## PROOF-OF-WELL-FOUNDEDNESS

a proof that `e0-ord-<` is well-founded on `e0-ordinalp`s
```Major Section:  MISCELLANEOUS
```

The soundness of ACL2 rests in part on the well-foundedness of `e0-ord-<` on `e0-ordinalp`s. This can be taken as obvious if one is willing to grant that those concepts are simply encodings of the standard mathematical notions of the ordinals below `epsilon-0` and its natural ordering relation. But it is possible to prove that `e0-ord-<` is well-founded on `e0-ordinalp`s without having to assert any connection to the ordinals and that is what we do here.

We first observe three facts about `e0-ord-<` on ordinals that have been proved by ACL2 using only structural induction on lists. These theorems can be proved by hand.

```(defthm transitivity-of-e0-ord-<
(implies (and (e0-ord-< x y)
(e0-ord-< y z))
(e0-ord-< x z))
:rule-classes nil)

(defthm non-circularity-of-e0-ord-<
(implies (e0-ord-< x y)
(not (e0-ord-< y x)))
:rule-classes nil)

(defthm trichotomy-of-e0-ord-<
(implies (and (e0-ordinalp x)
(e0-ordinalp y))
(or (equal x y)
(e0-ord-< x y)
(e0-ord-< y x)))
:rule-classes nil)
```
These three properties establish that `e0-ord-<` orders the `e0-ordinalp`s. To put such a statement in the most standard mathematical nomenclature, we can define the function:
```(defun e0-ord-<= (x y)
(or (equal x y) (e0-ord-< x y)))
```
and then establish that `e0-ord-<=` is a relation that is a simple, complete (i.e., total) order on ordinals by the following three lemmas, which have been proved:
```(defthm antisymmetry-of-e0-ord-<=
(implies (and (e0-ordinalp x)
(e0-ordinalp y)
(e0-ord-<= x y)
(e0-ord-<= y x))
(equal x y))
:rule-classes nil
:hints (("Goal" :use non-circularity-of-e0-ord-<)))

(defthm transitivity-of-e0-ord-<=
(implies (and (e0-ord-<= x y)
(e0-ord-<= y z))
(e0-ord-<= x z))
:rule-classes nil
:hints (("Goal" :use transitivity-of-e0-ord-<)))

(defthm trichotomy-of-e0-ord-<=
(implies (and (e0-ordinalp x)
(e0-ordinalp y))
(or (e0-ord-<= x y)
(e0-ord-<= y x)))
:rule-classes nil
:hints (("Goal" :use trichotomy-of-e0-ord-<)))
```
Crucially important to the proof of the well-foundedness of `e0-ord-<` on `e0-ordinalp`s is the concept of ordinal-depth, abbreviated `od`:
```(defun od (l) (if (atom l) 0 (1+ (od (car l)))))
```
If the `od` of an `e0-ordinalp` `x` is smaller than that of an `e0-ordinalp` `y`, then `x` is `e0-ord-<` `y`:
```(defthm od-implies-ordlessp
(implies (< (od x) (od y))
(e0-ord-< x y)))
```
Remark. A consequence of this lemma is the fact that if `s = s(1)`, `s(2)`, ... is an infinite, `e0-ord-<` descending sequence, then `od(s(1))`, `od(s(2))`, ... is a ``weakly'' descending sequence of non-negative integers: `od(s(i))` is greater than or equal to `od(s(i+1))`.

Lemma Main. For each non-negative integer `n`, `e0-ord-<` well-orders the set of `e0-ordinalp`s with `od` less than or equal to `n` .

``` Base Case.  n = 0.  The e0-ordinalps with 0 od are the non-negative
integers.  On the non-negative integers, e0-ord-< is the same as <.

Induction Step.  n > 0.  We assume that e0-ord-< well-orders the
e0-ordinalps with od less than n.

If e0-ord-< does not well-order the e0-ordinalps with od less
than or equal to n, consider, D, the set of infinite, e0-ord-<
descending sequences of e0-ordinalps of od less than or equal to n.
The first element of a sequence in D has od n.  Therefore, the car
of the first element of a sequence in D has od n-1.  Since
e0-ord-<, by IH, well-orders the e0-ordinalps with od less than n,
the set of cars of first elements of the sequences in D has a
minimal element, which we denote by B and which has od of n-1.

Let k be the least integer such that for some infinite,
e0-ord-< descending sequence s of e0-ordinalps with od less than
or equal to n, the first element of s begins with k occurrences
of B but not k+1 occurrences of B. Notice that k is positive.

Having fixed B and k, let s = s(1), s(2), ... be an infinite,
e0-ord-< descending sequence of e0-ordinalps with od less than
or equal to n such that B occurs exactly k times at the
beginning of s(1).

B occurs exactly k times at the beginning of each s(i).  For
suppose that s(j) is the first member of s with exactly m
occurrences of B at the beginning, m /= k.  If m = 0, then
the car of s(j) has od n-1 (otherwise, by IH, s would not be
infinite) and the car of s(j) is e0-ord-< B, contradicting
the minimality of B.  If 0 < m < k, then the fact that the
sequence beginning at s(j) is infinitely descending
contradicts the minimality of k.  If m > k, then s(j) is
greater than its predecessor, which has only k occurrences of
B at the beginning; but this contradicts the fact that s is
descending.

Let t = t(1), t(2), ... be the sequence of e0-ordinalps that
is obtained by letting t(i) be the result of removing B from
the front of s(i) exactly k times.  t is infinitely
descending.  Furthermore, t(1) begins with an e0-ordinalp B'
that is e0-ord-< B.  Since t is in D, t(1) has od n,
therefore, B' has od n-1.  But this contradicts the
minimality of B. Q.E.D.
```
Theorem. `e0-ord-<` well-orders the `e0-ordinalp`s. Proof. Every infinite,` e0-ord-<` descending sequence of `e0-ordinalp`s has the property that each member has `od` less than or equal to the `od`, `n`, of the first member of the sequence. This contradicts Lemma Main. Q.E.D.