• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
      • Svex-stvs
      • Svex-decomposition-methodology
      • Sv-versus-esim
      • Svex-decomp
      • Svex-compose-dfs
      • Svex-compilation
      • Moddb
        • Moddb.lisp
          • Moddb-add-modinst-to-last
          • Moddb-add-module1
          • Moddb-norm
          • Elab-modlist-norm
          • Moddb-ok
          • Elab-modinsts-rem-dups
          • Moddb-add-modinst
          • Elab-mod-initialize-aliases
          • Modinstlist-add-modinsts
          • Moddb-mod-ok
          • Wirelist-rem-dups
          • Moddb-norm-p
          • Elab-mod$a-fix
          • Moddb-mod-order-ok
          • Moddb-mod-insts-ok
          • Elab-mod-wire-find-inst-aux
          • Svex-alist->absindexed
          • Modscope-push-frame
          • Moddb-modinst-ok
          • Lhspairs->absindexed
          • Moddb-mod-inst-wireoffset
          • Moddb-find-bad-modinst-order
          • Constraintlist->absindexed
          • Wirelist-remove-names
          • Moddb-mod-inst-instoffset
          • Lhspairs-named->indexed
          • Elab-modinst-fix
          • Moddb-mod-totalwires
          • Svar-map->absindexed
          • Moddb-modinst-order-ok
          • Moddb-mod-totalinsts
          • Moddb-find-bad-modinst
          • Modscope
          • Constraintlist-named->indexed
          • Assigns->absindexed
          • Moddb-indices-ok
          • Lhs->absindexed
          • Svar-map-named->indexed
          • Module-named->indexed
          • Moddb-find-bad-index
          • Assigns-named->indexed
          • Svar-named->indexed
          • Lhs-named->indexed
          • Elab-mod$c-add-wire
          • Moddb-modname-get-index
          • Moddb-maybe-grow
          • Lhspairs-named->indexed-aux-nrev
          • Elab-modinst-list-names
          • Elab-mod-wire-find-inst
          • Svar->absindexed
          • Moddb-path->wiredecl
          • Modalist-named->indexed
          • Lhspairs->absindexed-nrev
          • Elab-mod$ap
          • Elab-modinst-remove-names
          • Moddb-wireidx->paths
          • Moddb-mods-ok
          • Moddb-find-bad-mod
          • Elab-mod$c-add-inst
          • Elab-mod$c-modinsts-ok
          • Elab-modinst-remove-name
          • Modscope->nth
          • Moddb-basics-ok
          • Svex->absindexed-memo-ok
          • Svex-named->indexed-memo-ok
          • Svarlist-idxaddr-okp
          • Elab-modlist-normp
          • Wirelist-remove-name
          • Modscope->top
          • Moddb-fix
          • Elab-mod$a-add-inst
          • Elab-mod-wiresearch-smartpivot
          • Elab-mod$c-wires-ok
          • Update-elab-mod$a->totalwires
          • Update-elab-mod$a->totalinsts
          • Update-elab-mod$a->orig-mod
          • Update-elab-mod$a->name
          • Moddb-modinst-order-badguy
          • Elab-mod$a-add-wire
          • Elab-mod$a-wiretablei
          • Elab-mod-wiresearch-pivot
          • Elab-mod-wireoffset
          • Elab-mod-instoffset
          • Svar-idxaddr-okp
          • Paths-add-scope
          • Moddb-modinst-badguy
          • Moddb-mod-nwires
          • Moddb-mod-ninsts
          • Modalist-all-idxaddr-okp
          • Elab-mod$a->instname
          • Elab-mods->names
          • Elab-modinst$c-copy
          • Elab-mod$a->inst-wireoffset
          • Elab-mod$a->inst-instoffset
          • Moddb-elab-mod-stats
          • Moddb-contains-modnames
          • Elab-mod$c-inst-abstraction
          • Elab-mod$a->inst-modidx
          • Elab-mod$a-wirename->idx
          • Elab-mod$a-instname->idx
          • Elab-mod-add-wires
          • Modscope-top-bound
          • Modscope-local-bound
          • Constraintlist-add-scope
          • Moddb-modidx-get-name
          • Moddb-add-module
          • Elab-mod-wiresearch-dumbpivot
          • Update-moddb->nmods
          • Elab-mod$c->inst-wireoffset
          • Elab-mod$c->inst-modidx
          • Elab-mod$c->inst-instoffset
          • Elab-mod$c-wire-abstraction
          • Moddb-clear
          • Elab-mod$c->instname
          • Svex-mod->flatten
          • Names->paths
          • Modscope->wireoffset
          • Modscope->instoffset
          • Moddb-mod-badguy
          • Elab-modinsts-nodups-p
          • Wirelist-nodups-p
          • Nat-list-max
          • Modscope->modidx
          • Elab-mod-wiresearch-next-smartp
          • Elab-mod$a->totalwires
          • Elab-mod$a->totalinsts
          • Elab-mod$a->orig-mod
          • Elab-mod$a->name
          • Elab-mod$a-nwires
          • Elab-mod$a-ninsts
          • Elab-modinst$c-fix
          • Elab-mod-fix
          • Create-elab-mod$a
          • Pathlist
          • Module->db
          • Elab-modlist
          • Elab-modinst-list
          • Nrec-list-mods
          • Moddb->nmods
          • Nrec-list
          • Nrec
        • Elab-mod
        • Moddb-path->wireidx/decl
        • Moddb-wireidx->path/decl
        • Moddb-path->wireidx
        • Moddb-address->wireidx
        • Moddb-address->wiredecl
        • Moddb-wireidx->path
        • Modscope-okp
      • Svmods
      • Svstmt
      • Sv-tutorial
      • Expressions
      • Symbolic-test-vector
      • Vl-to-svex
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Moddb.lisp

Moddb-add-modinst-to-last

Signature

(moddb-add-modinst-to-last instname modidx moddb) → moddb

Arguments

instname — Guard (name-p instname).

modidx — instantiated module.
    Guard (natp modidx).

Definitions and Theorems

Function: moddb-add-modinst-to-last

(defun moddb-add-modinst-to-last (instname modidx moddb)
 (declare (xargs :stobjs (moddb)))
 (declare (xargs :guard (and (name-p instname) (natp modidx))))
 (declare
      (xargs :guard (and (moddb-ok moddb)
                         (< modidx (+ -1 (moddb->nmods moddb))))))
 (let ((__function__ 'moddb-add-modinst-to-last))
  (declare (ignorable __function__))
  (flet
   ((body
     (instname modidx moddb)
     (b*
      ((instname (mbe :logic (name-fix instname)
                      :exec instname))
       (modidx (lnfix modidx))
       ((unless (mbt (< 0 (moddb->nmods moddb))))
        moddb)
       (modified-modidx (1- (moddb->nmods moddb)))
       ((acl2::local-stobjs elab-modinst$c)
        (mv moddb elab-modinst$c))
       (elab-modinst$c
          (update-elab-modinst$c->instname instname elab-modinst$c))
       (elab-modinst$c
            (update-elab-modinst$c->modidx modidx elab-modinst$c))
       ((stobj-get subwires subinsts)
        ((elab-mod2 (moddb->modsi modidx moddb)))
        (mv (elab-mod->totalwires elab-mod2)
            (elab-mod->totalinsts elab-mod2)))
       ((mv subwires subinsts)
        (if (mbt (< modidx modified-modidx))
            (mv subwires subinsts)
          (mv 0 0))))
      (stobj-let
       ((elab-mod (moddb->modsi modified-modidx moddb)))
       (elab-mod elab-modinst$c)
       (b*
        (((when (elab-mod-instname->idx instname elab-mod))
          (mv elab-mod elab-modinst$c))
         (totalwires (elab-mod->totalwires elab-mod))
         (totalinsts (elab-mod->totalinsts elab-mod))
         (elab-modinst$c (update-elab-modinst$c->wire-offset
                              totalwires elab-modinst$c))
         (elab-mod
              (update-elab-mod->totalwires (+ totalwires subwires)
                                           elab-mod))
         (elab-modinst$c (update-elab-modinst$c->inst-offset
                              totalinsts elab-modinst$c))
         (elab-mod
              (update-elab-mod->totalinsts (+ 1 totalinsts subinsts)
                                           elab-mod))
         (elab-mod (elab-mod-add-inst elab-modinst$c elab-mod)))
        (mv elab-mod elab-modinst$c))
       (mv moddb elab-modinst$c)))))
   (mbe :logic (non-exec (let ((moddb (moddb-fix moddb)))
                           (body instname modidx moddb)))
        :exec (body instname modidx moddb)))))

Theorem: len-of-cons

(defthm len-of-cons
  (equal (len (cons a b)) (+ 1 (len b))))

Theorem: moddb-add-modinst-to-last-of-name-fix-instname

(defthm moddb-add-modinst-to-last-of-name-fix-instname
  (equal (moddb-add-modinst-to-last (name-fix instname)
                                    modidx moddb)
         (moddb-add-modinst-to-last instname modidx moddb)))

Theorem: moddb-add-modinst-to-last-name-equiv-congruence-on-instname

(defthm moddb-add-modinst-to-last-name-equiv-congruence-on-instname
 (implies
    (name-equiv instname instname-equiv)
    (equal (moddb-add-modinst-to-last instname modidx moddb)
           (moddb-add-modinst-to-last instname-equiv modidx moddb)))
 :rule-classes :congruence)

Theorem: moddb-add-modinst-to-last-of-nfix-modidx

(defthm moddb-add-modinst-to-last-of-nfix-modidx
  (equal (moddb-add-modinst-to-last instname (nfix modidx)
                                    moddb)
         (moddb-add-modinst-to-last instname modidx moddb)))

Theorem: moddb-add-modinst-to-last-nat-equiv-congruence-on-modidx

(defthm moddb-add-modinst-to-last-nat-equiv-congruence-on-modidx
 (implies
    (nat-equiv modidx modidx-equiv)
    (equal (moddb-add-modinst-to-last instname modidx moddb)
           (moddb-add-modinst-to-last instname modidx-equiv moddb)))
 :rule-classes :congruence)

Theorem: moddb-add-modinst-to-last-of-moddb-fix-moddb

(defthm moddb-add-modinst-to-last-of-moddb-fix-moddb
  (equal
       (moddb-add-modinst-to-last instname modidx (moddb-fix moddb))
       (moddb-add-modinst-to-last instname modidx moddb)))

Theorem: moddb-add-modinst-to-last-moddb-equiv-congruence-on-moddb

(defthm moddb-add-modinst-to-last-moddb-equiv-congruence-on-moddb
 (implies
    (moddb-equiv moddb moddb-equiv)
    (equal (moddb-add-modinst-to-last instname modidx moddb)
           (moddb-add-modinst-to-last instname modidx moddb-equiv)))
 :rule-classes :congruence)

Theorem: moddb-add-modinst-to-last-of-moddb-norm-moddb-under-moddb-norm-equiv

(defthm
 moddb-add-modinst-to-last-of-moddb-norm-moddb-under-moddb-norm-equiv
 (moddb-norm-equiv
      (moddb-add-modinst-to-last instname modidx (moddb-norm moddb))
      (moddb-add-modinst-to-last instname modidx moddb)))

Theorem: moddb-add-modinst-to-last-moddb-norm-equiv-congruence-on-moddb-under-moddb-norm-equiv

(defthm
 moddb-add-modinst-to-last-moddb-norm-equiv-congruence-on-moddb-under-moddb-norm-equiv
 (implies
      (moddb-norm-equiv moddb moddb-equiv)
      (moddb-norm-equiv
           (moddb-add-modinst-to-last instname modidx moddb)
           (moddb-add-modinst-to-last instname modidx moddb-equiv)))
 :rule-classes :congruence)

Theorem: moddb-add-modinst-to-last-basics-ok

(defthm moddb-add-modinst-to-last-basics-ok
  (implies (moddb-basics-ok moddb)
           (moddb-basics-ok
                (moddb-add-modinst-to-last instname modidx moddb))))

Theorem: g-of-elab-mod$a-fix-elab-mod-under-nat-equiv

(defthm acl2::g-of-elab-mod$a-fix-elab-mod-under-nat-equiv
  (nat-equiv (g :totalwires (elab-mod$a-fix elab-mod))
             (g :totalwires elab-mod)))

Theorem: g-elab-mod$a-equiv-congruence-on-elab-mod-under-nat-equiv

(defthm
    acl2::g-elab-mod$a-equiv-congruence-on-elab-mod-under-nat-equiv
  (implies (elab-mod$a-equiv elab-mod acl2::elab-mod-equiv)
           (nat-equiv (g :totalwires elab-mod)
                      (g :totalwires acl2::elab-mod-equiv)))
  :rule-classes :congruence)

Theorem: g-of-elab-mod$a-fix-elab-mod-under-nat-equiv-insts

(defthm acl2::g-of-elab-mod$a-fix-elab-mod-under-nat-equiv-insts
  (nat-equiv (g :totalinsts (elab-mod$a-fix elab-mod))
             (g :totalinsts elab-mod)))

Theorem: g-elab-mod$a-equiv-congruence-on-elab-mod-under-nat-equiv-insts

(defthm
 acl2::g-elab-mod$a-equiv-congruence-on-elab-mod-under-nat-equiv-insts
 (implies (elab-mod$a-equiv elab-mod acl2::elab-mod-equiv)
          (nat-equiv (g :totalinsts elab-mod)
                     (g :totalinsts acl2::elab-mod-equiv)))
 :rule-classes :congruence)

Theorem: moddb-modinst-order-ok-of-update-other-module

(defthm moddb-modinst-order-ok-of-update-other-module
  (implies (not (equal (nfix modmodidx) (nfix modidx)))
           (equal (moddb-modinst-order-ok
                       inst modidx
                       (update-nth *moddb->modsi*
                                   (update-nth modmodidx mod mods)
                                   moddb))
                  (moddb-modinst-order-ok
                       inst modidx
                       (update-nth *moddb->modsi* mods moddb)))))

Theorem: moddb-modinst-order-ok-of-nrec-list-mods

(defthm moddb-modinst-order-ok-of-nrec-list-mods
 (equal
    (moddb-modinst-order-ok inst
                            modidx (nrec-list-mods '(:insts) moddb))
    (moddb-modinst-order-ok inst modidx moddb)))

Theorem: moddb-modinst-order-ok-apply-nrec

(defthm moddb-modinst-order-ok-apply-nrec
 (implies
  (and (bind-free (nrec-list-mods_unfix moddb '(:insts)
                                        moddb '|MODDB-wrapped?|
                                        '|MODDB-unwrapped|
                                        '|MODDB-hyps|)
                  (|MODDB-wrapped?| |MODDB-unwrapped| |MODDB-hyps|))
       (equal |MDB-wrapped|
              (if |MODDB-wrapped?| moddb
                (nrec-list-mods '(:insts) moddb)))
       (bind-free (nrec-list-mods_unfix |MDB-wrapped| '(:insts)
                                        moddb '|MDB-wrapped?|
                                        'mdb
                                        '|MDB-wrapped-hyps|)
                  (|MDB-wrapped?| mdb |MDB-wrapped-hyps|))
       (nrec-list-mods_unfix_check |MDB-wrapped?| |MDB-wrapped|
                                   mdb |MDB-wrapped-hyps| '(:insts)
                                   moddb)
       (syntaxp (or (not (equal moddb mdb)))))
  (equal
    (moddb-modinst-order-ok inst modidx moddb)
    (acl2::skip-rewrite (moddb-modinst-order-ok inst modidx mdb)))))

Theorem: elab-mod$a-ninsts-of-nrec

(defthm elab-mod$a-ninsts-of-nrec
  (equal (elab-mod$a-ninsts (nrec '(:insts) x))
         (elab-mod$a-ninsts x)))

Theorem: elab-mod$a-ninsts-apply-nrec

(defthm elab-mod$a-ninsts-apply-nrec
 (implies
  (and
    (bind-free
         (nrec_unfix elab-mod '(:insts)
                     elab-mod '|ELAB-MOD-wrapped?|
                     '|ELAB-MOD-unwrapped|
                     '|ELAB-MOD-hyps|)
         (|ELAB-MOD-wrapped?| |ELAB-MOD-unwrapped| |ELAB-MOD-hyps|))
    (equal |ELMO-wrapped|
           (if |ELAB-MOD-wrapped?| elab-mod
             (nrec '(:insts) elab-mod)))
    (bind-free (nrec_unfix |ELMO-wrapped| '(:insts)
                           elab-mod '|ELMO-wrapped?|
                           'elmo
                           '|ELMO-wrapped-hyps|)
               (|ELMO-wrapped?| elmo |ELMO-wrapped-hyps|))
    (nrec_unfix_check |ELMO-wrapped?| |ELMO-wrapped|
                      elmo |ELMO-wrapped-hyps| '(:insts)
                      elab-mod)
    (syntaxp (or (not (equal elab-mod elmo)))))
  (equal (elab-mod$a-ninsts elab-mod)
         (acl2::skip-rewrite (elab-mod$a-ninsts elmo)))))

Theorem: moddb-mod-inst-wireoffset-of-update-later-module

(defthm moddb-mod-inst-wireoffset-of-update-later-module
  (implies (case-split (> (nfix modmodidx) (nfix modidx)))
           (equal (moddb-mod-inst-wireoffset
                       inst modidx
                       (update-nth *moddb->modsi*
                                   (update-nth modmodidx mod mods)
                                   moddb))
                  (moddb-mod-inst-wireoffset
                       inst modidx
                       (update-nth *moddb->modsi* mods moddb)))))

Theorem: moddb-mod-inst-instoffset-of-update-later-module

(defthm moddb-mod-inst-instoffset-of-update-later-module
  (implies (case-split (> (nfix modmodidx) (nfix modidx)))
           (equal (moddb-mod-inst-instoffset
                       inst modidx
                       (update-nth *moddb->modsi*
                                   (update-nth modmodidx mod mods)
                                   moddb))
                  (moddb-mod-inst-instoffset
                       inst modidx
                       (update-nth *moddb->modsi* mods moddb)))))

Theorem: moddb-modinst-ok-of-update-later-module

(defthm moddb-modinst-ok-of-update-later-module
 (implies
  (case-split (> (nfix modmodidx) (nfix modidx)))
  (equal
       (moddb-modinst-ok inst modidx
                         (update-nth *moddb->modsi*
                                     (update-nth modmodidx mod mods)
                                     moddb))
       (moddb-modinst-ok inst modidx
                         (update-nth *moddb->modsi* mods moddb)))))

Theorem: moddb-mod-inst-instoffset-of-update-later

(defthm moddb-mod-inst-instoffset-of-update-later
 (implies
  (and (case-split (< (nfix instidx)
                      (elab-mod$a-ninsts mod))))
  (equal
   (moddb-mod-inst-instoffset
       instidx modidx
       (update-nth *moddb->modsi*
                   (update-nth modidx (elab-mod$a-add-inst inst mod)
                               mods)
                   moddb))
   (moddb-mod-inst-instoffset
        instidx modidx
        (update-nth *moddb->modsi*
                    (update-nth modidx mod mods)
                    moddb)))))

Theorem: moddb-mod-inst-wireoffset-of-update-later

(defthm moddb-mod-inst-wireoffset-of-update-later
 (implies
  (and (case-split (< (nfix instidx)
                      (elab-mod$a-ninsts mod))))
  (equal
   (moddb-mod-inst-wireoffset
       instidx modidx
       (update-nth *moddb->modsi*
                   (update-nth modidx (elab-mod$a-add-inst inst mod)
                               mods)
                   moddb))
   (moddb-mod-inst-wireoffset
        instidx modidx
        (update-nth *moddb->modsi*
                    (update-nth modidx mod mods)
                    moddb)))))

Theorem: moddb-mod-inst-wireoffset-of-update-mod-nrec

(defthm moddb-mod-inst-wireoffset-of-update-mod-nrec
 (equal
     (moddb-mod-inst-wireoffset
          instidx modidx
          (update-nth *moddb->modsi*
                      (update-nth modidx (nrec '(:insts :wires) mod)
                                  mods)
                      moddb))
     (moddb-mod-inst-wireoffset
          instidx modidx
          (update-nth *moddb->modsi*
                      (update-nth modidx mod mods)
                      moddb))))

Theorem: moddb-mod-inst-wireoffset-of-update-mod-propagate-nrec

(defthm moddb-mod-inst-wireoffset-of-update-mod-propagate-nrec
 (implies
  (and
   (bind-free
      (nrec_unfix mod '(:insts :wires)
                  mod 'acl2::|MOD-wrapped?|
                  'acl2::|MOD-unwrapped|
                  'acl2::|MOD-hyps|)
      (acl2::|MOD-wrapped?| acl2::|MOD-unwrapped| acl2::|MOD-hyps|))
   (equal |M-wrapped|
          (if acl2::|MOD-wrapped?| mod
            (nrec '(:insts :wires) mod)))
   (bind-free (nrec_unfix |M-wrapped| '(:insts :wires)
                          mod '|M-wrapped?|
                          'm
                          '|M-wrapped-hyps|)
              (|M-wrapped?| m |M-wrapped-hyps|))
   (nrec_unfix_check |M-wrapped?| |M-wrapped|
                     m |M-wrapped-hyps| '(:insts :wires)
                     mod)
   (syntaxp (or (not (equal mod m)))))
  (equal
     (moddb-mod-inst-wireoffset
          instidx modidx
          (update-nth *moddb->modsi*
                      (update-nth modidx mod mods)
                      moddb))
     (acl2::skip-rewrite (moddb-mod-inst-wireoffset
                              instidx modidx
                              (update-nth *moddb->modsi*
                                          (update-nth modidx m mods)
                                          moddb))))))

Theorem: moddb-mod-inst-instoffset-of-update-mod-nrec

(defthm moddb-mod-inst-instoffset-of-update-mod-nrec
 (equal
     (moddb-mod-inst-instoffset
          instidx modidx
          (update-nth *moddb->modsi*
                      (update-nth modidx (nrec '(:insts :wires) mod)
                                  mods)
                      moddb))
     (moddb-mod-inst-instoffset
          instidx modidx
          (update-nth *moddb->modsi*
                      (update-nth modidx mod mods)
                      moddb))))

Theorem: moddb-mod-inst-instoffset-of-update-mod-propagate-nrec

(defthm moddb-mod-inst-instoffset-of-update-mod-propagate-nrec
 (implies
  (and
   (bind-free
      (nrec_unfix mod '(:insts :wires)
                  mod 'acl2::|MOD-wrapped?|
                  'acl2::|MOD-unwrapped|
                  'acl2::|MOD-hyps|)
      (acl2::|MOD-wrapped?| acl2::|MOD-unwrapped| acl2::|MOD-hyps|))
   (equal |M-wrapped|
          (if acl2::|MOD-wrapped?| mod
            (nrec '(:insts :wires) mod)))
   (bind-free (nrec_unfix |M-wrapped| '(:insts :wires)
                          mod '|M-wrapped?|
                          'm
                          '|M-wrapped-hyps|)
              (|M-wrapped?| m |M-wrapped-hyps|))
   (nrec_unfix_check |M-wrapped?| |M-wrapped|
                     m |M-wrapped-hyps| '(:insts :wires)
                     mod)
   (syntaxp (or (not (equal mod m)))))
  (equal
     (moddb-mod-inst-instoffset
          instidx modidx
          (update-nth *moddb->modsi*
                      (update-nth modidx mod mods)
                      moddb))
     (acl2::skip-rewrite (moddb-mod-inst-instoffset
                              instidx modidx
                              (update-nth *moddb->modsi*
                                          (update-nth modidx m mods)
                                          moddb))))))

Theorem: moddb-modinst-ok-of-add-inst-nrec

(defthm moddb-modinst-ok-of-add-inst-nrec
 (equal
     (moddb-modinst-ok
          instidx modidx
          (update-nth *moddb->modsi*
                      (update-nth modidx (nrec '(:insts :wires) mod)
                                  mods)
                      moddb))
     (moddb-modinst-ok instidx modidx
                       (update-nth *moddb->modsi*
                                   (update-nth modidx mod mods)
                                   moddb))))

Theorem: moddb-modinst-ok-of-add-inst-apply-nrec

(defthm moddb-modinst-ok-of-add-inst-apply-nrec
 (implies
  (and
   (bind-free
      (nrec_unfix mod '(:insts :wires)
                  mod 'acl2::|MOD-wrapped?|
                  'acl2::|MOD-unwrapped|
                  'acl2::|MOD-hyps|)
      (acl2::|MOD-wrapped?| acl2::|MOD-unwrapped| acl2::|MOD-hyps|))
   (equal |M-wrapped|
          (if acl2::|MOD-wrapped?| mod
            (nrec '(:insts :wires) mod)))
   (bind-free (nrec_unfix |M-wrapped| '(:insts :wires)
                          mod '|M-wrapped?|
                          'm
                          '|M-wrapped-hyps|)
              (|M-wrapped?| m |M-wrapped-hyps|))
   (nrec_unfix_check |M-wrapped?| |M-wrapped|
                     m |M-wrapped-hyps| '(:insts :wires)
                     mod)
   (syntaxp (or (not (equal mod m)))))
  (equal
       (moddb-modinst-ok instidx modidx
                         (update-nth *moddb->modsi*
                                     (update-nth modidx mod mods)
                                     moddb))
       (acl2::skip-rewrite
            (moddb-modinst-ok instidx modidx
                              (update-nth *moddb->modsi*
                                          (update-nth modidx m mods)
                                          moddb))))))

Theorem: s-of-nrec-when-member

(defthm s-of-nrec-when-member
  (implies (member k keys)
           (equal (s k v (nrec keys x))
                  (nrec keys (s k v x)))))

Theorem: propagate-nrec-over-s

(defthm propagate-nrec-over-s
 (implies
  (and (member k keys)
       (bind-free
            (nrec_unfix x keys x 'acl2::|X-wrapped?|
                        'acl2::|X-unwrapped|
                        'acl2::|X-hyps|)
            (acl2::|X-wrapped?| acl2::|X-unwrapped| acl2::|X-hyps|))
       (equal |XX-wrapped|
              (if acl2::|X-wrapped?| x (nrec keys x)))
       (bind-free (nrec_unfix |XX-wrapped| keys x '|XX-wrapped?|
                              'xx
                              '|XX-wrapped-hyps|)
                  (|XX-wrapped?| xx |XX-wrapped-hyps|))
       (nrec_unfix_check |XX-wrapped?| |XX-wrapped|
                         xx |XX-wrapped-hyps| keys x)
       (syntaxp (or (not (equal x xx)))))
  (equal (nrec keys (s k v x))
         (acl2::skip-rewrite (nrec keys (s k v xx))))))

Theorem: moddb-mod-inst-wireoffset-of-append-insts

(defthm moddb-mod-inst-wireoffset-of-append-insts
 (implies
  (<= (nfix instidx)
      (len (elab-modinsts-rem-dups insts)))
  (equal
   (moddb-mod-inst-wireoffset
    instidx modidx
    (update-nth *moddb->modsi*
                (update-nth modidx (s :insts (append insts new) mod)
                            mods)
                moddb))
   (moddb-mod-inst-wireoffset
        instidx modidx
        (update-nth *moddb->modsi*
                    (update-nth modidx (s :insts insts mod)
                                mods)
                    moddb)))))

Theorem: moddb-mod-inst-instoffset-of-append-insts

(defthm moddb-mod-inst-instoffset-of-append-insts
 (implies
  (<= (nfix instidx)
      (len (elab-modinsts-rem-dups insts)))
  (equal
   (moddb-mod-inst-instoffset
    instidx modidx
    (update-nth *moddb->modsi*
                (update-nth modidx (s :insts (append insts new) mod)
                            mods)
                moddb))
   (moddb-mod-inst-instoffset
        instidx modidx
        (update-nth *moddb->modsi*
                    (update-nth modidx (s :insts insts mod)
                                mods)
                    moddb)))))

Theorem: s-of-elab-modinsts-rem-dups-v-under-elab-mod$a-equiv

(defthm acl2::s-of-elab-modinsts-rem-dups-v-under-elab-mod$a-equiv
  (elab-mod$a-equiv (s :insts (elab-modinsts-rem-dups v) x)
                    (s :insts v x)))

Theorem: s-elab-modinsts-nodups-equiv-congruence-on-v-under-elab-mod$a-equiv

(defthm
 acl2::s-elab-modinsts-nodups-equiv-congruence-on-v-under-elab-mod$a-equiv
 (implies (elab-modinsts-nodups-equiv v acl2::v-equiv)
          (elab-mod$a-equiv (s :insts v x)
                            (s :insts acl2::v-equiv x)))
 :rule-classes :congruence)

Theorem: fix-of-number

(defthm fix-of-number
  (implies (acl2-numberp x)
           (equal (fix x) x))
  :rule-classes ((:rewrite :backchain-limit-lst 0)))

Theorem: moddb-add-modinst-to-last-mods-ok

(defthm moddb-add-modinst-to-last-mods-ok
  (implies (and (moddb-mods-ok moddb)
                (< (nfix modidx)
                   (+ -1 (moddb->nmods moddb))))
           (moddb-mods-ok
                (moddb-add-modinst-to-last instname modidx moddb))))