I'd like to learn the Newman's Lemma or Diamond Lemma (the one used in abstract rewriting system), can someone recommend me some books where I can read it? I'd appreciate self-contained books with examples. Thank you.



Newman's Lemma or Diamond Lemma
* [Franz Baader and Tobias Nipkow, *Term Rewriting and All That*](https://www21.in.tum.de/~nipkow/TRaAT/) is a book fully devoted to term rewriting; much of it is about applying the diamond lemma.
* [Vincent van Oostrom, *Newman's proof of Newman's lemma*](http://gen.lib.rus.ec/book/index.php?md5=98C760060ED7C8CBA02612BDC53EF201) proves the lemma itself on just 1 page. That's not the shortest proof.
* [Gert Smolka, *Confluence and Normalization in Reduction Systems*](https://www.ps.uni-saarland.de/courses/sem-ws15/ars.pdf) proves the diamond lemma in §15, after showing all sorts of related things. These notes are clearly written for computer scientists (the notations resemble Coq), but from what I've seen are fairly readable.
* [Kimmo Eriksson, *Strong convergence and the polygon property of 1-player games*, Discrete Mathematics, Volume 153, Issues 1--3, 1 June 1996, Pages 105--122](https://doi.org/10.1016/0012-365X(95)00131-F) explores the "Polygon property theorem", which is similar to the diamond lemma. (It requires the play sequences to be of the same length, which makes it somewhat more restrictive, but its conclusion is accordingly stronger.)
* [George M. Bergman, *The diamond lemma for ring theory*, Advances in Mathematics, Volume 29, Issue 2, February 1978, Pages 178--218](https://doi.org/10.1016/0001-8708(78)90010-5) ([errata](https://math.berkeley.edu/~gbergman/papers/updates/diamond.html)) applies the diamond lemma to the study of algebras.
* As @MarkSapir pointed out, [Mark Sapir, *Combinatorial algebra: syntax and
semantics*, Springer 2014](https://math.vanderbilt.edu/sapirmv/book/b2.pdf) has a section (§1.7) on confluence.
* [Marc Bezem, Thierry Coquand, *Newman's Lemma -- a Case Study in Proof Automation and Geometric Logic*](http://www.cse.chalmers.se/~coquand/bul.ps) proves a "bi-colored" analogue of Newman's lemma.
* [Lars Hellström, *The Diamond Lemma for Power Series Algebras*](http://www.diva-portal.org/smash/record.jsf?pid=diva2%3A145049&dswid=-6405) gives an analogue of the ring-theoretical diamond lemma for infinite-but-sort-of-convergent rewriting sequences (I am being deliberately vague here, since I've read only the motivating sections of this).


Self-containedness isn't really an issue in this subject; the proof of the lemma is usually less than a page long, and there are zero prerequisites. I once gave an [expository talk about confluence](http://www.cip.ifi.lmu.de/~grinberg/algebra/diamond-talk.pdf) that includes a proof of the diamond lemma.


