Impressum bounded_interval_props.pvs Sprache: PVS

%------------------------------------------------------------------------------
% Properties of bounded intervals
%
%     Author: David Lester, Manchester University
%
%     Version 1.0            26/2/10   Initial Version
%------------------------------------------------------------------------------
bounded_interval_props: THEORY

BEGIN

  IMPORTING real_intervals_aux

  A,B: VAR bounded_interval
  a,b: VAR real

  bounded_interval1: LEMMA A(a) => inf(A) <= a AND a <= sup(A)
  bounded_interval2: LEMMA nonempty?[real](A) AND inf(A) < a AND a < sup(A)
                           => A(a)
  bounded_interval3: LEMMA nonempty?[real](A) => inf(A) <= sup(A)
  bounded_interval4: LEMMA disjoint?[real](A,B) AND A(a) AND B(b) AND a <= b =>
                           sup(A) <= inf(B)
  bounded_interval5: LEMMA disjoint?[real](A,B) AND A(a) AND B(b) AND a <= b =>
                           FORALL (x:(A),y:(B)): x < y

  bounded_interval_disjoint_union1:
     LEMMA disjoint?[real](A,B) AND bounded_interval?(union[real](A,B)) AND
           A(a) AND B(b) AND a <= b =>
           sup(A) = inf(B)

  bounded_interval_disjoint_union2:
     LEMMA disjoint?[real](A,B) AND bounded_interval?(union[real](A,B)) AND
           A(a) AND B(b) AND a <= b =>
           (A(sup(A)) OR B(inf(B)))

  bounded_interval_disjoint_union3:
     LEMMA disjoint?[real](A,B) AND bounded_interval?(union[real](A,B)) AND
           A(a) AND B(b) AND a <= b =>
           inf(union[real](A,B)) = inf(A)

  bounded_interval_disjoint_union4:
     LEMMA disjoint?[real](A,B) AND bounded_interval?(union[real](A,B)) AND
           A(a) AND B(b) AND a <= b =>
           sup(union[real](A,B)) = sup(B)

END bounded_interval_props

quality86%

¤ 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.1Bemerkung: (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.