(vl-design-prohibit-incexprs x) → new-x
Function:
(defun vl-design-prohibit-incexprs (x) (declare (xargs :guard (vl-design-p x))) (let ((__function__ 'vl-design-prohibit-incexprs)) (declare (ignorable __function__)) (b* ((warnings (vl-design-prohibit-incexprs-aux x nil)) (new-x1 (vl-design-prohibit-incexprs-top-aux x))) (change-vl-design new-x1 :warnings (append-without-guard warnings (vl-design->warnings new-x1))))))
Theorem:
(defthm vl-design-p-of-vl-design-prohibit-incexprs (b* ((new-x (vl-design-prohibit-incexprs x))) (vl-design-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm vl-design-prohibit-incexprs-of-vl-design-fix-x (equal (vl-design-prohibit-incexprs (vl-design-fix x)) (vl-design-prohibit-incexprs x)))
Theorem:
(defthm vl-design-prohibit-incexprs-vl-design-equiv-congruence-on-x (implies (vl-design-equiv x x-equiv) (equal (vl-design-prohibit-incexprs x) (vl-design-prohibit-incexprs x-equiv))) :rule-classes :congruence)