Constraints induced by a tree that matches a group
Theorem:
(defthm constraints-from-tree-match-dash-etc (implies (and (tree-match-element-p tree element *grammar*) (equal (element-kind element) :group) (consp (element-group->get element)) (not (consp (cdr (element-group->get element)))) (consp (car (element-group->get element))) (equal (car (car (element-group->get element))) (repetition (repeat-range 1 (nati-finite 1)) (element-char-val (char-val-insensitive nil "-"))))) (equal (car (tree->string tree)) (char-code #\-))) :rule-classes nil)