|
abstract_min[T: TYPE, f: [T -> nat], P: pred[T]]: THEORY
BEGIN
ASSUMING
T_ne: ASSUMPTION EXISTS (t: T): P(t)
ENDASSUMING
IMPORTING min_nat
TP: TYPE = {t: T | P(t)}
n: VAR nat
S,SS: VAR T
is_one(n): bool = (EXISTS (S: T): P(S) AND f(S) = n)
prep0: LEMMA nonempty?({n: nat | is_one(n)})
min_f: nat = min({n: nat | is_one(n)})
prep1: LEMMA nonempty?({S: T | f(S) = min_f AND P(S)})
minimal?(S): bool = P(S) AND
(FORALL (SS: T): P(SS) IMPLIES f(S) <= f(SS))
min: {S: T | minimal?(S)}
min_def: LEMMA minimal?(min)
min_in : LEMMA P(min)
min_is_min: LEMMA P(SS) IMPLIES f(min) <= f(SS)
END abstract_min
¤ Dauer der Verarbeitung: 0.82 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
