Rules about value-integerp holding when the predicates for the integer types hold.
Theorem:
(defthm value-integerp-when-scharp (implies (scharp x) (value-integerp x)))
Theorem:
(defthm value-integerp-when-ucharp (implies (ucharp x) (value-integerp x)))
Theorem:
(defthm value-integerp-when-sshortp (implies (sshortp x) (value-integerp x)))
Theorem:
(defthm value-integerp-when-ushortp (implies (ushortp x) (value-integerp x)))
Theorem:
(defthm value-integerp-when-sintp (implies (sintp x) (value-integerp x)))
Theorem:
(defthm value-integerp-when-uintp (implies (uintp x) (value-integerp x)))
Theorem:
(defthm value-integerp-when-slongp (implies (slongp x) (value-integerp x)))
Theorem:
(defthm value-integerp-when-ulongp (implies (ulongp x) (value-integerp x)))
Theorem:
(defthm value-integerp-when-sllongp (implies (sllongp x) (value-integerp x)))
Theorem:
(defthm value-integerp-when-ullongp (implies (ullongp x) (value-integerp x)))
Theorem:
(defthm value-integerp-when-cintegerp (implies (cintegerp x) (value-integerp x)))