# Automatic Addition of Fault-Tolerance in Presence of Unchangeable Environment Actions +
## Appendix B Soundness, Completeness, and Complexity of Algorithm 3  
### Soundness  
First, we show that the program constructed by Algorithm 3 never reaches a state in \(ms_{1}\). Specifically,  
**Lemma A5**: _For any \(p^{\prime}[]_{2}\delta_{\epsilon}[]f\) computation \(\langle s_{0},s_{1},\ldots\rangle\) where \(s_{0}\in S^{\prime}\), there dose not exist \(s_{i}\) such that \(s_{i}\) is in \(ms_{1}\)._  
Consider a computation \(\langle s_{0},s_{1},\ldots\rangle\) of \(p^{\prime}[]_{2}\delta_{\epsilon}[]f\) where \(s_{0}\in S^{\prime}\). We proof by induction that for all \(i\geq 0\), \(s_{i}\
otin ms_{1}\):  
**Base case**: \(i\in\{0,1\}\)  
It is clear \(s_{0}\
otin ms_{1}\), because \(ms_{1}\subseteq ms_{2}\) and \(s_{0}\in S^{\prime}\) and by construction, we know \(S^{\prime}\cap ms_{1}=\emptyset\) (see Line 33). Also, \(s_{1}\
otin ms_{1}\), because otherwise \(s_{0}\in ms_{2}\) that is contradiction to \(S^{\prime}\cap ms_{2}=\emptyset\). **Induction hypothesis**: \(\forall i:0\leq i\leq n:s_{i}\
otin ms_{1}\)  
**Induction step**: \(s_{n+1}\
otin ms_{1}\)  
Suppose \(s_{n+1}\in ms_{1}\). Then, \((s_{n},s_{n+1})\in mt\). By construction, the program does not have any transition in \(mt\). Thus, we have two cases for \((s_{n},s_{n+1})\):  
**Case 1**: \((s_{n},s_{n+1})\in f\)  
In this case, \(s_{n}\in ms_{1}\) (by Line 28) that is contradictory to the induction hypothesis. **Case 2**: \((s_{n},s_{n+1})\in\delta_{\epsilon}\)  
In this case, \(s_{n}\in ms_{2}\). If \(n=0\), then \(s_{0}\in ms_{2}\) that is contradiction to \(S^{\prime}\cap ms_{2}=\emptyset\). If \(n>0\), then \((s_{n-1},s_{n})\in mt\). By construction, the program does not have any transition in \(mt\). Thus, we have two cases for \((s_{n-1},s_{n})\)  
**Case 2.1**: \((s_{n-1},s_{n})\in f\):  
In this case, \(s_{n-1}\in ms_{1}\) that is contradictory to the induction hypothesis. **Case 2.2**: \((s_{n-1},s_{n})\in\delta_{\epsilon}\):  
In this case, as both \((s_{n-1},s_{n})\) and \((s_{n},s_{n+1})\) are in \(\delta_{\epsilon}\), according to the fairness assumption, there does not exist a transition \(\delta^{\prime}_{p}\) starting from \(s_{n}\) and it means that \(s_{n}\) is added to \(ms_{1}\) by Line 28 which is in contradiction with the induction hypothesis. Since we never reach any state in \(ms_{1}\) starting from \(S^{\prime}\) and since any state in \(\
eg(R\cup R_{p})\) is in \(ms_{1}\) by Line 23, we conclude we never reach \(\
eg(R\cup R_{p})\). Thus, we have the following corollary:  
**Corollary A1**: \(R\cup R_{p}\) _in the last iteration of loop on Lines 6-43 is a \(f\)-span for the program resulted by Algorithm 3._The following lemma states that in every computation of the repaired program that starts from its invariant (i.e., \(S^{\prime}\)), if the program reaches a state in \(R\), in the rest of the computation it will reach \(S^{\prime}\). Specifically,  
**Lemma A6**. : _For every \(\delta^{\prime}_{p}[]_{2}\delta_{e}[]f\) computation \(\langle s_{0},s_{1},\ldots\rangle\) such that \(s_{0}\in S^{\prime}\), for \(S^{\prime}\) and \(R\) in the last iteration of the loop on Lines 6-43, we have: \(\forall s_{i}:s_{i}\in R:(\exists j:j\geq i:s_{j}\in S^{\prime})\)._  
Proof. : We prove this lemma by induction as we expand set \(R\):  
**Base case**: \(R=S^{\prime}\)  
The proof is trivial. **Induction hypothesis**: Theorem holds for current \(R\). **Induction step**:  
For any state \(s_{0}\) that is added to \(R\) we have  
\[\left(\
exists_{2}:s_{2}\in(\
eg(R\cup R_{p})\cup ms_{1}):(s_{0},s_{2})\in\delta_{e}\right)\wedge\] \[\left((\exists s_{1}:s_{1}\in(R\cup R_{p})-ms_{1}:(s_{0},s_{1}) \in\delta_{e})\wedge(\
exists_{2}::(s_{0},s_{2})\in(\delta_{e}\cap\delta_{b}) )\right)\] \[\lor s_{0}\in R_{p}\right)\]  
Thus, any environment transition either reaches \(R\) or \(R_{p}\). In the second case, since we have reached a state in \(R_{p}\) by an environment transition, and since from any state in \(R_{p}\) there is a program transition to \(R\) (cf. Line 17), based on the fairness assumption, the computation will reach \(R\).