		Search-engine friendly clone of the ACL2 documentation.

Digits-any-base

Nat=>bendian

Convert a natural number to its big-endian list of digits of specified length.

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

The number must be representable in the specified number of digits. The resulting list starts with zero or more 0s.

See also nat=>bendian* and nat=>bendian+.

Definitions and Theorems

Function: nat=>bendian

(defun nat=>bendian (base width nat)
  (declare (xargs :guard (and (dab-basep base)
                              (natp width)
                              (natp nat))))
  (declare (xargs :guard (< nat (expt base width))))
  (let ((__function__ 'nat=>bendian))
    (declare (ignorable __function__))
    (rev (nat=>lendian base width nat))))

Theorem: return-type-of-nat=>bendian

(defthm return-type-of-nat=>bendian
  (b* ((digits (nat=>bendian base width nat)))
    (dab-digit-listp base digits))
  :rule-classes :rewrite)

Theorem: nat-listp-of-nat=>bendian

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

Theorem: consp-of-nat=>bendian

(defthm consp-of-nat=>bendian
  (implies (not (zp width))
           (b* ((digits (nat=>bendian base width nat)))
             (consp digits)))
  :rule-classes :type-prescription)

Theorem: nat=>bendian-of-mod

(defthm nat=>bendian-of-mod
 (implies (and (dab-basep base)
               (natp width)
               (natp nat)
               (equal expt-base-width (expt base width)))
          (equal (nat=>bendian base width (mod nat expt-base-width))
                 (nat=>bendian base width nat))))

Theorem: len-of-nat=>bendian

(defthm len-of-nat=>bendian
  (equal (len (nat=>bendian base width nat))
         (nfix width)))

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

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

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

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

Theorem: nat=>bendian-of-nfix-width

(defthm nat=>bendian-of-nfix-width
  (equal (nat=>bendian base (nfix width) nat)
         (nat=>bendian base width nat)))

Theorem: nat=>bendian-nat-equiv-congruence-on-width

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

Theorem: nat=>bendian-of-nfix-nat

(defthm nat=>bendian-of-nfix-nat
  (equal (nat=>bendian base width (nfix nat))
         (nat=>bendian base width nat)))

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

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