Top-level soundness theorem of the parser of ABNF grammars.
If parse-grammar succeeds,
it returns a parse tree for the input rooted at
An alternative formulation is to avoid nat-list-fix but include the hypothesis that the input satisfies nat-listp.
Theorem:
(defthm parse-treep-of-parse-grammar (let ((tree? (parse-grammar nats))) (implies tree? (parse-treep tree? (nat-list-fix nats) *rulelist* *grammar*))))