diff --git a/Recherche/BFT-ARBover/6_BFT_ARB/index.tex b/Recherche/BFT-ARBover/6_BFT_ARB/index.tex
index 4cf662c..19a74a6 100644
--- a/Recherche/BFT-ARBover/6_BFT_ARB/index.tex
+++ b/Recherche/BFT-ARBover/6_BFT_ARB/index.tex
@@ -36,119 +36,128 @@ There are 3 operations : $\BFTPROVE(x), \BFTAPPEND(x), \BFTREAD(x)$ such that :
 
 \paragraph{Termination.} Every operation $\BFTAPPEND(x)$, $\BFTPROVE(x)$, and $\BFTREAD()$ invoked by a correct process always returns.
 
-\paragraph{APPEND Validity.} The invocation of $\BFTAPPEND(x)$ by a correct process $p_i$ is valid iff $i \in \Pi_M$. Otherwise the operation is invalid.
+% \paragraph{APPEND Validity.} The invocation of $\BFTAPPEND(x)$ by a correct process $p_i$ is valid iff $i \in \Pi_M$. Otherwise the operation is invalid.
 
-\paragraph{PROVE Validity.} If the invocation of a $op = \BFTPROVE(x)$ by a correct process $p$ is not valid, then:
-\begin{itemize}
-  \item $p \not\in \Pi_V$; \textbf{or}
-  \item At least $t+1$ valid $\BFTAPPEND(x)$ appears before $op$ in $\Seq$.
-\end{itemize}
-Otherwise, the operation is valid.
+\paragraph{PROVE Validity.} The invocation of $op = \BFTPROVE(x)$ by a correct process is valid iff there exist a set of correct process $C$ such that $\forall c \in C$, $c$ invoke $op_2 = \BFTAPPEND(x)$ with $op_2 \prec op_1$ and $|C| \leq t$
 
 \paragraph{PROVE Anti-Flickering.} If the invocation of a operation $op = \BFTPROVE(x)$ by a correct process $p \in \Pi_V$ is invalid, then any $\BFTPROVE(x)$ operation that appears after $op$ in $\Seq$ is invalid.
 
 \paragraph{READ Validity.} The invocation of $op = \BFTREAD()$ by a process $p$ returns the list of valid invocations of $\BFTPROVE$ that appears before $op$ in $\Seq$ along with the names of the processes that invoked each operation.
 
-\subsubsection{t-BFT-GE}
+\paragraph{Local consistency.} For all correct process $p_i$ such that $p_i$ invoke an valid $\BFTPROVE(x)$ before a $P \gets \BFTREAD()$ operation in his local execution. Then the set of valid $\BFTPROVE(x)$ in $P$ must contain the previous valid $\BFTPROVE(x)$.
 
-We consider a t-Byzantine Fault Tolerant Group Election Object (t-$\BFTGE[r]$) per round $r \in \mathcal{R}$ with the following properties.
+\paragraph{Liveness} For all correct process $p_i$ such that $p_i$ invoke an invalid $\BFTPROVE(x)$ before a $P \gets \BFTREAD()$ operation in his local execution. Then the set of valid $\BFTPROVE(x)$ in $P$ must be the same for any $p_i$.
 
-There are three operations: $\BFTVOTE(j, r)$, $\BFTCOMMIT(r)$, and $\BFTRESULT(r)$.
+% \subsubsection{t-BFT-GE}
 
-\paragraph{Termination.} Every operation $\BFTVOTE(i, r)$, $\BFTCOMMIT(r)$, and $\BFTRESULT(r)$ invoked by a correct process always returns.
+% We consider a t-Byzantine Fault Tolerant Group Election Object (t-$\BFTGE[r]$) per round $r \in \mathcal{R}$ with the following properties.
 
-\paragraph{Stability.} If there exist at least $n-f$ invocations of $\BFTCOMMIT(r)$ by distincts processes and let call $\BFTCOMMIT(r)^\star$ the $(n-f)^{th}$ such invocation in the linearization of $\Seq$. Then any invocation of $\BFTRESULT(r)$ that appears after $\BFTCOMMIT(r)^\star$ in $\Seq$ returns the same set of processes $W_r$.
+% There are three operations: $\BFTVOTE(j, r)$, $\BFTCOMMIT(r)$, and $\BFTRESULT(r)$.
 
-\paragraph{VOTE-Validity.} The invocation of $\BFTVOTE(j, r)$ by a correct process is not valid if $\BFTCOMMIT(r)^\star$ appears before in $\Seq$. Otherwise, the operation is valid.
+% \paragraph{Termination.} Every operation $\BFTVOTE(i, r)$, $\BFTCOMMIT(r)$, and $\BFTRESULT(r)$ invoked by a correct process always returns.
 
-\paragraph{Election.} If at least $f+1$ correct processes invoked a valid $\BFTVOTE(j, r)$ for the same process $j$ then $j$ will be enventually included in the set $W_r$ returned by $\BFTRESULT(r)$. 
+% \paragraph{Stability.} If there exist at least $n-f$ invocations of $\BFTCOMMIT(r)$ by distincts processes and let call $\BFTCOMMIT(r)^\star$ the $(n-f)^{th}$ such invocation in the linearization of $\Seq$. Then any invocation of $\BFTRESULT(r)$ that appears after $\BFTCOMMIT(r)^\star$ in $\Seq$ returns the same set of processes $W_r$.
+
+% \paragraph{VOTE-Validity.} The invocation of $\BFTVOTE(j, r)$ by a correct process is not valid if $\BFTCOMMIT(r)^\star$ appears before in $\Seq$. Otherwise, the operation is valid.
+
+% \paragraph{Election.} If at least $f+1$ correct processes invoked a valid $\BFTVOTE(j, r)$ for the same process $j$ then $j$ will be enventually included in the set $W_r$ returned by $\BFTRESULT(r)$. 
 
 \subsection{DL $\Rightarrow$ t-BFT-DL}
 
 \begin{lemma}
-    For any fixed value $t < |M|$, multiple DenyList Object can be used to implement a t-Byzantine Fault Tolerant DenyList Object.
+    For any fixed value $t$ such that $3t < |M|$, multiple DenyList Object can be used to implement a t-Byzantine Fault Tolerant DenyList Object.
 \end{lemma}
 
 \begin{proof}
-    Fix $t < |M|$. Let
+    Fix $3t < |M|$. Let
     \[
-    \mathcal{T} = \{\, T \subseteq M \mid |T| = t \,\}.
+    \mathcal{U} = \{\, U \subseteq M \mid |U| = |M| - t \,\}.
     \]
-    For each $T \in \mathcal{T}$, we instantiate one DenyList object $DL_T$ whose authorization sets are
+    For each $U \in \mathcal{U}$, we instantiate one DenyList object $DL_U$ whose authorization sets are
     \[
-    \Pi_M(DL_T) = S_T = M \setminus T
+    \Pi_M(DL_T) = S_T = U
     \qquad\text{and}\qquad
     \Pi_V(DL_T) = V.
     \]
     Let
     \[
-    K = \{\, DL_T \mid T \in \mathcal{T} \,\},
+    K = \{\, DL_U \mid U \in \mathcal{U} \,\},
     \qquad\text{so that}\qquad
-    |K| = \binom{|M|}{t}.
+    |U| = \binom{|M|}{|M| - t}.
     \]
 
-    \begin{algorithmic}
-        \State $K \gets \{DL_T : T \subseteq M, |T|=t\}$
+    \begin{algorithmic}[1]
+        % \State $K \gets \{DL_T : T \subseteq M, |T|=t\}$
 
-        \Function{BFTAPPEND}{x}
-            \If{$p_i \notin M$}
-                \State \Return \textbf{false}
-            \EndIf
-            \For{\textbf{each } $DL_T \in K$} 
-                \State $DL_T.\APPEND(x)$
-            \EndFor
-            \State \Return \textbf{true}
-        \EndFunction
+        \renewcommand{\algletter}{DL}
+        \begin{algorithm}[H]
+            \caption{\BFTAPPEND}
+            \Function{$\BFTAPPEND$}{x}
+                \For{\textbf{each } $DL_U \in K$ such that $p_i \in U$} 
+                \State $DL_U.\APPEND(x)$
+                \EndFor
+            \EndFunction
+        \end{algorithm}
         
-        \Function{BFTPROVE}{x}
-            \If{$p_i \notin V$}
-                \State \Return $\bot$
-            \EndIf
-            \State $state \gets false$
-            \For{\textbf{each } $DL_T \in K$}
-                \State $state \gets state \textbf{ OR } DL_T.\PROVE(x)$
-            \EndFor
-            \State \Return $state$
-        \EndFunction
+        % \renewcommand{\algletter}{B}    
+        \begin{algorithm}[H]
+            \caption{\BFTPROVE}
+            \Function{$\BFTPROVE$}{x}
+                \State $state \gets false$
+                \For{\textbf{each } $DL_U \in K$}
+                    \State $state \gets state \textbf{ OR } DL_U.\PROVE(x)$
+                \EndFor
+                \State \Return $state$
+            \EndFunction
+        \end{algorithm}
         
-        \Function{BFTREAD}{}
-            \State $results \gets \emptyset$
-            \For{\textbf{each } $DL_T \in K$}
-                \State $results \gets results \cup DL_T.\READ()$
-            \EndFor
-            \State \Return $results$
-        \EndFunction
+        % \renewcommand{\algletter}{C}  
+        \begin{algorithm}[H]
+            \caption{\BFTREAD}
+            \Function{$\BFTREAD$}{$\bot$}
+                \State $results \gets \emptyset$
+                \For{\textbf{each } $DL_U \in K$}
+                    \State $results \gets results \cup DL_U.\READ()$
+                \EndFor
+                \State \Return $results$
+            \EndFunction
+        \end{algorithm}
     \end{algorithmic}
         
-    \paragraph{BFT-APPEND Validity.} Let $A\subseteq M$ be the set of distinct issuers that invoked a valid $\BFTAPPEND(x)$ Suppose by contradiction that there exists $T\in\mathcal{T}$ with $A\cap S_T=\emptyset$. Since $S_T=M\setminus T$, this implies $A\subseteq T$, hence $|A|\le |T|=t$, contradicting $|A|\ge t+1$.
+    % \paragraph{BFT-APPEND Validity.} Let $A\subseteq M$ be the set of distinct issuers that invoked a valid $\BFTAPPEND(x)$ Suppose by contradiction that there exists $T\in\mathcal{T}$ with $A\cap S_T=\emptyset$. Since $S_T=M\setminus T$, this implies $A\subseteq T$, hence $|A|\le |T|=t$, contradicting $|A|\ge t+1$.
 
     \paragraph{BFT-PROVE Validity.} Let $op=\BFTPROVE(x)$ be an invocation by a correct process $p_i$. Let $A\subseteq M$ be the set of distinct issuers that invoked a valid $\BFTAPPEND(x)$ before $op$ in $\Seq$.
 
-    \smallskip
-    \noindent\textbf{Case (i): $i\notin V$.}
-    For every $T\in\mathcal{T}$, we configured $\Pi_V(DL_T)=V$, hence the induced operation $DL_T.\PROVE(x)$ is invalid by \textbf{PROVE Validity} of $\DL$. Therefore $op$ is invalid.
-
-    \smallskip
-    \noindent\textbf{Case (ii): $|A|\ge t+1$ and $i\in V$.} Fix any $T\in\mathcal{T}$. By BFT-APPEND Validity, $A\cap S_T\neq\emptyset$. Pick $j\in A\cap S_T$. Since $j\in S_T$, the call $\BFTAPPEND^{(j)}(x)$ triggers $DL_T.\APPEND(x)$, and because $\BFTAPPEND^{(j)}(x)\prec op$ in $\Seq$, this induces a valid $DL_T.\APPEND(x)$ that appears before the induced $DL_T.\PROVE(x)$. By \textbf{PROVE Validity} of $\DL$, the induced $DL_T.\PROVE(x)$ is invalid. As this holds for every $T\in\mathcal{T}$, there is \emph{no} component $DL_T$ where $\PROVE(x)$ is valid, so $op$ is invalid.
-
-    \smallskip
-    \noindent\textbf{Case (iii): $|A|\le t$ and $i\in V$.}
-    By BFT-APPEND Validity, there exists $T^\star\in\mathcal{T}$ such that $A\cap S_{T^\star}=\emptyset$, i.e., $A\subseteq T^\star$. For any $j\in A$, we have $j\notin S_{T^\star}$, so $\BFTAPPEND^{(j)}(x)$ does \emph{not} call $DL_{T^\star}.\APPEND(x)$. Hence no valid $DL_{T^\star}.\APPEND(x)$ appears before the induced $DL_{T^\star}.\PROVE(x)$. Since also $i\in V=\Pi_V(DL_{T^\star})$, by \textbf{PROVE Validity} of $\DL$ the induced $DL_{T^\star}.\PROVE(x)$ is valid. Therefore, there exists a component with a valid $\PROVE(x)$, so by the lifting convention $op$ is valid.
-
+    \begin{itemize}
+        % \item \textbf{Case (i): $i\notin V$.}
+        % For every $T\in\mathcal{T}$, we configured $\Pi_V(DL_T)=V$, hence the induced operation $DL_T.\PROVE(x)$ is invalid by \textbf{PROVE Validity} of $\DL$. Therefore $op$ is invalid.
+        
+        \item \textbf{Case (i): $|A|\ge t+1$.} 
+        Fix any $U\in\mathcal{U}$. $A\cap U\neq\emptyset$. Pick $j\in A\cap U$. Since $j\in u$, the call $\BFTAPPEND^{(j)}(x)$ triggers $DL_U.\APPEND(x)$, and because $\BFTAPPEND^{(j)}(x)\prec op$ in $\Seq$, this induces a valid $DL_U.\APPEND(x)$ that appears before the induced $DL_U.\PROVE(x)$. By \textbf{PROVE Validity} of $\DL$, the induced $DL_U.\PROVE(x)$ is invalid. As this holds for every $T\in\mathcal{T}$, there is \emph{no} component $DL_U$ where $\PROVE(x)$ is valid, so $op$ is invalid.
+        
+        \item \textbf{Case (ii): $|A|\le t$.}
+        Fix any $U\in\mathcal{U}$, there exists $U^\star\in\mathcal{U}$ such that $A\cap U^\star=\emptyset$. For any $j\in A$, we have $j\notin U^\star$, so $\BFTAPPEND^{(j)}(x)$ does \emph{not} call $DL_{U^\star}.\APPEND(x)$. Hence no valid $DL_{U^\star}.\APPEND(x)$ appears before the induced $DL_{U^\star}.\PROVE(x)$. Since also $i\in V=\Pi_V(DL_{U^\star})$, by \textbf{PROVE Validity} of $\DL$ the induced $DL_{U^\star}.\PROVE(x)$ is valid. Therefore, there exists a component with a valid $\PROVE(x)$, so by the lifting convention $op$ is valid.
+    \end{itemize}
+        
     \smallskip
     Combining the cases yields the claimed characterization of invalidity.
 
     \paragraph{BFT-PROVE Anti-Flickering.} Let $op=\BFTPROVE(x)$ be an invocation by a correct process $p_i\in V$ that is \emph{invalid} in $\Seq$.
-    By BFT-PROVE Validity, since $i\in V$, this implies that there exist at least $t+1$ \emph{distinct} processes in $M$ that invoked a \emph{valid} $\BFTAPPEND(x)$ before $op$ in $\Seq$. Let $A\subseteq M$ denote that set, with $|A|\ge t+1$.
+    By BFT-PROVE Validity, this implies that there exist at least $t+1$ \emph{distinct} processes in $M$ that invoked a \emph{valid} $\BFTAPPEND(x)$ before $op$ in $\Seq$. Let $A\subseteq M$ denote that set, with $|A|\ge t+1$.
 
-    Fix any $T\in\mathcal{T}$ and $DL_T$ with $\Pi_M(DL_T)=S_T=M\setminus T$. By BFT-APPEND Validity, we have $A\cap S_T\neq\emptyset$. Pick $j\in A\cap S_T$. Since $j\in S_T$, the call $\BFTAPPEND^{(j)}(x)$ triggers a call $DL_T.\APPEND(x)$. Moreover, because $\BFTAPPEND^{(j)}(x)\prec op$ in $\Seq$, the induced $DL_T.\APPEND(x)$ appears before the induced $DL_T.\PROVE(x)$ of $op$ in the projection $\Seq_T$.
+    Fix any $U\in\mathcal{U}$. We have $A\cap U\neq\emptyset$. Pick $j\in A\cap U$. Since $j\in U$, the call $\BFTAPPEND^{(j)}(x)$ triggers a call $DL_U.\APPEND(x)$. Moreover, because $\BFTAPPEND^{(j)}(x)\prec op$ in $\Seq$, the induced $DL_U.\APPEND(x)$ appears before the induced $DL_U.\PROVE(x)$ of $op$ in the projection $\Seq_U$.
 
-    Hence, in $\Seq_T$, there exists a \emph{valid} $DL_T.\APPEND(x)$ that appears before the $DL_T.\PROVE(x)$ induced by $op$. By \textbf{PROVE Validity} the base $\DL$ object, the induced $DL_T.\PROVE(x)$ is therefore \emph{invalid} in $\Seq_T$.
+    Hence, in $\Seq_U$, there exists a \emph{valid} $DL_U.\APPEND(x)$ that appears before the $DL_U.\PROVE(x)$ induced by $op$. By \textbf{PROVE Validity} the base $\DL$ object, the induced $DL_U.\PROVE(x)$ is therefore \emph{invalid} in $\Seq_U$.
 
-    Now let $op'=\BFTPROVE(x)$ be any invocation such that $op\prec op'$ in $\Seq$. Fix again any $T\in\mathcal{T}$. Hence, the $DL_T.\PROVE(x)$ induced by $op'$ appears after the $DL_T.\PROVE(x)$ induced by $op$ in $\Seq_T$. Since the induced $DL_T.\PROVE(x)$ of $op$ is invalid, by \textbf{PROVE Anti-Flickering} of $\DL$, \emph{every} subsequent $DL_T.\PROVE(x)$ in $\Seq_T$ is invalid.
+    Now let $op'=\BFTPROVE(x)$ be any invocation such that $op\prec op'$ in $\Seq$. Fix again any $U\in\mathcal{U}$. Hence, the $DL_U.\PROVE(x)$ induced by $op'$ appears after the $DL_U.\PROVE(x)$ induced by $op$ in $\Seq_U$. Since the induced $DL_U.\PROVE(x)$ of $op$ is invalid, by \textbf{PROVE Anti-Flickering} of $\DL$, \emph{every} subsequent $DL_U.\PROVE(x)$ in $\Seq_U$ is invalid.
 
-    As this holds for every $T\in\mathcal{T}$, there is no component $DL_T$ in which the induced $\PROVE(x)$ of $op'$ is valid.
+    As this holds for every $U\in\mathcal{U}$, there is no component $DL_U$ in which the induced $\PROVE(x)$ of $op'$ is valid.
     
+
+    \paragraph{Local consistency.}
+    
+    \paragraph{Liveness.}
+
 \end{proof}
 
 
diff --git a/Recherche/BFT-ARBover/main.pdf b/Recherche/BFT-ARBover/main.pdf
index 14f5972..77479a8 100644
Binary files a/Recherche/BFT-ARBover/main.pdf and b/Recherche/BFT-ARBover/main.pdf differ