		Search-engine friendly clone of the ACL2 documentation.

Ubyte32-ihs-theorems

Theorems about ubyte32 and IHS functions.

Theorem: ubyte32p-of-loghead-of-32

(defthm ubyte32p-of-loghead-of-32
  (ubyte32p (loghead 32 x)))

Theorem: loghead-of-32-when-ubyte32p

(defthm loghead-of-32-when-ubyte32p
  (implies (ubyte32p x)
           (equal (loghead 32 x) x)))

Theorem: logtail-of-32-when-ubyte32p

(defthm logtail-of-32-when-ubyte32p
  (implies (ubyte32p x)
           (equal (logtail 32 x) 0)))