# Automatic Addition of Fault-Tolerance in Presence of Unchangeable Environment Actions +
## Appendix A Soundness, Completeness and Complexity of Algorithm 2  
### Soundness  
The following lemma splits condition **C1** into easily verifiable conditions that assist in proving the soundness of Algorithm 2. **Lemma A1**. : _The condition **C1** in the problem definition of addition of fault-tolerance is satisfied for \(k=2\) if conditions below are satisfied:_  
1. \(S^{\prime}\subseteq S\)__
2. \(\delta^{\prime}_{p}|S^{\prime}\subseteq\delta_{p}|S\)__\(\forall s_{1}:\big{(}\exists s_{0},s_{2},s_{3}:s_{0}\in S^{\prime}\wedge(s_{0},s_{1} ),(s_{1},s_{2})\in\delta_{e}\wedge(s_{1},s_{3})\in\delta_{p}\big{)}:\big{(}\exists s _{4}::(s_{1},s_{4})\in\delta^{\prime}_{p}\big{)}\)
4. \(\forall s_{0}:(\exists s_{1}::(s_{0},s_{1})\in\delta_{p}\cup\delta_{e})\)  
**Proof. ** We show by induction that if all conditions of the lemma are satisfied, then every prefix of any \(p^{\prime}\big{[}\!\big{]}_{2}\delta_{e}\) computation that starts from a state in \(S^{\prime}\) is a prefix of a \(p\big{[}\!\big{]}_{2}\delta_{e}\) computation which starts in \(S\). **Base case:** Let \(\langle s_{0}\rangle\) be the prefix of a \(p^{\prime}\big{[}\!\big{]}_{2}\delta_{e}\) computation that starts from \(S^{\prime}\). Since \(S^{\prime}\subseteq S\), \(s_{0}\in S\). Thus, \(\langle s_{0}\rangle\) is also a prefix of a \(p\big{[}\!\big{]}_{2}\delta_{e}\) computation that starts from \(S\). **Induction hypothesis:** The theorem holds for \(\langle s_{0},s_{1},\ldots,s_{i}\rangle\). **Induction step:** We show theorem holds for \(\langle s_{0},s_{1},\ldots,s_{i+1}\rangle\). Since \(p^{\prime}\cup\delta_{e}\) is closed in \(S^{\prime}\), we know that \(s_{i+1}\in S^{\prime}\). We have two cases for \((s_{i},s_{i+1})\):  
**Case 1**\((s_{i},s_{i+1})\in\delta^{\prime}_{p}\)  
From \(\delta^{\prime}_{p}|S^{\prime}\subseteq\delta_{p}|S^{\prime}\), we have \((s_{i},s_{i+1})\in\delta_{p}\). Therefore, if \(\langle s_{0},s_{1},\ldots,s_{i}\rangle\) is a prefix of \(p\big{[}\!\big{]}_{2}\delta_{e}\), then \(\langle s_{0},s_{1},\ldots,s_{i},s_{i+1}\rangle\) is a prefix of \(p\big{[}\!\big{]}_{2}\delta_{e}\). **Case 2**\((s_{i},s_{i+1})\in\delta_{e}\) :  
Two sub-cases are possible below this case:  
**Case 2.1**\((s_{i-1},s_{i})\in\delta^{\prime}_{p}\)  
In this case, as we have reached \(s_{i}\) by a program transition, even with the fairness assumption, \((s_{i},s_{i+1})\) can occur in \(p\big{[}\!\big{]}_{2}\delta_{e}\), Therefore, if \(\langle s_{0},s_{1},\ldots,s_{i}\rangle\) is a prefix of \(p\big{[}\!\big{]}_{2}\delta_{e}\), then \(\langle s_{0},s_{1},\ldots,s_{i},s_{i+1}\rangle\) is a prefix of \(p\big{[}\!\big{]}_{2}\delta_{e}\). **Case 2.2**\((s_{i-1},s_{i})\in\delta_{e}\)  
In this case, there does not exist \(s^{\prime}\) such that \((s_{i},s^{\prime})\in\delta^{\prime}_{p}\) (otherwise, because of fairness \((s_{i},s_{i+1})\) cannot be in any prefix of \(p^{\prime}\big{[}\!\big{]}_{2}\delta_{e}\)). Now, according to condition 3, we know there does not exist state \(s^{\prime\prime}\) such that \((s_{i},s^{\prime\prime})\in\delta_{p}\). Thus, even with the fairness assumption \((s_{i},s_{i+1})\) can occur in \(p\big{[}\!\big{]}_{2}\delta_{e}\). Therefore, if \(\langle s_{0},s_{1},\ldots,s_{i}\rangle\) is a prefix of \(p\big{[}\!\big{]}_{2}\delta_{e}\), then \(\langle s_{0},s_{1},\ldots,s_{i},s_{i+1}\rangle\) is a prefix of \(p\big{[}\!\big{]}_{2}\delta_{e}\). Since every prefix of \(p^{\prime}\big{[}\!\big{]}_{2}\delta_{e}\) that starts from a state in \(S^{\prime}\) is a prefix of \(p\big{[}\!\big{]}_{2}\delta_{e}\) which starts in \(S\), **C1** is satisfied. Theorem A.1: _Algorithm 2 is sound._  
To show the soundness of our algorithm, we need to show that the three conditions of the addition problem are satisfied. **C1**: Consider a computation \(c\) of \(p^{\prime}\big{[}\!\big{]}_{2}\delta_{e}\) that starts from a state in \(S^{\prime}\). By construction, \(c\) starts from a state in \(S\) and \(\delta^{\prime}_{p}|S^{\prime}\) is a subset of \(\delta_{p}|S^{\prime}\). Therefore, the first two requirements of Lemma A.1 are satisfied.