Theory Reduced_MLSS_Formula_Singleton_Model_Property

theory Reduced_MLSS_Formula_Singleton_Model_Property
  imports Syntactic_Description Place_Realisation MLSSmf_to_MLSS
begin

locale satisfiable_normalized_MLSS_clause_with_vars_for_proper_Venn_regions =
  satisfiable_normalized_MLSS_clause 𝒞 𝒜 for 𝒞 𝒜 +
    fixes U :: "'a set"
    ―‹The collection of variables representing
       the proper Venn regions of the "original" variable set of the MLSSmf clause›
  assumes U_subset_V: "U ⊆ V"
      and no_overlap_within_U: "⟦u⇩1 ∈ U; u⇩2 ∈ U; u⇩1 ≠ u⇩2⟧ ⟹ 𝒜 u⇩1 ⊓ 𝒜 u⇩2 = 0"
      and U_collect_places_neq: "AF (Var x =⇩s Var y) ∈ 𝒞 ⟹
          ∃L M. L ⊆ U ∧ M ⊆ U ∧ 𝒜 x = ⨆HF (𝒜 ` L) ∧ 𝒜 y = ⨆HF (𝒜 ` M)"
      and U_collect_places_single: "AT (Var x =⇩s Single (Var y)) ∈ 𝒞 ⟹
          ∃L M. L ⊆ U ∧ M ⊆ U ∧ 𝒜 x = ⨆HF (𝒜 ` L) ∧ 𝒜 y = ⨆HF (𝒜 ` M)"
begin

interpretation 𝔅: adequate_place_framework 𝒞 PI at⇩p
  using syntactic_description_is_adequate by blast

lemma fact_1:
  assumes "u⇩1 ∈ U"
      and "u⇩2 ∈ U"
      and "u⇩1 ≠ u⇩2"
      and "π ∈ PI"
    shows "¬ (π u⇩1 ∧ π u⇩2)"
proof (rule ccontr)
  assume "¬ ¬ (π u⇩1 ∧ π u⇩2)"
  then have "π u⇩1" "π u⇩2" by blast+
  from ‹π ∈ PI› obtain σ where "σ ∈ Σ" "π = π⇘σ⇙" by auto
  then have "σ ≠ 0" by fastforce
  from ‹π = π⇘σ⇙› ‹π u⇩1› ‹π u⇩2› have "σ ≤ 𝒜 u⇩1" "σ ≤ 𝒜 u⇩2" by simp+
  with ‹σ ≠ 0› have "𝒜 u⇩1 ⊓ 𝒜 u⇩2 ≠ 0" by blast
  with no_overlap_within_U show False
    using ‹u⇩1 ∈ U› ‹u⇩2 ∈ U› ‹u⇩1 ≠ u⇩2› by blast
qed

fun place_eq :: "('a ⇒ bool) ⇒ ('a ⇒ bool) ⇒ bool" where
  "place_eq π⇩1 π⇩2 ⟷ (∀x ∈ V. π⇩1 x = π⇩2 x)"

fun place_sim :: "('a ⇒ bool) ⇒ ('a ⇒ bool) ⇒ bool" (infixl "∼" 50) where
  "place_sim π⇩1 π⇩2 ⟷ place_eq π⇩1 π⇩2 ∨ (∃u ∈ U. π⇩1 u ∧ π⇩2 u)"

abbreviation "rel_place_sim ≡ {(π⇩1, π⇩2) ∈ PI × PI. π⇩1 ∼ π⇩2}"

lemma place_sim_rel_equiv_on_PI: "equiv PI rel_place_sim"
proof (rule equivI)
  have "rel_place_sim ⊆ PI × PI" by blast
  moreover
  have "(π, π) ∈ rel_place_sim" if "π ∈ PI" for π
    using that by fastforce
  ultimately
  show "refl_on PI rel_place_sim" using refl_onI by blast
  
  show "sym rel_place_sim"
  proof (rule symI)
    fix π⇩1 π⇩2 assume "(π⇩1, π⇩2) ∈ rel_place_sim"
    then have "π⇩1 ∈ PI" "π⇩2 ∈ PI" "π⇩1 ∼ π⇩2" by blast+
    then show "(π⇩2, π⇩1) ∈ rel_place_sim" by auto
  qed
  
  show "trans rel_place_sim"
  proof (rule transI)
    fix π⇩1 π⇩2 π⇩3
    assume "(π⇩1, π⇩2) ∈ rel_place_sim" "(π⇩2, π⇩3) ∈ rel_place_sim"
    then have "π⇩1 ∈ PI" "π⇩2 ∈ PI" "π⇩3 ∈ PI" "π⇩1 ∼ π⇩2" "π⇩2 ∼ π⇩3" by blast+
    then consider "place_eq π⇩1 π⇩2 ∧ place_eq π⇩2 π⇩3" | "place_eq π⇩1 π⇩2 ∧ (∃u ∈ U. π⇩2 u ∧ π⇩3 u)"
      | "(∃u ∈ U. π⇩1 u ∧ π⇩2 u) ∧ place_eq π⇩2 π⇩3" | "(∃u ∈ U. π⇩1 u ∧ π⇩2 u) ∧ (∃u ∈ U. π⇩2 u ∧ π⇩3 u)"
      by auto
    then have "π⇩1 ∼ π⇩3"
    proof (cases)
      case 1
      then have "place_eq π⇩1 π⇩3" by auto
      then show ?thesis by auto
    next
      case 2
      then obtain u where "u ∈ U" "π⇩2 u" "π⇩3 u" by blast
      with U_subset_V have "u ∈ V" by blast
      with 2 have "π⇩1 u ⟷ π⇩2 u" by force
      with ‹π⇩2 u› have "π⇩1 u" by blast
      with ‹u ∈ U› ‹π⇩3 u›
      show ?thesis by auto
    next
      case 3
      then obtain u where "u ∈ U" "π⇩1 u" "π⇩2 u" by blast
      with U_subset_V have "u ∈ V" by blast
      with 3 have "π⇩2 u ⟷ π⇩3 u" by force
      with ‹π⇩2 u› have "π⇩3 u" by blast
      with ‹u ∈ U› ‹π⇩1 u›
      show ?thesis by auto
    next
      case 4
      then obtain u⇩1 u⇩2 where "u⇩1 ∈ U" "π⇩1 u⇩1" "π⇩2 u⇩1" and "u⇩2 ∈ U" "π⇩2 u⇩2" "π⇩3 u⇩2"
        by blast
      with fact_1 have "u⇩1 = u⇩2"
        using ‹π⇩2 ∈ PI› by blast
      with ‹π⇩3 u⇩2› have "π⇩3 u⇩1" by blast
      with ‹π⇩1 u⇩1› ‹u⇩1 ∈ U› show ?thesis
        by auto
    qed
    with ‹π⇩1 ∈ PI› ‹π⇩2 ∈ PI› ‹π⇩3 ∈ PI›
    show "(π⇩1, π⇩3) ∈ rel_place_sim" by blast
  qed
qed

lemma refl_sim:
  assumes "a ∈ PI"
      and "b ∈ PI"
      and "a ∼ b"
    shows "b ∼ a"
  using assms by auto

lemma trans_sim:
  assumes "a ∈ PI"
      and "b ∈ PI"
      and "c ∈ PI"
      and "a ∼ b"
      and "b ∼ c"
    shows "a ∼ c"
proof -
  from assms have "(a, b) ∈ rel_place_sim" "(b, c) ∈ rel_place_sim"
    by blast+
  with place_sim_rel_equiv_on_PI have "(a, c) ∈ rel_place_sim"
    using equivE transE
    by (smt (verit, ccfv_SIG))
  then show "a ∼ c" by blast
qed

lemma fact_2:
  assumes "x ∈ V"
      and exL: "∃L ⊆ U. 𝒜 x = ⨆HF (𝒜 ` L)"
      and "π⇩1 ∈ PI"
      and "π⇩2 ∈ PI"
      and "π⇩1 ∼ π⇩2"
    shows "π⇩1 x ⟷ π⇩2 x"
proof (cases "place_eq π⇩1 π⇩2")
  case True
  with ‹x ∈ V› show ?thesis by force
next
  case False
  with ‹π⇩1 ∼ π⇩2› obtain u where "u ∈ U" "π⇩1 u" "π⇩2 u" by auto
  from exL obtain L where "L ⊆ U" "𝒜 x = ⨆HF (𝒜 ` L)" by blast
  from ‹L ⊆ U› U_subset_V finite_V have "finite L"
    by (simp add: finite_subset)

  have "π x ⟷ u ∈ L" if "π u" "π ∈ PI" for π
  proof -
    from ‹π ∈ PI› obtain σ where "π = π⇘σ⇙" "σ ∈ Σ" by auto
    with ‹π u› have "σ ≤ 𝒜 u"
      using ‹u ∈ U› U_subset_V by auto
    have "σ ≤ 𝒜 x ⟷ u ∈ L"
    proof (standard)
      assume "σ ≤ 𝒜 x"
      {assume "u ∉ L"
        then have "∀v ∈ L. v ≠ u" by blast
        with no_overlap_within_U have "∀v ∈ L. 𝒜 v ⊓ 𝒜 u = 0"
          using ‹L ⊆ U› ‹u ∈ U› by auto
        with ‹σ ≤ 𝒜 u› have "∀v ∈ L. 𝒜 v ⊓ σ = 0" by blast
        then have "⨆HF (𝒜 ` L) ⊓ σ = 0"
          using finite_V U_subset_V ‹L ⊆ U› by auto
        with ‹𝒜 x = ⨆HF (𝒜 ` L)› have "𝒜 x ⊓ σ = 0" by argo
        with ‹σ ≤ 𝒜 x› have False
          using ‹σ ∈ Σ› mem_Σ_not_empty by blast
      }
      then show "u ∈ L" by blast
    next
      assume "u ∈ L"
      with ‹σ ≤ 𝒜 u› have "σ ≤ ⨆HF (𝒜 ` L)"
        using ‹finite L› by force
      with ‹𝒜 x = ⨆HF (𝒜 ` L)› show "σ ≤ 𝒜 x" by simp
    qed
    with ‹π = π⇘σ⇙› show "π x ⟷ u ∈ L"
      using ‹x ∈ V› associated_place.simps by blast
  qed
  with ‹π⇩1 ∈ PI› ‹π⇩1 u› ‹π⇩2 ∈ PI› ‹π⇩2 u›
  have "π⇩1 x ⟷ u ∈ L" "π⇩2 x ⟷ u ∈ L" by blast+
  then show ?thesis by blast
qed

lemma U_collect_places_single': "y ∈ W ⟹ ∃L. L ⊆ U ∧ 𝒜 y = ⨆HF (𝒜 ` L)"
  using U_collect_places_single
  by (meson memW_E)

definition PI' :: "('a ⇒ bool) set" where
  "PI' ≡ (λπs. SOME π. π ∈ πs) ` (PI // rel_place_sim)"

definition rep :: "('a ⇒ bool) ⇒ ('a ⇒ bool)" where
  "rep π = (SOME π'. π' ∈ rel_place_sim `` {π})"

lemma range_rep:
  assumes "π ∈ PI"
    shows "rep π ∈ PI'"
  using assms
  unfolding PI'_def rep_def
  using quotientI[where ?x = π and ?A = PI and ?r = rel_place_sim]
  by blast

lemma PI'_eq_image_of_rep_on_PI: "PI' = rep ` PI"
proof (standard; standard)
  fix π assume "π ∈ PI'"
  then obtain πs where "πs ∈ PI // rel_place_sim" "π = (SOME π. π ∈ πs)"
    unfolding PI'_def by blast
  then obtain π⇩0 where "πs = rel_place_sim `` {π⇩0}" "π⇩0 ∈ PI"
    using quotientE[where ?A = PI and ?r = rel_place_sim and ?X = πs]
    by blast
  with ‹π = (SOME π. π ∈ πs)› have "π = rep π⇩0"
    unfolding rep_def by blast
 with ‹π⇩0 ∈ PI› show "π ∈ rep ` PI" by blast
next
  fix π assume "π ∈ rep ` PI"
  then obtain π⇩0 where "π⇩0 ∈ PI" "π = rep π⇩0" by blast
  then show "π ∈ PI'" using range_rep by blast
qed

lemma rep_sim:
  assumes "π ∈ PI"
    shows "π ∼ rep π"
      and "rep π ∼ π"
proof -
  from ‹π ∈ PI› have "π ∈ rel_place_sim `` {π}" by fastforce
  then obtain π' where "π' = rep π" by blast
  with someI[of "λx. x ∈ rel_place_sim `` {π}"] have "π' ∈ rel_place_sim `` {π}"
    using ‹π ∈ rel_place_sim `` {π}›
    unfolding rep_def by fast
  with ‹π' = rep π› show "π ∼ rep π" by fast
  with place_sim_rel_equiv_on_PI show "rep π ∼ π"
    by (metis (full_types) place_eq.simps place_sim.elims(1))
qed

lemma PI'_subset_PI: "PI' ⊆ PI"
  unfolding PI'_def
  using equiv_Eps_preserves place_sim_rel_equiv_on_PI by blast

lemma sim_self:
  assumes "π ∈ PI'"
      and "π' ∈ PI'"
      and "π ∼ π'"
    shows "π' = π"
proof -
  from ‹π ∼ π'› have "(π, π') ∈ rel_place_sim"
    using ‹π ∈ PI'› ‹π' ∈ PI'› PI'_subset_PI by blast
  from ‹π ∈ PI'› obtain πs where "πs ∈ PI // rel_place_sim" "π = (SOME π. π ∈ πs)"
    unfolding PI'_def by blast
  then have "π ∈ πs"
    using equiv_Eps_in place_sim_rel_equiv_on_PI by blast
  from ‹π' ∈ PI'› obtain πs' where "πs' ∈ PI // rel_place_sim" "π' = (SOME π. π ∈ πs')"
    unfolding PI'_def by blast
  then have "π' ∈ πs'"
    using equiv_Eps_in place_sim_rel_equiv_on_PI by blast
  from place_sim_rel_equiv_on_PI ‹πs ∈ PI // rel_place_sim› ‹πs' ∈ PI // rel_place_sim›
       ‹π ∈ πs› ‹π' ∈ πs'› ‹(π, π') ∈ rel_place_sim›
  have "πs = πs'"
    using quotient_eqI[where ?A = PI and ?r = rel_place_sim and ?x = π and ?X = πs and ?y = π' and ?Y = πs']
    by fast
  with ‹π = (SOME π. π ∈ πs)› ‹π' = (SOME π. π ∈ πs')› show "π' = π"
    by auto
qed

fun at⇩p_f' :: "'a ⇒ ('a ⇒ bool)" where
  "at⇩p_f' w = rep (at⇩p_f w)"

definition "at⇩p' = {(y, at⇩p_f' y)|y. y ∈ W}"
declare at⇩p'_def [simp]

lemma range_at⇩p_f':
  assumes "w ∈ W"
  shows "at⇩p_f' w ∈ PI'"
proof -
  from ‹w ∈ W› range_at⇩p_f have "at⇩p_f w ∈ PI" by blast
  then have "rel_place_sim `` {at⇩p_f w} ∈ PI // rel_place_sim"
    using quotientI by fast
  then show ?thesis unfolding PI'_def
    apply (simp only: at⇩p_f'.simps rep_def)
    by (smt (verit, best) Eps_cong at⇩p_f'.elims image_insert insert_iff mk_disjoint_insert)
qed

lemma rep_at:
  assumes "π ∈ PI"
      and "(y, π) ∈ at⇩p"
    shows "(y, rep π) ∈ at⇩p'"
proof -
  from ‹(y, π) ∈ at⇩p› have "at⇩p_f y = π" by auto
  from ‹(y, π) ∈ at⇩p› have "y ∈ W" by auto
  with W_subset_V have "y ∈ V" by fast
  from ‹(y, π) ∈ at⇩p› obtain x where "AT (Var x =⇩s Single (Var y)) ∈ 𝒞" "x ∈ V"
    using memW_E by fastforce
  with U_collect_places_single have "∃L. L ⊆ U ∧ 𝒜 x = ⨆HF (𝒜 ` L)" by meson
  with fact_2 have "π⇩1 x ⟷ π⇩2 x" if "π⇩1 ∼ π⇩2" "π⇩1 ∈ PI" "π⇩2 ∈ PI" for π⇩1 π⇩2
    using ‹x ∈ V› that by blast
  with rep_sim have "(rep π) x ⟷ π x"
    using PI'_subset_PI ‹π ∈ PI› range_rep by blast
  
  from 𝔅.C5_1[where ?x = x and ?y = y] have "π x" "∀π'∈PI. π' ≠ π ⟶ ¬ π' x"
    using ‹AT (Var x =⇩s Single (Var y)) ∈ 𝒞› ‹(y, π) ∈ at⇩p› by fastforce+
  
  from ‹π x› ‹(rep π) x ⟷ π x› have "(rep π) x" by blast
  with ‹∀π'∈PI. π' ≠ π ⟶ ¬ π' x› have "rep π = π"
    using range_rep PI'_subset_PI ‹π ∈ PI› by blast
  then have "at⇩p_f' y = rep π"
    using ‹at⇩p_f y = π› by (simp only: at⇩p_f'.simps)
  then show "(y, rep π) ∈ at⇩p'"
    using ‹y ∈ W›
    by (metis (mono_tags, lifting) at⇩p'_def mem_Collect_eq)
qed

interpretation 𝔅': adequate_place_framework 𝒞 PI' at⇩p'
proof -
  from PI'_subset_PI 𝔅.PI_subset_places_V
  have PI'_subset_places_V: "PI' ⊆ places V" by blast

  have dom_at⇩p': "Domain at⇩p' = W" by auto
  have range_at⇩p': "Range at⇩p' ⊆ PI'"
  proof -
    {fix y lt assume "lt ∈ 𝒞" "y ∈ singleton_vars lt"
      then have "rep (at⇩p_f y) ∈ PI'"
        using range_at⇩p_f[of y] range_rep[of "at⇩p_f y"]
        by blast
    }
    then show ?thesis by auto
  qed

  from 𝔅.single_valued_at⇩p
  have single_valued_at⇩p': "single_valued at⇩p'"
    unfolding single_valued_def at⇩p'_def
    apply (simp only: at⇩p_f'.simps)
    by blast

  from PI'_subset_PI have "place_membership 𝒞 PI' ⊆ place_membership 𝒞 PI" by auto
  with 𝔅.membership_irreflexive have membership_irreflexive:
    "(π, π) ∉ place_membership 𝒞 PI'" for π
    by blast

  from PI'_subset_PI have subgraph: "subgraph (place_mem_graph 𝒞 PI') (place_mem_graph 𝒞 PI)"
  proof -
    have "verts (place_mem_graph 𝒞 PI') = PI'" by simp
    moreover
    have "verts (place_mem_graph 𝒞 PI) = PI" by simp
    ultimately
    have verts: "verts (place_mem_graph 𝒞 PI') ⊆ verts (place_mem_graph 𝒞 PI)"
      using PI'_subset_PI by presburger

    have "arcs (place_mem_graph 𝒞 PI') = place_membership 𝒞 PI'" by simp
    moreover
    have "arcs (place_mem_graph 𝒞 PI) = place_membership 𝒞 PI" by simp
    moreover
    have "place_membership 𝒞 PI' ⊆ place_membership 𝒞 PI"
      using PI'_subset_PI by auto
    ultimately
    have arcs: "arcs (place_mem_graph 𝒞 PI') ⊆ arcs (place_mem_graph 𝒞 PI)" by blast

    have "compatible (place_mem_graph 𝒞 PI) (place_mem_graph 𝒞 PI')"
      unfolding compatible_def by simp
    with verts arcs show "subgraph (place_mem_graph 𝒞 PI') (place_mem_graph 𝒞 PI)"
      unfolding subgraph_def
      using place_mem_graph_wf_digraph
      by blast
  qed

  from 𝔅.C6 have "∄c. pre_digraph.cycle (place_mem_graph 𝒞 PI) c"
    using dag.acyclic by blast
  then have "∄c. pre_digraph.cycle (place_mem_graph 𝒞 PI') c"
    using subgraph wf_digraph.subgraph_cycle by blast
  then have C6: "dag (place_mem_graph 𝒞 PI')"
    using ‹dag (place_mem_graph 𝒞 PI)› dag_axioms_def dag_def digraph.digraph_subgraph subgraph
    by blast

  from 𝔅.C1_1 PI'_subset_PI
  have C1_1: "∃n. AT (Var x =⇩s ∅ n) ∈ 𝒞 ⟹ ∀π ∈ PI'. ¬ π x" for x
    by fast

  from 𝔅.C1_2 PI'_subset_PI
  have C1_2: "AT (Var x =⇩s Var y) ∈ 𝒞 ⟹ ∀π ∈ PI'. π x ⟷ π y" for x y
    by fast

  from 𝔅.C2 PI'_subset_PI
  have C2: "AT (Var x =⇩s Var y ⊔⇩s Var z) ∈ 𝒞 ⟹ ∀π ∈ PI'. π x ⟷ π y ∨ π z" for x y z
    by fast

  from 𝔅.C3 PI'_subset_PI
  have C3: "AT (Var x =⇩s Var y -⇩s Var z) ∈ 𝒞 ⟹ ∀π ∈ PI'. π x ⟷ π y ∧ ¬ π z" for x y z
    by fast

  have C4: "AF (Var x =⇩s Var y) ∈ 𝒞 ⟹ ∃π ∈ PI'. π x ⟷ ¬ π y" for x y
  proof -
    assume neq: "AF (Var x =⇩s Var y) ∈ 𝒞"
    with 𝔅.C4 obtain π where "π ∈ PI" "π x ⟷ ¬ π y" by blast
    from neq have "x ∈ V" "y ∈ V" by fastforce+
    from neq U_collect_places_neq[where ?x = x and ?y = y] fact_2[of x]
    have sim_π_x: "π⇩1 x = π⇩2 x" if "π⇩1 ∈ PI" "π⇩2 ∈ PI" "π⇩1 ∼ π⇩2" for π⇩1 π⇩2
      using that ‹x ∈ V› by blast
    from neq U_collect_places_neq[where ?x = x and ?y = y] fact_2[of y]
    have sim_π_y: "π⇩1 y = π⇩2 y" if "π⇩1 ∈ PI" "π⇩2 ∈ PI" "π⇩1 ∼ π⇩2" for π⇩1 π⇩2
      using that ‹y ∈ V› by blast
    from ‹π ∈ PI› have "rep π ∈ PI'" using range_rep by blast
    then have "rep π ∈ PI" using PI'_subset_PI by blast

    from rep_sim sim_π_x have "(rep π) x ⟷ π x"
      using ‹rep π ∈ PI› ‹π ∈ PI› by blast
    moreover
    from rep_sim sim_π_y have "π y ⟷ (rep π) y"
      using ‹rep π ∈ PI› ‹π ∈ PI› by blast
    ultimately
    have "(rep π) x ⟷ ¬ (rep π) y"
      using ‹π x ⟷ ¬ π y› by blast
    with ‹rep π ∈ PI'› show ?thesis by blast
  qed

  have C5_1: "∃π. (y, π) ∈ at⇩p' ∧ π x ∧ (∀π' ∈ PI'. π' ≠ π ⟶ ¬ π' x)"
    if "AT (Var x =⇩s Single (Var y)) ∈ 𝒞" for x y
  proof -
    from that have "y ∈ W" "x ∈ V" "y ∈ V" by fastforce+
    from that 𝔅.C5_1[where ?y = y and ?x = x]
    obtain π where π: "(y, π) ∈ at⇩p" "π x" "∀π' ∈ PI. π' ≠ π ⟶ ¬ π' x"
      by blast
    with 𝔅.range_at⇩p have "π ∈ PI" by fast
    then have "rep π ∈ PI'" using range_rep by blast
    from rep_sim have "rep π ∼ π" using ‹π ∈ PI› by fast
    with U_collect_places_single ‹π x› fact_2 have "(rep π) x"
      using ‹x ∈ V› ‹π ∈ PI› ‹rep π ∈ PI'› PI'_subset_PI that
      by blast
    with π have "rep π = π"
      using ‹rep π ∈ PI'› PI'_subset_PI by blast
    with π show ?thesis
      using ‹rep π ∈ PI'› PI'_subset_PI
      by (metis rep_at subset_iff)
  qed

  have C5_2: "∀π ∈ PI'. π y ⟷ π z" if "y ∈ W" "z ∈ W" and at'_eq: "∃π. (y, π) ∈ at⇩p' ∧ (z, π) ∈ at⇩p'" for y z
  proof
    fix π assume "π ∈ PI'"
    from at'_eq obtain π' where π': "at⇩p_f' y = π'" "at⇩p_f' z = π'"
      by (simp only: at⇩p'_def) fast
    with range_at⇩p_f' ‹y ∈ W› have "π' ∈ PI'" by blast
    from π' have "at⇩p_f' y ∼ at⇩p_f' z"
      apply (simp only: at⇩p_f'.simps place_sim.simps place_eq.simps)
      by blast
    moreover
    from rep_sim have "at⇩p_f' y ∼ at⇩p_f y"
      using at⇩p_f'.simps range_at⇩p_f that(1) by presburger
    moreover
    from rep_sim have "at⇩p_f' z ∼ at⇩p_f z"
      using at⇩p_f'.simps range_at⇩p_f that(2) by presburger
    ultimately
    have "at⇩p_f y ∼ at⇩p_f z"
      using trans_sim[of "at⇩p_f y" "at⇩p_f' y" "at⇩p_f' z"]
      using trans_sim[of "at⇩p_f y" "at⇩p_f' z" "at⇩p_f z"]
      using refl_sim[of "at⇩p_f' y" "at⇩p_f y"]
      using range_at⇩p_f[of y] range_at⇩p_f[of z] range_at⇩p_f' PI'_subset_PI that(1-2)
      by (meson subset_iff)
    then consider "at⇩p_f y = at⇩p_f z" | "∃u ∈ U. at⇩p_f y u ∧ at⇩p_f z u"
      by force
    then show "π y ⟷ π z"
    proof (cases)
      case 1
      then have "∃π. (y, π) ∈ at⇩p ∧ (z, π) ∈ at⇩p"
        using at⇩p_def ‹y ∈ W› ‹z ∈ W› by blast
      with 𝔅.C5_2 have "∀π ∈ PI. π y ⟷ π z"
        using ‹y ∈ W› ‹z ∈ W› by presburger
      with ‹π ∈ PI'› PI'_subset_PI show "π y ⟷ π z"
        by fast
    next
      case 2
      then obtain u where "u ∈ U" "at⇩p_f y u" "at⇩p_f z u" by blast
      then have "𝒜 y ❙∈ 𝒜 u" "𝒜 z ❙∈ 𝒜 u"
        by (simp add: less_eq_hf_def)+
      from ‹y ∈ W› obtain x⇩1 where x⇩1_single_y: "AT (Var x⇩1 =⇩s Single (Var y)) ∈ 𝒞"
        using memW_E by blast
      with 𝒜_sat_𝒞 have "𝒜 x⇩1 = HF {𝒜 y}" by fastforce
      then have "𝒜 y ❙∈ 𝒜 x⇩1" by simp      
      from x⇩1_single_y U_collect_places_single obtain L where "L ⊆ U" "𝒜 x⇩1 = ⨆HF (𝒜 ` L)"
        by meson
      with ‹𝒜 y ❙∈ 𝒜 x⇩1› obtain u' where "u' ∈ L" "𝒜 y ❙∈ 𝒜 u'" by auto
      from ‹𝒜 x⇩1 = ⨆HF (𝒜 ` L)› ‹u' ∈ L› have "𝒜 u' ≤ 𝒜 x⇩1"
        using ‹𝒜 y ❙∈ 𝒜 x⇩1› by auto
      with ‹𝒜 x⇩1 = HF {𝒜 y}› ‹𝒜 y ❙∈ 𝒜 u'› have "𝒜 u' = HF {𝒜 y}" by auto
      with ‹𝒜 y ❙∈ 𝒜 u› ‹u ∈ U› ‹u' ∈ L› ‹L ⊆ U› no_overlap_within_U
      have "u' = u" by fastforce
      with ‹𝒜 u' = HF {𝒜 y}› ‹𝒜 z ❙∈ 𝒜 u› have "𝒜 y = 𝒜 z" by simp
      with realise_same_implies_eq_under_all_π[of y z π] show ?thesis
        using ‹y ∈ W› ‹z ∈ W› W_subset_V ‹π ∈ PI'› PI'_subset_PI by blast
    qed
  qed

  have C5_3: "∃π. (y, π) ∈ at⇩p' ∧ (y', π) ∈ at⇩p'"
    if "y ∈ W" "y' ∈ W" "∀π' ∈ PI'. π' y' ⟷ π' y" for y' y
  proof -
    from ‹∀π' ∈ PI'. π' y' ⟷ π' y› have "∀π ∈ PI. rep π y' ⟷ rep π y"
      by (metis range_rep)
    {fix π assume "π ∈ PI"
      with ‹∀π' ∈ PI'. π' y' ⟷ π' y› have "rep π y' ⟷ rep π y"
        using range_rep by fast
      from ‹π ∈ PI› PI'_subset_PI range_rep have "rep π ∈ PI" by blast
      from U_collect_places_single'[of y'] fact_2[of y' "rep π" π] rep_sim[of π]
      have "rep π y' ⟷ π y'"
        using ‹y' ∈ W› W_subset_V ‹π ∈ PI› ‹rep π ∈ PI›
        by blast
      from U_collect_places_single'[of y] fact_2[of y "rep π" π] rep_sim[of π]
      have "rep π y ⟷ π y"
        using ‹y ∈ W› W_subset_V ‹π ∈ PI› ‹rep π ∈ PI›
        by blast
      from ‹rep π y' ⟷ rep π y› ‹rep π y' ⟷ π y'› ‹rep π y ⟷ π y›
      have "π y ⟷ π y'" by blast
    }
    with 𝔅.C5_3 obtain π where "(y, π) ∈ at⇩p" "(y', π) ∈ at⇩p"
      using ‹y ∈ W› ‹y' ∈ W› by blast
    then have "(y, rep π) ∈ at⇩p'" "(y', rep π) ∈ at⇩p'"
      by (meson Range_iff 𝔅.range_at⇩p rep_at subset_iff)+
    then show ?thesis by fast
  qed

  have "π = π⇘HF {0}⇙" if "π ∈ Range at⇩p' - Range (place_membership 𝒞 PI')" for π
  proof -
    from that obtain y where "(y, π) ∈ at⇩p'" by blast
    then have "y ∈ W" "π ∈ PI'"
      using dom_at⇩p' range_at⇩p' by blast+
    from ‹(y, π) ∈ at⇩p'› have "π = rep (at⇩p_f y)" by simp
    from ‹y ∈ W› obtain x where lt_in_𝒞: "AT (Var x =⇩s Single (Var y)) ∈ 𝒞"
      using memW_E by blast
    with 𝒜_sat_𝒞 have "𝒜 x = HF {𝒜 y}" by fastforce
    then have "σ⇘y⇙ ≤ 𝒜 x" by simp
    with lt_in_𝒞 have "at⇩p_f y x" by force
    with ‹π = rep (at⇩p_f y)› fact_2[of x] rep_sim[of "at⇩p_f y"] U_collect_places_single[of x y]
    have "π x"
      using lt_in_𝒞 ‹π ∈ PI'› PI'_subset_PI ‹y ∈ W›
      by (smt (verit, best) 𝔅.PI_subset_places_V places_domain range_at⇩p_f rev_contra_hsubsetD)

    have "∀π ∈ PI. ¬ π y"
    proof (rule ccontr)
      assume "¬ (∀π∈PI. ¬ π y)"
      then obtain π' where "π' ∈ PI" "π' y" by blast
      with U_collect_places_single'[of y] fact_2[of y "rep π'" π'] rep_sim[of π']
      have "rep π' y"
        using ‹y ∈ W› PI'_subset_PI W_subset_V range_rep by blast
      with ‹AT (Var x =⇩s Single (Var y)) ∈ 𝒞› ‹π x›
      have "(rep π', π) ∈ place_membership 𝒞 PI'"
        using ‹π ∈ PI'› ‹π' ∈ PI› range_rep
        by (simp only: place_membership.simps) blast
      then have "π ∈ Range (place_membership 𝒞 PI')" by blast
      with that show False by blast
    qed
    have "∀α ∈ ℒ V y. proper_Venn_region α = 0"
    proof (rule ccontr)
      assume "¬ (∀α ∈ ℒ V y. proper_Venn_region α = 0)"
      then obtain α where α: "α ∈ ℒ V y" "proper_Venn_region α ≠ 0" by blast
      then have "y ∈ α" "α ∈ P⇧+ V" by auto
      with ‹proper_Venn_region α ≠ 0› have "proper_Venn_region α ≤ 𝒜 y"
        using proper_Venn_region_subset_variable_iff
        by (meson mem_P_plus_subset subset_iff)
      then have "π⇘proper_Venn_region α⇙ y"
        using W_subset_V ‹y ∈ W› by auto
      with ‹∀π ∈ PI. ¬ π y› show False
        using α by auto
    qed
    then have "⨆HF (proper_Venn_region ` ℒ V y) = 0"
      by fastforce
    with variable_as_composition_of_proper_Venn_regions[of y]
    have "𝒜 y = 0"
      using ‹y ∈ W› W_subset_V by auto
    with ‹𝒜 x = HF {𝒜 y}› have "𝒜 x = HF {0}" by argo

    from ‹π ∈ PI'› PI'_subset_PI obtain σ where "σ ∈ Σ" "π = π⇘σ⇙"
      by (metis PI_def image_iff in_mono)
    with ‹π x› have "σ ≠ 0" "σ ≤ 𝒜 x" by simp+
    with ‹𝒜 x = HF {0}› have "σ = HF {0}" by fastforce
    with ‹π = π⇘σ⇙› show "π = π⇘HF {0}⇙" by blast
  qed
  then have C7:
    "⟦π⇩1 ∈ Range at⇩p' - Range (place_membership 𝒞 PI');
      π⇩2 ∈ Range at⇩p' - Range (place_membership 𝒞 PI')⟧ ⟹ π⇩1 = π⇩2" for π⇩1 π⇩2
    by blast

  from PI'_subset_places_V dom_at⇩p' range_at⇩p' single_valued_at⇩p'
       membership_irreflexive C6
       C1_1 C1_2 C2 C3 C4 C5_1 C5_2 C5_3 C7
  show "adequate_place_framework 𝒞 PI' at⇩p'"
    apply intro_locales
    unfolding adequate_place_framework_axioms_def
    by blast
qed

lemma singleton_model_for_normalized_reduced_literals:
  "∃ℳ. ∀lt ∈ 𝒞. interp I⇩s⇩a ℳ lt ∧ (∀u ∈ U. hcard (ℳ u) ≤ 1)"
proof -
  from 𝔅'.finite_PI have "finite (PI' - Range at⇩p')" by blast
  with u_exists[of "PI' - Range at⇩p'" "card PI'"] obtain u where
    "⟦π⇩1 ∈ PI' - Range at⇩p'; π⇩2 ∈ PI' - Range at⇩p'; π⇩1 ≠ π⇩2⟧ ⟹ u π⇩1 ≠ u π⇩2"
    "π ∈ PI' - Range at⇩p' ⟹ hcard (u π) ≥ card PI'"
  for π⇩1 π⇩2 π
    by blast
  then have "place_realization 𝒞 PI' at⇩p' u"
    by unfold_locales blast+
  
  {fix x assume "x ∈ U"
    then have "π⇩1 = π⇩2" if "π⇩1 x" "π⇩2 x" "π⇩1 ∈ PI'" "π⇩2 ∈ PI'" for π⇩1 π⇩2
      using sim_self that by auto
    then consider "{π ∈ PI'. π x} = {}" | "(∃π. {π ∈ PI'. π x} = {π})"
      by blast
    then have "hcard (place_realization.ℳ 𝒞 PI' at⇩p' u x) ≤ 1"
    proof (cases)
      case 1
      then have "place_realization.ℳ 𝒞 PI' at⇩p' u x = 0"
        using ‹place_realization 𝒞 PI' at⇩p' u› "place_realization.ℳ.simps"
        by fastforce
      then show ?thesis by simp
    next
      case 2
      then obtain π where "{π ∈ PI'. π x} = {π}" "π ∈ PI'" by auto
      then have "place_realization.ℳ 𝒞 PI' at⇩p' u x = ⨆HF (place_realization.place_realise 𝒞 PI' at⇩p' u ` {π})"
        using ‹place_realization 𝒞 PI' at⇩p' u› "place_realization.ℳ.simps"
        by fastforce
      also have "... = ⨆HF {place_realization.place_realise 𝒞 PI' at⇩p' u π}"
        by simp
      finally have "place_realization.ℳ 𝒞 PI' at⇩p' u x = ⨆HF {place_realization.place_realise 𝒞 PI' at⇩p' u π}" .
      moreover
      from place_realization.place_realise_singleton[of 𝒞 PI' at⇩p' u]
      have "hcard (place_realization.place_realise 𝒞 PI' at⇩p' u π) = 1"
        using ‹place_realization 𝒞 PI' at⇩p' u› ‹π ∈ PI'› by blast
      then obtain c where "place_realization.place_realise 𝒞 PI' at⇩p' u π = HF {c}"
        using hcard_1E[of "place_realization.place_realise 𝒞 PI' at⇩p' u π"]
        by fastforce
      ultimately
      have "place_realization.ℳ 𝒞 PI' at⇩p' u x = ⨆HF {HF {c}}"
        by presburger
      also have "... = HF {c}" by fastforce
      also have "hcard ... = 1"
        by (simp add: hcard_def)
      finally show ?thesis by linarith
    qed
  }
  moreover
  from place_realization.ℳ_sat_𝒞
  have "∀lt ∈ 𝒞. interp I⇩s⇩a (place_realization.ℳ 𝒞 PI' at⇩p' u) lt"
    using ‹place_realization 𝒞 PI' at⇩p' u› by fastforce
  ultimately
  show ?thesis by blast
qed

end

theorem singleton_model_for_reduced_MLSS_clause:
  assumes norm_𝒞: "normalized_MLSSmf_clause 𝒞"
      and V: "V = vars⇩m 𝒞"
      and 𝒜_model: "normalized_MLSSmf_clause.is_model_for_reduced_dnf 𝒞 𝒜"
    shows "∃ℳ. normalized_MLSSmf_clause.is_model_for_reduced_dnf 𝒞 ℳ ∧
                (∀α ∈ P⇧+ V. hcard (ℳ v⇘α⇙) ≤ 1)"
proof -
  from norm_𝒞 interpret normalized_MLSSmf_clause 𝒞 by blast
  interpret proper_Venn_regions V "𝒜 ∘ Solo"
    using V by unfold_locales blast

  from 𝒜_model have "∀fm∈introduce_v. interp I⇩s⇩a 𝒜 fm"
    unfolding is_model_for_reduced_dnf_def reduced_dnf_def
    by blast
  with eval_v have 𝒜_v: "∀α ∈ P⇧+ V. 𝒜 v⇘α⇙ = proper_Venn_region α"
    using V V_def proper_Venn_region.simps by auto

  from 𝒜_model have "∀lt ∈ introduce_UnionOfVennRegions. interp I⇩s⇩a 𝒜 lt"
    unfolding is_model_for_reduced_dnf_def reduced_dnf_def by blast
  then have "∀a ∈ restriction_on_UnionOfVennRegions αs. I⇩s⇩a 𝒜 a"
    if "αs ∈ set all_V_set_lists" for αs
    unfolding introduce_UnionOfVennRegions_def
    using that by simp
  with eval_UnionOfVennRegions have 𝒜_UnionOfVennRegions:
    "𝒜 (UnionOfVennRegions αs) = ⨆HF (𝒜 ` VennRegion ` set αs)"
    if "αs ∈ set all_V_set_lists" for αs
    using that by (simp add: Sup.SUP_image)

  have Solo_variable_as_composition_of_v:
    "∃L ⊆ {v⇘α⇙ |α. α ∈ P⇧+ V}. 𝒜 z = ⨆HF (𝒜 ` L)" if "∃z' ∈ V. z = Solo z'" for z
  proof -
    from that obtain z' where "z' ∈ V" "z = Solo z'" by blast
    then have "VennRegion ` ℒ V z' ⊆ {v⇘α⇙ |α. α ∈ P⇧+ V}" by fastforce
    moreover
    from 𝒜_v have "∀α ∈ ℒ V z'. 𝒜 v⇘α⇙ = proper_Venn_region α"
      using ℒ_subset_P_plus finite_V by fast
    then have "⨆HF (𝒜 ` (VennRegion ` ℒ V z')) = ⨆HF (proper_Venn_region ` ℒ V z')"
      using HUnion_eq[where ?S = "ℒ V z'" and ?f = "𝒜 ∘ VennRegion" and ?g = proper_Venn_region]
      by (simp add: image_comp)
    moreover
    from variable_as_composition_of_proper_Venn_regions
    have "(𝒜 ∘ Solo) z' = ⨆HF (proper_Venn_region ` ℒ V z')"
      using ‹z' ∈ V› by presburger
    with ‹z = Solo z'› have "𝒜 z = ⨆HF (proper_Venn_region ` ℒ V z')" by simp
    ultimately
    have "VennRegion ` ℒ V z' ⊆ {v⇘α⇙ |α. α ∈ P⇧+ V} ∧ 𝒜 z = ⨆HF (𝒜 ` VennRegion ` ℒ V z')"
      by simp
    then show ?thesis by blast
  qed

  from 𝒜_model obtain clause where clause:
    "clause ∈ reduced_dnf" "∀lt ∈ clause. interp I⇩s⇩a 𝒜 lt"
    unfolding is_model_for_reduced_dnf_def by blast
  with reduced_dnf_normalized have "normalized_MLSS_clause clause" by blast
  with clause
  have "satisfiable_normalized_MLSS_clause_with_vars_for_proper_Venn_regions clause 𝒜 {v⇘α⇙ |α. α ∈ P⇧+ V}"
  proof (unfold_locales, goal_cases)
    case 1
    then show ?case
      using normalized_MLSS_clause.norm_𝒞 by blast
  next
    case 2
    then show ?case
      by (simp add: normalized_MLSS_clause.finite_𝒞)
  next
    case 3
    then show ?case
      by (simp add: finite_vars_fm normalized_MLSS_clause.finite_𝒞)
  next
    case 4
    then show ?case by simp
  next
    case 5
    from ‹clause ∈ reduced_dnf› normalized_clause_contains_all_v_α
    have "∀α∈P⇧+ V. v⇘α⇙ ∈ ⋃ (vars ` clause)"
      using V V_def by simp
    then show ?case by blast      
  next
    case (6 x y)
    then obtain α β where αβ: "α ∈ P⇧+ V" "β ∈ P⇧+ V" "x = v⇘α⇙" "y = v⇘β⇙"
      by blast
    with ‹x ≠ y› have "α ≠ β" by blast

    from αβ have "α ⊆ V" "β ⊆ V" by auto

    from 𝒜_model have "∀fm∈introduce_v. interp I⇩s⇩a 𝒜 fm"
      unfolding is_model_for_reduced_dnf_def reduced_dnf_def by blast
    with αβ eval_v have "𝒜 x = proper_Venn_region α" "𝒜 y = proper_Venn_region β"
      using V V_def proper_Venn_region.simps by auto
    with proper_Venn_region_disjoint ‹α ≠ β›
    show ?case
      using ‹α ⊆ V› ‹β ⊆ V› by presburger
  next
    case (7 x y)
    from ‹AF (Var x =⇩s Var y) ∈ clause› ‹clause ∈ reduced_dnf›
    consider "AF (Var x =⇩s Var y) ∈ reduce_clause" | "∃clause ∈ introduce_w. AF (Var x =⇩s Var y) ∈ clause"
      unfolding reduced_dnf_def introduce_v_def introduce_UnionOfVennRegions_def by blast
    then show ?case
    proof (cases)
      case 1
      then obtain lt where lt: "lt ∈ set 𝒞" "AF (Var x =⇩s Var y) ∈ reduce_literal lt"
        unfolding reduce_clause_def by blast
      then obtain a where "lt = AF⇩m a"
        by (cases lt rule: reduce_literal.cases) auto
      from ‹lt ∈ set 𝒞› norm_𝒞 have "norm_literal lt" by blast
      with ‹lt = AF⇩m a› norm_literal_neq
      obtain x' y' where lt: "lt = AF⇩m (Var⇩m x' =⇩m Var⇩m y')" by blast
      then have "reduce_literal lt = {AF (Var (Solo x') =⇩s Var (Solo y'))}"
        by simp
      with ‹AF (Var x =⇩s Var y) ∈ reduce_literal lt› have "x = Solo x'" "y = Solo y'"
        by simp+
      from lt ‹lt ∈ set 𝒞› have "x' ∈ V" "y' ∈ V"
        using V by fastforce+

      from Solo_variable_as_composition_of_v show ?thesis
        using ‹x = Solo x'› ‹y = Solo y'› ‹x' ∈ V› ‹y' ∈ V›
        by (smt (verit, best))
    next
      case 2
      with lt_in_clause_in_introduce_w_E obtain l' m' f
        where l': "l' ∈ set all_V_set_lists"
          and m': "m' ∈ set all_V_set_lists"
          and f: "f ∈ set F_list"
          and "AF (Var x =⇩s Var y) ∈ set (restriction_on_FunOfUnionOfVennRegions l' m' f)"
        by blast
      then have "AF (Var x =⇩s Var y) = AF (Var (UnionOfVennRegions l') =⇩s Var (UnionOfVennRegions m'))"
        by auto
      then have "x = UnionOfVennRegions l'" "y = UnionOfVennRegions m'" by blast+
      with 𝒜_UnionOfVennRegions l' m'
      have "𝒜 x = ⨆HF (𝒜 ` VennRegion ` set l')" "𝒜 y = ⨆HF (𝒜 ` VennRegion ` set m')"
        by blast+
      moreover
      from l' set_all_V_set_lists have "set l' ⊆ P⇧+ V"
        using V V_def by auto
      then have "VennRegion ` set l' ⊆ {v⇘α⇙ |α. α ∈ P⇧+ V}"
        by blast
      moreover
      from m' set_all_V_set_lists have "set m' ⊆ P⇧+ V"
        using V V_def by auto
      then have "VennRegion ` set m' ⊆ {v⇘α⇙ |α. α ∈ P⇧+ V}"
        by blast
      ultimately
      show ?thesis by blast
    qed
  next
    case (8 x y)
    then consider "AT (Var x =⇩s Single (Var y)) ∈ introduce_v"
      | "∃clause ∈ introduce_w. AT (Var x =⇩s Single (Var y)) ∈ clause"
      | "AT (Var x =⇩s Single (Var y)) ∈ introduce_UnionOfVennRegions"
      | "AT (Var x =⇩s Single (Var y)) ∈ reduce_clause"
      unfolding reduced_dnf_def by blast
    then show ?case
    proof (cases)
      case 1
      have "Var x =⇩s Single (Var y) ≠ restriction_on_v α" for α
        by simp
      moreover
      have "Var x =⇩s Single (Var y) ∉ restriction_on_InterOfVars xs" for xs
        by (induction xs rule: restriction_on_InterOfVars.induct) auto
      then have "Var x =⇩s Single (Var y) ∉ (restriction_on_InterOfVars ∘ var_set_to_list) α" for α
        by simp
      moreover
      have "Var x =⇩s Single (Var y) ∉ restriction_on_UnionOfVars xs" for xs
        by (induction xs rule: restriction_on_UnionOfVars.induct) auto
      then have "Var x =⇩s Single (Var y) ∉ (restriction_on_UnionOfVars ∘ var_set_to_list) α" for α
        by simp
      ultimately
      have "AT (Var x =⇩s Single (Var y)) ∉ introduce_v"
        unfolding introduce_v_def by blast
      with 1 show ?thesis by blast
    next
      case 2
      with lt_in_clause_in_introduce_w_E obtain l' m' f
        where "AT (Var x =⇩s Single (Var y)) ∈ set (restriction_on_FunOfUnionOfVennRegions l' m' f)"
        by blast
      moreover
      have "AT (Var x =⇩s Single (Var y)) ∉ set (restriction_on_FunOfUnionOfVennRegions l' m' f)"
        by simp
      ultimately
      show ?thesis by blast
    next
      case 3
      have "Var x =⇩s Single (Var y) ∉ restriction_on_UnionOfVennRegions αs" for αs
        by (induction αs rule: restriction_on_UnionOfVennRegions.induct) auto
      then have "AT (Var x =⇩s Single (Var y)) ∉ introduce_UnionOfVennRegions"
        unfolding introduce_UnionOfVennRegions_def by blast
      with 3 show ?thesis by blast
    next
      case 4
      then obtain lt where "lt ∈ set 𝒞" and reduce_lt: "AT (Var x =⇩s Single (Var y)) ∈ reduce_literal lt"
        unfolding reduce_clause_def by blast
      with norm_𝒞 have "norm_literal lt" by blast
      then have "∃x' y'. lt = AT⇩m (Var⇩m x' =⇩m Single⇩m (Var⇩m y'))"
        apply (cases lt rule: norm_literal.cases)
        using reduce_lt by auto
      then obtain x' y' where lt: "lt = AT⇩m (Var⇩m x' =⇩m Single⇩m (Var⇩m y'))" by blast
      with reduce_lt have "x = Solo x'" "y = Solo y'" by simp+
      from ‹lt ∈ set 𝒞› lt have "x' ∈ V" "y' ∈ V"
        using V by fastforce+
      from Solo_variable_as_composition_of_v show ?thesis
        using ‹x = Solo x'› ‹y = Solo y'› ‹x' ∈ V› ‹y' ∈ V›
        by (smt (verit, best))
    qed
  qed
  then show ?thesis
    using satisfiable_normalized_MLSS_clause_with_vars_for_proper_Venn_regions.singleton_model_for_normalized_reduced_literals
    unfolding is_model_for_reduced_dnf_def
    by (smt (verit) V V_def clause(1) introduce_v_subset_reduced_fms mem_Collect_eq subset_iff v_α_in_vars_introduce_v)
qed

end