[<A HREF="ArithOps.ps">PostScript</A>]

<PRE>
ArithOps (N): <b>trait</b>
  % Defines operators div and mod relative to + and *
  % for positive denominators
  <b>assumes</b> <A HREF="TotalOrder.html">TotalOrder</A> (N)
  <b>includes</b> <A HREF="Multiplication.html">Multiplication</A> (N)
  <b>introduces</b>
    div, mod: N, N -&gt; N
  <b>asserts</b> <b>forall</b> x, y: N
    y &gt; 0
      =&gt; (0 &lt;= mod(x, y)
          /\ mod(x, y) &lt; y
          /\ (mod(x, y) + (div(x, y) * y)) = x)
</PRE>

[<A HREF="toc.html">Table of Contents</A>] [<A HREF="index.html">Index</A>]