:: deftheorem defines firable_set_on PETRI_3:def 12 :
for CPN being with-nontrivial-ColoredSet Colored-PT-net
for m being colored-state of CPN
for t being Element of the carrier' of CPN holds firable_set_on (m,t) = { D where D is thin_cylinder of the ColoredSet of CPN, *' {t} : ex ColD being color-threshold of D st t is_firable_on m,ColD } ;