Theory Clique_Large_Monotone_Circuits

theory Clique_Large_Monotone_Circuits
  imports 
  Sunflowers.Erdos_Rado_Sunflower
  Preliminaries
  Assumptions_and_Approximations
  Monotone_Formula
begin

text disable list-syntax
no_syntax "_list" :: "args  'a list" ("[(_)]")
no_syntax "__listcompr" :: "args  'a list" ("[(_)]")

hide_const (open) Sigma_Algebra.measure

subsection Plain Graphs

definition binprod :: "'a set  'a set  'a set set" (infixl "" 60) where
  "X  Y = {{x,y} | x y. x  X  y  Y  x  y}"

abbreviation sameprod :: "'a set  'a set set" ("(_)^𝟮") where
  "X^𝟮  X  X" 

lemma sameprod_altdef: "X^𝟮 = {Y. Y  X  card Y = 2}" 
  unfolding binprod_def by (auto simp: card_2_iff)

definition numbers :: "nat  nat set" ("[(_)]") where
  "[n]  {..<n}" 

lemma card_sameprod: "finite X  card (X^𝟮) = card X choose 2" 
  unfolding sameprod_altdef
  by (subst n_subsets, auto)

lemma sameprod_mono: "X  Y  X^𝟮  Y^𝟮"
  unfolding sameprod_altdef by auto

lemma sameprod_finite: "finite X  finite (X^𝟮)" 
  unfolding sameprod_altdef by simp

lemma numbers2_mono: "x  y  [x]^𝟮  [y]^𝟮"
  by (rule sameprod_mono, auto simp: numbers_def)

lemma card_numbers[simp]: "card [n] = n" 
  by (simp add: numbers_def)

lemma card_numbers2[simp]: "card ([n]^𝟮) = n choose 2" 
  by (subst card_sameprod, auto simp: numbers_def)


type_synonym vertex = nat
type_synonym graph = "vertex set set" 

definition Graphs :: "vertex set  graph set" where
  "Graphs V = { G. G  V^𝟮 }"  

definition Clique :: "vertex set  nat  graph set" where
  "Clique V k = { G. G  Graphs V  ( C  V. C^𝟮  G  card C = k) }" 

context first_assumptions
begin

abbreviation 𝒢 where "𝒢  Graphs [m]" 

lemmas 𝒢_def = Graphs_def[of "[m]"]

lemma empty_𝒢[simp]: "{}  𝒢" unfolding 𝒢_def by auto

definition v :: "graph  vertex set" where
 "v G = { x .  y. {x,y}  G}" 

lemma v_union: "v (G  H) = v G  v H" 
  unfolding v_def by auto

definition 𝒦 :: "graph set" where
  "𝒦 = { K . K  𝒢  card (v K) = k  K = (v K)^𝟮 }" 

lemma v_𝒢: "G  𝒢  v G  [m]" 
  unfolding v_def 𝒢_def sameprod_altdef by auto

lemma v_mono: "G  H  v G  v H" unfolding v_def by auto

lemma v_sameprod[simp]: assumes "card X  2" 
  shows "v (X^𝟮) = X" 
proof -
  from obtain_subset_with_card_n[OF assms] obtain Y where "Y  X" 
    and Y: "card Y = 2" by auto
  then obtain x y where "x  X" "y  X" and "x  y"
    by (auto simp: card_2_iff)
  thus ?thesis unfolding sameprod_altdef v_def
    by (auto simp: card_2_iff doubleton_eq_iff) blast
qed

lemma v_mem_sub: assumes "card e = 2" "e  G" shows "e  v G" 
proof -
  obtain x y where e: "e = {x,y}" and xy: "x  y" using assms
    by (auto simp: card_2_iff)
  from assms(2) have x: "x  v G" unfolding e
    by (auto simp: v_def)
  from e have e: "e = {y,x}" unfolding e by auto
  from assms(2) have y: "y  v G" unfolding e
    by (auto simp: v_def)
  show "e  v G" using x y unfolding e by auto
qed

lemma v_𝒢_2: assumes "G  𝒢" shows "G  (v G)^𝟮" 
proof
  fix e
  assume eG: "e  G" 
  with assms[unfolded 𝒢_def binprod_def] obtain x y where e: "e = {x,y}" and xy: "x  y" by auto
  from eG e xy have x: "x  v G" by (auto simp: v_def)
  from e have e: "e = {y,x}" unfolding e by auto
  from eG e xy have y: "y  v G" by (auto simp: v_def)
  from x y xy show "e  (v G)^𝟮" unfolding binprod_def e by auto
qed

  
lemma v_numbers2[simp]: "x  2  v ([x]^𝟮) = [x]" 
  by (rule v_sameprod, auto)

lemma sameprod_𝒢: assumes "X  [m]" "card X  2" 
  shows "X^𝟮  𝒢" 
  unfolding 𝒢_def using assms(2) sameprod_mono[OF assms(1)] 
  by auto

lemma finite_numbers[simp,intro]: "finite [n]" 
  unfolding numbers_def by auto

lemma finite_numbers2[simp,intro]: "finite ([n]^𝟮)" 
  unfolding sameprod_altdef using finite_subset[of _ "[m]"] by auto

lemma finite_members_𝒢: "G  𝒢  finite G"
  unfolding 𝒢_def using finite_subset[of G "[m]^𝟮"] by auto

lemma finite_𝒢[simp,intro]: "finite 𝒢" 
  unfolding 𝒢_def by simp

lemma finite_vG: assumes "G  𝒢"
  shows "finite (v G)"
proof -
  from finite_members_𝒢[OF assms]
  show ?thesis 
  proof (induct rule: finite_induct)
    case (insert xy F)
    show ?case
    proof (cases " x y. xy = {x,y}")
      case False
      hence "v (insert xy F) = v F" unfolding v_def by auto
      thus ?thesis using insert by auto
    next
      case True
      then obtain x y where xy: "xy = {x,y}" by auto
      hence "v (insert xy F) = insert x (insert y (v F))" 
        unfolding v_def by auto
      thus ?thesis using insert by auto
    qed
  qed (auto simp: v_def)
qed

lemma v_empty[simp]: "v {} = {}" unfolding v_def by auto

lemma v_card2: assumes "G  𝒢" "G  {}" 
  shows "2  card (v G)" 
proof -
  from assms[unfolded 𝒢_def] obtain edge where *: "edge  G" "edge  [m]^𝟮" by auto
  then obtain x y where edge: "edge = {x,y}" "x  y" unfolding binprod_def by auto
  with * have sub: "{x,y}  v G" unfolding v_def
    by (smt (verit, best) insert_commute insert_compr mem_Collect_eq singleton_iff subsetI)
  from assms finite_vG have "finite (v G)" by auto
  from sub x  y this show "2  card (v G)"
    by (metis card_2_iff card_mono)
qed


lemma 𝒦_altdef: "𝒦 = {V^𝟮 | V. V  [m]  card V = k}" 
  (is "_ = ?R")
proof -
  {
    fix K 
    assume "K  𝒦"
    hence K: "K  𝒢" and card: "card (v K) = k" and KvK: "K = (v K)^𝟮" 
      unfolding 𝒦_def by auto
    from v_𝒢[OF K] card KvK have "K  ?R" by auto
  }
  moreover
  {
    fix V
    assume 1: "V  [m]" and "card V = k" 
    hence "V^𝟮  𝒦" unfolding 𝒦_def using k2 sameprod_𝒢[OF 1]
      by auto
  }
  ultimately show ?thesis by auto
qed
    
lemma 𝒦_𝒢: "𝒦  𝒢" 
  unfolding 𝒦_def by auto
  
definition CLIQUE :: "graph set" where
  "CLIQUE = { G. G  𝒢  ( K  𝒦. K  G) }" 

lemma empty_CLIQUE[simp]: "{}  CLIQUE" unfolding CLIQUE_def 𝒦_def using k2 by (auto simp: v_def)

subsection Test Graphs

text Positive test graphs are precisely the cliques of size @{term k}.

abbreviation "POS  𝒦"

lemma POS_𝒢: "POS  𝒢" by (rule 𝒦_𝒢)

text Negative tests are coloring-functions of vertices that encode graphs
  which have cliques of size at most @{term "k - 1"}.

type_synonym colorf = "vertex  nat" 

definition  :: "colorf set" where
  " = [m] E [k - 1]" 

lemma finite_ℱ: "finite "
  unfolding ℱ_def numbers_def
  by (meson finite_PiE finite_lessThan)

definition C :: "colorf  graph" where
  "C f = { {x, y} | x y . {x,y}  [m]^𝟮  f x  f y}" 

definition NEG :: "graph set" where
  "NEG = C ` "

paragraph Lemma 1

lemma CLIQUE_NEG: "CLIQUE  NEG = {}" 
proof -
  {
    fix G
    assume GC: "G  CLIQUE" and GN: "G  NEG" 
    from GC[unfolded CLIQUE_def] obtain K where 
      K: "K  𝒦" and G: "G  𝒢" and KsubG: "K  G" by auto
    from GN[unfolded NEG_def] obtain f where fF: "f  " and 
      GCf: "G = C f" by auto
    from K[unfolded 𝒦_def] have KG: "K  𝒢" and 
      KvK: "K = v K^𝟮" and card1: "card (v K) = k" by auto
    from k2 card1 have ineq: "card (v K) > card [k - 1]" by auto
    from v_𝒢[OF KG] have vKm: "v K  [m]" by auto
    from fF[unfolded ℱ_def] vKm have f: "f  v K  [k - 1]"  
      by auto
    from card_inj[OF f] ineq 
    have "¬ inj_on f (v K)" by auto
    then obtain x y where *: "x  v K" "y  v K" "x  y" and ineq: "f x = f y" 
      unfolding inj_on_def by auto
    have "{x,y}  G" unfolding GCf C_def using ineq
      by (auto simp: doubleton_eq_iff)
    with KsubG KvK have "{x,y}  v K^𝟮" by auto
    with * have False unfolding binprod_def by auto
  }
  thus ?thesis by auto
qed

lemma NEG_𝒢: "NEG  𝒢" 
proof -
  {
    fix f
    assume "f  " 
    hence "C f  𝒢" 
      unfolding NEG_def C_def 𝒢_def 
      by (auto simp: sameprod_altdef)
  }
  thus "NEG  𝒢" unfolding NEG_def by auto
qed

lemma finite_POS_NEG: "finite (POS  NEG)" 
  using POS_𝒢 NEG_𝒢 
  by (intro finite_subset[OF _ finite_𝒢], auto)

lemma POS_sub_CLIQUE: "POS  CLIQUE" 
  unfolding CLIQUE_def using 𝒦_𝒢 by auto

lemma POS_CLIQUE: "POS  CLIQUE" 
proof -
  have "[k+1]^𝟮  CLIQUE" 
    unfolding CLIQUE_def
  proof (standard, intro conjI bexI[of _ "[k]^𝟮"])
    show "[k]^𝟮  [k+1]^𝟮" 
      by (rule numbers2_mono, auto)
    show "[k]^𝟮  𝒦" unfolding 𝒦_altdef using km 
      by (auto intro!: exI[of _ "[k]"], auto simp: numbers_def)
    show "[k+1]^𝟮  𝒢" using km k2
      by (intro sameprod_𝒢, auto simp: numbers_def)
  qed
  moreover have "[k+1]^𝟮  POS" unfolding 𝒦_def using v_numbers2[of "k + 1"] k2 
    by auto
  ultimately show ?thesis using POS_sub_CLIQUE by blast
qed

lemma card_POS: "card POS = m choose k" 
proof -
  have "m choose k =
    card {B. B  [m]  card B = k}" (is "_ = card ?A")
    by (subst n_subsets[of "[m]" k], auto simp: numbers_def) 
  also have " = card (sameprod ` ?A)" 
  proof (rule card_image[symmetric])
    { 
      fix A
      assume "A  ?A" 
      hence "v (sameprod A) = A" using k2
        by (subst v_sameprod, auto)
    }
    thus "inj_on sameprod ?A" by (rule inj_on_inverseI)
  qed
  also have "sameprod ` {B. B  [m]  card B = k} = POS" 
    unfolding 𝒦_altdef by auto
  finally show ?thesis by simp
qed

subsection Basic operations on sets of graphs

definition odot :: "graph set  graph set  graph set" (infixl "" 65) where 
  "X  Y = { D  E | D E. D  X  E  Y}" 

lemma union_𝒢[intro]: "G  𝒢  H  𝒢  G  H  𝒢" 
  unfolding 𝒢_def by auto

lemma odot_𝒢: "X  𝒢  Y  𝒢  X  Y  𝒢" 
  unfolding odot_def by auto

subsection Acceptability

text Definition 2

definition accepts :: "graph set  graph  bool" (infixl "" 55) where
  "(X  G) = ( D  X. D  G)" 


lemma acceptsI[intro]: "D  G  D  X  X  G" 
  unfolding accepts_def by auto

definition ACC :: "graph set  graph set" where
  "ACC X = { G. G  𝒢  X  G}" 

definition ACC_cf :: "graph set  colorf set" where
  "ACC_cf X = { F. F    X  C F}" 

lemma ACC_cf_ℱ: "ACC_cf X  " 
  unfolding ACC_cf_def by auto

lemma finite_ACC[intro,simp]: "finite (ACC_cf X)" 
  by (rule finite_subset[OF ACC_cf_ℱ finite_ℱ])

lemma ACC_I[intro]: "G  𝒢  X  G  G  ACC X" 
  unfolding ACC_def by auto

lemma ACC_cf_I[intro]: "F    X  C F  F  ACC_cf X" 
  unfolding ACC_cf_def by auto

lemma ACC_cf_mono: "X  Y  ACC_cf X  ACC_cf Y"
  unfolding ACC_cf_def accepts_def by auto

text Lemma 3

lemma ACC_cf_empty: "ACC_cf {} = {}" 
  unfolding ACC_cf_def accepts_def by auto

lemma ACC_empty[simp]: "ACC {} = {}" 
  unfolding ACC_def accepts_def by auto

lemma ACC_cf_union: "ACC_cf (X  Y) = ACC_cf X  ACC_cf Y" 
  unfolding ACC_cf_def accepts_def by blast

lemma ACC_union: "ACC (X  Y) = ACC X  ACC Y" 
  unfolding ACC_def accepts_def by blast

lemma ACC_odot: "ACC (X  Y) = ACC X  ACC Y"
proof -
  {
    fix G
    assume "G  ACC (X  Y)" 
    from this[unfolded ACC_def accepts_def]
    obtain D E F :: graph where *: "D  X" "E  Y" "G  𝒢" "D  E  G"       
      by (force simp: odot_def)
    hence "G  ACC X  ACC Y" 
      unfolding ACC_def accepts_def by auto
  }
  moreover
  {
    fix G
    assume "G  ACC X  ACC Y" 
    from this[unfolded ACC_def accepts_def]
    obtain D E where *: "D  X" "E  Y" "G  𝒢" "D  G" "E  G" 
      by auto
    let ?F = "D  E" 
    from * have "?F  X  Y" unfolding odot_def using * by blast
    moreover have "?F  G" using * by auto
    ultimately have "G  ACC (X  Y)" using *
      unfolding ACC_def accepts_def by blast
  }
  ultimately show ?thesis by blast
qed

lemma ACC_cf_odot: "ACC_cf (X  Y) = ACC_cf X  ACC_cf Y"
proof -
  {
    fix G
    assume "G  ACC_cf (X  Y)" 
    from this[unfolded ACC_cf_def accepts_def]
    obtain D E :: graph where *: "D  X" "E  Y" "G  " "D  E  C G"       
      by (force simp: odot_def)
    hence "G  ACC_cf X  ACC_cf Y" 
      unfolding ACC_cf_def accepts_def by auto
  }
  moreover
  {
    fix F
    assume "F  ACC_cf X  ACC_cf Y" 
    from this[unfolded ACC_cf_def accepts_def]
    obtain D E where *: "D  X" "E  Y" "F  " "D  C F" "E  C F" 
      by auto
    let ?F = "D  E" 
    from * have "?F  X  Y" unfolding odot_def using * by blast
    moreover have "?F  C F" using * by auto
    ultimately have "F  ACC_cf (X  Y)" using *
      unfolding ACC_cf_def accepts_def by blast 
  }
  ultimately show ?thesis by blast
qed

subsection Approximations and deviations

definition 𝒢l :: "graph set" where 
  "𝒢l = { G. G  𝒢  card (v G)  l }" 

definition v_gs :: "graph set  vertex set set" where
  "v_gs X = v ` X" 

lemma v_gs_empty[simp]: "v_gs {} = {}" 
  unfolding v_gs_def by auto

lemma v_gs_union: "v_gs (X  Y) = v_gs X  v_gs Y"
  unfolding v_gs_def by auto

lemma v_gs_mono: "X  Y  v_gs X  v_gs Y" 
  using v_gs_def by auto  

lemma finite_v_gs: assumes "X  𝒢" 
  shows "finite (v_gs X)" 
proof -
  have "v_gs X  v ` 𝒢"
    using assms unfolding v_gs_def by force
  moreover have "finite 𝒢" using finite_𝒢 by auto
  ultimately show ?thesis by (metis finite_surj)
qed

lemma finite_v_gs_Gl: assumes "X  𝒢l" 
  shows "finite (v_gs X)" 
  by (rule finite_v_gs, insert assms, auto simp: 𝒢l_def)


definition 𝒫L𝒢l :: "graph set set" where
  "𝒫L𝒢l = { X . X  𝒢l  card (v_gs X)  L}"

definition odotl :: "graph set  graph set  graph set" (infixl "⊙l" 65) where
  "X ⊙l Y = (X  Y)  𝒢l" 


lemma joinl_join: "X ⊙l Y  X  Y" 
  unfolding odot_def odotl_def by blast

lemma card_v_gs_join: assumes X: "X  𝒢" and Y: "Y  𝒢" 
  and Z: "Z  X  Y" 
  shows "card (v_gs Z)  card (v_gs X) * card (v_gs Y)" 
proof -
  note fin = finite_v_gs[OF X] finite_v_gs[OF Y]
  have "card (v_gs Z)  card ((λ (A, B). A  B) ` (v_gs X × v_gs Y))" 
  proof (rule card_mono[OF finite_imageI])
    show "finite (v_gs X × v_gs Y)" 
      using fin by auto
    have "v_gs Z  v_gs (X  Y)" 
      using v_gs_mono[OF Z] .
    also have "  (λ(x, y). x  y) ` (v_gs X × v_gs Y)" (is "?L  ?R")
      unfolding odot_def v_gs_def by (force split: if_splits simp: v_union)
    finally show "v_gs Z  (λ(x, y). x  y) ` (v_gs X × v_gs Y)" .
  qed
  also have "  card (v_gs X × v_gs Y)" 
    by (rule card_image_le, insert fin, auto)
  also have " = card (v_gs X) * card (v_gs Y)" 
    by (rule card_cartesian_product)
  finally show ?thesis .
qed

text Definition 6 -- elementary plucking step

definition plucking_step :: "graph set  graph set" where
  "plucking_step X = (let vXp = v_gs X;
      S = (SOME S. S  vXp  sunflower S  card S = p);
      U = {E  X. v E  S};
      Vs =  S;
      Gs = Vs^𝟮
     in X - U  {Gs})"
end

context second_assumptions
begin

text Lemma 9 -- for elementary plucking step

lemma v_sameprod_subset: "v (Vs^𝟮)  Vs" unfolding binprod_def v_def
  by (auto simp: doubleton_eq_iff)

lemma plucking_step: assumes X: "X  𝒢l"
  and L: "card (v_gs X) > L" 
  and Y: "Y = plucking_step X" 
shows "card (v_gs Y)  card (v_gs X) - p + 1" 
  "Y  𝒢l" 
  "POS  ACC X  ACC Y" 
  "2 ^ p * card (ACC_cf Y - ACC_cf X)  (k - 1) ^ m"
  "Y  {}"
proof -
  let ?vXp = "v_gs X"
  have sf_precond: "A ?vXp. finite A  card A  l" 
    using X unfolding 𝒢l_def 𝒢l_def v_gs_def by (auto intro: finite_vG intro!: v_𝒢 v_card2)
  note sunflower = Erdos_Rado_sunflower[OF sf_precond]
  from p have p0: "p  0" by auto
  have "(p - 1) ^ l * fact l < card ?vXp"  using L[unfolded L_def]
    by (simp add: ac_simps)
  note sunflower = sunflower[OF this]
  define S where "S = (SOME S. S  ?vXp  sunflower S  card S = p)" 
  define U where "U = {E  X. v E  S}" 
  define Vs where "Vs =  S"
  define Gs where "Gs = Vs^𝟮"
  let ?U = U 
  let ?New = "Gs :: graph" 
  have Y: "Y = X - U  {?New}" 
    using Y[unfolded plucking_step_def Let_def, folded S_def, folded U_def, 
        folded Vs_def, folded Gs_def] .
  have U: "U  𝒢l" using X unfolding U_def by auto 
  hence "U  𝒢" unfolding 𝒢l_def by auto
  from sunflower
  have " S. S  ?vXp  sunflower S  card S = p" by auto
  from someI_ex[OF this, folded S_def]
  have S: "S  ?vXp" "sunflower S" "card S = p" by (auto simp: Vs_def)
  have fin1: "finite ?vXp" using finite_v_gs_Gl[OF X] .
  from X have finX: "finite X" unfolding 𝒢l_def 
    using finite_subset[of X, OF _  finite_𝒢] by auto
  from fin1 S have finS: "finite S" by (metis finite_subset)
  from finite_subset[OF _ finX] have finU: "finite U" unfolding U_def by auto
  from S p have Snempty: "S  {}" by auto  
  have UX: "U  X" unfolding U_def by auto
  {
    from Snempty obtain s where sS: "s  S" by auto
    with S have "s  v_gs X" by auto
    then obtain Sp where "Sp  X" and sSp: "s = v Sp" 
      unfolding v_gs_def by auto
    hence *: "Sp  U" using s  S unfolding U_def by auto
    from * X UX have le: "card (v Sp)  l" "finite (v Sp)" "Sp  𝒢" 
      unfolding 𝒢l_def 𝒢l_def using finite_vG[of Sp] by auto
    hence m: "v Sp  [m]" by (intro v_𝒢)
    have "Vs  v Sp" using sS sSp unfolding Vs_def by auto
    with card_mono[OF finite (v Sp) this] finite_subset[OF this finite (v Sp)] le * m
    have "card Vs  l" "U  {}" "finite Vs" "Vs  [m]" by auto
  } 
  hence card_Vs: "card Vs  l" and Unempty: "U  {}" 
    and fin_Vs: "finite Vs" and Vsm: "Vs  [m]" by auto
  have vGs: "v Gs  Vs" unfolding Gs_def by (rule v_sameprod_subset)
  have GsG: "Gs  𝒢" unfolding Gs_def 𝒢_def
    by (intro CollectI Inter_subset sameprod_mono Vsm)
  have GsGl: "Gs  𝒢l" unfolding 𝒢l_def using GsG vGs card_Vs card_mono[OF _ vGs] 
    by (simp add: fin_Vs)
  hence DsDl: "?New  𝒢l" using UX  
    unfolding 𝒢l_def 𝒢_def 𝒢l_def 𝒢_def by auto
  with X U show "Y  𝒢l" unfolding Y by auto
  from X have XD: "X  𝒢" unfolding 𝒢l_def by auto
  have vplus_dsU: "v_gs U = S" using S(1)
    unfolding v_gs_def U_def by force
  have vplus_dsXU: "v_gs (X - U) = v_gs X - v_gs U"
    unfolding v_gs_def U_def by auto
  have "card (v_gs Y) = card (v_gs (X - U  {?New}))"  
    unfolding Y by simp
  also have "v_gs (X - U  {?New}) = v_gs (X - U)  v_gs ({?New})"
    unfolding v_gs_union ..
  also have "v_gs ({?New}) = {v (Gs)}" unfolding v_gs_def image_comp o_def by simp
  also have "card (v_gs (X - U)  )  card (v_gs (X - U)) + card "
    by (rule card_Un_le)
  also have "  card (v_gs (X - U)) + 1" by auto
  also have "v_gs (X - U) = v_gs X - v_gs U" by fact
  also have "card  = card (v_gs X) - card (v_gs U)" 
    by (rule card_Diff_subset, force simp: vplus_dsU finS, 
      insert UX, auto simp: v_gs_def)
  also have "card (v_gs U) = card S" unfolding vplus_dsU ..
  finally show "card (v_gs Y)  card (v_gs X) - p + 1" 
    using S by auto
  show "Y  {}" unfolding Y using Unempty by auto
  {
    fix G
    assume "G  ACC X" and GPOS: "G  POS"  
    from this[unfolded ACC_def] POS_𝒢 have G: "G  𝒢" "X  G" by auto
    from this[unfolded accepts_def] obtain D :: graph where 
      D: "D  X" "D  G" by auto
    have "G  ACC Y" 
    proof (cases "D  Y")
      case True
      with D G show ?thesis unfolding accepts_def ACC_def by auto
    next
      case False
      with D have DU: "D  U" unfolding Y by auto
      from GPOS[unfolded POS_def 𝒦_def] obtain K where GK: "G = (v K)^𝟮" "card (v K) = k" by auto
      from DU[unfolded U_def] have "v D  S" by auto
      hence "Vs  v D" unfolding Vs_def by auto
      also have "  v G" 
        by (intro v_mono D)
      also have " = v K" unfolding GK 
        by (rule v_sameprod, unfold GK, insert k2, auto)
      finally have "Gs  G" unfolding Gs_def GK
        by (intro sameprod_mono)
      with D DU have "D  ?U" "?New  G" by (auto)
      hence "Y  G" unfolding accepts_def Y by auto 
      thus ?thesis using G by auto
    qed
  }
  thus "POS  ACC X  ACC Y" by auto

  from ex_bij_betw_nat_finite[OF finS, unfolded card S = p]
  obtain Si where Si: "bij_betw Si {0 ..< p} S" by auto
  define G where "G = (λ i. SOME Gb. Gb  X  v Gb = Si i)" 
  {
    fix i
    assume "i < p" 
    with Si have SiS: "Si i  S" unfolding bij_betw_def by auto
    with S have "Si i  v_gs X" by auto
    hence " G. G  X  v G = Si i" 
      unfolding v_gs_def by auto
    from someI_ex[OF this] 
    have "(G i)  X  v (G i) = Si i" 
      unfolding G_def by blast
    hence "G i  X" "v (G i) = Si i" 
      "G i  U" "v (G i)  S" using SiS unfolding U_def 
      by auto
  } note G = this
  have SvG: "S = v ` G ` {0 ..< p}" unfolding Si[unfolded bij_betw_def, 
        THEN conjunct2, symmetric] image_comp o_def using G(2) by auto
  have injG: "inj_on G {0 ..< p}" 
  proof (standard, goal_cases)
    case (1 i j)
    hence "Si i = Si j" using G[of i] G[of j] by simp
    with 1(1,2) Si show "i = j"  
      by (metis Si bij_betw_iff_bijections)
  qed
  define r where "r = card U" 
  have rq: "r  p" unfolding r_def card S = p[symmetric] vplus_dsU[symmetric]
    unfolding v_gs_def
    by (rule card_image_le[OF finU])

  let ?Vi = "λ i. v (G i)"
  let ?Vis = "λ i. ?Vi i - Vs"
  define s where "s = card Vs" 
  define si where "si i = card (?Vi i)" for i
  define ti where "ti i = card (?Vis i)" for i
  {
    fix i
    assume i: "i < p" 
    have Vs_Vi: "Vs  ?Vi i" using i unfolding Vs_def 
      using G[OF i] unfolding SvG by auto
    have finVi: "finite (?Vi i)"  
      using G(4)[OF i] S(1) sf_precond
      by (meson finite_numbers finite_subset subset_eq)
    from S(1) have "G i  𝒢" using G(1)[OF i] X unfolding 𝒢l_def 𝒢_def 𝒢l_def by auto
    hence finGi: "finite (G i)"
      using finite_members_𝒢 by auto
    have ti: "ti i = si i - s" unfolding ti_def si_def s_def
      by (rule card_Diff_subset[OF fin_Vs Vs_Vi])
    have size1: "s  si i" unfolding s_def si_def
      by (intro card_mono finVi Vs_Vi)
    have size2: "si i  l" unfolding si_def using G(4)[OF i] S(1) sf_precond by auto
    note Vs_Vi finVi ti size1 size2 finGi G i  𝒢
  } note i_props = this
  define fstt where "fstt e = (SOME x. x  e  x  Vs)" for e
  define sndd where "sndd e = (SOME x. x  e  x  fstt e)" for e
  {
    fix e :: "nat set" 
    assume *: "card e = 2" "¬ e  Vs" 
    from *(1) obtain x y where e: "e = {x,y}" "x  y" 
      by (meson card_2_iff)
    with * have " x. x  e  x  Vs" by auto
    from someI_ex[OF this, folded fstt_def]
    have fst: "fstt e  e" "fstt e  Vs" by auto
    with * e have " x. x  e  x  fstt e"
      by (metis insertCI)
    from someI_ex[OF this, folded sndd_def] have snd: "sndd e  e" "sndd e  fstt e" by auto
    from fst snd e have "{fstt e, sndd e} = e" "fstt e  Vs" "fstt e  sndd e" by auto
  } note fstt = this
  {
    fix f
    assume "f  ACC_cf Y - ACC_cf X" 
    hence fake: "f  ACC_cf {?New} - ACC_cf U" unfolding Y ACC_cf_def accepts_def 
      Diff_iff U_def Un_iff mem_Collect_eq by blast
    hence f: "f  " using ACC_cf_ℱ by auto
    hence "C f  NEG" unfolding NEG_def by auto
    with NEG_𝒢 have Cf: "C f  𝒢" by auto
    from fake have "f  ACC_cf {?New}" by auto
    from this[unfolded ACC_cf_def accepts_def] Cf
    have GsCf: "Gs  C f" and Cf: "C f  𝒢" by auto
    from fake have "f  ACC_cf U" by auto
    from this[unfolded ACC_cf_def] Cf f have "¬ (U  C f)" by auto
    from this[unfolded accepts_def] 
    have UCf: "D  U  ¬ D  C f" for D by auto
    let ?prop = "λ i e. fstt e  v (G i) - Vs  
           sndd e  v (G i)  e  G i  ([m]^𝟮)
          f (fstt e) = f (sndd e)  f (sndd e)  [k - 1]  {fstt e, sndd e} = e" 
    define pair where "pair i = (if i < p then (SOME pair. ?prop i pair) else undefined)" for i 
    define u where "u i = fstt (pair i)" for i
    define w where "w i = sndd (pair i)" for i
    {
      fix i
      assume i: "i < p" 
      from i have "?Vi i  S" unfolding SvG by auto
      hence "Vs  ?Vi i" unfolding Vs_def by auto
      from sameprod_mono[OF this, folded Gs_def] 
      have *: "Gs  v (G i)^𝟮" .  
      from i have Gi: "G i  U" using G[OF i] by auto
      from UCf[OF Gi] i_props[OF i] have "¬ G i  C f" and Gi: "G i  𝒢" by auto
      then obtain edge where 
        edgep: "edge  G i" and edgen: "edge  C f" by auto
      from edgep Gi obtain x y where edge: "edge = {x,y}" 
        and xy: "{x,y}  [m]^𝟮" "{x,y}  [m]" "card {x,y} = 2" unfolding 𝒢_def binprod_def
        by force        
      define a where "a = fstt edge" 
      define b where "b = sndd edge" 
      from edgen[unfolded C_def edge] xy have id: "f x = f y" by simp
      from edgen GsCf edge have edgen: "{x,y}  Gs" by auto
      from edgen[unfolded Gs_def sameprod_altdef] xy have "¬ {x,y}  Vs" by auto
      from fstt[OF card {x,y} = 2 this, folded edge, folded a_def b_def] edge
      have  a: "a  Vs" and id_ab: "{x,y} = {a,b}" by auto
      from id_ab id have id: "f a = f b" by (auto simp: doubleton_eq_iff)
      let ?pair = "(a,b)" 
      note ab = xy[unfolded id_ab]
      from f[unfolded ℱ_def] ab have fb: "f b  [k - 1]" by auto
      note edge = edge[unfolded id_ab]
      from edgep[unfolded edge] v_mem_sub[OF card {a,b} = 2, of "G i"] id
      have "?prop i edge" using edge ab a fb unfolding a_def b_def by auto
      from someI[of "?prop i", OF this] have "?prop i (pair i)" using i unfolding pair_def by auto
      from this[folded u_def w_def] edgep
      have "u i  v (G i) - Vs" "w i  v (G i)" "pair i  G i  [m]^𝟮" 
        "f (u i) = f (w i)" "f (w i)  [k - 1]" "pair i = {u i, w i}" 
        by auto
    } note uw = this
    from uw(3) have Pi: "pair  PiE {0 ..< p} G" unfolding pair_def by auto
    define Us where "Us = u ` {0 ..< p}" 
    define Ws where "Ws = [m] - Us"
    {
      fix i
      assume i: "i < p"
      note uwi = uw[OF this]
      from uwi have ex: " x  [k - 1]. f ` {u i, w i} = {x}" by auto
      from uwi have *: "u i  [m]" "w i  [m]" "{u i, w i}  G i" by (auto simp: sameprod_altdef)
      have "w i  Us" 
      proof
        assume "w i  Us" 
        then obtain j where j: "j < p" and wij: "w i = u j" unfolding Us_def by auto
        with uwi have ij: "i  j" unfolding binprod_def by auto
        note uwj = uw[OF j]
        from ij i j Si[unfolded bij_betw_def] 
        have diff: "v (G i)  v (G j)" unfolding G(2)[OF i] G(2)[OF j] inj_on_def by auto      
        from uwi wij have uj: "u j  v (G i)" by auto
        with sunflower S[unfolded sunflower_def, rule_format] G(4)[OF i] G(4)[OF j] uwj(1) diff
        have "u j   S" by blast
        with uwj(1)[unfolded Vs_def] show False by simp
      qed
      with * have wi: "w i  Ws" unfolding Ws_def by auto
      from uwi have wi2: "w i  v (G i)" by auto
      define W where "W = Ws  v (G i)" 
      from G(1)[OF i] X[unfolded 𝒢l_def 𝒢l_def] i_props[OF i] 
      have "finite (v (G i))" "card (v (G i))  l" by auto
      with card_mono[OF this(1), of W] have 
        W: "finite W" "card W  l" "W  [m] - Us" unfolding W_def Ws_def by auto
      from wi wi2 have wi: "w i  W" unfolding W_def by auto
      from wi ex W * have "{u i, w i}  G i  u i  [m]  w i  [m] - Us  f (u i) = f (w i)" by force
    } note uw1 = this
    have inj: "inj_on u {0 ..< p}" 
    proof -
      {
        fix i j
        assume i: "i < p" and j: "j < p" 
          and id: "u i = u j" and ij: "i  j" 
        from ij i j Si[unfolded bij_betw_def] 
        have diff: "v (G i)  v (G j)" unfolding G(2)[OF i] G(2)[OF j] inj_on_def by auto      
        from uw[OF i] have ui: "u i  v (G i) - Vs" by auto
        from uw[OF j, folded id] have uj: "u i  v (G j)" by auto
        with sunflower S[unfolded sunflower_def, rule_format] G(4)[OF i] G(4)[OF j] uw[OF i] diff
        have "u i   S" by blast
        with ui have False unfolding Vs_def by auto
      }
      thus ?thesis unfolding inj_on_def by fastforce
    qed
    have card: "card ([m] - Us) = m - p" 
    proof (subst card_Diff_subset)
      show "finite Us" unfolding Us_def by auto
      show "Us  [m]" unfolding Us_def using uw1 by auto
      have "card Us = p" unfolding Us_def using inj
        by (simp add: card_image)
      thus "card [m] - card Us = m - p" by simp
    qed
    hence "( i < p. pair i  G i)  inj_on u {0 ..< p}  ( i < p. w i  [m] - u ` {0 ..< p}  f (u i) = f (w i))" 
      using inj uw1 uw unfolding Us_def by auto
    from this[unfolded u_def w_def] Pi card[unfolded Us_def u_def w_def]
    have " e  PiE {0..<p} G. (i<p. e i  G i) 
      card ([m] - (λi. fstt (e i)) ` {0..<p}) = m - p 
      (i<p. sndd (e i)  [m] - (λi. fstt (e i)) ` {0..<p}  f (fstt (e i)) = f (sndd (e i)))" 
      by blast
  } note fMem = this
  define Pi2 where "Pi2 W = PiE ([m] - W) (λ _. [k - 1])" for W
  define merge where "merge = 
    (λ e  (g :: nat  nat) v. if v  (λ i. fstt (e i)) ` {0 ..< p} then g (sndd (e (SOME i. i < p  v = fstt (e i)))) else g v)"     
  let ?W = "λ e. (λ i. fstt (e i)) ` {0..<p}" 
  have "ACC_cf Y - ACC_cf X  { merge e g | e g. e  PiE {0..<p} G  card ([m] - ?W e) = m - p  g  Pi2 (?W e)}"
    (is "_  ?R")
  proof
    fix f
    assume mem: "f  ACC_cf Y - ACC_cf X" 
    with ACC_cf_ℱ have "f  " by auto
    hence f: "f  [m] E [k - 1]" unfolding ℱ_def .
    from fMem[OF mem] obtain e where e: "e  PiE {0..<p} G" 
     " i. i<p  e i  G i" 
     "card ([m] - ?W e) = m - p" 
     " i. i<p  sndd (e i)  [m] - ?W e  f (fstt (e i)) = f (sndd (e i))" by auto
    define W where "W = ?W e" 
    note e = e[folded W_def]
    let ?g = "restrict f ([m] - W)" 
    let ?h = "merge e ?g" 
    have "f  ?R"
    proof (intro CollectI exI[of _ e] exI[of _ ?g], unfold W_def[symmetric], intro conjI e)
      show "?g  Pi2 W" unfolding Pi2_def using f by auto
      {
        fix v :: nat
        have "?h v = f v" 
        proof (cases "v  W")
          case False
          thus ?thesis using f unfolding merge_def unfolding W_def[symmetric] by auto
        next
          case True
          from this[unfolded W_def] obtain i where i: "i < p" and v: "v = fstt (e i)" by auto
          define j where "j = (SOME j. j < p  v = fstt (e j))" 
          from i v have " j. j < p  v = fstt (e j)" by auto
          from someI_ex[OF this, folded j_def] have j: "j < p" and v: "v = fstt (e j)" by auto
          have "?h v = restrict f ([m] - W) (sndd (e j))" 
            unfolding merge_def unfolding W_def[symmetric] j_def using True by auto
          also have " = f (sndd (e j))" using e(4)[OF j] by auto
          also have " = f (fstt (e j))" using e(4)[OF j] by auto
          also have " = f v" using v by simp
          finally show ?thesis .
        qed
      }
      thus "f = ?h" by auto
    qed
    thus "f  ?R" by auto
  qed
  also have "  (λ (e,g). (merge e g)) ` (Sigma (PiE {0..<p} G  {e. card ([m] - ?W e) = m - p}) (λ e. Pi2 (?W e)))" 
    (is "_  ?f ` ?R")
    by auto
  finally have sub: "ACC_cf Y - ACC_cf X  ?f ` ?R" .
  have fin[simp,intro]: "finite [m]" "finite [k - Suc 0]" unfolding numbers_def by auto
  have finPie[simp, intro]: "finite (PiE {0..<p} G)" 
    by (intro finite_PiE, auto intro: i_props)
  have finR: "finite ?R" unfolding Pi2_def
    by (intro finite_SigmaI finite_Int allI finite_PiE i_props, auto)
  have "card (ACC_cf Y - ACC_cf X)  card (?f ` ?R)" 
    by (rule card_mono[OF finite_imageI[OF finR] sub])
  also have "  card ?R" 
    by (rule card_image_le[OF finR])
  also have " = (e(PiE {0..<p} G  {e. card ([m] - ?W e) = m - p}). card (Pi2 (?W e)))" 
    by (rule card_SigmaI, unfold Pi2_def,
    (intro finite_SigmaI allI finite_Int finite_PiE i_props, auto)+)
  also have " = (ePiE {0..<p} G  {e. card ([m] - ?W e) = m - p}. (k - 1) ^ (card ([m] - ?W e)))" 
    by (rule sum.cong[OF refl], unfold Pi2_def, subst card_PiE, auto)
  also have " = (ePiE {0..<p} G  {e. card ([m] - ?W e) = m - p}. (k - 1) ^ (m - p))" 
    by (rule sum.cong[OF refl], rule arg_cong[of _ _ "λ n. (k - 1)^n"], auto)
  also have "  (ePiE {0..<p} G. (k - 1) ^ (m - p))" 
    by (rule sum_mono2, auto)
  also have " = card (PiE {0..<p} G) * (k - 1) ^ (m - p)" by simp
  also have " = (i = 0..<p. card (G i)) * (k - 1) ^ (m - p)"
    by (subst card_PiE, auto)
  also have "  (i = 0..<p. (k - 1) div 2) * (k - 1) ^ (m - p)"
  proof - 
    {
      fix i
      assume i: "i < p" 
      from G[OF i] X
      have GiG: "G i  𝒢"
        unfolding 𝒢l_def 𝒢_def 𝒢_def sameprod_altdef by force
      from i_props[OF i] have finGi: "finite (G i)" by auto
      have finvGi: "finite (v (G i))" by (rule finite_vG, insert i_props[OF i], auto)
      have "card (G i)  card ((v (G i))^𝟮)" 
        by (intro card_mono[OF sameprod_finite], rule finvGi, rule v_𝒢_2[OF GiG])
      also have "  l choose 2"
      proof (subst card_sameprod[OF finvGi], rule choose_mono)
        show "card (v (G i))  l" using i_props[OF i] unfolding ti_def si_def by simp
      qed
      also have "l choose 2 = l * (l - 1) div 2" unfolding choose_two by simp
      also have "l * (l - 1) = k - l" unfolding kl2 power2_eq_square by (simp add: algebra_simps)
      also have " div 2  (k - 1) div 2" 
        by (rule div_le_mono, insert l2, auto)    
      finally have "card (G i)  (k - 1) div 2" .
    } 
    thus ?thesis by (intro mult_right_mono prod_mono, auto)
  qed
  also have " = ((k - 1) div 2) ^ p * (k - 1) ^ (m - p)" 
    by simp
  also have "  ((k - 1) ^ p div (2^p)) * (k - 1) ^ (m - p)" 
    by (rule mult_right_mono; auto simp: div_mult_pow_le)
  also have "  ((k - 1) ^ p * (k - 1) ^ (m - p)) div 2^p" 
    by (rule div_mult_le)
  also have " = (k - 1)^m div 2^p"  
  proof - 
    have "p + (m - p) = m" using mp by simp
    thus ?thesis by (subst power_add[symmetric], simp)
  qed
  finally have "card (ACC_cf Y - ACC_cf X)  (k - 1) ^ m div 2 ^ p" .
  hence "2 ^ p * card (ACC_cf Y - ACC_cf X)  2^p * ((k - 1) ^ m div 2 ^ p)" by simp
  also have "  (k - 1)^m"  by simp
  finally show "2^p * card (ACC_cf Y - ACC_cf X)  (k - 1) ^ m" .
qed


text Definition 6

function PLU_main :: "graph set  graph set × nat" where
  "PLU_main X = (if X  𝒢l  L < card (v_gs X) then
     map_prod id Suc (PLU_main (plucking_step X)) else
     (X, 0))"
  by pat_completeness auto

termination 
proof (relation "measure (λ X. card (v_gs X))", force, goal_cases)
  case (1 X)
  hence "X  𝒢l" and LL: "L < card (v_gs X)" by auto
  from plucking_step(1)[OF this refl]
  have "card (v_gs (plucking_step X))  card (v_gs X) - p + 1" .
  also have " < card (v_gs X)" using p L3 LL
    by auto
  finally show ?case by simp
qed

declare PLU_main.simps[simp del]

definition PLU :: "graph set  graph set" where
  "PLU X = fst (PLU_main X)" 

text Lemma 7

lemma PLU_main_n: assumes "X  𝒢l" and "PLU_main X = (Z, n)" 
  shows "n * (p - 1)  card (v_gs X)" 
  using assms 
proof (induct X  arbitrary: Z n  rule: PLU_main.induct)
  case (1 X Z n)
  note [simp] = PLU_main.simps[of X]
  show ?case
  proof (cases "card (v_gs X)  L")
    case True
    thus ?thesis using 1 by auto
  next
    case False
    define Y where "Y = plucking_step X" 
    obtain q where PLU: "PLU_main Y = (Z, q)" and n: "n = Suc q" 
      using PLU_main X = (Z,n)[unfolded PLU_main.simps[of X], folded Y_def] using False 1(2) by (cases "PLU_main Y", auto)    
    from False have L: "card (v_gs X) > L" by auto
    note step = plucking_step[OF 1(2) this Y_def]
    from False 1 have "X  𝒢l  L < card (v_gs X)" by auto
    note IH = 1(1)[folded Y_def, OF this step(2) PLU]
    have "n * (p - 1) = (p - 1) + q * (p - 1)" unfolding n by simp
    also have "  (p - 1) + card (v_gs Y)" using IH by simp
    also have "  p - 1 + (card (v_gs X) - p + 1)" using step(1) by simp
    also have " = card (v_gs X)" using L Lp p by simp
    finally show ?thesis .
  qed
qed

text Definition 8

definition sqcup :: "graph set  graph set  graph set" (infixl "" 65) where
  "X  Y = PLU (X  Y)" 

definition sqcap :: "graph set  graph set  graph set" (infixl "" 65) where
  "X  Y = PLU (X ⊙l Y)" 

definition deviate_pos_cup :: "graph set  graph set  graph set" ("∂⊔Pos") where
  "∂⊔Pos X Y = POS  ACC (X  Y) - ACC (X  Y)" 

definition deviate_pos_cap :: "graph set  graph set  graph set" ("∂⊓Pos") where
  "∂⊓Pos X Y = POS  ACC (X  Y) - ACC (X  Y)" 

definition deviate_neg_cup :: "graph set  graph set  colorf set" ("∂⊔Neg") where
  "∂⊔Neg X Y = ACC_cf (X  Y) - ACC_cf (X  Y)" 

definition deviate_neg_cap :: "graph set  graph set  colorf set" ("∂⊓Neg") where
  "∂⊓Neg X Y = ACC_cf (X  Y) - ACC_cf (X  Y)" 

text Lemma 9 -- without applying Lemma 7

lemma PLU_main: assumes "X  𝒢l" 
  and "PLU_main X = (Z, n)" 
shows "Z  𝒫L𝒢l
   (Z = {}  X = {})
   POS  ACC X  ACC Z
   2 ^ p * card (ACC_cf Z - ACC_cf X)  (k - 1) ^ m * n" 
  using assms
proof (induct X  arbitrary: Z n  rule: PLU_main.induct)
  case (1 X Z n)
  note [simp] = PLU_main.simps[of X]
  show ?case
  proof (cases "card (v_gs X)  L")
    case True
    from True show ?thesis using 1 by (auto simp: id 𝒫L𝒢l_def)
  next
    case False
    define Y where "Y = plucking_step X" 
    obtain q where PLU: "PLU_main Y = (Z, q)" and n: "n = Suc q" 
      using PLU_main X = (Z,n)[unfolded PLU_main.simps[of X], folded Y_def] using False 1(2) by (cases "PLU_main Y", auto)    
    from False have "card (v_gs X) > L" by auto
    note step = plucking_step[OF 1(2) this Y_def]
    from False 1 have "X  𝒢l  L < card (v_gs X)" by auto
    note IH = 1(1)[folded Y_def, OF this step(2) PLU] Y  {}
    let ?Diff = "λ X Y. ACC_cf X - ACC_cf Y" 
    have finNEG: "finite NEG"
      using NEG_𝒢 infinite_super by blast
    have "?Diff Z X  ?Diff Z Y  ?Diff Y X" by auto
    from card_mono[OF finite_subset[OF _ finite_ℱ] this] ACC_cf_ℱ
    have "2 ^ p * card (?Diff Z X)  2 ^ p * card (?Diff Z Y  ?Diff Y X)" by auto
    also have "  2 ^ p * (card (?Diff Z Y) + card (?Diff Y X))" 
      by (rule mult_left_mono, rule card_Un_le, simp)
    also have " = 2 ^ p * card (?Diff Z Y) + 2 ^ p * card (?Diff Y X)" 
      by (simp add: algebra_simps)
    also have "  ((k - 1) ^ m) * q + (k - 1) ^ m" using IH step by auto
    also have " = ((k - 1) ^ m) * Suc q" by (simp add: ac_simps)
    finally have c: "2 ^ p * card (ACC_cf Z - ACC_cf X)  ((k - 1) ^ m) * Suc q" by simp
    from False have "X  {}" by auto
    thus ?thesis unfolding n using IH step c by auto
  qed
qed

text Lemma 9

lemma assumes X: "X  𝒫L𝒢l" and Y: "Y  𝒫L𝒢l"
  shows PLU_union: "PLU (X  Y)  𝒫L𝒢l" and
  sqcup: "X  Y  𝒫L𝒢l" and
  sqcup_sub: "POS  ACC (X  Y)  ACC (X  Y)" and
  deviate_pos_cup: "∂⊔Pos X Y = {}" and
  deviate_neg_cup: "card (∂⊔Neg X Y) < (k - 1)^m * L / 2^(p - 1)" 
proof -
  obtain Z n where res: "PLU_main (X  Y) = (Z, n)" by force
  hence PLU: "PLU (X  Y) = Z" unfolding PLU_def by simp
  from X Y have XY: "X  Y  𝒢l" unfolding 𝒫L𝒢l_def by auto
  note main = PLU_main[OF this(1) res]
  from main show "PLU (X  Y)  𝒫L𝒢l" unfolding PLU by simp
  thus "X  Y  𝒫L𝒢l" unfolding sqcup_def .
  from main show "POS  ACC (X  Y)  ACC (X  Y)" 
    unfolding sqcup_def PLU by simp
  thus "∂⊔Pos X Y = {}" unfolding deviate_pos_cup_def PLU sqcup_def by auto
  have "card (v_gs (X  Y))  card (v_gs X) + card (v_gs Y)" 
    unfolding v_gs_union by (rule card_Un_le)
  also have "  L + L" using X Y unfolding 𝒫L𝒢l_def by simp
  finally have "card (v_gs (X  Y))  2 * L" by simp
  with PLU_main_n[OF XY(1) res] have "n * (p - 1)  2 * L" by simp
  with p Lm m2 have n: "n < 2 * L" by (cases n, auto, cases "p - 1", auto)
  let ?r = real
  have *: "(k - 1) ^ m > 0" using k l2 by simp
  have "2 ^ p * card (∂⊔Neg X Y)  2 ^ p * card (ACC_cf Z - ACC_cf (X  Y))" unfolding deviate_neg_cup_def PLU sqcup_def
    by (rule mult_left_mono, rule card_mono[OF finite_subset[OF _ finite_ℱ]], insert ACC_cf_ℱ, force, auto)
  also have "  (k - 1) ^ m * n" using main by simp
  also have " < (k - 1) ^ m * (2 * L)" unfolding mult_less_cancel1 using n * by simp
  also have " = 2 * ((k - 1) ^ m * L)" by simp
  finally have "2 * (2^(p - 1) * card (∂⊔Neg X Y)) < 2 * ((k - 1) ^ m * L)" using p by (cases p, auto)
  hence "2 ^ (p - 1) * card (∂⊔Neg X Y) < (k - 1)^m * L" by simp
  hence "?r (2 ^ (p - 1) * card (∂⊔Neg X Y)) < ?r ((k - 1)^m * L)" by linarith
  thus "card (∂⊔Neg X Y) < (k - 1)^m * L / 2^(p - 1)" by (simp add: field_simps)
qed

text Lemma 10

lemma assumes X: "X  𝒫L𝒢l" and Y: "Y  𝒫L𝒢l"
  shows PLU_joinl: "PLU (X ⊙l Y)  𝒫L𝒢l" and
  sqcap: "X  Y  𝒫L𝒢l" and
  deviate_neg_cap: "card (∂⊓Neg X Y) < (k - 1)^m * L^2 / 2^(p - 1)" and
  deviate_pos_cap: "card (∂⊓Pos X Y)  ((m - l - 1) choose (k - l - 1)) * L^2" 
proof -
  obtain Z n where res: "PLU_main (X ⊙l Y) = (Z, n)" by force
  hence PLU: "PLU (X ⊙l Y) = Z" unfolding PLU_def by simp
  from X Y have XY: "X  𝒢l" "Y  𝒢l" "X  𝒢" "Y  𝒢" unfolding 𝒫L𝒢l_def 𝒢l_def by auto  
  have sub: "X ⊙l Y  𝒢l" unfolding odotl_def using XY 
    by (auto split: option.splits)
  note main = PLU_main[OF sub res]
  note finV = finite_v_gs_Gl[OF XY(1)] finite_v_gs_Gl[OF XY(2)]
  have "X  Y  𝒢" by (rule odot_𝒢, insert XY, auto simp: 𝒢l_def) 
  hence XYD: "X  Y  𝒢" by auto
  have finvXY: "finite (v_gs (X  Y))" by (rule finite_v_gs[OF XYD])
  have "card (v_gs (X  Y))  card (v_gs X) * card (v_gs Y)" 
    using XY(1-2) by (intro card_v_gs_join, auto simp: 𝒢l_def)
  also have "  L * L" using X Y unfolding 𝒫L𝒢l_def 
    by (intro mult_mono, auto)
  also have " = L^2" by algebra
  finally have card_join: "card (v_gs (X  Y))  L^2" .
  with card_mono[OF finvXY v_gs_mono[OF joinl_join]]
  have card: "card (v_gs (X ⊙l Y))  L^2" by simp
  with PLU_main_n[OF sub res] have "n * (p - 1)  L^2" by simp
  with p Lm m2 have n: "n < 2 * L^2" by (cases n, auto, cases "p - 1", auto)
  have *: "(k - 1) ^ m > 0" using k l2 by simp
  show "PLU (X ⊙l Y)  𝒫L𝒢l" unfolding PLU using main by auto
  thus "X  Y  𝒫L𝒢l" unfolding sqcap_def .
  let ?r = real
  have "2^p * card (∂⊓Neg X Y)  2 ^ p * card (ACC_cf Z - ACC_cf (X ⊙l Y))"
    unfolding deviate_neg_cap_def PLU sqcap_def
    by (rule mult_left_mono, rule card_mono[OF finite_subset[OF _ finite_ℱ]], insert ACC_cf_ℱ, force, 
      insert ACC_cf_mono[OF joinl_join, of X Y], auto)
  also have "  (k - 1) ^ m * n" using main by simp
  also have " < (k - 1) ^ m * (2 * L^2)" unfolding mult_less_cancel1 using n * by simp
  finally have "2 * (2^(p - 1) * card (∂⊓Neg X Y)) < 2 * ((k - 1) ^ m * L^2)" using p by (cases p, auto)
  hence "2 ^ (p - 1) * card (∂⊓Neg X Y) < (k - 1)^m * L^2" by simp
  hence "?r (2 ^ (p - 1) * card (∂⊓Neg X Y)) < (k - 1)^m * L^2" by linarith
  thus "card (∂⊓Neg X Y) < (k - 1)^m * L^2 / 2^(p - 1)" by (simp add: field_simps)
  (* now for the next approximation *)
  define Vs where "Vs = v_gs (X  Y)  {V . V  [m]  card V  Suc l}" 
  define C where "C (V :: nat set) = (SOME C. C  V  card C = Suc l)" for V
  define K where "K C = { W. W  [m] - C  card W = k - Suc l }" for C
  define merge where "merge C V = (C  V)^𝟮" for C V :: "nat set" 
  define GS where "GS = { merge (C V) W | V W. V  Vs  W  K (C V)}"
  {
    fix V
    assume V: "V  Vs" 
    hence card: "card V  Suc l" and Vm: "V  [m]" unfolding Vs_def by auto
    from card obtain D where C: "D  V" and cardV: "card D = Suc l" 
      by (rule obtain_subset_with_card_n)
    hence " C. C  V  card C = Suc l" by blast
    from someI_ex[OF this, folded C_def] have *: "C V  V" "card (C V) = Suc l" 
      by blast+
    with Vm have sub: "C V  [m]" by auto
    from finite_subset[OF this] have finCV: "finite (C V)" unfolding numbers_def by simp
    have "card (K (C V)) = (m - Suc l) choose (k - Suc l