--- a/Journal/Paper.thy	Fri Jun 23 00:27:16 2017 +0100
+++ b/Journal/Paper.thy	Tue Jun 27 14:49:42 2017 +0100
@@ -36,8 +36,8 @@
   holding ("holds") and
   waiting_raw ("waits") and
   waiting ("waits") and
-  dependants_raw ("dependants") and
-  dependants ("dependants") and
+  tG_raw ("TDG") and
+  tG ("TDG") and
   RAG_raw ("RAG") and
   RAG ("RAG") and
   Th ("T") and
@@ -459,8 +459,8 @@
   %
   %\begin{isabelle}\ \ \ \ \ %%%
   %\mbox{\begin{tabular}{@ {}l}
-  %@{thm cntP_def}\\
-  %@{thm cntV_def}
+  %@ {thm cntP_def}\\
+  %@ {thm cntV_def}
   %\end{tabular}}
   %\end{isabelle}
   % 
@@ -623,24 +623,26 @@
   finite, we can always start at a thread waiting for a resource and
   ``chase'' outgoing arrows leading to a single root of a tree.
   
-  The use of relations for representing RAGs allows us to conveniently define
-  the notion of the \emph{dependants} of a thread
+  The use of relations for representing @{text RAG}s allows us to conveniently define
+  the \emph{thread dependants graph} 
 
   \begin{isabelle}\ \ \ \ \ %%%
-  @{thm dependants_raw_def}\hfill\numbered{dependants}
+  @{thm tG_raw_def}\\
+  \mbox{}\hfill\numbered{dependants}
   \end{isabelle}
 
-  \noindent This definition needs to account for all threads that wait
-  for a thread to release a resource. This means we need to include
-  threads that transitively wait for a resource to be released (in the
-  picture above this means the dependants of @{text "th\<^sub>0"} are
-  @{text "th\<^sub>1"} and @{text "th\<^sub>2"}, which wait for
-  resource @{text "cs\<^sub>1"}, but also @{text "th\<^sub>3"}, which
-  cannot make any progress unless @{text "th\<^sub>2"} makes progress,
-  which in turn needs to wait for @{text "th\<^sub>0"} to finish). If
-  there is a circle of dependencies in a RAG, then clearly we have a
+  \noindent This definition represents all threads in a @{text RAG} that wait
+  for a thread to release a resource, but the resource is ``hidden''. 
+  In the
+  picture above this means the @{text TDG} connects @{text "th\<^sub>0"} with
+  @{text "th\<^sub>1"} and @{text "th\<^sub>2"}, which both wait for
+  resource @{text "cs\<^sub>1"}; and @{text "th\<^sub>2"} with @{text "th\<^sub>3"}, which
+  cannot make any progress unless @{text "th\<^sub>2"} makes progress. 
+  Similarly for the other threads.
+  If
+  there is a circle of dependencies in a @{text RAG} (and thus @{text TDG}), then clearly we have a
   deadlock. Therefore when a thread requests a resource, we must
-  ensure that the resulting RAG is not circular. In practice, the
+  ensure that the resulting @{text RAG} and @{text TDG} are not circular. In practice, the
   programmer has to ensure this. Our model will enforce that critical 
   resources can only be requested provided no circularity can arise.
 
@@ -648,19 +650,20 @@
   state @{text s}. It is defined as
 
   \begin{isabelle}\ \ \ \ \ %%%
-  @{thm cpreced_def3}\hfill\numbered{cpreced}
+  @{thm cpreced_def}
+  \hfill\numbered{cpreced}
   \end{isabelle}
 
-   \noindent where the dependants of @{text th} are given by the
-  waiting queue function.  While the precedence @{term prec} of any
+   \noindent 
+  While the precedence @{term prec} of any
   thread is determined statically (for example when the thread is
   created), the point of the current precedence is to dynamically
   increase this precedence, if needed according to PIP. Therefore the
   current precedence of @{text th} is given as the maximum of the
   precedence of @{text th} \emph{and} all threads that are dependants
-  of @{text th} in the state @{text s}. Since the notion @{term
-  "dependants"} is defined as the transitive closure of all dependent
-  threads, we deal correctly with the problem in the informal
+  of @{text th} in the state @{text s}. Since the notion of current precedence is defined as the 
+  transitive closure of the dependent
+  threads in the @{text TDG}, 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 "cprecs wq s ths"}.
@@ -781,27 +784,31 @@
 
   Having the scheduler function @{term schs} at our disposal, we can
   ``lift'', or overload, the notions @{term waiting}, @{term holding},
-  @{term RAG}, @{term dependants} and @{term cp} to operate on states
-  only.
+  @{term RAG}, %%@ {term dependants} 
+  and @{term cp} to operate on states only.
 
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}rcl}
   @{thm (lhs) s_holding_abv}  & @{text "\<equiv>"} & @{thm (rhs) s_holding_abv[simplified wq_def]}\\
   @{thm (lhs) s_waiting_abv}  & @{text "\<equiv>"} & @{thm (rhs) s_waiting_abv[simplified wq_def]}\\
   @{thm (lhs) s_RAG_abv}      & @{text "\<equiv>"} & @{thm (rhs) s_RAG_abv[simplified wq_def]}\\
-  @{thm (lhs) s_dependants_abv}& @{text "\<equiv>"} & @{thm (rhs) s_dependants_abv[simplified wq_def]}\\
+  @{thm (lhs) s_tG_abv}& @{text "\<equiv>"} & @{thm (rhs) s_tG_abv[simplified wq_def]}\\
   @{thm (lhs) cp_def}         & @{text "\<equiv>"} & @{thm (rhs) cp_def}\\  
   \end{tabular}
   \end{isabelle}
 
   \noindent
   With these abbreviations in place we can derive for every valid trace @{text s} 
-  the following two facts about  @{term dependants} and @{term cprec} (see \eqref{dependants} 
-  and \eqref{cpreced}): Given @{thm (prem 1) valid_trace.cp_alt_def}, then 
+  the following two facts about  ???????
+  %@ {term dependants} 
+  and @{term cprec} (see \eqref{dependants} 
+  and \eqref{cpreced}): Given ????? %@ {thm (prem 1) valid_trace.cp_alt_def}, 
+  then 
 
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}rcl}
-  @{thm (concl) valid_trace.cp_alt_def3}\\
+  @{thm tG_alt_def}\\
+  @{thm cp_s_def}\\
   \end{tabular}\hfill\numbered{overloaded}
   \end{isabelle}
 
@@ -1839,11 +1846,11 @@
 
   \begin{center}
   @{thm tG_alt_def}\\
-  @{thm dependants_alt_tG} 
+  ???? %@ {thm dependants_alt_tG} 
   \end{center}
 
   \begin{center}
-  @{thm valid_trace.cp_alt_def3} 
+  ???? %@ {thm valid_trace.cp_alt_def3} 
   \end{center}