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