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