# Set-well-founded-relation

Set the default well-founded relation

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

provided lex2 has been proved to be a well-founded relation (see well-founded-relation-rule). 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; see well-founded-relation-rule.
This macro is equivalent to (table acl2-defaults-table
:well-founded-relation 'rel), and hence is `local` to any books
and `encapsulate` events in which it 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.