environ
vocabularies HIDDEN, NUMBERS, FUNCT_1, CARD_1, RELAT_1, TARSKI, FUNCT_4, FUNCOP_1, XBOOLE_0, SUBSET_1, XXREAL_0, ARYTM_3, FINSET_1, ORDINAL1, ARYTM_1, NAT_1, ZFMISC_1, FINSEQ_1, UPROOTS, VALUED_0, RELAT_2, BAGORDER, PRE_POLY, WELLORD1, GLIB_000, GLIB_001, ORDINAL4, PBOOLE, PARTFUN1, MCART_1, FUNCT_2, FINSUB_1, CHORD, TOPGEN_1, RCOMP_1, FINSEQ_4, GRAPH_1, MEMBERED, ABIAN, LEXBFS, MATROID0, REAL_1, XCMPLX_0;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, MCART_1, CARD_1, ORDINAL1, NUMBERS, SUBSET_1, XXREAL_0, VALUED_0, XREAL_0, RELAT_1, RELAT_2, WELLORD1, MEMBERED, XXREAL_2, PARTFUN1, FUNCT_1, FUNCT_2, PBOOLE, FINSET_1, XCMPLX_0, NAT_1, NAT_D, FUNCOP_1, FUNCT_4, GLIB_000, GLIB_001, BAGORDER, TERMORD, UPROOTS, CHORD, FINSEQ_1, DOMAIN_1, ABIAN, RELSET_1, RECDEF_1, FINSUB_1, RFUNCT_3, PRE_POLY;
definitions TARSKI;
theorems AXIOMS, CARD_1, CARD_2, FUNCOP_1, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSET_1, FUNCT_1, FUNCT_2, FUNCT_4, GLIB_000, GLIB_001, INT_1, NAT_1, BAGORDER, TERMORD, ORDINAL1, PARTFUN1, PBOOLE, NAT_D, XREAL_0, RELAT_1, RELSET_1, TARSKI, XBOOLE_0, XBOOLE_1, XREAL_1, ZFMISC_1, ENUMSET1, CHORD, NECKLACE, FINSEQ_4, WELLORD1, UPROOTS, TREES_1, NAT_2, XXREAL_0, XXREAL_2, VALUED_0, MCART_1, FINSUB_1, SYSREL, GRFUNC_1;
schemes NAT_1, FUNCT_1, RECDEF_1, FRAENKEL, PBOOLE, FUNCT_2, CLASSES1;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1, FINSET_1, XXREAL_0, XREAL_0, XXREAL_2, NAT_1, INT_1, MEMBERED, FINSEQ_1, CARD_1, GLIB_000, ABIAN, BAGORDER, TERMORD, GLIB_001, CHORD, VALUED_0, FINSUB_1, PARTFUN1, RELSET_1, PRE_POLY, XTUPLE_0;
constructors HIDDEN, DOMAIN_1, FUNCT_4, XXREAL_2, BAGORDER, TERMORD, UPROOTS, CHORD, RECDEF_1, RFUNCT_3, RELSET_1, PBOOLE, XTUPLE_0, NUMBERS;
requirements HIDDEN, NUMERALS, SUBSET, BOOLE, REAL, ARITHM;
equalities GLIB_000, GLIB_001, FUNCOP_1;
expansions GLIB_000, GLIB_001, TARSKI;
Lm1:
for F being Function
for x, y being set holds dom (F +* (x .--> y)) = (dom F) \/ {x}
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
Lm3:
for a, b, c being Real 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
Lm4:
for G being _Graph
for W being Walk of G
for e, v being object st e Joins W .last() ,v,G holds
(W .addEdge e) .length() = (W .length()) + 1
Lm5:
for G being _Graph
for W being Walk of G holds W .length() = (W .reverse()) .length()
Lm6:
for G being _Graph
for W being Walk of G
for e, x being object st e Joins W .last() ,x,G holds
for n being Nat st n in dom W holds
( (W .addEdge e) . n = W . n & n in dom (W .addEdge e) )
definition
let G be
finite _Graph;
let L be
LexBFS:Labeling of
G;
existence
( ( dom (L `1) = the_Vertices_of G implies ex b1 being Vertex of G st b1 = the Element of 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 = the Element of F " {(support (max (B,(InvLexOrder NAT))))} ) ) )
uniqueness
for b1, b2 being Vertex of G holds
( ( dom (L `1) = the_Vertices_of G & b1 = the Element of the_Vertices_of G & b2 = the Element of 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 = the Element of F " {(support (max (B,(InvLexOrder NAT))))} ) & ex S being non empty finite Subset of (bool NAT) ex B being non empty finite Subset of (Bags NAT) ex F being Function st
( S = rng F & F = (L `2) | ((the_Vertices_of G) \ (dom (L `1))) & ( for x being finite Subset of NAT st x in S holds
(x,1) -bag in B ) & ( for x being set st x in B holds
ex y being finite Subset of NAT st
( y in S & x = (y,1) -bag ) ) & b2 = the Element of F " {(support (max (B,(InvLexOrder NAT))))} ) implies b1 = b2 ) )
consistency
for b1 being Vertex of G holds verum
;
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 = {} )