| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/ints/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 720 B |
|
Quelle abstract_max.pvs Sprache: PVS |
|||||||||
|
abstract_max[T: TYPE, N: nat, f: [T -> upto[N]], P: pred[T]]: THEORY
BEGIN ASSUMING T_ne: ASSUMPTION EXISTS (t: T): P(t) ENDASSUMING IMPORTING max_upto TP: TYPE = {t: T | P(t)} n: VAR upto[N] S,SS: VAR T is_one(n): bool = (EXISTS (S: T): P(S) AND f(S) = n) prep0: LEMMA nonempty?({n: upto[N] | is_one(n)}) max_f: upto[N] = max({n: upto[N] | is_one(n)}) prep1: LEMMA nonempty?({S: T | f(S) = max_f AND P(S)}) maximal?(S): bool = P(S) AND (FORALL (SS: T): P(SS) IMPLIES f(S) >= f(SS)) max: {S: T | maximal?(S)} max_def: LEMMA maximal?(max) max_in : LEMMA P(max) max_is_max: LEMMA P(SS) IMPLIES f(max) >= f(SS) END abstract_max ¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28