(lhatom-overridemux-eval x env out) → val
Function:
(defun lhatom-overridemux-eval (x env out) (declare (xargs :guard (and (lhatom-p x) (svex-env-p env) (svex-env-p out)))) (let ((__function__ 'lhatom-overridemux-eval)) (declare (ignorable __function__)) (lhatom-case x :z 0 :var (4vec-rsh (2vec x.rsh) (if (svar-override-p x.name :val) (4vec-bit?! (svex-env-fastlookup (svar-change-override x.name :test) env) (svex-env-fastlookup x.name env) (svex-env-fastlookup (svar-change-override x.name nil) out)) (svex-env-fastlookup x.name env))))))
Theorem:
(defthm 4vec-p-of-lhatom-overridemux-eval (b* ((val (lhatom-overridemux-eval x env out))) (4vec-p val)) :rule-classes :rewrite)
Theorem:
(defthm lhatom-overridemux-eval-of-lhatom-fix-x (equal (lhatom-overridemux-eval (lhatom-fix x) env out) (lhatom-overridemux-eval x env out)))
Theorem:
(defthm lhatom-overridemux-eval-lhatom-equiv-congruence-on-x (implies (lhatom-equiv x x-equiv) (equal (lhatom-overridemux-eval x env out) (lhatom-overridemux-eval x-equiv env out))) :rule-classes :congruence)
Theorem:
(defthm lhatom-overridemux-eval-of-svex-env-fix-env (equal (lhatom-overridemux-eval x (svex-env-fix env) out) (lhatom-overridemux-eval x env out)))
Theorem:
(defthm lhatom-overridemux-eval-svex-env-equiv-congruence-on-env (implies (svex-env-equiv env env-equiv) (equal (lhatom-overridemux-eval x env out) (lhatom-overridemux-eval x env-equiv out))) :rule-classes :congruence)
Theorem:
(defthm lhatom-overridemux-eval-of-svex-env-fix-out (equal (lhatom-overridemux-eval x env (svex-env-fix out)) (lhatom-overridemux-eval x env out)))
Theorem:
(defthm lhatom-overridemux-eval-svex-env-equiv-congruence-on-out (implies (svex-env-equiv out out-equiv) (equal (lhatom-overridemux-eval x env out) (lhatom-overridemux-eval x env out-equiv))) :rule-classes :congruence)