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 )
proof
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;
per cases ( ( a in field the reduction of X & b in field the reduction of X ) or a = b ) by ;
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 ;
hence a,b are_convergent_wrt the reduction of X by ; :: thesis: verum
end;
end;
end;
assume A5: for a, b being object st a,b are_divergent_wrt the reduction of X holds
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 ; :: thesis: verum