# Automatic Addition of Fault-Tolerance in Presence of Unchangeable Environment Actions +
## Appendix B Soundness, Completeness, and Complexity of Algorithm 3
### Completeness
: _If \(\alpha\) is a prefix of a \(p^{\prime\prime}[]_{2}\delta_{e}[]f\) computation and \(\alpha=\langle s_{i},\ldots,s_{m}\rangle\) such that \(s_{i}\in ms_{2}\), or \(\alpha=\langle s_{0},\ldots,s_{i-1},s_{i}\rangle\) such that \(s_{i}\in ms_{2}\) and \((s_{i-1},s_{i})\in f\cup\delta_{p}^{\prime\prime}\), then, 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}\)._  
Proof. : We prove this lemma by looking at lines where we expand \(ms2\):  
**Line 4**: \(ms_{2}=ms_{1}\cup\{s_{0}|\exists s_{1}:(s_{0},s_{1})\in\delta_{e}\cap\delta_{b}\}\)  
In this case, we add \(s_{0}\) to \(ms_{2}\) if either it is in \(ms_{1}\), or it has a \((s_{0},s_{1})\) transition that is in \(\delta_{b}\). If \(s_{0}\in ms_{1}\), any computation starting from \(s_{0}\) proves the theorem. Otherwise, any computation \(\langle s_{0},s_{1},\ldots\rangle\) proves the theorem. **Line 24**: \(ms_{2}=ms_{2}\cup\
eg R\):  
According to Observation 6, there is a suffix (possibly \(\langle\rangle\)) that reaches \(\
eg(R\cup R_{p})\). According to Corollary A3 there is a computation that either reaches \(ms_{1}\), or never reaches \(S^{\prime}\). **Line 29**: \(ms_{2}=ms_{2}\cup ms_{1}\cup\{s_{0}|\exists s_{1}:s_{1}\in ms_{1}:(s_{0},s_{1} )\in\delta_{e}\}\)  
In this case, we add state \(s_{0}\) to \(ms_{2}\), if \(s_{0}\) is in \(ms_{1}\) or can reach state \(s_{1}\in ms_{1}\) with an environment transition. If \(s_{0}\in ms_{1}\), any computation starting from \(s_{0}\) proves the theorem. Otherwise, any computation \(\langle s_{0},s_{1},\ldots\rangle\) proves the theorem. Note that, since we have started the computation from \(s_{0}\), or we have reached \(s_{0}\) with a fault or program transition, even with the fairness assumption, the environment transition \((s_{0},s_{1})\) can execute. The following lemma states that reaching any state in \(ms_{1}\) will result in bad consequences that can be either executing a bad transition or never recovering to the invariant. Specifically,  
Lemma A10. : _If \(\alpha=\langle s_{0},\ldots,s_{i-1},s_{i}\rangle\) where \(s_{i}\in ms_{1}\) is a prefix of a \(p^{\prime\prime}[]_{2}\delta_{e}[]f\) computation, then, there exists a suffix \(\beta=\langle s_{i+1},s_{i+2},\ldots\rangle\) such that \(\alpha\beta\) is a \(p^{\prime\prime}[]_{2}\delta_{e}[]f\) computation and \(\bullet\quad\exists j:j\geq i:(s_{j},s_{j+1})\in\delta_{  
\(\bullet\)\(\forall j:j\geq 0:s_{j}\
otin S^{\prime}\). Proof. : We prove this theorem inductively based on where we expand \(ms_{1}\):  
**Base Case**: \(ms_{1}=\{s_{0}|(s_{0},s_{1})\in f\cap\delta_{b}\}\)  
Let \(\beta\) be any \(p^{\prime\prime}[]2\delta_{e}[]f\) computation starting from \(s_{1}\). Since fault transitions can execute in any state, \(\alpha\beta\) is a \(p^{\prime\prime}[]2\delta_{e}[]f\) computation such that \((s_{0},s_{1})\in\delta_{b}\). **Induction hypothesis**: Theorem holds for current \(ms_{1}\). **Induction step**: We look at lines where we add a state to \(s_{0}\):  
**Line 23**: \(ms_{1}=ms_{1}\cup-(R\cup R_{p})\)  
According to Corollary A3, there is a suffix that either runs a transition in \(\delta_{b}\), never reaches \(S^{\prime}\), or reaches a state in \(ms_{1}\). Thus, the theorem is proved by the induction hypothesis.