Constraints induced by parse-hexdig.
Theorem:
(defthm constraints-from-parse-hexdig (implies (not (mv-nth 0 (parse-hexdig input))) (or (and (<= (char-code #\0) (car input)) (<= (car input) (char-code #\9))) (and (<= (char-code #\A) (car input)) (<= (car input) (char-code #\F))) (and (<= (char-code #\a) (car input)) (<= (car input) (char-code #\z))))) :rule-classes nil)