:: by Broderick Arneson and Piotr Rudnicki

::

:: Received August 18, 2006

:: Copyright (c) 2006-2021 Association of Mizar Users

Lm1: for a, b, c being Integer st a + 2 < b holds

((c - b) + 1) + 2 < (c - a) + 1

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

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 ) )

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

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 )

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

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

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

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 )

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

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

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

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;

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 )

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

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

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())

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

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

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

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

:: should be in GLIBs

:: PathLike15

:: should be in GLIB

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

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;

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

for W2 being Walk of G st W2 is_Walk_from W .first() ,W .last() holds

len W2 >= len W;

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

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

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;

::$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

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 )

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

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

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

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 ) ) )

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;

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;
let a, b be Vertex of 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;

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

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

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 )

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

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 )

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 )

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 ;

{ 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)

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

{ 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;

:: 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 ) ) } ;

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 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 ) ) )

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

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 ) )

for u, v being Vertex of G holds

( u in G .AdjacentSet {v} iff ( u <> v & v,u are_adjacent ) )

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} )

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 ) )

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.

:: 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 )

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

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}

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 ;

( S is Subset of (the_Vertices_of G) implies ex b_{1} being Subgraph of G st b_{1} is inducedSubgraph of G,(G .AdjacentSet S) )

for b_{1} being Subgraph of G holds verum
;

end;
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 it is inducedSubgraph of G,(G .AdjacentSet S) if S is Subset of (the_Vertices_of G)

;

( S is Subset of (the_Vertices_of G) implies ex b

proof end;

consistency for b

:: deftheorem Def5 defines AdjGraph CHORD:def 5 :

for G being _Graph

for S being set

for b_{3} being Subgraph of G st S is Subset of (the_Vertices_of G) holds

( b_{3} is AdjGraph of G,S iff b_{3} is inducedSubgraph of G,(G .AdjacentSet S) );

for G being _Graph

for S being set

for b

( b

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

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

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;

end;
attr G is complete means :Def6: :: CHORD:def 6

for u, v being Vertex of G st u <> v holds

u,v are_adjacent ;

for u, v being Vertex of G st u <> v holds

u,v are_adjacent ;

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

for G being _Graph holds

( G is complete iff for u, v being Vertex of G st u <> v holds

u,v are_adjacent );

registration

for b_{1} being _Graph st b_{1} is _trivial holds

b_{1} is complete
by Th60;

end;

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

coherence for b

b

registration

ex b_{1} being _Graph st

( b_{1} is _trivial & b_{1} is simple & b_{1} is complete )

ex b_{1} being _Graph st

( not b_{1} is _trivial & b_{1} is _finite & b_{1} is simple & b_{1} is complete )
end;

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

existence ex b

( b

proof end;

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

existence ex b

( not b

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

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;

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

( G .AdjacentSet {v} <> {} implies for G2 being AdjGraph of G,{v} holds G2 is complete );

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

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 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

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 )

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

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 )

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 ;

ex b_{1} being Subset of (the_Vertices_of G) st

( not a in b_{1} & not b in b_{1} & ( for G2 being removeVertices of G,b_{1}

for W being Walk of G2 holds not W is_Walk_from a,b ) )

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

ex b

( not a in b

for W being Walk of G2 holds not W is_Walk_from a,b ) )

proof 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_{4} being Subset of (the_Vertices_of G) holds

( b_{4} is VertexSeparator of a,b iff ( not a in b_{4} & not b in b_{4} & ( for G2 being removeVertices of G,b_{4}

for W being Walk of G2 holds not W is_Walk_from a,b ) ) );

for G being _Graph

for a, b being Vertex of G st a <> b & not a,b are_adjacent holds

for b

( 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

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() ) ) ) )

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 )

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

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

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 = {}

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) = {}

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 )

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;

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

for T being Subset of S st T <> S holds

not T is VertexSeparator of a,b;

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

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

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

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;

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() )

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 )

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 )

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, 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?

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

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

:: 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.

:: 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 ) ) ) )

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

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

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 )

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 )

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

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 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 )

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 )

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 )

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;

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

for P being Walk of G st P .length() > 3 & P is Cycle-like holds

P is chordal ;

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

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

registration

ex b_{1} being _Graph st

( b_{1} is _trivial & b_{1} is _finite & b_{1} is chordal )

ex b_{1} being _Graph st

( not b_{1} is _trivial & b_{1} is _finite & b_{1} is simple & b_{1} is chordal )

coherence

for b_{1} being _Graph st b_{1} is complete holds

b_{1} is chordal ;

end;

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

existence ex b

( b

proof end;

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

existence ex b

( not b

proof end;

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

correctness coherence

for b

b

proof end;

registration

let G be chordal _Graph;

let V be set ;

coherence

for b_{1} being inducedSubgraph of G,V holds b_{1} is chordal

end;
let V be set ;

coherence

for b

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

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

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

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

:: 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 ) )

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 )

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 )

ex a, b being Vertex of G st

( a <> b & not a,b are_adjacent & a is simplicial & b is simplicial )

proof end;

definition

let G be _finite _Graph;

ex b_{1} being FinSequence of the_Vertices_of G st

( b_{1} is one-to-one & rng b_{1} = the_Vertices_of G )

end;
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 ( it is one-to-one & rng it = the_Vertices_of G );

ex b

( b

proof end;

:: deftheorem Def12 defines VertexScheme CHORD:def 12 :

for G being _finite _Graph

for b_{2} being FinSequence of the_Vertices_of G holds

( b_{2} is VertexScheme of G iff ( b_{2} is one-to-one & rng b_{2} = the_Vertices_of G ) );

for G being _finite _Graph

for b

( b

registration

let G be _finite _Graph;

correctness

coherence

for b_{1} being VertexScheme of G holds not b_{1} is empty ;

by Def12, RELAT_1:38;

end;
correctness

coherence

for b

by Def12, RELAT_1:38;

theorem :: CHORD:105

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 ;

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

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)

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

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

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;

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

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 ;

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

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 )

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 )

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;

ex b_{1} being VertexScheme of G st b_{1} is perfect

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

proof 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

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)

:: Golubmic pg 83-84, Theorem 4.1 (ii) ==> (i)