\subsubsection{Model Properties}

The model is defined as Message-passing Aysnchronous. \\
There is n process. Each process is associated to a unique unforgeable id $i$.\\
Each process know the identity of all the process in the system\\
Each process have a reliable communication channel with all the others process such as:
\begin{itemize}
  \item send(m) is the send primitive
  \item recv(m) is the reception primitive
\end{itemize}
A message send is eventualy received\\
The system is Crash-Prone. There is at most f process who can crash such as f < n.\\


\subsubsection{AtomicBroadcast Properties}

\begin{theorem}{AB\_broadcast Validity}
  if a message is sent by a correct process, the message is eventually received by all the correct process. 
\end{theorem}

\begin{theorem}{AB\_receive Validity}
  if a message is received by a correct process, the message is eventually received by all the correct process. 
\end{theorem}

\begin{theorem}{AB\_receive safety No creation}
  if a message is received by a correct process, the message was emitted by a correct porcess. 
\end{theorem}

\begin{theorem}{AB\_receive safety No duplication}
  each message is received at most 1 time by each process. 
\end{theorem}

\begin{theorem}{AB\_receive safety Ordering}
  $\forall m_1, m_2$ two messages, $\forall p_i, p_j$ two process. \\
  if AB\_recv(m1) and AB\_recv(m2) for $p_i, p_j$ \\
  and AB\_recv(m1) is before AB\_recv(m2) for $p_i$ \\
  so AB\_recv(m1) is before AB\_recv(m2) for $p_j$ \\
\end{theorem}



\subsubsection{DenyList Properties}

\begin{theorem}{APPEND Validity}
  a APPEND(x) is valid iff the process p who sent the operation is such as $p \in \Pi_M$.
  And iff $x \in S$ where S is a set of valid values.
\end{theorem}

\begin{theorem}{PROVE Validity}
  a PROVE(x) is valid iff the process $p$ who sent the operation is such as $p \in \Pi_V$.
  And iff $\exists$ APPEND(x) who appears before PROVE(x) in Seq.
\end{theorem}

\begin{theorem}{PROGRESS}
  if an APPEND(x) is invoked, so there is a point in the linearization of the operations such as all PROVE(x) are valids.
\end{theorem}

\begin{theorem}{READ Validity}
  READ() return a list of tuples who is a random permutation of all valids PROVE() associated to the identity of the emiter process. 
\end{theorem}