		Search-engine friendly clone of the ACL2 documentation.

Ubyte20-ihs-theorems

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)))

Theorem: logtail-of-20-when-ubyte20p

(defthm logtail-of-20-when-ubyte20p
  (implies (ubyte20p x)
           (equal (logtail 20 x) 0)))