let P be set ; :: thesis: 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; :: thesis: 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; :: thesis: (R1 concur R2) concur R3 = R1 concur (R2 concur R3)
thus
(R1 concur R2) concur R3 c= R1 concur (R2 concur R3)
:: according to XBOOLE_0:def 10 :: thesis: R1 concur (R2 concur R3) c= (R1 concur R2) concur R3proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in (R1 concur R2) concur R3 or x in R1 concur (R2 concur R3) )
assume
x in (R1 concur R2) concur R3
;
:: thesis: x in R1 concur (R2 concur R3)
then consider C1 being
firing-sequence of
N such that A1:
(
x = C1 & 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 A2:
(
C1 = q1 \/ q2 &
q1 misses q2 &
Seq q1 in R1 concur R2 &
Seq q2 in R3 )
by A1;
consider C2 being
firing-sequence of
N such that A3:
(
Seq q1 = C2 & ex
q3,
q4 being
FinSubsequence st
(
C2 = q3 \/ q4 &
q3 misses q4 &
Seq q3 in R1 &
Seq q4 in R2 ) )
by A2;
consider q3,
q4 being
FinSubsequence such that A4:
(
C2 = q3 \/ q4 &
q3 misses q4 &
Seq q3 in R1 &
Seq q4 in R2 )
by A3;
consider n1 being
Nat such that A5:
dom q1 c= Seg n1
by FINSEQ_1:def 12;
A6:
(
q3 c= Seq q1 &
q4 c= Seq q1 )
by A3, A4, XBOOLE_1:7;
Sgm (dom q1) is
one-to-one
by A5, FINSEQ_3:99;
then A7:
(Sgm (dom q1)) .: (dom q3) misses (Sgm (dom q1)) .: (dom q4)
by A4, A6, Th10, FUNCT_1:125;
A8:
(
rng ((Sgm (dom q1)) | (dom q3)) = (Sgm (dom q1)) .: (dom q3) &
rng ((Sgm (dom q1)) | (dom q4)) = (Sgm (dom q1)) .: (dom q4) )
by RELAT_1:148;
then A9:
q1 | (rng ((Sgm (dom q1)) | (dom q3))) misses q1 | (rng ((Sgm (dom q1)) | (dom q4)))
by A7, Th9;
A10:
dom (Sgm (dom q1)) =
dom (q3 \/ q4)
by A3, A4, Lm4
.=
(dom q3) \/ (dom q4)
by RELAT_1:13
;
A11:
(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 A8, RELAT_1:153
.=
q1 | (rng ((Sgm (dom q1)) | (dom (Sgm (dom q1)))))
by A10, RELAT_1:148
.=
q1 | (rng (Sgm (dom q1)))
by RELAT_1:98
.=
q1 | (dom q1)
by FINSEQ_1:71
.=
q1
by RELAT_1:98
;
A12:
(
dom (q1 | (rng ((Sgm (dom q1)) | (dom q3)))) c= rng ((Sgm (dom q1)) | (dom q3)) &
dom (q1 | (rng ((Sgm (dom q1)) | (dom q4)))) c= rng ((Sgm (dom q1)) | (dom q4)) )
by RELAT_1:87;
(
rng ((Sgm (dom q1)) | (dom q3)) c= rng (Sgm (dom q1)) &
rng ((Sgm (dom q1)) | (dom q4)) c= rng (Sgm (dom q1)) )
by RELAT_1:99;
then
(
rng ((Sgm (dom q1)) | (dom q3)) c= dom q1 &
rng ((Sgm (dom q1)) | (dom q4)) c= dom q1 )
by FINSEQ_1:71;
then
(
dom (q1 | (rng ((Sgm (dom q1)) | (dom q3)))) c= dom q1 &
dom (q1 | (rng ((Sgm (dom q1)) | (dom q4)))) c= dom q1 )
by A12, XBOOLE_1:1;
then A13:
(
dom (q1 | (rng ((Sgm (dom q1)) | (dom q3)))) c= Seg n1 &
dom (q1 | (rng ((Sgm (dom q1)) | (dom q4)))) c= Seg n1 )
by A5, XBOOLE_1:1;
A14:
q1 c= C1
by A2, XBOOLE_1:7;
A15:
q1 | (rng ((Sgm (dom q1)) | (dom q3))) c= q1
by A11, XBOOLE_1:7;
A16:
q1 | (rng ((Sgm (dom q1)) | (dom q4))) c= q1
by A11, XBOOLE_1:7;
rng C1 = (rng q1) \/ (rng q2)
by A2, RELAT_1:26;
then A17:
rng q1 c= rng C1
by XBOOLE_1:7;
A18:
rng q1 = rng (Seq q1)
by Lm5;
A19:
rng (Seq q1) c= rng C1
by A17, Lm5;
A20:
rng (Seq q1) = (rng q3) \/ (rng q4)
by A3, A4, RELAT_1:26;
then A21:
rng q3 c= rng (Seq q1)
by XBOOLE_1:7;
rng q3 = rng (Seq q3)
by Lm5;
then A22:
rng (Seq q3) c= rng C1
by A19, A21, XBOOLE_1:1;
A23:
rng q4 c= rng (Seq q1)
by A20, XBOOLE_1:7;
rng q4 = rng (Seq q4)
by Lm5;
then A24:
rng (Seq q4) c= rng C1
by A19, A23, XBOOLE_1:1;
reconsider q5 =
q1 | (rng ((Sgm (dom q1)) | (dom q3))),
q6 =
q1 | (rng ((Sgm (dom q1)) | (dom q4))) as
FinSubsequence by A13, FINSEQ_1:def 12;
reconsider fs =
C1 as
FinSequence of
rng C1 by FINSEQ_1:def 4;
reconsider fs1 =
Seq q1 as
FinSequence of
rng C1 by A17, A18, FINSEQ_1:def 4;
reconsider fs2 =
Seq q3 as
FinSequence of
rng C1 by A22, FINSEQ_1:def 4;
reconsider fs3 =
Seq q4 as
FinSequence of
rng C1 by A24, FINSEQ_1:def 4;
reconsider fss =
q1,
fss1 =
q5,
fss2 =
q6 as
Subset of
fs by A14, A15, A16, XBOOLE_1:1;
reconsider fss3 =
q3,
fss4 =
q4 as
Subset of
fs1 by A3, A4, XBOOLE_1:7;
(
Seq fss = fs1 &
Seq fss3 = fs2 &
fss1 = fss | (rng ((Sgm (dom fss)) | (dom fss3))) )
;
then A25:
Seq q3 = Seq q5
by GRAPH_2:30;
(
Seq fss = fs1 &
Seq fss4 = fs3 &
fss2 = fss | (rng ((Sgm (dom fss)) | (dom fss4))) )
;
then A26:
Seq q4 = Seq q6
by GRAPH_2:30;
q1 /\ q2 = {}
by A2, XBOOLE_0:def 7;
then
(q5 /\ q2) \/ (q6 /\ q2) = {}
by A11, XBOOLE_1:23;
then A27:
(
q5 /\ q2 = {} &
q6 /\ q2 = {} )
;
then A28:
q6 misses q2
by XBOOLE_0:def 7;
A29:
(
q1 c= C1 &
q2 c= C1 )
by A2, XBOOLE_1:7;
q6 c= q1
by A11, XBOOLE_1:7;
then
q6 c= C1
by A29, XBOOLE_1:1;
then A30:
dom q6 misses dom q2
by A28, A29, Th10;
then reconsider q7 =
q6 \/ q2 as
Function by GRFUNC_1:31;
A31:
dom C1 =
(dom q1) \/ (dom q2)
by A2, RELAT_1:13
.=
((dom q5) \/ (dom q6)) \/ (dom q2)
by A11, RELAT_1:13
.=
(dom q5) \/ ((dom q6) \/ (dom q2))
by XBOOLE_1:4
.=
(dom q5) \/ (dom q7)
by RELAT_1:13
;
then A32:
dom q7 c= dom C1
by XBOOLE_1:7;
A33:
dom C1 = Seg (len C1)
by FINSEQ_1:def 3;
then reconsider q7 =
q7 as
FinSubsequence by A32, FINSEQ_1:def 12;
A34:
C1 = q5 \/ q7
by A2, A11, XBOOLE_1:4;
A35:
q5 /\ q7 = (q5 /\ q6) \/ (q5 /\ q2)
by XBOOLE_1:23;
q5 /\ q6 = {}
by A9, XBOOLE_0:def 7;
then A36:
q5 misses q7
by A27, A35, XBOOLE_0:def 7;
A37:
rng (Seq q7) = rng q7
by Lm5;
rng C1 = (rng q7) \/ (rng q5)
by A34, RELAT_1:26;
then A38:
rng (Seq q7) c= rng C1
by A37, XBOOLE_1:7;
rng C1 c= N
by FINSEQ_1:def 4;
then
rng (Seq q7) c= N
by A38, 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;
A39:
dom (Seq q7) = Seg (len (Seq q7))
by FINSEQ_1:def 3;
(
dom (q6 * (Sgm (dom q7))) c= dom (Sgm (dom q7)) &
dom (q2 * (Sgm (dom q7))) c= dom (Sgm (dom q7)) )
by RELAT_1:44;
then
(
dom (q6 * (Sgm (dom q7))) c= dom (Seq q7) &
dom (q2 * (Sgm (dom q7))) c= dom (Seq q7) )
by Lm4;
then reconsider q8 =
q6 * (Sgm (dom q7)),
q9 =
q2 * (Sgm (dom q7)) as
FinSubsequence by A39, FINSEQ_1:def 12;
ex
ss1,
ss2 being
FinSubsequence st
(
C3 = ss1 \/ ss2 &
ss1 misses ss2 &
Seq ss1 in R2 &
Seq ss2 in R3 )
proof
A40:
C3 =
q7 * (Sgm (dom q7))
by FINSEQ_1:def 14
.=
q8 \/ q9
by RELAT_1:51
;
A41:
dom q8 = (Sgm (dom q7)) " (dom q6)
by RELAT_1:182;
A42:
dom q9 = (Sgm (dom q7)) " (dom q2)
by RELAT_1:182;
(dom q2) /\ (dom q6) = {}
by A30, 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 A43:
(Sgm (dom q7)) " (dom q6) misses (Sgm (dom q7)) " (dom q2)
by XBOOLE_0:def 7;
(
dom q6 c= (dom q6) \/ (dom q2) &
dom q2 c= (dom q6) \/ (dom q2) )
by XBOOLE_1:7;
then
(
dom q6 c= dom q7 &
dom q2 c= dom q7 )
by RELAT_1:13;
then A44:
(
dom q6 c= rng (Sgm (dom q7)) &
dom q2 c= rng (Sgm (dom q7)) )
by FINSEQ_1:71;
A45:
(
dom q8 = (Sgm (dom q7)) " (dom q6) &
dom q9 = (Sgm (dom q7)) " (dom q2) )
by RELAT_1:182;
then A46:
rng ((Sgm (dom q7)) | (dom q8)) =
rng ((dom q6) | (Sgm (dom q7)))
by Th12
.=
dom q6
by A44, RELAT_1:120
;
A47:
(
dom q8 c= dom (Sgm (dom q7)) &
dom q9 c= dom (Sgm (dom q7)) )
by RELAT_1:44;
then A48:
(Sgm (dom q7)) * (Sgm (dom q8)) = Sgm (rng ((Sgm (dom q7)) | (dom q8)))
by A31, A33, GRAPH_2:3, XBOOLE_1:7;
A49:
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 A46, A48, FINSEQ_1:def 14
;
A50:
rng ((Sgm (dom q7)) | (dom q9)) =
rng ((dom q2) | (Sgm (dom q7)))
by A45, Th12
.=
dom q2
by A44, RELAT_1:120
;
A51:
(Sgm (dom q7)) * (Sgm (dom q9)) = Sgm (rng ((Sgm (dom q7)) | (dom q9)))
by A31, A33, A47, GRAPH_2:3, XBOOLE_1:7;
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 A50, A51, FINSEQ_1:def 14
;
hence
ex
ss1,
ss2 being
FinSubsequence st
(
C3 = ss1 \/ ss2 &
ss1 misses ss2 &
Seq ss1 in R2 &
Seq ss2 in R3 )
by A2, A4, A26, A40, A41, A42, A43, A49, Th8;
:: thesis: verum
end;
then
Seq q7 in R2 concur R3
;
hence
x in R1 concur (R2 concur R3)
by A1, A4, A25, A34, A36;
:: thesis: verum
end;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in R1 concur (R2 concur R3) or x in (R1 concur R2) concur R3 )
assume
x in R1 concur (R2 concur R3)
; :: thesis: x in (R1 concur R2) concur R3
then consider C1 being firing-sequence of N such that
A52:
( x = C1 & 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
A53:
( C1 = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 & Seq q2 in R2 concur R3 )
by A52;
consider C2 being firing-sequence of N such that
A54:
( Seq q2 = C2 & ex q3, q4 being FinSubsequence st
( C2 = q3 \/ q4 & q3 misses q4 & Seq q3 in R2 & Seq q4 in R3 ) )
by A53;
consider q3, q4 being FinSubsequence such that
A55:
( C2 = q3 \/ q4 & q3 misses q4 & Seq q3 in R2 & Seq q4 in R3 )
by A54;
consider n1 being Nat such that
A56:
dom q2 c= Seg n1
by FINSEQ_1:def 12;
A57:
( q3 c= Seq q2 & q4 c= Seq q2 )
by A54, A55, XBOOLE_1:7;
Sgm (dom q2) is one-to-one
by A56, FINSEQ_3:99;
then A58:
(Sgm (dom q2)) .: (dom q3) misses (Sgm (dom q2)) .: (dom q4)
by A55, A57, Th10, FUNCT_1:125;
A59:
( rng ((Sgm (dom q2)) | (dom q3)) = (Sgm (dom q2)) .: (dom q3) & rng ((Sgm (dom q2)) | (dom q4)) = (Sgm (dom q2)) .: (dom q4) )
by RELAT_1:148;
then A60:
q2 | (rng ((Sgm (dom q2)) | (dom q3))) misses q2 | (rng ((Sgm (dom q2)) | (dom q4)))
by A58, Th9;
A61: dom (Sgm (dom q2)) =
dom (Seq q2)
by Lm4
.=
(dom q3) \/ (dom q4)
by A54, A55, RELAT_1:13
;
A62: (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 A59, RELAT_1:153
.=
q2 | (rng ((Sgm (dom q2)) | (dom (Sgm (dom q2)))))
by A61, RELAT_1:148
.=
q2 | (rng (Sgm (dom q2)))
by RELAT_1:98
.=
q2 | (dom q2)
by FINSEQ_1:71
.=
q2
by RELAT_1:98
;
A63:
( dom (q2 | (rng ((Sgm (dom q2)) | (dom q3)))) c= rng ((Sgm (dom q2)) | (dom q3)) & dom (q2 | (rng ((Sgm (dom q2)) | (dom q4)))) c= rng ((Sgm (dom q2)) | (dom q4)) )
by RELAT_1:87;
( rng ((Sgm (dom q2)) | (dom q3)) c= rng (Sgm (dom q2)) & rng ((Sgm (dom q2)) | (dom q4)) c= rng (Sgm (dom q2)) )
by RELAT_1:99;
then
( rng ((Sgm (dom q2)) | (dom q3)) c= dom q2 & rng ((Sgm (dom q2)) | (dom q4)) c= dom q2 )
by FINSEQ_1:71;
then
( dom (q2 | (rng ((Sgm (dom q2)) | (dom q3)))) c= dom q2 & dom (q2 | (rng ((Sgm (dom q2)) | (dom q4)))) c= dom q2 )
by A63, XBOOLE_1:1;
then A64:
( dom (q2 | (rng ((Sgm (dom q2)) | (dom q3)))) c= Seg n1 & dom (q2 | (rng ((Sgm (dom q2)) | (dom q4)))) c= Seg n1 )
by A56, XBOOLE_1:1;
A65:
q2 c= C1
by A53, XBOOLE_1:7;
A66:
q2 | (rng ((Sgm (dom q2)) | (dom q3))) c= q2
by A62, XBOOLE_1:7;
A67:
q2 | (rng ((Sgm (dom q2)) | (dom q4))) c= q2
by A62, XBOOLE_1:7;
rng C1 = (rng q1) \/ (rng q2)
by A53, RELAT_1:26;
then A68:
rng q2 c= rng C1
by XBOOLE_1:7;
A69:
rng q2 = rng (Seq q2)
by Lm5;
A70:
rng (Seq q2) c= rng C1
by A68, Lm5;
A71:
rng (Seq q2) = (rng q3) \/ (rng q4)
by A54, A55, RELAT_1:26;
then A72:
rng q3 c= rng (Seq q2)
by XBOOLE_1:7;
rng q3 = rng (Seq q3)
by Lm5;
then A73:
rng (Seq q3) c= rng C1
by A70, A72, XBOOLE_1:1;
A74:
rng q4 c= rng (Seq q2)
by A71, XBOOLE_1:7;
rng q4 = rng (Seq q4)
by Lm5;
then A75:
rng (Seq q4) c= rng C1
by A70, A74, XBOOLE_1:1;
reconsider q5 = q2 | (rng ((Sgm (dom q2)) | (dom q3))), q6 = q2 | (rng ((Sgm (dom q2)) | (dom q4))) as FinSubsequence by A64, FINSEQ_1:def 12;
reconsider fs = C1 as FinSequence of rng C1 by FINSEQ_1:def 4;
reconsider fs1 = Seq q2 as FinSequence of rng C1 by A68, A69, FINSEQ_1:def 4;
reconsider fs2 = Seq q3 as FinSequence of rng C1 by A73, FINSEQ_1:def 4;
reconsider fs3 = Seq q4 as FinSequence of rng C1 by A75, FINSEQ_1:def 4;
reconsider fss = q2, fss1 = q5, fss2 = q6 as Subset of fs by A65, A66, A67, XBOOLE_1:1;
reconsider fss3 = q3, fss4 = q4 as Subset of fs1 by A54, A55, XBOOLE_1:7;
( Seq fss = fs1 & Seq fss3 = fs2 & fss1 = fss | (rng ((Sgm (dom fss)) | (dom fss3))) )
;
then A76:
Seq q5 in R2
by A55, GRAPH_2:30;
( Seq fss = fs1 & Seq fss4 = fs3 & fss2 = fss | (rng ((Sgm (dom fss)) | (dom fss4))) )
;
then A77:
Seq q4 = Seq q6
by GRAPH_2:30;
q1 /\ q2 = {}
by A53, XBOOLE_0:def 7;
then
(q1 /\ q5) \/ (q1 /\ q6) = {}
by A62, XBOOLE_1:23;
then A78:
( q1 /\ q5 = {} & q1 /\ q6 = {} )
;
then A79:
q1 misses q5
by XBOOLE_0:def 7;
A80:
( q1 c= C1 & q2 c= C1 )
by A53, XBOOLE_1:7;
q5 c= q2
by A62, XBOOLE_1:7;
then
q5 c= C1
by A80, XBOOLE_1:1;
then A81:
dom q1 misses dom q5
by A79, A80, Th10;
then reconsider q7 = q1 \/ q5 as Function by GRFUNC_1:31;
A82: dom C1 =
(dom q1) \/ (dom q2)
by A53, RELAT_1:13
.=
(dom q1) \/ ((dom q5) \/ (dom q6))
by A62, RELAT_1:13
.=
((dom q1) \/ (dom q5)) \/ (dom q6)
by XBOOLE_1:4
.=
(dom q7) \/ (dom q6)
by RELAT_1:13
;
then A83:
dom q7 c= dom C1
by XBOOLE_1:7;
A84:
dom C1 = Seg (len C1)
by FINSEQ_1:def 3;
then reconsider q7 = q7 as FinSubsequence by A83, FINSEQ_1:def 12;
A85:
C1 = q7 \/ q6
by A53, A62, XBOOLE_1:4;
A86:
q7 /\ q6 = (q1 /\ q6) \/ (q5 /\ q6)
by XBOOLE_1:23;
q5 /\ q6 = {}
by A60, XBOOLE_0:def 7;
then A87:
q7 misses q6
by A78, A86, XBOOLE_0:def 7;
A88:
rng (Seq q7) = rng q7
by Lm5;
rng C1 = (rng q7) \/ (rng q6)
by A85, RELAT_1:26;
then A89:
rng (Seq q7) c= rng C1
by A88, XBOOLE_1:7;
rng C1 c= N
by FINSEQ_1:def 4;
then
rng (Seq q7) c= N
by A89, 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;
A90:
dom (Seq q7) = Seg (len (Seq q7))
by FINSEQ_1:def 3;
( dom (q1 * (Sgm (dom q7))) c= dom (Sgm (dom q7)) & dom (q5 * (Sgm (dom q7))) c= dom (Sgm (dom q7)) )
by RELAT_1:44;
then
( dom (q1 * (Sgm (dom q7))) c= dom (Seq q7) & dom (q5 * (Sgm (dom q7))) c= dom (Seq q7) )
by Lm4;
then reconsider q8 = q1 * (Sgm (dom q7)), q9 = q5 * (Sgm (dom q7)) as FinSubsequence by A90, FINSEQ_1:def 12;
ex ss1, ss2 being FinSubsequence st
( C3 = ss1 \/ ss2 & ss1 misses ss2 & Seq ss1 in R1 & Seq ss2 in R2 )
proof
A91:
C3 =
q7 * (Sgm (dom q7))
by FINSEQ_1:def 14
.=
q8 \/ q9
by RELAT_1:51
;
A92:
dom q8 = (Sgm (dom q7)) " (dom q1)
by RELAT_1:182;
A93:
dom q9 = (Sgm (dom q7)) " (dom q5)
by RELAT_1:182;
(dom q1) /\ (dom q5) = {}
by A81, 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 A94:
(Sgm (dom q7)) " (dom q1) misses (Sgm (dom q7)) " (dom q5)
by XBOOLE_0:def 7;
(
dom q1 c= (dom q1) \/ (dom q5) &
dom q5 c= (dom q1) \/ (dom q5) )
by XBOOLE_1:7;
then
(
dom q1 c= dom q7 &
dom q5 c= dom q7 )
by RELAT_1:13;
then A95:
(
dom q1 c= rng (Sgm (dom q7)) &
dom q5 c= rng (Sgm (dom q7)) )
by FINSEQ_1:71;
A96:
(
dom q8 = (Sgm (dom q7)) " (dom q1) &
dom q9 = (Sgm (dom q7)) " (dom q5) )
by RELAT_1:182;
then A97:
rng ((Sgm (dom q7)) | (dom q8)) =
rng ((dom q1) | (Sgm (dom q7)))
by Th12
.=
dom q1
by A95, RELAT_1:120
;
A98:
(
dom q8 c= dom (Sgm (dom q7)) &
dom q9 c= dom (Sgm (dom q7)) )
by RELAT_1:44;
then A99:
(Sgm (dom q7)) * (Sgm (dom q8)) = Sgm (rng ((Sgm (dom q7)) | (dom q8)))
by A82, A84, GRAPH_2:3, XBOOLE_1:7;
A100:
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 A97, A99, FINSEQ_1:def 14
;
A101:
rng ((Sgm (dom q7)) | (dom q9)) =
rng ((dom q5) | (Sgm (dom q7)))
by A96, Th12
.=
dom q5
by A95, RELAT_1:120
;
A102:
(Sgm (dom q7)) * (Sgm (dom q9)) = Sgm (rng ((Sgm (dom q7)) | (dom q9)))
by A82, A84, A98, 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 A101, A102, FINSEQ_1:def 14
;
hence
ex
ss1,
ss2 being
FinSubsequence st
(
C3 = ss1 \/ ss2 &
ss1 misses ss2 &
Seq ss1 in R1 &
Seq ss2 in R2 )
by A53, A76, A91, A92, A93, A94, A100, Th8;
:: thesis: verum
end;
then
Seq q7 in R1 concur R2
;
hence
x in (R1 concur R2) concur R3
by A52, A55, A77, A85, A87; :: thesis: verum