		Search-engine friendly clone of the ACL2 documentation.

Programming

<<

A total ordering on ACL2 objects.

(<< x y) is a total ordering on ACL2 objects, defined in the misc/total-order book. For more information about the development of this order, see the associated workshop paper:

Matt Kaufmann and Pete Manolios. Adding a Total Order to ACL2. ACL2 Workshop, 2002.

Efficiency note. In the implementation, we generally use fast-<< and fast-lexorder, which are probably faster alternatives to << and lexorder, respectively.

Definitions and Theorems

Function: <<

(defun << (x y)
  (declare (xargs :guard t))
  (mbe :logic (and (lexorder x y) (not (equal x y)))
       :exec (fast-<< x y)))

Theorem: <<-irreflexive

(defthm <<-irreflexive (not (<< x x)))

Theorem: <<-transitive

(defthm <<-transitive
  (implies (and (<< x y) (<< y z))
           (<< x z)))

Theorem: <<-asymmetric

(defthm <<-asymmetric
  (implies (<< x y) (not (<< y x))))

Theorem: <<-trichotomy

(defthm <<-trichotomy
  (implies (and (not (<< y x)) (not (equal x y)))
           (<< x y)))

Theorem: <<-implies-lexorder

(defthm <<-implies-lexorder
  (implies (<< x y) (lexorder x y)))

Subtopics

Alphorder: Total order on atoms
Lexorder: Total order on ACL2 objects
Fast-<<: Probably faster alternative to <<.