		Search-engine friendly clone of the ACL2 documentation.

Bits/ubyte11s-digit-grouping

Leubyte11s=>bits

Ungroup unsigned 11-bit bytes into bits, little-endian.

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

Definitions and Theorems

Function: leubyte11s=>bits

(defun leubyte11s=>bits (digits)
  (declare (xargs :guard (ubyte11-listp digits)))
  (let ((__function__ 'leubyte11s=>bits))
    (declare (ignorable __function__))
    (ungroup-lendian 2 11 digits)))

Theorem: bit-listp-of-leubyte11s=>bits

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

Theorem: leubyte11s=>bits-of-ubyte11-list-fix-digits

(defthm leubyte11s=>bits-of-ubyte11-list-fix-digits
  (equal (leubyte11s=>bits (ubyte11-list-fix digits))
         (leubyte11s=>bits digits)))

Theorem: leubyte11s=>bits-ubyte11-list-equiv-congruence-on-digits

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