Theorems about sbyte64 and IHS functions.
Theorem: sbyte64p-of-logext-of-64
(defthm sbyte64p-of-logext-of-64 (sbyte64p (logext 64 x)))
