Theorem: signed-byte-p-forward
(defthm signed-byte-p-forward (implies (signed-byte-p bits i) (and (integerp i) (>= i (- (expt 2 (- bits 1)))) (< i (expt 2 (- bits 1))))) :rule-classes :forward-chaining)