Some tau rules about values.
Theorem:
(defthm signed-integer-value-kinds (implies (or (scharp x) (sshortp x) (sintp x) (slongp x) (sllongp x)) (and (value-scalarp x) (value-arithmeticp x) (value-realp x) (value-integerp x) (value-signed-integerp x))) :rule-classes :tau-system)
Theorem:
(defthm unsigned-integer-value-kinds (implies (or (ucharp x) (ushortp x) (uintp x) (ulongp x) (ullongp x)) (and (value-scalarp x) (value-arithmeticp x) (value-realp x) (value-integerp x) (value-unsigned-integerp x))) :rule-classes :tau-system)