Parsing failure propagation from DIGIT and "*" to repeat.
Theorem: fail-repeat-when-fail-digit-and-fail-star
(defthm fail-repeat-when-fail-digit-and-fail-star (implies (and (mv-nth 0 (parse-digit input)) (mv-nth 0 (parse-ichar #\* input))) (mv-nth 0 (parse-repeat input))))