let R be Relation; :: thesis: ( R is confluent iff for a, b, c being object st R reduces a,b & [a,c] in R holds
b,c are_convergent_wrt R )
hereby :: thesis: ( ( for a, b, c being object st R reduces a,b & [a,c] in R holds
b,c are_convergent_wrt R ) implies R is confluent )
assume A1: R is confluent ; :: thesis: for a, b, c being object st R reduces a,b & [a,c] in R holds
b,c are_convergent_wrt R
let a, b, c be object ; :: thesis: ( R reduces a,b & [a,c] in R implies b,c are_convergent_wrt R )
assume that
A2: R reduces a,b and
A3: [a,c] in R ; :: thesis: b,c are_convergent_wrt R
R reduces a,c by A3, Th15;
then b,c are_divergent_wrt R by A2;
hence b,c are_convergent_wrt R by A1; :: thesis: verum
end;
assume A4: for a, b, c being object st R reduces a,b & [a,c] in R holds
b,c are_convergent_wrt R ; :: thesis: R is confluent
let b, c be object ; :: according to REWRITE1:def 22 :: thesis: ( b,c are_divergent_wrt R implies b,c are_convergent_wrt R )
given a being object such that A5: R reduces a,b and
A6: R reduces a,c ; :: according to REWRITE1:def 8 :: thesis: b,c are_convergent_wrt R
consider p being RedSequence of R such that
A7: p . 1 = a and
A8: p . (len p) = b by A5;
consider q being RedSequence of R such that
A9: q . 1 = a and
A10: q . (len q) = c by A6;
defpred S1[ Nat, Nat] means p . $1,q . $2 are_convergent_wrt R;
defpred S2[ Nat] means ( $1 in dom p implies for j being Nat st j in dom q holds
S1[$1,j] );
A11: for i being Nat st S2[i] holds
S2[i + 1]
proof
let i be Nat; :: thesis: ( S2[i] implies S2[i + 1] )
assume that
( i in dom p implies for j being Nat st j in dom q holds
S1[i,j] ) and
A12: i + 1 in dom p ; :: thesis: for j being Nat st j in dom q holds
S1[i + 1,j]
defpred S3[ Nat] means ( $1 in dom q implies S1[i + 1,$1] );
A13: for j being Nat st S3[j] holds
S3[j + 1]
proof
1 in dom p by FINSEQ_5:6;
then A14: R reduces a,p . (i + 1) by A7, A12, Th17, NAT_1:11;
let j be Nat; :: thesis: ( S3[j] implies S3[j + 1] )
assume that
A15: ( j in dom q implies S1[i + 1,j] ) and
A16: j + 1 in dom q ; :: thesis: S1[i + 1,j + 1]
per cases ( j = 0 or j > 0 ) ;
suppose j = 0 ; :: thesis: S1[i + 1,j + 1]
hence S1[i + 1,j + 1] by A9, A14, Th36; :: thesis: verum
end;
suppose A17: j > 0 ; :: thesis: S1[i + 1,j + 1]
A18: j < len q by A16, Lm2;
then consider d being object such that
A19: R reduces p . (i + 1),d and
A20: R reduces q . j,d by A15, A17, Def7, Lm3;
j in dom q by A17, A18, Lm3;
then [(q . j),(q . (j + 1))] in R by A16, Def2;
then d,q . (j + 1) are_convergent_wrt R by A4, A20;
hence S1[i + 1,j + 1] by A19, Th42; :: thesis: verum
end;
end;
end;
A21: S3[ 0 ] by Lm1;
thus for j being Nat holds S3[j] from NAT_1:sch 2(A21, A13); :: thesis: verum
end;
A22: ( len p in dom p & len q in dom q ) by FINSEQ_5:6;
A23: S2[ 0 ] by Lm1;
for i being Nat holds S2[i] from NAT_1:sch 2(A23, A11);
 hence b,c are_convergent_wrt R by A8, A10, A22; :: thesis: verum