(svex-alist-evaluation-to-symenv x env) → al
Function:
(defun svex-alist-evaluation-to-symenv (x env) (declare (xargs :guard (and (svex-alist-p x) (pseudo-termp env)))) (let ((__function__ 'svex-alist-evaluation-to-symenv)) (declare (ignorable __function__)) (b* (((when (atom x)) nil) ((unless (mbt (and (consp (car x)) (svar-p (caar x))))) (svex-alist-evaluation-to-symenv (cdr x) env)) ((cons var svex) (car x))) (cons (cons var (cons 'svex-eval (cons (cons 'quote (cons (svex-fix svex) 'nil)) (cons env 'nil)))) (svex-alist-evaluation-to-symenv (cdr x) env)))))
Theorem:
(defthm return-type-of-svex-alist-evaluation-to-symenv (b* ((al (svex-alist-evaluation-to-symenv x env))) (and (svar-alist-p al) (implies (pseudo-termp env) (svdecomp-symenv-p al)))) :rule-classes :rewrite)
Theorem:
(defthm eval-lookup-of-svex-alist-evaluation-to-symenv (b* ((al (svex-alist-evaluation-to-symenv x env))) (equal (svdecomp-ev (cdr (svar-lookup k al)) a) (and (svar-lookup k x) (svex-eval (cdr (svar-lookup k x)) (svdecomp-ev env a))))))
Theorem:
(defthm lookup-exists-of-svex-alist-evaluation-to-symenv (b* ((al (svex-alist-evaluation-to-symenv x env))) (iff (svar-lookup k al) (svar-lookup k x))))
Theorem:
(defthm svdecomp-ev-symenv-of-svex-alist-evaluation-to-symenv (b* ((al (svex-alist-evaluation-to-symenv x env))) (equal (svdecomp-ev-symenv al a) (svex-alist-eval x (svdecomp-ev env a)))))
Theorem:
(defthm svex-alist-evaluation-to-symenv-of-svex-alist-fix-x (equal (svex-alist-evaluation-to-symenv (svex-alist-fix x) env) (svex-alist-evaluation-to-symenv x env)))
Theorem:
(defthm svex-alist-evaluation-to-symenv-svex-alist-equiv-congruence-on-x (implies (svex-alist-equiv x x-equiv) (equal (svex-alist-evaluation-to-symenv x env) (svex-alist-evaluation-to-symenv x-equiv env))) :rule-classes :congruence)