SSL 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

quality91%

¤ 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.0.0Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.