		Search-engine friendly clone of the ACL2 documentation.

Lhs.lisp

Lhslist-vars

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

Definitions and Theorems

Function: lhslist-vars

(defun lhslist-vars (x)
  (declare (xargs :guard (lhslist-p x)))
  (let ((__function__ 'lhslist-vars))
    (declare (ignorable __function__))
    (if (atom x)
        nil
      (append (lhs-vars (car x))
              (lhslist-vars (cdr x))))))

Theorem: svarlist-p-of-lhslist-vars

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

Theorem: lhslist-vars-of-append

(defthm lhslist-vars-of-append
  (equal (lhslist-vars (append a b))
         (append (lhslist-vars a)
                 (lhslist-vars b))))

Theorem: lhslist-vars-of-lhslist-fix-x

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

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

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