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