theorem :: PNPROC_1:19

for P being set
for m being marking of P
for t1, t2 being transition of P st (Pre t1) + (Pre t2) c= m holds
fire (t2,(fire (t1,m))) = (((m - (Pre t1)) - (Pre t2)) + (Post t1)) + (Post t2)