|
%------------------------------------------------------------------------------
% 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.15 Sekunden
(vorverarbeitet)
¤
|
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.
|
