diff --git a/tesi/conv.py b/tesi/conv.py
index 20477f4..1f28a56 100644
--- a/tesi/conv.py
+++ b/tesi/conv.py
@@ -3,7 +3,7 @@ import re
 from sys import argv
 
 allsymbols = json.load(open('./unicode-latex.json'))
-mysymbols = ['≡', '≠', '≼', '→', '←', '⊀', '⋠', '≺', '∀', '∈', 'ε','₀', '₂', '₁', '₃', 'ₐ', 'ₖ', 'ₘ', 'ₙ', 'ᵢ', 'ⁱ', '⋮', 'ₛ', 'ₜ', '≃', '⇔', '∧', '∅', 'ℕ', 'ⱼ', 'ʲ', '⊥', 'π', 'α', 'β', '∞', 'σ', '≤', '⊈', '∧', '∨', '∃', '⇒' ]
+mysymbols = ['≡', '≠', '≼', '→', '←', '⊀', '⋠', '≺', '∀', '∈', 'ε','₀', '₂', '₁', '₃', 'ₐ', 'ₖ', 'ₘ', 'ₙ', 'ᵢ', 'ⁱ', '⋮', 'ₛ', 'ₜ', '≃', '⇔', '∧', '∅', 'ℕ', 'ⱼ', 'ʲ', '⊥', 'π', 'α', 'β', '∞', 'σ', '≤', '⊈', '∧', '∨', '∃', '⇒', '∩', '∉', '⋃' ]
 extrasymbols = {'〚': '\llbracket', '〛': '\rrbracket'}
 
 symbols = {s: allsymbols[s] for s in mysymbols}
diff --git a/tesi/mathpartir.sty b/tesi/mathpartir.sty
new file mode 100644
index 0000000..bcd26a1
--- /dev/null
+++ b/tesi/mathpartir.sty
@@ -0,0 +1,469 @@
+%%
+%% This is file `mathpartir.sty',
+%% generated with the docstrip utility.
+%%
+%% The original source files were:
+%%
+%% mathpartir.dtx  (with options: `package')
+%% 
+%% This is a generated file.
+%% 
+%% Copyright (C) 2015, 2020 by Didier Remy <didier.remy(at)inria(dot)fr>
+%% 
+%% This file is part of mathpartir.
+%% 
+%% mathpartir is free software: you can redistribute it and/or modify
+%% it under the terms of the GNU General Public License as published by
+%% the Free Software Foundation, either version 2 of the License, or
+%% (at your option) any later version.
+%% 
+%% mathpartir is distributed in the hope that it will be useful,
+%% but WITHOUT ANY WARRANTY; without even the implied warranty of
+%% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+%% GNU General Public License for more details.
+%% 
+%% You should have received a copy of the GNU General Public License
+%% along with mathpartir.  If not, see <http://www.gnu.org/licenses/>.
+%% 
+\NeedsTeXFormat{LaTeX2e}
+\ProvidesPackage{mathpartir}
+    [2020/02/15 version 1.4.0 Math Paragraph for Typesetting Inference Rules]
+%% Identification
+%% Preliminary declarations
+
+\RequirePackage {keyval}
+
+%% Options
+%% More declarations
+
+%% PART I: Typesetting maths in paragraphe mode
+
+%% \newdimen \mpr@tmpdim
+%% Dimens are a precious ressource. Uses seems to be local.
+\let \mpr@tmpdim \@tempdima
+
+\let \mpr@hva \empty
+
+%% normal paragraph parametters, should rather be taken dynamically
+\def \mpr@savepar {%
+  \edef \MathparNormalpar
+     {\noexpand \lineskiplimit \the\lineskiplimit
+      \noexpand \lineskip \the\lineskip}%
+  }
+
+\def \mpr@rulelineskip {\lineskiplimit=0.3em\lineskip=0.2em plus 0.1em}
+\def \mpr@lesslineskip {\lineskiplimit=0.6em\lineskip=0.5em plus 0.2em}
+\def \mpr@lineskip  {\lineskiplimit=1.2em\lineskip=1.2em plus 0.2em}
+\let \MathparLineskip \mpr@lineskip
+\def \mpr@paroptions {\MathparLineskip}
+\let \mpr@prebindings \relax
+
+\newskip \mpr@andskip \mpr@andskip 2em plus 0.5fil minus 0.5em
+
+\def \mpr@goodbreakand
+   {\hskip -\mpr@andskip  \penalty -1000\hskip \mpr@andskip}
+\def \mpr@and {\hskip \mpr@andskip}
+\def \mpr@andcr {\penalty 50\mpr@and}
+\def \mpr@cr {\penalty -10000\mpr@and}
+\def \mpr@eqno #1{\mpr@andcr #1\hskip 0em plus -1fil \penalty 10}
+
+\def \mpr@bindings {%
+  \let \and \mpr@andcr
+  \let \par \mpr@andcr
+  \let \\\mpr@cr
+  \let \eqno \mpr@eqno
+  \let \hva \mpr@hva
+  }
+\let \MathparBindings \mpr@bindings
+\def \MathparBeginhook {}
+\def \MathparEndhook {}
+
+\let \MathparCentering \centering
+\newenvironment{mathpar}[1][]
+  {$$
+     \MathparBeginhook
+     %% We save \lineskip parameters so that the user can restore them
+     %% inside math \MathparNormalpar
+     \mpr@savepar
+     %% We define the shape of the paragrah
+     \parskip 0em \hsize \linewidth \MathparCentering
+     \vbox \bgroup \mpr@prebindings \mpr@paroptions #1\ifmmode $\else
+     \noindent $\displaystyle\fi
+     \MathparBindings}
+  {\MathparEndhook \unskip \ifmmode $\fi\egroup $$\ignorespacesafterend}
+
+\newenvironment{mathparpagebreakable}[1][]
+  {\begingroup
+   \par
+   \mpr@savepar \parskip 0em \hsize \linewidth \centering
+      \mpr@prebindings \mpr@paroptions #1%
+      \vskip \abovedisplayskip \vskip -\lineskip%
+     \ifmmode  \else  $\displaystyle\fi
+     \MathparBindings
+  }
+  {\unskip
+   \ifmmode $\fi \par\endgroup
+   \vskip \belowdisplayskip
+   \noindent
+  \ignorespacesafterend}
+
+
+%%% HOV BOXES
+
+\def \mathvbox@ #1{\hbox \bgroup \mpr@normallineskip
+  \vbox \bgroup \tabskip 0em \let \\ \cr
+  \halign \bgroup \hfil $##$\hfil\cr #1\crcr \egroup \egroup
+  \egroup}
+
+\def \mathhvbox@ #1{\setbox0 \hbox {\let \\\qquad $#1$}\ifnum \wd0 < \hsize
+      \box0\else \mathvbox {#1}\fi}
+
+%% Part II -- operations on lists
+
+\newtoks \mpr@lista
+\newtoks \mpr@listb
+
+\long \def\mpr@cons #1\mpr@to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter
+{#2}\edef #2{\the \mpr@lista \the \mpr@listb}}
+
+\long \def\mpr@snoc #1\mpr@to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter
+{#2}\edef #2{\the \mpr@listb\the\mpr@lista}}
+
+\long \def \mpr@concat#1=#2\mpr@to#3{\mpr@lista \expandafter {#2}\mpr@listb
+\expandafter {#3}\edef #1{\the \mpr@listb\the\mpr@lista}}
+
+\def \mpr@head #1\mpr@to #2{\expandafter \mpr@head@ #1\mpr@head@ #1#2}
+\long \def \mpr@head@ #1#2\mpr@head@ #3#4{\def #4{#1}\def#3{#2}}
+
+\def \mpr@flatten #1\mpr@to #2{\expandafter \mpr@flatten@ #1\mpr@flatten@ #1#2}
+\long \def \mpr@flatten@ \\#1\\#2\mpr@flatten@ #3#4{\def #4{#1}\def #3{\\#2}}
+
+\def \mpr@makelist #1\mpr@to #2{\def \mpr@all {#1}%
+   \mpr@lista {\\}\mpr@listb \expandafter {\mpr@all}\edef \mpr@all {\the
+   \mpr@lista \the \mpr@listb \the \mpr@lista}\let #2\empty
+   \def \mpr@stripof ##1##2\mpr@stripend{\def \mpr@stripped{##2}}\loop
+     \mpr@flatten \mpr@all \mpr@to \mpr@one
+     \expandafter \mpr@snoc \mpr@one \mpr@to #2\expandafter \mpr@stripof
+     \mpr@all \mpr@stripend
+     \ifx \mpr@stripped \empty \let \mpr@isempty 0\else \let \mpr@isempty 1\fi
+     \ifx 1\mpr@isempty
+   \repeat
+}
+
+\def \mpr@rev #1\mpr@to #2{\let \mpr@tmp \empty
+   \def \\##1{\mpr@cons ##1\mpr@to \mpr@tmp}#1\let #2\mpr@tmp}
+
+%% Part III -- Type inference rules
+
+\newif \if@premisse
+\newbox \mpr@hlist
+\newbox \mpr@vlist
+\newif \ifmpr@center \mpr@centertrue
+\def \mpr@vskip {}
+\let \mpr@vbox \vbox
+\def \mpr@htovlist {%
+   \setbox \mpr@hlist
+      \hbox {\strut
+             \ifmpr@center \hskip -0.5\wd\mpr@hlist\fi
+             \unhbox \mpr@hlist}%
+   \setbox \mpr@vlist
+      \mpr@vbox {\if@premisse
+                \box \mpr@hlist
+                \ifx \mpr@vskip \empty \else
+                  \hrule height 0em depth \mpr@vskip width 0em
+                \fi
+                \unvbox \mpr@vlist
+             \else
+                \unvbox \mpr@vlist
+                \ifx \mpr@vskip \empty \else
+                  \hrule height 0em depth \mpr@vskip width 0em
+                \fi
+                \box \mpr@hlist
+             \fi}%
+}
+
+\def \mpr@item #1{$\displaystyle #1$}
+\def \mpr@sep{2em}
+\def \mpr@blank { }
+\def \mpr@hovbox #1#2{\hbox
+  \bgroup
+  \ifx #1T\@premissetrue
+  \else \ifx #1B\@premissefalse
+  \else
+     \PackageError{mathpartir}
+       {Premisse orientation should either be T or B}
+       {Fatal error in Package}%
+  \fi \fi
+  \def \@test {#2}\ifx \@test \mpr@blank\else
+  \setbox \mpr@hlist \hbox {}%
+  \setbox \mpr@vlist \vbox {}%
+  \if@premisse \let \snoc \mpr@cons \else \let \snoc \mpr@snoc \fi
+  \let \@hvlist \empty \let \@rev \empty
+  \mpr@tmpdim 0em
+  \expandafter \mpr@makelist #2\mpr@to \mpr@flat
+  \if@premisse \mpr@rev \mpr@flat \mpr@to \@rev \else \let \@rev \mpr@flat \fi
+  \def \\##1{%
+     \def \@test {##1}\ifx \@test \empty
+        \mpr@htovlist
+        \mpr@tmpdim 0em %%% last bug fix not extensively checked
+     \else
+      \setbox0 \hbox{\mpr@item {##1}}\relax
+      \advance \mpr@tmpdim by \wd0
+      %\mpr@tmpdim 1.02\mpr@tmpdim
+      \ifnum \mpr@tmpdim < \hsize
+         \ifnum \wd\mpr@hlist > 0
+           \if@premisse
+             \setbox \mpr@hlist
+                \hbox {\unhbox0 \hskip \mpr@sep \unhbox \mpr@hlist}%
+           \else
+             \setbox \mpr@hlist
+                \hbox {\unhbox \mpr@hlist  \hskip \mpr@sep \unhbox0}%
+           \fi
+         \else
+         \setbox \mpr@hlist \hbox {\unhbox0}%
+         \fi
+      \else
+         \ifnum \wd \mpr@hlist > 0
+            \mpr@htovlist
+            \mpr@tmpdim \wd0
+         \fi
+         \setbox \mpr@hlist \hbox {\unhbox0}%
+      \fi
+      \advance \mpr@tmpdim by \mpr@sep
+   \fi
+   }%
+   \@rev
+   \mpr@htovlist
+   \ifmpr@center \hskip \wd\mpr@vlist\fi \box \mpr@vlist
+   \fi
+   \egroup
+}
+
+%%% INFERENCE RULES
+
+\@ifundefined{@@over}{%
+    \let\@@over\over % fallback if amsmath is not loaded
+    \let\@@overwithdelims\overwithdelims
+    \let\@@atop\atop \let\@@atopwithdelims\atopwithdelims
+    \let\@@above\above \let\@@abovewithdelims\abovewithdelims
+  }{}
+
+%% The default
+
+\def \mpr@@fraction #1#2{\hbox {\advance \hsize by -0.5em
+    $\displaystyle {#1\mpr@over #2}$}}
+\def \mpr@@nofraction #1#2{\hbox {\advance \hsize by -0.5em
+    $\displaystyle {#1\@@atop #2}$}}
+
+\let \mpr@fraction \mpr@@fraction
+
+%% A generic solution to arrow
+
+\def \mpr@@fractionaboveskip {0ex}
+\def \mpr@@fractionbelowskip {0.22ex}
+
+\def \mpr@make@fraction #1#2#3#4#5{\hbox {%
+     \def \mpr@tail{#1}%
+     \def \mpr@body{#2}%
+     \def \mpr@head{#3}%
+     \setbox1=\hbox{$#4$}\setbox2=\hbox{$#5$}%
+     \setbox3=\hbox{$\mkern -3mu\mpr@body\mkern -3mu$}%
+     \dimen0\ht3\advance\dimen0 by \dp3\relax
+     \dimen0 0.5\dimen0\relax
+     \advance \dimen0 by \mpr@@fractionaboveskip
+     \setbox1=\hbox {\raise \dimen0 \box1}\relax
+     \dimen0 -\dimen0\advance \dimen0 \mpr@@fractionaboveskip\dimen0 -\dimen0
+     \advance \dimen0 by \mpr@@fractionbelowskip
+     \setbox2=\hbox {\lower \dimen0 \box2}\relax
+     \setbox0=\hbox {$\displaystyle {\box1 \atop \box2}$}%
+     \dimen0=\wd0\box0
+     \box0 \hskip -\dimen0\relax
+     \hbox to \dimen0 {$%\color{blue}
+       \mathrel{\mpr@tail}\joinrel
+       \xleaders\hbox{\copy3}\hfil\joinrel\mathrel{\mpr@head}%
+     $}}}
+
+%% Old stuff should be removed in next version
+\def \mpr@@nothing #1#2
+    {$\lower 0.01pt \mpr@@nofraction {#1}{#2}$}
+\def \mpr@@reduce #1#2{\hbox
+    {$\lower 0.01pt \mpr@@fraction {#1}{#2}\mkern -15mu\rightarrow$}}
+\def \mpr@@rewrite #1#2#3{\hbox
+    {$\lower 0.01pt \mpr@@fraction {#2}{#3}\mkern -8mu#1$}}
+\def \mpr@infercenter #1{\vcenter {\mpr@hovbox{T}{#1}}}
+
+\def \mpr@empty {}
+\def \mpr@inferrule
+  {\bgroup
+     \ifnum \linewidth<\hsize \hsize \linewidth\fi
+     \mpr@rulelineskip
+     \let \and \qquad
+     \let \hva \mpr@hva
+     \let \@rulename \mpr@empty
+     \let \@rule@options \mpr@empty
+     \let \mpr@over \@@over
+     \mpr@inferrule@}
+\newcommand {\mpr@inferrule@}[3][]
+  {\everymath={\displaystyle}%
+   \def \@test {#2}\ifx \empty \@test
+      \def \@test {#3}\ifx \empty \@test
+        \PackageWarning {mathpartir}
+          {\string\inferrule\space empty arguments substituted}{}%
+        \setbox0 \mpr@fraction {?}{?}%
+      \else
+        \setbox0 \hbox {$\vcenter {\mpr@hovbox{B}{#3}}$}%
+      \fi
+   \else
+   \def \@test {#3}\ifx \empty \@test
+      \setbox0 \hbox {$\vcenter {\mpr@hovbox{T}{#2}}$}%
+   \else
+   \setbox0 \mpr@fraction {\mpr@hovbox{T}{#2}}{\mpr@hovbox{B}{#3}}%
+   \fi \fi
+   \def \@test {#1}\ifx \@test\empty \box0
+   \else \vbox
+%%% Suggestion de Francois pour les etiquettes longues
+%%%   {\hbox to \wd0 {\RefTirName {#1}\hfil}\box0}\fi
+      {\hbox {\DefTirName {#1}}\box0}\fi
+   \egroup}
+
+\def \mpr@vdotfil #1{\vbox to #1{\leaders \hbox{$\cdot$} \vfil}}
+
+
+%% Version for Hoare triples
+
+\def \triple@hlinebox{\noalign{\setbox0\hbox {}\dp0 0.1ex\ht0 0.1ex\box0}}
+\def \triple@hline {\triple@hlinebox\hline\triple@hlinebox}
+
+\newcommand{\triplerule}[4][]
+  {\bgroup
+     \ifnum \linewidth<\hsize \hsize \linewidth\fi
+     \mpr@rulelineskip
+     \let \and \qquad
+     \let \hva \mpr@hva
+     \setbox0 \hbox {\begin{array}[b]{@{}c@{}}
+     \mpr@hovbox{T}{#2}\cr\triple@hline
+     \mpr@hovbox{T}{#3}\cr\triple@hline 
+     \let \mpr@vbox \vtop \ht0 0em
+     \setbox0 \strut \@tempdima \ht0
+     \setbox0 \mpr@hovbox{B}{#4}\advance \@tempdima by -\ht0
+     \setbox0 \hbox{\raise \@tempdima \box0}\box0
+     \end{array}}%
+   \def \@test {#1}\ifx \@test\empty \box0
+   \else \vbox
+      %%% Suggestion de Francois pour les etiquettes longues
+      %%%   {\hbox to \wd0 {\RefTirName {#1}\hfil}\box0}\fi
+      {\hbox {\DefTirName {#1}}\box0}\fi
+   \egroup}
+   
+
+%% Keys that make sence in all kinds of rules
+\def \mprset #1{\setkeys{mprset}{#1}}
+\define@key {mprset}{andskip}[]{\mpr@andskip=#1}
+\define@key {mprset}{lineskip}[]{\lineskip=#1}
+\define@key {mprset}{lessskip}[]{\lineskip=0.5\lineskip}
+\define@key {mprset}{flushleft}[]{\mpr@centerfalse}
+\define@key {mprset}{center}[]{\mpr@centertrue}
+\define@key {mprset}{rewrite}[]{\let \mpr@fraction \mpr@@rewrite}
+\define@key {mprset}{atop}[]{\let \mpr@fraction \mpr@@nofraction}
+\define@key {mprset}{myfraction}[]{\let \mpr@fraction #1}
+\define@key {mprset}{fraction}[]{\def \mpr@fraction {\mpr@make@fraction #1}}
+\define@key {mprset}{defaultfraction}[]{\let \mpr@fraction \mpr@@fraction}
+\define@key {mprset}{sep}{\def\mpr@sep{#1}}
+\define@key {mprset}{fractionaboveskip}{\def\mpr@@fractionaboveskip{#1}}
+\define@key {mprset}{fractionbelowskip}{\def\mpr@@fractionbelowskip{#1}}
+\define@key {mprset}{style}[1]{\def\TirNameStyle{#1}def}
+\define@key {mprset}{rightstyle}[1]{\def\RightTirNameStyle{#1}}
+\define@key {mprset}{leftstyle}[1]{\def\LeftTirNameStyle{#1}}
+\define@key {mprset}{vskip}[1]{\def \mpr@vskip{#1}}
+
+\newbox \mpr@right
+\define@key {mpr}{flushleft}[]{\mpr@centerfalse}
+\define@key {mpr}{center}[]{\mpr@centertrue}
+\define@key {mpr}{rewrite}[]{\let \mpr@fraction \mpr@@rewrite}
+\define@key {mpr}{myfraction}[]{\let \mpr@fraction #1}
+\define@key {mpr}{fraction}[]{\def \mpr@fraction {\mpr@make@fraction #1}}
+\define@key {mpr}{width}{\hsize #1}
+\define@key {mpr}{sep}{\def\mpr@sep{#1}}
+\define@key {mpr}{before}{#1}
+\define@key {mpr}{lab}{\let \DefTirName \LabTirName \def \mpr@rulename {#1}}
+\define@key {mpr}{Lab}{\let \DefTirName \LabTirName \def \mpr@rulename {#1}}
+\define@key {mpr}{style}[1]{\def\TirNameStyle{#1}def}
+\define@key {mpr}{rightstyle}[1]{\def\RightTirNameStyle{#1}}
+\define@key {mpr}{leftstyle}[1]{\def\LeftTirNameStyle{#1}}
+\define@key {mpr}{vskip}[1]{\def \mpr@vskip{#1}}
+\define@key {mpr}{narrower}{\hsize #1\hsize}
+\define@key {mpr}{leftskip}{\hskip -#1}
+\define@key {mpr}{reduce}[]{\let \mpr@fraction \mpr@@reduce}
+\define@key {mpr}{rightskip}
+  {\setbox \mpr@right \hbox {\unhbox \mpr@right \hskip -#1}}
+\define@key {mpr}{LEFT}{\setbox0 \hbox {$#1$}\relax
+     \advance \hsize by -\wd0\box0}
+
+\define@key {mpr}{left}{\setbox0 \hbox {$\LeftTirName {#1}\;$}\relax
+     \advance \hsize by -\wd0\box0}
+\define@key {mpr}{Left}{\llap{$\LeftTirName {#1}\;$}}
+\define@key {mpr}{right}
+  {\setbox0 \hbox {$\;\RightTirName {#1}$}\relax \advance \hsize by -\wd0
+   \setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}}
+\define@key {mpr}{RIGHT}
+  {\setbox0 \hbox {$#1$}\relax \advance \hsize by -\wd0
+   \setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}}
+\define@key {mpr}{Right}
+  {\setbox \mpr@right \hbox {\unhbox \mpr@right \rlap {$\;\RightTirName {#1}$}}}
+\define@key {mpr}{vdots}{\def \mpr@vdots {\@@atop \mpr@vdotfil{#1}}}
+\define@key {mpr}{after}{\edef \mpr@after {\mpr@after #1}}
+\define@key {mpr}{vcenter}[]{\mpr@vcentertrue}
+
+\newif \ifmpr@vcenter \mpr@vcenterfalse
+\newcommand \mpr@inferstar@ [3][]{\begingroup
+  \setbox0 \hbox
+        {\let \mpr@rulename \mpr@empty \let \mpr@vdots \relax
+         \setbox \mpr@right \hbox{}%
+         \setkeys{mpr}{#1}%
+         $\ifx \mpr@rulename \mpr@empty \mpr@inferrule {#2}{#3}\else
+          \mpr@inferrule [{\mpr@rulename}]{#2}{#3}\fi
+          \box \mpr@right \mpr@vdots$
+          \ifmpr@vcenter \aftergroup \mpr@vcentertrue \fi}
+  \ifmpr@vcenter
+     \box0
+  \else
+     \setbox1 \hbox {\strut}
+     \@tempdima \dp0 \advance \@tempdima by -\dp1
+     \raise \@tempdima \box0
+  \fi
+  \endgroup}
+
+\def \mpr@infer {\@ifnextchar *{\mpr@inferstar}{\mpr@inferrule}}
+\newcommand \mpr@err@skipargs[3][]{}
+\def \mpr@inferstar*{\ifmmode
+    \let \@do \mpr@inferstar@
+  \else
+    \let \@do \mpr@err@skipargs
+    \PackageError {mathpartir}
+      {\string\inferrule* can only be used in math mode}{}%
+  \fi \@do}
+
+%%% Exports
+
+
+\let \inferrule \mpr@infer
+
+\@ifundefined {infer}{\let \infer \mpr@infer}{}
+
+\def \TirNameStyle #1{\small \textsc{#1}}
+\def \LeftTirNameStyle #1{\TirNameStyle {#1}}
+\def \RightTirNameStyle #1{\TirNameStyle {#1}}
+
+\def \lefttir@name #1{\hbox {\small \LeftTirNameStyle{#1}}}
+\def \righttir@name #1{\hbox {\small \RightTirNameStyle{#1}}}
+\let \TirName \lefttir@name
+\let \LeftTirName \lefttir@name
+\let \DefTirName \lefttir@name
+\let \LabTirName \lefttir@name
+\let \RightTirName \righttir@name
+
+%%% Other Exports
+
+\endinput
+%%
+%% End of file `mathpartir.sty'.
diff --git a/tesi/mumble_meeting_gabriel b/tesi/mumble_meeting_gabriel
index 3436c00..d299e58 100644
--- a/tesi/mumble_meeting_gabriel
+++ b/tesi/mumble_meeting_gabriel
@@ -12,7 +12,7 @@ Test(S,true) = Yes
 
 
 -------------------------------
-equiv \emptyset Cs Ct gs ~> Yes
+equiv \emptyset Cs Ct gs \to Yes
 
 -----------------------------------------
 equiv S Failure (Leaf BBt) gs ~>No(vs, vt)
diff --git a/tesi/notations.sty b/tesi/notations.sty
new file mode 100644
index 0000000..a7c051c
--- /dev/null
+++ b/tesi/notations.sty
@@ -0,0 +1,36 @@
+\newcommand{\bnfeq}{\mathrel{::=}\;}
+\newcommand{\bnfor}{\mathrel{\vert}}
+
+\newcommand{\paramrel}[3]{#2 \mathrel{\approx_{#1}} #3}
+\newcommand{\vrel}[2]{\paramrel{\mathsf{val}}{#1}{#2}}
+\newcommand{\trel}[2]{\paramrel{\mathsf{term}}{#1}{#2}}
+
+\newcommand{\sem}[1]{{\llbracket{#1}\rrbracket}}
+
+\newcommand{\Fam}[2]{{(#2)}^{#1}}
+
+\newcommand{\match}[2]{\mathtt{match}(#1,#2)}
+
+\newcommand{\var}[1]{\mathtt{#1}}
+\newcommand{\pK}{\mathtt{K}}
+\newcommand{\any}{\mathtt{\_}}
+
+% \equiv is already taken
+\newcommand{\Equiv}[4]{\mathsf{equiv}(#1, #2, #3, #4)}
+\newcommand{\Equivrel}[4]{#1 \vdash_{#4} #2 \approx #3}
+
+\newcommand{\covers}[2]{#1 \mathrel{\mathsf{covers}} #2}
+
+\newcommand{\Yes}{\mathsf{Yes}}
+\newcommand{\No}[2]{\mathsf{No}(#1, #2)}
+
+\newcommand{\Leaf}[1]{\mathsf{Leaf}(#1)}
+\newcommand{\Failure}{\mathsf{Failure}}
+\newcommand{\Switch}[3]{\mathsf{Switch}(#1, #2, #3)}
+\newcommand{\Guard}[3]{\mathsf{Guard}(#1, #2, #3)}
+
+\newcommand{\emptyqueue}{\mathord{[]}}
+
+\newcommand{\Cfb}{C_{\mathsf{fb}}}
+
+\newcommand{\trim}[2]{\mathsf{trim}(#1, #2)}
\ No newline at end of file
diff --git a/tesi/tesi.pdf b/tesi/tesi.pdf
index 7089d0d..cc26d50 100644
Binary files a/tesi/tesi.pdf and b/tesi/tesi.pdf differ
diff --git a/tesi/tesi_unicode.org b/tesi/tesi_unicode.org
index 336adb1..f11e5c5 100644
--- a/tesi/tesi_unicode.org
+++ b/tesi/tesi_unicode.org
@@ -1,11 +1,11 @@
 \begin{comment}
 * TODO Scaletta [1/6]
   - [X] Introduction
-  - [-] Background [60%]
+  - [-] Background [80%]
     - [X] Low level representation
     - [X] Lambda code [0%]
     - [X] Pattern matching 
-    - [ ] Symbolic execution
+    - [X] Symbolic execution
     - [ ] Translation Validation
   - [ ] Translation validation of the Pattern Matching Compiler
     - [ ] Source translation
@@ -46,6 +46,27 @@ Magari prima pattern matching poi compilatore?
 #+LaTeX_HEADER: \newcommand{\covers}[2]{#1 \mathrel{\mathsf{covers}} #2}
 #+LaTeX_HEADER: \newcommand{\Yes}{\mathsf{Yes}}
 #+LaTeX_HEADER: \newcommand{\No}[2]{\mathsf{No}(#1, #2)}
+#+LaTeX_HEADER: \usepackage{comment}
+#+LaTeX_HEADER: \usepackage{mathpartir}
+#+LaTeX_HEADER: \usepackage{stmaryrd} % llbracket, rrbracket
+#+LaTeX_HEADER: \usepackage{listings}
+#+LaTeX_HEADER: \usepackage{notations}
+#+LaTeX_HEADER: \lstset{
+#+LaTeX_HEADER:  mathescape=true,
+#+LaTeX_HEADER:  language=[Objective]{Caml},
+#+LaTeX_HEADER:  basicstyle=\ttfamily,
+#+LaTeX_HEADER:  extendedchars=true,
+#+LaTeX_HEADER:  showstringspaces=false,
+#+LaTeX_HEADER:  aboveskip=\smallskipamount,
+#+LaTeX_HEADER:  % belowskip=\smallskipamount,
+#+LaTeX_HEADER:  columns=fullflexible,
+#+LaTeX_HEADER:  moredelim=**[is][\color{blue}]{/*}{*/},
+#+LaTeX_HEADER:  moredelim=**[is][\color{green!60!black}]{/!}{!/},
+#+LaTeX_HEADER:  moredelim=**[is][\color{orange}]{/(}{)/},
+#+LaTeX_HEADER:  moredelim=[is][\color{red}]{/[}{]/},
+#+LaTeX_HEADER:  xleftmargin=1em,
+#+LaTeX_HEADER: }
+#+LaTeX_HEADER: \lstset{aboveskip=0.4ex,belowskip=0.4ex}
 
 #+EXPORT_SELECT_TAGS: export
 #+EXPORT_EXCLUDE_TAGS: noexport
@@ -257,22 +278,22 @@ The algorithm respects the following correctness statement:
 
 The algorithm proceeds by case analysis. Inference rules are shown.
 If $S$ is empty the results is $\Yes$.
-
-\begin{verbatim}
-------------------------
-equiv \emptyset Cs Ct gs
-\end{verbatim}
+\begin{mathpar}
+  \infer{ }
+  {\Equivrel \emptyset {C_S} {C_T} G}
+\end{mathpar}
 
 If the two decision trees are both terminal nodes the algorithm checks
 for content equality.
-\begin{verbatim}
---------------------------
-equiv S Failure Failure []
+\begin{mathpar}
+  \infer{ }
+  {\Equivrel S \Failure \Failure \emptyqueue}
+\\
+  \infer
+  {\trel {t_S} {t_T}}
+  {\Equivrel S {\Leaf {t_S}} {\Leaf {t_T}} \emptyqueue}
 
-equiv_BB BBs BBt
--------------------------------
-equiv S (Leaf BBs) (Leaf BBt) []
-\end{verbatim}
+\end{mathpar}
 
 If the source decision tree (left hand side) is a terminal while the
 target decistion tree (right hand side) is not, the algorithm proceeds
@@ -280,13 +301,16 @@ by \emph{explosion} of the right hand side. Explosion means that every
 child of the right hand side is tested for equality against the left
 hand side.
 
-\begin{verbatim}
-(equiv S Cs Ci gs)^i
-equiv S Cs Cf gs
------------------------------------------
-equiv S Cs (Node(a, (Domi,Ci)^i, Cf)) gs
-\end{verbatim}
-
+\begin{mathpar}
+  \infer
+  {C_S \in {\Leaf t, \Failure}
+   \\
+   \forall i,\; \Equivrel {(S \land a \in D_i)} {C_S} {C_i} G
+   \\
+   \Equivrel {(S \land a \notin \Fam i {D_i})} {C_S} \Cfb G}
+  {\Equivrel S
+    {C_S} {\Switch a {\Fam i {D_i} {C_i}} \Cfb} G}
+\end{mathpar}
 
 \begin{comment}
 % TODO: [Gabriel] in practice the $dom_S$ are constructors and the
@@ -304,12 +328,20 @@ the accessors on both side are equal, and removing the branches that
 result in an empty intersection. If the accessors are different,
 \emph{$dom_T$} is left unchanged.
 
-\begin{verbatim}
-equiv S Ci (trim Ct a=Ki) gs
-equiv S Cf (trim Ct (a\notin(K_i)^i) gs
--------------------------------------
-equiv S (Node(a, (Ki,Ci)^i, Cf) Ct gs
-\end{verbatim}
+\begin{mathpar}
+  \infer
+  {\forall i,\;
+    \Equivrel
+      {(S \land a = K_i)}
+      {C_i} {\trim {C_T} {a = K_i}} G
+   \\
+   \Equivrel
+     {(S \land a \notin \Fam i {K_i})}
+     \Cfb {\trim {C_T} {a \notin \Fam i {K_i}}} G
+  }
+  {\Equivrel S
+    {\Switch a {\Fam i {K_i, C_i}} \Cfb} {C_T} G}
+\end{mathpar}
 
 The equivalence checking algorithm deals with guards by storing a
 queue. A guard blackbox is pushed to the queue whenever the algorithm
@@ -321,17 +353,21 @@ 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.
-\begin{verbatim}
-equiv S Ctrue Ct (gs++[condition])
-equiv S Cfalse Ct (gs++[condition])
---------------------------------------------
-equiv S (Guard condition Ctrue Cfalse) Ct gs
+\begin{mathpar}
+  \infer
+  {\Equivrel S {C_0} {C_T} {G, (t_S = 0)}
+   \\
+   \Equivrel S {C_1} {C_T} {G, (t_S = 1)}}
+  {\Equivrel S
+    {\Guard {t_S} {C_0} {C_1}} {C_T} G}
 
-equiv S Cs Ctrue gs
-equiv S Cs Cfalse gs
---------------------------------------------
-equiv S Cs (Guard condition Ctrue Cfalse) ([condition]++gs)
-\end{verbatim}
+  \infer
+  {\trel {t_S} {t_T}
+   \\
+   \Equivrel S {C_S} {C_b} G}
+  {\Equivrel S
+    {C_S} {\Guard {t_T} {C_0} {C_1}} {(t_S = b), G}}
+\end{mathpar}
 
 \begin{comment}
 TODO: replace inference rules with good latex
@@ -1129,6 +1165,106 @@ following four rules:
    apply, and P₂ → L₂ containing the remaining rows. The algorithm is
    applied to both matrices.
 
+** Target translation
+
+TODO
+
+** Equivalence checking
+
+The equivalence checking algorithm takes as input a domain of
+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.
+The algorithm respects the following correctness statement:
+
+% TODO: we have to define what \covers mean for readers to understand the specifications
+% (or we use a simplifying lie by hiding \covers in the statements).
+
+\begin{align*}
+ \Equiv S {C_S} {C_T} \emptyqueue = \Yes \;\land\; \covers {C_T} S
+ & \implies
+ \forall v_S \approx v_T \in S,\; C_S(v_S) = C_T(v_T)
+\\
+ \Equiv S {C_S} {C_T} \emptyqueue = \No {v_S} {v_T} \;\land\; \covers {C_T} S
+ & \implies
+ v_S \approx v_T \in S \;\land\; C_S(v_S) \neq C_T(v_T)
+\end{align*}
+
+Our equivalence-checking algorithm $\Equiv S {C_S} {C_T} G$ is
+a exactly decision procedure for the provability of the judgment
+$(\Equivrel S {C_S} {C_T} G)$, defined below.
+\begin{mathpar}
+  \begin{array}{l@{~}r@{~}l}
+    & & \text{\emph{constraint trees}} \\
+    C & \bnfeq & \Leaf t \\
+    & \bnfor & \Failure \\
+    & \bnfor & \Switch a {\Fam i {\pi_i, C_i}} \Cfb \\
+    & \bnfor & \Guard t {C_0} {C_1} \\
+  \end{array}
+
+  \begin{array}{l@{~}r@{~}l}
+    & & \text{\emph{boolean result}} \\
+    b & \in & \{ 0, 1 \} \\[0.5em]
+    & & \text{\emph{guard queues}} \\
+    G & \bnfeq & (t_1 = b_1), \dots, (t_n = b_n) \\
+  \end{array}
+
+  \begin{array}{l@{~}r@{~}l}
+    & & \text{\emph{input space}} \\
+    S & \subseteq & \{ (v_S, v_T) \mid \vrel {v_S} {v_T} \} \\
+  \end{array}
+  \\
+  \infer{ }
+  {\Equivrel \emptyset {C_S} {C_T} G}
+
+  \infer{ }
+  {\Equivrel S \Failure \Failure \emptyqueue}
+
+  \infer
+  {\trel {t_S} {t_T}}
+  {\Equivrel S {\Leaf {t_S}} {\Leaf {t_T}} \emptyqueue}
+
+  \infer
+  {\forall i,\;
+    \Equivrel
+      {(S \land a = K_i)}
+      {C_i} {\trim {C_T} {a = K_i}} G
+   \\
+   \Equivrel
+     {(S \land a \notin \Fam i {K_i})}
+     \Cfb {\trim {C_T} {a \notin \Fam i {K_i}}} G
+  }
+  {\Equivrel S
+    {\Switch a {\Fam i {K_i, C_i}} \Cfb} {C_T} G}
+
+\begin{comment}
+  % TODO explain somewhere why the judgment is not symmetric:
+  % we avoid defining trimming on source trees, which would
+  % require more expressive conditions than just constructors
+\end{comment}
+  \infer
+  {C_S \in {\Leaf t, \Failure}
+   \\
+   \forall i,\; \Equivrel {(S \land a \in D_i)} {C_S} {C_i} G
+   \\
+   \Equivrel {(S \land a \notin \Fam i {D_i})} {C_S} \Cfb G}
+  {\Equivrel S
+    {C_S} {\Switch a {\Fam i {D_i} {C_i}} \Cfb} G}
+
+  \infer
+  {\Equivrel S {C_0} {C_T} {G, (t_S = 0)}
+   \\
+   \Equivrel S {C_1} {C_T} {G, (t_S = 1)}}
+  {\Equivrel S
+    {\Guard {t_S} {C_0} {C_1}} {C_T} G}
+
+  \infer
+  {\trel {t_S} {t_T}
+   \\
+   \Equivrel S {C_S} {C_b} G}
+  {\Equivrel S
+    {C_S} {\Guard {t_T} {C_0} {C_1}} {(t_S = b), G}}
+\end{mathpar}
+
 * Correctness of the algorithm
 Running a program tₛ or its translation 〚tₛ〛 against an input vₛ
 produces as a result a result /r/ in the following way:
@@ -1258,7 +1394,41 @@ We define
 
 
 ** Proof of equivalence checking
+\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 → π relation (In other words???)
+| ∀vₜ ∈ (a→π), Cₜ(vₜ) = C_{t/a→π(kᵢ)}(vₜ)
+         We prove this by induction on Cₜ:
+               a. Case where Cₜ = Leaf_{bb}:
+                   Leaf_{bb/a→π}(v) = Leaf_{bb}(v) 
+                   That means that the result of trimming on a Leaf is
+                   the Leaf itself
+               b. Same for failure terminal
+               e. Unreachabe → ⊥
+               c. When Cₜ = Node(b, (π→Cᵢ)ⁱ)_{/a→π}  then
+                   we define πᵢ' =  πᵢ if a≠b else πᵢ∩π  ;
+                   Node(b, (π→Cᵢ)ⁱ)_{/a→π} :=  Node(b, (π'ᵢ→C_{i/a→π})ⁱ)
 
+                   Goal: prove that Cₜ(vₜ) = Node(b, (πᵢ'→C_{i/a→π})ⁱ)(vₜ)
+                   Either vₜ∉(b→πᵢ)ⁱ and that means that the node is a Failure node
+                   Or vₜ∈(b→πₖ) for some k, then
+                       C_{k/a→π}(vₜ) = Node(b, (πᵢ'→C_{i/a→π})ⁱ)(vₜ)
+                   because when a ≠ b then πₖ'= πₖ => vₜ∈πₖ'
+                   while when a = b  then πₖ'=(πₖ∩π)
+                     - vₜ∈π because of hypothesis
+                     - we already know that vₜ∈πₖ
+                     So vₜ ∈ πₖ' and by induction Cₖ(vₜ) = C_{k/a→π}(vₜ)
+                     and Cₜ(vₜ) = Cₖ(vₜ) when vₜ∈(b→πₖ)
+                    This proves that Node(b, (πᵢ'→C_{i/a→π})ⁱ)(vₜ) = Cₜ(vₜ)
+                            
+   Covering lemma:
+         ∀a,π covers(Cₜ,S) => covers(C_{t/a→π}, (S∩a→π))
+             Uᵢπⁱ ≈ Uᵢπ'∩(a→π) ≈ (Uᵢπ')∩(a→π) %% # TODO swap π and π' 
+
+\subsubsection Proof of equivalence checking
 The equivalence checking algorithm takes as parameters an input space
 /S/, a source decision tree /Cₛ/ and a target decision tree /Cₜ/:
 | equiv(S, Cₛ, Cₜ) → Yes | No(vₛ, vₜ)
@@ -1297,6 +1467,7 @@ We proceed by case analysis:
 Devo spiegarlo?
 \end{comment}
 In the other subcases S is always non-empty.
+0. in case of unreachable: Cₛ(vₛ) = Absurd(Unreachable) ≠ Cₜ(vₜ) ∀vₛ,vₜ
 2. equiv(S, Failure, Failure) := Yes
    the statement holds because of equality between Failure nodes in
    the case of every possible value /v/.
@@ -1318,3 +1489,23 @@ In the other subcases S is always non-empty.
    | vₛ≃vₜ∈S ∧ Cₛ(vₛ)≠Cₜ(vₜ) 
    and the result of the algorithm is
    | equiv(Sᵢ, Cₛ, Cₜᵢ) = No(vₛ, vₜ) for some minimal k∈I
+4. equiv(S, Node(a, (kᵢ → Cₛᵢ)ⁱ, C_{sf}), Cₜ) := 
+    let π' = ⋃π(kᵢ) ∀i in
+    Forall(equiv( S∩(a→π(kᵢ)ⁱ), Cₛᵢ, C_{t/a→π(kᵢ)})ⁱ +++   equiv(S∩(a→π(kᵢ)), Cₛ, C_{/a¬̸π'}))
+    The statement  holds because:
+    a. Forall(equiv( S∩(a→π(kᵢ)ⁱ), Cₛᵢ, C_{t/a→π(kᵢ)})ⁱ = Yes
+       In the yes case let's reason by case analysis:
+       i. When k∈(kᵢ)ⁱ
+            there is a k=kₖ for some k and this means that Cₛ(vₛ) = Cₛᵢ(vₛ)
+            By induction we know that  Cₛᵢ(vₛ) = c_{t/a→πᵢ}(vₜ)
+            and because of the trimming lemma:
+            Cₜ(vₜ) = C_{t/a→πᵢ}(vₜ)
+            Putting all together:
+            Cₛ(vₛ) = Cₛᵢ(vₛ) = C_{t/a→πᵢ}(vₜ) = Cₜ(vₜ)
+            
+       ii. or k∉(kᵢ)ⁱ ???
+
+    b. Forall(...) = No(vₛ, vₜ)
+        for a minimum k, equiv(Sₖ, Cₛₖ, C_{t/a→πₖ} = No(vₛ, vₜ)
+           then Cₛₖ(vₛ) ≠ C_{t/a→πₖ}(vₜ)  and C_{t/a→πₖ}(vₜ) = Cₜ(vt) 
+             => (Cₛₖ(vₛ) = Cₛ(vₛ)) ≠ Cₜ(vₜ) # Same for fallback?