This is one fun little theorem.

Basically… if symbolic systems terminate (program halts/gives output), the terminating expression is independent of how the rules were applied.

You get “confluence” out of this.

You probably are thinking, “and so what does this have to do with my life?”

a) maybe nothing if arithmetic never enters your life (unlikely)

b) it’s extremely good to know when you use functional programming that you can get to the same answer with many different ways of writing something.  For good overview of functional programming, go here.