:: deftheorem Defb defines Firing PETRI_DF:def 14 :
for PTN being Petri_net
for M0 being marking of PTN
for Q being FinSequence of the carrier' of PTN
for b₄ being marking of PTN holds
( ( Q = {} implies ( b₄ = Firing (Q,M0) iff b₄ = M0 ) ) & ( not Q = {} implies ( b₄ = Firing (Q,M0) iff ex M being FinSequence of nat_marks_of PTN st
( len Q = len M & b₄ = M /. (len M) & M /. 1 = Firing ((Q /. 1),M0) & ( for i being Nat st i < len Q & i > 0 holds
M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) ) ) );