Convert a natural number to its big-endian list of unsigned 11-bit bytes, seen as digits in base 2048, of specified length.
(nat=>beubyte11s width nat) → digits
Function:
(defun nat=>beubyte11s (width nat) (declare (xargs :guard (and (natp width) (natp nat)))) (declare (xargs :guard (< nat (expt 2048 width)))) (let ((__function__ 'nat=>beubyte11s)) (declare (ignorable __function__)) (nat=>bendian 2048 width nat)))
Theorem:
(defthm ubyte11-listp-of-nat=>beubyte11s (b* ((digits (nat=>beubyte11s width nat))) (ubyte11-listp digits)) :rule-classes :rewrite)
Theorem:
(defthm nat=>beubyte11s-of-nfix-width (equal (nat=>beubyte11s (nfix width) nat) (nat=>beubyte11s width nat)))
Theorem:
(defthm nat=>beubyte11s-nat-equiv-congruence-on-width (implies (nat-equiv width width-equiv) (equal (nat=>beubyte11s width nat) (nat=>beubyte11s width-equiv nat))) :rule-classes :congruence)
Theorem:
(defthm nat=>beubyte11s-of-nfix-nat (equal (nat=>beubyte11s width (nfix nat)) (nat=>beubyte11s width nat)))
Theorem:
(defthm nat=>beubyte11s-nat-equiv-congruence-on-nat (implies (nat-equiv nat nat-equiv) (equal (nat=>beubyte11s width nat) (nat=>beubyte11s width nat-equiv))) :rule-classes :congruence)
Theorem:
(defthm len-of-nat=>beubyte11s (equal (len (nat=>beubyte11s width nat)) (nfix width)))