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

<PRE>
Integer (Int): <b>trait</b>
  % The usual (unbounded) integers operators 
  <b>includes</b>
    <A HREF="DecimalLiterals.html">DecimalLiterals</A> (Int <b>for</b> N),
    <A HREF="TotalOrder.html">TotalOrder</A> (Int)
  <b>introduces</b>
    0, 1: -&gt; Int
    succ, pred, -__, abs: Int -&gt; Int
    __+__, __-__, __*__: Int, Int -&gt; Int
    div, mod, min, max: Int, Int -&gt; Int
  <b>asserts</b> 
    Int <b>generated</b> <b>by</b> 0, succ, pred
    <b>forall</b> x, y: Int
      succ(pred(x)) == x;
      pred(succ(x)) == x;
      -0 == 0;
      -succ(x) == pred(-x);
      -pred(x) == succ(-x);
      abs(x) == max(-x, x);
      x + 0 == x;
      x + succ(y) == succ(x + y);
      x + pred(y) == pred(x + y);
      x - y == x + (-y);
      x * 0 == 0;
      x*succ(y) == (x*y) + x;
      x*pred(y) == (x*y) - x;
      y &gt; 0 =&gt; mod(x, y) + (div(x, y) * y) = x;
      y &gt; 0 =&gt; mod(x, y) &gt;= 0;
      y &gt; 0 =&gt; mod(x, y) &lt; y;
      min(x, y) == <b>if</b> x &lt;= y <b>then</b> x <b>else</b> y;
      max(x, y) == <b>if</b> x &lt;= y <b>then</b> y <b>else</b> x;
      x &lt; succ(x)
  <b>implies</b>
    <A HREF="AC.html">AC</A> (+, Int),
    <A HREF="AC.html">AC</A> (*, Int),
    <A HREF="AC.html">AC</A> (min, Int),
    <A HREF="AC.html">AC</A> (max, Int),
    <A HREF="RingWithUnit.html">RingWithUnit</A> (Int <b>for</b> T)
    Int <b>generated</b> <b>by</b> 1, +, -__:Int-&gt;Int
    <b>forall</b> x, y: Int
      x &lt; y == succ(x) &lt; succ(y);
      x &lt;= y == x &lt; succ(y)
    <b>converts</b>
      1, -__:Int-&gt;Int, __-__:Int,Int-&gt;Int, 
      abs, +, *, div, mod, min, max, &lt;=, &gt;=, &lt;, &gt;
</PRE>

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