The ACL2 integer value of
Based on the discussion in schar-format,
this is always
Function:
(defun ienv->schar-max (ienv) (declare (xargs :guard (ienvp ienv))) (let ((__function__ 'ienv->schar-max)) (declare (ignorable __function__)) (1- (expt 2 (1- (ienv->char-bits ienv))))))
Theorem:
(defthm posp-of-ienv->schar-max (b* ((max (ienv->schar-max ienv))) (posp max)) :rule-classes :rewrite)
Theorem:
(defthm ienv->schar-max-type-prescription (b* ((common-lisp::?max (ienv->schar-max ienv))) (and (posp max) (> max 1))) :rule-classes :type-prescription)
Theorem:
(defthm ienv->schar-max-lower-bound (b* ((common-lisp::?max (ienv->schar-max ienv))) (>= max 127)) :rule-classes :linear)
Theorem:
(defthm ienv->schar-max-of-ienv-fix-ienv (equal (ienv->schar-max (ienv-fix ienv)) (ienv->schar-max ienv)))
Theorem:
(defthm ienv->schar-max-ienv-equiv-congruence-on-ienv (implies (ienv-equiv ienv ienv-equiv) (equal (ienv->schar-max ienv) (ienv->schar-max ienv-equiv))) :rule-classes :congruence)