Quelle max_finite_set_nat.pvs Sprache: PVS

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

quality71%

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.