		Search-engine friendly clone of the ACL2 documentation.

Lhs.lisp

Aliases-vars-aux

Signature
(aliases-vars-aux n lhsarr) → vars
Arguments: n — Guard (natp n).
Returns: vars — Type (svarlist-p vars).

Definitions and Theorems

Function: aliases-vars-aux

(defun aliases-vars-aux (n lhsarr)
  (declare (xargs :stobjs (lhsarr)))
  (declare (xargs :guard (natp n)))
  (declare (xargs :guard (<= (lnfix n) (lhss-length lhsarr))))
  (let ((__function__ 'aliases-vars-aux))
    (declare (ignorable __function__))
    (if (zp n)
        nil
      (append (lhs-vars (get-lhs (1- n) lhsarr))
              (aliases-vars-aux (1- n) lhsarr)))))

Theorem: svarlist-p-of-aliases-vars-aux

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

Theorem: vars-of-get-lhs-aux

(defthm vars-of-get-lhs-aux
  (implies (and (not (member v (aliases-vars-aux n lhsarr)))
                (< (nfix m) (nfix n)))
           (not (member v (lhs-vars (nth m lhsarr))))))

Theorem: aliases-vars-aux-of-nfix-n

(defthm aliases-vars-aux-of-nfix-n
  (equal (aliases-vars-aux (nfix n) lhsarr)
         (aliases-vars-aux n lhsarr)))

Theorem: aliases-vars-aux-nat-equiv-congruence-on-n

(defthm aliases-vars-aux-nat-equiv-congruence-on-n
  (implies (nat-equiv n n-equiv)
           (equal (aliases-vars-aux n lhsarr)
                  (aliases-vars-aux n-equiv lhsarr)))
  :rule-classes :congruence)

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

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

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

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