## SET-WELL-FOUNDED-RELATION

set the default well-founded relation
Major Section: EVENTS

Examples:
(set-well-founded-relation lex2)

provided `lex2`

has been proved to be a well-founded relation
(see well-founded-relation). Note: This is an event! It does
not print the usual event summary but nevertheless changes the ACL2
logical world and is so recorded.

General Form:
(set-well-founded-relation rel)

where `rel`

has been proved to be a well-founded relation on objects
satisfying some predicate, `mp`

, as described in the documentation for
well-founded-relation. This macro is equivalent to
`(table acl2-defaults-table :well-founded-relation 'rel)`

,
and hence is local to any books in which is occurs;
see acl2-defaults-table.
This event sets the default well-founded relation to be that imposed
on `mp`

-measures by the relation `rel`

. Subsequently, if a recursively
defined function is submitted to `defun`

with no explicitly given
`:`

`well-founded-relation`

argument, `defun`

uses the default relation,
`rel`

, and the associated domain predicate `mp`

used in its
well-foundedness theorem. That is, the termination conditions
generated will require proving that the measure used by the `defun`

is
an `mp`

-measure and that in every recursive call the measure of the
arguments decreases according to `rel`

.