Constraints induced by parse-alpha/digit/dash.
Theorem:
(defthm constraints-from-parse-alpha/digit/dash (implies (not (mv-nth 0 (parse-alpha/digit/dash 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))) (equal (car input) (char-code #\-)))) :rule-classes nil)