Church–Rosser theorem

The Church–Rosser theorem is a fundamental result in the field of lambda calculus and more generally in the theory of computation. It establishes an important property regarding the reduction of expressions in lambda calculus. Specifically, the theorem states that if a lambda expression can be reduced to two different normal forms, then those two normal forms must be equivalent (i.e., they represent the same lambda expression).