		Search-engine friendly clone of the ACL2 documentation.

Ubyte3-ihs-theorems

Theorems about ubyte3 and IHS functions.

Theorem: ubyte3p-of-loghead-of-3

(defthm ubyte3p-of-loghead-of-3
  (ubyte3p (loghead 3 x)))

Theorem: loghead-of-3-when-ubyte3p

(defthm loghead-of-3-when-ubyte3p
  (implies (ubyte3p x)
           (equal (loghead 3 x) x)))

Theorem: logtail-of-3-when-ubyte3p

(defthm logtail-of-3-when-ubyte3p
  (implies (ubyte3p x)
           (equal (logtail 3 x) 0)))