A theorem, proved jointly by Alonzo Church and J. B. Rosser, concerning Church’s lambda calculus. It states that if a lambda-expression x can be reduced in two ways leading respectively to expressions y₁ and y₂ then there must be an expression z to which both y₁ and y₂ can be reduced. The choice of ways to reduce an expression arises from the possibility of separately reducing different ‘parts’ of the expression. The Church-Rosser theorem shows that either part can be worked on first, without the loss of any possibilities obtainable from starting with the other part. A corresponding theorem exists for combinatory logic. More generally, any language for which there is a notion of reduction for expressions within the language is said to have the Church-Rosser property, or to be confluent, if it admits an appropriate version of the Church-Rosser theorem. The property plays an important role in term rewriting with equations.