diamond lemma
The diamond lemmas constitute a of results about the existence of a unique normal form. Diamond lemmas exist in many diverse areas of mathematics, and as a result their technical contents can be quite different, but they are easily recognisable from their overall and basic idea — the “diamond” condition from which they inherit their name.
1 Newman’s Diamond Lemma
The basic diamond lemma, that of Newman [Newman], is today most easily presented in of binary relations^{}.
Theorem 1.
Let $X$ be a set and let $\mathrm{\to}$ be a binary relation on $X$. If $\mathrm{\to}$ is terminating, then the following conditions are equivalent^{}:

1.
For all $a,b,c\in X$ such that $a\to b$ and $a\to c$, then $b$ and $c$ are joinable.

2.
Every $a\in X$ has a unique normal form.
Condition 1 can be graphically drawn as
$$\text{xymatrix@}2ex\mathrm{\&}a\text{xy@@ix@}$$ 