		Search-engine friendly clone of the ACL2 documentation.

Unparameterization

Vl-genblob-rejoin-scopeitems

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

Definitions and Theorems

Function: vl-genblob-rejoin-scopeitems

(defun vl-genblob-rejoin-scopeitems (scopeitems nonscopeitems)
  (declare (xargs :guard (and (vl-genblob-p scopeitems)
                              (vl-genblob-p nonscopeitems))))
  (let ((__function__ 'vl-genblob-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 scopeitems.generates
                         :modinsts scopeitems.modinsts))))

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

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

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

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

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

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

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

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

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

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