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

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

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

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

then
i < len dct
by XXREAL_0:1, T5;
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 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

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

then
i + 1 < len dct
by XXREAL_0:1, H4;
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 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

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