let R be Relation; ( R is confluent implies ( R is locally-confluent & R is with_Church-Rosser_property ) )
assume A2:
for a, b being object st a,b are_divergent_wrt R holds
a,b are_convergent_wrt R
; REWRITE1:def 22 ( R is locally-confluent & R is with_Church-Rosser_property )
hereby REWRITE1:def 24 R is with_Church-Rosser_property
let a,
b,
c be
object ;
( [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 Rthen
(
R reduces a,
b &
R reduces a,
c )
by Th15;
then
b,
c are_divergent_wrt R
;
hence
b,
c are_convergent_wrt R
by A2;
verum
end;
let a, b be object ; REWRITE1:def 23 ( a,b are_convertible_wrt R implies a,b are_convergent_wrt R )
given p being RedSequence of R \/ (R ~) such that A3:
p . 1 = a
and
A4:
p . (len p) = b
; REWRITE1:def 3,REWRITE1:def 4 a,b are_convergent_wrt R
defpred S1[ Nat] means ( c1 in dom p implies a,p . c1 are_convergent_wrt R );
now for i being Nat st ( i in dom p implies a,p . i are_convergent_wrt R ) & i + 1 in dom p holds
a,p . (i + 1) are_convergent_wrt Rlet i be
Nat;
( ( i in dom p implies a,p . i are_convergent_wrt R ) & i + 1 in dom p implies a,p . (b1 + 1) are_convergent_wrt R )assume that A5:
(
i in dom p implies
a,
p . i are_convergent_wrt R )
and A6:
i + 1
in dom p
;
a,p . (b1 + 1) are_convergent_wrt Rper cases
( i in dom p or not i in dom p )
;
suppose A7:
i in dom p
;
a,p . (b1 + 1) are_convergent_wrt Rthen consider c being
object such that A8:
R reduces a,
c
and A9:
R reduces p . i,
c
by A5;
[(p . i),(p . (i + 1))] in R \/ (R ~)
by A6, A7, Def2;
then
(
[(p . i),(p . (i + 1))] in R or
[(p . i),(p . (i + 1))] in R ~ )
by XBOOLE_0:def 3;
then
(
[(p . i),(p . (i + 1))] in R or
[(p . (i + 1)),(p . i)] in R )
by RELAT_1:def 7;
then
(
R reduces p . i,
p . (i + 1) or
R reduces p . (i + 1),
p . i )
by Th15;
then
(
c,
p . (i + 1) are_divergent_wrt R or
R reduces p . (i + 1),
c )
by A9, Th16;
then
(
c,
p . (i + 1) are_convergent_wrt R or
a,
p . (i + 1) are_convergent_wrt R )
by A2, A8;
hence
a,
p . (i + 1) are_convergent_wrt R
by A8, Th42;
verum end; end; end;
then A10:
for k being Nat st S1[k] holds
S1[k + 1]
;
A11:
len p in dom p
by FINSEQ_5:6;
A12:
S1[ 0 ]
by Lm1;
for i being Nat holds S1[i]
from NAT_1:sch 2(A12, A10);
hence
a,b are_convergent_wrt R
by A4, A11; verum