		Search-engine friendly clone of the ACL2 documentation.

Binary-digits-grammar-validation

Bin-digit-tree

Tree for a binary digit.

Signature
(bin-digit-tree digit) → tree
Arguments: digit — Guard (bin-digitp digit).
Returns: tree — Type (abnf-tree-with-root-p tree "binary-digit").

This is used in grammar-bin-digitp-when-bin-digitp.

Definitions and Theorems

Function: bin-digit-tree

(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: return-type-of-bin-digit-tree

(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: tree->string-of-bin-digit-tree

(defthm tree->string-of-bin-digit-tree
  (equal (abnf::tree->string (bin-digit-tree digit))
         (list (bin-digit-fix digit))))

Theorem: bin-digit-tree-of-bin-digit-fix-digit

(defthm bin-digit-tree-of-bin-digit-fix-digit
  (equal (bin-digit-tree (bin-digit-fix digit))
         (bin-digit-tree digit)))

Theorem: bin-digit-tree-bin-digit-equiv-congruence-on-digit

(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)