Constraints induced by parse-digit.
Theorem: constraints-from-parse-digit
(defthm constraints-from-parse-digit (implies (not (mv-nth 0 (parse-digit input))) (and (<= (char-code #\0) (nfix (car input))) (<= (nfix (car input)) (char-code #\9)))) :rule-classes nil)