let R be Relation; ( R is strongly-normalizing & R is locally-confluent implies R is confluent )
assume A1:
R is strongly-normalizing
; ( not R is locally-confluent or R is confluent )
defpred S1[ object ] means for b, c being object st R reduces c1,b & R reduces c1,c holds
b,c are_convergent_wrt R;
assume A2:
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
A3:
for a being object st ( for b being object st [a,b] in R & a <> b holds
S1[b] ) holds
S1[a]
proof
let a be
object ;
( ( for b being object st [a,b] in R & a <> b holds
S1[b] ) implies S1[a] )
assume A4:
for
b being
object st
[a,b] in R &
a <> b holds
S1[
b]
;
S1[a]
let b,
c be
object ;
( R reduces a,b & R reduces a,c implies b,c are_convergent_wrt R )
assume that A5:
R reduces a,
b
and A6:
R reduces a,
c
;
b,c are_convergent_wrt R
consider p being
RedSequence of
R such that A7:
a = p . 1
and A8:
b = p . (len p)
by A5;
A9:
len p >= 0 + 1
by NAT_1:13;
consider q being
RedSequence of
R such that A10:
a = q . 1
and A11:
c = q . (len q)
by A6;
A12:
len q >= 0 + 1
by NAT_1:13;
per cases
( len p = 1 or len q = 1 or ( len p <> 1 & len q <> 1 ) )
;
suppose A13:
(
len p <> 1 &
len q <> 1 )
;
b,c are_convergent_wrt Rthen
len q > 1
by A12, XXREAL_0:1;
then A14:
1
+ 1
<= len q
by NAT_1:13;
then A15:
1
+ 1
in dom q
by Lm3;
len q in dom q
by FINSEQ_5:6;
then A16:
R reduces q . 2,
c
by A11, A14, A15, Th17;
len p > 1
by A9, A13, XXREAL_0:1;
then A17:
1
+ 1
<= len p
by NAT_1:13;
then A18:
1
+ 1
in dom p
by Lm3;
len p in dom p
by FINSEQ_5:6;
then A19:
R reduces p . 2,
b
by A8, A17, A18, Th17;
1
in dom p
by A9, Lm3;
then A20:
[a,(p . 2)] in R
by A7, A18, Def2;
then A21:
a in field R
by RELAT_1:15;
1
in dom q
by A12, Lm3;
then A22:
[a,(q . 2)] in R
by A10, A15, Def2;
then
p . 2,
q . 2
are_convergent_wrt R
by A2, A20;
then consider d being
object such that A23:
R reduces p . 2,
d
and A24:
R reduces q . 2,
d
;
A25:
R is_irreflexive_in field R
by A1, RELAT_2:def 10;
then A26:
a <> q . 2
by A22, A21;
a <> p . 2
by A20, A21, A25;
then
b,
d are_convergent_wrt R
by A4, A20, A23, A19;
then consider e being
object such that A27:
R reduces b,
e
and A28:
R reduces d,
e
;
R reduces q . 2,
e
by A24, A28, Th16;
then
e,
c are_convergent_wrt R
by A4, A22, A26, A16;
hence
b,
c are_convergent_wrt R
by A27, Th42;
verum end;
end;
A29:
R is co-well_founded
by A1;
A30:
for a being object st a in field R holds
S1[a]
from REWRITE1:sch 2(A29, A3);
given a0, b0 being object such that A31:
a0,b0 are_divergent_wrt R
and
A32:
not a0,b0 are_convergent_wrt R
; REWRITE1:def 22 contradiction
consider c0 being object such that
A33:
( R reduces c0,a0 & R reduces c0,b0 )
by A31;
( a0 <> c0 or b0 <> c0 )
by A32, Th38;
then
c0 in field R
by A33, Th18;
hence
contradiction
by A32, A33, A30; verum