		Search-engine friendly clone of the ACL2 documentation.

Ubyte8s<=>hexchars-inverses-theorems

ubyte8s=>hexchars and hexchars=>ubyte8s are mutual inverses.

Definitions and Theorems

Theorem: hexchars=>ubyte8s-of-ubyte8s=>hexchars

(defthm hexchars=>ubyte8s-of-ubyte8s=>hexchars
  (equal (hexchars=>ubyte8s (ubyte8s=>hexchars bytes))
         (unsigned-byte-list-fix 8 bytes)))

Theorem: ubyte8s=>hexchars-of-hexchars=>ubyte8s

(defthm ubyte8s=>hexchars-of-hexchars=>ubyte8s
  (implies (and (str::hex-digit-char-list*p chars)
                (true-listp chars)
                (evenp (len chars)))
           (equal (ubyte8s=>hexchars (hexchars=>ubyte8s chars))
                  (str::upcase-charlist chars))))