		Search-engine friendly clone of the ACL2 documentation.

Digits-any-base

Nat=>digits-injectivity-theorems

Theorems about the injectivity of the conversions from natural numbers to digits.

The conversions from natural numbers to digits are injective over natural numbers. These are simple consequences of the theorems about converting natural numbers to digits and back.

Definitions and Theorems

Theorem: nat=>lendian*-injectivity

(defthm nat=>lendian*-injectivity
  (equal (equal (nat=>lendian* base nat1)
                (nat=>lendian* base nat2))
         (equal (nfix nat1) (nfix nat2))))

Theorem: nat=>lendian+-injectivity

(defthm nat=>lendian+-injectivity
  (equal (equal (nat=>lendian+ base nat1)
                (nat=>lendian+ base nat2))
         (equal (nfix nat1) (nfix nat2))))

Theorem: nat=>lendian-injectivity

(defthm nat=>lendian-injectivity
  (implies (and (< (nfix nat1)
                   (expt (dab-base-fix base) (nfix width)))
                (< (nfix nat2)
                   (expt (dab-base-fix base)
                         (nfix width))))
           (equal (equal (nat=>lendian base width nat1)
                         (nat=>lendian base width nat2))
                  (equal (nfix nat1) (nfix nat2)))))

Theorem: nat=>bendian*-injectivity

(defthm nat=>bendian*-injectivity
  (equal (equal (nat=>bendian* base nat1)
                (nat=>bendian* base nat2))
         (equal (nfix nat1) (nfix nat2))))

Theorem: nat=>bendian+-injectivity

(defthm nat=>bendian+-injectivity
  (equal (equal (nat=>bendian+ base nat1)
                (nat=>bendian+ base nat2))
         (equal (nfix nat1) (nfix nat2))))

Theorem: nat=>bendian-injectivity

(defthm nat=>bendian-injectivity
  (implies (and (< (nfix nat1)
                   (expt (dab-base-fix base) (nfix width)))
                (< (nfix nat2)
                   (expt (dab-base-fix base)
                         (nfix width))))
           (equal (equal (nat=>bendian base width nat1)
                         (nat=>bendian base width nat2))
                  (equal (nfix nat1) (nfix nat2)))))