(vl-design-increwrite x) → new-x
Function:
(defun vl-design-increwrite (x) (declare (xargs :guard (vl-design-p x))) (let ((__function__ 'vl-design-increwrite)) (declare (ignorable __function__)) (b* (((vl-design x) (vl-design-fix x))) (b* ((mods (vl-modulelist-increwrite x.mods)) (interfaces (vl-interfacelist-increwrite x.interfaces)) (classes (vl-classlist-increwrite x.classes)) (packages (vl-packagelist-increwrite x.packages)) (taskdecls (vl-taskdecllist-increwrite x.taskdecls)) (fundecls (vl-fundecllist-increwrite x.fundecls))) (change-vl-design x :mods mods :interfaces interfaces :classes classes :packages packages :taskdecls taskdecls :fundecls fundecls)))))
Theorem:
(defthm vl-design-p-of-vl-design-increwrite (b* ((new-x (vl-design-increwrite x))) (vl-design-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm vl-design-increwrite-of-vl-design-fix-x (equal (vl-design-increwrite (vl-design-fix x)) (vl-design-increwrite x)))
Theorem:
(defthm vl-design-increwrite-vl-design-equiv-congruence-on-x (implies (vl-design-equiv x x-equiv) (equal (vl-design-increwrite x) (vl-design-increwrite x-equiv))) :rule-classes :congruence)