A theorem of the lambda calculus. It states, basically, that each lambda expression with a terminating beta-reduction has a unique normal form, and that two lambda expressions are beta-equivalent if and only if they reduce to the same normal form. The Church-Rosser theorem also holds if beta reduction is replaced by beta-eta reduction.