		Search-engine friendly clone of the ACL2 documentation.

Base58-encode/decode-inverses-theorems

base58-encode and base58-decode are mutual inverses.

Theorem: base58-decode-of-base58-encode

(defthm base58-decode-of-base58-encode
  (equal (base58-decode (base58-encode bytes))
         (byte-list-fix bytes)))

Theorem: base58-encode-of-base58-decode

(defthm base58-encode-of-base58-decode
  (equal (base58-encode (base58-decode chars))
         (base58-character-list-fix chars)))