		Search-engine friendly clone of the ACL2 documentation.

Sbyte16-ihs-theorems

Theorems about sbyte16 and IHS functions.

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

Theorem: logtail-of-16-when-sbyte16p

(defthm logtail-of-16-when-sbyte16p
  (implies (sbyte16p x)
           (equal (logtail 16 x)
                  (if (< x 0) -1 0))))