let P be set ; 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; 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; (R1 concur R2) before (P1 concur P2) c= (R1 before P1) concur (R2 before P2)
let x be object ; TARSKI:def 3 ( 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)
; 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; verum