Quelle prelude_aux.pvs Sprache: 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

quality92%

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