# Parsing Unranked Tree Languages, Folded Once +
## 4 Unfolding Folded Trees
### Reassembly Sequences by Vector Addition Systems
This produces an operation sequence, since we maintain the destructured sequence invariant that summing \(P\), \(S\) and \(v\) produces \(0\), and as the \(i\) picked in each step is not generated by any operation in \(S\), all needed visits must already be in \(P\). After these steps, \(S\) is empty and \(P\) is an operation sequence reaching \(0\) from \(v\). For a metered \((k,l)\)-VAS \(V\) and vectors \(s_{0}\in\mathbb{N}^{k}\) and \(b_{0}\in\mathbb{N}^{l}\), it is decidable in time \(\mathcal{O}(|V|^{k^{2}+1}(\sum b_{0}))\) as to whether \(0\) is reachable from \((s_{0};b_{0})\). Proof. : All relevant tuples \((v,I,P,S)\) can be evaluated to see if they are a destructured sequence, as in Definition 9; if there is one, then by Lemma 2, there exists an operation sequence reaching \(0\) from \(v\), which is the definition of reachability. First, for a vector \(v\), define the _next smaller_ vector \(v^{\prime}\) as the one formed by decrementing the _first_ nonzero element of \(v\) (for example, for \((0,1,2)\) the next vector is \((0,0,2)\), and the next smaller of that is \((0,0,1)\)). To see that the bound holds, regard what tuples we need to test. There are \(|V|^{k^{2}}\) ways of picking \(P\) by the bound on its length, and \(I\) is entirely determined by \(P\). Try the following for all such \(P\). Given \(v\), \(I\) and \(P\), compute the \(v^{\prime}\) reached from \(v\) using the operations in \(P\). Then, construct \(S\) by searching for a path from \(v^{\prime}\) to \(0\) in the following graph. The vector \(v^{\prime}\) is a node in the graph. If the vector \((s;b)\) is a node in the graph and there exists an operation \(p=((u;v),\)\((u^{\prime};v^{\prime}))\in V\) such that:  
\(\bullet\)\(\quad s^{\prime}=s+u+u^{\prime}\), \(b^{\prime}=b+v+v^{\prime}\) (vector elements can be negative);  
The next smaller vector than \(b\) is \(b^{\prime}\);  
\(\bullet\)\(\quad u\) and \(v\) are zero in all positions not in \(I\). then there is a node \((s^{\prime};b^{\prime})\) and an edge from \((s;b)\) to \((s^{\prime};b^{\prime})\) labelled \(p\). Then, let \(S\) be a multiset of operations used (i.e., edges traversed) finding a path from \(v^{\prime}\) to \(0\) in this graph. This procedure is sound and complete. An \(S\) found this way does make \((v,I,P,S)\) a valid destructured sequence, as by construction \(v+\sum_{(s,s^{\prime})\in S}(s+s^{\prime})+\sum_{(p,p^{\prime})\in P}(p+p^{ \prime})=0\) and \(S\) only visits \(I\). All other needed properties derive from an exhaustive enumeration of possible operation sequences \(P\). If a destructured sequence does exist, this procedure will find it. Note that the only real pruning happening is requiring the budget to decrease according to the _next smaller_ order. This is necessary to limit the effect \(l\) has on the size of the graph, but as \(S\) is itself unordered requiring the budget to be used in a certain order is not a real restriction. Finally, all paths in this graph is of length at most \(\sum b_{0}\) and each node has, at most, \(|V|\) outgoing edges. Combining trying all \(P\) with exhaustive search on the graph gives a bound of \(\mathcal{O}(|V|^{k^{2}})\mathcal{O}(|V|(\sum b_{0}))=\mathcal{O}(|V|^{k^{2}+1 }(\sum b_{0}))\).