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 object ; :: 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 Th20;
then b,c are_divergent_wrt R ;
then b,c are_convergent_wrt R by A1;
then consider d being object such that
A2: ( R reduces b,d & R reduces c,d ) ;
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, Th20; :: thesis: verum

end;

end;

assume A3: for a, b, c being object 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 object ; :: according to REWRITE1:def 22 :: thesis: ( a,b are_divergent_wrt R implies a,b are_convergent_wrt R )
given c being object such that A4: R reduces c,a and
A5: R reduces c,b ; :: according to REWRITE1:def 8 :: thesis: a,b are_convergent_wrt R
A6: ( [c,b] in R [*] or c = b ) by A5, Th20;
( [c,a] in R [*] or c = a ) by A4, Th20;
then a,b are_convergent<=1_wrt R [*] by A3, A6;
then a,b are_convergent_wrt R [*] by Th44;
then consider d being object such that
A7: ( R [*] reduces a,d & R [*] reduces b,d ) ;
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 A7, Th21; :: thesis: verum