diff git a/tesi/tesi.pdf b/tesi/tesi.pdf
index 5f042c3..47fecaa 100644
 a/tesi/tesi.pdf
+++ b/tesi/tesi.pdf
Binary files differ
diff git a/tesi/tesi.pdf b/tesi/tesi.pdf
index 5f042c3..47fecaa 100644
 a/tesi/tesi.pdf
+++ b/tesi/tesi.pdf
Binary files differ
diff git a/tesi/tesi_unicode.org b/tesi/tesi_unicode.org
index 7280497..bd08a56 100644
 a/tesi/tesi_unicode.org
+++ b/tesi/tesi_unicode.org
@@ 33,6 +33,7 @@
#+LaTeX_HEADER: \usepackage{hyperref}
#+LaTeX_HEADER: \usepackage{amsmath}
#+LaTeX_HEADER: \usepackage{appendix}
+#+LaTeX_HEADER: \newcommand{\Rule}[1]{\LabTirName{#1}}
#+LaTeX_HEADER: \usepackage{a4}
#+LaTeX_HEADER: \usepackage{amsfonts}
#+LaTeX_HEADER: \usepackage{amsfonts}
@@ 1944,13 +1945,23 @@
{\Switch a {\Fam i {K_i, D_i}} \Dfb} {D_T} G}
\end{mathpar}
When the left hand side is not a terminal, the algorithm explodes the
left hand side while trimming every right hand side subtree. Trimming
a left hand side tree on an interval set $\pi_S$ computed from the right hand
side tree constructor means mapping every branch condition $\pi_T$ (interval set of
possible values) on the left to the intersection of $\pi_T$ and $\pi_S$ when
the accessors on both side are equal, and removing the branches that
result in an empty intersection. If the accessors are different,
\emph{$\pi_T$} is left unchanged.
+left hand side while trimming every right hand side subtree. As an optimization, in the \Rule{explodeleft} rule we \emph{trim} the
+target tree, by simplifying the tree in depth with the source
+condition. Trimming a target tree on a domain $\pi$ computed from
+a source constructor $K$ means mapping every branch condition $\pi'$
+of every node of the target tree to the intersection $\pi \cap \pi'$
+when the accessors on both sides are equal, and removing the branches
+that result in an empty intersection. If the accessors are different,
+$\pi'$ is left unchanged. Trimming avoids redundant work, because
+each target subtree removed (in one step) by trimming would have been
+traversed during the equivalence computation of each source subtree
+and their children, potentially many times.\\
+We have only defined trimming of a target tree, not of a source tree:
+the branch condition on the source tree are just constructors, so they
+are less expressive than target domains and it is hard to define an
+intersection between the two. We restrict the \Rule{exploderight}
+rule to only work on terminal source trees, so that no duplicate work
+occurs.
\begin{mathpar}
\infer[Push]
{\erel {e_S} {e_T}
@@ 1975,17 +1986,26 @@
blackbox on the left hand Guard node are different, otherwise in
continues by exploding to two subtrees, one in which the guard
condition evaluates to true, the other when it evaluates to false.
Termination of the algorithm is successful only when the guards queue
is empty.\\
+There is no guarantee that the guards will appear at the same tree
+level on both sides: guards cannot be reordered (their evaluation may
+perform observable sideeffects), but they can be permuted with
+(nonobservable) switches. We store a \emph{guard queue} $G$ that
+tracks the guard conditions that we have traversed in the source tree,
+but not yet in the target tree, with the boolean result of each
+condition.\\
+Termination of the algorithm (in the \textsf{Failure} and
+\textsf{Leaf} rules) is successful only when the guards queue is
+empty. This ensures that both sides executed the same guards, in the
+same order.\\
Running a program tₛ or its translation 〚tₛ〛 against an input vₛ
produces as a result /r/ in the following way:
+ result r ::= guard list * (Match blackbox \vert{} NoMatch \vert{} Absurd)
+ guard ::= blackbox.
 ( 〚tₛ〛ₛ(vₛ) ≡ Dₛ(vₛ) ) → r
 tₛ(vₛ) → r
Likewise
 ( 〚tₜ〛ₜ(vₜ) ≡ Dₜ(vₜ) ) → r
 tₜ(vₜ) → r
 result r ::= guard list * (Match blackbox \vert{} NoMatch \vert{} Absurd)
 guard ::= blackbox.
Having defined equivalence between two inputs of which one is
expressed in the source language and the other in the target language,
$\vrel {v_S} {v_T}$, we can define the equivalence between a couple of programs or
@@ 1995,33 +2015,26 @@
The result of the proposed equivalence algorithm is /Yes/ or /No(vₛ,
vₜ)/. In particular, in the negative case, vₛ and vₜ are a couple of
possible counter examples for which the decision trees produce a
different result.
\\
+different result, which can be constructed by taking any pair of
+values respectively inside the domain of πₛ and πₜ.\\
In the presence of guards we can say that two results are
equivalent modulo the guards queue, written /r₁ ≃gs r₂/, when:
 (gs₁, r₁) ≃_{gs} (gs₂, r₂) ⇔ (gs₁, r₁) = (gs₂ +++ gs, r₂)
We say that Dₜ covers the input space /S/, written
/covers(Dₜ, S)/ when every value vₛ∈S is a valid input to the
decision tree Dₜ. (TODO: rephrase)
Given an input space /S/ and a couple of decision trees, where
the target decision tree Dₜ covers the input space /S/ we can define equivalence:
+Given an input space /S/ and a pair of decision trees we can define equivalence:
 $equiv(S, D_S, D_T, gs) = Yes \wedge covers(D_T, S) \to \forall \vrel {v_S} {v_T} \in S, D_S(v_S) \simeq_{gs} D_T(v_T)$
Similarly we say that a couple of decision trees in the presence of
an input space /S/ are /not/ equivalent in the following way:
 $equiv(S, D_S, D_T, gs) = No(v_S, v_T) \wedge covers(D_T, S) \to \vrel {v_S} {v_T} \in S \wedge D_S(v_S) \ne_{gs} D_T(v_T)$
Corollary: For a full input space /S/, that is the universe of the
+ $equiv(S, D_S, D_T, gs) = No(v_S, v_T) \to \vrel {v_S} {v_T} \in S \wedge D_S(v_S) \ne_{gs} D_T(v_T)$
+As a corollary, we have that 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}
\subsubsection{The trimming lemma}
The trimming lemma allows to reduce the size of a decision tree given
an accessor /a/ → π relation
 ∀vₜ ∈ (a→π), Dₜ(vₜ) = D_{t/a→π}(vₜ)
We prove this by induction on Dₜ:

+ ∀vₜ ∈ (aᵢ→πᵢ)^{i∈I}, Dₜ(vₜ) = D_{t/a→π}(vₜ)
+The trimming lemma is central to the \Rule{explodeleft} rule.\\
+We prove the trimming lemma by induction on Dₜ:
 Dₜ = Leaf_{bb}: when the decision tree is a leaf terminal, the result of trimming on a Leaf is the Leaf itself
 Leaf_{bb/a→π}(v) = Leaf_{bb}(v)
 The same applies to Failure terminal
@@ 2030,10 +2043,6 @@
/a/ of the subtree Dᵢ and we define πᵢ' = πᵢ if a≠b else πᵢ∩π Trimming
a switch node yields the following result:
 Switch(b, (π→Dᵢ)^{i∈I})_{/a→π} := Switch(b, (π'ᵢ→D_{i/a→π})^{i∈I})
\begin{comment}
TODO: understand how to properly align lists
check that every list is aligned
\end{comment}
For the trimming lemma we have to prove that running the value vₜ against
the decision tree Dₜ is the same as running vₜ against the tree
D_{trim} that is the result of the trimming operation on Dₜ