# Changeset 1801 for Deliverables/D1.2

Ignore:
Timestamp:
Mar 2, 2012, 3:16:23 PM (9 years ago)
Message:

small correction

File:
1 edited

### Legend:

Unmodified
 r1797 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. $\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}