--- a/Journal/Paper.thy	Mon Jul 03 15:29:29 2017 +0100
+++ b/Journal/Paper.thy	Fri Jul 07 15:10:14 2017 +0100
@@ -1960,8 +1960,9 @@
 
 text {*
   \noindent
-  \colorbox{mygrey}{@{term "V th cs"}:} We assume that @{text s'} and 
-  @{term "s \<equiv> V th cs#s'"} are both valid. We have to consider two
+  \colorbox{mygrey}{@{term "V th cs"}:} We assume that @{text s} and 
+  @{term "e#s"} with @{text e} being @{term "V th cs"} are both valid. 
+  We have to consider two
   subcases: one where there is a thread to ``take over'' the released
   resource @{text cs}, and one where there is not. Let us consider them
   in turn. Suppose in state @{text s}, the thread @{text th'} takes over
@@ -1969,8 +1970,8 @@
 
 
   \begin{isabelle}\ \ \ \ \ %%%
-  @{thm (concl) valid_trace_v_n.RAG_s}\\
-  %@ {thm RAG_s}
+  %@ { thm (concl) valid_trace_v_n.RAG_s}\\
+  @{term "RAG (e#s) = RAG s - {(C cs,T th), (T th',C cs)} \<union> {(C cs, T th')}"}
   \end{isabelle}
   
   \noindent
@@ -1980,38 +1981,50 @@
   can show
 
   \begin{isabelle}\ \ \ \ \ %%%
-  %@ {thm[mode=IfThen] cp_kept}
+  @{text "If"} @{text "th'' \<noteq> th"} and 
+  @{text "th'' \<noteq> th'"}
+  @{thm (concl) valid_trace_v_n.cp_kept[where ?th1.0="th''"]}
   \end{isabelle}
   
   \noindent
   For @{text th} and @{text th'} we need to use Lemma~\ref{childrenlem} to
-  recalculate their current precedence since their children have changed. *}
+  recalculate their current precedence since their children have changed. 
+
+  
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{thm (concl) valid_trace_v_n.t1}\\
+  @{thm (concl) valid_trace_v_n.t2}
+  \end{isabelle}
+*}
 
 text {*
   \noindent
-  In the other case where there is no thread that takes over @{text cs}, we can show how
+  In the other case where there is no thread that takes over @{text cs}, 
+  we can show how
   to recalculate the @{text RAG} and also show that no current precedence needs
   to be recalculated.
 
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
-  %@ {thm RAG_s}\\
-  %@ {thm eq_cp}
+  @{thm (concl) valid_trace_v_e.RAG_s}\\
+  @{thm (concl) valid_trace_v_e.eq_cp}
   \end{tabular}
   \end{isabelle}
   *}
 
 text {*
   \noindent
-  \colorbox{mygrey}{@{term "P th cs"}:} We assume that @{text s'} and 
-  @{term "s \<equiv> P th cs#s'"} are both valid. We again have to analyse two subcases, namely
-  the one where @{text cs} is not locked, and one where it is. We treat the former case
+  \colorbox{mygrey}{@{term "P th cs"}:} We assume that @{text s} and 
+  @{term "e#s"} with @{term "e \<equiv> P th cs"} are both valid. 
+  We again have to analyse two subcases, namely
+  the one where @{text cs} is not locked, and one where it is. We 
+  treat the former case
   first by showing that
   
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
-  %@ {thm RAG_s}\\
-  HERE %@ {thm eq_cp}
+  @{thm valid_trace_p_h.RAG_es}\\
+  %@ { thm valid_trace_p_h.eq_cp}
   \end{tabular}
   \end{isabelle}