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

[Table of Contents] [Index]