let i be Nat; :: thesis: for Dftn being Petri With_directed_path Petri_net

for dct being directed_path_like FinSequence of places_and_trans_of Dftn st dct . i in transitions_of dct & i in dom dct holds

( [(dct . (i - 1)),(dct . i)] in the S-T_Arcs of Dftn & [(dct . i),(dct . (i + 1))] in the T-S_Arcs of Dftn )

let Dftn be Petri With_directed_path Petri_net; :: thesis: for dct being directed_path_like FinSequence of places_and_trans_of Dftn st dct . i in transitions_of dct & i in dom dct holds

( [(dct . (i - 1)),(dct . i)] in the S-T_Arcs of Dftn & [(dct . i),(dct . (i + 1))] in the T-S_Arcs of Dftn )

let dct be directed_path_like FinSequence of places_and_trans_of Dftn; :: thesis: ( dct . i in transitions_of dct & i in dom dct implies ( [(dct . (i - 1)),(dct . i)] in the S-T_Arcs of Dftn & [(dct . i),(dct . (i + 1))] in the T-S_Arcs of Dftn ) )

assume H1: ( dct . i in transitions_of dct & i in dom dct ) ; :: thesis: ( [(dct . (i - 1)),(dct . i)] in the S-T_Arcs of Dftn & [(dct . i),(dct . (i + 1))] in the T-S_Arcs of Dftn )

L1: [(dct . ((len dct) - 1)),(dct . (len dct))] in the T-S_Arcs of Dftn by The;

reconsider im1 = i - 1 as Element of NAT by NAT_1:21, FINSEQ_3:25, H1;

consider t being transition of Dftn such that

H6: ( t = dct . i & t in rng dct ) by H1;

H4: ( 1 <= i & i <= len dct ) by FINSEQ_3:25, H1;

i <> len dct

hence [(dct . (i - 1)),(dct . i)] in the S-T_Arcs of Dftn by Def5, H2; :: thesis: [(dct . i),(dct . (i + 1))] in the T-S_Arcs of Dftn

[(dct . (im1 + 1)),(dct . (im1 + 2))] in the T-S_Arcs of Dftn by Def5, H2, H3;

hence [(dct . i),(dct . (i + 1))] in the T-S_Arcs of Dftn ; :: thesis: verum

for dct being directed_path_like FinSequence of places_and_trans_of Dftn st dct . i in transitions_of dct & i in dom dct holds

( [(dct . (i - 1)),(dct . i)] in the S-T_Arcs of Dftn & [(dct . i),(dct . (i + 1))] in the T-S_Arcs of Dftn )

let Dftn be Petri With_directed_path Petri_net; :: thesis: for dct being directed_path_like FinSequence of places_and_trans_of Dftn st dct . i in transitions_of dct & i in dom dct holds

( [(dct . (i - 1)),(dct . i)] in the S-T_Arcs of Dftn & [(dct . i),(dct . (i + 1))] in the T-S_Arcs of Dftn )

let dct be directed_path_like FinSequence of places_and_trans_of Dftn; :: thesis: ( dct . i in transitions_of dct & i in dom dct implies ( [(dct . (i - 1)),(dct . i)] in the S-T_Arcs of Dftn & [(dct . i),(dct . (i + 1))] in the T-S_Arcs of Dftn ) )

assume H1: ( dct . i in transitions_of dct & i in dom dct ) ; :: thesis: ( [(dct . (i - 1)),(dct . i)] in the S-T_Arcs of Dftn & [(dct . i),(dct . (i + 1))] in the T-S_Arcs of Dftn )

L1: [(dct . ((len dct) - 1)),(dct . (len dct))] in the T-S_Arcs of Dftn by The;

reconsider im1 = i - 1 as Element of NAT by NAT_1:21, FINSEQ_3:25, H1;

consider t being transition of Dftn such that

H6: ( t = dct . i & t in rng dct ) by H1;

H4: ( 1 <= i & i <= len dct ) by FINSEQ_3:25, H1;

now :: thesis: not im1 mod 2 = 0

then H2:
im1 mod 2 = 1
by NAT_D:12;assume
im1 mod 2 = 0
; :: thesis: contradiction

then (im1 + 1) mod 2 = 1 by NAT_D:16;

hence contradiction by Thcc, H1; :: thesis: verum

end;then (im1 + 1) mod 2 = 1 by NAT_D:16;

hence contradiction by Thcc, H1; :: thesis: verum

i <> len dct

proof

then H3:
im1 + 1 < len dct
by XXREAL_0:1, H4;
assume
i = len dct
; :: thesis: contradiction

then dct . i in the carrier of Dftn by L1, ZFMISC_1:87;

hence contradiction by H6, NET_1:def 2, XBOOLE_0:3; :: thesis: verum

end;then dct . i in the carrier of Dftn by L1, ZFMISC_1:87;

hence contradiction by H6, NET_1:def 2, XBOOLE_0:3; :: thesis: verum

hence [(dct . (i - 1)),(dct . i)] in the S-T_Arcs of Dftn by Def5, H2; :: thesis: [(dct . i),(dct . (i + 1))] in the T-S_Arcs of Dftn

[(dct . (im1 + 1)),(dct . (im1 + 2))] in the T-S_Arcs of Dftn by Def5, H2, H3;

hence [(dct . i),(dct . (i + 1))] in the T-S_Arcs of Dftn ; :: thesis: verum