(typo-read-special substrings x) → (mv prefix remainder)
Function:
(defun typo-read-special (substrings x) (declare (xargs :guard (and (character-list-listp substrings) (character-listp x)))) (let ((__function__ 'typo-read-special)) (declare (ignorable __function__)) (cond ((atom substrings) (mv nil x)) ((str::iprefixp (car substrings) x) (let ((len (mbe :logic (len (car substrings)) :exec (length (car substrings))))) (mv (take len x) (nthcdr len x)))) (t (typo-read-special (cdr substrings) x)))))
Theorem:
(defthm character-listp-of-typo-read-special.prefix (implies (force (character-listp x)) (b* (((mv ?prefix ?remainder) (typo-read-special substrings x))) (character-listp prefix))) :rule-classes :rewrite)
Theorem:
(defthm character-listp-of-typo-read-special.remainder (implies (force (character-listp x)) (b* (((mv ?prefix ?remainder) (typo-read-special substrings x))) (character-listp remainder))) :rule-classes :rewrite)
Theorem:
(defthm true-listp-of-typo-read-special (true-listp (mv-nth 0 (typo-read-special substrings x))) :rule-classes :type-prescription)
Theorem:
(defthm acl2-count-of-typo-read-special-weak (<= (acl2-count (mv-nth 1 (typo-read-special substrings x))) (acl2-count x)) :rule-classes ((:rewrite) (:linear)))
Theorem:
(defthm acl2-count-of-typo-read-special-strong (implies (mv-nth 0 (typo-read-special substrings x)) (< (acl2-count (mv-nth 1 (typo-read-special substrings x))) (acl2-count x))) :rule-classes ((:rewrite) (:linear)))