reconsider n = (2 * 2) + 1 as odd Nat ;
reconsider m = (2 * 0) + 1 as odd Nat ;
let G be _finite _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 & 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
; G is chordal
let P be Walk of G; CHORD:def 11 ( P .length() > 3 & P is Cycle-like implies P is chordal )
assume that
A2:
P .length() > 3
and
A3:
P is Cycle-like
; P is chordal
P .length() >= 3 + 1
by A2, NAT_1:13;
then
2 * (P .length()) >= 2 * 4
by XREAL_1:64;
then
(2 * (P .length())) + 1 >= 8 + 1
by XREAL_1:7;
then A4:
len P >= 9
by GLIB_001:112;
per cases
( ex e being object st e Joins P . m,P . n,G or for e being object holds not e Joins P . m,P . n,G )
;
suppose A11:
for
e being
object holds not
e Joins P . m,
P . n,
G
;
P is chordal reconsider Pn =
P . n as
Vertex of
G by A4, GLIB_001:7, XXREAL_0:2;
reconsider Pm =
P . m as
Vertex of
G by A4, GLIB_001:7, XXREAL_0:2;
set P5l =
P .cut (
n,
(len P));
consider S being
VertexSeparator of
Pm,
Pn such that A12:
S is
minimal
by Th78;
set G2 = the
inducedSubgraph of
G,
S;
A13:
n <= len P
by A4, XXREAL_0:2;
then
P .cut (
n,
(len P))
is_Walk_from P . n,
P . (len P)
by GLIB_001:37;
then A14:
P .cut (
n,
(len P))
is_Walk_from P . n,
P . m
by A3, GLIB_001:118;
A15:
not
Pm,
Pn are_adjacent
by A11;
then
S is
VertexSeparator of
Pn,
Pm
by A5, Th69;
then consider l being
odd Nat such that A16:
1
< l
and A17:
l < len (P .cut (n,(len P)))
and A18:
(P .cut (n,(len P))) . l in S
by A5, A15, A14, Th71;
A19:
1
+ (- 1) < l + (- 1)
by A16, XREAL_1:8;
then reconsider l2 =
l - 1 as
even Element of
NAT by INT_1:3;
reconsider l2 =
l2 as
even Nat ;
A20:
l + (- 1) < (len (P .cut (n,(len P)))) + (- 1)
by A17, XREAL_1:8;
((len (P .cut (n,(len P)))) + 5) + (- 5) = ((len P) + 1) + (- 5)
by A13, GLIB_001:36;
then A21:
l2 + n < ((len P) - 5) + n
by A20, XREAL_1:8;
l + (- 1) < l + 0
by XREAL_1:8;
then
l - 1
< len (P .cut (n,(len P)))
by A17, XXREAL_0:2;
then
(P .cut (n,(len P))) . (l2 + 1) = P . (n + l2)
by A13, GLIB_001:36;
then reconsider bb =
P . (n + l2) as
Vertex of the
inducedSubgraph of
G,
S by A18, GLIB_000:def 37;
set P15 =
P .cut (
m,
n);
A22:
n <= len P
by A4, XXREAL_0:2;
then A23:
P .cut (
m,
n)
is_Walk_from P . m,
P . n
by GLIB_001:37;
then
not
S is
empty
by A5, A15, Th72;
then A24:
the
inducedSubgraph of
G,
S is
complete
by A1, A5, A15, A12;
A25:
((len (P .cut (m,n))) + 1) + (- 1) = (5 + 1) + (- 1)
by A22, GLIB_001:36;
then consider k being
odd Nat such that A26:
m < k
and A27:
k < n
and A28:
(P .cut (m,n)) . k in S
by A5, A15, A23, Th71;
A29:
k <= 5
- 2
by A27, Th3;
A30:
1
+ 2
<= k
by A26, Th4;
then A31:
k = 3
by A29, XXREAL_0:1;
(P .cut (m,n)) . (2 + 1) = P . (1 + 2)
by A22, A25, GLIB_001:36;
then
P . 3
in S
by A28, A30, A29, XXREAL_0:1;
then reconsider aa =
P . 3 as
Vertex of the
inducedSubgraph of
G,
S by GLIB_000:def 37;
A32:
(k + 2) + 0 < (k + 2) + l2
by A19, XREAL_1:8;
A33:
n + l2 in NAT
by ORDINAL1:def 12;
then
aa,
bb are_adjacent
by A24;
then consider e being
object such that A35:
e Joins P . 3,
P . (n + l2), the
inducedSubgraph of
G,
S
;
e Joins P . k,
P . (n + l2),
G
by A31, A35, GLIB_000:72;
hence
P is
chordal
by A3, A31, A21, A32, Th84;
verum end;