:: deftheorem Def5 defines directed_path_like PETRI_DF:def 8 :
for PTN being Petri_net
for IT being FinSequence of places_and_trans_of PTN holds
( IT is directed_path_like iff ( len IT >= 3 & (len IT) mod 2 = 1 & ( for i being Nat st i mod 2 = 1 & i + 1 < len IT holds
( [(IT . i),(IT . (i + 1))] in the S-T_Arcs of PTN & [(IT . (i + 1)),(IT . (i + 2))] in the T-S_Arcs of PTN ) ) & IT . (len IT) in the carrier of PTN ) );