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