diff -r ad57323fd4d6 -r 0a069a667301 CpsG.thy~
--- a/CpsG.thy~	Tue Dec 15 21:45:46 2015 +0800
+++ b/CpsG.thy~	Tue Dec 15 15:10:40 2015 +0000
@@ -1843,7 +1843,7 @@
     also have "... = 
           Max ({the_preced s' th2} \<union> cp_gen s' ` RTree.children (tRAG s') x)"
     proof -
-      have "the_preced s th2 = the_preced s' th2" sorry
+      from preced_kept have "the_preced s th2 = the_preced s' th2" by simp
       moreover have "cp_gen s ` RTree.children (tRAG s) x =
                      cp_gen s' ` RTree.children (tRAG s') x"
       proof -
@@ -1871,52 +1871,58 @@
         qed
         moreover have "cp_gen s ` RTree.children (tRAG s) x =
                        cp_gen s' ` RTree.children (tRAG s) x" (is "?f ` ?A = ?g ` ?A")
-        proof -
-          have h: "?A = ({y. y \<in> ?A \<and> y \<in> ancestors (tRAG s) u} \<union> 
-                      {y. y \<in> ?A \<and> \<not> (y \<in> ancestors (tRAG s) u)})" (is "_ = ?B \<union> ?C")
-             by (rule set_prop_split)
-          show ?thesis
-          proof(subst h, subst (3) h, rule f_image_union_eq)
-            show "?f ` ?B = ?g ` ?B"
-            proof(rule f_image_eq)
-              fix a
-              assume "a \<in> ?B"
-              hence h: "a \<in>  RTree.children (tRAG s) x" "a \<in> ancestors (tRAG s) u" by auto
-              show "?f a = ?g a"
-              proof(rule 1(1)[rule_format])
-                from h(2) show "a \<in> ancestors (tRAG s) u" .
-              next
-                from h(1) show "(a, x) \<in> tRAG s"
-                  unfolding RTree.children_def by auto
-              qed
-            qed
+        proof(rule f_image_eq)
+          fix a
+          assume a_in: "a \<in> ?A"
+          from 1(2)
+          show "?f a = ?g a"
+          proof(cases rule:vat_s.rtree_s.ancestors_childrenE[case_names in_ch out_ch])
+             case in_ch
+             show ?thesis
+             proof(cases "a = u")
+                case True
+                from assms(2)[folded this] show ?thesis .
+             next
+                case False
+                have a_not_in: "a \<notin> ancestors (tRAG s) (Th th)"
+                proof
+                  assume a_in': "a \<in> ancestors (tRAG s) (Th th)"
+                  have "a = u"
+                  proof(rule vat_s.rtree_s.ancestors_children_unique)
+                    from a_in' a_in show "a \<in> ancestors (tRAG s) (Th th) \<inter> 
+                                          RTree.children (tRAG s) x" by auto
+                  next 
+                    from assms(1) in_ch show "u \<in> ancestors (tRAG s) (Th th) \<inter> 
+                                      RTree.children (tRAG s) x" by auto
+                  qed
+                  with False show False by simp
+                qed
+                from a_in obtain th_a where eq_a: "a = Th th_a" 
+                    by (unfold RTree.children_def tRAG_alt_def, auto)
+                from cp_kept[OF a_not_in[unfolded eq_a]]
+                have "cp s th_a = cp s' th_a" .
+                from this [unfolded cp_gen_def_cond[OF eq_a], folded eq_a]
+                show ?thesis .
+             qed
           next
-            show "?f ` ?C = ?g ` ?C"
-            proof(rule f_image_eq)
-              fix a
-              assume "a \<in> ?C"
-              hence h: "a \<in> RTree.children (tRAG s) x" "a \<notin> ancestors (tRAG s) u" by auto
-              from h(1) obtain th3 where eq_a: "a = Th th3"
-                by (unfold RTree.children_def tRAG_alt_def, auto)
-              thm cp_gen_def_cond[OF eq_a, folded eq_a]
-              show "?f a = ?g a"
-              proof(fold cp_gen_def_cond[OF eq_a, folded eq_a], rule cp_kept)
-                show "Th th3 \<notin> ancestors (tRAG s) (Th th)"
-                proof
-                  assume "Th th3 \<in> ancestors (tRAG s) (Th th)"
-                  from this[folded eq_a] have "(Th th, a) \<in> (tRAG s)^+" by (auto simp:ancestors_def)
-                  from plus_rpath[OF this] obtain xs1
-                  where h_a: "rpath (tRAG s) (Th th) xs1 a"  "xs1 \<noteq> []" by auto
-                  from assms(1) have "(Th th, u) \<in> (tRAG s)^+" by (auto simp:ancestors_def)
-                  from plus_rpath[OF this] obtain xs2
-                  where h_u: "rpath (tRAG s) (Th th) xs2 u"  "xs2 \<noteq> []" by auto
-                  show False
-                  proof(cases rule:vat_s.rtree_s.rpath_overlap[OF h_a(1) h_u(1)])
-                     case (1 xs3)
-                     (* ccc *)
-                  qed
-                qed
-             qed
+            case (out_ch z)
+            hence h: "z \<in> ancestors (tRAG s) u" "z \<in> RTree.children (tRAG s) x" by auto
+            show ?thesis
+            proof(cases "a = z")
+              case True
+              from h(2) have zx_in: "(z, x) \<in> (tRAG s)" by (auto simp:RTree.children_def)
+              from 1(1)[rule_format, OF this h(1)]
+              have eq_cp_gen: "cp_gen s z = cp_gen s' z" .
+              with True show ?thesis by metis
+            next
+              case False
+              from a_in obtain th_a where eq_a: "a = Th th_a"
+                by (auto simp:RTree.children_def tRAG_alt_def)
+              have "a \<notin> ancestors (tRAG s) (Th th)" sorry
+              from cp_kept[OF this[unfolded eq_a]]
+              have "cp s th_a = cp s' th_a" .
+              from this[unfolded cp_gen_def_cond[OF eq_a], folded eq_a]
+              show ?thesis .
             qed
           qed
         qed