(svex-decomp-process-env-term x vars) → (mv err sval symenv)
Function:
(defun svex-decomp-process-env-term (x vars) (declare (xargs :guard (and (svdecomp-symenv-p x) (svarlist-p vars)))) (let ((__function__ 'svex-decomp-process-env-term)) (declare (ignorable __function__)) (b* ((xsymenv (with-fast-alist x (svdecomp-env-extract vars x))) ((mv err base-env envmap) (alist-collect-compositions xsymenv)) ((when err) (mv err nil nil)) ((mv err envunion) (envmap-extract-union-env envmap)) ((when err) (mv err nil nil)) ((mv err fullenv) (svdecomp-symenv-compat-union base-env envunion)) ((when err) (mv err nil nil))) (mv nil (envmap->svex-alist envmap) fullenv))))
Theorem:
(defthm svex-alist-p-of-svex-decomp-process-env-term.sval (b* (((mv ?err ?sval ?symenv) (svex-decomp-process-env-term x vars))) (svex-alist-p sval)) :rule-classes :rewrite)
Theorem:
(defthm svdecomp-symenv-p-of-svex-decomp-process-env-term.symenv (implies (and (svdecomp-symenv-p x) (svarlist-p vars)) (b* (((mv ?err ?sval ?symenv) (svex-decomp-process-env-term x vars))) (svdecomp-symenv-p symenv))) :rule-classes :rewrite)
Theorem:
(defthm svex-decomp-process-env-correct (b* (((mv err sval symenv) (svex-decomp-process-env-term x vars)) (env (svdecomp-ev-symenv symenv a))) (implies (and (not err) (member (svar-fix k) (svarlist-fix vars))) (and (implies (svar-lookup k sval) (4vec-equiv (svex-eval (cdr (svar-lookup k sval)) env) (svex-env-lookup k (svdecomp-ev-symenv x a)))) (implies (not (svar-lookup k sval)) (and (svar-lookup k symenv) (4vec-equiv (svdecomp-ev (cdr (svar-lookup k symenv)) a) (svex-env-lookup k (svdecomp-ev-symenv x a)))))))))
Theorem:
(defthm svex-eval-with-svex-decomp-process-env (b* (((mv err sval symenv) (svex-decomp-process-env-term env1 vars)) (env (svdecomp-ev-symenv symenv a))) (implies (and (not err) (double-rewrite (subsetp (svex-vars x) (svarlist-fix vars)))) (equal (svex-eval x (append (svex-alist-eval sval env) env)) (svex-eval x (svdecomp-ev-symenv env1 a))))))
Theorem:
(defthm svexlist-eval-with-svex-decomp-process-env (b* (((mv err sval symenv) (svex-decomp-process-env-term env1 vars)) (env (svdecomp-ev-symenv symenv a))) (implies (and (not err) (double-rewrite (subsetp (svexlist-vars x) (svarlist-fix vars)))) (equal (svexlist-eval x (append (svex-alist-eval sval env) env)) (svexlist-eval x (svdecomp-ev-symenv env1 a))))))
Theorem:
(defthm svex-decomp-process-env-term-of-svarlist-fix-vars (equal (svex-decomp-process-env-term x (svarlist-fix vars)) (svex-decomp-process-env-term x vars)))
Theorem:
(defthm svex-decomp-process-env-term-svarlist-equiv-congruence-on-vars (implies (svarlist-equiv vars vars-equiv) (equal (svex-decomp-process-env-term x vars) (svex-decomp-process-env-term x vars-equiv))) :rule-classes :congruence)