# Complete Subhedge Projection for Stepwise Hedge Automata +
## 7 Congruence Projection
### Soundness
\(\Delta^{det}\). Since \(D^{\prime}\subseteq down^{\Delta}_{Q}(D)\) and \((P^{\prime}\times P^{\prime\prime})\cap D^{\prime}=\emptyset\), it follows from \(Q@P^{\prime\prime}\to Q^{\prime}\) and \(Q@P^{\prime\prime}\to Q^{\prime\prime}\) wrt. \(\Delta^{det}\) that \((Q^{\prime}\cap Q^{\prime\prime})\cap D=\emptyset\). That is, condition \((0^{b})\) of \((Q^{\prime},Q^{\prime\prime})\in dep^{b}(D)\). Since \(P^{\prime}\
ot\in dPrj^{\Delta}(D^{\prime})\), condition \((1^{b})\) of \((P^{\prime},P^{\prime\prime})\in dep^{b}(D^{\prime})\) is \(P^{\prime\prime}\subseteq P^{\prime}\). From \(Q@P^{\prime\prime}\to Q^{\prime\prime}\) and \(Q@P^{\prime}\to Q^{\prime}\), it thus follows that \(Q^{\prime\prime}\subseteq Q^{\prime}\). Hence, conditions \((1^{b})\) and \((2^{b})\) of \((Q^{\prime},Q^{\prime\prime})\in dep^{b}(D)\) are valid, so that \((Q^{\prime},Q^{\prime\prime})\in dep^{b}(D)\) holds. Furthermore,  
This shows that \(Q\xrightarrow{\langle H^{\prime}\rangle}Q^{\prime\prime}\) wrt \(\Delta\). The other two requirements of the claim, \(\mu=(Q^{\prime},D)\) and \((Q^{\prime},Q^{\prime\prime})\in dep^{b}(D)\), were shown earlier. **Case \(h=a\). **: Since \(Q\
ot\in dPr\hat{\gamma}^{\Delta}(D)\), the following inference rule must be used:  
\[\frac{Q\xrightarrow{a}Q^{\prime}\text{ in }\Delta\quad Q\
ot\in dPr\hat{\gamma}^{ \Delta}(D)}{(Q,D)\xrightarrow{a}(Q^{\prime},D)\text{ in }\Delta^{\text{cgr}}}\]  
So \(\mu=(Q^{\prime},D)\), \(Q\xrightarrow{a}Q^{\prime}\) wrt \(\Delta^{\text{det}}\). Furthermore, since \(Q\) is compatible with \(D\), and \(D\) is a difference relation, \(Q^{\prime}\) is compatible with \(D\) too. Hence, \((Q^{\prime}\times Q^{\prime})\cap D=\emptyset\), showing condition \((0^{b})\) of \((Q^{\prime},Q^{\prime})\in\mathit{dep}^{b}(D)\). Trivially, \(Q^{\prime}\subseteq Q^{\prime}\subseteq\mathit{acc}^{\Delta}(Q^{\prime})\) so conditions \((1^{b})\) and \((2^{b})\) of \((Q^{\prime},Q^{\prime})\in\mathit{dep}^{b}(D)\) hold, too. Hence, \((Q^{\prime},Q^{\prime})\in\mathit{dep}^{b}(D)\). **Case \(h=\varepsilon\). **: Obvious. **Case \(h=h_{1}\cdot h_{2}\). **: Since \((Q,D)\xrightarrow{h_{1}}\mu\) wrt. \(\Delta^{\text{cgr}}\), there exists some \(\mu_{1}\in Q^{\text{cgr}}\), such that \((Q,D)\xrightarrow{h_{1}}\mu_{1}\) and \(\mu_{1}\xrightarrow{h_{2}}\mu\) wrt \(\Delta^{\text{cgr}}\). We can apply the induction hypothesis to \(h_{1}\). Hence, there exist subsets of states \(Q_{1}\), \(Q^{\prime}_{1}\subseteq Q\), such that \(\mu_{1}=(Q_{1},D)\), \(Q\xrightarrow{h_{1}}Q^{\prime}_{1}\) wrt \(\Delta\), and \((Q_{1},Q^{\prime}_{1})\in\mathit{dep}^{b}(D)\). We distinguish two cases:  
**Subcase \(Q_{1}\in dPr\hat{\gamma}^{\Delta}(D)\)**. Since \(\mu_{1}=(Q_{1},D)\xrightarrow{h_{2}}\mu\) wrt \(\Delta^{\text{cgr}}\), Claim 2.1b shows that \(\mu=(Q_{1},D)\) so that \((Q_{1},D)\xrightarrow{h_{2}}(Q_{1},D)\) wrt. \(\Delta^{\text{cgr}}\). Condition \((2^{b})\) of \((Q_{1},Q^{\prime}_{1})\in\mathit{dep}^{b}(D)\) and \(Q_{1}\in dPr\hat{\gamma}^{\Delta}(D)\) imply that \(Q^{\prime}_{1}\in\mathit{acc}^{\Delta}(Q_{1})\). Let \(Q_{2}\) be the unique subset of states, such that \(Q^{\prime}_{1}\xrightarrow{h_{2}}Q_{2}\) wrt. \(\Delta^{\text{det}}\). Then, \(Q_{2}\subseteq\mathit{acc}^{\Delta}(Q^{\prime}_{1})\) so that \(Q_{2}\subseteq\mathit{acc}^{\Delta}(Q_{1})\), and thus, condition \((2^{b})\) of \((Q_{1},Q_{2})\in\mathit{dep}^{b}(D)\) holds. Condition \((1^{b})\) of \((Q_{1},Q_{2})\in\mathit{dep}^{b}(D)\) is trivial since \(Q_{1}\in dPr\hat{\gamma}^{\Delta}(D)\). Since \(Q_{1}\in dPr\hat{\gamma}^{\Delta}(D)\) and \(Q_{1}\times Q_{2}\subseteq\mathit{acc}^{\Delta}(Q)^{2}\), it follows that \(Q_{1}\times Q_{2}\cap D=\emptyset\) so condition \((0^{b})\) of \((Q_{1},Q_{2})\in\mathit{dep}^{b}(D)\) holds, too. Hence, \(Q\xrightarrow{h}Q_{2}\) wrt \(\Delta^{\text{det}}\) and \((Q_{1},Q_{2})\in\mathit{dep}^{b}(D)\). **Subcase \(Q_{1}\
ot\in dPr\hat{\gamma}^{\Delta}(D)\)**.