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 & i in dom dct holds

i mod 2 = 1

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 & i in dom dct holds

i mod 2 = 1

let dct be directed_path_like FinSequence of places_and_trans_of Dftn; :: thesis: ( dct . i in places_of dct & i in dom dct implies i mod 2 = 1 )

assume that

T2: dct . i in places_of dct and

T4: i in dom dct ; :: thesis: i mod 2 = 1

consider p being place of Dftn such that

T3: ( p = dct . i & p in rng dct ) by T2;

E1: ( 1 <= i & i <= len dct ) by T4, FINSEQ_3:25;

E41: ( i = len dct or i < len dct ) by XXREAL_0:1, E1;

i mod 2 = 1

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

i mod 2 = 1

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 & i in dom dct holds

i mod 2 = 1

let dct be directed_path_like FinSequence of places_and_trans_of Dftn; :: thesis: ( dct . i in places_of dct & i in dom dct implies i mod 2 = 1 )

assume that

T2: dct . i in places_of dct and

T4: i in dom dct ; :: thesis: i mod 2 = 1

consider p being place of Dftn such that

T3: ( p = dct . i & p in rng dct ) by T2;

E1: ( 1 <= i & i <= len dct ) by T4, FINSEQ_3:25;

E41: ( i = len dct or i < len dct ) by XXREAL_0:1, E1;

i mod 2 = 1

proof

hence
i mod 2 = 1
; :: thesis: verum
assume E6:
i mod 2 <> 1
; :: thesis: contradiction

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

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

then dct . (i1 + 1) in the carrier' of Dftn by ZFMISC_1:87;

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

end;reconsider i1 = i - 1 as Element of NAT by NAT_1:21, T4, FINSEQ_3:25;

now :: thesis: not i1 mod 2 = 0

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

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

hence contradiction by E6; :: thesis: verum

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

hence contradiction by E6; :: thesis: verum

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

then dct . (i1 + 1) in the carrier' of Dftn by ZFMISC_1:87;

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