404 lemma subtree_tRAG_thread:

   405   assumes "th \<in> threads s"

   406   shows "subtree (tRAG s) (Th th) \<subseteq> Th ` threads s" (is "?L \<subseteq> ?R")

   407 proof -

   408   have "?L = {Th th' |th'. Th th' \<in> subtree (RAG s) (Th th)}"

   409     by (unfold tRAG_subtree_eq, simp)

   410   also have "... \<subseteq> ?R"

   411   proof

   412     fix x

   413     assume "x \<in> {Th th' |th'. Th th' \<in> subtree (RAG s) (Th th)}"

   414     then obtain th' where h: "x = Th th'" "Th th' \<in> subtree (RAG s) (Th th)" by auto

   415     from this(2)

   416     show "x \<in> ?R"

   417     proof(cases rule:subtreeE)

   418       case 1

   419       thus ?thesis by (simp add: assms h(1)) 

   420     next

   421       case 2

   422       thus ?thesis by (metis ancestors_Field dm_RAG_threads h(1) image_eqI) 

   423     qed

   424   qed

   425   finally show ?thesis .

   426 qed