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


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

proof end;

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

proof end;

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

Lm3: for a, b, c being Real st a < b holds
(c - b) + 1 < (c - a) + 1

proof end;

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

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 & b1 is finite & b1 is with_finite-elements )
proof end;
end;

definition
let f, g be Function;
func f .\/ g -> Function means :Def1: :: 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) ) );
existence
ex b1 being Function st
( dom b1 = (dom f) \/ (dom g) & ( for x being object st x in (dom f) \/ (dom g) holds
b1 . x = (f . x) \/ (g . x) ) )
proof end;
uniqueness
for b1, b2 being Function st dom b1 = (dom f) \/ (dom g) & ( for x being object st x in (dom f) \/ (dom g) holds
b1 . x = (f . x) \/ (g . x) ) & dom b2 = (dom f) \/ (dom g) & ( for x being object st x in (dom f) \/ (dom g) holds
b2 . x = (f . x) \/ (g . x) ) holds
b1 = b2
proof end;
end;

:: deftheorem LEXBFS:def 1 :
canceled;

:: deftheorem Def1 defines .\/ LEXBFS:def 2 :
for f, g, b3 being Function holds
( b3 = f .\/ g iff ( dom b3 = (dom f) \/ (dom g) & ( for x being object 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 & m <= k ) )
proof end;

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

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

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

:: deftheorem Def2 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 & b1 is natsubset-yielding )
proof end;
end;

definition
let f be finite-yielding natsubset-yielding Function;
let x be set ;
:: original: .
redefine func f . x -> finite Subset of NAT;
coherence
f . x is finite Subset of NAT
proof end;
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
proof end;

definition
let F be natural-valued Function;
let S be set ;
let k be Nat;
func F .incSubset (S,k) -> natural-valued Function means :Def3: :: 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 ) ) ) );
existence
ex b1 being natural-valued Function st
( dom b1 = dom F & ( for y being object holds
( ( y in S & y in dom F implies b1 . y = (F . y) + k ) & ( not y in S implies b1 . y = F . y ) ) ) )
proof end;
uniqueness
for b1, b2 being natural-valued Function st dom b1 = dom F & ( for y being object holds
( ( y in S & y in dom F implies b1 . y = (F . y) + k ) & ( not y in S implies b1 . y = F . y ) ) ) & dom b2 = dom F & ( for y being object holds
( ( y in S & y in dom F implies b2 . y = (F . y) + k ) & ( not y in S implies b2 . y = F . y ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 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 & ( for y being object holds
( ( y in S & y in dom F implies b4 . y = (F . y) + k ) & ( 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 :Def4: :: LEXBFS:def 5
( it in B & ( 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 & ( for x being bag of n st x in B holds
x <= b1,T ) )
proof end;
uniqueness
for b1, b2 being bag of n st b1 in B & ( for x being bag of n st x in B holds
x <= b1,T ) & b2 in B & ( for x being bag of n st x in B holds
x <= b2,T ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 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 & ( 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
proof end;
end;

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

proof end;

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

proof end;

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

proof end;

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

:: deftheorem Def5 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 ;
attr S is eventually-constant means :Def6: :: LEXBFS:def 7
ex n being Nat st
for m being Nat st n <= m holds
S . n = S . m;
end;

:: deftheorem Def6 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 & b1 is iterative & b1 is eventually-constant )
proof end;
end;

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

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

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

theorem Th10: :: 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
proof end;

definition
let G be _finite _Graph;
mode preVNumberingSeq of G -> ManySortedSet of NAT means :Def7: :: 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
proof end;
end;

:: deftheorem Def7 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 func S . n -> PartFunc of (the_Vertices_of G),NAT;
coherence
S . n is PartFunc of (the_Vertices_of G),NAT
by Def7;
end;

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

:: deftheorem Def8 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 = {} & S is iterative & S is halting & S .Lifespan() = G .order() & ( for n being Nat st n < S .Lifespan() holds
ex w being Vertex of G st
( not w in dom (S . n) & 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
proof end;
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 & b1 is iterative )
;
;
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;
func S .PickedAt n -> set means :Def9: :: 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)) );
existence
( ( n >= S .Lifespan() implies ex b1 being set st b1 = the Element of the_Vertices_of G ) & ( not n >= S .Lifespan() implies ex b1 being set st
( not b1 in dom (S . n) & S . (n + 1) = (S . n) +* (b1 .--> ((S .Lifespan()) -' n)) ) ) )
proof end;
uniqueness
for b1, b2 being set holds
( ( n >= S .Lifespan() & b1 = the Element of the_Vertices_of G & b2 = the Element of the_Vertices_of G implies b1 = b2 ) & ( not n >= S .Lifespan() & not b1 in dom (S . n) & S . (n + 1) = (S . n) +* (b1 .--> ((S .Lifespan()) -' n)) & not b2 in dom (S . n) & S . (n + 1) = (S . n) +* (b2 .--> ((S .Lifespan()) -' n)) implies b1 = b2 ) )
proof end;
consistency
for b1 being set holds verum
;
end;

:: deftheorem Def9 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 = the Element of the_Vertices_of G ) ) & ( not n >= S .Lifespan() implies ( b4 = S .PickedAt n iff ( not b4 in dom (S . n) & 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)) & dom (S . (n + 1)) = (dom (S . n)) \/ {(S .PickedAt n)} )
proof end;

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

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

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

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() & ( x in dom (S . n) implies 1 <= (S . n) . x ) )
proof end;

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 & m <= S .Lifespan() holds
ex v being Vertex of G st
( v in dom (S . n) & (S . n) . v = m )
proof end;

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

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

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) & v in dom (S . n) holds
(S . m) . v = (S . n) . v
proof end;

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) & (S . m) . v = n holds
S .PickedAt ((S .Lifespan()) -' n) = v
proof end;

theorem Th21: :: LEXBFS:21
for G being _finite _Graph
for S being VNumberingSeq of G
for 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 )
proof end;

:: 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 & (S .Lifespan()) -' m < (S . m) . v )
proof end;

:: 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) & b in dom (S . i) & (S . i) . a < (S . i) . b holds
b in dom (S . ((S .Lifespan()) -' ((S . i) . a)))
proof end;

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) & (S . i) . a < (S . i) . b holds
not a in dom (S . ((S .Lifespan()) -' ((S . i) . b)))
proof end;

definition
let X1, X3 be set ;
let X2 be non empty set ;
let x be Element of [:(PFuncs (X1,X3)),X2:];
:: original: `1
redefine func x `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 func x `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;
cluster L `1 -> finite for set ;
coherence
for b1 being set st b1 = L `1 holds
b1 is finite
proof end;
cluster L `2 -> finite for set ;
coherence
for b1 being set st b1 = L `2 holds
b1 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
proof end;
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 :Def11: :: 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) ex B being non empty finite Subset of (Bags NAT) ex F being Function st
( S = rng F & F = (L `2) | ((the_Vertices_of G) \ (dom (L `1))) & ( for x being finite Subset of NAT st x in S holds
(x,1) -bag in B ) & ( for x being set st x in B holds
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))))} );
existence
( ( dom (L `1) = the_Vertices_of G implies ex b1 being Vertex of G st b1 = the Element of the_Vertices_of G ) & ( 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 & F = (L `2) | ((the_Vertices_of G) \ (dom (L `1))) & ( for x being finite Subset of NAT st x in S holds
(x,1) -bag in B ) & ( for x being set st x in B holds
ex y being finite Subset of NAT st
( y in S & x = (y,1) -bag ) ) & b1 = the Element of F " {(support (max (B,(InvLexOrder NAT))))} ) ) )
proof end;
uniqueness
for b1, b2 being Vertex of G holds
( ( dom (L `1) = the_Vertices_of G & b1 = the Element of the_Vertices_of G & b2 = the Element of the_Vertices_of G implies b1 = b2 ) & ( not dom (L `1) = the_Vertices_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 & F = (L `2) | ((the_Vertices_of G) \ (dom (L `1))) & ( for x being finite Subset of NAT st x in S holds
(x,1) -bag in B ) & ( for x being set st x in B holds
ex y being finite Subset of NAT st
( y in S & x = (y,1) -bag ) ) & b1 = the Element of F " {(support (max (B,(InvLexOrder NAT))))} ) & 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 & F = (L `2) | ((the_Vertices_of G) \ (dom (L `1))) & ( for x being finite Subset of NAT st x in S holds
(x,1) -bag in B ) & ( for x being set st x in B holds
ex y being finite Subset of NAT st
( y in S & x = (y,1) -bag ) ) & b2 = the Element of F " {(support (max (B,(InvLexOrder NAT))))} ) implies b1 = b2 ) )
proof end;
consistency
for b1 being Vertex of G holds verum
;
end;

:: deftheorem Def11 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 = the Element of the_Vertices_of G ) ) & ( 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 & F = (L `2) | ((the_Vertices_of G) \ (dom (L `1))) & ( for x being finite Subset of NAT st x in S holds
(x,1) -bag in B ) & ( for x being set st x in B holds
ex y being finite Subset of NAT st
( y in S & x = (y,1) -bag ) ) & b3 = the Element of 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
proof end;
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
proof end;

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

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} & not x in dom (L `1) holds
((LexBFS:Update (L,v,k)) `2) . x = ((L `2) . x) \/ {((G .order()) -' k)}
proof end;

definition
let G be _finite _Graph;
let L be LexBFS:Labeling of G;
func LexBFS:Step L -> LexBFS:Labeling of G equals :Def13: :: 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 ) & ( 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 Def13 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 ) & ( 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 :Def14: :: 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
proof end;
end;

:: deftheorem Def14 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 func S . n -> LexBFS:Labeling of G;
coherence
S . n is LexBFS:Labeling of G
by Def14;
end;

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

definition
let G be _finite _Graph;
let S be LexBFS:LabelingSeq of G;
func S ``1 -> preVNumberingSeq of G means :Def15: :: 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
proof end;
uniqueness
for b1, b2 being preVNumberingSeq of G st ( for n being Nat holds b1 . n = (S . n) `1 ) & ( for n being Nat holds b2 . n = (S . n) `1 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def15 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 :Def16: :: LEXBFS:def 17
( it . 0 = LexBFS:Init G & ( 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 & ( for n being Nat holds b1 . (n + 1) = LexBFS:Step (b1 . n) ) )
proof end;
uniqueness
for b1, b2 being LexBFS:LabelingSeq of G st b1 . 0 = LexBFS:Init G & ( for n being Nat holds b1 . (n + 1) = LexBFS:Step (b1 . n) ) & b2 . 0 = LexBFS:Init G & ( for n being Nat holds b2 . (n + 1) = LexBFS:Step (b2 . n) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def16 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 & ( 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
proof end;

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

definition
let X, Y be set ;
let f be Function of X,(Fin Y);
let x be set ;
:: original: .
redefine func f . x -> finite Subset of Y;
coherence
f . x is finite Subset of Y
proof end;
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) & dom (L `1) <> the_Vertices_of G holds
(((L `2) . x),1) -bag <= (((L `2) . (LexBFS:PickUnnumbered L)),1) -bag , InvLexOrder NAT
proof end;

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

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

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

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

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

theorem Th35: :: LEXBFS:35
for G being _finite _Graph holds LexBFS:CSeq G is eventually-constant
proof end;

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

theorem Th37: :: LEXBFS:37
for G being _finite _Graph holds (LexBFS:CSeq G) .Lifespan() = G .order()
proof end;

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

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

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

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

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

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

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

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

theorem Th45: :: LEXBFS:45
for G being _finite _Graph
for m, n being Nat
for 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
proof end;

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

:: 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 & 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
proof end;

:: 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 & not y in dom (((LexBFS:CSeq G) . ((G .order()) -' n)) `1) & x in G .AdjacentSet {y} )
proof end;

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

:: WP: Lexicographic_breadth-first_search
theorem Th50: :: LEXBFS:50
for G being _finite _Graph holds (((LexBFS:CSeq G) .Result()) `1) " is VertexScheme of G
proof end;

:: 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) & 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
proof end;

:: 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) & (((LexBFS:CSeq G) . i) `1) . w = j & v in G .AdjacentSet {w} )
proof end;

definition
let G be _Graph;
let 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 holds
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;

:: deftheorem 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 & 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 holds
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 ) ) );

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

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 & dom L = the_Vertices_of G holds
for V being VertexScheme of G st V " = L holds
V is perfect
proof end;

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

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
proof end;
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 :Def19: :: LEXBFS:def 20
it = the Element of 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 & F = (L `2) | ((the_Vertices_of G) \ (dom (L `1))) & it = the Element of F " {(max S)} );
existence
( ( dom (L `1) = the_Vertices_of G implies ex b1 being Vertex of G st b1 = the Element of the_Vertices_of G ) & ( 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 & F = (L `2) | ((the_Vertices_of G) \ (dom (L `1))) & b1 = the Element of F " {(max S)} ) ) )
proof end;
uniqueness
for b1, b2 being Vertex of G holds
( ( dom (L `1) = the_Vertices_of G & b1 = the Element of the_Vertices_of G & b2 = the Element of the_Vertices_of G implies b1 = b2 ) & ( not dom (L `1) = the_Vertices_of G & ex S being non empty natural-membered finite set ex F being Function st
( S = rng F & F = (L `2) | ((the_Vertices_of G) \ (dom (L `1))) & b1 = the Element of F " {(max S)} ) & ex S being non empty natural-membered finite set ex F being Function st
( S = rng F & F = (L `2) | ((the_Vertices_of G) \ (dom (L `1))) & b2 = the Element of F " {(max S)} ) implies b1 = b2 ) )
;
consistency
for b1 being Vertex of G holds verum
;
end;

:: deftheorem Def19 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 = the Element of the_Vertices_of G ) ) & ( 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 & F = (L `2) | ((the_Vertices_of G) \ (dom (L `1))) & b3 = the Element of 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
proof end;
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 :Def21: :: 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) );
existence
ex b1, M being MCS:Labeling of G st
( M = [((L `1) +* (v .--> ((G .order()) -' n))),(L `2)] & b1 = MCS:LabelAdjacent (M,v) )
proof end;
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)] & b1 = MCS:LabelAdjacent (M,v) ) & ex M being MCS:Labeling of G st
( M = [((L `1) +* (v .--> ((G .order()) -' n))),(L `2)] & b2 = MCS:LabelAdjacent (M,v) ) holds
b1 = b2
;
end;

:: deftheorem Def21 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)] & 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 :Def22: :: 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 ) & ( 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 Def22 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 ) & ( 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 :Def23: :: 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
proof end;
end;

:: deftheorem Def23 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 func S . n -> MCS:Labeling of G;
coherence
S . n is MCS:Labeling of G
by Def23;
end;

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

definition
let G be _finite _Graph;
let S be MCS:LabelingSeq of G;
func S ``1 -> preVNumberingSeq of G means :Def24: :: 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
proof end;
uniqueness
for b1, b2 being preVNumberingSeq of G st ( for n being Nat holds b1 . n = (S . n) `1 ) & ( for n being Nat holds b2 . n = (S . n) `1 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def24 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 :Def25: :: LEXBFS:def 26
( it . 0 = MCS:Init G & ( 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 & ( for n being Nat holds b1 . (n + 1) = MCS:Step (b1 . n) ) )
proof end;
uniqueness
for b1, b2 being MCS:LabelingSeq of G st b1 . 0 = MCS:Init G & ( for n being Nat holds b1 . (n + 1) = MCS:Step (b1 . n) ) & b2 . 0 = MCS:Init G & ( for n being Nat holds b2 . (n + 1) = MCS:Step (b2 . n) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def25 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 & ( 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
proof end;

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

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

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) & dom (L `1) <> the_Vertices_of G holds
(L `2) . x <= (L `2) . (MCS:PickUnnumbered L)
proof end;

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

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

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

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) & x in G .AdjacentSet {v} & not x in dom (L `1) holds
((MCS:LabelAdjacent (L,v)) `2) . x = ((L `2) . x) + 1
proof end;

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 by Def3;

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

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

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

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

theorem Th68: :: LEXBFS:68
for G being _finite _Graph holds MCS:CSeq G is eventually-constant
proof end;

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

theorem Th70: :: LEXBFS:70
for G being _finite _Graph holds (MCS:CSeq G) .Lifespan() = G .order()
proof end;

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

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

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

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

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

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

definition
let G be _Graph;
let 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 holds
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;

:: deftheorem 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 & 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 holds
ex d being Vertex of G st
( d in dom F & F . b < F . d & b,d are_adjacent & 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
proof end;

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

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 & dom L = the_Vertices_of G holds
for V being VertexScheme of G st V " = L holds
V is perfect
proof end;