:: Recognizing Chordal Graphs: Lex BFS and MCS
:: by Broderick Arneson and Piotr Rudnicki
::
:: Received November 17, 2006
:: Copyright (c) 2006-2012 Association of Mizar Users


begin

Lm1:  for F being Function
for x, y being set holds dom (F +* (x .--> y)) = (dom F) \/ {x}
proofend;

Lm2:  for f being one-to-one Function
for X, Y being set st X c= Y holds
for x being set st x in dom ((f | X) ") holds
((f | X) ") . x = ((f | Y) ") . x
proofend;

:: More general than GRAPH_2:4
theorem :: LEXBFS:1
for A, B being Element of NAT
for X being non empty set
for F being Function of NAT,X st F is one-to-one holds
card  {  (F . w) where w is Element of NAT : ( A <= w &amp; w <= A + B )  }  = B + 1
proofend;

Lm3:  for a, b, c being real number st a < b holds
(c - b) + 1 < (c - a) + 1
proofend;

theorem Th2: :: LEXBFS:2
for n, m, k being Nat st m <= k &amp; n < m holds
k -' m < k -' n
proofend;

notation
let S be set ;
synonym  with_finite-elements S for  finite-membered ;
end;

registration
cluster non empty finite with_finite-elements for Element of bool (bool NAT);
existence
 ex b1 being Subset of (bool NAT) st
( not b1 is empty &amp; b1 is finite &amp; b1 is with_finite-elements )
proofend;
end;

definition
canceled;
let f, g be Function;
funcf .\/ g ->  Function means :Def2: :: LEXBFS:def 2
( dom it = (dom f) \/ (dom g) &amp; ( for x being set st x in (dom f) \/ (dom g) holds
it . x = (f . x) \/ (g . x) ) );
existence
 ex b1 being Function st
( dom b1 = (dom f) \/ (dom g) &amp; ( for x being set st x in (dom f) \/ (dom g) holds
b1 . x = (f . x) \/ (g . x) ) )
proofend;
uniqueness
 for b1, b2 being Function st dom b1 = (dom f) \/ (dom g) &amp; ( for x being set st x in (dom f) \/ (dom g) holds
b1 . x = (f . x) \/ (g . x) ) &amp; dom b2 = (dom f) \/ (dom g) &amp; ( for x being set st x in (dom f) \/ (dom g) holds
b2 . x = (f . x) \/ (g . x) ) holds
b1 = b2
proofend;
end;

:: deftheorem  LEXBFS:def_1_:_
canceled;

:: deftheorem Def2 defines .\/ LEXBFS:def_2_:_
 for f, g, b3 being Function holds
( b3 = f .\/ g iff ( dom b3 = (dom f) \/ (dom g) &amp; ( for x being set st x in (dom f) \/ (dom g) holds
b3 . x = (f . x) \/ (g . x) ) ) );

theorem Th3: :: LEXBFS:3
for m, n, k being Nat holds
( m in (Seg k) \ (Seg (k -' n)) iff ( k -' n < m &amp; m <= k ) )
proofend;

theorem Th4: :: LEXBFS:4
for n, k, m being Nat st n <= m holds
(Seg k) \ (Seg (k -' n)) c= (Seg k) \ (Seg (k -' m))
proofend;

theorem Th5: :: LEXBFS:5
for n, k being Nat st n < k holds
((Seg k) \ (Seg (k -' n))) \/ {(k -' n)} = (Seg k) \ (Seg (k -' (n + 1)))
proofend;

definition
let f be Relation;
attrf is natsubset-yielding  means :Def3: :: LEXBFS:def 3
 rng f c= bool NAT;
end;

:: deftheorem Def3 defines natsubset-yielding LEXBFS:def_3_:_
 for f being Relation holds
( f is natsubset-yielding iff rng f c= bool NAT );

registration
cluster Relation-like Function-like finite-yielding natsubset-yielding for set ;
existence
 ex b1 being Function st
( b1 is finite-yielding &amp; b1 is natsubset-yielding )
proofend;
end;

definition
let f be finite-yielding natsubset-yielding Function;
let x be set ;
:: original:.
redefine funcf . x ->  finite Subset of NAT;
coherence
 f . x is finite Subset of NAT
proofend;
end;

theorem Th6: :: LEXBFS:6
for X being Ordinal
for a, b being finite Subset of X st a <> b holds
(a,1) -bag <> (b,1) -bag
proofend;

definition
let F be natural-valued Function;
let S be set ;
let k be Nat;
funcF .incSubset (S,k) ->  natural-valued Function means :Def4: :: LEXBFS:def 4
( dom it = dom F &amp; ( for y being set holds
( ( y in S &amp; y in dom F implies it . y = (F . y) + k ) &amp; ( not y in S implies it . y = F . y ) ) ) );
existence
 ex b1 being natural-valued Function st
( dom b1 = dom F &amp; ( for y being set holds
( ( y in S &amp; y in dom F implies b1 . y = (F . y) + k ) &amp; ( not y in S implies b1 . y = F . y ) ) ) )
proofend;
uniqueness
 for b1, b2 being natural-valued Function st dom b1 = dom F &amp; ( for y being set holds
( ( y in S &amp; y in dom F implies b1 . y = (F . y) + k ) &amp; ( not y in S implies b1 . y = F . y ) ) ) &amp; dom b2 = dom F &amp; ( for y being set holds
( ( y in S &amp; y in dom F implies b2 . y = (F . y) + k ) &amp; ( not y in S implies b2 . y = F . y ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines .incSubset LEXBFS:def_4_:_
 for F being natural-valued Function
for S being set
for k being Nat
for b4 being natural-valued Function holds
( b4 = F .incSubset (S,k) iff ( dom b4 = dom F &amp; ( for y being set holds
( ( y in S &amp; y in dom F implies b4 . y = (F . y) + k ) &amp; ( not y in S implies b4 . y = F . y ) ) ) ) );

definition
let n be Ordinal;
let T be connected TermOrder of n;
let B be non empty finite Subset of (Bags n);
func max (B,T) ->  bag of n means :Def5: :: LEXBFS:def 5
( it in B &amp; ( for x being bag of n st x in B holds
x <= it,T ) );
existence
 ex b1 being bag of n st
( b1 in B &amp; ( for x being bag of n st x in B holds
x <= b1,T ) )
proofend;
uniqueness
 for b1, b2 being bag of n st b1 in B &amp; ( for x being bag of n st x in B holds
x <= b1,T ) &amp; b2 in B &amp; ( for x being bag of n st x in B holds
x <= b2,T ) holds
b1 = b2
proofend;
end;

:: deftheorem Def5 defines max LEXBFS:def_5_:_
 for n being Ordinal
for T being connected TermOrder of n
for B being non empty finite Subset of (Bags n)
for b4 being bag of n holds
( b4 = max (B,T) iff ( b4 in B &amp; ( for x being bag of n st x in B holds
x <= b4,T ) ) );

registration
let O be Ordinal;
cluster InvLexOrder O ->  connected ;
coherence
 InvLexOrder O is connected
proofend;
end;

Lm4:  for G being _Graph
for W being Walk of G
for e, v being set st e Joins W .last() ,v,G holds
(W .addEdge e) .length() = (W .length()) + 1
proofend;

Lm5:  for G being _Graph
for W being Walk of G holds W .length() = (W .reverse()) .length()
proofend;

Lm6:  for G being _Graph
for W being Walk of G
for e, x being set st e Joins W .last() ,x,G holds
for n being Nat st n in dom W holds
( (W .addEdge e) . n = W . n &amp; n in dom (W .addEdge e) )
proofend;

begin

definition
let s be ManySortedSet of NAT ;
attrs is iterative  means :Def6: :: LEXBFS:def 6
 for k, n being Nat st s . k = s . n holds
s . (k + 1) = s . (n + 1);
end;

:: deftheorem Def6 defines iterative LEXBFS:def_6_:_
 for s being ManySortedSet of NAT holds
( s is iterative iff for k, n being Nat st s . k = s . n holds
s . (k + 1) = s . (n + 1) );

definition
let S be ManySortedSet of NAT ;
attrS is eventually-constant  means :Def7: :: LEXBFS:def 7
 ex n being Nat st
for m being Nat st n <= m holds
S . n = S . m;
end;

:: deftheorem Def7 defines eventually-constant LEXBFS:def_7_:_
 for S being ManySortedSet of NAT holds
( S is eventually-constant iff ex n being Nat st
for m being Nat st n <= m holds
S . n = S . m );

registration
cluster Relation-like NAT -defined Function-like total halting iterative eventually-constant for set ;
existence
 ex b1 being ManySortedSet of NAT st
( b1 is halting &amp; b1 is iterative &amp; b1 is eventually-constant )
proofend;
end;

theorem Th7: :: LEXBFS:7
for Gs being ManySortedSet of NAT st Gs is halting &amp; Gs is iterative holds
Gs is eventually-constant
proofend;

registration
cluster Relation-like NAT -defined Function-like total halting iterative  ->  eventually-constant for set ;
coherence
 for b1 being ManySortedSet of NAT st b1 is halting &amp; b1 is iterative holds
b1 is eventually-constant by Th7;
end;

theorem Th8: :: LEXBFS:8
for Gs being ManySortedSet of NAT st Gs is eventually-constant holds
Gs is halting
proofend;

registration
cluster Relation-like NAT -defined Function-like total eventually-constant  ->  halting for set ;
coherence
 for b1 being ManySortedSet of NAT st b1 is eventually-constant holds
b1 is halting by Th8;
end;

theorem Th9: :: 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
proofend;

theorem Th10: :: LEXBFS:10
for Gs being iterative eventually-constant ManySortedSet of NAT
for n, m being Nat st Gs .Lifespan() <= n &amp; n <= m holds
Gs . m = Gs . n
proofend;

begin

definition
let G be finite _Graph;
mode preVNumberingSeq of G ->  ManySortedSet of NAT  means :Def8: :: LEXBFS:def 8
 for i being Nat holds it . i is PartFunc of (the_Vertices_of G),NAT;
existence
 ex b1 being ManySortedSet of NAT st
for i being Nat holds b1 . i is PartFunc of (the_Vertices_of G),NAT
proofend;
end;

:: deftheorem Def8 defines preVNumberingSeq LEXBFS:def_8_:_
 for G being finite _Graph
for b2 being ManySortedSet of NAT holds
( b2 is preVNumberingSeq of G iff for i being Nat holds b2 . i is PartFunc of (the_Vertices_of G),NAT );

definition
let G be finite _Graph;
let S be preVNumberingSeq of G;
let n be Nat;
:: original:.
redefine funcS . n ->  PartFunc of (the_Vertices_of G),NAT;
coherence
 S . n is PartFunc of (the_Vertices_of G),NAT by Def8;
end;

definition
let G be finite _Graph;
let S be preVNumberingSeq of G;
attrS is vertex-numbering  means :Def9: :: LEXBFS:def 9
( S . 0 = {} &amp; S is iterative &amp; S is halting &amp; S .Lifespan() = G .order() &amp; ( for n being Nat st n < S .Lifespan() holds
ex w being Vertex of G st
( not w in dom (S . n) &amp; S . (n + 1) = (S . n) +* (w .--> ((S .Lifespan()) -' n)) ) ) );
end;

:: deftheorem Def9 defines vertex-numbering LEXBFS:def_9_:_
 for G being finite _Graph
for S being preVNumberingSeq of G holds
( S is vertex-numbering iff ( S . 0 = {} &amp; S is iterative &amp; S is halting &amp; S .Lifespan() = G .order() &amp; ( for n being Nat st n < S .Lifespan() holds
ex w being Vertex of G st
( not w in dom (S . n) &amp; S . (n + 1) = (S . n) +* (w .--> ((S .Lifespan()) -' n)) ) ) ) );

registration
let G be finite _Graph;
cluster Relation-like NAT -defined Function-like total vertex-numbering for preVNumberingSeq of G;
existence
 ex b1 being preVNumberingSeq of G st b1 is vertex-numbering
proofend;
end;

:: Facts hidden in the existence proof?
registration
let G be finite _Graph;
cluster vertex-numbering  ->  halting iterative for preVNumberingSeq of G;
correctness
coherence
for b1 being preVNumberingSeq of G st b1 is vertex-numbering holds
( b1 is halting &amp; b1 is iterative );
by Def9;
end;

definition
let G be finite _Graph;
mode VNumberingSeq of G is vertex-numbering preVNumberingSeq of G;
end;

definition
let G be finite _Graph;
let S be VNumberingSeq of G;
let n be Nat;
funcS .PickedAt n ->  set  means :Def10: :: LEXBFS:def 10
it = choose (the_Vertices_of G) if n >= S .Lifespan()
otherwise ( not it in dom (S . n) &amp; S . (n + 1) = (S . n) +* (it .--> ((S .Lifespan()) -' n)) );
existence
 ( ( n >= S .Lifespan() implies ex b1 being set st b1 = choose (the_Vertices_of G) ) &amp; ( not n >= S .Lifespan() implies ex b1 being set st
( not b1 in dom (S . n) &amp; S . (n + 1) = (S . n) +* (b1 .--> ((S .Lifespan()) -' n)) ) ) )
proofend;
uniqueness
 for b1, b2 being set holds
( ( n >= S .Lifespan() &amp; b1 = choose (the_Vertices_of G) &amp; b2 = choose (the_Vertices_of G) implies b1 = b2 ) &amp; ( not n >= S .Lifespan() &amp; not b1 in dom (S . n) &amp; S . (n + 1) = (S . n) +* (b1 .--> ((S .Lifespan()) -' n)) &amp; not b2 in dom (S . n) &amp; S . (n + 1) = (S . n) +* (b2 .--> ((S .Lifespan()) -' n)) implies b1 = b2 ) )
proofend;
consistency
 for b1 being set holds verum ;
end;

:: deftheorem Def10 defines .PickedAt LEXBFS:def_10_:_
 for G being finite _Graph
for S being VNumberingSeq of G
for n being Nat
for b4 being set holds
( ( n >= S .Lifespan() implies ( b4 = S .PickedAt n iff b4 = choose (the_Vertices_of G) ) ) &amp; ( not n >= S .Lifespan() implies ( b4 = S .PickedAt n iff ( not b4 in dom (S . n) &amp; S . (n + 1) = (S . n) +* (b4 .--> ((S .Lifespan()) -' n)) ) ) ) );

theorem Th11: :: LEXBFS:11
for G being finite _Graph
for S being VNumberingSeq of G
for n being Nat st n < S .Lifespan() holds
( S .PickedAt n in dom (S . (n + 1)) &amp; dom (S . (n + 1)) = (dom (S . n)) \/ {(S .PickedAt n)} )
proofend;

theorem Th12: :: LEXBFS:12
for G being finite _Graph
for S being VNumberingSeq of G
for n being Nat st n < S .Lifespan() holds
(S . (n + 1)) . (S .PickedAt n) = (S .Lifespan()) -' n
proofend;

theorem :: LEXBFS:13
for G being finite _Graph
for S being VNumberingSeq of G
for n being Nat st n <= S .Lifespan() holds
card (dom (S . n)) = n
proofend;

theorem Th14: :: LEXBFS:14
for G being finite _Graph
for S being VNumberingSeq of G
for n being Nat holds rng (S . n) = (Seg (S .Lifespan())) \ (Seg ((S .Lifespan()) -' n))
proofend;

theorem Th15: :: LEXBFS:15
for G being finite _Graph
for S being VNumberingSeq of G
for n being Nat
for x being set holds
( (S . n) . x <= S .Lifespan() &amp; ( x in dom (S . n) implies 1 <= (S . n) . x ) )
proofend;

theorem Th16: :: LEXBFS:16
for G being finite _Graph
for S being VNumberingSeq of G
for n, m being Nat st (S .Lifespan()) -' n < m &amp; m <= S .Lifespan() holds
ex v being Vertex of G st
( v in dom (S . n) &amp; (S . n) . v = m )
proofend;

theorem Th17: :: LEXBFS:17
for G being finite _Graph
for S being VNumberingSeq of G
for m, n being Nat st m <= n holds
S . m c= S . n
proofend;

theorem Th18: :: LEXBFS:18
for G being finite _Graph
for S being VNumberingSeq of G
for n being Nat holds S . n is one-to-one
proofend;

theorem Th19: :: LEXBFS:19
for G being finite _Graph
for S being VNumberingSeq of G
for m, n being Nat
for v being set st v in dom (S . m) &amp; v in dom (S . n) holds
(S . m) . v = (S . n) . v
proofend;

theorem Th20: :: LEXBFS:20
for G being finite _Graph
for S being VNumberingSeq of G
for m, n being Nat
for v being set st v in dom (S . m) &amp; (S . m) . v = n holds
S .PickedAt ((S .Lifespan()) -' n) = v
proofend;

theorem Th21: :: LEXBFS:21
for G being finite _Graph
for S being VNumberingSeq of G
for m, n being Nat st n < S .Lifespan() &amp; n < m holds
( S .PickedAt n in dom (S . m) &amp; (S . m) . (S .PickedAt n) = (S .Lifespan()) -' n )
proofend;

:: Inequalities relating the vlabel and the current iteration
theorem Th22: :: LEXBFS:22
for G being finite _Graph
for S being VNumberingSeq of G
for m being Nat
for v being set st v in dom (S . m) holds
( (S .Lifespan()) -' ((S . m) . v) < m &amp; (S .Lifespan()) -' m < (S . m) . v )
proofend;

:: 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 Th23: :: LEXBFS:23
for G being finite _Graph
for S being VNumberingSeq of G
for i being Nat
for a, b being set st a in dom (S . i) &amp; b in dom (S . i) &amp; (S . i) . a < (S . i) . b holds
b in dom (S . ((S .Lifespan()) -' ((S . i) . a)))
proofend;

theorem Th24: :: LEXBFS:24
for G being finite _Graph
for S being VNumberingSeq of G
for i being Nat
for a, b being set st a in dom (S . i) &amp; (S . i) . a < (S . i) . b holds
not a in dom (S . ((S .Lifespan()) -' ((S . i) . b)))
proofend;

begin

definition
let X1, X3 be set ;
let X2 be non empty set ;
let x be Element of [:(PFuncs (X1,X3)),X2:];
:: original:`1
redefine funcx `1  ->  Element of PFuncs (X1,X3);
coherence
 x `1 is Element of PFuncs (X1,X3) by MCART_1:10;
end;

definition
let X1, X3 be non empty set ;
let X2 be set ;
let x be Element of [:X1,(Funcs (X2,X3)):];
:: original:`2
redefine funcx `2  ->  Element of Funcs (X2,X3);
coherence
 x `2 is Element of Funcs (X2,X3) by MCART_1:10;
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;
let L be LexBFS:Labeling of G;
clusterL `1  ->  finite ;
coherence
 L `1 is finite
proofend;
clusterL `2  ->  finite ;
coherence
 L `2 is finite ;
end;

definition
let G be _Graph;
func LexBFS:Init G ->  LexBFS:Labeling of G equals :: LEXBFS:def 11
[{},((the_Vertices_of G) --> {})];
coherence
 [{},((the_Vertices_of G) --> {})] is LexBFS:Labeling of G
proofend;
end;

:: deftheorem  defines LexBFS:Init LEXBFS:def_11_:_
 for G being _Graph holds LexBFS:Init G = [{},((the_Vertices_of G) --> {})];

definition
let G be finite _Graph;
let L be LexBFS:Labeling of G;
func LexBFS:PickUnnumbered L ->  Vertex of G means :Def12: :: LEXBFS:def 12
it = choose (the_Vertices_of G) if  dom (L `1) = the_Vertices_of G
otherwise  ex S being non empty finite Subset of (bool NAT) ex B being non empty finite Subset of (Bags NAT) ex F being Function st
( S = rng F &amp; F = (L `2) | ((the_Vertices_of G) \ (dom (L `1))) &amp; ( for x being finite Subset of NAT st x in S holds
(x,1) -bag in B ) &amp; ( for x being set st x in B holds
ex y being finite Subset of NAT st
( y in S &amp; x = (y,1) -bag ) ) &amp; it = choose (F " {(support (max (B,(InvLexOrder NAT))))}) );
existence
 ( ( dom (L `1) = the_Vertices_of G implies ex b1 being Vertex of G st b1 = choose (the_Vertices_of G) ) &amp; ( not dom (L `1) = the_Vertices_of G implies ex b1 being Vertex of G ex S being non empty finite Subset of (bool NAT) ex B being non empty finite Subset of (Bags NAT) ex F being Function st
( S = rng F &amp; F = (L `2) | ((the_Vertices_of G) \ (dom (L `1))) &amp; ( for x being finite Subset of NAT st x in S holds
(x,1) -bag in B ) &amp; ( for x being set st x in B holds
ex y being finite Subset of NAT st
( y in S &amp; x = (y,1) -bag ) ) &amp; b1 = choose (F " {(support (max (B,(InvLexOrder NAT))))}) ) ) )
proofend;
uniqueness
 for b1, b2 being Vertex of G holds
( ( dom (L `1) = the_Vertices_of G &amp; b1 = choose (the_Vertices_of G) &amp; b2 = choose (the_Vertices_of G) implies b1 = b2 ) &amp; ( not dom (L `1) = the_Vertices_of G &amp; ex S being non empty finite Subset of (bool NAT) ex B being non empty finite Subset of (Bags NAT) ex F being Function st
( S = rng F &amp; F = (L `2) | ((the_Vertices_of G) \ (dom (L `1))) &amp; ( for x being finite Subset of NAT st x in S holds
(x,1) -bag in B ) &amp; ( for x being set st x in B holds
ex y being finite Subset of NAT st
( y in S &amp; x = (y,1) -bag ) ) &amp; b1 = choose (F " {(support (max (B,(InvLexOrder NAT))))}) ) &amp; ex S being non empty finite Subset of (bool NAT) ex B being non empty finite Subset of (Bags NAT) ex F being Function st
( S = rng F &amp; F = (L `2) | ((the_Vertices_of G) \ (dom (L `1))) &amp; ( for x being finite Subset of NAT st x in S holds
(x,1) -bag in B ) &amp; ( for x being set st x in B holds
ex y being finite Subset of NAT st
( y in S &amp; x = (y,1) -bag ) ) &amp; b2 = choose (F " {(support (max (B,(InvLexOrder NAT))))}) ) implies b1 = b2 ) )
proofend;
consistency
 for b1 being Vertex of G holds verum ;
end;

:: deftheorem Def12 defines LexBFS:PickUnnumbered LEXBFS:def_12_:_
 for G being finite _Graph
for L being LexBFS:Labeling of G
for b3 being Vertex of G holds
( ( dom (L `1) = the_Vertices_of G implies ( b3 = LexBFS:PickUnnumbered L iff b3 = choose (the_Vertices_of G) ) ) &amp; ( not dom (L `1) = the_Vertices_of G implies ( b3 = LexBFS:PickUnnumbered L iff ex S being non empty finite Subset of (bool NAT) ex B being non empty finite Subset of (Bags NAT) ex F being Function st
( S = rng F &amp; F = (L `2) | ((the_Vertices_of G) \ (dom (L `1))) &amp; ( for x being finite Subset of NAT st x in S holds
(x,1) -bag in B ) &amp; ( for x being set st x in B holds
ex y being finite Subset of NAT st
( y in S &amp; x = (y,1) -bag ) ) &amp; b3 = choose (F " {(support (max (B,(InvLexOrder NAT))))}) ) ) ) );

definition
let G be finite _Graph;
let L be LexBFS:Labeling of G;
let v be Vertex of G;
let 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)}))];
coherence
 [((L `1) +* (v .--> ((G .order()) -' n))),((L `2) .\/ (((G .AdjacentSet {v}) \ (dom (L `1))) --> {((G .order()) -' n)}))] is LexBFS:Labeling of G
proofend;
end;

:: deftheorem  defines LexBFS:Update LEXBFS:def_13_:_
 for G being finite _Graph
for L being LexBFS:Labeling of G
for v being Vertex of G
for n being Nat holds LexBFS:Update (L,v,n) = [((L `1) +* (v .--> ((G .order()) -' n))),((L `2) .\/ (((G .AdjacentSet {v}) \ (dom (L `1))) --> {((G .order()) -' n)}))];

theorem Th25: :: LEXBFS:25
for G being finite _Graph
for L being LexBFS:Labeling of G
for v being Vertex of G
for x being set
for k being Nat st not x in G .AdjacentSet {v} holds
(L `2) . x = ((LexBFS:Update (L,v,k)) `2) . x
proofend;

theorem Th26: :: LEXBFS:26
for G being finite _Graph
for L being LexBFS:Labeling of G
for v being Vertex of G
for x being set
for k being Nat st x in dom (L `1) holds
((LexBFS:Update (L,v,k)) `2) . x = (L `2) . x
proofend;

theorem Th27: :: LEXBFS:27
for G being finite _Graph
for L being LexBFS:Labeling of G
for v being Vertex of G
for x being set
for k being Nat st x in G .AdjacentSet {v} &amp; not x in dom (L `1) holds
((LexBFS:Update (L,v,k)) `2) . x = ((L `2) . x) \/ {((G .order()) -' k)}
proofend;

definition
let G be finite _Graph;
let L be LexBFS:Labeling of G;
func LexBFS:Step L ->  LexBFS:Labeling of G equals :Def14: :: LEXBFS:def 14
L if G .order() <= card (dom (L `1))
otherwise  LexBFS:Update (L,(LexBFS:PickUnnumbered L),(card (dom (L `1))));
coherence
 ( ( G .order() <= card (dom (L `1)) implies L is LexBFS:Labeling of G ) &amp; ( not G .order() <= card (dom (L `1)) implies LexBFS:Update (L,(LexBFS:PickUnnumbered L),(card (dom (L `1)))) is LexBFS:Labeling of G ) ) ;
consistency
 for b1 being LexBFS:Labeling of G holds verum ;
end;

:: deftheorem Def14 defines LexBFS:Step LEXBFS:def_14_:_
 for G being finite _Graph
for L being LexBFS:Labeling of G holds
( ( G .order() <= card (dom (L `1)) implies LexBFS:Step L = L ) &amp; ( not G .order() <= card (dom (L `1)) implies LexBFS:Step L = LexBFS:Update (L,(LexBFS:PickUnnumbered L),(card (dom (L `1)))) ) );

definition
let G be _Graph;
mode LexBFS:LabelingSeq of G ->  ManySortedSet of NAT  means :Def15: :: LEXBFS:def 15
 for n being Nat holds it . n is LexBFS:Labeling of G;
existence
 ex b1 being ManySortedSet of NAT st
for n being Nat holds b1 . n is LexBFS:Labeling of G
proofend;
end;

:: deftheorem Def15 defines LexBFS:LabelingSeq LEXBFS:def_15_:_
 for G being _Graph
for b2 being ManySortedSet of NAT holds
( b2 is LexBFS:LabelingSeq of G iff for n being Nat holds b2 . n is LexBFS:Labeling of G );

definition
let G be _Graph;
let S be LexBFS:LabelingSeq of G;
let n be Nat;
:: original:.
redefine funcS . n ->  LexBFS:Labeling of G;
coherence
 S . n is LexBFS:Labeling of G by Def15;
end;

definition
let G be _Graph;
let S be LexBFS:LabelingSeq of G;
:: original:.Result()
redefine funcS .Result()  ->  LexBFS:Labeling of G;
coherence
 S .Result() is LexBFS:Labeling of G by Def15;
end;

definition
let G be finite _Graph;
let S be LexBFS:LabelingSeq of G;
funcS ``1  ->  preVNumberingSeq of G means :Def16: :: LEXBFS:def 16
 for n being Nat holds it . n = (S . n) `1 ;
existence
 ex b1 being preVNumberingSeq of G st
for n being Nat holds b1 . n = (S . n) `1
proofend;
uniqueness
 for b1, b2 being preVNumberingSeq of G st ( for n being Nat holds b1 . n = (S . n) `1 ) &amp; ( for n being Nat holds b2 . n = (S . n) `1 ) holds
b1 = b2
proofend;
end;

:: deftheorem Def16 defines ``1 LEXBFS:def_16_:_
 for G being finite _Graph
for S being LexBFS:LabelingSeq of G
for b3 being preVNumberingSeq of G holds
( b3 = S ``1 iff for n being Nat holds b3 . n = (S . n) `1 );

definition
let G be finite _Graph;
func LexBFS:CSeq G ->  LexBFS:LabelingSeq of G means :Def17: :: LEXBFS:def 17
( it . 0 = LexBFS:Init G &amp; ( for n being Nat holds it . (n + 1) = LexBFS:Step (it . n) ) );
existence
 ex b1 being LexBFS:LabelingSeq of G st
( b1 . 0 = LexBFS:Init G &amp; ( for n being Nat holds b1 . (n + 1) = LexBFS:Step (b1 . n) ) )
proofend;
uniqueness
 for b1, b2 being LexBFS:LabelingSeq of G st b1 . 0 = LexBFS:Init G &amp; ( for n being Nat holds b1 . (n + 1) = LexBFS:Step (b1 . n) ) &amp; b2 . 0 = LexBFS:Init G &amp; ( for n being Nat holds b2 . (n + 1) = LexBFS:Step (b2 . n) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def17 defines LexBFS:CSeq LEXBFS:def_17_:_
 for G being finite _Graph
for b2 being LexBFS:LabelingSeq of G holds
( b2 = LexBFS:CSeq G iff ( b2 . 0 = LexBFS:Init G &amp; ( for n being Nat holds b2 . (n + 1) = LexBFS:Step (b2 . n) ) ) );

theorem Th28: :: LEXBFS:28
for G being finite _Graph holds LexBFS:CSeq G is iterative
proofend;

registration
let G be finite _Graph;
cluster LexBFS:CSeq G ->  iterative ;
coherence
 LexBFS:CSeq G is iterative by Th28;
end;

Lm7:  for G being _Graph
for v being set holds
( dom ((LexBFS:Init G) `2) = the_Vertices_of G &amp; ((LexBFS:Init G) `2) . v = {} )
proofend;

definition
let X, Y be set ;
let f be Function of X,(Fin Y);
let x be set ;
:: original:.
redefine funcf . x ->  finite Subset of Y;
coherence
 f . x is finite Subset of Y
proofend;
end;

:: the vertex picked has the largest v2label
theorem Th29: :: LEXBFS:29
for G being finite _Graph
for L being LexBFS:Labeling of G
for x being set st not x in dom (L `1) &amp; dom (L `1) <> the_Vertices_of G holds
(((L `2) . x),1) -bag <= (((L `2) . (LexBFS:PickUnnumbered L)),1) -bag , InvLexOrder NAT
proofend;

:: the vertex picked is not currently in the vlabel
theorem Th30: :: LEXBFS:30
for G being finite _Graph
for L being LexBFS:Labeling of G st dom (L `1) <> the_Vertices_of G holds
not LexBFS:PickUnnumbered L in dom (L `1)
proofend;

theorem Th31: :: LEXBFS:31
for G being finite _Graph
for 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)))))
proofend;

theorem Th32: :: LEXBFS:32
for G being finite _Graph
for n being Nat st n <= G .order() holds
card (dom (((LexBFS:CSeq G) . n) `1)) = n
proofend;

theorem Th33: :: LEXBFS:33
for G being finite _Graph
for n being Nat st G .order() <= n holds
(LexBFS:CSeq G) . (G .order()) = (LexBFS:CSeq G) . n
proofend;

theorem Th34: :: LEXBFS:34
for G being finite _Graph
for m, n being Nat st G .order() <= m &amp; m <= n holds
(LexBFS:CSeq G) . m = (LexBFS:CSeq G) . n
proofend;

theorem Th35: :: LEXBFS:35
for G being finite _Graph holds LexBFS:CSeq G is eventually-constant
proofend;

registration
let G be finite _Graph;
cluster LexBFS:CSeq G ->  eventually-constant ;
coherence
 LexBFS:CSeq G is eventually-constant by Th35;
end;

theorem Th36: :: LEXBFS:36
for G being finite _Graph
for n being Nat holds
( dom (((LexBFS:CSeq G) . n) `1) = the_Vertices_of G iff G .order() <= n )
proofend;

theorem Th37: :: LEXBFS:37
for G being finite _Graph holds (LexBFS:CSeq G) .Lifespan() = G .order()
proofend;

theorem Th38: :: LEXBFS:38
for G being finite _Graph holds (LexBFS:CSeq G) ``1 is eventually-constant
proofend;

theorem Th39: :: LEXBFS:39
for G being finite _Graph holds ((LexBFS:CSeq G) ``1) .Lifespan() = (LexBFS:CSeq G) .Lifespan()
proofend;

registration
let G be finite _Graph;
cluster(LexBFS:CSeq G) ``1  ->  vertex-numbering ;
correctness
coherence
(LexBFS:CSeq G) ``1 is vertex-numbering ;
proofend;
end;

theorem Th40: :: LEXBFS:40
for G being finite _Graph holds ((LexBFS:CSeq G) ``1) .Result() = ((LexBFS:CSeq G) .Result()) `1
proofend;

theorem Th41: :: LEXBFS:41
for G being finite _Graph
for n being Nat st n < G .order() holds
((LexBFS:CSeq G) ``1) .PickedAt n = LexBFS:PickUnnumbered ((LexBFS:CSeq G) . n)
proofend;

theorem Th42: :: LEXBFS:42
for G being finite _Graph
for n being Nat st n < G .order() holds
ex w being Vertex of G st
( w = LexBFS:PickUnnumbered ((LexBFS:CSeq G) . n) &amp; ( for v being set holds
( ( v in G .AdjacentSet {w} &amp; 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)} ) &amp; ( ( 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 ) ) ) )
proofend;

theorem Th43: :: LEXBFS:43
for G being finite _Graph
for i being Nat
for v being set holds (((LexBFS:CSeq G) . i) `2) . v c= (Seg (G .order())) \ (Seg ((G .order()) -' i))
proofend;

theorem Th44: :: LEXBFS:44
for G being finite _Graph
for x being set
for i, j being Nat st i <= j holds
(((LexBFS:CSeq G) . i) `2) . x c= (((LexBFS:CSeq G) . j) `2) . x
proofend;

theorem Th45: :: LEXBFS:45
for G being finite _Graph
for m, n being Nat
for x, y being set st n < G .order() &amp; n < m &amp; y = LexBFS:PickUnnumbered ((LexBFS:CSeq G) . n) &amp; not x in dom (((LexBFS:CSeq G) . n) `1) &amp; x in G .AdjacentSet {y} holds
(G .order()) -' n in (((LexBFS:CSeq G) . m) `2) . x
proofend;

theorem Th46: :: LEXBFS:46
for G being finite _Graph
for m, n being Nat st m < n holds
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
proofend;

:: 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 Th47: :: LEXBFS:47
for G being finite _Graph
for m, n, k being Nat st k < n &amp; n <= m holds
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
proofend;

:: relates a value in a vertex's v2label to the vertex chosen at that time
theorem Th48: :: LEXBFS:48
for G being finite _Graph
for m, n being Nat
for x being Vertex of G st n in (((LexBFS:CSeq G) . m) `2) . x holds
ex y being Vertex of G st
( LexBFS:PickUnnumbered ((LexBFS:CSeq G) . ((G .order()) -' n)) = y &amp; not y in dom (((LexBFS:CSeq G) . ((G .order()) -' n)) `1) &amp; x in G .AdjacentSet {y} )
proofend;

theorem Th49: :: LEXBFS:49
for G being finite _Graph holds dom (((LexBFS:CSeq G) .Result()) `1) = the_Vertices_of G
proofend;

:: [WP: ] Lexicographic_breadth-first_search
theorem Th50: :: LEXBFS:50
for G being finite _Graph holds (((LexBFS:CSeq G) .Result()) `1) " is VertexScheme of G
proofend;

:: A vertex with a vlabel of k must have had the largest v2label when chosen
theorem Th51: :: LEXBFS:51
for G being finite _Graph
for i, j being Nat
for a, b being Vertex of G st a in dom (((LexBFS:CSeq G) . i) `1) &amp; b in dom (((LexBFS:CSeq G) . i) `1) &amp; (((LexBFS:CSeq G) . i) `1) . a < (((LexBFS:CSeq G) . i) `1) . b &amp; 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
proofend;

:: Any value in our v2label corresponds to a vertex that we are
:: adjacent to in our in our vlabel
theorem Th52: :: LEXBFS:52
for G being finite _Graph
for i, j being Nat
for v being Vertex of G st j in (((LexBFS:CSeq G) . i) `2) . v holds
ex w being Vertex of G st
( w in dom (((LexBFS:CSeq G) . i) `1) &amp; (((LexBFS:CSeq G) . i) `1) . w = j &amp; v in G .AdjacentSet {w} )
proofend;

definition
let G be _Graph;
let F be PartFunc of (the_Vertices_of G),NAT;
attrF is with_property_L3  means :Def18: :: LEXBFS:def 18
 for a, b, c being Vertex of G st a in dom F &amp; b in dom F &amp; c in dom F &amp; F . a < F . b &amp; F . b < F . c &amp; a,c are_adjacent &amp; not b,c are_adjacent holds
ex d being Vertex of G st
( d in dom F &amp; F . c < F . d &amp; b,d are_adjacent &amp; not a,d are_adjacent &amp; ( for e being Vertex of G st e <> d &amp; e,b are_adjacent &amp; not e,a are_adjacent holds
F . e < F . d ) );
end;

:: deftheorem Def18 defines with_property_L3 LEXBFS:def_18_:_
 for G being _Graph
for F being PartFunc of (the_Vertices_of G),NAT holds
( F is with_property_L3 iff for a, b, c being Vertex of G st a in dom F &amp; b in dom F &amp; c in dom F &amp; F . a < F . b &amp; F . b < F . c &amp; a,c are_adjacent &amp; not b,c are_adjacent holds
ex d being Vertex of G st
( d in dom F &amp; F . c < F . d &amp; b,d are_adjacent &amp; not a,d are_adjacent &amp; ( for e being Vertex of G st e <> d &amp; e,b are_adjacent &amp; not e,a are_adjacent holds
F . e < F . d ) ) );

theorem Th53: :: LEXBFS:53
for G being finite _Graph
for n being Nat holds ((LexBFS:CSeq G) . n) `1 is with_property_L3
proofend;

theorem Th54: :: LEXBFS:54
for G being finite chordal _Graph
for L being PartFunc of (the_Vertices_of G),NAT st L is with_property_L3 &amp; dom L = the_Vertices_of G holds
for V being VertexScheme of G st V " = L holds
V is perfect
proofend;

theorem :: LEXBFS:55
for G being finite chordal _Graph holds (((LexBFS:CSeq G) .Result()) `1) " is perfect VertexScheme of G
proofend;

begin

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)];
coherence
 [{},((the_Vertices_of G) --> 0)] is MCS:Labeling of G
proofend;
end;

:: deftheorem  defines MCS:Init LEXBFS:def_19_:_
 for G being finite _Graph holds MCS:Init G = [{},((the_Vertices_of G) --> 0)];

definition
let G be finite _Graph;
let L be MCS:Labeling of G;
func MCS:PickUnnumbered L ->  Vertex of G means :Def20: :: LEXBFS:def 20
it = choose (the_Vertices_of G) if  dom (L `1) = the_Vertices_of G
otherwise  ex S being non empty natural-membered finite set ex F being Function st
( S = rng F &amp; F = (L `2) | ((the_Vertices_of G) \ (dom (L `1))) &amp; it = choose (F " {(max S)}) );
existence
 ( ( dom (L `1) = the_Vertices_of G implies ex b1 being Vertex of G st b1 = choose (the_Vertices_of G) ) &amp; ( not dom (L `1) = the_Vertices_of G implies ex b1 being Vertex of G ex S being non empty natural-membered finite set ex F being Function st
( S = rng F &amp; F = (L `2) | ((the_Vertices_of G) \ (dom (L `1))) &amp; b1 = choose (F " {(max S)}) ) ) )
proofend;
uniqueness
 for b1, b2 being Vertex of G holds
( ( dom (L `1) = the_Vertices_of G &amp; b1 = choose (the_Vertices_of G) &amp; b2 = choose (the_Vertices_of G) implies b1 = b2 ) &amp; ( not dom (L `1) = the_Vertices_of G &amp; ex S being non empty natural-membered finite set ex F being Function st
( S = rng F &amp; F = (L `2) | ((the_Vertices_of G) \ (dom (L `1))) &amp; b1 = choose (F " {(max S)}) ) &amp; ex S being non empty natural-membered finite set ex F being Function st
( S = rng F &amp; F = (L `2) | ((the_Vertices_of G) \ (dom (L `1))) &amp; b2 = choose (F " {(max S)}) ) implies b1 = b2 ) ) ;
consistency
 for b1 being Vertex of G holds verum ;
end;

:: deftheorem Def20 defines MCS:PickUnnumbered LEXBFS:def_20_:_
 for G being finite _Graph
for L being MCS:Labeling of G
for b3 being Vertex of G holds
( ( dom (L `1) = the_Vertices_of G implies ( b3 = MCS:PickUnnumbered L iff b3 = choose (the_Vertices_of G) ) ) &amp; ( not dom (L `1) = the_Vertices_of G implies ( b3 = MCS:PickUnnumbered L iff ex S being non empty natural-membered finite set ex F being Function st
( S = rng F &amp; F = (L `2) | ((the_Vertices_of G) \ (dom (L `1))) &amp; b3 = choose (F " {(max S)}) ) ) ) );

definition
let G be finite _Graph;
let L be MCS:Labeling of G;
let 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))];
coherence
 [(L `1),((L `2) .incSubset (((G .AdjacentSet {v}) \ (dom (L `1))),1))] is MCS:Labeling of G
proofend;
end;

:: deftheorem  defines MCS:LabelAdjacent LEXBFS:def_21_:_
 for G being finite _Graph
for L being MCS:Labeling of G
for v being set holds MCS:LabelAdjacent (L,v) = [(L `1),((L `2) .incSubset (((G .AdjacentSet {v}) \ (dom (L `1))),1))];

definition
let G be finite _Graph;
let L be MCS:Labeling of G;
let v be Vertex of G;
let n be Nat;
func MCS:Update (L,v,n) ->  MCS:Labeling of G means :Def22: :: LEXBFS:def 22
 ex M being MCS:Labeling of G st
( M = [((L `1) +* (v .--> ((G .order()) -' n))),(L `2)] &amp; it = MCS:LabelAdjacent (M,v) );
existence
 ex b1, M being MCS:Labeling of G st
( M = [((L `1) +* (v .--> ((G .order()) -' n))),(L `2)] &amp; b1 = MCS:LabelAdjacent (M,v) )
proofend;
uniqueness
 for b1, b2 being MCS:Labeling of G st ex M being MCS:Labeling of G st
( M = [((L `1) +* (v .--> ((G .order()) -' n))),(L `2)] &amp; b1 = MCS:LabelAdjacent (M,v) ) &amp; ex M being MCS:Labeling of G st
( M = [((L `1) +* (v .--> ((G .order()) -' n))),(L `2)] &amp; b2 = MCS:LabelAdjacent (M,v) ) holds
b1 = b2 ;
end;

:: deftheorem Def22 defines MCS:Update LEXBFS:def_22_:_
 for G being finite _Graph
for L being MCS:Labeling of G
for v being Vertex of G
for n being Nat
for b5 being MCS:Labeling of G holds
( b5 = MCS:Update (L,v,n) iff ex M being MCS:Labeling of G st
( M = [((L `1) +* (v .--> ((G .order()) -' n))),(L `2)] &amp; b5 = MCS:LabelAdjacent (M,v) ) );

definition
let G be finite _Graph;
let L be MCS:Labeling of G;
func MCS:Step L ->  MCS:Labeling of G equals :Def23: :: LEXBFS:def 23
L if G .order() <= card (dom (L `1))
otherwise  MCS:Update (L,(MCS:PickUnnumbered L),(card (dom (L `1))));
coherence
 ( ( G .order() <= card (dom (L `1)) implies L is MCS:Labeling of G ) &amp; ( not G .order() <= card (dom (L `1)) implies MCS:Update (L,(MCS:PickUnnumbered L),(card (dom (L `1)))) is MCS:Labeling of G ) ) ;
consistency
 for b1 being MCS:Labeling of G holds verum ;
end;

:: deftheorem Def23 defines MCS:Step LEXBFS:def_23_:_
 for G being finite _Graph
for L being MCS:Labeling of G holds
( ( G .order() <= card (dom (L `1)) implies MCS:Step L = L ) &amp; ( not G .order() <= card (dom (L `1)) implies MCS:Step L = MCS:Update (L,(MCS:PickUnnumbered L),(card (dom (L `1)))) ) );

definition
let G be _Graph;
mode MCS:LabelingSeq of G ->  ManySortedSet of NAT  means :Def24: :: LEXBFS:def 24
 for n being Nat holds it . n is MCS:Labeling of G;
existence
 ex b1 being ManySortedSet of NAT st
for n being Nat holds b1 . n is MCS:Labeling of G
proofend;
end;

:: deftheorem Def24 defines MCS:LabelingSeq LEXBFS:def_24_:_
 for G being _Graph
for b2 being ManySortedSet of NAT holds
( b2 is MCS:LabelingSeq of G iff for n being Nat holds b2 . n is MCS:Labeling of G );

definition
let G be _Graph;
let S be MCS:LabelingSeq of G;
let n be Nat;
:: original:.
redefine funcS . n ->  MCS:Labeling of G;
coherence
 S . n is MCS:Labeling of G by Def24;
end;

definition
let G be _Graph;
let S be MCS:LabelingSeq of G;
:: original:.Result()
redefine funcS .Result()  ->  MCS:Labeling of G;
coherence
 S .Result() is MCS:Labeling of G by Def24;
end;

definition
let G be finite _Graph;
let S be MCS:LabelingSeq of G;
funcS ``1  ->  preVNumberingSeq of G means :Def25: :: LEXBFS:def 25
 for n being Nat holds it . n = (S . n) `1 ;
existence
 ex b1 being preVNumberingSeq of G st
for n being Nat holds b1 . n = (S . n) `1
proofend;
uniqueness
 for b1, b2 being preVNumberingSeq of G st ( for n being Nat holds b1 . n = (S . n) `1 ) &amp; ( for n being Nat holds b2 . n = (S . n) `1 ) holds
b1 = b2
proofend;
end;

:: deftheorem Def25 defines ``1 LEXBFS:def_25_:_
 for G being finite _Graph
for S being MCS:LabelingSeq of G
for b3 being preVNumberingSeq of G holds
( b3 = S ``1 iff for n being Nat holds b3 . n = (S . n) `1 );

definition
let G be finite _Graph;
func MCS:CSeq G ->  MCS:LabelingSeq of G means :Def26: :: LEXBFS:def 26
( it . 0 = MCS:Init G &amp; ( for n being Nat holds it . (n + 1) = MCS:Step (it . n) ) );
existence
 ex b1 being MCS:LabelingSeq of G st
( b1 . 0 = MCS:Init G &amp; ( for n being Nat holds b1 . (n + 1) = MCS:Step (b1 . n) ) )
proofend;
uniqueness
 for b1, b2 being MCS:LabelingSeq of G st b1 . 0 = MCS:Init G &amp; ( for n being Nat holds b1 . (n + 1) = MCS:Step (b1 . n) ) &amp; b2 . 0 = MCS:Init G &amp; ( for n being Nat holds b2 . (n + 1) = MCS:Step (b2 . n) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def26 defines MCS:CSeq LEXBFS:def_26_:_
 for G being finite _Graph
for b2 being MCS:LabelingSeq of G holds
( b2 = MCS:CSeq G iff ( b2 . 0 = MCS:Init G &amp; ( for n being Nat holds b2 . (n + 1) = MCS:Step (b2 . n) ) ) );

theorem Th56: :: LEXBFS:56
for G being finite _Graph holds MCS:CSeq G is iterative
proofend;

registration
let G be finite _Graph;
cluster MCS:CSeq G ->  iterative ;
coherence
 MCS:CSeq G is iterative by Th56;
end;

theorem Th57: :: LEXBFS:57
for G being finite _Graph
for v being set holds ((MCS:Init G) `2) . v = 0
proofend;

theorem Th58: :: LEXBFS:58
for G being finite _Graph
for L being MCS:Labeling of G
for x being set st not x in dom (L `1) &amp; dom (L `1) <> the_Vertices_of G holds
(L `2) . x <= (L `2) . (MCS:PickUnnumbered L)
proofend;

theorem Th59: :: LEXBFS:59
for G being finite _Graph
for L being MCS:Labeling of G st dom (L `1) <> the_Vertices_of G holds
not MCS:PickUnnumbered L in dom (L `1)
proofend;

theorem Th60: :: LEXBFS:60
for G being finite _Graph
for L being MCS:Labeling of G
for v, x being set st not x in G .AdjacentSet {v} holds
(L `2) . x = ((MCS:LabelAdjacent (L,v)) `2) . x
proofend;

theorem Th61: :: LEXBFS:61
for G being finite _Graph
for L being MCS:Labeling of G
for v, x being set st x in dom (L `1) holds
(L `2) . x = ((MCS:LabelAdjacent (L,v)) `2) . x
proofend;

theorem Th62: :: LEXBFS:62
for G being finite _Graph
for L being MCS:Labeling of G
for v, x being set st x in dom (L `2) &amp; x in G .AdjacentSet {v} &amp; not x in dom (L `1) holds
((MCS:LabelAdjacent (L,v)) `2) . x = ((L `2) . x) + 1
proofend;

theorem :: LEXBFS:63
for G being finite _Graph
for L being MCS:Labeling of G
for v being set st dom (L `2) = the_Vertices_of G holds
dom ((MCS:LabelAdjacent (L,v)) `2) = the_Vertices_of G
proofend;

theorem Th64: :: LEXBFS:64
for G being finite _Graph
for 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)))))
proofend;

theorem Th65: :: LEXBFS:65
for G being finite _Graph
for n being Nat st n <= G .order() holds
card (dom (((MCS:CSeq G) . n) `1)) = n
proofend;

theorem Th66: :: LEXBFS:66
for G being finite _Graph
for n being Nat st G .order() <= n holds
(MCS:CSeq G) . (G .order()) = (MCS:CSeq G) . n
proofend;

theorem Th67: :: LEXBFS:67
for G being finite _Graph
for m, n being Nat st G .order() <= m &amp; m <= n holds
(MCS:CSeq G) . m = (MCS:CSeq G) . n
proofend;

theorem Th68: :: LEXBFS:68
for G being finite _Graph holds MCS:CSeq G is eventually-constant
proofend;

registration
let G be finite _Graph;
cluster MCS:CSeq G ->  eventually-constant ;
coherence
 MCS:CSeq G is eventually-constant by Th68;
end;

theorem Th69: :: LEXBFS:69
for G being finite _Graph
for n being Nat holds
( dom (((MCS:CSeq G) . n) `1) = the_Vertices_of G iff G .order() <= n )
proofend;

theorem Th70: :: LEXBFS:70
for G being finite _Graph holds (MCS:CSeq G) .Lifespan() = G .order()
proofend;

theorem Th71: :: LEXBFS:71
for G being finite _Graph holds (MCS:CSeq G) ``1 is eventually-constant
proofend;

theorem Th72: :: LEXBFS:72
for G being finite _Graph holds ((MCS:CSeq G) ``1) .Lifespan() = (MCS:CSeq G) .Lifespan()
proofend;

theorem Th73: :: LEXBFS:73
for G being finite _Graph holds (MCS:CSeq G) ``1 is vertex-numbering
proofend;

registration
let G be finite _Graph;
cluster(MCS:CSeq G) ``1  ->  vertex-numbering ;
coherence
 (MCS:CSeq G) ``1 is vertex-numbering by Th73;
end;

theorem Th74: :: LEXBFS:74
for G being finite _Graph
for n being Nat st n < G .order() holds
((MCS:CSeq G) ``1) .PickedAt n = MCS:PickUnnumbered ((MCS:CSeq G) . n)
proofend;

theorem Th75: :: LEXBFS:75
for G being finite _Graph
for n being Nat st n < G .order() holds
ex w being Vertex of G st
( w = MCS:PickUnnumbered ((MCS:CSeq G) . n) &amp; ( for v being set holds
( ( v in G .AdjacentSet {w} &amp; not v in dom (((MCS:CSeq G) . n) `1) implies (((MCS:CSeq G) . (n + 1)) `2) . v = ((((MCS:CSeq G) . n) `2) . v) + 1 ) &amp; ( ( 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 ) ) ) )
proofend;

theorem Th76: :: LEXBFS:76
for G being finite _Graph
for n being Nat
for 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)))
proofend;

definition
let G be _Graph;
let F be PartFunc of (the_Vertices_of G),NAT;
attrF is with_property_T  means :Def27: :: LEXBFS:def 27
 for a, b, c being Vertex of G st a in dom F &amp; b in dom F &amp; c in dom F &amp; F . a < F . b &amp; F . b < F . c &amp; a,c are_adjacent &amp; not b,c are_adjacent holds
ex d being Vertex of G st
( d in dom F &amp; F . b < F . d &amp; b,d are_adjacent &amp; not a,d are_adjacent );
end;

:: deftheorem Def27 defines with_property_T LEXBFS:def_27_:_
 for G being _Graph
for F being PartFunc of (the_Vertices_of G),NAT holds
( F is with_property_T iff for a, b, c being Vertex of G st a in dom F &amp; b in dom F &amp; c in dom F &amp; F . a < F . b &amp; F . b < F . c &amp; a,c are_adjacent &amp; not b,c are_adjacent holds
ex d being Vertex of G st
( d in dom F &amp; F . b < F . d &amp; b,d are_adjacent &amp; not a,d are_adjacent ) );

theorem :: LEXBFS:77
for G being finite _Graph
for n being Nat holds ((MCS:CSeq G) . n) `1 is with_property_T
proofend;

theorem :: LEXBFS:78
for G being finite _Graph holds ((LexBFS:CSeq G) .Result()) `1 is with_property_T
proofend;

theorem :: LEXBFS:79
for G being finite chordal _Graph
for L being PartFunc of (the_Vertices_of G),NAT st L is with_property_T &amp; dom L = the_Vertices_of G holds
for V being VertexScheme of G st V " = L holds
V is perfect
proofend;