[PostScript]
Enumeration (T): **trait**
% Enumeration, comparison, and ordinal position
% operators, often used with "enumeration of"
**assumes** Integer
**includes** DerivedOrders
**introduces**
first, last: -> T
succ, pred: T -> T
ord: T -> Int
val: Int -> T
**asserts**
T **generated** **by** first, succ
T **generated** **by** last, pred
**forall** x, y: T
ord(first) == 0;
x \neq last => ord(succ(x)) = ord(x) + 1;
x \neq last => pred(succ(x)) = x;
val(ord(x)) == x;
x <= y == ord(x) <= ord(y);
x <= last
**implies**
TotalOrder
T **generated** **by** val
T **partitioned** **by** ord
**forall** x: T
x \neq first => succ(pred(x)) = x;
x \neq last => x < succ(x);
first <= x;
ord(x) >= 0
**converts**
first:->T, succ:T->T, pred:T->T, ord,
<=:T,T->Bool, >=:T,T->Bool,
<:T,T->Bool, >:T,T->Bool
exempting succ(last), pred(first)

[Table of Contents] [Index]