		Search-engine friendly clone of the ACL2 documentation.

Sbyte32-ihs-theorems

Theorems about sbyte32 and IHS functions.

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)))

Theorem: logtail-of-32-when-sbyte32p

(defthm logtail-of-32-when-sbyte32p
  (implies (sbyte32p x)
           (equal (logtail 32 x)
                  (if (< x 0) -1 0))))