let P be set ; for N being Petri_net of P
for R1, R2, R3 being process of N holds (R1 concur R2) concur R3 = R1 concur (R2 concur R3)
let N be Petri_net of P; for R1, R2, R3 being process of N holds (R1 concur R2) concur R3 = R1 concur (R2 concur R3)
let R1, R2, R3 be process of N; (R1 concur R2) concur R3 = R1 concur (R2 concur R3)
thus
(R1 concur R2) concur R3 c= R1 concur (R2 concur R3)
XBOOLE_0:def 10 R1 concur (R2 concur R3) c= (R1 concur R2) concur R3proof
let x be
set ;
TARSKI:def 3 ( not x in (R1 concur R2) concur R3 or x in R1 concur (R2 concur R3) )
assume
x in (R1 concur R2) concur R3
;
x in R1 concur (R2 concur R3)
then consider C1 being
firing-sequence of
N such that A1:
x = C1
and A2:
ex
q1,
q2 being
FinSubsequence st
(
C1 = q1 \/ q2 &
q1 misses q2 &
Seq q1 in R1 concur R2 &
Seq q2 in R3 )
;
consider q1,
q2 being
FinSubsequence such that A3:
C1 = q1 \/ q2
and A4:
q1 misses q2
and A5:
Seq q1 in R1 concur R2
and A6:
Seq q2 in R3
by A2;
consider C2 being
firing-sequence of
N such that A7:
Seq q1 = C2
and A8:
ex
q3,
q4 being
FinSubsequence st
(
C2 = q3 \/ q4 &
q3 misses q4 &
Seq q3 in R1 &
Seq q4 in R2 )
by A5;
consider q3,
q4 being
FinSubsequence such that A9:
C2 = q3 \/ q4
and A10:
q3 misses q4
and A11:
Seq q3 in R1
and A12:
Seq q4 in R2
by A8;
consider n1 being
Nat such that A13:
dom q1 c= Seg n1
by FINSEQ_1:def 12;
A14:
q3 c= Seq q1
by A7, A9, XBOOLE_1:7;
A15:
q4 c= Seq q1
by A7, A9, XBOOLE_1:7;
Sgm (dom q1) is
one-to-one
by A13, FINSEQ_3:99;
then A16:
(Sgm (dom q1)) .: (dom q3) misses (Sgm (dom q1)) .: (dom q4)
by A10, A14, A15, Th10, FUNCT_1:125;
A17:
rng ((Sgm (dom q1)) | (dom q3)) = (Sgm (dom q1)) .: (dom q3)
by RELAT_1:148;
A18:
rng ((Sgm (dom q1)) | (dom q4)) = (Sgm (dom q1)) .: (dom q4)
by RELAT_1:148;
then A19:
q1 | (rng ((Sgm (dom q1)) | (dom q3))) misses q1 | (rng ((Sgm (dom q1)) | (dom q4)))
by A16, A17, Th9;
A20:
dom (Sgm (dom q1)) =
dom (q3 \/ q4)
by A7, A9, Lm4
.=
(dom q3) \/ (dom q4)
by RELAT_1:13
;
A21:
(q1 | (rng ((Sgm (dom q1)) | (dom q3)))) \/ (q1 | (rng ((Sgm (dom q1)) | (dom q4)))) =
q1 | ((rng ((Sgm (dom q1)) | (dom q3))) \/ (rng ((Sgm (dom q1)) | (dom q4))))
by RELAT_1:107
.=
q1 | ((Sgm (dom q1)) .: ((dom q3) \/ (dom q4)))
by A17, A18, RELAT_1:153
.=
q1 | (rng ((Sgm (dom q1)) | (dom (Sgm (dom q1)))))
by A20, RELAT_1:148
.=
q1 | (rng (Sgm (dom q1)))
by RELAT_1:98
.=
q1 | (dom q1)
by FINSEQ_1:71
.=
q1
by RELAT_1:98
;
A32:
q1 c= C1
by A3, XBOOLE_1:7;
A33:
q1 | (rng ((Sgm (dom q1)) | (dom q3))) c= q1
by A21, XBOOLE_1:7;
A34:
q1 | (rng ((Sgm (dom q1)) | (dom q4))) c= q1
by A21, XBOOLE_1:7;
rng C1 = (rng q1) \/ (rng q2)
by A3, RELAT_1:26;
then A35:
rng q1 c= rng C1
by XBOOLE_1:7;
A36:
rng q1 = rng (Seq q1)
by Lm5;
A37:
rng (Seq q1) c= rng C1
by A35, Lm5;
A38:
rng (Seq q1) = (rng q3) \/ (rng q4)
by A7, A9, RELAT_1:26;
then A39:
rng q3 c= rng (Seq q1)
by XBOOLE_1:7;
rng q3 = rng (Seq q3)
by Lm5;
then A40:
rng (Seq q3) c= rng C1
by A37, A39, XBOOLE_1:1;
A41:
rng q4 c= rng (Seq q1)
by A38, XBOOLE_1:7;
rng q4 = rng (Seq q4)
by Lm5;
then A42:
rng (Seq q4) c= rng C1
by A37, A41, XBOOLE_1:1;
reconsider q5 =
q1 | (rng ((Sgm (dom q1)) | (dom q3))),
q6 =
q1 | (rng ((Sgm (dom q1)) | (dom q4))) as
FinSubsequence ;
reconsider fs =
C1 as
FinSequence of
rng C1 by FINSEQ_1:def 4;
reconsider fs1 =
Seq q1 as
FinSequence of
rng C1 by A35, A36, FINSEQ_1:def 4;
reconsider fs2 =
Seq q3 as
FinSequence of
rng C1 by A40, FINSEQ_1:def 4;
reconsider fs3 =
Seq q4 as
FinSequence of
rng C1 by A42, FINSEQ_1:def 4;
reconsider fss =
q1,
fss1 =
q5,
fss2 =
q6 as
Subset of
fs by A32, A33, A34, XBOOLE_1:1;
reconsider fss3 =
q3,
fss4 =
q4 as
Subset of
fs1 by A7, A9, XBOOLE_1:7;
A43:
Seq fss3 = fs2
;
fss1 = fss | (rng ((Sgm (dom fss)) | (dom fss3)))
;
then A44:
Seq q3 = Seq q5
by A43, GRAPH_2:30;
A45:
Seq fss4 = fs3
;
A46:
fss2 = fss | (rng ((Sgm (dom fss)) | (dom fss4)))
;
q1 /\ q2 = {}
by A4, XBOOLE_0:def 7;
then A47:
(q5 /\ q2) \/ (q6 /\ q2) = {}
by A21, XBOOLE_1:23;
then A48:
q5 /\ q2 = {}
;
q6 /\ q2 = {}
by A47;
then A49:
q6 misses q2
by XBOOLE_0:def 7;
A50:
q1 c= C1
by A3, XBOOLE_1:7;
A51:
q2 c= C1
by A3, XBOOLE_1:7;
q6 c= q1
by A21, XBOOLE_1:7;
then
q6 c= C1
by A50, XBOOLE_1:1;
then A52:
dom q6 misses dom q2
by A49, A51, Th10;
then reconsider q7 =
q6 \/ q2 as
Function by GRFUNC_1:31;
A53:
dom C1 =
(dom q1) \/ (dom q2)
by A3, RELAT_1:13
.=
((dom q5) \/ (dom q6)) \/ (dom q2)
by A21, RELAT_1:13
.=
(dom q5) \/ ((dom q6) \/ (dom q2))
by XBOOLE_1:4
.=
(dom q5) \/ (dom q7)
by RELAT_1:13
;
then A54:
dom q7 c= dom C1
by XBOOLE_1:7;
A55:
dom C1 = Seg (len C1)
by FINSEQ_1:def 3;
then reconsider q7 =
q7 as
FinSubsequence by A54, FINSEQ_1:def 12;
A56:
C1 = q5 \/ q7
by A3, A21, XBOOLE_1:4;
A57:
q5 /\ q7 = (q5 /\ q6) \/ (q5 /\ q2)
by XBOOLE_1:23;
q5 /\ q6 = {}
by A19, XBOOLE_0:def 7;
then A58:
q5 misses q7
by A48, A57, XBOOLE_0:def 7;
A59:
rng (Seq q7) = rng q7
by Lm5;
rng C1 = (rng q7) \/ (rng q5)
by A56, RELAT_1:26;
then A60:
rng (Seq q7) c= rng C1
by A59, XBOOLE_1:7;
rng C1 c= N
by FINSEQ_1:def 4;
then
rng (Seq q7) c= N
by A60, XBOOLE_1:1;
then
Seq q7 is
FinSequence of
N
by FINSEQ_1:def 4;
then reconsider C3 =
Seq q7 as
firing-sequence of
N by FINSEQ_1:def 11;
A61:
dom (Seq q7) = Seg (len (Seq q7))
by FINSEQ_1:def 3;
A62:
dom (q6 * (Sgm (dom q7))) c= dom (Sgm (dom q7))
by RELAT_1:44;
A63:
dom (q2 * (Sgm (dom q7))) c= dom (Sgm (dom q7))
by RELAT_1:44;
A64:
dom (q6 * (Sgm (dom q7))) c= dom (Seq q7)
by A62, Lm4;
dom (q2 * (Sgm (dom q7))) c= dom (Seq q7)
by A63, Lm4;
then reconsider q8 =
q6 * (Sgm (dom q7)),
q9 =
q2 * (Sgm (dom q7)) as
FinSubsequence by A61, A64, FINSEQ_1:def 12;
A65:
C3 =
q7 * (Sgm (dom q7))
by FINSEQ_1:def 14
.=
q8 \/ q9
by RELAT_1:51
;
A66:
dom q8 = (Sgm (dom q7)) " (dom q6)
by RELAT_1:182;
A67:
dom q9 = (Sgm (dom q7)) " (dom q2)
by RELAT_1:182;
(dom q2) /\ (dom q6) = {}
by A52, XBOOLE_0:def 7;
then
(Sgm (dom q7)) " ((dom q6) /\ (dom q2)) = {}
by RELAT_1:171;
then
((Sgm (dom q7)) " (dom q6)) /\ ((Sgm (dom q7)) " (dom q2)) = {}
by FUNCT_1:137;
then A68:
(Sgm (dom q7)) " (dom q6) misses (Sgm (dom q7)) " (dom q2)
by XBOOLE_0:def 7;
A69:
dom q6 c= (dom q6) \/ (dom q2)
by XBOOLE_1:7;
A70:
dom q2 c= (dom q6) \/ (dom q2)
by XBOOLE_1:7;
A71:
dom q6 c= dom q7
by A69, RELAT_1:13;
A72:
dom q2 c= dom q7
by A70, RELAT_1:13;
A73:
dom q6 c= rng (Sgm (dom q7))
by A71, FINSEQ_1:71;
A74:
dom q2 c= rng (Sgm (dom q7))
by A72, FINSEQ_1:71;
A75:
dom q8 = (Sgm (dom q7)) " (dom q6)
by RELAT_1:182;
A76:
dom q9 = (Sgm (dom q7)) " (dom q2)
by RELAT_1:182;
A77:
rng ((Sgm (dom q7)) | (dom q8)) =
rng ((dom q6) | (Sgm (dom q7)))
by A75, Th12
.=
dom q6
by A73, RELAT_1:120
;
A78:
dom q8 c= dom (Sgm (dom q7))
by RELAT_1:44;
A79:
dom q9 c= dom (Sgm (dom q7))
by RELAT_1:44;
A80:
(Sgm (dom q7)) * (Sgm (dom q8)) = Sgm (rng ((Sgm (dom q7)) | (dom q8)))
by A53, A55, A78, GRAPH_2:3, XBOOLE_1:7;
A81:
Seq q8 =
(q6 * (Sgm (dom q7))) * (Sgm (dom q8))
by FINSEQ_1:def 14
.=
q6 * ((Sgm (dom q7)) * (Sgm (dom q8)))
by RELAT_1:55
.=
Seq q6
by A77, A80, FINSEQ_1:def 14
;
A82:
rng ((Sgm (dom q7)) | (dom q9)) =
rng ((dom q2) | (Sgm (dom q7)))
by A76, Th12
.=
dom q2
by A74, RELAT_1:120
;
A83:
(Sgm (dom q7)) * (Sgm (dom q9)) = Sgm (rng ((Sgm (dom q7)) | (dom q9)))
by A53, A55, A79, GRAPH_2:3, XBOOLE_1:7;
A84:
Seq q9 =
(q2 * (Sgm (dom q7))) * (Sgm (dom q9))
by FINSEQ_1:def 14
.=
q2 * ((Sgm (dom q7)) * (Sgm (dom q9)))
by RELAT_1:55
.=
Seq q2
by A82, A83, FINSEQ_1:def 14
;
Seq q8 in R2
by A12, A45, A46, A81, GRAPH_2:30;
then
ex
ss1,
ss2 being
FinSubsequence st
(
C3 = ss1 \/ ss2 &
ss1 misses ss2 &
Seq ss1 in R2 &
Seq ss2 in R3 )
by A6, A65, A66, A67, A68, A84, Th8;
then
Seq q7 in R2 concur R3
;
hence
x in R1 concur (R2 concur R3)
by A1, A11, A44, A56, A58;
verum
end;
let x be set ; TARSKI:def 3 ( not x in R1 concur (R2 concur R3) or x in (R1 concur R2) concur R3 )
assume
x in R1 concur (R2 concur R3)
; x in (R1 concur R2) concur R3
then consider C1 being firing-sequence of N such that
A85:
x = C1
and
A86:
ex q1, q2 being FinSubsequence st
( C1 = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 & Seq q2 in R2 concur R3 )
;
consider q1, q2 being FinSubsequence such that
A87:
C1 = q1 \/ q2
and
A88:
q1 misses q2
and
A89:
Seq q1 in R1
and
A90:
Seq q2 in R2 concur R3
by A86;
consider C2 being firing-sequence of N such that
A91:
Seq q2 = C2
and
A92:
ex q3, q4 being FinSubsequence st
( C2 = q3 \/ q4 & q3 misses q4 & Seq q3 in R2 & Seq q4 in R3 )
by A90;
consider q3, q4 being FinSubsequence such that
A93:
C2 = q3 \/ q4
and
A94:
q3 misses q4
and
A95:
Seq q3 in R2
and
A96:
Seq q4 in R3
by A92;
consider n1 being Nat such that
A97:
dom q2 c= Seg n1
by FINSEQ_1:def 12;
A98:
q3 c= Seq q2
by A91, A93, XBOOLE_1:7;
A99:
q4 c= Seq q2
by A91, A93, XBOOLE_1:7;
Sgm (dom q2) is one-to-one
by A97, FINSEQ_3:99;
then A100:
(Sgm (dom q2)) .: (dom q3) misses (Sgm (dom q2)) .: (dom q4)
by A94, A98, A99, Th10, FUNCT_1:125;
A101:
rng ((Sgm (dom q2)) | (dom q3)) = (Sgm (dom q2)) .: (dom q3)
by RELAT_1:148;
A102:
rng ((Sgm (dom q2)) | (dom q4)) = (Sgm (dom q2)) .: (dom q4)
by RELAT_1:148;
then A103:
q2 | (rng ((Sgm (dom q2)) | (dom q3))) misses q2 | (rng ((Sgm (dom q2)) | (dom q4)))
by A100, A101, Th9;
A104: dom (Sgm (dom q2)) =
dom (Seq q2)
by Lm4
.=
(dom q3) \/ (dom q4)
by A91, A93, RELAT_1:13
;
A105: (q2 | (rng ((Sgm (dom q2)) | (dom q3)))) \/ (q2 | (rng ((Sgm (dom q2)) | (dom q4)))) =
q2 | ((rng ((Sgm (dom q2)) | (dom q3))) \/ (rng ((Sgm (dom q2)) | (dom q4))))
by RELAT_1:107
.=
q2 | ((Sgm (dom q2)) .: ((dom q3) \/ (dom q4)))
by A101, A102, RELAT_1:153
.=
q2 | (rng ((Sgm (dom q2)) | (dom (Sgm (dom q2)))))
by A104, RELAT_1:148
.=
q2 | (rng (Sgm (dom q2)))
by RELAT_1:98
.=
q2 | (dom q2)
by FINSEQ_1:71
.=
q2
by RELAT_1:98
;
A116:
q2 c= C1
by A87, XBOOLE_1:7;
A117:
q2 | (rng ((Sgm (dom q2)) | (dom q3))) c= q2
by A105, XBOOLE_1:7;
A118:
q2 | (rng ((Sgm (dom q2)) | (dom q4))) c= q2
by A105, XBOOLE_1:7;
rng C1 = (rng q1) \/ (rng q2)
by A87, RELAT_1:26;
then A119:
rng q2 c= rng C1
by XBOOLE_1:7;
A120:
rng q2 = rng (Seq q2)
by Lm5;
A121:
rng (Seq q2) c= rng C1
by A119, Lm5;
A122:
rng (Seq q2) = (rng q3) \/ (rng q4)
by A91, A93, RELAT_1:26;
then A123:
rng q3 c= rng (Seq q2)
by XBOOLE_1:7;
rng q3 = rng (Seq q3)
by Lm5;
then A124:
rng (Seq q3) c= rng C1
by A121, A123, XBOOLE_1:1;
A125:
rng q4 c= rng (Seq q2)
by A122, XBOOLE_1:7;
rng q4 = rng (Seq q4)
by Lm5;
then A126:
rng (Seq q4) c= rng C1
by A121, A125, XBOOLE_1:1;
reconsider q5 = q2 | (rng ((Sgm (dom q2)) | (dom q3))), q6 = q2 | (rng ((Sgm (dom q2)) | (dom q4))) as FinSubsequence ;
reconsider fs = C1 as FinSequence of rng C1 by FINSEQ_1:def 4;
reconsider fs1 = Seq q2 as FinSequence of rng C1 by A119, A120, FINSEQ_1:def 4;
reconsider fs2 = Seq q3 as FinSequence of rng C1 by A124, FINSEQ_1:def 4;
reconsider fs3 = Seq q4 as FinSequence of rng C1 by A126, FINSEQ_1:def 4;
reconsider fss = q2, fss1 = q5, fss2 = q6 as Subset of fs by A116, A117, A118, XBOOLE_1:1;
reconsider fss3 = q3, fss4 = q4 as Subset of fs1 by A91, A93, XBOOLE_1:7;
A127:
Seq fss3 = fs2
;
A128:
fss1 = fss | (rng ((Sgm (dom fss)) | (dom fss3)))
;
A129:
Seq fss4 = fs3
;
fss2 = fss | (rng ((Sgm (dom fss)) | (dom fss4)))
;
then A130:
Seq q4 = Seq q6
by A129, GRAPH_2:30;
q1 /\ q2 = {}
by A88, XBOOLE_0:def 7;
then A131:
(q1 /\ q5) \/ (q1 /\ q6) = {}
by A105, XBOOLE_1:23;
then A132:
q1 /\ q5 = {}
;
A133:
q1 /\ q6 = {}
by A131;
A134:
q1 misses q5
by A132, XBOOLE_0:def 7;
A135:
q1 c= C1
by A87, XBOOLE_1:7;
A136:
q2 c= C1
by A87, XBOOLE_1:7;
q5 c= q2
by A105, XBOOLE_1:7;
then
q5 c= C1
by A136, XBOOLE_1:1;
then A137:
dom q1 misses dom q5
by A134, A135, Th10;
then reconsider q7 = q1 \/ q5 as Function by GRFUNC_1:31;
A138: dom C1 =
(dom q1) \/ (dom q2)
by A87, RELAT_1:13
.=
(dom q1) \/ ((dom q5) \/ (dom q6))
by A105, RELAT_1:13
.=
((dom q1) \/ (dom q5)) \/ (dom q6)
by XBOOLE_1:4
.=
(dom q7) \/ (dom q6)
by RELAT_1:13
;
then A139:
dom q7 c= dom C1
by XBOOLE_1:7;
A140:
dom C1 = Seg (len C1)
by FINSEQ_1:def 3;
then reconsider q7 = q7 as FinSubsequence by A139, FINSEQ_1:def 12;
A141:
C1 = q7 \/ q6
by A87, A105, XBOOLE_1:4;
A142:
q7 /\ q6 = (q1 /\ q6) \/ (q5 /\ q6)
by XBOOLE_1:23;
q5 /\ q6 = {}
by A103, XBOOLE_0:def 7;
then A143:
q7 misses q6
by A133, A142, XBOOLE_0:def 7;
A144:
rng (Seq q7) = rng q7
by Lm5;
rng C1 = (rng q7) \/ (rng q6)
by A141, RELAT_1:26;
then A145:
rng (Seq q7) c= rng C1
by A144, XBOOLE_1:7;
rng C1 c= N
by FINSEQ_1:def 4;
then
rng (Seq q7) c= N
by A145, XBOOLE_1:1;
then
Seq q7 is FinSequence of N
by FINSEQ_1:def 4;
then reconsider C3 = Seq q7 as firing-sequence of N by FINSEQ_1:def 11;
A146:
dom (Seq q7) = Seg (len (Seq q7))
by FINSEQ_1:def 3;
A147:
dom (q1 * (Sgm (dom q7))) c= dom (Sgm (dom q7))
by RELAT_1:44;
A148:
dom (q5 * (Sgm (dom q7))) c= dom (Sgm (dom q7))
by RELAT_1:44;
A149:
dom (q1 * (Sgm (dom q7))) c= dom (Seq q7)
by A147, Lm4;
dom (q5 * (Sgm (dom q7))) c= dom (Seq q7)
by A148, Lm4;
then reconsider q8 = q1 * (Sgm (dom q7)), q9 = q5 * (Sgm (dom q7)) as FinSubsequence by A146, A149, FINSEQ_1:def 12;
A150: C3 =
q7 * (Sgm (dom q7))
by FINSEQ_1:def 14
.=
q8 \/ q9
by RELAT_1:51
;
A151:
dom q8 = (Sgm (dom q7)) " (dom q1)
by RELAT_1:182;
A152:
dom q9 = (Sgm (dom q7)) " (dom q5)
by RELAT_1:182;
(dom q1) /\ (dom q5) = {}
by A137, XBOOLE_0:def 7;
then
(Sgm (dom q7)) " ((dom q1) /\ (dom q5)) = {}
by RELAT_1:171;
then
((Sgm (dom q7)) " (dom q1)) /\ ((Sgm (dom q7)) " (dom q5)) = {}
by FUNCT_1:137;
then A153:
(Sgm (dom q7)) " (dom q1) misses (Sgm (dom q7)) " (dom q5)
by XBOOLE_0:def 7;
A154:
dom q1 c= (dom q1) \/ (dom q5)
by XBOOLE_1:7;
A155:
dom q5 c= (dom q1) \/ (dom q5)
by XBOOLE_1:7;
A156:
dom q1 c= dom q7
by A154, RELAT_1:13;
A157:
dom q5 c= dom q7
by A155, RELAT_1:13;
A158:
dom q1 c= rng (Sgm (dom q7))
by A156, FINSEQ_1:71;
A159:
dom q5 c= rng (Sgm (dom q7))
by A157, FINSEQ_1:71;
A160:
dom q8 = (Sgm (dom q7)) " (dom q1)
by RELAT_1:182;
A161:
dom q9 = (Sgm (dom q7)) " (dom q5)
by RELAT_1:182;
A162: rng ((Sgm (dom q7)) | (dom q8)) =
rng ((dom q1) | (Sgm (dom q7)))
by A160, Th12
.=
dom q1
by A158, RELAT_1:120
;
A163:
dom q8 c= dom (Sgm (dom q7))
by RELAT_1:44;
A164:
dom q9 c= dom (Sgm (dom q7))
by RELAT_1:44;
A165:
(Sgm (dom q7)) * (Sgm (dom q8)) = Sgm (rng ((Sgm (dom q7)) | (dom q8)))
by A138, A140, A163, GRAPH_2:3, XBOOLE_1:7;
A166: Seq q8 =
(q1 * (Sgm (dom q7))) * (Sgm (dom q8))
by FINSEQ_1:def 14
.=
q1 * ((Sgm (dom q7)) * (Sgm (dom q8)))
by RELAT_1:55
.=
Seq q1
by A162, A165, FINSEQ_1:def 14
;
A167: rng ((Sgm (dom q7)) | (dom q9)) =
rng ((dom q5) | (Sgm (dom q7)))
by A161, Th12
.=
dom q5
by A159, RELAT_1:120
;
A168:
(Sgm (dom q7)) * (Sgm (dom q9)) = Sgm (rng ((Sgm (dom q7)) | (dom q9)))
by A138, A140, A164, GRAPH_2:3, XBOOLE_1:7;
Seq q9 =
(q5 * (Sgm (dom q7))) * (Sgm (dom q9))
by FINSEQ_1:def 14
.=
q5 * ((Sgm (dom q7)) * (Sgm (dom q9)))
by RELAT_1:55
.=
Seq q5
by A167, A168, FINSEQ_1:def 14
;
then
Seq q9 in R2
by A95, A127, A128, GRAPH_2:30;
then
ex ss1, ss2 being FinSubsequence st
( C3 = ss1 \/ ss2 & ss1 misses ss2 & Seq ss1 in R1 & Seq ss2 in R2 )
by A89, A150, A151, A152, A153, A166, Th8;
then
Seq q7 in R1 concur R2
;
hence
x in (R1 concur R2) concur R3
by A85, A96, A130, A141, A143; verum