for Dftn being Decision_free_PT
for dct being Circuit_of_places_and_trans of Dftn
for M0 being marking of Dftn
for t being transition of Dftn holds num_marks ((places_of dct),M0) = num_marks ((places_of dct),(Firing (t,M0)))