# Complete Subhedge Projection for Stepwise Hedge Automata +
## Appendix B Proofs for Section 6 (Safe-No-Change Projection)
** By induction hypothesis applied to \((p,p^{\prime})\xrightarrow{h^{\prime}}\mu^{\prime}_{1}\) wrt \(\Delta\), there exists \(p^{\prime\prime}\), such that  
\[(q,P)\xrightarrow{h_{1}}(q_{1}^{\prime},P)\text{ wrt }\Delta^{\text{snc}}\text{ and }q_{1}\sim_{P}q_{1}^{\prime}.\]1  
Since \(\Delta\) does not have blocking runs on \(h\) starting with \(q\), there exist \(q^{\prime\prime}\) such that \(q\emptyset p^{\prime\prime}\to q^{\prime\prime}\) wrt \(\Delta\). There are two ways to satisfy \(p^{\prime}\sim_{p^{\prime}}p^{\prime\prime}\):  
**Subsubcase \(p^{\prime}=p^{\prime\prime}\). ** We then have the following:  
This shows \(q\xrightarrow{\langle\mu^{\prime}\rangle}q^{\prime}\) wrt \(\Delta\). **Subsubcase \(p^{\prime},p^{\prime\prime}\in P\). ** By definition of \(P^{\prime}\), it follows that \(q^{\prime}=q=q^{\prime\prime}\). Hence,  
This shows \(q\xrightarrow{\langle\mu^{\prime}\rangle}q\) wrt \(\Delta\). **Case \(h=a\). ** Since \(q\
ot\in P\cup\text{no-change}^{\Delta}\), the following inference rule must be used:  
\[(q,P)\xrightarrow{h_{1}}(q_{1}^{\prime},P)\text{ wrt }\Delta^{\text{snc}}\text{ and }q_{1}\sim_{P}q_{1}^{\prime}.\]2  
So \(\mu=(q^{\prime},P)\) and \(q\xrightarrow{a}q^{\prime}\) wrt \(\Delta\). **Case \(h=\epsilon\). ** Obvious. **Case \(h=h_{1}\cdot h_{2}\). ** The judgement \((q,P)\xrightarrow{h}\mu\) wrt \(\Delta^{\text{src}}\) shows that there exists \(\mu_{1}\), such that \((q,P)\xrightarrow{h_{1}}\mu_{1}\xrightarrow{h_{2}}\mu\) wrt \(\Delta^{\text{src}}\). Since \(q\
ot\in P\cup\text{no-change}^{\Delta}\), we can apply the induction hypothesis to \(h_{1}\). It shows that there exists \(q^{\prime}_{1}\) and \(q^{\prime\prime}_{1}\), such that \(\mu_{1}=(q^{\prime}_{1},P)\), \(q\xrightarrow{h_{1}}q^{\prime\prime}\) wrt \(\Delta\), and \(q^{\prime}_{1}\sim_{p}q^{\prime\prime}_{1}\). **Subcase \(q^{\prime}_{1}=q^{\prime\prime}_{1}\). ** Hence, \((q_{1},P)\xrightarrow{h_{2}}\mu\) wrt \(\Delta^{\text{src}}\). **Subsubcase \(q^{\prime}_{1}\
ot\in P\cup\text{no-change}^{\Delta}\). ** In this case, we can apply the induction hypothesis to \((q^{\prime}_{1},P)\xrightarrow{h_{2}}\mu\) wrt \(\Delta^{\text{src}}\), showing the existence of \(q^{\prime}\), such that \(\mu=(q^{\prime},P)\) and state \(q^{\prime\prime}\), such that \(q^{\prime}_{1}\xrightarrow{h_{2}}q^{\prime\prime}\) and \(q^{\prime}\sim_{p}q^{\prime\prime}\). Hence, \(\exists q^{\prime\prime}\). \(q\xrightarrow{h}q^{\prime\prime}\) wrt \(\Delta\) and \(q^{\prime}\sim_{p}q^{\prime\prime}\) so the claim holds. **Subsubcase \(q^{\prime}_{1}\in P\cup\text{no-change}^{\Delta}\). ** Claim A1.2b applied to \((q^{\prime}_{1},P)\xrightarrow{h_{2}}\mu\) wrt \(\Delta^{\text{src}}\) shows that \(\mu=(q^{\prime}_{1},P)\). **Subcase \(q^{\prime}_{1},q^{\prime\prime}_{1}\in P\). ** Recall that \((q^{\prime\prime}_{1},P)\xrightarrow{h_{2}}\mu\) wrt \(\Delta^{\text{src}}\) and \(q^{\prime\prime}_{1}\in P\). Claim A1.2b shows that \(\mu=(q^{\prime\prime}_{1},P)\) wrt \(\Delta^{\text{src}}\). We also have \(q\xrightarrow{h_{1}}q^{\prime\prime}_{1}\) wrt \(\Delta\). Since there are no blocking partial runs on \(h\) starting from \(q\) there exist a state \(q^{\prime\prime}\) such that \(q^{\prime\prime}_{1}\xrightarrow{h_{2}}q^{\prime\prime}\) wrt \(\Delta\). Since \(q^{\prime}_{1}\in P\) and \(P\) is closed by accessibility, we have \(q^{\prime\prime}\in acc(\{q^{\prime\prime}_{1}\})\subseteq acc(P)\subseteq P\). From \(q\xrightarrow{h_{1}}q^{\prime\prime}_{1}\) wrt \(\Delta\), we get \(q\xrightarrow{h}q^{\prime\prime}\) wrt \(\Delta\). Since \(q^{\prime\prime}_{1},q^{\prime\prime}\in P\), it follows that \(q^{\prime\prime}_{1}\sim_{p}q^{\prime\prime}\), and thus, the claim holds. This ends the proof of Claim A1.3b. Proof of Inclusion \(\mathcal{L}(A^{snc})\cap\mathbf{S}\subseteq\mathcal{L}(A)\). : Let \(h\in\mathcal{L}(A^{snc})\cap\mathbf{S}\). Since \(h\in\mathcal{L}(A^{snc})\), then there exists \(q_{0}\in I\) and \(q\in F\), such that \((q_{0},\emptyset)\xrightarrow{h}(q,\emptyset)\) wrt \(\Delta^{snc}\).