		Search-engine friendly clone of the ACL2 documentation.

Digits-any-base

Nat=>digits=>nat-inverses-theorems

Theorems about converting natural numbers to digits and back.

lendian=>nat is left inverse of nat=>lendian*, nat=>lendian+, and nat=>lendian, over natural numbers.

bendian=>nat is left inverse of nat=>bendian*, nat=>bendian+, and nat=>bendian, over natural numbers.

That is, converting a natural number to digits (whether zero or more, one or more, or of given width), and then converting the digits to a number, yields the starting natural number.

Definitions and Theorems

Theorem: lendian=>nat-of-nat=>lendian*

(defthm lendian=>nat-of-nat=>lendian*
  (equal (lendian=>nat base (nat=>lendian* base nat))
         (nfix nat)))

Theorem: lendian=>nat-of-nat=>lendian+

(defthm lendian=>nat-of-nat=>lendian+
  (equal (lendian=>nat base (nat=>lendian+ base nat))
         (nfix nat)))

Theorem: lendian=>nat-of-nat=>lendian

(defthm lendian=>nat-of-nat=>lendian
  (implies (< (nfix nat)
              (expt (dab-base-fix base) (nfix width)))
           (equal (lendian=>nat base (nat=>lendian base width nat))
                  (nfix nat))))

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

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

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

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

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

(defthm bendian=>nat-of-nat=>bendian
  (implies (< (nfix nat)
              (expt (dab-base-fix base) (nfix width)))
           (equal (bendian=>nat base (nat=>bendian base width nat))
                  (nfix nat))))