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