(sse-max/min-sign rat rat1 sign1 sign2) → *
Function:
(defun sse-max/min-sign$inline (rat rat1 sign1 sign2) (declare (xargs :guard (and (rationalp rat) (rationalp rat1) (integerp sign1) (integerp sign2)))) (if (eql rat rat1) sign1 sign2))
Theorem:
(defthm integerp-sse-max/min-sign (implies (forced-and (integerp sign1) (integerp sign2)) (integerp (sse-max/min-sign rat rat1 sign1 sign2))) :rule-classes :type-prescription)