Read as many uppercase characters as we can.
(typo-read-uppercase-part x) → (mv prefix remainder)
Function:
(defun typo-read-uppercase-part (x) (declare (xargs :guard (character-listp x))) (let ((__function__ 'typo-read-uppercase-part)) (declare (ignorable __function__)) (b* (((when (atom x)) (mv nil x)) ((unless (vl-typo-uppercase-p (car x))) (mv nil x)) ((mv prefix remainder) (typo-read-uppercase-part (cdr x)))) (mv (cons (car x) prefix) remainder))))
Theorem:
(defthm character-listp-of-typo-read-uppercase-part.prefix (implies (force (character-listp x)) (b* (((mv ?prefix ?remainder) (typo-read-uppercase-part x))) (character-listp prefix))) :rule-classes :rewrite)
Theorem:
(defthm character-listp-of-typo-read-uppercase-part.remainder (implies (force (character-listp x)) (b* (((mv ?prefix ?remainder) (typo-read-uppercase-part x))) (character-listp remainder))) :rule-classes :rewrite)
Theorem:
(defthm true-listp-of-typo-read-uppercase-part (true-listp (mv-nth 0 (typo-read-uppercase-part x))) :rule-classes :type-prescription)
Theorem:
(defthm typo-read-uppercase-under-iff (iff (mv-nth 0 (typo-read-uppercase-part x)) (vl-typo-uppercase-p (car x))))
Theorem:
(defthm acl2-count-of-typo-read-uppercase-weak (<= (acl2-count (mv-nth 1 (typo-read-uppercase-part x))) (acl2-count x)) :rule-classes ((:rewrite) (:linear)))
Theorem:
(defthm acl2-count-of-typo-read-uppercase-strong (implies (mv-nth 0 (typo-read-uppercase-part x)) (< (acl2-count (mv-nth 1 (typo-read-uppercase-part x))) (acl2-count x))) :rule-classes ((:rewrite) (:linear)))