for PTN being Petri_net
for M0 being marking of PTN
for t being transition of PTN holds Firing (t,M0) = Firing (<*t*>,M0)