|
max_finite_set_nat: THEORY
BEGIN
IMPORTING finite_sets@finite_sets_inductions[nat]
a,x: VAR nat
S: VAR non_empty_finite_set[nat]
fsmax(x,y:nat): nat = IF x <= y THEN y ELSE x ENDIF
maxrec(S): RECURSIVE nat =
IF empty?(sets.rest(S)) THEN choose(S)
ELSE fsmax(choose(S),maxrec(sets.rest(S)))
ENDIF
MEASURE (LAMBDA S: card(S))
max(S): {a: nat | S(a) AND (FORALL x: S(x) IMPLIES x <= a)}
maximum?(a, S) : bool = S(a) AND (FORALL x: S(x) IMPLIES x <= a)
max_def : LEMMA max(S) = a IFF maximum?(a, S)
max_lem : LEMMA maximum?(max(S),S)
max_in : LEMMA S(max(S))
END max_finite_set_nat
¤ Dauer der Verarbeitung: 0.14 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.
|
