Rules about disjointness of integer values.
Theorem:
(defthm not-scharp-when-ucharp (implies (ucharp x) (not (scharp x))))
Theorem:
(defthm not-ushortp-when-ucharp (implies (ucharp x) (not (ushortp x))))
Theorem:
(defthm not-sshortp-when-ucharp (implies (ucharp x) (not (sshortp x))))
Theorem:
(defthm not-uintp-when-ucharp (implies (ucharp x) (not (uintp x))))
Theorem:
(defthm not-sintp-when-ucharp (implies (ucharp x) (not (sintp x))))
Theorem:
(defthm not-ulongp-when-ucharp (implies (ucharp x) (not (ulongp x))))
Theorem:
(defthm not-slongp-when-ucharp (implies (ucharp x) (not (slongp x))))
Theorem:
(defthm not-ullongp-when-ucharp (implies (ucharp x) (not (ullongp x))))
Theorem:
(defthm not-sllongp-when-ucharp (implies (ucharp x) (not (sllongp x))))
Theorem:
(defthm not-ucharp-when-scharp (implies (scharp x) (not (ucharp x))))
Theorem:
(defthm not-ushortp-when-scharp (implies (scharp x) (not (ushortp x))))
Theorem:
(defthm not-sshortp-when-scharp (implies (scharp x) (not (sshortp x))))
Theorem:
(defthm not-uintp-when-scharp (implies (scharp x) (not (uintp x))))
Theorem:
(defthm not-sintp-when-scharp (implies (scharp x) (not (sintp x))))
Theorem:
(defthm not-ulongp-when-scharp (implies (scharp x) (not (ulongp x))))
Theorem:
(defthm not-slongp-when-scharp (implies (scharp x) (not (slongp x))))
Theorem:
(defthm not-ullongp-when-scharp (implies (scharp x) (not (ullongp x))))
Theorem:
(defthm not-sllongp-when-scharp (implies (scharp x) (not (sllongp x))))
Theorem:
(defthm not-ucharp-when-ushortp (implies (ushortp x) (not (ucharp x))))
Theorem:
(defthm not-scharp-when-ushortp (implies (ushortp x) (not (scharp x))))
Theorem:
(defthm not-sshortp-when-ushortp (implies (ushortp x) (not (sshortp x))))
Theorem:
(defthm not-uintp-when-ushortp (implies (ushortp x) (not (uintp x))))
Theorem:
(defthm not-sintp-when-ushortp (implies (ushortp x) (not (sintp x))))
Theorem:
(defthm not-ulongp-when-ushortp (implies (ushortp x) (not (ulongp x))))
Theorem:
(defthm not-slongp-when-ushortp (implies (ushortp x) (not (slongp x))))
Theorem:
(defthm not-ullongp-when-ushortp (implies (ushortp x) (not (ullongp x))))
Theorem:
(defthm not-sllongp-when-ushortp (implies (ushortp x) (not (sllongp x))))
Theorem:
(defthm not-ucharp-when-sshortp (implies (sshortp x) (not (ucharp x))))
Theorem:
(defthm not-scharp-when-sshortp (implies (sshortp x) (not (scharp x))))
Theorem:
(defthm not-ushortp-when-sshortp (implies (sshortp x) (not (ushortp x))))
Theorem:
(defthm not-uintp-when-sshortp (implies (sshortp x) (not (uintp x))))
Theorem:
(defthm not-sintp-when-sshortp (implies (sshortp x) (not (sintp x))))
Theorem:
(defthm not-ulongp-when-sshortp (implies (sshortp x) (not (ulongp x))))
Theorem:
(defthm not-slongp-when-sshortp (implies (sshortp x) (not (slongp x))))
Theorem:
(defthm not-ullongp-when-sshortp (implies (sshortp x) (not (ullongp x))))
Theorem:
(defthm not-sllongp-when-sshortp (implies (sshortp x) (not (sllongp x))))
Theorem:
(defthm not-ucharp-when-uintp (implies (uintp x) (not (ucharp x))))
Theorem:
(defthm not-scharp-when-uintp (implies (uintp x) (not (scharp x))))
Theorem:
(defthm not-ushortp-when-uintp (implies (uintp x) (not (ushortp x))))
Theorem:
(defthm not-sshortp-when-uintp (implies (uintp x) (not (sshortp x))))
Theorem:
(defthm not-sintp-when-uintp (implies (uintp x) (not (sintp x))))
Theorem:
(defthm not-ulongp-when-uintp (implies (uintp x) (not (ulongp x))))
Theorem:
(defthm not-slongp-when-uintp (implies (uintp x) (not (slongp x))))
Theorem:
(defthm not-ullongp-when-uintp (implies (uintp x) (not (ullongp x))))
Theorem:
(defthm not-sllongp-when-uintp (implies (uintp x) (not (sllongp x))))
Theorem:
(defthm not-ucharp-when-sintp (implies (sintp x) (not (ucharp x))))
Theorem:
(defthm not-scharp-when-sintp (implies (sintp x) (not (scharp x))))
Theorem:
(defthm not-ushortp-when-sintp (implies (sintp x) (not (ushortp x))))
Theorem:
(defthm not-sshortp-when-sintp (implies (sintp x) (not (sshortp x))))
Theorem:
(defthm not-uintp-when-sintp (implies (sintp x) (not (uintp x))))
Theorem:
(defthm not-ulongp-when-sintp (implies (sintp x) (not (ulongp x))))
Theorem:
(defthm not-slongp-when-sintp (implies (sintp x) (not (slongp x))))
Theorem:
(defthm not-ullongp-when-sintp (implies (sintp x) (not (ullongp x))))
Theorem:
(defthm not-sllongp-when-sintp (implies (sintp x) (not (sllongp x))))
Theorem:
(defthm not-ucharp-when-ulongp (implies (ulongp x) (not (ucharp x))))
Theorem:
(defthm not-scharp-when-ulongp (implies (ulongp x) (not (scharp x))))
Theorem:
(defthm not-ushortp-when-ulongp (implies (ulongp x) (not (ushortp x))))
Theorem:
(defthm not-sshortp-when-ulongp (implies (ulongp x) (not (sshortp x))))
Theorem:
(defthm not-uintp-when-ulongp (implies (ulongp x) (not (uintp x))))
Theorem:
(defthm not-sintp-when-ulongp (implies (ulongp x) (not (sintp x))))
Theorem:
(defthm not-slongp-when-ulongp (implies (ulongp x) (not (slongp x))))
Theorem:
(defthm not-ullongp-when-ulongp (implies (ulongp x) (not (ullongp x))))
Theorem:
(defthm not-sllongp-when-ulongp (implies (ulongp x) (not (sllongp x))))
Theorem:
(defthm not-ucharp-when-slongp (implies (slongp x) (not (ucharp x))))
Theorem:
(defthm not-scharp-when-slongp (implies (slongp x) (not (scharp x))))
Theorem:
(defthm not-ushortp-when-slongp (implies (slongp x) (not (ushortp x))))
Theorem:
(defthm not-sshortp-when-slongp (implies (slongp x) (not (sshortp x))))
Theorem:
(defthm not-uintp-when-slongp (implies (slongp x) (not (uintp x))))
Theorem:
(defthm not-sintp-when-slongp (implies (slongp x) (not (sintp x))))
Theorem:
(defthm not-ulongp-when-slongp (implies (slongp x) (not (ulongp x))))
Theorem:
(defthm not-ullongp-when-slongp (implies (slongp x) (not (ullongp x))))
Theorem:
(defthm not-sllongp-when-slongp (implies (slongp x) (not (sllongp x))))
Theorem:
(defthm not-ucharp-when-ullongp (implies (ullongp x) (not (ucharp x))))
Theorem:
(defthm not-scharp-when-ullongp (implies (ullongp x) (not (scharp x))))
Theorem:
(defthm not-ushortp-when-ullongp (implies (ullongp x) (not (ushortp x))))
Theorem:
(defthm not-sshortp-when-ullongp (implies (ullongp x) (not (sshortp x))))
Theorem:
(defthm not-uintp-when-ullongp (implies (ullongp x) (not (uintp x))))
Theorem:
(defthm not-sintp-when-ullongp (implies (ullongp x) (not (sintp x))))
Theorem:
(defthm not-ulongp-when-ullongp (implies (ullongp x) (not (ulongp x))))
Theorem:
(defthm not-slongp-when-ullongp (implies (ullongp x) (not (slongp x))))
Theorem:
(defthm not-sllongp-when-ullongp (implies (ullongp x) (not (sllongp x))))
Theorem:
(defthm not-ucharp-when-sllongp (implies (sllongp x) (not (ucharp x))))
Theorem:
(defthm not-scharp-when-sllongp (implies (sllongp x) (not (scharp x))))
Theorem:
(defthm not-ushortp-when-sllongp (implies (sllongp x) (not (ushortp x))))
Theorem:
(defthm not-sshortp-when-sllongp (implies (sllongp x) (not (sshortp x))))
Theorem:
(defthm not-uintp-when-sllongp (implies (sllongp x) (not (uintp x))))
Theorem:
(defthm not-sintp-when-sllongp (implies (sllongp x) (not (sintp x))))
Theorem:
(defthm not-ulongp-when-sllongp (implies (sllongp x) (not (ulongp x))))
Theorem:
(defthm not-slongp-when-sllongp (implies (sllongp x) (not (slongp x))))
Theorem:
(defthm not-ullongp-when-sllongp (implies (sllongp x) (not (ullongp x))))