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
  
  $rcved = rcved \bigcup \{m\}$ \;
  \textbf{upon} RB\_deliver(PROP, r, S) \textbf{from} j \;
  prop[r][j] = S

  \caption{\textbf{Upon} RB\_deliver(m)}
\end{algorithm}

\begin{algorithm}[H]
\DontPrintSemicolon
\SetAlgoLined
\KwIn{le message $m$}

\KwData{rcved = $\emptyset$ \;
delivered = $\emptyset$ \;
r = 0 \;}

\BlankLine

RB\_cast(m) \;
$rcved = rcvd \bigcup \{m\}$ \;

\While{true}{
  $r = r+1$ \;
  $RB\_cast(PROP, r, S)$ \;
  PROVE(r) \;
  APPEND(r) \;
  proves = READ() \;
  $winner^r = \{j : (j, PROVE(r)) \in proves\}$ \;
  \textbf{wait until} $(\forall j \in winner^k: prop[r][j])$ \;
  \If{$\exists j \in winner^k : m \in prop[r][j]$}{
    break \;
  }
}

\caption{AB\_Broadcast}
\end{algorithm}

\begin{algorithm}[H]
  \DontPrintSemicolon
  \SetAlgoLined

  r\_prev = 0 \;
  \While{true}{
    proves = READ() \;
    $r\_max = MAX(\{r : \exists i, (i, PROVE(r)) \in proves\})$ \; 
    \For{$r = r\_prev + 1 \textbf{to} r\_max$}{
      APPEND(r) \;
      proves = READ() \;
      $winner^k = \{j : (j, PROVE(r)) \in proves \}$ \;
      $\textbf{wait until} (\forall j \in winner^k : prop[r][j] \neq \emptyset)$ \;
      $M^r = (\bigcup_{j \in winner^k} prop[r][j]) \setminus delivered$ \;
      
      \tcc*{we assume $M^r$ as an ordered list s.a. $\forall m_1, m_2, if m_1 < m_2$, $m_1$ appears before $m_2$ in $M^r$}

      \BlankLine
      
      \ForEach{$m \in M^r$}{
        $delivered = delivered \bigcup \{m\}$ \;
        AB\_deliver(m) \;
      } 
    }
  }
\caption{AB\_Listen}
\end{algorithm}