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