A critical pair for two rules 
and 
of a term rewriting
system is the pair consisting of 
and the result of replacing 
in 
by 
, where 
is a nonvariable subterm of 
(possibly 
itself) and 
has most general unifier 
. The two rules are taken to have no variables in common,
with variables renamed when necessary.
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 
and 
,
then 
and 
would form a critical pair because they can both be derived from 
.
Note that it is possible for a critical pair to be produced by one rule, used in two different ways. For instance, in the string rewrite "AA" -> "B", the critical pair ("BA", "AB") results from applying the one rule to "AAA" in two different ways.
