| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/fault_tolerance/ (PVS Prover Version 6.0.9©) Datei vom 28.9.2014 mit Größe 515 B |
|
Quelle bounded_ints.pvsSprache: PVS |
|||||||||||||||
|
% % % 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
¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet am 2026-06-14) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-07-09