diff -r def87c589516 -r daf75d6ebc89 Journal/Paper.thy
--- a/Journal/Paper.thy	Fri May 12 14:55:35 2017 +0100
+++ b/Journal/Paper.thy	Tue May 16 17:20:49 2017 +0100
@@ -1601,8 +1601,7 @@
   be seen as a \textit{rough(!)} abstraction of the ``runtime
   behaviour'' of threads and also as an abstract notion of
   ``time''---when a new event happened, some time must have passed.
-  In this setting we can prove a more direct bound for the absence of
-  indefinite Priority Inversion. This is what we shall show below.
+
 
   What we will establish in this section is that there can only be a
   finite number of states after state @{term s} in which the thread
@@ -1615,9 +1614,10 @@
   that in our model we can create or exit threads
   arbitrarily. Consequently, the avoidance of indefinite priority
   inversion we are trying to establish is in our model not true,
-  unless we require that the number of threads created is bounded in
-  every valid future state after @{term s}. So our first assumption
-  states:
+  unless we put up an upper bound on the number of threads that
+  have been created upto any valid future state after @{term
+  s}. Otherwise our PIP scheduler could be ``swamped'' with @{text
+  "Create"}-requests.  So our first assumption states:
 
   \begin{quote} {\bf Assumption on the number of threads created in
   every valid state after the state {\boldmath@{text s}}:} Given the
@@ -1629,9 +1629,11 @@
   \end{quote}
 
   \noindent Note that it is not enough to just to state that there are
-  only finite number of threads created in a single state @{text "s' @
-  s"} after @{text s}.  Instead, we need to put this bound on the
-  @{text "Create"} events for all valid states after @{text s}.
+  only finite number of threads created up until a single state @{text
+  "s' @ s"} after @{text s}.  Instead, we need to put this bound on
+  the @{text "Create"} events for all valid states after @{text s}.
+  This ensures that no matter which ``future'' state is reached, the number
+  of creates is finite.
 
   For our second assumption about giving up resources after a finite
   amount of ``time'', let us introduce the following definition about