Index: Deliverables/D1.2/CompilerProofOutline/outline.tex
===================================================================
--- Deliverables/D1.2/CompilerProofOutline/outline.tex (revision 1800)
+++ Deliverables/D1.2/CompilerProofOutline/outline.tex (revision 1801)
@@ -1039,5 +1039,7 @@
It is easy to see that this linearisation process eventually terminates.
-In particular, the size of the visited label set is monotonically increasing, and is bounded above by the size of the graph that we are linearising.
+In particular, the size of the visited label set is non decreasing and bounded above by the size of the graph that we are linearising. Moreover when it remains the same we are
+decreasing the size of the todo list. So the lexicographic measure $(n - |\mathtt{visited}|, |\mathtt{todo}|)$ (where $n$ is the number of nodes in the graph) strictly decreases upon each
+call\footnote{The use of a lexicographic measure can be avoided by taking the first element in $\mathtt{todo}$ not in $\mathtt{visited}$ and discarding all preceding nodes before making the recursive call.}.
The initial call to \texttt{linearise} sees the \texttt{visited}, \texttt{required} and \texttt{generated} sets set to the empty set, and \texttt{todo} initialized with the singleton list consisting of the entry point of the graph.
@@ -1050,7 +1052,7 @@
$\forall \mathtt{l} \in \mathtt{generated}.\ \mathtt{succ(l,\ graph)} \subseteq \mathtt{required} \cup \mathtt{todo}$,
\item
-$\mathtt{required} \subseteq \mathtt{visited}$,
-\item
-$\mathtt{visited} \cap \mathtt{todo} = \emptyset$.
+$\mathtt{required} \subseteq \mathtt{visited}$.
+% \item
+% $\mathtt{visited} \cap \mathtt{todo} = \emptyset$.
\end{enumerate}