| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/orders/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle range_real.pvs Sprache: 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 ¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28