# Parsing Unranked Tree Languages, Folded Once +
## 4 Unfolding Folded Trees
### Reassembly Sequences by Vector Addition Systems
: _For any metered \((k,l)\)-VAS \(V\) and operation sequence \(v_{0}\rightarrow_{p_{1}}\cdots\rightarrow_{p_{n}}v_{n}\) which visits \(I\), there exists an operation sequence \(v^{\prime}_{0}\rightarrow_{p^{\prime}_{1}}\cdots\rightarrow_{p^{\prime}_{l} }v^{\prime}_{\ell}\) such that: (i) this sequence also visits \(I\); (ii) \(v^{\prime}_{0}=v_{0}\); (iii) the sequence \(p^{\prime}_{1}\cdots p^{\prime}_{\ell}\) forms a subsequence of \(p_{1}\cdots p_{n}\); (iv) and \(\ell\leq k|I|\)._  
Proof. : Let \((s_{0};b_{0})\rightarrow_{p_{1}}\cdots\rightarrow_{p_{n}}(s_{n};b_{n})\) be an operation sequence visiting \(I\), for an arbitrary \(n\in\mathbb{N}\). Let us abbreviate it as \(p_{1}\cdots p_{n}\), leaving the vectors implicit. First, consider the singleton case where \(I=\{i\}\), when the following procedure constructs the indicated subsequence. Define \(P(p_{1}\cdots p_{n},i)\) recursively as:  
1. Let \(j\) be the smallest index such that, with \((s_{0};b_{0})\rightarrow_{p_{1}}\cdots\rightarrow_{p_{j}}(s_{j};b_{j})\), the vector \(s_{j}\) is nonzero at position \(i\). 2. If \(j=0\), return the empty sequence. 3. Letting \(p_{j}=((v_{1};v_{2}),(v^{\prime}_{1};v^{\prime}_{2}))\), take \(i^{\prime}\) to be the unique (as \(V\) is metered) position in \(v_{1}\), which equals \(-1\). 4. Return \(P(p_{1}\cdots p_{j-1},i^{\prime})\cdot p_{j}\). That is, the sequence constructed by finding a short visit of \(i^{\prime}\) in steps \(1\) through \(j-1\) (one must exist as step \(p_{j}\) subtracted \(1\) from that position) followed by the operation \(p_{j}\) (which visits \(i\)). Now, \(P(p_{1}\cdots p_{n},i)\), starting from \((s_{0};b_{0})\), forms an operation sequence of a length of at most \(k\), which visits \(i\). The visit to \(i\) is straight-forward (the final \"\(p_{j}\)\"), it is of a length of at most \(k\), as each level of the recursion has a distinct \(i\) (as the current one is eliminated from the sequence used in the recursive call), and adds one operation. Finally, it is an operation sequence, as each \(p_{j}\) appended in step \(4\) has its required visit provided by the step immediately prior. The budget part of the vector is unproblematic, as it can only be increased by shortening the sequence. Generalizing this to an arbitrary set \(I\subseteq[k]\) amounts to an iteration of the above argument. Here, elements of \(I\) may compete for the same operations, but this can be handled by having Step 1 in the above procedure pick nondeterministically among the \(k\) first such indices \(j\), and then letting the computation fail if two elements of \(i\) reuse an operation. In the worst case, each \(i\in I\) introduces \(k\) new operations to the subsequence, for a total of \(k|I|\) operations. Next, we define a relaxed operation sequence, which contains less information, but the existence of which implies the existence of an operation sequence. **Definition 9**. : _For a metered \((k,l)\)-VAS \(V\), a vector \(v\in\mathbb{N}^{k+l}\), and any \(I\subseteq[k]\), a destructured sequence is a tuple \((v,I,P,S)\) where \(P=p_{1}\cdots p_{k|I|}\in V^{*}\), where_  
1. \(v\rightarrow_{p_{1}}\cdots\rightarrow_{p_{k|I}}v^{\prime}\) _is an operation sequence visiting \(I\);__
2. \(S\) _is a multiset over_ \(V\) _such that for all_ \(((s;b),(s^{\prime};b^{\prime}))\in S\) _the vectors_ \(s\) _and_ \(s^{\prime}\) _are zero in all positions_ \(z\
otin I\)_;_
3. \(v+\sum_{(s,s^{\prime})\in S}(s+s^{\prime})+\sum_{(p,p^{\prime})\in P}(p+p^{ \prime})=0\)_._  
The key then becomes that we only need to consider destructured sequences to demonstrate reachability, as they turn out equivalent to full operation sequences in this setting. That is, past a certain length and ensuring a certain subsequence exists, we can disregard the order of operations. Lemma 2: _For a metered \((k,l)\)-VAS \(V\) and vector \(v\in\mathbb{N}^{k+l}\), there exists an operation sequence \(v\rightarrow\cdots\rightarrow\mathbf{0}\) iff there exists a destructured sequence \((v,I,P,S)\)._  
Proof.