		Search-engine friendly clone of the ACL2 documentation.

Sbyte8-ihs-theorems

Theorems about sbyte8 and IHS functions.

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

Theorem: logtail-of-8-when-sbyte8p

(defthm logtail-of-8-when-sbyte8p
  (implies (sbyte8p x)
           (equal (logtail 8 x)
                  (if (< x 0) -1 0))))