		Search-engine friendly clone of the ACL2 documentation.

Lhs.lisp

Lhatom-vars

Signature
(lhatom-vars x) → vars
Arguments: x — Guard (lhatom-p x).
Returns: vars — Type (svarlist-p vars).

Definitions and Theorems

Function: lhatom-vars

(defun lhatom-vars (x)
  (declare (xargs :guard (lhatom-p x)))
  (let ((__function__ 'lhatom-vars))
    (declare (ignorable __function__))
    (lhatom-case x
                 :z nil
                 :var (list x.name))))

Theorem: svarlist-p-of-lhatom-vars

(defthm svarlist-p-of-lhatom-vars
  (b* ((vars (lhatom-vars x)))
    (svarlist-p vars))
  :rule-classes :rewrite)

Theorem: vars-of-lhrange-combine

(defthm vars-of-lhrange-combine
 (implies
   (lhrange-combine x y)
   (iff (member v
                (lhatom-vars (lhrange->atom (lhrange-combine x y))))
        (member v (lhatom-vars (lhrange->atom x))))))

Theorem: lhatom-vars-of-lhatom-fix-x

(defthm lhatom-vars-of-lhatom-fix-x
  (equal (lhatom-vars (lhatom-fix x))
         (lhatom-vars x)))

Theorem: lhatom-vars-lhatom-equiv-congruence-on-x

(defthm lhatom-vars-lhatom-equiv-congruence-on-x
  (implies (lhatom-equiv x x-equiv)
           (equal (lhatom-vars x)
                  (lhatom-vars x-equiv)))
  :rule-classes :congruence)