# Complete Subhedge Projection for Stepwise Hedge Automata +
## 7 Congruence Projection
### Completeness
: Induction on the number of dangling opening parenthesis of \(u\). In the base case, \(u\) does not have any dangling opening parenthesis so \(u\in\mathcal{N}_{\Sigma}\) is a nested word. In this case, \(D=D^{A,F_{\mathbf{S}}}_{init}\). So, \(A^{\text{cgr}(\mathbf{S})}\) has a partial run on nested word \(u\in\mathcal{N}_{\Sigma}\) to \((P,D^{A,F_{\mathbf{S}}}_{init})\), where \(P\subseteq\mathcal{Q}\). Let \((p^{\prime},p^{\prime\prime})\in P^{2}\), \((r^{\prime},r^{\prime\prime  
such that \((p^{\prime}_{1},p^{\prime\prime}_{1})\in(P_{1})^{2}\), \(p^{\prime}_{1}\)\(\frac{hdg(v^{\prime}_{1})}{r^{\prime}_{1}}\), \(p^{\prime}_{1}\)\(\frac{hdg(v^{\prime\prime}_{1})}{r^{\prime\prime}_{1}}\), and \((r^{\prime}_{1},r^{\prime\prime}_{1})\in D\), there exist \((u^{\prime}_{1},u^{\prime\prime}_{1})\in\mathit{class}_{\mathbf{S}}^{\mathbf{ L}}(u_{1})\), \(w_{1}\in\mathit{suffix}(\mathcal{N}_{\Sigma})\), \(q^{\prime}\
ot\in_{\mathbf{F}_{\mathbf{S}}}^{F}q^{\prime\prime}\), and \(q_{0}\in I\), such that  
\[q_{0}\xrightarrow{hdg(u^{\prime}_{1}\cdot v^{\prime}_{1},w_{1})}q^{\prime}\ \mathrm{wrt}\ \Delta\ \wedge\ q_{0}\xrightarrow{hdg(u^{\prime\prime}_{1}\cdot u^{\prime\prime}_{1},w_{1})}q^{\prime\prime}\ \mathrm{wrt}\ \Delta\]  
Let \(u^{\prime}=u^{\prime}_{1}\cdot(\cdot\cdot u^{\prime}_{2}\), \(u^{\prime\prime}=u^{\prime\prime}_{1}\cdot(\cdot u^{\prime\prime}_{2}\), and \(w=\)\cdot w_{1}\). The above then yields the following:  
\[q_{0}\xrightarrow{hdg(u^{\prime}\cdot v^{\prime\prime}\cdot w)}q^{\prime}\ \mathrm{wrt}\ \Delta\ \wedge\ q_{0}\xrightarrow{hdg(u^{\prime\prime}\cdot v^{\prime\prime}\cdot w )}q^{\prime\prime}\ \mathrm{wrt}\ \Delta\]  
Furthermore, \((u^{\prime},u^{\prime\prime})\in(\mathit{class}_{\mathbf{S}}^{\mathbf{L}}(u))^{2}\), so this was to be shown. **Proposition 6**. : _Let \(A=(\Sigma,Q,\Delta,I,F)\) a \(d\mathit{SHA}\), \(F\subseteq F_{\mathbf{S}}\subseteq\mathcal{Q}\), \(L=\mathcal{L}(A)\), and \(\mathbf{S}=\mathcal{L}(A[F/F_{\mathbf{S}}])\). If \(A^{\mathit{cgr}(\mathbf{S})}\) has a partial run on prefix \(u\in\mathit{prefs}(\mathcal{N}_{\Sigma})\) to some state \((P,D)\in 2^{Q}\times\mathcal{D}^{\Delta}\) so that \(P\
ot\in d\mathit{PP}^{\Delta}(D)\), then \(\mathit{class}_{\mathbf{S}}^{\mathbf{L}}(u)\) is subedge relevant for \(L\)\(\mathrm{wrt}\ \mathbf{S}\)._  
Proof. : Suppose that \(A^{\mathit{cgr}(\mathbf{S})}\) has a partial run on prefix \(u\in\mathit{prefs}(\mathcal{N}_{\Sigma})\) to some state \((P,D)\in 2^{Q}\times\mathcal{D}^{\Delta}\) so that \(P\
ot\in d\mathit{PP}^{\Delta}(D)\). Since \(P\
ot\in d\mathit{PP}^{\Delta}(D)\), there exist \(acc^{\Delta}(P)^{2}\cap D\
eq\mathit{empryset}\). So, there exist \((p^{\prime},p^{\prime\prime})\in P^{2}\), \((r^{\prime},r^{\prime\prime})\in D\), and \((r^{\prime},v^{\prime\prime})\in\mathcal{N}_{\Sigma}^{2}\), such that  
\[p^{\prime}\xrightarrow{hdg(v^{\prime})}r^{\prime}\ \mathrm{wrt}\ \Delta\ \wedge\ p^{\prime\prime}\xrightarrow{hdg(v^{\prime\prime})}r^{\prime\prime}\ \mathrm{wrt}\ \Delta\]  
Using Lemma 17, there exist \((u^{\prime},u^{\prime\prime})\in\mathit{class}_{\mathbf{S}}^{\mathbf{L}}(u)\), \(w\in\mathit{suffix}(\mathcal{N}_{\Sigma})\), \(q^{\prime}\
ot\in_{\mathbf{F}_{\mathbf{S}}}^{F}q^{\prime\prime}\), and \(q_{0}\in I\), such that  
\[q_{0}\xrightarrow{hdg(u^{\prime}\cdot v^{\prime}\cdot w)}q^{\prime}\ \mathrm{wrt}\ \Delta\ \wedge\ q_{0}\xrightarrow{hdg((u^{\prime\prime}\cdot v^{\prime\prime}\cdot w ))}q^{\prime\prime}\ \mathrm{wrt}\ \Delta\]  
Hence, \(\mathit{class}_{\mathbf{S}}^{L}(u)\) is relevant for \(L\)\(\mathrm{wrt}\ \mathbf{S}\). **Theorem 3** (Completeness of congruence projection.). : _For any complete \(d\mathit{SHA}\)\((\Sigma,Q,\Delta,I,F)\) and set \(F\subseteq F_{\mathbf{S}}\subseteq\mathcal{Q}\), the congruence projection \(A^{\mathit{cgr}(\mathbf{S})}\) is sound and complete for subbedge projection for the regular pattern \(\mathcal{L}(A)\)\(\mathrm{wrt}\) the regular schema \(\mathbf{S}=\mathcal{L}(A[F_{\mathbf{S}}/F])\)._  
Proof. : The soundness of congruence projection is shown in Theorem 2.