--- a/Journal/Paper.thy	Tue Jul 11 17:01:50 2017 +0100
+++ b/Journal/Paper.thy	Fri Jul 14 15:08:39 2017 +0100
@@ -1832,8 +1832,8 @@
   of @{term children} of a thread @{text th} (defined in \eqref{children})
   where a child is a thread that is only one ``hop'' away from the thread
   @{text th} in the @{term TDG} (and waiting for @{text th} to release
-  a resource). Using children, we can prove the following lemma for calculating
-  @{text cprec}.
+  a resource). Using children, we can prove the following lemma for more efficiently calculating
+  @{text cprec} of a thread @{text th}.
 
 
   \begin{lemma}\label{childrenlem}
@@ -1845,13 +1845,19 @@
   
   \noindent
   That means the current precedence of a thread @{text th} can be
-  computed locally by considering only the static precedence of @{text th}
+  computed by considering the static precedence of @{text th}
   and 
-  the current precedences of the children of @{text th}. In
-  effect, it only needs to be recomputed for @{text th} when its static
-  precedence is re-set or when one of
-  its children changes its current precedence.  This is much more efficient 
-  because when the  @{text cprec}-value is not changed for a child, 
+  the current precedences of the children of @{text th}. Their 
+  @{text "cprec"}s, in general general, need to be computed by recursively decending into 
+  deeper ``levels'' of the @{text TDG}. 
+  However, the current precedence of a thread @{text th}, say, 
+  only needs to be recomputed when @{text "(i)"} its static
+  precedence is re-set or when @{text "(ii)"} one of
+  its children changes its current precedence or when @{text "(iii)"} the children set changes
+  (for example in an @{text "V"}-event).   
+  If only the static precedence or the children-set changes, the we can 
+  avoid the recursion and compute the @{text cprec} of @{text th} locally.
+  In this cases
   the recursion does not need to decend into the corresponding subtree.
   Once the current 
   precedence is computed in this more efficient manner, the selection

Binary file journal.pdf has changed