Add
(vl-gateinst-origexprs x) → new-x
Function:
(defun vl-gateinst-origexprs (x) (declare (xargs :guard (vl-gateinst-p x))) (let ((__function__ 'vl-gateinst-origexprs)) (declare (ignorable __function__)) (let ((x (vl-gateinst-fix x))) (b* (((vl-gateinst x))) (change-vl-gateinst x :args (vl-plainarglist-origexprs x.args) :range (vl-maybe-range-origexprs x.range) :delay (vl-maybe-gatedelay-origexprs x.delay))))))
Theorem:
(defthm vl-gateinst-p-of-vl-gateinst-origexprs (b* ((new-x (vl-gateinst-origexprs x))) (vl-gateinst-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm vl-gateinst-origexprs-of-vl-gateinst-fix-x (equal (vl-gateinst-origexprs (vl-gateinst-fix x)) (vl-gateinst-origexprs x)))
Theorem:
(defthm vl-gateinst-origexprs-vl-gateinst-equiv-congruence-on-x (implies (vl-gateinst-equiv x x-equiv) (equal (vl-gateinst-origexprs x) (vl-gateinst-origexprs x-equiv))) :rule-classes :congruence)