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 )

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

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 A3:
for a, b, c being object st [a,b] in the reduction of X & [a,c] in the reduction of X holds
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 A1, Ch12; :: thesis: verum

end;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 A1, Ch12; :: thesis: verum

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