[STATEMENT]
lemma mmulti_join'_correct:
  assumes "A_pos \<noteq> []"
      and "list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) (A_pos @ A_neg) L"
  shows "z \<in> mmulti_join' A_pos A_neg L \<longleftrightarrow> wf_tuple n (\<Union>A\<in>set A_pos. A) z \<and>
    list_all2 (\<lambda>A X. restrict A z \<in> X) A_pos (take (length A_pos) L) \<and>
    list_all2 (\<lambda>A X. restrict A z \<notin> X) A_neg (drop (length A_pos) L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (z \<in> mmulti_join' A_pos A_neg L) = (wf_tuple n (\<Union>A\<in>set A_pos. A) z \<and> list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_pos (take (length A_pos) L) \<and> list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_neg (drop (length A_pos) L))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (z \<in> mmulti_join' A_pos A_neg L) = (wf_tuple n (\<Union>A\<in>set A_pos. A) z \<and> list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_pos (take (length A_pos) L) \<and> list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_neg (drop (length A_pos) L))
[PROOF STEP]
define Q where "Q = set (zip A_pos L)"
[PROOF STATE]
proof (state)
this:
Q = set (zip A_pos L)

goal (1 subgoal):
 1. (z \<in> mmulti_join' A_pos A_neg L) = (wf_tuple n (\<Union>A\<in>set A_pos. A) z \<and> list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_pos (take (length A_pos) L) \<and> list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_neg (drop (length A_pos) L))
[PROOF STEP]
have Q_alt: "Q = set (zip A_pos (take (length A_pos) L))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q = set (zip A_pos (take (length A_pos) L))
[PROOF STEP]
unfolding Q_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (zip A_pos L) = set (zip A_pos (take (length A_pos) L))
[PROOF STEP]
by (fastforce simp: in_set_zip)
[PROOF STATE]
proof (state)
this:
Q = set (zip A_pos (take (length A_pos) L))

goal (1 subgoal):
 1. (z \<in> mmulti_join' A_pos A_neg L) = (wf_tuple n (\<Union>A\<in>set A_pos. A) z \<and> list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_pos (take (length A_pos) L) \<and> list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_neg (drop (length A_pos) L))
[PROOF STEP]
define Q_neg where "Q_neg = set (zip A_neg (drop (length A_pos) L))"
[PROOF STATE]
proof (state)
this:
Q_neg = set (zip A_neg (drop (length A_pos) L))

goal (1 subgoal):
 1. (z \<in> mmulti_join' A_pos A_neg L) = (wf_tuple n (\<Union>A\<in>set A_pos. A) z \<and> list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_pos (take (length A_pos) L) \<and> list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_neg (drop (length A_pos) L))
[PROOF STEP]
let ?r = "mmulti_join' A_pos A_neg L"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (z \<in> mmulti_join' A_pos A_neg L) = (wf_tuple n (\<Union>A\<in>set A_pos. A) z \<and> list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_pos (take (length A_pos) L) \<and> list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_neg (drop (length A_pos) L))
[PROOF STEP]
have "?r = New_max_getIJ_wrapperGenericJoin Q Q_neg"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mmulti_join' A_pos A_neg L = New_max_getIJ_wrapperGenericJoin Q Q_neg
[PROOF STEP]
unfolding Q_def Q_neg_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mmulti_join' A_pos A_neg L = New_max_getIJ_wrapperGenericJoin (set (zip A_pos L)) (set (zip A_neg (drop (length A_pos) L)))
[PROOF STEP]
by (simp del: New_max.wrapperGenericJoin.simps)
[PROOF STATE]
proof (state)
this:
mmulti_join' A_pos A_neg L = New_max_getIJ_wrapperGenericJoin Q Q_neg

goal (1 subgoal):
 1. (z \<in> mmulti_join' A_pos A_neg L) = (wf_tuple n (\<Union>A\<in>set A_pos. A) z \<and> list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_pos (take (length A_pos) L) \<and> list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_neg (drop (length A_pos) L))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
mmulti_join' A_pos A_neg L = New_max_getIJ_wrapperGenericJoin Q Q_neg

goal (1 subgoal):
 1. (z \<in> mmulti_join' A_pos A_neg L) = (wf_tuple n (\<Union>A\<in>set A_pos. A) z \<and> list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_pos (take (length A_pos) L) \<and> list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_neg (drop (length A_pos) L))
[PROOF STEP]
have "card Q \<ge> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<le> card Q
[PROOF STEP]
unfolding Q_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<le> card (set (zip A_pos L))
[PROOF STEP]
using assms(1,2)
[PROOF STATE]
proof (prove)
using this:
A_pos \<noteq> []
list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) (A_pos @ A_neg) L

goal (1 subgoal):
 1. 1 \<le> card (set (zip A_pos L))
[PROOF STEP]
by (auto simp: Suc_le_eq card_gt_0_iff zip_eq_Nil_iff)
[PROOF STATE]
proof (state)
this:
1 \<le> card Q

goal (1 subgoal):
 1. (z \<in> mmulti_join' A_pos A_neg L) = (wf_tuple n (\<Union>A\<in>set A_pos. A) z \<and> list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_pos (take (length A_pos) L) \<and> list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_neg (drop (length A_pos) L))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
1 \<le> card Q

goal (1 subgoal):
 1. (z \<in> mmulti_join' A_pos A_neg L) = (wf_tuple n (\<Union>A\<in>set A_pos. A) z \<and> list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_pos (take (length A_pos) L) \<and> list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_neg (drop (length A_pos) L))
[PROOF STEP]
have "\<forall>(A, X)\<in>(Q \<union> Q_neg). table n A X \<and> wf_set n A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>(A, X)\<in>Q \<union> Q_neg. table n A X \<and> wf_set n A
[PROOF STEP]
unfolding Q_alt Q_neg_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>(A, X)\<in>set (zip A_pos (take (length A_pos) L)) \<union> set (zip A_neg (drop (length A_pos) L)). table n A X \<and> wf_set n A
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) (A_pos @ A_neg) L

goal (1 subgoal):
 1. \<forall>(A, X)\<in>set (zip A_pos (take (length A_pos) L)) \<union> set (zip A_neg (drop (length A_pos) L)). table n A X \<and> wf_set n A
[PROOF STEP]
by (simp add: zip_append1 list_all2_iff)
[PROOF STATE]
proof (state)
this:
\<forall>(A, X)\<in>Q \<union> Q_neg. table n A X \<and> wf_set n A

goal (1 subgoal):
 1. (z \<in> mmulti_join' A_pos A_neg L) = (wf_tuple n (\<Union>A\<in>set A_pos. A) z \<and> list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_pos (take (length A_pos) L) \<and> list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_neg (drop (length A_pos) L))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
mmulti_join' A_pos A_neg L = New_max_getIJ_wrapperGenericJoin Q Q_neg
1 \<le> card Q
\<forall>(A, X)\<in>Q \<union> Q_neg. table n A X \<and> wf_set n A
[PROOF STEP]
have "z \<in> ?r \<longleftrightarrow> wf_tuple n (\<Union>(A, X)\<in>Q. A) z \<and>
      (\<forall>(A, X)\<in>Q. restrict A z \<in> X) \<and> (\<forall>(A, X)\<in>Q_neg. restrict A z \<notin> X)"
[PROOF STATE]
proof (prove)
using this:
mmulti_join' A_pos A_neg L = New_max_getIJ_wrapperGenericJoin Q Q_neg
1 \<le> card Q
\<forall>(A, X)\<in>Q \<union> Q_neg. table n A X \<and> wf_set n A

goal (1 subgoal):
 1. (z \<in> mmulti_join' A_pos A_neg L) = (wf_tuple n (\<Union>(A, X)\<in>Q. A) z \<and> (\<forall>(A, X)\<in>Q. restrict A z \<in> X) \<and> (\<forall>(A, X)\<in>Q_neg. restrict A z \<notin> X))
[PROOF STEP]
using New_max.wrapper_correctness case_prod_beta'
[PROOF STATE]
proof (prove)
using this:
mmulti_join' A_pos A_neg L = New_max_getIJ_wrapperGenericJoin Q Q_neg
1 \<le> card Q
\<forall>(A, X)\<in>Q \<union> Q_neg. table n A X \<and> wf_set n A
\<lbrakk>1 \<le> card ?Q_pos; \<forall>(A, X)\<in>?Q_pos \<union> ?Q_neg. table ?n A X \<and> wf_set ?n A\<rbrakk> \<Longrightarrow> (?z \<in> New_max_getIJ_wrapperGenericJoin ?Q_pos ?Q_neg) = (wf_tuple ?n (\<Union>(A, X)\<in>?Q_pos. A) ?z \<and> (\<forall>(A, X)\<in>?Q_pos. restrict A ?z \<in> X) \<and> (\<forall>(A, X)\<in>?Q_neg. restrict A ?z \<notin> X))
(\<lambda>(x, y). ?f x y) = (\<lambda>x. ?f (fst x) (snd x))

goal (1 subgoal):
 1. (z \<in> mmulti_join' A_pos A_neg L) = (wf_tuple n (\<Union>(A, X)\<in>Q. A) z \<and> (\<forall>(A, X)\<in>Q. restrict A z \<in> X) \<and> (\<forall>(A, X)\<in>Q_neg. restrict A z \<notin> X))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(z \<in> mmulti_join' A_pos A_neg L) = (wf_tuple n (\<Union>(A, X)\<in>Q. A) z \<and> (\<forall>(A, X)\<in>Q. restrict A z \<in> X) \<and> (\<forall>(A, X)\<in>Q_neg. restrict A z \<notin> X))

goal (1 subgoal):
 1. (z \<in> mmulti_join' A_pos A_neg L) = (wf_tuple n (\<Union>A\<in>set A_pos. A) z \<and> list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_pos (take (length A_pos) L) \<and> list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_neg (drop (length A_pos) L))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(z \<in> mmulti_join' A_pos A_neg L) = (wf_tuple n (\<Union>(A, X)\<in>Q. A) z \<and> (\<forall>(A, X)\<in>Q. restrict A z \<in> X) \<and> (\<forall>(A, X)\<in>Q_neg. restrict A z \<notin> X))

goal (1 subgoal):
 1. (z \<in> mmulti_join' A_pos A_neg L) = (wf_tuple n (\<Union>A\<in>set A_pos. A) z \<and> list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_pos (take (length A_pos) L) \<and> list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_neg (drop (length A_pos) L))
[PROOF STEP]
have "(\<Union>A\<in>set A_pos. A) = (\<Union>(A, X)\<in>Q. A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>A\<in>set A_pos. A) = (\<Union>(A, X)\<in>Q. A)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Union>A\<in>set A_pos. A) = (\<Union>(A, X)\<in>Q. A)
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) (A_pos @ A_neg) L
[PROOF STEP]
have "length A_pos \<le> length L"
[PROOF STATE]
proof (prove)
using this:
list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) (A_pos @ A_neg) L

goal (1 subgoal):
 1. length A_pos \<le> length L
[PROOF STEP]
by (auto dest!: list_all2_lengthD)
[PROOF STATE]
proof (state)
this:
length A_pos \<le> length L

goal (1 subgoal):
 1. (\<Union>A\<in>set A_pos. A) = (\<Union>(A, X)\<in>Q. A)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length A_pos \<le> length L
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
length A_pos \<le> length L

goal (1 subgoal):
 1. (\<Union>A\<in>set A_pos. A) = (\<Union>(A, X)\<in>Q. A)
[PROOF STEP]
unfolding Q_alt
[PROOF STATE]
proof (prove)
using this:
length A_pos \<le> length L

goal (1 subgoal):
 1. (\<Union>A\<in>set A_pos. A) = (\<Union>(A, X)\<in>set (zip A_pos (take (length A_pos) L)). A)
[PROOF STEP]
by (auto elim: in_set_impl_in_set_zip1[rotated, where ys="take (length A_pos) L"]
          dest: set_zip_leftD)
[PROOF STATE]
proof (state)
this:
(\<Union>A\<in>set A_pos. A) = (\<Union>(A, X)\<in>Q. A)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Union>A\<in>set A_pos. A) = (\<Union>(A, X)\<in>Q. A)

goal (1 subgoal):
 1. (z \<in> mmulti_join' A_pos A_neg L) = (wf_tuple n (\<Union>A\<in>set A_pos. A) z \<and> list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_pos (take (length A_pos) L) \<and> list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_neg (drop (length A_pos) L))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<Union>A\<in>set A_pos. A) = (\<Union>(A, X)\<in>Q. A)

goal (1 subgoal):
 1. (z \<in> mmulti_join' A_pos A_neg L) = (wf_tuple n (\<Union>A\<in>set A_pos. A) z \<and> list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_pos (take (length A_pos) L) \<and> list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_neg (drop (length A_pos) L))
[PROOF STEP]
have "\<And>z. (\<forall>(A, X)\<in>Q. restrict A z \<in> X) \<longleftrightarrow>
    list_all2 (\<lambda>A X. restrict A z \<in> X) A_pos (take (length A_pos) L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>z. (\<forall>(A, X)\<in>Q. restrict A z \<in> X) = list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_pos (take (length A_pos) L)
[PROOF STEP]
unfolding Q_alt
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>z. (\<forall>(A, X)\<in>set (zip A_pos (take (length A_pos) L)). restrict A z \<in> X) = list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_pos (take (length A_pos) L)
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) (A_pos @ A_neg) L

goal (1 subgoal):
 1. \<And>z. (\<forall>(A, X)\<in>set (zip A_pos (take (length A_pos) L)). restrict A z \<in> X) = list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_pos (take (length A_pos) L)
[PROOF STEP]
by (auto simp add: list_all2_iff)
[PROOF STATE]
proof (state)
this:
(\<forall>(A, X)\<in>Q. restrict A ?z \<in> X) = list_all2 (\<lambda>A. (\<in>) (restrict A ?z)) A_pos (take (length A_pos) L)

goal (1 subgoal):
 1. (z \<in> mmulti_join' A_pos A_neg L) = (wf_tuple n (\<Union>A\<in>set A_pos. A) z \<and> list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_pos (take (length A_pos) L) \<and> list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_neg (drop (length A_pos) L))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<forall>(A, X)\<in>Q. restrict A ?z \<in> X) = list_all2 (\<lambda>A. (\<in>) (restrict A ?z)) A_pos (take (length A_pos) L)

goal (1 subgoal):
 1. (z \<in> mmulti_join' A_pos A_neg L) = (wf_tuple n (\<Union>A\<in>set A_pos. A) z \<and> list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_pos (take (length A_pos) L) \<and> list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_neg (drop (length A_pos) L))
[PROOF STEP]
have "\<And>z. (\<forall>(A, X)\<in>Q_neg. restrict A z \<notin> X) \<longleftrightarrow>
    list_all2 (\<lambda>A X. restrict A z \<notin> X) A_neg (drop (length A_pos) L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>z. (\<forall>(A, X)\<in>Q_neg. restrict A z \<notin> X) = list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_neg (drop (length A_pos) L)
[PROOF STEP]
unfolding Q_neg_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>z. (\<forall>(A, X)\<in>set (zip A_neg (drop (length A_pos) L)). restrict A z \<notin> X) = list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_neg (drop (length A_pos) L)
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) (A_pos @ A_neg) L

goal (1 subgoal):
 1. \<And>z. (\<forall>(A, X)\<in>set (zip A_neg (drop (length A_pos) L)). restrict A z \<notin> X) = list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_neg (drop (length A_pos) L)
[PROOF STEP]
by (auto simp add: list_all2_iff)
[PROOF STATE]
proof (state)
this:
(\<forall>(A, X)\<in>Q_neg. restrict A ?z \<notin> X) = list_all2 (\<lambda>A. (\<notin>) (restrict A ?z)) A_neg (drop (length A_pos) L)

goal (1 subgoal):
 1. (z \<in> mmulti_join' A_pos A_neg L) = (wf_tuple n (\<Union>A\<in>set A_pos. A) z \<and> list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_pos (take (length A_pos) L) \<and> list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_neg (drop (length A_pos) L))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(z \<in> mmulti_join' A_pos A_neg L) = (wf_tuple n (\<Union>(A, X)\<in>Q. A) z \<and> (\<forall>(A, X)\<in>Q. restrict A z \<in> X) \<and> (\<forall>(A, X)\<in>Q_neg. restrict A z \<notin> X))
(\<Union>A\<in>set A_pos. A) = (\<Union>(A, X)\<in>Q. A)
(\<forall>(A, X)\<in>Q. restrict A ?z \<in> X) = list_all2 (\<lambda>A. (\<in>) (restrict A ?z)) A_pos (take (length A_pos) L)
(\<forall>(A, X)\<in>Q_neg. restrict A ?z \<notin> X) = list_all2 (\<lambda>A. (\<notin>) (restrict A ?z)) A_neg (drop (length A_pos) L)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(z \<in> mmulti_join' A_pos A_neg L) = (wf_tuple n (\<Union>(A, X)\<in>Q. A) z \<and> (\<forall>(A, X)\<in>Q. restrict A z \<in> X) \<and> (\<forall>(A, X)\<in>Q_neg. restrict A z \<notin> X))
(\<Union>A\<in>set A_pos. A) = (\<Union>(A, X)\<in>Q. A)
(\<forall>(A, X)\<in>Q. restrict A ?z \<in> X) = list_all2 (\<lambda>A. (\<in>) (restrict A ?z)) A_pos (take (length A_pos) L)
(\<forall>(A, X)\<in>Q_neg. restrict A ?z \<notin> X) = list_all2 (\<lambda>A. (\<notin>) (restrict A ?z)) A_neg (drop (length A_pos) L)

goal (1 subgoal):
 1. (z \<in> mmulti_join' A_pos A_neg L) = (wf_tuple n (\<Union>A\<in>set A_pos. A) z \<and> list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_pos (take (length A_pos) L) \<and> list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_neg (drop (length A_pos) L))
[PROOF STEP]
unfolding Q_def Q_neg_def
[PROOF STATE]
proof (prove)
using this:
(z \<in> mmulti_join' A_pos A_neg L) = (wf_tuple n (\<Union>(A, X)\<in>set (zip A_pos L). A) z \<and> (\<forall>(A, X)\<in>set (zip A_pos L). restrict A z \<in> X) \<and> (\<forall>(A, X)\<in>set (zip A_neg (drop (length A_pos) L)). restrict A z \<notin> X))
(\<Union>A\<in>set A_pos. A) = (\<Union>(A, X)\<in>set (zip A_pos L). A)
(\<forall>(A, X)\<in>set (zip A_pos L). restrict A ?z \<in> X) = list_all2 (\<lambda>A. (\<in>) (restrict A ?z)) A_pos (take (length A_pos) L)
(\<forall>(A, X)\<in>set (zip A_neg (drop (length A_pos) L)). restrict A ?z \<notin> X) = list_all2 (\<lambda>A. (\<notin>) (restrict A ?z)) A_neg (drop (length A_pos) L)

goal (1 subgoal):
 1. (z \<in> mmulti_join' A_pos A_neg L) = (wf_tuple n (\<Union>A\<in>set A_pos. A) z \<and> list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_pos (take (length A_pos) L) \<and> list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_neg (drop (length A_pos) L))
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
(z \<in> mmulti_join' A_pos A_neg L) = (wf_tuple n (\<Union>(A, X)\<in>set (zip A_pos L). A) z \<and> (\<forall>(A, X)\<in>set (zip A_pos L). restrict A z \<in> X) \<and> (\<forall>(A, X)\<in>set (zip A_neg (drop (length A_pos) L)). restrict A z \<notin> X))
(\<Union>A\<in>set A_pos. A) = (\<Union>(A, X)\<in>set (zip A_pos L). A)
(\<forall>(A, X)\<in>set (zip A_pos L). restrict A ?z \<in> X) = list_all2 (\<lambda>A. (\<in>) (restrict A ?z)) A_pos (take (length A_pos) L)
(\<forall>(A, X)\<in>set (zip A_neg (drop (length A_pos) L)). restrict A ?z \<notin> X) = list_all2 (\<lambda>A. (\<notin>) (restrict A ?z)) A_neg (drop (length A_pos) L)
list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) (A_pos @ A_neg) L

goal (1 subgoal):
 1. (z \<in> mmulti_join' A_pos A_neg L) = (wf_tuple n (\<Union>A\<in>set A_pos. A) z \<and> list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_pos (take (length A_pos) L) \<and> list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_neg (drop (length A_pos) L))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(z \<in> mmulti_join' A_pos A_neg L) = (wf_tuple n (\<Union>A\<in>set A_pos. A) z \<and> list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_pos (take (length A_pos) L) \<and> list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_neg (drop (length A_pos) L))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma list_all2_opt_True:
  assumes "list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) ((A_zs @ A_x # A_xs @ A_y # A_ys) @ A_neg)
    ((zs @ x # xs @ y # ys) @ L_neg)"
    "length A_xs = length xs" "length A_ys = length ys" "length A_zs = length zs"
  shows "list_all2 (\<lambda>A X. table n A X \<and> wf_set n A)
    ((A_zs @ (A_x \<union> A_y) # A_xs @ A_ys) @ A_neg) ((zs @ join x True y # xs @ ys) @ L_neg)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) ((A_zs @ (A_x \<union> A_y) # A_xs @ A_ys) @ A_neg) ((zs @ join x True y # xs @ ys) @ L_neg)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) ((A_zs @ (A_x \<union> A_y) # A_xs @ A_ys) @ A_neg) ((zs @ join x True y # xs @ ys) @ L_neg)
[PROOF STEP]
have assms_dest: "table n A_x x" "table n A_y y" "wf_set n A_x" "wf_set n A_y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (table n A_x x &&& table n A_y y) &&& wf_set n A_x &&& wf_set n A_y
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) ((A_zs @ A_x # A_xs @ A_y # A_ys) @ A_neg) ((zs @ x # xs @ y # ys) @ L_neg)
length A_xs = length xs
length A_ys = length ys
length A_zs = length zs

goal (1 subgoal):
 1. (table n A_x x &&& table n A_y y) &&& wf_set n A_x &&& wf_set n A_y
[PROOF STEP]
by (auto simp del: mmulti_join'.simps simp add: list_all2_append1 dest: list_all2_lengthD)
[PROOF STATE]
proof (state)
this:
table n A_x x
table n A_y y
wf_set n A_x
wf_set n A_y

goal (1 subgoal):
 1. list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) ((A_zs @ (A_x \<union> A_y) # A_xs @ A_ys) @ A_neg) ((zs @ join x True y # xs @ ys) @ L_neg)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
table n A_x x
table n A_y y
wf_set n A_x
wf_set n A_y
[PROOF STEP]
have tabs: "table n (A_x \<union> A_y) (join x True y)" "wf_set n (A_x \<union> A_y)"
[PROOF STATE]
proof (prove)
using this:
table n A_x x
table n A_y y
wf_set n A_x
wf_set n A_y

goal (1 subgoal):
 1. table n (A_x \<union> A_y) (join x True y) &&& wf_set n (A_x \<union> A_y)
[PROOF STEP]
using join_table[of n A_x x A_y y True "A_x \<union> A_y", OF assms_dest(1,2)] assms_dest(3,4)
[PROOF STATE]
proof (prove)
using this:
table n A_x x
table n A_y y
wf_set n A_x
wf_set n A_y
\<lbrakk>\<not> True \<Longrightarrow> A_y \<subseteq> A_x; A_x \<union> A_y = A_x \<union> A_y\<rbrakk> \<Longrightarrow> table n (A_x \<union> A_y) (join x True y)
wf_set n A_x
wf_set n A_y

goal (1 subgoal):
 1. table n (A_x \<union> A_y) (join x True y) &&& wf_set n (A_x \<union> A_y)
[PROOF STEP]
by (auto simp add: wf_set_def)
[PROOF STATE]
proof (state)
this:
table n (A_x \<union> A_y) (join x True y)
wf_set n (A_x \<union> A_y)

goal (1 subgoal):
 1. list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) ((A_zs @ (A_x \<union> A_y) # A_xs @ A_ys) @ A_neg) ((zs @ join x True y # xs @ ys) @ L_neg)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
table n (A_x \<union> A_y) (join x True y)
wf_set n (A_x \<union> A_y)
[PROOF STEP]
show "list_all2 (\<lambda>A X. table n A X \<and> wf_set n A)
    ((A_zs @ (A_x \<union> A_y) # A_xs @ A_ys) @ A_neg) ((zs @ join x True y # xs @ ys) @ L_neg)"
[PROOF STATE]
proof (prove)
using this:
table n (A_x \<union> A_y) (join x True y)
wf_set n (A_x \<union> A_y)

goal (1 subgoal):
 1. list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) ((A_zs @ (A_x \<union> A_y) # A_xs @ A_ys) @ A_neg) ((zs @ join x True y # xs @ ys) @ L_neg)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
table n (A_x \<union> A_y) (join x True y)
wf_set n (A_x \<union> A_y)
list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) ((A_zs @ A_x # A_xs @ A_y # A_ys) @ A_neg) ((zs @ x # xs @ y # ys) @ L_neg)
length A_xs = length xs
length A_ys = length ys
length A_zs = length zs

goal (1 subgoal):
 1. list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) ((A_zs @ (A_x \<union> A_y) # A_xs @ A_ys) @ A_neg) ((zs @ join x True y # xs @ ys) @ L_neg)
[PROOF STEP]
by (auto simp del: mmulti_join'.simps simp add: list_all2_append1 list_all2_append2
        list_all2_Cons1 list_all2_Cons2 dest: list_all2_lengthD) fastforce
[PROOF STATE]
proof (state)
this:
list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) ((A_zs @ (A_x \<union> A_y) # A_xs @ A_ys) @ A_neg) ((zs @ join x True y # xs @ ys) @ L_neg)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mmulti_join'_opt_True:
  assumes "list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) ((A_zs @ A_x # A_xs @ A_y # A_ys) @ A_neg)
    ((zs @ x # xs @ y # ys) @ L_neg)"
    "length A_xs = length xs" "length A_ys = length ys" "length A_zs = length zs"
  shows "mmulti_join' (A_zs @ A_x # A_xs @ A_y # A_ys) A_neg ((zs @ x # xs @ y # ys) @ L_neg) =
    mmulti_join' (A_zs @ (A_x \<union> A_y) # A_xs @ A_ys) A_neg
    ((zs @ join x True y # xs @ ys) @ L_neg)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mmulti_join' (A_zs @ A_x # A_xs @ A_y # A_ys) A_neg ((zs @ x # xs @ y # ys) @ L_neg) = mmulti_join' (A_zs @ (A_x \<union> A_y) # A_xs @ A_ys) A_neg ((zs @ join x True y # xs @ ys) @ L_neg)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mmulti_join' (A_zs @ A_x # A_xs @ A_y # A_ys) A_neg ((zs @ x # xs @ y # ys) @ L_neg) = mmulti_join' (A_zs @ (A_x \<union> A_y) # A_xs @ A_ys) A_neg ((zs @ join x True y # xs @ ys) @ L_neg)
[PROOF STEP]
have assms_dest: "table n A_x x" "table n A_y y" "wf_set n A_x" "wf_set n A_y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (table n A_x x &&& table n A_y y) &&& wf_set n A_x &&& wf_set n A_y
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) ((A_zs @ A_x # A_xs @ A_y # A_ys) @ A_neg) ((zs @ x # xs @ y # ys) @ L_neg)
length A_xs = length xs
length A_ys = length ys
length A_zs = length zs

goal (1 subgoal):
 1. (table n A_x x &&& table n A_y y) &&& wf_set n A_x &&& wf_set n A_y
[PROOF STEP]
by (auto simp del: mmulti_join'.simps simp add: list_all2_append1 dest: list_all2_lengthD)
[PROOF STATE]
proof (state)
this:
table n A_x x
table n A_y y
wf_set n A_x
wf_set n A_y

goal (1 subgoal):
 1. mmulti_join' (A_zs @ A_x # A_xs @ A_y # A_ys) A_neg ((zs @ x # xs @ y # ys) @ L_neg) = mmulti_join' (A_zs @ (A_x \<union> A_y) # A_xs @ A_ys) A_neg ((zs @ join x True y # xs @ ys) @ L_neg)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
table n A_x x
table n A_y y
wf_set n A_x
wf_set n A_y
[PROOF STEP]
have tabs: "table n (A_x \<union> A_y) (join x True y)" "wf_set n (A_x \<union> A_y)"
[PROOF STATE]
proof (prove)
using this:
table n A_x x
table n A_y y
wf_set n A_x
wf_set n A_y

goal (1 subgoal):
 1. table n (A_x \<union> A_y) (join x True y) &&& wf_set n (A_x \<union> A_y)
[PROOF STEP]
using join_table[of n A_x x A_y y True "A_x \<union> A_y", OF assms_dest(1,2)] assms_dest(3,4)
[PROOF STATE]
proof (prove)
using this:
table n A_x x
table n A_y y
wf_set n A_x
wf_set n A_y
\<lbrakk>\<not> True \<Longrightarrow> A_y \<subseteq> A_x; A_x \<union> A_y = A_x \<union> A_y\<rbrakk> \<Longrightarrow> table n (A_x \<union> A_y) (join x True y)
wf_set n A_x
wf_set n A_y

goal (1 subgoal):
 1. table n (A_x \<union> A_y) (join x True y) &&& wf_set n (A_x \<union> A_y)
[PROOF STEP]
by (auto simp add: wf_set_def)
[PROOF STATE]
proof (state)
this:
table n (A_x \<union> A_y) (join x True y)
wf_set n (A_x \<union> A_y)

goal (1 subgoal):
 1. mmulti_join' (A_zs @ A_x # A_xs @ A_y # A_ys) A_neg ((zs @ x # xs @ y # ys) @ L_neg) = mmulti_join' (A_zs @ (A_x \<union> A_y) # A_xs @ A_ys) A_neg ((zs @ join x True y # xs @ ys) @ L_neg)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
table n (A_x \<union> A_y) (join x True y)
wf_set n (A_x \<union> A_y)
[PROOF STEP]
have list_all2': "list_all2 (\<lambda>A X. table n A X \<and> wf_set n A)
    ((A_zs @ (A_x \<union> A_y) # A_xs @ A_ys) @ A_neg) ((zs @ join x True y # xs @ ys) @ L_neg)"
[PROOF STATE]
proof (prove)
using this:
table n (A_x \<union> A_y) (join x True y)
wf_set n (A_x \<union> A_y)

goal (1 subgoal):
 1. list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) ((A_zs @ (A_x \<union> A_y) # A_xs @ A_ys) @ A_neg) ((zs @ join x True y # xs @ ys) @ L_neg)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
table n (A_x \<union> A_y) (join x True y)
wf_set n (A_x \<union> A_y)
list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) ((A_zs @ A_x # A_xs @ A_y # A_ys) @ A_neg) ((zs @ x # xs @ y # ys) @ L_neg)
length A_xs = length xs
length A_ys = length ys
length A_zs = length zs

goal (1 subgoal):
 1. list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) ((A_zs @ (A_x \<union> A_y) # A_xs @ A_ys) @ A_neg) ((zs @ join x True y # xs @ ys) @ L_neg)
[PROOF STEP]
by (auto simp del: mmulti_join'.simps simp add: list_all2_append1 list_all2_append2
        list_all2_Cons1 list_all2_Cons2 dest: list_all2_lengthD) fastforce
[PROOF STATE]
proof (state)
this:
list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) ((A_zs @ (A_x \<union> A_y) # A_xs @ A_ys) @ A_neg) ((zs @ join x True y # xs @ ys) @ L_neg)

goal (1 subgoal):
 1. mmulti_join' (A_zs @ A_x # A_xs @ A_y # A_ys) A_neg ((zs @ x # xs @ y # ys) @ L_neg) = mmulti_join' (A_zs @ (A_x \<union> A_y) # A_xs @ A_ys) A_neg ((zs @ join x True y # xs @ ys) @ L_neg)
[PROOF STEP]
have res: "\<And>z Z. wf_tuple n Z z \<Longrightarrow> A_x \<union> A_y \<subseteq> Z \<Longrightarrow>
    restrict (A_x \<union> A_y) z \<in> join x True y \<longleftrightarrow> restrict A_x z \<in> x \<and> restrict A_y z \<in> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>z Z. \<lbrakk>wf_tuple n Z z; A_x \<union> A_y \<subseteq> Z\<rbrakk> \<Longrightarrow> (restrict (A_x \<union> A_y) z \<in> join x True y) = (restrict A_x z \<in> x \<and> restrict A_y z \<in> y)
[PROOF STEP]
using join_restrict[of x n A_x y A_y True] wf_tuple_restrict_simple[of n _ _ "A_x \<union> A_y"]
      assms_dest(1,2)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>v. v \<in> x \<Longrightarrow> wf_tuple n A_x v; \<And>v. v \<in> y \<Longrightarrow> wf_tuple n A_y v; \<not> True \<Longrightarrow> A_y \<subseteq> A_x\<rbrakk> \<Longrightarrow> (?v \<in> join x True y) = (wf_tuple n (A_x \<union> A_y) ?v \<and> restrict A_x ?v \<in> x \<and> join_cond True y (restrict A_y ?v))
\<lbrakk>wf_tuple n ?B ?v; A_x \<union> A_y \<subseteq> ?B\<rbrakk> \<Longrightarrow> wf_tuple n (A_x \<union> A_y) (restrict (A_x \<union> A_y) ?v)
table n A_x x
table n A_y y

goal (1 subgoal):
 1. \<And>z Z. \<lbrakk>wf_tuple n Z z; A_x \<union> A_y \<subseteq> Z\<rbrakk> \<Longrightarrow> (restrict (A_x \<union> A_y) z \<in> join x True y) = (restrict A_x z \<in> x \<and> restrict A_y z \<in> y)
[PROOF STEP]
by (auto simp add: table_def restrict_nested Int_absorb2)
[PROOF STATE]
proof (state)
this:
\<lbrakk>wf_tuple n ?Z ?z; A_x \<union> A_y \<subseteq> ?Z\<rbrakk> \<Longrightarrow> (restrict (A_x \<union> A_y) ?z \<in> join x True y) = (restrict A_x ?z \<in> x \<and> restrict A_y ?z \<in> y)

goal (1 subgoal):
 1. mmulti_join' (A_zs @ A_x # A_xs @ A_y # A_ys) A_neg ((zs @ x # xs @ y # ys) @ L_neg) = mmulti_join' (A_zs @ (A_x \<union> A_y) # A_xs @ A_ys) A_neg ((zs @ join x True y # xs @ ys) @ L_neg)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mmulti_join' (A_zs @ A_x # A_xs @ A_y # A_ys) A_neg ((zs @ x # xs @ y # ys) @ L_neg) = mmulti_join' (A_zs @ (A_x \<union> A_y) # A_xs @ A_ys) A_neg ((zs @ join x True y # xs @ ys) @ L_neg)
[PROOF STEP]
proof (rule set_eqI, rule iffI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>xa. xa \<in> mmulti_join' (A_zs @ A_x # A_xs @ A_y # A_ys) A_neg ((zs @ x # xs @ y # ys) @ L_neg) \<Longrightarrow> xa \<in> mmulti_join' (A_zs @ (A_x \<union> A_y) # A_xs @ A_ys) A_neg ((zs @ join x True y # xs @ ys) @ L_neg)
 2. \<And>xa. xa \<in> mmulti_join' (A_zs @ (A_x \<union> A_y) # A_xs @ A_ys) A_neg ((zs @ join x True y # xs @ ys) @ L_neg) \<Longrightarrow> xa \<in> mmulti_join' (A_zs @ A_x # A_xs @ A_y # A_ys) A_neg ((zs @ x # xs @ y # ys) @ L_neg)
[PROOF STEP]
fix z
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>xa. xa \<in> mmulti_join' (A_zs @ A_x # A_xs @ A_y # A_ys) A_neg ((zs @ x # xs @ y # ys) @ L_neg) \<Longrightarrow> xa \<in> mmulti_join' (A_zs @ (A_x \<union> A_y) # A_xs @ A_ys) A_neg ((zs @ join x True y # xs @ ys) @ L_neg)
 2. \<And>xa. xa \<in> mmulti_join' (A_zs @ (A_x \<union> A_y) # A_xs @ A_ys) A_neg ((zs @ join x True y # xs @ ys) @ L_neg) \<Longrightarrow> xa \<in> mmulti_join' (A_zs @ A_x # A_xs @ A_y # A_ys) A_neg ((zs @ x # xs @ y # ys) @ L_neg)
[PROOF STEP]
assume "z \<in> mmulti_join' (A_zs @ A_x # A_xs @ A_y # A_ys) A_neg
      ((zs @ x # xs @ y # ys) @ L_neg)"
[PROOF STATE]
proof (state)
this:
z \<in> mmulti_join' (A_zs @ A_x # A_xs @ A_y # A_ys) A_neg ((zs @ x # xs @ y # ys) @ L_neg)

goal (2 subgoals):
 1. \<And>xa. xa \<in> mmulti_join' (A_zs @ A_x # A_xs @ A_y # A_ys) A_neg ((zs @ x # xs @ y # ys) @ L_neg) \<Longrightarrow> xa \<in> mmulti_join' (A_zs @ (A_x \<union> A_y) # A_xs @ A_ys) A_neg ((zs @ join x True y # xs @ ys) @ L_neg)
 2. \<And>xa. xa \<in> mmulti_join' (A_zs @ (A_x \<union> A_y) # A_xs @ A_ys) A_neg ((zs @ join x True y # xs @ ys) @ L_neg) \<Longrightarrow> xa \<in> mmulti_join' (A_zs @ A_x # A_xs @ A_y # A_ys) A_neg ((zs @ x # xs @ y # ys) @ L_neg)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
z \<in> mmulti_join' (A_zs @ A_x # A_xs @ A_y # A_ys) A_neg ((zs @ x # xs @ y # ys) @ L_neg)
[PROOF STEP]
have z_in_dest: "wf_tuple n (\<Union>(set (A_zs @ A_x # A_xs @ A_y # A_ys))) z"
      "list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_zs zs"
      "restrict A_x z \<in> x"
      "list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_ys ys"
      "restrict A_y z \<in> y"
      "list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_xs xs"
      "list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_neg L_neg"
[PROOF STATE]
proof (prove)
using this:
z \<in> mmulti_join' (A_zs @ A_x # A_xs @ A_y # A_ys) A_neg ((zs @ x # xs @ y # ys) @ L_neg)

goal (1 subgoal):
 1. (wf_tuple n (\<Union> (set (A_zs @ A_x # A_xs @ A_y # A_ys))) z &&& list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_zs zs &&& restrict A_x z \<in> x) &&& (list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_ys ys &&& restrict A_y z \<in> y) &&& list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_xs xs &&& list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_neg L_neg
[PROOF STEP]
using mmulti_join'_correct[OF _ assms(1), of z]
[PROOF STATE]
proof (prove)
using this:
z \<in> mmulti_join' (A_zs @ A_x # A_xs @ A_y # A_ys) A_neg ((zs @ x # xs @ y # ys) @ L_neg)
A_zs @ A_x # A_xs @ A_y # A_ys \<noteq> [] \<Longrightarrow> (z \<in> mmulti_join' (A_zs @ A_x # A_xs @ A_y # A_ys) A_neg ((zs @ x # xs @ y # ys) @ L_neg)) = (wf_tuple n (\<Union>A\<in>set (A_zs @ A_x # A_xs @ A_y # A_ys). A) z \<and> list_all2 (\<lambda>A. (\<in>) (restrict A z)) (A_zs @ A_x # A_xs @ A_y # A_ys) (take (length (A_zs @ A_x # A_xs @ A_y # A_ys)) ((zs @ x # xs @ y # ys) @ L_neg)) \<and> list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_neg (drop (length (A_zs @ A_x # A_xs @ A_y # A_ys)) ((zs @ x # xs @ y # ys) @ L_neg)))

goal (1 subgoal):
 1. (wf_tuple n (\<Union> (set (A_zs @ A_x # A_xs @ A_y # A_ys))) z &&& list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_zs zs &&& restrict A_x z \<in> x) &&& (list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_ys ys &&& restrict A_y z \<in> y) &&& list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_xs xs &&& list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_neg L_neg
[PROOF STEP]
by (auto simp del: mmulti_join'.simps simp add: assms list_all2_append1
          dest: list_all2_lengthD)
[PROOF STATE]
proof (state)
this:
wf_tuple n (\<Union> (set (A_zs @ A_x # A_xs @ A_y # A_ys))) z
list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_zs zs
restrict A_x z \<in> x
list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_ys ys
restrict A_y z \<in> y
list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_xs xs
list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_neg L_neg

goal (2 subgoals):
 1. \<And>xa. xa \<in> mmulti_join' (A_zs @ A_x # A_xs @ A_y # A_ys) A_neg ((zs @ x # xs @ y # ys) @ L_neg) \<Longrightarrow> xa \<in> mmulti_join' (A_zs @ (A_x \<union> A_y) # A_xs @ A_ys) A_neg ((zs @ join x True y # xs @ ys) @ L_neg)
 2. \<And>xa. xa \<in> mmulti_join' (A_zs @ (A_x \<union> A_y) # A_xs @ A_ys) A_neg ((zs @ join x True y # xs @ ys) @ L_neg) \<Longrightarrow> xa \<in> mmulti_join' (A_zs @ A_x # A_xs @ A_y # A_ys) A_neg ((zs @ x # xs @ y # ys) @ L_neg)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
wf_tuple n (\<Union> (set (A_zs @ A_x # A_xs @ A_y # A_ys))) z
list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_zs zs
restrict A_x z \<in> x
list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_ys ys
restrict A_y z \<in> y
list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_xs xs
list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_neg L_neg
[PROOF STEP]
show "z \<in> mmulti_join' (A_zs @ (A_x \<union> A_y) # A_xs @ A_ys) A_neg
      ((zs @ join x True y # xs @ ys) @ L_neg)"
[PROOF STATE]
proof (prove)
using this:
wf_tuple n (\<Union> (set (A_zs @ A_x # A_xs @ A_y # A_ys))) z
list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_zs zs
restrict A_x z \<in> x
list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_ys ys
restrict A_y z \<in> y
list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_xs xs
list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_neg L_neg

goal (1 subgoal):
 1. z \<in> mmulti_join' (A_zs @ (A_x \<union> A_y) # A_xs @ A_ys) A_neg ((zs @ join x True y # xs @ ys) @ L_neg)
[PROOF STEP]
using mmulti_join'_correct[OF _ list_all2', of z] res[OF z_in_dest(1)]
[PROOF STATE]
proof (prove)
using this:
wf_tuple n (\<Union> (set (A_zs @ A_x # A_xs @ A_y # A_ys))) z
list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_zs zs
restrict A_x z \<in> x
list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_ys ys
restrict A_y z \<in> y
list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_xs xs
list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_neg L_neg
A_zs @ (A_x \<union> A_y) # A_xs @ A_ys \<noteq> [] \<Longrightarrow> (z \<in> mmulti_join' (A_zs @ (A_x \<union> A_y) # A_xs @ A_ys) A_neg ((zs @ join x True y # xs @ ys) @ L_neg)) = (wf_tuple n (\<Union>A\<in>set (A_zs @ (A_x \<union> A_y) # A_xs @ A_ys). A) z \<and> list_all2 (\<lambda>A. (\<in>) (restrict A z)) (A_zs @ (A_x \<union> A_y) # A_xs @ A_ys) (take (length (A_zs @ (A_x \<union> A_y) # A_xs @ A_ys)) ((zs @ join x True y # xs @ ys) @ L_neg)) \<and> list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_neg (drop (length (A_zs @ (A_x \<union> A_y) # A_xs @ A_ys)) ((zs @ join x True y # xs @ ys) @ L_neg)))
A_x \<union> A_y \<subseteq> \<Union> (set (A_zs @ A_x # A_xs @ A_y # A_ys)) \<Longrightarrow> (restrict (A_x \<union> A_y) z \<in> join x True y) = (restrict A_x z \<in> x \<and> restrict A_y z \<in> y)

goal (1 subgoal):
 1. z \<in> mmulti_join' (A_zs @ (A_x \<union> A_y) # A_xs @ A_ys) A_neg ((zs @ join x True y # xs @ ys) @ L_neg)
[PROOF STEP]
by (auto simp add: assms list_all2_appendI le_supI2 Un_assoc simp del: mmulti_join'.simps
          dest: list_all2_lengthD)
[PROOF STATE]
proof (state)
this:
z \<in> mmulti_join' (A_zs @ (A_x \<union> A_y) # A_xs @ A_ys) A_neg ((zs @ join x True y # xs @ ys) @ L_neg)

goal (1 subgoal):
 1. \<And>xa. xa \<in> mmulti_join' (A_zs @ (A_x \<union> A_y) # A_xs @ A_ys) A_neg ((zs @ join x True y # xs @ ys) @ L_neg) \<Longrightarrow> xa \<in> mmulti_join' (A_zs @ A_x # A_xs @ A_y # A_ys) A_neg ((zs @ x # xs @ y # ys) @ L_neg)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> mmulti_join' (A_zs @ (A_x \<union> A_y) # A_xs @ A_ys) A_neg ((zs @ join x True y # xs @ ys) @ L_neg) \<Longrightarrow> xa \<in> mmulti_join' (A_zs @ A_x # A_xs @ A_y # A_ys) A_neg ((zs @ x # xs @ y # ys) @ L_neg)
[PROOF STEP]
fix z
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> mmulti_join' (A_zs @ (A_x \<union> A_y) # A_xs @ A_ys) A_neg ((zs @ join x True y # xs @ ys) @ L_neg) \<Longrightarrow> xa \<in> mmulti_join' (A_zs @ A_x # A_xs @ A_y # A_ys) A_neg ((zs @ x # xs @ y # ys) @ L_neg)
[PROOF STEP]
assume "z \<in> mmulti_join' (A_zs @ (A_x \<union> A_y) # A_xs @ A_ys) A_neg
      ((zs @ join x True y # xs @ ys) @ L_neg)"
[PROOF STATE]
proof (state)
this:
z \<in> mmulti_join' (A_zs @ (A_x \<union> A_y) # A_xs @ A_ys) A_neg ((zs @ join x True y # xs @ ys) @ L_neg)

goal (1 subgoal):
 1. \<And>xa. xa \<in> mmulti_join' (A_zs @ (A_x \<union> A_y) # A_xs @ A_ys) A_neg ((zs @ join x True y # xs @ ys) @ L_neg) \<Longrightarrow> xa \<in> mmulti_join' (A_zs @ A_x # A_xs @ A_y # A_ys) A_neg ((zs @ x # xs @ y # ys) @ L_neg)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
z \<in> mmulti_join' (A_zs @ (A_x \<union> A_y) # A_xs @ A_ys) A_neg ((zs @ join x True y # xs @ ys) @ L_neg)
[PROOF STEP]
have z_in_dest: "wf_tuple n (\<Union>(set (A_zs @ A_x # A_xs @ A_y # A_ys))) z"
      "list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_zs zs"
      "restrict (A_x \<union> A_y) z \<in> join x True y"
      "list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_ys ys"
      "list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_xs xs"
      "list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_neg L_neg"
[PROOF STATE]
proof (prove)
using this:
z \<in> mmulti_join' (A_zs @ (A_x \<union> A_y) # A_xs @ A_ys) A_neg ((zs @ join x True y # xs @ ys) @ L_neg)

goal (1 subgoal):
 1. (wf_tuple n (\<Union> (set (A_zs @ A_x # A_xs @ A_y # A_ys))) z &&& list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_zs zs &&& restrict (A_x \<union> A_y) z \<in> join x True y) &&& list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_ys ys &&& list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_xs xs &&& list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_neg L_neg
[PROOF STEP]
using mmulti_join'_correct[OF _ list_all2', of z]
[PROOF STATE]
proof (prove)
using this:
z \<in> mmulti_join' (A_zs @ (A_x \<union> A_y) # A_xs @ A_ys) A_neg ((zs @ join x True y # xs @ ys) @ L_neg)
A_zs @ (A_x \<union> A_y) # A_xs @ A_ys \<noteq> [] \<Longrightarrow> (z \<in> mmulti_join' (A_zs @ (A_x \<union> A_y) # A_xs @ A_ys) A_neg ((zs @ join x True y # xs @ ys) @ L_neg)) = (wf_tuple n (\<Union>A\<in>set (A_zs @ (A_x \<union> A_y) # A_xs @ A_ys). A) z \<and> list_all2 (\<lambda>A. (\<in>) (restrict A z)) (A_zs @ (A_x \<union> A_y) # A_xs @ A_ys) (take (length (A_zs @ (A_x \<union> A_y) # A_xs @ A_ys)) ((zs @ join x True y # xs @ ys) @ L_neg)) \<and> list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_neg (drop (length (A_zs @ (A_x \<union> A_y) # A_xs @ A_ys)) ((zs @ join x True y # xs @ ys) @ L_neg)))

goal (1 subgoal):
 1. (wf_tuple n (\<Union> (set (A_zs @ A_x # A_xs @ A_y # A_ys))) z &&& list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_zs zs &&& restrict (A_x \<union> A_y) z \<in> join x True y) &&& list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_ys ys &&& list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_xs xs &&& list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_neg L_neg
[PROOF STEP]
by (auto simp del: mmulti_join'.simps simp add: assms list_all2_append Un_assoc
          dest: list_all2_lengthD)
[PROOF STATE]
proof (state)
this:
wf_tuple n (\<Union> (set (A_zs @ A_x # A_xs @ A_y # A_ys))) z
list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_zs zs
restrict (A_x \<union> A_y) z \<in> join x True y
list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_ys ys
list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_xs xs
list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_neg L_neg

goal (1 subgoal):
 1. \<And>xa. xa \<in> mmulti_join' (A_zs @ (A_x \<union> A_y) # A_xs @ A_ys) A_neg ((zs @ join x True y # xs @ ys) @ L_neg) \<Longrightarrow> xa \<in> mmulti_join' (A_zs @ A_x # A_xs @ A_y # A_ys) A_neg ((zs @ x # xs @ y # ys) @ L_neg)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
wf_tuple n (\<Union> (set (A_zs @ A_x # A_xs @ A_y # A_ys))) z
list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_zs zs
restrict (A_x \<union> A_y) z \<in> join x True y
list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_ys ys
list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_xs xs
list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_neg L_neg
[PROOF STEP]
show "z \<in> mmulti_join' (A_zs @ A_x # A_xs @ A_y # A_ys) A_neg
      ((zs @ x # xs @ y # ys) @ L_neg)"
[PROOF STATE]
proof (prove)
using this:
wf_tuple n (\<Union> (set (A_zs @ A_x # A_xs @ A_y # A_ys))) z
list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_zs zs
restrict (A_x \<union> A_y) z \<in> join x True y
list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_ys ys
list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_xs xs
list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_neg L_neg

goal (1 subgoal):
 1. z \<in> mmulti_join' (A_zs @ A_x # A_xs @ A_y # A_ys) A_neg ((zs @ x # xs @ y # ys) @ L_neg)
[PROOF STEP]
using mmulti_join'_correct[OF _ assms(1), of z] res[OF z_in_dest(1)]
[PROOF STATE]
proof (prove)
using this:
wf_tuple n (\<Union> (set (A_zs @ A_x # A_xs @ A_y # A_ys))) z
list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_zs zs
restrict (A_x \<union> A_y) z \<in> join x True y
list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_ys ys
list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_xs xs
list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_neg L_neg
A_zs @ A_x # A_xs @ A_y # A_ys \<noteq> [] \<Longrightarrow> (z \<in> mmulti_join' (A_zs @ A_x # A_xs @ A_y # A_ys) A_neg ((zs @ x # xs @ y # ys) @ L_neg)) = (wf_tuple n (\<Union>A\<in>set (A_zs @ A_x # A_xs @ A_y # A_ys). A) z \<and> list_all2 (\<lambda>A. (\<in>) (restrict A z)) (A_zs @ A_x # A_xs @ A_y # A_ys) (take (length (A_zs @ A_x # A_xs @ A_y # A_ys)) ((zs @ x # xs @ y # ys) @ L_neg)) \<and> list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_neg (drop (length (A_zs @ A_x # A_xs @ A_y # A_ys)) ((zs @ x # xs @ y # ys) @ L_neg)))
A_x \<union> A_y \<subseteq> \<Union> (set (A_zs @ A_x # A_xs @ A_y # A_ys)) \<Longrightarrow> (restrict (A_x \<union> A_y) z \<in> join x True y) = (restrict A_x z \<in> x \<and> restrict A_y z \<in> y)

goal (1 subgoal):
 1. z \<in> mmulti_join' (A_zs @ A_x # A_xs @ A_y # A_ys) A_neg ((zs @ x # xs @ y # ys) @ L_neg)
[PROOF STEP]
by (auto simp add: assms list_all2_appendI le_supI2 Un_assoc simp del: mmulti_join'.simps
          dest: list_all2_lengthD)
[PROOF STATE]
proof (state)
this:
z \<in> mmulti_join' (A_zs @ A_x # A_xs @ A_y # A_ys) A_neg ((zs @ x # xs @ y # ys) @ L_neg)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
mmulti_join' (A_zs @ A_x # A_xs @ A_y # A_ys) A_neg ((zs @ x # xs @ y # ys) @ L_neg) = mmulti_join' (A_zs @ (A_x \<union> A_y) # A_xs @ A_ys) A_neg ((zs @ join x True y # xs @ ys) @ L_neg)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma list_all2_opt_False:
  assumes "list_all2 (\<lambda>A X. table n A X \<and> wf_set n A)
    ((A_zs @ A_x # A_xs) @ (A_ws @ A_y # A_ys)) ((zs @ x # xs) @ (ws @ y # ys))"
    "length A_ws = length ws" "length A_xs = length xs"
    "length A_ys = length ys" "length A_zs = length zs"
    "A_y \<subseteq> A_x"
  shows "list_all2 (\<lambda>A X. table n A X \<and> wf_set n A)
    ((A_zs @ A_x # A_xs) @ (A_ws @ A_ys)) ((zs @ join x False y # xs) @ (ws @ ys))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) ((A_zs @ A_x # A_xs) @ A_ws @ A_ys) ((zs @ join x False y # xs) @ ws @ ys)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) ((A_zs @ A_x # A_xs) @ A_ws @ A_ys) ((zs @ join x False y # xs) @ ws @ ys)
[PROOF STEP]
have assms_dest: "table n A_x x" "table n A_y y" "wf_set n A_x" "wf_set n A_y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (table n A_x x &&& table n A_y y) &&& wf_set n A_x &&& wf_set n A_y
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) ((A_zs @ A_x # A_xs) @ A_ws @ A_y # A_ys) ((zs @ x # xs) @ ws @ y # ys)
length A_ws = length ws
length A_xs = length xs
length A_ys = length ys
length A_zs = length zs
A_y \<subseteq> A_x

goal (1 subgoal):
 1. (table n A_x x &&& table n A_y y) &&& wf_set n A_x &&& wf_set n A_y
[PROOF STEP]
by (auto simp del: mmulti_join'.simps simp add: list_all2_append dest: list_all2_lengthD)
[PROOF STATE]
proof (state)
this:
table n A_x x
table n A_y y
wf_set n A_x
wf_set n A_y

goal (1 subgoal):
 1. list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) ((A_zs @ A_x # A_xs) @ A_ws @ A_ys) ((zs @ join x False y # xs) @ ws @ ys)
[PROOF STEP]
have tabs: "table n A_x (join x False y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. table n A_x (join x False y)
[PROOF STEP]
using join_table[of n A_x x A_y y False A_x, OF assms_dest(1,2) assms(6)] assms(6)
[PROOF STATE]
proof (prove)
using this:
A_x \<union> A_y = A_x \<Longrightarrow> table n A_x (join x False y)
A_y \<subseteq> A_x

goal (1 subgoal):
 1. table n A_x (join x False y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
table n A_x (join x False y)

goal (1 subgoal):
 1. list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) ((A_zs @ A_x # A_xs) @ A_ws @ A_ys) ((zs @ join x False y # xs) @ ws @ ys)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
table n A_x (join x False y)
[PROOF STEP]
show "list_all2 (\<lambda>A X. table n A X \<and> wf_set n A)
    ((A_zs @ A_x # A_xs) @ (A_ws @ A_ys)) ((zs @ join x False y # xs) @ (ws @ ys))"
[PROOF STATE]
proof (prove)
using this:
table n A_x (join x False y)

goal (1 subgoal):
 1. list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) ((A_zs @ A_x # A_xs) @ A_ws @ A_ys) ((zs @ join x False y # xs) @ ws @ ys)
[PROOF STEP]
using assms assms_dest(3)
[PROOF STATE]
proof (prove)
using this:
table n A_x (join x False y)
list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) ((A_zs @ A_x # A_xs) @ A_ws @ A_y # A_ys) ((zs @ x # xs) @ ws @ y # ys)
length A_ws = length ws
length A_xs = length xs
length A_ys = length ys
length A_zs = length zs
A_y \<subseteq> A_x
wf_set n A_x

goal (1 subgoal):
 1. list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) ((A_zs @ A_x # A_xs) @ A_ws @ A_ys) ((zs @ join x False y # xs) @ ws @ ys)
[PROOF STEP]
by (auto simp del: mmulti_join'.simps simp add: list_all2_append1 list_all2_append2
        list_all2_Cons1 list_all2_Cons2 dest: list_all2_lengthD) fastforce
[PROOF STATE]
proof (state)
this:
list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) ((A_zs @ A_x # A_xs) @ A_ws @ A_ys) ((zs @ join x False y # xs) @ ws @ ys)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mmulti_join'_opt_False:
  assumes "list_all2 (\<lambda>A X. table n A X \<and> wf_set n A)
    ((A_zs @ A_x # A_xs) @ (A_ws @ A_y # A_ys)) ((zs @ x # xs) @ (ws @ y # ys))"
    "length A_ws = length ws" "length A_xs = length xs"
    "length A_ys = length ys" "length A_zs = length zs"
    "A_y \<subseteq> A_x"
  shows "mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_y # A_ys) ((zs @ x # xs) @ (ws @ y # ys)) =
    mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_ys) ((zs @ join x False y # xs) @ (ws @ ys))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_y # A_ys) ((zs @ x # xs) @ ws @ y # ys) = mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_ys) ((zs @ join x False y # xs) @ ws @ ys)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_y # A_ys) ((zs @ x # xs) @ ws @ y # ys) = mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_ys) ((zs @ join x False y # xs) @ ws @ ys)
[PROOF STEP]
have assms_dest: "table n A_x x" "table n A_y y" "wf_set n A_x" "wf_set n A_y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (table n A_x x &&& table n A_y y) &&& wf_set n A_x &&& wf_set n A_y
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) ((A_zs @ A_x # A_xs) @ A_ws @ A_y # A_ys) ((zs @ x # xs) @ ws @ y # ys)
length A_ws = length ws
length A_xs = length xs
length A_ys = length ys
length A_zs = length zs
A_y \<subseteq> A_x

goal (1 subgoal):
 1. (table n A_x x &&& table n A_y y) &&& wf_set n A_x &&& wf_set n A_y
[PROOF STEP]
by (auto simp del: mmulti_join'.simps simp add: list_all2_append dest: list_all2_lengthD)
[PROOF STATE]
proof (state)
this:
table n A_x x
table n A_y y
wf_set n A_x
wf_set n A_y

goal (1 subgoal):
 1. mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_y # A_ys) ((zs @ x # xs) @ ws @ y # ys) = mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_ys) ((zs @ join x False y # xs) @ ws @ ys)
[PROOF STEP]
have tabs: "table n A_x (join x False y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. table n A_x (join x False y)
[PROOF STEP]
using join_table[of n A_x x A_y y False A_x, OF assms_dest(1,2) assms(6)] assms(6)
[PROOF STATE]
proof (prove)
using this:
A_x \<union> A_y = A_x \<Longrightarrow> table n A_x (join x False y)
A_y \<subseteq> A_x

goal (1 subgoal):
 1. table n A_x (join x False y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
table n A_x (join x False y)

goal (1 subgoal):
 1. mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_y # A_ys) ((zs @ x # xs) @ ws @ y # ys) = mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_ys) ((zs @ join x False y # xs) @ ws @ ys)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
table n A_x (join x False y)
[PROOF STEP]
have list_all2': "list_all2 (\<lambda>A X. table n A X \<and> wf_set n A)
    ((A_zs @ A_x # A_xs) @ (A_ws @ A_ys)) ((zs @ join x False y # xs) @ (ws @ ys))"
[PROOF STATE]
proof (prove)
using this:
table n A_x (join x False y)

goal (1 subgoal):
 1. list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) ((A_zs @ A_x # A_xs) @ A_ws @ A_ys) ((zs @ join x False y # xs) @ ws @ ys)
[PROOF STEP]
using assms assms_dest(3)
[PROOF STATE]
proof (prove)
using this:
table n A_x (join x False y)
list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) ((A_zs @ A_x # A_xs) @ A_ws @ A_y # A_ys) ((zs @ x # xs) @ ws @ y # ys)
length A_ws = length ws
length A_xs = length xs
length A_ys = length ys
length A_zs = length zs
A_y \<subseteq> A_x
wf_set n A_x

goal (1 subgoal):
 1. list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) ((A_zs @ A_x # A_xs) @ A_ws @ A_ys) ((zs @ join x False y # xs) @ ws @ ys)
[PROOF STEP]
by (auto simp del: mmulti_join'.simps simp add: list_all2_append1 list_all2_append2
        list_all2_Cons1 list_all2_Cons2 dest: list_all2_lengthD) fastforce
[PROOF STATE]
proof (state)
this:
list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) ((A_zs @ A_x # A_xs) @ A_ws @ A_ys) ((zs @ join x False y # xs) @ ws @ ys)

goal (1 subgoal):
 1. mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_y # A_ys) ((zs @ x # xs) @ ws @ y # ys) = mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_ys) ((zs @ join x False y # xs) @ ws @ ys)
[PROOF STEP]
have res: "\<And>z. restrict A_x z \<in> join x False y \<longleftrightarrow> restrict A_x z \<in> x \<and> restrict A_y z \<notin> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>z. (restrict A_x z \<in> join x False y) = (restrict A_x z \<in> x \<and> restrict A_y z \<notin> y)
[PROOF STEP]
using join_restrict[of x n A_x y A_y False, OF _ _ assms(6)] assms_dest(1,2) assms(6)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>v. v \<in> x \<Longrightarrow> wf_tuple n A_x v; \<And>v. v \<in> y \<Longrightarrow> wf_tuple n A_y v\<rbrakk> \<Longrightarrow> (?v \<in> join x False y) = (wf_tuple n (A_x \<union> A_y) ?v \<and> restrict A_x ?v \<in> x \<and> join_cond False y (restrict A_y ?v))
table n A_x x
table n A_y y
A_y \<subseteq> A_x

goal (1 subgoal):
 1. \<And>z. (restrict A_x z \<in> join x False y) = (restrict A_x z \<in> x \<and> restrict A_y z \<notin> y)
[PROOF STEP]
by (auto simp add: table_def restrict_nested Int_absorb2 Un_absorb2)
[PROOF STATE]
proof (state)
this:
(restrict A_x ?z \<in> join x False y) = (restrict A_x ?z \<in> x \<and> restrict A_y ?z \<notin> y)

goal (1 subgoal):
 1. mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_y # A_ys) ((zs @ x # xs) @ ws @ y # ys) = mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_ys) ((zs @ join x False y # xs) @ ws @ ys)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_y # A_ys) ((zs @ x # xs) @ ws @ y # ys) = mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_ys) ((zs @ join x False y # xs) @ ws @ ys)
[PROOF STEP]
proof (rule set_eqI, rule iffI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>xa. xa \<in> mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_y # A_ys) ((zs @ x # xs) @ ws @ y # ys) \<Longrightarrow> xa \<in> mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_ys) ((zs @ join x False y # xs) @ ws @ ys)
 2. \<And>xa. xa \<in> mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_ys) ((zs @ join x False y # xs) @ ws @ ys) \<Longrightarrow> xa \<in> mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_y # A_ys) ((zs @ x # xs) @ ws @ y # ys)
[PROOF STEP]
fix z
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>xa. xa \<in> mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_y # A_ys) ((zs @ x # xs) @ ws @ y # ys) \<Longrightarrow> xa \<in> mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_ys) ((zs @ join x False y # xs) @ ws @ ys)
 2. \<And>xa. xa \<in> mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_ys) ((zs @ join x False y # xs) @ ws @ ys) \<Longrightarrow> xa \<in> mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_y # A_ys) ((zs @ x # xs) @ ws @ y # ys)
[PROOF STEP]
assume "z \<in> mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_y # A_ys)
      ((zs @ x # xs) @ ws @ y # ys)"
[PROOF STATE]
proof (state)
this:
z \<in> mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_y # A_ys) ((zs @ x # xs) @ ws @ y # ys)

goal (2 subgoals):
 1. \<And>xa. xa \<in> mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_y # A_ys) ((zs @ x # xs) @ ws @ y # ys) \<Longrightarrow> xa \<in> mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_ys) ((zs @ join x False y # xs) @ ws @ ys)
 2. \<And>xa. xa \<in> mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_ys) ((zs @ join x False y # xs) @ ws @ ys) \<Longrightarrow> xa \<in> mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_y # A_ys) ((zs @ x # xs) @ ws @ y # ys)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
z \<in> mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_y # A_ys) ((zs @ x # xs) @ ws @ y # ys)
[PROOF STEP]
have z_in_dest: "wf_tuple n (\<Union>(set (A_zs @ A_x # A_xs))) z"
      "list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_zs zs"
      "restrict A_x z \<in> x"
      "list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_xs xs"
      "list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_ws ws"
      "restrict A_y z \<notin> y"
      "list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_ys ys"
[PROOF STATE]
proof (prove)
using this:
z \<in> mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_y # A_ys) ((zs @ x # xs) @ ws @ y # ys)

goal (1 subgoal):
 1. (wf_tuple n (\<Union> (set (A_zs @ A_x # A_xs))) z &&& list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_zs zs &&& restrict A_x z \<in> x) &&& (list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_xs xs &&& list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_ws ws) &&& restrict A_y z \<notin> y &&& list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_ys ys
[PROOF STEP]
using mmulti_join'_correct[OF _ assms(1), of z]
[PROOF STATE]
proof (prove)
using this:
z \<in> mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_y # A_ys) ((zs @ x # xs) @ ws @ y # ys)
A_zs @ A_x # A_xs \<noteq> [] \<Longrightarrow> (z \<in> mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_y # A_ys) ((zs @ x # xs) @ ws @ y # ys)) = (wf_tuple n (\<Union>A\<in>set (A_zs @ A_x # A_xs). A) z \<and> list_all2 (\<lambda>A. (\<in>) (restrict A z)) (A_zs @ A_x # A_xs) (take (length (A_zs @ A_x # A_xs)) ((zs @ x # xs) @ ws @ y # ys)) \<and> list_all2 (\<lambda>A. (\<notin>) (restrict A z)) (A_ws @ A_y # A_ys) (drop (length (A_zs @ A_x # A_xs)) ((zs @ x # xs) @ ws @ y # ys)))

goal (1 subgoal):
 1. (wf_tuple n (\<Union> (set (A_zs @ A_x # A_xs))) z &&& list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_zs zs &&& restrict A_x z \<in> x) &&& (list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_xs xs &&& list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_ws ws) &&& restrict A_y z \<notin> y &&& list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_ys ys
[PROOF STEP]
by (auto simp del: mmulti_join'.simps simp add: assms list_all2_append1
          dest: list_all2_lengthD)
[PROOF STATE]
proof (state)
this:
wf_tuple n (\<Union> (set (A_zs @ A_x # A_xs))) z
list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_zs zs
restrict A_x z \<in> x
list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_xs xs
list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_ws ws
restrict A_y z \<notin> y
list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_ys ys

goal (2 subgoals):
 1. \<And>xa. xa \<in> mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_y # A_ys) ((zs @ x # xs) @ ws @ y # ys) \<Longrightarrow> xa \<in> mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_ys) ((zs @ join x False y # xs) @ ws @ ys)
 2. \<And>xa. xa \<in> mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_ys) ((zs @ join x False y # xs) @ ws @ ys) \<Longrightarrow> xa \<in> mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_y # A_ys) ((zs @ x # xs) @ ws @ y # ys)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
wf_tuple n (\<Union> (set (A_zs @ A_x # A_xs))) z
list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_zs zs
restrict A_x z \<in> x
list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_xs xs
list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_ws ws
restrict A_y z \<notin> y
list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_ys ys
[PROOF STEP]
show "z \<in> mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_ys)
      ((zs @ join x False y # xs) @ ws @ ys)"
[PROOF STATE]
proof (prove)
using this:
wf_tuple n (\<Union> (set (A_zs @ A_x # A_xs))) z
list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_zs zs
restrict A_x z \<in> x
list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_xs xs
list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_ws ws
restrict A_y z \<notin> y
list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_ys ys

goal (1 subgoal):
 1. z \<in> mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_ys) ((zs @ join x False y # xs) @ ws @ ys)
[PROOF STEP]
using mmulti_join'_correct[OF _ list_all2', of z] res
[PROOF STATE]
proof (prove)
using this:
wf_tuple n (\<Union> (set (A_zs @ A_x # A_xs))) z
list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_zs zs
restrict A_x z \<in> x
list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_xs xs
list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_ws ws
restrict A_y z \<notin> y
list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_ys ys
A_zs @ A_x # A_xs \<noteq> [] \<Longrightarrow> (z \<in> mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_ys) ((zs @ join x False y # xs) @ ws @ ys)) = (wf_tuple n (\<Union>A\<in>set (A_zs @ A_x # A_xs). A) z \<and> list_all2 (\<lambda>A. (\<in>) (restrict A z)) (A_zs @ A_x # A_xs) (take (length (A_zs @ A_x # A_xs)) ((zs @ join x False y # xs) @ ws @ ys)) \<and> list_all2 (\<lambda>A. (\<notin>) (restrict A z)) (A_ws @ A_ys) (drop (length (A_zs @ A_x # A_xs)) ((zs @ join x False y # xs) @ ws @ ys)))
(restrict A_x ?z \<in> join x False y) = (restrict A_x ?z \<in> x \<and> restrict A_y ?z \<notin> y)

goal (1 subgoal):
 1. z \<in> mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_ys) ((zs @ join x False y # xs) @ ws @ ys)
[PROOF STEP]
by (auto simp add: assms list_all2_appendI Un_assoc simp del: mmulti_join'.simps
          dest: list_all2_lengthD)
[PROOF STATE]
proof (state)
this:
z \<in> mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_ys) ((zs @ join x False y # xs) @ ws @ ys)

goal (1 subgoal):
 1. \<And>xa. xa \<in> mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_ys) ((zs @ join x False y # xs) @ ws @ ys) \<Longrightarrow> xa \<in> mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_y # A_ys) ((zs @ x # xs) @ ws @ y # ys)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_ys) ((zs @ join x False y # xs) @ ws @ ys) \<Longrightarrow> xa \<in> mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_y # A_ys) ((zs @ x # xs) @ ws @ y # ys)
[PROOF STEP]
fix z
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_ys) ((zs @ join x False y # xs) @ ws @ ys) \<Longrightarrow> xa \<in> mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_y # A_ys) ((zs @ x # xs) @ ws @ y # ys)
[PROOF STEP]
assume "z \<in> mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_ys)
      ((zs @ join x False y # xs) @ ws @ ys)"
[PROOF STATE]
proof (state)
this:
z \<in> mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_ys) ((zs @ join x False y # xs) @ ws @ ys)

goal (1 subgoal):
 1. \<And>xa. xa \<in> mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_ys) ((zs @ join x False y # xs) @ ws @ ys) \<Longrightarrow> xa \<in> mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_y # A_ys) ((zs @ x # xs) @ ws @ y # ys)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
z \<in> mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_ys) ((zs @ join x False y # xs) @ ws @ ys)
[PROOF STEP]
have z_in_dest: "wf_tuple n (\<Union>(set (A_zs @ A_x # A_xs))) z"
      "list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_zs zs"
      "restrict A_x z \<in> join x False y"
      "list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_xs xs"
      "list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_ws ws"
      "list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_ys ys"
[PROOF STATE]
proof (prove)
using this:
z \<in> mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_ys) ((zs @ join x False y # xs) @ ws @ ys)

goal (1 subgoal):
 1. (wf_tuple n (\<Union> (set (A_zs @ A_x # A_xs))) z &&& list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_zs zs &&& restrict A_x z \<in> join x False y) &&& list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_xs xs &&& list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_ws ws &&& list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_ys ys
[PROOF STEP]
using mmulti_join'_correct[OF _ list_all2', of z]
[PROOF STATE]
proof (prove)
using this:
z \<in> mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_ys) ((zs @ join x False y # xs) @ ws @ ys)
A_zs @ A_x # A_xs \<noteq> [] \<Longrightarrow> (z \<in> mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_ys) ((zs @ join x False y # xs) @ ws @ ys)) = (wf_tuple n (\<Union>A\<in>set (A_zs @ A_x # A_xs). A) z \<and> list_all2 (\<lambda>A. (\<in>) (restrict A z)) (A_zs @ A_x # A_xs) (take (length (A_zs @ A_x # A_xs)) ((zs @ join x False y # xs) @ ws @ ys)) \<and> list_all2 (\<lambda>A. (\<notin>) (restrict A z)) (A_ws @ A_ys) (drop (length (A_zs @ A_x # A_xs)) ((zs @ join x False y # xs) @ ws @ ys)))

goal (1 subgoal):
 1. (wf_tuple n (\<Union> (set (A_zs @ A_x # A_xs))) z &&& list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_zs zs &&& restrict A_x z \<in> join x False y) &&& list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_xs xs &&& list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_ws ws &&& list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_ys ys
[PROOF STEP]
by (auto simp del: mmulti_join'.simps simp add: assms list_all2_append1
          dest: list_all2_lengthD)
[PROOF STATE]
proof (state)
this:
wf_tuple n (\<Union> (set (A_zs @ A_x # A_xs))) z
list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_zs zs
restrict A_x z \<in> join x False y
list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_xs xs
list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_ws ws
list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_ys ys

goal (1 subgoal):
 1. \<And>xa. xa \<in> mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_ys) ((zs @ join x False y # xs) @ ws @ ys) \<Longrightarrow> xa \<in> mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_y # A_ys) ((zs @ x # xs) @ ws @ y # ys)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
wf_tuple n (\<Union> (set (A_zs @ A_x # A_xs))) z
list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_zs zs
restrict A_x z \<in> join x False y
list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_xs xs
list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_ws ws
list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_ys ys
[PROOF STEP]
show "z \<in> mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_y # A_ys)
      ((zs @ x # xs) @ ws @ y # ys)"
[PROOF STATE]
proof (prove)
using this:
wf_tuple n (\<Union> (set (A_zs @ A_x # A_xs))) z
list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_zs zs
restrict A_x z \<in> join x False y
list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_xs xs
list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_ws ws
list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_ys ys

goal (1 subgoal):
 1. z \<in> mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_y # A_ys) ((zs @ x # xs) @ ws @ y # ys)
[PROOF STEP]
using mmulti_join'_correct[OF _ assms(1), of z] res
[PROOF STATE]
proof (prove)
using this:
wf_tuple n (\<Union> (set (A_zs @ A_x # A_xs))) z
list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_zs zs
restrict A_x z \<in> join x False y
list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_xs xs
list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_ws ws
list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_ys ys
A_zs @ A_x # A_xs \<noteq> [] \<Longrightarrow> (z \<in> mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_y # A_ys) ((zs @ x # xs) @ ws @ y # ys)) = (wf_tuple n (\<Union>A\<in>set (A_zs @ A_x # A_xs). A) z \<and> list_all2 (\<lambda>A. (\<in>) (restrict A z)) (A_zs @ A_x # A_xs) (take (length (A_zs @ A_x # A_xs)) ((zs @ x # xs) @ ws @ y # ys)) \<and> list_all2 (\<lambda>A. (\<notin>) (restrict A z)) (A_ws @ A_y # A_ys) (drop (length (A_zs @ A_x # A_xs)) ((zs @ x # xs) @ ws @ y # ys)))
(restrict A_x ?z \<in> join x False y) = (restrict A_x ?z \<in> x \<and> restrict A_y ?z \<notin> y)

goal (1 subgoal):
 1. z \<in> mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_y # A_ys) ((zs @ x # xs) @ ws @ y # ys)
[PROOF STEP]
by (auto simp add: assms list_all2_appendI Un_assoc simp del: mmulti_join'.simps
          dest: list_all2_lengthD)
[PROOF STATE]
proof (state)
this:
z \<in> mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_y # A_ys) ((zs @ x # xs) @ ws @ y # ys)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_y # A_ys) ((zs @ x # xs) @ ws @ y # ys) = mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_ys) ((zs @ join x False y # xs) @ ws @ ys)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma find_sub_in_sound: "find_sub_in X xs b = Some (ys, z, zs) \<Longrightarrow>
  xs = ys @ z # zs \<and> (z \<subseteq> X \<or> (b \<and> X \<subseteq> z))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. find_sub_in X xs b = Some (ys, z, zs) \<Longrightarrow> xs = ys @ z # zs \<and> (z \<subseteq> X \<or> b \<and> X \<subseteq> z)
[PROOF STEP]
by (induction X xs b arbitrary: ys z zs rule: find_sub_in.induct)
     (fastforce split: if_splits option.splits)+


[STATEMENT]
lemma find_sub_True_sound: "find_sub_True xs = Some (ys, w, ws, z, zs) \<Longrightarrow>
  xs = ys @ w # ws @ z # zs \<and> (z \<subseteq> w \<or> w \<subseteq> z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. find_sub_True xs = Some (ys, w, ws, z, zs) \<Longrightarrow> xs = ys @ w # ws @ z # zs \<and> (z \<subseteq> w \<or> w \<subseteq> z)
[PROOF STEP]
using find_sub_in_sound
[PROOF STATE]
proof (prove)
using this:
find_sub_in ?X ?xs ?b = Some (?ys, ?z, ?zs) \<Longrightarrow> ?xs = ?ys @ ?z # ?zs \<and> (?z \<subseteq> ?X \<or> ?b \<and> ?X \<subseteq> ?z)

goal (1 subgoal):
 1. find_sub_True xs = Some (ys, w, ws, z, zs) \<Longrightarrow> xs = ys @ w # ws @ z # zs \<and> (z \<subseteq> w \<or> w \<subseteq> z)
[PROOF STEP]
by (induction xs arbitrary: ys w ws z zs rule: find_sub_True.induct)
     (fastforce split: option.splits)+


[STATEMENT]
lemma find_sub_False_sound: "find_sub_False xs ns = Some ((rs, w, ws), (ys, z, zs)) \<Longrightarrow>
  xs = rs @ w # ws \<and> ns = ys @ z # zs \<and> (z \<subseteq> w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. find_sub_False xs ns = Some ((rs, w, ws), ys, z, zs) \<Longrightarrow> xs = rs @ w # ws \<and> ns = ys @ z # zs \<and> z \<subseteq> w
[PROOF STEP]
using find_sub_in_sound
[PROOF STATE]
proof (prove)
using this:
find_sub_in ?X ?xs ?b = Some (?ys, ?z, ?zs) \<Longrightarrow> ?xs = ?ys @ ?z # ?zs \<and> (?z \<subseteq> ?X \<or> ?b \<and> ?X \<subseteq> ?z)

goal (1 subgoal):
 1. find_sub_False xs ns = Some ((rs, w, ws), ys, z, zs) \<Longrightarrow> xs = rs @ w # ws \<and> ns = ys @ z # zs \<and> z \<subseteq> w
[PROOF STEP]
by (induction xs ns arbitrary: rs w ws ys z zs rule: find_sub_False.induct)
     (fastforce split: option.splits)+


[STATEMENT]
lemma proj_list_3_same:
  assumes "proj_list_3 xs (ys, z, zs) = (ys', z', zs')"
    "length xs = length ys + 1 + length zs"
  shows "xs = ys' @ z' # zs'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs = ys' @ z' # zs'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
proj_list_3 xs (ys, z, zs) = (ys', z', zs')
length xs = length ys + 1 + length zs

goal (1 subgoal):
 1. xs = ys' @ z' # zs'
[PROOF STEP]
by (auto simp add: id_take_nth_drop)


[STATEMENT]
lemma proj_list_3_length:
  assumes "proj_list_3 xs (ys, z, zs) = (ys', z', zs')"
    "length xs = length ys + 1 + length zs"
  shows "length ys = length ys'" "length zs = length zs'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length ys = length ys' &&& length zs = length zs'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
proj_list_3 xs (ys, z, zs) = (ys', z', zs')
length xs = length ys + 1 + length zs

goal (1 subgoal):
 1. length ys = length ys' &&& length zs = length zs'
[PROOF STEP]
by auto


[STATEMENT]
lemma proj_list_5_same:
  assumes "proj_list_5 xs (ys, w, ws, z, zs) = (ys', w', ws', z', zs')"
    "length xs = length ys + 1 + length ws + 1 + length zs"
  shows "xs = ys' @ w' # ws' @ z' # zs'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs = ys' @ w' # ws' @ z' # zs'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. xs = ys' @ w' # ws' @ z' # zs'
[PROOF STEP]
have "xs ! length ys # take (length ws) (drop (Suc (length ys)) xs) = take (Suc (length ws)) (drop (length ys) xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs ! length ys # take (length ws) (drop (Suc (length ys)) xs) = take (Suc (length ws)) (drop (length ys) xs)
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
length xs = length ys + 1 + length ws + 1 + length zs

goal (1 subgoal):
 1. xs ! length ys # take (length ws) (drop (Suc (length ys)) xs) = take (Suc (length ws)) (drop (length ys) xs)
[PROOF STEP]
by (simp add: list_eq_iff_nth_eq nth_Cons split: nat.split)
[PROOF STATE]
proof (state)
this:
xs ! length ys # take (length ws) (drop (Suc (length ys)) xs) = take (Suc (length ws)) (drop (length ys) xs)

goal (1 subgoal):
 1. xs = ys' @ w' # ws' @ z' # zs'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
xs ! length ys # take (length ws) (drop (Suc (length ys)) xs) = take (Suc (length ws)) (drop (length ys) xs)

goal (1 subgoal):
 1. xs = ys' @ w' # ws' @ z' # zs'
[PROOF STEP]
have "take (Suc (length ws)) (drop (length ys) xs) @ drop (Suc (length ys + length ws)) xs =
      drop (length ys) xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. take (Suc (length ws)) (drop (length ys) xs) @ drop (Suc (length ys + length ws)) xs = drop (length ys) xs
[PROOF STEP]
unfolding Suc_eq_plus1 add.assoc[of _ _ 1] add.commute[of _ "length ws + 1"]
      drop_drop[symmetric, of "length ws + 1"] append_take_drop_id
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. drop (length ys) xs = drop (length ys) xs
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
take (Suc (length ws)) (drop (length ys) xs) @ drop (Suc (length ys + length ws)) xs = drop (length ys) xs

goal (1 subgoal):
 1. xs = ys' @ w' # ws' @ z' # zs'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
xs ! length ys # take (length ws) (drop (Suc (length ys)) xs) = take (Suc (length ws)) (drop (length ys) xs)
take (Suc (length ws)) (drop (length ys) xs) @ drop (Suc (length ys + length ws)) xs = drop (length ys) xs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
xs ! length ys # take (length ws) (drop (Suc (length ys)) xs) = take (Suc (length ws)) (drop (length ys) xs)
take (Suc (length ws)) (drop (length ys) xs) @ drop (Suc (length ys + length ws)) xs = drop (length ys) xs

goal (1 subgoal):
 1. xs = ys' @ w' # ws' @ z' # zs'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
xs ! length ys # take (length ws) (drop (Suc (length ys)) xs) = take (Suc (length ws)) (drop (length ys) xs)
take (Suc (length ws)) (drop (length ys) xs) @ drop (Suc (length ys + length ws)) xs = drop (length ys) xs
proj_list_5 xs (ys, w, ws, z, zs) = (ys', w', ws', z', zs')
length xs = length ys + 1 + length ws + 1 + length zs

goal (1 subgoal):
 1. xs = ys' @ w' # ws' @ z' # zs'
[PROOF STEP]
by (auto simp: Cons_nth_drop_Suc append_Cons[symmetric])
[PROOF STATE]
proof (state)
this:
xs = ys' @ w' # ws' @ z' # zs'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma proj_list_5_length:
  assumes "proj_list_5 xs (ys, w, ws, z, zs) = (ys', w', ws', z', zs')"
    "length xs = length ys + 1 + length ws + 1 + length zs"
  shows "length ys = length ys'" "length ws = length ws'"
    "length zs = length zs'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length ys = length ys' &&& length ws = length ws' &&& length zs = length zs'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
proj_list_5 xs (ys, w, ws, z, zs) = (ys', w', ws', z', zs')
length xs = length ys + 1 + length ws + 1 + length zs

goal (1 subgoal):
 1. length ys = length ys' &&& length ws = length ws' &&& length zs = length zs'
[PROOF STEP]
by auto


[STATEMENT]
lemma find_sub_True_proj_list_5_same:
  assumes "find_sub_True xs = Some (ys, w, ws, z, zs)" "length xs = length xs'"
    "proj_list_5 xs' (ys, w, ws, z, zs) = (ys', w', ws', z', zs')"
  shows "xs' = ys' @ w' # ws' @ z' # zs'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs' = ys' @ w' # ws' @ z' # zs'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. xs' = ys' @ w' # ws' @ z' # zs'
[PROOF STEP]
have len: "length xs' = length ys + 1 + length ws + 1 + length zs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length xs' = length ys + 1 + length ws + 1 + length zs
[PROOF STEP]
using find_sub_True_sound[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
xs = ys @ w # ws @ z # zs \<and> (z \<subseteq> w \<or> w \<subseteq> z)

goal (1 subgoal):
 1. length xs' = length ys + 1 + length ws + 1 + length zs
[PROOF STEP]
by (auto simp add: assms(2)[symmetric])
[PROOF STATE]
proof (state)
this:
length xs' = length ys + 1 + length ws + 1 + length zs

goal (1 subgoal):
 1. xs' = ys' @ w' # ws' @ z' # zs'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs' = ys' @ w' # ws' @ z' # zs'
[PROOF STEP]
using proj_list_5_same[OF assms(3) len]
[PROOF STATE]
proof (prove)
using this:
xs' = ys' @ w' # ws' @ z' # zs'

goal (1 subgoal):
 1. xs' = ys' @ w' # ws' @ z' # zs'
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
xs' = ys' @ w' # ws' @ z' # zs'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma find_sub_True_proj_list_5_length:
  assumes "find_sub_True xs = Some (ys, w, ws, z, zs)" "length xs = length xs'"
    "proj_list_5 xs' (ys, w, ws, z, zs) = (ys', w', ws', z', zs')"
  shows "length ys = length ys'" "length ws = length ws'"
    "length zs = length zs'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length ys = length ys' &&& length ws = length ws' &&& length zs = length zs'
[PROOF STEP]
using find_sub_True_sound[OF assms(1)] proj_list_5_length[OF assms(3)] assms(2)
[PROOF STATE]
proof (prove)
using this:
xs = ys @ w # ws @ z # zs \<and> (z \<subseteq> w \<or> w \<subseteq> z)
length xs' = length ys + 1 + length ws + 1 + length zs \<Longrightarrow> length ys = length ys'
length xs' = length ys + 1 + length ws + 1 + length zs \<Longrightarrow> length ws = length ws'
length xs' = length ys + 1 + length ws + 1 + length zs \<Longrightarrow> length zs = length zs'
length xs = length xs'

goal (1 subgoal):
 1. length ys = length ys' &&& length ws = length ws' &&& length zs = length zs'
[PROOF STEP]
by auto


[STATEMENT]
lemma dominate_True_sound:
  assumes "dominate_True A_pos L_pos = Some ((A_zs, A_x, A_xs, A_y, A_ys), (zs, x, xs, y, ys))"
    "length A_pos = length L_pos"
  shows "A_pos = A_zs @ A_x # A_xs @ A_y # A_ys" "L_pos = zs @ x # xs @ y # ys"
    "length A_xs = length xs" "length A_ys = length ys" "length A_zs = length zs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A_pos = A_zs @ A_x # A_xs @ A_y # A_ys &&& L_pos = zs @ x # xs @ y # ys) &&& length A_xs = length xs &&& length A_ys = length ys &&& length A_zs = length zs
[PROOF STEP]
using assms find_sub_True_sound find_sub_True_proj_list_5_same find_sub_True_proj_list_5_length
[PROOF STATE]
proof (prove)
using this:
dominate_True A_pos L_pos = Some ((A_zs, A_x, A_xs, A_y, A_ys), zs, x, xs, y, ys)
length A_pos = length L_pos
find_sub_True ?xs = Some (?ys, ?w, ?ws, ?z, ?zs) \<Longrightarrow> ?xs = ?ys @ ?w # ?ws @ ?z # ?zs \<and> (?z \<subseteq> ?w \<or> ?w \<subseteq> ?z)
\<lbrakk>find_sub_True ?xs = Some (?ys, ?w, ?ws, ?z, ?zs); length ?xs = length ?xs'; proj_list_5 ?xs' (?ys, ?w, ?ws, ?z, ?zs) = (?ys', ?w', ?ws', ?z', ?zs')\<rbrakk> \<Longrightarrow> ?xs' = ?ys' @ ?w' # ?ws' @ ?z' # ?zs'
\<lbrakk>find_sub_True ?xs = Some (?ys, ?w, ?ws, ?z, ?zs); length ?xs = length ?xs'; proj_list_5 ?xs' (?ys, ?w, ?ws, ?z, ?zs) = (?ys', ?w', ?ws', ?z', ?zs')\<rbrakk> \<Longrightarrow> length ?ys = length ?ys'
\<lbrakk>find_sub_True ?xs = Some (?ys, ?w, ?ws, ?z, ?zs); length ?xs = length ?xs'; proj_list_5 ?xs' (?ys, ?w, ?ws, ?z, ?zs) = (?ys', ?w', ?ws', ?z', ?zs')\<rbrakk> \<Longrightarrow> length ?ws = length ?ws'
\<lbrakk>find_sub_True ?xs = Some (?ys, ?w, ?ws, ?z, ?zs); length ?xs = length ?xs'; proj_list_5 ?xs' (?ys, ?w, ?ws, ?z, ?zs) = (?ys', ?w', ?ws', ?z', ?zs')\<rbrakk> \<Longrightarrow> length ?zs = length ?zs'

goal (1 subgoal):
 1. (A_pos = A_zs @ A_x # A_xs @ A_y # A_ys &&& L_pos = zs @ x # xs @ y # ys) &&& length A_xs = length xs &&& length A_ys = length ys &&& length A_zs = length zs
[PROOF STEP]
by (auto simp del: proj_list_5.simps split: option.splits) fast+


[STATEMENT]
lemma find_sub_False_proj_list_3_same_left:
  assumes "find_sub_False xs ns = Some ((rs, w, ws), (ys, z, zs))"
    "length xs = length xs'" "proj_list_3 xs' (rs, w, ws) = (rs', w', ws')"
  shows "xs' = rs' @ w' # ws'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs' = rs' @ w' # ws'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. xs' = rs' @ w' # ws'
[PROOF STEP]
have len: "length xs' = length rs + 1 + length ws"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length xs' = length rs + 1 + length ws
[PROOF STEP]
using find_sub_False_sound[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
xs = rs @ w # ws \<and> ns = ys @ z # zs \<and> z \<subseteq> w

goal (1 subgoal):
 1. length xs' = length rs + 1 + length ws
[PROOF STEP]
by (auto simp add: assms(2)[symmetric])
[PROOF STATE]
proof (state)
this:
length xs' = length rs + 1 + length ws

goal (1 subgoal):
 1. xs' = rs' @ w' # ws'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs' = rs' @ w' # ws'
[PROOF STEP]
using proj_list_3_same[OF assms(3) len]
[PROOF STATE]
proof (prove)
using this:
xs' = rs' @ w' # ws'

goal (1 subgoal):
 1. xs' = rs' @ w' # ws'
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
xs' = rs' @ w' # ws'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma find_sub_False_proj_list_3_length_left:
  assumes "find_sub_False xs ns = Some ((rs, w, ws), (ys, z, zs))"
    "length xs = length xs'" "proj_list_3 xs' (rs, w, ws) = (rs', w', ws')"
  shows "length rs = length rs'" "length ws = length ws'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length rs = length rs' &&& length ws = length ws'
[PROOF STEP]
using find_sub_False_sound[OF assms(1)] proj_list_3_length[OF assms(3)] assms(2)
[PROOF STATE]
proof (prove)
using this:
xs = rs @ w # ws \<and> ns = ys @ z # zs \<and> z \<subseteq> w
length xs' = length rs + 1 + length ws \<Longrightarrow> length rs = length rs'
length xs' = length rs + 1 + length ws \<Longrightarrow> length ws = length ws'
length xs = length xs'

goal (1 subgoal):
 1. length rs = length rs' &&& length ws = length ws'
[PROOF STEP]
by auto


[STATEMENT]
lemma find_sub_False_proj_list_3_same_right:
  assumes "find_sub_False xs ns = Some ((rs, w, ws), (ys, z, zs))"
    "length ns = length ns'" "proj_list_3 ns' (ys, z, zs) = (ys', z', zs')"
  shows "ns' = ys' @ z' # zs'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ns' = ys' @ z' # zs'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ns' = ys' @ z' # zs'
[PROOF STEP]
have len: "length ns' = length ys + 1 + length zs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length ns' = length ys + 1 + length zs
[PROOF STEP]
using find_sub_False_sound[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
xs = rs @ w # ws \<and> ns = ys @ z # zs \<and> z \<subseteq> w

goal (1 subgoal):
 1. length ns' = length ys + 1 + length zs
[PROOF STEP]
by (auto simp add: assms(2)[symmetric])
[PROOF STATE]
proof (state)
this:
length ns' = length ys + 1 + length zs

goal (1 subgoal):
 1. ns' = ys' @ z' # zs'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ns' = ys' @ z' # zs'
[PROOF STEP]
using proj_list_3_same[OF assms(3) len]
[PROOF STATE]
proof (prove)
using this:
ns' = ys' @ z' # zs'

goal (1 subgoal):
 1. ns' = ys' @ z' # zs'
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
ns' = ys' @ z' # zs'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma find_sub_False_proj_list_3_length_right:
  assumes "find_sub_False xs ns = Some ((rs, w, ws), (ys, z, zs))"
    "length ns = length ns'" "proj_list_3 ns' (ys, z, zs) = (ys', z', zs')"
  shows "length ys = length ys'" "length zs = length zs'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length ys = length ys' &&& length zs = length zs'
[PROOF STEP]
using find_sub_False_sound[OF assms(1)] proj_list_3_length[OF assms(3)] assms(2)
[PROOF STATE]
proof (prove)
using this:
xs = rs @ w # ws \<and> ns = ys @ z # zs \<and> z \<subseteq> w
length ns' = length ys + 1 + length zs \<Longrightarrow> length ys = length ys'
length ns' = length ys + 1 + length zs \<Longrightarrow> length zs = length zs'
length ns = length ns'

goal (1 subgoal):
 1. length ys = length ys' &&& length zs = length zs'
[PROOF STEP]
by auto


[STATEMENT]
lemma dominate_False_sound:
  assumes "dominate_False A_pos L_pos A_neg L_neg =
    Some (((A_zs, A_x, A_xs), A_ws, A_y, A_ys), ((zs, x, xs), ws, y, ys))"
    "length A_pos = length L_pos" "length A_neg = length L_neg"
  shows "A_pos = (A_zs @ A_x # A_xs)" "A_neg = A_ws @ A_y # A_ys"
    "L_pos = (zs @ x # xs)" "L_neg = ws @ y # ys"
    "length A_ws = length ws" "length A_xs = length xs"
    "length A_ys = length ys" "length A_zs = length zs"
    "A_y \<subseteq> A_x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((A_pos = A_zs @ A_x # A_xs &&& A_neg = A_ws @ A_y # A_ys) &&& L_pos = zs @ x # xs &&& L_neg = ws @ y # ys) &&& (length A_ws = length ws &&& length A_xs = length xs) &&& length A_ys = length ys &&& length A_zs = length zs &&& A_y \<subseteq> A_x
[PROOF STEP]
using assms find_sub_False_proj_list_3_same_left find_sub_False_proj_list_3_same_right
    find_sub_False_proj_list_3_length_left find_sub_False_proj_list_3_length_right
    find_sub_False_sound
[PROOF STATE]
proof (prove)
using this:
dominate_False A_pos L_pos A_neg L_neg = Some (((A_zs, A_x, A_xs), A_ws, A_y, A_ys), (zs, x, xs), ws, y, ys)
length A_pos = length L_pos
length A_neg = length L_neg
\<lbrakk>find_sub_False ?xs ?ns = Some ((?rs, ?w, ?ws), ?ys, ?z, ?zs); length ?xs = length ?xs'; proj_list_3 ?xs' (?rs, ?w, ?ws) = (?rs', ?w', ?ws')\<rbrakk> \<Longrightarrow> ?xs' = ?rs' @ ?w' # ?ws'
\<lbrakk>find_sub_False ?xs ?ns = Some ((?rs, ?w, ?ws), ?ys, ?z, ?zs); length ?ns = length ?ns'; proj_list_3 ?ns' (?ys, ?z, ?zs) = (?ys', ?z', ?zs')\<rbrakk> \<Longrightarrow> ?ns' = ?ys' @ ?z' # ?zs'
\<lbrakk>find_sub_False ?xs ?ns = Some ((?rs, ?w, ?ws), ?ys, ?z, ?zs); length ?xs = length ?xs'; proj_list_3 ?xs' (?rs, ?w, ?ws) = (?rs', ?w', ?ws')\<rbrakk> \<Longrightarrow> length ?rs = length ?rs'
\<lbrakk>find_sub_False ?xs ?ns = Some ((?rs, ?w, ?ws), ?ys, ?z, ?zs); length ?xs = length ?xs'; proj_list_3 ?xs' (?rs, ?w, ?ws) = (?rs', ?w', ?ws')\<rbrakk> \<Longrightarrow> length ?ws = length ?ws'
\<lbrakk>find_sub_False ?xs ?ns = Some ((?rs, ?w, ?ws), ?ys, ?z, ?zs); length ?ns = length ?ns'; proj_list_3 ?ns' (?ys, ?z, ?zs) = (?ys', ?z', ?zs')\<rbrakk> \<Longrightarrow> length ?ys = length ?ys'
\<lbrakk>find_sub_False ?xs ?ns = Some ((?rs, ?w, ?ws), ?ys, ?z, ?zs); length ?ns = length ?ns'; proj_list_3 ?ns' (?ys, ?z, ?zs) = (?ys', ?z', ?zs')\<rbrakk> \<Longrightarrow> length ?zs = length ?zs'
find_sub_False ?xs ?ns = Some ((?rs, ?w, ?ws), ?ys, ?z, ?zs) \<Longrightarrow> ?xs = ?rs @ ?w # ?ws \<and> ?ns = ?ys @ ?z # ?zs \<and> ?z \<subseteq> ?w

goal (1 subgoal):
 1. ((A_pos = A_zs @ A_x # A_xs &&& A_neg = A_ws @ A_y # A_ys) &&& L_pos = zs @ x # xs &&& L_neg = ws @ y # ys) &&& (length A_ws = length ws &&& length A_xs = length xs) &&& length A_ys = length ys &&& length A_zs = length zs &&& A_y \<subseteq> A_x
[PROOF STEP]
by (auto simp del: proj_list_3.simps split: option.splits) fast+