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