Let x->y and u->v be two rules of a term rewriting system, and suppose these rules have no variables in common. If they do, rename the variables. If x_1 is a subterm of x (or the term x itself) such that it is not a variable, and the pair (x_1, u) is unifiable with the most general unifier θ, then y θ and the result of replacing x_1 θ in x θ by v θ are called a critical pair. The fact that all critical pairs of a term rewriting system are joinable, i.e., can be reduced to the same expression, implies that the system is locally confluent. For instance, if f(x, x)->x and g(f(x, y), x)->h(x), then g(x, x) and h(x) would form a critical pair because they can both be derived from g(f(x, x), x).

Church-Rosser property | confluent | finitely terminating | Knuth-Bendix completion algorithm | reduction order | term rewriting system