# Complete Subhedge Projection for Stepwise Hedge Automata +
## 7 Congruence Projection
### Completeness
Then, there exist \(P\subseteq\mathcal{Q}\), such that \((\langle\rangle^{\Delta},D^{\prime})\xrightarrow{v}(P,D^{\prime})\) wrt \(A^{\text{cgr}(\mathbf{S})}\). So, the run of \((A^{\prime})^{\text{cgr}(\mathbf{S})}\) on \(v\) goes to state \((P,D^{\prime})\). **Subsubcase \(P\in\text{dPrj}^{\Delta}(D^{\prime})\)**. By construction of \(A^{\text{cgr}(\mathbf{S})}\), we then have \(Q=\tilde{Q}\texttt{@}^{\Delta}acc^{\Delta}(P)\). Since \(q\in Q\), there exist \(\tilde{q}\in\tilde{Q}\) and \(p\in acc^{\Delta}(P)\), such that \(\tilde{q}\texttt{@}p\rightarrowq\) in \(\Delta\). By induction hypothesis, there exists \(v^{\prime}\in class^{L^{\prime}}_{\mathcal{S}^{\prime}}(v)\), suchthat the run of \(A^{\prime}\) on \(v^{\prime}\) ends in \(p\). Hence, the run of \(A\) on \(u^{\prime}=\tilde{u}\cdot\langle\cdot v^{\prime}\cdot\rangle\) ends in \(q\), and furthermore, \(u^{\prime}\in class^{L}_{\mathbb{S}}(u)\). **Subsubcase**\(P\
ot\in dPr\tilde{\pi}^{\Delta}(D^{\prime})\). By construction of \(A^{\mathit{cgr}(\mathbb{S})}\), we then have \(Q=\tilde{Q}@^{\Delta}P\). Since \(q\in Q\), there exist \(\tilde{q}\in\tilde{Q}\) and \(p\in P\), such that \(\tilde{q}@p\to q\) in \(\Delta\). By induction hypothesis, there exists \(v^{\prime}\in class^{L}_{\mathbb{S}}(v)\), such that the run of \(A^{\prime}\) on \(v^{\prime}\) ends in \(p\). Hence, the run of \(A\) on \(u^{\prime}=\tilde{u}\cdot\langle\cdot v^{\prime}\cdot\rangle\) ends in \(q\), and furthermore, \(u^{\prime}\in class^{L}_{\mathbb{S}}(u)\). **Subcase**\(\tilde{Q}\in dPr\tilde{\pi}^{\Delta}(D)\). Then, \(Q=\tilde{Q}\) and \(q\in acc^{\Delta}(\tilde{Q})\). Using the induction hypothesis applied to \(\tilde{u}\), there exists \(\tilde{u}^{\prime}\in class^{L}_{\mathbb{S}}(\tilde{u})\), such that \(\langle\rangle^{\Delta}\xrightarrow{\mathit{hdg}(a^{\prime})}q\). Since \(\tilde{u}\) is irrelevant for \(L\) and \(\mathbb{S}^{\prime}\), we have \(\tilde{u}^{\prime}\in class^{L}_{\mathbb{S}}(u)\). **Case**\(u=\tilde{u}\cdot a\). This is easier to achieve than the previous cases and is thus omitted. **Lemma 16**. : _A partial run of \(A^{\mathit{cgr}(\mathbb{S})}\) assigns a state \((Q,D)\) to a prefix \(u\in\mathit{prefs}(\mathcal{N}_{\Sigma})\). If \(Q\
ot\in dPr\tilde{\pi}^{\Delta}(D)\) and \(q\in Q\), then there exists a prefix \(u^{\prime}\in class^{L}_{\mathbb{S}}(u)\), such that a partial run of \(A\) assigns state \(q\) to \(u^{\prime}\)._  
Proof. : By induction on the length of \(u\). In the base case, we have \(u=\varepsilon\). The partial run of \(A^{\mathit{cgr}(\mathbb{S})}\) on \(u\) assigns state \((Q,D)\), where \(Q=I\) and \(D=D^{A,F_{\mathbb{S}}}_{init}\). Suppose that \(Q\
ot\in dPr\tilde{\pi}^{\Delta}(D)\) and \(q\in Q\). Then, \(I=\{q\}\). The unique partial run of \(A\) on \(u=\varepsilon\) ends in the initial state \(q\in I\). For the induction step, let \(A^{\prime}=A[I/\langle\rangle^{\Delta}]\), \(L^{\prime}=\mathcal{L}(A^{\prime})\), and \(\mathbb{S}^{\prime}=\mathcal{L}(A^{\prime}[F/F_{\mathbb{S}}]\). We distinguish the possible forms of \(u\). So, \(\tilde{u}\in\mathit{prefs}(\mathcal{N}_{\Sigma})\), \(v\in\mathcal{N}_{\Sigma}\), and \(a\in\Sigma\) exist, such that either of the following hold:  
**Case**\(u=\tilde{u}\cdot\langle\cdot v\cdot\rangle\). Let \((\tilde{Q},\tilde{D})\) be the state in which the partial run of \(A^{\mathit{cgr}(\mathbb{S})}\) on \(\tilde{u}\) ends. From \(Q\
ot\in dPr\tilde{\pi}^{\Delta}(D)\), it follows that \(\tilde{Q}\
ot\in dPr\tilde{\pi}^{\Delta}(\tilde{D})\). Furthermore, \((\langle\rangle^{\Delta},D)\xrightarrow{v}(Q,D)\) wrt \(A^{\mathit{cgr}(\mathbb{S})}\). So, the partial run of \((A^{\prime})^{\mathit{cgr}(\mathbb{S})}\) on \(v\) goes to state \((Q,D)\). Using the induction hypothesis, there exists \(v^{\prime}\in class^{L^{\prime}}_{\mathbb{S}}(v)\), such that the partial run of \(A^{\prime}\) on \(v^{\prime}\) ends in \(q\). Hence, the partial run of \(A\) on \(u^{\prime}=\tilde{u}\cdot\langle\cdot v^{\prime}\) ends in \(q\), and furthermore, \(u^{\prime}\in class^{L}_{\mathbb{S}}(u)\).