Rules related to integer sizes.
These are the same as the linear rules, but they are rewrite rules.
Theorem:
(defthm uchar-max-vs-sint-max-rewrite (<= (uchar-max) (sint-max)))
Theorem:
(defthm ushort-max-vs-sint-max-rewrite (<= (ushort-max) (sint-max)))
Theorem:
(defthm uchar-max-vs-slong-max-rewrite (<= (uchar-max) (slong-max)))
Theorem:
(defthm ushort-max-vs-slong-max-rewrite (<= (ushort-max) (slong-max)))
Theorem:
(defthm uint-max-vs-slong-max-rewrite (<= (uint-max) (slong-max)))
Theorem:
(defthm uchar-max-vs-sllong-max-rewrite (<= (uchar-max) (sllong-max)))
Theorem:
(defthm ushort-max-vs-sllong-max-rewrite (<= (ushort-max) (sllong-max)))
Theorem:
(defthm uint-max-vs-sllong-max-rewrite (<= (uint-max) (sllong-max)))
Theorem:
(defthm ulong-max-vs-sllong-max-rewrute (> (ulong-max) (sllong-max)))