let G2 be _Graph; for v being object
for V being set
for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & G2 is acyclic & ( for G3 being Component of G2
for w1, w2 being Vertex of G3 st w1 in V & w2 in V holds
w1 = w2 ) holds
G1 is acyclic
let v be object ; for V being set
for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & G2 is acyclic & ( for G3 being Component of G2
for w1, w2 being Vertex of G3 st w1 in V & w2 in V holds
w1 = w2 ) holds
G1 is acyclic
let V be set ; for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & G2 is acyclic & ( for G3 being Component of G2
for w1, w2 being Vertex of G3 st w1 in V & w2 in V holds
w1 = w2 ) holds
G1 is acyclic
let G1 be addAdjVertexAll of G2,v,V; ( V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & G2 is acyclic & ( for G3 being Component of G2
for w1, w2 being Vertex of G3 st w1 in V & w2 in V holds
w1 = w2 ) implies G1 is acyclic )
assume that
A1:
( V c= the_Vertices_of G2 & not v in the_Vertices_of G2 )
and
A2:
G2 is acyclic
and
A3:
for G3 being Component of G2
for w1, w2 being Vertex of G3 st w1 in V & w2 in V holds
w1 = w2
; G1 is acyclic
consider E being set such that
( card V = card E & E misses the_Edges_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ E )
and
A4:
for v1 being object st v1 in V holds
ex e1 being object st
( e1 in E & e1 Joins v1,v,G1 & ( for e2 being object st e2 Joins v1,v,G1 holds
e1 = e2 ) )
by A1, Def4;
for W being Walk of G1 holds not W is Cycle-like
proof
given C being
Walk of
G1 such that A5:
C is
Cycle-like
;
contradiction
A6:
(
C is
closed &
C is
Path-like )
by A5;
set v1 =
C .first() ;
A7:
C .first() = C .last()
by A6, GLIB_001:def 24;
per cases
( C .first() <> v or C .first() = v )
;
suppose A8:
C .first() <> v
;
contradictionthen A9:
not
C .first() in {v}
by TARSKI:def 1;
A10:
the_Vertices_of G1 = (the_Vertices_of G2) \/ {v}
by A1, Def4;
then reconsider v1 =
C .first() as
Vertex of
G2 by A9, XBOOLE_0:def 3;
set G3 = the
inducedSubgraph of
G2,
(G2 .reachableFrom v1);
per cases
( C .vertices() c= G2 .reachableFrom v1 or not C .vertices() c= G2 .reachableFrom v1 )
;
suppose
not
C .vertices() c= G2 .reachableFrom v1
;
contradictionthen consider v2 being
object such that A13:
(
v2 in C .vertices() & not
v2 in G2 .reachableFrom v1 )
by TARSKI:def 3;
reconsider v2 =
v2 as
Vertex of
G1 by A13;
consider n being
odd Element of
NAT such that A14:
n <= len C
and A15:
C . n = v2
by A13, GLIB_001:87;
A16:
( 1
< n &
n < len C )
per cases
( v2 <> v or v2 = v )
;
suppose A18:
v2 <> v
;
contradictionthen
not
v2 in {v}
by TARSKI:def 1;
then reconsider v2 =
v2 as
Vertex of
G2 by A10, XBOOLE_0:def 3;
set P1 =
C .cut (1,
n);
set P2 =
C .cut (
n,
(len C));
A19:
1 is
odd Element of
NAT
by Lm16;
A20:
( 1
<= n &
n <= len C )
by ABIAN:12, A14;
A21:
(
n <= len C &
len C <= len C )
by A14;
A22:
(len (C .cut (1,n))) + 1
= n + 1
by A20, A19, GLIB_001:36;
A23:
(len (C .cut (n,(len C)))) + n = (len C) + 1
by A21, GLIB_001:36;
( not
v in (C .cut (1,n)) .vertices() or not
v in (C .cut (n,(len C))) .vertices() )
proof
assume
v in (C .cut (1,n)) .vertices()
;
not v in (C .cut (n,(len C))) .vertices()
then consider m being
odd Element of
NAT such that A24:
(
m <= len (C .cut (1,n)) &
(C .cut (1,n)) . m = v )
by GLIB_001:87;
reconsider m1 =
m -' 1 as
Element of
NAT ;
A25:
m1 + 1
= m
by Lm14;
m1 < len (C .cut (1,n))
by A24, Lm14;
then A26:
C . (1 + m1) = v
by A19, A20, A24, A25, GLIB_001:36;
assume
v in (C .cut (n,(len C))) .vertices()
;
contradiction
then consider k being
odd Element of
NAT such that A27:
(
k <= len (C .cut (n,(len C))) &
(C .cut (n,(len C))) . k = v )
by GLIB_001:87;
A28:
k < len (C .cut (n,(len C)))
reconsider k1 =
k -' 1 as
Element of
NAT ;
A30:
k1 + 1
= k
by Lm14;
k1 < len (C .cut (n,(len C)))
by A27, Lm14;
then
C . (n + k1) = v
by A21, A27, A30, GLIB_001:36;
then A31:
C . m = C . (n + k1)
by A25, A26;
reconsider nk =
n + k1 as
odd Element of
NAT by Lm15;
A32:
1
<= k1
m < (len (C .cut (1,n))) + 1
by A24, NAT_1:13;
then A35:
m < n + 1
by A22;
n + 1
<= n + k1
by A32, XREAL_1:6;
then A36:
m < nk
by A35, XXREAL_0:2;
A37:
1
<= k
by ABIAN:12;
k + n <= (len C) + 1
by A27, A23, XREAL_1:6;
then
(k + n) - 1
<= ((len C) + 1) - 1
by XREAL_1:9;
then
n + (k - 1) <= len C
;
then
n + k1 <= len C
by A37, XREAL_1:233;
then
(
m = 1 &
nk = len C )
by A6, A31, GLIB_001:def 28, A36;
hence
contradiction
by A28, A30, A23;
verum
end; per cases then
( not v in (C .cut (1,n)) .vertices() or not v in (C .cut (n,(len C))) .vertices() )
;
suppose
not
v in (C .cut (1,n)) .vertices()
;
contradictionthen reconsider P3 =
C .cut (1,
n) as
Walk of
G2 by A1, Th64;
C .cut (1,
n)
is_Walk_from C . 1,
C . n
by A20, A19, GLIB_001:37;
then
C .cut (1,
n)
is_Walk_from v1,
v2
by A15, GLIB_001:def 6;
then
P3 is_Walk_from v1,
v2
by GLIB_001:19;
then
v2 in G2 .reachableFrom v1
by GLIB_002:def 5;
hence
contradiction
by A13;
verum end; suppose
not
v in (C .cut (n,(len C))) .vertices()
;
contradictionthen reconsider P3 =
C .cut (
n,
(len C)) as
Walk of
G2 by A1, Th64;
C .cut (
n,
(len C))
is_Walk_from C . n,
C . (len C)
by A21, GLIB_001:37;
then
C .cut (
n,
(len C))
is_Walk_from v2,
v1
by A15, A7, GLIB_001:def 7;
then
P3 is_Walk_from v2,
v1
by GLIB_001:19;
then
P3 .reverse() is_Walk_from v1,
v2
by GLIB_001:23;
hence
contradiction
by A13, GLIB_002:def 5;
verum end; end; end; suppose A38:
v2 = v
;
contradictionreconsider m =
n - 2 as
odd Element of
NAT by A16, Lm13;
set P1 =
C .cut (1,
m);
set P2 =
C .cut (
(n + 2),
(len C));
n - 2
<= (len C) - 0
by A14, XREAL_1:13;
then A39:
( 1
<= m &
m <= len C )
by ABIAN:12;
A40:
(
n + 2
<= len C &
len C <= len C )
by A16, GLIB_001:1;
A41:
(len (C .cut (1,m))) + 1
= m + 1
by A39, Lm16, GLIB_001:36;
A42:
(len (C .cut ((n + 2),(len C)))) + (n + 2) = (len C) + 1
by A40, GLIB_001:36;
A43:
( not
v in (C .cut (1,m)) .vertices() & not
v in (C .cut ((n + 2),(len C))) .vertices() )
proof
assume
(
v in (C .cut (1,m)) .vertices() or
v in (C .cut ((n + 2),(len C))) .vertices() )
;
contradiction
per cases then
( v in (C .cut (1,m)) .vertices() or v in (C .cut ((n + 2),(len C))) .vertices() )
;
suppose
v in (C .cut (1,m)) .vertices()
;
contradictionthen consider k being
odd Element of
NAT such that A44:
(
k <= len (C .cut (1,m)) &
(C .cut (1,m)) . k = v )
by GLIB_001:87;
reconsider k1 =
k -' 1 as
Element of
NAT ;
k1 < len (C .cut (1,m))
by A44, Lm14;
then
(C .cut (1,m)) . (k1 + 1) = C . (1 + k1)
by A39, Lm16, GLIB_001:36;
then
(C .cut (1,m)) . k = C . (k1 + 1)
by Lm14;
then
(C .cut (1,m)) . k = C . k
by Lm14;
then A45:
C . k = C . n
by A38, A15, A44;
n - 2
< n - 0
by XREAL_1:15;
then A46:
m < n
;
k <= m
by A44, A41;
then
(
k < n &
n <= len C )
by A14, A46, XXREAL_0:2;
then
n = len C
by A5, A45, GLIB_001:def 28;
hence
contradiction
by A16;
verum end; suppose
v in (C .cut ((n + 2),(len C))) .vertices()
;
contradictionthen consider k being
odd Element of
NAT such that A47:
(
k <= len (C .cut ((n + 2),(len C))) &
(C .cut ((n + 2),(len C))) . k = v )
by GLIB_001:87;
reconsider k1 =
k -' 1 as
Element of
NAT ;
k1 < len (C .cut ((n + 2),(len C)))
by A47, Lm14;
then
(C .cut ((n + 2),(len C))) . (k1 + 1) = C . ((n + 2) + k1)
by A40, GLIB_001:36;
then
(C .cut ((n + 2),(len C))) . k = C . ((n + (k1 + 1)) + 1)
by Lm14;
then A48:
(C .cut ((n + 2),(len C))) . k = C . ((n + k) + 1)
by Lm14;
reconsider nk =
(n + k) + 1 as
odd Element of
NAT ;
A49:
C . nk = C . n
by A38, A15, A47, A48;
(
n < nk &
nk <= len C )
then
n = 1
by A49, A5, GLIB_001:def 28;
hence
contradiction
by A16;
verum end; end;
end; then reconsider P1 =
C .cut (1,
m),
P2 =
C .cut (
(n + 2),
(len C)) as
Walk of
G2 by A1, Th64;
set w1 =
C . m;
set w2 =
C . (n + 2);
set e1 =
C . (m + 1);
set e2 =
C . (n + 1);
n - 2
< (len C) - 0
by A14, XREAL_1:15;
then
(
C . (m + 1) Joins C . m,
C . (m + 2),
G1 &
C . (n + 1) Joins C . n,
C . (n + 2),
G1 )
by GLIB_001:def 3, A16;
then A50:
(
C . (m + 1) Joins C . m,
v,
G1 &
C . (n + 1) Joins C . (n + 2),
v,
G1 )
by A38, GLIB_000:14, A15;
then A51:
(
C . m in V &
C . (n + 2) in V )
by A1, Def4;
then reconsider w1 =
C . m,
w2 =
C . (n + 2) as
Vertex of
G2 by A1;
(
(C .cut (1,m)) .first() = C . 1 &
(C .cut (1,m)) .last() = C . m )
by A39, Lm16, GLIB_001:37;
then A52:
(
(C .cut (1,m)) .first() = v1 &
(C .cut (1,m)) .last() = w1 )
by GLIB_001:def 6;
(
(C .cut ((n + 2),(len C))) .first() = w2 &
(C .cut ((n + 2),(len C))) .last() = C . (len C) )
by A40, GLIB_001:37;
then
(
(C .cut ((n + 2),(len C))) .first() = w2 &
(C .cut ((n + 2),(len C))) .last() = v1 )
by A7, GLIB_001:def 7;
then A53:
(
((C .cut ((n + 2),(len C))) .reverse()) .first() = v1 &
((C .cut ((n + 2),(len C))) .reverse()) .last() = w2 )
by GLIB_001:22;
w1 in G2 .reachableFrom v1
by A1, A43, A52, Th69;
then reconsider w1 =
w1 as
Vertex of the
inducedSubgraph of
G2,
(G2 .reachableFrom v1) by GLIB_000:def 37;
w2 in G2 .reachableFrom v1
then reconsider w2 =
w2 as
Vertex of the
inducedSubgraph of
G2,
(G2 .reachableFrom v1) by GLIB_000:def 37;
A54:
w1 = w2
by A51, A3;
consider e3 being
object such that
(
e3 in E &
e3 Joins w1,
v,
G1 )
and A55:
for
e5 being
object st
e5 Joins w1,
v,
G1 holds
e5 = e3
by A4, A51;
(
C . (m + 1) = e3 &
C . (n + 1) = e3 )
by A54, A50, A55;
then A56:
C . (n - 1) = C . (n + 1)
;
reconsider n2 =
m + 1 as
even Element of
NAT ;
n + (- 1) < n + 1
by XREAL_1:8;
then A57:
n2 < n + 1
;
A58:
1
+ 0 <= m + 1
by XREAL_1:7;
(n + 2) - 1
<= (len C) - 0
by A40, XREAL_1:13;
then
( 1
<= n2 &
n2 < n + 1 &
n + 1
<= len C )
by A57, A58;
then
C . n2 <> C . (n + 1)
by A6, GLIB_001:138;
hence
contradiction
by A56;
verum end; end; end; end; end; suppose A59:
C .first() = v
;
contradictionA60:
len C >= 5
proof
assume
len C < 5
;
contradiction
then
len C < 4
+ 1
;
then
len C <= 4
by NAT_1:13;
then A61:
len C = 3
by A5, GLIB_001:126, CHORD:7;
then
1
< len C
;
then
C . (1 + 1) Joins C . 1,
C . (1 + 2),
G1
by Lm16, GLIB_001:def 3;
then
C . 2
Joins C .first() ,
C . (len C),
G1
by A61, GLIB_001:def 6;
then
C . 2
Joins C .first() ,
C .last() ,
G1
by GLIB_001:def 7;
then
C . 2
Joins v,
v,
G1
by A59, A7;
hence
contradiction
by A1, Def4;
verum
end; A62:
1
< len C
then reconsider m =
(len C) - 2 as
odd Element of
NAT by Lm13;
(len C) - 2
< (len C) - 0
by XREAL_1:15;
then A64:
m < len C
;
set w1 =
C . 3;
set w2 =
C . m;
set e1 =
C . 2;
set e2 =
C . (m + 1);
set P =
C .cut (3,
m);
A65:
3 is
odd Element of
NAT
by Lm16;
A66:
(len C) - 2
<= (len C) - 0
by XREAL_1:13;
5
- 2
<= (len C) - 2
by A60, XREAL_1:9;
then A67:
( 3
<= m &
m <= len C )
by A66;
then
(len (C .cut (3,m))) + 3
= ((len C) - 2) + 1
by A65, GLIB_001:36;
then A68:
(len (C .cut (3,m))) + 4
= len C
;
not
v in (C .cut (3,m)) .vertices()
proof
assume
v in (C .cut (3,m)) .vertices()
;
contradiction
then consider k being
odd Element of
NAT such that A69:
(
k <= len (C .cut (3,m)) &
(C .cut (3,m)) . k = v )
by GLIB_001:87;
reconsider k1 =
k -' 1 as
Element of
NAT ;
A70:
k1 + 1
= k
by Lm14;
k1 < len (C .cut (3,m))
by A69, Lm14;
then
(C .cut (3,m)) . (k1 + 1) = C . (3 + k1)
by A67, A65, GLIB_001:36;
then A71:
C . (3 + k1) = C . (len C)
by A7, A59, A69, A70, GLIB_001:def 7;
reconsider k3 = 3
+ k1 as
odd Element of
NAT by Lm15, Lm16;
(len (C .cut (3,m))) + 2
= (len C) - 2
by A68;
then A72:
(len (C .cut (3,m))) + 2
< (len C) - 0
by XREAL_1:15;
k3 = (k1 + 1) + 2
;
then
k3 = k + 2
by Lm14;
then
k3 <= (len (C .cut (3,m))) + 2
by A69, XREAL_1:6;
then
k3 < len C
by A72, XXREAL_0:2;
then A73:
k3 = 1
by A71, A6, GLIB_001:def 28;
3
<= k3
by NAT_1:11;
hence
contradiction
by A73;
verum
end; then reconsider P =
C .cut (3,
m) as
Walk of
G2 by A1, Th64;
(
C . (1 + 1) Joins C . 1,
C . (1 + 2),
G1 &
C . (m + 1) Joins C . m,
C . (m + 2),
G1 )
by A62, A64, Lm16, GLIB_001:def 3;
then
(
C . 2
Joins C .first() ,
C . 3,
G1 &
C . (m + 1) Joins C . m,
C . (len C),
G1 )
by GLIB_001:def 6;
then
(
C . 2
Joins C . 3,
v,
G1 &
C . (m + 1) Joins C . m,
C .last() ,
G1 )
by A59, GLIB_000:14, GLIB_001:def 7;
then A74:
(
C . 2
Joins C . 3,
v,
G1 &
C . (m + 1) Joins C . m,
v,
G1 )
by A59, A7;
then A75:
(
C . 3
in V &
C . m in V )
by A1, Def4;
then reconsider w1 =
C . 3,
w2 =
C . m as
Vertex of
G2 by A1;
set G3 = the
inducedSubgraph of
G2,
(G2 .reachableFrom w1);
C .cut (3,
m)
is_Walk_from w1,
w2
by A67, Lm16, GLIB_001:37;
then
P is_Walk_from w1,
w2
by GLIB_001:19;
then
w2 in G2 .reachableFrom w1
by GLIB_002:def 5;
then reconsider w2 =
w2 as
Vertex of the
inducedSubgraph of
G2,
(G2 .reachableFrom w1) by GLIB_000:def 37;
w1 in G2 .reachableFrom w1
by GLIB_002:9;
then reconsider w1 =
w1 as
Vertex of the
inducedSubgraph of
G2,
(G2 .reachableFrom w1) by GLIB_000:def 37;
A76:
w1 = w2
by A3, A75;
consider e3 being
object such that
(
e3 in E &
e3 Joins w1,
v,
G1 )
and A77:
for
e5 being
object st
e5 Joins w1,
v,
G1 holds
e3 = e5
by A4, A75;
A78:
(
C . 2
= e3 &
C . (m + 1) = e3 )
by A74, A76, A77;
reconsider n2 = 1
+ 1 as
even Element of
NAT by Lm16;
(len C) - 1
<= (len C) - 0
by XREAL_1:13;
then A79:
m + 1
<= len C
;
( 2
< 3 & 3
+ 0 <= m + 1 )
by A67, XREAL_1:7;
then
( 1
<= n2 &
n2 < m + 1 &
m + 1
<= len C )
by A79, XXREAL_0:2;
then
C . n2 <> C . (m + 1)
by A5, GLIB_001:138;
hence
contradiction
by A78;
verum end; end;
end;
hence
G1 is acyclic
by GLIB_002:def 2; verum