Constraints induced by parse-num-val.
Theorem: constraints-from-parse-num-val
(defthm constraints-from-parse-num-val (implies (not (mv-nth 0 (parse-num-val input))) (equal (car input) (char-code #\%))) :rule-classes nil)