Constraints induced by a tree
that matches
Theorem:
(defthm constraints-from-tree-match-hex-val-rest-when-nonempty (implies (and (tree-match-element-p tree (?_ (/_ (1*_ (!_ (/_ "." (1*_ *hexdig*))))) (/_ (!_ (/_ "-" (1*_ *hexdig*))))) *grammar*) (consp (tree->string tree))) (member-equal (car (tree->string tree)) (chars=>nats '(#\- #\.)))) :rule-classes nil)