# Complete Subhedge Projection for Stepwise Hedge Automata +
## 7 Congruence Projection
### Completeness  
We next show the completeness of congruence projection for subhedge projection according to Definition 10. Let \(A=(\Sigma,\mathcal{Q},\Delta,I,F)\) be a complete dSha and \(F\subseteq F_{\mathbf{S}}\subseteq\mathcal{Q}\). Automaton \(A\) defines the regular pattern \(L=\mathcal{L}(A)\) with the schema-final states in \(F_{\mathbf{S}}\) the regular schema \(\mathbf{S}=\mathcal{L}(A[F/F_{\mathbf{S}}])\). We first show that all subhedge irrelevant states of difference relations are subhedge projection states \(A^{\text{cgr}(\mathbf{S})}\) according to Definition 7. **Lemma 14**. : _If \(Q\in\text{dPrj}^{\Delta}(D)\), then \((Q,D)\) is a subhedge projection state of \(\Delta^{\text{cgr}}\) with witness \((Q,D)\)._  
Proof. : We assume that \(q\in\text{dPrj}^{\Delta}(D)\) and have to show that \((Q,D)\) is a subhedge projection state of \(\Delta^{\text{cgr}}\). We have to show that all transition rules starting with \((Q,D)\) are permitted for a subhedge projection state \((Q,D)\) with \((Q,D)\). They are generated by the following rules, all of which are looping:  
\[ \begin{array}{c}a\in\Sigma\quad Q\in\text{dPrj}^{\Delta}(D)\\ \hline(Q,D)\xrightarrow{a}(Q,D)\text{ in }\Delta^{\text{cgr}}\end{array} \frac{Q \in\text{dPrj}^{\Delta}(D)}{(Q,D)\texttt{@}(Q,D)\rightarrow(Q,D)\text{ in }\Delta^{\text{cgr}}}\ \frac{Q\in\text{dPrj}^{\Delta}(D)}{(Q,D) \xrightarrow{\langle}(Q,D)\text{ in }\Delta^{\text{cgr}}}\end{array}\]  
So, if a partial run of \(A^{\text{cgr}(\mathbf{S})}\) on a prefix \(u\) assigns some state \((P,D)\) with \(P\in\text{dPrj}^{\Delta}(D)\), then \((P,D)\) is a subhedge projection state by Lemma 14, and thus, subhedge irrelevant by Proposition 2. **Lemma 15**. : _Let \(A^{\prime}=A[I/\langle\rangle^{\Delta}]\), \(L^{\prime}=\mathcal{L}(A^{\prime})\), and \(\mathcal{S}^{\prime}=\mathcal{L}(A^{\prime}[F/F_{\mathbf{S}}])\). If \((\langle\rangle^{\Delta},D)\xrightarrow{hdg(u)}(Q,D)\) wrt \(A^{\text{cgr}(\mathbf{S})}\) for some nested word \(u\in\mathcal{N}_{\Sigma}\) and either_  
* \(Q\
ot\in\text{dPrj}^{\Delta}(D)\) _and_ \(q\in Q\)_, or_
* \(Q\in\text{dPrj}^{\Delta}(D)\) _and_ \(q\in acc^{\Delta}(Q)\)_,_  
_then there exists a nested word \(u^{\prime}\in class^{L^{\prime}}_{\mathcal{S}^{\prime}}(u)\) and \(q_{0}\in\langle\rangle^{\Delta}\), such that \(q_{0}\xrightarrow{hdg(u^{\prime})}q\) wrt \(\Delta\)._  
Proof. : By induction on the length of \(u\), suppose that \((\langle\rangle^{\Delta},D)\xrightarrow{hdg(u)}(Q,D)\) wrt \(A^{\text{cgr}(\mathbf{S})}\). In the base case, we have \(u=\varepsilon\). Hence, \(Q=\langle\rangle^{\Delta}\). **Case \(Q\
ot\in\text{dPrj}^{\Delta}(D)\)** and \(q\in Q\). Then, \(\langle\rangle^{\Delta}=\{q\}\). The unique run of \(A^{\prime}\) on \(u=\varepsilon\) starts and ends in the tree initial state \(q\in\langle\rangle^{\Delta}\). **Case \(Q\in\text{dPrj}^{\Delta}(D)\)** and \(q\in acc^{\Delta}(Q)\). Since \(Q\in\text{dPrj}^{\Delta}(D)\), Lemma 14 shows that \((Q,D)\) is a subhedge projection state, so that \(\varepsilon\) is subhedge irrelevant for \(L^{\prime}\) and \(\mathbf{S}^{\prime}\) by Proposition 2. Hence, \(class^{L^{\prime}}_{\mathcal{S}^{\prime}}(\varepsilon)=\mathcal{N}_{\Sigma}\). Furthermore, since \(q\in acc^{\Delta}(Q)\), there exists a hedge \(h\) and \(q_{0}\in I\), such that \(q_{0}\xrightarrow{h}q\) wrt \(\Delta\). Let \(u^{\prime}=nw(h)\). The run of \(A\) on \(u^{\prime}\) ends in \(q\) and \(u^{\prime}\in class^{L^{\prime}}_{\mathcal{S}^{\prime}}(u)\). For the induction step, we distinguish the possible forms of the nested word \(u\). So, there exist \(\tilde{u},v\in\mathcal{N}_{\Sigma}\) and \(a\in\Sigma\), such that either of the following cases holds:  
**Case \(u=\tilde{u}\cdot\langle\cdot v\cdot\rangle\)**. Let \((\tilde{Q},D)\) be the state in which the run of \((A^{\prime})^{\text{cgr}(\mathbf{S})}\) on \(\tilde{u}\) ends. **Subcase \(\tilde{Q}\
ot\in\text{dPrj}^{\Delta}(D)\)**. Let \(D^{\prime}=D_{\tilde{Q}}\).