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