Newman's lemma

In theoretical computer science, specifically in term rewriting, Newman's lemma, also commonly called the diamond lemma, is a criterion to prove that an abstract rewriting system is confluent. It states that local confluence is a sufficient condition for confluence, provided that the system is also terminating. This is useful since local confluence is usually easier to verify than confluence.

The lemma was originally proved by Max Newman in 1942. A considerably simpler proof (given below) was proposed by Gérard Huet. A number of other proofs exist.