Executable version of bip32-path-set-closedp.
(bip32-path-set-closedp-exec paths) → yes/no
Roughly, bip32-path-set-closedp has the form
(forall (path prefix) (implies (and (in path paths) (true-listp prefix) (prefixp prefix path)) (in prefix paths)))
which can be written as
(forall (path) (implies (in path paths) (forall (prefix) (implies (and (true-listp prefix) (prefixp prefix path)) (in prefix paths)))))
We execute this via
an outer iteration of
Function:
(defun bip32-path-set-closedp-exec-inner (cur-path all-paths) (declare (xargs :guard (and (ubyte32-listp cur-path) (bip32-path-setp all-paths)))) (and (in (ubyte32-list-fix cur-path) (bip32-path-sfix all-paths)) (or (endp cur-path) (bip32-path-set-closedp-exec-inner (butlast cur-path 1) all-paths))))
Theorem:
(defthm booleanp-of-bip32-path-set-closedp-exec-inner (b* ((yes/no (bip32-path-set-closedp-exec-inner cur-path all-paths))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm bip32-path-set-closedp-exec-inner-of-ubyte32-list-fix-cur-path (equal (bip32-path-set-closedp-exec-inner (ubyte32-list-fix cur-path) all-paths) (bip32-path-set-closedp-exec-inner cur-path all-paths)))
Theorem:
(defthm bip32-path-set-closedp-exec-inner-ubyte32-list-equiv-congruence-on-cur-path (implies (acl2::ubyte32-list-equiv cur-path cur-path-equiv) (equal (bip32-path-set-closedp-exec-inner cur-path all-paths) (bip32-path-set-closedp-exec-inner cur-path-equiv all-paths))) :rule-classes :congruence)
Theorem:
(defthm bip32-path-set-closedp-exec-inner-of-bip32-path-sfix-all-paths (equal (bip32-path-set-closedp-exec-inner cur-path (bip32-path-sfix all-paths)) (bip32-path-set-closedp-exec-inner cur-path all-paths)))
Theorem:
(defthm bip32-path-set-closedp-exec-inner-bip32-path-set-equiv-congruence-on-all-paths (implies (bip32-path-set-equiv all-paths all-paths-equiv) (equal (bip32-path-set-closedp-exec-inner cur-path all-paths) (bip32-path-set-closedp-exec-inner cur-path all-paths-equiv))) :rule-classes :congruence)
Function:
(defun bip32-path-set-closedp-exec-outer (cur-paths all-paths) (declare (xargs :guard (and (bip32-path-setp cur-paths) (bip32-path-setp all-paths)))) (or (not (mbt (bip32-path-setp cur-paths))) (emptyp cur-paths) (and (bip32-path-set-closedp-exec-inner (head cur-paths) all-paths) (bip32-path-set-closedp-exec-outer (tail cur-paths) all-paths))))
Theorem:
(defthm booleanp-of-bip32-path-set-closedp-exec-outer (b* ((yes/no (bip32-path-set-closedp-exec-outer cur-paths all-paths))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm bip32-path-set-closedp-exec-outer-of-bip32-path-sfix-cur-paths (equal (bip32-path-set-closedp-exec-outer (bip32-path-sfix cur-paths) all-paths) (bip32-path-set-closedp-exec-outer cur-paths all-paths)))
Theorem:
(defthm bip32-path-set-closedp-exec-outer-bip32-path-set-equiv-congruence-on-cur-paths (implies (bip32-path-set-equiv cur-paths cur-paths-equiv) (equal (bip32-path-set-closedp-exec-outer cur-paths all-paths) (bip32-path-set-closedp-exec-outer cur-paths-equiv all-paths))) :rule-classes :congruence)
Theorem:
(defthm bip32-path-set-closedp-exec-outer-of-bip32-path-sfix-all-paths (equal (bip32-path-set-closedp-exec-outer cur-paths (bip32-path-sfix all-paths)) (bip32-path-set-closedp-exec-outer cur-paths all-paths)))
Theorem:
(defthm bip32-path-set-closedp-exec-outer-bip32-path-set-equiv-congruence-on-all-paths (implies (bip32-path-set-equiv all-paths all-paths-equiv) (equal (bip32-path-set-closedp-exec-outer cur-paths all-paths) (bip32-path-set-closedp-exec-outer cur-paths all-paths-equiv))) :rule-classes :congruence)
Function:
(defun bip32-path-set-closedp-exec (paths) (declare (xargs :guard (bip32-path-setp paths))) (bip32-path-set-closedp-exec-outer paths paths))
Theorem:
(defthm booleanp-of-bip32-path-set-closedp-exec (b* ((yes/no (bip32-path-set-closedp-exec paths))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm bip32-path-set-closedp-exec-of-bip32-path-sfix-paths (equal (bip32-path-set-closedp-exec (bip32-path-sfix paths)) (bip32-path-set-closedp-exec paths)))
Theorem:
(defthm bip32-path-set-closedp-exec-bip32-path-set-equiv-congruence-on-paths (implies (bip32-path-set-equiv paths paths-equiv) (equal (bip32-path-set-closedp-exec paths) (bip32-path-set-closedp-exec paths-equiv))) :rule-classes :congruence)