		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Moddb-mod-inst-instoffset

Signature
(moddb-mod-inst-instoffset instidx modidx moddb) → offset
Arguments: instidx — Guard (natp instidx).; modidx — Guard (natp modidx).
Returns: offset — Type (natp offset).

Definitions and Theorems

Function: moddb-mod-inst-instoffset

(defun moddb-mod-inst-instoffset (instidx modidx moddb)
 (declare (xargs :stobjs (moddb)))
 (declare (xargs :guard (and (natp instidx) (natp modidx))))
 (declare
  (xargs
     :guard (and (< modidx (moddb->nmods moddb))
                 (<= (moddb->nmods moddb)
                     (moddb->mods-length moddb))
                 (moddb-mod-order-ok modidx moddb)
                 (stobj-let ((elab-mod (moddb->modsi modidx moddb)))
                            (ok)
                            (<= instidx (elab-mod-ninsts elab-mod))
                            ok))))
 (let ((__function__ 'moddb-mod-inst-instoffset))
  (declare (ignorable __function__))
  (b*
   (((unless (mbt (< (lnfix modidx)
                     (lnfix (moddb->nmods moddb)))))
     0)
    (instidx
       (mbe :logic
            (min (nfix instidx)
                 (stobj-let ((elab-mod (moddb->modsi modidx moddb)))
                            (ninsts)
                            (elab-mod-ninsts elab-mod)
                            ninsts))
            :exec instidx))
    ((when (zp instidx)) 0)
    (prev-instidx (1- instidx))
    ((stobj-get prevoffset instmod)
     ((elab-mod (moddb->modsi modidx moddb)))
     (mv (elab-mod->inst-instoffset prev-instidx elab-mod)
         (elab-mod->inst-modidx prev-instidx elab-mod)))
    ((unless (mbt (< instmod (lnfix modidx))))
     (+ 1 prevoffset))
    ((stobj-get inst-totalinsts)
     ((elab-mod (moddb->modsi instmod moddb)))
     (elab-mod->totalinsts elab-mod)))
   (+ 1 prevoffset inst-totalinsts))))

Theorem: natp-of-moddb-mod-inst-instoffset

(defthm natp-of-moddb-mod-inst-instoffset
  (b* ((offset (moddb-mod-inst-instoffset instidx modidx moddb)))
    (natp offset))
  :rule-classes :type-prescription)

Theorem: moddb-mod-inst-instoffset-of-nfix-instidx

(defthm moddb-mod-inst-instoffset-of-nfix-instidx
  (equal (moddb-mod-inst-instoffset (nfix instidx)
                                    modidx moddb)
         (moddb-mod-inst-instoffset instidx modidx moddb)))

Theorem: moddb-mod-inst-instoffset-nat-equiv-congruence-on-instidx

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

Theorem: moddb-mod-inst-instoffset-of-nfix-modidx

(defthm moddb-mod-inst-instoffset-of-nfix-modidx
  (equal (moddb-mod-inst-instoffset instidx (nfix modidx)
                                    moddb)
         (moddb-mod-inst-instoffset instidx modidx moddb)))

Theorem: moddb-mod-inst-instoffset-nat-equiv-congruence-on-modidx

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

Theorem: moddb-mod-inst-instoffset-of-moddb-fix-moddb

(defthm moddb-mod-inst-instoffset-of-moddb-fix-moddb
 (equal (moddb-mod-inst-instoffset instidx modidx (moddb-fix moddb))
        (moddb-mod-inst-instoffset instidx modidx moddb)))

Theorem: moddb-mod-inst-instoffset-moddb-equiv-congruence-on-moddb

(defthm moddb-mod-inst-instoffset-moddb-equiv-congruence-on-moddb
 (implies
     (moddb-equiv moddb moddb-equiv)
     (equal (moddb-mod-inst-instoffset instidx modidx moddb)
            (moddb-mod-inst-instoffset instidx modidx moddb-equiv)))
 :rule-classes :congruence)

Theorem: moddb-mod-inst-instoffset-of-moddb-norm-moddb

(defthm moddb-mod-inst-instoffset-of-moddb-norm-moddb
  (equal (moddb-mod-inst-instoffset idx modidx (moddb-norm moddb))
         (moddb-mod-inst-instoffset idx modidx moddb)))

Theorem: moddb-mod-inst-instoffset-moddb-norm-equiv-congruence-on-moddb

(defthm
     moddb-mod-inst-instoffset-moddb-norm-equiv-congruence-on-moddb
  (implies
       (moddb-norm-equiv moddb moddb-equiv)
       (equal (moddb-mod-inst-instoffset idx modidx moddb)
              (moddb-mod-inst-instoffset idx modidx moddb-equiv)))
  :rule-classes :congruence)