Disambiguation between two disjoint numeric ranges.
Theorem:
(defthm fail-1st-range-when-match-2nd-range (implies (and (tree-match-element-p tree element *grammar*) (element-case element :num-val) (num-val-case (element-num-val->get element) :range) (equal (num-val-range->min (element-num-val->get element)) min2) (equal (num-val-range->max (element-num-val->get element)) max2) (< (nfix max1) min2)) (mv-nth 0 (parse-in-range min1 max1 (append (tree->string tree) rest-input)))))