Alternations, concatenation, repetitions, and elements whose terminal value notations all denote values in a set, can be matched only by (lists of (lists of)) trees whose terminal leaves are in the set.
The proof uses leaves-in-termset-when-match-num-val-in-termset and leaves-in-termset-when-match-char-val-in-termset.
Theorem:
(defthm leaves-in-termset-when-match-alternation-in-termset (implies (and (tree-list-list-match-alternation-p treess alternation rules) (alternation-in-termset-p alternation termset) (rulelist-in-termset-p rules termset)) (string-in-termset-p (tree-list-list->string treess) termset)))
Theorem:
(defthm leaves-in-termset-when-match-concatenation-in-termset (implies (and (tree-list-list-match-concatenation-p treess concatenation rules) (concatenation-in-termset-p concatenation termset) (rulelist-in-termset-p rules termset)) (string-in-termset-p (tree-list-list->string treess) termset)))
Theorem:
(defthm leaves-in-termset-when-match-repetition-in-termset (implies (and (tree-list-match-repetition-p trees repetition rules) (repetition-in-termset-p repetition termset) (rulelist-in-termset-p rules termset)) (string-in-termset-p (tree-list->string trees) termset)))
Theorem:
(defthm leaves-in-termset-when-list-match-element-in-termset (implies (and (tree-list-match-element-p trees element rules) (element-in-termset-p element termset) (rulelist-in-termset-p rules termset)) (string-in-termset-p (tree-list->string trees) termset)))
Theorem:
(defthm leaves-in-termset-when-match-element-in-termset (implies (and (tree-match-element-p tree element rules) (element-in-termset-p element termset) (rulelist-in-termset-p rules termset)) (string-in-termset-p (tree->string tree) termset)))