Attachment of bip32-path-set-closedp-exec to bip32-path-set-closedp.
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-path-set-closedp-exec-constraint1 (equal (bip32-path-set-closedp-exec paths) (mv-let (path prefix) (bip32-path-set-closedp-witness paths) (let ((paths (bip32-path-sfix paths))) (implies (and (in path paths) (true-listp prefix) (prefixp prefix path)) (in prefix paths))))))
Theorem:
(defthm bip32-path-set-closedp-exec-constraint2 (implies (bip32-path-set-closedp-exec paths) (let ((paths (bip32-path-sfix paths))) (implies (and (in path paths) (true-listp prefix) (prefixp prefix path)) (in prefix paths)))))