--- a/Journal/Paper.thy	Sun Oct 02 14:32:05 2016 +0100
+++ b/Journal/Paper.thy	Fri Oct 07 14:05:08 2016 +0100
@@ -1070,13 +1070,61 @@
   However, we are able to combine their two separate bounds into a
   single theorem improving their bound.
 
+%% HERE
+
+  Given our assumptions (on @{text th}), the first property we can
+  show is that any running thread, say @{text "th'"}, has the same
+  precedence of @{text th}:
+
+  \begin{lemma}\label{runningpreced}
+  @{thm [mode=IfThen] running_preced_inversion}
+  \end{lemma}
+
+  \begin{proof}
+  By definition the running thread has as precedence the maximum of
+  all ready threads, that is
+
+  \begin{center}
+  @{term "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))"}
+  \end{center}
+  \end{proof}
+
+  @{thm "th_blockedE_pretty"} -- thm-blockedE??
+  
+
   @{text "th_kept"} shows that th is a thread in s'-s
 
+
+
+
   \begin{proof}[of Theorem 1]
   If @{term "th \<in> running (s' @ s)"}, then there is nothing to show. So let us
-  assume otherwise. 
+  assume otherwise. By Lem.~\ref{thblockedE} we know there exists a thread
+  @{text "th'"} that is an acestor of @{text th} in the @{text "RAG"}
+  and @{text "th'"} is running, that is we know
+
+  \begin{center}
+  @{term "th' \<in> nancestors (tG (s' @ s)) th"} \quad and \quad
+  @{term "th' \<in> running (s' @ s)"}
+  \end{center}
+
+  \noindent We have that @{term "th \<noteq> th'"} since we assumed
+  @{text th} is not running.  By Lem.~\ref{thkept}, we know that
+  @{text "th'"} is also running in state @{text s} and by
+  Lem.~\ref{detached} that @{term "\<not>detached s th'"}.
+  By Lem.~\ref{runningpreced} we have
+
+  \begin{center}
+  @{term "cp (t @ s) th' = preced th s"}
+  \end{center}
+
+  \noindent
+  This concludes the proof of Theorem 1.
   \end{proof}
 
+
+
+
   In what follows we will describe properties of PIP that allow us to
   prove Theorem~\ref{mainthm} and, when instructive, briefly describe
   our argument. Recall we want to prove that in state @{term "s' @ s"}
@@ -1161,7 +1209,7 @@
   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
@@ -1173,7 +1221,7 @@
   thread is exactly @{term "th'"}.
 
   \begin{lemma}
-  If @{thm (prem 1) th_blockedE_pretty} then there exists a thread @{text "th'"}
+  There exists a thread @{text "th'"}
   such that @{thm (no_quants) th_blockedE_pretty}.
   \end{lemma}