let fs be FinSequence of places_and_trans_of PetriNet; ( fs = <*0,1,0*> implies fs is directed_path_like )
assume L1:
fs = <*0,1,0*>
; 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
verumproof
2
mod 2
= 0
by NAT_D:25;
then L3:
(2 + 1) mod 2
= 1
by NAT_D:16;
L4:
now 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;
( 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 )
;
( [(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;
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;
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;
verum
end;