Completeness theorem for parse-*-rule-/-*cwsp-cnl.
Theorem:
(defthm parse-*-rule-/-*cwsp-cnl-when-tree-list-match-and-restriction (implies (and (tree-list-match-repetition-p trees (*_ (!_ (/_ *rule*) (/_ (!_ (/_ (*_ *c-wsp*) *c-nl*))))) *grammar*) (tree-list-terminatedp trees) (tree-list-*-rule-/-*cwsp-cnl-restriction-p trees) (mv-nth 0 (parse-rule-/-*cwsp-cnl rest-input)) (mv-nth 0 (parse-wsp rest-input))) (equal (parse-*-rule-/-*cwsp-cnl (append (tree-list->string trees) rest-input)) (mv nil (tree-list-fix trees) (nat-list-fix rest-input)))))