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