1; This total order book, put together by Matt Kaufmann, is culled from events
2; contributed by Pete Manolios and also benefits from contributions by Rob
3; Sumners.
4
5(in-package "ACL2")
6
7(defun << (x y)
8  (declare (xargs :guard t))
9  (and (lexorder x y)
10       (not (equal x y))))
11
12(defthm <<-irreflexive
13  (not (<< x x)))
14
15(defthm <<-transitive
16  (implies (and (<< x y)
17                (<< y z))
18           (<< x z)))
19
20(defthm <<-asymmetric
21  (implies (<< x y)
22           (not (<< y x))))
23
24(defthm <<-trichotomy
25  (implies (and (not (<< y x))
26                (not (equal x y)))
27           (<< x y)))
28
29(defthm <<-implies-lexorder
30  (implies (<< x y)
31	   (lexorder x y)))
32
33(in-theory (disable <<))
34