## E0-ORD-<

the well-founded less-than relation on ordinals up to `epsilon-0`
```Major Section:  MISCELLANEOUS
```

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

`e0-ord-<` 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 recurses 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 `e0-ord-<`. The validity of this method rests on the well-foundedness of `e0-ord-<` on the `e0-ordinalp`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 `e0-ordinalp`. Furthermore, consider any recursive call, `(f (d x))`, in the body of the definition. Let `hyps` be the conjunction 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 (E0-ORD-< (m (d x)) (m x))).
```
When we say `e0-ord-<` is ``well-founded'' on the `e0-ordinalp`s we mean that there is no infinite sequence of `e0-ordinalp`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 e0-ordinalp for a discussion of the ordinals and how to compare two ordinals.

The definitional principle permits the use of relations other than `e0-ord-<` but they must first be proved to be well-founded on some domain. See well-founded-relation. 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.