Completeness lemmas for the mutually recursive parsing functions.
Theorem:
(defthm parse-alternation-when-tree-match-lemma (pred-alternation input))
Theorem:
(defthm parse-concatenation-when-tree-match-lemma (pred-concatenation input))
Theorem:
(defthm parse-repetition-when-tree-match-lemma (pred-repetition input))
Theorem:
(defthm parse-element-when-tree-match-lemma (pred-element input))
Theorem:
(defthm parse-group-when-tree-match-lemma (pred-group input))
Theorem:
(defthm parse-option-when-tree-match-lemma (pred-option input))
Theorem:
(defthm parse-alt-rest-when-tree-list-match-lemma (pred-alt-rest input))
Theorem:
(defthm parse-alt-rest-comp-when-tree-match-lemma (pred-alt-rest-comp input))
Theorem:
(defthm parse-conc-rest-when-tree-list-match-lemma (pred-conc-rest input))
Theorem:
(defthm parse-conc-rest-comp-when-tree-match-lemma (pred-conc-rest-comp input))