Rules that rewrite type-of-value to specific types under hypotheses on different array types of values.
Theorem:
(defthm type-of-value-when-uchar-arrayp (implies (uchar-arrayp x) (equal (type-of-value x) (type-array (type-uchar) (value-array->length x)))))
Theorem:
(defthm type-of-value-when-schar-arrayp (implies (schar-arrayp x) (equal (type-of-value x) (type-array (type-schar) (value-array->length x)))))
Theorem:
(defthm type-of-value-when-ushort-arrayp (implies (ushort-arrayp x) (equal (type-of-value x) (type-array (type-ushort) (value-array->length x)))))
Theorem:
(defthm type-of-value-when-sshort-arrayp (implies (sshort-arrayp x) (equal (type-of-value x) (type-array (type-sshort) (value-array->length x)))))
Theorem:
(defthm type-of-value-when-uint-arrayp (implies (uint-arrayp x) (equal (type-of-value x) (type-array (type-uint) (value-array->length x)))))
Theorem:
(defthm type-of-value-when-sint-arrayp (implies (sint-arrayp x) (equal (type-of-value x) (type-array (type-sint) (value-array->length x)))))
Theorem:
(defthm type-of-value-when-ulong-arrayp (implies (ulong-arrayp x) (equal (type-of-value x) (type-array (type-ulong) (value-array->length x)))))
Theorem:
(defthm type-of-value-when-slong-arrayp (implies (slong-arrayp x) (equal (type-of-value x) (type-array (type-slong) (value-array->length x)))))
Theorem:
(defthm type-of-value-when-ullong-arrayp (implies (ullong-arrayp x) (equal (type-of-value x) (type-array (type-ullong) (value-array->length x)))))
Theorem:
(defthm type-of-value-when-sllong-arrayp (implies (sllong-arrayp x) (equal (type-of-value x) (type-array (type-sllong) (value-array->length x)))))