Sbyte32-ihs-theorems
Theorems about sbyte32 and IHS functions.
Definitions and Theorems
Theorem: sbyte32p-of-logext-of-32
(defthm sbyte32p-of-logext-of-32
(sbyte32p (logext 32 x)))
Theorem: logext-of-32-when-sbyte32p
(defthm logext-of-32-when-sbyte32p
(implies (sbyte32p x)
(equal (logext 32 x) x)))
