|
|
|---|
|
|
|
|---|
Fixer for bip43-purpose.
(bip43-purpose-fix x) → fixed-x
Function:
(defun bip43-purpose-fix (x) (declare (xargs :guard (bip43-purposep x))) (mbe :logic (if (bip43-purposep x) x 1) :exec x))
Theorem:
(defthm bip43-purposep-of-bip43-purpose-fix (b* ((fixed-x (bip43-purpose-fix x))) (bip43-purposep fixed-x)) :rule-classes :rewrite)
Theorem:
(defthm bip43-purpose-fix-when-bip43-purposep (implies (bip43-purposep x) (equal (bip43-purpose-fix x) x)))