next up previous contents
Next: The Hypothesis Facility Up: The Tactic Language Previous: The Special Theorems INPUT

The Special Theorem ORDERED

The built-in theorem ORDERED has no effect on a term to which it is applied. When it is presented with an infix term, it reports success when the two top-level subterms are in order (an order is defined on terms, which is lexicographic on atoms with constants prededing variables and is determined by the rightmost element of a complex term) and failure otherwise. When presented with other kinds of terms, it reports success as a default. The theorem can be applied in conjunction with commutative laws for operations in the building of sorting algorithms.

Randall Holmes
Fri Sep 5 16:28:58 MDT 1997