diff -r 42767f6e0ae9 -r 4e0bc10f7907 Journal/Paper.thy
--- a/Journal/Paper.thy	Fri Jul 07 15:10:14 2017 +0100
+++ b/Journal/Paper.thy	Tue Jul 11 17:01:50 2017 +0100
@@ -1975,7 +1975,7 @@
   \end{isabelle}
   
   \noindent
-  which shows how the @{text RAG} needs to be changed. The next lemma suggests
+  which shows how the @{text RAG} needs to be changed. The next lemmas suggest
   how the current precedences need to be recalculated. For threads that are
   not @{text "th"} and @{text "th'"} nothing needs to be changed, since we
   can show
@@ -1984,17 +1984,33 @@
   @{text "If"} @{text "th'' \<noteq> th"} and 
   @{text "th'' \<noteq> th'"}
   @{thm (concl) valid_trace_v_n.cp_kept[where ?th1.0="th''"]}
+  \hfill\numbered{fone}
   \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. 
+  However, neither @{text "th"} and @{text "th'"} is element of the 
+  respective children, which is shown by the following two facts:
 
-  
+
   \begin{isabelle}\ \ \ \ \ %%%
-  @{thm (concl) valid_trace_v_n.t1}\\
-  @{thm (concl) valid_trace_v_n.t2}
+  \begin{tabular}{@ {}l}
+  @{term "th' \<notin> children (TDG (e#s)) th"}\\
+  @{term "th \<notin> children (TDG (e#s)) th'"}
+  \end{tabular}\hfill{}\numbered{ftwo}
   \end{isabelle}
+  
+  \noindent
+  This means the recalculation of the @{text cprec} of @{text "th"} and 
+  @{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.
+
 *}
 
 text {*