Attachment of bip32-valid-keys-p-exec to bip32-valid-keys-p.
The fact that the executable function satisfies all the constraints of the non-executable one follows from their equivalence.
We prove two of the constraints as separate theorems. Attempts at proving the attachment directly fail.
Theorem:
(defthm bip32-valid-keys-p-exec-constraint1 (equal (bip32-valid-keys-p-exec root paths) (let ((path (bip32-valid-keys-p-witness root paths))) (implies (in path (bip32-path-sfix paths)) (not (mv-nth 0 (bip32-ckd* root path)))))))
Theorem:
(defthm bip32-valid-keys-p-exec-constraint2 (implies (bip32-valid-keys-p-exec root paths) (implies (in path (bip32-path-sfix paths)) (not (mv-nth 0 (bip32-ckd* root path))))))