Theorem: unsigned-byte-p-logrev
(defthm unsigned-byte-p-logrev (implies (and (>= size1 size) (>= size 0) (integerp size) (integerp size1)) (unsigned-byte-p size1 (logrev size i))))
