Function:
(defun string-has-some-up-alpha-p (x n xl) (declare (type string x) (type (integer 0 *) n) (type (integer 0 *) xl)) (declare (xargs :guard (and (stringp x) (natp n) (eql xl (length x))))) (declare (xargs :split-types t :guard (<= n xl))) (let ((acl2::__function__ 'string-has-some-up-alpha-p)) (declare (ignorable acl2::__function__)) (mbe :logic (charlist-has-some-up-alpha-p (nthcdr n (explode x))) :exec (if (eql n xl) nil (or (up-alpha-p (char x n)) (string-has-some-up-alpha-p x (+ 1 n) xl))))))