diff --git a/tesi/tesi_unicode.org b/tesi/tesi_unicode.org
index 1e8ca0d..8e4fd59 100644
--- a/tesi/tesi_unicode.org
+++ b/tesi/tesi_unicode.org
@@ -271,7 +271,7 @@ environment $\sigma$ mapping variables to accessors.\\
 $\Failure$ expresses a match failure that occurs when no clause matches the input
 value.
 \\
-$\Switch a {\Fam {i \in I} {\pi_i, D_i}} \Dfb$ has one subtree $D_i$
+$\Switch a {\Fam {i \in I} {\pi_i, D_i}} D_{fallback}$ has one subtree $D_i$
 for every head constructor that appears in the pattern matching
 clauses, and a fallback case that is used when at least one variant of
 the constructor doesn't appear in the clauses. The presence of the
@@ -362,9 +362,9 @@ If we have two terminals, such as leaves in the first example,
 we check that the two right-hand-sides are equivalent.
 If we have a node $N$ and another tree $T$ we check equivalence for
 each child of $N$, which is a pair of a branch condition $\pi_i$ and a
-subtree $C_i$. For every child $(\pi_i, C_i)$ we reduce $T$ by killing all
+subtree $D_i$. For every child $(\pi_i, D_i)$ we reduce $T$ by killing all
 the branches that are incompatible with $\pi_i$ and check that the
-reduced tree is equivalent to $C_i$.
+reduced tree is equivalent to $D_i$.
 \\
 \subsection{From source programs to decision trees}
 Our source language supports integers, lists, tuples and all algebraic
@@ -436,13 +436,13 @@ possible values \emph{S} and a pair of source and target decision trees and
 in case the two trees are not equivalent it returns a counter example.
 Our algorithm respects the following correctness statement:
 \begin{align*}
- \EquivTEX S {C_S} {C_T} = \YesTEX \;\land\; \coversTEX {C_T} S
+ \EquivTEX S {D_S} {D_T} = \YesTEX \;\land\; \coversTEX {D_T} S
  & \implies
- \forall v_S \approx v_T \in S,\; C_S(v_S) = C_T(v_T)
+ \forall v_S \approx v_T \in S,\; D_S(v_S) = D_T(v_T)
 \\
- \EquivTEX S {C_S} {C_T} = \NoTEX {v_S} {v_T} \;\land\; \coversTEX {C_T} S
+ \EquivTEX S {D_S} {D_T} = \NoTEX {v_S} {v_T} \;\land\; \coversTEX {D_T} S
  & \implies
- v_S \approx v_T \in S \;\land\; C_S(v_S) \neq C_T(v_T)
+ v_S \approx v_T \in S \;\land\; D_S(v_S) \neq D_T(v_T)
 \end{align*}
 * Background
 ** OCaml
@@ -1439,7 +1439,7 @@ target programs.
     \text{\emph{decision trees}} & D(\pi, e)
     & \bnfeq & \Leaf {\cle(a)} \\
     & & \bnfor & \Failure \\
-    & & \bnfor & \Switch a {\Fam {i \in I} {\pi_i, D_i}} \Dfb \\
+    & & \bnfor & \Switch a {\Fam {i \in I} {\pi_i, D_i}} D_{fallback} \\
     & & \bnfor & \Guard {\cle(a)} {D_0} {D_1} \\
     & & \bnfor & Unreachable  \\
     \text{\emph{accessors}} & a 
@@ -1854,7 +1854,7 @@ counter-example.)
 
   \begin{array}{l@{~}r@{~}l}
     & & \text{\emph{boolean result}} \\
-    b & \in & \{ 0, 1 \} \\
+    b & \in & \{ No, Yes \} \\
   \end{array}
 
   \begin{array}{l@{~}r@{~}l}
@@ -1908,7 +1908,7 @@ hand side.
    \\
    \forall i,\; \Equivrel {(S \cap a \in \pi_i)} {D_S} {D_i} G
    \\
-   \Equivrel {(S \cap a \notin \Fam i {\pi_i})} {D_S} \Dfb G}
+   \Equivrel {(S \cap a \notin \Fam i {\pi_i})} {D_S} {D_{fallback}} G}
   {\Equivrel S
     {D_S} {\Switch a {\Fam i {\pi_i} {D_i}} \Dfb} G}
 \end{mathpar}
@@ -2005,7 +2005,6 @@ Corollary: For a full input space /S/, that is the universe of the
 target program:
 | $equiv(S, \llbracket t_S \rrbracket{_S}, \llbracket t_T \rrbracket{_T}, \emptyset) = Yes \Leftrightarrow  \progrel {t_S} {t_T}$
 
-
 \begin{comment}
 TODO: put ^i∈I where needed
 \end{comment}
@@ -2047,7 +2046,7 @@ lemma.
 \begin{comment}
 TODO: what should I say about covering??? I swap π and π' 
 Covering lemma:
-        ∀a,π covers(Cₜ,S) → covers(C_{t/a→π}, (S∩a→π))
+        ∀a,π covers(Dₜ,S) → covers(D_{t/a→π}, (S∩a→π))
             Uᵢπⁱ ≈ Uᵢπ'∩(a→π) ≈ (Uᵢπ')∩(a→π) %%
 
 
diff --git a/todo.org b/todo.org
index c6a6ba1..10293b4 100644
--- a/todo.org
+++ b/todo.org
@@ -27,7 +27,7 @@
   - [ ] chiedi a Galla`, Marco e Naz quali sono tutti gli es
   - [ ] linear models.zip?
 
-* Tesi [9/33]
+* Tesi [18/33]
 - [X] Rivedere inference rules di Gabriel e aggiustarle con le mie
 - [ ] Definisci domain sempre allo stesso modo, con bigcup o |
 - [ ] Scegli se usare [[t_s]\] o D(ts)
@@ -42,7 +42,7 @@
 - [ ] Equivalenza R_s R_T (run)
 - [ ] TODO t_t
 - [ ] Introduzione: Explain covers alla fine (o vedi che si fa nel paper)
-- [ ] Paginazione:
+- [-] Paginazione:
   + [ ] figura (function scrutinee) fuori pagina
   + [ ] figura primo decision tree: migliorala
   + [ ] Line breaks
@@ -50,7 +50,7 @@
   + [ ] correct. stat. di eq. checking: fuori margine
   + [ ] Minipages: spazio o divisore dalle linee prima e dopo
   + [ ] Minipages: allinea
-  + [ ]  {\progrel t_S    t_T}: t_S finisce fuori
+  + [X]  {\progrel t_S    t_T}: t_S finisce fuori
 - [X] segreteria: tesi inglese
 - [X] Gatti: inglese
 - [X] Gatti: Coppo mio relatore
@@ -64,21 +64,21 @@
     - [X] snellendo un po' la presentazione formale. 
     - [ ] spiegando meglio il ruolo della symbolic interpretation
     - [X] Perche' ci si concentra sulla traduzione dei pattern?
-- [ ] riferimenti bibliografici
-- [ ] paper pattern matching C++
-- [ ] Gabriel: finisci
-- [ ] SimpleEquiv Latex
-- [ ] Boolean result o Yes|No? (Inference rules)
+- [X] riferimenti bibliografici
+- [X] paper pattern matching C++
+- [X] Gabriel: finisci
+- [X] SimpleEquiv Latex
+- [X] Boolean result o Yes|No? (Inference rules)
 - [ ] Mostra altri casi per la empty rule
-- [ ] Adatta i cambiamenti al paper
+- [X] Adatta i cambiamenti al paper
 - [ ] Esempio trimming
 - [ ] Trimming e resto: mi sa che usi left e right male
 - [ ] Spiega perche` trimming non simmetrico
-- [ ] Spiega meglio le guards on equivalence checking
-- [ ] t_T e t_S o t_t e t_s???
+- [X] Spiega meglio le guards on equivalence checking
+- [X] t_T e t_S o t_t e t_s???
 - [X] TODO eq_muovi : si parla di eq checking, forse non li`
 - [X] Gabriel: quello che penso sulle equivalenze omesse e` giusto?
-- [ ] Cambia le C di constraint tree in D
+- [X] Cambia le C di constraint tree in D
 - [ ] TODO on the org file
 HALP
 HALP!