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