|
|
|---|
|
|
|
|---|
Correctness of bip32-valid-keys-p-exec.
We prove that bip32-valid-keys-p-exec is equivalent to bip32-valid-keys-p.
We first prove that each one implies the other, and then the equality follows from the fact that these functions are boolean-valued.
Theorem:
(defthm bip32-valid-keys-p-when-bip32-valid-keys-p-exec (implies (bip32-valid-keys-p-exec root paths) (bip32-valid-keys-p root paths)))
Theorem:
(defthm bip32-valid-keys-p-exec-when-bip32-valid-keys-p (implies (bip32-valid-keys-p root paths) (bip32-valid-keys-p-exec root paths)))
Theorem:
(defthm bip32-valid-keys-p-exec-is-bip32-valid-keys-p (equal (bip32-valid-keys-p-exec root paths) (bip32-valid-keys-p root paths)))