Check if a set of key tree paths is closed under prefix.

The set of paths of a tree is closed under prefix: if a path is in the tree, every prefix path is in the tree too. Thus, in order to represent a tree (of keys), a set of paths must satisfy this condition.

The condition that the prefix is a true list
is needed because `prefixp` ignores the final `cdr`s.
Without this condition, prefixes that are not true lists
would be required to be in the set,
which would be impossible because the set's elements are all true lists.

We introduce this function as a constrained function,
so that we can make an executable attachment for it
(in `std::define-sk` does not support
`defun-sk`'s `defun-sk` forces the guard to `encapsulate` for now to introduce this function.
A `std::define-sk` is used to locally define the witness,
which also guard-verifies the matrix of the function,
as additional validation.

A closed non-empty set of paths always contains the empty path, because the empty path is a prefix of every path.

The singleton set consisting of the empty path is closed.

If a set of paths is closed under prefix, extending a path in the set (more precisely, extending the set with the path obtained by extending an existing path in the set) results in a set of paths that is still closed under prefix. This is because every strict prefix of the new path is also a prefix of the existing path, and therefore already in the set by hypothesis.

**Theorem: **

(defthm bip32-path-set-closedp-definition (equal (bip32-path-set-closedp paths) (mv-let (path prefix) (bip32-path-set-closedp-witness paths) (b* ((paths (bip32-path-sfix paths))) (implies (and (in path paths) (true-listp prefix) (prefixp prefix path)) (in prefix paths))))) :rule-classes :definition)

**Theorem: **

(defthm booleanp-of-bip32-path-set-closedp (booleanp (bip32-path-set-closedp paths)) :rule-classes (:rewrite :type-prescription))

**Theorem: **

(defthm bip32-path-set-closedp-necc (implies (bip32-path-set-closedp paths) (b* ((paths (bip32-path-sfix paths))) (implies (and (in path paths) (true-listp prefix) (prefixp prefix path)) (in prefix paths)))))

**Theorem: **

(defthm bip32-path-set-closedp-of-bip32-path-sfix-paths (equal (bip32-path-set-closedp (bip32-path-sfix paths)) (bip32-path-set-closedp paths)))

**Theorem: **

(defthm bip32-path-set-closedp-bip32-path-set-equiv-congruence-on-paths (implies (bip32-path-set-equiv paths paths-equiv) (equal (bip32-path-set-closedp paths) (bip32-path-set-closedp paths-equiv))) :rule-classes :congruence)

**Theorem: **

(defthm empty-path-in-closed-nonempty-bip32-path-set (implies (and (bip32-path-setp paths) (not (emptyp paths)) (bip32-path-set-closedp paths)) (in nil paths)))

**Theorem: **

(defthm bip32-path-set-closedp-of-singleton-empty-path (bip32-path-set-closedp '(nil)))

**Theorem: **

(defthm bip32-path-set-closedp-of-insert-of-rcons (implies (and (bip32-path-setp paths) (bip32-path-set-closedp paths) (in path paths) (ubyte32p index)) (bip32-path-set-closedp (insert (rcons index path) paths))))

- Bip32-path-set-closedp-executable-attachment
- Executable attachment for
`bip32-path-set-closedp`.