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