:: deftheorem defines concur PNPROC_1:def 13 :
for P being set
for N being Petri_net of P
for R1, R2 being process of N holds R1 concur R2 = { C where C is firing-sequence of N : ex q1, q2 being FinSubsequence st
( C = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 & Seq q2 in R2 ) } ;