let P be set ; :: thesis: for N being Petri_net of P

for R1, R2, P1, P2 being process of N holds (R1 concur R2) before (P1 concur P2) c= (R1 before P1) concur (R2 before P2)

let N be Petri_net of P; :: thesis: for R1, R2, P1, P2 being process of N holds (R1 concur R2) before (P1 concur P2) c= (R1 before P1) concur (R2 before P2)

let R1, R2, P1, P2 be process of N; :: thesis: (R1 concur R2) before (P1 concur P2) c= (R1 before P1) concur (R2 before P2)

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (R1 concur R2) before (P1 concur P2) or x in (R1 before P1) concur (R2 before P2) )

assume x in (R1 concur R2) before (P1 concur P2) ; :: thesis: x in (R1 before P1) concur (R2 before P2)

then consider C1, C2 being firing-sequence of N such that

A1: x = C1 ^ C2 and

A2: C1 in R1 concur R2 and

A3: C2 in P1 concur P2 ;

consider C3 being firing-sequence of N such that

A4: C1 = C3 and

A5: ex q1, q2 being FinSubsequence st

( C3 = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 & Seq q2 in R2 ) by A2;

consider q1, q2 being FinSubsequence such that

A6: C3 = q1 \/ q2 and

A7: q1 misses q2 and

A8: Seq q1 in R1 and

A9: Seq q2 in R2 by A5;

consider C4 being firing-sequence of N such that

A10: C2 = C4 and

A11: ex q3, q4 being FinSubsequence st

( C4 = q3 \/ q4 & q3 misses q4 & Seq q3 in P1 & Seq q4 in P2 ) by A3;

consider q3, q4 being FinSubsequence such that

A12: C4 = q3 \/ q4 and

A13: q3 misses q4 and

A14: Seq q3 in P1 and

A15: Seq q4 in P2 by A11;

reconsider C = C1 ^ C2 as firing-sequence of N ;

reconsider q5 = (len C1) Shift q3, q6 = (len C1) Shift q4 as FinSubsequence ;

A16: q1 c= C1 by A4, A6, XBOOLE_1:7;

A17: q2 c= C1 by A4, A6, XBOOLE_1:7;

A18: q3 c= C2 by A10, A12, XBOOLE_1:7;

A19: q4 c= C2 by A10, A12, XBOOLE_1:7;

A20: C1 c= C1 ^ C2 by FINSEQ_6:10;

then A21: q1 c= C1 ^ C2 by A16;

A22: q2 c= C1 ^ C2 by A17, A20;

reconsider ss = C2 as FinSubsequence ;

A23: q5 c= (len C1) Shift ss by A10, A12, VALUED_1:52, XBOOLE_1:7;

A24: q6 c= (len C1) Shift ss by A10, A12, VALUED_1:52, XBOOLE_1:7;

A25: (len C1) Shift C2 c= C1 ^ C2 by VALUED_1:53;

then A26: q5 c= C1 ^ C2 by A23;

A27: q6 c= C1 ^ C2 by A24, A25;

A28: dom q1 misses dom q5 by A16, A21, A26, Lm3, FUNCT_1:112;

dom q2 misses dom q6 by A17, A22, A27, Lm3, FUNCT_1:112;

then reconsider ss1 = q1 \/ q5, ss2 = q2 \/ q6 as Function by A28, GRFUNC_1:13;

A29: dom C = Seg (len C) by FINSEQ_1:def 3;

A30: dom ss1 c= dom C by A16, A18, Lm2;

dom ss2 c= dom C by A17, A19, Lm2;

then reconsider ss1 = ss1, ss2 = ss2 as FinSubsequence by A29, A30, FINSEQ_1:def 12;

A31: ss1 \/ ss2 = ((q1 \/ ((len C1) Shift q3)) \/ q2) \/ ((len C1) Shift q4) by XBOOLE_1:4

.= ((q1 \/ q2) \/ ((len C1) Shift q3)) \/ ((len C1) Shift q4) by XBOOLE_1:4

.= C1 \/ (((len C1) Shift q3) \/ ((len C1) Shift q4)) by A4, A6, XBOOLE_1:4

.= C1 \/ ((len C1) Shift C2) by A10, A12, A13, VALUED_1:55

.= C by VALUED_1:49 ;

A32: ss1 /\ q2 = (q1 /\ q2) \/ (((len C1) Shift q3) /\ q2) by XBOOLE_1:23;

ss1 /\ ((len C1) Shift q4) = (q1 /\ ((len C1) Shift q4)) \/ (((len C1) Shift q3) /\ ((len C1) Shift q4)) by XBOOLE_1:23;

then A33: ss1 /\ ss2 = ((q1 /\ q2) \/ (((len C1) Shift q3) /\ q2)) \/ ((q1 /\ ((len C1) Shift q4)) \/ (((len C1) Shift q3) /\ ((len C1) Shift q4))) by A32, XBOOLE_1:23;

A34: q1 /\ q2 = {} by A7;

A35: (len C1) Shift q3 misses q2 by A4, A6, Lm3, XBOOLE_1:7;

A36: q1 misses (len C1) Shift q4 by A4, A6, Lm3, XBOOLE_1:7;

A37: ((len C1) Shift q3) /\ q2 = {} by A35;

A38: q1 /\ ((len C1) Shift q4) = {} by A36;

dom q3 misses dom q4 by A13, A18, A19, FUNCT_1:112;

then dom ((len C1) Shift q3) misses dom ((len C1) Shift q4) by VALUED_1:54;

then (len C1) Shift q3 misses (len C1) Shift q4 by RELAT_1:179;

then ss1 /\ ss2 = {} by A33, A34, A37, A38;

then A39: ss1 misses ss2 ;

A40: ex ss3 being FinSubsequence st

( ss3 = ss1 & (Seq q1) ^ (Seq q3) = Seq ss3 ) by A16, A18, VALUED_1:64;

A41: ex ss4 being FinSubsequence st

( ss4 = ss2 & (Seq q2) ^ (Seq q4) = Seq ss4 ) by A17, A19, VALUED_1:64;

A42: Seq ss1 in R1 before P1 by A8, A14, A40;

Seq ss2 in R2 before P2 by A9, A15, A41;

hence x in (R1 before P1) concur (R2 before P2) by A1, A31, A39, A42; :: thesis: verum

for R1, R2, P1, P2 being process of N holds (R1 concur R2) before (P1 concur P2) c= (R1 before P1) concur (R2 before P2)

let N be Petri_net of P; :: thesis: for R1, R2, P1, P2 being process of N holds (R1 concur R2) before (P1 concur P2) c= (R1 before P1) concur (R2 before P2)

let R1, R2, P1, P2 be process of N; :: thesis: (R1 concur R2) before (P1 concur P2) c= (R1 before P1) concur (R2 before P2)

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (R1 concur R2) before (P1 concur P2) or x in (R1 before P1) concur (R2 before P2) )

assume x in (R1 concur R2) before (P1 concur P2) ; :: thesis: x in (R1 before P1) concur (R2 before P2)

then consider C1, C2 being firing-sequence of N such that

A1: x = C1 ^ C2 and

A2: C1 in R1 concur R2 and

A3: C2 in P1 concur P2 ;

consider C3 being firing-sequence of N such that

A4: C1 = C3 and

A5: ex q1, q2 being FinSubsequence st

( C3 = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 & Seq q2 in R2 ) by A2;

consider q1, q2 being FinSubsequence such that

A6: C3 = q1 \/ q2 and

A7: q1 misses q2 and

A8: Seq q1 in R1 and

A9: Seq q2 in R2 by A5;

consider C4 being firing-sequence of N such that

A10: C2 = C4 and

A11: ex q3, q4 being FinSubsequence st

( C4 = q3 \/ q4 & q3 misses q4 & Seq q3 in P1 & Seq q4 in P2 ) by A3;

consider q3, q4 being FinSubsequence such that

A12: C4 = q3 \/ q4 and

A13: q3 misses q4 and

A14: Seq q3 in P1 and

A15: Seq q4 in P2 by A11;

reconsider C = C1 ^ C2 as firing-sequence of N ;

reconsider q5 = (len C1) Shift q3, q6 = (len C1) Shift q4 as FinSubsequence ;

A16: q1 c= C1 by A4, A6, XBOOLE_1:7;

A17: q2 c= C1 by A4, A6, XBOOLE_1:7;

A18: q3 c= C2 by A10, A12, XBOOLE_1:7;

A19: q4 c= C2 by A10, A12, XBOOLE_1:7;

A20: C1 c= C1 ^ C2 by FINSEQ_6:10;

then A21: q1 c= C1 ^ C2 by A16;

A22: q2 c= C1 ^ C2 by A17, A20;

reconsider ss = C2 as FinSubsequence ;

A23: q5 c= (len C1) Shift ss by A10, A12, VALUED_1:52, XBOOLE_1:7;

A24: q6 c= (len C1) Shift ss by A10, A12, VALUED_1:52, XBOOLE_1:7;

A25: (len C1) Shift C2 c= C1 ^ C2 by VALUED_1:53;

then A26: q5 c= C1 ^ C2 by A23;

A27: q6 c= C1 ^ C2 by A24, A25;

A28: dom q1 misses dom q5 by A16, A21, A26, Lm3, FUNCT_1:112;

dom q2 misses dom q6 by A17, A22, A27, Lm3, FUNCT_1:112;

then reconsider ss1 = q1 \/ q5, ss2 = q2 \/ q6 as Function by A28, GRFUNC_1:13;

A29: dom C = Seg (len C) by FINSEQ_1:def 3;

A30: dom ss1 c= dom C by A16, A18, Lm2;

dom ss2 c= dom C by A17, A19, Lm2;

then reconsider ss1 = ss1, ss2 = ss2 as FinSubsequence by A29, A30, FINSEQ_1:def 12;

A31: ss1 \/ ss2 = ((q1 \/ ((len C1) Shift q3)) \/ q2) \/ ((len C1) Shift q4) by XBOOLE_1:4

.= ((q1 \/ q2) \/ ((len C1) Shift q3)) \/ ((len C1) Shift q4) by XBOOLE_1:4

.= C1 \/ (((len C1) Shift q3) \/ ((len C1) Shift q4)) by A4, A6, XBOOLE_1:4

.= C1 \/ ((len C1) Shift C2) by A10, A12, A13, VALUED_1:55

.= C by VALUED_1:49 ;

A32: ss1 /\ q2 = (q1 /\ q2) \/ (((len C1) Shift q3) /\ q2) by XBOOLE_1:23;

ss1 /\ ((len C1) Shift q4) = (q1 /\ ((len C1) Shift q4)) \/ (((len C1) Shift q3) /\ ((len C1) Shift q4)) by XBOOLE_1:23;

then A33: ss1 /\ ss2 = ((q1 /\ q2) \/ (((len C1) Shift q3) /\ q2)) \/ ((q1 /\ ((len C1) Shift q4)) \/ (((len C1) Shift q3) /\ ((len C1) Shift q4))) by A32, XBOOLE_1:23;

A34: q1 /\ q2 = {} by A7;

A35: (len C1) Shift q3 misses q2 by A4, A6, Lm3, XBOOLE_1:7;

A36: q1 misses (len C1) Shift q4 by A4, A6, Lm3, XBOOLE_1:7;

A37: ((len C1) Shift q3) /\ q2 = {} by A35;

A38: q1 /\ ((len C1) Shift q4) = {} by A36;

dom q3 misses dom q4 by A13, A18, A19, FUNCT_1:112;

then dom ((len C1) Shift q3) misses dom ((len C1) Shift q4) by VALUED_1:54;

then (len C1) Shift q3 misses (len C1) Shift q4 by RELAT_1:179;

then ss1 /\ ss2 = {} by A33, A34, A37, A38;

then A39: ss1 misses ss2 ;

A40: ex ss3 being FinSubsequence st

( ss3 = ss1 & (Seq q1) ^ (Seq q3) = Seq ss3 ) by A16, A18, VALUED_1:64;

A41: ex ss4 being FinSubsequence st

( ss4 = ss2 & (Seq q2) ^ (Seq q4) = Seq ss4 ) by A17, A19, VALUED_1:64;

A42: Seq ss1 in R1 before P1 by A8, A14, A40;

Seq ss2 in R2 before P2 by A9, A15, A41;

hence x in (R1 before P1) concur (R2 before P2) by A1, A31, A39, A42; :: thesis: verum