Theory Generic_Join.Generic_Join_Correctness

section ‹Correctness›

subsection ‹Well-formed queries›

theory Generic_Join_Correctness
  imports Generic_Join
begin

definition wf_set :: "nat ⇒ vertices ⇒ bool" where
  "wf_set n V ⟷ (∀x∈V. x < n)"

definition wf_atable :: "nat ⇒ 'a atable ⇒ bool" where
  "wf_atable n X ⟷ table n (fst X) (snd X) ∧ finite (fst X)"

definition wf_query :: "nat ⇒ vertices ⇒ 'a query ⇒ 'a query ⇒ bool" where
  "wf_query n V Q_pos Q_neg ⟷ (∀X∈(Q_pos ∪ Q_neg). wf_atable n X) ∧ (wf_set n V) ∧ (card Q_pos ≥ 1)"

definition included :: "vertices ⇒ 'a query ⇒ bool" where
  "included V Q ⟷ (∀(S, X)∈Q. S ⊆ V)"

definition covering :: "vertices ⇒ 'a query ⇒ bool" where
  "covering V Q ⟷ V ⊆ (⋃(S, X)∈Q. S)"

definition non_empty_query :: "'a query ⇒ bool" where
  "non_empty_query Q = (∀X∈Q. card (fst X) ≥ 1)"

definition rwf_query :: "nat ⇒ vertices ⇒ 'a query ⇒ 'a query ⇒ bool" where
  "rwf_query n V Qp Qn ⟷ wf_query n V Qp Qn ∧ covering V Qp ∧ included V Qp ∧ included V Qn
                         ∧ non_empty_query Qp ∧ non_empty_query Qn"

lemma wf_tuple_empty: "wf_tuple n {} v ⟷ v = replicate n None"
  by (auto intro!: replicate_eqI simp add: wf_tuple_def in_set_conv_nth)

lemma table_empty: "table n {} X ⟷ (X = empty_table ∨ X = unit_table n)"
  by (auto simp add: wf_tuple_empty unit_table_def table_def)

context getIJ begin

lemma isSame_equi_dev:
  assumes "wf_set n V"
  assumes "wf_tuple n A t1"
  assumes "wf_tuple n B t2"
  assumes "s ⊆ A"
  assumes "s ⊆ B"
  assumes "A ⊆ V"
  assumes "B ⊆ V"
  shows "isSameIntersection t1 s t2 = (restrict s t1 = restrict s t2)"
proof -
  have "(∀i∈s. t1!i = t2!i) ⟷ (restrict s t1 = restrict s t2)" (is "?A ⟷ ?B")
  proof -
    have "?B ⟹ ?A"
    proof -
      assume "?B"
      have "⋀i. i∈s ⟹ t1!i = t2!i"
      proof -
        fix i assume "i ∈ s"
        then have "i ∈ A" using assms(4) by blast
        then have "i < n" using assms(1) assms(6) wf_set_def by auto
        then show "t1!i = t2!i" by (metis (no_types, lifting) ‹i ∈ s› ‹restrict s t1 = restrict s t2›
              assms(2) length_restrict nth_restrict wf_tuple_length)
      qed
      then show "?A" by blast
    qed
    moreover have "?A ⟹ ?B"
    proof -
      assume "?A"
      obtain "length (restrict s t1) = n" "length (restrict s t2) = n"
        using assms(2) assms(3) length_restrict wf_tuple_length by blast
      then have "⋀i. i < n ⟹ (restrict s t1)!i = (restrict s t2)!i"
      proof -
        fix i assume "i < n"
        then show "(restrict s t1)!i = (restrict s t2)!i"
        proof (cases "i ∈ s")
          case True
          then show ?thesis by (metis ‹∀i∈s. t1 ! i = t2 ! i› ‹i < n› ‹length (restrict s t1) = n›
                ‹length (restrict s t2) = n› length_restrict nth_restrict)
        next
          case False
          then show ?thesis
            by (metis (no_types, opaque_lifting) ‹i < n› assms(2) assms(3) assms(4) assms(5) wf_tuple_def
                wf_tuple_restrict_simple)
        qed
      qed
      then show "?B"
        by (metis ‹length (restrict s t1) = n› ‹length (restrict s t2) = n› nth_equalityI)
    qed
    then show ?thesis using calculation by linarith
  qed
  then show ?thesis by simp
qed

lemma wf_getIJ:
  assumes "card V ≥ 2"
  assumes "wf_set n V"
  assumes "(I, J) = getIJ Q_pos Q_neg V"
  shows "wf_set n I" and "wf_set n J"
  using assms unfolding wf_set_def by (metis Un_iff coreProperties)+

lemma wf_projectTable:
  assumes "wf_atable n X"
  shows "wf_atable n (projectTable I X) ∧ (fst (projectTable I X) = (fst X ∩ I))"
proof -
  obtain Y where "Y = projectTable I X" by simp
  obtain sX tX where "(sX, tX) = X" by (metis surj_pair)
  moreover obtain S where "S = I ∩ sX" by simp
  moreover obtain sY tY where "(sY, tY) = Y" by (metis surj_pair)
  then have "sY = S"
    using calculation(1) calculation(2) ‹Y = projectTable I X› by auto
  then have "⋀t. t ∈ tY ⟹ wf_tuple n S t"
  proof -
    fix t assume "t ∈ tY"
    obtain x where "x ∈ tX" "t = restrict I x" using ‹(sY, tY) = Y› ‹t ∈ tY› ‹Y = projectTable I X› calculation(1) by auto
    then have "wf_tuple n sX x"
    proof -
      have "table n sX tX" using assms(1) calculation(1) wf_atable_def by fastforce
      then show ?thesis using ‹x ∈ tX› table_def by blast
    qed
    then show "wf_tuple n S t" using ‹t = restrict I x› calculation(2) wf_tuple_restrict by blast      
  qed
  then have "∀t ∈ tY. wf_tuple n S t" by blast
  then have "table n S tY" using table_def by blast
  then show ?thesis
    by (metis ‹(sY, tY) = Y› ‹Y = projectTable I X› ‹sY = S› assms calculation(1) calculation(2) finite_Int fst_conv inf_commute snd_conv wf_atable_def)
qed

lemma set_filterQuery:
  assumes "QQ = filterQuery I Q"
  assumes "non_empty_query Q"
  shows "∀X∈Q. (card (fst X ∩ I) ≥ 1 ⟷ X ∈ QQ)"
proof -
  have "⋀X. X ∈ Q ⟹ (card (fst X ∩ I) ≥ 1 ⟷ X ∈ QQ)"
  proof -
    fix X assume "X ∈ Q"
    have "card (fst X ∩ I) ≥ 1 ⟹ X ∈ QQ"
    proof -
      assume "card (fst X ∩ I) ≥ 1"
      then have "(λ(s, _). s ∩ I ≠ {}) X" by force
      then show ?thesis by (simp add: ‹case X of (s, uu_) ⇒ s ∩ I ≠ {}› Set.is_empty_def ‹X ∈ Q› assms(1))        
    qed
    moreover have "X ∈ QQ ⟹ card (fst X ∩ I) ≥ 1"
    proof -
      assume "X ∈ QQ"
      have "(λ(s, _). s ∩ I ≠ {}) X" using Set.is_empty_def ‹X ∈ QQ› assms(1) by auto
      then have "fst X ∩ I ≠ {}" by (simp add: case_prod_beta')
      then show ?thesis
        by (metis One_nat_def Suc_leI ‹X ∈ Q› assms(2) card.infinite card_gt_0_iff finite_Int non_empty_query_def)
    qed
    then show "(card (fst X ∩ I) ≥ 1 ⟷ X ∈ QQ)"
      using calculation by blast
  qed
  then show ?thesis by blast
qed

lemma wf_filterQuery:
  assumes "I ⊆ V"
  assumes "card I ≥ 1"
  assumes "rwf_query n V Qp Qn"
  assumes "QQp = filterQuery I Qp"
  assumes "QQn = filterQueryNeg I Qn"
  shows "wf_query n I QQp QQn" "non_empty_query QQp" "covering I QQp"
proof -
  show "non_empty_query QQp"
    by (metis assms(3) assms(4) filterQuery.simps member_filter non_empty_query_def rwf_query_def)
  show "covering I QQp"
  proof -
    have "∀X∈Qp. (card (fst X ∩ I) ≥ 1 ⟷ X ∈ QQp)"
      using set_filterQuery assms(3) assms(4) rwf_query_def by fastforce
    have "(⋃(S, X)∈Qp. S) ∩ I ⊆ (⋃(S, _)∈QQp. S)" (is "?A ∩ I ⊆ ?B")
    proof (rule subsetI)
      fix x assume "x ∈ ?A ∩ I"
      have "x ∈ ?A" using ‹x ∈ (⋃(S, X)∈Qp. S) ∩ I› by blast
      then obtain S X where "(S, X) ∈ Qp" and "x ∈ S" by blast
      moreover have "(S, X) ∈ QQp" by (metis Int_iff One_nat_def Suc_le_eq
            ‹∀X∈Qp. (1 ≤ card (fst X ∩ I)) = (X ∈ QQp)› ‹x ∈ (⋃(S, X)∈Qp. S) ∩ I› assms(2)
            calculation(1) calculation(2) card_gt_0_iff empty_iff finite_Int fst_conv)
      ultimately show "x ∈ ?B" by auto
    qed
    then show ?thesis
      by (metis (mono_tags, lifting) assms(1) assms(3) covering_def inf.absorb_iff2 le_infI1 rwf_query_def)
  qed
  show "wf_query n I QQp QQn"
  proof -
    have "(∀X∈QQp. wf_atable n X)"
      using assms(3) assms(4) rwf_query_def wf_query_def by fastforce
    moreover have "(wf_set n I)"
      by (meson assms(1) assms(3) rwf_query_def subsetD wf_query_def wf_set_def)
    moreover have "card QQp ≥ 1"
    proof -
      have "covering I QQp" by (simp add: ‹covering I QQp›)
      have "¬ (Set.is_empty QQp)"
      proof (rule ccontr)
        assume "¬ (¬ (Set.is_empty QQp))"
        have "Set.is_empty QQp" using ‹¬ ¬ Set.is_empty QQp› by auto
        have "(⋃(S, X)∈QQp. S) = {}" by (metis SUP_empty Set.is_empty_def ‹Set.is_empty QQp›)
        then show "False"
          by (metis ‹covering I QQp› assms(2) card_eq_0_iff covering_def not_one_le_zero subset_empty)
      qed
      moreover have "finite QQp"
        by (metis assms(3) assms(4) card.infinite filterQuery.simps finite_filter not_one_le_zero rwf_query_def wf_query_def)
      then show ?thesis
        by (metis One_nat_def Set.is_empty_def Suc_leI calculation card_gt_0_iff)
    qed
    moreover have "QQn ⊆ Qn"
    proof -
      have "QQn = filterQueryNeg I Qn" by (simp add: assms(5))
      then show ?thesis by auto
    qed
    moreover have "wf_query n I QQp Qn"
      by (meson Un_iff assms(3) calculation(1) calculation(2) calculation(3) rwf_query_def wf_query_def)
    then have "(∀X∈Qn. wf_atable n X)" by (simp add: wf_query_def)
    then show ?thesis 
      by (meson ‹wf_query n I QQp Qn› calculation(4) subset_eq sup_mono wf_query_def)
  qed
qed

lemma wf_set_subset:
  assumes "I ⊆ V"
  assumes "card I ≥ 1"
  assumes "wf_set n V"
  shows "wf_set n I"
  using assms(1) assms(3) wf_set_def by auto

lemma wf_projectQuery:
  assumes "card I ≥ 1"
  assumes "wf_query n I Q Qn"
  assumes "non_empty_query Q"
  assumes "covering I Q"
  assumes "∀X∈Q. card (fst X ∩ I) ≥ 1"
  assumes "QQ = projectQuery I Q"
  assumes "included I Qn"
  assumes "non_empty_query Qn"
  shows "rwf_query n I QQ Qn"
proof -
  have "wf_query n I QQ Qn"
  proof -
    have "∀X∈QQ. wf_atable n X" using assms(2) assms(6) wf_query_def
      by (simp add: wf_projectTable wf_query_def)
    moreover have "wf_set n I" using assms(2) wf_query_def by blast
    moreover have "card QQ ≥ 1"
    proof -
      have "card QQ = card (Set.image (projectTable I) Q)" by (simp add: assms(6))
      then show ?thesis
        by (metis One_nat_def Suc_le_eq assms(2) card_gt_0_iff finite_imageI image_is_empty wf_query_def)
    qed
    then show ?thesis by (metis Un_iff assms(2) calculation(1) wf_query_def)
  qed
  moreover have "covering I QQ"
  proof -
    have "I ⊆ (⋃(S, X)∈Q. S)" using assms(4) covering_def by auto
    moreover have "(⋃(S, X)∈Q. S ∩ I) ⊆ (⋃(S, X)∈QQ. S)"
    proof (rule subsetI)
      fix x assume "x ∈ (⋃(S, X)∈Q. S ∩ I)"
      obtain S X where "(S, X) ∈ Q" and "x ∈ S ∩ I" using ‹x ∈ (⋃(S, X)∈Q. S ∩ I)› by blast
      then have "fst (projectTable I (S, X)) = S ∩ I" by simp
      have "wf_atable n (S, X)" using ‹(S, X) ∈ Q› assms(2) wf_query_def by blast
      then have "wf_atable n (projectTable I (S, X))" using wf_projectTable by blast 
      then show "x ∈ (⋃(S, X)∈QQ. S)" using ‹(S, X) ∈ Q› ‹x ∈ S ∩ I› assms(6) by fastforce
    qed
    moreover have "(⋃(S, X)∈Q. S ∩ I) = (⋃(S, X)∈Q. S) ∩ I" by blast
    then show ?thesis using calculation(1) calculation(2) covering_def inf_absorb2 by fastforce
  qed
  moreover have "included I QQ"
  proof -
    have "⋀S X. (S, X) ∈ QQ ⟹ S ⊆ I"
    proof -
      fix S X assume "(S, X) ∈ QQ"
      have "(S, X) ∈ Set.image (projectTable I) Q" using ‹(S, X) ∈ QQ› assms(6) by simp
      obtain XX where "XX ∈ Q" and "(S, X) = projectTable I XX" using ‹(S, X) ∈ projectTable I ` Q› by blast
      then have "S = I ∩ (fst XX)"
        by (metis projectTable.simps fst_conv inf_commute prod.collapse)
      then show "S ⊆ I" by simp
    qed
    then have "(∀(S, X)∈QQ. S ⊆ I)" by blast
    then show ?thesis by (simp add: included_def)
  qed
  moreover have "non_empty_query QQ" using assms(5) assms(6) non_empty_query_def by fastforce
  then show ?thesis
    by (simp add: assms(7) assms(8) calculation(1) calculation(2) calculation(3) rwf_query_def)
qed

lemma wf_firstRecursiveCall:
  assumes "rwf_query n V Qp Qn"
  assumes "card V ≥ 2"
  assumes "(I, J) = getIJ Qp Qn V"
  assumes "Q_I_pos = projectQuery I (filterQuery I Qp)"
  assumes "Q_I_neg = filterQueryNeg I Qn"
  shows "rwf_query n I Q_I_pos Q_I_neg"
proof -
  obtain "I ⊆ V" "card I ≥ 1" using assms(2) assms(3) getIJProperties(5) getIJProperties(1) by fastforce
  define tQ where "tQ = filterQuery I Qp"
  obtain "wf_query n I tQ Q_I_neg" "non_empty_query tQ" "covering I tQ"
    by (metis wf_filterQuery(1) wf_filterQuery(2) wf_filterQuery(3)
        ‹1 ≤ card I› ‹I ⊆ V› assms(1) assms(5) tQ_def)
  moreover obtain "card I ≥ 1" and "∀X∈tQ. card (fst X ∩ I) ≥ 1"
    using set_filterQuery ‹1 ≤ card I› assms(1) rwf_query_def tQ_def by fastforce
  moreover have "included I Q_I_neg" by (simp add: assms(5) included_def)
  then show ?thesis
    by (metis wf_projectQuery ‹⋀thesis. (⟦wf_query n I tQ Q_I_neg; non_empty_query tQ; covering I tQ⟧ ⟹ thesis) ⟹ thesis›
        assms(1) assms(4) assms(5) calculation(4) calculation(5) filterQueryNeg.simps member_filter non_empty_query_def rwf_query_def tQ_def)
qed

lemma wf_atable_subset:
  assumes "table n V X"
  assumes "Y ⊆ X"
  shows "table n V Y"
  by (meson assms(1) assms(2) subsetD table_def)

lemma same_set_semiJoin:
  "fst (semiJoin x other) = fst x"
proof -
  obtain sx tx where "x = (sx, tx)" by (metis surj_pair)
  obtain so to where "other = (so, to)" by (metis surj_pair)
  then show ?thesis by (simp add: ‹x = (sx, tx)›)
qed

lemma wf_semiJoin:
  assumes "card J ≥ 1"
  assumes "wf_query n J Q Qn"
  assumes "non_empty_query Q"
  assumes "covering J Q"
  assumes "∀X∈Q. card (fst X ∩ J) ≥ 1"
  assumes "QQ = (Set.image (λtab. semiJoin tab (st, t)) Q)"
  shows "wf_query n J QQ Qn" "non_empty_query QQ" "covering J QQ"
proof -
  show "wf_query n J QQ Qn"
  proof -
    have "∀X∈QQ. wf_atable n X"
    proof -
      have "⋀X. X∈QQ ⟹ wf_atable n X"
      proof -
        fix X assume "X ∈ QQ"
        obtain Y where "Y ∈ Q" and "X = semiJoin Y (st, t)" using ‹X ∈ QQ› assms(6) by blast
        then have "wf_atable n Y" using assms(2) wf_query_def by blast
        then show "wf_atable n X"
        proof -
          have "fst X = fst Y"
            by (metis ‹X = semiJoin Y (st, t)› fst_conv prod.collapse semiJoin.simps)
          moreover have "snd X ⊆ snd Y"
            by (metis ‹X = semiJoin Y (st, t)› member_filter prod.collapse semiJoin.simps snd_conv subsetI)
          then have "table n (fst X) (snd X)" by (metis ‹wf_atable n Y› calculation wf_atable_def wf_atable_subset)
          moreover have "finite (fst X)" by (metis ‹wf_atable n Y› calculation(1) wf_atable_def)
          then show ?thesis by (simp add: calculation(2) wf_atable_def)
        qed
      qed
      then show ?thesis by blast
    qed
    moreover have "wf_set n J" using assms(2) wf_query_def by blast
    moreover have "card QQ ≥ 1"
      by (metis One_nat_def Suc_leI assms(2) assms(6) card.infinite card_gt_0_iff finite_imageI image_is_empty wf_query_def)
    then show ?thesis using calculation(1) calculation(2) wf_query_def Un_iff assms(2) by metis
  qed
  show "non_empty_query QQ"
    by (metis (no_types, lifting) assms(3) assms(6) image_iff non_empty_query_def same_set_semiJoin)
  show "covering J QQ"
  proof -
    have "(⋃(S, X)∈Q. S) = (⋃(S, X)∈QQ. S)" using assms(6) same_set_semiJoin by auto
    then show ?thesis by (metis assms(4) covering_def)
  qed
qed

lemma newQuery_equiv_def:
  "newQuery V Q (st, t) = projectQuery V (Set.image (λtab. semiJoin tab (st, t)) Q)"
  by (metis image_image newQuery.simps projectQuery.elims)

lemma included_project:
  "included V (projectQuery V Q)"
proof -
  have "⋀S X. (S, X)∈(projectQuery V Q) ⟹ S ⊆ V"
  proof -
    fix S X assume "(S, X)∈(projectQuery V Q)"
    obtain SS XX where "(S, X) = projectTable V (SS, XX)"
      using ‹(S, X) ∈ projectQuery V Q› by auto
    then have "S = SS ∩ V" by auto
    then show "S ⊆ V" by simp
  qed
  then show ?thesis by (metis case_prodI2 included_def)
qed

lemma non_empty_newQuery:
  assumes "Q1 = filterQuery J Q0"
  assumes "Q2 = newQuery J Q1 (I, t)"
  assumes "∀X∈Q0. wf_atable n X"
  shows "non_empty_query Q2"
proof -
  have "⋀X. X∈Q2 ⟹ card (fst X) ≥ 1"
  proof -
    fix X assume "X ∈ Q2"
    obtain X2 where "X = projectTable J X2" and "X2 ∈ Set.image (λtab. semiJoin tab (I, t)) Q1"
      by (metis (mono_tags, lifting) newQuery.simps ‹X ∈ Q2› assms(2) image_iff)
    then have "card (fst X2 ∩ J) ≥ 1"
    proof -
      obtain X1 where "X1 ∈ Q1" and "X2 = semiJoin X1 (I, t)"
        using ‹X2 ∈ (λtab. semiJoin tab (I, t)) ` Q1› by blast
      then have "fst X1 = fst X2" by (simp add: same_set_semiJoin)
      moreover have "X1 ∈ filterQuery J Q0" using ‹X1 ∈ Q1› assms(1) by blast
      then have "(λ(s, _). s ∩ J ≠ {}) X1" using Set.is_empty_def by auto
      then have "¬ (Set.is_empty (fst X1 ∩ J))" by (simp add: Set.is_empty_def case_prod_beta')
      then show ?thesis
        by (metis filterQuery.elims One_nat_def Set.is_empty_def Suc_leI ‹X1 ∈ Q1› assms(1)
            assms(3) calculation card_gt_0_iff finite_Int member_filter wf_atable_def)
    qed
    then show "card (fst X) ≥ 1"
      by (metis projectTable.simps ‹X = projectTable J X2› fst_conv prod.collapse)
  qed
  then show ?thesis by (simp add: non_empty_query_def)
qed

lemma wf_newQuery:
  assumes "card J ≥ 1"
  assumes "wf_query n J Q Qn0"
  assumes "non_empty_query Q"
  assumes "covering J Q"
  assumes "∀X∈Q. card (fst X ∩ J) ≥ 1"
  assumes "QQ = newQuery J Q t"
  assumes "QQn = newQuery J Qn t"
  assumes "non_empty_query Qn"
  assumes "Qn = filterQuery J Qn0"
  shows "rwf_query n J QQ QQn"
proof -
  obtain tt st where "(st, tt) = t" by (metis surj_pair)
  have "QQ = projectQuery J (Set.image (λtab. semiJoin tab (st, tt)) Q)"
    by (metis ‹(st, tt) = t› assms(6) newQuery_equiv_def)
  define QS where "QS = Set.image (λtab. semiJoin tab (st, tt)) Q"
  obtain "wf_query n J QS Qn0" "non_empty_query QS" "covering J QS"
    by (metis wf_semiJoin(1) wf_semiJoin(2) wf_semiJoin(3) QS_def
        assms(1) assms(2) assms(3) assms(4) assms(5))
  moreover have "∀X∈QS. card (fst X ∩ J) ≥ 1" using QS_def assms(5) by auto
  then have "∀X∈(projectQuery J QS). wf_atable n X"
    by (metis (no_types, lifting) projectQuery.simps Un_iff calculation(1) image_iff
        wf_projectTable wf_query_def)
  then have "wf_query n J QQ QQn"
  proof -
    have "⋀X. X∈QQn ⟹ wf_atable n X"
    proof -
      fix X assume "X ∈ QQn"
      have "QQn = projectQuery J (Set.image (λtab. semiJoin tab (st, tt)) Qn)"
        using newQuery_equiv_def ‹(st, tt) = t› assms(7) by blast
      then obtain XX where "X = projectTable J XX" "XX ∈ (Set.image (λtab. semiJoin tab (st, tt)) Qn)"
        using ‹X ∈ QQn› by auto
      then obtain XXX where "XX = semiJoin XXX (st, tt)" "XXX ∈ Qn" by blast
      then have "wf_atable n XXX"
        by (metis filterQuery.elims Un_iff assms(2) assms(9) member_filter wf_query_def)
      then have "wf_atable n XX"
      proof -
        have "fst XX = fst XXX"
          by (simp add: same_set_semiJoin ‹XX = semiJoin XXX (st, tt)›)
        moreover have "snd XX = Set.filter (isSameIntersection tt (fst XX ∩ st)) (snd XXX)"
          by (metis semiJoin.simps ‹XX = semiJoin XXX (st, tt)› calculation prod.collapse snd_conv)
        moreover have "snd XX ⊆ snd XXX" using calculation(2) by auto
        then show ?thesis
          by (metis wf_atable_subset ‹wf_atable n XXX› calculation(1) wf_atable_def)
      qed
      then show "wf_atable n X" by (simp add: wf_projectTable ‹X = projectTable J XX›)
    qed
    then have "∀X∈QQn. wf_atable n X" by blast
    then have "∀X∈(QQ ∪ QQn). wf_atable n X"
      using QS_def ‹QQ = projectQuery J ((λtab. semiJoin tab (st, tt)) ` Q)› ‹∀X∈projectQuery J QS. wf_atable n X› by blast
    moreover have "card QQ ≥ 1"
      by (metis (no_types, lifting) newQuery.simps One_nat_def Suc_leI ‹(st, tt) = t› assms(2)
          assms(6) card.infinite card_gt_0_iff finite_imageI image_is_empty wf_query_def)
    then show ?thesis using assms(2) calculation wf_query_def by blast
  qed
  moreover have "included J QQn"
  proof -
    have "QQn = projectQuery J (Set.image (λtab. semiJoin tab (st, tt)) Qn)"
      using newQuery_equiv_def ‹(st, tt) = t› assms(7) by blast
    then show ?thesis using included_project by blast
  qed
  moreover have "covering J QQ"
  proof -
    have "QQ = projectQuery J ((λtab. semiJoin tab (st, tt)) `Q)"
      using ‹QQ = projectQuery J ((λtab. semiJoin tab (st, tt)) ` Q)› by blast
    then have "covering J ((λtab. semiJoin tab (st, tt)) `Q)" using QS_def calculation(3) by blast
    then have "J ⊆ (⋃(S, X)∈(((λtab. semiJoin tab (st, tt)) `Q)). S)"
      by (simp add: covering_def)
    then have "J ⊆ (⋃(S, X)∈(((λtab. semiJoin tab (st, tt)) `Q)). S) ∩ J" by blast
    moreover have "(⋃(S, X)∈(((λtab. semiJoin tab (st, tt)) `Q)). S) ∩ J  ⊆ (⋃(S, X)∈(((λtab. semiJoin tab (st, tt)) `Q)). S ∩ J)"
      using image_cong by auto
    then have "(⋃(S, X)∈((λtab. semiJoin tab (st, tt)) `Q). S) ∩ J  ⊆ (⋃(S, X)∈(projectQuery J ((λtab. semiJoin tab (st, tt)) `Q)). S)"
      by auto
    then show ?thesis
      by (metis ‹J ⊆ (⋃(S, X)∈(λtab. semiJoin tab (st, tt)) ` Q. S)› ‹QQ = projectQuery J ((λtab. semiJoin tab (st, tt)) ` Q)› covering_def inf_absorb2)
  qed
  moreover have "non_empty_query QQ" using QS_def ‹QQ = projectQuery J ((λtab. semiJoin tab (st, tt)) ` Q)›
      ‹∀X∈QS. 1 ≤ card (fst X ∩ J)› non_empty_query_def by fastforce
  moreover have "non_empty_query QQn"
    by (metis non_empty_newQuery Un_iff ‹(st, tt) = t› assms(7) assms(9) calculation(1) wf_query_def)
  then show ?thesis
    using included_project ‹QQ = projectQuery J ((λtab. semiJoin tab (st, tt)) ` Q)›
      calculation(4) calculation(5) calculation(6) calculation(7) rwf_query_def by blast
qed

lemma subset_Q_neg:
  assumes "rwf_query n V Q Qn"
  assumes "QQn ⊆ Qn"
  shows "rwf_query n V Q QQn"
proof -
  have "wf_query n V Q QQn"
  proof -
    have "∀X∈QQn. wf_atable n X" by (meson Un_iff assms(1) assms(2) rwf_query_def subsetD wf_query_def)
    then show ?thesis
      by (meson UnE UnI1 assms(1) rwf_query_def wf_query_def)
  qed
  moreover have "included V QQn" by (meson assms(1) assms(2) included_def rwf_query_def subsetD)
  then show ?thesis by (metis (full_types) assms(2) non_empty_query_def subsetD assms(1) calculation rwf_query_def)
qed

lemma wf_secondRecursiveCalls:
  assumes "card V ≥ 2"
  assumes "rwf_query n V Q Qn"
  assumes "(I, J) = getIJ Q Qn V"
  assumes "Qns ⊆ Qn"
  assumes "Q_J_neg = filterQuery J Qns"
  assumes "Q_J_pos = filterQuery J Q"
  shows "rwf_query n J (newQuery J Q_J_pos t) (newQuery J Q_J_neg t)"
proof -
  have "∀X∈Q_J_pos. card (fst X ∩ J) ≥ 1"
    using set_filterQuery assms(2) assms(6) rwf_query_def by fastforce
  moreover have "card J ≥ 1" by (metis assms(1) assms(3) getIJ.coreProperties getIJ_axioms)
  moreover have "wf_query n J Q_J_pos Qns"
  proof -
    have "wf_query n J Q Qns"
      by (metis subset_Q_neg wf_set_subset assms(1) assms(2) assms(3) assms(4)
          getIJ.coreProperties getIJ_axioms rwf_query_def sup_ge2 wf_query_def)
    moreover have "Q_J_pos ⊆ Q" using assms(6) by auto
    then have "∀X∈(Q_J_pos ∪ Qns). wf_atable n X" using calculation wf_query_def by fastforce
    moreover have "card Q_J_pos ≥ 1"
      by (metis wf_filterQuery(1) assms(1) assms(2) assms(3) assms(6) getIJ.coreProperties
          getIJ_axioms sup_ge2 wf_query_def)
    then show ?thesis using calculation(1) calculation(2) wf_query_def by blast
  qed
  moreover have "non_empty_query Q_J_pos"
    by (metis wf_filterQuery(2) assms(1) assms(2) assms(3) assms(6) getIJ.coreProperties
        getIJ_axioms sup_ge2)
  moreover have  "covering J Q_J_pos"
    by (metis wf_filterQuery(3) assms(1) assms(2) assms(3) assms(6) getIJ.coreProperties
        getIJ_axioms sup_ge2)
  moreover have "non_empty_query Q_J_neg"
    by (metis (no_types, lifting) filterQuery.elims assms(2) assms(4) assms(5) member_filter
        non_empty_query_def rwf_query_def subsetD)
  then show ?thesis
    using wf_newQuery assms(5) calculation(1) calculation(2) calculation(3) calculation(4)
      calculation(5) by blast
qed

lemma simple_merge_option:
  "merge_option (a, b) = None ⟷ (a = None ∧ b = None)"
  using merge_option.elims by blast

lemma wf_merge:
  assumes "wf_tuple n I t1"
  assumes "wf_tuple n J t2"
  assumes "V = I ∪ J"
  assumes "t = merge t1 t2"
  shows "wf_tuple n V t"
proof -
  have "⋀i. i < n ⟹ (t ! i = None ⟷ i ∉ V)"
  proof -
    fix i
    assume "i < n"
    show "t ! i = None ⟷ i ∉ V"
    proof (cases "t ! i = None")
      case True
      have "t = merge t1 t2" by (simp add: assms(4))
      then have "... = map merge_option (zip t1 t2)" by simp
      then have "merge_option (t1 ! i, t2 ! i) = None"
        by (metis True ‹i < n› assms(1) assms(2) assms(4) length_zip min_less_iff_conj nth_map nth_zip wf_tuple_def)
      obtain "t1 ! i = None" and "t2 ! i = None"
        by (meson ‹merge_option (t1 ! i, t2 ! i) = None› simple_merge_option)
      then show ?thesis
        using True ‹i < n› assms(1) assms(2) assms(3) wf_tuple_def by auto
    next
      case False
      have "t = map merge_option (zip t1 t2)" by (simp add: assms(4))
      then obtain x where "merge_option (t1 ! i, t2 ! i) = Some x"
        by (metis False ‹i < n› assms(1) assms(2) length_zip merge_option.elims min_less_iff_conj nth_map nth_zip wf_tuple_def)
      then show ?thesis
        by (metis False UnI1 UnI2 ‹i < n› assms(1) assms(2) assms(3) option.distinct(1) simple_merge_option wf_tuple_def)
    qed
  qed
  moreover have "length t = n"
  proof -
    obtain "length t1 = n" and "length t2 = n"
      using assms(1) assms(2) wf_tuple_def by blast
    then have "length (zip t1 t2) = n" by simp
    then show ?thesis by (simp add: assms(4))
  qed
  then show ?thesis by (simp add: calculation wf_tuple_def)
qed

lemma wf_inter:
  assumes "rwf_query n {i} Q Qn"
  assumes "(sa, a) ∈ Q"
  assumes "(sb, b) ∈ Q"
  shows "table n {i} (a ∩ b)"
proof -
  obtain "card sa ≥ 1" "card sb ≥ 1"
    by (metis assms(1) assms(2) assms(3) fst_conv non_empty_query_def rwf_query_def)
  have "included {i} Q" using assms(1) rwf_query_def by blast
  then have "(∀(S, X)∈Q. S ⊆ {i})" by (simp add: included_def)
  then obtain "sa ⊆ {i}" "sb ⊆ {i}" using assms(2) assms(3) by blast
  then obtain "sa = {i}" "sb = {i}"
    by (metis ‹1 ≤ card sa› ‹1 ≤ card sb› card.empty not_one_le_zero subset_singletonD)
  then show ?thesis
    using assms(1) assms(2) inf_le1 prod.sel(1) prod.sel(2) rwf_query_def wf_atable_def
      wf_atable_subset wf_query_def Un_iff by metis
qed

lemma table_subset:
  assumes "table n V T"
  assumes "S ⊆ T"
  shows "table n V S"
  using wf_atable_subset assms(1) assms(2) by blast

lemma wf_base_case:
  assumes "card V = 1"
  assumes "rwf_query n V Q Qn"
  assumes "R = genericJoin V Q Qn"
  shows "table n V R"
proof -
  have "wf_query n V Q Qn ∧ included V Q ∧ non_empty_query Q ⟹ table n V ((⋂(_, x) ∈ Q. x) - (⋃(_, x) ∈ Qn. x))"
  proof (induction "card Q - 1" arbitrary: Q)
    case 0
    have "card Q = 1"
      by (metis "0.hyps" "0.prems" One_nat_def le_add_diff_inverse plus_1_eq_Suc wf_query_def)
    obtain s x where "Q = {(s, x)}"
      by (metis One_nat_def ‹card Q = 1› card_eq_0_iff card_eq_SucD card_mono finite_insert insertE
          nat.simps(3) not_one_le_zero subrelI)
    moreover obtain i where "V = {i}" using assms(1) card_1_singletonE by auto
    then have "card s ≥ 1"
    proof -
      have "(s, x) ∈ Q" by (simp add: calculation)
      moreover obtain X where "X = (s, x)" by simp
      then show ?thesis
        using "0.prems" calculation non_empty_query_def rwf_query_def by fastforce
    qed
    moreover obtain i where "V = {i}" using ‹⋀thesis. (⋀i. V = {i} ⟹ thesis) ⟹ thesis› by blast
    then have "s = {i}"
    proof -
      have "included {i} Q" using "0.prems" ‹V = {i}› rwf_query_def by simp
      then show ?thesis
        by (metis ‹V = {i}› assms(1) calculation(1) calculation(2) card_seteq case_prodD finite.emptyI finite.insertI included_def singletonI)
    qed
    moreover have "table n s x"
      using "0.prems" calculation(1) rwf_query_def wf_atable_def wf_query_def
      by (simp add: rwf_query_def wf_atable_def wf_query_def)
    then show ?case
      by (simp add: wf_atable_subset ‹V = {i}› calculation(1) calculation(3))
  next
    case (Suc y)
    obtain xx where "xx ∈ Q" by (metis Suc.hyps(2) all_not_in_conv card.empty nat.simps(3) zero_diff)
    moreover obtain H where "H = Q - {xx}" by simp
    then have "card H - 1 = y"
      by (metis Suc.hyps(2) calculation card_Diff_singleton card.infinite diff_Suc_1 less_imp_le not_one_le_zero zero_less_Suc zero_less_diff)
    moreover have "wf_query n V H Qn ∧ included V H ∧ non_empty_query H"
    proof -
      have "wf_query n V H Qn"
        using DiffD1 Suc.hyps(2) Suc.prems ‹H = Q - {xx}› calculation(1) card_Diff_singleton
          card.infinite le_add1 not_one_le_zero plus_1_eq_Suc wf_query_def
        by (metis (no_types, lifting) Un_iff)
      then show ?thesis
        using DiffD1 Suc.prems ‹H = Q - {xx}› included_def non_empty_query_def by fastforce
    qed
    then have "wf_query n V H Qn ∧ included V H ∧ non_empty_query H" by simp
    then have "table n V ((⋂(_, x)∈H. x) - (⋃(_, x)∈Qn. x))" using Suc.hyps(1) calculation(2) by simp
    moreover obtain sa a where "(sa, a) ∈ H"
      by (metis One_nat_def Suc.hyps(2) ‹H = Q - {xx}› calculation(1) calculation(2) card.empty card_eq_0_iff card_le_Suc0_iff_eq diff_is_0_eq' equals0I insert_Diff le0 nat.simps(3) prod.collapse singletonD)
    moreover have "¬ (Set.is_empty sa)"
      by (metis Set.is_empty_def ‹wf_query n V H Qn ∧ included V H ∧ non_empty_query H› calculation(4)
          card.empty non_empty_query_def not_one_le_zero prod.sel(1))
    then have "table n V (((⋂(_, x) ∈ H. x) ∩ (snd xx)) - (⋃(_, x)∈Qn. x))"
      by (metis Diff_Int2 Diff_Int_distrib2 IntE calculation(3) table_def)
    then show ?case using INF_insert Int_commute ‹H = Q - {xx}› calculation(1) insert_Diff snd_def by metis
  qed
  then show ?thesis
    using assms(1) assms(2) assms(3) genericJoin.simps le_numeral_extra(4) rwf_query_def by auto
qed

lemma filter_Q_J_neg_same:
  assumes "card V ≥ 2"
  assumes "(I, J) = getIJ Q Qn V"
  assumes "Q_I_neg = filterQueryNeg I Qn"
  assumes "rwf_query n V Q Qn"
  shows "filterQuery J (Qn - Q_I_neg) = Qn - Q_I_neg" (is "?A = ?B")
proof-
  have "?A ⊆ ?B" by (simp add: subset_iff)
  moreover have "?B ⊆ ?A"
  proof (rule subsetI)
    fix x assume "x ∈ Qn - Q_I_neg"
    obtain A X where "(A, X) = x" by (metis surj_pair)
    have "card (A ∩ J) ≥ 1"
    proof (rule ccontr)
      assume "¬ (card (A ∩ J) ≥ 1)"
      have "Set.is_empty (A ∩ J)"
        by (metis One_nat_def Set.is_empty_def Suc_leI Suc_le_lessD ‹¬ 1 ≤ card (A ∩ J)› assms(1)
            assms(2) card_gt_0_iff finite_Int getIJ.coreProperties getIJ_axioms)
      moreover have "A ⊆ I"
      proof -
        have "(A, X) ∈ Qn" using ‹(A, X) = x› ‹x ∈ Qn - Q_I_neg› by auto
        then have "included V Qn" using assms(4) rwf_query_def by blast
        then have "A ⊆ V" using ‹(A, X) ∈ Qn› included_def by fastforce
        then show ?thesis
          by (metis Set.is_empty_def UnE assms(1) assms(2) calculation disjoint_iff_not_equal
              getIJProperties(5) subsetD subsetI)
      qed
      then have "(A, X) ∈ Q_I_neg" using ‹(A, X) = x› ‹x ∈ Qn - Q_I_neg› assms(3) by auto
      then show "False" using ‹(A, X) = x› ‹x ∈ Qn - Q_I_neg› by blast
    qed
    then show "x ∈ ?A" using ‹(A, X) = x› ‹x ∈ Qn - Q_I_neg›
      by (metis Diff_subset subset_Q_neg assms(4) fst_conv rwf_query_def set_filterQuery)
  qed
  then show ?thesis by auto
qed

lemma vars_genericJoin:
  assumes "card V ≥ 2"
  assumes "(I, J) = getIJ Q Qn V"
  assumes "Q_I_pos = projectQuery I (filterQuery I Q)"
  assumes "Q_I_neg = filterQueryNeg I Qn"
  assumes "R_I = genericJoin I Q_I_pos Q_I_neg"
  assumes "Q_J_neg = filterQuery J (Qn - Q_I_neg)"
  assumes "Q_J_pos = filterQuery J Q"
  assumes "X = {(t, genericJoin J (newQuery J Q_J_pos (I, t)) (newQuery J Q_J_neg (I, t))) | t . t ∈ R_I}"
  assumes "R = (⋃(t, x) ∈ X. {merge xx t | xx . xx ∈ x})"
  assumes "rwf_query n V Q Qn"
  shows "R = genericJoin V Q Qn"
proof -
  have "filterQuery J (Qn - Q_I_neg) = Qn - Q_I_neg"
    using assms(1) assms(10) assms(2) assms(4) filter_Q_J_neg_same by blast
  then have "Q_J_neg = Qn - Q_I_neg" by (simp add: assms(6))
  moreover have "genericJoin V Q Qn =
    (if card V ≤ 1 then
      (⋂(_, x) ∈ Q. x) - (⋃(_, x) ∈ Qn. x)
    else
      let (I, J) = getIJ Q Qn V in
      let Q_I_pos = projectQuery I (filterQuery I Q) in
      let Q_I_neg = filterQueryNeg I Qn in
      let R_I = genericJoin I Q_I_pos Q_I_neg in
      let Q_J_neg = Qn - Q_I_neg in
      let Q_J_pos = filterQuery J Q in
      let X = {(t, genericJoin J (newQuery J Q_J_pos (I, t)) (newQuery J Q_J_neg (I, t))) | t . t ∈ R_I} in
      (⋃(t, x) ∈ X. {merge xx t | xx . xx ∈ x}))"
    by simp
  moreover have "¬ (card V ≤ 1)" using assms(1) by linarith
  then have gen: "genericJoin V Q Qn = (let (I, J) = getIJ Q Qn V in
      let Q_I_pos = projectQuery I (filterQuery I Q) in
      let Q_I_neg = filterQueryNeg I Qn in
      let R_I = genericJoin I Q_I_pos Q_I_neg in
      let Q_J_neg = Qn - Q_I_neg in
      let Q_J_pos = filterQuery J Q in
      let X = {(t, genericJoin J (newQuery J Q_J_pos (I, t)) (newQuery J Q_J_neg (I, t))) | t . t ∈ R_I} in
      (⋃(t, x) ∈ X. {merge xx t | xx . xx ∈ x}))"
    using assms by simp
  then have "... = (
      let Q_I_pos = projectQuery I (filterQuery I Q) in
      let Q_I_neg = filterQueryNeg I Qn in
      let R_I = genericJoin I Q_I_pos Q_I_neg in
      let Q_J_neg = Qn - Q_I_neg in
      let Q_J_pos = filterQuery J Q in
      let X = {(t, genericJoin J (newQuery J Q_J_pos (I, t)) (newQuery J Q_J_neg (I, t))) | t . t ∈ R_I} in
      (⋃(t, x) ∈ X. {merge xx t | xx . xx ∈ x}))"
    using assms(2) by (metis (no_types, lifting) case_prod_conv)
  then show ?thesis using assms by (metis calculation(1) gen)
qed

lemma base_genericJoin:
  assumes "card V ≤ 1"
  shows "genericJoin V Q Qn =  (⋂(_, x) ∈ Q. x) - (⋃(_, x) ∈ Qn. x)"
proof -
  have "genericJoin V Q Qn =
    (if card V ≤ 1 then
      (⋂(_, x) ∈ Q. x) - (⋃(_, x) ∈ Qn. x)
    else
      let (I, J) = getIJ Q Qn V in
      let Q_I_pos = projectQuery I (filterQuery I Q) in
      let Q_I_neg = filterQueryNeg I Qn in
      let R_I = genericJoin I Q_I_pos Q_I_neg in

      let Q_J_neg = Qn - Q_I_neg in
      let Q_J_pos = filterQuery J Q in
      let X = {(t, genericJoin J (newQuery J Q_J_pos (I, t)) (newQuery J Q_J_neg (I, t))) | t . t ∈ R_I} in
      (⋃(t, x) ∈ X. {merge xx t | xx . xx ∈ x}))"
    by simp
  then show ?thesis using assms by auto
qed

lemma wf_genericJoin:
  "⟦rwf_query n V Q Qn; card V ≥ 1⟧ ⟹ table n V (genericJoin V Q Qn)"
proof (induction V Q Qn rule: genericJoin.induct)
  case (1 V Q Qn)
  then show ?case
  proof (cases "card V ≤ 1")
    case True
    then show ?thesis using "1.prems"(1) "1.prems"(2) le_antisym wf_base_case by blast
  next
    case False
    obtain I J where "(I, J) = getIJ Q Qn V" by (metis surj_pair)
    define Q_I_pos where "Q_I_pos = projectQuery I (filterQuery I Q)"
    define Q_I_neg where "Q_I_neg = filterQueryNeg I Qn"
    define R_I where "R_I = genericJoin I Q_I_pos Q_I_neg"
    define Q_J_neg where "Q_J_neg = filterQuery J (Qn - Q_I_neg)"
    define Q_J_pos where "Q_J_pos = filterQuery J Q"
    define X where "X = {(t, genericJoin J (newQuery J Q_J_pos (I, t)) (newQuery J Q_J_neg (I, t))) | t . t ∈ R_I}"
    define R where "R = (⋃(t, x) ∈ X. {merge xx t | xx . xx ∈ x})"
    moreover have "card V ≥ 2" using False by auto
    then have "R = genericJoin V Q Qn"
      using vars_genericJoin[where ?V=V and ?I=I and ?J=J and ?Q_I_pos=Q_I_pos and ?Q=Q and ?Qn=Qn and
        ?Q_I_neg=Q_I_neg and ?R_I=R_I and ?Q_J_neg=Q_J_neg and ?Q_J_pos=Q_J_pos]
      using "1.prems"(1) Q_I_neg_def Q_I_pos_def Q_J_neg_def Q_J_pos_def R_I_def X_def ‹(I, J) = getIJ Q Qn V› calculation by blast
    obtain "card I ≥ 1" "card J ≥ 1"
      using ‹(I, J) = getIJ Q Qn V› ‹2 ≤ card V› getIJ.getIJProperties(1) getIJProperties(2) getIJ_axioms by blast
    moreover have "rwf_query n I Q_I_pos Q_I_neg"
      using "1.prems"(1) Q_I_neg_def Q_I_pos_def ‹(I, J) = getIJ Q Qn V› ‹2 ≤ card V› getIJ.wf_firstRecursiveCall getIJ_axioms by blast
    moreover have "⋀t. t∈R_I ⟹ table n J (genericJoin J (newQuery J Q_J_pos (I, t)) (newQuery J Q_J_neg (I, t)))"
    proof -
      fix t assume "t ∈ R_I"
      have "rwf_query n J (newQuery J Q_J_pos (I, t)) (newQuery J Q_J_neg (I, t))"
        using "1.prems"(1) Q_J_neg_def Q_J_pos_def ‹(I, J) = getIJ Q Qn V› ‹2 ≤ card V›
          getIJ.wf_secondRecursiveCalls getIJ_axioms by fastforce
      then show "table n J (genericJoin J (newQuery J Q_J_pos (I, t)) (newQuery J Q_J_neg (I, t)))"
        by (metis "1.IH"(2) "1.prems"(1) False Q_I_neg_def Q_J_neg_def Q_J_pos_def ‹(I, J) = getIJ Q Qn V›
            ‹2 ≤ card V› calculation(3) filter_Q_J_neg_same)
    qed
    then have "⋀t xx. t ∈ R_I ∧ xx ∈ (genericJoin J (newQuery J Q_J_pos (I, t)) (newQuery J Q_J_neg (I, t)))
               ⟹ wf_tuple n V (merge xx t)"
    proof -
      fix t xx assume "t ∈ R_I ∧ xx ∈ genericJoin J (newQuery J Q_J_pos (I, t)) (newQuery J Q_J_neg (I, t))"
      have "V = I ∪ J"
        using ‹(I, J) = getIJ Q Qn V› ‹2 ≤ card V› getIJ.coreProperties getIJ_axioms by metis
      moreover have "wf_tuple n J xx"
        using ‹⋀t. t ∈ R_I ⟹ table n J (genericJoin J (newQuery J Q_J_pos (I, t)) (newQuery J Q_J_neg (I, t)))›
          ‹t ∈ R_I ∧ xx ∈ genericJoin J (newQuery J Q_J_pos (I, t)) (newQuery J Q_J_neg (I, t))› table_def by blast
      moreover have "wf_tuple n I t"
        by (metis "1.IH"(1) False Q_I_neg_def Q_I_pos_def
            R_I_def ‹(I, J) = getIJ Q Qn V› ‹⋀thesis. (⟦1 ≤ card I; 1 ≤ card J⟧ ⟹ thesis) ⟹ thesis›
            ‹rwf_query n I Q_I_pos Q_I_neg› ‹t ∈ R_I ∧ xx ∈ genericJoin J (newQuery J Q_J_pos (I, t))
            (newQuery J Q_J_neg (I, t))› table_def)
      then show "wf_tuple n V (merge xx t)"
        by (metis calculation(1) calculation(2) sup_commute wf_merge)
    qed
    then have "∀t∈R_I. ∀xx ∈ (genericJoin J (newQuery J Q_J_pos (I, t)) (newQuery J Q_J_neg (I, t))).
                wf_tuple n V (merge xx t)" by blast
    then have "∀x∈R. wf_tuple n V x" using R_def X_def by blast
    then show ?thesis using ‹R = genericJoin V Q Qn› table_def by blast
  qed
qed

subsection ‹Correctness›

lemma base_correctness:
  assumes "card V = 1"
  assumes "rwf_query n V Q Qn"
  assumes "R = genericJoin V Q Qn"
  shows "z ∈ genericJoin V Q Qn ⟷ wf_tuple n V z ∧ (∀(A, X)∈Q. restrict A z ∈ X) ∧ (∀(A, X)∈Qn. restrict A z ∉ X)"
proof -
  have "z ∈ genericJoin V Q Qn ⟹ wf_tuple n V z ∧ (∀(A, X)∈Q. restrict A z ∈ X) ∧ (∀(A, X)∈Qn. restrict A z ∉ X)"
  proof -
    fix z assume "z ∈ genericJoin V Q Qn"
    have "wf_tuple n V z" by (meson ‹z ∈ genericJoin V Q Qn› assms(1) assms(2) table_def wf_base_case)
    moreover have "⋀A X. (A, X) ∈ Q ⟹ restrict A z ∈ X"
    proof -
      fix A X assume "(A, X) ∈ Q"
      have "A = V"
      proof -
        have "card A ≥ 1"
          using ‹(A, X) ∈ Q› assms(2) non_empty_query_def rwf_query_def by fastforce
        moreover have "A ⊆ V"
          using ‹(A, X) ∈ Q› assms(2) included_def rwf_query_def by fastforce
        then show ?thesis
          by (metis One_nat_def assms(1) calculation card.infinite card_seteq nat.simps(3))
      qed
      then have "restrict A z = z" using calculation restrict_idle by blast
      moreover have "z ∈ (⋂(_, x) ∈ Q. x)"
        using ‹z ∈ genericJoin V Q Qn› assms(1) by auto
      then have "z ∈ X" using INT_D ‹(A, X) ∈ Q› case_prod_conv by auto
      then show "restrict A z ∈ X" using calculation by auto
    qed
    moreover have "⋀A X. (A, X) ∈ Qn ⟹ restrict A z ∉ X"
    proof -
      fix A X assume "(A, X) ∈ Qn"
      have "card A ≥ 1" using ‹(A, X) ∈ Qn› assms(2) non_empty_query_def rwf_query_def by fastforce
      moreover have "A ⊆ V" using ‹(A, X) ∈ Qn› assms(2) included_def rwf_query_def by blast
      then have "A = V" by (metis assms(1) calculation card_gt_0_iff card_seteq zero_less_one)
      then have "restrict A z = z"  using ‹wf_tuple n V z› restrict_idle by blast
      moreover have "z ∉ (⋃(_, x) ∈ Qn. x)"
      proof -
        have "z ∈ (⋂(_, x) ∈ Q. x) - (⋃(_, x) ∈ Qn. x)"
          using ‹z ∈ genericJoin V Q Qn› assms(1) by auto
        then show ?thesis by (metis DiffD2)
      qed
      then show "restrict A z ∉ X" using UN_iff ‹(A, X) ∈ Qn› calculation(2) prod.sel(2) snd_def by auto
    qed
    then show "wf_tuple n V z ∧ (∀(A, X)∈Q. restrict A z ∈ X) ∧ (∀(A, X)∈Qn. restrict A z ∉ X)"
      using calculation(1) calculation(2) by blast
  qed
  moreover have "wf_tuple n V z ∧ (∀(A, X)∈Q. restrict A z ∈ X) ∧ (∀(A, X)∈Qn. restrict A z ∉ X) ⟹ z ∈ genericJoin V Q Qn"
  proof -
    assume "wf_tuple n V z ∧ (∀(A, X)∈Q. restrict A z ∈ X) ∧ (∀(A, X)∈Qn. restrict A z ∉ X)"
    have "genericJoin V Q Qn = (⋂(_, x) ∈ Q. x) - (⋃(_, x) ∈ Qn. x)" by (simp add: assms(1))
    moreover have "∀(A, X)∈Q. restrict A z = z"
      by (metis (mono_tags, lifting) One_nat_def ‹wf_tuple n V z ∧ (∀(A, X)∈Q. restrict A z ∈ X) ∧ (∀(A, X)∈Qn. restrict A z ∉ X)›
          assms(1) assms(2) card.infinite card_seteq case_prod_beta' included_def nat.simps(3)
          non_empty_query_def restrict_idle rwf_query_def)
    moreover have "card Q ≥ 1" using assms(2) rwf_query_def wf_query_def by blast
    moreover have "z ∉ (⋃(_, x) ∈ Qn. x)"
    proof -
      have "∀(_, x) ∈ Qn. z ∉ x"
        by (metis (mono_tags, lifting) One_nat_def ‹wf_tuple n V z ∧ (∀(A, X)∈Q. restrict A z ∈ X) ∧ (∀(A, X)∈Qn. restrict A z ∉ X)›
            assms(1) assms(2) card.infinite card_seteq case_prod_beta' included_def nat.simps(3)
            non_empty_query_def restrict_idle rwf_query_def)
      then show ?thesis using UN_iff case_prod_beta' by auto
    qed
    moreover have "z ∈ (⋂(_, x) ∈ Q. x)"
    proof -
      have "∀(_, x) ∈ Q. z ∈ x"
        using ‹wf_tuple n V z ∧ (∀(A, X)∈Q. restrict A z ∈ X) ∧ (∀(A, X)∈Qn. restrict A z ∉ X)› calculation(2) by fastforce
      then show ?thesis using INT_I case_prod_beta' by auto
    qed
    ultimately show ?thesis
    proof -
      have "genericJoin V Q Qn ⊆ R"
        using assms(3) by blast
      then have "(⋂(N, Z)∈Q. Z) - (⋃(N, Z)∈Qn. Z) ⊆ R"
        by (metis ‹genericJoin V Q Qn = (⋂(_, x)∈Q. x) - (⋃(_, x)∈Qn. x)›)
      then have "∃Z Za. Z - Za ⊆ R ∧ z ∉ Za ∧ z ∈ Z"
        by (metis ‹z ∈ (⋂(_, x)∈Q. x)› ‹z ∉ (⋃(_, x)∈Qn. x)›)
      then show ?thesis
        using assms(3) by blast
    qed
  qed
  then show ?thesis using calculation by linarith
qed

lemma simple_list_index_equality:
  assumes "length a = n"
  assumes "length b = n"
  assumes "∀i < n. a!i = b!i"
  shows "a = b"
  using assms(1) assms(2) assms(3) nth_equalityI by force

lemma simple_restrict_none:
  assumes "i < length X"
  assumes "i ∉ A"
  shows "(restrict A X)!i = None"
  by (simp add: assms(1) assms(2) restrict_def)

lemma simple_restrict_some:
  assumes "i < length X"
  assumes "i ∈ A"
  shows "(restrict A X)!i = X!i"
  by (simp add: assms(1) assms(2) restrict_def)

lemma merge_restrict:
  assumes "A ∩ J = {}"
  assumes "A ⊆ I"
  assumes "length xx = n"
  assumes "length t = n"
  assumes "restrict J xx = xx"
  shows "restrict A (merge xx t) = restrict A t"
proof -
  have "⋀i. i < n ⟹ (restrict A (merge xx t))!i = (restrict A t)!i"
  proof -
    fix i assume "i < n"
    show "(restrict A (merge xx t))!i = (restrict A t)!i"
    proof (cases "i ∈ A")
      case True
      have "(restrict A t)!i = t!i" by (simp add: True ‹i < n› assms(4) nth_restrict)
      moreover have "(restrict A (merge xx t))!i = t!i"
      proof -
        have "xx!i = None"
          by (metis True ‹i < n› assms(1) assms(3) assms(5) disjoint_iff_not_equal simple_restrict_none)
        obtain "length xx = length t" by (simp add: assms(3) assms(4))
        moreover have "(merge xx t)!i = merge_option (xx!i, t!i)"
          using ‹i < n› ‹length xx = length t› assms(3) by auto
        moreover have "merge_option (None, t!i) = t!i" 
          by (metis merge_option.simps(1) merge_option.simps(3) option.exhaust)
        then have "(merge xx t)!i = t!i" using ‹xx ! i = None› calculation(2) by auto
        moreover have "(restrict A (merge xx t))!i = (merge xx t)!i"
        proof -
          have "length (zip xx t) = n" using assms(3) calculation(1) by auto
          then have "length (merge xx t) = n" by simp
          then show ?thesis by (simp add: True ‹i < n› nth_restrict)
        qed
        then show ?thesis using calculation(3) by auto
      qed
      then show ?thesis by (simp add: calculation)
    next
      case False
      have "(restrict A t)!i = None" by (simp add: False ‹i < n› assms(4) restrict_def)
      obtain "length xx = n" and "length t = n"
        by (simp add: assms(3) assms(4))
      then have "length (merge xx t) = n" by simp
      moreover have "(restrict A (merge xx t))!i = None"
        using False ‹i < n› calculation simple_restrict_none by blast
      then show ?thesis by (simp add: ‹restrict A t ! i = None›)
    qed
  qed
  then have "∀i < n. (restrict A (merge xx t))!i = (restrict A t)!i" by blast
  then show ?thesis using simple_list_index_equality[where ?a="restrict A (merge xx t)" and ?b="restrict A t" and ?n="n"]
      assms(3) assms(4) by simp
qed

lemma restrict_idle_include:
  assumes "wf_tuple n A v"
  assumes "A ⊆ I"
  shows "restrict I v = v"
proof -
  have "⋀i. i < length v ⟹ (restrict I v)!i = v!i"
  proof -
    fix i assume "i < length v"
    show "(restrict I v)!i = v!i"
    proof (cases "i ∈ A")
      case True
      then show ?thesis using ‹i < length v› assms(2) nth_restrict by blast
    next
      case False
      then show ?thesis by (metis ‹i < length v› assms(1) nth_restrict simple_restrict_none wf_tuple_def)
    qed
  qed
  then show ?thesis by (simp add: list_eq_iff_nth_eq)
qed

lemma merge_index:
  assumes "I ∩ J = {}"
  assumes "wf_tuple n I tI"
  assumes "wf_tuple n J tJ"
  assumes "t = merge tI tJ"
  assumes "i < n"
  shows "(i ∈ I ∧ t!i = tI!i) ∨ (i ∈ J ∧ t!i = tJ!i) ∨ (i ∉ I ∧ i ∉ J ∧ t!i = None)"
proof -
  have "t!i = merge_option ((zip tI tJ)!i)"
    by (metis (full_types) assms(2) assms(3) assms(4) assms(5) length_zip merge.simps
        min_less_iff_conj nth_map wf_tuple_def)
  then have "t!i = merge_option (tI!i, tJ!i)" by (metis assms(2) assms(3) assms(5) nth_zip wf_tuple_def)
  then show ?thesis
  proof (cases "i ∈ I")
    case True
    have "t!i = tI!i"
    proof -
      have "tJ!i = None" by (meson True assms(1) assms(3) assms(5) disjoint_iff_not_equal wf_tuple_def)
      moreover have "merge_option (tI!i, None) = tI!i"
        by (metis True assms(2) assms(5) merge_option.simps(2) option.exhaust wf_tuple_def)
      then show ?thesis by (simp add: ‹t ! i = merge_option (tI ! i, tJ ! i)› calculation)
    qed
    then show ?thesis using True by blast
  next
    case False
    have "i ∉ I" by (simp add: False)
    then show ?thesis
    proof (cases "i ∈ J")
      case True
      have "t!i = tJ!i"
      proof -
        have "tI!i = None" using False assms(2) assms(5) wf_tuple_def by blast
        moreover have "merge_option (None, tJ!i) = tJ!i"
          by (metis True assms(3) assms(5) merge_option.simps(3) option.exhaust wf_tuple_def)
        then show ?thesis by (simp add: ‹t ! i = merge_option (tI ! i, tJ ! i)› calculation)
      qed
      then show ?thesis using True by blast
    next
      case False
      obtain "tI!i = None" and "tJ!i = None " by (meson False ‹i ∉ I› assms(2) assms(3) assms(5) wf_tuple_def)
      have "t!i = None"
        by (simp add: ‹t ! i = merge_option (tI ! i, tJ ! i)› ‹tI ! i = None› ‹tJ ! i = None›)
      then show ?thesis using False ‹i ∉ I› by blast
    qed
  qed
qed

lemma restrict_index_in:
  assumes "i < length X"
  assumes "i ∈ I"
  shows "(restrict I X)!i = X!i"
  by (simp add: assms(1) assms(2) nth_restrict)

lemma restrict_index_out:
  assumes "i < length X"
  assumes "i ∉ I"
  shows "(restrict I X)!i = None"
  by (simp add: assms(1) assms(2) simple_restrict_none)

lemma merge_length:
  assumes "length a = n"
  assumes "length b = n"
  shows "length (merge a b) = n"
  by (simp add: assms(1) assms(2))

lemma real_restrict_merge:
  assumes "I ∩ J = {}"
  assumes "wf_tuple n I tI"
  assumes "wf_tuple n J tJ"
  shows "restrict I (merge tI tJ) = restrict I tI ∧ restrict J (merge tI tJ) = restrict J tJ"
proof -
  have "length (merge tI tJ) = n"
    using assms(2) assms(3) merge_length wf_tuple_def by blast
  have "⋀i. i < n ⟹ (restrict I (merge tI tJ))!i = (restrict I tI)!i
                     ∧ (restrict J (merge tI tJ))!i = (restrict J tJ)!i"
  proof -
    fix i assume "i < n"
    show "(restrict I (merge tI tJ))!i = (restrict I tI)!i ∧ (restrict J (merge tI tJ))!i = (restrict J tJ)!i"
    proof (cases "i ∈ I")
      case True
      have "(merge tI tJ)!i = tI!i"
        by (meson True ‹i < n› assms(1) assms(2) assms(3) disjoint_iff_not_equal merge_index)
      then have "(restrict I (merge tI tJ))!i = tI!i"
        by (metis True ‹i < n› ‹length (merge tI tJ) = n› simple_restrict_some)
      then show ?thesis
        by (metis True ‹i < n› ‹length (merge tI tJ) = n› assms(1) assms(2) assms(3) disjoint_iff_not_equal restrict_idle simple_restrict_none wf_tuple_def)
    next
      case False
      have "i ∉ I" by (simp add: False)
      then show ?thesis
      proof (cases "i ∈ J")
        case True
        have "(merge tI tJ)!i = tJ!i"
          using True ‹i < n› assms(1) assms(2) assms(3) merge_index by blast
        then show ?thesis
          by (metis (no_types, lifting) False ‹i < n› ‹length (merge tI tJ) = n› assms(2) assms(3) simple_restrict_none simple_restrict_some wf_tuple_def)
      next
        case False
        have "(merge tI tJ)!i = None" using False ‹i < n› ‹i ∉ I› assms(1) assms(2) assms(3) merge_index by blast
        then show ?thesis 
          by (metis False ‹i < n› ‹i ∉ I› ‹length (merge tI tJ) = n› assms(2) assms(3) eq_iff equalityD1 restrict_idle_include simple_restrict_none wf_tuple_def wf_tuple_restrict_simple)
      qed
    qed
  qed
  then obtain "∀i < n. (restrict I (merge tI tJ))!i = (restrict I tI)!i" 
          and "∀i < n. (restrict J (merge tI tJ))!i = (restrict J tJ)!i" by blast
  moreover have "length (merge tI tJ) = n" by (meson assms(2) assms(3) wf_merge wf_tuple_def)
  moreover obtain "length (restrict I tI) = n" and "length (restrict J tJ) = n"
    using assms(2) assms(3) wf_tuple_def by auto
  then show ?thesis
    by (metis ‹⋀i. i < n ⟹ restrict I (merge tI tJ) ! i = restrict I tI ! i ∧ restrict J (merge tI tJ) ! i = restrict J tJ ! i› calculation(3) length_restrict simple_list_index_equality)
qed

lemma simple_set_image_id:
  assumes "∀x∈X. f x = x"
  shows "Set.image f X = X"
proof -
  have "Set.image f X = {f x |x. x ∈ X}" by (simp add: Setcompr_eq_image)
  then have "... = {x |x. x ∈ X}" by (simp add: assms)
  moreover have "... = X" by simp
  then show ?thesis by (simp add: ‹f ` X = {f x |x. x ∈ X}› calculation)
qed

lemma nested_include_restrict:
  assumes "restrict I z = t"
  assumes "A ⊆ I"
  shows "restrict A z = restrict A t"
proof -
  have "length (restrict A z) = length (restrict A t)" using assms(1) by auto
  moreover have "⋀i. i < length (restrict A z) ⟹ (restrict A z) ! i = (restrict A t) ! i"
  proof -
    fix i assume "i < length (restrict A z)"
    then show "(restrict A z) ! i = (restrict A t) ! i"
    proof (cases "i ∈ A")
      case True
      then show ?thesis
        by (metis restrict_index_in ‹i < length (restrict A z)› assms(1) assms(2) length_restrict subsetD)
    next
      case False
      then show ?thesis
        by (metis simple_restrict_none ‹i < length (restrict A z)› calculation length_restrict)
    qed
  qed
  ultimately show ?thesis by (simp add: list_eq_iff_nth_eq)
qed

lemma restrict_nested:
  "restrict A (restrict B x) = restrict (A ∩ B) x" (is "?lhs = ?rhs")
proof -
  have "⋀i. i < length x ⟹ ?lhs!i = ?rhs!i"
    by (metis Int_iff length_restrict restrict_index_in simple_restrict_none)
  then show ?thesis by (simp add: simple_list_index_equality)
qed

lemma newQuery_equi_dev:
  "newQuery V Q (I, t) = Set.image (projectTable V) (Set.image (λtab. semiJoin tab (I, t)) Q)"
  by (metis newQuery_equiv_def projectQuery.elims)

lemma projectTable_idle:
  assumes "table n A X"
  assumes "A ⊆ I"
  shows "projectTable I (A, X) = (A, X)"
proof -
  have "projectTable I (A, X) = (A ∩ I, Set.image (restrict I) X)"
          using projectTable.simps by blast
  then have "A ∩ I = A" using assms(2) by blast
  have "⋀x. x ∈ X ⟹ (restrict I) x = x"
  proof -
    fix x assume "x ∈ X"
    have "wf_tuple n A x" using ‹x ∈ X› assms(1) table_def by blast
    then show "(restrict I) x = x" using assms(2) restrict_idle_include by blast
  qed
  then have "∀x ∈ X. (restrict I) x = x" by blast
  moreover have "Set.image (restrict I) X = X"
    by (simp add: ‹⋀x. x ∈ X ⟹ restrict I x = x›)
  then show ?thesis by (simp add: ‹A ∩ I = A›)
qed

lemma restrict_partition_merge:
  assumes "I ∪ J = V"
  assumes "wf_tuple n V z"
  assumes "xx = restrict J z"
  assumes "t = restrict I z"
  assumes "Set.is_empty (I ∩ J)"
  shows "z = merge xx t"
proof -
  have "⋀i. i < n ⟹ z!i = (merge xx t)!i"
  proof -
    fix i assume "i < n"
    show "z!i = (merge xx t)!i"
    proof (cases "i ∈ I")
      case True
      have "z!i = t!i"
        by (metis True ‹i < n› assms(2) assms(4) nth_restrict wf_tuple_def)
      moreover have "(merge xx t)!i = t!i"
      proof -
        have "xx ! i = None"
          by (metis simple_restrict_none Set.is_empty_def True ‹i < n› assms(2) assms(3) assms(5) disjoint_iff_not_equal wf_tuple_length)
        moreover have "(merge xx t) ! i = merge_option (xx ! i, t ! i)" using ‹i < n› assms(2) assms(3) assms(4) wf_tuple_length by fastforce
        ultimately show ?thesis
        proof (cases "t ! i")
          case None
          then show ?thesis using ‹merge xx t ! i = merge_option (xx ! i, t ! i)› ‹xx ! i = None› by auto
        next
          case (Some a)
          then show ?thesis using ‹merge xx t ! i = merge_option (xx ! i, t ! i)› ‹xx ! i = None› by auto
        qed
      qed
      then show ?thesis by (simp add: calculation)
    next
      case False
      have "i ∉ I" by (simp add: False)
      then show ?thesis
      proof (cases "i ∈ J")
        case True
        have "z!i = xx!i"
          by (metis True ‹i < n› assms(2) assms(3) nth_restrict wf_tuple_def)
        moreover have "(merge xx t)!i = xx!i"
        proof (cases "xx ! i")
          case None
          then show ?thesis  by (metis True UnI1 ‹i < n› assms(1) assms(2) calculation sup_commute wf_tuple_def)
        next
          case (Some a)
          have "t ! i = None" by (metis False simple_restrict_none ‹i < n› assms(2) assms(4) wf_tuple_length)
          then show ?thesis using Some ‹i < n› assms(2) assms(3) assms(4) wf_tuple_length by fastforce
        qed
        then show ?thesis by (simp add: calculation)
      next
        case False
        have "z!i = None" by (metis False UnE ‹i < n› ‹i ∉ I› assms(1) assms(2) wf_tuple_def)
        moreover have "(merge xx t)!i = None"
        proof -
          have "xx ! i = None"
            by (metis False New_max.simple_restrict_none ‹i < n› assms(2) assms(3) wf_tuple_length)
          moreover have "t ! i = None"
            by (metis New_max.simple_restrict_none ‹i < n› ‹i ∉ I› assms(2) assms(4) wf_tuple_length)
          ultimately show ?thesis using ‹i < n› assms(2) assms(3) assms(4) wf_tuple_length by fastforce
        qed
        then show ?thesis by (simp add: calculation)
      qed
    qed
  qed
  moreover have "length z = n" using assms(2) wf_tuple_def by blast
  then show ?thesis
    by (simp add: assms(3) assms(4) calculation simple_list_index_equality)
qed

lemma restrict_merge:
  assumes "zI = restrict I z"
  assumes "zJ = restrict J z"
  assumes "restrict (A ∩ I) zI ∈ Set.image (restrict I) X"
  assumes "restrict (A ∩ J) zJ ∈ Set.image (restrict J) (Set.filter (isSameIntersection zI (A ∩ I)) X)"
  assumes "z = merge zJ zI"
  assumes "table n A X"
  assumes "A ⊆ I ∪ J"
  assumes "card (A ∩ I) ≥ 1"
  assumes "wf_set n (I ∪ J)"
  assumes "wf_tuple n (I ∪ J) z"
  shows "restrict A z ∈ X"
proof -
  define zAJ where "zAJ = restrict (A ∩ J) zJ"
  obtain zz where "zAJ = restrict J zz" "isSameIntersection zI (A ∩ I) zz" "zz ∈ X"
    using assms(4) zAJ_def by auto
  then have "restrict (A ∩ I) zz = restrict A zI"
  proof -
    have "restrict (A ∩ I) zI = restrict (A ∩ I) zz"
    proof -
      have "wf_set n A" using assms(7) assms(9) wf_set_def by auto
      moreover have "wf_tuple n I zI" using assms(1) assms(10) wf_tuple_restrict_simple by auto
      moreover have "wf_tuple n A zz" using ‹zz ∈ X› assms(6) table_def by blast
      moreover obtain "A ∩ I ⊆ A" "A ∩ I ⊆ I" by simp
      then show ?thesis using isSame_equi_dev[of n _ I zI A zz "A ∩ I"]
        using ‹isSameIntersection zI (A ∩ I) zz› assms(7) assms(9) calculation(2) calculation(3) by blast
    qed
    then show ?thesis
      by (simp add: restrict_nested assms(1))
  qed
  then have "zz = restrict A z"
  proof -
    have "length zz = n" using ‹zz ∈ X› assms(6) table_def wf_tuple_def by blast
    moreover have "length (restrict A z) = n"
      by (metis ‹restrict (A ∩ I) zz = restrict A zI› assms(1) calculation length_restrict)
    moreover have "⋀i. i < n ⟹ zz!i = (restrict A z)!i"
    proof -
      fix i assume "i < n"
      show "zz!i = (restrict A z)!i"
      proof (cases "i ∈ A")
        case True
        have "i ∈ A" using True by simp
        then show ?thesis
        proof (cases "i ∈ I")
          case True
          have "zz!i = (restrict (A ∩ I) zz)!i"
            by (simp add: True ‹i < n› ‹i ∈ A› calculation(1) restrict_index_in)
          then have "... = (restrict A zI)!i" by (simp add: ‹restrict (A ∩ I) zz = restrict A zI›)
          then show ?thesis
            by (metis True ‹i < n› ‹i ∈ A› ‹zz ! i = restrict (A ∩ I) zz ! i› assms(1) calculation(2)
                length_restrict restrict_index_in)
        next
          case False
          have "zz!i = (restrict (A ∩ J) zJ)!i"
            by (metis False True UnE ‹i < n› ‹zAJ = restrict J zz› assms(7) calculation(1)
                restrict_index_in subsetD zAJ_def)
          then have "... = (restrict A zJ)!i" by (simp add: assms(2) restrict_nested)
          then show ?thesis
            by (metis False True UnE ‹i < n› ‹zz ! i = restrict (A ∩ J) zJ ! i› assms(2) assms(7)
                calculation(2) length_restrict restrict_index_in subsetD)
        qed
      next
        case False
        then show ?thesis
          by (metis ‹i < n› ‹zz ∈ X› assms(6) calculation(2) length_restrict simple_restrict_none table_def wf_tuple_def)
      qed
    qed
    then show ?thesis using calculation(1) calculation(2) simple_list_index_equality by blast
  qed
  then show ?thesis
    using ‹zz ∈ X› by auto
qed

lemma partial_correctness:
  assumes "V = I ∪ J"
  assumes "Set.is_empty (I ∩ J)"
  assumes "card I ≥ 1"
  assumes "card J ≥ 1"
  assumes "Q_I_pos = projectQuery I (filterQuery I Q)"
  assumes "Q_J_pos = filterQuery J Q"
  assumes "Q_I_neg = filterQueryNeg I Qn"
  assumes "Q_J_neg = filterQuery J (Qn - Q_I_neg)"
  assumes "NQ_pos = newQuery J Q_J_pos (I, t)"
  assumes "NQ_neg = newQuery J Q_J_neg (I, t)"
  assumes "R_NQ = genericJoin J NQ_pos NQ_neg"
  assumes "∀x. (x ∈ R_I ⟷ wf_tuple n I x ∧ (∀(A, X)∈Q_I_pos. restrict A x ∈ X) ∧ (∀(A, X)∈Q_I_neg. restrict A x ∉ X))"
  assumes "∀y. (y ∈ R_NQ ⟷ wf_tuple n J y ∧ (∀(A, X)∈NQ_pos. restrict A y ∈ X) ∧ (∀(A, X)∈NQ_neg. restrict A y ∉ X))"
  assumes "z = merge xx t"
  assumes "t ∈ R_I"
  assumes "xx ∈ R_NQ"
  assumes "rwf_query n V Q Qn"
  shows "wf_tuple n V z ∧ (∀(A, X)∈Q. restrict A z ∈ X) ∧ (∀(A, X)∈Qn. restrict A z ∉ X)"
proof -
  obtain "wf_tuple n I t" "wf_tuple n J xx"
    using assms(12) assms(13) assms(15) assms(16) by blast
  then have "wf_tuple n V z"
    by (metis wf_merge assms(1) assms(14) sup_commute)
  moreover have "⋀A X. (A, X) ∈ Qn ⟹ restrict A z ∉ X"
  proof -
    fix A X assume "(A, X) ∈ Qn"
    have "restrict I (merge xx t) = restrict I t"
      by (metis (no_types, lifting) Set.is_empty_def ‹⋀thesis. (⟦wf_tuple n I t; wf_tuple n J xx⟧ ⟹ thesis) ⟹ thesis›
          assms(2) merge_restrict restrict_idle sup.cobounded1 wf_tuple_def)
    moreover have "restrict J (merge xx t) = restrict J xx"
      by (metis Set.is_empty_def ‹⋀thesis. (⟦wf_tuple n I t; wf_tuple n J xx⟧ ⟹ thesis) ⟹ thesis›
          assms(2) inf_commute real_restrict_merge)
    moreover have "restrict J xx = xx" using ‹wf_tuple n J xx› restrict_idle by auto
    moreover have "restrict I t = t" using ‹wf_tuple n I t› restrict_idle by auto
    then obtain "restrict I z = t" "restrict J z = xx"
      using assms(14) calculation(1) calculation(2) calculation(3) by auto
    moreover have "∀(A, X)∈Q_I_pos. restrict A t ∈ X" using assms(12) assms(15) by blast
    moreover have "∀(A, X)∈NQ_pos. restrict A xx ∈ X" using assms(13) assms(16) by blast
    moreover have "card A ≥ 1"
      using ‹(A, X) ∈ Qn› assms(17) non_empty_query_def rwf_query_def by fastforce
    then show "restrict A z ∉ X"
    proof (cases "A ⊆ I")
      case True
      have "(A, X) ∈ Q_I_neg" by (simp add: True ‹(A, X) ∈ Qn› assms(7))
      have "table n A X"
      proof -
        have "wf_query n V Q Qn" using assms(17) rwf_query_def by blast
        moreover have "(A, X) ∈ (Q ∪ Qn)" by (simp add: ‹(A, X) ∈ Qn›)
        then show ?thesis by (metis calculation fst_conv snd_conv wf_atable_def wf_query_def)
      qed
      then have "restrict A t ∉ X" using ‹(A, X) ∈ Q_I_neg› assms(12) assms(15) by blast
      moreover have "restrict A z = restrict A t" using True ‹restrict I z = t› nested_include_restrict by blast
      then show ?thesis by (simp add: calculation)
    next
      case False
      have "(A, X) ∈ Q_J_neg"
      proof -
        have "(A, X) ∈ Qn - Q_I_neg" using False ‹(A, X) ∈ Qn› assms(7) by auto
        moreover have "card (A ∩ J) ≥ 1"
          by (metis (no_types, lifting) False Int_greatest One_nat_def Set.is_empty_def Suc_leI
              Suc_le_lessD ‹(A, X) ∈ Qn› assms(1) assms(17) assms(2) assms(4) card_gt_0_iff case_prodD
              finite_Int included_def rwf_query_def sup_ge2 sup_inf_absorb sup_inf_distrib1)
        then show ?thesis using assms(8) calculation
          by (metis Diff_subset subset_Q_neg assms(17) fst_conv rwf_query_def set_filterQuery)
      qed
      define AI where "AI = A ∩ I"
      define AJ where "AJ = A ∩ J"
      then have "NQ_neg = projectQuery J (Set.image (λtab. semiJoin tab (I, t)) Q_J_neg)"
        by (metis newQuery_equi_dev projectQuery.simps assms(10))
      then obtain XX where "(A, XX) = (λtab. semiJoin tab (I, t)) (A, X)" by simp
      then obtain XXX where "(AJ, XXX) ∈ NQ_neg" and "(AJ, XXX) = projectTable J (A, XX)"
        by (metis AJ_def newQuery.simps projectTable.simps ‹(A, X) ∈ Q_J_neg› assms(10) image_eqI)
      then have "restrict AJ xx ∉ XXX"
      proof -
        have "xx ∈ R_NQ" by (simp add: assms(16))
        then have "wf_tuple n J xx ∧ (∀(A, X)∈NQ_pos. restrict A xx ∈ X) ∧ (∀(A, X)∈NQ_neg. restrict A xx ∉ X)"
          by (simp add: assms(13))
        then show ?thesis using ‹(AJ, XXX) ∈ NQ_neg› by blast
      qed

      define zA where "zA = restrict A z"
      have "zA ∉ X"
      proof (rule ccontr)
        assume "¬ (zA ∉ X)"
        then have "zA ∈ X" by simp
        moreover have "restrict (A ∩ I) zA = restrict (A ∩ I) t"
          by (metis nested_include_restrict ‹restrict I z = t› inf_le1 inf_le2 zA_def)
        then have "isSameIntersection t (A ∩ I) zA"
        proof -
          have "wf_set n V" using assms(17) rwf_query_def wf_query_def by blast
          moreover obtain "A ∩ I ⊆ A" "A ∩ I ⊆ I" "I ⊆ V" using assms(1) by blast
          moreover have "A ⊆ V" using ‹(A, X) ∈ Qn› assms(17) included_def rwf_query_def by fastforce
          moreover have "wf_tuple n A zA"
            using ‹wf_tuple n V z› calculation(5) wf_tuple_restrict_simple zA_def by blast
          then show ?thesis using isSame_equi_dev[of n V A zA I t "A ∩ I"]
            by (simp add: ‹restrict (A ∩ I) zA = restrict (A ∩ I) t› ‹wf_tuple n I t› calculation(1) calculation(4) calculation(5))
        qed
        then have "zA ∈ XX" using ‹(A, XX) = semiJoin (A, X) (I, t)› calculation by auto
        then have "restrict J zA ∈ XXX" using ‹(AJ, XXX) = projectTable J (A, XX)› by auto
        moreover have "restrict AJ xx = restrict J zA"
          by (metis AJ_def restrict_nested ‹restrict J z = xx› inf.right_idem inf_commute zA_def)
        then show "False" using ‹restrict AJ xx ∉ XXX› calculation(2) by auto
      qed
      then show ?thesis using zA_def by auto
    qed
  qed
  moreover have "⋀A X. (A, X) ∈ Q ⟹ restrict A z ∈ X"
  proof -
    fix A X assume "(A, X) ∈ Q"
    have "restrict I (merge xx t) = restrict I t"
      by (metis (no_types, lifting) Set.is_empty_def ‹⋀thesis. (⟦wf_tuple n I t; wf_tuple n J xx⟧ ⟹ thesis) ⟹ thesis›
          assms(2) merge_restrict restrict_idle sup.cobounded1 wf_tuple_def)
    moreover have "restrict J (merge xx t) = restrict J xx"
      by (metis Set.is_empty_def ‹⋀thesis. (⟦wf_tuple n I t; wf_tuple n J xx⟧ ⟹ thesis) ⟹ thesis›
          assms(2) inf_commute real_restrict_merge)
    moreover have "restrict J xx = xx" using ‹wf_tuple n J xx› restrict_idle by auto
    moreover have "restrict I t = t" using ‹wf_tuple n I t› restrict_idle by auto
    then obtain "restrict I z = t" "restrict J z = xx"
      using assms(14) calculation(1) calculation(2) calculation(3) by auto
    moreover have "∀(A, X)∈Q_I_pos. restrict A t ∈ X" using assms(12) assms(15) by blast
    moreover have "∀(A, X)∈NQ_pos. restrict A xx ∈ X" using assms(13) assms(16) by blast
    moreover have "card A ≥ 1"
      using ‹(A, X) ∈ Q› assms(17) non_empty_query_def rwf_query_def by fastforce
    then show "restrict A z ∈ X"
    proof (cases "A ⊆ I")
      case True
      have "(A, X) ∈ filterQuery I Q"
      proof -
        have "A ∩ I = A" using True by auto
        then have "A ∩ I ≠ {}" using ‹1 ≤ card A› by auto
        then have "(λ(s, _). s ∩ V ≠ {}) (A, X)" using assms(1) by blast
        then show ?thesis
          by (metis ‹(A, X) ∈ Q› ‹1 ≤ card A› ‹A ∩ I = A› assms(17) fst_conv rwf_query_def set_filterQuery)          
      qed
      have "table n A X"
      proof -
        have "wf_query n V Q Qn" using assms(17) rwf_query_def by blast
        moreover have "(A, X) ∈ (Q ∪ Qn)" by (simp add: ‹(A, X) ∈ Q›)
        then show ?thesis by (metis calculation fst_conv snd_conv wf_atable_def wf_query_def)
      qed
      moreover have "projectTable I (A, X) = (A, X)" using True calculation projectTable_idle by blast
      then have "(A, X) ∈ Q_I_pos" by (metis ‹(A, X) ∈ filterQuery I Q› assms(5) image_eqI projectQuery.elims)
      then have "restrict A t ∈ X" using ‹∀(A, X)∈Q_I_pos. restrict A t ∈ X› by blast
      moreover have "restrict A z = restrict A t" using True ‹restrict I z = t› nested_include_restrict by blast
      then show ?thesis by (simp add: calculation(2))
    next
      case False
      have "A ⊆ V"
      proof -
        have "included V Q" using assms(17) rwf_query_def by blast
        then show ?thesis using ‹(A, X) ∈ Q› included_def by fastforce
      qed
      then have "card (A ∩ J) ≥ 1" by (metis False One_nat_def Suc_leI Suc_le_lessD UnE assms(1) 
            assms(4) card_gt_0_iff disjoint_iff_not_equal finite_Int subsetD subsetI)
      then show ?thesis
      proof (cases "card (A ∩ I) ≥ 1")
        case True
        define zI where "zI = restrict I z"
        define zJ where "zJ = restrict J z"
        obtain "zI = t" "zJ = xx"
          by (simp add: calculation(4) calculation(5) zI_def zJ_def)
        then have "wf_tuple n I zI ∧ (∀(A, X)∈Q_I_pos. restrict A zI ∈ X)"
          using ‹wf_tuple n I t› calculation(6) by blast
        moreover have "wf_tuple n J zJ ∧ (∀(A, X)∈NQ_pos. restrict A zJ ∈ X)"
          using ‹∀(A, X)∈NQ_pos. restrict A xx ∈ X› ‹wf_tuple n J xx› ‹zJ = xx› by blast
        obtain "(A, X) ∈ (filterQuery I Q)" "(A, X) ∈ Q_J_pos"
          using True ‹(A, X) ∈ Q› ‹1 ≤ card (A ∩ J)› assms(6) assms(17) rwf_query_def set_filterQuery by fastforce
        define AI where "AI = A∩I"
        define XI where "XI = Set.image (restrict I) X"
        then have "(AI, XI) = projectTable I (A, X)" using AI_def XI_def by simp
        then have "(AI, XI) ∈ Q_I_pos" by (metis ‹(A, X) ∈ filterQuery I Q› assms(5) image_eqI projectQuery.elims)
        then have "restrict AI zI ∈ XI" using ‹wf_tuple n I zI ∧ (∀(A, X)∈Q_I_pos. restrict A zI ∈ X)› by blast
        obtain AJ XJ where "(AJ, XJ) = projectTable J (semiJoin (A, X) (I, zI))" by simp
        then have "AJ = A ∩ J" by auto
        then have "(AJ, XJ) ∈ NQ_pos"
          using ‹(A, X) ∈ Q_J_pos› ‹(AJ, XJ) = projectTable J (semiJoin (A, X) (I, zI))› ‹zI = t› image_iff
          using assms(9) by fastforce
        then have "restrict AJ zJ ∈ XJ"
          using ‹wf_tuple n J zJ ∧ (∀(A, X)∈NQ_pos. restrict A zJ ∈ X)› by blast
        have "XJ = Set.image (restrict J) (Set.filter (isSameIntersection zI (A ∩ I)) X)"
          using ‹(AJ, XJ) = projectTable J (semiJoin (A, X) (I, zI))› by auto
        then have "restrict AJ zJ ∈ Set.image (restrict J) (Set.filter (isSameIntersection zI (A ∩ I)) X)"
          using ‹restrict AJ zJ ∈ XJ› by blast
        moreover have "table n A X"
          using ‹(A, X) ∈ Q› assms(17) rwf_query_def wf_atable_def wf_query_def by fastforce
        moreover have "A ⊆ I ∪ J" using ‹A ⊆ V› assms(1) by auto
        then show ?thesis using restrict_merge[of zI I z zJ J A X n] AI_def True XI_def ‹AJ = A ∩ J›
            ‹restrict AI zI ∈ XI› ‹restrict I z = t› ‹restrict J z = xx› ‹wf_tuple n V z› assms(1)
            assms(14) assms(17) calculation(2) calculation(3) rwf_query_def wf_query_def zI_def zJ_def by blast
      next
        case False
        have "(A, X) ∈ Q_J_pos" using ‹(A, X) ∈ Q› ‹1 ≤ card (A ∩ J)› assms(6) assms(17)
            rwf_query_def set_filterQuery by fastforce
        moreover have "A ⊆ J"
          by (metis False One_nat_def Set.is_empty_def Suc_leI Suc_le_lessD ‹1 ≤ card A› ‹A ⊆ V›
              assms(1) assms(2) card_gt_0_iff finite_Int inf.absorb_iff2 inf_commute sup_commute sup_inf_absorb sup_inf_distrib1)
        then have "restrict A z = restrict A xx" using ‹restrict J z = xx› nested_include_restrict by blast
        define zI where "zI = restrict I z"
        define zJ where "zJ = restrict J z"
        have "zJ = xx" by (simp add: ‹restrict J z = xx› zJ_def)
        have "zI = t" by (simp add: ‹restrict I z = t› zI_def)
        have "z = merge zJ zI" by (simp add: ‹zI = t› ‹zJ = xx› assms(14))
        obtain AA XX where "(AA, XX) = projectTable J (semiJoin (A, X) (I, t))" by simp
        have "AA = A ∩ J"
          using ‹(AA, XX) = projectTable J (semiJoin (A, X) (I, t))› by auto
        have "(AA, XX) ∈ NQ_pos"
          using ‹(AA, XX) = projectTable J (semiJoin (A, X) (I, t))› calculation image_iff assms(9)
            by fastforce
        then have "restrict AA zJ ∈ XX"
          using ‹(AA, XX) ∈ NQ_pos› ‹∀(A, X)∈NQ_pos. restrict A xx ∈ X› ‹zJ = xx› by blast
        then have "restrict A z = restrict A zJ" by (simp add: ‹restrict A z = restrict A xx› ‹zJ = xx›)
        moreover have "restrict AA zJ = restrict A zJ" by (simp add: ‹A ⊆ J› ‹AA = A ∩ J› inf.absorb1)
        then have "restrict A z ∈ XX" using ‹restrict AA zJ ∈ XX› calculation(2) by auto
        moreover have "XX ⊆ Set.image (restrict J) X"
        proof -
          obtain AAA XXX where "(AAA, XXX) = semiJoin (A, X) (I, t)" by simp
          then have "XXX ⊆ X" by auto
          then have "XX = Set.image (restrict J) XXX"
            using ‹(AA, XX) = projectTable J (semiJoin (A, X) (I, t))› ‹(AAA, XXX) = semiJoin (A, X) (I, t)› by auto
          then show ?thesis by (simp add: ‹XXX ⊆ X› image_mono)
        qed
        then have "restrict A z ∈ Set.image (restrict J) X" using calculation(3) by blast
        obtain zz where "restrict A z = restrict J zz" "zz ∈ X"
          using ‹restrict A z ∈ restrict J ` X› by blast
        then have "restrict A z = restrict A zz"
          by (metis Int_absorb2 ‹A ⊆ J› restrict_nested subset_refl)
        moreover have "restrict A zz = zz"
        proof -
          have "(A, X) ∈ Q" by (simp add: ‹(A, X) ∈ Q›)
          then have "table n A X" using assms(17) rwf_query_def wf_atable_def wf_query_def by fastforce
          then have "wf_tuple n A zz" using ‹zz ∈ X› table_def by blast
          then show ?thesis using restrict_idle by blast
        qed
        then have "restrict A zz = zz" using ‹restrict A z = restrict J zz› calculation(4) by auto
        then show ?thesis by (simp add: ‹zz ∈ X› calculation(4))
      qed
    qed
  qed
  then show ?thesis using calculation by blast
qed

lemma simple_set_inter:
  assumes "I ⊆ (⋃X∈A. f X)"
  shows "I ⊆ (⋃X∈A. (f X) ∩ I)"
proof -
  have "⋀x. x ∈ I ⟹ x ∈ (⋃X∈A. (f X) ∩ I)"
  proof -
    fix x assume "x ∈ I"
    obtain X where "X ∈ A" "x ∈ f X" using ‹x ∈ I› assms by auto
    then show "x ∈ (⋃X∈A. (f X) ∩ I)" using ‹x ∈ I› by blast
  qed
  then show ?thesis by (simp add: subsetI)
qed

lemma union_restrict:
  assumes "restrict I z1 = restrict I z2"
  assumes "restrict J z1 = restrict J z2"
  shows "restrict (I ∪ J) z1 = restrict (I ∪ J) z2"
proof -
  define zz1 where "zz1 = restrict (I ∪ J) z1"
  define zz2 where "zz2 = restrict (I ∪ J) z2"
  have "length z1 = length z2" by (metis assms(2) length_restrict)
  have "⋀i. i < length z1 ⟹ zz1!i = zz2!i"
  proof -
    fix i assume "i < length z1"
    then show "zz1!i = zz2!i"
    proof (cases "i ∈ I")
      case True
      then show ?thesis
        by (metis simple_restrict_none ‹i < length z1› ‹length z1 = length z2› assms(1)
            nth_restrict zz1_def zz2_def)
    next
      case False
      then show ?thesis
        by (metis simple_restrict_none UnE ‹i < length z1› ‹length z1 = length z2› assms(2)
            nth_restrict zz1_def zz2_def)
    qed
  qed
  then have "∀i < length z1. (restrict (I ∪ J) z1)!i = (restrict (I ∪ J) z2)!i"
    using zz1_def zz2_def by blast
  then show ?thesis
    by (simp add: simple_list_index_equality ‹length z1 = length z2›)
qed

lemma partial_correctness_direct:
  assumes "V = I ∪ J"
  assumes "Set.is_empty (I ∩ J)"
  assumes "card I ≥ 1"
  assumes "card J ≥ 1"
  assumes "Q_I_pos = projectQuery I (filterQuery I Q)"
  assumes "Q_J_pos = filterQuery J Q"
  assumes "Q_I_neg = filterQueryNeg I Qn"
  assumes "Q_J_neg = filterQuery J (Qn - Q_I_neg)"
  assumes "R_I = genericJoin I Q_I_pos Q_I_neg"
  assumes "X = {(t, genericJoin J (newQuery J Q_J_pos (I, t)) (newQuery J Q_J_neg (I, t))) | t . t ∈ R_I}"
  assumes "R = (⋃(t, x) ∈ X. {merge xx t | xx . xx ∈ x})"
  assumes "R_NQ = genericJoin J NQ_pos NQ_neg"
  assumes "∀x. (x ∈ R_I ⟷ wf_tuple n I x ∧ (∀(A, X)∈Q_I_pos. restrict A x ∈ X) ∧ (∀(A, X)∈Q_I_neg. restrict A x ∉ X))"
  assumes "∀t∈R_I. (∀y. (y ∈ genericJoin J (newQuery J Q_J_pos (I, t)) (newQuery J Q_J_neg (I, t)) ⟷ wf_tuple n J y ∧
  (∀(A, X)∈(newQuery J Q_J_pos (I, t)). restrict A y ∈ X) ∧ (∀(A, X)∈(newQuery J Q_J_neg (I, t)). restrict A y ∉ X)))"
  assumes "wf_tuple n V z ∧ (∀(A, X)∈Q. restrict A z ∈ X) ∧ (∀(A, X)∈Qn. restrict A z ∉ X)"
  assumes "rwf_query n V Q Qn"
  shows "z ∈ R"
proof -
  define CI where "CI = filterQuery I Q"
  define zI where "zI = restrict I z"
  have "wf_tuple n I zI"
    using assms(1) assms(15) wf_tuple_restrict_simple zI_def by auto
  have "⋀A X. ((A, X)∈Q_I_pos ⟹ restrict A zI ∈ X)"
  proof -
    fix A X assume "(A, X)∈Q_I_pos"
    have "(A, X) ∈ projectQuery I Q" using ‹(A, X) ∈ Q_I_pos› assms(5) by auto
    then obtain AA XX where "X = Set.image (restrict I) XX" "(AA, XX) ∈ Q" "A = AA ∩ I" by auto
    moreover have "(restrict AA z) ∈ XX" using assms(15) calculation(2) by blast
    then have "restrict I (restrict AA z) ∈ X" by (simp add: calculation(1))
    then show "restrict A zI ∈ X"
      by (metis calculation(3) inf.right_idem inf_commute restrict_nested zI_def)
  qed
  moreover have "⋀A X. ((A, X)∈Q_I_neg ⟹ restrict A zI ∉ X)"
  proof -
    fix A X assume "(A, X)∈Q_I_neg"
    then have "(A, X) ∈ Qn" by (simp add: assms(7))
    then have "restrict A z ∉ X" using assms(15) by blast
    moreover have "A ⊆ I" using ‹(A, X) ∈ Q_I_neg› assms(7) by auto
    then have "restrict A z = restrict A zI"
      using nested_include_restrict zI_def by metis
    then show "restrict A zI ∉ X" using calculation by auto
  qed
  then have "zI ∈ R_I" using ‹wf_tuple n I zI› assms(13) calculation by auto
  define zJ where "zJ = restrict J z"
  have "wf_tuple n J zJ" using assms(1) assms(15) wf_tuple_restrict_simple zJ_def by auto
  have "⋀A X. ((A, X)∈Q_J_pos ⟹ restrict A z ∈ X)" using assms(15) assms(6) by auto
  define NQ where "NQ = newQuery J Q_J_pos (I, zI)"
  have "⋀A X. ((A, X)∈Q_J_pos ⟹ (isSameIntersection zI (A ∩ I) (restrict A z)))"
  proof -
    fix A X assume "(A, X) ∈ Q_J_pos"
    obtain "wf_set n V" "wf_tuple n I zI" using ‹wf_tuple n I zI› assms(16) rwf_query_def wf_query_def by blast
    moreover have "A ⊆ V"
    proof -
      have "included V Q_J_pos"
        by (metis filterQuery.elims assms(16) assms(6) included_def member_filter rwf_query_def)
      then show ?thesis using ‹(A, X) ∈ Q_J_pos› included_def by fastforce
    qed
    moreover have "wf_tuple n A (restrict A z)" by (meson assms(15) calculation(3) wf_tuple_restrict_simple)
    then show "isSameIntersection zI (A ∩ I) (restrict A z)"
      using isSame_equi_dev[of n V I zI A "restrict A z" "A ∩ I"]
      by (metis nested_include_restrict assms(1) calculation(1) calculation(2) calculation(3) inf_le1 inf_le2 sup_ge1 zI_def)
  qed
  then have "⋀A X. ((A, X)∈NQ ⟹ restrict A zJ ∈ X)"
  proof -
    fix A X assume "(A, X)∈NQ"
    obtain AA XX where "(A, X) = projectTable J (semiJoin (AA, XX) (I, zI))" "(AA, XX) ∈ Q_J_pos"
      using NQ_def ‹(A, X) ∈ NQ› by auto
    then have "restrict AA z ∈ XX" using ‹⋀X A. (A, X) ∈ Q_J_pos ⟹ restrict A z ∈ X› by blast
    then have "restrict AA z ∈ snd (semiJoin (AA, XX) (I, zI))"
      using ‹(AA, XX) ∈ Q_J_pos› ‹⋀X A. (A, X) ∈ Q_J_pos ⟹ isSameIntersection zI (A ∩ I) (restrict A z)› by auto
    then have "restrict J (restrict AA z) ∈ X"
      using ‹(A, X) = projectTable J (semiJoin (AA, XX) (I, zI))› by auto
    then show "restrict A zJ ∈ X"
      by (metis ‹(A, X) = projectTable J (semiJoin (AA, XX) (I, zI))› fst_conv inf.idem inf_commute
          projectTable.simps restrict_nested semiJoin.simps zJ_def)
  qed
  moreover have "∀y. (y ∈ genericJoin J (newQuery J Q_J_pos (I, zI)) (newQuery J Q_J_neg (I, zI)) ⟷ wf_tuple n J y ∧
  (∀(A, X)∈newQuery J Q_J_pos (I, zI). restrict A y ∈ X) ∧ (∀(A, X)∈newQuery J Q_J_neg (I, zI). restrict A y ∉ X))"
    using ‹zI ∈ R_I› assms(14) by auto
  then have "zJ ∈ genericJoin J (newQuery J Q_J_pos (I, zI)) (newQuery J Q_J_neg (I, zI))
                     ⟷ wf_tuple n J zJ ∧ (∀(A, X)∈newQuery J Q_J_pos (I, zI). restrict A zJ ∈ X) ∧
  (∀(A, X)∈newQuery J Q_J_neg (I, zI). restrict A zJ ∉ X)" by blast
  moreover have "∀(A, X)∈newQuery J Q_J_pos (I, zI). restrict A zJ ∈ X"
    using NQ_def calculation(2) by blast
  moreover have "⋀A X. (A, X)∈newQuery J Q_J_neg (I, zI) ⟹ restrict A zJ ∉ X"
  proof -
    fix A X assume "(A, X) ∈ newQuery J Q_J_neg (I, zI)"
    then have "(A, X) ∈ (Set.image (λtab. projectTable J (semiJoin tab (I, zI))) Q_J_neg)"
      using newQuery.simps by blast
    then obtain AA XX where "(A, X) = projectTable J (semiJoin (AA, XX) (I, zI))" and "(AA, XX) ∈ Q_J_neg"
      by auto
    then have "A = AA ∩ J" by auto
    then have "(AA, XX) ∈ Qn" using ‹(AA, XX) ∈ Q_J_neg› assms(8) by auto
    then have "restrict AA z ∉ XX" using assms(15) by blast
    show "restrict A zJ ∉ X"
    proof (rule ccontr)
      assume "¬ (restrict A zJ ∉ X)"
      then have "restrict A zJ ∈ X" by simp
      then have "restrict A zJ ∈ Set.image (restrict J) (Set.filter (isSameIntersection zI (I ∩ AA)) XX)"
        by (metis projectTable.simps semiJoin.simps ‹(A, X) = projectTable J (semiJoin (AA, XX) (I, zI))›
            inf_commute snd_conv)
      then obtain zz where "restrict A zJ = restrict J zz" and "zz ∈ (Set.filter (isSameIntersection zI (I ∩ AA)) XX)"
        by blast
      moreover have "restrict A zJ = restrict AA zJ"
        by (simp add: restrict_nested ‹A = AA ∩ J› zJ_def)
      then have "restrict AA z = zz"
      proof -
        have "restrict J (restrict AA zz) = restrict J (restrict AA z)"
          by (metis (no_types, lifting) restrict_nested ‹restrict A zJ = restrict AA zJ›
              calculation(1) inf_commute inf_left_idem zJ_def)
        moreover have "isSameIntersection zI (I ∩ AA) zz"
          using ‹zz ∈ Set.filter (isSameIntersection zI (I ∩ AA)) XX› by auto
        moreover have "wf_tuple n AA zz"
        proof -
          have "rwf_query n V Q Qn" by (simp add: assms(16))
          moreover have "(AA, XX) ∈ Q ∪ Qn" by (simp add: ‹(AA, XX) ∈ Qn›)
          then have "wf_atable n (AA, XX)" using calculation rwf_query_def wf_query_def by blast
          then show ?thesis
            using ‹zz ∈ Set.filter (isSameIntersection zI (I ∩ AA)) XX› table_def wf_atable_def by fastforce
        qed
        moreover have "restrict AA zz = zz" using calculation(3) restrict_idle by blast
        moreover have "AA ⊆ V"
        proof -
          have "included V Qn" using assms(16) rwf_query_def by blast
          then show ?thesis using ‹(AA, XX) ∈ Qn› included_def by fastforce
        qed
        moreover have "wf_set n V" using assms(16) rwf_query_def wf_query_def by blast
        moreover have "restrict (I ∩ AA) zz = restrict (I ∩ AA) zI"
          using isSame_equi_dev[of n V AA zz V z "I ∩ AA"]
          by (metis (mono_tags, lifting) isSame_equi_dev ‹wf_tuple n I zI› assms(1)
              calculation(2) calculation(3) calculation(5) calculation(6) inf_le1 inf_le2 sup_ge1)
        then have "restrict I (restrict AA zz) = restrict I (restrict AA z)"
          by (metis (mono_tags, lifting) restrict_nested inf_le1 nested_include_restrict zI_def)
        then have "restrict (I ∪ J) (restrict AA z) = restrict (I ∪ J) (restrict AA zz)"
          using union_restrict calculation(1) by fastforce
        moreover have "AA ⊆ I ∪ J"
          by (metis ‹(AA, XX) ∈ Qn› assms(1) assms(16) case_prodD included_def rwf_query_def)
        then show ?thesis
          by (metis restrict_nested calculation(4) calculation(7) inf.absorb_iff2)
      qed
      then show "False" using ‹restrict AA z ∉ XX› calculation(2) by auto
    qed
  qed
  then have "zJ ∈ genericJoin J (newQuery J Q_J_pos (I, zI)) (newQuery J Q_J_neg (I, zI))"
    using ‹wf_tuple n J zJ› calculation(3) calculation(4) by blast
  have "z = merge zJ zI"
    using restrict_partition_merge assms(1) assms(15) assms(2) zI_def zJ_def by fastforce
  moreover have "(zI, genericJoin J (newQuery J Q_J_pos (I, zI)) (newQuery J Q_J_neg (I, zI))) ∈ X"
    using ‹zI ∈ R_I› assms(10) by blast
  then show ?thesis
    using ‹zJ ∈ genericJoin J (newQuery J Q_J_pos (I, zI)) (newQuery J Q_J_neg (I, zI))› assms(11)
      calculation(5) by blast
qed

lemma obvious_forall:
  assumes "∀x∈X. P x"
  assumes "x∈X"
  shows "P x"
  by (simp add: assms(1) assms(2))

lemma correctness:
  "⟦rwf_query n V Q Qn; card V ≥ 1⟧ ⟹ (z ∈ genericJoin V Q Qn ⟷ wf_tuple n V z ∧
  (∀(A, X)∈Q. restrict A z ∈ X) ∧ (∀(A, X)∈Qn. restrict A z ∉ X))"
proof (induction V Q Qn arbitrary: z rule: genericJoin.induct)
  case (1 V Q Qn)
    then show ?case
    proof (cases "card V ≤ 1")
      case True
      have "card V = 1" using "1.prems"(2) True le_antisym by blast
      then show ?thesis using base_correctness[of V n Q Qn "genericJoin V Q Qn" z] using "1.prems"(1) by blast
    next
      case False
      obtain I J where "(I, J) = getIJ Q Qn V" by (metis surj_pair)
      define Q_I_pos where "Q_I_pos = projectQuery I (filterQuery I Q)"
      define Q_I_neg where "Q_I_neg = filterQueryNeg I Qn"
      define R_I where "R_I = genericJoin I Q_I_pos Q_I_neg"
      define Q_J_neg where "Q_J_neg = filterQuery J (Qn - Q_I_neg)"
      define Q_J_pos where "Q_J_pos = filterQuery J Q"
      define X where "X = {(t, genericJoin J (newQuery J Q_J_pos (I, t)) (newQuery J Q_J_neg (I, t))) | t . t ∈ R_I}"
      define R where "R = (⋃(t, x) ∈ X. {merge xx t | xx . xx ∈ x})"
      then have "R = genericJoin V Q Qn"
        using vars_genericJoin[of V I J Q Qn Q_I_pos Q_I_neg R_I Q_J_neg Q_J_pos X R]
        by (metis "1.prems"(1) False Q_I_neg_def Q_I_pos_def Q_J_neg_def Q_J_pos_def R_I_def Suc_1 X_def
            ‹(I, J) = getIJ Q Qn V› not_less_eq_eq)
      obtain "rwf_query n I Q_I_pos Q_I_neg" and "card I ≥ 1"
        by (metis "1.prems"(1) False Q_I_neg_def Q_I_pos_def Suc_1 ‹(I, J) = getIJ Q Qn V› getIJ.getIJProperties(1)
            getIJ.wf_firstRecursiveCall getIJ_axioms not_less_eq_eq)
      then have "∀x. (x ∈ R_I ⟷
  wf_tuple n I x ∧ (∀(A, X)∈Q_I_pos. restrict A x ∈ X)  ∧ (∀(A, X)∈Q_I_neg. restrict A x ∉ X))"
        using "1.IH"(1) False Q_I_neg_def Q_I_pos_def R_I_def ‹(I, J) = getIJ Q Qn V› by auto
      moreover have "∀t∈R_I. (∀y. (y ∈ genericJoin J (newQuery J Q_J_pos (I, t)) (newQuery J Q_J_neg (I, t)) ⟷ wf_tuple n J y ∧
  (∀(A, X)∈(newQuery J Q_J_pos (I, t)). restrict A y ∈ X) ∧ (∀(A, X)∈(newQuery J Q_J_neg (I, t)). restrict A y ∉ X)))"
      proof
        fix t assume "t ∈ R_I"
        have "card J ≥ 1"
          by (metis False Suc_1 ‹(I, J) = getIJ Q Qn V› getIJProperties(2) le_SucE nat_le_linear)
        moreover have "rwf_query n J (newQuery J Q_J_pos (I, t)) (newQuery J Q_J_neg (I, t))"
          by (metis "1.prems"(1) Diff_subset False Q_J_neg_def Q_J_pos_def Suc_1 ‹(I, J) = getIJ Q Qn V›
              getIJ.wf_secondRecursiveCalls getIJ_axioms not_less_eq_eq)
        define NQ_pos where "NQ_pos = newQuery J Q_J_pos (I, t)"
        define NQ_neg where "NQ_neg = newQuery J Q_J_neg (I, t)"
        have "⋀y. y ∈ genericJoin J NQ_pos NQ_neg ⟷
  wf_tuple n J y ∧ (∀(A, X)∈NQ_pos. restrict A y ∈ X) ∧ (∀(A, X)∈NQ_neg. restrict A y ∉ X)"
        proof -
          fix y
          have "rwf_query n J NQ_pos NQ_neg"
            using NQ_neg_def NQ_pos_def ‹rwf_query n J (newQuery J Q_J_pos (I, t)) (newQuery J Q_J_neg (I, t))› by blast
          then show "y ∈ genericJoin J NQ_pos NQ_neg ⟷
  wf_tuple n J y ∧ (∀(A, X)∈NQ_pos. restrict A y ∈ X) ∧ (∀(A, X)∈NQ_neg. restrict A y ∉ X)"
            using "1.IH"(2)[of "(I, J)" I J Q_I_pos Q_I_neg R_I Q_J_neg Q_J_pos t y]
            by (metis "1.prems"(1) False NQ_neg_def NQ_pos_def Q_I_neg_def Q_I_pos_def Q_J_neg_def
                Q_J_pos_def R_I_def Suc_1 ‹(I, J) = getIJ Q Qn V› calculation filter_Q_J_neg_same not_less_eq_eq)
        qed
        then show "∀y. (y ∈ genericJoin J (newQuery J Q_J_pos (I, t)) (newQuery J Q_J_neg (I, t)) ⟷ wf_tuple n J y ∧
  (∀(A, X)∈(newQuery J Q_J_pos (I, t)). restrict A y ∈ X) ∧ (∀(A, X)∈(newQuery J Q_J_neg (I, t)). restrict A y ∉ X))"
          using NQ_neg_def NQ_pos_def by blast
      qed
      moreover obtain "V = I ∪ J" "Set.is_empty (I ∩ J)" "card I ≥ 1" "card J ≥ 1"
        by (metis False Set.is_empty_def Suc_1 ‹(I, J) = getIJ Q Qn V› coreProperties not_less_eq_eq)
      moreover have "rwf_query n V Q Qn" by (simp add: "1.prems"(1))
      then show ?thesis
      proof -
        have "z ∈ genericJoin V Q Qn ⟹ wf_tuple n V z ∧ (∀(A, X)∈Q. restrict A z ∈ X) ∧ (∀(A, X)∈Qn. restrict A z ∉ X)"
        proof -
          fix z assume "z ∈ genericJoin V Q Qn"
          have "z ∈ (⋃(t, x) ∈ X. {merge xx t | xx . xx ∈ x})"
            using R_def ‹R = genericJoin V Q Qn› ‹z ∈ genericJoin V Q Qn› by blast
          obtain t R_NQ where "z ∈ {merge xx t | xx . xx ∈ R_NQ}" "(t, R_NQ) ∈ X"
            using ‹z ∈ (⋃(t, x)∈X. {merge xx t |xx. xx ∈ x})› by blast
          then have "t ∈ R_I" using X_def by blast
          define NQ where "NQ = newQuery J Q_J_pos (I, t)"
          define NQ_neg where "NQ_neg = newQuery J Q_J_neg (I, t)"
          have "R_NQ = genericJoin J NQ NQ_neg" using NQ_def NQ_neg_def X_def ‹(t, R_NQ) ∈ X› by blast
          obtain xx where "z = merge xx t" "xx ∈ R_NQ"
            using ‹z ∈ {merge xx t |xx. xx ∈ R_NQ}› by blast
          have "∀y. (y ∈ R_NQ ⟷ wf_tuple n J y ∧ (∀(A, X)∈NQ. restrict A y ∈ X) ∧ (∀(A, X)∈NQ_neg. restrict A y ∉ X))"
          proof -
            have "∀tt∈R_I. (∀x. (x ∈ genericJoin J NQ NQ_neg
                         ⟷ wf_tuple n J x ∧ (∀(A, X)∈NQ. restrict A x ∈ X) ∧ (∀(A, X)∈NQ_neg. restrict A x ∉ X)))"
              using NQ_def NQ_neg_def ‹t ∈ R_I› calculation(2) by auto
            moreover have "t∈R_I" by (simp add: ‹t ∈ R_I›)
            then have "(∀x. (x ∈ genericJoin J NQ NQ_neg
                         ⟷ wf_tuple n J x ∧ (∀(A, X)∈NQ. restrict A x ∈ X) ∧  (∀(A, X)∈NQ_neg. restrict A x ∉ X)))"
              using obvious_forall[where ?x=t and ?X=R_I] calculation by fastforce
            then show ?thesis using ‹R_NQ = genericJoin J NQ NQ_neg› by blast
          qed
          show "wf_tuple n V z ∧ (∀(A, X)∈Q. restrict A z ∈ X) ∧ (∀(A, X)∈Qn. restrict A z ∉ X)"
            using partial_correctness[of V I J Q_I_pos Q Q_J_pos Q_I_neg Qn Q_J_neg NQ t NQ_neg R_NQ R_I n z xx]
            using "1.prems"(1) NQ_def NQ_neg_def Q_I_neg_def Q_I_pos_def Q_J_neg_def Q_J_pos_def
              ‹R_NQ = genericJoin J NQ NQ_neg› ‹∀y. (y ∈ R_NQ) = (wf_tuple n J y ∧ (∀(A, X)∈NQ. restrict A y ∈ X) ∧ (∀(A, X)∈NQ_neg. restrict A y ∉ X))›
              ‹t ∈ R_I› ‹xx ∈ R_NQ› ‹z = merge xx t› calculation(1) calculation(3) calculation(4) calculation(5) calculation(6) by blast
        qed
        moreover have "wf_tuple n V z ∧ (∀(A, X)∈Q. restrict A z ∈ X) ∧ (∀(A, X)∈Qn. restrict A z ∉ X) ⟹ z ∈ genericJoin V Q Qn"
        proof -
          fix z assume "wf_tuple n V z ∧ (∀(A, X)∈Q. restrict A z ∈ X) ∧ (∀(A, X)∈Qn. restrict A z ∉ X)"
          have "z ∈ R"
            using partial_correctness_direct[of V I J Q_I_pos Q Q_J_pos Q_I_neg Qn Q_J_neg R_I X R
                _ _ _ n z]
            "1.prems"(1) Q_I_neg_def Q_I_pos_def Q_J_neg_def Q_J_pos_def R_I_def R_def X_def
              ‹1 ≤ card I› ‹1 ≤ card J› ‹Set.is_empty (I ∩ J)› ‹V = I ∪ J›
              ‹∀t∈R_I. ∀y. (y ∈ genericJoin J (newQuery J Q_J_pos (I, t)) (newQuery J Q_J_neg (I, t))) = (wf_tuple n J y ∧ (∀(A, X)∈newQuery J Q_J_pos (I, t). restrict A y ∈ X) ∧ (∀(A, X)∈newQuery J Q_J_neg (I, t). restrict A y ∉ X))›
              ‹∀x. (x ∈ R_I) = (wf_tuple n I x ∧ (∀(A, X)∈Q_I_pos. restrict A x ∈ X) ∧ (∀(A, X)∈Q_I_neg. restrict A x ∉ X))›
              ‹wf_tuple n V z ∧ (∀(A, X)∈Q. restrict A z ∈ X) ∧ (∀(A, X)∈Qn. restrict A z ∉ X)› by blast
          then show "z ∈ genericJoin V Q Qn" using ‹R = genericJoin V Q Qn› by blast
        qed
        then show ?thesis using calculation by linarith
      qed
  qed
qed

lemma wf_set_finite:
  assumes "wf_set n A"
  shows "finite A"
  using assms finite_nat_set_iff_bounded wf_set_def by auto

lemma vars_wrapperGenericJoin:
  fixes Q :: "'a query" and Q_pos :: "'a query" and Q_neg :: "'a query"
  and V :: "nat set" and Qn :: "'a query"
  assumes "Q = Set.filter (λ(A, _). ¬ Set.is_empty A) Q_pos"
      and "V = (⋃(A, X)∈Q. A)"
      and "Qn = Set.filter (λ(A, _). A ⊆ V ∧ card A ≥ 1) Q_neg"
      and "¬ Set.is_empty Q"
      and "¬((∃(A, X)∈Q_pos. Set.is_empty X) ∨ (∃(A, X)∈Q_neg. Set.is_empty A ∧ ¬ Set.is_empty X))"
    shows "wrapperGenericJoin Q_pos Q_neg = genericJoin V Q Qn"
  using assms wrapperGenericJoin.simps
proof -
  let ?r = "wrapperGenericJoin Q_pos Q_neg"
  have "?r = (if ((∃(A, X)∈Q_pos. Set.is_empty X) ∨ (∃(A, X)∈Q_neg. Set.is_empty A ∧ ¬ Set.is_empty X)) then
      {}
    else
      let Q = Set.filter (λ(A, _). ¬ Set.is_empty A) Q_pos in
      if Set.is_empty Q then
        (⋂(A, X)∈Q_pos. X) -  (⋃(A, X)∈Q_neg. X)
      else
        let V = (⋃(A, X)∈Q. A) in
        let Qn = Set.filter (λ(A, _). A ⊆ V ∧ card A ≥ 1) Q_neg in
        genericJoin V Q Qn)" by simp
  also have "... = (let Q = Set.filter (λ(A, _). ¬ Set.is_empty A) Q_pos in
      if Set.is_empty Q then
        (⋂(A, X)∈Q_pos. X) -  (⋃(A, X)∈Q_neg. X)
      else
        let V = (⋃(A, X)∈Q. A) in
        let Qn = Set.filter (λ(A, _). A ⊆ V ∧ card A ≥ 1) Q_neg in
        genericJoin V Q Qn)" using assms(5) by simp
  moreover have "¬ (let Q = Set.filter (λ(A, _). ¬ Set.is_empty A) Q_pos in Set.is_empty Q)"
    using assms(1) assms(4) by auto
  ultimately have "(let Q = Set.filter (λ(A, _). ¬ Set.is_empty A) Q_pos in
      if Set.is_empty Q then
        (⋂(A, X)∈Q_pos. X) -  (⋃(A, X)∈Q_neg. X)
      else
        let V = (⋃(A, X)∈Q. A) in
        let Qn = Set.filter (λ(A, _). A ⊆ V ∧ card A ≥ 1) Q_neg in
        genericJoin V Q Qn) = (let Q = Set.filter (λ(A, _). ¬ Set.is_empty A) Q_pos in
        let V = (⋃(A, X)∈Q. A) in
        let Qn = Set.filter (λ(A, _). A ⊆ V ∧ card A ≥ 1) Q_neg in
        genericJoin V Q Qn)" by presburger
  also have "... = (genericJoin V Q Qn)" using assms(1) assms(2) assms(3) by metis
  then show ?thesis using wrapperGenericJoin.simps assms(5) calculation by simp
qed

lemma wrapper_correctness:
  assumes "card Q_pos ≥1"
  assumes "∀(A, X)∈(Q_pos ∪ Q_neg). table n A X ∧ wf_set n A"
  shows "z ∈ wrapperGenericJoin Q_pos Q_neg ⟷ wf_tuple n (⋃(A, X)∈Q_pos. A) z ∧ (∀(A, X)∈Q_pos. restrict A z ∈ X) ∧ (∀(A, X)∈Q_neg. restrict A z ∉ X)"
proof (cases "(∃(A, X)∈Q_pos. Set.is_empty X) ∨ (∃(A, X)∈Q_neg. Set.is_empty A ∧ ¬ Set.is_empty X)")
  let ?r = "wrapperGenericJoin Q_pos Q_neg"
  case True
  then have "?r = {}" using wrapperGenericJoin.simps by simp
  have "¬ (wf_tuple n (⋃(A, X)∈Q_pos. A) z ∧ (∀(A, X)∈Q_pos. restrict A z ∈ X) ∧ (∀(A, X)∈Q_neg. restrict A z ∉ X))"
  proof (rule notI)
    assume "wf_tuple n (⋃(A, X)∈Q_pos. A) z ∧ (∀(A, X)∈Q_pos. restrict A z ∈ X) ∧ (∀(A, X)∈Q_neg. restrict A z ∉ X)"
    then show "False"
    proof (cases "∃(A, X)∈Q_pos. Set.is_empty X")
      case True
      then show ?thesis
        using ‹wf_tuple n (⋃(A, X)∈Q_pos. A) z ∧ (∀(A, X)∈Q_pos. restrict A z ∈ X) ∧ (∀(A, X)∈Q_neg. restrict A z ∉ X)›
        by (metis (no_types, lifting) Set.is_empty_def case_prod_beta' empty_iff)
    next
      let ?v = "replicate n None"
      case False
      then have "∃(A, X)∈Q_neg. Set.is_empty A ∧ ¬ Set.is_empty X" using True by blast
      then obtain A X where "(A, X) ∈ Q_neg" "Set.is_empty A" "¬ Set.is_empty X" by auto
      then have "table n A X" using assms(2) by auto
      then have "X ⊆ {?v}" using ‹Set.is_empty A› table_empty unit_table_def
        by (metis Set.is_empty_def ‹¬ Set.is_empty X› empty_table_def set_eq_subset)
      then show ?thesis using ‹(A, X) ∈ Q_neg› ‹Set.is_empty A› ‹¬ Set.is_empty X›
          ‹wf_tuple n (⋃(A, X)∈Q_pos. A) z ∧ (∀(A, X)∈Q_pos. restrict A z ∈ X) ∧ (∀(A, X)∈Q_neg. restrict A z ∉ X)›
        by (metis (no_types, lifting) Set.is_empty_def ‹table n A X› case_prod_beta' empty_table_def
            in_unit_table inf_le1 inf_le2 prod.sel(1) snd_conv subset_empty table_empty wf_tuple_restrict_simple)
    qed
  qed
  then show ?thesis using ‹?r = {}› by simp
next
  case False
  then have forall: "(∀(A, X)∈Q_pos. ¬ Set.is_empty X) ∧ (∀(A, X)∈Q_neg. ¬ Set.is_empty A ∨ Set.is_empty X)" by auto
  define Q where "Q = Set.filter (λ(A, _). ¬ Set.is_empty A) Q_pos"
  define V where "V = (⋃(A, X)∈Q. A)"
  let ?r = "wrapperGenericJoin Q_pos Q_neg"
  show ?thesis
  proof (cases "Q = {}")
    case True
    then have r_def: "?r = (⋂(A, X)∈Q_pos. X) -  (⋃(A, X)∈Q_neg. X)" using Q_def Set.is_empty_def False by auto
    moreover have empty_u: "(⋃(A, X)∈Q_pos. A) = {}"
      by (metis (no_types, lifting) Q_def SUP_bot_conv(2) Set.is_empty_def True case_prod_beta' empty_iff member_filter)
    then have "V = {}" using True V_def by blast
    moreover have "⋀A X. (A, X) ∈ Q_pos ⟹ X ⊆ {replicate n None}"
    proof -
      fix A X assume "(A, X) ∈ Q_pos"
      then have "table n A X" using assms(2) by auto
      then have "A = {}"
      proof -
        have "(A, X) ∉ Q" by (simp add: True)
        then show ?thesis by (simp add: Q_def Set.is_empty_def ‹(A, X) ∈ Q_pos›)
      qed
      then show "X ⊆ {replicate n None}" using ‹A = {}› ‹table n A X› table_empty unit_table_def by fastforce
    qed
    have "?r ⊆ {replicate n None}"
    proof (rule subsetI)
      fix x assume "x ∈ ?r"
      obtain A X where "(A, X) ∈ Q_pos" using ‹card Q_pos ≥ 1›
        using True card.empty not_one_le_zero by (metis bot.extremum_uniqueI subrelI)
      then have "x ∈ X" using ‹x ∈ ?r› r_def by auto
      then show "x ∈ {replicate n None}" using ‹(A, X) ∈ Q_pos› ‹⋀X A. (A, X) ∈ Q_pos ⟹ X ⊆ {replicate n None}› by blast
    qed
    let ?v = "replicate n None"
    show ?thesis
    proof (cases "?r = {}")
      case True
      have disj: "∃A X. ((A, X) ∈ Q_pos ∧ X = {}) ∨ ((A, X) ∈ Q_neg ∧ {?v} ⊆ X)"
      proof (rule ccontr)
        assume "∄A X. (A, X) ∈ Q_pos ∧ X = {} ∨ (A, X) ∈ Q_neg ∧ {?v} ⊆ X"
        then have x_pos: "∀(A, X)∈Q_pos. X = {?v}" using ‹⋀X A. (A, X) ∈ Q_pos ⟹ X ⊆ {replicate n None}› by blast
        moreover have x_neg: "∀(A, X)∈Q_neg. ?v ∉ X" using ‹∄A X. (A, X) ∈ Q_pos ∧ X = {} ∨ (A, X) ∈ Q_neg ∧ {replicate n None} ⊆ X› by blast
        ultimately have "?v ∈ ?r" using r_def
        proof -
          have "?v ∈ (⋂(A, X)∈Q_pos. X)" using x_pos by auto
          moreover have "?v ∉ (⋃(A, X)∈Q_neg. X)" using x_neg by auto
          ultimately show ?thesis using r_def by auto
        qed
        then show "False" using True by blast
      qed
      have "¬ (wf_tuple n (⋃(A, X)∈Q_pos. A) z ∧ (∀(A, X)∈Q_pos. restrict A z ∈ X) ∧ (∀(A, X)∈Q_neg. restrict A z ∉ X))"
      proof (rule notI)
        assume "wf_tuple n (⋃(A, X)∈Q_pos. A) z ∧ (∀(A, X)∈Q_pos. restrict A z ∈ X) ∧ (∀(A, X)∈Q_neg. restrict A z ∉ X)"
        have "z = ?v"
          using ‹wf_tuple n (⋃(A, X)∈Q_pos. A) z ∧ (∀(A, X)∈Q_pos. restrict A z ∈ X) ∧ (∀(A, X)∈Q_neg. restrict A z ∉ X)› empty_u wf_tuple_empty by auto
        then have "⋀A. restrict A z = z"
          by (metis getIJ.restrict_index_out getIJ_axioms length_replicate length_restrict nth_replicate nth_restrict simple_list_index_equality)
        then have "(∃(A, X)∈Q_pos. z ∉ X) ∨ (∃(A, X)∈Q_neg. z ∈ X)" using disj using ‹z = replicate n None› by auto
        then show "False"
          using ‹⋀A. restrict A z = z› ‹wf_tuple n (⋃(A, X)∈Q_pos. A) z ∧ (∀(A, X)∈Q_pos. restrict A z ∈ X) ∧ (∀(A, X)∈Q_neg. restrict A z ∉ X)› by auto
      qed
      then show ?thesis using True by blast
    next
      case False
      then have "?r = {?v}" using ‹wrapperGenericJoin Q_pos Q_neg ⊆ {replicate n None}› by blast
      then have "⋀A X. (A, X) ∈ Q_pos ⟹ X = {?v}"
          using Set.is_empty_def ‹⋀X A. (A, X) ∈ Q_pos ⟹ X ⊆ {replicate n None}› forall by fastforce
      then have "∀(A, X)∈Q_pos. X = {?v}" by blast
      moreover have "∀(A, X)∈Q_neg. ?v ∉ X" using ‹wrapperGenericJoin Q_pos Q_neg = {replicate n None}› r_def by auto
      ultimately show ?thesis (is "?a ⟷ ?b")
      proof -
        have "?a ⟹ ?b"
        proof -
          assume "?a"
          then have "z = ?v" using ‹wrapperGenericJoin Q_pos Q_neg = {replicate n None}› by blast
          then have "⋀A. restrict A z = z"
            by (metis getIJ.restrict_index_out getIJ_axioms length_replicate length_restrict nth_replicate nth_restrict simple_list_index_equality)
          then show "?b" using ‹∀(A, X)∈Q_neg. replicate n None ∉ X› ‹∀(A, X)∈Q_pos. X = {replicate n None}›
              ‹z = replicate n None› empty_u wf_tuple_empty by fastforce
        qed
        moreover have "?b ⟹ ?a"
          using ‹wrapperGenericJoin Q_pos Q_neg = {replicate n None}› empty_u wf_tuple_empty by auto
        ultimately show ?thesis by blast
      qed
    qed
  next
    case False
    then have False_prev: "Q ≠ {}" by simp
    have "covering V Q" using V_def covering_def by blast
    moreover have "included V Q" using included_def V_def by fastforce
    define Qn where "Qn = Set.filter (λ(A, _). A ⊆ V ∧ card A ≥ 1) Q_neg"
    then have "Qn ⊆ Q_neg" by auto
    moreover have "wf_query n V Q Qn"
    proof -
      have "wf_set n V"
      proof -
        have "⋀x. x ∈ V ⟹ x < n"
        proof -
          fix x assume "x ∈ V"
          obtain A X where "x ∈ A" "(A, X) ∈ Q" using V_def ‹x ∈ V› by blast
          then have "(A, X) ∈ (Q_pos ∪ Q_neg)" by (simp add: Q_def)
          then have "wf_set n A" using assms(2) by auto
          then show "x < n" using ‹x ∈ A› wf_set_def by blast
        qed
        then show ?thesis using wf_set_def by blast
      qed
      moreover have "card Q ≥ 1"
      proof -
        have "finite Q_pos" using assms(1) not_one_le_zero by fastforce
        then have "finite Q" by (simp add: Q_def)
        then show ?thesis using False by (simp add: Suc_leI card_gt_0_iff)
      qed
      moreover have "⋀Y. Y ∈ (Q ∪ Q_neg) ⟹ wf_atable n Y"
      proof -
        fix Y assume "Y ∈ (Q ∪ Q_neg)"
        then obtain A X where "Y = (A, X)" by (meson case_prodE case_prodI2)
        then have "table n A X"
          by (metis (no_types, lifting) Q_def UnE Un_iff ‹Y ∈ Q ∪ Q_neg› assms(2) case_prodD member_filter sup_commute)
        moreover have "finite A"
        proof -
          have "wf_set n A"
            by (metis (no_types, lifting) Q_def UnE Un_iff ‹Y = (A, X)› ‹Y ∈ Q ∪ Q_neg› assms(2) case_prod_conv member_filter sup.commute)
          then show ?thesis using wf_set_finite by blast
        qed
        ultimately show "wf_atable n Y" by (simp add: ‹Y = (A, X)› wf_atable_def)
      qed
      ultimately have "wf_query n V Q Q_neg" using wf_query_def by blast
      then show ?thesis using Un_iff ‹Qn ⊆ Q_neg› subsetD wf_query_def
      proof -
        obtain pp :: "(nat set × 'a option list set) set ⇒ (nat set × 'a option list set) set ⇒ nat ⇒ nat set × 'a option list set" where
          f1: "∀n N P Pa. (wf_query n N P Pa ∨ ¬ 1 ≤ card P ∨ ¬ wf_set n N ∨ ¬ wf_atable n (pp Pa P n) ∧ pp Pa P n ∈ P ∪ Pa) ∧ (1 ≤ card P ∧ wf_set n N ∧ (∀p. wf_atable n p ∨ p ∉ P ∪ Pa) ∨ ¬ wf_query n N P Pa)"
          by (metis (full_types) wf_query_def)
        have "pp Qn Q n ∈ Qn ⟶ pp Qn Q n ∈ Q_neg"
          using ‹Qn ⊆ Q_neg› by blast
        then have "pp Qn Q n ∈ Q ∪ Q_neg ∨ wf_query n V Q Qn" using ‹1 ≤ card Q› ‹wf_set n V› f1 by auto
        then show ?thesis using ‹1 ≤ card Q› ‹⋀Y. Y ∈ Q ∪ Q_neg ⟹ wf_atable n Y› ‹wf_set n V› f1 by blast
      qed
    qed
    moreover have "non_empty_query Q"
    proof -
      have "⋀A X. (A, X) ∈ Q ⟹ card A ≥ 1"
      proof -
        fix A X assume asm: "(A, X) ∈ Q"
        then have "wf_set n A"
          by (metis ‹included V Q› calculation(3) case_prodD included_def subsetD wf_query_def wf_set_def)
        then have "finite A" using wf_set_finite by blast
        then show "card A ≥ 1"
          by (metis (no_types, lifting) One_nat_def Q_def Set.is_empty_def Suc_leI asm card_gt_0_iff case_prod_beta' member_filter prod.sel(1))
      qed
      then show ?thesis by (metis Q_def case_prodE fst_conv member_filter non_empty_query_def)
    qed
    moreover have "included V Qn" by (simp add: Qn_def case_prod_beta' included_def)
    moreover have "non_empty_query Qn" by (simp add: Qn_def case_prod_beta' non_empty_query_def)
    then have "rwf_query n V Q Qn"
      by (simp add: ‹included V Q› calculation(1) calculation(3) calculation(4) calculation(5) rwf_query_def)
    moreover have "card V ≥ 1"
    proof -
      obtain A X where "(A, X) ∈ Q_pos" "¬ Set.is_empty A" using False Q_def by force
      then have "A ⊆ V" by (metis Q_def ‹included V Q› included_def member_filter prod.simps(2))
      moreover have "finite V" using wf_set_finite ‹wf_query n V Q Qn› wf_query_def by blast
      ultimately show ?thesis
        by (metis One_nat_def Set.is_empty_def Suc_leI ‹¬ Set.is_empty A› card_gt_0_iff subset_empty)
    qed
    then have "z ∈ genericJoin V Q Qn ⟷ wf_tuple n V z ∧ (∀(A, X)∈Q. restrict A z ∈ X) ∧ (∀(A, X)∈Qn. restrict A z ∉ X)"
      using correctness[where ?n=n and ?V=V and ?Q=Q and ?z=z] by (simp add: calculation(6))
    moreover have "?r = genericJoin V Q Qn"
    proof -
      have "Qn = Set.filter (λ(A, _). A ⊆ V ∧ 1 ≤ card A) Q_neg" using Qn_def by blast
      moreover have "¬ Set.is_empty Q" by (simp add: False_prev Set.is_empty_def)
      moreover have "¬ ((∃(A, X)∈Q_pos. Set.is_empty X) ∨ (∃(A, X)∈Q_neg. Set.is_empty A ∧ ¬ Set.is_empty X))"
        using forall by blast
      ultimately show ?thesis using vars_wrapperGenericJoin[of Q Q_pos V Qn Q_neg] Q_def V_def by simp
    qed
    moreover have "z ∈ genericJoin V Q Qn ⟹ (∀(A, X)∈Q_pos - Q. restrict A z ∈ X) ∧ (∀(A, X)∈Q_neg - Qn. restrict A z ∉ X)"
    proof -
      assume "z ∈ genericJoin V Q Qn"
      have "(⋀A X. (A, X)∈Q_pos - Q ⟹ restrict A z ∈ X)"
      proof -
        fix A X assume "(A, X) ∈ Q_pos - Q"
        then have "table n A X" using assms(2) by auto
        moreover have "Set.is_empty A"
          by (metis (no_types, lifting) DiffD1 DiffD2 Q_def ‹(A, X) ∈ Q_pos - Q› case_prod_beta' member_filter prod.sel(1))
        moreover have "¬ Set.is_empty X" using forall using ‹(A, X) ∈ Q_pos - Q› by blast
        ultimately have "X = {replicate n None}" by (simp add: Set.is_empty_def empty_table_def table_empty unit_table_def)
        moreover have "wf_tuple n V z"
          using ‹(z ∈ genericJoin V Q Qn) = (wf_tuple n V z ∧ (∀(A, X)∈Q. restrict A z ∈ X) ∧ (∀(A, X)∈Qn. restrict A z ∉ X))› ‹z ∈ genericJoin V Q Qn› by linarith
        then have "restrict A z = replicate n None"
          using ‹Set.is_empty A› wf_tuple_empty wf_tuple_restrict_simple
          by (metis Diff_Int2 Diff_Int_distrib2 Diff_eq_empty_iff Set.is_empty_def inf_le2)
        then show "restrict A z ∈ X" by (simp add: calculation)
      qed
      moreover have "⋀A X. (A, X)∈Q_neg - Qn ⟹ restrict A z ∉ X"
      proof -
        fix A X assume "(A, X) ∈ Q_neg - Qn"
        then have notc: "¬ (card A ≥ 1 ∧ A ⊆ V)" using Qn_def by auto
        then show "restrict A z ∉ X"
        proof (cases "A ⊆ V")
          case True
          then have "card A = 0" using Qn_def using notc by linarith
          then have "Set.is_empty X"
            by (metis DiffD1 Set.is_empty_def True ‹(A, X) ∈ Q_neg - Qn› ‹1 ≤ card V› card_eq_0_iff forall notc prod.simps(2) rev_finite_subset)
          then show ?thesis by (simp add: Set.is_empty_def)
        next
          case False
          then obtain i where "i ∈ A" "i ∉ V" by blast
          then have "i < n"
          proof -
            have "(A, X) ∈ Q_neg" using ‹(A, X) ∈ Q_neg - Qn› by auto
            then have "wf_set n A" using assms(2) by auto
            then show ?thesis by (simp add: ‹i ∈ A› wf_set_def)
          qed
          moreover have "table n A X"
          proof -
            have "(A, X) ∈ Q_neg" using ‹(A, X) ∈ Q_neg - Qn› by auto
            then show ?thesis using assms(2) by auto
          qed
          have "wf_tuple n V z"
            using ‹(z ∈ genericJoin V Q Qn) = (wf_tuple n V z ∧ (∀(A, X)∈Q. restrict A z ∈ X) ∧ (∀(A, X)∈Qn. restrict A z ∉ X))› ‹z ∈ genericJoin V Q Qn› by blast
          show ?thesis
          proof (rule ccontr)
            let ?zz = "restrict A z"
            assume "¬ ?zz ∉ X"
            then have "?zz ∈ X" by blast
            then have "wf_tuple n A ?zz" using ‹table n A X› table_def by blast
            then have "?zz ! i ≠ None"
              by (simp add: ‹i ∈ A› calculation wf_tuple_def)
            moreover have "z ! i = None" using ‹wf_tuple n V z› ‹i ∉ V› wf_tuple_def using ‹i < n› by blast
            ultimately show "False"
              using ‹i < n› ‹i ∈ A› ‹wf_tuple n A (restrict A z)› nth_restrict wf_tuple_length by fastforce
          qed
        qed
      qed
      ultimately show ?thesis by blast
    qed
    ultimately have "z ∈ genericJoin V Q Qn ⟷ (∀(A, X)∈Q_pos - Q. restrict A z ∈ X) ∧ (∀(A, X)∈Q_neg - Qn. restrict A z ∉ X)
∧ wf_tuple n V z ∧ (∀(A, X)∈Q. restrict A z ∈ X) ∧ (∀(A, X)∈Qn. restrict A z ∉ X)" by blast
    moreover have "V = (⋃(A, X)∈Q_pos. A)"
    proof -
      have "(⋃(A, X)∈Q_pos - Q. A) = {}"
      proof -
        have "⋀A X. (A, X) ∈ (Q_pos - Q) ⟹ A = {}" by (simp add: Q_def Set.is_empty_def)
        then show ?thesis by blast
      qed
      moreover have "V = (⋃(A, X)∈Q. A)" using V_def by simp
      moreover have "(⋃(A, X)∈Q_pos. A) = (⋃(A, X)∈Q. A) ∪ (⋃(A, X)∈Q_pos - Q. A)" using Q_def by auto
      ultimately show ?thesis by simp
    qed
    ultimately show ?thesis (is "?a = ?b")
    proof -
      have "?a ⟹ ?b" using Diff_iff ‹(z ∈ genericJoin V Q Qn) = ((∀(A, X)∈Q_pos - Q. restrict A z ∈ X) ∧ (∀(A, X)∈Q_neg - Qn. restrict A z ∉ X) ∧ wf_tuple n V z ∧ (∀(A, X)∈Q. restrict A z ∈ X) ∧ (∀(A, X)∈Qn. restrict A z ∉ X))› ‹V = (⋃(A, X)∈Q_pos. A)› ‹wrapperGenericJoin Q_pos Q_neg = genericJoin V Q Qn› by blast
      moreover have "?b ⟹ ?a" using Q_def Qn_def ‹(z ∈ genericJoin V Q Qn) = (wf_tuple n V z ∧ (∀(A, X)∈Q. restrict A z ∈ X) ∧ (∀(A, X)∈Qn. restrict A z ∉ X))› ‹V = (⋃(A, X)∈Q_pos. A)› ‹wrapperGenericJoin Q_pos Q_neg = genericJoin V Q Qn› by auto
      ultimately show ?thesis by blast
    qed
  qed
qed

end

end