Recognizer for cutscore bit structures.
(cutscore-p x) → *
Function:
(defun cutscore-p (x) (declare (xargs :guard t)) (let ((__function__ 'cutscore-p)) (declare (ignorable __function__)) (mbe :logic (unsigned-byte-p 12 x) :exec (and (natp x) (< x 4096)))))
Theorem:
(defthm cutscore-p-when-unsigned-byte-p (implies (unsigned-byte-p 12 x) (cutscore-p x)))
Theorem:
(defthm unsigned-byte-p-when-cutscore-p (implies (cutscore-p x) (unsigned-byte-p 12 x)))
Theorem:
(defthm cutscore-p-compound-recognizer (implies (cutscore-p x) (natp x)) :rule-classes :compound-recognizer)