Proved another lemma (aux1 + aux2)

diff --git a/macros.tex b/macros.tex
index 5e151cc18eef3e7b032943819266ef7f6a32127f..4c30e1512cda8f659a4ff7d3a1c5a6677d6ba808 100644 (file)
--- a/macros.tex
+++ b/macros.tex
@@ -87,4 +87,6 @@
 \r
 \renewcommand{\Lam}[2]{\lambda#1.\, \{\!\!\{#2\}\!\!\}}\r
 \renewcommand{\vec}{\overrightarrow}\r
-\newcommand{\reflemma}[1]{Lemma~\ref{l:#1}}
\ No newline at end of file
+\newcommand{\reflemma}[1]{Lemma~\ref{l:#1}}\r
+\newcommand{\head}{h}\r
+\newcommand{\args}{a}\r

diff --git a/notes.tex b/notes.tex
index 81c92808e09d3e51a1753fafad826513b89aa7fa..3dd97d13033ed783b6287ff312fb9ba330de46e4 100644 (file)
--- a/notes.tex
+++ b/notes.tex
@@ -291,23 +291,23 @@
   Then for every $j \geq \xK'$, $\nf{\tm\Subst\var{\Perm i j}}$ is defined and it is a $\xK'$-nf.\r
 \end{lemma}\r
 \begin{proof}\r
-  By (course-of-value) structural induction on $\tm$.\r
-  Let $\tm=\lambda\vec\vartwo.\,\varthree\,\vec\tmtwo$ and $\sigma\defeq\Subst\var{\Perm i j}$.\r
+  By induction on $|\tm|$.\r
+  Let $\tm=\lambda\vec\vartwo.\,\head\,\vec\args$ and $\sigma\defeq\Subst\var{\Perm i j}$.\r
   By cases:\r
   \begin{itemize}\r
-    \item Case $\varthree\neq\var$: $\nf{(\lambda\vec\vartwo.\,\varthree\,\vec\tmtwo)\sigma} = \lambda\vec\vartwo.\,\varthree\,\vec{(\nf{\tmtwo\sigma})}$.\r
-    By \ih{} each term in $\vec{(\nf{\tmtwo\sigma})}$ is a $\xK'$-nf.\r
+    \item Case $\head\neq\var$: $\nf{\tm\sigma} = \lambda\vec\vartwo.\,\head\,\vec{(\nf{\args\sigma})}$.\r
+    By \ih{} each term in $\vec{(\nf{\args\sigma})}$ is a $\xK'$-nf.\r
     We conclude since by hypothesis $|\vec\vartwo|\leq\xK{}<\xK'$.\r
-    \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.\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
-    $\tm\sigma \to^* \lambda\vec\vartwo\vec\varthree\varthree'.\, \varthree'\vec\alpha \vec{(\tmtwo\sigma)}\vec\varthree $ for \r
-    $|\vec\varthree| = i - |\vec\tmtwo|$.\r
+    \item Case $\head=\var$ and $|\vec\args| \leq i$:\r
+    $\tm\sigma \to^* \lambda\vec\vartwo\vec\varthree\varthree'.\, \varthree'\vec\alpha \vec{(\args\sigma)}\vec\varthree $ for \r
+    $|\vec\varthree| = i - |\vec\args|$.\r
     Conclude by \ih{} and because $|\vec\vartwo\vec\varthree\varthree'| \leq \xK{} + i - |\vec\tmtwo| + 1 \leq \xK{} + i + 1 = \xK'$.\r
+    \item Case $\head=\var$ and $i<|\vec\args|$:\r
+     $\tm\sigma \to^* \lambda\vec\vartwo.\, (\args_i\sigma)\vec\alpha \vec{(\args\sigma)} $.\r
+     Now, by \ih{} $\nf{\args_i\sigma}$ is a $\xK'$-nf, and since $|\vec\alpha|\geq\xK'$,\r
+     $\nf{(\args_i\sigma\vec\alpha)}$ is inert.\r
+     Therefore $\nf\tm = \lambda\vec\vartwo.\,\nf{(\args_i\sigma\vec\alpha)} \vec{(\nf{\args\sigma})}$,\r
+     and again by \ih{} it is also a $\xK'$-nf.\r
   \end{itemize}\r
   \r
 \end{proof}\r
@@ -345,7 +345,7 @@
 % \end{proof}\r
 \r
 \r
-\begin{lemma}\r
+\begin{lemma}\label{l:aux1}\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
@@ -362,14 +362,28 @@
   and we conclude.\r
 \end{proof}\r
 \r
-\begin{lemma}\r
+\begin{lemma}\label{l:aux2}\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
+  By induction on $|\tm|$.\r
+  Let $\tm = \lambda\vec\vartwo.\,h\,\vec a$ and $\sigma\defeq\Subst\var\perm$:\r
+  \begin{itemize}\r
+    \item If $h \neq \var$, then $\nf{\tm\sigma} = \lambda\vec\vartwo.\,h\,\vec {(\nf {a\sigma})}$,\r
+    and we conclude since $h\neq \alpha_j$ by the hypothesis that $\alpha_j$ is\r
+    a fresh variable.\r
+    \item If $h=\var$ and $|\vec a| \leq i$, then\r
+    $\tm\sigma \to^* \lambda\vec\vartwo\vec\varthree\varthree'.\, \varthree'\vec\alpha \vec{(\args\sigma)}\vec\varthree $,\r
+    and we conclude since the head $\varthree'$ is a bound variable,\r
+    while $\alpha_j$ is free.\r
+    \item If $h=\var$ and $|\vec a| > i$, then\r
+    $\tm\sigma \to^* \lambda\vec\vartwo.\, (\args_i\sigma)\vec\alpha \vec{(\args\sigma)} $.\r
+    $\nf{(\args_i\sigma\,\vec\alpha)} = \tmtwo\,\alpha_j$ by \reflemma{aux1}\r
+    for some inert $\tmtwo$. Clearly $\tmtwo\,\alpha_j \EtaNeq \alpha_j$.\r
+  \end{itemize}\r
 \end{proof}\r
 \r
 \begin{theorem}\r
@@ -410,6 +424,7 @@
      and we conclude because the two terms have a different number of arguments.\r
      \r
      We now consider the other subcase $h_1=h_2=\var$, and the following subsubcases:\r
+     {\color{red}[Usare \reflemma{aux2} nei punti seguenti]}\r
      \begin{itemize}\r
        \item $|\vec a|,|\vec b|\leq i$: \TODO\r
        \item $|\vec a|>i$ and $|\vec b|\leq i$: use boh \TODO\r