A recognizer for the ordinals up to epsilon-0

Using the nonnegative integers and lists we can represent the
ordinals up to

The following essay is intended to provide intuition about ordinals. The
truth, of course, lies simply in the ACL2 definitions of `o<`.

Very intuitively, think of each non-zero natural number as by being denoted by a series of the appropriate number of strokes, i.e.,

0 0 1 | 2 || 3 ||| 4 |||| ... ...

Then ``

w |||||...,

i.e., an infinite number of strokes. Addition here is just concatenation.
Observe that adding one to the front of

We denote by

w*2 |||||... |||||...

One way to think of

2 w |||||... |||||... |||||... |||||... |||||... ...

We can analogously construct

3 2 2 2 2 w w ... w ... w ... w ... ...

Then we can construct

. . . w w w w w

That is epsilon-0.

Below we begin listing some ordinals up to

ordinal ACL2 representation 0 0 1 1 2 2 3 3 ... ... w '((1 . 1) . 0) w+1 '((1 . 1) . 1) w+2 '((1 . 1) . 2) ... ... w*2 '((1 . 2) . 0) (w*2)+1 '((1 . 2) . 1) ... ... w*3 '((1 . 3) . 0) (w*3)+1 '((1 . 3) . 1) ... ... 2 w '((2 . 1) . 0) ... ... 2 w +w*4+3 '((2 . 1) (1 . 4) . 3) ... ... 3 w '((3 . 1) . 0) ... ... w w '((((1 . 1) . 0) . 1) . 0) ... ... w 99 w +w +w4+3 '((((1 . 1) . 0) . 1) (99 . 1) (1 . 4) . 3) ... ... 2 w w '((((2 . 1) . 0) . 1) . 0) ... ... w w w '((((((1 . 1) . 0) . 1) . 0) . 1) . 0) ... ...

Observe that the sequence of `natp`). This is convenient because it means
that if a term, such as a measure expression for justifying a recursive
function (see o<) must produce an

The ordinals listed above are listed in ascending order. This is the
ordering tested by `o<`.

The ```cons` pairs whose final `cdr` is a natural
number, `o<`). Each `posp`).

Note that infinite ordinals should generally be created using the ordinal
constructor, `make-ord`, rather than `cons`. The functions `o-first-expt`, `o-first-coeff`, and `o-rst` are ordinals
destructors. Finally, the function `o-finp` and the macro `o-infp` tell whether an ordinal is finite or infinite, respectively.

The function `o<` compares two `cons`, the integer is the smaller.
Otherwise, `o<` recursively compares the `o-first-expt`s of the
ordinals to determine which is smaller. If they are the same, the `o-first-coeff`s of the ordinals are compared. If they are equal, the `o-rst`s of the ordinals are recursively compared.

Fundamental to ACL2 is the fact that `o<` is well-founded on

**Function: **

(defun o-p (x) (declare (xargs :guard t)) (if (o-finp x) (natp x) (and (consp (car x)) (o-p (o-first-expt x)) (not (eql 0 (o-first-expt x))) (posp (o-first-coeff x)) (o-p (o-rst x)) (o< (o-first-expt (o-rst x)) (o-first-expt x)))))