# 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 $\rightarrow$ be a binary relation on $X$. If $\rightarrow$ is terminating, then the following conditions are equivalent:

1. 1.

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

2. 2.

Every $a\in X$ has a unique normal form.

Condition 1 can be graphically drawn as

 $\xymatrix@-2ex{&a{}{}{}{}{}{}{}{}{}{}\xy@@ix@{{\hbox{}}}}$