Sbyte16-ihs-theorems
Theorems about sbyte16 and IHS functions.
Definitions and Theorems
Theorem: sbyte16p-of-logext-of-16
(defthm sbyte16p-of-logext-of-16
(sbyte16p (logext 16 x)))
Theorem: logext-of-16-when-sbyte16p
(defthm logext-of-16-when-sbyte16p
(implies (sbyte16p x)
(equal (logext 16 x) x)))
