environ
vocabularies HIDDEN, NUMBERS, FINSEQ_1, XBOOLE_0, SUBSET_1, NAT_1, ARYTM_3, XXREAL_0, INT_1, ARYTM_1, RELAT_1, FUNCT_1, TARSKI, FINSET_1, CARD_1, ORDINAL1, ORDINAL4, GRAPH_1, STRUCT_0, TREES_2, PARTFUN1, GLIB_000, FINSEQ_2, ZFMISC_1, FINSEQ_4, FUNCT_4, GRAPH_2;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0, XXREAL_0, RELAT_1, RELSET_1, XXREAL_2, FINSEQ_1, FUNCT_1, PARTFUN1, FUNCT_2, ZFMISC_1, FINSEQ_2, FINSEQ_4, FUNCT_7, FINSET_1, INT_1, NAT_1, NAT_D, RECDEF_1, STRUCT_0, GRAPH_1;
definitions TARSKI, GRAPH_1, XBOOLE_0, FINSEQ_1;
theorems TARSKI, ENUMSET1, NAT_1, FINSEQ_1, FINSEQ_2, GRAPH_1, RELAT_1, FUNCT_1, GRFUNC_1, FUNCT_2, INT_1, CARD_1, CARD_2, FINSEQ_3, FINSEQ_4, ZFMISC_1, XBOOLE_0, XBOOLE_1, XCMPLX_1, ORDINAL1, XREAL_1, FINSEQ_5, XXREAL_0, MEMBERED, FUNCT_7, PARTFUN1, XXREAL_2, XREAL_0, NAT_D, XTUPLE_0;
schemes NAT_1, FINSEQ_1, FUNCT_1;
registrations XBOOLE_0, RELAT_1, FUNCT_1, FINSET_1, XXREAL_0, XREAL_0, NAT_1, INT_1, CARD_1, FINSEQ_1, FINSEQ_6, GRAPH_1, NUMBERS, MEMBERED, VALUED_0, XXREAL_2, STRUCT_0, RELSET_1, ORDINAL1;
constructors HIDDEN, WELLORD2, RECDEF_1, FINSEQ_4, FINSEQ_6, GRAPH_1, FUNCT_7, XXREAL_2, NAT_D, RELSET_1, FINSEQ_2;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities FINSEQ_2, FINSEQ_1;
expansions TARSKI, GRAPH_1, FINSEQ_1;
theorem Th1:
for
m,
k,
n being
Nat holds
( (
m + 1
<= k &
k <= n ) iff ex
i being
Nat st
(
m <= i &
i < n &
k = i + 1 ) )
Lm1:
for m, n being Nat
for F being finite set st F = { k where k is Nat : ( m <= k & k <= m + n ) } holds
card F = n + 1
theorem Th5:
for
m,
n,
l being
Nat st 1
<= l &
l <= n holds
(Sgm { kk where kk is Nat : ( m + 1 <= kk & kk <= m + n ) } ) . l = m + l
Lm2:
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) ) )
then Lm4:
<*1,2*> is TwoValued
by Lm3;
Lm5:
now for i being Nat st 1 <= i & i + 1 <= len <*1,2*> holds
<*1,2*> . i <> <*1,2*> . (i + 1)
let i be
Nat;
( 1 <= i & i + 1 <= len <*1,2*> implies <*1,2*> . i <> <*1,2*> . (i + 1) )set p =
<*1,2*>;
assume that A1:
1
<= i
and A2:
i + 1
<= len <*1,2*>
;
<*1,2*> . i <> <*1,2*> . (i + 1)
i + 1
<= 1
+ 1
by A2, FINSEQ_1:44;
then
i <= 1
by XREAL_1:6;
then A3:
i = 1
by A1, XXREAL_0:1;
then
<*1,2*> . i = 1
by FINSEQ_1:44;
hence
<*1,2*> . i <> <*1,2*> . (i + 1)
by A3, FINSEQ_1:44;
verum
end;
Lm6:
<*1,2*> is Alternating
by Lm5;
theorem
for
G being
Graph for
v1,
v2,
v3,
v4 being
Element of
G for
e being
set st
e joins v1,
v2 &
e joins v3,
v4 & not (
v1 = v3 &
v2 = v4 ) holds
(
v1 = v4 &
v2 = v3 ) ;
Lm7:
for D being non empty set st ( for x, y being set st x in D & y in D holds
x = y ) holds
card D = 1
Lm8:
for G being Graph
for v being Element of G holds <*v*> is_vertex_seq_of {}
by FINSEQ_1:39;
:: The following chain:
:: .--->.
:: ^ |
:: | v
:: .--->.<---.--->.
:: | ^
:: v |
:: .--->.
:: is a case in point: