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
i mod 2 = 0
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
i mod 2 = 0
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 i mod 2 = 0 )
assume that
T2: dct . i in transitions_of dct and
T4: i in dom dct ; :: thesis: i mod 2 = 0
L1: [(dct . ((len dct) - 1)),(dct . (len dct))] in the T-S_Arcs of Dftn by The;
consider t being transition of Dftn such that
T3: ( t = dct . i & t in rng dct ) by T2;
T5: ( 1 <= i & i <= len dct ) by T4, FINSEQ_3:25;
i <> len dct

proof

assume i = len dct ; :: thesis: contradiction
then dct . i in the carrier of Dftn by L1, ZFMISC_1:87;
hence contradiction by NET_1:def 2, XBOOLE_0:3, T3; :: thesis: verum

end;

then i < len dct by XXREAL_0:1, T5;
then H4: i + 1 <= len dct by NAT_1:13;
assume i mod 2 <> 0 ; :: thesis: contradiction
then H1: i mod 2 = 2 - 1 by NAT_D:12;
i + 1 <> len dct

proof

assume H6: i + 1 = len dct ; :: thesis: contradiction
then reconsider p = dct . (i + 1) as place of Dftn by L1, ZFMISC_1:87;
1 <= 1 + i by NAT_1:11;
then H5: i + 1 in dom dct by FINSEQ_3:25, H6;
then p in rng dct by FUNCT_1:3;
then p in places_of dct ;
then (i + 1) mod 2 = 1 by Thc, H5;
hence contradiction by NAT_D:69, H1; :: thesis: verum

end;

then i + 1 < len dct by XXREAL_0:1, H4;
then [(dct . i),(dct . (i + 1))] in the S-T_Arcs of Dftn by Def5, H1;
then dct . i in the carrier of Dftn by ZFMISC_1:87;
hence contradiction by XBOOLE_0:3, T3, NET_1:def 2; :: thesis: verum