|
min_posnat: THEORY
BEGIN
S: VAR (nonempty?[posnat])
n,a,x: VAR posnat
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
¤ Dauer der Verarbeitung: 0.18 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.
|
