Proof. By introducing slack variables \(\boldsymbol{y} \in \mathbb{N}^m\), we can replace the inequality \(A \boldsymbol{x} \le \boldsymbol{b}\) by the equation \(A \boldsymbol{x} + \boldsymbol{y} = \boldsymbol{b}\). Then apply 1. ◻

Proof of 2. Equivalently, we have \(t \xrightarrow{*} p(\boldsymbol{x})\) in \({V}^{\mathrm{rev}}\). By [thm:hybrid-2vass-hybrid], there exists a hybrid set \(S'\) such that \(\boldsymbol{x} \in S' \subseteq \mathop{\operatorname{\mathrm{Reach}}}\nolimits_{p}({{V}^{\mathrm{rev}}},{t})\) and \(\mathop{\operatorname{\mathrm{\mathrm{\small norm}}}}\nolimits(S') \le {\mathop{\operatorname{\mathrm{poly}}}\nolimits({\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V,t)})}\). Therefore, one has that \(\boldsymbol{x} \in S \cap S' \neq \emptyset\). Assume that \[S = \boldsymbol{b} + {P}^{\langle {{\boldsymbol{c}}, \cdot} \rangle \le {K}}\text{ and }S' = \boldsymbol{b}' + {P'}^{\langle {{\boldsymbol{c}'}, \cdot} \rangle \le {K'}}.\] We may interpret each periodic set as a matrix whose columns are the vectors contained in the set, e.g., \(P' \in \mathbb{N}^{d \times |P'|}\). Then the intersection of these two sets can be described as the following linear system: \[\label{eq:intersect-of-hybrid-set} \begin{align} \begin{pmatrix} P &-P' \end{pmatrix} \boldsymbol{\lambda} &= \boldsymbol{b}' - \boldsymbol{b}\\ \begin{pmatrix} \boldsymbol{c}^{\dagger} & \boldsymbol{0}\\ \boldsymbol{0} & (\boldsymbol{c}')^{\dagger} \end{pmatrix}\boldsymbol{\lambda} &\le \begin{pmatrix} K\\ K' \end{pmatrix}, \end{align}\tag{4}\] where \(\boldsymbol{\lambda} \in \mathbb{N}^{|P|+|P'|}\), and the dimension \(|P|+|P'|\) is bounded by \[(\mathop{\operatorname{\mathrm{\mathrm{\small norm}}}}\nolimits(S)+1)^3+(\mathop{\operatorname{\mathrm{\mathrm{\small norm}}}}\nolimits(S')+1)^3 \le {\mathop{\operatorname{\mathrm{poly}}}\nolimits({\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V,t), \mathop{\operatorname{\mathrm{\mathrm{\small norm}}}}\nolimits(S)})}.\] Note that \(\boldsymbol{x}\) induces a solution \(\boldsymbol{\lambda}_{\boldsymbol{x}}\) to this system. We omit the inequalities in 4 and apply 2 to obtain a solution \(\boldsymbol{\lambda}_0 \le \boldsymbol{\lambda}_{\boldsymbol{x}}\) with \[\begin{pmatrix} P &-P' \end{pmatrix} \boldsymbol{\lambda}_0 = \boldsymbol{b}' - \boldsymbol{b},\] and \(\left\Vert{\boldsymbol{\lambda}_0}\right\Vert \le {\mathop{\operatorname{\mathrm{poly}}}\nolimits({\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V,t), \mathop{\operatorname{\mathrm{\mathrm{\small norm}}}}\nolimits(S)})}\). However, since \(\boldsymbol{c},\boldsymbol{c}' \ge \boldsymbol{0}\) and \(\boldsymbol{\lambda}_0 \le \boldsymbol{\lambda}_{\boldsymbol{x}}\), one has that \[\begin{pmatrix} \boldsymbol{c}^{\dagger} & \boldsymbol{0} \\ \boldsymbol{0} & (\boldsymbol{c}')^{\dagger} \end{pmatrix}\boldsymbol{\lambda}_0 \le \begin{pmatrix} \boldsymbol{c}^{\dagger} & \boldsymbol{0}\\ \boldsymbol{0} & (\boldsymbol{c}')^{\dagger} \end{pmatrix}\boldsymbol{\lambda}_{\boldsymbol{x}} \le \begin{pmatrix} K\\ K' \end{pmatrix},\] which implies that \(\boldsymbol{\lambda}_0\) is also a solution to 4 . Let \[\boldsymbol{x}':=\boldsymbol{b} + \begin{pmatrix} P &\boldsymbol{0} \end{pmatrix} \boldsymbol{\lambda}_0.\] It holds that \(\boldsymbol{x}' \in S \cap S'\) and \(\left\Vert{\boldsymbol{x}'}\right\Vert \le {\mathop{\operatorname{\mathrm{poly}}}\nolimits({\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V,t),\mathop{\operatorname{\mathrm{\mathrm{\small norm}}}}\nolimits(S)})}\). Since \(\boldsymbol{x}' \in S'\), we obtain that \(t\xrightarrow{*}p(\boldsymbol{x}')\) in \({V}^{\mathrm{rev}}\), which implies that \(p(\boldsymbol{x}')\xrightarrow{*}t\) in \(V\). By applying 2, there exists a short run \(\rho\) with \[|\rho| \le H(\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V,t) + 3\cdot\left\Vert{\boldsymbol{x}'}\right\Vert)\le {\mathop{\operatorname{\mathrm{poly}}}\nolimits({\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V,t), \mathop{\operatorname{\mathrm{\mathrm{\small norm}}}}\nolimits(S)})}.\] We are done. ◻

Proof. Notice that any run from \(p(S)\) to \(t\) must use the bridge \(u_j\). Let \(u_j\) be the transition \(r\xrightarrow{\boldsymbol{a}}r'\) where \(r\) is a state in \(V_j\) and \(r'\) is a state in \(V_{j+1}\) (or \(r'\) is the state of \(t\) when \(j = k\)). As configurations in \(p(S)\) is reachable from \(s\), and \(t\) is reachable from \(p(S)\), by [lem:non-wide-bounded-inner-prod] our construction of \(V_j'\) guarantees that \(t\) is also reachable (in the original VASS) from \(r'(\mathop{\operatorname{\mathrm{Reach}}}\nolimits_{r'}({V_j'},{p_u(S)}))\) where \(u = \langle {\boldsymbol{n}_j, \boldsymbol{b}} \rangle\). To justify this, consider any run \(p(\boldsymbol{s}) \xrightarrow{\pi_j} r'(\boldsymbol{s}') \xrightarrow{*} t\) where \(\boldsymbol{s} \in S\). By [lem:non-wide-bounded-inner-prod] every configuration \(q(\boldsymbol{z})\) on \(\pi_j\) satisfies \(|\langle {\boldsymbol{n}_j, \boldsymbol{z}} \rangle| \le B_h\). Hence \(\pi_j\) can be easily projected into a run in \(V_j'\) from \(p_u(\boldsymbol{s})\) to \(r'(\boldsymbol{s}')\). Hence, the set \(r'(\mathop{\operatorname{\mathrm{Reach}}}\nolimits_{r'}({V_j'},{p_u(S)}))\) must contain all configurations that occurs on some run from \(p(S)\) to \(t\) after the bridge \(u_j\). Notice that \(\mathop{\operatorname{\mathrm{\mathrm{\small cyc}}}}\nolimits(V_j')\) is orthogonal to \(\boldsymbol{n}_j\). We may further assume that \(\mathop{\operatorname{\mathrm{\mathrm{\small cyc}}}}\nolimits(V_j')\) is the whole plane orthogonal to \(\boldsymbol{n}_j\) by adding isolated cycles to \(V_j'\) if necessary, hence the condition \(\langle {\boldsymbol{n}_j, P} \rangle = 0\) guarantees \(P\subseteq \mathop{\operatorname{\mathrm{\mathrm{\small cyc}}}}\nolimits(V_j')\).

We prove the lemma by backward induction on \(j\). The base case \(j = k\) is exactly 2 applied to \(V_k'\). Now we proceed with \(j < k\). By [thm:hybrid-2vass-hybrid], \(\mathop{\operatorname{\mathrm{Reach}}}\nolimits_{r'}({V_j'},{p_u(S)})\) is a finite union of hybrid sets \(S' = \boldsymbol{b}' + {P'}^{\langle {{\boldsymbol{c}'}, \cdot} \rangle \le {K'}}\) with \(\mathop{\operatorname{\mathrm{\mathrm{\small norm}}}}\nolimits(S') \le H(\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V_j'), \mathop{\operatorname{\mathrm{\mathrm{\small norm}}}}\nolimits(S))\). In the following, we let \(\overline{V_j}\) be the VASS obtained from \(V_j\) by adding the bridge transition \(u_j\) from \(r\) to \(r'\), as we need to consider the sub-runs before \(\mathcal{T}_{j+1}\). By the above argument, for one of such set \(S'\) we have \(p(S) \xrightarrow{*} r'(S')\) in \(\overline{V_j}\) and \(r'(S') \xrightarrow{*} t\) in \(\mathcal{T}_{j+1}\). We would like to apply the induction hypothesis to \(r'(S')\) in \(\mathcal{T}_{j+1}\). We are however not guaranteed that \(\langle {\boldsymbol{n}_{j+1}, P'} \rangle = 0\), and it is not straightforward to see \(P' \subseteq \mathop{\operatorname{\mathrm{\mathrm{\small SeqCone}}}}\nolimits(\mathcal{H}_{j+1})\). To meet these properties, recall that by [thm:hybrid-2vass-hybrid] we have \(P' \subseteq\mathop{\operatorname{\mathrm{\mathrm{\small cone}}}}\nolimits(V_j') + \mathop{\operatorname{\mathrm{\mathrm{\small cone}}}}\nolimits(P) \subseteq \mathop{\operatorname{\mathrm{\mathrm{\small cone}}}}\nolimits(V_j) + \mathop{\operatorname{\mathrm{\mathrm{\small cone}}}}\nolimits(P)\). Together with the condition \(P \subseteq \mathop{\operatorname{\mathrm{\mathrm{\small SeqCone}}}}\nolimits(\mathcal{H}_j)\), we have \[P' \subseteq(\mathop{\operatorname{\mathrm{\mathrm{\small cone}}}}\nolimits(P) + \mathop{\operatorname{\mathrm{\mathrm{\small cone}}}}\nolimits(V_j) ) \cap \mathbb{N}^3 \subseteq (\mathop{\operatorname{\mathrm{\mathrm{\small SeqCone}}}}\nolimits(\mathcal{H}_j) + \mathop{\operatorname{\mathrm{\mathrm{\small cone}}}}\nolimits(V_{j+1})) \cap \mathbb{N}^3 = \mathop{\operatorname{\mathrm{\mathrm{\small SeqCone}}}}\nolimits(\mathcal{H}_{j+1}).\] Then by [lem:separating-plane-non-wide] we have \(\langle {\boldsymbol{n}_{j+1}, P'} \rangle \ge 0\). Extract from \(P'\) the set of vectors \(P_+'\) with positive inner products with \(\boldsymbol{n}_{j+1}\), we claim that it is enough to add these vectors for a bounded number of times to produce a vector \(\boldsymbol{s}'\) with \(p(S) \xrightarrow{*} r'(\boldsymbol{s}') \xrightarrow{*} t\), since vectors reachable at state \(r'\) have bounded inner products with \(\boldsymbol{n}_{j+1}\) by [lem:non-wide-bounded-inner-prod]. To be specific, let \(\boldsymbol{s} \in S\) and \(\boldsymbol{s}' \in S'\) render true \(p(\boldsymbol{s}) \xrightarrow{*} r'(\boldsymbol{s}') \xrightarrow{*} t\). Then \(\boldsymbol{s}' = \boldsymbol{b}' + P'_+ \boldsymbol{c}_+ + P'_0\boldsymbol{c}_0\) for some coefficients \(\boldsymbol{c}_+\) and \(\boldsymbol{c}_0\), where \(P'_0 = P' \setminus P_+'\) contains the vectors in \(P'\) orthogonal to \(\boldsymbol{n}_{j+1}\). By [lem:non-wide-bounded-inner-prod], we have \(|\langle {\boldsymbol{n}_{j+1}, \boldsymbol{s}'} \rangle| = |\langle {\boldsymbol{n}_{j+1}, \boldsymbol{b}' + P'_+\boldsymbol{c}_+} \rangle| \le B_h\). Hence \(|\langle {\boldsymbol{n}_{j+1}, P_+'\boldsymbol{c}_+} \rangle| \le B_h + |\langle {\boldsymbol{n}_{j+1}, \boldsymbol{b}'} \rangle| \le B_h + 3B_n\cdot \mathop{\operatorname{\mathrm{\mathrm{\small norm}}}}\nolimits(S')\). Clearly the norm of \(\boldsymbol{c}_+\) is bounded by \(\left\Vert{\boldsymbol{c}_+}\right\Vert_1 \le B_h + 3B_n\cdot \mathop{\operatorname{\mathrm{\mathrm{\small norm}}}}\nolimits(S')\). In other words, \(\boldsymbol{p}' := P_+'\boldsymbol{c}_+\) is a sum of at most \(B_h + 3B_n\cdot\mathop{\operatorname{\mathrm{\mathrm{\small norm}}}}\nolimits(S')\) vectors from \(P_+'\). We have \(\left\Vert{\boldsymbol{p}'}\right\Vert \le (B_h + 3B_n)\cdot\mathop{\operatorname{\mathrm{\mathrm{\small norm}}}}\nolimits(S')^2\).

We then replace \(S'\) by \(S'' = \boldsymbol{b}' + \boldsymbol{p}' + {P_0'}^{\langle {{\boldsymbol{c}''}, \cdot} \rangle \le {K''}}\), where \(\boldsymbol{c}''\) is obtained by projecting \(\boldsymbol{c}'\) onto indices corresponding to \(P_0'\), and \(K''\) is obtained by subtracting from \(K'\) the inner product induced by \(\boldsymbol{p}'\). It still holds that \(r'(S'') \xrightarrow{*} t\) in \(\mathcal{T}_{j+1}\). Moreover, \(\mathop{\operatorname{\mathrm{\mathrm{\small norm}}}}\nolimits(S'') \le (B_h+3B_n + 1)\cdot \mathop{\operatorname{\mathrm{\mathrm{\small norm}}}}\nolimits(S')^2\). Now we apply the induction hypothesis, and deduce that there exists \(\boldsymbol{s}'' \in S''\) and a run \(r'(\boldsymbol{s}'') \xrightarrow{\pi''} t\) in \(\mathcal{T}_{k+1}\) such that \[\begin{align} \left\Vert{\boldsymbol{s}''}\right\Vert, |\pi''| &\le f_{j+1}(\mathop{\operatorname{\mathrm{\mathrm{\small norm}}}}\nolimits(S''))\\ &\le f_{j+1}((B_h + 3B_n + 1)\cdot H(\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V_j'), \mathop{\operatorname{\mathrm{\mathrm{\small norm}}}}\nolimits(S))^2)\\ &= f_{j+1}(C\cdot H(\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V_j'), \mathop{\operatorname{\mathrm{\mathrm{\small norm}}}}\nolimits(S))^2). \end{align}\] Moreover, as \(\boldsymbol{s}'' \in S'' \subseteq S' \subseteq \mathop{\operatorname{\mathrm{Reach}}}\nolimits_{r'}({V_j'},{p_u(S)}) \subseteq \mathop{\operatorname{\mathrm{Reach}}}\nolimits_{r'}({\overline{V_j}},{p(S)})\), there exists \(\boldsymbol{s} \in S\) and a run \(\pi: p(\boldsymbol{s}) \xrightarrow{\pi_1} r'(\boldsymbol{s}'') \xrightarrow{\pi''} t\) in \(\mathcal{T}_j\). By applying 2 to \(S\) and \(p(\boldsymbol{s}) \xrightarrow{*} r'(\boldsymbol{s}'')\), we may assume that \(\left\Vert{\boldsymbol{s}}\right\Vert\) and \(|\pi_1|\) are bounded by \[\begin{align} \left\Vert{\boldsymbol{s}}\right\Vert,|\pi_1| &\leq L(\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V_j',\boldsymbol{s}''), \mathop{\operatorname{\mathrm{\mathrm{\small norm}}}}\nolimits(S))\\ &\leq L(\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V_j')+f_{j+1}(C\cdot H(\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V_j'), \mathop{\operatorname{\mathrm{\mathrm{\small norm}}}}\nolimits(S))^2). \end{align}\] Therefore, \(|\pi| = |\pi_1| + |\pi''| \le 2L(\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V_j')+f_{j+1}(C\cdot H(\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V_j'), \mathop{\operatorname{\mathrm{\mathrm{\small norm}}}}\nolimits(S))^2) = f_j(\mathop{\operatorname{\mathrm{\mathrm{\small norm}}}}\nolimits(S))\). ◻

Proof of [prop:len-par-pump-3-vass]. Let \((V, s, t) \in \rm{Pump}\mathbb{VASS}^3\) be a \(k\)-component 3-VASS. By [prop:2-exp-lcr-for-par-pump-3-vass] and [lem:2-exp-preserve-via-reduction], it holds that \(\min \mathop{\operatorname{\mathrm{\mathrm{\small len}}}}\nolimits(V,s,t) \le \mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V, s, t)^{2^{\mathop{\operatorname{\mathrm{poly}}}\nolimits({k})}}\). ◻

Proof of [prop:prog-pump-to-diag-pump]. Assume that \(V=(Q,T)\) and let \(M:=\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V,s)\). Note that \(M > 1\). By [lem:prog-pump-or-bounded-in-par-3-vass], we obtain a partition of \(\pi\) in the form of \[s = c_1 \xrightarrow{\pi_1} c_2 \xrightarrow{\pi_2} c_3 \xrightarrow{\pi_3} t\] with \(|\mathop{\operatorname{\mathrm{\mathrm{\small bd}}}}\nolimits(\pi_1, B)| \ge 2\) and \(|\mathop{\operatorname{\mathrm{\mathrm{\small bd}}}}\nolimits(\pi_1\pi_2, B)| \ge 1\) for some \(B = {\mathop{\operatorname{\mathrm{poly}}}\nolimits({M})}^k\). We assume that \(B \le M^{m\cdot k}\) for some \(m \ge 1\) and let the polynomials given in [lem:one-turn-approx] be bounded by \(F(x):=x^{m}\). There are two cases.

Case 1. \(\pi_3 = \varepsilon\).

Then \(\mathop{\operatorname{\mathrm{\mathrm{\small bd}}}}\nolimits(\pi, B) \neq \emptyset\). Suppose \(s=p(\boldsymbol{x})\) and let \(c = q(\boldsymbol{y}) :=t\). Applying [lem:one-turn-approx] to the trivial hybrid set \(\{\boldsymbol{x}\}\), one obtains a hybrid set \(S\) such that \(\boldsymbol{y} \in S \subseteq \mathop{\operatorname{\mathrm{Reach}}}\nolimits_{q}({V},{s})\) and \[\mathop{\operatorname{\mathrm{\mathrm{\small norm}}}}\nolimits(S) \le F(B + M) \le \left(M^{mk} + M\right)^m \le M ^{2m^2k}.\] Moreover, for each \(\boldsymbol{z} \in S\), one has that \(s \xrightarrow{\rho} q(\boldsymbol{z})\) in \(V\) with \(|\rho| \le F(B+M+\left\Vert{\boldsymbol{z}}\right\Vert)\), which implies that \(\boldsymbol{z} \in \mathop{\operatorname{\mathrm{Reach}}}\nolimits_{q}({V},{s})\) and \[\min \mathop{\operatorname{\mathrm{\mathrm{\small len}}}}\nolimits(V,s,q(\boldsymbol{z})) \le F(B+ \mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V,s,q(\boldsymbol{z}))) \le \mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V,s,q(\boldsymbol{z})) ^{2m^2k}.\] This justifies the first case.

Case 2. \(\pi_3 \ne\varepsilon\).

Then by [lem:prog-pump-or-bounded-in-par-3-vass], there exist jointly diagonal cycles \(\theta_1\), \(\theta_2\), \(\theta_3\) of length bounded by \(B\), enabled along \(\pi\), witnessed by configurations \(c_1\), \(c_2\), and \(c_3\). Assume that \(c_2=r(\boldsymbol{w})\) and \(c_3=p(\boldsymbol{v})\). For the first segment, we assume, w.l.o.g., that \(\Delta(\theta_1)(1) > 0\) and \(\{2,3\} \subseteq \mathop{\operatorname{\mathrm{\mathrm{\small bd}}}}\nolimits(\pi_1, B)\). Using again [lem:one-turn-approx], we get some hybrid set \(S_r = \boldsymbol{b}_r + {P_r}^{\langle {{\boldsymbol{c}_r}, \cdot} \rangle \le {K_r}}\) with \(\mathop{\operatorname{\mathrm{\mathrm{\small norm}}}}\nolimits(S_r) \le M ^{2m^2k}\) such that

• \(\boldsymbol{w} \in S_r\) and \(\boldsymbol{z}(\iota) = \boldsymbol{w}(\iota)\) for all \(\boldsymbol{z} \in S_r\) and all \(\iota \in \{2,3\}\), and

• for each \(\boldsymbol{z} \in S_r\), there is a run \(s\xrightarrow{\rho} r(\boldsymbol{z})\) in \(V\) such that \(|\rho| \le \mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V,s,q(\boldsymbol{z}))^{2m^2k}.\)

Now consider the second cycle \(\theta_2\). Let \(\lambda := BM + 1\) and \[\boldsymbol{a} := \lambda \cdot \mathop{\operatorname{\mathrm{\mathrm{\small eff}}}}\nolimits(\theta_1) + \mathop{\operatorname{\mathrm{\mathrm{\small eff}}}}\nolimits(\theta_2).\] Since \(|\theta_2| \le B\), we have \(\boldsymbol{a} \ge \boldsymbol{0}\) and \(\boldsymbol{a}(\iota) > 0\) holds for every \(\iota \in [3]\) such that \(\mathop{\operatorname{\mathrm{\mathrm{\small eff}}}}\nolimits(\theta_1)(\iota) > 0\) or \(\mathop{\operatorname{\mathrm{\mathrm{\small eff}}}}\nolimits(\theta_2)(\iota) > 0\). Let \(S_r' := S_r+\{\boldsymbol{a}\}^* = \boldsymbol{b}_r + {P_r}^{\langle {{\boldsymbol{c}_r}, \cdot} \rangle \le {K_r}} + \{\boldsymbol{a}\}^*\). Notice that \(\left\Vert{\boldsymbol{a}}\right\Vert \le (\lambda+1)\cdot BM \le M^{2mk+3}\). Consequently \[\mathop{\operatorname{\mathrm{\mathrm{\small norm}}}}\nolimits(S_r') \le M^{2m^2k} + \left\Vert{\boldsymbol{a}}\right\Vert \le M^{6m^2k}.\]

claimclaimLenFirstRoundApprox \(\boldsymbol{w}\in S_r'\subseteq \mathop{\operatorname{\mathrm{Reach}}}\nolimits_{r}({V},{s})\) and \(\min \mathop{\operatorname{\mathrm{\mathrm{\small len}}}}\nolimits(V,s,r(\boldsymbol{z})) \le \mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V,s,r(\boldsymbol{z}))^{6m^2k}\) holds for each \(\boldsymbol{z}\in S_r'\).

If \(\boldsymbol{a} \ge \boldsymbol{1}\), we can finish the proof by taking \(c:=r(\boldsymbol{w})\). Otherwise, we continue with the second segment \(r(\boldsymbol{w})\xrightarrow{\pi_2} p(\boldsymbol{v})\), which satisfies \(|\mathop{\operatorname{\mathrm{\mathrm{\small bd}}}}\nolimits(\pi_2, B)| \ge 1\). Since \(\mathop{\operatorname{\mathrm{\mathrm{\small eff}}}}\nolimits(\theta_1)(1) > 0\), we assume w.l.o.g. that \(\boldsymbol{a}(3) = 0\), which implies that \(3 \in \mathop{\operatorname{\mathrm{\mathrm{\small bd}}}}\nolimits(\pi_1\pi_2, B)\) by [lem:prog-pump-or-bounded-in-par-3-vass]. For the hybrid set \(S_r'\), all elements in \(S_r'\) have \(\boldsymbol{w}(3)\) on their third entries. Applying [lem:one-turn-approx], there exists a hybrid set \(S_p = \boldsymbol{b}_p + {P_p}^{\langle {{\boldsymbol{c}_p}, \cdot} \rangle \le {K_p}}\) with \[\mathop{\operatorname{\mathrm{\mathrm{\small norm}}}}\nolimits(S_p) \le F(B+M+\mathop{\operatorname{\mathrm{\mathrm{\small norm}}}}\nolimits(S_r')) \le \left(3 \cdot M^{6m^2k}\right)^m \le M^{8m^3k}.\] Moreover, it renders true that

• \(\boldsymbol{v} \in S_p\) and \(\boldsymbol{z}(3) = \boldsymbol{v}(3)\) holds for all \(\boldsymbol{z} \in S_p\), and

• for each \(\boldsymbol{v}' \in S_p\), there exists some \(\boldsymbol{w}' \in S'_r\) with a run \(r(\boldsymbol{w}')\xrightarrow{\rho} p(\boldsymbol{v}')\) in \(V\) such that \[\label{eq:norm-w39-len-rho} \left\Vert{\boldsymbol{w}'}\right\Vert, |\rho| \le F(B+M+\mathop{\operatorname{\mathrm{\mathrm{\small norm}}}}\nolimits(S_r') + \left\Vert{\boldsymbol{v}'}\right\Vert) \le \mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V,s,p(\boldsymbol{v}'))^{8m^3k}.\tag{5}\]

Consider the last cycle \(\theta_3\). Recall that \(\lambda = BM + 1\). Let \(\boldsymbol{p} := \lambda \cdot \boldsymbol{a} + \mathop{\operatorname{\mathrm{\mathrm{\small eff}}}}\nolimits(\theta_3)\). Clearly \(\boldsymbol{p} \ge \boldsymbol{1}\). Let \(S_p' := \boldsymbol{b}_p + {P_p}^{\langle {{\boldsymbol{c}_p}, \cdot} \rangle \le {K_p}} + \{\boldsymbol{p}\}^*\). Then \(\mathop{\operatorname{\mathrm{\mathrm{\small norm}}}}\nolimits(S_p') \le \mathop{\operatorname{\mathrm{\mathrm{\small norm}}}}\nolimits(S_p) + \left\Vert{\boldsymbol{p}}\right\Vert \le 2\cdot M^{8m^3k} \le M^{9m^3k}\). Let \(c := p(\boldsymbol{v})\) and \(S := S_p'\). The following claim justifies the second case.

claimclaimSecondRoundApprox \(\boldsymbol{v} \in S_p' \subseteq \mathop{\operatorname{\mathrm{Reach}}}\nolimits_{p}({V},{s})\) and \(\min \mathop{\operatorname{\mathrm{\mathrm{\small len}}}}\nolimits(V, s, p(\boldsymbol{z})) \le \mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V,s,p(\boldsymbol{z}))^{68m^5k^2}\) for all \(\boldsymbol{z} \in S_p'\).

The polynomial \(x^{68m^5}\) subsumes all the upper-bound polynomials mentioned in the proof. ◻

Proof of [prop:2-exp-lcr-for-par-pump-3-vass]. We define a family of functions \((L_k)_{k \in \mathbb{N}}\) by letting \(L_k(x) := x^{2^{f(k)}}\) for all \(k \in \mathbb{N}\), where \(f\) is the polynomial given in [prop:diagonal-case-lenbound]. We then show that \(\rm{Semi\text{-}diag}\mathbb{VASS}^3\) is \((L_k)_{k \in \mathbb{N}}\)-controlled self-reducible. Let \(g\) be the maximum of the two polynomials appearing in [prop:prog-pump-to-diag-pump]. Assume that \(m \ge 1\) is such that \(g(x) \le x^m\) for all \(x >1\). Let \(R(x) := x^{21mk^2}\).

For every \(k \ge 1\) and every \(k\)-component VASS \((V,s,t)\in \rm{Semi\text{-}diag}\mathbb{VASS}^3\) with size \(M:=\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V,s,t)\), we assume that \(s \xrightarrow{\pi} t\) in \(V\) for some run \(\pi\). In the case where \((V,s,t)\) is diagonal, \(\min\mathop{\operatorname{\mathrm{\mathrm{\small len}}}}\nolimits(V,s,t) \le L_k(M)\) by [prop:diagonal-case-lenbound]. Then \((V,s,t)\) is reduced to a \(0\)-component 3-VASS \((V',s',t')\) where \(V'\) contains a single state \(q\) and a single self-loop \((q,\boldsymbol{1}, q)\), \(s'=q(\boldsymbol{0})\) and \(t'=q(L_k(M)\cdot\boldsymbol{1})\).

Suppose \(s\) is not diagonal in \(V\). By [prop:prog-pump-to-diag-pump], there exist a configuration \(c = q(\boldsymbol{y})\) on \(\pi\) and a hybrid set \(S = \boldsymbol{b} + {P_1}^{\langle {{\boldsymbol{c}}, \cdot} \rangle \le {K}} + P_0^*\) such that \(\boldsymbol{y} \in S \subseteq \mathop{\operatorname{\mathrm{Reach}}}\nolimits_{q}({V},{s})\) and the following is valid. \[\label{eq:2-exp-lcr-for-par-pump-3-vass-1} \mathop{\operatorname{\mathrm{\mathrm{\small norm}}}}\nolimits(S) \le g(M)^{k^2} \text{ and } \min \mathop{\operatorname{\mathrm{\mathrm{\small len}}}}\nolimits(V, s, q(\boldsymbol{z})) \le g(\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V,s,q(\boldsymbol{z})))^{k^2} \text{ for all } \boldsymbol{z} \in S.\tag{6}\] Moreover \(q(\boldsymbol{y}) = t\) whenever \(P_0 \cap \mathbb{Q}_{>0}^3 = \emptyset\). There are two cases.

Case 1. \(P_0 \cap \mathbb{Q}_{>0}^3 = \emptyset\).

Then \(c = t\), and \(\min \mathop{\operatorname{\mathrm{\mathrm{\small len}}}}\nolimits(V, s, t) \le g(M)^{k^2}\le R(M)\). We are done.

Case 2. \(P_0 \cap \mathbb{Q}_{>0}^3 \neq \emptyset\).

There exists some \(\boldsymbol{\delta} \in P_0\) with \(\boldsymbol{\delta}\ge \boldsymbol{1}\). Assume that \(P_1\) can be enumerated as \(\boldsymbol{p}_1,\dots, \boldsymbol{p}_n\), \(V = (V_1)u_1\dots u_{k-1}(V_k)\) and \(q\) belongs to \(V_\iota\). We claim that \(\iota>1\). Otherwise, there would be a simple path from \(q\) to \(p\). Note that \(\boldsymbol{b} + \{\boldsymbol{\delta}\}^* \subseteq \mathop{\operatorname{\mathrm{Reach}}}\nolimits_{q}({V},{s})\). We have \(s\xrightarrow{*} q(\boldsymbol{z})\), where \(\boldsymbol{z}:=\boldsymbol{b} + (|\sigma| \cdot \mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V) + 1) \cdot \boldsymbol{\delta} \ge \mathop{\operatorname{\mathrm{\mathrm{\small drop}}}}\nolimits(\sigma)\). Hence, \(s \xrightarrow{*} q(\boldsymbol{z}) \xrightarrow{\sigma}p(\boldsymbol{z} + \mathop{\operatorname{\mathrm{\mathrm{\small eff}}}}\nolimits(\sigma))\) and \(\boldsymbol{z} + \mathop{\operatorname{\mathrm{\mathrm{\small eff}}}}\nolimits(\sigma) \ge \boldsymbol{\delta}\ge \boldsymbol{1}\). This implies that \(s\) is diagonal, which is a contradiction. Now construct a VASS \(V_{S}\) from \((V_\iota)u_{\iota}\dots u_{k-1}(V_k)\) by adding a transition set \(T_S\), where \[T_S := \{(q,\boldsymbol{a},q)\mid \boldsymbol{a} \in P_1 \cup P_0\}.\] Notice that \(V_S\) has at most \(k - 1\) components, and \(q(\boldsymbol{b}) \xrightarrow{*} q(\boldsymbol{y}) \xrightarrow{*} t\) in \(V_S\). The size bound can be derived as follows. \[\label{eq:2-exp-lcr-for-par-pump-3-vass-2} \begin{align} \mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V_S, q(\boldsymbol{b}),t) &\le M + 3\cdot\left\Vert{\boldsymbol{b}}\right\Vert + 3 \cdot(|T| + |T_S|) \cdot (\left\Vert{T}\right\Vert + \left\Vert{T_S}\right\Vert + 1)\\ &\le M + 3\cdot M^{mk^2} + 3 \cdot(M + (M^{mk^2} + 1)^3) \cdot(M+M^{mk^2} + 1)\\ &\le M + 3\cdot M^{mk^2} + 81 \cdot M^{4mk^2}\\ &\le 85\cdot M^{4mk^2}. \end{align}\tag{7}\] Moreover, \((V_S, q(\boldsymbol{b}),t)\) is diagonal as \((V,s,t)\) is backward diagonal and \(q(\boldsymbol{b}) \xrightarrow{*} q(\boldsymbol{b} + \boldsymbol{\delta})\). Let \(\ell := \min\mathop{\operatorname{\mathrm{\mathrm{\small len}}}}\nolimits(V_S, q(\boldsymbol{b}), t)\). We now invoke a result about the diagonal \(3\)-VASS. By [prop:diagonal-case-lenbound], \[\ell \le L_k(85\cdot M^{4mk^2}) \le M^{(4mk^2+7)\cdot 2^{f(k)}} = L_k(M)^{11mk^2}.\]

Case I. \(\left\Vert{\boldsymbol{c}}\right\Vert\cdot \ell \le K\).

The following claim implies that the construction from \((V,s,t)\) to the diagonal VASS \((V',s',t') := (V_S, q(\boldsymbol{b}), t)\) is doubly-exponentially self-reducible.

claimClaimSemiDiagSecond The diagonal \((V',s',t')\) has at most \(k-1\) components, \(s'\xrightarrow{*}t'\) in \(V'\), \(\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V',s',t') \le R(L_k(M))\), and \(\min\mathop{\operatorname{\mathrm{\mathrm{\small len}}}}\nolimits(V,s,t) \le R(\min\mathop{\operatorname{\mathrm{\mathrm{\small len}}}}\nolimits(V',s',t')+M)\).

Case II. \(K < \left\Vert{\boldsymbol{c}}\right\Vert \cdot \ell\).

We have \(K < \left\Vert{\boldsymbol{c}}\right\Vert \cdot \ell \le g(M)^{k^2}\cdot L_k(M)^{11mk^2} \le L_k(M)^{12mk^2}\). Since \(\boldsymbol{y} \in S\), we can write it as \(\boldsymbol{y} = \boldsymbol{w} + \boldsymbol{q}\), where \(\boldsymbol{q} \in P_0^*\) and \(\boldsymbol{w} = \boldsymbol{b} + \sum_{i=1}^n \boldsymbol{\lambda}(i)\cdot \boldsymbol{p}_i\) for some \(\boldsymbol{\lambda} \in \mathbb{N}^n\) satisfying \(\langle {\boldsymbol{c}, \boldsymbol{\lambda}} \rangle \le K\). We may assume that \(\boldsymbol{c} \ge \boldsymbol{1}\), since each \(\boldsymbol{p}_i\) correspond to \(\boldsymbol{c}(i) = 0\) can be removed and inserted into \(P_0\). Then \[\left\Vert{\boldsymbol{w}}\right\Vert \le \left\Vert{\boldsymbol{b}}\right\Vert + \langle {\boldsymbol{1}, \boldsymbol{\lambda}} \rangle\cdot \left\Vert{P}\right\Vert \le 2g(M)^{k^2} \cdot \langle {\boldsymbol{c}, \boldsymbol{\lambda}} \rangle \le 2M^{mk^2} \cdot K \le L_k(M)^{14mk^2}.\] We define a diagonal \((k{-}1)\)-component VASS \((V',s',t')\) from \((V_\iota)u_{\iota}\dots u_{k-1}(V_k)\) by setting \(s' := q(\boldsymbol{w})\text{ and }t' := t\text{ and }T':=T\cup T_{\boldsymbol{w}}\), where \(T_{\boldsymbol{w}} := \{(q,\boldsymbol{a},q)\mid \boldsymbol{a} \in P_0\}\). By the following claim, \((V',s',t')\) satisfies all the required properties.

claimClaimSemiDiagThrid The diagonal \((k{-}1)\)-component \((V',s',t')\) renders true that \(s'\xrightarrow{*}t'\) in \(V'\), \(\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V',s',t') \le R(L_k(M))\) and \(\min\mathop{\operatorname{\mathrm{\mathrm{\small len}}}}\nolimits(V,s,t) \le R(\min\mathop{\operatorname{\mathrm{\mathrm{\small len}}}}\nolimits(V',s',t')+M)\).

We conclude that \(\rm{Semi\text{-}diag}\mathbb{VASS}^3\) is \((L_k)_{k \in \mathbb{N}}\)-controlled self-reducible. By [lem:2-exp-preserve-via-reduction], it admits \((G_k)_{k \in \mathbb{N}}\)-short runs, where \(G_k(x) = x^{2^{\mathcal{O}({f(k)})k}}\). By the same token, we can show that \(\rm{Pump}\mathbb{VASS}^3\) is doubly-exponentially self-reducible and admits doubly-exponentially short runs. ◻

Proof of [prop:3-VASS-lenbound-intro]. Let \((V, s, t)\) be a \(k\)-component 3-VASS with \(s \xrightarrow{*} t\) in \(V\). By [prop:2-exp-lcr-for-gen-3-vass] and [lem:2-exp-preserve-via-reduction], it holds that \(\min \mathop{\operatorname{\mathrm{\mathrm{\small len}}}}\nolimits(V,s,t) \le \mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V, s, t)^{2^{\mathop{\operatorname{\mathrm{poly}}}\nolimits({k})}}\). ◻

Proof of [prop:2-exp-lcr-for-gen-3-vass]. Define a family of functions \((L_k)_{k \in \mathbb{N}}\) by letting \(L_k(x) := x^{2^{f(k)}}\) for each \(k \in \mathbb{N}\), where \(f\) is the polynomial given in [prop:len-par-pump-3-vass]. We show that \(\rm{Semi\text{-}pump}\mathbb{VASS}^3\) is \((L_k)_{k \in \mathbb{N}}\)-controlled self-reducible. Let \(g\) be the maximum of the two polynomials appearing in [lem:one-turn-approx]. Assume that \(g(x) \le x^m\) holds for some \(m \ge 1\) and all \(x >1\). Let \(R(x) := x^{30\cdot m^2}\).

Suppose \((V,s,t)\in \rm{Semi\text{-}pump}\mathbb{VASS}^3\), where \(V=(V_1)u_1\dots u_{k-1}(V_k)\) and \(t = q(\boldsymbol{y})\). Let \(M:=\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V,s,t)\). Suppose \(s\) is not pumpable in \(V\), and \[s \xrightarrow{\pi_1} q_1(\boldsymbol{y}_1) \xrightarrow{u_1} p_2(\boldsymbol{x}_2) \xrightarrow{\pi'} t,\] where \(\pi'\) is a run in \((V_2)u_2\dots u_{k-1}(V_k)\). By [cor:diag-pump-of-unbounded], the index set of bounded coordinates along \(\pi_1\) is non-empty, i.e., \(\mathop{\operatorname{\mathrm{\mathrm{\small bd}}}}\nolimits(\pi_1, B) \neq \emptyset\), where \(B = {\mathop{\operatorname{\mathrm{poly}}}\nolimits({\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V,s)})}\). We may as well assume that \(B \le \mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V,s)^m \le M^m\) for the \(m\) introduced in the above. Thus \(I:=\mathop{\operatorname{\mathrm{\mathrm{\small bd}}}}\nolimits(\pi_1u_1, B') \supseteq \mathop{\operatorname{\mathrm{\mathrm{\small bd}}}}\nolimits(\pi_1, B) \neq \emptyset\), where \(B' := B+M\). By applying [lem:one-turn-approx] to \((V,s,p_2(\boldsymbol{x}_2))\) and \(I\), one can obtain a hybrid set \(S = \boldsymbol{b} + {P_1}^{\langle {{\boldsymbol{c}}, \cdot} \rangle \le {K}}+P_0^*\) rendering true \(\boldsymbol{x}_2 \in S \subseteq \mathop{\operatorname{\mathrm{Reach}}}\nolimits_{p_2}({V},{s})\) and the following inequalities. \[\label{eq:2-exp-lcr-for-gen-3-vass-1} \begin{align} \mathop{\operatorname{\mathrm{\mathrm{\small norm}}}}\nolimits(S) &\le g(B'+M) \le M^{3m^2},\\ \min \mathop{\operatorname{\mathrm{\mathrm{\small len}}}}\nolimits(V, s, p_2(\boldsymbol{z})) &\le g(B'+\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V,s,p_2(\boldsymbol{z}))) \le \mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V,s,p_2(\boldsymbol{z}))^{3m^2}\;\text{for all}\;\boldsymbol{z} \in S. \end{align}\tag{8}\] We may assume that \(\boldsymbol{c}\ge \boldsymbol{1}\) if \(P_1 \neq \emptyset\). We now construct a \((k-1)\)-component VASS \((V_{S}, s_S,t)\) by removing the first SCC and turning the periods in \(P_1\cup P_0\) into self-loops at the first state \(p_2\) of \((V_2)u_2\dots u_{k-1}(V_k)\). Let \(T_{tail}\) be the transition set of \((V_2)u_2\dots u_{k-1}(V_k)\) and \(Q_{tail}\) be the state set of \((V_2)u_2\dots u_{k-1}(V_k)\). The new 3-VASS instance \((V_{S}, s_S,t)=((Q_S,T_S),s_S,t)\) is given by \[s_S := p_2(\boldsymbol{b}) \text{ and } Q_S=Q_{tail} \text{ and } T_S := T_{tail}\cup \{(p_2,\boldsymbol{a},p_2)\mid \boldsymbol{a} \in P_1 \cup P_0\}.\] Observe that \(s_S \xrightarrow{*}p_2(\boldsymbol{x}_2) \xrightarrow{\pi'} t\) in \(V_S\) and \[\label{eq:2-exp-lcr-for-gen-3-vass-2} \begin{align} \mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V_S, s_S, t) &\le M + 3 \cdot \left\Vert{\boldsymbol{b}}\right\Vert + 3\cdot (M + |T_S|) \cdot (M + \left\Vert{T_S}\right\Vert + 1)\\ &\le M + 3\cdot M^{3m^2} + 3 \cdot (M + (M^{3m^2} + 1)^3) \cdot (M + M^{3m^2} + 1)\\ &\le 85\cdot M^{12m^2}. \end{align}\tag{9}\] Suppose \(P_1=\{\boldsymbol{p}_1,\cdots,\boldsymbol{p}_n\}\), where the order of \(\boldsymbol{p}_1,\cdots,\boldsymbol{p}_n\) is consistent with the order of \(\boldsymbol{c}(1),\ldots,\boldsymbol{c}(n)\). Let \(\ell := \min\mathop{\operatorname{\mathrm{\mathrm{\small len}}}}\nolimits(V_S,s_S,t)\). There are two cases depending on whether \(\left\Vert{\boldsymbol{c}}\right\Vert\cdot \ell\le K\).

Case 1. \(\left\Vert{\boldsymbol{c}}\right\Vert\cdot \ell\le K\).

We let \((V',s',t'):=(V_S,s_S,t)\). It suffices to establish the following claim.

claimClaimSemiParFirst The \((k{-}1)\)-component 3-VASS \((V',s',t') \in \rm{Semi\text{-}pump}\mathbb{VASS}^3\) and renders true the inequlities: \(\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V',s',t') \le R(L_k(M))\) and \(\min\mathop{\operatorname{\mathrm{\mathrm{\small len}}}}\nolimits(V,s,t) \le R(\min\mathop{\operatorname{\mathrm{\mathrm{\small len}}}}\nolimits(V',s',t')+M)\).

Case 2. \(K < \left\Vert{\boldsymbol{c}}\right\Vert\cdot \ell\).

In this case, \(P_1 \ne \emptyset\). By construction, \((V_S,s_S,t)\) is forward pumpable since \(p_2(\boldsymbol{x}_2)\xrightarrow{*}p_2(\boldsymbol{x}_2+\boldsymbol{\delta})\) for some \(\boldsymbol{\delta} \in P_1\) and \(\boldsymbol{\delta}>\boldsymbol{0}\). So \((V_S,s_S,t)\) is pumpable. By [prop:len-par-pump-3-vass], \[\begin{align} \ell &\le L_k(85\cdot M^{12m^2}) \le L_k(M^{19m^2}) = M^{19m^2\cdot 2^{f(k)}} \le L_k(M)^{19m^2}, \text{\;and}\\ K &\le \left\Vert{\boldsymbol{c}}\right\Vert \cdot \ell \le M^{3m^2}\cdot L_k(M)^{19m^2} \le L_k(M)^{22m^2}. \end{align}\] Since \(\boldsymbol{x}_2 \in S\), we can write it as \(\boldsymbol{x}_2 = \boldsymbol{w} + \boldsymbol{q}\), where \(\boldsymbol{q} \in P_0^*\) and \(\boldsymbol{w} = \boldsymbol{b} + \sum_{i=1}^n \boldsymbol{\lambda}(i)\cdot \boldsymbol{p}_i\) for some \(\boldsymbol{\lambda} \in \mathbb{N}^n\) satisfying \(\langle {\boldsymbol{c}, \boldsymbol{\lambda}} \rangle \le K\). Hence, \[\left\Vert{\boldsymbol{w}}\right\Vert \le \left\Vert{\boldsymbol{b}}\right\Vert + \langle {\boldsymbol{1}, \boldsymbol{\lambda}} \rangle\cdot \left\Vert{P_1}\right\Vert \le 2M^{3m^2} \cdot \langle {\boldsymbol{c}, \boldsymbol{\lambda}} \rangle \le 2M^{3m^2} \cdot K \le 2L_k(M)^{25m^2}.\] We construct a VASS \(V'\) from \((V_2)u_2\dots u_{k-1}(V_k)\) by adding some self-loops to represent \(P_0\): \[T' := T_{tail}\cup\{(p_2,\boldsymbol{a},p_2)\mid \boldsymbol{a} \in P_0\}.\] Let \(s' := p_2(\boldsymbol{w})\) and \(t' := t\). We can prove the following claim for \((V',s',t')\).

claimClaimSemiParSecond The \((k{-}1)\)-component 3-VASS \((V',s',t')\in\rm{Semi\text{-}pump}\mathbb{VASS}^3\) and renders true the inequlities: \(\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V',s',t') \le R( L_k(M))\) and \(\min\mathop{\operatorname{\mathrm{\mathrm{\small len}}}}\nolimits(V,s,t) \le R(\min\mathop{\operatorname{\mathrm{\mathrm{\small len}}}}\nolimits(V',s',t')+M)\).

We conclude from [claim:semi-par-1], [claim:semi-par-2] and [lem:2-exp-preserve-via-reduction] that \(\rm{Semi\text{-}pump}\mathbb{VASS}^3\) is \((L_k)_{k \in \mathbb{N}}\)-controlled self-reducible and admits doubly-exponentially short runs. Similarly, \(\mathrm{Seq}\mathbb{VASS}^3\) is doubly-exponentially self-reducible and admits doubly-exponentially short runs. ◻

Proof. It suffices to consider the sequential 3-VASS. For each \(k \ge 1\) and every \(k\)-component 3-VASS \((V,s,t)\), if \(s\xrightarrow{*}t\) in \(V\), by [prop:3-VASS-lenbound-intro], there exists a short path \(s\xrightarrow{\pi} t\) in \(V\) with \(|\pi| \le \mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V,s,t)^{2^{{\mathop{\operatorname{\mathrm{poly}}}\nolimits({k})}}}\). The reachability \(s\xrightarrow{*}t\) is decided by inspecting all runs of length at most \(\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V,s,t)^{2^{{\mathop{\operatorname{\mathrm{poly}}}\nolimits({k})}}}\). Now \[\log|\pi| = 2^{{\mathop{\operatorname{\mathrm{poly}}}\nolimits({k})}} \cdot \log\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V,s,t) \leq 2^{{\mathop{\operatorname{\mathrm{poly}}}\nolimits({\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits_{\mathrm{\small bin}}(V,s,t)})}} \leq 2^{{\mathop{\operatorname{\mathrm{poly}}}\nolimits({\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V,s,t)})}}\] where \(\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits_{\mathrm{\small bin}}(V,s,t)\) denotes the input size under binary encoding. That is, \[\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits_{\mathrm{\small bin}}(V,s,t) = |Q| + d \cdot |T| \cdot \log (\left\Vert{T}\right\Vert + 1) + d \cdot \log (\left\Vert{s}\right\Vert + 1) + d\cdot \log (\left\Vert{t}\right\Vert + 1).\] The nondeterministic traversal algorithm can be carried out in exponential space under both binary and unary encoding schemes. Hence, \(\mathbb{VASS}^3\) is in EXPSPACE. ◻

Proof. Suppose that \(V=(Q,T)\) and \(s \xrightarrow{\rho}t\) in \(V\). We can assume that \(\rho\) contains no zero transitions. Since each transition increases at least one coordinate by at least \(1\), it is immediate that \(|\rho| \le d\cdot \left\Vert{t}\right\Vert\). ◻

Proof. Let \(L_k(x) = x^{2^{f(k)}}\). By definition of length-controlled self-reduction, there exists a polynomial \(f(x)\) satisfying the required conditions. We choose a sufficiently large \(c \ge 2\) such that \(f(x) \le x^c\) for every \(x > 1\). Then \(R(x) \le x^{ck^2}\) for each \(x > 1\). Define \[g(k) := \left(c^3\cdot (k+1)^4\cdot 2^{f(k)}\right)^{k} \le \left(c\cdot 2^{f(k)}\right)^{5k} \le 2^{\mathcal{O}(f(k))\cdot k}\] and \(G_k(x):= x^{g(k)}\) for each \(k \in \mathbb{N}\). Note that \(G_0(x)=x\). Let \((V,s,t) \in \mathcal{V}\) be a \(k\)-component VASS with \(s \xrightarrow{*} t\) for some \(\pi\) with \(M := \mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V, s, t) > 1\). We prove by induction on \(k \ge 0\). In the base case, we have \(k = 0\). By [obs:0-com-vass-len], we immediately obtain that \[\min\mathop{\operatorname{\mathrm{\mathrm{\small len}}}}\nolimits(V,s,t) \le d\cdot \left\Vert{t}\right\Vert \le M \le G_0(M).\] Then we consider the case where \(k \ge 1\). By definition, there exists a sequential VASS \((V',s',t')\) such that \(s'\xrightarrow{*}t'\) in \(V'\), \(\min\mathop{\operatorname{\mathrm{\mathrm{\small len}}}}\nolimits(V,s,t) \le R(\ell + M) \le (\ell + M)^{ck^2}\), and \[\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V',s',t')\le R(L_k(M)) \le M^{ck^2 \cdot 2^{f(k)}},\] where \(\ell := \min\mathop{\operatorname{\mathrm{\mathrm{\small len}}}}\nolimits(V',s',t')\). Since \((V',s',t') \in \mathcal{V}\) has at most \(k-1\) components, then by the induction hypothesis, we have \(\ell \le M^{ck^2 \cdot 2^{f(k)} \cdot g(k-1)}\), \(g(k-1)=\left(c^3\cdot k^4 \cdot 2^{f(k-1)}\right)^{k-1}\), and \[\min \mathop{\operatorname{\mathrm{\mathrm{\small len}}}}\nolimits(V,s,t) \le \left(M^{ck^2\cdot 2^{f(k)} \cdot g(k-1)} + M\right) ^ {ck^2} \le M^{c^3\cdot (k+1)^4 \cdot 2^{f(k)}\cdot g(k-1)}\le M^{g(k)}.\] We conclude that \(\mathcal{V}\) admits \((G_k)_{k \in \mathbb{N}}\)-short runs. ◻

Proof. It is well known that every run in \(\Lambda\) starting from a vector in \(S\) is captured by a system of linear inequalities [26]. We introduce variables \(n_1, \ldots, n_k \in \mathbb{N}\) for the number of repetitions of each loop, and \(\boldsymbol{a}_i, \boldsymbol{b}_i\) where \(i = 0, 1, \ldots, k\) for the intermediate configurations before and after the bridge \(\alpha_i\). Also, we introduce a variable \(\boldsymbol{\ell} \in \mathbb{N}^{|P|}\) to determine the source, and a variable \(\boldsymbol{r} \in \mathbb{N}^{|Q|}\) to determine the target in \(T\). The constraints are as follows, where \(P\) and \(Q\) are the matrices whose columns are vectors in \(P\) and \(Q\) respectively: \[\begin{align} \begin{cases} \boldsymbol{b} + P \cdot \boldsymbol{\ell} & = \boldsymbol{a}_0 \\ \boldsymbol{d} + Q \cdot \boldsymbol{r} &= \boldsymbol{b}_k \\ \boldsymbol{a}_i & \ge \mathop{\operatorname{\mathrm{\mathrm{\small drop}}}}\nolimits(\alpha_i) \qquad i = 0, 1, 2, \ldots, k\\ \boldsymbol{a}_i + \mathop{\operatorname{\mathrm{\mathrm{\small eff}}}}\nolimits(\alpha_i) & = \boldsymbol{b}_i \qquad i = 0, 1, 2, \ldots, k\\ \boldsymbol{b}_{i-1} + \beta_i \cdot n_i & = \boldsymbol{a}_{i} \qquad i = 1, 2, \ldots, k \end{cases} \end{align}\] Observe that the non-negative solutions of this system are in one-to-one correspondence with runs from \(\boldsymbol{a}_0 = \boldsymbol{b} + P \boldsymbol{\ell}\) to \(\boldsymbol{b}_k = \boldsymbol{d} + Q\boldsymbol{r}\): the variables \(\boldsymbol{a}_i\) and \(\boldsymbol{b}_i\) record the configurations immediately before and after the bridge \(\alpha_i\), respectively. Let \(\mathcal{E}\) be the above system, and \(\mathcal{E}_0\) be its homogeneous version. For a solution \(\boldsymbol{h}\) of \(\mathcal{E}\), we write for example \(\boldsymbol{\ell}^{\boldsymbol{h}}\) for the value assigned to \(\boldsymbol{\ell}\) by \(\boldsymbol{h}\). In the following, we also refer to the variable \(\boldsymbol{b}_k\) by the name \(\boldsymbol{t}\) as it is the target of the whole run. Now we have \[\{\boldsymbol{t}^{\boldsymbol{h}} \mid \boldsymbol{h} \text{ is a solution to } \mathcal{E}\} = \mathop{\operatorname{\mathrm{Reach}}}\nolimits({\Lambda},{\boldsymbol{b} + P^*}) \cap T.\] The number of constraints of \(\mathcal{E}\) is \(m = 4 + (3k + 2) \times 2 = \mathcal{O}(k)\), and the number of variables is \(n = |P| + |Q| + k + 2 \times (k+1) \times 2 = |P| + |Q| + \mathcal{O}(k)\). Notice that \(|P| \le (\left\Vert{P}\right\Vert + 1)^2\) and \(|Q| \le (\left\Vert{P}\right\Vert + 1)^2\), so we have \(n \le {\mathop{\operatorname{\mathrm{poly}}}\nolimits({\left\Vert{P}\right\Vert, \left\Vert{Q}\right\Vert, \mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(\Lambda)})}\). Also, the norm of coefficients of \(\mathcal{E}\) is bounded by \(A := \left\Vert{\Lambda}\right\Vert + \left\Vert{P}\right\Vert + \left\Vert{Q}\right\Vert\) and the norm of constant terms of \(\mathcal{E}\) is bounded by \(C := \left\Vert{\boldsymbol{b}}\right\Vert + \left\Vert{\boldsymbol{d}}\right\Vert + \mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(\Lambda)\). Towards applying 1, define \[\begin{align} M & := ((m + n + 1) A + C + 1)^m = {\mathop{\operatorname{\mathrm{poly}}}\nolimits({\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(\Lambda), \mathop{\operatorname{\mathrm{\mathrm{\small norm}}}}\nolimits(S), \mathop{\operatorname{\mathrm{\mathrm{\small norm}}}}\nolimits(T)})}^k;\\ M_0 & := ((m + n) A + 1)^m \le {\mathop{\operatorname{\mathrm{poly}}}\nolimits({\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits{\Lambda}, \mathop{\operatorname{\mathrm{\mathrm{\small norm}}}}\nolimits(S), \mathop{\operatorname{\mathrm{\mathrm{\small norm}}}}\nolimits(T)})}^k. \end{align}\] Denote by \(X\) the solutions to \(\mathcal{E}\) and by \(X_0\) the solutions to \(\mathcal{E}_0\). Also let \(\overline{X} = \{\boldsymbol{h} \in X \mid \left\Vert{\boldsymbol{h}}\right\Vert \le M\}\) and \(\overline{X}_0 = \{\boldsymbol{h}_0 \in X_0 \mid \left\Vert{\boldsymbol{h}_0}\right\Vert \le M_0\}\). We have \(X = \overline{X} + (\overline{X}_0)^*\) by 1.

Next, let \[\begin{align} \overline{Y} := \{ \boldsymbol{h} \in \overline{X} \mid \langle {\boldsymbol{c}, \boldsymbol{\ell}^{\boldsymbol{h}}} \rangle \le K \}. \end{align}\] Also, enumerate \(\overline{X}_0\) as \(\{\boldsymbol{g}_1, \ldots, \boldsymbol{g}_h\}\). We define \[\begin{align} P' := \{ \boldsymbol{t}^{\boldsymbol{g}_i} \mid i = 1, \ldots, h \}, \quad \boldsymbol{c}' := (\langle {\boldsymbol{c}, \boldsymbol{\ell}^{\boldsymbol{g}_1}} \rangle, \dots, \langle {\boldsymbol{c}, \boldsymbol{\ell}^{\boldsymbol{g}_h}} \rangle). \end{align}\] It is routine to check that \[\begin{align} \label{eq:reach-const-short} \bigcup_{\boldsymbol{h} \in \overline{Y}} \boldsymbol{t}^{\boldsymbol{h}} + {P'}^{\langle {{\boldsymbol{c}'}, \cdot} \rangle \le {K - \langle {\boldsymbol{c}, \boldsymbol{\ell}^{\boldsymbol{h}}} \rangle}} = \mathop{\operatorname{\mathrm{Reach}}}\nolimits({\Lambda},{S}) \cap T. \end{align}\tag{11}\] We are left to bound the norm of the left-hand side. Notice that \[\begin{align} \left\Vert{\boldsymbol{t}^{\boldsymbol{h}}}\right\Vert &\le \left\Vert{\overline{Y}}\right\Vert \le \left\Vert{\overline{X}}\right\Vert \le M \le {\mathop{\operatorname{\mathrm{poly}}}\nolimits({\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(\Lambda), \mathop{\operatorname{\mathrm{\mathrm{\small norm}}}}\nolimits(S), \mathop{\operatorname{\mathrm{\mathrm{\small norm}}}}\nolimits(T)})}^k;\\ \left\Vert{P'}\right\Vert & \le \left\Vert{\overline{X_0}}\right\Vert \le M_0 \le {\mathop{\operatorname{\mathrm{poly}}}\nolimits({\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(\Lambda), \mathop{\operatorname{\mathrm{\mathrm{\small norm}}}}\nolimits(S), \mathop{\operatorname{\mathrm{\mathrm{\small norm}}}}\nolimits(T)})}^k;\\ \left\Vert{\boldsymbol{c}'}\right\Vert &\le \max_{i \in [h]}|\langle {\boldsymbol{c}, \boldsymbol{\ell}^{\boldsymbol{g}_i}} \rangle| \le 3 \left\Vert{\boldsymbol{c}}\right\Vert M_0 \le {\mathop{\operatorname{\mathrm{poly}}}\nolimits({\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(\Lambda), \mathop{\operatorname{\mathrm{\mathrm{\small norm}}}}\nolimits(S), \mathop{\operatorname{\mathrm{\mathrm{\small norm}}}}\nolimits(T)})}^k. \end{align}\] Hence, we deduce that the norm of each resulting hybrid set in 11 is also bounded by \({\mathop{\operatorname{\mathrm{poly}}}\nolimits({\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(\Lambda), \mathop{\operatorname{\mathrm{\mathrm{\small norm}}}}\nolimits(S), \mathop{\operatorname{\mathrm{\mathrm{\small norm}}}}\nolimits(T)})}^k\). ◻

Proof of 11. Let \(T := (x, 0) + \{(0, 1)\}^*\) be the target set we are considering. Applying 12 to \(\Lambda\) where the number of loops is \(k \le 3\), we represent \(\mathop{\operatorname{\mathrm{Reach}}}\nolimits({\Lambda},{S}) \cap T\) as a finite union of hybrid sets \(S' = \boldsymbol{b}' + {P'}^{\langle {{\boldsymbol{c'}}, \cdot} \rangle \le {K'}}\), where \(\mathop{\operatorname{\mathrm{\mathrm{\small norm}}}}\nolimits(S') \le {\mathop{\operatorname{\mathrm{poly}}}\nolimits({\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(\Lambda), \mathop{\operatorname{\mathrm{\mathrm{\small norm}}}}\nolimits(S), B})}\). Since \(S' \subseteq T\), we must have \(\boldsymbol{b}' = (x, a_0)\) for some \(a_0 \in \mathbb{N}\), and \(P' \subseteq \{(0, 1)\}^*\). Let \(P'' = \{y \mid (0, y) \in P'\}\), the set \[\{\boldsymbol{t}(2) \mid \boldsymbol{s} \xrightarrow{\Lambda} \boldsymbol{t}, \boldsymbol{s} \in \boldsymbol{b} + {P}^{\langle {{\boldsymbol{c}}, \cdot} \rangle \le {K}} , \boldsymbol{t}(1) = x\}\] is a finite union of hybrid sets \(a_0 + {P''}^{\langle {{\boldsymbol{c'}}, \cdot} \rangle \le {K'}}\). It remains to represent these hybrid sets as a finite union of arithmetic sets.

Now the one-dimensional hybrid set \(a_0 + {P''}^{\langle {{\boldsymbol{c}'}, \cdot} \rangle \le {K'}}\) can be represented as a finite union of \((a, p, K)\)-arithmetic sets with \[\begin{align} a &\le a_0 + |P''| \left\Vert{P''}\right\Vert^2 \le \left\Vert{\boldsymbol{b}'}\right\Vert + |P'| \left\Vert{P'}\right\Vert^2 \le {\mathop{\operatorname{\mathrm{poly}}}\nolimits({\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(\Lambda), \mathop{\operatorname{\mathrm{\mathrm{\small norm}}}}\nolimits(S), B})},\\ p & \le \left\Vert{P'}\right\Vert \le {\mathop{\operatorname{\mathrm{poly}}}\nolimits({\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(\Lambda), \mathop{\operatorname{\mathrm{\mathrm{\small norm}}}}\nolimits(S), B})}. \end{align}\] The proof of 11 is completed. ◻

Proof of 13. By 3, every run in \(\Lambda\) can be represented by a detailing \(\Lambda' = \Lambda_1\Lambda_2\Lambda_3\) where \(\Lambda_1\) and \(\Lambda_3\) are short, \(\Lambda_2\) is zigzagging, and \(\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(\Lambda') \le {\mathop{\operatorname{\mathrm{poly}}}\nolimits({\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(\Lambda)})}\). If \(\Lambda_2\) is empty, then we are done by applying 12 to \(\Lambda_1\Lambda_3\) with target set \(T := \mathbb{N}^2\). Otherwise, assume \(\Lambda_2\) is nonempty. Any run starting from \(\boldsymbol{x}\) is then captured by a run in the form of \[\begin{align} \boldsymbol{x} \xrightarrow{\Lambda_1} \boldsymbol{u} {\mathop{\;\raisebox{-0.17em}{\searrow}\kern-0.88em\raisebox{0.17em}{\nwarrow}}}^{\Lambda_2}_{B} \boldsymbol{v} \xrightarrow{\Lambda_3} \boldsymbol{y} \end{align}\] where \(B \le {\mathop{\operatorname{\mathrm{poly}}}\nolimits({\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(\Lambda)})}\) and \(\boldsymbol{u}, \boldsymbol{v} \in [0, B] \times \mathbb{N}\).

Let \(S = \boldsymbol{s} + {P}^{\langle {{\boldsymbol{c}}, \cdot} \rangle \le {K}}\). For the detailing \(\Lambda' = \Lambda_1\Lambda_2\Lambda_3\), we first apply 11 and obtain that \(\mathop{\operatorname{\mathrm{Reach}}}\nolimits(\Lambda_1, S) \cap ([0, B] \times \mathbb{N})\) is a finite union of sets \(\boldsymbol{a}_1 + \{\boldsymbol{p}_1\}^{\le K_1}\), where \(\boldsymbol{a}_1 = (x, a)\) and \(\boldsymbol{p}_1 = (0, p)\) satisfy: (i) \(x \in [0, B]\), (ii) \(a, p \le {\mathop{\operatorname{\mathrm{poly}}}\nolimits({\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(\Lambda), \mathop{\operatorname{\mathrm{\mathrm{\small norm}}}}\nolimits(S)})}\).

For each such hybrid set, we apply 9 to each one-turn segment of \(\Lambda_2\). Since the number of one-turn segments in \(\Lambda_2\) is bounded by \(\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(\Lambda_2) \le {\mathop{\operatorname{\mathrm{poly}}}\nolimits({\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(\Lambda)})}\), we conclude that \(\mathop{\operatorname{\mathrm{Reach}}}\nolimits(\Lambda_1\Lambda_2, S) \cap ([0, B] \times \mathbb{N})\) is a finite union of hybrid sets \(\boldsymbol{a}_2 + \{\boldsymbol{p}_2\}^{\le K_2}\), where \(\boldsymbol{a}_2 = (x, a')\) and \(\boldsymbol{p}_2 = (0, p')\) satisfy: (i) \(x \in [0, B]\), (ii) \(a' \le a + \mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(\Lambda_2) \cdot {\mathop{\operatorname{\mathrm{poly}}}\nolimits({B, \mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(\Lambda_2), p})} \le {\mathop{\operatorname{\mathrm{poly}}}\nolimits({\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(\Lambda), \mathop{\operatorname{\mathrm{\mathrm{\small norm}}}}\nolimits(S)})}\), and (iii) \(p' \le {\mathop{\operatorname{\mathrm{poly}}}\nolimits({\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(\Lambda), \mathop{\operatorname{\mathrm{\mathrm{\small norm}}}}\nolimits(S)})}\).

Finally, we apply 10 to \(\Lambda_3\) with each of the hybrid sets \(\boldsymbol{a}_2 + \{\boldsymbol{p}_2\}^{\le K_2}\) as a source. This shows that \(\mathop{\operatorname{\mathrm{Reach}}}\nolimits\{\Lambda_1\Lambda_2\Lambda_3, S\}\) is a finite union of hybrid sets \(S' = \boldsymbol{b} + {P'}^{\langle {{\boldsymbol{c}'}, \cdot} \rangle \le {K'}}\), where \(\mathop{\operatorname{\mathrm{\mathrm{\small norm}}}}\nolimits(S') \le {\mathop{\operatorname{\mathrm{poly}}}\nolimits({\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(\Lambda), \left\Vert{\boldsymbol{a}_2}\right\Vert, \left\Vert{\boldsymbol{p}_2}\right\Vert})} \le {\mathop{\operatorname{\mathrm{poly}}}\nolimits({\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(\Lambda), \mathop{\operatorname{\mathrm{\mathrm{\small norm}}}}\nolimits(S)})}\).

To see that the periods belong to \(\mathop{\operatorname{\mathrm{\mathrm{\small cone}}}}\nolimits(P) + \mathop{\operatorname{\mathrm{\mathrm{\small cone}}}}\nolimits(\Lambda)\), one needs to go through in detail the proof of 11 9 10 12. It can be verified that periods constructed there correspond to some non-negative homogeneous solutions of the characterization system of \(\Lambda\). Hence, they are non-negative combinations of vectors from \(P\) and loops in \(\Lambda\). ◻

Proof. By 7, reachability in \(V\) from \(p\) to \(q\) is characterized by finitely many SLPSs \(\Lambda\) of size \(\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(\Lambda) \le {\mathop{\operatorname{\mathrm{poly}}}\nolimits({\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V)})}\). Hence, the polynomial-sized representation of \(\mathop{\operatorname{\mathrm{Reach}}}\nolimits_{q}({V},{p(S)})\) can be derived from 13. In order to justify that \(P' \subseteq \mathop{\operatorname{\mathrm{\mathrm{\small cone}}}}\nolimits(P) + \mathop{\operatorname{\mathrm{\mathrm{\small cone}}}}\nolimits(V)\), we need to show that every loop in \(\Lambda\) belongs to \(\mathop{\operatorname{\mathrm{\mathrm{\small cone}}}}\nolimits(V)\). This could be verified by looking carefully into the proof of 7. Here, we also provide a black-box proof of this fact.

Let \(\Lambda = \alpha_0 \beta_1 \alpha_1 \ldots \beta_k \alpha_k\) be an SLPS satisfying that \(\boldsymbol{x} \xrightarrow{\Lambda} \boldsymbol{y}\) implies \(p(\boldsymbol{x}) \xrightarrow{*} q(\boldsymbol{y})\) in \(V\). We show that \(\beta_j \in \mathop{\operatorname{\mathrm{\mathrm{\small cone}}}}\nolimits(V)\) for any \(j \in [k]\). Indeed, one can easily see that for all \(\ell \in \mathbb{N}\), there exists a vector \(\boldsymbol{s}_\ell \in \mathbb{N}^2\) sufficiently large, so that \[\boldsymbol{s}_\ell \xrightarrow{\alpha_0\alpha_1\ldots\alpha_{j-1}\beta_j^{\ell}\alpha_j\ldots\alpha_k} \boldsymbol{t}_\ell = \boldsymbol{s}_{\ell} + \ell \cdot {\beta_j} + \mathop{\operatorname{\mathrm{\mathrm{\small eff}}}}\nolimits(\alpha_0\alpha_1\ldots\alpha_k).\] Hence, there also exists a path \(\pi_\ell\) in \(V\) such that \(p(\boldsymbol{s}_\ell) \xrightarrow{\pi_\ell} q(\boldsymbol{t}_\ell)\) for \(\ell \in \mathbb{N}\), where \(\mathop{\operatorname{\mathrm{\mathrm{\small eff}}}}\nolimits(\pi_\ell) = \ell \cdot {\beta_j} + \mathop{\operatorname{\mathrm{\mathrm{\small eff}}}}\nolimits(\alpha_0\alpha_1\ldots\alpha_k)\). Denote \(\mathcal{I}_{\pi_\ell}\) the Parikh image of \(\pi_\ell\), which is the function mapping each transition in \(V\) to its number of occurrences along \(\pi_\ell\). We may view \(\mathcal{I}_{\pi_\ell}\) as a vector comparable by the well-quasi-order \(\le\). So there exist \(m < n \in \mathbb{N}\) such that \(\mathcal{I}_{\pi_m} \le \mathcal{I}_{\pi_n}\). Their difference \(\mathcal{I} = \mathcal{I}_{\pi_n} - \mathcal{I}_{\pi_m}\) maps each transition to a non-negative number. Observe that for each state \(s\) in \(V\), \(\mathcal{I}\) specifies the same number of transitions flowing in \(s\) as those flowing out of \(s\). Hence, \(\mathcal{I}\) is the sum of Parikh images of finitely many cycles in \(V\). Moreover, the “effect” of \(\mathcal{I}\) is \[\begin{align} \mathop{\operatorname{\mathrm{\mathrm{\small eff}}}}\nolimits(\mathcal{I}) := \sum_{\text{transition }u} \mathop{\operatorname{\mathrm{\mathrm{\small eff}}}}\nolimits(u) \cdot \mathcal{I}(u) & = \sum_{\text{transition }u} \mathop{\operatorname{\mathrm{\mathrm{\small eff}}}}\nolimits(u) \cdot \mathcal{I}_{\pi_n}(u) - \sum_{\text{transition }u} \mathop{\operatorname{\mathrm{\mathrm{\small eff}}}}\nolimits(u) \cdot \mathcal{I}_{\pi_m}(u)\\ &= \mathop{\operatorname{\mathrm{\mathrm{\small eff}}}}\nolimits(\pi_n) - \mathop{\operatorname{\mathrm{\mathrm{\small eff}}}}\nolimits(\pi_m) = (n-m) \cdot {\beta_j}. \end{align}\] This justifies that \(\beta_j\) belongs to \(\mathop{\operatorname{\mathrm{\mathrm{\small cone}}}}\nolimits(V)\). ◻

Proof. Let \(Q, T\) be the states and transitions of \(V\). Let \(U := \mathop{\operatorname{\mathrm{\mathrm{\small cyc}}}}\nolimits(V)\). A normal vector of \(U\) is a vector \(\boldsymbol{n} \in \mathbb{Z}^3\) such that \(\langle {\boldsymbol{n}, \boldsymbol{u}} \rangle = 0\) for all \(\boldsymbol{u} \in U\). We consider two cases.

Case 1. \(U\) has a non-zero normal vector \(\boldsymbol{n} \in \mathbb{Z}_{\ge0}^3\).

Consider a run \(p(\boldsymbol{s} + \boldsymbol{p}) \xrightarrow{\pi} q(\boldsymbol{t})\) where \(\boldsymbol{p} \in {P}^{\langle {{\boldsymbol{c}}, \cdot} \rangle \le {K}}\). By extracting cycles from \(\pi\) exhaustively, it can be justified that \(\mathop{\operatorname{\mathrm{\mathrm{\small eff}}}}\nolimits(\pi)\) is decomposed into \(\boldsymbol{z} + \boldsymbol{u}\) where \(\boldsymbol{u} \in U\) and \(\boldsymbol{z}\) is the effect of some simple path. Hence, \[\begin{align} \langle {\boldsymbol{n}, \boldsymbol{t}} \rangle & = \langle {\boldsymbol{n}, \boldsymbol{s} + \boldsymbol{p}} \rangle + \langle {\boldsymbol{n}, \mathop{\operatorname{\mathrm{\mathrm{\small eff}}}}\nolimits(\pi)} \rangle = \langle {\boldsymbol{n}, \boldsymbol{s}} \rangle + \langle {\boldsymbol{n}, \boldsymbol{z}} \rangle \end{align}\] where we use the fact that \(\boldsymbol{p} \in P^* \subseteq \mathop{\operatorname{\mathrm{\mathrm{\small cyc}}}}\nolimits(V)\). By 2, we may assume a polynomial bound on the norm of the normal vector \(\left\Vert{\boldsymbol{n}}\right\Vert \le {\mathop{\operatorname{\mathrm{poly}}}\nolimits({\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V)})}\). Thus, \[\begin{align} \langle {\boldsymbol{n}, \boldsymbol{t}} \rangle \le 3\left\Vert{\boldsymbol{n}}\right\Vert \cdot (\left\Vert{\boldsymbol{s}}\right\Vert + \left\Vert{\boldsymbol{z}}\right\Vert) \le {\mathop{\operatorname{\mathrm{poly}}}\nolimits({\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V), \left\Vert{\boldsymbol{s}}\right\Vert})}. \end{align}\] As \(\boldsymbol{n} \in \mathbb{Z}_{\ge0}^3\), let \(K = \mathop{\operatorname{\mathrm{supp}}}\nolimits(\boldsymbol{n})\), we deduce that \(\left\Vert{\boldsymbol{t}|_K}\right\Vert \le {\mathop{\operatorname{\mathrm{poly}}}\nolimits({\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V), \left\Vert{\boldsymbol{s}}\right\Vert})} =: B\) as well. This shows that any configuration reachable from \(p(S)\) has bounded counter values for counters in \(K\). We may encode counters in \(K\) into the states of a VASS. To be explicit, choose \(i \in K\) and construct a 2-VASS \(V_S = (Q_S, T_S)\) defined by

• \(Q_S = \{q_v \mid q \in Q, v \in [0, B]\}\);

• \(T_S = \{p_u \xrightarrow{\boldsymbol{a}|_{-i}} q_v \mid p \xrightarrow{\boldsymbol{a}} q \in T, \boldsymbol{a}(i) = v - u \}\).

Clearly \(\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V_S) \le {\mathop{\operatorname{\mathrm{poly}}}\nolimits({B,\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V)})} \le {\mathop{\operatorname{\mathrm{poly}}}\nolimits({\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V), \left\Vert{\boldsymbol{s}}\right\Vert})}\). Let \(p' := p_u\) where \(u = \boldsymbol{s}(i)\). Notice that for any \(\boldsymbol{p} \in P^*\) we must have \(\boldsymbol{p}(i) = 0\) as \(\langle {\boldsymbol{n}, \boldsymbol{p}} \rangle = 0\), and \(P \subseteq \mathbb{N}^3\), \(\boldsymbol{n} \ge \boldsymbol{0}\). We deduce that \[\mathop{\operatorname{\mathrm{Reach}}}\nolimits_{q}({V},{p(S)}) = \bigcup_{v \in [0, B]} \{\boldsymbol{t} \in \mathbb{N}^3 \mid \boldsymbol{t}(i) = v, \boldsymbol{t}|_{-i} \in \mathop{\operatorname{\mathrm{Reach}}}\nolimits_{q_v}({V_S},{p_u(S|_{-i})})\}\] By 14, each \(\mathop{\operatorname{\mathrm{Reach}}}\nolimits_{q_v}({V_S},{p_u(S|_{-i})})\) is a finite union of hybrid sets \(S' = \boldsymbol{b'} + {P'}^{\langle {{\boldsymbol{c}'}, \cdot} \rangle \le {K'}}\). We may lift \(S'\) to three dimensions by adding the \(i\)-th coordinate back to \(\boldsymbol{b}'\) with value \(v\) and to \(P'\) with value \(0\). As \(P' \subseteq \mathop{\operatorname{\mathrm{\mathrm{\small cone}}}}\nolimits(P|_{-i}) + \mathop{\operatorname{\mathrm{\mathrm{\small cone}}}}\nolimits(V_S)\), we deduce that the lifted version is also contained in \(\mathop{\operatorname{\mathrm{\mathrm{\small cone}}}}\nolimits(P) + \mathop{\operatorname{\mathrm{\mathrm{\small cone}}}}\nolimits(V)\).

Case 2. Every normal vector of \(U\) contains two different signs.

Take a non-zero normal vector \(\boldsymbol{n} \in \mathbb{Z}^3\) with \(\left\Vert{\boldsymbol{n}}\right\Vert \le {\mathop{\operatorname{\mathrm{poly}}}\nolimits({\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V)})}\). We may assume \(\boldsymbol{n} = (a, b, -c)\) for some \(a, b, c \in \mathbb{N}\) and \(c\ne 0\). For a vector \(\boldsymbol{x} \in \mathbb{N}^3\) we define its shift as \[\delta(\boldsymbol{x}) = \langle {\boldsymbol{n}, \boldsymbol{x}} \rangle - \langle {\boldsymbol{n}, \boldsymbol{s}} \rangle\] Similar to case 1, for any configuration \(q(\boldsymbol{t})\) reachable from \(p(S)\), we have \(|\delta(\boldsymbol{t})| \le B\) for some \(B \le {\mathop{\operatorname{\mathrm{poly}}}\nolimits({\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V)})}\). Thus, we encode shifts into states and ignore the third counter. To be explicit, we construct a 2-VASS \(V_S = (Q_S, T_S)\) where

• \(Q_S\) contains \(q_v, q_v'\) for each \(q \in Q\) and \(v \in [-B, B]\);

• \(T_S\) contains \(p_u \xrightarrow{\boldsymbol{a}|_{-3}} q_v'\) if there is a transition \(p \xrightarrow{\boldsymbol{a}} q\) in \(T\) such that \(\delta(\boldsymbol{a}) = v - u\).

A configuration \(q_v(x, y)\) is supposed to represent the configuration \(q(x, y, z)\) in \(V\) such that \(\delta(x, y, z) = v\). Let \(z(x, y, v) = (ax + by - v - \langle {\boldsymbol{n}, \boldsymbol{s}} \rangle) / c\), which is supposedly the missing counter value in \(q_v(x, y)\). One can verify that if \(z(x, y, v)\) is an integer, then every configuration \(p_u(x', y')\) reachable from \(q_v(x, y)\) renders \(z(x', y', u)\) an integer. To check non-negativity of \(z\), we add a gadget from each \(q_v'\) to \(q_v\) that tests the inequality \(ax + by -v \ge \langle {\boldsymbol{n}, \boldsymbol{s}} \rangle\). The minimal solutions to this inequality are finite and bounded by \({\mathop{\operatorname{\mathrm{poly}}}\nolimits({\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V), \left\Vert{\boldsymbol{s}}\right\Vert})}\), which creates a polynomial amplification in \(\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V_S)\). Verify that \[\mathop{\operatorname{\mathrm{Reach}}}\nolimits_{q}({V},{p(S)}) = \bigcup_{v \in [-B, B]} \{(x, y, z(x, y, v)) \mid (x, y) \in \mathop{\operatorname{\mathrm{Reach}}}\nolimits_{q_v}({V_S},{p_0(S|_{-3})})\}.\] Again by 14, each \(\mathop{\operatorname{\mathrm{Reach}}}\nolimits_{q_v}({V_S},{p_0(S|_{-3})})\) is a finite union of hybrid sets \(\boldsymbol{b}' + {P'}^{\langle {{\boldsymbol{c}'}, \cdot} \rangle \le {K'}}\). We lift it to three dimensions by mapping \(\boldsymbol{b}' = (x, y)\) to \(\boldsymbol{b}'' = (x, y, z(x, y, v))\), and mapping each \(\boldsymbol{p}' = (x, y) \in P'\) to \(\boldsymbol{p}'' = (x, y, (ax + by) / c)\). We need to justify that the lifted vectors are integral. Notice that for each \((x_s, y_s) \in S|_{-3}\) there exists \(z_s \in \mathbb{N}\) such that \((x_s, y_s, z_s) \in S\). We must have \(z(x_s, y_s, 0) = z_s \in \mathbb{N}\). As \(q_v(\boldsymbol{b}')\) is reachable from \(p_0(x_s, y_s)\) for some \((x_s, y_s) \in S|_{-3}\), we deduce that \(z(\boldsymbol{b}'(1), \boldsymbol{b}'(2), v) = \boldsymbol{b}''(3)\) is integral as well. Similarly, for each \(\boldsymbol{p}' \in P'\), \(q_v(\boldsymbol{b}'+\boldsymbol{p}')\) is reachable from \(p_0(x_s, y_s)\) for some \((x_s, y_s) \in S|_{-3}\) (we may assume each period in \(P'\) can be used at least once), so \(\boldsymbol{b}'' + \boldsymbol{p}''\) is integral. Hence, so is \(\boldsymbol{p}''\) itself.

This completes the proof of [thm:hybrid-2vass-hybrid]. ◻

Proof. Let \(V = (V_1)u_1(V_2)\ldots u_{k-1}(V_k)\), with \(C_i := \mathop{\operatorname{\mathrm{\mathrm{\small cone}}}}\nolimits_{>0}(V_i)\) and \(\overline{C_i} := \mathop{\operatorname{\mathrm{\mathrm{\small cone}}}}\nolimits(V_i)\). As \((V,s)\) is fowrard diagonal, there exists a cycle \(\pi_+\) in \(V_1\) such that \(\boldsymbol{p} := \mathop{\operatorname{\mathrm{\mathrm{\small eff}}}}\nolimits(\pi_+) \in \mathbb{Q}_{>0}^3\). Also, as \((V,t)\) is backward diagonal, there exists a cycle \(\pi_-\) in \(V_k\) such that \(\boldsymbol{q} := \mathop{\operatorname{\mathrm{\mathrm{\small eff}}}}\nolimits(\pi_-) \in \mathbb{Q}_{<0}^3\)

(\(\implies\))

Assume w.l.o.g.that \(\mathbb{Q}_{\ge0}^3 \subseteq \mathop{\operatorname{\mathrm{\mathrm{\small SeqCone}}}}\nolimits(V)\). We prove that \(\mathbb{Q}_{>0}^3 \subseteq \mathop{\operatorname{\mathrm{\mathrm{\small SeqCone}}}}\nolimits_{>0}(V)\). Let \(\boldsymbol{x} \in \mathbb{Q}_{>0}^3\). For each \(C_i\), take a vector \(\boldsymbol{c}_i\) whose norm is small enough such that \(\boldsymbol{p} + \boldsymbol{c}_1 + \cdots + \boldsymbol{c}_j \in \mathbb{Q}_{>0}^3\) for all \(j \in [k]\). Let \(\epsilon > 0\) be a rational number small enough so that \[\boldsymbol{x}' := \boldsymbol{x} - \epsilon(\boldsymbol{p} + \boldsymbol{c}_1 + \boldsymbol{c}_2 + \cdots + \boldsymbol{c}_k) \in \mathbb{Q}_{>0}^3 \subseteq \mathbb{Q}_{\ge 0}^3.\] Then \(\boldsymbol{x}' \in \mathop{\operatorname{\mathrm{\mathrm{\small SeqCone}}}}\nolimits(V)\) and there exists \(\boldsymbol{v}_1 \in \overline{C_1}, \ldots, \boldsymbol{v}_k \in \overline{C_k}\) such that \(\boldsymbol{x}' = \boldsymbol{v}_1 + \cdots + \boldsymbol{v}_k\) and \(\boldsymbol{v}_1 + \cdots + \boldsymbol{v}_j \ge \boldsymbol{0}\) for all \(j \in [k]\). We have \[\boldsymbol{x} = (\boldsymbol{v}_1 + \epsilon(\boldsymbol{p} + \boldsymbol{c}_1)) + (\boldsymbol{v}_2 + \epsilon\boldsymbol{c}_2) + \cdots + (\boldsymbol{v}_k + \epsilon\boldsymbol{c}_k),\] which witnesses that \(\boldsymbol{x} \in \mathop{\operatorname{\mathrm{\mathrm{\small SeqCone}}}}\nolimits_{>0}(V)\). As the choice of \(\boldsymbol{x}\) is arbitrary, we conclude that \(\mathbb{Q}_{>0}^3 \subseteq \mathop{\operatorname{\mathrm{\mathrm{\small SeqCone}}}}\nolimits_{>0}(V)\).

(\(\impliedby\))

Assume w.l.o.g.that \(\mathbb{Q}_{>0}^3 \subseteq \mathop{\operatorname{\mathrm{\mathrm{\small SeqCone}}}}\nolimits_{>0}(V)\). We prove that \(\mathbb{Q}_{\ge0}^3 \subseteq \mathop{\operatorname{\mathrm{\mathrm{\small SeqCone}}}}\nolimits(V)\). As \(\mathop{\operatorname{\mathrm{\mathrm{\small SeqCone}}}}\nolimits(V)\) is a convex set, it suffices to show that each unit vector \(\boldsymbol{e}_i\) lies in \(\mathop{\operatorname{\mathrm{\mathrm{\small SeqCone}}}}\nolimits(V)\). Observe that \(\boldsymbol{x}_i := \boldsymbol{e}_i - \boldsymbol{q} \in \mathbb{Q}_{>0}^3 \subseteq \mathop{\operatorname{\mathrm{\mathrm{\small SeqCone}}}}\nolimits_{>0}(V) \subseteq \mathop{\operatorname{\mathrm{\mathrm{\small SeqCone}}}}\nolimits(V)\). As \(\boldsymbol{q} \in \overline{C_k}\), it is straightforward to check that \(\boldsymbol{e}_i = \boldsymbol{x}_i + \boldsymbol{q} \in \mathop{\operatorname{\mathrm{\mathrm{\small SeqCone}}}}\nolimits(V)\).

 ◻

Proof. We express \(\boldsymbol{a} = \boldsymbol{c}_1 + \cdots + \boldsymbol{c}_j\) and \(\boldsymbol{a}' = \boldsymbol{d}_1 + \cdots + \boldsymbol{d}_\ell\) that are summations witnessing the membership \(\boldsymbol{a} \in \mathop{\operatorname{\mathrm{\mathrm{\small SeqCone}}}}\nolimits(C_1, \ldots, C_j)\) and \(\boldsymbol{a}' \in \mathop{\operatorname{\mathrm{\mathrm{\small SeqCone}}}}\nolimits(D_1, \ldots, D_\ell)\). Then \[\boldsymbol{a} - \boldsymbol{a}' = \boldsymbol{c}_1 + \cdots + \boldsymbol{c}_j + (-\boldsymbol{d}_\ell) + \cdots + (-\boldsymbol{d}_1).\] We need to verify for every \(x \in [0, \ell - 1]\), that \(\boldsymbol{c}_1 + \cdots + \boldsymbol{c}_j + (-\boldsymbol{d}_{\ell - 0}) + \cdots + (-\boldsymbol{d}_{\ell - x}) \ge \boldsymbol{0}\). This can be justified as \[\begin{align} \boldsymbol{c}_1 + \cdots + \boldsymbol{c}_j + (-\boldsymbol{d}_{\ell - 0}) + \cdots + (-\boldsymbol{d}_{\ell - x}) &= \boldsymbol{a} - (\boldsymbol{a}' - (\boldsymbol{d}_1 + \ldots + \boldsymbol{d}_{\ell - x - 1}))\\ &= (\boldsymbol{a} - \boldsymbol{a}') + (\boldsymbol{d}_1 + \ldots + \boldsymbol{d}_{\ell - x - 1}) \ge \boldsymbol{0}, \end{align}\] where the last inequality is valid because every prefix sum of \(\boldsymbol{d}_1 + \cdots + \boldsymbol{d}_\ell\) is non-negative. We conclude that \(\boldsymbol{a} - \boldsymbol{a}' \in \mathop{\operatorname{\mathrm{\mathrm{\small SeqCone}}}}\nolimits(C_1, \ldots, C_j, -D_\ell, \ldots, -D_1)\). ◻

Proof. The “only if” direction can be easily justified by taking \(i = j = k\). For the “if” direction, by 15 we have \[\begin{align} \mathbb{Q}_{\ge0}^d &= \mathbb{Q}_{\ge0}^d \cap (\mathop{\operatorname{\mathrm{\mathrm{\small SeqCone}}}}\nolimits(C_1, \ldots, C_i) - \mathop{\operatorname{\mathrm{\mathrm{\small SeqCone}}}}\nolimits(-C_k, \ldots, -C_j))\\ &\subseteq \mathop{\operatorname{\mathrm{\mathrm{\small SeqCone}}}}\nolimits(C_1, \ldots, C_i, C_j, \ldots, C_k)\\ &\subseteq \mathop{\operatorname{\mathrm{\mathrm{\small SeqCone}}}}\nolimits(C_1, \ldots, C_k). \end{align}\] As any sequential cone is contained in \(\mathbb{Q}_{\ge0}^d\) we conclude \(\mathop{\operatorname{\mathrm{\mathrm{\small SeqCone}}}}\nolimits(C_1, \ldots, C_k) = \mathbb{Q}_{\ge 0}^d\). ◻

Proof. Let \(P_i\) be the \((d \times n_i)\)-matrix whose columns are the generators of \(C_i\), for \(i \in [k]\). Notice that we have \(n_i \le (M+1)^d\) as \(\left\Vert{P_i}\right\Vert \le M\). Let \(n := \sum_{i} n_i\), then \(n \le k(M+1)^d\). Consider the following linear system \[\begin{align} \label{eq:seq-cone-ge-0} \begin{pmatrix} P_1 & 0 & 0 & \cdots & 0\\ P_1 & P_2 & 0 & \cdots & 0\\ & & \vdots & &\\ P_1 & P_2 & P_3 & \cdots & P_k\\ \end{pmatrix} \cdot \begin{pmatrix} \boldsymbol{x}_1 \\ \boldsymbol{x}_2 \\ \vdots \\ \boldsymbol{x}_k \end{pmatrix} \ge \boldsymbol{0} \end{align}\tag{12}\] Each non-negative integer solution induces a vector \(P_1\boldsymbol{x}_1 + \cdots + P_k\boldsymbol{x}_k\) in \(\mathop{\operatorname{\mathrm{\mathrm{\small SeqCone}}}}\nolimits(C_1, \ldots, C_k)\) and vice versa. Let \(X\) be the set of the non-negative integer solutions to 12 . By 1, \(X\) is a cone generated by some finite set \(X_0\) where \[\begin{align} \left\Vert{X_0}\right\Vert &\le ((n+kd+1)M+1)^{kd} \le ((k(M+1)^d + kd + 1)M+1)^{kd} \\&\le ((M+1)^{(2d+1)k})^{kd} \le {\mathop{\operatorname{\mathrm{poly}}}\nolimits({M})}^{k^2d^2} \end{align}\] Each solution \((\boldsymbol{x}_1, \ldots, \boldsymbol{x}_k) \in X_0\) yields a generator of \(\mathop{\operatorname{\mathrm{\mathrm{\small SeqCone}}}}\nolimits(P_1, \ldots, P_k)\), namely \(\boldsymbol{g} := P_1\boldsymbol{x}_1 + \cdots + P_k\boldsymbol{x}_k\). It holds that \(\left\Vert{\boldsymbol{g}}\right\Vert\le n \cdot M \cdot \left\Vert{X_0}\right\Vert \le {\mathop{\operatorname{\mathrm{poly}}}\nolimits({M})}^{(kd)^3}\). ◻

Proof of [lem:separating-plane-non-wide]. Denote \(C_h = \mathop{\operatorname{\mathrm{\mathrm{\small SeqCone}}}}\nolimits(V_h)\) and \(C_t = \mathop{\operatorname{\mathrm{\mathrm{\small SeqCone}}}}\nolimits({V_t}^{\mathrm{rev}})\). Let \(P_h = \{\boldsymbol{u}_1, \ldots, \boldsymbol{u}_\ell\}\) be the set of generators of \(C_h\), and let \(P_t = \{\boldsymbol{v}_1, \ldots, \boldsymbol{v}_m\}\) be the set of generators of \(C_t\). By 16, we assume \(\left\Vert{P_h}\right\Vert, \left\Vert{P_t}\right\Vert \le {\mathop{\operatorname{\mathrm{poly}}}\nolimits({\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V)})}^{(kd)^3}\). Let \(W = P_h \cup P_t\), we identify two cases:

Case 1. \(\mathop{\operatorname{\mathrm{span}}}\nolimits(W) \ne \mathbb{Q}^d\).

In this case, both \(C_h\) and \(C_t\) are already contained in a hyperplane. Let \(X = \{\boldsymbol{x}_1, \ldots, \boldsymbol{x}_r\}\) be a basis of \(\mathop{\operatorname{\mathrm{span}}}\nolimits(W)\) comprising vectors from \(W\). Then any non-zero vector \(\boldsymbol{n} \in \mathbb{Z}^d\) orthogonal to \(X\) “separates” \(C_h\) and \(C_t\), in the sense that \(\langle {\boldsymbol{n}, C_h} \rangle \ge 0\) and \(\langle {\boldsymbol{n}, C_t} \rangle \le 0\) (because they are both equal to zero). We may take \(\boldsymbol{n}\) as any non-zero integer solution of the equation \(X^T\boldsymbol{n} = \boldsymbol{0}\). By 2, such an \(\boldsymbol{n}\) exists with \(\left\Vert{\boldsymbol{n}}\right\Vert \le \mathcal{O}(d\left\Vert{W}\right\Vert)^d \le {\mathop{\operatorname{\mathrm{poly}}}\nolimits({\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V)})}^{k^3d^5}\). Here we remark that 2 is stated for non-negative solutions. We may negate some columns of \(X\) to assume that \(\boldsymbol{n} \ge \boldsymbol{0}\), which does not affect the norm of \(\boldsymbol{n}\).

Case 2. \(\mathop{\operatorname{\mathrm{span}}}\nolimits(W) = \mathbb{Q}^d\).

As \(V\) is not wide, by 3, there exists a non-zero vector \(\boldsymbol{p} \in \mathbb{Z}_{\ge0}^d\) such that \(\boldsymbol{p} \notin C_h - C_t\). Viewing \(P_h\) and \(P_t\) as matrices whose columns are their elements, the following equation has no non-negative solution: \[\begin{pmatrix} P_h & -P_t \end{pmatrix} \cdot \boldsymbol{x} = \boldsymbol{p}.\] By the fundamental theorem of linear inequalities [27], there exists a non-zero vector \(\boldsymbol{n}_0 \in \mathbb{Q}^d\) such that \(\langle {\boldsymbol{n}_0, \boldsymbol{p}} \rangle < 0\) and

• \(\langle {\boldsymbol{n}_0, \boldsymbol{u}} \rangle \ge 0\) for \(\boldsymbol{u} \in P_h\), and \(\langle {\boldsymbol{n}_0, -\boldsymbol{v}} \rangle \ge 0\) for \(\boldsymbol{v} \in P_t\); hence \(\langle {\boldsymbol{n}_0, \mathop{\operatorname{\mathrm{\mathrm{\small SeqCone}}}}\nolimits(V_h)} \rangle \ge 0\), and \(\langle {\boldsymbol{n}_0, \mathop{\operatorname{\mathrm{\mathrm{\small SeqCone}}}}\nolimits({V_t}^{\mathrm{rev}})} \rangle \le 0\);

• the hyperplane \(\{\boldsymbol{x} \in \mathbb{Q}^d \mid \langle {\boldsymbol{n}_0, \boldsymbol{x}} \rangle = 0\}\) contains \(d - 1\) linear independent vectors from \(W\); here we let \(X\) denote the set of these \(d-1\) vectors.

The solutions to the equation \(X^T \boldsymbol{n} = 0\) is exactly \(\mathop{\operatorname{\mathrm{\mathrm{\small cone}}}}\nolimits\{\boldsymbol{n}_0, -\boldsymbol{n}_0\}\), as the rank of \(X\) is \(d - 1\). Let \(j \in [d]\) be such that \(\boldsymbol{n}_0(j) \ne 0\), we further assume \(\boldsymbol{n}_0(j) > 0\). The desired vector \(\boldsymbol{n}\) may be taken as any non-zero integer solution to the system \(X^T \boldsymbol{n} = 0, \boldsymbol{n}(j) > 0\). By 1, such an \(\boldsymbol{n}\) exists with \(\left\Vert{\boldsymbol{n}}\right\Vert \le \mathcal{O}(d\left\Vert{W}\right\Vert)^{d+1} \le {\mathop{\operatorname{\mathrm{poly}}}\nolimits({\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V)})}^{k^3d^5}\).

 ◻

Proof. Assume that \(V=(Q, T)\), \(s=p(\boldsymbol{x})\), and \(M:=\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V)\). For the first statement, let \(\boldsymbol{a} \in \mathop{\operatorname{\mathrm{\mathrm{\small cone}}}}\nolimits(V) \cap \mathbb{Q}_{>0}^d\) be a positive vector. By Carathéodory’s Theorem [27], there exists \(d\) simple cycles \((\theta_i)_{i \in [d]}\) in \(V\) such that \[\sum_{i \in [d]}\lambda_i\cdot\mathop{\operatorname{\mathrm{\mathrm{\small eff}}}}\nolimits(\theta_i) = \boldsymbol{a},\] where \(\lambda_i \in \mathbb{N}\) for each \(i \in [d]\). By scaling, we may assume that each \(\lambda_i\) is an integer and \(\boldsymbol{a}\) an integer vector. It holds \(\boldsymbol{a}\geq \boldsymbol{1}\). Consider the underlying Diophantine system \(A\boldsymbol{\lambda} \ge \boldsymbol{1}\), where \(\boldsymbol{\lambda} \in \mathbb{N}^d\) are variables and \(A \in \mathbb{Z}^{d \times d}\) is the matrix whose columns are exactly \((\mathop{\operatorname{\mathrm{\mathrm{\small eff}}}}\nolimits(\theta_i))_{i \in [d]}\). Note that \(\left\Vert{A}\right\Vert \le |Q| \cdot \left\Vert{T}\right\Vert\). Applying 1, we obtain that there exists some minimal solution \(\boldsymbol{\lambda}_0\) with \(\left\Vert{\boldsymbol{\lambda}_0}\right\Vert \le \mathcal{O}(M)^{2d}\). One can construct a cycle accordingly: select the shortest cycle \(\theta_0\) visiting all states, and then concatenate each of the \(d\) simple cycles; we repeat the cycle \(\theta_i\) exactly \((|\theta_0|\cdot \left\Vert{T}\right\Vert + 1)\cdot \boldsymbol{\lambda}_0(i)\) times for each \(i \in [d]\), to obtain a single cycle \(\theta\), whose size is \[|\theta| \le |\theta_0|+(|\theta_0|\cdot \left\Vert{T}\right\Vert + 1)\cdot d \cdot \left\Vert{\boldsymbol{\lambda}_0}\right\Vert \le \mathcal{O}(M)^{2d+3} \le {\mathop{\operatorname{\mathrm{poly}}}\nolimits({M})}^d.\] and its effect is \(\mathop{\operatorname{\mathrm{\mathrm{\small eff}}}}\nolimits(\theta) = \mathop{\operatorname{\mathrm{\mathrm{\small eff}}}}\nolimits(\theta_0) + (|\theta_0|\cdot \left\Vert{T}\right\Vert + 1) \cdot A \boldsymbol{\lambda}_0 \ge -|\theta_0|\cdot \left\Vert{T}\right\Vert\cdot \boldsymbol{1} + (|\theta_0|\cdot \left\Vert{T}\right\Vert + 1) \cdot \boldsymbol{1} \ge \boldsymbol{1}\). ◻

Proof. A run \(\pi\) from \(s\) to \(t\) can be factored to \(k\) segments, one for each component. The effect of each segment \(\pi_i\) can be further decomposed into a sum of the effect \(\boldsymbol{z}_i\) of some simple path, and a vector \(\boldsymbol{c}_i \in \mathop{\operatorname{\mathrm{\mathrm{\small cone}}}}\nolimits(V_i)\). We have \[\label{2026-07-07-0828} \boldsymbol{t}_i := \boldsymbol{u} + (\boldsymbol{z}_1 + \boldsymbol{c}_1) + \cdots + (\boldsymbol{z}_i + \boldsymbol{c}_i) \ge \boldsymbol{0}\tag{13}\] for all \(i \in [k]\), as it is the vector of some configuration on \(\pi\). Now let \(\boldsymbol{p}\) be the effect of a diagonal cycle in \(V_1\) whose existence is guaranteed. We may assume \(\left\Vert{\boldsymbol{p}}\right\Vert \le {\mathop{\operatorname{\mathrm{poly}}}\nolimits({\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V)})}^{d}\) by 17. Let \(m := \left\Vert{\boldsymbol{u}}\right\Vert + \sum_{i=1}^k \left\Vert{\boldsymbol{z}_i}\right\Vert \le \left\Vert{s}\right\Vert + {\mathop{\operatorname{\mathrm{poly}}}\nolimits({\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V)})}\). We claim that \(m\boldsymbol{p} + \boldsymbol{c}_1 + \cdots + \boldsymbol{c}_k \in \mathop{\operatorname{\mathrm{\mathrm{\small SeqCone}}}}\nolimits(V)\). Indeed, for \(i \in [k]\), \[\begin{align} m\boldsymbol{p} + \boldsymbol{c}_1 + \cdots + \boldsymbol{c_i} &= \boldsymbol{t}_i + m\boldsymbol{p} - (\boldsymbol{u} + \boldsymbol{z}_1 + \cdots + \boldsymbol{z}_i) \ge \boldsymbol{t}_i \ge \boldsymbol{0}. \end{align}\] Now \(\boldsymbol{v}=\boldsymbol{t}_k\) by 13 . It follows that the difference between \(\boldsymbol{v}\) and \(\mathop{\operatorname{\mathrm{\mathrm{\small SeqCone}}}}\nolimits(V)\) is bounded by \(\boldsymbol{h} = (m\boldsymbol{p} + \boldsymbol{c}_1 + \cdots + \boldsymbol{c_k})-\boldsymbol{v} = m\boldsymbol{p} - (\boldsymbol{u} + \boldsymbol{z}_1 + \cdots + \boldsymbol{z}_k)\). Clearly \(\left\Vert{\boldsymbol{h}}\right\Vert \le 2m\left\Vert{\boldsymbol{p}}\right\Vert \le {\mathop{\operatorname{\mathrm{poly}}}\nolimits({\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V)})}^{d+1}\cdot\left\Vert{s}\right\Vert\). ◻

Proof. By [lem:reach-eq-seq-cone-plus-bounded-of-diag], there exist vectors \(\boldsymbol{h}_h, \boldsymbol{h}_t \in \mathbb{Z}^3\) such that \(\boldsymbol{z} = \boldsymbol{s}_h + \boldsymbol{h}_h = \boldsymbol{s}_t + \boldsymbol{h}_t\), where \(\boldsymbol{s}_h \in \mathop{\operatorname{\mathrm{\mathrm{\small SeqCone}}}}\nolimits(\mathcal{H}_i)\) and \(\boldsymbol{s}_t \in \mathop{\operatorname{\mathrm{\mathrm{\small SeqCone}}}}\nolimits({\mathcal{T}_i}^{\mathrm{rev}})\). Moreover, \(\left\Vert{\boldsymbol{h}_h}\right\Vert \le {\mathop{\operatorname{\mathrm{poly}}}\nolimits({\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V)})} \cdot \left\Vert{s}\right\Vert\) and \(\left\Vert{\boldsymbol{h}_t}\right\Vert \le {\mathop{\operatorname{\mathrm{poly}}}\nolimits({\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V)})} \cdot \left\Vert{t}\right\Vert\). By [lem:separating-plane-non-wide], the vector \(\boldsymbol{n}_i\) satisfies \(\langle {\boldsymbol{n}_i, \boldsymbol{s}_h} \rangle \ge 0\) and \(\langle {\boldsymbol{n}_i, \boldsymbol{s}_t} \rangle \le 0\). Hence, \[\begin{align} \langle {\boldsymbol{n}_i, \boldsymbol{z}} \rangle & = \langle {\boldsymbol{n}_i, \boldsymbol{s}_h} \rangle + \langle {\boldsymbol{n}_i, \boldsymbol{h}_h} \rangle \ge - 3\left\Vert{\boldsymbol{n}_i}\right\Vert\left\Vert{\boldsymbol{h}_h}\right\Vert \ge - {\mathop{\operatorname{\mathrm{poly}}}\nolimits({\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V)})}^{k^3}\left\Vert{s}\right\Vert,\\ \langle {\boldsymbol{n}_i, \boldsymbol{z}} \rangle & = \langle {\boldsymbol{n}_i, \boldsymbol{s}_t} \rangle + \langle {\boldsymbol{n}_i, \boldsymbol{h}_t} \rangle \le 3\left\Vert{\boldsymbol{n}_i}\right\Vert\left\Vert{\boldsymbol{h}_t}\right\Vert \le {\mathop{\operatorname{\mathrm{poly}}}\nolimits({\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V)})}^{k^3}\left\Vert{t}\right\Vert. \end{align}\] We conclude that \(|\langle {\boldsymbol{n}_i, \boldsymbol{z}} \rangle| \le {\mathop{\operatorname{\mathrm{poly}}}\nolimits({\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V)})}^{k^3} \cdot (\left\Vert{s}\right\Vert + \left\Vert{t}\right\Vert)\). ◻

Proof. Let \(M\) denote \(\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V,s,t)\), and let \(c\) be a constant satisfying \(L(x, y) \le (x+y)^c\), \(H(x, y)^2 \le (x+y)^c\), and \(B_h, B_n, \mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V_j') \le M^{ck^3}\). We prove by induction that \(f_j(x) \le (M + x)^{(4c^3k^3)^{k-j+1}}\). Firstly, for \(j = k\) we have \[f_k(x) \le (\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V_k', t) + x)^c \le (M^{ck^3} + x)^c \le (M + x)^{c^2k^3}.\] Secondly, for \(j < k\), verify that \[y := (B_h +3B_n+ 1)\cdot H(\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V_j'), x)^2 \le (M + x)^{2c^2k^3}.\] By the induction hypothesis, \(B_j(x) = f_{j+1}(y) \le (M + x)^{(2c^2k^3) \cdot (4c^3k^3)^{k-j}}\). \[\begin{align} f_j(x) & = 2L(\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V_j')+B_j(x), x) \le 2(M^{ck^3} + (M + x)^{(2c^2k^3) \cdot (4c^3k^3)^{k-j}}+x)^c\\ &\leq 2(M+x)^{(3c^3k^3)\cdot (4c^3k^3)^{k-j}}\\ & \le (M + x)^{(4c^3k^3)^{k-j+1}}. \end{align}\] Finally, we have \(f_1(x) \le (\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V, s, t) + x)^{2^{{\mathop{\operatorname{\mathrm{poly}}}\nolimits({k})}}}\). ◻

Proof. Assume that \(s = p(\boldsymbol{x})\) and \(M:=\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V)\). Let \(U := 2P(M)^{2k} \cdot (\left\Vert{s}\right\Vert + 2)\), where \(P(x)\) is the polynomial defined in 5. If \(\mathop{\operatorname{\mathrm{\mathrm{\small bd}}}}\nolimits(\pi, U) \ne \emptyset\), then there exists a coordinate that remains bounded by \(U\) throughout \(\pi\), and we are done by taking \(\pi_1=\pi_3:=\varepsilon\) and \(\pi_2 := \pi\). We shall focus on the case \(\mathop{\operatorname{\mathrm{\mathrm{\small bd}}}}\nolimits(\pi, U) = \emptyset\) and will show that there exists a sequence of jointly diagonal cycles \(\theta_1, \theta_2, \theta_3\) enabled along \(\pi\). Since \(c_1:=s\) is pumpable in \(V\), there exists some \(\iota \in [d]\) such that \(p(\boldsymbol{x})\xrightarrow{*}p(\boldsymbol{x}')\) in \(V\) for some \(\boldsymbol{x}' \ge \boldsymbol{x}+\boldsymbol{e}_\iota\). Applying Rackoff’s classical upper bound of coverability [28], we obtain a covering run \(p(\boldsymbol{x})\xrightarrow{\theta_1}p(\boldsymbol{x}'')\) in \(V\) of length \[|\theta_1|\le {\mathop{\operatorname{\mathrm{poly}}}\nolimits({M, \left\Vert{\boldsymbol{x}}\right\Vert+1})} \le {\mathop{\operatorname{\mathrm{poly}}}\nolimits({\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V,s)})},\] where \(\boldsymbol{x}'' > \boldsymbol{x}\). This also implies that \(\mathop{\operatorname{\mathrm{\mathrm{\small eff}}}}\nolimits(\theta_1)>\boldsymbol{0}\).

Now there are two subcases. In the case where \(\mathop{\operatorname{\mathrm{\mathrm{\small eff}}}}\nolimits(\theta_1) \ge \boldsymbol{1}\), we are done by taking \(\theta_2=\theta_3:=\theta_1\), and \(c_2 = c_3:=c_1\). Otherwise, we assume, w.l.o.g., that \(\mathop{\operatorname{\mathrm{\mathrm{\small eff}}}}\nolimits(\theta_1)(3) > 0\). Given a vector \(\boldsymbol{x} \in \mathbb{Q}^3\), we use \(\boldsymbol{x}|_{-3} \in \mathbb{Q}^2\) to denote the unique vector satisfying \(\boldsymbol{x}|_{-3}(i)=\boldsymbol{x}(i)\) for \(i \in [2]\). This subscription can be extended to configurations, runs, and VASS to denote the counterpart obtained by dropping the third coordinate. Now we omit the third coordinate of \((V, s, t)\) to obtain a new 2-VASS \((V',s',t')\) with size at most \(M\). Also, \(\pi\) induces a run \(\pi':=\pi|_{-3}\) in \(V'\) with \(\mathop{\operatorname{\mathrm{\mathrm{\small bd}}}}\nolimits(\pi', U) = \emptyset\), which means that there exists a configuration along \(\pi'\) whose norm exceeds \(U\). Let \(c\) be the first configuration with \(\left\Vert{c}\right\Vert \ge P(\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V'))^k\cdot(\left\Vert{s'}\right\Vert+1)\). Note that \(V\) and \(V'\) have the same state graph; hence, \(V'\) is also \(k\)-component. By 5, there is a cycle \(\theta'_2\) such that \(\mathop{\operatorname{\mathrm{\mathrm{\small eff}}}}\nolimits(\theta'_2) > \boldsymbol{0}\) and \(|\theta'_2| \le P(M)\), which is fireable at some \(p_2(\boldsymbol{x}'_2)\) before \(c\). For the original VASS \(V\), these induce a cycle \(\theta_2\) with \(|\theta_2|\le P(M)\) and \(\mathop{\operatorname{\mathrm{\mathrm{\small eff}}}}\nolimits(\theta_2)|_{-3} = \mathop{\operatorname{\mathrm{\mathrm{\small eff}}}}\nolimits(\theta_2')>\boldsymbol{0}\). Moreover, there exists a configuration \(c_2=p_2(\boldsymbol{x}_2)\) such that \((\boldsymbol{x}_2)|_{-3} = \boldsymbol{x}_2' \ge \mathop{\operatorname{\mathrm{\mathrm{\small drop}}}}\nolimits(\theta_2)|_{-3}\). The third entry of \(\mathop{\operatorname{\mathrm{\mathrm{\small eff}}}}\nolimits(\theta_3)\) may be negative. But considering the vector \[\boldsymbol{a}_2:=(\left\Vert{\mathop{\operatorname{\mathrm{\mathrm{\small drop}}}}\nolimits(\theta_2)}\right\Vert+1) \cdot \mathop{\operatorname{\mathrm{\mathrm{\small eff}}}}\nolimits(\theta_1),\] it is easy to see that \(\boldsymbol{a}_2 \in \mathop{\operatorname{\mathrm{\mathrm{\small SeqCone}}}}\nolimits(\theta_1)\). As \(\boldsymbol{x}_2 + \boldsymbol{a}_2 \ge \mathop{\operatorname{\mathrm{\mathrm{\small drop}}}}\nolimits(\theta_2)\), we conclude that \(\theta_2\) is fireable at \(p_2(\boldsymbol{x}_2 + \boldsymbol{a}_2)\). Let \(\pi_1\) be the prefix from \(s\) to \(c_2\). Since \(c\) is the first configuration whose norm exceeds the specified bound, it follows that \[\boldsymbol{z}(i) \le P(M)^k\cdot(\left\Vert{s'}\right\Vert+1) + M \le P(M)^k\cdot(\left\Vert{s}\right\Vert+2) \le U,\] holds for every \(i \in [2]\) and \(q(\boldsymbol{z})\) along \(\pi_1\). Therefore, we have \(|\mathop{\operatorname{\mathrm{\mathrm{\small bd}}}}\nolimits(\pi_1, U)|\ge 2\) and for each \(\iota \in [3]\) with \(\mathop{\operatorname{\mathrm{\mathrm{\small eff}}}}\nolimits(\theta_1)(\iota) = 0\), it holds that \(\iota \in [2] \subseteq \mathop{\operatorname{\mathrm{\mathrm{\small bd}}}}\nolimits(\pi_1, U)\)

If \(\boldsymbol{a}_2 + \mathop{\operatorname{\mathrm{\mathrm{\small eff}}}}\nolimits(\theta_2) \in \mathbb{Q}_{>0}^3\), then we are done by taking \(\theta_3:=\theta_2\) and \(c_3:=c_2\). Otherwise, we assume, w.l.o.g., that \(\mathop{\operatorname{\mathrm{\mathrm{\small eff}}}}\nolimits(\theta_2)(2) > 0\) and \(\mathop{\operatorname{\mathrm{\mathrm{\small eff}}}}\nolimits(\theta_2)(1) = 0\). Since \[P(\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V))^k\cdot(\left\Vert{c_2}\right\Vert + 1) \le P(M)^k \cdot (P(M)^k \cdot (\left\Vert{s}\right\Vert + 2) + 1) \le U,\] following the same argument, we can obtain a cycle \(\theta_3\) with \(\mathop{\operatorname{\mathrm{\mathrm{\small eff}}}}\nolimits(\theta_3)(1) > 0\), together with some \(c_3=p_3(\boldsymbol{x}_3)\) with \(\boldsymbol{x}_3(1) \ge \mathop{\operatorname{\mathrm{\mathrm{\small drop}}}}\nolimits(\theta_3)(1)\). Let \[\boldsymbol{a}_3 := (\left\Vert{\mathop{\operatorname{\mathrm{\mathrm{\small drop}}}}\nolimits(\theta_3)}\right\Vert + 1)\cdot \boldsymbol{a}_2 \in \mathop{\operatorname{\mathrm{\mathrm{\small SeqCone}}}}\nolimits(\theta_1, \theta_2).\] Then \(\boldsymbol{a}_3 + \mathop{\operatorname{\mathrm{\mathrm{\small eff}}}}\nolimits(\theta_3) \ge \boldsymbol{1}\), which implies that \(\theta_1, \theta_2, \theta_3\) are jointly diagonal. Moreover, the cycle \(\theta_3\) are fireable at \(p_3(\boldsymbol{x}_3+\boldsymbol{a}_3)\), and consequently \(\theta_1\), \(\theta_2\), \(\theta_3\) are enabled along \(c_1\), \(c_2\), and \(c_3\). Let \(\pi_2\) be the infix of \(\pi\) from \(c_2\) to \(c_3\). Then \(|\mathop{\operatorname{\mathrm{\mathrm{\small bd}}}}\nolimits(\pi_1\pi_2, U + M)| \ge 1\), and for each \(\iota \in [3]\) with \(\mathop{\operatorname{\mathrm{\mathrm{\small eff}}}}\nolimits(\theta_1)(\iota) = \mathop{\operatorname{\mathrm{\mathrm{\small eff}}}}\nolimits(\theta_2)(\iota) = 0\), it holds that \(\iota \in \{1\} \subseteq \mathop{\operatorname{\mathrm{\mathrm{\small bd}}}}\nolimits(\pi_2, U)\). Finally, we complete the proof by letting \(B\) be the maximum of all the bounds appearing in the above argument. ◻

Proof. Let \(s \xrightarrow{\pi} q(\boldsymbol{y})\) be the shortest run between these two configurations. It suffices to show that, for each \(\ell \in \mathbb{N}\), there exists a run \(s\xrightarrow{\rho_i} q(\boldsymbol{y}+\ell\cdot\boldsymbol{a})\) with \(|\rho_i| \le |\pi| + \ell \cdot \lambda \cdot |\theta_1| + \ell\cdot |\theta_2|\). Indeed, we can take \(\rho_i := \theta_1^{\ell\lambda} \pi \theta_2^{\ell}\). Since \(\boldsymbol{a} \ge \boldsymbol{0}\) and \(s \xrightarrow{\theta_1} p(x+\boldsymbol{a})\), it must hold that \(s \xrightarrow{\theta_1^{\ell\lambda}} p(\boldsymbol{x}+\ell\cdot\lambda\cdot\boldsymbol{a})\). By the monotonicity of VASS, we have \(p(\boldsymbol{x}+\ell\cdot\lambda\cdot\boldsymbol{a}) \xrightarrow{\pi} q(\boldsymbol{y}+\ell\cdot\lambda\cdot\boldsymbol{a})\). Therefore, it remains to justify that \(q(\boldsymbol{y}+\ell\cdot\lambda\cdot\boldsymbol{b}) \xrightarrow{\theta_2^\ell} q(\boldsymbol{y} + \ell \cdot \boldsymbol{b})\), which is already a \(\mathbb{Z}\)-run. It suffices to show that the first iteration and the last iteration of \(\theta_2\) are fireable, when \(\ell \ge 1\). By assumption, we have \(\boldsymbol{y} + \ell\cdot\lambda\cdot\boldsymbol{a} \ge \boldsymbol{y} + \lambda\cdot\boldsymbol{a} \ge \mathop{\operatorname{\mathrm{\mathrm{\small drop}}}}\nolimits(\theta_2)\), which implies that the first iteration is valid. As for the last iteration, just note that \[\boldsymbol{y} + \ell\cdot\lambda \cdot \boldsymbol{a} + (\ell-1)\cdot \mathop{\operatorname{\mathrm{\mathrm{\small eff}}}}\nolimits(\theta_2) = \boldsymbol{y} + (\ell - 1)\cdot\boldsymbol{b} + \lambda\cdot \boldsymbol{a} \ge \boldsymbol{y} + \lambda\cdot\boldsymbol{a} \ge \mathop{\operatorname{\mathrm{\mathrm{\small drop}}}}\nolimits(\theta_2).\] Therefore, we have \(s \xrightarrow{\rho_i} q(\boldsymbol{y} + \ell \cdot \boldsymbol{b})\), which completes the proof. ◻

Proof. Note that we do not distinguish between \(\mathbb{Q}^{I}\) and \(\mathbb{Q}^{|I|}\). Let \(M := \mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V)\). For each vector \(\boldsymbol{z} \in \mathbb{Q}^3\), we denote by \(\boldsymbol{z}|_{I}\) the unique vector in \(\mathbb{Q}^{I}\) such that \(\boldsymbol{z}|_{I}(\iota) = \boldsymbol{z}(\iota)\) for each \(\iota \in I\), and write \(\boldsymbol{z}|_{-I}:=\boldsymbol{z}|_{[d]\setminus I}\). Let \(Q' := Q \times [0,B-1]^{I}\), and we write \(p_{\boldsymbol{u}}\) for the state \((p,\boldsymbol{u}) \in Q'\). Define \[T':=\{(p_{\boldsymbol{u}},\boldsymbol{a}|_{-I},q_{\boldsymbol{v}})\mid (p,\boldsymbol{a},q) \in T, \boldsymbol{u},\boldsymbol{v} \in [0,B-1]^{I},\text{ and }\boldsymbol{u}+\boldsymbol{a}|_I=\boldsymbol{v}\}.\] Then we can construct a VASS \(V' := (Q', T')\) with \(\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V') \le B^{|I|}\cdot M\le B^3\cdot M\), which is intuitively obtained from \(V\) by encoding all the coordinates in \(I\) into states. We may add one isolated state and at most two self-loops to \(V'\) to ensure that \(\mathop{\operatorname{\mathrm{\mathrm{\small cyc}}}}\nolimits(V') = \mathbb{Q}^{[3] \setminus I}\). Assume that \(S_p = \boldsymbol{b} + {P}^{\langle {{\boldsymbol{c}}, \cdot} \rangle \le {K}}\). We shall assume that each vector in \(P\) can be used at least once. We first show that \(\boldsymbol{p}|_I = \boldsymbol{0}\) for each \(\boldsymbol{p}\in P\). Otherwise, there exists some \(\boldsymbol{p} \in P\) with \(\boldsymbol{p}|_I > \boldsymbol{0}\). Note that \(\boldsymbol{z} := \boldsymbol{b} + \boldsymbol{p} \in S\) while \(\boldsymbol{z}|_I > \boldsymbol{b}|_I\), which contradicts with the fact that \(\boldsymbol{z}|_I = \boldsymbol{x}|_I = \boldsymbol{b}|_I\). Now we can obtain a hybrid set \(S_p' = \boldsymbol{b}' + {(P')}^{\langle {{\boldsymbol{c}}, \cdot} \rangle \le {K}}\) containing \(\boldsymbol{x}|_{-I}\) by projecting \(S_p\) onto \(\mathbb{Q}^{[3]\setminus I}\), which renders true the following claim.

It is routine to check that \(p_{\boldsymbol{x}|_I}(\boldsymbol{x}|_{-I}) \xrightarrow{*} q_{\boldsymbol{y}|_I}(\boldsymbol{y}|_{-I})\) in \(V'\). Note that \(V'\) is at most 2-dimensional, given that \(I \neq \emptyset\). Since \(P' \subseteq \mathop{\operatorname{\mathrm{\mathrm{\small cyc}}}}\nolimits(V')\), by [thm:hybrid-2vass-hybrid], there exists a hybrid set in the form of \(S_q':=\boldsymbol{b}_q' + {(P'_q)}^{\langle {{\boldsymbol{c}_q}, \cdot} \rangle \le {K_q}}\) with \(\mathop{\operatorname{\mathrm{\mathrm{\small norm}}}}\nolimits(S_q') \le {\mathop{\operatorname{\mathrm{poly}}}\nolimits({B,M,\mathop{\operatorname{\mathrm{\mathrm{\small norm}}}}\nolimits(S_p)})}\) and \[\boldsymbol{y}|_{-I} \in S_q' \subseteq \mathop{\operatorname{\mathrm{Reach}}}\nolimits_{q_{\boldsymbol{y}|_I}}({V'},{p_{\boldsymbol{x}|_I}(S_p')}).\] Let \(\boldsymbol{b}_q \in \mathbb{N}^3\) be the vector obtained by augmenting \(\boldsymbol{b}_q'\) with the values \(\boldsymbol{y}|_I\) at the coordinates in \(I\). Similarly, let \(P_q\subseteq \mathbb{N}^3\) be the sets obtained by augmenting \(P'\) with zero values at the coordinates in \(I\). We claim that \(S_q := \boldsymbol{b}_q + {P_q}^{\langle {{\boldsymbol{c}_q}, \cdot} \rangle \le {K_q}}\) satisfies the requirements.

• Since \(\left\Vert{(\boldsymbol{y}|_I)}\right\Vert \le B\), it holds that \(\mathop{\operatorname{\mathrm{\mathrm{\small norm}}}}\nolimits(S_q) \le \mathop{\operatorname{\mathrm{\mathrm{\small norm}}}}\nolimits(S_q') + B \le {\mathop{\operatorname{\mathrm{poly}}}\nolimits({B + M + \mathop{\operatorname{\mathrm{\mathrm{\small norm}}}}\nolimits(S_p)})}\).

• It is trivial that \(\boldsymbol{y} \in S_q\). For every \(\boldsymbol{z} \in S_q\), we have \(\boldsymbol{z} - \boldsymbol{b}_q \in P_q^*\). It holds by construction that \((\boldsymbol{z} - \boldsymbol{b}_q)|_I = \boldsymbol{0}\). Therefore, \(\boldsymbol{z}(\iota) = \boldsymbol{b}_q(\iota) = \boldsymbol{y}(\iota)\) for every \(\iota \in I\).

• For each \(\boldsymbol{y}' \in S_q\), we have \(\boldsymbol{y}'|_{-I} \in S_q'\), which implies that there exists some \(\boldsymbol{z} \in S_p'\) with \(p_{\boldsymbol{x}|_I}(\boldsymbol{z}) \xrightarrow{*} q_{\boldsymbol{y}|_I}(\boldsymbol{y}'|_{-I})\) in \(V'\). By 2, there is a run \(p_{\boldsymbol{x}|_I}(\boldsymbol{z}') \xrightarrow{\rho'}q_{\boldsymbol{y}|_I}(\boldsymbol{y}'|_{-I})\) in \(V'\) for some \(\boldsymbol{z}' \in S_p'\) with \[\left\Vert{\boldsymbol{z}'}\right\Vert, |\rho'| \le {\mathop{\operatorname{\mathrm{poly}}}\nolimits({B, M,\mathop{\operatorname{\mathrm{\mathrm{\small norm}}}}\nolimits(S_p'), \left\Vert{\boldsymbol{y}'}\right\Vert})} \le {\mathop{\operatorname{\mathrm{poly}}}\nolimits({B, M,\mathop{\operatorname{\mathrm{\mathrm{\small norm}}}}\nolimits(S_p), \left\Vert{\boldsymbol{y}'}\right\Vert})}.\] Let \(\boldsymbol{x}' \in \mathbb{N}^3\) be the vector obtained by augmenting \(\boldsymbol{z}'\) with the values \(\boldsymbol{x}|_I\) at the coordinates in \(I\). Then by [claim:project-hybrid-set-recoverable], \(\boldsymbol{x}' \in S_p\) and \(\left\Vert{\boldsymbol{x}'}\right\Vert \le {\mathop{\operatorname{\mathrm{poly}}}\nolimits({B + \mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V) + \mathop{\operatorname{\mathrm{\mathrm{\small norm}}}}\nolimits(S_p) + \left\Vert{\boldsymbol{y}'}\right\Vert})}\). It is straightforward that \(\rho''\) induces a run \(p(\boldsymbol{x}')\xrightarrow{\rho} q(\boldsymbol{y}')\) in \(V\) with \[|\rho| = |\rho'| \le {\mathop{\operatorname{\mathrm{poly}}}\nolimits({B + \mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V) + \mathop{\operatorname{\mathrm{\mathrm{\small norm}}}}\nolimits(S_p) + \left\Vert{\boldsymbol{y}'}\right\Vert})}.\]

The argument above completes the proof of the lemma. ◻

Proof. It is trivial that \(\boldsymbol{w} \in S_r \subseteq S_r'\). For any \(\boldsymbol{z} \in S_r'\), we can write it as \[\boldsymbol{z} = \boldsymbol{z}' + \ell\cdot\boldsymbol{a} = \boldsymbol{z}' + \ell\cdot \lambda\cdot \mathop{\operatorname{\mathrm{\mathrm{\small eff}}}}\nolimits(\theta_1) + \ell \cdot \mathop{\operatorname{\mathrm{\mathrm{\small eff}}}}\nolimits(\theta_2),\] where \(\boldsymbol{z}' \in S_r \subseteq \mathop{\operatorname{\mathrm{Reach}}}\nolimits_{r}({V},{s})\) and \(\ell \in \mathbb{N}\). Note that \(\boldsymbol{z} \ge \boldsymbol{z}'\). Assume that \(\boldsymbol{a}(\iota) > 0\) for some \(\iota \in [3]\). Since \(\boldsymbol{z}(\iota) \ge \boldsymbol{z}'(\iota) + \ell \ge \ell\), we have \(\ell, \left\Vert{\boldsymbol{z}'}\right\Vert \le \left\Vert{\boldsymbol{z}}\right\Vert\). Then we have \[\min\mathop{\operatorname{\mathrm{\mathrm{\small len}}}}\nolimits(V,s,r(\boldsymbol{z}')) \le \mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V,s,r(\boldsymbol{z}'))^{2m^2k} \le \mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V,s,r(\boldsymbol{z}))^{2m^2k}.\] Since \(\theta_1\), \(\theta_2\), \(\theta_3\) can be enabled, by definition, \(\theta_1\) is fireable at \(s\) and \(\boldsymbol{w} + \lambda'\cdot\mathop{\operatorname{\mathrm{\mathrm{\small eff}}}}\nolimits(\theta_1) \ge \mathop{\operatorname{\mathrm{\mathrm{\small drop}}}}\nolimits(\theta_2)\) for some \(\lambda'\in \mathbb{N}\). Note that \(\boldsymbol{z}'\) coincides with \(\boldsymbol{w}\) in the second and third coordinates. We have \(\boldsymbol{z}' + \lambda' \cdot \mathop{\operatorname{\mathrm{\mathrm{\small eff}}}}\nolimits(\theta_1) \ge \mathop{\operatorname{\mathrm{\mathrm{\small drop}}}}\nolimits(\theta_2)\). It is clear that choosing \(\lambda = BM+1 \ge \left\Vert{\mathop{\operatorname{\mathrm{\mathrm{\small drop}}}}\nolimits(\theta_2)}\right\Vert\) suffices, which ensures that \(\boldsymbol{z}' + \lambda\cdot \mathop{\operatorname{\mathrm{\mathrm{\small eff}}}}\nolimits(\theta_1)\ge \mathop{\operatorname{\mathrm{\mathrm{\small drop}}}}\nolimits(\theta_2)\), or equivalently, \[r(\boldsymbol{z}' + \lambda\cdot\mathop{\operatorname{\mathrm{\mathrm{\small eff}}}}\nolimits(\theta_1))\xrightarrow{\theta_2} r(\boldsymbol{z}' + \boldsymbol{a}).\] By [lem:reach-closed-under-pumping-cycle], we have \(\boldsymbol{z} \in \mathop{\operatorname{\mathrm{Reach}}}\nolimits_{r}({V},{s})\) and \[\begin{align} \min \mathop{\operatorname{\mathrm{\mathrm{\small len}}}}\nolimits(V, s, r(\boldsymbol{z})) &\le \min\mathop{\operatorname{\mathrm{\mathrm{\small len}}}}\nolimits(V,s,r(\boldsymbol{z}')) + \ell\cdot\lambda \cdot|\theta_1| + \ell \cdot |\theta_2|\\ &\le \mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V,s,r(\boldsymbol{z}))^{2m^2k} + \left\Vert{\boldsymbol{z}}\right\Vert \cdot (BM + 1) \cdot B + \left\Vert{\boldsymbol{z}}\right\Vert\cdot B \\ &\le \mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V,s,r(\boldsymbol{z}))^{6m^2k}. \end{align}\] Note that \(\mathop{\operatorname{\mathrm{\mathrm{\small norm}}}}\nolimits(S_r') \le M^{2m^2k} + \left\Vert{\boldsymbol{a}}\right\Vert \le M^{6m^2k}\), which completes the proof. ◻

Proof. For any \(\boldsymbol{z} \in S_p'\), we can write it as \[\boldsymbol{z} = \boldsymbol{z}' + \ell\cdot\boldsymbol{p} = \boldsymbol{z}' + \ell\cdot \lambda\cdot \boldsymbol{a} + \ell \cdot \mathop{\operatorname{\mathrm{\mathrm{\small eff}}}}\nolimits(\theta_3),\] where \(\ell \in \mathbb{N}\) and \(\boldsymbol{z}' \in S_p\). Similarly, we have \(\ell, \left\Vert{\boldsymbol{z}'}\right\Vert \le \left\Vert{\boldsymbol{z}}\right\Vert\). Then by 5 , there exists some \(\boldsymbol{w}' \in S'_r\) with a run \(r(\boldsymbol{w}')\xrightarrow{\rho} p(\boldsymbol{z}')\) in \(V\) such that \[\left\Vert{\boldsymbol{w}'}\right\Vert, |\rho| \le \mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V,s,p(\boldsymbol{z}'))^{8m^3k} \le \mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V,s,p(\boldsymbol{z}))^{8m^3k}.\] Note that \(\boldsymbol{w}'':=\boldsymbol{w}' + \ell \cdot\lambda\cdot\boldsymbol{a} \in S_r'\) holds by construction. Then \[\left\Vert{\boldsymbol{w}''}\right\Vert \le \left\Vert{\boldsymbol{w}'}\right\Vert + \left\Vert{\boldsymbol{z}}\right\Vert \cdot \lambda \cdot \left\Vert{\boldsymbol{a}}\right\Vert \le 2\cdot\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V,s,p(\boldsymbol{z}))^{8m^3k} \le \mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V,s,p(\boldsymbol{z}))^{9m^3k}.\] By [claim:len-first-round-approx], there exists a run \(s \xrightarrow{\sigma} r(\boldsymbol{w}'')\) with \[\begin{align} |\sigma| &\le (M + 3 \cdot \left\Vert{\boldsymbol{w}''}\right\Vert)^{6m^2k} \\ &\le \left(4 \cdot \mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V,s,p(\boldsymbol{z}))^{9m^3k}\right)^{6m^2k} \\ &\le \mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V,s,p(\boldsymbol{z}))^{66m^5k^2}. \end{align}\] Again by the monotonicity of VASS reachability, we have \(r(\boldsymbol{w}'')\xrightarrow{\rho}p(\boldsymbol{z}'')\) in \(V\), where \(\boldsymbol{z}'':=\boldsymbol{z}' + \ell\cdot \lambda\cdot \boldsymbol{a}\). It is routine to check that \(p(\boldsymbol{z}'') \xrightarrow{\theta_3^\ell} p(\boldsymbol{z})\). Thus, we conclude that \(s \xrightarrow{\sigma\rho\theta_3^\ell} p(\boldsymbol{z})\) and \[\begin{align} \min \mathop{\operatorname{\mathrm{\mathrm{\small len}}}}\nolimits(V, s, p(\boldsymbol{z})) &\le |\sigma| + |\rho| + \ell\cdot |\theta_3|\\ &\le 3\cdot \mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V,s,p(\boldsymbol{z}))^{66m^5k^2}\\ &\le \mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V,s,p(\boldsymbol{z}))^{68m^5k^2}. \end{align}\] ◻

Proof. It is clear that \(s'\xrightarrow{*} t'\) in \(V'\). Note that \(\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V',s',t') \le 3L_k(M) + 10 \le 13 L_k(M)\), and \(\min \mathop{\operatorname{\mathrm{\mathrm{\small len}}}}\nolimits(V, s, t) \le L_k(M) = \min \mathop{\operatorname{\mathrm{\mathrm{\small len}}}}\nolimits(V',s',t')\). ◻

Proof. The size bound is already given in 7 . Let \(\rho\) be the shortest run from \(s'\) to \(t'\) in \(V'\). The self-loops defined by the transitions in \(T_S\) can be moved to the front of the run in \(V_S\) while keeping the whole run valid, as their effects are non-negative. So \(\rho\) can be rearranged into \(s' \xrightarrow{\rho_1} q(\boldsymbol{z})\xrightarrow{\rho_2}t\), where \(\boldsymbol{z} \in \boldsymbol{b} + (P_1 \cup P_0)^*\) and \(\rho_2\) is also a run in \(V\). Let \(\boldsymbol{\lambda} \in \mathbb{N}^{n}\) be the vector such that \(\boldsymbol{\lambda}(i)\) is the number of occurrences of the transition \((q,\boldsymbol{p}_i, q)\) in \(\rho_1\). Then we have \(\boldsymbol{z} - \sum_{i = 1}^n \boldsymbol{\lambda}(i) \cdot \boldsymbol{p}_i \in \boldsymbol{b} + P_0^*\) and \[\langle {\boldsymbol{c},\boldsymbol{\lambda}} \rangle \le \left\Vert{\boldsymbol{c}}\right\Vert \cdot \sum_{i=1}^n \boldsymbol{\lambda}(i) \le \left\Vert{\boldsymbol{c}}\right\Vert \cdot |\rho_1| \le \left\Vert{\boldsymbol{c}}\right\Vert \cdot |\rho| = \left\Vert{\boldsymbol{c}}\right\Vert \cdot \ell \le K,\] which implies that \(\boldsymbol{z} \in S\). We can also estimate the norm of \(\boldsymbol{z}\) by \[\left\Vert{\boldsymbol{z}}\right\Vert \le \left\Vert{t}\right\Vert + \mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V) \cdot |\rho_2| \le M \cdot (1 + \ell) \le (M+\ell)^2.\] It follows from 6 that \(s\xrightarrow{\sigma} q(\boldsymbol{z})\) in \(V\) for some \(\sigma\) with \[|\sigma| \le g(\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V,s,q(\boldsymbol{z})))^{k^2} \le (M + 3 \cdot \left\Vert{\boldsymbol{z}}\right\Vert)^{mk^2} \le (M + \ell)^{4mk^2}.\] Note that \(s \xrightarrow{\sigma\rho_2} t\) in \(V\), and hence, the length bound is given by \[\begin{align} \min \mathop{\operatorname{\mathrm{\mathrm{\small len}}}}\nolimits(V, s, t) &\le |\sigma| + |\rho_2|\le 2\cdot (M + \ell)^{4mk^2} \le (M + \ell)^{6mk^2} \le R(M+\ell). \end{align}\] The claim is proved. ◻

Proof. Clearly, \((V',s',t')\) is diagonal and \(s' \xrightarrow{*} q(\boldsymbol{y}) \xrightarrow{*} t'\) in \(V'\), given that \(\boldsymbol{\delta} \in P_0\). Recall that \(R(x)=x^{21mk^2}\). The size bound is derived as follows. \[\begin{align} \mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V',s',t') &\le M + 3\cdot\left\Vert{\boldsymbol{w}}\right\Vert + 3 \cdot(M + |T_{\boldsymbol{w}}|) \cdot (\left\Vert{T}\right\Vert+\left\Vert{T_{\boldsymbol{w}}}\right\Vert + 1)\\ &\le M + 6\cdot L_k(M)^{14mk^2} + 81 \cdot M^{4mk^2}\\ &\le 88L_k(M)^{14mk^2}\\ &\le R(L_k(M)). \end{align}\] We can similarly rearrange the shortest run \(\rho\) from \(s'\) to \(t'\) into a run \(s' \xrightarrow{\rho_1} q(\boldsymbol{z})\xrightarrow{\rho_2}t'\), where \(\boldsymbol{z} \in \boldsymbol{w} + P_0^* \subseteq S\) and \(\rho_2\) is also a run from \(q(\boldsymbol{z})\) to \(t\) in \(V\). We can also estimate the norm of \(\boldsymbol{z}\) by \[\left\Vert{\boldsymbol{z}}\right\Vert \le \left\Vert{t}\right\Vert + \mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V) \cdot |\rho_2|\le (M + |\rho|)^2.\] It follows from 6 that \(s\xrightarrow{\sigma} q(\boldsymbol{z})\) in \(V\) for some \(\sigma\) with \[|\sigma| \le g(\mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V,s,q(\boldsymbol{z})))^{k^2} \le \left(M +3 \cdot \left\Vert{\boldsymbol{z}}\right\Vert\right)^{mk^2} \le (M +|\rho|)^{4mk^2}.\] Note that \(s \xrightarrow{\sigma\rho_2} t\) in \(V\), and consequently, \[\min \mathop{\operatorname{\mathrm{\mathrm{\small len}}}}\nolimits(V, s, t) \le |\sigma| + |\rho_2| \le (M +|\rho|)^{6mk^2} \le R(M+|\rho|),\] where \(|\rho| = \min\mathop{\operatorname{\mathrm{\mathrm{\small len}}}}\nolimits(V',s',t')\). ◻

Proof. Let \(U:= R(\left\Vert{\boldsymbol{x}}\right\Vert + 1 + |Q| \cdot \left\Vert{T}\right\Vert, M)\), where \(R\) is given by 6. If there is a run \(\pi\) starting from \(s\) with \(\mathop{\operatorname{\mathrm{\mathrm{\small bd}}}}\nolimits(\pi, U) = \emptyset\), then by 6, there is a run \(s \xrightarrow{\rho} q(\boldsymbol{y})\) with \[\boldsymbol{y} \ge (\left\Vert{\boldsymbol{x}}\right\Vert + 1 + |Q| \cdot \left\Vert{T}\right\Vert) \cdot \boldsymbol{1} \ge \boldsymbol{x} + (1 + |Q| \cdot \left\Vert{T}\right\Vert)\cdot\boldsymbol{1}.\] Choose any simple path \(\sigma\) from \(q\) back to \(p\), and we have \(s \xrightarrow{\rho\sigma} p(\boldsymbol{y}')\), where \[\boldsymbol{y}':= \boldsymbol{y} + \mathop{\operatorname{\mathrm{\mathrm{\small eff}}}}\nolimits(\sigma) \ge \boldsymbol{x} + (1 + |Q| \cdot \left\Vert{T}\right\Vert)\cdot\boldsymbol{1} - |\sigma|\cdot \left\Vert{T}\right\Vert\cdot \boldsymbol{1} \ge \boldsymbol{x} + \boldsymbol{1}.\] Therefore \(s\) is diagonal in \(V\). ◻

Proof. It remains to show that \(\min \mathop{\operatorname{\mathrm{\mathrm{\small len}}}}\nolimits(V,s,t) \leq R(\ell + M)\). Assume that the shortest run in \((V',s',t')\) is given by \(s' \xrightarrow{\rho_1}p_2(\boldsymbol{z})\xrightarrow{\rho_2}t' = t\) where \(\rho_1\) contains only self-loops in \(T_S\) and \(\rho_2\) is a path of \(V\). Immediately, \(|\rho_1|+|\rho_2| = \ell\), which implies that \[\left\Vert{\boldsymbol{z}}\right\Vert \leq \left\Vert{t}\right\Vert + \mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V) \cdot \ell\le (M + \ell)^2.\] Let \(\boldsymbol{\lambda} \in \mathbb{N}^{n}\) be the vector such that \(\boldsymbol{\lambda}(i)\) is the number of occurrences of the transition \((q,\boldsymbol{p}_i, q)\) in \(\rho_1\). Then we have \(\boldsymbol{z} - \sum_{i = 1}^n \boldsymbol{\lambda}(i) \cdot \boldsymbol{p}_i \in \boldsymbol{b} + P_0^*\) and \[\langle {\boldsymbol{c},\boldsymbol{\lambda}} \rangle \le \left\Vert{\boldsymbol{c}}\right\Vert \cdot \sum_{i=1}^n \boldsymbol{\lambda}(i) \le \left\Vert{\boldsymbol{c}}\right\Vert \cdot |\rho_1| \le \left\Vert{\boldsymbol{c}}\right\Vert \cdot \ell \le K,\] which justifies that \(\boldsymbol{z} \in S\). This also implies that \(s\xrightarrow{*}p_2(\boldsymbol{z})\) in \(V\). The length of the shortest path for \((V,s,t)\) is bounded by \[\begin{align} \min\mathop{\operatorname{\mathrm{\mathrm{\small len}}}}\nolimits(V,s,t) &\leq \min\mathop{\operatorname{\mathrm{\mathrm{\small len}}}}\nolimits(V,s,p_2(\boldsymbol{z})) + \min\mathop{\operatorname{\mathrm{\mathrm{\small len}}}}\nolimits(V,p_2(\boldsymbol{z}),t) \\ &\leq \mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V,s,p_2(\boldsymbol{z}))^{3m^2} + \ell \\ &\leq (M + 3\cdot \left\Vert{\boldsymbol{z}}\right\Vert) ^ {3m^2} + \ell \\ &\leq (M + 3\cdot (M + \ell)^2) ^ {3m^2} + \ell \\ &\leq (M + \ell) ^{13m^2} \\ &\le R(M+\min\mathop{\operatorname{\mathrm{\mathrm{\small len}}}}\nolimits(V',s',t')), \end{align}\] bearing in mind that \(R(x)=x^{30m^2}\). ◻

Proof. Clearly, \((V',s',t')\) is a \((k{-}1)\)-component forward pumpable VASS with \(s' \xrightarrow{*} p_2(\boldsymbol{x}_2) \xrightarrow{\pi'} t'\) in \(V'\). The size bound is derived as follows. \[\begin{align} \mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V',s',t') &\le M + 3\cdot\left\Vert{\boldsymbol{w}}\right\Vert + 3 \cdot(M + |T_{\boldsymbol{w}}|) \cdot (\left\Vert{T}\right\Vert+\left\Vert{T_{\boldsymbol{w}}}\right\Vert + 1)\\ &\le M + 6\cdot L_k(M)^{25m^2} + 81 \cdot M^{12m^2}\\ &\le 88\cdot L_k(M)^{25m^2}\\ &\le R(L_k(M)). \end{align}\] It is routine to rearrange the shortest run \(\rho\) from \(s'\) to \(t'\) into a run \(s' \xrightarrow{\rho_1} p_2(\boldsymbol{z})\xrightarrow{\rho_2}t'\), where \(\boldsymbol{z} \in \boldsymbol{w} + P_0^* \subseteq S\) and \(\rho_2\) is also a run from \(p_2(\boldsymbol{z})\) to \(t\) in \(V\). Notice that \[\left\Vert{\boldsymbol{z}}\right\Vert \le \left\Vert{t}\right\Vert + \mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V) \cdot |\rho_2|\le (M + |\rho|)^2.\] Thus, by 8 , it follows that \(s\xrightarrow{\sigma} p_2(\boldsymbol{z})\) in \(V\) for some \(\sigma\) with \[|\sigma| \le \mathop{\operatorname{\mathrm{\mathrm{\small size}}}}\nolimits(V,s,q(\boldsymbol{z}))^{3m^2} \le \left(M +3 \cdot \left\Vert{\boldsymbol{z}}\right\Vert\right)^{3m^2} \le (M +|\rho|)^{12mk^2}.\] It follows from \(s \xrightarrow{\sigma\rho_2} t\) that \[\min \mathop{\operatorname{\mathrm{\mathrm{\small len}}}}\nolimits(V, s, t) \le |\sigma| + |\rho_2| \le (M +|\rho|)^{14m^2} \le R(M+\min\mathop{\operatorname{\mathrm{\mathrm{\small len}}}}\nolimits(V',s',t')),\] where \(|\rho| = \min\mathop{\operatorname{\mathrm{\mathrm{\small len}}}}\nolimits(V',s',t')\) by definition. ◻