Tree for a decimal digit.
(dec-digit-tree digit) → tree
This is used in grammar-dec-digitp-when-dec-digitp.
If the digit is
Function:
(defun dec-digit-tree (digit) (declare (xargs :guard (dec-digitp digit))) (let ((__function__ 'dec-digit-tree)) (declare (ignorable __function__)) (b* ((digit (dec-digit-fix digit))) (if (equal digit (char-code #\0)) (abnf::tree-nonleaf (abnf::rulename "digit") (list (list (abnf::tree-leafterm (list digit))))) (abnf::tree-nonleaf (abnf::rulename "digit") (list (list (abnf::tree-nonleaf (abnf::rulename "non-zero-digit") (list (list (abnf::tree-leafterm (list digit))))))))))))
Theorem:
(defthm return-type-of-dec-digit-tree (b* ((tree (dec-digit-tree digit))) (abnf-tree-with-root-p tree "digit")) :rule-classes :rewrite)
Theorem:
(defthm tree->string-of-dec-digit-tree (equal (abnf::tree->string (dec-digit-tree digit)) (list (dec-digit-fix digit))))
Theorem:
(defthm dec-digit-tree-of-dec-digit-fix-digit (equal (dec-digit-tree (dec-digit-fix digit)) (dec-digit-tree digit)))
Theorem:
(defthm dec-digit-tree-dec-digit-equiv-congruence-on-digit (implies (dec-digit-equiv digit digit-equiv) (equal (dec-digit-tree digit) (dec-digit-tree digit-equiv))) :rule-classes :congruence)