Constraints induced by a list of terminated trees that matches
Theorem:
(defthm constraints-from-tree-list-match-1*digit (implies (and (tree-list-match-repetition-p trees (1*_ *digit*) *grammar*) (tree-list-terminatedp trees)) (and (<= (char-code #\0) (car (tree-list->string trees))) (<= (car (tree-list->string trees)) (char-code #\9)))) :rule-classes nil)