(bip32-path-set-closedp-exec-inner cur-path all-paths) → yes/no
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)