		Search-engine friendly clone of the ACL2 documentation.

Digits-any-base

Group/ungroup-inverses-theorems

Theorems about grouping and ungrouping digits.

ungroup-lendian is left inverse of group-lendian, over lists of digits whose length is a multiple of the power that relates smaller and larger bases.

ungroup-bendian is left inverse of group-bendian, over lists of digits whose length is a multiple of the power that relates smaller and larger bases.

ungroup-lendian is right inverse of group-lendian.

ungroup-bendian is right inverse of group-bendian.

Definitions and Theorems

Theorem: ungroup-lendian-of-group-lendian

(defthm ungroup-lendian-of-group-lendian
  (implies
       (integerp (/ (len digits) (pos-fix exp)))
       (equal (ungroup-lendian base
                               exp (group-lendian base exp digits))
              (dab-digit-list-fix base digits))))

Theorem: ungroup-bendian-of-group-bendian

(defthm ungroup-bendian-of-group-bendian
  (implies
       (integerp (/ (len digits) (pos-fix exp)))
       (equal (ungroup-bendian base
                               exp (group-bendian base exp digits))
              (dab-digit-list-fix base digits))))

Theorem: group-lendian-of-ungroup-lendian

(defthm group-lendian-of-ungroup-lendian
 (equal (group-lendian base
                       exp (ungroup-lendian base exp digits))
        (dab-digit-list-fix (expt (dab-base-fix base) (pos-fix exp))
                            digits)))

Theorem: group-bendian-of-ungroup-bendian

(defthm group-bendian-of-ungroup-bendian
 (equal (group-bendian base
                       exp (ungroup-bendian base exp digits))
        (dab-digit-list-fix (expt (dab-base-fix base) (pos-fix exp))
                            digits)))