Quelle  range_real.pvs

%-------------------------------------------------------------------------
%
%  The range theory, specialized for ranges of real numbers.
%
%  For PVS version 3.2.  February 9, 2005
%  ---------------------------------------------------------------------
%      Author: Jerry James (jamesj@acm.org), University of Kansas
%
%  EXPORTS
%  -------
%  prelude: finite_sets[real], orders[real], relations[real], sets[real]
%  finite_sets: finite_sets_inductions, finite_sets_minmax
%  orders: bounded_orders[real], minmax_orders[real], numbers_infinite,
%    range[real], range_real, relations_extra[real]
%
%-------------------------------------------------------------------------
range_real: THEORY
BEGIN

  IMPORTING range[real], numbers_infinite

  r: VAR real

  real_no_minimum: JUDGEMENT real SUBTYPE_OF (no_least)

  real_no_maximum: JUDGEMENT real SUBTYPE_OF (no_greatest)

  ntc_range_infinite: JUDGEMENT ntc_range SUBTYPE_OF infinite_set[real]
  nto_range_infinite: JUDGEMENT nto_range SUBTYPE_OF infinite_set[real]

END range_real