Uchar-max-vs-slong-max
Relation between
unsigned char and signed int maxima.
Definitions and Theorems
Theorem: uchar-max-vs-slong-max
(defthm uchar-max-vs-slong-max
(<= (uchar-max) (slong-max))
:rule-classes ((:linear :trigger-terms ((uchar-max) (slong-max)))))