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

TH2: for f being Function st f is one-to-one holds
card (dom f) = card (rng f)

proof end;

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

proof end;

invrngrestr: 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;

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 & w <= A + B ) } = B + 1

proof end;

Lm1: for a, b, c being real number 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;

definition

let S be set ;
attr S is with_finite-elements means :Def1: :: LEXBFS:def 1
for x being Element of S holds x is finite;

end;

:: deftheorem Def1 defines with_finite-elements LEXBFS:def 1 :

for S being set holds
( S is with_finite-elements iff for x being Element of S holds x is finite );

registration

cluster non empty with_finite-elements set ;
existence
ex b₁ being set st
( not b₁ is empty & b₁ is with_finite-elements )

proof end;

cluster non empty finite with_finite-elements 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;

registration

let S be with_finite-elements set ;
cluster -> finite Element of S;
coherence
for b₁ being Element of S holds b₁ is finite by Def1;

end;

definition

let f, g be Function;
func f .\/ g -> Function means :Def2: :: LEXBFS:def 2
( dom it = (dom f) \/ (dom g) & ( for x being set 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 set 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 set st x in (dom f) \/ (dom g) holds
b₁ . x = (f . x) \/ (g . x) ) & dom b₂ = (dom f) \/ (dom g) & ( for x being set st x in (dom f) \/ (dom g) holds
b₂ . x = (f . x) \/ (g . x) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines .\/ LEXBFS:def 2 :

for f, g, b₃ being Function holds
( b₃ = f .\/ g iff ( dom b₃ = (dom f) \/ (dom g) & ( for x being set st x in (dom f) \/ (dom g) holds
b₃ . x = (f . x) \/ (g . x) ) ) );

theorem Th5: :: 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 Th6: :: 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 Th7: :: 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 :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 );

Lm2: for F being Function st ( for x being set st x in rng F holds
x is finite ) holds
F is finite-yielding

proof end;

registration

cluster finite-yielding natsubset-yielding 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 Th8: :: 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 :Def4: :: LEXBFS:def 4
( dom it = dom F & ( for y being set 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 set 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 set 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 set 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 Def4 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 set 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 :Def5: :: 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 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 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 set 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 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 & n in dom (W .addEdge e) )

proof end;

definition

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

end;

:: deftheorem Def15 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 :Def16: :: LEXBFS:def 7
ex n being Nat st
for m being Nat st n <= m holds
S . n = S . m;

end;

:: deftheorem Def16 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 halting iterative eventually-constant ManySortedSet of NAT ;
existence
ex b₁ being ManySortedSet of NAT st
( b₁ is halting & b₁ is iterative & b₁ is eventually-constant )

proof end;

end;

theorem Th14: :: LEXBFS:7

for Gs being ManySortedSet of NAT st Gs is halting & Gs is iterative holds
Gs is eventually-constant

proof end;

registration

cluster halting iterative -> eventually-constant ManySortedSet of NAT ;
coherence
for b₁ being ManySortedSet of NAT st b₁ is halting & b₁ is iterative holds
b₁ is eventually-constant by Th14;

end;

theorem Th15: :: LEXBFS:8

for Gs being ManySortedSet of NAT st Gs is eventually-constant holds
Gs is halting

proof end;

registration

cluster eventually-constant -> halting ManySortedSet of NAT ;
coherence
for b₁ being ManySortedSet of NAT st b₁ is eventually-constant holds
b₁ is halting by Th15;

end;

theorem Th16: :: 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 Th17: :: 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 :dpVNumSeq: :: 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 dpVNumSeq 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 dpVNumSeq;

end;

definition

let G be finite _Graph;
let S be preVNumberingSeq of G;
attr S is vertex-numbering means :dVNumSeq: :: 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 dVNumSeq 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 vertex-numbering preVNumberingSeq of G;
existence
ex b₁ being preVNumberingSeq of G st b₁ is vertex-numbering

proof end;

end;

registration

let G be finite _Graph;
cluster vertex-numbering -> halting iterative preVNumberingSeq of G;
correctness
coherence
for b₁ being preVNumberingSeq of G st b₁ is vertex-numbering holds
( b₁ is halting & b₁ is iterative );
by dVNumSeq;

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 :Def27: :: LEXBFS:def 10
it = choose (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₁ = choose (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₁ = choose (the_Vertices_of G) & b₂ = choose (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 Def27 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₄ = choose (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 Th18: :: 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 Th19: :: 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 Th21: :: 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 Th22: :: 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 Th23: :: 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 Th24: :: 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 Th25: :: 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 Th26: :: 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 Th27: :: 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 Th28: :: 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;

theorem Th29: :: 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;

theorem Th30: :: 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 Th31: :: 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) & b 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 ;
coherence
L `1 is finite

proof end;

cluster L `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

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 :Def29: :: 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 & 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 = choose (F " {(support (max B,(InvLexOrder NAT )))}) );
existence
( ( dom (L `1 ) = the_Vertices_of G implies ex b₁ being Vertex of G st b₁ = choose (the_Vertices_of G) ) & ( not dom (L `1 ) = the_Vertices_of G implies ex b<sub>1</sub> 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₁ = choose (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> = choose (the_Vertices_of G) & b<sub>2</sub> = choose (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₁ = choose (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₂ = choose (F " {(support (max B,(InvLexOrder NAT )))}) ) implies b₁ = b₂ ) )

proof end;

consistency
for b₁ being Vertex of G holds verum ;

end;

:: deftheorem Def29 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> = choose (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₃ = 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

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 Th32u: :: 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 Th33u: :: 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 Th34u: :: 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 :Def32: :: 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 Def32 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 :dLBFSSeq: :: 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 dLBFSSeq 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 dLBFSSeq;

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 dLBFSSeq;

end;

definition

let G be finite _Graph;
let S be LexBFS:LabelingSeq of G;
func S ``1 -> preVNumberingSeq of G means :d1stBFSLS: :: LEXBFS:def 16
for n being Nat holds it . n = (S . n) `1 ;
existence
ex b<sub>1</sub> being preVNumberingSeq of G st
for n being Nat holds b<sub>1</sub> . 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 d1stBFSLS defines ``1 LEXBFS:def 16 :

for G being finite _Graph
for S being LexBFS:LabelingSeq of G
for b₃ being preVNumberingSeq of G holds
( b₃ = 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 :Def33: :: 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 Def33 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 Th36: :: 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 Th36;

end;

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

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

theorem Th40: :: 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;

theorem Th41: :: 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 Th44: :: 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 Th46: :: 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 Th47: :: 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 Th48: :: 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 Th49: :: 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 Th49;

end;

theorem Th50: :: 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 Th51: :: LEXBFS:37

for G being finite _Graph holds (LexBFS:CSeq G) .Lifespan() = G .order()

proof end;

theorem VNS0a: :: LEXBFS:38

for G being finite _Graph holds (LexBFS:CSeq G) ``1 is eventually-constant

proof end;

theorem VNS0: :: 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 VNS1: :: LEXBFS:40

for G being finite _Graph holds ((LexBFS:CSeq G) ``1 ) .Result() = ((LexBFS:CSeq G) .Result() ) `1

proof end;

theorem Th53: :: 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 Th54: :: 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 Th55: :: 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 Th56: :: 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 Th57: :: 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 Th58: :: 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;

theorem Th59: :: 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;

theorem Th60: :: 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 Th61: :: LEXBFS:49

for G being finite _Graph holds dom (((LexBFS:CSeq G) .Result() ) `1 ) = the_Vertices_of G

proof end;

theorem Th62: :: LEXBFS:50

for G being finite _Graph holds (((LexBFS:CSeq G) .Result() ) `1 ) " is VertexScheme of G

proof end;

theorem Th63: :: 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;

theorem Th64: :: 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 :Def34: :: 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 Def34 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 Th65: :: LEXBFS:53

for G being finite _Graph
for n being Nat holds ((LexBFS:CSeq G) . n) `1 is with_property_L3

proof end;

theorem Th66: :: 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 :Def36: :: 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 & F = (L `2 ) | ((the_Vertices_of G) \ (dom (L `1 ))) & it = choose (F " {(max S)}) );
existence
( ( dom (L `1 ) = the_Vertices_of G implies ex b₁ being Vertex of G st b₁ = choose (the_Vertices_of G) ) & ( not dom (L `1 ) = the_Vertices_of G implies ex b<sub>1</sub> 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₁ = choose (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> = choose (the_Vertices_of G) & b<sub>2</sub> = choose (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₁ = choose (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₂ = choose (F " {(max S)}) ) implies b₁ = b₂ ) ) ;
consistency
for b₁ being Vertex of G holds verum ;

end;

:: deftheorem Def36 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> = choose (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₃ = 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

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 :dLMCSU: :: 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 dLMCSU 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 :Def39: :: 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 Def39 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 :dMCSSeq: :: 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 dMCSSeq 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 dMCSSeq;

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 dMCSSeq;

end;

definition

let G be finite _Graph;
let S be MCS:LabelingSeq of G;
func S ``1 -> preVNumberingSeq of G means :d1stMCSLS: :: LEXBFS:def 25
for n being Nat holds it . n = (S . n) `1 ;
existence
ex b<sub>1</sub> being preVNumberingSeq of G st
for n being Nat holds b<sub>1</sub> . 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 d1stMCSLS defines ``1 LEXBFS:def 25 :

for G being finite _Graph
for S being MCS:LabelingSeq of G
for b₃ being preVNumberingSeq of G holds
( b₃ = 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 :Def40: :: 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 Def40 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 Th68: :: 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 Th68;

end;

theorem Th70: :: LEXBFS:57

for G being finite _Graph
for v being set holds ((MCS:Init G) `2 ) . v = 0

proof end;

theorem Th72: :: 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 Th73: :: 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 Th74: :: 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 Th75: :: 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 Th76: :: 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

proof end;

theorem Th81: :: 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 Th82: :: 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 Th83: :: 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 Th84: :: 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 Th85: :: 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 Th85;

end;

theorem Th86: :: 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 Th87: :: LEXBFS:70

for G being finite _Graph holds (MCS:CSeq G) .Lifespan() = G .order()

proof end;

theorem mVNS0a: :: LEXBFS:71

for G being finite _Graph holds (MCS:CSeq G) ``1 is eventually-constant

proof end;

theorem mVNS0: :: LEXBFS:72

for G being finite _Graph holds ((MCS:CSeq G) ``1 ) .Lifespan() = (MCS:CSeq G) .Lifespan()

proof end;

theorem Th88: :: 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 Th88;

end;

theorem Th89: :: 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 Th90: :: 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 Th91: :: 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 :Def41: :: 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 Def41 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;