		Search-engine friendly clone of the ACL2 documentation.

Keywords-grammar-validation

Contextual-keywordp-when-grammar-contextual-keywordp

Proof of contextual-keywordp from grammar-contextual-keywordp.

This is proved via a lemma asserting that a terminated tree rooted at contextual-keyword has leaves that satisfy contextual-keywordp. The lemma is proved by exhaustively opening abnf-tree-with-root-p, which splits into many cases corresponding to the many alternatives of the contextual-keyword rule, thus prescribing the exact form of the tree in each case, and in particular its leaves. The theorem is then proved by instantiating the lemma to the witness tree of grammar-contextual-keywordp.

Definitions and Theorems

Theorem: contextual-keywordp-when-grammar-contextual-keywordp

(defthm contextual-keywordp-when-grammar-contextual-keywordp
  (implies (grammar-contextual-keywordp x)
           (contextual-keywordp x)))