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