Church-Rosser property

Alonzo Church and J. Barkley Rosser proved in 1936 that lambda calculus has this property.

Church-Rosser property (plural Church-Rosser properties)

1. (logic, computer science) The property of a rewriting system for which ${\displaystyle x{\stackrel {*}{\leftrightarrow }}y}$ implies ${\displaystyle x{\mathbin {\downarrow }}y}$ for all objects ${\displaystyle x}$, ${\displaystyle y}$.