reconsider n = (2 * 2) + 1 as odd Nat ;

reconsider m = (2 * 0) + 1 as odd Nat ;

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 that

A2: P .length() > 3 and

A3: P is Cycle-like ; :: thesis: 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;

reconsider m = (2 * 0) + 1 as odd Nat ;

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 that

A2: P .length() > 3 and

A3: P is Cycle-like ; :: thesis: 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;

A5: now :: thesis: not P . m = P . n

assume A6:
P . m = P . n
; :: thesis: contradiction

n <= len P by A4, XXREAL_0:2;

then n = len P by A3, A6, GLIB_001:def 28;

hence contradiction by A4; :: thesis: verum

end;n <= len P by A4, XXREAL_0:2;

then n = len P by A3, A6, GLIB_001:def 28;

hence contradiction by A4; :: thesis: verum

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 )
;

end;

suppose A7:
ex e being object st e Joins P . m,P . n,G
; :: thesis: P is chordal

A8:
m + 2 < n
;

(len P) + (- 2) >= 9 + (- 2) by A4, XREAL_1:7;

then A9: ( not m = 1 or not n = (len P) - 2 ) ;

A10: ( not m = 1 or not n = len P ) by A4;

n <= len P by A4, XXREAL_0:2;

hence P is chordal by A3, A7, A8, A10, A9, Th84; :: thesis: verum

end;(len P) + (- 2) >= 9 + (- 2) by A4, XREAL_1:7;

then A9: ( not m = 1 or not n = (len P) - 2 ) ;

A10: ( not m = 1 or not n = len P ) by A4;

n <= len P by A4, XXREAL_0:2;

hence P is chordal by A3, A7, A8, A10, A9, Th84; :: thesis: verum

suppose A11:
for e being object holds not e Joins P . m,P . n,G
; :: thesis: 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 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; :: thesis: verum

end;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;

now :: thesis: not aa = bb

then
aa,bb are_adjacent
by A24;assume A34:
aa = bb
; :: thesis: contradiction

k < n + l2 by A31, A32, XXREAL_0:2;

hence contradiction by A3, A31, A21, A33, A34, GLIB_001:def 28; :: thesis: verum

end;k < n + l2 by A31, A32, XXREAL_0:2;

hence contradiction by A3, A31, A21, A33, A34, GLIB_001:def 28; :: thesis: verum

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; :: thesis: verum