|
|
|---|
|
|
|
|---|
Theorems about ubyte128 and IHS functions.
Theorem:
(defthm ubyte128p-of-loghead-of-128 (ubyte128p (loghead 128 x)))
Theorem:
(defthm loghead-of-128-when-ubyte128p (implies (ubyte128p x) (equal (loghead 128 x) x)))
Theorem:
(defthm logtail-of-128-when-ubyte128p (implies (ubyte128p x) (equal (logtail 128 x) 0)))