:: Chordal Graphs :: by Broderick Arneson and Piotr Rudnicki :: :: Received August 18, 2006 :: Copyright (c) 2006-2012 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, XCMPLX_0, ORDINAL1, ARYTM_1, XXREAL_0, NAT_1, CARD_1, ARYTM_3, ABIAN, SUBSET_1, RELAT_1, INT_1, FINSEQ_1, FUNCT_1, FINSEQ_4, XBOOLE_0, FINSET_1, GRAPH_2, ORDINAL4, GLIB_000, GLIB_001, TARSKI, ZFMISC_1, RCOMP_1, GRAPH_1, RELAT_2, REWRITE1, FUNCOP_1, GLIB_002, PARTFUN1, MEMBERED, TOPGEN_1, CHORD; notations TARSKI, XBOOLE_0, SUBSET_1, XXREAL_2, ORDINAL1, INT_1, XCMPLX_0, XXREAL_0, DOMAIN_1, RELAT_1, FUNCT_1, FUNCT_2, FINSEQ_1, CARD_1, FINSET_1, NAT_1, ZFMISC_1, GLIB_000, GLIB_001, GLIB_002, FUNCOP_1, ABIAN, ENUMSET1, FINSEQ_4, NUMBERS, GRAPH_2, MEMBERED; constructors DOMAIN_1, REAL_1, NAT_D, FINSEQ_4, GRAPH_2, GLIB_001, GLIB_002, VALUED_1, XXREAL_2, RELSET_1; registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1, FINSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1, MEMBERED, FINSEQ_1, GLIB_000, ABIAN, GRAPH_2, GLIB_001, GLIB_002, FUNCT_2, XXREAL_2, CARD_1, RELSET_1; requirements ARITHM, BOOLE, NUMERALS, REAL, SUBSET; definitions TARSKI, XBOOLE_0, GLIB_000, GLIB_001, GLIB_002, FUNCOP_1; theorems FINSEQ_1, FUNCT_1, GLIB_000, GLIB_001, GLIB_002, GRAPH_2, GRAPH_3, TREES_1, INT_1, JORDAN12, NAT_1, ORDINAL1, RELAT_1, TARSKI, XBOOLE_0, XBOOLE_1, FUNCOP_1, FUNCT_2, FINSEQ_3, FINSEQ_4, ZFMISC_1, ABIAN, CARD_2, ENUMSET1, FINSEQ_2, XREAL_1, MEMBERED, FINSEQ_5, XXREAL_0, NAT_D, PARTFUN1, XXREAL_2, PRE_POLY; schemes NAT_1, GRAPH_5, FUNCT_2, FRAENKEL; begin :: Preliminaries theorem Th1: for n being non zero Nat holds n-1 is Nat & 1 <= n proof let n be non zero Nat; A1: 0+1 <= n by NAT_1:13; then 0+1-1 <= n-1 by XREAL_1:9; then n-1 in NAT by INT_1:3; hence n-1 is Nat; thus thesis by A1; end; theorem Th2: :: Nat02 for n being odd Nat holds n-1 is Nat & 1 <= n by Th1; Lm1: for a,b,c being Integer st a+2 < b holds c-b+1 + 2 < c-a+1 proof let a,b,c be Integer such that A1: a+2 < b; assume c-b+1 + 2 >= c-a+1; then c-b+3-3 >= c-a + 1 -3 by XREAL_1:9; then c - b >= c - (a+2); hence contradiction by A1,XREAL_1:10; end; theorem Th3: :: EvenOdd02 for n,m being odd Integer st n < m holds n <= m-2 proof let n,m be odd Integer; assume n < m; then n+1 <= m by INT_1:7; then n+1+(-1) <= m+(-1) by XREAL_1:7; then n < m-1 by XXREAL_0:1; then n+1 <= m-1 by INT_1:7; then n+1+(-1) <= m-1+(-1) by XREAL_1:7; hence thesis; end; theorem Th4: :: EvenOdd03: for n,m being odd Integer st m < n holds m+2 <= n proof let n,m be odd Integer; assume m < n; then m+1 <= n by INT_1:7; then m+1 < n by XXREAL_0:1; then m+1+1 <= n by INT_1:7; hence thesis; end; theorem Th5: :: EvenOdd04: for n being odd Nat st 1 <> n ex m being odd Nat st m+2 = n proof let n being odd Nat; A1: 1 <= n by ABIAN:12; assume 1 <> n; then 2*0+1 < n by A1,XXREAL_0:1; then 1+2 <= n by Th4; then 1+2-2 <= n-2 by XREAL_1:9; then n-2*1 in NAT by INT_1:3; then reconsider m = n-2 as odd Nat; take m; thus thesis; end; theorem Th6: :: Odd100 for n being odd Nat st n<=2 holds n=1 proof let n be odd Nat such that A1: n<=2; n <> 2*1; then n < 1+1 by A1,XXREAL_0:1; then A2: n <= 1 by NAT_1:13; n >= 1 by ABIAN:12; hence thesis by A2,XXREAL_0:1; end; theorem Th7: :: Odd101 for n being odd Nat st n<=4 holds n=1 or n=3 proof let n be odd Nat such that A1: n<=4; n<>2*2; then n<3+1 by A1,XXREAL_0:1; then A2: n<=3 by NAT_1:13; per cases by A2,XXREAL_0:1; suppose n=3; hence thesis; end; suppose n<2+1; then n<=2 by NAT_1:13; hence thesis by Th6; end; end; theorem Th8: :: Odd102 for n being odd Nat st n<=6 holds n=1 or n=3 or n=5 proof let n be odd Nat such that A1: n<=6; n<>2*3; then n<5+1 by A1,XXREAL_0:1; then A2: n<=5 by NAT_1:13; per cases by A2,XXREAL_0:1; suppose n=5; hence thesis; end; suppose n<4+1; then n<=4 by NAT_1:13; hence thesis by Th7; end; end; theorem for n being odd Nat st n<=8 holds n=1 or n=3 or n=5 or n=7 proof let n be odd Nat such that A1: n<=8; n<>2*4; then n<7+1 by A1,XXREAL_0:1; then A2: n<=7 by NAT_1:13; per cases by A2,XXREAL_0:1; suppose n=7; hence thesis; end; suppose n<6+1; then n<=6 by NAT_1:13; hence thesis by Th8; end; end; theorem Th10: :: Even100 for n being even Nat st n<=1 holds n=0 proof let n be even Nat such that A1: n<=1; n<>2*0+1; then n<0+1 by A1,XXREAL_0:1; hence thesis by NAT_1:13; end; theorem Th11: :: Even101 for n being even Nat st n<=3 holds n=0 or n=2 proof let n be even Nat such that A1: n<=3; n<>2*1+1; then n<2+1 by A1,XXREAL_0:1; then A2: n<=2 by NAT_1:13; per cases by A2,XXREAL_0:1; suppose n=2; hence thesis; end; suppose n<1+1; then n<=1 by NAT_1:13; hence thesis by Th10; end; end; theorem Th12: :: Even102 for n being even Nat st n<=5 holds n=0 or n=2 or n=4 proof let n be even Nat such that A1: n<=5; n<>2*2+1; then n<4+1 by A1,XXREAL_0:1; then A2: n<=4 by NAT_1:13; per cases by A2,XXREAL_0:1; suppose n=4; hence thesis; end; suppose n<3+1; then n<=3 by NAT_1:13; hence thesis by Th11; end; end; theorem Th13: :: Even103 for n being even Nat st n<=7 holds n=0 or n=2 or n=4 or n=6 proof let n be even Nat such that A1: n<=7; n<>2*3+1; then n<6+1 by A1,XXREAL_0:1; then A2: n<=6 by NAT_1:13; per cases by A2,XXREAL_0:1; suppose n=6; hence thesis; end; suppose n<5+1; then n<=5 by NAT_1:13; hence thesis by Th12; end; end; Lm2: for i,j being odd Nat st i <= j ex k being Nat st i+2*k = j proof let i,j be odd Nat; assume i <= j; then consider jjj being Nat such that A1: j = i+jjj by NAT_1:10; A2: jjj in NAT by ORDINAL1:def 12; jjj is even by A1; then consider jj being Element of NAT such that A3: 2*jj = jjj by A2,ABIAN:def 2; reconsider jj as Nat; take jj; thus thesis by A1,A3; end; theorem for p being FinSequence, n being non zero Nat st p is one-to-one & n <= len p holds (p.n)..p = n proof let S be FinSequence; let n be non zero Nat such that A1: S is one-to-one and A2: n <= len S; set m = (S.n)..S; 0+1 <= n by NAT_1:14; then A3: n in dom S by A2,FINSEQ_3:25; then A4: S.n in rng S by FUNCT_1:3; then A5: S.m = S.n by FINSEQ_4:19; m in dom S by A4,FINSEQ_4:20; hence thesis by A1,A3,A5,FUNCT_1:def 4; end; theorem Th15: :: Index01 for p being non empty FinSequence, T being non empty Subset of rng p ex x being set st x in T & for y being set st y in T holds x..p <= y..p proof let S be non empty FinSequence; let T be non empty Subset of rng S; deffunc F(set) = $1..S; consider m being Element of T such that A1: for y being Element of T holds F(m) <= F(y) from GRAPH_5:sch 2; take m; thus m in T; let y be set; assume y in T; hence thesis by A1; end; definition let p be FinSequence, n be Nat; func p.followSet(n) -> finite set equals rng (n,len p)-cut p; correctness; end; theorem Th16: :: Follow00 for p being FinSequence, x being set, n being Nat st x in rng p & n in dom p & p is one-to-one holds x in p.followSet(n) iff x..p >= n proof let p be FinSequence, x be set, n be Nat such that A1: x in rng p and A2: n in dom p and A3: p is one-to-one; A4: n <= len p by A2,FINSEQ_3:25; hereby A5: p.(x..p) = x by A1,FINSEQ_4:19; assume x in p.followSet(n); then consider a being Nat such that A6: a in dom (n, len p)-cut p and A7: ((n, len p)-cut p).a = x by FINSEQ_2:10; A8: x..p in dom p by A1,FINSEQ_4:20; n in NAT by ORDINAL1:def 12; then ex k being Element of NAT st k in dom p & p.k = ((n, len p)-cut p).a & k+1 = n+a & n <= k & k <= len p by A6,GRAPH_3:2; hence x..p >= n by A3,A7,A8,A5,FUNCT_1:def 4; end; assume x..p >= n; then consider k being Nat such that A9: x..p = n + k by NAT_1:10; A10: 1 <= n by A2,FINSEQ_3:25; then A11: len ((n, len p)-cut p) + n = len p + 1 by A4,GRAPH_2:def 1; x..p in dom p by A1,FINSEQ_4:20; then k + n <= len p by A9,FINSEQ_3:25; then k + n + (-n) <= len p + (-n) by XREAL_1:7; then A12: k + 1 <= len p - n + 1 by XREAL_1:7; then k < len ((n, len p)-cut p) by A11,NAT_1:13; then A13: ((n, len p)-cut p).(k+1) = p.(x..p) by A9,A10,A4,GRAPH_2:def 1; A14: p.(x..p) = x by A1,FINSEQ_4:19; 0+1 <= k+1 by XREAL_1:7; then k+1 in dom ((n, len p)-cut p) by A11,A12,FINSEQ_3:25; hence thesis by A14,A13,FUNCT_1:3; end; theorem Th17: :: Follow03 for p, q being FinSequence, x being set st p = <*x*>^q for n being non zero Nat holds p.followSet(n+1) = q.followSet(n) proof let p,q be FinSequence, x be set such that A1: p = <*x*>^q; let n be non zero Nat; len <*x*> = 1 by FINSEQ_1:40; then A2: len p = 1 + len q by A1,FINSEQ_1:22; per cases; suppose A3: n > len q; then n+1 > len p by A2,XREAL_1:8; then (n+1,len p)-cut p = {} by GRAPH_2:def 1; hence thesis by A3,GRAPH_2:def 1; end; suppose A4: n <= len q; then A5: n+1 <= len p by A2,XREAL_1:7; A6: 0+1 <= n by NAT_1:13; then A7: 1 <= n+1 by XREAL_1:7; then A8: len ((n+1, len p)-cut p) + (n+1) = len p + 1 by A5,GRAPH_2:def 1; A9: len (n, len q)-cut q + n = len q + 1 by A4,A6,GRAPH_2:def 1; then dom ((n+1,len p)-cut p) = Seg (len ((n, len q)-cut q)) by A2,A8, FINSEQ_1:def 3; then A10: dom ((n+1,len p)-cut p) = dom ((n, len q)-cut q) by FINSEQ_1:def 3; A11: now let i be Nat; assume i in dom q; then p.(len <*x*> + i) = q.i by A1,FINSEQ_1:def 7; hence p.(i+1) = q.i by FINSEQ_1:40; end; A12: now let k be Nat such that A13: k in dom ((n, len q)-cut q); A14: k <= (len p - n) by A8,A10,A13,FINSEQ_3:25; then A15: -1 + k < 0 + (len p - n) by XREAL_1:8; 1 <= k by A13,FINSEQ_3:25; then 1+-1 <= k+-1 by XREAL_1:7; then k-1 in NAT by INT_1:3; then reconsider k1 = k-1 as Nat; n+k <= n+((len p)-n) by A14,XREAL_1:7; then A16: k1+n +1 + -1 <= len q + 1 + -1 by A2,XREAL_1:7; 1+0 <= n+k1 by NAT_1:13; then A17: n+k1 in dom q by A16,FINSEQ_3:25; thus ((n+1,len p)-cut p).k = ((n+1, len p)-cut p).(k1+1) .= p.(n+1+k1) by A7,A5,A8,A15,GRAPH_2:def 1 .= p.(n+k1+1) .= q.(n+k1) by A11,A17 .= ((n,len q)-cut q).(k1+1) by A2,A4,A6,A9,A15,GRAPH_2:def 1 .= ((n,len q)-cut q).k; end; now let y be set; hereby assume y in rng (n+1,len p)-cut p; then consider k being Nat such that A18: k in dom (n+1, len p)-cut p and A19: ((n+1,len p)-cut p).k = y by FINSEQ_2:10; ((n+1,len p)-cut p).k = ((n, len q)-cut q).k by A10,A12,A18; hence y in rng (n, len q)-cut q by A10,A18,A19,FUNCT_1:3; end; assume y in rng ((n, len q)-cut q); then consider k being Nat such that A20: k in dom (n, len q)-cut q and A21: ((n, len q)-cut q).k = y by FINSEQ_2:10; ((n+1,len p)-cut p).k = ((n, len q)-cut q).k by A12,A20; hence y in rng (n+1,len p)-cut p by A10,A20,A21,FUNCT_1:3; end; hence thesis by TARSKI:1; end; end; theorem Th18: :: FinSubseq00 for X being set, f being FinSequence of X, g being Subset of f st len Seq g = len f holds Seq g = f proof let X be set, f be FinSequence of X, g be Subset of f such that A1: len Seq g = len f; A2: len Seq g = card g by GLIB_001:5; now assume g <> f; then g c< f by XBOOLE_0:def 8; hence contradiction by A1,A2,CARD_2:48; end; hence thesis by FINSEQ_3:116; end; begin :: Miscellany on graphs theorem Th19: for G being _Graph, S being Subset of the_Vertices_of G for H being inducedSubgraph of G,S for u,v being set st u in S & v in S for e being set st e Joins u,v,G holds e Joins u,v,H proof let G be _Graph, S be Subset of the_Vertices_of G; let H be inducedSubgraph of G,S; let u,v be set such that A1: u in S and A2: v in S; reconsider S as non empty Subset of the_Vertices_of G by A1; let e be set such that A3: e Joins u,v,G; e in G.edgesBetween(S) by A1,A2,A3,GLIB_000:32; then A4: e in the_Edges_of H by GLIB_000:def 37; the_Target_of H = (the_Target_of G) | the_Edges_of H by GLIB_000:45; then A5: (the_Target_of H).e = (the_Target_of G).e by A4,FUNCT_1:49; A6: (the_Source_of G).e = u & (the_Target_of G).e = v or (the_Source_of G).e = v & (the_Target_of G).e = u by A3,GLIB_000:def 13; the_Source_of H = (the_Source_of G) | the_Edges_of H by GLIB_000:45; then (the_Source_of H).e = (the_Source_of G).e by A4,FUNCT_1:49; hence thesis by A4,A6,A5,GLIB_000:def 13; end; theorem for G being _Graph, W being Walk of G holds W is Trail-like iff len W = 2*(card W.edges())+1 proof let G be _Graph, W be Walk of G; set WE = W.edges(), WES = W.edgeSeq(); W is Trail-like iff W.edgeSeq() is one-to-one by GLIB_001:def 27; then W is Trail-like iff 2*card WE + 1 = 2*len WES+1 by FINSEQ_4:62; hence thesis by GLIB_001:def 15; end; theorem Th21: :: Walk02 for G being _Graph, S being Subset of the_Vertices_of G for H being removeVertices of G,S for W being Walk of G st (for n being odd Nat st n <= len W holds not W.n in S) holds W is Walk of H proof let G be _Graph, S be Subset of the_Vertices_of G; let H be removeVertices of G,S; let W be Walk of G such that A1: for n being odd Nat st n <= len W holds not W.n in S; A2: now assume the_Vertices_of G\S = {}; then A3: the_Vertices_of G c= S by XBOOLE_1:37; W.last() in the_Vertices_of G; hence contradiction by A1,A3; end; then A4: the_Edges_of H = G.edgesBetween(the_Vertices_of G\S) by GLIB_000:def 37; A5: W.edges() c= G.edgesBetween(W.vertices()) by GLIB_001:109; A6: the_Vertices_of H = the_Vertices_of G\S by A2,GLIB_000:def 37; now let x be set such that A7: x in W.vertices(); ex n being odd Element of NAT st n <= len W & W.n = x by A7,GLIB_001:87; then not x in S by A1; hence x in the_Vertices_of H by A6,A7,XBOOLE_0:def 5; end; then A8: W.vertices() c= the_Vertices_of H by TARSKI:def 3; then G.edgesBetween(W.vertices()) c= G.edgesBetween(the_Vertices_of H) by GLIB_000:36; then W.edges() c= G.edgesBetween(the_Vertices_of H) by A5,XBOOLE_1:1; hence thesis by A6,A4,A8,GLIB_001:170; end; theorem Th22: :: Walk03 for G being _Graph, a,b be set st a<>b for W being Walk of G st W.vertices() = {a,b} holds ex e being set st e Joins a,b,G proof let G be _Graph, a,b be set such that A1: a<>b; let W be Walk of G such that A2: W.vertices() = {a,b}; A3: W.first() in W.vertices() by GLIB_001:88; A4: now let x be set such that A5: W.first() = x; A6: x = a or x = b by A2,A3,A5,TARSKI:def 2; A7: x in {x} by TARSKI:def 1; let y be set such that A8: y in {a,b} \ {x}; A9: y = a or y = b by A8,TARSKI:def 2; set k = W.find(y); A10: W.k = y by A2,A8,GLIB_001:def 19; then k <> 1 by A5,A8,A7,XBOOLE_0:def 5; then consider m being odd Nat such that A11: m+2 = k by Th5; A12: m < k by A11,NAT_1:16; k <= len W by A2,A8,GLIB_001:def 19; then A13: m < len W by A11,NAT_1:16,XXREAL_0:2; A14: m in NAT by ORDINAL1:def 12; then W.m in {a,b} by A2,A13,GLIB_001:87; then A15: W.m = a or W.m = b by TARSKI:def 2; W.(m+1) Joins W.m,W.k,G by A11,A13,A14,GLIB_001:def 3; hence ex e being set st e Joins x,y,G by A2,A8,A7,A6,A10,A12,A13,A15,A9, GLIB_001:def 19,XBOOLE_0:def 5; end; per cases by A2,A3,TARSKI:def 2; suppose A16: W.first() = a; b in {b} by TARSKI:def 1; then b in {a,b}\{a} by A1,ZFMISC_1:17; hence thesis by A4,A16; end; suppose A17: W.first() = b; a in {a} by TARSKI:def 1; then a in {a,b}\{b} by A1,ZFMISC_1:17; then ex e be set st e Joins b,a,G by A4,A17; hence thesis by GLIB_000:14; end; end; theorem Th23: :: Walk04 for G being _Graph, S being non empty Subset of the_Vertices_of G for H being inducedSubgraph of G,S for W being Walk of G st W.vertices() c= S holds W is Walk of H proof let G be _Graph, S be non empty Subset of the_Vertices_of G; let H be inducedSubgraph of G,S; A1: the_Vertices_of H = S by GLIB_000:def 37; A2: the_Edges_of H = G.edgesBetween(S) by GLIB_000:def 37; let W be Walk of G; assume W.vertices() c= S; then A3: W.vertices() c= the_Vertices_of H by GLIB_000:def 37; A4: W.edges() c= G.edgesBetween(W.vertices()) by GLIB_001:109; G.edgesBetween(W.vertices()) c= G.edgesBetween(the_Vertices_of H) by A3, GLIB_000:36; then W.edges() c= the_Edges_of H by A1,A2,A4,XBOOLE_1:1; hence thesis by A3,GLIB_001:170; end; theorem Th24: :: Cyclelike01 for G1,G2 being _Graph st G1 == G2 for W1 be Walk of G1, W2 being Walk of G2 st W1 = W2 holds W1 is Cycle-like implies W2 is Cycle-like proof let G1,G2 be _Graph such that A1: G1 == G2; let W1 be Walk of G1,W2 be Walk of G2 such that A2: W1 = W2; assume A3: W1 is Cycle-like; then len W2 <> 1 by A2,GLIB_001:126; then A4: W2 is non trivial by GLIB_001:126; W1.first() = W1.last() by A3,GLIB_001:def 24; then W2.first() = W2.last() by A2; then A5: W2 is closed by GLIB_001:def 24; W2 is Path-like by A1,A2,A3,GLIB_001:181; hence thesis by A4,A5,GLIB_001:def 31; end; theorem Th25: :: Path01 for G being _Graph, P being Path of G, m, n being odd Nat st m <= len P & n <= len P & P.m = P.n holds m = n or m = 1 & n = len P or m = len P & n = 1 proof let G be _Graph, P be Path of G, m, n be odd Nat such that A1: m <= len P and A2: n <= len P and A3: P.m = P.n; A4: m in NAT by ORDINAL1:def 12; A5: n in NAT by ORDINAL1:def 12; m=n or m 3; then not n in Seg 3 by FINSEQ_1:1; then not n in Seg (len T) by A4,GLIB_001:14; then A16: not n in dom T by FINSEQ_1:def 3; 1 <= n by A15,XXREAL_0:2; then n in dom J by A10,FINSEQ_3:25; then consider j being Element of NAT such that A17: j < len P and A18: n = len T + j by A16,GLIB_001:34; reconsider jj=j as even Nat by A18; reconsider j1=jj+1 as odd Nat; j+1 <= len P by A17,NAT_1:13; then P.j1 in P.vertices() by GLIB_001:87; hence contradiction by A5,A11,A14,A17,A18,GLIB_001:33; end; end; then 2*0+1 < m by A12,XXREAL_0:1; then A19: 1+2 <= m by Th4; then 3 <= n by A9,XXREAL_0:2; then 1 <= n by XXREAL_0:2; then n in Seg (len J) by A10,FINSEQ_1:1; then A20: n in dom J by FINSEQ_1:def 3; 3 < n by A9,A19,XXREAL_0:2; then not n in Seg 3 by FINSEQ_1:1; then not n in Seg (len T) by A4,GLIB_001:14; then not n in dom T by FINSEQ_1:def 3; then consider j being Element of NAT such that A21: j < len P and A22: n = len T + j by A20,GLIB_001:34; reconsider jj=j as even Nat by A22; reconsider j1=jj+1 as odd Nat; A23: j1 <= len P by A21,NAT_1:13; m < len J by A9,A10,XXREAL_0:2; then A24: m in dom J by A12,FINSEQ_3:25; A25: J.n = P.(j+1) by A5,A21,A22,GLIB_001:33; now assume m = 3; then A26: J.m = P.1 by A3,A4,A6,GLIB_001:15; 0 <> j by A4,A9,A19,A22,GLIB_001:14; then 2*0+1 < j1 by XREAL_1:8; hence contradiction by A1,A11,A25,A23,A26,GLIB_001:147; end; then 3 < m by A19,XXREAL_0:1; then not m in Seg 3 by FINSEQ_1:1; then not m in Seg (len T) by A4,GLIB_001:14; then not m in dom T by FINSEQ_1:def 3; then consider k being Element of NAT such that A27: k < len P and A28: m = len T + k by A24,GLIB_001:34; reconsider kk=k as even Nat by A28; reconsider k1=kk+1 as odd Nat; k < j by A9,A22,A28,XREAL_1:7; then A29: k1 < j1 by XREAL_1:8; J.m = P.(k+1) by A5,A27,A28,GLIB_001:33; hence contradiction by A1,A11,A25,A23,A29,GLIB_001:147; end; now let m,n be odd Element of NAT such that A30: m <= len J and A31: n <= len J; assume A32: J.m = J.n; then A33: not n < m by A8,A30; m >= n by A8,A31,A32; hence n = m by A33,XXREAL_0:1; end; hence thesis by GLIB_001:146; end; theorem Th27: :: PathLike03 :: A similar theorem is needed for obtaining non closed Path for G being _Graph, P,H being Path of G st P.edges() misses H .edges() & P is open & H is non trivial & H is open & P.vertices() /\ H .vertices() = { P.first(), P.last() } & H.first() = P.last() & H.last() = P .first() holds P.append(H) is Cycle-like proof let G be _Graph, P,H be Path of G such that A1: P.edges() misses H.edges() and A2: P is open and A3: H is non trivial and A4: H is open and A5: P.vertices() /\ H.vertices() = { P.first(), P.last() } and A6: H.first() = P.last() and A7: H.last() = P.first(); set J = P.append(H); A8: J.first() = P.first() by A6,GLIB_001:30; A9: now let m be odd Nat; A10: 1 <= m by ABIAN:12; assume m <= len P; then m in dom P by A10,FINSEQ_3:25; hence J.m = P.m by GLIB_001:32; end; A11: for m being odd Nat st m > len P & m <= len J holds m in dom J & not m in dom P proof let m be odd Nat such that A12: m > len P and A13: m <= len J; 1 <= m by ABIAN:12; hence thesis by A12,A13,FINSEQ_3:25; end; A14: len J + 1 + (-1) = len P + len H + (-1) by A6,GLIB_001:28; A15: now let m,n being odd Element of NAT such that A16: m < n and A17: n <= len J; A18: m <= len J by A16,A17,XXREAL_0:2; A19: 1 <= m by ABIAN:12; per cases; suppose A20: m <= len P & n <= len P; then A21: P.m = J.m by A9; P.m <> P.n by A2,A16,A20,GLIB_001:147; hence J.m = J.n implies m = 1 & n = len J by A9,A20,A21; end; suppose A22: m <= len P & n > len P; then A23: J.m = P.m by A9; A24: not n in dom P by A11,A17,A22; n in dom J by A11,A17,A22; then consider j being Element of NAT such that A25: j < len H and A26: n = len P + j by A24,GLIB_001:34; reconsider jj=j as even Nat by A26; reconsider j1=jj+1 as odd Nat; A27: j1 <= len H by A25,NAT_1:13; A28: J.n = H.(j+1) by A6,A25,A26,GLIB_001:33; now assume A29: J.m = J.n; A30: now j <> 0 by A22,A26; then 0+1 < j1 by XREAL_1:8; then A31: H.(2*0+1) <> H.j1 by A4,A27,GLIB_001:147; assume J.m = P.last(); hence contradiction by A6,A25,A26,A29,A31,GLIB_001:33; end; A32: J.m in P.vertices() by A22,A23,GLIB_001:87; J.m in H.vertices() by A28,A27,A29,GLIB_001:87; then A33: J.m in P.vertices() /\ H.vertices() by A32,XBOOLE_0:def 4; then A34: J.n = H.last() by A5,A7,A29,A30,TARSKI:def 2; A35: now assume n < len J; then j1 <> len H by A14,A26; then A36: j1 < len H by A27,XXREAL_0:1; H.j1 = H.(len H) by A6,A25,A26,A34,GLIB_001:33; hence contradiction by A4,A36,GLIB_001:147; end; A37: J.m = P.first() by A5,A33,A30,TARSKI:def 2; now assume 1 < m; then P.m <> P.(2*0+1) by A2,A22,GLIB_001:147; hence contradiction by A9,A22,A37; end; hence m = 1 & n = len J by A17,A19,A35,XXREAL_0:1; end; hence J.m = J.n implies m = 1 & n = len J; end; suppose m > len P & n <= len P; hence J.m = J.n implies m = 1 & n = len J by A16,XXREAL_0:2; end; suppose A38: m > len P & n > len P; then A39: not n in dom P by A11,A17; n in dom J by A11,A17,A38; then consider j being Element of NAT such that A40: j < len H and A41: n = len P + j by A39,GLIB_001:34; reconsider jj=j as even Nat by A41; reconsider j1=jj+1 as odd Element of NAT; A42: j1 <= len H by A40,NAT_1:13; A43: not m in dom P by A11,A18,A38; m in dom J by A11,A18,A38; then consider k being Element of NAT such that A44: k < len H and A45: m = len P + k by A43,GLIB_001:34; reconsider kk = k as even Nat by A45; reconsider k1=kk+1 as odd Nat; k < j by A16,A45,A41,XREAL_1:7; then A46: k1 < j1 by XREAL_1:8; A47: J.(len P + j) = H.(j+1) by A6,A40,GLIB_001:33; J.(len P + k) = H.(k+1) by A6,A44,GLIB_001:33; hence J.m = J.n implies m = 1 & n = len J by A4,A45,A41,A47,A46,A42, GLIB_001:147; end; end; A48: H.edgeSeq() is one-to-one by GLIB_001:def 27; now assume len J = 1; then A49: 1 + 1 = len P + len H by A6,GLIB_001:28; now assume A50: len P <> 1; 1 <= len P by Th2; then 1 < len P by A50,XXREAL_0:1; then len P + len H <= len P by A49,NAT_1:13; then len P + len H + (-len P) <= len P + (-len P) by XREAL_1:7; then len H <= 0; hence contradiction; end; hence contradiction by A3,A49,GLIB_001:126; end; then A51: J is non trivial by GLIB_001:126; J.last() = P.first() by A6,A7,GLIB_001:30; then A52: J is closed by A8,GLIB_001:def 24; P.edgeSeq() is one-to-one by GLIB_001:def 27; then P.edgeSeq() ^ H.edgeSeq() is one-to-one by A1,A48,FINSEQ_3:91; then J.edgeSeq() is one-to-one by A6,GLIB_001:85; then J is Trail-like by GLIB_001:def 27; then J is Path-like by A15,GLIB_001:def 28; hence thesis by A52,A51,GLIB_001:def 31; end; theorem Th28: for G being _Graph, W1,W2 being Walk of G st W1.last() = W2 .first() holds W1.append(W2).length() = W1.length() + W2.length() proof let G being _Graph, P,H being Walk of G; assume H.first() = P.last(); hence P.append(H).length() = len (P.edgeSeq() ^ H.edgeSeq()) by GLIB_001:85 .= P.length() + H.length() by FINSEQ_1:22; end; theorem Th29: :: Subgraph01 for G being _Graph, A,B being non empty Subset of the_Vertices_of G st B c= A for H1 being inducedSubgraph of G,A for H2 being inducedSubgraph of H1,B holds H2 is inducedSubgraph of G,B proof let G be _Graph; let A,B be non empty Subset of the_Vertices_of G such that A1: B c= A; let H1 be inducedSubgraph of G,A; let H2 be inducedSubgraph of H1,B; A2: the_Vertices_of H1 = A by GLIB_000:def 37; then A3: the_Vertices_of H2 = B by A1,GLIB_000:def 37; A4: now let e be set such that A5: e in G.edgesBetween(B); A6: (the_Target_of G).e in B by A5,GLIB_000:31; A7: (the_Source_of G).e in B by A5,GLIB_000:31; then e in G.edgesBetween(A) by A1,A5,A6,GLIB_000:31; then A8: e in the_Edges_of H1 by GLIB_000:def 37; then A9: (the_Target_of H1).e = (the_Target_of G).e by GLIB_000:def 32; (the_Source_of H1).e = (the_Source_of G).e by A8,GLIB_000:def 32; then e in H1.edgesBetween(B) by A7,A6,A8,A9,GLIB_000:31; hence e in the_Edges_of H2 by A1,A2,GLIB_000:def 37; end; H1.edgesBetween(B) c= G.edgesBetween(B) by GLIB_000:76; then the_Edges_of H2 c= G.edgesBetween(B) by A1,A2,GLIB_000:def 37; then for x being set holds x in the_Edges_of H2 iff x in G.edgesBetween(B) by A4; then A10: the_Edges_of H2 = G.edgesBetween(B) by TARSKI:1; A11: now let e be set such that A12: e in the_Edges_of H2; A13: (the_Target_of H2).e = (the_Target_of H1).e by A12,GLIB_000:def 32; (the_Source_of H2).e = (the_Source_of H1).e by A12,GLIB_000:def 32; hence (the_Source_of H2).e = (the_Source_of G).e & (the_Target_of H2).e = ( the_Target_of G).e by A12,A13,GLIB_000:def 32; end; the_Edges_of H2 c= the_Edges_of H1; then the_Edges_of H2 c= the_Edges_of G by XBOOLE_1:1; then H2 is Subgraph of G by A3,A11,GLIB_000:def 32; hence thesis by A3,A10,GLIB_000:def 37; end; theorem Th30: :: Subgraph01a for G being _Graph, A,B being non empty Subset of the_Vertices_of G st B c= A for H1 being inducedSubgraph of G,A for H2 being inducedSubgraph of G,B holds H2 is inducedSubgraph of H1,B proof let G be _Graph; let A,B be non empty Subset of the_Vertices_of G such that A1: B c= A; let H1 be inducedSubgraph of G,A; let H2 be inducedSubgraph of G,B; A2: the_Edges_of H2 = G.edgesBetween(B) by GLIB_000:def 37; the_Edges_of H1 = G.edgesBetween(A) by GLIB_000:def 37; then A3: the_Edges_of H2 c= the_Edges_of H1 by A1,A2,GLIB_000:36; A4: now let e be set such that A5: e in the_Edges_of H2; A6: (the_Target_of G).e = (the_Target_of H1).e by A3,A5,GLIB_000:def 32; A7: (the_Target_of G).e in B by A2,A5,GLIB_000:31; A8: (the_Source_of G).e in B by A2,A5,GLIB_000:31; (the_Source_of G).e = (the_Source_of H1).e by A3,A5,GLIB_000:def 32; hence e in H1.edgesBetween(B) by A3,A5,A6,A8,A7,GLIB_000:31; end; H1.edgesBetween(B) c= the_Edges_of H2 by A2,GLIB_000:76; then for x being set holds x in the_Edges_of H2 iff x in H1.edgesBetween(B ) by A4; then A9: the_Edges_of H2 = H1.edgesBetween(B) by TARSKI:1; A10: the_Vertices_of H1 = A by GLIB_000:def 37; A11: the_Vertices_of H2 = B by GLIB_000:def 37; now let e be set such that A12: e in the_Edges_of H2; thus (the_Source_of H2).e = (the_Source_of G).e by A12,GLIB_000:def 32 .= (the_Source_of H1).e by A3,A12,GLIB_000:def 32; thus (the_Target_of H2).e = (the_Target_of G).e by A12,GLIB_000:def 32 .= (the_Target_of H1).e by A3,A12,GLIB_000:def 32; end; then H2 is Subgraph of H1 by A1,A10,A11,A3,GLIB_000:def 32; hence thesis by A1,A10,A11,A9,GLIB_000:def 37; end; theorem Th31: :: Subgraph02 for G being _Graph, S,T being non empty Subset of the_Vertices_of G st T c= S for G2 being inducedSubgraph of G,S holds G2 .edgesBetween(T) = G.edgesBetween(T) proof let G be _Graph; let S,T be non empty Subset of the_Vertices_of G such that A1: T c= S; let G2 be inducedSubgraph of G,S; A2: the_Edges_of G2 = G.edgesBetween(S) by GLIB_000:def 37; now let e be set; hereby assume A3: e in G.edgesBetween(T); then A4: (the_Source_of G).e in T by GLIB_000:31; A5: (the_Target_of G).e in T by A3,GLIB_000:31; A6: G.edgesBetween(T) c= G.edgesBetween(S) by A1,GLIB_000:36; then A7: (the_Target_of G2).e = (the_Target_of G).e by A2,A3,GLIB_000:def 32; (the_Source_of G2).e = (the_Source_of G).e by A2,A3,A6,GLIB_000:def 32; hence e in G2.edgesBetween(T) by A2,A3,A6,A4,A5,A7,GLIB_000:31; end; assume A8: e in G2.edgesBetween(T); then (the_Source_of G2).e in T by GLIB_000:31; then A9: (the_Source_of G).e in T by A8,GLIB_000:def 32; (the_Target_of G2).e in T by A8,GLIB_000:31; then A10: (the_Target_of G).e in T by A8,GLIB_000:def 32; e in the_Edges_of G2 by A8; hence e in G.edgesBetween(T) by A9,A10,GLIB_000:31; end; hence thesis by TARSKI:1; end; :: we do not consider infinite graphs scheme FinGraphOrderCompInd{P[set]}: for G being finite _Graph holds P[G] provided A1: for k being non zero Nat st (for Gk being finite _Graph st Gk.order() < k holds P[Gk]) holds for Gk1 being finite _Graph st Gk1.order() = k holds P[Gk1] proof let G be finite _Graph; defpred pP[non zero Nat] means for Gk being finite _Graph st Gk.order() < $1 holds P[Gk]; A2: for n being non zero Nat holds pP[n] implies pP[n+1] proof let n be non zero Nat such that A3: pP[n]; now let Gk be finite _Graph; assume Gk.order() < n+1; then Gk.order() <= n by NAT_1:13; then Gk.order() < n or Gk.order() = n by XXREAL_0:1; hence P[Gk] by A1,A3; end; hence thesis; end; A4: pP[1] by NAT_1:14; for k being non zero Nat holds pP[k] from NAT_1:sch 10(A4,A2); then for Gk being finite _Graph st Gk.order() n; per cases by A6,XXREAL_0:1; suppose A7: m < n; then A8: W.n = W.last() by A2,A4,A5,GLIB_001:def 28; W.m = W.first() by A2,A4,A5,A7,GLIB_001:def 28; hence contradiction by A1,A5,A8,GLIB_001:def 24; end; suppose A9: m > n; then A10: W.n = W.first() by A2,A3,A5,GLIB_001:def 28; W.m = W.last() by A2,A3,A5,A9,GLIB_001:def 28; hence contradiction by A1,A5,A10,GLIB_001:def 24; end; end; hence thesis by GLIB_001:def 29; end; :: PathLike15 :: should be in GLIB theorem Th33: for G being _Graph, P being Path of G st P is open & len P > 3 for e being set st e Joins P.last(),P.first(),G holds P.addEdge(e) is Cycle-like proof let G be _Graph, W be Path of G such that A1: W is open and A2: len W > 3; let e be set such that A3: e Joins W.last(),W.first(),G; A4: now assume e in W.edges(); then consider v1,v2 being Vertex of G, n being odd Element of NAT such that A5: n+2 <= len W and A6: v1 = W.n and e = W.(n+1) and A7: v2 = W.(n+2) and A8: e Joins v1,v2,G by GLIB_001:103; A9: n < len W by A5,XREAL_1:39; per cases by A3,A8,GLIB_000:15; suppose A10: v1 = W.first() & v2 = W.last(); now assume A11: 1 <> n; 1 <= n by Th2; then 2*0+1 < n by A11,XXREAL_0:1; hence contradiction by A1,A6,A9,A10,GLIB_001:147; end; hence contradiction by A1,A2,A7,A10,GLIB_001:147; end; suppose v1 = W.last() & v2 = W.first(); hence contradiction by A1,A6,A9,GLIB_001:147; end; end; set P = W.addEdge(e); A12: P.last() = W.first() by A3,GLIB_001:63; A13: len P = len W + 2*1 by A3,GLIB_001:64; A14: now let m,n be odd Element of NAT such that A15: m < n and A16: n <= len P; m < len W + 2*1 by A13,A15,A16,XXREAL_0:2; then A17: m <= len W + 2 - 2 by Th3; assume A18: P.m = P.n; 1 <= m by Th2; then A19: m in dom W by A17,FINSEQ_3:25; then A20: W.m = P.m by A3,GLIB_001:65; A21: now assume n < len P; then n < len W + 2*1 by A3,GLIB_001:64; then A22: n <= len W + 2 - 2 by Th3; 1 <= n by Th2; then A23: n in dom W by A22,FINSEQ_3:25; W.n <> W.m by A1,A15,A22,GLIB_001:147; hence contradiction by A3,A18,A20,A23,GLIB_001:65; end; then A24: P.n = W.1 by A12,A16,XXREAL_0:1; now assume A25: m <> 1; 1 <= m by Th2; then 2*0+1 < m by A25,XXREAL_0:1; then W.1 <> W.m by A1,A17,GLIB_001:147; hence contradiction by A3,A18,A19,A24,GLIB_001:65; end; hence m = 1 & n = len P by A16,A21,XXREAL_0:1; end; e in W.last().edgesInOut() by A3,GLIB_000:62; then P is Trail-like by A4,GLIB_001:142; then A26: P is Path-like by A14,GLIB_001:def 28; P.first() = W.first() by A3,GLIB_001:63; then A27: P is closed by A12,GLIB_001:def 24; P is non trivial by A3,GLIB_001:132; hence thesis by A27,A26,GLIB_001:def 31; end; begin :: Shortest topological path definition let G be _Graph, W be Walk of G; attr W is minlength means :Def2: for W2 being Walk of G st W2 is_Walk_from W .first(),W.last() holds len W2 >= len W; end; theorem Th34: :: WalkSubwalk00 for G being _Graph, W being Walk of G, S being Subwalk of W st S .first() = W.first() & S.edgeSeq() = W.edgeSeq() holds S = W proof let G be _Graph, W be Walk of G, S be Subwalk of W such that A1: S.first() = W.first() and A2: S.edgeSeq() = W.edgeSeq(); defpred P[Nat] means $1 in dom S implies S.$1 = W.$1; len S = 2*len W.edgeSeq() + 1 by A2,GLIB_001:def 15; then A3: len S = len W by GLIB_001:def 15; A4: now let k be Nat such that A5: for n being Nat st n < k holds P[n]; A6: k in NAT by ORDINAL1:def 12; per cases; suppose A7: k in dom S; then A8: 1 <= k by FINSEQ_3:25; A9: k <= len S by A7,FINSEQ_3:25; per cases; suppose A10: k is even; then S.k = S.edgeSeq().(k div 2) by A6,A8,A9,GLIB_001:77; hence P[k] by A2,A3,A8,A9,A10,GLIB_001:77; end; suppose k is odd; then reconsider kk=k as odd Nat; per cases by A8,XXREAL_0:1; suppose k = 1; hence P[k] by A1; end; suppose k > 2*0+1; then A11: 1+2 <= kk by Th4; then A12: 3+-2 <= k+-2 by XREAL_1:7; A13: 0<=2; 3+-1 <= k+-1 by A11,XREAL_1:7; then reconsider k1=k-1 as Element of NAT by A13,INT_1:3; k1 < k by XREAL_1:44; then A14: k1 <= len S by A9,XXREAL_0:2; 3+-1 <= k+-1 by A11,XREAL_1:7; then 1 <= k1 by XXREAL_0:2; then k1 in dom S by A14,FINSEQ_3:25; then A15: S.k1 = W.k1 by A5,XREAL_1:44; 3+-2 <= k+-2 by A11,XREAL_1:7; then reconsider k2=kk-2*1 as odd Element of NAT by INT_1:3; A16: k2 < k by XREAL_1:44; then k2 < len S by A9,XXREAL_0:2; then A17: S.(k2+1) Joins S.k2,S.(k2+2),G by GLIB_001:def 3; k2 <= len S by A9,A16,XXREAL_0:2; then k2 in dom S by A12,FINSEQ_3:25; then A18: S.k2 = W.k2 by A5,XREAL_1:44; k2 < len W by A3,A9,A16,XXREAL_0:2; then W.(k2+1) Joins W.k2,W.(k2+2),G by GLIB_001:def 3; then S.k2 = S.k2 & S.k = W.k or S.k2 = W.k & S.k = S.k2 by A15,A18 ,A17,GLIB_000:15; hence P[k]; end; end; end; suppose not k in dom S; hence P[k]; end; end; A19: for n being Nat holds P[n] from NAT_1:sch 4(A4); now let k be Nat such that A20: 1 <= k and A21: k <= len S; k in dom S by A20,A21,FINSEQ_3:25; hence S.k = W.k by A19; end; hence thesis by A3,FINSEQ_1:14; end; theorem Th35: :: LenSubwalk00 for G being _Graph, W being Walk of G, S being Subwalk of W st len S = len W holds S = W proof let G be _Graph, W be Walk of G, S be Subwalk of W such that A1: len S = len W; A2: len S = 2*len S.edgeSeq() +1 by GLIB_001:def 15; A3: S.first() = W.first() by GLIB_001:161; A4: len W = 2*len W.edgeSeq() +1 by GLIB_001:def 15; ex es being Subset of W.edgeSeq() st S.edgeSeq() = Seq es by GLIB_001:def 32; hence thesis by A1,A2,A4,A3,Th18,Th34; end; theorem for G being _Graph, W being Walk of G st W is minlength holds W is Path-like proof let G be _Graph, W be Walk of G such that A1: W is minlength and A2: not W is Path-like; set s = the Path-like Subwalk of W; s is_Walk_from W.first(),W.last() by GLIB_001:def 32; then A3: len W <= len s by A1,Def2; len s <= len W by GLIB_001:162; hence contradiction by A2,A3,Th35,XXREAL_0:1; end; theorem for G being _Graph, W being Walk of G st W is minlength holds W is Path-like proof let G be _Graph, W be Walk of G such that A1: W is minlength; assume not W is Path-like; then consider m,n be odd Element of NAT such that A2: m <= len W and A3: n <= len W and A4: W.m = W.n and A5: m <> n by GLIB_001:146; per cases by A5,XXREAL_0:1; suppose A6: m < n; set R = W.cut(1,m), S = W.cut(n,len W); set P = R.append(S); A7: len S + n - n = len W + 1 - n by A3,GLIB_001:36; A8: 2*0+1 <= m by ABIAN:12; then A9: len R + 1 - 1 = m + 1 - 1 by A2,GLIB_001:36; A10: S.first() = W.m by A3,A4,GLIB_001:37; A11: R.last() = W.m by A2,A8,GLIB_001:37; then len P + 1 = len R + len S by A10,GLIB_001:28; then len P = len W - n + m by A9,A7; then A12: len P < len W - n + n by A6,XREAL_1:8; A13: S.last() = W.(len W) by A3,GLIB_001:37; R.first() = W.(2*0+1) by A2,A8,GLIB_001:37; then P is_Walk_from W.first(),W.last() by A11,A10,A13,GLIB_001:30; hence contradiction by A1,A12,Def2; end; suppose A14: n < m; set R = W.cut(1,n), S = W.cut(m,len W); set P = R.append(S); A15: len S + m - m = len W + 1 - m by A2,GLIB_001:36; A16: 2*0+1 <= n by ABIAN:12; then A17: len R + 1 - 1 = n + 1 - 1 by A3,GLIB_001:36; A18: S.first() = W.n by A2,A4,GLIB_001:37; A19: R.last() = W.n by A3,A16,GLIB_001:37; then len P + 1 = len R + len S by A18,GLIB_001:28; then len P = len W - m + n by A17,A15; then A20: len P < len W - m + m by A14,XREAL_1:8; A21: S.last() = W.(len W) by A2,GLIB_001:37; R.first() = W.(2*0+1) by A3,A16,GLIB_001:37; then P is_Walk_from W.first(),W.last() by A19,A18,A21,GLIB_001:30; hence contradiction by A1,A20,Def2; end; end; theorem Th38: for G being _Graph, W being Walk of G holds (for P being Path of G st P is_Walk_from W.first(),W.last() holds len P >= len W) implies W is minlength proof let G be _Graph, W be Walk of G; assume A1: for P2 being Path of G st P2 is_Walk_from W.first(),W.last() holds len P2 >= len W; now let V be Walk of G such that A2: V is_Walk_from W.first(),W.last(); set P3 = the Path-like Subwalk of V; V.last() = W.last() by A2,GLIB_001:def 23; then A3: P3.last()=W.last() by GLIB_001:161; V.first() = W.first() by A2,GLIB_001:def 23; then P3.first()=W.first() by GLIB_001:161; then P3 is_Walk_from W.first(),W.last() by A3,GLIB_001:def 23; then A4: len W <= len P3 by A1; len P3 <= len V by GLIB_001:162; hence len V >= len W by A4,XXREAL_0:2; end; hence thesis by Def2; end; theorem Th39: :: TopPath02 for G being _Graph, W being Walk of G ex P being Path of G st P is_Walk_from W.first(),W.last() & P is minlength proof let G being _Graph, W being Walk of G; set X = { len P where P is Path of G : P is_Walk_from W.first(),W.last() }; set T = the Path-like Subwalk of W; A1: T.last() = W.last() by GLIB_001:161; T.first() = W.first() by GLIB_001:161; then T is_Walk_from W.first(),W.last() by A1,GLIB_001:def 23; then A2: len T in X; X c= NAT proof let x be set; assume x in X; then ex P being Path of G st x = len P & P is_Walk_from W.first(),W .last(); hence thesis; end; then reconsider X as non empty Subset of NAT by A2; min X in X by XXREAL_2:def 7; then consider P being Path of G such that A3: len P = min X and A4: P is_Walk_from W.first(),W.last(); A5: P.first() = W.first() by A4,GLIB_001:def 23; take P; thus P is_Walk_from W.first(),W.last() by A4; let W2 be Walk of G such that A6: W2 is_Walk_from P.first(),P.last(); A7: P.last() = W2.last() by A6,GLIB_001:def 23; set T = the Path-like Subwalk of W2; A8: T.first() = W2.first() by GLIB_001:161; A9: T.last() = W2.last() by GLIB_001:161; A10: P.last() = W.last() by A4,GLIB_001:def 23; P.first() = W2.first() by A6,GLIB_001:def 23; then T is_Walk_from W.first(),W.last() by A7,A5,A10,A8,A9,GLIB_001:def 23; then len T in X; then A11: len P <= len T by A3,XXREAL_2:def 7; len T <= len W2 by GLIB_001:162; hence thesis by A11,XXREAL_0:2; end; theorem Th40: :: TopPath03 for G being _Graph, W being Walk of G st W is minlength holds for m,n being odd Nat st m+2 < n & n <= len W holds not ex e being set st e Joins W.m,W.n,G proof let G be _Graph; let P be Walk of G such that A1: P is minlength; let m,n be odd Nat such that A2: m+2 < n and A3: n <= len P; A4: len P - n + (m + 2) < len P - n + n by A2,XREAL_1:8; m+0 <= m+2 by XREAL_1:7; then m <= n by A2,XXREAL_0:2; then A5: m <= len P by A3,XXREAL_0:2; set P3 = P.cut(n,len P); A6: n in NAT by ORDINAL1:def 12; then A7: P3.last() = P.last() by A3,GLIB_001:37; set P1 = P.cut(1,m); let e be set such that A8: e Joins P.m,P.n,G; set P2 = P1.addEdge(e); set P4 = P2.append(P3); A9: 2*0+1 <= m by ABIAN:12; A10: m in NAT by ORDINAL1:def 12; then A11: len P1 + 1 = m + 1 by A9,A5,GLIB_001:36; A12: P1.last() = P.m by A10,A9,A5,GLIB_001:37; then A13: P2.last() = P.n by A8,GLIB_001:63; P1.first() = P.first() by A10,A9,A5,GLIB_001:37; then A14: P2.first() = P.first() by A8,A12,GLIB_001:63; P3.first() = P.n by A3,A6,GLIB_001:37; then A15: P4 is_Walk_from P.first(),P.last() by A14,A13,A7,GLIB_001:30; P3.first() = P.n by A3,A6,GLIB_001:37; then A16: len P4 + 1 = len P2 + len P3 by A13,GLIB_001:28; P1.last() = P.m by A10,A9,A5,GLIB_001:37; then A17: len P2 = m + 2 by A8,A11,GLIB_001:64; len P3 + n = len P+1 by A3,A6,GLIB_001:36; hence contradiction by A1,A17,A15,A16,A4,Def2; end; theorem Th41: :: TopPath04 for G being _Graph, S being non empty Subset of the_Vertices_of G for H being inducedSubgraph of G,S for W being Walk of H st W is minlength for m,n being odd Nat st m+2 < n & n <= len W holds not ex e being set st e Joins W.m,W.n,G proof let G be _Graph, S be non empty Subset of the_Vertices_of G; let GA be inducedSubgraph of G,S; let P be Walk of GA; A1: S = the_Vertices_of GA by GLIB_000:def 37; assume A2: P is minlength; now let m,n be odd Nat such that A3: m+2 < n and A4: n <= len P; m + 0 <= m + 2 by XREAL_1:7; then A5: m <= n by A3,XXREAL_0:2; n in NAT by ORDINAL1:def 12; then A6: P.n in the_Vertices_of GA by A4,GLIB_001:7; m in NAT by ORDINAL1:def 12; then A7: P.m in the_Vertices_of GA by A4,A5,GLIB_001:7,XXREAL_0:2; let e be set; assume e Joins P.m,P.n,G; hence contradiction by A2,A1,A3,A4,A7,A6,Th19,Th40; end; hence thesis; end; theorem Th42: :: TopPath05 for G being _Graph for W being Walk of G st W is minlength for m,n being odd Nat st m<=n & n<=len W holds W.cut(m,n) is minlength proof let G be _Graph, W be Walk of G such that A1: W is minlength; let m,n be odd Nat such that A2: m <= n and A3: n <= len W; set S = W.cut(m,n); assume not S is minlength; then consider M being Walk of G such that A4: M is_Walk_from S.first(),S.last() and A5: len M < len S by Def2; set R = W.cut(1,m); A6: 2*0+1 <= m by ABIAN:12; set T = W.cut(n,len W); A7: n in NAT by ORDINAL1:def 12; then A8: T.first() = W.n by A3,GLIB_001:37; set A = R.append(M); A9: m in NAT by ORDINAL1:def 12; A10: m <= len W by A2,A3,XXREAL_0:2; then A11: R.last() = W.m by A6,A9,GLIB_001:37; S.first() = W.m by A2,A3,A9,A7,GLIB_001:37; then A12: M.first() = W.m by A4,GLIB_001:def 23; then len A + 1 = len R + len M by A11,GLIB_001:28; then A13: len A + 1 < len R + len S by A5,XREAL_1:8; set B = A.append(T); S.last() = W.n by A2,A3,A9,A7,GLIB_001:37; then M.last() = W.n by A4,GLIB_001:def 23; then A14: A.last() = W.n by A11,A12,GLIB_001:30; then A15: len B + 1 = len A + len T by A8,GLIB_001:28; A16: len R + 1 = m + 1 by A6,A10,A9,GLIB_001:36; len S + m = n + 1 by A2,A3,A9,A7,GLIB_001:36; then len A + 1 - 1 < n + 1 - 1 by A16,A13,XREAL_1:14; then A17: len B + 1 < len T + n by A15,XREAL_1:8; len T + n = len W + 1 by A3,A7,GLIB_001:36; then A18: len B + 1 - 1 < len W + 1 - 1 by A17,XREAL_1:14; T.last() = W.(len W) by A3,A7,GLIB_001:37; then A19: B.last() = W.last() by A8,A14,GLIB_001:30; R.first() = W.1 by A6,A10,A9,GLIB_001:37; then A.first() = W.1 by A11,A12,GLIB_001:30; then B.first() = W.first() by A8,A14,GLIB_001:30; then B is_Walk_from W.first(),W.last() by A19,GLIB_001:def 23; hence contradiction by A1,A18,Def2; end; theorem for G being _Graph st G is connected for A,B being non empty Subset of the_Vertices_of G st A misses B holds ex P being Path of G st P is minlength & P is non trivial & P.first() in A & P.last() in B & for n being odd Nat st 1 < n & n < len P holds not P.n in A & not P.n in B proof let G be _Graph such that A1: G is connected; let A,B be non empty Subset of the_Vertices_of G such that A2: A misses B; set X = { len P where P is Path of G : P.first() in A & P.last() in B }; A3: X c= NAT proof let x be set; assume x in X; then ex P being Path of G st x = len P & P.first() in A & P.last() in B; hence thesis; end; consider b being set such that A4: b in B by XBOOLE_0:def 1; reconsider b as Vertex of G by A4; consider a being set such that A5: a in A by XBOOLE_0:def 1; reconsider a as Vertex of G by A5; consider W being Walk of G such that A6: W is_Walk_from a,b by A1,GLIB_002:def 1; consider W2 being Path of G such that A7: W2 is_Walk_from W.first(),W.last() and W2 is minlength by Th39; W.last() = b by A6,GLIB_001:def 23; then A8: W2.last() in B by A4,A7,GLIB_001:def 23; W.first() = a by A6,GLIB_001:def 23; then W2.first() in A by A5,A7,GLIB_001:def 23; then len W2 in X by A8; then reconsider X as non empty Subset of NAT by A3; min X in X by XXREAL_2:def 7; then consider M being Path of G such that A9: len M = min X and A10: M.first() in A and A11: M.last() in B; now let P2 be Path of G such that A12: P2 is_Walk_from M.first(),M.last(); A13: P2.last() in B by A11,A12,GLIB_001:def 23; P2.first() in A by A10,A12,GLIB_001:def 23; then len P2 in X by A13; hence len P2 >= len M by A9,XXREAL_2:def 7; end; then A14: M is minlength by Th38; A15: now let n be odd Nat such that A16: 1 < n and A17: n < len M; reconsider nn = n as Element of NAT by ORDINAL1:def 12; assume A18: M.n in A or M.n in B; per cases by A18; suppose A19: M.n in A; reconsider T = M.cut(nn,len M) as Path of G; A20: T.last() in B by A11,A17,GLIB_001:37; len T + nn = len M+1 by A17,GLIB_001:36; then A21: len T + 0 < len M + 1 + (-n) + (n + (-1)) by A16,XREAL_1:8; T.first() in A by A17,A19,GLIB_001:37; then len T in X by A20; hence contradiction by A9,A21,XXREAL_2:def 7; end; suppose A22: M.n in B; reconsider T = M.cut(1,nn) as Path of G; A23: 2*0+1 <= n by A16; then A24: T.last() = M.nn by A17,GLIB_001:37; 2*0+1 <= n by A16; then A25: len T + 1 = nn + 1 by A17,GLIB_001:36; T.first() = M.1 by A17,A23,GLIB_001:37; then len T in X by A10,A22,A24; hence contradiction by A9,A17,A25,XXREAL_2:def 7; end; end; now assume M.first() = M.last(); then M.first() in A /\ B by A10,A11,XBOOLE_0:def 4; hence contradiction by A2,XBOOLE_0:def 7; end; then M is non trivial by GLIB_001:127; hence thesis by A10,A11,A14,A15; end; begin :: Adjacency and complete graphs definition let G be _Graph, a,b be Vertex of G; pred a,b are_adjacent means :: DefAdjacent :Def3: ex e being set st e Joins a,b,G; symmetry by GLIB_000:14; end; theorem Th44: :: VAdjacent00 for G1,G2 being _Graph st G1 == G2 for u1,v1 being Vertex of G1 st u1,v1 are_adjacent for u2,v2 being Vertex of G2 st u1=u2 & v1=v2 holds u2,v2 are_adjacent proof let G1,G2 be _Graph such that A1: G1 == G2; let u1,v1 be Vertex of G1; assume u1,v1 are_adjacent; then consider e being set such that A2: e Joins u1,v1,G1 by Def3; let u2,v2 be Vertex of G2 such that A3: u1=u2 and A4: v1=v2; e Joins u2,v2,G2 by A1,A3,A4,A2,GLIB_000:88; hence thesis by Def3; end; theorem Th45: :: VAdjacent01 for G being _Graph, S being non empty Subset of the_Vertices_of G for H being inducedSubgraph of G,S for u, v being Vertex of G, t, w being Vertex of H st u = t & v = w holds u,v are_adjacent iff t,w are_adjacent proof let G be _Graph, S be non empty Subset of the_Vertices_of G; let H be inducedSubgraph of G,S; let u, v be Vertex of G, t, w be Vertex of H such that A1: u = t and A2: v = w; A3: S = the_Vertices_of H by GLIB_000:def 37; hereby assume u,v are_adjacent; then consider e being set such that A4: e Joins u,v,G by Def3; e Joins t,w,H by A1,A2,A3,A4,Th19; hence t,w are_adjacent by Def3; end; assume t,w are_adjacent; then consider e being set such that A5: e Joins t,w,H by Def3; e Joins u,v,G by A1,A2,A5,GLIB_000:72; hence thesis by Def3; end; theorem Th46: :: PathLike05 for G being _Graph, W being Walk of G st W.first() <> W.last() & not W.first(),W.last() are_adjacent holds W.length() >= 2 proof let G be _Graph, W be Walk of G such that A1: W.first() <> W.last() and A2: not W.first(),W.last() are_adjacent; set l = W.length(); assume l < 2; then l < 1+1; then A3: l <= 1 by NAT_1:13; per cases by A3,NAT_1:25; suppose l = 0; then W is trivial by GLIB_001:def 26; hence contradiction by A1,GLIB_001:127; end; suppose l = 1; then A4: len W = 2*1+1 by GLIB_001:112 .= 3; 1 = 2*0+1; then W.(1+1) Joins W.1,W.(1+2),G by A4,GLIB_001:def 3; hence contradiction by A2,A4,Def3; end; end; theorem Th47: :: PathBuilder00 :: add sequences of vertices and edges:: PathBuilder01 for G being _Graph, v1,v2,v3 being Vertex of G st v1<>v2 & v1<> v3 & v2<>v3 & v1,v2 are_adjacent & v2,v3 are_adjacent ex P being Path of G, e1, e2 being set st P is open & len P = 5 & P.length() = 2 & e1 Joins v1,v2,G & e2 Joins v2,v3,G & P.edges() = {e1,e2} & P.vertices() = {v1,v2,v3} & P.1 = v1 & P. 3 = v2 & P.5 = v3 proof let G be _Graph; let v1,v2,v3 be Vertex of G such that A1: v1 <> v2 and A2: v1 <> v3 and A3: v2 <> v3 and A4: v1,v2 are_adjacent and A5: v2,v3 are_adjacent; consider e1 being set such that A6: e1 Joins v1,v2,G by A4,Def3; set P1 = G.walkOf(v1,e1,v2); A7: P1.vertices() = {v1,v2} by A6,GLIB_001:91; then A8: not v3 in P1.vertices() by A2,A3,TARSKI:def 2; consider e2 being set such that A9: e2 Joins v2,v3,G by A5,Def3; set P = P1.addEdge(e2); A10: P1.last() = v2 by A6,GLIB_001:15; then A11: P.last() = v3 by A9,GLIB_001:63; A12: P1.first() = v1 by A6,GLIB_001:15; then A13: P.first() = v1 by A9,A10,GLIB_001:63; P1 is open by A1,A12,A10,GLIB_001:def 24; then reconsider P as Path of G by A9,A10,A8,GLIB_001:151; take P,e1,e2; thus P is open by A2,A13,A11,GLIB_001:def 24; A14: len P1 = 3 by A6,GLIB_001:14; then A15: len P = 3 + 2 by A9,A10,GLIB_001:64; hence len P = 5; 5 = 2*P.length() + 1 by A15,GLIB_001:112; hence P.length() = 2; thus e1 Joins v1,v2,G by A6; thus e2 Joins v2,v3,G by A9; P1.edges() = {e1} by A6,GLIB_001:108; then P.edges() = {e1} \/ {e2} by A9,A10,GLIB_001:111; hence P.edges() = {e1,e2} by ENUMSET1:1; P.vertices() = {v1,v2} \/ {v3} by A9,A10,A7,GLIB_001:95; hence P.vertices() = {v1,v2,v3} by ENUMSET1:3; thus P.1 = v1 by A13; 3 in dom P1 by A14,FINSEQ_3:25; hence P.3 = P1.3 by A9,A10,GLIB_001:65 .= v2 by A6,A10,GLIB_001:14; thus thesis by A11,A15; end; theorem Th48: for G being _Graph, v1,v2,v3,v4 being Vertex of G st v1<>v2 & v1 <>v3 & v2<>v3 & v2<>v4 & v3<>v4 & v1,v2 are_adjacent & v2,v3 are_adjacent & v3, v4 are_adjacent ex P being Path of G st len P = 7 & P.length() = 3 & P .vertices() = {v1,v2,v3,v4} & P.1 = v1 & P.3 = v2 & P.5 = v3 & P.7 = v4 proof let G be _Graph, v1,v2,v3,v4 be Vertex of G such that A1: v1<>v2 and A2: v1<>v3 and A3: v2<>v3 and A4: v2<>v4 and A5: v3<>v4 and A6: v1,v2 are_adjacent and A7: v2,v3 are_adjacent and A8: v3,v4 are_adjacent; consider R being Path of G,e1,e2 being set such that A9: R is open and A10: len R = 5 and R.length() = 2 and A11: e1 Joins v1,v2,G and A12: e2 Joins v2,v3,G and A13: R.edges() = {e1,e2} and A14: R.vertices() = {v1,v2,v3} and A15: R.1 = v1 and A16: R.3 = v2 and A17: R.5 = v3 by A1,A2,A3,A6,A7,Th47; consider e3 being set such that A18: e3 Joins v3,v4,G by A8,Def3; A19: for n being odd Element of NAT st 1 < n & n <= len R holds R.n <> v4 proof let n be odd Element of NAT such that A20: 1 < n and A21: n <= len R; per cases by A10,A20,A21,Th8,XXREAL_0:2; suppose n = 3; hence thesis by A4,A16; end; suppose n = 5; hence thesis by A5,A17; end; end; A22: e2 <> e3 by A3,A4,A18,A12,GLIB_000:15; set P = R.addEdge(e3); e1 <> e3 by A2,A3,A18,A11,GLIB_000:15; then not e3 in R.edges() by A13,A22,TARSKI:def 2; then reconsider P as Path of G by A18,A9,A10,A17,A19,GLIB_001:150; take P; A23: len P = 5 + 2 by A18,A10,A17,GLIB_001:64; hence len P = 7; 7 = 2*P.length() + 1 by A23,GLIB_001:112; hence P.length() = 3; P.vertices() = {v1,v2,v3} \/ {v4} by A18,A10,A14,A17,GLIB_001:95; hence P.vertices() = {v1,v2,v3,v4} by ENUMSET1:6; 1 in dom R by A10,FINSEQ_3:25; hence P.1 = v1 by A18,A10,A15,A17,GLIB_001:65; 3 in dom R by A10,FINSEQ_3:25; hence P.3 = v2 by A18,A10,A16,A17,GLIB_001:65; 5 in dom R by A10,FINSEQ_3:25; hence P.5 = v3 by A18,A10,A17,GLIB_001:65; P.last() = v4 by A18,A10,A17,GLIB_001:63; hence thesis by A23; end; definition let G be _Graph, S be set; func G.AdjacentSet(S) -> Subset of the_Vertices_of G equals {u where u is Vertex of G : not u in S & ex v being Vertex of G st (v in S & u,v are_adjacent )}; coherence proof set X = {u where u is Vertex of G : not u in S & ex v being Vertex of G st (v in S & u,v are_adjacent)}; now let x be set; assume x in X; then ex u being Vertex of G st u=x &( not u in S)& ex v being Vertex of G st v in S & u,v are_adjacent; hence x in the_Vertices_of G; end; hence thesis by TARSKI:def 3; end; end; theorem for G being _Graph, S, x being set st x in G.AdjacentSet(S) holds not x in S proof let G be _Graph, S,x be set; assume x in G.AdjacentSet(S); then ex t being Vertex of G st t=x &( not t in S)& ex v being Vertex of G st v in S & t,v are_adjacent; hence thesis; end; theorem Th50: :: Adjacent00 for G being _Graph, S being set for u being Vertex of G holds u in G.AdjacentSet(S) iff not u in S & ex v being Vertex of G st v in S & u,v are_adjacent proof let G be _Graph, S be set; let u be Vertex of G; hereby assume u in G.AdjacentSet(S); then ex t being Vertex of G st u=t &( not t in S)& ex v being Vertex of G st v in S & t,v are_adjacent; hence not u in S & ex v being Vertex of G st v in S & u,v are_adjacent; end; assume that A1: not u in S and A2: ex v being Vertex of G st v in S & u,v are_adjacent; thus thesis by A1,A2; end; theorem Th51: :: Adjacent01 for G1,G2 being _Graph st G1 == G2 for S being set holds G1 .AdjacentSet(S) = G2.AdjacentSet(S) proof let G1,G2 be _Graph such that A1: G1 == G2; let S be set; A2: now let x be set such that A3: x in G2.AdjacentSet(S); reconsider t2 = x as Vertex of G2 by A3; A4: not t2 in S by A3,Th50; consider v2 being Vertex of G2 such that A5: v2 in S and A6: t2,v2 are_adjacent by A3,Th50; reconsider t1 = t2, v1 = v2 as Vertex of G1 by A1,GLIB_000:def 34; t1,v1 are_adjacent by A1,A6,Th44; hence x in G1.AdjacentSet(S) by A4,A5; end; now let x be set such that A7: x in G1.AdjacentSet(S); reconsider t1 = x as Vertex of G1 by A7; A8: not t1 in S by A7,Th50; consider v1 being Vertex of G1 such that A9: v1 in S and A10: t1,v1 are_adjacent by A7,Th50; reconsider t2 = t1, v2 = v1 as Vertex of G2 by A1,GLIB_000:def 34; t2,v2 are_adjacent by A1,A10,Th44; hence x in G2.AdjacentSet(S) by A8,A9; end; hence thesis by A2,TARSKI:1; end; theorem Th52: :: AdjacentV00 for G being _Graph, u,v being Vertex of G holds u in G .AdjacentSet({v}) iff u <> v & v,u are_adjacent proof let G be _Graph, u,v be Vertex of G; A1: v in {v} by TARSKI:def 1; hereby assume A2: u in G.AdjacentSet({v}); then consider x being Vertex of G such that A3: x in {v} and A4: u,x are_adjacent by Th50; x = v by A3,TARSKI:def 1; hence u <> v & v,u are_adjacent by A2,A3,A4,Th50; end; assume that A5: u <> v and A6: v,u are_adjacent; not u in {v} by A5,TARSKI:def 1; hence thesis by A6,A1; end; theorem for G being _Graph, x,y being set holds x in G.AdjacentSet({y}) iff y in G.AdjacentSet({x}) proof let G be _Graph, x,y be set; hereby assume A1: x in G.AdjacentSet({y}); then reconsider xg = x as Vertex of G; now consider vy being Vertex of G such that A2: vy in {y} and vy,xg are_adjacent by A1,Th50; assume A3: not y in the_Vertices_of G; vy = y by A2,TARSKI:def 1; hence contradiction by A3; end; then reconsider yg = y as Vertex of G; A4: xg,yg are_adjacent by A1,Th52; xg <> yg by A1,Th52; hence y in G.AdjacentSet({x}) by A4,Th52; end; assume A5: y in G.AdjacentSet({x}); then reconsider yg = y as Vertex of G; now consider vx being Vertex of G such that A6: vx in {x} and vx,yg are_adjacent by A5,Th50; assume A7: not x in the_Vertices_of G; vx = x by A6,TARSKI:def 1; hence contradiction by A7; end; then reconsider xg = x as Vertex of G; A8: xg,yg are_adjacent by A5,Th52; xg <> yg by A5,Th52; hence thesis by A8,Th52; end; theorem for G being _Graph, C being Path of G st C is Cycle-like & C.length() > 3 for x being Vertex of G st x in C.vertices() ex m,n being odd Nat st m+2 < n & n <= len C & not (m=1 & n = len C) & not (m=1 & n = len C-2) & not (m=3 & n = len C) & C.m <> C.n & C.m in G.AdjacentSet({x}) & C.n in G.AdjacentSet({x}) proof let G be _Graph, C be Path of G such that A1: C is Cycle-like and A2: C.length() > 3; C.length() >= 3+1 by A2,NAT_1:13; then 2*C.length() >= 2*4 by XREAL_1:64; then 2*C.length() + 1 >= 8 + 1 by XREAL_1:7; then A3: len C >= 9 by GLIB_001:112; let x be Vertex of G; assume x in C.vertices(); then consider n being odd Element of NAT such that A4: n <= len C and A5: C.n = x by GLIB_001:87; A6: 0+1 <= n by ABIAN:12; per cases; suppose A7: n = 1 or n = len C; reconsider i=2*1+1 as odd Nat; reconsider k=2*0+1 as odd Nat; A8: len C + 0 > 9 + (-6) by A3,XREAL_1:8; then reconsider Ci=C.i as Vertex of G by GLIB_001:7; A9: now per cases by A7; suppose n = 1; hence x = C.k by A5; end; suppose n = len C; then x = C.last() by A5; then x = C.first() by A1,GLIB_001:def 24; hence x = C.k; end; end; then A10: x <> Ci by A8,GLIB_001:def 28; len C + (-2) >= 9 + (-2) by A3,XREAL_1:7; then len C - 2*1 >= 0 by XXREAL_0:2; then len C - 2 is odd Element of NAT by INT_1:3; then reconsider j=len C-2 as odd Nat; take i, j; A11: len C + (-2) >= 9 + (-2) by A3,XREAL_1:7; hence i+2 < j by XXREAL_0:2; A12: len C + 0 > len C+(-2) by XREAL_1:8; hence j <= len C; thus not (i=1 & j=len C) & not (i=1 & j=len C-2) & not (i=3 & j=len C); hereby assume A13: C.i = C.j; i+2+(-2) < j+0 by A11,XXREAL_0:2; hence contradiction by A12,A13,GLIB_001:def 28; end; len C + 0 > 9 + (-8) by A3,XREAL_1:8; then C.(k+1) Joins C.k,C.i,G by GLIB_001:def 3; then x,Ci are_adjacent by A9,Def3; hence C.i in G.AdjacentSet({x}) by A10,Th52; A14: j in NAT by ORDINAL1:def 12; then reconsider Cj=C.j as Vertex of G by A12,GLIB_001:7; A15: now per cases by A7; suppose n = 1; then x = C.first() by A5; then x = C.last() by A1,GLIB_001:def 24; hence x = C.(j+2); end; suppose n = len C; hence x = C.(j+2) by A5; end; end; A16: now assume x = Cj; then A17: j = 1 by A14,A12,A15,GLIB_001:def 28; j+2 = len C; hence contradiction by A3,A17; end; C.(j+1) Joins Cj,x,G by A14,A12,A15,GLIB_001:def 3; then x,Cj are_adjacent by Def3; hence thesis by A16,Th52; end; suppose A18: not (n = 1 or n = len C); then 2*0+1 < n by A6,XXREAL_0:1; then 1+2 <= n by Th4; then 3+(-2) <= n+(-2) by XREAL_1:7; then 0 <= n-2*1; then n-2 is odd Element of NAT by INT_1:3; then reconsider i=n-2 as odd Nat; A19: i+0 < i+2 by XREAL_1:8; then reconsider Ci=C.i as Vertex of G by A4,GLIB_001:7,XXREAL_0:2; reconsider j=n+2 as odd Nat; A20: n < len C by A4,A18,XXREAL_0:1; then A21: n+2 <= len C -2 + 2 by Th4; then reconsider Cj=C.j as Vertex of G by GLIB_001:7; A22: now A23: n+2 > n+0 by XREAL_1:8; assume Cj = x; hence contradiction by A5,A18,A21,A23,GLIB_001:def 28; end; take i,j; n+0 < n+2 by XREAL_1:8; hence i+2 < j & j <= len C by A20,Th4; A24: now assume that A25: i = 1 and A26: j = len C; j = i + 4; hence contradiction by A3,A25,A26; end; hence not (i = 1 & j = len C); hereby assume that A27: i = 1 and A28: j = len C-2; len C+(-2) >= 9+(-3) by A3,XREAL_1:7; hence contradiction by A27,A28; end; hereby assume that A29: i = 3 and A30: j = len C; j = i + 4; hence contradiction by A3,A29,A30; end; A31: i in NAT by ORDINAL1:def 12; A32: now A33: n+0 > n+(-2) by XREAL_1:8; assume Ci = x; hence contradiction by A4,A5,A18,A31,A33,GLIB_001:def 28; end; A34: n+2 <= len C-2+2 by A20,Th4; hereby A35: i+2+(-2) < j+0 by XREAL_1:8; assume C.i = C.j; hence contradiction by A31,A34,A24,A35,GLIB_001:def 28; end; i < len C by A4,A19,XXREAL_0:2; then C.(i+1) Joins C.i,C.(i+2),G by A31,GLIB_001:def 3; then x,Ci are_adjacent by A5,Def3; hence C.i in G.AdjacentSet({x}) by A32,Th52; C.(n+1) Joins C.n,C.j,G by A20,GLIB_001:def 3; then x,Cj are_adjacent by A5,Def3; hence thesis by A22,Th52; end; end; theorem Th55: :: Cycle01a for G being _Graph, C being Path of G st C is Cycle-like & C .length() > 3 for x being Vertex of G st x in C.vertices() ex m,n being odd Nat st m+2 < n & n <= len C & C.m <> C.n & C.m in G.AdjacentSet({x}) & C.n in G.AdjacentSet({x}) & for e being set st e in C.edges() holds not e Joins C.m,C.n,G proof let G be _Graph, C be Path of G such that A1: C is Cycle-like and A2: C.length() > 3; C.length() >= 3+1 by A2,NAT_1:13; then 2*C.length() >= 2*4 by XREAL_1:64; then 2*C.length() + 1 >= 8 + 1 by XREAL_1:7; then A3: len C >= 9 by GLIB_001:112; let x be Vertex of G; assume x in C.vertices(); then consider n being odd Element of NAT such that A4: n <= len C and A5: C.n = x by GLIB_001:87; A6: 0+1 <= n by ABIAN:12; per cases; suppose A7: n = 1 or n = len C; reconsider k=2*0+1 as odd Nat; A8: now per cases by A7; suppose n = 1; hence x = C.k by A5; end; suppose n = len C; then x = C.last() by A5; then x = C.first() by A1,GLIB_001:def 24; hence x = C.k; end; end; len C + (-2) >= 9 + (-2) by A3,XREAL_1:7; then len C - 2*1 >= 0 by XXREAL_0:2; then len C-2 is odd Element of NAT by INT_1:3; then reconsider j=len C-2 as odd Nat; reconsider i=2*1+1 as odd Nat; take i, j; A9: len C + (-2) >= 9 + (-2) by A3,XREAL_1:7; hence i+2 < j by XXREAL_0:2; A10: len C + 0 > len C+(-2) by XREAL_1:8; hence j <= len C; i < j by A9,XXREAL_0:2; then A11: i < len C by A10,XXREAL_0:2; hereby assume A12: C.i = C.j; i+2+(-2) < j+0 by A9,XXREAL_0:2; hence contradiction by A10,A12,GLIB_001:def 28; end; A13: len C + 0 > 9 + (-6) by A3,XREAL_1:8; then reconsider Ci=C.i as Vertex of G by GLIB_001:7; len C + 0 > 9 + (-8) by A3,XREAL_1:8; then C.(k+1) Joins C.k,C.i,G by GLIB_001:def 3; then A14: x,Ci are_adjacent by A8,Def3; x <> Ci by A13,A8,GLIB_001:def 28; hence C.i in G.AdjacentSet({x}) by A14,Th52; A15: j <> 1 by A9; A16: j in NAT by ORDINAL1:def 12; then reconsider Cj=C.j as Vertex of G by A10,GLIB_001:7; A17: now per cases by A7; suppose n = 1; then x = C.first() by A5; then x = C.last() by A1,GLIB_001:def 24; hence x = C.(j+2); end; suppose n = len C; hence x = C.(j+2) by A5; end; end; A18: now assume x = Cj; then A19: j = 1 by A16,A10,A17,GLIB_001:def 28; j+2 = len C; hence contradiction by A3,A19; end; C.(j+1) Joins C.j,C.(j+2),G by A16,A10,GLIB_001:def 3; then x,Cj are_adjacent by A17,Def3; hence C.j in G.AdjacentSet({x}) by A18,Th52; let e be set such that A20: e in C.edges() and A21: e Joins C.i,C.j,G; consider k being even Element of NAT such that A22: 1 <= k and A23: k <= len C and A24: C.k = e by A20,GLIB_001:99; A25: (the_Source_of G).e = C.i & (the_Target_of G).e = C.j or ( the_Source_of G).e = C.j & (the_Target_of G).e = C.i by A21,GLIB_000:def 13; k in dom C by A22,A23,FINSEQ_3:25; then consider ku1 being odd Element of NAT such that A26: ku1 = k-1 and A27: k-1 in dom C and A28: k+1 in dom C and A29: C.k Joins C.(ku1), C.(k+1),G by GLIB_001:9; A30: ku1 <= len C by A26,A27,FINSEQ_3:25; A31: k+1 <= len C by A28,FINSEQ_3:25; per cases by A24,A29,A25,GLIB_000:def 13; suppose A32: C.i = C.ku1 & C.j = C.(k+1); then i+2 = k-1+(1+1) by A26,A30,A11,Th25 .= j by A10,A31,A15,A32,Th25; hence contradiction by A9; end; suppose A33: C.i = C.(k+1) & C.j = C.ku1; then i = k+1 by A31,A11,Th25; hence contradiction by A10,A26,A30,A15,A33,Th25; end; end; suppose A34: not (n = 1 or n = len C); then 2*0+1 < n by A6,XXREAL_0:1; then 1+2 <= n by Th4; then 3+(-2) <= n+(-2) by XREAL_1:7; then n-2*1 is odd Element of NAT by INT_1:3; then reconsider i=n-2*1 as odd Nat; A35: i+0 < i+2 by XREAL_1:8; then reconsider Ci=C.i as Vertex of G by A4,GLIB_001:7,XXREAL_0:2; reconsider j=n+2 as odd Nat; take i, j; n+0 < n+2 by XREAL_1:8; hence i+2 < j; A36: n < len C by A4,A34,XXREAL_0:1; hence A37: j <= len C by Th4; then reconsider Cj=C.j as Vertex of G by GLIB_001:7; A38: i in NAT by ORDINAL1:def 12; A39: now A40: n+0 > n+(-2) by XREAL_1:8; assume Ci = x; hence contradiction by A4,A5,A34,A38,A40,GLIB_001:def 28; end; A41: now assume that A42: i = 1 and A43: j = len C; j = i + 4; hence contradiction by A3,A42,A43; end; hereby A44: i+2+(-2) < j+0 by XREAL_1:8; assume C.i = C.j; hence contradiction by A38,A37,A41,A44,GLIB_001:def 28; end; A45: i < len C by A4,A35,XXREAL_0:2; then C.(i+1) Joins C.i,C.(i+2),G by A38,GLIB_001:def 3; then x,Ci are_adjacent by A5,Def3; hence C.i in G.AdjacentSet({x}) by A39,Th52; 1+2 <= j by A6,XREAL_1:7; then A46: j <> 1; A47: n+2 <= len C -2 + 2 by A36,Th4; A48: now A49: n+2 > n+0 by XREAL_1:8; assume Cj = x; hence contradiction by A5,A34,A47,A49,GLIB_001:def 28; end; C.(n+1) Joins C.n,C.j,G by A36,GLIB_001:def 3; then x,Cj are_adjacent by A5,Def3; hence C.j in G.AdjacentSet({x}) by A48,Th52; let e be set such that A50: e in C.edges() and A51: e Joins C.i,C.j,G; consider k being even Element of NAT such that A52: 1 <= k and A53: k <= len C and A54: C.k = e by A50,GLIB_001:99; A55: (the_Source_of G).e = C.i & (the_Target_of G).e = C.j or ( the_Source_of G).e = C.j & (the_Target_of G).e = C.i by A51,GLIB_000:def 13; 1+1 <= k+1 by A52,XREAL_1:7; then A56: k+1 <> 1; A57: k-1 < len C by A53,XREAL_1:146,XXREAL_0:2; k in dom C by A52,A53,FINSEQ_3:25; then consider ku1 being odd Element of NAT such that A58: ku1 = k-1 and k-1 in dom C and A59: k+1 in dom C and A60: C.k Joins C.(ku1), C.(k+1),G by GLIB_001:9; A61: k+1 <= len C by A59,FINSEQ_3:25; per cases by A54,A60,A55,GLIB_000:def 13; suppose A62: C.i = C.ku1 & C.j = C.(k+1); then i+2 = k-1+(1+1) by A45,A58,A57,Th25 .= j by A37,A61,A46,A56,A62,Th25; hence contradiction; end; suppose A63: C.i = C.(k+1) & C.j = C.ku1; per cases by A37,A45,A58,A57,A61,A63,Th25; suppose i = k+1 & j = k-1; hence contradiction; end; suppose A64: i = k+1 & k-1 = 1 & j = len C; j = i+4; hence contradiction by A3,A64; end; suppose A65: i = 1 & k+1 = len C & j = k-1; then k+1 = 7; hence contradiction by A3,A65; end; suppose i = 1 & k+1 = len C & k-1 = 1 & j = len C; hence contradiction; end; end; end; end; :: Gilbert's definition of isolated does not allow a vertex to have a :: loop and a vertex just with a loop on it is NOT isolated. :: This needs to be fixed, e.g. :: v is isolated means G.AdjacentSet({v}) = {} :: But we can keep the old one and the new one can be expressed just :: by G.AdjacentSet({v}) = {}. Should this be revised? :: Ask Lorna and Ryan. For loopless graphs it :: does not matter, see below. theorem :: AdjacentV01: for G being loopless _Graph, u being Vertex of G holds G.AdjacentSet({ u}) = {} iff u is isolated proof let G be loopless _Graph, u be Vertex of G; hereby assume A1: G.AdjacentSet({u}) = {}; now assume u.edgesInOut() <> {}; then consider e being set such that A2: e in u.edgesInOut() by XBOOLE_0:def 1; consider v being Vertex of G such that A3: e Joins u,v,G by A2,GLIB_000:64; A4: now A5: e in the_Edges_of G by A3,GLIB_000:def 13; assume A6: u = v; then A7: (the_Target_of G).e = u by A3,GLIB_000:def 13; (the_Source_of G).e = u by A3,A6,GLIB_000:def 13; hence contradiction by A5,A7,GLIB_000:def 18; end; v,u are_adjacent by A3,Def3; hence contradiction by A1,A4,Th52; end; hence u is isolated by GLIB_000:def 49; end; assume u is isolated; then A8: u.edgesInOut() = {} by GLIB_000:def 49; now let v be set such that A9: v in G.AdjacentSet({u}); reconsider v as Vertex of G by A9; v,u are_adjacent by A9,Th52; then ex e being set st e Joins v,u,G by Def3; hence contradiction by A8,GLIB_000:14,62; end; hence thesis by XBOOLE_0:def 1; end; theorem Th57: :: Connected0 for G being _Graph, G0 being Subgraph of G, S being non empty Subset of the_Vertices_of G, x being Vertex of G, G1 being (inducedSubgraph of G,S), G2 being (inducedSubgraph of G,S\/{x}) st G1 is connected & x in G .AdjacentSet(the_Vertices_of G1) holds G2 is connected proof let G be _Graph, G0 be Subgraph of G, S be non empty Subset of the_Vertices_of G, x be Vertex of G, G1 be (inducedSubgraph of G,S), G2 be ( inducedSubgraph of G,S\/{x}) such that A1: G1 is connected and A2: x in G.AdjacentSet(the_Vertices_of G1); A3: the_Vertices_of G1 = S by GLIB_000:def 37; then consider xs being Vertex of G such that A4: xs in S and A5: x,xs are_adjacent by A2,Th50; consider e being set such that A6: e Joins x,xs,G by A5,Def3; reconsider Sx = S\/{x} as Subset of the_Vertices_of G; let u,v be Vertex of G2; A7: the_Vertices_of G2 = Sx by GLIB_000:def 37; then A8: u in S or u in {x} by XBOOLE_0:def 3; x in {x} by TARSKI:def 1; then A9: x in Sx by XBOOLE_0:def 3; A10: xs in Sx by A4,XBOOLE_0:def 3; e Joins xs,x,G by A6,GLIB_000:14; then A11: e Joins xs,x,G2 by A9,A10,Th19; then A12: e Joins x,xs,G2 by GLIB_000:14; A13: v in S or v in {x} by A7,XBOOLE_0:def 3; A14: G1 is inducedSubgraph of G2,S by Th30,XBOOLE_1:7; per cases by A8,A13,TARSKI:def 1; suppose A15: u in S & v in S; the_Vertices_of G1 = S by GLIB_000:def 37; then consider W being Walk of G1 such that A16: W is_Walk_from u,v by A1,A15,GLIB_002:def 1; reconsider W as Walk of G2 by A14,GLIB_001:167; take W; thus thesis by A16,GLIB_001:19; end; suppose A17: u in S & v = x; then consider W being Walk of G1 such that A18: W is_Walk_from u,xs by A1,A3,A4,GLIB_002:def 1; reconsider W as Walk of G2 by A14,GLIB_001:167; take W.append(G2.walkOf(xs,e,x)); A19: G2.walkOf(xs,e,x) is_Walk_from xs,x by A11,GLIB_001:15; W is_Walk_from u, xs by A18,GLIB_001:19; hence thesis by A17,A19,GLIB_001:31; end; suppose A20: u = x & v in S; then consider W being Walk of G1 such that A21: W is_Walk_from xs,v by A1,A3,A4,GLIB_002:def 1; reconsider W as Walk of G2 by A14,GLIB_001:167; take G2.walkOf(x,e,xs).append(W); A22: G2.walkOf(x,e,xs) is_Walk_from x,xs by A12,GLIB_001:15; W is_Walk_from xs, v by A21,GLIB_001:19; hence thesis by A20,A22,GLIB_001:31; end; suppose u = x & v = x; then G2.walkOf(u) is_Walk_from u,v by GLIB_001:13; hence thesis; end; end; theorem Th58: :: Simplicial2a for G being _Graph for S being non empty Subset of the_Vertices_of G for H being inducedSubgraph of G,S for u being Vertex of G st u in S & G.AdjacentSet({u}) c= S for v being Vertex of H st u=v holds G .AdjacentSet({u}) = H.AdjacentSet({v}) proof let G be _Graph; let S be non empty Subset of the_Vertices_of G; let G2 be inducedSubgraph of G,S; let u be Vertex of G such that A1: u in S and A2: G.AdjacentSet({u}) c= S; let v be Vertex of G2 such that A3: u=v; now let x be set; hereby assume A4: x in G.AdjacentSet({u}); then reconsider y=x as Vertex of G; reconsider w=x as Vertex of G2 by A2,A4,GLIB_000:def 37; y,u are_adjacent by A4,Th52; then consider e being set such that A5: e Joins y,u,G by Def3; e Joins y,u,G2 by A1,A2,A4,A5,Th19; then A6: w,v are_adjacent by A3,Def3; w <> v by A3,A4,Th52; hence x in G2.AdjacentSet({v}) by A6,Th52; end; assume A7: x in G2.AdjacentSet({v}); then reconsider y=x as Vertex of G2; x in the_Vertices_of G2 by A7; then reconsider w=x as Vertex of G; y,v are_adjacent by A7,Th52; then consider e being set such that A8: e Joins y,v,G2 by Def3; e Joins y,v,G by A8,GLIB_000:72; then A9: w,u are_adjacent by A3,Def3; w <> u by A3,A7,Th52; hence x in G.AdjacentSet({u}) by A9,Th52; end; hence thesis by TARSKI:1; end; :: Adjacency set as a subgraph of G definition let G be _Graph, S be set; mode AdjGraph of G,S -> Subgraph of G means :Def5: it is inducedSubgraph of G,G.AdjacentSet(S) if S is Subset of the_Vertices_of G; existence proof set T = the inducedSubgraph of G,G.AdjacentSet(S); T is Subgraph of G; hence thesis; end; consistency; end; theorem Th59: :: AdjGraph00 for G1, G2 be _Graph st G1 == G2 for u1 being Vertex of G1, u2 being Vertex of G2 st u1 = u2 for H1 being AdjGraph of G1,{u1}, H2 being AdjGraph of G2,{u2} holds H1 == H2 proof let G1,G2 be _Graph such that A1: G1 == G2; let u1 be Vertex of G1, u2 be Vertex of G2 such that A2: u1 = u2; set G2Adj = G2.AdjacentSet({u2}); set G1Adj = G1.AdjacentSet({u1}); A3: G1Adj = G2Adj by A1,A2,Th51; let H1 be AdjGraph of G1,{u1}; let H2 be AdjGraph of G2,{u2}; A4: H1 is inducedSubgraph of G1,G1Adj by Def5; A5: H2 is inducedSubgraph of G2,G2Adj by Def5; per cases; suppose A6: not G1Adj is non empty Subset of the_Vertices_of G1; then H1 == G1 by A4,GLIB_000:def 37; then A7: H1 == G2 by A1,GLIB_000:85; H2 == G2 by A5,A3,A6,GLIB_000:def 37; hence thesis by A7,GLIB_000:85; end; suppose A8: G1Adj is non empty Subset of the_Vertices_of G1; then the_Vertices_of H1 = G1Adj by A4,GLIB_000:def 37; then A9: the_Vertices_of H1 = the_Vertices_of H2 by A5,A3,GLIB_000:def 37; G1 is Subgraph of G2 by A1,GLIB_000:87; then A10: G1.edgesBetween(G1Adj) c= G2.edgesBetween(G1Adj) by GLIB_000:76; A11: the_Edges_of H1 = G1.edgesBetween(G1Adj) by A4,A8,GLIB_000:def 37; G2 is Subgraph of G1 by A1,GLIB_000:87; then A12: G2.edgesBetween(G1Adj) c= G1.edgesBetween(G1Adj) by GLIB_000:76; G2 is Subgraph of G1 by A1,GLIB_000:87; then A13: H2 is Subgraph of G1 by GLIB_000:43; the_Edges_of H2 = G2.edgesBetween(G2Adj) by A5,A3,A8,GLIB_000:def 37; then the_Edges_of H1 = the_Edges_of H2 by A3,A11,A10,A12,XBOOLE_0:def 10; hence thesis by A9,A13,GLIB_000:86; end; end; theorem Th60: :: Simplicial2b for G being _Graph for S being non empty Subset of the_Vertices_of G for H being inducedSubgraph of G,S for u being Vertex of G st u in S & G.AdjacentSet({u}) c= S & G.AdjacentSet({u}) <> {} for v being Vertex of H st u=v for Ga being AdjGraph of G,{u}, Ha being AdjGraph of H,{v} holds Ga == Ha proof let G be _Graph; let S being non empty Subset of the_Vertices_of G; let H be inducedSubgraph of G,S; let u be Vertex of G such that A1: u in S and A2: G.AdjacentSet({u}) c= S and A3: G.AdjacentSet({u}) <> {}; let v be Vertex of H; assume u=v; then A4: G.AdjacentSet({u}) = H.AdjacentSet({v}) by A1,A2,Th58; let Ga be AdjGraph of G,{u}, Ha being AdjGraph of H,{v}; A5: Ha is inducedSubgraph of H,H.AdjacentSet({v}) by Def5; A6: Ga is inducedSubgraph of G,G.AdjacentSet({u}) by Def5; then A7: the_Edges_of Ga = G.edgesBetween(G.AdjacentSet({u})) by A3,GLIB_000:def 37; the_Vertices_of Ga = G.AdjacentSet({u}) by A3,A6,GLIB_000:def 37; hence the_Vertices_of Ga = the_Vertices_of Ha by A4,A5,GLIB_000:def 37; the_Edges_of Ha = H.edgesBetween(H.AdjacentSet({v})) by A3,A4,A5, GLIB_000:def 37; hence A8: the_Edges_of Ga = the_Edges_of Ha by A2,A3,A4,A7,Th31; A9: the_Target_of Ga = (the_Target_of G)|the_Edges_of Ga by GLIB_000:45; Ha is inducedSubgraph of H,G.AdjacentSet({u}) by A4,Def5; then A10: Ha is inducedSubgraph of G,G.AdjacentSet({u}) by A2,A3,Th29; the_Source_of Ga = (the_Source_of G)|the_Edges_of Ga by GLIB_000:45; hence the_Source_of Ha = the_Source_of Ga & the_Target_of Ha = the_Target_of Ga by A8,A9,A10,GLIB_000:45; end; definition let G be _Graph; attr G is complete means :Def6: for u,v being Vertex of G st u <> v holds u, v are_adjacent; end; theorem Th61: :: Completetr for G being _Graph st G is trivial holds G is complete proof let G be _Graph; assume G is trivial; then consider x being Vertex of G such that A1: the_Vertices_of G = {x} by GLIB_000:22; let u,v being Vertex of G such that A2: u <> v and not u,v are_adjacent; u = x by A1,TARSKI:def 1; hence contradiction by A1,A2,TARSKI:def 1; end; registration cluster trivial -> complete for _Graph; coherence by Th61; end; registration cluster trivial simple complete for _Graph; existence proof set G = the trivial simple _Graph; take G; thus thesis; end; cluster non trivial finite simple complete for _Graph; existence proof set V = {0,1}, E = {0}, S = 0 .--> 0, T = 0 .--> 1; A1: dom T = E by FUNCOP_1:13; A2: now let x be set; assume x in E; then x = 0 by TARSKI:def 1; then T.x = 1 by FUNCOP_1:72; hence T.x in V by TARSKI:def 2; end; A3: now let x be set; assume x in E; then x = 0 by TARSKI:def 1; then S.x = 0 by FUNCOP_1:72; hence S.x in V by TARSKI:def 2; end; reconsider T as Function of E,V by A1,A2,FUNCT_2:3; dom S = E by FUNCOP_1:13; then reconsider S as Function of E,V by A3,FUNCT_2:3; set G = createGraph(V,E,S,T); take G; the_Source_of G = S by GLIB_000:6; then A4: (the_Source_of G).0 = 0 by FUNCOP_1:72; A5: the_Edges_of G = E by GLIB_000:6; now let e1,e2,v1,v2 be set such that A6: e1 Joins v1,v2,G and A7: e2 Joins v1,v2,G; e1 in {0} by A5,A6,GLIB_000:def 13; then A8: e1 = 0 by TARSKI:def 1; assume A9: e1 <> e2; e2 in {0} by A5,A7,GLIB_000:def 13; hence contradiction by A9,A8,TARSKI:def 1; end; then A10: G is non-multi by GLIB_000:def 20; A11: the_Vertices_of G = V by GLIB_000:6; now assume card (the_Vertices_of G) = 1; then ex x being set st the_Vertices_of G = {x} by CARD_2:42; hence contradiction by A11,ZFMISC_1:5; end; hence G is non trivial & G is finite by GLIB_000:def 19; the_Target_of G = T by GLIB_000:6; then A12: (the_Target_of G).0 = 1 by FUNCOP_1:72; 0 in the_Edges_of G by A5,TARSKI:def 1; then A13: 0 Joins 0,1,G by A4,A12,GLIB_000:def 13; now let v be set; let e being set such that A14: e Joins v,v,G; reconsider v as Vertex of G by A14,GLIB_000:13; e in the_Edges_of G by A14,GLIB_000:def 13; then e Joins 0,1,G by A5,A13,TARSKI:def 1; then 0 = v & 1 = v or 0 = v & 1 = v by A14,GLIB_000:15; hence contradiction; end; then G is loopless by GLIB_000:18; hence G is simple by A10; now let u,v be Vertex of G such that A15: u <> v; per cases by A11,TARSKI:def 2; suppose A16: u = 0; A17: 0 in the_Edges_of G by A5,TARSKI:def 1; v = 1 by A11,A15,A16,TARSKI:def 2; then 0 Joins u,v,G by A4,A12,A16,A17,GLIB_000:def 13; hence u,v are_adjacent by Def3; end; suppose A18: u = 1; A19: 0 in the_Edges_of G by A5,TARSKI:def 1; v = 0 by A11,A15,A18,TARSKI:def 2; then 0 Joins v,u,G by A4,A12,A18,A19,GLIB_000:def 13; hence u,v are_adjacent by Def3; end; end; hence thesis by Def6; end; end; theorem Th62: :: Complete00 for G1,G2 being _Graph st G1 == G2 holds G1 is complete implies G2 is complete proof let G1,G2 be _Graph such that A1: G1 == G2; assume A2: G1 is complete; now let u,v be Vertex of G2 such that A3: u <> v; reconsider v2=v as Vertex of G1 by A1,GLIB_000:def 34; reconsider u2=u as Vertex of G1 by A1,GLIB_000:def 34; u2,v2 are_adjacent by A2,A3,Def6; hence u,v are_adjacent by A1,Th44; end; hence thesis by Def6; end; theorem Th63: :: Complete01 for G being complete _Graph, S being Subset of the_Vertices_of G for H being inducedSubgraph of G,S holds H is complete proof let G be complete _Graph; let S be Subset of the_Vertices_of G; let H be inducedSubgraph of G,S; per cases; suppose S = {}; then H == G by GLIB_000:def 37; hence thesis by Th62; end; suppose S <> {}; then A1: the_Vertices_of H = S by GLIB_000:def 37; now let u,v be Vertex of H such that A2: u <> v; reconsider v2=v as Vertex of G by A1,TARSKI:def 3; reconsider u2=u as Vertex of G by A1,TARSKI:def 3; u2,v2 are_adjacent by A2,Def6; then consider e being set such that A3: e Joins u2,v2,G by Def3; e Joins u,v,H by A1,A3,Th19; hence u,v are_adjacent by Def3; end; hence thesis by Def6; end; end; begin :: Simplicial vertex :: Golumbic p. 81 definition let G be _Graph, v be Vertex of G; attr v is simplicial means :Def7: G.AdjacentSet({v}) <> {} implies for G2 being AdjGraph of G,{v} holds G2 is complete; end; theorem Th64: :: Simplicial0 for G being complete _Graph, v being Vertex of G holds v is simplicial proof let G be complete _Graph, v be Vertex of G; now let G2 be AdjGraph of G,{v}; G2 is inducedSubgraph of G,G.AdjacentSet({v}) by Def5; hence G2 is complete by Th63; end; hence thesis by Def7; end; theorem Th65: :: Simplicial01 for G being trivial _Graph, v being Vertex of G holds v is simplicial proof let G be trivial _Graph, v be Vertex of G; now assume G.AdjacentSet({v}) <> {}; then consider x being set such that A1: x in G.AdjacentSet({v}) by XBOOLE_0:def 1; A2: ex u being Vertex of G st x = u &( not u in {v})& ex v1 being Vertex of G st v1 in {v} & u,v1 are_adjacent by A1; consider w being Vertex of G such that A3: the_Vertices_of G = {w} by GLIB_000:22; v = w by A3,TARSKI:def 1; hence contradiction by A2,A3; end; hence thesis by Def7; end; theorem Th66: :: Simplicial1 for G1,G2 being _Graph st G1 == G2 for u1 being Vertex of G1, u2 being Vertex of G2 st u1=u2 & u1 is simplicial holds u2 is simplicial proof let G1,G2 be _Graph such that A1: G1 == G2; let u1 be Vertex of G1, u2 be Vertex of G2 such that A2: u1 = u2; assume A3: u1 is simplicial; now per cases; suppose G1.AdjacentSet({u1}) = {}; then G2.AdjacentSet({u2}) = {} by A1,A2,Th51; hence thesis by Def7; end; suppose A4: G1.AdjacentSet({u1}) <> {}; set H1 = the AdjGraph of G1,{u1}; H1 is complete by A3,A4,Def7; then for H2 being AdjGraph of G2,{u2} holds H2 is complete by A1,A2,Th59 ,Th62; hence thesis by Def7; end; end; hence thesis; end; theorem Th67: :: Simplicial2 for G being _Graph for S being non empty Subset of the_Vertices_of G for H being inducedSubgraph of G,S for u being Vertex of G st u in S & G.AdjacentSet({u}) c= S for v being Vertex of H st u=v holds u is simplicial iff v is simplicial proof let G be _Graph; let S be non empty Subset of the_Vertices_of G; let G2 be inducedSubgraph of G,S; let u be Vertex of G such that A1: u in S and A2: G.AdjacentSet({u}) c= S; let v be Vertex of G2 such that A3: u=v; A4: G.AdjacentSet({u}) = {} iff G2.AdjacentSet({v}) = {} by A1,A2,A3,Th58; per cases; suppose G.AdjacentSet({u}) = {}; hence thesis by A4,Def7; end; suppose A5: G.AdjacentSet({u}) <> {}; hereby set Ga = the AdjGraph of G,{u}; assume u is simplicial; then A6: Ga is complete by A5,Def7; thus v is simplicial proof assume G2.AdjacentSet({v}) <> {}; let Ha be AdjGraph of G2,{v}; thus thesis by A1,A2,A3,A5,A6,Th60,Th62; end; end; set Ha = the AdjGraph of G2,{v}; assume A7: v is simplicial; G2.AdjacentSet({v}) <> {} by A1,A2,A3,A5,Th58; then A8: Ha is complete by A7,Def7; thus u is simplicial proof assume G.AdjacentSet({u}) <> {}; let Ga be AdjGraph of G,{u}; Ga == Ha by A1,A2,A3,A5,Th60; hence thesis by A8,Th62; end; end; end; theorem Th68: :: Simplicial03 for G being _Graph, v being Vertex of G st v is simplicial for a ,b being set st a<>b & a in G.AdjacentSet({v}) & b in G.AdjacentSet({v}) holds ex e being set st e Joins a,b,G proof let G be _Graph, x be Vertex of G such that A1: x is simplicial; set H = the AdjGraph of G,{x}; let a,b be set such that A2: a<>b and A3: a in G.AdjacentSet({x}) and A4: b in G.AdjacentSet({x}); A5: H is inducedSubgraph of G,G.AdjacentSet({x}) by Def5; then reconsider u=a as Vertex of H by A3,GLIB_000:def 37; reconsider v=b as Vertex of H by A4,A5,GLIB_000:def 37; H is complete by A1,A3,Def7; then u,v are_adjacent by A2,Def6; then consider e being set such that A6: e Joins u,v,H by Def3; e Joins a,b,G by A6,GLIB_000:72; hence thesis; end; theorem Th69: :: Simplicial03a for G being _Graph, v being Vertex of G st not v is simplicial ex a,b being Vertex of G st a<>b & v<>a & v<>b & v,a are_adjacent & v,b are_adjacent & not a,b are_adjacent proof let G be _Graph, v be Vertex of G such that A1: not v is simplicial; assume A2: not ex a,b being Vertex of G st a<>b & v<>a & v<>b & v,a are_adjacent & v,b are_adjacent & not a,b are_adjacent; per cases; suppose G.AdjacentSet({v}) = {}; hence contradiction by A1,Def7; end; suppose A3: G.AdjacentSet({v}) <> {}; now let H be AdjGraph of G,{v}; A4: H is inducedSubgraph of G,G.AdjacentSet({v}) by Def5; now let a,b be Vertex of H such that A5: a<>b; A6: the_Vertices_of H = G.AdjacentSet({v}) by A3,A4,GLIB_000:def 37; then A7: b in G.AdjacentSet({v}); a in G.AdjacentSet({v}) by A6; then reconsider vv=v,aa=a,bb=b as Vertex of G by A7; A8: aa,vv are_adjacent by A6,Th52; A9: bb,vv are_adjacent by A6,Th52; aa<>vv by A6,Th52; then aa,bb are_adjacent by A2,A5,A8,A9; hence a,b are_adjacent by A3,A4,Th45; end; hence H is complete by Def6; end; hence contradiction by A1,Def7; end; end; begin :: Vertex separator :: Golumbic, p. 84 definition let G be _Graph, a,b be Vertex of G; assume that A1: a<>b and A2: not a,b are_adjacent; mode VertexSeparator of a,b -> Subset of the_Vertices_of G means : Def8: not a in it & not b in it & for G2 being removeVertices of G,it holds not (ex W being Walk of G2 st W is_Walk_from a,b); existence proof set S = the_Vertices_of G\{a,b}; a in {a,b} by TARSKI:def 2; then A3: not a in S by XBOOLE_0:def 5; A4: not ex e being set st e Joins a,b,G by A2,Def3; A5: for G2 being removeVertices of G,S holds not ex W being Walk of G2 st W is_Walk_from a,b proof let G2 be removeVertices of G,S; let W be Walk of G2 such that A6: W is_Walk_from a,b; A7: now let x be set such that A8: x in {a,b}; now per cases by A8,TARSKI:def 2; suppose x = a; then x = W.first() by A6,GLIB_001:def 23; hence x in W.vertices() by GLIB_001:88; end; suppose x = b; then x = W.last() by A6,GLIB_001:def 23; hence x in W.vertices() by GLIB_001:88; end; end; hence x in W.vertices(); end; reconsider W2=W as Walk of G by GLIB_001:167; A9: now let x be set; hereby assume x in W2.vertices(); then ex n being odd Element of NAT st n<=len W & W.n=x by GLIB_001:87 ; hence x in W.vertices() by GLIB_001:87; end; assume x in W.vertices(); then ex n being odd Element of NAT st n<=len W2 & W2.n=x by GLIB_001:87 ; hence x in W2.vertices() by GLIB_001:87; end; the_Vertices_of G\S is non empty by A3,XBOOLE_0:def 5; then the_Vertices_of G2 = the_Vertices_of G\S by GLIB_000:def 37; then the_Vertices_of G2 = the_Vertices_of G /\ {a,b} by XBOOLE_1:48; then the_Vertices_of G2 = {a,b} by XBOOLE_1:28; then for x being set holds x in W.vertices() iff x in {a,b} by A7; then W.vertices() = {a,b} by TARSKI:1; then W2.vertices() = {a,b} by A9,TARSKI:1; hence contradiction by A1,A4,Th22; end; b in {a,b} by TARSKI:def 2; then not b in S by XBOOLE_0:def 5; hence thesis by A3,A5; end; end; theorem Th70: :: VS01 for G being _Graph, a,b being Vertex of G st a<>b & not a,b are_adjacent for S being VertexSeparator of a,b holds S is VertexSeparator of b ,a proof let G be _Graph; let a,b be Vertex of G such that A1: a<>b and A2: not a,b are_adjacent; let S be VertexSeparator of a,b; A3: not b in S by A1,A2,Def8; A4: for G2 being removeVertices of G,S holds not ex W being Walk of G2 st W is_Walk_from b,a proof let G2 be removeVertices of G,S; let W be Walk of G2; assume W is_Walk_from b,a; then W.reverse() is_Walk_from a,b by GLIB_001:23; hence contradiction by A1,A2,Def8; end; not a in S by A1,A2,Def8; hence thesis by A1,A2,A3,A4,Def8; end; :: alternate characterization of Vertex Separator theorem Th71: :: VS02 for G being _Graph, a,b being Vertex of G st a<>b & not a,b are_adjacent for S being Subset of the_Vertices_of G holds S is VertexSeparator of a,b iff (not a in S & not b in S & for W being Walk of G st W is_Walk_from a ,b holds ex x being Vertex of G st x in S & x in W.vertices()) proof let G be _Graph; let a,b be Vertex of G such that A1: a<>b and A2: not a,b are_adjacent; let S be Subset of the_Vertices_of G; hereby assume A3: S is VertexSeparator of a,b; hence not a in S & not b in S by A1,A2,Def8; then A4: the_Vertices_of G \ S is non empty by XBOOLE_0:def 5; let W be Walk of G such that A5: W is_Walk_from a,b; now assume A6: not ex x being Vertex of G st x in S & x in W.vertices(); let G2 be removeVertices of G,S; A7: the_Vertices_of G2 = the_Vertices_of G\S by A4,GLIB_000:def 37; then A8: the_Edges_of G2 = G.edgesBetween(the_Vertices_of G2) by GLIB_000:def 37; A9: W.edges() c= G.edgesBetween(W.vertices()) by GLIB_001:109; now let x be set such that A10: x in W.vertices(); not x in S by A6,A10; hence x in the_Vertices_of G2 by A7,A10,XBOOLE_0:def 5; end; then A11: W.vertices() c= the_Vertices_of G2 by TARSKI:def 3; then G.edgesBetween(W.vertices()) c= G.edgesBetween(the_Vertices_of G2) by GLIB_000:36; then W.edges() c= the_Edges_of G2 by A8,A9,XBOOLE_1:1; then reconsider W2=W as Walk of G2 by A11,GLIB_001:170; W.last() = b by A5,GLIB_001:def 23; then A12: W2.last()=b; W.first() = a by A5,GLIB_001:def 23; then W2.first()=a; then W2 is_Walk_from a,b by A12,GLIB_001:def 23; hence contradiction by A1,A2,A3,Def8; end; hence ex x being Vertex of G st x in S & x in W.vertices(); end; assume that A13: not a in S and A14: not b in S and A15: for W being Walk of G st W is_Walk_from a,b holds ex x being Vertex of G st x in S & x in W.vertices(); now let G2 be removeVertices of G,S; given W be Walk of G2 such that A16: W is_Walk_from a,b; reconsider W2=W as Walk of G by GLIB_001:167; W.last() = b by A16,GLIB_001:def 23; then A17: W2.last()=b; now let x be set; hereby assume x in W2.vertices(); then ex n being odd Element of NAT st n<=len W & W.n=x by GLIB_001:87; hence x in W.vertices() by GLIB_001:87; end; assume x in W.vertices(); then ex n being odd Element of NAT st n<=len W2 & W2.n=x by GLIB_001:87; hence x in W2.vertices() by GLIB_001:87; end; then A18: W2.vertices() = W.vertices() by TARSKI:1; the_Vertices_of G \ S is non empty by A13,XBOOLE_0:def 5; then the_Vertices_of G2 = the_Vertices_of G \ S by GLIB_000:def 37; then A19: for x being Vertex of G holds not (x in S & x in W2.vertices() ) by A18, XBOOLE_0:def 5; W.first() = a by A16,GLIB_001:def 23; then W2.first()=a; then W2 is_Walk_from a,b by A17,GLIB_001:def 23; hence contradiction by A15,A19; end; hence thesis by A1,A2,A13,A14,Def8; end; theorem Th72: :: VS07 for G being _Graph, a,b being Vertex of G st a<>b & not a,b are_adjacent for S being VertexSeparator of a,b for W being Walk of G st W is_Walk_from a,b ex k being odd Nat st 1 < k & k < len W & W.k in S proof let G be _Graph; let a,b be Vertex of G such that A1: a<>b and A2: not a,b are_adjacent; let S be VertexSeparator of a,b; let W be Walk of G such that A3: W is_Walk_from a,b; consider x being Vertex of G such that A4: x in S and A5: x in W.vertices() by A1,A2,A3,Th71; consider n being odd Element of NAT such that A6: n <= len W and A7: W.n = x by A5,GLIB_001:87; A8: not a in S by A1,A2,Th71; A9: now assume 1 = n; then W.n = W.first(); hence contradiction by A3,A8,A4,A7,GLIB_001:def 23; end; A10: not b in S by A1,A2,Th71; now assume n = len W; then W.n = W.last(); hence contradiction by A3,A10,A4,A7,GLIB_001:def 23; end; then A11: n < len W by A6,XXREAL_0:1; 1 <= n by ABIAN:12; then 1 < n by A9,XXREAL_0:1; hence thesis by A4,A7,A11; end; theorem Th73: :: VS08a for G being _Graph, a,b being Vertex of G st a<>b & not a,b are_adjacent for S being VertexSeparator of a,b st S = {} holds not ex W being Walk of G st W is_Walk_from a,b proof let G be _Graph; let a,b be Vertex of G such that A1: a<>b and A2: not a,b are_adjacent; let S be VertexSeparator of a,b; assume A3: S = {}; A4: the_Edges_of G c= G.edgesBetween(the_Vertices_of G) by GLIB_000:34; A5: the_Vertices_of G c= the_Vertices_of G; set G2 = the removeVertices of G,S; given W be Walk of G such that A6: W is_Walk_from a,b; the_Vertices_of G2 = the_Vertices_of G by A3,GLIB_000:def 37; then A7: W.vertices() c= the_Vertices_of G2; G2 is inducedSubgraph of G,the_Vertices_of G,the_Edges_of G by A3,GLIB_000:34 ; then the_Edges_of G2 = the_Edges_of G by A5,A4,GLIB_000:def 37; then W.edges() c= the_Edges_of G2; then reconsider W2=W as Walk of G2 by A7,GLIB_001:170; W.last() = b by A6,GLIB_001:def 23; then A8: W2.last()=b; W.first() = a by A6,GLIB_001:def 23; then W2.first()=a; then W2 is_Walk_from a,b by A8,GLIB_001:def 23; hence contradiction by A1,A2,Def8; end; theorem for G being _Graph, a,b being Vertex of G st a<>b ¬ a,b are_adjacent & not ex W being Walk of G st W is_Walk_from a,b holds {} is VertexSeparator of a,b proof let G be _Graph; let a,b be Vertex of G such that A1: a<>b and A2: not a,b are_adjacent; assume A3: not ex W being Walk of G st W is_Walk_from a,b; A4: now let G2 be removeVertices of G,{}; given W be Walk of G2 such that A5: W is_Walk_from a,b or W is_Walk_from b,a; per cases by A5; suppose A6: W is_Walk_from a,b; reconsider W2=W as Walk of G by GLIB_001:167; W.last() = b by A6,GLIB_001:def 23; then A7: W2.last()=b; W.first() = a by A6,GLIB_001:def 23; then W2.first()=a; then W2 is_Walk_from a,b by A7,GLIB_001:def 23; hence contradiction by A3; end; suppose A8: W is_Walk_from b,a; set P=W.reverse(); reconsider W2=P as Walk of G by GLIB_001:167; A9: P is_Walk_from a,b by A8,GLIB_001:23; then P.last() = b by GLIB_001:def 23; then A10: W2.last()=b; P.first() = a by A9,GLIB_001:def 23; then W2.first()=a; then W2 is_Walk_from a,b by A10,GLIB_001:def 23; hence contradiction by A3; end; end; {} is Subset of the_Vertices_of G by XBOOLE_1:2; hence thesis by A1,A2,A4,Def8; end; theorem Th75: :: VS11 for G being _Graph, a,b being Vertex of G st a<>b & not a,b are_adjacent for S being VertexSeparator of a,b, G2 being removeVertices of G,S for a2 being Vertex of G2 holds G2.reachableFrom(a2) /\ S = {} proof let G be _Graph; let a,b be Vertex of G such that A1: a<>b and A2: not a,b are_adjacent; let S be VertexSeparator of a,b, G2 be removeVertices of G,S; let a2 be Vertex of G2; set A = G2.reachableFrom(a2); not a in S by A1,A2,Def8; then a in the_Vertices_of G \ S by XBOOLE_0:def 5; then A3: the_Vertices_of G2 = the_Vertices_of G \ S by GLIB_000:def 37; now let x be set such that A4: x in A /\ S; A5: x in S by A4,XBOOLE_0:def 4; x in A by A4,XBOOLE_0:def 4; hence contradiction by A3,A5,XBOOLE_0:def 5; end; hence thesis by XBOOLE_0:def 1; end; theorem Th76: for G being _Graph, a,b being Vertex of G st a<>b & not a,b are_adjacent for S being VertexSeparator of a,b, G2 being removeVertices of G,S for a2,b2 being Vertex of G2 st a2=a & b2=b holds G2.reachableFrom(a2) /\ G2 .reachableFrom(b2) = {} proof let G be _Graph; let a,b be Vertex of G such that A1: a<>b and A2: not a,b are_adjacent; let S be VertexSeparator of a,b, G2 be removeVertices of G,S; let a2,b2 be Vertex of G2 such that A3: a2=a and A4: b2=b; set A = G2.reachableFrom(a2), B = G2.reachableFrom(b2); now let x be set such that A5: x in A /\ B; x in A by A5,XBOOLE_0:def 4; then consider W1 being Walk of G2 such that A6: W1 is_Walk_from a2,x by GLIB_002:def 5; x in B by A5,XBOOLE_0:def 4; then consider rW2 being Walk of G2 such that A7: rW2 is_Walk_from b2,x by GLIB_002:def 5; set W2 = rW2.reverse(); set W = W1.append(W2); W2 is_Walk_from x,b2 by A7,GLIB_001:23; then W is_Walk_from a2,b2 by A6,GLIB_001:31; hence contradiction by A1,A2,A3,A4,Def8; end; hence thesis by XBOOLE_0:def 1; end; theorem Th77: :: VS10 for G being _Graph, a,b being Vertex of G st a<>b & not a,b are_adjacent for S being VertexSeparator of a,b for G2 being removeVertices of G,S holds a is Vertex of G2 & b is Vertex of G2 proof let G be _Graph; let a,b be Vertex of G such that A1: a<>b and A2: not a,b are_adjacent; let S be VertexSeparator of a,b, G2 be removeVertices of G,S; not b in S by A1,A2,Def8; then A3: b in the_Vertices_of G\S by XBOOLE_0:def 5; not a in S by A1,A2,Def8; then a in the_Vertices_of G\S by XBOOLE_0:def 5; hence thesis by A3,GLIB_000:def 37; end; definition let G be _Graph, a,b be Vertex of G; let S be VertexSeparator of a,b; attr S is minimal means : Def9: for T being Subset of S st T <> S holds not T is VertexSeparator of a,b; end; theorem :: VS000 for G being _Graph, a,b being Vertex of G for S being VertexSeparator of a,b st S = {} holds S is minimal proof let G be _Graph; let a,b be Vertex of G, S be VertexSeparator of a,b; assume A1: S = {}; now assume not S is minimal; then ex T being Subset of S st T <> S & T is VertexSeparator of a,b by Def9 ; hence contradiction by A1; end; hence thesis; end; theorem Th79: :: minVSexistance for G being finite _Graph for a,b being Vertex of G ex S being VertexSeparator of a,b st S is minimal proof let G be finite _Graph, a,b be Vertex of G; set X = {S where S is VertexSeparator of a,b : not contradiction }; set s = the VertexSeparator of a,b; A1: s in X; now let x be set; assume x in X; then ex y being VertexSeparator of a,b st x = y; hence x in bool the_Vertices_of G; end; then X c= bool the_Vertices_of G by TARSKI:def 3; then reconsider X as non empty finite set by A1; defpred P[set,set] means ex p being VertexSeparator of a,b st $1 = p & $2 = card p; A2: now let x be set; assume x in X; then consider Y being VertexSeparator of a,b such that A3: Y = x; card Y is Element of NAT; hence ex y being set st y in REAL & P[x,y] by A3; end; consider F being Function of X, REAL such that A4: for x being set st x in X holds P[x,F.x] from FUNCT_2:sch 1(A2); deffunc FF(Element of X) = F/.$1; consider Min being Element of X such that A5: for N being Element of X holds FF(Min) <= FF(N) from GRAPH_5:sch 2; consider M being VertexSeparator of a,b such that M = Min and A6: card M = F.Min by A4; A7: dom F = X by FUNCT_2:def 1; now assume not M is minimal; then consider T being Subset of M such that A8: T<>M and A9: T is VertexSeparator of a,b by Def9; T in X by A9; then reconsider T2=T as Element of X; consider Tp being VertexSeparator of a,b such that A10: Tp=T2 and A11: card Tp = F.T2 by A4; Tp in dom F by A7; then F/.Tp = F.Tp by PARTFUN1:def 6; then A12: card M <= card T by A5,A6,A10,A11; card T <= card M by NAT_1:43; hence contradiction by A8,A12,PRE_POLY:8,XXREAL_0:1; end; hence thesis; end; theorem Th80: :: VS13 :: Property "symmetry" for 2 argument modes could be used if we had it :: as VertexSeparator of a,b is a VertexSeparator of b,a :: then this theorem would not be needed for G being _Graph, a,b being Vertex of G st a<>b & not a,b are_adjacent for S being VertexSeparator of a,b st S is minimal for T being VertexSeparator of b,a st S=T holds T is minimal proof let G be _Graph; let a,b be Vertex of G such that A1: a<>b and A2: not a,b are_adjacent; let S be VertexSeparator of a,b such that A3: S is minimal; let T be VertexSeparator of b,a such that A4: S=T; assume not T is minimal; then consider H being Subset of T such that A5: H <> T and A6: H is VertexSeparator of b,a by Def9; H is VertexSeparator of a,b by A1,A2,A6,Th70; hence contradiction by A3,A4,A5,Def9; end; theorem :: VS06 for G being _Graph, a,b being Vertex of G st a<>b & not a,b are_adjacent for S being VertexSeparator of a,b st S is minimal for x being Vertex of G st x in S ex W being Walk of G st W is_Walk_from a,b & x in W .vertices() proof let G be _Graph; let a,b be Vertex of G such that A1: a<>b and A2: not a,b are_adjacent; let S be VertexSeparator of a,b such that A3: S is minimal; let x be Vertex of G such that A4: x in S; set T = S\{x}; A5: T c= S by XBOOLE_1:36; then A6: not b in T by A1,A2,Def8; assume A7: not ex W being Walk of G st W is_Walk_from a,b & x in W.vertices(); A8: now let W be Walk of G such that A9: W is_Walk_from a,b; consider y being Vertex of G such that A10: y in S and A11: y in W.vertices() by A1,A2,A9,Th71; take y; y <> x by A7,A9,A11; then not y in {x} by TARSKI:def 1; hence y in T by A10,XBOOLE_0:def 5; thus y in W.vertices() by A11; end; x in {x} by TARSKI:def 1; then A12: T <> S by A4,XBOOLE_0:def 5; not a in T by A1,A2,A5,Def8; then T is VertexSeparator of a,b by A1,A2,A6,A8,Th71; hence contradiction by A3,A12,A5,Def9; end; theorem Th82: :: VertexSep0 for G being _Graph for a,b being Vertex of G st a<>b & not a,b are_adjacent for S being VertexSeparator of a,b st S is minimal for H being removeVertices of G,S for aa being Vertex of H st aa=a for x being Vertex of G st x in S ex y being Vertex of G st y in H.reachableFrom(aa) & x,y are_adjacent proof let G be _Graph; let a,b be Vertex of G such that A1: a<>b and A2: not a,b are_adjacent; let S be VertexSeparator of a,b such that A3: S is minimal; let H be removeVertices of G,S; let aa be Vertex of H such that A4: aa=a; set A=H.reachableFrom(aa); let x be Vertex of G such that A5: x in S; set T = S\{x}; A6: T c= S by XBOOLE_1:36; then A7: not b in T by A1,A2,Def8; assume A8: not ex y being Vertex of G st y in H.reachableFrom(aa) & x,y are_adjacent; A9: for W being Walk of G st W is_Walk_from a,b & x in W.vertices() ex y being Vertex of G st y in T & y in W.vertices() proof let W be Walk of G such that A10: W is_Walk_from a,b and A11: x in W.vertices(); A12: now assume W.find(x) = 1; then W.(W.find(x)) = W.first(); then W.(W.find(x)) = a by A10,GLIB_001:def 23; then not W.(W.find(x)) in S by A1,A2,Def8; hence contradiction by A5,A11,GLIB_001:def 19; end; consider k being odd Element of NAT such that A13: k <= len W and A14: W.k = x by A11,GLIB_001:87; W.find(W.k) <= k by A13,GLIB_001:115; then A15: W.find(x) <= len W by A13,A14,XXREAL_0:2; then A16: W.find(x)+(-2) <= len W+0 by XREAL_1:7; 0+1 <= W.find(x) by ABIAN:12; then 2*0+1 < W.find(x) by A12,XXREAL_0:1; then 2*1+1 <= W.find(x) by Th4; then A17: 3+(-2) <= W.find(x)+(-2) by XREAL_1:7; then A18: W.find(x)-2 is Element of NAT by INT_1:3; then reconsider j=W.find(x)-2*1 as odd Nat; set P = W.cut(1,j); A19: 2*0+1 <= j by A17; then A20: len P + 1 + (-1) = j + 1 + (-1) by A18,A16,GLIB_001:36; assume A21: not ex y being Vertex of G st y in T & y in W.vertices(); A22: for n being odd Nat st n <= j holds not P.n in S & P.n=W.n proof let n be odd Nat such that A23: n <= j; 1 <= n by ABIAN:12; then 1+(-1) <= n+(-1) by XREAL_1:7; then A24: n-1 is Element of NAT by INT_1:3; then reconsider nu1 = n-1 as Nat; n < j + 1 by A23,NAT_1:13; then n+(-1) < j+1+(-1) by XREAL_1:8; then A25: P.(nu1+1) = W.(1+nu1) by A16,A19,A20,A24,GLIB_001:36; now A26: P.vertices() c= W.vertices() by A18,A16,A19,GLIB_001:94; A27: n in NAT by ORDINAL1:def 12; then P.n in P.vertices() by A20,A23,GLIB_001:87; then A28: not P.n in T by A21,A26; n < j + 1 by A23,NAT_1:13; then A29: n+0 < j + 1 + 1 by XREAL_1:8; A30: S \/ {x} = {x} \/ T by XBOOLE_1:39; {x} c= S by A5,ZFMISC_1:31; then A31: S = {x} \/ T by A30,XBOOLE_1:12; A32: n <= len W by A16,A23,XXREAL_0:2; assume P.n in S; then P.n in {x} by A28,A31,XBOOLE_0:def 3; then n < W.find(W.n) by A25,A29,TARSKI:def 1; hence contradiction by A27,A32,GLIB_001:115; end; hence thesis by A25; end; then for n being odd Nat st n <= j holds not P.n in S; then reconsider HP=P as Walk of H by A20,Th21; W.first() = a by A10,GLIB_001:def 23; then P.(2*0+1) = a by A17,A22; then aa in HP.vertices() by A4,A17,A20,GLIB_001:87; then A33: HP.vertices() c= A by GLIB_002:13; W.find(x) < len W + 1 by A15,NAT_1:13; then A34: W.find(x)+(-2) < len W + 1 + (-2) by XREAL_1:8; P.j is Vertex of G by A20,GLIB_001:7; then reconsider Wj=W.j as Vertex of G by A22; len W +(-1) < len W+0 by XREAL_1:8; then j < len W by A34,XXREAL_0:2; then W.(j+1) Joins Wj,W.(j+2),G by A18,GLIB_001:def 3; then W.(j+1) Joins Wj,x,G by A11,GLIB_001:def 19; then A35: Wj,x are_adjacent by Def3; P.j in HP.vertices() by A20,GLIB_001:87; then W.j in HP.vertices() by A22; hence contradiction by A8,A33,A35; end; A36: now let W be Walk of G such that A37: W is_Walk_from a,b; consider y being Vertex of G such that A38: y in S and A39: y in W.vertices() by A1,A2,A37,Th71; per cases; suppose y = x; hence ex y being Vertex of G st y in T & y in W.vertices() by A9,A37,A39; end; suppose A40: y <> x; take y; not y in {x} by A40,TARSKI:def 1; hence y in T by A38,XBOOLE_0:def 5; thus y in W.vertices() by A39; end; end; x in {x} by TARSKI:def 1; then A41: T <> S by A5,XBOOLE_0:def 5; not a in T by A1,A2,A6,Def8; then T is VertexSeparator of a,b by A1,A2,A7,A36,Th71; hence contradiction by A3,A41,A6,Def9; end; theorem Th83: :: VertexSep01 :: Property "symmetry" for 2 argument modes could be used if we had it :: as VertexSeparator of a,b is a VertexSeparator of b,a for G being _Graph for a,b being Vertex of G st a<>b & not a,b are_adjacent for S being VertexSeparator of a,b st S is minimal for H being removeVertices of G,S for aa being Vertex of H st aa=b for x being Vertex of G st x in S ex y being Vertex of G st y in H.reachableFrom(aa) & x,y are_adjacent proof let G be _Graph, a,b be Vertex of G such that A1: a<>b and A2: not a,b are_adjacent; let S be VertexSeparator of a,b such that A3: S is minimal; reconsider S1 = S as VertexSeparator of b,a by A1,A2,Th70; A4: S1 is minimal by A1,A2,A3,Th80; let H be (removeVertices of G,S), aa be Vertex of H such that A5: aa=b; let x be Vertex of G; assume x in S; hence thesis by A1,A2,A5,A4,Th82; end; begin :: Chordal graphs :: Golumbic, p. 81 :: The notion of a chord. Is it worthwhile having it? :: definition let G be _Graph, W be Walk of G, e be set; :: pred e is_chord_of W means :: ex m, n being odd Nat st m < n & n <= len W & W.m <> W.n & :: e Joins W.m,W.n,G & :: for f being set st f in W.edges() holds not f Joins W.m,W.n,G; :: end; :: More general notion of a chordal Walk. Is such a notion useful? Or :: should we stick with chordal Path? definition let G be _Graph, W be Walk of G; attr W is chordal means :Def10: ex m, n being odd Nat st m+2 < n & n <= len W & W.m <> W.n & (ex e being set st e Joins W.m,W.n,G) & for f being set st f in W.edges() holds not f Joins W.m,W.n,G; end; notation let G be _Graph, W be Walk of G; antonym W is chordless for W is chordal; end; :: The other characterization of chordal is 'more' technical and :: sometimes more convenient to work with. Is this really true? :: I have tried to save as much as possible of what Broderic has already done. :: Need separate theorems for walks and paths! They cannot be put as an iff. theorem Th84: :: ChordalWalk01 for G being _Graph, W being Walk of G st W is chordal ex m,n being odd Nat st m+2 < n & n <= len W & W.m <> W.n & (ex e being set st e Joins W.m,W.n,G) & (W is Cycle-like implies not (m=1 & n = len W) & not (m =1 & n = len W-2) & not (m=3 & n = len W)) proof let G be _Graph, W be Walk of G; given m, n being odd Nat such that A1: m+2 < n and A2: n <= len W and A3: W.m <> W.n and A4: ex e being set st e Joins W.m,W.n,G and A5: for f being set st f in W.edges() holds not f Joins W.m,W.n,G; take m, n; thus m+2 < n by A1; thus n <= len W by A2; thus W.m <> W.n by A3; thus ex e being set st e Joins W.m,W.n,G by A4; A6: W.last() = W.len W; assume A7: W is Cycle-like; then A8: 3 <= len W by GLIB_001:125; then reconsider lW2 = len W -2*1 as odd Element of NAT by INT_1:5,XXREAL_0:2 ; A9: W.first() = W.1; then A10: W.1 = W.len W by A7,A6,GLIB_001:def 24; reconsider lW2 as odd Nat; reconsider le = lW2+1 as even Nat; A11: 1 <= le by NAT_1:12; A12: lW2 < len W by XREAL_1:44; then A13: le <= len W by NAT_1:13; then le div 2 in dom W.edgeSeq() by A11,GLIB_001:77; then W.edgeSeq().(le div 2) in rng W.edgeSeq() by FUNCT_1:3; then A14: W.(len W -2+1) in W.edges() by A11,A13,GLIB_001:77; thus not (m=1 & n = len W) by A3,A7,A9,A6,GLIB_001:def 24; W.(lW2+1) Joins W.(lW2),W.(lW2+2),G by A12,GLIB_001:def 3; hence not (m=1 & n = len W-2) by A5,A10,A14,GLIB_000:14; A15: 2*0+1 is odd Nat; A16: 2*1 div 2 = 1 by NAT_D:18; A17: 1+1 <= len W by A8,XXREAL_0:2; then 1 in dom W.edgeSeq() by A16,GLIB_001:77; then W.edgeSeq().1 in rng W.edgeSeq() by FUNCT_1:3; then A18: W.(1+1) in rng W.edgeSeq() by A16,A17,GLIB_001:77; 1 < len W by A8,XXREAL_0:2; then W.(1+1) Joins W.1,W.(1+2),G by A15,GLIB_001:def 3; hence thesis by A5,A10,A18,GLIB_000:14; end; theorem Th85: :: ChordalPath01 for G being _Graph, P being Path of G st ex m,n being odd Nat st m+2 < n & n <= len P & (ex e being set st e Joins P.m,P.n,G) & (P is Cycle-like implies not (m=1 & n = len P) & not (m=1 & n = len P-2) & not (m=3 & n = len P)) holds P is chordal proof let G be _Graph, P be Path of G; given m, n being odd Nat such that A1: m+2 < n and A2: n <= len P and A3: ex e being set st e Joins P.m,P.n,G and A4: P is Cycle-like implies not (m=1 & n = len P) & not (m=1 & n = len P -2) & not (m=3 & n = len P); A5: n in NAT by ORDINAL1:def 12; take m,n; thus m+2 < n by A1; thus n <= len P by A2; A6: m in NAT by ORDINAL1:def 12; A7: m < n by A1,NAT_1:12; then A8: m < len P by A2,XXREAL_0:2; now assume len P = 1; then m+2 < 1 by A1,A2,XXREAL_0:2; hence contradiction by NAT_1:12; end; then A9: P is non trivial by GLIB_001:126; hereby A10: P.last() = P.len P; A11: P.first() = P.1; assume A12: P.m = P.n; then A13: n = len P by A2,A6,A5,A7,GLIB_001:def 28; m = 1 by A2,A6,A5,A7,A12,GLIB_001:def 28; then P is closed by A12,A13,A11,A10,GLIB_001:def 24; hence contradiction by A2,A4,A6,A5,A7,A9,A12,GLIB_001:def 28,def 31; end; thus ex e being set st e Joins P.m,P.n,G by A3; let f be set such that A14: f in P.edges() and A15: f Joins P.m,P.n,G; consider i being Nat such that A16: i in dom P.edgeSeq() and A17: P.edgeSeq().i = f by A14,FINSEQ_2:10; reconsider i as Element of NAT by ORDINAL1:def 12; set k = 2*i-1; A18: 1 <= i by A16,FINSEQ_3:25; then 2*1 <= 2*i by XREAL_1:64; then 2-1 <= k by XREAL_1:9; then A19: k is Element of NAT by INT_1:3; i <= len P.edgeSeq() by A16,FINSEQ_3:25; then A20: P.edgeSeq().i = P.(2*i) by A18,GLIB_001:def 15; reconsider k as odd Nat by A19; 2*i in dom P by A16,GLIB_001:78; then A21: 2*i <= len P by FINSEQ_3:25; k+1 = 2*i; then A22: k < len P by A21,NAT_1:13; then A23: k+2 <= len P by Th4; A24: k in NAT by ORDINAL1:def 12; then A25: P.(k+1) Joins P.k,P.(k+2),G by A22,GLIB_001:def 3; per cases by A15,A17,A20,A25,GLIB_000:15; suppose A26: P.k = P.m & P.(k+2) = P.n; per cases by XXREAL_0:1; suppose k < m; hence contradiction by A6,A8,A24,A26,GLIB_001:def 28; end; suppose A27: k = m; per cases by XXREAL_0:1; suppose A28: k+2 < n; A29: 1 <= k by ABIAN:12; k+2 = 1 by A2,A5,A26,A28,GLIB_001:def 28; then k+2 < k+1 by A29,NAT_1:13; hence contradiction by XREAL_1:6; end; suppose k+2 = n; hence contradiction by A1,A27; end; suppose A30: k+2 > n; k+2 <= len P by A22,Th4; then n = 1 by A5,A26,A30,GLIB_001:def 28; hence contradiction by A1,ABIAN:12; end; end; suppose k > m; hence contradiction by A6,A24,A22,A26,GLIB_001:def 28; end; end; suppose A31: P.k = P.n & P.(k+2) = P.m; per cases by XXREAL_0:1; suppose A32: k < n; then A33: n = len P by A2,A5,A24,A31,GLIB_001:def 28; A34: k = 1 by A2,A5,A24,A31,A32,GLIB_001:def 28; per cases by XXREAL_0:1; suppose k+2 < m; hence contradiction by A6,A8,A31,GLIB_001:def 28; end; suppose A35: k+2 = m; A36: P.last() = P.len P; P.first() = P.1; then P is closed by A31,A34,A33,A36,GLIB_001:def 24; hence contradiction by A2,A4,A5,A9,A31,A32,A34,A35,GLIB_001:def 28 ,def 31; end; suppose A37: k+2 > m; A38: P.last() = P.len P; A39: k+2 <= n by A32,Th4; A40: P.first() = P.1; A41: k+2 = len P by A6,A23,A31,A37,GLIB_001:def 28; m = 1 by A6,A23,A31,A37,GLIB_001:def 28; then P is closed by A31,A41,A40,A38,GLIB_001:def 24; hence contradiction by A2,A4,A6,A9,A31,A37,A41,A39,GLIB_001:def 28 ,def 31,XXREAL_0:1; end; end; suppose A42: k = n; per cases by XXREAL_0:1; suppose k+2 < m; hence contradiction by A7,A42,NAT_1:12; end; suppose k+2 = m; hence contradiction by A7,A42,NAT_1:12; end; suppose A43: k+2 > m; A44: P.last() = P.len P; A45: P.first() = P.1; A46: k+2 = len P by A6,A23,A31,A43,GLIB_001:def 28; m = 1 by A6,A23,A31,A43,GLIB_001:def 28; then P is closed by A31,A46,A45,A44,GLIB_001:def 24; hence contradiction by A4,A6,A9,A31,A42,A43,A46,GLIB_001:def 28,def 31; end; end; suppose k > n; hence contradiction by A5,A24,A22,A31,GLIB_001:def 28; end; end; end; theorem Th86: :: ChordalWalk02 for G1,G2 being _Graph st G1 == G2 for W1 being Walk of G1, W2 being Walk of G2 st W1=W2 holds W1 is chordal implies W2 is chordal proof let G1,G2 be _Graph such that A1: G1 == G2; let W1 be Walk of G1, W2 be Walk of G2 such that A2: W1 = W2; given m, n being odd Nat such that A3: m+2 < n and A4: n <= len W1 and A5: W1.m <> W1.n and A6: ex e being set st e Joins W1.m,W1.n,G1 and A7: for f being set st f in W1.edges() holds not f Joins W1.m,W1.n,G1; take m,n; thus m+2 < n & n <= len W2 & W2.m <> W2.n by A2,A3,A4,A5; consider e being set such that A8: e Joins W1.m,W1.n,G1 by A6; e Joins W2.m,W2.n,G2 by A1,A2,A8,GLIB_000:88; hence ex e being set st e Joins W2.m,W2.n,G2; let f be set; assume f in W2.edges(); then f in W1.edges() by A2,GLIB_001:110; then not f Joins W1.m,W1.n,G1 by A7; hence thesis by A1,A2,GLIB_000:88; end; theorem Th87: :: ChordalWalk03 for G being _Graph, S being non empty Subset of the_Vertices_of G, H being (inducedSubgraph of G,S), W1 being Walk of G, W2 being Walk of H st W1 = W2 holds W2 is chordal iff W1 is chordal proof let G be _Graph, S be non empty Subset of the_Vertices_of G, H be ( inducedSubgraph of G,S), W1 be Walk of G, W2 be Walk of H such that A1: W1 = W2; thus W2 is chordal implies W1 is chordal proof given m, n being odd Nat such that A2: m+2 < n and A3: n <= len W2 and A4: W2.m <> W2.n and A5: ex e being set st e Joins W2.m,W2.n,H and A6: for f being set st f in W2.edges() holds not f Joins W2.m,W2.n,H; take m,n; thus m+2 < n & n <= len W1 & W1.m <> W1.n by A1,A2,A3,A4; consider e being set such that A7: e Joins W2.m,W2.n,H by A5; e Joins W1.m,W1.n,G by A1,A7,GLIB_000:72; hence ex e being set st e Joins W1.m,W1.n,G; let f be set; assume f in W1.edges(); then A8: f in W2.edges() by A1,GLIB_001:110; then not f Joins W1.m,W1.n,H by A1,A6; hence thesis by A8,GLIB_000:73; end; A9: S = the_Vertices_of H by GLIB_000:def 37; thus W1 is chordal implies W2 is chordal proof given m, n being odd Nat such that A10: m+2 < n and A11: n <= len W1 and A12: W1.m <> W1.n and A13: ex e being set st e Joins W1.m,W1.n,G and A14: for f being set st f in W1.edges() holds not f Joins W1.m,W1.n,G; take m,n; thus m+2 < n & n <= len W2 & W2.m <> W2.n by A1,A10,A11,A12; A15: m in NAT by ORDINAL1:def 12; n in NAT by ORDINAL1:def 12; then A16: W1.n in the_Vertices_of H by A1,A11,GLIB_001:7; m < n by A10,NAT_1:12; then W1.m in the_Vertices_of H by A1,A11,A15,GLIB_001:7,XXREAL_0:2; hence ex e being set st e Joins W2.m,W2.n,H by A1,A9,A13,A16,Th19; let f be set; assume f in W2.edges(); then f in W1.edges() by A1,GLIB_001:110; then not f Joins W2.m,W2.n,G by A1,A14; hence thesis by GLIB_000:72; end; end; theorem for G being _Graph, W being Walk of G st W is Cycle-like & W is chordal & W.length()=4 holds ex e being set st e Joins W.1,W.5,G or e Joins W.3 ,W.7,G proof let G be _Graph, W be Walk of G such that A1: W is Cycle-like and A2: W is chordal and A3: W.length() = 4; A4: len W = 2*4+1 by A3,GLIB_001:112; consider m, n being odd Nat such that A5: m+2 < n and A6: n <= len W and W.m <> W.n and A7: ex e being set st e Joins W.m,W.n,G and A8: W is Cycle-like implies not (m=1 & n = len W) & not (m=1 & n = len W-2) & not (m=3 & n = len W) by A2,Th84; consider e being set such that A9: e Joins W.m,W.n,G by A7; assume A10: not(ex e being set st e Joins W.1,W.5,G or e Joins W.3,W.7,G); A11: now assume A12: m = 3; then n < len W by A1,A6,A8,XXREAL_0:1; then A13: n <= 9 - 2 by A4,Th3; n <> 7 by A10,A9,A12; then n < 2*3+1 by A13,XXREAL_0:1; then n <= 7 - 2 by Th3; hence contradiction by A5,A12; end; A14: now reconsider jj=2*3+1 as odd Nat; assume A15: m = 1; then n < len W by A1,A6,A8,XXREAL_0:1; then n <= 9 - 2 by A4,Th3; then n < jj by A1,A4,A8,A15,XXREAL_0:1; then A16: n <= jj-2 by Th3; n <> 5 by A10,A9,A15; then n < 2*2+1 by A16,XXREAL_0:1; then n <= 5-2 by Th3; hence contradiction by A5,A15; end; A17: W.first() = W.last() by A1,GLIB_001:def 24; A18: now assume A19: m = 5; now assume n = 9; then e Joins W.1,W.5,G by A17,A4,A9,A19,GLIB_000:14; hence contradiction by A10; end; then n < len W by A4,A6,XXREAL_0:1; then n <= len W - 2 by Th3; hence contradiction by A4,A5,A19; end; 0+1 <= m by ABIAN:12; then 2*0+1 < m by A14,XXREAL_0:1; then 1+2 <= m by Th4; then 2*1+1 < m by A11,XXREAL_0:1; then 3+2 <= m by Th4; then 2*2+1 < m by A18,XXREAL_0:1; then 5+2 <= m by Th4; then 7+2 <= m + 2 by XREAL_1:7; hence contradiction by A4,A5,A6,XXREAL_0:2; end; theorem Th89: :: MinChordal01 for G being _Graph, W being Walk of G st W is minlength holds W is chordless proof let G be _Graph, W be Walk of G; assume A1: W is minlength; assume W is chordal; then ex m,n being odd Nat st m+2 < n & n <= len W & W.m <> W .n &( ex e being set st e Joins W.m,W.n,G)&( W is Cycle-like implies not (m=1 & n = len W) & not (m=1 & n = len W-2) & not (m=3 & n = len W)) by Th84; hence contradiction by A1,Th40; end; theorem for G being _Graph, W being Walk of G st len W = 5 & not W.first(),W .last() are_adjacent holds W is chordless proof let G be _Graph, W be Walk of G such that A1: len W = 5 and A2: not W.first(),W.last() are_adjacent; assume W is chordal; then consider m,n being odd Nat such that A3: m+2 < n and A4: n <= len W and W.m <> W.n and A5: ex e being set st e Joins W.m,W.n,G and W is Cycle-like implies not (m=1 & n = len W) & not (m=1 & n = len W-2) & not (m=3 & n = len W) by Th84; A6: now assume A7: m <> 1; 1 <= m by Th2; then 2*0+1 < m by A7,XXREAL_0:1; then 1+2 <= m by Th4; then 3+2 <= m+2 by XREAL_1:7; hence contradiction by A1,A3,A4,XXREAL_0:2; end; then 3+2 <= n by A3,Th4; then W.n = W.last() by A1,A4,XXREAL_0:1; hence contradiction by A2,A5,A6,Def3; end; Lm3: for G being _Graph, W being Walk of G holds W is chordal implies W .reverse() is chordal proof let G be _Graph, W be Walk of G; set U = W.reverse(); assume W is chordal; then consider m, n being odd Nat such that A1: m+2 < n and A2: n <= len W and A3: W.m <> W.n and A4: ex e being set st e Joins W.m,W.n,G and A5: for f being set st f in W.edges() holds not f Joins W.m,W.n,G by Def10; consider e being set such that A6: e Joins W.m,W.n,G by A4; set um = len W - m + 1, un = len W - n + 1; m < m+2 by XREAL_1:29; then A7: m < n by A1,XXREAL_0:2; then reconsider um, un as odd Element of NAT by A2,FINSEQ_5:1,XXREAL_0:2; reconsider um, un as odd Nat; A8: un + 2 < um by A1,Lm1; 1 <= n by Th2; then n in dom W by A2,FINSEQ_3:25; then A9: W.n = U.un by GLIB_001:24; A10: 1 <= m by Th2; len W - m + 1 <= len W by INT_1:7,XREAL_1:44; then A11: um <= len U by GLIB_001:21; m <= len W by A2,A7,XXREAL_0:2; then m in dom W by A10,FINSEQ_3:25; then A12: W.m = U.um by GLIB_001:24; then A13: e Joins U.un,U.um,G by A6,A9,GLIB_000:14; W.edges() = U.edges() by GLIB_001:107; then for f being set st f in U.edges() holds not f Joins U.un,U.um,G by A5 ,A12,A9,GLIB_000:14; hence thesis by A3,A8,A11,A12,A9,A13,Def10; end; theorem for G being _Graph, W being Walk of G holds W is chordal iff W .reverse() is chordal proof let G be _Graph, W be Walk of G; thus W is chordal implies W.reverse() is chordal by Lm3; assume W.reverse() is chordal; then W.reverse().reverse() is chordal by Lm3; hence thesis; end; theorem Th92: :: CPath03 for G being _Graph, P being Path of G st P is open & P is chordless for m,n being odd Nat st m < n & n <= len P holds (ex e being set st e Joins P.m,P.n,G) iff m+2 = n proof let G be _Graph, P be Path of G such that A1: P is open and A2: P is chordless; A3: P is vertex-distinct by A1,Th32; let m,n be odd Nat such that A4: m < n and A5: n <= len P; A6: m <= len P by A4,A5,XXREAL_0:2; A7: m in NAT by ORDINAL1:def 12; A8: n in NAT by ORDINAL1:def 12; then A9: P.m <> P.n by A1,A4,A5,A7,GLIB_001:147; hereby assume A10: ex e being set st e Joins P.m,P.n,G; A11: now assume A12: m+2 < n; now let f be set; assume f in P.edges(); then consider k being odd Element of NAT such that A13: k < len P and A14: P.(k+1) = f by GLIB_001:100; A15: f Joins P.k,P.(k+2),G by A13,A14,GLIB_001:def 3; A16: k+2 <= len P by A13,Th4; assume A17: f Joins P.m,P.n,G; per cases by A15,A17,GLIB_000:15; suppose A18: P.m = P.k & P.n = P.(k+2); then m = k by A7,A3,A6,A13,GLIB_001:def 29; hence contradiction by A5,A8,A3,A12,A16,A18,GLIB_001:def 29; end; suppose A19: P.m = P.(k+2) & P.n = P.k; then A20: n = k by A5,A8,A3,A13,GLIB_001:def 29; m = k+2*1 by A7,A3,A6,A16,A19,GLIB_001:def 29; then A21: m > n by A20,XREAL_1:29; m+2 > m by XREAL_1:29; hence contradiction by A12,A21,XXREAL_0:2; end; end; hence contradiction by A2,A5,A9,A10,A12,Def10; end; m+2 <= n by A4,Th4; hence m+2 = n by A11,XXREAL_0:1; end; assume A22: m+2 = n; take P.(m+1); m < len P by A4,A5,XXREAL_0:2; hence thesis by A7,A22,GLIB_001:def 3; end; theorem for G being _Graph, P being Path of G st P is open & P is chordless for m,n being odd Nat st m < n & n <= len P holds P.cut(m,n) is chordless & P.cut(m,n) is open proof let G be _Graph, P be Path of G such that A1: P is open and A2: P is chordless; let m,n be odd Nat such that A3: m < n and A4: n <= len P; set Q = P.cut(m,n); A5: n in NAT by ORDINAL1:def 12; A6: m in NAT by ORDINAL1:def 12; now assume Q is chordal; then consider i,j being odd Nat such that A7: i+2 < j and A8: j <= len Q and Q.i <> Q.j and A9: ex e being set st e Joins Q.i,Q.j,G and for f being set st f in Q.edges() holds not f Joins Q.i,Q.j,G by Def10; consider e being set such that A10: e Joins Q.i,Q.j,G by A9; set mi = m+i-1; set mj = m+j-1; 1 <= j by Th2; then A11: j in dom Q by A8,FINSEQ_3:25; then A12: Q.j = P.mj by A3,A4,A6,A5,GLIB_001:47; A13: mj in dom P by A3,A4,A6,A5,A11,GLIB_001:47; i+0 V.n and A6: ex e being set st e Joins V.m,V.n,H and A7: for f being set st f in V.edges() holds not f Joins V.m,V.n,H by Def10; consider e being set such that A8: e Joins V.m,V.n,H by A6; n in NAT by ORDINAL1:def 12; then V.n in V.vertices() by A4,GLIB_001:87; then V.n in the_Vertices_of H; then A9: V.n in S by GLIB_000:def 37; m+0 <= m+2 by XREAL_1:7; then m <= n by A3,XXREAL_0:2; then A10: m <= len V by A4,XXREAL_0:2; m in NAT by ORDINAL1:def 12; then V.m in V.vertices() by A10,GLIB_001:87; then V.m in the_Vertices_of H; then A11: V.m in S by GLIB_000:def 37; A12: for f being set st f in W.edges() holds not f Joins W.m,W.n,G proof let f be set; assume f in W.edges(); then A13: f in V.edges() by A1,GLIB_001:110; assume f Joins W.m,W.n,G; hence contradiction by A1,A7,A9,A11,A13,Th19; end; e Joins W.m,W.n,G by A1,A8,GLIB_000:72; hence contradiction by A1,A2,A3,A4,A5,A12,Def10; end; assume A14: V is chordless; assume W is chordal; then consider m,n being odd Nat such that A15: m+2 < n and A16: n <= len W and A17: W.m <> W.n and A18: ex e being set st e Joins W.m,W.n,G and A19: for f being set st f in W.edges() holds not f Joins W.m,W.n,G by Def10; consider e being set such that A20: e Joins W.m,W.n,G by A18; A21: for f being set st f in V.edges() holds not f Joins V.m,V.n,H proof let f be set; assume f in V.edges(); then A22: f in W.edges() by A1,GLIB_001:110; assume f Joins V.m,V.n,H; then f Joins W.m,W.n,G by A1,GLIB_000:72; hence contradiction by A19,A22; end; n in NAT by ORDINAL1:def 12; then W.n in V.vertices() by A1,A16,GLIB_001:87; then W.n in the_Vertices_of H; then A23: W.n in S by GLIB_000:def 37; m+0 <= m+2 by XREAL_1:7; then m <= n by A15,XXREAL_0:2; then A24: m <= len W by A16,XXREAL_0:2; m in NAT by ORDINAL1:def 12; then W.m in V.vertices() by A1,A24,GLIB_001:87; then W.m in the_Vertices_of H; then W.m in S by GLIB_000:def 37; then e Joins V.m,V.n,H by A1,A20,A23,Th19; hence contradiction by A1,A14,A15,A16,A17,A21,Def10; end; definition let G be _Graph; attr G is chordal means :Def11: for P being Walk of G st P.length() > 3 & P is Cycle-like holds P is chordal; end; theorem Th95: :: Chordal01 for G1,G2 being _Graph st G1 == G2 holds G1 is chordal implies G2 is chordal proof let G1,G2 be _Graph such that A1: G1 == G2; assume A2: G1 is chordal; now let W be Walk of G2 such that A3: W.length() > 3 and A4: W is Cycle-like; reconsider W2=W as Walk of G1 by A1,GLIB_001:179; 2*W2.length() + 1 = len W by GLIB_001:112; then A5: 2*W2.length() + 1 = 2*W.length() + 1 by GLIB_001:112; W2 is Cycle-like by A1,A4,Th24; then W2 is chordal by A2,A3,A5,Def11; hence W is chordal by A1,Th86; end; hence thesis by Def11; end; theorem Th96: :: Chordal02 for G being finite _Graph st card the_Vertices_of G <= 3 holds G is chordal proof let G be finite _Graph such that A1: card the_Vertices_of G <= 3; now reconsider n4=2*3+1 as odd Nat; reconsider n3=2*2+1 as odd Nat; reconsider n2=2*1+1 as odd Nat; reconsider n1=2*0+1 as odd Nat; let W be Walk of G such that A2: W.length() > 3 and A3: W is Cycle-like; set x3=W.n3; set x2=W.n2; set x4=W.n4; set x1=W.n1; W.length() >= 3+1 by A2,NAT_1:13; then 2*W.length() >= 2*4 by XREAL_1:64; then 2*W.length() + 1 >= 8 + 1 by XREAL_1:7; then A4: len W >= 9 by GLIB_001:112; then A5: n4 < len W by XXREAL_0:2; then A6: x1 <> x4 by A3,GLIB_001:def 28; n2 < len W by A4,XXREAL_0:2; then A7: x1 <> x2 by A3,GLIB_001:def 28; A8: n3 < len W by A4,XXREAL_0:2; then A9: x2 <> x3 by A3,GLIB_001:def 28; A10: x3 <> x4 by A3,A5,GLIB_001:def 28; A11: x2 <> x4 by A3,A5,GLIB_001:def 28; now let x be set; assume A12: x in {x1,x2,x3,x4}; now per cases by A12,ENUMSET1:def 2; suppose x=x1; hence x in the_Vertices_of G by A4,GLIB_001:7,XXREAL_0:2; end; suppose x=x2; hence x in the_Vertices_of G by A4,GLIB_001:7,XXREAL_0:2; end; suppose x=x3; hence x in the_Vertices_of G by A4,GLIB_001:7,XXREAL_0:2; end; suppose x=x4; hence x in the_Vertices_of G by A4,GLIB_001:7,XXREAL_0:2; end; end; hence x in the_Vertices_of G; end; then A13: {x1,x2,x3,x4} c= the_Vertices_of G by TARSKI:def 3; x1 <> x3 by A3,A8,GLIB_001:def 28; then card {x1,x2,x3,x4} = 4 by A7,A6,A9,A11,A10,CARD_2:59; then 4 <= card the_Vertices_of G by A13,NAT_1:43; hence contradiction by A1,XXREAL_0:2; end; then for W being Walk of G st W.length() > 3 & W is Cycle-like holds W is chordal; hence thesis by Def11; end; registration cluster trivial finite chordal for _Graph; existence proof set G = the trivial finite _Graph; consider v being Vertex of G such that A1: the_Vertices_of G = {v} by GLIB_000:22; now reconsider j5=2*2+1 as odd Nat; reconsider j3=2*1+1 as odd Nat; let W be Walk of G such that A2: W.length() > 3 and A3: W is Cycle-like; 2*W.length() > 2*3 by A2,XREAL_1:68; then 2*W.length() + 1 > 6 + 1 by XREAL_1:8; then A4: len W > 7 by GLIB_001:112; then j3 <= len W by XXREAL_0:2; then W.j3 in W.vertices() by GLIB_001:87; then A5: W.j3 = v by A1,TARSKI:def 1; A6: j5 <= len W by A4,XXREAL_0:2; then W.j5 in W.vertices() by GLIB_001:87; then W.j5 = v by A1,TARSKI:def 1; hence contradiction by A3,A6,A5,GLIB_001:def 28; end; then for W being Walk of G st W.length() > 3 & W is Cycle-like holds W is chordal; then G is chordal by Def11; hence thesis; end; cluster non trivial finite simple chordal for _Graph; existence proof set V = {0,1}, E = {0}, S = 0 .--> 0, T = 0 .--> 1; A7: dom T = E by FUNCOP_1:13; A8: now let x be set; assume x in E; then x = 0 by TARSKI:def 1; then T.x = 1 by FUNCOP_1:72; hence T.x in V by TARSKI:def 2; end; A9: now let x be set; assume x in E; then x = 0 by TARSKI:def 1; then S.x = 0 by FUNCOP_1:72; hence S.x in V by TARSKI:def 2; end; reconsider T as Function of E,V by A7,A8,FUNCT_2:3; dom S = E by FUNCOP_1:13; then reconsider S as Function of E,V by A9,FUNCT_2:3; set G = createGraph(V,E,S,T); take G; the_Source_of G = S by GLIB_000:6; then A10: (the_Source_of G).0 = 0 by FUNCOP_1:72; A11: the_Vertices_of G = V by GLIB_000:6; now assume card (the_Vertices_of G) = 1; then ex x being set st the_Vertices_of G = {x} by CARD_2:42; hence contradiction by A11,ZFMISC_1:5; end; hence G is non trivial & G is finite by GLIB_000:def 19; the_Target_of G = T by GLIB_000:6; then A12: (the_Target_of G).0 = 1 by FUNCOP_1:72; A13: the_Edges_of G = E by GLIB_000:6; then 0 in the_Edges_of G by TARSKI:def 1; then A14: 0 Joins 0,1,G by A10,A12,GLIB_000:def 13; now let v be set; let e being set such that A15: e Joins v,v,G; reconsider v as Vertex of G by A15,GLIB_000:13; e in the_Edges_of G by A15,GLIB_000:def 13; then e Joins 0,1,G by A13,A14,TARSKI:def 1; then 0 = v & 1 = v or 0 = v & 1 = v by A15,GLIB_000:15; hence contradiction; end; then A16: G is loopless by GLIB_000:18; now let e1,e2,v1,v2 be set such that A17: e1 Joins v1,v2,G and A18: e2 Joins v1,v2,G; e1 in {0} by A13,A17,GLIB_000:def 13; then A19: e1 = 0 by TARSKI:def 1; assume A20: e1 <> e2; e2 in {0} by A13,A18,GLIB_000:def 13; hence contradiction by A20,A19,TARSKI:def 1; end; then G is non-multi by GLIB_000:def 20; hence G is simple by A16; card the_Vertices_of G = 2 by A11,CARD_2:57; hence thesis by Th96; end; cluster complete -> chordal for _Graph; correctness proof let G be _Graph; assume A21: G is complete; now reconsider t7=2*3+1 as odd Nat; reconsider t3=2*1+1 as odd Nat; let W be Walk of G such that A22: W.length() > 3 and A23: W is Cycle-like; W.length() >= 3+1 by A22,NAT_1:13; then 2*W.length() >= 2*4 by XREAL_1:64; then 2*W.length() + 1 >= 8 + 1 by XREAL_1:7; then A24: len W >= 9 by GLIB_001:112; then reconsider W3=W.t3 as Vertex of G by GLIB_001:7,XXREAL_0:2; A25: not (t3=3 & t7 = len W) by A24; reconsider W7=W.t7 as Vertex of G by A24,GLIB_001:7,XXREAL_0:2; t7 <= len W by A24,XXREAL_0:2; then W3 <> W7 by A23,GLIB_001:def 28; then W3,W7 are_adjacent by A21,Def6; then A26: ex e being set st e Joins W3,W7,G by Def3; A27: t3+2 < t7; t7 <= len W by A24,XXREAL_0:2; hence W is chordal by A23,A26,A27,A25,Th85; end; hence thesis by Def11; end; end; registration let G be chordal _Graph, V be set; cluster -> chordal for inducedSubgraph of G,V; coherence proof let H be inducedSubgraph of G,V; now per cases; suppose not V is non empty Subset of the_Vertices_of G; then H == G by GLIB_000:def 37; hence thesis by Th95; end; suppose V is non empty Subset of the_Vertices_of G; then A1: V = the_Vertices_of H by GLIB_000:def 37; now let W be Walk of H such that A2: W.length() > 3 and A3: W is Cycle-like; reconsider P=W as Walk of G by GLIB_001:167; reconsider P as Path of G by A3,GLIB_001:175; A4: P is non trivial by A3,GLIB_001:176; A5: P.length() > 3 by A2,GLIB_001:114; A6: P is closed by A3,GLIB_001:176; then P is Cycle-like by A4,GLIB_001:def 31; then P is chordal by A5,Def11; then consider m, n being odd Nat such that A7: m+2 < n and A8: n <= len P and P.m <> P.n and A9: ex e being set st e Joins P.m,P.n,G and A10: P is Cycle-like implies not (m=1 & n = len P) & not (m=1 & n = len P-2) & not (m=3 & n = len P) by Th84; consider e being set such that A11: e Joins P.m,P.n,G by A9; m + 0 <= m + 2 by XREAL_1:7; then A12: m <= n by A7,XXREAL_0:2; n in NAT by ORDINAL1:def 12; then A13: P.n in the_Vertices_of H by A8,GLIB_001:7; m in NAT by ORDINAL1:def 12; then P.m in the_Vertices_of H by A8,A12,GLIB_001:7,XXREAL_0:2; then e Joins P.m,W.n,H by A1,A11,A13,Th19; hence W is chordal by A3,A6,A4,A7,A8,A10,Th85,GLIB_001:def 31; end; hence thesis by Def11; end; end; hence thesis; end; end; theorem for G being chordal _Graph, P being Path of G st P is open & P is chordless for x,e being set st (not x in P.vertices() & e Joins P.last(),x,G & not ex f being set st f Joins P.(len P-2),x,G) holds P.addEdge(e) is Path-like & P.addEdge(e) is open & P.addEdge(e) is chordless proof let G be chordal _Graph, P be Path of G such that A1: P is open and A2: P is chordless; let x,e be set such that A3: not x in P.vertices() and A4: e Joins P.last(),x,G and A5: not ex f being set st f Joins P.(len P-2),x,G; reconsider Q = P.addEdge(e) as Path of G by A1,A3,A4,GLIB_001:151; A6: len Q = len P + 2 by A4,GLIB_001:64; defpred P[Nat] means (4 <= 2*$1 & 2*$1 <= len P+1) implies for j being odd Nat st j + 2*$1 = len P + 2 holds not ex e being set st e Joins Q.j,x,G; A7: now let n be odd Nat such that A8: n <= len P; 1 <= n by Th2; then n in dom P by A8,FINSEQ_3:25; hence P.n = Q.n by A4,GLIB_001:65; end; A9: Q.last() = x by A4,GLIB_001:63; for k being Nat st for a being Nat st a < k holds P[a] holds P[k] proof let k be Nat such that A10: for a being Nat st a < k holds P[a]; assume that A11: 4 <= 2*k and 2*k <= len P+1; let j be odd Nat such that A12: j + 2*k = len P + 2; j + 4 <= j + 2*k by A11,XREAL_1:7; then A13: j + 4 - 4 <= len P + 2 - 4 by A12,XREAL_1:9; A14: len P - 2 <= len P by XREAL_1:43; then A15: j <= len P by A13,XXREAL_0:2; A16: j in NAT by ORDINAL1:def 12; let e be set such that A17: e Joins Q.j,x,G; per cases by A13,XXREAL_0:1; suppose j = len P - 2; then Q.j = P.(len P - 2) by A7,XREAL_1:43; hence contradiction by A5,A17; end; suppose A18: j < len P - 2*1; reconsider lP2 = len P+2 as odd Element of NAT; reconsider jj = j as odd Element of NAT by ORDINAL1:def 12; set B = Q.cut(jj,lP2); len P < len P + 2 by XREAL_1:29; then A19: j <= len P + 2 by A15,XXREAL_0:2; then A20: B.last() = x by A9,A6,GLIB_001:37; A21: len B + j = len P + 2 + 1 by A6,A19,GLIB_001:36; A22: now let i be even Nat such that A23: i < len B-1; j + i < (len B - 1) + j by A23,XREAL_1:8; then A24: j + i <= len P + 2 - 2 by A21,Th3; len B - 1 < len B by XREAL_1:44; then A25: i < len B by A23,XXREAL_0:2; A26: i in NAT by ORDINAL1:def 12; then j+i in dom Q by A6,A19,A25,GLIB_001:36; then A27: 1 <= j + i by FINSEQ_3:25; B.(i+1) = Q.(j+i) by A6,A19,A26,A25,GLIB_001:36; hence B.(i+1) = P.(j+i) & j+i in dom P by A7,A27,A24,FINSEQ_3:25; end; set C = B.addEdge(e); A28: B.first() = Q.j by A6,A19,GLIB_001:37; A29: B.first() = Q.j by A6,A19,GLIB_001:37; then A30: e Joins B.last(),B.first(),G by A17,A20,GLIB_000:14; A31: now let n be odd Nat such that A32: n <= len B; 1 <= n by Th2; then n in dom B by A32,FINSEQ_3:25; hence C.n = B.n by A30,GLIB_001:65; end; A33: len P + 3 - (len P - 2) < len P + 3 - j by A18,XREAL_1:15; then A34: 3 < len B by A21,XXREAL_0:2; len B + 2 > 5 + 2 by A21,A33,XREAL_1:8; then A35: len C > 7 by A17,A20,GLIB_000:14,GLIB_001:64; A36: now assume C.length() <= 3; then 2*C.length() <= 2*3 by XREAL_1:64; then 2*C.length()+1 <= 2*3+1 by XREAL_1:6; hence contradiction by A35,GLIB_001:112; end; P.vertexAt(j) = P.j by A15,GLIB_001:def 8; then P.j in P.vertices() by A16,A13,A14,GLIB_001:89,XXREAL_0:2; then B.first() in P.vertices() by A7,A13,A14,A28,XXREAL_0:2; then A37: B is open by A3,A20,GLIB_001:def 24; then C is Cycle-like by A17,A34,A29,A20,Th33,GLIB_000:14; then C is chordal by A36,Def11; then consider m,n being odd Nat such that A38: m+2 < n and A39: n <= len C and A40: C.m <> C.n and A41: ex e being set st e Joins C.m,C.n,G and A42: C is Cycle-like implies not (m=1 & n = len C) & not (m=1 & n = len C-2) & not (m=3 & n = len C) by Th84; consider e being set such that A43: e Joins C.m,C.n,G by A41; 1 <= m by Th2; then 1-1 <= m-1 by XREAL_1:9; then reconsider m1 = m-1 as even Element of NAT by INT_1:3; reconsider m1 as even Nat; A44: len C = len B + 2 by A17,A20,GLIB_000:14,GLIB_001:64; then m+2 < len B+2 by A38,A39,XXREAL_0:2; then A45: m+2-2 < len B+2-2 by XREAL_1:9; then A46: m1 < len B-1 by XREAL_1:9; then A47: B.(m1+1) = P.(j+m1) by A22; A48: j+m1 in dom P by A22,A46; then A49: j+m1 <= len P by FINSEQ_3:25; A50: C.last() = Q.j by A28,A30,GLIB_001:63; now assume A51: n = len C; then e Joins P.(j+m1),Q.j,G by A31,A50,A43,A45,A47; then e Joins P.(j+m1),P.j,G by A7,A13,A14,XXREAL_0:2; then A52: e Joins P.j,P.(j+m1),G by GLIB_000:14; now assume m <= 3; then m <= 4 by XXREAL_0:2; hence contradiction by A17,A34,A29,A20,A37,A42,A51,Th7,Th33, GLIB_000:14; end; then A53: 2+1-1 < m-1 by XREAL_1:9; then A54: j < j+m1 by XREAL_1:29; j + 2 < j+m1 by A53,XREAL_1:8; hence contradiction by A1,A2,A49,A52,A54,Th92; end; then n < len B+2*1 by A44,A39,XXREAL_0:1; then A55: n <= len B+2-2 by Th3; then A56: C.n = B.n by A31; 1 <= n by Th2; then 1-1 <= n-1 by XREAL_1:9; then reconsider n1 = n-1 as even Element of NAT by INT_1:3; reconsider n1 as even Nat; m+2-1 len P + 1; then 2*kk >= len P + 1 + 1 by NAT_1:13; hence contradiction by A60,XREAL_1:29; end; A65: now assume kk >= k; then A66: 2*kk >= 2*k by XREAL_1:64; j + 2*kk + m1 > j + 2*kk by A63,XREAL_1:29; hence contradiction by A12,A60,A66,XREAL_1:7; end; C.n = x by A20,A31,A61; hence contradiction by A10,A43,A60,A62,A64,A65,A58; end; then n < len B by A55,XXREAL_0:1; then A67: n1 < len B-1 by XREAL_1:9; then j+n1 in dom P by A22; then A68: j+n1 <= len P by FINSEQ_3:25; m < m+2 by XREAL_1:29; then m < n by A38,XXREAL_0:2; then m1 < n1 by XREAL_1:9; then A69: j+m1 < j+n1 by XREAL_1:8; A70: C.m = B.m by A31,A45; B.(n1+1) = P.(j+n1) by A22,A67; hence contradiction by A1,A2,A43,A47,A68,A70,A56,A69,A57,Th92; end; end; then A71: for k being Nat st for a being Nat st a < k holds P[a] holds P[k]; A72: for k being Nat holds P[k] from NAT_1:sch 4(A71); A73: now let n be odd Nat such that A74: n <= len P-2; len P-2 <= len P-2+4 by XREAL_1:31; then consider k being Nat such that A75: n + 2*k = len P + 2 by A74,Lm2,XXREAL_0:2; A76: now assume 2*k > len P + 1; then n + 2*k > 1 + (len P + 1) by Th2,XREAL_1:8; hence contradiction by A75; end; now assume A77: 2*k < 4; n + 4 <= len P-2+4 by A74,XREAL_1:7; hence contradiction by A75,A77,XREAL_1:8; end; hence not ex e being set st e Joins Q.n,x,G by A72,A75,A76; end; A78: now assume Q is chordal; then consider m,n being odd Nat such that A79: m+2 < n and A80: n <= len Q and Q.m <> Q.n and A81: ex e being set st e Joins Q.m,Q.n,G and Q is Cycle-like implies not (m=1 & n = len Q) & not (m=1 & n = len Q-2 ) & not (m=3 & n = len Q) by Th84; m+2 < len P+2 by A6,A79,A80,XXREAL_0:2; then A82: m+2-2 < len P+2-2 by XREAL_1:9; m < m+2 by XREAL_1:29; then A83: m < n by A79,XXREAL_0:2; per cases by A80,XXREAL_0:1; suppose A84: n = len Q; then m+2-2 < len P+2-2 by A6,A79,XREAL_1:9; hence contradiction by A9,A73,A81,A84,Th3; end; suppose A85: n < len Q; A86: Q.m = P.m by A7,A82; A87: n <= len P + 2 - 2 by A6,A85,Th3; then Q.n = P.n by A7; hence contradiction by A1,A2,A79,A81,A83,A87,A86,Th92; end; end; Q.first() = P.first() by A4,GLIB_001:63; then Q.first() in P.vertices() by GLIB_001:88; hence thesis by A3,A9,A78,GLIB_001:def 24; end; :: Golumbic, page 83. Theorem 4.1 (i) ==> (iii) theorem Th98: for G being chordal _Graph, a,b being Vertex of G st a<>b & not a,b are_adjacent for S being VertexSeparator of a,b st S is minimal & S is non empty for H being inducedSubgraph of G,S holds H is complete proof let G be chordal _Graph; set tVG = the_Vertices_of G; let a,b be Vertex of G such that A1: a<>b and A2: not a,b are_adjacent; let S be VertexSeparator of a,b such that A3: S is minimal and A4: S is non empty; set Gns = the removeVertices of G,S; reconsider sa = a, sb = b as Vertex of Gns by A1,A2,Th77; set A = Gns.reachableFrom(sa), B = Gns.reachableFrom(sb); A5: A/\B = {} by A1,A2,Th76; set Gb = the inducedSubgraph of Gns,B; set Ga = the inducedSubgraph of Gns,A; A6: the_Vertices_of Ga = A by GLIB_000:def 37; A7: the_Vertices_of Gb = B by GLIB_000:def 37; A8: B /\ S = {} by A1,A2,Th75; A9: A/\S = {} by A1,A2,Th75; the_Vertices_of Gns c= tVG; then reconsider A, B as non empty Subset of tVG by XBOOLE_1:1; let Gs be inducedSubgraph of G,S; let x,y be Vertex of Gs such that A10: x <> y and A11: not x,y are_adjacent; reconsider xg = x, yg = y as Vertex of G by GLIB_000:42; A12: S = the_Vertices_of Gs by A4,GLIB_000:def 37; then A13: ex xag being Vertex of G st xag in A & xg,xag are_adjacent by A1,A2,A3 ,Th82; set Bx = B\/{xg}, Ax = A\/{xg}; set Gbx = the inducedSubgraph of G,Bx; set Gax = the inducedSubgraph of G,Ax; set xy = {xg, yg}; A14: the_Vertices_of Gbx = Bx by GLIB_000:def 37; now let x be set such that A15: x in A; not x in S by A9,A15,XBOOLE_0:def 4; hence x in tVG \ S by A15,XBOOLE_0:def 5; end; then A16: A c= tVG \ S by TARSKI:def 3; consider yag being Vertex of G such that A17: yag in A and A18: yg,yag are_adjacent by A1,A2,A3,A12,Th82; A19: yag in Ax by A17,XBOOLE_0:def 3; set Gb1 = the inducedSubgraph of G,B\/{x}\/{y}; set Ga1 = the inducedSubgraph of G,A\/{x}\/{y}; A20: the_Vertices_of Gax = Ax by GLIB_000:def 37; not a in S by A1,A2,Def8; then A21: tVG\S is non empty Subset of tVG by XBOOLE_0:def 5; then reconsider Ga as inducedSubgraph of G,A by A16,Th29; A22: not y in {x} by A10,TARSKI:def 1; now let x be set such that A23: x in B; not x in S by A8,A23,XBOOLE_0:def 4; hence x in tVG \ S by A23,XBOOLE_0:def 5; end; then A24: B c= tVG \ S by TARSKI:def 3; then reconsider Gb as inducedSubgraph of G,B by A21,Th29; y in xy by TARSKI:def 2; then A25: y in A\/xy by XBOOLE_0:def 3; A26: ex xbg being Vertex of G st xbg in B & xg,xbg are_adjacent by A1,A2,A3,A12 ,Th83; not x in B by A24,A12,XBOOLE_0:def 5; then x in G.AdjacentSet(the_Vertices_of Gb) by A7,A26; then A27: Gbx is connected by Th57; y in xy by TARSKI:def 2; then A28: y in B\/xy by XBOOLE_0:def 3; consider ybg being Vertex of G such that A29: ybg in B and A30: yg,ybg are_adjacent by A1,A2,A3,A12,Th83; A31: B\/{x}\/{y} = B\/({x}\/{y}) by XBOOLE_1:4 .= B\/xy by ENUMSET1:1; then A32: the_Vertices_of Gb1 c= B\/xy by GLIB_000:def 37; x in xy by TARSKI:def 2; then x in B\/xy by XBOOLE_0:def 3; then reconsider xb = x, yb = y as Vertex of Gb1 by A31,A28,GLIB_000:def 37; A33: ybg in Bx by A29,XBOOLE_0:def 3; not y in B by A24,A12,XBOOLE_0:def 5; then not yg in the_Vertices_of Gbx by A14,A22,XBOOLE_0:def 3; then y in G.AdjacentSet(the_Vertices_of Gbx) by A14,A30,A33; then Gb1 is connected by A27,Th57; then consider Wb being Walk of Gb1 such that A34: Wb is_Walk_from yb,xb by GLIB_002:def 1; not x in A by A16,A12,XBOOLE_0:def 5; then x in G.AdjacentSet(the_Vertices_of Ga) by A6,A13; then A35: Gax is connected by Th57; A36: A\/{x}\/{y} = A\/({x}\/{y}) by XBOOLE_1:4 .= A\/xy by ENUMSET1:1; then A37: the_Vertices_of Ga1 c= A\/xy by GLIB_000:def 37; x in xy by TARSKI:def 2; then x in A\/xy by XBOOLE_0:def 3; then reconsider xa = x, ya = y as Vertex of Ga1 by A36,A25,GLIB_000:def 37; A38: not y in {x} by A10,TARSKI:def 1; not y in A by A16,A12,XBOOLE_0:def 5; then not yg in the_Vertices_of Gax by A20,A38,XBOOLE_0:def 3; then y in G.AdjacentSet(the_Vertices_of Gax) by A20,A18,A19; then Ga1 is connected by A35,Th57; then consider Wa being Walk of Ga1 such that A39: Wa is_Walk_from xa,ya by GLIB_002:def 1; A40: (A\/xy)/\(B\/xy) = A/\B\/xy by XBOOLE_1:24 .= xy by A5; A41: Wa.last() = ya by A39,GLIB_001:def 23; A42: Wa.first() = xa by A39,GLIB_001:def 23; A43: Wb.last() = xa by A34,GLIB_001:def 23; A44: Wb.first() = ya by A34,GLIB_001:def 23; consider Pb being Path of Gb1 such that A45: Pb is_Walk_from Wb.first(),Wb.last() and A46: Pb is minlength by Th39; consider Pa being Path of Ga1 such that A47: Pa is_Walk_from Wa.first(),Wa.last() and A48: Pa is minlength by Th39; reconsider Pag = Pa, Pbg = Pb as Path of G by GLIB_001:175; Pb.first() = Pb.1; then A49: Pbg.1 = yg by A44,A45,GLIB_001:def 23; Pbg.vertices() = Pb.vertices() by GLIB_001:98; then A50: Pbg.vertices() c= B\/xy by A32,XBOOLE_1:1; Pag.vertices() = Pa.vertices() by GLIB_001:98; then Pag.vertices() c= A\/xy by A37,XBOOLE_1:1; then A51: Pag.vertices() /\ Pbg.vertices() c= xy by A50,A40,XBOOLE_1:27; set P = Pag.append(Pbg); Pa.last() = Pa.len Pa; then A52: Pag.len Pag = yg by A41,A47,GLIB_001:def 23; A53: Pb.last() = Pb.len Pb; then A54: Pbg.len Pbg = xg by A43,A45,GLIB_001:def 23; A55: Pbg.last() = Pbg.len Pbg; then A56: x in Pbg.vertices() by A54,GLIB_001:88; A57: Pbg.first() = Pbg.1; then A58: y in Pbg.vertices() by A49,GLIB_001:88; A59: Pbg is non trivial by A10,A57,A55,A49,A54,GLIB_001:127; A60: Pbg is open by A10,A57,A55,A49,A54,GLIB_001:def 24; A61: not Pbg is Cycle-like by A10,A57,A55,A49,A54,GLIB_001:def 24; A62: not xg,yg are_adjacent by A4,A11,Th45; then A63: Pbg.length() >= 2 by A10,A57,A55,A49,A54,Th46; Pa.first() = Pa.1; then A64: Pag.1 = xg by A42,A47,GLIB_001:def 23; A65: Pag.edges() misses Pbg.edges() proof assume Pag.edges() /\ Pbg.edges() <> {}; then consider e being set such that A66: e in Pag.edges() /\ Pbg.edges() by XBOOLE_0:def 1; e in Pag.edges() by A66,XBOOLE_0:def 4; then e in Pa.edges() by GLIB_001:110; then consider a1, a2 being Vertex of Ga1, na being odd Element of NAT such that A67: na+2 <= len Pag and A68: a1 = Pag.na and e = Pag.(na+1) and A69: a2 = Pag.(na+2) and A70: e Joins a1, a2,Ga1 by GLIB_001:103; A71: e Joins a1,a2,G by A70,GLIB_000:72; e in Pbg.edges() by A66,XBOOLE_0:def 4; then e in Pb.edges() by GLIB_001:110; then consider b1, b2 being Vertex of Gb1, nb being odd Element of NAT such that nb+2 <= len Pbg and b1 = Pbg.nb and e = Pbg.(nb+1) and b2 = Pbg.(nb+2) and A72: e Joins b1, b2,Gb1 by GLIB_001:103; A73: the_Vertices_of Gb1 = B\/xy by A31,GLIB_000:def 37; e Joins b1,b2,G by A72,GLIB_000:72; then A74: a1=b1 & a2=b2 or a1=b2 & a2=b1 by A71,GLIB_000:15; then A75: a1 in B or a1 in xy by A73,XBOOLE_0:def 3; A76: the_Vertices_of Ga1 = A\/xy by A36,GLIB_000:def 37; then A77: a1 in A or a1 in xy by XBOOLE_0:def 3; A78: a2 in A or a2 in xy by A76,XBOOLE_0:def 3; A79: a2 in B or a2 in xy by A74,A73,XBOOLE_0:def 3; per cases by A5,A77,A78,A75,A79,TARSKI:def 2,XBOOLE_0:def 4; suppose A80: a1 = x & a2 = x or a1 = y & a2 = y; na < na+2 by XREAL_1:39; hence contradiction by A10,A64,A52,A67,A68,A69,A80,GLIB_001:def 28; end; suppose a1 = x & a2 = y or a1 = y & a2 = x; hence contradiction by A62,A71,Def3; end; end; A81: Pag.first() = Pag.1; then A82: x in Pag.vertices() by A64,GLIB_001:88; A83: Pag.last() = Pag.len Pag; then A84: len P +1 = len Pag + len Pbg by A52,A57,A49,GLIB_001:28; A85: Pag.length() >= 2 by A10,A62,A81,A83,A64,A52,Th46; P.length() = Pag.length()+Pbg.length() by A83,A52,A57,A49,Th28; then P.length() >= 2+2 by A85,A63,XREAL_1:7; then P.length() >= 3+1; then A86: P.length() > 3 by NAT_1:13; A87: Pag is open by A10,A81,A83,A64,A52,GLIB_001:def 24; A88: y in Pag.vertices() by A83,A52,GLIB_001:88; xy c= Pag.vertices() /\ Pbg.vertices() proof let a be set; assume a in xy; then a = x or a = y by TARSKI:def 2; hence thesis by A82,A88,A56,A58,XBOOLE_0:def 4; end; then Pag.vertices() /\ Pbg.vertices() = xy by A51,XBOOLE_0:def 10; then P is Cycle-like by A81,A83,A64,A52,A87,A57,A55,A49,A54,A60,A59,A65,Th27; then P is chordal by A86,Def11; then consider m, n being odd Nat such that A89: m+2 < n and A90: n <= len P and A91: P.m <> P.n and A92: ex e being set st e Joins P.m,P.n,G and A93: for f being set st f in P.edges() holds not f Joins P.m,P.n,G by Def10; A94: m < n by A89,NAT_1:12; consider e being set such that A95: e Joins P.m,P.n,G by A92; A96: e Joins P.n,P.m,G by A95,GLIB_000:14; A97: m in NAT by ORDINAL1:def 12; A98: not Pag is Cycle-like by A10,A81,A83,A64,A52,GLIB_001:def 24; A99: 1 <= n by ABIAN:12; A100: 1 <= m by ABIAN:12; per cases; suppose A101: m < len Pag & n <= len Pag; then n in dom Pag by A99,FINSEQ_3:25; then A102: P.n = Pag.n by GLIB_001:32; m in dom Pag by A100,A101,FINSEQ_3:25; then P.m = Pag.m by GLIB_001:32; then Pag is chordal by A98,A89,A92,A101,A102,Th85; then Pa is chordal by A36,Th87; hence contradiction by A48,Th89; end; suppose A103: m < len Pag & len Pag < n; then A104: Pag.m in the_Vertices_of Ga1 by A97,GLIB_001:7; m in dom Pag by A100,A103,FINSEQ_3:25; then A105: P.m = Pag.m by GLIB_001:32; A106: not n in dom Pag by A103,FINSEQ_3:25; n in dom P by A90,A99,FINSEQ_3:25; then consider n1 being Element of NAT such that A107: n1 < len Pbg and A108: n = len Pag + n1 by A106,GLIB_001:34; A109: P.(len Pag +n1) = Pbg.(n1+1) by A83,A52,A57,A49,A107,GLIB_001:33; reconsider n1 as even Element of NAT by A108; reconsider n11 = n1+1 as odd Element of NAT; A110: n11 <= len Pbg by A107,NAT_1:13; then A111: Pbg.n11 in the_Vertices_of Gb1 by GLIB_001:7; per cases by A37,A32,A104,A111,XBOOLE_0:def 3; suppose A112: Pag.m in A & Pbg.n11 in xy; per cases by A64,A52,A112,TARSKI:def 2; suppose A113: Pbg.n11 = Pag.1; now assume A114: 1+2 >= m; per cases by A114,XXREAL_0:1; suppose 1+2 > m; then 1 >= m by Th4,JORDAN12:2; hence contradiction by A91,A100,A105,A108,A109,A113,XXREAL_0:1; end; suppose A115: 1+2 = m; then A116: 1+1 < len Pag by A103,XXREAL_0:2; then 1+1 in dom Pag by FINSEQ_3:25; then A117: Pag.(1+1) = P.(1+1) by GLIB_001:32; 1 < len Pag -1 by A116,XREAL_1:20; then 1+0 < (len Pag -1) + len Pbg by XREAL_1:8; then A118: P.(1+1) in P.edges() by A84,GLIB_001:100,JORDAN12:2; 1 < len Pag by A100,A103,XXREAL_0:2; then Pag.(1+1) Joins Pag.1,Pag.m,G by A115,GLIB_001:def 3 ,JORDAN12:2; hence contradiction by A93,A105,A108,A109,A113,A117,A118, GLIB_000:14; end; end; then Pag is chordal by A98,A96,A103,A105,A108,A109,A113,Th85,JORDAN12:2 ; then Pa is chordal by A36,Th87; hence contradiction by A48,Th89; end; suppose A119: Pbg.n11 = Pag.len Pag; now set L = len Pag; assume A120: m+2 >= len Pag; per cases by A120,XXREAL_0:1; suppose A121: m+2 = L; then A122: L = m+1+1; then A123: m +1 < L by NAT_1:13; 1<=m+1 by NAT_1:12; then m+1 in dom Pag by A123,FINSEQ_3:25; then A124: Pag.(m+1) = P.(m+1) by GLIB_001:32; m < len Pag -1 by A122,NAT_1:13; then m+0 < (len Pag -1) + len Pbg by XREAL_1:8; then A125: P.(m+1) in P.edges() by A84,GLIB_001:100; m < L by A123,NAT_1:13; then Pag.(m+1) Joins Pag.m,Pag.L,G by A97,A121,GLIB_001:def 3; hence contradiction by A93,A105,A108,A109,A119,A124,A125; end; suppose m+2 > len Pag; hence contradiction by A103,Th4; end; end; then Pag is chordal by A98,A92,A105,A108,A109,A119,Th85; then Pa is chordal by A36,Th87; hence contradiction by A48,Th89; end; end; suppose A126: Pag.m in A & Pbg.n11 in B; then reconsider bc = Pb.n11 as Vertex of Gb by GLIB_000:def 37; reconsider ac = Pa.m as Vertex of Ga by A126,GLIB_000:def 37; set WAB = Gns.walkOf(ac,e,bc); e Joins ac,bc,Gns by A16,A24,A95,A105,A108,A109,A126,Th19; then A127: WAB is_Walk_from ac,bc by GLIB_001:15; b in B by GLIB_002:9; then reconsider bb = b as Vertex of Gb by GLIB_000:def 37; a in A by GLIB_002:9; then reconsider aa = a as Vertex of Ga by GLIB_000:def 37; consider WA being Walk of Ga such that A128: WA is_Walk_from aa, ac by GLIB_002:def 1; consider WB being Walk of Gb such that A129: WB is_Walk_from bc, bb by GLIB_002:def 1; reconsider WA, WB as Walk of Gns by GLIB_001:167; reconsider WAs = WA, WBs = WB as Walk of Gns; A130: WBs is_Walk_from bc, bb by A129,GLIB_001:19; set WaB = WAs.append(WAB); set Wab = WaB.append(WBs); WAs is_Walk_from aa, ac by A128,GLIB_001:19; then WaB is_Walk_from aa, bc by A127,GLIB_001:31; then Wab is_Walk_from a,b by A130,GLIB_001:31; hence contradiction by A1,A2,Def8; end; suppose Pag.m in xy & Pbg.n11 in B; then Pag.m = x or Pag.m = y by TARSKI:def 2; then A131: Pag.m = x by A64,A52,A97,A103,GLIB_001:def 28 .= Pbg.len Pbg by A43,A45,A53,GLIB_001:def 23; now set L = len Pbg; assume A132: n11+2 >= len Pbg; per cases by A132,XXREAL_0:1; suppose A133: n11+2 = L; then A134: L = n11+1+1; then n11 < len Pbg -1 by NAT_1:13; then A135: len Pag +n11 < (len Pbg -1) + len Pag by XREAL_1:6; n11 +1 < L by A134,NAT_1:13; then A136: n11 < L by NAT_1:13; then Pbg.(n11+1) Joins Pbg.n11,Pbg.L,Gb1 by A133,GLIB_001:def 3; then Pbg.(n11+1) Joins Pbg.L,Pbg.n11,Gb1 by GLIB_000:14; then A137: Pbg.(n11+1) Joins Pbg.L,Pbg.n11,G by GLIB_000:72; A138: 1 <= len Pag +n11 by ABIAN:12,NAT_1:12; Pbg.(n11+1) = P.(len Pag + n11) by A83,A52,A57,A49,A136,GLIB_001:33; then Pbg.(n11+1) in P.edges() by A84,A138,A135,GLIB_001:99; hence contradiction by A93,A105,A108,A109,A131,A137; end; suppose n11+2 > len Pbg; then n11 >= len Pbg by Th4; hence contradiction by A91,A105,A108,A109,A110,A131,XXREAL_0:1; end; end; then Pbg is chordal by A61,A96,A105,A108,A109,A131,Th85; then Pb is chordal by A31,Th87; hence contradiction by A46,Th89; end; suppose A139: Pag.m in xy & Pbg.n11 in xy; then A140: Pbg.n11 = x or Pbg.n11 = y by TARSKI:def 2; Pag.m = x or Pag.m = y by A139,TARSKI:def 2; then xg,yg are_adjacent by A91,A92,A105,A108,A109,A140,Def3; hence contradiction by A4,A11,Th45; end; end; suppose A141: len Pag <= m; then consider m1 being Nat such that A142: m = len Pag + m1 by NAT_1:10; n > len Pag by A94,A141,XXREAL_0:2; then A143: not n in dom Pag by FINSEQ_3:25; n in dom P by A90,A99,FINSEQ_3:25; then consider n1 being Element of NAT such that A144: n1 < len Pbg and A145: n = len Pag + n1 by A143,GLIB_001:34; A146: P.(len Pag +n1) = Pbg.(n1+1) by A83,A52,A57,A49,A144,GLIB_001:33; A147: m1 in NAT by ORDINAL1:def 12; A148: m1 < n1 by A94,A142,A145,XREAL_1:6; then m1 < len Pbg by A144,XXREAL_0:2; then A149: P.(len Pag +m1) = Pbg.(m1+1) by A83,A52,A57,A49,A147,GLIB_001:33; reconsider n1, m1 as even Element of NAT by A142,A145,ORDINAL1:def 12; reconsider m11 = m1+1, n11 = n1+1 as odd Element of NAT; A150: m11 < n11 by A148,XREAL_1:6; n11 <= len Pbg by A144,NAT_1:13; then A151: m11 < len Pbg by A150,XXREAL_0:2; A152: now assume A153: m11+2 >= n11; per cases by A153,XXREAL_0:1; suppose A154: m11+2 = n11; then m11 +1 < len Pbg by A144; then m11 < len Pbg -1 by XREAL_1:20; then A155: len Pag +m11 < (len Pbg -1) + len Pag by XREAL_1:6; A156: 1 <= len Pag +m11 by ABIAN:12,NAT_1:12; A157: Pbg.(m11+1) Joins Pbg.m11,Pbg.n11,G by A151,A154,GLIB_001:def 3; Pbg.(m11+1) = P.(len Pag +m11) by A83,A52,A57,A49,A151,GLIB_001:33; then Pbg.(m11+1) in P.edges() by A84,A156,A155,GLIB_001:99; hence contradiction by A93,A142,A145,A146,A149,A157; end; suppose m11+2 > n11; then m11 >= n11 by Th4; hence contradiction by A148,XREAL_1:6; end; end; n11 <= len Pbg by A144,NAT_1:13; then Pbg is chordal by A61,A92,A142,A145,A146,A149,A152,Th85; then Pb is chordal by A31,Th87; hence contradiction by A46,Th89; end; end; :: Golumbic, page 83, Theorem 4.1 (iii)->(i) theorem for G being finite _Graph st for a,b being Vertex of G st a<>b & not a ,b are_adjacent for S being VertexSeparator of a,b st S is minimal & S is non empty for G2 being inducedSubgraph of G,S holds G2 is complete holds G is chordal proof reconsider n = 2*2+1 as odd Nat; reconsider m = 2*0+1 as odd Nat; let G be finite _Graph such that 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 & S is non empty for G2 being inducedSubgraph of G,S holds G2 is complete; let P be Walk of G such that A2: P.length() > 3 and A3: P is Cycle-like; 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 assume A6: P.m = P.n; n <= len P by A4,XXREAL_0:2; then n=len P by A3,A6,GLIB_001:def 28; hence contradiction by A4; end; per cases; suppose A7: ex e being set st e Joins P.m,P.n,G; A8: m+2 < n; len P+(-2) >= 9+(-2) by A4,XREAL_1:7; then A9: not (m=1 & n = len P-2); A10: not (m=1 & n = len P) by A4; n <= len P by A4,XXREAL_0:2; hence thesis by A3,A7,A8,A10,A9,Th85; end; suppose A11: not ex e being set st e Joins P.m,P.n,G; 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 Th79; set G2 = the inducedSubgraph of G,S; A13: n <= len P by A4,XXREAL_0:2; then P5l is_Walk_from P.n,P.(len P) by GLIB_001:37; then A14: P5l is_Walk_from P.n,P.m by A3,GLIB_001:118; A15: not Pm,Pn are_adjacent by A11,Def3; then S is VertexSeparator of Pn,Pm by A5,Th70; then consider l being odd Nat such that A16: 1 < l and A17: l < len P5l and A18: P5l.l in S by A5,A15,A14,Th72; 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 as even Nat; A20: l+(-1) < len P5l + (-1) by A17,XREAL_1:8; len P5l + 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 P5l by A17,XXREAL_0:2; then P5l.(l2+1) = P.(n+l2) by A13,GLIB_001:36; then reconsider bb=P.(n+l2) as Vertex of G2 by A18,GLIB_000:def 37; set P15=P.cut(m,n); A22: n <= len P by A4,XXREAL_0:2; then A23: P15 is_Walk_from P.m,P.n by GLIB_001:37; then S is non empty by A5,A15,Th73; then A24: G2 is complete by A1,A5,A15,A12; A25: len P15 + 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: P15.k in S by A5,A15,A23,Th72; A29: k <= 5-2 by A27,Th3; A30: 1+2 <= k by A26,Th4; then A31: k = 3 by A29,XXREAL_0:1; P15.(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 G2 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 assume A34: aa = bb; k < n+l2 by A31,A32,XXREAL_0:2; hence contradiction by A3,A31,A21,A33,A34,GLIB_001:def 28; end; then aa,bb are_adjacent by A24,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 A31,A35,GLIB_000:72; hence thesis by A3,A31,A21,A32,Th85; end; end; :: Exercise 12, p. 101. :: This needs "finite-branching", we do it for finite though theorem Th100: for G being finite chordal _Graph, a, b being Vertex of G st a <> b & not a,b are_adjacent for S being VertexSeparator of a,b st S is minimal for H being removeVertices of G,S, a1 being Vertex of H st 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 proof let G be finite chordal _Graph, a, b be Vertex of G such that A1: a <> b and A2: not a,b are_adjacent; let S be VertexSeparator of a,b such that A3: S is minimal; let H be removeVertices of G,S, a1 be Vertex of H such that A4: a = a1; 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; per cases; suppose S is empty; then not ex x being Vertex of G st x in S & not a,x are_adjacent; hence contradiction by A4,A5,GLIB_002:9; end; suppose S is non empty; then reconsider S as non empty Subset of the_Vertices_of G; set A = H.reachableFrom(a1); deffunc F(set) = card (G.AdjacentSet({$1}) /\ S); set M = { F(x) where x is Vertex of G : x in A }; A6: now let x be set; assume x in M; then ex y being Vertex of G st x = card (G.AdjacentSet({y}) /\ S) & y in A; hence x is natural; end; A7: A is finite; A8: M is finite from FRAENKEL:sch 21(A7); a in A by A4,GLIB_002:9; then card (G.AdjacentSet({a}) /\ S) in M; then reconsider M as finite non empty natural-membered set by A8,A6, MEMBERED:def 6; set Ga = the inducedSubgraph of H,A; A9: the_Vertices_of Ga = A 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 A; set gcs = G.AdjacentSet({c}) /\ S; A12: A/\S = {} by A1,A2,Th75; 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: tVG\S is non empty Subset of tVG by XBOOLE_0:def 5; the_Vertices_of H c= tVG; then reconsider A as non empty Subset of tVG by XBOOLE_1:1; now let x be set such that A15: x in A; not x in S by A12,A15,XBOOLE_0:def 4; hence x in tVG \ S by A15,XBOOLE_0:def 5; end; then A c= tVG \ S by TARSKI:def 3; then reconsider Ga 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,Ay; y in {y} by TARSKI:def 1; then A19: y in Ay by XBOOLE_0:def 3; c in Ay by A11,XBOOLE_0:def 3; then reconsider ca = c, ya = y as Vertex of Gay 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,Th82; then y in G.AdjacentSet(the_Vertices_of Ga) by A9,A18; then Gay is connected by Th57; then consider Wa being Walk of Gay such that A20: Wa is_Walk_from ca,ya by GLIB_002:def 1; consider P being Path of Gay such that A21: P is_Walk_from Wa.first(),Wa.last() and A22: P is minlength by Th39; Wa.first() = ca by A20,GLIB_001:def 23; then A23: P.first() = ca by A21,GLIB_001:def 23; Wa.last() = ya by A20,GLIB_001:def 23; then A24: P.last() = y by A21,GLIB_001:def 23; c <> y by A11,A16,A12,XBOOLE_0:def 4; then P is non trivial by A23,A24,GLIB_001:127; then A25: len P >= 3 by GLIB_001:125; A26: now assume len P < 2*2+1; then len P <= 5-2 by Th3; then A27: len P = 3 by A25,XXREAL_0:1; then 2*0+1 < len P; then P.(1+1) Joins P.1,P.(1+2),Gay by GLIB_001:def 3; then P.2 Joins c,y,G by A23,A24,A27,GLIB_000:72; hence contradiction by A17,Def3; end; 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 assume d = y; then len P - 2 = 1 by A24,A28,GLIB_001:def 28; then len P = 1 + 2; hence contradiction by A26; end; A30: not y in G.AdjacentSet({c}) by A17,Th52; A31: the_Vertices_of Gay = Ay by GLIB_000:def 37; A32: P.j in the_Vertices_of Gay by A28,GLIB_001:7; then A33: d in A or d in {y} by A31,XBOOLE_0:def 3; reconsider d as Vertex of G by A32; set gds = G.AdjacentSet({d}) /\ S; P.(j+1) Joins d,P.(len P-2+2),Gay 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 by Def3; then A35: y in G.AdjacentSet({d}) by A29,Th52; then A36: y in G.AdjacentSet({d}) /\ S by A16,XBOOLE_0:def 4; now assume A37: gcs c= gds; not y in gcs by A30,XBOOLE_0:def 4; then gcs c< gds by A36,A37,XBOOLE_0:def 8; then A38: card gcs < card gds by TREES_1:6; card gds in M by A33,A29,TARSKI:def 1; hence contradiction by A10,A38,XXREAL_2:def 8; end; then consider x being set such that A39: x in G.AdjacentSet({c}) /\ S and A40: not x in G.AdjacentSet({d}) /\ S by TARSKI:def 3; 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 as Vertex of G by A39; defpred Pmax[Nat] means $1 in dom P & $1 is odd & $1 < len P & ex e being set st e Joins x,P.($1),G; A43: for k being Nat st Pmax[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 Th52; then ex e being set st e Joins x,P.1,G by A23,Def3; then A47: ex k being Nat st Pmax[k] by A45,A46,A13; consider k being Nat such that A48: Pmax[k] and A49: for i being Nat st Pmax[i] holds k >= i from NAT_1:sch 6(A43,A47); reconsider k as odd Element of NAT by A48; set Q1 = P.cut(k,j); reconsider Q=Q1 as Path of G by GLIB_001:175; A50: k <= j by A48,Th3; A51: j < len P by XREAL_1:44; then A52: Q1 is minlength by A22,A50,Th42; A53: len Q + k = j + 1 by A50,A51,GLIB_001:36; A54: now let i be odd Nat such that A55: i in dom Q and A56: i <> 1; 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 set st e Joins Q.i,x,G; 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; now assume i1 <> 0; then k+0 < k + i1 by XREAL_1:8; hence contradiction by A49,A61,A63,A59,A62,GLIB_000:14; end; hence contradiction by A56; end; set cc = Q.first(), dd = Q.last(); A64: Q1.first() = P.k by A50,A51,GLIB_001:37; then A65: x,cc are_adjacent by A48,Def3; 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 Gs by A16,A41,GLIB_000:def 37; Gs is complete by A1,A2,A3,Th98; then xs,ys are_adjacent by A66,Def6; then consider ej being set such that A68: ej Joins xs,ys,Gs by Def3; ej Joins x,y,G by A68,GLIB_000:72; then A69: x,y are_adjacent by Def3; A70: Q1.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,Th52; then A73: Q.first() <> Q.last() by A48,A64,A70,Def3; then A74: Q is open by GLIB_001:def 24; A75: Q.vertices() = Q1.vertices() by GLIB_001:98; then dd in Q1.vertices() by GLIB_001:88; then A76: dd <> x by A31,A44,A67,XBOOLE_0:def 3; A77: now A78: 2*0+1 <= k by ABIAN:12; then A79: len P.cut(1,k) + 1 = k + 1 by A48,GLIB_001:36; assume P.k = P.(len P); then P.cut(1,k) is_Walk_from P.first(),P.last() by A48,A78,GLIB_001:37; hence contradiction by A22,A48,A79,Def2; end; A80: now let v be set such that A81: v in Q.vertices(); consider 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 A88: 1 <= k by ABIAN:12; assume A89: v = y; then A90: k+(n+-1) = 1 by A24,A83,A87,A86,GLIB_001:def 28; A91: now assume 1 < n; then 1+1 <= n by NAT_1:13; then 2+1 <= k+n by A88,XREAL_1:7; hence contradiction by A90; end; 1 <= n by ABIAN:12; hence contradiction by A24,A77,A64,A83,A89,A91,XXREAL_0:1; 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; end; cc in Q1.vertices() by A75,GLIB_001:88; then A93: cc <> x by A31,A44,A67,XBOOLE_0:def 3; dd,y are_adjacent by A34,A70,Def3; then consider R being Path of G such that A94: len R = 7 and A95: R.length() = 3 and A96: R.vertices() = {dd,y,x,cc} and A97: R.1 = dd and A98: R.3 = y and A99: R.5 = x and A100: R.7 = cc by A24,A29,A66,A69,A77,A64,A70,A76,A93,A65,Th48; A101: R is non trivial by A94,GLIB_001:126; A102: Q.edges() misses R.edges() proof assume not Q.edges() misses R.edges(); then Q.edges() /\ R.edges() <> {} by XBOOLE_0:def 7; then consider e being set such that A103: e in Q.edges() /\ R.edges() by XBOOLE_0:def 1; A104: e in Q.edges() by A103,XBOOLE_0:def 4; e in R.edges() by A103,XBOOLE_0:def 4; then consider n being even Element of NAT such that A105: 1 <= n and A106: n <= 7 and A107: R.n = e by A94,GLIB_001:99; per cases by A105,A106,Th13; suppose A108: n = 2; 2*0+1 < len R by A94; then R.(1+1) Joins R.1,R.(1+2),G by GLIB_001:def 3; then y in Q.vertices() by A98,A104,A107,A108,GLIB_001:105; then y in A by A80; hence contradiction by A16,A12,XBOOLE_0:def 4; end; suppose A109: n = 4; 2*1+1 < len R by A94; then R.(3+1) Joins R.3,R.(3+2),G by GLIB_001:def 3; then y in Q.vertices() by A98,A104,A107,A109,GLIB_001:105; then y in A by A80; hence contradiction by A16,A12,XBOOLE_0:def 4; end; suppose A110: n = 6; 2*2+1 < len R by A94; then R.(5+1) Joins R.5,R.(5+2),G by GLIB_001:def 3; then x in Q.vertices() by A99,A104,A107,A110,GLIB_001:105; then x in A by A80; hence contradiction by A12,A41,XBOOLE_0:def 4; end; end; now let v be set such that A111: v in {Q.first(), Q.last()}; per cases by A111,TARSKI:def 2; suppose A112: v = cc; then A113: v in Q.vertices() by GLIB_001:88; v in R.vertices() by A94,A100,A112,GLIB_001:87; hence v in Q.vertices() /\ R.vertices() by A113,XBOOLE_0:def 4; end; suppose A114: v = dd; 2*0+1 <= len R by A94; then A115: v in R.vertices() by A97,A114,GLIB_001:87; v in Q.vertices() by A114,GLIB_001:88; hence v in Q.vertices() /\ R.vertices() by A115,XBOOLE_0:def 4; end; end; then A116: {Q.first(),Q.last()} c= Q.vertices()/\R.vertices() by TARSKI:def 3; now let v be set such that A117: v in Q.vertices() /\ R.vertices(); v in {dd,y,x,cc} by A96,A117,XBOOLE_0:def 4; then A118: v = dd or v = y or v = x or v = cc 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; end; then Q.vertices() /\ R.vertices() c= {Q.first(), Q.last()} by TARSKI:def 3; then A119: Q.vertices() /\ R.vertices() = { Q.first(), Q.last() } by A116, XBOOLE_0:def 10; A120: now let i be odd Nat such that A121: i in dom Q and A122: i <> len Q; 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 Ay by A31,GLIB_001:7; now A128: len P - k + -1 < len P - k by XREAL_1:30; assume ki1 = len P; hence contradiction by A53,A124,A123,A128,XXREAL_0:2; end; 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 Ay by A31,GLIB_001:7; assume A132: ex e being set st e Joins Q.i,y,G; Q.(i1+1) = P.(ki1) by A50,A51,A125,GLIB_001:36; hence contradiction by A22,A24,A132,A130,A127,A131,Th19,Th40; end; A133: Q.first() = P.k by A64; P.k <> P.j by A72,A48,Def3; then A134: Q is non trivial by A133,A71,GLIB_001:127; then Q.length() <> 0 by GLIB_001:def 26; then A135: Q.length() >= 0+1 by NAT_1:13; set C = Q.append(R); A136: R.first() = dd by A97; then A137: C.(len Q+6) = R.(6+1) by A94,GLIB_001:33; A138: C.(len Q+4) = R.(4+1) by A94,A136,GLIB_001:33; A139: C.(len Q+2) = R.(2+1) by A94,A136,GLIB_001:33; C.length() = Q.length() + 3 by A95,A136,Th28; then C.length() >= 1 + 3 by A135,XREAL_1:7; then A140: C.length() > 3 by NAT_1:13; A141: R.last() = cc by A94,A100; then A142: R is open by A73,A136,GLIB_001:def 24; then C is Cycle-like by A74,A136,A141,A101,A102,A119,Th27; then C is chordal by A140,Def11; then consider m, n being odd Nat such that A143: m+2 < n and A144: n <= len C and C.m <> C.n and A145: ex e being set st e Joins C.m,C.n,G and A146: C is Cycle-like implies not (m=1 & n = len C) & not (m=1 & n = len C-2) & not (m=3 & n = len C) by Th84; consider e being set such that A147: e Joins C.m,C.n,G by A145; A148: len C +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 proof per cases; suppose n <= len Q; hence thesis; end; suppose n > len Q; then A150: len Q +2 <= n by Th4; per cases by A150,XXREAL_0:1; suppose len Q +2 = n; hence thesis; end; suppose len Q +2 < n; then A151: len Q +2+2 <= n by Th4; per cases by A151,XXREAL_0:1; suppose len Q +4 = n; hence thesis; end; suppose len Q +2*2 < n; then len Q +4+2 <= n by Th4; hence thesis by A94,A148,A144,XXREAL_0:1; end; end; end; end; A152: 1 <= m by ABIAN:12; per cases by A149; suppose A153: n <= len Q; A154: 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 = C.m by GLIB_001:32; 1 <= n by ABIAN:12; then n in dom Q by A153,FINSEQ_3:25; then Q.n = C.n by GLIB_001:32; hence contradiction by A52,A143,A147,A153,A155,Th41; end; suppose A156: n = len Q + 2; then 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; end; suppose A158: n = len Q + 4; then 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 by A152,XXREAL_0:1; suppose 1 = m; hence contradiction by A74,A94,A136,A141,A101,A142,A102,A119,A148,A146 ,A158,Th27; end; suppose 1 < m; hence contradiction by A54,A159,A160; end; end; suppose A161: n = len Q +6; then 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 by A162,XXREAL_0:1; suppose A163: m < len Q +2; now assume 1+2 >= m; then 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; 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 C.m = Q.m by GLIB_001:32; hence contradiction by A52,A100,A137,A147,A161,A165,A164,Th41, GLIB_000:14; end; suppose A166: m = len Q + 2; 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; end; end; end; end; theorem for G being finite chordal _Graph, a, b being Vertex of G st a <> b & not a,b are_adjacent for S being VertexSeparator of a,b st S is minimal for H being removeVertices of G,S, a1 being Vertex of H st a = a1 for x, y being Vertex of G st x in S & y in S holds ex c being Vertex of G st c in H .reachableFrom(a1) & c,x are_adjacent & c,y are_adjacent proof let G be finite chordal _Graph; let a,b be Vertex of G such that A1: a <> b and A2: not a,b are_adjacent; let S be VertexSeparator of a,b such that A3: S is minimal; let H be removeVertices of G,S, a1 be Vertex of H; assume a = a1; then consider c being Vertex of G such that A4: c in H.reachableFrom(a1) and A5: for x being Vertex of G st x in S holds c,x are_adjacent by A1,A2,A3,Th100; let x,y be Vertex of G such that A6: x in S and A7: y in S; A8: c,y are_adjacent by A7,A5; c,x are_adjacent by A6,A5; hence thesis by A4,A8; end; :: Golumbic, page 83, Lemma 4.2. theorem Th102: for G being non trivial finite chordal _Graph st not G is complete ex a,b being Vertex of G st a<>b & not a,b are_adjacent & a is simplicial & b is simplicial proof defpred P[finite _Graph] means $1 is non trivial & $1 is chordal & not $1 is complete implies ex a,b being Vertex of $1 st a <> b & not a,b are_adjacent & a is simplicial & b is simplicial; A1: for k being non zero Nat st for Gk being finite _Graph st Gk.order() < k holds P[Gk] holds for Gk1 being finite _Graph st Gk1.order() = k holds P[Gk1] proof let k be non zero Nat such that A2: for Gk being finite _Graph st Gk.order() < k holds P[Gk]; let Gk1 be finite _Graph such that A3: Gk1.order() = k and A4: Gk1 is non trivial and A5: Gk1 is chordal and A6: not Gk1 is complete; reconsider G=Gk1 as non trivial finite chordal _Graph by A4,A5; consider a,b being Vertex of G such that A7: a <> b and A8: not a,b are_adjacent by A6,Def6; consider S being VertexSeparator of a,b such that A9: S is minimal by Th79; set Gns = the removeVertices of G,S; reconsider sa = a, sb = b as Vertex of Gns by A7,A8,Th77; set A = Gns.reachableFrom(sa), B = Gns.reachableFrom(sb); set Gas = the inducedSubgraph of G,(A \/ S); A10: A c= the_Vertices_of Gns; then A11: A c= the_Vertices_of G by XBOOLE_1:1; then A12: A\/S is non empty Subset of the_Vertices_of G by XBOOLE_1:8; A13: A /\ B = {} by A7,A8,Th76; A14: now assume A15: b in A \/ S; not b in S by A7,A8,Def8; then A16: b in A by A15,XBOOLE_0:def 3; b in B by GLIB_002:9; hence contradiction by A13,A16,XBOOLE_0:def 4; end; A17: now assume Gas.order() = k; then A18: the_Vertices_of Gas = the_Vertices_of G by A3,PRE_POLY:8; the_Vertices_of Gas = A\/S by A12,GLIB_000:def 37; hence contradiction by A14,A18; end; set Gbs = the inducedSubgraph of G,(B \/ S); A19: B c= the_Vertices_of G by A10,XBOOLE_1:1; then A20: B\/S is non empty Subset of the_Vertices_of G by XBOOLE_1:8; A21: now assume A22: a in B \/ S; not a in S by A7,A8,Def8; then A23: a in B by A22,XBOOLE_0:def 3; a in A by GLIB_002:9; hence contradiction by A13,A23,XBOOLE_0:def 4; end; A24: now assume Gbs.order() = k; then A25: the_Vertices_of Gbs = the_Vertices_of G by A3,PRE_POLY:8; the_Vertices_of Gbs = B\/S by A20,GLIB_000:def 37; hence contradiction by A21,A25; end; set Gs = the inducedSubgraph of G,S; not a in S by A7,A8,Def8; then a in the_Vertices_of G \ S by XBOOLE_0:def 5; then A26: the_Vertices_of Gns = the_Vertices_of G \ S by GLIB_000:def 37; Gbs.order() <= k by A3,GLIB_000:75; then A27: Gbs.order() < k by A24,XXREAL_0:1; ex b being Vertex of Gk1 st b in B & b is simplicial proof consider aa being set such that A28: aa in B by XBOOLE_0:def 1; A29: the_Vertices_of Gbs = B \/ S by A20,GLIB_000:def 37; then reconsider a = aa as Vertex of Gbs by A28,XBOOLE_0:def 3; ex c being Vertex of Gbs st c in B & c is simplicial proof per cases; suppose Gbs is complete; then a is simplicial by Th64; hence thesis by A28; end; suppose A30: not Gbs is complete; then not Gbs is trivial; then consider a2,b2 being Vertex of Gbs such that A31: a2 <> b2 and A32: not a2,b2 are_adjacent and A33: a2 is simplicial and A34: b2 is simplicial by A2,A27,A30; now assume that A35: a2 in S and A36: b2 in S; reconsider a4 = a2, b4 = b2 as Vertex of Gs by A35,A36, GLIB_000:def 37; Gs is complete by A7,A8,A9,A35,Th98; then A37: a4,b4 are_adjacent by A31,Def6; reconsider a3 = a2, b3 = b2 as Vertex of G by A35,A36; not a3,b3 are_adjacent by A20,A32,Th45; hence contradiction by A35,A37,Th45; end; then b2 in B or a2 in B by A29,XBOOLE_0:def 3; hence thesis by A33,A34; end; end; then consider cc being Vertex of Gbs such that A38: cc in B and A39: cc is simplicial; reconsider c = cc as Vertex of Gk1 by A19,A38; now let x be set such that A40: x in Gk1.AdjacentSet({c}); assume A41: not x in B\/S; then A42: not x in B by XBOOLE_0:def 3; A43: not x in S by A41,XBOOLE_0:def 3; reconsider x as Vertex of Gk1 by A40; c,x are_adjacent by A40,Th52; then consider e being set such that A44: e Joins c,x,Gk1 by Def3; x in the_Vertices_of Gns by A26,A43,XBOOLE_0:def 5; then e Joins c,x,Gns by A26,A38,A44,Th19; hence contradiction by A38,A42,GLIB_002:10; end; then A45: Gk1.AdjacentSet({c}) c= B\/S by TARSKI:def 3; c in B\/S by A38,XBOOLE_0:def 3; then c is simplicial by A20,A39,A45,Th67; hence thesis by A38; end; then consider b being Vertex of Gk1 such that A46: b in B and A47: b is simplicial; Gas.order() <= k by A3,GLIB_000:75; then A48: Gas.order() < k by A17,XXREAL_0:1; ex a being Vertex of Gk1 st a in A & a is simplicial proof consider aa being set such that A49: aa in A by XBOOLE_0:def 1; A50: the_Vertices_of Gas = A \/ S by A12,GLIB_000:def 37; then reconsider a = aa as Vertex of Gas by A49,XBOOLE_0:def 3; ex c being Vertex of Gas st c in A & c is simplicial proof per cases; suppose Gas is complete; then a is simplicial by Th64; hence thesis by A49; end; suppose A51: not Gas is complete; then not Gas is trivial; then consider a2,b2 being Vertex of Gas such that A52: a2 <> b2 and A53: not a2,b2 are_adjacent and A54: a2 is simplicial and A55: b2 is simplicial by A2,A48,A51; now assume that A56: a2 in S and A57: b2 in S; reconsider a4 = a2, b4 = b2 as Vertex of Gs by A56,A57, GLIB_000:def 37; Gs is complete by A7,A8,A9,A56,Th98; then A58: a4,b4 are_adjacent by A52,Def6; reconsider a3 = a2, b3 = b2 as Vertex of G by A56,A57; not a3,b3 are_adjacent by A12,A53,Th45; hence contradiction by A56,A58,Th45; end; then b2 in A or a2 in A by A50,XBOOLE_0:def 3; hence thesis by A54,A55; end; end; then consider cc being Vertex of Gas such that A59: cc in A and A60: cc is simplicial; reconsider c = cc as Vertex of Gk1 by A11,A59; now let x be set such that A61: x in Gk1.AdjacentSet({c}); assume A62: not x in A\/S; then A63: not x in A by XBOOLE_0:def 3; A64: not x in S by A62,XBOOLE_0:def 3; reconsider x as Vertex of Gk1 by A61; c,x are_adjacent by A61,Th52; then consider e being set such that A65: e Joins c,x,Gk1 by Def3; x in the_Vertices_of Gns by A26,A64,XBOOLE_0:def 5; then e Joins c,x,Gns by A26,A59,A65,Th19; hence contradiction by A59,A63,GLIB_002:10; end; then A66: Gk1.AdjacentSet({c}) c= A\/S by TARSKI:def 3; c in A\/S by A59,XBOOLE_0:def 3; then c is simplicial by A12,A60,A66,Th67; hence thesis by A59; end; then consider a being Vertex of Gk1 such that A67: a in A and A68: a is simplicial; A69: now reconsider aa=a, bb=b as Vertex of Gns by A67,A46; assume a,b are_adjacent; then consider e being set such that A70: e Joins a,b,Gk1 by Def3; e Joins aa,bb,Gns by A26,A70,Th19; then bb in A by A67,GLIB_002:10; hence contradiction by A13,A46,XBOOLE_0:def 4; end; a<>b by A13,A67,A46,XBOOLE_0:def 4; hence thesis by A68,A47,A69; end; A71: for G being finite _Graph holds P[G] from FinGraphOrderCompInd(A1); let G be non trivial finite chordal _Graph; assume not G is complete; hence thesis by A71; end; theorem Th103: for G being finite chordal _Graph ex v being Vertex of G st v is simplicial proof let G be finite chordal _Graph; per cases; suppose A1: G is complete; set u = the Vertex of G; u is simplicial by A1,Th64; hence thesis; end; suppose A2: not G is complete; then not G is trivial; then ex a,b being Vertex of G st a<>b &( not a,b are_adjacent) & a is simplicial & b is simplicial by A2,Th102; hence thesis; end; end; begin :: Vertex Elimination Scheme :: Golumbic, p. 82 definition let G be finite _Graph; mode VertexScheme of G -> FinSequence of the_Vertices_of G means : Def12: it is one-to-one & rng it = the_Vertices_of G; existence proof consider p being FinSequence such that A1: rng p = the_Vertices_of G and A2: p is one-to-one by FINSEQ_4:58; reconsider p as FinSequence of the_Vertices_of G by A1,FINSEQ_1:def 4; take p; thus thesis by A1,A2; end; end; registration let G be finite _Graph; cluster -> non empty for VertexScheme of G; correctness by Def12,RELAT_1:38; end; theorem for G being finite _Graph, S being VertexScheme of G holds len S = card the_Vertices_of G proof let G be finite _Graph, S be VertexScheme of G; A1: S is one-to-one by Def12; rng S = the_Vertices_of G by Def12; hence thesis by A1,FINSEQ_4:62; end; theorem for G being finite _Graph, S being VertexScheme of G holds 1 <= len S by NAT_1:14; theorem Th106: for G, H being finite _Graph, g being VertexScheme of G st G == H holds g is VertexScheme of H proof let G,H be finite _Graph, g be VertexScheme of G such that A1: G == H; rng g = the_Vertices_of G by Def12; then A2: rng g = the_Vertices_of H by A1,GLIB_000:def 34; A3: g is one-to-one by Def12; g is FinSequence of the_Vertices_of H by A1,GLIB_000:def 34; hence thesis by A3,A2,Def12; end; definition let G be finite _Graph, S be VertexScheme of G, x be Vertex of G; redefine func x..S -> non zero Element of NAT; correctness proof rng S = the_Vertices_of G by Def12; hence thesis by FINSEQ_4:21; end; end; definition let G be finite _Graph, S be VertexScheme of G, n be Nat; redefine func S.followSet(n) -> Subset of the_Vertices_of G; coherence proof n in NAT by ORDINAL1:def 12; then A1: rng (n,len S)-cut S c= rng S by GRAPH_2:11; now let x be set; assume x in S.followSet(n); then x in rng S by A1; hence x in the_Vertices_of G by Def12; end; hence thesis by TARSKI:def 3; end; end; theorem Th107: :: NeVSchFol: for G being finite _Graph, S being VertexScheme of G, n being non zero Nat st n <= len S holds S.followSet(n) is non empty proof let G be finite _Graph, S be VertexScheme of G; let n be non zero Nat such that A1: n <= len S; 0+1 <= n by NAT_1:13; then A2: len ((n, len S)-cut S) + n = len S + 1 by A1,GRAPH_2:def 1; len S + 1 - n <> 0 by A1,NAT_1:13; then (n, len S)-cut S <> {} by A2; hence thesis; end; definition let G be finite _Graph, S be VertexScheme of G; attr S is perfect means :Def13: for n being non zero Nat st n <= len S for Gf being inducedSubgraph of G,S.followSet(n) for v being Vertex of Gf st v = S.n holds v is simplicial; end; :: finite is needed unless we add loopless theorem Th108: for G being finite trivial _Graph, v being Vertex of G ex S being VertexScheme of G st S = <*v*> & S is perfect proof let G be finite trivial _Graph, v being Vertex of G; consider v1 being Vertex of G such that A1: the_Vertices_of G = {v1} by GLIB_000:22; set S = <*v*>; v1 = v by A1,TARSKI:def 1; then A2: rng S = the_Vertices_of G by A1,FINSEQ_1:39; S is one-to-one by FINSEQ_3:93; then reconsider S as VertexScheme of G by A2,Def12; take S; thus S = <*v*>; let n be non zero Nat such that n <= len S; let Gf be inducedSubgraph of G,S.followSet(n); thus thesis by Th65; end; theorem for G being finite _Graph, V being VertexScheme of G holds V is perfect iff for a,b,c being Vertex of G st b<>c & a,b are_adjacent & a,c are_adjacent for va,vb,vc being Nat st va in dom V & vb in dom V & vc in dom V & V.va = a & V.vb = b & V.vc = c & va < vb & va < vc holds b,c are_adjacent proof let G be finite _Graph, V be VertexScheme of G; A1: V is one-to-one by Def12; A2: now let a,b,c be Vertex of G such that A3: b<>c and A4: a,b are_adjacent and A5: a,c are_adjacent and A6: not b,c are_adjacent; let va,vb,vc be Nat such that A7: va in dom V and A8: vb in dom V and A9: vc in dom V and A10: V.va=a and A11: V.vb=b and A12: V.vc=c and A13: va < vb and A14: va < vc; set Gf = the inducedSubgraph of G,V.followSet(va); set fs = (va,len V)-cut V; A15: va <= len V by A7,FINSEQ_3:25; then A16: va - va <= len V - va by XREAL_1:9; A17: 1 <= va by A7,FINSEQ_3:25; then A18: len fs + va - va = len V + 1 - va by A15,GRAPH_2:def 1; then A19: len fs = len V - va + 1; then 0+1 <= len fs by A16,NAT_1:13; then A20: 0+1 in dom fs by FINSEQ_3:25; fs.(0+1) = V.(va + 0) by A17,A15,A19,A16,GRAPH_2:def 1; then a in V.followSet(va) by A10,A20,FUNCT_1:3; then reconsider ag=a as Vertex of Gf by GLIB_000:def 37; consider jc being Nat such that A21: va + jc = vc by A14,NAT_1:10; A22: 0+1 <= jc+1 by XREAL_1:7; A23: now assume jc >= len fs; then va + jc >= len V + 1 - va + va by A18,XREAL_1:7; then vc > len V by A21,NAT_1:13; hence contradiction by A9,FINSEQ_3:25; end; then jc+1 <= len fs by NAT_1:13; then A24: jc+1 in dom fs by A22,FINSEQ_3:25; fs.(jc+1) = V.(va + jc) by A17,A15,A23,GRAPH_2:def 1; then c in V.followSet(va) by A12,A21,A24,FUNCT_1:3; then reconsider cg=c as Vertex of Gf by GLIB_000:def 37; A25: V.followSet(va) is non empty by A17,A15,Th107; then A26: ag,cg are_adjacent by A5,Th45; consider jb being Nat such that A27: va + jb = vb by A13,NAT_1:10; A28: 0+1 <= jb+1 by XREAL_1:7; A29: now assume jb >= len fs; then va + jb >= len V + 1 - va + va by A18,XREAL_1:7; then vb > len V by A27,NAT_1:13; hence contradiction by A8,FINSEQ_3:25; end; then jb+1 <= len fs by NAT_1:13; then A30: jb+1 in dom fs by A28,FINSEQ_3:25; fs.(jb+1) = V.(va + jb) by A17,A15,A29,GRAPH_2:def 1; then b in V.followSet(va) by A11,A27,A30,FUNCT_1:3; then reconsider bg=b as Vertex of Gf by GLIB_000:def 37; A31: not bg,cg are_adjacent by A6,A25,Th45; assume V is perfect; then A32: ag is simplicial by A10,A17,A15,Def13; a <> c by A1,A7,A9,A10,A12,A14,FUNCT_1:def 4; then A33: cg in Gf.AdjacentSet({ag}) by A26,Th52; ag,bg are_adjacent by A4,A25,Th45; then bg in Gf.AdjacentSet({ag}) by A26,A31,Th52; then ex e being set st e Joins bg,cg,Gf by A3,A32,A33,Th68; hence contradiction by A31,Def3; end; A34: rng V = the_Vertices_of G by Def12; now assume not V is perfect; then not (for n being non zero Nat st n <= len V for Gf being inducedSubgraph of G,V.followSet(n) for v being Vertex of Gf st v = V.n holds v is simplicial) by Def13; then consider n being non zero Nat, Gf being (inducedSubgraph of G,V.followSet( n)), v being Vertex of Gf such that A35: n <= len V and A36: v = V.n and A37: not v is simplicial; A38: V.followSet(n) is non empty Subset of the_Vertices_of G by A35,Th107; then A39: the_Vertices_of Gf = V.followSet(n) by GLIB_000:def 37; then reconsider vg=v as Vertex of G by TARSKI:def 3; consider a,b being Vertex of Gf such that A40: a<>b and A41: v<>a and A42: v<>b and A43: v,a are_adjacent and A44: v,b are_adjacent and A45: not a,b are_adjacent by A37,Th69; reconsider ag=a, bg=b as Vertex of G by A39,TARSKI:def 3; A46: vg,bg are_adjacent by A44,A38,Th45; 1 <= n by Th1; then A47: n in dom V by A35,FINSEQ_3:25; b in the_Vertices_of G by A39,TARSKI:def 3; then consider vb being Nat such that A48: vb in dom V and A49: V.vb = b by A34,FINSEQ_2:10; A50: b in rng V by A34,A39,TARSKI:def 3; A51: now assume vb <= n; then A52: vb < n by A36,A42,A49,XXREAL_0:1; b..V >= n by A1,A47,A39,A50,Th16; then vb < b..V by A52,XXREAL_0:2; hence contradiction by A48,A49,FINSEQ_4:24; end; a in the_Vertices_of G by A39,TARSKI:def 3; then consider va being Nat such that A53: va in dom V and A54: V.va = a by A34,FINSEQ_2:10; A55: a in rng V by A34,A39,TARSKI:def 3; A56: now assume va <= n; then A57: va < n by A36,A41,A54,XXREAL_0:1; a..V >= n by A1,A47,A39,A55,Th16; then va < a..V by A57,XXREAL_0:2; hence contradiction by A53,A54,FINSEQ_4:24; end; A58: not ag,bg are_adjacent by A45,A38,Th45; vg,ag are_adjacent by A43,A38,Th45; hence ex a,b,c being Vertex of G, va,vb,vc being Nat st b<>c & a,b are_adjacent & a,c are_adjacent & va in dom V & vb in dom V & vc in dom V & V. va = a & V.vb = b & V.vc = c & va < vb & va < vc & not b,c are_adjacent by A36 ,A47,A40,A46,A58,A53,A54,A48,A49,A56,A51; end; hence thesis by A2; end; :: Golubmic pg 83-84, Theorem 4.1 (i) ==> (ii) registration let G be finite chordal _Graph; cluster perfect for VertexScheme of G; existence proof defpred P[finite _Graph] means $1 is chordal implies ex S being VertexScheme of $1 st S is perfect; A1: now let k be non zero Nat such that A2: for Gk being finite _Graph st Gk.order() < k holds P[Gk]; let Gk1 be finite _Graph such that A3: Gk1.order() = k; thus P[Gk1] proof assume A4: Gk1 is chordal; per cases; suppose A5: k = 1; set v = the Vertex of Gk1; Gk1 is trivial by A3,A5,GLIB_000:26; then ex S being VertexScheme of Gk1 st S = <*v*> & S is perfect by Th108; hence thesis; end; suppose k <> 1; then reconsider G=Gk1 as non trivial finite chordal _Graph by A3,A4, GLIB_000:26; consider x being Vertex of G such that A6: x is simplicial by Th103; set H = the removeVertex of G,x; A7: <*x*> is one-to-one by FINSEQ_3:93; A8: the_Vertices_of G\{x} is non empty by GLIB_000:20; then A9: the_Vertices_of H=the_Vertices_of G\{x} by GLIB_000:def 37; H.order() = card (the_Vertices_of G\{x}) by A8,GLIB_000:def 37 .= G.order() - card {x} by CARD_2:44 .= k - 1 by A3,CARD_2:42; then consider T being VertexScheme of H such that A10: T is perfect by A2,XREAL_1:146; {x} /\ rng T = {x} /\ (the_Vertices_of G\{x}) by A9,Def12 .= ({x} /\ the_Vertices_of G) \ {x} by XBOOLE_1:49 .= {x} \ {x} by XBOOLE_1:28 .= {} by XBOOLE_1:37; then {x} misses rng T by XBOOLE_0:def 7; then A11: rng <*x*> misses rng T by FINSEQ_1:38; set S = <*x*>^T; rng T = the_Vertices_of G\{x} by A9,Def12; then rng S = the_Vertices_of G\{x} \/ rng <*x*> by FINSEQ_1:31; then rng S = the_Vertices_of G\{x} \/ {x} by FINSEQ_1:38; then rng S = {x} \/ the_Vertices_of G by XBOOLE_1:39; then A12: rng S = the_Vertices_of G by XBOOLE_1:12; then reconsider S as FinSequence of the_Vertices_of G by FINSEQ_1:def 4; T is one-to-one by Def12; then S is one-to-one by A11,A7,FINSEQ_3:91; then reconsider S as VertexScheme of Gk1 by A12,Def12; take S; let n be non zero Nat such that A13: n <= len S; A14: 1 <= n by NAT_1:14; let Gf be inducedSubgraph of Gk1,S.followSet(n); let v be Vertex of Gf such that A15: v = S.n; per cases by A14,XXREAL_0:1; suppose A16: 1 = n; then A17: S.followSet(n) = rng S by GRAPH_2:7 .= the_Vertices_of G by Def12; x = v by A15,A16,FINSEQ_1:41; hence thesis by A6,A17,Th66,GLIB_000:94; end; suppose A18: 1 < n; then 1+(-1) < n+(-1) by XREAL_1:8; then reconsider n1 = n - 1 as non zero Element of NAT by INT_1:3; len <*x*> = 1 by FINSEQ_1:39; then A19: S.n = T.n1 by A13,A18,FINSEQ_1:24; A20: T.followSet(n1) = S.followSet(n1+1) by Th17; n+(-1) <= len S+(-1) by A13,XREAL_1:7; then n1 <= len <*x*> + len T + (-1) by FINSEQ_1:22; then A21: n1 <= 1 + len T + (-1) by FINSEQ_1:39; then T.followSet(n1) is non empty by Th107; then Gf is inducedSubgraph of H,T.followSet(n1) by A9,A20,Th30; hence thesis by A10,A15,A19,A21,Def13; end; end; end; end; for G being finite _Graph holds P[G] from FinGraphOrderCompInd(A1 ); then consider S being VertexScheme of G such that A22: S is perfect; take S; thus thesis by A22; end; end; theorem for G, H being finite chordal _Graph, g being perfect VertexScheme of G st G == H holds g is perfect VertexScheme of H proof let G,H be finite chordal _Graph, g be perfect VertexScheme of G such that A1: G == H; reconsider h=g as VertexScheme of H by A1,Th106; now let n be non zero Nat such that A2: n <= len h; let Hf be inducedSubgraph of H,h.followSet(n); let vh be Vertex of Hf such that A3: vh = h.n; G.edgesBetween(g.followSet(n)) = H.edgesBetween(g.followSet(n)) by A1, GLIB_000:90; then reconsider Gf = Hf as inducedSubgraph of G,g.followSet(n) by A1, GLIB_000:95; reconsider vg = vh as Vertex of Gf; vg is simplicial by A2,A3,Def13; hence vh is simplicial; end; hence thesis by Def13; end; :: Chordal41c: :: Golubmic pg 83-84, Theorem 4.1 (ii) ==> (i) theorem for G being finite _Graph st ex S being VertexScheme of G st S is perfect holds G is chordal proof let G be finite _Graph; given S being VertexScheme of G such that A1: S is perfect; A2: rng S = the_Vertices_of G by Def12; let P be Walk of G such that A3: P.length() > 3 and A4: P is Cycle-like; P.vertices() is non empty by GLIB_001:88; then consider x being set such that A5: x in P.vertices() and A6: for y being set st y in P.vertices() holds x..S <= y..S by A2,Th15; reconsider x as Vertex of G by A5; set n = x..S; set H = the inducedSubgraph of G,S.followSet(n); A7: rng S = the_Vertices_of G by Def12; then A8: n in dom S by FINSEQ_4:20; A9: S is one-to-one by Def12; then x in S.followSet(n) by A7,A8,Th16; then reconsider y=x as Vertex of H by GLIB_000:def 37; A10: S.followSet(n) is non empty by A7,Th107,FINSEQ_4:21; now let y be set such that A11: y in P.vertices(); reconsider z=y as Vertex of G by A11; x..S <= z..S by A6,A11; hence y in S.followSet(n) by A7,A8,A9,Th16; end; then P.vertices() c= S.followSet(n) by TARSKI:def 3; then reconsider C=P as Walk of H by A10,Th23; reconsider C as Path of H by A4,GLIB_001:176; A12: C is closed by A4,GLIB_001:176; A13: y in C.vertices() by A5,GLIB_001:98; A14: rng S = the_Vertices_of G by Def12; then A15: S.n = x by FINSEQ_4:19; C is non trivial by A4,GLIB_001:176; then A16: C is Cycle-like by A12,GLIB_001:def 31; C.length() > 3 by A3,GLIB_001:114; then consider a,b being odd Nat such that A17: a+2 < b and A18: b <= len C and A19: C.a <> C.b and A20: C.a in H.AdjacentSet({y}) and A21: C.b in H.AdjacentSet({y}) and A22: for e being set st e in C.edges() holds not e Joins C.a,C.b,H by A16,A13 ,Th55; n <= len S by A14,FINSEQ_4:21; then y is simplicial by A1,A15,Def13; then ex e being set st e Joins C.a,C.b,H by A19,A20,A21,Th68; then C is chordal by A17,A18,A19,A22,Def10; hence thesis by A10,Th87; end;