Recognizer for sbyte1.
(sbyte1p x) → yes/no
Function:
(defun sbyte1p (x) (declare (xargs :guard t)) (mbe :logic (signed-byte-p 1 x) :exec (and (integerp x) (<= -1 x) (< x 1))))
Theorem:
(defthm booleanp-of-sbyte1p (b* ((yes/no (sbyte1p x))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm sbyte1p-forward-signed-byte-p (implies (sbyte1p x) (signed-byte-p 1 x)) :rule-classes :forward-chaining)
Theorem:
(defthm signed-byte-p-rewrite-sbyte1p (equal (signed-byte-p 1 x) (sbyte1p x)))
Theorem:
(defthm integerp-when-sbyte1p (implies (sbyte1p x) (integerp x)) :rule-classes :compound-recognizer)