begin
Lm1:
for f being Function st f is one-to-one holds
card (dom f) = card (rng f)
Lm2:
for F being Function
for x, y being set holds dom (F +* (x .--> y)) = (dom F) \/ {x}
Lm3:
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
theorem
Lm4:
for a, b, c being real number st a < b holds
(c - b) + 1 < (c - a) + 1
theorem Th2:
for
n,
m,
k being
Nat st
m <= k &
n < m holds
k -' m < k -' n
:: deftheorem Def1 defines with_finite-elements LEXBFS:def 1 :
:: deftheorem Def2 defines .\/ LEXBFS:def 2 :
theorem Th3:
theorem Th4:
theorem Th5:
:: deftheorem Def3 defines natsubset-yielding LEXBFS:def 3 :
Lm5:
for F being Function st ( for x being set st x in rng F holds
x is finite ) holds
F is finite-yielding
theorem Th6:
:: deftheorem Def4 defines .incSubset LEXBFS:def 4 :
:: deftheorem Def5 defines max LEXBFS:def 5 :
Lm6:
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
Lm7:
for G being _Graph
for W being Walk of G holds W .length() = (W .reverse() ) .length()
Lm8:
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) )
begin
:: deftheorem Def6 defines iterative LEXBFS:def 6 :
:: deftheorem Def7 defines eventually-constant LEXBFS:def 7 :
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
begin
:: deftheorem Def8 defines preVNumberingSeq LEXBFS:def 8 :
:: deftheorem Def9 defines vertex-numbering LEXBFS:def 9 :
:: deftheorem Def10 defines .PickedAt LEXBFS:def 10 :
theorem Th11:
theorem Th12:
theorem
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
begin
:: 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:
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 b1 being Vertex of G st b1 = choose (the_Vertices_of G) ) & ( not dom (L `1 ) = the_Vertices_of G implies ex b1 being Vertex of G ex S being non empty finite Subset of (bool NAT ) ex B being non empty finite Subset of (Bags NAT ) ex F being Function st
( S = rng F & F = (L `2 ) | ((the_Vertices_of G) \ (dom (L `1 ))) & ( for x being finite Subset of NAT st x in S holds
x,1 -bag in B ) & ( for x being set st x in B holds
ex y being finite Subset of NAT st
( y in S & x = y,1 -bag ) ) & b1 = choose (F " {(support (max B,(InvLexOrder NAT )))}) ) ) )
uniqueness
for b1, b2 being Vertex of G holds
( ( dom (L `1 ) = the_Vertices_of G & b1 = choose (the_Vertices_of G) & b2 = choose (the_Vertices_of G) implies b1 = b2 ) & ( not dom (L `1 ) = the_Vertices_of G & ex S being non empty finite Subset of (bool NAT ) ex B being non empty finite Subset of (Bags NAT ) ex F being Function st
( S = rng F & F = (L `2 ) | ((the_Vertices_of G) \ (dom (L `1 ))) & ( for x being finite Subset of NAT st x in S holds
x,1 -bag in B ) & ( for x being set st x in B holds
ex y being finite Subset of NAT st
( y in S & x = y,1 -bag ) ) & b1 = 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 ) ) & b2 = choose (F " {(support (max B,(InvLexOrder NAT )))}) ) implies b1 = b2 ) )
consistency
for b1 being Vertex of G holds verum
;
end;
:: deftheorem Def12 defines LexBFS:PickUnnumbered LEXBFS:def 12 :
:: deftheorem defines LexBFS:Update LEXBFS:def 13 :
theorem Th25:
theorem Th26:
theorem Th27:
:: deftheorem Def14 defines LexBFS:Step LEXBFS:def 14 :
:: deftheorem Def15 defines LexBFS:LabelingSeq LEXBFS:def 15 :
:: deftheorem Def16 defines ``1 LEXBFS:def 16 :
:: deftheorem Def17 defines LexBFS:CSeq LEXBFS:def 17 :
theorem Th28:
Lm9:
for G being _Graph
for v being set holds
( dom ((LexBFS:Init G) `2 ) = the_Vertices_of G & ((LexBFS:Init G) `2 ) . v = {} )
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
theorem Th39:
theorem Th40:
theorem Th41:
theorem Th42:
theorem Th43:
theorem Th44:
theorem Th45:
theorem Th46:
theorem Th47:
theorem Th48:
theorem Th49:
theorem Th50:
theorem Th51:
theorem Th52:
:: deftheorem Def18 defines with_property_L3 LEXBFS:def 18 :
theorem Th53:
theorem Th54:
theorem
begin
:: deftheorem defines MCS:Init LEXBFS:def 19 :
:: deftheorem Def20 defines MCS:PickUnnumbered LEXBFS:def 20 :
:: 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:
ex
M being
MCS:Labeling of
G st
(
M = [((L `1 ) +* (v .--> ((G .order() ) -' n))),(L `2 )] &
it = MCS:LabelAdjacent M,
v );
existence
ex b1, M being MCS:Labeling of G st
( M = [((L `1 ) +* (v .--> ((G .order() ) -' n))),(L `2 )] & b1 = MCS:LabelAdjacent M,v )
uniqueness
for b1, b2 being MCS:Labeling of G st ex M being MCS:Labeling of G st
( M = [((L `1 ) +* (v .--> ((G .order() ) -' n))),(L `2 )] & b1 = MCS:LabelAdjacent M,v ) & ex M being MCS:Labeling of G st
( M = [((L `1 ) +* (v .--> ((G .order() ) -' n))),(L `2 )] & b2 = MCS:LabelAdjacent M,v ) holds
b1 = b2
;
end;
:: deftheorem Def22 defines MCS:Update LEXBFS:def 22 :
:: deftheorem Def23 defines MCS:Step LEXBFS:def 23 :
:: deftheorem Def24 defines MCS:LabelingSeq LEXBFS:def 24 :
:: deftheorem Def25 defines ``1 LEXBFS:def 25 :
:: deftheorem Def26 defines MCS:CSeq LEXBFS:def 26 :
theorem Th56:
theorem Th57:
theorem Th58:
theorem Th59:
theorem Th60:
theorem Th61:
theorem Th62:
theorem
theorem Th64:
theorem Th65:
theorem Th66:
theorem Th67:
theorem Th68:
theorem Th69:
theorem Th70:
theorem Th71:
theorem Th72:
theorem Th73:
theorem Th74:
theorem Th75:
theorem Th76:
:: deftheorem Def27 defines with_property_T LEXBFS:def 27 :
theorem
theorem
theorem