		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Elab-mod$a->inst-instoffset

Signature
(elab-mod$a->inst-instoffset idx elab-mod$a) → *
Arguments: idx — Guard (natp idx).; elab-mod$a — Guard (elab-mod$ap elab-mod$a).

Definitions and Theorems

Function: elab-mod$a->inst-instoffset

(defun elab-mod$a->inst-instoffset (idx elab-mod$a)
  (declare (xargs :guard (and (natp idx)
                              (elab-mod$ap elab-mod$a))))
  (declare (xargs :guard (< idx (elab-mod$a-ninsts elab-mod$a))))
  (let ((__function__ 'elab-mod$a->inst-instoffset))
    (declare (ignorable __function__))
    (nfix (nth *elab-modinst$c->inst-offset*
               (nth idx
                    (g :insts (elab-mod$a-fix elab-mod$a)))))))

Theorem: elab-mod$a->inst-instoffset-of-nfix-idx

(defthm elab-mod$a->inst-instoffset-of-nfix-idx
  (equal (elab-mod$a->inst-instoffset (nfix idx)
                                      elab-mod$a)
         (elab-mod$a->inst-instoffset idx elab-mod$a)))

Theorem: elab-mod$a->inst-instoffset-nat-equiv-congruence-on-idx

(defthm elab-mod$a->inst-instoffset-nat-equiv-congruence-on-idx
  (implies
       (nat-equiv idx idx-equiv)
       (equal (elab-mod$a->inst-instoffset idx elab-mod$a)
              (elab-mod$a->inst-instoffset idx-equiv elab-mod$a)))
  :rule-classes :congruence)

Theorem: elab-mod$a->inst-instoffset-of-elab-mod$a-fix-elab-mod$a

(defthm elab-mod$a->inst-instoffset-of-elab-mod$a-fix-elab-mod$a
  (equal
       (elab-mod$a->inst-instoffset idx (elab-mod$a-fix elab-mod$a))
       (elab-mod$a->inst-instoffset idx elab-mod$a)))

Theorem: elab-mod$a->inst-instoffset-elab-mod$a-equiv-congruence-on-elab-mod$a

(defthm
 elab-mod$a->inst-instoffset-elab-mod$a-equiv-congruence-on-elab-mod$a
 (implies
      (elab-mod$a-equiv elab-mod$a elab-mod$a-equiv)
      (equal (elab-mod$a->inst-instoffset idx elab-mod$a)
             (elab-mod$a->inst-instoffset idx elab-mod$a-equiv)))
 :rule-classes :congruence)