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