Top-level completeness theorem of the parser of ABNF grammars.
For every terminated tree rooted at
This is proved from parse-rulelist-when-tree-match-and-restriction and the fact that its two parsing failure hypotheses are satisfied because there is no extra input beyond the string at the leaves of the tree.
An alternative formulation is to avoid tree-fix but include the hypothesis that the tree satisfies treep.
Theorem:
(defthm parse-grammar-when-tree-match (implies (and (tree-match-element-p tree (element-rulename *rulelist*) *grammar*) (tree-terminatedp tree) (tree-rulelist-restriction-p tree)) (equal (parse-grammar (tree->string tree)) (tree-fix tree))))