		Search-engine friendly clone of the ACL2 documentation.

Sbyte64-ihs-theorems

Theorems about sbyte64 and IHS functions.

Theorem: sbyte64p-of-logext-of-64

(defthm sbyte64p-of-logext-of-64
  (sbyte64p (logext 64 x)))

Theorem: logext-of-64-when-sbyte64p

(defthm logext-of-64-when-sbyte64p
  (implies (sbyte64p x)
           (equal (logext 64 x) x)))

Theorem: logtail-of-64-when-sbyte64p

(defthm logtail-of-64-when-sbyte64p
  (implies (sbyte64p x)
           (equal (logtail 64 x)
                  (if (< x 0) -1 0))))