:: 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 b₁ being Subset of (bool NAT) st
( not b₁ is empty & b₁ is finite & b₁ 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 b₁ being Function st
( dom b₁ = (dom f) \/ (dom g) & ( for x being object st x in (dom f) \/ (dom g) holds
b₁ . x = (f . x) \/ (g . x) ) )

proof end;

uniqueness
for b₁, b₂ being Function st dom b₁ = (dom f) \/ (dom g) & ( for x being object st x in (dom f) \/ (dom g) holds
b₁ . x = (f . x) \/ (g . x) ) & dom b₂ = (dom f) \/ (dom g) & ( for x being object st x in (dom f) \/ (dom g) holds
b₂ . x = (f . x) \/ (g . x) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem LEXBFS:def 1 :
canceled;

:: deftheorem Def1 defines .\/ LEXBFS:def 2 :
for f, g, b₃ being Function holds
( b₃ = f .\/ g iff ( dom b₃ = (dom f) \/ (dom g) & ( for x being object st x in (dom f) \/ (dom g) holds
b₃ . 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 b₁ being Function st
( b₁ is finite-yielding & b₁ 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 b₁ being natural-valued Function st
( dom b₁ = dom F & ( for y being object holds
( ( y in S & y in dom F implies b₁ . y = (F . y) + k ) & ( not y in S implies b₁ . y = F . y ) ) ) )

proof end;

uniqueness
for b₁, b₂ being natural-valued Function st dom b₁ = dom F & ( for y being object holds
( ( y in S & y in dom F implies b₁ . y = (F . y) + k ) & ( not y in S implies b₁ . y = F . y ) ) ) & dom b₂ = dom F & ( for y being object holds
( ( y in S & y in dom F implies b₂ . y = (F . y) + k ) & ( not y in S implies b₂ . y = F . y ) ) ) holds
b₁ = b₂

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 b₄ being natural-valued Function holds
( b₄ = F .incSubset (S,k) iff ( dom b₄ = dom F & ( for y being object holds
( ( y in S & y in dom F implies b₄ . y = (F . y) + k ) & ( not y in S implies b₄ . 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 b₁ being bag of n st
( b₁ in B & ( for x being bag of n st x in B holds
x <= b₁,T ) )

proof end;

uniqueness
for b₁, b₂ being bag of n st b₁ in B & ( for x being bag of n st x in B holds
x <= b₁,T ) & b₂ in B & ( for x being bag of n st x in B holds
x <= b₂,T ) holds
b₁ = b₂

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 b₄ being bag of n holds
( b₄ = max (B,T) iff ( b₄ in B & ( for x being bag of n st x in B holds
x <= b₄,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 b₁ being ManySortedSet of NAT st
( b₁ is halting & b₁ is iterative & b₁ 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 b₁ being ManySortedSet of NAT st b₁ is halting & b₁ is iterative holds
b₁ 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 b₁ being ManySortedSet of NAT st b₁ is eventually-constant holds
b₁ 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 b₁ being ManySortedSet of NAT st
for i being Nat holds b₁ . 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 b₂ being ManySortedSet of NAT holds
( b₂ is preVNumberingSeq of G iff for i being Nat holds b₂ . 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 b₁ being preVNumberingSeq of G st b₁ 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 b₁ being preVNumberingSeq of G st b₁ is vertex-numbering holds
( b₁ is halting & b₁ 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 b₁ being set st b₁ = the Element of the_Vertices_of G ) & ( not n >= S .Lifespan() implies ex b₁ being set st
( not b₁ in dom (S . n) & S . (n + 1) = (S . n) +* (b₁ .--> ((S .Lifespan()) -' n)) ) ) )

proof end;

uniqueness
for b₁, b₂ being set holds
( ( n >= S .Lifespan() & b₁ = the Element of the_Vertices_of G & b₂ = the Element of the_Vertices_of G implies b₁ = b₂ ) & ( not n >= S .Lifespan() & not b₁ in dom (S . n) & S . (n + 1) = (S . n) +* (b₁ .--> ((S .Lifespan()) -' n)) & not b₂ in dom (S . n) & S . (n + 1) = (S . n) +* (b₂ .--> ((S .Lifespan()) -' n)) implies b₁ = b₂ ) )

proof end;

consistency
for b₁ 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 b₄ being set holds
( ( n >= S .Lifespan() implies ( b₄ = S .PickedAt n iff b₄ = the Element of the_Vertices_of G ) ) & ( not n >= S .Lifespan() implies ( b₄ = S .PickedAt n iff ( not b₄ in dom (S . n) & S . (n + 1) = (S . n) +* (b₄ .--> ((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 b₁ being set st b₁ = L `1 holds
b₁ is finite

proof end;

cluster L `2 -> finite for set ;

coherence
for b₁ being set st b₁ = L `2 holds
b₁ 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 b<sub>1</sub> being Vertex of G st b<sub>1</sub> = the Element of the_Vertices_of G ) & ( not dom (L `1) = the_Vertices_of G implies ex b₁ 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 ) ) & b₁ = the Element of F " {(support (max (B,(InvLexOrder NAT))))} ) ) )

proof end;

uniqueness
for b₁, b₂ being Vertex of G holds
( ( dom (L `1) = the_Vertices_of G & b<sub>1</sub> = the Element of the_Vertices_of G & b<sub>2</sub> = the Element of the_Vertices_of G implies b<sub>1</sub> = b<sub>2</sub> ) & ( 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 ) ) & b₁ = 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 ) ) & b₂ = the Element of F " {(support (max (B,(InvLexOrder NAT))))} ) implies b₁ = b₂ ) )

proof end;

consistency
for b₁ 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 b₃ being Vertex of G holds
( ( dom (L `1) = the_Vertices_of G implies ( b<sub>3</sub> = LexBFS:PickUnnumbered L iff b<sub>3</sub> = the Element of the_Vertices_of G ) ) & ( not dom (L `1) = the_Vertices_of G implies ( b₃ = 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 ) ) & b₃ = 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 b₁ 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 b₁ being ManySortedSet of NAT st
for n being Nat holds b₁ . n is LexBFS:Labeling of G

proof end;

end;

:: deftheorem Def14 defines LexBFS:LabelingSeq LEXBFS:def 15 :
for G being _Graph
for b₂ being ManySortedSet of NAT holds
( b₂ is LexBFS:LabelingSeq of G iff for n being Nat holds b₂ . 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 b₁ being preVNumberingSeq of G st
for n being Nat holds b₁ . n = (S . n) `1

proof end;

uniqueness
for b₁, b₂ being preVNumberingSeq of G st ( for n being Nat holds b₁ . n = (S . n) `1 ) & ( for n being Nat holds b<sub>2</sub> . n = (S . n) `1 ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def15 defines ``1 LEXBFS:def 16 :
for G being _finite _Graph
for S being LexBFS:LabelingSeq of G
for b<sub>3</sub> being preVNumberingSeq of G holds
( b<sub>3</sub> = S ``1 iff for n being Nat holds b₃ . 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 b₁ being LexBFS:LabelingSeq of G st
( b₁ . 0 = LexBFS:Init G & ( for n being Nat holds b₁ . (n + 1) = LexBFS:Step (b₁ . n) ) )

proof end;

uniqueness
for b₁, b₂ being LexBFS:LabelingSeq of G st b₁ . 0 = LexBFS:Init G & ( for n being Nat holds b₁ . (n + 1) = LexBFS:Step (b₁ . n) ) & b₂ . 0 = LexBFS:Init G & ( for n being Nat holds b₂ . (n + 1) = LexBFS:Step (b₂ . n) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def16 defines LexBFS:CSeq LEXBFS:def 17 :
for G being _finite _Graph
for b₂ being LexBFS:LabelingSeq of G holds
( b₂ = LexBFS:CSeq G iff ( b₂ . 0 = LexBFS:Init G & ( for n being Nat holds b₂ . (n + 1) = LexBFS:Step (b₂ . 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;

:: 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 b<sub>1</sub> being Vertex of G st b<sub>1</sub> = the Element of the_Vertices_of G ) & ( not dom (L `1) = the_Vertices_of G implies ex b₁ 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))) & b₁ = the Element of F " {(max S)} ) ) )

proof end;

uniqueness
for b₁, b₂ being Vertex of G holds
( ( dom (L `1) = the_Vertices_of G & b<sub>1</sub> = the Element of the_Vertices_of G & b<sub>2</sub> = the Element of the_Vertices_of G implies b<sub>1</sub> = b<sub>2</sub> ) & ( 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))) & b₁ = 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))) & b₂ = the Element of F " {(max S)} ) implies b₁ = b₂ ) ) ;
consistency
for b₁ 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 b₃ being Vertex of G holds
( ( dom (L `1) = the_Vertices_of G implies ( b<sub>3</sub> = MCS:PickUnnumbered L iff b<sub>3</sub> = the Element of the_Vertices_of G ) ) & ( not dom (L `1) = the_Vertices_of G implies ( b₃ = 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))) & b₃ = 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 b₁, M being MCS:Labeling of G st
( M = [((L `1) +* (v .--> ((G .order()) -' n))),(L `2)] & b₁ = MCS:LabelAdjacent (M,v) )

proof end;

uniqueness
for b₁, b₂ being MCS:Labeling of G st ex M being MCS:Labeling of G st
( M = [((L `1) +* (v .--> ((G .order()) -' n))),(L `2)] & b₁ = MCS:LabelAdjacent (M,v) ) & ex M being MCS:Labeling of G st
( M = [((L `1) +* (v .--> ((G .order()) -' n))),(L `2)] & b₂ = MCS:LabelAdjacent (M,v) ) holds
b₁ = b₂ ;

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 b₅ being MCS:Labeling of G holds
( b₅ = MCS:Update (L,v,n) iff ex M being MCS:Labeling of G st
( M = [((L `1) +* (v .--> ((G .order()) -' n))),(L `2)] & b₅ = 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 b₁ 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 b₁ being ManySortedSet of NAT st
for n being Nat holds b₁ . n is MCS:Labeling of G

proof end;

end;

:: deftheorem Def23 defines MCS:LabelingSeq LEXBFS:def 24 :
for G being _Graph
for b₂ being ManySortedSet of NAT holds
( b₂ is MCS:LabelingSeq of G iff for n being Nat holds b₂ . 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 b₁ being preVNumberingSeq of G st
for n being Nat holds b₁ . n = (S . n) `1

proof end;

uniqueness
for b₁, b₂ being preVNumberingSeq of G st ( for n being Nat holds b₁ . n = (S . n) `1 ) & ( for n being Nat holds b<sub>2</sub> . n = (S . n) `1 ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def24 defines ``1 LEXBFS:def 25 :
for G being _finite _Graph
for S being MCS:LabelingSeq of G
for b<sub>3</sub> being preVNumberingSeq of G holds
( b<sub>3</sub> = S ``1 iff for n being Nat holds b₃ . 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 b₁ being MCS:LabelingSeq of G st
( b₁ . 0 = MCS:Init G & ( for n being Nat holds b₁ . (n + 1) = MCS:Step (b₁ . n) ) )

proof end;

uniqueness
for b₁, b₂ being MCS:LabelingSeq of G st b₁ . 0 = MCS:Init G & ( for n being Nat holds b₁ . (n + 1) = MCS:Step (b₁ . n) ) & b₂ . 0 = MCS:Init G & ( for n being Nat holds b₂ . (n + 1) = MCS:Step (b₂ . n) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def25 defines MCS:CSeq LEXBFS:def 26 :
for G being _finite _Graph
for b₂ being MCS:LabelingSeq of G holds
( b₂ = MCS:CSeq G iff ( b₂ . 0 = MCS:Init G & ( for n being Nat holds b₂ . (n + 1) = MCS:Step (b₂ . 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;