:: deftheorem Def16Sub defines Ptr_Sub PETRI_3:def 13 :
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
for D being thin_cylinder of the ColoredSet of CPN, *' {t}
for ColD being color-threshold of D
for p being Element of CPN st t is_firable_on m,ColD holds
for b₇ being Function of the ColoredSet of CPN,NAT holds
( b₇ = Ptr_Sub (ColD,m,p) iff for x being Element of the ColoredSet of CPN holds
( ( p in loc D & x = ColD . p implies b₇ . x = ((m . p) . x) - 1 ) & ( ( not p in loc D or not x = ColD . p ) implies b₇ . x = (m . p) . x ) ) );