		Search-engine friendly clone of the ACL2 documentation.

Base58

Base58-val=>char

Turn a Base58 value into the corresponding character.

Signature
(base58-val=>char val) → char
Arguments: val — Guard (base58-valuep val).
Returns: char — Type (base58-characterp char).

The correspondence is given in the table in Section `Base58 symbol chart' of Page `Base58Check encoding' of [Wiki]. Since the list *base58-characters* is ordered according to increasing values, this function is essentially nth.

Definitions and Theorems

Function: base58-val=>char

(defun base58-val=>char (val)
  (declare (xargs :guard (base58-valuep val)))
  (let ((__function__ 'base58-val=>char))
    (declare (ignorable __function__))
    (nth (base58-value-fix val)
         *base58-characters*)))

Theorem: base58-characterp-of-base58-val=>char

(defthm base58-characterp-of-base58-val=>char
  (b* ((char (base58-val=>char val)))
    (base58-characterp char))
  :rule-classes :rewrite)

Theorem: base58-val=>char-of-base58-value-fix-val

(defthm base58-val=>char-of-base58-value-fix-val
  (equal (base58-val=>char (base58-value-fix val))
         (base58-val=>char val)))

Theorem: base58-val=>char-base58-value-equiv-congruence-on-val

(defthm base58-val=>char-base58-value-equiv-congruence-on-val
  (implies (base58-value-equiv val val-equiv)
           (equal (base58-val=>char val)
                  (base58-val=>char val-equiv)))
  :rule-classes :congruence)

Subtopics

Base58-val<=>char-inverses-theorems: base58-val=>char and base58-char=>val are mutual inverses.