From 8aad1acb7c14493e78888722ce93d9b9c96c9f76 Mon Sep 17 00:00:00 2001 From: Guillaume GENESTIER Date: Thu, 20 Jun 2019 11:43:04 +0200 Subject: [PATCH] Majuscules --- Slides/SlidesFSCD.tex | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/Slides/SlidesFSCD.tex b/Slides/SlidesFSCD.tex index 660e2d6..b73e1d2 100644 --- a/Slides/SlidesFSCD.tex +++ b/Slides/SlidesFSCD.tex @@ -294,7 +294,7 @@ def sum : (n: Nat) -> F n \newcommand{\ens}[1]{\left\{#1\right\}} \newcommand{\enscond}[2]{\ens{\left.\vphantom{#2}#1\right|#2}} -\section{Termination criterion} +\section{Termination Criterion} \begin{frame}\frametitle{Main Goal} @@ -303,7 +303,7 @@ def sum : (n: Nat) -> F n \LARGE If $\Gamma\vdash t:T$, then $t\in\mathrm{SN}(\to_{\beta\mathcal{R}})$. \end{frame} -\subsection{Logical relation} +\subsection{Logical Relations} \begin{frame}\frametitle{Logical Relations} \begin{block}{Goal} @@ -394,7 +394,7 @@ $\color{red}{(3)}$ append _ (cons x p l) q m $\color{red}{>}$ p + q \end{frame} -\begin{frame}[fragile]\frametitle{Call-graph: Example} +\begin{frame}[fragile]\frametitle{Call-Graph: Example} \begin{lstlisting}[mathescape=true] def plus : Nat -> Nat -> Nat. set infix "+" := plus. @@ -423,15 +423,15 @@ def append: (p: Nat) -> List p -> \end{center} \end{frame} -\subsection{Well-structuring} +\subsection{Well-Structuring} -\begin{frame}\frametitle{Well-structuring} +\begin{frame}\frametitle{Well-Structuring} \begin{block}{} $\succeq$ quasi-order on the signature compatible with rewriting and typing. \end{block} -\begin{definition}[Well-structured system]\label{def-well-struct} +\begin{definition}[Well-Structured System]\label{def-well-struct} $\mathcal{R}$ is \emph{well-structured} if for all rule $(\Delta,f\,\bar l\to r)$, with $\Theta_f=\Pi(\bar x:\bar T).U$, we have $\Delta\vdash_{\!\!\preceq f} r:U[\bar x\to \bar l]$. @@ -475,7 +475,7 @@ def append: (p: Nat) -> List p -> \subsection{Size-Change Termination} -\begin{frame}[fragile]\frametitle{Call-graph: Example} +\begin{frame}[fragile]\frametitle{Call-Graph: Example} \begin{lstlisting}[mathescape=true] def plus : Nat -> Nat -> Nat. set infix "+" := plus. -- 2.24.1