let R be Relation; :: thesis: ( R is confluent iff R [*] is subcommutative )

hereby :: thesis: ( R [*] is subcommutative implies R is confluent )

assume A1: R is confluent ; :: thesis: R [*] is subcommutative
thus R [*] is subcommutative :: thesis: verum

proof

let a, b, c be set ; :: according to REWRITE1:def 21 :: thesis: ( [a,b] in R [*] & [a,c] in R [*] implies b,c are_convergent<=1_wrt R [*] )
assume ( [a,b] in R [*] & [a,c] in R [*] ) ; :: thesis: b,c are_convergent<=1_wrt R [*]
then ( R reduces a,b & R reduces a,c ) by Th21;
then b,c are_divergent_wrt R by Def8;
then b,c are_convergent_wrt R by A1, Def22;
then consider d being set such that
A2: ( R reduces b,d & R reduces c,d ) by Def7;
take d ; :: according to REWRITE1:def 9 :: thesis: ( ( [b,d] in R [*] or b = d ) & ( [c,d] in R [*] or c = d ) )
thus ( ( [b,d] in R [*] or b = d ) & ( [c,d] in R [*] or c = d ) ) by A2, Th21; :: thesis: verum

end;

end;

assume A3: for a, b, c being set st [a,b] in R [*] & [a,c] in R [*] holds
b,c are_convergent<=1_wrt R [*] ; :: according to REWRITE1:def 21 :: thesis: R is confluent
let a, b be set ; :: according to REWRITE1:def 22 :: thesis: ( a,b are_divergent_wrt R implies a,b are_convergent_wrt R )
given c being set such that A4: ( R reduces c,a & R reduces c,b ) ; :: according to REWRITE1:def 8 :: thesis: a,b are_convergent_wrt R
( ( [c,a] in R [*] or c = a ) & ( [c,b] in R [*] or c = b ) ) by A4, Th21;
then a,b are_convergent<=1_wrt R [*] by A3, Def9;
then a,b are_convergent_wrt R [*] by Th45;
then consider d being set such that
A5: ( R [*] reduces a,d & R [*] reduces b,d ) by Def7;
take d ; :: according to REWRITE1:def 7 :: thesis: ( R reduces a,d & R reduces b,d )
thus ( R reduces a,d & R reduces b,d ) by A5, Th22; :: thesis: verum