Constraints induced by parse-char-val.
Theorem:
(defthm constraints-from-parse-char-val (implies (not (mv-nth 0 (parse-char-val input))) (or (and (equal (car input) (char-code #\%)) (member-equal (cadr input) (chars=>nats '(#\I #\S #\i #\s)))) (equal (car input) (char-code #\")))) :rule-classes nil)