Constraints induced by parse-in-either-range.
Theorem:
(defthm constraints-from-parse-in-either-range (implies (not (mv-nth 0 (parse-in-either-range min1 max1 min2 max2 input))) (or (and (<= (nfix min1) (nfix (car input))) (<= (nfix (car input)) (nfix max1))) (and (<= (nfix min2) (nfix (car input))) (<= (nfix (car input)) (nfix max2))))) :rule-classes nil)