Suchen Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Haftungshinweis

Bemerkung: zur Agenda Produktseite wechseln Projekt Beratung

Suchen Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/lebesgue/ (Columbo Version 0.7^©) Datei vom 28.9.2014 mit Größe 1 kB

Quelle 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%

¤ Dauer der Verarbeitung: 0.0 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.