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