Numeric value notations that denote values in a set can be matched only by trees whose terminal leaves are in the set.
Theorem:
(defthm leaves-in-termset-when-match-num-val-in-termset (implies (and (tree-match-num-val-p tree num-val) (num-val-in-termset-p num-val termset)) (string-in-termset-p (tree->string tree) termset)))