487   shows "(x, y) \<in> r^*"

   487   shows "(x, y) \<in> r^*"

   488 proof -

   488 proof -

   489   from iffD2[OF rtranclp_eq_rtrancl_path] and assms[unfolded rpath_def]

   489   from iffD2[OF rtranclp_eq_rtrancl_path] and assms[unfolded rpath_def]

   490   have "(pred_of r)\<^sup>*\<^sup>* x y" by metis

   490   have "(pred_of r)\<^sup>*\<^sup>* x y" by metis

   491   thus ?thesis by (simp add: pred_of_star star_2_pstar)

   491   thus ?thesis by (simp add: pred_of_star star_2_pstar)

   493 

   493 

   494 lemma subtree_transfer:

   494 lemma subtree_transfer:

   495   assumes "a \<in> subtree r1 a'"

   495   assumes "a \<in> subtree r1 a'"

   496   and "r1 \<subseteq> r2"

   496   and "r1 \<subseteq> r2"

   497   shows "a \<in> subtree r2 a'"

   497   shows "a \<in> subtree r2 a'"

   561 

   561 

   562 lemma ancestors_subtreeI:

   562 lemma ancestors_subtreeI:

   563   assumes "b \<in> ancestors r a"

   563   assumes "b \<in> ancestors r a"

   564   shows "a \<in> subtree r b"

   564   shows "a \<in> subtree r b"

   565   using assms by (auto simp:subtree_def ancestors_def)

   565   using assms by (auto simp:subtree_def ancestors_def)

   566 

   573 

   567 lemma subtreeE:

   574 lemma subtreeE:

   568   assumes "a \<in> subtree r b"

   575   assumes "a \<in> subtree r b"

   569   obtains "a = b"

   576   obtains "a = b"

   570       | "a \<noteq> b" and "b \<in> ancestors r a"

   577       | "a \<noteq> b" and "b \<in> ancestors r a"