		Search-engine friendly clone of the ACL2 documentation.

Lhs.lisp

Aliases-normorderedp

Signature
(aliases-normorderedp aliases) → *

Definitions and Theorems

Function: aliases-normorderedp

(defun aliases-normorderedp (aliases)
  (declare (xargs :stobjs (aliases)))
  (declare (xargs :guard t))
  (let ((__function__ 'aliases-normorderedp))
    (declare (ignorable __function__))
    (and (aliasesp aliases)
         (aliases-normorderedp-aux (aliass-length aliases)
                                   aliases))))

Theorem: aliases-normorderedp-implies-get-alias

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

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

(defthm aliases-not-normorderedp-implies-unnormorderedp-idx
  (implies (and (not (aliases-normorderedp aliases))
                (lhslist-p aliases))
           (let ((idx (aliases-unnormorderedp-idx aliases)))
             (not (lhs-vars-normorderedp (nfix idx)
                                         0 (nth idx aliases))))))

Theorem: aliases-normorderedp-of-resize

(defthm aliases-normorderedp-of-resize
  (implies (aliases-normorderedp aliases)
           (aliases-normorderedp (resize-list aliases n nil))))

Theorem: aliases-normorderedp-of-update-nth

(defthm aliases-normorderedp-of-update-nth
  (implies (and (aliases-normorderedp aliases)
                (lhs-p x)
                (lhs-vars-normorderedp (nfix n) 0 x))
           (aliases-normorderedp (update-nth n x aliases))))

Theorem: aliases-normorderedp-of-replicate

(defthm aliases-normorderedp-of-replicate
  (aliases-normorderedp (replicate n nil)))