1846       have "the_preced s th2 = the_preced s' th2" sorry

  1846       from preced_kept have "the_preced s th2 = the_preced s' th2" by simp

  1874         proof -

  1874         proof(rule f_image_eq)

  1875           have h: "?A = ({y. y \<in> ?A \<and> y \<in> ancestors (tRAG s) u} \<union> 

  1875           fix a

  1876                       {y. y \<in> ?A \<and> \<not> (y \<in> ancestors (tRAG s) u)})" (is "_ = ?B \<union> ?C")

  1876           assume a_in: "a \<in> ?A"

  1877              by (rule set_prop_split)

  1877           from 1(2)

  1878           show ?thesis

  1878           show "?f a = ?g a"

  1879           proof(subst h, subst (3) h, rule f_image_union_eq)

  1879           proof(cases rule:vat_s.rtree_s.ancestors_childrenE[case_names in_ch out_ch])

  1880             show "?f ` ?B = ?g ` ?B"

  1880              case in_ch

  1881             proof(rule f_image_eq)

  1881              show ?thesis

  1882               fix a

  1882              proof(cases "a = u")

  1883               assume "a \<in> ?B"

  1883                 case True

  1884               hence h: "a \<in>  RTree.children (tRAG s) x" "a \<in> ancestors (tRAG s) u" by auto

  1884                 from assms(2)[folded this] show ?thesis .

  1885               show "?f a = ?g a"

  1885              next

  1886               proof(rule 1(1)[rule_format])

  1886                 case False

  1887                 from h(2) show "a \<in> ancestors (tRAG s) u" .

  1887                 have a_not_in: "a \<notin> ancestors (tRAG s) (Th th)"

  1888               next

  1888                 proof

  1889                 from h(1) show "(a, x) \<in> tRAG s"

  1889                   assume a_in': "a \<in> ancestors (tRAG s) (Th th)"

  1890                   unfolding RTree.children_def by auto

  1890                   have "a = u"

  1891               qed

  1891                   proof(rule vat_s.rtree_s.ancestors_children_unique)

  1892             qed

  1892                     from a_in' a_in show "a \<in> ancestors (tRAG s) (Th th) \<inter> 

  1893                                           RTree.children (tRAG s) x" by auto

  1894                   next 

  1895                     from assms(1) in_ch show "u \<in> ancestors (tRAG s) (Th th) \<inter> 

  1896                                       RTree.children (tRAG s) x" by auto

  1897                   qed

  1898                   with False show False by simp

  1899                 qed

  1900                 from a_in obtain th_a where eq_a: "a = Th th_a" 

  1901                     by (unfold RTree.children_def tRAG_alt_def, auto)

  1902                 from cp_kept[OF a_not_in[unfolded eq_a]]

  1903                 have "cp s th_a = cp s' th_a" .

  1904                 from this [unfolded cp_gen_def_cond[OF eq_a], folded eq_a]

  1905                 show ?thesis .

  1906              qed

  1894             show "?f ` ?C = ?g ` ?C"

  1908             case (out_ch z)

  1895             proof(rule f_image_eq)

  1909             hence h: "z \<in> ancestors (tRAG s) u" "z \<in> RTree.children (tRAG s) x" by auto

  1896               fix a

  1910             show ?thesis

  1897               assume "a \<in> ?C"

  1911             proof(cases "a = z")

  1898               hence h: "a \<in> RTree.children (tRAG s) x" "a \<notin> ancestors (tRAG s) u" by auto

  1912               case True

  1899               from h(1) obtain th3 where eq_a: "a = Th th3"

  1913               from h(2) have zx_in: "(z, x) \<in> (tRAG s)" by (auto simp:RTree.children_def)

  1900                 by (unfold RTree.children_def tRAG_alt_def, auto)

  1914               from 1(1)[rule_format, OF this h(1)]

  1901               thm cp_gen_def_cond[OF eq_a, folded eq_a]

  1915               have eq_cp_gen: "cp_gen s z = cp_gen s' z" .

  1902               show "?f a = ?g a"

  1916               with True show ?thesis by metis

  1903               proof(fold cp_gen_def_cond[OF eq_a, folded eq_a], rule cp_kept)

  1917             next

  1904                 show "Th th3 \<notin> ancestors (tRAG s) (Th th)"

  1918               case False

  1905                 proof

  1919               from a_in obtain th_a where eq_a: "a = Th th_a"

  1906                   assume "Th th3 \<in> ancestors (tRAG s) (Th th)"

  1920                 by (auto simp:RTree.children_def tRAG_alt_def)

  1907                   from this[folded eq_a] have "(Th th, a) \<in> (tRAG s)^+" by (auto simp:ancestors_def)

  1921               have "a \<notin> ancestors (tRAG s) (Th th)" sorry

  1908                   from plus_rpath[OF this] obtain xs1

  1922               from cp_kept[OF this[unfolded eq_a]]

  1909                   where h_a: "rpath (tRAG s) (Th th) xs1 a"  "xs1 \<noteq> []" by auto

  1923               have "cp s th_a = cp s' th_a" .

  1910                   from assms(1) have "(Th th, u) \<in> (tRAG s)^+" by (auto simp:ancestors_def)

  1924               from this[unfolded cp_gen_def_cond[OF eq_a], folded eq_a]

  1911                   from plus_rpath[OF this] obtain xs2

  1925               show ?thesis .

  1912                   where h_u: "rpath (tRAG s) (Th th) xs2 u"  "xs2 \<noteq> []" by auto

  1913                   show False

  1914                   proof(cases rule:vat_s.rtree_s.rpath_overlap[OF h_a(1) h_u(1)])

  1915                      case (1 xs3)

  1916                      (* ccc *)

  1917                   qed

  1918                 qed

  1919              qed