(envmap-entry-extract-env x env) → res
Function:
(defun envmap-entry-extract-env (x env) (declare (xargs :guard (and (svex-alist-p x) (svdecomp-symenv-p env)))) (let ((__function__ 'envmap-entry-extract-env)) (declare (ignorable __function__)) (b* ((keys (mergesort (cwtime (svexlist-collect-vars (svex-alist-vals x)))))) (with-fast-alist env (svdecomp-env-extract keys env)))))
Theorem:
(defthm svdecomp-symenv-p-of-envmap-entry-extract-env (implies (svdecomp-symenv-p env) (b* ((res (envmap-entry-extract-env x env))) (svdecomp-symenv-p res))) :rule-classes :rewrite)
Theorem:
(defthm svex-alist-eval-under-envmap-entry-extract-env (equal (svex-alist-eval x (svdecomp-ev-symenv (envmap-entry-extract-env x env) a)) (svex-alist-eval x (svdecomp-ev-symenv env a))))
Theorem:
(defthm lookup-vars-subset-of-alist-vars (subsetp (svex-vars (cdr (svar-lookup k x))) (svex-alist-vars x)))
Theorem:
(defthm eval-lookup-in-svdecomp-ev-symenv (equal (svex-eval (cdr (svar-lookup k x)) (svdecomp-ev-symenv (envmap-entry-extract-env x env) a)) (svex-eval (cdr (svar-lookup k x)) (svdecomp-ev-symenv env a))))
Theorem:
(defthm keys-of-envmap-entry-extract-env (set-equiv (svar-alist-keys (envmap-entry-extract-env x env)) (svex-alist-vars x)))
Theorem:
(defthm ev-lookup-of-envmap-entry-extract-env (implies (member (svar-fix k) (svex-alist-vars x)) (4vec-equiv (svdecomp-ev (cdr (svar-lookup k (envmap-entry-extract-env x env))) a) (svex-env-lookup k (svdecomp-ev-symenv env a)))))
Theorem:
(defthm envmap-entry-extract-env-of-svex-alist-fix-x (equal (envmap-entry-extract-env (svex-alist-fix x) env) (envmap-entry-extract-env x env)))
Theorem:
(defthm envmap-entry-extract-env-svex-alist-equiv-congruence-on-x (implies (svex-alist-equiv x x-equiv) (equal (envmap-entry-extract-env x env) (envmap-entry-extract-env x-equiv env))) :rule-classes :congruence)
Theorem:
(defthm envmap-entry-extract-env-of-svar-alist-fix-env (equal (envmap-entry-extract-env x (svar-alist-fix env)) (envmap-entry-extract-env x env)))
Theorem:
(defthm envmap-entry-extract-env-svar-alist-equiv-congruence-on-env (implies (svar-alist-equiv env env-equiv) (equal (envmap-entry-extract-env x env) (envmap-entry-extract-env x env-equiv))) :rule-classes :congruence)