We define $k$ as the id of the round \\
the $getMax(proves)$ return $MAX({(\_, r) : \exists (\_, PROVE(r)) \in proves})$ \\
$buffer$ a FIFO list with $buffer[front]$ returning the first element

% \begin{algorithm}[H]
% \DontPrintSemicolon
% \SetAlgoLined
% \KwIn{le message $m$}
% \BlankLine
% \While{true}{
%   proves = READ() \\
%   k = getMax(dump) + 1 \\
%   APPEND(k || m) \\
%   \If{PROVE(k)}{
%     APPEND(k) \\
%     return
%   }
% }
% \caption{AB\_Broadcast}
% \end{algorithm}

\begin{algorithm}[H]
\DontPrintSemicolon
\SetAlgoLined
\KwIn{le message $m$}
\BlankLine
k\_max = getMax(READ()) \\
\While{buffer $\neq [\emptyset] $}{
  (i, m) = buffer[front] \\
  \textbf{wait} PROVE(k\_max || m) = false \\
  proves = READ() \\
  \If{$((i, PROVE(k\_max || m)) \in proves) \wedge ((i, PROVE(k\_max)) \in proves)$}{
    $buffer = buffer - \{(i, m)\}$
  }
}
\BlankLine
\While{true}{
  proves = READ() \\
  k = getMax(proves) + 1 \\
  PROVE(k || m) \\
  APPEND(k || m) \\
  \If{PROVE(k)}{
    APPEND(k) \\
    return
  }
}
\caption{AB\_Broadcast}
\end{algorithm}

$proves_r = {(i, r) : \forall i, \exists (i, PROVE(r)) \in proves}$ \\
$proves_r^i = ((i, r) : \exists (i, PROVE(r)) \in proves)$ ?? NULL \\

% $proves_r \subseteq proves$ s.a. $\forall PROVE(x) \in proves_r$, x is in the form $r || m$ with $m$ who cannot be empty \\
% $proves_r^i$ is the $PROVE(r || m )$ operation submited by the process i if exist \\

\begin{algorithm}[H]
  \DontPrintSemicolon
  \SetAlgoLined
  buffer = $[\emptyset]$ \\
  k = 0 \\
  \BlankLine
  \While{true}{
    proves = READ() \\
    k\_max = getMax(proves) \\
    \For{r=k+1 \emph{\KwTo} k\_max}{
      APPEND(r)\\
      \For{i = 1 \emph{\KwTo} $|P|$}{
        \If{$(\exists m : \exists(i, PROVE(r || m)) \in proves)$}{
          \uIf{$(\exists(i, PROVE(r)) \in proves)$} {
            AB\_Recv(m)
          }
          \Else{
            $buffer = buffer \cup \{(i, m)\}$
          }
        }
      }
    }
  }
\caption{AB\_Listen}
\end{algorithm}
  
% \begin{algorithm}[H]
%   \DontPrintSemicolon
%   \SetAlgoLined
%   \BlankLine
%   \While{true}{
%     proves = READ() \\
%     k\_max = getMax(proves) \\
%     \For{r=k+1 \emph{\KwTo} k\_max}{
%       APPEND(r)\\
%       $proves_r$ = \{$\forall i, PROVE(r)_i \in READ()$\} \\
%       \For{i = 1 \emph{\KwTo} $|P|$}{
%         \If{$\exists PROVE(r)_i \in proves_r$}{
%           AB\_Recv($m$ s.t. $PROVE(r || m) \in proves$)
%         }
%       }
%     }
%   }
  
%   \caption{AB\_Listen}
% \end{algorithm}