		Search-engine friendly clone of the ACL2 documentation.

Digits-any-base

Nat=>bendian+

Convert a natural number to its non-empty minimum-length big-endian list of digits.

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

The resulting list is never empty; it is (0) if nat is 0. The + in the name of this function can be read as `one or more' (as in typical regular expression notation).

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

Definitions and Theorems

Function: nat=>bendian+

(defun nat=>bendian+ (base nat)
  (declare (xargs :guard (and (dab-basep base) (natp nat))))
  (let ((__function__ 'nat=>bendian+))
    (declare (ignorable __function__))
    (b* ((digits (nat=>bendian* base nat)))
      (or digits (list 0)))))

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

(defthm return-type-of-nat=>bendian+
  (b* ((digits (nat=>bendian+ base 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 nat)))
    (nat-listp digits))
  :rule-classes :rewrite)

Theorem: nat=>bendian+-of-0

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

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

(defthm nat=>bendian+-of-dab-base-fix-base
  (equal (nat=>bendian+ (dab-base-fix base) nat)
         (nat=>bendian+ base 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 nat)
                  (nat=>bendian+ base-equiv nat)))
  :rule-classes :congruence)

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

(defthm nat=>bendian+-of-nfix-nat
  (equal (nat=>bendian+ base (nfix nat))
         (nat=>bendian+ base 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 nat)
                  (nat=>bendian+ base nat-equiv)))
  :rule-classes :congruence)