base58-vals=>chars and base58-chars=>vals are mutual inverses.
Theorem:
(defthm base58-chars=>vals=>chars (equal (base58-vals=>chars (base58-chars=>vals chars)) (base58-character-list-fix chars)))
Theorem:
(defthm base58-vals=>chars=>vals (equal (base58-chars=>vals (base58-vals=>chars vals)) (base58-value-list-fix vals)))