(vl-modulelist-delayredux-aux x &key vecp state-onlyp) → (mv new-x addmods)
Function:
(defun vl-modulelist-delayredux-aux-fn (x vecp state-onlyp) (declare (xargs :guard (vl-modulelist-p x))) (let ((__function__ 'vl-modulelist-delayredux-aux)) (declare (ignorable __function__)) (b* (((when (atom x)) (mv nil nil)) ((mv car car-addmods) (vl-module-delayredux (car x) :vecp vecp :state-onlyp state-onlyp)) ((mv cdr cdr-addmods) (vl-modulelist-delayredux-aux (cdr x) :vecp vecp :state-onlyp state-onlyp))) (mv (cons car cdr) (append-without-guard car-addmods cdr-addmods)))))
Theorem:
(defthm vl-modulelist-p-of-vl-modulelist-delayredux-aux.new-x (implies (and (force (vl-modulelist-p x))) (b* (((mv ?new-x ?addmods) (vl-modulelist-delayredux-aux-fn x vecp state-onlyp))) (vl-modulelist-p new-x))) :rule-classes :rewrite)
Theorem:
(defthm vl-modulelist-p-of-vl-modulelist-delayredux-aux.addmods (implies (and (force (vl-modulelist-p x))) (b* (((mv ?new-x ?addmods) (vl-modulelist-delayredux-aux-fn x vecp state-onlyp))) (vl-modulelist-p addmods))) :rule-classes :rewrite)
Theorem:
(defthm vl-modulelist->names-of-vl-modulelist-delayredux-aux (b* (((mv new-x ?addmods) (vl-modulelist-delayredux-aux x :vecp vecp :state-onlyp state-onlyp))) (equal (vl-modulelist->names new-x) (vl-modulelist->names x))))