Lemmas showing the basic preservation of signed-byte-p by operations like logand, logior, etc.
Theorem:
(defthm signed-byte-p-logops (and (implies (signed-byte-p size i) (signed-byte-p size (lognot i))) (implies (and (signed-byte-p size i) (signed-byte-p size j)) (and (signed-byte-p size (logior i j)) (signed-byte-p size (logxor i j)) (signed-byte-p size (logand i j)) (signed-byte-p size (logeqv i j)) (signed-byte-p size (lognand i j)) (signed-byte-p size (lognor i j)) (signed-byte-p size (logandc1 i j)) (signed-byte-p size (logandc2 i j)) (signed-byte-p size (logorc1 i j)) (signed-byte-p size (logorc2 i j))))))