(vl-gateinstlist-ctxexprs-nrev x mod ss nrev) → nrev
Function:
(defun vl-gateinstlist-ctxexprs-nrev (x mod ss nrev) (declare (xargs :stobjs (nrev))) (declare (xargs :guard (and (vl-gateinstlist-p x) (stringp mod) (vl-scopestack-p ss)))) (let ((__function__ 'vl-gateinstlist-ctxexprs-nrev)) (declare (ignorable __function__)) (b* (((when (atom x)) (nrev-fix nrev)) (nrev (nrev-append (vl-gateinst-ctxexprs (car x) mod ss) nrev))) (vl-gateinstlist-ctxexprs-nrev (cdr x) mod ss nrev))))
Theorem:
(defthm vl-gateinstlist-ctxexprs-nrev-of-vl-gateinstlist-fix-x (equal (vl-gateinstlist-ctxexprs-nrev (vl-gateinstlist-fix x) mod ss nrev) (vl-gateinstlist-ctxexprs-nrev x mod ss nrev)))
Theorem:
(defthm vl-gateinstlist-ctxexprs-nrev-vl-gateinstlist-equiv-congruence-on-x (implies (vl-gateinstlist-equiv x x-equiv) (equal (vl-gateinstlist-ctxexprs-nrev x mod ss nrev) (vl-gateinstlist-ctxexprs-nrev x-equiv mod ss nrev))) :rule-classes :congruence)
Theorem:
(defthm vl-gateinstlist-ctxexprs-nrev-of-str-fix-mod (equal (vl-gateinstlist-ctxexprs-nrev x (str-fix mod) ss nrev) (vl-gateinstlist-ctxexprs-nrev x mod ss nrev)))
Theorem:
(defthm vl-gateinstlist-ctxexprs-nrev-streqv-congruence-on-mod (implies (streqv mod mod-equiv) (equal (vl-gateinstlist-ctxexprs-nrev x mod ss nrev) (vl-gateinstlist-ctxexprs-nrev x mod-equiv ss nrev))) :rule-classes :congruence)
Theorem:
(defthm vl-gateinstlist-ctxexprs-nrev-of-vl-scopestack-fix-ss (equal (vl-gateinstlist-ctxexprs-nrev x mod (vl-scopestack-fix ss) nrev) (vl-gateinstlist-ctxexprs-nrev x mod ss nrev)))
Theorem:
(defthm vl-gateinstlist-ctxexprs-nrev-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-gateinstlist-ctxexprs-nrev x mod ss nrev) (vl-gateinstlist-ctxexprs-nrev x mod ss-equiv nrev))) :rule-classes :congruence)