An ARS is said to possess the Church–Rosser property if formula_50 implies formula_47. In words, the Church–Rosser property means that any two equivalent objects are joinable. Alonzo Church and J. Barkley Rosser proved in 1936 that lambda calculus has this property; hence the name of the property. (That lambda calculus has this property is also known as the Church–Rosser theorem.) In an ARS with the Church–Rosser property the word problem may be reduced to the search for a common successor. In a Church–Rosser system, an object has "at most one" normal form; that is the normal form of an object is unique if it exists, but it may well not exist.