%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%  New template code for TAMU Theses and Dissertations starting Fall 2012.  
%  For more info about this template or the 
%  TAMU LaTeX User's Group, see http://www.howdy.me/.
%
%  Author: Wendy Lynn Turner 
%	 Version 1.0 
%  Last updated 8/5/2012
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%                           SECTION II
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\chapter{\uppercase {Regional Consecutive Leader Election\\in Mobile Ad Hoc Networks}}
\label{chap:rcle}

%Leader election is a challenging task even in a static infrastructure since node
%and link failures make it necessary to reelect a leader.  In a mobile ad hoc
%environment, leader election becomes even more challenging since link failures
%become the norm due to unrestricted node mobility.  In addition to failures,
%performing leader election among nodes that are connected but far apart from
%each other may cause problems: the amount of time that it takes to elect a leader
%and/or knowing which node became the leader could be significant.

We consider leader election in a fixed
geographic region $R$ with bounded communication diameter which allows leader
election to be performed among nodes that are relatively close to each other
(leader election is performed in a \emph{local} fashion).  By bounded
communication diameter we mean that if a node in $R$ initiates the propagation
of a message at some time $t$, then the message will be relayed through a fixed
maximum number of hops $D$ to any node that stays in the region sufficiently long
after time $t$ --- this is formally defined as $D$-connectedness in Section \ref{sec:rcle:sysmodel}. \blfootnote{Part of this section is reprinted from the following paper:  Hyun Chul Chung, Peter Robinson, and Jennifer L. Welch, ``Optimal regional consecutive leader election in mobile ad-hoc networks,'' In proceedings of the 7th ACM SIGACT/SIGMOBILE Workshop on Foundations of Mobile Computing (FOMC 2011), \copyright 2011 ACM, Inc. Reprinted by permission. http://doi.acm.org/10.1145/1998476.1998485.}  

In this section, we solve the \emph{Regional Consecutive Leader Election} (RCLE)
problem which was originally introduced in \cite{CRW:10}.  Roughly
speaking, the RCLE problem requires the following:\\
(\emph{Agreement}) All nodes in the region that elect a leader elect the same leader.\\
(\emph{Termination}) If some live\footnote{Live nodes are those nodes that have
not yet crashed or have already recovered from a crash. See Section
\ref{sec:rcle:sysmodel}.} node $p$ remains in the region for a sufficiently long
period of time, then $p$ must elect a leader.\\
(\emph{Validity}) If some live node $p$ in the region elects a leader, then that
leader node must have been in the region in the recent past.\\
(\emph{Stability}) If some live node $p$ in the region stops considering
some other node $q$ as the leader, then $q$ has either crashed
or left the region in the recent past.

We provide a lower bound with respect to the (\emph{Termination}) property of
the RCLE problem.  More specifically, we prove that any algorithm requires
$\Omega(Dn)$ rounds for electing a leader, where $D$ is the bounded
communication diameter of the network and $n$ is the total number of nodes in
the system.  Also, we provide a novel algorithm that solves the RCLE problem.  The
provided algorithm guarantees termination in $\mathcal{O}(Dn)$ rounds which
shows that our algorithm is asymptotically tight with respect to time
complexity.  Our algorithm does not rely on the knowledge of the number of nodes
in the system nor on a common start-up time. 

Since the proposed algorithm solves the RCLE problem under the assumption that
the region has a bounded communication diameter, the question arises how to
ensure that the region has a bounded communication diameter?  To answer this
question, we can think of restricting the nodes to follow a certain condition on
mobility.  We provide a novel and intuitive condition on mobility
that ensures the existence of a bounded communication diameter.  The proposed
mobility condition requires nodes to move in a way such that the propagated
information makes a certain amount of progress towards its destination in each
round while not relying on a fixed coordinate system.

\section{Contributions}
%We have provided the following contributions:
%\begin{compactitem}
%\item We define $D$-connectedness which is weaker than usual connectivity assumptions in the sense that it allows scenarios where a set of nodes within the region of interest are temporarily partitioned.
%\item We introduce the RCLE problem by extending the leader election problem to the ever changing environment of mobile ad hoc networks.
%\item We prove a lower bound with respect to the (Termination) property of the RCLE problem and then present and prove correct an asymptotically optimal crash fault-tolerant algorithm that solves the RCLE problem.
%\item We provide a condition on mobility that allows us to obtain a bounded communication diameter within the region of interest.
%\end{compactitem}

We define $D$-connectedness which is weaker than usual connectivity assumptions in the sense that it allows scenarios where a set of nodes within the region of interest are temporarily partitioned.

We introduce the RCLE problem by extending the leader election problem to the ever changing environment of mobile ad hoc networks.

We prove a lower bound with respect to the (Termination) property of the RCLE problem and then present and prove correct an asymptotically optimal crash fault-tolerant algorithm that solves the RCLE problem.

Finally, we provide a condition on mobility that allows us to obtain a bounded communication diameter within the region of interest.


\section{Related Work}
\label{sec:rcle:related}

Geographical information has been widely used in mobile ad hoc environments
(e.g., \cite{KV99,KV00,KK00}). However, there are only a few papers that
consider location information in solving leader election in MANETs.  Chung et
al.\ \cite{CRW:10} provide an algorithm that solves the RCLE
problem with a message bit complexity of $\mathcal{O}(n(\log n +\log r))$ per node per round.  The
algorithm of \cite{CRW:10} runs under the assumption that nodes
have access to synchronized clocks. Also, \cite{CRW:10} provides a condition on
mobility that guarantees the existence of a bounded communication diameter.
However, this mobility condition becomes highly restrictive in some situations
because of the fact that it relies on a fixed coordinate system.  In Section \ref{chap:rcle},
we significantly improve on the results of \cite{CRW:10}, 
by providing an algorithm that solves the RCLE problem with a message bit complexity
of $\mathcal{O}(\log n + \log r)$ per node per round without requiring nodes to have access
to synchronized clocks.  We also provide a mobility condition that is less
restrictive in the sense that it does not rely on any fixed coordinate system.
In addition, we provide a lower bound on the number of rounds for a node to
elect a leader.

In Kuhn et al.\ \cite{Kuhn2011}, the entire geographical space is divided into
regions where nodes in a region forms a single hop network.  A leader is elected
for each region and these leaders form a backbone for message propagation.  Our
approach differs from \cite{Kuhn2011}, since we consider a single fixed region in
which nodes exchange messages through multi-hop communication.

Hatzis et al.\ \cite{HPSTT99} provide an algorithm where a leader is elected by
nodes encountering each other.  When two or more nodes meet, they decide on
which one of them continues to participate in electing a leader.  The entire
space is divided into non-intersecting subspaces and nodes get to meet each
other when they fall into the same subspace.  
Furthermore, a probabilistic analysis is given considering the movement of nodes as
random walks.  In Section \ref{sec:rcle:mobility}, we provide a condition on mobility that
gives a \emph{deterministic} bound on message propagation.   

Leader election algorithms presented in
\cite{BA06,DLP:10,Ingram2013,MWV00,MAB06,PKY04} and \cite{VKT04}
consider a mobile environment where geographical information is \emph{not} used.
In addition, they all consider networks that can have an arbitrarily large
communication diameter.  Our approach considers leader election in a region with
a bounded communication diameter which is a better fit for situations when
leader election is needed only among nearby nodes. 

\section{System Model and Problem Specification}
\label{sec:rcle:sysmodel}

We consider a system consisting of a set $\Pi$ of nodes that move in
  two-dimensional Euclidean space.  
Each node has a unique id and communicates with other nodes via wireless broadcast.

We assume that nodes execute in synchronous rounds of communication
and computation, where each round lasts $\Delta$ time, for an appropriately
chosen value $\Delta$.
Such rounds can be provided by, for instance, the use of the abstract
MAC layer \cite{Kuhn2011}.
This round abstraction allows us to focus on the algorithmic aspects;
  the collision-free scheduling of wireless transmissions, while nevertheless being an
  important problem, is {assumed} by the round abstraction.
It is important to note that the round abstraction does \emph{not} provide nodes
  with additional timing information.
That is, we neither require nodes to be equipped with synchronized clocks nor
  assume that nodes can access the current round number.

Every node executes an instance of a distributed algorithm and is modeled as a 
  deterministic state machine.
In more detail, each round begins with broadcasts by the nodes and
continues with nodes receiving certain broadcasts. 
We denote the (possibly infinite) \emph{set of messages} that can be generated
by the algorithm as $\M$.
At the end of each round, each node uses its current state and the set of
messages received during the round to change its state and decide what to
  broadcast at the beginning of the next round.  
An \emph{execution} of an algorithm is simply an infinite sequence of rounds.

Nodes can \emph{fail} by crashing and might recover from the crash after some
  non-zero number of rounds; a node reinitializes its state upon recovery.
We assume that processing done at the end of each round takes 0 time units and
  only \emph{live} nodes---nodes that have not crashed or have already
  recovered---operate during a round.
As we do not assume that all nodes startup at the exact same time, we simply
  model nodes that have not yet booted (not yet recovered) as crashed nodes.

We focus on a specific {\em region} $R$ of the two-dimensional space
  in which the nodes are present.
Every node has access to geographical information with respect to region $R$ by using functions
  $\EnteredSinceEndOfLastRound()$ and $\Location()$ which can be provided by an underlying location service.

Calling function $\Location()$ yields the exact position in the Euclidean space of the querying node, whereas function $\EnteredSinceEndOfLastRound()$ evaluates to true if (a) the node has entered 
  $R$ since the end of the last round or (b) the node has just recovered from a crash inside $R$.

To specify which broadcasts are received by a node in a round, we
use the notion of two nodes $p$ and $q$ being {\em connected in
the round}:  this means that throughout the round, the Euclidean
distance between $p$ and $q$ is at most $C$, the (common) \emph{communication
radius}.
If $p$ and $q$ are live and connected throughout a round, node $p$ receives exactly
one copy of the message that is broadcast by $q$ at the beginning of
the round ($p$ can also possibly receive a message from a node that is within $C$ at some point during the round).  Thus, communication is timely and reliable, with no lost, corrupted or
spurious messages. 

For each round $r$, we define the following sets of nodes, depending on their
  location with respect to region $R$:
\begin{compactitem}
\item $\Pi_A^r=\{p_i \in \Pi \mid p_i$ is live and within $R$ throughout round $r \}$.
\item $\Pi_E^r=\{p_i \in \Pi \mid p_i$ is live and within $R$ at the end of round $r\}$. 
\item $\Pi_B^r=\{p_i \in \Pi \mid p_i$ is live and within $R$ at the beginning of round $r \}$. 
\end{compactitem}
For rounds $r_a$ and $r_b$ with $r_a \le r_b$,
we define $\Pi_A^{[r_a,r_b]}$ as the set $\{p_i \in \Pi \mid \forall r, r_a \le r \le r_b\colon p_i \in \Pi_A^r \}$. 

Sometimes we only care about a prefix of an execution $S$ until some round $r$; we denote this by $S|_r$.  Executions $S$ and $S'$ are indistinguishable for a node $p$, if $p$ receives the
same messages in $S$ and the values of $\Location()$ and
  $\EnteredSinceEndOfLastRound()$ are the same at $p$ in $S$ and $S'$, for
  all rounds $r$.
Intuitively speaking, node $p$ observes an indistinguishable environment in both
  executions.

Given a particular execution, we define a {\em Just-In-Time (JIT) path
starting at round $r$ from node $p$ to node $q$ of length $m$}
to be a sequence of nodes $p = v_0, v_1 \ldots, v_m = q$ such that,
for all $i$, $0 \le i < m$, $v_i \in \Pi_B^{r+i}$, $v_i$ is live throughout $r+i$, $v_{i+1} \in \Pi_A^{r+i}$, and $v_i$ and $v_{i+1}$ are connected in round $r+i$.

Without any assumptions on the mobility pattern of the nodes,
it is impossible to guarantee the existence of JIT paths.
Thus, we are motivated to assume that every execution satisfies
the following property, which was originally introduced in \cite{CRW:10} and is
also related to the ``dynamic diameter'' of \cite{KMO:11}.

\begin{assumption}[$D$-Connectedness]
\label{assume:rcle:existd}
There exists an integer $D$
such that for every pair of nodes $p$ and $q$, and every round $r$,
the following holds:  if $p \in \Pi_B^{r}$, $p$ is live throughout $r$, and $q \in \Pi_A^{[r,r+D-1]}$, then there exists
a JIT path starting at round $r$ from $p$ to $q$ of length at
most $D$.
\end{assumption}
Intuitively speaking, Assumption~\ref{assume:rcle:existd} guarantees the existence of
  a JIT path from $p$ to $q$, if node $q$ stays sufficiently long inside the region, 
  starting at the time when $p$ sends its message.
We further assume that the value of $D$ is known to all nodes in the system.

\subsection{Problem Specification} 
We assume that every node has access to a special variable $leader$ that is
either set to $\falsum$ or contains a node id.
We denote the value of $leader$ at node $p_i$ at the end of round $r$ as $leader_{p_i}^r$.
If $p_i$ has crashed before or in round $r$ and has not yet recovered (or has not yet booted), 
  we assume that $leader_{p_i}^r=\falsum$.
\begin{definition} \label{def:rcle:RCLE}
An algorithm $A$ solves the \emph{regional consecutive leader election
(RCLE) problem} if there exist integer bounds $B_T$, $B_V$, and $B_S$ such
  that the following properties are satisfied for every D-connected
  execution of $A$:
	\begin{align}
    \label{eq:agreement}\nonumber
      &\forall r\in\mathbb{N}\ \forall p_i,p_j\in \Pi_E^r\colon \Big(
      \left( leader_{p_i}^r \neq \falsum \neq leader_{p_j}^r \right)\\
      &~~~\Rightarrow\ \left( leader_{p_i}^r = leader_{p_j}^r \right)\Big) \tag{\emph{Agreement}} \\
    \label{eq:validity}\nonumber
      &\forall r\in\mathbb{N}\ \forall p_j \in \Pi\colon \Big(\left(\exists
      p_i \in \Pi_E^r \colon leader_{p_i}^r = j\right)\\
      &~~~\Rightarrow \left( \exists r'
      \in \left[r-B_V,r\right] \colon \left( p_j \in \Pi_B^{r'} \wedge leader_{p_j}^{r'} = j\right)\right)\Big) \tag{\emph{Validity}} \\
    \label{eq:termination}\nonumber
      &\forall r\in\mathbb{N}\ \forall p_i \in \Pi\colon \Big(\left(\forall
      r_1 \in \left[r,r+B_T\right]\colon p_i \in \Pi_A^{r_1}\right)\\
      &~~~\Rightarrow
      \left(\exists r_2 \in \left[r,r+B_T\right] \colon leader_{p_i}^{r_2} \neq \falsum
      \right)\Big) \tag{\emph{Termination}} \\   
    \label{eq:stability} \nonumber
    	&\forall r_1,r_2 \in\mathbb{N}\ \forall p_j \in \Pi\colon  
    	\Big(\left( r_1 < r_2 \wedge p_i \in \Pi_A^{[r_1,r_2]} \wedge
    	leader_{p_i}^{r_1} = j \wedge leader_{p_i}^{r_2} \neq j\right) \nonumber \\
    	&~~~\Rightarrow
    	\left(\exists r \in \left[r_1-B_S,r_2\right] \colon p_j \notin \Pi_A^{r}\right)\Big)  \tag{\emph{Stability}}
  \end{align}
\end{definition}
Property \eqref{eq:validity} ensures that only nodes, which have recently been inside the region 
  (i.e.\ within bounded time) and have claimed to be the leader, can be elected
  as the leader, whereas \eqref{eq:stability} guarantees that the leader only
  changes when the previous leader node crashed or is no longer in the region.
Note that (\emph{Termination}) only requires a node to elect
  a leader \emph{if} it remains in the region for a sufficiently long period of
  time.

\section{A Lower Bound on Time Complexity} 
\label{sec:rcle:lowerbound}

In this section, we will prove a lower bound on the time (i.e.\ number of rounds)
  that it takes until a newly incoming node has set its leader variable in the
  worst case.

\begin{lemma} \label{lem:rcle:atLeastD}
Let $A$ be an algorithm that solves the RCLE problem.
Then there is an execution such that the following hold:
  \begin{compactitem}
  \item[(a)] For all $r \in [1,D)$ and for all $p_i\in\Pi_A^{[1,D)}$ we have that
    $leader_{p_i}^r=\falsum$;
  \item[(b)] $|\Pi_A^{[1,\infty)}|=\Theta(n)$.
  \end{compactitem}
\end{lemma}
\begin{proof}
Assume in contradiction that no such execution exists.
First, consider the execution $S$ where all nodes in $\Pi$ are in $\Pi_A^{[1,\infty)}$
  and are all pairwise disconnected during $[1,D)$.
Moreover, in round $D$, the connectivity graph of nodes in the region is fully
  connected, and from round $D+1$ on, the connectivity graph is arbitrary, but with
  the restriction that $D$-connectedness holds.
By assumption, the set of nodes $P\subseteq \Pi_A^{[1,D]}$, such that every $p_i\in P$
  claims to be the leader in some round during $[1,D)$ in $S$, is nonempty.
Due to \eqref{eq:stability}, every node $p_i\in P$ still has $leader_{p_i}^D=i$, which,
  by \eqref{eq:agreement}, implies that $|P|=1$, i.e., $P=\set{p_j}$, for some
  node $p_j$.
Now consider the execution $S'$ that is identical to $S$ for all nodes in
  $\Pi\setminus\set{p_j}$ and where $p_j$ is not inside the region during $[1,D]$.
Clearly $S'$ is indistinguishable from $S$ for all nodes in
  $\Pi\setminus\set{p_j}$ until round $D$, and thus no node inside the region
  terminates before round $D$.
Note that execution $S'$ satisfies (a) and (b), therefore providing a
  contradiction.
%\hfill~
\end{proof}

\begin{theorem} \label{thm:rcle:lowerbound}
Let $A$ be an algorithm that solves the RCLE problem and suppose that
  $A$ satisfies termination with some bound $B_T$. Then it holds that $B_T=\Omega(Dn)$.
\end{theorem}
\begin{proof}
We will show by induction that there exists a permutation $\pi$, a sequence of executions $(S_k)_{1\le k\le n}$, and
  a sequence of rounds $(r_k)_{1\le k\le n}$, such that
  node $p_{\pi(i)}$ takes $r_i\ge iD$ rounds before setting its leader variable
  in execution $S_{i}$, for $1\le i\le n$.

Lemma~\ref{lem:rcle:atLeastD} shows that there is some execution $S_1$ where
  no node terminates before round $D$.
Since algorithm $A$ is correct, some node $p_{\pi(1)}$ is the first one to
  claim to be the leader in some round $r_1\ge D$ in $S_1$; this provides us with the induction base.
Considering property \eqref{eq:validity} we have that
\begin{equation*} \label{eq:allfalse1}
\forall r \in [1,r_1)\ \forall p_j\in \Pi_A^r\colon
  leader_{p_j}^r = \falsum\text{.}
\end{equation*}
Moreover, no other node apart from $p_{\pi(1)}$ can set its leader variable in
round $r_1$. To see why this is the case, assume that $p_{\pi(1)}$ crashed at
the beginning of round $r_1$ and some node $p'$ has $leader_{p'}^{r_1}={\pi(1)}$. 
Clearly, since $p_{\pi(1)}$ crashed and thus never claimed to be the leader, we have a
violation to \eqref{eq:validity}.

Note that we can assume that $p_{\pi(1)}$ is connected to every other 
node in round $r_1$.
We will make use of this assumption in the induction step below.

For the induction step, suppose that, for some $i\in [1,n)$, node $p_{\pi(i)}$ has claimed to be the leader in round
  $r_i$, i.e., $leader_{p_{\pi(i)}}^{r_i}=i$, and assume that
  nodes in $$P=\Pi\setminus\set{p_{\pi(1)},\dots,p_{\pi(i)}}$$ have not yet set their leader variable by round
  $r_i$ in execution $S_i$.
By using the same argument as for $p_{\pi(1)}$ in the induction base, we can
assume that only $p_{\pi(i)}$ sets its leader variable in round $r_i$.
More specifically, the induction hypothesis tells us that
  $$\forall r \in [1,r_{i}] \supseteq [1,iD]\colon leader_{p_j}^r=\falsum\text{,}$$
  for all nodes $p_j\in P$,
  and that $p_{\pi(i)}$ is connected to 
  every node in $\Pi_A^{r_i}$ during round $r_i$.
Now consider the following execution $S_{i+1}$: During rounds $[1,r_i)$, execution $S_{i+1}$ is
  equivalent to the prefix $S_i|_{[1,r_i)}$, but we assume that node
  $p_{\pi(i)}$ exits the region at the end of round $r_i$ in $S_{i+1}$, just before
  electing itself as the leader.
Furthermore, if $i>1$, node $p_{\pi(i-1)}$ reenters the region at the end of $r_i$.
The nodes in $P$ remain in the region forever
  in execution $S_{i+1}$.
Let $\pi(i+1)$ be such that $p_{\pi(i+1)}$ is the first node that claims to be the
  leader in $S_{i+1}$ in some round $r_{i+1} > r_i$.

We will now show that $r_{i+1}-r_i\ge D$.
Suppose that this is false and consider execution $S_{i+1}'$ that is identical
  until round $r_i+D$ to $S_{i+1}$, for all nodes except for $p_{\pi(i)}$.
The only difference is that $p_{\pi(i)}$ does not leave the region, but instead is
  disconnected from all other nodes during rounds $(r_i,r_i+D)$.
Note that this does not violate $D$-connectedness, since by assumption $p_{\pi(i)}$ 
is connected to every node in $\Pi_A^{r_i}$ in $r_i$ and we can assume that 
  execution $S_{i+1}'$ is chosen in a way such that this is also true in $r_i+D$.
Considering that $S_{i+1}'$ is indistinguishable for $p_{i+1}$ from execution $S_{i+1}$ up to round
  $r_i+D-1 \ge r_{i+1}$, node $p_{i+1}$ must claim to be the leader in 
  round $r_{i+1}$, and since \eqref{eq:stability} holds, $p_{i}$ also still claims to be the leader in
  $r_{i+1}$.
As this would be a contradiction to \eqref{eq:agreement}, it follows that
  $r_{i+1}-r_i\ge D$.

By the induction hypothesis and the fact that $A$ satisfies \eqref{eq:validity},
  we have that
  $$\forall r \in [1,r_{i+1}] \supseteq [1,(i+1)D]\colon leader_{p_j}^r=\falsum\text{,}$$
  for any node $p_j \in P\setminus\set{p_{\pi(i+1)}}$ in execution $S_{i+1}$.

This proves that some node $p_{\pi(n)}$ does not terminate before round $nD$, as required.
%\hfill~
\end{proof}

\section{An Optimal RCLE Algorithm}
\label{sec:rcle:algorithm}

The pseudocode of the optimal RCLE algorithm is given in Figures \ref{alg:noClockleader1} and \ref{alg:noClockleader2}.
We will first describe the building blocks of the algorithm
  and then take a closer look at the election process.
We denote the value of variable $var$ at node $p_i$ at the end of round $r$ as $var_{p_i}^r$.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{figure}[tp]
\centering
\begin{framed}
\begin{algorithmic}[1]
  %\myfontsize
  \item[] $\langle$ {\bf Variables and Initialization} $\rangle$
  \STATE $leader, candidate \la \perp$; in $\Pi \cup \set{\perp}$
  \STATE $enteredSince, longest \la -1$; in $\mathbb{Z}$
  \STATE $attemptNum \la 0$; in $\mathbb{N}$
  \STATE $\nullMsg \la \msg{\text{I},0,0,3D,i}$; in $\M$; constant
  \STATE $toSend, prevToSend \la \nullMsg$; in $\M$
  \STATE $Timer\ \waitT, \electT, \leaderT$;
  \EMPTY \hrulefill
  \EMPTY
    \IF{\EnteredSinceEndOfLastRound()} \label{line:rcle:entered}
    	\STATE stop all timers;
    	\STATE initialize variables (as above);
    	\STATE \startTimer($\waitT, 5D$); \label{line:rcle:startWaitT}
    \ENDIF
  	\EMPTY
    \STATE $enteredSince \la enteredSince + 1$;
    \STATE $\update(\recvBuf \cup \set{toSend,prevToSend})$;\label{line:rcle:incTimeStamps}
    \STATE $longest \la \max(longest{+}1,\set{m.entSince \mid m \in \recvBuf})$; \label{line:rcle:maxEarliest}
    \STATE $msg \la \max\set{m\in (\recvBuf\cup\nullMsg)}$; \label{line:rcle:maxMsg}
  	\EMPTY
    \IF{$msg > toSend$} \label{line:rcle:ifMsgToSend}
  		\STATE $toSend \la msg$; \label{line:rcle:assignMsg1}
   		\STATE $attemptNum \la msg.attNum$;
				\IF{$\neg$\running($\waitT$)} \label{line:rcle:notRunningWaitT}
        	\IF{$msg.type = \text{L}$} \label{line:rcle:rcvdLeaderMsg}
            \STATE $leader \la msg.oid$; \label{line:rcle:setOtherLeader}
  					\STATE \startTimer($\leaderT, 2D - msg.age$);\label{line:rcle:startLeaderTOther}
        	\ELSE \label{line:rcle:rcvdInstanceMsg} %ELSIF{$\neg$\running($\waitT$)} 
          	\STATE $leader \la \falsum$; \label{line:rcle:setFalsumLeader}
  	  			\IF{$msg.oid = i$}
  	  				\STATE $candidate \la \perp$;
  	  			\ELSE
  	  				\STATE $candidate \la msg.oid$;
  	  			\ENDIF
          	\STATE \startTimer($\electT,2D - msg.age$); \label{line:rcle:syncElectT}
  				\ENDIF
  			\ENDIF
  	\ENDIF
\end{algorithmic}
\end{framed}
\caption{Optimal RCLE algorithm; code for node $p_i$ (part $1$ of $2$).}
\label{alg:noClockleader1}
\end{figure}  	
  	
\begin{figure}[tp]
\centering
\begin{framed}
\begin{algorithmic}[1]
  %\myfontsize  
  %\EMPTY
  \setalglineno{29}
  \IF{\expired($\waitT$)}\label{line:rcle:expiredWaitT}
    \IF{$(longest > enteredSince) \wedge differ(prevToSend,toSend)$} \label{line:rcle:earliestCheck}
      \STATE $longest \la enteredSince$;
      \STATE $prevToSend \la toSend$;
      \STATE $\startTimer(\waitT,5D)$;
    \ELSE
      \IF{$toSend.type = \text{L}$} \label{line:rcle:endWaitingLeader}
      	\IF{$toSend.oid \neq i$} \label{line:rcle:selfReceiveLeader}
      		\STATE $leader \la toSend.oid$; \label{line:rcle:setOtherLeader2}
      	\ENDIF
        \STATE $\startTimer(leaderT,2D-toSend.age)$;\label{line:rcle:startLeaderTWaitLeader}
      \ELSE
        \STATE $\startTimer(electT,2D-toSend.age)$;\label{line:rcle:startElectTWaitInst}
      \ENDIF
    \ENDIF
  \ENDIF
  \EMPTY
  \IF{\expired($\electT$)} \label{line:rcle:expiredElectT}
    \IF{$candidate = i$} \label{line:rcle:selfCandidate}
        \STATE $leader \la i$; \label{line:rcle:setSelfLeader}
        \STATE $attemptNum \la attemptNum + 1$; \label{line:rcle:incAttemptNum}
        \STATE $toSend \la \msg{\text{L},attemptNum,enteredSince,0,i}$; \label{line:rcle:assignMsg2}
        \STATE \startTimer($\leaderT,D$);\label{line:rcle:startLeaderTInstSelf}
    \ELSE
      \STATE \startTimer($\leaderT,3D-toSend.age$);\label{line:rcle:startLeaderTInstOther}
    \ENDIF
  \ENDIF
  \EMPTY
  \IF{\expired($\leaderT$)}\label{line:rcle:expiredLeaderT}
    \IF{$leader = i$} \label{line:rcle:selfLeader}
      \STATE $toSend \la \msg{\text{L},attemptNum,enteredSince,0,i}$;\label{line:rcle:assignMsg3}
      \STATE \startTimer($\leaderT,D$);\label{line:rcle:startLeaderT}
    \ELSE
      \STATE \startInstance();\label{line:rcle:startInst}
    \ENDIF
  \ENDIF
  \EMPTY
  \IF{$toSend \neq \nullMsg$}
    \STATE broadcast $toSend$ at the start of next round;
  \ENDIF
\EMPTY
\PROC{\startInstance()}
  \STATE $leader \la \perp$; \label{line:rcle:resetLeader2}
    \STATE $candidate \la i$;
    \STATE $attemptNum \la attemptNum + 1$;
    \STATE $toSend \la \msg{\text{I},attemptNum,enteredSince,0,i}$; \label{line:rcle:genInstMsg}
  \STATE \startTimer($\electT,2D$); \label{line:rcle:startTimerElectT}
\ENDPROC
\end{algorithmic}
\end{framed}
\caption{Optimal RCLE algorithm; code for node $p_i$ (part $2$ of $2$).}
\label{alg:noClockleader2}
\end{figure}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%\vspace{-0.2cm}
\subsection{Variables and Timers}  
Since nodes do not have access to clocks, each node employs a local counter
  $enteredSince$ for measuring the number of rounds that have passed since the node entered 
  the region.
On the other hand, local variable $attemptNum$ represents each node's view of the number of times that nodes have attempted to elect a leader.

The algorithm makes heavy use of \emph{timers}, which are local counter
  variables with a special interface that can easily be implemented in any
  round-based system.
By executing $\startTimer(T,of\!fset)$ in round $r$, a node $p_i$ can set its timer
  $T$ to expire in $of\!fset$ rounds.
That is, the predicate $\expired(T)$ will be true in round
  $r+of\!fset$ at $p_i$ and any following round until some other timer has been 
  started.\footnote{Recall that $p_i$ does not know the actual round number,
  as we do not assume access to clocks.}
Also, from the call of $\startTimer(T,of\!fset)$ on until round $r+of\!fset-1$, the
  predicate $\running(T)$ will hold at $p_i$.  Moreover, the call of
  $\startTimer(T,of\!fset)$ will stop any other timer $T'$ at $p_i$ from running (and expiring).

%\vspace{-0.2cm}
\subsection{Message Fields}
A node $p_i$ communicates with other nodes by broadcasting messages 
  consisting of $5$ fields.
If the $oid$ field (see below) of the message contains the id of node $p_g$, we say
  that $p_g$ has \emph{generated} the message.
Considering some round $r_s$, we will now describe the fields of a message $m$ that
  was generated (i.e.\ initially broadcast) by node $p_g$ in round $r_g$ and
  which is broadcast in round $r_s>r_g$ by some node $p_s$:
\begin{compactenum}
\item $type$: We distinguish between so called \emph{leader messages}
  ($m.type=\text{L}$), which are generated only by nodes that claim to be the leader, 
  and \emph{instance messages} ($m.type=\text{I}$).
\item $attNum$: This field contains the value of $attemptNum$ at 
  generator $p_g$ in round $r_g$.
\item $entSince$: The time stamp $entSince$ corresponds to the number of rounds that
  have passed since $p_g$ has entered the region, assuming it has not yet
  exited. That is, $m.entSince = enteredSince_{p_g}^{r_s}$.
\item $age$: The value of $m.age$ is the number of rounds since the message 
  has been generated, i.e., $m.age = r_s - r_g$.
\item $oid$: This field simply contains the id of the generator, i.e.,
  $m.oid=g$.
\end{compactenum}
Note that the values of fields $m.entSince$ and $m.age$ need to be adapted in
  every round, since $p_g$ continuously increases its variable $enteredSince$ as
  long as it is in the region.
This is ensured by calling the function $\update(M)$ in
  Line~\ref{line:rcle:incTimeStamps}, which takes a set $M$ of messages and increases
  the value of $m.entSince$ and $m.age$ by $1$, for every $m\in M$.
For example, if the message $\msg{I,a,e,0,i}$ is generated in round $r$ by node
  $p_i$, its fields will have the values $\msg{I,a,e+k,k,i}$ by round $r+k$.
When we consider a message $m$ with the field values of some specific round $r$, 
  we denote this as $m^r$.
We will omit the superscript $r$, when it is clear from the context.

%\vspace{-0.2cm}
\subsection{Priority and Similarity of Messages}
As we aim for low message complexity, it is important to ensure that relevant information is
  still propagated within the region.
To this end, we introduce a relation on messages, which is first used by the algorithm
  to select the most ``important'' received message $msg$ in Line~\ref{line:rcle:maxMsg}
  and then in Line~\ref{line:rcle:ifMsgToSend}, in order to check if the information
  contained in $msg$ is relevant for the node.

We say that \emph{message $m_1=\msg{t_1,a_1,e_1,r_1,i}$ has priority over
  message $m_2=\msg{t_2,a_2,e_2,r_2,j}$}, denoted by
  $m_1 > m_2$, \emph{iff} one of the following conditions hold:
  \begin{compactenum}
\item $(t_1=\text{L}) \wedge (t_2=\text{L}) \wedge ((a_1 > a_2) \vee ((a_1=a_2) \wedge (r_1<r_2)) \vee
((a_1=a_2) \wedge (r_1=r_2) \wedge (i > j)))$.
  \item $(t_1=\text{I}) \wedge (t_2=\text{L}) \wedge (a_1 > a_2)$.
  \item $(t_1=\text{L}) \wedge (t_2=\text{I})
    \wedge (a_1 \ge a_2)$.
  \item $(t_1=\text{I}) \wedge (t_2=\text{I}) \wedge ((a_1 > a_2)\vee ( (a_1 = a_2) \wedge (e_1 > e_2) ) \vee ( (a_1 = a_2) \wedge (e_1 = e_2) \wedge (r_1 > r_2) ) \vee ( (a_1 = a_2) \wedge (e_1 = e_2) \wedge (r_1 = r_2) \wedge (i>j)))$.
  \end{compactenum}
For two messages of different message types, the message that has a higher value in its $attNum$ field has higher priority than the other; if even the values in their $attNum$ fields are the same, then the leader message takes priority over the instance message.  For two leader messages, the message that has a higher value in its $attNum$ field has higher priority than the other; if the values in their $attNum$ fields are the same, then the one that was generated \emph{later} has priority over the other; if the two messages were even generated at the same round, then the one with the higher $oid$ takes priority over the other.  Finally, for two instance messages, they simply follow lexicographical ordering.

Furthermore, messages $m_1$ and $m_2$ are called \emph{similar}, if they are
  either identical or both leader messages that were generated by the same node, having
  the same value in the field $attNum$.
Predicate $\differ(m_1,m_2)$ (see Line~\ref{line:rcle:earliestCheck}) holds if $m_1$
  and $m_2$ are not similar, formally,
\begin{align}
&\differ(m_1,m_2) \equiv (m_1 \neq m_2) \wedge \neg\left(m_1=\msg{L,a,\_,\_,j} \wedge m_2=\msg{L,a,\_,\_,j}\right). \nonumber
\end{align}
We will make use of this notion of similarity for determining when to exit the
waiting phase (see Section \ref{subsubsec:rcle:waitingphase}).

\subsection{Description of the Election Process} \label{sec:rcle:electionDesc}
Depending on which timer is running ($\waitT$, $\electT$, or $\leaderT$) and 
  the state of variable $leader$, we distinguish nodes to be in one of $3$ phases: waiting phase, election phase, or leader phase.

%\vspace{-0.2cm}
\subsubsection{Waiting Phase}
\label{subsubsec:rcle:waitingphase}
When a node $p_i$ enters the region, it resets its state to the initial configuration
  (Line~\ref{line:rcle:entered} et seq.).  
It also sets its timer $\waitT$ to expire in $5D$ rounds
  (Line~\ref{line:rcle:startWaitT}) and thus starts \emph{waiting} by entering the so called 
  initial {waiting phase}.
Moreover, $p_i$ marks the round when it has entered by setting its variable
  $enteredSince$ to $0$, which will be incremented until $p_i$ leaves the region.
In every computing step, $p_i$ chooses the greatest received message
  (Line~\ref{line:rcle:maxMsg}) with respect to the priority relation and updates its 
  variables $toSend$ and $attemptNumber$ accordingly.
Node $p_i$ also stores the maximum value of the $entSince$ fields of the received
  messages in its variable $longest$, which corresponds to the current value of variable
  $enteredSince$ of the node that has been in the region longest. 
While $p_i$ is in the waiting phase, it restricts itself on forwarding the
  message stored in $toSend$ and performs no computation otherwise.
When the timer $\waitT$ expires for the first time, $p_i$ checks if itself has
  entered the region earliest and if the messages stored in variables
  $prevToSend$ and $toSend$ are not similar. 
If some node has entered before $p_i$ did, $p_i$ will restart $\waitT$ and
  starts another waiting phase of length $5D$ rounds. 
This process will repeat itself until either (a) all
  previously entered nodes have left the region, or (b) $p_i$ has received
  similar messages in two consecutive waiting phases.
Note that the latter will happen when some (previously entered) node claims to
  be the leader. 

%\vspace{-0.2cm}
\subsubsection{Election Phase}
When $p_i$ does not reset its timer $\waitT$, it sets its timer $\leaderT$ or $\electT$
  instead, the expiration of which depends on the message stored in $p_i$'s
  $toSend$ variable; we call nodes where $\neg\running(\waitT)$ is true,
  \emph{``non-waiting''} nodes.
If $p_i$, while running either timer $\leaderT$ or $\electT$, receives an
instance message $m_1$ that has higher priority than the stored
message in its variable $toSend$, then $p_i$ stops the currently running timer and starts timer
$\electT$ with the expiration round being set to $2D-m_1.age$ rounds after the current
round. This allows nodes to synchronize their $\electT$ timers based on the
highest priority message in $R$.
In the round when $\leaderT$ expires, $p_i$ calls $\startInstance()$, assuming
  that $p_i$ has not received a leader message from some other node so far.
In $\startInstance()$, node $p_i$ sets its $\electT$ timer, generates an instance
  message $m_i$ and listens for (higher priority) messages. 
In the round when $\electT$ expires, $p_i$ checks if variable $toSend$ still contains message $m_i$.  If so, node $p_i$ concludes that
  there are no other nodes in the region that have priority and elects itself as
  the leader.
Otherwise, $p_i$ waits for a leader message from the node whose id is stored in
variable $toSend$ (by starting timer $\leaderT$) and updates its leader 
variable upon reception of such a message.

%\vspace{-0.2cm} 
\subsubsection{Leader Phase}
If $p_i$ itself is the leader, it periodically generates leader messages by
expiring and resetting the timer $\leaderT$ every $D$ rounds, until it leaves
the region (or crashes).  If, on the other hand, $p_i$ assumes that some node
$p_j$ is the leader, it simply waits for leader messages from $p_j$ by
periodically setting $\leaderT$.  Should $p_j$ leave the region, $p_i$ will call
$\startInstance()$ (Line~\ref{line:rcle:startInst}) upon expiring timer $\leaderT$,
and return to the election phase.

\subsection{Proof Outline}
In this section, we give a brief intuition why our algorithm
is correct, i.e., satisfies Definition~\ref{def:rcle:RCLE}. 
%The complete correctness proof is relegated to Appendix \ref{app:algoproofs}.

When a node $p$ receives a leader message $m$ and therefore updates its leader variable,
it sets timer $\leaderT$ to expire exactly $2D$ rounds after $m$ was generated. 
If $p$ receives no further leader message, its timer $\leaderT$ will expire and
it will reset its leader variable; thus (validity) holds (see
Lemma~\ref{lem:rcle:validity}).

For (agreement) (see Lemma~\ref{lem:rcle:agreement}), we first observe that the message
priority relation ensures correct propagation of the highest priority message
(Lemma~\ref{lem:rcle:propagation}), which ensures that no two nodes will contain
distinct messages in their $toSend$ variable after the election phase. Moreover,
if some node claims to be the leader, no higher priority instance messages have
been created in the near past (Lemma~\ref{lem:rcle:dominatingLeader}) or will be 
created while the leader does not change
(Corollary~\ref{cor:continousDomination}).

Corollary~\ref{cor:continousDomination} is also instrumental for showing
(stability) (see Lemma~\ref{lem:rcle:stability}), since it is used in the proof of the crucial
Lemma~\ref{lem:rcle:stableLeader}, which states that the leader node does not change
unless it crashes or leaves the region.

The proof of the (termination) (see Lemma~\ref{lem:rcle:termination}) property consists of two parts: First, we show
that if some node $p$ remains in region $R$ for a sufficiently long amount of time
(in the worst case $15D+10(n-1)D$ rounds where $n$ is the total number of nodes),
then $p$ must exit its waiting phase, i.e., $\neg\running(\waitT)$ holds at $p$.
The basic idea behind the proof of this part is that, after every sequence of
$10D$ rounds, if node $p$ decides to remain in the waiting phase, then, during
those 10D rounds, there must be a non-waiting node $q$ that crashed or left the
region.  This idea is enforced by Line~\ref{line:rcle:earliestCheck}, since 
$\differ(prevToSend,toSend)$ becomes true when $p$ decides to stay in the waiting 
period; if, on the other hand, $q$ elected itself as the leader
and stayed alive in $R$ long enough, then $\differ(prevToSend,toSend)$ will
become false, thus causing $p$ to stop waiting.  Even if $q$ reenters region $R$
after leaving $R$, $q$ will not directly cause $p$ to remain in its waiting
phase 
since the condition $longest > enteredSince$ in Line~\ref{line:rcle:earliestCheck} will 
evaluate to false due to $enteredSince_q < enteredSince_p$; note that in this
case $p$ was already inside $R$ when $q$ reenters.

For the rest of the termination proof, we show that if node $p$ remains in
region $R$ sufficiently long enough after exiting its waiting phase (in the
worst case $7D+4(n-1)D$ rounds), then $p$ elects a leader by setting its leader
variable. The worst case scenario would be that all ``better'' candidate leaders 
leave region $R$ or crash sparsely (i.e.\ one-by-one)
without ever electing themselves as the actual leader and, finally, $p$ electing 
itself as the leader.  The basic idea behind the proof of this part is that the nodes that
enter $R$ after $p$ exits its waiting phase will keep waiting as long as $p$ is 
live and does not elect a leader (which is the case by assumption). This
is true because $p$, along with the other non-waiting nodes in $R$, will 
generate new instance messages at least every $4D$ rounds.
Our $D$-connectedness assumption ensures that nodes in their waiting phase
receive new instance messages at least every $5D$ rounds so when 
Line~\ref{line:rcle:earliestCheck} is executed, it will evaluate to true, causing these
nodes to keep waiting.

\subsection{Proof of Correctness}

The following lemma follows directly by inspecting the code.

\begin{lemma} \label{lem:rcle:toSendAttemptNumPair}
Suppose that $p_i \in \Pi_A^{[r,r+k]}$, for some $k\ge 0$.
Then, for all $r' \in [r,r+k]$,
\begin{compactenum}
\item[(a)] $toSend_{p_i}^{r'}.attNum = attemptNum_{p_i}^{r'}$.  
  %In other words, at the end of each round that $p_i$ was live and in region $R$, the value in the $attNum$ field of the message in the $toSend$ variable is the same as the value in the $attemptNum$ variable.
\item[(b)] $attemptNum_{p_i}^{r'}$ is non-decreasing.
\end{compactenum}
\end{lemma}

\begin{lemma} \label{lem:rcle:toSendMonotonic}
Suppose that $p_i \in \Pi_A^{[r,r+k]}$, for some $k\ge 0$.
Then, for all $r'\in [r+1,r+k]$ where $\update(toSend_{p_i}^{r'-1}) \neq
toSend_{p_i}^{r'}$, we have that $toSend_{p_i}^{r'} >
toSend_{p_i}^{r'-1}$ and 
$toSend_{p_i}^{r'}.attNum \geq toSend_{p_i}^{r'-1}.attNum$.
\end{lemma}
\begin{proof} 
  Let $m_1 = toSend_{p_i}^{r'-1}$ and $m_2 = toSend_{p_i}^{r'}$.  Now,
  suppose in contradiction, for some $r'\in [r+1,r+k]$ where 
  \begin{align} \label{eq:notEq}
  \update(m_1) \neq m_2\text{,}
  \end{align}
  it holds that $$(m_2 \leq m_1) \vee (m_2.attNum <
  m_1.attNum)\text{.}$$  By \eqref{eq:notEq}, message $m_2$ must be assigned to $toSend_{p_i}^{r'}$ by either
  line~\ref{line:rcle:assignMsg1}, line~\ref{line:rcle:assignMsg2},
  line~\ref{line:rcle:assignMsg3}, or line~\ref{line:rcle:genInstMsg}.  We consider four
  cases: \\ (\emph{Case 1}) $m_2$ was assigned to $toSend_{p_i}^{r'}$ by
  line~\ref{line:rcle:assignMsg1}: In order for $m_2$ to be assigned by
  line~\ref{line:rcle:assignMsg1}, the if-condition in line~\ref{line:rcle:ifMsgToSend}
  must evaluate to true which directly yields a contradiction.\\ (\emph{Case 2})
  $m_2$ was assigned to $toSend_{p_i}^{r'}$ by line~\ref{line:rcle:assignMsg2}:
  Notice that $attemptNum$ is incremented just before executing
  line~\ref{line:rcle:assignMsg2}.  Hence, Lemma \ref{lem:rcle:toSendAttemptNumPair}.(a)
  tells us that $m_1.attNum < m_2.attNum$ which yields $m_1 < m_2$ by the
  definition of the message priority relation, a contradition.\\ (\emph{Case 3})
  $m_2$ was assigned to $toSend_{p_i}^{r'}$ by line~\ref{line:rcle:assignMsg3}: If
  $m_1.type = I$, then Lemma \ref{lem:rcle:toSendAttemptNumPair} implies that
  $m_1.attNum \leq m_2.attNum$.  Hence, the definition of the message priority
  relation gives us $m_1 < m_2$ since $m_2.type = L$, a contradiction.  If
  $m_1.type = L$, then, due to line~\ref{line:rcle:incTimeStamps}, $m_1$ becomes at
  least 1 rounds old (i.e., $m_1.age \geq 1$).  Also, by Lemma
  \ref{lem:rcle:toSendAttemptNumPair}, we know that $m_1.attNum \leq
  m_2.attNum$.
  Hence, by the definition of the message priority relation, we always get $m_2
  > m_1$ since $m_1.age < m_2.age$ at round $r'$ ($m_1.age \geq 1$ and $m_2.age
  = 0$ at round $r'$), a contradiction.\\ (\emph{Case 4}) $m_2$ was assigned to
  $toSend_{p_i}^{r'}$ by line~\ref{line:rcle:genInstMsg}: The proof is similar to
  (\emph{Case 2}).
\end{proof}

\begin{lemma} \label{lem:rcle:beforeLeader}
  The following statements are true if $leader_{p_i}^r = p_i$:
  \begin{compactenum}
  \item[(a)] Node $p_i$ did not pass the if-condition in Line~\ref{line:rcle:ifMsgToSend}
    during rounds $(r-2D,r]$.
  \item[(b)] $p_i \in \Pi_E^{r-5D}$ and $p_i \in \Pi_A^{(r-5D,r]}$.
  \end{compactenum}
\end{lemma}
\begin{proof}
  \emph{(a)}. Assume in contradiction that $p_i$ received a message $m$ that enabled it to pass 
    the if-condition in Line~\ref{line:rcle:ifMsgToSend} in some round $r' \in (r-2D,r]$. We divide into two cases:\\
    (\emph{Case 1}) $\running(\waitT)$ holds at $p_i$ at round $r'$: There must exist a round during $(r',r]$ where $\neg\running(\waitT)$ holds at $p_i$ since $leader_{p_i}^r \neq \falsum$.  Let $r'' \in (r',r]$ be the earliest round when $\neg\running(\waitT)$ holds at $p_i$.  Note that $r-r'' <2D$.  Considering that, after the generation of an instance message by $p_i$, it requires exactly $2D$ rounds to execute Line~\ref{line:rcle:setSelfLeader}, $leader_{p_i}$ must be set to $p_i$ using Line~\ref{line:rcle:setOtherLeader} during $[r'',r]$.  This implies that $p_i$ received a leader message $m_l$ that was generated by itself.  If $m_l$ was generated at $r_l \in [r'',r]$, then Line~\ref{line:rcle:ifMsgToSend} will prevent Line~\ref{line:rcle:setOtherLeader} from being executed since $toSend_{p_i}^{r_l}$ already contains $m_l$ and, in any subsequent rounds after $r_l$, $toSend_{p_i}$ contains $m_l$ or some message that has higher priority than $m_l$ (by Lemma~\ref{lem:rcle:toSendMonotonic}), a contradiction.  If $m_l$ was not generated during $[r'',r]$, then it must have been generated before or at round $r''-5D$ because of the fact that every node stays in their waiting phase for at least $5D$ before $\neg\running(\waitT)$ holds and during the waiting phase no messages are generated.  This shows that $m_l.age > 2D$ at round $r''$.  Then, at round $r''$, the if-condition at Line~\ref{line:rcle:endWaitingLeader} evaluates to true, however, $leader_{p_i}$ will not be set by Line~\ref{line:rcle:setOtherLeader2} (it will remain as $leader_{p_i} = \falsum$) since $m_l.oid = p_i$, a contradiction.\\ 
    (\emph{Case 2}) $\neg\running(\waitT)$ holds at $p_i$ at round $r'$: If $m.type = L$ and $m.oid = p_i$, then, similar to (\emph{Case 1}), it must be that $m$ was generated before the most recent round when $p_i$ entered region $R$ ($m$ was generated at least $5D$ rounds before round $r$).  Since $\neg\running(\waitT)$ holds at $p_i$ at round $r'$, there exists a round $r_e$ ($\leq r'$) where $\neg\running(\waitT)$ holds at $p_i$ at round $r_e$ and $\running(\waitT)$ holds at $p_i$ at round $r_e-1$.  Note that $m.age \leq r_e-5D$ at round $r_e$.  Thus, similar to (\emph{Case 1}), at round $r_e$, the if-condition at Line~\ref{line:rcle:endWaitingLeader} evaluates to true, however, $leader_{p_i}$ will not be set by Line~\ref{line:rcle:setOtherLeader2} (it will remain as $leader_{p_i} = \falsum$) since $m.oid = p_i$.  This implies that $toSend_{p_i} \geq m$ by the end of round $r_e$.  Hence, by Lemma~\ref{lem:rcle:toSendMonotonic} and the fact that $r' \geq r_e$, $p_i$ cannot evaluate the if-condition in Line~\ref{line:rcle:ifMsgToSend} to true, a contradiction.
    
    If $m.type = I$ or ($m.type = L$ and $m.oid \neq p_i$), there must exist a round $r'' \in [r',r]$ where either Line~\ref{line:rcle:setOtherLeader} or Line~\ref{line:rcle:setSelfLeader} is executed.  The rest of the proof is similar to (\emph{Case} 1).
    
\emph{(b)}. The proof is immediate by inspecting the code; after node $p_i$ enters region $R$, it runs its $\waitT$ timer at least $5D$ rounds and while timer $\waitT$ is running, $p_i$ does not update its $leader$ variable (Lines~\ref{line:rcle:rcvdLeaderMsg} to \ref{line:rcle:syncElectT} are not executed).
\end{proof}

\subsubsection{Agreement and Validity}

\begin{lemma}[Priority Propagation] \label{lem:rcle:propagation}
Suppose that $p_1$ broadcasts a message $m$ in round $r$.
Then, for every $p_j \in \Pi_A^{[r,r+D]}$, it holds that $toSend_{p_j}^{r+D} \ge m^{r+D}$.
\end{lemma}
\begin{proof}
For the sake of a contradiction, assume that there exists some node $p_j\in\Pi_{A}^{[r,r+D]}$
  such that $p_j$ has $toSend_{p_j}^{r+D}<m^{r+D}$.
We know that there exists a JIT path from $p_1$ to $p_j$ starting in round $r$; w.l.o.g.,
  assume that this JIT path is $p_1\rightarrow p_2\rightarrow \dots \rightarrow p_k \rightarrow
  \dots \rightarrow p_j$, where $p_k$ is the first node that 
  has $toSend_{p_k}^{r+k-1}<m^{r+k-1}$.
We will now show by induction that for $i\in [1,k]$, every node $p_i$, 
  on the JIT path has $toSend_{p_i}^{r+i-1}\ge m^{r+i-1}$, which, together with
  Lemma~\ref{lem:rcle:toSendMonotonic}, yields the required contradiction.
For the induction base, we have by assumption that $toSend_{p_1}^r=m^r$.
For $i>1$, the induction hypothesis tells us that $toSend_{p_{i-1}}^{r+i-2}\ge
  m^{r+i-2}$. 
Moreover, by assumption $p_i$ has an incoming link from $p_{i-1}$ during round
$r+i-1$, thus clearly $toSend_{p_i}^{r+i-1}\ge m^{r+i-1}$. 
What remains to show is that for all $r'\in (r+i-1,r+D]$, we have that 
$toSend_{p_i}^{r'}\ge m^{r'}$. But this follows directly from the message
priority relation and Lemma~\ref{lem:rcle:toSendMonotonic}.
\end{proof}


\begin{lemma}[Dominating Leader] \label{lem:rcle:dominatingLeader}
Let $p_\ell$ be a node in $\Pi_A^{[r_\ell,r_\ell+D]}$ that generates $m_\ell = \msg{L,a_\ell,\_,0,\ell}$ in
  round $r_\ell$ and suppose that
  $toSend_{p_\ell}^{r_\ell-1}.type\neq L$; that is, $p_\ell$ claims to be the
  new leader in round $r_\ell$.
Then, no instance message $m_j$ with $a_j>a_\ell$ is generated during $[r_\ell-3D,r_\ell+D)$.
\end{lemma}
\begin{proof}
Assume in contradiction that some node $p_j$ generates such a message $m_j$ in
  round $r_j$.  We divide into two cases:\\
(\emph{Case 1}) $r_j \in [r_\ell - 3D, r_\ell - D]$: 
  By Lemma~\ref{lem:rcle:propagation}, $p_\ell$ must receive a message $m$ with
  $$m.attNum\geq m_j.attNum > attemptNum_{p_\ell}$$ by round $r_\ell$, contradicting
  Lemma~\ref{lem:rcle:toSendAttemptNumPair}.\\
(\emph{Case 2}) $r_j \in (r_\ell - D,r_\ell+D]$: We know that $expired(\leaderT)$ holds for
  node $p_j$ in round $r_j$; let $m_j'$ be the message that was in
  variable $toSend_{p_j}$ when $p_j$ passed Line~\ref{line:rcle:expiredLeaderT}.
Note that 
\begin{equation} \label{eq:attNum}
  m_j'.attNum = m_j.attNum-1\geq m_\ell.attNum
\end{equation}
by assumption.
Since $p_j$ called $\startInstance()$ in Line~\ref{line:rcle:startInst}, we know 
  that $leader_{p_j}\neq j$.
Thus, $p_j$ did not set $\leaderT$ using
  Line~\ref{line:rcle:startLeaderT} and we can observe that timer 
  $\leaderT$ is always set such that its expiration date is at least 
  $2D$ later than the round when $m_j'$ was generated.
It follows that $m_j'$ was broadcast  (not necessarily by $p_j$) during rounds
  $[r_j-2D,r_j)$.
By Lemmas~\ref{lem:rcle:propagation}, it follows that $p_\ell$ has set its $toSend$
variable to some message $m''\ge m_j'$ by round $r_\ell-1$.

First consider the case where $m''.type={L}$: The priority
relation together with \eqref{eq:attNum} imply a contradiction to 
$toSend_{p_\ell}^{r_\ell-1}\neq L$.
If $m''.type=I$, then the execution of Line~\ref{line:rcle:incAttemptNum} by $p_\ell$
in $r_\ell$ provides a contradiction to \eqref{eq:attNum}. 
\end{proof}

\begin{corollary}[Continuously Dominating Leader] \label{cor:continousDomination}
Suppose that there is an integer $\lambda>0$, such that node $p_\ell$ generates leader messages 
  in every round in $\set{ r_\ell + kD \mid k \in [0,\lambda] }$, which all have
  the fixed value $a_\ell$ in the field $attNum$, and suppose that
  $toSend_{p_\ell}^{r_\ell-1}.type\neq L$.
Then, no instance message $m_j$ with $a_j>a_\ell$ is generated during 
  the interval of rounds $[r_\ell-3D,r_\ell+\lambda D)$.
\end{corollary}
\begin{proof}
%The proof uses induction over $2k$, for $k\in [0,\lambda)$.
Assume in contradiction that some node generates a message $m_j$ with
$a_j>a_\ell$ in round $r\in[r_\ell-3D,r_\ell+(\lambda-1)D]$. 
The case $r\in[r_\ell-3D,r_\ell+D]$ follows immediately by Lemma~\ref{lem:rcle:dominatingLeader}.

Next, we will show that the result also holds for $r\in[r_\ell+D,r_\ell+(\lambda-1)D]$.
By Lemma~\ref{lem:rcle:propagation}, it follows that $p_\ell$ will receive a message
$m'\geq m_j$ by round $r+D$, causing it to pass Line~\ref{line:rcle:ifMsgToSend}. But
since, $p_i$ still generates a leader message $m'$ in some round in
$r_\ell+\lambda D$ with $m'.attNum=a_\ell$, this is a contradiction.

Finally, we need to consider the case where $r\in
(r_\ell+(\lambda-1)D,r_\ell+\lambda D]$, for $\lambda >1$:
Note that node $p_j$ must have called $\startInstance()$ in round $r$ after its
$\leaderT$ timer expired. Let $m'$ be the message that caused $p_j$ to
previously set $\leaderT$, i.e., $toSend_{p_j}^{r-1}=m'$. Note that 
$m'$ (or some greater message) is also received by $p_\ell$.
Moreover, since node $p_j$ must have previously been in the waiting phase, we
know that $p_j \in \Pi_A^{(r-5D,r]}$, i.e., $p_j$ has received some leader
message generated by $p_\ell$. Therefore, either $p_\ell$ passes the
if-condition in Line~\ref{line:rcle:ifMsgToSend} upon receiving $m'$, and thus does
not generate a leader message in round $r_\ell+\lambda D$, or $p_j$ does not
pass the if-condition in Line~\ref{line:rcle:ifMsgToSend} upon receiving $m'$, and
thus does not set its timer $\leaderT$ to expire according to $m'.age$. 
Both cases yield a contradiction.
\end{proof}

\begin{lemma}[Validity] \label{lem:rcle:validity}
  The algorithm in Figures \ref{alg:noClockleader1} and \ref{alg:noClockleader2} satisfies property (validity) with
  bound $B_V=2D-1$.
\end{lemma}
\begin{proof}
Suppose that some node $p_i$ has $leader_{p_i}^{r}=j$.
This implies that $p_i$ is no longer in the waiting phase, and thus
  $\neg\running(\waitT)$ holds at $p_i$ in round $r$.
If $i = j$, then \eqref{eq:validity} trivially holds; therefore
  assume that $i \neq j$.  
By the code, if $p_i$ sets $leader_{p_i} \la j$ then $p_i$ has received a leader 
  message $m$ generated by node $p_j$ in round $r_j$, i.e.,
  $toSend_{p_i}^{r_i}=m$, for some round $r_i$.  
Note that $p_i$ sets its timer $\leaderT$ to expire in round $r_j+2D$.
W.l.o.g., we can assume that $r_i$ is the round where $p_i$ updates its $leader$
  variable the last time before $r$.
Again, by the code, it follows that if $p_i$ received any message $m'>m$ during
  $(r_i,r]$, it would update its $leader$ variable, which is a contradiction; thus we have that
  $toSend_{p_i}^{r}=m^r$.
If $m^{r}.age\ge 2D$, then $\expired(\leaderT)$ would have been true in some
  round in $[r_i,r]$, and hence $leader_{p_i}^{r}\neq j$ by
  Line~\ref{line:rcle:resetLeader2}, again yielding a contradiction.
On the other hand, if  $m^{r}.age< 2D$, it follows that $r_j\ge r-2D+1$, which
  means that $p_j$ was inside the region in round $r-2D+1$ or some later round,
  i.e., $B_V=2D-1$, as required.    
\end{proof}

\begin{lemma}[Agreement] \label{lem:rcle:agreement}
The algorithm in Figures \ref{alg:noClockleader1} and \ref{alg:noClockleader2} guarantees property \eqref{eq:agreement}.
\end{lemma}
\begin{proof}
For the sake of a contradiction, assume that there is a $D$-connected
  execution where property \eqref{eq:agreement} is violated the first time in
  some round $r_2$, and let $p_1$ and $p_2$ be nodes such that
  $leader_{p_1}^{r_2} = v_1 \neq v_2 = leader_{p_2}^{r_2}$.
Without loss of generality, let $r_1$ be the round when $p_1$ has updated
  $leader_{p_1}$ the last time before $r_2$ and assume that $r_1\leq r_2$.
Depending on how $p_1$ and $p_2$ updated their variable $leader$ 
  (Lines~\ref{line:rcle:setOtherLeader} or \ref{line:rcle:setSelfLeader}; the case of using Line~\ref{line:rcle:setOtherLeader2} will be analogous to the case of using Line~\ref{line:rcle:setOtherLeader}), we distinguish several cases:\\
(\emph{Case 1}) Nodes $p_1$ and $p_2$ both used Line~\ref{line:rcle:setSelfLeader} (i.e., $p_1$ and $p_2$ both
  claim to be the leader):  
This implies that $p_1$ and $p_2$ both passed the check
  $\expired(\electT)$
  in Line~\ref{line:rcle:expiredElectT}. 
By Lemma~\ref{lem:rcle:beforeLeader}.(b), we
  know that $p_1 \in \Pi^{(r_1-2D,r_2]}_A$ and $p_2 \in \Pi^{(r_2-2D,r_2]}_A$.
Let $m_1$ resp.\ $m_2$ be the instance messages generated by $p_1$ resp.\ $p_2$
  in round $r_1-2D$ resp.\ round $r_2-2D$:\\
(\emph{Case 1a}) $r_1 \leq r_2-D$: Let $m_\ell$ be the leader message
  generated by $p_1$ in round $r_1$. 
By Lemma~\ref{lem:rcle:propagation}, we know
  that $p_2$ must have received some message $m_1'\ge m_\ell$  by round $r_2$.
By assumption, $p_2$ could not have passed Line~\ref{line:rcle:ifMsgToSend},
  therefore, $m_2 > m_1$. 
Since $p_1$ remains inside the region until round $r_2$, however, it follows
  again by Lemma~\ref{lem:rcle:propagation} that $p_1$ must have also received some
  message $m_2'\ge m_2 > m_\ell$ by round $r_2$, causing $p_1$ to reset its
  $leader$ variable and thus yielding a contradiction.\\
(\emph{Case 1b}) $r_1 > r_2-D$: Since $r_1-2D \le r_2-2D$, it follows
by Lemma~\ref{lem:rcle:beforeLeader}.(b) that nodes $p_1$ and $p_2$ are in $\Pi_A^{(r_2-2D,r_2-D]}$.
Then, because of Lemma~\ref{lem:rcle:propagation}, we know that either $p_1$ or $p_2$ passes
the if-condition in Line~\ref{line:rcle:ifMsgToSend} in some round in $(r_2-2D,r_2-D]$.
Applying Lemma~\ref{lem:rcle:beforeLeader}.(a) provides a contradiction.\\
(\emph{Case 2}) $p_1$ used Line~\ref{line:rcle:setSelfLeader} and $p_2$ used
  Line~\ref{line:rcle:setOtherLeader}: 
This implies that $p_2$ received a leader message from some distinct node
  $v_2$.
Let $r_v$ be the most recent round before round $r_2$ in which $v_2$ considers itself as the
  leader, i.e., $r_v < r_2$ and $v_2 \in \Pi_E^{r_v}$.
Recall the assumption that the first violation of agreement happened in round $r_2$.
It follows that $r_v<r_1$, otherwise this violation would have already taken
  place in round $r_v$.
We distinguish several cases, depending on when $r_v$ takes place:\\
(\emph{Case 2a}) $r_1 - 2D > r_v$:
Since $r_2\ge r_1$ we have $r_2 - 2D > r_v$. 
Considering that node $v_2$ does not generate any leader messages during 
$(r_v,r_2)$, it follows by the fact that $p_2$ received such a message in $r_2$ 
that $p_2$ sets its timer $\leaderT$ according to the $age$ field of $v_2$'s leader message $m_v$.
Clearly we have $m_v.age>2D$, and thus $\expired(\leaderT)$ holds in
round $r_2$, causing $p_2$ to reset its $leader$ variable to $\falsum$,
a contradiction.\\
(\emph{Case 2b}) $r_1 - D \ge r_v$:
By (Case~2a) we know that $r_v \ge r_1 - 2D$, i.e., $r_v \in [r_1-2D,r_1-D]$.
Since $v_2$ is in $\Pi_E^{r_v}$, applying
Lemma~\ref{lem:rcle:propagation} shows that $p_1$ receives some message $m'$ that is
at least as high as $v_2$'s leader message $m$ in some round $r' \in (r_v,r_1]$. 
By assumption, $p_1$ does not pass the if-condition in
Line~\ref{line:rcle:ifMsgToSend}, therefore $p_1$'s instance message $m_1>m'$.
On the other hand, we know that $p_2$ does pass Line~\ref{line:rcle:ifMsgToSend} in
round $r_2$ by receiving $m$, i.e., $m_1>m'\geq m$. Since $p_1$ sends $m_1$ in
round $r_1-2D$, Lemma~\ref{lem:rcle:propagation} tells us that $p_2$ must have
received a message that is at least as great as $m_1$ before round $r_2$.
Therefore, $p_2$ cannot pass Line~\ref{line:rcle:ifMsgToSend} in round $r_2$ by
receiving $m$.\\ 
(\emph{Case 2c}) $r_1 - D < r_v$:
We know that $r_v < r_1$, which means that $r_v \in (r_1-D,r_1)$.
The proof is similar to (Case 2b). In particular, it follows that the instance
message $m_1$ must be greater than the leader message $m$ of $v_2$, which in turn
means that $p_2$ cannot have pass Line~\ref{line:rcle:ifMsgToSend} in round $r_2$ by
receiving $m$.\\ 
(\emph{Case 3}) 
  $p_1$ used Line~\ref{line:rcle:setOtherLeader} and $p_2$ used
  Line~\ref{line:rcle:setSelfLeader}: This implies that $p_1$ received a leader
  message $m_v$ from node $v_1$.  
  Let $r_v$ be the most recent round before $r_1$
  that $v_1$ considers itself as the leader, i.e., $r_v<r_1$.
  We further distinguish two cases:\\
(\emph{Case 3a}) $r_1 \leq r_2-D$: 
  Note that, by Lemma~\ref{lem:rcle:propagation}, $p_2$ must have received some
  message $m'\geq m_v$ by round $r_2$, but since $p_2$ does not pass the
  if-condition in Line~\ref{line:rcle:ifMsgToSend}, it must be that $m_2>m'\geq m_v$. Moreover, $p_1$ receives $m_2$
  before round $r_2$, and since $p_1$ still has $leader_{p_1}^{r_2}=v_1$, 
  $p_1$ does not pass Line~\ref{line:rcle:ifMsgToSend} during $(r_1,r_2]$,
  contradicting the fact that $m_2>m_v$.\\
(\emph{Case 3b}) $r_1 > r_2-D$:   
First, assume that $r_v \leq r_2-D$:
By Lemma~\ref{lem:rcle:propagation}, we know that $p_2$ receives some message $m'\geq
m_v$ by round $r_2$, and, by Lemma~\ref{lem:rcle:beforeLeader}.(a), we have
$m_2>m'>m_v$. Moreover, $p_1$ receives some message $m''\geq m_2>m_v$ by round
$r_1$, thus it cannot be that $leader_{p_1}^{r_2}=v_1$.
For the case where $r_v > r_2-D$, we can use an analogous argument as in (Case~2c).\\
(\emph{Case 4}) $p_1$ and $p_2$ both used Line~\ref{line:rcle:setOtherLeader}: 
This implies that there are distinct nodes $v_1$ and $v_2$ that generate 
  leader messages in rounds $r_1'(\leq r_1-1)$ and $r_2'(\leq r_2-1)$, respectively. 
We assume that $r_1' \le r_2'$; the case $r_1'>r_2'$ follows analogously.
Note that $p_1$ receives the leader message $\msg{L,a_1,\_,v_1}$ from $v_1$ in 
  round $r_1$.
Clearly it holds that $r_2'-r_1'<2D$, otherwise
$p_1$ would have executed $\startInstance()$ in Line~\ref{line:rcle:startInst} and updated its leader
  variable during $(r_1,r_2]$, therefore violating the assumption that $r_1$ was the last
  update before $r_2$.
Thus we can restrict our treatment to two cases:\\
(\emph{Case 4a}) $r_1' \in (r_2'-2D,r_2'-D)$:
We know that $leader_{v_2}^{r_1'} \neq v_2$, since we assumed that the
\emph{first} violation of agreement happened at $r_2>r_1'$.  Considering that
$leader_{v_2}^{r_2'} = v_2$, it follows that the $electT$ timer of node
$v_2$ must expire in some round $r_2''\in (r_1',r_2']$.  It follows that the
instance message in $toSend_{v_2}$ must be greater than the leader message
generated by $v_1$ in round $r_1'$, otherwise $r_2$ would have passed
Line~\ref{line:rcle:ifMsgToSend}, contradicting Lemma~\ref{lem:rcle:beforeLeader}.(a). 
But this directly contradicts Corollary~\ref{cor:continousDomination}.\\
(\emph{Case 4b}) $r_1' \in [r_2'-D,r_2')$:
By Lemma~\ref{lem:rcle:beforeLeader}.(b), we know that $v_1 \in \Pi_E^{r_1'-2D}$ and $v_1 \in \Pi_A^{(r_1'-2D,r_1']}$.

First suppose that both, $v_1$ and $v_2$ generate their respective first leader
message in round $r_1'$ resp.\ $r_2'$. Then, by Lemma~\ref{lem:rcle:propagation} it
follows that one of them will receive a message greater than or equal to the instance 
message of the respective other node, and thus pass Line~\ref{line:rcle:ifMsgToSend}
during $[r_2'-D,r_2')$, a contradiction. 

If both, $v_1$ and $v_2$ have also generated a leader message in $r_1'-D$
resp.\ $r_2'-D$, we immediately have a contradiction to the assumption that 
$r_2$ is the earliest round when agreement is violated.
Now consider the case where $v_2$ also generates a leader message in $r_2'-D$,
while $v_1$ still has $leader_{v_1}^{r}\neq v_1$ for $r\in [r_1',r_1'-2D]$. It
follows that $v_1$ receives the message that was in
$toSend_{v_2}^{r_2'-2D}$ before round $r_1'$. If
$toSend_{v_2}^{r_2'-2D}.type=L$, we know by Corollary~\ref{cor:continousDomination} 
that $v_1$ will pass Line~\ref{line:rcle:ifMsgToSend}, which contradicts
Lemma~\ref{lem:rcle:beforeLeader}. On the other hand, if
$toSend_{v_2}^{r_2'-2D}.type=I$ and $v_1$ does not pass
Line~\ref{line:rcle:ifMsgToSend}, then, by Lemma~\ref{lem:rcle:propagation}, $v_2$ will
receive some message equal or greater to $v_1$'s instance message and pass
Line~\ref{line:rcle:ifMsgToSend}, a contradiction. 
\end{proof}

%The next lemma follows immediately from inspecting the code:
%\begin{lemma} \label{lem:rcle:electTwaitTexpiring}
%The timer $\electT$ is always set to expire after $2D$ rounds and
%Timer $\waitT$ is always set to expire after $3D$ rounds.
%\end{lemma}

%To ensure agreement holds when a node $p_i$ enters $R$,  
%  $p_i$ should wait for existing leader messages before 
%  claiming to be the leader.
%Moreover, a node elects itself as the leader only if it is unaware of any
%  other leader and there is no other higher priority leader election instance in
%  progress:

\subsubsection{Stability}

\begin{lemma} \label{lem:rcle:leaderNoWaitAndElectTimer}
Suppose that $leader_{p_i}^{r} = p_i$. Then, at round $r$, $p_i$ does not run its $\waitT$ nor its $\electT$ timer, i.e.,  
$\neg\running(\waitT)_{p_i}^r \wedge \neg\running(\electT)_{p_i}^r$ hold.
\end{lemma}
\begin{proof}
Note that the only place where $p_i$ sets its leader variable to its \emph{own}
  id is in Line~\ref{line:rcle:setSelfLeader}.
First, assume that $\running(\waitT)_{p_i}^r$ holds.
Observe that timer $\waitT$ is only set in Line~\ref{line:rcle:startWaitT} upon $p_i$
  entering the region in some round $r_1<r$. 
Moreover, $p_i$ does not start any other timer until $\waitT$ has expired. Thus
  $p_i$ does not pass Line~\ref{line:rcle:expiredElectT} during $[r_1,r]$, 
  a contradiction.

Now, suppose that $\neg\running(\electT)_{p_i}^r$ holds.
In that case $p_i$ must have executed $\startTimer(\electT,2D)$ in
  Line~\ref{line:rcle:startTimerElectT}, which means that $p_i$ has reset its leader
  variable in Line~\ref{line:rcle:resetLeader2}. 
Again, $p_i$ does not pass Line~\ref{line:rcle:expiredElectT} before round $r$, which
  provides the contradiction.
\end{proof}

The next lemma shows that if a node claims to be the leader, it continues to do
  so until it crashes or leaves the region.

\begin{lemma} \label{lem:rcle:stableLeader}
Suppose that $leader_{p_i}^{r_1}=p_i$ and $p_1 \in \Pi_A^{(r_1,r_2]}$.
Then it holds for all $r \in (r_1,r_2]$ that $leader_{p_i}^{r}=p_i$.
\end{lemma}
%The complete formal proof of Lemma~\ref{lem:rcle:stableLeader} can be found in Appendix~\ref{sec:rcle:app}. 
\begin{proof}
Assume for the sake of a contradiction that there is a round $r \in (r_1,r_2]$
  such that $leader_{p_i}^{r}\ne p_i$; choose $r$ such that it is the earliest round after
  $r_1$ where this happens.

First, suppose that $p_i$ updated its leader variable in Line~\ref{line:rcle:resetLeader2}.
Lemma~\ref{lem:rcle:leaderNoWaitAndElectTimer} tells us that $p_i$ does not pass the
  if-checks in Lines~\ref{line:rcle:expiredWaitT} or \ref{line:rcle:expiredElectT}, and
  since $leader_{p_i}^{r-1}=i$, node $p_i$ does not execute
  Line~\ref{line:rcle:startInst} in round $r$;
  therefore $p_i$ does not call $\startInstance()$ in round $r$.

Observe that $p_i$ generates a leader message at some round $r'$ where $r-r'<D$,
since $r$ is the earliest round after $r_1$ where $p_i$ is not a leader. 
Then, Corollary~\ref{cor:continousDomination} and \eqref{eq:agreement} provides a contradiction

Now, suppose that $p_i$ executed Line~\ref{line:rcle:setOtherLeader} in $r$ by
  receiving a leader message $m_\ell$ that was generated by itself before entering the
  region for the last time before $r$.
Considering that $p_i$ contains a newer leader message in $toSend_{p_i}^r$, this yields a
  contradiction to the priority relation on leader messages, since $m_\ell <
  toSend_{p_i}^r$ and thus $p_i$ does not pass the if-condition in
  Line~\ref{line:rcle:ifMsgToSend}.
Thus, if $p_i$ executed Line~\ref{line:rcle:setOtherLeader}, it must be that $p_i$ received a leader
  message $m_k=\msg{L,\_,\_,p_k}$ in round $r$ that was generated by some distinct 
  node $p_k$ in round $r_k$ where 
  \begin{equation} \label{eq:attNum2}
  m_k.attNum>attemptNum_{p_i}^{r}\text{.}
  \end{equation}
By the agreement property (Lemma~\ref{lem:rcle:agreement}), we know that $r_k<r_1$
  because $p_k$ only generates leader messages when $leader_{p_k}^{r_k}=p_k$.
Together with the fact that some node broadcasts $m_k$ in all rounds in
$[r_k,r)$, the $D$-connectedness assumption yields upper and lower
  bounds on $r_k$, i.e., $r_k \in (r_1-D,r_1)$.
Note that Lemma~\ref{lem:rcle:beforeLeader}.(b) tells us that $p_i \in
  \Pi_A^{(r_1-2D,r_1]}$.
Again, applying the agreement property shows that $leader_{p_i}^{r_k}\ne p_i$,
  thus the $\electT$ of $p_i$ must have expired during $(r_k,r_1]$, for
  $leader_{p_i}^{r_1}=p_i$ to hold. 
If $p_k$ has previously generated a leader message in $r_k-D$, or if
$r_1-r_k\geq D$, 
a leader message of $p_k$ will be received by $p_i$ before $r_1$, contradicting 
\eqref{eq:attNum2}.
Thus we can assume that $r_1-r_k<D$.
If $p_k$ has $leader_{p_k}^{r_k-1}\neq k$, then the instance message $m_k'$ that is in
$toSend_{p_k}^{r_k-1}$ is broadcast during $[r_k-2D,r_k)$ by $p_k$ and therefore
also received by $p_i$. Since $$m_k'.attNum = m_k.attNum-1$$ and $p_i$ increases
its variable $attemptNum$ by exactly one before generating the leader message in $r_1$,
it follows that $p_i$ must have passed Line~\ref{line:rcle:ifMsgToSend}, again a contradiction.
%But since $r_k+2D>r_1$, we deduce from Lemma~\ref{lem:rcle:electTwaitTexpiring} that the
%  $\electT$ timer could not have expired by round $r_1$, which provides us 
%  with the required contradiction.
\end{proof}

\begin{lemma}[Stability] \label{lem:rcle:stability}
 The algorithm in Figures \ref{alg:noClockleader1} and \ref{alg:noClockleader2} satisfies property \eqref{eq:stability} with
  bound $B_S=2D-1$.
\end{lemma}
\begin{proof}
For the sake of a contradiction, suppose that for rounds $r_1$ and $r_2$, where
$r_1<r_2$, it holds that $$leader_{p_i}^{r_1}=p_j \wedge leader_{p_i}^{r_2}\ne
  p_j\text{,}$$ and assume that $p_i \in \Pi_A^{[r_1,r_2]}$ and $p_j \in
  \Pi_A^{[r_1-B_S,r_2]}$.
    
Let $r \in (r_1,r_2]$ be the earliest round where $p_i$ sets
  $leader_{p_i}^{r}$ such that $leader_{p_i}^r\ne p_j$.
If $j=i$, Lemma~\ref{lem:rcle:stableLeader} tells us that $p_i$ 
  must have left the region during $(r_1,r]$; we can therefore
  restrict ourselves to the case where $j\ne i$.
Note that it is sufficient to consider the case where $p_i$ 
  updates its leader variable in either
  Lines~\ref{line:rcle:setOtherLeader}, \ref{line:rcle:setFalsumLeader} or Line~\ref{line:rcle:resetLeader2},
  since for setting the leader via Line~\ref{line:rcle:setSelfLeader}, 
  $p_i$ needs to execute Line~\ref{line:rcle:resetLeader2} first.

Consider the case where $p_i$ used Line~\ref{line:rcle:resetLeader2}.
%By Lemma~\ref{lem:rcle:leaderNoWaitAndElectTimer} we know that
%  $$\text{$\neg\running(\waitT)_{p_i}^{r-1}$ and
%  $\neg\running(\electT)_{p_i}^{r-1}$}$$
%  hold.
%Therefore, Lemma~\ref{lem:rcle:electTwaitTexpiring} implies that $p_i$ must
%  have called $\startInstance()$ in round $r$.
Let $r_j$ be the latest round before $r_1$ where $p_j$ still claims to be the leader. 
We can assume that either $p_i$ did not receive a leader message from $p_j$ that
was generated during $(r-2D,r]$ or, $p_i$ did receive such a leader message
from $p_j$ but subsequently also received a message $m_k$ from some node
$p_k\neq p_j$ that enabled it to pass Line~\ref{line:rcle:rcvdLeaderMsg}.
In the former case, it follows by Lemma~\ref{lem:rcle:stableLeader} and the fact that
a leader generates new leader messages in intervals of $D$ rounds that there must be
a round after $r_j$ where $p_j$ left the region, yielding a contradiction.
In the case where $p_i$ receives message $m_k$, it follows by the code of the
algorithm that $r$ is not the earliest round after $r_1$ where $p_i$ updates its
leader variable, a contradiction.

Now, consider the case where $p_i$ used Lines~\ref{line:rcle:setOtherLeader} or
\ref{line:rcle:setFalsumLeader}, i.e., $p_i$
received a message $m_k$ in round $r$ generated by some 
node $p_k$ in round $r_k$, where $p_k\ne p_j$ and such that
\begin{equation} \label{eq:attNum3}
m_k.attNum>toSend_{p_i}^{r}.attNum\text{.}
\end{equation}
If $m_k$ was generated before or at round $r-3D$, it follows by
Lemma~\ref{lem:rcle:propagation} that $p_j$ will pass
Line~\ref{line:rcle:ifMsgToSend} by receiving some message $\geq m_k$ 
before generating the last leader message and therefore still being inside the
region; a contradiction to Lemma~\ref{lem:rcle:stableLeader}.
Thus, $m_k$ was generated in round $r_k\in(r-3D,r)$.
Corollary~\ref{cor:continousDomination} tells us that $m_k.type=L$, which by
Lemma~\ref{lem:rcle:agreement} implies that $r_k \in (r-3D,r_1)$.  
If $r_k\geq r_j$, Lemma~\ref{lem:rcle:agreement} implies that $p_j$ must have left
the region and we are done.
Therefore, consider the case where $r_k<r_j$.
If $r_j - r_k>D$, we again have a contradiction to Lemma~\ref{lem:rcle:stableLeader}
due to \eqref{eq:attNum3}; therefore $r_j - r_k<D$. 
For the case where $p_k$ already generated a leader message in $r_k-D$, the
contradiction again follows by \eqref{eq:attNum3}, hence, we can assume that
$\running(\electT)_{p_k}$ holds during $[r_k-2D,r_k)$ and $toSend_{p_k}.type=I$.
If $$toSend.attNum_{p_k}^{r_k-1}>toSend.attNum_{p_j}^{r_k-1}\text{,}$$ we 
have a contradiction since $p_j$ will pass Line~\ref{line:rcle:ifMsgToSend} before
$r_j$; otherwise, it must be that
$$toSend.attNum_{p_k}^{r_k-1}=toSend.attNum_{p_j}^{r_k-1}\text{.}$$
This, however, implies that $toSend.type_{p_j}^{r_k-1}=L$, and, since $p_k$
will receive this leader message before $r_j$, it will not generate a leader
message itself, a contradiction.
\end{proof}

\subsubsection{Termination}

We say that node $p$ \emph{expired} message $m$ at round $r$, if p expired its 
$leaderT$ timer at $r$ and called \startInstance()
while having $m$ in its $toSend$ variable just before the generation of a new
message.  In addition, we say that a message $m$ \emph{caused} the generation
of instance message $m'$ at round $r$, if there exists a node $p$
such that it expired message $m$ at round r and as a consequence $p$ generated
$m'$ in round $r$.

The next lemma is immediate from the code.

\begin{lemma} \label{lem:rcle:initial5D}
A node stays live at least $5D$ rounds in $R$ before starting/expiring any timer other than the $waitT$ timer.  In other words, it requires at least $5D$ rounds to expire the waitT timer.
\end{lemma}

\begin{lemma} \label{lem:rcle:suffMsgAge}
Suppose some node $p$ expired message $m$ at round $r$.  Then the following holds:
\begin{compactenum}
\item[(a)] If $m.type = L$ (i.e.\ $m$ is a leader message), $m$ must have been generated before or at $r-2D$.
\item[(b)] If $m.type = I$ (i.e.\ $m$ is an instance message), $m$ must have been generated before or at $r-3D$.
\end{compactenum}
\end{lemma}
\begin{proof}
\emph{(a)} Suppose, in contradiction, that leader message $m$ was generated during $(r-2D,r]$.  If $m$
was generated by $p$, then Line~\ref{line:rcle:startInst} will simply not be executed since Line~\ref{line:rcle:selfLeader} will become true.  If $m$ was not generated by $p$, then, by Line~\ref{line:rcle:startLeaderTOther}, $p$ must not have expired its $leaderT$ timer by $r$ since $leaderT$ is set to expire exactly $2D$ rounds after the generation of the leader message.\\
\emph{(b)} Suppose, in contradiction, that instance message $m$ was generated during $(r-3D,r]$.  Let $r' \in (r-3D,r]$ be the earliest round where $toSend^{[r',r)}_{p} = m$.  We divide into two cases:\\
(\emph{Case 1}) Instance message $m$ was generated by $p$:  In this case, $p \in \Pi^{[r',r]}_{A}$ and $p$ must not be running its $waitT$ timer during $[r',r]$ because otherwise $p$ must have reentered region $R$ and Lemma \ref{lem:rcle:initial5D} prevents $p$ from expiring $m$ at $r$.  If $p$ generated $m$ at $r'' \in (r-3D,r')$, then Lemma \ref{lem:rcle:toSendMonotonic} implies that $toSend^{[r'',r)}_{p} = m$ which contradicts the fact that $r'$ is the earliest round where $toSend^{[r',r)}_{p} = m$.  So, $r'$ is the round when $p$ generated $m$.  We further divide into two cases:\\
(\emph{Case 1a}) $r' \leq r-2D$: By the code, Line~\ref{line:rcle:startTimerElectT} is executed when $m$ is generated.  Also, Lemma \ref{lem:rcle:toSendMonotonic} tells us that Line~\ref{line:rcle:ifMsgToSend} does not become true until round $r$.  So, by the code, $electT$ timer will expire with Line~\ref{line:rcle:selfCandidate} being true causing the generation of a leader message $m'$ by round $r$ where $m' > m$.  Hence, $toSend^{r}_{p} \neq m$.\\
(\emph{Case 1b}) $r' > r-2D$: Same as in (\emph{Case 1a}), Line~\ref{line:rcle:startTimerElectT} is executed when $m$ is generated and Line~\ref{line:rcle:ifMsgToSend} will not become true until round $r$.  Hence, by the code, $electT$ timer will still be running at round $r$ at $p$ since $electT$ timer is set to expire $2D$ rounds after the generation of message $m$.\\
(\emph{Case 2}) Instance message $m$ was not generated by $p$: We further divide into two cases:\\
(\emph{Case 2a}) Node $p$ is running its $waitT$ timer at round $r'$: Since $p$ expires $m$ at round $r$, there exists a round $r'' \in (r',r]$ where $p$ stops running its $waitT$ timer. By the code, $p$ executes Line~\ref{line:rcle:startElectTWaitInst} at $r''$.  Let $r_1 \in (r-3D,r]$ be the round when $m$ was generated.  The execution of Line~\ref{line:rcle:startElectTWaitInst} sets $p$'s $electT$ timer to expire at round $r''+2D$ and after the $electT$ timer expires, by Line~\ref{line:rcle:startLeaderTInstOther}, an additional $D$ rounds is needed to expire the $leaderT$ timer.  Hence, $p$ does not expire $m$ at round $r$.\\ 
(\emph{Case 2b}) Node $p$ is not running its $waitT$ timer at round $r'$: The proof is similar to (\emph{Case 2a}) except that Line~\ref{line:rcle:syncElectT} is executed instead of Line~\ref{line:rcle:startElectTWaitInst}.
\end{proof}

\begin{lemma} \label{lem:rcle:termInvariant}
Suppose instance message $m$ was generated by $p$ at round $r$.  Let $m'$ be the message that caused the generation of $m$ at $p$ at round $r$ ($m' < m$).  Then, for all $r_q \in [r-D,r+D]$, any node $q \in \Pi^{[r_q-D,r_q]}_A$ has in $toSend^{r_q}_{q}$ either $m'$ or an instance message generated by expiring $m'$.  
\end{lemma}
\begin{proof}
Suppose not.  We divide into two cases:\\
(\emph{Case 1}) For some $r_q \in [r-D,r]$, some node $q \in \Pi^{[r_q-D,r_q]}_A$ has a message $m_1$ in $toSend^{r_q}_{q}$ where $m_1 \neq m'$ and $m_1$ was not generated by expiring $m'$: By Lemma \ref{lem:rcle:suffMsgAge}, $m'$ must have been generated before or at $r-2D$ and by Assumption \ref{assume:rcle:existd} and Lemma \ref{lem:rcle:propagation}, $m'$ is the highest priority instance message in $R$ until round $r-D$.  Message $m_1$ must have been generated during $(r-D,r]$ because otherwise, by Assumption \ref{assume:rcle:existd}, Lemma \ref{lem:rcle:initial5D}, and Lemma \ref{lem:rcle:propagation}, $p$ receives $m_1$ or some message that has higher priority than $m_1$ by round $r$ if $m_1 > m'$ and $q$ receives $m'$ or some message that has higher priority than $m'$ by round $r-D$ otherwise.  A contradiction.

Now, suppose $m_1$ is a leader message.  Let $p_1$ be the node that generated
$m_1$.  Then, $p_1$ must have generated an instance message $m''$ at round $r_1
\in (r-3D,r-2D]$ since it requires exactly $2D$ rounds for leader message $m_1$
to be generated after the generation of $m''$.  By Assumption
\ref{assume:rcle:existd}, Lemma \ref{lem:rcle:initial5D}, and Lemma \ref{lem:rcle:propagation},
$p$ receives $m''$ or some message $> m''$ by round
$r$ if $m'' > m$, and $p_1$ receives $m'$ or some message that has higher
priority than $m'$ by $r-D$ otherwise.  A contradiction.

From the above, we can restrict $m_1$ to be an instance message generated during
$(r-D,r]$.  Then, there exists a message $m_2$ that caused the generation of
$m_1$ at some node $q'$ at round $r'\in (r-D,r]$. Message $m_2$ must be $m_2 <
m'$ because otherwise, by Assumption \ref{assume:rcle:existd}, Lemma
\ref{lem:rcle:initial5D}, and Lemma \ref{lem:rcle:propagation}, $q$ receives $m_2$ or some
message that has higher priority than $m_2$ by round $r$ which yields a
contradiction.

Now, by Lemma \ref{lem:rcle:suffMsgAge}, $m_2$ must be generated before or at round $r-2D$.  But, by round $r'$, node $q'$ must receive $m'$ or some message that has higher priority than $m'$ (again by Assumption \ref{assume:rcle:existd}, Lemma \ref{lem:rcle:initial5D}, and Lemma \ref{lem:rcle:propagation}), Hence, $m_1$ does not exist, a contradiction.\\
(\emph{Case 2}) For some $r_q \in (r,r+D]$, some node $q \in \Pi^{[r_q-D,r_q]}_A$ has a message $m_1$ in $toSend^{r_q}_{q}$ where $m_1 \neq m'$ and $m_1$ was not generated by expiring $m'$:  By (\emph{Case 1}), $m_1$ must have been generated during $(r,r+D]$.  The rest of the proof is similar to (\emph{Case 1}).
\end{proof}

\begin{lemma} \label{lem:rcle:termKeyInvariant}
Suppose instance message $m$ was generated by $p$ at round $r$.  Let $m'$ be the message that caused the generation of $m$ at $p$ at round $r$ ($m' < m$).  Then, for all $r_q \in [r-D,r+D]$, any node $q$ that is live, in $R$, and not running its $waitT$ timer at $r_q$  has in $toSend^{r_q}_{q}$ either $m'$ or an instance message generated by expiring $m'$.
\end{lemma}
\begin{proof}
The proof is direct from Lemma \ref{lem:rcle:initial5D} and Lemma \ref{lem:rcle:termInvariant}.
\end{proof}

\begin{lemma} \label{lem:rcle:withinD}
For any two instance messages $m_1$ and $m_2$ that were generated by $p_1$ and $p_2$ by expiring the same message $m$ at rounds $r_1$ and $r_2$, respectively, $|r_1 - r_2| < D$ holds.
\end{lemma}
\begin{proof}
First note that both $m_1$ and $m_2$ have higher priority than $m$, and
$m_1.attNum = m_2.attNum$.  Without loss of generality, suppose $m_1$ has higher
priority than $m_2$ ($p_1$ entered $R$ ealier than $p_2$ or $p_1$ and $p_2$
entered $R$ at the same round) and $(r_2 - r_1) \geq D$. By Assumption
\ref{assume:rcle:existd}, Lemma \ref{lem:rcle:initial5D}, and Lemma
\ref{lem:rcle:propagation}, $p_2$ receives $m_1$ or some message that has higher
priority than $m_1$ by round $r_2$.  Hence, by Lemma \ref{lem:rcle:toSendMonotonic},
$p_2$ will not expire $m$, a contradiction.
\end{proof}

\begin{lemma} \label{lem:rcle:termSync}
Suppose message $m'$ caused the generation of instance message $m$ ($m > m'$) at
node $p$ at round $r$.  Let $m_1$ be the highest priority instance message that
was generated by any node by expiring $m'$ and let $p_1$ be the node that generated
$m_1$.  Also, let $r_1$ be the round when $m_1$ was generated.  Then, the
following holds:
\begin{compactenum}
\item[(a)] If $p_1 \in \Pi^{r_1+2D}_{E}$ and $p_1$ is not running its $waitT$
  timer at $r_1+2D$, then $p_1$ elects itself as the leader at round $r_1+2D$. 
\item[(b)] For each node $q$($\neq p_1$) that is not running its $waitT$ timer
  at $r_1+3D$ and $q \in \Pi^{r_1+3D}_{E}$, it holds for all $r' \in [r_1+2D,r_1+3D]$
  that $toSend^{r'}_{q} = m_1$, if $p_1$ did not elect itself as the
  leader. 
\item[(c)] For any node $q$($\neq p_1$) that is not running its $waitT$ timer at
  $r_1+2D$ and $q \in \Pi^{r_1+2D}_{E}$, it holds that $q$ expires its
  $electT$ timer at round $r_1+2D$ and sets its $leaderT$ timer to expire at $r_1+3D$. 
\end{compactenum}
\end{lemma}
\begin{proof}
\emph{(a)} Suppose, in contradiction, that $p_1$ did not elect itself as the
leader at round $r_1+2D$.  This means that $p_1$ received a message $m_2$ during
$[r_1,r_1+2D]$ where $m_2 > m_1$.  By Lemma \ref{lem:rcle:termKeyInvariant} and the
fact that $m_1$ was the highest priority instance message that was ever
generated by expiring $m'$, $m_2$ must have been generated during $(r_1+D,
r_1+2D)$ by expiring a message $m''$ that was in turn generated by expiring
$m'$.  By Lemma \ref{lem:rcle:withinD}, the earliest round that $m''$ can be
generated is $r_1-D$.  Hence, Lemma \ref{lem:rcle:suffMsgAge} implies that $m''$
cannot become $\geq 3D$ rounds old (i.e., cannot expire) until round $r_1+2D$. A
contradiction.\\
\emph{(b)} Suppose, in contradiction that for some $r_2 \in [r_1+2D, r_1+3D]$,
$toSend^{r_2}_{q} = m_2 \neq m_1$.  Let $r_2$ be the round when $m_2$ was
generated by some node $p_2$.  By Lemma \ref{lem:rcle:termKeyInvariant} and the fact
that $m_1$ was the highest priority instance message that was ever generated by
expiring $m'$, $m_2$ must have been generated at $r'' \in (r_1+D, r_1+3D]$.  We
divide into two cases: \\
(\emph{Case 1}) $m_2$ is a leader message: Then, $p_2$ must have generated an instance message $m_2'$ at round
$r''-2D \in (r_1-D,r_1+D]$ and $toSend^{r''}_{p_2} = m_2'$ holds before $p_2$ called
$\startInstance()$.  By Lemma \ref{lem:rcle:termKeyInvariant}, $m_2'$ must
be the same as either $m'$ or some message generated by expiring $m'$.  By
Assumption \ref{assume:rcle:existd}, Lemma \ref{lem:rcle:initial5D}, and Lemma
\ref{lem:rcle:propagation}, $p_2$ receives $m_1$ or some message that has higher
priority than $m_1$ by round $r''-D$($<r_1+2D$), since $m_1$ is the highest
priority instance message generated by a node by expiring $m'$.  Hence, by Lemma
\ref{lem:rcle:toSendMonotonic}, $toSend^{r''}_{p_2} > m_2'$, a contradiction.\\
(\emph{Case 2}) $m_2$ is an instance message:  Then, there exists a message $m_2'$ that expired at $p_2$ at
$r''$.  By Lemma \ref{lem:rcle:suffMsgAge}, $m_2'$ must have been generated before or
at $r''-2D$($<r_1+D$). By Lemma \ref{lem:rcle:termKeyInvariant} and the fact that
$m_1$ was the highest priority instance message that was ever generated by
expiring $m'$, we have $m_2' < m_1$.  Hence, by Assumption \ref{assume:rcle:existd},
Lemma \ref{lem:rcle:initial5D}, and Lemma \ref{lem:rcle:propagation}, $p_2$ receives
$m_1$ or some message that has higher priority than $m_1$ by round $r''$
preventing $m_2'$ to expire at $p_2$ at round $r''$ (by Lemma
\ref{lem:rcle:toSendMonotonic}). A contradiction.\\
\emph{(c)} Suppose $q$ does not expire its $electT$ timer at $r_1+2D$.  This
means that $toSend^{r_1+2D}_{q}$ does not contain $m_1$ because otherwise
Line~\ref{line:rcle:syncElectT} enforces $q$ to set its $electT$ timer to expire at
round $r_1+2D$.  Assumption \ref{assume:rcle:existd} and Lemma
\ref{lem:rcle:termKeyInvariant} implies that, by round $r_1+D$, $q$ receives $m_1$
and $toSend^{r_1+D}_{q}=m_1$.  So, in order for $q$ to not expire its $electT$
timer at $r_1+2D$, $q$ must receive some message $m_2 > m_1$ during
$(r_1+D,r_1+2D]$.  The rest of the proof is similar to (\emph{Case 1}) and
(\emph{Case 2}) of \emph{(b)}.
\end{proof}

\begin{lemma} \label{lem:rcle:waitingCrashOrLeave}
Suppose node $q$ entered $R$ at round $r$.  Consider the three rounds $r+5iD$,
$r+5(i+1)D$, and $r+5(i+2)D$, for $i \geq 2$, and assume that $waitT$ is running for all $r'
\in [r+5iD, r+5(i+2)D)$. If $q$ decides not to stop running $waitT$ at round
$r+5(i+2)D$, then at least one node that was live, inside $R$, and not running its
$waitT$ timer crashed or left region $R$ during $[r+5(i-1)D-D, r+5(i+2)D]$.
\end{lemma}
\begin{proof}
For some $k (\geq 2)$, let $m_1$, $m_2$, and $m_3$ be the message contained in
$toSend^{r+5kD}_{q}$, $toSend^{r+5(k+1)D}_{q}$, and variable $toSend^{r+5(k+2)D}_{q}$,
respectively.  Suppose that all nodes that are still live, in $R$, and not running their
$waitT$ timer do not crash or leave region $R$ during $[r+5(k-1)D-D,
r+5(k+2)D]$.  We divide into five cases:\\
(\emph{Case 1}) $m_1$ is a leader message and $m_2$ is an instance message: In
this case, $m_1$ must have been generated during $(r+5(k-1)D-D,r+5kD]$ because
otherwise, by Assumption \ref{assume:rcle:existd}, $q$ receives $m_1$ by round
$r+5(k-1)D$ and as a consequence $\differ(prevToSend,toSend)$ will return false
causing $q$ to stop running its $waitT$ timer at round $r+5kD$.  This means that
there exists a node $q'$ that elected itself as the leader during
$(r+5(k-1)D-D,r+5kD]$.  Applying (stability)  and Corollary
\ref{cor:continousDomination} on $q$ tells us that $q$ crashed or left the
region during $(r+5(k-1)D-D,r+5(k+1)D]$. A contradiction.\\
(\emph{Case 2}) $m_1$ is a leader message and $m_2$ is a leader message ($m_1
\neq m_2$): The proof of this case is similar to (\emph{Case 1}).\\
(\emph{Case 3}) $m_1$ is an instance message and $m_2$ is an instance message:
Similar to (\emph{Case 1}), $m_1$ must have been generated during
$(r+5(k-1)D-D,r+5kD]$.  This means that there exists a message $m'$ that caused
the generation of $m_1$ at $r' \in (r+5(k-1)D-D,r+5kD]$.  By Lemma
\ref{lem:rcle:termSync}.(a), the node, say $q''$, that generated the highest priority
instance message $m''$ by expiring $m'$ elects itself as the leader and by Lemma
\ref{lem:rcle:withinD}, the round that $q''$ elects itself as the leader cannot be
later than $r+5kD+3D$ ($D$ rounds for the difference between the generation
round of $m_1$ and $m''$, and $2D$ rounds for $m''$ electing itself as the
leader). Again, applying (stability)  and Corollary
\ref{cor:continousDomination} tells us that $q$ must have crashed or left the
region during $(r+5(k-1)D-D,r+5(k+1)D]$, A contradiction.\\
(\emph{Case 4}) $m_1$ is an instance message, $m_2$ is a leader message, and
$m_3$ is a leader message: Simply applying (\emph{Case 2}) on $m_2$ and $m_3$
gives us a contradiction.\\
(\emph{Case 5}) $m_1$ is an instance message, $m_2$ is a leader message, and
$m_3$ is an instance message: Applying (\emph{Case 1}) on $m_2$ and $m_3$
provides us with a contradiction.
\end{proof}

\begin{lemma} \label{lem:rcle:generateEvery4D}
Suppose that node $p$ stops running its $waitT$ timer at round $r$.  If $p \in
\Pi^{[r,r+4D]}_{A}$, $p$ is not running its $waitT$ timer during $[r,r+4D]$, and
$p$ does not elect a leader other than itself during $[r,r+4D]$, then there
exists a round $r_p \in [r,r+4D]$ such that $p$ generates an instance message.
%and for every $q \in \Pi^{r_p}_{E}$ where $\neg\running(waitT)_{q}^{r_p}$ is true,
%it holds that $q$ generates an instance message at $r_p$.
\end{lemma}
\begin{proof}
We distinguish the following four cases:\\ 
(\emph{Case 1}) An expired ($2D$
rounds old or older) leader message was in $toSend^{r}_{p}$: In this case,
Line~\ref{line:rcle:selfReceiveLeader} to Line~\ref{line:rcle:startLeaderTWaitLeader} will
be executed and in turn Line~\ref{line:rcle:expiredLeaderT} will evaluate to true at
round $r$.  Since Line~\ref{line:rcle:selfReceiveLeader} prevents $p$ from electing
itself as the leader, $\startInstance()$ will be called at
Line~\ref{line:rcle:startInst}.  Hence, $p$ generates an instance message by
executing Line~\ref{line:rcle:genInstMsg} at round $r$.\\
(\emph{Case 2}) An expired ($3D$ rounds old or older) instance message was in
$toSend^{r}_{p}$: In this case, Line~\ref{line:rcle:startElectTWaitInst} will be
executed and in turn Line~\ref{line:rcle:expiredElectT} evaluates to true.  Also,
Line~\ref{line:rcle:selfCandidate} evaluates to false since initially $candidate =
\falsum$.  So, Line~\ref{line:rcle:startLeaderTInstOther} will be executed and in
turn Line~\ref{line:rcle:expiredLeaderT} will evaluate to true at round $r$.  Now,
since initially $leader = \falsum$, Line~\ref{line:rcle:selfLeader} will evaluate to
false causing Line~\ref{line:rcle:startInst} to be executed. Hence, $p$ generates an
instance message by executing Line~\ref{line:rcle:genInstMsg} at round $r$. \\
(\emph{Case 3}) A non-expired (less than $2D$ rounds old) leader message was in
$toSend^{r}_{p}$: Let $m$ be the leader message in $toSend^{r}_{p}$.  If $m$ was
not generated by $p$, then Line~\ref{line:rcle:setOtherLeader2} is executed at round
$r$ which contradicts the assumption that $p$ does not elect a leader other than
itself during $[r,r+4D]$.  If $m$ was generated by $p$, then Lemma
\ref{lem:rcle:initial5D} implies that $m$ was generated before round $r-5D$ which
contradicts the assumption that $m$ is less than $2D$ rounds old.\\
(\emph{Case 4}) A non-expired (less than $3D$ rounds old) instance message was
in $toSend^{r}_{p}$: Let $m$ be the instance message in $toSend^{r}_{p}$ and let
$m'$ be the message that caused the generation $m$.  Also, let $r' \in (r-3D,r]$
be the round when $m$ was generated (since $m$ did not expire at round $r$, $m$
must have been generated during $(r-3D,r]$).  By Lemma \ref{lem:rcle:withinD}, the
highest priority instance message, say $m_1$, that was ever generated by
expiring $m'$ is generated at $r_1 \in (r'-D, r'+D)$. Also, by Lemma
\ref{lem:rcle:termSync}.(a) and Lemma \ref{lem:rcle:termSync}.(b), for each node $q \in
\Pi^{r_1+3D}_{E}$, $toSend^{r_1+3D}_{q} = m_1$ and the $leaderT$ timer expires
at $r_1+3D$.  Hence, $\startInstance()$ is executed (Line~\ref{line:rcle:startInst})
at $r_1+3D \in (r-D, r+4D)$.  If $r_1+3D \in (r,r+4D)$, then we are done.  If
$r_1+3D \in (r-D,r]$, then, by Assumption \ref{assume:rcle:existd} and Lemma \ref{lem:rcle:propagation}, $p$ also must have received $m_1$ or some message that has higher priority than $m_1$ by $r_1+3D$.  Variable $toSend^{r}_{p}$ cannot have $m$ in it because it will contradict Lemma \ref{lem:rcle:toSendMonotonic} since $m < m_1$.
\end{proof}

\begin{lemma} \label{lem:rcle:generateEvery4D2}
Suppose that node $p$ generates an instance message $m$ at round $r$.  If $p \in
\Pi^{[r,r+4D]}_{A}$, $p$ is not running its $waitT$ timer during $[r,r+4D]$, and
$p$ does not elect a leader other than itself during $[r,r+4D]$, then there
exists a round $r_p \in (r,r+4D]$ such that $p$ generates an instance message.
%and for all $q \in \Pi^{r_p}_{E}$ where $\neg\running(waitT)_{q}^{r_p}$ is true,
%it holds that $q$ generates an instance message at $r_p$.
\end{lemma}
\begin{proof}
The proof is similar to (\emph{Case 4}) of Lemma \ref{lem:rcle:generateEvery4D}.
\end{proof}

\begin{lemma} \label{lem:rcle:blockWaitingNodes}
Suppose node $q$ enters $R$ at round $r$ and there exists a node $p$ that is
live, in $R$, and not running its $waitT$ timer at round $r$.  Then, $q$ does
not stop running its $waitT$ timer unless $p$ elects a leader, crashes, or
leaves region $R$.
\end{lemma}
\begin{proof}
By Lemma \ref{lem:rcle:generateEvery4D} and Lemma \ref{lem:rcle:generateEvery4D2}, we know
that $p$ generates an instance message at least every $4D$ rounds as long as $p$
does not crash, leave the region, or elect a leader.   So, by Assumption
\ref{assume:rcle:existd} and Lemma \ref{lem:rcle:propagation}, $q$ receives the instance message generated by $p$ or some
message that has higher priority than it at least every $5D$ rounds.  Along with
Lemma \ref{lem:rcle:termSync}, the above implies that $q$ receives a new message
every $5D$ rounds from a node that entered earlier than itself.  Hence,
Line~\ref{line:rcle:earliestCheck} will evaluate to true which causes $q$ to start
its $waitT$ timer again.
\end{proof}

\begin{lemma}[Termination] \label{lem:rcle:termination}
The algorithm in Figures \ref{alg:noClockleader1} and \ref{alg:noClockleader2} satisfies (termination) with bound $B_T =
22D+14(n-1)D$ where $n$ is the total number of nodes in the system.
\end{lemma}
\begin{proof}
Suppose that node $p$ entered $R$ at round $r_e$.  For the sake of a contradiction, we
assume that $p \in \Pi^{r_e}_{E}$, $p \in \Pi^{(r_e, r_e+22D+14(n-1)D]}_{A}$,
and for all $r \in [r_e, r_e+22D+14(n-1)D]$, $leader^{r}_{p}=\falsum$.  The worst case
bound on $B_T$ can be obtained if the adversary causes $p$ to run its $waitT$ timer as long as
possible and, after $p$ stops running its $waitT$ timer, the adversary forces $p$ to delay its
decision as long as possible.  By Lemma \ref{lem:rcle:waitingCrashOrLeave}, we know
that, after round $r_e+10D$, at least one node that was not running its $waitT$
timer crashes or leaves region $R$ in every $10D$ rounds if $p$ manages to run
its $waitT$ timer continuously during those $10D$ rounds.  However, this can
happen only  at most $n-1$ times because there can be at most $n-1$ nodes not
running its $waitT$ timer.  Also, Lemma \ref{lem:rcle:waitingCrashOrLeave} implies
that even in the case where a node $q$ that has left the region (resp.\ crashed)
reenters (resp.\ recovers from its crash inside $R$) it will always hold that  
$enteredSince_q<enteredSince_p$ upon reentering (resp.
recovering).  Therefore,  all newly generated messages $m$ will have $m.entSince <
enteredSince_p$ from round $r_e+10D+10(n-1)D$ on.  Hence, Line
\ref{line:rcle:earliestCheck} evaluates to false at round $r_e+10D+10(n-1)D+5D$
causing timer $waitT$ to stop running.  

Now, we consider the worst case for delaying $p$'s decision after $p$ stops
running its $waitT$ timer; let $r_w$ be the respective earliest round when
$\neg\running(waitT)_p^{r_w}$ holds.  Note that $r_w$ can be at most
$r_e+15D+10(n-1)D$.  Let $r_f$ be the first round after $r_w+D$ when $p$
generates an instance message.  By assumption, we know that $p$ did not elect a leader
during $[r_w,r_f+4D]$.  Therefore,
Lemma \ref{lem:rcle:generateEvery4D} and Lemma \ref{lem:rcle:generateEvery4D2} imply
that $r_f \in (r_w+D, r_w+5D]$, since $p$ generates an instance message every
$4D$ rounds if it did not elect a leader.  Let $m_f$ be such an instance message
generated by $p$ at round $r_f$. We know that there exists a message
$m'$ that caused the generation of $m_f$.  Let $m_f'$ be the
highest priority instance message that was ever generated by expiring $m'$ and
let $p_f'$ be the node that generated $m_f'$.  Lemma \ref{lem:rcle:termSync}.(a)
tells us that if $p_f'$ does not crash or leaves region $R$, then $p_f'$ elects
itself as the leader by round $r_f +3D$ (by Lemma \ref{lem:rcle:withinD}, $m_f'$ can
be generated as late as $r_f+D$ and it takes $2D$ rounds to elect itself as the
leader).  To delay $p$'s decision as long as possible, we consider the case of
node $p_f'$ crashing or leaving region $R$ after generating $m_f'$ but before
electing itself as the leader.  Note that even if $p_f'$ reenters $R$ (resp.
recovers in $R$) after leaving $R$ (resp.  crashing), the round that $p_f'$ reenters $R$ (resp. recovers in $R$)
cannot be less than $r_w$ since, by Lemma \ref{lem:rcle:withinD}, $m_f$ can only be
generated as early as $r_f-D > r_w$.  So, as long as $p$ is live, in $R$, and
not running its $waitT$ timer, Lemma \ref{lem:rcle:blockWaitingNodes} prevents $p_f'$
from stopping its $waitT$ timer after its reentry (resp. recovery).  Now, since
$p_f'$ did not elect itself as the leader, we know by Lemma
\ref{lem:rcle:generateEvery4D2} that $p$ will generate a new instance message by
round $r_f+4D$.  The above can happen at most $n-1$ times since there can be at
most $n-1$ nodes that are not running their $waitT$ timer along with $p$.  So,
after round $r_f+4(n-1)D$, $p$ will be the only node that is live, in $R$, and
not running its $waitT$ timer and $p$ will elect itself as the leader by round
$r_f+4(n-1)D+2D$ (since $p$ is the only node left, it will be the only node
generating an instance message).  Hence, in the worst case, $p$ elects a leader by
round $r_w+7D+4(n-1)D$ since $r_f$ is at most $r_w+5D$.

For node $p$, the overall worst case would be taking $15D+10(n-1)D$ rounds for
stopping its $waitT$ timer and taking $7D+4(n-1)D$ for electing a leader after
stopping its $waitT$ timer.  Summing up shows that in the worst case, by round
$r_e+15D+10(n-1)D+7D+4(n-1)D = r_e+22D+14(n-1)D$, node $p$ elects a leader, a
contradiction. 
\end{proof}

We obtain the following theorem directly from Lemmas \ref{lem:rcle:validity}, \ref{lem:rcle:agreement}, \ref{lem:rcle:stability}, and \ref{lem:rcle:termination}:

\begin{theorem} \label{thm:rcle:main}
  The algorithm in Figures \ref{alg:noClockleader1} and \ref{alg:noClockleader2} solves the RCLE problem with bounds 
  $B_V=B_S=2D-1$ and $B_T=22D+14D(n-1)=\mathcal{O}(nD)$.
\end{theorem}

\section{A Condition on Mobility} \label{sec:rcle:mobility}

In this section, we provide a condition on mobility that implies Assumption
\ref{assume:rcle:existd} with a bounded communication diameter $D$.  Our mobility
condition generalizes the mobility condition of \cite{CRW:10} in a way such 
that it no longer depends on a specific coordinate system.
We assume region $R$ to be a 2-dimensional convex polygon.  In
addition, we assume that nodes move at a speed bounded by some constant $\sigma$.  

We first define some basic properties for our mobility condition.  Let $\delta$
be a fixed constant such that $0 < \delta \leq C -
  \Delta\sigma$.\footnote{Recall from Section~\ref{sec:rcle:sysmodel} that $C$
  refers to the communication radius and $\Delta$ denotes the round duration.  We allow a range of values for $\delta$ to accommodate a range of mobility patterns.}  Given two
positions $\phi_1$ and $\phi_2$, let $dist(\phi_1, \phi_2)$ be the Euclidean
distance between $\phi_1$ and $\phi_2$.

\begin{definition} \label{def:rcle:proper}
Let $p_0, p_1, \dots, p_{n-1}$ be a sequence of nodes such that $p_i$ is at
position $\phi_i$ at the beginning of round $r+i$, $0 \leq i \leq n-1$,
and let $\phi_n$ be any position in $R$.  The sequence of positions $\phi_0,
\phi_1, \dots, \phi_{n}$ is called a \emph{proper propagation sequence from
$p_0$ to $\phi_n$ starting at round $r$}, denoted as $P^{r}_{\phi_0
\rightarrow \phi_n}$, if it holds that
\begin{compactitem}
\item[(a)] $\phi_0$ and $\phi_n$ are both in $R$,
\item[(b)] $p_i$ broadcasts in round $r+i$,
\item[(c)] $p_i$ and $p_{i+1}$ are live and connected in round $r+i$, $0 \leq i \leq n-2$, and throughout round $r+n-1$, $p_{n-1}$ is live and within distance $C$ of $\phi_n$,
\item[(d)] $\delta \leq dist(\phi_i,\phi_{i+1})$, and
\item[(e)] for $0 \leq i \leq n-2$, at the beginning of round $r+i+1$, $\phi_{i+1}$ lies within $R$ and within a circle that is uniquely defined by positions $\phi_i$ and $\phi_n$, which serve as the two endpoints of the axis of the circle.
\end{compactitem}
\end{definition}

\begin{figure}[t]
\centering
\includegraphics[scale=0.7]{figures/infoprop.pdf}
\caption{Worst case information propagation. Points $S$ and $F$ corresponds to
$\phi_i$ and $\phi_n$, respectively. The shaded region of the circle that is uniquely
defined by $S$ and $F$, corresponds to the geographic region in which $\phi_{i+1}$ must lie.
Points $A$ and $B$ represent the worst case for information propagation.}
\label{fig:rcle:infoprop}
\end{figure}

Similar to the properties of the well-directed propagation sequence defined in
\cite{CRW:10}, property (d) of Definition \ref{def:rcle:proper} says that
information gets closer to its destination in each
round and property (e) of Definition \ref{def:rcle:proper} says that as information
propagates to its destination, it should reside within a certain geographic
sector (see Figure \ref{fig:rcle:infoprop}).   Also, note that Definition
\ref{def:rcle:proper} corresponds to a JIT path if a real node resides at position
$\phi_n$.   However, notice that Definition \ref{def:rcle:proper} is independent
of any specific coordinate system.

The following assumption states our mobility condition:

\begin{assumption}[Mobility Condition] \label{assume:rcle:mobility}
For every node $p_i$ that is live throughout round $r$ and broadcasts a
message at the beginning of round $r$ at position $\phi_i$ in $R$, and
for all positions $\phi_j$ in $R$, there exists a proper propagation sequence
$P^{r}_{\phi_i \rightarrow \phi_j}$ starting at round $r$.
\end{assumption}

Given the above mobility condition, it is possible to obtain the bounded communication diameter $D$ of region $R$:

\begin{theorem} \label{thm:rcle:mobility}
Suppose that nodes follow the mobility condition given by Assumption
\ref{assume:rcle:mobility}.  Then, property D-connectedness is ensured with $D=\lceil
\frac{L^2 - (C-\Delta\sigma)^2}{\delta^2} \rceil$ where $L$ is the maximum
Euclidean distance between any two points in $R$.
\end{theorem}
\begin{proof}
The proof is given with the assistance of Figure \ref{fig:rcle:infoprop}.  Consider
some node $p_i$ that
participates in $P^{r}_{\phi_i \rightarrow \phi_n}$, where $0 \leq i \leq n-1$, and suppose that at the
beginning of round $r+i$, node $p_i$ broadcasts information $I$ at
position $S$ (=$\phi_i$) which needs to be propagated to position $F$
(=$\phi_n$) as depicted in Figure \ref{fig:rcle:infoprop}.  By properties (d) and
(e) of Definition \ref{def:rcle:proper}, $p_{i+1}$, which obtained information $I$
from $p_i$, has to be in the shaded region of Figure \ref{fig:rcle:infoprop} at the
beginning of round $r+i+1$.  Within the shaded region of Figure
\ref{fig:rcle:infoprop}, the position farthest away from $F$ is either $A$ or $B$.
This means that, in worst case, $\phi_{i+1}$ (the position of $p_{i+1}$ at the
beginning of round $r+i+1$) can be either $A$ or $B$.  Without loss of
generality, suppose $\phi_{i+1} = A$.  Let $h_i$ be the Euclidean distance
between $\phi_i$ and $\phi_n$. Since angle $\angle SAF$ is
a right angle by construction, we obtain the recursive formula
\begin{align} \label{eq:dist}
h_{i+1}^2 &= h_i^2 - \delta^2\text{.} \\
\intertext{Since $L$ is the maximum Euclidean distance between any two points in $R$, we
have $h_0 = L$ in the worst case.  From this, we can obtain the following closed-form
solution to \eqref{eq:dist}:} 
h_{i+1} &= \sqrt{L^2 - i\delta^2} \nonumber 
\end{align}
Now, suppose that $h_{k+1} \leq
C-\Delta\sigma$.  In this case, $p_{k+1}$ will be within $C$ of $\phi_n$
throughout round $r+k+1$ since the maximum distance that a node can
move is bounded by $\Delta\sigma$.  Applying this to the above closed-form
solution yields
\begin{align} 
h_{k+1} = \sqrt{L^2 - k\delta^2} &\leq C-\Delta\sigma \nonumber \\ 
\intertext{and therefore}
\dfrac{L^2 - (C-\Delta\sigma)^2}{\delta^2} &\leq k\text{.} \nonumber 
\end{align} 
Since $k$
is the worst case number of hops for an information $I$ to reach
its destination, we can conclude that the bounded communication diameter is  
$D=\left\lceil \frac{L^2 - (C-\Delta\sigma)^2}{\delta^2} \right\rceil$.
\end{proof}


%\begin{theorem} \label{thm:rcle:main}
%  Algorithm~\ref{alg:noClockleader} solves the RCLE problem with bounds 
%  $B_V=B_S=2D-1$ and $B_T=22D+14D(n-1)=\mathcal{O}(nD)$.
%\end{theorem}

%Text goes here.

%\section{New Section}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\begin{figure}[H]
%\centering
%\includegraphics[scale=.50]{figures/Penguins.jpg}
%\caption{TAMU figure - This is an example of a long figure title.  Figure titles need to be single-spaced within and double spaced between in the list of figures.}
%\label{fig:rcle:landscapepenguins}
%\end{figure}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\subsection{Subsection}
%\begin{table}[H]
%\centering
%\caption{This is a table template - This is an example of a long table title.  Table titles need to be single-spaced within and double spaced between in the list of tables.}
%\begin{tabular}{|l|c|c|c|c|c|}
%\hline
%Product & 1 & 2 & 3 & 4 & 5\\
%\hline
%Price & 124.- & 136.- & 85.- & 156.- & 23.-\\
%Guarantee [years] & 1 & 2 & - & 3 & 1\\
%Rating & 89\% & 84\% & 51\% & & 45\%\\
%\hline
%\hline
%Recommended & yes & yes & no & no & no\\
%\hline
%\end{tabular}
%\label{tab:template1}
%\end{table}


%\subsection{Subsection}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\begin{figure}[H]
%\centering
%\includegraphics[scale=.50]{figures/Sunset.jpg}
%\caption{Sunset figure}
%\label{fig:rcle:sunset-fig2}
%\end{figure}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\subsubsection{This is a subsubsection}
%\begin{table}[H]
%\centering
%\caption{This is a table template - This is an example of a long table title.  Table titles need to be single-spaced within and double spaced between in the list of tables.}
%\begin{tabular}{|l|c|c|c|c|c|}
%\hline
%Product & 1 & 2 & 3 & 4 & 5\\
%\hline
%Price & 124.- & 136.- & 85.- & 156.- & 23.-\\
%Guarantee [years] & 1 & 2 & - & 3 & 1\\
%Rating & 89\% & 84\% & 51\% & & 45\%\\
%\hline
%\hline
%Recommended & yes & yes & no & no & no\\
%\hline
%\end{tabular}
%\label{tab:template1-2}
%\end{table}
%\section{Another Section}
