Theorems about converting digits to natural numbers and back.
lendian=>nat is right inverse of nat=>lendian*, nat=>lendian+, and nat=>lendian, over digits without superfluous zeros in the most significant positions.
bendian=>nat is right inverse of nat=>bendian*, nat=>bendian+, and nat=>bendian, over digits without superfluous zeros in the most significant positions.
That is, converting digits to a natural number, and then converting the number to digits, yields the original digits, but without superfluous zeros in the most significant positions. We remove those superfluous zeros, in the right hand sides of the equalities, via the trimming functions, as appropriate.
Theorem:
(defthm nat=>lendian*-of-lendian=>nat (equal (nat=>lendian* base (lendian=>nat base digits)) (trim-lendian* (dab-digit-list-fix base digits))))
Theorem:
(defthm nat=>lendian+-of-lendian=>nat (equal (nat=>lendian+ base (lendian=>nat base digits)) (trim-lendian+ (dab-digit-list-fix base digits))))
Theorem:
(defthm nat=>lendian-of-lendian=>nat (equal (nat=>lendian base (len digits) (lendian=>nat base digits)) (dab-digit-list-fix base digits)))
Theorem:
(defthm nat=>bendian*-of-bendian=>nat (equal (nat=>bendian* base (bendian=>nat base digits)) (trim-bendian* (dab-digit-list-fix base digits))))
Theorem:
(defthm nat=>bendian+-of-bendian=>nat (equal (nat=>bendian+ base (bendian=>nat base digits)) (trim-bendian+ (dab-digit-list-fix base digits))))
Theorem:
(defthm nat=>bendian-of-bendian=>nat (equal (nat=>bendian base (len digits) (bendian=>nat base digits)) (dab-digit-list-fix base digits)))