From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 11 Oct 2005 13:20:11 +0000 (+0000)
Subject: fixed some typos
X-Git-Tag: V_0_7_2_3~220
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d928ebab750b6ac49b3ae97e2f9d1634c18a43fa;p=helm.git

fixed some typos
---

diff --git a/helm/papers/system_T/Makefile b/helm/papers/system_T/Makefile
new file mode 100644
index 000000000..fb2792fc5
--- /dev/null
+++ b/helm/papers/system_T/Makefile
@@ -0,0 +1,5 @@
+all:
+		latex t
+		latex t
+		latex t
+		dvips -ta4 t
diff --git a/helm/papers/system_T/t.tex b/helm/papers/system_T/t.tex
index d3ca4e6a1..d6a1b6de1 100644
--- a/helm/papers/system_T/t.tex
+++ b/helm/papers/system_T/t.tex
@@ -7,6 +7,9 @@
 
 \newcommand{\sem}[1]{[\![ #1 ]\!]}
 \newcommand{\R}{\,\mathscr{R}\,}
+\newcommand{\N}{\,\mathbb{N}\,}
+\newcommand{\NT}{\,\mathbb{N}\,}
+\newcommand{\NH}{\,\mathbb{N}\,}
 \title{...}
 \author{...}
 
@@ -36,7 +39,7 @@
 \item $plus\_O:\forall x.x+0=x$
 \item $plus\_S:\forall x,y.x+S(y)=S(x+y)$ 
 \item $times\_O:\forall x.x*0=0$
-\item $timies\_S:\forall x,y.x*S(y)=x+(x*y)$ 
+\item $times\_S:\forall x,y.x*S(y)=x+(x*y)$ 
 \end{itemize}
 
 \noindent
@@ -59,7 +62,7 @@
 
 \[ 
    (\forall_i)\frac{\Gamma \vdash M:P}{\Gamma \vdash 
-   \lambda x:N.M: \forall x.P}(*) \hspace{2cm}
+   \lambda x:\N.M: \forall x.P}(*) \hspace{2cm}
    (\forall_e)\frac{\Gamma \vdash M :\forall x.P}{\Gamma \vdash M t: P[t/x]} 
 \]
 
@@ -76,8 +79,8 @@
 \item $\sem{A} = 1$ if A is atomic
 \item $\sem{A \land B} = \sem{A}\times \sem{B}$
 \item $\sem{A \to B} = \sem{A}\to \sem{B}$
-\item $\sem{\forall x.P} = N \to \sem{P}$
-\item $\sem{\exists x.P} = N \times \sem{P}$
+\item $\sem{\forall x.P} = \N \to \sem{P}$
+\item $\sem{\exists x.P} = \N \times \sem{P}$
 \end{itemize}
 
 definition.
@@ -91,24 +94,24 @@ For any type T of system T $\bot_T: 1 \to T$  is inuctively defined as follows:
 
 \begin{itemize}
 \item $\sem{nat\_ind} = R$
-\item $\sem{ex\_ind} = (\lambda f:(N \to \sem{P} \to \sem{Q}).
-\lambda p:N\times \sem{P}.f (fst \,p) (snd \,p)$. 
-\item $\sem{ex\_intro} = \lambda x:N.\lambda f:\sem{P}.<x,f>$
+\item $\sem{ex\_ind} = (\lambda f:(\N \to \sem{P} \to \sem{Q}).
+\lambda p:\N\times \sem{P}.f (fst \,p) (snd \,p)$. 
+\item $\sem{ex\_intro} = \lambda x:\N.\lambda f:\sem{P}.<x,f>$
 \item $\sem{fst} = fst$
 \item $\sem{snd} = snd$
 \item $\sem{conj} = \lambda x:\sem{P}.\lambda y:\sem{Q}.<x,y>$
 \item $\sem{false\_ind} = \bot_{\sem{Q}}$
-\item $\sem{discriminate} = \lambda \_:N.\lambda \_:1.*$
-\item $\sem{injS}= \lambda \_:N. \lambda \_:N.\lambda \_:1.*$
-\item $\sem{plus\_O} = \sem{times\_O} = \lambda \_:N.*$
-\item $\sem{plus\_S} = \sem{times_S} = \lambda \_:N. \lambda \_:N.*$
+\item $\sem{discriminate} = \lambda \_:\N.\lambda \_:1.*$
+\item $\sem{injS}= \lambda \_:\N. \lambda \_:\N.\lambda \_:1.*$
+\item $\sem{plus\_O} = \sem{times\_O} = \lambda \_:\N.*$
+\item $\sem{plus\_S} = \sem{times_S} = \lambda \_:\N. \lambda \_:\N.*$
 \end{itemize}
 
 In the case of structured proofs:
 \begin{itemize}
 \item $\sem{M N} = \sem{M} \sem{N}$
 \item $\sem{\lambda x:A.M} = \lambda x:\sem{A}.\sem{M}$
-\item $\sem{\lambda x:N.M} = \lambda x:N.\sem{M}$
+\item $\sem{\lambda x:\N.M} = \lambda x:\N.\sem{M}$
 \item $\sem{M t} = \sem{M} \sem{t}$
 \end{itemize}
 
@@ -125,7 +128,7 @@ In particular:
 \end{itemize}
 
 \noindent
-We proceed to prove that alla axioms $ax:Ax$ are realized by $\sem{ax}$.
+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