Correctness of bip32-path-set-closedp-exec.
We prove that bip32-path-set-closedp-exec is equivalent to bip32-path-set-closedp.
We first prove that each one implies the other, and then the equality follows from the fact that these functions are boolean-valued.
To prove that bip32-path-set-closedp-exec implies bip32-path-set-closedp, first recall the nested quantification of the latter illustrated in the documentation of bip32-path-set-closedp-exec: we prove that bip32-path-set-closedp-exec-inner implies the inner matrix, and that bip32-path-set-closedp-exec-outer implies the outer matrix. From these two lemmas, the desired theorem follows.
To prove that bip32-path-set-closedp implies bip32-path-set-closedp-exec, we first prove that it implies bip32-path-set-closedp-exec-inner and bip32-path-set-closedp-exec-outer.
Theorem:
(defthm bip32-path-set-closedp-exec-inner-implies-inner-matrix (implies (and (bip32-path-set-closedp-exec-inner cur-path all-paths) (ubyte32-listp cur-path) (true-listp prefix) (prefixp prefix cur-path)) (in prefix all-paths)) :rule-classes ((:rewrite :corollary (implies (and (prefixp prefix cur-path) (bip32-path-set-closedp-exec-inner cur-path all-paths) (ubyte32-listp cur-path) (true-listp prefix)) (in prefix all-paths)))))
Theorem:
(defthm bip32-path-set-closedp-exec-outer-implies-outer-matrix (implies (and (bip32-path-set-closedp-exec-outer cur-paths all-paths) (in cur-path (bip32-path-sfix cur-paths))) (bip32-path-set-closedp-exec-inner cur-path all-paths)))
Theorem:
(defthm bip32-path-set-closedp-when-bip32-path-set-closedp-exec (implies (bip32-path-set-closedp-exec paths) (bip32-path-set-closedp paths)))
Theorem:
(defthm bip32-path-set-closedp-exec-inner-when-bip32-path-set-closedp (implies (and (bip32-path-set-closedp all-paths) (bip32-path-setp all-paths) (ubyte32-listp cur-path) (in cur-path all-paths)) (bip32-path-set-closedp-exec-inner cur-path all-paths)))
Theorem:
(defthm bip32-path-set-closedp-exec-outer-when-bip32-path-set-closedp (implies (and (bip32-path-set-closedp all-paths) (bip32-path-setp all-paths) (subset cur-paths all-paths)) (bip32-path-set-closedp-exec-outer cur-paths all-paths)))
Theorem:
(defthm bip32-path-set-closedp-exec-when-bip32-path-set-closedp (implies (bip32-path-set-closedp paths) (bip32-path-set-closedp-exec paths)))
Theorem:
(defthm bip32-path-set-closedp-exec-is-bip32-path-set-closedp (equal (bip32-path-set-closedp-exec paths) (bip32-path-set-closedp paths)))