		Search-engine friendly clone of the ACL2 documentation.

Unparameterization

Vl-genblob-resolve-rejoin-scopeitems

Signature
(vl-genblob-resolve-rejoin-scopeitems scopeitems nonscopeitems generates modinsts) → new-x
Arguments: scopeitems — Guard (vl-genblob-p scopeitems).; nonscopeitems — Guard (vl-genblob-p nonscopeitems).; generates — Guard (vl-genelementlist-p generates).; modinsts — Guard (vl-modinstlist-p modinsts).
Returns: new-x — Type (vl-genblob-p new-x).

Definitions and Theorems

Function: vl-genblob-resolve-rejoin-scopeitems

(defun vl-genblob-resolve-rejoin-scopeitems
       (scopeitems nonscopeitems generates modinsts)
  (declare (xargs :guard (and (vl-genblob-p scopeitems)
                              (vl-genblob-p nonscopeitems)
                              (vl-genelementlist-p generates)
                              (vl-modinstlist-p modinsts))))
  (let ((__function__ 'vl-genblob-resolve-rejoin-scopeitems))
    (declare (ignorable __function__))
    (b* (((vl-genblob scopeitems)))
      (change-vl-genblob nonscopeitems
                         :portdecls scopeitems.portdecls
                         :vardecls scopeitems.vardecls
                         :paramdecls scopeitems.paramdecls
                         :fundecls scopeitems.fundecls
                         :taskdecls scopeitems.taskdecls
                         :gateinsts scopeitems.gateinsts
                         :typedefs scopeitems.typedefs
                         :fwdtypedefs scopeitems.fwdtypedefs
                         :modports scopeitems.modports
                         :genvars scopeitems.genvars
                         :ports scopeitems.ports
                         :generates generates
                         :modinsts modinsts))))

Theorem: vl-genblob-p-of-vl-genblob-resolve-rejoin-scopeitems

(defthm vl-genblob-p-of-vl-genblob-resolve-rejoin-scopeitems
  (b* ((new-x (vl-genblob-resolve-rejoin-scopeitems
                   scopeitems
                   nonscopeitems generates modinsts)))
    (vl-genblob-p new-x))
  :rule-classes :rewrite)

Theorem: vl-genblob-resolve-rejoin-scopeitems-of-vl-genblob-fix-scopeitems

(defthm
  vl-genblob-resolve-rejoin-scopeitems-of-vl-genblob-fix-scopeitems
  (equal (vl-genblob-resolve-rejoin-scopeitems
              (vl-genblob-fix scopeitems)
              nonscopeitems generates modinsts)
         (vl-genblob-resolve-rejoin-scopeitems
              scopeitems
              nonscopeitems generates modinsts)))

Theorem: vl-genblob-resolve-rejoin-scopeitems-vl-genblob-equiv-congruence-on-scopeitems

(defthm
 vl-genblob-resolve-rejoin-scopeitems-vl-genblob-equiv-congruence-on-scopeitems
 (implies (vl-genblob-equiv scopeitems scopeitems-equiv)
          (equal (vl-genblob-resolve-rejoin-scopeitems
                      scopeitems
                      nonscopeitems generates modinsts)
                 (vl-genblob-resolve-rejoin-scopeitems
                      scopeitems-equiv
                      nonscopeitems generates modinsts)))
 :rule-classes :congruence)

Theorem: vl-genblob-resolve-rejoin-scopeitems-of-vl-genblob-fix-nonscopeitems

(defthm
 vl-genblob-resolve-rejoin-scopeitems-of-vl-genblob-fix-nonscopeitems
 (equal (vl-genblob-resolve-rejoin-scopeitems
             scopeitems
             (vl-genblob-fix nonscopeitems)
             generates modinsts)
        (vl-genblob-resolve-rejoin-scopeitems
             scopeitems
             nonscopeitems generates modinsts)))

Theorem: vl-genblob-resolve-rejoin-scopeitems-vl-genblob-equiv-congruence-on-nonscopeitems

(defthm
 vl-genblob-resolve-rejoin-scopeitems-vl-genblob-equiv-congruence-on-nonscopeitems
 (implies (vl-genblob-equiv nonscopeitems nonscopeitems-equiv)
          (equal (vl-genblob-resolve-rejoin-scopeitems
                      scopeitems
                      nonscopeitems generates modinsts)
                 (vl-genblob-resolve-rejoin-scopeitems
                      scopeitems nonscopeitems-equiv
                      generates modinsts)))
 :rule-classes :congruence)

Theorem: vl-genblob-resolve-rejoin-scopeitems-of-vl-genelementlist-fix-generates

(defthm
 vl-genblob-resolve-rejoin-scopeitems-of-vl-genelementlist-fix-generates
 (equal (vl-genblob-resolve-rejoin-scopeitems
             scopeitems nonscopeitems
             (vl-genelementlist-fix generates)
             modinsts)
        (vl-genblob-resolve-rejoin-scopeitems
             scopeitems
             nonscopeitems generates modinsts)))

Theorem: vl-genblob-resolve-rejoin-scopeitems-vl-genelementlist-equiv-congruence-on-generates

(defthm
 vl-genblob-resolve-rejoin-scopeitems-vl-genelementlist-equiv-congruence-on-generates
 (implies
  (vl-genelementlist-equiv generates generates-equiv)
  (equal
   (vl-genblob-resolve-rejoin-scopeitems
        scopeitems
        nonscopeitems generates modinsts)
   (vl-genblob-resolve-rejoin-scopeitems scopeitems nonscopeitems
                                         generates-equiv modinsts)))
 :rule-classes :congruence)

Theorem: vl-genblob-resolve-rejoin-scopeitems-of-vl-modinstlist-fix-modinsts

(defthm
 vl-genblob-resolve-rejoin-scopeitems-of-vl-modinstlist-fix-modinsts
 (equal (vl-genblob-resolve-rejoin-scopeitems
             scopeitems nonscopeitems
             generates (vl-modinstlist-fix modinsts))
        (vl-genblob-resolve-rejoin-scopeitems
             scopeitems
             nonscopeitems generates modinsts)))

Theorem: vl-genblob-resolve-rejoin-scopeitems-vl-modinstlist-equiv-congruence-on-modinsts

(defthm
 vl-genblob-resolve-rejoin-scopeitems-vl-modinstlist-equiv-congruence-on-modinsts
 (implies
  (vl-modinstlist-equiv modinsts modinsts-equiv)
  (equal
   (vl-genblob-resolve-rejoin-scopeitems
        scopeitems
        nonscopeitems generates modinsts)
   (vl-genblob-resolve-rejoin-scopeitems scopeitems nonscopeitems
                                         generates modinsts-equiv)))
 :rule-classes :congruence)