Check if a conversion from type
Function:
(defun sshort-from-slong-okp (x) (declare (xargs :guard (slongp x))) (let ((__function__ 'sshort-from-slong-okp)) (declare (ignorable __function__)) (sshort-integerp (integer-from-slong x))))
Theorem:
(defthm booleanp-of-sshort-from-slong-okp (b* ((yes/no (sshort-from-slong-okp x))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm sshort-from-slong-okp-of-slong-fix-x (equal (sshort-from-slong-okp (slong-fix x)) (sshort-from-slong-okp x)))
Theorem:
(defthm sshort-from-slong-okp-slong-equiv-congruence-on-x (implies (slong-equiv x x-equiv) (equal (sshort-from-slong-okp x) (sshort-from-slong-okp x-equiv))) :rule-classes :congruence)