let R be Relation; ( R is confluent iff R [*] is locally-confluent )
hereby ( R [*] is locally-confluent implies R is confluent )
assume A1:
R is
confluent
;
R [*] is locally-confluent thus
R [*] is
locally-confluent
verumproof
let a,
b,
c be
object ;
REWRITE1:def 24 ( [a,b] in R [*] & [a,c] in R [*] implies b,c are_convergent_wrt R [*] )
assume
(
[a,b] in R [*] &
[a,c] in R [*] )
;
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
;
REWRITE1:def 7 ( R [*] reduces b,d & R [*] reduces c,d )
thus
(
R [*] reduces b,
d &
R [*] reduces c,
d )
by A2, Th21;
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 [*]
; REWRITE1:def 24 R is confluent
let a, b be object ; REWRITE1:def 22 ( 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
; REWRITE1:def 8 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
; REWRITE1:def 7 ( R reduces a,d & R reduces b,d )
thus
( R reduces a,d & R reduces b,d )
by A7, Th21; verum