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.
