		Search-engine friendly clone of the ACL2 documentation.

Digits-any-base

Bendian=>nat

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

Signature
(bendian=>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: bendian=>nat

(defun bendian=>nat (base digits)
  (declare (xargs :guard (and (dab-basep base)
                              (dab-digit-listp base digits))))
  (let ((__function__ 'bendian=>nat))
    (declare (ignorable __function__))
    (mbe :exec (digits=>nat-exec base digits 0)
         :logic (lendian=>nat base (rev digits)))))

Theorem: natp-of-bendian=>nat

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

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

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

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

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

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

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

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

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

Theorem: bendian=>nat-of-cons

(defthm bendian=>nat-of-cons
  (equal (bendian=>nat base (cons hidigit lodigits))
         (+ (* (dab-digit-fix base hidigit)
               (expt (dab-base-fix base)
                     (len lodigits)))
            (bendian=>nat base lodigits))))

Theorem: bendian=>nat-of-append

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

Theorem: bendian=>nat-of-nil

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

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

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

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

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

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

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

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

(defthm bendian=>nat-when-most-significant-is-0
  (implies (equal (car digits) 0)
           (equal (bendian=>nat base digits)
                  (bendian=>nat base (cdr digits)))))

Theorem: lendian=>nat-as-bendian=>nat

(defthm lendian=>nat-as-bendian=>nat
  (equal (lendian=>nat base digits)
         (bendian=>nat base (rev digits))))

Theorem: lendian=>nat-of-rev

(defthm lendian=>nat-of-rev
  (equal (lendian=>nat base (rev digits))
         (bendian=>nat base digits)))

Theorem: bendian=>nat-of-rev

(defthm bendian=>nat-of-rev
  (equal (bendian=>nat base (rev digits))
         (lendian=>nat base digits)))

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

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

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

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

Theorem: bendian=>nat-upper-bound

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

Subtopics

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