--- a/Journal/Paper.thy	Thu May 04 15:21:18 2017 +0100
+++ b/Journal/Paper.thy	Fri May 05 14:26:00 2017 +0100
@@ -1159,10 +1159,24 @@
   then there is nothing to show. So let us assume otherwise. Since the
   @{text "RAG"} is well-founded, we know there exists an ancestor of
   @{text "th"} that is the root of the corrsponding subtree and
-  therefore is ready. Let us call this thread @{text "th'"}. We know
-  that @{text "th'"} has the highest precedence of all ready threads.
-  Therefore it is running.  We have that @{term "th \<noteq> th'"}
-  since we assumed @{text th} is not running.  By
+  therefore is ready (it does not request any resources). Let us call
+  this thread @{text "th'"}.  Since in PIP the @{term "cpreced"}-value
+  of any thread equals the maximum precedence of all threads in its
+  @{term "RAG"}-subtree, and @{text "th"} is in the subtree of @{text
+  "th'"}, the @{term "cpreced"}-value of @{text "th'"} cannot be lower
+  than the precedence of @{text "th"}. But, it can also not be higher,
+  because the precedence of @{text "th"} is the maximum among all
+  threads.  Therefore we know that the @{term "cpreced"}-value of
+  @{text "th'"} is the same as the precedence of @{text "th"}.  The
+  result is that @{text "th'"} must be running. This is because @{term
+  "cpreced"}-value of @{text "th'"} is the highest of all ready
+  threads. This follows from the fact that the @{term "cpreced"}-value
+  of any ready thread is the maximum of the precedences of all threads
+  in its subtrees (with @{text "th"} having the highest of all threads
+  and being in the subtree of @{text "th'"}).  We also have that @{term
+  "th \<noteq> th'"} since we assumed @{text th} is not running.
+
+  By
   Lem.~\ref{notdetached} we have that @{term "\<not>detached s th'"}.
   If @{text "th'"} is not detached in @{text s}, that is either
   holding or waiting for a resource, it must be that @{term "th' \<in>

Binary file journal.pdf has changed