:: deftheorem defines is_Cell-Petri-nets PETRI_3:def 8 :
for I being non trivial finite set
for CPNT being Colored-PT-net-Family of I
for N being Function of I,(bool (rng CPNT))
for O being connecting-mapping of CPNT holds
( N,O is_Cell-Petri-nets iff for i being Element of I holds N . i = { (CPNT . j) where j is Element of I : ( j <> i & ex t being transition of (CPNT . i) ex s being object st [t,s] in O . [i,j] ) } );