--- a/Journal/Paper.thy	Tue May 02 14:42:52 2017 +0100
+++ b/Journal/Paper.thy	Thu May 04 15:21:18 2017 +0100
@@ -46,8 +46,10 @@
   preced ("prec") and
   preceds ("precs") and
   cpreced ("cprec") and
+  cpreceds ("cprecs") and
   wq_fun ("wq") and
-  cprec_fun ("cp'_fun") and
+  cp ("cprec") and
+  (*cprec_fun ("cp_fun") and*)
   holdents ("resources") and
   DUMMY  ("\<^raw:\mbox{$\_\!\_$}>") and
   cntP ("c\<^bsub>P\<^esub>") and
@@ -667,7 +669,7 @@
   threads, we deal correctly with the problem in the informal
   algorithm by Sha et al.~\cite{Sha90} where a priority of a thread is
   lowered prematurely (see Introduction). We again introduce an abbreviation for current
-  precedeces of a set of threads, written @{text "cpreceds wq s ths"}.
+  precedeces of a set of threads, written @{text "cprecs wq s ths"}.
   
   \begin{isabelle}\ \ \ \ \ %%%
   @{thm cpreceds_def}
@@ -1085,11 +1087,10 @@
   the highest precedence in the state @{text s}, is either running in
   state @{term "s' @ s"}, or can only be blocked in the state @{text
   "s' @ s"} by a thread @{text th'} that already existed in @{text s}
-  and requested a resource or had a lock on at least one resource---that means
+  and is waiting for a resource or had a lock on at least one resource---that means
   the thread was not \emph{detached} in @{text s}.  As we shall see
   shortly, that means there are only finitely many threads that can
-  block @{text th} in this way and then they need to run with the same
-  precedence as @{text th}.
+  block @{text th} in this way.
 
   
 %% HERE
@@ -1115,7 +1116,7 @@
   that is
 
   \begin{center}
-  @{term "cp (t @ s) th' = Max (cp (t @ s) ` treads (t @ s))"}
+  @{term "cp (t @ s) th' = Max (cp (t @ s) ` threads (t @ s))"}
   \end{center}
 
   \noindent
@@ -1143,13 +1144,14 @@
   @{text "s"}, then, according to the definition of detached, @{text
   "th’"} does not hold or wait for any resource. Hence the @{text
   cp}-value of @{text "th'"} in @{text s} is not boosted, that is
-  @{term "cp s th' = prec th s"}, and is therefore lower than the
+  @{term "cp s th' = prec th' s"}, and is therefore lower than the
   precedence (as well as the @{text "cp"}-value) of @{term "th"}. This
-  means @{text "th'"} will not run as long as @{text "th"} is a
-  live thread. In turn this means @{text "th'"} cannot acquire a reseource
-  and is still detached in state @{text "s' @ s"}.  Consequently
-  @{text "th'"} is also not boosted in state @{text "s' @ s"} and
-  would not run. This contradicts our assumption.\qed
+  means @{text "th'"} will not run as long as @{text "th"} is a live
+  thread. In turn this means @{text "th'"} cannot take any action in
+  state @{text "s' @ s"} to change its current status; therefore
+  @{text "th'"} is still detached in state @{text "s' @ s"}.
+  Consequently @{text "th'"} is also not boosted in state @{text "s' @
+  s"} and would not run. This contradicts our assumption.\qed
   \end{proof}
 
 
@@ -1176,85 +1178,87 @@
 
 
   %\endnote{
-  %In what follows we will describe properties of PIP that allow us to
-  %prove Theorem~\ref{mainthm} and, when instructive, briefly describe
-  %our argument. Recall we want to prove that in state @ {term "s' @ s"}
-  %either @{term th} is either running or blocked by a thread @ {term
-  %"th'"} (@{term "th \<noteq> th'"}) which was alive in state @{term s}. We
-  %can show that
+  
+In what follows we will describe properties of PIP that allow us to
+  prove Theorem~\ref{mainthm} and, when instructive, briefly describe
+  our argument. Recall we want to prove that in state @ {term "s' @ s"} 
+either @{term th} is either running or blocked by a thread @
+  {term "th'"} (@{term "th \<noteq> th'"}) which was alive in state
+  @{term s}. We can show that
 
 
-  %\begin{lemma}
-  %If @{thm (prem 2) eq_pv_blocked}
-  %then @{thm (concl) eq_pv_blocked}
-  %\end{lemma}
+  \begin{lemma}
+  If @{thm (prem 2) eq_pv_blocked}
+  then @{thm (concl) eq_pv_blocked}
+  \end{lemma}
 
-  %\begin{lemma}
-  %If @{thm (prem 2) eq_pv_persist}
-  %then @{thm (concl) eq_pv_persist}
-  %\end{lemma}}
+  \begin{lemma}
+  If @{thm (prem 2) eq_pv_persist}
+  then @{thm (concl) eq_pv_persist}
+  \end{lemma}
+  %%%}
 
 %  \endnote{{\bf OUTLINE}
 
-%  Since @{term "th"} is the most urgent thread, if it is somehow
-%  blocked, people want to know why and wether this blocking is
-%  reasonable.
+  Since @{term "th"} is the most urgent thread, if it is somehow
+  blocked, people want to know why and wether this blocking is
+  reasonable.
 
-%  @{thm [source] th_blockedE} @{thm th_blockedE}
+  @{thm [source] th_blockedE} @{thm th_blockedE}
 
-%  if @{term "th"} is blocked, then there is a path leading from 
-%  @{term "th"} to @{term "th'"}, which means:
-%  there is a chain of demand leading from @{term th} to @{term th'}.
+  if @{term "th"} is blocked, then there is a path leading from 
+  @{term "th"} to @{term "th'"}, which means:
+  there is a chain of demand leading from @{term th} to @{term th'}.
 
-  %%% in other words
-  %%% th -> cs1 -> th1 -> cs2 -> th2 -> ... -> csn -> thn -> cs -> th'. 
-  %%% 
-  %%% We says that th is blocked by "th'".
+   in other words
+   th -> cs1 -> th1 -> cs2 -> th2 -> ... -> csn -> thn -> cs -> th'. 
+   
+   We says that th is blocked by @{text "th'"}.
 
-%  THEN
+  THEN
 
-%  @ {thm [source] vat_t.th_chain_to_ready} @ {thm vat_t.th_chain_to_ready}
+  @{thm [source] vat_t.th_chain_to_ready} @{thm vat_t.th_chain_to_ready}
 
-%  It is basic propery with non-trival proof. 
+  It is basic propery with non-trival proof. 
 
-%  THEN
+  THEN
 
-%  @ {thm [source] max_preced} @ {thm max_preced}
+  @{thm [source] max_preced} @{thm max_preced}
 
-%  which says @{term "th"} holds the max precedence.
+  which says @{term "th"} holds the max precedence.
 
-%  THEN
+  THEN
  
-%  @ {thm [source] th_cp_max th_cp_preced th_kept}
-%  @ {thm th_cp_max th_cp_preced th_kept}
+  @{thm [source] th_cp_max th_cp_preced th_kept}
+  @{thm th_cp_max th_cp_preced th_kept}
 
-%  THENTHEN
+  THEN
 
- %@ {thm [source] running_inversion_4} @  {thm running_inversion_4}
+ ??? %%@ {thm [source] running_inversion_4} @  {thm running_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.
- % To see what kind of thread can block @{term th}.
+ 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.
+ To see what kind of thread can block @{term th}.
 
- % From these two lemmas we can see the correctness of PIP, which is
- % that: the blockage of th is reasonable and under control.
+  From these two lemmas we can see the correctness of PIP, which is
+  that: the blockage of th is reasonable and under control.
 
- % Lemmas we want to describe:
+  Lemmas we want to describe:
 
- % \begin{lemma}
- % @ {thm running_cntP_cntV_inv}
- % \end{lemma}
+  \begin{lemma}
+  @{thm running_cntP_cntV_inv}
+  \end{lemma}
 
-%  \noindent
-%  Remember we do not have the well-nestedness restriction in our
-%  proof, which means the difference between the counters @{const cntV}
-%  and @{const cntP} can be larger than @{term 1}.
+  \noindent
+  Remember we do not have the well-nestedness restriction in our
+  proof, which means the difference between the counters @{const cntV}
+  and @{const cntP} can be larger than @{term 1}.
 
-%  \begin{lemma}\label{runninginversion}
-%  @ {thm running_inversion}
-%  \end{lemma}
+  \begin{lemma}\label{runninginversion}
+  @{thm running_inversion}
+  \end{lemma}
   
-%  explain tRAG
+  explain tRAG
 %}
 
   

Binary file journal.pdf has changed