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
