# Complete Subhedge Projection for Stepwise Hedge Automata +
## 7 Congruence Projection
### Completeness
**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}(P,D)\) wrt \(A^{\mathit{cgr}(\mathbb{S})}\) for some \(P\subseteq Q\). **Subcase**\(P\in dPr\tilde{\pi}^{\Delta}(D)\). Then, \(Q=\tilde{Q}@\Delta acc^{\Delta}(P)\). So, there exists \(\tilde{q}\in Q\) and \(p\in acc^{\Delta}(P)\), such that \(\tilde{q}@p\to q\) in \(\Delta\). Using Lemma 15, there exists \(v^{\prime}\in class^{L^{\prime}}_{\mathbb{S}^{\prime}}(v)\), such that \(\langle\rangle^{\Delta}\xrightarrow{\mathit{hdg}(v^{\prime})}p\) wrt \(\Delta\). Using the induction hypothesis applied to \(\tilde{u}\), there exists an initial state \(q_{0}\in I\) and a prefix \(\tilde{u}^{\prime}\in class^{L}_{\mathbb{S}}(\tilde{u})\), such that the partial run of \(A\) on \(\tilde{u}^{\prime}\) goes on to state \(\tilde{q}\). Hence, the partial run of \(A\) on \(u^{\prime}=\tilde{u}^{\prime}\cdot\langle\cdot v^{\prime}\cdot\rangle\) goes on to \(q\) and \(u^{\prime}\in class^{L}_{\mathbb{S}}(u)\). **Subcase**\(P\
ot\in dPr\tilde{\pi}^{\Delta}(D)\). Then, \(Q=\tilde{Q}@\Delta Arc^{\Delta}(P)\). So, there exists \(\tilde{q}\in Q\) and \(p\in P\), such that \(\tilde{q}@p\to q\) in \(\Delta\). Using Lemma 15, there exists \(v^{\prime}\in class^{L^{\prime}}_{\mathbb{S}^{\prime}}(v)\), such that \(\langle\rangle^{\Delta}\xrightarrow{\mathit{hdg}(v^{\prime})}p\) wrt \(\Delta\). Using the induction hypothesis applied to \(\tilde{u}\), there exists an initial state \(q_{0}\in I\) and a prefix \(\tilde{u}^{\prime}\in class^{L}_{\mathbb{S}}(\tilde{u})\), such that the partial run of \(A\) on \(\tilde{u}^{\prime}\) goes on to state \(\tilde{q}\). Hence, the partial run of \(A\) on \(u^{\prime}=\tilde{u}^{\prime}\langle\cdot\langle\cdot v^{\prime}\cdot\rangle\) goes on to \(q\) and \(u^{\prime}\in class^{L}_{\mathbb{S}}(u)\). **Subcase**\(u=\tilde{u}\cdot a\). This is easier to achieve than the previous case and is thus omitted. The next lemma states the key invariant of congruence projection, which eventually proves its completeness for subhedge projection. For this, we define for any \(F\subseteq F_{\mathbf{S}}\subseteq F\) the binary relation \(\
ot\approx^{F}_{F_{\mathbf{S}}}\) as the symmetric closure of \(F\times(F_{\mathbf{S}}\setminus F)\), i.e., for all \((q^{\prime},q^{\prime\prime})\in\mathcal{Q}^{2}\):  
\[q^{\prime}\
ot\approx^{F}_{F_{\mathbf{S}}}q^{\prime\prime}\Leftrightarrow \left\{ \begin{array}{lcl}(q^{\prime}\in F&\wedge&q^{\prime\prime}\in F_{ \mathbf{S}}\setminus F)&\vee\\ (q^{\prime}\in F_{\mathbf{S}}\setminus F&\wedge&q^{\prime\prime}\in F&)\end{array} \right.\]  
**Lemma 17** (Key Invariant). : _Let \(A=(\Sigma,\mathcal{Q},\Delta,I,F)\) a \(d\)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^{\text{cgr}(\mathbf{S})}\) has a partial run on prefix \(u\in\text{prefs}(\mathcal{N}_{\Sigma})\) to state \((P,D)\in 2^{\mathcal{Q}}\times\mathcal{D}^{\Delta}\), then for all \((p^{\prime},p^{\prime\prime})\in P^{2}\), \((r^{\prime},r^{\prime\prime})\in D\), and \((v^{\prime},v^{\prime\prime})\in\mathcal{N}_{\Sigma}^{2}\), such that_  
\[p^{\prime}\xrightarrow{\text{hdg}(v^{\prime})}r^{\prime}\text{ wrt }\Delta\ \wedge\ p^{\prime\prime}\xrightarrow{\text{hdg}(v^{\prime\prime})}r^{\prime \prime}\text{ wrt }\Delta\]  
_there exist \((u^{\prime},u^{\prime\prime})\in\text{class}^{L}_{\mathbf{S}}(u)\), \(w\in\text{suffs}(\mathcal{N}_{\Sigma})\), \(q^{\prime}\
ot\approx^{F}_{F_{\mathbf{S}}}q^{\prime\prime}\), and \(q_{0}\in I\) such that_  
\[q_{0}\xrightarrow{\text{hdg}(u^{\prime}\cdot v^{\prime}\cdot w)}q^{\prime} \text{ wrt }\Delta\ \wedge\ q_{0}\xrightarrow{\text{hdg}(u^{\prime\prime}\cdot v^{\prime\prime} \cdot w)}q^{\prime\prime}\text{ wrt }\Delta\]  
Proof.