:: deftheorem defines num_marks PETRI_DF:def 6 :
for N being PT_net_Str
for P being finite Subset of N
for M0 being marking of N holds num_marks (P,M0) = Sum the Enumeration of M0,P;