Make-ord
A constructor for ordinals.
Make-ord is the ordinal constructor. Its use is recommended
instead of using cons to make ordinals. For a discussion of ordinals,
see ordinals.
For any ordinal, alpha < epsilon-0, there exist natural numbers p
and n, positive integers x1, x2, ..., xn and ordinals a1 > a2 >
... > an > 0 such that alpha > a1 and alpha = w^(a1)x1 + w^(a2)x2 +
... + w^(an)xn + p. We call a1 the ``first exponent'', x1 the
``first coefficient'', and the remainder (w^(a2)x2 + ... + w^(an)xn + p)
the ``rest'' of alpha.
(Make-ord fe fco rst) corresponds to the ordinal (w^fe)fco + rst.
Thus the first infinite ordinal, w (omega), is constructed by
(make-ord 1 1 0)
and, for example, the ordinal (w^2)5 + w2 + 7 is constructed by:
(make-ord 2 5 (make-ord 1 2 7)) .
The reason make-ord is used rather than cons is that it allows
us to reason more abstractly about the ordinals, without having to worry about
the underlying representation.
Function: make-ord
(defun make-ord (fe fco rst)
(declare (xargs :guard (and (posp fco) (o-p fe) (o-p rst))))
(cons (cons fe fco) rst))
