Filtering...

defarbrec

books/std/util/tests/defarbrec

Included Books

defarbrec theorem-namep assert-equal must-fail must-succeed-star
other
(in-package "ACL2")
include-book
(include-book "../defarbrec")
include-book
(include-book "std/system/theorem-namep" :dir :system)
include-book
(include-book "std/testing/assert-equal" :dir :system)
include-book
(include-book "std/testing/must-fail" :dir :system)
include-book
(include-book "std/testing/must-succeed-star" :dir :system)
other
(must-succeed* (defstub a (*) => *)
  (defstub b (*) => *)
  (defstub c (* *) => *)
  (defstub d (*) => *)
  (defarbrec f
    (x)
    (if (a x)
      (b x)
      (c x (f (d x))))))
other
(must-succeed* (defstub a (* *) => *)
  (defstub b (* *) => *)
  (defstub c (* * *) => *)
  (defstub dx (* *) => *)
  (defstub dy (* *) => *)
  (defarbrec f
    (x y)
    (if (a x y)
      (b x y)
      (c x y (f (dx x y) (dy x y))))))
other
(must-succeed* (defstub a (* * *) => *)
  (defstub b (* * *) => *)
  (defstub c (* * * *) => *)
  (defstub dx (* * *) => *)
  (defstub dy (* * *) => *)
  (defstub dz (* * *) => *)
  (defarbrec f
    (x y z)
    (if (a x y z)
      (b x y z)
      (c x y z (f (dx x y z) (dy x y z) (dz x y z))))))
other
(must-succeed* (defstub a (*) => *)
  (defstub b (*) => *)
  (defstub c (* *) => *)
  (defstub d (*) => *)
  (defarbrec f
    (x)
    (if (a x)
      (c x (f (d x)))
      (b x))))
other
(must-succeed* (defstub a (* *) => *)
  (defstub b (* *) => *)
  (defstub c (* * *) => *)
  (defstub dx (* *) => *)
  (defstub dy (* *) => *)
  (defarbrec f
    (x y)
    (if (a x y)
      (c x y (f (dx x y) (dy x y)))
      (b x y))))
other
(must-succeed* (defstub a (* * *) => *)
  (defstub b (* * *) => *)
  (defstub c (* * * *) => *)
  (defstub dx (* * *) => *)
  (defstub dy (* * *) => *)
  (defstub dz (* * *) => *)
  (defarbrec f
    (x y z)
    (if (a x y z)
      (c x y z (f (dx x y z) (dy x y z) (dz x y z)))
      (b x y z))))
other
(must-succeed* (defstub a (*) => *)
  (defstub b (*) => *)
  (defstub d (*) => *)
  (defarbrec f
    (x)
    (if (a x)
      (b x)
      (f (d x)))))
other
(must-succeed* (defstub a (* *) => *)
  (defstub b (* *) => *)
  (defstub dx (* *) => *)
  (defstub dy (* *) => *)
  (defarbrec f
    (x y)
    (if (a x y)
      (b x y)
      (f (dx x y) (dy x y)))))
other
(must-succeed* (defstub a (* * *) => *)
  (defstub b (* * *) => *)
  (defstub dx (* * *) => *)
  (defstub dy (* * *) => *)
  (defstub dz (* * *) => *)
  (defarbrec f
    (x y z)
    (if (a x y z)
      (b x y z)
      (f (dx x y z) (dy x y z) (dz x y z)))))
other
(must-succeed* (defstub a (*) => *)
  (defstub b (*) => *)
  (defstub d (*) => *)
  (defarbrec f
    (x)
    (if (a x)
      (f (d x))
      (b x))))
other
(must-succeed* (defstub a (* *) => *)
  (defstub b (* *) => *)
  (defstub dx (* *) => *)
  (defstub dy (* *) => *)
  (defarbrec f
    (x y)
    (if (a x y)
      (f (dx x y) (dy x y))
      (b x y))))
other
(must-succeed* (defstub a (* * *) => *)
  (defstub b (* * *) => *)
  (defstub dx (* * *) => *)
  (defstub dy (* * *) => *)
  (defstub dz (* * *) => *)
  (defarbrec f
    (x y z)
    (if (a x y z)
      (f (dx x y z) (dy x y z) (dz x y z))
      (b x y z))))
other
(must-succeed* (defstub a1 (*) => *)
  (defstub a2 (*) => *)
  (defstub b1 (*) => *)
  (defstub b2 (*) => *)
  (defstub c (* *) => *)
  (defstub d (*) => *)
  (defarbrec f
    (x)
    (cond ((a1 x) (b1 x)) ((a2 x) (b2 x)) (t (c x (f (d x)))))))
other
(must-succeed* (defstub a1 (* *) => *)
  (defstub a2 (* *) => *)
  (defstub b1 (* *) => *)
  (defstub b2 (* *) => *)
  (defstub c (* * *) => *)
  (defstub dx (* *) => *)
  (defstub dy (* *) => *)
  (defarbrec f
    (x y)
    (cond ((a1 x y) (b1 x y))
      ((a2 x y) (b2 x y))
      (t (c x y (f (dx x y) (dy x y)))))))
other
(must-succeed* (defstub a1 (* * *) => *)
  (defstub a2 (* * *) => *)
  (defstub b1 (* * *) => *)
  (defstub b2 (* * *) => *)
  (defstub c (* * * *) => *)
  (defstub dx (* * *) => *)
  (defstub dy (* * *) => *)
  (defstub dz (* * *) => *)
  (defarbrec f
    (x y z)
    (cond ((a1 x y z) (b1 x y z))
      ((a2 x y z) (b2 x y z))
      (t (c x y z (f (dx x y z) (dy x y z) (dz x y z)))))))
other
(must-succeed* (defstub a1 (*) => *)
  (defstub a2 (*) => *)
  (defstub b1 (*) => *)
  (defstub b2 (*) => *)
  (defstub c (* *) => *)
  (defstub d (*) => *)
  (defarbrec f
    (x)
    (cond ((a1 x) (b1 x)) ((a2 x) (c x (f (d x)))) (t (b2 x)))))
other
(must-succeed* (defstub a1 (* *) => *)
  (defstub a2 (* *) => *)
  (defstub b1 (* *) => *)
  (defstub b2 (* *) => *)
  (defstub c (* * *) => *)
  (defstub dx (* *) => *)
  (defstub dy (* *) => *)
  (defarbrec f
    (x y)
    (cond ((a1 x y) (b1 x y))
      ((a2 x y) (c x y (f (dx x y) (dy x y))))
      (t (b2 x y)))))
other
(must-succeed* (defstub a1 (* * *) => *)
  (defstub a2 (* * *) => *)
  (defstub b1 (* * *) => *)
  (defstub b2 (* * *) => *)
  (defstub c (* * * *) => *)
  (defstub dx (* * *) => *)
  (defstub dy (* * *) => *)
  (defstub dz (* * *) => *)
  (defarbrec f
    (x y z)
    (cond ((a1 x y z) (b1 x y z))
      ((a2 x y z) (c x y z (f (dx x y z) (dy x y z) (dz x y z))))
      (t (b2 x y z)))))
other
(must-succeed* (defstub a1 (*) => *)
  (defstub a2 (*) => *)
  (defstub b1 (*) => *)
  (defstub b2 (*) => *)
  (defstub c (* *) => *)
  (defstub d (*) => *)
  (defarbrec f
    (x)
    (cond ((a1 x) (c x (f (d x)))) ((a2 x) (b1 x)) (t (b2 x)))))
other
(must-succeed* (defstub a1 (* *) => *)
  (defstub a2 (* *) => *)
  (defstub b1 (* *) => *)
  (defstub b2 (* *) => *)
  (defstub c (* * *) => *)
  (defstub dx (* *) => *)
  (defstub dy (* *) => *)
  (defarbrec f
    (x y)
    (cond ((a1 x y) (c x y (f (dx x y) (dy x y))))
      ((a2 x y) (b1 x y))
      (t (b2 x y)))))
other
(must-succeed* (defstub a1 (* * *) => *)
  (defstub a2 (* * *) => *)
  (defstub b1 (* * *) => *)
  (defstub b2 (* * *) => *)
  (defstub c (* * * *) => *)
  (defstub dx (* * *) => *)
  (defstub dy (* * *) => *)
  (defstub dz (* * *) => *)
  (defarbrec f
    (x y z)
    (cond ((a1 x y z) (c x y z (f (dx x y z) (dy x y z) (dz x y z))))
      ((a2 x y z) (b1 x y z))
      (t (b2 x y z)))))
other
(must-fail (defarbrec 3 (x) x) :with-output-off nil)
other
(must-fail (defarbrec "f" (x) x) :with-output-off nil)
other
(must-fail (defarbrec cons (x) x) :with-output-off nil)
other
(must-fail (defarbrec :g (x) x) :with-output-off nil)
other
(must-fail (defarbrec len (x) x) :with-output-off nil)
other
(must-succeed* (defun g (x) x)
  (must-fail (defarbrec g (x) x) :with-output-off nil)
  :with-output-off nil)
other
(must-succeed* (defstub a (*) => *)
  (defstub b (*) => *)
  (defstub c (* *) => *)
  (defstub d (*) => *)
  (assert! (not (function-namep 'f (w state))))
  (defarbrec f
    (x)
    (if (a x)
      (b x)
      (c x (f (d x)))))
  (assert! (logic-function-namep 'f (w state)))
  :with-output-off nil)
other
(must-fail (defarbrec f (x y) (mv x y))
  :with-output-off nil)
other
(must-fail (defarbrec f (state) state) :with-output-off nil)
other
(must-fail (defarbrec f (x) x) :with-output-off nil)
other
(must-fail (defarbrec f
    (x)
    (if (atom x)
      x
      (cons (f (car x)) (f (cdr x)))))
  :with-output-off nil)
other
(must-fail (defarbrec g (x) (list x (g (car x)) (g (cdr x))))
  :with-output-off nil)
other
(must-succeed* (defun h (x) (declare (xargs :mode :program)) x)
  (must-fail (defarbrec f
      (x)
      (if (h x)
        (f (car x))
        x))
    :with-output-off nil)
  :with-output-off nil)
other
(must-succeed* (defstub a (*) => *)
  (defstub b (*) => *)
  (defstub c (* *) => *)
  (defstub d (*) => *)
  (defarbrec f
    (x)
    (if (a x)
      (b x)
      (c x (f (d x)))))
  (assert-equal (ubody 'f (w state))
    '(if (f-terminates x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      ':nonterminating))
  :with-output-off nil)
other
(must-succeed* (defstub a (*) => *)
  (defstub b (*) => *)
  (defstub c (* *) => *)
  (defstub d (*) => *)
  (must-fail (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :update-names 4/5)
    :with-output-off nil)
  (must-fail (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :update-names (1 2 3))
    :with-output-off nil)
  (must-fail (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :update-names upd)
    :with-output-off nil)
  (must-fail (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :update-names (upd 3))
    :with-output-off nil)
  (must-fail (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :update-names (upd upd))
    :with-output-off nil)
  (must-fail (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :update-names (upd upd2))
    :with-output-off nil)
  (must-fail (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :update-names (cons))
    :with-output-off nil)
  (must-fail (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :update-names (:upd))
    :with-output-off nil)
  (must-fail (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :update-names (len))
    :with-output-off nil)
  (must-succeed* (defun g (x) x)
    (must-fail (defarbrec f
        (x)
        (if (a x)
          (b x)
          (c x (f (d x))))
        :update-names (g))
      :with-output-off nil)
    :with-output-off nil)
  (must-fail (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :update-names (f))
    :with-output-off nil)
  (must-succeed* (assert! (not (function-namep 'upd (w state))))
    (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :update-names (upd))
    (assert! (function-namep 'upd (w state)))
    :with-output-off nil)
  (must-succeed* (assert! (not (function-namep 'f-x* (w state))))
    (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x)))))
    (assert! (function-namep 'f-x* (w state)))
    :with-output-off nil)
  (must-succeed* (assert! (not (function-namep 'f-x* (w state))))
    (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :update-names nil)
    (assert! (function-namep 'f-x* (w state)))
    :with-output-off nil)
  :with-output-off nil)
other
(must-succeed* (defstub a (* *) => *)
  (defstub b (* *) => *)
  (defstub c (* * *) => *)
  (defstub dx (* *) => *)
  (defstub dy (* *) => *)
  (must-fail (defarbrec f
      (x y)
      (if (a x y)
        (b x y)
        (c x y (f (dx x y) (dy x y))))
      :update-names 4/5)
    :with-output-off nil)
  (must-fail (defarbrec f
      (x y)
      (if (a x y)
        (b x y)
        (c x y (f (dx x y) (dy x y))))
      :update-names (1 2 3))
    :with-output-off nil)
  (must-fail (defarbrec f
      (x y)
      (if (a x y)
        (b x y)
        (c x y (f (dx x y) (dy x y))))
      :update-names upd)
    :with-output-off nil)
  (must-fail (defarbrec f
      (x y)
      (if (a x y)
        (b x y)
        (c x y (f (dx x y) (dy x y))))
      :update-names (upd 3))
    :with-output-off nil)
  (must-fail (defarbrec f
      (x y)
      (if (a x y)
        (b x y)
        (c x y (f (dx x y) (dy x y))))
      :update-names (upd upd upd2))
    :with-output-off nil)
  (must-fail (defarbrec f
      (x y)
      (if (a x y)
        (b x y)
        (c x y (f (dx x y) (dy x y))))
      :update-names (upd))
    :with-output-off nil)
  (must-fail (defarbrec f
      (x y)
      (if (a x y)
        (b x y)
        (c x y (f (dx x y) (dy x y))))
      :update-names (upd upd2 upd3))
    :with-output-off nil)
  (must-fail (defarbrec f
      (x y)
      (if (a x y)
        (b x y)
        (c x y (f (dx x y) (dy x y))))
      :update-names (upd cons))
    :with-output-off nil)
  (must-fail (defarbrec f
      (x y)
      (if (a x y)
        (b x y)
        (c x y (f (dx x y) (dy x y))))
      :update-names (cons upd))
    :with-output-off nil)
  (must-fail (defarbrec f
      (x y)
      (if (a x y)
        (b x y)
        (c x y (f (dx x y) (dy x y))))
      :update-names (:upd upd))
    :with-output-off nil)
  (must-fail (defarbrec f
      (x y)
      (if (a x y)
        (b x y)
        (c x y (f (dx x y) (dy x y))))
      :update-names (upd :upd))
    :with-output-off nil)
  (must-fail (defarbrec f
      (x y)
      (if (a x y)
        (b x y)
        (c x y (f (dx x y) (dy x y))))
      :update-names (len upd))
    :with-output-off nil)
  (must-fail (defarbrec f
      (x y)
      (if (a x y)
        (b x y)
        (c x y (f (dx x y) (dy x y))))
      :update-names (upd len))
    :with-output-off nil)
  (must-succeed* (defun g (x) x)
    (must-fail (defarbrec f
        (x y)
        (if (a x y)
          (b x y)
          (c x y (f (dx x y) (dy x y))))
        :update-names (g upd))
      :with-output-off nil)
    (must-fail (defarbrec f
        (x y)
        (if (a x y)
          (b x y)
          (c x y (f (dx x y) (dy x y))))
        :update-names (upd g))
      :with-output-off nil)
    :with-output-off nil)
  (must-fail (defarbrec f
      (x y)
      (if (a x y)
        (b x y)
        (c x y (f (dx x y) (dy x y))))
      :update-names (f upd))
    :with-output-off nil)
  (must-fail (defarbrec f
      (x y)
      (if (a x y)
        (b x y)
        (c x y (f (dx x y) (dy x y))))
      :update-names (upd f))
    :with-output-off nil)
  (must-succeed* (assert! (not (function-namep 'updx (w state))))
    (assert! (not (function-namep 'updy (w state))))
    (defarbrec f
      (x y)
      (if (a x y)
        (b x y)
        (c x y (f (dx x y) (dy x y))))
      :update-names (updx updy))
    (assert! (function-namep 'updx (w state)))
    (assert! (function-namep 'updy (w state)))
    :with-output-off nil)
  (must-succeed* (assert! (not (function-namep 'f-x* (w state))))
    (assert! (not (function-namep 'f-y* (w state))))
    (defarbrec f
      (x y)
      (if (a x y)
        (b x y)
        (c x y (f (dx x y) (dy x y)))))
    (assert! (function-namep 'f-x* (w state)))
    (assert! (function-namep 'f-y* (w state)))
    :with-output-off nil)
  (must-succeed* (assert! (not (function-namep 'f-x* (w state))))
    (assert! (not (function-namep 'f-y* (w state))))
    (defarbrec f
      (x y)
      (if (a x y)
        (b x y)
        (c x y (f (dx x y) (dy x y))))
      :update-names nil)
    (assert! (function-namep 'f-x* (w state)))
    (assert! (function-namep 'f-y* (w state)))
    :with-output-off nil)
  :with-output-off nil)
other
(must-succeed* (defstub a (*) => *)
  (defstub b (*) => *)
  (defstub c (* *) => *)
  (defstub d (*) => *)
  (must-fail (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :terminates-name #\u)
    :with-output-off nil)
  (must-fail (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :terminates-name (term))
    :with-output-off nil)
  (must-fail (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :terminates-name cons)
    :with-output-off nil)
  (must-fail (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :terminates-name :term)
    :with-output-off nil)
  (must-fail (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :terminates-name len)
    :with-output-off nil)
  (must-succeed* (defun g (x) x)
    (must-fail (defarbrec f
        (x)
        (if (a x)
          (b x)
          (c x (f (d x))))
        :terminates-name g)
      :with-output-off nil)
    :with-output-off nil)
  (must-succeed* (defun g-witness (x) x)
    (must-fail (defarbrec f
        (x)
        (if (a x)
          (b x)
          (c x (f (d x))))
        :terminates-name g)
      :with-output-off nil)
    :with-output-off nil)
  (must-succeed* (defun g-suff (x) x)
    (must-fail (defarbrec f
        (x)
        (if (a x)
          (b x)
          (c x (f (d x))))
        :terminates-name g)
      :with-output-off nil)
    :with-output-off nil)
  (must-fail (defarbrec term
      (x)
      (if (a x)
        (b x)
        (c x (term (d x))))
      :terminates-name term)
    :with-output-off nil)
  (must-fail (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :terminates-name f-x*)
    :with-output-off nil)
  (must-fail (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :update-names (term)
      :terminates-name term)
    :with-output-off nil)
  (must-fail (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :update-names (term-witness)
      :terminates-name term)
    :with-output-off nil)
  (must-fail (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :update-names (term-suff)
      :terminates-name term)
    :with-output-off nil)
  (must-succeed* (assert! (not (function-namep 'term (w state))))
    (assert! (not (function-namep 'term-witness (w state))))
    (assert! (not (theorem-namep 'term-suff (w state))))
    (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :terminates-name term)
    (assert! (function-namep 'term (w state)))
    (assert! (function-namep 'term-witness (w state)))
    (assert! (theorem-namep 'term-suff (w state)))
    :with-output-off nil)
  (must-succeed* (assert! (not (function-namep 'f-terminates (w state))))
    (assert! (not (function-namep 'f-terminates-witness (w state))))
    (assert! (not (theorem-namep 'f-terminates-suff (w state))))
    (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x)))))
    (assert! (function-namep 'f-terminates (w state)))
    (assert! (function-namep 'f-terminates-witness (w state)))
    (assert! (theorem-namep 'f-terminates-suff (w state)))
    :with-output-off nil)
  (must-succeed* (assert! (not (function-namep 'f-terminates (w state))))
    (assert! (not (function-namep 'f-terminates-witness (w state))))
    (assert! (not (theorem-namep 'f-terminates-suff (w state))))
    (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :terminates-name nil)
    (assert! (function-namep 'f-terminates (w state)))
    (assert! (function-namep 'f-terminates-witness (w state)))
    (assert! (theorem-namep 'f-terminates-suff (w state)))
    :with-output-off nil)
  :with-output-off nil)
other
(must-succeed* (defstub a (*) => *)
  (defstub b (*) => *)
  (defstub c (* *) => *)
  (defstub d (*) => *)
  (must-fail (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :measure-name "meas")
    :with-output-off nil)
  (must-fail (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :measure-name (meas))
    :with-output-off nil)
  (must-fail (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :measure-name cons)
    :with-output-off nil)
  (must-fail (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :measure-name :meas)
    :with-output-off nil)
  (must-fail (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :measure-name len)
    :with-output-off nil)
  (must-succeed* (defun g (x) x)
    (must-fail (defarbrec f
        (x)
        (if (a x)
          (b x)
          (c x (f (d x))))
        :measure-name g)
      :with-output-off nil)
    :with-output-off nil)
  (must-fail (defarbrec meas
      (x)
      (if (a x)
        (b x)
        (c x (meas (d x))))
      :measure-name meas)
    :with-output-off nil)
  (must-fail (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :measure-name f-x*)
    :with-output-off nil)
  (must-fail (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :update-names (meas)
      :measure-name meas)
    :with-output-off nil)
  (must-fail (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :measure-name f-terminates)
    :with-output-off nil)
  (must-fail (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :terminates-name meas
      :measure-name meas)
    :with-output-off nil)
  (must-fail (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :terminates-name meas
      :measure-name meas-witness)
    :with-output-off nil)
  (must-fail (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :terminates-name meas
      :measure-name meas-suff)
    :with-output-off nil)
  (must-succeed* (assert! (not (function-namep 'meas (w state))))
    (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :measure-name meas)
    (assert! (function-namep 'meas (w state)))
    :with-output-off nil)
  (must-succeed* (assert! (not (function-namep 'f-measure (w state))))
    (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x)))))
    (assert! (function-namep 'f-measure (w state)))
    :with-output-off nil)
  (must-succeed* (assert! (not (function-namep 'f-measure (w state))))
    (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :measure-name nil)
    (assert! (function-namep 'f-measure (w state)))
    :with-output-off nil)
  :with-output-off nil)
other
(must-succeed* (defstub a (*) => *)
  (defstub b (*) => *)
  (defstub c (* *) => *)
  (defstub d (*) => *)
  (must-fail (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :nonterminating (len x x))
    :with-output-off nil)
  (must-fail (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :nonterminating (ggggg x))
    :with-output-off nil)
  (must-fail (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :nonterminating (cons x y))
    :with-output-off nil)
  (must-fail (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :nonterminating (f 0))
    :with-output-off nil)
  (must-succeed* (defun g (x) (declare (xargs :mode :program)) x)
    (must-fail (defarbrec f
        (x)
        (if (a x)
          (b x)
          (c x (f (d x))))
        :nonterminating (g x))
      :with-output-off nil)
    :with-output-off nil)
  (must-fail (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :nonterminating (mv 1 2))
    :with-output-off nil)
  (must-succeed* (defstobj s)
    (set-irrelevant-formals-ok t)
    (must-fail (defarbrec g
        (x s)
        (if (a x)
          (b x)
          (c x (g (d x) s)))
        :nonterminating s)
      :with-output-off nil)
    :with-output-off nil)
  (must-succeed* (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :nonterminating (cons x x))
    (defthm check-nonterminating
      (implies (not (f-terminates x)) (equal (f x) (cons x x))))
    :with-output-off nil)
  (must-succeed* (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x)))))
    (defthm check-nonterminating
      (implies (not (f-terminates x))
        (equal (f x) :nonterminating)))
    :with-output-off nil)
  (must-succeed* (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :nonterminating :nonterminating)
    (defthm check-nonterminating
      (implies (not (f-terminates x))
        (equal (f x) :nonterminating)))
    :with-output-off nil)
  :with-output-off nil)
other
(must-succeed* (defstub a (*) => *)
  (defstub b (*) => *)
  (defstub c (* *) => *)
  (defstub d (*) => *)
  (must-fail (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :print 44)
    :with-output-off nil)
  (must-fail (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :print :nil)
    :with-output-off nil)
  (must-fail (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :print "ALL")
    :with-output-off nil)
  (must-fail (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :print (:result :submit))
    :with-output-off nil)
  (must-succeed (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x)))))
    :with-output-off nil)
  (must-succeed (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :print nil)
    :with-output-off nil)
  (must-succeed (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :print :error)
    :with-output-off nil)
  (must-succeed (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :print :result)
    :with-output-off nil)
  (must-succeed (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :print :all)
    :with-output-off nil)
  :with-output-off nil)
other
(must-succeed* (defstub a (*) => *)
  (defstub b (*) => *)
  (defstub c (* *) => *)
  (defstub d (*) => *)
  (must-fail (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :show-only 't)
    :with-output-off nil)
  (must-fail (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :show-only :nil)
    :with-output-off nil)
  (must-succeed (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))))
  (must-succeed (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :show-only t))
  (must-succeed (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :print nil
      :show-only t))
  (must-succeed (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :print :error :show-only t))
  (must-succeed (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :print :result :show-only t))
  (must-succeed (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :print :all :show-only t))
  (must-succeed (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :show-only nil))
  :with-output-off nil)
other
(must-succeed* (defstub a (*) => *)
  (defstub b (*) => *)
  (defstub c (* *) => *)
  (defstub d (*) => *)
  (must-succeed* (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :show-only t)
    (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x)))))
    :with-output-off nil)
  (must-succeed* (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x)))))
    (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x)))))
    (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :print :all)
    (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :show-only t)
    (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :show-only nil)
    :with-output-off nil)
  (must-succeed* (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :print :error)
    (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x)))))
    (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :print :all)
    (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :show-only t)
    (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :show-only nil)
    :with-output-off nil)
  (must-succeed* (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :show-only nil)
    (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x)))))
    (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :print :all)
    (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :show-only t)
    (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :show-only nil)
    :with-output-off nil)
  (must-succeed* (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :print nil
      :show-only nil)
    (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x)))))
    (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :print :all)
    (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :show-only t)
    (defarbrec f
      (x)
      (if (a x)
        (b x)
        (c x (f (d x))))
      :show-only nil)
    :with-output-off nil)
  :with-output-off nil)
other
(must-succeed* (defarbrec fact
    (n)
    (if (equal n 0)
      1
      (* n (fact (1- n))))))
other
(must-succeed* (set-irrelevant-formals-ok t)
  (defarbrec paradox (x) (1+ (paradox x))))
other
(must-succeed* (set-irrelevant-formals-ok t)
  (defarbrec indet (x) (car (list (indet x)))))