let G be non void Graph; :: thesis: for c being non empty directed Chain of G st c is cyclic holds
for n being Element of NAT ex ch being directed Chain of G st
( len ch = n & ch ^ c is non empty directed Chain of G )
let c be non empty directed Chain of G; :: thesis: ( c is cyclic implies for n being Element of NAT ex ch being directed Chain of G st
( len ch = n & ch ^ c is non empty directed Chain of G ) )
assume A1:
c is cyclic
; :: thesis: for n being Element of NAT ex ch being directed Chain of G st
( len ch = n & ch ^ c is non empty directed Chain of G )
c is FinSequence of the carrier' of G
by Def1;
then A2:
rng c c= the carrier' of G
by FINSEQ_1:def 4;
defpred S1[ Element of NAT ] means ex ch being directed Chain of G st
( rng ch c= rng c & len ch = $1 & ch ^ c is non empty directed Chain of G );
A3:
S1[ 0 ]
A4:
for i being Element of NAT st S1[i] holds
S1[i + 1]
proof
let n be
Element of
NAT ;
:: thesis: ( S1[n] implies S1[n + 1] )
given ch being
directed Chain of
G such that A5:
(
rng ch c= rng c &
len ch = n &
ch ^ c is non
empty directed Chain of
G )
;
:: thesis: S1[n + 1]
len c in dom c
by FINSEQ_5:6;
then A6:
c . (len c) in rng c
by FUNCT_1:def 5;
then reconsider clc =
c . (len c) as
Element of the
carrier' of
G by A2;
reconsider ch' =
<*clc*> as
directed Chain of
G by Th5;
A7:
len ch' = 1
by FINSEQ_1:56;
A8:
rng ch' = {(c . (len c))}
by FINSEQ_1:55;
then A9:
rng ch' c= rng c
by A6, ZFMISC_1:37;
per cases
( n = 0 or n <> 0 )
;
suppose
n <> 0
;
:: thesis: S1[n + 1]then A11:
not
ch is
empty
by A5;
then
1
in dom ch
by FINSEQ_5:6;
then
ch . 1
in rng ch
by FUNCT_1:def 5;
then consider i being
Nat such that A12:
(
i in dom c &
c . i = ch . 1 )
by A5, FINSEQ_2:11;
A13:
( 1
<= i &
i <= len c )
by A12, FINSEQ_3:27;
now per cases
( i = 1 or i <> 1 )
;
suppose A14:
i = 1
;
:: thesis: ex ch1 being directed Chain of G st
( rng ch1 c= rng c & len ch1 = n + 1 & ch1 ^ c is non empty directed Chain of G )set vsch' =
vertex-seq ch';
vertex-seq ch' = <*(the Source of G . clc),(the Target of G . clc)*>
by Th7;
then A15:
(vertex-seq ch') . ((len ch') + 1) =
the
Target of
G . clc
by A7, FINSEQ_1:61
.=
(vertex-seq c) . ((len c) + 1)
by Th14
.=
(vertex-seq c) . 1
by A1, Th17
.=
the
Source of
G . (ch . 1)
by A12, A14, GRAPH_2:def 11
.=
(vertex-seq ch) . 1
by A11, GRAPH_2:def 11
;
reconsider ch1 =
ch' ^ ch as
directed Chain of
G by A11, A15, Th15;
take ch1 =
ch1;
:: thesis: ( rng ch1 c= rng c & len ch1 = n + 1 & ch1 ^ c is non empty directed Chain of G )
rng ch1 = (rng ch') \/ (rng ch)
by FINSEQ_1:44;
hence
rng ch1 c= rng c
by A5, A9, XBOOLE_1:8;
:: thesis: ( len ch1 = n + 1 & ch1 ^ c is non empty directed Chain of G )thus
len ch1 = n + 1
by A5, A7, FINSEQ_1:35;
:: thesis: ch1 ^ c is non empty directed Chain of G(vertex-seq ch1) . ((len ch1) + 1) =
(vertex-seq ch) . ((len ch) + 1)
by A11, Th16
.=
(vertex-seq c) . 1
by A5, A11, Th15
;
hence
ch1 ^ c is non
empty directed Chain of
G
by Th15;
:: thesis: verum end; suppose
i <> 1
;
:: thesis: ex ch1 being directed Chain of G st
( rng ch1 c= rng c & len ch1 = n + 1 & ch1 ^ c is non empty directed Chain of G )then
1
< i
by A13, XXREAL_0:1;
then
1
+ 1
<= i
by NAT_1:13;
then consider k being
Element of
NAT such that A17:
( 1
<= k &
k < len c &
i = k + 1 )
by A13, GRAPH_2:1;
k in dom c
by A17, FINSEQ_3:27;
then A18:
c . k in rng c
by FUNCT_1:def 5;
then reconsider ck =
c . k as
Element of the
carrier' of
G by A2;
reconsider ch' =
<*ck*> as
directed Chain of
G by Th5;
A19:
len ch' = 1
by FINSEQ_1:56;
rng ch' = {(c . k)}
by FINSEQ_1:55;
then A20:
rng ch' c= rng c
by A18, ZFMISC_1:37;
set vsch' =
vertex-seq ch';
vertex-seq ch' = <*(the Source of G . ck),(the Target of G . ck)*>
by Th7;
then A21:
(vertex-seq ch') . ((len ch') + 1) =
the
Target of
G . ck
by A19, FINSEQ_1:61
.=
the
Source of
G . (ch . 1)
by A12, A17, GRAPH_1:def 13
.=
(vertex-seq ch) . 1
by A11, GRAPH_2:def 11
;
reconsider ch1 =
ch' ^ ch as
directed Chain of
G by A11, A21, Th15;
take ch1 =
ch1;
:: thesis: ( rng ch1 c= rng c & len ch1 = n + 1 & ch1 ^ c is non empty directed Chain of G )
rng ch1 = (rng ch') \/ (rng ch)
by FINSEQ_1:44;
hence
rng ch1 c= rng c
by A5, A20, XBOOLE_1:8;
:: thesis: ( len ch1 = n + 1 & ch1 ^ c is non empty directed Chain of G )thus
len ch1 = n + 1
by A5, A19, FINSEQ_1:35;
:: thesis: ch1 ^ c is non empty directed Chain of G(vertex-seq ch1) . ((len ch1) + 1) =
(vertex-seq ch) . ((len ch) + 1)
by A11, Th16
.=
(vertex-seq c) . 1
by A5, A11, Th15
;
hence
ch1 ^ c is non
empty directed Chain of
G
by Th15;
:: thesis: verum end; hence
S1[
n + 1]
;
:: thesis: verum end;
end;
A23:
for n being Element of NAT holds S1[n]
from NAT_1:sch 1(A3, A4);
let n be Element of NAT ; :: thesis: ex ch being directed Chain of G st
( len ch = n & ch ^ c is non empty directed Chain of G )
ex ch being directed Chain of G st
( rng ch c= rng c & len ch = n & ch ^ c is non empty directed Chain of G )
by A23;
hence
ex ch being directed Chain of G st
( len ch = n & ch ^ c is non empty directed Chain of G )
; :: thesis: verum