--- a/PIPBasics.thy	Mon Jul 04 14:04:11 2016 +0100
+++ b/PIPBasics.thy	Thu Jul 07 13:32:09 2016 +0100
@@ -2846,8 +2846,9 @@
 
 sublocale valid_trace < fsbtRAGs?: fgraph "RAG s"
 proof
-  show "\<forall>x\<in>Range (RAG s). finite (children (RAG s) x)" 
-    by (rule finite_fbranchI[OF finite_RAG])
+  show "\<And>x. finite (children (RAG s) x)"
+    by (smt Collect_empty_eq Range.intros children_def finite.emptyI finite_RAG finite_fbranchI) 
+    (*by (rule finite_fbranchI[OF finite_RAG])*)
 next
   show "wf (RAG s)" using wf_RAG .
 qed
@@ -2892,21 +2893,22 @@
   from acyclic_tRAG show "acyclic (tRAG s)" .
 qed
 
+
 sublocale valid_trace < fsbttRAGs?: fgraph "tRAG s"
 proof
-  show "\<forall>x\<in>Range (tRAG s). finite (children (tRAG s) x)"
-  proof(unfold tRAG_def, rule fbranch_compose)
-        show "\<forall>x\<in>Range (wRAG s). finite (children (wRAG s) x)"
-        proof(rule finite_fbranchI)
-           from finite_RAG show "finite (wRAG s)"
-           by (unfold RAG_split, auto)
-        qed
-    next
-        show "\<forall>x\<in>Range (hRAG s). finite (children (hRAG s) x)"
-        proof(rule finite_fbranchI)
-           from finite_RAG 
-           show "finite (hRAG s)" by (unfold RAG_split, auto)
-        qed
+  fix x
+  show "finite (children (tRAG s) x)"
+  proof(unfold tRAG_def, rule fbranch_compose1[rule_format])
+    fix x show "finite (children (wRAG s) x)" 
+    proof(rule finite_fbranchI1[rule_format])
+      show "finite (wRAG s)" using finite_RAG[unfolded RAG_split] by auto
+    qed
+  next
+    fix x
+    show "finite (children (hRAG s) x)"
+    proof(rule finite_fbranchI1[rule_format])
+      show "finite (hRAG s)" using finite_RAG[unfolded RAG_split] by auto
+    qed
   qed
 next
   show "wf (tRAG s)"