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