		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Elab-mod-instoffset

Signature
(elab-mod-instoffset instidx elab-mod) → *
Arguments: instidx — Guard (natp instidx).

Definitions and Theorems

Function: elab-mod-instoffset

(defun elab-mod-instoffset (instidx elab-mod)
  (declare (xargs :stobjs (elab-mod)))
  (declare (xargs :guard (natp instidx)))
  (declare (xargs :guard (<= instidx (elab-mod-ninsts elab-mod))))
  (let ((__function__ 'elab-mod-instoffset))
    (declare (ignorable __function__))
    (if (>= (lnfix instidx)
            (elab-mod-ninsts elab-mod))
        (elab-mod->totalinsts elab-mod)
      (elab-mod->inst-instoffset instidx elab-mod))))

Theorem: elab-mod-inst-instoffset-norm

(defthm elab-mod-inst-instoffset-norm
  (implies (< (nfix instidx)
              (elab-mod$a-ninsts elab-mod))
           (equal (elab-mod$a->inst-instoffset instidx elab-mod)
                  (elab-mod-instoffset instidx elab-mod))))

Theorem: elab-mod-totalinsts-norm

(defthm elab-mod-totalinsts-norm
  (equal (elab-mod$a->totalinsts elab-mod)
         (elab-mod-instoffset (elab-mod-ninsts elab-mod)
                              elab-mod)))

Theorem: elab-mod-instoffset-of-nfix-instidx

(defthm elab-mod-instoffset-of-nfix-instidx
  (equal (elab-mod-instoffset (nfix instidx)
                              elab-mod)
         (elab-mod-instoffset instidx elab-mod)))

Theorem: elab-mod-instoffset-nat-equiv-congruence-on-instidx

(defthm elab-mod-instoffset-nat-equiv-congruence-on-instidx
  (implies (nat-equiv instidx instidx-equiv)
           (equal (elab-mod-instoffset instidx elab-mod)
                  (elab-mod-instoffset instidx-equiv elab-mod)))
  :rule-classes :congruence)

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

(defthm elab-mod-instoffset-of-elab-mod$a-fix-elab-mod
  (equal (elab-mod-instoffset instidx (elab-mod$a-fix elab-mod))
         (elab-mod-instoffset instidx elab-mod)))

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

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