:: deftheorem defines is_firable_on BOOLMARK:def 2 :
for PTN being Petri_net
for M0 being Boolean_marking of PTN
for t being transition of PTN holds
( t is_firable_on M0 iff M0 .: (*' {t}) c= {TRUE} );