:: by Broderick Arneson and Piotr Rudnicki

::

:: Received November 17, 2006

:: Copyright (c) 2006-2012 Association of Mizar Users

begin

Lm1: for F being Function

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

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

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;

Lm3: for a, b, c being real number st a < b holds

(c - b) + 1 < (c - a) + 1

proof end;

registration

existence

ex b_{1} being Subset of (bool NAT) st

( not b_{1} is empty & b_{1} is finite & b_{1} is with_finite-elements )

end;
ex b

( not b

proof end;

definition

canceled;

let f, g be Function;

ex b_{1} being Function st

( dom b_{1} = (dom f) \/ (dom g) & ( for x being set st x in (dom f) \/ (dom g) holds

b_{1} . x = (f . x) \/ (g . x) ) )

for b_{1}, b_{2} being Function st dom b_{1} = (dom f) \/ (dom g) & ( for x being set st x in (dom f) \/ (dom g) holds

b_{1} . x = (f . x) \/ (g . x) ) & dom b_{2} = (dom f) \/ (dom g) & ( for x being set st x in (dom f) \/ (dom g) holds

b_{2} . x = (f . x) \/ (g . x) ) holds

b_{1} = b_{2}

end;
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 ( dom it = (dom f) \/ (dom g) & ( for x being set st x in (dom f) \/ (dom g) holds

it . x = (f . x) \/ (g . x) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

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

for f, g, b_{3} being Function holds

( b_{3} = f .\/ g iff ( dom b_{3} = (dom f) \/ (dom g) & ( for x being set st x in (dom f) \/ (dom g) holds

b_{3} . x = (f . x) \/ (g . x) ) ) );

for f, g, b

( b

b

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)))

((Seg k) \ (Seg (k -' n))) \/ {(k -' n)} = (Seg k) \ (Seg (k -' (n + 1)))

proof end;

definition
end;

:: deftheorem Def3 defines natsubset-yielding LEXBFS:def 3 :

for f being Relation holds

( f is natsubset-yielding iff rng f c= bool NAT );

for f being Relation holds

( f is natsubset-yielding iff rng f c= bool NAT );

registration

existence

ex b_{1} being Function st

( b_{1} is finite-yielding & b_{1} is natsubset-yielding )

end;
ex b

( b

proof 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

end;
let x be set ;

:: original: .

redefine func f . x -> finite Subset of NAT;

coherence

f . x is finite Subset of NAT

proof end;

definition

let F be natural-valued Function;

let S be set ;

let k be Nat;

ex b_{1} being natural-valued Function st

( dom b_{1} = dom F & ( for y being set holds

( ( y in S & y in dom F implies b_{1} . y = (F . y) + k ) & ( not y in S implies b_{1} . y = F . y ) ) ) )

for b_{1}, b_{2} being natural-valued Function st dom b_{1} = dom F & ( for y being set holds

( ( y in S & y in dom F implies b_{1} . y = (F . y) + k ) & ( not y in S implies b_{1} . y = F . y ) ) ) & dom b_{2} = dom F & ( for y being set holds

( ( y in S & y in dom F implies b_{2} . y = (F . y) + k ) & ( not y in S implies b_{2} . y = F . y ) ) ) holds

b_{1} = b_{2}

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

ex b

( dom b

( ( y in S & y in dom F implies b

proof end;

uniqueness for b

( ( y in S & y in dom F implies b

( ( y in S & y in dom F implies b

b

proof end;

:: deftheorem Def4 defines .incSubset LEXBFS:def 4 :

for F being natural-valued Function

for S being set

for k being Nat

for b_{4} being natural-valued Function holds

( b_{4} = F .incSubset (S,k) iff ( dom b_{4} = dom F & ( for y being set holds

( ( y in S & y in dom F implies b_{4} . y = (F . y) + k ) & ( not y in S implies b_{4} . y = F . y ) ) ) ) );

for F being natural-valued Function

for S being set

for k being Nat

for b

( b

( ( y in S & y in dom F implies b

definition

let n be Ordinal;

let T be connected TermOrder of n;

let B be non empty finite Subset of (Bags n);

ex b_{1} being bag of n st

( b_{1} in B & ( for x being bag of n st x in B holds

x <= b_{1},T ) )

for b_{1}, b_{2} being bag of n st b_{1} in B & ( for x being bag of n st x in B holds

x <= b_{1},T ) & b_{2} in B & ( for x being bag of n st x in B holds

x <= b_{2},T ) holds

b_{1} = b_{2}

end;
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 ( it in B & ( for x being bag of n st x in B holds

x <= it,T ) );

ex b

( b

x <= b

proof end;

uniqueness for b

x <= b

x <= b

b

proof 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_{4} being bag of n holds

( b_{4} = max (B,T) iff ( b_{4} in B & ( for x being bag of n st x in B holds

x <= b_{4},T ) ) );

for n being Ordinal

for T being connected TermOrder of n

for B being non empty finite Subset of (Bags n)

for b

( b

x <= b

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;

begin

:: deftheorem Def6 defines iterative LEXBFS:def 6 :

for s being ManySortedSet of NAT holds

( s is iterative iff for k, n being Nat st s . k = s . n holds

s . (k + 1) = s . (n + 1) );

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 ;

end;
attr S is eventually-constant means :Def7: :: LEXBFS:def 7

ex n being Nat st

for m being Nat st n <= m holds

S . n = S . m;

ex n being Nat st

for m being Nat st n <= m holds

S . n = S . m;

:: deftheorem Def7 defines eventually-constant LEXBFS:def 7 :

for S being ManySortedSet of NAT holds

( S is eventually-constant iff ex n being Nat st

for m being Nat st n <= m holds

S . n = S . m );

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

ex b_{1} being ManySortedSet of NAT st

( b_{1} is halting & b_{1} is iterative & b_{1} is eventually-constant )
end;

cluster Relation-like NAT -defined Function-like total halting iterative eventually-constant for set ;

existence ex b

( b

proof end;

theorem Th7: :: LEXBFS:7

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

Gs is eventually-constant

Gs is eventually-constant

proof end;

registration

for b_{1} being ManySortedSet of NAT st b_{1} is halting & b_{1} is iterative holds

b_{1} is eventually-constant
by Th7;

end;

cluster Relation-like NAT -defined Function-like total halting iterative -> eventually-constant for set ;

coherence for b

b

registration

coherence

for b_{1} being ManySortedSet of NAT st b_{1} is eventually-constant holds

b_{1} is halting
by Th8;

end;
for b

b

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

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

for n, m being Nat st Gs .Lifespan() <= n & n <= m holds

Gs . m = Gs . n

proof end;

begin

definition

let G be finite _Graph;

ex b_{1} being ManySortedSet of NAT st

for i being Nat holds b_{1} . i is PartFunc of (the_Vertices_of G),NAT

end;
mode preVNumberingSeq of G -> ManySortedSet of NAT means :Def8: :: LEXBFS:def 8

for i being Nat holds it . i is PartFunc of (the_Vertices_of G),NAT;

existence for i being Nat holds it . i is PartFunc of (the_Vertices_of G),NAT;

ex b

for i being Nat holds b

proof end;

:: deftheorem Def8 defines preVNumberingSeq LEXBFS:def 8 :

for G being finite _Graph

for b_{2} being ManySortedSet of NAT holds

( b_{2} is preVNumberingSeq of G iff for i being Nat holds b_{2} . i is PartFunc of (the_Vertices_of G),NAT );

for G being finite _Graph

for b

( b

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

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

:: deftheorem Def9 defines vertex-numbering LEXBFS:def 9 :

for G being finite _Graph

for S being preVNumberingSeq of G holds

( S is vertex-numbering iff ( S . 0 = {} & 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)) ) ) ) );

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;

existence

ex b_{1} being preVNumberingSeq of G st b_{1} is vertex-numbering

end;
existence

ex b

proof end;

:: Facts hidden in the existence proof?

registration

let G be finite _Graph;

correctness

coherence

for b_{1} being preVNumberingSeq of G st b_{1} is vertex-numbering holds

( b_{1} is halting & b_{1} is iterative );

by Def9;

end;
correctness

coherence

for b

( b

by Def9;

definition
end;

definition

let G be finite _Graph;

let S be VNumberingSeq of G;

let n be Nat;

( ( n >= S .Lifespan() implies ex b_{1} being set st b_{1} = choose (the_Vertices_of G) ) & ( not n >= S .Lifespan() implies ex b_{1} being set st

( not b_{1} in dom (S . n) & S . (n + 1) = (S . n) +* (b_{1} .--> ((S .Lifespan()) -' n)) ) ) )

for b_{1}, b_{2} being set holds

( ( n >= S .Lifespan() & b_{1} = choose (the_Vertices_of G) & b_{2} = choose (the_Vertices_of G) implies b_{1} = b_{2} ) & ( not n >= S .Lifespan() & not b_{1} in dom (S . n) & S . (n + 1) = (S . n) +* (b_{1} .--> ((S .Lifespan()) -' n)) & not b_{2} in dom (S . n) & S . (n + 1) = (S . n) +* (b_{2} .--> ((S .Lifespan()) -' n)) implies b_{1} = b_{2} ) )

for b_{1} being set holds verum
;

end;
let S be VNumberingSeq of G;

let n be Nat;

func S .PickedAt n -> set means :Def10: :: LEXBFS:def 10

it = choose (the_Vertices_of G) if n >= S .Lifespan()

otherwise ( not it in dom (S . n) & S . (n + 1) = (S . n) +* (it .--> ((S .Lifespan()) -' n)) );

existence 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)) );

( ( n >= S .Lifespan() implies ex b

( not b

proof end;

uniqueness for b

( ( n >= S .Lifespan() & b

proof end;

consistency for b

:: deftheorem Def10 defines .PickedAt LEXBFS:def 10 :

for G being finite _Graph

for S being VNumberingSeq of G

for n being Nat

for b_{4} being set holds

( ( n >= S .Lifespan() implies ( b_{4} = S .PickedAt n iff b_{4} = choose (the_Vertices_of G) ) ) & ( not n >= S .Lifespan() implies ( b_{4} = S .PickedAt n iff ( not b_{4} in dom (S . n) & S . (n + 1) = (S . n) +* (b_{4} .--> ((S .Lifespan()) -' n)) ) ) ) );

for G being finite _Graph

for S being VNumberingSeq of G

for n being Nat

for b

( ( n >= S .Lifespan() implies ( b

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)} )

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

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

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))

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 ) )

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 )

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

for S being VNumberingSeq of G

for m, n being Nat st m <= n holds

S . m c= S . n

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

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

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 )

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 )

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

:: 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)))

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)))

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;

begin

definition

let X1, X3 be set ;

let X2 be non empty set ;

let x be Element of [:(PFuncs (X1,X3)),X2:];

:: original: `1

redefine func x `1 -> Element of PFuncs (X1,X3);

coherence

x `1 is Element of PFuncs (X1,X3) by MCART_1:10;

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

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

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;
mode LexBFS:Labeling of G is Element of [:(PFuncs ((the_Vertices_of G),NAT)),(Funcs ((the_Vertices_of G),(Fin NAT))):];

registration

let G be finite _Graph;

let L be LexBFS:Labeling of G;

coherence

L `1 is finite

L `2 is finite ;

end;
let L be LexBFS:Labeling of G;

coherence

L `1 is finite

proof end;

coherence L `2 is finite ;

definition

let G be _Graph;

[{},((the_Vertices_of G) --> {})] is LexBFS:Labeling of G

end;
func LexBFS:Init G -> LexBFS:Labeling of G equals :: LEXBFS:def 11

[{},((the_Vertices_of G) --> {})];

coherence [{},((the_Vertices_of G) --> {})];

[{},((the_Vertices_of G) --> {})] is LexBFS:Labeling of G

proof end;

:: deftheorem defines LexBFS:Init LEXBFS:def 11 :

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

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;

( ( dom (L `1) = the_Vertices_of G implies ex b_{1} being Vertex of G st b_{1} = choose (the_Vertices_of G) ) & ( not dom (L `1) = the_Vertices_of G implies ex b_{1} 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_{1} = choose (F " {(support (max (B,(InvLexOrder NAT))))}) ) ) )

for b_{1}, b_{2} being Vertex of G holds

( ( dom (L `1) = the_Vertices_of G & b_{1} = choose (the_Vertices_of G) & b_{2} = choose (the_Vertices_of G) implies b_{1} = b_{2} ) & ( 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_{1} = 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_{2} = choose (F " {(support (max (B,(InvLexOrder NAT))))}) ) implies b_{1} = b_{2} ) )

for b_{1} being Vertex of G holds verum
;

end;
let L be LexBFS:Labeling of G;

func LexBFS:PickUnnumbered L -> Vertex of G means :Def12: :: LEXBFS:def 12

it = choose (the_Vertices_of G) if dom (L `1) = the_Vertices_of G

otherwise ex S being non empty finite Subset of (bool NAT) ex B being non empty finite Subset of (Bags NAT) ex F being Function st

( S = rng F & 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 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))))}) );

( ( dom (L `1) = the_Vertices_of G implies ex b

( 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

proof end;

uniqueness for b

( ( dom (L `1) = the_Vertices_of G & b

( 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

( 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

proof end;

consistency for b

:: deftheorem Def12 defines LexBFS:PickUnnumbered LEXBFS:def 12 :

for G being finite _Graph

for L being LexBFS:Labeling of G

for b_{3} being Vertex of G holds

( ( dom (L `1) = the_Vertices_of G implies ( b_{3} = LexBFS:PickUnnumbered L iff b_{3} = choose (the_Vertices_of G) ) ) & ( not dom (L `1) = the_Vertices_of G implies ( b_{3} = 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_{3} = choose (F " {(support (max (B,(InvLexOrder NAT))))}) ) ) ) );

for G being finite _Graph

for L being LexBFS:Labeling of G

for b

( ( dom (L `1) = the_Vertices_of G implies ( b

( 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

definition

let G be finite _Graph;

let L be LexBFS:Labeling of G;

let v be Vertex of G;

let n be Nat;

[((L `1) +* (v .--> ((G .order()) -' n))),((L `2) .\/ (((G .AdjacentSet {v}) \ (dom (L `1))) --> {((G .order()) -' n)}))] is LexBFS:Labeling of G

end;
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)}))];

[((L `1) +* (v .--> ((G .order()) -' n))),((L `2) .\/ (((G .AdjacentSet {v}) \ (dom (L `1))) --> {((G .order()) -' n)}))] is LexBFS:Labeling of G

proof 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)}))];

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

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

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)}

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;

( ( 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_{1} being LexBFS:Labeling of G holds verum
;

end;
let L be LexBFS:Labeling of G;

func LexBFS:Step L -> LexBFS:Labeling of G equals :Def14: :: LEXBFS:def 14

L if G .order() <= card (dom (L `1))

otherwise LexBFS:Update (L,(LexBFS:PickUnnumbered L),(card (dom (L `1))));

coherence L if G .order() <= card (dom (L `1))

otherwise LexBFS:Update (L,(LexBFS:PickUnnumbered L),(card (dom (L `1))));

( ( 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

:: deftheorem Def14 defines LexBFS:Step LEXBFS:def 14 :

for G being finite _Graph

for L being LexBFS:Labeling of G holds

( ( G .order() <= card (dom (L `1)) implies LexBFS:Step L = L ) & ( not G .order() <= card (dom (L `1)) implies LexBFS:Step L = LexBFS:Update (L,(LexBFS:PickUnnumbered L),(card (dom (L `1)))) ) );

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;

ex b_{1} being ManySortedSet of NAT st

for n being Nat holds b_{1} . n is LexBFS:Labeling of G

end;
mode LexBFS:LabelingSeq of G -> ManySortedSet of NAT means :Def15: :: LEXBFS:def 15

for n being Nat holds it . n is LexBFS:Labeling of G;

existence for n being Nat holds it . n is LexBFS:Labeling of G;

ex b

for n being Nat holds b

proof end;

:: deftheorem Def15 defines LexBFS:LabelingSeq LEXBFS:def 15 :

for G being _Graph

for b_{2} being ManySortedSet of NAT holds

( b_{2} is LexBFS:LabelingSeq of G iff for n being Nat holds b_{2} . n is LexBFS:Labeling of G );

for G being _Graph

for b

( b

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

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

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

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

definition

let G be finite _Graph;

let S be LexBFS:LabelingSeq of G;

ex b_{1} being preVNumberingSeq of G st

for n being Nat holds b_{1} . n = (S . n) `1

for b_{1}, b_{2} being preVNumberingSeq of G st ( for n being Nat holds b_{1} . n = (S . n) `1 ) & ( for n being Nat holds b_{2} . n = (S . n) `1 ) holds

b_{1} = b_{2}

end;
let S be LexBFS:LabelingSeq of G;

func S ``1 -> preVNumberingSeq of G means :Def16: :: LEXBFS:def 16

for n being Nat holds it . n = (S . n) `1 ;

existence for n being Nat holds it . n = (S . n) `1 ;

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def16 defines ``1 LEXBFS:def 16 :

for G being finite _Graph

for S being LexBFS:LabelingSeq of G

for b_{3} being preVNumberingSeq of G holds

( b_{3} = S ``1 iff for n being Nat holds b_{3} . n = (S . n) `1 );

for G being finite _Graph

for S being LexBFS:LabelingSeq of G

for b

( b

definition

let G be finite _Graph;

ex b_{1} being LexBFS:LabelingSeq of G st

( b_{1} . 0 = LexBFS:Init G & ( for n being Nat holds b_{1} . (n + 1) = LexBFS:Step (b_{1} . n) ) )

for b_{1}, b_{2} being LexBFS:LabelingSeq of G st b_{1} . 0 = LexBFS:Init G & ( for n being Nat holds b_{1} . (n + 1) = LexBFS:Step (b_{1} . n) ) & b_{2} . 0 = LexBFS:Init G & ( for n being Nat holds b_{2} . (n + 1) = LexBFS:Step (b_{2} . n) ) holds

b_{1} = b_{2}

end;
func LexBFS:CSeq G -> LexBFS:LabelingSeq of G means :Def17: :: LEXBFS:def 17

( it . 0 = LexBFS:Init G & ( for n being Nat holds it . (n + 1) = LexBFS:Step (it . n) ) );

existence ( it . 0 = LexBFS:Init G & ( for n being Nat holds it . (n + 1) = LexBFS:Step (it . n) ) );

ex b

( b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def17 defines LexBFS:CSeq LEXBFS:def 17 :

for G being finite _Graph

for b_{2} being LexBFS:LabelingSeq of G holds

( b_{2} = LexBFS:CSeq G iff ( b_{2} . 0 = LexBFS:Init G & ( for n being Nat holds b_{2} . (n + 1) = LexBFS:Step (b_{2} . n) ) ) );

for G being finite _Graph

for b

( b

Lm7: 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

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

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

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)

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)))))

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

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

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

for m, n being Nat st G .order() <= m & m <= n holds

(LexBFS:CSeq G) . m = (LexBFS:CSeq G) . n

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

for n being Nat holds

( dom (((LexBFS:CSeq G) . n) `1) = the_Vertices_of G iff G .order() <= n )

proof end;

registration
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)

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 ) ) ) )

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))

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

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

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

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)

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

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} )

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;

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

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

:: 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} )

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;

end;
let F be PartFunc of (the_Vertices_of G),NAT;

attr F is with_property_L3 means :Def18: :: 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 ) );

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

:: deftheorem Def18 defines with_property_L3 LEXBFS:def 18 :

for G being _Graph

for F being PartFunc of (the_Vertices_of G),NAT holds

( F is with_property_L3 iff for a, b, c being Vertex of G st a in dom F & 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 ) ) );

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

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;

begin

definition

let G be _Graph;

mode MCS:Labeling of G is Element of [:(PFuncs ((the_Vertices_of G),NAT)),(Funcs ((the_Vertices_of G),NAT)):];

end;
mode MCS:Labeling of G is Element of [:(PFuncs ((the_Vertices_of G),NAT)),(Funcs ((the_Vertices_of G),NAT)):];

definition
end;

:: deftheorem defines MCS:Init LEXBFS:def 19 :

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

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;

( ( dom (L `1) = the_Vertices_of G implies ex b_{1} being Vertex of G st b_{1} = choose (the_Vertices_of G) ) & ( not dom (L `1) = the_Vertices_of G implies ex b_{1} 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_{1} = choose (F " {(max S)}) ) ) )

for b_{1}, b_{2} being Vertex of G holds

( ( dom (L `1) = the_Vertices_of G & b_{1} = choose (the_Vertices_of G) & b_{2} = choose (the_Vertices_of G) implies b_{1} = b_{2} ) & ( 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_{1} = 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_{2} = choose (F " {(max S)}) ) implies b_{1} = b_{2} ) )
;

consistency

for b_{1} being Vertex of G holds verum
;

end;
let L be MCS:Labeling of G;

func MCS:PickUnnumbered L -> Vertex of G means :Def20: :: LEXBFS:def 20

it = choose (the_Vertices_of G) if dom (L `1) = the_Vertices_of G

otherwise ex S being non empty natural-membered finite set ex F being Function st

( S = rng F & F = (L `2) | ((the_Vertices_of G) \ (dom (L `1))) & it = choose (F " {(max S)}) );

existence 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)}) );

( ( dom (L `1) = the_Vertices_of G implies ex b

( S = rng F & F = (L `2) | ((the_Vertices_of G) \ (dom (L `1))) & b

proof end;

uniqueness for b

( ( dom (L `1) = the_Vertices_of G & b

( S = rng F & F = (L `2) | ((the_Vertices_of G) \ (dom (L `1))) & b

( S = rng F & F = (L `2) | ((the_Vertices_of G) \ (dom (L `1))) & b

consistency

for b

:: deftheorem Def20 defines MCS:PickUnnumbered LEXBFS:def 20 :

for G being finite _Graph

for L being MCS:Labeling of G

for b_{3} being Vertex of G holds

( ( dom (L `1) = the_Vertices_of G implies ( b_{3} = MCS:PickUnnumbered L iff b_{3} = choose (the_Vertices_of G) ) ) & ( not dom (L `1) = the_Vertices_of G implies ( b_{3} = 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_{3} = choose (F " {(max S)}) ) ) ) );

for G being finite _Graph

for L being MCS:Labeling of G

for b

( ( dom (L `1) = the_Vertices_of G implies ( b

( S = rng F & F = (L `2) | ((the_Vertices_of G) \ (dom (L `1))) & b

definition

let G be finite _Graph;

let L be MCS:Labeling of G;

let v be set ;

[(L `1),((L `2) .incSubset (((G .AdjacentSet {v}) \ (dom (L `1))),1))] is MCS:Labeling of G

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

[(L `1),((L `2) .incSubset (((G .AdjacentSet {v}) \ (dom (L `1))),1))] is MCS:Labeling of G

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

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;

ex b_{1}, M being MCS:Labeling of G st

( M = [((L `1) +* (v .--> ((G .order()) -' n))),(L `2)] & b_{1} = MCS:LabelAdjacent (M,v) )

for b_{1}, b_{2} being MCS:Labeling of G st ex M being MCS:Labeling of G st

( M = [((L `1) +* (v .--> ((G .order()) -' n))),(L `2)] & b_{1} = MCS:LabelAdjacent (M,v) ) & ex M being MCS:Labeling of G st

( M = [((L `1) +* (v .--> ((G .order()) -' n))),(L `2)] & b_{2} = MCS:LabelAdjacent (M,v) ) holds

b_{1} = b_{2}
;

end;
let L be MCS:Labeling of G;

let v be Vertex of G;

let n be Nat;

func MCS:Update (L,v,n) -> MCS:Labeling of G means :Def22: :: LEXBFS:def 22

ex M being MCS:Labeling of G st

( M = [((L `1) +* (v .--> ((G .order()) -' n))),(L `2)] & it = MCS:LabelAdjacent (M,v) );

existence ex M being MCS:Labeling of G st

( M = [((L `1) +* (v .--> ((G .order()) -' n))),(L `2)] & it = MCS:LabelAdjacent (M,v) );

ex b

( M = [((L `1) +* (v .--> ((G .order()) -' n))),(L `2)] & b

proof end;

uniqueness for b

( M = [((L `1) +* (v .--> ((G .order()) -' n))),(L `2)] & b

( M = [((L `1) +* (v .--> ((G .order()) -' n))),(L `2)] & b

b

:: deftheorem Def22 defines MCS:Update LEXBFS:def 22 :

for G being finite _Graph

for L being MCS:Labeling of G

for v being Vertex of G

for n being Nat

for b_{5} being MCS:Labeling of G holds

( b_{5} = MCS:Update (L,v,n) iff ex M being MCS:Labeling of G st

( M = [((L `1) +* (v .--> ((G .order()) -' n))),(L `2)] & b_{5} = MCS:LabelAdjacent (M,v) ) );

for G being finite _Graph

for L being MCS:Labeling of G

for v being Vertex of G

for n being Nat

for b

( b

( M = [((L `1) +* (v .--> ((G .order()) -' n))),(L `2)] & b

definition

let G be finite _Graph;

let L be MCS:Labeling of G;

( ( 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_{1} being MCS:Labeling of G holds verum
;

end;
let L be MCS:Labeling of G;

func MCS:Step L -> MCS:Labeling of G equals :Def23: :: LEXBFS:def 23

L if G .order() <= card (dom (L `1))

otherwise MCS:Update (L,(MCS:PickUnnumbered L),(card (dom (L `1))));

coherence L if G .order() <= card (dom (L `1))

otherwise MCS:Update (L,(MCS:PickUnnumbered L),(card (dom (L `1))));

( ( 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

:: deftheorem Def23 defines MCS:Step LEXBFS:def 23 :

for G being finite _Graph

for L being MCS:Labeling of G holds

( ( G .order() <= card (dom (L `1)) implies MCS:Step L = L ) & ( not G .order() <= card (dom (L `1)) implies MCS:Step L = MCS:Update (L,(MCS:PickUnnumbered L),(card (dom (L `1)))) ) );

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;

ex b_{1} being ManySortedSet of NAT st

for n being Nat holds b_{1} . n is MCS:Labeling of G

end;
mode MCS:LabelingSeq of G -> ManySortedSet of NAT means :Def24: :: LEXBFS:def 24

for n being Nat holds it . n is MCS:Labeling of G;

existence for n being Nat holds it . n is MCS:Labeling of G;

ex b

for n being Nat holds b

proof end;

:: deftheorem Def24 defines MCS:LabelingSeq LEXBFS:def 24 :

for G being _Graph

for b_{2} being ManySortedSet of NAT holds

( b_{2} is MCS:LabelingSeq of G iff for n being Nat holds b_{2} . n is MCS:Labeling of G );

for G being _Graph

for b

( b

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

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

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

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

definition

let G be finite _Graph;

let S be MCS:LabelingSeq of G;

ex b_{1} being preVNumberingSeq of G st

for n being Nat holds b_{1} . n = (S . n) `1

for b_{1}, b_{2} being preVNumberingSeq of G st ( for n being Nat holds b_{1} . n = (S . n) `1 ) & ( for n being Nat holds b_{2} . n = (S . n) `1 ) holds

b_{1} = b_{2}

end;
let S be MCS:LabelingSeq of G;

func S ``1 -> preVNumberingSeq of G means :Def25: :: LEXBFS:def 25

for n being Nat holds it . n = (S . n) `1 ;

existence for n being Nat holds it . n = (S . n) `1 ;

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def25 defines ``1 LEXBFS:def 25 :

for G being finite _Graph

for S being MCS:LabelingSeq of G

for b_{3} being preVNumberingSeq of G holds

( b_{3} = S ``1 iff for n being Nat holds b_{3} . n = (S . n) `1 );

for G being finite _Graph

for S being MCS:LabelingSeq of G

for b

( b

definition

let G be finite _Graph;

ex b_{1} being MCS:LabelingSeq of G st

( b_{1} . 0 = MCS:Init G & ( for n being Nat holds b_{1} . (n + 1) = MCS:Step (b_{1} . n) ) )

for b_{1}, b_{2} being MCS:LabelingSeq of G st b_{1} . 0 = MCS:Init G & ( for n being Nat holds b_{1} . (n + 1) = MCS:Step (b_{1} . n) ) & b_{2} . 0 = MCS:Init G & ( for n being Nat holds b_{2} . (n + 1) = MCS:Step (b_{2} . n) ) holds

b_{1} = b_{2}

end;
func MCS:CSeq G -> MCS:LabelingSeq of G means :Def26: :: LEXBFS:def 26

( it . 0 = MCS:Init G & ( for n being Nat holds it . (n + 1) = MCS:Step (it . n) ) );

existence ( it . 0 = MCS:Init G & ( for n being Nat holds it . (n + 1) = MCS:Step (it . n) ) );

ex b

( b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def26 defines MCS:CSeq LEXBFS:def 26 :

for G being finite _Graph

for b_{2} being MCS:LabelingSeq of G holds

( b_{2} = MCS:CSeq G iff ( b_{2} . 0 = MCS:Init G & ( for n being Nat holds b_{2} . (n + 1) = MCS:Step (b_{2} . n) ) ) );

for G being finite _Graph

for b

( b

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)

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)

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

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

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

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

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 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)))))

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

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

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

for m, n being Nat st G .order() <= m & m <= n holds

(MCS:CSeq G) . m = (MCS:CSeq G) . n

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

for n being Nat holds

( dom (((MCS:CSeq G) . n) `1) = the_Vertices_of G iff G .order() <= n )

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

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 ) ) ) )

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)))

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;

end;
let F be PartFunc of (the_Vertices_of G),NAT;

attr F is with_property_T means :Def27: :: 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 );

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

:: deftheorem Def27 defines with_property_T LEXBFS:def 27 :

for G being _Graph

for F being PartFunc of (the_Vertices_of G),NAT holds

( F is with_property_T iff for a, b, c being Vertex of G st a in dom F & 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 ) );

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

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;