		Search-engine friendly clone of the ACL2 documentation.

4veclist-<<=

Nth-wise lattice ordering for 4veclists.

Definitions and Theorems

Theorem: 4veclist-<<=-necc

(defthm 4veclist-<<=-necc
  (implies (4veclist-<<= x y)
           (4vec-<<= (4veclist-nth-safe idx x)
                     (4veclist-nth-safe idx y))))

Theorem: 4veclist-<<=-witnessing-witness-rule-correct

(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: 4veclist-<<=-instancing-instance-rule-correct

(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: 4veclist-<<=-of-4veclist-fix-x

(defthm 4veclist-<<=-of-4veclist-fix-x
  (equal (4veclist-<<= (4veclist-fix x) y)
         (4veclist-<<= x y)))

Theorem: 4veclist-<<=-4veclist-equiv-congruence-on-x

(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: 4veclist-<<=-of-4veclist-fix-y

(defthm 4veclist-<<=-of-4veclist-fix-y
  (equal (4veclist-<<= x (4veclist-fix y))
         (4veclist-<<= x y)))

Theorem: 4veclist-<<=-4veclist-equiv-congruence-on-y

(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: 4veclist-<<=-empty

(defthm 4veclist-<<=-empty
  (4veclist-<<= nil x))

Theorem: 4veclist-<<=-refl

(defthm 4veclist-<<=-refl
  (4veclist-<<= x x))

Theorem: 4veclist-<<=-of-cons

(defthm 4veclist-<<=-of-cons
  (iff (4veclist-<<= (cons a b) c)
       (and (4vec-<<= a (car c))
            (4veclist-<<= b (cdr c)))))

Theorem: 4veclist-<<=-of-cons-2

(defthm 4veclist-<<=-of-cons-2
  (iff (4veclist-<<= c (cons a b))
       (and (4vec-<<= (car c) a)
            (4veclist-<<= (cdr c) b))))

Theorem: 4veclist-<<=-of-atom

(defthm 4veclist-<<=-of-atom
  (implies (atom x) (4veclist-<<= x y)))

Theorem: 4veclist-<<=-transitive-1

(defthm 4veclist-<<=-transitive-1
  (implies (and (4veclist-<<= a b)
                (4veclist-<<= b c))
           (4veclist-<<= a c)))

Theorem: 4veclist-<<=-transitive-2

(defthm 4veclist-<<=-transitive-2
  (implies (and (4veclist-<<= b c)
                (4veclist-<<= a b))
           (4veclist-<<= a c)))

Theorem: 4veclist-<<=-asymm

(defthm 4veclist-<<=-asymm
  (implies (and (4veclist-<<= x y)
                (equal (len x) (len y)))
           (iff (4veclist-<<= y x)
                (4veclist-equiv y x))))