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

Use the macro `(expt 2 bound)`.

Usage:

(defthm-unsigned-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 following form
(if both

(defthm <theorem-name> (implies <hypotheses> (unsigned-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> (natp <conclusion>)) :hints <usual ACL2 hints for the :type-prescription corollary>) (:linear :corollary (implies <hypotheses for the :linear corollary> (and (<= 0 <conclusion>) (< <conclusion> (expt 2 <n>)))) :hints <usual ACL2 hints for the :linear corollary>)))

If `force`.
Analogous remarks apply to

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