let R be Relation; :: thesis: ( R is confluent iff R [*] is locally-confluent )
hereby :: thesis: ( R [*] is locally-confluent implies R is confluent )
assume A1: R is confluent ; :: thesis: R [*] is locally-confluent
thus R [*] is locally-confluent :: thesis: verum
proof
let a, b, c be object ; :: 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 [*]
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 7 :: thesis: ( R [*] reduces b,d & R [*] reduces c,d )
thus ( R [*] reduces b,d & R [*] reduces c,d ) by A2, Th21; :: 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_wrt R [*] ; :: according to REWRITE1:def 24 :: 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_wrt R [*] or R [*] reduces a,b or R [*] reduces b,a ) by A3, A6, Th15, Th38;
then a,b are_convergent_wrt R [*] by Th36;
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