| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/orders/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 2 kB |
|
Quelle bounded_integers.pvs Sprache: PVS |
|||||||||
|
% every above (below) bounded, non-empty set of integers has a greatest
% (least) element. This also holds for any subtype T of the integers. % % Author: Alfons Geser (geser@nianet.org), National Institute of Aerospace % Date: 2003/04 % % remove_greatest, remove_greatest_monotone, intersection_greatest, and % intersection_least added 13 Jan 2005 by Jerry James (jamesj@acm.org), % University of Kansas bounded_integers[T: TYPE FROM int]: THEORY BEGIN IMPORTING non_empty_bounded_sets[T] Su, Su1, Su2: VAR (non_empty_bounded_above?) Sl, Sl1, Sl2: VAR (non_empty_bounded_below?) i, j: VAR T S: VAR set[T] c: VAR nat non_empty_bounded_above_has_greatest_lem: LEMMA S(i) & upper_bound?[T](j, S, <=) & c = j - i => has_greatest?(S, <=) non_empty_bounded_above_has_greatest: JUDGEMENT (non_empty_bounded_above?) SUBTYPE_OF (has_greatest?(<=)) non_empty_bounded_below_has_least_lem: LEMMA S(i) & lower_bound?[T](j, S, <=) & c = i - j => has_least?(S, <=) non_empty_bounded_below_has_least: JUDGEMENT (non_empty_bounded_below?) SUBTYPE_OF (has_least?(<=)) remove_least: LEMMA nonempty?(remove(least[T](restrict[[real, real], [T, T], bool](<=))(Sl), Sl)) => least[T](restrict[[real, real], [T, T], bool](<=))(Sl) < least[T](restrict[[real, real], [T, T], bool](<=))( remove(least[T](restrict[[real, real], [T, T], bool](<=))(Sl), Sl)) remove_least_monotone: LEMMA subset?(Sl1, Sl2) => subset?( remove(least[T](restrict[[real, real], [T, T], bool](<=))(Sl1), Sl1), remove(least[T](restrict[[real, real], [T, T], bool](<=))(Sl2), Sl2)) remove_greatest: LEMMA nonempty?(remove(greatest[T](restrict[[real, real], [T, T], bool](<=))(Su), Su)) => greatest[T](restrict[[real, real], [T, T], bool](<=))( remove(greatest[T](restrict[[real, real], [T, T], bool](<=))(Su), Su)) < greatest[T](restrict[[real, real], [T, T], bool](<=))(Su) remove_greatest_monotone: LEMMA subset?(Su1, Su2) => subset?( remove(greatest[T](restrict[[real, real], [T, T], bool](<=))(Su1), Su1), remove(greatest[T](restrict[[real, real], [T, T], bool](<=))(Su2), Su2)) intersection_greatest: LEMMA disjoint?(Su1, Su2) OR has_greatest?(intersection(Su1, Su2), <=) intersection_least: LEMMA disjoint?(Sl1, Sl2) OR has_least?(intersection(Sl1, Sl2), <=) END bounded_integers ¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28