min(S): {a: posnat | S(a) AND (FORALL x: S(x) IMPLIES a <= x)}
minimum?(a, S) : bool = S(a) AND (FORALL x: S(x) IMPLIES a <= x)
min_def : LEMMA min(S) = a IFF minimum?(a, S)
min_lem : LEMMA minimum?(min(S),S)
END min_posnat
¤ 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.0.1Bemerkung:
(vorverarbeitet)
¤
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.
