		Search-engine friendly clone of the ACL2 documentation.

Ubyte6-ihs-theorems

Theorems about ubyte6 and IHS functions.

Theorem: ubyte6p-of-loghead-of-6

(defthm ubyte6p-of-loghead-of-6
  (ubyte6p (loghead 6 x)))

Theorem: loghead-of-6-when-ubyte6p

(defthm loghead-of-6-when-ubyte6p
  (implies (ubyte6p x)
           (equal (loghead 6 x) x)))

Theorem: logtail-of-6-when-ubyte6p

(defthm logtail-of-6-when-ubyte6p
  (implies (ubyte6p x)
           (equal (logtail 6 x) 0)))