Theorem:
(defthm svex-alist-ovcongruent-necc (implies (svex-alist-ovcongruent x) (implies (svex-envs-ovsimilar env1 env2) (equal (svex-envs-equivalent (svex-alist-eval x env1) (svex-alist-eval x env2)) t))))
Theorem:
(defthm svex-alist-eval-equiv-implies-equal-svex-alist-ovcongruent-1 (implies (svex-alist-eval-equiv x x-equiv) (equal (svex-alist-ovcongruent x) (svex-alist-ovcongruent x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm lookup-when-svex-alist-ovcongruent (implies (svex-alist-ovcongruent x) (svex-ovcongruent (svex-lookup k x))))
Theorem:
(defthm svex-compose-lookup-when-svex-alist-ovcongruent (implies (and (svex-alist-ovcongruent x) (not (svar-override-p k :test)) (not (svar-override-p k :val))) (svex-ovcongruent (svex-compose-lookup k x))))
Theorem:
(defthm svex-compose-preserves-svex-ovcongruent (implies (and (svex-ovcongruent x) (svex-alist-ovcongruent a) (svarlist-nonoverride-p (svex-alist-keys a) :test) (svarlist-nonoverride-p (svex-alist-keys a) :val)) (svex-ovcongruent (svex-compose x a))))
Theorem:
(defthm svexlist-compose-preserves-svexlist-ovcongruent (implies (and (svexlist-ovcongruent x) (svex-alist-ovcongruent a) (svarlist-nonoverride-p (svex-alist-keys a) :test) (svarlist-nonoverride-p (svex-alist-keys a) :val)) (svexlist-ovcongruent (svexlist-compose x a))))
Theorem:
(defthm svex-alist-compose-preserves-svex-alist-ovcongruent (implies (and (svex-alist-ovcongruent x) (svex-alist-ovcongruent a) (svarlist-nonoverride-p (svex-alist-keys a) :test) (svarlist-nonoverride-p (svex-alist-keys a) :val)) (svex-alist-ovcongruent (svex-alist-compose x a))))