let G be _finite chordal _Graph; for a, b being Vertex of G st a <> b & not a,b are_adjacent holds
for S being VertexSeparator of a,b st S is minimal holds
for H being removeVertices of G,S
for a1 being Vertex of H st a = a1 holds
ex c being Vertex of G st
( c in H .reachableFrom a1 & ( for x being Vertex of G st x in S holds
c,x are_adjacent ) )
let a, b be Vertex of G; ( a <> b & not a,b are_adjacent implies for S being VertexSeparator of a,b st S is minimal holds
for H being removeVertices of G,S
for a1 being Vertex of H st a = a1 holds
ex c being Vertex of G st
( c in H .reachableFrom a1 & ( for x being Vertex of G st x in S holds
c,x are_adjacent ) ) )
assume that
A1:
a <> b
and
A2:
not a,b are_adjacent
; for S being VertexSeparator of a,b st S is minimal holds
for H being removeVertices of G,S
for a1 being Vertex of H st a = a1 holds
ex c being Vertex of G st
( c in H .reachableFrom a1 & ( for x being Vertex of G st x in S holds
c,x are_adjacent ) )
let S be VertexSeparator of a,b; ( S is minimal implies for H being removeVertices of G,S
for a1 being Vertex of H st a = a1 holds
ex c being Vertex of G st
( c in H .reachableFrom a1 & ( for x being Vertex of G st x in S holds
c,x are_adjacent ) ) )
assume A3:
S is minimal
; for H being removeVertices of G,S
for a1 being Vertex of H st a = a1 holds
ex c being Vertex of G st
( c in H .reachableFrom a1 & ( for x being Vertex of G st x in S holds
c,x are_adjacent ) )
let H be removeVertices of G,S; for a1 being Vertex of H st a = a1 holds
ex c being Vertex of G st
( c in H .reachableFrom a1 & ( for x being Vertex of G st x in S holds
c,x are_adjacent ) )
let a1 be Vertex of H; ( a = a1 implies ex c being Vertex of G st
( c in H .reachableFrom a1 & ( for x being Vertex of G st x in S holds
c,x are_adjacent ) ) )
assume A4:
a = a1
; ex c being Vertex of G st
( c in H .reachableFrom a1 & ( for x being Vertex of G st x in S holds
c,x are_adjacent ) )
assume A5:
for c being Vertex of G holds
( not c in H .reachableFrom a1 or ex x being Vertex of G st
( x in S & not c,x are_adjacent ) )
; contradiction
per cases
( S is empty or not S is empty )
;
suppose
not
S is
empty
;
contradictionthen reconsider S =
S as non
empty Subset of
(the_Vertices_of G) ;
set A =
H .reachableFrom a1;
deffunc H1(
set )
-> Element of
omega =
card ((G .AdjacentSet {$1}) /\ S);
set M =
{ H1(x) where x is Vertex of G : x in H .reachableFrom a1 } ;
A7:
H .reachableFrom a1 is
finite
;
A8:
{ H1(x) where x is Vertex of G : x in H .reachableFrom a1 } is
finite
from FRAENKEL:sch 21(A7);
a in H .reachableFrom a1
by A4, GLIB_002:9;
then
card ((G .AdjacentSet {a}) /\ S) in { H1(x) where x is Vertex of G : x in H .reachableFrom a1 }
;
then reconsider M =
{ H1(x) where x is Vertex of G : x in H .reachableFrom a1 } as non
empty finite natural-membered set by A8, A6, MEMBERED:def 6;
set Ga = the
inducedSubgraph of
H,
(H .reachableFrom a1);
A9:
the_Vertices_of the
inducedSubgraph of
H,
(H .reachableFrom a1) = H .reachableFrom a1
by GLIB_000:def 37;
max M in M
by XXREAL_2:def 8;
then consider c being
Vertex of
G such that A10:
max M = card ((G .AdjacentSet {c}) /\ S)
and A11:
c in H .reachableFrom a1
;
set gcs =
(G .AdjacentSet {c}) /\ S;
A12:
(H .reachableFrom a1) /\ S = {}
by A1, A2, Th74;
set Gs = the
inducedSubgraph of
G,
S;
set tVG =
the_Vertices_of G;
A13:
(2 * 0) + 1 is
odd
;
not
a in S
by A1, A2, Def8;
then A14:
(the_Vertices_of G) \ S is non
empty Subset of
(the_Vertices_of G)
by XBOOLE_0:def 5;
the_Vertices_of H c= the_Vertices_of G
;
then reconsider A =
H .reachableFrom a1 as non
empty Subset of
(the_Vertices_of G) by XBOOLE_1:1;
then
A c= (the_Vertices_of G) \ S
;
then reconsider Ga = the
inducedSubgraph of
H,
(H .reachableFrom a1) as
inducedSubgraph of
G,
A by A14, Th29;
consider y being
Vertex of
G such that A16:
y in S
and A17:
not
c,
y are_adjacent
by A5, A11;
A18:
not
y in A
by A16, A12, XBOOLE_0:def 4;
set Ay =
A \/ {y};
set Gay = the
inducedSubgraph of
G,
(A \/ {y});
y in {y}
by TARSKI:def 1;
then A19:
y in A \/ {y}
by XBOOLE_0:def 3;
c in A \/ {y}
by A11, XBOOLE_0:def 3;
then reconsider ca =
c,
ya =
y as
Vertex of the
inducedSubgraph of
G,
(A \/ {y}) by A19, GLIB_000:def 37;
ex
yaa being
Vertex of
G st
(
yaa in A &
y,
yaa are_adjacent )
by A1, A2, A3, A4, A16, Th81;
then
y in G .AdjacentSet (the_Vertices_of Ga)
by A9, A18;
then
the
inducedSubgraph of
G,
(A \/ {y}) is
connected
by Th56;
then consider Wa being
Walk of the
inducedSubgraph of
G,
(A \/ {y}) such that A20:
Wa is_Walk_from ca,
ya
;
consider P being
Path of the
inducedSubgraph of
G,
(A \/ {y}) such that A21:
P is_Walk_from Wa .first() ,
Wa .last()
and A22:
P is
minlength
by Th38;
Wa .first() = ca
by A20;
then A23:
P .first() = ca
by A21;
Wa .last() = ya
by A20;
then A24:
P .last() = y
by A21;
c <> y
by A11, A16, A12, XBOOLE_0:def 4;
then
P is
trivial
by A23, A24, GLIB_001:127;
then A25:
len P >= 3
by GLIB_001:125;
then
5
+ (- 2) <= (len P) + (- 2)
by XREAL_1:7;
then reconsider j =
(len P) - (2 * 1) as
odd Element of
NAT by INT_1:3, XXREAL_0:2;
set d =
P . j;
A28:
j < len P
by XREAL_1:44;
A29:
now not P . j = yend; A30:
not
y in G .AdjacentSet {c}
by A17, Th51;
A31:
the_Vertices_of the
inducedSubgraph of
G,
(A \/ {y}) = A \/ {y}
by GLIB_000:def 37;
A32:
P . j in the_Vertices_of the
inducedSubgraph of
G,
(A \/ {y})
by A28, GLIB_001:7;
then A33:
(
P . j in A or
P . j in {y} )
by A31, XBOOLE_0:def 3;
reconsider d =
P . j as
Vertex of
G by A32;
set gds =
(G .AdjacentSet {d}) /\ S;
P . (j + 1) Joins d,
P . (((len P) - 2) + 2), the
inducedSubgraph of
G,
(A \/ {y})
by A28, GLIB_001:def 3;
then A34:
P . (j + 1) Joins d,
y,
G
by A24, GLIB_000:72;
then
d,
y are_adjacent
;
then A35:
y in G .AdjacentSet {d}
by A29, Th51;
then A36:
y in (G .AdjacentSet {d}) /\ S
by A16, XBOOLE_0:def 4;
then consider x being
object such that A39:
x in (G .AdjacentSet {c}) /\ S
and A40:
not
x in (G .AdjacentSet {d}) /\ S
;
A41:
x in S
by A39, XBOOLE_0:def 4;
then A42:
not
x in G .AdjacentSet {d}
by A40, XBOOLE_0:def 4;
reconsider x =
x as
Vertex of
G by A39;
defpred S1[
Nat]
means ( $1
in dom P & $1 is
odd & $1
< len P & ex
e being
object st
e Joins x,
P . $1,
G );
A43:
for
k being
Nat st
S1[
k] holds
k <= len P
;
A44:
not
x in A
by A12, A41, XBOOLE_0:def 4;
A45:
1
< len P
by A26, XXREAL_0:2;
then A46:
1
in dom P
by FINSEQ_3:25;
x in G .AdjacentSet {c}
by A39, XBOOLE_0:def 4;
then
c,
x are_adjacent
by Th51;
then
ex
e being
object st
e Joins x,
P . 1,
G
by A23, Def3;
then A47:
ex
k being
Nat st
S1[
k]
by A45, A46, A13;
consider k being
Nat such that A48:
S1[
k]
and A49:
for
i being
Nat st
S1[
i] holds
k >= i
from NAT_1:sch 6(A43, A47);
reconsider k =
k as
odd Element of
NAT by A48;
set Q1 =
P .cut (
k,
j);
reconsider Q =
P .cut (
k,
j) as
Path of
G by GLIB_001:175;
A50:
k <= j
by A48, Th3;
A51:
j < len P
by XREAL_1:44;
then A52:
P .cut (
k,
j) is
minlength
by A22, A50, Th41;
A53:
(len Q) + k = j + 1
by A50, A51, GLIB_001:36;
A54:
now for i being odd Nat st i in dom Q & i <> 1 holds
for e being object holds not e Joins Q . i,x,Glet i be
odd Nat;
( i in dom Q & i <> 1 implies for e being object holds not e Joins Q . i,x,G )assume that A55:
i in dom Q
and A56:
i <> 1
;
for e being object holds not e Joins Q . i,x,G
1
<= i
by A55, FINSEQ_3:25;
then
1
+ (- 1) <= i + (- 1)
by XREAL_1:7;
then reconsider i1 =
i - 1 as
even Element of
NAT by INT_1:3;
reconsider ki1 =
k + i1 as
odd Element of
NAT ;
A57:
i + (- 1) < i + (- 0)
by XREAL_1:8;
i <= len Q
by A55, FINSEQ_3:25;
then A58:
i1 < len Q
by A57, XXREAL_0:2;
then A59:
ki1 in dom P
by A50, A51, GLIB_001:36;
A60:
(len P) + (- 1) < (len P) + (- 0)
by XREAL_1:8;
assume A61:
ex
e being
object st
e Joins Q . i,
x,
G
;
contradiction
i1 + k < (((len P) - 1) - k) + k
by A53, A58, XREAL_1:8;
then A62:
ki1 < len P
by A60, XXREAL_0:2;
A63:
Q . (i1 + 1) = P . ki1
by A50, A51, A58, GLIB_001:36;
hence
contradiction
by A56;
verum end; set cc =
Q .first() ;
set dd =
Q .last() ;
A64:
(P .cut (k,j)) .first() = P . k
by A50, A51, GLIB_001:37;
then A65:
x,
Q .first() are_adjacent
by A48;
A66:
x <> y
by A16, A35, A40, XBOOLE_0:def 4;
then A67:
not
x in {y}
by TARSKI:def 1;
reconsider xs =
x,
ys =
y as
Vertex of the
inducedSubgraph of
G,
S by A16, A41, GLIB_000:def 37;
the
inducedSubgraph of
G,
S is
complete
by A1, A2, A3, Th97;
then
xs,
ys are_adjacent
by A66;
then consider ej being
object such that A68:
ej Joins xs,
ys, the
inducedSubgraph of
G,
S
;
ej Joins x,
y,
G
by A68, GLIB_000:72;
then A69:
x,
y are_adjacent
;
A70:
(P .cut (k,j)) .last() = P . j
by A50, A51, GLIB_001:37;
then A71:
Q .last() = P . j
;
d <> x
by A12, A33, A29, A41, TARSKI:def 1, XBOOLE_0:def 4;
then A72:
not
d,
x are_adjacent
by A42, Th51;
then A73:
Q .first() <> Q .last()
by A48, A64, A70, Def3;
then A74:
Q is
open
;
A75:
Q .vertices() = (P .cut (k,j)) .vertices()
by GLIB_001:98;
then
Q .last() in (P .cut (k,j)) .vertices()
by GLIB_001:88;
then A76:
Q .last() <> x
by A31, A44, A67, XBOOLE_0:def 3;
A80:
now for v being set st v in Q .vertices() holds
v in Alet v be
set ;
( v in Q .vertices() implies v in A )assume A81:
v in Q .vertices()
;
v in Aconsider n being
odd Element of
NAT such that A82:
n <= len Q
and A83:
Q . n = v
by A81, GLIB_001:87;
1
<= n
by ABIAN:12;
then
1
+ (- 1) <= n + (- 1)
by XREAL_1:7;
then reconsider n1 =
n - 1 as
even Element of
NAT by INT_1:3;
reconsider kn1 =
k + n1 as
odd Element of
NAT ;
A84:
(len P) + (- 1) < (len P) + (- 0)
by XREAL_1:8;
n + (- 1) < n + (- 0)
by XREAL_1:8;
then A85:
n1 < len Q
by A82, XXREAL_0:2;
then
k + n1 < (((len P) - 1) - k) + k
by A53, XREAL_1:8;
then A86:
kn1 < len P
by A84, XXREAL_0:2;
A87:
Q . (n1 + 1) = P . kn1
by A50, A51, A85, GLIB_001:36;
now not v = yA88:
1
<= k
by ABIAN:12;
assume A89:
v = y
;
contradictionthen A90:
k + (n + (- 1)) = 1
by A24, A83, A87, A86, GLIB_001:def 28;
1
<= n
by ABIAN:12;
hence
contradiction
by A24, A77, A64, A83, A89, A91, XXREAL_0:1;
verum end; then A92:
not
v in {y}
by TARSKI:def 1;
Q .vertices() c= P .vertices()
by A50, A51, A75, GLIB_001:94;
then
v in P .vertices()
by A81;
hence
v in A
by A31, A92, XBOOLE_0:def 3;
verum end;
Q .first() in (P .cut (k,j)) .vertices()
by A75, GLIB_001:88;
then A93:
Q .first() <> x
by A31, A44, A67, XBOOLE_0:def 3;
Q .last() ,
y are_adjacent
by A34, A70;
then consider R being
Path of
G such that A94:
len R = 7
and A95:
R .length() = 3
and A96:
R .vertices() = {(Q .last()),y,x,(Q .first())}
and A97:
R . 1
= Q .last()
and A98:
R . 3
= y
and A99:
R . 5
= x
and A100:
R . 7
= Q .first()
by A24, A29, A66, A69, A77, A64, A70, A76, A93, A65, Th47;
A101:
R is
trivial
by A94, GLIB_001:126;
A102:
Q .edges() misses R .edges()
then A116:
{(Q .first()),(Q .last())} c= (Q .vertices()) /\ (R .vertices())
;
now for v being object st v in (Q .vertices()) /\ (R .vertices()) holds
v in {(Q .first()),(Q .last())}let v be
object ;
( v in (Q .vertices()) /\ (R .vertices()) implies v in {(Q .first()),(Q .last())} )assume A117:
v in (Q .vertices()) /\ (R .vertices())
;
v in {(Q .first()),(Q .last())}
v in {(Q .last()),y,x,(Q .first())}
by A96, A117, XBOOLE_0:def 4;
then A118:
(
v = Q .last() or
v = y or
v = x or
v = Q .first() )
by ENUMSET1:def 2;
v in Q .vertices()
by A117, XBOOLE_0:def 4;
then
v in A
by A80;
hence
v in {(Q .first()),(Q .last())}
by A16, A12, A41, A118, TARSKI:def 2, XBOOLE_0:def 4;
verum end; then
(Q .vertices()) /\ (R .vertices()) c= {(Q .first()),(Q .last())}
;
then A119:
(Q .vertices()) /\ (R .vertices()) = {(Q .first()),(Q .last())}
by A116;
A120:
now for i being odd Nat st i in dom Q & i <> len Q holds
for e being object holds not e Joins Q . i,y,Glet i be
odd Nat;
( i in dom Q & i <> len Q implies for e being object holds not e Joins Q . i,y,G )assume that A121:
i in dom Q
and A122:
i <> len Q
;
for e being object holds not e Joins Q . i,y,G
1
<= i
by A121, FINSEQ_3:25;
then
1
+ (- 1) <= i + (- 1)
by XREAL_1:7;
then reconsider i1 =
i - 1 as
even Element of
NAT by INT_1:3;
reconsider ki1 =
k + i1 as
odd Element of
NAT ;
A123:
i + (- 1) < i + (- 0)
by XREAL_1:8;
A124:
i <= len Q
by A121, FINSEQ_3:25;
then A125:
i1 < len Q
by A123, XXREAL_0:2;
then
ki1 in dom P
by A50, A51, GLIB_001:36;
then A126:
ki1 <= len P
by FINSEQ_3:25;
then A127:
P . ki1 in A \/ {y}
by A31, GLIB_001:7;
then
ki1 < len P
by A126, XXREAL_0:1;
then A129:
ki1 + 2
<= len P
by Th4;
ki1 + 2
<> len P
by A53, A122;
then A130:
ki1 + 2
< len P
by A129, XXREAL_0:1;
A131:
P . (len P) in A \/ {y}
by A31, GLIB_001:7;
assume A132:
ex
e being
object st
e Joins Q . i,
y,
G
;
contradiction
Q . (i1 + 1) = P . ki1
by A50, A51, A125, GLIB_001:36;
hence
contradiction
by A22, A24, A132, A130, A127, A131, Th19, Th39;
verum end; A133:
Q .first() = P . k
by A64;
P . k <> P . j
by A72, A48, Def3;
then A134:
Q is
trivial
by A133, A71, GLIB_001:127;
then
Q .length() <> 0
;
then A135:
Q .length() >= 0 + 1
by NAT_1:13;
set C =
Q .append R;
A136:
R .first() = Q .last()
by A97;
then A137:
(Q .append R) . ((len Q) + 6) = R . (6 + 1)
by A94, GLIB_001:33;
A138:
(Q .append R) . ((len Q) + 4) = R . (4 + 1)
by A94, A136, GLIB_001:33;
A139:
(Q .append R) . ((len Q) + 2) = R . (2 + 1)
by A94, A136, GLIB_001:33;
(Q .append R) .length() = (Q .length()) + 3
by A95, A136, Th28;
then
(Q .append R) .length() >= 1
+ 3
by A135, XREAL_1:7;
then A140:
(Q .append R) .length() > 3
by NAT_1:13;
A141:
R .last() = Q .first()
by A94, A100;
then A142:
R is
open
by A73, A136;
then
Q .append R is
Cycle-like
by A74, A136, A141, A101, A102, A119, Th27;
then
Q .append R is
chordal
by A140, Def11;
then consider m,
n being
odd Nat such that A143:
m + 2
< n
and A144:
n <= len (Q .append R)
and
(Q .append R) . m <> (Q .append R) . n
and A145:
ex
e being
object st
e Joins (Q .append R) . m,
(Q .append R) . n,
G
and A146:
(
Q .append R is
Cycle-like implies ( ( not
m = 1 or not
n = len (Q .append R) ) & ( not
m = 1 or not
n = (len (Q .append R)) - 2 ) & ( not
m = 3 or not
n = len (Q .append R) ) ) )
by Th83;
consider e being
object such that A147:
e Joins (Q .append R) . m,
(Q .append R) . n,
G
by A145;
A148:
((len (Q .append R)) + 1) + (- 1) = ((len Q) + (len R)) + (- 1)
by A136, GLIB_001:28;
A149:
(
n <= len Q or
n = (len Q) + 2 or
n = (len Q) + 4 or
n = (len Q) + 6 )
A152:
1
<= m
by ABIAN:12;
per cases
( n <= len Q or n = (len Q) + 2 or n = (len Q) + 4 or n = (len Q) + 6 )
by A149;
suppose A153:
n <= len Q
;
contradictionA154:
m + 0 <= m + 2
by XREAL_1:7;
m + 2
<= len Q
by A143, A153, XXREAL_0:2;
then
m <= len Q
by A154, XXREAL_0:2;
then
m in dom Q
by A152, FINSEQ_3:25;
then A155:
Q . m = (Q .append R) . m
by GLIB_001:32;
1
<= n
by ABIAN:12;
then
n in dom Q
by A153, FINSEQ_3:25;
then
Q . n = (Q .append R) . n
by GLIB_001:32;
hence
contradiction
by A52, A143, A147, A153, A155, Th40;
verum end; suppose A156:
n = (len Q) + 2
;
contradictionthen
m < len Q
by A143, XREAL_1:6;
then A157:
m in dom Q
by A152, FINSEQ_3:25;
then
e Joins Q . m,
y,
G
by A98, A139, A147, A156, GLIB_001:32;
hence
contradiction
by A120, A143, A156, A157;
verum end; suppose A158:
n = (len Q) + 4
;
contradictionthen
(m + 2) + 2
<= (len Q) + 4
by A143, Th4;
then
m + 4
<= (len Q) + 4
;
then
m <= len Q
by XREAL_1:6;
then A159:
m in dom Q
by A152, FINSEQ_3:25;
then A160:
e Joins Q . m,
x,
G
by A99, A138, A147, A158, GLIB_001:32;
per cases
( 1 = m or 1 < m )
by A152, XXREAL_0:1;
suppose
1
= m
;
contradictionhence
contradiction
by A74, A94, A136, A141, A101, A142, A102, A119, A148, A146, A158, Th27;
verum end; end; suppose A161:
n = (len Q) + 6
;
contradictionthen
(m + 2) + 2
<= (len Q) + 6
by A143, Th4;
then
m + 4
<= ((len Q) + 2) + 4
;
then A162:
m <= (len Q) + 2
by XREAL_1:6;
per cases
( m < (len Q) + 2 or m = (len Q) + 2 )
by A162, XXREAL_0:1;
suppose A163:
m < (len Q) + 2
;
contradictionnow not 1 + 2 >= massume
1
+ 2
>= m
;
contradictionthen
m < (2 * 1) + 1
by A74, A94, A136, A141, A101, A142, A102, A119, A148, A146, A161, Th27, XXREAL_0:1;
then
m <= 3
- 2
by Th3;
then
m < 1
by A74, A94, A136, A141, A101, A142, A102, A119, A148, A146, A161, Th27, XXREAL_0:1;
hence
contradiction
by ABIAN:12;
verum end; then A164:
((2 * 0) + 1) + 2
< m
;
A165:
m <= len Q
by A163, Th4;
then
m in dom Q
by A152, FINSEQ_3:25;
then
(Q .append R) . m = Q . m
by GLIB_001:32;
hence
contradiction
by A52, A100, A137, A147, A161, A165, A164, Th40, GLIB_000:14;
verum suppose A166:
m = (len Q) + 2
;
contradiction
3
<= len Q
by A134, GLIB_001:125;
then
1
<= len Q
by XXREAL_0:2;
then A167:
(2 * 0) + 1
in dom Q
by FINSEQ_3:25;
1
<> len Q
by A72, A48, A64, A70, Def3;
hence
contradiction
by A120, A98, A100, A137, A139, A147, A161, A166, A167, GLIB_000:14;
verum end; end;