diff --git a/Recherche/ALDLoverAB/main.pdf b/Recherche/ALDLoverAB/main.pdf
index 1569599..452d17d 100644
Binary files a/Recherche/ALDLoverAB/main.pdf and b/Recherche/ALDLoverAB/main.pdf differ
diff --git a/Recherche/ALDLoverAB/main.tex b/Recherche/ALDLoverAB/main.tex
index d8668d4..1db871a 100644
--- a/Recherche/ALDLoverAB/main.tex
+++ b/Recherche/ALDLoverAB/main.tex
@@ -52,6 +52,7 @@
 \newcommand{\RBreceived}{\textsf{RB-received}}
 \newcommand{\ordered}{\textsf{ordered}}
 \newcommand{\Winners}{\mathsf{Winners}}
+\newcommand{\Messages}{\mathsf{Messages}}
 \newcommand{\ABlisten}{\textsf{AB-listen}}
 
 \newcommand{\delivered}{\mathsf{delivered}}
@@ -86,6 +87,7 @@ We consider a static set of $n$ processes with known identities, communicating b
 \paragraph{Communication.} Processes can exchange through a Reliable Broadcast (\RB) primitive (defined below) which's invoked with the functions \RBcast$(m)$ and \RBreceived$(m)$. There exists a shared object called DenyList (\DL) (defined below) that is interfaced with the functions \APPEND$(x)$, \PROVE$(x)$ and \READ$()$. 
 
 \paragraph{Notation.} Let $\Pi$ be the finite set of process identifiers and let $n \triangleq |\Pi|$. Two authorization subsets are $\Pi_M \subseteq \Pi$ (processes allowed to issue \APPEND) and $\Pi_V \subseteq \Pi$ (processes allowed to issue \PROVE). Indices $i,j \in \Pi$ refer to processes, and $p_i$ denotes the process with identifier $i$. Let $\mathcal{M}$ denote the universe of uniquely identifiable messages, with $m \in \mathcal{M}$. Let $\mathcal{R} \subseteq \mathbb{N}$ be the set of round identifiers; we write $r \in \mathcal{R}$ for a round. We use the precedence relation $\prec$ for the \DL{} linearization: $x \prec y$ means that operation $x$ appears strictly before $y$ in the linearized history of \DL. For any finite set $A \subseteq \mathcal{M}$, \ordered$(A)$ returns a deterministic total order over $A$ (e.g., lexicographic order on $(\textit{senderId},\textit{messageId})$ or on message hashes). For any round $r \in \mathcal{R}$, define $\Winners_r \triangleq \{\, j \in \Pi \mid (j,\PROVEtrace(r)) \prec \APPEND(r) \,\}$, i.e., the set of processes whose $\PROVE(r)$ appears before the first $\APPEND(r)$ in the \DL{} linearization.
+We denoted by $\PROVE^{(j)}(r)$ or $\APPEND^{(j)}(r)$ the operation $\PROVE(r)$ or $\APPEND(r)$ invoked by process $j$.
 
 % For any round r ∈ R, define Winnersr ≜ { j ∈ Π | (j, prove(r)) ≺ APPEND(r) }. Pas bien on compare des tuples et des operations
 
@@ -134,10 +136,6 @@ plus Integrity/No-duplicates/Validity (inherited from \RB and the construction).
   Equivalently, there exists a time after which every $\PROVE(r)$ is invalid in $H$.
 \end{definition}
 
-\begin{definition}[First APPEND]\label{def:first-append}
-  Given a \DL{} linearization $H$, for any closed round $r\in\mathcal{R}$, we denote by $\APPEND^\star(r)$ the earliest $\APPEND(r)$ in $H$.  
-\end{definition}
-
 \subsection{Variables}
 Each process $p_i$ maintains:
 
@@ -238,13 +236,17 @@ Once closed, a round never becomes open again.
 \end{lemma}
 
 \begin{proof}
-  By definition of closed round, some $\APPEND(r)$ occurs in the linearization $H$. \\
-  $H$ is a total order of operations, the set of $\APPEND(r)$ operations is totally ordered, and hence there exists a smallest $\APPEND(r)$ in $H$. We denote this operation $\APPEND^\star(r)$ and $t_0$ its linearization point. \\
-  By the validity property of \DL, a $\PROVE(r)$ is valid iff $\PROVE(r) \prec \APPEND^\star(r)$. Thus, after $t_0$, no $\PROVE(r)$ can be valid. \\
+  By \Cref{def:closed-round}, some $\APPEND(r)$ occurs in the linearization $H$. \\
+  $H$ is a total order of operations, the set of $\APPEND(r)$ operations is totally ordered, and hence there exists a smallest $\APPEND(r)$ in $H$. We denote this operation $\APPEND^{(\star)}(r)$ and $t_0$ its linearization point. \\
+  By the validity property of \DL, a $\PROVE(r)$ is valid iff $\PROVE(r) \prec \APPEND^{(\star)}(r)$. Thus, after $t_0$, no $\PROVE(r)$ can be valid. \\
   $H$ is a immutable grow-only history, and hence once closed, a round never becomes open again. \\
   Hence there exists a linearization point $t_0$ of $\APPEND(r)$ in the \DL, and from that point on, no $\PROVE(r)$ can be valid and the closure is stable. 
 \end{proof}
 
+\begin{definition}[First APPEND]\label{def:first-append}
+  Given a \DL{} linearization $H$, for any closed round $r\in\mathcal{R}$, we denote by $\APPEND^{(\star)}(r)$ the earliest $\APPEND(r)$ in $H$.  
+\end{definition}
+
 \begin{lemma}[Across rounds]\label{lem:across}
 If there exists a $r$ such that $r$ is closed, $\forall r'$ such that $r' < r$, r' is also closed.
 \end{lemma}
@@ -255,30 +257,34 @@ If there exists a $r$ such that $r$ is closed, $\forall r'$ such that $r' < r$,
   \emph{Induction.} Assume the lemma is true for round $k\geq 0$, we prove it for round $k+1$.
   
   \smallskip
-  Assume $k+1$ is closed and let $\APPEND^\star(k+1)$ be the earliest $\APPEND(k+1)$ in the DL linearization $H$.
+  Assume $k+1$ is closed and let $\APPEND^{(\star)}(k+1)$ be the earliest $\APPEND(k+1)$ in the DL linearization $H$.
   By Lemma 1, after an $\APPEND(k)$ is in $H$, any later $\PROVE(k)$ is rejected also, a process’s program order is preserved in $H$.
   
-  There are two possibilities for where $\APPEND^\star(k+1)$ is invoked.
-  
-  \paragraph{Case (B6).}
-  Some process $p^\star$ executes the loop (lines B5–B11) and invokes $\APPEND^\star(k+1)$ at line B6.
-  Immediately before line B6, line B5 sets $r\leftarrow r+1$, so the previous loop iteration (if any) targeted $k$. We consider two sub-cases.
-  
-  \emph{(i) $p^\star$ is not in its first loop iteration.}
-  In the previous iteration, $p^\star$ executed $\PROVE^\star(k)$ at B6, followed (in program order) by $\APPEND^\star(k)$. 
-  If round $k$ wasn't closed when $p^\star$ execute $\PROVE^\star(k)$ at B9, then the condition at B8 would be true hence the tuple $(p^\star, \PROVEtrace(k))$ should be visible in P which implies that $p^\star$ should leave the loop at round $k$, contradicting the assumption that $p^\star$ is now executing another iteration.
-  Since the tuple is not visible, the $\PROVE^\star(k)$ was rejected by the DL which implies by definition an $\APPEND(k)$ already exists in $H$. Thus in this case $k$ is closed.
-  
-  \emph{(ii) $p^\star$ is in its first loop iteration.}
-  To compute the value $r_{max}$, $p^\star$ must have observed one or many $(\_ , \PROVEtrace(k+1))$ in $P$ at B2/B3, issued by some processes (possibly different from $p^\star$). Let's call $p_1$ the issuer of the first $\PROVE(k+1)$ in the linearization $H$. \\
-  When $p_1$ executed $P \gets \READ()$ at B2 and compute $r_{max}$ at B3, he observed no tuple $(j,\PROVEtrace(k+1))$ in $P$ because he's the issuer of the first one. So when $p_1$ executed the loop (B5–B11), he run it for the round $k$, didn't seen any $(1,\PROVEtrace(k))$ in $P$ at B8, and then executed the first $\PROVE(k+1)$ at B6 in a second iteration. \\
-  If round $k$ wasn't closed when $p_1$ execute $\PROVE(k)$ at B6, then the condition at B8 should be true which implies that $p_1$ sould leave the loop at round $k$, contradicting the assumption that $p_1$ is now executing $\PROVE(r+1)$. In this case $k$ is closed.
-  
-  \paragraph{Case (C9).}
-  Some process invokes $\APPEND(k+1)$ at C9. 
-  Line C9 is guarded by the presence of $\PROVE(\textit{next})$ in $P$ with $\textit{next}=k+1$ (C6). 
-  Moreover, the local pointer $\textit{next}$ grow by increment of 1 and only advances after finishing the current round (C20), so if a process can reach $\textit{next}=k+1$ it implies that he has completed round $k$, which includes closing $k$ at C9 when $\PROVE(k)$ is observed. 
-  Hence $\APPEND^\star(k+1)$ implies a prior $\APPEND(k)$ in $H$, so $k$ is closed.
+  There are two possibilities for where $\APPEND^{(\star)}(k+1)$ is invoked.
+
+  \begin{itemize}
+    \item \textbf{Case (B6) :}
+    Some process $p^\star$ executes the loop (lines B5–B11) and invokes $\APPEND^{(\star)}(k+1)$ at line B6.
+    Immediately before line B6, line B5 sets $r\leftarrow r+1$, so the previous loop iteration (if any) targeted $k$. We consider two sub-cases.
+    
+    \begin{itemize}
+      \item \emph{(i) $p^\star$ is not in its first loop iteration.}
+      In the previous iteration, $p^\star$ executed $\PROVE^{(\star)}(k)$ at B6, followed (in program order) by $\APPEND^{(\star)}(k)$. 
+      If round $k$ wasn't closed when $p^\star$ execute $\PROVE^{(\star)}(k)$ at B9, then the condition at B8 would be true hence the tuple $(p^\star, \PROVEtrace(k))$ should be visible in P which implies that $p^\star$ should leave the loop at round $k$, contradicting the assumption that $p^\star$ is now executing another iteration.
+      Since the tuple is not visible, the $\PROVE^{(\star)}(k)$ was rejected by the DL which implies by definition an $\APPEND(k)$ already exists in $H$. Thus in this case $k$ is closed.
+    
+      \item \emph{(ii) $p^\star$ is in its first loop iteration.}
+      To compute the value $r_{max}$, $p^\star$ must have observed one or many $(\_ , \PROVEtrace(k+1))$ in $P$ at B2/B3, issued by some processes (possibly different from $p^\star$). Let's call $p_1$ the issuer of the first $\PROVE^{(1)}(k+1)$ in the linearization $H$. \\
+      When $p_1$ executed $P \gets \READ()$ at B2 and compute $r_{max}$ at B3, he observed no tuple $(\_,\PROVEtrace(k+1))$ in $P$ because he's the issuer of the first one. So when $p_1$ executed the loop (B5–B11), he run it for the round $k$, didn't seen any $(1,\PROVEtrace(k))$ in $P$ at B8, and then executed the first $\PROVE^{(1)}(k+1)$ at B6 in a second iteration. \\
+      If round $k$ wasn't closed when $p_1$ execute $\PROVE^{(1)}(k)$ at B6, then the condition at B8 should be true which implies that $p_1$ sould leave the loop at round $k$, contradicting the assumption that $p_1$ is now executing $\PROVE^{(1)}(r+1)$. In this case $k$ is closed.
+    \end{itemize}
+    
+    \item \textbf{Case (C9) :} 
+    Some process invokes $\APPEND(k+1)$ at C9. 
+    Line C9 is guarded by the presence of $\PROVE(\textit{next})$ in $P$ with $\textit{next}=k+1$ (C6). 
+    Moreover, the local pointer $\textit{next}$ grow by increment of 1 and only advances after finishing the current round (C20), so if a process can reach $\textit{next}=k+1$ it implies that he has completed round $k$, which includes closing $k$ at C9 when $\PROVE(k)$ is observed. 
+    Hence $\APPEND^\star(k+1)$ implies a prior $\APPEND(k)$ in $H$, so $k$ is closed.
+  \end{itemize}
   
   \smallskip
   In all cases, $k+1$ closed implie $k$ closed. By induction on $k$, if the lemme is true for a closed $k$ then it is true for a closed $k+1$.
@@ -286,11 +292,11 @@ If there exists a $r$ such that $r$ is closed, $\forall r'$ such that $r' < r$,
 \end{proof}
 
 \begin{definition}[Winner Invariant]\label{def:winner-invariant}
-  Let take a closed round $r$ (which implies by \Cref{def:closed-round} that some $\APPEND(r)$ occurs in the DL linearization $H$), there exist a unique and defined set of winners such as 
+  For any closed round $r$, define
   \[
-    \Winners_r = \{ j : (j,\PROVEtrace(r)) \prec \APPEND^\star(r) \}
+    \Winners_r \triangleq \{ j : \PROVE^{(j)}(r) \prec \APPEND^\star(r) \}
   \] 
-  with $\APPEND^\star(r)$ being the earliest \APPEND$(r)$ in the \DL linearization.
+  as the unique set of winners of round $r$.
 \end{definition}
 
 \begin{lemma}[Invariant view of closure]\label{lem:closure-view}
@@ -298,7 +304,7 @@ If there exists a $r$ such that $r$ is closed, $\forall r'$ such that $r' < r$,
 \end{lemma}
   
 \begin{proof}
-  Fix a round $r$ such that some $\APPEND(r)$ occurs; hence $r$ is \emph{closed}. By \Cref{lem:closure-stable}, there exists a unique earliest $\APPEND(r)$ in the DL linearization, denoted $\APPEND^\star(r)$.
+  Let's take a closed round $r$. By \Cref{def:first-append}, there exists a unique earliest $\APPEND(r)$ in the DL linearization, denoted $\APPEND^\star(r)$.
 
   Consider any correct process $p$ that invokes $\READ()$ after $\APPEND^\star(r)$ in the DL linearization. Since $\APPEND^\star(r)$ invalidates all subsequent $\PROVE(r)$, the set of valid tuples $(\_,\PROVEtrace(r))$ observed by any correct process after $\APPEND^\star(r)$ is fixed and identical across all correct processes.
 
@@ -306,106 +312,127 @@ If there exists a $r$ such that $r$ is closed, $\forall r'$ such that $r' < r$,
 \end{proof}
 
 \begin{lemma}[Well-defined winners]\label{lem:winners}
-In any execution, when a process computes $W_{r}$, $r$ is closed. 
+  For any correct process and round $r$, if the process computes $W_r$ at line C10, then :
+  \begin{itemize}
+    \item $\Winners_r$ is defined;
+    \item the computed $W_r$ is exactly $\Winners_r$.
+  \end{itemize}
 \end{lemma}
 
 \begin{proof}
-  Fix a process $p$ that reaches line C10 (computing $W_{\textit{next}}$). Immediately before C10, line C9 executes
+  Let take a correct process $p_i$ that reach line C10 to compute $W_r$. \\
+  By program order, $p_i$ must have executed $\APPEND^{(i)}(r)$ at C9 before, which implies by \Cref{def:closed-round} that round $r$ is closed. So by \Cref{def:winner-invariant}, $\Winners_r$ is defined. \\
+  By \Cref{lem:closure-view}, all correct processes eventually observe the same set of valid tuples $(\_,\PROVEtrace(r))$ in their \DL view. Hence, when $p_i$ executes the $\READ()$ at C9 after the $\APPEND^{(i)}(r)$, it observes a set $P$ that includes all valid tuples $(\_,\PROVEtrace(r))$ such that
   \[
-  \APPEND(\textit{next});\; P \gets \READ()
+    W_r = \{ j : (j,\PROVEtrace(r)) \in P \} = \{j : \PROVE^{(j)}(r) \prec \APPEND^\star(r) \} = \Winners_r
   \]
-  
-  Line C9 is guarded by the condition at line C6, which 
-\end{proof}
-
-\begin{lemma}[View-Invariant Winners]\label{lem:view-invariant}
-For any closed round $r$, there exists a unique set
-\[
-    \Winners_r = \{ j : (j,\PROVEtrace(r)) \prec \APPEND^\star(r) \}
-\]
-with $\APPEND^\star(r)$ being the earliest \APPEND$(r)$ in the \DL linearization.\\
-Such that for any correct process $p$ that computes $W_r$, $W_r = \Winners_r$.
-\end{lemma}
-
-\begin{proof}[Proof]
-  Fix a round $r$ such that some $\APPEND(r)$ occurs; hence $r$ is \emph{closed}. By \Cref{lem:closure-stable}, there exists a unique earliest $\APPEND(r)$ in the DL linearization, denoted $\APPEND^\star(r)$.
-
-  Consider any correct process $p$ that computes $W_r$ at line C10. By \Cref{lem:winners}, $r$ is closed when $p$ computes $W_r$. By \Cref{lem:closure-stable}, the linearization point of $\APPEND^\star(r)$ precedes that of the subsequent $\READ()$ at C9, therefore the $P$ returned by this $\READ()$ is posterior to $\APPEND^\star(r)$ in the DL linearization.
-
-  Hence, at the moment C10 computes
-  \[
-    W_r \;\leftarrow\; \{\, j : (j,\PROVEtrace(r)) \in P \,\},
-  \]
-  the view $P$ is posterior to $\APPEND^\star(r)$, so
-  \[
-    W_r = \{\, j : (j,\PROVEtrace(r)) \prec \APPEND^\star(r) \,\} = \Winners_r.
-  \]
-  
-  Since this argument holds for any correct process computing $W_r$, all correct processes compute the same winner set $\Winners_r$ for closed round $r$.
 \end{proof}
 
 \begin{lemma}[No APPEND without PROVE]\label{lem:append-prove}
-If some correct process invokes $\APPEND(r)$, then some correct process must have previously invoked $\PROVE(r)$.
+If some process invokes $\APPEND(r)$, then at least a process must have previously invoked $\PROVE(r)$.
 \end{lemma}
 
 \begin{proof}[Proof]
-  Consider the round $r$ such that some correct process invokes $\APPEND(r)$. There are two possible cases
+  Consider the round $r$ such that some process invokes $\APPEND(r)$. There are two possible cases
   
-  \paragraph{Case (B6).}
-  There exists a process $p^\star$ who's the issuer of the earliest $\APPEND^\star(r)$ in the DL linearization $H$. By program order, $p^\star$ must have previously invoked $\PROVE(r)$ before invoking $\APPEND^\star(r)$ at B6. In this case, there is at least one $\PROVE(r)$ valid in $H$ issued by a correct process before $\APPEND^\star(r)$.
-
-  \paragraph{Case (C9).}
-  There exist a process $p^\star$ invokes $\APPEND^\star(r)$ at C9. Line C9 is guarded by the condition at C6, which ensures that $p$ observed some $(\_,\PROVEtrace(r))$ in $P$. In this case, there is at least one $\PROVE(r)$ valid in $H$ issued by some process before $\APPEND^\star(r)$.
-
-  In both cases, if some correct process invokes $\APPEND(r)$, then some correct process must have previously invoked $\PROVE(r)$.
+  \begin{itemize}
+    \item \textbf{Case (B6) :}
+    There exists a process $p^\star$ who's the issuer of the earliest $\APPEND^{(\star)}(r)$ in the DL linearization $H$. By program order, $p^\star$ must have previously invoked $\PROVE^{(\star)}(r)$ before invoking $\APPEND^{(\star)}(r)$ at B6. In this case, there is at least one $\PROVE(r)$ valid in $H$ issued by a correct process before $\APPEND^{(\star)}(r)$.
+    
+    \item \textbf{Case (C9) :}
+    There exist a process $p^\star$ invokes $\APPEND^{(\star)}(r)$ at C9. Line C9 is guarded by the condition at C6, which ensures that $p$ observed some $(\_,\PROVEtrace(r))$ in $P$. In this case, there is at least one $\PROVE(r)$ valid in $H$ issued by some process before $\APPEND^{(\star)}(r)$.
+  \end{itemize}
+    
+  In both cases, if some process invokes $\APPEND(r)$, then some process must have previously invoked $\PROVE(r)$.
 \end{proof}
 
 \begin{lemma}[No empty winners]\label{lem:nonempty}
-For any correct process that computes $W_r$, $W_r \neq \emptyset$.
+  Let $r$ be a round, if $\Winners_r$ is defined, then $\Winners_r \neq \emptyset$.
 \end{lemma}
 
 \begin{proof}[Proof]
-  By \Cref{lem:winners}, any correct process that computes $W_r$ implies that round $r$ is closed. By \Cref{lem:closure-stable}, there exists a unique earliest $\APPEND(r)$ in the DL linearization, denoted $\APPEND^\star(r)$.
+  If $\Winners_r$ is defined, then by \Cref{def:winner-invariant}, round $r$ is closed. By \Cref{def:closed-round}, some $\APPEND(r)$ occurs in the DL linearization. \\
+  By \Cref{lem:append-prove}, at least a process must have invoked a valid $\PROVE(r)$ before $\APPEND^{(\star)}(r)$. Hence, there exists at least one $j$ such that $\{j: \PROVE^{(j)}(r) \prec \APPEND^\star(r)\}$, so $\Winners_r \neq \emptyset$.
+\end{proof}
 
-  By \Cref{lem:view-invariant}, any correct process computing $W_r$ obtains
+\begin{lemma}[Winners must propose]\label{lem:winners-propose}
+  For any closed round $r$, $\forall j \in \Winners_r$, process $j$ must have invoked a $\RBcast(S^{(j)}, r, j)$
+\end{lemma}
+
+\begin{proof}[Proof]
+  Fix a closed round $r$. By \Cref{def:winner-invariant}, for any $j \in \Winners_r$, there exist a valid $\PROVE^{(j)}(r)$ such that $\PROVE^{(j)}(r) \prec \APPEND^\star(r)$ in the DL linearization. By program order, if $j$ invoked a valid $\PROVE^{(j)}(r)$ at line B6 he must have invoked $\RBcast(S^{(j)}, r, j)$ directly before.
+\end{proof}
+
+\begin{definition}[Messages invariant]\label{def:messages-invariant}
+  For any closed round $r$ and any correct process $p_i$ such that $\nexists j \in \Winners_r : prop^{[i)}[r][j] = \bot$, define
   \[
-    W_r = \Winners_r = \{\, j : (j,\PROVEtrace(r)) \prec \APPEND^\star(r) \,\}.
+    \Messages_r \triangleq \bigcup_{j\in\Winners_r} \prop^{(i)}[r][j]
   \]
+  as the unique set of messages proposed by the winners of round $r$.
+\end{definition}
 
-  So
-  \[
-    W_r \neq \emptyset \implies \exists j : (j,\PROVEtrace(r)) \prec \APPEND^\star(r).
-  \]
+\begin{lemma}[Non-empty winners proposal]\label{lem:winner-propose-nonbot}
+  For any closed round $r$, $\forall j \in \Winners_r$, for any correct process $p_i$, eventually $\prop^{(i)}[r][j] \neq \bot$.  
+\end{lemma}
 
-  Consider any correct process $p$ that computes $W_k$ at line C10. We show that $k$ is closed when $p$ executed the $\READ$ operation at C9 by \Cref{lem:winners}. This implies that some process must have invoked $\APPEND(k)$, which by \Cref{lem:append-prove} implies that some correct process must have previously invoked $\PROVE(k)$. Hence there exists at least one $j$ such that $(j,\PROVEtrace(k)) \prec \APPEND^\star(k)$, so $W_k \neq \emptyset$.
+\begin{proof}[Proof]
+  Fix a closed round $r$. By \Cref{def:winner-invariant}, for any $j \in \Winners_r$, there exist a valid $\PROVE^{(j)}(r)$ such that $\PROVE^{(j)}(r) \prec \APPEND^\star(r)$ in the DL linearization. By \Cref{lem:winners-propose}, $j$ must have invoked $\RBcast(S^{(j)}, r, j)$.
+
+  Let take a process $p_i$, by \RB \emph{Validity}, every correct process eventually receives $j$'s \RB message for round $r$, which sets $\prop[r][j]$ to a non-$\bot$ value at line A3.
 \end{proof}
 
 \begin{lemma}[Eventual proposal closure]\label{lem:eventual-closure}
-  For any correct process $p_i$ that computes $M_r$ for round $r$, there exist no $j$ such that $j \in \Winners_r$ and $\prop^{(i)}[r][j] = \bot$.
+  If a correct process $p_i$ define $M_r$ at line C14, then for every $j \in \Winners_r$, $\prop^{(i)}[r][j] \neq \bot$. 
 \end{lemma}
 
 \begin{proof}[Proof]
-  Fix a correct process $p_i$ that computes $M_r$ at line C14. By \Cref{lem:winners}, $r$ is closed when $p_i$ executed the $\READ$ operation at C9. By \Cref{lem:view-invariant}, $p_i$ computes the unique winner set $\Winners_r$.
+  Let take a correct process $p_i$ that computes $M_r$ at line C14. By \Cref{lem:winners}, $p_i$ computes the unique winner set $\Winners_r$.
 
-  By \Cref{lem:nonempty}, $\Winners_r \neq \emptyset$. Consider any $j \in \Winners_r$. Since $j$ is a winner, by definition of $\Winners_r$, $j$ must have invoked a valid $\PROVE(r)$ before the earliest $\APPEND(r)$ in the DL linearization. Since $j$ is correct and by program order, if he invoked a valid $\PROVE(r)$ he must have invoked $\RBcast(S^{(j)}, r, j)$ directly before. By \RB \emph{Validity}, every correct process eventually receives $j$'s \RB message for round $r$, which sets $\prop[r][j]$ to a non-$\bot$ value (A3). The instruction C14 where $p_i$ computes $M_r$ is guarded by the condition at C11, which ensures that $p_i$ has received all \RB messages from every winner $j \in \Winners_r$. Hence, when $p_i$ computes $M_r = \bigcup_{j\in\Winners_r} \prop[r][j]$, we have $\prop[r][j] \neq \bot$ for all $j \in \Winners_r$.
+  By \Cref{lem:nonempty}, $\Winners_r \neq \emptyset$. The instruction at line C14 where $p_i$ computes $M_r$ is guarded by the condition at C11, which ensures that $p_i$ has received all \RB messages from every winner $j \in \Winners_r$. Hence, when $p_i$ computes $M_r = \bigcup_{j\in\Winners_r} \prop^{(i)}[r][j]$, we have $\prop^{(i)}[r][j] \neq \bot$ for all $j \in \Winners_r$.
 \end{proof}
 
 \begin{lemma}[Unique proposal per sender per round]\label{lem:unique-proposal}
-  For any round $r$ and any process $j$, $j$ invokes at most one $\RBcast(S, r, j)$.
+  For any round $r$ and any process $p_i$, $p_i$ invokes at most one $\RBcast(S, r, i)$.
 \end{lemma}
 
 \begin{proof}[Proof]
-  By program order, any process $j$ invokes $\RBcast(S, r, j)$ at line B6 must be in the loop (B5–B11). No matter the number of iterations of the loop, line B5 always uses the current value of $r$ which is incremented by 1 at line B5. Hence, in any execution, any process $j$ invokes $\RBcast(S, r, j)$ at most once for any round $r$.
+  By program order, any process $p_i$ invokes $\RBcast(S, r, i)$ at line B6 must be in the loop B5–B11. No matter the number of iterations of the loop, line B5 always uses the current value of $r$ which is incremented by 1 at each turn. Hence, in any execution, any process $p_i$ invokes $\RBcast(S, r, j)$ at most once for any round $r$.
 \end{proof}
 
 \begin{lemma}[Proposal convergence]\label{lem:convergence}
-For any closed round $r$, after all \RB messages from $\Winners_r$ are received, every correct process computes the same $M_r = \bigcup_{j\in \Winners_r} \prop[r][j]$.
+  For any round $r$, for any correct processes $p_i$ that define $M_r$ at line C14, we have
+  \[
+    M_r^{(i)} = \Messages_r
+  \]
 \end{lemma}
 
 \begin{proof}[Proof]
-  Fix a closed round $r$. By \Cref{lem:view-invariant}, any correct process computing $W_r$ obtains the same winner set $\Winners_r$. By \Cref{lem:eventual-closure}, every correct process that computes $M_r$ has received all \RB messages from every winner $j \in \Winners_r$, so $\prop[r][j]$ is non-$\bot$ for all $j \in \Winners_r$. By \Cref{lem:unique-proposal}, each winner $j$ invokes at most one $\RBcast(S^{(j)}, r, j)$, so $\prop[r][j] = S^{(j)}$ is uniquely defined. Hence, every correct process computes the same
+  Let take a correct process $p_i$ that define $M_r$ at line C14. That implies that $p_i$ has defined $W_r$ at line C10. It implies that, by \Cref{lem:winners}, $r$ is closed and $W_r = \Winners_r$. \\
+  By \Cref{lem:eventual-closure}, for every $j \in \Winners_r$, $\prop^{(i)}[r][j] \neq \bot$. By \Cref{lem:unique-proposal}, each winner $j$ invokes at most one $\RBcast(S^{(j)}, r, j)$, so $\prop^{(i)}[r][j] = S^{(j)}$ is uniquely defined. Hence, when $p_i$ computes
   \[
-    M_r = \bigcup_{j\in\Winners_r} \prop[r][j] = \bigcup_{j\in\Winners_r} S^{(j)}.
+    M_r^{(i)} = \bigcup_{j\in\Winners_r} \prop^{(i)}[r][j] = \bigcup_{j\in\Winners_r} S^{(j)} = \Messages_r.
+  \]
+\end{proof}
+
+\begin{lemma}[Inclusion]\label{lem:inclusion}
+  If some correct process invokes $\ABbroadcast(m)$, then there exist a round $r$ and a process $j\in\Winners_r$ such that $p_j$ invokes
+  \[
+  \RBcast(S, r, j)\quad\text{with}\quad m\in S.
+  \]
+\end{lemma}
+
+\begin{proof}
+  Fix a correct process $p_i$ that invokes $\ABbroadcast(m)$ and eventually exits the loop (B5–B11) at some round $r$. There are two possible cases.
+
+  \begin{itemize}
+    \item \textbf{Case 1:} $p_i$ exits the loop because $(i, \PROVEtrace(r)) \in P$. In this case, by \Cref{def:winner-invariant}, $p_i$ is a winner in round $r$. By program order, $p_i$ must have invoked $\RBcast(S, r, i)$ at B6 before invoking $\PROVE^{(i)}(r)$ at B7. By line B4, $m \in S$. Hence there exist a closed round $r$ and a correct process $j=i\in\Winners_r$ such that $j$ invokes $\RBcast(S, r, j)$ with $m\in S$.
+    
+    \item \textbf{Case 2:} $p_i$ exits the loop because $\exists j, r': (j, \PROVEtrace(r')) \in P \wedge m \in \prop[r'][j]$. In this case, by \Cref{lem:winners-propose} and \Cref{lem:unique-proposal} $j$ must have invoked a unique $\RBcast(S, r', j)$. Which set $\prop^{(i)}[r'][j] = S$ with $m \in S$.   
+  \end{itemize}
+    
+  In both cases, if some correct process invokes $\ABbroadcast(m)$, then there exist a round $r$ and a correct process $j\in\Winners_r$ such that $j$ invokes
+  \[
+    \RBcast(S, r, j)\quad\text{with}\quad m\in S.
   \]
 \end{proof}
 
@@ -414,73 +441,73 @@ For any closed round $r$, after all \RB messages from $\Winners_r$ are received,
 \end{lemma}
 
 \begin{proof}[Proof]
-  Fix a correct process $p$ that invokes $\ABbroadcast(m)$. The lemma is true iff $(i, \PROVEtrace(r)) \in P$ or $\exists j, r': (j, \PROVEtrace(r')) \in P \wedge m \in \prop[r'][j]$ (like guarded at B8).
+  Let a correct process $p_i$ that invokes $\ABbroadcast(m)$. The lemma is true if $(i, \PROVEtrace(r)) \in P$; or there exists $j: (j, \PROVEtrace(r')) \in P \wedge m \in \prop[r'][j]$ (like guarded at B8).
 
   \begin{itemize}
-    \item \textbf{Case 1:} there exists a round $r$ such that $p$ invokes $\PROVE(r)$ and this $\PROVE(r)$ is valid. Hence eventually $(i, \PROVEtrace(r)) \in P$ and $p$ exits the loop at B8.
-    \item \textbf{Case 2:} there exists no round $r$ such that $p$ invokes $\PROVE(r)$ and this $\PROVE(r)$ is valid. In this case $p$ invokes infinitely many $\RBcast(S, r, i)$ at B6 with $m \in S$ (line B4).\\
-    The assumption that no $\PROVE(r)$ invoked by $p$ is valid implies by \Cref{lem:nonempty} that for every possible round $r$ there at least one winner. Because there is an infinite number of rounds, and a finite number of processes, there exists at least one correct process $j$ that invokes infinitely many valid $\PROVE(r)$ and by extension infinitely many $\ABbroadcast(\_)$. By \RB \emph{Validity}, $j$ eventually receives $p$ 's \RB messages. Let call $t$ the time when $j$ receives $p$ 's \RB message \\
-    For the first invocation of $\ABbroadcast(m)$ by $j$ after $t$, $j$ must include $m$ in his proposal $S$ at B4 for round $r'$ (because $m$ is pending in $j$ 's $\received \setminus \delivered$). Because $j \in \Winners_{r'}$ and by \RB \emph{Validity}, every correct process eventually receives $j$ 's \RB message for round $r'$, including $p$. When $p$ receives $j$ 's \RB message, $\prop[r'][j]$ is set to a non-$\bot$ value (A3) which includes $m$. Hence eventually $\exists j, r': (j, \PROVEtrace(r')) \in P \wedge m \in \prop[r'][j]$ and $p$ exits the loop at B8.
+    \item \textbf{Case 1:} there exists a round $r'$ such that $p_i$ invokes a valid $\PROVE(r')$. Hence by \DL \emph{Progress} and \emph{Semantics} the following $\READ()$ at line B7 will defined a P such as $(i, \PROVEtrace(r')) \in P$. Hence $p_i$ exits the loop at B8.
+    \item \textbf{Case 2:} there exists no round $r'$ such that $p_i$ invokes a valid $\PROVE(r')$. In this case $p_i$ invokes infinitely many $\RBcast(S, r', i)$ at B6 with $m \in S$ (line B4).\\
+    The assumption that no $\PROVE(r')$ invoked by $p$ is valid implies by \DL \emph{Validity} that for every round $r'$, there exists at least one $\APPEND(r')$ in the DL linearization, hence by \Cref{lem:nonempty} for every possible round $r'$ there at least a winner. Because there is an infinite number of rounds, and a finite number of processes, there exists at least a correct process $p_k$ that invokes infinitely many valid $\PROVE(r')$ and by extension infinitely many $\ABbroadcast(\_)$. By \RB \emph{Validity}, $p_k$ eventually receives $p_i$ 's \RB messages. Let call $t_0$ the time when $p_k$ receives $p_i$ 's \RB message. \\
+    At $t_0$, $p_k$ execute \Cref{alg:rb-handler} and do $\received \leftarrow \received \cup \{S\}$ with $m \in S$ (line A2). 
+    For the first invocation of $\ABbroadcast(\_)$ by $p_k$ after the execution of \Cref{alg:rb-handler}, $p_k$ must include $m$ in his proposal $S$ at line B4 (because $m$ is pending in $j$'s $\received \setminus \delivered$ set). There exists a minimum round $r_1$ such that $p_k \in \Winners_{r_1}$ after $t_0$. By \Cref{lem:winner-propose-nonbot}, eventually $\prop^{(i)}[r_1][k] \neq \bot$. By \Cref{lem:unique-proposal}, $\prop^{(i)}[r_1][k]$ is uniquely defined as the set $S$ proposed by $p_k$ at B6, which by \Cref{lem:inclusion} includes $m$. Hence eventually $m \in \prop^{(i)}[r_1][k]$ and $k \in \Winners_{r_1}$. 
   \end{itemize}
-  The first case explicit the case where $p$ is a winner and also covers the condition $(i, \PROVEtrace(r)) \in P$. And in the second case, we show that if the first condition is never satisfied, the second one will eventually be satisfied. Hence either the first or the second condition will eventually be satisfied, and $p$ eventually exits the loop and returns from $\ABbroadcast(m)$.
+  The first case explicit the case where $p_i$ is a winner and also covers the condition $(i, \PROVEtrace(r')) \in P$. And in the second case, we show that if the first condition is never satisfied, the second one will eventually be satisfied. Hence either the first or the second condition will eventually be satisfied, and $p_i$ eventually exits the loop and returns from $\ABbroadcast(m)$.
 \end{proof}
-  
-
-\begin{lemma}[Inclusion]\label{lem:inclusion}
-If some correct process invokes $\ABbroadcast(m)$, then there exist a (closed) round $r$ and a corrcet process $j\in\Winners_r$ such that $j$ invokes
-\[
-\RBcast(S, r, j)\quad\text{with}\quad m\in S.
-\]
-\end{lemma}
-
-\begin{proof}
-  Fix a correct process $p$ that invokes $\ABbroadcast(m)$. By \Cref{lem:bcast-termination}, $p$ eventually exits the loop (B5–B11) at some round $r$. There are two possible cases.
-
-  \paragraph{Case 1:} $p$ exits the loop because $(i, \PROVEtrace(r)) \in P$. In this case, $p$ is a winner in round $r$ by definition of $\Winners_r$. By program order, $p$ must have invoked $\RBcast(S, r, i)$ at B6 before invoking $\PROVE(r)$ at B7. By line B4, $m \in S$. Hence there exist a closed round $r$ and a correct process $j=i\in\Winners_r$ such that $j$ invokes $\RBcast(S, r, j)$ with $m\in S$.
-
-  \paragraph{Case 2:} $p$ exits the loop because $\exists j, r': (j, \PROVEtrace(r')) \in P \wedge m \in \prop[r'][j]$. In this case, by \Cref{lem:view-invariant}, any correct process computing $W_{r'}$ obtains the unique winner set $\Winners_{r'}$, so $j\in\Winners_{r'}$. By program order, $j$ must have invoked $\RBcast(S, r', j)$ at B6 before invoking $\PROVE(r')$ at B7. By line B4, $m \in S$. Hence there exist a closed round $r'=r$ and a correct process $j\in\Winners_{r'}$ such that $j$ invokes $\RBcast(S, r', j)$ with $m\in S$.
-
-  In both cases, if some correct process invokes $\ABbroadcast(m)$, then there exist a (closed) round $r$ and a correct process $j\in\Winners_r$ such that $j$ invokes
-  \[
-    \RBcast(S, r, j)\quad\text{with}\quad m\in S.
-  \]
-\end{proof}
-
-
-% \begin{proof}[Proof]
-  % 2 cas, p_i est winner et cest gagné.
-  % Si p_i n'est pas winner on fait par l'absurde comme quoi personne ne propose m. Et on montre que c'est impossible.
-
-  % S est modif a chaque iteration de la boucle. On montre que y a un plus petit S bloqué
-
-  % Pour sortir de la boucle on doit avoir A ou B vrai, et il faut montrer que non A implique B
-% \end{proof}
 
 \begin{lemma}[Validity]\label{lem:validity}
-  If a correct process $p$ invokes $\ABbroadcast(m)$, then every correct process who eventually invokes $\ABdeliver()$ delivers $m$.
+  If a correct process $p$ invokes $\ABbroadcast(m)$, then every correct process that invokes a infinitely often times $\ABdeliver()$ eventually delivers $m$.
 \end{lemma}
 
 \begin{proof}[Proof]
-  Fix a correct process $p$ that invokes $\ABbroadcast(m)$. By \Cref{lem:inclusion}, there exist a closed round $r$ and a correct process $j\in\Winners_r$ such that $j$ invokes
+  Let $p_i$ a correct process that invokes $\ABbroadcast(m)$ and $p_q$ a correct process that infinitely invokes $\ABdeliver()$. By \Cref{lem:inclusion}, there exist a closed round $r$ and a correct process $j\in\Winners_r$ such that $p_j$ invokes
   \[
     \RBcast(S, r, j)\quad\text{with}\quad m\in S.
   \]
 
-  Consider any correct process $q$ that eventually invokes $\ABdeliver()$. By \Cref{lem:eventual-closure}, when $q$ computes $M_r$ at line C14, $\prop[r][j]$ is non-$\bot$ because $j \in \Winners_r$. By \Cref{lem:unique-proposal}, $j$ invokes at most one $\RBcast(S, r, j)$, so $\prop[r][j] = S$ is uniquely defined. Hence, when $q$ computes
+  By \Cref{lem:eventual-closure}, when $p_q$ computes $M_r$ at line C14, $\prop[r][j]$ is non-$\bot$ because $j \in \Winners_r$. By \Cref{lem:unique-proposal}, $p_j$ invokes at most one $\RBcast(S, r, j)$, so $\prop[r][j]$ is uniquely defined. Hence, when $p_q$ computes
   \[
     M_r = \bigcup_{k\in\Winners_r} \prop[r][k],
   \]
-  we have $m \in \prop[r][j] = S$, so $m \in M_r$. By line C16–C18, $m$ is enqueued into $to\_deliver$ unless it has already been delivered. Therefore, when $q$ eventually invokes $\ABdeliver()$, it eventually delivers $m$.
+  we have $m \in \prop[r][j] = S$, so $m \in M_r$. By line C16–C18, $m$ is enqueued into $to\_deliver$ unless it has already been delivered. Therefore, $p_q$ will eventually invokes $\ABdeliver()$, which will returns $m$.
 \end{proof}
 
-\begin{lemma}[Total Order]\label{lem:total-order}
-  For any two messages $m_1$ and $m_2$ broadcast by correct processes such that $m_1$ is broadcast before $m_2$, any correct process $p_j$ that delivers both $m_1$ and $m_2$ delivers $m_1$ before $m_2$.
+\begin{lemma}[Across \ABdeliver]\label{lem:across-abdeliver}
+  A $\ABdeliver()$ invocation return $m$, a non-$\bot$ value, implie that there exist an invocation of $\ABdeliver()$ which is the earliest of the round $r$ where $m$ is proposed by a winner and which define $M_r$.   
 \end{lemma}
 
-\begin{proof}[Proof]
-  Fix two messages $m_1$ and $m_2$ broadcast by correct processes. Consider any correct process $p_i$ that delivers $m_1$ before $m_2$. By program order, $p_i$ must have invoked $\ABbroadcast(m_1)$ before $\ABbroadcast(m_2)$. Let $r_1$ and $r_2$ be the rounds at which $p_i$ exits the loop (B5–B11) when invoking $\ABbroadcast(m_1)$ and $\ABbroadcast(m_2)$ respectively. By program order, $r_1 < r_2$.
+\begin{proof}
+  Let take any $\ABdeliver()$ invocation which return a non-$\bot$ value, $m$ which was proposed in round $r$. To return a non-$\bot$ value we can distinguish two cases:
+  \begin{itemize}
+    \item This actual invocation of $\ABdeliver$ have the queue $to\_deliver \neq \emptyset$ which implies that there exist an earliest invocation of $\ABdeliver$ which reach the line C17 to fill this queue for round $next = r$. We can call this invocation $\ABdeliver^{(\star r)}$. $\ABdeliver^{(\star r)}$ have to fill $to\_deliver$ at line C17, hence by program order define $M_r$ at C14.
+    \item This actual invocation of $\ABdeliver$ have the queue $to\_deliver = \emptyset$. To return a non-$\bot$ this execution have to pass the two conditions at lines C6 and C11 to compute $m_r$. Hence $\ABdeliver()$ is the $\ABdeliver^{(\star r)}()$ as described in the first case.
+  \end{itemize}  
+\end{proof}
 
-  Consider any correct process $p_j$ that delivers both $m_1$ and $m_2$. By \Cref{lem:validity}, there exist closed rounds $r'_1$ and $r'_2$ and correct processes $k_1 \in \Winners_{r'_1}$ and $k_2 \in \Winners_{r'_2}$ such that
+\begin{definition}[First \ABdeliver]\label{def:first-abdeliver}
+  For any process which invoke an infinite times $\ABdeliver()$. There exist for any round $r$ an unique earliest invocation which defined $M_r$ and return a non-$\bot$ value. We denote by $\ABdeliver^{(\star r)}()$ this invocation. 
+\end{definition}
+
+\begin{lemma}[No duplication]\label{lem:no-duplication}
+  No correct process delivers the same message more than once.
+\end{lemma}
+
+\begin{proof}
+  Let consider two invokations of $\ABdeliver()$ made by the same correct process which returns respectively $m_1$ and $m_2$. Let call these two invokations respectively $\ABdeliver^{(A)}()$ and $\ABdeliver^{(B)}()$.
+
+  By \Cref{def:first-abdeliver} we denote $\ABdeliver^{(\star A)}()$ and $\ABdeliver^{(\star B)}()$ the two earliest invocations of each $\ABdeliver()$ respectively in theirs rounds with $A$ the round where $m_1$ is delivered and $B$ the round where $m_2$ is delivered.
+
+  Let consider the following cases :
+  \begin{itemize}
+    \item \textbf{$A < B$ :} Let consider $m_1 = m_2 = m$. In the execution of $\ABdeliver^{(\star A)}$ the process iterate on line C17 and push $m$ in $to\_deliver$ since $m$ is not in $\delivered$. When the process invoke later $\ABdeliver^{(\star B)}$ he empties the queue. The only way to empties the queue is at line C22 which implie by program order to add $m$ to the $\delivered$ set. Hence when $\ABdeliver^{(\star B)}$ iterate on line C17 he will never be able to push $m$ in the queue because the condition $m \not\in \delivered$ at line C16 is never satisfied. Hence in this case $\ABdeliver^{(B)}()$ can't happen if $m_1 = m_2$.
+    \item \text{$A = B$ :} Let consider $m_1 = m_2 = m$. $\ABdeliver^{(\star A)}$ and $\ABdeliver^{(\star B)}$ reference the same invocation of $\ABdeliver()$. In this unique execution, when the process define $M_r$ he's making a union operation on all the sets which can contains a multiple times the same message $m$. This operation must result in a unique set which contain a unique time $m$. Hence when the iteration on C17 is done, $m$ is pushed only once, and can be delivered only once too. So $\ABdeliver^{(B)}()$ can't happen if $m_1 = m_2$.
+  \end{itemize}
+\end{proof}
+
+\begin{lemma}[Total order]\label{lem:total-order}
+  For any two messages $m_1$ and $m_2$ delivered by correct processes, if a correct process $p_i$ delivers $m_1$ before $m_2$, then any correct process $p_j$ that delivers both $m_1$ and $m_2$ delivers $m_1$ before $m_2$.  
+\end{lemma}
+
+\begin{proof}
+  Consider any correct process that delivers both $m_1$ and $m_2$. By \Cref{lem:validity}, there exist closed rounds $r'_1$ and $r'_2$ and correct processes $k_1 \in \Winners_{r'_1}$ and $k_2 \in \Winners_{r'_2}$ such that
   \[
     \RBcast(S_1, r'_1, k_1)\quad\text{with}\quad m_1\in S_1,
   \]
@@ -488,11 +515,36 @@ If some correct process invokes $\ABbroadcast(m)$, then there exist a (closed) r
     \RBcast(S_2, r'_2, k_2)\quad\text{with}\quad m_2\in S_2.
   \]
 
-  By program order, $p_i$ must have waited for the loop (B5–B11) to exit at round $r_1$ before invoking $\ABbroadcast(m_2)$. Hence, $r_1 \leq r'_1 < r_2 \leq r'_2$, so $r'_1 < r'_2$. Because $p_j$ delivers messages in round order (C5–C20), $p_j$ delivers all messages from round $r'_1$ (including $m_1$) before delivering any message from round $r'_2$ (including $m_2$). Therefore, $p_j$ delivers $m_1$ before $m_2$.
+  Let consider three cases :
+  \begin{itemize}
+    \item \textbf{Case 1:} $r_1 < r_2$. By program order, any correct process must have waited to empty the queue $to\_deliver$ (which contains $m_1$) to exit at round $r_1$ before invoking $\ABdeliver()$ that returns $m_2$. Hence, for any correct process that delivers both $m_1$ and $m_2$, it delivers $m_1$ before $m_2$.
+    
+    \item \textbf{Case 2:} $r_1 = r_2$. By \Cref{lem:convergence}, any correct process that computes $M_{r_1}$ at line C14 computes the same set of messages $\Messages_{r_1}$. By line C16–C18, messages are enqueued into $to\_deliver$ in a deterministic order defined by $\ordered(\_)$. Hence, for any correct process that delivers both $m_1$ and $m_2$, it delivers $m_1$ and $m_2$ in the deterministic order defined by $\ordered(\_)$.
+  \end{itemize}
+
+  In all possible cases, any correct process that delivers both $m_1$ and $m_2$ delivers $m_1$ and $m_2$ in the same order.
 \end{proof}
 
-\begin{theorem}[\ARB]
-Under the assumed \DL synchrony and \RB reliability, the algorithm implements Atomic Reliable Broadcast.
+\begin{lemma}[Fifo Order]\label{lem:fifo-order}
+  For any two messages $m_1$ and $m_2$ broadcast by the same correct process $p_i$, if $p_i$ invokes $\ABbroadcast(m_1)$ before $\ABbroadcast(m_2)$, then any correct process $p_j$ that delivers both $m_1$ and $m_2$ delivers $m_1$ before $m_2$.
+\end{lemma}
+
+\begin{proof}
+  Let take two messages $m_1$ and $m_2$ broadcast by the same correct process $p_i$, with $p_i$ invoking $\ABbroadcast(m_1)$ before $\ABbroadcast(m_2)$. By \Cref{lem:validity}, there exist closed rounds $r_1$ and $r_2$ and correct processes $k_1 \in \Winners_{r_1}$ and $k_2 \in \Winners_{r_2}$ such that
+  \[
+    \RBcast(S_1, r_1, k_1)\quad\text{with}\quad m_1\in S_1,
+  \]
+  \[
+    \RBcast(S_2, r_2, k_2)\quad\text{with}\quad m_2\in S_2.
+  \]
+
+  By program order, $p_i$ must have invoked $\RBcast(S_1, r_1, i)$ before $\RBcast(S_2, r_2, i)$. By \Cref{lem:unique-proposal}, any process invokes at most one $\RBcast(S, r, i)$ per round, hence $r_1 < r_2$. By \Cref{lem:total-order}, any correct process that delivers both $m_1$ and $m_2$ delivers them in a deterministic order.
+  
+  In all possible cases, any correct process that delivers both $m_1$ and $m_2$ delivers $m_1$ before $m_2$.
+\end{proof}
+
+\begin{theorem}[FIFO-\ARB]
+Under the assumed \DL synchrony and \RB reliability, the algorithm implements FIFO Atomic Reliable Broadcast.
 \end{theorem}
 
 \bibliographystyle{plain}