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.
