		Search-engine friendly clone of the ACL2 documentation.

Bfrstate

Bfrstate-p

Recognizer for a bfrstate object.

Signature
(bfrstate-p x) → *

Definitions and Theorems

Function: bfrstate-p

(defun bfrstate-p (x)
  (declare (xargs :guard t))
  (let ((__function__ 'bfrstate-p))
    (declare (ignorable __function__))
    (and (natp x)
         (bfr-mode-p (logand 3 x)))))

Theorem: bfrstate-p-compound-recognizer

(defthm bfrstate-p-compound-recognizer
  (implies (bfrstate-p x) (natp x))
  :rule-classes :compound-recognizer)