products/sources/formale sprachen/Delphi/Bille 0.71/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: max_upto.pvs   Sprache: Unknown

max_upto[N: nat]: THEORY

  EXPORTING ALL

BEGIN

  IMPORTING min_nat

  S: VAR (nonempty?[upto[N]])
  n,a,x: VAR upto[N]

  max(S): {a: upto[N] | S(a) AND (FORALL x: S(x) IMPLIES a >= x)}

  maximum?(a, S) : bool = S(a) AND (FORALL x: S(x) IMPLIES a >= x)

  max_def         : LEMMA max(S) = a IFF maximum?(a, S)

  max_lem         : LEMMA maximum?(max(S), S)

END max_upto

[ Dauer der Verarbeitung: 0.0 Sekunden  (vorverarbeitet)  ]