| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/structures/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle seq2set.pvs Sprache: PVS |
|||||||||
|
seq2set[T: TYPE]: THEORY
%---------------------------------------------------------------------------- % % Utility functions for converting to/from sets and sequences % % Version 1.0, January, 2004 % Author: Kristin Y. Rozier %---------------------------------------------------------------------------- BEGIN IMPORTING seqs[T] fs: VAR finite_sequence[T] seq2set(fs): finite_set[T] = {s: T | (EXISTS (kk: below(length(fs))): fs(kk) = s)} seq2set_lem: LEMMA (FORALL (ii: below(length(fs))): seq2set(fs)(fs(ii))) card_seq2set: LEMMA card[T](seq2set(fs)) <= length(fs) ss: VAR ne_seqs % length > 0 JUDGEMENT seq2set(ss) HAS_TYPE (nonempty?[T]) END seq2set minmax_seq2set[T: TYPE+, <= : (total_order?[T]) ]: THEORY BEGIN IMPORTING sort_seq_lems[T,<=], finite_sets@finite_sets_minmax[T,<=], seq2set[T] ne_fs: VAR ne_seqs[T] minmax_seq2set: LEMMA min[T,<=](seq2set(ne_fs)) = min(ne_fs) AND max[T,<=](seq2set(ne_fs)) = max(ne_fs) END minmax_seq2set ¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28