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.Setup Suppose 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 keep simplifying, you will eventually reach a terminal state where no simplifications are possible.If some state s1 has simplifications to both s2 and s3, then there are paths to “merge” s2 and s3 back to some common state t (see the diagram). This is the “diamond” from the lemma’s name.If both of these requirements are met, the diamond lemma guarantees that if you start simplifying from a given state s, the final state you end up at is the same, regardless of which path you choose.ExamplesAbelian sandpilesLet G be a connected graph. Label some vertex t of G as the sink. Each vertex will have some nonnegative number of grains of sand on it. If the number of grains of sand on some vertex v is at least the number of neighboring vertices, you can “topple” that vertex by moving one grain of sand to each neighboring vertex from v. Any grains of sand that move to the sink disappear instead of accumulating.Initial configuration. The vertex marked “-” is the sink.State of the sandpile after toppling the vertex with 5 grains.State of the sandpile when no further topples are possible.It turns out that if you start topple from some initial configuration until no further topples are possible, the final state is independent of which topples you choose to make! This fact was pretty surprising to me when I first heard it, but is easy to prove with the diamond lemma.First we have to show there is no infinite chain. If there was an infinite chain then some vertex would have to fire infinitely ma