(svex-envlists-ovtests-ok x y overridekeys) → *
Function:
(defun svex-envlists-ovtests-ok (x y overridekeys) (declare (xargs :guard (and (svex-envlist-p x) (svex-envlist-p y) (svarlist-p overridekeys)))) (let ((__function__ 'svex-envlists-ovtests-ok)) (declare (ignorable __function__)) (if (atom x) (atom y) (and (consp y) (ec-call (svex-envs-ovtests-ok (car x) (car y) overridekeys)) (svex-envlists-ovtests-ok (cdr x) (cdr y) overridekeys)))))
Theorem:
(defthm svex-envlists-ovtestsimilar-implies-iff-svex-envlists-ovtests-ok-1 (implies (svex-envlists-ovtestsimilar x x-equiv) (iff (svex-envlists-ovtests-ok x y overridekeys) (svex-envlists-ovtests-ok x-equiv y overridekeys))) :rule-classes (:congruence))
Theorem:
(defthm svex-envlists-ovtestsimilar-implies-iff-svex-envlists-ovtests-ok-2 (implies (svex-envlists-ovtestsimilar y y-equiv) (iff (svex-envlists-ovtests-ok x y overridekeys) (svex-envlists-ovtests-ok x y-equiv overridekeys))) :rule-classes (:congruence))
Theorem:
(defthm svex-envlists-ovtests-ok-of-svex-envlist-fix-x (equal (svex-envlists-ovtests-ok (svex-envlist-fix x) y overridekeys) (svex-envlists-ovtests-ok x y overridekeys)))
Theorem:
(defthm svex-envlists-ovtests-ok-svex-envlist-equiv-congruence-on-x (implies (svex-envlist-equiv x x-equiv) (equal (svex-envlists-ovtests-ok x y overridekeys) (svex-envlists-ovtests-ok x-equiv y overridekeys))) :rule-classes :congruence)
Theorem:
(defthm svex-envlists-ovtests-ok-of-svex-envlist-fix-y (equal (svex-envlists-ovtests-ok x (svex-envlist-fix y) overridekeys) (svex-envlists-ovtests-ok x y overridekeys)))
Theorem:
(defthm svex-envlists-ovtests-ok-svex-envlist-equiv-congruence-on-y (implies (svex-envlist-equiv y y-equiv) (equal (svex-envlists-ovtests-ok x y overridekeys) (svex-envlists-ovtests-ok x y-equiv overridekeys))) :rule-classes :congruence)
Theorem:
(defthm svex-envlists-ovtests-ok-of-svarlist-fix-overridekeys (equal (svex-envlists-ovtests-ok x y (svarlist-fix overridekeys)) (svex-envlists-ovtests-ok x y overridekeys)))
Theorem:
(defthm svex-envlists-ovtests-ok-svarlist-equiv-congruence-on-overridekeys (implies (svarlist-equiv overridekeys overridekeys-equiv) (equal (svex-envlists-ovtests-ok x y overridekeys) (svex-envlists-ovtests-ok x y overridekeys-equiv))) :rule-classes :congruence)