(vl-elabtask-increwrite x) → new-x
Function:
(defun vl-elabtask-increwrite (x) (declare (xargs :guard (vl-elabtask-p x))) (let ((__function__ 'vl-elabtask-increwrite)) (declare (ignorable __function__)) (b* (((vl-elabtask x) (vl-elabtask-fix x))) (b* ((stmt (vl-stmt-increwrite-flat x.stmt))) (change-vl-elabtask x :stmt stmt)))))
Theorem:
(defthm vl-elabtask-p-of-vl-elabtask-increwrite (b* ((new-x (vl-elabtask-increwrite x))) (vl-elabtask-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm vl-elabtask-increwrite-of-vl-elabtask-fix-x (equal (vl-elabtask-increwrite (vl-elabtask-fix x)) (vl-elabtask-increwrite x)))
Theorem:
(defthm vl-elabtask-increwrite-vl-elabtask-equiv-congruence-on-x (implies (vl-elabtask-equiv x x-equiv) (equal (vl-elabtask-increwrite x) (vl-elabtask-increwrite x-equiv))) :rule-classes :congruence)