| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/orders/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle monotone_sequences.pvs Sprache: PVS |
|||||||||
|
% infinite ascending and descending sequences and their subsequences
% % Author: Alfons Geser (geser@nianet.org), 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.1 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28