(svex-env-<<= x y) checks whether an entire svex-env
conservatively approximates another: i.e., is every variable's value in
Theorem:
(defthm svex-env-<<=-necc (implies (svex-env-<<= x y) (4vec-<<= (svex-env-lookup var x) (svex-env-lookup var y))))
Theorem:
(defthm svex-env-<<=-witnessing-witness-rule-correct (implies (not ((lambda (var y x) (not (4vec-<<= (svex-env-lookup var x) (svex-env-lookup var y)))) (svex-env-<<=-witness x y) y x)) (svex-env-<<= x y)) :rule-classes nil)
Theorem:
(defthm svex-env-<<=-instancing-instance-rule-correct (implies (not (4vec-<<= (svex-env-lookup var x) (svex-env-lookup var y))) (not (svex-env-<<= x y))) :rule-classes nil)
Theorem:
(defthm svex-env-<<=-of-svex-env-fix-x (equal (svex-env-<<= (svex-env-fix x) y) (svex-env-<<= x y)))
Theorem:
(defthm svex-env-<<=-svex-env-equiv-congruence-on-x (implies (svex-env-equiv x x-equiv) (equal (svex-env-<<= x y) (svex-env-<<= x-equiv y))) :rule-classes :congruence)
Theorem:
(defthm svex-env-<<=-of-svex-env-fix-y (equal (svex-env-<<= x (svex-env-fix y)) (svex-env-<<= x y)))
Theorem:
(defthm svex-env-<<=-svex-env-equiv-congruence-on-y (implies (svex-env-equiv y y-equiv) (equal (svex-env-<<= x y) (svex-env-<<= x y-equiv))) :rule-classes :congruence)
Theorem:
(defthm svex-env-<<=-empty (svex-env-<<= nil x))