|
|
|---|
|
|
|
|---|
Theorems about ubyte16 and IHS functions.
Theorem:
(defthm ubyte16p-of-loghead-of-16 (ubyte16p (loghead 16 x)))
Theorem:
(defthm loghead-of-16-when-ubyte16p (implies (ubyte16p x) (equal (loghead 16 x) x)))
Theorem:
(defthm logtail-of-16-when-ubyte16p (implies (ubyte16p x) (equal (logtail 16 x) 0)))