Definition of the null literal based on the grammar.
This defines a null literal as a string at the leaves of
a terminated tree rooted at the
Theorem:
(defthm grammar-null-literalp-suff (implies (and (abnf-tree-with-root-p tree "null-literal") (equal (abnf::tree->string tree) x)) (grammar-null-literalp x)))
Theorem:
(defthm booleanp-of-grammar-null-literalp (b* ((yes/no (grammar-null-literalp x))) (booleanp yes/no)) :rule-classes :rewrite)