		Search-engine friendly clone of the ACL2 documentation.

Bits/ubyte11s-digit-grouping

Beubyte11s=>bits

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

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

Definitions and Theorems

Function: beubyte11s=>bits

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

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

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

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

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

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

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