From c9b7cd573efcb687d5d0e225bf3990b656446dc6 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 8 Nov 2005 14:59:53 +0000 Subject: [PATCH] fix --- helm/papers/system_T/t.tex | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/helm/papers/system_T/t.tex b/helm/papers/system_T/t.tex index 77b159fff..14ead6b91 100644 --- a/helm/papers/system_T/t.tex +++ b/helm/papers/system_T/t.tex @@ -453,9 +453,9 @@ 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 +In the induction step we have as induction hypothesis that for each recursive +argument $t_i$ of the head constructor $c_i$, $r_i\equiv +\Rx~\vec{f}~t_i \R Q(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 -- 2.39.2