Newman's Lemma - Diamond Lemma

Diamond Lemma

In general, Newman's lemma can be seen as a general result in order theory, which holds for every preorder on a set A that has the following two properties:

• The preorder is a well-founded relation: every non-empty subset of A has a minimal element.

• (The diamond property) Every covering is bounded below. That is, if an element a in A covers elements b and c in A, so and, then there is an element in the pre-order A, such that and . Equivalently, a rewriting system is locally confluent.

If the above two conditions hold, then the lemma states that there is a bijection between the connected, directed graphs of the pre-order, and the minimal elements of A.

If A is a partial order, not just a preorder, the first condition is sometimes strengthened into an easier-to-recognize form: that every downward-descending chain terminates in a finite number of steps. That is, given a chain with, such a chain has at most n terms. Equivalently, a re-writing system is terminating in at most n steps.