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

<PRE>
Natural (N): <b>trait</b>
  % The usual operators on the natural numbers,
  % starting from 0.
  <b>includes</b>
    <A HREF="ArithOps.html">ArithOps</A> (N),
    <A HREF="DecimalLiterals.html">DecimalLiterals</A>,
    <A HREF="Exponentiation.html">Exponentiation</A> (N),
    <A HREF="MinMax.html">MinMax</A> (N),
    <A HREF="TotalOrder.html">TotalOrder</A> (N)
  <b>introduces</b>
    __ \ominus __: N, N -&gt; N
  <b>asserts</b>
    N <b>generated</b> <b>by</b> 0, succ
    <b>forall</b> x, y: N
      succ(x) \neq 0;
      succ(x) = succ(y) == x = y;
      x &lt; succ(x);
      0 \ominus x == 0;
      x \ominus 0 == x;
      succ(x) \ominus succ(y) == x \ominus y
  <b>implies</b>
    <A HREF="NaturalOrder.html">NaturalOrder</A>
    N <b>generated</b> <b>by</b> 0, 1, +
    <b>forall</b> x, y: N
      x \ominus x == 0;
      x &lt;= y == x \ominus y = 0
    <b>converts</b> 1:-&gt;N, +, \ominus, *, div, mod,
        **, min, max, &lt;=, &gt;=, &lt;, &gt;
      exempting <b>forall</b> x: N
        div(x, 0), mod(x, 0)
</PRE>

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