--- a/Journal/Paper.thy	Fri Apr 15 14:44:09 2016 +0100
+++ b/Journal/Paper.thy	Thu Jun 02 13:15:03 2016 +0100
@@ -1002,15 +1002,47 @@
   proof, which means the difference between the counters @{const cntV}
   and @{const cntP} can be larger than @{term 1}.
 
-  \begin{lemma}
+  \begin{lemma}\label{runninginversion}
   @{thm runing_inversion}
   \end{lemma}
   
+  explain tRAG
+  \bigskip
+
+
+  Suppose the thread @{term th} is \emph{not} running in state @{term
+  "t @ s"}, meaning that it should be blocked by some other thread.
+  It is first shown that there is a path in the RAG leading from node
+  @{term th} to another thread @{text "th'"}, which is also in the
+  @{term readys}-set.  Since @{term readys}-set is non-empty, there
+  must be one in it which holds the highest @{term cp}-value, which,
+  by definition, is currently the @{term running}-thread.  However, we
+  are going to show in the next lemma slightly more: this running
+  thread is exactly @{term "th'"}.
 
   \begin{lemma}
-  @{thm th_blockedE}
+  If @{thm (prem 1) th_blockedE_pretty} then
+  @{thm (concl) th_blockedE_pretty}.
   \end{lemma}
 
+  \begin{proof}
+  %Let me distinguish between cp (current precedence) and assigned precedence (the precedence the
+  %thread ``normally'' has).
+  %So we want to show what the cp of th' is in state t @ s.
+  %We look at all the assingned precedences in the subgraph starting from th'
+  %We are looking for the maximum of these assigned precedences.
+  %This subgraph must contain the thread th, which actually has the highest precednence
+  %so cp of th' in t @ s has this (assigned) precedence of th
+  %We know that cp (t @ s) th' 
+  %is the Maximum of the threads in the subgraph starting from th'
+  %this happens to be the precedence of th
+  %th has the highest precedence of all threads
+  \end{proof}
+
+  \begin{corollary}  
+  Using the lemma \ref{runninginversion} we can say more about the thread th'
+  \end{corollary}
+
   \subsection*{END OUTLINE}