let G be _finite chordal _Graph; :: thesis: for L being PartFunc of (the_Vertices_of G),NAT st L is with_property_L3 & dom L = the_Vertices_of G holds

for V being VertexScheme of G st V " = L holds

V is perfect

let L be PartFunc of (the_Vertices_of G),NAT; :: thesis: ( L is with_property_L3 & dom L = the_Vertices_of G implies for V being VertexScheme of G st V " = L holds

V is perfect )

assume that

A1: L is with_property_L3 and

A2: dom L = the_Vertices_of G ; :: thesis: for V being VertexScheme of G st V " = L holds

V is perfect

let V be VertexScheme of G; :: thesis: ( V " = L implies V is perfect )

assume A3: V " = L ; :: thesis: V is perfect

A4: V is one-to-one by CHORD:def 12;

A5: for x, y being Vertex of G

for i, j being Nat st i in dom V & j in dom V & V /. i = x & V /. j = y holds

( i < j iff L . x < L . y )_{1}[ Nat] means ex P being Walk of G ex v1, v2, v3, v4 being Vertex of G st

( P is Path-like & P is open & P is chordless & P .length() = $1 - 1 & v1 = P . ((len P) - 2) & v2 = P . 3 & v3 = P .last() & v4 = P .first() & L . v4 > L . v3 & L . v3 > L . v2 & L . v2 > L . v1 & ( for x being set st x in P .vertices() holds

L . x <= L . v4 ) & ( for x being Vertex of G st x <> v4 & x,v2 are_adjacent & not x,v1 are_adjacent holds

L . x < L . v4 ) );

A12: for k being Nat st 4 <= k & S_{1}[k] holds

S_{1}[k + 1]

assume not V is perfect ; :: thesis: contradiction

then consider k being non zero Nat such that

A60: k <= len V and

A61: ex H being inducedSubgraph of G,(V .followSet k) ex v being Vertex of H st

( v = V . k & not v is simplicial ) by CHORD:def 13;

consider HH being inducedSubgraph of G,(V .followSet k), hv being Vertex of HH such that

A62: hv = V . k and

A63: not hv is simplicial by A61;

consider ha, hb being Vertex of HH such that

A64: ha <> hb and

hv <> ha and

hv <> hb and

A65: hv,ha are_adjacent and

A66: hv,hb are_adjacent and

A67: not ha,hb are_adjacent by A63, CHORD:69;

A68: hv in the_Vertices_of HH ;

A69: hb in the_Vertices_of HH ;

ha in the_Vertices_of HH ;

then reconsider v = hv, aa = ha, bb = hb as Vertex of G by A68, A69;

A70: V .followSet k is non empty Subset of (the_Vertices_of G) by A60, CHORD:107;

then A71: the_Vertices_of HH = V .followSet k by GLIB_000:def 37;

A75: a in V .followSet k and

A76: L . a < L . bb and

A77: v,a are_adjacent and

A78: v,bb are_adjacent and

A79: not a,bb are_adjacent ;

defpred S_{2}[ Nat] means ( $1 in dom V & L . a < L . (V /. $1) & a <> V /. $1 & v,V /. $1 are_adjacent & not a,V /. $1 are_adjacent );

A80: rng V = the_Vertices_of G by CHORD:def 12;

A81: ex k being Nat st S_{2}[k]
_{2}[k] holds

k <= len V by FINSEQ_3:25;

consider mb being Nat such that

A85: S_{2}[mb]
and

for n being Nat st S_{2}[n] holds

n <= mb from NAT_1:sch 6(A84, A81);

reconsider v = v, a = a, b = V /. mb as Vertex of G ;

consider ma being object such that

A86: ma in dom V and

A87: a = V . ma by A80, FUNCT_1:def 3;

reconsider ma = ma as Element of NAT by A86;

A88: a = V /. ma by A86, A87, PARTFUN1:def 6;

0 + 1 <= k by NAT_1:13;

then A89: k in dom V by A60, FINSEQ_3:25;

then A94: L . v < L . a by A5, A89, A86, A88, A90;

A95: v <> b by A77, A85;

A96: S_{1}[4]

S_{1}[i]
from NAT_1:sch 8(A96, A12);

then S_{1}[(G .order()) + 11]
by A59, XXREAL_0:2;

then consider P being Walk of G, v1, v2, v3, v4 being Vertex of G such that

A131: P is Path-like and

P is open and

P is chordless and

A132: P .length() = ((G .order()) + 11) - 1 and

v1 = P . ((len P) - 2) and

v2 = P . 3 and

v3 = P .last() and

v4 = P .first() and

L . v4 > L . v3 and

L . v3 > L . v2 and

L . v2 > L . v1 and

for x being Vertex of G st x <> v4 & x,v2 are_adjacent & not x,v1 are_adjacent holds

L . x < L . v4 ;

len P = (2 * ((G .order()) + 10)) + 1 by A132, GLIB_001:112;

then ((2 * (G .order())) + 21) + 1 = 2 * (len (P .vertexSeq())) by GLIB_001:def 14;

then (G .order()) + 11 <= (G .order()) + 1 by A131, GLIB_001:154;

hence contradiction by XREAL_1:8; :: thesis: verum

for V being VertexScheme of G st V " = L holds

V is perfect

let L be PartFunc of (the_Vertices_of G),NAT; :: thesis: ( L is with_property_L3 & dom L = the_Vertices_of G implies for V being VertexScheme of G st V " = L holds

V is perfect )

assume that

A1: L is with_property_L3 and

A2: dom L = the_Vertices_of G ; :: thesis: for V being VertexScheme of G st V " = L holds

V is perfect

let V be VertexScheme of G; :: thesis: ( V " = L implies V is perfect )

assume A3: V " = L ; :: thesis: V is perfect

A4: V is one-to-one by CHORD:def 12;

A5: for x, y being Vertex of G

for i, j being Nat st i in dom V & j in dom V & V /. i = x & V /. j = y holds

( i < j iff L . x < L . y )

proof

defpred S
let x, y be Vertex of G; :: thesis: for i, j being Nat st i in dom V & j in dom V & V /. i = x & V /. j = y holds

( i < j iff L . x < L . y )

let i, j be Nat; :: thesis: ( i in dom V & j in dom V & V /. i = x & V /. j = y implies ( i < j iff L . x < L . y ) )

assume that

A6: i in dom V and

A7: j in dom V and

A8: V /. i = x and

A9: V /. j = y ; :: thesis: ( i < j iff L . x < L . y )

V . j = y by A7, A9, PARTFUN1:def 6;

then A10: L . y = j by A3, A4, A7, FUNCT_1:34;

A11: V . i = x by A6, A8, PARTFUN1:def 6;

hence ( i < j implies L . x < L . y ) by A3, A4, A6, A10, FUNCT_1:34; :: thesis: ( L . x < L . y implies i < j )

thus ( L . x < L . y implies i < j ) by A3, A4, A6, A11, A10, FUNCT_1:34; :: thesis: verum

end;( i < j iff L . x < L . y )

let i, j be Nat; :: thesis: ( i in dom V & j in dom V & V /. i = x & V /. j = y implies ( i < j iff L . x < L . y ) )

assume that

A6: i in dom V and

A7: j in dom V and

A8: V /. i = x and

A9: V /. j = y ; :: thesis: ( i < j iff L . x < L . y )

V . j = y by A7, A9, PARTFUN1:def 6;

then A10: L . y = j by A3, A4, A7, FUNCT_1:34;

A11: V . i = x by A6, A8, PARTFUN1:def 6;

hence ( i < j implies L . x < L . y ) by A3, A4, A6, A10, FUNCT_1:34; :: thesis: ( L . x < L . y implies i < j )

thus ( L . x < L . y implies i < j ) by A3, A4, A6, A11, A10, FUNCT_1:34; :: thesis: verum

( P is Path-like & P is open & P is chordless & P .length() = $1 - 1 & v1 = P . ((len P) - 2) & v2 = P . 3 & v3 = P .last() & v4 = P .first() & L . v4 > L . v3 & L . v3 > L . v2 & L . v2 > L . v1 & ( for x being set st x in P .vertices() holds

L . x <= L . v4 ) & ( for x being Vertex of G st x <> v4 & x,v2 are_adjacent & not x,v1 are_adjacent holds

L . x < L . v4 ) );

A12: for k being Nat st 4 <= k & S

S

proof

A59:
11 <= 11 + (G .order())
by NAT_1:11;
A13:
(2 * 0) + 1 < (2 * 1) + 1
;

let kk be Nat; :: thesis: ( 4 <= kk & S_{1}[kk] implies S_{1}[kk + 1] )

assume that

A14: 4 <= kk and

A15: S_{1}[kk]
; :: thesis: S_{1}[kk + 1]

reconsider k = kk as non zero Nat by A14;

consider P being Walk of G, v1, v2, v3, v4 being Vertex of G such that

A16: P is Path-like and

A17: P is open and

A18: P is chordless and

A19: P .length() = k - 1 and

A20: v1 = P . ((len P) - 2) and

A21: v2 = P . 3 and

A22: v3 = P .last() and

A23: v4 = P .first() and

A24: L . v4 > L . v3 and

A25: L . v3 > L . v2 and

A26: L . v2 > L . v1 and

A27: for x being set st x in P .vertices() holds

L . x <= L . v4 and

A28: for x being Vertex of G st x <> v4 & x,v2 are_adjacent & not x,v1 are_adjacent holds

L . x < L . v4 by A15;

A29: len P = (2 * (k - 1)) + 1 by A19, GLIB_001:112;

2 * k >= 2 * 4 by A14, XREAL_1:64;

then A30: (2 * k) - 1 >= 8 - 1 by XREAL_1:9;

then 1 <= len P by A29, XXREAL_0:2;

then A31: len P in dom P by FINSEQ_3:25;

3 < len P by A29, A30, XXREAL_0:2;

then ex ez being object st ez Joins P . 1,P . 3,G by A16, A17, A18, A13, CHORD:92;

then v4,v2 are_adjacent by A21, A23, CHORD:def 3;

then consider v5 being Vertex of G such that

v5 in dom L and

A34: L . v4 < L . v5 and

A35: v5,v3 are_adjacent and

A36: not v5,v2 are_adjacent and

A37: for x being Vertex of G st x <> v5 & x,v3 are_adjacent & not x,v2 are_adjacent holds

L . x < L . v5 by A1, A2, A24, A25, A33;

consider e being object such that

A38: e Joins P .last() ,v5,G by A22, A35, CHORD:def 3;

set Qr = P .addEdge e;

set Q = (P .addEdge e) .reverse() ;

A44: len ((P .addEdge e) .reverse()) = len (P .addEdge e) by GLIB_001:21;

A45: not v5 in P .vertices() by A27, A34;

then P .addEdge e is open by A16, A17, A18, A38, A43, CHORD:97;

then A46: (P .addEdge e) .reverse() is open by GLIB_001:120;

3 <= len P by A29, A30, XXREAL_0:2;

then A47: 3 in dom P by FINSEQ_3:25;

then A48: 3 in dom (P .addEdge e) by A38, Lm6;

v2 = (P .addEdge e) . 3 by A21, A38, A47, Lm6;

then A49: v2 = ((P .addEdge e) .reverse()) . (((len ((P .addEdge e) .reverse())) - 3) + 1) by A48, A44, GLIB_001:24;

v4 = (P .addEdge e) .first() by A23, A38, GLIB_001:63;

then A50: v4 = ((P .addEdge e) .reverse()) .last() by GLIB_001:22;

A51: len (P .addEdge e) = (len P) + 2 by A38, GLIB_001:64;

then A52: (len (P .addEdge e)) - 2 in dom (P .addEdge e) by A38, A31, Lm6;

v3 = (P .addEdge e) . ((len (P .addEdge e)) - 2) by A22, A38, A51, A31, Lm6;

then A53: v3 = ((P .addEdge e) .reverse()) . (((len ((P .addEdge e) .reverse())) - ((len (P .addEdge e)) - 2)) + 1) by A52, A44, GLIB_001:24;

v5 = (P .addEdge e) .last() by A38, GLIB_001:63;

then A54: v5 = ((P .addEdge e) .reverse()) .first() by GLIB_001:22;

P .addEdge e is chordless by A16, A17, A18, A38, A45, A43, CHORD:97;

then A55: (P .addEdge e) .reverse() is chordless by CHORD:91;

(P .addEdge e) .length() = (k - 1) + 1 by A19, A38, Lm4;

then A56: ((P .addEdge e) .reverse()) .length() = (k + 1) - 1 by Lm5;

hence S_{1}[kk + 1]
by A24, A25, A34, A37, A46, A55, A56, A44, A49, A53, A50, A54, A57; :: thesis: verum

end;let kk be Nat; :: thesis: ( 4 <= kk & S

assume that

A14: 4 <= kk and

A15: S

reconsider k = kk as non zero Nat by A14;

consider P being Walk of G, v1, v2, v3, v4 being Vertex of G such that

A16: P is Path-like and

A17: P is open and

A18: P is chordless and

A19: P .length() = k - 1 and

A20: v1 = P . ((len P) - 2) and

A21: v2 = P . 3 and

A22: v3 = P .last() and

A23: v4 = P .first() and

A24: L . v4 > L . v3 and

A25: L . v3 > L . v2 and

A26: L . v2 > L . v1 and

A27: for x being set st x in P .vertices() holds

L . x <= L . v4 and

A28: for x being Vertex of G st x <> v4 & x,v2 are_adjacent & not x,v1 are_adjacent holds

L . x < L . v4 by A15;

A29: len P = (2 * (k - 1)) + 1 by A19, GLIB_001:112;

2 * k >= 2 * 4 by A14, XREAL_1:64;

then A30: (2 * k) - 1 >= 8 - 1 by XREAL_1:9;

then 1 <= len P by A29, XXREAL_0:2;

then A31: len P in dom P by FINSEQ_3:25;

now :: thesis: for e being object holds not e Joins v4,v3,G

then A33:
not v4,v3 are_adjacent
by CHORD:def 3;A32:
(2 * 0) + 1 < len P
by A29, A30, XXREAL_0:2;

let e be object ; :: thesis: not e Joins v4,v3,G

assume e Joins v4,v3,G ; :: thesis: contradiction

then 1 + 2 = len P by A16, A17, A18, A22, A23, A32, CHORD:92;

hence contradiction by A14, A29; :: thesis: verum

end;let e be object ; :: thesis: not e Joins v4,v3,G

assume e Joins v4,v3,G ; :: thesis: contradiction

then 1 + 2 = len P by A16, A17, A18, A22, A23, A32, CHORD:92;

hence contradiction by A14, A29; :: thesis: verum

3 < len P by A29, A30, XXREAL_0:2;

then ex ez being object st ez Joins P . 1,P . 3,G by A16, A17, A18, A13, CHORD:92;

then v4,v2 are_adjacent by A21, A23, CHORD:def 3;

then consider v5 being Vertex of G such that

v5 in dom L and

A34: L . v4 < L . v5 and

A35: v5,v3 are_adjacent and

A36: not v5,v2 are_adjacent and

A37: for x being Vertex of G st x <> v5 & x,v3 are_adjacent & not x,v2 are_adjacent holds

L . x < L . v5 by A1, A2, A24, A25, A33;

consider e being object such that

A38: e Joins P .last() ,v5,G by A22, A35, CHORD:def 3;

now :: thesis: not v5,v1 are_adjacent

then A43:
for e being object holds not e Joins P . ((len P) - 2),v5,G
by A20, CHORD:def 3;
L . v2 < L . v4
by A24, A25, XXREAL_0:2;

then A39: L . v2 < L . v5 by A34, XXREAL_0:2;

assume v5,v1 are_adjacent ; :: thesis: contradiction

then consider v6 being Vertex of G such that

v6 in dom L and

A40: L . v5 < L . v6 and

A41: v6,v2 are_adjacent and

A42: not v6,v1 are_adjacent and

for x being Vertex of G st x <> v6 & x,v2 are_adjacent & not x,v1 are_adjacent holds

L . x < L . v6 by A1, A2, A26, A36, A39;

thus contradiction by A28, A34, A40, A41, A42, XXREAL_0:2; :: thesis: verum

end;then A39: L . v2 < L . v5 by A34, XXREAL_0:2;

assume v5,v1 are_adjacent ; :: thesis: contradiction

then consider v6 being Vertex of G such that

v6 in dom L and

A40: L . v5 < L . v6 and

A41: v6,v2 are_adjacent and

A42: not v6,v1 are_adjacent and

for x being Vertex of G st x <> v6 & x,v2 are_adjacent & not x,v1 are_adjacent holds

L . x < L . v6 by A1, A2, A26, A36, A39;

thus contradiction by A28, A34, A40, A41, A42, XXREAL_0:2; :: thesis: verum

set Qr = P .addEdge e;

set Q = (P .addEdge e) .reverse() ;

A44: len ((P .addEdge e) .reverse()) = len (P .addEdge e) by GLIB_001:21;

A45: not v5 in P .vertices() by A27, A34;

then P .addEdge e is open by A16, A17, A18, A38, A43, CHORD:97;

then A46: (P .addEdge e) .reverse() is open by GLIB_001:120;

3 <= len P by A29, A30, XXREAL_0:2;

then A47: 3 in dom P by FINSEQ_3:25;

then A48: 3 in dom (P .addEdge e) by A38, Lm6;

v2 = (P .addEdge e) . 3 by A21, A38, A47, Lm6;

then A49: v2 = ((P .addEdge e) .reverse()) . (((len ((P .addEdge e) .reverse())) - 3) + 1) by A48, A44, GLIB_001:24;

v4 = (P .addEdge e) .first() by A23, A38, GLIB_001:63;

then A50: v4 = ((P .addEdge e) .reverse()) .last() by GLIB_001:22;

A51: len (P .addEdge e) = (len P) + 2 by A38, GLIB_001:64;

then A52: (len (P .addEdge e)) - 2 in dom (P .addEdge e) by A38, A31, Lm6;

v3 = (P .addEdge e) . ((len (P .addEdge e)) - 2) by A22, A38, A51, A31, Lm6;

then A53: v3 = ((P .addEdge e) .reverse()) . (((len ((P .addEdge e) .reverse())) - ((len (P .addEdge e)) - 2)) + 1) by A52, A44, GLIB_001:24;

v5 = (P .addEdge e) .last() by A38, GLIB_001:63;

then A54: v5 = ((P .addEdge e) .reverse()) .first() by GLIB_001:22;

P .addEdge e is chordless by A16, A17, A18, A38, A45, A43, CHORD:97;

then A55: (P .addEdge e) .reverse() is chordless by CHORD:91;

(P .addEdge e) .length() = (k - 1) + 1 by A19, A38, Lm4;

then A56: ((P .addEdge e) .reverse()) .length() = (k + 1) - 1 by Lm5;

A57: now :: thesis: for x being set st x in ((P .addEdge e) .reverse()) .vertices() holds

L . x <= L . v5

P .addEdge e is Path-like
by A16, A17, A18, A38, A45, A43, CHORD:97;L . x <= L . v5

let x be set ; :: thesis: ( x in ((P .addEdge e) .reverse()) .vertices() implies L . b_{1} <= L . v5 )

assume x in ((P .addEdge e) .reverse()) .vertices() ; :: thesis: L . b_{1} <= L . v5

then x in (P .addEdge e) .vertices() by GLIB_001:92;

then A58: x in (P .vertices()) \/ {v5} by A38, GLIB_001:95;

end;assume x in ((P .addEdge e) .reverse()) .vertices() ; :: thesis: L . b

then x in (P .addEdge e) .vertices() by GLIB_001:92;

then A58: x in (P .vertices()) \/ {v5} by A38, GLIB_001:95;

hence S

assume not V is perfect ; :: thesis: contradiction

then consider k being non zero Nat such that

A60: k <= len V and

A61: ex H being inducedSubgraph of G,(V .followSet k) ex v being Vertex of H st

( v = V . k & not v is simplicial ) by CHORD:def 13;

consider HH being inducedSubgraph of G,(V .followSet k), hv being Vertex of HH such that

A62: hv = V . k and

A63: not hv is simplicial by A61;

consider ha, hb being Vertex of HH such that

A64: ha <> hb and

hv <> ha and

hv <> hb and

A65: hv,ha are_adjacent and

A66: hv,hb are_adjacent and

A67: not ha,hb are_adjacent by A63, CHORD:69;

A68: hv in the_Vertices_of HH ;

A69: hb in the_Vertices_of HH ;

ha in the_Vertices_of HH ;

then reconsider v = hv, aa = ha, bb = hb as Vertex of G by A68, A69;

A70: V .followSet k is non empty Subset of (the_Vertices_of G) by A60, CHORD:107;

then A71: the_Vertices_of HH = V .followSet k by GLIB_000:def 37;

now :: thesis: ex aa, bb being Vertex of G st

( aa in V .followSet k & L . aa < L . bb & v,aa are_adjacent & v,bb are_adjacent & not aa,bb are_adjacent )

then consider a, bb being Vertex of G such that ( aa in V .followSet k & L . aa < L . bb & v,aa are_adjacent & v,bb are_adjacent & not aa,bb are_adjacent )

A72:
L . aa <> L . bb
by A2, A3, A4, A64, FUNCT_1:def 4;

end;per cases
( L . aa < L . bb or L . aa > L . bb )
by A72, XXREAL_0:1;

end;

suppose A73:
L . aa < L . bb
; :: thesis: ex aa, bb being Vertex of G st

( aa in V .followSet k & L . aa < L . bb & v,aa are_adjacent & v,bb are_adjacent & not aa,bb are_adjacent )

( aa in V .followSet k & L . aa < L . bb & v,aa are_adjacent & v,bb are_adjacent & not aa,bb are_adjacent )

take aa = aa; :: thesis: ex bb being Vertex of G st

( aa in V .followSet k & L . aa < L . bb & v,aa are_adjacent & v,bb are_adjacent & not aa,bb are_adjacent )

take bb = bb; :: thesis: ( aa in V .followSet k & L . aa < L . bb & v,aa are_adjacent & v,bb are_adjacent & not aa,bb are_adjacent )

thus aa in V .followSet k by A71; :: thesis: ( L . aa < L . bb & v,aa are_adjacent & v,bb are_adjacent & not aa,bb are_adjacent )

thus L . aa < L . bb by A73; :: thesis: ( v,aa are_adjacent & v,bb are_adjacent & not aa,bb are_adjacent )

thus v,aa are_adjacent by A65, A70, CHORD:45; :: thesis: ( v,bb are_adjacent & not aa,bb are_adjacent )

thus v,bb are_adjacent by A66, A70, CHORD:45; :: thesis: not aa,bb are_adjacent

thus not aa,bb are_adjacent by A67, A70, CHORD:45; :: thesis: verum

end;( aa in V .followSet k & L . aa < L . bb & v,aa are_adjacent & v,bb are_adjacent & not aa,bb are_adjacent )

take bb = bb; :: thesis: ( aa in V .followSet k & L . aa < L . bb & v,aa are_adjacent & v,bb are_adjacent & not aa,bb are_adjacent )

thus aa in V .followSet k by A71; :: thesis: ( L . aa < L . bb & v,aa are_adjacent & v,bb are_adjacent & not aa,bb are_adjacent )

thus L . aa < L . bb by A73; :: thesis: ( v,aa are_adjacent & v,bb are_adjacent & not aa,bb are_adjacent )

thus v,aa are_adjacent by A65, A70, CHORD:45; :: thesis: ( v,bb are_adjacent & not aa,bb are_adjacent )

thus v,bb are_adjacent by A66, A70, CHORD:45; :: thesis: not aa,bb are_adjacent

thus not aa,bb are_adjacent by A67, A70, CHORD:45; :: thesis: verum

suppose A74:
L . aa > L . bb
; :: thesis: ex bb, aa being Vertex of G st

( bb in V .followSet k & L . aa > L . bb & v,bb are_adjacent & v,aa are_adjacent & not bb,aa are_adjacent )

( bb in V .followSet k & L . aa > L . bb & v,bb are_adjacent & v,aa are_adjacent & not bb,aa are_adjacent )

take bb = bb; :: thesis: ex aa being Vertex of G st

( bb in V .followSet k & L . aa > L . bb & v,bb are_adjacent & v,aa are_adjacent & not bb,aa are_adjacent )

take aa = aa; :: thesis: ( bb in V .followSet k & L . aa > L . bb & v,bb are_adjacent & v,aa are_adjacent & not bb,aa are_adjacent )

thus bb in V .followSet k by A71; :: thesis: ( L . aa > L . bb & v,bb are_adjacent & v,aa are_adjacent & not bb,aa are_adjacent )

thus L . aa > L . bb by A74; :: thesis: ( v,bb are_adjacent & v,aa are_adjacent & not bb,aa are_adjacent )

thus v,bb are_adjacent by A66, A70, CHORD:45; :: thesis: ( v,aa are_adjacent & not bb,aa are_adjacent )

thus v,aa are_adjacent by A65, A70, CHORD:45; :: thesis: not bb,aa are_adjacent

thus not bb,aa are_adjacent by A67, A70, CHORD:45; :: thesis: verum

end;( bb in V .followSet k & L . aa > L . bb & v,bb are_adjacent & v,aa are_adjacent & not bb,aa are_adjacent )

take aa = aa; :: thesis: ( bb in V .followSet k & L . aa > L . bb & v,bb are_adjacent & v,aa are_adjacent & not bb,aa are_adjacent )

thus bb in V .followSet k by A71; :: thesis: ( L . aa > L . bb & v,bb are_adjacent & v,aa are_adjacent & not bb,aa are_adjacent )

thus L . aa > L . bb by A74; :: thesis: ( v,bb are_adjacent & v,aa are_adjacent & not bb,aa are_adjacent )

thus v,bb are_adjacent by A66, A70, CHORD:45; :: thesis: ( v,aa are_adjacent & not bb,aa are_adjacent )

thus v,aa are_adjacent by A65, A70, CHORD:45; :: thesis: not bb,aa are_adjacent

thus not bb,aa are_adjacent by A67, A70, CHORD:45; :: thesis: verum

A75: a in V .followSet k and

A76: L . a < L . bb and

A77: v,a are_adjacent and

A78: v,bb are_adjacent and

A79: not a,bb are_adjacent ;

defpred S

A80: rng V = the_Vertices_of G by CHORD:def 12;

A81: ex k being Nat st S

proof

A84:
for k being Nat st S
consider mbb being object such that

A82: mbb in dom V and

A83: bb = V . mbb by A80, FUNCT_1:def 3;

reconsider mbb = mbb as Element of NAT by A82;

take mbb ; :: thesis: S_{2}[mbb]

thus mbb in dom V by A82; :: thesis: ( L . a < L . (V /. mbb) & a <> V /. mbb & v,V /. mbb are_adjacent & not a,V /. mbb are_adjacent )

thus L . a < L . (V /. mbb) by A76, A82, A83, PARTFUN1:def 6; :: thesis: ( a <> V /. mbb & v,V /. mbb are_adjacent & not a,V /. mbb are_adjacent )

thus a <> V /. mbb by A76, A82, A83, PARTFUN1:def 6; :: thesis: ( v,V /. mbb are_adjacent & not a,V /. mbb are_adjacent )

thus v,V /. mbb are_adjacent by A78, A82, A83, PARTFUN1:def 6; :: thesis: not a,V /. mbb are_adjacent

thus not a,V /. mbb are_adjacent by A79, A82, A83, PARTFUN1:def 6; :: thesis: verum

end;A82: mbb in dom V and

A83: bb = V . mbb by A80, FUNCT_1:def 3;

reconsider mbb = mbb as Element of NAT by A82;

take mbb ; :: thesis: S

thus mbb in dom V by A82; :: thesis: ( L . a < L . (V /. mbb) & a <> V /. mbb & v,V /. mbb are_adjacent & not a,V /. mbb are_adjacent )

thus L . a < L . (V /. mbb) by A76, A82, A83, PARTFUN1:def 6; :: thesis: ( a <> V /. mbb & v,V /. mbb are_adjacent & not a,V /. mbb are_adjacent )

thus a <> V /. mbb by A76, A82, A83, PARTFUN1:def 6; :: thesis: ( v,V /. mbb are_adjacent & not a,V /. mbb are_adjacent )

thus v,V /. mbb are_adjacent by A78, A82, A83, PARTFUN1:def 6; :: thesis: not a,V /. mbb are_adjacent

thus not a,V /. mbb are_adjacent by A79, A82, A83, PARTFUN1:def 6; :: thesis: verum

k <= len V by FINSEQ_3:25;

consider mb being Nat such that

A85: S

for n being Nat st S

n <= mb from NAT_1:sch 6(A84, A81);

reconsider v = v, a = a, b = V /. mb as Vertex of G ;

consider ma being object such that

A86: ma in dom V and

A87: a = V . ma by A80, FUNCT_1:def 3;

reconsider ma = ma as Element of NAT by A86;

A88: a = V /. ma by A86, A87, PARTFUN1:def 6;

0 + 1 <= k by NAT_1:13;

then A89: k in dom V by A60, FINSEQ_3:25;

A90: now :: thesis: not ma <= k

A93:
v = V /. k
by A62, A89, PARTFUN1:def 6;assume
ma <= k
; :: thesis: contradiction

then A91: ma < k by A62, A78, A79, A87, XXREAL_0:1;

a in the_Vertices_of G ;

then A92: a in rng V by CHORD:def 12;

V is one-to-one by CHORD:def 12;

then a .. V >= k by A75, A89, A92, CHORD:16;

then a .. V > ma by A91, XXREAL_0:2;

hence contradiction by A86, A87, FINSEQ_4:24; :: thesis: verum

end;then A91: ma < k by A62, A78, A79, A87, XXREAL_0:1;

a in the_Vertices_of G ;

then A92: a in rng V by CHORD:def 12;

V is one-to-one by CHORD:def 12;

then a .. V >= k by A75, A89, A92, CHORD:16;

then a .. V > ma by A91, XXREAL_0:2;

hence contradiction by A86, A87, FINSEQ_4:24; :: thesis: verum

then A94: L . v < L . a by A5, A89, A86, A88, A90;

A95: v <> b by A77, A85;

A96: S

proof

for i being Nat st 4 <= i holds
A97:
L . a > L . v
by A5, A89, A93, A86, A88, A90;

consider c being Vertex of G such that

c in dom L and

A98: L . b < L . c and

A99: c,a are_adjacent and

A100: not c,v are_adjacent and

A101: for x being Vertex of G st x <> c & x,a are_adjacent & not x,v are_adjacent holds

L . x < L . c by A1, A2, A85, A94;

consider P being Path of G, e1, e2 being object such that

A102: P is open and

A103: len P = 5 and

A104: P .length() = 2 and

e1 Joins b,v,G and

e2 Joins v,a,G and

P .edges() = {e1,e2} and

A105: P .vertices() = {b,v,a} and

A106: P . 1 = b and

A107: P . 3 = v and

A108: P . 5 = a by A77, A85, A95, CHORD:47;

consider e being object such that

A109: e Joins P .last() ,c,G by A99, A103, A108, CHORD:def 3;

set Qr = P .addEdge e;

set Q = (P .addEdge e) .reverse() ;

A110: (P .addEdge e) .last() = c by A109, GLIB_001:63;

A111: len (P .addEdge e) = 5 + 2 by A103, A109, GLIB_001:64;

then A112: 1 in dom (P .addEdge e) by FINSEQ_3:25;

5 in dom P by A103, FINSEQ_3:25;

then A113: (P .addEdge e) . 5 = a by A108, A109, GLIB_001:65;

5 in dom (P .addEdge e) by A111, FINSEQ_3:25;

then A114: a = ((P .addEdge e) .reverse()) . ((7 - 5) + 1) by A111, A113, GLIB_001:24;

7 in dom (P .addEdge e) by A111, FINSEQ_3:25;

then c = ((P .addEdge e) .reverse()) . ((7 - 7) + 1) by A111, A110, GLIB_001:24;

then A115: c = ((P .addEdge e) .reverse()) .first() ;

3 in dom P by A103, FINSEQ_3:25;

then A116: (P .addEdge e) . 3 = v by A107, A109, GLIB_001:65;

(P .addEdge e) .length() = 2 + 1 by A104, A109, Lm4;

then A117: ((P .addEdge e) .reverse()) .length() = (3 + 1) - 1 by Lm5;

1 in dom P by A103, FINSEQ_3:25;

then (P .addEdge e) . 1 = b by A106, A109, GLIB_001:65;

then b = ((P .addEdge e) .reverse()) . (((len (P .addEdge e)) - 1) + 1) by A112, GLIB_001:24;

then A118: b = ((P .addEdge e) .reverse()) .last() by GLIB_001:21;

A119: len ((P .addEdge e) .reverse()) = len (P .addEdge e) by GLIB_001:21;

A120: P .first() = b by A106;

P .last() = a by A103, A108;

then A121: P is chordless by A85, A103, A120, CHORD:90;

A125: for e being object holds not e Joins P . ((len P) - 2),c,G by A100, A103, A107, CHORD:def 3;

then P .addEdge e is open by A102, A121, A109, A124, CHORD:97;

then A126: (P .addEdge e) .reverse() is open by GLIB_001:120;

then v = ((P .addEdge e) .reverse()) . ((7 - 3) + 1) by A111, A116, GLIB_001:24;

then A129: v = ((P .addEdge e) .reverse()) . ((len ((P .addEdge e) .reverse())) - 2) by A111, A119;

P .addEdge e is chordless by A102, A121, A109, A124, A125, CHORD:97;

then A130: (P .addEdge e) .reverse() is chordless by CHORD:91;

P .addEdge e is Path-like by A102, A121, A109, A124, A125, CHORD:97;

hence S_{1}[4]
by A85, A98, A101, A126, A130, A117, A114, A129, A118, A115, A97, A127; :: thesis: verum

end;consider c being Vertex of G such that

c in dom L and

A98: L . b < L . c and

A99: c,a are_adjacent and

A100: not c,v are_adjacent and

A101: for x being Vertex of G st x <> c & x,a are_adjacent & not x,v are_adjacent holds

L . x < L . c by A1, A2, A85, A94;

consider P being Path of G, e1, e2 being object such that

A102: P is open and

A103: len P = 5 and

A104: P .length() = 2 and

e1 Joins b,v,G and

e2 Joins v,a,G and

P .edges() = {e1,e2} and

A105: P .vertices() = {b,v,a} and

A106: P . 1 = b and

A107: P . 3 = v and

A108: P . 5 = a by A77, A85, A95, CHORD:47;

consider e being object such that

A109: e Joins P .last() ,c,G by A99, A103, A108, CHORD:def 3;

set Qr = P .addEdge e;

set Q = (P .addEdge e) .reverse() ;

A110: (P .addEdge e) .last() = c by A109, GLIB_001:63;

A111: len (P .addEdge e) = 5 + 2 by A103, A109, GLIB_001:64;

then A112: 1 in dom (P .addEdge e) by FINSEQ_3:25;

5 in dom P by A103, FINSEQ_3:25;

then A113: (P .addEdge e) . 5 = a by A108, A109, GLIB_001:65;

5 in dom (P .addEdge e) by A111, FINSEQ_3:25;

then A114: a = ((P .addEdge e) .reverse()) . ((7 - 5) + 1) by A111, A113, GLIB_001:24;

7 in dom (P .addEdge e) by A111, FINSEQ_3:25;

then c = ((P .addEdge e) .reverse()) . ((7 - 7) + 1) by A111, A110, GLIB_001:24;

then A115: c = ((P .addEdge e) .reverse()) .first() ;

3 in dom P by A103, FINSEQ_3:25;

then A116: (P .addEdge e) . 3 = v by A107, A109, GLIB_001:65;

(P .addEdge e) .length() = 2 + 1 by A104, A109, Lm4;

then A117: ((P .addEdge e) .reverse()) .length() = (3 + 1) - 1 by Lm5;

1 in dom P by A103, FINSEQ_3:25;

then (P .addEdge e) . 1 = b by A106, A109, GLIB_001:65;

then b = ((P .addEdge e) .reverse()) . (((len (P .addEdge e)) - 1) + 1) by A112, GLIB_001:24;

then A118: b = ((P .addEdge e) .reverse()) .last() by GLIB_001:21;

A119: len ((P .addEdge e) .reverse()) = len (P .addEdge e) by GLIB_001:21;

A120: P .first() = b by A106;

P .last() = a by A103, A108;

then A121: P is chordless by A85, A103, A120, CHORD:90;

A122: now :: thesis: for x being set st x in P .vertices() holds

L . x <= L . b

then A124:
not c in P .vertices()
by A98;L . x <= L . b

let x be set ; :: thesis: ( x in P .vertices() implies L . b_{1} <= L . b )

assume A123: x in P .vertices() ; :: thesis: L . b_{1} <= L . b

end;assume A123: x in P .vertices() ; :: thesis: L . b

A125: for e being object holds not e Joins P . ((len P) - 2),c,G by A100, A103, A107, CHORD:def 3;

then P .addEdge e is open by A102, A121, A109, A124, CHORD:97;

then A126: (P .addEdge e) .reverse() is open by GLIB_001:120;

A127: now :: thesis: for x being set st x in ((P .addEdge e) .reverse()) .vertices() holds

L . x <= L . c

3 in dom (P .addEdge e)
by A111, FINSEQ_3:25;L . x <= L . c

let x be set ; :: thesis: ( x in ((P .addEdge e) .reverse()) .vertices() implies L . b_{1} <= L . c )

assume x in ((P .addEdge e) .reverse()) .vertices() ; :: thesis: L . b_{1} <= L . c

then x in (P .addEdge e) .vertices() by GLIB_001:92;

then A128: x in (P .vertices()) \/ {c} by A109, GLIB_001:95;

end;assume x in ((P .addEdge e) .reverse()) .vertices() ; :: thesis: L . b

then x in (P .addEdge e) .vertices() by GLIB_001:92;

then A128: x in (P .vertices()) \/ {c} by A109, GLIB_001:95;

then v = ((P .addEdge e) .reverse()) . ((7 - 3) + 1) by A111, A116, GLIB_001:24;

then A129: v = ((P .addEdge e) .reverse()) . ((len ((P .addEdge e) .reverse())) - 2) by A111, A119;

P .addEdge e is chordless by A102, A121, A109, A124, A125, CHORD:97;

then A130: (P .addEdge e) .reverse() is chordless by CHORD:91;

P .addEdge e is Path-like by A102, A121, A109, A124, A125, CHORD:97;

hence S

S

then S

then consider P being Walk of G, v1, v2, v3, v4 being Vertex of G such that

A131: P is Path-like and

P is open and

P is chordless and

A132: P .length() = ((G .order()) + 11) - 1 and

v1 = P . ((len P) - 2) and

v2 = P . 3 and

v3 = P .last() and

v4 = P .first() and

L . v4 > L . v3 and

L . v3 > L . v2 and

L . v2 > L . v1 and

for x being Vertex of G st x <> v4 & x,v2 are_adjacent & not x,v1 are_adjacent holds

L . x < L . v4 ;

len P = (2 * ((G .order()) + 10)) + 1 by A132, GLIB_001:112;

then ((2 * (G .order())) + 21) + 1 = 2 * (len (P .vertexSeq())) by GLIB_001:def 14;

then (G .order()) + 11 <= (G .order()) + 1 by A131, GLIB_001:154;

hence contradiction by XREAL_1:8; :: thesis: verum