		Search-engine friendly clone of the ACL2 documentation.

Process.lisp

Svtv-baseentry-svex

Signature
(svtv-baseentry-svex ent) → expr
Arguments: ent — Guard (svtv-baseentry-p ent).
Returns: expr — Type (svex-p expr).

Definitions and Theorems

Function: svtv-baseentry-svex

(defun svtv-baseentry-svex (ent)
  (declare (xargs :guard (svtv-baseentry-p ent)))
  (let ((__function__ 'svtv-baseentry-svex))
    (declare (ignorable __function__))
    (b* ((ent (svtv-baseentry-fix ent)))
      (cond ((4vec-p ent) (svex-quote ent))
            ((eq ent 'x) (svex-quote (4vec-x)))
            ((eq ent :ones) (svex-quote -1))
            (t (svex-var ent))))))

Theorem: svex-p-of-svtv-baseentry-svex

(defthm svex-p-of-svtv-baseentry-svex
  (b* ((expr (svtv-baseentry-svex ent)))
    (svex-p expr))
  :rule-classes :rewrite)

Theorem: svtv-baseentry-svex-of-svtv-baseentry-fix-ent

(defthm svtv-baseentry-svex-of-svtv-baseentry-fix-ent
  (equal (svtv-baseentry-svex (svtv-baseentry-fix ent))
         (svtv-baseentry-svex ent)))

Theorem: svtv-baseentry-svex-svtv-baseentry-equiv-congruence-on-ent

(defthm svtv-baseentry-svex-svtv-baseentry-equiv-congruence-on-ent
  (implies (svtv-baseentry-equiv ent ent-equiv)
           (equal (svtv-baseentry-svex ent)
                  (svtv-baseentry-svex ent-equiv)))
  :rule-classes :congruence)