# Automatic Addition of Fault-Tolerance in Presence of Unchangeable Environment Actions +
## Appendix B Soundness, Completeness, and Complexity of Algorithm 3
### Completeness  
Like the proof of the completeness of Algorithm 2, the proof of the completeness of Algorithm 3 is based on the analysis of states that are removed from S. For Algorithm 3, we focus on the iterations of the loop on Lines 6-43. Similar to Observation 1, we have the following observation for Algorithm 3:  
**Observation 5**. : _In any given iteration \(i\) of loop on 6-43, let \(R\), \(R_{p}\) and \(ms_{1}\) be \(R\), \(R_{p}\) and \(ms_{1}\) at the end of iteration \(i\). Then, for any \(s_{0}\) such that \(s_{0}\
otin R\) and \(\exists s_{1}::(s_{0},s_{1})\in\delta_{e}\), we have \((\exists s_{2}:s_{2}\in\
eg(R\cup Rp)\cup ms_{1}:(s_{0},s_{2})\in\delta_{e})\lor\)\((\exists s_{2}::(s_{0},s_{2})\in\delta_{e})\in\delta_{e})\)._  
We also note the following observation:  
**Observation 6**. : _For any \(s_{0}\) such that \(s_{0}\
otin R\), either \(s_{0}\in\
eg(R\cup R_{p})\), or \(\exists s_{2}:s_{2}\in\
eg(R\cup Rp)\cup ms_{1}:(s_{0},s_{2})\in\delta_{e}\)._  
Lemmas A8, A9, A10 and A11, Corollary A3 and Theorem A5 provided in the following, hold for any given iteration \(i\) of loop on Lines 6-43 assuming Algorithm 3 has declared failure. For these results, let \(p^{\prime\prime}=\langle S_{p},\delta^{\prime\prime}_{p}\rangle\) with invariant \(S^{\prime\prime}\) be any revision for program \(p=\langle S_{p},\delta_{p}\rangle\) with invariant \(S\) such that \(S^{\prime\prime}\subseteq S^{\prime}\), \(\delta^{\prime\prime}_{p}\subseteq\delta^{\prime}_{p}\) and \(\delta^{\prime\prime}_{p}\cap mt=\emptyset\). Consider \(S^{\prime}\), \(\delta^{\prime}_{p}\) and \(mt\) at the beginning of iteration \(i\) and \(ms_{1}\), \(ms_{2}\), \(R\) and \(R_{p}\) at the end of the iteration. Also, let \(f\) and \(\delta_{e}\) be a set of fault transitions and a set of environment transitions for \(p\) (i.e., \(p^{\prime\prime}\)), respectively. The following lemma focuses on the situation where a given revision \(p^{\prime\prime}\) reaches a state that our algorithm marks as \(\
eg(R\cup R_{p})\). **Lemma A8**. : _For every \(p^{\prime\prime}[]_{2}\delta_{e}[]f\) prefix \(\alpha=\langle s_{0},\ldots,s_{i}\rangle\) such that \(s_{i}\in\
eg(R\cup R_{p})\), there exists a suffix \(\beta\) such that \(\alpha\beta\) is a \(p^{\prime\prime}[]\)\(\lfloor 2\delta_{e}[]f\) computation and_\((s_{i},s_{i+1})\in\delta_{b}\), or \(s_{i+1}\in ms_{1}\), or \(s_{i+1}\in\
eg(R\cup R_{p})\), or \(s_{i+1}\in(R_{p}-R)\wedge s_{i+2}\in\
eg(R\cup R_{p})\). Proof. : There are two cases for \(s_{i}\):  
**Case 1**: \(s_{i}\) is environment-enabled (see Definition 18) in prefix \(\alpha=\langle s_{0},s_{1},\ldots,s_{i}\rangle\):  
According to Observation 5, there exists \(s\in\
eg(R\cup R_{p})\cup ms_{1}\) such that \((s_{i},s)\in\delta_{e}\), \((s_{i},s)\in\delta_{e}\cap\delta_{b}\). Any suffix that starts from \(s\) proves the theorem. **Case 2**: \(s_{i}\) is not environment-enabled in prefix \(\alpha=\langle s_{0},s_{1},\ldots,s_{i}\rangle\)  
The proof for this case is identical to the proof of Case 2 of Lemma 2. Corollary A3. : _For every \(p^{\prime\prime}[]_{2}\delta_{e}[]f\) prefix \(\alpha=\langle s_{0},\ldots,s_{i}\rangle\) such that \(s_{i}\in\
eg(R\cup R_{p})\), there exists a suffix \(\beta\) such that \(\alpha\beta\) is a \(p^{\prime\prime}[]_{2}\delta_{e}[]f\) computation and \(\bullet\quad\exists j:j\geq i:(s_{j-1},s_{j})\in\delta_{b}\), or \(\bullet\quad\exists j:j\geq i:s_{j}\in ms_{1}\), or \(\bullet\quad\forall i:i\geq 0:s_{i}\
otin S^{\prime}\)._  
The following lemma focuses on states that are marked as \(ms_{2}\). Lemma A9.