Prove rules about a term yielding values in `signed-byte-p`.

Use the macro `(- (expt 2 (1- bound)))` and
less than `(expt 2 (1- bound))`.

Usage:

(defthm-signed-byte-p <theorem-name> :hyp <hypotheses> :bound <n> :concl <conclusion> :hints <usual ACL2 hints for the main theorem> :gen-type <t or nil> ;; Generate :type-prescription corollary :gen-linear <t or nil> ;; Generate :linear corollary :hyp-t <hypotheses for the :type-prescription corollary> :hyp-l <hypotheses for the :linear corollary> :hints-t <usual ACL2 hints for the :type-prescription corollary> :hints-l <usual ACL2 hints for the :linear corollary> :otf-flg <t or nil>)

The above form produces a theorem of the form
(if both

(defthm <theorem-name> (implies <hypotheses> (signed-byte-p <n> <conclusion>)) :hints <usual ACL2 hints for the main theorem> :otf-flg <t or nil> :rule-classes (:rewrite (:type-prescription :corollary (implies <hypotheses for the :type-prescription corollary> (integerp <conclusion>)) :hints <usual ACL2 hints for the :type-prescription corollary>) (:linear :corollary (implies <hypotheses for the :linear corollary> (and (<= (- (expt 2 (1- <n>)) <conclusion>)) (< <conclusion> (expt 2 (1- <n>))))) :hints <usual ACL2 hints for the :linear corollary>)))

If `force`.
Analogous remarks apply to

Also see the related macros
`defthm-natp` and `defthm-unsigned-byte-p`.