The ACL2 integer value of
Function:
(defun ienv->sint-min (ienv) (declare (xargs :guard (ienvp ienv))) (let ((__function__ 'ienv->sint-min)) (declare (ignorable __function__)) (sinteger-format->min (uinteger+sinteger-format->signed (integer-format->pair (char+short+int+long+llong-format->int (ienv->char+short+int+long+llong-format ienv)))))))
Theorem:
(defthm integerp-of-ienv->sint-min (b* ((min (ienv->sint-min ienv))) (integerp min)) :rule-classes :rewrite)
Theorem:
(defthm ienv->sint-min-of-ienv-fix-ienv (equal (ienv->sint-min (ienv-fix ienv)) (ienv->sint-min ienv)))
Theorem:
(defthm ienv->sint-min-ienv-equiv-congruence-on-ienv (implies (ienv-equiv ienv ienv-equiv) (equal (ienv->sint-min ienv) (ienv->sint-min ienv-equiv))) :rule-classes :congruence)