--- a/Journal/Paper.thy	Wed Jan 13 13:20:45 2016 +0000
+++ b/Journal/Paper.thy	Wed Jan 13 14:20:58 2016 +0000
@@ -890,10 +890,10 @@
   programs that contain for every looking request also a corresponding
   unlocking request for a resource. Second, we would need to specify a
   kind of global clock that tracks the time how long a thread locks a
-  resource. But this seems difficult, because how do we conveninet
+  resource. But this seems difficult, because how do we conveniently
   distinguish between a thread that ``just'' lock a resource for a
   very long time and one that locks it forever.  Therefore we decided
-  to leave it out this property and let the programmer assume the
+  to leave out this property and let the programmer assume the
   responsibility to program threads in such a benign manner (in
   addition to causing no circularity in the RAG). In this detail, we
   do not make any progress in comparison with the work by Sha et al.
@@ -936,7 +936,7 @@
 
   THENTHEN
 
-  @{thm [source] runing_inversion_4} @{thm runing_inversion_4}
+  (here) %@ {thm [source] runing_inversion_4} @  {thm runing_inversion_4}
 
   which explains what the @{term "th'"} looks like. Now, we have found the 
   @{term "th'"} which blocks @{term th}, we need to know more about it.
@@ -1166,6 +1166,20 @@
   %if every such thread can release all its resources in finite duration, then after finite
   %duration, none of them may block @{term "th"} anymore. So, no priority inversion may happen
   %then.
+
+  NOTE: about bounds in sha et al and ours:
+
+  There are low priority threads, 
+  which do not hold any resources, 
+  such thread will not block th. 
+  Their Theorem 3 does not exclude such threads.
+
+  There are resources, which are not held by any low prioirty threads,
+  such resources can not cause blockage of th neither. And similiary, 
+  theorem 6 does not exlude them.
+
+  Our one bound excudle them by using a different formaulation. "
+
   *}
 (*<*)
 end