		Search-engine friendly clone of the ACL2 documentation.

Ubyte5-ihs-theorems

Theorems about ubyte5 and IHS functions.

Theorem: ubyte5p-of-loghead-of-5

(defthm ubyte5p-of-loghead-of-5
  (ubyte5p (loghead 5 x)))

Theorem: loghead-of-5-when-ubyte5p

(defthm loghead-of-5-when-ubyte5p
  (implies (ubyte5p x)
           (equal (loghead 5 x) x)))

Theorem: logtail-of-5-when-ubyte5p

(defthm logtail-of-5-when-ubyte5p
  (implies (ubyte5p x)
           (equal (logtail 5 x) 0)))