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.