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 set ; :: according to REWRITE1:def 22 :: thesis: ( a,b are_divergent_wrt R \/ Q implies a,b are_convergent_wrt R \/ Q )
given c being set such that A2: ( R \/ Q reduces c,a & 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
A3: ( c = p . 1 & a = p . (len p) ) by A2, Def3;
defpred S₁[ Element of NAT ] means ( $1 in dom p implies p . $1,b are_convergent_wrt R \/ Q );
A4: S₁[ 0 ] by Lm1;

now

let i be Element of NAT ; :: thesis: ( ( i in dom p implies p . i,b are_convergent_wrt R \/ Q ) & i + 1 in dom p implies p . (b₁ + 1),b are_convergent_wrt R \/ Q )
assume that
A5: ( i in dom p implies p . i,b are_convergent_wrt R \/ Q ) and
A6: i + 1 in dom p ; :: thesis: p . (b₁ + 1),b are_convergent_wrt R \/ Q

per cases ( i = 0 or i > 0 ) ;

suppose i = 0 ; :: thesis: p . (b₁ + 1),b are_convergent_wrt R \/ Q

hence p . (i + 1),b are_convergent_wrt R \/ Q by A2, A3, Th37; :: thesis: verum

end;

suppose i > 0 ; :: thesis: p . (b₁ + 1),b are_convergent_wrt R \/ Q

then A7: ( i >= 0 + 1 & i < len p ) by A6, Lm2, NAT_1:13;
then A8: i in dom p by Lm3;
consider d being set such that
A9: ( R \/ Q reduces p . i,d & R \/ Q reduces b,d ) by A5, A7, Def7, Lm3;
consider q being RedSequence of R \/ Q such that
A10: ( p . i = q . 1 & d = q . (len q) ) by A9, Def3;
[(p . i),(p . (i + 1))] in R \/ Q by A6, A8, Def2;
then A11: ( [(p . i),(p . (i + 1))] in R or [(p . i),(p . (i + 1))] in Q ) by XBOOLE_0:def 3;
defpred S₂[ Element of NAT ] means ( $1 in dom q implies ex e being set st
( R \/ Q reduces p . (i + 1),e & ( R reduces q . $1,e or Q reduces q . $1,e ) ) );
A12: S₂[ 0 ] by Lm1;

now

let j be Element of NAT ; :: thesis: ( ( j in dom q implies ex e being set 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 set st
( R \/ Q reduces p . (i + 1),b₂ & ( R reduces q . (e + 1),b₂ or Q reduces q . (e + 1),b₂ ) ) )
assume that
A13: ( j in dom q implies ex e being set st
( R \/ Q reduces p . (i + 1),e & ( R reduces q . j,e or Q reduces q . j,e ) ) ) and
A14: j + 1 in dom q ; :: thesis: ex e being set st
( R \/ Q reduces p . (i + 1),b₂ & ( R reduces q . (e + 1),b₂ or Q reduces q . (e + 1),b₂ ) )
A15: j < len q by A14, Lm2;

per cases ( j = 0 or j > 0 ) ;

suppose j = 0 ; :: thesis: ex e being set st
( R \/ Q reduces p . (i + 1),b₂ & ( R reduces q . (e + 1),b₂ or Q reduces q . (e + 1),b₂ ) )

then ( R \/ Q reduces p . (i + 1),p . (i + 1) & ( R reduces q . (j + 1),p . (i + 1) or Q reduces q . (j + 1),p . (i + 1) ) ) by A10, A11, Th13, Th16;
hence ex e being set st
( R \/ Q reduces p . (i + 1),e & ( R reduces q . (j + 1),e or Q reduces q . (j + 1),e ) ) ; :: thesis: verum

end;

suppose A16: j > 0 ; :: thesis: ex e being set st
( R \/ Q reduces p . (i + 1),b₂ & ( R reduces q . (e + 1),b₂ or Q reduces q . (e + 1),b₂ ) )

then j in dom q by A15, Lm3;
then [(q . j),(q . (j + 1))] in R \/ Q by A14, Def2;
then A17: ( [(q . j),(q . (j + 1))] in R or [(q . j),(q . (j + 1))] in Q ) by XBOOLE_0:def 3;
consider e being set such that
A18: ( R \/ Q reduces p . (i + 1),e & ( R reduces q . j,e or Q reduces q . j,e ) ) by A13, A15, A16, Lm3;

A19: now

assume ( R reduces q . j,q . (j + 1) & R reduces q . j,e ) ; :: thesis: ex x being set 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 by Def8;
then e,q . (j + 1) are_convergent_wrt R by Def22;
then consider x being set such that
A20: ( R reduces e,x & R reduces q . (j + 1),x ) by Def7;
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 A20, Th23, 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 A18, A20, Th17; :: thesis: verum

end;

A21: now

assume ( Q reduces q . j,q . (j + 1) & Q reduces q . j,e ) ; :: thesis: ex x being set 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 by Def8;
then e,q . (j + 1) are_convergent_wrt Q by Def22;
then consider x being set such that
A22: ( Q reduces e,x & Q reduces q . (j + 1),x ) by Def7;
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 A22, Th23, 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 A18, A22, Th17; :: thesis: verum

end;

A23: now

assume ( R reduces q . j,q . (j + 1) & Q reduces q . j,e ) ; :: thesis: ex x being set 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 set such that
A24: ( Q reduces q . (j + 1),x & R 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 A24, Th23, 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 A18, A24, Th17; :: thesis: verum

end;

now

assume ( Q reduces q . j,q . (j + 1) & R reduces q . j,e ) ; :: thesis: ex x being set 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 set such that
A25: ( R reduces q . (j + 1),x & 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 A25, Th23, 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 A18, A25, Th17; :: thesis: verum

end;

hence ex e being set st
( R \/ Q reduces p . (i + 1),e & ( R reduces q . (j + 1),e or Q reduces q . (j + 1),e ) ) by A17, A18, A19, A21, A23, Th16; :: thesis: verum

end;

end;

end;

then A26: for k being Element of NAT st S₂[k] holds
S₂[k + 1] ;
A27: for j being Element of NAT holds S₂[j] from NAT_1:sch 1(A12, A26);
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 set such that
A28: ( R \/ Q reduces p . (i + 1),e & ( R reduces d,e or Q reduces d,e ) ) by A10, A27;
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 A28, Th23, XBOOLE_1:7;
hence ( R \/ Q reduces p . (i + 1),e & R \/ Q reduces b,e ) by A9, A28, Th17; :: thesis: verum

end;

end;

end;

end;

then A29: for k being Element of NAT st S₁[k] holds
S₁[k + 1] ;
A30: for i being Element of NAT holds S₁[i] from NAT_1:sch 1(A4, A29);
len p in dom p by FINSEQ_5:6;
hence a,b are_convergent_wrt R \/ Q by A3, A30; :: thesis: verum

end;

then R \/ Q is confluent Relation ;
hence R \/ Q is with_Church-Rosser_property ; :: thesis: verum