Major Section: ACL2-BUILT-INS
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.
To see the ACL2 definition of this function, see pf.
