% infinite ascending and descending sequences and their subsequences
%
% Author: Alfons Geser ([email protected]), National Institute of Aerospace
% Date: Dec 2004
monotone_sequences[T: TYPE]: THEORY
BEGIN
IMPORTING closure_ops[T]
n: VAR nat
x, y: VAR T
rel: VAR pred[[T, T]]
seq: VAR sequence[T]
lt: VAR (transitive?[T])
asc: VAR (preserves[nat, nat](<, <))
% these definitions do not require rel to be a partial order
ascending?(rel)(seq): bool =
FORALL n: rel(seq(n), seq(n + 1))
descending?(rel)(seq): bool =
FORALL n: rel(seq(n + 1), seq(n))
reflexive_closure_ascending: LEMMA
FORALL (seq: (ascending?(rel))): ascending?(reflexive_closure(rel))(seq)
reflexive_closure_descending: LEMMA
FORALL (seq: (descending?(rel))): descending?(reflexive_closure(rel))(seq)
ascending_lem: LEMMA
FORALL (seq: (ascending?(lt))): preserves(seq, <, lt)
descending_lem: LEMMA
FORALL (seq: (descending?(lt))): preserves(seq, <, converse(lt))
% subsequences
ascending_subsequence: THEOREM
FORALL (seq: (ascending?(lt))): ascending?(lt)(seq o asc)
descending_subsequence: THEOREM
FORALL (seq: (descending?(lt))): descending?(lt)(seq o asc)
END monotone_sequences
¤ Dauer der Verarbeitung: 0.3 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.
|
