		Search-engine friendly clone of the ACL2 documentation.

Lhs.lisp

Lhs->svex-zero

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

Definitions and Theorems

Function: lhs->svex-zero

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

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

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

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

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

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

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

Theorem: lhs->svex-zero-correct

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

Theorem: vars-of-lhs->svex-zero

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