		Search-engine friendly clone of the ACL2 documentation.

Ubyte11s-as-digits-in-base-2048

Nat=>beubyte11s*

Convert a natural number to its minimum-length big-endian list of unsigned 11-bit bytes, seen as sigits in base 2048.

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

Definitions and Theorems

Function: nat=>beubyte11s*

(defun nat=>beubyte11s* (nat)
       (declare (xargs :guard (natp nat)))
       (let ((__function__ 'nat=>beubyte11s*))
            (declare (ignorable __function__))
            (nat=>bendian* 2048 nat)))

Theorem: ubyte11-listp-of-nat=>beubyte11s*

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

Theorem: nat=>beubyte11s*-of-nfix-nat

(defthm nat=>beubyte11s*-of-nfix-nat
        (equal (nat=>beubyte11s* (nfix nat))
               (nat=>beubyte11s* nat)))

Theorem: nat=>beubyte11s*-nat-equiv-congruence-on-nat

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

Subtopics

Len-of-nat=>beubyte11s*-leq-width
Nat=>beubyte11s*-of-beubyte11s=>nat
Nat=>beubyte11s*-injectivity
Beubyte11s=>nat-of-nat=>beubyte11s*