One more lemma

diff --git a/notes.tex b/notes.tex
index c4e4cfdfa015e5296236c1ca136055b46a685691..81c92808e09d3e51a1753fafad826513b89aa7fa 100644 (file)
--- a/notes.tex
+++ b/notes.tex
@@ -281,19 +281,6 @@
   with $|\vec\var| = i$ and $|\vec\alpha| = j$.\r
 \end{definition}\r
 \r
-{\color{yellow}\begin{definition}[Good permutation]\r
-  Let $\tm$ a \knnf.\r
-  $\Perm i j$ is \emph{good} for $\tm$ if\r
-  $i<\Args\tm$ and $j \geq \xK + i + 1$.\r
-\end{definition}}\r
-\r
-% \begin{lemma}\r
-%   Let $\tm$ in nf.\r
-%   Let $\vec\alpha$ fresh variables.\r
-%   If $|\vec\alpha|\geq \lams\tm$,\r
-%   then the normal form of $\tm\,\vec\alpha$ is inert.\r
-% \end{lemma}\r
-\r
 \begin{lemma}[Monotonicity]\label{l:k-nf-mono}\r
   If $\tm$ is a \knnf{}, then it is also a $\xK'$-nf\r
   for every $\xK' \geq \xK{}$.\r
@@ -314,7 +301,7 @@
     \item Case $\varthree=\var$ and $i<|\vec\tmtwo|$:\r
      $\tm\sigma \to^* \lambda\vec\vartwo.\, (\tmtwo_i\sigma)\vec\alpha \vec{(\tmtwo\sigma)} $.\r
      Now, by \ih{} $\nf{\tmtwo_i\sigma}$ is a $\xK'$-nf, and since $|\vec\alpha|\geq\xK'$,\r
-     $\nf{(\tmtwo_i\sigma\vec\alpha)}$ is inert (\textcolor{red}{Serve lemma?}).\r
+     $\nf{(\tmtwo_i\sigma\vec\alpha)}$ is inert.\r
      Therefore $\nf\tm = \lambda\vec\vartwo.\,\nf{(\tmtwo_i\sigma\vec\alpha)} \vec{(\nf{\tmtwo\sigma})}$,\r
      and again by \ih{} it is also a $\xK'$-nf.\r
     \item Case $\varthree=\var$ and $i \geq |\vec\tmtwo|$:\r
@@ -325,6 +312,19 @@
   \r
 \end{proof}\r
 \r
+\begin{lemma}[Admissible]\r
+  Let $\tm$ an inert \knnf.\r
+  If $i<\Args\tm$ and $j \geq \xK + i + 1$\r
+  then $\nf{\tm\Subst{\HeadOf\tm}{\Perm i j}}$\r
+  is inert.\r
+\end{lemma}\r
+\begin{proof}\r
+  Let $\tm = \var\,\vec a$, $\perm \defeq \Perm i j$, and $\sigma\defeq\Subst\var\perm$.\r
+  Then $\nf{\tm\Subst\var\perm} = \nf{(a_i\sigma\,\vec\alpha\,\vec {(a\sigma)})}$.\r
+  By \reflemma{k-prime-nf} $\nf{a_i\sigma}$ is a $\xK'$-nf with $\xK'\defeq \xK+i+1$.\r
+  Therefore $\nf{(a_i\sigma\vec\alpha)}$ is inert because $|\vec\alpha|=j\geq\xK'$.\r
+\end{proof}\r
+\r
 % \begin{lemma}\r
 %   Let $\tm$ a \knnf, and $\Head\tm=\var$.\r
 %   If $i<\Args\tm$ and $j \geq \xK + i + 1$,\r
@@ -349,26 +349,35 @@
   For every \knnf s $\tm$,\r
   every fresh variable $\var$,\r
   every $\perm\defeq\Perm{i}{j}$ permutator with $j>\xK+i+1$:\r
-  $\nf{\tm\Subst\var\perm\vec\alpha} \EtaNeq \alpha_j$.\r
+  $\nf{(\tm\Subst\var\perm\vec\alpha)} = \tmtwo \, \alpha_j$\r
+  for some inert $\tmtwo$.\r
 \end{lemma}\r
 \begin{proof}\r
   First of all note that by \reflemma{k-prime-nf}\r
   $\nf{\tm\Subst\var\perm}$ is a $\xK'$-nf for $\xK' \defeq \xK+i+1$, therefore\r
-  $\nf{\tm\Subst\var\perm\vec\alpha}$ is inert because $|\vec\alpha|>\xK'$ by hypothesis.\r
+  $\nf{(\tm\Subst\var\perm\vec\alpha)}$ is inert because $|\vec\alpha|>\xK'$ by hypothesis.\r
   \r
-  By structural induction on $\tm$.\r
-  Let $\tm = \lambda\vec\vartwo.\, h\,\vec a$ for $|\vec\vartwo|\leq\xK$.\r
-  \TODO{}\r
+  More precisely, $\nf{(\tm\Subst\var\perm\,\alpha_1\cdots\alpha_{\xK'})}$ is inert,\r
+  and therefore $\nf{(\tm\Subst\var\perm\vec\alpha)} = \nf{(\tm\Subst\var\perm\,\alpha_1\cdots\alpha_{\xK'})}\,\alpha_{\xK'+1}\cdots\alpha_j$,\r
+  and we conclude.\r
 \end{proof}\r
 \r
-% TODO: $\xK$-standard proof of $\eta$.\r
-\r
 \begin{lemma}\r
+  For every \knnf s $\tm$,\r
+  every fresh variable $\var$,\r
+  every $\perm\defeq\Perm{i}{j}$ permutator with $j>\xK+i+1$:\r
+  $\nf{(\tm\Subst\var\perm)} \EtaNeq \alpha_j$.\r
+\end{lemma}\r
+\begin{proof}\r
+  \TODO{}\r
+\end{proof}\r
+\r
+\begin{theorem}\r
   For every \knnf s $\tm$ and $\tmtwo$,\r
   every fresh variable $\var$,\r
   $\perm\defeq\Perm{i}{j}$ permutator with $j>\xK+i+1$,\r
   $\tm\EtaEq\tmtwo$ iff $\nf{\tm\Subst\var\perm}\EtaEq\nf{\tmtwo\Subst\var\perm}$.\r
-\end{lemma}\r
+\end{theorem}\r
 \begin{proof}\r
   Let $\sigma \defeq \Subst\var\perm$.\r
   First of all, note that by \reflemma{k-prime-nf}\r
@@ -380,7 +389,7 @@
   $\nf{\tm\sigma}\EtaNeq\nf{\tmtwo\sigma}$.\r
   Let $\tm \EtaEq \lambda\vec\vartwo.\, h_1\,\vec a$ and \r
   $\tmtwo \EtaEq \lambda\vec\vartwo.\, h_2\,\vec b$,\r
-  with $|\vec\vartwo| = \xK$ {\color{red}[Capire perche' si puo' $\xK$-$\eta$-espandere qui]}.\r
+  with $|\vec a|,|\vec b| > i$ {\color{red}[Capire perche' si puo' $\eta$-espandere qui]}.\r
   By (course-of-value) induction on the size of $\tm$ and $\tmtwo$,\r
   and by cases on the definition of eta-difference:\r
   \begin{itemize}\r
@@ -392,6 +401,7 @@
        and therefore $\nf{\tm\sigma} \EtaNeq \nf{\tmtwo\sigma}$ because\r
        their head variables are different.\r
       \item $h_1=\var$ and $h_2\neq \var$: \TODO\r
+       $\nf{\tmtwo\sigma} = \nf{(\lambda\vec\vartwo.\,h_2\,\vec b)\sigma} = \lambda\vec\vartwo.\,h_2\,\vec{(\nf{b\sigma})}$\r
       \item $h_1\neq\var$ and $h_2=\var$: symmetric to the case above.\r
     \end{itemize}\r
     \item $h_1 = h_2$ and $|\vec a| \neq |\vec b|$:\r