		Search-engine friendly clone of the ACL2 documentation.

Ubyte7-ihs-theorems

Theorems about ubyte7 and IHS functions.

Theorem: ubyte7p-of-loghead-of-7

(defthm ubyte7p-of-loghead-of-7
  (ubyte7p (loghead 7 x)))

Theorem: loghead-of-7-when-ubyte7p

(defthm loghead-of-7-when-ubyte7p
  (implies (ubyte7p x)
           (equal (loghead 7 x) x)))

Theorem: logtail-of-7-when-ubyte7p

(defthm logtail-of-7-when-ubyte7p
  (implies (ubyte7p x)
           (equal (logtail 7 x) 0)))