		Search-engine friendly clone of the ACL2 documentation.

Bip43-purposep

Recognizer for bip43-purpose.

Function: bip43-purposep

(defun bip43-purposep (x)
  (declare (xargs :guard t))
  (integer-range-p 1 (expt 2 31) x))

Theorem: booleanp-of-bip43-purposep

(defthm booleanp-of-bip43-purposep
  (b* ((yes/no (bip43-purposep x)))
    (booleanp yes/no))
  :rule-classes :rewrite)