# Complete Subhedge Projection for Stepwise Hedge Automata +
## 7 Congruence Projection
### Algorithm
#### 7.2.2. Initial Difference Relation  
The initial difference relation on states \(D^{A,\text{F_{S}}}_{init}\in\mathcal{D}^{\Delta}\) is induced from the difference relation on prefixes \(\mathit{diff}^{L}_{\mathbf{S}}\) as follows:  
\[D^{A,\text{F_{S}}}_{init}=\{(q^{\prime},q^{\prime\prime})\ |\ \exists(v^{\prime},v^{ \prime\prime})\in\mathit{diff}^{L}_{\mathbf{S}}\colon\exists q_{0}\in I.\ q_{0}\xrightarrow{\mathit{hdg}(v^{ \prime\prime})}q^{\prime}\ \text{wrt}\ \Delta\wedge q_{0}\xrightarrow{\mathit{hdg}(v^{ \prime\prime})}q^{\prime\prime}\ \text{wrt}\ \Delta\}.\]  
The next lemma indicates how \(D^{A,\text{F_{S}}}_{init}\) can be defined from \(A\) and \(F_{\mathbf{S}}\) without reference to the languages \(L=\mathcal{L}(A)\) and \(\mathbf{S}=\mathcal{L}(A[F/F_{\mathbf{S}}])\). **Lemma 10**. : \(D^{A,\text{F_{S}}}_{init}=\mathit{ldr}^{\Delta}(F\times(F_{\mathbf{S}}\setminus F ))\cap acc^{\Delta}(I)^{2}\)_._  
Proof. : For one direction let \((p^{\prime},p^{\prime\prime})\in D^{A,\text{F_{S}}}_{init}\). Then, there exist nested words \((v^{\prime},v^{\prime\prime})\in\mathit{diff}^{L}_{\mathbf{S}}\) and an initial state \(q_{0}\in I\), such that \(q_{0}\xrightarrow{\mathit{hdg}(v^{\prime})}p^{\prime}\ \text{wrt}\ \Delta\) and \(q_{0}\xrightarrow{\mathit{hdg}(v^{\prime\prime})}p^{\prime\prime}\ \text{wrt}\ \Delta\). Since \(v^{\prime},v^{\prime\prime}\) are nested words, hedge accessibility \((p^{\prime},p^{\prime\prime})\in acc^{\Delta}(I)^{2}\) follows. Furthermore, \((v^{\prime},v^{\prime\prime})\in\mathit{diff}^{L}_{\mathbf{S}}\) requires the existence of a hedge \(h\in\mathcal{H}_{\Sigma}\), such that \(\mathit{hdg}(v^{\prime})\cdot h\in L\) and \(\mathit{hdg}(v^{\prime\prime})\cdot h\in\mathbf{S}\setminus L\). Hence, there are states \(q^{\prime}\in F\) and \(q^{\prime\prime}\in F_{\mathbf{S}}\setminus F\), such that \(p^{\prime}\xrightarrow{h}q^{\prime}\) and \(p^{\prime\prime}\xrightarrow{h}q^{\prime\prime}\). Using Lemma 8, this implies that \((p^{\prime},p^{\prime\prime})\in\mathit{ldr}^{\Delta}(F\times(F_{\mathbf{S}} \setminus F))\). For the other direction, let \((p^{\prime},p^{\prime\prime})\in\mathit{ldr}^{\Delta}(F\times(F_{\mathbf{S}} \setminus F))\cap acc^{\Delta}(I)^{2}\). Using Lemma 8, property \((p^{\prime},p^{\prime\prime})\in\mathit{ldr}^{\Delta}(F\times(F_{\mathbf{S}} \setminus F))\) shows that there exist states \(q^{\prime}\in F\), \(q^{\prime\prime}\in F_{\mathbf{S}}\setminus F\), and \(h\in\mathcal{H}_{\Sigma}\), such that \(p^{\prime}\xrightarrow{h}q^{\prime}\ \text{wrt}\ \Delta\) and \(p^{\prime\prime}\xrightarrow{h}q^{\prime\prime}\ \text{wrt}\ \Delta\). From \((p^{\prime},p^{\prime\prime})\in acc^{\Delta}(I)^{2}\), it follows that there are nested words \(v^{\prime},v^{\prime\prime}\in\mathcal{N}_{\Sigma}\) and an initial state \(q_{0}\in I\), such that \(q_{0}\xrightarrow{\mathit{hdg}(v^{\prime\prime})}p^{\prime}\ \text{wrt}\ \Delta\) and \(q_{0}^{\prime}\xrightarrow{\mathit{hdg}(v^{\prime\prime})}p^{\prime\prime}\ \text{wrt}\ \Delta\). Hence, \((v^{\prime},v^{\prime\prime})\in\mathit{diff}^{L}_{\mathbf{S}}\), so that \((q^{\prime},q^{\prime\prime})\in D^{A,\text{F_{S}}}_{init}\). As a consequence of Lemma 10 and Proposition 4, the initial difference relation \(D^{A,\text{F_{S}}}_{init}\) can be computed in time \(O(|A|^{2})\) from \(A\) and \(F_{\mathbf{S}}\). **Proposition 5** (Soundness of the initial difference relation). : _Let \(A=(\Sigma,\mathcal{Q},\Delta,I,F)\) be a complete \(\mathit{dSha}\), \(F\subseteq F_{\mathbf{S}}\subseteq\mathcal{Q}\), \(L=\mathcal{L}(A)\), and \(\mathbf{S}=\mathcal{L}(A[F/F_{\mathbf{S}}])\). For any hedge \(h\in\mathcal{H}_{\Sigma}\) and state \(q\in\mathcal{Q}\), such that \(q_{0}\xrightarrow{h}q\ \text{wrt}\ \Delta\) for some \(q_{0}\in I\), the nested word \(\mathit{nw}(h)\) is subhedge irrelevant for \(L\) and \(\mathbf{S}\) if and only if \(q\) is subhedge irrelevant for \(D^{A,\text{F_{S}}}_{init}\) wrt. \(\Delta\)._  
Proof.