(lhprobe/4vec-overridemux-eval x envs outs) → val
Function:
(defun lhprobe/4vec-overridemux-eval (x envs outs) (declare (xargs :guard (and (lhprobe/4vec-p x) (svex-envlist-p envs) (svex-envlist-p outs)))) (let ((__function__ 'lhprobe/4vec-overridemux-eval)) (declare (ignorable __function__)) (lhprobe/4vec-case x :lhprobe (lhprobe-overridemux-eval x envs outs) :4vec (4vec-fix x))))
Theorem:
(defthm 4vec-p-of-lhprobe/4vec-overridemux-eval (b* ((val (lhprobe/4vec-overridemux-eval x envs outs))) (4vec-p val)) :rule-classes :rewrite)
Theorem:
(defthm lhprobe/4vec-overridemux-eval-of-lhprobe/4vec-fix-x (equal (lhprobe/4vec-overridemux-eval (lhprobe/4vec-fix x) envs outs) (lhprobe/4vec-overridemux-eval x envs outs)))
Theorem:
(defthm lhprobe/4vec-overridemux-eval-lhprobe/4vec-equiv-congruence-on-x (implies (lhprobe/4vec-equiv x x-equiv) (equal (lhprobe/4vec-overridemux-eval x envs outs) (lhprobe/4vec-overridemux-eval x-equiv envs outs))) :rule-classes :congruence)
Theorem:
(defthm lhprobe/4vec-overridemux-eval-of-svex-envlist-fix-envs (equal (lhprobe/4vec-overridemux-eval x (svex-envlist-fix envs) outs) (lhprobe/4vec-overridemux-eval x envs outs)))
Theorem:
(defthm lhprobe/4vec-overridemux-eval-svex-envlist-equiv-congruence-on-envs (implies (svex-envlist-equiv envs envs-equiv) (equal (lhprobe/4vec-overridemux-eval x envs outs) (lhprobe/4vec-overridemux-eval x envs-equiv outs))) :rule-classes :congruence)
Theorem:
(defthm lhprobe/4vec-overridemux-eval-of-svex-envlist-fix-outs (equal (lhprobe/4vec-overridemux-eval x envs (svex-envlist-fix outs)) (lhprobe/4vec-overridemux-eval x envs outs)))
Theorem:
(defthm lhprobe/4vec-overridemux-eval-svex-envlist-equiv-congruence-on-outs (implies (svex-envlist-equiv outs outs-equiv) (equal (lhprobe/4vec-overridemux-eval x envs outs) (lhprobe/4vec-overridemux-eval x envs outs-equiv))) :rule-classes :congruence)