The ACL2 integer value of
Based on the discussion in schar-format,
this is either
Function:
(defun ienv->schar-min (ienv) (declare (xargs :guard (ienvp ienv))) (let ((__function__ 'ienv->schar-min)) (declare (ignorable __function__)) (if (and (equal (signed-format-kind (schar-format->signed (ienv->schar-format ienv))) :twos-complement) (not (schar-format->trap (ienv->schar-format ienv)))) (- (expt 2 (1- (ienv->char-bits ienv)))) (- (1- (expt 2 (1- (ienv->char-bits ienv))))))))
Theorem:
(defthm integerp-of-ienv->schar-min (b* ((min (ienv->schar-min ienv))) (integerp min)) :rule-classes :rewrite)
Theorem:
(defthm ienv->schar-min-type-prescription (b* ((common-lisp::?min (ienv->schar-min ienv))) (and (integerp min) (< min 0))) :rule-classes :type-prescription)
Theorem:
(defthm ienv->schar-min-upper-bound (b* ((common-lisp::?min (ienv->schar-min ienv))) (<= min (if (and (equal (signed-format-kind (schar-format->signed (ienv->schar-format ienv))) :twos-complement) (not (schar-format->trap (ienv->schar-format ienv)))) -128 -127))) :rule-classes ((:linear :trigger-terms ((ienv->schar-min ienv)))))
Theorem:
(defthm ienv->schar-min-of-ienv-fix-ienv (equal (ienv->schar-min (ienv-fix ienv)) (ienv->schar-min ienv)))
Theorem:
(defthm ienv->schar-min-ienv-equiv-congruence-on-ienv (implies (ienv-equiv ienv ienv-equiv) (equal (ienv->schar-min ienv) (ienv->schar-min ienv-equiv))) :rule-classes :congruence)