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 FINSEQ_1:45, L1;

set N = PetriNet ;

thus fs is directed_path_like :: thesis: verum

assume L1: fs = <*0,1,0*> ; :: thesis: fs is directed_path_like

A12: ( fs . 1 = 0 & fs . 2 = 1 & fs . 3 = 0 ) by FINSEQ_1:45, 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;

hence fs is directed_path_like by FINSEQ_1:45, L1, L3, L4, TARSKI:def 1; :: thesis: verum

end;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 )

fs . (len fs) = 0
by A12, FINSEQ_1:45, L1;( [(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;

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;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

then A11:
i = 1
by XXREAL_0:1, A17;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 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

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

hence fs is directed_path_like by FINSEQ_1:45, L1, L3, L4, TARSKI:def 1; :: thesis: verum