		Search-engine friendly clone of the ACL2 documentation.

Digits=>nat-exec

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

Signature
(digits=>nat-exec base digits current-nat) → final-nat
Arguments: base — Guard (dab-basep base).; digits — Guard (dab-digit-listp base digits).; current-nat — Guard (natp current-nat).
Returns: final-nat — Type (natp final-nat), given the guard.

This interprets the digits in big-endian order. Thus, bendian=>nat calls this function on the digits directly, while lendian=>nat calls this function on the reversed digits.

This definition is used for execution. For reasoning, the logic definitions of bendian=>nat and lendian=>nat should be used.

Definitions and Theorems

Function: digits=>nat-exec

(defun digits=>nat-exec (base digits current-nat)
  (declare (xargs :guard (and (dab-basep base)
                              (natp current-nat)
                              (dab-digit-listp base digits))))
  (let ((__function__ 'digits=>nat-exec))
    (declare (ignorable __function__))
    (cond ((endp digits) current-nat)
          (t (digits=>nat-exec base (cdr digits)
                               (+ (* base current-nat)
                                  (car digits)))))))

Theorem: natp-of-digits=>nat-exec

(defthm natp-of-digits=>nat-exec
  (implies
       (and (dab-basep base)
            (natp current-nat)
            (dab-digit-listp base digits))
       (b* ((final-nat (digits=>nat-exec base digits current-nat)))
         (natp final-nat)))
  :rule-classes :rewrite)