Parsing failure propagation from "." to ("." 1*HEXDIG).
Theorem: fail-dot-1*hexdig-when-fail-dot
(defthm fail-dot-1*hexdig-when-fail-dot (implies (mv-nth 0 (parse-ichar #\. input)) (mv-nth 0 (parse-dot-1*hexdig input))))