let X be ARS ; :: thesis: ( X is WCR iff the reduction of X is locally-confluent )
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 WCR implies the reduction of X is locally-confluent ) :: thesis: ( the reduction of X is locally-confluent implies X is WCR )
proof
assume A1: for x, y being Element of X st x <<01>> y holds
x >><< y ; :: according to ABSRED_0:def 27 :: thesis: the reduction of X is locally-confluent
let a, b, c be object ; :: according to REWRITE1:def 24 :: thesis: ( not [a,b] in the reduction of X or not [a,c] in the reduction of X or b,c are_convergent_wrt the reduction of X )
assume A2: ( [a,b] in the reduction of X & [a,c] in the reduction of X ) ; :: thesis: b,c are_convergent_wrt the reduction of X
then ( a in field the reduction of X & b in field the reduction of X & c in field the reduction of X ) by RELAT_1:15;
then reconsider x = a, y = b, z = c as Element of X by F0;
( x ==> y & x ==> z ) by A2;
then ( x =01=> y & x =01=> z ) ;
then y <<01>> z ;
hence b,c are_convergent_wrt the reduction of X by ; :: thesis: verum
end;
assume A3: for a, b, c being object st [a,b] in the reduction of X & [a,c] in the reduction of X holds
b,c are_convergent_wrt the reduction of X ; :: according to REWRITE1:def 24 :: thesis: X is WCR
let x be Element of X; :: according to ABSRED_0:def 27 :: thesis: for y being Element of X st x <<01>> y holds
x >><< y

let y be Element of X; :: thesis: ( x <<01>> y implies x >><< y )
given z being Element of X such that A4: ( x <=01= z & z =01=> y ) ; :: according to ABSRED_0:def 22 :: thesis: x >><< y
per cases ( ( x <== z & z ==> y ) or ( x = z & z = y ) or ( x <== z & z = y ) or ( x = z & z ==> y ) ) by A4;
suppose ( x <== z & z ==> y ) ; :: thesis: x >><< y
hence x >><< y by ; :: thesis: verum
end;
suppose ( x = z & z = y ) ; :: thesis: x >><< y
hence x >><< y ; :: thesis: verum
end;
suppose ( x <== z & z = y ) ; :: thesis: x >><< y
hence x >><< y by Th17a; :: thesis: verum
end;
suppose ( x = z & z ==> y ) ; :: thesis: x >><< y
hence x >><< y by Th17a; :: thesis: verum
end;
end;