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