Constraints induced by a tree that matches a direct numeric value notation.
Theorem:
(defthm constraints-from-tree-match-exact (implies (and (tree-match-element-p tree element *grammar*) (element-case element :num-val) (num-val-case (element-num-val->get element) :direct) (equal (num-val-direct->get (element-num-val->get element)) nats)) (equal (car (tree->string tree)) (car (nat-list-fix nats)))) :rule-classes nil)