:: deftheorem defines Firing BOOLMARK:def 3 :
for PTN being Petri_net
for M0 being Boolean_marking of PTN
for t being transition of PTN holds Firing (t,M0) = (M0 +* ((*' {t}) --> FALSE)) +* (({t} *') --> TRUE);