		Search-engine friendly clone of the ACL2 documentation.

Lhs.lisp

Aliases-vars

Signature
(aliases-vars lhsarr) → vars
Returns: vars — Type (svarlist-p vars).

Definitions and Theorems

Function: aliases-vars

(defun aliases-vars (lhsarr)
  (declare (xargs :stobjs (lhsarr)))
  (declare (xargs :guard t))
  (let ((__function__ 'aliases-vars))
    (declare (ignorable __function__))
    (aliases-vars-aux (lhss-length lhsarr)
                      lhsarr)))

Theorem: svarlist-p-of-aliases-vars

(defthm svarlist-p-of-aliases-vars
  (b* ((vars (aliases-vars lhsarr)))
    (svarlist-p vars))
  :rule-classes :rewrite)

Theorem: vars-of-get-lhs

(defthm vars-of-get-lhs
  (implies (not (member v (aliases-vars lhsarr)))
           (not (member v (lhs-vars (nth n lhsarr))))))

Theorem: aliases-vars-of-lhslist-fix-lhsarr

(defthm aliases-vars-of-lhslist-fix-lhsarr
  (equal (aliases-vars (lhslist-fix lhsarr))
         (aliases-vars lhsarr)))

Theorem: aliases-vars-lhslist-equiv-congruence-on-lhsarr

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