Theory MLSSmf_to_MLSS_Completeness

theory MLSSmf_to_MLSS_Completeness
  imports MLSSmf_Semantics MLSSmf_to_MLSS MLSSmf_HF_Extras
          Proper_Venn_Regions Reduced_MLSS_Formula_Singleton_Model_Property
begin

locale MLSSmf_to_MLSS_complete =
  normalized_MLSSmf_clause š’ž for š’ž :: "('v, 'f) MLSSmf_clause" +
    fixes ā„¬ :: "('v, 'f) Composite ā‡’ hf"
  assumes ā„¬: "is_model_for_reduced_dnf ā„¬"

    fixes Ī› :: "hf ā‡’ 'v set set"
  assumes Ī›_subset_V: "Ī› x āŠ† P+ V"
      and Ī›_preserves_zero: "Ī› 0 = {}"
      and Ī›_inc: "a ā‰¤ b āŸ¹ Ī› a āŠ† Ī› b"
      and Ī›_add: "Ī› (a āŠ” b) = Ī› a āˆŖ Ī› b"
      and Ī›_mul: "Ī› (a āŠ“ b) = Ī› a āˆ© Ī› b"
      and Ī›_discr: "l āŠ† P+ V āŸ¹
                    a = ā؆HF ((ā„¬ āˆ˜ VennRegion) ` l) āŸ¹ a = ā؆HF ((ā„¬ āˆ˜ VennRegion) ` (Ī› a))"
begin

fun discretizev :: "(('v, 'f) Composite ā‡’ hf) ā‡’ ('v ā‡’ hf)" where
  "discretizev ā„³ = ā„³ āˆ˜ Solo"

fun discretizef :: "(('v, 'f) Composite ā‡’ hf) ā‡’ ('f ā‡’ hf ā‡’ hf)" where
  "discretizef ā„³ = (Ī»f a. ā„³ wā‡˜fā‡™ā‡˜Ī› aā‡™)"

interpretation proper_Venn_regions V "discretizev ā„¬"
  using finite_V by unfold_locales

lemma all_literal_sat: "āˆ€lt āˆˆ set š’ž. Il (discretizev ā„¬) (discretizef ā„¬) lt"
proof
  fix lt assume "lt āˆˆ set š’ž"

  from ā„¬ obtain clause where clause: "clause āˆˆ reduced_dnf"
                         and ā„¬_sat_clause: "āˆ€lt āˆˆ clause. interp Isa ā„¬ lt"
    unfolding is_model_for_reduced_dnf_def by blast

  from ā€¹lt āˆˆ set š’žā€ŗ have "norm_literal lt"
    using norm_š’ž by blast
  then show "Il (discretizev ā„¬) (discretizef ā„¬) lt"
  proof (cases lt rule: norm_literal.cases)
    case (inc f)
    have "s ā‰¤ t āŸ¹ discretizef ā„¬ f s ā‰¤ discretizef ā„¬ f t" for s t
    proof -
      let ?atom = "Var wā‡˜fā‡™ā‡˜Ī› tā‡™ =s Var wā‡˜fā‡™ā‡˜Ī› tā‡™ āŠ”s Var wā‡˜fā‡™ā‡˜Ī› sā‡™"
      assume "s ā‰¤ t"
      then have "Ī› s āŠ† Ī› t" using Ī›_inc by simp
      then have "?atom āˆˆ reduce_atom (inc(f))"
        using Ī›_subset_V
        by (simp add: V_def)
      then have "AT ?atom āˆˆ clause"
        using ā€¹lt = ATm (inc(f))ā€ŗ ā€¹lt āˆˆ set š’žā€ŗ clause
        unfolding reduced_dnf_def reduce_clause_def by fastforce
      with ā„¬_sat_clause have "Isa ā„¬ ?atom" by fastforce
      then have "ā„¬ wā‡˜fā‡™ā‡˜Ī› tā‡™ = ā„¬ wā‡˜fā‡™ā‡˜Ī› tā‡™ āŠ” ā„¬ wā‡˜fā‡™ā‡˜Ī› sā‡™" by simp
      then have "ā„¬ wā‡˜fā‡™ā‡˜Ī› sā‡™ ā‰¤ ā„¬ wā‡˜fā‡™ā‡˜Ī› tā‡™"
        by (simp add: sup.order_iff)
      then show "discretizef ā„¬ f s ā‰¤ discretizef ā„¬ f t" by simp
    qed
    then show ?thesis using inc by auto

  next
    case (dec f)
    have "s ā‰¤ t āŸ¹ discretizef ā„¬ f t ā‰¤ discretizef ā„¬ f s" for s t
    proof -
      let ?atom = "Var wā‡˜fā‡™ā‡˜Ī› sā‡™ =s Var wā‡˜fā‡™ā‡˜Ī› sā‡™ āŠ”s Var wā‡˜fā‡™ā‡˜Ī› tā‡™"
      assume "s ā‰¤ t"
      then have "Ī› s āŠ† Ī› t" using Ī›_inc by simp
      then have "?atom āˆˆ reduce_atom (dec(f))"
        using Ī›_subset_V
        by (simp add: V_def)
      then have "AT ?atom āˆˆ clause"
        using ā€¹lt = ATm (dec(f))ā€ŗ ā€¹lt āˆˆ set š’žā€ŗ clause
        unfolding reduced_dnf_def reduce_clause_def by fastforce
      with ā„¬_sat_clause have "Isa ā„¬ ?atom" by fastforce
      then have "ā„¬ wā‡˜fā‡™ā‡˜Ī› sā‡™ = ā„¬ wā‡˜fā‡™ā‡˜Ī› sā‡™ āŠ” ā„¬ wā‡˜fā‡™ā‡˜Ī› tā‡™" by simp
      then have "ā„¬ wā‡˜fā‡™ā‡˜Ī› tā‡™ ā‰¤ ā„¬ wā‡˜fā‡™ā‡˜Ī› sā‡™"
        by (simp add: sup.order_iff)
      then show "discretizef ā„¬ f t ā‰¤ discretizef ā„¬ f s" by simp
    qed
    then show ?thesis using dec by auto

  next
    case (add f)
    have "discretizef ā„¬ f (s āŠ” t) = discretizef ā„¬ f s āŠ” discretizef ā„¬ f t" for s t
    proof -
      let ?atom = "Var wā‡˜fā‡™ā‡˜Ī› (s āŠ” t)ā‡™ =s Var wā‡˜fā‡™ā‡˜Ī› sā‡™ āŠ”s Var wā‡˜fā‡™ā‡˜Ī› tā‡™"
      have "?atom āˆˆ reduce_atom (add(f))"
        using Ī›_subset_V Ī›_add 
        by (simp add: V_def)
      then have "AT ?atom āˆˆ clause"
        using ā€¹lt = ATm (add(f))ā€ŗ ā€¹lt āˆˆ set š’žā€ŗ clause
        unfolding reduced_dnf_def reduce_clause_def by fastforce
      with ā„¬_sat_clause have "Isa ā„¬ ?atom" by fastforce
      then have "ā„¬ wā‡˜fā‡™ā‡˜Ī› (s āŠ” t)ā‡™ = ā„¬ wā‡˜fā‡™ā‡˜Ī› sā‡™ āŠ” ā„¬ wā‡˜fā‡™ā‡˜Ī› tā‡™" by simp
      then show "discretizef ā„¬ f (s āŠ” t) = discretizef ā„¬ f s āŠ” discretizef ā„¬ f t" by simp
    qed
    then show ?thesis using add by auto

  next
    case (mul f)
    have "discretizef ā„¬ f (s āŠ“ t) = discretizef ā„¬ f s āŠ“ discretizef ā„¬ f t" for s t
    proof -
      let ?atom_1 = "Var (InterOfWAux f (Ī› s) (Ī› t)) =s Var wā‡˜fā‡™ā‡˜Ī› sā‡™ -s Var wā‡˜fā‡™ā‡˜Ī› tā‡™"
      have "?atom_1 āˆˆ reduce_atom (mul(f))"
        using Ī›_subset_V 
        by (simp add: V_def)
      then have "AT ?atom_1 āˆˆ clause"
        using ā€¹lt = ATm (mul(f))ā€ŗ ā€¹lt āˆˆ set š’žā€ŗ clause
        unfolding reduced_dnf_def reduce_clause_def by fastforce
      with ā„¬_sat_clause have "Isa ā„¬ ?atom_1" by fastforce
      then have "ā„¬ (InterOfWAux f (Ī› s) (Ī› t)) = ā„¬ wā‡˜fā‡™ā‡˜Ī› sā‡™ - ā„¬ wā‡˜fā‡™ā‡˜Ī› tā‡™" by simp
      moreover
      let ?atom_2 = "Var wā‡˜fā‡™ā‡˜Ī› (s āŠ“ t)ā‡™ =s Var wā‡˜fā‡™ā‡˜Ī› sā‡™ -s Var (InterOfWAux f (Ī› s) (Ī› t))"
      have "?atom_2 āˆˆ reduce_atom (mul(f))"
        using Ī›_subset_V Ī›_mul
        by (simp add: V_def)
      then have "AT ?atom_2 āˆˆ clause"
        using ā€¹lt = ATm (mul(f))ā€ŗ ā€¹lt āˆˆ set š’žā€ŗ clause
        unfolding reduced_dnf_def reduce_clause_def by fastforce
      with ā„¬_sat_clause have "Isa ā„¬ ?atom_2" by fastforce
      then have "ā„¬ wā‡˜fā‡™ā‡˜Ī› (s āŠ“ t)ā‡™ = ā„¬ wā‡˜fā‡™ā‡˜Ī› sā‡™ - ā„¬ (InterOfWAux f (Ī› s) (Ī› t))" by simp
      ultimately
      have "ā„¬ wā‡˜fā‡™ā‡˜Ī› (s āŠ“ t)ā‡™ = ā„¬ wā‡˜fā‡™ā‡˜Ī› sā‡™ āŠ“ ā„¬ wā‡˜fā‡™ā‡˜Ī› tā‡™" by auto
      then show "discretizef ā„¬ f (s āŠ“ t) = discretizef ā„¬ f s āŠ“ discretizef ā„¬ f t" by simp
    qed
    then show ?thesis using mul by auto

  next
    case (le f g)
    have "discretizef ā„¬ f s ā‰¤ discretizef ā„¬ g s" for s
    proof -
      let ?atom = "Var wā‡˜gā‡™ā‡˜Ī› sā‡™ =s Var wā‡˜gā‡™ā‡˜Ī› sā‡™ āŠ”s Var wā‡˜fā‡™ā‡˜Ī› sā‡™"
      have "?atom āˆˆ reduce_atom (f ā‰¼m g)"
        using Ī›_subset_V 
        by (simp add: V_def)
      then have "AT ?atom āˆˆ clause"
        using ā€¹lt = ATm (f ā‰¼m g)ā€ŗ ā€¹lt āˆˆ set š’žā€ŗ clause
        unfolding reduced_dnf_def reduce_clause_def by fastforce
      with ā„¬_sat_clause have "Isa ā„¬ ?atom" by fastforce
      then have "ā„¬ wā‡˜gā‡™ā‡˜Ī› sā‡™ = ā„¬ wā‡˜gā‡™ā‡˜Ī› sā‡™ āŠ” ā„¬ wā‡˜fā‡™ā‡˜Ī› sā‡™" by simp
      then have "ā„¬ wā‡˜fā‡™ā‡˜Ī› sā‡™ ā‰¤ ā„¬ wā‡˜gā‡™ā‡˜Ī› sā‡™"
        by (simp add: sup.orderI)
      then show "discretizef ā„¬ f s ā‰¤ discretizef ā„¬ g s" by simp
    qed
    then show ?thesis using le by auto

  next
    case (eq_empty x n)
    let ?lt = "AT (Var (Solo x) =s āˆ… n)"
    from eq_empty have "?lt āˆˆ reduce_literal lt"
      using ā€¹lt āˆˆ set š’žā€ŗ by simp
    then have "?lt āˆˆ clause"
      using ā€¹lt āˆˆ set š’žā€ŗ clause
      unfolding reduced_dnf_def reduce_clause_def by fastforce
    with ā„¬_sat_clause have "interp Isa ā„¬ ?lt" by fastforce
    with eq_empty show ?thesis by simp

  next
    case (eq x y)
    let ?lt = "AT (Var (Solo x) =s Var (Solo y))"
    from eq have "?lt āˆˆ reduce_literal lt"
      using ā€¹lt āˆˆ set š’žā€ŗ by simp
    then have "?lt āˆˆ clause"
      using ā€¹lt āˆˆ set š’žā€ŗ clause
      unfolding reduced_dnf_def reduce_clause_def by fastforce
    with ā„¬_sat_clause have "interp Isa ā„¬ ?lt" by fastforce
    with eq show ?thesis by simp

  next
    case (neq x y)
    let ?lt = "AF (Var (Solo x) =s Var (Solo y))"
    from neq have "?lt āˆˆ reduce_literal lt"
      using ā€¹lt āˆˆ set š’žā€ŗ by simp
    then have "?lt āˆˆ clause"
      using ā€¹lt āˆˆ set š’žā€ŗ clause
      unfolding reduced_dnf_def reduce_clause_def by fastforce
    with ā„¬_sat_clause have "interp Isa ā„¬ ?lt" by fastforce
    with neq show ?thesis by simp

  next
    case (union x y z)
    let ?lt = "AT (Var (Solo x) =s Var (Solo y) āŠ”s Var (Solo z))"
    from union have "?lt āˆˆ reduce_literal lt"
      using ā€¹lt āˆˆ set š’žā€ŗ by simp
    then have "?lt āˆˆ clause"
      using neq ā€¹lt āˆˆ set š’žā€ŗ clause
      unfolding reduced_dnf_def reduce_clause_def by fastforce
    with ā„¬_sat_clause have "interp Isa ā„¬ ?lt" by fastforce
    with union show ?thesis by simp

  next
    case (diff x y z)
    let ?lt = "AT (Var (Solo x) =s Var (Solo y) -s Var (Solo z))"
    from diff have "?lt āˆˆ reduce_literal lt"
      using ā€¹lt āˆˆ set š’žā€ŗ by simp
    then have "?lt āˆˆ clause"
      using neq ā€¹lt āˆˆ set š’žā€ŗ clause
      unfolding reduced_dnf_def reduce_clause_def by fastforce
    with ā„¬_sat_clause have "interp Isa ā„¬ ?lt" by fastforce
    with diff show ?thesis by simp

  next
    case (single x y)
    let ?lt = "AT (Var (Solo x) =s Single (Var (Solo y)))"
    from single have "?lt āˆˆ reduce_literal lt"
      using ā€¹lt āˆˆ set š’žā€ŗ by simp
    then have "?lt āˆˆ clause"
      using neq ā€¹lt āˆˆ set š’žā€ŗ clause
      unfolding reduced_dnf_def reduce_clause_def by fastforce
    with ā„¬_sat_clause have "interp Isa ā„¬ ?lt" by fastforce
    with single show ?thesis by simp

  next
    case (app x f y)
    with ā€¹lt āˆˆ set š’žā€ŗ have "f āˆˆ F" unfolding F_def by force
    from ā„¬_sat_clause clause eval_v
    have ā„¬_v: "(ā„¬ āˆ˜ VennRegion) Ī± = proper_Venn_region Ī±" if "Ī± āˆˆ P+ V" for Ī±
      unfolding reduced_dnf_def
      using proper_Venn_region.simps that by force
    from ā„¬_sat_clause clause eval_w
    have ā„¬_w: "ā؆HF ((ā„¬ āˆ˜ VennRegion) ` l) = ā؆HF ((ā„¬ āˆ˜ VennRegion) ` m) āŸ¶ ā„¬ wā‡˜fā‡™ā‡˜lā‡™ = ā„¬ wā‡˜fā‡™ā‡˜mā‡™"
      if "l āŠ† P+ V" "m āŠ† P+ V" "f āˆˆ F" for l m f
      by (meson in_mono introduce_UnionOfVennRegions_subset_reduced_fms introduce_w_subset_reduced_fms that)
    
    from app ā€¹lt āˆˆ set š’žā€ŗ have "y āˆˆ V" using V_def by fastforce
    with variable_as_composition_of_proper_Venn_regions
    have "ā؆HF (proper_Venn_region ` ā„’ V y) = discretizev ā„¬ y" by blast
    with Ī›_discr ā„’_subset_P_plus ā„¬_v
    have "ā؆HF ((ā„¬ āˆ˜ VennRegion) ` ā„’ V y) = ā؆HF ((ā„¬ āˆ˜ VennRegion) ` Ī› (discretizev ā„¬ y))"
      by (smt (verit, best) HUnion_eq subset_eq)
    with ā„¬_w have ā„¬_w_eq: "ā„¬ wā‡˜fā‡™ā‡˜ā„’ V yā‡™ = ā„¬ wā‡˜fā‡™ā‡˜Ī› (discretizev ā„¬ y)ā‡™"
      using ā„’_subset_P_plus Ī›_subset_V ā€¹f āˆˆ Fā€ŗ finite_V by meson

    let ?lt = "AT (Var (Solo x) =s Var wā‡˜fā‡™ā‡˜ā„’ V yā‡™)"
    from app have "?lt āˆˆ reduce_literal lt"
      using ā€¹lt āˆˆ set š’žā€ŗ by simp
    then have "?lt āˆˆ clause"
      using neq ā€¹lt āˆˆ set š’žā€ŗ clause
      unfolding reduced_dnf_def reduce_clause_def by fastforce
    with ā„¬_sat_clause have "interp Isa ā„¬ ?lt" by fastforce
    then have "ā„¬ (Solo x) = ā„¬ wā‡˜fā‡™ā‡˜ā„’ V yā‡™" by simp
    with ā„¬_w_eq have "ā„¬ (Solo x) = ā„¬ wā‡˜fā‡™ā‡˜Ī› (discretizev ā„¬ y)ā‡™" by argo
    then have "ā„¬ (Solo x) = (discretizef ā„¬ f) (discretizev ā„¬ y)" by simp
    then have "discretizev ā„¬ x = (discretizef ā„¬ f) (discretizev ā„¬ y)" by simp
    with app show ?thesis by simp
  qed
qed

lemma š’ž_sat: "Icl (discretizev ā„¬) (discretizef ā„¬) š’ž"
  using all_literal_sat by blast

end
                          
lemma (in normalized_MLSSmf_clause) MLSSmf_to_MLSS_completeness:
  assumes "is_model_for_reduced_dnf M"
    shows "āˆƒMv Mf. Icl Mv Mf š’ž"
proof -
  from assms singleton_model_for_reduced_MLSS_clause obtain ā„³ where
    ā„³_singleton: "āˆ€Ī± āˆˆ P+ V. hcard (ā„³ (vā‡˜Ī±ā‡™)) ā‰¤ 1" and
    ā„³_model: "is_model_for_reduced_dnf ā„³"
    using normalized_MLSSmf_clause_axioms V_def by blast
  then obtain clause where "clause āˆˆ reduced_dnf" "āˆ€lt āˆˆ clause. interp Isa ā„³ lt"
    unfolding is_model_for_reduced_dnf_def by blast
  with normalized_clause_contains_all_v_Ī± have v_Ī±_in_vars:
    "āˆ€Ī±āˆˆP+ V. vā‡˜Ī±ā‡™ āˆˆ ā‹ƒ (vars ` clause)"
    by blast

  from ā„³_singleton have assigned_set_card_0_or_1:
    "āˆ€Ī± āˆˆ P+ V. hcard (ā„³ (vā‡˜Ī±ā‡™)) = 0 āˆØ hcard (ā„³ (vā‡˜Ī±ā‡™)) = 1"
    using antisym_conv2 by blast

  let ?Ī› = "Ī»a. {Ī± āˆˆ P+ V. ā„³ vā‡˜Ī±ā‡™ āŠ“ a ā‰  0}"

  have Ī›_subset_V: "?Ī› x āŠ† P+ V" for x
    by fast

  have Ī›_preserves_zero: "?Ī› 0 = {}" by blast

  have Ī›_inc: "a ā‰¤ b āŸ¹ ?Ī› a āŠ† ?Ī› b" for a b
    by (smt (verit) Collect_mono hinter_hempty_right inf.absorb_iff1 inf_left_commute)

  have Ī›_add: "?Ī› (a āŠ” b) = ?Ī› a āˆŖ ?Ī› b" for a b
  proof (standard; standard)
    fix Ī± assume Ī±: "Ī± āˆˆ {Ī± āˆˆ P+ V. ā„³ vā‡˜Ī±ā‡™ āŠ“ (a āŠ” b) ā‰  0}"
    then have "Ī± āˆˆ P+ V" "ā„³ vā‡˜Ī±ā‡™ āŠ“ (a āŠ” b) ā‰  0" by blast+
    then have "ā„³ vā‡˜Ī±ā‡™ āŠ“ a ā‰  0 āˆØ ā„³ vā‡˜Ī±ā‡™ āŠ“ b ā‰  0"
      by (metis hunion_hempty_right inf_sup_distrib1) 
    then show "Ī± āˆˆ {Ī± āˆˆ P+ V. ā„³ vā‡˜Ī±ā‡™ āŠ“ a ā‰  0} āˆŖ {Ī± āˆˆ P+ V. ā„³ vā‡˜Ī±ā‡™ āŠ“ b ā‰  0}"
      using Ī± by blast
  next
    fix Ī± assume "Ī± āˆˆ {Ī± āˆˆ P+ V. ā„³ vā‡˜Ī±ā‡™ āŠ“ a ā‰  0} āˆŖ {Ī± āˆˆ P+ V. ā„³ vā‡˜Ī±ā‡™ āŠ“ b ā‰  0}"
    then have "Ī± āˆˆ P+ V" "ā„³ vā‡˜Ī±ā‡™ āŠ“ a ā‰  0 āˆØ ā„³ vā‡˜Ī±ā‡™ āŠ“ b ā‰  0"
      by blast+
    then have "ā„³ vā‡˜Ī±ā‡™ āŠ“ (a āŠ” b) ā‰  0"
      by (metis hinter_hempty_right hunion_hempty_left inf_sup_absorb inf_sup_distrib1)
    then show "Ī± āˆˆ {Ī± āˆˆ P+ V. ā„³ vā‡˜Ī±ā‡™ āŠ“ (a āŠ” b) ā‰  0}"
      using ā€¹Ī± āˆˆ P+ Vā€ŗ by blast
  qed

  have Ī›_mul: "?Ī› (a āŠ“ b) = ?Ī› a āˆ© ?Ī› b" for a b
  proof (standard; standard)
    fix Ī± assume Ī±: "Ī± āˆˆ {Ī± āˆˆ P+ V. ā„³ vā‡˜Ī±ā‡™ āŠ“ (a āŠ“ b) ā‰  0}"
    then have "Ī± āˆˆ P+ V" "ā„³ vā‡˜Ī±ā‡™ āŠ“ (a āŠ“ b) ā‰  0" by blast+
    then have "ā„³ vā‡˜Ī±ā‡™ āŠ“ a ā‰  0 āˆ§ ā„³ vā‡˜Ī±ā‡™ āŠ“ b ā‰  0"
      by (metis hinter_hempty_left inf_assoc inf_left_commute)
    then show "Ī± āˆˆ {Ī± āˆˆ P+ V. ā„³ vā‡˜Ī±ā‡™ āŠ“ a ā‰  0} āˆ© {Ī± āˆˆ P+ V. ā„³ vā‡˜Ī±ā‡™ āŠ“ b ā‰  0}"
      using Ī± by blast
  next
    fix Ī± assume "Ī± āˆˆ {Ī± āˆˆ P+ V. ā„³ vā‡˜Ī±ā‡™ āŠ“ a ā‰  0} āˆ© {Ī± āˆˆ P+ V. ā„³ vā‡˜Ī±ā‡™ āŠ“ b ā‰  0}"
    then have "Ī± āˆˆ P+ V" "ā„³ vā‡˜Ī±ā‡™ āŠ“ a ā‰  0" "ā„³ vā‡˜Ī±ā‡™ āŠ“ b ā‰  0"
      by blast+
    then have "ā„³ vā‡˜Ī±ā‡™ ā‰  0" by force
    then have "hcard (ā„³ vā‡˜Ī±ā‡™) ā‰  0" using hcard_0E by blast
    then have "hcard (ā„³ vā‡˜Ī±ā‡™) = 1"
      using assigned_set_card_0_or_1 v_Ī±_in_vars ā€¹Ī± āˆˆ P+ Vā€ŗ
      by fastforce
    then obtain c where "ā„³ vā‡˜Ī±ā‡™ = 0 ā—ƒ c"
      using hcard_1E by blast
    moreover
    from ā€¹ā„³ vā‡˜Ī±ā‡™ = 0 ā—ƒ cā€ŗ ā€¹ā„³ vā‡˜Ī±ā‡™ āŠ“ a ā‰  0ā€ŗ
    have "ā„³ vā‡˜Ī±ā‡™ āŠ“ a = 0 ā—ƒ c" by auto
    moreover
    from ā€¹ā„³ vā‡˜Ī±ā‡™ = 0 ā—ƒ cā€ŗ ā€¹ā„³ vā‡˜Ī±ā‡™ āŠ“ b ā‰  0ā€ŗ
    have "ā„³ vā‡˜Ī±ā‡™ āŠ“ b = 0 ā—ƒ c" by auto
    ultimately
    have "ā„³ vā‡˜Ī±ā‡™ āŠ“ (a āŠ“ b) = 0 ā—ƒ c"
      by (simp add: inf_commute inf_left_commute)
    then have "ā„³ vā‡˜Ī±ā‡™ āŠ“ (a āŠ“ b) ā‰  0" by simp
    then show "Ī± āˆˆ {Ī± āˆˆ P+ V. ā„³ vā‡˜Ī±ā‡™ āŠ“ (a āŠ“ b) ā‰  0}"
      using ā€¹Ī± āˆˆ P+ Vā€ŗ by blast
  qed

  have "l āŠ† P+ V āŸ¹
        a = ā؆HF ((ā„³ āˆ˜ VennRegion) ` l) āŸ¹ a ā‰¤ ā؆HF ((ā„³ āˆ˜ VennRegion) ` (?Ī› a))" for l a
  proof
    fix c assume l_a_c: "l āŠ† P+ V" "a = ā؆HF ((ā„³ āˆ˜ VennRegion) ` l)" "c āˆˆ a"
    then obtain Ī± where "Ī± āˆˆ l" "c āˆˆ ā„³ vā‡˜Ī±ā‡™" by auto
    then have "Ī± āˆˆ ?Ī› a" using l_a_c by blast
    then have "ā„³ vā‡˜Ī±ā‡™ āˆˆ (ā„³ āˆ˜ VennRegion) ` (?Ī› a)" by simp
    then have "ā„³ vā‡˜Ī±ā‡™ āˆˆ HF ((ā„³ āˆ˜ VennRegion) ` (?Ī› a))" by fastforce
    with ā€¹c āˆˆ ā„³ vā‡˜Ī±ā‡™ā€ŗ show "c āˆˆ ā؆HF ((ā„³ āˆ˜ VennRegion) ` (?Ī› a))" by blast
  qed
  moreover
  have "l āŠ† P+ V āŸ¹
        a = ā؆HF ((ā„³ āˆ˜ VennRegion) ` l) āŸ¹ ā؆HF ((ā„³ āˆ˜ VennRegion) ` (?Ī› a)) ā‰¤ a" for l a
  proof -
    assume "l āŠ† P+ V" and a: "a = ā؆HF ((ā„³ āˆ˜ VennRegion) ` l)"
    then have "finite l"
      by (simp add: finite_V finite_subset)
    have "?Ī› a āŠ† l"
    proof
      fix Ī± assume "Ī± āˆˆ ?Ī› a"
      then obtain c where "c āˆˆ ā„³ vā‡˜Ī±ā‡™ āŠ“ a" by blast
      then have "c āˆˆ ā„³ vā‡˜Ī±ā‡™" "c āˆˆ a" by blast+
      then obtain Ī² where "Ī² āˆˆ l" "c āˆˆ ā„³ vā‡˜Ī²ā‡™" using a by force


      interpret proper_Venn_regions V "ā„³ āˆ˜ Solo"
        using finite_V by unfold_locales
      from ā€¹Ī± āˆˆ ?Ī› aā€ŗ have "Ī± āˆˆ P+ V" by auto
      moreover
      from ā€¹l āŠ† P+ Vā€ŗ ā€¹Ī² āˆˆ lā€ŗ have "Ī² āˆˆ P+ V" by auto
      moreover
      from ā€¹c āˆˆ ā„³ vā‡˜Ī±ā‡™ā€ŗ have "c āˆˆ proper_Venn_region Ī±"
        using eval_v ā€¹Ī± āˆˆ P+ Vā€ŗ ā„³_model
        unfolding is_model_for_reduced_dnf_def reduced_dnf_def
        by fastforce
      moreover
      from ā€¹c āˆˆ ā„³ vā‡˜Ī²ā‡™ā€ŗ have "c āˆˆ proper_Venn_region Ī²"
        using eval_v ā€¹Ī² āˆˆ P+ Vā€ŗ ā„³_model
        unfolding is_model_for_reduced_dnf_def reduced_dnf_def
        by fastforce
      ultimately
      have "Ī± = Ī²"
        using finite_V proper_Venn_region_strongly_injective by auto
      with ā€¹Ī² āˆˆ lā€ŗ show "Ī± āˆˆ l" by simp
    qed
    then have "(ā„³ āˆ˜ VennRegion) ` ?Ī› a āŠ† (ā„³ āˆ˜ VennRegion) ` l" by blast
    moreover
    from ā€¹finite lā€ŗ have "finite ((ā„³ āˆ˜ VennRegion) ` l)" by blast
    ultimately
    have "ā؆HF ((ā„³ āˆ˜ VennRegion) ` ?Ī› a) ā‰¤ ā؆HF ((ā„³ āˆ˜ VennRegion) ` l)"
      by (metis (no_types, lifting) HUnion_hunion finite_subset sup.orderE sup.orderI union_hunion)
    then show "ā؆HF ((ā„³ āˆ˜ VennRegion) ` (?Ī› a)) ā‰¤ a"
      using a by blast
  qed
  ultimately
  have Ī›_discr: "l āŠ† P+ V āŸ¹
                 a = ā؆HF ((ā„³ āˆ˜ VennRegion) ` l) āŸ¹ a = ā؆HF ((ā„³ āˆ˜ VennRegion) ` (?Ī› a))" for l a
    by (simp add: inf.absorb_iff1 inf_commute)

  interpret Ī›_plus: MLSSmf_to_MLSS_complete š’ž ā„³ ?Ī›
    using assms ā„³_singleton ā„³_model
          Ī›_subset_V Ī›_preserves_zero Ī›_inc Ī›_add Ī›_mul Ī›_discr
    by unfold_locales

  show ?thesis
    using Ī›_plus.š’ž_sat by fast
qed

end