Disambiguation between
Theorem:
(defthm fail-wsp-when-match-*-rule-/-*cwsp-cnl-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-wsp rest-input))) (mv-nth 0 (parse-wsp (append (tree-list->string trees) rest-input)))))