(vl-alwayslist-stmttemps x delta) → (mv new-x delta)
Function:
(defun vl-alwayslist-stmttemps (x delta) (declare (xargs :guard (and (vl-alwayslist-p x) (vl-delta-p delta)))) (let ((__function__ 'vl-alwayslist-stmttemps)) (declare (ignorable __function__)) (b* (((when (atom x)) (mv x delta)) ((mv car delta) (vl-always-stmttemps (car x) delta)) ((mv cdr delta) (vl-alwayslist-stmttemps (cdr x) delta))) (mv (cons car cdr) delta))))
Theorem:
(defthm vl-alwayslist-p-of-vl-alwayslist-stmttemps.new-x (implies (and (force (vl-alwayslist-p x)) (force (vl-delta-p delta))) (b* (((mv ?new-x ?delta) (vl-alwayslist-stmttemps x delta))) (vl-alwayslist-p new-x))) :rule-classes :rewrite)
Theorem:
(defthm vl-delta-p-of-vl-alwayslist-stmttemps.delta (implies (and (force (vl-alwayslist-p x)) (force (vl-delta-p delta))) (b* (((mv ?new-x ?delta) (vl-alwayslist-stmttemps x delta))) (vl-delta-p delta))) :rule-classes :rewrite)