		Search-engine friendly clone of the ACL2 documentation.

Ubyte11s-as-digits-in-base-2048

Beubyte11s=>nat

Convert a big-endian list of unsigned 11-bit bytes, seen as digits in base 2048, to their value.

Signature
(beubyte11s=>nat digits) → nat
Arguments: digits — Guard (ubyte11-listp digits).
Returns: nat — Type (natp nat).

Definitions and Theorems

Function: beubyte11s=>nat

(defun beubyte11s=>nat (digits)
       (declare (xargs :guard (ubyte11-listp digits)))
       (let ((__function__ 'beubyte11s=>nat))
            (declare (ignorable __function__))
            (bendian=>nat 2048 digits)))

Theorem: natp-of-beubyte11s=>nat

(defthm natp-of-beubyte11s=>nat
        (b* ((nat (beubyte11s=>nat digits)))
            (natp nat))
        :rule-classes :rewrite)

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

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

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

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

Subtopics

Beubyte11s=>nat-injectivity+
Beubyte11s=>nat-injectivity*
Nat=>beubyte11s-of-beubyte11s=>nat
Beubyte11s=>nat-of-nat=>beubyte11s
Beubyte11s=>nat-injectivity
Nat=>beubyte11s+-of-beubyte11s=>nat
Nat=>beubyte11s*-of-beubyte11s=>nat
Beubyte11s=>nat-of-nat=>beubyte11s+
Beubyte11s=>nat-of-nat=>beubyte11s*