		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Elab-mod$c->inst-wireoffset

Signature
(elab-mod$c->inst-wireoffset idx elab-mod$c) → *
Arguments: idx — Guard (natp idx).

Definitions and Theorems

Function: elab-mod$c->inst-wireoffset

(defun elab-mod$c->inst-wireoffset (idx elab-mod$c)
 (declare (xargs :stobjs (elab-mod$c)))
 (declare (xargs :guard (natp idx)))
 (declare
      (xargs :guard (and (elab-mod$c-modinsts-ok elab-mod$c)
                         (< idx (elab-mod$c->ninsts elab-mod$c)))))
 (let ((__function__ 'elab-mod$c->inst-wireoffset))
  (declare (ignorable __function__))
  (stobj-let
     ((elab-modinst$c (elab-mod$c->modinsttablei idx elab-mod$c)))
     (res)
     (mbe :logic (nfix (elab-modinst$c->wire-offset elab-modinst$c))
          :exec (elab-modinst$c->wire-offset elab-modinst$c))
     res)))

Theorem: elab-mod$c->inst-wireoffset-in-terms-of-abstraction

(defthm elab-mod$c->inst-wireoffset-in-terms-of-abstraction
 (implies
  (< (nfix idx)
     (nfix (nth *elab-mod$c->ninsts* elab-mod$c)))
  (equal
      (elab-mod$c->inst-wireoffset idx elab-mod$c)
      (nfix (nth *elab-modinst$c->wire-offset*
                 (nth idx
                      (elab-mod$c-inst-abstraction elab-mod$c)))))))

Theorem: elab-mod$c->inst-wireoffset-of-nfix-idx

(defthm elab-mod$c->inst-wireoffset-of-nfix-idx
  (equal (elab-mod$c->inst-wireoffset (nfix idx)
                                      elab-mod$c)
         (elab-mod$c->inst-wireoffset idx elab-mod$c)))

Theorem: elab-mod$c->inst-wireoffset-nat-equiv-congruence-on-idx

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