-
-\subsection{$R_X : \sem{X_{ind}}$ and $R_X\R X_{ind}$}
-We have to compare the definition of $\square$ and $\vartriangle$
-since thay play the same role in constructing respectively $R_X$ and
-$X_{ind}$. If we assume $\alpha = \sem{Q}$ and we apply the $\sem$
-function to each righ side of the $\vartriangle$ definition we obtain
-exactly $\square$. The last two elements of the arrows $R_X$ and
-$X_{ind}$ are again the same up to $\sem$.
-
-questa non va bene, il caso base e' se il tipo del costruttore usa
-solo le prime 2 regole di delta, quello induttivo se usa ANCHE la
-terza...
-
-To prove that $R_X\R X_{ind}$ we must assume that for each $i$ index
-of a constructor of $X$, $f_i \R \vartriangle\{C(X)_i, c_i\}$ and we
-have to proove that for each $t:X$
-$$R_X~\overrightarrow{f}~t \R Q(t)$$.
-We proceede by induction on the type of the head constructor $c_i$ in $t$.
-The first base case is $c_i=X$ that, according to $\triangledown$,
-reduces in one
-step to $f_i$ and by hypothesis we have $f_i \R \vartriangle\{X,
-c_i\}$. Unfolding $\vartriangle$ we have $f_i \R Q(c_i)$. The second
-base case is $c_i=\overrightarrow{\forall t:T}.X$ and is analoug to
-the first case.\\
-The inductive step is when we have one or more recursive aruments in
-$c_i$ and the induction hypothesis is that for each recursve argument
-$m$, $R_X~\overrightarrow{f}~m \R X \to Q$. Since $f_i \R
-\vartriangle\{C(X)_i, c_i\}$ and
-$R_X~\overrightarrow{f}~(c_i~\overrightarrow{m})$ reduces to
-$f_i~\overrightarrow{...}$
-
-
-
-
-
-
+We assume $\Rx~\vec{f}~(c_i~\vec{m})$ is well typed, so in the first case we
+can omit $\vec{m}$ since it is an empty sequence.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsection{Realizability of the induction principle}
+Once we have inductive types and their induction principle we want to show that
+the recursor $\Rx$ realizes $\Xind$, that is that $\Rx$ has type
+$\sem{\Xind}$ and is in relation $\R$ with $\Xind$.
+
+\begin{thm}$\Rx : \sem{\Xind}$\end{thm}
+\begin{proof}
+We have to compare the definition of $\square$ and $\triUP$
+since they play the same role in constructing respectively the types of
+$\Rx$ and
+$\Xind$. If we assume $\alpha = \sem{Q}$ and we apply the $\sem{\cdot}$
+function to each right side of the $\triUP$ definition we obtain
+exactly $\square$. The last two elements of the arrows $\Rx$ and
+$\Xind$ are again the same up to $\sem{\cdot}$.
+\end{proof}
+
+\begin{thm}$\Rx\R \Xind$\end{thm}
+\begin{proof}
+To prove that $\Rx\R \Xind$ we must assume that for each $i$ index
+of a constructor of $X$, $f_i \R \triUP\{C(X)_i, c_i\}$ and we
+have to prove that for each $t:X$
+$$\Rx~\vec{f}~t \R Q(t)$$
+\noindent
+We proceed by induction on the structure of $t$.
+\\
+The base case is when the
+type of the head constructor of $t$ has no recursive arguments (i.e. the type
+is generated using only the first two rules $C(X)$), so
+$(\Rx~\vec{f}~(c_i~\vec{m}))$ reduces in one step to $(f_i~\vec{m})$. $f_i$
+realizes $\triUP\{C(X)_i, c_i\}$ by assumption and since we are in the base
+case $\triUP\{C(X)_i, c_i\}$ is of the form $\vec{\forall t:T}.Q(c_i~\vec{t})$.
+Thus $f_i~\vec{m} \R Q(c_i~\vec{m})$.
+\\
+In the induction step we have as induction hypothesis that each recursive
+argument $t_i$ of the head constructor $c_i$ is realized by $r_i\equiv
+\Rx~\vec{f}~t_i$. By the third rule of $\triDOWN$ we obtain the reduct
+$f_i~\vec{m}~\vec{t~r}$ (here we write first all the non recursive arguments,
+then all the recursive one. In general they can be mixed and the proof is
+exactly the same but the notation is really heavier). We know by hypothesis
+that $f_i \R \triUP\{C(X)_i, c_i\} \equiv \vec{\forall m:T}.\vec{\forall
+t:X.Q(t)} \to Q(c_i~\vec{m}~\vec{t})$, thus $f_i~\vec{m}~\vec{t~r} \R
+Q(c_i~\vec{m}~\vec{t})$.
+\end{proof}
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%