Index: /Deliverables/D1.2/CompilerProofOutline/outline.tex
===================================================================
 /Deliverables/D1.2/CompilerProofOutline/outline.tex (revision 1787)
+++ /Deliverables/D1.2/CompilerProofOutline/outline.tex (revision 1788)
@@ 879,5 +879,6 @@
Given $LA:\mathtt{label}\to\mathtt{lattice}$ (where $\mathtt{lattice}$
is the type of sets of registers\footnote{More precisely, it is the lattice
of pairs of sets of pseudoregisters and sets of hardware registers,
+$\mathtt{set}(\mathtt{register})\times
+\mathtt{set}(\mathtt{hdwregister})$,
with pointwise operations.}), we also have have the following
predicates:
@@ 933,6 +934,6 @@
$$x\sim y \at \ell$$
to state that registers $x$ and $y$ are similar at $\ell$. The formal definition
will be given next, but intuitively it means that those two registers \emph{must}
have the same value at $\ell$. The analysis that produces this information can be
+of this relation's property will be given next, but intuitively it means that those two registers \emph{must}
+have the same value after $\ell$. The analysis that produces this information can be
coarse: in our case, we just set two different registers to be similar at $\ell$
if at $\ell$ itself there is a move instruction between the two.
@@ 959,7 +960,10 @@
\end{itemize}
The overall effect is that if $T$ is an LTL state with $\ell(T)=\ell$
then we will have $T\to^+T'$ where $T'(\Colour(r_1))=T(\Colour(r_2))+T(\Colour(r_2))$.

We skip over the details of correctly dealing with the stack and its size.
+then we will have $T\to^+T'$ where $T'(\Colour(r_1))=T(\Colour(r_2))+T(\Colour(r_2))$,
+while $T'(y)=T(y)$ for any $y$ \emph{in the image of $\Colour$} different from
+$\Colour(r_1)$. Some hardware registers that are used for bookkeeping and which
+are explicitly excluded from colouring may have different values.
+
+We skip the details of correctly dealing with the stack and its size.
\subsubsection{The relation between ERTL and LTL states}
Given a state $S$ in ERTL, we abuse the notation by using $S$ as the underlying map