From 71c9c97dfca2393bd6d90ea45f6d2e4e6ae15793 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 12 Oct 2005 11:31:10 +0000 Subject: [PATCH] few more cases --- helm/papers/system_T/t.tex | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/helm/papers/system_T/t.tex b/helm/papers/system_T/t.tex index fc6b1bd1e..1e1b6c46c 100644 --- a/helm/papers/system_T/t.tex +++ b/helm/papers/system_T/t.tex @@ -156,6 +156,18 @@ We proceed to prove that all axioms $ax:Ax$ are realized by $\sem{ax}$. 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 $ex\_intro$. + We must prove that + $$\lambda x:\N.\lambda f:\sem{P}. \R \forall x.(P\to\exists x.P(x)$$ + that leads to prove that foreach n + $\underline{ex\_into}~n \R (P\to\exists x.P(x))[\underline{n}/x]$.\\ + Evaluating the substitution we have + $\underline{ex\_into}~n \R (P[\underline{n}/x]\to\exists x.P(x))$.\\ + Again by definition of $\R$ we have to prove that given a + $m \R P[\underline{n}/x]$ then $\underline{ex\_into}~n~m \R \exists x.P(x)$. + Expanding the definition of $\underline{ex\_intro}$ we have + $ \R \exists x.P(x)$ that is true since $m \R P[\underline{n}/x]$. + \item $false\_ind$. We have to prove that $\bot_{\sem{Q}} \R \bot \to Q$. Trivial, since there is no $m \R \bot$. @@ -164,6 +176,14 @@ We proceed to prove that all axioms $ax:Ax$ are realized by $\sem{ax}$. 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. +\item $injS$. + We have to prove that for each $n_1$ and $n_2$\\ + $\lambda \_:\N. \lambda \_:\N.\lambda \_:1.*~n_1~n_2 \R + (S(x)=S(y)\to x=y)[n_1/x][n_2/y]$.\\ + Assuming $m \R S(n_1)=S(n_2)$ we have to prove + + + \end{itemize} \begin{thebibliography}{} -- 2.39.2