Convert a little-endian list of unsigned 11-bit bytes, seen as digits in base 2048, to their value.
(leubyte11s=>nat digits) → nat
Function:
(defun leubyte11s=>nat (digits) (declare (xargs :guard (ubyte11-listp digits))) (let ((__function__ 'leubyte11s=>nat)) (declare (ignorable __function__)) (lendian=>nat 2048 digits)))
Theorem:
(defthm natp-of-leubyte11s=>nat (b* ((nat (leubyte11s=>nat digits))) (natp nat)) :rule-classes :rewrite)
Theorem:
(defthm leubyte11s=>nat-of-ubyte11-list-fix-digits (equal (leubyte11s=>nat (ubyte11-list-fix digits)) (leubyte11s=>nat digits)))
Theorem:
(defthm leubyte11s=>nat-ubyte11-list-equiv-congruence-on-digits (implies (ubyte11-list-equiv digits digits-equiv) (equal (leubyte11s=>nat digits) (leubyte11s=>nat digits-equiv))) :rule-classes :congruence)