let P be set ; :: thesis: for N being Petri_net of P
for R1, R2 being process of N holds R1 before R2 c= R1 concur R2
let N be Petri_net of P; :: thesis: for R1, R2 being process of N holds R1 before R2 c= R1 concur R2
let R1, R2 be process of N; :: thesis: R1 before R2 c= R1 concur R2
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in R1 before R2 or x in R1 concur R2 )
assume A1: x in R1 before R2 ; :: thesis: x in R1 concur R2
then reconsider C = x as firing-sequence of N ;
consider C1, C2 being firing-sequence of N such that
A2: x = C1 ^ C2 and
A3: C1 in R1 and
A4: C2 in R2 by A1;
set q1 = C1;
set q2 = (len C1) Shift C2;
reconsider q1 = C1 as FinSequence ;
A5: C = q1 \/ ((len C1) Shift C2) by A2, Th64;
A6: q1 misses (len C1) Shift C2 by Th65;
A7: Seq q1 in R1 by A3, FINSEQ_3:116;
Seq ((len C1) Shift C2) in R2 by A4, Th61;
hence x in R1 concur R2 by A5, A6, A7; :: thesis: verum