Rules about value-pointer not satisfying the predicates for the integer types.
Theorem:
(defthm not-scharp-of-value-pointer (not (scharp (value-pointer core reftype))))
Theorem:
(defthm not-ucharp-of-value-pointer (not (ucharp (value-pointer core reftype))))
Theorem:
(defthm not-sshortp-of-value-pointer (not (sshortp (value-pointer core reftype))))
Theorem:
(defthm not-ushortp-of-value-pointer (not (ushortp (value-pointer core reftype))))
Theorem:
(defthm not-sintp-of-value-pointer (not (sintp (value-pointer core reftype))))
Theorem:
(defthm not-uintp-of-value-pointer (not (uintp (value-pointer core reftype))))
Theorem:
(defthm not-slongp-of-value-pointer (not (slongp (value-pointer core reftype))))
Theorem:
(defthm not-ulongp-of-value-pointer (not (ulongp (value-pointer core reftype))))
Theorem:
(defthm not-sllongp-of-value-pointer (not (sllongp (value-pointer core reftype))))
Theorem:
(defthm not-ullongp-of-value-pointer (not (ullongp (value-pointer core reftype))))