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