Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: max_finite_set_nat.pvs Sprache: PVS

Original von: 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

¤ Dauer der Verarbeitung: 0.0 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.