[STATEMENT]
lemma merge_ffold_fsts_in_childverts:
  "\<lbrakk>list_dtree (Node r xs); y \<in> fst ` set (ffold (merge_f r xs) [] xs)\<rbrakk>
    \<Longrightarrow> \<exists>t1 \<in> fst `  fset xs. y \<in> dverts t1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>list_dtree (Node r xs); y \<in> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset xs \<and> list_dtree (Node r xs) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs)\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset xs. y \<in> dverts t1
[PROOF STEP]
proof(induction xs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>list_dtree (Node r {||}); y \<in> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset {||} \<and> list_dtree (Node r {||}) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] {||})\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset {||}. y \<in> dverts t1
 2. \<And>x xs. \<lbrakk>x |\<notin>| xs; \<lbrakk>list_dtree (Node r xs); y \<in> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset xs \<and> list_dtree (Node r xs) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs)\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset xs. y \<in> dverts t1; list_dtree (Node r (finsert x xs)); y \<in> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x xs)) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] (finsert x xs))\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset (finsert x xs). y \<in> dverts t1
[PROOF STEP]
case (insert x xs)
[PROOF STATE]
proof (state)
this:
x |\<notin>| xs
\<lbrakk>list_dtree (Node r xs); y \<in> fst ` set (ffold (\<lambda>a. case a of (t, e) \<Rightarrow> \<lambda>b. if (t, e) \<in> fset xs \<and> list_dtree (Node r xs) \<and> (\<forall>a\<in>set b. case a of (v, e') \<Rightarrow> set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs)\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset xs. y \<in> dverts t1
list_dtree (Node r (finsert x xs))
y \<in> fst ` set (ffold (\<lambda>a. case a of (t, e) \<Rightarrow> \<lambda>b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x xs)) \<and> (\<forall>a\<in>set b. case a of (v, e') \<Rightarrow> set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] (finsert x xs))

goal (2 subgoals):
 1. \<lbrakk>list_dtree (Node r {||}); y \<in> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset {||} \<and> list_dtree (Node r {||}) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] {||})\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset {||}. y \<in> dverts t1
 2. \<And>x xs. \<lbrakk>x |\<notin>| xs; \<lbrakk>list_dtree (Node r xs); y \<in> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset xs \<and> list_dtree (Node r xs) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs)\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset xs. y \<in> dverts t1; list_dtree (Node r (finsert x xs)); y \<in> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x xs)) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] (finsert x xs))\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset (finsert x xs). y \<in> dverts t1
[PROOF STEP]
obtain t1 e1 where t1_def[simp]: "x = (t1,e1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>t1 e1. x = (t1, e1) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
x = (t1, e1)

goal (2 subgoals):
 1. \<lbrakk>list_dtree (Node r {||}); y \<in> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset {||} \<and> list_dtree (Node r {||}) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] {||})\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset {||}. y \<in> dverts t1
 2. \<And>x xs. \<lbrakk>x |\<notin>| xs; \<lbrakk>list_dtree (Node r xs); y \<in> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset xs \<and> list_dtree (Node r xs) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs)\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset xs. y \<in> dverts t1; list_dtree (Node r (finsert x xs)); y \<in> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x xs)) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] (finsert x xs))\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset (finsert x xs). y \<in> dverts t1
[PROOF STEP]
let ?f = "merge_f r (finsert x xs)"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>list_dtree (Node r {||}); y \<in> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset {||} \<and> list_dtree (Node r {||}) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] {||})\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset {||}. y \<in> dverts t1
 2. \<And>x xs. \<lbrakk>x |\<notin>| xs; \<lbrakk>list_dtree (Node r xs); y \<in> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset xs \<and> list_dtree (Node r xs) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs)\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset xs. y \<in> dverts t1; list_dtree (Node r (finsert x xs)); y \<in> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x xs)) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] (finsert x xs))\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset (finsert x xs). y \<in> dverts t1
[PROOF STEP]
let ?f' = "merge_f r xs"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>list_dtree (Node r {||}); y \<in> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset {||} \<and> list_dtree (Node r {||}) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] {||})\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset {||}. y \<in> dverts t1
 2. \<And>x xs. \<lbrakk>x |\<notin>| xs; \<lbrakk>list_dtree (Node r xs); y \<in> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset xs \<and> list_dtree (Node r xs) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs)\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset xs. y \<in> dverts t1; list_dtree (Node r (finsert x xs)); y \<in> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x xs)) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] (finsert x xs))\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset (finsert x xs). y \<in> dverts t1
[PROOF STEP]
have "(t1, e1) \<in> fset (finsert x xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (t1, e1) \<in> fset (finsert x xs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(t1, e1) \<in> fset (finsert x xs)

goal (2 subgoals):
 1. \<lbrakk>list_dtree (Node r {||}); y \<in> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset {||} \<and> list_dtree (Node r {||}) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] {||})\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset {||}. y \<in> dverts t1
 2. \<And>x xs. \<lbrakk>x |\<notin>| xs; \<lbrakk>list_dtree (Node r xs); y \<in> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset xs \<and> list_dtree (Node r xs) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs)\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset xs. y \<in> dverts t1; list_dtree (Node r (finsert x xs)); y \<in> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x xs)) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] (finsert x xs))\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset (finsert x xs). y \<in> dverts t1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(t1, e1) \<in> fset (finsert x xs)

goal (2 subgoals):
 1. \<lbrakk>list_dtree (Node r {||}); y \<in> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset {||} \<and> list_dtree (Node r {||}) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] {||})\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset {||}. y \<in> dverts t1
 2. \<And>x xs. \<lbrakk>x |\<notin>| xs; \<lbrakk>list_dtree (Node r xs); y \<in> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset xs \<and> list_dtree (Node r xs) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs)\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset xs. y \<in> dverts t1; list_dtree (Node r (finsert x xs)); y \<in> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x xs)) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] (finsert x xs))\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset (finsert x xs). y \<in> dverts t1
[PROOF STEP]
have "(t1, e1) \<notin> fset xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (t1, e1) \<notin> fset xs
[PROOF STEP]
using insert.hyps notin_fset
[PROOF STATE]
proof (prove)
using this:
x |\<notin>| xs
(?x |\<notin>| ?S) = (?x \<notin> fset ?S)

goal (1 subgoal):
 1. (t1, e1) \<notin> fset xs
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(t1, e1) \<notin> fset xs

goal (2 subgoals):
 1. \<lbrakk>list_dtree (Node r {||}); y \<in> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset {||} \<and> list_dtree (Node r {||}) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] {||})\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset {||}. y \<in> dverts t1
 2. \<And>x xs. \<lbrakk>x |\<notin>| xs; \<lbrakk>list_dtree (Node r xs); y \<in> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset xs \<and> list_dtree (Node r xs) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs)\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset xs. y \<in> dverts t1; list_dtree (Node r (finsert x xs)); y \<in> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x xs)) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] (finsert x xs))\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset (finsert x xs). y \<in> dverts t1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(t1, e1) \<in> fset (finsert x xs)
(t1, e1) \<notin> fset xs
[PROOF STEP]
have xs_val:
    "(\<forall>(v,e) \<in> set (ffold ?f' [] xs). set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1})"
[PROOF STATE]
proof (prove)
using this:
(t1, e1) \<in> fset (finsert x xs)
(t1, e1) \<notin> fset xs

goal (1 subgoal):
 1. \<forall>(v, e)\<in>set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset xs \<and> list_dtree (Node r xs) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs). set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
[PROOF STEP]
using merge_ffold_empty_inter_preserv'[OF insert.prems(1) empty_list_valid_merge]
[PROOF STATE]
proof (prove)
using this:
(t1, e1) \<in> fset (finsert x xs)
(t1, e1) \<notin> fset xs
\<lbrakk>(?t1.0, ?e1.0) \<in> fset (finsert x xs); (?t1.0, ?e1.0) \<notin> fset xs; (?v, ?e) \<in> set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset xs \<and> list_dtree (Node r xs) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs)\<rbrakk> \<Longrightarrow> set ?v \<inter> dlverts ?t1.0 = {} \<and> ?v \<noteq> [] \<and> ?e \<notin> darcs ?t1.0 \<union> {?e1.0}

goal (1 subgoal):
 1. \<forall>(v, e)\<in>set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset xs \<and> list_dtree (Node r xs) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs). set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>(v, e)\<in>set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset xs \<and> list_dtree (Node r xs) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs). set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}

goal (2 subgoals):
 1. \<lbrakk>list_dtree (Node r {||}); y \<in> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset {||} \<and> list_dtree (Node r {||}) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] {||})\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset {||}. y \<in> dverts t1
 2. \<And>x xs. \<lbrakk>x |\<notin>| xs; \<lbrakk>list_dtree (Node r xs); y \<in> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset xs \<and> list_dtree (Node r xs) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs)\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset xs. y \<in> dverts t1; list_dtree (Node r (finsert x xs)); y \<in> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x xs)) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] (finsert x xs))\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset (finsert x xs). y \<in> dverts t1
[PROOF STEP]
have 0: "list_dtree (Node r xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_dtree (Node r xs)
[PROOF STEP]
using list_dtree_subset insert.prems(1)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?xs |\<subseteq>| ?ys; list_dtree (Node ?r ?ys)\<rbrakk> \<Longrightarrow> list_dtree (Node ?r ?xs)
list_dtree (Node r (finsert x xs))

goal (1 subgoal):
 1. list_dtree (Node r xs)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
list_dtree (Node r xs)

goal (2 subgoals):
 1. \<lbrakk>list_dtree (Node r {||}); y \<in> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset {||} \<and> list_dtree (Node r {||}) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] {||})\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset {||}. y \<in> dverts t1
 2. \<And>x xs. \<lbrakk>x |\<notin>| xs; \<lbrakk>list_dtree (Node r xs); y \<in> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset xs \<and> list_dtree (Node r xs) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs)\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset xs. y \<in> dverts t1; list_dtree (Node r (finsert x xs)); y \<in> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x xs)) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] (finsert x xs))\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset (finsert x xs). y \<in> dverts t1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
list_dtree (Node r xs)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
list_dtree (Node r xs)

goal (1 subgoal):
 1. \<exists>t1\<in>fst ` fset (finsert x xs). y \<in> dverts t1
[PROOF STEP]
proof(cases "y \<in> fst ` set (ffold (merge_f r xs) [] xs)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>list_dtree (Node r xs); y \<in> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset xs \<and> list_dtree (Node r xs) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs)\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset (finsert x xs). y \<in> dverts t1
 2. \<lbrakk>list_dtree (Node r xs); y \<notin> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset xs \<and> list_dtree (Node r xs) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs)\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset (finsert x xs). y \<in> dverts t1
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
y \<in> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset xs \<and> list_dtree (Node r xs) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs)

goal (2 subgoals):
 1. \<lbrakk>list_dtree (Node r xs); y \<in> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset xs \<and> list_dtree (Node r xs) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs)\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset (finsert x xs). y \<in> dverts t1
 2. \<lbrakk>list_dtree (Node r xs); y \<notin> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset xs \<and> list_dtree (Node r xs) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs)\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset (finsert x xs). y \<in> dverts t1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y \<in> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset xs \<and> list_dtree (Node r xs) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
y \<in> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset xs \<and> list_dtree (Node r xs) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs)

goal (1 subgoal):
 1. \<exists>t1\<in>fst ` fset (finsert x xs). y \<in> dverts t1
[PROOF STEP]
using insert.IH[OF 0]
[PROOF STATE]
proof (prove)
using this:
y \<in> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset xs \<and> list_dtree (Node r xs) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs)
y \<in> fst ` set (ffold (\<lambda>a. case a of (t, e) \<Rightarrow> \<lambda>b. if (t, e) \<in> fset xs \<and> list_dtree (Node r xs) \<and> (\<forall>a\<in>set b. case a of (v, e') \<Rightarrow> set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs) \<Longrightarrow> \<exists>t1\<in>fst ` fset xs. y \<in> dverts t1

goal (1 subgoal):
 1. \<exists>t1\<in>fst ` fset (finsert x xs). y \<in> dverts t1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>t1\<in>fst ` fset (finsert x xs). y \<in> dverts t1

goal (1 subgoal):
 1. \<lbrakk>list_dtree (Node r xs); y \<notin> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset xs \<and> list_dtree (Node r xs) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs)\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset (finsert x xs). y \<in> dverts t1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>list_dtree (Node r xs); y \<notin> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset xs \<and> list_dtree (Node r xs) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs)\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset (finsert x xs). y \<in> dverts t1
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
y \<notin> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset xs \<and> list_dtree (Node r xs) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs)

goal (1 subgoal):
 1. \<lbrakk>list_dtree (Node r xs); y \<notin> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset xs \<and> list_dtree (Node r xs) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs)\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset (finsert x xs). y \<in> dverts t1
[PROOF STEP]
have "ffold ?f [] (finsert x xs) = ?f x (ffold ?f [] xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x xs)) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] (finsert x xs) = (case x of (t, e) \<Rightarrow> \<lambda>b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x xs)) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x xs)) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs)
[PROOF STEP]
using Comm.ffold_finsert[OF insert.hyps]
[PROOF STATE]
proof (prove)
using this:
ffold (\<lambda>(t, e) b. if (t, e) \<in> fset ?xs \<and> list_dtree (Node ?r ?xs) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node ?r {|(t, e)|})) b else b) ?z (finsert x xs) = (case x of (t, e) \<Rightarrow> \<lambda>b. if (t, e) \<in> fset ?xs \<and> list_dtree (Node ?r ?xs) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node ?r {|(t, e)|})) b else b) (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset ?xs \<and> list_dtree (Node ?r ?xs) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node ?r {|(t, e)|})) b else b) ?z xs)

goal (1 subgoal):
 1. ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x xs)) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] (finsert x xs) = (case x of (t, e) \<Rightarrow> \<lambda>b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x xs)) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x xs)) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x xs)) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] (finsert x xs) = (case x of (t, e) \<Rightarrow> \<lambda>b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x xs)) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x xs)) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs)

goal (1 subgoal):
 1. \<lbrakk>list_dtree (Node r xs); y \<notin> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset xs \<and> list_dtree (Node r xs) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs)\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset (finsert x xs). y \<in> dverts t1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x xs)) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] (finsert x xs) = (case x of (t, e) \<Rightarrow> \<lambda>b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x xs)) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x xs)) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs)

goal (1 subgoal):
 1. \<lbrakk>list_dtree (Node r xs); y \<notin> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset xs \<and> list_dtree (Node r xs) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs)\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset (finsert x xs). y \<in> dverts t1
[PROOF STEP]
have "\<dots> = ?f x (ffold ?f' [] xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case x of (t, e) \<Rightarrow> \<lambda>b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x xs)) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x xs)) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs) = (case x of (t, e) \<Rightarrow> \<lambda>b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x xs)) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset xs \<and> list_dtree (Node r xs) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs)
[PROOF STEP]
using merge_ffold_supset[of xs "finsert x xs" r "[]"] insert.prems(1)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>xs |\<subseteq>| finsert x xs; list_dtree (Node r (finsert x xs))\<rbrakk> \<Longrightarrow> ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x xs)) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs = ffold (\<lambda>(t, e) b. if (t, e) \<in> fset xs \<and> list_dtree (Node r xs) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs
list_dtree (Node r (finsert x xs))

goal (1 subgoal):
 1. (case x of (t, e) \<Rightarrow> \<lambda>b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x xs)) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x xs)) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs) = (case x of (t, e) \<Rightarrow> \<lambda>b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x xs)) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset xs \<and> list_dtree (Node r xs) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(case x of (t, e) \<Rightarrow> \<lambda>b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x xs)) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x xs)) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs) = (case x of (t, e) \<Rightarrow> \<lambda>b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x xs)) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset xs \<and> list_dtree (Node r xs) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs)

goal (1 subgoal):
 1. \<lbrakk>list_dtree (Node r xs); y \<notin> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset xs \<and> list_dtree (Node r xs) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs)\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset (finsert x xs). y \<in> dverts t1
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x xs)) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] (finsert x xs) = (case x of (t, e) \<Rightarrow> \<lambda>b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x xs)) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset xs \<and> list_dtree (Node r xs) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs)
[PROOF STEP]
have "ffold ?f [] (finsert x xs)
                = Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|x|})) (ffold ?f' [] xs)"
[PROOF STATE]
proof (prove)
using this:
ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x xs)) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] (finsert x xs) = (case x of (t, e) \<Rightarrow> \<lambda>b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x xs)) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset xs \<and> list_dtree (Node r xs) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs)

goal (1 subgoal):
 1. ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x xs)) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] (finsert x xs) = Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|x|})) (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset xs \<and> list_dtree (Node r xs) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs)
[PROOF STEP]
using xs_val insert.prems
[PROOF STATE]
proof (prove)
using this:
ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x xs)) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] (finsert x xs) = (case x of (t, e) \<Rightarrow> \<lambda>b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x xs)) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset xs \<and> list_dtree (Node r xs) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs)
\<forall>(v, e)\<in>set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset xs \<and> list_dtree (Node r xs) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs). set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
list_dtree (Node r (finsert x xs))
y \<in> fst ` set (ffold (\<lambda>a. case a of (t, e) \<Rightarrow> \<lambda>b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x xs)) \<and> (\<forall>a\<in>set b. case a of (v, e') \<Rightarrow> set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] (finsert x xs))

goal (1 subgoal):
 1. ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x xs)) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] (finsert x xs) = Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|x|})) (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset xs \<and> list_dtree (Node r xs) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x xs)) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] (finsert x xs) = Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|x|})) (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset xs \<and> list_dtree (Node r xs) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs)

goal (1 subgoal):
 1. \<lbrakk>list_dtree (Node r xs); y \<notin> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset xs \<and> list_dtree (Node r xs) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs)\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset (finsert x xs). y \<in> dverts t1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x xs)) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] (finsert x xs) = Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|x|})) (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset xs \<and> list_dtree (Node r xs) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs)
[PROOF STEP]
have "set (ffold ?f [] (finsert x xs))
          = set (Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|x|})) (ffold ?f' [] xs))"
[PROOF STATE]
proof (prove)
using this:
ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x xs)) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] (finsert x xs) = Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|x|})) (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset xs \<and> list_dtree (Node r xs) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs)

goal (1 subgoal):
 1. set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x xs)) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] (finsert x xs)) = set (Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|x|})) (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset xs \<and> list_dtree (Node r xs) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs))
[PROOF STEP]
by argo
[PROOF STATE]
proof (state)
this:
set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x xs)) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] (finsert x xs)) = set (Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|x|})) (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset xs \<and> list_dtree (Node r xs) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs))

goal (1 subgoal):
 1. \<lbrakk>list_dtree (Node r xs); y \<notin> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset xs \<and> list_dtree (Node r xs) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs)\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset (finsert x xs). y \<in> dverts t1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x xs)) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] (finsert x xs)) = set (Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|x|})) (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset xs \<and> list_dtree (Node r xs) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs))
[PROOF STEP]
have "set (ffold ?f [] (finsert x xs))
          = (set (dtree_to_list (Node r {|x|})) \<union> set (ffold ?f' [] xs))"
[PROOF STATE]
proof (prove)
using this:
set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x xs)) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] (finsert x xs)) = set (Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|x|})) (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset xs \<and> list_dtree (Node r xs) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs))

goal (1 subgoal):
 1. set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x xs)) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] (finsert x xs)) = set (dtree_to_list (Node r {|x|})) \<union> set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset xs \<and> list_dtree (Node r xs) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs)
[PROOF STEP]
using set_merge
[PROOF STATE]
proof (prove)
using this:
set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x xs)) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] (finsert x xs)) = set (Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|x|})) (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset xs \<and> list_dtree (Node r xs) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs))
set ?xs \<union> set ?ys = set (Sorting_Algorithms.merge ?cmp ?xs ?ys)

goal (1 subgoal):
 1. set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x xs)) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] (finsert x xs)) = set (dtree_to_list (Node r {|x|})) \<union> set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset xs \<and> list_dtree (Node r xs) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs)
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x xs)) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] (finsert x xs)) = set (dtree_to_list (Node r {|x|})) \<union> set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset xs \<and> list_dtree (Node r xs) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs)

goal (1 subgoal):
 1. \<lbrakk>list_dtree (Node r xs); y \<notin> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset xs \<and> list_dtree (Node r xs) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs)\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset (finsert x xs). y \<in> dverts t1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x xs)) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] (finsert x xs)) = set (dtree_to_list (Node r {|x|})) \<union> set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset xs \<and> list_dtree (Node r xs) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs)
[PROOF STEP]
have "y \<in> fst ` set (dtree_to_list (Node r {|x|}))"
[PROOF STATE]
proof (prove)
using this:
set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x xs)) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] (finsert x xs)) = set (dtree_to_list (Node r {|x|})) \<union> set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset xs \<and> list_dtree (Node r xs) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs)

goal (1 subgoal):
 1. y \<in> fst ` set (dtree_to_list (Node r {|x|}))
[PROOF STEP]
using False insert.prems
[PROOF STATE]
proof (prove)
using this:
set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x xs)) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] (finsert x xs)) = set (dtree_to_list (Node r {|x|})) \<union> set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset xs \<and> list_dtree (Node r xs) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs)
y \<notin> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset xs \<and> list_dtree (Node r xs) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs)
list_dtree (Node r (finsert x xs))
y \<in> fst ` set (ffold (\<lambda>a. case a of (t, e) \<Rightarrow> \<lambda>b. if (t, e) \<in> fset (finsert x xs) \<and> list_dtree (Node r (finsert x xs)) \<and> (\<forall>a\<in>set b. case a of (v, e') \<Rightarrow> set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] (finsert x xs))

goal (1 subgoal):
 1. y \<in> fst ` set (dtree_to_list (Node r {|x|}))
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
y \<in> fst ` set (dtree_to_list (Node r {|x|}))

goal (1 subgoal):
 1. \<lbrakk>list_dtree (Node r xs); y \<notin> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset xs \<and> list_dtree (Node r xs) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] xs)\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset (finsert x xs). y \<in> dverts t1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y \<in> fst ` set (dtree_to_list (Node r {|x|}))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
y \<in> fst ` set (dtree_to_list (Node r {|x|}))

goal (1 subgoal):
 1. \<exists>t1\<in>fst ` fset (finsert x xs). y \<in> dverts t1
[PROOF STEP]
by (simp add: dtree_to_list_x_in_dverts)
[PROOF STATE]
proof (state)
this:
\<exists>t1\<in>fst ` fset (finsert x xs). y \<in> dverts t1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>t1\<in>fst ` fset (finsert x xs). y \<in> dverts t1

goal (1 subgoal):
 1. \<lbrakk>list_dtree (Node r {||}); y \<in> fst ` set (ffold (\<lambda>(t, e) b. if (t, e) \<in> fset {||} \<and> list_dtree (Node r {||}) \<and> (\<forall>(v, e')\<in>set b. set v \<inter> dlverts t = {} \<and> v \<noteq> [] \<and> e' \<notin> darcs t \<union> {e}) then Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t, e)|})) b else b) [] {||})\<rbrakk> \<Longrightarrow> \<exists>t1\<in>fst ` fset {||}. y \<in> dverts t1
[PROOF STEP]
qed (simp)