(vl-paramdecllist-enumname-declarations x seen) → (mv new-x warnings paramdecls seen-out)
Function:
(defun vl-paramdecllist-enumname-declarations (x seen) (declare (xargs :guard (and (vl-paramdecllist-p x) (vl-datatype-map-p seen)))) (let ((__function__ 'vl-paramdecllist-enumname-declarations)) (declare (ignorable __function__)) (b* (((when (atom x)) (mv nil nil nil (vl-datatype-map-fix seen))) ((mv new-x1 warnings1 decls1 seen) (vl-paramdecl-enumname-declarations (car x) seen)) ((mv new-x2 warnings2 decls2 seen) (vl-paramdecllist-enumname-declarations (cdr x) seen))) (mv (cons new-x1 new-x2) (append-without-guard warnings1 warnings2) (append-without-guard decls1 decls2) seen))))
Theorem:
(defthm vl-paramdecllist-p-of-vl-paramdecllist-enumname-declarations.new-x (b* (((mv ?new-x ?warnings ?paramdecls ?seen-out) (vl-paramdecllist-enumname-declarations x seen))) (vl-paramdecllist-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm vl-warninglist-p-of-vl-paramdecllist-enumname-declarations.warnings (b* (((mv ?new-x ?warnings ?paramdecls ?seen-out) (vl-paramdecllist-enumname-declarations x seen))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-paramdecllist-p-of-vl-paramdecllist-enumname-declarations.paramdecls (b* (((mv ?new-x ?warnings ?paramdecls ?seen-out) (vl-paramdecllist-enumname-declarations x seen))) (vl-paramdecllist-p paramdecls)) :rule-classes :rewrite)
Theorem:
(defthm vl-datatype-map-p-of-vl-paramdecllist-enumname-declarations.seen-out (b* (((mv ?new-x ?warnings ?paramdecls ?seen-out) (vl-paramdecllist-enumname-declarations x seen))) (vl-datatype-map-p seen-out)) :rule-classes :rewrite)
Theorem:
(defthm vl-paramdecllist-enumname-declarations-of-vl-paramdecllist-fix-x (equal (vl-paramdecllist-enumname-declarations (vl-paramdecllist-fix x) seen) (vl-paramdecllist-enumname-declarations x seen)))
Theorem:
(defthm vl-paramdecllist-enumname-declarations-vl-paramdecllist-equiv-congruence-on-x (implies (vl-paramdecllist-equiv x x-equiv) (equal (vl-paramdecllist-enumname-declarations x seen) (vl-paramdecllist-enumname-declarations x-equiv seen))) :rule-classes :congruence)
Theorem:
(defthm vl-paramdecllist-enumname-declarations-of-vl-datatype-map-fix-seen (equal (vl-paramdecllist-enumname-declarations x (vl-datatype-map-fix seen)) (vl-paramdecllist-enumname-declarations x seen)))
Theorem:
(defthm vl-paramdecllist-enumname-declarations-vl-datatype-map-equiv-congruence-on-seen (implies (vl-datatype-map-equiv seen seen-equiv) (equal (vl-paramdecllist-enumname-declarations x seen) (vl-paramdecllist-enumname-declarations x seen-equiv))) :rule-classes :congruence)