Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: prelude_aux.pvs Sprache: PVS

Original von: PVS^©

prelude_aux: THEORY
BEGIN
   px: VAR posreal
   x,y: VAR real
   i: VAR nat

   floor_le    : LEMMA x <= y IMPLIES floor(x) <= floor(y)

   floor_lt    : LEMMA x < y IMPLIES floor(x) < floor(y) + 1

   floor_div_le: LEMMA y >= 1 IMPLIES floor(px/y) <= px

   floor_div_lt: LEMMA y > 1  IMPLIES floor(px/y) < px

   floor_le_floor: LEMMA y >= 1 IMPLIES floor(px/y) <= floor(px)

   floor_lt_floor_int: LEMMA i > 1 AND  x >= i IMPLIES
                           floor(x / i) < floor(x)

   %% this is a generalization of what is already in the prelude
   floor_small: LEMMA  abs(x) < abs(y) IMPLIES
                         floor(x/y) = IF x/y >= 0 THEN 0 ELSE -1 ENDIF

END prelude_aux

¤ Dauer der Verarbeitung: 0.2 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.