# HG changeset patch
# User zhangx
# Date 1450797211 -28800
# Node ID 031d2ae9c9b8c1ff68da0b0074fa314bc0688732
# Parent  f8194fd6214ffd39166de255c012b82609396334
In the middle of retrofiting ExtGG.thy.

diff -r f8194fd6214f -r 031d2ae9c9b8 CpsG.thy
--- a/CpsG.thy	Fri Dec 18 22:47:32 2015 +0800
+++ b/CpsG.thy	Tue Dec 22 23:13:31 2015 +0800
@@ -10,6 +10,10 @@
        difference is the order of arguemts. *}
 definition "the_preced s th = preced th s"
 
+lemma inj_the_preced: 
+  "inj_on (the_preced s) (threads s)"
+  by (metis inj_onI preced_unique the_preced_def)
+
 text {* @{term "the_thread"} extracts thread out of RAG node. *}
 fun the_thread :: "node \<Rightarrow> thread" where
    "the_thread (Th th) = th"
diff -r f8194fd6214f -r 031d2ae9c9b8 CpsG.thy~
--- a/CpsG.thy~	Fri Dec 18 22:47:32 2015 +0800
+++ b/CpsG.thy~	Tue Dec 22 23:13:31 2015 +0800
@@ -6,24 +6,37 @@
 imports PrioG Max RTree
 begin
 
+text {* @{text "the_preced"} is also the same as @{text "preced"}, the only
+       difference is the order of arguemts. *}
 definition "the_preced s th = preced th s"
 
+text {* @{term "the_thread"} extracts thread out of RAG node. *}
 fun the_thread :: "node \<Rightarrow> thread" where
    "the_thread (Th th) = th"
 
+text {* The following @{text "wRAG"} is the waiting sub-graph of @{text "RAG"}. *}
 definition "wRAG (s::state) = {(Th th, Cs cs) | th cs. waiting s th cs}"
 
+text {* The following @{text "hRAG"} is the holding sub-graph of @{text "RAG"}. *}
 definition "hRAG (s::state) =  {(Cs cs, Th th) | th cs. holding s th cs}"
 
+text {* The following lemma splits @{term "RAG"} graph into the above two sub-graphs. *}
+lemma RAG_split: "RAG s = (wRAG s \<union> hRAG s)"
+  by (unfold s_RAG_abv wRAG_def hRAG_def s_waiting_abv 
+             s_holding_abv cs_RAG_def, auto)
+
+text {* 
+  The following @{text "tRAG"} is the thread-graph derived from @{term "RAG"}.
+  It characterizes the dependency between threads when calculating current
+  precedences. It is defined as the composition of the above two sub-graphs, 
+  names @{term "wRAG"} and @{term "hRAG"}.
+ *}
 definition "tRAG s = wRAG s O hRAG s"
 
+(* ccc *)
+
 definition "cp_gen s x =
                   Max ((the_preced s \<circ> the_thread) ` subtree (tRAG s) x)"
-(* ccc *)
-
-lemma RAG_split: "RAG s = (wRAG s \<union> hRAG s)"
-  by (unfold s_RAG_abv wRAG_def hRAG_def s_waiting_abv 
-             s_holding_abv cs_RAG_def, auto)
 
 lemma tRAG_alt_def: 
   "tRAG s = {(Th th1, Th th2) | th1 th2. 
@@ -363,11 +376,6 @@
   from acyclic_RAG[OF vt] show "acyclic (RAG s)" .
 qed
 
-end
-
-context valid_trace
-begin
-
 lemma sgv_wRAG: "single_valued (wRAG s)"
   using waiting_unique[OF vt] 
   by (unfold single_valued_def wRAG_def, auto)
@@ -395,8 +403,19 @@
 lemma rtree_RAG: "rtree (RAG s)"
   using sgv_RAG acyclic_RAG[OF vt]
   by (unfold rtree_def rtree_axioms_def sgv_def, auto)
+end
 
-end
+
+sublocale valid_trace < rtree_RAG: rtree "RAG s"
+proof
+  show "single_valued (RAG s)"
+  apply (intro_locales)
+    by (unfold single_valued_def, 
+        auto intro:unique_RAG[OF vt])
+
+  show "acyclic (RAG s)"
+     by (rule acyclic_RAG[OF vt])
+qed
 
 sublocale valid_trace < rtree_s: rtree "tRAG s"
 proof(unfold_locales)
@@ -478,7 +497,6 @@
   finally show ?thesis by simp
 qed
 
-
 context valid_trace
 begin
 
@@ -560,363 +578,7 @@
 
 end
 
-(* ccc *)
-
-
-
-(* obvious lemma *)
-
-lemma wf_RAG:
-  assumes vt: "vt s"
-  shows "wf (RAG s)"
-proof(rule finite_acyclic_wf)
-  from finite_RAG[OF vt] show "finite (RAG s)" .
-next
-  from acyclic_RAG[OF vt] show "acyclic (RAG s)" .
-qed
-
-definition child :: "state \<Rightarrow> (node \<times> node) set"
-  where "child s \<equiv>
-            {(Th th', Th th) | th th'. \<exists>cs. (Th th', Cs cs) \<in> RAG s \<and> (Cs cs, Th th) \<in> RAG s}"
-
-definition children :: "state \<Rightarrow> thread \<Rightarrow> thread set"
-  where "children s th \<equiv> {th'. (Th th', Th th) \<in> child s}"
-
-lemma children_def2:
-  "children s th \<equiv> {th'. \<exists> cs. (Th th', Cs cs) \<in> RAG s \<and> (Cs cs, Th th) \<in> RAG s}"
-unfolding child_def children_def by simp
-
-lemma children_dependants: 
-  "children s th \<subseteq> dependants (wq s) th"
-  unfolding children_def2
-  unfolding cs_dependants_def
-  by (auto simp add: eq_RAG)
-
-lemma child_unique:
-  assumes vt: "vt s"
-  and ch1: "(Th th, Th th1) \<in> child s"
-  and ch2: "(Th th, Th th2) \<in> child s"
-  shows "th1 = th2"
-using ch1 ch2 
-proof(unfold child_def, clarsimp)
-  fix cs csa
-  assume h1: "(Th th, Cs cs) \<in> RAG s"
-    and h2: "(Cs cs, Th th1) \<in> RAG s"
-    and h3: "(Th th, Cs csa) \<in> RAG s"
-    and h4: "(Cs csa, Th th2) \<in> RAG s"
-  from unique_RAG[OF vt h1 h3] have "cs = csa" by simp
-  with h4 have "(Cs cs, Th th2) \<in> RAG s" by simp
-  from unique_RAG[OF vt h2 this]
-  show "th1 = th2" by simp
-qed 
-
-lemma RAG_children:
-  assumes h: "(Th th1, Th th2) \<in> (RAG s)^+"
-  shows "th1 \<in> children s th2 \<or> (\<exists> th3. th3 \<in> children s th2 \<and> (Th th1, Th th3) \<in> (RAG s)^+)"
-proof -
-  from h show ?thesis
-  proof(induct rule: tranclE)
-    fix c th2
-    assume h1: "(Th th1, c) \<in> (RAG s)\<^sup>+"
-    and h2: "(c, Th th2) \<in> RAG s"
-    from h2 obtain cs where eq_c: "c = Cs cs"
-      by (case_tac c, auto simp:s_RAG_def)
-    show "th1 \<in> children s th2 \<or> (\<exists>th3. th3 \<in> children s th2 \<and> (Th th1, Th th3) \<in> (RAG s)\<^sup>+)"
-    proof(rule tranclE[OF h1])
-      fix ca
-      assume h3: "(Th th1, ca) \<in> (RAG s)\<^sup>+"
-        and h4: "(ca, c) \<in> RAG s"
-      show "th1 \<in> children s th2 \<or> (\<exists>th3. th3 \<in> children s th2 \<and> (Th th1, Th th3) \<in> (RAG s)\<^sup>+)"
-      proof -
-        from eq_c and h4 obtain th3 where eq_ca: "ca = Th th3"
-          by (case_tac ca, auto simp:s_RAG_def)
-        from eq_ca h4 h2 eq_c
-        have "th3 \<in> children s th2" by (auto simp:children_def child_def)
-        moreover from h3 eq_ca have "(Th th1, Th th3) \<in> (RAG s)\<^sup>+" by simp
-        ultimately show ?thesis by auto
-      qed
-    next
-      assume "(Th th1, c) \<in> RAG s"
-      with h2 eq_c
-      have "th1 \<in> children s th2"
-        by (auto simp:children_def child_def)
-      thus ?thesis by auto
-    qed
-  next
-    assume "(Th th1, Th th2) \<in> RAG s"
-    thus ?thesis
-      by (auto simp:s_RAG_def)
-  qed
-qed
-
-lemma sub_child: "child s \<subseteq> (RAG s)^+"
-  by (unfold child_def, auto)
-
-lemma wf_child: 
-  assumes vt: "vt s"
-  shows "wf (child s)"
-apply(rule wf_subset)
-apply(rule wf_trancl[OF wf_RAG[OF vt]])
-apply(rule sub_child)
-done
-
-lemma RAG_child_pre:
-  assumes vt: "vt s"
-  shows
-  "(Th th, n) \<in> (RAG s)^+ \<longrightarrow> (\<forall> th'. n = (Th th') \<longrightarrow> (Th th, Th th') \<in> (child s)^+)" (is "?P n")
-proof -
-  from wf_trancl[OF wf_RAG[OF vt]]
-  have wf: "wf ((RAG s)^+)" .
-  show ?thesis
-  proof(rule wf_induct[OF wf, of ?P], clarsimp)
-    fix th'
-    assume ih[rule_format]: "\<forall>y. (y, Th th') \<in> (RAG s)\<^sup>+ \<longrightarrow>
-               (Th th, y) \<in> (RAG s)\<^sup>+ \<longrightarrow> (\<forall>th'. y = Th th' \<longrightarrow> (Th th, Th th') \<in> (child s)\<^sup>+)"
-    and h: "(Th th, Th th') \<in> (RAG s)\<^sup>+"
-    show "(Th th, Th th') \<in> (child s)\<^sup>+"
-    proof -
-      from RAG_children[OF h]
-      have "th \<in> children s th' \<or> (\<exists>th3. th3 \<in> children s th' \<and> (Th th, Th th3) \<in> (RAG s)\<^sup>+)" .
-      thus ?thesis
-      proof
-        assume "th \<in> children s th'"
-        thus "(Th th, Th th') \<in> (child s)\<^sup>+" by (auto simp:children_def)
-      next
-        assume "\<exists>th3. th3 \<in> children s th' \<and> (Th th, Th th3) \<in> (RAG s)\<^sup>+"
-        then obtain th3 where th3_in: "th3 \<in> children s th'" 
-          and th_dp: "(Th th, Th th3) \<in> (RAG s)\<^sup>+" by auto
-        from th3_in have "(Th th3, Th th') \<in> (RAG s)^+" by (auto simp:children_def child_def)
-        from ih[OF this th_dp, of th3] have "(Th th, Th th3) \<in> (child s)\<^sup>+" by simp
-        with th3_in show "(Th th, Th th') \<in> (child s)\<^sup>+" by (auto simp:children_def)
-      qed
-    qed
-  qed
-qed
-
-lemma RAG_child: "\<lbrakk>vt s; (Th th, Th th') \<in> (RAG s)^+\<rbrakk> \<Longrightarrow> (Th th, Th th') \<in> (child s)^+"
-  by (insert RAG_child_pre, auto)
-
-lemma child_RAG_p:
-  assumes "(n1, n2) \<in> (child s)^+"
-  shows "(n1, n2) \<in> (RAG s)^+"
-proof -
-  from assms show ?thesis
-  proof(induct)
-    case (base y)
-    with sub_child show ?case by auto
-  next
-    case (step y z)
-    assume "(y, z) \<in> child s"
-    with sub_child have "(y, z) \<in> (RAG s)^+" by auto
-    moreover have "(n1, y) \<in> (RAG s)^+" by fact
-    ultimately show ?case by auto
-  qed
-qed
-
-text {* (* ddd *)
-*}
-lemma child_RAG_eq: 
-  assumes vt: "vt s"
-  shows "(Th th1, Th th2) \<in> (child s)^+  \<longleftrightarrow> (Th th1, Th th2) \<in> (RAG s)^+"
-  by (auto intro: RAG_child[OF vt] child_RAG_p)
-
-text {* (* ddd *)
-*}
-lemma children_no_dep:
-  fixes s th th1 th2 th3
-  assumes vt: "vt s"
-  and ch1: "(Th th1, Th th) \<in> child s"
-  and ch2: "(Th th2, Th th) \<in> child s"
-  and ch3: "(Th th1, Th th2) \<in> (RAG s)^+"
-  shows "False"
-proof -
-  from RAG_child[OF vt ch3]
-  have "(Th th1, Th th2) \<in> (child s)\<^sup>+" .
-  thus ?thesis
-  proof(rule converse_tranclE)
-    assume "(Th th1, Th th2) \<in> child s"
-    from child_unique[OF vt ch1 this] have "th = th2" by simp
-    with ch2 have "(Th th2, Th th2) \<in> child s" by simp
-    with wf_child[OF vt] show ?thesis by auto
-  next
-    fix c
-    assume h1: "(Th th1, c) \<in> child s"
-      and h2: "(c, Th th2) \<in> (child s)\<^sup>+"
-    from h1 obtain th3 where eq_c: "c = Th th3" by (unfold child_def, auto)
-    with h1 have "(Th th1, Th th3) \<in> child s" by simp
-    from child_unique[OF vt ch1 this] have eq_th3: "th3 = th" by simp
-    with eq_c and h2 have "(Th th, Th th2) \<in> (child s)\<^sup>+" by simp
-    with ch2 have "(Th th, Th th) \<in> (child s)\<^sup>+" by auto
-    moreover have "wf ((child s)\<^sup>+)"
-    proof(rule wf_trancl)
-      from wf_child[OF vt] show "wf (child s)" .
-    qed
-    ultimately show False by auto
-  qed
-qed
-
-text {* (* ddd *)
-*}
-lemma unique_RAG_p:
-  assumes vt: "vt s"
-  and dp1: "(n, n1) \<in> (RAG s)^+"
-  and dp2: "(n, n2) \<in> (RAG s)^+"
-  and neq: "n1 \<noteq> n2"
-  shows "(n1, n2) \<in> (RAG s)^+ \<or> (n2, n1) \<in> (RAG s)^+"
-proof(rule unique_chain [OF _ dp1 dp2 neq])
-  from unique_RAG[OF vt]
-  show "\<And>a b c. \<lbrakk>(a, b) \<in> RAG s; (a, c) \<in> RAG s\<rbrakk> \<Longrightarrow> b = c" by auto
-qed
-
-text {* (* ddd *)
-*}
-lemma dependants_child_unique:
-  fixes s th th1 th2 th3
-  assumes vt: "vt s"
-  and ch1: "(Th th1, Th th) \<in> child s"
-  and ch2: "(Th th2, Th th) \<in> child s"
-  and dp1: "th3 \<in> dependants s th1"
-  and dp2: "th3 \<in> dependants s th2"
-shows "th1 = th2"
-proof -
-  { assume neq: "th1 \<noteq> th2"
-    from dp1 have dp1: "(Th th3, Th th1) \<in> (RAG s)^+" 
-      by (simp add:s_dependants_def eq_RAG)
-    from dp2 have dp2: "(Th th3, Th th2) \<in> (RAG s)^+" 
-      by (simp add:s_dependants_def eq_RAG)
-    from unique_RAG_p[OF vt dp1 dp2] and neq
-    have "(Th th1, Th th2) \<in> (RAG s)\<^sup>+ \<or> (Th th2, Th th1) \<in> (RAG s)\<^sup>+" by auto
-    hence False
-    proof
-      assume "(Th th1, Th th2) \<in> (RAG s)\<^sup>+ "
-      from children_no_dep[OF vt ch1 ch2 this] show ?thesis .
-    next
-      assume " (Th th2, Th th1) \<in> (RAG s)\<^sup>+"
-      from children_no_dep[OF vt ch2 ch1 this] show ?thesis .
-    qed
-  } thus ?thesis by auto
-qed
-
-lemma RAG_plus_elim:
-  assumes "vt s"
-  fixes x
-  assumes "(Th x, Th th) \<in> (RAG (wq s))\<^sup>+"
-  shows "\<exists>th'\<in>children s th. x = th' \<or> (Th x, Th th') \<in> (RAG (wq s))\<^sup>+"
-  using assms(2)[unfolded eq_RAG, folded child_RAG_eq[OF `vt s`]]
-  apply (unfold children_def)
-  by (metis assms(2) children_def RAG_children eq_RAG)
-
-text {* (* ddd *)
-*}
-lemma dependants_expand:
-  assumes "vt s"
-  shows "dependants (wq s) th = (children s th) \<union> (\<Union>((dependants (wq s)) ` children s th))"
-apply(simp add: image_def)
-unfolding cs_dependants_def
-apply(auto)
-apply (metis assms RAG_plus_elim mem_Collect_eq)
-apply (metis child_RAG_p children_def eq_RAG mem_Collect_eq r_into_trancl')
-by (metis assms child_RAG_eq children_def eq_RAG mem_Collect_eq trancl.trancl_into_trancl)
-
-lemma finite_children:
-  assumes "vt s"
-  shows "finite (children s th)"
-  using children_dependants dependants_threads[OF assms] finite_threads[OF assms]
-  by (metis rev_finite_subset)
-  
-lemma finite_dependants:
-  assumes "vt s"
-  shows "finite (dependants (wq s) th')"
-  using dependants_threads[OF assms] finite_threads[OF assms]
-  by (metis rev_finite_subset)
-
-abbreviation
-  "preceds s ths \<equiv> {preced th s| th. th \<in> ths}"
-
-abbreviation
-  "cpreceds s ths \<equiv> (cp s) ` ths"
-
-lemma Un_compr:
-  "{f th | th. R th \<or> Q th} = ({f th | th. R th} \<union> {f th' | th'. Q th'})"
-by auto
-
-lemma in_disj:
-  shows "x \<in> A \<or> (\<exists>y \<in> A. x \<in> Q y) \<longleftrightarrow> (\<exists>y \<in> A. x = y \<or> x \<in> Q y)"
-by metis
-
-lemma UN_exists:
-  shows "(\<Union>x \<in> A. {f y | y. Q y x}) = ({f y | y. (\<exists>x \<in> A. Q y x)})"
-by auto
-
-text {* (* ddd *)
-  This is the recursive equation used to compute the current precedence of 
-  a thread (the @{text "th"}) here. 
-*}
-lemma cp_rec:
-  fixes s th
-  assumes vt: "vt s"
-  shows "cp s th = Max ({preced th s} \<union> (cp s ` children s th))"
-proof(cases "children s th = {}")
-  case True
-  show ?thesis
-    unfolding cp_eq_cpreced cpreced_def 
-    by (subst dependants_expand[OF `vt s`]) (simp add: True)
-next
-  case False
-  show ?thesis (is "?LHS = ?RHS")
-  proof -
-    have eq_cp: "cp s = (\<lambda>th. Max (preceds s ({th} \<union> dependants (wq s) th)))"
-      by (simp add: fun_eq_iff cp_eq_cpreced cpreced_def Un_compr image_Collect[symmetric])
-  
-    have not_emptyness_facts[simp]: 
-      "dependants (wq s) th \<noteq> {}" "children s th \<noteq> {}"
-      using False dependants_expand[OF assms] by(auto simp only: Un_empty)
-
-    have finiteness_facts[simp]:
-      "\<And>th. finite (dependants (wq s) th)" "\<And>th. finite (children s th)"
-      by (simp_all add: finite_dependants[OF `vt s`] finite_children[OF `vt s`])
-
-    (* expanding definition *)
-    have "?LHS = Max ({preced th s} \<union> preceds s (dependants (wq s) th))"
-      unfolding eq_cp by (simp add: Un_compr)
-    
-    (* moving Max in *)
-    also have "\<dots> = max (Max {preced th s}) (Max (preceds s (dependants (wq s) th)))"
-      by (simp add: Max_Un)
-
-    (* expanding dependants *)
-    also have "\<dots> = max (Max {preced th s}) 
-      (Max (preceds s (children s th \<union> \<Union>(dependants (wq s) ` children s th))))"
-      by (subst dependants_expand[OF `vt s`]) (simp)
-
-    (* moving out big Union *)
-    also have "\<dots> = max (Max {preced th s})
-      (Max (preceds s (\<Union> ({children s th} \<union> (dependants (wq s) ` children s th)))))"  
-      by simp
-
-    (* moving in small union *)
-    also have "\<dots> = max (Max {preced th s})
-      (Max (preceds s (\<Union> ((\<lambda>th. {th} \<union> (dependants (wq s) th)) ` children s th))))"  
-      by (simp add: in_disj)
-
-    (* moving in preceds *)
-    also have "\<dots> = max (Max {preced th s})  
-      (Max (\<Union> ((\<lambda>th. preceds s ({th} \<union> (dependants (wq s) th))) ` children s th)))" 
-      by (simp add: UN_exists)
-
-    (* moving in Max *)
-    also have "\<dots> = max (Max {preced th s})  
-      (Max ((\<lambda>th. Max (preceds s ({th} \<union> (dependants (wq s) th)))) ` children s th))" 
-       by (subst Max_Union) (auto simp add: image_image) 
-
-    (* folding cp + moving out Max *)
-    also have "\<dots> = ?RHS" 
-      unfolding eq_cp by (simp add: Max_insert)
-
-    finally show "?LHS = ?RHS" .
-  qed
-qed
-
+(* keep *)
 lemma next_th_holding:
   assumes vt: "vt s"
   and nxt: "next_th s th cs th'"
@@ -1006,6 +668,16 @@
          the legitimacy of @{text "s"} can be derived. *}
   assumes vt_s: "vt s"
 
+sublocale step_set_cps < vat_s : valid_trace "s"
+proof
+  from vt_s show "vt s" .
+qed
+
+sublocale step_set_cps < vat_s' : valid_trace "s'"
+proof
+  from step_back_vt[OF vt_s[unfolded s_def]] show "vt s'" .
+qed
+
 context step_set_cps 
 begin
 
@@ -1015,7 +687,6 @@
 *}
 
 lemma eq_preced:
-  fixes th'
   assumes "th' \<noteq> th"
   shows "preced th' s = preced th' s'"
 proof -
@@ -1089,7 +760,8 @@
     hence "th \<in> runing s'" by (cases, simp)
     thus ?thesis by (simp add:readys_def runing_def)
   qed
-  from readys_in_no_subtree[OF step_back_vt[OF vt_s[unfolded s_def]] this assms(1)]
+  find_theorems readys subtree
+  from vat_s'.readys_in_no_subtree[OF this assms(1)]
   show ?thesis by blast
 qed
 
@@ -1118,40 +790,26 @@
   -- {* @{text "s"} is assumed to be valid, which implies the validity of @{text "s'"} *}
   assumes vt_s: "vt s"
 
-context step_v_cps
-begin
-
-lemma rtree_RAGs: "rtree (RAG s)"
+sublocale step_v_cps < vat_s : valid_trace "s"
 proof
-  show "single_valued (RAG s)"
-  apply (intro_locales)
-    by (unfold single_valued_def, auto intro: unique_RAG[OF vt_s])
-
-  show "acyclic (RAG s)"
-     by (rule acyclic_RAG[OF vt_s])
+  from vt_s show "vt s" .
 qed
 
-lemma rtree_RAGs': "rtree (RAG s')"
+sublocale step_v_cps < vat_s' : valid_trace "s'"
 proof
-  show "single_valued (RAG s')"
-  apply (intro_locales)
-    by (unfold single_valued_def, 
-        auto intro:unique_RAG[OF step_back_vt[OF vt_s[unfolded s_def]]])
-
-  show "acyclic (RAG s')"
-     by (rule acyclic_RAG[OF step_back_vt[OF vt_s[unfolded s_def]]])
+  from step_back_vt[OF vt_s[unfolded s_def]] show "vt s'" .
 qed
 
-lemmas vt_s' = step_back_vt[OF vt_s[unfolded s_def]]
+context step_v_cps
+begin
 
 lemma ready_th_s': "th \<in> readys s'"
   using step_back_step[OF vt_s[unfolded s_def]]
   by (cases, simp add:runing_def)
 
-
 lemma ancestors_th: "ancestors (RAG s') (Th th) = {}"
 proof -
-  from readys_root[OF vt_s' ready_th_s']
+  from vat_s'.readys_root[OF ready_th_s']
   show ?thesis
   by (unfold root_def, simp)
 qed
@@ -1174,9 +832,8 @@
 lemma ancestors_cs: 
   "ancestors (RAG s') (Cs cs) = {Th th}"
 proof -
-  find_theorems ancestors
   have "ancestors (RAG s') (Cs cs) = ancestors (RAG s') (Th th)  \<union>  {Th th}"
-  proof(rule RTree.rtree.ancestors_accum[OF rtree_RAGs'])
+  proof(rule vat_s'.rtree_RAG.ancestors_accum)
     from vt_s[unfolded s_def]
     have " PIP s' (V th cs)" by (cases, simp)
     thus "(Cs cs, Th th) \<in> RAG s'" 
@@ -1194,7 +851,6 @@
 
 end
 
-
 text {*
   The following @{text "step_v_cps_nt"} is the sub-locale for @{text "V"}-operation, 
   which represents the case when there is another thread @{text "th'"}
@@ -1249,13 +905,13 @@
 *)
 
 lemma sub_RAGs': "{(Cs cs, Th th), (Th th', Cs cs)} \<subseteq> RAG s'"
-                using next_th_RAG[OF vt_s' nt] .
+                using next_th_RAG[OF vat_s'.vt nt]  .
 
 lemma ancestors_th': 
   "ancestors (RAG s') (Th th') = {Th th, Cs cs}" 
 proof -
   have "ancestors (RAG s') (Th th') = ancestors (RAG s') (Cs cs) \<union> {Cs cs}"
-  proof(rule  RTree.rtree.ancestors_accum[OF rtree_RAGs'])
+  proof(rule  vat_s'.rtree_RAG.ancestors_accum)
     from sub_RAGs' show "(Th th', Cs cs) \<in> RAG s'" by auto
   qed
   thus ?thesis using ancestors_th ancestors_cs by auto
@@ -1386,7 +1042,8 @@
 
 lemma subtree_th: 
   "subtree (RAG s) (Th th) = subtree (RAG s') (Th th) - {Cs cs}"
-proof(unfold RAG_s, fold subtree_cs, rule RTree.rtree.subtree_del_inside[OF rtree_RAGs'])
+find_theorems "subtree" "_ - _" RAG
+proof(unfold RAG_s, fold subtree_cs, rule vat_s'.rtree_RAG.subtree_del_inside)
   from edge_of_th
   show "(Cs cs, Th th) \<in> edges_in (RAG s') (Th th)"
     by (unfold edges_in_def, auto simp:subtree_def)
@@ -1401,18 +1058,8 @@
   shows "cp s th' = cp s' th'"
   using cp_kept_1 cp_kept_2
   by (cases "th' = th", auto)
- 
 end
 
-find_theorems "_`_" "\<Union> _"
-
-find_theorems "Max" "\<Union> _"
-
-find_theorems wf RAG
-
-thm wf_def
-
-thm image_Union
 
 locale step_P_cps =
   fixes s' th cs s 
@@ -1429,7 +1076,6 @@
   from step_back_vt[OF vt_s[unfolded s_def]] show "vt s'" .
 qed
 
-
 context step_P_cps
 begin
 
@@ -1442,7 +1088,7 @@
 qed
 
 lemma root_th: "root (RAG s') (Th th)"
-  using readys_root[OF vat_s'.vt readys_th] .
+  using readys_root[OF readys_th] .
 
 lemma in_no_others_subtree:
   assumes "th' \<noteq> th"
@@ -1873,7 +1519,8 @@
     qed auto
     have neq_th_a: "th_a \<noteq> th"
     proof -
-      from readys_in_no_subtree[OF vat_s'.vt th_ready assms]
+    find_theorems readys subtree s'
+      from vat_s'.readys_in_no_subtree[OF th_ready assms]
       have "(Th th) \<notin> subtree (RAG s') (Th th')" .
       with tRAG_subtree_RAG[of s' "Th th'"]
       have "(Th th) \<notin> subtree (tRAG s') (Th th')" by auto
diff -r f8194fd6214f -r 031d2ae9c9b8 ExtGG.thy
--- a/ExtGG.thy	Fri Dec 18 22:47:32 2015 +0800
+++ b/ExtGG.thy	Tue Dec 22 23:13:31 2015 +0800
@@ -1,5 +1,5 @@
 theory ExtGG
-imports PrioG
+imports PrioG CpsG
 begin
 
 lemma birth_time_lt:  "s \<noteq> [] \<Longrightarrow> last_set th s < length s"
@@ -34,44 +34,24 @@
   and highest: "preced th s = Max ((cp s)`threads s)"
   and preced_th: "preced th s = Prc prio tm"
 
+sublocale highest_gen < vat_s: valid_trace "s"
+  by (unfold_locales, insert vt_s, simp)
+
 context highest_gen
 begin
 
-
-
 lemma lt_tm: "tm < length s"
   by (insert preced_tm_lt[OF threads_s preced_th], simp)
 
-lemma eq_cp_s_th: "cp s th = preced th s"
+lemma eq_cp_s_th: "cp s th = preced th s" (is "?L = ?R")
 proof -
-  from highest and max_cp_eq[OF vt_s]
-  have is_max: "preced th s = Max ((\<lambda>th. preced th s) ` threads s)" by simp
-  have sbs: "({th} \<union> dependants (wq s) th) \<subseteq> threads s"
-  proof -
-    from threads_s and dependants_threads[OF vt_s, of th]
-    show ?thesis by auto
-  qed
-  show ?thesis
-  proof(unfold cp_eq_cpreced cpreced_def, rule Max_eqI)
-    show "preced th s \<in> (\<lambda>th. preced th s) ` ({th} \<union> dependants (wq s) th)" by simp
-  next
-    fix y 
-    assume "y \<in> (\<lambda>th. preced th s) ` ({th} \<union> dependants (wq s) th)"
-    then obtain th1 where th1_in: "th1 \<in> ({th} \<union> dependants (wq s) th)"
-      and eq_y: "y = preced th1 s" by auto
-    show "y \<le> preced th s"
-    proof(unfold is_max, rule Max_ge)
-      from finite_threads[OF vt_s] 
-      show "finite ((\<lambda>th. preced th s) ` threads s)" by simp
-    next
-      from sbs th1_in and eq_y 
-      show "y \<in> (\<lambda>th. preced th s) ` threads s" by auto
-    qed
-  next
-    from sbs and finite_threads[OF vt_s]
-    show "finite ((\<lambda>th. preced th s) ` ({th} \<union> dependants (wq s) th))"
-      by (auto intro:finite_subset)
-  qed
+  have "?L \<le> ?R"
+  by (unfold highest, rule Max_ge, 
+        auto simp:threads_s finite_threads[OF vt_s])
+  moreover have "?R \<le> ?L"
+    by (unfold vat_s.cp_rec, rule Max_ge, 
+        auto simp:the_preced_def vat_s.fsbttRAGs.finite_children)
+  ultimately show ?thesis by auto
 qed
 
 lemma highest_cp_preced: "cp s th = Max ((\<lambda> th'. preced th' s) ` threads s)"
@@ -117,18 +97,28 @@
   qed
 qed
 
-context extend_highest_gen
-begin
 
-thm extend_highest_gen_axioms_def
+locale red_extend_highest_gen = extend_highest_gen +
+   fixes i::nat
 
-lemma red_moment:
-  "extend_highest_gen s th prio tm (moment i t)"
+sublocale red_extend_highest_gen <   red_moment: extend_highest_gen "s" "th" "prio" "tm" "(moment i t)"
   apply (insert extend_highest_gen_axioms, subst (asm) (1) moment_restm_s [of i t, symmetric])
   apply (unfold extend_highest_gen_def extend_highest_gen_axioms_def, clarsimp)
   by (unfold highest_gen_def, auto dest:step_back_vt_app)
 
-lemma ind [consumes 0, case_names Nil Cons, induct type]:
+
+context extend_highest_gen
+begin
+
+(*
+ lemma red_moment:
+  "extend_highest_gen s th prio tm (moment i t)"
+  apply (insert extend_highest_gen_axioms, subst (asm) (1) moment_restm_s [of i t, symmetric])
+  apply (unfold extend_highest_gen_def extend_highest_gen_axioms_def, clarsimp)
+  by (unfold highest_gen_def, auto dest:step_back_vt_app) 
+*)
+
+ lemma ind [consumes 0, case_names Nil Cons, induct type]:
   assumes 
     h0: "R []"
   and h2: "\<And> e t. \<lbrakk>vt (t@s); step (t@s) e; 
@@ -164,237 +154,195 @@
   qed
 qed
 
+
 lemma th_kept: "th \<in> threads (t @ s) \<and> 
-                 preced th (t@s) = preced th s" (is "?Q t")
+                 preced th (t@s) = preced th s" (is "?Q t") 
 proof -
   show ?thesis
   proof(induct rule:ind)
     case Nil
     from threads_s
-    show "th \<in> threads ([] @ s) \<and> preced th ([] @ s) = preced th s"
+    show ?case
       by auto
   next
     case (Cons e t)
+    interpret h_e: extend_highest_gen _ _ _ _ "(e # t)" using Cons by auto
+    interpret h_t: extend_highest_gen _ _ _ _ t using Cons by auto
     show ?case
     proof(cases e)
       case (Create thread prio)
-      assume eq_e: " e = Create thread prio"
       show ?thesis
       proof -
-        from Cons and eq_e have "step (t@s) (Create thread prio)" by auto
+        from Cons and Create have "step (t@s) (Create thread prio)" by auto
         hence "th \<noteq> thread"
         proof(cases)
-          assume "thread \<notin> threads (t @ s)"
+          case thread_create
           with Cons show ?thesis by auto
         qed
         hence "preced th ((e # t) @ s)  = preced th (t @ s)"
-          by (unfold eq_e, auto simp:preced_def)
+          by (unfold Create, auto simp:preced_def)
         moreover note Cons
         ultimately show ?thesis
-          by (auto simp:eq_e)
+          by (auto simp:Create)
       qed
     next
       case (Exit thread)
-      assume eq_e: "e = Exit thread"
-      from Cons have "extend_highest_gen s th prio tm (e # t)" by auto
-      from extend_highest_gen.exit_diff [OF this] and eq_e
+      from h_e.exit_diff and Exit
       have neq_th: "thread \<noteq> th" by auto
       with Cons
       show ?thesis
-        by (unfold eq_e, auto simp:preced_def)
+        by (unfold Exit, auto simp:preced_def)
     next
       case (P thread cs)
-      assume eq_e: "e = P thread cs"
       with Cons
       show ?thesis 
-        by (auto simp:eq_e preced_def)
+        by (auto simp:P preced_def)
     next
       case (V thread cs)
-      assume eq_e: "e = V thread cs"
       with Cons
       show ?thesis 
-        by (auto simp:eq_e preced_def)
+        by (auto simp:V preced_def)
     next
       case (Set thread prio')
-      assume eq_e: " e = Set thread prio'"
       show ?thesis
       proof -
-        from Cons have "extend_highest_gen s th prio tm (e # t)" by auto
-        from extend_highest_gen.set_diff_low[OF this] and eq_e
+        from h_e.set_diff_low and Set
         have "th \<noteq> thread" by auto
         hence "preced th ((e # t) @ s)  = preced th (t @ s)"
-          by (unfold eq_e, auto simp:preced_def)
+          by (unfold Set, auto simp:preced_def)
         moreover note Cons
         ultimately show ?thesis
-          by (auto simp:eq_e)
+          by (auto simp:Set)
       qed
     qed
   qed
 qed
 
-lemma max_kept: "Max ((\<lambda> th'. preced th' (t @ s)) ` (threads (t@s))) = preced th s"
+lemma Max_remove_less:
+  assumes "finite A"
+  and "a \<in> A"
+  and "b \<in> A"
+  and "a \<noteq> b"
+  and "inj_on f A"
+  and "f a = Max (f ` A)" 
+  shows "Max (f ` (A - {b})) = (Max (f ` A))"
+proof -
+  have "Max (f ` (A - {b})) = Max (f`A - {f b})"
+  proof -
+    have "f ` (A - {b}) = f ` A - f ` {b}"
+    by (rule inj_on_image_set_diff[OF assms(5)], insert assms(3), auto)
+    thus ?thesis by simp
+  qed
+  also have "... =  
+       (if f ` A - {f b} - {f a} = {} then f a else max (f a) (Max (f ` A - {f b} - {f a})))" 
+  proof(subst Max.remove)
+    from assms show "f a \<in> f ` A - {f b}"
+      by (meson DiffI empty_iff imageI inj_on_eq_iff insert_iff) 
+  next
+    from assms(1) show "finite (f ` A - {f b})" by auto
+  qed auto
+  also have "... = Max (f ` A)" (is "?L = ?R")
+  proof(cases "f ` A - {f b} - {f a} = {}")
+    case True
+    with assms show ?thesis by auto
+  next
+    case False
+    hence "?L =  max (f a) (Max (f ` A - {f b} - {f a}))" 
+      by simp
+    also have "... = ?R" 
+    proof -
+      from assms False
+      have "(Max (f ` A - {f b} - {f a})) \<le> f a" by auto
+      thus ?thesis by (simp add: assms(6) max_def) 
+    qed
+    finally show ?thesis .
+  qed
+  finally show ?thesis .
+qed
+
+lemma max_kept: "Max (the_preced (t @ s) ` (threads (t@s))) = preced th s"
 proof(induct rule:ind)
   case Nil
   from highest_preced_thread
-  show "Max ((\<lambda>th'. preced th' ([] @ s)) ` threads ([] @ s)) = preced th s"
-    by simp
+  show ?case
+    by (unfold the_preced_def, simp)
 next
   case (Cons e t)
+    interpret h_e: extend_highest_gen _ _ _ _ "(e # t)" using Cons by auto
+    interpret h_t: extend_highest_gen _ _ _ _ t using Cons by auto
   show ?case
   proof(cases e)
     case (Create thread prio')
-    assume eq_e: " e = Create thread prio'"
-    from Cons and eq_e have stp: "step (t@s) (Create thread prio')" by auto
-    hence neq_thread: "thread \<noteq> th"
-    proof(cases)
-      assume "thread \<notin> threads (t @ s)"
-      moreover have "th \<in> threads (t@s)"
-      proof -
-        from Cons have "extend_highest_gen s th prio tm t" by auto
-        from extend_highest_gen.th_kept[OF this] show ?thesis by (simp)
-      qed
-      ultimately show ?thesis by auto
-    qed
-    from Cons have "extend_highest_gen s th prio tm t" by auto
-    from extend_highest_gen.th_kept[OF this]
-    have h': " th \<in> threads (t @ s) \<and> preced th (t @ s) = preced th s" 
-      by (auto)
-    from stp
-    have thread_ts: "thread \<notin> threads (t @ s)"
-      by (cases, auto)
+    from Cons(2)[unfolded this] 
+    have thread_not_in: "thread \<notin> threads (t@s)" by (cases, simp)
     show ?thesis (is "Max (?f ` ?A) = ?t")
     proof -
-      have "Max (?f ` ?A) = Max(insert (?f thread) (?f ` (threads (t@s))))"
-        by (unfold eq_e, simp)
+      have "Max (?f ` ?A) = Max (insert (?f thread) (?f ` (threads (t@s))))"
+        by (unfold Create, simp)
       moreover have "\<dots> = max (?f thread) (Max (?f ` (threads (t@s))))"
-      proof(rule Max_insert)
-        from Cons have "vt (t @ s)" by auto
-        from finite_threads[OF this]
+      proof(rule Max.insert)
+        from finite_threads[OF Cons(1)]
         show "finite (?f ` (threads (t@s)))" by simp
-      next
-        from h' show "(?f ` (threads (t@s))) \<noteq> {}" by auto
-      qed
-      moreover have "(Max (?f ` (threads (t@s)))) = ?t"
+      qed (insert h_t.th_kept, auto)
+      moreover have "(Max (?f ` (threads (t@s)))) = ?t" 
       proof -
         have "(\<lambda>th'. preced th' ((e # t) @ s)) ` threads (t @ s) = 
-          (\<lambda>th'. preced th' (t @ s)) ` threads (t @ s)" (is "?f1 ` ?B = ?f2 ` ?B")
-        proof -
-          { fix th' 
-            assume "th' \<in> ?B"
-            with thread_ts eq_e
-            have "?f1 th' = ?f2 th'" by (auto simp:preced_def)
-          } thus ?thesis 
-            apply (auto simp:Image_def)
-          proof -
-            fix th'
-            assume h: "\<And>th'. th' \<in> threads (t @ s) \<Longrightarrow> 
-              preced th' (e # t @ s) = preced th' (t @ s)"
-              and h1: "th' \<in> threads (t @ s)"
-            show "preced th' (t @ s) \<in> (\<lambda>th'. preced th' (e # t @ s)) ` threads (t @ s)"
-            proof -
-              from h1 have "?f1 th' \<in> ?f1 ` ?B" by auto
-              moreover from h[OF h1] have "?f1 th' = ?f2 th'" by simp
-              ultimately show ?thesis by simp
-            qed
-          qed
-        qed
-        with Cons show ?thesis by auto
+                (\<lambda>th'. preced th' (t @ s)) ` threads (t @ s)" 
+        by (intro f_image_eq, insert thread_not_in, auto simp:Create preced_def)
+        with Cons show ?thesis by (auto simp:the_preced_def)
       qed
       moreover have "?f thread < ?t"
       proof -
-        from Cons have "extend_highest_gen s th prio tm (e # t)" by auto
-        from extend_highest_gen.create_low[OF this] and eq_e
+        from h_e.create_low and Create
         have "prio' \<le> prio" by auto
         thus ?thesis
-        by (unfold preced_th, unfold eq_e, insert lt_tm, 
-          auto simp:preced_def precedence_less_def preced_th)
+        by (unfold preced_th, unfold Create, insert lt_tm, 
+          auto simp:preced_def precedence_less_def preced_th the_preced_def)
+     qed
+     ultimately show ?thesis by (auto simp:max_def)
     qed
-    ultimately show ?thesis by (auto simp:max_def)
-  qed
-next
+  next 
     case (Exit thread)
-    assume eq_e: "e = Exit thread"
-    from Cons have vt_e: "vt (e#(t @ s))" by auto
-    from Cons and eq_e have stp: "step (t@s) (Exit thread)" by auto
-    from stp have thread_ts: "thread \<in> threads (t @ s)"
-      by(cases, unfold runing_def readys_def, auto)
-    from Cons have "extend_highest_gen s th prio tm (e # t)" by auto
-    from extend_highest_gen.exit_diff[OF this] and eq_e
-    have neq_thread: "thread \<noteq> th" by auto
-    from Cons have "extend_highest_gen s th prio tm t" by auto
-    from extend_highest_gen.th_kept[OF this]
-    have h': "th \<in> threads (t @ s) \<and> preced th (t @ s) = preced th s" .
-    show ?thesis (is "Max (?f ` ?A) = ?t")
+    show ?thesis
     proof -
-      have "threads (t@s) = insert thread ?A"
-        by (insert stp thread_ts, unfold eq_e, auto)
-      hence "Max (?f ` (threads (t@s))) = Max (?f ` \<dots>)" by simp
-      also from this have "\<dots> = Max (insert (?f thread) (?f ` ?A))" by simp
-      also have "\<dots> = max (?f thread) (Max (?f ` ?A))"
-      proof(rule Max_insert)
-        from finite_threads [OF vt_e]
-        show "finite (?f ` ?A)" by simp
+      have "Max (the_preced (t @ s) ` (threads (t @ s) - {thread})) = 
+            Max (the_preced (t @ s) ` (threads (t @ s)))"
+      proof(rule Max_remove_less)
+        show "th \<noteq> thread" using Exit h_e.exit_diff by auto 
+      next
+        from Cons(2)[unfolded Exit]
+        show "thread \<in> threads (t @ s)" 
+          by (cases, simp add: readys_def runing_def)
       next
-        from Cons have "extend_highest_gen s th prio tm (e # t)" by auto
-        from extend_highest_gen.th_kept[OF this]
-        show "?f ` ?A \<noteq> {}" by  auto
-      qed
-      finally have "Max (?f ` (threads (t@s))) = max (?f thread) (Max (?f ` ?A))" .
-      moreover have "Max (?f ` (threads (t@s))) = ?t"
-      proof -
-        from Cons show ?thesis
-          by (unfold eq_e, auto simp:preced_def)
+        show "finite (threads (t @ s))" by (simp add: finite_threads h_t.vt_t) 
+      next
+        show "th \<in> threads (t @ s)" by (simp add: h_t.th_kept) 
+      next
+        show "inj_on (the_preced (t @ s)) (threads (t @ s))" by (simp add: inj_the_preced) 
+      next
+        show "the_preced (t @ s) th = Max (the_preced (t @ s) ` threads (t @ s))"
+            by (simp add: Cons.hyps(5) h_t.th_kept the_preced_def)
       qed
-      ultimately have "max (?f thread) (Max (?f ` ?A)) = ?t" by simp
-      moreover have "?f thread < ?t"
-      proof(unfold eq_e, simp add:preced_def, fold preced_def)
-        show "preced thread (t @ s) < ?t"
-        proof -
-          have "preced thread (t @ s) \<le> ?t" 
-          proof -
-            from Cons
-            have "?t = Max ((\<lambda>th'. preced th' (t @ s)) ` threads (t @ s))" 
-              (is "?t = Max (?g ` ?B)") by simp
-            moreover have "?g thread \<le> \<dots>"
-            proof(rule Max_ge)
-              have "vt (t@s)" by fact
-              from finite_threads [OF this]
-              show "finite (?g ` ?B)" by simp
-            next
-              from thread_ts
-              show "?g thread \<in> (?g ` ?B)" by auto
-            qed
-            ultimately show ?thesis by auto
-          qed
-          moreover have "preced thread (t @ s) \<noteq> ?t"
-          proof
-            assume "preced thread (t @ s) = preced th s"
-            with h' have "preced thread (t @ s) = preced th (t@s)" by simp
-            from preced_unique [OF this] have "thread = th"
-            proof
-              from h' show "th \<in> threads (t @ s)" by simp
-            next
-              from thread_ts show "thread \<in> threads (t @ s)" .
-            qed(simp)
-            with neq_thread show "False" by simp
-          qed
-          ultimately show ?thesis by auto
-        qed
-      qed
-      ultimately show ?thesis 
-        by (auto simp:max_def split:if_splits)
+      from this[unfolded Cons(5)]
+      have "Max (the_preced (t @ s) ` (threads (t @ s) - {thread})) = preced th s" .
+      moreover have "the_preced ((e # t) @ s) = the_preced (t@s)"
+                             by (auto simp:Exit the_preced_def preced_def)
+      ultimately show ?thesis by (simp add:Exit)
     qed
   next
     case (P thread cs)
     with Cons
-    show ?thesis by (auto simp:preced_def)
+    show ?thesis by (auto simp:preced_def the_preced_def)
   next
     case (V thread cs)
     with Cons
-    show ?thesis by (auto simp:preced_def)
-  next
+    show ?thesis by (auto simp:preced_def the_preced_def)
+  next (* ccc *)
     case (Set thread prio')
-    show ?thesis (is "Max (?f ` ?A) = ?t")
+    show ?thesis
+    apply (unfold Set, simp, insert Cons(5)) (* ccc *)
+    find_theorems priority Set
+    find_theorems preced Set
     proof -
       let ?B = "threads (t@s)"
       from Cons have "extend_highest_gen s th prio tm (e # t)" by auto
@@ -964,8 +912,6 @@
 apply(auto simp add: detached_eq[OF vt_s])
 done
 
-
-
 lemma live: "runing (t@s) \<noteq> {}"
 proof(cases "th \<in> runing (t@s)")
   case True thus ?thesis by auto
diff -r f8194fd6214f -r 031d2ae9c9b8 PrioG.thy
--- a/PrioG.thy	Fri Dec 18 22:47:32 2015 +0800
+++ b/PrioG.thy	Tue Dec 22 23:13:31 2015 +0800
@@ -2923,6 +2923,5 @@
   shows "th1 = th2"
 using assms by (unfold next_th_def, auto)
 
-
  
 end
diff -r f8194fd6214f -r 031d2ae9c9b8 PrioG.thy~
--- a/PrioG.thy~	Fri Dec 18 22:47:32 2015 +0800
+++ b/PrioG.thy~	Tue Dec 22 23:13:31 2015 +0800
@@ -2914,4 +2914,15 @@
   from the concise and miniature model of PIP given in PrioGDef.thy.
 *}
 
+lemma eq_dependants: "dependants (wq s) = dependants s"
+  by (simp add: s_dependants_abv wq_def)
+
+lemma next_th_unique: 
+  assumes nt1: "next_th s th cs th1"
+  and nt2: "next_th s th cs th2"
+  shows "th1 = th2"
+using assms by (unfold next_th_def, auto)
+
+
+ 
 end
diff -r f8194fd6214f -r 031d2ae9c9b8 RTree.thy
--- a/RTree.thy	Fri Dec 18 22:47:32 2015 +0800
+++ b/RTree.thy	Tue Dec 22 23:13:31 2015 +0800
@@ -128,6 +128,21 @@
 locale fbranch =
   fixes r
   assumes fb: "\<forall> x \<in> Range r . finite (children r x)"
+begin
+
+lemma finite_children: "finite (children r x)"
+proof(cases "children r x = {}")
+  case True
+  thus ?thesis by auto
+next
+  case False
+  then obtain y where "(y, x) \<in> r" by (auto simp:children_def)
+  hence "x \<in> Range r" by auto
+  from fb[rule_format, OF this]
+  show ?thesis .
+qed
+
+end
 
 locale fsubtree = fbranch + 
    assumes wf: "wf r"