From 0fd76d8a70c67669bae7798495d33dad55bc3c6f Mon Sep 17 00:00:00 2001 From: acondolu Date: Fri, 27 Jul 2018 19:36:55 +0200 Subject: [PATCH] More comments and small fixes --- notes.tex | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/notes.tex b/notes.tex index 264e827..c4e4cfd 100644 --- a/notes.tex +++ b/notes.tex @@ -380,7 +380,7 @@ $\nf{\tm\sigma}\EtaNeq\nf{\tmtwo\sigma}$. Let $\tm \EtaEq \lambda\vec\vartwo.\, h_1\,\vec a$ and $\tmtwo \EtaEq \lambda\vec\vartwo.\, h_2\,\vec b$, - with $|\vec\vartwo| = \xK$. + with $|\vec\vartwo| = \xK$ {\color{red}[Capire perche' si puo' $\xK$-$\eta$-espandere qui]}. By (course-of-value) induction on the size of $\tm$ and $\tmtwo$, and by cases on the definition of eta-difference: \begin{itemize} @@ -401,9 +401,10 @@ We now consider the other subcase $h_1=h_2=\var$, and the following subsubcases: \begin{itemize} - \item Both $|\vec a|,|\vec b|\leq i$: \TODO - \item w.l.o.g. $|\vec a|>i$ and $|\vec b|\leq i$: use boh \TODO - \item Both $|\vec a|,|\vec b|> i$: \TODO use the lemma above + \item $|\vec a|,|\vec b|\leq i$: \TODO + \item $|\vec a|>i$ and $|\vec b|\leq i$: use boh \TODO + \item $|\vec a|\leq i$ and $|\vec b|> i$: symmetric to the case above. + \item $|\vec a|,|\vec b|> i$: \TODO use the lemma above plus another one. Reason on the numebr of arguments $\Args{\nf{a_i\sigma\vec\alpha}}$ vs $\Args{\nf{b_i\sigma\vec\alpha}}$. @@ -417,7 +418,7 @@ \lambda\vec\vartwo.\,h_2\,\vec{(\nf{b\sigma})}$, and we conclude by \ih{} since $a_n \EtaNeq b_n$ implies that $\nf{a_n\sigma} \EtaNeq \nf{b_n\sigma}$. - {\color{red}[Can we use the \ih{} here?]} + {\color{red}[Capire se possiamo davvero usare l'\ih{} qui]} We now consider the other subcase $h_1=h_2=\var$, and the following subsubcases: \begin{itemize} -- 2.39.2