--- a/CpsG.thy~	Wed Jan 06 16:34:26 2016 +0000
+++ b/CpsG.thy~	Thu Jan 07 08:33:13 2016 +0800
@@ -401,6 +401,29 @@
   using assms
   by (metis Field_def UnE dm_RAG_threads range_in vt)
 
+lemma subtree_tRAG_thread:
+  assumes "th \<in> threads s"
+  shows "subtree (tRAG s) (Th th) \<subseteq> Th ` threads s" (is "?L \<subseteq> ?R")
+proof -
+  have "?L = {Th th' |th'. Th th' \<in> subtree (RAG s) (Th th)}"
+    by (unfold tRAG_subtree_eq, simp)
+  also have "... \<subseteq> ?R"
+  proof
+    fix x
+    assume "x \<in> {Th th' |th'. Th th' \<in> subtree (RAG s) (Th th)}"
+    then obtain th' where h: "x = Th th'" "Th th' \<in> subtree (RAG s) (Th th)" by auto
+    from this(2)
+    show "x \<in> ?R"
+    proof(cases rule:subtreeE)
+      case 1
+      thus ?thesis by (simp add: assms h(1)) 
+    next
+      case 2
+      thus ?thesis by (metis ancestors_Field dm_RAG_threads h(1) image_eqI) 
+    qed
+  qed
+  finally show ?thesis .
+qed
 
 lemma readys_root:
   assumes "th \<in> readys s"