let Dftn be With_directed_path Petri_net; :: thesis: for dct being directed_path_like FinSequence of places_and_trans_of Dftn holds [(dct . ((len dct) - 1)),(dct . (len dct))] in the T-S_Arcs of Dftn

let dct be directed_path_like FinSequence of places_and_trans_of Dftn; :: thesis: [(dct . ((len dct) - 1)),(dct . (len dct))] in the T-S_Arcs of Dftn

len dct >= 3 by Def5;

then reconsider ln2 = (len dct) - 2 as Element of NAT by NAT_1:21, XXREAL_0:2;

F8: 1 = (ln2 + 2) mod 2 by Def5

.= ((ln2 mod 2) + (2 mod 2)) mod 2 by NAT_D:66

.= ((ln2 mod 2) + 0) mod 2 by NAT_D:25

.= ln2 mod 2 by NAT_D:65 ;

(len dct) + (- 1) < len dct by XREAL_1:30;

then [(dct . (ln2 + 1)),(dct . (ln2 + 2))] in the T-S_Arcs of Dftn by Def5, F8;

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

let dct be directed_path_like FinSequence of places_and_trans_of Dftn; :: thesis: [(dct . ((len dct) - 1)),(dct . (len dct))] in the T-S_Arcs of Dftn

len dct >= 3 by Def5;

then reconsider ln2 = (len dct) - 2 as Element of NAT by NAT_1:21, XXREAL_0:2;

F8: 1 = (ln2 + 2) mod 2 by Def5

.= ((ln2 mod 2) + (2 mod 2)) mod 2 by NAT_D:66

.= ((ln2 mod 2) + 0) mod 2 by NAT_D:25

.= ln2 mod 2 by NAT_D:65 ;

(len dct) + (- 1) < len dct by XREAL_1:30;

then [(dct . (ln2 + 1)),(dct . (ln2 + 2))] in the T-S_Arcs of Dftn by Def5, F8;

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