SSL bounded_ints.pvs   Sprache: unbekannt

%
%
% Purpose: A proof that the least upper bound of an above bounded set 
%          of integers is in the set. This includes the JUDGEMENT that 
%          the least upper bound is an integer.
%
% Author: Alfons Geser National Institute of Aerospace, 2003
%
%

bounded_ints: THEORY

BEGIN

  IMPORTING reals@bounded_reals[int]

  SS: VAR sup_set

  sup_int_int: JUDGEMENT sup(SS) HAS_TYPE int

  sup_int_in_set: LEMMA
    in_set(sup(SS),SS)

  sup_int_is_in_set: JUDGEMENT sup(SS) HAS_TYPE (SS)

END bounded_ints

quality96%

[ Verzeichnis aufwärts0.8unsichere Verbindung  Übersetzung europäischer Sprachen durch Browser  ]