		Search-engine friendly clone of the ACL2 documentation.

Digits-any-base

Digits=>nat-injectivity-theorems

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

The conversions from digits to natural numbers are injective over digits without superfluous zeros in the most significant positions. These are simple consequences of the theorems about converting digits to natural numbers and back. The absence of suprfluous digits can be expressed by saying that the digits, fixed with dab-digit-list-fix, are invariant under trim-lendian* or trim-lendian+.

Another formulation of the inejctivity theorems is that the conversions from digits to natural numbers are injective over lists of digits of the same length.

Note that each formulation of the injectivity theorem is proved via a ``corresponding'' inversion theorem.

Definitions and Theorems

Theorem: lendian=>nat-injectivity*

(defthm lendian=>nat-injectivity*
  (implies
       (and (equal (trim-lendian* (dab-digit-list-fix base digits1))
                   digits1)
            (equal (trim-lendian* (dab-digit-list-fix base digits2))
                   digits2))
       (equal (equal (lendian=>nat base digits1)
                     (lendian=>nat base digits2))
              (equal digits1 digits2))))

Theorem: lendian=>nat-injectivity+

(defthm lendian=>nat-injectivity+
  (implies
       (and (equal (trim-lendian+ (dab-digit-list-fix base digits1))
                   digits1)
            (equal (trim-lendian+ (dab-digit-list-fix base digits2))
                   digits2))
       (equal (equal (lendian=>nat base digits1)
                     (lendian=>nat base digits2))
              (equal digits1 digits2))))

Theorem: lendian=>nat-injectivity

(defthm lendian=>nat-injectivity
  (implies (equal (len digits1) (len digits2))
           (equal (equal (lendian=>nat base digits1)
                         (lendian=>nat base digits2))
                  (equal (dab-digit-list-fix base digits1)
                         (dab-digit-list-fix base digits2)))))

Theorem: bendian=>nat-injectivity*

(defthm bendian=>nat-injectivity*
  (implies
       (and (equal (trim-bendian* (dab-digit-list-fix base digits1))
                   digits1)
            (equal (trim-bendian* (dab-digit-list-fix base digits2))
                   digits2))
       (equal (equal (bendian=>nat base digits1)
                     (bendian=>nat base digits2))
              (equal digits1 digits2))))

Theorem: bendian=>nat-injectivity+

(defthm bendian=>nat-injectivity+
  (implies
       (and (equal (trim-bendian+ (dab-digit-list-fix base digits1))
                   digits1)
            (equal (trim-bendian+ (dab-digit-list-fix base digits2))
                   digits2))
       (equal (equal (bendian=>nat base digits1)
                     (bendian=>nat base digits2))
              (equal digits1 digits2))))

Theorem: bendian=>nat-injectivity

(defthm bendian=>nat-injectivity
  (implies (equal (len digits1) (len digits2))
           (equal (equal (bendian=>nat base digits1)
                         (bendian=>nat base digits2))
                  (equal (dab-digit-list-fix base digits1)
                         (dab-digit-list-fix base digits2)))))