		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Elab-mod-wire-find-inst

Signature
(elab-mod-wire-find-inst wire elab-mod) → *
Arguments: wire — Guard (natp wire).; elab-mod — Guard (elab-mod-of-good-moddb elab-mod).

Definitions and Theorems

Function: elab-mod-wire-find-inst

(defun elab-mod-wire-find-inst (wire elab-mod)
 (declare (xargs :stobjs (elab-mod)))
 (declare (xargs :guard (and (natp wire)
                             (elab-mod-of-good-moddb elab-mod))))
 (declare
      (xargs :guard (and (<= (elab-mod-nwires elab-mod) wire)
                         (< wire (elab-mod->totalwires elab-mod)))))
 (let ((__function__ 'elab-mod-wire-find-inst))
  (declare (ignorable __function__))
  (flet
   ((fn
      (wire elab-mod)
      (if (<= (elab-mod-ninsts elab-mod) 1)
          0
        (elab-mod-wire-find-inst-aux (lnfix wire)
                                     0 (elab-mod-nwires elab-mod)
                                     (elab-mod-ninsts elab-mod)
                                     (elab-mod->totalwires elab-mod)
                                     t elab-mod))))
   (mbe :logic (non-exec (let ((elab-mod (elab-mod-fix elab-mod)))
                           (fn wire elab-mod)))
        :exec (fn wire elab-mod)))))

Theorem: elab-mod-wire-find-inst-upper-bound

(defthm elab-mod-wire-find-inst-upper-bound
  (implies (< 0 (elab-mod$a-ninsts elab-mod))
           (< (elab-mod-wire-find-inst wire elab-mod)
              (elab-mod$a-ninsts elab-mod)))
  :rule-classes (:rewrite :linear))

Theorem: elab-mod-wire-find-inst-correct1

(defthm elab-mod-wire-find-inst-correct1
 (implies
    (and (<= (elab-mod-nwires elab-mod)
             (nfix wire))
         (< (nfix wire)
            (elab-mod->totalwires elab-mod))
         (elab-mod-of-good-moddb elab-mod))
    (<= (elab-mod-wireoffset (elab-mod-wire-find-inst wire elab-mod)
                             elab-mod)
        (nfix wire)))
 :rule-classes :linear)

Theorem: elab-mod-wire-find-inst-correct2

(defthm elab-mod-wire-find-inst-correct2
 (implies
  (and (<= (elab-mod-nwires elab-mod)
           (nfix wire))
       (< (nfix wire)
          (elab-mod->totalwires elab-mod))
       (elab-mod-of-good-moddb elab-mod))
  (<
    (nfix wire)
    (elab-mod-wireoffset (+ 1
                            (elab-mod-wire-find-inst wire elab-mod))
                         elab-mod)))
 :rule-classes :linear)

Theorem: elab-mod-wire-find-inst-of-nfix-wire

(defthm elab-mod-wire-find-inst-of-nfix-wire
  (equal (elab-mod-wire-find-inst (nfix wire)
                                  elab-mod)
         (elab-mod-wire-find-inst wire elab-mod)))

Theorem: elab-mod-wire-find-inst-nat-equiv-congruence-on-wire

(defthm elab-mod-wire-find-inst-nat-equiv-congruence-on-wire
  (implies (nat-equiv wire wire-equiv)
           (equal (elab-mod-wire-find-inst wire elab-mod)
                  (elab-mod-wire-find-inst wire-equiv elab-mod)))
  :rule-classes :congruence)

Theorem: elab-mod-wire-find-inst-of-elab-mod$a-fix-elab-mod

(defthm elab-mod-wire-find-inst-of-elab-mod$a-fix-elab-mod
  (equal (elab-mod-wire-find-inst wire (elab-mod$a-fix elab-mod))
         (elab-mod-wire-find-inst wire elab-mod)))

Theorem: elab-mod-wire-find-inst-elab-mod$a-equiv-congruence-on-elab-mod

(defthm
    elab-mod-wire-find-inst-elab-mod$a-equiv-congruence-on-elab-mod
  (implies (elab-mod$a-equiv elab-mod elab-mod-equiv)
           (equal (elab-mod-wire-find-inst wire elab-mod)
                  (elab-mod-wire-find-inst wire elab-mod-equiv)))
  :rule-classes :congruence)