Definition of hexadecimal digits based on the grammar.
This defines a hexadecimal digit as a string at the leaves of
a terminated tree rooted at the
This characterizes a (singleton) list of Unicode characters, while hex-digitp characterizes a single Unicode character. Thus, the equivalence theorem has to take this into account.
Theorem:
(defthm grammar-hex-digitp-suff (implies (and (abnf-tree-with-root-p tree "hex-digit") (equal (abnf::tree->string tree) x)) (grammar-hex-digitp x)))
Theorem:
(defthm booleanp-of-grammar-hex-digitp (b* ((yes/no (grammar-hex-digitp x))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm singleton-when-grammar-hex-digitp (implies (grammar-hex-digitp x) (equal (len x) 1)))