| products/sources/formale Sprachen/Coq/pretyping/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: Sprache: PVSOriginal von: 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 ([email protected]), National Institute of Aerospace % Date: 2003/04 % % remove_greatest, remove_greatest_monotone, intersection_greatest, and % intersection_least added 13 Jan 2005 by Jerry James ([email protected]), % 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.18 Sekunden (vorverarbeitet) ¤ |
Laden
Fehler beim Verzeichnis:
in der Quellcodebibliothek suchenDie farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
