:: deftheorem Def5 defines Firing BOOLMARK:def 5 :

for PTN being Petri_net

for M0 being Boolean_marking of PTN

for Q being FinSequence of the carrier' of PTN

for b_{4} being Boolean_marking of PTN holds

( ( Q = {} implies ( b_{4} = Firing (Q,M0) iff b_{4} = M0 ) ) & ( not Q = {} implies ( b_{4} = Firing (Q,M0) iff ex M being FinSequence of Bool_marks_of PTN st

( len Q = len M & b_{4} = 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)) ) ) ) ) );

for PTN being Petri_net

for M0 being Boolean_marking of PTN

for Q being FinSequence of the carrier' of PTN

for b

( ( Q = {} implies ( b

( len Q = len M & b

M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) ) ) );