get-well-founded-relation-tests

(in-package "ACL2")

(assert-equal (get-well-founded-relation 'len (w state))
  'o<)

(must-succeed* (defun f
    (x)
    (declare (xargs :measure (nfix (- 10 x))))
    (if (and (natp x) (< x 10))
      (f (1+ x))
      nil))
  (assert-equal (get-well-founded-relation 'f (w state)) 'o<))

(must-succeed* (defun o-p$ (x) (o-p x))
  (defun o<$ (x y) (o< x y))
  (defun id (x) x)
  (defthm o<$-is-well-founded-relation
    (and (implies (o-p$ x) (o-p (id x)))
      (implies (and (o-p$ x) (o-p$ y) (o<$ x y))
        (o< (id x) (id y))))
    :rule-classes :well-founded-relation)
  (defun f
    (x)
    (declare (xargs :well-founded-relation o<$))
    (if (zp x)
      nil
      (f (1- x))))
  (assert-equal (get-well-founded-relation 'f (w state)) 'o<$))