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
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) )
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 ;
A15: q4 c= Seq q1 by ;
Sgm (dom q1) is one-to-one by ;
then A16: (Sgm (dom q1)) .: (dom q3) misses (Sgm (dom q1)) .: (dom q4) by ;
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 ;
A20: dom (Sgm (dom q1)) = dom (q3 \/ q4) by
.= (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
.= q1 | (rng ((Sgm (dom q1)) | (dom (Sgm (dom q1))))) by
.= q1 | (rng (Sgm (dom q1)))
.= q1 | (dom q1) by FINSEQ_1:50
.= q1 ;
A22: q1 c= C1 by ;
A23: q1 | (rng ((Sgm (dom q1)) | (dom q3))) c= q1 by ;
A24: q1 | (rng ((Sgm (dom q1)) | (dom q4))) c= q1 by ;
rng C1 = (rng q1) \/ (rng q2) by ;
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 ;
A28: rng (Seq q1) = (rng q3) \/ (rng q4) by ;
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 ;
A31: rng q4 c= rng (Seq q1) by ;
rng q4 = rng (Seq q4) by FINSEQ_1:101;
then A32: rng (Seq q4) c= rng C1 by ;
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 ;
reconsider fs2 = Seq q3 as FinSequence of rng C1 by ;
reconsider fs3 = Seq q4 as FinSequence of rng C1 by ;
reconsider fss = q1, fss1 = q5, fss2 = q6 as Subset of fs by ;
reconsider fss3 = q3, fss4 = q4 as Subset of fs1 by ;
A33: Seq fss3 = fs2 ;
fss1 = fss | (rng ((Sgm (dom fss)) | (dom fss3))) ;
then A34: Seq q3 = Seq q5 by ;
A35: Seq fss4 = fs3 ;
A36: fss2 = fss | (rng ((Sgm (dom fss)) | (dom fss4))) ;
q1 /\ q2 = {} by A4;
then A37: (q5 /\ q2) \/ (q6 /\ q2) = {} by ;
then A38: q5 /\ q2 = {} ;
q6 /\ q2 = {} by A37;
then A39: q6 misses q2 ;
A40: q1 c= C1 by ;
A41: q2 c= C1 by ;
q6 c= q1 by ;
then q6 c= C1 by A40;
then A42: dom q6 misses dom q2 by ;
then reconsider q7 = q6 \/ q2 as Function by GRFUNC_1:13;
A43: dom C1 = (dom q1) \/ (dom q2) by
.= ((dom q5) \/ (dom q6)) \/ (dom q2) by
.= (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 ;
A46: C1 = q5 \/ q7 by ;
A47: q5 /\ q7 = (q5 /\ q6) \/ (q5 /\ q2) by XBOOLE_1:23;
q5 /\ q6 = {} by A19;
then A48: q5 misses q7 by ;
A49: rng (Seq q7) = rng q7 by FINSEQ_1:101;
rng C1 = (rng q7) \/ (rng q5) by ;
then A50: rng (Seq q7) c= rng C1 by ;
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 ;
dom (q2 * (Sgm (dom q7))) c= dom (Seq q7) by ;
then reconsider q8 = q6 * (Sgm (dom q7)), q9 = q2 * (Sgm (dom q7)) as FinSubsequence by ;
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 ;
A62: dom q2 c= dom q7 by ;
A63: dom q6 c= rng (Sgm (dom q7)) by ;
A64: dom q2 c= rng (Sgm (dom q7)) by ;
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
.= dom q6 by ;
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 ;
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 ;
A72: rng ((Sgm (dom q7)) | (dom q9)) = rng ((dom q2) |` (Sgm (dom q7))) by
.= dom q2 by ;
A73: (Sgm (dom q7)) * (Sgm (dom q9)) = Sgm (rng ((Sgm (dom q7)) | (dom q9))) by ;
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 ;
Seq q8 in R2 by ;
then ex ss1, ss2 being FinSubsequence st
( C3 = ss1 \/ ss2 & ss1 misses ss2 & Seq ss1 in R2 & Seq ss2 in R3 ) by ;
then Seq q7 in R2 concur R3 ;
hence x in R1 concur (R2 concur R3) by A1, A11, A34, A46, A48; :: thesis: verum
end;
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
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 ;
A89: q4 c= Seq q2 by ;
Sgm (dom q2) is one-to-one by ;
then A90: (Sgm (dom q2)) .: (dom q3) misses (Sgm (dom q2)) .: (dom q4) by ;
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 ;
A94: dom (Sgm (dom q2)) = dom (Seq q2) by FINSEQ_1:100
.= (dom q3) \/ (dom q4) by ;
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
.= q2 | (rng ((Sgm (dom q2)) | (dom (Sgm (dom q2))))) by
.= q2 | (rng (Sgm (dom q2)))
.= q2 | (dom q2) by FINSEQ_1:50
.= q2 ;
A96: q2 c= C1 by ;
A97: q2 | (rng ((Sgm (dom q2)) | (dom q3))) c= q2 by ;
A98: q2 | (rng ((Sgm (dom q2)) | (dom q4))) c= q2 by ;
rng C1 = (rng q1) \/ (rng q2) by ;
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 ;
A102: rng (Seq q2) = (rng q3) \/ (rng q4) by ;
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 ;
A105: rng q4 c= rng (Seq q2) by ;
rng q4 = rng (Seq q4) by FINSEQ_1:101;
then A106: rng (Seq q4) c= rng C1 by ;
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 ;
reconsider fs2 = Seq q3 as FinSequence of rng C1 by ;
reconsider fs3 = Seq q4 as FinSequence of rng C1 by ;
reconsider fss = q2, fss1 = q5, fss2 = q6 as Subset of fs by ;
reconsider fss3 = q3, fss4 = q4 as Subset of fs1 by ;
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 ;
q1 /\ q2 = {} by A78;
then A111: (q1 /\ q5) \/ (q1 /\ q6) = {} by ;
then A112: q1 /\ q5 = {} ;
A113: q1 /\ q6 = {} by A111;
A114: q1 misses q5 by A112;
A115: q1 c= C1 by ;
A116: q2 c= C1 by ;
q5 c= q2 by ;
then q5 c= C1 by A116;
then A117: dom q1 misses dom q5 by ;
then reconsider q7 = q1 \/ q5 as Function by GRFUNC_1:13;
A118: dom C1 = (dom q1) \/ (dom q2) by
.= (dom q1) \/ ((dom q5) \/ (dom q6)) by
.= ((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 ;
A121: C1 = q7 \/ q6 by ;
A122: q7 /\ q6 = (q1 /\ q6) \/ (q5 /\ q6) by XBOOLE_1:23;
q5 /\ q6 = {} by A93;
then A123: q7 misses q6 by ;
A124: rng (Seq q7) = rng q7 by FINSEQ_1:101;
rng C1 = (rng q7) \/ (rng q6) by ;
then A125: rng (Seq q7) c= rng C1 by ;
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 ;
dom (q5 * (Sgm (dom q7))) c= dom (Seq q7) by ;
then reconsider q8 = q1 * (Sgm (dom q7)), q9 = q5 * (Sgm (dom q7)) as FinSubsequence by ;
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 ;
A137: dom q5 c= dom q7 by ;
A138: dom q1 c= rng (Sgm (dom q7)) by ;
A139: dom q5 c= rng (Sgm (dom q7)) by ;
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
.= dom q1 by ;
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 ;
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 ;
A147: rng ((Sgm (dom q7)) | (dom q9)) = rng ((dom q5) |` (Sgm (dom q7))) by
.= dom q5 by ;
A148: (Sgm (dom q7)) * (Sgm (dom q9)) = Sgm (rng ((Sgm (dom q7)) | (dom q9))) by ;
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 ;
then Seq q9 in R2 by ;
then ex ss1, ss2 being FinSubsequence st
( C3 = ss1 \/ ss2 & ss1 misses ss2 & Seq ss1 in R1 & Seq ss2 in R2 ) by ;
then Seq q7 in R1 concur R2 ;
hence x in (R1 concur R2) concur R3 by ; :: thesis: verum