Theorem:
(defthm unsigned-byte-p-forward (implies (unsigned-byte-p bits i) (and (integerp i) (>= i 0) (< i (expt 2 bits)))) :rule-classes :forward-chaining)
Theorem:
(defthm unsigned-byte-p-unsigned-byte-p (implies (and (unsigned-byte-p size i) (integerp size1) (>= size1 size)) (unsigned-byte-p size1 i)))