(charlist-has-some-down-alpha-p x) → *
Function:
(defun charlist-has-some-down-alpha-p (x) (declare (xargs :guard (character-listp x))) (let ((acl2::__function__ 'charlist-has-some-down-alpha-p)) (declare (ignorable acl2::__function__)) (if (atom x) nil (or (down-alpha-p (car x)) (charlist-has-some-down-alpha-p (cdr x))))))