Newman's lemma
In mathematics, in the theory of rewriting systems, Newman's lemma, also commonly called the diamond lemma, states that a terminating (or strongly normalizing) abstract rewriting system (ARS), that is, one in which there are no infinite reduction sequences, is confluent if it is locally confluent. In fact a terminating ARS is confluent precisely when it is locally confluent. Equivalently, for every binary relation with no decreasing infinite chains and satisfying a weak version of the diamond property, there is a unique minimal element in every connected component of the relation considered as a graph. Today, this is seen as a purely combinatorial result based on well-foundedness due to a proof of Gérard Huet in 1980. Newman's original proof was considerably more complicated. Diamond lemma

In general, Newman's lemma can be seen as a combinatorial result about binary relations → on a set A (written backwards, so that a → b means that b is below a) with the following two properties:

 → is a well-founded relation: every non-empty subset X of A has a minimal element (an element a of X such that a → b for no b in X). Equivalently, there is no infinite chain . In the terminology of rewriting systems, → is terminating. Every covering is bounded below. That is, if an element a in A covers elements b and c in A in the sense that  and , then there is an element d in A such that  and , where  denotes the reflexive transitive closure of →. In the terminology of rewriting systems, → is locally confluent. The lemma states that if the above two conditions hold, then → is confluent: whenever  and , there is an element d such that  and . In view of the termination of →, this implies that every connected component of → as a graph contains a unique minimal element a, moreover  for every element b of the component. Notes

References
 M. H. A. Newman. On theories with a combinatorial definition of "equivalence". Annals of Mathematics, 43, Number 2, pages 223–243, 1942. Textbooks 
 Term Rewriting Systems, Terese, Cambridge Tracts in Theoretical Computer Science, 2003. (book weblink)
 Term Rewriting and All That, Franz Baader and Tobias Nipkow, Cambridge University Press, 1998 (book weblink)
 John Harrison, Handbook of Practical Logic and Automated Reasoning, Cambridge University Press, 2009, , chapter 4 "Equality". External links
 
 "Newman's Proof of Newman's Lemma", a PDF on the original proof, 

Wellfoundedness
Lemmas
Rewriting systems