Theorem:
(defthm svex-alist-<<=-necc (implies (svex-alist-<<= x y) (svex-env-<<= (svex-alist-eval x env) (svex-alist-eval y env))))
Theorem:
(defthm svex-alist-eval-equiv-implies-equal-svex-alist-<<=-1 (implies (svex-alist-eval-equiv x x-equiv) (equal (svex-alist-<<= x y) (svex-alist-<<= x-equiv y))) :rule-classes (:congruence))
Theorem:
(defthm svex-alist-eval-equiv-implies-equal-svex-alist-<<=-2 (implies (svex-alist-eval-equiv y y-equiv) (equal (svex-alist-<<= x y) (svex-alist-<<= x y-equiv))) :rule-classes (:congruence))
Theorem:
(defthm svex-<<=-of-svex-lookup-when-svex-alist-<<= (implies (svex-alist-<<= x y) (svex-<<= (svex-lookup k x) (svex-lookup k y))))
Theorem:
(defthm svex-<<=-of-svex-compose-lookup-when-svex-alist-<<= (implies (and (svex-alist-<<= x y) (set-equiv (svex-alist-keys x) (svex-alist-keys y))) (svex-<<= (svex-compose-lookup k x) (svex-compose-lookup k y))))
Function:
(defun svex-alist-<<=-lookup-witness (x y) (svex-env-<<=-witness (svex-alist-eval x (svex-alist-<<=-witness x y)) (svex-alist-eval y (svex-alist-<<=-witness x y))))
Theorem:
(defthm svex-alist-<<=-in-terms-of-lookup (equal (svex-alist-<<= x y) (let ((var (svex-alist-<<=-lookup-witness x y))) (svex-<<= (svex-lookup var x) (svex-lookup var y)))) :rule-classes ((:definition :install-body nil)))
Theorem:
(defthm svex-alist-<<=-refl (svex-alist-<<= x x))
Theorem:
(defthm svex-alist-<<=-transitive-1 (implies (and (svex-alist-<<= x y) (svex-alist-<<= y z)) (svex-alist-<<= x z)))
Theorem:
(defthm svex-alist-<<=-transitive-2 (implies (and (svex-alist-<<= y z) (svex-alist-<<= x y)) (svex-alist-<<= x z)))
Theorem:
(defthm svex-alist-<<=-asymm (implies (and (svex-alist-<<= x y) (set-equiv (svex-alist-keys x) (svex-alist-keys y))) (iff (svex-alist-<<= y x) (svex-alist-eval-equiv y x))))