:: Chordal Graphs :: by Broderick Arneson and Piotr Rudnicki :: :: Received August 18, 2006 :: Copyright (c) 2006-2021 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, FINSEQ_6; constructors DOMAIN_1, REAL_1, NAT_D, FINSEQ_4, GRAPH_2, GLIB_001, GLIB_002, VALUED_1, XXREAL_2, RELSET_1, NUMBERS, FINSEQ_6; 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, GLIB_001, GLIB_002, FUNCT_2, XXREAL_2, CARD_1, RELSET_1, FINSEQ_6; requirements ARITHM, BOOLE, NUMERALS, REAL, SUBSET; begin :: Preliminaries theorem :: CHORD:1 for n being non zero Nat holds n-1 is Nat & 1 <= n; theorem :: CHORD:2 :: Nat02 for n being odd Nat holds n-1 is Nat & 1 <= n; theorem :: CHORD:3 :: EvenOdd02 for n,m being odd Integer st n < m holds n <= m-2; theorem :: CHORD:4 :: EvenOdd03: for n,m being odd Integer st m < n holds m+2 <= n; theorem :: CHORD:5 :: EvenOdd04: for n being odd Nat st 1 <> n ex m being odd Nat st m+2 = n; theorem :: CHORD:6 :: Odd100 for n being odd Nat st n<=2 holds n=1; theorem :: CHORD:7 :: Odd101 for n being odd Nat st n<=4 holds n=1 or n=3; theorem :: CHORD:8 :: Odd102 for n being odd Nat st n<=6 holds n=1 or n=3 or n=5; theorem :: CHORD:9 for n being odd Nat st n<=8 holds n=1 or n=3 or n=5 or n=7; theorem :: CHORD:10 :: Even100 for n being even Nat st n<=1 holds n=0; theorem :: CHORD:11 :: Even101 for n being even Nat st n<=3 holds n=0 or n=2; theorem :: CHORD:12 :: Even102 for n being even Nat st n<=5 holds n=0 or n=2 or n=4; theorem :: CHORD:13 :: Even103 for n being even Nat st n<=7 holds n=0 or n=2 or n=4 or n=6; theorem :: CHORD:14 for p being FinSequence, n being non zero Nat st p is one-to-one & n <= len p holds (p.n)..p = n; theorem :: CHORD:15 :: 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 ; definition let p be FinSequence, n be Nat; func p.followSet(n) -> finite set equals :: CHORD:def 1 rng (n,len p)-cut p; end; theorem :: CHORD:16 :: 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; theorem :: CHORD:17 :: 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); theorem :: CHORD:18 :: 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; begin :: Miscellany on graphs theorem :: CHORD:19 for G being _Graph, S being Subset of the_Vertices_of G for H being inducedSubgraph of G,S for u,v being object st u in S & v in S for e being object st e Joins u,v,G holds e Joins u,v,H; theorem :: CHORD:20 for G being _Graph, W being Walk of G holds W is Trail-like iff len W = 2*(card W.edges())+1; theorem :: CHORD:21 :: 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; theorem :: CHORD:22 :: 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; theorem :: CHORD:23 :: 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; theorem :: CHORD:24 :: 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; theorem :: CHORD:25 :: 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; theorem :: CHORD:26 for G being _Graph, P being Path of G st P is open for a,e,b being set st not a in P.vertices() & b = P.first() & e Joins a,b,G holds G.walkOf(a,e,b) .append(P) is Path-like; theorem :: CHORD:27 :: 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; theorem :: CHORD:28 for G being _Graph, W1,W2 being Walk of G st W1.last() = W2 .first() holds W1.append(W2).length() = W1.length() + W2.length(); theorem :: CHORD:29 :: 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; theorem :: CHORD:30 :: 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; theorem :: CHORD:31 :: 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); :: we do not consider infinite graphs scheme :: CHORD:sch 1 FinGraphOrderCompInd{P[set]}: for G being _finite _Graph holds P[G] provided 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]; :: should be in GLIBs theorem :: CHORD:32 for G being _Graph, W being Walk of G st W is open & W is Path-like holds W is vertex-distinct; :: PathLike15 :: should be in GLIB theorem :: CHORD:33 for G being _Graph, P being Path of G st P is open & len P > 3 for e being object st e Joins P.last(),P.first(),G holds P.addEdge(e) is Cycle-like; begin :: Shortest topological path definition let G be _Graph, W be Walk of G; attr W is minlength means :: CHORD:def 2 for W2 being Walk of G st W2 is_Walk_from W .first(),W.last() holds len W2 >= len W; end; theorem :: CHORD:34 :: 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; theorem :: CHORD:35 :: LenSubwalk00 for G being _Graph, W being Walk of G, S being Subwalk of W st len S = len W holds S = W; theorem :: CHORD:36 for G being _Graph, W being Walk of G st W is minlength holds W is Path-like; ::$CT theorem :: CHORD:38 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; theorem :: CHORD:39 :: 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; theorem :: CHORD:40 :: 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 object st e Joins W.m,W.n,G; theorem :: CHORD:41 :: 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 object st e Joins W.m,W.n,G; theorem :: CHORD:42 :: 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; theorem :: CHORD:43 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; begin :: Adjacency and complete graphs definition let G be _Graph, a,b be Vertex of G; pred a,b are_adjacent means :: CHORD:def 3 :: DefAdjacent ex e being object st e Joins a,b,G; symmetry; end; theorem :: CHORD:44 :: 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; theorem :: CHORD:45 :: 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; theorem :: CHORD:46 :: 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; theorem :: CHORD:47 :: 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 object 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; theorem :: CHORD:48 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; definition let G be _Graph, S be set; func G.AdjacentSet(S) -> Subset of the_Vertices_of G equals :: CHORD:def 4 {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 )}; end; theorem :: CHORD:49 for G being _Graph, S, x being set st x in G.AdjacentSet(S) holds not x in S; theorem :: CHORD:50 :: 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; theorem :: CHORD:51 :: Adjacent01 for G1,G2 being _Graph st G1 == G2 for S being set holds G1 .AdjacentSet(S) = G2.AdjacentSet(S); theorem :: CHORD:52 :: AdjacentV00 for G being _Graph, u,v being Vertex of G holds u in G .AdjacentSet({v}) iff u <> v & v,u are_adjacent; theorem :: CHORD:53 for G being _Graph, x,y being set holds x in G.AdjacentSet({y}) iff y in G.AdjacentSet({x}); theorem :: CHORD:54 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}) ; theorem :: CHORD:55 :: 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 object st e in C.edges() holds not e Joins C.m,C.n,G; :: 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 :: CHORD:56 :: AdjacentV01: for G being loopless _Graph, u being Vertex of G holds G.AdjacentSet({ u}) = {} iff u is isolated; theorem :: CHORD:57 :: 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; theorem :: CHORD:58 :: 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}); :: Adjacency set as a subgraph of G definition let G be _Graph, S be set; mode AdjGraph of G,S -> Subgraph of G means :: CHORD:def 5 it is inducedSubgraph of G,G.AdjacentSet(S) if S is Subset of the_Vertices_of G; end; theorem :: CHORD:59 :: 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; theorem :: CHORD:60 :: 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; definition let G be _Graph; attr G is complete means :: CHORD:def 6 for u,v being Vertex of G st u <> v holds u, v are_adjacent; end; theorem :: CHORD:61 :: Completetr for G being _Graph st G is _trivial holds G is complete; registration cluster _trivial -> complete for _Graph; end; registration cluster _trivial simple complete for _Graph; cluster non _trivial _finite simple complete for _Graph; end; theorem :: CHORD:62 :: Complete00 for G1,G2 being _Graph st G1 == G2 holds G1 is complete implies G2 is complete; theorem :: CHORD:63 :: 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; begin :: Simplicial vertex :: Golumbic p. 81 definition let G be _Graph, v be Vertex of G; attr v is simplicial means :: CHORD:def 7 G.AdjacentSet({v}) <> {} implies for G2 being AdjGraph of G,{v} holds G2 is complete; end; theorem :: CHORD:64 :: Simplicial0 for G being complete _Graph, v being Vertex of G holds v is simplicial; theorem :: CHORD:65 :: Simplicial01 for G being _trivial _Graph, v being Vertex of G holds v is simplicial; theorem :: CHORD:66 :: 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; theorem :: CHORD:67 :: 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; theorem :: CHORD:68 :: Simplicial03 for G being _Graph, v being Vertex of G st v is simplicial for a,b being object st a<>b & a in G.AdjacentSet({v}) & b in G.AdjacentSet({v}) holds ex e being object st e Joins a,b,G; theorem :: CHORD:69 :: 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; begin :: Vertex separator :: Golumbic, p. 84 definition let G be _Graph, a,b be Vertex of G; assume that a<>b and not a,b are_adjacent; mode VertexSeparator of a,b -> Subset of the_Vertices_of G means :: CHORD:def 8 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); end; theorem :: CHORD:70 :: 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; :: alternate characterization of Vertex Separator theorem :: CHORD:71 :: 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()); theorem :: CHORD:72 :: 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; theorem :: CHORD:73 :: 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; theorem :: CHORD:74 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; theorem :: CHORD:75 :: 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 = {}; theorem :: CHORD:76 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) = {}; theorem :: CHORD:77 :: 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; definition let G be _Graph, a,b be Vertex of G; let S be VertexSeparator of a,b; attr S is minimal means :: CHORD:def 9 for T being Subset of S st T <> S holds not T is VertexSeparator of a,b; end; theorem :: CHORD:78 :: VS000 for G being _Graph, a,b being Vertex of G for S being VertexSeparator of a,b st S = {} holds S is minimal; theorem :: CHORD:79 :: minVSexistance for G being _finite _Graph for a,b being Vertex of G ex S being VertexSeparator of a,b st S is minimal; theorem :: CHORD:80 :: 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; theorem :: CHORD:81 :: 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(); theorem :: CHORD:82 :: 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 ; theorem :: CHORD:83 :: 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 ; 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 :: CHORD:def 10 ex m, n being odd Nat st m+2 < n & n <= len W & W.m <> W.n & (ex e being object st e Joins W.m,W.n,G) & for f being object 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 :: CHORD:84 :: 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 object 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)); theorem :: CHORD:85 :: 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 object 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; theorem :: CHORD:86 :: 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; theorem :: CHORD:87 :: 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; theorem :: CHORD:88 for G being _Graph, W being Walk of G st W is Cycle-like & W is chordal & W.length()=4 ex e being object st e Joins W.1,W.5,G or e Joins W.3,W.7,G; theorem :: CHORD:89 :: MinChordal01 for G being _Graph, W being Walk of G st W is minlength holds W is chordless; theorem :: CHORD:90 for G being _Graph, W being Walk of G st len W = 5 & not W.first(),W .last() are_adjacent holds W is chordless; theorem :: CHORD:91 for G being _Graph, W being Walk of G holds W is chordal iff W .reverse() is chordal; theorem :: CHORD:92 :: 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 object st e Joins P.m,P.n,G) iff m+2 = n; theorem :: CHORD:93 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; theorem :: CHORD:94 for G being _Graph, S being non empty Subset of the_Vertices_of G, H being (inducedSubgraph of G,S), W being Walk of G, V being Walk of H st W = V holds W is chordless iff V is chordless; definition let G be _Graph; attr G is chordal means :: CHORD:def 11 for P being Walk of G st P.length() > 3 & P is Cycle-like holds P is chordal; end; theorem :: CHORD:95 :: Chordal01 for G1,G2 being _Graph st G1 == G2 holds G1 is chordal implies G2 is chordal; theorem :: CHORD:96 :: Chordal02 for G being _finite _Graph st card the_Vertices_of G <= 3 holds G is chordal; registration cluster _trivial _finite chordal for _Graph; cluster non _trivial _finite simple chordal for _Graph; cluster complete -> chordal for _Graph; end; registration let G be chordal _Graph, V be set; cluster -> chordal for inducedSubgraph of G,V; end; theorem :: CHORD:97 for G being chordal _Graph, P being Path of G st P is open & P is chordless for x,e being object st (not x in P.vertices() & e Joins P.last(),x,G & not ex f being object 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; :: Golumbic, page 83. Theorem 4.1 (i) ==> (iii) theorem :: CHORD:98 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; :: Golumbic, page 83, Theorem 4.1 (iii)->(i) theorem :: CHORD:99 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; :: Exercise 12, p. 101. :: This needs "finite-branching", we do it for finite though theorem :: CHORD:100 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; theorem :: CHORD:101 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; :: Golumbic, page 83, Lemma 4.2. theorem :: CHORD:102 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; theorem :: CHORD:103 for G being _finite chordal _Graph ex v being Vertex of G st v is simplicial; begin :: Vertex Elimination Scheme :: Golumbic, p. 82 definition let G be _finite _Graph; mode VertexScheme of G -> FinSequence of the_Vertices_of G means :: CHORD:def 12 it is one-to-one & rng it = the_Vertices_of G; end; registration let G be _finite _Graph; cluster -> non empty for VertexScheme of G; end; theorem :: CHORD:104 for G being _finite _Graph, S being VertexScheme of G holds len S = card the_Vertices_of G; theorem :: CHORD:105 for G being _finite _Graph, S being VertexScheme of G holds 1 <= len S; theorem :: CHORD:106 for G, H being _finite _Graph, g being VertexScheme of G st G == H holds g is VertexScheme of H; 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; 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; end; theorem :: CHORD:107 :: 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; definition let G be _finite _Graph, S be VertexScheme of G; attr S is perfect means :: CHORD:def 13 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 :: CHORD:108 for G being _finite _trivial _Graph, v being Vertex of G ex S being VertexScheme of G st S = <*v*> & S is perfect; theorem :: CHORD:109 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; :: Golubmic pg 83-84, Theorem 4.1 (i) ==> (ii) registration let G be _finite chordal _Graph; cluster perfect for VertexScheme of G; end; theorem :: CHORD:110 for G, H being _finite chordal _Graph, g being perfect VertexScheme of G st G == H holds g is perfect VertexScheme of H; :: Chordal41c: :: Golubmic pg 83-84, Theorem 4.1 (ii) ==> (i) theorem :: CHORD:111 for G being _finite _Graph st ex S being VertexScheme of G st S is perfect holds G is chordal;