		Search-engine friendly clone of the ACL2 documentation.

Defsoft-implementation

Ensure-wfrel-o<

Ensure that a function, if logic-mode and recursive, has o< as well-founded relation.

Signature
(ensure-wfrel-o< fn ctx state) → (mv erp nothing state)
Arguments: fn — Guard (symbolp fn).
Returns: nothing — Type (null nothing).

For now, we only support logic-mode recursive second-order functions with the default well-founded relation (i.e. o<). This might be relaxed in the future.

Definitions and Theorems

Function: ensure-wfrel-o<

(defun ensure-wfrel-o< (fn ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (symbolp fn)))
 (let ((__function__ 'ensure-wfrel-o<))
  (declare (ignorable __function__))
  (b* ((wrld (w state))
       ((unless (logicp fn wrld)) (value nil))
       ((unless (irecursivep fn wrld))
        (value nil))
       (wfrel (well-founded-relation+ fn wrld))
       ((when (eq wfrel 'o<)) (value nil)))
   (er-soft+
    ctx t nil
    "The well-founded relation of the recursive function ~x0 ~
               must be O<, but it is ~x1 instead."
    fn wfrel))))

Theorem: null-of-ensure-wfrel-o<.nothing

(defthm null-of-ensure-wfrel-o<.nothing
  (b* (((mv ?erp ?nothing acl2::?state)
        (ensure-wfrel-o< fn ctx state)))
    (null nothing))
  :rule-classes :rewrite)