a constructor for ordinals.
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.