876 section {* Preliminaries *}

   877 

   878 (*<*)

   879 context valid_trace

   880 begin

   881 (*>*)

   882 text {*

   883 

   884   In this section we prove facts that immediately follow from

   885   our definitions of valid traces.

   886 

   887   \begin{lemma}??\label{precedunique}

   888   @{thm [mode=IfThen] preced_unique[where ?th1.0=th\<^sub>1 and ?th2.0=th\<^sub>2]} 

   889   \end{lemma}

   890 

   891 

   892   We can verify that in any valid state, there can only be at most

   893   one running thread---if there are more than one running thread,

   894   say @{text "th\<^sub>1"} and @{text "th\<^sub>2"}, they must be 

   895   equal.

   896 

   897   \begin{lemma}

   898   @{thm [mode=IfThen] running_unique[where ?th1.0=th\<^sub>1 and ?th2.0=th\<^sub>2]} 

   899   \end{lemma}

   900   

   901   \begin{proof}

   902   Since @{text "th\<^sub>1"} and @{text "th\<^sub>2"} are running, they must be

   903   roots in the RAG.

   904   According to XXX, there exists a chain in the RAG-subtree of @{text "th\<^sub>1"}, 

   905   say starting from @{text "th'\<^sub>1"}, such that @{text "th'\<^sub>1"} has the 

   906   highest precedence in this subtree (@{text "th\<^sub>1"} inherited

   907   the precedence of @{text "th'\<^sub>1"}). We have a similar chain starting from, say 

   908   @{text "th'\<^sub>2"}, in the RAG-subtree of @{text "th\<^sub>2"}. Since @{text "th\<^sub>1"}

   909   and @{text "th\<^sub>2"} are running we know their cp-value must be the same, that is

   910   \begin{center}

   911   @{term "cp s th\<^sub>1 = cp s th\<^sub>2"} 

   912   \end{center}

   913   

   914   \noindent

   915   That means the precedences of @{text "th'\<^sub>1"} and @{text "th'\<^sub>2"}

   916   must be the same (they are the maxima in the respective RAG-subtrees). From this we can

   917   infer by Lemma~\ref{precedunique} that @{text "th'\<^sub>1"}

   918   and @{text "th'\<^sub>2"} are the same threads. However, this also means the

   919   roots @{text "th\<^sub>1"} and @{text "th\<^sub>2"} must be the same.\qed

   920   \end{proof}

   921 

   922   *}

   923 (*<*)end(*>*)

   924