		Search-engine friendly clone of the ACL2 documentation.

Nat=>digits-exec

Tail-recursive code for the execution of nat=>bendian* and nat=>lendian* (and, indirectly, of their variants).

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

This calculates the digits in big-endian order. Thus, nat=>bendian* returns the resulting digits directly, while nat=>lendian* returns the reversed resulting digits.

The fixing of the base divisor of floor serves to prove termination.

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

Definitions and Theorems

Function: nat=>digits-exec

(defun nat=>digits-exec (base nat current-digits)
 (declare
      (xargs :guard (and (dab-basep base)
                         (natp nat)
                         (dab-digit-listp base current-digits))))
 (let ((__function__ 'nat=>digits-exec))
   (declare (ignorable __function__))
   (cond ((zp nat) current-digits)
         (t (nat=>digits-exec base
                              (floor nat
                                     (mbe :logic (dab-base-fix base)
                                          :exec base))
                              (cons (mod nat base)
                                    current-digits))))))

Theorem: return-type-of-nat=>digits-exec

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