Recognize non-limit errors.
(reserr-nonlimitp x) → yes/no
This recognizes all the errors that are not recognized by reserr-limitp. See that recognizer's documentation.
Function:
(defun reserr-nonlimitp (x) (declare (xargs :guard t)) (let ((__function__ 'reserr-nonlimitp)) (declare (ignorable __function__)) (and (reserrp x) (not (reserr-limitp x)))))
Theorem:
(defthm booleanp-of-reserr-nonlimitp (b* ((yes/no (reserr-nonlimitp x))) (booleanp yes/no)) :rule-classes :rewrite)