|
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.1 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.
|
