Convert a natural number to its minimum-length big-endian list of unsigned 11-bit bytes, seen as sigits in base 2048.
(nat=>beubyte11s* nat) → digits
Function:
(defun nat=>beubyte11s* (nat) (declare (xargs :guard (natp nat))) (let ((__function__ 'nat=>beubyte11s*)) (declare (ignorable __function__)) (nat=>bendian* 2048 nat)))
Theorem:
(defthm ubyte11-listp-of-nat=>beubyte11s* (b* ((digits (nat=>beubyte11s* nat))) (ubyte11-listp digits)) :rule-classes :rewrite)
Theorem:
(defthm nat=>beubyte11s*-of-nfix-nat (equal (nat=>beubyte11s* (nfix nat)) (nat=>beubyte11s* nat)))
Theorem:
(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)