(vl-modulelist-latchsynth-aux x careful-p vecp) → (mv new-x addmods)
Function:
(defun vl-modulelist-latchsynth-aux (x careful-p vecp) (declare (xargs :guard (and (vl-modulelist-p x) (booleanp careful-p)))) (let ((__function__ 'vl-modulelist-latchsynth-aux)) (declare (ignorable __function__)) (b* (((when (atom x)) (mv nil nil)) ((mv car addmods1) (vl-module-latchsynth (car x) careful-p vecp)) ((mv cdr addmods2) (vl-modulelist-latchsynth-aux (cdr x) careful-p vecp))) (mv (cons car cdr) (append-without-guard addmods1 addmods2)))))
Theorem:
(defthm vl-modulelist-p-of-vl-modulelist-latchsynth-aux.new-x (implies (and (force (vl-modulelist-p x)) (force (booleanp careful-p))) (b* (((mv ?new-x ?addmods) (vl-modulelist-latchsynth-aux x careful-p vecp))) (vl-modulelist-p new-x))) :rule-classes :rewrite)
Theorem:
(defthm vl-modulelist-p-of-vl-modulelist-latchsynth-aux.addmods (implies (and (force (vl-modulelist-p x)) (force (booleanp careful-p))) (b* (((mv ?new-x ?addmods) (vl-modulelist-latchsynth-aux x careful-p vecp))) (vl-modulelist-p addmods))) :rule-classes :rewrite)