:: 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{ P₁[ set ] } :

for G being _finite _Graph holds P₁[G]

provided

A1: for k being non zero Nat st ( for Gk being _finite _Graph st Gk .order() < k holds
P₁[Gk] ) holds
for Gk1 being _finite _Graph st Gk1 .order() = k holds
P₁[Gk1]

proof 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 b₁ being Subgraph of G st b₁ is inducedSubgraph of G,(G .AdjacentSet S) )

proof end;

consistency
for b₁ being Subgraph of G holds verum ;

end;

:: deftheorem Def5 defines AdjGraph CHORD:def 5 :
for G being _Graph
for S being set
for b₃ being Subgraph of G st S is Subset of (the_Vertices_of G) holds
( b₃ is AdjGraph of G,S iff b₃ 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 b₁ being _Graph st b₁ is _trivial holds
b₁ is complete by Th60;

end;

registration

cluster Relation-like omega -defined Function-like finite [Graph-like] _trivial simple complete for set ;

existence
ex b₁ being _Graph st
( b₁ is _trivial & b₁ is simple & b₁ is complete )

proof end;

cluster Relation-like omega -defined Function-like finite [Graph-like] _finite non _trivial simple complete for set ;

existence
ex b₁ being _Graph st
( not b₁ is _trivial & b₁ is _finite & b₁ is simple & b₁ 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 b₁ being Subset of (the_Vertices_of G) st
( not a in b₁ & not b in b₁ & ( for G2 being removeVertices of G,b₁
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 b₄ being Subset of (the_Vertices_of G) holds
( b₄ is VertexSeparator of a,b iff ( not a in b₄ & not b in b₄ & ( for G2 being removeVertices of G,b₄
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 b₁ being _Graph st
( b₁ is _trivial & b₁ is _finite & b₁ is chordal )

proof end;

cluster Relation-like omega -defined Function-like finite [Graph-like] _finite non _trivial simple chordal for set ;

existence
ex b₁ being _Graph st
( not b₁ is _trivial & b₁ is _finite & b₁ is simple & b₁ is chordal )

proof end;

cluster Relation-like omega -defined Function-like finite [Graph-like] complete -> chordal for set ;

correctness
coherence
for b₁ being _Graph st b₁ is complete holds
b₁ 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 b₁ being inducedSubgraph of G,V holds b₁ 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 b₁ being FinSequence of the_Vertices_of G st
( b₁ is one-to-one & rng b₁ = the_Vertices_of G )

proof end;

end;

:: deftheorem Def12 defines VertexScheme CHORD:def 12 :
for G being _finite _Graph
for b₂ being FinSequence of the_Vertices_of G holds
( b₂ is VertexScheme of G iff ( b₂ is one-to-one & rng b₂ = the_Vertices_of G ) );

registration

let G be _finite _Graph;

cluster -> non empty for VertexScheme of G;

correctness
coherence
for b₁ being VertexScheme of G holds not b₁ 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 b₁ being VertexScheme of G st b₁ 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;