Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: bounded_interval_props.pvs Sprache: PVS

Original von: 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

¤ Dauer der Verarbeitung: 0.20 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.