let R be Relation; :: thesis: ( R is confluent iff R commutes_with R )

hereby :: thesis: ( R commutes_with R implies R is confluent )

assume A1: R is confluent ; :: thesis: R commutes_with R
thus R commutes_with R :: thesis: verum

proof

let a, b, c be object ; :: according to REWRITE1:def 18 :: thesis: ( R reduces a,b & R reduces a,c implies ex d being object st
( R reduces b,d & R reduces c,d ) )
assume ( R reduces a,b & R reduces a,c ) ; :: thesis: ex d being object st
( R reduces b,d & R reduces c,d )
then b,c are_divergent_wrt R ;
then b,c are_convergent_wrt R by A1;
hence ex d being object st
( R reduces b,d & R reduces c,d ) ; :: thesis: verum

end;

end;

assume A2: for a, b, c being object st R reduces a,b & R reduces a,c holds
ex d being object st
( R reduces b,d & R reduces c,d ) ; :: according to REWRITE1:def 18 :: thesis: R is confluent
let a, b be object ; :: according to REWRITE1:def 22 :: thesis: ( a,b are_divergent_wrt R implies a,b are_convergent_wrt R )
assume ex c being object st
( R reduces c,a & R reduces c,b ) ; :: according to REWRITE1:def 8 :: thesis: a,b are_convergent_wrt R
hence ex d being object st
( R reduces a,d & R reduces b,d ) by A2; :: according to REWRITE1:def 7 :: thesis: verum