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


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

theorem Th2: :: CHORD:2
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 end;

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

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

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

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

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

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

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

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

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

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

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

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

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

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 & ( for y being set st y in T holds
x .. p <= y .. p ) )
proof end;

definition
let p be FinSequence;
let n be Nat;
func p .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 & n in dom p & p is one-to-one holds
( x in p .followSet n iff x .. p >= n )
proof end;

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

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

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 object st u in S & v in S holds
for e being object st e Joins u,v,G holds
e Joins u,v,H
proof end;

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

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

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

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

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 & W1 is Cycle-like holds
W2 is Cycle-like by GLIB_001:181;

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

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() & b = P .first() & e Joins a,b,G holds
(G .walkOf (a,e,b)) .append P is Path-like
proof end;

theorem Th27: :: CHORD:27
for G being _Graph
for P, H being Path of G st P .edges() misses H .edges() & P is open & H is V5() & 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 end;

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())
proof end;

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

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

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

:: we do not consider infinite graphs
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]
proof end;

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

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

definition
let G be _Graph;
let 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;

:: deftheorem 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() & S .edgeSeq() = W .edgeSeq() holds
S = W
proof end;

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

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

theorem :: CHORD:37
canceled;

::$CT
theorem Th37: :: 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
proof end;

theorem Th38: :: 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() & P is minlength )
proof end;

theorem Th39: :: 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 & n <= len W holds
for e being object holds not e Joins W . m,W . n,G
proof end;

theorem Th40: :: 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 & n <= len W holds
for e being object holds not e Joins W . m,W . n,G
proof end;

theorem Th41: :: 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 & n <= len W holds
W .cut (m,n) is minlength
proof end;

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 & P is V5() & 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 end;

definition
let G be _Graph;
let a, b be Vertex of G;
pred a,b are_adjacent means :Def3: :: CHORD:def 3
 ex e being object st e Joins a,b,G;
symmetry
for a, b being Vertex of G st ex e being object st e Joins a,b,G holds
ex e being object 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 object st e Joins a,b,G );

theorem Th43: :: 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 & v1 = v2 holds
u2,v2 are_adjacent
proof end;

theorem Th44: :: 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 & v = w holds
( u,v are_adjacent iff t,w are_adjacent )
proof end;

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

theorem Th46: :: CHORD:47
for G being _Graph
for v1, v2, v3 being Vertex of G st v1 <> v2 & v1 <> v3 & v2 <> v3 & v1,v2 are_adjacent & v2,v3 are_adjacent holds
ex P being Path of G ex 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 )
proof end;

theorem Th47: :: CHORD:48
for G being _Graph
for 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 holds
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 end;

definition
let G be _Graph;
let 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 ) ) } ;
coherence
{ 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 ) ) } is Subset of (the_Vertices_of G)
proof end;
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 & ex v being Vertex of G st
( v in S & 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
proof end;

theorem Th49: :: 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 & ex v being Vertex of G st
( v in S & u,v are_adjacent ) ) )
proof end;

theorem Th50: :: CHORD:51
for G1, G2 being _Graph st G1 == G2 holds
for S being set holds G1 .AdjacentSet S = G2 .AdjacentSet S
proof end;

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

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

theorem :: CHORD:54
for G being _Graph
for C being Path of G st C is Cycle-like & 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 & n <= len C & ( not m = 1 or not n = len C ) & ( not m = 1 or not n = (len C) - 2 ) & ( not m = 3 or not n = len C ) & C . m <> C . n & C . m in G .AdjacentSet {x} & C . n in G .AdjacentSet {x} )
proof end;

theorem Th54: :: CHORD:55
for G being _Graph
for C being Path of G st C is Cycle-like & 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 & 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 ) )
proof 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 :: CHORD:56
for G being loopless _Graph
for u being Vertex of G holds
( G .AdjacentSet {u} = {} iff u is isolated )
proof end;

theorem Th56: :: 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 & x in G .AdjacentSet (the_Vertices_of G1) holds
G2 is connected
proof end;

theorem Th57: :: 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 & G .AdjacentSet {u} c= S holds
for v being Vertex of H st u = v holds
G .AdjacentSet {u} = H .AdjacentSet {v}
proof end;

:: 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) )
proof end;
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 Th58: :: 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
proof end;

theorem Th59: :: 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 & G .AdjacentSet {u} c= S & 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
proof end;

definition
let G be _Graph;
attr G 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 Th60: :: CHORD:61
for G being _Graph st G is _trivial holds
G is complete
proof end;

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

registration
cluster Relation-like omega -defined Function-like finite [Graph-like] _trivial simple complete for set ;
existence
ex b1 being _Graph st
( b1 is _trivial & b1 is simple & b1 is complete )
proof end;
cluster Relation-like omega -defined Function-like finite [Graph-like] _finite non _trivial simple complete for set ;
existence
ex b1 being _Graph st
( not b1 is _trivial & b1 is _finite & b1 is simple & b1 is complete )
proof end;
end;

theorem Th61: :: CHORD:62
for G1, G2 being _Graph st G1 == G2 & G1 is complete holds
G2 is complete
proof end;

theorem Th62: :: 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
proof end;

definition
let G be _Graph;
let 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;

:: deftheorem 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 Th63: :: CHORD:64
for G being complete _Graph
for v being Vertex of G holds v is simplicial
proof end;

theorem :: CHORD:65
for G being _trivial _Graph
for v being Vertex of G holds v is simplicial ;

theorem Th65: :: 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 & u1 is simplicial holds
u2 is simplicial
proof end;

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

theorem Th67: :: CHORD:68
for G being _Graph
for v being Vertex of G st v is simplicial holds
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
proof end;

theorem Th68: :: 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 & v <> a & v <> b & v,a are_adjacent & v,b are_adjacent & not a,b are_adjacent )
proof end;

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 & not b in it & ( 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 & not b in b1 & ( for G2 being removeVertices of G,b1
for W being Walk of G2 holds not W is_Walk_from a,b ) )
proof end;
end;

:: deftheorem Def8 defines VertexSeparator CHORD:def 8 :
for G being _Graph
for a, b being Vertex of G st a <> b & 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 & not b in b4 & ( for G2 being removeVertices of G,b4
for W being Walk of G2 holds not W is_Walk_from a,b ) ) );

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

:: alternate characterization of Vertex Separator
theorem Th70: :: CHORD:71
for G being _Graph
for a, b being Vertex of G st a <> b & 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 & 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 end;

theorem Th71: :: CHORD:72
for G being _Graph
for a, b being Vertex of G st a <> b & 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 & k < len W & W . k in S )
proof end;

theorem Th72: :: CHORD:73
for G being _Graph
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 = {} holds
for W being Walk of G holds not W is_Walk_from a,b
proof end;

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

theorem Th74: :: CHORD:75
for G being _Graph
for a, b being Vertex of G st a <> b & 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 = {}
proof end;

theorem Th75: :: CHORD:76
for G being _Graph
for a, b being Vertex of G st a <> b & 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 & b2 = b holds
(G2 .reachableFrom a2) /\ (G2 .reachableFrom b2) = {}
proof end;

theorem Th76: :: CHORD:77
for G being _Graph
for a, b being Vertex of G st a <> b & 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 & b is Vertex of G2 )
proof end;

definition
let G be _Graph;
let 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;

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

theorem Th78: :: 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
proof end;

theorem Th79: :: CHORD:80
for G being _Graph
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 holds
for T being VertexSeparator of b,a st S = T holds
T is minimal by Th69;

theorem :: CHORD:81
for G being _Graph
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 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 & x in W .vertices() )
proof end;

theorem Th81: :: CHORD:82
for G being _Graph
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 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 & x,y are_adjacent )
proof end;

theorem Th82: :: CHORD:83
for G being _Graph
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 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 & x,y are_adjacent )
proof end;

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

:: deftheorem 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 & 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 ) ) );

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 Th83: :: 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 & 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 or not n = len W ) & ( not m = 1 or not n = (len W) - 2 ) & ( not m = 3 or not n = len W ) ) ) )
proof end;

theorem Th84: :: CHORD:85
for G being _Graph
for 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 or not n = len P ) & ( not m = 1 or not n = (len P) - 2 ) & ( not m = 3 or not n = len P ) ) ) ) holds
P is chordal
proof end;

theorem Th85: :: 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 & W1 is chordal holds
W2 is chordal
proof end;

theorem Th86: :: 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 )
proof end;

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

theorem Th88: :: CHORD:89
for G being _Graph
for W being Walk of G st W is minlength holds
W is chordless by Th39;

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

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

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

theorem Th91: :: CHORD:92
for G being _Graph
for P being Path of G st P is open & P is chordless holds
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 )
proof end;

theorem :: CHORD:93
for G being _Graph
for P being Path of G st P is open & P is chordless holds
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 end;

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

definition
let G be _Graph;
attr G is chordal means :Def11: :: CHORD:def 11
 for P being Walk of G st P .length() > 3 & 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 & P is Cycle-like holds
P is chordal );

theorem Th94: :: CHORD:95
for G1, G2 being _Graph st G1 == G2 & G1 is chordal holds
G2 is chordal
proof end;

theorem Th95: :: CHORD:96
for G being _finite _Graph st card (the_Vertices_of G) <= 3 holds
G is chordal
proof end;

registration
cluster Relation-like omega -defined Function-like finite [Graph-like] _finite _trivial chordal for set ;
existence
ex b1 being _Graph st
( b1 is _trivial & b1 is _finite & b1 is chordal )
proof end;
cluster Relation-like omega -defined Function-like finite [Graph-like] _finite non _trivial simple chordal for set ;
existence
ex b1 being _Graph st
( not b1 is _trivial & b1 is _finite & b1 is simple & b1 is chordal )
proof end;
cluster Relation-like omega -defined Function-like finite [Graph-like] complete -> chordal for set ;
correctness
coherence
for b1 being _Graph st b1 is complete holds
b1 is chordal ;
proof end;
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
proof end;
end;

theorem :: CHORD:97
for G being chordal _Graph
for P being Path of G st P is open & P is chordless holds
for x, e being object st not x in P .vertices() & e Joins P .last() ,x,G & ( for f being object holds not 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 end;

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

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

:: Exercise 12, p. 101.
:: This needs "finite-branching", we do it for finite though
theorem Th99: :: CHORD:100
for G being _finite chordal _Graph
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 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 & ( for x being Vertex of G st x in S holds
c,x are_adjacent ) )
proof end;

theorem :: CHORD:101
for G being _finite chordal _Graph
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 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 & 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 end;

:: Golumbic, page 83, Lemma 4.2.
theorem Th101: :: 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 & not a,b are_adjacent & a is simplicial & b is simplicial )
proof end;

theorem Th102: :: CHORD:103
for G being _finite chordal _Graph ex v being Vertex of G st v is simplicial
proof end;

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 & rng it = the_Vertices_of G );
existence
ex b1 being FinSequence of the_Vertices_of G st
( b1 is one-to-one & rng b1 = the_Vertices_of G )
proof end;
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 & 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)
proof end;

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

theorem Th105: :: CHORD:106
for G, H being _finite _Graph
for g being VertexScheme of G st G == H holds
g is VertexScheme of H
proof end;

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

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

theorem Th106: :: 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
proof end;

definition
let G be _finite _Graph;
let S be VertexScheme of G;
attr S 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 Th107: :: CHORD:108
for G being _finite _trivial _Graph
for v being Vertex of G ex S being VertexScheme of G st
( S = <*v*> & S is perfect )
proof end;

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 & a,b are_adjacent & a,c are_adjacent holds
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 end;

:: Golubmic pg 83-84, Theorem 4.1 (i) ==> (ii)
registration
let G be _finite chordal _Graph;
cluster non empty Relation-like omega -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
proof end;
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
proof end;

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