# Complete Subhedge Projection for Stepwise Hedge Automata +
## 7 Congruence Projection
### Soundness  
We next adapt the soundness result and proof from the safe-no-change projection to congruence projection. **Theorem 2** (Soundness of congruence projection.). : _For any dSha\(A=(\Sigma,Q,\Delta,I,F)\) and set \(F\subseteq F_{\mathsf{S}}\subseteq\mathcal{Q}\), the congruence projection of \(A\) with respect to \(F_{\mathsf{S}}\) preserves the language of \(A\) within schema \(\mathsf{S}=\mathcal{L}(A[F/F_{\mathsf{S}}])\), i.e.,_  
\[\mathcal{L}(A^{\texttt{cgr}(\mathsf{S})})\cap\mathsf{S}=\mathcal{L}(A).\]  
We note that \(\mathsf{S}\) is a schema for \(A\) since \(F\subseteq F_{\mathsf{S}}\). Furthermore, \(A\) is schema-complete for \(\mathsf{S}\) since \(A\) is deterministic and \(\mathsf{S}=\mathcal{L}(A[F/F_{\mathsf{S}}])\). Proof. : The proof of the inclusion \(\mathcal{L}(A)\subseteq\mathcal{L}(A^{\texttt{cgr}(\mathsf{S})})\cap\mathsf{S}\) will be based on the following two claims:  
**Claim 2.1a. ** For all \(h\in\mathcal{H}_{\Sigma}\), \(D\in\mathcal{D}^{\Delta}\), and \(Q\in d\mathsf{Pr}\hat{\tau}^{\Delta}(D)\), \((Q,D)\xrightarrow{h}(Q,D)\) wrt \(\Delta^{\texttt{cgr}}\). Figure 18: The congruence projection \(A^{\texttt{cgr}([\texttt{doc}])}\) of the dSha\(A\) in Figure 4 for the XPath filter \([\texttt{self:list/child:item}]\) with schema \([\texttt{doc}]\). Subhedge irrelevant states are colored in orange. The underscore stands for any label, either list or item. Proof. : We prove Claim 2.1a by induction on the structure of \(h\). Suppose that \(Q\in dPrj^{\Delta}(D)\). **Case \(h=\langle h^{\prime}\rangle\). **: The induction hypothesis applied to \(h^{\prime}\) yields \((Q,D)\xrightarrow{h^{\prime}}(Q,D)\) wrt \(\Delta^{\mathit{cgr}}\). We can thus apply the following two inference rules:  
\[\frac{Q\in dPrj^{\Delta}(D)}{(Q,D)\xrightarrow{\langle}(Q,D)\text{ in }\Delta^{ \mathit{cgr}}}\qquad\frac{Q\in dPrj^{\Delta}(D)}{(Q,D))@(Q,D)\to(Q,D)\text{ in }\Delta^{\mathit{cgr}}}\]  
in order to close the following diagram with respect to \(\Delta^{\mathit{cgr}}\):  
This proves \((Q,D)\xrightarrow{h}(Q,D)\) wrt \(\Delta^{\mathit{cgr}}\), as required by the claim. **Case \(h=a\). **: Since \(q\in dPrj^{\Delta}(D)\), we can apply the inference rule:  
\[\frac{a\in\Sigma\quad Q\in dPrj^{\Delta}(D)}{(Q,D)\xrightarrow{a}(Q,D)\text{ in }\Delta^{\mathit{cgr}}}\]  
This proves this case of the claim. **Case \(h=\varepsilon\). **: We trivially have \((Q,D)\xrightarrow{\varepsilon}(Q,D)\) wrt \(\Delta^{\mathit{cgr}}\). **Case \(h=h^{\prime}\cdot h^{\prime\prime}\). **: By the induction hypothesis applied to \(h^{\prime}\) and \(h^{\prime\prime}\), we obtain the following:  
\[(Q,D)\xrightarrow{h^{\prime}}(Q,D)\text{ and }(Q,D)\xrightarrow{h^{\prime \prime}}(Q,D)\text{ wrt }\Delta^{\mathit{cgr}}\text{. Hence, }(Q,D) \xrightarrow{h^{\prime}\cdot h^{\prime\prime}}(Q,D)\text{ wrt }\Delta^{\mathit{cgr}}\text{.}\]  
This ends the proof of Claim 2.1a. The next claim is the key of the soundness proof. For any difference relation \(D\), we define a binary relation \(\mathit{dep}^{\mu}(D)\subseteq 2^{Q}\times 2^{Q}\), such that, for any two subsets of states \(Q^{\prime}\), \(Q^{\prime\prime}\subseteq\mathcal{Q}\),  
\[(Q^{\prime},Q^{\prime\prime})\in\mathit{dep}^{\mu}(D)\Leftrightarrow\left\{ \begin{array}{l}Q^{\prime}\
ot\in dPrj^{\Delta}(D)\Rightarrow Q^{\prime} \subseteq Q^{\prime\prime}\qquad\land\qquad\qquad\qquad\qquad\qquad(1^{a})\\ Q^{\prime}\in dPrj^{\Delta}(D)\Rightarrow(Q^{\prime}\subseteq acc^{\Delta}(Q ^{\prime\prime})\land Q^{\prime\prime}\in dPrj^{\Delta}(D))\quad(2^{a})\end{array} \right.\]  
Furthermore, note that \(Q^{\prime\prime}\in dPrj^{\Delta}(D)\land Q^{\prime}\subseteq acc^{\Delta}(Q ^{\prime\prime})\) implies \(Q^{\prime}\in dPrj^{\Delta}(D)\), and thus, \((Q^{\prime},Q^{\prime\prime})\in\mathit{dep}^{\mu}(D)\). **Claim 2.2a. **: Let \(h\in\mathcal{H}_{\Sigma}\) a hedge, \(Q\), \(Q^{\prime}\subseteq\mathcal{Q}\) subsets of states, and \(D\in\mathcal{D}^{\Delta}\) a difference relation.