# Well-founded-relation+

Enhanced variant of `well-founded-relation`.

- Signature
(well-founded-relation+ fn wrld) → well-founded-relation

- Arguments
`fn` — Guard (symbolp fn).
`wrld` — Guard (plist-worldp wrld).
- Returns
`well-founded-relation` — Type (symbolp well-founded-relation).

This returns the same result as `well-founded-relation`,
but it is guard-verified
and includes a run-time check (which should always succeed) on the result
that allows us to prove the return type theorem
without strengthening the guard on wrld.
This utility also includes a run-time check (which should always succeed)
on the form of the justification property of the function
that allows us to verify the guards
without strengthening the guard of wrld.
Furthermore, this utility causes an error if called on a symbol
that does not name a recursive logic-mode function;
the reason for ensuring logic-mode is that
recursive program-mode functions do not have a well-founded relation.

### Definitions and Theorems

**Function: **well-founded-relation+

(defun
well-founded-relation+ (fn wrld)
(declare (xargs :guard (and (symbolp fn) (plist-worldp wrld))))
(let
((__function__ 'well-founded-relation+))
(declare (ignorable __function__))
(if
(not (irecursivep+ fn wrld))
(raise "The function ~x0 is not recursive." fn)
(b*
((justification (getpropc fn 'justification nil wrld))
((unless (weak-justification-p justification))
(raise
"Internal error: ~
the justification ~x0 of ~x1 is not well-formed."
justification fn))
(well-founded-relation
(access justification justification :rel))
((unless (symbolp well-founded-relation))
(raise
"Internal error: ~
the well-founded relation ~x0 of ~x1 is not a symbol."
well-founded-relation fn)))
well-founded-relation))))

**Theorem: **symbolp-of-well-founded-relation+

(defthm
symbolp-of-well-founded-relation+
(b* ((well-founded-relation (well-founded-relation+ fn wrld)))
(symbolp well-founded-relation))
:rule-classes :rewrite)