:: deftheorem defines is_firable_on BOOLMARK:def 4 :

for PTN being Petri_net

for M0 being Boolean_marking of PTN

for Q being FinSequence of the carrier' of PTN holds

( Q is_firable_on M0 iff ( Q = {} or ex M being FinSequence of Bool_marks_of PTN st

( len Q = len M & Q /. 1 is_firable_on M0 & M /. 1 = Firing ((Q /. 1),M0) & ( for i being Element of NAT st i < len Q & i > 0 holds

( Q /. (i + 1) is_firable_on M /. i & 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 holds

( Q is_firable_on M0 iff ( Q = {} or ex M being FinSequence of Bool_marks_of PTN st

( len Q = len M & Q /. 1 is_firable_on M0 & M /. 1 = Firing ((Q /. 1),M0) & ( for i being Element of NAT st i < len Q & i > 0 holds

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