--- a/Journal/Paper.thy	Tue Aug 16 11:49:37 2016 +0100
+++ b/Journal/Paper.thy	Wed Aug 24 16:13:20 2016 +0200
@@ -873,6 +873,55 @@
   properties that show our model of PIP is correct.
 *}
 
+section {* Preliminaries *}
+
+(*<*)
+context valid_trace
+begin
+(*>*)
+text {*
+
+  In this section we prove facts that immediately follow from
+  our definitions of valid traces.
+
+  \begin{lemma}??\label{precedunique}
+  @{thm [mode=IfThen] preced_unique[where ?th1.0=th\<^sub>1 and ?th2.0=th\<^sub>2]} 
+  \end{lemma}
+
+
+  We can verify that in any valid state, there can only be at most
+  one running thread---if there are more than one running thread,
+  say @{text "th\<^sub>1"} and @{text "th\<^sub>2"}, they must be 
+  equal.
+
+  \begin{lemma}
+  @{thm [mode=IfThen] running_unique[where ?th1.0=th\<^sub>1 and ?th2.0=th\<^sub>2]} 
+  \end{lemma}
+  
+  \begin{proof}
+  Since @{text "th\<^sub>1"} and @{text "th\<^sub>2"} are running, they must be
+  roots in the RAG.
+  According to XXX, there exists a chain in the RAG-subtree of @{text "th\<^sub>1"}, 
+  say starting from @{text "th'\<^sub>1"}, such that @{text "th'\<^sub>1"} has the 
+  highest precedence in this subtree (@{text "th\<^sub>1"} inherited
+  the precedence of @{text "th'\<^sub>1"}). We have a similar chain starting from, say 
+  @{text "th'\<^sub>2"}, in the RAG-subtree of @{text "th\<^sub>2"}. Since @{text "th\<^sub>1"}
+  and @{text "th\<^sub>2"} are running we know their cp-value must be the same, that is
+  \begin{center}
+  @{term "cp s th\<^sub>1 = cp s th\<^sub>2"} 
+  \end{center}
+  
+  \noindent
+  That means the precedences of @{text "th'\<^sub>1"} and @{text "th'\<^sub>2"}
+  must be the same (they are the maxima in the respective RAG-subtrees). From this we can
+  infer by Lemma~\ref{precedunique} that @{text "th'\<^sub>1"}
+  and @{text "th'\<^sub>2"} are the same threads. However, this also means the
+  roots @{text "th\<^sub>1"} and @{text "th\<^sub>2"} must be the same.\qed
+  \end{proof}
+
+  *}
+(*<*)end(*>*)
+
 section {* The Correctness Proof *}
 
 (*<*)