Theory MLSSmf_to_MLSS_Complexity

theory MLSSmf_to_MLSS_Complexity
  imports MLSSmf_to_MLSS
begin

definition sizem :: "('v, 'f) MLSSmf_clause ⇒ nat" where
  "sizem 𝒞 ≡ card (set 𝒞)"

lemma (in normalized_MLSSmf_clause) card_V_upper_bound:
  "card V ≤ 3 * sizem 𝒞"
  unfolding V_def
  using norm_𝒞
proof (induction 𝒞)
  case 1
  then show ?case by simp
next
  case (2 ls l)
  from ‹norm_literal l› have "card (varsm l) ≤ 3"
    by (cases l rule: norm_literal.cases) (auto simp: card_insert_if)
  with 2 show ?case
  proof (cases "l ∈ set ls")
    case True
    then have "varsm l ⊆ varsm ls" by blast
    moreover
    have "varsm (l # ls) = varsm l ∪ varsm ls" by auto
    ultimately
    have "varsm (l # ls) = varsm ls" by blast
    then have "card (varsm (l # ls)) = card (varsm ls)" by argo
    moreover
    from True have "sizem (l # ls) = sizem ls"
      unfolding sizem_def
      by (simp add: insert_absorb)
    ultimately
    show ?thesis using "2.IH" by argo
  next
    case False
    have "varsm (l # ls) = varsm l ∪ varsm ls" by auto
    then have "card (varsm (l # ls)) ≤ card (varsm l) + card (varsm ls)"
      by (simp add: card_Un_le)
    with ‹card (varsm l) ≤ 3› "2.IH"
    have "card (varsm (l # ls)) ≤ 3 * (Suc (sizem ls))"
      by simp
    moreover
    from False have "sizem (l # ls) = Suc (sizem ls)"
      unfolding sizem_def by simp
    ultimately
    show ?thesis by argo
  qed
qed

lemma (in normalized_MLSSmf_clause) card_F_upper_bound:
  "card F ≤ 2 * sizem 𝒞"
  unfolding F_def
  using norm_𝒞
proof (induction 𝒞)
  case 1
  then show ?case by simp
next
  case (2 ls l)
  from ‹norm_literal l› have "card (funsm l) ≤ 2"
    by (cases l rule: norm_literal.cases) (auto simp: card_insert_if)
  with 2 show ?case
  proof (cases "l ∈ set ls")
    case True
    then have "funsm l ⊆ funsm ls" by blast
    moreover
    have "funsm (l # ls) = funsm l ∪ funsm ls" by auto
    ultimately
    have "funsm (l # ls) = funsm ls" by blast
    then have "card (funsm (l # ls)) = card (funsm ls)" by argo
    moreover
    from True have "sizem (l # ls) = sizem ls"
      unfolding sizem_def
      by (simp add: insert_absorb)
    ultimately
    show ?thesis using "2.IH" by argo
  next
    case False
    have "funsm (l # ls) = funsm l ∪ funsm ls" by auto
    then have "card (funsm (l # ls)) ≤ card (funsm l) + card (funsm ls)"
      by (simp add: card_Un_le)
    with ‹card (funsm l) ≤ 2› "2.IH"
    have "card (funsm (l # ls)) ≤ 2 * (Suc (sizem ls))"
      by simp
    moreover
    from False have "sizem (l # ls) = Suc (sizem ls)"
      unfolding sizem_def by simp
    ultimately
    show ?thesis by argo
  qed
qed

lemma (in normalized_MLSSmf_clause) size_restriction_on_InterOfVars:
  "card (restriction_on_InterOfVars vs) ≤ 2 * length vs"
proof (induction vs rule: restriction_on_InterOfVars.induct)
  case (3 x v vs)
  have "length zs > length ys ⟹ InterOfVarsAux zs ∉ ⋃ (vars ` restriction_on_InterOfVars ys)"
    for y ys zs
    by (induction ys rule: restriction_on_InterOfVars.induct) auto
  then have "InterOfVarsAux (x # v # vs) ∉ ⋃ (vars ` restriction_on_InterOfVars (v # vs))"
    by force
  then have "Var (InterOfVarsAux (x # v # vs)) =s Var (Solo x) -s Var (InterOfVars (v # vs)) ∉ restriction_on_InterOfVars (v # vs)"
            "Var (InterOfVars (x # v # vs)) =s Var (Solo x) -s Var (InterOfVarsAux (x # v # vs)) ∉ restriction_on_InterOfVars (v # vs)"
    by auto
  then have "card (restriction_on_InterOfVars (x # v # vs)) = Suc (Suc (card (restriction_on_InterOfVars (v # vs))))"
    using restriction_on_InterOfVar_finite by force
  with "3.IH" show ?case by simp
qed simp+

lemma (in normalized_MLSSmf_clause) size_restriction_on_UnionOfVars:
  "card (restriction_on_UnionOfVars vs) ≤ Suc (length vs)"
  apply (induction vs rule: restriction_on_UnionOfVars.induct)
   apply simp
  by (simp add: card_insert_if restriction_on_UnionOfVar_finite)

theorem (in normalized_MLSSmf_clause) size_introduce_v:
  "card introduce_v ≤ (3 * card V + 2) * (2 ^ card V)"
proof -
  have "card (restriction_on_v ` P+ V) ≤ card (P+ V)"
    using P_plus_finite card_image_le by blast
  then have 1: "card (restriction_on_v ` P+ V) ≤ card (Pow V)"
    by simp

  have "card ((restriction_on_InterOfVars ∘ var_set_to_list) α) ≤ 2 * card V" for α
  proof -
    have "length (var_set_to_list α) ≤ length V_list" by simp
    then have "length (var_set_to_list α) ≤ card V"
      unfolding V_list_def
      by (metis V_list_def distinct_V_list distinct_card set_V_list)
    with size_restriction_on_InterOfVars[of "var_set_to_list α"]
    have "card (restriction_on_InterOfVars (var_set_to_list α)) ≤ 2 * card V"
      by linarith
    then show ?thesis by fastforce
  qed
  then have "(∑α∈P+ V. card ((restriction_on_InterOfVars ∘ var_set_to_list) α)) ≤ 2 * card V * card (P+ V)"
    by (smt (verit) card_eq_sum nat_mult_1_right sum_distrib_left sum_mono)
  moreover  
  from card_UN_le[where ?I = "P+ V" and ?A = "restriction_on_InterOfVars ∘ var_set_to_list"]
  have "card (⋃ ((restriction_on_InterOfVars ∘ var_set_to_list) ` P+ V)) ≤
        (∑α∈P+ V. card ((restriction_on_InterOfVars ∘ var_set_to_list) α))"
    using P_plus_finite finite_V by blast
  ultimately
  have "card (⋃ ((restriction_on_InterOfVars ∘ var_set_to_list) ` P+ V)) ≤ 2 * card V * card (P+ V)"
    by linarith
  also have "... ≤ 2 * card V * card (Pow V)" by simp
  finally have 2: "card (⋃ ((restriction_on_InterOfVars ∘ var_set_to_list) ` P+ V)) ≤ 2 * card V * card (Pow V)"
    by blast

  have "card ((restriction_on_UnionOfVars ∘ var_set_to_list) α) ≤ Suc (card V)" for α
  proof -
    have "length (var_set_to_list α) ≤ length V_list" by simp
    then have "length (var_set_to_list α) ≤ card V"
      unfolding V_list_def
      by (metis V_list_def distinct_V_list distinct_card set_V_list)
    with size_restriction_on_UnionOfVars[of "var_set_to_list α"]
    have "card (restriction_on_UnionOfVars (var_set_to_list α)) ≤ Suc (card V)"
      by linarith
    then show ?thesis by fastforce
  qed
  then have "(∑α∈Pow V. card ((restriction_on_UnionOfVars ∘ var_set_to_list) α)) ≤ Suc (card V) * card (Pow V)"
    by (smt (verit) card_eq_sum nat_mult_1_right sum_distrib_left sum_mono)
  moreover  
  from card_UN_le[where ?I = "Pow V" and ?A = "restriction_on_UnionOfVars ∘ var_set_to_list"]
  have "card (⋃ ((restriction_on_UnionOfVars ∘ var_set_to_list) ` Pow V)) ≤
        (∑α∈Pow V. card ((restriction_on_UnionOfVars ∘ var_set_to_list) α))"
    using finite_V by blast
  ultimately
  have 3: "card (⋃ ((restriction_on_UnionOfVars ∘ var_set_to_list) ` Pow V)) ≤ Suc (card V) * card (Pow V)"
    by linarith

  let ?atoms = "restriction_on_v ` P+ V ∪
        ⋃ ((restriction_on_InterOfVars ∘ var_set_to_list) ` P+ V) ∪
        ⋃ ((restriction_on_UnionOfVars ∘ var_set_to_list) ` Pow V)"
  from restriction_on_InterOfVar_finite restriction_on_UnionOfVar_finite
  have "finite ?atoms" using finite_V by auto
  then have "card introduce_v ≤ card ?atoms"
    unfolding introduce_v_def
    using card_image_le by meson
  also have "... ≤ card (restriction_on_v ` P+ V) +
              card (⋃ ((restriction_on_InterOfVars ∘ var_set_to_list) ` P+ V)) +
              card (⋃ ((restriction_on_UnionOfVars ∘ var_set_to_list) ` Pow V))"
    using finite_V by (auto intro!: order.trans[OF card_Un_le])
  also have "... ≤ card (Pow V) +
              card (⋃ ((restriction_on_InterOfVars ∘ var_set_to_list) ` P+ V)) +
              card (⋃ ((restriction_on_UnionOfVars ∘ var_set_to_list) ` Pow V))"
    using 1 by linarith
  also have "... ≤ card (Pow V) + 2 * card V * card (Pow V) +
              card (⋃ ((restriction_on_UnionOfVars ∘ var_set_to_list) ` Pow V))"
    using 2 by linarith
  also have "... ≤ card (Pow V) + 2 * card V * card (Pow V) + Suc (card V) * card (Pow V)"
    using 3 by linarith
  also have "... = (1 + 2 * card V + Suc (card V)) * card (Pow V)"
    by algebra
  also have "... = (3 * card V + 2) * card (Pow V)"
    by simp
  also have "... = (3 * card V + 2) * (2 ^ card V)"
    using card_Pow finite_V by fastforce
  finally show ?thesis .
qed

lemma (in normalized_MLSSmf_clause) size_restriction_on_UnionOfVennRegions:
  "card (restriction_on_UnionOfVennRegions αs) ≤ Suc (length αs)"
  apply (induction αs rule: restriction_on_UnionOfVennRegions.induct)
   apply simp+
  by (metis add_mono_thms_linordered_semiring(2) card.infinite card_insert_if finite_insert le_SucI plus_1_eq_Suc)

lemma (in normalized_MLSSmf_clause) length_all_V_set_lists:
  "length all_V_set_lists = 2 ^ card (P+ V)"
  unfolding all_V_set_lists_def
  using length_subseqs set_V_set_list distinct_V_set_list distinct_card
  by force

lemma (in normalized_MLSSmf_clause) length_F_list:
  "length F_list = card F"
  unfolding F_list_def F_def
  by (auto simp add: length_remdups_card_conv)

lemma (in normalized_MLSSmf_clause) size_introduce_UnionOfVennRegions:
  "card introduce_UnionOfVennRegions ≤ Suc (2 ^ card V) * 2 ^ 2 ^ card V"
proof -
  have 1: "card (restriction_on_UnionOfVennRegions αs) ≤ Suc (2 ^ card V)"
    if "αs ∈ set all_V_set_lists" for αs
  proof -
    from that have "length αs ≤ length V_set_list"
      unfolding all_V_set_lists_def
      using length_subseq_le by blast
    then have "length αs ≤ card (P+ V)"
      by (metis distinct_V_set_list distinct_card set_V_set_list)
    then have "length αs ≤ 2 ^ card V"
      using card_Pow finite_V by fastforce
    with size_restriction_on_UnionOfVennRegions[of "αs"]
    have "card (restriction_on_UnionOfVennRegions αs) ≤ Suc (2 ^ card V)"
      by linarith
    then show ?thesis by fastforce
  qed

  from length_all_V_set_lists have "card (set all_V_set_lists) = 2 ^ card (P+ V)"
    using distinct_card distinct_all_V_set_lists by metis
  also have "... ≤ 2 ^ card (Pow V)" by auto
  also have "... = 2 ^ 2 ^ card V"
    using finite_V by (simp add: card_Pow)
  finally have 2: "card (set all_V_set_lists) ≤ 2 ^ 2 ^ card V".

  let ?atoms = "⋃ (restriction_on_UnionOfVennRegions ` set all_V_set_lists)"
  from AT_inj have "inj_on AT ?atoms"
    using inj_on_def by force
  from 1 have "(∑αs∈set all_V_set_lists. card (restriction_on_UnionOfVennRegions αs)) ≤
    Suc (2 ^ card V) * (card (set all_V_set_lists))"
    using Sum_le_times[where ?s = "set all_V_set_lists"
                         and ?f = "λαs. card (restriction_on_UnionOfVennRegions αs)"]
    by blast
  with 2 have "(∑αs∈set all_V_set_lists. card (restriction_on_UnionOfVennRegions αs)) ≤
    Suc (2 ^ card V) * 2 ^ 2 ^ card V"
    by (meson Suc_mult_le_cancel1 le_trans)
  moreover
  from card_UN_le[where ?I = "set all_V_set_lists" and ?A = "restriction_on_UnionOfVennRegions"]
  have "card ?atoms ≤ (∑αs∈set all_V_set_lists. card (restriction_on_UnionOfVennRegions αs))"
    by blast
  ultimately
  have "card ?atoms ≤ Suc (2 ^ card V) * 2 ^ 2 ^ card V"
    by linarith
  moreover
  from introduce_UnionOfVennRegions_normalized
  have "finite introduce_UnionOfVennRegions"
    unfolding normalized_MLSS_clause_def by blast
  then have "finite ?atoms"
    using finite_image_iff ‹inj_on AT ?atoms›
    unfolding introduce_UnionOfVennRegions_def by blast
  ultimately
  show ?thesis
    unfolding introduce_UnionOfVennRegions_def
    using card_image[where ?f = "AT" and ?A = ?atoms]
    using ‹inj_on AT ?atoms›
    by presburger
qed

lemma (in normalized_MLSSmf_clause) length_choices_from_lists:
  "∀choice ∈ set (choices_from_lists xss). length choice = length xss"
  by (induction xss) auto

lemma (in normalized_MLSSmf_clause) size_introduce_w:
  "∀clause ∈ introduce_w. card clause ≤ 2 ^ (2 * 2 ^ card V) * card F"
proof
  let ?xss = "map (λ(l, m, f). restriction_on_FunOfUnionOfVennRegions l m f)
                  (List.product all_V_set_lists (List.product all_V_set_lists F_list))"
  fix clause assume "clause ∈ introduce_w"
  then obtain choice where choice: "choice ∈ set (choices_from_lists ?xss)" "clause = set choice"
    unfolding introduce_w_def by auto
  then have "card clause ≤ length choice"
    using card_length by blast
  also have "length choice = length ?xss"
    using choice length_choices_from_lists by blast
  also have "... = length (List.product all_V_set_lists (List.product all_V_set_lists F_list))"
    by simp
  also have "... = length all_V_set_lists * length all_V_set_lists * length F_list"
    using length_product by auto
  also have "... = 2 ^ card (P+ V) * 2 ^ card (P+ V) * card F"
    using length_all_V_set_lists length_F_list by presburger
  also have "... = 2 ^ (2 * (card (P+ V))) * card F"
    by (simp add: mult_2 power_add)
  also have "... ≤ 2 ^ (2 * (card (Pow V))) * card F"
    by simp
  also have "... = 2 ^ (2 * 2 ^ card V) * card F"
    using card_Pow by auto
  finally show "card clause ≤ 2 ^ (2 * 2 ^ card V) * card F" .
qed

lemma (in normalized_MLSSmf_clause) card_P_P_V_ge_1:
  "card (Pow (P+ V) × Pow (P+ V)) ≥ 1"
proof -
  have "Pow (P+ V) ≠ {}" by blast
  then have "Pow (P+ V) × Pow (P+ V) ≠ {}" by blast
  moreover
  from finite_V P_plus_finite have "finite (Pow (P+ V))" by blast
  then have "finite (Pow (P+ V) × Pow (P+ V))" by blast
  ultimately
  have "card (Pow (P+ V) × Pow (P+ V)) > 0" by auto
  then show ?thesis by linarith
qed

lemma (in normalized_MLSSmf_clause) size_reduce_norm_literal:
  assumes "norm_literal lt"
    shows "card (reduce_literal lt) ≤ 2 * card (Pow (P+ V) × Pow (P+ V))"
  using assms
proof (cases lt rule: norm_literal.cases)
  case (inc f)
  let ?l = "λ(l, m). AT (Var w⇘f⇙⇘m⇙ =s Var w⇘f⇙⇘m⇙ ⊔s Var w⇘f⇙⇘l⇙)"
  from inc have "reduce_literal lt ⊆ ?l ` (Pow (P+ V) × Pow (P+ V))"
    by force
  then have "card (reduce_literal lt) ≤ card (Pow (P+ V) × Pow (P+ V))"
    by (meson finite_SigmaI finite_V pow_of_p_Plus_finite surj_card_le)
  also have "... ≤ 2 * card (Pow (P+ V) × Pow (P+ V))" by linarith
  finally show ?thesis .
next
  case (dec f)
  let ?l = "λ(l, m). AT (Var w⇘f⇙⇘l⇙ =s Var w⇘f⇙⇘l⇙ ⊔s Var w⇘f⇙⇘m⇙)"
  from dec have "reduce_literal lt ⊆ ?l ` (Pow (P+ V) × Pow (P+ V))"
    by force
  then have "card (reduce_literal lt) ≤ card (Pow (P+ V) × Pow (P+ V))"
    by (meson finite_SigmaI finite_V pow_of_p_Plus_finite surj_card_le)
  also have "... ≤ 2 * card (Pow (P+ V) × Pow (P+ V))" by linarith
  finally show ?thesis .
next
  case (add f)
  let ?l = "λ(l, m). AT (Var w⇘f⇙⇘l ∪ m⇙ =s Var w⇘f⇙⇘l⇙ ⊔s Var w⇘f⇙⇘m⇙)"
  from add have "reduce_literal lt ⊆ ?l ` (Pow (P+ V) × Pow (P+ V))"
    by force
  then have "card (reduce_literal lt) ≤ card (Pow (P+ V) × Pow (P+ V))"
    by (meson finite_SigmaI finite_V pow_of_p_Plus_finite surj_card_le)
  also have "... ≤ 2 * card (Pow (P+ V) × Pow (P+ V))" by linarith
  finally show ?thesis .
next
  case (mul f)
  let ?l1 = "λ(l, m). AT (Var (InterOfWAux f l m) =s Var w⇘f⇙⇘l⇙ -s Var w⇘f⇙⇘m⇙)"
  let ?l2 = "λ(l, m). AT (Var w⇘f⇙⇘l∩m⇙ =s Var w⇘f⇙⇘l⇙ -s Var (InterOfWAux f l m))"
  from mul have "reduce_literal lt ⊆ ?l1 ` (Pow (P+ V) × Pow (P+ V)) ∪ ?l2 ` (Pow (P+ V) × Pow (P+ V))"
    by force
  moreover
  have "?l1 ` (Pow (P+ V) × Pow (P+ V)) ∩ ?l2 ` (Pow (P+ V) × Pow (P+ V)) = {}"
    by fastforce
  moreover
  from finite_V P_plus_finite have "finite (Pow (P+ V) × Pow (P+ V))"
    by auto
  then have "finite (?l1 ` (Pow (P+ V) × Pow (P+ V)))" "finite (?l2 ` (Pow (P+ V) × Pow (P+ V)))"
    by blast+
  ultimately
  have "card (reduce_literal lt) ≤ card (?l1 ` (Pow (P+ V) × Pow (P+ V))) + card (?l2 ` (Pow (P+ V) × Pow (P+ V)))"
    using card_Un_disjoint[where ?A = "?l1 ` (Pow (P+ V) × Pow (P+ V))" and ?B = "?l2 ` (Pow (P+ V) × Pow (P+ V))"]
    using card_mono[where ?A = "reduce_literal lt" and ?B = "?l1 ` (Pow (P+ V) × Pow (P+ V)) ∪ ?l2 ` (Pow (P+ V) × Pow (P+ V))"]
    by fastforce
  also have "... ≤ card (Pow (P+ V) × Pow (P+ V)) + card (Pow (P+ V) × Pow (P+ V))"
    using card_image_le[where ?A = "Pow (P+ V) × Pow (P+ V)"]
    using ‹finite (Pow (P+ V) × Pow (P+ V))› add_mono by blast
  also have "... = 2 * card (Pow (P+ V) × Pow (P+ V))" by linarith
  finally show ?thesis .
next
  case (le f g)
  let ?l = "λl. AT (Var w⇘g⇙⇘l⇙ =s Var w⇘g⇙⇘l⇙ ⊔s Var w⇘f⇙⇘l⇙)"
  from le have "reduce_literal lt ⊆ ?l ` Pow (P+ V)"
    by force
  then have "card (reduce_literal lt) ≤ card (Pow (P+ V))"
    by (simp add: finite_V surj_card_le)
  also have "... ≤ card (Pow (P+ V) × Pow (P+ V))"
    by (simp add: finite_V surj_card_le)
  also have "... ≤ 2 * card (Pow (P+ V) × Pow (P+ V))"
    by linarith
  finally show ?thesis .
next
  case (eq x y)
  then have "card (reduce_literal lt) = 1" by simp
  with card_P_P_V_ge_1 show ?thesis by linarith
next
  case (eq_empty x n)
  then have "card (reduce_literal lt) = 1" by simp
  with card_P_P_V_ge_1 show ?thesis by linarith
next
  case (neq x y)
  then have "card (reduce_literal lt) = 1" by simp
  with card_P_P_V_ge_1 show ?thesis by linarith
next
  case (union x y z)
  then have "card (reduce_literal lt) = 1" by simp
  with card_P_P_V_ge_1 show ?thesis by linarith
next
  case (diff x y z)
  then have "card (reduce_literal lt) = 1" by simp
  with card_P_P_V_ge_1 show ?thesis by linarith
next
  case (single x y)
  then have "card (reduce_literal lt) = 1" by simp
  with card_P_P_V_ge_1 show ?thesis by linarith
next
  case (app x f y)
  then have "card (reduce_literal lt) = 1" by simp
  with card_P_P_V_ge_1 show ?thesis by linarith
qed

lemma (in normalized_MLSSmf_clause) size_reduce_clause:
  "card reduce_clause ≤ 2 ^ (Suc (2 * 2 ^ card V)) * sizem 𝒞"
proof -
  have "card (P+ V) ≤ 2 ^ card V"
    using card_Pow[of V] finite_V by simp
  from card_UN_le
  have "card reduce_clause ≤ (∑lt∈set 𝒞. card (reduce_literal lt))"
    using reduce_clause_finite
    unfolding reduce_clause_def
    by blast
  also have "... ≤ 2 * card (Pow (P+ V) × Pow (P+ V)) * card (set 𝒞)"
    using size_reduce_norm_literal norm_𝒞 literal_in_norm_clause_is_norm
    using Sum_le_times[where ?s = "set 𝒞" and ?f = "λlt. card (reduce_literal lt)"
                         and ?n = "2 * card (Pow (P+ V) × Pow (P+ V))"]
    by blast
  also have "... = 2 * card (Pow (P+ V)) * card (Pow (P+ V)) * card (set 𝒞)"
    using card_cartesian_product by auto
  also have "... = 2 * 2 ^ (card (P+ V)) * 2 ^ (card (P+ V)) * card (set 𝒞)"
    using card_Pow[of "P+ V"] finite_V P_plus_finite by fastforce
  also have "... ≤ 2 * 2 ^ (2 ^ card V) * 2 ^ (2 ^ card V) * card (set 𝒞)"
    using ‹card (P+ V) ≤ 2 ^ card V›
    using power_increasing_iff[where ?b = 2 and ?x = "card (P+ V)" and ?y = "2 ^ card V"]
    by (simp add: mult_le_mono)
  also have "... = 2 ^ (Suc (2 * 2 ^ card V)) * card (set 𝒞)"
    by (simp add: power2_eq_square power_even_eq)
  also have "... = 2 ^ (Suc (2 * 2 ^ card V)) * sizem 𝒞"
    unfolding sizem_def by blast
  finally show ?thesis .
qed

theorem (in normalized_MLSSmf_clause) size_reduced_dnf:
  "∀clause ∈ reduced_dnf. card clause ≤
    2 ^ (2 * 2 ^ (3 * sizem 𝒞)) * (2 * sizem 𝒞) +
    (3 * (3 * sizem 𝒞) + 2) * (2 ^ (3 * sizem 𝒞)) +
    Suc (2 ^ (3 * sizem 𝒞)) * 2 ^ 2 ^ (3 * sizem 𝒞) +
    2 ^ (Suc (2 * 2 ^ (3 * sizem 𝒞))) * sizem 𝒞"
proof -
  let ?upper_bound = "2 ^ (2 * 2 ^ (3 * sizem 𝒞)) * (2 * sizem 𝒞) +
                      (3 * (3 * sizem 𝒞) + 2) * (2 ^ (3 * sizem 𝒞)) +
                      Suc (2 ^ (3 * sizem 𝒞)) * 2 ^ 2 ^ (3 * sizem 𝒞) +
                      2 ^ (Suc (2 * 2 ^ (3 * sizem 𝒞))) * sizem 𝒞"
  {fix clause assume "clause ∈ reduced_dnf"
    then obtain fms where "fms ∈ introduce_w"
                      and clause: "clause = fms ∪ introduce_v ∪ introduce_UnionOfVennRegions ∪ reduce_clause"
      unfolding reduced_dnf_def by blast    
    then have "card clause ≤ card fms + card introduce_v + card introduce_UnionOfVennRegions + card reduce_clause"
      by (auto intro!: order.trans[OF card_Un_le])
    also have "... ≤ 2 ^ (2 * 2 ^ card V) * card F + card introduce_v + card introduce_UnionOfVennRegions + card reduce_clause"
      using size_introduce_w ‹fms ∈ introduce_w› by fastforce
    also have "... ≤ 2 ^ (2 * 2 ^ card V) * card F + (3 * card V + 2) * (2 ^ card V) + card introduce_UnionOfVennRegions + card reduce_clause"
      using size_introduce_v by simp
    also have "... ≤ 2 ^ (2 * 2 ^ card V) * card F + (3 * card V + 2) * (2 ^ card V) + Suc (2 ^ card V) * 2 ^ 2 ^ card V + card reduce_clause"
      using size_introduce_UnionOfVennRegions by simp
    also have "... ≤ 2 ^ (2 * 2 ^ card V) * card F + (3 * card V + 2) * (2 ^ card V) + Suc (2 ^ card V) * 2 ^ 2 ^ card V + 2 ^ (Suc (2 * 2 ^ card V)) * sizem 𝒞"
      using size_reduce_clause by simp
    also have "... ≤ ?upper_bound"
      using card_V_upper_bound card_F_upper_bound
      by (metis Suc_le_mono add_le_mono add_le_mono1 mult_le_mono mult_le_mono1 mult_le_mono2 one_le_numeral power_increasing)
    finally have "card clause ≤ ?upper_bound" .
  }
  then show ?thesis by blast
qed

end