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