Critical pair lemma
In mathematical logic, a critical pair arises in term rewriting systems where rewrite rules overlap to yield two different terms. In more detail, (t1, t2) is a critical pair if there is a term t for which two different applications of a rewrite rule (either the same rule applied differently, or two different rules) yield the terms t1 and t2.
For example, in the term rewriting system with rules
the only critical pair is ⟨g(x,z), f(x,z)⟩. Both of these terms can be derived from the term f(g(x,y),z) by applying a single rewrite rule.
As another example, consider the term rewriting system with the single rule
By applying this rule in two different ways to the term f(f(x,x),x), we see that (f(x,x), f(x,x)) is a (trivial) critical pair.
When both sides of the critical pair can reduce to the same term, the critical pair is called convergent. Where one side of the critical pair is identical to the other, the critical pair is called trivial.
If the term rewriting system is not confluent, the critical pair may not converge, so critical pairs are potential sources where confluence will fail. In fact, the critical pair lemma states that a term rewriting system is weakly (a.k.a. locally) confluent if all critical pairs are convergent. Thus, to find out if a term rewriting system is weakly confluent, it suffices to test all critical pairs and see if they are convergent. This makes it possible to find out algorithmically if a term rewriting system is weakly confluent or not, given that one can algorithmically check if two terms converge.
Weak confluence clearly implies convergent critical pairs: if any critical pair ⟨a, b⟩ arises, then a and b have common reduct and thus the critical pair is convergent.
...
Wikipedia