Theorems saying that the value list recognizers imply value-listp.
Theorem:
(defthm value-listp-when-uchar-listp (implies (uchar-listp x) (value-listp x)))
Theorem:
(defthm value-listp-when-schar-listp (implies (schar-listp x) (value-listp x)))
Theorem:
(defthm value-listp-when-ushort-listp (implies (ushort-listp x) (value-listp x)))
Theorem:
(defthm value-listp-when-sshort-listp (implies (sshort-listp x) (value-listp x)))
Theorem:
(defthm value-listp-when-uint-listp (implies (uint-listp x) (value-listp x)))
Theorem:
(defthm value-listp-when-sint-listp (implies (sint-listp x) (value-listp x)))
Theorem:
(defthm value-listp-when-ulong-listp (implies (ulong-listp x) (value-listp x)))
Theorem:
(defthm value-listp-when-slong-listp (implies (slong-listp x) (value-listp x)))
Theorem:
(defthm value-listp-when-ullong-listp (implies (ullong-listp x) (value-listp x)))
Theorem:
(defthm value-listp-when-sllong-listp (implies (sllong-listp x) (value-listp x)))