Top-level increment-elim transform.
(vl-design-increment-elim x) → new-x
Function:
(defun vl-design-increment-elim (x) (declare (xargs :guard (vl-design-p x))) (let ((__function__ 'vl-design-increment-elim)) (declare (ignorable __function__)) (b* ((x (xf-cwtime (vl-design-increwrite x))) (x (xf-cwtime (vl-design-prohibit-incexprs x)))) x)))
Theorem:
(defthm vl-design-p-of-vl-design-increment-elim (b* ((new-x (vl-design-increment-elim x))) (vl-design-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm vl-design-increment-elim-of-vl-design-fix-x (equal (vl-design-increment-elim (vl-design-fix x)) (vl-design-increment-elim x)))
Theorem:
(defthm vl-design-increment-elim-vl-design-equiv-congruence-on-x (implies (vl-design-equiv x x-equiv) (equal (vl-design-increment-elim x) (vl-design-increment-elim x-equiv))) :rule-classes :congruence)