let R be Relation; :: thesis: ( R is locally-confluent iff R commutes-weakly_with R )

hereby :: thesis: ( R commutes-weakly_with R implies R is locally-confluent )

assume A1: R is locally-confluent ; :: thesis: R commutes-weakly_with R
thus R commutes-weakly_with R :: thesis: verum

proof

let a, b, c be set ; :: according to REWRITE1:def 17 :: thesis: ( [a,b] in R & [a,c] in R implies ex d being set st
( R reduces b,d & R reduces c,d ) )
assume ( [a,b] in R & [a,c] in R ) ; :: thesis: ex d being set st
( R reduces b,d & R reduces c,d )
then b,c are_convergent_wrt R by A1, Def24;
hence ex d being set st
( R reduces b,d & R reduces c,d ) by Def7; :: thesis: verum

end;

end;

assume A2: for a, b, c being set st [a,b] in R & [a,c] in R holds
ex d being set st
( R reduces b,d & R reduces c,d ) ; :: according to REWRITE1:def 17 :: thesis: R is locally-confluent
let a, b, c be set ; :: according to REWRITE1:def 24 :: thesis: ( [a,b] in R & [a,c] in R implies b,c are_convergent_wrt R )
assume ( [a,b] in R & [a,c] in R ) ; :: thesis: b,c are_convergent_wrt R
hence ex d being set st
( R reduces b,d & R reduces c,d ) by A2; :: according to REWRITE1:def 7 :: thesis: verum