let R be Relation; ( R is locally-confluent iff R commutes-weakly_with R )
hereby ( R commutes-weakly_with R implies R is locally-confluent )
assume A1:
R is
locally-confluent
;
R commutes-weakly_with Rthus
R commutes-weakly_with R
verumproof
let a,
b,
c be
object ;
REWRITE1:def 17 ( [a,b] in R & [a,c] in R implies ex d being object st
( R reduces b,d & R reduces c,d ) )
assume
(
[a,b] in R &
[a,c] in R )
;
ex d being object st
( R reduces b,d & R reduces c,d )
then
b,
c are_convergent_wrt R
by A1;
hence
ex
d being
object st
(
R reduces b,
d &
R reduces c,
d )
;
verum
end;
end;
assume A2:
for a, b, c being object st [a,b] in R & [a,c] in R holds
ex d being object st
( R reduces b,d & R reduces c,d )
; REWRITE1:def 17 R is locally-confluent
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
hence
ex d being object st
( R reduces b,d & R reduces c,d )
by A2; REWRITE1:def 7 verum