Physlib.Mathematics.DataStructures.FourTree.UniqueMap

Given a function $f: \alpha_4 \to \alpha_4$, the function `uniqueMap4` maps a value of type $\text{Leaf } \alpha_4$. Specifically, for a leaf containing an element $x \in \alpha_4$, denoted as $\text{leaf}(x)$, the function returns a new leaf containing the transformed element, $\text{leaf}(f(x))$.

Given a function $f: \alpha_4 \to \alpha_4$, the function `uniqueMap4` acts on a `Twig` $T$, which consists of a value $x \in \alpha_3$ and a multiset of leaves $L = \{ \text{leaf}(y_1), \text{leaf}(y_2), \dots, \text{leaf}(y_n) \}$ containing values $y_i \in \alpha_4$. The function returns a new `Twig` $(x, L')$, where the new multiset of leaves $L'$ is constructed by applying $f$ to each $y_i$ and retaining the result $f(y_i)$ only if it is not already present in the original set of values $\{y_1, \dots, y_n\}$. Formally, if $Y = \{y_1, \dots, y_n\}$, then $L' = \{ \text{leaf}(f(y)) \mid y \in Y, f(y) \notin Y \}$.

Given a function $f: \alpha_4 \to \alpha_4$, the function `uniqueMap4` transforms a branch $T = (x_0, \mathcal{T})$, where $x_0 \in \alpha_2$ and $\mathcal{T}$ is a multiset of twigs $\{T_1, T_2, \dots, T_n\}$ of type `Twig α3 α4`. The result is a new branch $(x_0, \{T'_1, T'_2, \dots, T'_n\})$, where each $T'_i$ is obtained by applying the `Twig.uniqueMap4` function with $f$ to the corresponding twig $T_i$. Specifically, for each twig, the function maps $f$ over its leaves and retains only those transformed values that were not originally present in that twig's leaf multiset.

Given a function $f: \alpha_4 \to \alpha_4$, the function `uniqueMap4` transforms a trunk $T = (x_0, \mathcal{B})$, where $x_0 \in \alpha_1$ is a root value and $\mathcal{B}$ is a multiset of branches. The resulting trunk is defined as $(x_0, \{ \text{Branch.uniqueMap4}(f, B) \mid B \in \mathcal{B} \})$. This operation maps $f$ over all the leaf values within the hierarchical structure of the trunk, while retaining only those transformed values that were not already present in the original leaf multiset of their respective twigs.

Given a function $f: \alpha_4 \to \alpha_4$, the function `uniqueMap4` transforms a `FourTree` $T$ (a multiset of trunks) by applying $f$ to the leaf values $a_4 \in \alpha_4$ at the bottom of the tree's hierarchy. The transformation is applied recursively through the `Trunk`, `Branch`, and `Twig` levels. For each leaf in the original tree, the transformed value $f(a_4)$ is included in the resulting tree only if it was not already present in the multiset of leaves belonging to the original twig from which the leaf was derived.

Let $T$ be a `FourTree` over types $\alpha_1, \alpha_2, \alpha_3$, and $\alpha_4$. For any quadruple $x = (x_1, x_2, x_3, x_4)$ such that $x \in T$, and for any function $f : \alpha_4 \to \alpha_4$, the transformed quadruple $(x_1, x_2, x_3, f(x_4))$ is either a member of the transformed tree $T.\text{uniqueMap4 } f$ or it is a member of the original tree $T$.

Let $T$ be a `FourTree` over types $\alpha_1, \alpha_2, \alpha_3$, and $\alpha_4$. If a quadruple $C \in \alpha_1 \times \alpha_2 \times \alpha_3 \times \alpha_4$ is a member of the transformed tree $T.\text{uniqueMap4 } f$ (the tree obtained by applying $f: \alpha_4 \to \alpha_4$ to the leaf values while filtering out transformed values that were already present in the original structure), then there exists an original quadruple $(x_1, x_2, x_3, x_4) \in T$ such that $C = (x_1, x_2, x_3, f(x_4))$.

Given a function $f : \alpha_3 \to \alpha_3$, the function `uniqueMap3` transforms a `Twig` $T$, which consists of a value $x \in \alpha_3$ and a multiset of leaves. The transformation results in a new `Twig` where the function $f$ is applied to the value $x$ while the leaves remain unchanged, represented as $\text{twig}(f(x), \text{leafs})$.

Given a function $f: \alpha_3 \to \alpha_3$ and a branch $T = (v, \mathcal{T})$ consisting of a value $v \in \alpha_2$ and a multiset of twigs $\mathcal{T}$, the function `uniqueMap3` transforms the branch by mapping the data $w \in \alpha_3$ within each twig to $f(w)$. It filters the multiset of leaves $\mathcal{L}$ associated with each twig such that a leaf $z \in \alpha_4$ is retained in the new structure only if the tuple $(v, f(w), z)$ is not already a member of the original branch $T$.

Given a function $f: \alpha_3 \to \alpha_3$ and a trunk node $T = (q, \mathcal{B})$, where $q \in \alpha_1$ and $\mathcal{B}$ is a multiset of branches of type `Branch α2 α3 α4`, the function `uniqueMap3` transforms the trunk by applying the branch-level transformation `uniqueMap3` to each branch in $\mathcal{B}$ using $f$. Specifically, it preserves the trunk value $q$ and maps each branch $B \in \mathcal{B}$ to a new branch where the underlying data in the twigs (of type $\alpha_3$) is transformed by $f$, while any resulting leaf nodes (of type $\alpha_4$) that were already present in the original branch are removed.

Given a function $f: \alpha_3 \to \alpha_3$, this function transforms a `FourTree` $T$ by applying $f$ to the values of type $\alpha_3$ stored within its twigs. The operation maps the trunk-level transformation `uniqueMap3` over the multiset of trunks that constitute the root of $T$. This transformation updates the twig values and filters the leaf nodes of type $\alpha_4$ such that a path $(a_1, a_2, f(a_3), a_4)$ is retained in the new structure only if it was not already a member of the original branch in $T$.

Let $T$ be a `FourTree` over types $\alpha_1, \alpha_2, \alpha_3, \alpha_4$, representing a hierarchical collection of quadruples. If a quadruple $x = (x_1, x_2, x_3, x_4)$ is a member of $T$, then for any function $f: \alpha_3 \to \alpha_3$, the transformed quadruple $(x_1, x_2, f(x_3), x_4)$ is either a member of the tree $T.\text{uniqueMap3 } f$ (the tree resulting from applying $f$ to the third component and filtering duplicates) or was already a member of the original tree $T$.

Let $T$ be a `FourTree` defined over types $\alpha_1, \alpha_2, \alpha_3$, and $\alpha_4$, and let $f: \alpha_3 \to \alpha_3$ be a function. If a quadruple $C \in \alpha_1 \times \alpha_2 \times \alpha_3 \times \alpha_4$ is a member of the tree $T.\text{uniqueMap3 } f$ (the tree resulting from applying $f$ to the $\alpha_3$ components and filtering existing entries), then there exists a quadruple $(q_1, q_2, q_3, q_4)$ in the original tree $T$ such that $C = (q_1, q_2, f(q_3), q_4)$.