Theorem: unsigned-byte-p-wrb
(defthm unsigned-byte-p-wrb (implies (and (unsigned-byte-p n j) (<= (+ (bsp-size bsp) (bsp-position bsp)) n) (integerp i) (integerp n) (bspp bsp)) (unsigned-byte-p n (wrb i bsp j))))
