From 28a48f475540b149a042e27fc2e125b1497194f3 Mon Sep 17 00:00:00 2001
From: Francesco Mecca <me@francescomecca.eu>
Date: Sat, 11 Apr 2020 00:31:10 +0200
Subject: [PATCH] mail gabriel e coppo

---
 tesi/.gitignore            |   1 -
 tesi/gabriel/notations.sty |   1 +
 tesi/gabriel/part4.pdf     | Bin 308599 -> 308599 bytes
 tesi/gabriel/part4.tex     |  12 ++++++------
 4 files changed, 7 insertions(+), 7 deletions(-)
 create mode 120000 tesi/gabriel/notations.sty

diff --git a/tesi/.gitignore b/tesi/.gitignore
index 03ea693..bbd865c 100644
--- a/tesi/.gitignore
+++ b/tesi/.gitignore
@@ -3,7 +3,6 @@ tesi.tex
 
 tesi_unicode.tex
 part4_unicode.tex
-part4.tex
                      
 
 ## Core latex/pdflatex auxiliary files:
diff --git a/tesi/gabriel/notations.sty b/tesi/gabriel/notations.sty
new file mode 120000
index 0000000..24ae4a2
--- /dev/null
+++ b/tesi/gabriel/notations.sty
@@ -0,0 +1 @@
+../notations.sty
\ No newline at end of file
diff --git a/tesi/gabriel/part4.pdf b/tesi/gabriel/part4.pdf
index 4d09d10c6684cd526c482ec7f380a3f3d43bee25..a91659ee326c9966e5952bec3a39572da4649d3e 100644
GIT binary patch
delta 112
zcmezVO6dD5p@tU57N!>FEiB9{Sd0w~OsBK2V37y2wrj0m*~#T>ZeZ-};%sK<W?<-S
jYG7$#Zs6o%=3->(WNGH&>ga4~r(i=!$#%8PEP+e_KNKDV

delta 112
zcmezVO6dD5p@tU57N!>FEiB9{Sd7e!45qWMV37y2wrj0m*~#VXX5wP$Y+&eWXl&|i
jW?|y&?C9uZVPNWHY++<>;O1gzr(i=!$#%8PEP+e_MTi~&

diff --git a/tesi/gabriel/part4.tex b/tesi/gabriel/part4.tex
index a0d244c..017c251 100644
--- a/tesi/gabriel/part4.tex
+++ b/tesi/gabriel/part4.tex
@@ -1,4 +1,4 @@
-% Created 2020-04-11 Sat 00:26
+% Created 2020-04-11 Sat 00:31
 % Intended LaTeX compiler: pdflatex
 \documentclass[11pt]{article}
 \usepackage[utf8]{inputenc}
@@ -64,10 +64,10 @@ xleftmargin=1em,
 \begin{document}
 
 \section{Translation validation of the Pattern Matching Compiler}
-\label{sec:org3d79c1b}
+\label{sec:org9d32dd4}
 
 \subsection{Source program}
-\label{sec:orgc2c278d}
+\label{sec:org0032637}
 The algorithm takes as its input a source program and translates it
 into an algebraic data structure which type we call \emph{decision\_tree}.
 
@@ -412,7 +412,7 @@ TODO: fix \{0}
 
 \begin{enumerate}
 \item Proof:
-\label{sec:org160a47b}
+\label{sec:orgb73fb4f}
 Let \(m\) be a matrix with \[Group(m) = (k_r \to m_r)^k, m_{wild}\]
 Let \((v_i)^i\) be an input matrix with \(v_0 = k(v'_l)^l\) for some k.
 We proceed by case analysis:
@@ -472,7 +472,7 @@ We can also show that a$_i$ = (a\(_{\text{0.l}}\))$^l$ \sout{+} a\(_{\text{i$\in
 
 
 \subsection{Target translation}
-\label{sec:orgd2ea1d0}
+\label{sec:org0337fa8}
 
 The target program of the following general form is parsed using a parser
 generated by Menhir, a LR(1) parser generator for the OCaml programming language.
@@ -560,7 +560,7 @@ $\forall$v$_T$, t$_T$(v$_T$) = $\llbracket$t$_T$$\rrbracket$$_T$(v$_T$)\\
 
 
 \subsection{Equivalence checking}
-\label{sec:org33b978b}
+\label{sec:org7268798}
 
 The equivalence checking algorithm takes as input a domain of
 possible values \emph{S} and a pair of source and target decision trees and