:: deftheorem defines fire PNPROC_1:def 11 :
for P being set
for N being Petri_net of P
for C being firing-sequence of N
for m being marking of P holds fire (C,m) = (fire C) . m;