Some theorems about terminated trees matching certain elements.
Theorem:
(defthm tree-nonleaf-when-match-rulename/group/option (implies (and (tree-match-element-p tree element rules) (member-eq (element-kind element) '(:rulename :group :option)) (tree-terminatedp tree)) (equal (tree-kind tree) :nonleaf)))
Theorem:
(defthm tree-rulename-when-match-rulename (implies (and (tree-match-element-p tree element rules) (element-case element :rulename) (tree-terminatedp tree)) (equal (tree-nonleaf->rulename? tree) (element-rulename->get element))))
Theorem:
(defthm tree-branches-match-alt-when-match-rulename (implies (and (tree-match-element-p tree element rules) (element-case element :rulename) (equal alt (lookup-rulename (element-rulename->get element) rules)) (tree-terminatedp tree)) (tree-list-list-match-alternation-p (tree-nonleaf->branches tree) alt rules)))