		Search-engine friendly clone of the ACL2 documentation.

Ubyte11s-as-digits-in-base-2048

Nat=>leubyte11s*

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

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

Definitions and Theorems

Function: nat=>leubyte11s*

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

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

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

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

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

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

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

Subtopics

Len-of-nat=>leubyte11s*-leq-width
Nat=>leubyte11s*-of-leubyte11s=>nat
Nat=>leubyte11s*-injectivity
Leubyte11s=>nat-of-nat=>leubyte11s*