The ACL2 integer value of
This directly derives from
This is at least 255, as required by [C:5.2.4.2.1/1].
Function:
(defun ienv->uchar-max (ienv) (declare (xargs :guard (ienvp ienv))) (let ((__function__ 'ienv->uchar-max)) (declare (ignorable __function__)) (1- (expt 2 (ienv->char-bits ienv)))))
Theorem:
(defthm posp-of-ienv->uchar-max (b* ((max (ienv->uchar-max ienv))) (posp max)) :rule-classes :rewrite)
Theorem:
(defthm ienv->uchar-max-type-prescription (b* ((common-lisp::?max (ienv->uchar-max ienv))) (and (posp max) (> max 1))) :rule-classes :type-prescription)
Theorem:
(defthm ienv->uchar-max-lower-bound (b* ((common-lisp::?max (ienv->uchar-max ienv))) (>= max 255)) :rule-classes :linear)
Theorem:
(defthm ienv->uchar-max-of-ienv-fix-ienv (equal (ienv->uchar-max (ienv-fix ienv)) (ienv->uchar-max ienv)))
Theorem:
(defthm ienv->uchar-max-ienv-equiv-congruence-on-ienv (implies (ienv-equiv ienv ienv-equiv) (equal (ienv->uchar-max ienv) (ienv->uchar-max ienv-equiv))) :rule-classes :congruence)