+\clearpage\r
+\section[Tentativi X-separability]{Tentativi $\mathbf X$--separability (July, 15$^{\mathbf{th}}\div\infty$)}\r
+\newcommand{\perm}{p}\r
+\newcommand{\Perm}[2]{\operatorname{P}[#1,#2]}\r
+\newcommand{\xK}{\kappa}\r
+\newcommand{\xN}{n}\r
+\newcommand{\LAM}[2]{\Lambda_{#2,#1}}\r
+\newcommand{\LAMNK}{\LAM\xN\xK}\r
+% \newcommand{\kn}{$(\kappa,n)$}\r
+\newcommand{\knnf}{$\xK{}$-nf}\r
+\newcommand{\Lams}[1]{\operatorname{lams}(#1)}\r
+\newcommand{\Args}[1]{\operatorname{args}(#1)}\r
+\newcommand{\Head}[1]{\operatorname{head}(#1)}\r
+\newcommand{\nf}[1]{#1{\downarrow}}\r
+\newcommand{\Nat}{\mathbb{N}}\r
+\begin{definition}[$\Lams\cdot,\Args\cdot,\Head\cdot$]\r
+ \[\Lams{\lambda\vec\var.\,\vartwo\,\vec\tm} \defeq |\vec\var| \]\r
+ \[\Args{\lambda\vec\var.\,\vartwo\,\vec\tm} \defeq |\vec\tm| \]\r
+ \[\Head{\lambda\vec\var.\,\vartwo\,\vec\tm} \defeq \vartwo \]\r
+\end{definition}\r
+\r
+\begin{definition}[$\xK$-normal forms]\r
+ First recall that terms in normal form have the shape\r
+ $\lambda\vec\var.\,\vartwo\,\vec\tm$, where the terms $\vec\tm$ are in normal form too.\r
+ \r
+ We define inductively the set of \knnf s (where $\xK$ is a natural number):\r
+ $\lambda\vec\var.\,\vartwo\,\vec\tm$ is a \knnf{} iff \r
+ $|\vec\var|\leq\xK$%\r
+ %, $|\vec\tm|\leq\xN$\r
+ , and every term in $\vec\tm$ is a \knnf{} as well.\r
+\end{definition}\r
+\r
+\begin{definition}[Normal form $\nf\cdot$]\r
+ \r
+\end{definition}\r
+\r
+\begin{definition}[Permutator $\Perm\cdot\cdot$]~\r
+ \[\Perm i j \defeq \lambda\vec\var\vartwo.\,\vartwo\, \vec\alpha\,\vec\var\,\vartwo\]\r
+ where $\vec\var$, $\vec\alpha$ and $\vartwo$ are fresh variables,\r
+ 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
+\end{lemma}\r
+\r
+\begin{lemma}\label{l:k-prime-nf}\r
+ Let $\tm$ a \knnf, $\var$ a variable, $i$ a natural number, and $\xK'\defeq \xK + i + 1$.\r
+ 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 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
+ 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 (\textcolor{red}{Serve lemma?}).\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
+ Conclude by \ih{} and because $|\vec\vartwo\vec\varthree\varthree'| \leq \xK{} + i - |\vec\tmtwo| + 1 \leq \xK{} + i + 1 = \xK'$.\r
+ \end{itemize}\r
+ \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
+% then $\tmtwo\defeq\nf{\tm\Subst\var{\Perm i j}}$ is defined;\r
+% $\Lams\tm=\Lams{\tmtwo}$; $\tmtwo$ is a $(j,\xN + j)$-nf.\r
+% \end{lemma}\r
+% \begin{proof}\color{red}\TODO{}\r
+% By induction on the normal form structure of $\tm$:\r
+% let $\tm=\lambda\vec\var.\,\vartwo\,\vec\tmtwo$.\r
+% By \ih{}, $\nf{\tmtwo\Subst\var\perm}$ are $(j,\xN+j)$-nfs.\r
+% \begin{itemize}\r
+% \item if $\vartwo=\var$, then\r
+% $\nf{\tm\Subst\var\perm} = \lambda\var_1\ldots\var_{???}.\,\var\,\vec\tmthree$\r
+% \item if $\vartwo\neq\var$, then $\nf{\tm\Subst\var\perm} = \lambda\vec\var.\,\vartwo\,\vec\tmthree$\r
+% where $\vec\tmthree\defeq \nf{\vec\tmtwo\Subst\var\perm}$.\r
+% Conclude by inductive hypothesis.\r
+% \end{itemize}\r
+% \end{proof}\r
+\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\vec\alpha} \EtaNeq \alpha_j$.\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
+ \r
+ By structural induction on $\tm$.\r
+ Let $\tm = \lambda\vec\vartwo.\, h\,\vec a$ for $|\vec\vartwo|\leq\xK$.\r
+ \TODO{}\r
+\end{proof}\r
+\r
+% TODO: $\xK$-standard proof of $\eta$.\r
+\r
+\begin{lemma}\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
+\begin{proof}\r
+ Let $\sigma \defeq \Subst\var\perm$.\r
+ First of all, note that by \reflemma{k-prime-nf}\r
+ $\nf{\tm\sigma}$ and $\nf{\tmtwo\sigma}$ are defined and\r
+ are $\xK'$-nfs for $\xK'\defeq\xK + i + 1$.\r
+ \r
+ If $\tm\EtaEq\tmtwo$ then necessarily $\nf{\tm\sigma}\EtaEq\nf{\tmtwo\sigma}$.\r
+ Let us now assume that $\tm\EtaNeq\tmtwo$, and prove that\r
+ $\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$.\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
+ \item $h_1 \neq h_2$: we distinguish three subcases.\r
+ \begin{itemize}\r
+ \item $h_1,h_2\neq \var$:\r
+ it follows that $\nf{\tm\sigma} = \nf{(\lambda\vec\vartwo.\,h_1\,\vec a)\sigma} = \lambda\vec\vartwo.\,h_1\,\vec{(\nf{a\sigma})}$\r
+ and $\nf{\tmtwo\sigma} = \nf{(\lambda\vec\vartwo.\,h_2\,\vec b)\sigma} = \lambda\vec\vartwo.\,h_2\,\vec{(\nf{b\sigma})}$,\r
+ 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
+ \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
+ if $h_1,h_2\neq\var$, then again $\nf{\tm\sigma} = \lambda\vec\vartwo.\,h_1\,\vec{(\nf{a\sigma})}$\r
+ and $\nf{\tmtwo\sigma} = \lambda\vec\vartwo.\,h_2\,\vec{(\nf{b\sigma})}$,\r
+ 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
+ \begin{itemize}\r
+ \item Both $|\vec a|,|\vec b|\leq i$: \TODO\r
+ \item w.l.o.g. $|\vec a|>i$ and $|\vec b|\leq i$: use boh \TODO\r
+ \item Both $|\vec a|,|\vec b|> i$: \TODO use the lemma above\r
+ plus another one. Reason on the numebr of arguments\r
+ $\Args{\nf{a_i\sigma\vec\alpha}}$ vs \r
+ $\Args{\nf{b_i\sigma\vec\alpha}}$.\r
+ If equal conclude, otherwise conclude by lemma above.\r
+ \end{itemize}\r
+ \item \r
+ $h_1 = h_2$ and $|\vec a| = |\vec b|$\r
+ but $a_n \EtaNeq b_n$ for some $n$.\r
+ If $h_1=h_2\neq\var$, then again\r
+ $\lambda\vec\vartwo.\,h_1\,\vec{(\nf{a\sigma})} =%\r
+ \lambda\vec\vartwo.\,h_2\,\vec{(\nf{b\sigma})}$,\r
+ and we conclude by \ih{} since $a_n \EtaNeq b_n$ implies that \r
+ $\nf{a_n\sigma} \EtaNeq \nf{b_n\sigma}$.\r
+ {\color{red}[Can we use the \ih{} here?]}\r
+ \r
+ We now consider the other subcase $h_1=h_2=\var$, and the following subsubcases:\r
+ \begin{itemize}\r
+ \item $|\vec a| = |\vec b| \leq i$: \TODO easy \r
+ \item $|\vec a| = |\vec b| > i$ and $a_i\EtaEq b_i$: \TODO ok\r
+ \item $|\vec a| = |\vec b| > i$ and $a_i\EtaNeq b_i$: \TODO\r
+ by \ih{} already $\nf{a_i\sigma\vec\alpha}\EtaNeq\nf{b_i\sigma\vec\alpha}$\r
+ and conclude by appending the $\vec a$ and $\vec b$.\r
+ \end{itemize}\r
+ \end{itemize}\r
+\end{proof}\r