		Search-engine friendly clone of the ACL2 documentation.

Bits/ubyte11s-digit-grouping

Bits=>beubyte11s

Group bits into unsigned 11-bit bytes, big-endian.

Signature
(bits=>beubyte11s digits) → new-digits
Arguments: digits — Guard (bit-listp digits).
Returns: new-digits — Type (ubyte11-listp new-digits).

Definitions and Theorems

Function: bits=>beubyte11s

(defun bits=>beubyte11s (digits)
  (declare (xargs :guard (bit-listp digits)))
  (declare (xargs :guard (integerp (/ (len digits) 11))))
  (let ((__function__ 'bits=>beubyte11s))
    (declare (ignorable __function__))
    (group-bendian 2 11 digits)))

Theorem: ubyte11-listp-of-bits=>beubyte11s

(defthm ubyte11-listp-of-bits=>beubyte11s
  (b* ((new-digits (bits=>beubyte11s digits)))
    (ubyte11-listp new-digits))
  :rule-classes :rewrite)

Theorem: bits=>beubyte11s-of-bit-list-fix-digits

(defthm bits=>beubyte11s-of-bit-list-fix-digits
  (equal (bits=>beubyte11s (bit-list-fix digits))
         (bits=>beubyte11s digits)))

Theorem: bits=>beubyte11s-bit-list-equiv-congruence-on-digits

(defthm bits=>beubyte11s-bit-list-equiv-congruence-on-digits
  (implies (bit-list-equiv digits digits-equiv)
           (equal (bits=>beubyte11s digits)
                  (bits=>beubyte11s digits-equiv)))
  :rule-classes :congruence)