--- a/RTree.thy	Mon Jul 04 14:04:11 2016 +0100
+++ b/RTree.thy	Thu Jul 07 13:32:09 2016 +0100
@@ -110,9 +110,8 @@
 
 definition "children r x = {y. (y, x) \<in> r}"
 
-locale fgraph =
-  fixes r
-  assumes fb: "\<forall> x \<in> Range r . finite (children r x)"
+locale fgraph = rtree +
+  assumes fb: "finite (children r x)"
   assumes wf: "wf r"
 begin
 
@@ -1402,7 +1401,7 @@
     next
       case False
       hence "x \<in> Range r" by (auto simp:children_def)
-      from fb[rule_format, OF this] 
+      from fb 
       have "finite (children r x)" .
       thus ?thesis by (rule finite_imageI)
     qed
@@ -1645,6 +1644,14 @@
   } thus ?thesis using assms by auto
 qed
 
+lemma fbranch_compose1 [intro, simp]:
+  assumes "\<forall>x. finite (children r1 x)"
+  and "\<forall>x. finite (children r2 x)"
+  shows "\<forall>x. finite (children (r1 O r2) x)"
+by (metis (no_types, lifting) Collect_empty_eq Range.intros assms(1) 
+         assms(2) children_def fbranch_compose finite.emptyI)
+
+
 lemma finite_fbranchI [intro]:
   assumes "finite r"
   shows "\<forall> x \<in> Range r . finite (children r x)"
@@ -1661,6 +1668,12 @@
   } thus ?thesis by auto
 qed
 
+lemma finite_fbranchI1 [intro]:
+  assumes "finite r"
+  shows "\<forall> x . finite (children r x)"
+  by (metis (no_types, lifting) Collect_empty_eq Range.intros assms 
+      children_def finite.emptyI finite_fbranchI)
+
 lemma subset_fbranchI [intro]:
   assumes "\<forall> x \<in> Range r1 . finite (children r1 x)"
   and "r2 \<subseteq> r1"