amaury_joly/bwconsistency
1
0
Fork 0
Code Issues 5 Pull Requests Packages Projects 3 Releases Wiki Activity

intro et algo propre. Proof en cours

Browse Source
This commit is contained in:
Amaury JOLY 2025-05-15 11:48:32 +00:00
parent 2c04ad710e
commit d81a1e232a
10 changed files with 687 additions and 392 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

121
recherches/ALDLoverAB/algo/index.tex
View File

@ -1,73 +1,60 @@
We define $k$ as the id of the round \\ We consider a set of processes communicating asynchronously over reliable point-to-point channels. Each process maintains the following shared variables:
the $getMax(proves)$ return $MAX({(\_, r) : \exists (\_, PROVE(r)) \in proves})$ \\
$buffer$ a FIFO list with $buffer[front]$ returning the first element
\begin{itemize}
\item \textbf{received}: the set of messages received (but not yet delivered).
\item \textbf{delivered}: the set of messages that have been received, ordered, and delivered.
\item \textbf{prop[$r$][$j$]}: the proposal set of process $j$ at round $r$. It contains the set of messages that process $j$ claims to have received but not yet delivered at round $r$, concatenated with its newly broadcast message.
\item \textbf{proves}: the current content of the \texttt{DenyList} registry, accessible via the operation \texttt{READ()}. It returns a list of tuples $(j, \texttt{PROVE}(r))$, each indicating that process $j$ has issued a valid \texttt{PROVE} for round $r$.
\item \textbf{winner$^r$}: the set of processes that have issued a valid \texttt{PROVE} operation for round $r$.
\item \textbf{RB-cast}: a reliable broadcast primitive that satisfies the properties defined in Section~1.1.2.
\item \textbf{APPEND$(r)$}, \textbf{PROVE$(r)$}: operations that respectively insert (APPEND) and attest (PROVE) the participation of a process in round $r$ in the DenyList registry.
\item \textbf{READ()}: retrieves the current local view of valid operations (APPENDs and PROVEs) from the DenyList.
\item \textbf{ordered$(S)$}: returns a deterministic total order over a set $S$ of messages (e.g., via hash or lexicographic order).
\end{itemize}
\begin{algorithm}[H] \resetalgline
\DontPrintSemicolon \begin{algorithm}
\SetAlgoLined
$rcved = rcved \bigcup \{m\}$ \; \vspace{1em}
\textbf{upon} RB\_deliver(PROP, r, S) \textbf{from} j \; \textbf{RB-received$(m, S, r_0, j_0)$}
prop[r][j] = S \begin{algorithmic}[1]
\State \nextalgline $\textit{received} \gets \textit{received} \cup \{m\}$
\State \nextalgline $\textit{prop}[r_0][j_0] \gets S$
\end{algorithmic}
\caption{\textbf{Upon} RB\_deliver(m)} \vspace{1em}
\end{algorithm} \textbf{AB-broadcast$(m, j_0)$}
\begin{algorithmic}[1]
\State \nextalgline $\textit{proves} \gets \texttt{READ}()$
\State \nextalgline $r_0 \gets \max\{r : \exists j,\ (j, \texttt{PROVE}(r)) \in \textit{proves}\} + 1$
\State \nextalgline $\texttt{RB-cast}(m, (\textit{received} \setminus \textit{delivered}) \cup \{m\}, r_0, j_0)$
\State \nextalgline \texttt{PROVE}$(r_0)$
\State \nextalgline \texttt{APPEND}$(r_0)$
\Repeat
\State \nextalgline $\textit{proves} \gets \texttt{READ}()$
\State \nextalgline $r_1 \gets \max\{r : \exists j,\ (j, \texttt{PROVE}(r)) \in \textit{proves}\} - 1$
\State \nextalgline $\textit{winner}^{r_1} \gets \{j : (j, \texttt{PROVE}(r_1)) \in \textit{proves}\}$
\State \nextalgline \textbf{wait} $\forall j \in \textit{winner}^{r_1},\ \textit{prop}[r_1][j] \neq \bot$
\Until{\nextalgline $\forall r_2,\ \exists j_2 \in \textit{winner}^{r_2},\ m \in \textit{prop}[r_2][j_2]$} \nextalgline
\end{algorithmic}
\begin{algorithm}[H] \vspace{1em}
\DontPrintSemicolon \textbf{AB-listen}
\SetAlgoLined \begin{algorithmic}[1]
\KwIn{le message $m$} \While{true}
\State \nextalgline $\textit{proves} \gets \texttt{READ}()$
\KwData{rcved = $\emptyset$ \; \State \nextalgline $r_1 \gets \max\{r : \exists j,\ (j, \texttt{PROVE}(r)) \in \textit{proves}\} - 1$
delivered = $\emptyset$ \; \For{$r_2 \in [r_0, \dots, r_1]$} \nextalgline
r = 0 \;} \State \nextalgline \texttt{APPEND}$(r_2)$
\State \nextalgline $\textit{proves} \gets \texttt{READ}()$
\BlankLine \State \nextalgline $\textit{winner}^{r_2} \gets \{j : (i, \texttt{PROVE}(r_2)) \in \textit{proves}\}$
\State \nextalgline \textbf{wait} $\forall j \in \textit{winner}^{r_2},\ \textit{prop}[r_2][j] \neq \bot$
RB\_cast(m) \; \State \nextalgline $M^{r_2} \gets \bigcup_{j \in \textit{winner}^{r_2}} \textit{prop}[r_2][j]$
$rcved = rcvd \bigcup \{m\}$ \; \ForAll{$m \in \texttt{ordered}(M^{r_2})$} \nextalgline
\State \nextalgline $\textit{delivered} \gets \textit{delivered} \cup \{m\}$
\While{true}{ \State \nextalgline \texttt{AB-deliver}$(m)$
$r = r+1$ \; \EndFor
$RB\_cast(PROP, r, S)$ \; \EndFor
PROVE(r) \; \EndWhile
APPEND(r) \; \end{algorithmic}
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} \end{algorithm}

108
recherches/ALDLoverAB/intro/index.tex
View File

@ -1,61 +1,77 @@
\subsubsection{Model Properties} \subsubsection{Model Properties}
The model is defined as Message-passing Aysnchronous. \\ The system consists of \textit{n} asynchronous processes communicating via reliable point-to-point message passing. \\
There is n process. Each process is associated to a unique unforgeable id $i$.\\ Each process has a unique, unforgeable identifier and knows the identifiers of all other processes. \\
Each process know the identity of all the process in the system\\ Up to $f<n$ processes may crash (fail-stop). \\
Each process have a reliable communication channel with all the others process such as: The network is reliable: if a correct process sends a message to another correct process, it is eventually delivered. \\
\begin{itemize} Messages are uniquely identifiable: two messages sent by distinct processes or at different rounds are distinguishable \\
\item send(m) is the send primitive 2 messages sent by the same processus in two differents rounds are differents \\
\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.\\
\begin{property}[Message Uniqueness]
If two messages are sent by different processes, or by the same process in different rounds, then the messages are distinct. \\
Formally : \\
\[
\forall p_1, p_2,\ \forall r_1, r_2,\ \forall m_1, m_2,\
\left(
\begin{array}{l}
\text{send}(p_1, r_1, m_1) \land \text{send}(p_2, r_2, m_2) \\
\land\ (p_1 \ne p_2 \lor r_1 \ne r_2)
\end{array}
\right)
\Rightarrow m_1 \ne m_2
\]
\end{property}
\subsubsection{Reliable Broadcast Properties}
\begin{property}{Integrity}
Every message received was previously sent. \\
Formally : \\
$\forall p_i : \text{bc-recv}_i(m) \Rightarrow \exists p_j : \text{bc-send}_j(m)$
\end{property}
\begin{property}{No Duplicates}
No message is received more than once at any single processor. \\
Formally : \\
$\forall m, \forall p_i: \text{bc-recv}_i(m) \text{ occurs at most once}$ \\
\end{property}
\begin{property}{Validity}
All messages broadcast by a correct process are eventually received by all non faulty processors. \\
Formally : \\
$\forall m, \forall p_i: \text{correct}(p_i) \wedge \text{bc-send}_i(m) => \forall p_j : \text{correct}(p_j) \Rightarrow \text{bc-recv}_j(m)$
\end{property}
\subsubsection{AtomicBroadcast Properties} \subsubsection{AtomicBroadcast Properties}
\begin{theorem}{AB\_broadcast Validity} \begin{property}{AB Totally ordered}
if a message is sent by a correct process, the message is eventually received by all the correct process. $\forall m_1, m_2, \forall p_i, p_j : \text{ab-recv}_{p_i}(m_1) < \text{ab-recv}_{p_i}(m_2) \Rightarrow \text{ab-recv}_{p_j}(m_1) < \text{ab-recv}_{p_j}(m_2)$
\end{theorem} \end{property}
\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} \subsubsection{DenyList Properties}
\begin{theorem}{APPEND Validity} Let $\Pi_M$ be the set of processes authorized to issue \texttt{APPEND} operations,
a APPEND(x) is valid iff the process p who sent the operation is such as $p \in \Pi_M$. and $\Pi_V$ the set of processes authorized to issue \texttt{PROVE} operations. \\
And iff $x \in S$ where S is a set of valid values. Let $S$ be the set of valid values that may be appended. Let $\texttt{Seq}$ be
\end{theorem} the linearization of operations recorded in the DenyList.
\begin{theorem}{PROVE Validity} \begin{property}{APPEND Validity}
a PROVE(x) is valid iff the process $p$ who sent the operation is such as $p \in \Pi_V$. An operation $\texttt{APPEND}(x)$ is valid iff :
And iff $\exists$ APPEND(x) who appears before PROVE(x) in Seq. the issuing process $p \in \Pi_M$, and the value $x \in S$
\end{theorem} \end{property}
\begin{theorem}{PROGRESS} \begin{property}{PROVE Validity}
if an APPEND(x) is invoked, so there is a point in the linearization of the operations such as all PROVE(x) are valids. An operation $\texttt{PROVE}(x)$ is valid iff:
\end{theorem} the issuing process $p \in \Pi_V$, and there exists no $\texttt{APPEND}(x)$ that appears earlier in $\texttt{Seq}$.
\end{property}
\begin{theorem}{READ Validity} \begin{property}{PROGRESS}
If an APPEND(x) is invoked by a correct process, then all correct processes will eventually be unable to PROVE(x).
\end{property}
\begin{property}{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. 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} \end{property}

15
recherches/ALDLoverAB/main.aux
View File

@ -6,16 +6,15 @@
\catcode `!\active \catcode `!\active
\catcode `?\active \catcode `?\active
\abx@aux@refcontext{nty/global//global/global/global} \abx@aux@refcontext{nty/global//global/global/global}
\providecommand \oddpage@label [2]{}
\babel@aux{french}{} \babel@aux{french}{}
\@writefile{toc}{\contentsline {section}{\numberline {1}Introduction}{1}{}\protected@file@percent } \@writefile{toc}{\contentsline {section}{\numberline {1}Introduction}{1}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {1.1}Model}{1}{}\protected@file@percent } \@writefile{toc}{\contentsline {subsection}{\numberline {1.1}Model}{1}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsubsection}{\numberline {1.1.1}Model Properties}{1}{}\protected@file@percent } \@writefile{toc}{\contentsline {subsubsection}{\numberline {1.1.1}Model Properties}{1}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsubsection}{\numberline {1.1.2}AtomicBroadcast Properties}{1}{}\protected@file@percent } \@writefile{toc}{\contentsline {subsubsection}{\numberline {1.1.2}Reliable Broadcast Properties}{1}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsubsection}{\numberline {1.1.3}DenyList Properties}{1}{}\protected@file@percent } \@writefile{toc}{\contentsline {subsubsection}{\numberline {1.1.3}AtomicBroadcast Properties}{1}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {1.2}Algorithms}{1}{}\protected@file@percent } \@writefile{toc}{\contentsline {subsubsection}{\numberline {1.1.4}DenyList Properties}{1}{}\protected@file@percent }
\@writefile{loa}{\contentsline {algocf}{\numberline {1}{\ignorespaces \textbf {Upon} RB\_deliver(m)}}{2}{}\protected@file@percent } \@writefile{toc}{\contentsline {subsection}{\numberline {1.2}Algorithms}{2}{}\protected@file@percent }
\@writefile{loa}{\contentsline {algocf}{\numberline {2}{\ignorespaces AB\_Broadcast}}{2}{}\protected@file@percent } \@writefile{toc}{\contentsline {subsection}{\numberline {1.3}proof}{2}{}\protected@file@percent }
\@writefile{loa}{\contentsline {algocf}{\numberline {3}{\ignorespaces AB\_Listen}}{2}{}\protected@file@percent } \@writefile{toc}{\contentsline {subsubsection}{\numberline {1.3.1}Broadcast Validity}{4}{}\protected@file@percent }
\abx@aux@read@bbl@mdfivesum{76D65A242EC496C9B4361AF646FF12CB} \abx@aux@read@bbl@mdfivesum{76D65A242EC496C9B4361AF646FF12CB}
\gdef \@abspage@last{3} \gdef \@abspage@last{6}

60
recherches/ALDLoverAB/main.fdb_latexmk
View File

@ -1,42 +1,60 @@
# Fdb version 4 # Fdb version 4
["biber main"] 0 "main.bcf" "main.bbl" "main" 1746172816.43057 -1 ["biber main"] 0 "main.bcf" "main.bbl" "main" 1747309539.09877 -1
"main.bcf" 1746172816.38112 108486 d8549f9e7d9f09af6a94b466d27b9f55 "pdflatex" "main.bcf" 1747309539.00575 108486 d8549f9e7d9f09af6a94b466d27b9f55 "pdflatex"
"sources.bib" 1745505510 0 d41d8cd98f00b204e9800998ecf8427e "" "sources.bib" 1745505510 0 d41d8cd98f00b204e9800998ecf8427e ""
(generated) (generated)
"main.bbl" "main.bbl"
"main.blg" "main.blg"
(rewritten before read) (rewritten before read)
["pdflatex"] 1746172815.97294 "/workspaces/containers/recherches/ALDLoverAB/main.tex" "main.pdf" "main" 1746172816.431 0 ["pdflatex"] 1747309538.15653 "/workspaces/containers/recherches/ALDLoverAB/main.tex" "main.pdf" "main" 1747309539.09917 0
"/usr/local/texlive/2025/texmf-dist/fonts/enc/dvips/cm-super/cm-super-t1.enc" 1136849721 2971 def0b6c1f0b107b3b936def894055589 "" "/usr/local/texlive/2025/texmf-dist/fonts/enc/dvips/cm-super/cm-super-t1.enc" 1136849721 2971 def0b6c1f0b107b3b936def894055589 ""
"/usr/local/texlive/2025/texmf-dist/fonts/map/fontname/texfonts.map" 1577235249 3524 cb3e574dea2d1052e39280babc910dc8 "" "/usr/local/texlive/2025/texmf-dist/fonts/map/fontname/texfonts.map" 1577235249 3524 cb3e574dea2d1052e39280babc910dc8 ""
"/usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecbi0500.tfm" 1136768653 3072 5c02773c2e93e883bb03697d9281a6c7 ""
"/usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecbi0700.tfm" 1136768653 3072 d954c3b8c413504af8820bec51a4b82c ""
"/usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecbi1000.tfm" 1136768653 3072 e6fe53b666f9cbd66cb135c6fdea66d3 "" "/usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecbi1000.tfm" 1136768653 3072 e6fe53b666f9cbd66cb135c6fdea66d3 ""
"/usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecbx0700.tfm" 1136768653 3584 ca0c423beaacd28d53ddce5a826cd558 ""
"/usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecbx1000.tfm" 1136768653 3584 2d666ecf6d466d8b007246bc2f94d9da "" "/usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecbx1000.tfm" 1136768653 3584 2d666ecf6d466d8b007246bc2f94d9da ""
"/usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecbx1200.tfm" 1136768653 3584 402da0b29eafbad07963b1224b222f18 "" "/usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecbx1200.tfm" 1136768653 3584 402da0b29eafbad07963b1224b222f18 ""
"/usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecbx1440.tfm" 1136768653 3584 13049b61b922a28b158a38aeff75ee9b "" "/usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecbx1440.tfm" 1136768653 3584 13049b61b922a28b158a38aeff75ee9b ""
"/usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecit0800.tfm" 1136768653 1536 09682d3e827df9145fea3c41a21d8b01 ""
"/usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecit1000.tfm" 1136768653 1536 34ad639b0caa1b405dc14b9703b4e5b9 ""
"/usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecrm0500.tfm" 1136768653 3584 178baad7ffca7f5d3428a83bd7cc64c3 ""
"/usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecrm0700.tfm" 1136768653 3584 cf973739aac7ab6247f9150296af7954 ""
"/usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecrm1000.tfm" 1136768653 3584 adb004a0c8e7c46ee66cad73671f37b4 "" "/usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecrm1000.tfm" 1136768653 3584 adb004a0c8e7c46ee66cad73671f37b4 ""
"/usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecrm1200.tfm" 1136768653 3584 f80ddd985bd00e29e9a6047ebd9d4781 "" "/usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecrm1200.tfm" 1136768653 3584 f80ddd985bd00e29e9a6047ebd9d4781 ""
"/usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecrm1440.tfm" 1136768653 3584 3169d30142b88a27d4ab0e3468e963a2 "" "/usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecrm1440.tfm" 1136768653 3584 3169d30142b88a27d4ab0e3468e963a2 ""
"/usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecrm1728.tfm" 1136768653 3584 3c76ccb63eda935a68ba65ba9da29f1a "" "/usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecrm1728.tfm" 1136768653 3584 3c76ccb63eda935a68ba65ba9da29f1a ""
"/usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecti0500.tfm" 1136768653 3072 3d6a4805e3f8c4693f997dc6a16a6b93 ""
"/usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecti0700.tfm" 1136768653 3072 b90b057319ce008920857c32d19eeb4d ""
"/usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecti1000.tfm" 1136768653 3072 3bce340d4c075dffe6d4ec732b4c32fe "" "/usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecti1000.tfm" 1136768653 3072 3bce340d4c075dffe6d4ec732b4c32fe ""
"/usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecti1200.tfm" 1136768653 3072 8b5a64dc91775463bc95e2d818524028 "" "/usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecti1200.tfm" 1136768653 3072 8b5a64dc91775463bc95e2d818524028 ""
"/usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ectt0800.tfm" 1136768653 1536 0b0b8ca286de6a006b681926403f35cd ""
"/usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ectt1000.tfm" 1136768653 1536 06717a2b50de47d4087ac0e6cd759455 "" "/usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ectt1000.tfm" 1136768653 1536 06717a2b50de47d4087ac0e6cd759455 ""
"/usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/cmextra/cmex7.tfm" 1246382020 1004 54797486969f23fa377b128694d548df ""
"/usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam10.tfm" 1246382020 916 f87d7c45f9c908e672703b83b72241a3 ""
"/usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam5.tfm" 1246382020 924 9904cf1d39e9767e7a3622f2a125a565 ""
"/usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam7.tfm" 1246382020 928 2dc8d444221b7a635bb58038579b861a ""
"/usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm10.tfm" 1246382020 908 2921f8a10601f252058503cc6570e581 ""
"/usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm5.tfm" 1246382020 940 75ac932a52f80982a9f8ea75d03a34cf ""
"/usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm7.tfm" 1246382020 940 228d6584342e91276bf566bcf9716b83 ""
"/usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmex10.pfb" 1248133631 30251 6afa5cb1d0204815a708a080681d4674 "" "/usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmex10.pfb" 1248133631 30251 6afa5cb1d0204815a708a080681d4674 ""
"/usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb" 1248133631 36299 5f9df58c2139e7edcf37c8fca4bd384d "" "/usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb" 1248133631 36299 5f9df58c2139e7edcf37c8fca4bd384d ""
"/usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi5.pfb" 1248133631 37912 77d683123f92148345f3fc36a38d9ab1 "" "/usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi5.pfb" 1248133631 37912 77d683123f92148345f3fc36a38d9ab1 ""
"/usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi7.pfb" 1248133631 36281 c355509802a035cadc5f15869451dcee "" "/usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi7.pfb" 1248133631 36281 c355509802a035cadc5f15869451dcee ""
"/usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb" 1248133631 35752 024fb6c41858982481f6968b5fc26508 "" "/usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb" 1248133631 35752 024fb6c41858982481f6968b5fc26508 ""
"/usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmr5.pfb" 1248133631 31809 8670ca339bf94e56da1fc21c80635e2a ""
"/usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmr7.pfb" 1248133631 32762 224316ccc9ad3ca0423a14971cfa7fc1 "" "/usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmr7.pfb" 1248133631 32762 224316ccc9ad3ca0423a14971cfa7fc1 ""
"/usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb" 1248133631 32569 5e5ddc8df908dea60932f3c484a54c0d "" "/usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb" 1248133631 32569 5e5ddc8df908dea60932f3c484a54c0d ""
"/usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy7.pfb" 1248133631 32716 08e384dc442464e7285e891af9f45947 "" "/usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy7.pfb" 1248133631 32716 08e384dc442464e7285e891af9f45947 ""
"/usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/symbols/msam10.pfb" 1248133631 31764 459c573c03a4949a528c2cc7f557e217 ""
"/usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfbi1000.pfb" 1215737283 193571 dce9a978093738902238b3e227edef6c "" "/usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfbi1000.pfb" 1215737283 193571 dce9a978093738902238b3e227edef6c ""
"/usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfbx0700.pfb" 1215737283 144215 c89c56d5c5b828c5c1657b4326c29df7 ""
"/usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfbx1000.pfb" 1215737283 145408 43d44302ca7d82d487f511f83e309505 "" "/usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfbx1000.pfb" 1215737283 145408 43d44302ca7d82d487f511f83e309505 ""
"/usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfbx1200.pfb" 1215737283 140176 d4962f948b4cc0adf4d3dde77a128c95 "" "/usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfbx1200.pfb" 1215737283 140176 d4962f948b4cc0adf4d3dde77a128c95 ""
"/usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfbx1440.pfb" 1215737283 135942 859a90cad7494a1e79c94baf546d7de5 "" "/usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfbx1440.pfb" 1215737283 135942 859a90cad7494a1e79c94baf546d7de5 ""
"/usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfit1000.pfb" 1215737283 157419 ef2add7d886ed65124e72477bd51c8f4 ""
"/usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfrm1000.pfb" 1215737283 138258 6525c253f16cededa14c7fd0da7f67b2 "" "/usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfrm1000.pfb" 1215737283 138258 6525c253f16cededa14c7fd0da7f67b2 ""
"/usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfrm1200.pfb" 1215737283 136101 f533469f523533d38317ab5729d00c8a "" "/usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfrm1200.pfb" 1215737283 136101 f533469f523533d38317ab5729d00c8a ""
"/usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfrm1728.pfb" 1215737283 131438 3aa300b3e40e5c8ba7b4e5c6cebc5dd6 "" "/usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfrm1728.pfb" 1215737283 131438 3aa300b3e40e5c8ba7b4e5c6cebc5dd6 ""
"/usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfti0700.pfb" 1215737283 184338 71ec80cd6b45d5405da0f23c65ebdef8 ""
"/usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfti1000.pfb" 1215737283 186554 e8f0fa8ca05e038f257a06405232745f "" "/usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfti1000.pfb" 1215737283 186554 e8f0fa8ca05e038f257a06405232745f ""
"/usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfti1200.pfb" 1215737283 198221 ca5aa71411090ef358a6cc78b7458365 "" "/usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfti1200.pfb" 1215737283 198221 ca5aa71411090ef358a6cc78b7458365 ""
"/usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sftt1000.pfb" 1215737283 169201 9ebf99020dde51a5086e186761a34e8f "" "/usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sftt1000.pfb" 1215737283 169201 9ebf99020dde51a5086e186761a34e8f ""
@ -49,7 +67,18 @@
"/usr/local/texlive/2025/texmf-dist/tex/generic/infwarerr/infwarerr.sty" 1575499628 8356 7bbb2c2373aa810be568c29e333da8ed "" "/usr/local/texlive/2025/texmf-dist/tex/generic/infwarerr/infwarerr.sty" 1575499628 8356 7bbb2c2373aa810be568c29e333da8ed ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/ltxcmds/ltxcmds.sty" 1701727651 17865 1a9bd36b4f98178fa551aca822290953 "" "/usr/local/texlive/2025/texmf-dist/tex/generic/ltxcmds/ltxcmds.sty" 1701727651 17865 1a9bd36b4f98178fa551aca822290953 ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pdftexcmds/pdftexcmds.sty" 1593379760 20089 80423eac55aa175305d35b49e04fe23b "" "/usr/local/texlive/2025/texmf-dist/tex/generic/pdftexcmds/pdftexcmds.sty" 1593379760 20089 80423eac55aa175305d35b49e04fe23b ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/algorithm2e/algorithm2e.sty" 1500498588 167160 d91cee26d3ef5727644d2110445741dd "" "/usr/local/texlive/2025/texmf-dist/tex/latex/algorithmicx/algorithmicx.sty" 1160617237 26750 ce139c05a983e19ddca355b43e29c395 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/algorithmicx/algpseudocode.sty" 1160617237 3457 d9077efe6b74c5a094199256af8d7d9a ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/algorithms/algorithm.sty" 1251330371 3249 15763257e50278eef5db1952ccde229c ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/amsfonts/amsfonts.sty" 1359763108 5949 3f3fd50a8cc94c3d4cbf4fc66cd3df1c ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/amsfonts/amssymb.sty" 1359763108 13829 94730e64147574077f8ecfea9bb69af4 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/amsfonts/umsa.fd" 1359763108 961 6518c6525a34feb5e8250ffa91731cff ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/amsfonts/umsb.fd" 1359763108 961 d02606146ba5601b5645f987c92e6193 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amsbsy.sty" 1717359999 2222 2166a1f7827be30ddc30434e5efcee1b ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amsgen.sty" 1717359999 4173 d22509bc0c91281d991b2de7c88720dd ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amsmath.sty" 1730928152 88370 c780f23aea0ece6add91e09b44dca2cd ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amsopn.sty" 1717359999 4474 23ca1d3a79a57b405388059456d0a8df ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amstext.sty" 1717359999 2444 71618ea5f2377e33b04fb97afdd0eac2 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/base/article.cls" 1738182759 20144 63d8bacaf52e5abf4db3bc322373e1d4 "" "/usr/local/texlive/2025/texmf-dist/tex/latex/base/article.cls" 1738182759 20144 63d8bacaf52e5abf4db3bc322373e1d4 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/base/fontenc.sty" 1738182759 5275 0d62fb62162c7ab056e941ef18c5076d "" "/usr/local/texlive/2025/texmf-dist/tex/latex/base/fontenc.sty" 1738182759 5275 0d62fb62162c7ab056e941ef18c5076d ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/base/ifthen.sty" 1738182759 5525 9dced5929f36b19fa837947f5175b331 "" "/usr/local/texlive/2025/texmf-dist/tex/latex/base/ifthen.sty" 1738182759 5525 9dced5929f36b19fa837947f5175b331 ""
@ -70,8 +99,8 @@
"/usr/local/texlive/2025/texmf-dist/tex/latex/csquotes/csquotes.def" 1712263026 22135 0975a49eeaed232aa861e9425ffb2e7c "" "/usr/local/texlive/2025/texmf-dist/tex/latex/csquotes/csquotes.def" 1712263026 22135 0975a49eeaed232aa861e9425ffb2e7c ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/csquotes/csquotes.sty" 1712263026 62767 e79d6d7a989e7da62dcf3d0a65c1faee "" "/usr/local/texlive/2025/texmf-dist/tex/latex/csquotes/csquotes.sty" 1712263026 62767 e79d6d7a989e7da62dcf3d0a65c1faee ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/etoolbox/etoolbox.sty" 1739306980 46850 d87daedc2abdc653769a6f1067849fe0 "" "/usr/local/texlive/2025/texmf-dist/tex/latex/etoolbox/etoolbox.sty" 1739306980 46850 d87daedc2abdc653769a6f1067849fe0 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/float/float.sty" 1137110151 6749 16d2656a1984957e674b149555f1ea1d ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/graphics/keyval.sty" 1717359999 2671 70891d50dac933918b827d326687c6e8 "" "/usr/local/texlive/2025/texmf-dist/tex/latex/graphics/keyval.sty" 1717359999 2671 70891d50dac933918b827d326687c6e8 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/ifoddpage/ifoddpage.sty" 1666126449 2142 eae42205b97b7a3ad0e58db5fe99e3e6 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/kvoptions/kvoptions.sty" 1655478651 22555 6d8e155cfef6d82c3d5c742fea7c992e "" "/usr/local/texlive/2025/texmf-dist/tex/latex/kvoptions/kvoptions.sty" 1655478651 22555 6d8e155cfef6d82c3d5c742fea7c992e ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/kvsetkeys/kvsetkeys.sty" 1665067230 13815 760b0c02f691ea230f5359c4e1de23a7 "" "/usr/local/texlive/2025/texmf-dist/tex/latex/kvsetkeys/kvsetkeys.sty" 1665067230 13815 760b0c02f691ea230f5359c4e1de23a7 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/l3backend/l3backend-pdftex.def" 1716410060 29785 9f93ab201fe5dd053afcc6c1bcf7d266 "" "/usr/local/texlive/2025/texmf-dist/tex/latex/l3backend/l3backend-pdftex.def" 1716410060 29785 9f93ab201fe5dd053afcc6c1bcf7d266 ""
@ -81,20 +110,19 @@
"/usr/local/texlive/2025/texmf-dist/tex/latex/logreq/logreq.sty" 1284153563 6187 b27afc771af565d3a9ff1ca7d16d0d46 "" "/usr/local/texlive/2025/texmf-dist/tex/latex/logreq/logreq.sty" 1284153563 6187 b27afc771af565d3a9ff1ca7d16d0d46 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/preprint/authblk.sty" 1368488610 7016 985a983ce041cc8959cd31133cba0244 "" "/usr/local/texlive/2025/texmf-dist/tex/latex/preprint/authblk.sty" 1368488610 7016 985a983ce041cc8959cd31133cba0244 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/preprint/fullpage.sty" 1137110595 2789 05b418f78b224ec872f5b11081138605 "" "/usr/local/texlive/2025/texmf-dist/tex/latex/preprint/fullpage.sty" 1137110595 2789 05b418f78b224ec872f5b11081138605 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/relsize/relsize.sty" 1369619135 15542 c4cc3164fe24f2f2fbb06eb71b1da4c4 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/tools/xspace.sty" 1717359999 4545 e3f4de576c914e2000f07f69a891c071 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/url/url.sty" 1388531844 12796 8edb7d69a20b857904dd0ea757c14ec9 "" "/usr/local/texlive/2025/texmf-dist/tex/latex/url/url.sty" 1388531844 12796 8edb7d69a20b857904dd0ea757c14ec9 ""
"/usr/local/texlive/2025/texmf-dist/web2c/texmf.cnf" 1739380943 42148 61becc7c670cd061bb319c643c27fdd4 "" "/usr/local/texlive/2025/texmf-dist/web2c/texmf.cnf" 1739380943 42148 61becc7c670cd061bb319c643c27fdd4 ""
"/usr/local/texlive/2025/texmf-var/fonts/map/pdftex/updmap/pdftex.map" 1743313660 5501089 f2ffe622267f7d8bfaba0244ab87ba6f "" "/usr/local/texlive/2025/texmf-var/fonts/map/pdftex/updmap/pdftex.map" 1743313660 5501089 f2ffe622267f7d8bfaba0244ab87ba6f ""
"/usr/local/texlive/2025/texmf-var/web2c/pdftex/pdflatex.fmt" 1743313810 3345755 ba2ca5aadbc395a8eb3e969a7d392ec2 "" "/usr/local/texlive/2025/texmf-var/web2c/pdftex/pdflatex.fmt" 1743313810 3345755 ba2ca5aadbc395a8eb3e969a7d392ec2 ""
"/usr/local/texlive/2025/texmf.cnf" 1743313649 455 5b996dcaa0eb4ef14a83b026bc0a008c "" "/usr/local/texlive/2025/texmf.cnf" 1743313649 455 5b996dcaa0eb4ef14a83b026bc0a008c ""
"/workspaces/containers/recherches/ALDLoverAB/main.tex" 1745569300.58113 728 260366a29ef55ffa4b47d22972e9e4f8 "" "/workspaces/containers/recherches/ALDLoverAB/main.tex" 1747299196.84721 1315 a94740caa185b946ba5aaded501a4fac ""
"algo/index.tex" 1746172815.76911 1775 b458edc79675260c269751db3322cda9 "" "algo/index.tex" 1747297294.63478 3848 bbe77613f7a73141ef38e5297b411992 ""
"intro/index.tex" 1745569389.83114 2291 8451d9b4ced1f44c45b59e7619773077 "" "intro/index.tex" 1747297807.29159 3161 448e66cc700f6c11abf8aafdf01ab6a8 ""
"main.aux" 1746172816.38012 1400 8864237b874322217e4ed828cbb90076 "pdflatex" "main.aux" 1747309539.00275 1342 dbdb34d6c1afc7be4a9ecbc27e420731 "pdflatex"
"main.bbl" 1746171033.92694 466 76d65a242ec496c9b4361af646ff12cb "biber main" "main.bbl" 1747233716.74109 466 76d65a242ec496c9b4361af646ff12cb "biber main"
"main.run.xml" 1746172816.38212 2301 7adc9b5a22e7927ebfdd8580ad5d647d "pdflatex" "main.run.xml" 1747309539.00575 2301 7adc9b5a22e7927ebfdd8580ad5d647d "pdflatex"
"main.tex" 1745569300.58113 728 260366a29ef55ffa4b47d22972e9e4f8 "" "main.tex" 1747299196.84721 1315 a94740caa185b946ba5aaded501a4fac ""
"proof/index.tex" 1747309536.90972 6390 ff2a2396c48aac05b56092c04c844d25 ""
(generated) (generated)
"main.aux" "main.aux"
"main.bcf" "main.bcf"

66
recherches/ALDLoverAB/main.fls
View File

@ -43,6 +43,20 @@ INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/preprint/authblk.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/preprint/authblk.sty INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/preprint/authblk.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/preprint/fullpage.sty INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/preprint/fullpage.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/preprint/fullpage.sty INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/preprint/fullpage.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amsmath.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amsmath.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amsopn.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amstext.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amstext.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amsgen.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amsgen.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amsbsy.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amsbsy.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amsopn.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/amsfonts/amssymb.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/amsfonts/amssymb.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/amsfonts/amsfonts.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/amsfonts/amsfonts.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/biblatex/biblatex.sty INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/biblatex/biblatex.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/biblatex/biblatex.sty INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/biblatex/biblatex.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pdftexcmds/pdftexcmds.sty INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pdftexcmds/pdftexcmds.sty
@ -95,14 +109,14 @@ INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/biblatex/blx-case-expl3.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/biblatex/blx-case-expl3.sty INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/biblatex/blx-case-expl3.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/l3packages/xparse/xparse.sty INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/l3packages/xparse/xparse.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/l3packages/xparse/xparse.sty INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/l3packages/xparse/xparse.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/algorithm2e/algorithm2e.sty INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/algorithms/algorithm.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/algorithm2e/algorithm2e.sty INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/algorithms/algorithm.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/ifoddpage/ifoddpage.sty INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/float/float.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/ifoddpage/ifoddpage.sty INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/float/float.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/tools/xspace.sty INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/algorithmicx/algorithmicx.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/tools/xspace.sty INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/algorithmicx/algorithmicx.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/relsize/relsize.sty INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/algorithmicx/algpseudocode.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/relsize/relsize.sty INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/algorithmicx/algpseudocode.sty
INPUT ./main.aux INPUT ./main.aux
INPUT ./main.aux INPUT ./main.aux
INPUT main.aux INPUT main.aux
@ -130,12 +144,39 @@ INPUT ./intro/index.tex
INPUT intro/index.tex INPUT intro/index.tex
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecbx1000.tfm INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecbx1000.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecti1000.tfm INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecti1000.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/cmextra/cmex7.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/cmextra/cmex7.tfm
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/amsfonts/umsa.fd
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/amsfonts/umsa.fd
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/amsfonts/umsa.fd
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam10.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam7.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam5.tfm
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/amsfonts/umsb.fd
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/amsfonts/umsb.fd
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/amsfonts/umsb.fd
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm10.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm7.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm5.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecti0700.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecti0500.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ectt1000.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecrm0700.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ectt0800.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecrm0500.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ectt0800.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecit1000.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecit0800.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecit0800.tfm
INPUT ./algo/index.tex INPUT ./algo/index.tex
INPUT ./algo/index.tex INPUT ./algo/index.tex
INPUT algo/index.tex INPUT algo/index.tex
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecbx0700.tfm INPUT ./proof/index.tex
INPUT ./proof/index.tex
INPUT proof/index.tex
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecbi1000.tfm INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecbi1000.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ectt1000.tfm INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecbi0700.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecbi0500.tfm
INPUT main.aux INPUT main.aux
INPUT main.run.xml INPUT main.run.xml
OUTPUT main.run.xml OUTPUT main.run.xml
@ -144,17 +185,20 @@ INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.p
INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi5.pfb INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi5.pfb
INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi7.pfb INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi7.pfb
INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb
INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmr5.pfb
INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmr7.pfb INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmr7.pfb
INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb
INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy7.pfb INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy7.pfb
INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/symbols/msam10.pfb
INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfbi1000.pfb INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfbi1000.pfb
INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfbx0700.pfb
INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfbx1000.pfb INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfbx1000.pfb
INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfbx1200.pfb INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfbx1200.pfb
INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfbx1440.pfb INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfbx1440.pfb
INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfit1000.pfb
INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfrm1000.pfb INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfrm1000.pfb
INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfrm1200.pfb INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfrm1200.pfb
INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfrm1728.pfb INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfrm1728.pfb
INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfti0700.pfb
INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfti1000.pfb INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfti1000.pfb
INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfti1200.pfb INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfti1200.pfb
INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sftt1000.pfb INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sftt1000.pfb

562
recherches/ALDLoverAB/main.log
View File

@ -1,4 +1,4 @@
This is pdfTeX, Version 3.141592653-2.6-1.40.27 (TeX Live 2025) (preloaded format=pdflatex 2025.3.30) 2 MAY 2025 08:00 This is pdfTeX, Version 3.141592653-2.6-1.40.27 (TeX Live 2025) (preloaded format=pdflatex 2025.3.30) 15 MAY 2025 11:45
entering extended mode entering extended mode
restricted \write18 enabled. restricted \write18 enabled.
file:line:error style messages enabled. file:line:error style messages enabled.
@ -100,7 +100,80 @@ Package: authblk 2001/02/27 1.3 (PWD)
) (/usr/local/texlive/2025/texmf-dist/tex/latex/preprint/fullpage.sty ) (/usr/local/texlive/2025/texmf-dist/tex/latex/preprint/fullpage.sty
Package: fullpage 1999/02/23 1.1 (PWD) Package: fullpage 1999/02/23 1.1 (PWD)
\FP@margin=\skip53 \FP@margin=\skip53
) (/usr/local/texlive/2025/texmf-dist/tex/latex/biblatex/biblatex.sty ) (/usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amsmath.sty
Package: amsmath 2024/11/05 v2.17t AMS math features
\@mathmargin=\skip54
For additional information on amsmath, use the `?' option.
(/usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amstext.sty
Package: amstext 2021/08/26 v2.01 AMS text
(/usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amsgen.sty
File: amsgen.sty 1999/11/30 v2.0 generic functions
\@emptytoks=\toks22
\ex@=\dimen152
)) (/usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amsbsy.sty
Package: amsbsy 1999/11/29 v1.2d Bold Symbols
\pmbraise@=\dimen153
) (/usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amsopn.sty
Package: amsopn 2022/04/08 v2.04 operator names
)
\inf@bad=\count289
LaTeX Info: Redefining \frac on input line 233.
\uproot@=\count290
\leftroot@=\count291
LaTeX Info: Redefining \overline on input line 398.
LaTeX Info: Redefining \colon on input line 409.
\classnum@=\count292
\DOTSCASE@=\count293
LaTeX Info: Redefining \ldots on input line 495.
LaTeX Info: Redefining \dots on input line 498.
LaTeX Info: Redefining \cdots on input line 619.
\Mathstrutbox@=\box52
\strutbox@=\box53
LaTeX Info: Redefining \big on input line 721.
LaTeX Info: Redefining \Big on input line 722.
LaTeX Info: Redefining \bigg on input line 723.
LaTeX Info: Redefining \Bigg on input line 724.
\big@size=\dimen154
LaTeX Font Info: Redeclaring font encoding OML on input line 742.
LaTeX Font Info: Redeclaring font encoding OMS on input line 743.
\macc@depth=\count294
LaTeX Info: Redefining \bmod on input line 904.
LaTeX Info: Redefining \pmod on input line 909.
LaTeX Info: Redefining \smash on input line 939.
LaTeX Info: Redefining \relbar on input line 969.
LaTeX Info: Redefining \Relbar on input line 970.
\c@MaxMatrixCols=\count295
\dotsspace@=\muskip17
\c@parentequation=\count296
\dspbrk@lvl=\count297
\tag@help=\toks23
\row@=\count298
\column@=\count299
\maxfields@=\count300
\andhelp@=\toks24
\eqnshift@=\dimen155
\alignsep@=\dimen156
\tagshift@=\dimen157
\tagwidth@=\dimen158
\totwidth@=\dimen159
\lineht@=\dimen160
\@envbody=\toks25
\multlinegap=\skip55
\multlinetaggap=\skip56
\mathdisplay@stack=\toks26
LaTeX Info: Redefining \[ on input line 2953.
LaTeX Info: Redefining \] on input line 2954.
) (/usr/local/texlive/2025/texmf-dist/tex/latex/amsfonts/amssymb.sty
Package: amssymb 2013/01/14 v3.01 AMS font symbols
(/usr/local/texlive/2025/texmf-dist/tex/latex/amsfonts/amsfonts.sty
Package: amsfonts 2013/01/14 v3.01 Basic AMSFonts support
\symAMSa=\mathgroup4
\symAMSb=\mathgroup5
LaTeX Font Info: Redeclaring math symbol \hbar on input line 98.
LaTeX Font Info: Overwriting math alphabet `\mathfrak' in version `bold'
(Font) U/euf/m/n --> U/euf/b/n on input line 106.
)) (/usr/local/texlive/2025/texmf-dist/tex/latex/biblatex/biblatex.sty
Package: biblatex 2024/03/21 v3.20 programmable bibliographies (PK/MW) Package: biblatex 2024/03/21 v3.20 programmable bibliographies (PK/MW)
(/usr/local/texlive/2025/texmf-dist/tex/generic/pdftexcmds/pdftexcmds.sty (/usr/local/texlive/2025/texmf-dist/tex/generic/pdftexcmds/pdftexcmds.sty
Package: pdftexcmds 2020-06-27 v0.33 Utility functions of pdfTeX for LuaTeX (HO) Package: pdftexcmds 2020-06-27 v0.33 Utility functions of pdfTeX for LuaTeX (HO)
@ -120,72 +193,72 @@ Package: kvoptions 2022-06-15 v3.15 Key value format for package options (HO)
Package: kvsetkeys 2022-10-05 v1.19 Key value parser (HO) Package: kvsetkeys 2022-10-05 v1.19 Key value parser (HO)
)) (/usr/local/texlive/2025/texmf-dist/tex/latex/logreq/logreq.sty )) (/usr/local/texlive/2025/texmf-dist/tex/latex/logreq/logreq.sty
Package: logreq 2010/08/04 v1.0 xml request logger Package: logreq 2010/08/04 v1.0 xml request logger
\lrq@indent=\count289 \lrq@indent=\count301
(/usr/local/texlive/2025/texmf-dist/tex/latex/logreq/logreq.def (/usr/local/texlive/2025/texmf-dist/tex/latex/logreq/logreq.def
File: logreq.def 2010/08/04 v1.0 logreq spec v1.0 File: logreq.def 2010/08/04 v1.0 logreq spec v1.0
)) (/usr/local/texlive/2025/texmf-dist/tex/latex/base/ifthen.sty )) (/usr/local/texlive/2025/texmf-dist/tex/latex/base/ifthen.sty
Package: ifthen 2024/03/16 v1.1e Standard LaTeX ifthen package (DPC) Package: ifthen 2024/03/16 v1.1e Standard LaTeX ifthen package (DPC)
) (/usr/local/texlive/2025/texmf-dist/tex/latex/url/url.sty ) (/usr/local/texlive/2025/texmf-dist/tex/latex/url/url.sty
\Urlmuskip=\muskip17 \Urlmuskip=\muskip18
Package: url 2013/09/16 ver 3.4 Verb mode for urls, etc. Package: url 2013/09/16 ver 3.4 Verb mode for urls, etc.
) )
\c@tabx@nest=\count290 \c@tabx@nest=\count302
\c@listtotal=\count291 \c@listtotal=\count303
\c@listcount=\count292 \c@listcount=\count304
\c@liststart=\count293 \c@liststart=\count305
\c@liststop=\count294 \c@liststop=\count306
\c@citecount=\count295 \c@citecount=\count307
\c@citetotal=\count296 \c@citetotal=\count308
\c@multicitecount=\count297 \c@multicitecount=\count309
\c@multicitetotal=\count298 \c@multicitetotal=\count310
\c@instcount=\count299 \c@instcount=\count311
\c@maxnames=\count300 \c@maxnames=\count312
\c@minnames=\count301 \c@minnames=\count313
\c@maxitems=\count302 \c@maxitems=\count314
\c@minitems=\count303 \c@minitems=\count315
\c@citecounter=\count304 \c@citecounter=\count316
\c@maxcitecounter=\count305 \c@maxcitecounter=\count317
\c@savedcitecounter=\count306 \c@savedcitecounter=\count318
\c@uniquelist=\count307 \c@uniquelist=\count319
\c@uniquename=\count308 \c@uniquename=\count320
\c@refsection=\count309 \c@refsection=\count321
\c@refsegment=\count310 \c@refsegment=\count322
\c@maxextratitle=\count311 \c@maxextratitle=\count323
\c@maxextratitleyear=\count312 \c@maxextratitleyear=\count324
\c@maxextraname=\count313 \c@maxextraname=\count325
\c@maxextradate=\count314 \c@maxextradate=\count326
\c@maxextraalpha=\count315 \c@maxextraalpha=\count327
\c@abbrvpenalty=\count316 \c@abbrvpenalty=\count328
\c@highnamepenalty=\count317 \c@highnamepenalty=\count329
\c@lownamepenalty=\count318 \c@lownamepenalty=\count330
\c@maxparens=\count319 \c@maxparens=\count331
\c@parenlevel=\count320 \c@parenlevel=\count332
\blx@tempcnta=\count321 \blx@tempcnta=\count333
\blx@tempcntb=\count322 \blx@tempcntb=\count334
\blx@tempcntc=\count323 \blx@tempcntc=\count335
\c@blx@maxsection=\count324 \c@blx@maxsection=\count336
\blx@maxsegment@0=\count325 \blx@maxsegment@0=\count337
\blx@notetype=\count326 \blx@notetype=\count338
\blx@parenlevel@text=\count327 \blx@parenlevel@text=\count339
\blx@parenlevel@foot=\count328 \blx@parenlevel@foot=\count340
\blx@sectionciteorder@0=\count329 \blx@sectionciteorder@0=\count341
\blx@sectionciteorderinternal@0=\count330 \blx@sectionciteorderinternal@0=\count342
\blx@entrysetcounter=\count331 \blx@entrysetcounter=\count343
\blx@biblioinstance=\count332 \blx@biblioinstance=\count344
\labelnumberwidth=\skip54 \labelnumberwidth=\skip57
\labelalphawidth=\skip55 \labelalphawidth=\skip58
\biblabelsep=\skip56 \biblabelsep=\skip59
\bibitemsep=\skip57 \bibitemsep=\skip60
\bibnamesep=\skip58 \bibnamesep=\skip61
\bibinitsep=\skip59 \bibinitsep=\skip62
\bibparsep=\skip60 \bibparsep=\skip63
\bibhang=\skip61 \bibhang=\skip64
\blx@bcfin=\read3 \blx@bcfin=\read3
\blx@bcfout=\write3 \blx@bcfout=\write3
\blx@langwohyphens=\language91 \blx@langwohyphens=\language91
\c@mincomprange=\count333 \c@mincomprange=\count345
\c@maxcomprange=\count334 \c@maxcomprange=\count346
\c@mincompwidth=\count335 \c@mincompwidth=\count347
Package biblatex Info: Trying to load biblatex default data model... Package biblatex Info: Trying to load biblatex default data model...
Package biblatex Info: ... file 'blx-dm.def' found. Package biblatex Info: ... file 'blx-dm.def' found.
(/usr/local/texlive/2025/texmf-dist/tex/latex/biblatex/blx-dm.def (/usr/local/texlive/2025/texmf-dist/tex/latex/biblatex/blx-dm.def
@ -193,88 +266,88 @@ File: blx-dm.def 2024/03/21 v3.20 biblatex datamodel (PK/MW)
) )
Package biblatex Info: Trying to load biblatex custom data model... Package biblatex Info: Trying to load biblatex custom data model...
Package biblatex Info: ... file 'biblatex-dm.cfg' not found. Package biblatex Info: ... file 'biblatex-dm.cfg' not found.
\c@afterword=\count336 \c@afterword=\count348
\c@savedafterword=\count337 \c@savedafterword=\count349
\c@annotator=\count338 \c@annotator=\count350
\c@savedannotator=\count339 \c@savedannotator=\count351
\c@author=\count340 \c@author=\count352
\c@savedauthor=\count341 \c@savedauthor=\count353
\c@bookauthor=\count342 \c@bookauthor=\count354
\c@savedbookauthor=\count343 \c@savedbookauthor=\count355
\c@commentator=\count344 \c@commentator=\count356
\c@savedcommentator=\count345 \c@savedcommentator=\count357
\c@editor=\count346 \c@editor=\count358
\c@savededitor=\count347 \c@savededitor=\count359
\c@editora=\count348 \c@editora=\count360
\c@savededitora=\count349 \c@savededitora=\count361
\c@editorb=\count350 \c@editorb=\count362
\c@savededitorb=\count351 \c@savededitorb=\count363
\c@editorc=\count352 \c@editorc=\count364
\c@savededitorc=\count353 \c@savededitorc=\count365
\c@foreword=\count354 \c@foreword=\count366
\c@savedforeword=\count355 \c@savedforeword=\count367
\c@holder=\count356 \c@holder=\count368
\c@savedholder=\count357 \c@savedholder=\count369
\c@introduction=\count358 \c@introduction=\count370
\c@savedintroduction=\count359 \c@savedintroduction=\count371
\c@namea=\count360 \c@namea=\count372
\c@savednamea=\count361 \c@savednamea=\count373
\c@nameb=\count362 \c@nameb=\count374
\c@savednameb=\count363 \c@savednameb=\count375
\c@namec=\count364 \c@namec=\count376
\c@savednamec=\count365 \c@savednamec=\count377
\c@translator=\count366 \c@translator=\count378
\c@savedtranslator=\count367 \c@savedtranslator=\count379
\c@shortauthor=\count368 \c@shortauthor=\count380
\c@savedshortauthor=\count369 \c@savedshortauthor=\count381
\c@shorteditor=\count370 \c@shorteditor=\count382
\c@savedshorteditor=\count371 \c@savedshorteditor=\count383
\c@labelname=\count372 \c@labelname=\count384
\c@savedlabelname=\count373 \c@savedlabelname=\count385
\c@institution=\count374 \c@institution=\count386
\c@savedinstitution=\count375 \c@savedinstitution=\count387
\c@lista=\count376 \c@lista=\count388
\c@savedlista=\count377 \c@savedlista=\count389
\c@listb=\count378 \c@listb=\count390
\c@savedlistb=\count379 \c@savedlistb=\count391
\c@listc=\count380 \c@listc=\count392
\c@savedlistc=\count381 \c@savedlistc=\count393
\c@listd=\count382 \c@listd=\count394
\c@savedlistd=\count383 \c@savedlistd=\count395
\c@liste=\count384 \c@liste=\count396
\c@savedliste=\count385 \c@savedliste=\count397
\c@listf=\count386 \c@listf=\count398
\c@savedlistf=\count387 \c@savedlistf=\count399
\c@location=\count388 \c@location=\count400
\c@savedlocation=\count389 \c@savedlocation=\count401
\c@organization=\count390 \c@organization=\count402
\c@savedorganization=\count391 \c@savedorganization=\count403
\c@origlocation=\count392 \c@origlocation=\count404
\c@savedoriglocation=\count393 \c@savedoriglocation=\count405
\c@origpublisher=\count394 \c@origpublisher=\count406
\c@savedorigpublisher=\count395 \c@savedorigpublisher=\count407
\c@publisher=\count396 \c@publisher=\count408
\c@savedpublisher=\count397 \c@savedpublisher=\count409
\c@language=\count398 \c@language=\count410
\c@savedlanguage=\count399 \c@savedlanguage=\count411
\c@origlanguage=\count400 \c@origlanguage=\count412
\c@savedoriglanguage=\count401 \c@savedoriglanguage=\count413
\c@pageref=\count402 \c@pageref=\count414
\c@savedpageref=\count403 \c@savedpageref=\count415
\shorthandwidth=\skip62 \shorthandwidth=\skip65
\shortjournalwidth=\skip63 \shortjournalwidth=\skip66
\shortserieswidth=\skip64 \shortserieswidth=\skip67
\shorttitlewidth=\skip65 \shorttitlewidth=\skip68
\shortauthorwidth=\skip66 \shortauthorwidth=\skip69
\shorteditorwidth=\skip67 \shorteditorwidth=\skip70
\locallabelnumberwidth=\skip68 \locallabelnumberwidth=\skip71
\locallabelalphawidth=\skip69 \locallabelalphawidth=\skip72
\localshorthandwidth=\skip70 \localshorthandwidth=\skip73
\localshortjournalwidth=\skip71 \localshortjournalwidth=\skip74
\localshortserieswidth=\skip72 \localshortserieswidth=\skip75
\localshorttitlewidth=\skip73 \localshorttitlewidth=\skip76
\localshortauthorwidth=\skip74 \localshortauthorwidth=\skip77
\localshorteditorwidth=\skip75 \localshorteditorwidth=\skip78
Package biblatex Info: Trying to load compatibility code... Package biblatex Info: Trying to load compatibility code...
Package biblatex Info: ... file 'blx-compat.def' found. Package biblatex Info: ... file 'blx-compat.def' found.
(/usr/local/texlive/2025/texmf-dist/tex/latex/biblatex/blx-compat.def (/usr/local/texlive/2025/texmf-dist/tex/latex/biblatex/blx-compat.def
@ -284,19 +357,19 @@ Package biblatex Info: Trying to load generic definitions...
Package biblatex Info: ... file 'biblatex.def' found. Package biblatex Info: ... file 'biblatex.def' found.
(/usr/local/texlive/2025/texmf-dist/tex/latex/biblatex/biblatex.def (/usr/local/texlive/2025/texmf-dist/tex/latex/biblatex/biblatex.def
File: biblatex.def 2024/03/21 v3.20 biblatex compatibility (PK/MW) File: biblatex.def 2024/03/21 v3.20 biblatex compatibility (PK/MW)
\c@textcitecount=\count404 \c@textcitecount=\count416
\c@textcitetotal=\count405 \c@textcitetotal=\count417
\c@textcitemaxnames=\count406 \c@textcitemaxnames=\count418
\c@biburlbigbreakpenalty=\count407 \c@biburlbigbreakpenalty=\count419
\c@biburlbreakpenalty=\count408 \c@biburlbreakpenalty=\count420
\c@biburlnumpenalty=\count409 \c@biburlnumpenalty=\count421
\c@biburlucpenalty=\count410 \c@biburlucpenalty=\count422
\c@biburllcpenalty=\count411 \c@biburllcpenalty=\count423
\biburlbigskip=\muskip18 \biburlbigskip=\muskip19
\biburlnumskip=\muskip19 \biburlnumskip=\muskip20
\biburlucskip=\muskip20 \biburlucskip=\muskip21
\biburllcskip=\muskip21 \biburllcskip=\muskip22
\c@smartand=\count412 \c@smartand=\count424
) )
Package biblatex Info: Trying to load bibliography style 'numeric'... Package biblatex Info: Trying to load bibliography style 'numeric'...
Package biblatex Info: ... file 'numeric.bbx' found. Package biblatex Info: ... file 'numeric.bbx' found.
@ -306,8 +379,8 @@ Package biblatex Info: Trying to load bibliography style 'standard'...
Package biblatex Info: ... file 'standard.bbx' found. Package biblatex Info: ... file 'standard.bbx' found.
(/usr/local/texlive/2025/texmf-dist/tex/latex/biblatex/bbx/standard.bbx (/usr/local/texlive/2025/texmf-dist/tex/latex/biblatex/bbx/standard.bbx
File: standard.bbx 2024/03/21 v3.20 biblatex bibliography style (PK/MW) File: standard.bbx 2024/03/21 v3.20 biblatex bibliography style (PK/MW)
\c@bbx:relatedcount=\count413 \c@bbx:relatedcount=\count425
\c@bbx:relatedtotal=\count414 \c@bbx:relatedtotal=\count426
)) ))
Package biblatex Info: Trying to load citation style 'numeric'... Package biblatex Info: Trying to load citation style 'numeric'...
Package biblatex Info: ... file 'numeric.cbx' found. Package biblatex Info: ... file 'numeric.cbx' found.
@ -336,8 +409,8 @@ Package biblatex Info: Document encoding is UTF8 ....
Package: expl3 2025-01-18 L3 programming layer (loader) Package: expl3 2025-01-18 L3 programming layer (loader)
(/usr/local/texlive/2025/texmf-dist/tex/latex/l3backend/l3backend-pdftex.def (/usr/local/texlive/2025/texmf-dist/tex/latex/l3backend/l3backend-pdftex.def
File: l3backend-pdftex.def 2024-05-08 L3 backend support: PDF output (pdfTeX) File: l3backend-pdftex.def 2024-05-08 L3 backend support: PDF output (pdfTeX)
\l__color_backend_stack_int=\count415 \l__color_backend_stack_int=\count427
\l__pdf_internal_box=\box52 \l__pdf_internal_box=\box54
)) ))
Package biblatex Info: ... and expl3 Package biblatex Info: ... and expl3
(biblatex) 2025-01-18 L3 programming layer (loader) (biblatex) 2025-01-18 L3 programming layer (loader)
@ -347,81 +420,67 @@ Package biblatex Info: ... and expl3
Package: xparse 2024-08-16 L3 Experimental document command parser Package: xparse 2024-08-16 L3 Experimental document command parser
) )
Package: blx-case-expl3 2024/03/21 v3.20 expl3 case changing code for biblatex Package: blx-case-expl3 2024/03/21 v3.20 expl3 case changing code for biblatex
)) (/usr/local/texlive/2025/texmf-dist/tex/latex/algorithm2e/algorithm2e.sty )) (/usr/local/texlive/2025/texmf-dist/tex/latex/algorithms/algorithm.sty
Package: algorithm2e 2017/07/18 v5.2 algorithms environments Package: algorithm 2009/08/24 v0.1 Document Style `algorithm' - floating environment
\c@AlgoLine=\count416 (/usr/local/texlive/2025/texmf-dist/tex/latex/float/float.sty
\algocf@hangindent=\skip76 Package: float 2001/11/08 v1.3d Float enhancements (AL)
(/usr/local/texlive/2025/texmf-dist/tex/latex/ifoddpage/ifoddpage.sty \c@float@type=\count428
Package: ifoddpage 2022/10/18 v1.2 Conditionals for odd/even page detection \float@exts=\toks27
\c@checkoddpage=\count417 \float@box=\box55
) (/usr/local/texlive/2025/texmf-dist/tex/latex/tools/xspace.sty \@float@everytoks=\toks28
Package: xspace 2014/10/28 v1.13 Space after command names (DPC,MH) \@floatcapt=\box56
) (/usr/local/texlive/2025/texmf-dist/tex/latex/relsize/relsize.sty
Package: relsize 2013/03/29 ver 4.1
) )
\skiptotal=\skip77 \@float@every@algorithm=\toks29
\skiplinenumber=\skip78 \c@algorithm=\count429
\skiprule=\skip79 ) (/usr/local/texlive/2025/texmf-dist/tex/latex/algorithmicx/algorithmicx.sty
\skiphlne=\skip80 Package: algorithmicx 2005/04/27 v1.2 Algorithmicx
\skiptext=\skip81
\skiplength=\skip82 Document Style algorithmicx 1.2 - a greatly improved `algorithmic' style
\algomargin=\skip83 \c@ALG@line=\count430
\skipalgocfslide=\skip84 \c@ALG@rem=\count431
\algowidth=\dimen152 \c@ALG@nested=\count432
\inoutsize=\dimen153 \ALG@tlm=\skip79
\inoutindent=\dimen154 \ALG@thistlm=\skip80
\interspacetitleruled=\dimen155 \c@ALG@Lnr=\count433
\interspacealgoruled=\dimen156 \c@ALG@blocknr=\count434
\interspacetitleboxruled=\dimen157 \c@ALG@storecount=\count435
\algocf@ruledwidth=\skip85 \c@ALG@tmpcounter=\count436
\algocf@inoutbox=\box53 \ALG@tmplength=\skip81
\algocf@inputbox=\box54 ) (/usr/local/texlive/2025/texmf-dist/tex/latex/algorithmicx/algpseudocode.sty
\AlCapSkip=\skip86 Package: algpseudocode
\AlCapHSkip=\skip87
\algoskipindent=\skip88 Document Style - pseudocode environments for use with the `algorithmicx' style
\algocf@nlbox=\box55
\algocf@hangingbox=\box56
\algocf@untilbox=\box57
\algocf@skipuntil=\skip89
\algocf@capbox=\box58
\algocf@lcaptionbox=\skip90
\algoheightruledefault=\skip91
\algoheightrule=\skip92
\algotitleheightruledefault=\skip93
\algotitleheightrule=\skip94
\c@algocfline=\count418
\c@algocfproc=\count419
\c@algocf=\count420
\algocf@algoframe=\box59
\algocf@algobox=\box60
) )
\c@theorem=\count421 \c@algoLine=\count437
\c@property=\count438
\c@theorem=\count439
\c@proof=\count440
Package csquotes Info: Checking for multilingual support... Package csquotes Info: Checking for multilingual support...
Package csquotes Info: ... found 'babel' package. Package csquotes Info: ... found 'babel' package.
Package csquotes Info: Adjusting default style. Package csquotes Info: Adjusting default style.
Package csquotes Info: Redefining alias 'default' -> 'french'. Package csquotes Info: Redefining alias 'default' -> 'french'.
(./main.aux (./main.aux
Package babel Info: 'french' activates 'french' shorthands. Package babel Info: 'french' activates 'french' shorthands.
(babel) Reported on input line 10. (babel) Reported on input line 9.
) )
\openout1 = `main.aux'. \openout1 = `main.aux'.
LaTeX Font Info: Checking defaults for OML/cmm/m/it on input line 18. LaTeX Font Info: Checking defaults for OML/cmm/m/it on input line 37.
LaTeX Font Info: ... okay on input line 18. LaTeX Font Info: ... okay on input line 37.
LaTeX Font Info: Checking defaults for OMS/cmsy/m/n on input line 18. LaTeX Font Info: Checking defaults for OMS/cmsy/m/n on input line 37.
LaTeX Font Info: ... okay on input line 18. LaTeX Font Info: ... okay on input line 37.
LaTeX Font Info: Checking defaults for OT1/cmr/m/n on input line 18. LaTeX Font Info: Checking defaults for OT1/cmr/m/n on input line 37.
LaTeX Font Info: ... okay on input line 18. LaTeX Font Info: ... okay on input line 37.
LaTeX Font Info: Checking defaults for T1/cmr/m/n on input line 18. LaTeX Font Info: Checking defaults for T1/cmr/m/n on input line 37.
LaTeX Font Info: ... okay on input line 18. LaTeX Font Info: ... okay on input line 37.
LaTeX Font Info: Checking defaults for TS1/cmr/m/n on input line 18. LaTeX Font Info: Checking defaults for TS1/cmr/m/n on input line 37.
LaTeX Font Info: ... okay on input line 18. LaTeX Font Info: ... okay on input line 37.
LaTeX Font Info: Checking defaults for OMX/cmex/m/n on input line 18. LaTeX Font Info: Checking defaults for OMX/cmex/m/n on input line 37.
LaTeX Font Info: ... okay on input line 18. LaTeX Font Info: ... okay on input line 37.
LaTeX Font Info: Checking defaults for U/cmr/m/n on input line 18. LaTeX Font Info: Checking defaults for U/cmr/m/n on input line 37.
LaTeX Font Info: ... okay on input line 18. LaTeX Font Info: ... okay on input line 37.
LaTeX Info: Redefining \degres on input line 18. LaTeX Info: Redefining \degres on input line 37.
LaTeX Info: Redefining \up on input line 18. LaTeX Info: Redefining \up on input line 37.
Package biblatex Info: Trying to load language 'french'... Package biblatex Info: Trying to load language 'french'...
Package biblatex Info: ... file 'french.lbx' found. Package biblatex Info: ... file 'french.lbx' found.
(/usr/local/texlive/2025/texmf-dist/tex/latex/biblatex/lbx/french.lbx (/usr/local/texlive/2025/texmf-dist/tex/latex/biblatex/lbx/french.lbx
@ -435,36 +494,55 @@ Package biblatex Info: Automatic encoding selection.
Package biblatex Info: Trying to load bibliographic data... Package biblatex Info: Trying to load bibliographic data...
Package biblatex Info: ... file 'main.bbl' found. Package biblatex Info: ... file 'main.bbl' found.
(./main.bbl) (./main.bbl)
Package biblatex Info: Reference section=0 on input line 18. Package biblatex Info: Reference section=0 on input line 37.
Package biblatex Info: Reference segment=0 on input line 18. Package biblatex Info: Reference segment=0 on input line 37.
[1 [1
{/usr/local/texlive/2025/texmf-var/fonts/map/pdftex/updmap/pdftex.map}{/usr/local/texlive/2025/texmf-dist/fonts/enc/dvips/cm-super/cm-super-t1.enc}] (./intro/index.tex {/usr/local/texlive/2025/texmf-var/fonts/map/pdftex/updmap/pdftex.map}{/usr/local/texlive/2025/texmf-dist/fonts/enc/dvips/cm-super/cm-super-t1.enc}] (./intro/index.tex
LaTeX Font Info: External font `cmex10' loaded for size LaTeX Font Info: Trying to load font information for U+msa on input line 6.
(Font) <7> on input line 5. (/usr/local/texlive/2025/texmf-dist/tex/latex/amsfonts/umsa.fd
LaTeX Font Info: External font `cmex10' loaded for size File: umsa.fd 2013/01/14 v3.01 AMS symbols A
(Font) <5> on input line 5. )
LaTeX Font Info: Trying to load font information for U+msb on input line 6.
(/usr/local/texlive/2025/texmf-dist/tex/latex/amsfonts/umsb.fd
File: umsb.fd 2013/01/14 v3.01 AMS symbols B
)
Underfull \hbox (badness 10000) in paragraph at lines 4--10
[]
Underfull \hbox (badness 10000) in paragraph at lines 12--14 Underfull \hbox (badness 10000) in paragraph at lines 12--14
[] []
Underfull \hbox (badness 10000) in paragraph at lines 34--39 Underfull \hbox (badness 10000) in paragraph at lines 35--39
[] []
) (./algo/index.tex
[1])
LaTeX Warning: Empty bibliography on input line 38. [1]) (./algo/index.tex) (./proof/index.tex
[2]
[3]
Underfull \hbox (badness 10000) in paragraph at lines 94--95
[]
[2] (./main.aux) [4])
LaTeX Warning: Empty bibliography on input line 60.
[5] (./main.aux)
*********** ***********
LaTeX2e <2024-11-01> patch level 2 LaTeX2e <2024-11-01> patch level 2
L3 programming layer <2025-01-18> L3 programming layer <2025-01-18>
@ -474,18 +552,18 @@ Package logreq Info: Writing requests to 'main.run.xml'.
) )
Here is how much of TeX's memory you used: Here is how much of TeX's memory you used:
12405 strings out of 473190 13334 strings out of 473190
235037 string characters out of 5715806 244064 string characters out of 5715806
1089239 words of memory out of 5000000 1101105 words of memory out of 5000000
35574 multiletter control sequences out of 15000+600000 36455 multiletter control sequences out of 15000+600000
567392 words of font info for 48 fonts, out of 8000000 for 9000 574192 words of font info for 66 fonts, out of 8000000 for 9000
1141 hyphenation exceptions out of 8191 1141 hyphenation exceptions out of 8191
66i,18n,81p,738b,1731s stack positions out of 10000i,1000n,20000p,200000b,200000s 66i,14n,81p,738b,1733s stack positions out of 10000i,1000n,20000p,200000b,200000s
</usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmex10.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi5.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi7.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmr7.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy7.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfbi1000.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfbx0700.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfbx1000.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfbx1200.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfbx1440.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfrm1000.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfrm1200.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfrm1728.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfti1000.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfti1200.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sftt1000.pfb> </usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmex10.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi5.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi7.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmr5.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmr7.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy7.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/symbols/msam10.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfbi1000.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfbx1000.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfbx1200.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfbx1440.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfit1000.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfrm1000.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfrm1200.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfrm1728.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfti0700.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfti1000.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfti1200.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sftt1000.pfb>
Output written on main.pdf (3 pages, 262569 bytes). Output written on main.pdf (6 pages, 341015 bytes).
PDF statistics: PDF statistics:
110 PDF objects out of 1000 (max. 8388607) 134 PDF objects out of 1000 (max. 8388607)
66 compressed objects within 1 object stream 81 compressed objects within 1 object stream
0 named destinations out of 1000 (max. 500000) 0 named destinations out of 1000 (max. 500000)
1 words of extra memory for PDF output out of 10000 (max. 10000000) 1 words of extra memory for PDF output out of 10000 (max. 10000000)

BIN
recherches/ALDLoverAB/main.pdf
View File

Binary file not shown.

BIN
recherches/ALDLoverAB/main.synctex.gz
View File

Binary file not shown.

26
recherches/ALDLoverAB/main.tex
View File

@ -7,11 +7,30 @@
\usepackage[affil-it]{authblk} \usepackage[affil-it]{authblk}
\usepackage{fullpage} \usepackage{fullpage}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{biblatex} \usepackage{biblatex}
\usepackage[linesnumbered,ruled,vlined]{algorithm2e} % \usepackage[linesnumbered,ruled,vlined]{algorithm2e}
\usepackage{algorithm}
\usepackage{algorithmicx}
\usepackage[noend]{algpseudocode}
\algrenewcommand\alglinenumber[1]{\tiny #1}
\newtheorem{theorem}{Property} \usepackage{etoolbox}
% --- Partage du compteur de lignes entre plusieurs algorithmes
\makeatletter
\newcounter{algoLine}
\renewcommand{\alglinenumber}[1]{\arabic{algoLine}}
\newcommand{\nextalgline}{\stepcounter{algoLine}}
\newcommand{\resetalgline}{\setcounter{algoLine}{1}}
\makeatother
\newtheorem{property}{Property}
\newtheorem{theorem}{Theorem}
\newtheorem{proof}{Proof}
\addbibresource{sources.bib} \addbibresource{sources.bib}
@ -35,6 +54,9 @@
\subsection{Algorithms} \subsection{Algorithms}
\input{algo/index.tex} \input{algo/index.tex}
\subsection{proof}
\input{proof/index.tex}
\printbibliography \printbibliography

121
recherches/ALDLoverAB/proof/index.tex Normal file
View File

@ -0,0 +1,121 @@
\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*}