:: Recognizing Chordal Graphs: Lex BFS and MCS
:: by Broderick Arneson and Piotr Rudnicki
::
:: Received November 17, 2006
:: Copyright (c) 2006-2016 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, FUNCT_1, CARD_1, RELAT_1, TARSKI, FUNCT_4, FUNCOP_1,
XBOOLE_0, SUBSET_1, XXREAL_0, ARYTM_3, FINSET_1, ORDINAL1, ARYTM_1,
NAT_1, ZFMISC_1, FINSEQ_1, UPROOTS, VALUED_0, RELAT_2, BAGORDER,
PRE_POLY, WELLORD1, GLIB_000, GLIB_001, ORDINAL4, PBOOLE, PARTFUN1,
MCART_1, FUNCT_2, FINSUB_1, CHORD, TOPGEN_1, RCOMP_1, FINSEQ_4, GRAPH_1,
MEMBERED, ABIAN, LEXBFS, MATROID0, REAL_1, XCMPLX_0;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, MCART_1, CARD_1, ORDINAL1,
NUMBERS, SUBSET_1, XXREAL_0, VALUED_0, XREAL_0, RELAT_1, RELAT_2,
WELLORD1, MEMBERED, XXREAL_2, PARTFUN1, FUNCT_1, FUNCT_2, PBOOLE,
FINSET_1, XCMPLX_0, NAT_1, NAT_D, FUNCOP_1, FUNCT_4, GLIB_000, GLIB_001,
BAGORDER, TERMORD, UPROOTS, CHORD, FINSEQ_1, DOMAIN_1, ABIAN, RELSET_1,
RECDEF_1, FINSUB_1, RFUNCT_3, PRE_POLY;
constructors DOMAIN_1, FUNCT_4, XXREAL_2, BAGORDER, TERMORD, UPROOTS, CHORD,
RECDEF_1, RFUNCT_3, RELSET_1, PBOOLE, XTUPLE_0, NUMBERS;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1,
FINSET_1, XXREAL_0, XREAL_0, XXREAL_2, NAT_1, INT_1, MEMBERED, FINSEQ_1,
CARD_1, GLIB_000, ABIAN, BAGORDER, TERMORD, GLIB_001, CHORD, VALUED_0,
FINSUB_1, PARTFUN1, RELSET_1, PRE_POLY, XTUPLE_0;
requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM;
begin
:: More general than GRAPH_2:4
theorem :: LEXBFS:1
for A,B being Element of NAT, X being non empty set for F being
sequence of X st F is one-to-one holds card {F.w where w is Element of NAT
: A <= w & w <= A + B} = B+1;
theorem :: LEXBFS:2
for n,m,k being Nat st m <= k & n < m holds k -' m < k -' n;
notation
let S be set;
synonym S is with_finite-elements for S is finite-membered;
end;
registration
cluster non empty finite with_finite-elements for Subset of bool NAT;
end;
definition
::$CD
let f,g be Function;
func f .\/ g -> Function means
:: LEXBFS:def 2
dom it = dom f \/ dom g & for x being
object st x in dom f \/ dom g holds it.x = f.x \/ g.x;
end;
theorem :: LEXBFS:3
for m,n,k being Nat holds m in ((Seg k) \ Seg (k -' n)) iff k -'
n < m & m <= k;
theorem :: LEXBFS:4
for n,k,m being Nat st n <= m holds ((Seg k) \ Seg (k -' n)) c= (
(Seg k) \ Seg (k -' m));
theorem :: LEXBFS:5
for n,k being Nat st n < k holds ((Seg k) \ Seg (k -' n)) \/ {k
-' n} = (Seg k) \ Seg (k -' (n+1));
definition
let f be Relation;
attr f is natsubset-yielding means
:: LEXBFS:def 3
rng f c= bool NAT;
end;
registration
cluster finite-yielding natsubset-yielding for Function;
end;
definition
let f be finite-yielding natsubset-yielding Function, x be set;
redefine func f.x -> finite Subset of NAT;
end;
theorem :: LEXBFS:6
for X being Ordinal, a, b be finite Subset of X st a <> b holds (
a,1)-bag <> (b,1)-bag;
definition
let F be natural-valued Function, S be set, k be Nat;
func F.incSubset(S,k) -> natural-valued Function means
:: LEXBFS:def 4
dom it = dom F
& for y being object holds (y in S & y in dom F implies it.y = F.y + k) &
(not y in S implies it.y = F.y);
end;
definition
let n be Ordinal, T be connected TermOrder of n, B be non empty finite
Subset of Bags n;
func max(B,T) -> bag of n means
:: LEXBFS:def 5
it in B & for x being bag of n st x in B holds x <= it,T;
end;
registration
let O be Ordinal;
cluster InvLexOrder O -> connected;
end;
begin :: More on Sequences
definition
let s be ManySortedSet of NAT;
attr s is iterative means
:: LEXBFS:def 6
for k, n being Nat st s.k = s.n holds s.(k+ 1) = s.(n+1);
end;
definition
let S be ManySortedSet of NAT;
attr S is eventually-constant means
:: LEXBFS:def 7
ex n being Nat st for m being Nat st n <= m holds S.n = S.m;
end;
registration
cluster halting iterative eventually-constant for ManySortedSet of NAT;
end;
theorem :: LEXBFS:7
for Gs being ManySortedSet of NAT st Gs is halting & Gs is
iterative holds Gs is eventually-constant;
registration
cluster halting iterative -> eventually-constant for ManySortedSet of NAT;
end;
theorem :: LEXBFS:8
for Gs being ManySortedSet of NAT st Gs is eventually-constant
holds Gs is halting;
registration
cluster eventually-constant -> halting for ManySortedSet of NAT;
end;
theorem :: LEXBFS:9
for Gs being iterative eventually-constant ManySortedSet of NAT
for n being Nat st Gs.Lifespan() <= n holds Gs.(Gs.Lifespan()) = Gs.n;
theorem :: LEXBFS:10
for Gs being iterative eventually-constant ManySortedSet of NAT
for n,m being Nat st Gs.Lifespan() <= n & n <= m holds Gs.m = Gs.n;
begin :: Vertex numbering sequences
definition
let G be finite _Graph;
mode preVNumberingSeq of G -> ManySortedSet of NAT means
:: LEXBFS:def 8
for i being Nat holds it.i is PartFunc of the_Vertices_of G, NAT;
end;
definition
let G be finite _Graph, S be preVNumberingSeq of G, n be Nat;
redefine func S.n -> PartFunc of the_Vertices_of G, NAT;
end;
definition
let G be finite _Graph, S be preVNumberingSeq of G;
attr S is vertex-numbering means
:: LEXBFS:def 9
S.0 = {} & S is iterative & S is
halting & S.Lifespan() = G.order() & for n being Nat st n < S.Lifespan() ex w
being Vertex of G st not w in dom (S.n) & (S.(n+1)) = (S.n) +* (w .--> (S
.Lifespan()-'n));
end;
registration
let G be finite _Graph;
cluster vertex-numbering for preVNumberingSeq of G;
end;
:: Facts hidden in the existence proof?
registration
let G be finite _Graph;
cluster vertex-numbering -> halting iterative for preVNumberingSeq of G;
end;
definition
let G be finite _Graph;
mode VNumberingSeq of G is vertex-numbering preVNumberingSeq of G;
end;
definition
let G be finite _Graph, S be VNumberingSeq of G, n be Nat;
func S.PickedAt(n) -> set means
:: LEXBFS:def 10
it = the Element of the_Vertices_of G if n
>= S.Lifespan() otherwise not it in dom (S.n) & S.(n+1) = S.n +* (it .--> (S
.Lifespan()-'n));
end;
theorem :: LEXBFS:11
for G being finite _Graph, S being VNumberingSeq of G, n being
Nat st n < S.Lifespan() holds S.PickedAt(n) in dom (S.(n+1)) & dom (S.(n+1)) =
dom (S.n) \/ {S.PickedAt(n)};
theorem :: LEXBFS:12
for G being finite _Graph, S being VNumberingSeq of G, n being
Nat st n < S.Lifespan() holds (S.(n+1)).(S.PickedAt(n)) = S.Lifespan()-'n;
theorem :: LEXBFS:13
for G being finite _Graph, S being VNumberingSeq of G, n being Nat st
n <= S.Lifespan() holds card dom (S.n) = n;
theorem :: LEXBFS:14
for G being finite _Graph, S being VNumberingSeq of G, n being
Nat holds rng (S.n) = (Seg S.Lifespan()) \ Seg (S.Lifespan()-'n);
theorem :: LEXBFS:15
for G being finite _Graph, S being VNumberingSeq of G, n being
Nat, x being set holds (S.n).x <= S.Lifespan() & (x in dom (S.n) implies 1 <= (
S.n).x);
theorem :: LEXBFS:16
for G being finite _Graph, S being VNumberingSeq of G, n,m being
Nat st S.Lifespan() -' n < m & m <= S.Lifespan() ex v being Vertex of G st v in
dom (S.n) & (S.n).v = m;
theorem :: LEXBFS:17
for G being finite _Graph, S being VNumberingSeq of G, m, n
being Nat st m <= n holds S.m c= S.n;
theorem :: LEXBFS:18
for G being finite _Graph, S being VNumberingSeq of G, n being
Nat holds S.n is one-to-one;
theorem :: LEXBFS:19
for G being finite _Graph, S being VNumberingSeq of G, m,n being
Nat, v being set st v in dom (S.m) & v in dom (S.n) holds (S.m).v = (S.n).v;
theorem :: LEXBFS:20
for G being finite _Graph, S being VNumberingSeq of G, m,n being
Nat, v being set st v in dom (S.m) & (S.m).v = n holds S.PickedAt(S.Lifespan()
-'n) = v;
theorem :: LEXBFS:21
for G being finite _Graph, S being VNumberingSeq of G, m, n
being Nat st n < S.Lifespan() & n < m holds S.PickedAt(n) in dom (S.m) & (S.m).
(S.PickedAt(n)) = S.Lifespan() -' n;
:: Inequalities relating the vlabel and the current iteration
theorem :: LEXBFS:22
for G being finite _Graph, S being VNumberingSeq of G, m being
Nat, v being set st v in dom (S.m) holds S.Lifespan() -' (S.m).v < m & S
.Lifespan() -' m < (S.m).v;
:: If a vertex has a larger vlabel than we do at some point in the
:: algorithm, then it must have been in the vlabel when we were picked
theorem :: LEXBFS:23
for G being finite _Graph, S being VNumberingSeq of G, i being
Nat, a,b being set st a in dom (S.i) & b in dom (S.i) & (S.i).a < (S.i).b holds
b in dom (S.(S.Lifespan() -' (S.i).a));
theorem :: LEXBFS:24
for G being finite _Graph, S being VNumberingSeq of G, i being
Nat, a,b being set st a in dom (S.i) & (S.i).a < (S.i).b holds not a in dom (S.
(S.Lifespan() -' (S.i).b));
begin :: Lexicographic Breadth-First Search
definition
let X1,X3 be set, X2 be non empty set;
let x be Element of [: PFuncs(X1,X3),X2 :];
redefine func x`1 -> Element of PFuncs(X1,X3);
end;
definition
let X1, X3 be non empty set, X2 be set;
let x be Element of [: X1, Funcs(X2,X3) :];
redefine func x`2 -> Element of Funcs(X2,X3);
end;
definition
let G be _Graph;
mode LexBFS:Labeling of G is Element of [: PFuncs(the_Vertices_of G, NAT),
Funcs(the_Vertices_of G, Fin NAT) :];
end;
registration
let G be finite _Graph, L be LexBFS:Labeling of G;
cluster L`1 -> finite for set;
cluster L`2 -> finite for set;
end;
definition
let G be _Graph;
func LexBFS:Init(G) -> LexBFS:Labeling of G equals
:: LEXBFS:def 11
[ {}, the_Vertices_of G
--> {} ];
end;
definition
let G be finite _Graph, L be LexBFS:Labeling of G;
func LexBFS:PickUnnumbered(L) -> Vertex of G means
:: LEXBFS:def 12
it = the Element of
the_Vertices_of G if dom L`1 = the_Vertices_of G otherwise ex S being non empty
finite Subset of bool NAT, B being non empty finite Subset of Bags NAT, F being
Function st S = rng F & F = L`2 | (the_Vertices_of G \ dom L`1) & (for x being
finite Subset of NAT holds x in S implies ((x,1)-bag in B)) & (for x being set
holds x in B implies ex y being finite Subset of NAT st y in S & x = (y,1)-bag)
& it = the Element of F " {support max(B,InvLexOrder NAT)};
end;
definition
let G be finite _Graph, L be LexBFS:Labeling of G, v be Vertex of G, n be
Nat;
func LexBFS:Update(L, v, n) -> LexBFS:Labeling of G equals
:: LEXBFS:def 13
[ L`1 +* (v .-->
(G.order()-'n)), L`2 .\/ ((G.AdjacentSet({v}) \ dom L`1) --> {G.order()-'n}) ];
end;
theorem :: LEXBFS:25
for G being finite _Graph, L being LexBFS:Labeling of G, v being
Vertex of G, x being set, k being Nat st not x in G.AdjacentSet({v}) holds L`2.
x = (LexBFS:Update(L,v,k))`2.x;
theorem :: LEXBFS:26
for G being finite _Graph, L being LexBFS:Labeling of G, v being
Vertex of G, x being set, k being Nat st x in dom L`1 holds LexBFS:Update(L,v,k
)`2.x = L`2.x;
theorem :: LEXBFS:27
for G being finite _Graph, L being LexBFS:Labeling of G, v be
Vertex of G, x being set, k being Nat st x in G.AdjacentSet({v}) & not x in dom
L`1 holds LexBFS:Update(L,v,k)`2.x = L`2.x \/ {G.order() -' k};
definition
let G be finite _Graph, L be LexBFS:Labeling of G;
func LexBFS:Step(L) -> LexBFS:Labeling of G equals
:: LEXBFS:def 14
L if G.order() <=
card (dom L`1) otherwise LexBFS:Update(L, LexBFS:PickUnnumbered(L), card dom L
`1);
end;
definition
let G be _Graph;
mode LexBFS:LabelingSeq of G -> ManySortedSet of NAT means
:: LEXBFS:def 15
for n being Nat holds it.n is LexBFS:Labeling of G;
end;
definition
let G be _Graph, S be LexBFS:LabelingSeq of G, n be Nat;
redefine func S.n -> LexBFS:Labeling of G;
end;
definition
let G be _Graph, S be LexBFS:LabelingSeq of G;
redefine func S.Result() -> LexBFS:Labeling of G;
end;
definition
let G be finite _Graph, S be LexBFS:LabelingSeq of G;
func S``1 -> preVNumberingSeq of G means
:: LEXBFS:def 16
for n being Nat holds it.n = (S.n)`1;
end;
definition
let G be finite _Graph;
func LexBFS:CSeq(G) -> LexBFS:LabelingSeq of G means
:: LEXBFS:def 17
it.0 = LexBFS:Init(G) & for n being Nat holds it.(n+1) = LexBFS:Step(it.n);
end;
theorem :: LEXBFS:28
for G being finite _Graph holds LexBFS:CSeq(G) is iterative;
registration
let G be finite _Graph;
cluster LexBFS:CSeq(G) -> iterative;
end;
definition
let X, Y be set, f be Function of X, Fin Y, x be set;
redefine func f.x -> finite Subset of Y;
end;
:: the vertex picked has the largest v2label
theorem :: LEXBFS:29
for G being finite _Graph, L be LexBFS:Labeling of G, x being
set st not x in dom L`1 & dom L`1 <> the_Vertices_of G holds (L`2.x,1)-bag <= (
L`2.(LexBFS:PickUnnumbered(L)),1)-bag, InvLexOrder NAT;
:: the vertex picked is not currently in the vlabel
theorem :: LEXBFS:30
for G being finite _Graph, L be LexBFS:Labeling of G st dom L`1
<> the_Vertices_of G holds not LexBFS:PickUnnumbered(L) in dom L`1;
theorem :: LEXBFS:31
for G being finite _Graph, n being Nat st card dom ((LexBFS:CSeq
(G)).n)`1 < G.order() holds ((LexBFS:CSeq(G)).(n+1))`1 = ((LexBFS:CSeq(G)).n)`1
+* (LexBFS:PickUnnumbered((LexBFS:CSeq(G)).n) .--> (G.order()-'(card (dom ((
LexBFS:CSeq(G)).n)`1))));
theorem :: LEXBFS:32
for G being finite _Graph, n being Nat st n <= G.order() holds
card dom ((LexBFS:CSeq(G)).n)`1 = n;
theorem :: LEXBFS:33
for G being finite _Graph, n being Nat st G.order() <= n holds (
LexBFS:CSeq(G)).(G.order()) = (LexBFS:CSeq(G)).n;
theorem :: LEXBFS:34
for G being finite _Graph, m,n being Nat st G.order() <= m & m
<= n holds (LexBFS:CSeq(G)).m = (LexBFS:CSeq(G)).n;
theorem :: LEXBFS:35
for G being finite _Graph holds LexBFS:CSeq(G) is eventually-constant;
registration
let G be finite _Graph;
cluster LexBFS:CSeq(G) -> eventually-constant;
end;
theorem :: LEXBFS:36
for G being finite _Graph, n being Nat holds dom ((LexBFS:CSeq(G
)).n)`1 = the_Vertices_of(G) iff G.order() <= n;
theorem :: LEXBFS:37
for G being finite _Graph holds (LexBFS:CSeq(G)).Lifespan() = G .order();
theorem :: LEXBFS:38
for G being finite _Graph holds (LexBFS:CSeq(G))``1 is eventually-constant;
theorem :: LEXBFS:39
for G being finite _Graph holds (LexBFS:CSeq(G))``1.Lifespan() =
(LexBFS:CSeq(G)).Lifespan();
registration
let G be finite _Graph;
cluster (LexBFS:CSeq(G))``1 -> vertex-numbering;
end;
theorem :: LEXBFS:40
for G being finite _Graph holds (LexBFS:CSeq(G))``1.Result() = (
LexBFS:CSeq(G)).Result()`1;
theorem :: LEXBFS:41
for G being finite _Graph, n being Nat st n < G.order() holds ((
LexBFS:CSeq(G))``1).PickedAt(n) = LexBFS:PickUnnumbered((LexBFS:CSeq(G)).n);
theorem :: LEXBFS:42
for G being finite _Graph, n being Nat st n < G.order() ex w
being Vertex of G st w = LexBFS:PickUnnumbered((LexBFS:CSeq(G)).n) & for v
being set holds (v in G.AdjacentSet({w}) & not v in dom ((LexBFS:CSeq(G)).n)`1
implies ((LexBFS:CSeq(G)).(n+1)) `2.v = (((LexBFS:CSeq(G)).n))`2.v \/ {G
.order() -' n}) & ((not v in G.AdjacentSet({w}) or v in dom (((LexBFS:CSeq(G)).
n))`1) implies ((LexBFS:CSeq(G)).(n+1)) `2.v = (((LexBFS:CSeq(G)).n))`2.v);
theorem :: LEXBFS:43
for G being finite _Graph, i being Nat, v being set holds ((
LexBFS:CSeq(G)).i)`2.v c= (Seg G.order()) \ Seg (G.order()-'i);
theorem :: LEXBFS:44
for G being finite _Graph, x being set, i,j being Nat st i <= j
holds ((LexBFS:CSeq(G)).i)`2.x c= ((LexBFS:CSeq(G)).j)`2.x;
theorem :: LEXBFS:45
for G being finite _Graph, m,n being Nat, x, y being set st n <
G.order() & n < m & y = LexBFS:PickUnnumbered((LexBFS:CSeq(G)).n) & not x in
dom ((LexBFS:CSeq(G)).n)`1 & x in G.AdjacentSet({y}) holds (G.order() -' n) in
((LexBFS:CSeq(G)).m)`2.x;
theorem :: LEXBFS:46
for G being finite _Graph, m,n being Nat st m < n for x being
set st not G.order()-'m in ((LexBFS:CSeq(G)).(m+1))`2.x holds not G.order()-'m
in ((LexBFS:CSeq(G)).n)`2.x;
:: More general version of the above:
:: if the value added during step k doesn't appear in a later step (n),
:: then that value cannot appear in an even later step (m)
theorem :: LEXBFS:47
for G being finite _Graph, m,n,k being Nat st k < n & n <= m for
x being set st not G.order()-'k in ((LexBFS:CSeq(G)).n)`2.x holds not G.order()
-'k in ((LexBFS:CSeq(G)).m)`2.x;
:: relates a value in a vertex's v2label to the vertex chosen at that time
theorem :: LEXBFS:48
for G being finite _Graph, m,n being Nat, x being Vertex of G st
n in ((LexBFS:CSeq(G)).m)`2.x ex y being Vertex of G st (LexBFS:PickUnnumbered(
(LexBFS:CSeq(G)).(G.order()-'n))) = y & not y in dom ((LexBFS:CSeq(G)).(G
.order()-'n))`1 & x in G.AdjacentSet({y});
theorem :: LEXBFS:49
for G being finite _Graph holds dom ((LexBFS:CSeq(G)).Result())
`1 = the_Vertices_of G;
::$N Lexicographic_breadth-first_search
theorem :: LEXBFS:50
for G being finite _Graph holds ((LexBFS:CSeq(G)).Result()`1)"
is VertexScheme of G;
:: A vertex with a vlabel of k must have had the largest v2label when chosen
theorem :: LEXBFS:51
for G being finite _Graph, i,j being Nat, a,b being Vertex of G
st a in dom ((LexBFS:CSeq(G)).i)`1 & b in dom ((LexBFS:CSeq(G)).i)`1 & ((
LexBFS:CSeq(G)).i)`1.a < ((LexBFS:CSeq(G)).i)`1.b & j = G.order() -' ((
LexBFS:CSeq(G)).i)`1.b holds (((LexBFS:CSeq(G)).j)`2.a,1)-bag <= ((((
LexBFS:CSeq(G)).j)`2).b,1)-bag, InvLexOrder NAT;
:: Any value in our v2label corresponds to a vertex that we are
:: adjacent to in our in our vlabel
theorem :: LEXBFS:52
for G being finite _Graph, i,j being Nat,v being Vertex of G st
j in ((LexBFS:CSeq(G)).i)`2.v ex w being Vertex of G st w in dom ((LexBFS:CSeq(
G)).i)`1 & (((LexBFS:CSeq(G)).i)`1).w = j & v in G.AdjacentSet{w};
definition
let G be _Graph, F be PartFunc of the_Vertices_of G, NAT;
attr F is with_property_L3 means
:: LEXBFS:def 18
for a,b,c being Vertex of G st a in
dom F & b in dom F & c in dom F & F.a < F.b & F.b < F.c & a,c are_adjacent &
not b,c are_adjacent ex d being Vertex of G st d in dom F & F.c < F.d & b,d
are_adjacent & not a,d are_adjacent & for e being Vertex of G st e <> d & e,b
are_adjacent & not e,a are_adjacent holds F.e < F.d;
end;
theorem :: LEXBFS:53
for G being finite _Graph, n being Nat holds ((LexBFS:CSeq(G)).n
)`1 is with_property_L3;
theorem :: LEXBFS:54 :: Theorem 4.3, Golumbic p. 86
for G being finite chordal _Graph, L be PartFunc of
the_Vertices_of G, NAT st L is with_property_L3 & dom L = the_Vertices_of G for
V being VertexScheme of G st V" = L holds V is perfect;
theorem :: LEXBFS:55 :: Theorem 4.3, Golumbic p. 86
for G being finite chordal _Graph holds (((LexBFS:CSeq(G)).Result())`1
)" is perfect VertexScheme of G;
begin :: The Maximum Cardinality Search algorithm
definition
let G be _Graph;
mode MCS:Labeling of G is Element of [: PFuncs(the_Vertices_of G, NAT),
Funcs(the_Vertices_of G, NAT) :];
end;
definition
let G be finite _Graph;
func MCS:Init(G) -> MCS:Labeling of G equals
:: LEXBFS:def 19
[ {}, the_Vertices_of G --> 0 ];
end;
definition
let G be finite _Graph, L be MCS:Labeling of G;
func MCS:PickUnnumbered(L) -> Vertex of G means
:: LEXBFS:def 20
it = the Element of
the_Vertices_of G if dom L`1 = the_Vertices_of G otherwise ex S being finite
non empty natural-membered set, F being Function st S = rng F & F = L`2 | (
the_Vertices_of G \ dom (L`1)) & it = the Element of F " {max S};
end;
definition
let G be finite _Graph, L be MCS:Labeling of G, v be set;
func MCS:LabelAdjacent(L, v) -> MCS:Labeling of G equals
:: LEXBFS:def 21
[ L`1, (L`2).incSubset(G.AdjacentSet({v}) \ dom L`1, 1) ];
end;
definition
let G be finite _Graph, L be MCS:Labeling of G, v be Vertex of G, n be Nat;
func MCS:Update(L, v, n) -> MCS:Labeling of G means
:: LEXBFS:def 22
ex M being
MCS:Labeling of G st M = [L`1 +* (v .--> (G.order()-'n)), L`2] & it =
MCS:LabelAdjacent(M, v);
end;
definition
let G be finite _Graph, L be MCS:Labeling of G;
func MCS:Step(L) -> MCS:Labeling of G equals
:: LEXBFS:def 23
L if G.order() <= card
dom (L`1) otherwise MCS:Update(L, MCS:PickUnnumbered(L), card dom (L`1));
end;
definition
let G be _Graph;
mode MCS:LabelingSeq of G -> ManySortedSet of NAT means
:: LEXBFS:def 24
for n being Nat holds it.n is MCS:Labeling of G;
end;
definition
let G be _Graph, S be MCS:LabelingSeq of G, n be Nat;
redefine func S.n -> MCS:Labeling of G;
end;
definition
let G be _Graph, S be MCS:LabelingSeq of G;
redefine func S.Result() -> MCS:Labeling of G;
end;
definition
let G be finite _Graph, S be MCS:LabelingSeq of G;
func S``1 -> preVNumberingSeq of G means
:: LEXBFS:def 25
for n being Nat holds it.n = (S.n)`1;
end;
definition
let G be finite _Graph;
func MCS:CSeq(G) -> MCS:LabelingSeq of G means
:: LEXBFS:def 26
it.0 = MCS:Init(G) & for n being Nat holds it.(n+1) = MCS:Step(it.n);
end;
theorem :: LEXBFS:56
for G being finite _Graph holds MCS:CSeq(G) is iterative;
registration
let G be finite _Graph;
cluster MCS:CSeq(G) -> iterative;
end;
theorem :: LEXBFS:57
for G being finite _Graph, v being set holds ((MCS:Init(G))`2).v = 0;
theorem :: LEXBFS:58
for G being finite _Graph, L be MCS:Labeling of G, x being set
st not x in dom L`1 & dom L`1 <> the_Vertices_of G holds (L`2).x <= (L`2).(
MCS:PickUnnumbered(L));
theorem :: LEXBFS:59
for G being finite _Graph, L be MCS:Labeling of G st dom L`1 <>
the_Vertices_of G holds not MCS:PickUnnumbered(L) in dom L`1;
theorem :: LEXBFS:60
for G being finite _Graph, L be MCS:Labeling of G, v,x being set
st not x in G.AdjacentSet({v}) holds (L`2).x = (MCS:LabelAdjacent(L,v))`2.x;
theorem :: LEXBFS:61
for G being finite _Graph, L be MCS:Labeling of G, v,x being set
st x in dom L`1 holds L`2.x = (MCS:LabelAdjacent(L,v))`2.x;
theorem :: LEXBFS:62
for G being finite _Graph, L being MCS:Labeling of G, v,x being
set st x in dom L`2 & x in G.AdjacentSet{v} & not x in dom L`1 holds (
MCS:LabelAdjacent(L,v))`2.x = (L`2).x + 1;
theorem :: LEXBFS:63
for G being finite _Graph, L being MCS:Labeling of G, v being set st
dom L`2 = the_Vertices_of G holds dom (MCS:LabelAdjacent(L,v))`2 =
the_Vertices_of G;
theorem :: LEXBFS:64
for G being finite _Graph, n being Nat st card dom (((MCS:CSeq(G
)).n))`1 < G.order() holds ((MCS:CSeq(G)).(n+1))`1 = ((MCS:CSeq(G)).n)`1 +* (
MCS:PickUnnumbered((MCS:CSeq(G)).n) .--> (G.order()-'(card (dom ((MCS:CSeq(G)).
n)`1))));
theorem :: LEXBFS:65
for G being finite _Graph, n being Nat st n <= G.order() holds
card dom ((MCS:CSeq(G)).n)`1 = n;
theorem :: LEXBFS:66
for G being finite _Graph, n being Nat st G.order() <= n holds (
MCS:CSeq(G)).(G.order()) = (MCS:CSeq(G)).n;
theorem :: LEXBFS:67
for G being finite _Graph, m,n being Nat st G.order() <= m & m
<= n holds (MCS:CSeq(G)).m = (MCS:CSeq(G)).n;
theorem :: LEXBFS:68
for G being finite _Graph holds MCS:CSeq(G) is eventually-constant;
registration
let G be finite _Graph;
cluster MCS:CSeq(G) -> eventually-constant;
end;
theorem :: LEXBFS:69
for G being finite _Graph, n being Nat holds dom ((MCS:CSeq(G)).
n)`1 = the_Vertices_of G iff G.order() <= n;
theorem :: LEXBFS:70
for G being finite _Graph holds (MCS:CSeq(G)).Lifespan() = G .order();
theorem :: LEXBFS:71
for G being finite _Graph holds (MCS:CSeq(G))``1 is eventually-constant;
theorem :: LEXBFS:72
for G being finite _Graph holds (MCS:CSeq(G))``1.Lifespan() = (
MCS:CSeq(G)).Lifespan();
theorem :: LEXBFS:73
for G being finite _Graph holds MCS:CSeq(G)``1 is vertex-numbering;
registration
let G be finite _Graph;
cluster (MCS:CSeq(G))``1 -> vertex-numbering;
end;
theorem :: LEXBFS:74
for G being finite _Graph, n being Nat st n < G.order() holds ((
MCS:CSeq(G))``1).PickedAt(n) = MCS:PickUnnumbered((MCS:CSeq(G)).n);
theorem :: LEXBFS:75
for G being finite _Graph, n being Nat st n < G.order() ex w
being Vertex of G st w = MCS:PickUnnumbered((MCS:CSeq(G)).n) & for v being set
holds (v in G.AdjacentSet({w}) & not v in dom (((MCS:CSeq(G)).n)`1) implies (((
MCS:CSeq(G)).(n+1))`2).v = (((MCS:CSeq(G)).n)`2).v + 1) & (not v in G
.AdjacentSet({w}) or v in dom (((MCS:CSeq(G)).n)`1) implies (((MCS:CSeq(G)).(n+
1))`2).v = (((MCS:CSeq(G)).n)`2).v);
theorem :: LEXBFS:76
for G being finite _Graph, n being Nat, x being set st not x in
dom ((MCS:CSeq(G)).n)`1 holds (((MCS:CSeq(G)).n)`2).x = card (G.AdjacentSet({x}
) /\ (dom ((MCS:CSeq(G)).n)`1));
definition
let G be _Graph, F be PartFunc of the_Vertices_of G, NAT;
attr F is with_property_T means
:: LEXBFS:def 27
for a,b,c being Vertex of G st a in
dom F & b in dom F & c in dom F & F.a < F.b & F.b < F.c & a,c are_adjacent &
not b,c are_adjacent ex d being Vertex of G st d in dom F & F.b < F.d & b,d
are_adjacent & not a,d are_adjacent;
end;
theorem :: LEXBFS:77
for G being finite _Graph, n being Nat holds ((MCS:CSeq(G)).n)`1 is
with_property_T;
theorem :: LEXBFS:78
for G being finite _Graph holds ((LexBFS:CSeq(G)).Result())`1 is
with_property_T;
theorem :: LEXBFS:79 :: Tarjan (SIAM Journal of Computing; 13(3):August 1984)
for G being finite chordal _Graph, L being PartFunc of the_Vertices_of
G, NAT st L is with_property_T & dom L = the_Vertices_of G for V being
VertexScheme of G st V" = L holds V is perfect;