Fixer for bip44-coin-type.
(bip44-coin-type-fix x) → fixed-x
Function:
(defun bip44-coin-type-fix (x) (declare (xargs :guard (bip44-coin-type-p x))) (mbe :logic (if (bip44-coin-type-p x) x 0) :exec x))
Theorem:
(defthm bip44-coin-type-p-of-bip44-coin-type-fix (b* ((fixed-x (bip44-coin-type-fix x))) (bip44-coin-type-p fixed-x)) :rule-classes :rewrite)
Theorem:
(defthm bip44-coin-type-fix-when-bip44-coin-type-p (implies (bip44-coin-type-p x) (equal (bip44-coin-type-fix x) x)))