		Search-engine friendly clone of the ACL2 documentation.

Grammar-parser-completeness

Parse-element-when-tree-match-induction-step-4

Fourth induction step of the completeness lemma for parse-element.

Definitions and Theorems

Theorem: parse-element-when-tree-match-induction-step-4

(defthm parse-element-when-tree-match-induction-step-4
  (implies (and (mv-nth 0 (parse-rulename input))
                (mv-nth 0 (parse-group input))
                (mv-nth 0 (parse-option input))
                (not (mv-nth 0 (parse-char-val input)))
                (pred-group input)
                (pred-option input))
           (pred-element input)))