\begin{theorem}[Integrity]
    If a message $m$ is delivered by any process, then it was previously broadcast by some process via the \texttt{AB-broadcast} primitive.
\end{theorem}

\begin{proof}
    Let $j$ be a process such that $\text{AB-deliver}_j(m)$ occurs.

    \begin{align*}
        &\text{AB-deliver}_j(m) & \text{(line 24)} \\
        \Rightarrow\; &\exists r_0 : m \in \texttt{ordered}(M^{r_0}) & \text{(line 22)} \\
        \Rightarrow\; &\exists j_0 : j_0 \in \textit{winner}^{r_0} \land m \in \textit{prop}[r_0][j_0] & \text{(line 21)} \\
        \Rightarrow\; &\exists m_0, S_0 : \text{RB-received}_{j_0}(m_0, S_0, r_0, j_0) \land m \in S_0 & \text{(line 2)} \\
        \Rightarrow\; &S_0 = (\textit{received}_{j_0} \setminus \textit{delivered}_{j_0}) \cup \{m_1\} & \text{(line 5)} \\
        \Rightarrow\; &\textbf{if } m_1 = m: \exists\, \text{AB-broadcast}_{j_0}(m) \hspace{1em} \square \\
        &\textbf{else if } m_1 \neq m: \\
        &\quad m \in \textit{received}_{j_0} \setminus \textit{delivered}_{j_0} \Rightarrow m \in \textit{received}_{j_0} \land m \notin \textit{delivered}_{j_0} \\
        &\quad \exists j_1, S_1, r_1 : \text{RB-received}_{j_1}(m, S_1, r_1, j_1) & \text{(line 1)} \\
        &\quad \Rightarrow \exists\, \text{AB-broadcast}_{j_1}(m) \hspace{1em} \square & \text{(line 5)}
    \end{align*}
\end{proof}
    



\begin{theorem}[No Duplication]
    No message is delivered more than once by any process.
\end{theorem}

\begin{proof}
    Let $j$ be a process such that both $\text{AB-deliver}_j(m_0)$ and $\text{AB-deliver}_j(m_1)$ occur, with $m_0 = m_1$.

    \begin{align*}
        &\text{AB-deliver}_j(m_0) \wedge \text{AB-deliver}_j(m_1) & \text{(line 24)} \\
        \Rightarrow\; & m_0, m_1 \in \textit{delivered}_j & \text{(line 23)} \\
        \Rightarrow\; &\exists r_0, r_1 : m_0 \in M^{r_0} \wedge m_1 \in M^{r_1} & \text{(line 22)} \\
        \Rightarrow\; &\exists j_0, j_1 : m_0 \in \textit{prop}[r_0][j_0] \wedge m_1 \in \textit{prop}[r_1][j_1] \\
        &\hspace{2.5em} \wedge\ j_0 \in \textit{winner}^{r_0},\ j_1 \in \textit{winner}^{r_1} & \text{(line 21)}
    \end{align*}
    
    We now distinguish two cases:
    
    \vspace{0.5em}
    \noindent\textbf{Case 1:} $r_0 = r_1$:
    \begin{itemize}
        \item If $j_0 \neq j_1$: this contradicts message uniqueness, since two different processes would include the same message in round $r_0$.
        \item If $j_0 = j_1$:
        \begin{align*}
            \Rightarrow & |{(j_0, \texttt{PROVE}(r_0)) \in proves}| \geq 2 & \text{(line 19)}\\
            \Rightarrow &\texttt{PROVE}_{j_0}(r_0) \text{ occurs 2 times} & \text{(line 6)}\\
            \Rightarrow &\texttt{AB-Broadcast}_{j_0}(m_0) \text{ were invoked two times} \\
            \Rightarrow &(max\{r: \exists j, (j, \texttt{PROVE}(r)) \in proves\} + 1) & \text{(line 4)}\\
            &\text{ returned the same value in two differents invokations of \texttt{AB-Broadcast}} \\
            &\textbf{But } \texttt{PROVE}(r_0) \Rightarrow \texttt{max}\{r: \exists j, (j, \texttt{PROVE}(r)) \in proves\} + 1 > r_0 \\
            &\text{It's impossible for a single process to submit two messages in the same round} \hspace{1em} \\
        \end{align*}
    \end{itemize}
    
    % \vspace{0.5em}
    \noindent\textbf{Case 2:} $r_0 \ne r_1$:
    \begin{itemize}
        \item If $j_0 \neq j_1$: again, message uniqueness prohibits two different processes from broadcasting the same message in different rounds.
        \item If $j_0 = j_1$: message uniqueness also prohibits the same process from broadcasting the same message in two different rounds.
    \end{itemize}
    
    In all cases, we reach a contradiction. Therefore, it is impossible for a process to deliver the same message more than once. $\square$
\end{proof}

% \subsubsection{No Duplication}

% $M = (\bigcup_{i \rightarrow |P|} AB\_receieved_{i}(m)), \not\exists m_0 m_1 \in M \text{s.t. } m_1 = m_2$
% \\
% Proof \\
% \begin{align*}
%     &\text{Soit } i, m_0, m_1 \text{ tels que } m_0 = m_1 \\
%     &\exists r_0,\ m_0 \in M^{r_0} \\
%     &\exists r_1,\ m_1 \in M^{r_1} \\
%     &\text{if } r_0 = r_1 \\
%     &\quad \exists j_0, j_1,\ \text{prop tq } \text{prop}[r_0][j_0] = m_0,\ \text{prop}[r_0][j_1] = m_1 \quad j_0, j_1 \in \text{winnner}^{r_0} \\
%     &\quad \text{if} j_0 \neq j_1 \\
%     &\quad\quad \text{On admet qu'il est impossible pour un processus de soumettre le même msg qu'un autre} \\
%     &\quad \text{if } j_0 = j_1 \\
%     &\quad\quad j_0 \text{ a émis son } \text{PROVE}(r_0) \text{ valide 2 fois}\\
%     &\quad\quad \text{Impossible si } j_0 \text{ correct} \\
%     &\text{else} \\
%     &\quad \exists j_0, j_1,\ \text{prop tq } \text{prop}[r_0][j_0] = m_0,\ \text{prop}[r_0][j_1] = m_1 \quad j_0, j_1 \in \text{winnner}^{r_0} \\
%     &\quad \text{if } j_0 \neq j_1 \\    
%     &\quad\quad \text{On admet qu'il est impossible pour un processus de soumettre le même msg qu'un autre} \\
%     &\quad \text{if } j_0 = j_1 \\
%     &j_0 \text{ à emis et validé 2 fois le même messages a des rounds différents.}\\
%     &\text{On admet que deux message identiques soumis a des rounds différents ne peuvent être identiques}
% \end{align*}

\subsubsection{Broadcast Validity}
$\exists j_0, m_0 \quad AB\_broadcast_{j_0}(m_0) \Rightarrow \forall j_1 \quad AB\_received_{j_1}(m_0)$ \\

Proof:
\begin{align*}
    &\exists j_0, m_0 \quad AB\_broadcast_{j_0}(m_0) \\
    &\forall j_1, \exists r_1 \quad RB\_deliver_{j_1}^{r_1}(m_0) \\
    &\exists receieved : m_0 \in receieved_{j_1} \\
    &\exists r_0 : RB\_deliver(PROP, r_0, m_0) & LOOP\\ 
    &\exists prop: \text{prop}[r_0][j_0] = m_0 \\
    &\text{if } \not\exists (j_0, PROVE(r_0)) \in \text{proves} \\
    &\quad r_0 += 1 \\
    &\quad \text{jump to LOOP} \\
    &\text{else} \\
    &\quad \exists \text{winner}, \text{winner}^{r_0} \ni j_0 \\
    &\quad \exists M^{r_0} \ni (\text{prop}[r_0][j_0] = m_0) \\
    &\quad \forall j_1, \quad AB\_deliver_{j_1}(m_0)
\end{align*}

\subsubsection*{AB receive width}
\[
\exists j_0, m_0 \quad AB\_deliver_{j_0}(m_0) \Rightarrow \forall j_1\ AB\_deliver_{j_1}
\]

Proof:
\begin{align*}
    &\forall j_0, m_0\ AB\_deliver_{j_0}(m_0) \Rightarrow \exists j_1 \text{ correct }, AB\_broadcast(m_0) \\
    &\exists j_0, m_0 \quad AB\_broadcast_{j_0}(m_0) \Rightarrow \forall j_1,\ AB\_deliver_{j_1}(m_0)
\end{align*}