# \(k\)-Circle Formation and \(k\)-epf by Asynchronous Robots
## 4 Algorithm
### Moveto Destination
At time \(t^{\prime}>t\), let \(p^{\prime}\) be the intersection point between \(C(f_{u},\rho)\) and \(\overline{r_{i}(t^{\prime})f_{j}}\). Note that \(p^{\prime}\) is not a robot position. Robot \(r_{i}\) selects \(P^{\prime}=\overline{r_{i}(t^{\prime})f_{j}}\) and \(q(t^{\prime})=p^{\prime}\) (Figure 13). We have \(d(r_{i}(t^{\prime}),s(t))>d(r_{i}(t^{\prime}),s(t^{\prime}))\) and \(d(r_{i}(t),s(t))-d(r_{i}(t^{\prime}),s(t^{\prime}))>d(r_{i}(t),s(t))-d(r_{i}(t^ {\prime}),s(t))\geq\delta\). This implies that \(d_{j}(t^{\prime})+\delta\leq d_{j}(t)\). **Case 5**. : \(d(r_{i},f_{j})<\rho\). We have \(q(t)=s(t)\). Let \(q\) be the intersection point between \(C(f_{j},\rho)\) and \(l_{ji}(t)\). First, consider the case when \(r_{i}\) selects \(P=\overline{r_{i}(t)q}\) and \(q(t)=q\) (Step 5 of Algorithm 1). At time \(t^{\prime}\), there would not be any robot position on \(q(t)\). Robot \(r_{i}\) selects \(P^{\prime}=\overline{r_{i}(t)q}\). Since \(\delta\) is the minimum displacement in a round, \(d_{j}(t^{\prime})+\delta\leq d_{j}(t)\). Movements are shown in (a)a. Next, consider the case in which \(r_{i}\) selects its movement path \(P\) by step 11 or step 17 of Algorithm 1. We have \(d(r_{i}(t^{\prime}),q(t))>d(r_{i}(t^{\prime}),q(t^{\prime}))\) and \(d(r_{i}(t),q(t))-d(r_{i}(t^{\prime}),q(t^{\prime}))>d(r_{i}(t),q(t))-d(r_{i}(t^ {\prime}),q(t))\geq\delta\). Hence, \(d_{j}(t^{\prime})+\delta\leq d_{j}(t)\). Movements are shown in (b)b,c. Figure 11: Robot \(r_{i}\) has moved from \(r_{i}(t)\) to \(r_{i}(t^{\prime})\), along \(P=\overline{r_{i}(t)q}\) towards \(q(t)=q\) computed at time \(t\) (\(q\) is the point of intersection between \(C(f_{j},\rho)\) and \(t^{\mu}\)). Robot \(r_{i}\) selects \(P^{\prime}=\overline{r_{i}(t^{\prime})p(t^{\prime})}\) and \(q(t^{\prime})=p(t^{\prime})\) at time \(t^{\prime}\). Furthermore, \(q(t)=s(t)\) and \(q(t^{\prime})=s(t^{\prime})\), i.e., the destination point lies on \(C(f_{j},\rho)\). Hence, execution of \(MovetoDestination(C(t))\) ensures \(d_{j}(t^{\prime})+\delta\leq d_{j}(t)\). **Lemma 5**. : _Let \(f_{j}\) be the target fixed point and \(r_{i}\) its candidate robot in the configuration \(C(t)\). During an execution of \(AlgorithmOneAxis(C(t))\), execution of \(MovetoDestination(C(t),f_{j},r_{i})\) ensures significant progress._

Proof of Lemma 5.: Let \(r_{i}\) compute movement path \(P\) and destination point \(q(t)\) by the execution of \(MovetoDestination(C(t),f_{j},r_{i})\) at time \(t\). Let \(t^{\prime}>t\) be an arbitrary point of time at which \(r_{i}\) has completed at least one LCM cycle. We need to show that there has been significant progress in between the time interval \(t\) to \(t^{\prime}\). We have the following cases:

**Case 1**. : \(r_{i}(t^{\prime})=q(t)\) and \(r_{i}\) is on the \(C(f_{j},\rho)\). We have the following two sub-cases:

**Subcase 1**. : If \(C(f_{j},\rho)\) has exactly \(k\) robots on it, then \(n_{k}(t^{\prime})=n_{k}(t)-1\), ensuring significant progress. **Subcase 2**. : If \(C(f_{j},\rho)\) has less than \(k\) robots on it, then \(N_{j}(t^{\prime})=N_{j}(t)-1\), ensuring significant progress. **Case 2**. : \(r_{i}(t^{\prime})\
eq q(t)\) and \(r_{i}\) is not on any oversaturated \(C(f_{u},\rho)\). In this case \(d_{j}(t^{\prime})+\delta\leq d_{j}(t)\) by Lemma 4, which ensures significant progress. **Case 3**. : \(r_{i}(t^{\prime})\
eq q(t)\) and \(r_{i}\) is on an oversaturated \(C(f_{u},\rho)\). Since at this stage, a candidate robot for \(f_{j}\) will be selected again, algorithm \(CandidateRSelection(C(t^{\prime}),f_{j})\) will select a robot \(r_{k}\) such that \(d(r_{k}(t^{\prime}),f_{j})\leq d(r_{i}(t^{\prime}),f_{j})\). Either \(r_{k}=r_{i}\) or \(r_{k}\
eq r_{i}\). By Lemma 4, significant progress is ensured, in both the cases. Hence, execution of \(MovetoDestination(C(t),f_{j},r_{i})\) ensures significant progress. **Lemma 6**. : _Let \(f_{j}\) be a target fixed point and \(r_{i}\) its unique selected candidate robot at time \(t\).