Boolean-literalp-when-grammar-boolean-literalp
Proof of boolean-literalp
from grammar-boolean-literalp.
This is proved via a lemma asserting that
a terminated tree rooted at boolean-literal
has leaves that satisfy boolean-literalp.
The lemma is proved by exhaustively opening abnf-tree-with-root-p,
which splits into two cases corresponding to
the two alternatives of the boolean-literal 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-boolean-literalp.
Definitions and Theorems
Theorem: boolean-literalp-when-grammar-boolean-literalp
(defthm boolean-literalp-when-grammar-boolean-literalp
(implies (grammar-boolean-literalp x)
(boolean-literalp x)))
