		Search-engine friendly clone of the ACL2 documentation.

Alias-norm.lisp

Getalias

Signature
(getalias n aliases) → lhs
Arguments: n — Guard (natp n).; aliases — Guard (aliases-normorderedp aliases).
Returns: lhs — Type (and (lhs-p lhs) (implies (natp n) (lhs-vars-normorderedp n 0 lhs))).

Definitions and Theorems

Function: getalias$inline

(defun getalias$inline (n aliases)
  (declare (xargs :stobjs (aliases)))
  (declare (xargs :guard (and (natp n)
                              (aliases-normorderedp aliases))))
  (declare (xargs :guard (< n (aliass-length aliases))))
  (let ((__function__ 'getalias))
    (declare (ignorable __function__))
    (mbe :logic (lhs-varbound-fix (nfix n)
                                  0 (get-alias n aliases))
         :exec (get-alias n aliases))))

Theorem: return-type-of-getalias

(defthm return-type-of-getalias
  (b* ((lhs (getalias$inline n aliases)))
    (and (lhs-p lhs)
         (implies (natp n)
                  (lhs-vars-normorderedp n 0 lhs))))
  :rule-classes :rewrite)

Theorem: getalias$inline-of-nfix-n

(defthm getalias$inline-of-nfix-n
  (equal (getalias$inline (nfix n) aliases)
         (getalias$inline n aliases)))

Theorem: getalias$inline-nat-equiv-congruence-on-n

(defthm getalias$inline-nat-equiv-congruence-on-n
  (implies (nat-equiv n n-equiv)
           (equal (getalias$inline n aliases)
                  (getalias$inline n-equiv aliases)))
  :rule-classes :congruence)

Theorem: getalias$inline-of-aliases-bound-fix-aliases

(defthm getalias$inline-of-aliases-bound-fix-aliases
  (equal (getalias$inline n (aliases-bound-fix aliases))
         (getalias$inline n aliases)))

Theorem: getalias$inline-aliases-equiv-congruence-on-aliases

(defthm getalias$inline-aliases-equiv-congruence-on-aliases
  (implies (aliases-equiv aliases aliases-equiv)
           (equal (getalias$inline n aliases)
                  (getalias$inline n aliases-equiv)))
  :rule-classes :congruence)