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; see well-founded-relation. 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.