term_order : term -> term -> bool

SYNOPSIS
Term order for use in AC-rewriting.

DESCRIPTION
This binary predicate implements a crude but fairly efficient ordering on terms that is appropriate for ensuring that ordered rewriting will perform normalization.

FAILURE CONDITIONS
Never fails.

EXAMPLE
This example shows how using ordered rewriting with this term ordering can give normalization under associative and commutative laws given the appropriate rewrites:
  # ADD_AC;;
val it : thm =
|- m + n = n + m /\ (m + n) + p = m + n + p /\ m + n + p = n + m + p

\noindent
  # TOP_DEPTH_CONV
(FIRST_CONV(map (ORDERED_REWR_CONV term_order) (CONJUNCTS ADD_AC)))
d + (f + a) + b + (c + e):num;;
val it : thm = |- d + (f + a) + b + c + e = a + b + c + d + e + f


USES
It is used automatically when applying permutative rewrite rules inside rewriting and simplification. Users will not normally want to use it explicitly, though the example above shows roughly what goes on there.

SEE ALSO
ORDERED_IMP_REWR_CONV, ORDERED_REWR_CONV.