		Search-engine friendly clone of the ACL2 documentation.

Keywords-grammar-validation

Reserved-keywordp-when-grammar-reserved-keywordp

Proof of reserved-keywordp from grammar-reserved-keywordp.

This is proved via a lemma asserting that a terminated tree rooted at reserved-keyword has leaves that satisfy reserved-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 reserved-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-reserved-keywordp.

Definitions and Theorems

Theorem: reserved-keywordp-when-grammar-reserved-keywordp

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