(svex-envs-check-ovtests-ok x y overridekey-set) → *
Function:
(defun svex-envs-check-ovtests-ok (x y overridekey-set) (declare (xargs :guard (and (svex-env-p x) (svex-env-p y)))) (let ((__function__ 'svex-envs-check-ovtests-ok)) (declare (ignorable __function__)) (svex-envs-check-ovtests-ok-rec (append (alist-keys (svex-env-fix x)) (alist-keys (svex-env-fix y))) x y overridekey-set)))
Theorem:
(defthm svex-envs-check-ovtests-ok-correct (iff (svex-envs-check-ovtests-ok x y (pairlis$ (svarlist-change-override overridekeys :test) nil)) (svex-envs-ovtests-ok x y overridekeys)))
Theorem:
(defthm svex-envs-check-ovtests-ok-of-svex-env-fix-x (equal (svex-envs-check-ovtests-ok (svex-env-fix x) y overridekey-set) (svex-envs-check-ovtests-ok x y overridekey-set)))
Theorem:
(defthm svex-envs-check-ovtests-ok-svex-env-equiv-congruence-on-x (implies (svex-env-equiv x x-equiv) (equal (svex-envs-check-ovtests-ok x y overridekey-set) (svex-envs-check-ovtests-ok x-equiv y overridekey-set))) :rule-classes :congruence)
Theorem:
(defthm svex-envs-check-ovtests-ok-of-svex-env-fix-y (equal (svex-envs-check-ovtests-ok x (svex-env-fix y) overridekey-set) (svex-envs-check-ovtests-ok x y overridekey-set)))
Theorem:
(defthm svex-envs-check-ovtests-ok-svex-env-equiv-congruence-on-y (implies (svex-env-equiv y y-equiv) (equal (svex-envs-check-ovtests-ok x y overridekey-set) (svex-envs-check-ovtests-ok x y-equiv overridekey-set))) :rule-classes :congruence)