		Search-engine friendly clone of the ACL2 documentation.

Digits-any-base

Lendian=>nat

Convert a little-endian list of digits to their value.

Signature
(lendian=>nat base digits) → nat
Arguments: base — Guard (dab-basep base).; digits — Guard (dab-digit-listp base digits).
Returns: nat — Type (natp nat).

Definitions and Theorems

Function: lendian=>nat

(defun lendian=>nat (base digits)
  (declare (xargs :guard (and (dab-basep base)
                              (dab-digit-listp base digits))))
  (let ((__function__ 'lendian=>nat))
    (declare (ignorable __function__))
    (mbe :exec (digits=>nat-exec base (rev digits) 0)
         :logic (cond ((atom digits) 0)
                      (t (+ (dab-digit-fix base (car digits))
                            (* (lendian=>nat base (cdr digits))
                               (dab-base-fix base))))))))

Theorem: natp-of-lendian=>nat

(defthm natp-of-lendian=>nat
  (b* ((nat (lendian=>nat base digits)))
    (natp nat))
  :rule-classes :rewrite)

Theorem: lendian=>nat-of-dab-digit-list-fix-digits

(defthm lendian=>nat-of-dab-digit-list-fix-digits
  (equal (lendian=>nat base (dab-digit-list-fix base digits))
         (lendian=>nat base digits)))

Theorem: lendian=>nat-of-dab-digit-list-fix-digits-normalize-const

(defthm lendian=>nat-of-dab-digit-list-fix-digits-normalize-const
 (implies (syntaxp (and (quotep digits)
                        (not (dab-digit-listp base (cadr digits)))))
          (equal (lendian=>nat base digits)
                 (lendian=>nat base
                               (dab-digit-list-fix base digits)))))

Theorem: lendian=>nat-of-true-list-fix

(defthm lendian=>nat-of-true-list-fix
  (equal (lendian=>nat base (true-list-fix digits))
         (lendian=>nat base digits)))

Theorem: lendian=>nat-of-nat-list-fix

(defthm lendian=>nat-of-nat-list-fix
  (equal (lendian=>nat base (nat-list-fix digits))
         (lendian=>nat base digits)))

Theorem: lendian=>nat-of-cons

(defthm lendian=>nat-of-cons
  (equal (lendian=>nat base (cons lodigit hidigits))
         (+ (dab-digit-fix base lodigit)
            (* (dab-base-fix base)
               (lendian=>nat base hidigits)))))

Theorem: lendian=>nat-of-append

(defthm lendian=>nat-of-append
  (equal (lendian=>nat base (append lodigits hidigits))
         (+ (lendian=>nat base lodigits)
            (* (lendian=>nat base hidigits)
               (expt (dab-base-fix base)
                     (len lodigits))))))

Theorem: digits=>nat-exec-to-lendian=>nat

(defthm digits=>nat-exec-to-lendian=>nat
  (implies (and (dab-basep base)
                (dab-digit-listp base digits)
                (natp current-nat))
           (equal (digits=>nat-exec base digits current-nat)
                  (+ (lendian=>nat base (rev digits))
                     (* (expt base (len digits))
                        current-nat)))))

Theorem: lendian=>nat-of-nil

(defthm lendian=>nat-of-nil
  (equal (lendian=>nat base nil) 0))

Theorem: lendian=>nat-of-all-zeros

(defthm lendian=>nat-of-all-zeros
  (equal (lendian=>nat base (repeat n 0))
         0))

Theorem: lendian=>nat-of-all-zeros-constant

(defthm lendian=>nat-of-all-zeros-constant
  (implies (and (syntaxp (quotep digits))
                (equal digits (repeat (len digits) 0)))
           (equal (lendian=>nat base digits) 0)))

Theorem: lendian=>nat-of-all-base-minus-1

(defthm lendian=>nat-of-all-base-minus-1
  (implies (equal digit (1- (dab-base-fix base)))
           (equal (lendian=>nat base (repeat n digit))
                  (1- (expt (dab-base-fix base) (nfix n))))))

Theorem: lendian=>nat-when-most-significant-is-0

(defthm lendian=>nat-when-most-significant-is-0
  (implies (equal (car (last digits)) 0)
           (equal (lendian=>nat base digits)
                  (lendian=>nat base (butlast digits 1)))))

Theorem: lendian=>nat-of-dab-base-fix-base

(defthm lendian=>nat-of-dab-base-fix-base
  (equal (lendian=>nat (dab-base-fix base)
                       digits)
         (lendian=>nat base digits)))

Theorem: lendian=>nat-dab-base-equiv-congruence-on-base

(defthm lendian=>nat-dab-base-equiv-congruence-on-base
  (implies (dab-base-equiv base base-equiv)
           (equal (lendian=>nat base digits)
                  (lendian=>nat base-equiv digits)))
  :rule-classes :congruence)

Theorem: lendian=>nat-upper-bound

(defthm lendian=>nat-upper-bound
  (< (lendian=>nat base digits)
     (expt (dab-base-fix base) (len digits)))
  :rule-classes
  ((:linear :trigger-terms ((lendian=>nat base digits)))))

Subtopics

Digits=>nat-exec: Tail-recursive code for the execution of bendian=>nat and lendian=>nat.