Church-Rosser property

Let $\to$ be a reduction (a binary relation) on a set $S$, and let ${\leftrightarrow }^{*}$ be the reflexive transitive symmetric closure of $\to$. The reduction $\to$ is said to have the Church-Rosser property provided that $a{\leftrightarrow }^{*}b$ implies that $a$ and $b$ are joinable, for any $a,b\in S$.

In terms of diagrams, the Church-Rosser property means the following, for any $a,b\in S$, if

$$a\leftrightarrow x_1\leftrightarrow x_2\leftrightarrow \mathrm{\cdots }\leftrightarrow x_n\leftrightarrow b$$

where $u\leftrightarrow v$ means $u\to v$ or $u\leftarrow v$ ($:=v\to u$), then there is some $x\in S$ such that

$$a\to a_1\mathrm{\cdots }\to a_p\to x\leftarrow b_q\leftarrow \mathrm{\cdots }\leftarrow b_1\leftarrow b.$$

Remark. It can be shown that $\to$ has the Church-Rosser property iff it is confluent.