|
%------------------------------------------------------------------------------
% Sub-sequence Properties
%
% Author: David Lester, Manchester University, NIA, Université Perpignan
%
% All references are to WA Sutherland "Introduction to Metric and
% Topological Spaces", OUP, 1981
%
% Version 1.0 06/09/07 Initial Version
%------------------------------------------------------------------------------
subseq[T:TYPE]: THEORY
BEGIN
IMPORTING sequences[T],
reals@real_fun_preds[nat],
orders[sequence]
u,v,w: VAR sequence
i: VAR nat
f: VAR ({f:[nat->nat] | strict_increasing?(f)})
subseq?(v,u): bool = EXISTS f: FORALL i: v(i) = u(f(i))
subseq_index: LEMMA f(i) >= i
reflexive_subseq : LEMMA subseq?(u, u)
transitive_subseq : LEMMA subseq?(u, v) AND subseq?(v, w) => subseq?(u, w)
END subseq
¤ Dauer der Verarbeitung: 0.0 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.
|
