		Search-engine friendly clone of the ACL2 documentation.

Bip32-wallet-structure

Bip32-compliant-accounts-p

Check if the account keys in a tree comply with the BIP 32 wallet structure.

This is similar to bip32-compliant-addresses-p.

Definitions and Theorems

Theorem: bip32-compliant-accounts-p-suff

(defthm bip32-compliant-accounts-p-suff
 (implies
  (and
    (natp account-index-limit)
    (bip32-compliant-accounts-for-limit-p tree account-index-limit))
  (bip32-compliant-accounts-p tree)))

Theorem: booleanp-of-bip32-compliant-accounts-p

(defthm booleanp-of-bip32-compliant-accounts-p
  (b* ((yes/no (bip32-compliant-accounts-p tree)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: bip32-compliant-accounts-p-of-bip32-key-tree-fix-tree

(defthm bip32-compliant-accounts-p-of-bip32-key-tree-fix-tree
  (equal (bip32-compliant-accounts-p (bip32-key-tree-fix tree))
         (bip32-compliant-accounts-p tree)))

Theorem: bip32-compliant-accounts-p-bip32-key-tree-equiv-congruence-on-tree

(defthm
 bip32-compliant-accounts-p-bip32-key-tree-equiv-congruence-on-tree
 (implies (bip32-key-tree-equiv tree tree-equiv)
          (equal (bip32-compliant-accounts-p tree)
                 (bip32-compliant-accounts-p tree-equiv)))
 :rule-classes :congruence)