added few cases

diff --git a/helm/papers/system_T/t.tex b/helm/papers/system_T/t.tex
index d6a1b6de1b4799fb01b098c6a78565510627916a..fc6b1bd1e66a382736cb9542a84ae0737640c938 100644 (file)
--- a/helm/papers/system_T/t.tex
+++ b/helm/papers/system_T/t.tex
@@ -6,7 +6,7 @@
 %\usepackage{picins}
 
 \newcommand{\sem}[1]{[\![ #1 ]\!]}
-\newcommand{\R}{\,\mathscr{R}\,}
+\newcommand{\R}{\;\mathscr{R}\;}
 \newcommand{\N}{\,\mathbb{N}\,}
 \newcommand{\NT}{\,\mathbb{N}\,}
 \newcommand{\NH}{\,\mathbb{N}\,}
@@ -131,17 +131,39 @@ In particular:
 We proceed to prove that all axioms $ax:Ax$ are realized by $\sem{ax}$.
 
 \begin{itemize}
-\item $nat\_ind$. We must prove that the recursion schema $R$ realizes the 
-induction principle. To this aim we must prove that for any $a$ and $f$ such that
-$a \R P(0)$ and  $f \R \forall x.(P(x) \to P(S(x)))$, and any natural number 
-$n$, $(R \,a \,f \,n) \R P(\underline{n})$.\\
-We proceed by induction on n.\\
-If $n=O$, $(R \,a \,f \,O) = a$ and by hypothesis $a \R P(0)$.\\
-Suppose by induction that $(R \,a \,f \,n) \R P(\underline{n})$, and let us prove that
-the relation still holds for $n+1$. 
-By definition $(R \,a \,f \,(n+1)) = f \,n \,(R \,a \,f \,n)$, 
-and since $f \R \forall x.(P(x) \to P(S(x)))$,  
-$(f n (R a f n)) \R P(S(\underline{n}))=P(\underline{n+1})$.
+\item $nat\_ind$. 
+  We must prove that the recursion schema $R$ realizes the induction principle.
+  To this aim we must prove that for any $a$ and $f$ such that $a \R P(0)$ and
+  $f \R \forall x.(P(x) \to P(S(x)))$, and any natural number $n$, $(R \,a \,f
+  \,n) \R P(\underline{n})$.\\ 
+  We proceed by induction on n.\\ 
+  If $n=O$, $(R \,a \,f \,O) = a$ and by hypothesis $a \R P(0)$.\\ 
+  Suppose by induction that
+  $(R \,a \,f \,n) \R P(\underline{n})$, and let us prove that the relation
+  still holds for $n+1$.  By definition 
+  $(R \,a \,f \,(n+1)) = f \,n \,(R \,a \,f \,n)$, 
+  and since $f \R \forall x.(P(x) \to P(S(x)))$,  
+  $(f n (R a f n)) \R P(S(\underline{n}))=P(\underline{n+1})$.
+
+\item $ex\_ind$. 
+  We must prove that $$\underline{ex\_ind} \R (\forall x:(P x)
+  \to Q) \to (\exists x:(P x)) \to Q$$ Following the definition of $\R$ we have
+  to prove that given\\ $f~\R~\forall~x:((P~x)~\to~Q)$ and
+  $p~\R~\exists~x:(P~x)$, then $\underline{ex\_ind}~f~p \R Q$.\\ 
+  $p$ is a couple $<n_p,g_p>$ such that $g_p \R P[\underline{n_p}/x]$, while
+  $f$ is a function such that forall $n$ and for all $m \R P[\underline{n}/x]$
+  then $f~n~m \R Q$.  Exapanding the definition of $\underline{ex\_ind}$, $fst$
+  and $snd$ we obtain $f~n_p~g_p$ that we know is in relation $\R$ with $Q$
+  since $g_p \R P[\underline{n_p}/x]$.
+
+\item $false\_ind$. 
+  We have to prove that $\bot_{\sem{Q}} \R \bot \to Q$. 
+  Trivial, since there is no $m \R \bot$.
+
+\item $discriminate$. 
+  Since there is no $n$ such that $0 = S n$ is true... \\
+  $\underline{discriminate}~n \R 0 = S~\underline{n} \to \bot$ for each n.
+
 \end{itemize}
 
 \begin{thebibliography}{}