term_order : term -> term -> bool
Term order for use in AC-rewriting.
This binary predicate implements a crude but fairly efficient ordering on terms
that is appropriate for ensuring that ordered rewriting will perform
- FAILURE CONDITIONS
This example shows how using ordered rewriting with this term ordering can give
normalization under associative and commutative laws given the appropriate
val it : thm =
|- m + n = n + m /\ (m + n) + p = m + n + p /\ m + n + p = n + m + p
(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
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