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