Completeness theorem for parse-in-either-range.
Theorem:
(defthm parse-in-either-range-when-tree-match (implies (and (tree-match-element-p tree element *grammar*) (element-case element :group) (b* ((alternation (element-group->get element))) (and (consp alternation) (consp (cdr alternation)) (atom (cddr alternation)) (b* ((concatenation1 (car alternation)) (concatenation2 (cadr alternation))) (and (consp concatenation1) (atom (cdr concatenation1)) (consp concatenation2) (atom (cdr concatenation2)) (b* ((repetition1 (car concatenation1)) (repetition2 (car concatenation2))) (and (equal (repetition->range repetition1) (make-repeat-range :min 1 :max (nati-finite 1))) (equal (repetition->range repetition2) (make-repeat-range :min 1 :max (nati-finite 1))) (b* ((element1 (repetition->element repetition1)) (element2 (repetition->element repetition2))) (and (element-case element1 :num-val) (num-val-case (element-num-val->get element1) :range) (equal (num-val-range->min (element-num-val->get element1)) min1) (equal (num-val-range->max (element-num-val->get element1)) max1) (element-case element2 :num-val) (num-val-case (element-num-val->get element2) :range) (equal (num-val-range->min (element-num-val->get element2)) min2) (equal (num-val-range->max (element-num-val->get element2)) max2))))))))) (< max1 min2)) (equal (parse-in-either-range min1 max1 min2 max2 (append (tree->string tree) rest-input)) (mv nil (tree-fix tree) (nat-list-fix rest-input)))))