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

<PRE>
IntCycle (first, last, N): <b>trait</b>
  % A finite subrange of the integers that includes 0,
  % and wraps at succ(last)
  <b>includes</b>
    <A HREF="ArithOps.html">ArithOps</A> (N),
    <A HREF="DecimalLiterals.html">DecimalLiterals</A>,
    <A HREF="MinMax.html">MinMax</A> (N),
    <A HREF="TotalOrder.html">TotalOrder</A> (N)
  <b>introduces</b>
    first, last: -&gt; N
    pred, -__, abs: N -&gt; N
    __-__: N, N -&gt; N
  <b>asserts</b>
    N <b>generated</b> <b>by</b> 0, succ
    <b>forall</b> x, y: N
      succ(last) == first;
      pred(succ(x)) == x;
      succ(pred(x)) == x;
      -0 == 0;
      -succ(x) == pred(-x);
      abs(x) == <b>if</b> x &lt; 0 <b>then</b> -x <b>else</b> x;
      x - y == x + (-y);
      x \neq last =&gt; x &lt; succ(x)
  <b>implies</b>
    <A HREF="Distributive.html">Distributive</A> (+, *, N),
    <A HREF="RingWithUnit.html">RingWithUnit</A> (N <b>for</b> T)
    N <b>generated</b> <b>by</b> 0, pred
    <b>forall</b> x: N
      pred(first) == last;
      first &lt;= x;
      x &lt;= last;
      -(-x) == x
    <b>converts</b>
      pred, -__:N-&gt;N, abs, __-__:N,N-&gt;N,
      1:-&gt;N, +, *, max, min, &lt;=, &gt;=, &lt;, &gt;
</PRE>

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