% @(#)$Id: Floor.lsl,v 1.1 1995/11/13 23:31:09 leavens Exp $
Floor(int): trait
  includes Rational(int for Int)
  introduces
    floor: Q -> int
  asserts
    \forall q: Q
      (q-1) < (floor(q)/1);
      (floor(q)/1) <= q;
  implies
    \forall n: int, a,b: P
      floor(n/1) == n;
      floor(floor(n/a)/b) == floor(n/(a*b));

[Index]

HTML generated using lcpp2html.