# O<

The well-founded less-than relation on ordinals up to epsilon-0

If x and y are both o-ps (see o-p) then
(o< x y) is true iff x is strictly less than y. o< is
well-founded on the `o-p`s. When x and y are both nonnegative
integers, o< is just the familiar ``less than'' relation (`<`).

o< plays a key role in the formal underpinnings of the ACL2 logic. In
order for a recursive definition to be admissible it must be proved to
``terminate.'' By terminate we mean that the arguments to the function ``get
smaller'' as the function recurs and this sense of size comparison must be
such that there is no ``infinitely descending'' sequence of ever smaller
arguments. That is, the relation used to compare successive arguments must be
well-founded on the domain being measured.

The most basic way ACL2 provides to prove termination requires the user to
supply (perhaps implicitly) a mapping of the argument tuples into the ordinals
with some ``measure'' expression in such a way that the measures of the
successive argument tuples produced by recursion decrease according to the
relation o<. The validity of this method rests on the well-foundedness
of o< on the `o-p`s.

Without loss of generality, suppose the definition in question introduces
the function f, with one formal parameter x (which might be a list
of objects). Then we require that there exist a measure expression, (m
x), that always produces an `o-p`. Furthermore, consider any
recursive call, (f (d x)), in the body of the definition. Let hyps
be the conjunction of terms, each of which is either the test of an `if`
in the body or else the negation of such a test, describing the path through
the body to the recursive call in question. Then it must be a theorem
that

(IMPLIES hyps (O< (m (d x)) (m x))).

When we say o< is ``well-founded'' on the `o-p`s we mean that
there is no infinite sequence of `o-p`s such that each is smaller than
its predecessor in the sequence. Thus, the theorems that must be proved about
f when it is introduced establish that it cannot recur forever because
each time a recursive call is taken (m x) gets smaller. From this, and
the syntactic restrictions on definitions, it can be shown (as on page 44 in
``A Computational Logic'', Boyer and Moore, Academic Press, 1979) that there
exists a function satisfying the definition; intuitively, the value assigned
to any given x by the alleged function is that computed by a sufficiently
large machine. Hence, the logic is consistent if the axiom defining f is
added.

See o-p for a discussion of the ordinals and how to compare two
ordinals.

The definitional principle permits the use of relations other than o<
but they must first be proved to be well-founded on some domain. See well-founded-relation-rule. Roughly put, alternative relations are shown
well-founded by providing an order-preserving mapping from their domain into
the ordinals. See defun for details on how to specify which
well-founded relation is to be used.

**Function: **o<

(defun o< (x y)
(declare (xargs :guard (and (o<g x) (o<g y))))
(cond ((o-finp x) (or (o-infp y) (< x y)))
((o-finp y) nil)
((not (equal (o-first-expt x)
(o-first-expt y)))
(o< (o-first-expt x) (o-first-expt y)))
((not (= (o-first-coeff x) (o-first-coeff y)))
(< (o-first-coeff x) (o-first-coeff y)))
(t (o< (o-rst x) (o-rst y)))))