:: deftheorem Def7 defines fire PNPROC_1:def 7 :
for P being set
for m being marking of P
for t being transition of P holds
( ( Pre t c= m implies fire (t,m) = (m - (Pre t)) + (Post t) ) & ( not Pre t c= m implies fire (t,m) = m ) );