--- a/Journal/Paper.thy	Thu Mar 16 13:20:46 2017 +0000
+++ b/Journal/Paper.thy	Fri Mar 17 14:57:30 2017 +0000
@@ -1551,47 +1551,52 @@
   programmer assume the responsibility to program threads in such a
   benign manner (in addition to causing no circularity in the
   RAG). This was also the approach taken by Sha et al.~in their paper.
-  However, in this paper we can make an improvement: we can look
-  at the \emph{events} that are happening once a Priority Inversion
+  However, in this paper we can make an improvement: we can look at
+  the \emph{events} that are happening once a Priority Inversion
   occurs. The events can be seen as a rough abstraction of the
   ``runtime behaviour'' of threads and also as an abstract notion of
-  ``time''.  We can then prove a more direct bound for the absence of
-  indefinite Priority Inversion.
+  ``time''---when an event occured, some time must have passed.  We
+  can then 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 amount of states after state @{term s} in which the thread
   @{term th} is blocked. For this to be true, Sha et al.~assume in
   their work that there is a finite pool of threads (active or
   hibernating). However, we do not have this concept of active or
-  hibernating threads in our model, but we can create or exit threads
-  arbitrarily. Consequently, in our model the avoidance of indefinite
-  priority inversion we are trying to establish is not true, unless we
-  require that there number of threads created is bounded in every
-  valid future state after @{term s}. So our first assumption 
-  states
+  hibernating threads in our model. Rather, 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:
 
   \begin{quote} {\bf Assumption on the number of threads created in
   every valid state after the state {\boldmath@{text s}}:} Given the
   state @{text s}, in every ``future'' valid state @{text "t @ s"}, we
   require that the number of created threads is less than
-  @{text "BC"}, that is @{text "len (filter isCreate (t @ s)) <
-  BC"}.  \end{quote}
+  a bound @{text "BC"}, that is 
+
+  \[@{text "len (filter isCreate (t @ s)) < BC"}\;.\]  
+  \end{quote}
 
-  \noindent Note that it is not enough for us to just to state that there
-  are only finite number of threads created in the state @{text "s' @ s"}.  Instead, we
-  need to put a bound on the @{text "Create"} events for all valid 
-  states after @{text s}. 
+  \noindent Note that it is not enough to just to state that there are
+  only finite number of threads created in the state @{text "s' @ s"}.
+  Instead, we need to put a bound on the @{text "Create"} events for
+  all valid states after @{text s}.
 
   For our second assumption about giving up resources after a finite
-  amount of ``time'', let us introduce the following definition:
+  amount of ``time'', let us introduce the following definition about
+  threads that can potentially block @{text th}:
 
   \begin{isabelle}\ \ \ \ \ %%%
   @{thm blockers_def}
   \end{isabelle}
 
-  \noindent This set contains all treads that can potentially block
-  @{text th} after state @{text s}. We need to make the following
-  assumption for the threads in this set:
+  \noindent This set contains all treads that are not detached in
+  state @{text s} (i.e.~have a lock on a resource) and therefore can
+  potentially block @{text th} after state @{text s}. We need to make
+  the following assumption about the threads in this set:
 
   \begin{quote}
   {\bf Assumptions on the threads {\boldmath{@{term "th' \<in> blockers"}}}:} 
@@ -1599,19 +1604,28 @@
   such that for all future 
   valid states @{text "t @ s"},
   we have that if @{term "\<not>(detached (t @ s) th')"}, then 
-  @{text "len(actions_of th' (t @ s)) < BND(th')"}. 
+  \[@{text "len(actions_of th' (t @ s)) < BND(th')"}\] 
   \end{quote} 
 
-  \noindent By this assumption we enforce that any thread blocking
-  @{term th} must become detached (that is hold no resource) after a
-  finite number of events in @{text "t @ s"}. Again we have to require
-  this bound to hold in all valid states after @{text s}. The bound
-  reflects how each thread @{text "th'"} is programmed: Though we cannot
-  express what instructions a thread is executing, the events correspond 
-  to the system calls made by thread. Our @{text "BND(th')"} bounds 
-  the number of these calls.
+  \noindent By this assumption we enforce that any thread potentially
+  blocking @{term th} must become detached (that is lock no resource)
+  after a finite number of events in @{text "t @ s"}. Again we have to
+  require this bound to hold in all valid states after @{text s}. The
+  bound reflects how each thread @{text "th'"} is programmed: Though
+  we cannot express what instructions a thread is executing, the
+  events in our model correspond to the system calls made by thread. Our @{text
+  "BND(th')"} binds the number of these calls.
   
-  The main reason for these two assumptions is that we can prove: 
+  The main reason for these two assumptions is that we can prove: the
+  number of states after @{text s} in which the thread @{text th} is
+  is not running (that is where PI occurs) can be bounded by the
+  number of actions the threads in @{text blockers} perform and how
+  many threads are newly created. This bound can be stated for all
+  valid states @{term "t @ s"} that can happen after @{text s}. To
+  state our bound we use the definition @{term "Postfixes t \<equiv> {p. \<exists> s'. t = s' @ p}"}.
+
+
+To state this we use the 
   
 
   \begin{isabelle}\ \ \ \ \ %%%