		Search-engine friendly clone of the ACL2 documentation.

Bip32-chain-code-p

Recognizer for bip32-chain-code.

Function: bip32-chain-code-p

(defun bip32-chain-code-p (x)
  (declare (xargs :guard t))
  (and (byte-listp x) (equal (len x) 32)))

Theorem: booleanp-of-bip32-chain-code-p

(defthm booleanp-of-bip32-chain-code-p
  (b* ((yes/no (bip32-chain-code-p x)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: byte-listp-when-bip32-chain-code-p

(defthm byte-listp-when-bip32-chain-code-p
  (implies (bip32-chain-code-p cc)
           (byte-listp cc)))

Theorem: len-when-bip32-chain-code-p

(defthm len-when-bip32-chain-code-p
  (implies (bip32-chain-code-p x)
           (equal (len x) 32))
  :rule-classes :tau-system)