|
|
|---|
|
|
|
|---|
Theorems about sbyte128 and IHS functions.
Theorem:
(defthm sbyte128p-of-logext-of-128 (sbyte128p (logext 128 x)))
Theorem:
(defthm logext-of-128-when-sbyte128p (implies (sbyte128p x) (equal (logext 128 x) x)))
Theorem:
(defthm logtail-of-128-when-sbyte128p (implies (sbyte128p x) (equal (logtail 128 x) (if (< x 0) -1 0))))