		Search-engine friendly clone of the ACL2 documentation.

Bip44

Bip44-compliant-coins-p

Check if the coin keys under the purpose key in a tree comply with the BIP 44 wallet structure.

This is similar to bip44-compliant-addresses-p, but we existentially quantify over the set of coin types.

Thus, the existential witness is the set of coin types supported by the key tree.

Definitions and Theorems

Theorem: bip44-compliant-coins-p-suff

(defthm bip44-compliant-coins-p-suff
  (implies (and (bip44-coin-type-setp coins)
                (bip44-compliant-coins-for-set-p tree coins))
           (bip44-compliant-coins-p tree)))

Theorem: booleanp-of-bip44-compliant-coins-p

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

Theorem: bip44-coin-type-setp-of-bip44-supported-coin-types

(defthm bip44-coin-type-setp-of-bip44-supported-coin-types
 (implies (bip44-compliant-coins-p tree)
          (bip44-coin-type-setp (bip44-supported-coin-types tree))))

Theorem: bip44-compliant-coins-p-of-bip32-key-tree-fix-tree

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

Theorem: bip44-compliant-coins-p-bip32-key-tree-equiv-congruence-on-tree

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