Diamond Lemma

In theoretical computer science , the Diamond Lemma (also: Newman's theorem , after Max Newman ) says that a well-founded relation is confluent if and only if it is locally confluent .

This result is the basis for deciding the confluence in terminating term replacement systems .

Since the diagram in the proof of this theorem is remotely reminiscent of a diamond , it was given this name.