Constraints induced by parse-repetition.
Theorem:
(defthm constraints-from-parse-repetition (implies (not (mv-nth 0 (parse-repetition input))) (or (and (<= (char-code #\A) (car input)) (<= (car input) (char-code #\Z))) (and (<= (char-code #\a) (car input)) (<= (car input) (char-code #\z))) (and (<= (char-code #\0) (car input)) (<= (car input) (char-code #\9))) (member-equal (car input) (chars=>nats '(#\" #\% #\( #\* #\< #\[))))) :rule-classes nil)