Project vl-assign-occform across a list of assignments.
(vl-assignlist-occform x nf mod ialist warnings) → (mv warnings mods insts assigns nf)
Function:
(defun vl-assignlist-occform (x nf mod ialist warnings) (declare (xargs :guard (and (vl-assignlist-p x) (vl-namefactory-p nf) (vl-module-p mod) (vl-warninglist-p warnings) (equal ialist (vl-make-moditem-alist mod))))) (let ((__function__ 'vl-assignlist-occform)) (declare (ignorable __function__)) (b* (((when (atom x)) (mv (ok) nil nil nil (vl-namefactory-fix nf))) ((mv warnings mods1 modinsts1 assigns1 nf) (vl-assign-occform (car x) nf mod ialist warnings)) ((mv warnings mods2 modinsts2 assigns2 nf) (vl-assignlist-occform (cdr x) nf mod ialist warnings)) (mods (append mods1 mods2)) (modinsts (append modinsts1 modinsts2)) (assigns (append assigns1 assigns2))) (mv warnings mods modinsts assigns nf))))
Theorem:
(defthm vl-warninglist-p-of-vl-assignlist-occform.warnings (b* (((mv ?warnings ?mods ?insts ?assigns ?nf) (vl-assignlist-occform x nf mod ialist warnings))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-modulelist-p-of-vl-assignlist-occform.mods (b* (((mv ?warnings ?mods ?insts ?assigns ?nf) (vl-assignlist-occform x nf mod ialist warnings))) (vl-modulelist-p mods)) :rule-classes :rewrite)
Theorem:
(defthm vl-modinstlist-p-of-vl-assignlist-occform.insts (b* (((mv ?warnings ?mods ?insts ?assigns ?nf) (vl-assignlist-occform x nf mod ialist warnings))) (vl-modinstlist-p insts)) :rule-classes :rewrite)
Theorem:
(defthm vl-assignlist-p-of-vl-assignlist-occform.assigns (b* (((mv ?warnings ?mods ?insts ?assigns ?nf) (vl-assignlist-occform x nf mod ialist warnings))) (vl-assignlist-p assigns)) :rule-classes :rewrite)
Theorem:
(defthm vl-namefactory-p-of-vl-assignlist-occform.nf (b* (((mv ?warnings ?mods ?insts ?assigns ?nf) (vl-assignlist-occform x nf mod ialist warnings))) (vl-namefactory-p nf)) :rule-classes :rewrite)
Theorem:
(defthm vl-assignlist-occform-mvtypes-1 (true-listp (mv-nth 1 (vl-assignlist-occform x nf mod ialist warnings))) :rule-classes :type-prescription)
Theorem:
(defthm vl-assignlist-occform-mvtypes-2 (true-listp (mv-nth 2 (vl-assignlist-occform x nf mod ialist warnings))) :rule-classes :type-prescription)
Theorem:
(defthm vl-assignlist-occform-mvtypes-3 (true-listp (mv-nth 3 (vl-assignlist-occform x nf mod ialist warnings))) :rule-classes :type-prescription)
Theorem:
(defthm vl-assignlist-occform-of-vl-assignlist-fix-x (equal (vl-assignlist-occform (vl-assignlist-fix x) nf mod ialist warnings) (vl-assignlist-occform x nf mod ialist warnings)))
Theorem:
(defthm vl-assignlist-occform-vl-assignlist-equiv-congruence-on-x (implies (vl-assignlist-equiv x x-equiv) (equal (vl-assignlist-occform x nf mod ialist warnings) (vl-assignlist-occform x-equiv nf mod ialist warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-assignlist-occform-of-vl-namefactory-fix-nf (equal (vl-assignlist-occform x (vl-namefactory-fix nf) mod ialist warnings) (vl-assignlist-occform x nf mod ialist warnings)))
Theorem:
(defthm vl-assignlist-occform-vl-namefactory-equiv-congruence-on-nf (implies (vl-namefactory-equiv nf nf-equiv) (equal (vl-assignlist-occform x nf mod ialist warnings) (vl-assignlist-occform x nf-equiv mod ialist warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-assignlist-occform-of-vl-module-fix-mod (equal (vl-assignlist-occform x nf (vl-module-fix mod) ialist warnings) (vl-assignlist-occform x nf mod ialist warnings)))
Theorem:
(defthm vl-assignlist-occform-vl-module-equiv-congruence-on-mod (implies (vl-module-equiv mod mod-equiv) (equal (vl-assignlist-occform x nf mod ialist warnings) (vl-assignlist-occform x nf mod-equiv ialist warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-assignlist-occform-of-vl-warninglist-fix-warnings (equal (vl-assignlist-occform x nf mod ialist (vl-warninglist-fix warnings)) (vl-assignlist-occform x nf mod ialist warnings)))
Theorem:
(defthm vl-assignlist-occform-vl-warninglist-equiv-congruence-on-warnings (implies (vl-warninglist-equiv warnings warnings-equiv) (equal (vl-assignlist-occform x nf mod ialist warnings) (vl-assignlist-occform x nf mod ialist warnings-equiv))) :rule-classes :congruence)