--- a/RTree.thy	Wed Aug 24 16:13:20 2016 +0200
+++ b/RTree.thy	Sun Oct 02 14:32:05 2016 +0100
@@ -77,6 +77,27 @@
 
 definition "ancestors r x = {y. (x, y) \<in> r^+}"
 
+(* tmp *)
+definition 
+  "nancestors r x \<equiv> ancestors r x \<union> {x}"
+
+lemma nancestors_def2:
+  "nancestors r x \<equiv> {y. (x, y) \<in> r\<^sup>*}"
+unfolding nancestors_def
+apply(auto)
+by (smt Collect_cong ancestors_def insert_compr mem_Collect_eq rtrancl_eq_or_trancl)
+
+lemma nancestors2:
+  "y \<in> ancestors r x \<Longrightarrow> y \<in> nancestors r x"
+apply(auto simp add: nancestors_def)
+done
+
+lemma nancestors3:
+  "\<lbrakk>y \<in> nancestors r x; x \<noteq> y\<rbrakk> \<Longrightarrow> y \<in> ancestors r x"
+apply(auto simp add: nancestors_def)
+done
+(* end tmp *)
+
 definition "root r x = (ancestors r x = {})"
 
 lemma root_indep: