Theorem:
(defthm svexlist-<<=-necc (implies (svexlist-<<= x y) (4veclist-<<= (svexlist-eval x env) (svexlist-eval y env))))
Theorem:
(defthm svexlist-eval-equiv-implies-equal-svexlist-<<=-1 (implies (svexlist-eval-equiv x x-equiv) (equal (svexlist-<<= x y) (svexlist-<<= x-equiv y))) :rule-classes (:congruence))
Theorem:
(defthm svexlist-eval-equiv-implies-equal-svexlist-<<=-2 (implies (svexlist-eval-equiv y y-equiv) (equal (svexlist-<<= x y) (svexlist-<<= x y-equiv))) :rule-classes (:congruence))
Theorem:
(defthm svex-<<=-car-when-svexlist-<<= (implies (svexlist-<<= x y) (svex-<<= (car x) (car y))))
Theorem:
(defthm svexlist-<<=-cdr-when-svexlist-<<= (implies (svexlist-<<= x y) (svexlist-<<= (cdr x) (cdr y))))
Theorem:
(defthm svex-<<=-nth-when-svexlist-<<= (implies (svexlist-<<= x y) (svex-<<= (nth n x) (nth n y))))
Theorem:
(defthm svexlist-<<=-of-cons (implies (and (svex-<<= x1 x2) (svexlist-<<= y1 y2)) (svexlist-<<= (cons x1 y1) (cons x2 y2))))
Theorem:
(defthm svexlist-<<=-refl (svexlist-<<= x x))
Theorem:
(defthm svexlist-<<=-transitive-1 (implies (and (svexlist-<<= x y) (svexlist-<<= y z)) (svexlist-<<= x z)))
Theorem:
(defthm svexlist-<<=-transitive-2 (implies (and (svexlist-<<= y z) (svexlist-<<= x y)) (svexlist-<<= x z)))
Theorem:
(defthm svexlist-<<=-asymm (implies (and (svexlist-<<= x y) (equal (len x) (len y))) (iff (svexlist-<<= y x) (svexlist-eval-equiv y x))))