(alist-collect-compositions x) → (mv err base-env envmap)
Function:
(defun alist-collect-compositions (x) (declare (xargs :guard (svdecomp-symenv-p x))) (let ((__function__ 'alist-collect-compositions)) (declare (ignorable __function__)) (b* ((x (fast-alist-free (fast-alist-clean (svar-alist-fix x)))) ((mv err base-env envmap) (alist-collect-compositions-aux x nil nil))) (mv err base-env (fast-alist-clean envmap)))))
Theorem:
(defthm svdecomp-symenv-p-of-alist-collect-compositions.base-env (implies (and (svdecomp-symenv-p x)) (b* (((mv ?err ?base-env ?envmap) (alist-collect-compositions x))) (svdecomp-symenv-p base-env))) :rule-classes :rewrite)
Theorem:
(defthm envmap-p-of-alist-collect-compositions.envmap (implies (and (svdecomp-symenv-p x)) (b* (((mv ?err ?base-env ?envmap) (alist-collect-compositions x))) (envmap-p envmap))) :rule-classes :rewrite)
Theorem:
(defthm alist-collect-compositions-envmap-lookup-eval (b* (((mv ?err ?base-env ?envmap) (alist-collect-compositions x))) (implies (and (svar-lookup k (envmap->svex-alist envmap)) (not err)) (equal (svdecomp-ev (cdr (svar-lookup k (envmap-to-term-alist envmap))) a) (svdecomp-ev (cdr (svar-lookup k x)) a)))))
Theorem:
(defthm eval-lookup-in-envmap-entry-to-term-alist (implies (svar-lookup k (svex-alist-fix svalist)) (equal (svdecomp-ev (cdr (svar-lookup k (envmap-entry-to-term-alist svalist env))) a) (svex-eval (cdr (svar-lookup k svalist)) (svdecomp-ev env a)))))
Theorem:
(defthm 4vec-p-lookup-in-envmap-to-term-alist (implies (svar-lookup k (envmap->svex-alist envmap)) (4vec-p (svdecomp-ev (cdr (svar-lookup k (envmap-to-term-alist envmap))) a))))
Theorem:
(defthm alist-collect-compositions-envmap-implies-4vec-term (b* (((mv ?err ?base-env ?envmap) (alist-collect-compositions x))) (implies (and (svar-lookup k (envmap->svex-alist envmap)) (not err)) (svdecomp-4vec-termp (cdr (svar-lookup k x))))) :rule-classes :forward-chaining)
Theorem:
(defthm alist-collect-compositions-base-env-lookup (b* (((mv ?err ?base-env ?envmap) (alist-collect-compositions x))) (implies (and (case-split (not (svar-lookup k (envmap->svex-alist envmap)))) (not err)) (equal (svar-lookup k base-env) (svar-lookup k x)))))
Theorem:
(defthm alist-collect-compositions-of-svar-alist-fix-x (equal (alist-collect-compositions (svar-alist-fix x)) (alist-collect-compositions x)))
Theorem:
(defthm alist-collect-compositions-svar-alist-equiv-congruence-on-x (implies (svar-alist-equiv x x-equiv) (equal (alist-collect-compositions x) (alist-collect-compositions x-equiv))) :rule-classes :congruence)