		Search-engine friendly clone of the ACL2 documentation.

Base58

Base58-vals=>chars

Lift base58-val=>char to lists.

Signature
(base58-vals=>chars vals) → chars
Arguments: vals — Guard (base58-value-listp vals).
Returns: chars — Type (base58-character-listp chars).

Definitions and Theorems

Function: base58-vals=>chars

(defun base58-vals=>chars (vals)
  (declare (xargs :guard (base58-value-listp vals)))
  (let ((__function__ 'base58-vals=>chars))
    (declare (ignorable __function__))
    (cond ((endp vals) nil)
          (t (cons (base58-val=>char (car vals))
                   (base58-vals=>chars (cdr vals)))))))

Theorem: base58-character-listp-of-base58-vals=>chars

(defthm base58-character-listp-of-base58-vals=>chars
  (b* ((chars (base58-vals=>chars vals)))
    (base58-character-listp chars))
  :rule-classes :rewrite)

Theorem: len-of-base58-vals=>chars

(defthm len-of-base58-vals=>chars
  (equal (len (base58-vals=>chars vals))
         (len vals)))

Theorem: base58-vals=>chars-of-append

(defthm base58-vals=>chars-of-append
  (equal (base58-vals=>chars (append vals1 vals2))
         (append (base58-vals=>chars vals1)
                 (base58-vals=>chars vals2))))

Theorem: base58-vals=>chars-of-repeat

(defthm base58-vals=>chars-of-repeat
  (equal (base58-vals=>chars (repeat n val))
         (repeat n (base58-val=>char val))))

Theorem: base58-vals=>chars-of-base58-value-list-fix-vals

(defthm base58-vals=>chars-of-base58-value-list-fix-vals
  (equal (base58-vals=>chars (base58-value-list-fix vals))
         (base58-vals=>chars vals)))

Theorem: base58-vals=>chars-base58-value-list-equiv-congruence-on-vals

(defthm
      base58-vals=>chars-base58-value-list-equiv-congruence-on-vals
  (implies (base58-value-list-equiv vals vals-equiv)
           (equal (base58-vals=>chars vals)
                  (base58-vals=>chars vals-equiv)))
  :rule-classes :congruence)

Subtopics

Base58-vals<=>chars-inverses-theorems: base58-vals=>chars and base58-chars=>vals are mutual inverses.