|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% From any sequence one can extract %
% an increasing or a decreasing sub-sequence %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
monotone_subsequence : THEORY
BEGIN
IMPORTING sequence_props
u, s : VAR sequence[real]
i, j, n : VAR nat
%---------------------------------------------------
% If all the suffixes of v have a minimal element
% then v contains an increasing sub-sequence
%---------------------------------------------------
has_minimum(u, n) : bool =
EXISTS i : n <= i AND FORALL j : n <= j IMPLIES u(i) <= u(j)
minimum_prefix : LEMMA
EXISTS i : FORALL j : j <= n IMPLIES u(i) <= u(j)
minimum_suffix : LEMMA
has_minimum(u, n) IMPLIES has_minimum(u, 0)
v : VAR { u | FORALL n : has_minimum(u, n) }
%--- a minimum of the elements n, n+1, .... ---%
mini(v, n) : nat =
epsilon! i : n <= i AND FORALL j : n <= j IMPLIES v(i) <= v(j)
min_prop : LEMMA
n <= mini(v, n) AND FORALL j : n <= j IMPLIES v(mini(v, n)) <= v(j)
min_prop1 : COROLLARY n <= mini(v, n)
min_prop2 : COROLLARY n <= i IMPLIES v(mini(v, n)) <= v(i)
%--- subsequence ---%
h(v)(i) : RECURSIVE nat =
IF i = 0
THEN mini(v, 0)
ELSE mini(v, h(v)(i - 1) + 1)
ENDIF
MEASURE i
hseq(v) : sequence[real] = LAMBDA i : v(h(v)(i))
h_increasing : LEMMA strict_increasing?(h(v))
hseq_extraction : LEMMA subseq(hseq(v), v)
hseq_increasing : LEMMA increasing?(hseq(v))
%------------------------------------------------------
% If a sequence has no minimal element it contains a
% (strictly) decreasing sub-sequence
%------------------------------------------------------
w : VAR { u | not has_minimum(u, 0) }
no_minimum : LEMMA not has_minimum(w, n)
pick(w, n) : nat = epsilon! i : n <= i AND w(i) < w(n)
pick_prop : LEMMA n <= pick(w, n) AND w(pick(w, n)) < w(n)
pick_prop1 : COROLLARY n < pick(w, n)
pick_prop2 : COROLLARY w(pick(w, n)) < w(n)
%--- subsequence ---%
g(w)(i) : RECURSIVE nat =
IF i = 0
THEN pick(w, 0)
ELSE pick(w, g(w)(i - 1))
ENDIF
MEASURE i
gseq(w) : sequence[real] = LAMBDA i : w(g(w)(i))
g_increasing : LEMMA strict_increasing?(g(w))
gseq_extraction : LEMMA subseq(gseq(w), w)
gseq_decreasing : LEMMA strict_decreasing(gseq(w))
%------------------------
% Suffix starting at n
%------------------------
suffix(u, n) : sequence[real] = LAMBDA i : u(n+i)
suffix_subseq : LEMMA subseq(suffix(u, n), u)
suffix_hasmin : LEMMA
has_minimum(suffix(u, n), 0) IFF has_minimum(u, n)
%----------------
% Main theorem
%----------------
monotone_subsequence : THEOREM
EXISTS s : subseq(s, u) AND (increasing?(s) OR decreasing(s))
END monotone_subsequence
¤ Dauer der Verarbeitung: 0.26 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
