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 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

A75: x = C1 and

A76: 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

A77: C1 = q1 \/ q2 and

A78: q1 misses q2 and

A79: Seq q1 in R1 and

A80: Seq q2 in R2 concur R3 by A76;

consider C2 being firing-sequence of N such that

A81: Seq q2 = C2 and

A82: ex q3, q4 being FinSubsequence st

( C2 = q3 \/ q4 & q3 misses q4 & Seq q3 in R2 & Seq q4 in R3 ) by A80;

consider q3, q4 being FinSubsequence such that

A83: C2 = q3 \/ q4 and

A84: q3 misses q4 and

A85: Seq q3 in R2 and

A86: Seq q4 in R3 by A82;

consider n1 being Nat such that

A87: dom q2 c= Seg n1 by FINSEQ_1:def 12;

A88: q3 c= Seq q2 by A81, A83, XBOOLE_1:7;

A89: q4 c= Seq q2 by A81, A83, XBOOLE_1:7;

Sgm (dom q2) is one-to-one by A87, FINSEQ_3:92;

then A90: (Sgm (dom q2)) .: (dom q3) misses (Sgm (dom q2)) .: (dom q4) by A84, A88, A89, FUNCT_1:66, FUNCT_1:112;

A91: rng ((Sgm (dom q2)) | (dom q3)) = (Sgm (dom q2)) .: (dom q3) by RELAT_1:115;

A92: rng ((Sgm (dom q2)) | (dom q4)) = (Sgm (dom q2)) .: (dom q4) by RELAT_1:115;

then A93: q2 | (rng ((Sgm (dom q2)) | (dom q3))) misses q2 | (rng ((Sgm (dom q2)) | (dom q4))) by A90, A91, RELAT_1:187;

A94: dom (Sgm (dom q2)) = dom (Seq q2) by FINSEQ_1:100

.= (dom q3) \/ (dom q4) by A81, A83, XTUPLE_0:23 ;

A95: (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:78

.= q2 | ((Sgm (dom q2)) .: ((dom q3) \/ (dom q4))) by A91, A92, RELAT_1:120

.= q2 | (rng ((Sgm (dom q2)) | (dom (Sgm (dom q2))))) by A94, RELAT_1:115

.= q2 | (rng (Sgm (dom q2)))

.= q2 | (dom q2) by FINSEQ_1:50

.= q2 ;

A96: q2 c= C1 by A77, XBOOLE_1:7;

A97: q2 | (rng ((Sgm (dom q2)) | (dom q3))) c= q2 by A95, XBOOLE_1:7;

A98: q2 | (rng ((Sgm (dom q2)) | (dom q4))) c= q2 by A95, XBOOLE_1:7;

rng C1 = (rng q1) \/ (rng q2) by A77, RELAT_1:12;

then A99: rng q2 c= rng C1 by XBOOLE_1:7;

A100: rng q2 = rng (Seq q2) by FINSEQ_1:101;

A101: rng (Seq q2) c= rng C1 by A99, FINSEQ_1:101;

A102: rng (Seq q2) = (rng q3) \/ (rng q4) by A81, A83, RELAT_1:12;

then A103: rng q3 c= rng (Seq q2) by XBOOLE_1:7;

rng q3 = rng (Seq q3) by FINSEQ_1:101;

then A104: rng (Seq q3) c= rng C1 by A101, A103;

A105: rng q4 c= rng (Seq q2) by A102, XBOOLE_1:7;

rng q4 = rng (Seq q4) by FINSEQ_1:101;

then A106: rng (Seq q4) c= rng C1 by A101, A105;

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 A99, A100, FINSEQ_1:def 4;

reconsider fs2 = Seq q3 as FinSequence of rng C1 by A104, FINSEQ_1:def 4;

reconsider fs3 = Seq q4 as FinSequence of rng C1 by A106, FINSEQ_1:def 4;

reconsider fss = q2, fss1 = q5, fss2 = q6 as Subset of fs by A96, A97, A98, XBOOLE_1:1;

reconsider fss3 = q3, fss4 = q4 as Subset of fs1 by A81, A83, XBOOLE_1:7;

A107: Seq fss3 = fs2 ;

A108: fss1 = fss | (rng ((Sgm (dom fss)) | (dom fss3))) ;

A109: Seq fss4 = fs3 ;

fss2 = fss | (rng ((Sgm (dom fss)) | (dom fss4))) ;

then A110: Seq q4 = Seq q6 by A109, FINSEQ_6:154;

q1 /\ q2 = {} by A78;

then A111: (q1 /\ q5) \/ (q1 /\ q6) = {} by A95, XBOOLE_1:23;

then A112: q1 /\ q5 = {} ;

A113: q1 /\ q6 = {} by A111;

A114: q1 misses q5 by A112;

A115: q1 c= C1 by A77, XBOOLE_1:7;

A116: q2 c= C1 by A77, XBOOLE_1:7;

q5 c= q2 by A95, XBOOLE_1:7;

then q5 c= C1 by A116;

then A117: dom q1 misses dom q5 by A114, A115, FUNCT_1:112;

then reconsider q7 = q1 \/ q5 as Function by GRFUNC_1:13;

A118: dom C1 = (dom q1) \/ (dom q2) by A77, XTUPLE_0:23

.= (dom q1) \/ ((dom q5) \/ (dom q6)) by A95, XTUPLE_0:23

.= ((dom q1) \/ (dom q5)) \/ (dom q6) by XBOOLE_1:4

.= (dom q7) \/ (dom q6) by XTUPLE_0:23 ;

then A119: dom q7 c= dom C1 by XBOOLE_1:7;

A120: dom C1 = Seg (len C1) by FINSEQ_1:def 3;

then reconsider q7 = q7 as FinSubsequence by A119, FINSEQ_1:def 12;

A121: C1 = q7 \/ q6 by A77, A95, XBOOLE_1:4;

A122: q7 /\ q6 = (q1 /\ q6) \/ (q5 /\ q6) by XBOOLE_1:23;

q5 /\ q6 = {} by A93;

then A123: q7 misses q6 by A113, A122;

A124: rng (Seq q7) = rng q7 by FINSEQ_1:101;

rng C1 = (rng q7) \/ (rng q6) by A121, RELAT_1:12;

then A125: rng (Seq q7) c= rng C1 by A124, XBOOLE_1:7;

rng C1 c= N by FINSEQ_1:def 4;

then rng (Seq q7) c= N by A125;

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;

A126: dom (Seq q7) = Seg (len (Seq q7)) by FINSEQ_1:def 3;

A127: dom (q1 * (Sgm (dom q7))) c= dom (Sgm (dom q7)) by RELAT_1:25;

A128: dom (q5 * (Sgm (dom q7))) c= dom (Sgm (dom q7)) by RELAT_1:25;

A129: dom (q1 * (Sgm (dom q7))) c= dom (Seq q7) by A127, FINSEQ_1:100;

dom (q5 * (Sgm (dom q7))) c= dom (Seq q7) by A128, FINSEQ_1:100;

then reconsider q8 = q1 * (Sgm (dom q7)), q9 = q5 * (Sgm (dom q7)) as FinSubsequence by A126, A129, FINSEQ_1:def 12;

A130: C3 = q7 * (Sgm (dom q7)) by FINSEQ_1:def 14

.= q8 \/ q9 by RELAT_1:32 ;

A131: dom q8 = (Sgm (dom q7)) " (dom q1) by RELAT_1:147;

A132: dom q9 = (Sgm (dom q7)) " (dom q5) by RELAT_1:147;

(dom q1) /\ (dom q5) = {} by A117;

then (Sgm (dom q7)) " ((dom q1) /\ (dom q5)) = {} ;

then ((Sgm (dom q7)) " (dom q1)) /\ ((Sgm (dom q7)) " (dom q5)) = {} by FUNCT_1:68;

then A133: (Sgm (dom q7)) " (dom q1) misses (Sgm (dom q7)) " (dom q5) ;

A134: dom q1 c= (dom q1) \/ (dom q5) by XBOOLE_1:7;

A135: dom q5 c= (dom q1) \/ (dom q5) by XBOOLE_1:7;

A136: dom q1 c= dom q7 by A134, XTUPLE_0:23;

A137: dom q5 c= dom q7 by A135, XTUPLE_0:23;

A138: dom q1 c= rng (Sgm (dom q7)) by A136, FINSEQ_1:50;

A139: dom q5 c= rng (Sgm (dom q7)) by A137, FINSEQ_1:50;

A140: dom q8 = (Sgm (dom q7)) " (dom q1) by RELAT_1:147;

A141: dom q9 = (Sgm (dom q7)) " (dom q5) by RELAT_1:147;

A142: rng ((Sgm (dom q7)) | (dom q8)) = rng ((dom q1) |` (Sgm (dom q7))) by A140, FUNCT_1:113

.= dom q1 by A138, RELAT_1:89 ;

A143: dom q8 c= dom (Sgm (dom q7)) by RELAT_1:25;

A144: dom q9 c= dom (Sgm (dom q7)) by RELAT_1:25;

A145: (Sgm (dom q7)) * (Sgm (dom q8)) = Sgm (rng ((Sgm (dom q7)) | (dom q8))) by A118, A120, A143, FINSEQ_6:129, XBOOLE_1:7;

A146: Seq q8 = (q1 * (Sgm (dom q7))) * (Sgm (dom q8)) by FINSEQ_1:def 14

.= q1 * ((Sgm (dom q7)) * (Sgm (dom q8))) by RELAT_1:36

.= Seq q1 by A142, A145, FINSEQ_1:def 14 ;

A147: rng ((Sgm (dom q7)) | (dom q9)) = rng ((dom q5) |` (Sgm (dom q7))) by A141, FUNCT_1:113

.= dom q5 by A139, RELAT_1:89 ;

A148: (Sgm (dom q7)) * (Sgm (dom q9)) = Sgm (rng ((Sgm (dom q7)) | (dom q9))) by A118, A120, A144, FINSEQ_6:129, 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:36

.= Seq q5 by A147, A148, FINSEQ_1:def 14 ;

then Seq q9 in R2 by A85, A107, A108, FINSEQ_6:154;

then ex ss1, ss2 being FinSubsequence st

( C3 = ss1 \/ ss2 & ss1 misses ss2 & Seq ss1 in R1 & Seq ss2 in R2 ) by A79, A130, A131, A132, A133, A146, RELAT_1:179;

then Seq q7 in R1 concur R2 ;

hence x in (R1 concur R2) concur R3 by A75, A86, A110, A121, A123; :: thesis: verum

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 R3

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in R1 concur (R2 concur R3) or x in (R1 concur R2) concur R3 )
let x be object ; :: 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 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:92;

then A16: (Sgm (dom q1)) .: (dom q3) misses (Sgm (dom q1)) .: (dom q4) by A10, A14, A15, FUNCT_1:66, FUNCT_1:112;

A17: rng ((Sgm (dom q1)) | (dom q3)) = (Sgm (dom q1)) .: (dom q3) by RELAT_1:115;

A18: rng ((Sgm (dom q1)) | (dom q4)) = (Sgm (dom q1)) .: (dom q4) by RELAT_1:115;

then A19: q1 | (rng ((Sgm (dom q1)) | (dom q3))) misses q1 | (rng ((Sgm (dom q1)) | (dom q4))) by A16, A17, RELAT_1:187;

A20: dom (Sgm (dom q1)) = dom (q3 \/ q4) by A7, A9, FINSEQ_1:100

.= (dom q3) \/ (dom q4) by XTUPLE_0:23 ;

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:78

.= q1 | ((Sgm (dom q1)) .: ((dom q3) \/ (dom q4))) by A17, A18, RELAT_1:120

.= q1 | (rng ((Sgm (dom q1)) | (dom (Sgm (dom q1))))) by A20, RELAT_1:115

.= q1 | (rng (Sgm (dom q1)))

.= q1 | (dom q1) by FINSEQ_1:50

.= q1 ;

A22: q1 c= C1 by A3, XBOOLE_1:7;

A23: q1 | (rng ((Sgm (dom q1)) | (dom q3))) c= q1 by A21, XBOOLE_1:7;

A24: q1 | (rng ((Sgm (dom q1)) | (dom q4))) c= q1 by A21, XBOOLE_1:7;

rng C1 = (rng q1) \/ (rng q2) by A3, RELAT_1:12;

then A25: rng q1 c= rng C1 by XBOOLE_1:7;

A26: rng q1 = rng (Seq q1) by FINSEQ_1:101;

A27: rng (Seq q1) c= rng C1 by A25, FINSEQ_1:101;

A28: rng (Seq q1) = (rng q3) \/ (rng q4) by A7, A9, RELAT_1:12;

then A29: rng q3 c= rng (Seq q1) by XBOOLE_1:7;

rng q3 = rng (Seq q3) by FINSEQ_1:101;

then A30: rng (Seq q3) c= rng C1 by A27, A29;

A31: rng q4 c= rng (Seq q1) by A28, XBOOLE_1:7;

rng q4 = rng (Seq q4) by FINSEQ_1:101;

then A32: rng (Seq q4) c= rng C1 by A27, A31;

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 A25, A26, FINSEQ_1:def 4;

reconsider fs2 = Seq q3 as FinSequence of rng C1 by A30, FINSEQ_1:def 4;

reconsider fs3 = Seq q4 as FinSequence of rng C1 by A32, FINSEQ_1:def 4;

reconsider fss = q1, fss1 = q5, fss2 = q6 as Subset of fs by A22, A23, A24, XBOOLE_1:1;

reconsider fss3 = q3, fss4 = q4 as Subset of fs1 by A7, A9, XBOOLE_1:7;

A33: Seq fss3 = fs2 ;

fss1 = fss | (rng ((Sgm (dom fss)) | (dom fss3))) ;

then A34: Seq q3 = Seq q5 by A33, FINSEQ_6:154;

A35: Seq fss4 = fs3 ;

A36: fss2 = fss | (rng ((Sgm (dom fss)) | (dom fss4))) ;

q1 /\ q2 = {} by A4;

then A37: (q5 /\ q2) \/ (q6 /\ q2) = {} by A21, XBOOLE_1:23;

then A38: q5 /\ q2 = {} ;

q6 /\ q2 = {} by A37;

then A39: q6 misses q2 ;

A40: q1 c= C1 by A3, XBOOLE_1:7;

A41: q2 c= C1 by A3, XBOOLE_1:7;

q6 c= q1 by A21, XBOOLE_1:7;

then q6 c= C1 by A40;

then A42: dom q6 misses dom q2 by A39, A41, FUNCT_1:112;

then reconsider q7 = q6 \/ q2 as Function by GRFUNC_1:13;

A43: dom C1 = (dom q1) \/ (dom q2) by A3, XTUPLE_0:23

.= ((dom q5) \/ (dom q6)) \/ (dom q2) by A21, XTUPLE_0:23

.= (dom q5) \/ ((dom q6) \/ (dom q2)) by XBOOLE_1:4

.= (dom q5) \/ (dom q7) by XTUPLE_0:23 ;

then A44: dom q7 c= dom C1 by XBOOLE_1:7;

A45: dom C1 = Seg (len C1) by FINSEQ_1:def 3;

then reconsider q7 = q7 as FinSubsequence by A44, FINSEQ_1:def 12;

A46: C1 = q5 \/ q7 by A3, A21, XBOOLE_1:4;

A47: q5 /\ q7 = (q5 /\ q6) \/ (q5 /\ q2) by XBOOLE_1:23;

q5 /\ q6 = {} by A19;

then A48: q5 misses q7 by A38, A47;

A49: rng (Seq q7) = rng q7 by FINSEQ_1:101;

rng C1 = (rng q7) \/ (rng q5) by A46, RELAT_1:12;

then A50: rng (Seq q7) c= rng C1 by A49, XBOOLE_1:7;

rng C1 c= N by FINSEQ_1:def 4;

then rng (Seq q7) c= N by A50;

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;

A51: dom (Seq q7) = Seg (len (Seq q7)) by FINSEQ_1:def 3;

A52: dom (q6 * (Sgm (dom q7))) c= dom (Sgm (dom q7)) by RELAT_1:25;

A53: dom (q2 * (Sgm (dom q7))) c= dom (Sgm (dom q7)) by RELAT_1:25;

A54: dom (q6 * (Sgm (dom q7))) c= dom (Seq q7) by A52, FINSEQ_1:100;

dom (q2 * (Sgm (dom q7))) c= dom (Seq q7) by A53, FINSEQ_1:100;

then reconsider q8 = q6 * (Sgm (dom q7)), q9 = q2 * (Sgm (dom q7)) as FinSubsequence by A51, A54, FINSEQ_1:def 12;

A55: C3 = q7 * (Sgm (dom q7)) by FINSEQ_1:def 14

.= q8 \/ q9 by RELAT_1:32 ;

A56: dom q8 = (Sgm (dom q7)) " (dom q6) by RELAT_1:147;

A57: dom q9 = (Sgm (dom q7)) " (dom q2) by RELAT_1:147;

(dom q2) /\ (dom q6) = {} by A42;

then (Sgm (dom q7)) " ((dom q6) /\ (dom q2)) = {} ;

then ((Sgm (dom q7)) " (dom q6)) /\ ((Sgm (dom q7)) " (dom q2)) = {} by FUNCT_1:68;

then A58: (Sgm (dom q7)) " (dom q6) misses (Sgm (dom q7)) " (dom q2) ;

A59: dom q6 c= (dom q6) \/ (dom q2) by XBOOLE_1:7;

A60: dom q2 c= (dom q6) \/ (dom q2) by XBOOLE_1:7;

A61: dom q6 c= dom q7 by A59, XTUPLE_0:23;

A62: dom q2 c= dom q7 by A60, XTUPLE_0:23;

A63: dom q6 c= rng (Sgm (dom q7)) by A61, FINSEQ_1:50;

A64: dom q2 c= rng (Sgm (dom q7)) by A62, FINSEQ_1:50;

A65: dom q8 = (Sgm (dom q7)) " (dom q6) by RELAT_1:147;

A66: dom q9 = (Sgm (dom q7)) " (dom q2) by RELAT_1:147;

A67: rng ((Sgm (dom q7)) | (dom q8)) = rng ((dom q6) |` (Sgm (dom q7))) by A65, FUNCT_1:113

.= dom q6 by A63, RELAT_1:89 ;

A68: dom q8 c= dom (Sgm (dom q7)) by RELAT_1:25;

A69: dom q9 c= dom (Sgm (dom q7)) by RELAT_1:25;

A70: (Sgm (dom q7)) * (Sgm (dom q8)) = Sgm (rng ((Sgm (dom q7)) | (dom q8))) by A43, A45, A68, FINSEQ_6:129, XBOOLE_1:7;

A71: Seq q8 = (q6 * (Sgm (dom q7))) * (Sgm (dom q8)) by FINSEQ_1:def 14

.= q6 * ((Sgm (dom q7)) * (Sgm (dom q8))) by RELAT_1:36

.= Seq q6 by A67, A70, FINSEQ_1:def 14 ;

A72: rng ((Sgm (dom q7)) | (dom q9)) = rng ((dom q2) |` (Sgm (dom q7))) by A66, FUNCT_1:113

.= dom q2 by A64, RELAT_1:89 ;

A73: (Sgm (dom q7)) * (Sgm (dom q9)) = Sgm (rng ((Sgm (dom q7)) | (dom q9))) by A43, A45, A69, FINSEQ_6:129, XBOOLE_1:7;

A74: Seq q9 = (q2 * (Sgm (dom q7))) * (Sgm (dom q9)) by FINSEQ_1:def 14

.= q2 * ((Sgm (dom q7)) * (Sgm (dom q9))) by RELAT_1:36

.= Seq q2 by A72, A73, FINSEQ_1:def 14 ;

Seq q8 in R2 by A12, A35, A36, A71, FINSEQ_6:154;

then ex ss1, ss2 being FinSubsequence st

( C3 = ss1 \/ ss2 & ss1 misses ss2 & Seq ss1 in R2 & Seq ss2 in R3 ) by A6, A55, A56, A57, A58, A74, RELAT_1:179;

then Seq q7 in R2 concur R3 ;

hence x in R1 concur (R2 concur R3) by A1, A11, A34, A46, A48; :: thesis: verum

end;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 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:92;

then A16: (Sgm (dom q1)) .: (dom q3) misses (Sgm (dom q1)) .: (dom q4) by A10, A14, A15, FUNCT_1:66, FUNCT_1:112;

A17: rng ((Sgm (dom q1)) | (dom q3)) = (Sgm (dom q1)) .: (dom q3) by RELAT_1:115;

A18: rng ((Sgm (dom q1)) | (dom q4)) = (Sgm (dom q1)) .: (dom q4) by RELAT_1:115;

then A19: q1 | (rng ((Sgm (dom q1)) | (dom q3))) misses q1 | (rng ((Sgm (dom q1)) | (dom q4))) by A16, A17, RELAT_1:187;

A20: dom (Sgm (dom q1)) = dom (q3 \/ q4) by A7, A9, FINSEQ_1:100

.= (dom q3) \/ (dom q4) by XTUPLE_0:23 ;

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:78

.= q1 | ((Sgm (dom q1)) .: ((dom q3) \/ (dom q4))) by A17, A18, RELAT_1:120

.= q1 | (rng ((Sgm (dom q1)) | (dom (Sgm (dom q1))))) by A20, RELAT_1:115

.= q1 | (rng (Sgm (dom q1)))

.= q1 | (dom q1) by FINSEQ_1:50

.= q1 ;

A22: q1 c= C1 by A3, XBOOLE_1:7;

A23: q1 | (rng ((Sgm (dom q1)) | (dom q3))) c= q1 by A21, XBOOLE_1:7;

A24: q1 | (rng ((Sgm (dom q1)) | (dom q4))) c= q1 by A21, XBOOLE_1:7;

rng C1 = (rng q1) \/ (rng q2) by A3, RELAT_1:12;

then A25: rng q1 c= rng C1 by XBOOLE_1:7;

A26: rng q1 = rng (Seq q1) by FINSEQ_1:101;

A27: rng (Seq q1) c= rng C1 by A25, FINSEQ_1:101;

A28: rng (Seq q1) = (rng q3) \/ (rng q4) by A7, A9, RELAT_1:12;

then A29: rng q3 c= rng (Seq q1) by XBOOLE_1:7;

rng q3 = rng (Seq q3) by FINSEQ_1:101;

then A30: rng (Seq q3) c= rng C1 by A27, A29;

A31: rng q4 c= rng (Seq q1) by A28, XBOOLE_1:7;

rng q4 = rng (Seq q4) by FINSEQ_1:101;

then A32: rng (Seq q4) c= rng C1 by A27, A31;

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 A25, A26, FINSEQ_1:def 4;

reconsider fs2 = Seq q3 as FinSequence of rng C1 by A30, FINSEQ_1:def 4;

reconsider fs3 = Seq q4 as FinSequence of rng C1 by A32, FINSEQ_1:def 4;

reconsider fss = q1, fss1 = q5, fss2 = q6 as Subset of fs by A22, A23, A24, XBOOLE_1:1;

reconsider fss3 = q3, fss4 = q4 as Subset of fs1 by A7, A9, XBOOLE_1:7;

A33: Seq fss3 = fs2 ;

fss1 = fss | (rng ((Sgm (dom fss)) | (dom fss3))) ;

then A34: Seq q3 = Seq q5 by A33, FINSEQ_6:154;

A35: Seq fss4 = fs3 ;

A36: fss2 = fss | (rng ((Sgm (dom fss)) | (dom fss4))) ;

q1 /\ q2 = {} by A4;

then A37: (q5 /\ q2) \/ (q6 /\ q2) = {} by A21, XBOOLE_1:23;

then A38: q5 /\ q2 = {} ;

q6 /\ q2 = {} by A37;

then A39: q6 misses q2 ;

A40: q1 c= C1 by A3, XBOOLE_1:7;

A41: q2 c= C1 by A3, XBOOLE_1:7;

q6 c= q1 by A21, XBOOLE_1:7;

then q6 c= C1 by A40;

then A42: dom q6 misses dom q2 by A39, A41, FUNCT_1:112;

then reconsider q7 = q6 \/ q2 as Function by GRFUNC_1:13;

A43: dom C1 = (dom q1) \/ (dom q2) by A3, XTUPLE_0:23

.= ((dom q5) \/ (dom q6)) \/ (dom q2) by A21, XTUPLE_0:23

.= (dom q5) \/ ((dom q6) \/ (dom q2)) by XBOOLE_1:4

.= (dom q5) \/ (dom q7) by XTUPLE_0:23 ;

then A44: dom q7 c= dom C1 by XBOOLE_1:7;

A45: dom C1 = Seg (len C1) by FINSEQ_1:def 3;

then reconsider q7 = q7 as FinSubsequence by A44, FINSEQ_1:def 12;

A46: C1 = q5 \/ q7 by A3, A21, XBOOLE_1:4;

A47: q5 /\ q7 = (q5 /\ q6) \/ (q5 /\ q2) by XBOOLE_1:23;

q5 /\ q6 = {} by A19;

then A48: q5 misses q7 by A38, A47;

A49: rng (Seq q7) = rng q7 by FINSEQ_1:101;

rng C1 = (rng q7) \/ (rng q5) by A46, RELAT_1:12;

then A50: rng (Seq q7) c= rng C1 by A49, XBOOLE_1:7;

rng C1 c= N by FINSEQ_1:def 4;

then rng (Seq q7) c= N by A50;

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;

A51: dom (Seq q7) = Seg (len (Seq q7)) by FINSEQ_1:def 3;

A52: dom (q6 * (Sgm (dom q7))) c= dom (Sgm (dom q7)) by RELAT_1:25;

A53: dom (q2 * (Sgm (dom q7))) c= dom (Sgm (dom q7)) by RELAT_1:25;

A54: dom (q6 * (Sgm (dom q7))) c= dom (Seq q7) by A52, FINSEQ_1:100;

dom (q2 * (Sgm (dom q7))) c= dom (Seq q7) by A53, FINSEQ_1:100;

then reconsider q8 = q6 * (Sgm (dom q7)), q9 = q2 * (Sgm (dom q7)) as FinSubsequence by A51, A54, FINSEQ_1:def 12;

A55: C3 = q7 * (Sgm (dom q7)) by FINSEQ_1:def 14

.= q8 \/ q9 by RELAT_1:32 ;

A56: dom q8 = (Sgm (dom q7)) " (dom q6) by RELAT_1:147;

A57: dom q9 = (Sgm (dom q7)) " (dom q2) by RELAT_1:147;

(dom q2) /\ (dom q6) = {} by A42;

then (Sgm (dom q7)) " ((dom q6) /\ (dom q2)) = {} ;

then ((Sgm (dom q7)) " (dom q6)) /\ ((Sgm (dom q7)) " (dom q2)) = {} by FUNCT_1:68;

then A58: (Sgm (dom q7)) " (dom q6) misses (Sgm (dom q7)) " (dom q2) ;

A59: dom q6 c= (dom q6) \/ (dom q2) by XBOOLE_1:7;

A60: dom q2 c= (dom q6) \/ (dom q2) by XBOOLE_1:7;

A61: dom q6 c= dom q7 by A59, XTUPLE_0:23;

A62: dom q2 c= dom q7 by A60, XTUPLE_0:23;

A63: dom q6 c= rng (Sgm (dom q7)) by A61, FINSEQ_1:50;

A64: dom q2 c= rng (Sgm (dom q7)) by A62, FINSEQ_1:50;

A65: dom q8 = (Sgm (dom q7)) " (dom q6) by RELAT_1:147;

A66: dom q9 = (Sgm (dom q7)) " (dom q2) by RELAT_1:147;

A67: rng ((Sgm (dom q7)) | (dom q8)) = rng ((dom q6) |` (Sgm (dom q7))) by A65, FUNCT_1:113

.= dom q6 by A63, RELAT_1:89 ;

A68: dom q8 c= dom (Sgm (dom q7)) by RELAT_1:25;

A69: dom q9 c= dom (Sgm (dom q7)) by RELAT_1:25;

A70: (Sgm (dom q7)) * (Sgm (dom q8)) = Sgm (rng ((Sgm (dom q7)) | (dom q8))) by A43, A45, A68, FINSEQ_6:129, XBOOLE_1:7;

A71: Seq q8 = (q6 * (Sgm (dom q7))) * (Sgm (dom q8)) by FINSEQ_1:def 14

.= q6 * ((Sgm (dom q7)) * (Sgm (dom q8))) by RELAT_1:36

.= Seq q6 by A67, A70, FINSEQ_1:def 14 ;

A72: rng ((Sgm (dom q7)) | (dom q9)) = rng ((dom q2) |` (Sgm (dom q7))) by A66, FUNCT_1:113

.= dom q2 by A64, RELAT_1:89 ;

A73: (Sgm (dom q7)) * (Sgm (dom q9)) = Sgm (rng ((Sgm (dom q7)) | (dom q9))) by A43, A45, A69, FINSEQ_6:129, XBOOLE_1:7;

A74: Seq q9 = (q2 * (Sgm (dom q7))) * (Sgm (dom q9)) by FINSEQ_1:def 14

.= q2 * ((Sgm (dom q7)) * (Sgm (dom q9))) by RELAT_1:36

.= Seq q2 by A72, A73, FINSEQ_1:def 14 ;

Seq q8 in R2 by A12, A35, A36, A71, FINSEQ_6:154;

then ex ss1, ss2 being FinSubsequence st

( C3 = ss1 \/ ss2 & ss1 misses ss2 & Seq ss1 in R2 & Seq ss2 in R3 ) by A6, A55, A56, A57, A58, A74, RELAT_1:179;

then Seq q7 in R2 concur R3 ;

hence x in R1 concur (R2 concur R3) by A1, A11, A34, A46, A48; :: thesis: verum

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

A75: x = C1 and

A76: 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

A77: C1 = q1 \/ q2 and

A78: q1 misses q2 and

A79: Seq q1 in R1 and

A80: Seq q2 in R2 concur R3 by A76;

consider C2 being firing-sequence of N such that

A81: Seq q2 = C2 and

A82: ex q3, q4 being FinSubsequence st

( C2 = q3 \/ q4 & q3 misses q4 & Seq q3 in R2 & Seq q4 in R3 ) by A80;

consider q3, q4 being FinSubsequence such that

A83: C2 = q3 \/ q4 and

A84: q3 misses q4 and

A85: Seq q3 in R2 and

A86: Seq q4 in R3 by A82;

consider n1 being Nat such that

A87: dom q2 c= Seg n1 by FINSEQ_1:def 12;

A88: q3 c= Seq q2 by A81, A83, XBOOLE_1:7;

A89: q4 c= Seq q2 by A81, A83, XBOOLE_1:7;

Sgm (dom q2) is one-to-one by A87, FINSEQ_3:92;

then A90: (Sgm (dom q2)) .: (dom q3) misses (Sgm (dom q2)) .: (dom q4) by A84, A88, A89, FUNCT_1:66, FUNCT_1:112;

A91: rng ((Sgm (dom q2)) | (dom q3)) = (Sgm (dom q2)) .: (dom q3) by RELAT_1:115;

A92: rng ((Sgm (dom q2)) | (dom q4)) = (Sgm (dom q2)) .: (dom q4) by RELAT_1:115;

then A93: q2 | (rng ((Sgm (dom q2)) | (dom q3))) misses q2 | (rng ((Sgm (dom q2)) | (dom q4))) by A90, A91, RELAT_1:187;

A94: dom (Sgm (dom q2)) = dom (Seq q2) by FINSEQ_1:100

.= (dom q3) \/ (dom q4) by A81, A83, XTUPLE_0:23 ;

A95: (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:78

.= q2 | ((Sgm (dom q2)) .: ((dom q3) \/ (dom q4))) by A91, A92, RELAT_1:120

.= q2 | (rng ((Sgm (dom q2)) | (dom (Sgm (dom q2))))) by A94, RELAT_1:115

.= q2 | (rng (Sgm (dom q2)))

.= q2 | (dom q2) by FINSEQ_1:50

.= q2 ;

A96: q2 c= C1 by A77, XBOOLE_1:7;

A97: q2 | (rng ((Sgm (dom q2)) | (dom q3))) c= q2 by A95, XBOOLE_1:7;

A98: q2 | (rng ((Sgm (dom q2)) | (dom q4))) c= q2 by A95, XBOOLE_1:7;

rng C1 = (rng q1) \/ (rng q2) by A77, RELAT_1:12;

then A99: rng q2 c= rng C1 by XBOOLE_1:7;

A100: rng q2 = rng (Seq q2) by FINSEQ_1:101;

A101: rng (Seq q2) c= rng C1 by A99, FINSEQ_1:101;

A102: rng (Seq q2) = (rng q3) \/ (rng q4) by A81, A83, RELAT_1:12;

then A103: rng q3 c= rng (Seq q2) by XBOOLE_1:7;

rng q3 = rng (Seq q3) by FINSEQ_1:101;

then A104: rng (Seq q3) c= rng C1 by A101, A103;

A105: rng q4 c= rng (Seq q2) by A102, XBOOLE_1:7;

rng q4 = rng (Seq q4) by FINSEQ_1:101;

then A106: rng (Seq q4) c= rng C1 by A101, A105;

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 A99, A100, FINSEQ_1:def 4;

reconsider fs2 = Seq q3 as FinSequence of rng C1 by A104, FINSEQ_1:def 4;

reconsider fs3 = Seq q4 as FinSequence of rng C1 by A106, FINSEQ_1:def 4;

reconsider fss = q2, fss1 = q5, fss2 = q6 as Subset of fs by A96, A97, A98, XBOOLE_1:1;

reconsider fss3 = q3, fss4 = q4 as Subset of fs1 by A81, A83, XBOOLE_1:7;

A107: Seq fss3 = fs2 ;

A108: fss1 = fss | (rng ((Sgm (dom fss)) | (dom fss3))) ;

A109: Seq fss4 = fs3 ;

fss2 = fss | (rng ((Sgm (dom fss)) | (dom fss4))) ;

then A110: Seq q4 = Seq q6 by A109, FINSEQ_6:154;

q1 /\ q2 = {} by A78;

then A111: (q1 /\ q5) \/ (q1 /\ q6) = {} by A95, XBOOLE_1:23;

then A112: q1 /\ q5 = {} ;

A113: q1 /\ q6 = {} by A111;

A114: q1 misses q5 by A112;

A115: q1 c= C1 by A77, XBOOLE_1:7;

A116: q2 c= C1 by A77, XBOOLE_1:7;

q5 c= q2 by A95, XBOOLE_1:7;

then q5 c= C1 by A116;

then A117: dom q1 misses dom q5 by A114, A115, FUNCT_1:112;

then reconsider q7 = q1 \/ q5 as Function by GRFUNC_1:13;

A118: dom C1 = (dom q1) \/ (dom q2) by A77, XTUPLE_0:23

.= (dom q1) \/ ((dom q5) \/ (dom q6)) by A95, XTUPLE_0:23

.= ((dom q1) \/ (dom q5)) \/ (dom q6) by XBOOLE_1:4

.= (dom q7) \/ (dom q6) by XTUPLE_0:23 ;

then A119: dom q7 c= dom C1 by XBOOLE_1:7;

A120: dom C1 = Seg (len C1) by FINSEQ_1:def 3;

then reconsider q7 = q7 as FinSubsequence by A119, FINSEQ_1:def 12;

A121: C1 = q7 \/ q6 by A77, A95, XBOOLE_1:4;

A122: q7 /\ q6 = (q1 /\ q6) \/ (q5 /\ q6) by XBOOLE_1:23;

q5 /\ q6 = {} by A93;

then A123: q7 misses q6 by A113, A122;

A124: rng (Seq q7) = rng q7 by FINSEQ_1:101;

rng C1 = (rng q7) \/ (rng q6) by A121, RELAT_1:12;

then A125: rng (Seq q7) c= rng C1 by A124, XBOOLE_1:7;

rng C1 c= N by FINSEQ_1:def 4;

then rng (Seq q7) c= N by A125;

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;

A126: dom (Seq q7) = Seg (len (Seq q7)) by FINSEQ_1:def 3;

A127: dom (q1 * (Sgm (dom q7))) c= dom (Sgm (dom q7)) by RELAT_1:25;

A128: dom (q5 * (Sgm (dom q7))) c= dom (Sgm (dom q7)) by RELAT_1:25;

A129: dom (q1 * (Sgm (dom q7))) c= dom (Seq q7) by A127, FINSEQ_1:100;

dom (q5 * (Sgm (dom q7))) c= dom (Seq q7) by A128, FINSEQ_1:100;

then reconsider q8 = q1 * (Sgm (dom q7)), q9 = q5 * (Sgm (dom q7)) as FinSubsequence by A126, A129, FINSEQ_1:def 12;

A130: C3 = q7 * (Sgm (dom q7)) by FINSEQ_1:def 14

.= q8 \/ q9 by RELAT_1:32 ;

A131: dom q8 = (Sgm (dom q7)) " (dom q1) by RELAT_1:147;

A132: dom q9 = (Sgm (dom q7)) " (dom q5) by RELAT_1:147;

(dom q1) /\ (dom q5) = {} by A117;

then (Sgm (dom q7)) " ((dom q1) /\ (dom q5)) = {} ;

then ((Sgm (dom q7)) " (dom q1)) /\ ((Sgm (dom q7)) " (dom q5)) = {} by FUNCT_1:68;

then A133: (Sgm (dom q7)) " (dom q1) misses (Sgm (dom q7)) " (dom q5) ;

A134: dom q1 c= (dom q1) \/ (dom q5) by XBOOLE_1:7;

A135: dom q5 c= (dom q1) \/ (dom q5) by XBOOLE_1:7;

A136: dom q1 c= dom q7 by A134, XTUPLE_0:23;

A137: dom q5 c= dom q7 by A135, XTUPLE_0:23;

A138: dom q1 c= rng (Sgm (dom q7)) by A136, FINSEQ_1:50;

A139: dom q5 c= rng (Sgm (dom q7)) by A137, FINSEQ_1:50;

A140: dom q8 = (Sgm (dom q7)) " (dom q1) by RELAT_1:147;

A141: dom q9 = (Sgm (dom q7)) " (dom q5) by RELAT_1:147;

A142: rng ((Sgm (dom q7)) | (dom q8)) = rng ((dom q1) |` (Sgm (dom q7))) by A140, FUNCT_1:113

.= dom q1 by A138, RELAT_1:89 ;

A143: dom q8 c= dom (Sgm (dom q7)) by RELAT_1:25;

A144: dom q9 c= dom (Sgm (dom q7)) by RELAT_1:25;

A145: (Sgm (dom q7)) * (Sgm (dom q8)) = Sgm (rng ((Sgm (dom q7)) | (dom q8))) by A118, A120, A143, FINSEQ_6:129, XBOOLE_1:7;

A146: Seq q8 = (q1 * (Sgm (dom q7))) * (Sgm (dom q8)) by FINSEQ_1:def 14

.= q1 * ((Sgm (dom q7)) * (Sgm (dom q8))) by RELAT_1:36

.= Seq q1 by A142, A145, FINSEQ_1:def 14 ;

A147: rng ((Sgm (dom q7)) | (dom q9)) = rng ((dom q5) |` (Sgm (dom q7))) by A141, FUNCT_1:113

.= dom q5 by A139, RELAT_1:89 ;

A148: (Sgm (dom q7)) * (Sgm (dom q9)) = Sgm (rng ((Sgm (dom q7)) | (dom q9))) by A118, A120, A144, FINSEQ_6:129, 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:36

.= Seq q5 by A147, A148, FINSEQ_1:def 14 ;

then Seq q9 in R2 by A85, A107, A108, FINSEQ_6:154;

then ex ss1, ss2 being FinSubsequence st

( C3 = ss1 \/ ss2 & ss1 misses ss2 & Seq ss1 in R1 & Seq ss2 in R2 ) by A79, A130, A131, A132, A133, A146, RELAT_1:179;

then Seq q7 in R1 concur R2 ;

hence x in (R1 concur R2) concur R3 by A75, A86, A110, A121, A123; :: thesis: verum