A strict order > on the set of terms of a term rewriting system is called a reduction order if 1. The set of terms is well ordered with respect to >, that is, all its nonempty subsets contain their least elements, 2. This order is compatible with functions (operations) of the system, i.e., t_i>t_i^, ⇒f(t_1, ..., t_i, ..., t_n)>f(t_1, ..., t_i^, , ..., t_n), and 3. For any substitution θ (cf. unification), s>t⇒s θ>t θ. If x>y holds for every rewriting rule x->y, then this term rewriting system is finitely terminating.

Church-Rosser property | confluent | critical pair | Knuth-Bendix completion algorithm | term rewriting system