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