# Complete Subhedge Projection for Stepwise Hedge Automata +
## 5 Subhedge Projection
### Completeness for Subhedge Projection  
Before defining when a Sha\({}^{\perp}\) is complete for subhedge projection, we show that subhedge projection states in runs of deterministic Shas may only occur at irrelevant prefixes. **Proposition 2**. : _Let \(A=(\Sigma,\mathcal{Q},\Delta,I,F)\) be a \(\textsc{{d}}\textsc{{Sha}}^{\perp}\) with schema \(\mathbf{S}\), \(R\in run^{\Delta}(h)\) is the run of \(compl(A)\) on some hedge \(h\in\mathbf{S}\), and \(q\) is a subhedge projection state for \(\Delta\). Then, for any prefix \(r\cdot q\) of \(nw(R)\), the prefix \(proj_{\Sigma}(r)\) of \(nw(h)\) is subhedge irrelevant for \(\mathcal{L}(A)\) for schema \(\mathbf{S}\)._  
Proof. : Let \(R\in run^{\Delta}(h)\) be the unique run of \(compl(A)\) on a hedge \(h\in\mathbf{S}\). Suppose that \(r\cdot q\cdot s=nw(R)\) for some subhedge projection states \(q\) of \(\Delta\) and let \(v=proj_{\Sigma}(r)\) and \(w=proj_{\Sigma}(s)\). Since \(v\cdot w=nw(h)\) and \(h\in\mathbf{S}\), it follows that \(v\cdot w\in nw(\mathbf{S})\). We fix some hedge \(h^{\prime}\in\mathcal{H}_{\Sigma}\), such that \(v\cdot nw(h^{\prime})\cdot w\in nw(\mathbf{S})\) arbitrarily. Let \(\tilde{h}\in\mathcal{H}_{\Sigma}\), such that \(nw(\tilde{h})=v\cdot nw(h^{\prime})\cdot w\). For the subhedge irrelevance of \(v\), we must show that  
\[h\in\mathcal{L}(A)\Leftrightarrow\tilde{h}\in\mathcal{L}(A).\]  
\"\(\Rightarrow\)\": We suppose that \(h\in\mathcal{L}(A)\) and have to show that \(\tilde{h}\in\mathcal{L}(A)\). For the partial run \(r\cdot q\) of \(A\) on \(\tilde{h}\), there must exist \(R^{\prime}\) and \(p\), such that \(q\cdot R^{\prime}\cdot p\in run^{\Delta}(h^{\prime})\). Since \(q\) is a subhedge projection state of \(\Delta\), it follows by Lemma 6 that \(q=p\). Hence, \(r\cdot q\cdot nw(R^{\prime})\cdot q\cdot s\) is a run of \(A\) on \(\tilde{h}\). Since \(R\) was successful for \(A\), \(s\) must end in \(F\); thus, the above run on \(\tilde{h}\) is successful for \(A\) too. Hence, \(\tilde{h}\in\mathcal{L}(A)\), as we have shown. \"\(\Leftarrow\)\": We suppose that \(\tilde{h}\in\mathcal{L}(A)\) and have to show that \(h\in\mathcal{L}(A)\). Let \(\tilde{R}\) be the unique run of \(compl(A)\) on \(\tilde{h}\). By determinism, \(\tilde{R}\) must have the prefix \(r\cdot q\). So, there exist \(R^{\prime},p^{\prime},s\), such that \(p\cdot R^{\prime}\cdot q\in run^{\Delta}(h^{\prime})\) and \(r\cdot q\cdot R^{\prime}\cdot p\cdot s=\tilde{R}\). Lemma 6 shows that \(p=q\). Hence, \(r\cdot q\cdot s\) is the unique run of \(compl(A)\) on \(h\) and this run is accepting. So, \(h\in\mathcal{L}(A)\). We note that Proposition 2 would not hold without assuming determinism. To see this, we can add some sink to any dSha as a second initial state. One can then always go to this sink, which is a subhedge projection state. Nevertheless, no prefix going to the sink may be subhedge irrelevant. Proposition 2 shows that subhedge projection states permit distinguishing prefixes that are subhedge irrelevant for deterministic Sha\({}^{\perp}\)s. An interesting question is whether all subhedge irrelevant prefixes can be found in this way. A closely related question is whether, for all regular patterns, there exist dShas that project all irrelevant subhedges. **Example 6**. : _Reconsider Example 3 with \(\Sigma=\{a\}\), a regular pattern \(L=\{\langle a\rangle\}\), and a regular schema \(\mathbf{S}=L\cup\{\langle\rangle\cdot a\}\). The prefix \(\langle\rangle\) is irrelevant for \(L\) and \(\mathbf{S}\), since all its continuations ending in the schema are rejected: there is only one such continuation, which is \(\langle\rangle\cdot a\). However, a dSha for \(L\) and \(\mathbf{S}\) with maximal subhedge projection is given in Figure 17 but will not go into a subhedge projection state at this prefix. The reason is that it will go into the same state \(\{3,4\}D0\) for any prefix in \(\langle\mathcal{N}_{\Sigma}\rangle\), ignoring the nested word of the irrelevant subhedge. Therefore, this state must accept \(\langle a\rangle\).