Nth-wise lattice ordering for 4veclists.
Theorem:
(defthm 4veclist-<<=-necc (implies (4veclist-<<= x y) (4vec-<<= (4veclist-nth-safe idx x) (4veclist-nth-safe idx y))))
Theorem:
(defthm 4veclist-<<=-witnessing-witness-rule-correct (implies (not ((lambda (idx y x) (not (4vec-<<= (4veclist-nth-safe idx x) (4veclist-nth-safe idx y)))) (4veclist-<<=-witness x y) y x)) (4veclist-<<= x y)) :rule-classes nil)
Theorem:
(defthm 4veclist-<<=-instancing-instance-rule-correct (implies (not (4vec-<<= (4veclist-nth-safe idx x) (4veclist-nth-safe idx y))) (not (4veclist-<<= x y))) :rule-classes nil)
Theorem:
(defthm 4veclist-<<=-of-4veclist-fix-x (equal (4veclist-<<= (4veclist-fix x) y) (4veclist-<<= x y)))
Theorem:
(defthm 4veclist-<<=-4veclist-equiv-congruence-on-x (implies (4veclist-equiv x x-equiv) (equal (4veclist-<<= x y) (4veclist-<<= x-equiv y))) :rule-classes :congruence)
Theorem:
(defthm 4veclist-<<=-of-4veclist-fix-y (equal (4veclist-<<= x (4veclist-fix y)) (4veclist-<<= x y)))
Theorem:
(defthm 4veclist-<<=-4veclist-equiv-congruence-on-y (implies (4veclist-equiv y y-equiv) (equal (4veclist-<<= x y) (4veclist-<<= x y-equiv))) :rule-classes :congruence)
Theorem:
(defthm 4veclist-<<=-empty (4veclist-<<= nil x))
Theorem:
(defthm 4veclist-<<=-refl (4veclist-<<= x x))
Theorem:
(defthm 4veclist-<<=-of-cons (iff (4veclist-<<= (cons a b) c) (and (4vec-<<= a (car c)) (4veclist-<<= b (cdr c)))))
Theorem:
(defthm 4veclist-<<=-of-cons-2 (iff (4veclist-<<= c (cons a b)) (and (4vec-<<= (car c) a) (4veclist-<<= (cdr c) b))))
Theorem:
(defthm 4veclist-<<=-of-atom (implies (atom x) (4veclist-<<= x y)))
Theorem:
(defthm 4veclist-<<=-transitive-1 (implies (and (4veclist-<<= a b) (4veclist-<<= b c)) (4veclist-<<= a c)))
Theorem:
(defthm 4veclist-<<=-transitive-2 (implies (and (4veclist-<<= b c) (4veclist-<<= a b)) (4veclist-<<= a c)))
Theorem:
(defthm 4veclist-<<=-asymm (implies (and (4veclist-<<= x y) (equal (len x) (len y))) (iff (4veclist-<<= y x) (4veclist-equiv y x))))