The Diamond Lemma

I found this result useful for a few different problems I was thinking about recently. It cleared up a lot of confusion I had around simplification rules. First I give a semiformal statement of the lemma and some applications. At the end I give a formal statement and proof.SetupSuppose you have a set S and some possible transitions where one element of S “simplifies” into another. The diamond lemma has two requirements:There is no infinite chain of simplifications. If you start somewhere and kee...