Theory 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  (xV. 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 = (XQ. 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 "(is. t1!i = t2!i)  (restrict s t1 = restrict s t2)" (is "?A  ?B")
  proof -
    have "?B  ?A"
    proof -
      assume "?B"
      have "i. is  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 is. 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 "XQ. (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 "XQp. (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
            XQp. (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 "(XQQp. 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 "(XQn. 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 "XQ. 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 "XQQ. 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 "XtQ. 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 "XQ. 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 "XQQ. wf_atable n X"
    proof -
      have "X. XQQ  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 "XQ0. wf_atable n X"
  shows "non_empty_query Q2"
proof -
  have "X. XQ2  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 "XQ. 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 "XQS. 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. XQQn  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 "XQQn. 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) XprojectQuery 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)
      XQS. 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 "XQQn. 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 "XQ_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. tR_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 "tR_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 "xR. 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 "xX. 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 = AI"
        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  (XA. f X)"
  shows "I  (XA. (f X)  I)"
proof -
  have "x. x  I  x  (XA. (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  (XA. (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 "tR_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 "xX. P x"
  assumes "xX"
  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 "tR_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 "ttR_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 "tR_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
              tR_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