Index: src/ASM/CPP2012policy/algorithm.tex
===================================================================
 src/ASM/CPP2012policy/algorithm.tex (revision 2097)
+++ src/ASM/CPP2012policy/algorithm.tex (revision 2098)
@@ 170,5 +170,5 @@
\mathtt{absolute\_jump},\mathtt{long\_jump}\}$; a function that associates a
pseudoaddress with a memory address and a jump length. We do this to be able
to more ease the comparison of jump lengths between iterations. In the algorithm,
+to ease the comparison of jump lengths between iterations. In the algorithm,
we use the notation $sigma_1(x)$ to denote the memory address corresponding to
$x$, and $sigma_2(x)$ to denote the jump length corresponding to $x$.
Index: src/ASM/CPP2012policy/biblio.bib
===================================================================
 src/ASM/CPP2012policy/biblio.bib (revision 2097)
+++ src/ASM/CPP2012policy/biblio.bib (revision 2098)
@@ 104,5 +104,5 @@
@misc{DC2012,
 title={On the correctness of an optimising assembler for the Intel MCS51 microprocessor},
+ title={{On the correctness of an optimising assembler for the Intel MCS51 microprocessor}},
author = {Dominic P. Mulligan and Claudio {Sacerdoti Coen}},
year = {2012},
Index: src/ASM/CPP2012policy/conclusion.tex
===================================================================
 src/ASM/CPP2012policy/conclusion.tex (revision 2097)
+++ src/ASM/CPP2012policy/conclusion.tex (revision 2098)
@@ 12,6 +12,11 @@
where it is important to have as small solution as possible.
+In itself the algorithm is already useful, as it results in a smaller solution
+than the simple `every branch instruction is long' used up until now. It also
+results in a smaller solution than the greatest fixed point algorithm that
+{\tt gcc} uses. It does this without sacrificing speed or correctness.
+
This algorithm is part of a greater whole, the CerCo project, which aims to
complete formalise and verify a concrete cost preserving compiler for a large
+completely formalise and verify a concrete cost preserving compiler for a large
subset of the C programming language. More information
on the formalisation of the assembler, of which the present work is a part,
Index: src/ASM/CPP2012policy/proof.tex
===================================================================
 src/ASM/CPP2012policy/proof.tex (revision 2097)
+++ src/ASM/CPP2012policy/proof.tex (revision 2098)
@@ 3,6 +3,4 @@
In this section, we present the correctness proof for the algorithm in more
detail. The main correctness statement is as follows (slightly simplified, here):

\clearpage
\begin{lstlisting}
@@ 114,5 +112,4 @@
\clearpage

\begin{lstlisting}
definition sigma_compact_unsafe :=
@@ 200,5 +197,5 @@
We need to use two different formulations, because the fact that $added$ is 0
does not guarantee that no branch instructions have changed. For instance,
it is possible that we have replaced a short jump with a absolute jump, which
+it is possible that we have replaced a short jump with an absolute jump, which
does not change the size of the branch instruction.
@@ 224,4 +221,5 @@
If an iteration returns {\tt None}, we have the following invariant:
+\clearpage
\begin{lstlisting}
definition nec_plus_ultra :=