--- a/Journal/Paper.thy	Fri Jun 09 15:08:54 2017 +0100
+++ b/Journal/Paper.thy	Fri Jun 23 00:27:16 2017 +0100
@@ -47,7 +47,7 @@
   preceds ("precs") and
   cpreced ("cprec") and
   cpreceds ("cprecs") and
-  wq_fun ("wq") and
+  (*wq_fun ("wq") and*)
   cp ("cprec") and
   (*cprec_fun ("cp_fun") and*)
   holdents ("resources") and
@@ -627,7 +627,7 @@
   the notion of the \emph{dependants} of a thread
 
   \begin{isabelle}\ \ \ \ \ %%%
-  @{thm dependants_raw_def}
+  @{thm dependants_raw_def}\hfill\numbered{dependants}
   \end{isabelle}
 
   \noindent This definition needs to account for all threads that wait
@@ -651,13 +651,7 @@
   @{thm cpreced_def3}\hfill\numbered{cpreced}
   \end{isabelle}
 
-  %\endnote{
-  %\begin{isabelle}\ \ \ \ \ %%%
-  %@ {thm cp_alt_def cp_alt_def1}
-  %\end{isabelle}
-  %}
-
-  \noindent where the dependants of @{text th} are given by the
+   \noindent where the dependants of @{text th} are given by the
   waiting queue function.  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
@@ -792,16 +786,27 @@
 
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}rcl}
-  @{thm (lhs) s_holding_abv}  & @{text "\<equiv>"} & @{thm (rhs) s_holding_abv}\\
-  @{thm (lhs) s_waiting_abv}  & @{text "\<equiv>"} & @{thm (rhs) s_waiting_abv}\\
-  @{thm (lhs) s_RAG_abv}      & @{text "\<equiv>"} & @{thm (rhs) s_RAG_abv}\\
-  @{thm (lhs) s_dependants_abv}& @{text "\<equiv>"} & @{thm (rhs) s_dependants_abv}\\
+  @{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) cp_def}         & @{text "\<equiv>"} & @{thm (rhs) cp_def}\\  
   \end{tabular}
   \end{isabelle}
 
   \noindent
-  With these abbreviations in place we can introduce 
+  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 
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  \begin{tabular}{@ {}rcl}
+  @{thm (concl) valid_trace.cp_alt_def3}\\
+  \end{tabular}\hfill\numbered{overloaded}
+  \end{isabelle}
+
+
+  can introduce 
   the notion of a thread being @{term ready} in a state (i.e.~threads
   that do not wait for any resource, which are the roots of the trees 
   in the RAG, see Figure~\ref{RAGgraph}). The @{term running} thread
@@ -1042,7 +1047,7 @@
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{l}
   @{term "th \<in> threads s"}\\
-  @{term "prec th s = Max (cprecs s (threads s))"}\\
+  @{term "prec th s = Max (precs s (threads s))"}\\
   @{term "prec th s = (prio, DUMMY)"}
   \end{tabular}
   \end{isabelle}
@@ -1832,10 +1837,20 @@
   @{text th} in the @{term RAG} (and waiting for @{text th} to release
   a resource). We can prove the following lemma.
 
+  \begin{center}
+  @{thm tG_alt_def}\\
+  @{thm dependants_alt_tG} 
+  \end{center}
+
+  \begin{center}
+  @{thm valid_trace.cp_alt_def3} 
+  \end{center}
+
+
   \begin{lemma}\label{childrenlem}
   HERE %@ {text "If"} @ {thm (prem 1) cp_rec} @{text "then"}
   \begin{center}
-  @{thm valid_trace.cp_rec}.
+  @{thm valid_trace.cp_rec_tG}.
   %@ {thm (concl) cp_rec}.
   \end{center}
   \end{lemma}