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;

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;

end;

suppose F4:
( 1 = i or i = len dct )
; :: thesis: t in transitions_of dct

end;

per cases
( [p1,t] in the S-T_Arcs of Dftn or [t,p1] in the T-S_Arcs of Dftn )
by A6;

end;

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;[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

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;[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

suppose F41:
( 1 < i & i < len dct )
; :: thesis: t in transitions_of dct

end;

per cases
( [p1,t] in the S-T_Arcs of Dftn or [t,p1] in the T-S_Arcs of Dftn )
by A6;

end;

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;

[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;now :: thesis: not i + 1 = len dct

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

[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

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;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