		Search-engine friendly clone of the ACL2 documentation.

Digits-any-base

Ungroup-bendian

Ungroup digits from a larger base to a smaller base, little-endian.

Signature
(ungroup-bendian base exp digits) → new-digits
Arguments: base — Guard (dab-basep base).; exp — Guard (posp exp).; digits — Guard (dab-digit-listp (expt (dab-base-fix base) (pos-fix exp)) digits).
Returns: new-digits — Type (dab-digit-listp base new-digits).

This is analogous to ungroup-lendian, but each digit in the larger base is converted to a big-endian sequence of exp digits in the smaller base.

Definitions and Theorems

Function: ungroup-bendian

(defun ungroup-bendian (base exp digits)
 (declare
  (xargs
      :guard
      (and (dab-basep base)
           (posp exp)
           (dab-digit-listp (expt (dab-base-fix base) (pos-fix exp))
                            digits))))
 (let ((__function__ 'ungroup-bendian))
   (declare (ignorable __function__))
   (b* ((exp (pos-fix exp))
        (base^exp (expt (dab-base-fix base) exp))
        (nat (bendian=>nat base^exp digits))
        (number-of-new-digits (* (len digits) exp))
        (new-digits (nat=>bendian base number-of-new-digits nat)))
     new-digits)))

Theorem: return-type-of-ungroup-bendian

(defthm return-type-of-ungroup-bendian
  (b* ((new-digits (ungroup-bendian base exp digits)))
    (dab-digit-listp base new-digits))
  :rule-classes :rewrite)

Theorem: ungroup-bendian-of-dab-digit-list-fix-digits

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

Theorem: ungroup-bendian-of-dab-digit-list-fix-digits-normalize-const

(defthm ungroup-bendian-of-dab-digit-list-fix-digits-normalize-const
 (implies
  (syntaxp (and (quotep digits)
                (not (dab-digit-listp base (cadr digits)))))
  (equal
   (ungroup-bendian base exp digits)
   (ungroup-bendian
        base exp
        (dab-digit-list-fix (expt (dab-base-fix base) (pos-fix exp))
                            digits)))))

Theorem: len-of-ungroup-bendian

(defthm len-of-ungroup-bendian
  (equal (len (ungroup-bendian base exp digits))
         (* (len digits) (pos-fix exp))))

Theorem: ungroup-bendian-when-exp-is-1

(defthm ungroup-bendian-when-exp-is-1
  (equal (ungroup-bendian base 1 digits)
         (dab-digit-list-fix base digits)))

Theorem: ungroup-bendian-of-dab-base-fix-base

(defthm ungroup-bendian-of-dab-base-fix-base
  (equal (ungroup-bendian (dab-base-fix base)
                          exp digits)
         (ungroup-bendian base exp digits)))

Theorem: ungroup-bendian-dab-base-equiv-congruence-on-base

(defthm ungroup-bendian-dab-base-equiv-congruence-on-base
  (implies (dab-base-equiv base base-equiv)
           (equal (ungroup-bendian base exp digits)
                  (ungroup-bendian base-equiv exp digits)))
  :rule-classes :congruence)

Theorem: ungroup-bendian-of-pos-fix-exp

(defthm ungroup-bendian-of-pos-fix-exp
  (equal (ungroup-bendian base (pos-fix exp)
                          digits)
         (ungroup-bendian base exp digits)))

Theorem: ungroup-bendian-pos-equiv-congruence-on-exp

(defthm ungroup-bendian-pos-equiv-congruence-on-exp
  (implies (pos-equiv exp exp-equiv)
           (equal (ungroup-bendian base exp digits)
                  (ungroup-bendian base exp-equiv digits)))
  :rule-classes :congruence)