# Complete Subhedge Projection for Stepwise Hedge Automata +
## Appendix B Proofs for Section 6 (Safe-No-Change Projection)  
Proof. : We have to prove that no more changing states \(q\in P\cup\mathit{no\text{-}change}^{\Delta}\) is sound. If \(q\in\mathit{no\text{-}change}^{\Delta}\), this follows from the schema-completeness of \(\Delta\) so that one can neither block on any hedge from the schema nor change the state. In the case \(q\in P\), theintuition is that the state on level above, say \(r\), can neither change, since \(P=s\)-_no-change\({}^{\Delta}(r)\)_, nor can the automaton block on any hedge from the schema due to schema-completeness. We first prove the inclusion \(\mathcal{L}(A)\subseteq\mathcal{L}(A^{\textit{src}})\). Since \(\mathcal{L}(A)\subseteq\mathbf{S}\) by definition of schemas, this implies \(\mathcal{L}(A)\subseteq\mathcal{L}(A^{\textit{src}})\cap\mathbf{S}\). The proof will be based on the following three Claims A1.1a, A1.2a, and A1.3a. Note that schema-completeness is not needed for this direction. \(\square\)  
Claim A1.1a. : \(\Pi\xrightarrow{h}\Pi\) wrt \(\Delta^{\textit{src}}\) for all hedges \(h\in\mathcal{H}_{\Sigma}\). The proof is straightforward by induction on the structure of \(h\). It uses the last three transition rules of \(\Delta^{\textit{src}}\) in Figure 10 permitting to always stay in \(\Pi\) for whatever hedge follows. Claim A1.2a. : For all \(h\in\mathcal{H}_{\Sigma}\), \(q\in\mathcal{Q}\), and \(P\subseteq\mathcal{Q}\), such that \(q\in P\cup\textit{no-change}^{\Delta}\),  
\[(q,P)\xrightarrow{h}(q,P)\text{ wrt }\Delta^{\textit{src}}.\]  
We prove Claim A1.2a by induction on the structure of \(h\). **Case \(h=\langle h^{\prime}\rangle\). **: In this case, we can use Claim A1.1a to show \(\Pi\xrightarrow{h^{\prime}}\Pi\) wrt \(\Delta^{\textit{src}}\) and the inference rules  
\[\frac{q\in P\cup\textit{no-change}^{\Delta}}{(q,P)\xrightarrow{\langle}\Pi \text{ in }\Delta^{\textit{src}}}\qquad\frac{q\in P\cup\textit{no-change}^{\Delta}}{(q,P )\boxplus\Pi\rightarrow(q,P)\text{ in }\Delta^{\textit{src}}}\]  
in order to close the following diagram with respect to \(\Delta^{\textit{src}}\):  
This proves \((q,P)\xrightarrow{h}(q,P)\) wrt \(\Delta^{\textit{src}}\), as required by the claim. **Case \(h=a\). **: Since \(q\in P\cup\textit{no-change}^{\Delta}\) we can apply the inference rule:  
\[\frac{a\in\Sigma\quad q\in P\cup\textit{no-change}^{\Delta}}{(q,P)\xrightarrow {a}(q,P)\text{ in }\Delta^{\textit{src}}}\]  
This proves this case of the claim. **Case \(h=\varepsilon\). **: We trivially have \((q,P)\xrightarrow{\varepsilon}(q,P)\) wrt \(\Delta^{\textit{src}}\). **Case \(h=h^{\prime}\cdot h^{\prime\prime}\). **: By induction hypothesis applied to \(h^{\prime}\) and \(h^{\prime\prime}\) we have: \((q,P)\xrightarrow{h^{\prime}}(q,P)\) and \((q,P)\xrightarrow{h^{\prime\prime}}(q,P)\) wrt \(\Delta^{\textit{src}}\). Hence, \((q,P)\xrightarrow{h^{\prime}\cdot h^{\prime\prime}}(q,P)\) wrt \(\Delta^{\textit{src}}\). This ends the proof of Claim A1.2a. The next claim, in which the induction step is a little more tedious to prove, is the key of the soundness proof. We define the following predicate for all \(q^{\prime},q^{\prime\prime}\in\mathcal{Q}\) and \(P\subseteq\mathcal{Q}\):  
\[q^{\prime}\sim_{P}q^{\prime\prime}\text{ iff }(q^{\prime}=q^{\prime\prime} \lor q^{\prime},q^{\prime\prime}\in P)\]  
Claim A1.3a. : Let \(h\in\mathcal{H}_{\Sigma}\) be a hedge, \(q,q^{\prime}\in\mathcal{Q}\) states and \(P\subseteq\mathcal{Q}\) a subset of states, such that \(acc^{\Delta}(P)\subseteq P\) and \(q\
ot\in P\cup\textit{no-change}^{\Delta}\). If \(q\xrightarrow{h}q^{\prime}\) wrt \(\Delta\), then there exists \(q^{\prime\prime}\), such that \((q,P)\xrightarrow{h}(q^{\prime\prime},P)\) wrt \(\Delta^{\textit{src}}\) and \(q^{\prime}\sim_{P}q^{\prime\prime}\). Proof. : Induction on the structure of \(h\). **Case \(h=\langle h^{\prime}\rangle\).