Add missing parts + cleanupHEADmaster

15 files changed, 1916 insertions, 409 deletions

diff --git a/.gitignore b/.gitignore
index 55388df..017ff35 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,5 +1,6 @@
 auto
 _region_.tex
+_minted-tfm
 *.aux
 *.bbl
 *.blg
diff --git a/Makefile b/Makefile
index 1ca0edb..3e0dba0 100644
--- a/Makefile
+++ b/Makefile
@@ -10,6 +10,6 @@ force:
 re: clean all
 
 clean:
-	rm -rf _region_.tex *.aux *.bbl *.blg *.brf *.dvi *.fdb_latexmk *.fls *.fmt *.idx *.log *.lol *.out *.prv *.toc *.pyg
+	rm -rf _region_.tex _minted-tfm *.aux *.bbl *.blg *.brf *.dvi *.fdb_latexmk *.fls *.fmt *.idx *.log *.lol *.out *.prv *.toc *.pyg
 
 .PHONY : all clean re
diff --git a/bib.bib b/bib.bib
index 4c559f3..3eb97ee 100644
--- a/bib.bib
+++ b/bib.bib
@@ -223,3 +223,31 @@ author={Mogensen, TorbenÆ.},
 pages={128-142},
 language={English}
 }
+
+@article{Coquand88,
+ author = {Coquand, Thierry and Huet, Gerard},
+ title = {The Calculus of Constructions},
+ journal = {Inf. Comput.},
+ issue_date = {February/March 1988},
+ volume = {76},
+ number = {2-3},
+ month = feb,
+ year = {1988},
+ issn = {0890-5401},
+ pages = {95--120},
+ numpages = {26},
+ url = {http://dx.doi.org/10.1016/0890-5401(88)90005-3},
+ doi = {10.1016/0890-5401(88)90005-3},
+ acmid = {47725},
+ publisher = {Academic Press, Inc.},
+ address = {Duluth, MN, USA},
+}
+
+@book{Baader98,
+ author = {Baader, Franz and Nipkow, Tobias},
+ title = {Term Rewriting and All That},
+ year = {1998},
+ isbn = {0-521-45520-0},
+ publisher = {Cambridge University Press},
+ address = {New York, NY, USA},
+}
diff --git a/from-copy.sh b/from-copy.sh
deleted file mode 100755
index 3321f23..0000000
--- a/from-copy.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-#!/bin/bash
-
-COPY_D="${HOME}/Copy/univ/master/tfm"
-
-cp -r ${COPY_D}/code ${COPY_D}/tfm.pdf ${COPY_D}/*.tex ${COPY_D}/Makefile ${COPY_D}/bib.bib .
-cp -r ${COPY_D}/front/*.tex front/
diff --git a/img/easycrypt.png b/img/easycrypt.png
new file mode 100644
index 0000000..a6d568a
--- /dev/null
+++ b/img/easycrypt.png
diff --git a/img/ec1.png b/img/ec1.png
new file mode 100644
index 0000000..c6b24d0
--- /dev/null
+++ b/img/ec1.png
diff --git a/img/ec2.png b/img/ec2.png
new file mode 100644
index 0000000..764962a
--- /dev/null
+++ b/img/ec2.png
diff --git a/img/ec3.png b/img/ec3.png
new file mode 100644
index 0000000..24f6f8d
--- /dev/null
+++ b/img/ec3.png
diff --git a/img/ec4.png b/img/ec4.png
new file mode 100644
index 0000000..6232c18
--- /dev/null
+++ b/img/ec4.png
diff --git a/img/ec5.png b/img/ec5.png
new file mode 100644
index 0000000..133f09d
--- /dev/null
+++ b/img/ec5.png
diff --git a/img/zamrules.png b/img/zamrules.png
new file mode 100644
index 0000000..a019ad8
--- /dev/null
+++ b/img/zamrules.png
diff --git a/minted.sty b/minted.sty
index 0e0585c..7fef35a 100644
--- a/minted.sty
+++ b/minted.sty
@@ -5,6 +5,7 @@
 %% The original source files were:
 %%
 %% minted.dtx  (with options: `package')
+%% Copyright 2013--2015 Geoffrey M. Poore
 %% Copyright 2010--2011 Konrad Rudolph
 %% 
 %% This work may be distributed and/or modified under the
@@ -20,220 +21,1201 @@
 %% 
 %% This work has the LPPL maintenance status `maintained'.
 %% 
-%% The Current Maintainer of this work is Konrad Rudolph.
+%% The Current Maintainer of this work is Geoffrey Poore.
 %% 
 %% This work consists of the files minted.dtx and minted.ins
 %% and the derived file minted.sty.
 \NeedsTeXFormat{LaTeX2e}
-\ProvidesPackage{minted}[2011/09/17 v1.7 Yet another Pygments shim for LaTeX]
+\ProvidesPackage{minted}
+    [2015/01/31 v2.0 Yet another Pygments shim for LaTeX]
 \RequirePackage{keyval}
+\RequirePackage{kvoptions}
 \RequirePackage{fancyvrb}
-\RequirePackage{xcolor}
 \RequirePackage{float}
 \RequirePackage{ifthen}
 \RequirePackage{calc}
 \RequirePackage{ifplatform}
-\DeclareOption{chapter}{\def\minted@float@within{chapter}}
-\DeclareOption{section}{\def\minted@float@within{section}}
-\ProcessOptions\relax
+\RequirePackage{pdftexcmds}
+\RequirePackage{etoolbox}
+\RequirePackage{xstring}
+\RequirePackage{lineno}
+\AtBeginDocument{%
+  \@ifpackageloaded{color}{}{%
+    \@ifpackageloaded{xcolor}{}{\RequirePackage{xcolor}}}%
+}
+\DeclareVoidOption{chapter}{\def\minted@float@within{chapter}}
+\DeclareVoidOption{section}{\def\minted@float@within{section}}
+\DeclareBoolOption{newfloat}
+\DeclareBoolOption[true]{cache}
+\StrSubstitute{\jobname}{ }{_}[\minted@jobname]
+\StrSubstitute{\minted@jobname}{"}{}[\minted@jobname]
+\StrSubstitute{\minted@jobname}{*}{-}[\minted@jobname]
+\newcommand{\minted@cachedir}{\detokenize{_}minted-\minted@jobname}
+\let\minted@cachedir@windows\minted@cachedir
+\define@key{minted}{cachedir}{%
+  \@namedef{minted@cachedir}{#1}%
+  \StrSubstitute{\minted@cachedir}{/}{\@backslashchar}[\minted@cachedir@windows]}
+\let\minted@outputdir\@empty
+\let\minted@outputdir@windows\@empty
+\define@key{minted}{outputdir}{%
+  \@namedef{minted@outputdir}{#1/}%
+  \StrSubstitute{\minted@outputdir}{/}%
+    {\@backslashchar}[\minted@outputdir@windows]}
+\DeclareBoolOption{kpsewhich}
+\DeclareBoolOption{langlinenos}
+\DeclareBoolOption{draft}
+\DeclareComplementaryOption{final}{draft}
+\ProcessKeyvalOptions*
+\ifthenelse{\boolean{minted@newfloat}}{\RequirePackage{newfloat}}{}
+\ifthenelse{\boolean{minted@cache}}{%
+  \AtEndOfPackage{\ProvideDirectory{\minted@outputdir\minted@cachedir}}}{}
+\newcommand{\minted@input}[1]{%
+  \IfFileExists{#1}%
+   {\input{#1}}%
+   {\PackageError{minted}{Missing Pygments output; \string\inputminted\space
+     was^^Jprobably given a file that does not exist--otherwise, you may need
+     ^^Jthe outputdir package option, or may be using an incompatible build
+     tool\ifwindows,^^Jor may be using the kpsewhich option without having
+     PowerShell installed\fi}%
+    {This could be caused by using -output-directory or -aux-directory
+     ^^Jwithout setting minted's outputdir, or by using a build tool that
+     ^^Jchanges paths in ways minted cannot detect\ifwindows, or by using the
+     ^^Jkpsewhich option without PowerShell\fi.}}%
+}
+\newcommand{\minted@infile}{\jobname.out.pyg}
+\newcommand{\minted@cachelist}{}
+\newcommand{\minted@addcachefile}[1]{%
+  \expandafter\long\expandafter\gdef\expandafter\minted@cachelist\expandafter{%
+    \minted@cachelist,^^J%
+    \space\space#1}%
+  \expandafter\gdef\csname minted@cached@#1\endcsname{}%
+}
+\newcommand{\minted@savecachelist}{%
+  \ifdefempty{\minted@cachelist}{}{%
+    \immediate\write\@mainaux{%
+      \string\gdef\string\minted@oldcachelist\string{%
+        \minted@cachelist\string}}%
+  }%
+}
+\newcommand{\minted@cleancache}{%
+  \ifcsname minted@oldcachelist\endcsname
+    \def\do##1{%
+      \ifthenelse{\equal{##1}{}}{}{%
+        \ifcsname minted@cached@##1\endcsname\else
+          \DeleteFile[\minted@outputdir\minted@cachedir]{##1}%
+        \fi
+      }%
+    }%
+    \expandafter\docsvlist\expandafter{\minted@oldcachelist}%
+  \else
+  \fi
+}
+\ifthenelse{\boolean{minted@draft}}%
+  {\AtEndDocument{%
+      \ifcsname minted@oldcachelist\endcsname
+        \let\minted@cachelist\minted@oldcachelist
+        \minted@savecachelist
+      \fi}}%
+  {\AtEndDocument{%
+      \minted@savecachelist
+      \minted@cleancache}}%
+\ifwindows
+  \providecommand{\DeleteFile}[2][]{%
+    \ifthenelse{\equal{#1}{}}%
+      {\IfFileExists{#2}{\immediate\write18{del "#2"}}{}}%
+      {\IfFileExists{#1/#2}{%
+        \StrSubstitute{#1}{/}{\@backslashchar}[\minted@windir]
+        \immediate\write18{del "\minted@windir\@backslashchar #2"}}{}}}
+\else
+  \providecommand{\DeleteFile}[2][]{%
+    \ifthenelse{\equal{#1}{}}%
+      {\IfFileExists{#2}{\immediate\write18{rm "#2"}}{}}%
+      {\IfFileExists{#1/#2}{\immediate\write18{rm "#1/#2"}}{}}}
+\fi
 \ifwindows
-  \providecommand\DeleteFile[1]{\immediate\write18{del #1}}
+  \newcommand{\ProvideDirectory}[1]{%
+    \StrSubstitute{#1}{/}{\@backslashchar}[\minted@windir]
+    \immediate\write18{if not exist "\minted@windir" mkdir "\minted@windir"}}
 \else
-  \providecommand\DeleteFile[1]{\immediate\write18{rm #1}}
+  \newcommand{\ProvideDirectory}[1]{%
+    \immediate\write18{mkdir -p "#1"}}
 \fi
 \newboolean{AppExists}
-\newcommand\TestAppExists[1]{
+\newread\minted@appexistsfile
+\newcommand{\TestAppExists}[1]{
   \ifwindows
     \DeleteFile{\jobname.aex}
     \immediate\write18{for \string^\@percentchar i in (#1.exe #1.bat #1.cmd)
-      do set >\jobname.aex <nul: /p x=\string^\@percentchar \string~$PATH:i>>\jobname.aex} %$
-    \newread\@appexistsfile
-    \immediate\openin\@appexistsfile\jobname.aex
+      do set >"\jobname.aex" <nul: /p
+      x=\string^\@percentchar \string~$PATH:i>>"\jobname.aex"}
+    %$ <- balance syntax highlighting
+    \immediate\openin\minted@appexistsfile\jobname.aex
     \expandafter\def\expandafter\@tmp@cr\expandafter{\the\endlinechar}
     \endlinechar=-1\relax
-    \readline\@appexistsfile to \@apppathifexists
+    \readline\minted@appexistsfile to \minted@apppathifexists
     \endlinechar=\@tmp@cr
-    \ifthenelse{\equal{\@apppathifexists}{}}
+    \ifthenelse{\equal{\minted@apppathifexists}{}}
      {\AppExistsfalse}
      {\AppExiststrue}
-    \immediate\closein\@appexistsfile
+    \immediate\closein\minted@appexistsfile
     \DeleteFile{\jobname.aex}
-\immediate\typeout{file deleted}
   \else
-    \immediate\write18{which #1 && touch \jobname.aex}
+    \immediate\write18{which "#1" && touch "\jobname.aex"}
     \IfFileExists{\jobname.aex}
-     {\AppExiststrue
-      \DeleteFile{\jobname.aex}}
-     {\AppExistsfalse}
-  \fi}
-\newcommand\minted@resetoptions{}
-\newcommand\minted@defopt[1]{
-  \expandafter\def\expandafter\minted@resetoptions\expandafter{%
-    \minted@resetoptions
-    \@namedef{minted@opt@#1}{}}}
-\newcommand\minted@opt[1]{
-  \expandafter\detokenize%
-    \expandafter\expandafter\expandafter{\csname minted@opt@#1\endcsname}}
-\newcommand\minted@define@opt[3][]{
-  \minted@defopt{#2}
-  \ifthenelse{\equal{#1}{}}{
-    \define@key{minted@opt}{#2}{\@namedef{minted@opt@#2}{#3}}}
-   {\define@key{minted@opt}{#2}[#1]{\@namedef{minted@opt@#2}{#3}}}}
-\newcommand\minted@define@switch[3][]{
-  \minted@defopt{#2}
-  \define@booleankey{minted@opt}{#2}
-   {\@namedef{minted@opt@#2}{#3}}
-   {\@namedef{minted@opt@#2}{#1}}}
-\minted@defopt{extra}
-\newcommand\minted@define@extra[1]{
-  \define@key{minted@opt}{#1}{
-    \expandafter\def\expandafter\minted@opt@extra\expandafter{%
-      \minted@opt@extra,#1=##1}}}
-\newcommand\minted@define@extra@switch[1]{
-  \define@booleankey{minted@opt}{#1}
-   {\expandafter\def\expandafter\minted@opt@extra\expandafter{%
-      \minted@opt@extra,#1}}
-   {\expandafter\def\expandafter\minted@opt@extra\expandafter{%
-      \minted@opt@extra,#1=false}}}
-\minted@define@switch{texcl}{-P texcomments}
-\minted@define@switch{mathescape}{-P mathescape}
-\minted@define@switch{linenos}{-P linenos}
-\minted@define@switch{startinline}{-P startinline}
-\minted@define@switch[-P funcnamehighlighting=False]%
-  {funcnamehighlighting}{-P funcnamehighlighting}
-\minted@define@opt{gobble}{-F gobble:n=#1}
-\minted@define@opt{bgcolor}{#1}
-\minted@define@extra{frame}
-\minted@define@extra{framesep}
-\minted@define@extra{framerule}
-\minted@define@extra{rulecolor}
-\minted@define@extra{numbersep}
-\minted@define@extra{firstnumber}
-\minted@define@extra{stepnumber}
-\minted@define@extra{firstline}
-\minted@define@extra{lastline}
-\minted@define@extra{baselinestretch}
-\minted@define@extra{xleftmargin}
-\minted@define@extra{xrightmargin}
-\minted@define@extra{fillcolor}
-\minted@define@extra{tabsize}
-\minted@define@extra{fontfamily}
-\minted@define@extra{fontsize}
-\minted@define@extra{fontshape}
-\minted@define@extra{fontseries}
-\minted@define@extra{formatcom}
-\minted@define@extra{label}
-\minted@define@extra@switch{numberblanklines}
-\minted@define@extra@switch{showspaces}
-\minted@define@extra@switch{resetmargins}
-\minted@define@extra@switch{samepage}
-\minted@define@extra@switch{showtabs}
-\minted@define@extra@switch{obeytabs}
+      {\AppExiststrue
+        \DeleteFile{\jobname.aex}}
+      {\AppExistsfalse}
+  \fi
+}
+\newcommand{\minted@optlistcl@g}{}
+\newcommand{\minted@optlistcl@g@i}{}
+\let\minted@lang\@empty
+\newcommand{\minted@optlistcl@lang}{}
+\newcommand{\minted@optlistcl@lang@i}{}
+\newcommand{\minted@optlistcl@cmd}{}
+\newcommand{\minted@optlistfv@g}{}
+\newcommand{\minted@optlistfv@g@i}{}
+\newcommand{\minted@optlistfv@lang}{}
+\newcommand{\minted@optlistfv@lang@i}{}
+\newcommand{\minted@optlistfv@cmd}{}
+\newcommand{\minted@configlang}[1]{%
+  \def\minted@lang{#1}%
+  \ifcsname minted@optlistcl@lang\minted@lang\endcsname\else
+    \expandafter\gdef\csname minted@optlistcl@lang\minted@lang\endcsname{}%
+  \fi
+  \ifcsname minted@optlistcl@lang\minted@lang @i\endcsname\else
+    \expandafter\gdef\csname minted@optlistcl@lang\minted@lang @i\endcsname{}%
+  \fi
+  \ifcsname minted@optlistfv@lang\minted@lang\endcsname\else
+    \expandafter\gdef\csname minted@optlistfv@lang\minted@lang\endcsname{}%
+  \fi
+  \ifcsname minted@optlistfv@lang\minted@lang @i\endcsname\else
+    \expandafter\gdef\csname minted@optlistfv@lang\minted@lang @i\endcsname{}%
+  \fi
+}
+\newcommand{\minted@addto@optlistcl}[2]{%
+  \expandafter\def\expandafter#1\expandafter{#1%
+    \detokenize{#2}\space}}
+\newcommand{\minted@addto@optlistcl@lang}[2]{%
+  \expandafter\let\expandafter\minted@tmp\csname #1\endcsname
+  \expandafter\def\expandafter\minted@tmp\expandafter{\minted@tmp%
+    \detokenize{#2}\space}%
+  \expandafter\let\csname #1\endcsname\minted@tmp}
+\newcommand{\minted@def@optcl}[4][]{%
+  \ifthenelse{\equal{#1}{}}%
+    {\define@key{minted@opt@g}{#2}{%
+        \minted@addto@optlistcl{\minted@optlistcl@g}{#3=#4}%
+        \@namedef{minted@opt@g:#2}{#4}}%
+      \define@key{minted@opt@g@i}{#2}{%
+        \minted@addto@optlistcl{\minted@optlistcl@g@i}{#3=#4}%
+        \@namedef{minted@opt@g@i:#2}{#4}}%
+      \define@key{minted@opt@lang}{#2}{%
+        \minted@addto@optlistcl@lang{minted@optlistcl@lang\minted@lang}{#3=#4}%
+        \@namedef{minted@opt@lang\minted@lang:#2}{#4}}%
+      \define@key{minted@opt@lang@i}{#2}{%
+        \minted@addto@optlistcl@lang{%
+          minted@optlistcl@lang\minted@lang @i}{#3=#4}%
+        \@namedef{minted@opt@lang\minted@lang @i:#2}{#4}}%
+      \define@key{minted@opt@cmd}{#2}{%
+        \minted@addto@optlistcl{\minted@optlistcl@cmd}{#3=#4}%
+        \@namedef{minted@opt@cmd:#2}{#4}}}%
+    {\define@key{minted@opt@g}{#2}[#1]{%
+        \minted@addto@optlistcl{\minted@optlistcl@g}{#3=#4}%
+        \@namedef{minted@opt@g:#2}{#4}}%
+      \define@key{minted@opt@g@i}{#2}[#1]{%
+        \minted@addto@optlistcl{\minted@optlistcl@g@i}{#3=#4}%
+        \@namedef{minted@opt@g@i:#2}{#4}}%
+      \define@key{minted@opt@lang}{#2}[#1]{%
+        \minted@addto@optlistcl@lang{minted@optlistcl@lang\minted@lang}{#3=#4}%
+        \@namedef{minted@opt@lang\minted@lang:#2}{#4}}%
+      \define@key{minted@opt@lang@i}{#2}[#1]{%
+        \minted@addto@optlistcl@lang{%
+          minted@optlistcl@lang\minted@lang @i}{#3=#4}%
+        \@namedef{minted@opt@lang\minted@lang @i:#2}{#4}}%
+      \define@key{minted@opt@cmd}{#2}[#1]{%
+        \minted@addto@optlistcl{\minted@optlistcl@cmd}{#3=#4}%
+        \@namedef{minted@opt@cmd:#2}{#4}}}%
+}
+\edef\minted@hashchar{\string#}
+\edef\minted@dollarchar{\string$}
+\edef\minted@ampchar{\string&}
+\edef\minted@underscorechar{\string_}
+\edef\minted@tildechar{\string~}
+\newcommand{\minted@escchars}{%
+  \let\#\minted@hashchar
+  \let\%\@percentchar
+  \let\{\@charlb
+  \let\}\@charrb
+  \let\$\minted@dollarchar
+  \let\&\minted@ampchar
+  \let\_\minted@underscorechar
+  \let\\\@backslashchar
+  \let~\minted@tildechar
+  \let\~\minted@tildechar
+} %$ <- highlighting
+\newcommand{\minted@addto@optlistcl@e}[2]{%
+  \begingroup
+  \minted@escchars
+  \xdef\minted@xtmp{#2}%
+  \endgroup
+  \expandafter\minted@addto@optlistcl@e@i\expandafter{\minted@xtmp}{#1}}
+\def\minted@addto@optlistcl@e@i#1#2{%
+  \expandafter\def\expandafter#2\expandafter{#2#1\space}}
+\newcommand{\minted@addto@optlistcl@lang@e}[2]{%
+  \begingroup
+  \minted@escchars
+  \xdef\minted@xtmp{#2}%
+  \endgroup
+  \expandafter\minted@addto@optlistcl@lang@e@i\expandafter{\minted@xtmp}{#1}}
+\def\minted@addto@optlistcl@lang@e@i#1#2{%
+  \expandafter\let\expandafter\minted@tmp\csname #2\endcsname
+  \expandafter\def\expandafter\minted@tmp\expandafter{\minted@tmp#1\space}%
+  \expandafter\let\csname #2\endcsname\minted@tmp}
+\newcommand{\minted@def@optcl@e}[4][]{%
+  \ifthenelse{\equal{#1}{}}%
+    {\define@key{minted@opt@g}{#2}{%
+        \minted@addto@optlistcl@e{\minted@optlistcl@g}{#3=#4}%
+        \@namedef{minted@opt@g:#2}{#4}}%
+      \define@key{minted@opt@g@i}{#2}{%
+        \minted@addto@optlistcl@e{\minted@optlistcl@g@i}{#3=#4}%
+        \@namedef{minted@opt@g@i:#2}{#4}}%
+      \define@key{minted@opt@lang}{#2}{%
+        \minted@addto@optlistcl@lang@e{minted@optlistcl@lang\minted@lang}{#3=#4}%
+        \@namedef{minted@opt@lang\minted@lang:#2}{#4}}%
+      \define@key{minted@opt@lang@i}{#2}{%
+        \minted@addto@optlistcl@lang@e{%
+          minted@optlistcl@lang\minted@lang @i}{#3=#4}%
+        \@namedef{minted@opt@lang\minted@lang @i:#2}{#4}}%
+      \define@key{minted@opt@cmd}{#2}{%
+        \minted@addto@optlistcl@e{\minted@optlistcl@cmd}{#3=#4}%
+        \@namedef{minted@opt@cmd:#2}{#4}}}%
+    {\define@key{minted@opt@g}{#2}[#1]{%
+        \minted@addto@optlistcl@e{\minted@optlistcl@g}{#3=#4}%
+        \@namedef{minted@opt@g:#2}{#4}}%
+      \define@key{minted@opt@g@i}{#2}[#1]{%
+        \minted@addto@optlistcl@e{\minted@optlistcl@g@i}{#3=#4}%
+        \@namedef{minted@opt@g@i:#2}{#4}}%
+      \define@key{minted@opt@lang}{#2}[#1]{%
+        \minted@addto@optlistcl@lang@e{minted@optlistcl@lang\minted@lang}{#3=#4}%
+        \@namedef{minted@opt@lang\minted@lang:#2}{#4}}%
+      \define@key{minted@opt@lang@i}{#2}[#1]{%
+        \minted@addto@optlistcl@lang@e{%
+          minted@optlistcl@lang\minted@lang @i}{#3=#4}%
+        \@namedef{minted@opt@lang\minted@lang @i:#2}{#4}}%
+      \define@key{minted@opt@cmd}{#2}[#1]{%
+        \minted@addto@optlistcl@e{\minted@optlistcl@cmd}{#3=#4}%
+        \@namedef{minted@opt@cmd:#2}{#4}}}%
+}
+\newcommand{\minted@def@optcl@style}{%
+  \define@key{minted@opt@g}{style}{%
+    \minted@addto@optlistcl{\minted@optlistcl@g}%
+      {-P style=##1 -P commandprefix=PYG##1}%
+    \minted@checkstyle{##1}%
+    \@namedef{minted@opt@g:style}{##1}}%
+  \define@key{minted@opt@g@i}{style}{%
+    \minted@addto@optlistcl{\minted@optlistcl@g@i}%
+      {-P style=##1 -P commandprefix=PYG##1}%
+    \minted@checkstyle{##1}%
+    \@namedef{minted@opt@g@i:style}{##1}}%
+  \define@key{minted@opt@lang}{style}{%
+    \minted@addto@optlistcl@lang{minted@optlistcl@lang\minted@lang}%
+      {-P style=##1 -P commandprefix=PYG##1}%
+    \minted@checkstyle{##1}%
+    \@namedef{minted@opt@lang\minted@lang:style}{##1}}%
+  \define@key{minted@opt@lang@i}{style}{%
+    \minted@addto@optlistcl@lang{minted@optlistcl@lang\minted@lang @i}%
+      {-P style=##1 -P commandprefix=PYG##1}%
+    \minted@checkstyle{##1}%
+    \@namedef{minted@opt@lang\minted@lang @i:style}{##1}}%
+  \define@key{minted@opt@cmd}{style}{%
+    \minted@addto@optlistcl{\minted@optlistcl@cmd}%
+      {-P style=##1 -P commandprefix=PYG##1}%
+    \minted@checkstyle{##1}%
+    \@namedef{minted@opt@cmd:style}{##1}}%
+}
+\newcommand{\minted@patch@Zsq}[1]{%
+  \ifx\upquote@cmtt\minted@undefined\else
+    \ifx\encodingdefault\upquote@OTone
+      \ifx\ttdefault\upquote@cmtt
+        \expandafter\ifdefstring\expandafter{\csname PYG#1Zsq\endcsname}{\char`\'}%
+        {\expandafter\gdef\csname PYG#1Zsq\endcsname{\char13 }}{}%
+      \else
+        \expandafter\ifdefstring\expandafter{\csname PYG#1Zsq\endcsname}{\char`\'}%
+        {\expandafter\gdef\csname PYG#1Zsq\endcsname{\textquotesingle}}{}%
+      \fi
+    \else
+      \expandafter\ifdefstring\expandafter{\csname PYG#1Zsq\endcsname}{\char`\'}%
+      {\expandafter\gdef\csname PYG#1Zsq\endcsname{\textquotesingle}}{}%
+    \fi
+  \fi
+}
+\newcommand{\minted@checkstyle}[1]{%
+  \ifcsname minted@styleloaded@#1\endcsname\else
+    \expandafter\gdef\csname minted@styleloaded@#1\endcsname{}%
+    \ifthenelse{\boolean{minted@cache}}%
+      {\IfFileExists{\minted@outputdir\minted@cachedir/#1.pygstyle}{}{%
+        \ifwindows
+          \immediate\write18{\MintedPygmentize\space -S #1 -f latex
+            -P commandprefix=PYG#1
+            > "\minted@outputdir@windows\minted@cachedir@windows\@backslashchar#1.pygstyle"}%
+        \else
+          \immediate\write18{\MintedPygmentize\space -S #1 -f latex
+            -P commandprefix=PYG#1
+            > "\minted@outputdir\minted@cachedir/#1.pygstyle"}%
+        \fi
+        }%
+        \begingroup
+        \let\def\gdef
+        \endlinechar=-1\relax
+        \minted@input{\minted@outputdir\minted@cachedir/#1.pygstyle}%
+        \endgroup
+        \minted@addcachefile{#1.pygstyle}}%
+      {\ifwindows
+          \immediate\write18{\MintedPygmentize\space -S #1 -f latex
+            -P commandprefix=PYG#1 > "\minted@outputdir@windows\jobname.out.pyg"}%
+        \else
+          \immediate\write18{\MintedPygmentize\space -S #1 -f latex
+            -P commandprefix=PYG#1 > "\minted@outputdir\jobname.out.pyg"}%
+        \fi
+        \begingroup
+        \let\def\gdef
+        \endlinechar=-1\relax
+        \minted@input{\minted@outputdir\jobname.out.pyg}%
+        \endgroup}%
+    \ifx\@onlypreamble\@notprerr
+      \minted@patch@Zsq{#1}%
+    \else
+      \minted@patch@Zsq{#1}%
+      \AtBeginDocument{\minted@patch@Zsq{#1}}%
+    \fi
+  \fi
+}
+\ifthenelse{\boolean{minted@draft}}{\renewcommand{\minted@checkstyle}[1]{}}{}
+\newcommand{\minted@def@optcl@switch}[2]{%
+  \define@booleankey{minted@opt@g}{#1}%
+    {\minted@addto@optlistcl{\minted@optlistcl@g}{#2=True}%
+      \@namedef{minted@opt@g:#1}{true}}
+    {\minted@addto@optlistcl{\minted@optlistcl@g}{#2=False}%
+      \@namedef{minted@opt@g:#1}{false}}
+  \define@booleankey{minted@opt@g@i}{#1}%
+    {\minted@addto@optlistcl{\minted@optlistcl@g@i}{#2=True}%
+      \@namedef{minted@opt@g@i:#1}{true}}
+    {\minted@addto@optlistcl{\minted@optlistcl@g@i}{#2=False}%
+      \@namedef{minted@opt@g@i:#1}{false}}
+  \define@booleankey{minted@opt@lang}{#1}%
+    {\minted@addto@optlistcl@lang{minted@optlistcl@lang\minted@lang}{#2=True}%
+      \@namedef{minted@opt@lang\minted@lang:#1}{true}}
+    {\minted@addto@optlistcl@lang{minted@optlistcl@lang\minted@lang}{#2=False}%
+      \@namedef{minted@opt@lang\minted@lang:#1}{false}}
+  \define@booleankey{minted@opt@lang@i}{#1}%
+    {\minted@addto@optlistcl@lang{minted@optlistcl@lang\minted@lang @i}{#2=True}%
+      \@namedef{minted@opt@lang\minted@lang @i:#1}{true}}
+    {\minted@addto@optlistcl@lang{minted@optlistcl@lang\minted@lang @i}{#2=False}%
+      \@namedef{minted@opt@lang\minted@lang @i:#1}{false}}
+  \define@booleankey{minted@opt@cmd}{#1}%
+      {\minted@addto@optlistcl{\minted@optlistcl@cmd}{#2=True}%
+        \@namedef{minted@opt@cmd:#1}{true}}
+      {\minted@addto@optlistcl{\minted@optlistcl@cmd}{#2=False}%
+        \@namedef{minted@opt@cmd:#1}{false}}
+}
+\newcommand{\minted@def@optfv}[1]{%
+  \define@key{minted@opt@g}{#1}{%
+    \expandafter\def\expandafter\minted@optlistfv@g\expandafter{%
+      \minted@optlistfv@g#1=##1,}%
+    \@namedef{minted@opt@g:#1}{##1}}
+  \define@key{minted@opt@g@i}{#1}{%
+    \expandafter\def\expandafter\minted@optlistfv@g@i\expandafter{%
+      \minted@optlistfv@g@i#1=##1,}%
+    \@namedef{minted@opt@g@i:#1}{##1}}
+  \define@key{minted@opt@lang}{#1}{%
+    \expandafter\let\expandafter\minted@tmp%
+      \csname minted@optlistfv@lang\minted@lang\endcsname
+    \expandafter\def\expandafter\minted@tmp\expandafter{%
+      \minted@tmp#1=##1,}%
+    \expandafter\let\csname minted@optlistfv@lang\minted@lang\endcsname%
+      \minted@tmp
+    \@namedef{minted@opt@lang\minted@lang:#1}{##1}}
+  \define@key{minted@opt@lang@i}{#1}{%
+    \expandafter\let\expandafter\minted@tmp%
+      \csname minted@optlistfv@lang\minted@lang @i\endcsname
+    \expandafter\def\expandafter\minted@tmp\expandafter{%
+      \minted@tmp#1=##1,}%
+    \expandafter\let\csname minted@optlistfv@lang\minted@lang @i\endcsname%
+      \minted@tmp
+    \@namedef{minted@opt@lang\minted@lang @i:#1}{##1}}
+  \define@key{minted@opt@cmd}{#1}{%
+    \expandafter\def\expandafter\minted@optlistfv@cmd\expandafter{%
+      \minted@optlistfv@cmd#1=##1,}%
+    \@namedef{minted@opt@cmd:#1}{##1}}
+}
+\newcommand{\minted@def@optfv@switch}[1]{%
+  \define@booleankey{minted@opt@g}{#1}%
+    {\expandafter\def\expandafter\minted@optlistfv@g\expandafter{%
+      \minted@optlistfv@g#1=true,}%
+     \@namedef{minted@opt@g:#1}{true}}%
+    {\expandafter\def\expandafter\minted@optlistfv@g\expandafter{%
+      \minted@optlistfv@g#1=false,}%
+     \@namedef{minted@opt@g:#1}{false}}%
+  \define@booleankey{minted@opt@g@i}{#1}%
+    {\expandafter\def\expandafter\minted@optlistfv@g@i\expandafter{%
+      \minted@optlistfv@g@i#1=true,}%
+     \@namedef{minted@opt@g@i:#1}{true}}%
+    {\expandafter\def\expandafter\minted@optlistfv@g@i\expandafter{%
+      \minted@optlistfv@g@i#1=false,}%
+     \@namedef{minted@opt@g@i:#1}{false}}%
+  \define@booleankey{minted@opt@lang}{#1}%
+    {\expandafter\let\expandafter\minted@tmp%
+        \csname minted@optlistfv@lang\minted@lang\endcsname
+      \expandafter\def\expandafter\minted@tmp\expandafter{%
+        \minted@tmp#1=true,}%
+      \expandafter\let\csname minted@optlistfv@lang\minted@lang\endcsname%
+        \minted@tmp
+     \@namedef{minted@opt@lang\minted@lang:#1}{true}}%
+    {\expandafter\let\expandafter\minted@tmp%
+        \csname minted@optlistfv@lang\minted@lang\endcsname
+      \expandafter\def\expandafter\minted@tmp\expandafter{%
+        \minted@tmp#1=false,}%
+      \expandafter\let\csname minted@optlistfv@lang\minted@lang\endcsname%
+        \minted@tmp
+     \@namedef{minted@opt@lang\minted@lang:#1}{false}}%
+  \define@booleankey{minted@opt@lang@i}{#1}%
+    {\expandafter\let\expandafter\minted@tmp%
+        \csname minted@optlistfv@lang\minted@lang @i\endcsname
+      \expandafter\def\expandafter\minted@tmp\expandafter{%
+        \minted@tmp#1=true,}%
+      \expandafter\let\csname minted@optlistfv@lang\minted@lang @i\endcsname%
+        \minted@tmp
+     \@namedef{minted@opt@lang\minted@lang @i:#1}{true}}%
+    {\expandafter\let\expandafter\minted@tmp%
+        \csname minted@optlistfv@lang\minted@lang @i\endcsname
+      \expandafter\def\expandafter\minted@tmp\expandafter{%
+        \minted@tmp#1=false,}%
+      \expandafter\let\csname minted@optlistfv@lang\minted@lang @i\endcsname%
+        \minted@tmp
+     \@namedef{minted@opt@lang\minted@lang @i:#1}{false}}%
+  \define@booleankey{minted@opt@cmd}{#1}%
+    {\expandafter\def\expandafter\minted@optlistfv@cmd\expandafter{%
+      \minted@optlistfv@cmd#1=true,}%
+     \@namedef{minted@opt@cmd:#1}{true}}%
+    {\expandafter\def\expandafter\minted@optlistfv@cmd\expandafter{%
+      \minted@optlistfv@cmd#1=false,}%
+     \@namedef{minted@opt@cmd:#1}{false}}%
+}
+\newboolean{minted@isinline}
+\newcommand{\minted@fvset}{%
+  \expandafter\fvset\expandafter{\minted@optlistfv@g}%
+  \expandafter\let\expandafter\minted@tmp%
+    \csname minted@optlistfv@lang\minted@lang\endcsname
+  \expandafter\fvset\expandafter{\minted@tmp}%
+  \ifthenelse{\boolean{minted@isinline}}%
+   {\expandafter\fvset\expandafter{\minted@optlistfv@g@i}%
+    \expandafter\let\expandafter\minted@tmp%
+      \csname minted@optlistfv@lang\minted@lang @i\endcsname
+    \expandafter\fvset\expandafter{\minted@tmp}}%
+   {}%
+  \expandafter\fvset\expandafter{\minted@optlistfv@cmd}%
+}
+\def\minted@get@opt#1#2{%
+  \ifcsname minted@opt@cmd:#1\endcsname
+    \csname minted@opt@cmd:#1\endcsname
+  \else
+    \ifminted@isinline
+      \ifcsname minted@opt@lang\minted@lang @i:#1\endcsname
+        \csname minted@opt@lang\minted@lang @i:#1\endcsname
+      \else
+        \ifcsname minted@opt@g@i:#1\endcsname
+          \csname minted@opt@g@i:#1\endcsname
+        \else
+          \ifcsname minted@opt@lang\minted@lang:#1\endcsname
+            \csname minted@opt@lang\minted@lang:#1\endcsname
+          \else
+            \ifcsname minted@opt@g:#1\endcsname
+              \csname minted@opt@g:#1\endcsname
+            \else
+              #2%
+            \fi
+          \fi
+        \fi
+      \fi
+    \else
+      \ifcsname minted@opt@lang\minted@lang:#1\endcsname
+        \csname minted@opt@lang\minted@lang:#1\endcsname
+      \else
+        \ifcsname minted@opt@g:#1\endcsname
+          \csname minted@opt@g:#1\endcsname
+        \else
+          #2%
+        \fi
+      \fi
+    \fi
+  \fi
+}%
+\newcommand{\minted@def@opt}[2][]{%
+  \define@key{minted@opt@g}{#2}{%
+    \@namedef{minted@opt@g:#2}{##1}}
+  \define@key{minted@opt@g@i}{#2}{%
+    \@namedef{minted@opt@g@i:#2}{##1}}
+  \define@key{minted@opt@lang}{#2}{%
+    \@namedef{minted@opt@lang\minted@lang:#2}{##1}}
+  \define@key{minted@opt@lang@i}{#2}{%
+    \@namedef{minted@opt@lang\minted@lang @i:#2}{##1}}
+  \define@key{minted@opt@cmd}{#2}{%
+    \@namedef{minted@opt@cmd:#2}{##1}}
+}
+\newcommand{\minted@def@opt@switch}[2][false]{%
+  \define@booleankey{minted@opt@g}{#2}%
+    {\@namedef{minted@opt@g:#2}{true}}%
+    {\@namedef{minted@opt@g:#2}{false}}
+  \define@booleankey{minted@opt@g@i}{#2}%
+    {\@namedef{minted@opt@g@i:#2}{true}}%
+    {\@namedef{minted@opt@g@i:#2}{false}}
+  \define@booleankey{minted@opt@lang}{#2}%
+    {\@namedef{minted@opt@lang\minted@lang:#2}{true}}%
+    {\@namedef{minted@opt@lang\minted@lang:#2}{false}}
+  \define@booleankey{minted@opt@lang@i}{#2}%
+    {\@namedef{minted@opt@lang\minted@lang @i:#2}{true}}%
+    {\@namedef{minted@opt@lang\minted@lang @i:#2}{false}}
+  \define@booleankey{minted@opt@cmd}{#2}%
+    {\@namedef{minted@opt@cmd:#2}{true}}%
+    {\@namedef{minted@opt@cmd:#2}{false}}%
+  \@namedef{minted@opt@g:#2}{#1}%
+}
+
+\minted@def@optcl{encoding}{-P encoding}{#1}
+\minted@def@optcl{outencoding}{-P outencoding}{#1}
+\minted@def@optcl@e{escapeinside}{-P "escapeinside}{#1"}
+\minted@def@optcl@switch{stripnl}{-P stripnl}
+\minted@def@optcl@switch{stripall}{-P stripall}
+\minted@def@optcl@switch{python3}{-P python3}
+\minted@def@optcl@switch{funcnamehighlighting}{-P funcnamehighlighting}
+\minted@def@optcl@switch{startinline}{-P startinline}
+\ifthenelse{\boolean{minted@draft}}%
+  {\minted@def@optfv{gobble}}%
+  {\minted@def@optcl{gobble}{-F gobble:n}{#1}}
+\minted@def@optcl{codetagify}{-F codetagify:codetags}{#1}
+\minted@def@optcl{keywordcase}{-F keywordcase:case}{#1}
+\minted@def@optcl@switch{texcl}{-P texcomments}
+\minted@def@optcl@switch{texcomments}{-P texcomments}
+\minted@def@optcl@switch{mathescape}{-P mathescape}
+\ifcsname KV@FV@linenos\endcsname\else
+\define@booleankey{FV}{linenos}%
+  {\@nameuse{FV@Numbers@left}}{\@nameuse{FV@Numbers@none}}
+\fi
+\minted@def@optfv@switch{linenos}
+\minted@def@optcl@style
+\minted@def@optfv{frame}
+\minted@def@optfv{framesep}
+\minted@def@optfv{framerule}
+\minted@def@optfv{rulecolor}
+\minted@def@optfv{numbersep}
+\minted@def@optfv{numbers}
+\minted@def@optfv{firstnumber}
+\minted@def@optfv{stepnumber}
+\minted@def@optfv{firstline}
+\minted@def@optfv{lastline}
+\minted@def@optfv{baselinestretch}
+\minted@def@optfv{xleftmargin}
+\minted@def@optfv{xrightmargin}
+\minted@def@optfv{fillcolor}
+\minted@def@optfv{tabsize}
+\minted@def@optfv{fontfamily}
+\minted@def@optfv{fontsize}
+\minted@def@optfv{fontshape}
+\minted@def@optfv{fontseries}
+\minted@def@optfv{formatcom}
+\minted@def@optfv{label}
+\minted@def@optfv@switch{numberblanklines}
+\minted@def@optfv@switch{showspaces}
+\minted@def@optfv@switch{resetmargins}
+\minted@def@optfv@switch{samepage}
+\minted@def@optfv@switch{showtabs}
+\minted@def@optfv@switch{obeytabs}
+\minted@def@optfv@switch{breaklines}
+\minted@def@optfv{breakindent}
+\minted@def@optfv@switch{breakautoindent}
+\minted@def@optfv{breaksymbol}
+\minted@def@optfv{breaksymbolsep}
+\minted@def@optfv{breaksymbolindent}
+\minted@def@optfv{breaksymbolleft}
+\minted@def@optfv{breaksymbolsepleft}
+\minted@def@optfv{breaksymbolindentleft}
+\minted@def@optfv{breaksymbolright}
+\minted@def@optfv{breaksymbolsepright}
+\minted@def@optfv{breaksymbolindentright}
+\minted@def@opt@switch{breakbytoken}
+\minted@def@opt{bgcolor}
+\minted@def@opt@switch{autogobble}
+\newcommand{\minted@encoding}{\minted@get@opt{encoding}{UTF8}}
+\ifcsname KV@FV@breaklines\endcsname\else
+\newboolean{FV@BreakLines}
+\let\FV@ListProcessLine@Orig\FV@ListProcessLine
+\define@booleankey{FV}{breaklines}%
+  {\FV@BreakLinestrue
+    \let\FV@ListProcessLine\FV@ListProcessLine@Break}%
+  {\FV@BreakLinesfalse
+    \let\FV@ListProcessLine\FV@ListProcessLine@Orig}
+\newdimen\FV@BreakIndent
+\define@key{FV}{breakindent}{\FV@BreakIndent=#1}
+\fvset{breakindent=0pt}
+\newboolean{FV@BreakAutoIndent}
+\define@booleankey{FV}{breakautoindent}%
+  {\FV@BreakAutoIndenttrue}{\FV@BreakAutoIndentfalse}
+\fvset{breakautoindent=true}
+\define@key{FV}{breaksymbolleft}{\def\FancyVerbBreakSymbolLeft{#1}}
+\define@key{FV}{breaksymbol}{\fvset{breaksymbolleft=#1}}
+\fvset{breaksymbolleft=\tiny\ensuremath{\hookrightarrow}}
+\define@key{FV}{breaksymbolright}{\def\FancyVerbBreakSymbolRight{#1}}
+\fvset{breaksymbolright={}}
+\newdimen\FV@BreakSymbolSepLeft
+\define@key{FV}{breaksymbolsepleft}{\FV@BreakSymbolSepLeft=#1}
+\define@key{FV}{breaksymbolsep}{\fvset{breaksymbolsepleft=#1}}
+\fvset{breaksymbolsepleft=1em}
+\newdimen\FV@BreakSymbolSepRight
+\define@key{FV}{breaksymbolsepright}{\FV@BreakSymbolSepRight=#1}
+\fvset{breaksymbolsepright=1em}
+\newdimen\FV@BreakSymbolIndentLeft
+\settowidth{\FV@BreakSymbolIndentLeft}{\ttfamily xxxx}
+\define@key{FV}{breaksymbolindentleft}{\FV@BreakSymbolIndentLeft=#1}
+\define@key{FV}{breaksymbolindent}{\fvset{breaksymbolindentleft=#1}}
+\newdimen\FV@BreakSymbolIndentRight
+\settowidth{\FV@BreakSymbolIndentRight}{\ttfamily xxxx}
+\define@key{FV}{breaksymbolindentright}{\FV@BreakSymbolIndentRight=#1}
+\newcommand{\FancyVerbFormatBreakSymbolLeft}[1]{%
+  \ifnum\value{linenumber}=1\relax\else{#1}\fi}
+\newcounter{FancyVerbLineBreakLast}
+\newcommand{\FV@SetLineBreakLast}{%
+  \setcounter{FancyVerbLineBreakLast}{\value{linenumber}}}
+\newcommand{\FancyVerbFormatBreakSymbolRight}[1]{%
+  \ifnum\value{linenumber}=\value{FancyVerbLineBreakLast}\relax\else{#1}\fi}
+\newsavebox{\FV@LineBox}
+\newsavebox{\FV@LineIndentBox}
+\let\FV@LineIndentChars\@empty
+\def\FV@GetNextChar{\let\FV@NextChar=}
+\def\FV@CleanRemainingChars#1\FV@Undefined{}
+\def\FV@GetLineIndent{\afterassignment\FV@CheckIndentChar\FV@GetNextChar}
+\def\FV@CheckIndentChar{%
+  \ifx\FV@NextChar\FV@Undefined
+    \let\FV@Next=\relax
+  \else
+    \expandafter\ifx\FV@NextChar\FV@Space
+      \g@addto@macro{\FV@LineIndentChars}{\FV@Space}%
+      \let\FV@Next=\FV@GetLineIndent
+    \else
+      \expandafter\ifx\FV@NextChar\FV@Tab
+        \g@addto@macro{\FV@LineIndentChars}{\FV@Tab}%
+        \let\FV@Next=\FV@GetLineIndent
+      \else
+        \let\FV@Next=\FV@CleanRemainingChars
+      \fi
+    \fi
+  \fi
+  \FV@Next
+}
+\def\FV@makeLineNumber{%
+  \hss
+  \FancyVerbFormatBreakSymbolLeft{\FancyVerbBreakSymbolLeft}%
+  \hbox to \FV@BreakSymbolSepLeft{\hfill}%
+  \rlap{\hskip\linewidth
+    \hbox to \FV@BreakSymbolSepRight{\hfill}%
+    \FancyVerbFormatBreakSymbolRight{\FancyVerbBreakSymbolRight}%
+    \FV@SetLineBreakLast
+  }%
+}
+\def\FV@SaveLineBox#1{%
+  \savebox{\FV@LineBox}{%
+    \advance\linewidth by -\FV@BreakIndent
+    \hbox to \FV@BreakIndent{\hfill}%
+    \ifthenelse{\boolean{FV@BreakAutoIndent}}%
+     {\let\FV@LineIndentChars\@empty
+      \FV@GetLineIndent#1\FV@Undefined
+      \savebox{\FV@LineIndentBox}{\FV@LineIndentChars}%
+      \hbox to \wd\FV@LineIndentBox{\hfill}%
+      \advance\linewidth by -\wd\FV@LineIndentBox}%
+     {}%
+    \ifdefempty{\FancyVerbBreakSymbolLeft}{}%
+     {\hbox to \FV@BreakSymbolIndentLeft{\hfill}%
+      \advance\linewidth by -\FV@BreakSymbolIndentLeft}%
+    \ifdefempty{\FancyVerbBreakSymbolRight}{}%
+     {\advance\linewidth by -\FV@BreakSymbolIndentRight}%
+    \parbox[t]{\linewidth}{%
+      \raggedright
+      \leftlinenumbers*
+      \begin{internallinenumbers*}%
+      \let\makeLineNumber\FV@makeLineNumber
+      \noindent\hspace*{-\FV@BreakIndent}%
+      \ifdefempty{\FancyVerbBreakSymbolLeft}{}{%
+        \hspace*{-\FV@BreakSymbolIndentLeft}}%
+      \ifthenelse{\boolean{FV@BreakAutoIndent}}%
+       {\hspace*{-\wd\FV@LineIndentBox}}%
+       {}%
+      \strut#1\strut
+      \end{internallinenumbers*}
+    }%
+    \ifdefempty{\FancyVerbBreakSymbolRight}{}%
+     {\hbox to \FV@BreakSymbolIndentRight{\hfill}}%
+  }%
+}
+\def\FV@ListProcessLine@Break#1{%
+  \hbox to \hsize{%
+  \kern\leftmargin
+  \hbox to \linewidth{%
+  \ifx\FV@RightListFrame\relax\else
+    \advance\linewidth by -\FV@FrameSep
+    \advance\linewidth by -\FV@FrameRule
+  \fi
+  \ifx\FV@LeftListFrame\relax\else
+    \advance\linewidth by -\FV@FrameSep
+    \advance\linewidth by -\FV@FrameRule
+  \fi
+  \sbox{\FV@LineBox}{\FancyVerbFormatLine{#1}}%
+  \ifdim\wd\FV@LineBox>\linewidth
+    \setcounter{FancyVerbLineBreakLast}{0}%
+    \FV@SaveLineBox{#1}%
+    \ifdefempty{\FancyVerbBreakSymbolRight}{}{%
+      \let\FV@SetLineBreakLast\relax
+      \FV@SaveLineBox{#1}}%
+    \FV@LeftListNumber
+    \FV@LeftListFrame
+    \FancyVerbFormatLine{\usebox{\FV@LineBox}}%
+    \FV@RightListFrame
+    \FV@RightListNumber
+  \else
+    \FV@LeftListNumber
+    \FV@LeftListFrame
+    \FancyVerbFormatLine{%
+      \parbox[t]{\linewidth}{\noindent\strut#1\strut}}%
+    \FV@RightListFrame
+    \FV@RightListNumber
+  \fi}%
+  \hss}\baselineskip\z@\lineskip\z@}
+\fi
 \newsavebox{\minted@bgbox}
 \newenvironment{minted@colorbg}[1]{
-  \def\minted@bgcol{#1}
-  \noindent
-  \begin{lrbox}{\minted@bgbox}
-  \begin{minipage}{\linewidth-2\fboxsep}}
+    %\setlength{\fboxsep}{-\fboxrule}
+    \def\minted@bgcol{#1}
+    \noindent
+    \begin{lrbox}{\minted@bgbox}
+    \begin{minipage}{\linewidth-2\fboxsep}}
  {\end{minipage}
-  \end{lrbox}%
-  \colorbox{\minted@bgcol}{\usebox{\minted@bgbox}}}
+    \end{lrbox}%
+    \colorbox{\minted@bgcol}{\usebox{\minted@bgbox}}}
 \newwrite\minted@code
-\newcommand\minted@savecode[1]{
-  \immediate\openout\minted@code\jobname.pyg
-  \immediate\write\minted@code{#1}
+\newcommand{\minted@savecode}[1]{
+  \immediate\openout\minted@code\jobname.pyg\relax
+  \immediate\write\minted@code{\expandafter\detokenize\expandafter{#1}}%
   \immediate\closeout\minted@code}
-\newcommand\minted@pygmentize[2][\jobname.pyg]{
-  \def\minted@cmd{pygmentize -l #2 -f latex -F tokenmerge
-    \minted@opt{gobble} \minted@opt{texcl} \minted@opt{mathescape}
-    \minted@opt{startinline} \minted@opt{funcnamehighlighting}
-    \minted@opt{linenos} -P "verboptions=\minted@opt{extra}"
-    -o \jobname.out.pyg #1}
-  \immediate\write18{\minted@cmd}
-  % For debugging, uncomment:
-  %\immediate\typeout{\minted@cmd}
-  \ifthenelse{\equal{\minted@opt@bgcolor}{}}
-   {}
-   {\begin{minted@colorbg}{\minted@opt@bgcolor}}
-  \input{\jobname.out.pyg}
-  \ifthenelse{\equal{\minted@opt@bgcolor}{}}
-   {}
-   {\end{minted@colorbg}}
-  \DeleteFile{\jobname.out.pyg}}
-\newcommand\minted@usedefaultstyle{\usemintedstyle{default}}
-\newcommand\usemintedstyle[1]{
-  \renewcommand\minted@usedefaultstyle{}
-  \immediate\write18{pygmentize -S #1 -f latex > \jobname.pyg}
-  \input{\jobname.pyg}}
-\newcommand\mint[3][]{
-  \DefineShortVerb{#3}
-  \minted@resetoptions
-  \setkeys{minted@opt}{#1}
-  \SaveVerb[aftersave={
-    \UndefineShortVerb{#3}
-    \minted@savecode{\FV@SV@minted@verb}
-    \minted@pygmentize{#2}
-    \DeleteFile{\jobname.pyg}}]{minted@verb}#3}
-\newcommand\minted@proglang[1]{}
-\newenvironment{minted}[2][]
- {\VerbatimEnvironment
-  \renewcommand{\minted@proglang}[1]{#2}
-  \minted@resetoptions
-  \setkeys{minted@opt}{#1}
-  \begin{VerbatimOut}[codes={\catcode`\^^I=12}]{\jobname.pyg}}%
- {\end{VerbatimOut}
-  \minted@pygmentize{\minted@proglang{}}
-  \DeleteFile{\jobname.pyg}}
-\newcommand\inputminted[3][]{
-  \minted@resetoptions
-  \setkeys{minted@opt}{#1}
-  \minted@pygmentize[#3]{#2}}
-\newcommand\newminted[3][]{
+\newcounter{minted@FancyVerbLineTemp}
+\newcommand{\minted@write@detok}[1]{%
+  \immediate\write\FV@OutFile{\detokenize{#1}}}
+\newcommand{\minted@FVB@VerbatimOut}[1]{%
+  \setcounter{minted@FancyVerbLineTemp}{\value{FancyVerbLine}}%
+  \@bsphack
+  \begingroup
+    \FV@UseKeyValues
+    \FV@DefineWhiteSpace
+    \def\FV@Space{\space}%
+    \FV@DefineTabOut
+    \let\FV@ProcessLine\minted@write@detok
+    \immediate\openout\FV@OutFile #1\relax
+    \let\FV@FontScanPrep\relax
+    \let\@noligs\relax
+    \FV@Scan}
+\newcommand{\minted@FVE@VerbatimOut}{%
+  \immediate\closeout\FV@OutFile\endgroup\@esphack
+  \setcounter{FancyVerbLine}{\value{minted@FancyVerbLineTemp}}}%
+\newcommand{\MintedPygmentize}{pygmentize}
+\newcommand{\minted@pygmentize}[2][\minted@outputdir\jobname.pyg]{%
+  \ifthenelse{\equal{\minted@get@opt{autogobble}{false}}{true}}%
+    {\def\minted@codefile{\minted@outputdir\jobname.pyg}}%
+    {\def\minted@codefile{#1}}%
+  \ifthenelse{\boolean{minted@isinline}}%
+    {\def\minted@optlistcl@inlines{%
+      \minted@optlistcl@g@i
+      \csname minted@optlistcl@lang\minted@lang @i\endcsname}}%
+    {\let\minted@optlistcl@inlines\@empty}%
+  \def\minted@cmd{%
+    \ifminted@kpsewhich\ifwindows powershell\space\fi\fi
+    \MintedPygmentize\space -l #2
+    -f latex -F tokenmerge
+    \minted@optlistcl@g \csname minted@optlistcl@lang\minted@lang\endcsname
+    \minted@optlistcl@inlines
+    \minted@optlistcl@cmd -o "\minted@outputdir\minted@infile"
+    \ifminted@kpsewhich
+      \ifwindows
+        \detokenize{$}(kpsewhich "\minted@codefile")%
+      \else
+        \detokenize{`}kpsewhich "\minted@codefile"
+          \detokenize{||} "\minted@codefile"\detokenize{`}%
+      \fi
+    \else
+      "\minted@codefile"
+    \fi}%
+  % For debugging, uncomment: %%%%
+  % \immediate\typeout{\minted@cmd}%
+  % %%%%
+  \ifthenelse{\boolean{minted@cache}}%
+    {%
+      \ifx\XeTeXinterchartoks\minted@undefined
+        \ifthenelse{\equal{\minted@get@opt{autogobble}{false}}{true}}%
+          {\edef\minted@hash{\pdf@filemdfivesum{#1}%
+            \pdf@mdfivesum{\minted@cmd autogobble}}}%
+          {\edef\minted@hash{\pdf@filemdfivesum{#1}%
+            \pdf@mdfivesum{\minted@cmd}}}%
+      \else
+        \immediate\openout\minted@code\jobname.mintedcmd\relax
+        \immediate\write\minted@code{\minted@cmd}%
+        \ifthenelse{\equal{\minted@get@opt{autogobble}{false}}{true}}%
+          {\immediate\write\minted@code{autogobble}}{}%
+        \immediate\closeout\minted@code
+        %Cheating a little here by using ASCII codes to write `{` and `}`
+        %in the Python code
+        \def\minted@hashcmd{%
+          \detokenize{python -c "import hashlib;
+            hasher = hashlib.sha1();
+            f = open(\"}\minted@outputdir\jobname.mintedcmd\detokenize{\", \"rb\");
+            hasher.update(f.read());
+            f.close();
+            f = open(\"}#1\detokenize{\", \"rb\");
+            hasher.update(f.read());
+            f.close();
+            f = open(\"}\minted@outputdir\jobname.mintedmd5\detokenize{\", \"w\");
+            macro = \"\\edef\\minted@hash\" + chr(123) + hasher.hexdigest() + chr(125) + \"\";
+            f.write(\"\\makeatletter\" + macro + \"\\makeatother\\endinput\n\");
+            f.close();"}}%
+        \immediate\write18{\minted@hashcmd}%
+        \minted@input{\minted@outputdir\jobname.mintedmd5}%
+      \fi
+      \edef\minted@infile{\minted@cachedir/\minted@hash.pygtex}%
+      \IfFileExists{\minted@infile}{}{%
+        \ifthenelse{\equal{\minted@get@opt{autogobble}{false}}{true}}{%
+          %Need a version of open() that supports encoding under Python 2
+          \edef\minted@autogobblecmd{%
+            \detokenize{python -c "import sys;
+            import textwrap;
+            from io import open;
+            f = open(\"}#1\detokenize{\", \"r\", encoding=\"}\minted@encoding\detokenize{\");
+            t = f.read();
+            f.close();
+            f = open(\"}\minted@outputdir\jobname.pyg\detokenize{\", \"w\", encoding=\"}\minted@encoding\detokenize{\");
+            f.write(textwrap.dedent(t));
+            f.close();"}%
+          }%
+          \immediate\write18{\minted@autogobblecmd}}{}%
+        \immediate\write18{\minted@cmd}}%
+      \expandafter\minted@addcachefile\expandafter{\minted@hash.pygtex}%
+      \minted@inputpyg}%
+    {%
+      \ifthenelse{\equal{\minted@get@opt{autogobble}{false}}{true}}{%
+        %Need a version of open() that supports encoding under Python 2
+        \edef\minted@autogobblecmd{%
+          \detokenize{python -c "import sys;
+          import textwrap;
+          from io import open;
+          f = open(\"}#1\detokenize{\", \"r\", encoding=\"}\minted@encoding\detokenize{\");
+          t = f.read();
+          f.close();
+          f = open(\"}\minted@outputdir\jobname.pyg\detokenize{\", \"w\", encoding=\"}\minted@encoding\detokenize{\");
+          f.write(textwrap.dedent(t));
+          f.close();"}%
+        }%
+        \immediate\write18{\minted@autogobblecmd}}{}%
+      \immediate\write18{\minted@cmd}%
+      \minted@inputpyg}%
+}
+\def\FV@SpaceMMode{ }
+\newcommand{\minted@inputpyg}{%
+  \everymath\expandafter{\the\everymath\let\FV@Space\FV@SpaceMMode}%
+  \ifthenelse{\boolean{minted@isinline}}%
+   {\ifthenelse{\equal{\minted@get@opt{breaklines}{false}}{true}}%
+    {\let\FV@BeginVBox\relax
+     \let\FV@EndVBox\relax
+     \def\FV@BProcessLine##1{\FancyVerbFormatLine{##1}}%
+     \ifthenelse{\equal{\minted@get@opt{breakbytoken}{false}}{true}}%
+      {\expandafter\let\expandafter\minted@orig@PYG%
+       \csname PYG\minted@get@opt{style}{default}\endcsname
+       \expandafter\def\csname PYG\minted@get@opt{style}{default}\endcsname##1##2{%
+         \allowbreak{}\hbox{\minted@orig@PYG{##1}{##2}}}%
+       \minted@inputpyg@inline}%
+      {\minted@inputpyg@inline}}%
+    {\minted@inputpyg@inline}}%
+   {\ifthenelse{\equal{\minted@get@opt{breaklines}{false}}{true}}%
+     {\ifthenelse{\equal{\minted@get@opt{breakbytoken}{false}}{true}}%
+       {\expandafter\let\expandafter\minted@orig@PYG%
+        \csname PYG\minted@get@opt{style}{default}\endcsname
+        \expandafter\def\csname PYG\minted@get@opt{style}{default}\endcsname##1##2{%
+        \allowbreak{}\hbox{\minted@orig@PYG{##1}{##2}}}%
+        \minted@inputpyg@block}%
+       {\minted@inputpyg@block}}%
+     {\minted@inputpyg@block}}%
+}
+\def\minted@inputpyg@inline{%
+  \ifthenelse{\equal{\minted@get@opt{bgcolor}{}}{}}%
+   {\minted@input{\minted@outputdir\minted@infile}}%
+   {\colorbox{\minted@get@opt{bgcolor}{}}{\minted@input{\minted@outputdir\minted@infile}}}%
+}
+\def\minted@inputpyg@block{%
+  \ifthenelse{\equal{\minted@get@opt{bgcolor}{}}{}}%
+   {\minted@input{\minted@outputdir\minted@infile}}%
+   {\begin{minted@colorbg}{\minted@get@opt{bgcolor}{}}%
+    \minted@input{\minted@outputdir\minted@infile}%
+    \end{minted@colorbg}}}
+\newcommand{\minted@langlinenoson}{%
+  \ifcsname c@minted@lang\minted@lang\endcsname\else
+    \newcounter{minted@lang\minted@lang}%
+  \fi
+  \setcounter{minted@FancyVerbLineTemp}{\value{FancyVerbLine}}%
+  \setcounter{FancyVerbLine}{\value{minted@lang\minted@lang}}%
+}
+\newcommand{\minted@langlinenosoff}{%
+  \setcounter{minted@lang\minted@lang}{\value{FancyVerbLine}}%
+  \setcounter{FancyVerbLine}{\value{minted@FancyVerbLineTemp}}%
+}
+\ifthenelse{\boolean{minted@langlinenos}}{}{%
+  \let\minted@langlinenoson\relax
+  \let\minted@langlinenosoff\relax
+}
+\newcommand{\setminted}[2][]{%
+  \ifthenelse{\equal{#1}{}}%
+    {\setkeys{minted@opt@g}{#2}}%
+    {\minted@configlang{#1}%
+      \setkeys{minted@opt@lang}{#2}}}
+\newcommand{\setmintedinline}[2][]{%
+  \ifthenelse{\equal{#1}{}}%
+    {\setkeys{minted@opt@g@i}{#2}}%
+    {\minted@configlang{#1}%
+      \setkeys{minted@opt@lang@i}{#2}}}
+\setmintedinline[php]{startinline=true}
+\newcommand{\usemintedstyle}[2][]{\setminted[#1]{style=#2}}
+\begingroup
+\catcode`\ =\active
+\catcode`\^^I=\active
+\gdef\minted@defwhitespace@retok{\def {\noexpand\FV@Space}\def^^I{\noexpand\FV@Tab}}%
+\endgroup
+\newcommand{\minted@writecmdcode}[1]{%
+  \immediate\openout\minted@code\jobname.pyg\relax
+  \immediate\write\minted@code{\detokenize{#1}}%
+  \immediate\closeout\minted@code}
+\newrobustcmd{\mintinline}[2][]{%
+  \begingroup
+  \setboolean{minted@isinline}{true}%
+  \minted@configlang{#2}%
+  \setkeys{minted@opt@cmd}{#1}%
+  \minted@fvset
+  \begingroup
+  \let\do\@makeother\dospecials
+  \catcode`\{=1
+  \catcode`\}=2
+  \catcode`\^^I=\active
+  \@ifnextchar\bgroup
+    {\minted@inline@iii}%
+    {\catcode`\{=12\catcode`\}=12
+      \minted@inline@i}}
+\def\minted@inline@i#1{%
+  \endgroup
+  \def\minted@inline@ii##1#1{%
+    \minted@inline@iii{##1}}%
+  \begingroup
+  \let\do\@makeother\dospecials
+  \catcode`\^^I=\active
+  \minted@inline@ii}
+\ifthenelse{\boolean{minted@draft}}%
+  {\newcommand{\minted@inline@iii}[1]{%
+    \endgroup
+    \begingroup
+    \minted@defwhitespace@retok
+    \everyeof{\noexpand}%
+    \endlinechar-1\relax
+    \let\do\@makeother\dospecials
+    \catcode`\ =\active
+    \catcode`\^^I=\active
+    \xdef\minted@tmp{\scantokens{#1}}%
+    \endgroup
+    \let\FV@Line\minted@tmp
+    \def\FV@SV@minted@tmp{%
+      \FV@Gobble
+      \expandafter\FV@ProcessLine\expandafter{\FV@Line}}%
+    \ifthenelse{\equal{\minted@get@opt{breaklines}{false}}{true}}%
+     {\let\FV@BeginVBox\relax
+      \let\FV@EndVBox\relax
+      \def\FV@BProcessLine##1{\FancyVerbFormatLine{##1}}%
+      \BUseVerbatim{minted@tmp}}%
+     {\BUseVerbatim{minted@tmp}}%
+    \endgroup}}%
+  {\newcommand{\minted@inline@iii}[1]{%
+    \endgroup
+    \minted@writecmdcode{#1}%
+    \RecustomVerbatimEnvironment{Verbatim}{BVerbatim}{}%
+    \setcounter{minted@FancyVerbLineTemp}{\value{FancyVerbLine}}%
+    \minted@pygmentize{\minted@lang}%
+    \setcounter{FancyVerbLine}{\value{minted@FancyVerbLineTemp}}%
+    \endgroup}}
+\newrobustcmd{\mint}[2][]{%
+  \begingroup
+  \minted@configlang{#2}%
+  \setkeys{minted@opt@cmd}{#1}%
+  \minted@fvset
+  \begingroup
+  \let\do\@makeother\dospecials
+  \catcode`\{=1
+  \catcode`\}=2
+  \catcode`\^^I=\active
+  \@ifnextchar\bgroup
+    {\mint@iii}%
+    {\catcode`\{=12\catcode`\}=12
+      \mint@i}}
+\def\mint@i#1{%
+  \endgroup
+  \def\mint@ii##1#1{%
+    \mint@iii{##1}}%
+  \begingroup
+  \let\do\@makeother\dospecials
+  \catcode`\^^I=\active
+  \mint@ii}
+\ifthenelse{\boolean{minted@draft}}%
+  {\newcommand{\mint@iii}[1]{%
+    \endgroup
+    \begingroup
+    \minted@defwhitespace@retok
+    \everyeof{\noexpand}%
+    \endlinechar-1\relax
+    \let\do\@makeother\dospecials
+    \catcode`\ =\active
+    \catcode`\^^I=\active
+    \xdef\minted@tmp{\scantokens{#1}}%
+    \endgroup
+    \let\FV@Line\minted@tmp
+    \def\FV@SV@minted@tmp{%
+      \FV@CodeLineNo=1\FV@StepLineNo
+      \FV@Gobble
+      \expandafter\FV@ProcessLine\expandafter{\FV@Line}}%
+    \minted@langlinenoson
+    \UseVerbatim{minted@tmp}%
+    \minted@langlinenosoff
+    \endgroup}}%
+  {\newcommand{\mint@iii}[1]{%
+    \endgroup
+    \minted@writecmdcode{#1}%
+    \minted@langlinenoson
+    \minted@pygmentize{\minted@lang}%
+    \minted@langlinenosoff
+    \endgroup}}
+\ifthenelse{\boolean{minted@draft}}%
+  {\newenvironment{minted}[2][]
+    {\VerbatimEnvironment
+      \minted@configlang{#2}%
+      \setkeys{minted@opt@cmd}{#1}%
+      \minted@fvset
+      \minted@langlinenoson
+      \begin{Verbatim}}%
+    {\end{Verbatim}%
+      \minted@langlinenosoff}}%
+  {\newenvironment{minted}[2][]
+    {\VerbatimEnvironment
+      \let\FVB@VerbatimOut\minted@FVB@VerbatimOut
+      \let\FVE@VerbatimOut\minted@FVE@VerbatimOut
+      \minted@configlang{#2}%
+      \setkeys{minted@opt@cmd}{#1}%
+      \minted@fvset
+      \begin{VerbatimOut}[codes={\catcode`\^^I=12}]{\jobname.pyg}}%
+    {\end{VerbatimOut}%
+        \minted@langlinenoson
+        \minted@pygmentize{\minted@lang}%
+        \minted@langlinenosoff}}
+\ifthenelse{\boolean{minted@draft}}%
+  {\newcommand{\inputminted}[3][]{%
+    \begingroup
+    \minted@configlang{#2}%
+    \setkeys{minted@optcmd}{#1}%
+    \minted@fvset
+    \VerbatimInput{#3}%
+    \endgroup}}%
+  {\newcommand{\inputminted}[3][]{%
+    \begingroup
+    \minted@configlang{#2}%
+    \setkeys{minted@opt@cmd}{#1}%
+    \minted@fvset
+    \minted@pygmentize[#3]{#2}%
+    \endgroup}}
+\newcommand{\newminted}[3][]{
   \ifthenelse{\equal{#1}{}}
-   {\def\minted@envname{#2code}}
-   {\def\minted@envname{#1}}
+    {\def\minted@envname{#2code}}
+    {\def\minted@envname{#1}}
   \newenvironment{\minted@envname}
-   {\VerbatimEnvironment\begin{minted}[#3]{#2}}
-   {\end{minted}}
+    {\VerbatimEnvironment
+      \begin{minted}[#3]{#2}}
+    {\end{minted}}
   \newenvironment{\minted@envname *}[1]
-   {\VerbatimEnvironment\begin{minted}[#3,##1]{#2}}
-   {\end{minted}}}
-\newcommand\newmint[3][]{
+    {\VerbatimEnvironment\begin{minted}[#3,##1]{#2}}
+    {\end{minted}}}
+\newcommand{\newmint}[3][]{
   \ifthenelse{\equal{#1}{}}
-   {\def\minted@shortname{#2}}
-   {\def\minted@shortname{#1}}
+    {\def\minted@shortname{#2}}
+    {\def\minted@shortname{#1}}
   \expandafter\newcommand\csname\minted@shortname\endcsname[2][]{
     \mint[#3,##1]{#2}##2}}
-\newcommand\newmintedfile[3][]{
+\newcommand{\newmintedfile}[3][]{
   \ifthenelse{\equal{#1}{}}
-   {\def\minted@shortname{#2file}}
-   {\def\minted@shortname{#1}}
+    {\def\minted@shortname{#2file}}
+    {\def\minted@shortname{#1}}
   \expandafter\newcommand\csname\minted@shortname\endcsname[2][]{
     \inputminted[#3,##1]{#2}{##2}}}
-\@ifundefined{minted@float@within}
- {\newfloat{listing}{h}{lol}}
- {\newfloat{listing}{h}{lol}[\minted@float@within]}
-\newcommand\listingscaption{Listing}
+\newcommand{\newmintinline}[3][]{%
+  \ifthenelse{\equal{#1}{}}%
+    {\def\minted@shortname{#2inline}}%
+    {\def\minted@shortname{#1}}%
+    \expandafter\newrobustcmd\csname\minted@shortname\endcsname{%
+      \begingroup
+      \let\do\@makeother\dospecials
+      \catcode`\{=1
+      \catcode`\}=2
+      \@ifnextchar[{\endgroup\minted@inliner[#3][#2]}%
+        {\endgroup\minted@inliner[#3][#2][]}}%
+    \def\minted@inliner[##1][##2][##3]{\mintinline[##1,##3]{##2}}%
+}
+\ifthenelse{\boolean{minted@newfloat}}%
+ {\@ifundefined{minted@float@within}%
+    {\DeclareFloatingEnvironment[fileext=lol,placement=h]{listing}}%
+    {\def\minted@tmp#1{%
+       \DeclareFloatingEnvironment[fileext=lol,placement=h, within=#1]{listing}}%
+     \expandafter\minted@tmp\expandafter{\minted@float@within}}}%
+ {\@ifundefined{minted@float@within}%
+    {\newfloat{listing}{h}{lol}}%
+    {\newfloat{listing}{h}{lol}[\minted@float@within]}}
+\ifminted@newfloat\else
+\newcommand{\listingscaption}{Listing}
 \floatname{listing}{\listingscaption}
-\newcommand\listoflistingscaption{List of listings}
-\providecommand\listoflistings{\listof{listing}{\listoflistingscaption}}
-\AtBeginDocument{
-  \minted@usedefaultstyle}
-\AtEndOfPackage{
-  \ifnum\pdf@shellescape=1\relax\else
-    \PackageError{minted}
-     {You must invoke LaTeX with the
-      -shell-escape flag}
-     {Pass the -shell-escape flag to LaTeX. Refer to the minted.sty
-      documentation for more information.}\fi
-  \TestAppExists{pygmentize}
-  \ifAppExists\else
-    \PackageError{minted}
-     {You must have `pygmentize' installed
-      to use this package}
-     {Refer to the installation instructions in the minted
-      documentation for more information.}
-  \fi}
+\newcommand{\listoflistingscaption}{List of Listings}
+\providecommand{\listoflistings}{\listof{listing}{\listoflistingscaption}}
+\fi
+\AtEndOfPackage{%
+  \ifthenelse{\boolean{minted@draft}}{}{%
+    \ifnum\pdf@shellescape=1\relax\else
+      \PackageError{minted}%
+       {You must invoke LaTeX with the
+        -shell-escape flag}%
+       {Pass the -shell-escape flag to LaTeX. Refer to the minted.sty
+        documentation for more information.}%
+    \fi
+    \TestAppExists{pygmentize}
+    \ifAppExists\else
+      \PackageError{minted}%
+       {You must have `pygmentize' installed
+        to use this package}%
+       {Refer to the installation instructions in the minted
+        documentation for more information.}%
+    \fi
+    \setminted{style=default}%
+  }%
+}
+\AtEndDocument{
+  \ifx\XeTeXinterchartoks\minted@undefined
+  \else
+    \DeleteFile[\minted@outputdir]{\jobname.mintedcmd}%
+    \DeleteFile[\minted@outputdir]{\jobname.mintedmd5}%
+  \fi
+  \DeleteFile[\minted@outputdir]{\jobname.pyg}%
+  \DeleteFile[\minted@outputdir]{\jobname.out.pyg}%
+}
 \endinput
 %%
 %% End of file `minted.sty'.
diff --git a/tfm.pdf b/tfm.pdf
index 4708bb5..8c7bd3b 100644
--- a/tfm.pdf
+++ b/tfm.pdf
diff --git a/tfm.tex b/tfm.tex
index 49a769e..f0d813a 100644
--- a/tfm.tex
+++ b/tfm.tex
@@ -65,11 +65,11 @@ recientemente en el Instituto IMDEA Software en respuesta a la creciente
 necesidad de disponer de herramientas fiables de verificación formal de
 criptografía.
 
-En este trabajo se abordará la implementación de una mejora en el procesador de
-lenguaje de EasyCrypt, sustituyéndolo por una máquina abstracta derivada de la
-ZAM (lenguaje OCaml). 
-
-(TODO: crypto, reescritura de términos, máquinas abstractas, mejoras a EasyCrypt)
+En este trabajo se abordará la implementación de una mejora en el reductor de
+términos de EasyCrypt, sustituyéndolo por una máquina abstracta simbólica. Para
+ello se estudiarán e implementarán previamente dos máquinas abstractas muy
+conocidas, la Máquina de Krivine y la ZAM, introduciendo variaciones sobre ellas
+y estudiando sus diferencias desde un punto de vista práctico.
 
 \chapter*{Abstract}
 
@@ -82,7 +82,11 @@ these tools is EasyCrypt, developed recently at IMDEA Software Institute in
 response to the increasing need of reliable formal verification tools for
 cryptography.
 
-(TODO: crypto, term rewriting, abstract machines, EasyCrypt impovements)
+This work will focus on the improvement of the EasyCrypt's term rewriting
+system, replacing it with a symbolic abstract machine. In order to do that, we
+will previously study and implement two widely known abstract machines, the
+Krivine Machine and the ZAM, introducing some variations and studying their
+differences from a practical point of view.
 
 \emptypage
 \tableofcontents
@@ -146,7 +150,7 @@ security, potentially worse that not having any security at all.
 
 In order to have the best guarantee that some cryptographic construction meets
 its security requirements, we can use use formal methods to prove that the
-requirements follow from the assumptions (scenario). (TODO: some more explaining.)
+requirements follow from the assumptions (scenario).
 
 While mathematical proofs greatly enhance the confidence we have in that a given
 cryptosystem behaves as expected, with the recent increase in complexity it has
@@ -165,8 +169,6 @@ Coq\footnote{\url{http://coq.inria.fr/}} and
 Isabelle\footnote{\url{http://isabelle.in.tum.de/}} are examples of widely used
 proof assistants.
 
-(TODO: more explaining, screenshots?)
-
 One downside of proof assistants is that they require a considerable amount of
 knowledge from the user, making them difficult to use for people that is not
 somewhat fluent with theoretical computer science and logic. This is a
@@ -214,26 +216,21 @@ sub-languages for working with different things, e.g., representing games,
 developing the proofs, etc. One of them is specially relevant in this thesis:
 the \textbf{expression language}. It is the language EasyCrypt uses to define
 typed values, like quantified formulas, arithmetic expressions, functions,
-function application and such. (TODO: briefly explain what it is used for and
-what can be improved)
-
-
-
-
-\section{Term Rewriting}
-
-(TODO: explain the need to improve the EasyCrypt's one)
+function application and such, and developing proofs relies heavily on the
+manipulation of this expressions.
 
 
 
 \section{Contributions} %%
 
-(TODO:)
-
-\begin{itemize}
-\item Study and implement some rewriting engines
-\item Improve the EasyCrypt's one
-\end{itemize}
+In this work we will study and implement some well-known abstract machines to
+improve the EasyCrypt's current term rewriting engine. As we will see in the
+corresponding section (~\ref{cha:reduction-easycrypt}), the current
+implementation is an ad-hoc solution that works well, but is monolithic,
+difficult to extend and somewhat inefficient. Before that, we will introduce
+some theory to the field of term rewriting and implement both the Krivine
+Machine and the ZAM, as a way to understand their differences and which is the
+best reference to improve the EasyCrypt's engine.
 
 
 
@@ -246,13 +243,13 @@ what can be improved)
 
 \chapter{CRYPTOGRAPHY} %%%%%%%%%%
 
-(TODO: brief introduction to crypto: encryption (signatures?) etc.)
-
+In this chapter we will review some concepts related to how cryptographic proofs
+are built, in order to understand how EasyCrypt works and how proofs are written
+in it.
 
+\section{Public-key Encryption} %%
 
-\section{Asymmetric Cryptography} %%
-
-Here we will introduce some of the most fundamental concepts in asymmetric
+Here we will introduce some basic concepts in asymmetric
 cryptography, as they will be useful to understand the next sections on
 EasyCrypt's proof system and sequences of games (section
 \ref{sec:sequences-games}).
@@ -272,16 +269,24 @@ $$\Enc(pk,M) = C$$
 $$\Dec(sk,C) = M$$
 
 That is, a message ($M$) can be encrypted using a public key to obtain a
-ciphertext ($C$).
-
-(TODO: expand)
+ciphertext ($C$). In turn, a ciphertext ($C$) can be decrypted using a private
+key to obtain a message ($M$). Any \textbf{complete} encryption algorithm must
+satisfy the following property, given that $pk$ and $sk$ were obtained by a call
+to $\KG$:
 
+$$\Dec(sk, \Enc(pk,M)) = M$$
 
 \section{Proofs by reduction} %%
 \label{sec:proofs-reduction}
 
-(TODO: explain: Shannon + perfect security size problems, need to rely on strong
-primitives -RSA, DDH...- and use them in reduction proofs)
+In cryptography it is usually not possible to prove \textbf{perfect security},
+as the only possible way to archieve it would be using keys as long as the
+message (Shannon's theory of information). So, the usual approach is to prove
+that some cryptographic protocol's security can be \textbf{reduced} to the
+security of some well-known primitive that is believed to be
+\textbf{computationally untractable}. That is, the security relies on the
+unability of any human being to solve some computationally hard problem.  The
+overall structure of this proofs is represented in the figure \ref{fig:proofs}.
 
 \begin{figure}[ht]
   \centering
@@ -302,8 +307,12 @@ primitives -RSA, DDH...- and use them in reduction proofs)
   \label{fig:proofs}
 \end{figure}
 
-
-
+One of the most famous hard problems in cryptography is \textbf{integer
+  factorization}. It can be proven that the computational power needed to factor
+the product of two big primes grows exponentially on the size of the primes,
+making it a practically impossible task to archieve for sufficiently big prime
+numbers. The RSA cryptosystem, for example, can be proven secure because it can
+be reduced to the integer factorization problem.
 
 \section{Sequences of games} %%
 \label{sec:sequences-games}
@@ -318,14 +327,13 @@ last one being usually encoded as a function (probabilistic program). In the
 end, we will want the sequence of games to form a proof by reduction (see
 section \ref{sec:proofs-reduction}), where the transition of games proves that
 our system can be reduced, under certain conditions, to some well-known
-cryptographic primitive (TODO: is this correct?).
-
-(TODO: explain transitions and events (adversary winning))
+cryptographic primitive. We say that the adversary \textbf{wins} when certain
+event takes place. It generally has to do with his capacity to extract some
+information or correctly guess some data.
 
-In order to see a practical example of how sequences of games work, let us
-define the following game:
+We can define the following game in order to see a practical example of how
+sequences of games work:
 
-\newpage
 \begin{game}[caption=IND-CPA game (from \cite{BartheGB09}),
   label={lst:indcpa}]{}
   $(pk,sk) \leftarrow \KG();$
@@ -335,21 +343,31 @@ define the following game:
   $\tilde{b} \leftarrow A_2(c)$
 \end{game}
 
-The Game \ref{lst:indcpa} can be used to define the IND-CPA property of public
-key encryption schemes. (TODO: explain IND-CPA)
+The game \ref{lst:indcpa}\footnote{$\KG$
+  and $\Enc$
+  are the key generation and encryption functions provided by the encryption
+  algorithm, respectively, and $A_1$
+  is the encoding of the adversary} can be used to define the IND-CPA property
+of public key encryption schemes. \textbf{IND-CPA} (Indistinguishability Under
+Chosen Ciphertext Attacks) means that the adversary is unable to distinguish
+between pairs of ciphertexts. The IND-CPA game encodes this fact by letting the
+adversary chose two messages, encrypting one of them, and making him guess which
+one was encrypted. In this case, the event that makes the adversary win is that he
+correctly guesses which of his plaintexts was encrypted. In a full sequence of
+games, we would start with this game and apply transformations over it trying to
+preserve the probability of that event (the adversary winning) constant. The
+final game would hopefully be one in which the calls 
+
 
-In the game, $\KG$ and $\Enc$ are the key generation and encryption functions
-provided by the encryption algorithm, respectively, and $A_1$ is the encoding of
-the adversary.
 
-(TODO)
 
 
 
 \section{Verification: EasyCrypt} %%
 \label{sec:verif-easycrypt}
 
-EasyCrypt has different languages to perform different tasks:
+EasyCrypt allows the encoding and verification of game-based proofs, but it has
+different languages to perform different tasks:
 
 
 \subsection{Specification languages}
@@ -358,6 +376,7 @@ This are the languages EasyCrypt uses to declare and define types, functions,
 axioms, games, oracles, adversaries and other entities involved in the proofs.
 
 \subsubsection{Expressions}
+\label{sec:expressions}
 
 The main specification language of EasyCrypt is the expression language, in
 which \textbf{types} are defined together with \textbf{operators} that can be
@@ -452,7 +471,7 @@ called \textbf{pWhile} \cite{BartheGB12} (probabilistic while) to define them:
 
 \subsection{Proof languages}
 
-These are the languages used to write and prove theorems:
+% These are the languages used to write and prove theorems:
 
 \subsubsection{Judgments}
 
@@ -507,7 +526,8 @@ and starts accepting \textbf{tactics} until the current goal is trivially
 true. Tactics are indications on what rules EasyCrypt must apply to transform
 the current goal.
 
-This is a simplified example of proof from the EasyCrypt's library:
+This is a simplified example of proof from the EasyCrypt's library, where we can
+see the tactics applied between the \rawec{proof} and \rawec{qed} keywords:
 
 \begin{easycrypt}[caption=Tactics usage, label={lst:tactics}]{}
 lemma cons_hd_tl :
@@ -524,7 +544,6 @@ proof.
 qed.
 \end{easycrypt}
 
-(TODO: briefly explain proof)
 
 
 
@@ -533,7 +552,21 @@ qed.
 
 
 
-\section{Term Rewriting Systems/Theory} %%
+\section{Introduction} %%
+
+In computing and programming languages it is common to encounter scenarios where
+objects (e.g., code) get transformed gradually for simplification, to perform a
+computation, etc. The transformations must obey some rules that relate ``input''
+and ``output'' objects, that is, how to make the transition from one object to
+the other. When we take both the objects and the rules and study them as a
+whole, the result is an \textbf{abstract reduction system} \cite{Baader98}.
+
+This is a very general framework, but for what this work is concerned, we are
+specially interested in reasoning about rewriting of ($\lambda$-)terms. In the
+end we will want to improve how EasyCrypt is able to reduce terms in its
+expression language, so we will start by understanding Lambda Calculus and how
+it is reduced, because it is very similar to how EasyCrypt represents its own
+terms.
 
 
 
@@ -543,11 +576,10 @@ The \textbf{Lambda Calculus} \cite{Church36} is a formal system developed by
 Alonzo Church in the decade of 1930 as part of his research on the foundations
 of mathematics and computation (it was later proven to be equivalent to the
 Turing Machine). In its essence, the Lambda Calculus is a simple term rewriting
-system that represents computation through the \textbf{application of
-  functions}.
+system that represents computation through \textbf{function application}.
 
-Following is the grammar representing \textbf{lambda terms} ($\mathcal{T}$),
-also called ``well-formed formulas'':
+Following is the grammar representing \textbf{$\lambda$-terms} (lambda-terms,
+$\mathcal{T}$):
 
 \begin{bnf}[caption=Lambda Calculus, label={lst:lambda}]{}
   $\mathcal{T} ::= x$               variable
@@ -563,7 +595,7 @@ are \textbf{bound} instances. The \textbf{application} rule represents function
 evaluation ($\mathcal{T}_1$) with an actual argument ($\mathcal{T}_2)$.
 
 Seen as a term rewriting system, the Lambda Calculus has some reduction rules
-that can be applied over terms in order to perform the computation:
+that can be applied over terms in order to perform the computation.
 
 
 \subsection{Reduction rules}
@@ -579,11 +611,18 @@ and can be outlined in the following way:
     \mathcal{T}_2]}
 \]
 
+
 An application with an abstraction in the left-hand side is called a
 \textbf{redex}, short for ``reducible expression'', because it can be
-$\beta$-reduced following the rule. The semantics of the rule match with the
-intuition of function application: the result is the body of the function with
-the formal parameter replaced by the actual argument.
+$\beta$-reduced following the rule\footnote{The <<$\rightsquigarrow$>> symbol
+  means ``reduces to'', and <<$\overset{\star}{\rightsquigarrow}$>> is its
+  symmetric and transitive closure (``reduces in 0 or more steps to'')} . The
+semantics of the rule match with the intuition of function application: the
+result is the body of the function with the formal parameter replaced by the
+actual argument. It has to be noted that even when a term is \textit{not} a
+redex, it can contain some other sub-expression that indeed is; the problem of
+knowing where to apply each reduction will be addressed in section
+\ref{sec:reduction-strategies}.
 
 The \textbf{substitution operation} $\mathcal{T}_1[x := \mathcal{T}_2]$ replaces
 $x$ by $\mathcal{T}_2$ in the body of $\mathcal{T}_1$, but we have to be careful
@@ -627,131 +666,108 @@ In general, we will treat $\alpha$-equivalent and $\eta$-equivalent functions as
 interchangeable.
 
 
-\subsection{Types}
-
-Until now, we have been discussing the \textbf{untyped} Lambda Calculus, where
-there are no restrictions to the kind of terms we can build. Every formula
-resulting from the grammar (\ref{lst:lambda}) is a valid term. There are
-alternative interpretations of the Lambda Calculus, the \textbf{Typed Lambda
-  Calculi}, which give \textbf{typing rules} to construct ``well-typed terms''
-(terms that have a \textbf{type} associated to it). The point is being unable to
-construct terms that ``make no sense'', like the ones that encode logical
-paradoxes or whose evaluation does not finish.
-
-As previously seen, EasyCrypt uses a statically typed expression language that
-in turn is represented internally as a typed Lambda Calculus. (TODO: put in
-context)
-
-
-\subsection{Extensions}
-\label{sec:extensions}
-
-Until there we have seen the ``basic'', or ``pure'' Lambda Calculus, where the
-only data primitive is the function. Being turing complete, it is all that is
-needed to express all the possible computations, but there are extensions that
-make it more suitable to be manipulated by human beings.
-
-One of the most typical is having natural numbers as primitive terms, that is
-way more convenient that representing them as \textbf{church numerals}:
-
-$$0 \Longleftrightarrow (\lambda f . (\lambda x . x))$$
-$$1 \Longleftrightarrow (\lambda f . (\lambda x . (f \: x)))$$
-$$2 \Longleftrightarrow (\lambda f . (\lambda x . (f \: (f \: x))))$$
-$$...$$
+% \subsection{Types}
 
-As with the natural numbers, any data structure can be encoded in basic Lambda
-Calculus \cite{Mogensen00}, but the representation is complex and the terms can
-rapidly become very difficult to handle. This is why the first major extension
-comes in: \textbf{algebraic data types}.
+% Until now, we have been discussing the \textbf{untyped} Lambda Calculus, where
+% there are no restrictions to the kind of terms we can build. Every formula
+% resulting from the grammar (\ref{lst:lambda}) is a valid term. There are
+% alternative interpretations of the Lambda Calculus, the \textbf{Typed Lambda
+%   Calculi} \cite{Church40}, which give \textbf{typing rules} to construct
+% ``well-typed terms'' (terms that have a \textbf{type} associated to it). The
+% point is being unable to construct terms that ``make no sense'', like the ones
+% that encode logical paradoxes or whose evaluation does not finish.
 
-\subsubsection{Algebraic Data Types}
 
-If we want to be able to extend the Lambda Calculus to encode structured data,
-we will want to have some way to build new data, instead of extending the
-language with every data type we can imagine (naturals, booleans,
-etc.). \textbf{Algebraic data types} (ADT's) offer a powerful way to compose
-existing terms into more complex ones\footnote{Although ADT's are a
-  type-theoretical concept, as we are concerned with the untyped version of the
-  Lambda Calculus, we will be only interested in how it allows us to build new
-  \textbf{terms}, not \textbf{types}. }. The composition can be made in two
-different ways:
 
-\paragraph{Product types}
 
-If we have some terms $T_1, T_2, ..., T_n$, we can produce a new term
-that is the ordered \textit{grouping} of them: $T = (T_1, T_2, ..., T_n)$. The
-resulting structure is often called an \textbf{n-tuple}.
-
-\paragraph{Sum types}
+\section{Normal forms}
 
-If we have some terms $T_1, T_2, ..., T_n$, we can produce a new term that can
-be \textbf{disjoint union} of them:
-$T = C_1(T_1) \: | \: C_2(T_2) \: | \: ... \: | \: C_n(T_n)$. It consists of a
-series of \textbf{variants}, one for every previous term, each tagged by a
-unique \textbf{constructor} ($C_1-C_n$). A sum type will take the form of one
-(and only one) of the variants, and the constructor is used to in runtime to
-know which of the variants it actually is.
+In abstract rewriting systems, a term $a$ is in \textbf{normal form} whenever it can
+not be reduced any further. That is, there does not exist any other term $b$
+such that $a \rightsquigarrow b$.
 
+When a $\lambda$-term has no subexpressions that can be reduced, it is already
+in normal form. There are also three additional notions of normal form in Lambda
+Calculus:
 
+\begin{itemize}
+\item \textbf{Weak normal form}: $\lambda$-terms with form
+  $(\lambda x . \mathcal{T})$ are not reduced
+\item \textbf{Head normal form}: $\lambda$-terms with form $(x \: \mathcal{T})$
+  are not reduced
+\item \textbf{Weak head normal form}: neither $\lambda$-terms in weak or head
+  normal form are not reduced
+\end{itemize}
 
-As a special interesting case, it is often useful not to parameterize a variant
-(sum type) and just have the constructor as one of the values. This can be done
-naturally by parameterizing it over the empty product type $()$, also called
-\textbf{unit}.
+The Lambda Calculus is \textbf{not normalising}, so there is not any guarantee
+that any normal form exists for a given term.
 
-While the
 
-\subsubsection{Fixpoints}
 
+\section{Reduction Strategies} %%
+\label{sec:reduction-strategies}
 
-There's also the problem of recursion: as the lambda
-functions are anonymous, they can't simply refer to themselves. As with the
-church numerals, there are ways to \cite{PeytonJones87}
+When reducing $\lambda$-terms, a \textbf{reduction strategy} \cite{Sestoft02} is
+also needed to remove the ambiguity about which sub-expression on a given term
+should be reduced next.  This is usually an algorithm that given some reducible
+term (redex), points to the redex inside it that sould be reduced next.
 
----
+Each reduction strategy knows when to stop searching based on some normal form
+(of the four we've already seen).
 
-http://adam.chlipala.net/cpdt/html/Equality.html
+Two of the most common reduction strategies, and the ones we will be more
+concerned with in this work, are the following:
 
 \begin{itemize}
-\item Alpha reduction
-\item Beta reduction
-\item ...
+\item \textbf{Call-by-name} reduces the leftmost outermost redex, unless it is
+  in weak head normal form. Due to the head normal form, the evaluation is
+  non-strict.
+\item \textbf{Call-by-value} reduces the leftmost innermost redex, unless it is
+  in weak normal form. The evaluation is strict.
+\item \textbf{Applicative order} reduces the leftmost innermost redex, unless it is
+  in normal form. The evaluation is strict.
 \end{itemize}
 
+The Lambda Calculus has an interesting property called \textbf{confluence}, that
+means that whenever some term has more than one possible reduction, there exists
+another term to which both branches will converge in the end:
 
+\[
+  \inferrule* [left=Confluence]
+  {a \overset{\star}{\rightsquigarrow} b_1 \\ a \overset{\star}{\rightsquigarrow} b_2}
+  {\exists c . (b_1 \overset{\star}{\rightsquigarrow} c \wedge
+    b_2 \overset{\star}{\rightsquigarrow} c)}
+\]
 
-\section{Evaluation Strategies} %%
-
-\cite{Sestoft02}
-
-
-
-\section{Normal forms}
+What this means is that the reduction order does not really matter unless one of
+them leads to non-termination (an infinite chain). Non-strict strategies, such
+as call-by-name, helps avoiding non-terminating reductions thanks to its head
+normal form (which does not evaluate function arguments until needed).
 
 
 
+\newpage
 \section{Abstract Machines} %%
 
-(TODO: basic intro, motivation, function application implementations
-(push-enter, eval-apply))
-
-
-\subsection{Krivine Machine} %%%%%%%%%%
+In order to actually implement the reduction over $\lambda$-terms, there are
+some different ways with different advantages and drawbacks, the most
+``extreme'' being direct interpretation of source code and compilation to native
+instructions of a real machine.
 
-\cite{Krivine07}
-\cite{Douence07}
-
-
-\subsection{ZAM: Standard version}
-
-\cite{Leroy90}
-
-
-\subsection{ZAM: Alternative version}
-
-\cite{LeroyG02}
+An intermediate point is simulating an \textbf{abstract machine} to which we can
+feed a sequence of instructions (requiring a previous compilation process) or
+the original language itself if it is simple enough. This approach is useful
+because it is more portable than native code generation while being more
+efficient than plain interpretation.
 
+There can be different abstracts machine for the same language, differing not
+only in their implementation details but in the reduction strategies they
+implement, so the output can also be different, with some machines implementing
+\textbf{stronger} reductions than others (i.e., to normal form).
 
+In the next part of the thesis we will study and implement two widely-known
+abstract machines to reduce $\lambda$-terms, and improve the EasyCrypt current
+reduction machinery by applying the same concepts.
 
 
 
@@ -780,15 +796,21 @@ call-by-name reduction strategy for pure lambda terms. What that means is that:
 \item It stops reducing whenever the formula is in weak-head normal form, that
   is:
   \begin{itemize}
-  \item does not reduce abstractions: $(\lambda x . \mathcal{T})$
-  \item does not reduce applications of non-abstractions: $(x \: \mathcal{T})$
+  \item does not further reduce abstractions: $(\lambda x . \mathcal{T})$
+  \item does not reduce arguments before substitution $(x \: \mathcal{T})$
   \end{itemize}
 \end{itemize}
 
+
+
+\section{Target language}
+\label{sec:krivine-target-language}
+
 The first thing we need to have is an encoding of the language we will be
 reducing, in this case the Lambda Calculus. We will define a module,
 \textbf{Lambda}, containing the data structure and basic operations over it:
 
+\newpage
 \begin{code}
   \begin{minted}[fontsize=\footnotesize]{ocaml}
 type symbol = string * int
@@ -849,17 +871,20 @@ pretty-printing. The function <<of_lambda>> accepts traditional lambda terms
 (Lambda.t) and returns its representation as a term using de Bruijn notation
 (DBILambda.t). Now we are ready to implement the actual reduction.
 
+
+
+\section{Reduction}
+
 The Krivine Machine has a state $(C, S, E)$ consisting on the \textbf{code} it
 is evaluating ($C$), an auxiliar \textbf{stack} ($S$) and the current
-\textbf{environment} ($E$). The code is just a Lambda expression, the stack is
-where the machine will store \textbf{closures} consisting of non-evaluated code
-together with its environment at the time the closure was created, and an
-environment associates variables (de Bruijn indices) to closures.
+\textbf{environment} ($E$). The code is just the current Lambda expression, the
+stack holds \textbf{closures} (not yet evaluated code + the environment at the
+time the closure was created), and an environment that associates variables (de
+Bruijn indices) to values (closures).
 
 The typical description of the Krivine Machine \cite{Douence07} is given by the
 following set of rules:
 
-\newpage
 \begin{center}
 \line(1,0){250}
 \end{center}
@@ -896,10 +921,9 @@ de Bruijn index $i$.
 \end{itemize}
 
 From this specification we can write a third module, \textbf{KM}, to define the
-data structures (state, closure, stack) and implement the reduction rules of the
-Krivine Machine:
+data structures (state, closure, stack) and implement the symbolic reduction
+rules of the Krivine Machine:
 
-\newpage
 \begin{code}
   \begin{minted}[fontsize=\scriptsize]{ocaml}
 module KM = struct
@@ -1005,35 +1029,20 @@ ocaml> List.iter dbi_and_red [ex_m1; ex_m2];;
 
 
 
-\section{Extending the machine} %%
+\section{Extended version} %%
 
 Now that we have a working Krivine Machine over basic Lambda Terms, we want to
-extend it to work with the extensions we saw in section \ref{sec:extensions}:
-\textbf{case expressions} and \textbf{fixpoints}.
+extend it to work with some extensions: \textbf{case expressions} and
+\textbf{fixpoints}.
 
 
 \subsection{Case expressions}
 
-%% TODO: maybe later
-% \begin{center}
-% \line(1,0){250}
-% \end{center}
-% \begin{table}[H]
-% \centering
-% \begin{tabular}{lllll}
-% $(Case(M, BS), S, E)$ & \rightsquigarrow & $(M, CaseCont(BS,E) :: S, E)$ \\ \\
-% $(Constr(X, MS), CaseCont(X, AS) :: S, E)$ & \rightsquigarrow & $(M, CaseCont(BS,E)
-%                                                             :: S, E)$ \\ \\
-% $(\lambda M, N :: S, E)$ & \rightsquigarrow & $(M, S, N :: E)$ \\ \\
-% $(0, S, (M,E_1) :: E_2)$ & \rightsquigarrow & $(M, S, E_1)$
-% \end{tabular}
-% \end{table}
-% \begin{center}
-% \line(1,0){250}
-% \end{center}
-
 First, we will need to extend our definition of the Lambda Calculus to support
-constructors and case expressions, both in Lambda and DBILambda:
+constructors and case expressions, both in Lambda and DBILambda. Constructors
+are just atomic symbols, optionally parameterized by some arguments, used to
+encode arbitrary data. Case expressions are used to ``destructure'' constructors
+and extract the value of their parameters:
 
 \begin{code}
   \begin{minted}[fontsize=\scriptsize]{ocaml}
@@ -1146,12 +1155,9 @@ let peano_of_int ?(base=Constr (z, [])) n = peano_add n base
 \subsection{Fixpoints}
 
 The second extension we are going to implement in our Krivine Machine is the
-ability to support fixpoints, that is, limited recursion. To prevent infinite
-reductions, every fixpoint must be defined over a constructor, in a way that
-(TODO: this is ZAM!).
-
-Again, we extend the data structures of the Lambda Calculus. As the extension to
-DBILambda follows trivially, we will omit it here:
+ability to support fixpoints, that is, recursion. Again, we extend the data
+structures of the Lambda Calculus. As the extension to DBILambda follows
+trivially, we will omit it here:
 
 \begin{code}
   \begin{minted}[fontsize=\scriptsize]{ocaml}
@@ -1170,7 +1176,6 @@ The ``Fix'' constructor is parameterized by a symbol and another lambda
 term. The symbol is the name of the fixpoint, and will expand to itself when
 referenced inside the term. Let's see an example:
 
-\newpage
 \begin{code}
 \begin{verbatim}
 fix(λf.λc. case c of (s(x) → s(s(f x)))
@@ -1213,7 +1218,6 @@ whenever some variable refers to a fixpoint closure, the result is its body,
 with the side effect of keeping the closure it in the environment (so that it is
 automatically bound to the first argument <<f>> of itself).
 
-\newpage
 The fixpoint tests:
 
 \begin{code}
@@ -1244,62 +1248,567 @@ applied once for each iteration over the number: in this case, <<g>> adds 3 to
 its argument, so the whole term is a ``by 3'' multiplier.
 
 
+
+
 \chapter{ZAM} %%%%%%%%%%
 
+The ZAM (ZINC Abstract Machine) \cite{Leroy90} is a call-by-value variant of the
+Krivine Machine, and currently powers the bytecode interpreter of the Caml Light
+and OCaml languages. We will implement the version introduced in
+\cite{LeroyG02} as a previous step before tackling the implementation of
+EasyCrypt's new reduction machinery. Again, the full code is available in the
+annex \ref{sec:zam-source-code}.
 
+As with the Krivine Machine before, it will be able to handle extended
+$\lambda$-terms with case expressions and fixpoints, but this time the machine
+will interpret actual abstract code instead of implementing symbolic reduction,
+so we will need an extra step to compile the the $\lambda$-terms to machine
+code. Also, we will skip the progressive exposition of the basic and extended
+machine, as it has already been done in the previous section, and just implement
+the final version. To finish, we will show how to use it to archieve
+\textbf{strong reduction}.
 
 
 
+\section{Target language}
 
-\chapter{REDUCTION IN EASYCRYPT} %%%%%%%%%%
+As the reference work \cite{LeroyG02} aimed to improve the performance of strong
+reduction in proof assistants, this version of the ZAM works over type-erased
+terms of the Calculus of Constructions \cite{Coquand88}, adding
+\textbf{inductive types} (for our purposes, equivalent to the previously
+implemented algebraic data types) and \textbf{fixpoints}.
+
+For this task, we will define a module called \textbf{CCLambda} with a type
+encoding the terms of our language:
+
+\begin{code}
+  \begin{minted}[fontsize=\scriptsize]{ocaml}
+module CCLambda = struct
+    type t = Var of symbol | App of t * t | Abs of symbol * t
+             | Constr of t constr | Case of t * (symbol constr * t) list
+             | Fix of symbol * symbol list * symbol * t
+    and 'a constr = symbol * 'a list
 
+    (* ... *)
+end
+  \end{minted}
+\end{code}
 
+The only difference we can see here with respect to the encoding of terms in the
+K-Machine (section \ref{sec:krivine-target-language}) is the more elaborate
+fixpoints. Even though our $\lambda$-terms are not typed, the Calculus of
+Constructions' fixpoints need an argument (``guard'') to structurally to the
+recursion and prevent infinite unrolling. We will represent fixpoints as <<Fix
+(f, xs, c, m)>>, where <<f>> is the symbol (bound in <<m>>) referring to the
+fixpoint itself, <<xs>> is the argument list, <<c>> is the guard (a
+constructor), and <<m>> is the $\lambda$-term.
 
-\section{Architecture overview} %%
 
 
+\section{Compilation}
 
-\section{Data types}
+Unlike the previous implementation, in this case we are going to implement a
+more efficient version. Instead of symbolically evaluating the $\lambda$-terms
+we need an extra step to compile them to some intermediate code Now we need to
+be able to compile $\lambda$-terms to instructions targeting the ZAM runtime,
+which will do the actual reduction.
 
+This is the type encoding the machine instructions:
 
+\begin{code}
+  \begin{minted}[fontsize=\scriptsize]{ocaml}
+module WeakRed = struct
+    open CCLambda
+
+    type dbi = symbol * int
+    type instr =
+      | ACCESS of dbi
+      | CLOSURE of instrs
+      | ACCLOSURE of symbol
+      | PUSHRETADDR of instrs
+      | APPLY of int
+      | GRAB of symbol
+      | RETURN
+      | MAKEBLOCK of symbol * int
+      | SWITCH of (symbol constr * instrs) list
+      | CLOSUREREC of (symbol * symbol list * symbol) * instrs
+      | GRABREC of symbol
+    and instrs = instr list
+    and mval =
+      | Cons of mval constr
+      | Clos of instrs * env
+      | Ret of instrs * env * int
+    and env = mval list
+    and stack = mval list
+    and state = {
+        st_c : instrs;
+        st_e : env;
+        st_s : stack;
+        st_n : int;
+    }
 
-\section{Implementation}
+    (* ... *)
+end
+  \end{minted}
+\end{code}
 
+The <<WeakRed.compile>> function in the code does the actual work of translating
+$\lambda$-terms to a sequence of instructions.
 
+\section{Reduction}
 
+The figure \ref{fig:zam-rules} details the reduction rules. The implementation
+is straightforward (although contrived) and follows the same structure as the
+Krivine Machine. I refer the reader to the annex in order to see how this rules
+are actually encoded in our program.
 
+\begin{figure}[h]
+  \centering
+  \includegraphics[width=1\textwidth]{img/zamrules.png}
+  \caption{ZAM reduction rules (from \cite{LeroyG02})}
+  \label{fig:zam-rules}
+\end{figure}
 
-\part{EPILOGUE} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\newpage
+At this point, we can try some code examples to see the results:
 
+\begin{code}
+\begin{verbatim}
+WEAK REDUCTION TEST
+Lambda term:
+    ((λx.x) (λy.(((λz.z) y) (λt.t))))
+Reduced term:
+    (λy.(((λz.z) y) (λt.t)))
+----------------------------------------------------------
 
+WEAK REDUCTION TEST
+Lambda term:
+    (((λf.(λx.(f (f x)))) (λy.y)) (λz.z))
+Reduced term:
+    (λz.z)
+----------------------------------------------------------
 
+WEAK REDUCTION TEST
+Lambda term:
+    ((λc.(case c of (Cons(x,xs) → x)
+                    (Nil() → Nil())))
+     Cons((λm.m), Nil()))
+Reduced term:
+    (λm.m)
+----------------------------------------------------------
 
-\chapter{CONCLUSIONS} %%%%%%%%%%
+WEAK REDUCTION TEST
+Lambda term:
+    (fix_0(λf.λc. (case c of (s(x) → s(s((f x))))
+                  (z() → z())))
+     s(s(s(z()))))
+Reduced term:
+    s(s(s(s(s(s(z()))))))
+----------------------------------------------------------
+\end{verbatim}
+\end{code}
 
-In this work we began by exposing the need to verify cryptographic protocols and
-what is the role that the EasyCrypt framework plays in the field. After
-some background in cryptography and analysing the inner working of
-EasyCrypt.
 
-\begin{itemize}
-\item Brief wrapping of importance of verified crypto today
-\item Survey of available reduction machineries, differences between them
-\item Improvements to EasyCrypt: modularity, extensibility, efficiency (?)
-\item Problems encountered during the implementation (debugging!!! specially the
-  compiled one, progressive replacing of the EasyCrypt's one due to state)
-\end{itemize}
 
+\newpage
+\section{Strong reduction}
+
+Once we have the machinery to perform call-by-value reduction (that is, until it
+reaches a weak normal form) we can use a callback procedure to apply it
+repeatedly and archieve strong normalization. The actual implementation is in
+the module <<StrongRed>> (annex \ref{sec:zam-source-code}).
+
+The most interesting detail about using the readback procedure is the need to
+support \textbf{accumulators} as another case of $\lambda$-terms. Accumulators
+are just terms that cannot get reduced, and are self-propagating: whenever a
+function is applied to an accumulator, the result is an accumulator containing
+the application of the function to the previous accumulator. The callback
+procedure needs it in order to reach the previously-unreachable terms inside an
+abstraction. Here are the modifications to the data structures:
 
+\newpage
+\begin{code}
+  \begin{minted}[fontsize=\scriptsize]{ocaml}
+module CCLambda = struct
+    type t = Var of symbol | App of t * t | Abs of symbol * t
+             | Constr of t constr | Case of t * (symbol constr * t) list
+             | Fix of symbol * symbol list * symbol * t
+             | Acc of t    (* Accumulators *)
+    and 'a constr = symbol * 'a list
 
+    (* ... *)
+end
 
-\chapter{FUTURE WORK} %%%%%%%%%%
+module WeakRed = struct
+    open CCLambda
+
+    type dbi = symbol * int
+    type instr =
+      | ACCESS of dbi
+      | CLOSURE of instrs
+      | ACCLOSURE of symbol
+      | PUSHRETADDR of instrs
+      | APPLY of int
+      | GRAB of symbol
+      | RETURN
+      | MAKEBLOCK of symbol * int
+      | SWITCH of (symbol constr * instrs) list
+      | CLOSUREREC of (symbol * symbol list * symbol) * instrs
+      | GRABREC of symbol
+    and instrs = instr list
+    and accum =
+      | NoVar of symbol
+      | NoApp of accum * mval list
+      | NoCase of accum * instrs * env
+      | NoFix of accum * instrs * env
+    and mval =
+      | Accu of accum
+      | Cons of mval constr
+      | Clos of instrs * env
+      | Ret of instrs * env * int
+    and env = mval list
+    and stack = mval list
+    and state = {
+        st_c : instrs;
+        st_e : env;
+        st_s : stack;
+        st_n : int;
+    }
+
+    (* ... *)
+end
+  \end{minted}
+\end{code}
+
+\newpage
+
+And we pass the tests again:
+
+\begin{code}
+\begin{verbatim}
+STRONG REDUCTION TEST
+Lambda term:
+    ((λx.x) (λy.(((λz.z) y) (λt.t))))
+Reduced term:
+    (λy.(y (λt.t)))
+----------------------------------------------------------
+
+STRONG REDUCTION TEST
+Lambda term:
+    (((λf.(λx.(f (f x)))) (λy.y)) (λz.z))
+Reduced term:
+    (λz.z)
+----------------------------------------------------------
+
+STRONG REDUCTION TEST
+Lambda term:
+    ((λc.(case c of (Cons(x,xs) → x)
+                    (Nil() → Nil())))
+     Cons((λm.m), Nil()))
+Reduced term:
+    (λm.m)
+----------------------------------------------------------
+
+STRONG REDUCTION TEST
+Lambda term:
+    (fix_0(λf.λc. (case c of (s(x) → s(s((f x))))
+                             (z() → z())))
+     s(s(s(z()))))
+Reduced term:
+    s(s(s(s(s(s(z()))))))
+----------------------------------------------------------
+\end{verbatim}
+\end{code}
+
+As we were expecting, the first term is now \textbf{strongly reduced} to
+normal form.
+
+
+
+\chapter{REDUCTION IN EASYCRYPT} %%%%%%%%%%
+\label{cha:reduction-easycrypt}
+
+The current approach that EasyCrypt uses to reduce terms is the iteration over
+the formula and application of ad-hoc transformations based on the information
+provided by its type and global state.
+
+To archieve strong reduction, EasyCrypt uses a similar ``read-back'' protocol to
+the one we've already seen in the ZAM: repeatedly application of a function that
+iterates the current formula and tries to reduce it in a call-by-value
+fashion. When there is no other expression to be reduced, the read-back
+procedure stops and the normalized formula is returned.
+
+
+
+\section{Target language} %%
+
+Each formula is composed by some metadata (type, free variables, unique tag)
+together with a \textbf{node} that holds the actual structure of the term:
+
+\begin{code}
+  \begin{minted}[fontsize=\scriptsize]{ocaml}
+type f_node =
+  | Fquant  of quantif * bindings * form
+  | Fif     of form * form * form
+  | Flet    of lpattern * form * form
+  | Fint    of BI.zint
+  | Flocal  of EcIdent.t
+  | Fpvar   of EcTypes.prog_var * memory
+  | Fglob   of EcPath.mpath     * memory
+  | Fop     of EcPath.path * ty list
+  | Fapp    of form * form list
+  | Ftuple  of form list
+  | Fproj   of form * int
+  | FhoareF of hoareF
+  | FhoareS of hoareS
+  | FbdHoareF of bdHoareF
+  | FbdHoareS of bdHoareS
+  | FequivF of equivF
+  | FequivS of equivS
+  | FeagerF of eagerF
+  | Fpr of pr
+  \end{minted}
+\end{code}
+
+As there are so much types and corner cases, we will briefly explain what are
+the most important constructors and what are they for:
+
+\begin{itemize}
+\item \textbf{FQuant}: They serve both as universal/existential quantifiers
+  (forall / exists) and lambda abstractions, depending on the value of the
+  <<quantif>> parameter (Lforall, Lexists, Llambda, respectively).
+\item \textbf{Fif}: Conditionals.
+\item \textbf{Fint}: Literal integers.
+\item \textbf{Flocal}: Local variables.
+\item \textbf{Fop}: Operators: as explained in the introduction (section
+  \ref{sec:expressions}). The actual code must be obtained by resolving its path.
+\item \textbf{Fapp}: Function application (to multiple arguments).
+\end{itemize}
+
+\section{Reduction rules}
+
+As the term language of EasyCrypt is more complex than standard Lambda
+Calculus, it has some reduction rules we have not seen befone:
 
 \begin{itemize}
-\item Compile code to abstract machine opcodes to improve efficiency
-\item Tests
-\item Make users able to define their own rules (expand the engine in ``userland'')
+\item $\delta$-reduction (\textbf{delta}): used to unfold global
+  definitions. Affects operators (<<Fop>>).
+\item $\zeta$-reduction (\textbf{zeta}): used to unfold a let expression in its
+  body. Affects let expressions (<<Flet>>).
+\item $\iota$-reduction (\textbf{iota}): used to unfold a case
+  expression. Affects conditionals (<<Fif>>), operators (<<Fop>>).
+\item Logical reduction: used to evaluate logic expressions (And, Or,
+  ...). Affects operators (<<Fop>>).
 \end{itemize}
 
+A structure containing information about which of this reductions must be done
+is passed to every reduction procedure:
+
+\begin{code}
+  \begin{minted}[fontsize=\scriptsize]{ocaml}
+type reduction_info = {
+  beta    : bool;
+  delta_p : (path  -> bool);
+  delta_h : (ident -> bool);
+  zeta    : bool;
+  iota    : bool;
+  logic   : bool;
+}
+  \end{minted}
+\end{code}
+
+
+
+\section{Reduction}
+
+The reduction machinery is implemented in an EasyCrypt module called
+\textbf{EcReduction}. The main entry point is the function <<\textbf{h_red}>>,
+which accepts the target formula and a <<reduction_info>> structure (see
+previous section) and returns the reduced formula according to it. An important
+point is that <<h_red>> only reduces until \textbf{weak normal form}, and there
+is another callback procedure that calls it repeatedly as we've already seen
+with the ZAM machine. So, we need to take that function and replace it with a
+ZAM-like machine to do only the weak reduction.
+
+This is a short fragment of the <<h_red>> function:
+
+\begin{code}
+  \begin{minted}[fontsize=\scriptsize]{ocaml}
+let rec h_red_old ri env hyps f =
+  match f.f_node with
+    (* β-reduction *)
+  | Fapp ({ f_node = Fquant (Llambda, _, _)}, _) when ri.beta ->
+      f_betared f
+
+    (* ζ-reduction *)
+  | Flocal x -> reduce_local ri hyps x
+
+    (* ζ-reduction *)
+  | Fapp ({ f_node = Flocal x }, args) ->
+      f_app_simpl (reduce_local ri hyps x) args f.f_ty
+
+  (* ... *)
+  \end{minted}
+\end{code}
+
+Although it is actually a pretty long function (around 220 lines of code), the
+structure is simple: a pattern matching over the structure of the current
+formula. We will start by defining the state of the new abstract machine and
+replacing the pattern matching by a recursive function over an initial state:
+
+\begin{code}
+  \begin{minted}[fontsize=\scriptsize]{ocaml}
+type st_elm =
+  | Clos of form * menv
+  | ClosCont of bindings
+  | IfCont of form * form
+and stack = st_elm list
+and menv = (EcIdent.t, form) Hashtbl.t
+
+let rec h_red ri env hyps f =
+  let iter st =
+    match (st : EcFol.form * stack * menv) with
+
+    (* β-red *)
+    | ({ f_node = Fapp (f, fs) }, s, e) when ri.beta ->
+       iter (f, List.map (fun f -> Clos (f, e)) fs @ s, e)
+
+  in
+  iter (f, [], Hashtbl.create 100)
+  \end{minted}
+\end{code}
+
+As we can see, the first block is very similar to what we did with the ZAM:
+define a stack, the types of the closures and an environment (for efficiency,
+this time it is implemented as a hash map from variables <<EcIdent.t>> to
+formulas).
+
+The new <<h_red>> function creates an initial state composed by the formula to
+be reduced, an empty stack and an empty environment, and begins the reduction by
+evaluating the auxiliar <<iter>> function in a tail-recursive manner. In this
+example it is included the evaluation of an application: iterate over the
+arguments, putting in the stack a new closure for every one of them.
+
+Here we have the new code that performs the full $\beta$-reduction:
+
+\begin{code}
+  \begin{minted}[fontsize=\scriptsize]{ocaml}
+let rec h_red ri env hyps f =
+  let iter st =
+    match (st : EcFol.form * stack * menv) with
+
+    (* β-red *)
+    | ({ f_node = Fapp (f, fs) }, s, e) when ri.beta ->
+       iter (f, List.map (fun f -> Clos (f, e)) fs @ s, e)
+    | ({ f_node = Fquant (Llambda, [], f) }, s, e) ->
+       iter (f, s, e)
+    | ({ f_node = Fquant (Llambda, (x,_)::bds, f) }, Clos (cf, _) :: s, e) ->
+       let e' = Hashtbl.copy e in
+       Hashtbl.add e' x cf;
+       iter (f_quant Llambda bds f, s, e')
+
+    (* ... *)
+  \end{minted}
+\end{code}
+
+The second and third cases handle the evaluation of a $\lambda$-abstraction: if
+it has no arguments, just keep going with the function body; if there are
+arguments and a function closure is present in the stack, bind the function to
+the closure in the environment and evaluate the function body with one parameter
+less. (The <<f_quant>> and <<f_lambda>> functions are just helpers to build
+formulas)
+
+In order to do some of the other reductions, as they have nothing to do with the
+abstract machine but with global state, we simply have to call standard
+EasyCrypt's functions. For example, to $\delta$-reduce operators and resolve
+local variables:
+
+\begin{code}
+  \begin{minted}[fontsize=\scriptsize]{ocaml}
+let rec h_red ri env hyps f =
+  let iter st =
+    match (st : EcFol.form * stack * menv) with
+    (* ... *)
+
+    | ({ f_node = Fop (p, tys) }, s, e) when ri.delta_p p ->
+       iter (reduce_op ri env p tys, s, e)
+
+    | ({ f_node = Flocal x }, s, e) -> let f' = if Hashtbl.mem e x
+                                              then Hashtbl.find e x
+                                              else reduce_local ri hyps x in
+                                      iter (f', s, e)
+
+    (* ... *)
+  \end{minted}
+\end{code}
+
+\newpage
+Once we are done replacing one by one the standard EasyCrypt operations by
+transitions in the abstract machine, we can see that it works (the formula being
+reduced appears in the upper right of the screen):
+
+\begin{figure}[h]
+  \centering
+  \includegraphics[width=0.8\textwidth]{img/ec1.png}
+  \caption{After entering proof mode}
+\end{figure}
+
+\begin{figure}[h]
+  \centering
+  \includegraphics[width=0.8\textwidth]{img/ec2.png}
+  \caption{Reduced $((\lambda x . x + x) \: 5) \Betared 10$}
+\end{figure}
+
+\begin{figure}[h]
+  \centering
+  \includegraphics[width=1\textwidth]{img/ec3.png}
+  \caption{The proof is finished (``no more goals'' at bottom right)}
+\end{figure}
+
+
+
+\part{EPILOGUE} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+
+
+\chapter{CONCLUSIONS} %%%%%%%%%%
+
+In this work we began by exposing the need to verify cryptographic protocols and
+the role that the EasyCrypt framework plays in the field. Then we moved on to
+abstract rewriting systems and how the current machinery that EasyCrypt uses to
+reduce its formulas could be improved. In order to do that, we implemented two
+abstract machines with multiple variations (extended lambda terms, strong
+reduction) and exposed the differences between them: evaluation strategies,
+symbolic evaluation, bytecode compilation, and so on. Lastly, we continued to
+the source language and current inner workings of EasyCrypt and proceeded to
+replace it in a way that closely resembles the work previously done with the
+abstract machines.
+
+In my opinion, the development of this thesis has resulted in two main
+contributions belonging to different scopes.
+
+The first one is, obviously, the technical improvement of an existing
+tool. Although it is not a contribution on features, but the replacing of an
+existing module for an improved one, we believe it is an important step that had
+to be taken in order to be able to further expand the system in the future.
+
+The second contribution is the insight given by the actual implementation of two
+different abstract machines. While none of these by itself was really needed for
+the task of replacing the EasyCrypt's engine, the research needed to understand
+the concepts of the abstract machines and correctly implement them has proven
+crucial when facing a complex system such as EasyCrypt. It might prove to be
+valuable to some of the interested readers as well, as having the source code of
+both the abstract machines is a nice way to experiment and compare their
+behaviors.
+
+Of course, this work can be improved in many ways. The engine is still
+evaluating code symbolically, which is slower than producing instructions
+(bytecode) for the machine to evaluate. Some EasyCrypt features make this a
+feature not trivial to implement (i.e., it would need to decompile bytecode to
+recover the original terms), but worth keeping it in mind as a possibility for
+future work.
+
 
 
 
@@ -1310,14 +1819,13 @@ EasyCrypt.
 \section{Krivine Machine source code} %%
 \label{sec:kriv-mach-source}
 
-% TODO: UNCOMMENT
-%\inputminted[linenos=true,fontsize=\scriptsize]{ocaml}{code/krivine.ml}
+\inputminted[linenos=true,fontsize=\scriptsize]{ocaml}{code/krivine.ml}
 
 %\newpage
 \section{ZAM source code} %%
+\label{sec:zam-source-code}
 
-% TODO: UNCOMMENT
-%\inputminted[linenos=true,fontsize=\scriptsize]{ocaml}{code/zam.ml}
+\inputminted[linenos=true,fontsize=\scriptsize]{ocaml}{code/zam.ml}
 
 \pagebreak \bibliography{bib}{} \bibliographystyle{ieeetr}
 
diff --git a/to-copy.sh b/to-copy.sh
deleted file mode 100755
index 8352ac2..0000000
--- a/to-copy.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-#!/bin/bash
-
-COPY_D="${HOME}/Copy/univ/master/tfm"
-
-cp -r code *.tex Makefile bib.bib ${COPY_D}/
-cp -r front/*.tex ${COPY_D}/front/