		Search-engine friendly clone of the ACL2 documentation.

Lhs->svex

Signature
(lhs->svex x) → xx
Arguments: x — Guard (lhs-p x).
Returns: xx — Type (svex-p xx).

Definitions and Theorems

Function: lhs->svex

(defun lhs->svex (x)
  (declare (xargs :guard (lhs-p x)))
  (let ((__function__ 'lhs->svex))
    (declare (ignorable __function__))
    (if (atom x)
        (svex-quote (4vec-z))
      (b* (((lhrange xf) (car x)))
        (svex-concat xf.w (lhatom->svex xf.atom)
                     (lhs->svex (cdr x)))))))

Theorem: svex-p-of-lhs->svex

(defthm svex-p-of-lhs->svex
  (b* ((xx (lhs->svex x))) (svex-p xx))
  :rule-classes :rewrite)

Theorem: lhs->svex-of-lhs-fix-x

(defthm lhs->svex-of-lhs-fix-x
  (equal (lhs->svex (lhs-fix x))
         (lhs->svex x)))

Theorem: lhs->svex-lhs-equiv-congruence-on-x

(defthm lhs->svex-lhs-equiv-congruence-on-x
  (implies (lhs-equiv x x-equiv)
           (equal (lhs->svex x)
                  (lhs->svex x-equiv)))
  :rule-classes :congruence)

Theorem: lhs->svex-correct

(defthm lhs->svex-correct
  (equal (svex-eval (lhs->svex x) env)
         (lhs-eval x env)))

Theorem: vars-of-lhs->svex

(defthm vars-of-lhs->svex
  (implies (not (member v (lhs-vars x)))
           (not (member v (svex-vars (lhs->svex x))))))