		Search-engine friendly clone of the ACL2 documentation.

Bip32-key-tree

Bip32-key-treep

Recognizer for bip32-key-tree structures.

Signature
(bip32-key-treep x) → *

Definitions and Theorems

Function: bip32-key-treep

(defun bip32-key-treep (x)
  (declare (xargs :guard t))
  (let ((__function__ 'bip32-key-treep))
    (declare (ignorable __function__))
    (and (true-listp x)
         (eql (len x) 5)
         (b* ((root-key (std::da-nth 0 x))
              (root-depth (std::da-nth 1 x))
              (root-index (std::da-nth 2 x))
              (root-parent (std::da-nth 3 x))
              (index-tree (std::da-nth 4 x)))
           (and (bip32-ext-key-p root-key)
                (bytep root-depth)
                (ubyte32p root-index)
                (byte-listp root-parent)
                (bip32-index-treep index-tree)
                (bip32-valid-keys-p root-key index-tree)
                (bip32-valid-depths-p root-depth index-tree)
                (implies (equal root-depth 0)
                         (equal root-index 0))
                (equal (len root-parent) 4)
                (implies (equal root-depth 0)
                         (equal root-parent (list 0 0 0 0))))))))

Theorem: consp-when-bip32-key-treep

(defthm consp-when-bip32-key-treep
  (implies (bip32-key-treep x) (consp x))
  :rule-classes :compound-recognizer)