let Dftn be Petri decision_free_like With_directed_path Petri_net; 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; 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; ( 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 ) )
; 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 F41:
( 1
< i &
i < len dct )
;
t in transitions_of dctper 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
;
t in transitions_of dctF40:
i + 1
<= len dct
by NAT_1:13, F41;
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
;
verum end; suppose B8a:
[t,p1] in the
T-S_Arcs of
Dftn
;
t in transitions_of dctF46:
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
;
verum end; end; end; end;