 we write formula_26 if "x" and "y" are joinable.An ARS is said to possess the Church-Rosser property if and only if formula_27 implies formula_26 for all objects "x", "y".Equivalently, the Church-Rosser property means that the reflexive transitive symmetric closure is contained in the joinability relation.