Commit e158a790 authored by Quentin Aristote's avatar Quentin Aristote
Browse files

add appendix

parent bf8379a3
......@@ -524,4 +524,74 @@
% <4> enfin je suis bloqué pour exprimer les bisimulations pour automates de buchi donc ce sera l'objet de recherches futures avec d'autres chercheurs
% <5> ça a quand même mené à une méthode de preuve intéressante dont la formalisation catégorique fera l'objet de futures recherches
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Appendices}
\begin{frame}
\sectionpage
\end{frame}
\begin{frame}
\frametitle{Mesures de progrès}
\[ u_i =_{\eta_i} f_i(\seq{u}{m}) \quad \rightarrow \quad (p_i(\seq{\alpha}{k}))_{\seq{\alpha}{k}}\]
\begin{itemize}
\item \textbf{(monotonicité)} si $(\seq{\alpha}{k}) \prec_i (\seq{\beta}{k})$,
\[ p_i(\seq{\alpha}{k}) \sqsubseteq p_i(\seq{\beta}{k}) \]
\item \textbf{($\boldsymbol{\mu}$)} si $\eta_i = \mu$,
\[
p_i(\seq{\alpha}{k}) \sqsubseteq f_i
\begin{pmatrix}
\bigsqcup_{(\seq{\beta}{k}) \prec_i (\seq{\alpha}{k})} p_1(\seq{\beta}{k}) \\
\vdots \\
\bigsqcup_{(\seq{\beta}{k}) \prec_i (\seq{\alpha}{k})} p_m(\seq{\beta}{k})
\end{pmatrix}
\]
\item \textbf{($\boldsymbol{\nu}$)} si $\eta_i = \nu$,
\[
p_i(\seq{\alpha}{k}) \sqsubseteq f_i
\begin{pmatrix}
\bigsqcup_{(\seq{\beta}{k}) \preceq_i (\seq{\alpha}{k})} p_1(\seq{\beta}{k}) \\
\vdots \\
\bigsqcup_{(\seq{\beta}{k}) \preceq_i (\seq{\alpha}{k})} p_m(\seq{\beta}{k})
\end{pmatrix}
\]
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{Ébauche de preuve du théorème}
\begin{enumerate}
\item $P \sqsubseteq l_i^\mathrm{sol}$
\vspace{10pt}
\item il existe $(\seq{\alpha}{k})$ t.q. $P \sqsubseteq p_i(\seq{\alpha}{k})$
\vspace{10pt}
\item il existe $(\seq{\alpha}{k})$ t.q. $(i,P,(\seq{\alpha}{k}))$ est gagnante dans le jeu de parité à codensité \emph{avec ordinaux}
\vspace{10pt}
\item $(i,P)$ est gagnante dans le jeu de parité à codensité
\end{enumerate}
\end{frame}
\begin{frame}
\frametitle{Un autre jeu pour les systèmes d'équations \tiny
[Baldan+, CONCUR'20]}
\begin{align*}
u_1 &=_{\eta_1} f_1(\seq{u}{m}) \\
\vdots& \\
u_m &=_{\eta_m} f_m(\seq{u}{m})
\end{align*}
\begin{table}[h]
\centering
\begin{tabular}{c c c c}
Position & Joueur & Coups possibles & Priorité \\
\toprule
\makecell{$i \in [1,m]$ \\ $P \in \mathbb{C}_X$} & \textcolor{blue}{\DejaSans 😇} & \makecell{$G \subseteq \mathbb{C}_X$ t.q. \\ $P \sqsubseteq f_i\left(\bigsqcup G\right)$} & $i$ \\
\midrule
$G \subseteq \mathbb{C}_X$ & \textcolor{purple}{\DejaSans 😈} & $Q \in G$ & $0$ \\
\bottomrule
\end{tabular}
\end{table}
\end{frame}
\end{document}
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment