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

<PRE>
NaturalOrder (N): <b>trait</b>
  % The natural numbers with an ordering
  <b>includes</b>
    <A HREF="Enumerable.html">Enumerable</A> (N),
    <A HREF="TotalOrder.html">TotalOrder</A> (N)
  <b>asserts</b> <b>forall</b> x: N
    x &lt; succ(x)
  <b>implies</b>
    <A HREF="Infinite.html">Infinite</A> (N)
    <b>forall</b> x, y: N 
      0 &lt;= x;
      x &lt; succ(y) == x &lt;= y;
      succ(x) &lt; succ(y) == x &lt; y
    <b>converts</b> &lt;=, &gt;=, &lt;, &gt;
</PRE>

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