let Dftn be Petri decision_free_like With_directed_path Petri_net; :: thesis: for dct being directed_path_like FinSequence of places_and_trans_of Dftn
for t being transition of Dftn st dct is circular & ex p1 being place of Dftn st
( p1 in places_of dct & ( [p1,t] in the S-T_Arcs of Dftn or [t,p1] in the T-S_Arcs of Dftn ) ) holds
t in transitions_of dct
let dct be directed_path_like FinSequence of places_and_trans_of Dftn; :: thesis: for t being transition of Dftn st dct is circular & ex p1 being place of Dftn st
( p1 in places_of dct & ( [p1,t] in the S-T_Arcs of Dftn or [t,p1] in the T-S_Arcs of Dftn ) ) holds
t in transitions_of dct
let t be transition of Dftn; :: thesis: ( dct is circular & ex p1 being place of Dftn st
( p1 in places_of dct & ( [p1,t] in the S-T_Arcs of Dftn or [t,p1] in the T-S_Arcs of Dftn ) ) implies t in transitions_of dct )
set P = places_of dct;
assume that
L1: dct is circular and
L2: ex p1 being place of Dftn st
( p1 in places_of dct & ( [p1,t] in the S-T_Arcs of Dftn or [t,p1] in the T-S_Arcs of Dftn ) ) ; :: thesis: t in transitions_of dct
consider p1 being place of Dftn such that
A5: p1 in places_of dct and
A6: ( [p1,t] in the S-T_Arcs of Dftn or [t,p1] in the T-S_Arcs of Dftn ) by L2;
consider p1n being place of Dftn such that
A9: ( p1n = p1 & p1n in rng dct ) by A5;
consider i being object such that
A11: i in dom dct and
A12: dct . i = p1 by FUNCT_1:def 3, A9;
reconsider i = i as Element of NAT by A11;
E1: ( 1 <= i & i <= len dct ) by A11, FINSEQ_3:25;
E10: i mod 2 = 1 by Thc, A5, A11, A12;
F3: [(dct . 1),(dct . 2)] in the S-T_Arcs of Dftn by Thd;
H1: 3 <= len dct by Def5;
then G4: 2 <= len dct by XXREAL_0:2;
then F2: 2 in dom dct by FINSEQ_3:25;
F3a: [(dct . ((len dct) - 1)),(dct . (len dct))] in the T-S_Arcs of Dftn by The;
reconsider ln1 = (len dct) - 1 as Element of NAT by NAT_1:21, XXREAL_0:2, H1;
P2: 2 + (- 1) <= (len dct) + (- 1) by XREAL_1:6, G4;
(len dct) + (- 1) < len dct by XREAL_1:30;
then F2a: ln1 in dom dct by FINSEQ_3:25, P2;
per cases ( 1 = i or i = len dct or ( 1 < i & i < len dct ) ) by XXREAL_0:1, E1;
suppose F4: ( 1 = i or i = len dct ) ; :: thesis: t in transitions_of dct
per cases ( [p1,t] in the S-T_Arcs of Dftn or [t,p1] in the T-S_Arcs of Dftn ) by A6;
suppose F10: [p1,t] in the S-T_Arcs of Dftn ; :: thesis: t in transitions_of dct
reconsider t1 = dct . 2 as transition of Dftn by ZFMISC_1:87, F3;
[p1,t1] in the S-T_Arcs of Dftn by F3, Lm1, L1, A12, F4;
then t = t1 by Def1, F10;
then t in rng dct by FUNCT_1:3, F2;
hence t in transitions_of dct ; :: thesis: verum
end;
suppose F10a: [t,p1] in the T-S_Arcs of Dftn ; :: thesis: t in transitions_of dct
reconsider tn1 = dct . ((len dct) - 1) as transition of Dftn by ZFMISC_1:87, F3a;
[tn1,p1] in the T-S_Arcs of Dftn by F3a, Lm1, L1, A12, F4;
then tn1 = t by Def1, F10a;
then t in rng dct by FUNCT_1:3, F2a;
hence t in transitions_of dct ; :: thesis: verum
end;
end;
end;
suppose F41: ( 1 < i & i < len dct ) ; :: thesis: t in transitions_of dct
per cases ( [p1,t] in the S-T_Arcs of Dftn or [t,p1] in the T-S_Arcs of Dftn ) by A6;
suppose B8: [p1,t] in the S-T_Arcs of Dftn ; :: thesis: t in transitions_of dct
F40: i + 1 <= len dct by NAT_1:13, F41;
now :: thesis: not i + 1 = len dct
assume E24: i + 1 = len dct ; :: thesis: contradiction
i mod 2 = 2 - 1 by Thc, A5, A11, A12;
then (i + 1) mod 2 = 0 by NAT_D:69;
hence contradiction by Def5, E24; :: thesis: verum
end;
then E12: i + 1 < len dct by XXREAL_0:1, F40;
[p1,(dct . (i + 1))] in the S-T_Arcs of Dftn by A12, Def5, E10, E12;
then reconsider t1 = dct . (i + 1) as transition of Dftn by ZFMISC_1:87;
A20: i + 1 in dom dct by FINSEQ_3:25, NAT_1:11, F40;
[p1,t1] in the S-T_Arcs of Dftn by A12, Def5, E10, E12;
then t = t1 by Def1, B8;
then t in rng dct by FUNCT_1:3, A20;
hence t in transitions_of dct ; :: thesis: verum
end;
suppose B8a: [t,p1] in the T-S_Arcs of Dftn ; :: thesis: t in transitions_of dct
F46: 1 + 1 <= i by F41, NAT_1:13;
reconsider i1 = i - 2 as Element of NAT by NAT_1:21, F46;
P5: i + (- 1) < len dct by F41, XREAL_1:36;
1 = (i1 + 2) mod 2 by Thc, A5, A11, A12
.= ((i1 mod 2) + (2 mod 2)) mod 2 by NAT_D:66
.= ((i1 mod 2) + 0) mod 2 by NAT_D:25
.= i1 mod 2 by NAT_D:65 ;
then P8: [(dct . (i1 + 1)),(dct . (i1 + 2))] in the T-S_Arcs of Dftn by Def5, P5;
then reconsider t0 = dct . (i1 + 1) as transition of Dftn by ZFMISC_1:87;
2 + (- 1) <= i + (- 1) by XREAL_1:6, F46;
then P6: i1 + 1 in dom dct by FINSEQ_3:25, P5;
t0 = t by Def1, B8a, A12, P8;
then t in rng dct by FUNCT_1:3, P6;
hence t in transitions_of dct ; :: thesis: verum
end;
end;
end;
end;