Tree for an octal digit.
(oct-digit-tree digit) → tree
This is used in grammar-oct-digitp-when-oct-digitp.
Function:
(defun oct-digit-tree (digit) (declare (xargs :guard (oct-digitp digit))) (let ((__function__ 'oct-digit-tree)) (declare (ignorable __function__)) (abnf::tree-nonleaf (abnf::rulename "octal-digit") (list (list (abnf::tree-leafterm (list (oct-digit-fix digit))))))))
Theorem:
(defthm return-type-of-oct-digit-tree (b* ((tree (oct-digit-tree digit))) (abnf-tree-with-root-p tree "octal-digit")) :rule-classes :rewrite)
Theorem:
(defthm tree->string-of-oct-digit-tree (equal (abnf::tree->string (oct-digit-tree digit)) (list (oct-digit-fix digit))))
Theorem:
(defthm oct-digit-tree-of-oct-digit-fix-digit (equal (oct-digit-tree (oct-digit-fix digit)) (oct-digit-tree digit)))
Theorem:
(defthm oct-digit-tree-oct-digit-equiv-congruence-on-digit (implies (oct-digit-equiv digit digit-equiv) (equal (oct-digit-tree digit) (oct-digit-tree digit-equiv))) :rule-classes :congruence)