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

[Table of Contents] [Index]