# Complete Subhedge Projection for Stepwise Hedge Automata +
## Appendix B Proofs for Section 6 (Safe-No-Change Projection)
**: The assumption \(q\xrightarrow{h}q^{\prime}\) wrt \(\Delta\) shows that there exists states \(p_{0}\in\langle\rangle^{\Delta}\) and \(p\in\mathcal{Q}\) closing the following diagram:  
Let \(P^{\prime}=\textit{s-no-change}^{\Delta}(q)\) and note that \(acc^{\Delta}(P^{\prime})\subseteq P^{\prime}\). Since \(q\
ot\in P\cup\textit{no-change}^{\Delta}\) we can infer the following:  
\[ \begin{array}{c}\xrightarrow{\langle\rangle}p_{0}\text{ in }\Delta\quad q \
ot\in P\cup\textit{no-change}^{\Delta}\\ \hline(q,P)\xrightarrow{\langle\rangle}(p_{0},P^{\prime})\text{ in }\Delta^{\textit{snc}} \end{array} \qquad \begin{array}{c}q@{}p\to q^{\prime}\text{ in }\Delta\quad q\
ot\in P\cup\textit{no-change}^{\Delta}\\ \hline(q,P)@{}(p,P^{\prime})\to(q^{\prime},P)\text{ in }\Delta^{\textit{snc}} \end{array} \]
**Subcase \(p_{0}\
ot\in P^{\prime}\cup\textit{no-change}^{\Delta}\)**. The induction hypothesis applied to \(h^{\prime}\) shows that there exists \(p^{\prime}\), such that \((p_{0},P^{\prime})\xrightarrow{h^{\prime}}(p^{\prime},P^{\prime})\) wrt \(\Delta^{\textit{snc}}\) and \(p\sim_{P}p^{\prime}\). We distinguish the two cases justifying the latter predicate:
**Subsubcase \(p^{\prime}=p\). **: Hence, \((p_{0},P^{\prime})\xrightarrow{h^{\prime}}(p,P^{\prime})\) wrt \(\Delta^{\textit{snc}}\), so we can close the diagram as follows:  
This shows that \((q,P)\xrightarrow{h}(q^{\prime},P)\) wrt \(\Delta^{\textit{snc}}\), and thus, the claim since \(q^{\prime}\sim_{P}q^{\prime}\). **Subsubcase \(p,p^{\prime}\in P^{\prime}\)**. Since \(p^{\prime}\in P^{\prime}\) and \(P^{\prime}=\textit{s-no-change}^{\Delta}(q)\), we have \(q@{}p^{\prime}\to q\) in \(\Delta\). Hence, we can close the diagram as follows:  
Since \(p\in P^{\prime}\) and \(q@{}p\to q^{\prime}\) in \(\Delta\), we have \(q=q^{\prime}\) by definition of \(P^{\prime}=\textit{s-no-change}^{\Delta}(q)\). This shows that \((q,P)\xrightarrow{h}(q,P)\) wrt \(\Delta^{\textit{snc}}\). Since \(q\sim_{P}q\), the claim follows. **Subcase \(p_{0}\in P^{\prime}\cup\textit{no-change}^{\Delta}\)**. **: Claim A1.2 then shows that \((p_{0},P^{\prime})\xrightarrow{h^{\prime}}(p_{0},P^{\prime})\) wrt \(\Delta^{\textit{snc}}\). **Subsubcase \(p_{0}\in P^{\prime}\)**. Since \(p\in acc^{\Delta}(p_{0})\) and \(acc^{\Delta}(P^{\prime})\subseteq P^{\prime}\), it follows that \(p\in P^{\prime}\), too. By definition \(P^{\prime}=\textit{s-no-change}^{\Delta}(q)\) and the completeness of \(\Delta\), the memberships \(p_{0}\in P^{\prime}\) and \(p\in P^{\prime}\) imply that \(q@^{\Delta}p_{0}=\{q\}=q@^{\Delta}p\). We can now close the diagram below as follows:  
**Subsubcase \(p_{0}\in\textit{no-change}^{\Delta}\)**. In this case, \(p_{0}=p\) so that \(q^{\prime}\in q@^{\Delta}p_{0}\). Hence,  
**Case \(h=a\). ** Since \(q\
ot\in P\cup\text{no-change}^{\Delta}\), we can apply the inference rule:  
\[\frac{q\xrightarrow{a}q^{\prime}\text{ in }\Delta}{(q,P)\xrightarrow{a}(q^{ \prime},P)\text{ in }\Delta^{\text{snc}}}\]  
This shows that \((q,P)\xrightarrow{h}(q^{\prime},P)\) validates the claim since \(q^{\prime}\sim_{P}q^{\prime}\). **Case \(h=\varepsilon\). ** In this case, we have \(q=q^{\prime}\) and \((q,P)\xrightarrow{\varepsilon}(q,P)\) so the claim holds. **Case \(h=h_{1}\cdot h_{2}\). ** Since \(q\xrightarrow{h}q^{\prime}\) wrt \(\Delta\), there exists \(q_{1}\in\mathcal{Q}\), such that \(q\xrightarrow{h_{1}}q_{1}\) wrt \(\Delta\) and \(q_{1}\xrightarrow{h_{2}}q^{\prime}\) wrt \(\Delta\). Since \(q\
ot\in P\cup\text{no-change}^{\Delta}\), we apply the induction hypothesis on \(h_{1}\). This implies that there exists \(q_{1}^{\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}.\]  
We distinguish the two cases of \(q_{1}\sim_{P}q_{1}^{\prime}\):  
**Subcase \(q_{1}=q_{1}^{\prime}\). **: We also distinguish two subcases here:  
**Subsubcase \(q_{1}\
ot\in P\).