let X be ARS ; :: thesis: ( X is CONF iff the reduction of X is 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 CONF implies the reduction of X is confluent ) :: thesis: ( the reduction of X is confluent implies X is CONF )

a,b are_convergent_wrt the reduction of X ; :: according to REWRITE1:def 22 :: thesis: X is CONF

let x be Element of X; :: according to ABSRED_0:def 25 :: 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

then x,y are_divergent_wrt the reduction of X by Ch11;

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 CONF implies the reduction of X is confluent ) :: thesis: ( the reduction of X is confluent implies X is CONF )

proof

assume A5:
for a, b being object st a,b are_divergent_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 25 :: thesis: the reduction of X is confluent

let a, b be object ; :: according to REWRITE1:def 22 :: thesis: ( not a,b are_divergent_wrt the reduction of X or a,b are_convergent_wrt the reduction of X )

assume A2: a,b are_divergent_wrt the reduction of X ; :: thesis: a,b are_convergent_wrt the reduction of X

then A3: a,b are_convertible_wrt the reduction of X by REWRITE1:37;

end;x >><< y ; :: according to ABSRED_0:def 25 :: thesis: the reduction of X is confluent

let a, b be object ; :: according to REWRITE1:def 22 :: thesis: ( not a,b are_divergent_wrt the reduction of X or a,b are_convergent_wrt the reduction of X )

assume A2: a,b are_divergent_wrt the reduction of X ; :: thesis: a,b are_convergent_wrt the reduction of X

then A3: a,b are_convertible_wrt the reduction of X by REWRITE1:37;

per cases
( ( a in field the reduction of X & b in field the reduction of X ) or a = b )
by A3, 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, Ch11;

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

end;x <<>> y by A2, Ch11;

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 22 :: thesis: X is CONF

let x be Element of X; :: according to ABSRED_0:def 25 :: 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

then x,y are_divergent_wrt the reduction of X by Ch11;

hence x >><< y by A5, Ch12; :: thesis: verum