(vl-gateinst-ctxexprs-nrev mod x nrev) → nrev
Function:
(defun vl-gateinst-ctxexprs-nrev$inline (mod x nrev) (declare (xargs :stobjs (nrev))) (declare (xargs :guard (and (stringp mod) (vl-gateinst-p x)))) (let ((__function__ 'vl-gateinst-ctxexprs-nrev)) (declare (ignorable __function__)) (let ((x (vl-gateinst-fix x))) (vl-make-exprctxalist-nrev (vl-gateinst-allexprs x) (make-vl-context1 :mod mod :elem x) nrev))))
Theorem:
(defthm vl-gateinst-ctxexprs-nrev$inline-of-str-fix-mod (equal (vl-gateinst-ctxexprs-nrev$inline (str-fix mod) x nrev) (vl-gateinst-ctxexprs-nrev$inline mod x nrev)))
Theorem:
(defthm vl-gateinst-ctxexprs-nrev$inline-streqv-congruence-on-mod (implies (streqv mod mod-equiv) (equal (vl-gateinst-ctxexprs-nrev$inline mod x nrev) (vl-gateinst-ctxexprs-nrev$inline mod-equiv x nrev))) :rule-classes :congruence)
Theorem:
(defthm vl-gateinst-ctxexprs-nrev$inline-of-vl-gateinst-fix-x (equal (vl-gateinst-ctxexprs-nrev$inline mod (vl-gateinst-fix x) nrev) (vl-gateinst-ctxexprs-nrev$inline mod x nrev)))
Theorem:
(defthm vl-gateinst-ctxexprs-nrev$inline-vl-gateinst-equiv-congruence-on-x (implies (vl-gateinst-equiv x x-equiv) (equal (vl-gateinst-ctxexprs-nrev$inline mod x nrev) (vl-gateinst-ctxexprs-nrev$inline mod x-equiv nrev))) :rule-classes :congruence)