Quelle non_empty_bounded_sets.pvs Sprache: PVS

% non-empty sets of reals that are bounded from above or below.
% These are exactly the sets that have least upper (greatest lower) bounds.
%
% Author: Alfons Geser (geser@nianet.org), National Institute of Aerospace
% Date: Dec 2004
%
% non_empty_finite_bounded_above and non_empty_finite_bounded_below added
% 13 Jan 2005 by Jerry James (james@acm.org), University of Kansas

non_empty_bounded_sets[T: TYPE FROM real]: THEORY

BEGIN

  IMPORTING total_lattices[T, <=]

  non_empty_bounded_above?(S: set[T]): bool =
    nonempty?[T](S) & bounded_above?[T](<=)(S)

  non_empty_bounded_below?(S: set[T]): bool =
    nonempty?[T](S) & bounded_below?[T](<=)(S)

  non_empty_bounded_above_is_nonempty: JUDGEMENT
    (non_empty_bounded_above?) SUBTYPE_OF (nonempty?[T])

  non_empty_bounded_above_is_bounded_above: JUDGEMENT
    (non_empty_bounded_above?) SUBTYPE_OF (bounded_above?[T](<=))

  non_empty_bounded_below_is_nonempty: JUDGEMENT
    (non_empty_bounded_below?) SUBTYPE_OF (nonempty?[T])

  non_empty_bounded_below_is_bounded_below: JUDGEMENT
    (non_empty_bounded_below?) SUBTYPE_OF (bounded_below?[T](<=))

  non_empty_finite_bounded_above: JUDGEMENT
    non_empty_finite_set[T] SUBTYPE_OF (non_empty_bounded_above?)

  non_empty_finite_bounded_below: JUDGEMENT
    non_empty_finite_set[T] SUBTYPE_OF (non_empty_bounded_below?)

END non_empty_bounded_sets

quality91%

¤ Dauer der Verarbeitung: 0.8 Sekunden (vorverarbeitet) ¤

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.