		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Elab-mod-wireoffset

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

Definitions and Theorems

Function: elab-mod-wireoffset

(defun elab-mod-wireoffset (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-wireoffset))
    (declare (ignorable __function__))
    (if (>= (lnfix instidx)
            (elab-mod-ninsts elab-mod))
        (elab-mod->totalwires elab-mod)
      (elab-mod->inst-wireoffset instidx elab-mod))))

Theorem: elab-mod-inst-wireoffset-norm

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

Theorem: elab-mod-totalwires-norm

(defthm elab-mod-totalwires-norm
  (nat-equiv (g :totalwires elab-mod)
             (elab-mod-wireoffset (elab-mod-ninsts elab-mod)
                                  elab-mod)))

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

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

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

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

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

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

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

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