# Complete Subhedge Projection for Stepwise Hedge Automata +
## 7 Congruence Projection
### Soundness
In this case, we can apply the induction hypothesis to \(Q_{1}\xrightarrow{h_{2}}Q^{\prime}\) wrt \(\Delta^{\text{det}}\), showing that there exists \(Q^{\prime\prime}\subseteq Q\), such that \((Q^{\prime}_{1},D)\xrightarrow{h_{2}}(Q^{\prime\prime},D)\) wrt \(\Delta^{\text{cgr}}\) and \((Q^{\prime},Q^{\prime\prime})\in dep^{\mu}(D)\). Hence, \((Q,D)\xrightarrow{h}(Q^{\prime\prime},D)\) wrt \(\Delta^{\text{cgr}}\) and \((Q^{\prime},Q^{\prime\prime})\in dep^{\mu}(D)\). This ends the proof of Claim 2.2a. **Proof of Inclusion**\(\mathcal{L}(A)\subseteq\mathcal{L}(A^{\text{cgr}(\mathbf{S})})\cap\mathbf{S}\). Since \(\mathbf{S}\) is a schema for \(A\), we have \(\mathcal{L}(A)\subseteq\mathbf{S}\), so that it is sufficient to show \(\mathcal{L}(A)\subseteq\mathcal{L}(A^{\text{cgr}(\mathbf{S})})\). Let \(h\in\mathcal{L}(A)\). Then, there exist \(q_{0}\in I\) and \(q\in F\), such that \(q_{0}\xrightarrow{h}q\) wrt \(\Delta\). Let \(Q=\{q\}\). Since \(A\) is deterministic, it follows that \(I\xrightarrow{h}Q\) wrt \(\Delta^{\text{det}}\). Using Claim 2.2a, this implies the existence of a subset of states \(Q^{\prime}\in\mathcal{Q}\), such that \((Q,Q^{\prime})\in dep^{\mu}(D)\) and \((I,D^{\prime}_{1},D^{\prime\prime}_{1})\xrightarrow{h}(Q^{\prime},D^{\prime \prime}_{init})\) wrt \(\Delta^{\text{cgr}}\). Furthermore, \((I,D^{\prime\prime}_{\text{in}}\mathcal{A}_{\text{F}_{8}})\in I^{\text{cgr}( \mathbf{S})}\). In order to prove \(h\in\mathcal{L}(A^{\text{cgr}(\mathbf{S})})\), it is thus sufficient to show that \((Q^{\prime},D^{\prime}_{init})\in F^{\text{cgr}(\mathbf{S})}\). We distinguish two cases:  
**Case \(Q^{\prime}\
ot\in dPr\hat{\Delta}(D^{A,F_{\mathsf{S}}}_{init})\)**. Condition (1\({}^{a}\)) of \((Q,Q^{\prime})\in dep^{a}(D)\), shows that \(Q\subseteq Q^{\prime}\) so that \(q\in Q^{\prime}\). Since \(q\in F\), it follows that \(Q^{\prime}\cap F\
eq\emptyset\). Thus, \((Q^{\prime},D^{A,F_{\mathsf{S}}}_{init})\in F^{\mathit{cgr}(\mathbf{S})}\), so that \(h\in\mathcal{L}(A^{\mathit{cgr}(\mathbf{S})})\). **Case \(Q^{\prime}\in dPr\hat{\Delta}(D^{A,F_{\mathsf{S}}}_{init})\)**. Condition (2\({}^{a}\)) of \((Q,Q^{\prime})\in dep^{a}(D)\) yields \(Q\subseteq acc^{\Delta}(Q^{\prime})\). Hence, \(q\in acc^{\Delta}(Q^{\prime})\cap F\) so that \((Q^{\prime},D^{A,F_{\mathsf{S}}}_{init})\in F^{\mathit{cgr}(\mathbf{S})}\), and thus, \(h\in\mathcal{L}(A^{\mathit{cgr}(\mathbf{S})})\). This ends the proof of the first inclusion. \(\square\)  
We next want to show the inverse inclusion \(\mathcal{L}(A^{\mathit{cgr}(\mathbf{S})})\cap\mathbf{S}\subseteq\mathcal{L}(A)\). It will eventually follow from the next two claims. **Claim 2.1b**. : For any hedge \(h\in\mathcal{H}_{\Sigma}\), difference relation \(D\subseteq\mathcal{D}^{\Delta}\), projection state \(Q\in dPr\hat{\Delta}(D)\) and state \(\mu\in\mathcal{Q}^{\mathit{cgr}}\): if \((Q,D)\xrightarrow{h}\mu\) wrt \(\Delta^{\mathit{cgr}}\), then \(\mu=(Q,D)\). Proof. : By induction on the structure of \(h\in\mathcal{H}_{\Sigma}\), suppose that \((Q,D)\xrightarrow{h}\mu\) wrt \(\Delta^{\mathit{cgr}}\):  
**Case \(h=\langle h^{\prime}\rangle\). **: There must exist states \(\mu_{1},\mu^{\prime}_{1}\in\mathcal{Q}^{\mathit{cgr}}\) closing the following diagram:  
Since \(Q\in dPr\hat{\Delta}(D)\), the following rule must have been applied to infer \((Q,D)\xrightarrow{\Diamond}\mu_{1}\) wrt \(\Delta^{\mathit{cgr}}\):  
\[\frac{Q\in dPr\hat{\Delta}(D)}{(Q,D)\xrightarrow{\Diamond}(Q,D)\text{ in } \Delta^{\mathit{cgr}}}\]  
Therefore, \(\mu_{1}=(Q,D)\). The induction hypothesis applied to \((Q,D)\xrightarrow{h^{\prime}}\mu^{\prime}_{1}\) wrt \(\Delta^{\mathit{cgr}}\) shows that \(\mu^{\prime}_{1}=(Q,D)\), too.