Theorems about ubyte20 and IHS functions.
Theorem: ubyte20p-of-loghead-of-20
(defthm ubyte20p-of-loghead-of-20 (ubyte20p (loghead 20 x)))
Theorem: loghead-of-20-when-ubyte20p
(defthm loghead-of-20-when-ubyte20p (implies (ubyte20p x) (equal (loghead 20 x) x)))
