:: deftheorem Def16Add defines Ptr_Add PETRI_3:def 14 :
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
for b₇ being Function of the ColoredSet of CPN,NAT holds
( b₇ = Ptr_Add (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 ) ) );