let R, Q be with_Church-Rosser_property Relation; ( R commutes_with Q implies R \/ Q is with_Church-Rosser_property )
assume A1:
R commutes_with Q
; R \/ Q is with_Church-Rosser_property
R \/ Q is confluent
proof
let a,
b be
object ;
REWRITE1:def 22 ( 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
;
REWRITE1:def 8 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 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 \/ Qlet i be
Nat;
( ( 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
;
p . (b1 + 1),b are_convergent_wrt R \/ Qper cases
( i = 0 or i > 0 )
;
suppose A8:
i > 0
;
p . (b1 + 1),b are_convergent_wrt R \/ QA9:
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 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;
( ( 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
;
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 A20:
j > 0
;
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 ( 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 )
;
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;
( 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;
verum end; A26:
now ( 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 )
;
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;
( 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;
verum end; A29:
now ( 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 )
;
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;
( 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;
verum end; A32:
now ( 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 )
;
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;
( 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;
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;
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
verumproof
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
;
REWRITE1:def 7 ( 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;
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;
verum
end;
hence
R \/ Q is with_Church-Rosser_property
; verum