		Search-engine friendly clone of the ACL2 documentation.

Ubyte12-ihs-theorems

Theorems about ubyte12 and IHS functions.

Theorem: ubyte12p-of-loghead-of-12

(defthm ubyte12p-of-loghead-of-12
  (ubyte12p (loghead 12 x)))

Theorem: loghead-of-12-when-ubyte12p

(defthm loghead-of-12-when-ubyte12p
  (implies (ubyte12p x)
           (equal (loghead 12 x) x)))

Theorem: logtail-of-12-when-ubyte12p

(defthm logtail-of-12-when-ubyte12p
  (implies (ubyte12p x)
           (equal (logtail 12 x) 0)))