:: Chordal Graphs
:: by Broderick Arneson and Piotr Rudnicki
::
:: Received August 18, 2006
:: Copyright (c) 2006-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, XCMPLX_0, ORDINAL1, ARYTM_1, XXREAL_0, NAT_1, CARD_1,
ARYTM_3, ABIAN, SUBSET_1, RELAT_1, INT_1, FINSEQ_1, FUNCT_1, FINSEQ_4,
XBOOLE_0, FINSET_1, GRAPH_2, ORDINAL4, GLIB_000, GLIB_001, TARSKI,
ZFMISC_1, RCOMP_1, GRAPH_1, RELAT_2, REWRITE1, FUNCOP_1, GLIB_002,
PARTFUN1, MEMBERED, TOPGEN_1, CHORD, CARD_2;
notations TARSKI, XBOOLE_0, SUBSET_1, XXREAL_2, ORDINAL1, INT_1, XCMPLX_0,
XXREAL_0, DOMAIN_1, RELAT_1, FUNCT_1, FUNCT_2, FINSEQ_1, CARD_1,
ARYTM_1, FINSET_1, NAT_1, NAT_D, ZFMISC_1, GLIB_000, GLIB_001, GLIB_002,
CARD_2, FUNCOP_1, ABIAN,
ENUMSET1, FINSEQ_4, NUMBERS, GRAPH_2, MEMBERED, FINSEQ_6;
constructors DOMAIN_1, REAL_1, NAT_D, FINSEQ_4, GRAPH_2, GLIB_001, GLIB_002,
VALUED_1, XXREAL_2, RELSET_1, NUMBERS, FINSEQ_6, ARYTM_1, CARD_2;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1,
FINSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1, MEMBERED, FINSEQ_1,
GLIB_000, ABIAN, GLIB_001, GLIB_002, FUNCT_2, XXREAL_2, CARD_1, RELSET_1,
FINSEQ_6;
requirements ARITHM, BOOLE, NUMERALS, REAL, SUBSET;
definitions TARSKI, XBOOLE_0, GLIB_000, GLIB_002;
equalities GLIB_000, GLIB_001, FUNCOP_1;
expansions TARSKI, XBOOLE_0, GLIB_000, GLIB_001, GLIB_002;
theorems FINSEQ_1, FUNCT_1, GLIB_000, GLIB_001, GLIB_002, GRAPH_2, GRAPH_3,
TREES_1, INT_1, JORDAN12, NAT_1, ORDINAL1, RELAT_1, TARSKI, XBOOLE_0,
XBOOLE_1, FUNCOP_1, FUNCT_2, FINSEQ_3, FINSEQ_4, ZFMISC_1, ABIAN, CARD_2,
ENUMSET1, FINSEQ_2, XREAL_1, MEMBERED, FINSEQ_5, XXREAL_0, NAT_D,
PARTFUN1, XXREAL_2, NUMBERS, FINSEQ_6, CARD_1;
schemes NAT_1, PRE_CIRC, FUNCT_2, FRAENKEL;
begin :: Preliminaries
theorem Th1:
for n being non zero Nat holds n-1 is Nat & 1 <= n
proof
let n be non zero Nat;
A1: 0+1 <= n by NAT_1:13;
then 0+1-1 <= n-1 by XREAL_1:9;
then n-1 in NAT by INT_1:3;
hence n-1 is Nat;
thus thesis by A1;
end;
theorem Th2: :: Nat02
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
let a,b,c be Integer such that
A1: a+2 < b;
assume c-b+1 + 2 >= c-a+1;
then c-b+3-3 >= c-a + 1 -3 by XREAL_1:9;
then c - b >= c - (a+2);
hence contradiction by A1,XREAL_1:10;
end;
theorem Th3: :: EvenOdd02
for n,m being odd Integer st n < m holds n <= m-2
proof
let n,m be odd Integer;
assume n < m;
then n+1 <= m by INT_1:7;
then n+1+(-1) <= m+(-1) by XREAL_1:7;
then n < m-1 by XXREAL_0:1;
then n+1 <= m-1 by INT_1:7;
then n+1+(-1) <= m-1+(-1) by XREAL_1:7;
hence thesis;
end;
theorem Th4: :: EvenOdd03:
for n,m being odd Integer st m < n holds m+2 <= n
proof
let n,m be odd Integer;
assume m < n;
then m+1 <= n by INT_1:7;
then m+1 < n by XXREAL_0:1;
then m+1+1 <= n by INT_1:7;
hence thesis;
end;
theorem Th5: :: EvenOdd04:
for n being odd Nat st 1 <> n
ex m being odd Nat st m+2 = n
proof
let n being odd Nat;
A1: 1 <= n by ABIAN:12;
assume 1 <> n;
then 2*0+1 < n by A1,XXREAL_0:1;
then 1+2 <= n by Th4;
then 1+2-2 <= n-2 by XREAL_1:9;
then n-2*1 in NAT by INT_1:3;
then reconsider m = n-2 as odd Nat;
take m;
thus thesis;
end;
theorem Th6: :: Odd100
for n being odd Nat st n<=2 holds n=1
proof
let n be odd Nat such that
A1: n<=2;
n <> 2*1;
then n < 1+1 by A1,XXREAL_0:1;
then
A2: n <= 1 by NAT_1:13;
n >= 1 by ABIAN:12;
hence thesis by A2,XXREAL_0:1;
end;
theorem Th7: :: Odd101
for n being odd Nat st n<=4 holds n=1 or n=3
proof
let n be odd Nat such that
A1: n<=4;
n<>2*2;
then n<3+1 by A1,XXREAL_0:1;
then
A2: n<=3 by NAT_1:13;
per cases by A2,XXREAL_0:1;
suppose
n=3;
hence thesis;
end;
suppose
n<2+1;
then n<=2 by NAT_1:13;
hence thesis by Th6;
end;
end;
theorem Th8: :: Odd102
for n being odd Nat st n<=6 holds n=1 or n=3 or n=5
proof
let n be odd Nat such that
A1: n<=6;
n<>2*3;
then n<5+1 by A1,XXREAL_0:1;
then
A2: n<=5 by NAT_1:13;
per cases by A2,XXREAL_0:1;
suppose
n=5;
hence thesis;
end;
suppose
n<4+1;
then n<=4 by NAT_1:13;
hence thesis by Th7;
end;
end;
theorem
for n being odd Nat st n<=8 holds n=1 or n=3 or n=5 or n=7
proof
let n be odd Nat such that
A1: n<=8;
n<>2*4;
then n<7+1 by A1,XXREAL_0:1;
then
A2: n<=7 by NAT_1:13;
per cases by A2,XXREAL_0:1;
suppose
n=7;
hence thesis;
end;
suppose
n<6+1;
then n<=6 by NAT_1:13;
hence thesis by Th8;
end;
end;
theorem Th10: :: Even100
for n being even Nat st n<=1 holds n=0
proof
let n be even Nat such that
A1: n<=1;
n<>2*0+1;
then n<0+1 by A1,XXREAL_0:1;
hence thesis by NAT_1:13;
end;
theorem Th11: :: Even101
for n being even Nat st n<=3 holds n=0 or n=2
proof
let n be even Nat such that
A1: n<=3;
n<>2*1+1;
then n<2+1 by A1,XXREAL_0:1;
then
A2: n<=2 by NAT_1:13;
per cases by A2,XXREAL_0:1;
suppose
n=2;
hence thesis;
end;
suppose
n<1+1;
then n<=1 by NAT_1:13;
hence thesis by Th10;
end;
end;
theorem Th12: :: Even102
for n being even Nat st n<=5 holds n=0 or n=2 or n=4
proof
let n be even Nat such that
A1: n<=5;
n<>2*2+1;
then n<4+1 by A1,XXREAL_0:1;
then
A2: n<=4 by NAT_1:13;
per cases by A2,XXREAL_0:1;
suppose
n=4;
hence thesis;
end;
suppose
n<3+1;
then n<=3 by NAT_1:13;
hence thesis by Th11;
end;
end;
theorem Th13: :: Even103
for n being even Nat st n<=7 holds n=0 or n=2 or n=4 or n=6
proof
let n be even Nat such that
A1: n<=7;
n<>2*3+1;
then n<6+1 by A1,XXREAL_0:1;
then
A2: n<=6 by NAT_1:13;
per cases by A2,XXREAL_0:1;
suppose
n=6;
hence thesis;
end;
suppose
n<5+1;
then n<=5 by NAT_1:13;
hence thesis by Th12;
end;
end;
Lm2: for i,j being odd Nat st i <= j
ex k being Nat st i+2*k = j
proof
let i,j be odd Nat;
assume i <= j;
then consider jjj being Nat such that
A1: j = i+jjj by NAT_1:10;
jjj is even by A1;
then consider jj being Nat such that
A2: 2*jj = jjj by ABIAN:def 2;
take jj;
thus thesis by A1,A2;
end;
theorem
for p being FinSequence, n being non zero Nat st
p is one-to-one & n <= len p holds (p.n)..p = n
proof
let S be FinSequence;
let n be non zero Nat such that
A1: S is one-to-one and
A2: n <= len S;
set m = (S.n)..S;
0+1 <= n by NAT_1:14;
then
A3: n in dom S by A2,FINSEQ_3:25;
then
A4: S.n in rng S by FUNCT_1:3;
then
A5: S.m = S.n by FINSEQ_4:19;
m in dom S by A4,FINSEQ_4:20;
hence thesis by A1,A3,A5,FUNCT_1:def 4;
end;
theorem Th15: :: Index01
for p being non empty FinSequence,
T being non empty Subset of rng p
ex x being set st x in T & for y being set st y in T holds x..p <= y..p
proof
let S be non empty FinSequence;
let T be non empty Subset of rng S;
deffunc F(set) = $1..S;
consider m being Element of T such that
A1: for y being Element of T holds F(m) <= F(y) from PRE_CIRC:sch 5;
take m;
thus m in T;
let y be set;
assume y in T;
hence thesis by A1;
end;
definition
let p be FinSequence, n be Nat;
func p.followSet(n) -> finite set equals
rng (n,len p)-cut p;
correctness;
end;
theorem Th16: :: Follow00
for p being FinSequence, x being set, n being Nat st
x in rng p & n in dom p & p is one-to-one holds
x in p.followSet(n) iff x..p >= n
proof
let p be FinSequence, x be set, n be Nat such that
A1: x in rng p and
A2: n in dom p and
A3: p is one-to-one;
A4: n <= len p by A2,FINSEQ_3:25;
hereby
A5: p.(x..p) = x by A1,FINSEQ_4:19;
assume x in p.followSet(n);
then consider a being Nat such that
A6: a in dom (n, len p)-cut p and
A7: ((n, len p)-cut p).a = x by FINSEQ_2:10;
A8: x..p in dom p by A1,FINSEQ_4:20;
ex k being Nat st k in dom p & p.k = ((n, len p)-cut p).a
& k+1 = n+a & n <= k & k <= len p by A6,GRAPH_3:2;
hence x..p >= n by A3,A7,A8,A5,FUNCT_1:def 4;
end;
assume x..p >= n;
then consider k being Nat such that
A9: x..p = n + k by NAT_1:10;
A10: 1 <= n by A2,FINSEQ_3:25;
then
A11: len ((n, len p)-cut p) + n = len p + 1 by A4,FINSEQ_6:def 4;
x..p in dom p by A1,FINSEQ_4:20;
then k + n <= len p by A9,FINSEQ_3:25;
then k + n + (-n) <= len p + (-n) by XREAL_1:7;
then
A12: k + 1 <= len p - n + 1 by XREAL_1:7;
then k < len ((n, len p)-cut p) by A11,NAT_1:13;
then
A13: ((n, len p)-cut p).(k+1) = p.(x..p) by A9,A10,A4,FINSEQ_6:def 4;
A14: p.(x..p) = x by A1,FINSEQ_4:19;
0+1 <= k+1 by XREAL_1:7;
then k+1 in dom ((n, len p)-cut p) by A11,A12,FINSEQ_3:25;
hence thesis by A14,A13,FUNCT_1:3;
end;
theorem Th17: :: Follow03
for p, q being FinSequence, x being set st p = <*x*>^q
for n being non zero Nat holds p.followSet(n+1) = q.followSet(n)
proof
let p,q be FinSequence, x be set such that
A1: p = <*x*>^q;
let n be non zero Nat;
len <*x*> = 1 by FINSEQ_1:40;
then
A2: len p = 1 + len q by A1,FINSEQ_1:22;
per cases;
suppose
A3: n > len q;
then n+1 > len p by A2,XREAL_1:8;
then (n+1,len p)-cut p = {} by FINSEQ_6:def 4;
hence thesis by A3,FINSEQ_6:def 4;
end;
suppose
A4: n <= len q;
then
A5: n+1 <= len p by A2,XREAL_1:7;
A6: 0+1 <= n by NAT_1:13;
then
A7: 1 <= n+1 by XREAL_1:7;
then
A8: len ((n+1, len p)-cut p) + (n+1) = len p + 1 by A5,FINSEQ_6:def 4;
A9: len (n, len q)-cut q + n = len q + 1 by A4,A6,FINSEQ_6:def 4;
then dom ((n+1,len p)-cut p) = Seg (len ((n, len q)-cut q)) by A2,A8,
FINSEQ_1:def 3;
then
A10: dom ((n+1,len p)-cut p) = dom ((n, len q)-cut q) by FINSEQ_1:def 3;
A11: now
let i be Nat;
assume i in dom q;
then p.(len <*x*> + i) = q.i by A1,FINSEQ_1:def 7;
hence p.(i+1) = q.i by FINSEQ_1:40;
end;
A12: now
let k be Nat such that
A13: k in dom ((n, len q)-cut q);
A14: k <= (len p - n) by A8,A10,A13,FINSEQ_3:25;
then
A15: -1 + k < 0 + (len p - n) by XREAL_1:8;
1 <= k by A13,FINSEQ_3:25;
then 1+-1 <= k+-1 by XREAL_1:7;
then k-1 in NAT by INT_1:3;
then reconsider k1 = k-1 as Nat;
n+k <= n+((len p)-n) by A14,XREAL_1:7;
then
A16: k1+n +1 + -1 <= len q + 1 + -1 by A2,XREAL_1:7;
1+0 <= n+k1 by NAT_1:13;
then
A17: n+k1 in dom q by A16,FINSEQ_3:25;
thus ((n+1,len p)-cut p).k = ((n+1, len p)-cut p).(k1+1)
.= p.(n+1+k1) by A7,A5,A8,A15,FINSEQ_6:def 4
.= p.(n+k1+1)
.= q.(n+k1) by A11,A17
.= ((n,len q)-cut q).(k1+1) by A2,A4,A6,A9,A15,FINSEQ_6:def 4
.= ((n,len q)-cut q).k;
end;
now
let y be object;
hereby
assume y in rng (n+1,len p)-cut p;
then consider k being Nat such that
A18: k in dom (n+1, len p)-cut p and
A19: ((n+1,len p)-cut p).k = y by FINSEQ_2:10;
((n+1,len p)-cut p).k = ((n, len q)-cut q).k by A10,A12,A18;
hence y in rng (n, len q)-cut q by A10,A18,A19,FUNCT_1:3;
end;
assume y in rng ((n, len q)-cut q);
then consider k being Nat such that
A20: k in dom (n, len q)-cut q and
A21: ((n, len q)-cut q).k = y by FINSEQ_2:10;
((n+1,len p)-cut p).k = ((n, len q)-cut q).k by A12,A20;
hence y in rng (n+1,len p)-cut p by A10,A20,A21,FUNCT_1:3;
end;
hence thesis by TARSKI:2;
end;
end;
theorem Th18: :: FinSubseq00
for X being set, f being FinSequence of X, g being Subset of f
st len Seq g = len f holds Seq g = f
proof
let X be set, f be FinSequence of X, g be Subset of f such that
A1: len Seq g = len f;
A2: len Seq g = card g by GLIB_001:5;
now
assume g <> f;
then g c< f;
hence contradiction by A1,A2,CARD_2:48;
end;
hence thesis by FINSEQ_3:116;
end;
begin :: Miscellany on graphs
theorem Th19:
for G being _Graph, S being Subset of the_Vertices_of G
for H being inducedSubgraph of G,S
for u,v being object st u in S & v in S
for e being object st e Joins u,v,G holds e Joins u,v,H
proof
let G be _Graph, S be Subset of the_Vertices_of G;
let H be inducedSubgraph of G,S;
let u,v be object such that
A1: u in S and
A2: v in S;
reconsider S as non empty Subset of the_Vertices_of G by A1;
let e be object such that
A3: e Joins u,v,G;
e in G.edgesBetween(S) by A1,A2,A3,GLIB_000:32;
then
A4: e in the_Edges_of H by GLIB_000:def 37;
the_Target_of H = (the_Target_of G) | the_Edges_of H by GLIB_000:45;
then
A5: (the_Target_of H).e = (the_Target_of G).e by A4,FUNCT_1:49;
A6: (the_Source_of G).e = u & (the_Target_of G).e = v or (the_Source_of G).e
= v & (the_Target_of G).e = u by A3;
the_Source_of H = (the_Source_of G) | the_Edges_of H by GLIB_000:45;
then (the_Source_of H).e = (the_Source_of G).e by A4,FUNCT_1:49;
hence thesis by A4,A6,A5;
end;
theorem
for G being _Graph, W being Walk of G holds
W is Trail-like iff len W = 2*(card W.edges())+1
proof
let G be _Graph, W be Walk of G;
set WE = W.edges(), WES = W.edgeSeq();
W is Trail-like iff 2*card WE + 1 = 2*len WES+1 by FINSEQ_4:62;
hence thesis by GLIB_001:def 15;
end;
theorem Th21: :: Walk02
for G being _Graph, S being Subset of the_Vertices_of G
for H being removeVertices of G,S for W being Walk of G st
(for n being odd Nat st n <= len W holds not W.n in S)
holds W is Walk of H
proof
let G be _Graph, S be Subset of the_Vertices_of G;
let H be removeVertices of G,S;
let W be Walk of G such that
A1: for n being odd Nat st n <= len W holds not W.n in S;
A2: now
assume the_Vertices_of G\S = {};
then
A3: the_Vertices_of G c= S by XBOOLE_1:37;
W.last() in the_Vertices_of G;
hence contradiction by A1,A3;
end;
then
A4: the_Edges_of H = G.edgesBetween(the_Vertices_of G\S) by GLIB_000:def 37;
A5: W.edges() c= G.edgesBetween(W.vertices()) by GLIB_001:109;
A6: the_Vertices_of H = the_Vertices_of G\S by A2,GLIB_000:def 37;
now
let x be object such that
A7: x in W.vertices();
ex n being odd Element of NAT st n <= len W & W.n = x by A7,GLIB_001:87;
then not x in S by A1;
hence x in the_Vertices_of H by A6,A7,XBOOLE_0:def 5;
end;
then
A8: W.vertices() c= the_Vertices_of H;
then G.edgesBetween(W.vertices()) c= G.edgesBetween(the_Vertices_of H) by
GLIB_000:36;
then W.edges() c= G.edgesBetween(the_Vertices_of H) by A5;
hence thesis by A6,A4,A8,GLIB_001:170;
end;
theorem Th22: :: Walk03
for G being _Graph, a,b be set st a<>b for W being Walk of G st
W.vertices() = {a,b} holds ex e being set st e Joins a,b,G
proof
let G be _Graph, a,b be set such that
A1: a<>b;
let W be Walk of G such that
A2: W.vertices() = {a,b};
A3: W.first() in W.vertices() by GLIB_001:88;
A4: now
let x be set such that
A5: W.first() = x;
A6: x = a or x = b by A2,A3,A5,TARSKI:def 2;
A7: x in {x} by TARSKI:def 1;
let y be set such that
A8: y in {a,b} \ {x};
A9: y = a or y = b by A8,TARSKI:def 2;
set k = W.find(y);
A10: W.k = y by A2,A8,GLIB_001:def 19;
then k <> 1 by A5,A8,A7,XBOOLE_0:def 5;
then consider m being odd Nat such that
A11: m+2 = k by Th5;
A12: m < k by A11,NAT_1:16;
k <= len W by A2,A8,GLIB_001:def 19;
then
A13: m < len W by A11,NAT_1:16,XXREAL_0:2;
A14: m in NAT by ORDINAL1:def 12;
then W.m in {a,b} by A2,A13,GLIB_001:87;
then
A15: W.m = a or W.m = b by TARSKI:def 2;
W.(m+1) Joins W.m,W.k,G by A11,A13,A14,GLIB_001:def 3;
hence ex e being set st e Joins x,y,G by A2,A8,A7,A6,A10,A12,A13,A15,A9,
GLIB_001:def 19,XBOOLE_0:def 5;
end;
per cases by A2,A3,TARSKI:def 2;
suppose
A16: W.first() = a;
b in {b} by TARSKI:def 1;
then b in {a,b}\{a} by A1,ZFMISC_1:17;
hence thesis by A4,A16;
end;
suppose
A17: W.first() = b;
a in {a} by TARSKI:def 1;
then a in {a,b}\{b} by A1,ZFMISC_1:17;
then ex e be set st e Joins b,a,G by A4,A17;
hence thesis by GLIB_000:14;
end;
end;
theorem Th23: :: Walk04
for G being _Graph,
S being non empty Subset of the_Vertices_of G
for H being inducedSubgraph of G,S for W being Walk of G st
W.vertices() c= S holds W is Walk of H
proof
let G be _Graph, S be non empty Subset of the_Vertices_of G;
let H be inducedSubgraph of G,S;
A1: the_Vertices_of H = S by GLIB_000:def 37;
A2: the_Edges_of H = G.edgesBetween(S) by GLIB_000:def 37;
let W be Walk of G;
assume W.vertices() c= S;
then
A3: W.vertices() c= the_Vertices_of H by GLIB_000:def 37;
A4: W.edges() c= G.edgesBetween(W.vertices()) by GLIB_001:109;
G.edgesBetween(W.vertices()) c= G.edgesBetween(the_Vertices_of H) by A3,
GLIB_000:36;
then W.edges() c= the_Edges_of H by A1,A2,A4;
hence thesis by A3,GLIB_001:170;
end;
:: generalizes part of GLIB_001:175 and GLIB_001:176
:: should be in GLIB_001 ?
ThA26:
for G1, G2 being _Graph, W1 being Walk of G1, W2 being Walk of G2
st W1 = W2 holds W1 is Trail-like implies W2 is Trail-like by GLIB_001:86;
ThA27: ::: should be in GLIB_001
for G1, G2 being _Graph, W1 being Walk of G1, W2 being Walk of G2
st W1 = W2 holds W1 is Path-like implies W2 is Path-like by ThA26;
:: generalizes part of GLIB_001:175 and GLIB_001:176
:: into GLIB_001 ?
theorem Th24: :: Cyclelike01 ::: should be in GLIB_001
for G1, G2 being _Graph, W1 being Walk of G1, W2 being Walk of G2
st W1 = W2 holds W1 is Cycle-like implies W2 is Cycle-like
by ThA27, GLIB_001:121;
theorem Th25: :: Path01
for G being _Graph, P being Path of G, m, n being odd Nat
st m <= len P & n <= len P & P.m = P.n holds m = n or m = 1 & n = len P
or m = len P & n = 1
proof
let G be _Graph, P be Path of G, m, n be odd Nat such that
A1: m <= len P and
A2: n <= len P and
A3: P.m = P.n;
A4: m in NAT by ORDINAL1:def 12;
A5: n in NAT by ORDINAL1:def 12;
m=n or m<n or n<m by XXREAL_0:1;
hence thesis by A1,A2,A3,A4,A5,GLIB_001:def 28;
end;
theorem
for G being _Graph, P being Path of G st P is open for a,e,b being set
st not a in P.vertices() & b = P.first() & e Joins a,b,G holds
G.walkOf(a,e,b).append(P) is Path-like
proof
let G be _Graph, P be Path of G such that
A1: P is open;
let a,e,b be set such that
A2: not a in P.vertices() and
A3: b = P.first() and
A4: e Joins a,b,G;
set T = G.walkOf(a,e,b);
A5: T.last() = P.first() by A3,A4,GLIB_001:15;
set J = T.append(P);
3 in Seg 3 by FINSEQ_1:3;
then 3 in Seg (len T) by A4,GLIB_001:14;
then 3 in dom T by FINSEQ_1:def 3;
then J.3 = T.3 by GLIB_001:32;
then
A6: J.3 = T.last() by A4,GLIB_001:14;
then
A7: J.3 = b by A4,GLIB_001:15;
A8: now
let m,n be odd Nat such that
A9: m < n and
A10: n <= len J;
assume
A11: J.m = J.n;
A12: 1 <= m by ABIAN:12;
then 2*0+1 < n by A9,XXREAL_0:2;
then
A13: 1+2 <= n by Th4;
now
assume m = 1;
then J.m = J.first();
then J.m = T.first() by A5,GLIB_001:30;
then
A14: not J.m in P.vertices() by A2,A4,GLIB_001:15;
per cases by A13,XXREAL_0:1;
suppose
n=3;
hence contradiction by A3,A7,A11,A14,GLIB_001:88;
end;
suppose
A15: n > 3;
then not n in Seg 3 by FINSEQ_1:1;
then not n in Seg (len T) by A4,GLIB_001:14;
then
A16: not n in dom T by FINSEQ_1:def 3;
1 <= n by A15,XXREAL_0:2;
then n in dom J by A10,FINSEQ_3:25;
then consider j being Element of NAT such that
A17: j < len P and
A18: n = len T + j by A16,GLIB_001:34;
reconsider jj=j as even Nat by A18;
reconsider j1=jj+1 as odd Nat;
j+1 <= len P by A17,NAT_1:13;
then P.j1 in P.vertices() by GLIB_001:87;
hence contradiction by A5,A11,A14,A17,A18,GLIB_001:33;
end;
end;
then 2*0+1 < m by A12,XXREAL_0:1;
then
A19: 1+2 <= m by Th4;
then 3 <= n by A9,XXREAL_0:2;
then 1 <= n by XXREAL_0:2;
then n in Seg (len J) by A10,FINSEQ_1:1;
then
A20: n in dom J by FINSEQ_1:def 3;
3 < n by A9,A19,XXREAL_0:2;
then not n in Seg 3 by FINSEQ_1:1;
then not n in Seg (len T) by A4,GLIB_001:14;
then not n in dom T by FINSEQ_1:def 3;
then consider j being Element of NAT such that
A21: j < len P and
A22: n = len T + j by A20,GLIB_001:34;
reconsider jj=j as even Nat by A22;
reconsider j1=jj+1 as odd Nat;
A23: j1 <= len P by A21,NAT_1:13;
m < len J by A9,A10,XXREAL_0:2;
then
A24: m in dom J by A12,FINSEQ_3:25;
A25: J.n = P.(j+1) by A5,A21,A22,GLIB_001:33;
now
assume m = 3;
then
A26: J.m = P.1 by A3,A4,A6,GLIB_001:15;
0 <> j by A4,A9,A19,A22,GLIB_001:14;
then 2*0+1 < j1 by XREAL_1:8;
hence contradiction by A1,A11,A25,A23,A26,GLIB_001:147;
end;
then 3 < m by A19,XXREAL_0:1;
then not m in Seg 3 by FINSEQ_1:1;
then not m in Seg (len T) by A4,GLIB_001:14;
then not m in dom T by FINSEQ_1:def 3;
then consider k being Element of NAT such that
A27: k < len P and
A28: m = len T + k by A24,GLIB_001:34;
reconsider kk=k as even Nat by A28;
reconsider k1=kk+1 as odd Nat;
k < j by A9,A22,A28,XREAL_1:7;
then
A29: k1 < j1 by XREAL_1:8;
J.m = P.(k+1) by A5,A27,A28,GLIB_001:33;
hence contradiction by A1,A11,A25,A23,A29,GLIB_001:147;
end;
now
let m,n be odd Element of NAT such that
A30: m <= len J and
A31: n <= len J;
assume
A32: J.m = J.n;
then
A33: not n < m by A8,A30;
m >= n by A8,A31,A32;
hence n = m by A33,XXREAL_0:1;
end;
hence thesis by GLIB_001:146;
end;
theorem Th27: :: PathLike03
:: A similar theorem is needed for obtaining non closed Path
for G being _Graph, P,H being Path of G st
P.edges() misses H.edges() & P is open & H is non trivial &
H is open & P.vertices() /\ H.vertices() = { P.first(), P.last() } &
H.first() = P.last() & H.last() = P.first() holds
P.append(H) is Cycle-like
proof
let G be _Graph, P,H be Path of G such that
A1: P.edges() misses H.edges() and
A2: P is open and
A3: H is non trivial and
A4: H is open and
A5: P.vertices() /\ H.vertices() = { P.first(), P.last() } and
A6: H.first() = P.last() and
A7: H.last() = P.first();
set J = P.append(H);
A8: J.first() = P.first() by A6,GLIB_001:30;
A9: now
let m be odd Nat;
A10: 1 <= m by ABIAN:12;
assume m <= len P;
then m in dom P by A10,FINSEQ_3:25;
hence J.m = P.m by GLIB_001:32;
end;
A11: for m being odd Nat st m > len P & m <= len J holds m in dom J & not m
in dom P
proof
let m be odd Nat such that
A12: m > len P and
A13: m <= len J;
1 <= m by ABIAN:12;
hence thesis by A12,A13,FINSEQ_3:25;
end;
A14: len J + 1 + (-1) = len P + len H + (-1) by A6,GLIB_001:28;
A15: now
let m,n being odd Element of NAT such that
A16: m < n and
A17: n <= len J;
A18: m <= len J by A16,A17,XXREAL_0:2;
A19: 1 <= m by ABIAN:12;
per cases;
suppose
A20: m <= len P & n <= len P;
then
A21: P.m = J.m by A9;
P.m <> P.n by A2,A16,A20,GLIB_001:147;
hence J.m = J.n implies m = 1 & n = len J by A9,A20,A21;
end;
suppose
A22: m <= len P & n > len P;
then
A23: J.m = P.m by A9;
A24: not n in dom P by A11,A17,A22;
n in dom J by A11,A17,A22;
then consider j being Element of NAT such that
A25: j < len H and
A26: n = len P + j by A24,GLIB_001:34;
reconsider jj=j as even Nat by A26;
reconsider j1=jj+1 as odd Nat;
A27: j1 <= len H by A25,NAT_1:13;
A28: J.n = H.(j+1) by A6,A25,A26,GLIB_001:33;
now
assume
A29: J.m = J.n;
A30: now
j <> 0 by A22,A26;
then 0+1 < j1 by XREAL_1:8;
then
A31: H.(2*0+1) <> H.j1 by A4,A27,GLIB_001:147;
assume J.m = P.last();
hence contradiction by A6,A25,A26,A29,A31,GLIB_001:33;
end;
A32: J.m in P.vertices() by A22,A23,GLIB_001:87;
J.m in H.vertices() by A28,A27,A29,GLIB_001:87;
then
A33: J.m in P.vertices() /\ H.vertices() by A32,XBOOLE_0:def 4;
then
A34: J.n = H.last() by A5,A7,A29,A30,TARSKI:def 2;
A35: now
assume n < len J;
then j1 <> len H by A14,A26;
then
A36: j1 < len H by A27,XXREAL_0:1;
H.j1 = H.(len H) by A6,A25,A26,A34,GLIB_001:33;
hence contradiction by A4,A36,GLIB_001:147;
end;
A37: J.m = P.first() by A5,A33,A30,TARSKI:def 2;
now
assume 1 < m;
then P.m <> P.(2*0+1) by A2,A22,GLIB_001:147;
hence contradiction by A9,A22,A37;
end;
hence m = 1 & n = len J by A17,A19,A35,XXREAL_0:1;
end;
hence J.m = J.n implies m = 1 & n = len J;
end;
suppose
m > len P & n <= len P;
hence J.m = J.n implies m = 1 & n = len J by A16,XXREAL_0:2;
end;
suppose
A38: m > len P & n > len P;
then
A39: not n in dom P by A11,A17;
n in dom J by A11,A17,A38;
then consider j being Element of NAT such that
A40: j < len H and
A41: n = len P + j by A39,GLIB_001:34;
reconsider jj=j as even Nat by A41;
reconsider j1=jj+1 as odd Element of NAT;
A42: j1 <= len H by A40,NAT_1:13;
A43: not m in dom P by A11,A18,A38;
m in dom J by A11,A18,A38;
then consider k being Element of NAT such that
A44: k < len H and
A45: m = len P + k by A43,GLIB_001:34;
reconsider kk = k as even Nat by A45;
reconsider k1=kk+1 as odd Nat;
k < j by A16,A45,A41,XREAL_1:7;
then
A46: k1 < j1 by XREAL_1:8;
A47: J.(len P + j) = H.(j+1) by A6,A40,GLIB_001:33;
J.(len P + k) = H.(k+1) by A6,A44,GLIB_001:33;
hence J.m = J.n implies m = 1 & n = len J by A4,A45,A41,A47,A46,A42,
GLIB_001:147;
end;
end;
A48: H.edgeSeq() is one-to-one by GLIB_001:def 27;
now
assume len J = 1;
then
A49: 1 + 1 = len P + len H by A6,GLIB_001:28;
now
assume
A50: len P <> 1;
1 <= len P by Th2;
then 1 < len P by A50,XXREAL_0:1;
then len P + len H <= len P by A49,NAT_1:13;
then len P + len H + (-len P) <= len P + (-len P) by XREAL_1:7;
then len H <= 0;
hence contradiction;
end;
hence contradiction by A3,A49,GLIB_001:126;
end;
then
A51: J is non trivial by GLIB_001:126;
J.last() = P.first() by A6,A7,GLIB_001:30;
then
A52: J is closed by A8;
P.edgeSeq() is one-to-one by GLIB_001:def 27;
then P.edgeSeq() ^ H.edgeSeq() is one-to-one by A1,A48,FINSEQ_3:91;
then J.edgeSeq() is one-to-one by A6,GLIB_001:85;
then J is Trail-like;
then J is Path-like by A15;
hence thesis by A52,A51;
end;
theorem Th28:
for G being _Graph, W1,W2 being Walk of G st
W1.last() = W2.first() holds
W1.append(W2).length() = W1.length() + W2.length()
proof
let G being _Graph, P,H being Walk of G;
assume H.first() = P.last();
hence P.append(H).length() = len (P.edgeSeq() ^ H.edgeSeq()) by GLIB_001:85
.= P.length() + H.length() by FINSEQ_1:22;
end;
theorem Th29: :: Subgraph01
for G being _Graph,
A,B being non empty Subset of the_Vertices_of G st B c= A
for H1 being inducedSubgraph of G,A
for H2 being inducedSubgraph of H1,B holds H2 is inducedSubgraph of G,B
proof
let G be _Graph;
let A,B be non empty Subset of the_Vertices_of G such that
A1: B c= A;
let H1 be inducedSubgraph of G,A;
let H2 be inducedSubgraph of H1,B;
A2: the_Vertices_of H1 = A by GLIB_000:def 37;
then
A3: the_Vertices_of H2 = B by A1,GLIB_000:def 37;
A4: now
let e be set such that
A5: e in G.edgesBetween(B);
A6: (the_Target_of G).e in B by A5,GLIB_000:31;
A7: (the_Source_of G).e in B by A5,GLIB_000:31;
then e in G.edgesBetween(A) by A1,A5,A6,GLIB_000:31;
then
A8: e in the_Edges_of H1 by GLIB_000:def 37;
then
A9: (the_Target_of H1).e = (the_Target_of G).e by GLIB_000:def 32;
(the_Source_of H1).e = (the_Source_of G).e by A8,GLIB_000:def 32;
then e in H1.edgesBetween(B) by A7,A6,A8,A9,GLIB_000:31;
hence e in the_Edges_of H2 by A1,A2,GLIB_000:def 37;
end;
H1.edgesBetween(B) c= G.edgesBetween(B) by GLIB_000:76;
then the_Edges_of H2 c= G.edgesBetween(B) by A1,A2,GLIB_000:def 37;
then for x being object holds x in the_Edges_of H2
iff x in G.edgesBetween(B)
by A4;
then
A10: the_Edges_of H2 = G.edgesBetween(B) by TARSKI:2;
A11: now
let e be set such that
A12: e in the_Edges_of H2;
A13: (the_Target_of H2).e = (the_Target_of H1).e by A12,GLIB_000:def 32;
(the_Source_of H2).e = (the_Source_of H1).e by A12,GLIB_000:def 32;
hence
(the_Source_of H2).e = (the_Source_of G).e & (the_Target_of H2).e = (
the_Target_of G).e by A12,A13,GLIB_000:def 32;
end;
the_Edges_of H2 c= the_Edges_of H1;
then the_Edges_of H2 c= the_Edges_of G by XBOOLE_1:1;
then H2 is Subgraph of G by A3,A11,GLIB_000:def 32;
hence thesis by A3,A10,GLIB_000:def 37;
end;
theorem Th30: :: Subgraph01a
for G being _Graph,
A,B being non empty Subset of the_Vertices_of G st B c= A
for H1 being inducedSubgraph of G,A
for H2 being inducedSubgraph of G,B holds H2 is inducedSubgraph of H1,B
proof
let G be _Graph;
let A,B be non empty Subset of the_Vertices_of G such that
A1: B c= A;
let H1 be inducedSubgraph of G,A;
let H2 be inducedSubgraph of G,B;
A2: the_Edges_of H2 = G.edgesBetween(B) by GLIB_000:def 37;
the_Edges_of H1 = G.edgesBetween(A) by GLIB_000:def 37;
then
A3: the_Edges_of H2 c= the_Edges_of H1 by A1,A2,GLIB_000:36;
A4: now
let e be set such that
A5: e in the_Edges_of H2;
A6: (the_Target_of G).e = (the_Target_of H1).e by A3,A5,GLIB_000:def 32;
A7: (the_Target_of G).e in B by A2,A5,GLIB_000:31;
A8: (the_Source_of G).e in B by A2,A5,GLIB_000:31;
(the_Source_of G).e = (the_Source_of H1).e by A3,A5,GLIB_000:def 32;
hence e in H1.edgesBetween(B) by A3,A5,A6,A8,A7,GLIB_000:31;
end;
H1.edgesBetween(B) c= the_Edges_of H2 by A2,GLIB_000:76;
then
for x being object holds x in the_Edges_of H2 iff x in H1.edgesBetween(B)
by A4;
then
A9: the_Edges_of H2 = H1.edgesBetween(B) by TARSKI:2;
A10: the_Vertices_of H1 = A by GLIB_000:def 37;
A11: the_Vertices_of H2 = B by GLIB_000:def 37;
now
let e be set such that
A12: e in the_Edges_of H2;
thus (the_Source_of H2).e = (the_Source_of G).e by A12,GLIB_000:def 32
.= (the_Source_of H1).e by A3,A12,GLIB_000:def 32;
thus (the_Target_of H2).e = (the_Target_of G).e by A12,GLIB_000:def 32
.= (the_Target_of H1).e by A3,A12,GLIB_000:def 32;
end;
then H2 is Subgraph of H1 by A1,A10,A11,A3,GLIB_000:def 32;
hence thesis by A1,A10,A11,A9,GLIB_000:def 37;
end;
theorem Th31: :: Subgraph02
for G being _Graph,
S,T being non empty Subset of the_Vertices_of G st T c= S
for G2 being inducedSubgraph of G,S holds
G2.edgesBetween(T) = G.edgesBetween(T)
proof
let G be _Graph;
let S,T be non empty Subset of the_Vertices_of G such that
A1: T c= S;
let G2 be inducedSubgraph of G,S;
A2: the_Edges_of G2 = G.edgesBetween(S) by GLIB_000:def 37;
now
let e be object;
hereby
assume
A3: e in G.edgesBetween(T);
then
A4: (the_Source_of G).e in T by GLIB_000:31;
A5: (the_Target_of G).e in T by A3,GLIB_000:31;
A6: G.edgesBetween(T) c= G.edgesBetween(S) by A1,GLIB_000:36;
then
A7: (the_Target_of G2).e = (the_Target_of G).e by A2,A3,GLIB_000:def 32;
(the_Source_of G2).e = (the_Source_of G).e by A2,A3,A6,GLIB_000:def 32;
hence e in G2.edgesBetween(T) by A2,A3,A6,A4,A5,A7,GLIB_000:31;
end;
assume
A8: e in G2.edgesBetween(T);
then (the_Source_of G2).e in T by GLIB_000:31;
then
A9: (the_Source_of G).e in T by A8,GLIB_000:def 32;
(the_Target_of G2).e in T by A8,GLIB_000:31;
then
A10: (the_Target_of G).e in T by A8,GLIB_000:def 32;
e in the_Edges_of G2 by A8;
hence e in G.edgesBetween(T) by A9,A10,GLIB_000:31;
end;
hence thesis by TARSKI:2;
end;
:: we do not consider infinite graphs
scheme
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
let G be _finite _Graph;
defpred pP[non zero Nat] means for Gk being _finite _Graph st Gk.order() < $1
holds P[Gk];
A2: for n being non zero Nat holds pP[n] implies pP[n+1]
proof
let n be non zero Nat such that
A3: pP[n];
now
let Gk be _finite _Graph;
assume Gk.order() < n+1;
then Gk.order() <= n by NAT_1:13;
then Gk.order() < n or Gk.order() = n by XXREAL_0:1;
hence P[Gk] by A1,A3;
end;
hence thesis;
end;
A4: pP[1] by NAT_1:14;
for k being non zero Nat holds pP[k] from NAT_1:sch 10(A4,A2);
then for Gk being _finite _Graph st Gk.order()<G.order() holds P[Gk];
hence thesis by A1;
end;
:: should be in GLIBs
theorem Th32:
for G being _Graph, W being Walk of G st
W is open & W is Path-like holds W is vertex-distinct
proof
let G be _Graph, W be Walk of G;
assume that
A1: W is open and
A2: W is Path-like;
now
let m,n be odd Element of NAT such that
A3: m <= len W and
A4: n <= len W and
A5: W.m = W.n;
assume
A6: m <> n;
per cases by A6,XXREAL_0:1;
suppose
A7: m < n;
then
A8: W.n = W.last() by A2,A4,A5;
W.m = W.first() by A2,A4,A5,A7;
hence contradiction by A1,A5,A8;
end;
suppose
A9: m > n;
then
A10: W.n = W.first() by A2,A3,A5;
W.m = W.last() by A2,A3,A5,A9;
hence contradiction by A1,A5,A10;
end;
end;
hence thesis;
end;
:: PathLike15
:: should be in GLIB
theorem Th33:
for G being _Graph, P being Path of G st P is open & len P > 3
for e being object st e Joins P.last(),P.first(),G holds
P.addEdge(e) is Cycle-like
proof
let G be _Graph, W be Path of G such that
A1: W is open and
A2: len W > 3;
let e be object such that
A3: e Joins W.last(),W.first(),G;
A4: now
assume e in W.edges();
then consider
v1,v2 being Vertex of G, n being odd Element of NAT such that
A5: n+2 <= len W and
A6: v1 = W.n and
e = W.(n+1) and
A7: v2 = W.(n+2) and
A8: e Joins v1,v2,G by GLIB_001:103;
A9: n < len W by A5,XREAL_1:39;
per cases by A3,A8;
suppose
A10: v1 = W.first() & v2 = W.last();
now
assume
A11: 1 <> n;
1 <= n by Th2;
then 2*0+1 < n by A11,XXREAL_0:1;
hence contradiction by A1,A6,A9,A10,GLIB_001:147;
end;
hence contradiction by A1,A2,A7,A10,GLIB_001:147;
end;
suppose
v1 = W.last() & v2 = W.first();
hence contradiction by A1,A6,A9,GLIB_001:147;
end;
end;
set P = W.addEdge(e);
A12: P.last() = W.first() by A3,GLIB_001:63;
A13: len P = len W + 2*1 by A3,GLIB_001:64;
A14: now
let m,n be odd Element of NAT such that
A15: m < n and
A16: n <= len P;
m < len W + 2*1 by A13,A15,A16,XXREAL_0:2;
then
A17: m <= len W + 2 - 2 by Th3;
assume
A18: P.m = P.n;
1 <= m by Th2;
then
A19: m in dom W by A17,FINSEQ_3:25;
then
A20: W.m = P.m by A3,GLIB_001:65;
A21: now
assume n < len P;
then n < len W + 2*1 by A3,GLIB_001:64;
then
A22: n <= len W + 2 - 2 by Th3;
1 <= n by Th2;
then
A23: n in dom W by A22,FINSEQ_3:25;
W.n <> W.m by A1,A15,A22,GLIB_001:147;
hence contradiction by A3,A18,A20,A23,GLIB_001:65;
end;
then
A24: P.n = W.1 by A12,A16,XXREAL_0:1;
now
assume
A25: m <> 1;
1 <= m by Th2;
then 2*0+1 < m by A25,XXREAL_0:1;
then W.1 <> W.m by A1,A17,GLIB_001:147;
hence contradiction by A3,A18,A19,A24,GLIB_001:65;
end;
hence m = 1 & n = len P by A16,A21,XXREAL_0:1;
end;
e in W.last().edgesInOut() by A3,GLIB_000:62;
then P is Trail-like by A4,GLIB_001:142;
then
A26: P is Path-like by A14;
P.first() = W.first() by A3,GLIB_001:63;
then
A27: P is closed by A12;
P is non trivial by A3,GLIB_001:132;
hence thesis by A27,A26;
end;
begin :: Shortest topological path
definition
let G be _Graph, W be Walk of G;
attr W is minlength means
for W2 being Walk of G st W2 is_Walk_from W.first(),W.last() holds
len W2 >= len W;
end;
theorem Th34: :: WalkSubwalk00
for G being _Graph, W being Walk of G, S being Subwalk of W st
S.first() = W.first() & S.edgeSeq() = W.edgeSeq() holds S = W
proof
let G be _Graph, W be Walk of G, S be Subwalk of W such that
A1: S.first() = W.first() and
A2: S.edgeSeq() = W.edgeSeq();
defpred P[Nat] means $1 in dom S implies S.$1 = W.$1;
len S = 2*len W.edgeSeq() + 1 by A2,GLIB_001:def 15;
then
A3: len S = len W by GLIB_001:def 15;
A4: now
let k be Nat such that
A5: for n being Nat st n < k holds P[n];
A6: k in NAT by ORDINAL1:def 12;
per cases;
suppose
A7: k in dom S;
then
A8: 1 <= k by FINSEQ_3:25;
A9: k <= len S by A7,FINSEQ_3:25;
per cases;
suppose
A10: k is even;
then S.k = S.edgeSeq().(k div 2) by A6,A8,A9,GLIB_001:77;
hence P[k] by A2,A3,A8,A9,A10,GLIB_001:77;
end;
suppose
k is odd;
then reconsider kk=k as odd Nat;
per cases by A8,XXREAL_0:1;
suppose
k = 1;
hence P[k] by A1;
end;
suppose k > 2*0+1;
then
A11: 1+2 <= kk by Th4;
then
A12: 3+-2 <= k+-2 by XREAL_1:7;
3+-1 <= k+-1 by A11,XREAL_1:7;
then 0 <= k-1;
then reconsider k1=k-1 as Element of NAT by INT_1:3;
k1 < k by XREAL_1:44;
then
A13: k1 <= len S by A9,XXREAL_0:2;
3+-1 <= k+-1 by A11,XREAL_1:7;
then 1 <= k1 by XXREAL_0:2;
then k1 in dom S by A13,FINSEQ_3:25;
then
A14: S.k1 = W.k1 by A5,XREAL_1:44;
3+-2 <= k+-2 by A11,XREAL_1:7;
then reconsider k2=kk-2*1 as odd Element of NAT by INT_1:3;
A15: k2 < k by XREAL_1:44;
then k2 < len S by A9,XXREAL_0:2;
then
A16: S.(k2+1) Joins S.k2,S.(k2+2),G by GLIB_001:def 3;
k2 <= len S by A9,A15,XXREAL_0:2;
then k2 in dom S by A12,FINSEQ_3:25;
then
A17: S.k2 = W.k2 by A5,XREAL_1:44;
k2 < len W by A3,A9,A15,XXREAL_0:2;
then W.(k2+1) Joins W.k2,W.(k2+2),G by GLIB_001:def 3;
then S.k2 = S.k2 & S.k = W.k or S.k2 = W.k & S.k = S.k2
by A14,A17,A16;
hence P[k];
end;
end;
end;
suppose
not k in dom S;
hence P[k];
end;
end;
A18: for n being Nat holds P[n] from NAT_1:sch 4(A4);
for k being Nat st 1 <= k <= len S holds S.k = W.k by A18,FINSEQ_3:25;
hence thesis by A3,FINSEQ_1:14;
end;
theorem Th35: :: LenSubwalk00
for G being _Graph, W being Walk of G, S being Subwalk of W st
len S = len W holds S = W
proof
let G be _Graph, W be Walk of G, S be Subwalk of W such that
A1: len S = len W;
A2: len S = 2*len S.edgeSeq() +1 by GLIB_001:def 15;
A3: S.first() = W.first() by GLIB_001:161;
A4: len W = 2*len W.edgeSeq() +1 by GLIB_001:def 15;
ex es being Subset of W.edgeSeq() st S.edgeSeq() = Seq es by GLIB_001:def 32;
hence thesis by A1,A2,A4,A3,Th18,Th34;
end;
theorem
for G being _Graph, W being Walk of G st W is minlength holds W is Path-like
proof
let G be _Graph, W be Walk of G such that
A1: W is minlength and
A2: not W is Path-like;
set s = the Path-like Subwalk of W;
s is_Walk_from W.first(),W.last() by GLIB_001:def 32;
then
A3: len W <= len s by A1;
len s <= len W by GLIB_001:162;
hence contradiction by A2,A3,Th35,XXREAL_0:1;
end;
::$CT
theorem Th37:
for G being _Graph, W being Walk of G holds
(for P being Path of G st P is_Walk_from W.first(),W.last() holds
len P >= len W) implies W is minlength
proof
let G be _Graph, W be Walk of G;
assume
A1: for P2 being Path of G st P2 is_Walk_from W.first(),W.last() holds
len P2 >= len W;
now
let V be Walk of G such that
A2: V is_Walk_from W.first(),W.last();
set P3 = the Path-like Subwalk of V;
V.last() = W.last() by A2;
then
A3: P3.last()=W.last() by GLIB_001:161;
V.first() = W.first() by A2;
then P3.first()=W.first() by GLIB_001:161;
then P3 is_Walk_from W.first(),W.last() by A3;
then
A4: len W <= len P3 by A1;
len P3 <= len V by GLIB_001:162;
hence len V >= len W by A4,XXREAL_0:2;
end;
hence thesis;
end;
theorem Th38: :: TopPath02
for G being _Graph, W being Walk of G ex P being Path of G st
P is_Walk_from W.first(),W.last() & P is minlength
proof
let G being _Graph, W being Walk of G;
set X = { len P where P is Path of G : P is_Walk_from W.first(),W.last() };
set T = the Path-like Subwalk of W;
A1: T.last() = W.last() by GLIB_001:161;
T.first() = W.first() by GLIB_001:161;
then T is_Walk_from W.first(),W.last() by A1;
then
A2: len T in X;
X c= NAT
proof
let x be object;
assume x in X;
then
ex P being Path of G st x = len P & P is_Walk_from W.first(),W .last();
hence thesis;
end;
then reconsider X as non empty Subset of NAT by A2;
min X in X by XXREAL_2:def 7;
then consider P being Path of G such that
A3: len P = min X and
A4: P is_Walk_from W.first(),W.last();
A5: P.first() = W.first() by A4;
take P;
thus P is_Walk_from W.first(),W.last() by A4;
let W2 be Walk of G such that
A6: W2 is_Walk_from P.first(),P.last();
A7: P.last() = W2.last() by A6;
set T = the Path-like Subwalk of W2;
A8: T.first() = W2.first() by GLIB_001:161;
A9: T.last() = W2.last() by GLIB_001:161;
A10: P.last() = W.last() by A4;
P.first() = W2.first() by A6;
then T is_Walk_from W.first(),W.last() by A7,A5,A10,A8,A9;
then len T in X;
then
A11: len P <= len T by A3,XXREAL_2:def 7;
len T <= len W2 by GLIB_001:162;
hence thesis by A11,XXREAL_0:2;
end;
theorem Th39: :: TopPath03
for G being _Graph, W being Walk of G st W is minlength holds
for m,n being odd Nat st m+2 < n & n <= len W holds
not ex e being object st e Joins W.m,W.n,G
proof
let G be _Graph;
let P be Walk of G such that
A1: P is minlength;
let m,n be odd Nat such that
A2: m+2 < n and
A3: n <= len P;
A4: len P - n + (m + 2) < len P - n + n by A2,XREAL_1:8;
m+0 <= m+2 by XREAL_1:7;
then m <= n by A2,XXREAL_0:2;
then
A5: m <= len P by A3,XXREAL_0:2;
set P3 = P.cut(n,len P);
A6: n in NAT by ORDINAL1:def 12;
then
A7: P3.last() = P.last() by A3,GLIB_001:37;
set P1 = P.cut(1,m);
let e be object such that
A8: e Joins P.m,P.n,G;
set P2 = P1.addEdge(e);
set P4 = P2.append(P3);
A9: 2*0+1 <= m by ABIAN:12;
A10: m in NAT by ORDINAL1:def 12;
then
A11: len P1 + 1 = m + 1 by A9,A5,GLIB_001:36;
A12: P1.last() = P.m by A10,A9,A5,GLIB_001:37;
then
A13: P2.last() = P.n by A8,GLIB_001:63;
P1.first() = P.first() by A10,A9,A5,GLIB_001:37;
then
A14: P2.first() = P.first() by A8,A12,GLIB_001:63;
P3.first() = P.n by A3,A6,GLIB_001:37;
then
A15: P4 is_Walk_from P.first(),P.last() by A14,A13,A7,GLIB_001:30;
P3.first() = P.n by A3,A6,GLIB_001:37;
then
A16: len P4 + 1 = len P2 + len P3 by A13,GLIB_001:28;
P1.last() = P.m by A10,A9,A5,GLIB_001:37;
then
A17: len P2 = m + 2 by A8,A11,GLIB_001:64;
len P3 + n = len P+1 by A3,A6,GLIB_001:36;
hence contradiction by A1,A17,A15,A16,A4;
end;
theorem Th40: :: TopPath04
for G being _Graph,
S being non empty Subset of the_Vertices_of G
for H being inducedSubgraph of G,S for W being Walk of H st W is minlength
for m,n being odd Nat st m+2 < n & n <= len W holds
not ex e being object st e Joins W.m,W.n,G
proof
let G be _Graph, S be non empty Subset of the_Vertices_of G;
let GA be inducedSubgraph of G,S;
let P be Walk of GA;
A1: S = the_Vertices_of GA by GLIB_000:def 37;
assume
A2: P is minlength;
now
let m,n be odd Nat such that
A3: m+2 < n and
A4: n <= len P;
m + 0 <= m + 2 by XREAL_1:7;
then
A5: m <= n by A3,XXREAL_0:2;
n in NAT by ORDINAL1:def 12;
then
A6: P.n in the_Vertices_of GA by A4,GLIB_001:7;
m in NAT by ORDINAL1:def 12;
then
A7: P.m in the_Vertices_of GA by A4,A5,GLIB_001:7,XXREAL_0:2;
let e be object;
assume e Joins P.m,P.n,G;
hence contradiction by A2,A1,A3,A4,A7,A6,Th19,Th39;
end;
hence thesis;
end;
theorem Th41: :: TopPath05
for G being _Graph for W being Walk of G st W is minlength
for m,n being odd Nat st m<=n & n<=len W holds
W.cut(m,n) is minlength
proof
let G be _Graph, W be Walk of G such that
A1: W is minlength;
let m,n be odd Nat such that
A2: m <= n and
A3: n <= len W;
set S = W.cut(m,n);
assume not S is minlength;
then consider M being Walk of G such that
A4: M is_Walk_from S.first(),S.last() and
A5: len M < len S;
set R = W.cut(1,m);
A6: 2*0+1 <= m by ABIAN:12;
set T = W.cut(n,len W);
A7: n in NAT by ORDINAL1:def 12;
then
A8: T.first() = W.n by A3,GLIB_001:37;
set A = R.append(M);
A9: m in NAT by ORDINAL1:def 12;
A10: m <= len W by A2,A3,XXREAL_0:2;
then
A11: R.last() = W.m by A6,A9,GLIB_001:37;
S.first() = W.m by A2,A3,A9,A7,GLIB_001:37;
then
A12: M.first() = W.m by A4;
then len A + 1 = len R + len M by A11,GLIB_001:28;
then
A13: len A + 1 < len R + len S by A5,XREAL_1:8;
set B = A.append(T);
S.last() = W.n by A2,A3,A9,A7,GLIB_001:37;
then M.last() = W.n by A4;
then
A14: A.last() = W.n by A11,A12,GLIB_001:30;
then
A15: len B + 1 = len A + len T by A8,GLIB_001:28;
A16: len R + 1 = m + 1 by A6,A10,A9,GLIB_001:36;
len S + m = n + 1 by A2,A3,A9,A7,GLIB_001:36;
then len A + 1 - 1 < n + 1 - 1 by A16,A13,XREAL_1:14;
then
A17: len B + 1 < len T + n by A15,XREAL_1:8;
len T + n = len W + 1 by A3,A7,GLIB_001:36;
then
A18: len B + 1 - 1 < len W + 1 - 1 by A17,XREAL_1:14;
T.last() = W.(len W) by A3,A7,GLIB_001:37;
then
A19: B.last() = W.last() by A8,A14,GLIB_001:30;
R.first() = W.1 by A6,A10,A9,GLIB_001:37;
then A.first() = W.1 by A11,A12,GLIB_001:30;
then B.first() = W.first() by A8,A14,GLIB_001:30;
then B is_Walk_from W.first(),W.last() by A19;
hence contradiction by A1,A18;
end;
theorem
for G being _Graph st G is connected
for A,B being non empty Subset of the_Vertices_of G st
A misses B holds ex P being Path of G st P is minlength &
P is non trivial & P.first() in A & P.last() in B & for n being odd Nat
st 1 < n & n < len P holds not P.n in A & not P.n in B
proof
let G be _Graph such that
A1: G is connected;
let A,B be non empty Subset of the_Vertices_of G such that
A2: A misses B;
set X = { len P where P is Path of G : P.first() in A & P.last() in B };
A3: X c= NAT
proof
let x be object;
assume x in X;
then ex P being Path of G st x = len P & P.first() in A & P.last() in B;
hence thesis;
end;
consider b being object such that
A4: b in B by XBOOLE_0:def 1;
reconsider b as Vertex of G by A4;
consider a being object such that
A5: a in A by XBOOLE_0:def 1;
reconsider a as Vertex of G by A5;
consider W being Walk of G such that
A6: W is_Walk_from a,b by A1;
consider W2 being Path of G such that
A7: W2 is_Walk_from W.first(),W.last() and
W2 is minlength by Th38;
W.last() = b by A6;
then
A8: W2.last() in B by A4,A7;
W.first() = a by A6;
then W2.first() in A by A5,A7;
then len W2 in X by A8;
then reconsider X as non empty Subset of NAT by A3;
min X in X by XXREAL_2:def 7;
then consider M being Path of G such that
A9: len M = min X and
A10: M.first() in A and
A11: M.last() in B;
now
let P2 be Path of G such that
A12: P2 is_Walk_from M.first(),M.last();
A13: P2.last() in B by A11,A12;
P2.first() in A by A10,A12;
then len P2 in X by A13;
hence len P2 >= len M by A9,XXREAL_2:def 7;
end;
then
A14: M is minlength by Th37;
A15: now
let n be odd Nat such that
A16: 1 < n and
A17: n < len M;
reconsider nn = n as Element of NAT by ORDINAL1:def 12;
assume
A18: M.n in A or M.n in B;
per cases by A18;
suppose
A19: M.n in A;
reconsider T = M.cut(nn,len M) as Path of G;
A20: T.last() in B by A11,A17,GLIB_001:37;
len T + nn = len M+1 by A17,GLIB_001:36;
then
A21: len T + 0 < len M + 1 + (-n) + (n + (-1)) by A16,XREAL_1:8;
T.first() in A by A17,A19,GLIB_001:37;
then len T in X by A20;
hence contradiction by A9,A21,XXREAL_2:def 7;
end;
suppose
A22: M.n in B;
reconsider T = M.cut(1,nn) as Path of G;
A23: 2*0+1 <= n by A16;
then
A24: T.last() = M.nn by A17,GLIB_001:37;
2*0+1 <= n by A16;
then
A25: len T + 1 = nn + 1 by A17,GLIB_001:36;
T.first() = M.1 by A17,A23,GLIB_001:37;
then len T in X by A10,A22,A24;
hence contradiction by A9,A17,A25,XXREAL_2:def 7;
end;
end;
M.first() <> M.last() by A2,A10,A11,XBOOLE_0:def 4;
then M is non trivial by GLIB_001:127;
hence thesis by A10,A11,A14,A15;
end;
begin :: Adjacency and complete graphs
definition
let G be _Graph, a,b be Vertex of G;
pred a,b are_adjacent means :: DefAdjacent
:Def3:
ex e being object st e Joins a,b,G;
symmetry by GLIB_000:14;
end;
theorem Th43: :: VAdjacent00
for G1,G2 being _Graph st G1 == G2 for u1,v1 being Vertex of G1
st u1,v1 are_adjacent for u2,v2 being Vertex of G2 st u1=u2 & v1=v2 holds u2,v2
are_adjacent
proof
let G1,G2 be _Graph such that
A1: G1 == G2;
let u1,v1 be Vertex of G1;
assume u1,v1 are_adjacent;
then consider e being object such that
A2: e Joins u1,v1,G1;
let u2,v2 be Vertex of G2 such that
A3: u1=u2 and
A4: v1=v2;
e Joins u2,v2,G2 by A1,A3,A4,A2;
hence thesis;
end;
theorem Th44: :: VAdjacent01
for G being _Graph, S being non empty Subset of the_Vertices_of
G for H being inducedSubgraph of G,S for u, v being Vertex of G, t, w being
Vertex of H st u = t & v = w holds u,v are_adjacent iff t,w are_adjacent
proof
let G be _Graph, S be non empty Subset of the_Vertices_of G;
let H be inducedSubgraph of G,S;
let u, v be Vertex of G, t, w be Vertex of H such that
A1: u = t and
A2: v = w;
S = the_Vertices_of H by GLIB_000:def 37;
hence u,v are_adjacent implies t,w are_adjacent by A1,A2,Th19;
assume t,w are_adjacent;
then consider e being object such that
A3: e Joins t,w,H;
e Joins u,v,G by A1,A2,A3,GLIB_000:72;
hence thesis;
end;
theorem Th45: :: PathLike05
for G being _Graph, W being Walk of G st W.first() <> W.last() &
not W.first(),W.last() are_adjacent holds W.length() >= 2
proof
let G be _Graph, W be Walk of G such that
A1: W.first() <> W.last() and
A2: not W.first(),W.last() are_adjacent;
set l = W.length();
assume l < 2;
then l < 1+1;
then
A3: l <= 1 by NAT_1:13;
per cases by A3,NAT_1:25;
suppose
l = 0;
then W is trivial;
hence contradiction by A1,GLIB_001:127;
end;
suppose
l = 1;
then
A4: len W = 2*1+1 by GLIB_001:112
.= 3;
1 = 2*0+1;
then W.(1+1) Joins W.1,W.(1+2),G by A4,GLIB_001:def 3;
hence contradiction by A2,A4;
end;
end;
theorem Th46: :: PathBuilder00
:: add sequences of vertices and edges:: PathBuilder01
for G being _Graph, v1,v2,v3 being Vertex of G st v1<>v2 & v1<>
v3 & v2<>v3 & v1,v2 are_adjacent & v2,v3 are_adjacent
ex P being Path of G, e1,e2 being object
st P is open & len P = 5 & P.length() = 2 & e1 Joins v1,v2,G & e2
Joins v2,v3,G & P.edges() = {e1,e2} & P.vertices() = {v1,v2,v3} & P.1 = v1 & P.
3 = v2 & P.5 = v3
proof
let G be _Graph;
let v1,v2,v3 be Vertex of G such that
A1: v1 <> v2 and
A2: v1 <> v3 and
A3: v2 <> v3 and
A4: v1,v2 are_adjacent and
A5: v2,v3 are_adjacent;
consider e1 being object such that
A6: e1 Joins v1,v2,G by A4;
set P1 = G.walkOf(v1,e1,v2);
A7: P1.vertices() = {v1,v2} by A6,GLIB_001:91;
then
A8: not v3 in P1.vertices() by A2,A3,TARSKI:def 2;
consider e2 being object such that
A9: e2 Joins v2,v3,G by A5;
set P = P1.addEdge(e2);
A10: P1.last() = v2 by A6,GLIB_001:15;
then
A11: P.last() = v3 by A9,GLIB_001:63;
A12: P1.first() = v1 by A6,GLIB_001:15;
then
A13: P.first() = v1 by A9,A10,GLIB_001:63;
P1 is open by A1,A12,A10;
then reconsider P as Path of G by A9,A10,A8,GLIB_001:151;
take P,e1,e2;
thus P is open by A2,A13,A11;
A14: len P1 = 3 by A6,GLIB_001:14;
then
A15: len P = 3 + 2 by A9,A10,GLIB_001:64;
hence len P = 5;
5 = 2*P.length() + 1 by A15,GLIB_001:112;
hence P.length() = 2;
thus e1 Joins v1,v2,G by A6;
thus e2 Joins v2,v3,G by A9;
P1.edges() = {e1} by A6,GLIB_001:108;
then P.edges() = {e1} \/ {e2} by A9,A10,GLIB_001:111;
hence P.edges() = {e1,e2} by ENUMSET1:1;
P.vertices() = {v1,v2} \/ {v3} by A9,A10,A7,GLIB_001:95;
hence P.vertices() = {v1,v2,v3} by ENUMSET1:3;
thus P.1 = v1 by A13;
3 in dom P1 by A14,FINSEQ_3:25;
hence P.3 = P1.3 by A9,A10,GLIB_001:65
.= v2 by A6,A10,GLIB_001:14;
thus thesis by A11,A15;
end;
theorem Th47:
for G being _Graph, v1,v2,v3,v4 being Vertex of G st v1<>v2 & v1
<>v3 & v2<>v3 & v2<>v4 & v3<>v4 & v1,v2 are_adjacent & v2,v3 are_adjacent & v3,
v4 are_adjacent ex P being Path of G st len P = 7 & P.length() = 3 & P
.vertices() = {v1,v2,v3,v4} & P.1 = v1 & P.3 = v2 & P.5 = v3 & P.7 = v4
proof
let G be _Graph, v1,v2,v3,v4 be Vertex of G such that
A1: v1<>v2 and
A2: v1<>v3 and
A3: v2<>v3 and
A4: v2<>v4 and
A5: v3<>v4 and
A6: v1,v2 are_adjacent and
A7: v2,v3 are_adjacent and
A8: v3,v4 are_adjacent;
consider R being Path of G,e1,e2 being object such that
A9: R is open and
A10: len R = 5 and
R.length() = 2 and
A11: e1 Joins v1,v2,G and
A12: e2 Joins v2,v3,G and
A13: R.edges() = {e1,e2} and
A14: R.vertices() = {v1,v2,v3} and
A15: R.1 = v1 and
A16: R.3 = v2 and
A17: R.5 = v3 by A1,A2,A3,A6,A7,Th46;
consider e3 being object such that
A18: e3 Joins v3,v4,G by A8;
A19: for n being odd Element of NAT st 1 < n & n <= len R holds R.n <> v4
proof
let n be odd Element of NAT such that
A20: 1 < n and
A21: n <= len R;
per cases by A10,A20,A21,Th8,XXREAL_0:2;
suppose
n = 3;
hence thesis by A4,A16;
end;
suppose
n = 5;
hence thesis by A5,A17;
end;
end;
A22: e2 <> e3 by A4,A18,A12;
set P = R.addEdge(e3);
e1 <> e3 by A2,A3,A18,A11;
then not e3 in R.edges() by A13,A22,TARSKI:def 2;
then reconsider P as Path of G by A18,A9,A10,A17,A19,GLIB_001:150;
take P;
A23: len P = 5 + 2 by A18,A10,A17,GLIB_001:64;
hence len P = 7;
7 = 2*P.length() + 1 by A23,GLIB_001:112;
hence P.length() = 3;
P.vertices() = {v1,v2,v3} \/ {v4} by A18,A10,A14,A17,GLIB_001:95;
hence P.vertices() = {v1,v2,v3,v4} by ENUMSET1:6;
1 in dom R by A10,FINSEQ_3:25;
hence P.1 = v1 by A18,A10,A15,A17,GLIB_001:65;
3 in dom R by A10,FINSEQ_3:25;
hence P.3 = v2 by A18,A10,A16,A17,GLIB_001:65;
5 in dom R by A10,FINSEQ_3:25;
hence P.5 = v3 by A18,A10,A17,GLIB_001:65;
P.last() = v4 by A18,A10,A17,GLIB_001:63;
hence thesis by A23;
end;
definition
let G be _Graph, S be set;
func G.AdjacentSet(S) -> Subset of the_Vertices_of G equals
{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
proof
set X = {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)};
now
let x be object;
assume x in X;
then
ex u being Vertex of G st u=x &( not u in S)& ex v being Vertex of
G st v in S & u,v are_adjacent;
hence x in the_Vertices_of G;
end;
hence thesis by TARSKI:def 3;
end;
end;
theorem
for G being _Graph, S, x being set st x in G.AdjacentSet(S) holds not x in S
proof
let G be _Graph, S,x be set;
assume x in G.AdjacentSet(S);
then ex t being Vertex of G st t=x &( not t in S)& ex v being Vertex of G
st v in S & t,v are_adjacent;
hence thesis;
end;
theorem Th49: :: Adjacent00
for G being _Graph, S being set for u being Vertex of G holds u
in G.AdjacentSet(S) iff not u in S & ex v being Vertex of G st v in S & u,v
are_adjacent
proof
let G be _Graph, S be set;
let u be Vertex of G;
hereby
assume u in G.AdjacentSet(S);
then
ex t being Vertex of G st u=t &( not t in S)& ex v being Vertex of G
st v in S & t,v are_adjacent;
hence not u in S & ex v being Vertex of G st v in S & u,v are_adjacent;
end;
assume that
A1: not u in S and
A2: ex v being Vertex of G st v in S & u,v are_adjacent;
thus thesis by A1,A2;
end;
theorem Th50: :: Adjacent01
for G1,G2 being _Graph st G1 == G2 for S being set holds G1
.AdjacentSet(S) = G2.AdjacentSet(S)
proof
let G1,G2 be _Graph such that
A1: G1 == G2;
let S be set;
A2: now
let x be object such that
A3: x in G2.AdjacentSet(S);
reconsider t2 = x as Vertex of G2 by A3;
A4: not t2 in S by A3,Th49;
consider v2 being Vertex of G2 such that
A5: v2 in S and
A6: t2,v2 are_adjacent by A3,Th49;
reconsider t1 = t2, v1 = v2 as Vertex of G1 by A1;
t1,v1 are_adjacent by A1,A6,Th43;
hence x in G1.AdjacentSet(S) by A4,A5;
end;
now
let x be object such that
A7: x in G1.AdjacentSet(S);
reconsider t1 = x as Vertex of G1 by A7;
A8: not t1 in S by A7,Th49;
consider v1 being Vertex of G1 such that
A9: v1 in S and
A10: t1,v1 are_adjacent by A7,Th49;
reconsider t2 = t1, v2 = v1 as Vertex of G2 by A1;
t2,v2 are_adjacent by A1,A10,Th43;
hence x in G2.AdjacentSet(S) by A8,A9;
end;
hence thesis by A2,TARSKI:2;
end;
theorem Th51: :: AdjacentV00
for G being _Graph, u,v being Vertex of G holds u in G
.AdjacentSet({v}) iff u <> v & v,u are_adjacent
proof
let G be _Graph, u,v be Vertex of G;
A1: v in {v} by TARSKI:def 1;
hereby
assume
A2: u in G.AdjacentSet({v});
then consider x being Vertex of G such that
A3: x in {v} and
A4: u,x are_adjacent by Th49;
x = v by A3,TARSKI:def 1;
hence u <> v & v,u are_adjacent by A2,A3,A4,Th49;
end;
assume that
A5: u <> v and
A6: v,u are_adjacent;
not u in {v} by A5,TARSKI:def 1;
hence thesis by A6,A1;
end;
theorem
for G being _Graph, x,y being set holds x in G.AdjacentSet({y}) iff y
in G.AdjacentSet({x})
proof
let G be _Graph, x,y be set;
hereby
assume
A1: x in G.AdjacentSet({y});
then reconsider xg = x as Vertex of G;
now
consider vy being Vertex of G such that
A2: vy in {y} and
vy,xg are_adjacent by A1,Th49;
assume
A3: not y in the_Vertices_of G;
vy = y by A2,TARSKI:def 1;
hence contradiction by A3;
end;
then reconsider yg = y as Vertex of G;
A4: xg,yg are_adjacent by A1,Th51;
xg <> yg by A1,Th51;
hence y in G.AdjacentSet({x}) by A4,Th51;
end;
assume
A5: y in G.AdjacentSet({x});
then reconsider yg = y as Vertex of G;
now
consider vx being Vertex of G such that
A6: vx in {x} and
vx,yg are_adjacent by A5,Th49;
assume
A7: not x in the_Vertices_of G;
vx = x by A6,TARSKI:def 1;
hence contradiction by A7;
end;
then reconsider xg = x as Vertex of G;
A8: xg,yg are_adjacent by A5,Th51;
xg <> yg by A5,Th51;
hence thesis by A8,Th51;
end;
theorem
for G being _Graph, C being Path of G st C is Cycle-like & C.length()
> 3 for x being Vertex of G st x in C.vertices() ex m,n being odd Nat st m+2 <
n & n <= len C & not (m=1 & n = len C) & not (m=1 & n = len C-2) & not (m=3 & n
= len C) & C.m <> C.n & C.m in G.AdjacentSet({x}) & C.n in G.AdjacentSet({x})
proof
let G be _Graph, C be Path of G such that
A1: C is Cycle-like and
A2: C.length() > 3;
C.length() >= 3+1 by A2,NAT_1:13;
then 2*C.length() >= 2*4 by XREAL_1:64;
then 2*C.length() + 1 >= 8 + 1 by XREAL_1:7;
then
A3: len C >= 9 by GLIB_001:112;
let x be Vertex of G;
assume x in C.vertices();
then consider n being odd Element of NAT such that
A4: n <= len C and
A5: C.n = x by GLIB_001:87;
A6: 0+1 <= n by ABIAN:12;
per cases;
suppose
A7: n = 1 or n = len C;
reconsider i=2*1+1 as odd Nat;
reconsider k=2*0+1 as odd Nat;
A8: len C + 0 > 9 + (-6) by A3,XREAL_1:8;
then reconsider Ci=C.i as Vertex of G by GLIB_001:7;
A9: now
per cases by A7;
suppose
n = 1;
hence x = C.k by A5;
end;
suppose
n = len C;
then x = C.last() by A5;
then x = C.first() by A1,GLIB_001:def 24;
hence x = C.k;
end;
end;
then
A10: x <> Ci by A8,GLIB_001:def 28;
len C + (-2) >= 9 + (-2) by A3,XREAL_1:7;
then len C - 2*1 >= 0 by XXREAL_0:2;
then len C - 2 is odd Element of NAT by INT_1:3;
then reconsider j=len C-2 as odd Nat;
take i, j;
A11: len C + (-2) >= 9 + (-2) by A3,XREAL_1:7;
hence i+2 < j by XXREAL_0:2;
A12: len C + 0 > len C+(-2) by XREAL_1:8;
hence j <= len C;
thus not (i=1 & j=len C) & not (i=1 & j=len C-2) & not (i=3 & j=len C);
hereby
assume
A13: C.i = C.j;
i+2+(-2) < j+0 by A11,XXREAL_0:2;
hence contradiction by A12,A13,GLIB_001:def 28;
end;
len C + 0 > 9 + (-8) by A3,XREAL_1:8;
then C.(k+1) Joins C.k,C.i,G by GLIB_001:def 3;
then x,Ci are_adjacent by A9;
hence C.i in G.AdjacentSet({x}) by A10,Th51;
A14: j in NAT by ORDINAL1:def 12;
then reconsider Cj=C.j as Vertex of G by A12,GLIB_001:7;
A15: now
per cases by A7;
suppose
n = 1;
then x = C.first() by A5;
then x = C.last() by A1,GLIB_001:def 24;
hence x = C.(j+2);
end;
suppose
n = len C;
hence x = C.(j+2) by A5;
end;
end;
A16: now
assume x = Cj;
then
A17: j = 1 by A14,A12,A15,GLIB_001:def 28;
j+2 = len C;
hence contradiction by A3,A17;
end;
C.(j+1) Joins Cj,x,G by A14,A12,A15,GLIB_001:def 3;
then x,Cj are_adjacent by Def3;
hence thesis by A16,Th51;
end;
suppose
A18: not (n = 1 or n = len C);
then 2*0+1 < n by A6,XXREAL_0:1;
then 1+2 <= n by Th4;
then 3+(-2) <= n+(-2) by XREAL_1:7;
then 0 <= n-2*1;
then n-2 is odd Element of NAT by INT_1:3;
then reconsider i=n-2 as odd Nat;
A19: i+0 < i+2 by XREAL_1:8;
then reconsider Ci=C.i as Vertex of G by A4,GLIB_001:7,XXREAL_0:2;
reconsider j=n+2 as odd Nat;
A20: n < len C by A4,A18,XXREAL_0:1;
then
A21: n+2 <= len C -2 + 2 by Th4;
then reconsider Cj=C.j as Vertex of G by GLIB_001:7;
A22: now
A23: n+2 > n+0 by XREAL_1:8;
assume Cj = x;
hence contradiction by A5,A18,A21,A23,GLIB_001:def 28;
end;
take i,j;
n+0 < n+2 by XREAL_1:8;
hence i+2 < j & j <= len C by A20,Th4;
A24: now
assume that
A25: i = 1 and
A26: j = len C;
j = i + 4;
hence contradiction by A3,A25,A26;
end;
hence not (i = 1 & j = len C);
hereby
assume that
A27: i = 1 and
A28: j = len C-2;
len C+(-2) >= 9+(-3) by A3,XREAL_1:7;
hence contradiction by A27,A28;
end;
hereby
assume that
A29: i = 3 and
A30: j = len C;
j = i + 4;
hence contradiction by A3,A29,A30;
end;
A31: i in NAT by ORDINAL1:def 12;
A32: now
A33: n+0 > n+(-2) by XREAL_1:8;
assume Ci = x;
hence contradiction by A4,A5,A18,A31,A33,GLIB_001:def 28;
end;
A34: n+2 <= len C-2+2 by A20,Th4;
hereby
A35: i+2+(-2) < j+0 by XREAL_1:8;
assume C.i = C.j;
hence contradiction by A31,A34,A24,A35,GLIB_001:def 28;
end;
i < len C by A4,A19,XXREAL_0:2;
then C.(i+1) Joins C.i,C.(i+2),G by A31,GLIB_001:def 3;
then x,Ci are_adjacent by A5,Def3;
hence C.i in G.AdjacentSet({x}) by A32,Th51;
C.(n+1) Joins C.n,C.j,G by A20,GLIB_001:def 3;
then x,Cj are_adjacent by A5;
hence thesis by A22,Th51;
end;
end;
theorem Th54: :: Cycle01a
for G being _Graph, C being Path of G st C is Cycle-like & C
.length() > 3 for x being Vertex of G st x in C.vertices() ex m,n being odd
Nat st m+2 < n & n <= len C & C.m <> C.n &
C.m in G.AdjacentSet({x})
& C.n in G.AdjacentSet({x}) &
for e being object st e in C.edges() holds not e Joins C.m,C.n,G
proof
let G be _Graph, C be Path of G such that
A1: C is Cycle-like and
A2: C.length() > 3;
C.length() >= 3+1 by A2,NAT_1:13;
then 2*C.length() >= 2*4 by XREAL_1:64;
then 2*C.length() + 1 >= 8 + 1 by XREAL_1:7;
then
A3: len C >= 9 by GLIB_001:112;
let x be Vertex of G;
assume x in C.vertices();
then consider n being odd Element of NAT such that
A4: n <= len C and
A5: C.n = x by GLIB_001:87;
A6: 0+1 <= n by ABIAN:12;
per cases;
suppose
A7: n = 1 or n = len C;
reconsider k=2*0+1 as odd Nat;
A8: now
per cases by A7;
suppose
n = 1;
hence x = C.k by A5;
end;
suppose
n = len C;
then x = C.last() by A5;
then x = C.first() by A1,GLIB_001:def 24;
hence x = C.k;
end;
end;
len C + (-2) >= 9 + (-2) by A3,XREAL_1:7;
then len C - 2*1 >= 0 by XXREAL_0:2;
then len C-2 is odd Element of NAT by INT_1:3;
then reconsider j=len C-2 as odd Nat;
reconsider i=2*1+1 as odd Nat;
take i, j;
A9: len C + (-2) >= 9 + (-2) by A3,XREAL_1:7;
hence i+2 < j by XXREAL_0:2;
A10: len C + 0 > len C+(-2) by XREAL_1:8;
hence j <= len C;
i < j by A9,XXREAL_0:2;
then
A11: i < len C by A10,XXREAL_0:2;
hereby
assume
A12: C.i = C.j;
i+2+(-2) < j+0 by A9,XXREAL_0:2;
hence contradiction by A10,A12,GLIB_001:def 28;
end;
A13: len C + 0 > 9 + (-6) by A3,XREAL_1:8;
then reconsider Ci=C.i as Vertex of G by GLIB_001:7;
len C + 0 > 9 + (-8) by A3,XREAL_1:8;
then C.(k+1) Joins C.k,C.i,G by GLIB_001:def 3;
then
A14: x,Ci are_adjacent by A8;
x <> Ci by A13,A8,GLIB_001:def 28;
hence C.i in G.AdjacentSet({x}) by A14,Th51;
A15: j <> 1 by A9;
A16: j in NAT by ORDINAL1:def 12;
then reconsider Cj=C.j as Vertex of G by A10,GLIB_001:7;
A17: now
per cases by A7;
suppose
n = 1;
then x = C.first() by A5;
then x = C.last() by A1,GLIB_001:def 24;
hence x = C.(j+2);
end;
suppose
n = len C;
hence x = C.(j+2) by A5;
end;
end;
A18: now
assume x = Cj;
then
A19: j = 1 by A16,A10,A17,GLIB_001:def 28;
j+2 = len C;
hence contradiction by A3,A19;
end;
C.(j+1) Joins C.j,C.(j+2),G by A16,A10,GLIB_001:def 3;
then x,Cj are_adjacent by A17,Def3;
hence C.j in G.AdjacentSet({x}) by A18,Th51;
let e be object such that
A20: e in C.edges() and
A21: e Joins C.i,C.j,G;
consider k being even Element of NAT such that
A22: 1 <= k and
A23: k <= len C and
A24: C.k = e by A20,GLIB_001:99;
A25: (the_Source_of G).e = C.i & (the_Target_of G).e = C.j or (
the_Source_of G).e = C.j & (the_Target_of G).e = C.i by A21;
k in dom C by A22,A23,FINSEQ_3:25;
then consider ku1 being odd Element of NAT such that
A26: ku1 = k-1 and
A27: k-1 in dom C and
A28: k+1 in dom C and
A29: C.k Joins C.(ku1), C.(k+1),G by GLIB_001:9;
A30: ku1 <= len C by A26,A27,FINSEQ_3:25;
A31: k+1 <= len C by A28,FINSEQ_3:25;
per cases by A24,A29,A25;
suppose
A32: C.i = C.ku1 & C.j = C.(k+1);
then i+2 = k-1+(1+1) by A26,A30,A11,Th25
.= j by A10,A31,A15,A32,Th25;
hence contradiction by A9;
end;
suppose
A33: C.i = C.(k+1) & C.j = C.ku1;
then i = k+1 by A31,A11,Th25;
hence contradiction by A10,A26,A30,A15,A33,Th25;
end;
end;
suppose
A34: not (n = 1 or n = len C);
then 2*0+1 < n by A6,XXREAL_0:1;
then 1+2 <= n by Th4;
then 3+(-2) <= n+(-2) by XREAL_1:7;
then n-2*1 is odd Element of NAT by INT_1:3;
then reconsider i=n-2*1 as odd Nat;
A35: i+0 < i+2 by XREAL_1:8;
then reconsider Ci=C.i as Vertex of G by A4,GLIB_001:7,XXREAL_0:2;
reconsider j=n+2 as odd Nat;
take i, j;
n+0 < n+2 by XREAL_1:8;
hence i+2 < j;
A36: n < len C by A4,A34,XXREAL_0:1;
hence
A37: j <= len C by Th4;
then reconsider Cj=C.j as Vertex of G by GLIB_001:7;
A38: i in NAT by ORDINAL1:def 12;
A39: now
A40: n+0 > n+(-2) by XREAL_1:8;
assume Ci = x;
hence contradiction by A4,A5,A34,A38,A40,GLIB_001:def 28;
end;
A41: now
assume that
A42: i = 1 and
A43: j = len C;
j = i + 4;
hence contradiction by A3,A42,A43;
end;
hereby
A44: i+2+(-2) < j+0 by XREAL_1:8;
assume C.i = C.j;
hence contradiction by A38,A37,A41,A44,GLIB_001:def 28;
end;
A45: i < len C by A4,A35,XXREAL_0:2;
then C.(i+1) Joins C.i,C.(i+2),G by A38,GLIB_001:def 3;
then x,Ci are_adjacent by A5,Def3;
hence C.i in G.AdjacentSet({x}) by A39,Th51;
1+2 <= j by A6,XREAL_1:7;
then
A46: j <> 1;
A47: n+2 <= len C -2 + 2 by A36,Th4;
A48: now
A49: n+2 > n+0 by XREAL_1:8;
assume Cj = x;
hence contradiction by A5,A34,A47,A49,GLIB_001:def 28;
end;
C.(n+1) Joins C.n,C.j,G by A36,GLIB_001:def 3;
then x,Cj are_adjacent by A5;
hence C.j in G.AdjacentSet({x}) by A48,Th51;
let e be object such that
A50: e in C.edges() and
A51: e Joins C.i,C.j,G;
consider k being even Element of NAT such that
A52: 1 <= k and
A53: k <= len C and
A54: C.k = e by A50,GLIB_001:99;
A55: (the_Source_of G).e = C.i & (the_Target_of G).e = C.j or (
the_Source_of G).e = C.j & (the_Target_of G).e = C.i by A51;
1+1 <= k+1 by A52,XREAL_1:7;
then
A56: k+1 <> 1;
A57: k-1 < len C by A53,XREAL_1:146,XXREAL_0:2;
k in dom C by A52,A53,FINSEQ_3:25;
then consider ku1 being odd Element of NAT such that
A58: ku1 = k-1 and
k-1 in dom C and
A59: k+1 in dom C and
A60: C.k Joins C.(ku1), C.(k+1),G by GLIB_001:9;
A61: k+1 <= len C by A59,FINSEQ_3:25;
per cases by A54,A60,A55;
suppose
A62: C.i = C.ku1 & C.j = C.(k+1);
then i+2 = k-1+(1+1) by A45,A58,A57,Th25
.= j by A37,A61,A46,A56,A62,Th25;
hence contradiction;
end;
suppose
A63: C.i = C.(k+1) & C.j = C.ku1;
per cases by A37,A45,A58,A57,A61,A63,Th25;
suppose
i = k+1 & j = k-1;
hence contradiction;
end;
suppose
A64: i = k+1 & k-1 = 1 & j = len C;
j = i+4;
hence contradiction by A3,A64;
end;
suppose
A65: i = 1 & k+1 = len C & j = k-1;
then k+1 = 7;
hence contradiction by A3,A65;
end;
suppose
i = 1 & k+1 = len C & k-1 = 1 & j = len C;
hence contradiction;
end;
end;
end;
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 :: AdjacentV01:
for G being loopless _Graph, u being Vertex of G holds G.AdjacentSet({
u}) = {} iff u is isolated
proof
let G be loopless _Graph, u be Vertex of G;
hereby
assume
A1: G.AdjacentSet({u}) = {};
now
assume u.edgesInOut() <> {};
then consider e being object such that
A2: e in u.edgesInOut() by XBOOLE_0:def 1;
consider v being Vertex of G such that
A3: e Joins u,v,G by A2,GLIB_000:64;
A4: u <> v by A3,GLIB_000:def 18;
v,u are_adjacent by A3,Def3;
hence contradiction by A1,A4,Th51;
end;
hence u is isolated;
end;
assume u is isolated;
then
A5: u.edgesInOut() = {};
now
let v be object such that
A6: v in G.AdjacentSet({u});
reconsider v as Vertex of G by A6;
v,u are_adjacent by A6,Th51;
then ex e being object st e Joins v,u,G;
hence contradiction by A5,GLIB_000:14,62;
end;
hence thesis by XBOOLE_0:def 1;
end;
theorem Th56: :: Connected0
for G being _Graph, G0 being Subgraph of G, S being non empty
Subset of the_Vertices_of G, x being Vertex of G, G1 being (inducedSubgraph of
G,S), G2 being (inducedSubgraph of G,S\/{x}) st G1 is connected & x in G
.AdjacentSet(the_Vertices_of G1) holds G2 is connected
proof
let G be _Graph, G0 be Subgraph of G, S be non empty Subset of
the_Vertices_of G, x be Vertex of G, G1 be (inducedSubgraph of G,S), G2 be (
inducedSubgraph of G,S\/{x}) such that
A1: G1 is connected and
A2: x in G.AdjacentSet(the_Vertices_of G1);
A3: the_Vertices_of G1 = S by GLIB_000:def 37;
then consider xs being Vertex of G such that
A4: xs in S and
A5: x,xs are_adjacent by A2,Th49;
consider e being object such that
A6: e Joins x,xs,G by A5;
reconsider Sx = S\/{x} as Subset of the_Vertices_of G;
let u,v be Vertex of G2;
A7: the_Vertices_of G2 = Sx by GLIB_000:def 37;
then
A8: u in S or u in {x} by XBOOLE_0:def 3;
x in {x} by TARSKI:def 1;
then
A9: x in Sx by XBOOLE_0:def 3;
A10: xs in Sx by A4,XBOOLE_0:def 3;
e Joins xs,x,G by A6;
then
A11: e Joins xs,x,G2 by A9,A10,Th19;
then
A12: e Joins x,xs,G2;
A13: v in S or v in {x} by A7,XBOOLE_0:def 3;
A14: G1 is inducedSubgraph of G2,S by Th30,XBOOLE_1:7;
per cases by A8,A13,TARSKI:def 1;
suppose
A15: u in S & v in S;
the_Vertices_of G1 = S by GLIB_000:def 37;
then consider W being Walk of G1 such that
A16: W is_Walk_from u,v by A1,A15;
reconsider W as Walk of G2 by A14,GLIB_001:167;
take W;
thus thesis by A16;
end;
suppose
A17: u in S & v = x;
then consider W being Walk of G1 such that
A18: W is_Walk_from u,xs by A1,A3,A4;
reconsider W as Walk of G2 by A14,GLIB_001:167;
take W.append(G2.walkOf(xs,e,x));
A19: G2.walkOf(xs,e,x) is_Walk_from xs,x by A11,GLIB_001:15;
W is_Walk_from u, xs by A18;
hence thesis by A17,A19,GLIB_001:31;
end;
suppose
A20: u = x & v in S;
then consider W being Walk of G1 such that
A21: W is_Walk_from xs,v by A1,A3,A4;
reconsider W as Walk of G2 by A14,GLIB_001:167;
take G2.walkOf(x,e,xs).append(W);
A22: G2.walkOf(x,e,xs) is_Walk_from x,xs by A12,GLIB_001:15;
W is_Walk_from xs, v by A21;
hence thesis by A20,A22,GLIB_001:31;
end;
suppose
u = x & v = x;
then G2.walkOf(u) is_Walk_from u,v by GLIB_001:13;
hence thesis;
end;
end;
theorem Th57: :: Simplicial2a
for G being _Graph for S being non empty Subset of
the_Vertices_of G for H being inducedSubgraph of G,S for u being Vertex of G st
u in S & G.AdjacentSet({u}) c= S for v being Vertex of H st u=v holds G
.AdjacentSet({u}) = H.AdjacentSet({v})
proof
let G be _Graph;
let S be non empty Subset of the_Vertices_of G;
let G2 be inducedSubgraph of G,S;
let u be Vertex of G such that
A1: u in S and
A2: G.AdjacentSet({u}) c= S;
let v be Vertex of G2 such that
A3: u=v;
now
let x be object;
hereby
assume
A4: x in G.AdjacentSet({u});
then reconsider y=x as Vertex of G;
reconsider w=x as Vertex of G2 by A2,A4,GLIB_000:def 37;
y,u are_adjacent by A4,Th51;
then consider e being object such that
A5: e Joins y,u,G;
e Joins y,u,G2 by A1,A2,A4,A5,Th19;
then
A6: w,v are_adjacent by A3;
w <> v by A3,A4,Th51;
hence x in G2.AdjacentSet({v}) by A6,Th51;
end;
assume
A7: x in G2.AdjacentSet({v});
then reconsider y=x as Vertex of G2;
x in the_Vertices_of G2 by A7;
then reconsider w=x as Vertex of G;
y,v are_adjacent by A7,Th51;
then consider e being object such that
A8: e Joins y,v,G2;
e Joins y,v,G by A8,GLIB_000:72;
then
A9: w,u are_adjacent by A3;
w <> u by A3,A7,Th51;
hence x in G.AdjacentSet({u}) by A9,Th51;
end;
hence thesis by TARSKI:2;
end;
:: Adjacency set as a subgraph of G
definition
let G be _Graph, S be set;
mode AdjGraph of G,S -> Subgraph of G means
:Def5:
it is inducedSubgraph of
G,G.AdjacentSet(S) if S is Subset of the_Vertices_of G;
existence
proof
set T = the inducedSubgraph of G,G.AdjacentSet(S);
T is Subgraph of G;
hence thesis;
end;
consistency;
end;
theorem Th58: :: AdjGraph00
for G1, G2 be _Graph st G1 == G2 for u1 being Vertex of G1, u2
being Vertex of G2 st u1 = u2 for H1 being AdjGraph of G1,{u1}, H2 being
AdjGraph of G2,{u2} holds H1 == H2
proof
let G1,G2 be _Graph such that
A1: G1 == G2;
let u1 be Vertex of G1, u2 be Vertex of G2 such that
A2: u1 = u2;
set G2Adj = G2.AdjacentSet({u2});
set G1Adj = G1.AdjacentSet({u1});
A3: G1Adj = G2Adj by A1,A2,Th50;
let H1 be AdjGraph of G1,{u1};
let H2 be AdjGraph of G2,{u2};
A4: H1 is inducedSubgraph of G1,G1Adj by Def5;
A5: H2 is inducedSubgraph of G2,G2Adj by Def5;
per cases;
suppose
A6: not G1Adj is non empty Subset of the_Vertices_of G1;
then H1 == G1 by A4,GLIB_000:def 37;
then
A7: H1 == G2 by A1;
H2 == G2 by A5,A3,A6,GLIB_000:def 37;
hence thesis by A7;
end;
suppose
A8: G1Adj is non empty Subset of the_Vertices_of G1;
then the_Vertices_of H1 = G1Adj by A4,GLIB_000:def 37;
then
A9: the_Vertices_of H1 = the_Vertices_of H2 by A5,A3,GLIB_000:def 37;
G1 is Subgraph of G2 by A1,GLIB_000:87;
then
A10: G1.edgesBetween(G1Adj) c= G2.edgesBetween(G1Adj) by GLIB_000:76;
A11: the_Edges_of H1 = G1.edgesBetween(G1Adj) by A4,A8,GLIB_000:def 37;
G2 is Subgraph of G1 by A1,GLIB_000:87;
then
A12: G2.edgesBetween(G1Adj) c= G1.edgesBetween(G1Adj) by GLIB_000:76;
G2 is Subgraph of G1 by A1,GLIB_000:87;
then
A13: H2 is Subgraph of G1 by GLIB_000:43;
the_Edges_of H2 = G2.edgesBetween(G2Adj) by A5,A3,A8,GLIB_000:def 37;
then the_Edges_of H1 = the_Edges_of H2 by A3,A11,A10,A12;
hence thesis by A9,A13,GLIB_000:86;
end;
end;
theorem Th59: :: Simplicial2b
for G being _Graph for S being non empty Subset of
the_Vertices_of G for H being inducedSubgraph of G,S for u being Vertex of G st
u in S & G.AdjacentSet({u}) c= S & G.AdjacentSet({u}) <> {} for v being Vertex
of H st u=v for Ga being AdjGraph of G,{u}, Ha being AdjGraph of H,{v} holds Ga
== Ha
proof
let G be _Graph;
let S being non empty Subset of the_Vertices_of G;
let H be inducedSubgraph of G,S;
let u be Vertex of G such that
A1: u in S and
A2: G.AdjacentSet({u}) c= S and
A3: G.AdjacentSet({u}) <> {};
let v be Vertex of H;
assume u=v;
then
A4: G.AdjacentSet({u}) = H.AdjacentSet({v}) by A1,A2,Th57;
let Ga be AdjGraph of G,{u}, Ha being AdjGraph of H,{v};
A5: Ha is inducedSubgraph of H,H.AdjacentSet({v}) by Def5;
A6: Ga is inducedSubgraph of G,G.AdjacentSet({u}) by Def5;
then
A7: the_Edges_of Ga = G.edgesBetween(G.AdjacentSet({u})) by A3,GLIB_000:def 37;
the_Vertices_of Ga = G.AdjacentSet({u}) by A3,A6,GLIB_000:def 37;
hence the_Vertices_of Ga = the_Vertices_of Ha by A4,A5,GLIB_000:def 37;
the_Edges_of Ha = H.edgesBetween(H.AdjacentSet({v})) by A3,A4,A5,
GLIB_000:def 37;
hence
A8: the_Edges_of Ga = the_Edges_of Ha by A2,A3,A4,A7,Th31;
A9: the_Target_of Ga = (the_Target_of G)|the_Edges_of Ga by GLIB_000:45;
Ha is inducedSubgraph of H,G.AdjacentSet({u}) by A4,Def5;
then
A10: Ha is inducedSubgraph of G,G.AdjacentSet({u}) by A2,A3,Th29;
the_Source_of Ga = (the_Source_of G)|the_Edges_of Ga by GLIB_000:45;
hence the_Source_of Ha = the_Source_of Ga & the_Target_of Ha = the_Target_of
Ga by A8,A9,A10,GLIB_000:45;
end;
definition
let G be _Graph;
attr G is complete means
:Def6:
for u,v being Vertex of G st u <> v holds u, v are_adjacent;
end;
theorem Th60: :: Completetr
for G being _Graph st G is _trivial holds G is complete
proof
let G be _Graph;
assume G is _trivial;
then consider x being Vertex of G such that
A1: the_Vertices_of G = {x} by GLIB_000:22;
let u,v being Vertex of G such that
A2: u <> v and
not u,v are_adjacent;
u = x by A1,TARSKI:def 1;
hence contradiction by A1,A2,TARSKI:def 1;
end;
registration
cluster _trivial -> complete for _Graph;
coherence by Th60;
end;
registration
cluster _trivial simple complete for _Graph;
existence
proof
set G = the _trivial simple _Graph;
take G;
thus thesis;
end;
cluster non _trivial _finite simple complete for _Graph;
existence
proof
set V = {0,1}, E = {0}, S = 0 .--> 0, T = 0 .--> 1;
A1: dom T = E;
A2: now
let x be object;
assume x in E;
then x = 0 by TARSKI:def 1;
then T.x = 1 by FUNCOP_1:72;
hence T.x in V by TARSKI:def 2;
end;
A3: now
let x be object;
assume x in E;
then x = 0 by TARSKI:def 1;
then S.x = 0 by FUNCOP_1:72;
hence S.x in V by TARSKI:def 2;
end;
reconsider T as Function of E,V by A1,A2,FUNCT_2:3;
dom S = E;
then reconsider S as Function of E,V by A3,FUNCT_2:3;
set G = createGraph(V,E,S,T);
take G;
A4: (the_Source_of G).0 = 0 by FUNCOP_1:72;
now
let e1,e2,v1,v2 be object such that
A6: e1 Joins v1,v2,G and
A7: e2 Joins v1,v2,G;
e1 in {0} by A6;
then
A8: e1 = 0 by TARSKI:def 1;
assume
A9: e1 <> e2;
e2 in {0} by A7;
hence contradiction by A9,A8,TARSKI:def 1;
end;
then
A10: G is non-multi;
now
assume card (the_Vertices_of G) = 1;
then ex x being object st the_Vertices_of G = {x} by CARD_2:42;
hence contradiction by ZFMISC_1:5;
end;
hence G is non _trivial & G is _finite;
A12: (the_Target_of G).0 = 1 by FUNCOP_1:72;
0 in the_Edges_of G by TARSKI:def 1;
then
A13: 0 Joins 0,1,G by A4,A12;
now
let v be object;
let e being object such that
A14: e Joins v,v,G;
reconsider v as Vertex of G by A14,GLIB_000:13;
e in the_Edges_of G by A14;
then e Joins 0,1,G by A13,TARSKI:def 1;
then 0 = v & 1 = v or 0 = v & 1 = v by A14;
hence contradiction;
end;
then G is loopless by GLIB_000:18;
hence G is simple by A10;
now
let u,v be Vertex of G such that
A15: u <> v;
per cases by TARSKI:def 2;
suppose
A16: u = 0;
A17: 0 in the_Edges_of G by TARSKI:def 1;
v = 1 by A15,A16,TARSKI:def 2;
then 0 Joins u,v,G by A4,A12,A16,A17;
hence u,v are_adjacent;
end;
suppose
A18: u = 1;
A19: 0 in the_Edges_of G by TARSKI:def 1;
v = 0 by A15,A18,TARSKI:def 2;
then 0 Joins v,u,G by A4,A12,A18,A19;
hence u,v are_adjacent by Def3;
end;
end;
hence thesis;
end;
end;
theorem Th61: :: Complete00
for G1,G2 being _Graph st G1 == G2 holds G1 is complete implies
G2 is complete
proof
let G1,G2 be _Graph such that
A1: G1 == G2;
assume
A2: G1 is complete;
now
let u,v be Vertex of G2 such that
A3: u <> v;
reconsider v2=v as Vertex of G1 by A1;
reconsider u2=u as Vertex of G1 by A1;
u2,v2 are_adjacent by A2,A3;
hence u,v are_adjacent by A1,Th43;
end;
hence thesis;
end;
theorem Th62: :: Complete01
for G being complete _Graph, S being Subset of the_Vertices_of G
for H being inducedSubgraph of G,S holds H is complete
proof
let G be complete _Graph;
let S be Subset of the_Vertices_of G;
let H be inducedSubgraph of G,S;
per cases;
suppose
S = {};
then H == G by GLIB_000:def 37;
hence thesis by Th61;
end;
suppose
S <> {};
then
A1: the_Vertices_of H = S by GLIB_000:def 37;
now
let u,v be Vertex of H such that
A2: u <> v;
reconsider v2=v as Vertex of G by A1,TARSKI:def 3;
reconsider u2=u as Vertex of G by A1,TARSKI:def 3;
u2,v2 are_adjacent by A2,Def6;
then consider e being object such that
A3: e Joins u2,v2,G;
e Joins u,v,H by A1,A3,Th19;
hence u,v are_adjacent;
end;
hence thesis;
end;
end;
begin :: Simplicial vertex :: Golumbic p. 81
definition
let G be _Graph, v be Vertex of G;
attr v is simplicial means
G.AdjacentSet({v}) <> {} implies for G2
being AdjGraph of G,{v} holds G2 is complete;
end;
theorem Th63: :: Simplicial0
for G being complete _Graph, v being Vertex of G holds v is simplicial
proof
let G be complete _Graph, v be Vertex of G;
now
let G2 be AdjGraph of G,{v};
G2 is inducedSubgraph of G,G.AdjacentSet({v}) by Def5;
hence G2 is complete by Th62;
end;
hence thesis;
end;
theorem :: Simplicial01
for G being _trivial _Graph, v being Vertex of G holds v is simplicial;
theorem Th65: :: Simplicial1
for G1,G2 being _Graph st G1 == G2 for u1 being Vertex of G1, u2
being Vertex of G2 st u1=u2 & u1 is simplicial holds u2 is simplicial
proof
let G1,G2 be _Graph such that
A1: G1 == G2;
let u1 be Vertex of G1, u2 be Vertex of G2 such that
A2: u1 = u2;
assume
A3: u1 is simplicial;
now
per cases;
suppose
G1.AdjacentSet({u1}) = {};
then G2.AdjacentSet({u2}) = {} by A1,A2,Th50;
hence thesis;
end;
suppose
A4: G1.AdjacentSet({u1}) <> {};
set H1 = the AdjGraph of G1,{u1};
H1 is complete by A3,A4;
then for H2 being AdjGraph of G2,{u2} holds H2 is complete by A1,A2,Th58
,Th61;
hence thesis;
end;
end;
hence thesis;
end;
theorem Th66: :: Simplicial2
for G being _Graph for S being non empty Subset of
the_Vertices_of G for H being inducedSubgraph of G,S for u being Vertex of G st
u in S & G.AdjacentSet({u}) c= S for v being Vertex of H st u=v holds u is
simplicial iff v is simplicial
proof
let G be _Graph;
let S be non empty Subset of the_Vertices_of G;
let G2 be inducedSubgraph of G,S;
let u be Vertex of G such that
A1: u in S and
A2: G.AdjacentSet({u}) c= S;
let v be Vertex of G2 such that
A3: u=v;
A4: G.AdjacentSet({u}) = {} iff G2.AdjacentSet({v}) = {} by A1,A2,A3,Th57;
per cases;
suppose
G.AdjacentSet({u}) = {};
hence thesis by A4;
end;
suppose
A5: G.AdjacentSet({u}) <> {};
hereby
set Ga = the AdjGraph of G,{u};
assume u is simplicial;
then
A6: Ga is complete by A5;
thus v is simplicial
by A1,A2,A3,A5,A6,Th59,Th61;
end;
set Ha = the AdjGraph of G2,{v};
assume
A7: v is simplicial;
G2.AdjacentSet({v}) <> {} by A1,A2,A3,A5,Th57;
then
A8: Ha is complete by A7;
thus u is simplicial
proof
assume G.AdjacentSet({u}) <> {};
let Ga be AdjGraph of G,{u};
Ga == Ha by A1,A2,A3,A5,Th59;
hence thesis by A8,Th61;
end;
end;
end;
theorem Th67: :: Simplicial03
for G being _Graph, v being Vertex of G st v is simplicial
for a,b being object
st a<>b & a in G.AdjacentSet({v}) & b in G.AdjacentSet({v}) holds
ex e being object st e Joins a,b,G
proof
let G be _Graph, x be Vertex of G such that
A1: x is simplicial;
set H = the AdjGraph of G,{x};
let a,b be object such that
A2: a<>b and
A3: a in G.AdjacentSet({x}) and
A4: b in G.AdjacentSet({x});
A5: H is inducedSubgraph of G,G.AdjacentSet({x}) by Def5;
then reconsider u=a as Vertex of H by A3,GLIB_000:def 37;
reconsider v=b as Vertex of H by A4,A5,GLIB_000:def 37;
H is complete by A1,A3;
then u,v are_adjacent by A2;
then consider e being object such that
A6: e Joins u,v,H;
e Joins a,b,G by A6,GLIB_000:72;
hence thesis;
end;
theorem Th68: :: Simplicial03a
for G being _Graph, v being Vertex of G st not v is simplicial
ex a,b being Vertex of G st a<>b & v<>a & v<>b & v,a are_adjacent & v,b
are_adjacent & not a,b are_adjacent
proof
let G be _Graph, v be Vertex of G such that
A1: not v is simplicial;
assume
A2: not 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;
per cases;
suppose
G.AdjacentSet({v}) = {};
hence contradiction by A1;
end;
suppose
A3: G.AdjacentSet({v}) <> {};
now
let H be AdjGraph of G,{v};
A4: H is inducedSubgraph of G,G.AdjacentSet({v}) by Def5;
now
let a,b be Vertex of H such that
A5: a<>b;
A6: the_Vertices_of H = G.AdjacentSet({v}) by A3,A4,GLIB_000:def 37;
then
A7: b in G.AdjacentSet({v});
a in G.AdjacentSet({v}) by A6;
then reconsider vv=v,aa=a,bb=b as Vertex of G by A7;
A8: aa,vv are_adjacent by A6,Th51;
A9: bb,vv are_adjacent by A6,Th51;
aa<>vv by A6,Th51;
then aa,bb are_adjacent by A2,A5,A8,A9;
hence a,b are_adjacent by A3,A4,Th44;
end;
hence H is complete;
end;
hence contradiction by A1;
end;
end;
begin :: Vertex separator :: Golumbic, p. 84
definition
let G be _Graph, 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:
not
a in it & not b in it & for G2 being removeVertices of G,it holds not (ex W
being Walk of G2 st W is_Walk_from a,b);
existence
proof
set S = the_Vertices_of G\{a,b};
a in {a,b} by TARSKI:def 2;
then
A3: not a in S by XBOOLE_0:def 5;
A4: not ex e being set st e Joins a,b,G by A2;
A5: for G2 being removeVertices of G,S holds not ex W being Walk of G2 st
W is_Walk_from a,b
proof
let G2 be removeVertices of G,S;
let W be Walk of G2 such that
A6: W is_Walk_from a,b;
A7: now
let x be set such that
A8: x in {a,b};
now
per cases by A8,TARSKI:def 2;
suppose
x = a;
then x = W.first() by A6;
hence x in W.vertices() by GLIB_001:88;
end;
suppose
x = b;
then x = W.last() by A6;
hence x in W.vertices() by GLIB_001:88;
end;
end;
hence x in W.vertices();
end;
reconsider W2=W as Walk of G by GLIB_001:167;
A9: now
let x be object;
hereby
assume x in W2.vertices();
then ex n being odd Element of NAT st n<=len W & W.n=x by GLIB_001:87
;
hence x in W.vertices() by GLIB_001:87;
end;
assume x in W.vertices();
then ex n being odd Element of NAT st n<=len W2 & W2.n=x by GLIB_001:87
;
hence x in W2.vertices() by GLIB_001:87;
end;
the_Vertices_of G\S is non empty by A3,XBOOLE_0:def 5;
then the_Vertices_of G2 = the_Vertices_of G\S by GLIB_000:def 37;
then the_Vertices_of G2 = the_Vertices_of G /\ {a,b} by XBOOLE_1:48;
then the_Vertices_of G2 = {a,b} by XBOOLE_1:28;
then for x being object holds x in W.vertices() iff x in {a,b} by A7;
then W.vertices() = {a,b} by TARSKI:2;
then W2.vertices() = {a,b} by A9,TARSKI:2;
hence contradiction by A1,A4,Th22;
end;
b in {a,b} by TARSKI:def 2;
then not b in S by XBOOLE_0:def 5;
hence thesis by A3,A5;
end;
end;
theorem Th69: :: VS01
for G being _Graph, a,b being Vertex of G st a<>b & not a,b
are_adjacent for S being VertexSeparator of a,b holds S is VertexSeparator of b
,a
proof
let G be _Graph;
let a,b be Vertex of G such that
A1: a<>b and
A2: not a,b are_adjacent;
let S be VertexSeparator of a,b;
A3: not b in S by A1,A2,Def8;
A4: for G2 being removeVertices of G,S holds not ex W being Walk of G2 st W
is_Walk_from b,a
proof
let G2 be removeVertices of G,S;
let W be Walk of G2;
assume W is_Walk_from b,a;
then W.reverse() is_Walk_from a,b by GLIB_001:23;
hence contradiction by A1,A2,Def8;
end;
not a in S by A1,A2,Def8;
hence thesis by A1,A2,A3,A4,Def8;
end;
:: alternate characterization of Vertex Separator
theorem Th70: :: VS02
for G being _Graph, a,b being Vertex of G st a<>b & not a,b
are_adjacent for S being Subset of the_Vertices_of G holds S is VertexSeparator
of a,b iff (not a in S & not b in S & for W being Walk of G st W is_Walk_from a
,b holds ex x being Vertex of G st x in S & x in W.vertices())
proof
let G be _Graph;
let a,b be Vertex of G such that
A1: a<>b and
A2: not a,b are_adjacent;
let S be Subset of the_Vertices_of G;
hereby
assume
A3: S is VertexSeparator of a,b;
hence not a in S & not b in S by A1,A2,Def8;
then
A4: the_Vertices_of G \ S is non empty by XBOOLE_0:def 5;
let W be Walk of G such that
A5: W is_Walk_from a,b;
now
assume
A6: not ex x being Vertex of G st x in S & x in W.vertices();
let G2 be removeVertices of G,S;
A7: the_Vertices_of G2 = the_Vertices_of G\S by A4,GLIB_000:def 37;
then
A8: the_Edges_of G2 = G.edgesBetween(the_Vertices_of G2) by GLIB_000:def 37;
A9: W.edges() c= G.edgesBetween(W.vertices()) by GLIB_001:109;
now
let x be object such that
A10: x in W.vertices();
not x in S by A6,A10;
hence x in the_Vertices_of G2 by A7,A10,XBOOLE_0:def 5;
end;
then
A11: W.vertices() c= the_Vertices_of G2;
then G.edgesBetween(W.vertices()) c= G.edgesBetween(the_Vertices_of G2)
by GLIB_000:36;
then W.edges() c= the_Edges_of G2 by A8,A9;
then reconsider W2=W as Walk of G2 by A11,GLIB_001:170;
W.last() = b by A5;
then
A12: W2.last()=b;
W.first() = a by A5;
then W2.first()=a;
then W2 is_Walk_from a,b by A12;
hence contradiction by A1,A2,A3,Def8;
end;
hence ex x being Vertex of G st x in S & x in W.vertices();
end;
assume that
A13: not a in S and
A14: not b in S and
A15: 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();
now
let G2 be removeVertices of G,S;
given W be Walk of G2 such that
A16: W is_Walk_from a,b;
reconsider W2=W as Walk of G by GLIB_001:167;
W.last() = b by A16;
then
A17: W2.last()=b;
now
let x be object;
hereby
assume x in W2.vertices();
then ex n being odd Element of NAT st n<=len W & W.n=x by GLIB_001:87;
hence x in W.vertices() by GLIB_001:87;
end;
assume x in W.vertices();
then ex n being odd Element of NAT st n<=len W2 & W2.n=x by GLIB_001:87;
hence x in W2.vertices() by GLIB_001:87;
end;
then
A18: W2.vertices() = W.vertices() by TARSKI:2;
the_Vertices_of G \ S is non empty by A13,XBOOLE_0:def 5;
then the_Vertices_of G2 = the_Vertices_of G \ S by GLIB_000:def 37;
then
A19: for x being Vertex of G holds not (x in S & x in W2.vertices() ) by A18,
XBOOLE_0:def 5;
W.first() = a by A16;
then W2.first()=a;
then W2 is_Walk_from a,b by A17;
hence contradiction by A15,A19;
end;
hence thesis by A1,A2,A13,A14,Def8;
end;
theorem Th71: :: VS07
for G being _Graph, a,b being Vertex of G st a<>b & not a,b
are_adjacent for S being VertexSeparator of a,b for W being Walk of G st W
is_Walk_from a,b ex k being odd Nat st 1 < k & k < len W & W.k in S
proof
let G be _Graph;
let a,b be Vertex of G such that
A1: a<>b and
A2: not a,b are_adjacent;
let S be VertexSeparator of a,b;
let W be Walk of G such that
A3: W is_Walk_from a,b;
consider x being Vertex of G such that
A4: x in S and
A5: x in W.vertices() by A1,A2,A3,Th70;
consider n being odd Element of NAT such that
A6: n <= len W and
A7: W.n = x by A5,GLIB_001:87;
not a in S by A1,A2,Th70;
then
A8: 1 <> n by A3,A4,A7;
not b in S by A1,A2,Th70;
then n <> len W by A3,A4,A7;
then
A9: n < len W by A6,XXREAL_0:1;
1 <= n by ABIAN:12;
then 1 < n by A8,XXREAL_0:1;
hence thesis by A4,A7,A9;
end;
theorem Th72: :: VS08a
for G being _Graph, a,b being Vertex of G st a<>b & not a,b
are_adjacent for S being VertexSeparator of a,b st S = {} holds not ex W being
Walk of G st W is_Walk_from a,b
proof
let G be _Graph;
let a,b be Vertex of G such that
A1: a<>b and
A2: not a,b are_adjacent;
let S be VertexSeparator of a,b;
assume
A3: S = {};
A4: the_Edges_of G c= G.edgesBetween(the_Vertices_of G) by GLIB_000:34;
A5: the_Vertices_of G c= the_Vertices_of G;
set G2 = the removeVertices of G,S;
given W be Walk of G such that
A6: W is_Walk_from a,b;
the_Vertices_of G2 = the_Vertices_of G by A3,GLIB_000:def 37;
then
A7: W.vertices() c= the_Vertices_of G2;
G2 is inducedSubgraph of G,the_Vertices_of G,the_Edges_of G by A3,GLIB_000:34
;
then the_Edges_of G2 = the_Edges_of G by A5,A4,GLIB_000:def 37;
then W.edges() c= the_Edges_of G2;
then reconsider W2=W as Walk of G2 by A7,GLIB_001:170;
W.last() = b by A6;
then
A8: W2.last()=b;
W.first() = a by A6;
then W2.first()=a;
then W2 is_Walk_from a,b by A8;
hence contradiction by A1,A2,Def8;
end;
theorem
for G being _Graph, a,b being Vertex of G st a<>b ¬ a,b
are_adjacent & not ex W being Walk of G st W is_Walk_from a,b holds {} is
VertexSeparator of a,b
proof
let G be _Graph;
let a,b be Vertex of G such that
A1: a<>b and
A2: not a,b are_adjacent;
assume
A3: not ex W being Walk of G st W is_Walk_from a,b;
A4: now
let G2 be removeVertices of G,{};
given W be Walk of G2 such that
A5: W is_Walk_from a,b or W is_Walk_from b,a;
per cases by A5;
suppose
A6: W is_Walk_from a,b;
reconsider W2=W as Walk of G by GLIB_001:167;
W.last() = b by A6;
then
A7: W2.last()=b;
W.first() = a by A6;
then W2.first()=a;
then W2 is_Walk_from a,b by A7;
hence contradiction by A3;
end;
suppose
A8: W is_Walk_from b,a;
set P=W.reverse();
reconsider W2=P as Walk of G by GLIB_001:167;
A9: P is_Walk_from a,b by A8,GLIB_001:23;
then P.last() = b;
then
A10: W2.last()=b;
P.first() = a by A9;
then W2.first()=a;
then W2 is_Walk_from a,b by A10;
hence contradiction by A3;
end;
end;
{} is Subset of the_Vertices_of G by XBOOLE_1:2;
hence thesis by A1,A2,A4,Def8;
end;
theorem Th74: :: VS11
for G being _Graph, a,b being Vertex of G st a<>b & not a,b
are_adjacent for S being VertexSeparator of a,b, G2 being removeVertices of G,S
for a2 being Vertex of G2 holds G2.reachableFrom(a2) /\ S = {}
proof
let G be _Graph;
let a,b be Vertex of G such that
A1: a<>b and
A2: not a,b are_adjacent;
let S be VertexSeparator of a,b, G2 be removeVertices of G,S;
let a2 be Vertex of G2;
set A = G2.reachableFrom(a2);
not a in S by A1,A2,Def8;
then a in the_Vertices_of G \ S by XBOOLE_0:def 5;
then
A3: the_Vertices_of G2 = the_Vertices_of G \ S by GLIB_000:def 37;
now
let x be object such that
A4: x in A /\ S;
A5: x in S by A4,XBOOLE_0:def 4;
x in A by A4,XBOOLE_0:def 4;
hence contradiction by A3,A5,XBOOLE_0:def 5;
end;
hence thesis by XBOOLE_0:def 1;
end;
theorem Th75:
for G being _Graph, a,b being Vertex of G st a<>b & not a,b
are_adjacent for S being VertexSeparator of a,b, G2 being removeVertices of G,S
for a2,b2 being Vertex of G2 st a2=a & b2=b holds G2.reachableFrom(a2) /\ G2
.reachableFrom(b2) = {}
proof
let G be _Graph;
let a,b be Vertex of G such that
A1: a<>b and
A2: not a,b are_adjacent;
let S be VertexSeparator of a,b, G2 be removeVertices of G,S;
let a2,b2 be Vertex of G2 such that
A3: a2=a and
A4: b2=b;
set A = G2.reachableFrom(a2), B = G2.reachableFrom(b2);
now
let x be object such that
A5: x in A /\ B;
x in A by A5,XBOOLE_0:def 4;
then consider W1 being Walk of G2 such that
A6: W1 is_Walk_from a2,x by GLIB_002:def 5;
x in B by A5,XBOOLE_0:def 4;
then consider rW2 being Walk of G2 such that
A7: rW2 is_Walk_from b2,x by GLIB_002:def 5;
set W2 = rW2.reverse();
set W = W1.append(W2);
W2 is_Walk_from x,b2 by A7,GLIB_001:23;
then W is_Walk_from a2,b2 by A6,GLIB_001:31;
hence contradiction by A1,A2,A3,A4,Def8;
end;
hence thesis by XBOOLE_0:def 1;
end;
theorem Th76: :: VS10
for G being _Graph, a,b being Vertex of G st a<>b & not a,b
are_adjacent for S being VertexSeparator of a,b for G2 being removeVertices of
G,S holds a is Vertex of G2 & b is Vertex of G2
proof
let G be _Graph;
let a,b be Vertex of G such that
A1: a<>b and
A2: not a,b are_adjacent;
let S be VertexSeparator of a,b, G2 be removeVertices of G,S;
not b in S by A1,A2,Def8;
then
A3: b in the_Vertices_of G\S by XBOOLE_0:def 5;
not a in S by A1,A2,Def8;
then a in the_Vertices_of G\S by XBOOLE_0:def 5;
hence thesis by A3,GLIB_000:def 37;
end;
definition
let G be _Graph, a,b be Vertex of G;
let S be VertexSeparator of a,b;
attr S is minimal means
for T being Subset of S st T <> S holds not T is VertexSeparator of a,b;
end;
theorem :: VS000
for G being _Graph, a,b being Vertex of G for S being VertexSeparator
of a,b st S = {} holds S is minimal;
theorem Th78: :: minVSexistance
for G being _finite _Graph for a,b being Vertex of G ex S being
VertexSeparator of a,b st S is minimal
proof
let G be _finite _Graph, a,b be Vertex of G;
set X = the set of all S where S is VertexSeparator of a,b ;
set s = the VertexSeparator of a,b;
A1: s in X;
now
let x be object;
assume x in X;
then ex y being VertexSeparator of a,b st x = y;
hence x in bool the_Vertices_of G;
end;
then X c= bool the_Vertices_of G;
then reconsider X as non empty finite set by A1;
defpred P[object,object] means
ex p being VertexSeparator of a,b st $1 = p & $2 = card p;
A2: now
let x be object;
assume x in X;
then consider Y being VertexSeparator of a,b such that
A3: Y = x;
card Y in REAL by NUMBERS:19;
hence ex y being object st y in REAL & P[x,y] by A3;
end;
consider F being Function of X, REAL such that
A4: for x being object st x in X holds P[x,F.x] from FUNCT_2:sch 1(A2);
deffunc FF(Element of X) = F/.$1;
consider Min being Element of X such that
A5: for N being Element of X holds FF(Min) <= FF(N) from PRE_CIRC:sch 5;
consider M being VertexSeparator of a,b such that
M = Min and
A6: card M = F.Min by A4;
A7: dom F = X by FUNCT_2:def 1;
now
assume not M is minimal;
then consider T being Subset of M such that
A8: T<>M and
A9: T is VertexSeparator of a,b;
T in X by A9;
then reconsider T2=T as Element of X;
consider Tp being VertexSeparator of a,b such that
A10: Tp=T2 and
A11: card Tp = F.T2 by A4;
Tp in dom F by A7;
then F/.Tp = F.Tp by PARTFUN1:def 6;
then
A12: card M <= card T by A5,A6,A10,A11;
card T <= card M by NAT_1:43;
hence contradiction by A8,A12,CARD_2:102,XXREAL_0:1;
end;
hence thesis;
end;
theorem Th79: :: VS13
:: Property "symmetry" for 2 argument modes could be used if we had it
:: as VertexSeparator of a,b is a VertexSeparator of b,a
:: then this theorem would not be needed
for G being _Graph, a,b being Vertex of G st a<>b & not a,b
are_adjacent for S being VertexSeparator of a,b st S is minimal for T being
VertexSeparator of b,a st S=T holds T is minimal
by Th69;
theorem :: VS06
for G being _Graph, a,b being Vertex of G st a<>b & not a,b
are_adjacent for S being VertexSeparator of a,b st S is minimal for x being
Vertex of G st x in S ex W being Walk of G st W is_Walk_from a,b & x in W
.vertices()
proof
let G be _Graph;
let a,b be Vertex of G such that
A1: a<>b and
A2: not a,b are_adjacent;
let S be VertexSeparator of a,b such that
A3: S is minimal;
let x be Vertex of G such that
A4: x in S;
set T = S\{x};
A5: T c= S by XBOOLE_1:36;
then
A6: not b in T by A1,A2,Def8;
assume
A7: not ex W being Walk of G st W is_Walk_from a,b & x in W.vertices();
A8: now
let W be Walk of G such that
A9: W is_Walk_from a,b;
consider y being Vertex of G such that
A10: y in S and
A11: y in W.vertices() by A1,A2,A9,Th70;
take y;
y <> x by A7,A9,A11;
then not y in {x} by TARSKI:def 1;
hence y in T by A10,XBOOLE_0:def 5;
thus y in W.vertices() by A11;
end;
x in {x} by TARSKI:def 1;
then
A12: T <> S by A4,XBOOLE_0:def 5;
not a in T by A1,A2,A5,Def8;
then T is VertexSeparator of a,b by A1,A2,A6,A8,Th70;
hence contradiction by A3,A12,A5;
end;
theorem Th81: :: VertexSep0
for G being _Graph for a,b being Vertex of G st a<>b & not a,b
are_adjacent for S being VertexSeparator of a,b st S is minimal for H being
removeVertices of G,S for aa being Vertex of H st aa=a for x being Vertex of G
st x in S ex y being Vertex of G st y in H.reachableFrom(aa) & x,y are_adjacent
proof
let G be _Graph;
let a,b be Vertex of G such that
A1: a<>b and
A2: not a,b are_adjacent;
let S be VertexSeparator of a,b such that
A3: S is minimal;
let H be removeVertices of G,S;
let aa be Vertex of H such that
A4: aa=a;
set A=H.reachableFrom(aa);
let x be Vertex of G such that
A5: x in S;
set T = S\{x};
A6: T c= S by XBOOLE_1:36;
then
A7: not b in T by A1,A2,Def8;
assume
A8: not ex y being Vertex of G st y in H.reachableFrom(aa) & x,y are_adjacent;
A9: for W being Walk of G st W is_Walk_from a,b & x in W.vertices() ex y
being Vertex of G st y in T & y in W.vertices()
proof
let W be Walk of G such that
A10: W is_Walk_from a,b and
A11: x in W.vertices();
A12: now
assume W.find(x) = 1;
then W.(W.find(x)) = W.first();
then W.(W.find(x)) = a by A10;
then not W.(W.find(x)) in S by A1,A2,Def8;
hence contradiction by A5,A11,GLIB_001:def 19;
end;
consider k being odd Element of NAT such that
A13: k <= len W and
A14: W.k = x by A11,GLIB_001:87;
W.find(W.k) <= k by A13,GLIB_001:115;
then
A15: W.find(x) <= len W by A13,A14,XXREAL_0:2;
then
A16: W.find(x)+(-2) <= len W+0 by XREAL_1:7;
0+1 <= W.find(x) by ABIAN:12;
then 2*0+1 < W.find(x) by A12,XXREAL_0:1;
then 2*1+1 <= W.find(x) by Th4;
then
A17: 3+(-2) <= W.find(x)+(-2) by XREAL_1:7;
then
A18: W.find(x)-2 is Element of NAT by INT_1:3;
then reconsider j=W.find(x)-2*1 as odd Nat;
set P = W.cut(1,j);
A19: 2*0+1 <= j by A17;
then
A20: len P + 1 + (-1) = j + 1 + (-1) by A18,A16,GLIB_001:36;
assume
A21: not ex y being Vertex of G st y in T & y in W.vertices();
A22: for n being odd Nat st n <= j holds not P.n in S & P.n=W.n
proof
let n be odd Nat such that
A23: n <= j;
1 <= n by ABIAN:12;
then 1+(-1) <= n+(-1) by XREAL_1:7;
then
A24: n-1 is Element of NAT by INT_1:3;
then reconsider nu1 = n-1 as Nat;
n < j + 1 by A23,NAT_1:13;
then n+(-1) < j+1+(-1) by XREAL_1:8;
then
A25: P.(nu1+1) = W.(1+nu1) by A16,A19,A20,A24,GLIB_001:36;
now
A26: P.vertices() c= W.vertices() by A18,A16,A19,GLIB_001:94;
A27: n in NAT by ORDINAL1:def 12;
then P.n in P.vertices() by A20,A23,GLIB_001:87;
then
A28: not P.n in T by A21,A26;
n < j + 1 by A23,NAT_1:13;
then
A29: n+0 < j + 1 + 1 by XREAL_1:8;
A30: S \/ {x} = {x} \/ T by XBOOLE_1:39;
{x} c= S by A5,ZFMISC_1:31;
then
A31: S = {x} \/ T by A30,XBOOLE_1:12;
A32: n <= len W by A16,A23,XXREAL_0:2;
assume P.n in S;
then P.n in {x} by A28,A31,XBOOLE_0:def 3;
then n < W.find(W.n) by A25,A29,TARSKI:def 1;
hence contradiction by A27,A32,GLIB_001:115;
end;
hence thesis by A25;
end;
then for n being odd Nat st n <= j holds not P.n in S;
then reconsider HP=P as Walk of H by A20,Th21;
W.first() = a by A10;
then P.(2*0+1) = a by A17,A22;
then aa in HP.vertices() by A4,A17,A20,GLIB_001:87;
then
A33: HP.vertices() c= A by GLIB_002:13;
W.find(x) < len W + 1 by A15,NAT_1:13;
then
A34: W.find(x)+(-2) < len W + 1 + (-2) by XREAL_1:8;
P.j is Vertex of G by A20,GLIB_001:7;
then reconsider Wj=W.j as Vertex of G by A22;
len W +(-1) < len W+0 by XREAL_1:8;
then j < len W by A34,XXREAL_0:2;
then W.(j+1) Joins Wj,W.(j+2),G by A18,GLIB_001:def 3;
then W.(j+1) Joins Wj,x,G by A11,GLIB_001:def 19;
then
A35: Wj,x are_adjacent;
P.j in HP.vertices() by A20,GLIB_001:87;
then W.j in HP.vertices() by A22;
hence contradiction by A8,A33,A35;
end;
A36: now
let W be Walk of G such that
A37: W is_Walk_from a,b;
consider y being Vertex of G such that
A38: y in S and
A39: y in W.vertices() by A1,A2,A37,Th70;
per cases;
suppose
y = x;
hence ex y being Vertex of G st y in T & y in W.vertices() by A9,A37,A39;
end;
suppose
A40: y <> x;
take y;
not y in {x} by A40,TARSKI:def 1;
hence y in T by A38,XBOOLE_0:def 5;
thus y in W.vertices() by A39;
end;
end;
x in {x} by TARSKI:def 1;
then
A41: T <> S by A5,XBOOLE_0:def 5;
not a in T by A1,A2,A6,Def8;
then T is VertexSeparator of a,b by A1,A2,A7,A36,Th70;
hence contradiction by A3,A41,A6;
end;
theorem Th82: :: VertexSep01
:: Property "symmetry" for 2 argument modes could be used if we had it
:: as VertexSeparator of a,b is a VertexSeparator of b,a
for G being _Graph for a,b being Vertex of G st a<>b & not a,b
are_adjacent for S being VertexSeparator of a,b st S is minimal for H being
removeVertices of G,S for aa being Vertex of H st aa=b for x being Vertex of G
st x in S ex y being Vertex of G st y in H.reachableFrom(aa) & x,y are_adjacent
proof
let G be _Graph, a,b be Vertex of G such that
A1: a<>b and
A2: not a,b are_adjacent;
let S be VertexSeparator of a,b such that
A3: S is minimal;
reconsider S1 = S as VertexSeparator of b,a by A1,A2,Th69;
A4: S1 is minimal by A1,A2,A3,Th79;
let H be (removeVertices of G,S), aa be Vertex of H such that
A5: aa=b;
let x be Vertex of G;
assume x in S;
hence thesis by A1,A2,A5,A4,Th81;
end;
begin :: Chordal graphs :: Golumbic, p. 81
:: The notion of a chord. Is it worthwhile having it?
:: definition let G be _Graph, W be Walk of G, e be set;
:: pred e is_chord_of W means
:: ex m, n being odd Nat st m < n & n <= len W & W.m <> W.n &
:: e Joins W.m,W.n,G &
:: for f being set st f in W.edges() holds not f Joins W.m,W.n,G;
:: end;
:: More general notion of a chordal Walk. Is such a notion useful? Or
:: should we stick with chordal Path?
definition
let G be _Graph, W be Walk of G;
attr W is chordal means
ex m, n being odd Nat st m+2 < n
& n <= len W & W.m <> W.n & (ex e being object st e Joins W.m,W.n,G) &
for f being object st f in W.edges() holds not f Joins W.m,W.n,G;
end;
notation
let G be _Graph, W be Walk of G;
antonym W is chordless for W is chordal;
end;
:: The other characterization of chordal is 'more' technical and
:: sometimes more convenient to work with. Is this really true?
:: I have tried to save as much as possible of what Broderic has already done.
:: Need separate theorems for walks and paths! They cannot be put as an iff.
theorem Th83: :: ChordalWalk01
for G being _Graph, W being Walk of G st W is chordal ex m,n
being odd Nat st m+2 < n & n <= len W & W.m <> W.n &
(ex e being object st e Joins W.m,W.n,G) &
(W is Cycle-like implies not (m=1 & n = len W) & not (m
=1 & n = len W-2) & not (m=3 & n = len W))
proof
let G be _Graph, W be Walk of G;
given m, n being odd Nat such that
A1: m+2 < n and
A2: n <= len W and
A3: W.m <> W.n and
A4: ex e being object st e Joins W.m,W.n,G and
A5: for f being object st f in W.edges() holds not f Joins W.m,W.n,G;
take m, n;
thus m+2 < n by A1;
thus n <= len W by A2;
thus W.m <> W.n by A3;
thus ex e being object st e Joins W.m,W.n,G by A4;
A6: W.last() = W.len W;
assume
A7: W is Cycle-like;
then
A8: 3 <= len W by GLIB_001:125;
then reconsider lW2 = len W -2*1 as odd Element of NAT by INT_1:5,XXREAL_0:2;
A9: W.first() = W.1;
then
A10: W.1 = W.len W by A7,A6,GLIB_001:def 24;
reconsider lW2 as odd Nat;
reconsider le = lW2+1 as even Nat;
A11: 1 <= le by NAT_1:12;
A12: lW2 < len W by XREAL_1:44;
then
A13: le <= len W by NAT_1:13;
then le div 2 in dom W.edgeSeq() by A11,GLIB_001:77;
then W.edgeSeq().(le div 2) in rng W.edgeSeq() by FUNCT_1:3;
then
A14: W.(len W -2+1) in W.edges() by A11,A13,GLIB_001:77;
thus not (m=1 & n = len W) by A3,A7,A9,A6,GLIB_001:def 24;
W.(lW2+1) Joins W.(lW2),W.(lW2+2),G by A12,GLIB_001:def 3;
hence not (m=1 & n = len W-2) by A5,A10,A14,GLIB_000:14;
A15: 2*0+1 is odd Nat;
A16: 2*1 div 2 = 1;
A17: 1+1 <= len W by A8,XXREAL_0:2;
then 1 in dom W.edgeSeq() by A16,GLIB_001:77;
then W.edgeSeq().1 in rng W.edgeSeq() by FUNCT_1:3;
then
A18: W.(1+1) in rng W.edgeSeq() by A16,A17,GLIB_001:77;
1 < len W by A8,XXREAL_0:2;
then W.(1+1) Joins W.1,W.(1+2),G by A15,GLIB_001:def 3;
hence thesis by A5,A10,A18,GLIB_000:14;
end;
theorem Th84: :: ChordalPath01
for G being _Graph, P being Path of G st ex m,n being odd Nat
st m+2 < n & n <= len P & (ex e being object st e Joins P.m,P.n,G)
& (P is Cycle-like implies not (m=1 & n = len P) & not (m=1 & n = len P-2) &
not (m=3 & n = len P)) holds P is chordal
proof
let G be _Graph, P be Path of G;
given m, n being odd Nat such that
A1: m+2 < n and
A2: n <= len P and
A3: ex e being object st e Joins P.m,P.n,G and
A4: P is Cycle-like implies not (m=1 & n = len P) & not (m=1 & n = len P
-2) & not (m=3 & n = len P);
A5: n in NAT by ORDINAL1:def 12;
take m,n;
thus m+2 < n by A1;
thus n <= len P by A2;
A6: m in NAT by ORDINAL1:def 12;
A7: m < n by A1,NAT_1:12;
then
A8: m < len P by A2,XXREAL_0:2;
now
assume len P = 1;
then m+2 < 1 by A1,A2,XXREAL_0:2;
hence contradiction by NAT_1:12;
end;
then
A9: P is non trivial by GLIB_001:126;
hereby
assume
A10: P.m = P.n;
then
A11: n = len P by A2,A6,A5,A7,GLIB_001:def 28;
m = 1 by A2,A6,A5,A7,A10,GLIB_001:def 28;
then P is closed by A10,A11;
hence contradiction by A2,A4,A6,A5,A7,A9,A10,GLIB_001:def 28;
end;
thus ex e being object st e Joins P.m,P.n,G by A3;
let f be object such that
A12: f in P.edges() and
A13: f Joins P.m,P.n,G;
consider i being Nat such that
A14: i in dom P.edgeSeq() and
A15: P.edgeSeq().i = f by A12,FINSEQ_2:10;
reconsider i as Element of NAT by ORDINAL1:def 12;
set k = 2*i-1;
A16: 1 <= i by A14,FINSEQ_3:25;
then 2*1 <= 2*i by XREAL_1:64;
then 2-1 <= k by XREAL_1:9;
then
A17: k is Element of NAT by INT_1:3;
i <= len P.edgeSeq() by A14,FINSEQ_3:25;
then
A18: P.edgeSeq().i = P.(2*i) by A16,GLIB_001:def 15;
reconsider k as odd Nat by A17;
2*i in dom P by A14,GLIB_001:78;
then
A19: 2*i <= len P by FINSEQ_3:25;
k+1 = 2*i;
then
A20: k < len P by A19,NAT_1:13;
then
A21: k+2 <= len P by Th4;
A22: k in NAT by ORDINAL1:def 12;
then
A23: P.(k+1) Joins P.k,P.(k+2),G by A20,GLIB_001:def 3;
per cases by A13,A15,A18,A23;
suppose
A24: P.k = P.m & P.(k+2) = P.n;
per cases by XXREAL_0:1;
suppose
k < m;
hence contradiction by A6,A8,A22,A24,GLIB_001:def 28;
end;
suppose
A25: k = m;
per cases by XXREAL_0:1;
suppose
A26: k+2 < n;
A27: 1 <= k by ABIAN:12;
k+2 = 1 by A2,A5,A24,A26,GLIB_001:def 28;
then k+2 < k+1 by A27,NAT_1:13;
hence contradiction by XREAL_1:6;
end;
suppose
k+2 = n;
hence contradiction by A1,A25;
end;
suppose
A28: k+2 > n;
k+2 <= len P by A20,Th4;
then n = 1 by A5,A24,A28,GLIB_001:def 28;
hence contradiction by A1,ABIAN:12;
end;
end;
suppose
k > m;
hence contradiction by A6,A22,A20,A24,GLIB_001:def 28;
end;
end;
suppose
A29: P.k = P.n & P.(k+2) = P.m;
per cases by XXREAL_0:1;
suppose
A30: k < n;
then
A31: n = len P by A2,A5,A22,A29,GLIB_001:def 28;
A32: k = 1 by A2,A5,A22,A29,A30,GLIB_001:def 28;
per cases by XXREAL_0:1;
suppose
k+2 < m;
hence contradiction by A6,A8,A29,GLIB_001:def 28;
end;
suppose
A33: k+2 = m;
P is closed by A29,A32,A31;
hence contradiction by A2,A4,A5,A9,A29,A30,A32,A33,GLIB_001:def 28;
end;
suppose
A34: k+2 > m;
A35: k+2 <= n by A30,Th4;
A36: k+2 = len P by A6,A21,A29,A34,GLIB_001:def 28;
m = 1 by A6,A21,A29,A34,GLIB_001:def 28;
then P is closed by A29,A36;
hence contradiction by A2,A4,A6,A9,A29,A34,A36,A35,GLIB_001:def 28
,XXREAL_0:1;
end;
end;
suppose
A37: k = n;
per cases by XXREAL_0:1;
suppose
k+2 < m;
hence contradiction by A7,A37,NAT_1:12;
end;
suppose
k+2 = m;
hence contradiction by A7,A37,NAT_1:12;
end;
suppose
A38: k+2 > m;
A39: k+2 = len P by A6,A21,A29,A38,GLIB_001:def 28;
m = 1 by A6,A21,A29,A38,GLIB_001:def 28;
then P is closed by A29,A39;
hence contradiction by A4,A6,A9,A29,A37,A38,A39,GLIB_001:def 28;
end;
end;
suppose
k > n;
hence contradiction by A5,A22,A20,A29,GLIB_001:def 28;
end;
end;
end;
theorem Th85: :: ChordalWalk02
for G1,G2 being _Graph st G1 == G2
for W1 being Walk of G1, W2 being Walk of G2 st W1=W2 holds
W1 is chordal implies W2 is chordal
proof
let G1,G2 be _Graph such that
A1: G1 == G2;
let W1 be Walk of G1, W2 be Walk of G2 such that
A2: W1 = W2;
given m, n being odd Nat such that
A3: m+2 < n and
A4: n <= len W1 and
A5: W1.m <> W1.n and
A6: ex e being object st e Joins W1.m,W1.n,G1 and
A7: for f being object st f in W1.edges() holds not f Joins W1.m,W1.n,G1;
take m,n;
thus m+2 < n & n <= len W2 & W2.m <> W2.n by A2,A3,A4,A5;
consider e being object such that
A8: e Joins W1.m,W1.n,G1 by A6;
e Joins W2.m,W2.n,G2 by A1,A2,A8;
hence ex e being object st e Joins W2.m,W2.n,G2;
let f be object;
assume f in W2.edges();
then f in W1.edges() by A2,GLIB_001:110;
then not f Joins W1.m,W1.n,G1 by A7;
hence thesis by A1,A2;
end;
theorem Th86: :: ChordalWalk03
for G being _Graph,
S being non empty Subset of the_Vertices_of G,
H being (inducedSubgraph of G,S),
W1 being Walk of G, W2 being Walk of H st
W1 = W2 holds W2 is chordal iff W1 is chordal
proof
let G be _Graph, S be non empty Subset of the_Vertices_of G,
H be (inducedSubgraph of G,S), W1 be Walk of G, W2 be Walk of H
such that
A1: W1 = W2;
thus W2 is chordal implies W1 is chordal
proof
given m, n being odd Nat such that
A2: m+2 < n and
A3: n <= len W2 and
A4: W2.m <> W2.n and
A5: ex e being object st e Joins W2.m,W2.n,H and
A6: for f being object st f in W2.edges() holds not f Joins W2.m,W2.n,H;
take m,n;
thus m+2 < n & n <= len W1 & W1.m <> W1.n by A1,A2,A3,A4;
consider e being object such that
A7: e Joins W2.m,W2.n,H by A5;
e Joins W1.m,W1.n,G by A1,A7,GLIB_000:72;
hence ex e being object st e Joins W1.m,W1.n,G;
let f be object;
assume f in W1.edges();
then
A8: f in W2.edges() by A1,GLIB_001:110;
then not f Joins W1.m,W1.n,H by A1,A6;
hence thesis by A8,GLIB_000:73;
end;
A9: S = the_Vertices_of H by GLIB_000:def 37;
thus W1 is chordal implies W2 is chordal
proof
given m, n being odd Nat such that
A10: m+2 < n and
A11: n <= len W1 and
A12: W1.m <> W1.n and
A13: ex e being object st e Joins W1.m,W1.n,G and
A14: for f being object st f in W1.edges() holds not f Joins W1.m,W1.n,G;
take m,n;
thus m+2 < n & n <= len W2 & W2.m <> W2.n by A1,A10,A11,A12;
A15: m in NAT by ORDINAL1:def 12;
n in NAT by ORDINAL1:def 12;
then
A16: W1.n in the_Vertices_of H by A1,A11,GLIB_001:7;
m < n by A10,NAT_1:12;
then W1.m in the_Vertices_of H by A1,A11,A15,GLIB_001:7,XXREAL_0:2;
hence ex e being object st e Joins W2.m,W2.n,H by A1,A9,A13,A16,Th19;
let f be object;
assume f in W2.edges();
then f in W1.edges() by A1,GLIB_001:110;
then not f Joins W2.m,W2.n,G by A1,A14;
hence thesis by GLIB_000:72;
end;
end;
theorem
for G being _Graph, W being Walk of G st
W is Cycle-like & W is chordal & W.length()=4
ex e being object st e Joins W.1,W.5,G or e Joins W.3,W.7,G
proof
let G be _Graph, W be Walk of G such that
A1: W is Cycle-like and
A2: W is chordal and
A3: W.length() = 4;
A4: len W = 2*4+1 by A3,GLIB_001:112;
consider m, n being odd Nat such that
A5: m+2 < n and
A6: n <= len W and
W.m <> W.n and
A7: ex e being object st e Joins W.m,W.n,G and
A8: W is Cycle-like implies not (m=1 & n = len W) & not (m=1 & n = len
W-2) & not (m=3 & n = len W) by A2,Th83;
consider e being object such that
A9: e Joins W.m,W.n,G by A7;
assume
A10: not(ex e being object st e Joins W.1,W.5,G or e Joins W.3,W.7,G);
A11: now
assume
A12: m = 3;
then n < len W by A1,A6,A8,XXREAL_0:1;
then
A13: n <= 9 - 2 by A4,Th3;
n <> 7 by A10,A9,A12;
then n < 2*3+1 by A13,XXREAL_0:1;
then n <= 7 - 2 by Th3;
hence contradiction by A5,A12;
end;
A14: now
reconsider jj=2*3+1 as odd Nat;
assume
A15: m = 1;
then n < len W by A1,A6,A8,XXREAL_0:1;
then n <= 9 - 2 by A4,Th3;
then n < jj by A1,A4,A8,A15,XXREAL_0:1;
then
A16: n <= jj-2 by Th3;
n <> 5 by A10,A9,A15;
then n < 2*2+1 by A16,XXREAL_0:1;
then n <= 5-2 by Th3;
hence contradiction by A5,A15;
end;
A17: W.first() = W.last() by A1,GLIB_001:def 24;
A18: now
assume
A19: m = 5;
n <> 9 by A17,A4,A9,A19,GLIB_000:14,A10;
then n < len W by A4,A6,XXREAL_0:1;
then n <= len W - 2 by Th3;
hence contradiction by A4,A5,A19;
end;
0+1 <= m by ABIAN:12;
then 2*0+1 < m by A14,XXREAL_0:1;
then 1+2 <= m by Th4;
then 2*1+1 < m by A11,XXREAL_0:1;
then 3+2 <= m by Th4;
then 2*2+1 < m by A18,XXREAL_0:1;
then 5+2 <= m by Th4;
then 7+2 <= m + 2 by XREAL_1:7;
hence contradiction by A4,A5,A6,XXREAL_0:2;
end;
theorem Th88: :: MinChordal01
for G being _Graph, W being Walk of G st W is minlength holds W is chordless
by Th39;
theorem
for G being _Graph, W being Walk of G st
len W = 5 & not W.first(),W.last() are_adjacent holds W is chordless
proof
let G be _Graph, W be Walk of G such that
A1: len W = 5 and
A2: not W.first(),W.last() are_adjacent;
assume W is chordal;
then consider m,n being odd Nat such that
A3: m+2 < n and
A4: n <= len W and
W.m <> W.n and
A5: ex e being object st e Joins W.m,W.n,G and
W is Cycle-like implies not (m=1 & n = len W) & not (m=1 & n = len W-2)
& not (m=3 & n = len W) by Th83;
A6: now
assume
A7: m <> 1;
1 <= m by Th2;
then 2*0+1 < m by A7,XXREAL_0:1;
then 1+2 <= m by Th4;
then 3+2 <= m+2 by XREAL_1:7;
hence contradiction by A1,A3,A4,XXREAL_0:2;
end;
then 3+2 <= n by A3,Th4;
then W.n = W.last() by A1,A4,XXREAL_0:1;
hence contradiction by A2,A5,A6;
end;
Lm3: for G being _Graph, W being Walk of G holds W is chordal implies W
.reverse() is chordal
proof
let G be _Graph, W be Walk of G;
set U = W.reverse();
assume W is chordal;
then consider m, n being odd Nat such that
A1: m+2 < n and
A2: n <= len W and
A3: W.m <> W.n and
A4: ex e being object st e Joins W.m,W.n,G and
A5: for f being object st f in W.edges() holds not f Joins W.m,W.n,G;
consider e being object such that
A6: e Joins W.m,W.n,G by A4;
set um = len W - m + 1, un = len W - n + 1;
m < m+2 by XREAL_1:29;
then
A7: m < n by A1,XXREAL_0:2;
then reconsider um, un as odd Element of NAT by A2,FINSEQ_5:1,XXREAL_0:2;
reconsider um, un as odd Nat;
A8: un + 2 < um by A1,Lm1;
1 <= n by Th2;
then n in dom W by A2,FINSEQ_3:25;
then
A9: W.n = U.un by GLIB_001:24;
A10: 1 <= m by Th2;
len W - m + 1 <= len W by INT_1:7,XREAL_1:44;
then
A11: um <= len U by GLIB_001:21;
m <= len W by A2,A7,XXREAL_0:2;
then m in dom W by A10,FINSEQ_3:25;
then
A12: W.m = U.um by GLIB_001:24;
then
A13: e Joins U.un,U.um,G by A6,A9;
W.edges() = U.edges() by GLIB_001:107;
then for f being object st f in U.edges() holds not f Joins U.un,U.um,G
by A5,A12,A9,GLIB_000:14;
hence thesis by A3,A8,A11,A12,A9,A13;
end;
theorem
for G being _Graph, W being Walk of G holds
W is chordal iff W.reverse() is chordal
proof
let G be _Graph, W be Walk of G;
thus W is chordal implies W.reverse() is chordal by Lm3;
assume W.reverse() is chordal;
then W.reverse().reverse() is chordal by Lm3;
hence thesis;
end;
theorem Th91: :: CPath03
for G being _Graph, P being Path of G st
P is open & P is chordless
for m,n being odd Nat st m < n & n <= len P holds
(ex e being object st e Joins P.m,P.n,G) iff m+2 = n
proof
let G be _Graph, P be Path of G such that
A1: P is open and
A2: P is chordless;
A3: P is vertex-distinct by A1,Th32;
let m,n be odd Nat such that
A4: m < n and
A5: n <= len P;
A6: m <= len P by A4,A5,XXREAL_0:2;
A7: m in NAT by ORDINAL1:def 12;
A8: n in NAT by ORDINAL1:def 12;
then
A9: P.m <> P.n by A1,A4,A5,A7,GLIB_001:147;
hereby
assume
A10: ex e being object st e Joins P.m,P.n,G;
A11: now
assume
A12: m+2 < n;
now
let f be object;
assume f in P.edges();
then consider k being odd Element of NAT such that
A13: k < len P and
A14: P.(k+1) = f by GLIB_001:100;
A15: f Joins P.k,P.(k+2),G by A13,A14,GLIB_001:def 3;
A16: k+2 <= len P by A13,Th4;
assume
A17: f Joins P.m,P.n,G;
per cases by A15,A17;
suppose
A18: P.m = P.k & P.n = P.(k+2);
then m = k by A7,A3,A6,A13;
hence contradiction by A5,A8,A3,A12,A16,A18;
end;
suppose
A19: P.m = P.(k+2) & P.n = P.k;
then
A20: n = k by A5,A8,A3,A13;
m = k+2*1 by A7,A3,A6,A16,A19;
then
A21: m > n by A20,XREAL_1:29;
m+2 > m by XREAL_1:29;
hence contradiction by A12,A21,XXREAL_0:2;
end;
end;
hence contradiction by A2,A5,A9,A10,A12;
end;
m+2 <= n by A4,Th4;
hence m+2 = n by A11,XXREAL_0:1;
end;
assume
A22: m+2 = n;
take P.(m+1);
m < len P by A4,A5,XXREAL_0:2;
hence thesis by A7,A22,GLIB_001:def 3;
end;
theorem
for G being _Graph, P being Path of G st P is open & P is chordless
for m,n being odd Nat st m < n & n <= len P holds P.cut(m,n) is
chordless & P.cut(m,n) is open
proof
let G be _Graph, P be Path of G such that
A1: P is open and
A2: P is chordless;
let m,n be odd Nat such that
A3: m < n and
A4: n <= len P;
set Q = P.cut(m,n);
A5: n in NAT by ORDINAL1:def 12;
A6: m in NAT by ORDINAL1:def 12;
now
assume Q is chordal;
then consider i,j being odd Nat such that
A7: i+2 < j and
A8: j <= len Q and
Q.i <> Q.j and
A9: ex e being object st e Joins Q.i,Q.j,G and
for f being object st f in Q.edges() holds not f Joins Q.i,Q.j,G;
consider e being object such that
A10: e Joins Q.i,Q.j,G by A9;
set mi = m+i-1;
set mj = m+j-1;
1 <= j by Th2;
then
A11: j in dom Q by A8,FINSEQ_3:25;
then
A12: Q.j = P.mj by A3,A4,A6,A5,GLIB_001:47;
A13: mj in dom P by A3,A4,A6,A5,A11,GLIB_001:47;
i+0<i+2 by XREAL_1:8;
then i<j by A7,XXREAL_0:2;
then
A14: i < len Q by A8,XXREAL_0:2;
1 <= i by Th2;
then
A15: i in dom Q by A14,FINSEQ_3:25;
then
A16: mi in dom P by A3,A4,A6,A5,GLIB_001:47;
reconsider mj as odd Element of NAT by A13;
reconsider mj as odd Nat;
A17: mj <= len P by A13,FINSEQ_3:25;
reconsider mi as odd Element of NAT by A16;
reconsider mi as odd Nat;
i+2+m < j+m by A7,XREAL_1:8;
then
A18: m+i+2-1 < m+j-1 by XREAL_1:9;
then
A19: mi+2 < mj;
mi+0 < mi+2 by XREAL_1:8;
then
A20: mi < mj by A18,XXREAL_0:2;
e Joins P.mi,P.mj,G by A3,A4,A6,A5,A10,A15,A12,GLIB_001:47;
hence contradiction by A1,A2,A19,A20,A17,Th91;
end;
hence Q is chordless;
now
assume Q is closed;
then
A21: Q.first() = Q.last();
A22: P.n = Q.last() by A3,A4,A6,A5,GLIB_001:37;
P.m = Q.first() by A3,A4,A6,A5,GLIB_001:37;
hence contradiction by A1,A3,A4,A6,A5,A21,A22,GLIB_001:147;
end;
hence thesis;
end;
theorem
for G being _Graph, S being non empty Subset of the_Vertices_of G,
H being (inducedSubgraph of G,S), W being Walk of G, V being Walk of H st
W = V holds W is chordless iff V is chordless
proof
let G be _Graph, S be non empty Subset of the_Vertices_of G;
let H be inducedSubgraph of G,S;
let W be Walk of G, V be Walk of H such that
A1: W = V;
hereby
assume
A2: W is chordless;
assume V is chordal;
then consider m,n being odd Nat such that
A3: m+2 < n and
A4: n <= len V and
A5: V.m <> V.n and
A6: ex e being object st e Joins V.m,V.n,H and
A7: for f being object st f in V.edges() holds not f Joins V.m,V.n,H;
consider e being object such that
A8: e Joins V.m,V.n,H by A6;
n in NAT by ORDINAL1:def 12;
then V.n in V.vertices() by A4,GLIB_001:87;
then V.n in the_Vertices_of H;
then
A9: V.n in S by GLIB_000:def 37;
m+0 <= m+2 by XREAL_1:7;
then m <= n by A3,XXREAL_0:2;
then
A10: m <= len V by A4,XXREAL_0:2;
m in NAT by ORDINAL1:def 12;
then V.m in V.vertices() by A10,GLIB_001:87;
then V.m in the_Vertices_of H;
then
A11: V.m in S by GLIB_000:def 37;
A12: for f being object st f in W.edges() holds not f Joins W.m,W.n,G
proof
let f be object;
assume f in W.edges();
then
A13: f in V.edges() by A1,GLIB_001:110;
assume f Joins W.m,W.n,G;
hence contradiction by A1,A7,A9,A11,A13,Th19;
end;
e Joins W.m,W.n,G by A1,A8,GLIB_000:72;
hence contradiction by A1,A2,A3,A4,A5,A12;
end;
assume
A14: V is chordless;
assume W is chordal;
then consider m,n being odd Nat such that
A15: m+2 < n and
A16: n <= len W and
A17: W.m <> W.n and
A18: ex e being object st e Joins W.m,W.n,G and
A19: for f being object st f in W.edges() holds not f Joins W.m,W.n,G;
consider e being object such that
A20: e Joins W.m,W.n,G by A18;
A21: for f being object st f in V.edges() holds not f Joins V.m,V.n,H
proof
let f be object;
assume f in V.edges();
then
A22: f in W.edges() by A1,GLIB_001:110;
assume f Joins V.m,V.n,H;
then f Joins W.m,W.n,G by A1,GLIB_000:72;
hence contradiction by A19,A22;
end;
n in NAT by ORDINAL1:def 12;
then W.n in V.vertices() by A1,A16,GLIB_001:87;
then W.n in the_Vertices_of H;
then
A23: W.n in S by GLIB_000:def 37;
m+0 <= m+2 by XREAL_1:7;
then m <= n by A15,XXREAL_0:2;
then
A24: m <= len W by A16,XXREAL_0:2;
m in NAT by ORDINAL1:def 12;
then W.m in V.vertices() by A1,A24,GLIB_001:87;
then W.m in the_Vertices_of H;
then W.m in S by GLIB_000:def 37;
then e Joins V.m,V.n,H by A1,A20,A23,Th19;
hence contradiction by A1,A14,A15,A16,A17,A21;
end;
definition
let G be _Graph;
attr G is chordal means
:Def11:
for P being Walk of G st P.length() > 3 & P is Cycle-like holds P is chordal;
end;
theorem Th94: :: Chordal01
for G1,G2 being _Graph st G1 == G2 holds G1 is chordal implies G2 is chordal
proof
let G1,G2 be _Graph such that
A1: G1 == G2;
assume
A2: G1 is chordal;
now
let W be Walk of G2 such that
A3: W.length() > 3 and
A4: W is Cycle-like;
reconsider W2=W as Walk of G1 by A1,GLIB_001:179;
2*W2.length() + 1 = len W by GLIB_001:112;
then
A5: 2*W2.length() + 1 = 2*W.length() + 1 by GLIB_001:112;
W2 is Cycle-like by A4,Th24;
then W2 is chordal by A2,A3,A5;
hence W is chordal by A1,Th85;
end;
hence thesis;
end;
theorem Th95: :: Chordal02
for G being _finite _Graph st card the_Vertices_of G <= 3 holds G is chordal
proof
let G be _finite _Graph such that
A1: card the_Vertices_of G <= 3;
now
reconsider n4=2*3+1 as odd Nat;
reconsider n3=2*2+1 as odd Nat;
reconsider n2=2*1+1 as odd Nat;
reconsider n1=2*0+1 as odd Nat;
let W be Walk of G such that
A2: W.length() > 3 and
A3: W is Cycle-like;
set x3=W.n3;
set x2=W.n2;
set x4=W.n4;
set x1=W.n1;
W.length() >= 3+1 by A2,NAT_1:13;
then 2*W.length() >= 2*4 by XREAL_1:64;
then 2*W.length() + 1 >= 8 + 1 by XREAL_1:7;
then
A4: len W >= 9 by GLIB_001:112;
then
A5: n4 < len W by XXREAL_0:2;
then
A6: x1 <> x4 by A3,GLIB_001:def 28;
n2 < len W by A4,XXREAL_0:2;
then
A7: x1 <> x2 by A3,GLIB_001:def 28;
A8: n3 < len W by A4,XXREAL_0:2;
then
A9: x2 <> x3 by A3,GLIB_001:def 28;
A10: x3 <> x4 by A3,A5,GLIB_001:def 28;
A11: x2 <> x4 by A3,A5,GLIB_001:def 28;
now
let x be object;
assume
A12: x in {x1,x2,x3,x4};
now
per cases by A12,ENUMSET1:def 2;
suppose
x=x1;
hence x in the_Vertices_of G by A4,GLIB_001:7,XXREAL_0:2;
end;
suppose
x=x2;
hence x in the_Vertices_of G by A4,GLIB_001:7,XXREAL_0:2;
end;
suppose
x=x3;
hence x in the_Vertices_of G by A4,GLIB_001:7,XXREAL_0:2;
end;
suppose
x=x4;
hence x in the_Vertices_of G by A4,GLIB_001:7,XXREAL_0:2;
end;
end;
hence x in the_Vertices_of G;
end;
then
A13: {x1,x2,x3,x4} c= the_Vertices_of G;
x1 <> x3 by A3,A8,GLIB_001:def 28;
then card {x1,x2,x3,x4} = 4 by A7,A6,A9,A11,A10,CARD_2:59;
then 4 <= card the_Vertices_of G by A13,NAT_1:43;
hence contradiction by A1,XXREAL_0:2;
end;
then for W being Walk of G st W.length() > 3 & W is Cycle-like holds W is
chordal;
hence thesis;
end;
registration
cluster _trivial _finite chordal for _Graph;
existence
proof
set G = the _trivial _finite _Graph;
consider v being Vertex of G such that
A1: the_Vertices_of G = {v} by GLIB_000:22;
now
reconsider j5=2*2+1 as odd Nat;
reconsider j3=2*1+1 as odd Nat;
let W be Walk of G such that
A2: W.length() > 3 and
A3: W is Cycle-like;
2*W.length() > 2*3 by A2,XREAL_1:68;
then 2*W.length() + 1 > 6 + 1 by XREAL_1:8;
then
A4: len W > 7 by GLIB_001:112;
then j3 <= len W by XXREAL_0:2;
then W.j3 in W.vertices() by GLIB_001:87;
then
A5: W.j3 = v by A1,TARSKI:def 1;
A6: j5 <= len W by A4,XXREAL_0:2;
then W.j5 in W.vertices() by GLIB_001:87;
then W.j5 = v by A1,TARSKI:def 1;
hence contradiction by A3,A6,A5,GLIB_001:def 28;
end;
then for W being Walk of G st W.length() > 3 & W is Cycle-like holds W is
chordal;
then G is chordal;
hence thesis;
end;
cluster non _trivial _finite simple chordal for _Graph;
existence
proof
set V = {0,1}, E = {0}, S = 0 .--> 0, T = 0 .--> 1;
A7: dom T = E;
A8: now
let x be object;
assume x in E;
then x = 0 by TARSKI:def 1;
then T.x = 1 by FUNCOP_1:72;
hence T.x in V by TARSKI:def 2;
end;
A9: now
let x be object;
assume x in E;
then x = 0 by TARSKI:def 1;
then S.x = 0 by FUNCOP_1:72;
hence S.x in V by TARSKI:def 2;
end;
reconsider T as Function of E,V by A7,A8,FUNCT_2:3;
dom S = E;
then reconsider S as Function of E,V by A9,FUNCT_2:3;
set G = createGraph(V,E,S,T);
take G;
A10: (the_Source_of G).0 = 0 by FUNCOP_1:72;
now
assume card (the_Vertices_of G) = 1;
then ex x being object st the_Vertices_of G = {x} by CARD_2:42;
hence contradiction by ZFMISC_1:5;
end;
hence G is non _trivial & G is _finite;
A12: (the_Target_of G).0 = 1 by FUNCOP_1:72;
0 in the_Edges_of G by TARSKI:def 1;
then
A14: 0 Joins 0,1,G by A10,A12;
now
let v be object;
let e being object such that
A15: e Joins v,v,G;
reconsider v as Vertex of G by A15,GLIB_000:13;
e in the_Edges_of G by A15;
then e Joins 0,1,G by A14,TARSKI:def 1;
then 0 = v & 1 = v or 0 = v & 1 = v by A15;
hence contradiction;
end;
then
A16: G is loopless by GLIB_000:18;
now
let e1,e2,v1,v2 be object such that
A17: e1 Joins v1,v2,G and
A18: e2 Joins v1,v2,G;
e1 in {0} by A17;
then
A19: e1 = 0 by TARSKI:def 1;
assume
A20: e1 <> e2;
e2 in {0} by A18;
hence contradiction by A20,A19,TARSKI:def 1;
end;
then G is non-multi;
hence G is simple by A16;
card the_Vertices_of G = 2 by CARD_2:57;
hence thesis by Th95;
end;
cluster complete -> chordal for _Graph;
correctness
proof
let G be _Graph;
assume
A21: G is complete;
now
reconsider t7=2*3+1 as odd Nat;
reconsider t3=2*1+1 as odd Nat;
let W be Walk of G such that
A22: W.length() > 3 and
A23: W is Cycle-like;
W.length() >= 3+1 by A22,NAT_1:13;
then 2*W.length() >= 2*4 by XREAL_1:64;
then 2*W.length() + 1 >= 8 + 1 by XREAL_1:7;
then
A24: len W >= 9 by GLIB_001:112;
then reconsider W3=W.t3 as Vertex of G by GLIB_001:7,XXREAL_0:2;
A25: not (t3=3 & t7 = len W) by A24;
reconsider W7=W.t7 as Vertex of G by A24,GLIB_001:7,XXREAL_0:2;
t7 <= len W by A24,XXREAL_0:2;
then W3 <> W7 by A23,GLIB_001:def 28;
then W3,W7 are_adjacent by A21;
then
A26: ex e being object st e Joins W3,W7,G;
A27: t3+2 < t7;
t7 <= len W by A24,XXREAL_0:2;
hence W is chordal by A23,A26,A27,A25,Th84;
end;
hence thesis;
end;
end;
registration
let G be chordal _Graph, V be set;
cluster -> chordal for inducedSubgraph of G,V;
coherence
proof
let H be inducedSubgraph of G,V;
now
per cases;
suppose
not V is non empty Subset of the_Vertices_of G;
then H == G by GLIB_000:def 37;
hence thesis by Th94;
end;
suppose
V is non empty Subset of the_Vertices_of G;
then
A1: V = the_Vertices_of H by GLIB_000:def 37;
now
let W be Walk of H such that
A2: W.length() > 3 and
A3: W is Cycle-like;
reconsider P=W as Walk of G by GLIB_001:167;
reconsider P as Path of G by A3,GLIB_001:175;
A4: P is non trivial by A3;
A5: P.length() > 3 by A2,GLIB_001:114;
A6: P is closed by A3,GLIB_001:176;
then P is Cycle-like by A4;
then P is chordal by A5,Def11;
then consider m, n being odd Nat such that
A7: m+2 < n and
A8: n <= len P and
P.m <> P.n and
A9: ex e being object st e Joins P.m,P.n,G and
A10: P is Cycle-like implies not (m=1 & n = len P) & not (m=1 &
n = len P-2) & not (m=3 & n = len P) by Th83;
consider e being object such that
A11: e Joins P.m,P.n,G by A9;
m + 0 <= m + 2 by XREAL_1:7;
then
A12: m <= n by A7,XXREAL_0:2;
n in NAT by ORDINAL1:def 12;
then
A13: P.n in the_Vertices_of H by A8,GLIB_001:7;
m in NAT by ORDINAL1:def 12;
then P.m in the_Vertices_of H by A8,A12,GLIB_001:7,XXREAL_0:2;
then e Joins P.m,W.n,H by A1,A11,A13,Th19;
hence W is chordal by A3,A6,A7,A8,A10,Th84;
end;
hence thesis;
end;
end;
hence thesis;
end;
end;
theorem
for G being chordal _Graph, P being Path of G st P is open & P is
chordless
for x,e being object st (not x in P.vertices() & e Joins P.last(),x,G &
not ex f being object st f Joins P.(len P-2),x,G)
holds P.addEdge(e) is Path-like
& P.addEdge(e) is open & P.addEdge(e) is chordless
proof
let G be chordal _Graph, P be Path of G such that
A1: P is open and
A2: P is chordless;
let x,e be object such that
A3: not x in P.vertices() and
A4: e Joins P.last(),x,G and
A5: not ex f being object st f Joins P.(len P-2),x,G;
reconsider Q = P.addEdge(e) as Path of G by A1,A3,A4,GLIB_001:151;
A6: len Q = len P + 2 by A4,GLIB_001:64;
defpred P[Nat] means (4 <= 2*$1 & 2*$1 <= len P+1) implies for j being odd
Nat st j + 2*$1 = len P + 2
holds not ex e being object st e Joins Q.j,x,G;
A7: now
let n be odd Nat such that
A8: n <= len P;
1 <= n by Th2;
then n in dom P by A8,FINSEQ_3:25;
hence P.n = Q.n by A4,GLIB_001:65;
end;
A9: Q.last() = x by A4,GLIB_001:63;
for k being Nat st for a being Nat st a < k holds P[a] holds P[k]
proof
let k be Nat such that
A10: for a being Nat st a < k holds P[a];
assume that
A11: 4 <= 2*k and
2*k <= len P+1;
let j be odd Nat such that
A12: j + 2*k = len P + 2;
j + 4 <= j + 2*k by A11,XREAL_1:7;
then
A13: j + 4 - 4 <= len P + 2 - 4 by A12,XREAL_1:9;
A14: len P - 2 <= len P by XREAL_1:43;
then
A15: j <= len P by A13,XXREAL_0:2;
A16: j in NAT by ORDINAL1:def 12;
let e be object such that
A17: e Joins Q.j,x,G;
per cases by A13,XXREAL_0:1;
suppose
j = len P - 2;
then Q.j = P.(len P - 2) by A7,XREAL_1:43;
hence contradiction by A5,A17;
end;
suppose
A18: j < len P - 2*1;
reconsider lP2 = len P+2 as odd Element of NAT;
reconsider jj = j as odd Element of NAT by ORDINAL1:def 12;
set B = Q.cut(jj,lP2);
len P < len P + 2 by XREAL_1:29;
then
A19: j <= len P + 2 by A15,XXREAL_0:2;
then
A20: B.last() = x by A9,A6,GLIB_001:37;
A21: len B + j = len P + 2 + 1 by A6,A19,GLIB_001:36;
A22: now
let i be even Nat such that
A23: i < len B-1;
j + i < (len B - 1) + j by A23,XREAL_1:8;
then
A24: j + i <= len P + 2 - 2 by A21,Th3;
len B - 1 < len B by XREAL_1:44;
then
A25: i < len B by A23,XXREAL_0:2;
A26: i in NAT by ORDINAL1:def 12;
then j+i in dom Q by A6,A19,A25,GLIB_001:36;
then
A27: 1 <= j + i by FINSEQ_3:25;
B.(i+1) = Q.(j+i) by A6,A19,A26,A25,GLIB_001:36;
hence B.(i+1) = P.(j+i) & j+i in dom P by A7,A27,A24,FINSEQ_3:25;
end;
set C = B.addEdge(e);
A28: B.first() = Q.j by A6,A19,GLIB_001:37;
A29: B.first() = Q.j by A6,A19,GLIB_001:37;
then
A30: e Joins B.last(),B.first(),G by A17,A20;
A31: now
let n be odd Nat such that
A32: n <= len B;
1 <= n by Th2;
then n in dom B by A32,FINSEQ_3:25;
hence C.n = B.n by A30,GLIB_001:65;
end;
A33: len P + 3 - (len P - 2) < len P + 3 - j by A18,XREAL_1:15;
then
A34: 3 < len B by A21,XXREAL_0:2;
len B + 2 > 5 + 2 by A21,A33,XREAL_1:8;
then
A35: len C > 7 by A17,A20,GLIB_000:14,GLIB_001:64;
A36: now
assume C.length() <= 3;
then 2*C.length() <= 2*3 by XREAL_1:64;
then 2*C.length()+1 <= 2*3+1 by XREAL_1:6;
hence contradiction by A35,GLIB_001:112;
end;
P.vertexAt(j) = P.j by A15,GLIB_001:def 8;
then P.j in P.vertices() by A16,A13,A14,GLIB_001:89,XXREAL_0:2;
then B.first() in P.vertices() by A7,A13,A14,A28,XXREAL_0:2;
then
A37: B is open by A3,A20;
then C is Cycle-like by A17,A34,A29,A20,Th33,GLIB_000:14;
then C is chordal by A36,Def11;
then consider m,n being odd Nat such that
A38: m+2 < n and
A39: n <= len C and
A40: C.m <> C.n and
A41: ex e being object st e Joins C.m,C.n,G and
A42: C is Cycle-like implies not (m=1 & n = len C) & not (m=1 & n =
len C-2) & not (m=3 & n = len C) by Th83;
consider e being object such that
A43: e Joins C.m,C.n,G by A41;
1 <= m by Th2;
then 1-1 <= m-1 by XREAL_1:9;
then reconsider m1 = m-1 as even Element of NAT by INT_1:3;
reconsider m1 as even Nat;
A44: len C = len B + 2 by A17,A20,GLIB_000:14,GLIB_001:64;
then m+2 < len B+2 by A38,A39,XXREAL_0:2;
then
A45: m+2-2 < len B+2-2 by XREAL_1:9;
then
A46: m1 < len B-1 by XREAL_1:9;
then
A47: B.(m1+1) = P.(j+m1) by A22;
A48: j+m1 in dom P by A22,A46;
then
A49: j+m1 <= len P by FINSEQ_3:25;
A50: C.last() = Q.j by A28,A30,GLIB_001:63;
now
assume
A51: n = len C;
then e Joins P.(j+m1),Q.j,G by A31,A50,A43,A45,A47;
then e Joins P.(j+m1),P.j,G by A7,A13,A14,XXREAL_0:2;
then
A52: e Joins P.j,P.(j+m1),G;
3 < m by A17,A34,A29,A20,A37,A42,A51,Th7,Th33,GLIB_000:14,XXREAL_0:2;
then
A53: 2+1-1 < m-1 by XREAL_1:9;
then
A54: j < j+m1 by XREAL_1:29;
j + 2 < j+m1 by A53,XREAL_1:8;
hence contradiction by A1,A2,A49,A52,A54,Th91;
end;
then n < len B+2*1 by A44,A39,XXREAL_0:1;
then
A55: n <= len B+2-2 by Th3;
then
A56: C.n = B.n by A31;
1 <= n by Th2;
then 1-1 <= n-1 by XREAL_1:9;
then reconsider n1 = n-1 as even Element of NAT by INT_1:3;
reconsider n1 as even Nat;
m+2-1 <n-1 by A38,XREAL_1:9;
then j+(m1+2) < j+n1 by XREAL_1:8;
then
A57: j+m1+2 < j+n1;
now
C.m = B.m by A31,A45;
then
A58: C.m = Q.(j+m1) by A7,A47,A49;
A59: len P < len P + 2 by XREAL_1:29;
j+m1 <= len P by A48,FINSEQ_3:25;
then consider kk being Nat such that
A60: (j+m1) + 2*kk = len P+2 by A59,Lm2,XXREAL_0:2;
assume
A61: n = len B;
A62: now
assume 2*kk < 3+1;
then 2*kk <= 3 by NAT_1:13;
then 2*kk = 0 or 2*kk = 2 by Th11;
hence contradiction by A21,A38,A40,A61,A60;
end;
1 <= m by Th2;
then 1 < m by A34,A37,A30,A44,A42,A61,Th33,XXREAL_0:1;
then
A63: 1-1 < m-1 by XREAL_1:9;
A64: now
assume 2*kk > len P + 1;
then 2*kk >= len P + 1 + 1 by NAT_1:13;
hence contradiction by A60,XREAL_1:29;
end;
A65: now
assume kk >= k;
then
A66: 2*kk >= 2*k by XREAL_1:64;
j + 2*kk + m1 > j + 2*kk by A63,XREAL_1:29;
hence contradiction by A12,A60,A66,XREAL_1:7;
end;
C.n = x by A20,A31,A61;
hence contradiction by A10,A43,A60,A62,A64,A65,A58;
end;
then n < len B by A55,XXREAL_0:1;
then
A67: n1 < len B-1 by XREAL_1:9;
then j+n1 in dom P by A22;
then
A68: j+n1 <= len P by FINSEQ_3:25;
m < m+2 by XREAL_1:29;
then m < n by A38,XXREAL_0:2;
then m1 < n1 by XREAL_1:9;
then
A69: j+m1 < j+n1 by XREAL_1:8;
A70: C.m = B.m by A31,A45;
B.(n1+1) = P.(j+n1) by A22,A67;
hence contradiction by A1,A2,A43,A47,A68,A70,A56,A69,A57,Th91;
end;
end;
then
A71: for k being Nat st for a being Nat st a < k holds P[a] holds P[k];
A72: for k being Nat holds P[k] from NAT_1:sch 4(A71);
A73: now
let n be odd Nat such that
A74: n <= len P-2;
len P-2 <= len P-2+4 by XREAL_1:31;
then consider k being Nat such that
A75: n + 2*k = len P + 2 by A74,Lm2,XXREAL_0:2;
A76: now
assume 2*k > len P + 1;
then n + 2*k > 1 + (len P + 1) by Th2,XREAL_1:8;
hence contradiction by A75;
end;
now
assume
A77: 2*k < 4;
n + 4 <= len P-2+4 by A74,XREAL_1:7;
hence contradiction by A75,A77,XREAL_1:8;
end;
hence not ex e being object st e Joins Q.n,x,G by A72,A75,A76;
end;
A78: now
assume Q is chordal;
then consider m,n being odd Nat such that
A79: m+2 < n and
A80: n <= len Q and
Q.m <> Q.n and
A81: ex e being object st e Joins Q.m,Q.n,G and
Q is Cycle-like implies not (m=1 & n = len Q) & not (m=1 & n = len Q-2
) & not (m=3 & n = len Q) by Th83;
m+2 < len P+2 by A6,A79,A80,XXREAL_0:2;
then
A82: m+2-2 < len P+2-2 by XREAL_1:9;
m < m+2 by XREAL_1:29;
then
A83: m < n by A79,XXREAL_0:2;
per cases by A80,XXREAL_0:1;
suppose
A84: n = len Q;
then m+2-2 < len P+2-2 by A6,A79,XREAL_1:9;
hence contradiction by A9,A73,A81,A84,Th3;
end;
suppose
A85: n < len Q;
A86: Q.m = P.m by A7,A82;
A87: n <= len P + 2 - 2 by A6,A85,Th3;
then Q.n = P.n by A7;
hence contradiction by A1,A2,A79,A81,A83,A87,A86,Th91;
end;
end;
Q.first() = P.first() by A4,GLIB_001:63;
then Q.first() in P.vertices() by GLIB_001:88;
hence thesis by A3,A9,A78;
end;
:: Golumbic, page 83. Theorem 4.1 (i) ==> (iii)
theorem Th97:
for G being chordal _Graph, a,b being Vertex of G st a<>b & not
a,b are_adjacent for S being VertexSeparator of a,b st S is minimal & S is non
empty for H being inducedSubgraph of G,S holds H is complete
proof
let G be chordal _Graph;
set tVG = the_Vertices_of G;
let a,b be Vertex of G such that
A1: a<>b and
A2: not a,b are_adjacent;
let S be VertexSeparator of a,b such that
A3: S is minimal and
A4: S is non empty;
set Gns = the removeVertices of G,S;
reconsider sa = a, sb = b as Vertex of Gns by A1,A2,Th76;
set A = Gns.reachableFrom(sa), B = Gns.reachableFrom(sb);
A5: A/\B = {} by A1,A2,Th75;
set Gb = the inducedSubgraph of Gns,B;
set Ga = the inducedSubgraph of Gns,A;
A6: the_Vertices_of Ga = A by GLIB_000:def 37;
A7: the_Vertices_of Gb = B by GLIB_000:def 37;
A8: B /\ S = {} by A1,A2,Th74;
A9: A/\S = {} by A1,A2,Th74;
the_Vertices_of Gns c= tVG;
then reconsider A, B as non empty Subset of tVG by XBOOLE_1:1;
let Gs be inducedSubgraph of G,S;
let x,y be Vertex of Gs such that
A10: x <> y and
A11: not x,y are_adjacent;
reconsider xg = x, yg = y as Vertex of G by GLIB_000:42;
A12: S = the_Vertices_of Gs by A4,GLIB_000:def 37;
then
A13: ex xag being Vertex of G st xag in A & xg,xag are_adjacent by A1,A2,A3
,Th81;
set Bx = B\/{xg}, Ax = A\/{xg};
set Gbx = the inducedSubgraph of G,Bx;
set Gax = the inducedSubgraph of G,Ax;
set xy = {xg, yg};
A14: the_Vertices_of Gbx = Bx by GLIB_000:def 37;
now
let x be object such that
A15: x in A;
not x in S by A9,A15,XBOOLE_0:def 4;
hence x in tVG \ S by A15,XBOOLE_0:def 5;
end;
then
A16: A c= tVG \ S;
consider yag being Vertex of G such that
A17: yag in A and
A18: yg,yag are_adjacent by A1,A2,A3,A12,Th81;
A19: yag in Ax by A17,XBOOLE_0:def 3;
set Gb1 = the inducedSubgraph of G,B\/{x}\/{y};
set Ga1 = the inducedSubgraph of G,A\/{x}\/{y};
A20: the_Vertices_of Gax = Ax by GLIB_000:def 37;
not a in S by A1,A2,Def8;
then
A21: tVG\S is non empty Subset of tVG by XBOOLE_0:def 5;
then reconsider Ga as inducedSubgraph of G,A by A16,Th29;
A22: not y in {x} by A10,TARSKI:def 1;
now
let x be object such that
A23: x in B;
not x in S by A8,A23,XBOOLE_0:def 4;
hence x in tVG \ S by A23,XBOOLE_0:def 5;
end;
then
A24: B c= tVG \ S;
then reconsider Gb as inducedSubgraph of G,B by A21,Th29;
y in xy by TARSKI:def 2;
then
A25: y in A\/xy by XBOOLE_0:def 3;
A26: ex xbg being Vertex of G st xbg in B & xg,xbg are_adjacent by A1,A2,A3,A12
,Th82;
not x in B by A24,A12,XBOOLE_0:def 5;
then x in G.AdjacentSet(the_Vertices_of Gb) by A7,A26;
then
A27: Gbx is connected by Th56;
y in xy by TARSKI:def 2;
then
A28: y in B\/xy by XBOOLE_0:def 3;
consider ybg being Vertex of G such that
A29: ybg in B and
A30: yg,ybg are_adjacent by A1,A2,A3,A12,Th82;
A31: B\/{x}\/{y} = B\/({x}\/{y}) by XBOOLE_1:4
.= B\/xy by ENUMSET1:1;
then
A32: the_Vertices_of Gb1 c= B\/xy by GLIB_000:def 37;
x in xy by TARSKI:def 2;
then x in B\/xy by XBOOLE_0:def 3;
then reconsider xb = x, yb = y as Vertex of Gb1 by A31,A28,GLIB_000:def 37;
A33: ybg in Bx by A29,XBOOLE_0:def 3;
not y in B by A24,A12,XBOOLE_0:def 5;
then not yg in the_Vertices_of Gbx by A14,A22,XBOOLE_0:def 3;
then y in G.AdjacentSet(the_Vertices_of Gbx) by A14,A30,A33;
then Gb1 is connected by A27,Th56;
then consider Wb being Walk of Gb1 such that
A34: Wb is_Walk_from yb,xb;
not x in A by A16,A12,XBOOLE_0:def 5;
then x in G.AdjacentSet(the_Vertices_of Ga) by A6,A13;
then
A35: Gax is connected by Th56;
A36: A\/{x}\/{y} = A\/({x}\/{y}) by XBOOLE_1:4
.= A\/xy by ENUMSET1:1;
then
A37: the_Vertices_of Ga1 c= A\/xy by GLIB_000:def 37;
x in xy by TARSKI:def 2;
then x in A\/xy by XBOOLE_0:def 3;
then reconsider xa = x, ya = y as Vertex of Ga1 by A36,A25,GLIB_000:def 37;
A38: not y in {x} by A10,TARSKI:def 1;
not y in A by A16,A12,XBOOLE_0:def 5;
then not yg in the_Vertices_of Gax by A20,A38,XBOOLE_0:def 3;
then y in G.AdjacentSet(the_Vertices_of Gax) by A20,A18,A19;
then Ga1 is connected by A35,Th56;
then consider Wa being Walk of Ga1 such that
A39: Wa is_Walk_from xa,ya;
A40: (A\/xy)/\(B\/xy) = A/\B\/xy by XBOOLE_1:24
.= xy by A5;
A41: Wa.last() = ya by A39;
A42: Wa.first() = xa by A39;
A43: Wb.last() = xa by A34;
A44: Wb.first() = ya by A34;
consider Pb being Path of Gb1 such that
A45: Pb is_Walk_from Wb.first(),Wb.last() and
A46: Pb is minlength by Th38;
consider Pa being Path of Ga1 such that
A47: Pa is_Walk_from Wa.first(),Wa.last() and
A48: Pa is minlength by Th38;
reconsider Pag = Pa, Pbg = Pb as Path of G by GLIB_001:175;
A49: Pbg.1 = yg by A44,A45;
Pbg.vertices() = Pb.vertices() by GLIB_001:98;
then
A50: Pbg.vertices() c= B\/xy by A32;
Pag.vertices() = Pa.vertices() by GLIB_001:98;
then Pag.vertices() c= A\/xy by A37;
then
A51: Pag.vertices() /\ Pbg.vertices() c= xy by A50,A40,XBOOLE_1:27;
set P = Pag.append(Pbg);
A52: Pag.len Pag = yg by A41,A47;
A53: Pbg.len Pbg = xg by A43,A45;
A54: Pbg.last() = Pbg.len Pbg;
then
A55: x in Pbg.vertices() by A53,GLIB_001:88;
A56: Pbg.first() = Pbg.1;
then
A57: y in Pbg.vertices() by A49,GLIB_001:88;
A58: Pbg is non trivial by A10,A56,A54,A49,A53,GLIB_001:127;
A59: Pbg is open by A10,A49,A53;
A60: not Pbg is Cycle-like by A10,A56,A54,A49,A53,GLIB_001:def 24;
A61: not xg,yg are_adjacent by A4,A11,Th44;
then
A62: Pbg.length() >= 2 by A10,A56,A54,A49,A53,Th45;
A63: Pag.1 = xg by A42,A47;
A64: Pag.edges() misses Pbg.edges()
proof
assume Pag.edges() /\ Pbg.edges() <> {};
then consider e being object such that
A65: e in Pag.edges() /\ Pbg.edges() by XBOOLE_0:def 1;
e in Pag.edges() by A65,XBOOLE_0:def 4;
then e in Pa.edges() by GLIB_001:110;
then consider
a1, a2 being Vertex of Ga1, na being odd Element of NAT such that
A66: na+2 <= len Pag and
A67: a1 = Pag.na and
e = Pag.(na+1) and
A68: a2 = Pag.(na+2) and
A69: e Joins a1, a2,Ga1 by GLIB_001:103;
A70: e Joins a1,a2,G by A69,GLIB_000:72;
e in Pbg.edges() by A65,XBOOLE_0:def 4;
then e in Pb.edges() by GLIB_001:110;
then consider
b1, b2 being Vertex of Gb1, nb being odd Element of NAT such that
nb+2 <= len Pbg and
b1 = Pbg.nb and
e = Pbg.(nb+1) and
b2 = Pbg.(nb+2) and
A71: e Joins b1, b2,Gb1 by GLIB_001:103;
A72: the_Vertices_of Gb1 = B\/xy by A31,GLIB_000:def 37;
e Joins b1,b2,G by A71,GLIB_000:72;
then
A73: a1=b1 & a2=b2 or a1=b2 & a2=b1 by A70;
then
A74: a1 in B or a1 in xy by A72,XBOOLE_0:def 3;
A75: the_Vertices_of Ga1 = A\/xy by A36,GLIB_000:def 37;
then
A76: a1 in A or a1 in xy by XBOOLE_0:def 3;
A77: a2 in A or a2 in xy by A75,XBOOLE_0:def 3;
A78: a2 in B or a2 in xy by A73,A72,XBOOLE_0:def 3;
per cases by A5,A76,A77,A74,A78,TARSKI:def 2,XBOOLE_0:def 4;
suppose
A79: a1 = x & a2 = x or a1 = y & a2 = y;
na < na+2 by XREAL_1:39;
hence contradiction by A10,A63,A52,A66,A67,A68,A79,GLIB_001:def 28;
end;
suppose
a1 = x & a2 = y or a1 = y & a2 = x;
hence contradiction by A61,A70,Def3;
end;
end;
A80: Pag.first() = Pag.1;
then
A81: x in Pag.vertices() by A63,GLIB_001:88;
A82: Pag.last() = Pag.len Pag;
then
A83: len P +1 = len Pag + len Pbg by A52,A56,A49,GLIB_001:28;
A84: Pag.length() >= 2 by A10,A61,A80,A82,A63,A52,Th45;
P.length() = Pag.length()+Pbg.length() by A82,A52,A56,A49,Th28;
then P.length() >= 2+2 by A84,A62,XREAL_1:7;
then P.length() >= 3+1;
then
A85: P.length() > 3 by NAT_1:13;
A86: Pag is open by A10,A63,A52;
A87: y in Pag.vertices() by A82,A52,GLIB_001:88;
xy c= Pag.vertices() /\ Pbg.vertices()
proof
let a be object;
assume a in xy;
then a = x or a = y by TARSKI:def 2;
hence thesis by A81,A87,A55,A57,XBOOLE_0:def 4;
end;
then Pag.vertices() /\ Pbg.vertices() = xy by A51;
then P is Cycle-like by A63,A52,A86,A49,A53,A59,A58,A64,Th27;
then P is chordal by A85,Def11;
then consider m, n being odd Nat such that
A88: m+2 < n and
A89: n <= len P and
A90: P.m <> P.n and
A91: ex e being object st e Joins P.m,P.n,G and
A92: for f being object st f in P.edges() holds not f Joins P.m,P.n,G;
A93: m < n by A88,NAT_1:12;
consider e being object such that
A94: e Joins P.m,P.n,G by A91;
A95: e Joins P.n,P.m,G by A94;
A96: m in NAT by ORDINAL1:def 12;
A97: not Pag is Cycle-like by A10,A80,A82,A63,A52,GLIB_001:def 24;
A98: 1 <= n by ABIAN:12;
A99: 1 <= m by ABIAN:12;
per cases;
suppose
A100: m < len Pag & n <= len Pag;
then n in dom Pag by A98,FINSEQ_3:25;
then
A101: P.n = Pag.n by GLIB_001:32;
m in dom Pag by A99,A100,FINSEQ_3:25;
then P.m = Pag.m by GLIB_001:32;
then Pag is chordal by A97,A88,A91,A100,A101,Th84;
then Pa is chordal by A36,Th86;
hence contradiction by A48,Th88;
end;
suppose
A102: m < len Pag & len Pag < n;
then
A103: Pag.m in the_Vertices_of Ga1 by A96,GLIB_001:7;
m in dom Pag by A99,A102,FINSEQ_3:25;
then
A104: P.m = Pag.m by GLIB_001:32;
A105: not n in dom Pag by A102,FINSEQ_3:25;
n in dom P by A89,A98,FINSEQ_3:25;
then consider n1 being Element of NAT such that
A106: n1 < len Pbg and
A107: n = len Pag + n1 by A105,GLIB_001:34;
A108: P.(len Pag +n1) = Pbg.(n1+1) by A82,A52,A56,A49,A106,GLIB_001:33;
reconsider n1 as even Element of NAT by A107;
reconsider n11 = n1+1 as odd Element of NAT;
A109: n11 <= len Pbg by A106,NAT_1:13;
then
A110: Pbg.n11 in the_Vertices_of Gb1 by GLIB_001:7;
per cases by A37,A32,A103,A110,XBOOLE_0:def 3;
suppose
A111: Pag.m in A & Pbg.n11 in xy;
per cases by A63,A52,A111,TARSKI:def 2;
suppose
A112: Pbg.n11 = Pag.1;
now
assume
A113: 1+2 >= m;
per cases by A113,XXREAL_0:1;
suppose
1+2 > m;
then 1 >= m by Th4,JORDAN12:2;
hence contradiction by A90,A99,A104,A107,A108,A112,XXREAL_0:1;
end;
suppose
A114: 1+2 = m;
then
A115: 1+1 < len Pag by A102,XXREAL_0:2;
then 1+1 in dom Pag by FINSEQ_3:25;
then
A116: Pag.(1+1) = P.(1+1) by GLIB_001:32;
1 < len Pag -1 by A115,XREAL_1:20;
then 1+0 < (len Pag -1) + len Pbg by XREAL_1:8;
then
A117: P.(1+1) in P.edges() by A83,GLIB_001:100,JORDAN12:2;
1 < len Pag by A99,A102,XXREAL_0:2;
then Pag.(1+1) Joins Pag.1,Pag.m,G by A114,GLIB_001:def 3
,JORDAN12:2;
hence contradiction by A92,A104,A107,A108,A112,A116,A117,
GLIB_000:14;
end;
end;
then Pag is chordal by A97,A95,A102,A104,A107,A108,A112,Th84,JORDAN12:2
;
then Pa is chordal by A36,Th86;
hence contradiction by A48,Th88;
end;
suppose
A118: Pbg.n11 = Pag.len Pag;
now
set L = len Pag;
assume
A119: m+2 >= len Pag;
per cases by A119,XXREAL_0:1;
suppose
A120: m+2 = L;
then
A121: L = m+1+1;
then
A122: m +1 < L by NAT_1:13;
1<=m+1 by NAT_1:12;
then m+1 in dom Pag by A122,FINSEQ_3:25;
then
A123: Pag.(m+1) = P.(m+1) by GLIB_001:32;
m < len Pag -1 by A121,NAT_1:13;
then m+0 < (len Pag -1) + len Pbg by XREAL_1:8;
then
A124: P.(m+1) in P.edges() by A83,GLIB_001:100;
m < L by A122,NAT_1:13;
then Pag.(m+1) Joins Pag.m,Pag.L,G by A96,A120,GLIB_001:def 3;
hence contradiction by A92,A104,A107,A108,A118,A123,A124;
end;
suppose
m+2 > len Pag;
hence contradiction by A102,Th4;
end;
end;
then Pag is chordal by A97,A91,A104,A107,A108,A118,Th84;
then Pa is chordal by A36,Th86;
hence contradiction by A48,Th88;
end;
end;
suppose
A125: Pag.m in A & Pbg.n11 in B;
then reconsider bc = Pb.n11 as Vertex of Gb by GLIB_000:def 37;
reconsider ac = Pa.m as Vertex of Ga by A125,GLIB_000:def 37;
set WAB = Gns.walkOf(ac,e,bc);
e Joins ac,bc,Gns by A16,A24,A94,A104,A107,A108,A125,Th19;
then
A126: WAB is_Walk_from ac,bc by GLIB_001:15;
b in B by GLIB_002:9;
then reconsider bb = b as Vertex of Gb by GLIB_000:def 37;
a in A by GLIB_002:9;
then reconsider aa = a as Vertex of Ga by GLIB_000:def 37;
consider WA being Walk of Ga such that
A127: WA is_Walk_from aa, ac by GLIB_002:def 1;
consider WB being Walk of Gb such that
A128: WB is_Walk_from bc, bb by GLIB_002:def 1;
reconsider WA, WB as Walk of Gns by GLIB_001:167;
reconsider WAs = WA, WBs = WB as Walk of Gns;
A129: WBs is_Walk_from bc, bb by A128;
set WaB = WAs.append(WAB);
set Wab = WaB.append(WBs);
WAs is_Walk_from aa, ac by A127;
then WaB is_Walk_from aa, bc by A126,GLIB_001:31;
then Wab is_Walk_from a,b by A129,GLIB_001:31;
hence contradiction by A1,A2,Def8;
end;
suppose
Pag.m in xy & Pbg.n11 in B;
then Pag.m = x or Pag.m = y by TARSKI:def 2;
then
A130: Pag.m = x by A63,A52,A96,A102,GLIB_001:def 28
.= Pbg.len Pbg by A43,A45;
now
set L = len Pbg;
assume
A131: n11+2 >= len Pbg;
per cases by A131,XXREAL_0:1;
suppose
A132: n11+2 = L;
then
A133: L = n11+1+1;
then n11 < len Pbg -1 by NAT_1:13;
then
A134: len Pag +n11 < (len Pbg -1) + len Pag by XREAL_1:6;
n11 +1 < L by A133,NAT_1:13;
then
A135: n11 < L by NAT_1:13;
then Pbg.(n11+1) Joins Pbg.n11,Pbg.L,Gb1 by A132,GLIB_001:def 3;
then Pbg.(n11+1) Joins Pbg.L,Pbg.n11,Gb1;
then
A136: Pbg.(n11+1) Joins Pbg.L,Pbg.n11,G by GLIB_000:72;
A137: 1 <= len Pag +n11 by ABIAN:12,NAT_1:12;
Pbg.(n11+1) = P.(len Pag + n11) by A82,A52,A56,A49,A135,GLIB_001:33;
then Pbg.(n11+1) in P.edges() by A83,A137,A134,GLIB_001:99;
hence contradiction by A92,A104,A107,A108,A130,A136;
end;
suppose
n11+2 > len Pbg;
then n11 >= len Pbg by Th4;
hence contradiction by A90,A104,A107,A108,A109,A130,XXREAL_0:1;
end;
end;
then Pbg is chordal by A60,A95,A104,A107,A108,A130,Th84;
then Pb is chordal by A31,Th86;
hence contradiction by A46,Th88;
end;
suppose
A138: Pag.m in xy & Pbg.n11 in xy;
then
A139: Pbg.n11 = x or Pbg.n11 = y by TARSKI:def 2;
Pag.m = x or Pag.m = y by A138,TARSKI:def 2;
then xg,yg are_adjacent by A90,A91,A104,A107,A108,A139,Def3;
hence contradiction by A4,A11,Th44;
end;
end;
suppose
A140: len Pag <= m;
then consider m1 being Nat such that
A141: m = len Pag + m1 by NAT_1:10;
n > len Pag by A93,A140,XXREAL_0:2;
then
A142: not n in dom Pag by FINSEQ_3:25;
n in dom P by A89,A98,FINSEQ_3:25;
then consider n1 being Element of NAT such that
A143: n1 < len Pbg and
A144: n = len Pag + n1 by A142,GLIB_001:34;
A145: P.(len Pag +n1) = Pbg.(n1+1) by A82,A52,A56,A49,A143,GLIB_001:33;
A146: m1 in NAT by ORDINAL1:def 12;
A147: m1 < n1 by A93,A141,A144,XREAL_1:6;
then m1 < len Pbg by A143,XXREAL_0:2;
then
A148: P.(len Pag +m1) = Pbg.(m1+1) by A82,A52,A56,A49,A146,GLIB_001:33;
reconsider n1, m1 as even Element of NAT by A141,A144,ORDINAL1:def 12;
reconsider m11 = m1+1, n11 = n1+1 as odd Element of NAT;
A149: m11 < n11 by A147,XREAL_1:6;
n11 <= len Pbg by A143,NAT_1:13;
then
A150: m11 < len Pbg by A149,XXREAL_0:2;
A151: now
assume
A152: m11+2 >= n11;
per cases by A152,XXREAL_0:1;
suppose
A153: m11+2 = n11;
then m11 +1 < len Pbg by A143;
then m11 < len Pbg -1 by XREAL_1:20;
then
A154: len Pag +m11 < (len Pbg -1) + len Pag by XREAL_1:6;
A155: 1 <= len Pag +m11 by ABIAN:12,NAT_1:12;
A156: Pbg.(m11+1) Joins Pbg.m11,Pbg.n11,G by A150,A153,GLIB_001:def 3;
Pbg.(m11+1) = P.(len Pag +m11) by A82,A52,A56,A49,A150,GLIB_001:33;
then Pbg.(m11+1) in P.edges() by A83,A155,A154,GLIB_001:99;
hence contradiction by A92,A141,A144,A145,A148,A156;
end;
suppose
m11+2 > n11;
then m11 >= n11 by Th4;
hence contradiction by A147,XREAL_1:6;
end;
end;
n11 <= len Pbg by A143,NAT_1:13;
then Pbg is chordal by A60,A91,A141,A144,A145,A148,A151,Th84;
then Pb is chordal by A31,Th86;
hence contradiction by A46,Th88;
end;
end;
:: Golumbic, page 83, Theorem 4.1 (iii)->(i)
theorem
for G being _finite _Graph st for a,b being Vertex of G st a<>b & not a
,b are_adjacent for S being VertexSeparator of a,b st S is minimal & S is non
empty for G2 being inducedSubgraph of G,S holds G2 is complete holds G is
chordal
proof
reconsider n = 2*2+1 as odd Nat;
reconsider m = 2*0+1 as odd Nat;
let G be _finite _Graph such that
A1: 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 & S is non empty for G2 being
inducedSubgraph of G,S holds G2 is complete;
let P be Walk of G such that
A2: P.length() > 3 and
A3: P is Cycle-like;
P.length() >= 3+1 by A2,NAT_1:13;
then 2*P.length() >= 2*4 by XREAL_1:64;
then 2*P.length() + 1 >= 8 + 1 by XREAL_1:7;
then
A4: len P >= 9 by GLIB_001:112;
A5: now
assume
A6: P.m = P.n;
n <= len P by A4,XXREAL_0:2;
then n=len P by A3,A6,GLIB_001:def 28;
hence contradiction by A4;
end;
per cases;
suppose
A7: ex e being object st e Joins P.m,P.n,G;
A8: m+2 < n;
len P+(-2) >= 9+(-2) by A4,XREAL_1:7;
then
A9: not (m=1 & n = len P-2);
A10: not (m=1 & n = len P) by A4;
n <= len P by A4,XXREAL_0:2;
hence thesis by A3,A7,A8,A10,A9,Th84;
end;
suppose
A11: not ex e being object st e Joins P.m,P.n,G;
reconsider Pn=P.n as Vertex of G by A4,GLIB_001:7,XXREAL_0:2;
reconsider Pm=P.m as Vertex of G by A4,GLIB_001:7,XXREAL_0:2;
set P5l=P.cut(n,len P);
consider S being VertexSeparator of Pm,Pn such that
A12: S is minimal by Th78;
set G2 = the inducedSubgraph of G,S;
A13: n <= len P by A4,XXREAL_0:2;
then P5l is_Walk_from P.n,P.(len P) by GLIB_001:37;
then
A14: P5l is_Walk_from P.n,P.m by A3,GLIB_001:118;
A15: not Pm,Pn are_adjacent by A11;
then S is VertexSeparator of Pn,Pm by A5,Th69;
then consider l being odd Nat such that
A16: 1 < l and
A17: l < len P5l and
A18: P5l.l in S by A5,A15,A14,Th71;
A19: 1+(-1) < l+(-1) by A16,XREAL_1:8;
then reconsider l2=l-1 as even Element of NAT by INT_1:3;
reconsider l2 as even Nat;
A20: l+(-1) < len P5l + (-1) by A17,XREAL_1:8;
len P5l + 5 + (-5) = len P + 1 + (-5) by A13,GLIB_001:36;
then
A21: l2+n < len P-5+n by A20,XREAL_1:8;
l+(-1) < l+0 by XREAL_1:8;
then l-1 < len P5l by A17,XXREAL_0:2;
then P5l.(l2+1) = P.(n+l2) by A13,GLIB_001:36;
then reconsider bb=P.(n+l2) as Vertex of G2 by A18,GLIB_000:def 37;
set P15=P.cut(m,n);
A22: n <= len P by A4,XXREAL_0:2;
then
A23: P15 is_Walk_from P.m,P.n by GLIB_001:37;
then S is non empty by A5,A15,Th72;
then
A24: G2 is complete by A1,A5,A15,A12;
A25: len P15 + 1 + (-1) = 5 + 1 + (-1) by A22,GLIB_001:36;
then consider k being odd Nat such that
A26: m < k and
A27: k < n and
A28: P15.k in S by A5,A15,A23,Th71;
A29: k <= 5-2 by A27,Th3;
A30: 1+2 <= k by A26,Th4;
then
A31: k = 3 by A29,XXREAL_0:1;
P15.(2+1) = P.(1+2) by A22,A25,GLIB_001:36;
then P.3 in S by A28,A30,A29,XXREAL_0:1;
then reconsider aa=P.3 as Vertex of G2 by GLIB_000:def 37;
A32: k+2+0 < k+2+l2 by A19,XREAL_1:8;
A33: n+l2 in NAT by ORDINAL1:def 12;
now
assume
A34: aa = bb;
k < n+l2 by A31,A32,XXREAL_0:2;
hence contradiction by A3,A31,A21,A33,A34,GLIB_001:def 28;
end;
then aa,bb are_adjacent by A24;
then consider e being object such that
A35: e Joins P.3,P.(n+l2),G2;
e Joins P.k,P.(n+l2),G by A31,A35,GLIB_000:72;
hence thesis by A3,A31,A21,A32,Th84;
end;
end;
:: Exercise 12, p. 101.
:: This needs "finite-branching", we do it for finite though
theorem Th99:
for G being _finite chordal _Graph, a, b being Vertex of G st a
<> b & not a,b are_adjacent for S being VertexSeparator of a,b st S is minimal
for H being removeVertices of G,S, a1 being Vertex of H st a = a1 ex c being
Vertex of G st c in H.reachableFrom(a1) & for x being Vertex of G st x in S
holds c,x are_adjacent
proof
let G be _finite chordal _Graph, a, b be Vertex of G such that
A1: a <> b and
A2: not a,b are_adjacent;
let S be VertexSeparator of a,b such that
A3: S is minimal;
let H be removeVertices of G,S, a1 be Vertex of H such that
A4: a = a1;
assume
A5: for c being Vertex of G holds not c in H.reachableFrom(a1) or ex x
being Vertex of G st x in S & not c,x are_adjacent;
per cases;
suppose
S is empty;
then not ex x being Vertex of G st x in S & not a,x are_adjacent;
hence contradiction by A4,A5,GLIB_002:9;
end;
suppose
S is non empty;
then reconsider S as non empty Subset of the_Vertices_of G;
set A = H.reachableFrom(a1);
deffunc F(set) = card (G.AdjacentSet({$1}) /\ S);
set M = { F(x) where x is Vertex of G : x in A };
A6: now
let x be object;
assume x in M;
then ex y being Vertex of G st x = card (G.AdjacentSet({y}) /\ S) & y
in A;
hence x is natural;
end;
A7: A is finite;
A8: M is finite from FRAENKEL:sch 21(A7);
a in A by A4,GLIB_002:9;
then card (G.AdjacentSet({a}) /\ S) in M;
then reconsider M as finite non empty natural-membered set by A8,A6,
MEMBERED:def 6;
set Ga = the inducedSubgraph of H,A;
A9: the_Vertices_of Ga = A by GLIB_000:def 37;
max M in M by XXREAL_2:def 8;
then consider c being Vertex of G such that
A10: max M = card (G.AdjacentSet({c}) /\ S) and
A11: c in A;
set gcs = G.AdjacentSet({c}) /\ S;
A12: A/\S = {} by A1,A2,Th74;
set Gs = the inducedSubgraph of G,S;
set tVG = the_Vertices_of G;
A13: 2*0+1 is odd;
not a in S by A1,A2,Def8;
then
A14: tVG\S is non empty Subset of tVG by XBOOLE_0:def 5;
the_Vertices_of H c= tVG;
then reconsider A as non empty Subset of tVG by XBOOLE_1:1;
now
let x be object such that
A15: x in A;
not x in S by A12,A15,XBOOLE_0:def 4;
hence x in tVG \ S by A15,XBOOLE_0:def 5;
end;
then A c= tVG \ S;
then reconsider Ga as inducedSubgraph of G,A by A14,Th29;
consider y being Vertex of G such that
A16: y in S and
A17: not c,y are_adjacent by A5,A11;
A18: not y in A by A16,A12,XBOOLE_0:def 4;
set Ay = A\/{y};
set Gay = the inducedSubgraph of G,Ay;
y in {y} by TARSKI:def 1;
then
A19: y in Ay by XBOOLE_0:def 3;
c in Ay by A11,XBOOLE_0:def 3;
then reconsider ca = c, ya = y as Vertex of Gay by A19,GLIB_000:def 37;
ex yaa being Vertex of G st yaa in A & y,yaa are_adjacent by A1,A2,A3,A4
,A16,Th81;
then y in G.AdjacentSet(the_Vertices_of Ga) by A9,A18;
then Gay is connected by Th56;
then consider Wa being Walk of Gay such that
A20: Wa is_Walk_from ca,ya;
consider P being Path of Gay such that
A21: P is_Walk_from Wa.first(),Wa.last() and
A22: P is minlength by Th38;
Wa.first() = ca by A20;
then
A23: P.first() = ca by A21;
Wa.last() = ya by A20;
then
A24: P.last() = y by A21;
c <> y by A11,A16,A12,XBOOLE_0:def 4;
then P is non trivial by A23,A24,GLIB_001:127;
then
A25: len P >= 3 by GLIB_001:125;
A26: now
assume len P < 2*2+1;
then len P <= 5-2 by Th3;
then
A27: len P = 3 by A25,XXREAL_0:1;
then 2*0+1 < len P;
then P.(1+1) Joins P.1,P.(1+2),Gay by GLIB_001:def 3;
then P.2 Joins c,y,G by A23,A24,A27,GLIB_000:72;
hence contradiction by A17;
end;
then 5 + -2 <= len P + -2 by XREAL_1:7;
then reconsider j = len P - 2*1 as odd Element of NAT by INT_1:3,XXREAL_0:2
;
set d = P.j;
A28: j < len P by XREAL_1:44;
A29: now
assume d = y;
then len P - 2 = 1 by A24,A28,GLIB_001:def 28;
then len P = 1 + 2;
hence contradiction by A26;
end;
A30: not y in G.AdjacentSet({c}) by A17,Th51;
A31: the_Vertices_of Gay = Ay by GLIB_000:def 37;
A32: P.j in the_Vertices_of Gay by A28,GLIB_001:7;
then
A33: d in A or d in {y} by A31,XBOOLE_0:def 3;
reconsider d as Vertex of G by A32;
set gds = G.AdjacentSet({d}) /\ S;
P.(j+1) Joins d,P.(len P-2+2),Gay by A28,GLIB_001:def 3;
then
A34: P.(j+1) Joins d,y,G by A24,GLIB_000:72;
then d,y are_adjacent;
then
A35: y in G.AdjacentSet({d}) by A29,Th51;
then
A36: y in G.AdjacentSet({d}) /\ S by A16,XBOOLE_0:def 4;
now
assume
A37: gcs c= gds;
not y in gcs by A30,XBOOLE_0:def 4;
then gcs c< gds by A36,A37;
then
A38: card gcs < card gds by TREES_1:6;
card gds in M by A33,A29,TARSKI:def 1;
hence contradiction by A10,A38,XXREAL_2:def 8;
end;
then consider x being object such that
A39: x in G.AdjacentSet({c}) /\ S and
A40: not x in G.AdjacentSet({d}) /\ S;
A41: x in S by A39,XBOOLE_0:def 4;
then
A42: not x in G.AdjacentSet({d}) by A40,XBOOLE_0:def 4;
reconsider x as Vertex of G by A39;
defpred Pmax[Nat] means $1 in dom P & $1 is odd & $1 < len P &
ex e being object st e Joins x,P.($1),G;
A43: for k being Nat st Pmax[k] holds k <= len P;
A44: not x in A by A12,A41,XBOOLE_0:def 4;
A45: 1 < len P by A26,XXREAL_0:2;
then
A46: 1 in dom P by FINSEQ_3:25;
x in G.AdjacentSet({c}) by A39,XBOOLE_0:def 4;
then c,x are_adjacent by Th51;
then ex e being object st e Joins x,P.1,G by A23,Def3;
then
A47: ex k being Nat st Pmax[k] by A45,A46,A13;
consider k being Nat such that
A48: Pmax[k] and
A49: for i being Nat st Pmax[i] holds k >= i from NAT_1:sch 6(A43,A47);
reconsider k as odd Element of NAT by A48;
set Q1 = P.cut(k,j);
reconsider Q=Q1 as Path of G by GLIB_001:175;
A50: k <= j by A48,Th3;
A51: j < len P by XREAL_1:44;
then
A52: Q1 is minlength by A22,A50,Th41;
A53: len Q + k = j + 1 by A50,A51,GLIB_001:36;
A54: now
let i be odd Nat such that
A55: i in dom Q and
A56: i <> 1;
1 <= i by A55,FINSEQ_3:25;
then 1+-1 <= i+-1 by XREAL_1:7;
then reconsider i1 = i-1 as even Element of NAT by INT_1:3;
reconsider ki1= k+i1 as odd Element of NAT;
A57: i+-1 < i+-0 by XREAL_1:8;
i <= len Q by A55,FINSEQ_3:25;
then
A58: i1 < len Q by A57,XXREAL_0:2;
then
A59: ki1 in dom P by A50,A51,GLIB_001:36;
A60: len P+-1 < len P+-0 by XREAL_1:8;
assume
A61: ex e being object st e Joins Q.i,x,G;
i1+k < len P - 1 - k + k by A53,A58,XREAL_1:8;
then
A62: ki1 < len P by A60,XXREAL_0:2;
A63: Q.(i1+1) = P.(ki1) by A50,A51,A58,GLIB_001:36;
now
assume i1 <> 0;
then k+0 < k + i1 by XREAL_1:8;
hence contradiction by A49,A61,A63,A59,A62,GLIB_000:14;
end;
hence contradiction by A56;
end;
set cc = Q.first(), dd = Q.last();
A64: Q1.first() = P.k by A50,A51,GLIB_001:37;
then
A65: x,cc are_adjacent by A48;
A66: x <> y by A16,A35,A40,XBOOLE_0:def 4;
then
A67: not x in {y} by TARSKI:def 1;
reconsider xs=x, ys=y as Vertex of Gs by A16,A41,GLIB_000:def 37;
Gs is complete by A1,A2,A3,Th97;
then xs,ys are_adjacent by A66;
then consider ej being object such that
A68: ej Joins xs,ys,Gs;
ej Joins x,y,G by A68,GLIB_000:72;
then
A69: x,y are_adjacent;
A70: Q1.last() = P.j by A50,A51,GLIB_001:37;
then
A71: Q.last() = P.j;
d <> x by A12,A33,A29,A41,TARSKI:def 1,XBOOLE_0:def 4;
then
A72: not d,x are_adjacent by A42,Th51;
then
A73: Q.first() <> Q.last() by A48,A64,A70,Def3;
then
A74: Q is open;
A75: Q.vertices() = Q1.vertices() by GLIB_001:98;
then dd in Q1.vertices() by GLIB_001:88;
then
A76: dd <> x by A31,A44,A67,XBOOLE_0:def 3;
A77: now
A78: 2*0+1 <= k by ABIAN:12;
then
A79: len P.cut(1,k) + 1 = k + 1 by A48,GLIB_001:36;
assume P.k = P.(len P);
then P.cut(1,k) is_Walk_from P.first(),P.last() by A48,A78,GLIB_001:37;
hence contradiction by A22,A48,A79;
end;
A80: now
let v be set such that
A81: v in Q.vertices();
consider n being odd Element of NAT such that
A82: n <= len Q and
A83: Q.n = v by A81,GLIB_001:87;
1 <= n by ABIAN:12;
then 1+-1 <= n+-1 by XREAL_1:7;
then reconsider n1 = n-1 as even Element of NAT by INT_1:3;
reconsider kn1 = k+n1 as odd Element of NAT;
A84: len P+-1 < len P+-0 by XREAL_1:8;
n+-1 < n+-0 by XREAL_1:8;
then
A85: n1 < len Q by A82,XXREAL_0:2;
then k+n1 < len P - 1 - k + k by A53,XREAL_1:8;
then
A86: kn1 < len P by A84,XXREAL_0:2;
A87: Q.(n1+1) = P.(kn1) by A50,A51,A85,GLIB_001:36;
now
A88: 1 <= k by ABIAN:12;
assume
A89: v = y;
then
A90: k+(n+-1) = 1 by A24,A83,A87,A86,GLIB_001:def 28;
A91: now
assume 1 < n;
then 1+1 <= n by NAT_1:13;
then 2+1 <= k+n by A88,XREAL_1:7;
hence contradiction by A90;
end;
1 <= n by ABIAN:12;
hence contradiction by A24,A77,A64,A83,A89,A91,XXREAL_0:1;
end;
then
A92: not v in {y} by TARSKI:def 1;
Q.vertices() c= P.vertices() by A50,A51,A75,GLIB_001:94;
then v in P.vertices() by A81;
hence v in A by A31,A92,XBOOLE_0:def 3;
end;
cc in Q1.vertices() by A75,GLIB_001:88;
then
A93: cc <> x by A31,A44,A67,XBOOLE_0:def 3;
dd,y are_adjacent by A34,A70;
then consider R being Path of G such that
A94: len R = 7 and
A95: R.length() = 3 and
A96: R.vertices() = {dd,y,x,cc} and
A97: R.1 = dd and
A98: R.3 = y and
A99: R.5 = x and
A100: R.7 = cc by A24,A29,A66,A69,A77,A64,A70,A76,A93,A65,Th47;
A101: R is non trivial by A94,GLIB_001:126;
A102: Q.edges() misses R.edges()
proof
assume not Q.edges() misses R.edges();
then Q.edges() /\ R.edges() <> {};
then consider e being object such that
A103: e in Q.edges() /\ R.edges() by XBOOLE_0:def 1;
A104: e in Q.edges() by A103,XBOOLE_0:def 4;
e in R.edges() by A103,XBOOLE_0:def 4;
then consider n being even Element of NAT such that
A105: 1 <= n and
A106: n <= 7 and
A107: R.n = e by A94,GLIB_001:99;
per cases by A105,A106,Th13;
suppose
A108: n = 2;
2*0+1 < len R by A94;
then R.(1+1) Joins R.1,R.(1+2),G by GLIB_001:def 3;
then y in Q.vertices() by A98,A104,A107,A108,GLIB_001:105;
then y in A by A80;
hence contradiction by A16,A12,XBOOLE_0:def 4;
end;
suppose
A109: n = 4;
2*1+1 < len R by A94;
then R.(3+1) Joins R.3,R.(3+2),G by GLIB_001:def 3;
then y in Q.vertices() by A98,A104,A107,A109,GLIB_001:105;
then y in A by A80;
hence contradiction by A16,A12,XBOOLE_0:def 4;
end;
suppose
A110: n = 6;
2*2+1 < len R by A94;
then R.(5+1) Joins R.5,R.(5+2),G by GLIB_001:def 3;
then x in Q.vertices() by A99,A104,A107,A110,GLIB_001:105;
then x in A by A80;
hence contradiction by A12,A41,XBOOLE_0:def 4;
end;
end;
now
let v be object such that
A111: v in {Q.first(), Q.last()};
per cases by A111,TARSKI:def 2;
suppose
A112: v = cc;
then
A113: v in Q.vertices() by GLIB_001:88;
v in R.vertices() by A94,A100,A112,GLIB_001:87;
hence v in Q.vertices() /\ R.vertices() by A113,XBOOLE_0:def 4;
end;
suppose
A114: v = dd;
2*0+1 <= len R by A94;
then
A115: v in R.vertices() by A97,A114,GLIB_001:87;
v in Q.vertices() by A114,GLIB_001:88;
hence v in Q.vertices() /\ R.vertices() by A115,XBOOLE_0:def 4;
end;
end;
then
A116: {Q.first(),Q.last()} c= Q.vertices()/\R.vertices();
now
let v be object such that
A117: v in Q.vertices() /\ R.vertices();
v in {dd,y,x,cc} by A96,A117,XBOOLE_0:def 4;
then
A118: v = dd or v = y or v = x or v = cc by ENUMSET1:def 2;
v in Q.vertices() by A117,XBOOLE_0:def 4;
then v in A by A80;
hence v in {Q.first(), Q.last()} by A16,A12,A41,A118,TARSKI:def 2
,XBOOLE_0:def 4;
end;
then Q.vertices() /\ R.vertices() c= {Q.first(), Q.last()};
then
A119: Q.vertices() /\ R.vertices() = { Q.first(), Q.last() } by A116;
A120: now
let i be odd Nat such that
A121: i in dom Q and
A122: i <> len Q;
1 <= i by A121,FINSEQ_3:25;
then 1+-1 <= i+-1 by XREAL_1:7;
then reconsider i1 = i-1 as even Element of NAT by INT_1:3;
reconsider ki1= k+i1 as odd Element of NAT;
A123: i+-1 < i+-0 by XREAL_1:8;
A124: i <= len Q by A121,FINSEQ_3:25;
then
A125: i1 < len Q by A123,XXREAL_0:2;
then ki1 in dom P by A50,A51,GLIB_001:36;
then
A126: ki1 <= len P by FINSEQ_3:25;
then
A127: P.(ki1) in Ay by A31,GLIB_001:7;
now
A128: len P - k + -1 < len P - k by XREAL_1:30;
assume ki1 = len P;
hence contradiction by A53,A124,A123,A128,XXREAL_0:2;
end;
then ki1 < len P by A126,XXREAL_0:1;
then
A129: ki1+2 <= len P by Th4;
ki1+2 <> len P by A53,A122;
then
A130: ki1+2 < len P by A129,XXREAL_0:1;
A131: P.(len P) in Ay by A31,GLIB_001:7;
assume
A132: ex e being object st e Joins Q.i,y,G;
Q.(i1+1) = P.(ki1) by A50,A51,A125,GLIB_001:36;
hence contradiction by A22,A24,A132,A130,A127,A131,Th19,Th39;
end;
A133: Q.first() = P.k by A64;
P.k <> P.j by A72,A48,Def3;
then
A134: Q is non trivial by A133,A71,GLIB_001:127;
then Q.length() <> 0;
then
A135: Q.length() >= 0+1 by NAT_1:13;
set C = Q.append(R);
A136: R.first() = dd by A97;
then
A137: C.(len Q+6) = R.(6+1) by A94,GLIB_001:33;
A138: C.(len Q+4) = R.(4+1) by A94,A136,GLIB_001:33;
A139: C.(len Q+2) = R.(2+1) by A94,A136,GLIB_001:33;
C.length() = Q.length() + 3 by A95,A136,Th28;
then C.length() >= 1 + 3 by A135,XREAL_1:7;
then
A140: C.length() > 3 by NAT_1:13;
A141: R.last() = cc by A94,A100;
then
A142: R is open by A73,A136;
then C is Cycle-like by A74,A136,A141,A101,A102,A119,Th27;
then C is chordal by A140,Def11;
then consider m, n being odd Nat such that
A143: m+2 < n and
A144: n <= len C and
C.m <> C.n and
A145: ex e being object st e Joins C.m,C.n,G and
A146: C is Cycle-like implies not (m=1 & n = len C) & not (m=1 & n =
len C-2) & not (m=3 & n = len C) by Th83;
consider e being object such that
A147: e Joins C.m,C.n,G by A145;
A148: len C +1+-1 = len Q + len R+-1 by A136,GLIB_001:28;
A149: n <= len Q or n = len Q+2 or n = len Q+4 or n = len Q+6
proof
per cases;
suppose
n <= len Q;
hence thesis;
end;
suppose
n > len Q;
then
A150: len Q +2 <= n by Th4;
per cases by A150,XXREAL_0:1;
suppose
len Q +2 = n;
hence thesis;
end;
suppose
len Q +2 < n;
then
A151: len Q +2+2 <= n by Th4;
per cases by A151,XXREAL_0:1;
suppose
len Q +4 = n;
hence thesis;
end;
suppose
len Q +2*2 < n;
then len Q +4+2 <= n by Th4;
hence thesis by A94,A148,A144,XXREAL_0:1;
end;
end;
end;
end;
A152: 1 <= m by ABIAN:12;
per cases by A149;
suppose
A153: n <= len Q;
A154: m+0 <= m+2 by XREAL_1:7;
m+2 <= len Q by A143,A153,XXREAL_0:2;
then m <= len Q by A154,XXREAL_0:2;
then m in dom Q by A152,FINSEQ_3:25;
then
A155: Q.m = C.m by GLIB_001:32;
1 <= n by ABIAN:12;
then n in dom Q by A153,FINSEQ_3:25;
then Q.n = C.n by GLIB_001:32;
hence contradiction by A52,A143,A147,A153,A155,Th40;
end;
suppose
A156: n = len Q + 2;
then m < len Q by A143,XREAL_1:6;
then
A157: m in dom Q by A152,FINSEQ_3:25;
then e Joins Q.m,y,G by A98,A139,A147,A156,GLIB_001:32;
hence contradiction by A120,A143,A156,A157;
end;
suppose
A158: n = len Q + 4;
then m+2+2 <= len Q+4 by A143,Th4;
then m+4 <= len Q +4;
then m <= len Q by XREAL_1:6;
then
A159: m in dom Q by A152,FINSEQ_3:25;
then
A160: e Joins Q.m,x,G by A99,A138,A147,A158,GLIB_001:32;
per cases by A152,XXREAL_0:1;
suppose
1 = m;
hence contradiction by A74,A94,A136,A141,A101,A142,A102,A119,A148,A146
,A158,Th27;
end;
suppose
1 < m;
hence contradiction by A54,A159,A160;
end;
end;
suppose
A161: n = len Q +6;
then m+2+2 <= len Q+6 by A143,Th4;
then m+4 <= len Q +2+4;
then
A162: m <= len Q +2 by XREAL_1:6;
per cases by A162,XXREAL_0:1;
suppose
A163: m < len Q +2;
now
assume 1+2 >= m;
then m< 2*1+1 by A74,A94,A136,A141,A101,A142,A102,A119,A148,A146,A161
,Th27,XXREAL_0:1;
then m <= 3-2 by Th3;
then m < 1 by A74,A94,A136,A141,A101,A142,A102,A119,A148,A146,A161
,Th27,XXREAL_0:1;
hence contradiction by ABIAN:12;
end;
then
A164: 2*0+1+2 < m;
A165: m <= len Q by A163,Th4;
then m in dom Q by A152,FINSEQ_3:25;
then C.m = Q.m by GLIB_001:32;
hence contradiction by A52,A100,A137,A147,A161,A165,A164,Th40,
GLIB_000:14;
end;
suppose
A166: m = len Q + 2;
3 <= len Q by A134,GLIB_001:125;
then 1 <= len Q by XXREAL_0:2;
then
A167: 2*0+1 in dom Q by FINSEQ_3:25;
1 <> len Q by A72,A48,A64,A70,Def3;
hence contradiction by A120,A98,A100,A137,A139,A147,A161,A166,A167,
GLIB_000:14;
end;
end;
end;
end;
theorem
for G being _finite chordal _Graph, a, b being Vertex of G st a <> b &
not a,b are_adjacent for S being VertexSeparator of a,b st S is minimal for H
being removeVertices of G,S, a1 being Vertex of H st a = a1 for x, y being
Vertex of G st x in S & y in S holds ex c being Vertex of G st c in H
.reachableFrom(a1) & c,x are_adjacent & c,y are_adjacent
proof
let G be _finite chordal _Graph;
let a,b be Vertex of G such that
A1: a <> b and
A2: not a,b are_adjacent;
let S be VertexSeparator of a,b such that
A3: S is minimal;
let H be removeVertices of G,S, a1 be Vertex of H;
assume a = a1;
then consider c being Vertex of G such that
A4: c in H.reachableFrom(a1) and
A5: for x being Vertex of G st x in S holds c,x are_adjacent by A1,A2,A3,Th99;
let x,y be Vertex of G such that
A6: x in S and
A7: y in S;
A8: c,y are_adjacent by A7,A5;
c,x are_adjacent by A6,A5;
hence thesis by A4,A8;
end;
:: Golumbic, page 83, Lemma 4.2.
theorem Th101:
for G being non _trivial _finite chordal _Graph st not G is
complete ex a,b being Vertex of G st a<>b & not a,b are_adjacent & a is
simplicial & b is simplicial
proof
defpred P[_finite _Graph] means $1 is non _trivial & $1 is chordal &
not $1 is
complete implies ex a,b being Vertex of $1 st a <> b & not a,b are_adjacent & a
is simplicial & b is simplicial;
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
let k be non zero Nat such that
A2: for Gk being _finite _Graph st Gk.order() < k holds P[Gk];
let Gk1 be _finite _Graph such that
A3: Gk1.order() = k and
A4: Gk1 is non _trivial and
A5: Gk1 is chordal and
A6: not Gk1 is complete;
reconsider G=Gk1 as non _trivial _finite chordal _Graph by A4,A5;
consider a,b being Vertex of G such that
A7: a <> b and
A8: not a,b are_adjacent by A6;
consider S being VertexSeparator of a,b such that
A9: S is minimal by Th78;
set Gns = the removeVertices of G,S;
reconsider sa = a, sb = b as Vertex of Gns by A7,A8,Th76;
set A = Gns.reachableFrom(sa), B = Gns.reachableFrom(sb);
set Gas = the inducedSubgraph of G,(A \/ S);
A10: A c= the_Vertices_of Gns;
then
A11: A c= the_Vertices_of G by XBOOLE_1:1;
then
A12: A\/S is non empty Subset of the_Vertices_of G by XBOOLE_1:8;
A13: A /\ B = {} by A7,A8,Th75;
A14: now
assume
A15: b in A \/ S;
not b in S by A7,A8,Def8;
then
A16: b in A by A15,XBOOLE_0:def 3;
b in B by GLIB_002:9;
hence contradiction by A13,A16,XBOOLE_0:def 4;
end;
A17: now
assume Gas.order() = k;
then
A18: the_Vertices_of Gas = the_Vertices_of G by A3,CARD_2:102;
the_Vertices_of Gas = A\/S by A12,GLIB_000:def 37;
hence contradiction by A14,A18;
end;
set Gbs = the inducedSubgraph of G,(B \/ S);
A19: B c= the_Vertices_of G by A10,XBOOLE_1:1;
then
A20: B\/S is non empty Subset of the_Vertices_of G by XBOOLE_1:8;
A21: now
assume
A22: a in B \/ S;
not a in S by A7,A8,Def8;
then
A23: a in B by A22,XBOOLE_0:def 3;
a in A by GLIB_002:9;
hence contradiction by A13,A23,XBOOLE_0:def 4;
end;
A24: now
assume Gbs.order() = k;
then
A25: the_Vertices_of Gbs = the_Vertices_of G by A3,CARD_2:102;
the_Vertices_of Gbs = B\/S by A20,GLIB_000:def 37;
hence contradiction by A21,A25;
end;
set Gs = the inducedSubgraph of G,S;
not a in S by A7,A8,Def8;
then a in the_Vertices_of G \ S by XBOOLE_0:def 5;
then
A26: the_Vertices_of Gns = the_Vertices_of G \ S by GLIB_000:def 37;
Gbs.order() <= k by A3,GLIB_000:75;
then
A27: Gbs.order() < k by A24,XXREAL_0:1;
ex b being Vertex of Gk1 st b in B & b is simplicial
proof
consider aa being object such that
A28: aa in B by XBOOLE_0:def 1;
A29: the_Vertices_of Gbs = B \/ S by A20,GLIB_000:def 37;
then reconsider a = aa as Vertex of Gbs by A28,XBOOLE_0:def 3;
ex c being Vertex of Gbs st c in B & c is simplicial
proof
per cases;
suppose
Gbs is complete;
then a is simplicial by Th63;
hence thesis by A28;
end;
suppose
A30: not Gbs is complete;
then not Gbs is _trivial;
then consider a2,b2 being Vertex of Gbs such that
A31: a2 <> b2 and
A32: not a2,b2 are_adjacent and
A33: a2 is simplicial and
A34: b2 is simplicial by A2,A27,A30;
now
assume that
A35: a2 in S and
A36: b2 in S;
reconsider a4 = a2, b4 = b2 as Vertex of Gs by A35,A36,
GLIB_000:def 37;
Gs is complete by A7,A8,A9,A35,Th97;
then
A37: a4,b4 are_adjacent by A31;
reconsider a3 = a2, b3 = b2 as Vertex of G by A35,A36;
not a3,b3 are_adjacent by A20,A32,Th44;
hence contradiction by A35,A37,Th44;
end;
then b2 in B or a2 in B by A29,XBOOLE_0:def 3;
hence thesis by A33,A34;
end;
end;
then consider cc being Vertex of Gbs such that
A38: cc in B and
A39: cc is simplicial;
reconsider c = cc as Vertex of Gk1 by A19,A38;
now
let x be object such that
A40: x in Gk1.AdjacentSet({c});
assume
A41: not x in B\/S;
then
A42: not x in B by XBOOLE_0:def 3;
A43: not x in S by A41,XBOOLE_0:def 3;
reconsider x as Vertex of Gk1 by A40;
c,x are_adjacent by A40,Th51;
then consider e being object such that
A44: e Joins c,x,Gk1;
x in the_Vertices_of Gns by A26,A43,XBOOLE_0:def 5;
then e Joins c,x,Gns by A26,A38,A44,Th19;
hence contradiction by A38,A42,GLIB_002:10;
end;
then
A45: Gk1.AdjacentSet({c}) c= B\/S;
c in B\/S by A38,XBOOLE_0:def 3;
then c is simplicial by A20,A39,A45,Th66;
hence thesis by A38;
end;
then consider b being Vertex of Gk1 such that
A46: b in B and
A47: b is simplicial;
Gas.order() <= k by A3,GLIB_000:75;
then
A48: Gas.order() < k by A17,XXREAL_0:1;
ex a being Vertex of Gk1 st a in A & a is simplicial
proof
consider aa being object such that
A49: aa in A by XBOOLE_0:def 1;
A50: the_Vertices_of Gas = A \/ S by A12,GLIB_000:def 37;
then reconsider a = aa as Vertex of Gas by A49,XBOOLE_0:def 3;
ex c being Vertex of Gas st c in A & c is simplicial
proof
per cases;
suppose
Gas is complete;
then a is simplicial by Th63;
hence thesis by A49;
end;
suppose
A51: not Gas is complete;
then not Gas is _trivial;
then consider a2,b2 being Vertex of Gas such that
A52: a2 <> b2 and
A53: not a2,b2 are_adjacent and
A54: a2 is simplicial and
A55: b2 is simplicial by A2,A48,A51;
now
assume that
A56: a2 in S and
A57: b2 in S;
reconsider a4 = a2, b4 = b2 as Vertex of Gs by A56,A57,
GLIB_000:def 37;
Gs is complete by A7,A8,A9,A56,Th97;
then
A58: a4,b4 are_adjacent by A52;
reconsider a3 = a2, b3 = b2 as Vertex of G by A56,A57;
not a3,b3 are_adjacent by A12,A53,Th44;
hence contradiction by A56,A58,Th44;
end;
then b2 in A or a2 in A by A50,XBOOLE_0:def 3;
hence thesis by A54,A55;
end;
end;
then consider cc being Vertex of Gas such that
A59: cc in A and
A60: cc is simplicial;
reconsider c = cc as Vertex of Gk1 by A11,A59;
now
let x be object such that
A61: x in Gk1.AdjacentSet({c});
assume
A62: not x in A\/S;
then
A63: not x in A by XBOOLE_0:def 3;
A64: not x in S by A62,XBOOLE_0:def 3;
reconsider x as Vertex of Gk1 by A61;
c,x are_adjacent by A61,Th51;
then consider e being object such that
A65: e Joins c,x,Gk1;
x in the_Vertices_of Gns by A26,A64,XBOOLE_0:def 5;
then e Joins c,x,Gns by A26,A59,A65,Th19;
hence contradiction by A59,A63,GLIB_002:10;
end;
then
A66: Gk1.AdjacentSet({c}) c= A\/S;
c in A\/S by A59,XBOOLE_0:def 3;
then c is simplicial by A12,A60,A66,Th66;
hence thesis by A59;
end;
then consider a being Vertex of Gk1 such that
A67: a in A and
A68: a is simplicial;
A69: now
reconsider aa=a, bb=b as Vertex of Gns by A67,A46;
assume a,b are_adjacent;
then consider e being object such that
A70: e Joins a,b,Gk1;
e Joins aa,bb,Gns by A26,A70,Th19;
then bb in A by A67,GLIB_002:10;
hence contradiction by A13,A46,XBOOLE_0:def 4;
end;
a<>b by A13,A67,A46,XBOOLE_0:def 4;
hence thesis by A68,A47,A69;
end;
A71: for G being _finite _Graph holds P[G] from FinGraphOrderCompInd(A1);
let G be non _trivial _finite chordal _Graph;
assume not G is complete;
hence thesis by A71;
end;
theorem Th102:
for G being _finite chordal _Graph ex v being Vertex of G st v is simplicial
proof
let G be _finite chordal _Graph;
per cases;
suppose
A1: G is complete;
set u = the Vertex of G;
u is simplicial by A1,Th63;
hence thesis;
end;
suppose
A2: not G is complete;
then not G is _trivial;
then ex a,b being Vertex of G st a<>b &( not a,b are_adjacent) & a is
simplicial & b is simplicial by A2,Th101;
hence thesis;
end;
end;
begin :: Vertex Elimination Scheme :: Golumbic, p. 82
definition
let G be _finite _Graph;
mode VertexScheme of G -> FinSequence of the_Vertices_of G means
: Def12:
it is one-to-one & rng it = the_Vertices_of G;
existence
proof
consider p being FinSequence such that
A1: rng p = the_Vertices_of G and
A2: p is one-to-one by FINSEQ_4:58;
reconsider p as FinSequence of the_Vertices_of G by A1,FINSEQ_1:def 4;
take p;
thus thesis by A1,A2;
end;
end;
registration
let G be _finite _Graph;
cluster -> non empty for VertexScheme of G;
correctness by Def12,RELAT_1:38;
end;
theorem
for G being _finite _Graph, S being VertexScheme of G holds len S =
card the_Vertices_of G
proof
let G be _finite _Graph, S be VertexScheme of G;
A1: S is one-to-one by Def12;
rng S = the_Vertices_of G by Def12;
hence thesis by A1,FINSEQ_4:62;
end;
theorem
for G being _finite _Graph, S being VertexScheme of G holds 1 <= len S
by NAT_1:14;
theorem Th105:
for G, H being _finite _Graph, g being VertexScheme of G st G ==
H holds g is VertexScheme of H
proof
let G,H be _finite _Graph, g be VertexScheme of G such that
A1: G == H;
rng g = the_Vertices_of G by Def12;
then
A2: rng g = the_Vertices_of H by A1;
A3: g is one-to-one by Def12;
g is FinSequence of the_Vertices_of H by A1;
hence thesis by A3,A2,Def12;
end;
definition
let G be _finite _Graph, S be VertexScheme of G, x be Vertex of G;
redefine func x..S -> non zero Element of NAT; :: redefines .. (FINSEQ_4, definition)
correctness
proof
rng S = the_Vertices_of G by Def12;
hence thesis by FINSEQ_4:21;
end;
end;
definition
let G be _finite _Graph, S be VertexScheme of G, n be Nat;
redefine func S.followSet(n) -> Subset of the_Vertices_of G; :: redefines .followSet (CHORD, definition)
coherence
proof
A1: rng (n,len S)-cut S c= rng S by FINSEQ_6:137;
now
let x be object;
assume x in S.followSet(n);
then x in rng S by A1;
hence x in the_Vertices_of G by Def12;
end;
hence thesis by TARSKI:def 3;
end;
end;
theorem Th106: :: NeVSchFol:
for G being _finite _Graph, S being VertexScheme of G, n being
non zero Nat st n <= len S holds S.followSet(n) is non empty
proof
let G be _finite _Graph, S be VertexScheme of G;
let n be non zero Nat such that
A1: n <= len S;
0+1 <= n by NAT_1:13;
then
A2: len ((n, len S)-cut S) + n = len S + 1 by A1,FINSEQ_6:def 4;
len S + 1 - n <> 0 by A1,NAT_1:13;
then (n, len S)-cut S <> {} by A2;
hence thesis;
end;
definition
let G be _finite _Graph, S be VertexScheme of G;
attr S is perfect means
:Def13:
for n being non zero Nat st n <=
len S for Gf being inducedSubgraph of G,S.followSet(n) for v being Vertex of Gf
st v = S.n holds v is simplicial;
end;
:: finite is needed unless we add loopless
theorem Th107:
for G being _finite _trivial _Graph, v being Vertex of G
ex S being VertexScheme of G st S = <*v*> & S is perfect
proof
let G be _finite _trivial _Graph, v being Vertex of G;
consider v1 being Vertex of G such that
A1: the_Vertices_of G = {v1} by GLIB_000:22;
set S = <*v*>;
v1 = v by A1,TARSKI:def 1;
then
A2: rng S = the_Vertices_of G by A1,FINSEQ_1:39;
S is one-to-one by FINSEQ_3:93;
then reconsider S as VertexScheme of G by A2,Def12;
take S;
thus S = <*v*>;
let n be non zero Nat such that
n <= len S;
let Gf be inducedSubgraph of G,S.followSet(n);
thus thesis;
end;
theorem
for G being _finite _Graph, V being VertexScheme of G holds
V is perfect iff
for a,b,c being Vertex of G st b<>c & a,b are_adjacent &
a,c are_adjacent
for va,vb,vc being Nat st va in dom V & vb in dom V & vc in dom V &
V.va = a & V.vb = b & V.vc = c & va < vb & va < vc holds
b,c are_adjacent
proof
let G be _finite _Graph, V be VertexScheme of G;
A1: V is one-to-one by Def12;
A2: now
let a,b,c be Vertex of G such that
A3: b<>c and
A4: a,b are_adjacent and
A5: a,c are_adjacent and
A6: not b,c are_adjacent;
let va,vb,vc be Nat such that
A7: va in dom V and
A8: vb in dom V and
A9: vc in dom V and
A10: V.va=a and
A11: V.vb=b and
A12: V.vc=c and
A13: va < vb and
A14: va < vc;
set Gf = the inducedSubgraph of G,V.followSet(va);
set fs = (va,len V)-cut V;
A15: va <= len V by A7,FINSEQ_3:25;
then
A16: va - va <= len V - va by XREAL_1:9;
A17: 1 <= va by A7,FINSEQ_3:25;
then
A18: len fs + va - va = len V + 1 - va by A15,FINSEQ_6:def 4;
then
A19: len fs = len V - va + 1;
then 0+1 <= len fs by A16,NAT_1:13;
then
A20: 0+1 in dom fs by FINSEQ_3:25;
fs.(0+1) = V.(va + 0) by A17,A15,A19,A16,FINSEQ_6:def 4;
then a in V.followSet(va) by A10,A20,FUNCT_1:3;
then reconsider ag=a as Vertex of Gf by GLIB_000:def 37;
consider jc being Nat such that
A21: va + jc = vc by A14,NAT_1:10;
A22: 0+1 <= jc+1 by XREAL_1:7;
A23: now
assume jc >= len fs;
then va + jc >= len V + 1 - va + va by A18,XREAL_1:7;
then vc > len V by A21,NAT_1:13;
hence contradiction by A9,FINSEQ_3:25;
end;
then jc+1 <= len fs by NAT_1:13;
then
A24: jc+1 in dom fs by A22,FINSEQ_3:25;
fs.(jc+1) = V.(va + jc) by A17,A15,A23,FINSEQ_6:def 4;
then c in V.followSet(va) by A12,A21,A24,FUNCT_1:3;
then reconsider cg=c as Vertex of Gf by GLIB_000:def 37;
A25: V.followSet(va) is non empty by A17,A15,Th106;
then
A26: ag,cg are_adjacent by A5,Th44;
consider jb being Nat such that
A27: va + jb = vb by A13,NAT_1:10;
A28: 0+1 <= jb+1 by XREAL_1:7;
A29: now
assume jb >= len fs;
then va + jb >= len V + 1 - va + va by A18,XREAL_1:7;
then vb > len V by A27,NAT_1:13;
hence contradiction by A8,FINSEQ_3:25;
end;
then jb+1 <= len fs by NAT_1:13;
then
A30: jb+1 in dom fs by A28,FINSEQ_3:25;
fs.(jb+1) = V.(va + jb) by A17,A15,A29,FINSEQ_6:def 4;
then b in V.followSet(va) by A11,A27,A30,FUNCT_1:3;
then reconsider bg=b as Vertex of Gf by GLIB_000:def 37;
A31: not bg,cg are_adjacent by A6,A25,Th44;
assume V is perfect;
then
A32: ag is simplicial by A10,A17,A15;
a <> c by A1,A7,A9,A10,A12,A14,FUNCT_1:def 4;
then
A33: cg in Gf.AdjacentSet({ag}) by A26,Th51;
ag,bg are_adjacent by A4,A25,Th44;
then bg in Gf.AdjacentSet({ag}) by A26,A31,Th51;
then ex e being object st e Joins bg,cg,Gf by A3,A32,A33,Th67;
hence contradiction by A31;
end;
A34: rng V = the_Vertices_of G by Def12;
now
assume not V is perfect;
then not (for n being non zero Nat st n <= len V for Gf being
inducedSubgraph of G,V.followSet(n) for v being Vertex of Gf st v = V.n holds v
is simplicial);
then consider
n being non zero Nat, Gf being (inducedSubgraph of G,V.followSet(
n)), v being Vertex of Gf such that
A35: n <= len V and
A36: v = V.n and
A37: not v is simplicial;
A38: V.followSet(n) is non empty Subset of the_Vertices_of G by A35,Th106;
then
A39: the_Vertices_of Gf = V.followSet(n) by GLIB_000:def 37;
then reconsider vg=v as Vertex of G by TARSKI:def 3;
consider a,b being Vertex of Gf such that
A40: a<>b and
A41: v<>a and
A42: v<>b and
A43: v,a are_adjacent and
A44: v,b are_adjacent and
A45: not a,b are_adjacent by A37,Th68;
reconsider ag=a, bg=b as Vertex of G by A39,TARSKI:def 3;
A46: vg,bg are_adjacent by A44,A38,Th44;
1 <= n by Th1;
then
A47: n in dom V by A35,FINSEQ_3:25;
b in the_Vertices_of G by A39,TARSKI:def 3;
then consider vb being Nat such that
A48: vb in dom V and
A49: V.vb = b by A34,FINSEQ_2:10;
A50: b in rng V by A34,A39,TARSKI:def 3;
A51: now
assume vb <= n;
then
A52: vb < n by A36,A42,A49,XXREAL_0:1;
b..V >= n by A1,A47,A39,A50,Th16;
then vb < b..V by A52,XXREAL_0:2;
hence contradiction by A48,A49,FINSEQ_4:24;
end;
a in the_Vertices_of G by A39,TARSKI:def 3;
then consider va being Nat such that
A53: va in dom V and
A54: V.va = a by A34,FINSEQ_2:10;
A55: a in rng V by A34,A39,TARSKI:def 3;
A56: now
assume va <= n;
then
A57: va < n by A36,A41,A54,XXREAL_0:1;
a..V >= n by A1,A47,A39,A55,Th16;
then va < a..V by A57,XXREAL_0:2;
hence contradiction by A53,A54,FINSEQ_4:24;
end;
A58: not ag,bg are_adjacent by A45,A38,Th44;
vg,ag are_adjacent by A43,A38,Th44;
hence ex a,b,c being Vertex of G, va,vb,vc being Nat st b<>c & a,b
are_adjacent & a,c are_adjacent & 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 & not b,c are_adjacent by A36
,A47,A40,A46,A58,A53,A54,A48,A49,A56,A51;
end;
hence thesis by A2;
end;
:: Golumbic pg 83-84, Theorem 4.1 (i) ==> (ii)
registration
let G be _finite chordal _Graph;
cluster perfect for VertexScheme of G;
existence
proof
defpred P[_finite _Graph] means $1 is chordal implies ex S being
VertexScheme of $1 st S is perfect;
A1: now
let k be non zero Nat such that
A2: for Gk being _finite _Graph st Gk.order() < k holds P[Gk];
let Gk1 be _finite _Graph such that
A3: Gk1.order() = k;
thus P[Gk1]
proof
assume
A4: Gk1 is chordal;
per cases;
suppose
A5: k = 1;
set v = the Vertex of Gk1;
Gk1 is _trivial by A3,A5;
then
ex S being VertexScheme of Gk1 st S = <*v*> & S is perfect by Th107;
hence thesis;
end;
suppose
k <> 1;
then reconsider G=Gk1 as non _trivial _finite chordal _Graph
by A3,A4,GLIB_000:26;
consider x being Vertex of G such that
A6: x is simplicial by Th102;
set H = the removeVertex of G,x;
A7: <*x*> is one-to-one by FINSEQ_3:93;
A8: the_Vertices_of G\{x} is non empty by GLIB_000:20;
then
A9: the_Vertices_of H=the_Vertices_of G\{x} by GLIB_000:def 37;
H.order() = card (the_Vertices_of G\{x}) by A8,GLIB_000:def 37
.= G.order() - card {x} by CARD_2:44
.= k - 1 by A3,CARD_2:42;
then consider T being VertexScheme of H such that
A10: T is perfect by A2,XREAL_1:146;
{x} /\ rng T = {x} /\ (the_Vertices_of G\{x}) by A9,Def12
.= ({x} /\ the_Vertices_of G) \ {x} by XBOOLE_1:49
.= {x} \ {x} by XBOOLE_1:28
.= {} by XBOOLE_1:37;
then {x} misses rng T;
then
A11: rng <*x*> misses rng T by FINSEQ_1:38;
set S = <*x*>^T;
rng T = the_Vertices_of G\{x} by A9,Def12;
then rng S = the_Vertices_of G\{x} \/ rng <*x*> by FINSEQ_1:31;
then rng S = the_Vertices_of G\{x} \/ {x} by FINSEQ_1:38;
then rng S = {x} \/ the_Vertices_of G by XBOOLE_1:39;
then
A12: rng S = the_Vertices_of G by XBOOLE_1:12;
then reconsider S as FinSequence of the_Vertices_of G by
FINSEQ_1:def 4;
T is one-to-one by Def12;
then S is one-to-one by A11,A7,FINSEQ_3:91;
then reconsider S as VertexScheme of Gk1 by A12,Def12;
take S;
let n be non zero Nat such that
A13: n <= len S;
A14: 1 <= n by NAT_1:14;
let Gf be inducedSubgraph of Gk1,S.followSet(n);
let v be Vertex of Gf such that
A15: v = S.n;
per cases by A14,XXREAL_0:1;
suppose
A16: 1 = n;
then
A17: S.followSet(n) = rng S by FINSEQ_6:133
.= the_Vertices_of G by Def12;
x = v by A15,A16,FINSEQ_1:41;
hence thesis by A6,A17,Th65,GLIB_000:94;
end;
suppose
A18: 1 < n;
then 1+(-1) < n+(-1) by XREAL_1:8;
then reconsider n1 = n - 1 as non zero Element of NAT by INT_1:3;
len <*x*> = 1 by FINSEQ_1:39;
then
A19: S.n = T.n1 by A13,A18,FINSEQ_1:24;
A20: T.followSet(n1) = S.followSet(n1+1) by Th17;
n+(-1) <= len S+(-1) by A13,XREAL_1:7;
then n1 <= len <*x*> + len T + (-1) by FINSEQ_1:22;
then
A21: n1 <= 1 + len T + (-1) by FINSEQ_1:39;
then T.followSet(n1) is non empty by Th106;
then Gf is inducedSubgraph of H,T.followSet(n1) by A9,A20,Th30;
hence thesis by A10,A15,A19,A21;
end;
end;
end;
end;
for G being _finite _Graph holds P[G] from FinGraphOrderCompInd(A1 );
then consider S being VertexScheme of G such that
A22: S is perfect;
take S;
thus thesis by A22;
end;
end;
theorem
for G, H being _finite chordal _Graph,
g being perfect VertexScheme of G st G == H holds
g is perfect VertexScheme of H
proof
let G,H be _finite chordal _Graph, g be perfect VertexScheme of G such that
A1: G == H;
reconsider h=g as VertexScheme of H by A1,Th105;
now
let n be non zero Nat such that
A2: n <= len h;
let Hf be inducedSubgraph of H,h.followSet(n);
let vh be Vertex of Hf such that
A3: vh = h.n;
G.edgesBetween(g.followSet(n)) = H.edgesBetween(g.followSet(n)) by A1,
GLIB_000:90;
then reconsider Gf = Hf as inducedSubgraph of G,g.followSet(n) by A1,
GLIB_000:95;
reconsider vg = vh as Vertex of Gf;
vg is simplicial by A2,A3,Def13;
hence vh is simplicial;
end;
hence thesis by Def13;
end;
:: Chordal41c:
:: Golumbic pg 83-84, Theorem 4.1 (ii) ==> (i)
theorem
for G being _finite _Graph st
ex S being VertexScheme of G st S is perfect holds
G is chordal
proof
let G be _finite _Graph;
given S being VertexScheme of G such that
A1: S is perfect;
A2: rng S = the_Vertices_of G by Def12;
let P be Walk of G such that
A3: P.length() > 3 and
A4: P is Cycle-like;
P.vertices() is non empty by GLIB_001:88;
then consider x being set such that
A5: x in P.vertices() and
A6: for y being set st y in P.vertices() holds x..S <= y..S by A2,Th15;
reconsider x as Vertex of G by A5;
set n = x..S;
set H = the inducedSubgraph of G,S.followSet(n);
A7: rng S = the_Vertices_of G by Def12;
then
A8: n in dom S by FINSEQ_4:20;
A9: S is one-to-one by Def12;
then x in S.followSet(n) by A7,A8,Th16;
then reconsider y=x as Vertex of H by GLIB_000:def 37;
A10: S.followSet(n) is non empty by A7,Th106,FINSEQ_4:21;
now
let y be object such that
A11: y in P.vertices();
reconsider z=y as Vertex of G by A11;
x..S <= z..S by A6,A11;
hence y in S.followSet(n) by A7,A8,A9,Th16;
end;
then P.vertices() c= S.followSet(n);
then reconsider C=P as Walk of H by A10,Th23;
reconsider C as Path of H by A4,GLIB_001:176;
A12: C is closed by A4,GLIB_001:176;
A13: y in C.vertices() by A5,GLIB_001:98;
A14: rng S = the_Vertices_of G by Def12;
then
A15: S.n = x by FINSEQ_4:19;
C is non trivial by A4;
then
A16: C is Cycle-like by A12;
C.length() > 3 by A3,GLIB_001:114;
then consider a,b being odd Nat such that
A17: a+2 < b and
A18: b <= len C and
A19: C.a <> C.b and
A20: C.a in H.AdjacentSet({y}) and
A21: C.b in H.AdjacentSet({y}) and
A22: for e being object st e in C.edges() holds not e Joins C.a,C.b,H
by A16,A13,Th54;
n <= len S by A14,FINSEQ_4:21;
then y is simplicial by A1,A15;
then ex e being object st e Joins C.a,C.b,H by A19,A20,A21,Th67;
then C is chordal by A17,A18,A19,A22;
hence thesis by A10,Th86;
end;
:: added by SK, 8.12.2024
registration
let G be _Graph;
cluster open Path-like -> vertex-distinct for Walk of G;
coherence by Th32;
end;
:: into CHORD ?
registration
let G be _Graph, W be vertex-distinct Walk of G;
cluster W.reverse() -> vertex-distinct;
coherence
proof
now
let m,n be odd Element of NAT;
assume A1: m <= len(W.reverse()) & n <= len(W.reverse());
1 <= m & 1 <= n by Th2;
then A2: m in dom W.reverse() & n in dom W.reverse() by A1, FINSEQ_3:25;
assume A3: W.reverse().m = W.reverse().n;
A4: len W - m + 1 in dom W by A2, GLIB_001:25;
then reconsider m9 = len W - m + 1 as odd Element of NAT;
A5: m9 <= len W by A4, FINSEQ_3:25;
A6: len W - n + 1 in dom W by A2, GLIB_001:25;
then reconsider n9 = len W - n + 1 as odd Element of NAT;
A7: n9 <= len W by A6, FINSEQ_3:25;
W.m9 = W.reverse().m by A2, GLIB_001:25
.= W.n9 by A2, A3, GLIB_001:25;
then m9 = n9 by A5, A7, GLIB_001:def 29;
hence m = n;
end;
hence thesis;
end;
cluster W.vertexSeq() -> one-to-one;
coherence
proof
set f = W.vertexSeq();
now
let x1,x2 be object;
assume A8: x1 in dom f & x2 in dom f & f.x1 = f.x2;
then reconsider n = x1, m = x2 as Nat;
A9: 1 <= n & n <= len f & 1 <= m & m <= len f by A8, FINSEQ_3:25;
A10: W.(2*n-1) = f.x1 by A9, GLIB_001:def 14
.= W.(2*m-1) by A8, A9, GLIB_001:def 14;
2*1 <= 2*n & 2*1 <= 2*m by A9, XREAL_1:64;
then 2-1 <= 2*n-1 & 2-1 <= 2*m-1 by XREAL_1:9;
then 2*n-'1 = 2*n-1 & 2*m-'1 = 2*m-1 by NAT_D:39;
then A11: 2*n-1 is odd Element of NAT & 2*m-1 is odd Element of NAT;
2*n <= 2*len f & 2*m <= 2*len f by A9, XREAL_1:64;
then 2*n <= len W + 1 & 2*m <= len W + 1 by GLIB_001:def 14;
then 2*n-1 <= len W +1-1 & 2*m-1 <= len W +1-1 by XREAL_1:9;
then 2*n-1 = 2*m-1 by A10, A11, GLIB_001:def 29;
hence x1 = x2;
end;
hence thesis by FUNCT_1:def 4;
end;
end;
::: into CHORD
theorem
for G being _Graph, T being Trail of G
for n being odd Element of NAT st 1 < n & n < len T
ex v being Vertex of G st v = T.n & T.(n-1) <> T.(n+1) &
{T.(n-1),T.(n+1)} c= v.edgesInOut() & 2 c= v.degree()
proof
let G be _Graph, T be Trail of G, n9 be odd Element of NAT;
assume A1: 1 < n9 & n9 < len T;
reconsider n = n9 as odd Nat;
consider m being odd Nat such that
A2: m+2 = n by A1, Th5;
reconsider m as odd Element of NAT by ORDINAL1:def 12;
A4: T.(n+1) Joins T.n,T.(n+2),G by A1, GLIB_001:def 3;
A5: m+2-2 < n-0 by A2, XREAL_1:15;
then m < len T by A1, XXREAL_0:2;
then A7: T.(m+1) Joins T.n,T.m,G by A2, GLIB_001:def 3, GLIB_000:14;
then reconsider v = T.n as Vertex of G by GLIB_000:13;
take v;
thus v = T.n9;
A8: n+1 <= len T by A1, NAT_1:13;
A9: 0+1 <= m+1 by XREAL_1:6;
m+1 < n+1 by A5, XREAL_1:8;
hence A10: T.(n9-1) <> T.(n9+1) by A2, A8, A9, GLIB_001:138;
T.(m+1) in v.edgesInOut() & T.(n+1) in v.edgesInOut()
by A4, A7, GLIB_000:62;
hence {T.(n9-1),T.(n9+1)} c= v.edgesInOut() by A2, ZFMISC_1:32;
then card{T.(n-1),T.(n+1)} c= card(v.edgesInOut()) by CARD_1:11;
then A11: 2 c= card(v.edgesInOut()) by A10, CARD_2:57;
card(v.edgesInOut()) c= v.inDegree() +` v.outDegree() by CARD_2:34;
hence 2 c= v.degree() by A11;
end;