Recognizer for bip44-coin-type.
(bip44-coin-type-p x) → yes/no
Function:
(defun bip44-coin-type-p (x) (declare (xargs :guard t)) (mbe :logic (unsigned-byte-p 31 x) :exec (and (integerp x) (<= 0 x) (< x 2147483648))))
Theorem:
(defthm booleanp-of-bip44-coin-type-p (b* ((yes/no (bip44-coin-type-p x))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm bip44-coin-type-p-forward-unsigned-byte-p (implies (bip44-coin-type-p x) (unsigned-byte-p 31 x)) :rule-classes :forward-chaining)
Theorem:
(defthm unsigned-byte-p-rewrite-bip44-coin-type-p (equal (unsigned-byte-p 31 x) (bip44-coin-type-p x)))
Theorem:
(defthm natp-when-bip44-coin-type-p (implies (bip44-coin-type-p x) (natp x)) :rule-classes :compound-recognizer)