(vl-module-expand-calls-in-nondecls assigns modinsts gateinsts alwayses initials ss nf vacc aacc warnings) → (mv okp warnings nf vacc aacc assigns modinsts gateinsts alwayses initials)
Function:
(defun vl-module-expand-calls-in-nondecls (assigns modinsts gateinsts alwayses initials ss nf vacc aacc warnings) (declare (xargs :guard (and (vl-assignlist-p assigns) (vl-modinstlist-p modinsts) (vl-gateinstlist-p gateinsts) (vl-alwayslist-p alwayses) (vl-initiallist-p initials) (vl-scopestack-p ss) (vl-namefactory-p nf) (vl-vardecllist-p vacc) (vl-assignlist-p aacc) (vl-warninglist-p warnings)))) (let ((__function__ 'vl-module-expand-calls-in-nondecls)) (declare (ignorable __function__)) (b* (((mv okp1 warnings nf assigns vacc aacc) (vl-assignlist-expand-function-calls assigns ss nf vacc aacc warnings 100)) ((mv okp2 warnings nf modinsts vacc aacc) (vl-modinstlist-expand-function-calls modinsts ss nf vacc aacc warnings)) ((mv okp3 warnings nf gateinsts vacc aacc) (vl-gateinstlist-expand-function-calls gateinsts ss nf vacc aacc warnings)) ((mv okp4 warnings nf alwayses vacc aacc) (vl-alwayslist-expand-function-calls alwayses ss nf vacc aacc warnings)) ((mv okp5 warnings nf initials vacc aacc) (vl-initiallist-expand-function-calls initials ss nf vacc aacc warnings))) (mv (and* okp1 okp2 okp3 okp4 okp5) warnings nf vacc aacc assigns modinsts gateinsts alwayses initials))))
Theorem:
(defthm booleanp-of-vl-module-expand-calls-in-nondecls.okp (b* (((mv ?okp ?warnings ?nf ?vacc ?aacc ?assigns ?modinsts ?gateinsts ?alwayses ?initials) (vl-module-expand-calls-in-nondecls assigns modinsts gateinsts alwayses initials ss nf vacc aacc warnings))) (booleanp okp)) :rule-classes :type-prescription)
Theorem:
(defthm vl-warninglist-p-of-vl-module-expand-calls-in-nondecls.warnings (b* (((mv ?okp ?warnings ?nf ?vacc ?aacc ?assigns ?modinsts ?gateinsts ?alwayses ?initials) (vl-module-expand-calls-in-nondecls assigns modinsts gateinsts alwayses initials ss nf vacc aacc warnings))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-namefactory-p-of-vl-module-expand-calls-in-nondecls.nf (b* (((mv ?okp ?warnings ?nf ?vacc ?aacc ?assigns ?modinsts ?gateinsts ?alwayses ?initials) (vl-module-expand-calls-in-nondecls assigns modinsts gateinsts alwayses initials ss nf vacc aacc warnings))) (vl-namefactory-p nf)) :rule-classes :rewrite)
Theorem:
(defthm vl-vardecllist-p-of-vl-module-expand-calls-in-nondecls.vacc (b* (((mv ?okp ?warnings ?nf ?vacc ?aacc ?assigns ?modinsts ?gateinsts ?alwayses ?initials) (vl-module-expand-calls-in-nondecls assigns modinsts gateinsts alwayses initials ss nf vacc aacc warnings))) (vl-vardecllist-p vacc)) :rule-classes :rewrite)
Theorem:
(defthm vl-assignlist-p-of-vl-module-expand-calls-in-nondecls.aacc (b* (((mv ?okp ?warnings ?nf ?vacc ?aacc ?assigns ?modinsts ?gateinsts ?alwayses ?initials) (vl-module-expand-calls-in-nondecls assigns modinsts gateinsts alwayses initials ss nf vacc aacc warnings))) (vl-assignlist-p aacc)) :rule-classes :rewrite)
Theorem:
(defthm vl-assignlist-p-of-vl-module-expand-calls-in-nondecls.assigns (b* (((mv ?okp ?warnings ?nf ?vacc ?aacc ?assigns ?modinsts ?gateinsts ?alwayses ?initials) (vl-module-expand-calls-in-nondecls assigns modinsts gateinsts alwayses initials ss nf vacc aacc warnings))) (vl-assignlist-p assigns)) :rule-classes :rewrite)
Theorem:
(defthm vl-modinstlist-p-of-vl-module-expand-calls-in-nondecls.modinsts (b* (((mv ?okp ?warnings ?nf ?vacc ?aacc ?assigns ?modinsts ?gateinsts ?alwayses ?initials) (vl-module-expand-calls-in-nondecls assigns modinsts gateinsts alwayses initials ss nf vacc aacc warnings))) (vl-modinstlist-p modinsts)) :rule-classes :rewrite)
Theorem:
(defthm vl-gateinstlist-p-of-vl-module-expand-calls-in-nondecls.gateinsts (b* (((mv ?okp ?warnings ?nf ?vacc ?aacc ?assigns ?modinsts ?gateinsts ?alwayses ?initials) (vl-module-expand-calls-in-nondecls assigns modinsts gateinsts alwayses initials ss nf vacc aacc warnings))) (vl-gateinstlist-p gateinsts)) :rule-classes :rewrite)
Theorem:
(defthm vl-alwayslist-p-of-vl-module-expand-calls-in-nondecls.alwayses (b* (((mv ?okp ?warnings ?nf ?vacc ?aacc ?assigns ?modinsts ?gateinsts ?alwayses ?initials) (vl-module-expand-calls-in-nondecls assigns modinsts gateinsts alwayses initials ss nf vacc aacc warnings))) (vl-alwayslist-p alwayses)) :rule-classes :rewrite)
Theorem:
(defthm vl-initiallist-p-of-vl-module-expand-calls-in-nondecls.initials (b* (((mv ?okp ?warnings ?nf ?vacc ?aacc ?assigns ?modinsts ?gateinsts ?alwayses ?initials) (vl-module-expand-calls-in-nondecls assigns modinsts gateinsts alwayses initials ss nf vacc aacc warnings))) (vl-initiallist-p initials)) :rule-classes :rewrite)