environ
vocabularies HIDDEN, NUMBERS, FINSEQ_2, XBOOLE_0, SUBSET_1, FINSEQ_1, ABIAN, INT_1, ARYTM_1, RELAT_1, XXREAL_0, ARYTM_3, GRAPH_2, FUNCT_1, CARD_1, GRAPH_1, GLIB_000, STRUCT_0, TREES_2, ORDINAL4, NAT_1, PARTFUN1, TARSKI, RELAT_2, FINSET_1, FUNCT_4, FUNCOP_1, ZFMISC_1, FINSEQ_6, GRAPH_3;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCOP_1, FUNCT_4, INT_1, NAT_1, FINSET_1, FINSEQ_1, FINSEQ_2, FINSEQ_4, XXREAL_2, STRUCT_0, GRAPH_1, GRAPH_2, MSSCYC_1, ABIAN, XXREAL_0;
definitions TARSKI, PARTFUN1, GRAPH_1, GRAPH_2, MSSCYC_1, XBOOLE_0;
theorems TARSKI, ZFMISC_1, RELAT_1, FUNCT_1, FUNCT_2, NAT_1, FUNCOP_1, FUNCT_4, PARTFUN1, CARD_1, CARD_2, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_4, FINSEQ_5, GRAPH_1, GRAPH_2, MSSCYC_1, ABIAN, RELSET_1, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, ORDINAL1, XXREAL_2, INT_1, XTUPLE_0;
schemes NAT_1, DOMAIN_1, XBOOLE_0, RECDEF_1;
registrations XBOOLE_0, ORDINAL1, FUNCOP_1, FINSET_1, XXREAL_0, XREAL_0, NAT_1, INT_1, CARD_1, MEMBERED, FINSEQ_1, ABIAN, GRAPH_2, MSSCYC_1, RELAT_1, XXREAL_2, STRUCT_0, RELSET_1, FINSEQ_2;
constructors HIDDEN, WELLORD2, FUNCT_4, FINSEQ_4, ABIAN, GRAPH_2, MSSCYC_1, XXREAL_2, RELSET_1, PRE_POLY;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
equalities GRAPH_1, GRAPH_2, FUNCOP_1;
expansions TARSKI, GRAPH_1, GRAPH_2, MSSCYC_1, XBOOLE_0;
Lm1:
for p being FinSequence
for m, n being Nat st 1 <= m & m <= n + 1 & n <= len p holds
( (len ((m,n) -cut p)) + m = n + 1 & ( for i being Nat st i < len ((m,n) -cut p) holds
((m,n) -cut p) . (i + 1) = p . (m + i) ) )
Lm2:
for G being Graph
for p being Path of G
for n, m being Nat st 1 <= n & n <= len p & 1 <= m & m <= len p & n <> m holds
p . n <> p . m
Lm3:
for G being Graph
for c being Chain of G
for vs being FinSequence of the carrier of G st vs is_vertex_seq_of c holds
for n being Nat st 1 <= n & n <= len c holds
( 1 <= n & n <= len vs & 1 <= n + 1 & n + 1 <= len vs & ( ( vs . n = the Target of G . (c . n) & vs . (n + 1) = the Source of G . (c . n) ) or ( vs . n = the Source of G . (c . n) & vs . (n + 1) = the Target of G . (c . n) ) ) )
Lm4:
for G being finite Graph
for c being cyclic Path of G
for vs being FinSequence of the carrier of G
for v being Vertex of G st vs is_vertex_seq_of c & v in rng vs holds
Degree (v,(rng c)) is even
Lm5:
for G being Graph
for c being Element of G -CycleSet
for v being Vertex of G st v in G -VSet (rng c) holds
rng (Rotate (c,v)) = rng c