		Search-engine friendly clone of the ACL2 documentation.

Ubyte64-ihs-theorems

Theorems about ubyte64 and IHS functions.

Theorem: ubyte64p-of-loghead-of-64

(defthm ubyte64p-of-loghead-of-64
  (ubyte64p (loghead 64 x)))

Theorem: loghead-of-64-when-ubyte64p

(defthm loghead-of-64-when-ubyte64p
  (implies (ubyte64p x)
           (equal (loghead 64 x) x)))

Theorem: logtail-of-64-when-ubyte64p

(defthm logtail-of-64-when-ubyte64p
  (implies (ubyte64p x)
           (equal (logtail 64 x) 0)))