A proof that `o<` is well-founded on `o-p`s

The soundness of ACL2 rests in part on the well-foundedness of
`o<` on `o-p`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 `o<` is well-founded on
`o-p`s without having to assert any connection to the ordinals and that
is what we do here. The community book

Before outlining the above mentioned proof, we note that in the analogous
documentation page of ACL2 Version_2.7, there is a proof of the
well-foundedness of `o<` and `o-p`)
are order-isomorphic to the old ordinals (based on

Manolios, Panagiotis & Vroon, Daron. Ordinal arithmetic in ACL2. Kaufmann, Matt, & Moore, J Strother (eds). Fourth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2003), July, 2003. See http://www.cs.utexas.edu/users/moore/acl2/workshop-2003/.

We now give an outline of the above mentioned proof of well-foundedness.
We first observe three facts about `o<` on ordinals that have been
proved by ACL2 using only structural induction on lists. These theorems can
be proved by hand.

(defthm transitivity-of-o< (implies (and (o< x y) (o< y z)) (o< x z)) :rule-classes nil) (defthm non-circularity-of-o< (implies (o< x y) (not (o< y x))) :rule-classes nil) (defthm trichotomy-of-o< (implies (and (o-p x) (o-p y)) (or (equal x y) (o< x y) (o< y x))) :rule-classes nil)

These three properties establish that `o<` orders the `o-p`s.
To put such a statement in the most standard mathematical nomenclature, we can
define the macro:

(defmacro o<= (x y) `(not (o< ,y ,x)))

and then establish that

(defthm antisymmetry-of-o<= (implies (and (o-p x) (o-p y) (o<= x y) (o<= y x)) (equal x y)) :rule-classes nil :hints (("Goal" :use non-circularity-of-o<))) (defthm transitivity-of-o<= (implies (and (o-p x) (o-p y) (o<= x y) (o<= y z)) (o<= x z)) :rule-classes nil :hints (("Goal" :use transitivity-of-o<))) (defthm trichotomy-of-o<= (implies (and (o-p x) (o-p y)) (or (o<= x y) (o<= y x))) :rule-classes nil :hints (("Goal" :use trichotomy-of-o<)))

Crucially important to the proof of the well-foundedness of `o<` on
`o-p`s is the concept of ordinal-depth, abbreviated

(defun od (l) (if (o-finp l) 0 (1+ (od (o-first-expt l)))))

If the `o-p` `o-p` `o<`

(defun od-1 (x y) (if (o-finp x) (list x y) (od-1 (o-first-expt x) (o-first-expt y)))) (defthm od-implies-ordlessp (implies (and (o-p x) (< (od x) (od y))) (o< x y)) :hints (("Goal" :induct (od-1 x y))))

Remark. A consequence of this lemma is the fact that if `o<` descending sequence of `o-p`s,
then

*Lemma Main.* For each non-negative integer `o<`
well-orders the set of `o-p`s with

Base Case. n = 0. The o-ps with 0 od are the non-negative integers. On the non-negative integers, o< is the same as <. Induction Step. n > 0. We assume that o< well-orders the o-ps with od less than n. If o< does not well-order the o-ps with od less than or equal to n, consider, D, the set of infinite, o< descending sequences of o-ps of od less than or equal to n. The first element of a sequence in D has od n. Therefore, the o-first-expt of the first element of a sequence in D has od n-1. Since o<, by IH, well-orders the o-ps with od less than n, the set of o-first-expts 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 minimum integer such that for some infinite, o< descending sequence s of o-ps with od less than or equal to n, the first element of s has an o-first-expt of B and an o-first-coeff of k. Notice that k is positive. Having fixed B and k, let s = s(1), s(2), ... be an infinite, o< descending sequence of o-ps with od less than or equal to n such that s(1) has a o-first-expt of B and an o-first-coeff of k. We show that each s(i) has a o-first-expt of B and an o-first-coeff of k. For suppose that s(j) is the first member of s either with o-first-expt B and o-first-coeff m (m neq k) or with o-first-expt B' and o-first-coeff B' (B' neq B). If (o-first-expt s(j)) = B', then B' has od n-1 (otherwise, by IH, s would not be infinite) and B' is o< 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; but this contradicts the fact that s is descending. Thus, by the definition of o<, for s to be a decreasing sequence of o-ps, (o-rst s(1)), (o-rst s(2)), ... must be a decreasing sequence. We end by showing this cannot be the case. Let t = t(1), t(2), ... be an infinite sequence of o-ps such that t(i) = (o-rst s(i)). Then t is infinitely descending. Furthermore, t(1) begins with an o-p B' that is o< 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. `o<` well-orders the `o-p`s. Proof. Every
infinite,`o-p`s has the property that
each member has