# Automatic Addition of Fault-Tolerance in Presence of Unchangeable Environment Actions +
## Appendix A Soundness, Completeness and Complexity of Algorithm 2
### Completeness
**Case 2**\(\exists s_{1}::(s_{1}\in ms_{1}\wedge(s_{0},s_{1})\in\delta_{e})\wedge(\forall s _{2}::(s_{0},s_{2})\in mt)\)  
In this case, if according to fairness, \((s_{0},s_{1})\) can occur, state \(s_{1}\in ms_{1}\) can be reached by \((s_{0},s_{1})\) and according to the induction hypothesis, the theorem is proved. However, if \((s_{0},s_{1})\) cannot occur, some other transition in \(\delta_{p}^{\prime\prime}\cup f\) should occur but we know such transition is in \(mt\) and reaches a state in \(ms_{2}\). Thus, according to Lemma A2, either a transition in \(\delta_{b}\) can occur, or a state in \(ms_{1}\) can be reached. Hence, according to the induction hypothesis, a transition in \(\delta_{b}\) can occur in both cases. **Case 3**\(\exists s_{1}::((s_{0},s_{1})\in\delta_{e}\cap\delta_{b})\wedge(\forall s_{2}:: (s_{0},s_{2})\in mt)\)  
In this case, if, according to fairness, \((s_{0},s_{1})\) can occur, by its occurrence a transition in \(\delta_{b}\) has occurred. However, if \((s_{0},s_{1})\) cannot occur, some other transition in \(\delta_{p}^{\prime\prime}\cup f\) should occur but we know such a transition is in \(mt\) and reaches a state in \(ms_{2}\). Thus, according to Lemma A2, either a transition in \(\delta_{b}\) can occur or a state in \(ms_{1}\) can be reached. Hence, according to the induction hypothesis, a transition in \(\delta_{b}\) can occur in both cases. The last lemma that we use to prove the completeness of Algorithm 2 is Lemma A4. This lemma states that having any state in \(ms_{4}\) in the invariant of any give revision \(p^{\prime\prime}\) of program \(p\) results in having new computation in the invariant that was not in the original program. **Lemma A4**. : _Let \(p^{\prime\prime}=\langle S_{p},\delta_{p}^{\prime\prime}\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}\) and \(\delta_{p}^{\prime\prime}|S^{\prime\prime}\subseteq\delta_{p}^{\prime}|S^{ \prime}\) for \(S^{\prime}\) and \(\delta_{p}^{\prime}\) at the beginning of the loop on Lines 13-21. If \(S^{\prime\prime}\) includes any state in \(ms_{4}\) in any iteration of the loop on Lines 13-21, then there is a \(p^{\prime\prime}[|2\delta_{e}\) computation that starts from \(S^{\prime\prime}\) that is not a \(p^{\prime\prime}[|2\delta_{e}\)._  
Proof. : Suppose there exists state \(s_{0}\in S^{\prime\prime}\cap ms_{4}\). Then, there is a state, \(s\in ms_{3}\) such that \((s_{0},s)\in\delta_{e}\) and \(\big{(}\exists s_{1},s_{2}::(s,s_{1})\in\delta_{e}\ \wedge(s,s_{2})\in\delta_{p}\big{)} \wedge\big{(}\
exists_{3}::(s,s_{3})\in\delta_{p}^{\prime}\big{)}\). Since \(\delta_{p}^{\prime\prime}|S^{\prime\prime}\subseteq\delta_{p}^{\prime}|S^{ \prime}\), \((\
exists_{3}::(s,s_{3})\in\delta_{p}^{\prime\prime})\). Since \(S^{\prime\prime}\) is closed in \(p^{\prime\prime}\cup\delta_{e}\), \(s\) and \(s_{1}\) are in \(S^{\prime\prime}\), as well. Now, observe that \((s_{0},s,s_{1},\cdots)\) is \(p^{\prime\prime}[|2\delta_{e}\) computation but it is not a \(p[|2\delta_{e}\) computation, as because of fairness, \((s,s_{1})\in\delta_{e}\) cannot occur when there exists \((s,s_{2})\in\delta_{p}\). **Theorem A2**. : _Algorithm 2 is complete._  
Proof. : Suppose program \(p^{\prime\prime}\) with invariant \(S^{\prime\prime}\) solves the addition problem. We show that at any point of Algorithm 2, \(S^{\prime\prime}\) must always be a subset of \(S^{\prime}\). We prove this by looking at lines where we set \(S^{\prime}\). According to Lemma A2 and Lemma A3, \(S^{\prime\prime}\) cannot have any transition in \(ms_{2}\), because by starting from a state in \(ms_{2}\), a computation may execute a bad transition. In addition, \(S^{\prime\prime}\) must be closed in \(\delta_{p}^{\prime\prime}\) and cannot have any deadlock state. Thus, \(S^{\prime\prime}\subseteq S^{\prime}\) for \(S^{\prime}\) of Line 12.