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