(svar/4vec-alistlist-eval x env) → val
Function:
(defun svar/4vec-alistlist-eval (x env) (declare (xargs :guard (and (svar/4vec-alistlist-p x) (svex-env-p env)))) (let ((__function__ 'svar/4vec-alistlist-eval)) (declare (ignorable __function__)) (if (atom x) nil (cons (svar/4vec-alist-eval (car x) env) (svar/4vec-alistlist-eval (cdr x) env)))))
Theorem:
(defthm svex-envlist-p-of-svar/4vec-alistlist-eval (b* ((val (svar/4vec-alistlist-eval x env))) (svex-envlist-p val)) :rule-classes :rewrite)
Theorem:
(defthm svar/4vec-alistlist-eval-in-terms-of-svex-alistlist-eval (implies (svex-alistlist-noncall-p x) (equal (svar/4vec-alistlist-eval x env) (svex-alistlist-eval x env))))
Theorem:
(defthm svar/4vec-alistlist-eval-of-svar/4vec-alistlist-fix-x (equal (svar/4vec-alistlist-eval (svar/4vec-alistlist-fix x) env) (svar/4vec-alistlist-eval x env)))
Theorem:
(defthm svar/4vec-alistlist-eval-svar/4vec-alistlist-equiv-congruence-on-x (implies (svar/4vec-alistlist-equiv x x-equiv) (equal (svar/4vec-alistlist-eval x env) (svar/4vec-alistlist-eval x-equiv env))) :rule-classes :congruence)
Theorem:
(defthm svar/4vec-alistlist-eval-of-svex-env-fix-env (equal (svar/4vec-alistlist-eval x (svex-env-fix env)) (svar/4vec-alistlist-eval x env)))
Theorem:
(defthm svar/4vec-alistlist-eval-svex-env-equiv-congruence-on-env (implies (svex-env-equiv env env-equiv) (equal (svar/4vec-alistlist-eval x env) (svar/4vec-alistlist-eval x env-equiv))) :rule-classes :congruence)