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 )

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

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 A5:
for a, b being object st a,b are_convertible_wrt the reduction of X holds
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

end;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;

end;

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;x <=*=> y by A2;

hence a,b are_convergent_wrt the reduction of X by A1, Ch12; :: thesis: verum

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