let R, Q be with_Church-Rosser_property Relation; :: thesis: ( R commutes_with Q implies R \/ Q is with_Church-Rosser_property )
assume A1: R commutes_with Q ; :: thesis: R \/ Q is with_Church-Rosser_property
R \/ Q is confluent
proof
let a, b be object ; :: according to REWRITE1:def 22 :: thesis: ( a,b are_divergent_wrt R \/ Q implies a,b are_convergent_wrt R \/ Q )
given c being object such that A2: R \/ Q reduces c,a and
A3: R \/ Q reduces c,b ; :: according to REWRITE1:def 8 :: thesis: a,b are_convergent_wrt R \/ Q
consider p being RedSequence of R \/ Q such that
A4: c = p . 1 and
A5: a = p . (len p) by A2;
defpred S1[ Nat] means ( $1 in dom p implies p . $1,b are_convergent_wrt R \/ Q );
now :: thesis: for i being Nat st ( i in dom p implies p . i,b are_convergent_wrt R \/ Q ) & i + 1 in dom p holds
p . (i + 1),b are_convergent_wrt R \/ Q
let i be Nat; :: thesis: ( ( i in dom p implies p . i,b are_convergent_wrt R \/ Q ) & i + 1 in dom p implies p . (b1 + 1),b are_convergent_wrt R \/ Q )
assume that
A6: ( i in dom p implies p . i,b are_convergent_wrt R \/ Q ) and
A7: i + 1 in dom p ; :: thesis: p . (b1 + 1),b are_convergent_wrt R \/ Q
per cases ( i = 0 or i > 0 ) ;
suppose i = 0 ; :: thesis: p . (b1 + 1),b are_convergent_wrt R \/ Q
hence p . (i + 1),b are_convergent_wrt R \/ Q by A3, A4, Th36; :: thesis: verum
end;
suppose A8: i > 0 ; :: thesis: p . (b1 + 1),b are_convergent_wrt R \/ Q
A9: i < len p by A7, Lm2;
then consider d being object such that
A10: R \/ Q reduces p . i,d and
A11: R \/ Q reduces b,d by A6, A8, Lm3;
consider q being RedSequence of R \/ Q such that
A12: p . i = q . 1 and
A13: d = q . (len q) by A10;
defpred S2[ Nat] means ( $1 in dom q implies ex e being object st
( R \/ Q reduces p . (i + 1),e & ( R reduces q . $1,e or Q reduces q . $1,e ) ) );
i in dom p by A8, A9, Lm3;
then [(p . i),(p . (i + 1))] in R \/ Q by A7, Def2;
then A14: ( [(p . i),(p . (i + 1))] in R or [(p . i),(p . (i + 1))] in Q ) by XBOOLE_0:def 3;
now :: thesis: for j being Nat st ( j in dom q implies ex e being object st
( R \/ Q reduces p . (i + 1),e & ( R reduces q . j,e or Q reduces q . j,e ) ) ) & j + 1 in dom q holds
ex e being object st
( R \/ Q reduces p . (i + 1),e & ( R reduces q . (j + 1),e or Q reduces q . (j + 1),e ) )
let j be Nat; :: thesis: ( ( j in dom q implies ex e being object st
( R \/ Q reduces p . (i + 1),e & ( R reduces q . j,e or Q reduces q . j,e ) ) ) & j + 1 in dom q implies ex e being object st
( R \/ Q reduces p . (i + 1),b2 & ( R reduces q . (e + 1),b2 or Q reduces q . (e + 1),b2 ) ) )
assume that
A15: ( j in dom q implies ex e being object st
( R \/ Q reduces p . (i + 1),e & ( R reduces q . j,e or Q reduces q . j,e ) ) ) and
A16: j + 1 in dom q ; :: thesis: ex e being object st
( R \/ Q reduces p . (i + 1),b2 & ( R reduces q . (e + 1),b2 or Q reduces q . (e + 1),b2 ) )
A17: j < len q by A16, Lm2;
per cases ( j = 0 or j > 0 ) ;
suppose A18: j = 0 ; :: thesis: ex e being object st
( R \/ Q reduces p . (i + 1),b2 & ( R reduces q . (e + 1),b2 or Q reduces q . (e + 1),b2 ) )
A19: R \/ Q reduces p . (i + 1),p . (i + 1) by Th12;
( R reduces q . (j + 1),p . (i + 1) or Q reduces q . (j + 1),p . (i + 1) ) by A12, A14, A18, Th15;
hence ex e being object st
( R \/ Q reduces p . (i + 1),e & ( R reduces q . (j + 1),e or Q reduces q . (j + 1),e ) ) by A19; :: thesis: verum
end;
suppose A20: j > 0 ; :: thesis: ex e being object st
( R \/ Q reduces p . (i + 1),b2 & ( R reduces q . (e + 1),b2 or Q reduces q . (e + 1),b2 ) )
then consider e being object such that
A21: R \/ Q reduces p . (i + 1),e and
A22: ( R reduces q . j,e or Q reduces q . j,e ) by A15, A17, Lm3;
A23: now :: thesis: ( R reduces q . j,q . (j + 1) & Q reduces q . j,e implies ex x being object st
( R \/ Q reduces p . (i + 1),x & ( R reduces q . (j + 1),x or Q reduces q . (j + 1),x ) ) )
assume ( R reduces q . j,q . (j + 1) & Q reduces q . j,e ) ; :: thesis: ex x being object st
( R \/ Q reduces p . (i + 1),x & ( R reduces q . (j + 1),x or Q reduces q . (j + 1),x ) )
then consider x being object such that
A24: Q reduces q . (j + 1),x and
A25: R reduces e,x by A1;
take x = x; :: thesis: ( R \/ Q reduces p . (i + 1),x & ( R reduces q . (j + 1),x or Q reduces q . (j + 1),x ) )
R \/ Q reduces e,x by A25, Th22, XBOOLE_1:7;
hence ( R \/ Q reduces p . (i + 1),x & ( R reduces q . (j + 1),x or Q reduces q . (j + 1),x ) ) by A21, A24, Th16; :: thesis: verum
end;
A26: now :: thesis: ( Q reduces q . j,q . (j + 1) & Q reduces q . j,e implies ex x being object st
( R \/ Q reduces p . (i + 1),x & ( R reduces q . (j + 1),x or Q reduces q . (j + 1),x ) ) )
assume ( Q reduces q . j,q . (j + 1) & Q reduces q . j,e ) ; :: thesis: ex x being object st
( R \/ Q reduces p . (i + 1),x & ( R reduces q . (j + 1),x or Q reduces q . (j + 1),x ) )
then e,q . (j + 1) are_divergent_wrt Q ;
then e,q . (j + 1) are_convergent_wrt Q by Def22;
then consider x being object such that
A27: Q reduces e,x and
A28: Q reduces q . (j + 1),x ;
take x = x; :: thesis: ( R \/ Q reduces p . (i + 1),x & ( R reduces q . (j + 1),x or Q reduces q . (j + 1),x ) )
R \/ Q reduces e,x by A27, Th22, XBOOLE_1:7;
hence ( R \/ Q reduces p . (i + 1),x & ( R reduces q . (j + 1),x or Q reduces q . (j + 1),x ) ) by A21, A28, Th16; :: thesis: verum
end;
A29: now :: thesis: ( R reduces q . j,q . (j + 1) & R reduces q . j,e implies ex x being object st
( R \/ Q reduces p . (i + 1),x & ( R reduces q . (j + 1),x or Q reduces q . (j + 1),x ) ) )
assume ( R reduces q . j,q . (j + 1) & R reduces q . j,e ) ; :: thesis: ex x being object st
( R \/ Q reduces p . (i + 1),x & ( R reduces q . (j + 1),x or Q reduces q . (j + 1),x ) )
then e,q . (j + 1) are_divergent_wrt R ;
then e,q . (j + 1) are_convergent_wrt R by Def22;
then consider x being object such that
A30: R reduces e,x and
A31: R reduces q . (j + 1),x ;
take x = x; :: thesis: ( R \/ Q reduces p . (i + 1),x & ( R reduces q . (j + 1),x or Q reduces q . (j + 1),x ) )
R \/ Q reduces e,x by A30, Th22, XBOOLE_1:7;
hence ( R \/ Q reduces p . (i + 1),x & ( R reduces q . (j + 1),x or Q reduces q . (j + 1),x ) ) by A21, A31, Th16; :: thesis: verum
end;
A32: now :: thesis: ( Q reduces q . j,q . (j + 1) & R reduces q . j,e implies ex x being object st
( R \/ Q reduces p . (i + 1),x & ( R reduces q . (j + 1),x or Q reduces q . (j + 1),x ) ) )
assume ( Q reduces q . j,q . (j + 1) & R reduces q . j,e ) ; :: thesis: ex x being object st
( R \/ Q reduces p . (i + 1),x & ( R reduces q . (j + 1),x or Q reduces q . (j + 1),x ) )
then consider x being object such that
A33: R reduces q . (j + 1),x and
A34: Q reduces e,x by A1, Def18;
take x = x; :: thesis: ( R \/ Q reduces p . (i + 1),x & ( R reduces q . (j + 1),x or Q reduces q . (j + 1),x ) )
R \/ Q reduces e,x by A34, Th22, XBOOLE_1:7;
hence ( R \/ Q reduces p . (i + 1),x & ( R reduces q . (j + 1),x or Q reduces q . (j + 1),x ) ) by A21, A33, Th16; :: thesis: verum
end;
j in dom q by A17, A20, Lm3;
then [(q . j),(q . (j + 1))] in R \/ Q by A16, Def2;
then ( [(q . j),(q . (j + 1))] in R or [(q . j),(q . (j + 1))] in Q ) by XBOOLE_0:def 3;
hence ex e being object st
( R \/ Q reduces p . (i + 1),e & ( R reduces q . (j + 1),e or Q reduces q . (j + 1),e ) ) by A22, A29, A26, A23, A32, Th15; :: thesis: verum
end;
end;
end;
then A35: for k being Nat st S2[k] holds
S2[k + 1] ;
A36: S2[ 0 ] by Lm1;
A37: for j being Nat holds S2[j] from NAT_1:sch 2(A36, A35);
thus p . (i + 1),b are_convergent_wrt R \/ Q :: thesis: verum
proof
len q in dom q by FINSEQ_5:6;
then consider e being object such that
A38: R \/ Q reduces p . (i + 1),e and
A39: ( R reduces d,e or Q reduces d,e ) by A13, A37;
take e ; :: according to REWRITE1:def 7 :: thesis: ( R \/ Q reduces p . (i + 1),e & R \/ Q reduces b,e )
R \/ Q reduces d,e by A39, Th22, XBOOLE_1:7;
hence ( R \/ Q reduces p . (i + 1),e & R \/ Q reduces b,e ) by A11, A38, Th16; :: thesis: verum
end;
end;
end;
end;
then A40: for k being Nat st S1[k] holds
S1[k + 1] ;
A41: len p in dom p by FINSEQ_5:6;
A42: S1[ 0 ] by Lm1;
for i being Nat holds S1[i] from NAT_1:sch 2(A42, A40);
 hence a,b are_convergent_wrt R \/ Q by A5, A41; :: thesis: verum
end;
hence R \/ Q is with_Church-Rosser_property ; :: thesis: verum