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