--- a/Journal/Paper.thy	Fri Jul 14 15:08:39 2017 +0100
+++ b/Journal/Paper.thy	Tue Jul 18 14:46:14 2017 +0100
@@ -2012,10 +2012,8 @@
   @{text "th'"} can be done independently and also done locally by only 
   looking at the children: according to \eqref{fone} and \eqref{ftwo} 
   none of the @{text cprecs} of the children 
-  changes, just the children-sets changes by a @{text V}-event. This 
-  in turn means the recalculation of 
-  @{text cprec} for @{text th} and @{text "th'"} terminates since
-  none of the  @{text cprec} need the be recalculated.
+  changes, just the children-sets changes by a @{text V}-event. 
+  
 
 *}
 
@@ -2024,12 +2022,12 @@
   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.
+  to be recalculated for any thread @{text "th''"}.
 
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
   @{thm (concl) valid_trace_v_e.RAG_s}\\
-  @{thm (concl) valid_trace_v_e.eq_cp}
+  @{term "\<forall>th''. cprec (e#s) th'' = cprec s th''"}
   \end{tabular}
   \end{isabelle}
   *}
@@ -2045,14 +2043,19 @@
   
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
-  @{thm valid_trace_p_h.RAG_es}\\
-  %@ { thm valid_trace_p_h.eq_cp}
+  @{thm (concl) valid_trace_p_h.RAG_es}\\
+  @{term "\<forall>th''. cprec (e#s) th'' = cprec s th''"}
   \end{tabular}
   \end{isabelle}
 
-  \noindent
-  This means we need to add a holding edge to the @{text RAG} and no
-  current precedence needs to be recalculated.*} 
+  \noindent This means we need to add a holding edge to the @{text
+  RAG}. However, note while the @{text RAG} changes the corresponding
+  @{text TDG} does not change. Together with the fact that the
+  precedences of all threads are unchanged, no @{text cprec} value is
+  changed. Therefore, no recalucation of the @{text cprec} value 
+  of any thread @{text "th''"} is needed.
+
+*} 
 
 text {*
   \noindent
@@ -2060,8 +2063,8 @@
   
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
-  %@ {thm RAG_s}\\
-  HERE %@ {thm[mode=IfThen] eq_cp}
+  %@ {thm (concl) valid_trace_p_hRAG_s}\\
+  %@ {thm (concl) valid_trace_p_h.eq_cp}
   \end{tabular}
   \end{isabelle}