(svdecomp-symenv-compat-union x y) → (mv err union)
Function:
(defun svdecomp-symenv-compat-union (x y) (declare (xargs :guard (and (svdecomp-symenv-p x) (svdecomp-symenv-p y)))) (let ((__function__ 'svdecomp-symenv-compat-union)) (declare (ignorable __function__)) (b* (((when (atom x)) (mv nil (svar-alist-fix y))) ((unless (mbt (and (consp (car x)) (svar-p (caar x))))) (svdecomp-symenv-compat-union (cdr x) y)) ((cons var val) (car x)) (look (svar-lookup var (svar-alist-fix y))) ((unless (or (not look) (equal (cdr look) val))) (mv (msg "Mismatch: key ~x0, val ~x1 versus ~x2~%" var val (cdr look)) nil))) (svdecomp-symenv-compat-union (cdr x) (if look y (hons-acons var val y))))))
Theorem:
(defthm svdecomp-symenv-p-of-svdecomp-symenv-compat-union.union (implies (and (svdecomp-symenv-p x) (svdecomp-symenv-p y)) (b* (((mv ?err set::?union) (svdecomp-symenv-compat-union x y))) (svdecomp-symenv-p union))) :rule-classes :rewrite)
Theorem:
(defthm svdecomp-symenv-compat-union-error-cond (b* (((mv symerr ?symunion) (svdecomp-symenv-compat-union x y)) ((mv err ?union) (svex-env-compat-union (svdecomp-ev-symenv x a) (svdecomp-ev-symenv y a)))) (implies (not symerr) (not err))))
Theorem:
(defthm eval-svdecomp-symenv-compat-union (b* (((mv symerr ?symunion) (svdecomp-symenv-compat-union x y)) ((mv ?err ?union) (svex-env-compat-union (svdecomp-ev-symenv x a) (svdecomp-ev-symenv y a)))) (implies (not symerr) (svex-env-equiv (svdecomp-ev-symenv symunion a) union))))
Theorem:
(defthm lookup-in-svdecomp-symenv-compat-union-when-in-y (b* (((mv symerr ?symunion) (svdecomp-symenv-compat-union x y))) (implies (and (not symerr) (svar-lookup k y)) (equal (svar-lookup k symunion) (svar-lookup k y)))))
Theorem:
(defthm lookup-in-svdecomp-symenv-compat-union-when-not-in-y (b* (((mv symerr ?symunion) (svdecomp-symenv-compat-union x y))) (implies (and (not symerr) (case-split (not (svar-lookup k y)))) (equal (svar-lookup k symunion) (svar-lookup k x)))))
Theorem:
(defthm lookup-in-svdecomp-symenv-compat-union-when-in-x (b* (((mv symerr ?symunion) (svdecomp-symenv-compat-union x y))) (implies (and (not symerr) (svar-lookup k x)) (equal (svar-lookup k symunion) (svar-lookup k x)))))
Theorem:
(defthm lookup-in-svdecomp-symenv-compat-union-when-not-in-x (b* (((mv symerr ?symunion) (svdecomp-symenv-compat-union x y))) (implies (and (not symerr) (case-split (not (svar-lookup k x)))) (equal (svar-lookup k symunion) (svar-lookup k y)))))
Theorem:
(defthm alist-keys-of-svdecomp-symenv-compat-union (b* (((mv err union) (svdecomp-symenv-compat-union env env2))) (implies (not err) (set-equiv (svar-alist-keys union) (append (svar-alist-keys env) (svar-alist-keys env2))))))
Theorem:
(defthm svdecomp-symenv-compat-union-of-svar-alist-fix-x (equal (svdecomp-symenv-compat-union (svar-alist-fix x) y) (svdecomp-symenv-compat-union x y)))
Theorem:
(defthm svdecomp-symenv-compat-union-svar-alist-equiv-congruence-on-x (implies (svar-alist-equiv x x-equiv) (equal (svdecomp-symenv-compat-union x y) (svdecomp-symenv-compat-union x-equiv y))) :rule-classes :congruence)
Theorem:
(defthm svdecomp-symenv-compat-union-of-svar-alist-fix-y (equal (svdecomp-symenv-compat-union x (svar-alist-fix y)) (svdecomp-symenv-compat-union x y)))
Theorem:
(defthm svdecomp-symenv-compat-union-svar-alist-equiv-congruence-on-y (implies (svar-alist-equiv y y-equiv) (equal (svdecomp-symenv-compat-union x y) (svdecomp-symenv-compat-union x y-equiv))) :rule-classes :congruence)