let G be finite _Graph; :: thesis: ( ( 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 & not S is empty holds
for G2 being inducedSubgraph of G,S holds G2 is complete ) implies G is chordal )
assume A1:
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 & not S is empty holds
for G2 being inducedSubgraph of G,S holds G2 is complete
; :: thesis: G is chordal
let P be Walk of G; :: according to CHORD:def 11 :: thesis: ( P .length() > 3 & P is Cycle-like implies P is chordal )
assume A2:
( P .length() > 3 & P is Cycle-like )
; :: thesis: P is chordal
A3:
P is Path-like
by A2;
P .length() >= 3 + 1
by A2, NAT_1:13;
then
2 * (P .length() ) >= 2 * 4
by XREAL_1:66;
then
(2 * (P .length() )) + 1 >= 8 + 1
by XREAL_1:9;
then A4:
len P >= 9
by GLIB_001:113;
reconsider m = (2 * 0 ) + 1 as odd Nat ;
reconsider n = (2 * 2) + 1 as odd Nat ;
per cases
( ex e being set st e Joins P . m,P . n,G or for e being set holds not e Joins P . m,P . n,G )
;
suppose A10:
for
e being
set holds not
e Joins P . m,
P . n,
G
;
:: thesis: P is chordal reconsider Pm =
P . m as
Vertex of
G by A4, GLIB_001:8, XXREAL_0:2;
reconsider Pn =
P . n as
Vertex of
G by A4, GLIB_001:8, XXREAL_0:2;
A11:
not
Pm,
Pn are_adjacent
by A10, Def3;
consider S being
VertexSeparator of
Pm,
Pn such that A12:
S is
minimal
by Th79;
set P15 =
P .cut m,
n;
set P5l =
P .cut n,
(len P);
A13:
(
m <= n &
n <= len P )
by A4, XXREAL_0:2;
then A14:
P .cut m,
n is_Walk_from P . m,
P . n
by GLIB_001:38;
then A15:
not
S is
empty
by A5, A11, Th73;
consider G2 being
inducedSubgraph of
G,
S;
A16:
G2 is
complete
by A1, A5, A11, A12, A15;
A17:
((len (P .cut m,n)) + 1) + (- 1) = (5 + 1) + (- 1)
by A13, GLIB_001:37;
then consider k being
odd Nat such that A18:
(
m < k &
k < n )
and A19:
(P .cut m,n) . k in S
by A5, A11, A14, Th72;
A20:
( 1
+ 2
<= k &
k <= 5
- 2 )
by A18, Th3, Th4;
then A21:
k = 3
by XXREAL_0:1;
(P .cut m,n) . (2 + 1) = P . (1 + 2)
by A13, A17, GLIB_001:37;
then A22:
P . 3
in S
by A19, A20, XXREAL_0:1;
A23:
P is
closed
by A2;
A24:
(
n <= len P &
len P <= len P )
by A4, XXREAL_0:2;
then
P .cut n,
(len P) is_Walk_from P . n,
P . (len P)
by GLIB_001:38;
then A25:
P .cut n,
(len P) is_Walk_from P . n,
P . m
by A23, GLIB_001:119;
S is
VertexSeparator of
Pn,
Pm
by A5, A11, Th70;
then consider l being
odd Nat such that A26:
( 1
< l &
l < len (P .cut n,(len P)) )
and A27:
(P .cut n,(len P)) . l in S
by A5, A11, A25, Th72;
A28:
1
+ (- 1) < l + (- 1)
by A26, XREAL_1:10;
then reconsider l2 =
l - 1 as
even Element of
NAT by INT_1:16;
reconsider l2 =
l2 as
even Nat ;
(
l + (- 1) < l + 0 &
l < len (P .cut n,(len P)) )
by A26, XREAL_1:10;
then
l - 1
< len (P .cut n,(len P))
by XXREAL_0:2;
then A29:
(P .cut n,(len P)) . (l2 + 1) = P . (n + l2)
by A24, GLIB_001:37;
reconsider aa =
P . 3 as
Vertex of
G2 by A22, GLIB_000:def 39;
reconsider bb =
P . (n + l2) as
Vertex of
G2 by A27, A29, GLIB_000:def 39;
A30:
((len (P .cut n,(len P))) + 5) + (- 5) = ((len P) + 1) + (- 5)
by A24, GLIB_001:37;
l + (- 1) < (len (P .cut n,(len P))) + (- 1)
by A26, XREAL_1:10;
then A31:
l2 + n < ((len P) - 5) + n
by A30, XREAL_1:10;
A32:
(k + 2) + 0 < (k + 2) + l2
by A28, XREAL_1:10;
A33:
n + l2 in NAT
by ORDINAL1:def 13;
then
aa,
bb are_adjacent
by A16, Def6;
then consider e being
set such that A35:
e Joins P . 3,
P . (n + l2),
G2
by Def3;
e Joins P . k,
P . (n + l2),
G
by A21, A35, GLIB_000:75;
hence
P is
chordal
by A3, A21, A31, A32, Th85;
:: thesis: verum end;