		Search-engine friendly clone of the ACL2 documentation.

Ubyte8-ihs-theorems

Theorems about ubyte8 and IHS functions.

Theorem: ubyte8p-of-loghead-of-8

(defthm ubyte8p-of-loghead-of-8
  (ubyte8p (loghead 8 x)))

Theorem: loghead-of-8-when-ubyte8p

(defthm loghead-of-8-when-ubyte8p
  (implies (ubyte8p x)
           (equal (loghead 8 x) x)))

Theorem: logtail-of-8-when-ubyte8p

(defthm logtail-of-8-when-ubyte8p
  (implies (ubyte8p x)
           (equal (logtail 8 x) 0)))