LEXBFS: Recognizing Chordal Graphs: Lex BFS and MCS

proof end;

end;

definition

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

proof end;

proof end;

end;

:: deftheorem LEXBFS:def 1 :

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

theorem Th3: :: LEXBFS:3

for m, n, k being Nat holds
( m in (Seg k) \ (Seg (k -' n)) iff ( k -' n < m & m <= k ) )

proof end;

theorem Th4: :: LEXBFS:4

for n, k, m being Nat st n <= m holds
(Seg k) \ (Seg (k -' n)) c= (Seg k) \ (Seg (k -' m))

proof end;

theorem Th5: :: LEXBFS:5

for n, k being Nat st n < k holds
((Seg k) \ (Seg (k -' n))) \/ {(k -' n)} = (Seg k) \ (Seg (k -' (n + 1)))

proof end;

definition

let f be Relation;

attr f is natsubset-yielding means :Def3: :: LEXBFS:def 3
rng f c= bool NAT;

end;

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

registration

cluster Relation-like Function-like finite-yielding natsubset-yielding for set ;

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

proof end;

end;

theorem Th6: :: LEXBFS:6

for X being Ordinal
for a, b being finite Subset of X st a <> b holds
(a,1) -bag <> (b,1) -bag

proof end;

definition

let F be natural-valued Function;
let S be set ;
let k be Nat;

func F .incSubset (S,k) -> natural-valued Function means :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 ) ) ) );

proof end;

proof end;

end;

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

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

proof end;

proof end;

end;

:: deftheorem Def5 defines max LEXBFS:def 5 :

registration

let O be Ordinal;

cluster InvLexOrder O -> 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;

begin

definition

let s be ManySortedSet of NAT ;

attr s is iterative means :Def6: :: LEXBFS:def 6
for k, n being Nat st s . k = s . n holds
s . (k + 1) = s . (n + 1);

end;

:: deftheorem Def6 defines iterative LEXBFS:def 6 :

definition

let S be ManySortedSet of NAT ;

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;

end;

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

registration

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

proof end;

end;

theorem Th7: :: LEXBFS:7

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

proof end;

registration

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

coherence by Th7;

end;

theorem Th8: :: LEXBFS:8

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

proof end;

registration

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

coherence by Th8;

end;

theorem Th9: :: LEXBFS:9

for Gs being iterative eventually-constant ManySortedSet of NAT
for n being Nat st Gs .Lifespan() <= n holds
Gs . (Gs .Lifespan()) = Gs . n

proof end;

theorem Th10: :: LEXBFS:10

for Gs being iterative eventually-constant ManySortedSet of NAT
for n, m being Nat st Gs .Lifespan() <= n & n <= m holds
Gs . m = Gs . n

proof end;

begin

definition

let G be finite _Graph;

mode preVNumberingSeq of G -> ManySortedSet of NAT means :Def8: :: LEXBFS:def 8
for i being Nat holds it . i is PartFunc of (the_Vertices_of G),NAT;

proof end;

end;

:: deftheorem Def8 defines preVNumberingSeq LEXBFS:def 8 :

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

end;

definition

let G be finite _Graph;
let S be preVNumberingSeq of G;

attr S is vertex-numbering means :Def9: :: 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 Def9 defines vertex-numbering LEXBFS:def 9 :

registration

let G be finite _Graph;

cluster Relation-like NAT -defined Function-like total vertex-numbering for preVNumberingSeq of G;

proof end;

end;

:: Facts hidden in the existence proof?

registration

let G be finite _Graph;

cluster vertex-numbering -> halting iterative for preVNumberingSeq of G;

correctness by Def9;

end;

definition

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

end;

definition

let G be finite _Graph;
let S be VNumberingSeq of G;
let n be Nat;

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

proof end;

proof end;

consistency ;

end;

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

theorem Th11: :: LEXBFS:11

for G being finite _Graph
for S being VNumberingSeq of G
for n being Nat st n < S .Lifespan() holds
( S .PickedAt n in dom (S . (n + 1)) & dom (S . (n + 1)) = (dom (S . n)) \/ {(S .PickedAt n)} )

proof end;

theorem Th12: :: LEXBFS:12

for G being finite _Graph
for S being VNumberingSeq of G
for n being Nat st n < S .Lifespan() holds
(S . (n + 1)) . (S .PickedAt n) = (S .Lifespan()) -' n

proof end;

theorem :: LEXBFS:13

for G being finite _Graph
for S being VNumberingSeq of G
for n being Nat st n <= S .Lifespan() holds
card (dom (S . n)) = n

proof end;

theorem Th14: :: LEXBFS:14

for G being finite _Graph
for S being VNumberingSeq of G
for n being Nat holds rng (S . n) = (Seg (S .Lifespan())) \ (Seg ((S .Lifespan()) -' n))

proof end;

theorem Th15: :: LEXBFS:15

for G being finite _Graph
for S being VNumberingSeq of G
for n being Nat
for x being set holds
( (S . n) . x <= S .Lifespan() & ( x in dom (S . n) implies 1 <= (S . n) . x ) )

proof end;

theorem Th16: :: LEXBFS:16

for G being finite _Graph
for S being VNumberingSeq of G
for n, m being Nat st (S .Lifespan()) -' n < m & m <= S .Lifespan() holds
ex v being Vertex of G st
( v in dom (S . n) & (S . n) . v = m )

proof end;

theorem Th17: :: LEXBFS:17

for G being finite _Graph
for S being VNumberingSeq of G
for m, n being Nat st m <= n holds
S . m c= S . n

proof end;

theorem Th18: :: LEXBFS:18

for G being finite _Graph
for S being VNumberingSeq of G
for n being Nat holds S . n is one-to-one

proof end;

theorem Th19: :: LEXBFS:19

for G being finite _Graph
for S being VNumberingSeq of G
for m, n being Nat
for v being set st v in dom (S . m) & v in dom (S . n) holds
(S . m) . v = (S . n) . v

proof end;

theorem Th20: :: LEXBFS:20

for G being finite _Graph
for S being VNumberingSeq of G
for m, n being Nat
for v being set st v in dom (S . m) & (S . m) . v = n holds
S .PickedAt ((S .Lifespan()) -' n) = v

proof end;

theorem Th21: :: LEXBFS:21

for G being finite _Graph
for S being VNumberingSeq of G
for m, n being Nat st n < S .Lifespan() & n < m holds
( S .PickedAt n in dom (S . m) & (S . m) . (S .PickedAt n) = (S .Lifespan()) -' n )

proof end;

:: Inequalities relating the vlabel and the current iteration

theorem Th22: :: LEXBFS:22

for G being finite _Graph
for S being VNumberingSeq of G
for m being Nat
for v being set st v in dom (S . m) holds
( (S .Lifespan()) -' ((S . m) . v) < m & (S .Lifespan()) -' m < (S . m) . v )

proof end;

:: If a vertex has a larger vlabel than we do at some point in the
:: algorithm, then it must have been in the vlabel when we were picked

theorem Th23: :: LEXBFS:23

for G being finite _Graph
for S being VNumberingSeq of G
for i being Nat
for a, b being set st a in dom (S . i) & b in dom (S . i) & (S . i) . a < (S . i) . b holds
b in dom (S . ((S .Lifespan()) -' ((S . i) . a)))

proof end;

theorem Th24: :: LEXBFS:24

for G being finite _Graph
for S being VNumberingSeq of G
for i being Nat
for a, b being set st a in dom (S . i) & (S . i) . a < (S . i) . b holds
not a in dom (S . ((S .Lifespan()) -' ((S . i) . b)))

proof end;

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

proof end;

cluster L `2 -> finite ;

coherence ;

end;

definition

let G be _Graph;

func LexBFS:Init G -> LexBFS:Labeling of G equals :: LEXBFS:def 11
[{},((the_Vertices_of G) --> {})];

proof end;

end;

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

definition

let G be finite _Graph;
let L be LexBFS:Labeling of G;

func LexBFS:PickUnnumbered L -> Vertex of G means :Def12: :: LEXBFS:def 12
it = choose (the_Vertices_of G) if dom (L `1) = the_Vertices_of G
otherwise ex S being non empty finite Subset of (bool NAT) ex B being non empty finite Subset of (Bags NAT) ex F being Function st
( S = rng F & 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))))}) );

proof end;

proof end;

consistency ;

end;

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

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

proof end;

end;

:: deftheorem defines LexBFS:Update LEXBFS:def 13 :

theorem Th25: :: LEXBFS:25

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

proof end;

theorem Th26: :: LEXBFS:26

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

proof end;

theorem Th27: :: LEXBFS:27

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

proof end;

definition

let G be finite _Graph;
let L be LexBFS:Labeling of G;

func LexBFS:Step L -> LexBFS:Labeling of G equals :Def14: :: LEXBFS:def 14
L if G .order() <= card (dom (L `1))
otherwise LexBFS:Update (L,(LexBFS:PickUnnumbered L),(card (dom (L `1))));

coherence ;
consistency ;

end;

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

definition

let G be _Graph;

mode LexBFS:LabelingSeq of G -> ManySortedSet of NAT means :Def15: :: LEXBFS:def 15
for n being Nat holds it . n is LexBFS:Labeling of G;

proof end;

end;

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

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

end;

definition

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

end;

definition

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

proof end;

proof end;

end;

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

definition

let G be finite _Graph;

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

proof end;

proof end;

end;

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

theorem Th28: :: LEXBFS:28

for G being finite _Graph holds LexBFS:CSeq G is iterative

proof end;

registration

let G be finite _Graph;

cluster LexBFS:CSeq G -> iterative ;

coherence by Th28;

end;

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

proof end;

end;

:: the vertex picked has the largest v2label

theorem Th29: :: LEXBFS:29

for G being finite _Graph
for L being LexBFS:Labeling of G
for x being set st not x in dom (L `1) & dom (L `1) <> the_Vertices_of G holds
(((L `2) . x),1) -bag <= (((L `2) . (LexBFS:PickUnnumbered L)),1) -bag , InvLexOrder NAT

proof end;

:: the vertex picked is not currently in the vlabel

theorem Th30: :: LEXBFS:30

for G being finite _Graph
for L being LexBFS:Labeling of G st dom (L `1) <> the_Vertices_of G holds
not LexBFS:PickUnnumbered L in dom (L `1)

proof end;

theorem Th31: :: LEXBFS:31

for G being finite _Graph
for n being Nat st card (dom (((LexBFS:CSeq G) . n) `1)) < G .order() holds
((LexBFS:CSeq G) . (n + 1)) `1 = (((LexBFS:CSeq G) . n) `1) +* ((LexBFS:PickUnnumbered ((LexBFS:CSeq G) . n)) .--> ((G .order()) -' (card (dom (((LexBFS:CSeq G) . n) `1)))))

proof end;

theorem Th32: :: LEXBFS:32

for G being finite _Graph
for n being Nat st n <= G .order() holds
card (dom (((LexBFS:CSeq G) . n) `1)) = n

proof end;

theorem Th33: :: LEXBFS:33

for G being finite _Graph
for n being Nat st G .order() <= n holds
(LexBFS:CSeq G) . (G .order()) = (LexBFS:CSeq G) . n

proof end;

theorem Th34: :: LEXBFS:34

for G being finite _Graph
for m, n being Nat st G .order() <= m & m <= n holds
(LexBFS:CSeq G) . m = (LexBFS:CSeq G) . n

proof end;

theorem Th35: :: LEXBFS:35

for G being finite _Graph holds LexBFS:CSeq G is eventually-constant

proof end;

registration

let G be finite _Graph;

cluster LexBFS:CSeq G -> eventually-constant ;

coherence by Th35;

end;

theorem Th36: :: LEXBFS:36

for G being finite _Graph
for n being Nat holds
( dom (((LexBFS:CSeq G) . n) `1) = the_Vertices_of G iff G .order() <= n )

proof end;

theorem Th37: :: LEXBFS:37

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

proof end;

theorem Th38: :: LEXBFS:38

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

proof end;

theorem Th39: :: LEXBFS:39

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

proof end;

registration

let G be finite _Graph;

cluster (LexBFS:CSeq G) ``1 -> vertex-numbering ;

correctness

proof end;

end;

theorem Th40: :: LEXBFS:40

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

proof end;

theorem Th41: :: LEXBFS:41

for G being finite _Graph
for n being Nat st n < G .order() holds
((LexBFS:CSeq G) ``1) .PickedAt n = LexBFS:PickUnnumbered ((LexBFS:CSeq G) . n)

proof end;

theorem Th42: :: LEXBFS:42

for G being finite _Graph
for n being Nat st n < G .order() holds
ex w being Vertex of G st
( w = LexBFS:PickUnnumbered ((LexBFS:CSeq G) . n) & ( for v being set holds
( ( v in G .AdjacentSet {w} & not v in dom (((LexBFS:CSeq G) . n) `1) implies (((LexBFS:CSeq G) . (n + 1)) `2) . v = ((((LexBFS:CSeq G) . n) `2) . v) \/ {((G .order()) -' n)} ) & ( ( not v in G .AdjacentSet {w} or v in dom (((LexBFS:CSeq G) . n) `1) ) implies (((LexBFS:CSeq G) . (n + 1)) `2) . v = (((LexBFS:CSeq G) . n) `2) . v ) ) ) )

proof end;

theorem Th43: :: LEXBFS:43

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

proof end;

theorem Th44: :: LEXBFS:44

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

proof end;

theorem Th45: :: LEXBFS:45

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

proof end;

theorem Th46: :: LEXBFS:46

for G being finite _Graph
for m, n being Nat st m < n holds
for x being set st not (G .order()) -' m in (((LexBFS:CSeq G) . (m + 1)) `2) . x holds
not (G .order()) -' m in (((LexBFS:CSeq G) . n) `2) . x

proof end;

:: More general version of the above:
:: if the value added during step k doesn't appear in a later step (n),
:: then that value cannot appear in an even later step (m)

theorem Th47: :: LEXBFS:47

for G being finite _Graph
for m, n, k being Nat st k < n & n <= m holds
for x being set st not (G .order()) -' k in (((LexBFS:CSeq G) . n) `2) . x holds
not (G .order()) -' k in (((LexBFS:CSeq G) . m) `2) . x

proof end;

:: relates a value in a vertex's v2label to the vertex chosen at that time

theorem Th48: :: LEXBFS:48

for G being finite _Graph
for m, n being Nat
for x being Vertex of G st n in (((LexBFS:CSeq G) . m) `2) . x holds
ex y being Vertex of G st
( LexBFS:PickUnnumbered ((LexBFS:CSeq G) . ((G .order()) -' n)) = y & not y in dom (((LexBFS:CSeq G) . ((G .order()) -' n)) `1) & x in G .AdjacentSet {y} )

proof end;

theorem Th49: :: LEXBFS:49

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

proof end;

Lexicographic_breadth-first_search

theorem Th50: :: LEXBFS:50

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

proof end;

:: A vertex with a vlabel of k must have had the largest v2label when chosen

theorem Th51: :: LEXBFS:51

for G being finite _Graph
for i, j being Nat
for a, b being Vertex of G st a in dom (((LexBFS:CSeq G) . i) `1) & b in dom (((LexBFS:CSeq G) . i) `1) & (((LexBFS:CSeq G) . i) `1) . a < (((LexBFS:CSeq G) . i) `1) . b & j = (G .order()) -' ((((LexBFS:CSeq G) . i) `1) . b) holds
(((((LexBFS:CSeq G) . j) `2) . a),1) -bag <= (((((LexBFS:CSeq G) . j) `2) . b),1) -bag , InvLexOrder NAT

proof end;

:: Any value in our v2label corresponds to a vertex that we are
:: adjacent to in our in our vlabel

theorem Th52: :: LEXBFS:52

for G being finite _Graph
for i, j being Nat
for v being Vertex of G st j in (((LexBFS:CSeq G) . i) `2) . v holds
ex w being Vertex of G st
( w in dom (((LexBFS:CSeq G) . i) `1) & (((LexBFS:CSeq G) . i) `1) . w = j & v in G .AdjacentSet {w} )

proof end;

definition

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

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

end;

:: deftheorem Def18 defines with_property_L3 LEXBFS:def 18 :

theorem Th53: :: LEXBFS:53

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

proof end;

theorem Th54: :: LEXBFS:54

for G being finite chordal _Graph
for L being PartFunc of (the_Vertices_of G),NAT st L is with_property_L3 & dom L = the_Vertices_of G holds
for V being VertexScheme of G st V " = L holds
V is perfect

proof end;

theorem :: LEXBFS:55

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

proof end;

begin

definition

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

end;

definition

let G be finite _Graph;

func MCS:Init G -> MCS:Labeling of G equals :: LEXBFS:def 19
[{},((the_Vertices_of G) --> 0)];

proof end;

end;

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

definition

let G be finite _Graph;
let L be MCS:Labeling of G;

func MCS:PickUnnumbered L -> Vertex of G means :Def20: :: LEXBFS:def 20
it = choose (the_Vertices_of G) if dom (L `1) = the_Vertices_of G
otherwise ex S being non empty natural-membered finite set ex F being Function st
( S = rng F & F = (L `2) | ((the_Vertices_of G) \ (dom (L `1))) & it = choose (F " {(max S)}) );

proof end;

uniqueness ;
consistency ;

end;

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

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

proof end;

end;

:: deftheorem defines MCS:LabelAdjacent LEXBFS:def 21 :

definition

let G be finite _Graph;
let L be MCS:Labeling of G;
let v be Vertex of G;
let n be Nat;

func MCS:Update (L,v,n) -> MCS:Labeling of G means :Def22: :: LEXBFS:def 22
ex M being MCS:Labeling of G st
( M = [((L `1) +* (v .--> ((G .order()) -' n))),(L `2)] & it = MCS:LabelAdjacent (M,v) );

proof end;

uniqueness ;

end;

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

definition

let G be finite _Graph;
let L be MCS:Labeling of G;

func MCS:Step L -> MCS:Labeling of G equals :Def23: :: LEXBFS:def 23
L if G .order() <= card (dom (L `1))
otherwise MCS:Update (L,(MCS:PickUnnumbered L),(card (dom (L `1))));

coherence ;
consistency ;

end;

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

definition

let G be _Graph;

mode MCS:LabelingSeq of G -> ManySortedSet of NAT means :Def24: :: LEXBFS:def 24
for n being Nat holds it . n is MCS:Labeling of G;

proof end;

end;

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

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

end;

definition

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

end;

definition

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

proof end;

proof end;

end;

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

definition

let G be finite _Graph;

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

proof end;