Correctness of bip32-valid-depths-p-exec.
We prove that bip32-valid-depths-p-exec is equivalent to bip32-valid-depths-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-depths-p-when-bip32-valid-depths-p-exec (implies (bip32-valid-depths-p-exec init paths) (bip32-valid-depths-p init paths)))
Theorem:
(defthm bip32-valid-depths-p-exec-when-bip32-valid-depths-p (implies (bip32-valid-depths-p init paths) (bip32-valid-depths-p-exec init paths)))
Theorem:
(defthm bip32-valid-depths-p-exec-is-bip32-valid-depths-p (equal (bip32-valid-depths-p-exec init paths) (bip32-valid-depths-p init paths)))