:: deftheorem Def11 defines Firing PETRI_DF:def 12 :
for PTN being Petri_net
for M0 being marking of PTN
for t being transition of PTN
for b₄ being marking of PTN holds
( ( t is_firable_at M0 implies ( b₄ = Firing (t,M0) iff for s being place of PTN holds
( ( s in *' {t} & not s in {t} *' implies b₄ . s = (M0 . s) - 1 ) & ( s in {t} *' & not s in *' {t} implies b₄ . s = (M0 . s) + 1 ) & ( ( ( s in *' {t} & s in {t} *' ) or ( not s in *' {t} & not s in {t} *' ) ) implies b₄ . s = M0 . s ) ) ) ) & ( not t is_firable_at M0 implies ( b₄ = Firing (t,M0) iff b₄ = M0 ) ) );