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 places_of dct & 1 < i & i < len dct holds

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

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 places_of dct & 1 < i & i < len dct holds

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

let dct be directed_path_like FinSequence of places_and_trans_of Dftn; :: thesis: ( dct . i in places_of dct & 1 < i & i < len dct implies ( [(dct . (i - 2)),(dct . (i - 1))] in the S-T_Arcs of Dftn & [(dct . (i - 1)),(dct . i)] in the T-S_Arcs of Dftn & [(dct . i),(dct . (i + 1))] in the S-T_Arcs of Dftn & [(dct . (i + 1)),(dct . (i + 2))] in the T-S_Arcs of Dftn & 3 <= i ) )

assume H1: ( dct . i in places_of dct & 1 < i & i < len dct ) ; :: thesis: ( [(dct . (i - 2)),(dct . (i - 1))] in the S-T_Arcs of Dftn & [(dct . (i - 1)),(dct . i)] in the T-S_Arcs of Dftn & [(dct . i),(dct . (i + 1))] in the S-T_Arcs of Dftn & [(dct . (i + 1)),(dct . (i + 2))] in the T-S_Arcs of Dftn & 3 <= i )

then P1: i in dom dct by FINSEQ_3:25;

then H4: i mod 2 = 1 by Thc, H1;

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

L2: [(dct . 1),(dct . 2)] in the S-T_Arcs of Dftn by Thd;

consider p being place of Dftn such that

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

H8: 1 + 1 <= i by H1, NAT_1:13;

then reconsider im2 = i - 2 as Element of NAT by NAT_1:21;

P2: i - 1 < len dct by H1, XREAL_1:147;

then [(dct . im2),(dct . (im2 + 1))] in the S-T_Arcs of Dftn by Def5, H2;

hence [(dct . (i - 2)),(dct . (i - 1))] in the S-T_Arcs of Dftn ; :: thesis: ( [(dct . (i - 1)),(dct . i)] in the T-S_Arcs of Dftn & [(dct . i),(dct . (i + 1))] in the S-T_Arcs of Dftn & [(dct . (i + 1)),(dct . (i + 2))] in the T-S_Arcs of Dftn & 3 <= i )

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

hence [(dct . (i - 1)),(dct . i)] in the T-S_Arcs of Dftn ; :: thesis: ( [(dct . i),(dct . (i + 1))] in the S-T_Arcs of Dftn & [(dct . (i + 1)),(dct . (i + 2))] in the T-S_Arcs of Dftn & 3 <= i )

H9: i + 1 <= len dct by NAT_1:13, H1;

i + 1 <> len dct

hence [(dct . i),(dct . (i + 1))] in the S-T_Arcs of Dftn by Def5, H4; :: thesis: ( [(dct . (i + 1)),(dct . (i + 2))] in the T-S_Arcs of Dftn & 3 <= i )

thus [(dct . (i + 1)),(dct . (i + 2))] in the T-S_Arcs of Dftn by Def5, H5, H4; :: thesis: 3 <= i

2 <> i

then 2 + 1 <= i by NAT_1:13;

hence 3 <= i ; :: thesis: verum

for dct being directed_path_like FinSequence of places_and_trans_of Dftn st dct . i in places_of dct & 1 < i & i < len dct holds

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

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 places_of dct & 1 < i & i < len dct holds

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

let dct be directed_path_like FinSequence of places_and_trans_of Dftn; :: thesis: ( dct . i in places_of dct & 1 < i & i < len dct implies ( [(dct . (i - 2)),(dct . (i - 1))] in the S-T_Arcs of Dftn & [(dct . (i - 1)),(dct . i)] in the T-S_Arcs of Dftn & [(dct . i),(dct . (i + 1))] in the S-T_Arcs of Dftn & [(dct . (i + 1)),(dct . (i + 2))] in the T-S_Arcs of Dftn & 3 <= i ) )

assume H1: ( dct . i in places_of dct & 1 < i & i < len dct ) ; :: thesis: ( [(dct . (i - 2)),(dct . (i - 1))] in the S-T_Arcs of Dftn & [(dct . (i - 1)),(dct . i)] in the T-S_Arcs of Dftn & [(dct . i),(dct . (i + 1))] in the S-T_Arcs of Dftn & [(dct . (i + 1)),(dct . (i + 2))] in the T-S_Arcs of Dftn & 3 <= i )

then P1: i in dom dct by FINSEQ_3:25;

then H4: i mod 2 = 1 by Thc, H1;

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

L2: [(dct . 1),(dct . 2)] in the S-T_Arcs of Dftn by Thd;

consider p being place of Dftn such that

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

H8: 1 + 1 <= i by H1, NAT_1:13;

then reconsider im2 = i - 2 as Element of NAT by NAT_1:21;

now :: thesis: not im2 mod 2 = 0

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

then (im2 + 1) mod 2 = 1 mod 2 by NAT_D:17

.= 2 - 1 by NAT_D:14 ;

then ((im2 + 1) + 1) mod 2 = 0 by NAT_D:69;

hence contradiction by Thc, H1, P1; :: thesis: verum

end;then (im2 + 1) mod 2 = 1 mod 2 by NAT_D:17

.= 2 - 1 by NAT_D:14 ;

then ((im2 + 1) + 1) mod 2 = 0 by NAT_D:69;

hence contradiction by Thc, H1, P1; :: thesis: verum

P2: i - 1 < len dct by H1, XREAL_1:147;

then [(dct . im2),(dct . (im2 + 1))] in the S-T_Arcs of Dftn by Def5, H2;

hence [(dct . (i - 2)),(dct . (i - 1))] in the S-T_Arcs of Dftn ; :: thesis: ( [(dct . (i - 1)),(dct . i)] in the T-S_Arcs of Dftn & [(dct . i),(dct . (i + 1))] in the S-T_Arcs of Dftn & [(dct . (i + 1)),(dct . (i + 2))] in the T-S_Arcs of Dftn & 3 <= i )

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

hence [(dct . (i - 1)),(dct . i)] in the T-S_Arcs of Dftn ; :: thesis: ( [(dct . i),(dct . (i + 1))] in the S-T_Arcs of Dftn & [(dct . (i + 1)),(dct . (i + 2))] in the T-S_Arcs of Dftn & 3 <= i )

H9: i + 1 <= len dct by NAT_1:13, H1;

i + 1 <> len dct

proof

then H5:
i + 1 < len dct
by XXREAL_0:1, H9;
assume
i + 1 = len dct
; :: thesis: contradiction

then dct . ((i + 1) - 1) in the carrier' of Dftn by L1, ZFMISC_1:87;

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

end;then dct . ((i + 1) - 1) in the carrier' of Dftn by L1, ZFMISC_1:87;

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

hence [(dct . i),(dct . (i + 1))] in the S-T_Arcs of Dftn by Def5, H4; :: thesis: ( [(dct . (i + 1)),(dct . (i + 2))] in the T-S_Arcs of Dftn & 3 <= i )

thus [(dct . (i + 1)),(dct . (i + 2))] in the T-S_Arcs of Dftn by Def5, H5, H4; :: thesis: 3 <= i

2 <> i

proof

then
2 < i
by XXREAL_0:1, H8;
assume
i = 2
; :: thesis: contradiction

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

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

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

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

then 2 + 1 <= i by NAT_1:13;

hence 3 <= i ; :: thesis: verum