(vl-unparam-instlist x ss warnings modname sigalist) → (mv successp warnings insts sigalist)
Function:
(defun vl-unparam-instlist (x ss warnings modname sigalist) (declare (xargs :guard (and (vl-modinstlist-p x) (vl-scopestack-p ss) (vl-warninglist-p warnings) (stringp modname) (vl-unparam-sigalist-p sigalist)))) (let ((__function__ 'vl-unparam-instlist)) (declare (ignorable __function__)) (b* (((when (atom x)) (mv t (ok) nil (vl-unparam-sigalist-fix sigalist))) ((mv ok1 warnings inst1 sig new-ss) (vl-unparam-inst (car x) ss warnings modname)) (sigalist (if sig (cons (cons sig new-ss) sigalist) sigalist)) ((mv ok2 warnings insts2 sigalist) (vl-unparam-instlist (cdr x) ss warnings modname sigalist))) (mv (and ok1 ok2) warnings (cons inst1 insts2) sigalist))))
Theorem:
(defthm booleanp-of-vl-unparam-instlist.successp (b* (((mv ?successp ?warnings ?insts ?sigalist) (vl-unparam-instlist x ss warnings modname sigalist))) (booleanp successp)) :rule-classes :type-prescription)
Theorem:
(defthm vl-warninglist-p-of-vl-unparam-instlist.warnings (b* (((mv ?successp ?warnings ?insts ?sigalist) (vl-unparam-instlist x ss warnings modname sigalist))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-modinstlist-p-of-vl-unparam-instlist.insts (b* (((mv ?successp ?warnings ?insts ?sigalist) (vl-unparam-instlist x ss warnings modname sigalist))) (vl-modinstlist-p insts)) :rule-classes :rewrite)
Theorem:
(defthm vl-unparam-sigalist-p-of-vl-unparam-instlist.sigalist (b* (((mv ?successp ?warnings ?insts ?sigalist) (vl-unparam-instlist x ss warnings modname sigalist))) (vl-unparam-sigalist-p sigalist)) :rule-classes :rewrite)
Theorem:
(defthm vl-unparam-instlist-of-vl-modinstlist-fix-x (equal (vl-unparam-instlist (vl-modinstlist-fix x) ss warnings modname sigalist) (vl-unparam-instlist x ss warnings modname sigalist)))
Theorem:
(defthm vl-unparam-instlist-vl-modinstlist-equiv-congruence-on-x (implies (vl-modinstlist-equiv x x-equiv) (equal (vl-unparam-instlist x ss warnings modname sigalist) (vl-unparam-instlist x-equiv ss warnings modname sigalist))) :rule-classes :congruence)
Theorem:
(defthm vl-unparam-instlist-of-vl-scopestack-fix-ss (equal (vl-unparam-instlist x (vl-scopestack-fix ss) warnings modname sigalist) (vl-unparam-instlist x ss warnings modname sigalist)))
Theorem:
(defthm vl-unparam-instlist-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-unparam-instlist x ss warnings modname sigalist) (vl-unparam-instlist x ss-equiv warnings modname sigalist))) :rule-classes :congruence)
Theorem:
(defthm vl-unparam-instlist-of-vl-warninglist-fix-warnings (equal (vl-unparam-instlist x ss (vl-warninglist-fix warnings) modname sigalist) (vl-unparam-instlist x ss warnings modname sigalist)))
Theorem:
(defthm vl-unparam-instlist-vl-warninglist-equiv-congruence-on-warnings (implies (vl-warninglist-equiv warnings warnings-equiv) (equal (vl-unparam-instlist x ss warnings modname sigalist) (vl-unparam-instlist x ss warnings-equiv modname sigalist))) :rule-classes :congruence)
Theorem:
(defthm vl-unparam-instlist-of-str-fix-modname (equal (vl-unparam-instlist x ss warnings (str-fix modname) sigalist) (vl-unparam-instlist x ss warnings modname sigalist)))
Theorem:
(defthm vl-unparam-instlist-streqv-congruence-on-modname (implies (streqv modname modname-equiv) (equal (vl-unparam-instlist x ss warnings modname sigalist) (vl-unparam-instlist x ss warnings modname-equiv sigalist))) :rule-classes :congruence)
Theorem:
(defthm vl-unparam-instlist-of-vl-unparam-sigalist-fix-sigalist (equal (vl-unparam-instlist x ss warnings modname (vl-unparam-sigalist-fix sigalist)) (vl-unparam-instlist x ss warnings modname sigalist)))
Theorem:
(defthm vl-unparam-instlist-vl-unparam-sigalist-equiv-congruence-on-sigalist (implies (vl-unparam-sigalist-equiv sigalist sigalist-equiv) (equal (vl-unparam-instlist x ss warnings modname sigalist) (vl-unparam-instlist x ss warnings modname sigalist-equiv))) :rule-classes :congruence)