		Search-engine friendly clone of the ACL2 documentation.

Lhs.lisp

Aliases-normorderedp-aux

Signature
(aliases-normorderedp-aux n aliases) → *
Arguments: n — Guard (natp n).

Definitions and Theorems

Function: aliases-normorderedp-aux

(defun aliases-normorderedp-aux (n aliases)
  (declare (xargs :stobjs (aliases)))
  (declare (xargs :guard (natp n)))
  (declare (xargs :guard (<= n (aliass-length aliases))))
  (let ((__function__ 'aliases-normorderedp-aux))
    (declare (ignorable __function__))
    (if (zp n)
        t
      (and (lhs-vars-normorderedp (1- n)
                                  0 (get-alias (1- n) aliases))
           (aliases-normorderedp-aux (1- n)
                                     aliases)))))

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

(defthm aliases-normorderedp-aux-of-nfix-n
  (equal (aliases-normorderedp-aux (nfix n)
                                   aliases)
         (aliases-normorderedp-aux n aliases)))

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

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

Theorem: aliases-normorderedp-aux-of-lhslist-fix-aliases

(defthm aliases-normorderedp-aux-of-lhslist-fix-aliases
  (equal (aliases-normorderedp-aux n (lhslist-fix aliases))
         (aliases-normorderedp-aux n aliases)))

Theorem: aliases-normorderedp-aux-lhslist-equiv-congruence-on-aliases

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

Definition: aliases-unnormorderedp-idx

(defchoose aliases-unnormorderedp-idx (idx)
                                      (aliases)
  (and (natp idx)
       (not (lhs-vars-normorderedp idx 0 (get-alias idx aliases)))))

Theorem: not-aliases-normorderedp-aux-implies-unnormorderedp-idx

(defthm not-aliases-normorderedp-aux-implies-unnormorderedp-idx
  (implies (not (aliases-normorderedp-aux n aliases))
           (let ((idx (aliases-unnormorderedp-idx aliases)))
             (not (lhs-vars-normorderedp (nfix idx)
                                         0 (nth idx aliases))))))

Theorem: aliases-normorderedp-aux-implies-get-alias

(defthm aliases-normorderedp-aux-implies-get-alias
  (implies (and (aliases-normorderedp-aux m aliases)
                (< (nfix n) (nfix m))
                (<= (nfix n) (ifix nn)))
           (lhs-vars-normorderedp nn 0 (nth n aliases))))