# Complete Subhedge Projection for Stepwise Hedge Automata +
## 5 Subhedge Projection
### Subhedge Projection States  
Intuitively, a subhedge projection state can only loop in itself until a hedge closes (and then it is applied). When going down into a subtree, the subhedge projection state may still be changed into some other looping state. When leaving the subtree, however, one must come back to the original subhedge projection state. Clearly, any sink is a subhedge projection state. The even more interesting cases, however, are subhedge projection states that are not sinks.  
We start with Sha\({}^{\downarrow}\)s without any restrictions but will impose schema-completeness and determinism later on.  
**Definition 7**.: _We call a state \(q\in\mathcal{Q}\) a subhedge projection state of \(\Delta\) if there exists \(q^{\prime}\in\mathcal{Q}\) called the witness of \(q\), such that the set of transition rules of \(\Delta\) containing \(q^{\prime}\) or \(q\) on the leftmost position is included in the following set:_  
\[\begin{array}{l}\{q\stackrel{{\searrow}}{{\to}}q^{\prime},\ q \bar{q}q^{\prime}\to q,\ q^{\prime}\stackrel{{\searrow}}{{\to}}q^{ \prime},\ q^{\prime}\bar{q}q^{\prime}\to q^{\prime}\}\\ \cup\{q^{\prime}\stackrel{{ a}}{{\to}}q^{\prime},\ q\stackrel{{ a}}{{\to}}q\mid a\in\Sigma\}\end{array}\]  
_The set of all subhedge projection states of \(\Delta\) is denoted by \(\mathcal{Q}^{\Delta}_{\mathit{shp}}\)._  
For any complete Sha\({}^{\downarrow}\), the above set of transition rules must be equal to the set of all transition rules of \(\Delta\) with \(q\) or \(q^{\prime}\) on the leftmost position. But, if the Sha\({}^{\downarrow}\) is only schema-complete for some schema \(\mathbf{S}\), then not all these transitions must be present. Note also that a subhedge projection state \(q\) may be equal to its witness \(q^{\prime}\). Therefore, any witness \(q^{\prime}\) of some subhedge projection state is itself a subhedge projection state with witness \(q^{\prime}\).  
In the example \(\textsc{dSha}^{\downarrow}\,A=(\Sigma,\mathcal{Q},\Delta,I,F)\) in Figure 7, we have \(\mathcal{Q}^{\Delta}_{\mathit{shp}}=\{\Pi,4,2^{\prime},3^{\prime},1^{\prime \prime},2^{\prime\prime}\}\). The witness of all these subhedge projection states is \(\Pi\). Note that not all possible transitions are present for the states in \(\mathcal{Q}^{\Delta}_{\mathit{shp}}\setminus\{\Pi\}\), given that this automaton is not complete (but still schema-complete for schema \([\mathsf{doc}]\)).  
**Lemma 6**.: _If \(q\in\mathcal{Q}^{\Delta}_{\mathit{shp}}\) is a subhedge projection state and \(q\stackrel{{ h}}{{\to}}p\) wrt \(\Delta\), then \(q=p\)._  
Proof.: Suppose that \(q\stackrel{{ h}}{{\to}}p\) wrt \(\Delta\) and that \(q\) is a subhedge projection state of \(\Delta\) with witness \(q^{\prime}\). So, the only possible transitions with \(q\) or \(q^{\prime}\) on the left-hand side are the following:  
Suppose that \(h=t_{1}\cdot\ldots\cdot t_{n}\) is a sequence of trees or letters \(t_{i}\in\langle\mathcal{H}_{\Sigma}\rangle\cup\Sigma\), where \(1\leq i\leq n\). Then, there exists runs \(R_{i}\in\mathit{run}^{\Delta}(t_{i})\) and a run \(R\in\mathit{run}^{\Delta}(h)\) that has the form \(h=q_{0}\cdot R_{1}\cdot q_{1}\cdot\ldots\cdot R_{n}\cdot q_{n}\), where \(q_{0}=q\) and \(q_{n}=p\). We prove for all \(0\leq i\leq n\) that \(q_{i}=q\) by induction on \(i\). For \(i=0\), this is trivial. For \(i>0\), the induction hypothesis shows that \(q_{i-1}=q\).  
**Case \(t_{i}=a\in\Sigma\).**: Then, \(q_{i-1}\stackrel{{ a}}{{\to}}q_{i}\) in \(\Delta\). Since \(q_{i-1}=q\) is a subhedge projection state of \(\Delta\), it follows that \(q_{i}=q\), too.
**Case \(t_{i}=\langle h^{\prime}\rangle\) for some \(h^{\prime}\in\mathcal{H}_{\Sigma}\).**: Since \(q_{i-1}=q\) is a subhedge projection state of \(\Delta\) with witness \(q^{\prime}\), the subrun of \(R\) recognizing \(t_{i}\) must be justified by the following diagram:  
So, the subrun of \(R\) of \(h^{\prime}\) may only contain the witness \(q^{\prime}\) and, furthermore, \(q_{i}=q\).