Additional return type theorems for conversions of natural numbers to digits in base 8, with ubyte3-listp.
Theorem:
(defthm ubyte3-listp-of-nat=>bendian* (ubyte3-listp (nat=>bendian* 8 nat)))
Theorem:
(defthm ubyte3-listp-of-nat=>bendian+ (ubyte3-listp (nat=>bendian+ 8 nat)))
Theorem:
(defthm ubyte3-listp-of-nat=>bendian (ubyte3-listp (nat=>bendian 8 width nat)))
Theorem:
(defthm ubyte3-listp-of-nat=>lendian* (ubyte3-listp (nat=>lendian* 8 nat)))
Theorem:
(defthm ubyte3-listp-of-nat=>lendian+ (ubyte3-listp (nat=>lendian+ 8 nat)))
Theorem:
(defthm ubyte3-listp-of-nat=>lendian (ubyte3-listp (nat=>lendian 8 width nat)))