defpred S1[ Nat] means for G being _finite simple connected _Graph st G .order() = $1 holds
ex p being non empty Graph-yielding _finite simple connected FinSequence st
( p . 1 is _trivial & p . 1 is edgeless & p . (len p) = G & len p = G .order() & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v being object ex V being non empty finite set st
( v in (the_Vertices_of G) \ (the_Vertices_of (p . n)) & V c= the_Vertices_of (p . n) & p . (n + 1) is addAdjVertexAll of p . n,v,V ) ) );
A1:
S1[1]
proof
let G be
_finite simple connected _Graph;
( G .order() = 1 implies ex p being non empty Graph-yielding _finite simple connected FinSequence st
( p . 1 is _trivial & p . 1 is edgeless & p . (len p) = G & len p = G .order() & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v being object ex V being non empty finite set st
( v in (the_Vertices_of G) \ (the_Vertices_of (p . n)) & V c= the_Vertices_of (p . n) & p . (n + 1) is addAdjVertexAll of p . n,v,V ) ) ) )
assume A2:
G .order() = 1
;
ex p being non empty Graph-yielding _finite simple connected FinSequence st
( p . 1 is _trivial & p . 1 is edgeless & p . (len p) = G & len p = G .order() & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v being object ex V being non empty finite set st
( v in (the_Vertices_of G) \ (the_Vertices_of (p . n)) & V c= the_Vertices_of (p . n) & p . (n + 1) is addAdjVertexAll of p . n,v,V ) ) )
set p =
<*G*>;
take
<*G*>
;
( <*G*> . 1 is _trivial & <*G*> . 1 is edgeless & <*G*> . (len <*G*>) = G & len <*G*> = G .order() & ( for n being Element of dom <*G*> st n <= (len <*G*>) - 1 holds
ex v being object ex V being non empty finite set st
( v in (the_Vertices_of G) \ (the_Vertices_of (<*G*> . n)) & V c= the_Vertices_of (<*G*> . n) & <*G*> . (n + 1) is addAdjVertexAll of <*G*> . n,v,V ) ) )
G is
_trivial
by A2, GLIB_000:26;
hence
(
<*G*> . 1 is
_trivial &
<*G*> . 1 is
edgeless )
by FINSEQ_1:40;
( <*G*> . (len <*G*>) = G & len <*G*> = G .order() & ( for n being Element of dom <*G*> st n <= (len <*G*>) - 1 holds
ex v being object ex V being non empty finite set st
( v in (the_Vertices_of G) \ (the_Vertices_of (<*G*> . n)) & V c= the_Vertices_of (<*G*> . n) & <*G*> . (n + 1) is addAdjVertexAll of <*G*> . n,v,V ) ) )
thus <*G*> . (len <*G*>) =
<*G*> . 1
by FINSEQ_1:40
.=
G
by FINSEQ_1:40
;
( len <*G*> = G .order() & ( for n being Element of dom <*G*> st n <= (len <*G*>) - 1 holds
ex v being object ex V being non empty finite set st
( v in (the_Vertices_of G) \ (the_Vertices_of (<*G*> . n)) & V c= the_Vertices_of (<*G*> . n) & <*G*> . (n + 1) is addAdjVertexAll of <*G*> . n,v,V ) ) )
thus
len <*G*> = G .order()
by A2, FINSEQ_1:40;
for n being Element of dom <*G*> st n <= (len <*G*>) - 1 holds
ex v being object ex V being non empty finite set st
( v in (the_Vertices_of G) \ (the_Vertices_of (<*G*> . n)) & V c= the_Vertices_of (<*G*> . n) & <*G*> . (n + 1) is addAdjVertexAll of <*G*> . n,v,V )
let n be
Element of
dom <*G*>;
( n <= (len <*G*>) - 1 implies ex v being object ex V being non empty finite set st
( v in (the_Vertices_of G) \ (the_Vertices_of (<*G*> . n)) & V c= the_Vertices_of (<*G*> . n) & <*G*> . (n + 1) is addAdjVertexAll of <*G*> . n,v,V ) )
( 1
<= n &
n <= len <*G*> )
by FINSEQ_3:25;
then
( 1
<= n &
n <= 1 )
by FINSEQ_1:40;
then A3:
n = 1
by XXREAL_0:1;
assume
n <= (len <*G*>) - 1
;
ex v being object ex V being non empty finite set st
( v in (the_Vertices_of G) \ (the_Vertices_of (<*G*> . n)) & V c= the_Vertices_of (<*G*> . n) & <*G*> . (n + 1) is addAdjVertexAll of <*G*> . n,v,V )
then
n <= 1
- 1
by FINSEQ_1:40;
hence
ex
v being
object ex
V being non
empty finite set st
(
v in (the_Vertices_of G) \ (the_Vertices_of (<*G*> . n)) &
V c= the_Vertices_of (<*G*> . n) &
<*G*> . (n + 1) is
addAdjVertexAll of
<*G*> . n,
v,
V )
by A3;
verum
end;
A4:
for k being non zero Nat st S1[k] holds
S1[k + 1]
proof
let k be non
zero Nat;
( S1[k] implies S1[k + 1] )
assume A5:
S1[
k]
;
S1[k + 1]
let G be
_finite simple connected _Graph;
( G .order() = k + 1 implies ex p being non empty Graph-yielding _finite simple connected FinSequence st
( p . 1 is _trivial & p . 1 is edgeless & p . (len p) = G & len p = G .order() & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v being object ex V being non empty finite set st
( v in (the_Vertices_of G) \ (the_Vertices_of (p . n)) & V c= the_Vertices_of (p . n) & p . (n + 1) is addAdjVertexAll of p . n,v,V ) ) ) )
assume A6:
G .order() = k + 1
;
ex p being non empty Graph-yielding _finite simple connected FinSequence st
( p . 1 is _trivial & p . 1 is edgeless & p . (len p) = G & len p = G .order() & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v being object ex V being non empty finite set st
( v in (the_Vertices_of G) \ (the_Vertices_of (p . n)) & V c= the_Vertices_of (p . n) & p . (n + 1) is addAdjVertexAll of p . n,v,V ) ) )
A7:
not
G is
_trivial
then consider v9,
v0 being
Vertex of
G such that
(
v9 <> v0 & not
v9 is
cut-vertex )
and A8:
not
v0 is
cut-vertex
by GLIB_002:37;
set G2 = the
removeVertex of
G,
v0;
A9:
( the removeVertex of G,v0 .order()) + 1
= G .order()
by A7, GLIB_000:48;
then A10:
the
removeVertex of
G,
v0 .order() = k
by A6;
the
removeVertex of
G,
v0 is
connected
by A8, GLIB_002:36;
then consider p being non
empty Graph-yielding _finite simple connected FinSequence such that A11:
(
p . 1 is
_trivial &
p . 1 is
edgeless &
p . (len p) = the
removeVertex of
G,
v0 &
len p = the
removeVertex of
G,
v0 .order() )
and A12:
for
n being
Element of
dom p st
n <= (len p) - 1 holds
ex
v being
object ex
V being non
empty finite set st
(
v in (the_Vertices_of the removeVertex of G,v0) \ (the_Vertices_of (p . n)) &
V c= the_Vertices_of (p . n) &
p . (n + 1) is
addAdjVertexAll of
p . n,
v,
V )
by A5, A10;
set q =
p ^ <*G*>;
take
p ^ <*G*>
;
( (p ^ <*G*>) . 1 is _trivial & (p ^ <*G*>) . 1 is edgeless & (p ^ <*G*>) . (len (p ^ <*G*>)) = G & len (p ^ <*G*>) = G .order() & ( for n being Element of dom (p ^ <*G*>) st n <= (len (p ^ <*G*>)) - 1 holds
ex v being object ex V being non empty finite set st
( v in (the_Vertices_of G) \ (the_Vertices_of ((p ^ <*G*>) . n)) & V c= the_Vertices_of ((p ^ <*G*>) . n) & (p ^ <*G*>) . (n + 1) is addAdjVertexAll of (p ^ <*G*>) . n,v,V ) ) )
1
in dom p
by FINSEQ_5:6;
hence
(
(p ^ <*G*>) . 1 is
_trivial &
(p ^ <*G*>) . 1 is
edgeless )
by A11, FINSEQ_1:def 7;
( (p ^ <*G*>) . (len (p ^ <*G*>)) = G & len (p ^ <*G*>) = G .order() & ( for n being Element of dom (p ^ <*G*>) st n <= (len (p ^ <*G*>)) - 1 holds
ex v being object ex V being non empty finite set st
( v in (the_Vertices_of G) \ (the_Vertices_of ((p ^ <*G*>) . n)) & V c= the_Vertices_of ((p ^ <*G*>) . n) & (p ^ <*G*>) . (n + 1) is addAdjVertexAll of (p ^ <*G*>) . n,v,V ) ) )
A13:
len (p ^ <*G*>) =
(len p) + (len <*G*>)
by FINSEQ_1:22
.=
(len p) + 1
by FINSEQ_1:40
;
hence A14:
(p ^ <*G*>) . (len (p ^ <*G*>)) = G
by FINSEQ_1:42;
( len (p ^ <*G*>) = G .order() & ( for n being Element of dom (p ^ <*G*>) st n <= (len (p ^ <*G*>)) - 1 holds
ex v being object ex V being non empty finite set st
( v in (the_Vertices_of G) \ (the_Vertices_of ((p ^ <*G*>) . n)) & V c= the_Vertices_of ((p ^ <*G*>) . n) & (p ^ <*G*>) . (n + 1) is addAdjVertexAll of (p ^ <*G*>) . n,v,V ) ) )
thus
len (p ^ <*G*>) = G .order()
by A9, A11, A13;
for n being Element of dom (p ^ <*G*>) st n <= (len (p ^ <*G*>)) - 1 holds
ex v being object ex V being non empty finite set st
( v in (the_Vertices_of G) \ (the_Vertices_of ((p ^ <*G*>) . n)) & V c= the_Vertices_of ((p ^ <*G*>) . n) & (p ^ <*G*>) . (n + 1) is addAdjVertexAll of (p ^ <*G*>) . n,v,V )
let n be
Element of
dom (p ^ <*G*>);
( n <= (len (p ^ <*G*>)) - 1 implies ex v being object ex V being non empty finite set st
( v in (the_Vertices_of G) \ (the_Vertices_of ((p ^ <*G*>) . n)) & V c= the_Vertices_of ((p ^ <*G*>) . n) & (p ^ <*G*>) . (n + 1) is addAdjVertexAll of (p ^ <*G*>) . n,v,V ) )
assume
n <= (len (p ^ <*G*>)) - 1
;
ex v being object ex V being non empty finite set st
( v in (the_Vertices_of G) \ (the_Vertices_of ((p ^ <*G*>) . n)) & V c= the_Vertices_of ((p ^ <*G*>) . n) & (p ^ <*G*>) . (n + 1) is addAdjVertexAll of (p ^ <*G*>) . n,v,V )
per cases then
( n = (len (p ^ <*G*>)) - 1 or n <= (len p) - 1 )
by Lm12;
suppose A15:
n = (len (p ^ <*G*>)) - 1
;
ex v being object ex V being non empty finite set st
( v in (the_Vertices_of G) \ (the_Vertices_of ((p ^ <*G*>) . n)) & V c= the_Vertices_of ((p ^ <*G*>) . n) & (p ^ <*G*>) . (n + 1) is addAdjVertexAll of (p ^ <*G*>) . n,v,V )then A16:
(p ^ <*G*>) . (n + 1) = G
by A14;
A17:
1
<= n
by FINSEQ_3:25;
A18:
n = len p
by A13, A15;
then
n in dom p
by A17, FINSEQ_3:25;
then A19:
(p ^ <*G*>) . n = the
removeVertex of
G,
v0
by A11, A18, FINSEQ_1:def 7;
reconsider V =
v0 .allNeighbors() as non
empty finite set by A7;
take
v0
;
ex V being non empty finite set st
( v0 in (the_Vertices_of G) \ (the_Vertices_of ((p ^ <*G*>) . n)) & V c= the_Vertices_of ((p ^ <*G*>) . n) & (p ^ <*G*>) . (n + 1) is addAdjVertexAll of (p ^ <*G*>) . n,v0,V )take
V
;
( v0 in (the_Vertices_of G) \ (the_Vertices_of ((p ^ <*G*>) . n)) & V c= the_Vertices_of ((p ^ <*G*>) . n) & (p ^ <*G*>) . (n + 1) is addAdjVertexAll of (p ^ <*G*>) . n,v0,V )
v0 in {v0}
by TARSKI:def 1;
then
not
v0 in (the_Vertices_of G) \ {v0}
by XBOOLE_0:def 5;
then
not
v0 in the_Vertices_of the
removeVertex of
G,
v0
by A7, GLIB_000:47;
hence
v0 in (the_Vertices_of G) \ (the_Vertices_of ((p ^ <*G*>) . n))
by A19, XBOOLE_0:def 5;
( V c= the_Vertices_of ((p ^ <*G*>) . n) & (p ^ <*G*>) . (n + 1) is addAdjVertexAll of (p ^ <*G*>) . n,v0,V )
for
x being
object st
x in V holds
x in the_Vertices_of the
removeVertex of
G,
v0
hence
V c= the_Vertices_of ((p ^ <*G*>) . n)
by A19, TARSKI:def 3;
(p ^ <*G*>) . (n + 1) is addAdjVertexAll of (p ^ <*G*>) . n,v0,Vthus
(p ^ <*G*>) . (n + 1) is
addAdjVertexAll of
(p ^ <*G*>) . n,
v0,
V
by A7, A16, A19, Th47;
verum end; suppose A22:
n <= (len p) - 1
;
ex v being object ex V being non empty finite set st
( v in (the_Vertices_of G) \ (the_Vertices_of ((p ^ <*G*>) . n)) & V c= the_Vertices_of ((p ^ <*G*>) . n) & (p ^ <*G*>) . (n + 1) is addAdjVertexAll of (p ^ <*G*>) . n,v,V )then A23:
n + 0 <= ((len p) - 1) + 1
by XREAL_1:7;
1
<= n
by FINSEQ_3:25;
then reconsider m =
n as
Element of
dom p by A23, FINSEQ_3:25;
consider v being
object ,
V being non
empty finite set such that A24:
(
v in (the_Vertices_of the removeVertex of G,v0) \ (the_Vertices_of (p . m)) &
V c= the_Vertices_of (p . m) &
p . (m + 1) is
addAdjVertexAll of
p . m,
v,
V )
by A12, A22;
( 1
+ 0 <= n + 1 &
n + 1
<= ((len p) - 1) + 1 )
by A22, XREAL_1:6;
then
n + 1
in dom p
by FINSEQ_3:25;
then A25:
(p ^ <*G*>) . (n + 1) = p . (m + 1)
by FINSEQ_1:def 7;
A26:
(p ^ <*G*>) . n = p . m
by FINSEQ_1:def 7;
take
v
;
ex V being non empty finite set st
( v in (the_Vertices_of G) \ (the_Vertices_of ((p ^ <*G*>) . n)) & V c= the_Vertices_of ((p ^ <*G*>) . n) & (p ^ <*G*>) . (n + 1) is addAdjVertexAll of (p ^ <*G*>) . n,v,V )take
V
;
( v in (the_Vertices_of G) \ (the_Vertices_of ((p ^ <*G*>) . n)) & V c= the_Vertices_of ((p ^ <*G*>) . n) & (p ^ <*G*>) . (n + 1) is addAdjVertexAll of (p ^ <*G*>) . n,v,V )
(the_Vertices_of the removeVertex of G,v0) \ (the_Vertices_of (p . m)) c= (the_Vertices_of G) \ (the_Vertices_of (p . m))
by XBOOLE_1:33;
hence
v in (the_Vertices_of G) \ (the_Vertices_of ((p ^ <*G*>) . n))
by A24, A26;
( V c= the_Vertices_of ((p ^ <*G*>) . n) & (p ^ <*G*>) . (n + 1) is addAdjVertexAll of (p ^ <*G*>) . n,v,V )thus
(
V c= the_Vertices_of ((p ^ <*G*>) . n) &
(p ^ <*G*>) . (n + 1) is
addAdjVertexAll of
(p ^ <*G*>) . n,
v,
V )
by A24, A25, A26;
verum end; end;
end;
for k being non zero Nat holds S1[k]
from NAT_1:sch 10(A1, A4);
hence
for G being _finite simple connected _Graph ex p being non empty Graph-yielding _finite simple connected FinSequence st
( p . 1 is _trivial & p . 1 is edgeless & p . (len p) = G & len p = G .order() & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v being object ex V being non empty finite set st
( v in (the_Vertices_of G) \ (the_Vertices_of (p . n)) & V c= the_Vertices_of (p . n) & p . (n + 1) is addAdjVertexAll of p . n,v,V ) ) )
; verum