1(IN-PACKAGE "ACL2")
2
3(DEFUN << (X Y) (IF (LEXORDER X Y) (NOT (EQUAL X Y)) 'NIL))
4
5(DEFTHM <<-IRREFLEXIVE (NOT (<< X X)))
6
7(DEFTHM <<-TRANSITIVE (IMPLIES (IF (<< X Y) (<< Y Z) 'NIL) (<< X Z)))
8
9(DEFTHM <<-ASYMMETRIC (IMPLIES (<< X Y) (NOT (<< Y X))))
10
11(DEFTHM <<-TRICHOTOMY
12        (IMPLIES (IF (NOT (<< Y X))
13                     (NOT (EQUAL X Y))
14                     'NIL)
15                 (<< X Y)))
16
17(DEFTHM <<-IMPLIES-LEXORDER (IMPLIES (<< X Y) (LEXORDER X Y)))
18