Nach dem Mausklick ist die Projektion eines vierdimensionalen Würfels zu sehen max_bounded_posnat.pvs
Sprache: PVS
max_bounded_posnat: THEORY BEGIN
a,x,y,n,UB: VAR posnat
S: VAR {A: (nonempty?[posnat]) | EXISTS UB: FORALL (y: (A)): y <= UB}
bnd(S): { a | FORALL (x: (S)): x <= a}
max_rec(S,(i:{j: posnat | j >= choose(S)})): RECURSIVE posnat = IF S(i) THEN i ELSE max_rec(S,i-1) ENDIF MEASURE i - choose(S)
m: VAR nat
max_rec_in: LEMMA n >= choose(S) AND m = n - choose(S) IMPLIES S(max_rec(S, n))
max_rec_bnd: LEMMA n >= x AND n >= choose(S) AND S(x) AND m >= n - x IMPLIES x <= max_rec(S, n)
max(S): {a: posnat | 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_bounded_posnat
¤ 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.0.0Bemerkung:
(vorverarbeitet)
¤
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.
