[STATEMENT]
lemma merge_property: "\<lbrakk>set t1 \<subseteq> A; set t2 \<subseteq> B; t1 \<upharpoonleft> B = t2 \<upharpoonleft> A \<rbrakk>
  \<Longrightarrow> let t = (merge A B t1 t2) in (t \<upharpoonleft> A = t1 \<and> t \<upharpoonleft> B = t2 \<and> set t \<subseteq> ((set t1) \<union> (set t2)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>set t1 \<subseteq> A; set t2 \<subseteq> B; t1 \<upharpoonleft> B = t2 \<upharpoonleft> A\<rbrakk> \<Longrightarrow> let t = merge A B t1 t2 in t \<upharpoonleft> A = t1 \<and> t \<upharpoonleft> B = t2 \<and> set t \<subseteq> set t1 \<union> set t2
[PROOF STEP]
unfolding Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>set t1 \<subseteq> A; set t2 \<subseteq> B; t1 \<upharpoonleft> B = t2 \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1 t2 \<upharpoonleft> A = t1 \<and> merge A B t1 t2 \<upharpoonleft> B = t2 \<and> set (merge A B t1 t2) \<subseteq> set t1 \<union> set t2
[PROOF STEP]
proof (induct A B t1 t2 rule: merge.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>A B t2. \<lbrakk>set [] \<subseteq> A; set t2 \<subseteq> B; [] \<upharpoonleft> B = t2 \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B [] t2 \<upharpoonleft> A = [] \<and> merge A B [] t2 \<upharpoonleft> B = t2 \<and> set (merge A B [] t2) \<subseteq> set [] \<union> set t2
 2. \<And>A B v va. \<lbrakk>set (v # va) \<subseteq> A; set [] \<subseteq> B; (v # va) \<upharpoonleft> B = [] \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B (v # va) [] \<upharpoonleft> A = v # va \<and> merge A B (v # va) [] \<upharpoonleft> B = [] \<and> set (merge A B (v # va) []) \<subseteq> set (v # va) \<union> set []
 3. \<And>A B e1 t1' e2 t2'. \<lbrakk>\<lbrakk>e1 = e2; set t1' \<subseteq> A; set t2' \<subseteq> B; t1' \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' t2' \<upharpoonleft> A = t1' \<and> merge A B t1' t2' \<upharpoonleft> B = t2' \<and> set (merge A B t1' t2') \<subseteq> set t1' \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<in> A \<inter> B; set (e1 # t1') \<subseteq> A; set t2' \<subseteq> B; (e1 # t1') \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') t2' \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') t2' \<upharpoonleft> B = t2' \<and> set (merge A B (e1 # t1') t2') \<subseteq> set (e1 # t1') \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<notin> A \<inter> B; set t1' \<subseteq> A; set (e2 # t2') \<subseteq> B; t1' \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' (e2 # t2') \<upharpoonleft> A = t1' \<and> merge A B t1' (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B t1' (e2 # t2')) \<subseteq> set t1' \<union> set (e2 # t2'); set (e1 # t1') \<subseteq> A; set (e2 # t2') \<subseteq> B; (e1 # t1') \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
case (1 A B t2)
[PROOF STATE]
proof (state)
this:
set [] \<subseteq> A
set t2 \<subseteq> B
[] \<upharpoonleft> B = t2 \<upharpoonleft> A

goal (3 subgoals):
 1. \<And>A B t2. \<lbrakk>set [] \<subseteq> A; set t2 \<subseteq> B; [] \<upharpoonleft> B = t2 \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B [] t2 \<upharpoonleft> A = [] \<and> merge A B [] t2 \<upharpoonleft> B = t2 \<and> set (merge A B [] t2) \<subseteq> set [] \<union> set t2
 2. \<And>A B v va. \<lbrakk>set (v # va) \<subseteq> A; set [] \<subseteq> B; (v # va) \<upharpoonleft> B = [] \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B (v # va) [] \<upharpoonleft> A = v # va \<and> merge A B (v # va) [] \<upharpoonleft> B = [] \<and> set (merge A B (v # va) []) \<subseteq> set (v # va) \<union> set []
 3. \<And>A B e1 t1' e2 t2'. \<lbrakk>\<lbrakk>e1 = e2; set t1' \<subseteq> A; set t2' \<subseteq> B; t1' \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' t2' \<upharpoonleft> A = t1' \<and> merge A B t1' t2' \<upharpoonleft> B = t2' \<and> set (merge A B t1' t2') \<subseteq> set t1' \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<in> A \<inter> B; set (e1 # t1') \<subseteq> A; set t2' \<subseteq> B; (e1 # t1') \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') t2' \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') t2' \<upharpoonleft> B = t2' \<and> set (merge A B (e1 # t1') t2') \<subseteq> set (e1 # t1') \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<notin> A \<inter> B; set t1' \<subseteq> A; set (e2 # t2') \<subseteq> B; t1' \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' (e2 # t2') \<upharpoonleft> A = t1' \<and> merge A B t1' (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B t1' (e2 # t2')) \<subseteq> set t1' \<union> set (e2 # t2'); set (e1 # t1') \<subseteq> A; set (e2 # t2') \<subseteq> B; (e1 # t1') \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
set [] \<subseteq> A
set t2 \<subseteq> B
[] \<upharpoonleft> B = t2 \<upharpoonleft> A

goal (1 subgoal):
 1. merge A B [] t2 \<upharpoonleft> A = [] \<and> merge A B [] t2 \<upharpoonleft> B = t2 \<and> set (merge A B [] t2) \<subseteq> set [] \<union> set t2
[PROOF STEP]
by (metis Un_empty_left empty_subsetI list_subset_iff_projection_neutral
      merge.simps(1) set_empty subset_iff_psubset_eq)
[PROOF STATE]
proof (state)
this:
merge A B [] t2 \<upharpoonleft> A = [] \<and> merge A B [] t2 \<upharpoonleft> B = t2 \<and> set (merge A B [] t2) \<subseteq> set [] \<union> set t2

goal (2 subgoals):
 1. \<And>A B v va. \<lbrakk>set (v # va) \<subseteq> A; set [] \<subseteq> B; (v # va) \<upharpoonleft> B = [] \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B (v # va) [] \<upharpoonleft> A = v # va \<and> merge A B (v # va) [] \<upharpoonleft> B = [] \<and> set (merge A B (v # va) []) \<subseteq> set (v # va) \<union> set []
 2. \<And>A B e1 t1' e2 t2'. \<lbrakk>\<lbrakk>e1 = e2; set t1' \<subseteq> A; set t2' \<subseteq> B; t1' \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' t2' \<upharpoonleft> A = t1' \<and> merge A B t1' t2' \<upharpoonleft> B = t2' \<and> set (merge A B t1' t2') \<subseteq> set t1' \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<in> A \<inter> B; set (e1 # t1') \<subseteq> A; set t2' \<subseteq> B; (e1 # t1') \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') t2' \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') t2' \<upharpoonleft> B = t2' \<and> set (merge A B (e1 # t1') t2') \<subseteq> set (e1 # t1') \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<notin> A \<inter> B; set t1' \<subseteq> A; set (e2 # t2') \<subseteq> B; t1' \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' (e2 # t2') \<upharpoonleft> A = t1' \<and> merge A B t1' (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B t1' (e2 # t2')) \<subseteq> set t1' \<union> set (e2 # t2'); set (e1 # t1') \<subseteq> A; set (e2 # t2') \<subseteq> B; (e1 # t1') \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>A B v va. \<lbrakk>set (v # va) \<subseteq> A; set [] \<subseteq> B; (v # va) \<upharpoonleft> B = [] \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B (v # va) [] \<upharpoonleft> A = v # va \<and> merge A B (v # va) [] \<upharpoonleft> B = [] \<and> set (merge A B (v # va) []) \<subseteq> set (v # va) \<union> set []
 2. \<And>A B e1 t1' e2 t2'. \<lbrakk>\<lbrakk>e1 = e2; set t1' \<subseteq> A; set t2' \<subseteq> B; t1' \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' t2' \<upharpoonleft> A = t1' \<and> merge A B t1' t2' \<upharpoonleft> B = t2' \<and> set (merge A B t1' t2') \<subseteq> set t1' \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<in> A \<inter> B; set (e1 # t1') \<subseteq> A; set t2' \<subseteq> B; (e1 # t1') \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') t2' \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') t2' \<upharpoonleft> B = t2' \<and> set (merge A B (e1 # t1') t2') \<subseteq> set (e1 # t1') \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<notin> A \<inter> B; set t1' \<subseteq> A; set (e2 # t2') \<subseteq> B; t1' \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' (e2 # t2') \<upharpoonleft> A = t1' \<and> merge A B t1' (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B t1' (e2 # t2')) \<subseteq> set t1' \<union> set (e2 # t2'); set (e1 # t1') \<subseteq> A; set (e2 # t2') \<subseteq> B; (e1 # t1') \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
case (2 A B t1)
[PROOF STATE]
proof (state)
this:
set (t1 # va_) \<subseteq> A
set [] \<subseteq> B
(t1 # va_) \<upharpoonleft> B = [] \<upharpoonleft> A

goal (2 subgoals):
 1. \<And>A B v va. \<lbrakk>set (v # va) \<subseteq> A; set [] \<subseteq> B; (v # va) \<upharpoonleft> B = [] \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B (v # va) [] \<upharpoonleft> A = v # va \<and> merge A B (v # va) [] \<upharpoonleft> B = [] \<and> set (merge A B (v # va) []) \<subseteq> set (v # va) \<union> set []
 2. \<And>A B e1 t1' e2 t2'. \<lbrakk>\<lbrakk>e1 = e2; set t1' \<subseteq> A; set t2' \<subseteq> B; t1' \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' t2' \<upharpoonleft> A = t1' \<and> merge A B t1' t2' \<upharpoonleft> B = t2' \<and> set (merge A B t1' t2') \<subseteq> set t1' \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<in> A \<inter> B; set (e1 # t1') \<subseteq> A; set t2' \<subseteq> B; (e1 # t1') \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') t2' \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') t2' \<upharpoonleft> B = t2' \<and> set (merge A B (e1 # t1') t2') \<subseteq> set (e1 # t1') \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<notin> A \<inter> B; set t1' \<subseteq> A; set (e2 # t2') \<subseteq> B; t1' \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' (e2 # t2') \<upharpoonleft> A = t1' \<and> merge A B t1' (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B t1' (e2 # t2')) \<subseteq> set t1' \<union> set (e2 # t2'); set (e1 # t1') \<subseteq> A; set (e2 # t2') \<subseteq> B; (e1 # t1') \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
set (t1 # va_) \<subseteq> A
set [] \<subseteq> B
(t1 # va_) \<upharpoonleft> B = [] \<upharpoonleft> A

goal (1 subgoal):
 1. merge A B (t1 # va_) [] \<upharpoonleft> A = t1 # va_ \<and> merge A B (t1 # va_) [] \<upharpoonleft> B = [] \<and> set (merge A B (t1 # va_) []) \<subseteq> set (t1 # va_) \<union> set []
[PROOF STEP]
by (metis Un_empty_right empty_subsetI list_subset_iff_projection_neutral
      merge.simps(2) set_empty subset_refl)
[PROOF STATE]
proof (state)
this:
merge A B (t1 # va_) [] \<upharpoonleft> A = t1 # va_ \<and> merge A B (t1 # va_) [] \<upharpoonleft> B = [] \<and> set (merge A B (t1 # va_) []) \<subseteq> set (t1 # va_) \<union> set []

goal (1 subgoal):
 1. \<And>A B e1 t1' e2 t2'. \<lbrakk>\<lbrakk>e1 = e2; set t1' \<subseteq> A; set t2' \<subseteq> B; t1' \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' t2' \<upharpoonleft> A = t1' \<and> merge A B t1' t2' \<upharpoonleft> B = t2' \<and> set (merge A B t1' t2') \<subseteq> set t1' \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<in> A \<inter> B; set (e1 # t1') \<subseteq> A; set t2' \<subseteq> B; (e1 # t1') \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') t2' \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') t2' \<upharpoonleft> B = t2' \<and> set (merge A B (e1 # t1') t2') \<subseteq> set (e1 # t1') \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<notin> A \<inter> B; set t1' \<subseteq> A; set (e2 # t2') \<subseteq> B; t1' \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' (e2 # t2') \<upharpoonleft> A = t1' \<and> merge A B t1' (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B t1' (e2 # t2')) \<subseteq> set t1' \<union> set (e2 # t2'); set (e1 # t1') \<subseteq> A; set (e2 # t2') \<subseteq> B; (e1 # t1') \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>A B e1 t1' e2 t2'. \<lbrakk>\<lbrakk>e1 = e2; set t1' \<subseteq> A; set t2' \<subseteq> B; t1' \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' t2' \<upharpoonleft> A = t1' \<and> merge A B t1' t2' \<upharpoonleft> B = t2' \<and> set (merge A B t1' t2') \<subseteq> set t1' \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<in> A \<inter> B; set (e1 # t1') \<subseteq> A; set t2' \<subseteq> B; (e1 # t1') \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') t2' \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') t2' \<upharpoonleft> B = t2' \<and> set (merge A B (e1 # t1') t2') \<subseteq> set (e1 # t1') \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<notin> A \<inter> B; set t1' \<subseteq> A; set (e2 # t2') \<subseteq> B; t1' \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' (e2 # t2') \<upharpoonleft> A = t1' \<and> merge A B t1' (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B t1' (e2 # t2')) \<subseteq> set t1' \<union> set (e2 # t2'); set (e1 # t1') \<subseteq> A; set (e2 # t2') \<subseteq> B; (e1 # t1') \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
case (3 A B e1 t1' e2 t2')
[PROOF STATE]
proof (state)
this:
\<lbrakk>e1 = e2; set t1' \<subseteq> A; set t2' \<subseteq> B; t1' \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' t2' \<upharpoonleft> A = t1' \<and> merge A B t1' t2' \<upharpoonleft> B = t2' \<and> set (merge A B t1' t2') \<subseteq> set t1' \<union> set t2'
\<lbrakk>e1 \<noteq> e2; e1 \<in> A \<inter> B; set (e1 # t1') \<subseteq> A; set t2' \<subseteq> B; (e1 # t1') \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') t2' \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') t2' \<upharpoonleft> B = t2' \<and> set (merge A B (e1 # t1') t2') \<subseteq> set (e1 # t1') \<union> set t2'
\<lbrakk>e1 \<noteq> e2; e1 \<notin> A \<inter> B; set t1' \<subseteq> A; set (e2 # t2') \<subseteq> B; t1' \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' (e2 # t2') \<upharpoonleft> A = t1' \<and> merge A B t1' (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B t1' (e2 # t2')) \<subseteq> set t1' \<union> set (e2 # t2')
set (e1 # t1') \<subseteq> A
set (e2 # t2') \<subseteq> B
(e1 # t1') \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A

goal (1 subgoal):
 1. \<And>A B e1 t1' e2 t2'. \<lbrakk>\<lbrakk>e1 = e2; set t1' \<subseteq> A; set t2' \<subseteq> B; t1' \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' t2' \<upharpoonleft> A = t1' \<and> merge A B t1' t2' \<upharpoonleft> B = t2' \<and> set (merge A B t1' t2') \<subseteq> set t1' \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<in> A \<inter> B; set (e1 # t1') \<subseteq> A; set t2' \<subseteq> B; (e1 # t1') \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') t2' \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') t2' \<upharpoonleft> B = t2' \<and> set (merge A B (e1 # t1') t2') \<subseteq> set (e1 # t1') \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<notin> A \<inter> B; set t1' \<subseteq> A; set (e2 # t2') \<subseteq> B; t1' \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' (e2 # t2') \<upharpoonleft> A = t1' \<and> merge A B t1' (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B t1' (e2 # t2')) \<subseteq> set t1' \<union> set (e2 # t2'); set (e1 # t1') \<subseteq> A; set (e2 # t2') \<subseteq> B; (e1 # t1') \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>e1 = e2; set t1' \<subseteq> A; set t2' \<subseteq> B; t1' \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' t2' \<upharpoonleft> A = t1' \<and> merge A B t1' t2' \<upharpoonleft> B = t2' \<and> set (merge A B t1' t2') \<subseteq> set t1' \<union> set t2'
\<lbrakk>e1 \<noteq> e2; e1 \<in> A \<inter> B; set (e1 # t1') \<subseteq> A; set t2' \<subseteq> B; (e1 # t1') \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') t2' \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') t2' \<upharpoonleft> B = t2' \<and> set (merge A B (e1 # t1') t2') \<subseteq> set (e1 # t1') \<union> set t2'
\<lbrakk>e1 \<noteq> e2; e1 \<notin> A \<inter> B; set t1' \<subseteq> A; set (e2 # t2') \<subseteq> B; t1' \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' (e2 # t2') \<upharpoonleft> A = t1' \<and> merge A B t1' (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B t1' (e2 # t2')) \<subseteq> set t1' \<union> set (e2 # t2')
set (e1 # t1') \<subseteq> A
set (e2 # t2') \<subseteq> B
(e1 # t1') \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A

goal (1 subgoal):
 1. merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>e1 = e2; set t1' \<subseteq> A; set t2' \<subseteq> B; t1' \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' t2' \<upharpoonleft> A = t1' \<and> merge A B t1' t2' \<upharpoonleft> B = t2' \<and> set (merge A B t1' t2') \<subseteq> set t1' \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<in> A \<inter> B; set (e1 # t1') \<subseteq> A; set t2' \<subseteq> B; (e1 # t1') \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') t2' \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') t2' \<upharpoonleft> B = t2' \<and> set (merge A B (e1 # t1') t2') \<subseteq> set (e1 # t1') \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<notin> A \<inter> B; set t1' \<subseteq> A; set (e2 # t2') \<subseteq> B; t1' \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' (e2 # t2') \<upharpoonleft> A = t1' \<and> merge A B t1' (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B t1' (e2 # t2')) \<subseteq> set t1' \<union> set (e2 # t2'); set (e1 # t1') \<subseteq> A; set (e2 # t2') \<subseteq> B; (e1 # t1') \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A; ?P6\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
 2. \<lbrakk>\<lbrakk>e1 = e2; set t1' \<subseteq> A; set t2' \<subseteq> B; t1' \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' t2' \<upharpoonleft> A = t1' \<and> merge A B t1' t2' \<upharpoonleft> B = t2' \<and> set (merge A B t1' t2') \<subseteq> set t1' \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<in> A \<inter> B; set (e1 # t1') \<subseteq> A; set t2' \<subseteq> B; (e1 # t1') \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') t2' \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') t2' \<upharpoonleft> B = t2' \<and> set (merge A B (e1 # t1') t2') \<subseteq> set (e1 # t1') \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<notin> A \<inter> B; set t1' \<subseteq> A; set (e2 # t2') \<subseteq> B; t1' \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' (e2 # t2') \<upharpoonleft> A = t1' \<and> merge A B t1' (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B t1' (e2 # t2')) \<subseteq> set t1' \<union> set (e2 # t2'); set (e1 # t1') \<subseteq> A; set (e2 # t2') \<subseteq> B; (e1 # t1') \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A; \<not> ?P6\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
assume e1_is_e2: "e1 = e2"
[PROOF STATE]
proof (state)
this:
e1 = e2

goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>e1 = e2; set t1' \<subseteq> A; set t2' \<subseteq> B; t1' \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' t2' \<upharpoonleft> A = t1' \<and> merge A B t1' t2' \<upharpoonleft> B = t2' \<and> set (merge A B t1' t2') \<subseteq> set t1' \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<in> A \<inter> B; set (e1 # t1') \<subseteq> A; set t2' \<subseteq> B; (e1 # t1') \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') t2' \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') t2' \<upharpoonleft> B = t2' \<and> set (merge A B (e1 # t1') t2') \<subseteq> set (e1 # t1') \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<notin> A \<inter> B; set t1' \<subseteq> A; set (e2 # t2') \<subseteq> B; t1' \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' (e2 # t2') \<upharpoonleft> A = t1' \<and> merge A B t1' (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B t1' (e2 # t2')) \<subseteq> set t1' \<union> set (e2 # t2'); set (e1 # t1') \<subseteq> A; set (e2 # t2') \<subseteq> B; (e1 # t1') \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A; ?P6\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
 2. \<lbrakk>\<lbrakk>e1 = e2; set t1' \<subseteq> A; set t2' \<subseteq> B; t1' \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' t2' \<upharpoonleft> A = t1' \<and> merge A B t1' t2' \<upharpoonleft> B = t2' \<and> set (merge A B t1' t2') \<subseteq> set t1' \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<in> A \<inter> B; set (e1 # t1') \<subseteq> A; set t2' \<subseteq> B; (e1 # t1') \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') t2' \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') t2' \<upharpoonleft> B = t2' \<and> set (merge A B (e1 # t1') t2') \<subseteq> set (e1 # t1') \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<notin> A \<inter> B; set t1' \<subseteq> A; set (e2 # t2') \<subseteq> B; t1' \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' (e2 # t2') \<upharpoonleft> A = t1' \<and> merge A B t1' (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B t1' (e2 # t2')) \<subseteq> set t1' \<union> set (e2 # t2'); set (e1 # t1') \<subseteq> A; set (e2 # t2') \<subseteq> B; (e1 # t1') \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A; \<not> ?P6\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
note e1_is_e2
[PROOF STATE]
proof (state)
this:
e1 = e2

goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>e1 = e2; set t1' \<subseteq> A; set t2' \<subseteq> B; t1' \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' t2' \<upharpoonleft> A = t1' \<and> merge A B t1' t2' \<upharpoonleft> B = t2' \<and> set (merge A B t1' t2') \<subseteq> set t1' \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<in> A \<inter> B; set (e1 # t1') \<subseteq> A; set t2' \<subseteq> B; (e1 # t1') \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') t2' \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') t2' \<upharpoonleft> B = t2' \<and> set (merge A B (e1 # t1') t2') \<subseteq> set (e1 # t1') \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<notin> A \<inter> B; set t1' \<subseteq> A; set (e2 # t2') \<subseteq> B; t1' \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' (e2 # t2') \<upharpoonleft> A = t1' \<and> merge A B t1' (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B t1' (e2 # t2')) \<subseteq> set t1' \<union> set (e2 # t2'); set (e1 # t1') \<subseteq> A; set (e2 # t2') \<subseteq> B; (e1 # t1') \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A; ?P6\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
 2. \<lbrakk>\<lbrakk>e1 = e2; set t1' \<subseteq> A; set t2' \<subseteq> B; t1' \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' t2' \<upharpoonleft> A = t1' \<and> merge A B t1' t2' \<upharpoonleft> B = t2' \<and> set (merge A B t1' t2') \<subseteq> set t1' \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<in> A \<inter> B; set (e1 # t1') \<subseteq> A; set t2' \<subseteq> B; (e1 # t1') \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') t2' \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') t2' \<upharpoonleft> B = t2' \<and> set (merge A B (e1 # t1') t2') \<subseteq> set (e1 # t1') \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<notin> A \<inter> B; set t1' \<subseteq> A; set (e2 # t2') \<subseteq> B; t1' \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' (e2 # t2') \<upharpoonleft> A = t1' \<and> merge A B t1' (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B t1' (e2 # t2')) \<subseteq> set t1' \<union> set (e2 # t2'); set (e1 # t1') \<subseteq> A; set (e2 # t2') \<subseteq> B; (e1 # t1') \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A; \<not> ?P6\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
e1 = e2

goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>e1 = e2; set t1' \<subseteq> A; set t2' \<subseteq> B; t1' \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' t2' \<upharpoonleft> A = t1' \<and> merge A B t1' t2' \<upharpoonleft> B = t2' \<and> set (merge A B t1' t2') \<subseteq> set t1' \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<in> A \<inter> B; set (e1 # t1') \<subseteq> A; set t2' \<subseteq> B; (e1 # t1') \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') t2' \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') t2' \<upharpoonleft> B = t2' \<and> set (merge A B (e1 # t1') t2') \<subseteq> set (e1 # t1') \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<notin> A \<inter> B; set t1' \<subseteq> A; set (e2 # t2') \<subseteq> B; t1' \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' (e2 # t2') \<upharpoonleft> A = t1' \<and> merge A B t1' (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B t1' (e2 # t2')) \<subseteq> set t1' \<union> set (e2 # t2'); set (e1 # t1') \<subseteq> A; set (e2 # t2') \<subseteq> B; (e1 # t1') \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A; ?P6\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
 2. \<lbrakk>\<lbrakk>e1 = e2; set t1' \<subseteq> A; set t2' \<subseteq> B; t1' \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' t2' \<upharpoonleft> A = t1' \<and> merge A B t1' t2' \<upharpoonleft> B = t2' \<and> set (merge A B t1' t2') \<subseteq> set t1' \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<in> A \<inter> B; set (e1 # t1') \<subseteq> A; set t2' \<subseteq> B; (e1 # t1') \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') t2' \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') t2' \<upharpoonleft> B = t2' \<and> set (merge A B (e1 # t1') t2') \<subseteq> set (e1 # t1') \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<notin> A \<inter> B; set t1' \<subseteq> A; set (e2 # t2') \<subseteq> B; t1' \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' (e2 # t2') \<upharpoonleft> A = t1' \<and> merge A B t1' (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B t1' (e2 # t2')) \<subseteq> set t1' \<union> set (e2 # t2'); set (e1 # t1') \<subseteq> A; set (e2 # t2') \<subseteq> B; (e1 # t1') \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A; \<not> ?P6\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
from 3(4)
[PROOF STATE]
proof (chain)
picking this:
set (e1 # t1') \<subseteq> A
[PROOF STEP]
have "set t1' \<subseteq> A"
[PROOF STATE]
proof (prove)
using this:
set (e1 # t1') \<subseteq> A

goal (1 subgoal):
 1. set t1' \<subseteq> A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set t1' \<subseteq> A

goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>e1 = e2; set t1' \<subseteq> A; set t2' \<subseteq> B; t1' \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' t2' \<upharpoonleft> A = t1' \<and> merge A B t1' t2' \<upharpoonleft> B = t2' \<and> set (merge A B t1' t2') \<subseteq> set t1' \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<in> A \<inter> B; set (e1 # t1') \<subseteq> A; set t2' \<subseteq> B; (e1 # t1') \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') t2' \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') t2' \<upharpoonleft> B = t2' \<and> set (merge A B (e1 # t1') t2') \<subseteq> set (e1 # t1') \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<notin> A \<inter> B; set t1' \<subseteq> A; set (e2 # t2') \<subseteq> B; t1' \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' (e2 # t2') \<upharpoonleft> A = t1' \<and> merge A B t1' (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B t1' (e2 # t2')) \<subseteq> set t1' \<union> set (e2 # t2'); set (e1 # t1') \<subseteq> A; set (e2 # t2') \<subseteq> B; (e1 # t1') \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A; ?P6\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
 2. \<lbrakk>\<lbrakk>e1 = e2; set t1' \<subseteq> A; set t2' \<subseteq> B; t1' \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' t2' \<upharpoonleft> A = t1' \<and> merge A B t1' t2' \<upharpoonleft> B = t2' \<and> set (merge A B t1' t2') \<subseteq> set t1' \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<in> A \<inter> B; set (e1 # t1') \<subseteq> A; set t2' \<subseteq> B; (e1 # t1') \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') t2' \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') t2' \<upharpoonleft> B = t2' \<and> set (merge A B (e1 # t1') t2') \<subseteq> set (e1 # t1') \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<notin> A \<inter> B; set t1' \<subseteq> A; set (e2 # t2') \<subseteq> B; t1' \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' (e2 # t2') \<upharpoonleft> A = t1' \<and> merge A B t1' (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B t1' (e2 # t2')) \<subseteq> set t1' \<union> set (e2 # t2'); set (e1 # t1') \<subseteq> A; set (e2 # t2') \<subseteq> B; (e1 # t1') \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A; \<not> ?P6\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set t1' \<subseteq> A

goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>e1 = e2; set t1' \<subseteq> A; set t2' \<subseteq> B; t1' \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' t2' \<upharpoonleft> A = t1' \<and> merge A B t1' t2' \<upharpoonleft> B = t2' \<and> set (merge A B t1' t2') \<subseteq> set t1' \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<in> A \<inter> B; set (e1 # t1') \<subseteq> A; set t2' \<subseteq> B; (e1 # t1') \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') t2' \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') t2' \<upharpoonleft> B = t2' \<and> set (merge A B (e1 # t1') t2') \<subseteq> set (e1 # t1') \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<notin> A \<inter> B; set t1' \<subseteq> A; set (e2 # t2') \<subseteq> B; t1' \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' (e2 # t2') \<upharpoonleft> A = t1' \<and> merge A B t1' (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B t1' (e2 # t2')) \<subseteq> set t1' \<union> set (e2 # t2'); set (e1 # t1') \<subseteq> A; set (e2 # t2') \<subseteq> B; (e1 # t1') \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A; ?P6\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
 2. \<lbrakk>\<lbrakk>e1 = e2; set t1' \<subseteq> A; set t2' \<subseteq> B; t1' \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' t2' \<upharpoonleft> A = t1' \<and> merge A B t1' t2' \<upharpoonleft> B = t2' \<and> set (merge A B t1' t2') \<subseteq> set t1' \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<in> A \<inter> B; set (e1 # t1') \<subseteq> A; set t2' \<subseteq> B; (e1 # t1') \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') t2' \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') t2' \<upharpoonleft> B = t2' \<and> set (merge A B (e1 # t1') t2') \<subseteq> set (e1 # t1') \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<notin> A \<inter> B; set t1' \<subseteq> A; set (e2 # t2') \<subseteq> B; t1' \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' (e2 # t2') \<upharpoonleft> A = t1' \<and> merge A B t1' (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B t1' (e2 # t2')) \<subseteq> set t1' \<union> set (e2 # t2'); set (e1 # t1') \<subseteq> A; set (e2 # t2') \<subseteq> B; (e1 # t1') \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A; \<not> ?P6\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
from 3(5)
[PROOF STATE]
proof (chain)
picking this:
set (e2 # t2') \<subseteq> B
[PROOF STEP]
have "set t2' \<subseteq> B"
[PROOF STATE]
proof (prove)
using this:
set (e2 # t2') \<subseteq> B

goal (1 subgoal):
 1. set t2' \<subseteq> B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set t2' \<subseteq> B

goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>e1 = e2; set t1' \<subseteq> A; set t2' \<subseteq> B; t1' \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' t2' \<upharpoonleft> A = t1' \<and> merge A B t1' t2' \<upharpoonleft> B = t2' \<and> set (merge A B t1' t2') \<subseteq> set t1' \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<in> A \<inter> B; set (e1 # t1') \<subseteq> A; set t2' \<subseteq> B; (e1 # t1') \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') t2' \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') t2' \<upharpoonleft> B = t2' \<and> set (merge A B (e1 # t1') t2') \<subseteq> set (e1 # t1') \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<notin> A \<inter> B; set t1' \<subseteq> A; set (e2 # t2') \<subseteq> B; t1' \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' (e2 # t2') \<upharpoonleft> A = t1' \<and> merge A B t1' (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B t1' (e2 # t2')) \<subseteq> set t1' \<union> set (e2 # t2'); set (e1 # t1') \<subseteq> A; set (e2 # t2') \<subseteq> B; (e1 # t1') \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A; ?P6\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
 2. \<lbrakk>\<lbrakk>e1 = e2; set t1' \<subseteq> A; set t2' \<subseteq> B; t1' \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' t2' \<upharpoonleft> A = t1' \<and> merge A B t1' t2' \<upharpoonleft> B = t2' \<and> set (merge A B t1' t2') \<subseteq> set t1' \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<in> A \<inter> B; set (e1 # t1') \<subseteq> A; set t2' \<subseteq> B; (e1 # t1') \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') t2' \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') t2' \<upharpoonleft> B = t2' \<and> set (merge A B (e1 # t1') t2') \<subseteq> set (e1 # t1') \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<notin> A \<inter> B; set t1' \<subseteq> A; set (e2 # t2') \<subseteq> B; t1' \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' (e2 # t2') \<upharpoonleft> A = t1' \<and> merge A B t1' (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B t1' (e2 # t2')) \<subseteq> set t1' \<union> set (e2 # t2'); set (e1 # t1') \<subseteq> A; set (e2 # t2') \<subseteq> B; (e1 # t1') \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A; \<not> ?P6\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set t2' \<subseteq> B

goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>e1 = e2; set t1' \<subseteq> A; set t2' \<subseteq> B; t1' \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' t2' \<upharpoonleft> A = t1' \<and> merge A B t1' t2' \<upharpoonleft> B = t2' \<and> set (merge A B t1' t2') \<subseteq> set t1' \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<in> A \<inter> B; set (e1 # t1') \<subseteq> A; set t2' \<subseteq> B; (e1 # t1') \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') t2' \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') t2' \<upharpoonleft> B = t2' \<and> set (merge A B (e1 # t1') t2') \<subseteq> set (e1 # t1') \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<notin> A \<inter> B; set t1' \<subseteq> A; set (e2 # t2') \<subseteq> B; t1' \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' (e2 # t2') \<upharpoonleft> A = t1' \<and> merge A B t1' (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B t1' (e2 # t2')) \<subseteq> set t1' \<union> set (e2 # t2'); set (e1 # t1') \<subseteq> A; set (e2 # t2') \<subseteq> B; (e1 # t1') \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A; ?P6\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
 2. \<lbrakk>\<lbrakk>e1 = e2; set t1' \<subseteq> A; set t2' \<subseteq> B; t1' \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' t2' \<upharpoonleft> A = t1' \<and> merge A B t1' t2' \<upharpoonleft> B = t2' \<and> set (merge A B t1' t2') \<subseteq> set t1' \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<in> A \<inter> B; set (e1 # t1') \<subseteq> A; set t2' \<subseteq> B; (e1 # t1') \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') t2' \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') t2' \<upharpoonleft> B = t2' \<and> set (merge A B (e1 # t1') t2') \<subseteq> set (e1 # t1') \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<notin> A \<inter> B; set t1' \<subseteq> A; set (e2 # t2') \<subseteq> B; t1' \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' (e2 # t2') \<upharpoonleft> A = t1' \<and> merge A B t1' (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B t1' (e2 # t2')) \<subseteq> set t1' \<union> set (e2 # t2'); set (e1 # t1') \<subseteq> A; set (e2 # t2') \<subseteq> B; (e1 # t1') \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A; \<not> ?P6\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
from e1_is_e2 3(4-6)
[PROOF STATE]
proof (chain)
picking this:
e1 = e2
set (e1 # t1') \<subseteq> A
set (e2 # t2') \<subseteq> B
(e1 # t1') \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A
[PROOF STEP]
have "t1' \<upharpoonleft> B = t2' \<upharpoonleft> A"
[PROOF STATE]
proof (prove)
using this:
e1 = e2
set (e1 # t1') \<subseteq> A
set (e2 # t2') \<subseteq> B
(e1 # t1') \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A

goal (1 subgoal):
 1. t1' \<upharpoonleft> B = t2' \<upharpoonleft> A
[PROOF STEP]
by (simp add: projection_def)
[PROOF STATE]
proof (state)
this:
t1' \<upharpoonleft> B = t2' \<upharpoonleft> A

goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>e1 = e2; set t1' \<subseteq> A; set t2' \<subseteq> B; t1' \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' t2' \<upharpoonleft> A = t1' \<and> merge A B t1' t2' \<upharpoonleft> B = t2' \<and> set (merge A B t1' t2') \<subseteq> set t1' \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<in> A \<inter> B; set (e1 # t1') \<subseteq> A; set t2' \<subseteq> B; (e1 # t1') \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') t2' \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') t2' \<upharpoonleft> B = t2' \<and> set (merge A B (e1 # t1') t2') \<subseteq> set (e1 # t1') \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<notin> A \<inter> B; set t1' \<subseteq> A; set (e2 # t2') \<subseteq> B; t1' \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' (e2 # t2') \<upharpoonleft> A = t1' \<and> merge A B t1' (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B t1' (e2 # t2')) \<subseteq> set t1' \<union> set (e2 # t2'); set (e1 # t1') \<subseteq> A; set (e2 # t2') \<subseteq> B; (e1 # t1') \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A; ?P6\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
 2. \<lbrakk>\<lbrakk>e1 = e2; set t1' \<subseteq> A; set t2' \<subseteq> B; t1' \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' t2' \<upharpoonleft> A = t1' \<and> merge A B t1' t2' \<upharpoonleft> B = t2' \<and> set (merge A B t1' t2') \<subseteq> set t1' \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<in> A \<inter> B; set (e1 # t1') \<subseteq> A; set t2' \<subseteq> B; (e1 # t1') \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') t2' \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') t2' \<upharpoonleft> B = t2' \<and> set (merge A B (e1 # t1') t2') \<subseteq> set (e1 # t1') \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<notin> A \<inter> B; set t1' \<subseteq> A; set (e2 # t2') \<subseteq> B; t1' \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' (e2 # t2') \<upharpoonleft> A = t1' \<and> merge A B t1' (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B t1' (e2 # t2')) \<subseteq> set t1' \<union> set (e2 # t2'); set (e1 # t1') \<subseteq> A; set (e2 # t2') \<subseteq> B; (e1 # t1') \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A; \<not> ?P6\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
t1' \<upharpoonleft> B = t2' \<upharpoonleft> A

goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>e1 = e2; set t1' \<subseteq> A; set t2' \<subseteq> B; t1' \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' t2' \<upharpoonleft> A = t1' \<and> merge A B t1' t2' \<upharpoonleft> B = t2' \<and> set (merge A B t1' t2') \<subseteq> set t1' \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<in> A \<inter> B; set (e1 # t1') \<subseteq> A; set t2' \<subseteq> B; (e1 # t1') \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') t2' \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') t2' \<upharpoonleft> B = t2' \<and> set (merge A B (e1 # t1') t2') \<subseteq> set (e1 # t1') \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<notin> A \<inter> B; set t1' \<subseteq> A; set (e2 # t2') \<subseteq> B; t1' \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' (e2 # t2') \<upharpoonleft> A = t1' \<and> merge A B t1' (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B t1' (e2 # t2')) \<subseteq> set t1' \<union> set (e2 # t2'); set (e1 # t1') \<subseteq> A; set (e2 # t2') \<subseteq> B; (e1 # t1') \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A; ?P6\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
 2. \<lbrakk>\<lbrakk>e1 = e2; set t1' \<subseteq> A; set t2' \<subseteq> B; t1' \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' t2' \<upharpoonleft> A = t1' \<and> merge A B t1' t2' \<upharpoonleft> B = t2' \<and> set (merge A B t1' t2') \<subseteq> set t1' \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<in> A \<inter> B; set (e1 # t1') \<subseteq> A; set t2' \<subseteq> B; (e1 # t1') \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') t2' \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') t2' \<upharpoonleft> B = t2' \<and> set (merge A B (e1 # t1') t2') \<subseteq> set (e1 # t1') \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<notin> A \<inter> B; set t1' \<subseteq> A; set (e2 # t2') \<subseteq> B; t1' \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' (e2 # t2') \<upharpoonleft> A = t1' \<and> merge A B t1' (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B t1' (e2 # t2')) \<subseteq> set t1' \<union> set (e2 # t2'); set (e1 # t1') \<subseteq> A; set (e2 # t2') \<subseteq> B; (e1 # t1') \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A; \<not> ?P6\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
note 3(1)
[PROOF STATE]
proof (state)
this:
\<lbrakk>e1 = e2; set t1' \<subseteq> A; set t2' \<subseteq> B; t1' \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' t2' \<upharpoonleft> A = t1' \<and> merge A B t1' t2' \<upharpoonleft> B = t2' \<and> set (merge A B t1' t2') \<subseteq> set t1' \<union> set t2'

goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>e1 = e2; set t1' \<subseteq> A; set t2' \<subseteq> B; t1' \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' t2' \<upharpoonleft> A = t1' \<and> merge A B t1' t2' \<upharpoonleft> B = t2' \<and> set (merge A B t1' t2') \<subseteq> set t1' \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<in> A \<inter> B; set (e1 # t1') \<subseteq> A; set t2' \<subseteq> B; (e1 # t1') \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') t2' \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') t2' \<upharpoonleft> B = t2' \<and> set (merge A B (e1 # t1') t2') \<subseteq> set (e1 # t1') \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<notin> A \<inter> B; set t1' \<subseteq> A; set (e2 # t2') \<subseteq> B; t1' \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' (e2 # t2') \<upharpoonleft> A = t1' \<and> merge A B t1' (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B t1' (e2 # t2')) \<subseteq> set t1' \<union> set (e2 # t2'); set (e1 # t1') \<subseteq> A; set (e2 # t2') \<subseteq> B; (e1 # t1') \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A; ?P6\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
 2. \<lbrakk>\<lbrakk>e1 = e2; set t1' \<subseteq> A; set t2' \<subseteq> B; t1' \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' t2' \<upharpoonleft> A = t1' \<and> merge A B t1' t2' \<upharpoonleft> B = t2' \<and> set (merge A B t1' t2') \<subseteq> set t1' \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<in> A \<inter> B; set (e1 # t1') \<subseteq> A; set t2' \<subseteq> B; (e1 # t1') \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') t2' \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') t2' \<upharpoonleft> B = t2' \<and> set (merge A B (e1 # t1') t2') \<subseteq> set (e1 # t1') \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<notin> A \<inter> B; set t1' \<subseteq> A; set (e2 # t2') \<subseteq> B; t1' \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' (e2 # t2') \<upharpoonleft> A = t1' \<and> merge A B t1' (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B t1' (e2 # t2')) \<subseteq> set t1' \<union> set (e2 # t2'); set (e1 # t1') \<subseteq> A; set (e2 # t2') \<subseteq> B; (e1 # t1') \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A; \<not> ?P6\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
e1 = e2
set t1' \<subseteq> A
set t2' \<subseteq> B
t1' \<upharpoonleft> B = t2' \<upharpoonleft> A
\<lbrakk>e1 = e2; set t1' \<subseteq> A; set t2' \<subseteq> B; t1' \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' t2' \<upharpoonleft> A = t1' \<and> merge A B t1' t2' \<upharpoonleft> B = t2' \<and> set (merge A B t1' t2') \<subseteq> set t1' \<union> set t2'
[PROOF STEP]
have ind1: "merge A B t1' t2' \<upharpoonleft> A = t1'"
      and ind2: "merge A B t1' t2' \<upharpoonleft> B = t2'"
      and ind3: "set (merge A B t1' t2') \<subseteq> (set t1') \<union> (set t2')"
[PROOF STATE]
proof (prove)
using this:
e1 = e2
set t1' \<subseteq> A
set t2' \<subseteq> B
t1' \<upharpoonleft> B = t2' \<upharpoonleft> A
\<lbrakk>e1 = e2; set t1' \<subseteq> A; set t2' \<subseteq> B; t1' \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' t2' \<upharpoonleft> A = t1' \<and> merge A B t1' t2' \<upharpoonleft> B = t2' \<and> set (merge A B t1' t2') \<subseteq> set t1' \<union> set t2'

goal (1 subgoal):
 1. merge A B t1' t2' \<upharpoonleft> A = t1' &&& merge A B t1' t2' \<upharpoonleft> B = t2' &&& set (merge A B t1' t2') \<subseteq> set t1' \<union> set t2'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
merge A B t1' t2' \<upharpoonleft> A = t1'
merge A B t1' t2' \<upharpoonleft> B = t2'
set (merge A B t1' t2') \<subseteq> set t1' \<union> set t2'

goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>e1 = e2; set t1' \<subseteq> A; set t2' \<subseteq> B; t1' \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' t2' \<upharpoonleft> A = t1' \<and> merge A B t1' t2' \<upharpoonleft> B = t2' \<and> set (merge A B t1' t2') \<subseteq> set t1' \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<in> A \<inter> B; set (e1 # t1') \<subseteq> A; set t2' \<subseteq> B; (e1 # t1') \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') t2' \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') t2' \<upharpoonleft> B = t2' \<and> set (merge A B (e1 # t1') t2') \<subseteq> set (e1 # t1') \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<notin> A \<inter> B; set t1' \<subseteq> A; set (e2 # t2') \<subseteq> B; t1' \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' (e2 # t2') \<upharpoonleft> A = t1' \<and> merge A B t1' (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B t1' (e2 # t2')) \<subseteq> set t1' \<union> set (e2 # t2'); set (e1 # t1') \<subseteq> A; set (e2 # t2') \<subseteq> B; (e1 # t1') \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A; ?P6\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
 2. \<lbrakk>\<lbrakk>e1 = e2; set t1' \<subseteq> A; set t2' \<subseteq> B; t1' \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' t2' \<upharpoonleft> A = t1' \<and> merge A B t1' t2' \<upharpoonleft> B = t2' \<and> set (merge A B t1' t2') \<subseteq> set t1' \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<in> A \<inter> B; set (e1 # t1') \<subseteq> A; set t2' \<subseteq> B; (e1 # t1') \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') t2' \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') t2' \<upharpoonleft> B = t2' \<and> set (merge A B (e1 # t1') t2') \<subseteq> set (e1 # t1') \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<notin> A \<inter> B; set t1' \<subseteq> A; set (e2 # t2') \<subseteq> B; t1' \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' (e2 # t2') \<upharpoonleft> A = t1' \<and> merge A B t1' (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B t1' (e2 # t2')) \<subseteq> set t1' \<union> set (e2 # t2'); set (e1 # t1') \<subseteq> A; set (e2 # t2') \<subseteq> B; (e1 # t1') \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A; \<not> ?P6\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
from e1_is_e2
[PROOF STATE]
proof (chain)
picking this:
e1 = e2
[PROOF STEP]
have merge_eq:
      "merge A B (e1 # t1') (e2 # t2') = e1 # (merge A B t1' t2')"
[PROOF STATE]
proof (prove)
using this:
e1 = e2

goal (1 subgoal):
 1. merge A B (e1 # t1') (e2 # t2') = e1 # merge A B t1' t2'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
merge A B (e1 # t1') (e2 # t2') = e1 # merge A B t1' t2'

goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>e1 = e2; set t1' \<subseteq> A; set t2' \<subseteq> B; t1' \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' t2' \<upharpoonleft> A = t1' \<and> merge A B t1' t2' \<upharpoonleft> B = t2' \<and> set (merge A B t1' t2') \<subseteq> set t1' \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<in> A \<inter> B; set (e1 # t1') \<subseteq> A; set t2' \<subseteq> B; (e1 # t1') \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') t2' \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') t2' \<upharpoonleft> B = t2' \<and> set (merge A B (e1 # t1') t2') \<subseteq> set (e1 # t1') \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<notin> A \<inter> B; set t1' \<subseteq> A; set (e2 # t2') \<subseteq> B; t1' \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' (e2 # t2') \<upharpoonleft> A = t1' \<and> merge A B t1' (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B t1' (e2 # t2')) \<subseteq> set t1' \<union> set (e2 # t2'); set (e1 # t1') \<subseteq> A; set (e2 # t2') \<subseteq> B; (e1 # t1') \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A; ?P6\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
 2. \<lbrakk>\<lbrakk>e1 = e2; set t1' \<subseteq> A; set t2' \<subseteq> B; t1' \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' t2' \<upharpoonleft> A = t1' \<and> merge A B t1' t2' \<upharpoonleft> B = t2' \<and> set (merge A B t1' t2') \<subseteq> set t1' \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<in> A \<inter> B; set (e1 # t1') \<subseteq> A; set t2' \<subseteq> B; (e1 # t1') \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') t2' \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') t2' \<upharpoonleft> B = t2' \<and> set (merge A B (e1 # t1') t2') \<subseteq> set (e1 # t1') \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<notin> A \<inter> B; set t1' \<subseteq> A; set (e2 # t2') \<subseteq> B; t1' \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' (e2 # t2') \<upharpoonleft> A = t1' \<and> merge A B t1' (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B t1' (e2 # t2')) \<subseteq> set t1' \<union> set (e2 # t2'); set (e1 # t1') \<subseteq> A; set (e2 # t2') \<subseteq> B; (e1 # t1') \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A; \<not> ?P6\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
from 3(4) ind1
[PROOF STATE]
proof (chain)
picking this:
set (e1 # t1') \<subseteq> A
merge A B t1' t2' \<upharpoonleft> A = t1'
[PROOF STEP]
have goal1:
      "merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1'"
[PROOF STATE]
proof (prove)
using this:
set (e1 # t1') \<subseteq> A
merge A B t1' t2' \<upharpoonleft> A = t1'

goal (1 subgoal):
 1. merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1'
[PROOF STEP]
by (simp only: merge_eq projection_def, auto)
[PROOF STATE]
proof (state)
this:
merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1'

goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>e1 = e2; set t1' \<subseteq> A; set t2' \<subseteq> B; t1' \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' t2' \<upharpoonleft> A = t1' \<and> merge A B t1' t2' \<upharpoonleft> B = t2' \<and> set (merge A B t1' t2') \<subseteq> set t1' \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<in> A \<inter> B; set (e1 # t1') \<subseteq> A; set t2' \<subseteq> B; (e1 # t1') \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') t2' \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') t2' \<upharpoonleft> B = t2' \<and> set (merge A B (e1 # t1') t2') \<subseteq> set (e1 # t1') \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<notin> A \<inter> B; set t1' \<subseteq> A; set (e2 # t2') \<subseteq> B; t1' \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' (e2 # t2') \<upharpoonleft> A = t1' \<and> merge A B t1' (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B t1' (e2 # t2')) \<subseteq> set t1' \<union> set (e2 # t2'); set (e1 # t1') \<subseteq> A; set (e2 # t2') \<subseteq> B; (e1 # t1') \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A; ?P6\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
 2. \<lbrakk>\<lbrakk>e1 = e2; set t1' \<subseteq> A; set t2' \<subseteq> B; t1' \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' t2' \<upharpoonleft> A = t1' \<and> merge A B t1' t2' \<upharpoonleft> B = t2' \<and> set (merge A B t1' t2') \<subseteq> set t1' \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<in> A \<inter> B; set (e1 # t1') \<subseteq> A; set t2' \<subseteq> B; (e1 # t1') \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') t2' \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') t2' \<upharpoonleft> B = t2' \<and> set (merge A B (e1 # t1') t2') \<subseteq> set (e1 # t1') \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<notin> A \<inter> B; set t1' \<subseteq> A; set (e2 # t2') \<subseteq> B; t1' \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' (e2 # t2') \<upharpoonleft> A = t1' \<and> merge A B t1' (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B t1' (e2 # t2')) \<subseteq> set t1' \<union> set (e2 # t2'); set (e1 # t1') \<subseteq> A; set (e2 # t2') \<subseteq> B; (e1 # t1') \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A; \<not> ?P6\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1'

goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>e1 = e2; set t1' \<subseteq> A; set t2' \<subseteq> B; t1' \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' t2' \<upharpoonleft> A = t1' \<and> merge A B t1' t2' \<upharpoonleft> B = t2' \<and> set (merge A B t1' t2') \<subseteq> set t1' \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<in> A \<inter> B; set (e1 # t1') \<subseteq> A; set t2' \<subseteq> B; (e1 # t1') \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') t2' \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') t2' \<upharpoonleft> B = t2' \<and> set (merge A B (e1 # t1') t2') \<subseteq> set (e1 # t1') \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<notin> A \<inter> B; set t1' \<subseteq> A; set (e2 # t2') \<subseteq> B; t1' \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' (e2 # t2') \<upharpoonleft> A = t1' \<and> merge A B t1' (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B t1' (e2 # t2')) \<subseteq> set t1' \<union> set (e2 # t2'); set (e1 # t1') \<subseteq> A; set (e2 # t2') \<subseteq> B; (e1 # t1') \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A; ?P6\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
 2. \<lbrakk>\<lbrakk>e1 = e2; set t1' \<subseteq> A; set t2' \<subseteq> B; t1' \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' t2' \<upharpoonleft> A = t1' \<and> merge A B t1' t2' \<upharpoonleft> B = t2' \<and> set (merge A B t1' t2') \<subseteq> set t1' \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<in> A \<inter> B; set (e1 # t1') \<subseteq> A; set t2' \<subseteq> B; (e1 # t1') \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') t2' \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') t2' \<upharpoonleft> B = t2' \<and> set (merge A B (e1 # t1') t2') \<subseteq> set (e1 # t1') \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<notin> A \<inter> B; set t1' \<subseteq> A; set (e2 # t2') \<subseteq> B; t1' \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' (e2 # t2') \<upharpoonleft> A = t1' \<and> merge A B t1' (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B t1' (e2 # t2')) \<subseteq> set t1' \<union> set (e2 # t2'); set (e1 # t1') \<subseteq> A; set (e2 # t2') \<subseteq> B; (e1 # t1') \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A; \<not> ?P6\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
from e1_is_e2 3(5) ind2
[PROOF STATE]
proof (chain)
picking this:
e1 = e2
set (e2 # t2') \<subseteq> B
merge A B t1' t2' \<upharpoonleft> B = t2'
[PROOF STEP]
have goal2:
      "merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2'"
[PROOF STATE]
proof (prove)
using this:
e1 = e2
set (e2 # t2') \<subseteq> B
merge A B t1' t2' \<upharpoonleft> B = t2'

goal (1 subgoal):
 1. merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2'
[PROOF STEP]
by (simp only: merge_eq projection_def, auto)
[PROOF STATE]
proof (state)
this:
merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2'

goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>e1 = e2; set t1' \<subseteq> A; set t2' \<subseteq> B; t1' \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' t2' \<upharpoonleft> A = t1' \<and> merge A B t1' t2' \<upharpoonleft> B = t2' \<and> set (merge A B t1' t2') \<subseteq> set t1' \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<in> A \<inter> B; set (e1 # t1') \<subseteq> A; set t2' \<subseteq> B; (e1 # t1') \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') t2' \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') t2' \<upharpoonleft> B = t2' \<and> set (merge A B (e1 # t1') t2') \<subseteq> set (e1 # t1') \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<notin> A \<inter> B; set t1' \<subseteq> A; set (e2 # t2') \<subseteq> B; t1' \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' (e2 # t2') \<upharpoonleft> A = t1' \<and> merge A B t1' (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B t1' (e2 # t2')) \<subseteq> set t1' \<union> set (e2 # t2'); set (e1 # t1') \<subseteq> A; set (e2 # t2') \<subseteq> B; (e1 # t1') \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A; ?P6\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
 2. \<lbrakk>\<lbrakk>e1 = e2; set t1' \<subseteq> A; set t2' \<subseteq> B; t1' \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' t2' \<upharpoonleft> A = t1' \<and> merge A B t1' t2' \<upharpoonleft> B = t2' \<and> set (merge A B t1' t2') \<subseteq> set t1' \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<in> A \<inter> B; set (e1 # t1') \<subseteq> A; set t2' \<subseteq> B; (e1 # t1') \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') t2' \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') t2' \<upharpoonleft> B = t2' \<and> set (merge A B (e1 # t1') t2') \<subseteq> set (e1 # t1') \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<notin> A \<inter> B; set t1' \<subseteq> A; set (e2 # t2') \<subseteq> B; t1' \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' (e2 # t2') \<upharpoonleft> A = t1' \<and> merge A B t1' (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B t1' (e2 # t2')) \<subseteq> set t1' \<union> set (e2 # t2'); set (e1 # t1') \<subseteq> A; set (e2 # t2') \<subseteq> B; (e1 # t1') \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A; \<not> ?P6\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2'

goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>e1 = e2; set t1' \<subseteq> A; set t2' \<subseteq> B; t1' \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' t2' \<upharpoonleft> A = t1' \<and> merge A B t1' t2' \<upharpoonleft> B = t2' \<and> set (merge A B t1' t2') \<subseteq> set t1' \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<in> A \<inter> B; set (e1 # t1') \<subseteq> A; set t2' \<subseteq> B; (e1 # t1') \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') t2' \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') t2' \<upharpoonleft> B = t2' \<and> set (merge A B (e1 # t1') t2') \<subseteq> set (e1 # t1') \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<notin> A \<inter> B; set t1' \<subseteq> A; set (e2 # t2') \<subseteq> B; t1' \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' (e2 # t2') \<upharpoonleft> A = t1' \<and> merge A B t1' (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B t1' (e2 # t2')) \<subseteq> set t1' \<union> set (e2 # t2'); set (e1 # t1') \<subseteq> A; set (e2 # t2') \<subseteq> B; (e1 # t1') \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A; ?P6\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
 2. \<lbrakk>\<lbrakk>e1 = e2; set t1' \<subseteq> A; set t2' \<subseteq> B; t1' \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' t2' \<upharpoonleft> A = t1' \<and> merge A B t1' t2' \<upharpoonleft> B = t2' \<and> set (merge A B t1' t2') \<subseteq> set t1' \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<in> A \<inter> B; set (e1 # t1') \<subseteq> A; set t2' \<subseteq> B; (e1 # t1') \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') t2' \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') t2' \<upharpoonleft> B = t2' \<and> set (merge A B (e1 # t1') t2') \<subseteq> set (e1 # t1') \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<notin> A \<inter> B; set t1' \<subseteq> A; set (e2 # t2') \<subseteq> B; t1' \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' (e2 # t2') \<upharpoonleft> A = t1' \<and> merge A B t1' (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B t1' (e2 # t2')) \<subseteq> set t1' \<union> set (e2 # t2'); set (e1 # t1') \<subseteq> A; set (e2 # t2') \<subseteq> B; (e1 # t1') \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A; \<not> ?P6\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
from ind3
[PROOF STATE]
proof (chain)
picking this:
set (merge A B t1' t2') \<subseteq> set t1' \<union> set t2'
[PROOF STEP]
have goal3:
      "set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')"
[PROOF STATE]
proof (prove)
using this:
set (merge A B t1' t2') \<subseteq> set t1' \<union> set t2'

goal (1 subgoal):
 1. set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
by (simp only: merge_eq, auto)
[PROOF STATE]
proof (state)
this:
set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')

goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>e1 = e2; set t1' \<subseteq> A; set t2' \<subseteq> B; t1' \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' t2' \<upharpoonleft> A = t1' \<and> merge A B t1' t2' \<upharpoonleft> B = t2' \<and> set (merge A B t1' t2') \<subseteq> set t1' \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<in> A \<inter> B; set (e1 # t1') \<subseteq> A; set t2' \<subseteq> B; (e1 # t1') \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') t2' \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') t2' \<upharpoonleft> B = t2' \<and> set (merge A B (e1 # t1') t2') \<subseteq> set (e1 # t1') \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<notin> A \<inter> B; set t1' \<subseteq> A; set (e2 # t2') \<subseteq> B; t1' \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' (e2 # t2') \<upharpoonleft> A = t1' \<and> merge A B t1' (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B t1' (e2 # t2')) \<subseteq> set t1' \<union> set (e2 # t2'); set (e1 # t1') \<subseteq> A; set (e2 # t2') \<subseteq> B; (e1 # t1') \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A; ?P6\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
 2. \<lbrakk>\<lbrakk>e1 = e2; set t1' \<subseteq> A; set t2' \<subseteq> B; t1' \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' t2' \<upharpoonleft> A = t1' \<and> merge A B t1' t2' \<upharpoonleft> B = t2' \<and> set (merge A B t1' t2') \<subseteq> set t1' \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<in> A \<inter> B; set (e1 # t1') \<subseteq> A; set t2' \<subseteq> B; (e1 # t1') \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') t2' \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') t2' \<upharpoonleft> B = t2' \<and> set (merge A B (e1 # t1') t2') \<subseteq> set (e1 # t1') \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<notin> A \<inter> B; set t1' \<subseteq> A; set (e2 # t2') \<subseteq> B; t1' \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' (e2 # t2') \<upharpoonleft> A = t1' \<and> merge A B t1' (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B t1' (e2 # t2')) \<subseteq> set t1' \<union> set (e2 # t2'); set (e1 # t1') \<subseteq> A; set (e2 # t2') \<subseteq> B; (e1 # t1') \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A; \<not> ?P6\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1'
merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2'
set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1'
merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2'
set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')

goal (1 subgoal):
 1. merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>e1 = e2; set t1' \<subseteq> A; set t2' \<subseteq> B; t1' \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' t2' \<upharpoonleft> A = t1' \<and> merge A B t1' t2' \<upharpoonleft> B = t2' \<and> set (merge A B t1' t2') \<subseteq> set t1' \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<in> A \<inter> B; set (e1 # t1') \<subseteq> A; set t2' \<subseteq> B; (e1 # t1') \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') t2' \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') t2' \<upharpoonleft> B = t2' \<and> set (merge A B (e1 # t1') t2') \<subseteq> set (e1 # t1') \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<notin> A \<inter> B; set t1' \<subseteq> A; set (e2 # t2') \<subseteq> B; t1' \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' (e2 # t2') \<upharpoonleft> A = t1' \<and> merge A B t1' (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B t1' (e2 # t2')) \<subseteq> set t1' \<union> set (e2 # t2'); set (e1 # t1') \<subseteq> A; set (e2 # t2') \<subseteq> B; (e1 # t1') \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A; e1 \<noteq> e2\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
(* case (3 e1 t1' e2 t2') for e1 = e2 *)
[PROOF STATE]
proof (state)
this:
merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>e1 = e2; set t1' \<subseteq> A; set t2' \<subseteq> B; t1' \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' t2' \<upharpoonleft> A = t1' \<and> merge A B t1' t2' \<upharpoonleft> B = t2' \<and> set (merge A B t1' t2') \<subseteq> set t1' \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<in> A \<inter> B; set (e1 # t1') \<subseteq> A; set t2' \<subseteq> B; (e1 # t1') \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') t2' \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') t2' \<upharpoonleft> B = t2' \<and> set (merge A B (e1 # t1') t2') \<subseteq> set (e1 # t1') \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<notin> A \<inter> B; set t1' \<subseteq> A; set (e2 # t2') \<subseteq> B; t1' \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' (e2 # t2') \<upharpoonleft> A = t1' \<and> merge A B t1' (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B t1' (e2 # t2')) \<subseteq> set t1' \<union> set (e2 # t2'); set (e1 # t1') \<subseteq> A; set (e2 # t2') \<subseteq> B; (e1 # t1') \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A; e1 \<noteq> e2\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>e1 = e2; set t1' \<subseteq> A; set t2' \<subseteq> B; t1' \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' t2' \<upharpoonleft> A = t1' \<and> merge A B t1' t2' \<upharpoonleft> B = t2' \<and> set (merge A B t1' t2') \<subseteq> set t1' \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<in> A \<inter> B; set (e1 # t1') \<subseteq> A; set t2' \<subseteq> B; (e1 # t1') \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') t2' \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') t2' \<upharpoonleft> B = t2' \<and> set (merge A B (e1 # t1') t2') \<subseteq> set (e1 # t1') \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<notin> A \<inter> B; set t1' \<subseteq> A; set (e2 # t2') \<subseteq> B; t1' \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' (e2 # t2') \<upharpoonleft> A = t1' \<and> merge A B t1' (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B t1' (e2 # t2')) \<subseteq> set t1' \<union> set (e2 # t2'); set (e1 # t1') \<subseteq> A; set (e2 # t2') \<subseteq> B; (e1 # t1') \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A; e1 \<noteq> e2\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
assume e1_isnot_e2: "e1 \<noteq> e2"
[PROOF STATE]
proof (state)
this:
e1 \<noteq> e2

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>e1 = e2; set t1' \<subseteq> A; set t2' \<subseteq> B; t1' \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' t2' \<upharpoonleft> A = t1' \<and> merge A B t1' t2' \<upharpoonleft> B = t2' \<and> set (merge A B t1' t2') \<subseteq> set t1' \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<in> A \<inter> B; set (e1 # t1') \<subseteq> A; set t2' \<subseteq> B; (e1 # t1') \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') t2' \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') t2' \<upharpoonleft> B = t2' \<and> set (merge A B (e1 # t1') t2') \<subseteq> set (e1 # t1') \<union> set t2'; \<lbrakk>e1 \<noteq> e2; e1 \<notin> A \<inter> B; set t1' \<subseteq> A; set (e2 # t2') \<subseteq> B; t1' \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' (e2 # t2') \<upharpoonleft> A = t1' \<and> merge A B t1' (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B t1' (e2 # t2')) \<subseteq> set t1' \<union> set (e2 # t2'); set (e1 # t1') \<subseteq> A; set (e2 # t2') \<subseteq> B; (e1 # t1') \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A; e1 \<noteq> e2\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
 2. \<not> ?P \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
assume e1_in_A_inter_B: "e1 \<in> A \<inter> B"
[PROOF STATE]
proof (state)
this:
e1 \<in> A \<inter> B

goal (2 subgoals):
 1. ?P \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
 2. \<not> ?P \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
from 3(6) e1_isnot_e2 e1_in_A_inter_B
[PROOF STATE]
proof (chain)
picking this:
(e1 # t1') \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A
e1 \<noteq> e2
e1 \<in> A \<inter> B
[PROOF STEP]
have e2_notin_A: "e2 \<notin> A"
[PROOF STATE]
proof (prove)
using this:
(e1 # t1') \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A
e1 \<noteq> e2
e1 \<in> A \<inter> B

goal (1 subgoal):
 1. e2 \<notin> A
[PROOF STEP]
by (simp add: projection_def, auto)
[PROOF STATE]
proof (state)
this:
e2 \<notin> A

goal (2 subgoals):
 1. ?P \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
 2. \<not> ?P \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
note e1_isnot_e2 e1_in_A_inter_B 3(4)
[PROOF STATE]
proof (state)
this:
e1 \<noteq> e2
e1 \<in> A \<inter> B
set (e1 # t1') \<subseteq> A

goal (2 subgoals):
 1. ?P \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
 2. \<not> ?P \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
e1 \<noteq> e2
e1 \<in> A \<inter> B
set (e1 # t1') \<subseteq> A

goal (2 subgoals):
 1. ?P \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
 2. \<not> ?P \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
from 3(5)
[PROOF STATE]
proof (chain)
picking this:
set (e2 # t2') \<subseteq> B
[PROOF STEP]
have "set t2' \<subseteq> B"
[PROOF STATE]
proof (prove)
using this:
set (e2 # t2') \<subseteq> B

goal (1 subgoal):
 1. set t2' \<subseteq> B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set t2' \<subseteq> B

goal (2 subgoals):
 1. ?P \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
 2. \<not> ?P \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set t2' \<subseteq> B

goal (2 subgoals):
 1. ?P \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
 2. \<not> ?P \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
from 3(6) e1_isnot_e2 e1_in_A_inter_B
[PROOF STATE]
proof (chain)
picking this:
(e1 # t1') \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A
e1 \<noteq> e2
e1 \<in> A \<inter> B
[PROOF STEP]
have "(e1 # t1') \<upharpoonleft> B = t2' \<upharpoonleft> A"
[PROOF STATE]
proof (prove)
using this:
(e1 # t1') \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A
e1 \<noteq> e2
e1 \<in> A \<inter> B

goal (1 subgoal):
 1. (e1 # t1') \<upharpoonleft> B = t2' \<upharpoonleft> A
[PROOF STEP]
by (simp add: projection_def, auto)
[PROOF STATE]
proof (state)
this:
(e1 # t1') \<upharpoonleft> B = t2' \<upharpoonleft> A

goal (2 subgoals):
 1. ?P \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
 2. \<not> ?P \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(e1 # t1') \<upharpoonleft> B = t2' \<upharpoonleft> A

goal (2 subgoals):
 1. ?P \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
 2. \<not> ?P \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
note 3(2)
[PROOF STATE]
proof (state)
this:
\<lbrakk>e1 \<noteq> e2; e1 \<in> A \<inter> B; set (e1 # t1') \<subseteq> A; set t2' \<subseteq> B; (e1 # t1') \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') t2' \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') t2' \<upharpoonleft> B = t2' \<and> set (merge A B (e1 # t1') t2') \<subseteq> set (e1 # t1') \<union> set t2'

goal (2 subgoals):
 1. ?P \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
 2. \<not> ?P \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
e1 \<noteq> e2
e1 \<in> A \<inter> B
set (e1 # t1') \<subseteq> A
set t2' \<subseteq> B
(e1 # t1') \<upharpoonleft> B = t2' \<upharpoonleft> A
\<lbrakk>e1 \<noteq> e2; e1 \<in> A \<inter> B; set (e1 # t1') \<subseteq> A; set t2' \<subseteq> B; (e1 # t1') \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') t2' \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') t2' \<upharpoonleft> B = t2' \<and> set (merge A B (e1 # t1') t2') \<subseteq> set (e1 # t1') \<union> set t2'
[PROOF STEP]
have ind1: "merge A B (e1 # t1') t2' \<upharpoonleft> A = (e1 # t1')"
        and ind2: "merge A B (e1 # t1') t2' \<upharpoonleft> B = t2'"
        and ind3: "set (merge A B (e1 # t1') t2') \<subseteq> set (e1 # t1') \<union> set t2'"
[PROOF STATE]
proof (prove)
using this:
e1 \<noteq> e2
e1 \<in> A \<inter> B
set (e1 # t1') \<subseteq> A
set t2' \<subseteq> B
(e1 # t1') \<upharpoonleft> B = t2' \<upharpoonleft> A
\<lbrakk>e1 \<noteq> e2; e1 \<in> A \<inter> B; set (e1 # t1') \<subseteq> A; set t2' \<subseteq> B; (e1 # t1') \<upharpoonleft> B = t2' \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B (e1 # t1') t2' \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') t2' \<upharpoonleft> B = t2' \<and> set (merge A B (e1 # t1') t2') \<subseteq> set (e1 # t1') \<union> set t2'

goal (1 subgoal):
 1. merge A B (e1 # t1') t2' \<upharpoonleft> A = e1 # t1' &&& merge A B (e1 # t1') t2' \<upharpoonleft> B = t2' &&& set (merge A B (e1 # t1') t2') \<subseteq> set (e1 # t1') \<union> set t2'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
merge A B (e1 # t1') t2' \<upharpoonleft> A = e1 # t1'
merge A B (e1 # t1') t2' \<upharpoonleft> B = t2'
set (merge A B (e1 # t1') t2') \<subseteq> set (e1 # t1') \<union> set t2'

goal (2 subgoals):
 1. ?P \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
 2. \<not> ?P \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
from e1_isnot_e2 e1_in_A_inter_B
[PROOF STATE]
proof (chain)
picking this:
e1 \<noteq> e2
e1 \<in> A \<inter> B
[PROOF STEP]
have merge_eq:
        "merge A B (e1 # t1') (e2 # t2') = e2 # (merge A B (e1 # t1') t2')"
[PROOF STATE]
proof (prove)
using this:
e1 \<noteq> e2
e1 \<in> A \<inter> B

goal (1 subgoal):
 1. merge A B (e1 # t1') (e2 # t2') = e2 # merge A B (e1 # t1') t2'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
merge A B (e1 # t1') (e2 # t2') = e2 # merge A B (e1 # t1') t2'

goal (2 subgoals):
 1. ?P \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
 2. \<not> ?P \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
from e1_isnot_e2 ind1 e2_notin_A
[PROOF STATE]
proof (chain)
picking this:
e1 \<noteq> e2
merge A B (e1 # t1') t2' \<upharpoonleft> A = e1 # t1'
e2 \<notin> A
[PROOF STEP]
have goal1:
        "merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1'"
[PROOF STATE]
proof (prove)
using this:
e1 \<noteq> e2
merge A B (e1 # t1') t2' \<upharpoonleft> A = e1 # t1'
e2 \<notin> A

goal (1 subgoal):
 1. merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1'
[PROOF STEP]
by (simp only: merge_eq projection_def, auto)
[PROOF STATE]
proof (state)
this:
merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1'

goal (2 subgoals):
 1. ?P \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
 2. \<not> ?P \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1'

goal (2 subgoals):
 1. ?P \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
 2. \<not> ?P \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
from 3(5) ind2
[PROOF STATE]
proof (chain)
picking this:
set (e2 # t2') \<subseteq> B
merge A B (e1 # t1') t2' \<upharpoonleft> B = t2'
[PROOF STEP]
have goal2: "merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2'"
[PROOF STATE]
proof (prove)
using this:
set (e2 # t2') \<subseteq> B
merge A B (e1 # t1') t2' \<upharpoonleft> B = t2'

goal (1 subgoal):
 1. merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2'
[PROOF STEP]
by (simp only: merge_eq projection_def, auto)
[PROOF STATE]
proof (state)
this:
merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2'

goal (2 subgoals):
 1. ?P \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
 2. \<not> ?P \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2'

goal (2 subgoals):
 1. ?P \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
 2. \<not> ?P \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
from 3(5) ind3
[PROOF STATE]
proof (chain)
picking this:
set (e2 # t2') \<subseteq> B
set (merge A B (e1 # t1') t2') \<subseteq> set (e1 # t1') \<union> set t2'
[PROOF STEP]
have goal3:
        "set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')"
[PROOF STATE]
proof (prove)
using this:
set (e2 # t2') \<subseteq> B
set (merge A B (e1 # t1') t2') \<subseteq> set (e1 # t1') \<union> set t2'

goal (1 subgoal):
 1. set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
by (simp only: merge_eq, auto)
[PROOF STATE]
proof (state)
this:
set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')

goal (2 subgoals):
 1. ?P \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
 2. \<not> ?P \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1'
merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2'
set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1'
merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2'
set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')

goal (1 subgoal):
 1. merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')

goal (1 subgoal):
 1. e1 \<notin> A \<inter> B \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
(* case (3 e1 t1' e2 t2') for e1 \<noteq> e2 e1 \<in> A \<inter> B *)
[PROOF STATE]
proof (state)
this:
merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')

goal (1 subgoal):
 1. e1 \<notin> A \<inter> B \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. e1 \<notin> A \<inter> B \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
assume e1_notin_A_inter_B: "e1 \<notin> A \<inter> B"
[PROOF STATE]
proof (state)
this:
e1 \<notin> A \<inter> B

goal (1 subgoal):
 1. e1 \<notin> A \<inter> B \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
from 3(4) e1_notin_A_inter_B
[PROOF STATE]
proof (chain)
picking this:
set (e1 # t1') \<subseteq> A
e1 \<notin> A \<inter> B
[PROOF STEP]
have e1_notin_B: "e1 \<notin> B"
[PROOF STATE]
proof (prove)
using this:
set (e1 # t1') \<subseteq> A
e1 \<notin> A \<inter> B

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

goal (1 subgoal):
 1. e1 \<notin> A \<inter> B \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
note e1_isnot_e2 e1_notin_A_inter_B
[PROOF STATE]
proof (state)
this:
e1 \<noteq> e2
e1 \<notin> A \<inter> B

goal (1 subgoal):
 1. e1 \<notin> A \<inter> B \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
e1 \<noteq> e2
e1 \<notin> A \<inter> B

goal (1 subgoal):
 1. e1 \<notin> A \<inter> B \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
from 3(4)
[PROOF STATE]
proof (chain)
picking this:
set (e1 # t1') \<subseteq> A
[PROOF STEP]
have "set t1' \<subseteq> A"
[PROOF STATE]
proof (prove)
using this:
set (e1 # t1') \<subseteq> A

goal (1 subgoal):
 1. set t1' \<subseteq> A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set t1' \<subseteq> A

goal (1 subgoal):
 1. e1 \<notin> A \<inter> B \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set t1' \<subseteq> A

goal (1 subgoal):
 1. e1 \<notin> A \<inter> B \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
note 3(5)
[PROOF STATE]
proof (state)
this:
set (e2 # t2') \<subseteq> B

goal (1 subgoal):
 1. e1 \<notin> A \<inter> B \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set (e2 # t2') \<subseteq> B

goal (1 subgoal):
 1. e1 \<notin> A \<inter> B \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
from 3(6) e1_notin_B
[PROOF STATE]
proof (chain)
picking this:
(e1 # t1') \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A
e1 \<notin> B
[PROOF STEP]
have "t1' \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A"
[PROOF STATE]
proof (prove)
using this:
(e1 # t1') \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A
e1 \<notin> B

goal (1 subgoal):
 1. t1' \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A
[PROOF STEP]
by (simp add: projection_def)
[PROOF STATE]
proof (state)
this:
t1' \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A

goal (1 subgoal):
 1. e1 \<notin> A \<inter> B \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
t1' \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A

goal (1 subgoal):
 1. e1 \<notin> A \<inter> B \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
note 3(3)
[PROOF STATE]
proof (state)
this:
\<lbrakk>e1 \<noteq> e2; e1 \<notin> A \<inter> B; set t1' \<subseteq> A; set (e2 # t2') \<subseteq> B; t1' \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' (e2 # t2') \<upharpoonleft> A = t1' \<and> merge A B t1' (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B t1' (e2 # t2')) \<subseteq> set t1' \<union> set (e2 # t2')

goal (1 subgoal):
 1. e1 \<notin> A \<inter> B \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
e1 \<noteq> e2
e1 \<notin> A \<inter> B
set t1' \<subseteq> A
set (e2 # t2') \<subseteq> B
t1' \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A
\<lbrakk>e1 \<noteq> e2; e1 \<notin> A \<inter> B; set t1' \<subseteq> A; set (e2 # t2') \<subseteq> B; t1' \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' (e2 # t2') \<upharpoonleft> A = t1' \<and> merge A B t1' (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B t1' (e2 # t2')) \<subseteq> set t1' \<union> set (e2 # t2')
[PROOF STEP]
have ind1: "merge A B t1' (e2 # t2') \<upharpoonleft> A = t1'"
        and ind2: "merge A B t1' (e2 # t2') \<upharpoonleft> B = (e2 # t2')"
        and ind3: "set (merge A B t1' (e2 # t2')) \<subseteq> set t1' \<union> set (e2 # t2')"
[PROOF STATE]
proof (prove)
using this:
e1 \<noteq> e2
e1 \<notin> A \<inter> B
set t1' \<subseteq> A
set (e2 # t2') \<subseteq> B
t1' \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A
\<lbrakk>e1 \<noteq> e2; e1 \<notin> A \<inter> B; set t1' \<subseteq> A; set (e2 # t2') \<subseteq> B; t1' \<upharpoonleft> B = (e2 # t2') \<upharpoonleft> A\<rbrakk> \<Longrightarrow> merge A B t1' (e2 # t2') \<upharpoonleft> A = t1' \<and> merge A B t1' (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B t1' (e2 # t2')) \<subseteq> set t1' \<union> set (e2 # t2')

goal (1 subgoal):
 1. merge A B t1' (e2 # t2') \<upharpoonleft> A = t1' &&& merge A B t1' (e2 # t2') \<upharpoonleft> B = e2 # t2' &&& set (merge A B t1' (e2 # t2')) \<subseteq> set t1' \<union> set (e2 # t2')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
merge A B t1' (e2 # t2') \<upharpoonleft> A = t1'
merge A B t1' (e2 # t2') \<upharpoonleft> B = e2 # t2'
set (merge A B t1' (e2 # t2')) \<subseteq> set t1' \<union> set (e2 # t2')

goal (1 subgoal):
 1. e1 \<notin> A \<inter> B \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
from e1_isnot_e2 e1_notin_A_inter_B
[PROOF STATE]
proof (chain)
picking this:
e1 \<noteq> e2
e1 \<notin> A \<inter> B
[PROOF STEP]
have merge_eq: "merge A B (e1 # t1') (e2 # t2') = e1 # (merge A B t1' (e2 # t2'))"
[PROOF STATE]
proof (prove)
using this:
e1 \<noteq> e2
e1 \<notin> A \<inter> B

goal (1 subgoal):
 1. merge A B (e1 # t1') (e2 # t2') = e1 # merge A B t1' (e2 # t2')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
merge A B (e1 # t1') (e2 # t2') = e1 # merge A B t1' (e2 # t2')

goal (1 subgoal):
 1. e1 \<notin> A \<inter> B \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
from 3(4) ind1
[PROOF STATE]
proof (chain)
picking this:
set (e1 # t1') \<subseteq> A
merge A B t1' (e2 # t2') \<upharpoonleft> A = t1'
[PROOF STEP]
have goal1: "merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1'"
[PROOF STATE]
proof (prove)
using this:
set (e1 # t1') \<subseteq> A
merge A B t1' (e2 # t2') \<upharpoonleft> A = t1'

goal (1 subgoal):
 1. merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1'
[PROOF STEP]
by (simp only: merge_eq projection_def, auto)
[PROOF STATE]
proof (state)
this:
merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1'

goal (1 subgoal):
 1. e1 \<notin> A \<inter> B \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1'

goal (1 subgoal):
 1. e1 \<notin> A \<inter> B \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
from ind2 e1_notin_B
[PROOF STATE]
proof (chain)
picking this:
merge A B t1' (e2 # t2') \<upharpoonleft> B = e2 # t2'
e1 \<notin> B
[PROOF STEP]
have goal2:
        "merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2'"
[PROOF STATE]
proof (prove)
using this:
merge A B t1' (e2 # t2') \<upharpoonleft> B = e2 # t2'
e1 \<notin> B

goal (1 subgoal):
 1. merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2'
[PROOF STEP]
by (simp only: merge_eq projection_def, auto)
[PROOF STATE]
proof (state)
this:
merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2'

goal (1 subgoal):
 1. e1 \<notin> A \<inter> B \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2'

goal (1 subgoal):
 1. e1 \<notin> A \<inter> B \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
from 3(4) ind3
[PROOF STATE]
proof (chain)
picking this:
set (e1 # t1') \<subseteq> A
set (merge A B t1' (e2 # t2')) \<subseteq> set t1' \<union> set (e2 # t2')
[PROOF STEP]
have goal3:
        "set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')"
[PROOF STATE]
proof (prove)
using this:
set (e1 # t1') \<subseteq> A
set (merge A B t1' (e2 # t2')) \<subseteq> set t1' \<union> set (e2 # t2')

goal (1 subgoal):
 1. set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
by (simp only: merge_eq, auto)
[PROOF STATE]
proof (state)
this:
set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')

goal (1 subgoal):
 1. e1 \<notin> A \<inter> B \<Longrightarrow> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1'
merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2'
set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1'
merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2'
set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')

goal (1 subgoal):
 1. merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')

goal:
No subgoals!
[PROOF STEP]
(* case (3 e1 t1' e2 t2') for e1 \<noteq> e2 e1 \<notin> A \<inter> B *)
[PROOF STATE]
proof (state)
this:
merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> A = e1 # t1' \<and> merge A B (e1 # t1') (e2 # t2') \<upharpoonleft> B = e2 # t2' \<and> set (merge A B (e1 # t1') (e2 # t2')) \<subseteq> set (e1 # t1') \<union> set (e2 # t2')

goal:
No subgoals!
[PROOF STEP]
qed