--- a/Implementation.thy	Tue Jul 18 14:46:14 2017 +0100
+++ b/Implementation.thy	Wed Aug 02 13:18:14 2017 +0100
@@ -594,7 +594,7 @@
 
 context valid_trace_p_h
 begin
-
+       
 text {*
   It can be shown that the @{text tG} is not changed by 
   the @{text P}-action. The reason is that the edge added to @{text RAG}
@@ -603,6 +603,8 @@
   the node of @{text cs} is isolated from the original @{text RAG}.
 *}
 
+thm RAG_es
+
 lemma tG_es: "tG (e # s) = tG s"
 proof -
   have [simp]: "\<And> th1. (Th th1, Cs cs) \<notin> RAG s"
@@ -640,12 +642,19 @@
   "tRAG (e#s) = tRAG s \<union> {(Th th, Th holder)}"
   using RAG_tRAG_transfer[OF RAG_es cs_held] .
 
+
+lemma tG_ancestors_tRAG_refute:
+  assumes "th'' \<notin> ancestors (tG (e#s)) th"
+  shows "Th th'' \<notin> ancestors (tRAG (e#s)) (Th th)"
+  using assms using node.inject(1) tRAG_ancestorsE_tG by force 
+
 text {*
   The following lemma shows only the ancestors of @{text th} (the initiating 
   thread of the @{text P}-operation) may possibly 
   need a @{text cp}-recalculation. All other threads (including @{text th} itself)
   do not need @{text cp}-recalculation. 
 *}
+
 lemma cp_kept:
   assumes "Th th'' \<notin> ancestors (tRAG (e#s)) (Th th)"
   shows "cp (e#s) th'' = cp s th''"
@@ -681,6 +690,12 @@
   show ?thesis by (unfold cp_alt_def1 h preced_kept, simp)
 qed
 
+lemma cp_kept_tG:
+  assumes "th'' \<notin> ancestors (tG (e#s)) th"
+  shows "cp (e#s) th'' = cp s th''"
+  using cp_kept tG_ancestors_tRAG_refute assms
+  by blast
+  
 text {*
   Lemma @{thm cp_kept} means that the @{text cp}-recalculation starts from the parent of @{text th},
   going upwards along the chain of ancestors until one root (which is a thread 
@@ -817,6 +832,7 @@
   qed
 qed
 
+
 text {*
   The following lemma is about the possible early termination of 
   @{text cp}-recalculation. The lemma says that @{text cp}-recalculation 
@@ -843,6 +859,13 @@
   show ?thesis by metis
 qed
 
+lemma cp_up_tG:
+  assumes "th' \<in> ancestors (tG (e#s)) th"
+  and "cp (e#s) th' = cp s th'"
+  and "th'' \<in> ancestors (tG (e#s)) th'"
+  shows "cp (e#s) th'' = cp s th''"
+  using assms cp_up ancestors_tG_tRAG by blast   
+
 end
 
 text {*