		Search-engine friendly clone of the ACL2 documentation.

Bip32-valid-keys-p-executable-attachment

Bip32-valid-keys-p-exec-attach

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.

Definitions and Theorems

Theorem: bip32-valid-keys-p-exec-constraint1

(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: bip32-valid-keys-p-exec-constraint2

(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))))))