[STATEMENT]
lemma merge_ffold_empty_inter_preserv:
  "\<lbrakk>list_dtree (Node r ys); xs |\<subseteq>| ys;
    \<forall>(v,e) \<in> set z. set v \<inter> dlverts t1 = {} \<and> v\<noteq>[] \<and> e \<notin> darcs t1 \<union> {e1};
    (t1,e1) \<in> fset ys; (t1,e1) \<notin> fset xs; (v,e) \<in> set (ffold (merge_f r xs) z xs)\<rbrakk>
      \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>list_dtree (Node r ys); xs |\<subseteq>| ys; \<forall>(v, e)\<in>set z. set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}; (t1, e1) \<in> fset ys; (t1, e1) \<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) z xs)\<rbrakk> \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
[PROOF STEP]
proof(induction xs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>list_dtree (Node r ys); {||} |\<subseteq>| ys; \<forall>(v, e)\<in>set z. set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}; (t1, e1) \<in> fset ys; (t1, e1) \<notin> fset {||}; (v, e) \<in> 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) z {||})\<rbrakk> \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
 2. \<And>x xs. \<lbrakk>x |\<notin>| xs; \<lbrakk>list_dtree (Node r ys); xs |\<subseteq>| ys; \<forall>(v, e)\<in>set z. set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}; (t1, e1) \<in> fset ys; (t1, e1) \<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) z xs)\<rbrakk> \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}; list_dtree (Node r ys); finsert x xs |\<subseteq>| ys; \<forall>(v, e)\<in>set z. set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}; (t1, e1) \<in> fset ys; (t1, e1) \<notin> fset (finsert x xs); (v, e) \<in> 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) z (finsert x xs))\<rbrakk> \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
[PROOF STEP]
case (insert x xs)
[PROOF STATE]
proof (state)
this:
x |\<notin>| xs
\<lbrakk>list_dtree (Node r ys); xs |\<subseteq>| ys; \<forall>a\<in>set z. case a of (v, e) \<Rightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}; (t1, e1) \<in> fset ys; (t1, e1) \<notin> fset xs; (v, e) \<in> 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) z xs)\<rbrakk> \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
list_dtree (Node r ys)
finsert x xs |\<subseteq>| ys
\<forall>a\<in>set z. case a of (v, e) \<Rightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
(t1, e1) \<in> fset ys
(t1, e1) \<notin> fset (finsert x xs)
(v, e) \<in> 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) z (finsert x xs))

goal (2 subgoals):
 1. \<lbrakk>list_dtree (Node r ys); {||} |\<subseteq>| ys; \<forall>(v, e)\<in>set z. set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}; (t1, e1) \<in> fset ys; (t1, e1) \<notin> fset {||}; (v, e) \<in> 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) z {||})\<rbrakk> \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
 2. \<And>x xs. \<lbrakk>x |\<notin>| xs; \<lbrakk>list_dtree (Node r ys); xs |\<subseteq>| ys; \<forall>(v, e)\<in>set z. set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}; (t1, e1) \<in> fset ys; (t1, e1) \<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) z xs)\<rbrakk> \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}; list_dtree (Node r ys); finsert x xs |\<subseteq>| ys; \<forall>(v, e)\<in>set z. set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}; (t1, e1) \<in> fset ys; (t1, e1) \<notin> fset (finsert x xs); (v, e) \<in> 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) z (finsert x xs))\<rbrakk> \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
[PROOF STEP]
let ?f = "merge_f r (finsert x xs)"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>list_dtree (Node r ys); {||} |\<subseteq>| ys; \<forall>(v, e)\<in>set z. set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}; (t1, e1) \<in> fset ys; (t1, e1) \<notin> fset {||}; (v, e) \<in> 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) z {||})\<rbrakk> \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
 2. \<And>x xs. \<lbrakk>x |\<notin>| xs; \<lbrakk>list_dtree (Node r ys); xs |\<subseteq>| ys; \<forall>(v, e)\<in>set z. set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}; (t1, e1) \<in> fset ys; (t1, e1) \<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) z xs)\<rbrakk> \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}; list_dtree (Node r ys); finsert x xs |\<subseteq>| ys; \<forall>(v, e)\<in>set z. set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}; (t1, e1) \<in> fset ys; (t1, e1) \<notin> fset (finsert x xs); (v, e) \<in> 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) z (finsert x xs))\<rbrakk> \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
[PROOF STEP]
let ?f' = "merge_f r xs"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>list_dtree (Node r ys); {||} |\<subseteq>| ys; \<forall>(v, e)\<in>set z. set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}; (t1, e1) \<in> fset ys; (t1, e1) \<notin> fset {||}; (v, e) \<in> 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) z {||})\<rbrakk> \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
 2. \<And>x xs. \<lbrakk>x |\<notin>| xs; \<lbrakk>list_dtree (Node r ys); xs |\<subseteq>| ys; \<forall>(v, e)\<in>set z. set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}; (t1, e1) \<in> fset ys; (t1, e1) \<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) z xs)\<rbrakk> \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}; list_dtree (Node r ys); finsert x xs |\<subseteq>| ys; \<forall>(v, e)\<in>set z. set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}; (t1, e1) \<in> fset ys; (t1, e1) \<notin> fset (finsert x xs); (v, e) \<in> 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) z (finsert x xs))\<rbrakk> \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
[PROOF STEP]
let ?merge = "Sorting_Algorithms.merge"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>list_dtree (Node r ys); {||} |\<subseteq>| ys; \<forall>(v, e)\<in>set z. set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}; (t1, e1) \<in> fset ys; (t1, e1) \<notin> fset {||}; (v, e) \<in> 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) z {||})\<rbrakk> \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
 2. \<And>x xs. \<lbrakk>x |\<notin>| xs; \<lbrakk>list_dtree (Node r ys); xs |\<subseteq>| ys; \<forall>(v, e)\<in>set z. set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}; (t1, e1) \<in> fset ys; (t1, e1) \<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) z xs)\<rbrakk> \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}; list_dtree (Node r ys); finsert x xs |\<subseteq>| ys; \<forall>(v, e)\<in>set z. set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}; (t1, e1) \<in> fset ys; (t1, e1) \<notin> fset (finsert x xs); (v, e) \<in> 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) z (finsert x xs))\<rbrakk> \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
[PROOF STEP]
interpret list_dtree "Node r ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_dtree (Node r ys)
[PROOF STEP]
using insert.prems(1)
[PROOF STATE]
proof (prove)
using this:
list_dtree (Node r ys)

goal (1 subgoal):
 1. list_dtree (Node r ys)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>list_dtree (Node r ys); {||} |\<subseteq>| ys; \<forall>(v, e)\<in>set z. set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}; (t1, e1) \<in> fset ys; (t1, e1) \<notin> fset {||}; (v, e) \<in> 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) z {||})\<rbrakk> \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
 2. \<And>x xs. \<lbrakk>x |\<notin>| xs; \<lbrakk>list_dtree (Node r ys); xs |\<subseteq>| ys; \<forall>(v, e)\<in>set z. set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}; (t1, e1) \<in> fset ys; (t1, e1) \<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) z xs)\<rbrakk> \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}; list_dtree (Node r ys); finsert x xs |\<subseteq>| ys; \<forall>(v, e)\<in>set z. set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}; (t1, e1) \<in> fset ys; (t1, e1) \<notin> fset (finsert x xs); (v, e) \<in> 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) z (finsert x xs))\<rbrakk> \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
[PROOF STEP]
have 0: "list_dtree (Node r (finsert x xs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_dtree (Node r (finsert x xs))
[PROOF STEP]
using list_dtree_subset insert.prems(1,2)
[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 ys)
finsert x xs |\<subseteq>| ys

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

goal (2 subgoals):
 1. \<lbrakk>list_dtree (Node r ys); {||} |\<subseteq>| ys; \<forall>(v, e)\<in>set z. set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}; (t1, e1) \<in> fset ys; (t1, e1) \<notin> fset {||}; (v, e) \<in> 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) z {||})\<rbrakk> \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
 2. \<And>x xs. \<lbrakk>x |\<notin>| xs; \<lbrakk>list_dtree (Node r ys); xs |\<subseteq>| ys; \<forall>(v, e)\<in>set z. set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}; (t1, e1) \<in> fset ys; (t1, e1) \<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) z xs)\<rbrakk> \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}; list_dtree (Node r ys); finsert x xs |\<subseteq>| ys; \<forall>(v, e)\<in>set z. set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}; (t1, e1) \<in> fset ys; (t1, e1) \<notin> fset (finsert x xs); (v, e) \<in> 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) z (finsert x xs))\<rbrakk> \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
[PROOF STEP]
proof(cases "ffold ?f z (finsert x xs) = ffold ?f' z xs")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 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) z (finsert x 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) z xs \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
 2. 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) z (finsert x xs) \<noteq> 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 \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
[PROOF STEP]
case True
[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) z (finsert x 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) z xs

goal (2 subgoals):
 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) z (finsert x 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) z xs \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
 2. 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) z (finsert x xs) \<noteq> 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 \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
[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) z (finsert x 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) z xs
[PROOF STEP]
have "(v,e) \<in> set (ffold ?f' z 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) z (finsert x 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) z xs

goal (1 subgoal):
 1. (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) z xs)
[PROOF STEP]
using insert.prems(6)
[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) z (finsert x 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) z xs
(v, e) \<in> 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) z (finsert x xs))

goal (1 subgoal):
 1. (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) z xs)
[PROOF STEP]
by argo
[PROOF STATE]
proof (state)
this:
(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) z xs)

goal (2 subgoals):
 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) z (finsert x 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) z xs \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
 2. 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) z (finsert x xs) \<noteq> 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 \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(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) z xs)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(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) z xs)

goal (1 subgoal):
 1. set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
[PROOF STEP]
using insert.IH insert.prems
[PROOF STATE]
proof (prove)
using this:
(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) z xs)
\<lbrakk>list_dtree (Node r ys); xs |\<subseteq>| ys; \<forall>a\<in>set z. case a of (v, e) \<Rightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}; (t1, e1) \<in> fset ys; (t1, e1) \<notin> fset xs; (v, e) \<in> 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) z xs)\<rbrakk> \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
list_dtree (Node r ys)
finsert x xs |\<subseteq>| ys
\<forall>a\<in>set z. case a of (v, e) \<Rightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
(t1, e1) \<in> fset ys
(t1, e1) \<notin> fset (finsert x xs)
(v, e) \<in> 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) z (finsert x xs))

goal (1 subgoal):
 1. set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}

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) z (finsert x xs) \<noteq> 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 \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
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) z (finsert x xs) \<noteq> 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 \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
[PROOF STEP]
case not_right: False
[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) z (finsert x xs) \<noteq> 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) z (finsert x xs) \<noteq> 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 \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
[PROOF STEP]
obtain t2 e2 where t2_def[simp]: "x = (t2,e2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>t2 e2. x = (t2, e2) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
x = (t2, e2)

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) z (finsert x xs) \<noteq> 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 \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
[PROOF STEP]
proof(cases "(v,e) \<in> set (dtree_to_list (Node r {|(t2,e2)|}))")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (v, e) \<in> set (dtree_to_list (Node r {|(t2, e2)|})) \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
 2. (v, e) \<notin> set (dtree_to_list (Node r {|(t2, e2)|})) \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
(v, e) \<in> set (dtree_to_list (Node r {|(t2, e2)|}))

goal (2 subgoals):
 1. (v, e) \<in> set (dtree_to_list (Node r {|(t2, e2)|})) \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
 2. (v, e) \<notin> set (dtree_to_list (Node r {|(t2, e2)|})) \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
[PROOF STEP]
have uneq: "(t2,e2) \<noteq> (t1,e1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (t2, e2) \<noteq> (t1, e1)
[PROOF STEP]
using insert.prems(5) t2_def
[PROOF STATE]
proof (prove)
using this:
(t1, e1) \<notin> fset (finsert x xs)
x = (t2, e2)

goal (1 subgoal):
 1. (t2, e2) \<noteq> (t1, e1)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(t2, e2) \<noteq> (t1, e1)

goal (2 subgoals):
 1. (v, e) \<in> set (dtree_to_list (Node r {|(t2, e2)|})) \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
 2. (v, e) \<notin> set (dtree_to_list (Node r {|(t2, e2)|})) \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(t2, e2) \<noteq> (t1, e1)

goal (2 subgoals):
 1. (v, e) \<in> set (dtree_to_list (Node r {|(t2, e2)|})) \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
 2. (v, e) \<notin> set (dtree_to_list (Node r {|(t2, e2)|})) \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
[PROOF STEP]
have 1: "(t2,e2) \<in> fset ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (t2, e2) \<in> fset ys
[PROOF STEP]
using insert.prems(2) notin_fset
[PROOF STATE]
proof (prove)
using this:
finsert x xs |\<subseteq>| ys
(?x |\<notin>| ?S) = (?x \<notin> fset ?S)

goal (1 subgoal):
 1. (t2, e2) \<in> fset ys
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(t2, e2) \<in> fset ys

goal (2 subgoals):
 1. (v, e) \<in> set (dtree_to_list (Node r {|(t2, e2)|})) \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
 2. (v, e) \<notin> set (dtree_to_list (Node r {|(t2, e2)|})) \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(t2, e2) \<noteq> (t1, e1)
(t2, e2) \<in> fset ys
[PROOF STEP]
have "dlverts t1 \<inter> dlverts t2 = {}"
[PROOF STATE]
proof (prove)
using this:
(t2, e2) \<noteq> (t1, e1)
(t2, e2) \<in> fset ys

goal (1 subgoal):
 1. dlverts t1 \<inter> dlverts t2 = {}
[PROOF STEP]
using insert.prems(4) wf_lverts
[PROOF STATE]
proof (prove)
using this:
(t2, e2) \<noteq> (t1, e1)
(t2, e2) \<in> fset ys
(t1, e1) \<in> fset ys
wf_dlverts (Node r ys)

goal (1 subgoal):
 1. dlverts t1 \<inter> dlverts t2 = {}
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
dlverts t1 \<inter> dlverts t2 = {}

goal (2 subgoals):
 1. (v, e) \<in> set (dtree_to_list (Node r {|(t2, e2)|})) \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
 2. (v, e) \<notin> set (dtree_to_list (Node r {|(t2, e2)|})) \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dlverts t1 \<inter> dlverts t2 = {}
[PROOF STEP]
have 2: "\<forall>x1\<in>fst ` set (dtree_to_list (Node r {|(t2, e2)|})). set x1 \<inter> dlverts t1 = {}"
[PROOF STATE]
proof (prove)
using this:
dlverts t1 \<inter> dlverts t2 = {}

goal (1 subgoal):
 1. \<forall>x1\<in>fst ` set (dtree_to_list (Node r {|(t2, e2)|})). set x1 \<inter> dlverts t1 = {}
[PROOF STEP]
using dtree_to_list_x1_disjoint
[PROOF STATE]
proof (prove)
using this:
dlverts t1 \<inter> dlverts t2 = {}
dlverts ?t1.0 \<inter> dlverts ?t2.0 = {} \<Longrightarrow> \<forall>x1\<in>fst ` set (dtree_to_list (Node ?r {|(?t1.0, ?e1.0)|})). set x1 \<inter> dlverts ?t2.0 = {}

goal (1 subgoal):
 1. \<forall>x1\<in>fst ` set (dtree_to_list (Node r {|(t2, e2)|})). set x1 \<inter> dlverts t1 = {}
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
\<forall>x1\<in>fst ` set (dtree_to_list (Node r {|(t2, e2)|})). set x1 \<inter> dlverts t1 = {}

goal (2 subgoals):
 1. (v, e) \<in> set (dtree_to_list (Node r {|(t2, e2)|})) \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
 2. (v, e) \<notin> set (dtree_to_list (Node r {|(t2, e2)|})) \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
[PROOF STEP]
have "(darcs t1 \<union> {e1}) \<inter> (darcs t2 \<union> {e2}) = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (darcs t1 \<union> {e1}) \<inter> (darcs t2 \<union> {e2}) = {}
[PROOF STEP]
using insert.prems(4) uneq 1 disjoint_darcs_if_wf_aux5 wf_arcs
[PROOF STATE]
proof (prove)
using this:
(t1, e1) \<in> fset ys
(t2, e2) \<noteq> (t1, e1)
(t2, e2) \<in> fset ys
\<lbrakk>wf_darcs (Node ?r ?xs); (?t1.0, ?e1.0) \<in> fset ?xs; (?t2.0, ?e2.0) \<in> fset ?xs; (?t1.0, ?e1.0) \<noteq> (?t2.0, ?e2.0)\<rbrakk> \<Longrightarrow> (darcs ?t1.0 \<union> {?e1.0}) \<inter> (darcs ?t2.0 \<union> {?e2.0}) = {}
wf_darcs (Node r ys)

goal (1 subgoal):
 1. (darcs t1 \<union> {e1}) \<inter> (darcs t2 \<union> {e2}) = {}
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
(darcs t1 \<union> {e1}) \<inter> (darcs t2 \<union> {e2}) = {}

goal (2 subgoals):
 1. (v, e) \<in> set (dtree_to_list (Node r {|(t2, e2)|})) \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
 2. (v, e) \<notin> set (dtree_to_list (Node r {|(t2, e2)|})) \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(darcs t1 \<union> {e1}) \<inter> (darcs t2 \<union> {e2}) = {}
[PROOF STEP]
have 3: "\<forall>e\<in>snd ` set (dtree_to_list (Node r {|(t2, e2)|})). e \<notin> darcs t1 \<union> {e1}"
[PROOF STATE]
proof (prove)
using this:
(darcs t1 \<union> {e1}) \<inter> (darcs t2 \<union> {e2}) = {}

goal (1 subgoal):
 1. \<forall>e\<in>snd ` set (dtree_to_list (Node r {|(t2, e2)|})). e \<notin> darcs t1 \<union> {e1}
[PROOF STEP]
using dtree_to_list_e_disjoint
[PROOF STATE]
proof (prove)
using this:
(darcs t1 \<union> {e1}) \<inter> (darcs t2 \<union> {e2}) = {}
(darcs ?t1.0 \<union> {?e1.0}) \<inter> (darcs ?t2.0 \<union> {?e2.0}) = {} \<Longrightarrow> \<forall>e\<in>snd ` set (dtree_to_list (Node ?r {|(?t1.0, ?e1.0)|})). e \<notin> darcs ?t2.0 \<union> {?e2.0}

goal (1 subgoal):
 1. \<forall>e\<in>snd ` set (dtree_to_list (Node r {|(t2, e2)|})). e \<notin> darcs t1 \<union> {e1}
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
\<forall>e\<in>snd ` set (dtree_to_list (Node r {|(t2, e2)|})). e \<notin> darcs t1 \<union> {e1}

goal (2 subgoals):
 1. (v, e) \<in> set (dtree_to_list (Node r {|(t2, e2)|})) \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
 2. (v, e) \<notin> set (dtree_to_list (Node r {|(t2, e2)|})) \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
[PROOF STEP]
have "[] \<notin> dverts t2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [] \<notin> dverts t2
[PROOF STEP]
using 1 wf_lverts empty_notin_wf_dlverts
[PROOF STATE]
proof (prove)
using this:
(t2, e2) \<in> fset ys
wf_dlverts (Node r ys)
wf_dlverts ?t \<Longrightarrow> [] \<notin> dverts ?t

goal (1 subgoal):
 1. [] \<notin> dverts t2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
[] \<notin> dverts t2

goal (2 subgoals):
 1. (v, e) \<in> set (dtree_to_list (Node r {|(t2, e2)|})) \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
 2. (v, e) \<notin> set (dtree_to_list (Node r {|(t2, e2)|})) \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[] \<notin> dverts t2
[PROOF STEP]
have "\<forall>x1\<in>fst ` set (dtree_to_list (Node r {|(t2, e2)|})). x1 \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
[] \<notin> dverts t2

goal (1 subgoal):
 1. \<forall>x1\<in>fst ` set (dtree_to_list (Node r {|(t2, e2)|})). x1 \<noteq> []
[PROOF STEP]
using 1 dtree_to_list_x_in_dverts
[PROOF STATE]
proof (prove)
using this:
[] \<notin> dverts t2
(t2, e2) \<in> fset ys
?x \<in> fst ` set (dtree_to_list (Node ?r {|(?t1.0, ?e1.0)|})) \<Longrightarrow> ?x \<in> dverts ?t1.0

goal (1 subgoal):
 1. \<forall>x1\<in>fst ` set (dtree_to_list (Node r {|(t2, e2)|})). x1 \<noteq> []
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<forall>x1\<in>fst ` set (dtree_to_list (Node r {|(t2, e2)|})). x1 \<noteq> []

goal (2 subgoals):
 1. (v, e) \<in> set (dtree_to_list (Node r {|(t2, e2)|})) \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
 2. (v, e) \<notin> set (dtree_to_list (Node r {|(t2, e2)|})) \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x1\<in>fst ` set (dtree_to_list (Node r {|(t2, e2)|})). x1 \<noteq> []
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>x1\<in>fst ` set (dtree_to_list (Node r {|(t2, e2)|})). x1 \<noteq> []

goal (1 subgoal):
 1. set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
[PROOF STEP]
using True 2 3
[PROOF STATE]
proof (prove)
using this:
\<forall>x1\<in>fst ` set (dtree_to_list (Node r {|(t2, e2)|})). x1 \<noteq> []
(v, e) \<in> set (dtree_to_list (Node r {|(t2, e2)|}))
\<forall>x1\<in>fst ` set (dtree_to_list (Node r {|(t2, e2)|})). set x1 \<inter> dlverts t1 = {}
\<forall>e\<in>snd ` set (dtree_to_list (Node r {|(t2, e2)|})). e \<notin> darcs t1 \<union> {e1}

goal (1 subgoal):
 1. set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}

goal (1 subgoal):
 1. (v, e) \<notin> set (dtree_to_list (Node r {|(t2, e2)|})) \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (v, e) \<notin> set (dtree_to_list (Node r {|(t2, e2)|})) \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
(v, e) \<notin> set (dtree_to_list (Node r {|(t2, e2)|}))

goal (1 subgoal):
 1. (v, e) \<notin> set (dtree_to_list (Node r {|(t2, e2)|})) \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
[PROOF STEP]
have "xs |\<subseteq>| finsert x xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs |\<subseteq>| finsert x xs
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
xs |\<subseteq>| finsert x xs

goal (1 subgoal):
 1. (v, e) \<notin> set (dtree_to_list (Node r {|(t2, e2)|})) \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xs |\<subseteq>| finsert x xs
[PROOF STEP]
have f_xs: "ffold ?f z xs = ffold ?f' z xs"
[PROOF STATE]
proof (prove)
using this:
xs |\<subseteq>| 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) z 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) z xs
[PROOF STEP]
using merge_ffold_supset 0
[PROOF STATE]
proof (prove)
using this:
xs |\<subseteq>| finsert x xs
\<lbrakk>?xs |\<subseteq>| ?ys; list_dtree (Node ?r ?ys)\<rbrakk> \<Longrightarrow> ffold (\<lambda>(t, e) b. if (t, e) \<in> fset ?ys \<and> list_dtree (Node ?r ?ys) \<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) ?acc ?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) ?acc ?xs
list_dtree (Node r (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) z 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) z xs
[PROOF STEP]
by presburger
[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) z 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) z xs

goal (1 subgoal):
 1. (v, e) \<notin> set (dtree_to_list (Node r {|(t2, e2)|})) \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
[PROOF STEP]
have "ffold ?f z (finsert x xs) = ?f x (ffold ?f z 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) z (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) z 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) z (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) z 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) z (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) z xs)

goal (1 subgoal):
 1. (v, e) \<notin> set (dtree_to_list (Node r {|(t2, e2)|})) \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
[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) z (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) z xs)
[PROOF STEP]
have 0: "ffold ?f z (finsert x xs) = ?f x (ffold ?f' z 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) z (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) 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) z (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) z xs)
[PROOF STEP]
using 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) z (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) z xs)
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) z 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) 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) z (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) z xs)
[PROOF STEP]
by argo
[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) z (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) z xs)

goal (1 subgoal):
 1. (v, e) \<notin> set (dtree_to_list (Node r {|(t2, e2)|})) \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
[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) z (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) z xs)
[PROOF STEP]
have "?f x (ffold ?f' z xs) \<noteq> ffold ?f' z 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) z (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) z 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 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) \<noteq> 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
[PROOF STEP]
using not_right
[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) z (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) z xs)
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) z (finsert x xs) \<noteq> 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. (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) z xs) \<noteq> 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
[PROOF STEP]
by argo
[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 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) \<noteq> 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. (v, e) \<notin> set (dtree_to_list (Node r {|(t2, e2)|})) \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking 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 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) \<noteq> 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
[PROOF STEP]
have "?f (t2,e2) (ffold ?f' z xs)
                = ?merge cmp' (dtree_to_list (Node r {|(t2,e2)|})) (ffold ?f' z xs)"
[PROOF STATE]
proof (prove)
using 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 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) \<noteq> 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. (case (t2, e2) 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) z xs) = Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t2, e2)|})) (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)
[PROOF STEP]
using merge_f_merge_if_not_snd t2_def
[PROOF STATE]
proof (prove)
using 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 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) \<noteq> 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
(case (?t1.0, ?e1.0) 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) ?z \<noteq> ?z \<Longrightarrow> (case (?t1.0, ?e1.0) 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) ?z = Sorting_Algorithms.merge cmp' (dtree_to_list (Node ?r {|(?t1.0, ?e1.0)|})) ?z
x = (t2, e2)

goal (1 subgoal):
 1. (case (t2, e2) 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) z xs) = Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t2, e2)|})) (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)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(case (t2, e2) 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) z xs) = Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t2, e2)|})) (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. (v, e) \<notin> set (dtree_to_list (Node r {|(t2, e2)|})) \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(case (t2, e2) 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) z xs) = Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t2, e2)|})) (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)
[PROOF STEP]
have "ffold ?f z (finsert x xs)
                = ?merge cmp' (dtree_to_list (Node r {|(t2,e2)|})) (ffold ?f' z xs)"
[PROOF STATE]
proof (prove)
using this:
(case (t2, e2) 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) z xs) = Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t2, e2)|})) (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) z (finsert x xs) = Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t2, e2)|})) (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)
[PROOF STEP]
using 0 t2_def
[PROOF STATE]
proof (prove)
using this:
(case (t2, e2) 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) z xs) = Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t2, e2)|})) (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)
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) z (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) z xs)
x = (t2, e2)

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) z (finsert x xs) = Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t2, e2)|})) (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)
[PROOF STEP]
by argo
[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) z (finsert x xs) = Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t2, e2)|})) (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. (v, e) \<notin> set (dtree_to_list (Node r {|(t2, e2)|})) \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
[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) z (finsert x xs) = Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t2, e2)|})) (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)
[PROOF STEP]
have "(v,e) \<in> set (?merge cmp' (dtree_to_list (Node r {|(t2,e2)|})) (ffold ?f' z 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) z (finsert x xs) = Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t2, e2)|})) (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. (v, e) \<in> set (Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t2, e2)|})) (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))
[PROOF STEP]
using insert.prems(6)
[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) z (finsert x xs) = Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t2, e2)|})) (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)
(v, e) \<in> 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) z (finsert x xs))

goal (1 subgoal):
 1. (v, e) \<in> set (Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t2, e2)|})) (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))
[PROOF STEP]
by argo
[PROOF STATE]
proof (state)
this:
(v, e) \<in> set (Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t2, e2)|})) (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. (v, e) \<notin> set (dtree_to_list (Node r {|(t2, e2)|})) \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(v, e) \<in> set (Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t2, e2)|})) (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))
[PROOF STEP]
have "(v,e) \<in> set (ffold ?f' z xs)"
[PROOF STATE]
proof (prove)
using this:
(v, e) \<in> set (Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t2, e2)|})) (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. (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) z xs)
[PROOF STEP]
using set_merge False
[PROOF STATE]
proof (prove)
using this:
(v, e) \<in> set (Sorting_Algorithms.merge cmp' (dtree_to_list (Node r {|(t2, e2)|})) (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))
set ?xs \<union> set ?ys = set (Sorting_Algorithms.merge ?cmp ?xs ?ys)
(v, e) \<notin> set (dtree_to_list (Node r {|(t2, e2)|}))

goal (1 subgoal):
 1. (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) z xs)
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
(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) z xs)

goal (1 subgoal):
 1. (v, e) \<notin> set (dtree_to_list (Node r {|(t2, e2)|})) \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(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) z xs)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(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) z xs)

goal (1 subgoal):
 1. set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
[PROOF STEP]
using insert.IH insert.prems
[PROOF STATE]
proof (prove)
using this:
(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) z xs)
\<lbrakk>list_dtree (Node r ys); xs |\<subseteq>| ys; \<forall>a\<in>set z. case a of (v, e) \<Rightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}; (t1, e1) \<in> fset ys; (t1, e1) \<notin> fset xs; (v, e) \<in> 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) z xs)\<rbrakk> \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
list_dtree (Node r ys)
finsert x xs |\<subseteq>| ys
\<forall>a\<in>set z. case a of (v, e) \<Rightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
(t1, e1) \<in> fset ys
(t1, e1) \<notin> fset (finsert x xs)
(v, e) \<in> 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) z (finsert x xs))

goal (1 subgoal):
 1. set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}

goal (1 subgoal):
 1. \<lbrakk>list_dtree (Node r ys); {||} |\<subseteq>| ys; \<forall>(v, e)\<in>set z. set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}; (t1, e1) \<in> fset ys; (t1, e1) \<notin> fset {||}; (v, e) \<in> 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) z {||})\<rbrakk> \<Longrightarrow> set v \<inter> dlverts t1 = {} \<and> v \<noteq> [] \<and> e \<notin> darcs t1 \<union> {e1}
[PROOF STEP]
qed(auto)


[STATEMENT]
lemma rank_le_if_ngt: "compare cmp'' (r, e) (r0, e0) \<noteq> Greater \<Longrightarrow> rank (rev r) \<le> rank (rev r0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. compare cmp'' (r, e) (r0, e0) \<noteq> Greater \<Longrightarrow> rank (rev r) \<le> rank (rev r0)
[PROOF STEP]
using gt_if_rank_contr
[PROOF STATE]
proof (prove)
using this:
rank (rev ?r0.0) < rank (rev ?r) \<Longrightarrow> compare cmp'' (?r, ?e) (?r0.0, ?e0.0) = Greater

goal (1 subgoal):
 1. compare cmp'' (r, e) (r0, e0) \<noteq> Greater \<Longrightarrow> rank (rev r) \<le> rank (rev r0)
[PROOF STEP]
by force


[STATEMENT]
lemma dom_restrict_idem[simp] : "(dom p) \<triangleleft> p = p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom p \<triangleleft> p = p
[PROOF STEP]
apply (rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. (dom p \<triangleleft> p) x = p x
[PROOF STEP]
apply (auto simp: dom_restrict_def
      dest: neq_commute[THEN iffD1,THEN not_None_eq [THEN iffD1]])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma length_INTT:
  assumes n_def: "length numbers = n"
  shows "length (INTT numbers) = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (INTT numbers) = n
[PROOF STEP]
unfolding INTT_def intt_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (map (\<lambda>i. \<Sum>j = 0..<n. numbers ! j * \<mu> ^ (i * j)) [0..<n]) = n
[PROOF STEP]
using n_def length_map[of _ "[0..<n]"]
[PROOF STATE]
proof (prove)
using this:
length numbers = n
length (map ?f [0..<n]) = length [0..<n]

goal (1 subgoal):
 1. length (map (\<lambda>i. \<Sum>j = 0..<n. numbers ! j * \<mu> ^ (i * j)) [0..<n]) = n
[PROOF STEP]
by simp


[STATEMENT]
lemma sorted_list_of_set_eq [dest]:
  "sorted_list_of_set (fset x) = sorted_list_of_set (fset y) \<Longrightarrow> x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted_list_of_set (fset x) = sorted_list_of_set (fset y) \<Longrightarrow> x = y
[PROOF STEP]
by (metis finite_fset fset_inject sorted_list_of_set(1))


[STATEMENT]
lemma "max_policy =
   \<lparr>nodesL = [''WebFrnt'', ''DB'', ''Log'', ''WebApp'', ''INET''],
    edgesL = [(''WebFrnt'', ''WebFrnt''), (''WebFrnt'', ''Log''), (''WebFrnt'', ''WebApp''), (''WebFrnt'', ''INET''), (''DB'', ''DB''),
              (''DB'', ''Log''), (''DB'', ''WebApp''), (''Log'', ''Log''), (''WebApp'', ''WebFrnt''), (''WebApp'', ''DB''),
              (''WebApp'', ''Log''), (''WebApp'', ''WebApp''), (''WebApp'', ''INET''), (''INET'', ''WebFrnt''), (''INET'', ''INET'')]\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max_policy = \<lparr>nodesL = [''WebFrnt'', ''DB'', ''Log'', ''WebApp'', ''INET''], edgesL = [(''WebFrnt'', ''WebFrnt''), (''WebFrnt'', ''Log''), (''WebFrnt'', ''WebApp''), (''WebFrnt'', ''INET''), (''DB'', ''DB''), (''DB'', ''Log''), (''DB'', ''WebApp''), (''Log'', ''Log''), (''WebApp'', ''WebFrnt''), (''WebApp'', ''DB''), (''WebApp'', ''Log''), (''WebApp'', ''WebApp''), (''WebApp'', ''INET''), (''INET'', ''WebFrnt''), (''INET'', ''INET'')]\<rparr>
[PROOF STEP]
by eval


[STATEMENT]
lemma new\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_is_element_ptr:
  assumes "new\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t h = (new_element_ptr, h')"
  shows "is_element_ptr new_element_ptr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_element_ptr new_element_ptr
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
new\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t h = (new_element_ptr, h')

goal (1 subgoal):
 1. is_element_ptr new_element_ptr
[PROOF STEP]
by(auto simp add: new\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def Let_def)


[STATEMENT]
lemma consistent_init:
  assumes "\<psi> \<in> \<R>\<^sup>2" and "f \<in> \<R>"
  shows "consistent \<psi> i (f \<triangleright> n) = (if \<psi> i \<triangleright> n = f \<triangleright> n then Some 0 else Some 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. consistent \<psi> i (f \<triangleright> n) = (if \<psi> i \<triangleright> n = f \<triangleright> n then Some 0 else Some 1)
[PROOF STEP]
using consistent_def[of _ _ "init f n"] assms  init_eq_iff_eq_upto
[PROOF STATE]
proof (prove)
using this:
consistent ?\<psi> ?i (f \<triangleright> n) \<equiv> if \<forall>k<e_length (f \<triangleright> n). ?\<psi> ?i k \<down> then if \<forall>k<e_length (f \<triangleright> n). ?\<psi> ?i k \<down>= e_nth (f \<triangleright> n) k then Some 0 else Some 1 else None
\<psi> \<in> \<R>\<^sup>2
f \<in> \<R>
\<lbrakk>?g \<in> \<R>; ?f \<in> \<R>\<rbrakk> \<Longrightarrow> (\<forall>j<Suc ?n. ?g j = ?f j) = (?g \<triangleright> ?n = ?f \<triangleright> ?n)

goal (1 subgoal):
 1. consistent \<psi> i (f \<triangleright> n) = (if \<psi> i \<triangleright> n = f \<triangleright> n then Some 0 else Some 1)
[PROOF STEP]
by simp


[STATEMENT]
lemma "any\<cdot>(\<Lambda> z. eq\<cdot>z\<cdot>a) = elem\<cdot>a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. any\<cdot>(\<Lambda> z. eq\<cdot>z\<cdot>a) = elem\<cdot>a
[PROOF STEP]
proof (rule cfun_eqI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. any\<cdot>(\<Lambda> z. eq\<cdot>z\<cdot>a)\<cdot>x = elem\<cdot>a\<cdot>x
[PROOF STEP]
fix xs
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. any\<cdot>(\<Lambda> z. eq\<cdot>z\<cdot>a)\<cdot>x = elem\<cdot>a\<cdot>x
[PROOF STEP]
show "any\<cdot>(\<Lambda> z. eq\<cdot>z\<cdot>a)\<cdot>xs = elem\<cdot>a\<cdot>xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. any\<cdot>(\<Lambda> z. eq\<cdot>z\<cdot>a)\<cdot>xs = elem\<cdot>a\<cdot>xs
[PROOF STEP]
by (induct xs) auto
[PROOF STATE]
proof (state)
this:
any\<cdot>(\<Lambda> z. eq\<cdot>z\<cdot>a)\<cdot>xs = elem\<cdot>a\<cdot>xs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma "drop\<cdot>n\<cdot>[] \<sqsubseteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Data_List.drop\<cdot>n\<cdot>[] \<sqsubseteq> []
[PROOF STEP]
by (subst drop.simps) (auto simp: if_equal)


[STATEMENT]
lemma succ_min: assumes "deg \<ge> 2" and "(x::nat) < mi" shows
  "vebt_succ (Node (Some (mi, ma)) deg treeList summary) x = Some mi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vebt_succ (Node (Some (mi, ma)) deg treeList summary) x = Some mi
[PROOF STEP]
by (metis add_2_eq_Suc assms(1) assms(2) le_add_diff_inverse vebt_succ.simps(6))


[STATEMENT]
lemma \<gamma>_mono: "mono \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mono \<gamma>
[PROOF STEP]
by rule (metis \<alpha>\<gamma>_defl galois inf_absorb1 le_infE)


[STATEMENT]
lemma None_orelse[simp]: "None orelse y = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. None orelse y = y
[PROOF STEP]
by (simp add: orelse_def)


[STATEMENT]
lemma fincomp_unit [simp]: "fincomp (\<lambda>i. \<one>) A = \<one>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fincomp (\<lambda>i. \<one>) A = \<one>
[PROOF STEP]
by (simp add: fincomp_unit_eqI)