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.