(svex-envlists-ovtestsimilar x y) → *
Function:
(defun svex-envlists-ovtestsimilar (x y) (declare (xargs :guard (and (svex-envlist-p x) (svex-envlist-p y)))) (let ((__function__ 'svex-envlists-ovtestsimilar)) (declare (ignorable __function__)) (if (atom x) (atom y) (and (consp y) (ec-call (svex-envs-ovtestsimilar (car x) (car y))) (svex-envlists-ovtestsimilar (cdr x) (cdr y))))))
Theorem:
(defthm svex-envlists-ovtestsimilar-is-an-equivalence (and (booleanp (svex-envlists-ovtestsimilar x y)) (svex-envlists-ovtestsimilar x x) (implies (svex-envlists-ovtestsimilar x y) (svex-envlists-ovtestsimilar y x)) (implies (and (svex-envlists-ovtestsimilar x y) (svex-envlists-ovtestsimilar y z)) (svex-envlists-ovtestsimilar x z))) :rule-classes (:equivalence))
Theorem:
(defthm svex-envlists-similar-refines-svex-envlists-ovtestsimilar (implies (svex-envlists-similar x y) (svex-envlists-ovtestsimilar x y)) :rule-classes (:refinement))
Theorem:
(defthm svex-envlists-ovtestsimilar-of-svex-envlist-fix-x (equal (svex-envlists-ovtestsimilar (svex-envlist-fix x) y) (svex-envlists-ovtestsimilar x y)))
Theorem:
(defthm svex-envlists-ovtestsimilar-svex-envlist-equiv-congruence-on-x (implies (svex-envlist-equiv x x-equiv) (equal (svex-envlists-ovtestsimilar x y) (svex-envlists-ovtestsimilar x-equiv y))) :rule-classes :congruence)
Theorem:
(defthm svex-envlists-ovtestsimilar-of-svex-envlist-fix-y (equal (svex-envlists-ovtestsimilar x (svex-envlist-fix y)) (svex-envlists-ovtestsimilar x y)))
Theorem:
(defthm svex-envlists-ovtestsimilar-svex-envlist-equiv-congruence-on-y (implies (svex-envlist-equiv y y-equiv) (equal (svex-envlists-ovtestsimilar x y) (svex-envlists-ovtestsimilar x y-equiv))) :rule-classes :congruence)