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