# Complete Subhedge Projection for Stepwise Hedge Automata +
## Appendix B Proofs for Section 6 (Safe-No-Change Projection)
**: The induction hypothesis applied to \(h_{2}\) yields the following:  
\[\exists q^{\prime\prime}.\ (q_{1},P)\xrightarrow{h_{2}}(q^{\prime\prime},P) \text{ wrt }\Delta^{\text{snc}}\wedge q^{\prime}\sim_{P}q^{\prime\prime},\]  
Hence  
\[\exists q^{\prime\prime}.\ (q,P)\xrightarrow{h}(q^{\prime\prime},P)\text{ wrt }\Delta^{\text{snc}}\wedge q^{\prime}\sim_{P}q^{\prime\prime}.\]
**Subsubcase \(q_{1}\in P\). **: By Claim A1.2a, we have \((q_{1},P)\xrightarrow{h_{2}}(q_{1},P)\). We also have \(q^{\prime}\in acc(\{q_{1}\})\), and since we assume \(acc(P)\subseteq P\), this implies \(q^{\prime}\in P\). Hence, \((q,P)\xrightarrow{h}(q_{1},P)\) and \(q^{\prime},q_{1}\in P\), implying the claim is \(q^{\prime}\sim_{P}q_{1}\). **Subcase \(q_{1},q_{1}^{\prime}\in P\). **: Since \(q_{1}^{\prime}\in P\), Claim A1.2a implies \((q_{1}^{\prime},P)\xrightarrow{h_{2}}(q_{1}^{\prime},P)\) wrt \(\Delta^{\text{snc}}\). Thus, \((q,P)\xrightarrow{h}(q_{1}^{\prime},P)\) wrt \(\Delta^{\text{snc}}\). Since \(q^{\prime}\in acc^{\Delta}(\{q_{1}\})\) and \(q_{1}\in P\), it follows that \(q^{\prime}\in acc^{\Delta}(P)\subseteq P\). Here, we used as in the previous subsubcase that \(acc(P)\subseteq P\) is assumed by the claim. Let \(q^{\prime\prime}=q_{1}^{\prime}\). Then, we have \((q,P)\xrightarrow{h}(q^{\prime\prime},P)\) wrt \(\Delta^{\text{snc}}\) and \(q^{\prime},q^{\prime\prime}\in P\) showing the claim. This ends the proof of Claim A1.3a. **Proof of Inclusion \(\mathcal{L}(A)\subseteq\mathcal{L}(A^{\text{snc}})\). **: Let \(h\in\mathcal{L}(A)\). Then, there exists \(q_{0}\in I\) and \(q\in F\), such that \(q_{0}\xrightarrow{h}q\). We distinguish two cases:  
**Case \(q_{0}\in\text{no-change}^{\Delta}\). **: By definition of _no-change_\({}^{\Delta}\) and since \(q\in acc^{\Delta}(q_{0})\) we have \(q_{0}=q\). Claim A1.2a shows that \((q_{0},\emptyset)\xrightarrow{h}(q_{0},\emptyset)\) wrt \(\Delta^{\text{snc}}\) and thus \((q_{0},\emptyset)\xrightarrow{h}(q,\emptyset)\) so that \(h\in\mathcal{L}(A^{\text{snc}})\). **Case \(q_{0}\
ot\in\text{no-change}^{\Delta}\). **: Claim A1.3a with \(P=\emptyset\) shows that \((q_{0},\emptyset)\xrightarrow{h}(q,\emptyset)\) wrt \(\Delta^{\text{snc}}\) and hence \(h\in\mathcal{L}(A^{\text{snc}})\). This ends the proof of the first inclusion. \(\square\)  
We next want to show the inverse inclusion \(\mathcal{L}(A^{\text{snc}})\cap\mathsf{S}\subseteq\mathcal{L}(A)\). It will eventually follow from the following three Claims A1.1b, A1.2b, and A1.3b. Claim A1.1b. : For any hedge \(h\) and state \(\mu\in\mathcal{Q}^{\text{snc}}\), if \(\Pi\xrightarrow{h}\mu\) wrt \(\Delta^{\text{snc}}\) then \(\mu=\Pi\). The proof is straightforward by induction on the structure of \(h\): the only transitions rules of \(\Delta^{\text{snc}}\) with \(\Pi\) on the left hand side are inferred by the last three rules in Figure 10. These require to stay in \(\Pi\) whatever hedge follows. Claim A1.2b. : For any hedge \(h\), set \(P\subseteq\mathcal{Q}\), state \(q\in P\cup\text{no-change}^{\Delta}\), and state \(\mu\in\mathcal{Q}^{\text{snc}}\): if \((q,P)\xrightarrow{h}\mu\) wrt \(\Delta^{\text{snc}}\), then \(\mu=(q,P)\). Proof. : By induction on the structure of \(h\). Suppose that \((q,P)\xrightarrow{h}\mu\) wrt \(\Delta^{\text{snc}}\):  
Case \(h=\left\langle\mu^{\prime}\right\rangle\). : There must exist states \(\mu_{1},\mu^{\prime}_{1}\in\mathcal{Q}^{\text{snc}}\) closing the following diagram:  
Since \(q\in P\cup\text{no-change}^{\Delta}\), the following rule must have been applied to infer \((q,P)\xrightarrow{\partial}\mu_{1}\) wrt \(\Delta^{\text{snc}}\):  
\[\frac{q\in P\cup\text{no-change}^{\Delta}}{(q,P)\xrightarrow{\partial}\Pi\text { in }\Delta^{\text{snc}}}\]  
Therefore, \(\mu_{1}=\Pi\). Claim A1.1b shows that \(\mu^{\prime}_{1}=\Pi\), too. So, \(\mu\) must have been inferred by applying the rule:  
\[\frac{q\in P\cup\text{no-change}^{\Delta}}{(q,P)\emptyset\Pi\to(q,P)\text{ in }\Delta^{\text{snc}}}\.\]  
So, \(\mu=(q,P)\), as required. Case \(h=a\).