remove redundant lemma and add inclusion lemma

Recherche/BFT-ARBover/5_BFT_ARB/index.tex

@@ -422,10 +422,6 @@ For each $U \in \mathcal{U}$, we instantiate one DenyList object $DL_U$ whose au
     By strong induction, if round $r$ is closed, all rounds $r_1 < r$ are closed.
 \end{proof}
 
-\begin{lemma}[Eventual Closure]\label{lem:eventual-closure}
-    For any correct process $p_i$, if $\unordered \setminus \ordered \neq \emptyset$ and if $r$ is the highest closed round observed by $p_i$, then eventually round $r+1$ will be closed with $|\winners[r+1]| \geq n - t$.
-\end{lemma}
-
 \begin{lemma}[Uniqueness of Winners' Proposals]\label{lem:unique-proposal}
     For any closed round $r$ and any process $p_j \in \winners[r]$, there exists a unique set $S_j \subseteq \mathcal{M}$ such that every correct process $p_i$ that has received a reliable delivery of a $\texttt{PROP}$ message from $p_j$ for round $r$ receives exactly this set $S_j$.
 \end{lemma}
@@ -489,6 +485,32 @@ For each $U \in \mathcal{U}$, we instantiate one DenyList object $DL_U$ whose au
     Therefore, all correct processes compute the same set $M$ for any closed round $r$.
 \end{proof}
 
+\begin{lemma}[Inclusion]\label{lem:inclusion}
+    If a correct process $p_i$ invokes $\ABbroadcast(m)$, then there exist a closed round $r$ and a winner $j \in \winners[r]$ such that $p_j$ invoked $\RBcast(j, \texttt{PROP}, S, r)$ with $m \in S$.
+\end{lemma}
+
+\begin{proof}
+    Let $p_i$ be a correct process that invokes $\ABbroadcast(m)$. By the algorithm, $p_i$ adds $m$ to $\unordered$. Consequently, $\unordered \setminus \ordered \neq \emptyset$, and the process enters the main loop and eventually invokes $\RBcast(i, \texttt{PROP}, S_i^{(1)}, r_1)$ for some round $r_1$ where $m \in S_i^{(1)}$.
+
+    We distinguish two cases:
+    
+    \textbf{Case 1: $p_i$ becomes a winner in round $r_1$.}
+    If $p_i$ is elected as a winner for round $r_1$ (i.e., $i \in \winners[r_1]$), then the claim holds with $r = r_1$ and $j = i$.
+    
+    \textbf{Case 2: $p_i$ does not become a winner in round $r_1$.}
+    If $p_i$ is not elected as a winner, by the properties of Reliable Broadcast (Bracha's specification), at least one correct process $p_{i_1}$ will eventually receive the reliable delivery of the $\texttt{PROP}$ message from $p_i$ for round $r_1$. Process $p_{i_1}$ adds all messages from $S_i^{(1)}$ to its $\unordered$ set at line \ref{alg:append}. In particular, $m$ is now in $p_{i_1}$'s $\unordered$ set.
+    
+    In round $r_2 > r_1$ (and any subsequent round), process $p_{i_1}$ computes $S_{i_1}^{(2)} = \unordered \setminus \ordered$ and invokes $\RBcast(i_1, \texttt{PROP}, S_{i_1}^{(2)}, r_2)$ with $m \in S_{i_1}^{(2)}$.
+    
+    This process repeats: either $p_{i_1}$ becomes a winner and the claim holds, or another correct process receives $p_{i_1}$'s proposal and includes $m$ in its own proposal.
+    
+    Since $n > 3f$, we have $n - t > t + 1 > f$. By the pigeonhole principle, there eventually exists a round $r$ where at least $n - t$ distinct processes have proposed sets containing $m$. Since more than $2f$ processes have proposed $m$, at least one of them must be correct and be elected as a winner. Therefore, there exist a round $r$ and a winner $j \in \winners[r]$ such that $m \in S_j$ was broadcast by $p_j$.
+\end{proof}
+
+\begin{lemma}[Eventual Closure]\label{lem:eventual-closure}
+    For any correct process $p_i$, if $\unordered \setminus \ordered \neq \emptyset$ and if $r$ is the highest closed round observed by $p_i$, then eventually round $r+1$ will be closed with $|\winners[r+1]| \geq n - t$.
+\end{lemma}
+
 \begin{lemma}[Total Order]\label{lem:total-order}
     For any two correct processes $p_i$ and $p_j$, the sequence $\ordered$ maintained locally by $p_i$ and the sequence maintained by $p_j$ contain the same messages in the same order, provided that both have reached the same set of closed rounds.
 \end{lemma}