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 set ; :: 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 & C1 in R1 concur R2 & C2 in P1 concur P2 ) ;
consider C3 being firing-sequence of N such that
A2: ( C1 = C3 & ex q1, q2 being FinSubsequence st
( C3 = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 & Seq q2 in R2 ) ) by A1;
consider q1, q2 being FinSubsequence such that
A3: ( C3 = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 & Seq q2 in R2 ) by A2;
consider C4 being firing-sequence of N such that
A4: ( C2 = C4 & ex q3, q4 being FinSubsequence st
( C4 = q3 \/ q4 & q3 misses q4 & Seq q3 in P1 & Seq q4 in P2 ) ) by A1;
consider q3, q4 being FinSubsequence such that
A5: ( C4 = q3 \/ q4 & q3 misses q4 & Seq q3 in P1 & Seq q4 in P2 ) by A4;
reconsider C = C1 ^ C2 as firing-sequence of N ;
reconsider q5 = (len C1) Shift q3, q6 = (len C1) Shift q4 as FinSubsequence ;
A6: ( q1 c= C1 & q2 c= C1 & q3 c= C2 & q4 c= C2 ) by A2, A3, A4, A5, XBOOLE_1:7;
C1 c= C1 ^ C2 by FINSEQ_6:12;
then A7: ( q1 c= C1 ^ C2 & q2 c= C1 ^ C2 ) by A6, XBOOLE_1:1;
reconsider ss = C2 as FinSubsequence ;
A8: ( q5 c= (len C1) Shift ss & q6 c= (len C1) Shift ss ) by A4, A5, Th70, XBOOLE_1:7;
(len C1) Shift C2 c= C1 ^ C2 by Th71;
then ( q5 c= C1 ^ C2 & q6 c= C1 ^ C2 ) by A8, XBOOLE_1:1;
then ( dom q1 misses dom q5 & dom q2 misses dom q6 ) by A6, A7, Lm9, Th10;
then reconsider ss1 = q1 \/ q5, ss2 = q2 \/ q6 as Function by GRFUNC_1:31;
A9: dom C = Seg (len C) by FINSEQ_1:def 3;
( dom ss1 c= dom C & dom ss2 c= dom C ) by A6, Lm8;
then reconsider ss1 = ss1, ss2 = ss2 as FinSubsequence by A9, FINSEQ_1:def 12;
A10: 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 A2, A3, XBOOLE_1:4
.= C1 \/ ((len C1) Shift C2) by A4, A5, Th73
.= C by Th64 ;
A11: ss1 misses ss2

proof

( ss1 /\ q2 = (q1 /\ q2) \/ (((len C1) Shift q3) /\ q2) & ss1 /\ ((len C1) Shift q4) = (q1 /\ ((len C1) Shift q4)) \/ (((len C1) Shift q3) /\ ((len C1) Shift q4)) ) by XBOOLE_1:23;
then A12: ss1 /\ ss2 = ((q1 /\ q2) \/ (((len C1) Shift q3) /\ q2)) \/ ((q1 /\ ((len C1) Shift q4)) \/ (((len C1) Shift q3) /\ ((len C1) Shift q4))) by XBOOLE_1:23;
A13: q1 /\ q2 = {} by A3, XBOOLE_0:def 7;
( (len C1) Shift q3 misses q2 & q1 misses (len C1) Shift q4 ) by A2, A3, Lm9, XBOOLE_1:7;
then A14: ( ((len C1) Shift q3) /\ q2 = {} & q1 /\ ((len C1) Shift q4) = {} ) by XBOOLE_0:def 7;
dom q3 misses dom q4 by A5, A6, Th10;
then dom ((len C1) Shift q3) misses dom ((len C1) Shift q4) by Th72;
then (len C1) Shift q3 misses (len C1) Shift q4 by Th8;
hence ss1 /\ ss2 = {} by A12, A13, A14, XBOOLE_0:def 7; :: according to XBOOLE_0:def 7 :: thesis: verum

end;

consider ss3 being FinSubsequence such that
A15: ( ss3 = ss1 & (Seq q1) ^ (Seq q3) = Seq ss3 ) by A6, Th82;
consider ss4 being FinSubsequence such that
A16: ( ss4 = ss2 & (Seq q2) ^ (Seq q4) = Seq ss4 ) by A6, Th82;
A17: Seq ss1 in R1 before P1 by A3, A5, A15;
Seq ss2 in R2 before P2 by A3, A5, A16;
hence x in (R1 before P1) concur (R2 before P2) by A1, A10, A11, A17; :: thesis: verum