Bin-digitp-when-grammar-bin-digitp
Proof of bin-digitp from grammar-bin-digitp.
This is proved via a lemma asserting that
a terminated tree rooted at binary-digit
has a string at the leaves
whose only element satisfies bin-digitp
(that this string is a singleton
is proved in grammar-bin-digitp).
The lemma is proved by exhaustively opening abnf-tree-with-root-p,
which splits into cases corresponding to
the alternatives of the binary-digit 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-bin-digitp.
Definitions and Theorems
Theorem: bin-digitp-when-grammar-bin-digitp
(defthm bin-digitp-when-grammar-bin-digitp
(implies (grammar-bin-digitp x)
(bin-digitp (car x))))
