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