let fs be FinSequence of places_and_trans_of PetriNet; :: thesis: ( fs = <*0,1,0*> implies fs is directed_path_like )
assume L1: fs = <*0,1,0*> ; :: thesis: fs is directed_path_like
A12: ( fs . 1 = 0 & fs . 2 = 1 & fs . 3 = 0 ) by L1;
set N = PetriNet ;
thus fs is directed_path_like :: thesis: verum

proof

2 mod 2 = 0 by NAT_D:25;
then L3: (2 + 1) mod 2 = 1 by NAT_D:16;

L4: now :: thesis: for i being Nat st i mod 2 = 1 & i + 1 < len fs holds
( [(fs . i),(fs . (i + 1))] in the S-T_Arcs of PetriNet & [(fs . (i + 1)),(fs . (i + 2))] in the T-S_Arcs of PetriNet )

let i be Nat; :: thesis: ( i mod 2 = 1 & i + 1 < len fs implies ( [(fs . i),(fs . (i + 1))] in the S-T_Arcs of PetriNet & [(fs . (i + 1)),(fs . (i + 2))] in the T-S_Arcs of PetriNet ) )
assume A16: ( i mod 2 = 1 & i + 1 < len fs ) ; :: thesis: ( [(fs . i),(fs . (i + 1))] in the S-T_Arcs of PetriNet & [(fs . (i + 1)),(fs . (i + 2))] in the T-S_Arcs of PetriNet )
0 mod 2 = 0 by NAT_D:26;
then 0 < i by A16;
then A17: 0 + 1 <= i by NAT_1:13;

now :: thesis: not 1 < i

assume 1 < i ; :: thesis: contradiction
then 1 + 1 <= i by NAT_1:13;
then 2 + 1 <= i + 1 by XREAL_1:6;
hence contradiction by A16, FINSEQ_1:45, L1; :: thesis: verum

end;

then A11: i = 1 by XXREAL_0:1, A17;
A15: ( 0 in {0} & 1 in {1} ) by TARSKI:def 1;
thus ( [(fs . i),(fs . (i + 1))] in the S-T_Arcs of PetriNet & [(fs . (i + 1)),(fs . (i + 2))] in the T-S_Arcs of PetriNet ) by A11, A12, ZFMISC_1:def 2, A15; :: thesis: verum

end;

fs . (len fs) = 0 by A12, FINSEQ_1:45, L1;
hence fs is directed_path_like by FINSEQ_1:45, L1, L3, L4, TARSKI:def 1; :: thesis: verum

end;