Show that a relation is well-founded on a set

See rule-classes for a general discussion of rule classes, including how they are used to build rules from formulas and a discussion of the various keywords in a rule class description.

Example: (defthm lex2p-is-well-founded-relation (and (implies (pairp x) (o-p (ordinate x))) (implies (and (pairp x) (pairp y) (lex2p x y)) (o< (ordinate x) (ordinate y)))) :rule-classes :well-founded-relation)

The example above creates a

Exactly two general forms are recognized:

General Forms (AND (IMPLIES (mp x) (O-P (fn x))) ; Property 1 (IMPLIES (AND (mp x) ; Property 2 (mp y) (rel x y)) (O< (fn x) (fn y)))),

or

(AND (O-P (fn x)) ; Property 1 (IMPLIES (rel x y) ; Property 2 (O< (fn x) (fn y))))

where

Note: We are very rigid when checking that the submitted formula is of one
of these forms. For example, in the first form, we insist that all the
conjuncts appear in the order shown above. Thus, interchanging the two
properties in the top-level conjunct or rearranging the hypotheses in the
second conjunct both produce unrecognized forms. The requirement that each

We also insist that the new ordering be embedded into the ordinals as
handled by `o-p` and `o<` and not some into previously admitted
user-defined well-founded set and relation. This restriction should pose no
hardship. If

`o<`. (See o<.)
Thus, the general form of a

Such well-founded relations are used in the admissibility test for recursive functions, in particular, to show that the recursion terminates. To illustrate how such information may be used, consider a generic function definition

(defun g (x) (if (test x) (g (step x)) (base x))).

If

(mp (m x)), ; Defun-goal-1

and that the argument to

(implies (test x) (rel (m (step x)) (m x))). ; Defun-goal-2

If

Suppose now that a `defun`? There are two ways. First,
an `xargs` keyword to the `defun` event allows the specification
of a

(defun g (x) (declare (xargs :well-founded-relation rel)) (if (test x) (g (step x)) (base x)))

Alternatively, `ACL2-defaults-table` by
executing the event

(set-well-founded-relation rel).

When a `defun` event does not explicitly specify the relation in its
`xargs` the default relation is used. When ACL2 is initialized, the
default relation is `o<`.

Finally, though it is probably obvious, we now show that

(defun g (x) (declare (xargs :well-founded-relation o< :measure (fn (m x)))) (if (test x) (g (step x)) (base x)))

Proof that

(o-p (fn (m x))) ; *1

and

(implies (test x) ; *2 (o< (fn (m (step x))) (fn (m x)))).

But *1 can be proved by instantiating

(implies (mp (m x)) (o-p (fn (m x)))),

and then relieving the hypothesis with

Similarly, *2 can be proved by instantiating

(implies (and (mp (m (step x))) (mp (m x)) (rel (m (step x)) (m x))) (o< (fn (m (step x))) (fn (m x))))

and relieving the first two hypotheses by appealing to two instances of

(implies (rel (m (step x)) (m x)) (o< (fn (m (step x))) (fn (m x)))).

By chaining this together with

(implies (test x) (rel (m (step x)) (m x)))

we obtain *2. Q.E.D.

- Nat-list-<
- An alternate well-founded-relation that allows lists of naturals to be used directly as measures.