Church-Rosser property of a reduction relation
= Church-Rosser property of a reduction relation
{c}
= Church-Rosser property
{c}
{synonym}
A reduction relation has the Church-Rosser property when its <equivalence relation> generated by forward and backward steps satisfies $b\leftrightarrow^*c\Rightarrow\exists d\;(b\to^*d\leftarrow^*c)$. It is equivalent to confluence of $\to^*$. The <Church-Rosser theorem> establishes it for <beta reduction>.