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