:: deftheorem defines is_firable_at PETRI_DF:def 11 :
for PTN being Petri_net
for M0 being marking of PTN
for t being transition of PTN holds
( t is_firable_at M0 iff for m being Nat st m in M0 .: (*' {t}) holds
m > 0 );