let X be ARS ; :: thesis: ( X is CR iff the reduction of X is with_Church-Rosser_property )
set R = the reduction of X;
set A = the carrier of X;
F0: field the reduction of X c= the carrier of X \/ the carrier of X by RELSET_1:8;
thus ( X is CR implies the reduction of X is with_Church-Rosser_property ) :: thesis: ( the reduction of X is with_Church-Rosser_property implies X is CR )
proof
assume A1: for x, y being Element of X st x <=*=> y holds
x >><< y ; :: according to ABSRED_0:def 26 :: thesis: the reduction of X is with_Church-Rosser_property
let a, b be object ; :: according to REWRITE1:def 23 :: thesis: ( not a,b are_convertible_wrt the reduction of X or a,b are_convergent_wrt the reduction of X )
assume A2: a,b are_convertible_wrt the reduction of X ; :: thesis: a,b are_convergent_wrt the reduction of X
per cases ( ( a in field the reduction of X & b in field the reduction of X ) or a = b ) by A2, REWRITE1:32;
suppose ( a in field the reduction of X & b in field the reduction of X ) ; :: thesis: a,b are_convergent_wrt the reduction of X
then reconsider x = a, y = b as Element of X by F0;
x <=*=> y by A2;
hence a,b are_convergent_wrt the reduction of X by A1, Ch12; :: thesis: verum
end;
end;
end;
assume A5: for a, b being object st a,b are_convertible_wrt the reduction of X holds
a,b are_convergent_wrt the reduction of X ; :: according to REWRITE1:def 23 :: thesis: X is CR
let x be Element of X; :: according to ABSRED_0:def 26 :: thesis: for y being Element of X st x <=*=> y holds
x >><< y
let y be Element of X; :: thesis: ( x <=*=> y implies x >><< y )
assume x <=*=> y ; :: thesis: x >><< y
hence x >><< y by A5, Ch12; :: thesis: verum