Constraints induced by a tree that matches a range numeric value notation.
Theorem:
(defthm constraints-from-tree-match-in-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)) min) (equal (num-val-range->max (element-num-val->get element)) max)) (and (<= min (car (tree->string tree))) (<= (car (tree->string tree)) max))) :rule-classes nil)