Church-Rosser theorem

• There is no more than one normal form:

• The normal form

• Order of reductions doesn't matter

• The normal form is the value of a -expression

• (Alonzo Church and J. Barkley Rosser)