Redaction des deux derniers lemmes du BFT + explication des algos + transition partie crash partie byzantine plus fluide

Recherche/BFT-ARBover/4_ARB_with_RB_DL/index.tex

@@ -66,6 +66,10 @@ We present below an example of implementation of Atomic Reliable Broadcast (\ARB
   }
 
 \end{algorithm}
+
+\paragraph{Algorithm intuition.}
+The crash-tolerant algorithm is organized around round closure and winner extraction. By \Cref{def:closed-round,def:first-append,lem:closure-view,lem:winners}, once a round is closed, every correct process eventually reads the same winner set $\Winners_r$. By \Cref{lem:nonempty}, this set is never empty, and by \Cref{lem:winners-propose} every winner has necessarily sent its proposal to all processes before becoming a winner, exactly because sending precedes $\PROVE(r)$ and $\APPEND(r)$ at line~\ref{code:submit-proposition}. Under reliable channels, these winner proposals are eventually received by every correct process, so the waiting condition at line~\ref{code:check-winners-ack} eventually becomes true, which is formalized by \Cref{lem:eventual-closure}. Then, by \Cref{lem:convergence}, all correct processes compute the same set $M$ at line~\ref{code:Mcompute-dl}, and because line~\ref{code:next-msg-extraction} applies the same deterministic ordering function, they append messages in the same order; this is exactly the core mechanism later used in \Cref{lem:validity,lem:no-duplication,lem:total-order}.
+
 \subsection{Correctness}
 
 \begin{definition}[First APPEND]\label{def:first-append}