Read the first "part" of a wire name.
(typo-read-part x) → (mv prefix remainder)
Function:
(defun typo-read-part (x) (declare (xargs :guard (character-listp x))) (let ((__function__ 'typo-read-part)) (declare (ignorable __function__)) (b* (((when (atom x)) (mv nil nil)) ((mv prefix remainder) (typo-read-special *typo-special-substrings-chars* x)) ((when prefix) (mv prefix remainder)) ((when (vl-typo-lowercase-p (car x))) (typo-read-lowercase-part x)) ((unless (vl-typo-uppercase-p (car x))) (typo-read-part (cdr x))) ((when (atom (cdr x))) (mv (list (car x)) (cdr x))) ((when (vl-typo-lowercase-p (second x))) (b* (((mv prefix remainder) (typo-read-lowercase-part (cdr x)))) (mv (cons (car x) prefix) remainder))) ((unless (vl-typo-uppercase-p (second x))) (mv (list (car x)) (cdr x))) ((mv prefix remainder) (typo-read-uppercase-part x)) ((when (atom remainder)) (mv prefix remainder)) ((unless (vl-typo-lowercase-p (car remainder))) (mv prefix remainder))) (mv (butlast prefix 1) (append (last prefix) remainder)))))
Theorem:
(defthm character-listp-of-typo-read-part.prefix (implies (force (character-listp x)) (b* (((mv ?prefix ?remainder) (typo-read-part x))) (character-listp prefix))) :rule-classes :rewrite)
Theorem:
(defthm character-listp-of-typo-read-part.remainder (implies (force (character-listp x)) (b* (((mv ?prefix ?remainder) (typo-read-part x))) (character-listp remainder))) :rule-classes :rewrite)
Theorem:
(defthm true-listp-of-typo-read-part (true-listp (mv-nth 0 (typo-read-part x))) :rule-classes :type-prescription)
Theorem:
(defthm acl2-count-of-typo-read-part-weak (<= (acl2-count (mv-nth 1 (typo-read-part x))) (acl2-count x)) :rule-classes ((:rewrite) (:linear)))
Theorem:
(defthm acl2-count-of-typo-read-part-strong (implies (mv-nth 0 (typo-read-part x)) (< (acl2-count (mv-nth 1 (typo-read-part x))) (acl2-count x))) :rule-classes ((:rewrite) (:linear)))