Rules about value-array->elemtype.
These turn value-array->elemtype into specific types given that the argument satisfies predicates like uchar-arrayp. Hypotheses that arrays satisfy these predicates are in the generated theorems, so they can be discharged.
Theorem:
(defthm value-array->elemtype-when-uchar-arrayp (implies (uchar-arrayp x) (equal (value-array->elemtype x) (type-uchar))))
Theorem:
(defthm value-array->elemtype-when-schar-arrayp (implies (schar-arrayp x) (equal (value-array->elemtype x) (type-schar))))
Theorem:
(defthm value-array->elemtype-when-ushort-arrayp (implies (ushort-arrayp x) (equal (value-array->elemtype x) (type-ushort))))
Theorem:
(defthm value-array->elemtype-when-sshort-arrayp (implies (sshort-arrayp x) (equal (value-array->elemtype x) (type-sshort))))
Theorem:
(defthm value-array->elemtype-when-uint-arrayp (implies (uint-arrayp x) (equal (value-array->elemtype x) (type-uint))))
Theorem:
(defthm value-array->elemtype-when-sint-arrayp (implies (sint-arrayp x) (equal (value-array->elemtype x) (type-sint))))
Theorem:
(defthm value-array->elemtype-when-ulong-arrayp (implies (ulong-arrayp x) (equal (value-array->elemtype x) (type-ulong))))
Theorem:
(defthm value-array->elemtype-when-slong-arrayp (implies (slong-arrayp x) (equal (value-array->elemtype x) (type-slong))))
Theorem:
(defthm value-array->elemtype-when-ullong-arrayp (implies (ullong-arrayp x) (equal (value-array->elemtype x) (type-ullong))))
Theorem:
(defthm value-array->elemtype-when-sllong-arrayp (implies (sllong-arrayp x) (equal (value-array->elemtype x) (type-sllong))))