Commit 9d1d3259 authored by Guillaume GENESTIER's avatar Guillaume GENESTIER

k

parent ec4d67e4
......@@ -23,7 +23,7 @@
\begin{cond}{cond-symb-order-wf}
$\sqsubset$ is well-founded.
\todo{Note that it is free if $\Func$ is finite.}
\end{cond}
......@@ -40,7 +40,7 @@
\AxiomC{$g\sqsubset f$}
\BinaryInfC{$\G\vdash_{\sqsubset f}g:\tau(g)$}
\end{prooftree}
Note that it introduces predicates well-formed${}_{\sqsubset f}$.
\begin{center}
\begin{tabular}{rcl}
......@@ -168,14 +168,18 @@
we have that $\rew_{arg}\cup{\call}$ terminates on $\mbb{U}$.
We now prove that, $f\,\bar t\in\interp{T'\pi}$ by induction on ${\rew_{arg}}\cup{\call}$.
Because of the assumptions we have on rules, $f\,\bar t$ is neutral.
Hence, it suffices to prove that,
for all $u$ such that $f\,\bar t\rew u$, we have $u\in\interp{T'\pi}$.
There are two cases:
\begin{itemize}
\item $u=f\bar u$ with $\bar t\rew\bar u$.
\begin{itemize}
\item
If $f\in\FObj\setminus\CObj$, $f\,\bar t$ is neutral.
Hence, it suffices to prove that,
for all $u$ such that $f\,\bar t\rew u$, we have $u\in\interp{T'\pi}$.
There are two cases:
\begin{itemize}
\item
$u=f\,\bar u$ with $f\,\bar t\rew_{arg}f\,\bar u$.
Then, we can conclude by induction hypothesis.
\item There are $fl_1\dots l_k\rul r\in\mcal{R}$ and $\sg$ such that
\item
There are $fl_1\dots l_k\rul r\in\mcal{R}$ and $\sg$ such that
$u=(r\sg)\,t_{k+1}\dots t_n$ and,
for all $i\in\{1,\dots,k\}$, $t_i=l_i\sg$.
Then, $\crochet{\overline{\sur{l}{x}}}\sg\vDash\G$.
......@@ -183,11 +187,17 @@
We now prove that, for all $\G$, $u$ and $U$, if $\G\vdash_{f\bar l} u:U$ and
$\sg\vDash\G$, then $u\sg\in\interp{U\sg}$.
The proof is the same as for \indthm{TypImpliInterp} except for (fun) replaced by (fun').
In this case, for all $i$, we have $\G\vdash_{f\bar l} u_i:U_i\g$.
By induction hypothesis, $u_i\sg\in\interp{U_i\g\sg}$.
So, $\g\sg\vDash\Sg$ and $g\,\bar u\sg\in\mbb{U}$.
Now, $g\,\bar u\sg\tilde{<}f\,\bar l\sg$ since $g\,\bar u<f\,\bar l$.
Therefore, by induction hypothesis, $g\,\bar u\sg\in\interp{V\g\sg}$.
\end{itemize}
The proof is the same as for \indthm{thm-adequacy} except for (fun) replaced by (dp).
\begin{description}
\item[(dp)]
In this case, for all $i$, we have $\G\vdash_{f\bar l} u_i:U_i\g$.
By induction hypothesis, $u_i\sg\in\interp{U_i\g\sg}$.
So, $\g\sg\vDash\Sg$ and $g\,\bar u\sg\in\mbb{U}$.
Now, $g\,\bar u\sg\tilde{<}f\,\bar l\sg$ since $g\,\bar u<f\,\bar l$.
Therefore, by induction hypothesis, $g\,\bar u\sg\in\interp{V\g\sg}$.
\end{description}
\end{itemize}
\item
If $f\in\CObj$, then $T'=C\,\bar u$ with $C\in\CTyp$.
\end{itemize}
\end{proof}
\usepackage[T1]{fontenc} %Permet d'imprimer les caractères spéciaux
\usepackage[utf8]{inputenc} %Permet de taper directement les caractères spéciaux dans le fichier Tex
\usepackage[francais]{babel} %Écrit Démonstration et non Proof
\frenchbsetup{StandardLists=true} %Met des puces rodes plutôt que des - pour les listes
\usepackage[english]{babel} %Écrit Démonstration et non Proof
%\frenchbsetup{StandardLists=true} %Met des puces rodes plutôt que des - pour les listes
\usepackage{amsthm} %Permet de définir les différents types de théorèmes, remarques...
\usepackage{amssymb} %Ajoute \mathbb
......@@ -23,7 +23,7 @@
\usepackage[toc,page]{appendix} % Pour gérer les annexes
\bibliographystyle{apalike} % Type de bibliographie
\usepackage{multirow}
\usepackage{imakeidx}
%\usepackage{imakeidx}
\usepackage[refpage]{nomencl}
\usepackage{listings}
\usepackage{enumitem}
......@@ -34,24 +34,24 @@
\usepackage{diagbox}
\theoremstyle{plain}
\newtheorem{thm}{Th\'{e}or\`{e}me}[section]
\newtheorem{thm}{Theorem}[section]
\newtheorem{propo}[thm]{Proposition}
\newtheorem{coro}[thm]{Corollaire}
\newtheorem{lem}[thm]{Lemme}
\newtheorem{propri}[thm]{Propri\'et\'e}
\newtheorem{propris}[thm]{Propri\'et\'es}
\newtheorem{defi}[thm]{D\'efinition}
\newtheorem{algo}[thm]{Algorithme}
\newtheorem{coro}[thm]{Corollary}
\newtheorem{lem}[thm]{Lemma}
\newtheorem{propri}[thm]{Property}
\newtheorem{propris}[thm]{Properties}
\newtheorem{defi}[thm]{Definition}
\newtheorem{algo}[thm]{Algorithm}
\theoremstyle{definition}
\newtheorem{exo}[thm]{Exercice}
\newtheorem{exo}[thm]{Exercise}
\theoremstyle{remark}
\newtheorem*{nots}{Notations}
\newtheorem*{rmq}{Remarque}
\newtheorem*{expl}{Exemple}
\newtheorem*{expls}{Exemples}
\newtheorem{sub}{But local}
\newtheorem{rest}{But restant}
\newtheorem*{locProof}{Démonstration}
\newtheorem*{rmq}{Remark}
\newtheorem*{expl}{Example}
\newtheorem*{expls}{Examples}
\newtheorem{sub}{Local goal}
\newtheorem{rest}{Remaining goal}
\newtheorem*{locProof}{Proof}
\newcommand{\sur}[2]{\raisebox{0.4ex}{$#1$} / \raisebox{-0.7ex}{$#2$}}
......
Markdown is supported
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