• 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

Elab-modinst-remove-names

Signature

(elab-modinst-remove-names names x) → xx

Arguments

names — Guard (namelist-p names).

x — Guard (elab-modinst-list-p x).

Returns

xx — Type (elab-modinst-list-p xx).

Definitions and Theorems

Function: elab-modinst-remove-names

(defun elab-modinst-remove-names (names x)
 (declare (xargs :guard (and (namelist-p names)
                             (elab-modinst-list-p x))))
 (let ((__function__ 'elab-modinst-remove-names))
  (declare (ignorable __function__))
  (if (atom names)
      (elab-modinst-list-fix x)
    (elab-modinst-remove-name (car names)
                              (elab-modinst-remove-names (cdr names)
                                                         x)))))

Theorem: elab-modinst-list-p-of-elab-modinst-remove-names

(defthm elab-modinst-list-p-of-elab-modinst-remove-names
  (b* ((xx (elab-modinst-remove-names names x)))
    (elab-modinst-list-p xx))
  :rule-classes :rewrite)

Theorem: elab-modinst-remove-names-of-nil

(defthm elab-modinst-remove-names-of-nil
  (equal (elab-modinst-remove-names nil x)
         (elab-modinst-list-fix x)))

Theorem: elab-modinst-remove-names-of-nil-second

(defthm elab-modinst-remove-names-of-nil-second
  (equal (elab-modinst-remove-names x nil)
         nil))

Theorem: elab-modinst-remove-names-of-cons-second

(defthm elab-modinst-remove-names-of-cons-second
  (equal (elab-modinst-remove-names x (cons y z))
         (if (member (name-fix (nth *elab-modinst$c->instname* y))
                     (namelist-fix x))
             (elab-modinst-remove-names x z)
           (cons (elab-modinst-fix y)
                 (elab-modinst-remove-names x z)))))

Theorem: elab-modinst-remove-names-of-namelist-fix-names

(defthm elab-modinst-remove-names-of-namelist-fix-names
  (equal (elab-modinst-remove-names (namelist-fix names)
                                    x)
         (elab-modinst-remove-names names x)))

Theorem: elab-modinst-remove-names-namelist-equiv-congruence-on-names

(defthm elab-modinst-remove-names-namelist-equiv-congruence-on-names
  (implies (namelist-equiv names names-equiv)
           (equal (elab-modinst-remove-names names x)
                  (elab-modinst-remove-names names-equiv x)))
  :rule-classes :congruence)

Theorem: elab-modinst-remove-names-of-elab-modinst-list-fix-x

(defthm elab-modinst-remove-names-of-elab-modinst-list-fix-x
  (equal (elab-modinst-remove-names names (elab-modinst-list-fix x))
         (elab-modinst-remove-names names x)))

Theorem: elab-modinst-remove-names-elab-modinst-list-equiv-congruence-on-x

(defthm
  elab-modinst-remove-names-elab-modinst-list-equiv-congruence-on-x
  (implies (elab-modinst-list-equiv x x-equiv)
           (equal (elab-modinst-remove-names names x)
                  (elab-modinst-remove-names names x-equiv)))
  :rule-classes :congruence)