Rules that rewrite predicates for values to equalities of the types of the values.
Theorem:
(defthm ucharp-to-type-of-value (implies (valuep x) (equal (ucharp x) (equal (type-of-value x) (type-uchar)))))
Theorem:
(defthm scharp-to-type-of-value (implies (valuep x) (equal (scharp x) (equal (type-of-value x) (type-schar)))))
Theorem:
(defthm ushortp-to-type-of-value (implies (valuep x) (equal (ushortp x) (equal (type-of-value x) (type-ushort)))))
Theorem:
(defthm sshortp-to-type-of-value (implies (valuep x) (equal (sshortp x) (equal (type-of-value x) (type-sshort)))))
Theorem:
(defthm uintp-to-type-of-value (implies (valuep x) (equal (uintp x) (equal (type-of-value x) (type-uint)))))
Theorem:
(defthm sintp-to-type-of-value (implies (valuep x) (equal (sintp x) (equal (type-of-value x) (type-sint)))))
Theorem:
(defthm ulongp-to-type-of-value (implies (valuep x) (equal (ulongp x) (equal (type-of-value x) (type-ulong)))))
Theorem:
(defthm slongp-to-type-of-value (implies (valuep x) (equal (slongp x) (equal (type-of-value x) (type-slong)))))
Theorem:
(defthm ullongp-to-type-of-value (implies (valuep x) (equal (ullongp x) (equal (type-of-value x) (type-ullong)))))
Theorem:
(defthm sllongp-to-type-of-value (implies (valuep x) (equal (sllongp x) (equal (type-of-value x) (type-sllong)))))