:: deftheorem Def11 defines Colored-PT-net-like PETRI_2:def 11 :
for CPNT being Colored_Petri_net holds
( CPNT is Colored-PT-net-like iff ( dom the firing-rule of CPNT c= the carrier' of CPNT \ (Outbds CPNT) & ( for t being transition of CPNT st t in dom the firing-rule of CPNT holds
ex CS being non empty Subset of the ColoredSet of CPNT ex I being Subset of (*' {t}) ex O being Subset of ({t} *') st the firing-rule of CPNT . t is Function of (thin_cylinders (CS,I)),(thin_cylinders (CS,O)) ) ) );