:: Chordal Graphs
:: by Broderick Arneson and Piotr Rudnicki
::
:: Received August 18, 2006
:: Copyright (c) 2006-2012 Association of Mizar Users


begin

theorem Th1: :: CHORD:1
for n being non zero Nat holds
( n - 1 is Nat &amp; 1 <= n )
proofend;

theorem Th2: :: CHORD:2
for n being odd Nat holds
( n - 1 is Nat &amp; 1 <= n ) by Th1;

Lm1:  for a, b, c being Integer st a + 2 < b holds
((c - b) + 1) + 2 < (c - a) + 1
proofend;

theorem Th3: :: CHORD:3
for n, m being odd Integer st n < m holds
n <= m - 2
proofend;

theorem Th4: :: CHORD:4
for n, m being odd Integer st m < n holds
m + 2 <= n
proofend;

theorem Th5: :: CHORD:5
for n being odd Nat st 1 <> n holds
ex m being odd Nat st m + 2 = n
proofend;

theorem Th6: :: CHORD:6
for n being odd Nat st n <= 2 holds
n = 1
proofend;

theorem Th7: :: CHORD:7
for n being odd Nat holds
( not n <= 4 or n = 1 or n = 3 )
proofend;

theorem Th8: :: CHORD:8
for n being odd Nat holds
( not n <= 6 or n = 1 or n = 3 or n = 5 )
proofend;

theorem :: CHORD:9
for n being odd Nat holds
( not n <= 8 or n = 1 or n = 3 or n = 5 or n = 7 )
proofend;

theorem Th10: :: CHORD:10
for n being even Nat st n <= 1 holds
n = 0
proofend;

theorem Th11: :: CHORD:11
for n being even Nat holds
( not n <= 3 or n = 0 or n = 2 )
proofend;

theorem Th12: :: CHORD:12
for n being even Nat holds
( not n <= 5 or n = 0 or n = 2 or n = 4 )
proofend;

theorem Th13: :: CHORD:13
for n being even Nat holds
( not n <= 7 or n = 0 or n = 2 or n = 4 or n = 6 )
proofend;

Lm2:  for i, j being odd Nat st i <= j holds
ex k being Nat st i + (2 * k) = j
proofend;

theorem :: CHORD:14
for p being FinSequence
for n being non zero Nat st p is one-to-one &amp; n <= len p holds
(p . n) .. p = n
proofend;

theorem Th15: :: CHORD:15
for p being non empty FinSequence
for T being non empty Subset of (rng p) ex x being set st
( x in T &amp; ( for y being set st y in T holds
x .. p <= y .. p ) )
proofend;

definition
let p be FinSequence;
let n be Nat;
funcp .followSet n ->  finite set  equals :: CHORD:def 1
 rng ((n,(len p)) -cut p);
correctness
coherence
rng ((n,(len p)) -cut p) is finite set ;
;
end;

:: deftheorem  defines .followSet CHORD:def_1_:_
 for p being FinSequence
for n being Nat holds p .followSet n = rng ((n,(len p)) -cut p);

theorem Th16: :: CHORD:16
for p being FinSequence
for x being set
for n being Nat st x in rng p &amp; n in dom p &amp; p is one-to-one holds
( x in p .followSet n iff x .. p >= n )
proofend;

theorem Th17: :: CHORD:17
for p, q being FinSequence
for x being set st p = <*x*> ^ q holds
for n being non zero Nat holds p .followSet (n + 1) = q .followSet n
proofend;

theorem Th18: :: CHORD:18
for X being set
for f being FinSequence of X
for g being Subset of f st len (Seq g) = len f holds
Seq g = f
proofend;

begin

theorem Th19: :: CHORD:19
for G being _Graph
for S being Subset of (the_Vertices_of G)
for H being inducedSubgraph of G,S
for u, v being set st u in S &amp; v in S holds
for e being set st e Joins u,v,G holds
e Joins u,v,H
proofend;

theorem :: CHORD:20
for G being _Graph
for W being Walk of G holds
( W is Trail-like iff len W = (2 * (card (W .edges()))) + 1 )
proofend;

theorem Th21: :: CHORD:21
for G being _Graph
for 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
proofend;

theorem Th22: :: CHORD:22
for G being _Graph
for a, b being set st a <> b holds
for W being Walk of G st W .vertices() = {a,b} holds
ex e being set st e Joins a,b,G
proofend;

theorem Th23: :: CHORD:23
for G being _Graph
for 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
proofend;

theorem Th24: :: CHORD:24
for G1, G2 being _Graph st G1 == G2 holds
for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 &amp; W1 is Cycle-like holds
W2 is Cycle-like
proofend;

theorem Th25: :: CHORD:25
for G being _Graph
for P being Path of G
for m, n being odd Nat st m <= len P &amp; n <= len P &amp; P . m = P . n &amp; not m = n &amp; not ( m = 1 &amp; n = len P ) holds
( m = len P &amp; n = 1 )
proofend;

theorem :: CHORD:26
for G being _Graph
for P being Path of G st P is open holds
for a, e, b being set st not a in P .vertices() &amp; b = P .first() &amp; e Joins a,b,G holds
(G .walkOf (a,e,b)) .append P is Path-like
proofend;

theorem Th27: :: CHORD:27
for G being _Graph
for P, H being Path of G st P .edges() misses H .edges() &amp; P is open &amp; not H is trivial &amp; H is open &amp; (P .vertices()) /\ (H .vertices()) = {(P .first()),(P .last())} &amp; H .first() = P .last() &amp; H .last() = P .first() holds
P .append H is Cycle-like
proofend;

theorem Th28: :: CHORD:28
for G being _Graph
for W1, W2 being Walk of G st W1 .last() = W2 .first() holds
(W1 .append W2) .length() = (W1 .length()) + (W2 .length())
proofend;

theorem Th29: :: CHORD:29
for G being _Graph
for A, B being non empty Subset of (the_Vertices_of G) st B c= A holds
for H1 being inducedSubgraph of G,A
for H2 being inducedSubgraph of H1,B holds H2 is inducedSubgraph of G,B
proofend;

theorem Th30: :: CHORD:30
for G being _Graph
for A, B being non empty Subset of (the_Vertices_of G) st B c= A holds
for H1 being inducedSubgraph of G,A
for H2 being inducedSubgraph of G,B holds H2 is inducedSubgraph of H1,B
proofend;

theorem Th31: :: CHORD:31
for G being _Graph
for S, T being non empty Subset of (the_Vertices_of G) st T c= S holds
for G2 being inducedSubgraph of G,S holds G2 .edgesBetween T = G .edgesBetween T
proofend;

scheme :: CHORD:sch 1
FinGraphOrderCompInd{ P1[ set ] } :
 for G being finite _Graph holds P1[G]
provided
A1: for k being non zero Nat st ( for Gk being finite _Graph st Gk .order() < k holds
P1[Gk] ) holds
for Gk1 being finite _Graph st Gk1 .order() = k holds
P1[Gk1]
proofend;

:: should be in GLIBs
theorem Th32: :: CHORD:32
for G being _Graph
for W being Walk of G st W is open &amp; W is Path-like holds
W is vertex-distinct
proofend;

:: PathLike15
:: should be in GLIB
theorem Th33: :: CHORD:33
for G being _Graph
for P being Path of G st P is open &amp; len P > 3 holds
for e being set st e Joins P .last() ,P .first() ,G holds
P .addEdge e is Cycle-like
proofend;

begin

definition
let G be _Graph;
let W be Walk of G;
attrW is minlength  means :Def2: :: CHORD:def 2
 for W2 being Walk of G st W2 is_Walk_from W .first() ,W .last() holds
len W2 >= len W;
end;

:: deftheorem Def2 defines minlength CHORD:def_2_:_
 for G being _Graph
for W being Walk of G holds
( W is minlength iff for W2 being Walk of G st W2 is_Walk_from W .first() ,W .last() holds
len W2 >= len W );

theorem Th34: :: CHORD:34
for G being _Graph
for W being Walk of G
for S being Subwalk of W st S .first() = W .first() &amp; S .edgeSeq() = W .edgeSeq() holds
S = W
proofend;

theorem Th35: :: CHORD:35
for G being _Graph
for W being Walk of G
for S being Subwalk of W st len S = len W holds
S = W
proofend;

theorem :: CHORD:36
for G being _Graph
for W being Walk of G st W is minlength holds
W is Path-like
proofend;

theorem :: CHORD:37
for G being _Graph
for W being Walk of G st W is minlength holds
W is Path-like
proofend;

theorem Th38: :: CHORD:38
for G being _Graph
for W being Walk of G st ( for P being Path of G st P is_Walk_from W .first() ,W .last() holds
len P >= len W ) holds
W is minlength
proofend;

theorem Th39: :: CHORD:39
for G being _Graph
for W being Walk of G ex P being Path of G st
( P is_Walk_from W .first() ,W .last() &amp; P is minlength )
proofend;

theorem Th40: :: CHORD:40
for G being _Graph
for W being Walk of G st W is minlength holds
for m, n being odd Nat st m + 2 < n &amp; n <= len W holds
for e being set holds not e Joins W . m,W . n,G
proofend;

theorem Th41: :: CHORD:41
for G being _Graph
for 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 holds
for m, n being odd Nat st m + 2 < n &amp; n <= len W holds
for e being set holds not e Joins W . m,W . n,G
proofend;

theorem Th42: :: CHORD:42
for G being _Graph
for W being Walk of G st W is minlength holds
for m, n being odd Nat st m <= n &amp; n <= len W holds
W .cut (m,n) is minlength
proofend;

theorem :: CHORD:43
for G being _Graph st G is connected holds
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 &amp; not P is trivial &amp; P .first() in A &amp; P .last() in B &amp; ( for n being odd Nat st 1 < n &amp; n < len P holds
( not P . n in A &amp; not P . n in B ) ) )
proofend;

begin

definition
let G be _Graph;
let a, b be Vertex of G;
preda,b are_adjacent  means :Def3: :: CHORD:def 3
 ex e being set st e Joins a,b,G;
symmetry
 for a, b being Vertex of G st ex e being set st e Joins a,b,G holds
ex e being set st e Joins b,a,G by GLIB_000:14;
end;

:: deftheorem Def3 defines are_adjacent CHORD:def_3_:_
 for G being _Graph
for a, b being Vertex of G holds
( a,b are_adjacent iff ex e being set st e Joins a,b,G );

theorem Th44: :: CHORD:44
for G1, G2 being _Graph st G1 == G2 holds
for u1, v1 being Vertex of G1 st u1,v1 are_adjacent holds
for u2, v2 being Vertex of G2 st u1 = u2 &amp; v1 = v2 holds
u2,v2 are_adjacent
proofend;

theorem Th45: :: CHORD:45
for G being _Graph
for S being non empty Subset of (the_Vertices_of G)
for H being inducedSubgraph of G,S
for u, v being Vertex of G
for t, w being Vertex of H st u = t &amp; v = w holds
( u,v are_adjacent iff t,w are_adjacent )
proofend;

theorem Th46: :: CHORD:46
for G being _Graph
for W being Walk of G st W .first() <> W .last() &amp; not W .first() ,W .last() are_adjacent holds
W .length() >= 2
proofend;

theorem Th47: :: CHORD:47
for G being _Graph
for v1, v2, v3 being Vertex of G st v1 <> v2 &amp; v1 <> v3 &amp; v2 <> v3 &amp; v1,v2 are_adjacent &amp; v2,v3 are_adjacent holds
ex P being Path of G ex e1, e2 being set st
( P is open &amp; len P = 5 &amp; P .length() = 2 &amp; e1 Joins v1,v2,G &amp; e2 Joins v2,v3,G &amp; P .edges() = {e1,e2} &amp; P .vertices() = {v1,v2,v3} &amp; P . 1 = v1 &amp; P . 3 = v2 &amp; P . 5 = v3 )
proofend;

theorem Th48: :: CHORD:48
for G being _Graph
for v1, v2, v3, v4 being Vertex of G st v1 <> v2 &amp; v1 <> v3 &amp; v2 <> v3 &amp; v2 <> v4 &amp; v3 <> v4 &amp; v1,v2 are_adjacent &amp; v2,v3 are_adjacent &amp; v3,v4 are_adjacent holds
ex P being Path of G st
( len P = 7 &amp; P .length() = 3 &amp; P .vertices() = {v1,v2,v3,v4} &amp; P . 1 = v1 &amp; P . 3 = v2 &amp; P . 5 = v3 &amp; P . 7 = v4 )
proofend;

definition
let G be _Graph;
let S be set ;
funcG .AdjacentSet S ->  Subset of (the_Vertices_of G) equals :: CHORD:def 4
 {  u where u is Vertex of G : ( not u in S &amp; ex v being Vertex of G st
( v in S &amp; u,v are_adjacent ) )  }  ;
coherence
  {  u where u is Vertex of G : ( not u in S &amp; ex v being Vertex of G st
( v in S &amp; u,v are_adjacent ) )  }  is Subset of (the_Vertices_of G)
proofend;
end;

:: deftheorem  defines .AdjacentSet CHORD:def_4_:_
 for G being _Graph
for S being set holds G .AdjacentSet S =  {  u where u is Vertex of G : ( not u in S &amp; ex v being Vertex of G st
( v in S &amp; u,v are_adjacent ) )  }  ;

theorem :: CHORD:49
for G being _Graph
for S, x being set st x in G .AdjacentSet S holds
not x in S
proofend;

theorem Th50: :: CHORD:50
for G being _Graph
for S being set
for u being Vertex of G holds
( u in G .AdjacentSet S iff ( not u in S &amp; ex v being Vertex of G st
( v in S &amp; u,v are_adjacent ) ) )
proofend;

theorem Th51: :: CHORD:51
for G1, G2 being _Graph st G1 == G2 holds
for S being set holds G1 .AdjacentSet S = G2 .AdjacentSet S
proofend;

theorem Th52: :: CHORD:52
for G being _Graph
for u, v being Vertex of G holds
( u in G .AdjacentSet {v} iff ( u <> v &amp; v,u are_adjacent ) )
proofend;

theorem :: CHORD:53
for G being _Graph
for x, y being set holds
( x in G .AdjacentSet {y} iff y in G .AdjacentSet {x} )
proofend;

theorem :: CHORD:54
for G being _Graph
for C being Path of G st C is Cycle-like &amp; C .length() > 3 holds
for x being Vertex of G st x in C .vertices() holds
ex m, n being odd Nat st
( m + 2 < n &amp; n <= len C &amp; ( not m = 1 or not n = len C ) &amp; ( not m = 1 or not n = (len C) - 2 ) &amp; ( not m = 3 or not n = len C ) &amp; C . m <> C . n &amp; C . m in G .AdjacentSet {x} &amp; C . n in G .AdjacentSet {x} )
proofend;

theorem Th55: :: CHORD:55
for G being _Graph
for C being Path of G st C is Cycle-like &amp; C .length() > 3 holds
for x being Vertex of G st x in C .vertices() holds
ex m, n being odd Nat st
( m + 2 < n &amp; n <= len C &amp; C . m <> C . n &amp; C . m in G .AdjacentSet {x} &amp; C . n in G .AdjacentSet {x} &amp; ( for e being set st e in C .edges() holds
not e Joins C . m,C . n,G ) )
proofend;

:: 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
for G being loopless _Graph
for u being Vertex of G holds
( G .AdjacentSet {u} = {} iff u is isolated )
proofend;

theorem Th57: :: CHORD:57
for G being _Graph
for G0 being Subgraph of G
for S being non empty Subset of (the_Vertices_of G)
for x being Vertex of G
for G1 being inducedSubgraph of G,S
for G2 being inducedSubgraph of G,(S \/ {x}) st G1 is connected &amp; x in G .AdjacentSet (the_Vertices_of G1) holds
G2 is connected
proofend;

theorem Th58: :: CHORD:58
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 &amp; G .AdjacentSet {u} c= S holds
for v being Vertex of H st u = v holds
G .AdjacentSet {u} = H .AdjacentSet {v}
proofend;

:: Adjacency set as a subgraph of G
definition
let G be _Graph;
let S be set ;
mode AdjGraph of G,S ->  Subgraph of G means :Def5: :: CHORD:def 5
it is inducedSubgraph of G,(G .AdjacentSet S) if S is Subset of (the_Vertices_of G)
;
existence
 ( S is Subset of (the_Vertices_of G) implies ex b1 being Subgraph of G st b1 is inducedSubgraph of G,(G .AdjacentSet S) )
proofend;
consistency
 for b1 being Subgraph of G holds verum ;
end;

:: deftheorem Def5 defines AdjGraph CHORD:def_5_:_
 for G being _Graph
for S being set
for b3 being Subgraph of G st S is Subset of (the_Vertices_of G) holds
( b3 is AdjGraph of G,S iff b3 is inducedSubgraph of G,(G .AdjacentSet S) );

theorem Th59: :: CHORD:59
for G1, G2 being _Graph st G1 == G2 holds
for u1 being Vertex of G1
for u2 being Vertex of G2 st u1 = u2 holds
for H1 being AdjGraph of G1,{u1}
for H2 being AdjGraph of G2,{u2} holds H1 == H2
proofend;

theorem Th60: :: CHORD:60
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 &amp; G .AdjacentSet {u} c= S &amp; G .AdjacentSet {u} <> {} holds
for v being Vertex of H st u = v holds
for Ga being AdjGraph of G,{u}
for Ha being AdjGraph of H,{v} holds Ga == Ha
proofend;

definition
let G be _Graph;
attrG is complete  means :Def6: :: CHORD:def 6
 for u, v being Vertex of G st u <> v holds
u,v are_adjacent ;
end;

:: deftheorem Def6 defines complete CHORD:def_6_:_
 for G being _Graph holds
( G is complete iff for u, v being Vertex of G st u <> v holds
u,v are_adjacent );

theorem Th61: :: CHORD:61
for G being _Graph st G is trivial holds
G is complete
proofend;

registration
cluster Relation-like NAT -defined Function-like finite [Graph-like] trivial  ->  complete for set ;
coherence
 for b1 being _Graph st b1 is trivial holds
b1 is complete by Th61;
end;

registration
cluster Relation-like NAT -defined Function-like finite [Graph-like] trivial simple complete for set ;
existence
 ex b1 being _Graph st
( b1 is trivial &amp; b1 is simple &amp; b1 is complete )
proofend;
cluster Relation-like NAT -defined Function-like finite [Graph-like] finite non trivial simple complete for set ;
existence
 ex b1 being _Graph st
( not b1 is trivial &amp; b1 is finite &amp; b1 is simple &amp; b1 is complete )
proofend;
end;

theorem Th62: :: CHORD:62
for G1, G2 being _Graph st G1 == G2 &amp; G1 is complete holds
G2 is complete
proofend;

theorem Th63: :: CHORD:63
for G being complete _Graph
for S being Subset of (the_Vertices_of G)
for H being inducedSubgraph of G,S holds H is complete
proofend;

begin

definition
let G be _Graph;
let v be Vertex of G;
attrv is simplicial  means :Def7: :: CHORD:def 7
( G .AdjacentSet {v} <> {} implies for G2 being AdjGraph of G,{v} holds G2 is complete );
end;

:: deftheorem Def7 defines simplicial CHORD:def_7_:_
 for G being _Graph
for v being Vertex of G holds
( v is simplicial iff ( G .AdjacentSet {v} <> {} implies for G2 being AdjGraph of G,{v} holds G2 is complete ) );

theorem Th64: :: CHORD:64
for G being complete _Graph
for v being Vertex of G holds v is simplicial
proofend;

theorem Th65: :: CHORD:65
for G being trivial _Graph
for v being Vertex of G holds v is simplicial
proofend;

theorem Th66: :: CHORD:66
for G1, G2 being _Graph st G1 == G2 holds
for u1 being Vertex of G1
for u2 being Vertex of G2 st u1 = u2 &amp; u1 is simplicial holds
u2 is simplicial
proofend;

theorem Th67: :: CHORD:67
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 &amp; G .AdjacentSet {u} c= S holds
for v being Vertex of H st u = v holds
( u is simplicial iff v is simplicial )
proofend;

theorem Th68: :: CHORD:68
for G being _Graph
for v being Vertex of G st v is simplicial holds
for a, b being set st a <> b &amp; a in G .AdjacentSet {v} &amp; b in G .AdjacentSet {v} holds
ex e being set st e Joins a,b,G
proofend;

theorem Th69: :: CHORD:69
for G being _Graph
for v being Vertex of G st not v is simplicial holds
ex a, b being Vertex of G st
( a <> b &amp; v <> a &amp; v <> b &amp; v,a are_adjacent &amp; v,b are_adjacent &amp; not a,b are_adjacent )
proofend;

begin

definition
let G be _Graph;
let 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: :: CHORD:def 8
( not a in it &amp; not b in it &amp; ( for G2 being removeVertices of G,it
for W being Walk of G2 holds not W is_Walk_from a,b ) );
existence
 ex b1 being Subset of (the_Vertices_of G) st
( not a in b1 &amp; not b in b1 &amp; ( for G2 being removeVertices of G,b1
for W being Walk of G2 holds not W is_Walk_from a,b ) )
proofend;
end;

:: deftheorem Def8 defines VertexSeparator CHORD:def_8_:_
 for G being _Graph
for a, b being Vertex of G st a <> b &amp; not a,b are_adjacent holds
for b4 being Subset of (the_Vertices_of G) holds
( b4 is VertexSeparator of a,b iff ( not a in b4 &amp; not b in b4 &amp; ( for G2 being removeVertices of G,b4
for W being Walk of G2 holds not W is_Walk_from a,b ) ) );

theorem Th70: :: CHORD:70
for G being _Graph
for a, b being Vertex of G st a <> b &amp; not a,b are_adjacent holds
for S being VertexSeparator of a,b holds S is VertexSeparator of b,a
proofend;

:: alternate characterization of Vertex Separator
theorem Th71: :: CHORD:71
for G being _Graph
for a, b being Vertex of G st a <> b &amp; not a,b are_adjacent holds
for S being Subset of (the_Vertices_of G) holds
( S is VertexSeparator of a,b iff ( not a in S &amp; not b in S &amp; ( for W being Walk of G st W is_Walk_from a,b holds
ex x being Vertex of G st
( x in S &amp; x in W .vertices() ) ) ) )
proofend;

theorem Th72: :: CHORD:72
for G being _Graph
for a, b being Vertex of G st a <> b &amp; not a,b are_adjacent holds
for S being VertexSeparator of a,b
for W being Walk of G st W is_Walk_from a,b holds
ex k being odd Nat st
( 1 < k &amp; k < len W &amp; W . k in S )
proofend;

theorem Th73: :: CHORD:73
for G being _Graph
for a, b being Vertex of G st a <> b &amp; not a,b are_adjacent holds
for S being VertexSeparator of a,b st S = {} holds
for W being Walk of G holds not W is_Walk_from a,b
proofend;

theorem :: CHORD:74
for G being _Graph
for a, b being Vertex of G st a <> b &amp; not a,b are_adjacent &amp; ( for W being Walk of G holds not W is_Walk_from a,b ) holds
{} is VertexSeparator of a,b
proofend;

theorem Th75: :: CHORD:75
for G being _Graph
for a, b being Vertex of G st a <> b &amp; not a,b are_adjacent holds
for S being VertexSeparator of a,b
for G2 being removeVertices of G,S
for a2 being Vertex of G2 holds (G2 .reachableFrom a2) /\ S = {}
proofend;

theorem Th76: :: CHORD:76
for G being _Graph
for a, b being Vertex of G st a <> b &amp; not a,b are_adjacent holds
for S being VertexSeparator of a,b
for G2 being removeVertices of G,S
for a2, b2 being Vertex of G2 st a2 = a &amp; b2 = b holds
(G2 .reachableFrom a2) /\ (G2 .reachableFrom b2) = {}
proofend;

theorem Th77: :: CHORD:77
for G being _Graph
for a, b being Vertex of G st a <> b &amp; not a,b are_adjacent holds
for S being VertexSeparator of a,b
for G2 being removeVertices of G,S holds
( a is Vertex of G2 &amp; b is Vertex of G2 )
proofend;

definition
let G be _Graph;
let a, b be Vertex of G;
let S be VertexSeparator of a,b;
attrS is minimal  means :Def9: :: CHORD:def 9
 for T being Subset of S st T <> S holds
not T is VertexSeparator of a,b;
end;

:: deftheorem Def9 defines minimal CHORD:def_9_:_
 for G being _Graph
for a, b being Vertex of G
for S being VertexSeparator of a,b holds
( S is minimal iff for T being Subset of S st T <> S holds
not T is VertexSeparator of a,b );

theorem :: CHORD:78
for G being _Graph
for a, b being Vertex of G
for S being VertexSeparator of a,b st S = {} holds
S is minimal
proofend;

theorem Th79: :: CHORD:79
for G being finite _Graph
for a, b being Vertex of G ex S being VertexSeparator of a,b st S is minimal
proofend;

theorem Th80: :: CHORD:80
for G being _Graph
for a, b being Vertex of G st a <> b &amp; not a,b are_adjacent holds
for S being VertexSeparator of a,b st S is minimal holds
for T being VertexSeparator of b,a st S = T holds
T is minimal
proofend;

theorem :: CHORD:81
for G being _Graph
for a, b being Vertex of G st a <> b &amp; not a,b are_adjacent holds
for S being VertexSeparator of a,b st S is minimal holds
for x being Vertex of G st x in S holds
ex W being Walk of G st
( W is_Walk_from a,b &amp; x in W .vertices() )
proofend;

theorem Th82: :: CHORD:82
for G being _Graph
for a, b being Vertex of G st a <> b &amp; not a,b are_adjacent holds
for S being VertexSeparator of a,b st S is minimal holds
for H being removeVertices of G,S
for aa being Vertex of H st aa = a holds
for x being Vertex of G st x in S holds
ex y being Vertex of G st
( y in H .reachableFrom aa &amp; x,y are_adjacent )
proofend;

theorem Th83: :: CHORD:83
for G being _Graph
for a, b being Vertex of G st a <> b &amp; not a,b are_adjacent holds
for S being VertexSeparator of a,b st S is minimal holds
for H being removeVertices of G,S
for aa being Vertex of H st aa = b holds
for x being Vertex of G st x in S holds
ex y being Vertex of G st
( y in H .reachableFrom aa &amp; x,y are_adjacent )
proofend;

begin

:: 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 &amp; n <= len W &amp; W.m <> W.n &amp;
:: e Joins W.m,W.n,G &amp;
:: 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;
let W be Walk of G;
attrW is chordal  means :Def10: :: CHORD:def 10
 ex m, n being odd Nat st
( m + 2 < n &amp; n <= len W &amp; W . m <> W . n &amp; ex e being set st e Joins W . m,W . n,G &amp; ( for f being set st f in W .edges() holds
not f Joins W . m,W . n,G ) );
end;

:: deftheorem Def10 defines chordal CHORD:def_10_:_
 for G being _Graph
for W being Walk of G holds
( W is chordal iff ex m, n being odd Nat st
( m + 2 < n &amp; n <= len W &amp; W . m <> W . n &amp; ex e being set st e Joins W . m,W . n,G &amp; ( for f being set st f in W .edges() holds
not f Joins W . m,W . n,G ) ) );

notation
let G be _Graph;
let W be Walk of G;
antonym  chordless W for  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: :: CHORD:84
for G being _Graph
for W being Walk of G st W is chordal holds
ex m, n being odd Nat st
( m + 2 < n &amp; n <= len W &amp; W . m <> W . n &amp; ex e being set st e Joins W . m,W . n,G &amp; ( W is Cycle-like implies ( ( not m = 1 or not n = len W ) &amp; ( not m = 1 or not n = (len W) - 2 ) &amp; ( not m = 3 or not n = len W ) ) ) )
proofend;

theorem Th85: :: CHORD:85
for G being _Graph
for P being Path of G st ex m, n being odd Nat st
( m + 2 < n &amp; n <= len P &amp; ex e being set st e Joins P . m,P . n,G &amp; ( P is Cycle-like implies ( ( not m = 1 or not n = len P ) &amp; ( not m = 1 or not n = (len P) - 2 ) &amp; ( not m = 3 or not n = len P ) ) ) ) holds
P is chordal
proofend;

theorem Th86: :: CHORD:86
for G1, G2 being _Graph st G1 == G2 holds
for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 &amp; W1 is chordal holds
W2 is chordal
proofend;

theorem Th87: :: CHORD:87
for G being _Graph
for S being non empty Subset of (the_Vertices_of G)
for H being inducedSubgraph of G,S
for W1 being Walk of G
for W2 being Walk of H st W1 = W2 holds
( W2 is chordal iff W1 is chordal )
proofend;

theorem :: CHORD:88
for G being _Graph
for W being Walk of G st W is Cycle-like &amp; W is chordal &amp; W .length() = 4 holds
ex e being set st
( e Joins W . 1,W . 5,G or e Joins W . 3,W . 7,G )
proofend;

theorem Th89: :: CHORD:89
for G being _Graph
for W being Walk of G st W is minlength holds
W is chordless
proofend;

theorem :: CHORD:90
for G being _Graph
for W being Walk of G st len W = 5 &amp; not W .first() ,W .last() are_adjacent holds
W is chordless
proofend;

Lm3:  for G being _Graph
for W being Walk of G st W is chordal holds
W .reverse() is chordal
proofend;

theorem :: CHORD:91
for G being _Graph
for W being Walk of G holds
( W is chordal iff W .reverse() is chordal )
proofend;

theorem Th92: :: CHORD:92
for G being _Graph
for P being Path of G st P is open &amp; P is chordless holds
for m, n being odd Nat st m < n &amp; n <= len P holds
( ex e being set st e Joins P . m,P . n,G iff m + 2 = n )
proofend;

theorem :: CHORD:93
for G being _Graph
for P being Path of G st P is open &amp; P is chordless holds
for m, n being odd Nat st m < n &amp; n <= len P holds
( P .cut (m,n) is chordless &amp; P .cut (m,n) is open )
proofend;

theorem :: CHORD:94
for G being _Graph
for S being non empty Subset of (the_Vertices_of G)
for H being inducedSubgraph of G,S
for W being Walk of G
for V being Walk of H st W = V holds
( W is chordless iff V is chordless )
proofend;

definition
let G be _Graph;
attrG is chordal  means :Def11: :: CHORD:def 11
 for P being Walk of G st P .length() > 3 &amp; P is Cycle-like holds
P is chordal ;
end;

:: deftheorem Def11 defines chordal CHORD:def_11_:_
 for G being _Graph holds
( G is chordal iff for P being Walk of G st P .length() > 3 &amp; P is Cycle-like holds
P is chordal );

theorem Th95: :: CHORD:95
for G1, G2 being _Graph st G1 == G2 &amp; G1 is chordal holds
G2 is chordal
proofend;

theorem Th96: :: CHORD:96
for G being finite _Graph st card (the_Vertices_of G) <= 3 holds
G is chordal
proofend;

registration
cluster Relation-like NAT -defined Function-like finite [Graph-like] finite trivial chordal for set ;
existence
 ex b1 being _Graph st
( b1 is trivial &amp; b1 is finite &amp; b1 is chordal )
proofend;
cluster Relation-like NAT -defined Function-like finite [Graph-like] finite non trivial simple chordal for set ;
existence
 ex b1 being _Graph st
( not b1 is trivial &amp; b1 is finite &amp; b1 is simple &amp; b1 is chordal )
proofend;
cluster Relation-like NAT -defined Function-like finite [Graph-like] complete  ->  chordal for set ;
correctness
coherence
for b1 being _Graph st b1 is complete holds
b1 is chordal ;
proofend;
end;

registration
let G be chordal _Graph;
let V be set ;
cluster  ->  chordal for inducedSubgraph of G,V,G .edgesBetween V;
coherence
 for b1 being inducedSubgraph of G,V holds b1 is chordal
proofend;
end;

theorem :: CHORD:97
for G being chordal _Graph
for P being Path of G st P is open &amp; P is chordless holds
for x, e being set st not x in P .vertices() &amp; e Joins P .last() ,x,G &amp; ( for f being set holds not f Joins P . ((len P) - 2),x,G ) holds
( P .addEdge e is Path-like &amp; P .addEdge e is open &amp; P .addEdge e is chordless )
proofend;

:: Golumbic, page 83. Theorem 4.1 (i) ==> (iii)
theorem Th98: :: CHORD:98
for G being chordal _Graph
for a, b being Vertex of G st a <> b &amp; not a,b are_adjacent holds
for S being VertexSeparator of a,b st S is minimal &amp; not S is empty holds
for H being inducedSubgraph of G,S holds H is complete
proofend;

:: 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 &amp; not a,b are_adjacent holds
for S being VertexSeparator of a,b st S is minimal &amp; not S is empty holds
for G2 being inducedSubgraph of G,S holds G2 is complete ) holds
G is chordal
proofend;

:: Exercise 12, p. 101.
:: This needs "finite-branching", we do it for finite though
theorem Th100: :: CHORD:100
for G being finite chordal _Graph
for a, b being Vertex of G st a <> b &amp; not a,b are_adjacent holds
for S being VertexSeparator of a,b st S is minimal holds
for H being removeVertices of G,S
for a1 being Vertex of H st a = a1 holds
ex c being Vertex of G st
( c in H .reachableFrom a1 &amp; ( for x being Vertex of G st x in S holds
c,x are_adjacent ) )
proofend;

theorem :: CHORD:101
for G being finite chordal _Graph
for a, b being Vertex of G st a <> b &amp; not a,b are_adjacent holds
for S being VertexSeparator of a,b st S is minimal holds
for H being removeVertices of G,S
for a1 being Vertex of H st a = a1 holds
for x, y being Vertex of G st x in S &amp; y in S holds
ex c being Vertex of G st
( c in H .reachableFrom a1 &amp; c,x are_adjacent &amp; c,y are_adjacent )
proofend;

:: Golumbic, page 83, Lemma 4.2.
theorem Th102: :: CHORD:102
for G being finite non trivial chordal _Graph st not G is complete holds
ex a, b being Vertex of G st
( a <> b &amp; not a,b are_adjacent &amp; a is simplicial &amp; b is simplicial )
proofend;

theorem Th103: :: CHORD:103
for G being finite chordal _Graph ex v being Vertex of G st v is simplicial
proofend;

begin

definition
let G be finite _Graph;
mode VertexScheme of G ->  FinSequence of the_Vertices_of G means :Def12: :: CHORD:def 12
( it is one-to-one &amp; rng it = the_Vertices_of G );
existence
 ex b1 being FinSequence of the_Vertices_of G st
( b1 is one-to-one &amp; rng b1 = the_Vertices_of G )
proofend;
end;

:: deftheorem Def12 defines VertexScheme CHORD:def_12_:_
 for G being finite _Graph
for b2 being FinSequence of the_Vertices_of G holds
( b2 is VertexScheme of G iff ( b2 is one-to-one &amp; rng b2 = the_Vertices_of G ) );

registration
let G be finite _Graph;
cluster  ->  non empty for VertexScheme of G;
correctness
coherence
for b1 being VertexScheme of G holds not b1 is empty ;
by Def12, RELAT_1:38;
end;

theorem :: CHORD:104
for G being finite _Graph
for S being VertexScheme of G holds len S = card (the_Vertices_of G)
proofend;

theorem :: CHORD:105
for G being finite _Graph
for S being VertexScheme of G holds 1 <= len S by NAT_1:14;

theorem Th106: :: CHORD:106
for G, H being finite _Graph
for g being VertexScheme of G st G == H holds
g is VertexScheme of H
proofend;

definition
let G be finite _Graph;
let S be VertexScheme of G;
let x be Vertex of G;
:: original:..
redefine funcx .. S ->  non zero Element of NAT ;
correctness
coherence
x .. S is non zero Element of NAT ;
proofend;
end;

definition
let G be finite _Graph;
let S be VertexScheme of G;
let n be Nat;
:: original:.followSet
redefine funcS .followSet n ->  Subset of (the_Vertices_of G);
coherence
 S .followSet n is Subset of (the_Vertices_of G)
proofend;
end;

theorem Th107: :: CHORD:107
for G being finite _Graph
for S being VertexScheme of G
for n being non zero Nat st n <= len S holds
not S .followSet n is empty
proofend;

definition
let G be finite _Graph;
let S be VertexScheme of G;
attrS is perfect  means :Def13: :: CHORD:def 13
 for n being non zero Nat st n <= len S holds
for Gf being inducedSubgraph of G,(S .followSet n)
for v being Vertex of Gf st v = S . n holds
v is simplicial ;
end;

:: deftheorem Def13 defines perfect CHORD:def_13_:_
 for G being finite _Graph
for S being VertexScheme of G holds
( S is perfect iff for n being non zero Nat st n <= len S holds
for Gf being inducedSubgraph of G,(S .followSet n)
for v being Vertex of Gf st v = S . n holds
v is simplicial );

:: finite is needed unless we add loopless
theorem Th108: :: CHORD:108
for G being finite trivial _Graph
for v being Vertex of G ex S being VertexScheme of G st
( S = <*v*> &amp; S is perfect )
proofend;

theorem :: CHORD:109
for G being finite _Graph
for V being VertexScheme of G holds
( V is perfect iff for a, b, c being Vertex of G st b <> c &amp; a,b are_adjacent &amp; a,c are_adjacent holds
for va, vb, vc being Nat st va in dom V &amp; vb in dom V &amp; vc in dom V &amp; V . va = a &amp; V . vb = b &amp; V . vc = c &amp; va < vb &amp; va < vc holds
b,c are_adjacent )
proofend;

:: Golubmic pg 83-84, Theorem 4.1 (i) ==> (ii)
registration
let G be finite chordal _Graph;
cluster non empty Relation-like NAT -defined the_Vertices_of G -valued Function-like finite FinSequence-like FinSubsequence-like perfect for VertexScheme of G;
existence
 ex b1 being VertexScheme of G st b1 is perfect
proofend;
end;

theorem :: CHORD:110
for G, H being finite chordal _Graph
for g being perfect VertexScheme of G st G == H holds
g is perfect VertexScheme of H
proofend;

:: 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
proofend;