Sbyte8-ihs-theorems
Theorems about sbyte8 and IHS functions.
Definitions and Theorems
Theorem: sbyte8p-of-logext-of-8
(defthm sbyte8p-of-logext-of-8
(sbyte8p (logext 8 x)))
Theorem: logext-of-8-when-sbyte8p
(defthm logext-of-8-when-sbyte8p
(implies (sbyte8p x)
(equal (logext 8 x) x)))
