Theory Calculi_And_Annotations

(* Title:        Formalizing an abstract calculus based on splitting in a modular way
 * Authors:      Sophie Tourret <stourret at mpi-inf.mpg.de>, 2020-2025
 *               Florent Krasnopol <florent.krasnopol at ens-paris-saclay.fr>, 2022
 *               Ghilain Bergeron <ghilain.bergeron at inria.fr>, 2023 *)


theory Calculi_And_Annotations
  imports Disjunctive_Consequence_Relations
begin


section ‹Calculi and Derivations›

context
begin

no_notation Extended.extended.Pinf (‹∞›)

typedef 'a infinite_llist = ‹{ l :: 'a llist. llength l = ∞ }›
  morphisms to_llist Abs_infinite_llist
  using llength_inf_llist
  by blast

setup_lifting type_definition_infinite_llist

lift_definition llmap :: ‹('a ⇒ 'b) ⇒ 'a infinite_llist ⇒ 'b infinite_llist› is lmap
  by auto

lift_definition llnth :: ‹'a infinite_llist ⇒ nat ⇒ 'a› is lnth .

lift_definition Liminf_infinite_llist :: ‹'a set infinite_llist ⇒ 'a set› is Liminf_llist .

lift_definition Limsup_infinite_llist :: ‹'a set infinite_llist ⇒ 'a set› is Limsup_llist .

lift_definition Sup_infinite_llist :: ‹'a set infinite_llist ⇒ 'a set› is Sup_llist .

lift_definition llhd :: ‹'a infinite_llist ⇒ 'a› is lhd .

lemma llength_of_to_llist_is_infinite: ‹llength (to_llist L) = ∞›
  using to_llist
  by auto

end (* unnamed context *)

locale sound_inference_system =
  inference_system Inf + sound_cons: consequence_relation bot entails_sound
  for
    Inf :: "'f inference set" and
    bot :: "'f" and
    entails_sound :: "'f set ⇒ 'f set ⇒ bool" (infix "⊨s" 50)
  + assumes
    sound: "ι ∈ Inf ⟹ set (prems_of ι) ⊨s {concl_of ι}"

no_notation IArray.sub (infixl "!!" 100)
  
definition is_derivation :: "('f set ⇒ 'f set ⇒ bool) ⇒ ('f set infinite_llist) ⇒ bool" where
  "is_derivation R Ns ≡ ∀i. R (llnth Ns i) (llnth Ns (Suc i))"
  
definition terminates :: "'f set infinite_llist ⇒ bool" where
  "terminates Ns ≡ ∃i. ∀j>i. llnth Ns j = llnth Ns i"

abbreviation ‹lim_inf ≡ Liminf_infinite_llist›

abbreviation limit :: "'f set infinite_llist ⇒ 'f set" where "limit Ns ≡ lim_inf Ns"

abbreviation lim_sup :: ‹'f set infinite_llist ⇒ 'f set› where
  ‹lim_sup Ns ≡ Limsup_infinite_llist Ns›

locale calculus = inference_system Inf + consequence_relation bot entails
  for
    bot :: "'f" and
    Inf :: ‹'f inference set› and
    entails :: "'f set ⇒ 'f set ⇒ bool" (infix "⊨" 50)
  + fixes
    Red⇩I :: "'f set ⇒ 'f inference set" and
    Red⇩F :: "'f set ⇒ 'f set"
  assumes
    Red_I_to_Inf: "Red⇩I N ⊆ Inf" and
    Red_F_Bot: "N ⊨ {bot} ⟹ N - Red⇩F N ⊨ {bot}" and
    Red_F_of_subset: "N ⊆ N' ⟹ Red⇩F N ⊆ Red⇩F N'" and
    Red_I_of_subset: "N ⊆ N' ⟹ Red⇩I N ⊆ Red⇩I N'" and
    Red_F_of_Red_F_subset: "N' ⊆ Red⇩F N ⟹ Red⇩F N ⊆ Red⇩F (N - N')" and
    Red_I_of_Red_F_subset: "N' ⊆ Red⇩F N ⟹ Red⇩I N ⊆ Red⇩I (N - N')" and
    Red_I_of_Inf_to_N: "ι ∈ Inf ⟹ concl_of ι ∈ N ⟹ ι ∈ Red⇩I N"
begin

definition saturated :: "'f set ⇒ bool" where
  "saturated N ⟷ Inf_from N ⊆ Red⇩I N"
  
definition Red⇩I_strict :: "'f set ⇒ 'f inference set" where
  "Red⇩I_strict N = {ι. ι ∈ Red⇩I N ∨ (ι ∈ Inf ∧ bot ∈ N)}"
  
definition Red⇩F_strict :: "'f set ⇒ 'f set" where
  "Red⇩F_strict N = {C. C ∈ Red⇩F N ∨ (bot ∈ N ∧ C ≠ bot)}"
  
(* This proof helped detect a lack of precision in rmk 3 (missing restriction in the hypotheses *)
lemma strict_calc_if_nobot:
  "∀N. bot ∉ Red⇩F N ⟹ calculus bot Inf entails Red⇩I_strict Red⇩F_strict"
proof
  fix N
  show ‹Red⇩I_strict N ⊆ Inf› unfolding Red⇩I_strict_def using Red_I_to_Inf by blast
next
  fix N
  assume
    bot_notin: "∀N. bot ∉ Red⇩F N" and
    entails_bot: ‹N ⊨ {bot}›
  show ‹N - Red⇩F_strict N ⊨ {bot}›
  proof (cases "bot ∈ N")
    assume bot_in: "bot ∈ N"
    have ‹bot ∉ Red⇩F N› using bot_notin by blast
    then have ‹bot ∉ Red⇩F_strict N› unfolding Red⇩F_strict_def by blast 
    then have ‹Red⇩F_strict N = UNIV - {bot}›
      unfolding Red⇩F_strict_def using bot_in by blast
    then have ‹N - Red⇩F_strict N = {bot}› using bot_in by blast
    then show ‹N - Red⇩F_strict N ⊨ {bot}› using entails_reflexive[of bot] by simp
  next
    assume ‹bot ∉ N›
    then have ‹Red⇩F_strict N = Red⇩F N› unfolding Red⇩F_strict_def by blast
    then show ‹N - Red⇩F_strict N ⊨ {bot}› using Red_F_Bot[OF entails_bot] by simp
  qed
next
  fix N N' :: "'f set"
  assume ‹N ⊆ N'›
  then show ‹Red⇩F_strict N ⊆ Red⇩F_strict N'›
    unfolding Red⇩F_strict_def using Red_F_of_subset by blast
next
  fix N N' :: "'f set"
  assume ‹N ⊆ N'›
  then show ‹Red⇩I_strict N ⊆ Red⇩I_strict N'›
    unfolding Red⇩I_strict_def using Red_I_of_subset by blast
next
  fix N' N
  assume
    bot_notin: "∀N. bot ∉ Red⇩F N" and
    subs_red: "N' ⊆ Red⇩F_strict N"
  have ‹bot ∉ Red⇩F_strict N›
    using bot_notin unfolding Red⇩F_strict_def by blast
  then have nbot_in: ‹bot ∉ N'› using subs_red by blast 
  show ‹Red⇩F_strict N ⊆ Red⇩F_strict (N - N')›
  proof (cases "bot ∈ N")
    case True
    then have bot_in: "bot ∈ N - N'" using nbot_in by blast
    then show ?thesis unfolding Red⇩F_strict_def using bot_notin by force
  next
    case False
    then have eq_red: "Red⇩F_strict N = Red⇩F N" unfolding Red⇩F_strict_def by simp
    then have "N' ⊆ Red⇩F N" using subs_red by simp
    then have "Red⇩F N ⊆ Red⇩F (N - N')" using Red_F_of_Red_F_subset by simp
    then show ?thesis using eq_red Red⇩F_strict_def by blast 
  qed
next
  fix N' N
  assume
    "∀N. bot ∉ Red⇩F N" and
    subs_red: "N' ⊆ Red⇩F_strict N"
  then have bot_notin: "bot ∉ N'" unfolding Red⇩F_strict_def by blast 
  then show "Red⇩I_strict N ⊆ Red⇩I_strict (N - N')"
  proof (cases "bot ∈ N")
    case True
    then show ?thesis
      unfolding Red⇩I_strict_def using bot_notin Red_I_to_Inf by fastforce 
  next
    case False
    then show ?thesis
      using bot_notin Red_I_to_Inf subs_red Red_I_of_Red_F_subset 
      unfolding Red⇩I_strict_def Red⇩F_strict_def by simp
  qed
next
  fix ι N
  assume "ι ∈ Inf"
  then show "concl_of ι ∈ N ⟹ ι ∈ Red⇩I_strict N"
    unfolding Red⇩I_strict_def using Red_I_of_Inf_to_N Red_I_to_Inf by simp
qed

definition weakly_fair :: "'f set infinite_llist ⇒ bool" where
  ‹weakly_fair Ns ≡ Inf_from (Liminf_infinite_llist Ns) ⊆ Sup_infinite_llist (llmap Red⇩I Ns)›

abbreviation fair :: "'f set infinite_llist ⇒ bool" where "fair N ≡ weakly_fair N"

definition derive :: "'f set ⇒ 'f set ⇒ bool" (infix "⊳" 50) where
  "M ⊳ N ≡ (M - N ⊆ Red⇩F N)"

(* for reference, the definition used in the saturation framework *)
(* inductive "derive" :: "'f set ⇒ 'f set ⇒ bool" (infix "⊳" 50) where
     derive: "M - N ⊆ Red⇩F N ⟹ M ⊳ N" *)

lemma derive_refl: "M ⊳ M" unfolding derive_def by simp

lemma deriv_red_in: ‹M ⊳ N ⟹ Red⇩F M ⊆ N ∪ Red⇩F N›
proof -
  fix M N
  assume deriv: ‹M ⊳ N›
  then have ‹M ⊆ N ∪ Red⇩F N›
    unfolding derive_def by blast 
  then have red_m_in: ‹Red⇩F M ⊆ Red⇩F (N ∪ Red⇩F N)›
    using Red_F_of_subset by blast 
  have ‹Red⇩F (N ∪ Red⇩F N) ⊆ Red⇩F (N ∪ Red⇩F N - (Red⇩F N - N))›
    using Red_F_of_Red_F_subset[of "Red⇩F N - N" "N ∪ Red⇩F N"]
      Red_F_of_subset[of "N" "N ∪ Red⇩F N"] by fast
  then have ‹Red⇩F (N ∪ Red⇩F N) ⊆ Red⇩F N›
    by (metis Diff_subset_conv Red_F_of_subset Un_Diff_cancel lfp.leq_trans subset_refl sup.commute)
  then show ‹Red⇩F M ⊆ N ∪ Red⇩F N› using red_m_in by blast
qed

lemma derive_trans: "M ⊳ N ⟹ N ⊳ N' ⟹ M ⊳ N'" 
  using deriv_red_in by (smt (z3) Diff_subset_conv derive_def subset_trans sup.absorb_iff2)

end
  
locale sound_calculus = sound_inference_system Inf bot entails_sound +
  consequence_relation bot entails
  for
    bot :: "'f" and
    Inf :: ‹'f inference set› and
    entails :: "'f set ⇒ 'f set ⇒ bool" (infix "⊨" 50) and
    entails_sound :: "'f set ⇒ 'f set ⇒ bool" (infix "⊨s" 50)
    + fixes
    Red⇩I :: "'f set ⇒ 'f inference set" and
    Red⇩F :: "'f set ⇒ 'f set"
    assumes
      Red_I_to_Inf: "Red⇩I N ⊆ Inf" and
      Red_F_Bot: "N ⊨ {bot} ⟹ N - Red⇩F N ⊨ {bot}" and
      Red_F_of_subset: "N ⊆ N' ⟹ Red⇩F N ⊆ Red⇩F N'" and
      Red_I_of_subset: "N ⊆ N' ⟹ Red⇩I N ⊆ Red⇩I N'" and
      Red_F_of_Red_F_subset: "N' ⊆ Red⇩F N ⟹ Red⇩F N ⊆ Red⇩F (N - N')" and
      Red_I_of_Red_F_subset: "N' ⊆ Red⇩F N ⟹ Red⇩I N ⊆ Red⇩I (N - N')" and
      Red_I_of_Inf_to_N: "ι ∈ Inf ⟹ concl_of ι ∈ N ⟹ ι ∈ Red⇩I N"
begin

sublocale calculus bot Inf entails
  by (simp add: calculus.intro calculus_axioms.intro Red_F_Bot
    Red_F_of_Red_F_subset Red_F_of_subset Red_I_of_Inf_to_N Red_I_of_Red_F_subset Red_I_of_subset
    Red_I_to_Inf consequence_relation_axioms)
end
      
locale statically_complete_calculus = calculus +
  assumes statically_complete: "saturated N ⟹ N ⊨ {bot} ⟹ bot ∈ N"
begin

lemma inf_from_subs: "M ⊆ N ⟹ Inf_from M ⊆ Inf_from N"
  unfolding Inf_from_def by blast
    
    (* Splitting report Lemma 2 *)
lemma nobot_in_Red: ‹bot ∉ Red⇩F N›
proof -
  have ‹UNIV ⊨ {bot}›
    using entails_reflexive[of bot] entails_subsets[of "{bot}" UNIV "{bot}" "{bot}"] by fast
  then have non_red_entails_bot: ‹UNIV - (Red⇩F UNIV) ⊨ {bot}› using Red_F_Bot[of UNIV] by simp
  have ‹Inf_from UNIV ⊆ Red⇩I UNIV›
    unfolding Inf_from_def using Red_I_of_Inf_to_N[of _ UNIV] by blast
  then have sat_non_red: ‹saturated (UNIV - Red⇩F UNIV)›
    unfolding saturated_def Inf_from_def using Red_I_of_Red_F_subset[of "Red⇩F UNIV" UNIV] by blast 
  have ‹bot ∉ Red⇩F UNIV› 
    using statically_complete[OF sat_non_red non_red_entails_bot] by fast
  then show ?thesis using Red_F_of_subset[of _ UNIV] by auto
qed
  
  (* Splitting report Remark 3 *)
interpretation strict_calculus:
  statically_complete_calculus bot Inf entails Red⇩I_strict Red⇩F_strict
proof -
  interpret strict_calc: calculus bot Inf entails Red⇩I_strict Red⇩F_strict
  using strict_calc_if_nobot nobot_in_Red by blast 
    (* next property is not needed for the proof, but it is one of the claims from Rmk 3
    that must be verified *)
  have ‹saturated N ⟹ strict_calc.saturated N›
    unfolding saturated_def strict_calc.saturated_def Red⇩I_strict_def by blast
  have ‹strict_calc.saturated N ⟹ N ⊨ {bot} ⟹ bot ∈ N› for N
  proof -
    assume
      strict_sat: "strict_calc.saturated N" and
      entails_bot: "N ⊨ {bot}"
    have ‹bot ∉ N ⟹ Red⇩I_strict N = Red⇩I N› unfolding Red⇩I_strict_def by simp
    then have ‹bot ∉ N ⟹ saturated N›
      unfolding saturated_def using strict_sat by (simp add: strict_calc.saturated_def) 
    then have ‹bot ∉ N ⟹ bot ∈ N›
      using statically_complete[OF _ entails_bot] by simp
    then show ‹bot ∈ N› by auto 
  qed
  then show ‹statically_complete_calculus bot Inf entails Red⇩I_strict Red⇩F_strict›
    unfolding statically_complete_calculus_def statically_complete_calculus_axioms_def
    using strict_calc.calculus_axioms by blast
qed

end

locale dynamically_complete_calculus = calculus +
  assumes dynamically_complete:
    ‹is_derivation (⊳) Ns ⟹ fair Ns ⟹ llhd Ns ⊨ {bot} ⟹ ∃i. bot ∈ llnth Ns i›


(*******************************************)
section ‹Annotated Formulas and Consequence Relations›

datatype ('f, 'v::countable) AF = Pair (F_of: "'f") (A_of: "'v sign fset")

definition is_interpretation :: "'v sign set ⇒ bool" where
  ‹is_interpretation J = (∀v1∈J. (∀v2∈J. (to_V v1 = to_V v2 ⟶ v1 = v2)))›
  
typedef 'v propositional_interpretation = "{J :: 'v sign set. is_interpretation J}"
proof
  show ‹{} ∈ {J. is_interpretation J}› unfolding is_interpretation_def by blast 
qed
  
abbreviation "interp_of ≡ Abs_propositional_interpretation"
abbreviation "strip ≡ Rep_propositional_interpretation"

setup_lifting type_definition_propositional_interpretation

lift_definition belong_to :: "'v sign ⇒ 'v propositional_interpretation ⇒ bool" (infix "∈⇩J" 90)
  is "(∈)::('v sign ⇒ 'v sign set ⇒ bool)" .

definition total :: "'v propositional_interpretation ⇒ bool" where
  ‹total J ≡ (∀v. (∃v⇩J. v⇩J ∈⇩J J ∧ to_V v⇩J = v))›
  
typedef 'v total_interpretation = "{J :: 'v propositional_interpretation. total J}"
proof
  show ‹interp_of (Pos ` (UNIV :: 'v set)) ∈ {J. total J}›
    unfolding total_def   
  proof 
    show "∀v. ∃v⇩J. v⇩J ∈⇩J interp_of (range Pos) ∧ to_V v⇩J = v"
    proof
      fix v
      have "Pos v ∈⇩J interp_of (range Pos) ∧ to_V (Pos v) = v"
        by (simp add: Abs_propositional_interpretation_inverse belong_to.rep_eq is_interpretation_def)
      then show "∃v⇩J. v⇩J ∈⇩J interp_of (range Pos) ∧ to_V v⇩J = v" by blast
    qed
  qed
qed

abbreviation "total_interp_of ≡ (λx. Abs_total_interpretation (interp_of x))"
abbreviation "total_strip ≡ (λx. strip (Rep_total_interpretation x))"

lemma neg_notin_total_strip [simp]: ‹(neg a ∉ total_strip J) = (a ∈ total_strip J)›
proof
  assume neg_a_notin: ‹neg a ∉ total_strip J›
  have ‹∃b. to_V a = to_V b ∧ b ∈ total_strip J›
    by (metis Rep_total_interpretation belong_to.rep_eq mem_Collect_eq total_def)
  then show ‹a ∈ total_strip J›
    using neg_a_notin by (metis neg.simps to_V.elims)
next
  assume a_in: ‹a ∈ total_strip J›
  then have ‹∃b. to_V a = to_V b ∧ b ∉ total_strip J›
    by (metis Rep_propositional_interpretation is_interpretation_def mem_Collect_eq sign.simps(4)
        to_V.simps)
  then show ‹neg a ∉ total_strip J›
    using a_in by (metis neg.simps to_V.elims)
qed

lemma neg_in_total_strip [simp]: ‹(neg a ∈ total_strip J) = (a ∉ total_strip J)›
proof
  assume neg_a_notin: ‹neg a ∈ total_strip J›
  have ‹∃b. to_V a = to_V b ∧ b ∉ total_strip J›
   by (metis Rep_propositional_interpretation is_interpretation_def mem_Collect_eq sign.simps(4)
        to_V.simps)
  then show ‹a ∉ total_strip J›
    using neg_a_notin by (metis neg.simps to_V.elims)
next
  assume a_in: ‹a ∉ total_strip J›
  then have ‹∃b. to_V a = to_V b ∧ b ∈ total_strip J›
    by (metis Rep_total_interpretation belong_to.rep_eq mem_Collect_eq total_def)
  then show ‹neg a ∈ total_strip J›
    using a_in by (metis neg.simps to_V.elims)
qed

setup_lifting type_definition_total_interpretation

lift_definition belong_to_total :: "'v sign ⇒ 'v total_interpretation ⇒ bool" (infix "∈⇩t" 90)
  is "(∈⇩J)::('v sign ⇒ 'v propositional_interpretation ⇒ bool)" .

lemma in_total_to_strip [simp]: ‹a ∈⇩t J ⟷ a ∈ total_strip J›
  unfolding belong_to_total_def belong_to_def by simp

lemma neg_prop_interp: ‹(v::'v sign) ∈⇩J J ⟹ ¬ ((neg v) ∈⇩J J)›
proof transfer
  fix v J
  assume
    j_is: ‹is_interpretation (J:: 'v sign set)› and
    v_in: ‹v ∈ J›
  then show ‹¬ (neg v) ∈ J›
  proof (cases v)
    case (Pos C)
    then show ?thesis
      using is_Pos.simps
      by (metis is_interpretation_def j_is neg.simps(1) to_V.simps v_in)
  next
    case (Neg C)
    then show ?thesis
      using j_is v_in
      using is_interpretation_def by fastforce
  qed
qed

lemma neg_total_interp: ‹(v::'v sign) ∈⇩t J ⟹ ¬ ((neg v) ∈⇩t J)›
proof transfer
  fix v J
  assume v_in: ‹v ∈⇩J (J :: 'v propositional_interpretation)›
  show ‹¬ neg v ∈⇩J J›
    using neg_prop_interp[OF v_in] by simp
qed

lemma neg_notin_total_interp: ‹¬ (v ∈⇩t J) ⟹ ((neg v) ∈⇩t J)›
proof transfer
  fix v::"'v sign" and J
  assume 
    tot: ‹total J› and
    not_in: ‹¬ v ∈⇩J J›
  show ‹neg v ∈⇩J J›
    using tot not_in unfolding total_def
    by (metis belong_to_total.abs_eq eq_onp_def in_total_to_strip neg_in_total_strip tot)
qed

definition to_AF :: "'f ⇒ ('f, 'v::countable) AF" where
  ‹to_AF C = Pair C {||}›

lemma F_of_to_AF: ‹F_of (to_AF 𝒞) = 𝒞›
  unfolding to_AF_def
  by auto

lemma A_of_to_AF: ‹A_of (to_AF 𝒞) = {||}›
  unfolding to_AF_def
  by auto

lemma F_of_circ_to_AF_is_id [simp]: ‹F_of ∘ to_AF = id›
  by (fastforce simp: F_of_to_AF)

lemma A_of_circ_to_AF_is_empty_set [simp]: ‹A_of ∘ to_AF = (λ _. {||})›
  by (fastforce simp: A_of_to_AF) 

lemma F_of_propositional_clauses [simp]:
  ‹(∀ x ∈ set 𝒩. F_of x = bot) ⟹ map F_of 𝒩 = map (λ _. bot) 𝒩›
  using map_eq_conv
  by blast

lemma F_of_Pair [simp]: ‹F_of ∘ (λ(x, y). AF.Pair x y) = (λ(x, y). x)›
  by (smt (verit, ccfv_SIG) AF.sel(1) comp_apply cond_case_prod_eta old.prod.case)

lemma A_of_Pair [simp]: ‹A_of ∘ (λ(x, y). AF.Pair x y) = (λ(x, y). y)›
  by fastforce

lemma map_A_of_map2_Pair: ‹length A = length B ⟹ map A_of (map2 AF.Pair A B) = B›
proof -
  assume ‹length A = length B›
  then have ‹map2 (λ x y. y) A B = B›
    by (metis map_eq_conv map_snd_zip snd_def)
  then show ?thesis
    by auto 
qed  

definition Neg_set :: "'v sign set ⇒ 'v sign set" ("∼_" 55) where
  ‹∼V ≡ {neg v |v. v ∈ V}›

definition F_of_Inf :: "(('f, 'v::countable) AF) inference ⇒ 'f inference" where
  ‹F_of_Inf ι⇩A⇩F = (Infer (map F_of (prems_of ι⇩A⇩F)) (F_of (concl_of ι⇩A⇩F)))›

section ‹Lifting Calculi to Add Annotations›

locale calculus_with_annotated_consrel = sound_calculus bot Inf entails entails_sound Red⇩I Red⇩F
  for
    bot :: "'f" and
    Inf :: ‹'f inference set› and
    entails :: "'f set ⇒ 'f set ⇒ bool" (infix "⊨" 50) and
    entails_sound :: "'f set ⇒ 'f set ⇒ bool" (infix "⊨s" 50) and
    Red⇩I :: "'f set ⇒ 'f inference set" and
    Red⇩F :: "'f set ⇒ 'f set"
  + fixes
    fml :: ‹'v :: countable ⇒ 'f› and 
    asn :: ‹'f sign ⇒ 'v sign set›
  assumes
    fml_entails_C: ‹∀ a ∈ asn C. sound_cons.entails_neg {map_sign fml a} {C}› and
    C_entails_fml: ‹∀ a ∈ asn C. sound_cons.entails_neg {C} {map_sign fml a}› and
    asn_not_empty: ‹asn C ≠ {}›
begin

notation sound_cons.entails_neg (infix ‹⊨s⇩∼› 50)

lemma equi_entails_if_a_in_asns: ‹a ∈ asn C ⟹ a ∈ asn D ⟹ {C} ⊨s⇩∼ {D} ∧ {D} ⊨s⇩∼ {C}›
  by (smt (verit) C_entails_fml Un_commute consequence_relation.entails_cut fml_entails_C
    sound_cons.ext_cons_rel sup_bot_left)

lemma equi_entails_if_neg_a_in_asn:
  ‹a ∈ asn C ⟹ neg a ∈ asn D ⟹ {C} ⊨s⇩∼ {neg D} ∧ {neg D} ⊨s⇩∼ {C}›
proof (intro conjI)
  assume a_in_asn_C: ‹a ∈ asn C› and
         neg_a_in_asn_D: ‹neg a ∈ asn D›

  have fml_neg_is_neg_fml: ‹map_sign fml (neg x) = neg (map_sign fml x)› for x
    by (smt (verit, ccfv_threshold) neg.simps(1) neg_neg_A_is_A sign.simps(10) sign.simps(9)
        to_V.elims)  

  have ‹{C} ⊨s⇩∼ {map_sign fml a}›
    using a_in_asn_C C_entails_fml
    by blast
  then have ‹{C} ⊨s⇩∼ {neg D, map_sign fml a}›
    by (smt (verit, best) Un_upper2 consequence_relation.entails_subsets insert_is_Un
        sound_cons.ext_cons_rel sup_ge1)
  moreover have ‹{D} ⊨s⇩∼ {map_sign fml (neg a)}›
    using neg_a_in_asn_D C_entails_fml
    by blast
  then have ‹{neg (neg D)} ⊨s⇩∼ {neg (map_sign fml a)}›
    by (simp add: fml_neg_is_neg_fml)
  then have ‹{map_sign fml a} ⊨s⇩∼ {neg D}›
    using sound_cons.swap_neg_in_entails_neg
    by blast 
  then have ‹{map_sign fml a, C} ⊨s⇩∼ {neg D}›
    by (smt (verit, best) consequence_relation.entails_subsets insert_is_Un sound_cons.ext_cons_rel
        sup_ge1)
  ultimately show ‹{C} ⊨s⇩∼ {neg D}›
    using consequence_relation.entails_cut
    by (smt (verit, ccfv_threshold) Un_commute insert_is_Un sound_cons.ext_cons_rel sup.idem)
next
  assume a_in_asn_C: ‹a ∈ asn C› and
         neg_a_in_asn_D: ‹neg a ∈ asn D›

  have fml_neg_is_neg_fml: ‹map_sign fml (neg x) = neg (map_sign fml x)› for x
    by (smt (verit, ccfv_threshold) neg.simps(1) neg_neg_A_is_A sign.simps(10) sign.simps(9)
        to_V.elims)  

  have ‹{map_sign fml a} ⊨s⇩∼ {C}›
    using a_in_asn_C fml_entails_C
    by blast
  then have ‹{neg D, map_sign fml a} ⊨s⇩∼ {C}›
    by (smt (verit, best) Un_upper2 consequence_relation.entails_subsets insert_is_Un
        sound_cons.ext_cons_rel sup_ge1)
  moreover have ‹{map_sign fml (neg a)} ⊨s⇩∼ {D}›
    using neg_a_in_asn_D fml_entails_C
    by blast
  then have ‹{neg (map_sign fml a)} ⊨s⇩∼ {neg (neg D)}›
    by (simp add: fml_neg_is_neg_fml)
  then have ‹{neg D} ⊨s⇩∼ {map_sign fml a}›
    using sound_cons.swap_neg_in_entails_neg
    by blast
  then have ‹{neg D} ⊨s⇩∼ {map_sign fml a, C}›
    by (smt (verit, best) consequence_relation.entails_subsets insert_is_Un sound_cons.ext_cons_rel
        sup_ge1)
  ultimately show ‹{neg D} ⊨s⇩∼ {C}›
    using consequence_relation.entails_cut
    by (smt (verit, ccfv_threshold) Un_commute insert_is_Un sound_cons.ext_cons_rel sup.idem)
qed                                  

definition ιF_of :: "('f, 'v) AF inference ⇒ 'f inference" where
  ‹ιF_of ι = Infer (List.map F_of (prems_of ι)) (F_of (concl_of ι))›
  
definition propositional_projection :: "('f, 'v) AF set ⇒ ('f, 'v) AF set" ("proj⇩⊥") where
  ‹proj⇩⊥ 𝒩 = {𝒞. 𝒞 ∈ 𝒩 ∧ F_of 𝒞 = bot}›

lemma prop_proj_in: ‹proj⇩⊥ 𝒩 ⊆ 𝒩›
  unfolding propositional_projection_def by blast

definition enabled :: "('f, 'v) AF ⇒ 'v total_interpretation ⇒ bool" where
  "enabled 𝒞 J ≡ fset (A_of 𝒞) ⊆ (total_strip J)"

lemma subformula_of_enabled_formula_is_enabled: ‹A_of 𝒞 |⊂| A_of 𝒞' ⟹ enabled 𝒞' J ⟹ enabled 𝒞 J›
  unfolding enabled_def
  by (meson less_eq_fset.rep_eq pfsubset_imp_fsubset subset_trans)

lemma enabled_iff: ‹A_of 𝒞 = A_of 𝒞' ⟹ enabled 𝒞 J ⟷ enabled 𝒞' J›
  unfolding enabled_def
  by simp

definition enabled_set :: "('f, 'v) AF set ⇒ 'v total_interpretation ⇒ bool" where
  ‹enabled_set 𝒩 J = (∀𝒞∈𝒩. enabled 𝒞 J)›

lemma enabled_set_singleton [simp]: ‹enabled_set {𝒞} J ⟷ enabled 𝒞 J›
  by (auto simp add: enabled_set_def)

definition enabled_inf :: "('f, 'v) AF inference ⇒ 'v total_interpretation ⇒ bool" where
  ‹enabled_inf ι J = (∀𝒞∈ set (prems_of ι). enabled 𝒞 J)›
  
definition enabled_projection :: "('f, 'v) AF set ⇒ 'v total_interpretation ⇒ 'f set"
  (infix "proj⇩J" 60)  where
  ‹𝒩 proj⇩J J = {F_of 𝒞 |𝒞. 𝒞 ∈ 𝒩 ∧ enabled 𝒞 J}›

lemma Union_of_enabled_projection_is_enabled_projection: ‹(⋃ 𝒞 ∈ 𝒩. {𝒞} proj⇩J 𝒥) = 𝒩 proj⇩J 𝒥›
  unfolding enabled_projection_def
  by blast

lemma projection_of_enabled_subset:
  ‹fset B ⊆ total_strip J ⟹ {AF.Pair C (A |∪| B)} proj⇩J J = {AF.Pair C A} proj⇩J J›
  unfolding enabled_projection_def enabled_def
  by auto

lemma Un_of_enabled_projection_is_enabled_projection_of_Un:
  ‹(⋃ x. P x) proj⇩J J = (⋃ x. P x proj⇩J J)›
proof (intro subset_antisym subsetI)
  fix x
  assume ‹x ∈ (⋃ x. P x) proj⇩J J›
  then have ‹∃ y. x = F_of y ∧ enabled y J ∧ y ∈ (⋃ x. P x)›
    unfolding enabled_projection_def
    by blast
  then have ‹∃ y. x = F_of y ∧ enabled y J ∧ (∃ z. y ∈ P z)›
    by blast
  then have ‹∃ y. ∃ z. x = F_of y ∧ enabled y J ∧ y ∈ P z›
    by blast
  then show ‹x ∈ (⋃ x. P x proj⇩J J)›
    unfolding enabled_projection_def
    by blast
next
  fix x
  assume ‹x ∈ (⋃ x. P x proj⇩J J)›
  then have ‹∃ y. x ∈ P y proj⇩J J›
    by blast
  then have ‹∃ y. ∃ z. x = F_of z ∧ enabled z J ∧ z ∈ P y›
    unfolding enabled_projection_def
    by blast
  then show ‹x ∈ (⋃ x. P x) proj⇩J J›
    unfolding enabled_projection_def
    by blast
qed

lemma enabled_projection_of_Int_is_Int_of_enabled_projection:
  ‹x ∈ (⋂ S) proj⇩J J ⟹ x ∈ ⋂ { x proj⇩J J | x. x ∈ S }›
  unfolding enabled_projection_def
  by blast

definition enabled_projection_Inf :: "('f, 'v) AF inference set ⇒ 'v total_interpretation ⇒
  'f inference set" (infix "ιproj⇩J" 60) where
  ‹I ιproj⇩J J = {ιF_of ι | ι. ι ∈ I ∧ enabled_inf ι J}›

fun fml_ext :: "'v sign ⇒ 'f sign" where
  "fml_ext (Pos v) = Pos (fml v)" |
  "fml_ext (Neg v) = Neg (fml v)"

lemma fml_ext_is_mapping: ‹fml_ext v = map_sign fml v›
  by (metis fml_ext.cases fml_ext.simps(1) fml_ext.simps(2) sign.simps(10) sign.simps(9)) 

lemma fml_ext_preserves_sign: "is_Pos v ≡ is_Pos (fml_ext v)"
  by (induct v, auto)

lemma to_V_fml_ext [simp]: ‹to_V (fml_ext v) = fml (to_V v)›
  by (induct v, auto) 

lemma fml_ext_preserves_val: ‹to_V v1 = to_V v2 ⟹ to_V (fml_ext v1) = to_V (fml_ext v2)›
  by simp
 
definition sound_consistent :: "'v total_interpretation ⇒ bool" where
  ‹sound_consistent J ≡ ¬ (sound_cons.entails_neg (fml_ext ` (total_strip J)) {Pos bot})›
  
definition propositional_model :: "'v total_interpretation ⇒ ('f, 'v) AF set ⇒ bool"
  (infix "⊨⇩p" 50) where
  ‹J ⊨⇩p 𝒩 ≡ bot ∉ ((proj⇩⊥ 𝒩) proj⇩J J)›

lemma ‹J ⊨⇩p {}› 
  unfolding propositional_model_def enabled_projection_def propositional_projection_def by blast

text ‹The definition below is essentially the same as the one above since term‹(proj⇩⊥ 𝒩) proj⇩J J› is 
either empty or contains only bot›
definition propositional_model2 :: "'v total_interpretation ⇒ ('f, 'v) AF set ⇒ bool"
  (infix "⊨⇩p2" 50) where
  ‹J ⊨⇩p2 𝒩 ≡ ({} = ((proj⇩⊥ 𝒩) proj⇩J J))›

lemma subset_model_p2: ‹𝒩' ⊆ 𝒩 ⟹ J ⊨⇩p2 𝒩 ⟹ J ⊨⇩p2 𝒩'›
  by (simp add: enabled_projection_def propositional_model2_def propositional_projection_def 
      subset_eq)

lemma subset_not_model: ‹¬ J ⊨⇩p2 𝒩 ⟹ 𝒩 = 𝒩⇩1 ∪ 𝒩⇩2 ⟹ J ⊨⇩p2 𝒩⇩1 ⟹ ¬ J ⊨⇩p2 𝒩⇩2›
  unfolding propositional_model2_def propositional_projection_def enabled_projection_def by blast

lemma supset_not_model_p2: ‹𝒩' ⊆ 𝒩 ⟹ ¬ J ⊨⇩p2 𝒩' ⟹ ¬ J ⊨⇩p2 𝒩›
  using subset_model_p2 by blast

fun sign_to_atomic_formula :: "'v sign ⇒ 'v formula" where
  ‹sign_to_atomic_formula (Pos v) = Atom v› |
  ‹sign_to_atomic_formula (Neg v) = Not (Atom v)›

definition sign_set_to_formula_set :: "'v sign set ⇒ 'v formula set" where
  ‹sign_set_to_formula_set A = sign_to_atomic_formula ` A›

lemma form_shape_sign_set: ‹∀f∈sign_set_to_formula_set A. ∃v. f = Atom v ∨ f = Not (Atom v)›
  unfolding sign_set_to_formula_set_def
  by (metis image_iff sign_to_atomic_formula.elims)

definition AF_to_formula_set :: "('f, 'v) AF ⇒ 'v formula set" where
  (* /!\ this formula set is to be understood as a disjunction *)
  ‹AF_to_formula_set 𝒞 = sign_set_to_formula_set (neg ` fset (A_of 𝒞))›

definition AF_to_formula :: "('f, 'v) AF ⇒ 'v formula" where
  ‹AF_to_formula 𝒞 = BigOr (map sign_to_atomic_formula (map neg (list_of_fset (A_of 𝒞))))›

lemma form_shape_AF: ‹∀f∈AF_to_formula_set 𝒞. ∃v. f = Atom v ∨ f = Not (Atom v)›
  using form_shape_sign_set unfolding AF_to_formula_set_def by simp

definition AF_proj_to_formula_set_set :: "('f, 'v) AF set ⇒ 'v formula set set" where
  (* /!\ formula set set represents here a conjuction of disjunctions *)
  ‹AF_proj_to_formula_set_set 𝒩 = AF_to_formula_set ` (proj⇩⊥ 𝒩)›

definition AF_proj_to_formula_set :: "('f, 'v) AF set ⇒ 'v formula set" where
  ‹AF_proj_to_formula_set 𝒩 = AF_to_formula ` (proj⇩⊥ 𝒩)›

definition AF_assertions_to_formula :: "('f, 'v) AF ⇒ 'v formula" where
  ‹AF_assertions_to_formula 𝒞 = BigAnd (map sign_to_atomic_formula (list_of_fset (A_of 𝒞)))›

definition AF_assertions_to_formula_set :: "('f, 'v) AF set ⇒ 'v formula set" where
  ‹AF_assertions_to_formula_set 𝒩 = AF_assertions_to_formula ` 𝒩›

lemma F_to_𝒞_set: ‹∀F∈AF_proj_to_formula_set_set 𝒩. ∃𝒞∈proj⇩⊥ 𝒩. F =
  sign_to_atomic_formula ` neg ` fset (A_of 𝒞)›
  unfolding AF_proj_to_formula_set_set_def AF_to_formula_set_def sign_set_to_formula_set_def
  by auto

lemma F_to_𝒞: ‹∀F∈AF_proj_to_formula_set 𝒩. ∃𝒞∈proj⇩⊥ 𝒩. F =
   BigOr (map sign_to_atomic_formula (map neg (list_of_fset (A_of 𝒞))))›
  unfolding AF_proj_to_formula_set_def AF_to_formula_def by auto

lemma 𝒞_to_F_set: ‹∀𝒞∈proj⇩⊥ 𝒩. ∃F∈AF_proj_to_formula_set_set 𝒩. F =
  sign_to_atomic_formula ` neg ` fset (A_of 𝒞)›
  unfolding AF_proj_to_formula_set_set_def AF_to_formula_set_def sign_set_to_formula_set_def
  by auto

lemma 𝒞_to_F: ‹∀𝒞∈proj⇩⊥ 𝒩. ∃F∈AF_proj_to_formula_set 𝒩. F =
  BigOr (map sign_to_atomic_formula (map neg (list_of_fset (A_of 𝒞))))›
  unfolding AF_proj_to_formula_set_def AF_to_formula_def by auto

lemma form_shape_proj: ‹∀f∈⋃ (AF_proj_to_formula_set_set 𝒩). ∃v. f = Atom v ∨ f = Not (Atom v)›
  using form_shape_AF unfolding AF_proj_to_formula_set_set_def by simp

definition to_valuation :: "'v total_interpretation ⇒ 'v valuation" where
  ‹to_valuation J = (λa. Pos a ∈⇩t J)›

lemma val_strip_pos: ‹to_valuation J a ≡ Pos a ∈ total_strip J›
  unfolding to_valuation_def belong_to_total_def belong_to_def by simp

lemma val_strip_neg: ‹(¬ to_valuation J a) = (Neg a ∈ total_strip J)›
proof -
  have ‹(¬ to_valuation J a) = (¬ Pos a ∈ total_strip J)›
    using val_strip_pos by simp
  also have ‹(¬ Pos a ∈ total_strip J) = (Neg a ∈ total_strip J)›
  proof
    fix a J
    assume not_pos: ‹Pos (a::'v) ∉ total_strip J›
    have ‹is_interpretation (total_strip J)›
      using Rep_propositional_interpretation by blast 
    then show ‹Neg a ∈ total_strip J› 
      unfolding is_interpretation_def using total_def not_pos
      by (metis Rep_total_interpretation belong_to.rep_eq mem_Collect_eq to_V.elims)
  next
    assume neg: ‹Neg a ∈ total_strip J›
    have ‹is_interpretation (total_strip J)›
      using Rep_propositional_interpretation by blast
    then show ‹Pos a ∉ total_strip J›
      unfolding is_interpretation_def using neg
    by (metis sign.distinct(1) to_V.simps(1) to_V.simps(2))
  qed
  finally show ‹(¬ to_valuation J a) = (Neg a ∈ total_strip J)› .
qed

lemma equiv_prop_entails: ‹(J ⊨⇩p 𝒩) ⟷ (J ⊨⇩p2 𝒩)›
  unfolding propositional_model_def propositional_model2_def propositional_projection_def
    enabled_projection_def
  by blast

definition propositional_model3 :: "'v total_interpretation ⇒ ('f, 'v) AF set ⇒ bool"
  (infix "⊨⇩p3" 50) where
  ‹J ⊨⇩p3 𝒩 ≡ (∀F∈AF_proj_to_formula_set_set 𝒩. ∃f∈F. formula_semantics (to_valuation J) f)›

(* The interest of this first semantic characterization is that it is computable, but it is not
   convenient to apply the compactness results *)
lemma equiv_prop_entail2_sema:
  ‹(J ⊨⇩p2 𝒩) ⟷ (J ⊨⇩p3 𝒩)›
  unfolding propositional_model3_def propositional_model2_def enabled_projection_def enabled_def
proof
  assume empty_proj: ‹{} = {F_of 𝒞 |𝒞. 𝒞 ∈ proj⇩⊥ 𝒩 ∧ fset (A_of 𝒞) ⊆ total_strip J}›
  then have ‹∀𝒞∈proj⇩⊥ 𝒩. ∃v∈fset (A_of 𝒞). neg v ∈ total_strip J› 
    by (smt (verit, ccfv_SIG) empty_iff mem_Collect_eq neg.elims subsetI
        val_strip_neg val_strip_pos)
  show ‹∀F∈AF_proj_to_formula_set_set 𝒩. ∃f∈F. formula_semantics (to_valuation J) f›
  proof
    fix F
    assume F_in: ‹F ∈ AF_proj_to_formula_set_set 𝒩›
    then obtain 𝒞 where ‹𝒞 ∈ proj⇩⊥ 𝒩› and F_from_𝒞: ‹F = sign_to_atomic_formula ` neg ` fset (A_of 𝒞)›
      using F_to_𝒞_set by meson
    then have ‹∃v∈fset (A_of 𝒞). v ∉ total_strip J›
      using empty_proj by blast
    then obtain v where v_in: ‹v ∈ fset (A_of 𝒞)› and v_notin: ‹v ∉ total_strip J› by auto
    define f where ‹f = sign_to_atomic_formula (neg v)›
    then have ‹formula_semantics (to_valuation J) f›
      using v_notin
      by (smt (z3) belong_to.rep_eq belong_to_total.rep_eq formula_semantics.simps neg.elims
          sign_to_atomic_formula.simps to_valuation_def val_strip_neg)
    moreover have ‹f ∈ F›
      using F_from_𝒞 v_in f_def by blast
    ultimately show ‹∃f∈F. formula_semantics (to_valuation J) f› by auto
  qed
next
  assume F_sat: ‹∀F∈AF_proj_to_formula_set_set 𝒩. ∃f∈F. formula_semantics (to_valuation J) f›
  have ‹∀𝒞∈proj⇩⊥ 𝒩. ∃v∈fset (A_of 𝒞). neg v ∈ total_strip J›
  proof
    fix 𝒞
    assume ‹𝒞 ∈ proj⇩⊥ 𝒩›
    then obtain F where ‹F ∈ AF_proj_to_formula_set_set 𝒩› and
      F_from_𝒞: ‹F = sign_to_atomic_formula ` neg ` fset (A_of 𝒞)›
      using 𝒞_to_F_set by blast
    then have ‹∃f∈F. formula_semantics (to_valuation J) f›
      using F_sat by blast
    then obtain f where f_in: ‹f ∈ F› and sat_f: ‹formula_semantics (to_valuation J) f›
      by blast
    then obtain v where v_is: ‹f = sign_to_atomic_formula (neg v)› and v_in: ‹v ∈ fset (A_of 𝒞)›
      using F_from_𝒞 by blast
    then have ‹neg v ∈ total_strip J›
      using sat_f unfolding to_valuation_def
      by (smt (z3) belong_to.rep_eq belong_to_total.rep_eq formula_semantics.simps sign.exhaust
          sign_to_atomic_formula.simps val_strip_neg val_strip_pos)
    then show ‹∃v∈fset (A_of 𝒞). neg v ∈ total_strip J›
      using v_in by auto
  qed
  then show ‹{} = {F_of 𝒞 |𝒞. 𝒞 ∈ proj⇩⊥ 𝒩 ∧ fset (A_of 𝒞) ⊆ total_strip J}›
    by (smt (verit, ccfv_threshold) empty_Collect_eq is_Pos.cases neg.simps(1) neg.simps(2) subsetD
        val_strip_neg val_strip_pos)
qed

(* this characterization can be used to apply the compactness from Michaelis & Nipkow but it uses
   something that can't be computed (SOME) *)
lemma equiv_prop_entail2_sema2:
  ‹(J ⊨⇩p2 𝒩) ⟷ (∀F∈AF_proj_to_formula_set 𝒩. formula_semantics (to_valuation J) F)›
  unfolding propositional_model2_def enabled_projection_def enabled_def
proof
  assume empty_proj: ‹{} = {F_of 𝒞 |𝒞. 𝒞 ∈ proj⇩⊥ 𝒩 ∧ fset (A_of 𝒞) ⊆ total_strip J}›
  show ‹∀F∈AF_proj_to_formula_set 𝒩. formula_semantics (to_valuation J) F›
  proof
    fix F
    assume F_in: ‹F ∈ AF_proj_to_formula_set 𝒩›
    then obtain 𝒞 where ‹𝒞 ∈ proj⇩⊥ 𝒩› and 
      F_from_𝒞: ‹F = BigOr (map sign_to_atomic_formula (map neg (list_of_fset (A_of 𝒞))))›
      using F_to_𝒞 by meson
    then have ‹∃v∈fset (A_of 𝒞). v ∉ total_strip J›
      using empty_proj by blast
    then obtain v where v_in: ‹v ∈ fset (A_of 𝒞)› and v_notin: ‹v ∉ total_strip J› by auto
    define f where ‹f = sign_to_atomic_formula (neg v)›
    then have ‹formula_semantics (to_valuation J) f›
      using v_notin
      by (smt (z3) belong_to.rep_eq belong_to_total.rep_eq formula_semantics.simps neg.elims
          sign_to_atomic_formula.simps to_valuation_def val_strip_neg)
    moreover have ‹f ∈ set (map sign_to_atomic_formula (map neg (list_of_fset (A_of 𝒞))))›
      unfolding f_def using fset_map2[OF v_in, of sign_to_atomic_formula neg] .
    ultimately have ‹∃f∈set (map sign_to_atomic_formula (map neg (list_of_fset (A_of 𝒞)))).
     formula_semantics (to_valuation J) f›
      by blast
    then show ‹formula_semantics (to_valuation J) F›
      using BigOr_semantics[of "to_valuation J"
          "map sign_to_atomic_formula (map neg (list_of_fset (A_of 𝒞)))"] F_from_𝒞
      by meson
    qed
next
  assume F_sat: ‹∀F∈AF_proj_to_formula_set 𝒩. formula_semantics (to_valuation J) F›
  have ‹∀𝒞∈proj⇩⊥ 𝒩. ∃v∈fset (A_of 𝒞). neg v ∈ total_strip J›
  proof
    fix 𝒞
    assume 𝒞_in: ‹𝒞 ∈ proj⇩⊥ 𝒩›
    define F where ‹F = AF_to_formula 𝒞›
    then have ‹F ∈ AF_proj_to_formula_set 𝒩›
      unfolding AF_proj_to_formula_set_def using 𝒞_in by blast
    then have ‹formula_semantics (to_valuation J) F› using F_sat by blast
    then have ‹∃f∈set (map sign_to_atomic_formula (map neg (list_of_fset (A_of 𝒞)))).
      formula_semantics (to_valuation J) f›
      using BigOr_semantics[of "to_valuation J"] unfolding F_def AF_to_formula_def by simp
    then obtain f where 
      f_in: ‹f ∈ set (map sign_to_atomic_formula (map neg (list_of_fset (A_of 𝒞))))›
      and val_f: ‹formula_semantics (to_valuation J) f› by blast
    obtain v where v_in: ‹v ∈ fset (A_of 𝒞)› and f_is: ‹f = sign_to_atomic_formula (neg v)›
      using f_in unfolding list_of_fset_def
      by (smt (z3) exists_fset_of_list fset_of_list.rep_eq image_iff list.set_map someI)
    have ‹neg v ∈ total_strip J›
      using f_is val_f unfolding to_valuation_def
      by (metis (mono_tags, lifting) belong_to.rep_eq belong_to_total.rep_eq 
          formula_semantics.simps(1) formula_semantics.simps(3) sign_to_atomic_formula.cases
          sign_to_atomic_formula.simps(1) sign_to_atomic_formula.simps(2) val_f val_strip_neg)
    then show ‹∃v∈fset (A_of 𝒞). neg v ∈ total_strip J›
      using v_in by blast
  qed
  then show ‹{} = {F_of 𝒞 |𝒞. 𝒞 ∈ proj⇩⊥ 𝒩 ∧ fset (A_of 𝒞) ⊆ total_strip J}›
    by (smt (verit, ccfv_threshold) empty_Collect_eq is_Pos.cases neg.simps(1) neg.simps(2) subsetD
        val_strip_neg val_strip_pos)
qed

lemma equiv_prop_entail_sema:
  ‹(J ⊨⇩p 𝒩) ⟷ (J ⊨⇩p3 𝒩)›
  using equiv_prop_entails equiv_prop_entail2_sema by presburger


lemma ‹f ` fset A = set (map f (list_of_fset A))›
proof
  show ‹f ` fset A ⊆ set (map f (list_of_fset A))›
  proof
    fix v
    assume v_in: ‹v ∈ f ` fset A›
    then obtain a where "a |∈| A" "f a = v"
     by blast 
    then show ‹v ∈ set (map f (list_of_fset A))›
      unfolding list_of_fset_def
      by (metis fset_map2 list_of_fset_def map_ident)
  qed
next
  show ‹set (map f (list_of_fset A)) ⊆ f ` fset A›
  proof
    fix v
    assume ‹v ∈ set (map f (list_of_fset A))›
    then obtain a where "a |∈| A" "f a = v"
      unfolding list_of_fset_def
      by (metis (mono_tags, lifting) exists_fset_of_list fimage.rep_eq fimageE fset_of_list.rep_eq 
          set_map someI_ex)
    then show ‹v ∈ f ` fset A›
      by blast
  qed
qed

lemma equiv_prop_sema1_sema2:
  ‹(J ⊨⇩p3 𝒩) ⟷
   (∀F∈AF_proj_to_formula_set 𝒩. formula_semantics (to_valuation J) F)›
  using equiv_prop_entail2_sema2 equiv_prop_entail2_sema
  unfolding propositional_model3_def by auto


lemma equiv_enabled_assertions_sema:
  ‹(enabled_set 𝒩 J) ⟷ (∀F∈AF_assertions_to_formula_set 𝒩. formula_semantics (to_valuation J) F)›
  unfolding enabled_projection_def enabled_def enabled_set_def
proof
  assume enab_N: ‹∀𝒞∈𝒩. fset (A_of 𝒞) ⊆ total_strip J› 
  show ‹∀F∈AF_assertions_to_formula_set 𝒩. formula_semantics (to_valuation J) F›
  proof
    fix F
    assume F_in: ‹F ∈ AF_assertions_to_formula_set 𝒩›
    then obtain 𝒞 where 𝒞_in: ‹𝒞 ∈ 𝒩› and 
      F_from_𝒞: ‹F = BigAnd (map sign_to_atomic_formula (list_of_fset (A_of 𝒞)))›
      unfolding AF_assertions_to_formula_def AF_assertions_to_formula_set_def by auto
    have ‹∀f∈set (map sign_to_atomic_formula (list_of_fset (A_of 𝒞))).
      formula_semantics (to_valuation J) f›
    proof
      fix f
      assume f_in: ‹f ∈ set (map sign_to_atomic_formula (list_of_fset (A_of 𝒞)))›
      define L where ‹L = (list_of_fset (A_of 𝒞))›
      then obtain a v where f_is: ‹sign_to_atomic_formula a = f› and a_in: ‹a ∈ set L›
        and v_is: ‹to_V a = v›
        using f_in by auto
      have ‹a ∈ fset (A_of 𝒞)›
        using a_in unfolding L_def by (smt (verit, ccfv_threshold) exists_fset_of_list
            fset_of_list.rep_eq list_of_fset_def someI_ex)
      then have a_in: ‹a ∈ total_strip J›
        using enab_N 𝒞_in by blast
      consider (Pos) "a = Pos v" | (Neg) ‹a = Neg v›
        using v_is is_Neg_to_V is_Pos_to_V by blast
      then show ‹formula_semantics (to_valuation J) f›
      proof cases
        case Pos
        then have ‹f = Atom v› using f_is by auto
        then show ?thesis
          using a_in unfolding to_valuation_def belong_to_total_def belong_to_def
          by (simp add: Pos)
      next
        case Neg
        then have ‹f = Not (Atom v)› using f_is by auto
        then show ?thesis
          using a_in Neg to_valuation_def val_strip_neg by force
      qed
    qed
    then show ‹formula_semantics (to_valuation J) F›
      using BigAnd_semantics[of "to_valuation J"
          "map sign_to_atomic_formula (list_of_fset (A_of 𝒞))"] F_from_𝒞 by blast
  qed
next
  assume F_sat: ‹∀F∈AF_assertions_to_formula_set 𝒩. formula_semantics (to_valuation J) F›
  have ‹∀𝒞∈𝒩. ∀a∈fset (A_of 𝒞). a ∈ total_strip J›
  proof clarify
    fix 𝒞 a
    assume 
      𝒞_in: ‹𝒞 ∈ 𝒩› and
      a_in: ‹a ∈ fset (A_of 𝒞)›
    define F where ‹F = AF_assertions_to_formula 𝒞›
    then have ‹F ∈ AF_assertions_to_formula_set 𝒩›
      unfolding AF_assertions_to_formula_set_def using 𝒞_in by blast
    then have ‹formula_semantics (to_valuation J) F› using F_sat by blast
    then have all_f_sat: ‹∀f∈set (map sign_to_atomic_formula (list_of_fset (A_of 𝒞))).
      formula_semantics (to_valuation J) f›
      using BigAnd_semantics[of "to_valuation J"] unfolding F_def AF_assertions_to_formula_def
      by simp
    define f where ‹f = sign_to_atomic_formula a›
    then have ‹f ∈ set (map sign_to_atomic_formula (list_of_fset (A_of 𝒞)))›
      using a_in fset_map2 by fastforce
    then have f_sat: ‹formula_semantics (to_valuation J) f›
      using all_f_sat by auto
    then show ‹a ∈ total_strip J›
      using f_def unfolding to_valuation_def
      by (metis f_sat belong_to.rep_eq belong_to_total.rep_eq formula_semantics.simps(1)
          formula_semantics.simps(3) sign_to_atomic_formula.elims val_strip_neg)
  qed
  then show ‹∀𝒞∈𝒩. fset (A_of 𝒞) ⊆ total_strip J› by blast
qed

definition sound_propositional_model :: "'v total_interpretation ⇒ ('f, 'v) AF set ⇒ bool"
  (infix "⊨s⇩p" 50) where
  ‹J ⊨s⇩p 𝒩 ≡ (bot ∉ ((enabled_projection (propositional_projection 𝒩) J)) ∨
    ¬ sound_consistent J)›

definition propositionally_unsatisfiable :: "('f, 'v) AF set ⇒ bool" where
  ‹propositionally_unsatisfiable 𝒩 ≡ ∀J. ¬ (J ⊨⇩p 𝒩)›

lemma unsat_simp: 
  assumes 
    ‹¬ sat (S' ∪ S::'v formula set)›
    ‹sat S'›
    ‹⋃ (atoms ` S') ∩ ⋃ (atoms ` S) = {}›
  shows
    ‹¬ sat S›
  unfolding sat_def
proof
  assume contra: ‹∃𝒜. ∀F∈S. formula_semantics 𝒜 F›
  then obtain 𝒜S where AS_is: ‹∀F∈S. formula_semantics 𝒜S F› by blast
  obtain 𝒜F where AF_is: ‹∀F∈S'. formula_semantics 𝒜F F› using assms(2) unfolding sat_def by blast
  define 𝒜 where ‹𝒜 = (λa. if a ∈ ⋃ (atoms ` S') then 𝒜F a else 𝒜S a)›
  have ‹∀F∈S'. formula_semantics 𝒜 F›
    using AF_is relevant_atoms_same_semantics unfolding 𝒜_def
    by (smt (verit, best) UN_I)
  moreover have ‹∀F∈S. formula_semantics 𝒜 F›
    using AS_is relevant_atoms_same_semantics assms(3) unfolding 𝒜_def
    by (smt (verit, del_insts) Int_iff UN_I empty_iff)
  ultimately have ‹∀F'∈(S'∪S). formula_semantics 𝒜 F'› by blast
  then show False
    using assms(1) unfolding sat_def by blast
qed

lemma proj_to_form_un: ‹AF_proj_to_formula_set (A ∪ B) = 
  AF_proj_to_formula_set A ∪ AF_proj_to_formula_set B›
  unfolding AF_proj_to_formula_set_def propositional_projection_def by blast

lemma unsat_AF_simp: 
  assumes 
    ‹¬ sat (AF_proj_to_formula_set (S' ∪ S))›
    ‹sat (AF_proj_to_formula_set S')›
    ‹⋃ (atoms ` (AF_proj_to_formula_set S')) ∩ ⋃ (atoms ` (AF_proj_to_formula_set S)) = {}›
  shows
    ‹¬ sat (AF_proj_to_formula_set S)›
  using unsat_simp assms proj_to_form_un by metis

lemma set_list_of_fset[simp]: ‹set (list_of_fset A) = fset A›
  unfolding list_of_fset_def
  by (smt (verit, del_insts) exists_fset_of_list fset_of_list.rep_eq someI_ex)

lemma vars_in_assertion: ‹to_V ` (set (list_of_fset A)) = to_V ` (fset A)›
  by simp

lemma atoms_bigor: ‹atoms (BigOr L) = ⋃ (atoms ` (set L))›
  unfolding BigOr_def by (induction L) auto

lemma atoms_neg: ‹atoms (sign_to_atomic_formula (neg A)) = atoms (sign_to_atomic_formula A)›
  by (metis formula.simps(92) neg.elims sign_to_atomic_formula.simps(1)
      sign_to_atomic_formula.simps(2))

lemma set_maps_list_of_fset: ‹set (map sign_to_atomic_formula (map neg (list_of_fset A))) = 
  sign_to_atomic_formula ` neg ` fset A›
  using set_map by auto

lemma atoms_to_V_mono: ‹atoms (sign_to_atomic_formula A) = {to_V A}›
  by (metis formula.set(1) formula.set(3) sign_to_atomic_formula.simps(1)
      sign_to_atomic_formula.simps(2) to_V.elims)

lemma atoms_to_V: ‹⋃(atoms ` sign_to_atomic_formula ` A) = to_V ` A›
proof -
  have ‹⋃(atoms ` sign_to_atomic_formula ` A) = ⋃{{to_V a} |a. a ∈ A}›
    using atoms_to_V_mono by auto
  also have ‹... = to_V ` A›
    by blast
  finally show ‹⋃(atoms ` sign_to_atomic_formula ` A) = to_V ` A› .
qed

lemma atoms_to_V_AF: ‹atoms (AF_to_formula (Pair C A)) = to_V ` (fset A)›
proof -
  have ‹atoms (AF_to_formula (Pair C A)) = ⋃ (atoms ` sign_to_atomic_formula ` fset A)›
    using atoms_bigor set_maps_list_of_fset atoms_neg unfolding AF_to_formula_def
    by (smt (z3) AF.sel(2) image_iff subsetI subset_antisym)
  also have ‹... = to_V ` (fset A)›
    using atoms_to_V by auto
  ultimately show ‹atoms (AF_to_formula (Pair C A)) = to_V ` (fset A)› by simp
qed

lemma atoms_to_V_A_of: ‹atoms (AF_to_formula 𝒞) = to_V ` (fset (A_of 𝒞))›
  using atoms_to_V_AF
  by (metis AF.collapse)

lemma atoms_to_V_un: ‹⋃(atoms ` AF_to_formula ` 𝒮) = ⋃{to_V ` fset A |A. A ∈ A_of ` 𝒮}›
proof -
  have ‹(x ∈ (atoms ` AF_to_formula ` 𝒮)) = (x ∈ {to_V ` (fset A) |A. A ∈ A_of ` 𝒮})› for x
    using atoms_to_V_A_of by blast
  then show ?thesis
    by (smt (verit, ccfv_SIG) Collect_cong Sup_set_def UNION_singleton_eq_range mem_Collect_eq)
qed

lemma atoms_simp: ‹⋃ (atoms ` (AF_proj_to_formula_set S)) = to_V ` ⋃ (fset ` (A_of ` (proj⇩⊥ S)))›
proof -
  have ‹⋃ (atoms ` (AF_proj_to_formula_set S)) = ⋃{to_V ` fset A | A. A ∈ A_of ` (proj⇩⊥ S)}›
    unfolding AF_proj_to_formula_set_def using atoms_to_V_un by auto
  also have ‹... = to_V ` ⋃ (fset ` (A_of ` (proj⇩⊥ S)))›
    by blast
  finally show ?thesis .
qed

lemma val_from_interp: ‹∀𝒜. ∃J. 𝒜 = to_valuation J›
proof
  fix 𝒜
  define J_bare where ‹J_bare = {Pos a |(a::'v). 𝒜 a} ∪ {Neg a |a. ¬ 𝒜 a}›
  then have interp_J_bare: ‹is_interpretation J_bare›
    unfolding is_interpretation_def
    by force
  then have total_J_bare: ‹total (interp_of J_bare)›
    unfolding total_def using J_bare_def
    by (metis (mono_tags, lifting) Abs_propositional_interpretation_inverse Un_iff belong_to.rep_eq
        mem_Collect_eq to_V.simps)
  define J where ‹J = total_interp_of J_bare›
  have ‹𝒜 = to_valuation J›
  proof
    fix a::'v
    show ‹𝒜 a = to_valuation J a›
      using J_def J_bare_def Abs_propositional_interpretation_inverse 
        Abs_total_interpretation_inverse interp_J_bare total_J_bare to_valuation_def val_strip_pos
      by fastforce
  qed
  then show ‹∃J. 𝒜 = to_valuation J›
    by fast
qed

lemma interp_from_val: ‹∀J. ∃𝒜. 𝒜 = to_valuation J›
  unfolding to_valuation_def by auto


lemma compactness_unsat: ‹(¬ sat (S::'v formula set)) ⟷ (∃s⊆S. finite s ∧ ¬ sat s)›
  using compactness[of S] unfolding fin_sat_def by blast

lemma never_enabled_finite_subset: 
  ‹∀J. ¬ enabled_set 𝒩 J ⟹ ∃𝒩'⊆𝒩. finite 𝒩' ∧ (∀J. ¬ enabled_set 𝒩' J)›
proof -
  assume not_enab_N: ‹∀J. ¬ enabled_set 𝒩 J›
  then have ‹¬ sat (AF_assertions_to_formula_set 𝒩)›
    unfolding sat_def using equiv_enabled_assertions_sema[of 𝒩] val_from_interp
    by metis
  then obtain S' where S'_sub: ‹S' ⊆ AF_assertions_to_formula ` 𝒩› and S'_fin: ‹finite S'› and
    S'_unsat: ‹¬ sat S'›
    using compactness_unsat unfolding AF_assertions_to_formula_set_def by metis
  obtain 𝒩' where N'_sub: ‹𝒩' ⊆ 𝒩› and N'_fin: ‹finite 𝒩'›
    and S'_im: ‹S' = AF_assertions_to_formula ` 𝒩'›
    using finite_subset_image[OF S'_fin S'_sub] by blast
  have not_enab_N': ‹∀J. ¬ enabled_set 𝒩' J›
    using equiv_enabled_assertions_sema[of 𝒩'] S'_unsat S'_im interp_from_val 
    unfolding sat_def AF_assertions_to_formula_set_def by blast
  then show ‹∃𝒩' ⊆ 𝒩. finite 𝒩' ∧ (∀J. ¬ enabled_set 𝒩' J)›
    using N'_sub N'_fin by auto
qed


lemma compactness_AF_proj: ‹(∀J. ¬ J ⊨⇩p2 𝒩) ⟷ (∃𝒩'⊆𝒩. finite 𝒩' ∧ (∀J. ¬ J ⊨⇩p2 𝒩'))›
proof -
  define ℱ where ‹ℱ = AF_proj_to_formula_set 𝒩›
  have ‹(∀J. ¬ J ⊨⇩p2 𝒩) ⟷ (∀J. ∃F∈ℱ. ¬ formula_semantics (to_valuation J) F)›
    by (simp add: ℱ_def equiv_prop_entail2_sema2)
  also have 
    ‹(∀J. ∃F∈ℱ. ¬ formula_semantics (to_valuation J) F) ⟷ (∀𝒜. ∃F∈ℱ. ¬ formula_semantics 𝒜 F)›
    using val_from_interp by metis
  also have ‹(∀𝒜. ∃F∈ℱ. ¬ formula_semantics 𝒜 F) ⟷ (¬ sat ℱ)›
    unfolding sat_def by blast
  also have ‹(¬ sat ℱ) ⟷ (∃ℱ'⊆ℱ. finite ℱ' ∧ ¬ sat ℱ')›
    using compactness_unsat[of ℱ] .
  also have ‹(∃ℱ'⊆ℱ. finite ℱ' ∧ ¬ sat ℱ') ⟷ (∃ℱ'⊆ℱ. finite ℱ' ∧ (∀𝒜. ∃F∈ℱ'. ¬ formula_semantics 𝒜 F))›
    unfolding sat_def by auto
  also have ‹... ⟷ (∃ℱ'⊆ℱ. finite ℱ' ∧ (∀J. ∃F∈ℱ'. ¬ formula_semantics (to_valuation J) F))›
    by (metis val_from_interp)
  also have ‹... ⟷ (∃𝒩'⊆𝒩. finite 𝒩' ∧ (∀J. ¬ J ⊨⇩p2 𝒩'))›
  proof
    assume ‹∃ℱ'⊆ℱ. finite ℱ' ∧ (∀J. ∃F∈ℱ'. ¬ formula_semantics (to_valuation J) F)›
    then obtain ℱ' where F'_sub: ‹ℱ'⊆ℱ› and F'_fin: ‹finite ℱ'› and
      F'_unsat: ‹∀J. ∃F∈ℱ'. ¬ formula_semantics (to_valuation J) F›
      by auto
    have ‹∀F∈ℱ'. ∃𝒞∈(proj⇩⊥ 𝒩). AF_to_formula 𝒞 = F›
      using F'_sub ℱ_def unfolding AF_proj_to_formula_set_def by blast
    then obtain 𝒩' where F'_is_map: ‹ℱ' = AF_to_formula ` 𝒩'› and N'_in_proj: ‹𝒩' ⊆ proj⇩⊥ 𝒩› and
      N'_fin: ‹finite 𝒩'›
      using F'_fin
      by (metis AF_proj_to_formula_set_def F'_sub ℱ_def finite_subset_image)
    have ‹proj⇩⊥ 𝒩' = 𝒩'›                               
      using N'_in_proj unfolding propositional_projection_def by blast
    then have F'_is: ‹ℱ' = AF_proj_to_formula_set 𝒩'›
      unfolding AF_proj_to_formula_set_def using F'_is_map by simp
    have N'_sub: ‹𝒩' ⊆ 𝒩›
      using prop_proj_in N'_in_proj by auto
    have N'_unsat: ‹∀J. ¬ J ⊨⇩p2 𝒩'›
      using equiv_prop_entail2_sema2[of _ 𝒩'] F'_is F'_unsat 
      by blast
    show ‹∃𝒩'⊆𝒩. finite 𝒩' ∧ (∀J. ¬ J ⊨⇩p2 𝒩')›
      using N'_sub N'_fin N'_unsat by blast
  next
    assume ‹∃𝒩'⊆𝒩. finite 𝒩' ∧ (∀J. ¬ J ⊨⇩p2 𝒩')›
    then obtain 𝒩' where N'_sub: ‹𝒩' ⊆ 𝒩› and N'_fin: ‹finite 𝒩'› and N'_unsat: ‹∀J. ¬ J ⊨⇩p2 𝒩'›
      by auto
    define ℱ' where ‹ℱ' = AF_proj_to_formula_set 𝒩'›
    then have ‹ℱ' ⊆ ℱ›
      using N'_sub unfolding ℱ_def AF_proj_to_formula_set_def propositional_projection_def by blast
    moreover have ‹finite ℱ'›
      using ℱ'_def N'_fin unfolding AF_proj_to_formula_set_def propositional_projection_def by simp
    moreover have ‹∀J. ∃F∈ℱ'. ¬ formula_semantics (to_valuation J) F›
      using N'_unsat equiv_prop_entail2_sema2[of _ 𝒩'] unfolding ℱ'_def by blast
    ultimately show ‹∃ℱ'⊆ℱ. finite ℱ' ∧ (∀J. ∃F∈ℱ'. ¬ formula_semantics (to_valuation J) F)›
      by auto
  qed
  finally show ‹(∀J. ¬ J ⊨⇩p2 𝒩) ⟷ (∃𝒩'⊆𝒩. finite 𝒩' ∧ (∀J. ¬ J ⊨⇩p2 𝒩'))›
    .
qed

lemma prop_unsat_compactness:
  ‹propositionally_unsatisfiable A ⟹ ∃ B ⊆ A. finite B ∧ propositionally_unsatisfiable B›
  by (meson compactness_AF_proj equiv_prop_entails propositionally_unsatisfiable_def)

definition ℰ_from :: ‹('f, 'v) AF set ⇒ ('f, 'v) AF set› where
  ‹ℰ_from 𝒩 ≡ {Pair bot {|neg a|} |a. ∃𝒞∈𝒩. a ∈ fset (A_of 𝒞)}›

lemma prop_proj_ℰ_from: ‹proj⇩⊥ (ℰ_from 𝒩) = ℰ_from 𝒩›
  unfolding propositional_projection_def ℰ_from_def by auto

lemma prop_proj_sub: ‹proj⇩⊥ 𝒩 = 𝒩 ⟹ 𝒩' ⊆ 𝒩 ⟹ proj⇩⊥ 𝒩' = 𝒩'›
  unfolding propositional_projection_def by blast

lemma prop_proj_distrib: ‹proj⇩⊥ (A ∪ B) = proj⇩⊥ A ∪ proj⇩⊥ B›
  unfolding propositional_projection_def by blast

lemma v_in_ℰ: ‹Pair bot {|Pos v|} ∈ ℰ_from 𝒩 ∨ Pair bot {|Neg v|} ∈ ℰ_from 𝒩 ⟹
  ∃𝒞∈𝒩. v ∈ to_V ` (fset (A_of 𝒞))›
  unfolding ℰ_from_def by (smt (verit, ccfv_threshold) AF.sel(2) fthe_felem_eq image_iff
    mem_Collect_eq neg.simps(1) neg.simps(2) to_V.elims to_V.simps(1) to_V.simps(2))

lemma a_in_ℰ: ‹∃J. J ⊨⇩p2 ℰ_from 𝒩 ⟹ Pair bot {|neg a|} ∈ ℰ_from 𝒩 ⟹
  ¬ (Pair bot {|a|} ∈ ℰ_from 𝒩)›
proof
  assume
    e_sat: ‹∃J. J ⊨⇩p2 ℰ_from 𝒩›  and
    neg_a_in: ‹Pair bot {|neg a|} ∈ ℰ_from 𝒩› and
    a_in: ‹AF.Pair bot {|a|} ∈ ℰ_from 𝒩›
  obtain J where J_sat_e: ‹J ⊨⇩p2 ℰ_from 𝒩›
    using e_sat by blast
  have neg_a_in_J: ‹neg a ∈ total_strip J›
    using a_in J_sat_e unfolding propositional_model2_def ℰ_from_def enabled_projection_def
      propositional_projection_def enabled_def by (smt (verit, ccfv_SIG) AF.collapse AF.inject
      bot_fset.rep_eq empty_iff empty_subsetI finsert.rep_eq insert_subset mem_Collect_eq
      neg.simps(1) neg.simps(2) to_V.elims val_strip_neg val_strip_pos)
  have ‹neg a ∈ total_strip J ⟹ ¬ J ⊨⇩p2 ℰ_from 𝒩›
    using neg_a_in J_sat_e enabled_def
      enabled_projection_def prop_proj_ℰ_from propositional_model2_def by fastforce
  then show False
    using neg_a_in_J J_sat_e by blast
qed

lemma equiv_ℰ_enabled_𝒩:
  shows ‹J ⊨⇩p2 ℰ_from 𝒩 ⟷ enabled_set 𝒩 J›
  unfolding propositional_model2_def enabled_set_def enabled_def propositional_projection_def
    enabled_projection_def
proof
  assume empty_proj_E: ‹{} = {F_of 𝒞 |𝒞. 𝒞 ∈ {𝒞 ∈ ℰ_from 𝒩. F_of 𝒞 = bot} ∧
    fset (A_of 𝒞) ⊆ total_strip J}›
  have ‹∀𝒞∈ℰ_from 𝒩. F_of 𝒞 = bot› using ℰ_from_def[of 𝒩] by auto
  then have a_in_E: ‹∀𝒞∈ℰ_from 𝒩. ∃a∈fset (A_of 𝒞). a ∉ total_strip J›
    using empty_proj_E by blast
  then have ‹∀𝒞∈ℰ_from 𝒩. ∀a∈fset (A_of 𝒞). a ∉ total_strip J›
    unfolding ℰ_from_def by fastforce
  moreover have ‹∀𝒞∈𝒩. ∀a∈fset (A_of 𝒞). ∃𝒞'∈ℰ_from 𝒩. neg a ∈ fset (A_of 𝒞')›
    unfolding ℰ_from_def by fastforce
  ultimately have ‹∀𝒞∈𝒩. ∀a∈fset (A_of 𝒞). a ∈ total_strip J›
    by fastforce
  then show ‹∀𝒞∈𝒩. fset (A_of 𝒞) ⊆ total_strip J›
    by blast
next
  assume enabled_𝒞: ‹∀𝒞∈𝒩. fset (A_of 𝒞) ⊆ total_strip J›
  have ‹∀𝒞∈ℰ_from 𝒩. ∀a∈fset (A_of 𝒞). ∃𝒞'∈𝒩. neg a ∈ fset (A_of 𝒞')›
    unfolding ℰ_from_def
    by (smt (verit) AF.exhaust_sel AF.inject bot_fset.rep_eq empty_iff finsert.rep_eq insertE
        is_Pos.cases mem_Collect_eq neg.simps)
  then have ‹∀𝒞∈ℰ_from 𝒩. ∀a∈fset (A_of 𝒞). a ∉ total_strip J›
    using enabled_𝒞 by (meson belong_to.rep_eq neg_prop_interp subsetD)
  then have ‹∀𝒞∈ℰ_from 𝒩. (¬ fset (A_of 𝒞) ⊆ total_strip J)›
    using ℰ_from_def by fastforce
  then show ‹{} = {F_of 𝒞 |𝒞. 𝒞 ∈ {𝒞 ∈ ℰ_from 𝒩. F_of 𝒞 = bot} ∧ fset (A_of 𝒞) ⊆ total_strip J}›
    by blast
qed

definition AF_entails :: "('f, 'v) AF set ⇒ ('f, 'v) AF set ⇒ bool" (infix "⊨⇩A⇩F" 50) where
  ‹AF_entails ℳ 𝒩 ≡ (∀J. (enabled_set 𝒩 J ⟶ ℳ proj⇩J J ⊨ F_of ` 𝒩))›

lemma prop_unsat_to_AF_entails_bot: ‹propositionally_unsatisfiable ℳ ⟹ ℳ ⊨⇩A⇩F {to_AF bot}›
proof -
  assume prop_unsat_ℳ: ‹propositionally_unsatisfiable ℳ›
  then show ‹ℳ ⊨⇩A⇩F {to_AF bot}›
    unfolding AF_entails_def
  proof (intro allI impI)
    fix J
    assume ‹enabled_set {to_AF bot} J›
    have ‹bot ∈ (proj⇩⊥ ℳ) proj⇩J J›
      using prop_unsat_ℳ
      unfolding propositionally_unsatisfiable_def propositional_model_def
      by blast
    then have ‹bot ∈ ℳ proj⇩J J›
      using enabled_projection_def prop_proj_in
      by fastforce
    then have ‹ℳ proj⇩J J ⊨ {bot}›
      using bot_entails_empty entails_subsets
      by (meson empty_subsetI insert_subset)
    then show ‹ℳ proj⇩J J ⊨ F_of ` {to_AF bot}›
      by (auto simp add: F_of_to_AF)
  qed
qed

lemma ‹enabled_set {} J›
  unfolding enabled_set_def by blast

lemma ‹(∀J. ¬ (enabled_set 𝒩 J)) ⟹ (ℳ ⊨⇩A⇩F 𝒩)›
  unfolding AF_entails_def by blast
  
definition AF_entails_sound :: "('f, 'v) AF set ⇒ ('f, 'v) AF set ⇒ bool" (infix "⊨s⇩A⇩F" 50) where
  ‹AF_entails_sound ℳ 𝒩 ≡ (∀J. (enabled_set 𝒩 J ⟶
  sound_cons.entails_neg ((fml_ext ` (total_strip J)) ∪ (Pos ` (ℳ proj⇩J J))) (Pos ` F_of ` 𝒩)))›

lemma distrib_proj: ‹ℳ ∪ 𝒩 proj⇩J J = (ℳ proj⇩J J) ∪ (𝒩 proj⇩J J)›
  unfolding enabled_projection_def by auto

lemma distrib_proj_singleton: ‹ℳ ∪ {𝒞} proj⇩J J = (ℳ proj⇩J J) ∪ ({𝒞} proj⇩J J)›
  unfolding enabled_projection_def by auto

lemma enabled_union2: ‹enabled_set (ℳ ∪ 𝒩) J ⟹ enabled_set 𝒩 J›
  unfolding enabled_set_def by blast

lemma enabled_union1: ‹enabled_set (ℳ ∪ 𝒩) J ⟹ enabled_set ℳ J›
  unfolding enabled_set_def by blast

lemma finite_subset_image_strong:
  assumes "finite U" and
    "(∀C ∈ U. (∃D ∈ W. P D = C ∧ Q D))"
  shows "∃W'⊆W. finite W' ∧ U = P ` W' ∧ (∀D'∈ W'. Q D')"
  using assms
proof (induction U rule: finite_induct)
  case empty
  then show ?case by blast
next
  case (insert D' U)
  then obtain C' W'' where wpp_and_cp_assms: "W'' ⊆ W" "finite W''" "U = P ` W''" "∀a ∈ W''. Q a"
    "C' ∈ W" "P C' = D'" "Q C'"
    by auto
  define W' where "W' = insert C' W''"
  then have ‹(insert C' W') ⊆W ∧ finite (insert C' W') ∧ insert D' U = P ` (insert C' W') ∧
             (∀a∈(insert C' W'). Q a)›
    using wpp_and_cp_assms by blast
  then show ?case
    by blast
qed

lemma all_to_ex: ‹∀x. P x ⟹ ∃x. P x› for P by blast

lemma three_skolems:
  assumes ‹⋀U. P U  ⟹ ∃X Y Z. Q U X Y Z›
  shows ‹(⋀X_of Y_of Z_of. (⋀U. P U ⟹ Q U (X_of U) (Y_of U) (Z_of U)) ⟹ thesis) ⟹ thesis›
  using assms
  by metis

lemma finite_subset_with_prop:
  assumes ‹∃Js. A = f ` Js ∧ (∀J∈Js. P J)› and
    ‹finite C› and
    ‹B = C ∩ A›
  shows ‹∃Js. B = f ` Js ∧ (∀J∈Js. P J) ∧ finite Js›
proof -
  have B_fin: ‹finite B› using assms(2) assms(3) by simp
  have B_sub: ‹B ⊆ A› using assms(2) assms(3) by auto
  obtain Js where A_is: ‹A = f ` Js› and P_Js: ‹∀J∈Js. P J›
    using assms(1) by blast
  then have ‹∀b∈B. ∃J∈Js. b = f J ∧ P J›
    using B_sub by blast
  then obtain Js' where ‹B = f ` Js'› and ‹finite Js'› ‹∀J∈Js'. P J›
    using B_fin by (smt (verit, ccfv_threshold) B_sub assms(1) finite_subset_image subsetD)
  then show ‹∃Js. B = f ` Js ∧ (∀J∈Js. P J) ∧ finite Js›
    by blast
qed

lemma to_V_neg [simp]: ‹to_V (neg a) = to_V a›
  by (metis is_Neg_to_V is_Pos_to_V neg.simps(1) neg.simps(2) to_V.simps(1) to_V.simps(2))

  (* Splitting report Lemma 4, 1/2 *)
sublocale AF_cons_rel: consequence_relation "to_AF bot" AF_entails
proof
  show ‹{to_AF bot} ⊨⇩A⇩F {}›
    unfolding to_AF_def AF_entails_def enabled_def enabled_projection_def
    using bot_entails_empty by simp
next
  fix 𝒞
  show ‹{𝒞} ⊨⇩A⇩F {𝒞}›
    unfolding to_AF_def AF_entails_def enabled_def enabled_projection_def enabled_set_def
    using entails_reflexive by simp
next
  fix ℳ 𝒩 𝒫 𝒬
  assume m_in_n: ‹ℳ ⊆ 𝒩› and
    p_in_q: ‹𝒫 ⊆ 𝒬› and
    m_entails_p: ‹ℳ ⊨⇩A⇩F 𝒫›
  show ‹𝒩 ⊨⇩A⇩F 𝒬›
    unfolding to_AF_def AF_entails_def enabled_def enabled_projection_def enabled_set_def
  proof (rule allI, rule impI)
    fix J
    assume q_enabled: ‹∀𝒞∈𝒬. fset (A_of 𝒞) ⊆ total_strip J›
    have ‹{F_of 𝒞 |𝒞. 𝒞 ∈ ℳ ∧ fset (A_of 𝒞) ⊆ total_strip J} ⊆ 
      {F_of 𝒞 |𝒞. 𝒞 ∈ 𝒩 ∧ fset (A_of 𝒞) ⊆ total_strip J}›
      using m_in_n by blast
    moreover have ‹F_of ` 𝒫 ⊆ F_of ` 𝒬›
      using p_in_q by blast
    ultimately show ‹{F_of 𝒞 |𝒞. 𝒞 ∈ 𝒩 ∧ fset (A_of 𝒞) ⊆ total_strip J} ⊨ F_of ` 𝒬›
      using m_entails_p  entails_subsets
      unfolding to_AF_def AF_entails_def enabled_def enabled_projection_def enabled_set_def
      by (metis (mono_tags, lifting) q_enabled p_in_q subset_iff)
  qed
next
  fix ℳ 𝒩 𝒞 ℳ' 𝒩'
  assume
    entails_c: ‹ℳ ⊨⇩A⇩F 𝒩 ∪ {𝒞}› and
    c_entails: ‹ℳ' ∪ {𝒞} ⊨⇩A⇩F 𝒩'›
  show ‹ℳ ∪ ℳ' ⊨⇩A⇩F 𝒩 ∪ 𝒩'›
    unfolding AF_entails_def
  proof (intro allI impI)
    fix J
    assume enabled_n: ‹enabled_set (𝒩 ∪ 𝒩') J›
    {
      assume enabled_c: ‹enabled_set {𝒞} J›
      then have proj_enabled_c: ‹{𝒞} proj⇩J J = {F_of 𝒞}› 
        unfolding enabled_projection_def using enabled_set_def by blast 
      have cut_hyp1: ‹ℳ proj⇩J J ⊨ F_of ` 𝒩 ∪ {F_of 𝒞}›
        using entails_c enabled_n enabled_c unfolding AF_entails_def by (simp add: enabled_set_def)
      have ‹(ℳ' ∪ {𝒞}) proj⇩J J ⊨ F_of ` 𝒩'›
        using c_entails enabled_union2[of 𝒩 𝒩' J, OF enabled_n] unfolding AF_entails_def by simp
      then have cut_hyp2: ‹(ℳ' proj⇩J J) ∪ {F_of 𝒞} ⊨ F_of ` 𝒩'›
        using proj_enabled_c distrib_proj_singleton by metis
      have ‹ℳ ∪ ℳ' proj⇩J J ⊨ F_of ` (𝒩 ∪ 𝒩')›
        using entails_cut[OF cut_hyp1 cut_hyp2] distrib_proj by (simp add: image_Un) 
    }
    moreover
    {
      assume not_enabled_c: ‹¬ enabled_set {𝒞} J›
      then have ‹ℳ' ∪ {𝒞} proj⇩J J = ℳ' proj⇩J J›
        unfolding enabled_projection_def enabled_set_def by auto
      then have ‹ℳ' proj⇩J J ⊨ F_of ` 𝒩'›
        using c_entails enabled_n unfolding AF_entails_def by (metis enabled_union2) 
      then have ‹ℳ ∪ ℳ' proj⇩J J ⊨ F_of ` (𝒩 ∪ 𝒩')›
        using entails_subsets by (metis distrib_proj image_Un sup.cobounded2) 
    }
    ultimately show ‹ℳ ∪ ℳ' proj⇩J J ⊨ F_of ` (𝒩 ∪ 𝒩')›
      by blast 
    qed
next
  fix ℳ 𝒩
  assume m_entails_n: ‹ℳ ⊨⇩A⇩F 𝒩›
  consider (NotEnabled) ‹∀J. ¬ enabled_set 𝒩 J› | (Enabled) ‹∃J. enabled_set 𝒩 J› by blast
  then show ‹∃M' N'. M' ⊆ ℳ ∧ N' ⊆ 𝒩 ∧ finite M' ∧ finite N' ∧ M' ⊨⇩A⇩F N'›
  proof cases
    case NotEnabled
    then obtain 𝒩' where N'_sub: ‹𝒩' ⊆ 𝒩› and N'_fin: ‹finite 𝒩'› and
      sub_not_enab: ‹∀J. ¬ enabled_set 𝒩' J›
      using never_enabled_finite_subset[of 𝒩] by blast
    obtain ℳ' where ‹ℳ' ⊆ ℳ› and ‹finite ℳ'› and ‹ℳ' ⊨⇩A⇩F 𝒩'›
      using sub_not_enab unfolding AF_entails_def by blast
    then show ?thesis using N'_sub N'_fin by blast
  next
    case Enabled
    then obtain J' where J'_is: ‹enabled_set 𝒩 J'› by auto
    {
      fix J
      assume enabled_N: ‹enabled_set 𝒩 J›
      then have ‹ℳ proj⇩J J ⊨ F_of ` 𝒩›
        using m_entails_n unfolding AF_entails_def by simp 
      then obtain M' N' where mp_proj: ‹M' ⊆ ℳ proj⇩J J› and
        np_proj: ‹N' ⊆ F_of ` 𝒩› and mp_fin: ‹finite M'› and np_fin: ‹finite N'› and
        mp_entails_np: ‹M' ⊨ N'›
        using entails_compactness by metis
          
      have mp_with_f_of: ‹∀C ∈ M'. ∃𝒞 ∈ ℳ. F_of 𝒞 = C ∧ enabled 𝒞 J› 
        using mp_proj unfolding enabled_projection_def by blast
      have ‹∃ℳ'⊆ ℳ. finite ℳ' ∧ M' = F_of ` ℳ' ∧ enabled_set ℳ' J›
        using finite_subset_image_strong[OF mp_fin mp_with_f_of]
        unfolding enabled_set_def by blast
      then have m_fin_subset: ‹∃ℳ' ⊆ ℳ. finite ℳ' ∧ M' = ℳ' proj⇩J J›
        unfolding enabled_projection_def enabled_set_def by blast
          
      have np_with_f_of: ‹∀C ∈ N'. ∃𝒞 ∈ 𝒩. F_of 𝒞 = C› 
        using np_proj unfolding enabled_projection_def by blast
      have n_fin_subset: ‹∃𝒩'⊆ 𝒩. finite 𝒩' ∧ N' = F_of ` 𝒩'›
        using finite_subset_image[OF np_fin np_proj] .
          
      obtain ℳ' 𝒩' where m_n_subs: ‹ℳ' ⊆ ℳ› ‹𝒩' ⊆ 𝒩› ‹finite ℳ'› ‹finite 𝒩'› ‹M' = ℳ' proj⇩J J›
        ‹N' = F_of ` 𝒩'›
        using m_fin_subset n_fin_subset by blast 
      then have m_proj: ‹ℳ' proj⇩J J ⊨ F_of ` 𝒩'›
        using mp_entails_np by simp
          
      have enabled_N': ‹enabled_set 𝒩' J›
        using enabled_N m_n_subs(2) unfolding enabled_set_def by blast

      let ?ℳ'_sel⇩J = ‹{𝒞. 𝒞 ∈ ℳ' ∧ enabled 𝒞 J}›
      have ‹?ℳ'_sel⇩J ⊆ ℳ'› by simp
      have ‹finite (⋃{fset (A_of 𝒞) |𝒞. 𝒞 ∈ 𝒩' ∪ ?ℳ'_sel⇩J})› (*{a. ∃𝒞∈𝒩'. a ∈ (fset (A_of 𝒞)) }›*)
        using m_n_subs(3) m_n_subs(4) by auto
      then obtain A⇩𝒥⇩' where AJ_is: ‹fset A⇩𝒥⇩' = ⋃{fset (A_of 𝒞) |𝒞. 𝒞 ∈ 𝒩' ∪ ?ℳ'_sel⇩J}›
        by (smt (verit, best) fset_cases mem_Collect_eq)
      define 𝒥' where ‹𝒥' = Pair bot A⇩𝒥⇩' ›
      have ‹∀a∈fset (A_of 𝒥'). a ∈⇩t J›
      proof
        fix a
        assume ‹a ∈ fset (A_of 𝒥')›
        then have ‹∃𝒞∈𝒩' ∪ ?ℳ'_sel⇩J. a ∈ fset (A_of 𝒞)›
          unfolding 𝒥'_def using AJ_is by auto
        then show ‹a ∈⇩t J› 
          using enabled_N' unfolding enabled_set_def enabled_def belong_to_total_def belong_to_def
          by auto 
      qed
      moreover have ‹F_of 𝒥' = bot›
        unfolding 𝒥'_def
        by simp
      moreover have ‹∀𝒞∈𝒩'. fset (A_of 𝒞) ⊆ fset (A_of 𝒥')›
        using AJ_is 𝒥'_def by auto
          
      ultimately have 
        ‹∃ℳ' 𝒩' 𝒥'. ℳ' ⊆ ℳ ∧ 𝒩' ⊆ 𝒩 ∧ finite ℳ' ∧ finite 𝒩' ∧ ℳ' proj⇩J J ⊨ F_of ` 𝒩' ∧
        enabled_set 𝒩' J ∧ F_of 𝒥' = bot ∧ (∀a∈fset (A_of 𝒥'). a ∈⇩t J) ∧
        (fset (A_of 𝒥') = ⋃{fset (A_of 𝒞) |𝒞. 𝒞 ∈ 𝒩' ∪ {𝒞. 𝒞 ∈ ℳ' ∧ enabled 𝒞 J}})›
        using enabled_N' m_n_subs m_proj AJ_is 𝒥'_def
        by (metis (mono_tags, lifting) AF.sel(2))
    }
        
    (* In the pen-and-paper proof, the 𝒥'_of function is left vague, but in Isabelle the last
          conjunct that fully defines it is extremelly important. Non trivial is the addition of
          constraints from the enabled formulas in ℳ'_of J, but it is necessary to ensure that
          ‹(ℳ'_of J') proj⇩J J' ⊆ (ℳ'_of J') proj⇩J J› close to the end of the proof*)
    then obtain ℳ'_of 𝒩'_of 𝒥'_of where 
      fsets_from_J: ‹enabled_set 𝒩 J ⟹ ℳ'_of J ⊆ ℳ ∧ 𝒩'_of J ⊆ 𝒩 ∧ finite (ℳ'_of J) ∧ 
      finite (𝒩'_of J) ∧ (ℳ'_of J) proj⇩J J ⊨ F_of ` (𝒩'_of J) ∧ enabled_set (𝒩'_of J) J ∧
      F_of (𝒥'_of J) = bot ∧ (∀a∈fset (A_of (𝒥'_of J)). a ∈⇩t J) ∧
      (fset (A_of (𝒥'_of J)) = ⋃{fset (A_of 𝒞) |𝒞. 𝒞 ∈ (𝒩'_of J) ∪
        {𝒞. 𝒞 ∈ (ℳ'_of J) ∧ enabled 𝒞 J}})› for J 
      using three_skolems[of "λU. enabled_set 𝒩 U" 
        "λJ ℳ' 𝒩' 𝒥'. ℳ' ⊆ ℳ ∧ 𝒩' ⊆ 𝒩 ∧ finite ℳ' ∧ finite 𝒩' ∧ ℳ' proj⇩J J ⊨ F_of ` 𝒩' ∧ 
        enabled_set 𝒩' J ∧ F_of 𝒥' = bot ∧ (∀a∈fset (A_of 𝒥'). a ∈⇩t J) ∧
        (fset (A_of 𝒥') = ⋃{fset (A_of 𝒞) |𝒞. 𝒞 ∈ 𝒩' ∪ {𝒞. 𝒞 ∈ ℳ' ∧ enabled 𝒞 J}})"]
      by force
        
    let ?𝒥'_set = ‹{𝒥'_of J |J. enabled_set 𝒩 J}›
    have ex_Js: ‹∃Js. ?𝒥'_set = 𝒥'_of ` Js ∧ (∀J∈Js. enabled_set 𝒩 J)›
      by blast
    have proj_prop_J': ‹proj⇩⊥ ?𝒥'_set = ?𝒥'_set›
      using fsets_from_J unfolding propositional_projection_def by blast
    let ?𝒩'_un = ‹⋃{𝒩'_of J |J. enabled_set 𝒩 J}›
    let ?ℳ'_un = ‹⋃{{𝒞. 𝒞 ∈ ℳ'_of J ∧ enabled 𝒞 J} |J. enabled_set 𝒩 J}›
    have A_of_enabled: ‹enabled_set 𝒩 J ⟹ (fset (A_of (𝒥'_of J)) =
      ⋃{fset (A_of 𝒞) |𝒞. 𝒞 ∈ (𝒩'_of J) ∪ {𝒞. 𝒞 ∈ (ℳ'_of J) ∧ enabled 𝒞 J}})› for J
      using fsets_from_J by presburger
    have A_of_eq: ‹⋃ (fset ` A_of ` ?𝒥'_set) = 
      ⋃ (fset ` A_of ` ?𝒩'_un) ∪ ⋃ (fset ` A_of ` ?ℳ'_un)›
    proof -
      have ‹⋃ (fset ` A_of ` ?𝒥'_set) = ⋃{fset (A_of (𝒥'_of J)) |J. enabled_set 𝒩 J}›
        by blast
      also have ‹... = ⋃{⋃{fset (A_of 𝒞) |𝒞. 𝒞 ∈
        (𝒩'_of J) ∪ {𝒞. 𝒞 ∈ (ℳ'_of J) ∧ enabled 𝒞 J}} |J. enabled_set 𝒩 J}›
        using A_of_enabled by (metis (no_types, lifting))
      also have ‹... = ⋃(fset ` A_of ` (?𝒩'_un ∪ ?ℳ'_un))› by blast
      finally show ‹⋃(fset ` A_of ` ?𝒥'_set) =
        ⋃(fset ` A_of ` ?𝒩'_un) ∪ ⋃ (fset ` A_of ` ?ℳ'_un)›
        by simp
    qed
      
    have ‹∀J. ¬ (enabled_set 𝒩 J) ⟶ ¬ (J ⊨⇩p2 (ℰ_from 𝒩))›
      using equiv_ℰ_enabled_𝒩 by blast
    then have not_enab_case: ‹∀J. ¬ (enabled_set 𝒩 J) ⟶ ¬ (J ⊨⇩p2 ?𝒥'_set ∪ (ℰ_from 𝒩))›
      using supset_not_model_p2 Un_upper2 by blast
    have ‹∀J. enabled_set 𝒩 J ⟶ ¬ (J ⊨⇩p2 ?𝒥'_set)›
    proof (rule allI, rule impI, rule notI)
      fix J
      assume
        enab_N_loc: ‹enabled_set 𝒩 J› and
        entails_J: ‹(J ⊨⇩p2 ?𝒥'_set)›
      have A_ok: ‹fset (A_of (𝒥'_of J)) ⊆ total_strip J›
        using enab_N_loc fsets_from_J by force
      then have ‹proj⇩⊥ {𝒥'_of J} proj⇩J J = {bot}›
        using enab_N_loc fsets_from_J unfolding propositional_projection_def enabled_projection_def
        by (simp add: enabled_def)
      then have ‹¬ J ⊨⇩p2 ?𝒥'_set›
        using A_ok enab_N_loc unfolding propositional_model2_def enabled_def enabled_projection_def
          proj_prop_J' by auto
      then show False 
        using entails_J by auto
    qed
    then have enab_case: ‹∀J. (enabled_set 𝒩 J) ⟶ ¬ (J ⊨⇩p2 ?𝒥'_set ∪ (ℰ_from 𝒩))›
      using supset_not_model_p2 Un_upper2 by blast
    have ‹∀J. ¬ (J ⊨⇩p2 (?𝒥'_set ∪ (ℰ_from 𝒩)))›
      using not_enab_case enab_case by blast

    then obtain 𝒮 where S_sub: ‹𝒮 ⊆ ?𝒥'_set ∪ (ℰ_from 𝒩)› and S_fin: ‹finite 𝒮› and
      S_unsat: ‹∀J. ¬ J ⊨⇩p2 𝒮›
      using compactness_AF_proj by meson
    have E_sat: ‹sat (AF_proj_to_formula_set (ℰ_from 𝒩))›
      unfolding sat_def using J'_is equiv_ℰ_enabled_𝒩 equiv_prop_entail2_sema2 by blast
    define 𝒮⇩𝒥 where ‹𝒮⇩𝒥 = 𝒮 ∩ ?𝒥'_set›
    define 𝒮⇩ℰ where ‹𝒮⇩ℰ = 𝒮 ∩ (ℰ_from 𝒩)›
    define 𝒮⇩ℰ' where ‹𝒮⇩ℰ' = {𝒞. 𝒞 ∈ 𝒮⇩ℰ ∧ (to_V ` (fset (A_of 𝒞))) ⊆ (to_V ` ⋃ (fset ` A_of ` 𝒮⇩𝒥))}›
    define 𝒮' where ‹𝒮' = 𝒮⇩𝒥 ∪ 𝒮⇩ℰ'›
    have proj_S':  ‹proj⇩⊥  𝒮' = 𝒮'›
      using proj_prop_J' prop_proj_ℰ_from S_sub prop_proj_sub prop_proj_distrib
      unfolding 𝒮'_def 𝒮⇩𝒥_def 𝒮⇩ℰ'_def 𝒮⇩ℰ_def
      by (smt (verit) Int_iff mem_Collect_eq subsetI)
    have S_is: ‹𝒮 = (𝒮⇩ℰ - 𝒮⇩ℰ') ∪ 𝒮'›
      using S_sub 𝒮⇩𝒥_def 𝒮⇩ℰ_def 𝒮'_def 𝒮⇩ℰ'_def by blast
    have a_from_E_to_J: ‹neg a ∈ ⋃(fset ` A_of ` 𝒮⇩ℰ') ⟹ a ∈ ⋃(fset ` A_of ` 𝒮⇩𝒥)› for a
    proof -
      fix a
      assume nega_in: ‹neg a ∈ ⋃(fset ` A_of ` 𝒮⇩ℰ')›
      then have ‹to_V (neg a) ∈ to_V ` ⋃(fset ` A_of ` 𝒮⇩𝒥)›
        unfolding 𝒮⇩ℰ'_def by blast
      then have a_or_nega_in: ‹a ∈ ⋃(fset ` A_of ` 𝒮⇩𝒥) ∨ neg a ∈ ⋃(fset ` A_of ` 𝒮⇩𝒥)›
        by (smt (verit) imageE neg.simps(1) neg.simps(2) to_V.elims) 
      obtain 𝒞1 where ‹𝒞1 ∈ ℰ_from 𝒩› and ‹neg a ∈ fset (A_of 𝒞1)›
        using nega_in unfolding 𝒮⇩ℰ'_def 𝒮⇩ℰ_def ℰ_from_def by blast
      then obtain 𝒞 where ‹𝒞 ∈ 𝒩› and ‹a ∈ fset (A_of 𝒞)›
        unfolding ℰ_from_def by (smt (verit) AF.sel(2) bot_fset.rep_eq empty_iff finsert.rep_eq
          insert_iff mem_Collect_eq neg.simps(1) neg.simps(2) to_V.elims)
      then have in_N_in_J: ‹∀J. (enabled_set 𝒩 J ⟶ a ∈⇩t J)›
        using in_total_to_strip unfolding enabled_set_def enabled_def by blast 
      have ‹b ∈  ⋃(fset ` A_of ` 𝒮⇩𝒥) ⟹ (∃J. enabled_set 𝒩 J ∧ b ∈⇩t J)› for b
      proof -
        have ‹x ∈ 𝒮⇩𝒥 ⟹ b |∈| A_of x ⟹ ∃J. enabled_set 𝒩 J ∧ b ∈ total_strip J› for x
        proof -
          fix 𝒞2
          assume C2_in: ‹𝒞2 ∈ 𝒮⇩𝒥› and
            b_in: ‹b ∈ fset (A_of 𝒞2)›
          obtain J where enab_J: ‹enabled_set 𝒩 J› and ‹𝒞2 = 𝒥'_of J›
            using C2_in unfolding 𝒮⇩𝒥_def by blast
          then have ‹b ∈ total_strip J›
            using b_in fsets_from_J by auto
          then show ‹∃J. enabled_set 𝒩 J ∧ b ∈ total_strip J›
            using enab_J by blast
        qed
        then show ‹b ∈  ⋃(fset ` A_of ` 𝒮⇩𝒥) ⟹ (∃J. enabled_set 𝒩 J ∧ b ∈⇩t J)›
          by clarsimp
      qed
      then have ‹¬  neg a ∈ ⋃(fset ` A_of ` 𝒮⇩𝒥)›
        using in_N_in_J by fastforce 
      then show ‹a ∈ ⋃(fset ` A_of ` 𝒮⇩𝒥)›
        using a_or_nega_in by blast
    qed
    have empty_inter_in_S: ‹to_V ` ⋃ (fset ` A_of ` (𝒮⇩ℰ - 𝒮⇩ℰ')) ∩ to_V ` ⋃ (fset ` A_of ` 𝒮') = {}›
    proof (rule ccontr)
      assume contra: ‹to_V ` ⋃ (fset ` A_of ` (𝒮⇩ℰ - 𝒮⇩ℰ')) ∩ to_V ` ⋃ (fset ` A_of ` 𝒮') ≠ {}›
      then obtain v where v_in1: ‹v ∈ to_V ` ⋃ (fset ` A_of ` (𝒮⇩ℰ - 𝒮⇩ℰ'))›
        and v_in2: ‹v ∈ to_V ` ⋃ (fset ` A_of ` 𝒮')› by blast
      obtain 𝒞 where C_in: ‹𝒞 ∈ 𝒮⇩ℰ - 𝒮⇩ℰ'› and v_in_C: ‹v ∈ to_V ` (fset (A_of 𝒞))›
        using v_in1 by blast
      obtain a where C_is1: ‹𝒞 = Pair bot {|a|}›
        using C_in unfolding 𝒮⇩ℰ_def ℰ_from_def by blast
      then have v_is: ‹v = to_V a›
        using v_in_C by simp
      obtain 𝒞' where C'_in: ‹𝒞' ∈ 𝒮'› and v_in_C': ‹v ∈ to_V ` (fset (A_of 𝒞'))›
        using v_in2 by blast
      then obtain a' where v_is': ‹v = to_V a'› and a'_in: ‹a' ∈ fset (A_of 𝒞')›
        by blast
      consider (J) ‹𝒞' ∈ 𝒮⇩𝒥› | (E') ‹𝒞' ∈ 𝒮⇩ℰ'›
        using C'_in 𝒮'_def by blast
      then show False
      proof cases
        case J
        then have ‹to_V ` (fset (A_of 𝒞')) ⊆ (to_V ` ⋃ (fset ` A_of ` 𝒮⇩𝒥))›
          by blast
        then have ‹to_V ` (fset (A_of 𝒞)) ⊆ (to_V ` ⋃ (fset ` A_of ` 𝒮⇩𝒥))›
          using C_is1 v_in_C' v_is by auto
        then have ‹𝒞 ∈ 𝒮⇩ℰ'›
          unfolding 𝒮⇩ℰ'_def using C_in by blast
        then show False
          using C_in by blast
      next
        case E'
        then consider (a) ‹𝒞' = Pair bot {|a|}› | (nega) ‹𝒞' = Pair bot {|neg a|}›
          unfolding 𝒮⇩ℰ'_def 𝒮⇩ℰ_def ℰ_from_def using v_in_C' v_is
            AF.sel(2) IntE empty_iff fset_simps(1) fset_simps(2) image_iff insert_iff
            mem_Collect_eq neg.simps(1) neg.simps(2) to_V.elims
          by (smt (verit, del_insts))
        then show False 
        proof cases
          case a
          then show ?thesis
            using E' a_in_ℰ Enabled equiv_ℰ_enabled_𝒩 C_in C_is1 unfolding 𝒮⇩ℰ_def 𝒮⇩ℰ'_def 
            by blast
        next
          case nega
          have ‹𝒞' ∈ ℰ_from 𝒩› 
            using E' unfolding 𝒮⇩ℰ'_def 𝒮⇩ℰ_def by auto
          moreover have ‹𝒞 ∈ ℰ_from 𝒩›
            using C_in unfolding 𝒮⇩ℰ_def by auto
          ultimately show ?thesis
            using a_in_ℰ nega C_is1 Enabled equiv_ℰ_enabled_𝒩 by blast
        qed
      qed
    qed
    then have empty_inter: ‹⋃ (atoms ` (AF_proj_to_formula_set (𝒮⇩ℰ - 𝒮⇩ℰ'))) ∩
      ⋃ (atoms ` (AF_proj_to_formula_set 𝒮')) = {}›
      using atoms_simp proj_S' prop_proj_distrib prop_proj_sub
      by (smt (verit, ccfv_threshold) S_sub Un_subset_iff ‹𝒮 = 𝒮⇩ℰ - 𝒮⇩ℰ' ∪ 𝒮'› proj_prop_J'
        prop_proj_ℰ_from)
    have sat_rest: ‹sat (AF_proj_to_formula_set (𝒮⇩ℰ - 𝒮⇩ℰ'))›
      using E_sat unfolding 𝒮⇩ℰ'_def 𝒮⇩ℰ_def AF_proj_to_formula_set_def
        propositional_projection_def sat_def by blast
    have S'_unsat: ‹∀J. ¬ J ⊨⇩p2 𝒮'›
      using unsat_AF_simp[OF _ sat_rest empty_inter] S_unsat equiv_prop_entail2_sema2 S_is
        val_from_interp unfolding sat_def by metis
    have ex_fin_Js: ‹∃Js. 𝒮⇩𝒥 = 𝒥'_of ` Js ∧ (∀J∈Js. enabled_set 𝒩 J) ∧ finite Js›
      using finite_subset_with_prop[OF ex_Js S_fin 𝒮⇩𝒥_def] .
    then obtain Js where Js_fin: ‹finite Js› and Js_enab: ‹∀J∈Js. enabled_set 𝒩 J› and
      Js_is: ‹𝒥'_of ` Js = 𝒮⇩𝒥›
      by blast

    have fin_inter: ‹finite (⋃(fset ` A_of ` 𝒮⇩𝒥) ∩ ⋃(fset ` A_of ` 𝒩))›
    proof
      have ‹finite (⋃(fset ` A_of ` 𝒮⇩𝒥))›
        unfolding 𝒮⇩𝒥_def using S_fin image_Int_subset by simp
      then show ‹(finite (⋃(fset ` A_of ` 𝒮⇩𝒥))) ∨ (finite (⋃ (fset ` A_of ` 𝒩)))›
        by auto
    qed
    have ‹∀a∈(⋃(fset ` A_of ` 𝒩)). ∃𝒞∈𝒩. a ∈ fset (A_of 𝒞)›
      by blast
    then obtain f where f_def: ‹∀a∈(⋃(fset ` A_of ` 𝒩)). f a ∈ 𝒩 ∧ a ∈ fset (A_of (f a))›
      by metis
        (* the fact that 𝒩⇩𝒥 is needed in the proof was found during the isabelle verification *)
    define 𝒩⇩𝒥 where ‹𝒩⇩𝒥 = (f ` (⋃(fset ` A_of ` 𝒮⇩𝒥) ∩ ⋃(fset ` A_of ` 𝒩)))›
    have nj_fin: ‹finite 𝒩⇩𝒥›
      unfolding 𝒩⇩𝒥_def using fin_inter by blast
    have nj_sub: ‹𝒩⇩𝒥 ⊆ 𝒩›
      unfolding 𝒩⇩𝒥_def using f_def by blast
    have nj_as: ‹(∀a∈(⋃(fset ` A_of ` 𝒮⇩𝒥))∩(⋃(fset ` A_of ` 𝒩)).
      a ∈ ⋃(fset ` A_of ` 𝒩⇩𝒥))›
      unfolding 𝒩⇩𝒥_def using f_def by fast
        
    define ℳ' where ‹ℳ' = ⋃{ℳ'_of J |J. J ∈ Js}›
    define 𝒩' where  ‹𝒩' = ⋃{𝒩'_of J |J. J ∈ Js} ∪ 𝒩⇩𝒥›
    then have ‹ℳ' ⊆ ℳ›
      unfolding ℳ'_def using fsets_from_J Js_enab by fast
    moreover have ‹𝒩' ⊆ 𝒩›
      unfolding 𝒩'_def using fsets_from_J Js_enab nj_sub by fast
    moreover have ‹finite ℳ'›
      unfolding ℳ'_def using fsets_from_J Js_fin Js_enab by auto
    moreover have ‹finite 𝒩'›
      unfolding 𝒩'_def using fsets_from_J Js_fin Js_enab nj_fin by auto
    moreover have ‹ℳ' ⊨⇩A⇩F 𝒩'› unfolding AF_entails_def
    proof (rule allI, rule impI)
      fix J
      assume enab_N': ‹enabled_set 𝒩' J›
      then have ‹J ⊨⇩p2 ℰ_from 𝒩'›
        using equiv_ℰ_enabled_𝒩 by auto
      moreover have ‹𝒮⇩ℰ' ⊆ ℰ_from 𝒩'›
        proof
          fix 𝒞 
          assume C_in: ‹𝒞 ∈ 𝒮⇩ℰ'›
          then obtain a where C_is: ‹𝒞 = Pair bot {|neg a|}›
            unfolding 𝒮⇩ℰ'_def 𝒮⇩ℰ_def ℰ_from_def by blast
          then have ‹neg a ∈ ⋃(fset ` A_of ` 𝒮⇩ℰ')›
            using C_in using image_iff by fastforce
          then have a_in_SJ: ‹a ∈ ⋃(fset ` A_of ` 𝒮⇩𝒥)›
            using a_from_E_to_J by presburger
          have ‹∃𝒞'∈𝒩. a ∈ fset (A_of 𝒞')›
            using C_is C_in unfolding 𝒮⇩ℰ'_def 𝒮⇩ℰ_def by (smt (verit, ccfv_threshold)
              AF.sel(2) IntE J'_is ℰ_from_def a_in_ℰ bot_fset.rep_eq empty_iff equiv_ℰ_enabled_𝒩
              finsert.rep_eq insert_iff mem_Collect_eq to_V.elims to_V_neg)
          then have ‹a ∈ ⋃(fset ` A_of ` 𝒩)›
            by blast 
          then have ‹a ∈ ⋃(fset ` A_of ` 𝒩')›
            using nj_as a_in_SJ unfolding 𝒩'_def by simp 
          then show ‹𝒞 ∈ ℰ_from 𝒩'›
            using C_is unfolding ℰ_from_def by blast
        qed
      ultimately have ‹J ⊨⇩p2 𝒮⇩ℰ'›
        unfolding 𝒮⇩ℰ'_def 𝒮⇩ℰ_def using subset_model_p2 by (metis (no_types, lifting))
      then have ‹¬ J ⊨⇩p2 𝒮⇩𝒥›
        using subset_not_model S'_unsat unfolding 𝒮'_def by blast
      then have  ‹∃J'∈Js. fset (A_of (𝒥'_of J')) ⊆ total_strip J›
        unfolding propositional_model2_def 𝒮⇩𝒥_def propositional_projection_def
          enabled_projection_def using Js_is
        by (smt (verit) Collect_cong Set.empty_def 𝒮⇩𝒥_def enabled_def image_iff mem_Collect_eq)
      then obtain J' where J'_in: ‹J' ∈ Js› and A_of_J'_in: ‹fset (A_of (𝒥'_of J')) ⊆ total_strip J›
        by blast
      then have enab_nj': ‹enabled_set 𝒩 J'›
        using Js_enab by blast
      then have ‹(ℳ'_of J') proj⇩J J' ⊨ F_of ` (𝒩'_of J')›
        using fsets_from_J by auto
      moreover have ‹(ℳ'_of J') proj⇩J J' ⊆ (ℳ'_of J') proj⇩J J›
      proof -
        have ‹𝒞 ∈ ℳ'_of J' ⟹ enabled 𝒞 J' ⟹ enabled 𝒞 J› for 𝒞
        proof -
          assume C_in: ‹𝒞 ∈ ℳ'_of J'› and
            ‹enabled 𝒞 J'›
          then have ‹fset (A_of 𝒞) ⊆ fset (A_of (𝒥'_of J'))›
            using fsets_from_J[OF enab_nj'] by blast
          then show ‹enabled 𝒞 J›
            using A_of_J'_in unfolding enabled_def by auto
        qed
        then have ‹(𝒞 ∈ ℳ'_of J' ∧ enabled 𝒞 J') ⟹ (𝒞 ∈ ℳ'_of J' ∧ enabled 𝒞 J)› for 𝒞
          by (smt (verit, ccfv_threshold))
        then have ‹{𝒞. 𝒞 ∈ ℳ'_of J' ∧ enabled 𝒞 J'} ⊆ {𝒞. 𝒞 ∈ ℳ'_of J' ∧ enabled 𝒞 J}›
          by blast
        then show ‹(ℳ'_of J') proj⇩J J' ⊆ (ℳ'_of J') proj⇩J J›
          unfolding enabled_projection_def by blast
      qed
      ultimately have entails_one: ‹(ℳ'_of J') proj⇩J J ⊨ F_of ` (𝒩'_of J')›
        using entails_subsets by blast
      have subs_M: ‹ℳ'_of J' proj⇩J J ⊆ ℳ' proj⇩J J›
        using J'_in using enabled_projection_def unfolding ℳ'_def by auto
      have subs_N: ‹F_of ` (𝒩'_of J') ⊆ F_of ` 𝒩'›
        using J'_in unfolding 𝒩'_def by blast
      show ‹ℳ' proj⇩J J ⊨ F_of ` 𝒩'›
        using entails_subsets[OF subs_M subs_N entails_one] .
    qed

    ultimately show ‹∃ℳ' 𝒩'. ℳ' ⊆ ℳ ∧ 𝒩' ⊆ 𝒩 ∧ finite ℳ' ∧ finite 𝒩' ∧ ℳ' ⊨⇩A⇩F 𝒩'›
      by blast
  qed
qed

sublocale neg_ext_sound_cons_rel: consequence_relation "Pos bot" sound_cons.entails_neg
  using sound_cons.ext_cons_rel by simp

(* Splitting report Lemma 4, 2/2 *)
lemma AF_ext_sound_cons_rel: ‹consequence_relation (to_AF bot) AF_entails_sound›
proof (standard)
  show ‹{to_AF bot} ⊨s⇩A⇩F {}›
   unfolding AF_entails_sound_def enabled_def enabled_projection_def
  proof (rule allI, rule impI)
   fix J
   assume ‹enabled_set {} J›
   have bot_in: ‹{Pos bot} ⊆ Pos ` {C. C = F_of (to_AF bot) ∧ fset (A_of (to_AF bot)) ⊆ total_strip J}›
     unfolding to_AF_def by simp
   have ‹sound_cons.entails_neg (fml_ext ` total_strip J ∪
     Pos ` {C. C = F_of (to_AF bot) ∧ fset (A_of (to_AF bot)) ⊆ total_strip J}) {}›
     using sound_cons.bot_entails_empty sound_cons.entails_subsets bot_in
     by (smt (verit, ccfv_threshold) AF.sel(2) Un_iff bot_fset.rep_eq
       consequence_relation.bot_entails_empty consequence_relation.entails_subsets empty_subsetI
       image_iff mem_Collect_eq sound_cons.ext_cons_rel subset_eq to_AF_def)
   then show ‹fml_ext ` total_strip J ∪ 
     Pos ` {F_of 𝒞 |𝒞. 𝒞 ∈ {to_AF bot} ∧ fset (A_of 𝒞) ⊆ total_strip J} ⊨s⇩∼ Pos ` F_of ` {}›
     by clarsimp
 qed
next
  fix 𝒞 :: "('f, 'v) AF"
  have ‹Pos ` {F_of Ca |Ca. Ca ∈ {𝒞} ∧ fset (A_of Ca) ⊆ total_strip J} ⊆ (Pos ` F_of ` {𝒞})›
    by auto
  show ‹{𝒞} ⊨s⇩A⇩F {𝒞}›
    unfolding AF_entails_sound_def enabled_def enabled_projection_def enabled_set_def
  proof (rule allI, rule impI)
    fix J
    assume a_of_C_in: ‹∀𝒞∈{𝒞}. fset (A_of 𝒞) ⊆ total_strip J›
    have ‹sound_cons.entails_neg (Pos (F_of 𝒞) ▹ fml_ext ` total_strip J) {Pos (F_of 𝒞)}›
      using sound_cons.entails_reflexive[of "F_of 𝒞"]
      by (smt (verit, best) Set.insert_mono bot.extremum consequence_relation.entails_reflexive
        consequence_relation.entails_subsets sound_cons.ext_cons_rel)
    then show ‹fml_ext ` total_strip J ∪ 
      Pos ` {F_of 𝒞' |𝒞'. 𝒞' ∈ {𝒞} ∧ fset (A_of 𝒞') ⊆ total_strip J} ⊨s⇩∼ Pos ` F_of ` {𝒞}›
      using a_of_C_in by clarsimp
  qed
next
  fix ℳ 𝒩 𝒫 𝒬
  assume m_in_n: ‹ℳ ⊆ 𝒩› and
    p_in_q: ‹𝒫 ⊆ 𝒬› and
    m_entails_p: ‹ℳ ⊨s⇩A⇩F 𝒫›
  show ‹𝒩 ⊨s⇩A⇩F 𝒬›
    unfolding AF_entails_sound_def enabled_def enabled_projection_def enabled_set_def
  proof (rule allI, rule impI)
    fix J
    assume q_enabled: ‹∀𝒞∈𝒬. fset (A_of 𝒞) ⊆ total_strip J›
    have ‹{F_of 𝒞 |𝒞. 𝒞 ∈ ℳ ∧ fset (A_of 𝒞) ⊆ total_strip J} ⊆
      {F_of 𝒞 |𝒞. 𝒞 ∈ 𝒩 ∧ fset (A_of 𝒞) ⊆ total_strip J}›
      using m_in_n by blast
    moreover have ‹F_of ` 𝒫 ⊆ F_of ` 𝒬›
      using p_in_q by blast
    ultimately show ‹sound_cons.entails_neg (fml_ext ` total_strip J ∪
      Pos ` {F_of 𝒞 |𝒞. 𝒞 ∈ 𝒩 ∧ fset (A_of 𝒞) ⊆ total_strip J}) (Pos ` F_of ` 𝒬)›
      using m_entails_p sound_cons.entails_subsets m_in_n p_in_q q_enabled
      unfolding AF_entails_sound_def enabled_def enabled_projection_def enabled_set_def
      by (smt (z3) Un_iff consequence_relation.entails_subsets image_iff mem_Collect_eq
        sound_cons.ext_cons_rel subset_eq)
  qed
next
  fix ℳ 𝒩 𝒞 ℳ' 𝒩'
  assume
    entails_c: ‹ℳ ⊨s⇩A⇩F 𝒩 ∪ {𝒞}› and
    c_entails: ‹ℳ' ∪ {𝒞} ⊨s⇩A⇩F 𝒩'›
  show ‹ℳ ∪ ℳ' ⊨s⇩A⇩F 𝒩 ∪ 𝒩'›
    unfolding AF_entails_sound_def
  proof (intro allI impI)
    fix J
    assume enabled_n: ‹enabled_set (𝒩 ∪ 𝒩') J›
    {
      assume enabled_c: ‹enabled_set {𝒞} J›
      then have proj_enabled_c: ‹{𝒞} proj⇩J J = {F_of 𝒞}›
        unfolding enabled_projection_def using enabled_set_def by blast
      have ‹sound_cons.entails_neg (fml_ext ` total_strip J ∪ Pos ` (ℳ proj⇩J J))
        (Pos ` F_of ` (𝒩 ∪ {𝒞}))›
        using entails_c enabled_n enabled_c unfolding AF_entails_sound_def
        by (metis Un_iff enabled_set_def)
      then have cut_hyp1: ‹sound_cons.entails_neg (fml_ext ` total_strip J ∪ Pos ` (ℳ proj⇩J J))
        (Pos ` F_of ` 𝒩 ∪ {Pos (F_of 𝒞)})›
        by force
      have ‹sound_cons.entails_neg (fml_ext ` total_strip J ∪ Pos ` (ℳ' ∪ {𝒞} proj⇩J J))
        (Pos ` F_of ` 𝒩')›
        using c_entails enabled_n enabled_union2 unfolding AF_entails_sound_def by blast
      then have cut_hyp2: ‹sound_cons.entails_neg
        (fml_ext ` total_strip J ∪ Pos ` (ℳ' proj⇩J J) ∪ {Pos (F_of 𝒞)}) (Pos ` F_of ` 𝒩')›
       by (metis Un_empty_right Un_insert_right distrib_proj image_insert proj_enabled_c)
       have ‹sound_cons.entails_neg (fml_ext ` total_strip J ∪ Pos ` (ℳ ∪ ℳ' proj⇩J J))
         (Pos ` F_of ` (𝒩 ∪ 𝒩'))›
         using neg_ext_sound_cons_rel.entails_cut[OF cut_hyp1 cut_hyp2]  distrib_proj[of ℳ ℳ' J]
           image_Un by (smt (verit, del_insts) Un_commute Un_left_absorb Un_left_commute)
    }
    moreover
    {
      assume not_enabled_c: ‹¬ enabled_set {𝒞} J›
      then have ‹ℳ' ∪ {𝒞} proj⇩J J = ℳ' proj⇩J J›
        unfolding enabled_projection_def enabled_set_def by auto
      then have ‹sound_cons.entails_neg (fml_ext ` total_strip J ∪ Pos ` (ℳ' proj⇩J J))
        (Pos ` F_of ` 𝒩')›
        using c_entails enabled_n enabled_union2 unfolding AF_entails_sound_def by metis
      then have ‹sound_cons.entails_neg (fml_ext ` total_strip J ∪ Pos ` (ℳ ∪ ℳ' proj⇩J J))
        (Pos ` F_of ` (𝒩 ∪ 𝒩'))›
        using neg_ext_sound_cons_rel.entails_subsets
        by (smt (verit, del_insts) Un_iff distrib_proj image_Un subsetI)
    }
    ultimately
    show ‹sound_cons.entails_neg (fml_ext ` total_strip J ∪ Pos ` (ℳ ∪ ℳ' proj⇩J J))
      (Pos ` F_of ` (𝒩 ∪ 𝒩'))›
      by blast
  qed
next
  fix ℳ 𝒩
  assume m_entails_n: ‹ℳ ⊨s⇩A⇩F 𝒩›
  consider (NotEnabled) ‹∀J. ¬ enabled_set 𝒩 J› | (Enabled) ‹∃J. enabled_set 𝒩 J› by blast
  then show ‹∃M' N'. M' ⊆ ℳ ∧ N' ⊆ 𝒩 ∧ finite M' ∧ finite N' ∧ M' ⊨s⇩A⇩F N'›
  proof cases
    case NotEnabled
    then obtain 𝒩' where N'_sub: ‹𝒩' ⊆ 𝒩› and N'_fin: ‹finite 𝒩'› and
      sub_not_enab: ‹∀J. ¬ enabled_set 𝒩' J›
      using never_enabled_finite_subset[of 𝒩] by blast
    obtain ℳ' where ‹ℳ' ⊆ ℳ› and ‹finite ℳ'› and ‹ℳ' ⊨s⇩A⇩F 𝒩'›
      using sub_not_enab unfolding AF_entails_sound_def by blast
    then show ?thesis using N'_sub N'_fin by blast
  next
    case Enabled
    then obtain J' where J'_is: ‹enabled_set 𝒩 J'› by auto
    {
      fix J
      assume enabled_N: ‹enabled_set 𝒩 J›
      then have ‹sound_cons.entails_neg (fml_ext ` total_strip J ∪ Pos ` (ℳ proj⇩J J)) (Pos ` F_of ` 𝒩)›
        using m_entails_n unfolding AF_entails_sound_def by blast
      then obtain MJ' N' where mj_in: ‹MJ' ⊆ fml_ext ` total_strip J ∪ Pos ` (ℳ proj⇩J J)› and
        np_proj: ‹N' ⊆ Pos ` F_of ` 𝒩› and mjp_fin: ‹finite MJ'› and np_fin: ‹finite N'› and
        mjp_entails_np: ‹sound_cons.entails_neg  MJ' N'›
        using neg_ext_sound_cons_rel.entails_compactness by metis

      define M' where "M' = MJ' ∩ Pos ` (ℳ proj⇩J J)"
      then have mp_fin: ‹finite M'›
        using mjp_fin by auto
      have mp_with_f_of: ‹∀C ∈ M'. ∃𝒞 ∈ ℳ. Pos (F_of 𝒞) = C ∧ enabled 𝒞 J›
        using mj_in unfolding enabled_projection_def M'_def by blast
      have ‹∃ℳ'⊆ ℳ. finite ℳ' ∧ M' = Pos ` F_of ` ℳ' ∧ enabled_set ℳ' J›
        using finite_subset_image_strong[of M' ℳ "(λx. Pos (F_of x))" "λx. enabled x J", OF mp_fin mp_with_f_of]
        unfolding enabled_set_def by blast
      then have ex_mp: ‹∃ℳ'⊆ℳ. finite ℳ' ∧ Pos ` (ℳ' proj⇩J J) = M'›
        unfolding enabled_projection_def enabled_set_def by blast
      then obtain ℳ' where mp_props: ‹ℳ' ⊆ ℳ› ‹finite ℳ'› ‹Pos ` (ℳ' proj⇩J J) = M'› by auto

      let ?ℳ'_sel⇩J = ‹{𝒞. 𝒞 ∈ ℳ' ∧ enabled 𝒞 J}›
      have ‹?ℳ'_sel⇩J ⊆ ℳ'› by simp
      have ‹finite (⋃{fset (A_of 𝒞) |𝒞. 𝒞 ∈ ?ℳ'_sel⇩J})› (*{a. ∃𝒞∈𝒩'. a ∈ (fset (A_of 𝒞)) }›*)
        using mp_props by auto
      then obtain 𝒜⇩ℳ⇩' where AM_is: ‹fset 𝒜⇩ℳ⇩' = (⋃{fset (A_of 𝒞) |𝒞. 𝒞 ∈ ?ℳ'_sel⇩J})›
        using fin_set_fset by fastforce
      then have AM_in_J: ‹fset 𝒜⇩ℳ⇩' ⊆ total_strip J›
        unfolding enabled_def by blast
      define J' where "J' = (MJ' ∩ fml_ext ` total_strip J)"
      then have jp_fin: ‹finite J'›
        using mjp_fin by blast
      then obtain 𝒥' where jp_props: "𝒥' ⊆ total_strip J" "fml_ext ` 𝒥' = J'" "finite 𝒥'"
        using J'_def by (metis Int_lower2 finite_subset_image)
      then obtain 𝒜⇩𝒥⇩' where AJ_is: ‹fset 𝒜⇩𝒥⇩' = 𝒥'›
        using fin_set_fset by blast
      then have AJ_in_J: ‹fset 𝒜⇩𝒥⇩' ⊆ total_strip J›
        using jp_props by auto
      define 𝒥⇩f' where ‹𝒥⇩f' = Pair bot (𝒜⇩𝒥⇩' |∪| 𝒜⇩ℳ⇩')›
      then have Jf_in: ‹fset (A_of 𝒥⇩f') ⊆ total_strip J› using AM_in_J AJ_in_J by simp
      have Jf_bot: ‹F_of 𝒥⇩f' = bot› using 𝒥⇩f'_def by auto
      have AM_in_Jf: ‹∀𝒞∈ℳ'. enabled 𝒞 J ⟶ fset (A_of 𝒞) ⊆ fset (A_of 𝒥⇩f')›
        using 𝒥⇩f'_def AM_is by auto

      have np_with_f_of: ‹∀C ∈ N'. ∃𝒞 ∈ 𝒩. Pos (F_of 𝒞) = C›
        using np_proj unfolding enabled_projection_def by blast
      have n_fin_subset: ‹∃𝒩'⊆ 𝒩. finite 𝒩' ∧ N' = Pos ` F_of ` 𝒩'›
        using finite_subset_image[OF np_fin, of "λx. Pos (F_of x)" 𝒩] np_proj by auto
      then obtain 𝒩' where np_props: ‹𝒩' ⊆ 𝒩› ‹finite 𝒩'› ‹N' = Pos ` F_of ` 𝒩'›
        by blast
      have enab_np: ‹enabled_set 𝒩' J›
        using enabled_N np_props unfolding enabled_set_def by blast

      have mjp_is: ‹MJ' = Pos ` (ℳ' proj⇩J J) ∪ fml_ext ` 𝒥'›
        using mj_in M'_def J'_def mp_props jp_props by auto
      have ‹sound_cons.entails_neg ((Pos ` (ℳ' proj⇩J J))∪ fml_ext ` 𝒥') (Pos ` F_of ` 𝒩')›
        using np_props mjp_entails_np unfolding mjp_is by blast
      then have fin_entail: ‹sound_cons.entails_neg ((Pos ` (ℳ' proj⇩J J))∪ fml_ext ` (fset (A_of 𝒥⇩f'))) (Pos ` F_of ` 𝒩')›
        using neg_ext_sound_cons_rel.entails_subsets[of
          "(Pos ` (ℳ' proj⇩J J))∪ fml_ext ` 𝒥'" "(Pos ` (ℳ' proj⇩J J))∪ fml_ext ` (fset (A_of 𝒥⇩f'))"
          "Pos ` F_of ` 𝒩'" "Pos ` F_of ` 𝒩'"] AJ_is unfolding 𝒥⇩f'_def by (simp add: image_Un subsetI)

      have ‹∃ℳ' 𝒩' 𝒥'. ℳ' ⊆ ℳ ∧ fset (A_of 𝒥') ⊆ total_strip J ∧ 𝒩' ⊆ 𝒩 ∧
        finite ℳ'  ∧ finite 𝒩' ∧ F_of 𝒥' = bot ∧ enabled_set 𝒩' J ∧
        (∀𝒞∈ℳ'. enabled 𝒞 J ⟶ fset (A_of 𝒞) ⊆ fset (A_of 𝒥')) ∧
        sound_cons.entails_neg ((Pos ` (ℳ' proj⇩J J))∪ fml_ext ` (fset (A_of 𝒥'))) (Pos ` F_of ` 𝒩')›
        using mp_props np_props fin_entail enab_np Jf_in Jf_bot 𝒥⇩f'_def AJ_is AM_is AM_in_Jf AF.sel(2) by blast
    }

    then obtain ℳ'_of 𝒩'_of 𝒥'_of where
      fsets_from_J: ‹enabled_set 𝒩 J ⟹ ℳ'_of J ⊆ ℳ ∧ fset (A_of (𝒥'_of J)) ⊆ total_strip J ∧ 𝒩'_of J ⊆ 𝒩 ∧
      finite (ℳ'_of J) ∧ finite (𝒩'_of J) ∧ F_of (𝒥'_of J) = bot ∧ enabled_set (𝒩'_of J) J ∧
      (∀𝒞∈(ℳ'_of J). enabled 𝒞 J ⟶ fset (A_of 𝒞) ⊆ fset (A_of (𝒥'_of J))) ∧
      sound_cons.entails_neg (Pos ` (ℳ'_of J proj⇩J J) ∪ fml_ext ` (fset (A_of (𝒥'_of J)))) (Pos ` F_of ` 𝒩'_of J) › for J
      by metis

    let ?𝒥'_set = ‹{𝒥'_of J |J. enabled_set 𝒩 J}›
    have ex_Js: ‹∃Js. ?𝒥'_set = 𝒥'_of ` Js ∧ (∀J∈Js. enabled_set 𝒩 J)›
      by blast
    have proj_prop_J': ‹proj⇩⊥ ?𝒥'_set = ?𝒥'_set›
      using fsets_from_J unfolding propositional_projection_def by blast
    let ?𝒩'_un = ‹⋃{𝒩'_of J |J. enabled_set 𝒩 J}›
    let ?ℳ'_un = ‹⋃{{𝒞. 𝒞 ∈ ℳ'_of J ∧ enabled 𝒞 J} |J. enabled_set 𝒩 J}›

    have ‹∀J. ¬ (enabled_set 𝒩 J) ⟶ ¬ (J ⊨⇩p2 (ℰ_from 𝒩))›
      using equiv_ℰ_enabled_𝒩 by blast
    then have not_enab_case: ‹∀J. ¬ (enabled_set 𝒩 J) ⟶ ¬ (J ⊨⇩p2 ?𝒥'_set ∪ (ℰ_from 𝒩))›
      using supset_not_model_p2 Un_upper2 by blast
    have ‹∀J. enabled_set 𝒩 J ⟶ ¬ (J ⊨⇩p2 ?𝒥'_set)›
    proof (rule allI, rule impI, rule notI)
      fix J
      assume
        enab_N_loc: ‹enabled_set 𝒩 J› and
        entails_J: ‹(J ⊨⇩p2 ?𝒥'_set)›
      have A_ok: ‹fset (A_of (𝒥'_of J)) ⊆ total_strip J›
        using enab_N_loc fsets_from_J by force
      then have ‹proj⇩⊥ {𝒥'_of J} proj⇩J J = {bot}›
        using enab_N_loc fsets_from_J unfolding propositional_projection_def enabled_projection_def
        by (simp add: enabled_def)
      then have ‹¬ J ⊨⇩p2 ?𝒥'_set›
        using A_ok enab_N_loc unfolding propositional_model2_def enabled_def enabled_projection_def
          proj_prop_J' by auto
      then show False
        using entails_J by auto
    qed
    then have enab_case: ‹∀J. (enabled_set 𝒩 J) ⟶ ¬ (J ⊨⇩p2 ?𝒥'_set ∪ (ℰ_from 𝒩))›
      using supset_not_model_p2 Un_upper2 by blast
    have ‹∀J. ¬ (J ⊨⇩p2 (?𝒥'_set ∪ (ℰ_from 𝒩)))›
      using not_enab_case enab_case by blast

    then obtain 𝒮 where S_sub: ‹𝒮 ⊆ ?𝒥'_set ∪ (ℰ_from 𝒩)› and S_fin: ‹finite 𝒮› and
      S_unsat: ‹∀J. ¬ J ⊨⇩p2 𝒮›
      using compactness_AF_proj by meson
    have E_sat: ‹sat (AF_proj_to_formula_set (ℰ_from 𝒩))›
      unfolding sat_def using J'_is equiv_ℰ_enabled_𝒩 equiv_prop_entail2_sema2 by blast
    define 𝒮⇩𝒥 where ‹𝒮⇩𝒥 = 𝒮 ∩ ?𝒥'_set›
    define 𝒮⇩ℰ where ‹𝒮⇩ℰ = 𝒮 ∩ (ℰ_from 𝒩)›
    define 𝒮⇩ℰ' where ‹𝒮⇩ℰ' = {𝒞. 𝒞 ∈ 𝒮⇩ℰ ∧ (to_V ` (fset (A_of 𝒞))) ⊆ (to_V ` ⋃ (fset ` A_of ` 𝒮⇩𝒥))}›
    define 𝒮' where ‹𝒮' = 𝒮⇩𝒥 ∪ 𝒮⇩ℰ'›
    have proj_S':  ‹proj⇩⊥  𝒮' = 𝒮'›
      using proj_prop_J' prop_proj_ℰ_from S_sub prop_proj_sub prop_proj_distrib
      unfolding 𝒮'_def 𝒮⇩𝒥_def 𝒮⇩ℰ'_def 𝒮⇩ℰ_def
      by (smt (verit) Int_iff mem_Collect_eq subsetI)
    have S_is: ‹𝒮 = (𝒮⇩ℰ - 𝒮⇩ℰ') ∪ 𝒮'›
      using S_sub 𝒮⇩𝒥_def 𝒮⇩ℰ_def 𝒮'_def 𝒮⇩ℰ'_def by blast
    have a_from_E_to_J: ‹neg a ∈ ⋃(fset ` A_of ` 𝒮⇩ℰ') ⟹ a ∈ ⋃(fset ` A_of ` 𝒮⇩𝒥)› for a
    proof -
      fix a
      assume nega_in: ‹neg a ∈ ⋃(fset ` A_of ` 𝒮⇩ℰ')›
      then have ‹to_V (neg a) ∈ to_V ` ⋃(fset ` A_of ` 𝒮⇩𝒥)›
        unfolding 𝒮⇩ℰ'_def by blast
      then have a_or_nega_in: ‹a ∈ ⋃(fset ` A_of ` 𝒮⇩𝒥) ∨ neg a ∈ ⋃(fset ` A_of ` 𝒮⇩𝒥)›
        by (smt (verit) imageE neg.simps(1) neg.simps(2) to_V.elims)
      obtain 𝒞1 where ‹𝒞1 ∈ ℰ_from 𝒩› and ‹neg a ∈ fset (A_of 𝒞1)›
        using nega_in unfolding 𝒮⇩ℰ'_def 𝒮⇩ℰ_def ℰ_from_def by blast
      then obtain 𝒞 where ‹𝒞 ∈ 𝒩› and ‹a ∈ fset (A_of 𝒞)›
        unfolding ℰ_from_def by (smt (verit) AF.sel(2) bot_fset.rep_eq empty_iff finsert.rep_eq
          insert_iff mem_Collect_eq neg.simps(1) neg.simps(2) to_V.elims)
      then have in_N_in_J: ‹∀J. (enabled_set 𝒩 J ⟶ a ∈⇩t J)›
        using in_total_to_strip unfolding enabled_set_def enabled_def by blast
      have ‹b ∈  ⋃(fset ` A_of ` 𝒮⇩𝒥) ⟹ (∃J. enabled_set 𝒩 J ∧ b ∈⇩t J)› for b
      proof -
        have ‹x ∈ 𝒮⇩𝒥 ⟹ b |∈| A_of x ⟹ ∃J. enabled_set 𝒩 J ∧ b ∈ total_strip J› for x
        proof -
          fix 𝒞2
          assume C2_in: ‹𝒞2 ∈ 𝒮⇩𝒥› and
            b_in: ‹b ∈ fset (A_of 𝒞2)›
          obtain J where enab_J: ‹enabled_set 𝒩 J› and ‹𝒞2 = 𝒥'_of J›
            using C2_in unfolding 𝒮⇩𝒥_def by blast
          then have ‹b ∈ total_strip J›
            using b_in fsets_from_J by (meson basic_trans_rules(31))
          then show ‹∃J. enabled_set 𝒩 J ∧ b ∈ total_strip J›
            using enab_J by blast
        qed
        then show ‹b ∈ ⋃ (fset ` A_of ` 𝒮⇩𝒥) ⟹ ∃J. enabled_set 𝒩 J ∧ b ∈⇩t J›
          by clarsimp
      qed
      then have ‹¬  neg a ∈ ⋃(fset ` A_of ` 𝒮⇩𝒥)›
        using in_N_in_J by fastforce
      then show ‹a ∈ ⋃(fset ` A_of ` 𝒮⇩𝒥)›
        using a_or_nega_in by blast
    qed
    have empty_inter_in_S: ‹to_V ` ⋃ (fset ` A_of ` (𝒮⇩ℰ - 𝒮⇩ℰ')) ∩ to_V ` ⋃ (fset ` A_of ` 𝒮') = {}›
    proof (rule ccontr)
      assume contra: ‹to_V ` ⋃ (fset ` A_of ` (𝒮⇩ℰ - 𝒮⇩ℰ')) ∩ to_V ` ⋃ (fset ` A_of ` 𝒮') ≠ {}›
      then obtain v where v_in1: ‹v ∈ to_V ` ⋃ (fset ` A_of ` (𝒮⇩ℰ - 𝒮⇩ℰ'))›
        and v_in2: ‹v ∈ to_V ` ⋃ (fset ` A_of ` 𝒮')› by blast
      obtain 𝒞 where C_in: ‹𝒞 ∈ 𝒮⇩ℰ - 𝒮⇩ℰ'› and v_in_C: ‹v ∈ to_V ` (fset (A_of 𝒞))›
        using v_in1 by blast
      obtain a where C_is1: ‹𝒞 = Pair bot {|a|}›
        using C_in unfolding 𝒮⇩ℰ_def ℰ_from_def by blast
      then have v_is: ‹v = to_V a›
        using v_in_C by simp
      obtain 𝒞' where C'_in: ‹𝒞' ∈ 𝒮'› and v_in_C': ‹v ∈ to_V ` (fset (A_of 𝒞'))›
        using v_in2 by blast
      then obtain a' where v_is': ‹v = to_V a'› and a'_in: ‹a' ∈ fset (A_of 𝒞')›
        by blast
      consider (J) ‹𝒞' ∈ 𝒮⇩𝒥› | (E') ‹𝒞' ∈ 𝒮⇩ℰ'›
        using C'_in 𝒮'_def by blast
      then show False
      proof cases
        case J
        then have ‹to_V ` (fset (A_of 𝒞')) ⊆ (to_V ` ⋃ (fset ` A_of ` 𝒮⇩𝒥))›
          by blast
        then have ‹to_V ` (fset (A_of 𝒞)) ⊆ (to_V ` ⋃ (fset ` A_of ` 𝒮⇩𝒥))›
          using C_is1 v_in_C' v_is by auto
        then have ‹𝒞 ∈ 𝒮⇩ℰ'›
          unfolding 𝒮⇩ℰ'_def using C_in by blast
        then show False
          using C_in by blast
      next
        case E'
        then consider (a) ‹𝒞' = Pair bot {|a|}› | (nega) ‹𝒞' = Pair bot {|neg a|}›
          unfolding 𝒮⇩ℰ'_def 𝒮⇩ℰ_def ℰ_from_def using v_in_C' v_is
            AF.sel(2) IntE empty_iff fset_simps(1) fset_simps(2) image_iff insert_iff
            mem_Collect_eq neg.simps(1) neg.simps(2) to_V.elims
          by (smt (verit, del_insts))
        then show False
        proof cases
          case a
          then show ?thesis
            using E' a_in_ℰ Enabled equiv_ℰ_enabled_𝒩 C_in C_is1 unfolding 𝒮⇩ℰ_def 𝒮⇩ℰ'_def
            by blast
        next
          case nega
          have ‹𝒞' ∈ ℰ_from 𝒩›
            using E' unfolding 𝒮⇩ℰ'_def 𝒮⇩ℰ_def by auto
          moreover have ‹𝒞 ∈ ℰ_from 𝒩›
            using C_in unfolding 𝒮⇩ℰ_def by auto
          ultimately show ?thesis
            using a_in_ℰ nega C_is1 Enabled equiv_ℰ_enabled_𝒩 by blast
        qed
      qed
    qed
    then have empty_inter: ‹⋃ (atoms ` (AF_proj_to_formula_set (𝒮⇩ℰ - 𝒮⇩ℰ'))) ∩
      ⋃ (atoms ` (AF_proj_to_formula_set 𝒮')) = {}›
      using atoms_simp proj_S' prop_proj_distrib prop_proj_sub
      by (smt (verit, ccfv_threshold) S_sub Un_subset_iff ‹𝒮 = 𝒮⇩ℰ - 𝒮⇩ℰ' ∪ 𝒮'› proj_prop_J'
        prop_proj_ℰ_from)
    have sat_rest: ‹sat (AF_proj_to_formula_set (𝒮⇩ℰ - 𝒮⇩ℰ'))›
      using E_sat unfolding 𝒮⇩ℰ'_def 𝒮⇩ℰ_def AF_proj_to_formula_set_def
        propositional_projection_def sat_def by blast
    have S'_unsat: ‹∀J. ¬ J ⊨⇩p2 𝒮'›
      using unsat_AF_simp[OF _ sat_rest empty_inter] S_unsat equiv_prop_entail2_sema2 S_is
        val_from_interp unfolding sat_def by metis
    have ex_fin_Js: ‹∃Js. 𝒮⇩𝒥 = 𝒥'_of ` Js ∧ (∀J∈Js. enabled_set 𝒩 J) ∧ finite Js›
      using finite_subset_with_prop[OF ex_Js S_fin 𝒮⇩𝒥_def] .
    then obtain Js where Js_fin: ‹finite Js› and Js_enab: ‹∀J∈Js. enabled_set 𝒩 J› and
      Js_is: ‹𝒥'_of ` Js = 𝒮⇩𝒥›
      by blast

    have fin_inter: ‹finite (⋃(fset ` A_of ` 𝒮⇩𝒥) ∩ ⋃(fset ` A_of ` 𝒩))›
    proof
      have ‹finite (⋃(fset ` A_of ` 𝒮⇩𝒥))›
        unfolding 𝒮⇩𝒥_def using S_fin image_Int_subset by simp
      then show ‹(finite (⋃(fset ` A_of ` 𝒮⇩𝒥))) ∨ (finite (⋃ (fset ` A_of ` 𝒩)))›
        by auto
    qed
    have ‹∀a∈(⋃(fset ` A_of ` 𝒩)). ∃𝒞∈𝒩. a ∈ fset (A_of 𝒞)›
      by blast
    then obtain f where f_def: ‹∀a∈(⋃(fset ` A_of ` 𝒩)). f a ∈ 𝒩 ∧ a ∈ fset (A_of (f a))›
      by metis
    define 𝒩⇩𝒥 where ‹𝒩⇩𝒥 = (f ` (⋃(fset ` A_of ` 𝒮⇩𝒥) ∩ ⋃(fset ` A_of ` 𝒩)))›
    have nj_fin: ‹finite 𝒩⇩𝒥›
      unfolding 𝒩⇩𝒥_def using fin_inter by blast
    have nj_sub: ‹𝒩⇩𝒥 ⊆ 𝒩›
      unfolding 𝒩⇩𝒥_def using f_def by blast
    have nj_as: ‹(∀a∈(⋃(fset ` A_of ` 𝒮⇩𝒥))∩(⋃(fset ` A_of ` 𝒩)).
      a ∈ ⋃(fset ` A_of ` 𝒩⇩𝒥))›
      unfolding 𝒩⇩𝒥_def using f_def by fast

    define ℳ' where ‹ℳ' = ⋃{ℳ'_of J |J. J ∈ Js}›
    define 𝒩' where  ‹𝒩' = ⋃{𝒩'_of J |J. J ∈ Js} ∪ 𝒩⇩𝒥›
    then have ‹ℳ' ⊆ ℳ›
      unfolding ℳ'_def using fsets_from_J Js_enab by fast
    moreover have ‹𝒩' ⊆ 𝒩›
      unfolding 𝒩'_def using fsets_from_J Js_enab nj_sub by fast
    moreover have ‹finite ℳ'›
      unfolding ℳ'_def using fsets_from_J Js_fin Js_enab by auto
    moreover have ‹finite 𝒩'›
      unfolding 𝒩'_def using fsets_from_J Js_fin Js_enab nj_fin by auto
    moreover have ‹ℳ' ⊨s⇩A⇩F 𝒩'› unfolding AF_entails_sound_def
    proof (rule allI, rule impI)
      fix J
      assume enab_N': ‹enabled_set 𝒩' J›
      then have ‹J ⊨⇩p2 ℰ_from 𝒩'›
        using equiv_ℰ_enabled_𝒩 by auto
      moreover have ‹𝒮⇩ℰ' ⊆ ℰ_from 𝒩'›
        proof
          fix 𝒞
          assume C_in: ‹𝒞 ∈ 𝒮⇩ℰ'›
          then obtain a where C_is: ‹𝒞 = Pair bot {|neg a|}›
            unfolding 𝒮⇩ℰ'_def 𝒮⇩ℰ_def ℰ_from_def by blast
          then have ‹neg a ∈ ⋃(fset ` A_of ` 𝒮⇩ℰ')›
            using C_in using image_iff by fastforce
          then have a_in_SJ: ‹a ∈ ⋃(fset ` A_of ` 𝒮⇩𝒥)›
            using a_from_E_to_J by presburger
          have ‹∃𝒞'∈𝒩. a ∈ fset (A_of 𝒞')›
            using C_is C_in unfolding 𝒮⇩ℰ'_def 𝒮⇩ℰ_def by (smt (verit, ccfv_threshold)
              AF.sel(2) IntE J'_is ℰ_from_def a_in_ℰ bot_fset.rep_eq empty_iff equiv_ℰ_enabled_𝒩
              finsert.rep_eq insert_iff mem_Collect_eq to_V.elims to_V_neg)
          then have ‹a ∈ ⋃(fset ` A_of ` 𝒩)›
            by blast
          then have ‹a ∈ ⋃(fset ` A_of ` 𝒩')›
            using nj_as a_in_SJ unfolding 𝒩'_def by simp
          then show ‹𝒞 ∈ ℰ_from 𝒩'›
            using C_is unfolding ℰ_from_def by blast
        qed
      ultimately have ‹J ⊨⇩p2 𝒮⇩ℰ'›
        unfolding 𝒮⇩ℰ'_def 𝒮⇩ℰ_def using subset_model_p2 by (metis (no_types, lifting))
      then have ‹¬ J ⊨⇩p2 𝒮⇩𝒥›
        using subset_not_model S'_unsat unfolding 𝒮'_def by blast
      then have  ‹∃J'∈Js. fset (A_of (𝒥'_of J')) ⊆ total_strip J›
        unfolding propositional_model2_def 𝒮⇩𝒥_def propositional_projection_def
          enabled_projection_def using Js_is
        by (smt (verit) Collect_cong Set.empty_def 𝒮⇩𝒥_def enabled_def image_iff mem_Collect_eq)
      then obtain J' where J'_in: ‹J' ∈ Js› and A_of_J'_in: ‹fset (A_of (𝒥'_of J')) ⊆ total_strip J›
        by blast
      then have enab_nj': ‹enabled_set 𝒩 J'›
        using Js_enab by blast
      then have ‹sound_cons.entails_neg (Pos ` (ℳ'_of J' proj⇩J J') ∪
        fml_ext ` (fset (A_of (𝒥'_of J')))) (Pos ` F_of ` 𝒩'_of J')›
        using fsets_from_J by auto
      moreover have ‹(ℳ'_of J') proj⇩J J' ⊆ (ℳ'_of J') proj⇩J J›
      proof -
        have ‹𝒞 ∈ ℳ'_of J' ⟹ enabled 𝒞 J' ⟹ enabled 𝒞 J› for 𝒞
        proof -
          assume C_in: ‹𝒞 ∈ ℳ'_of J'› and
            ‹enabled 𝒞 J'›
          then have ‹fset (A_of 𝒞) ⊆ fset (A_of (𝒥'_of J'))›
            using fsets_from_J[OF enab_nj'] by blast
          then show ‹enabled 𝒞 J›
            using A_of_J'_in unfolding enabled_def by auto
        qed
        then have ‹(𝒞 ∈ ℳ'_of J' ∧ enabled 𝒞 J') ⟹ (𝒞 ∈ ℳ'_of J' ∧ enabled 𝒞 J)› for 𝒞
          by (smt (verit, ccfv_threshold))
        then have ‹{𝒞. 𝒞 ∈ ℳ'_of J' ∧ enabled 𝒞 J'} ⊆ {𝒞. 𝒞 ∈ ℳ'_of J' ∧ enabled 𝒞 J}›
          by blast
        then show ‹(ℳ'_of J') proj⇩J J' ⊆ (ℳ'_of J') proj⇩J J›
          unfolding enabled_projection_def by blast
      qed
      ultimately have entails_one:  ‹sound_cons.entails_neg
        (Pos ` (ℳ'_of J' proj⇩J J) ∪ fml_ext ` (fset (A_of (𝒥'_of J')))) (Pos ` F_of ` 𝒩'_of J')›
        using sound_cons.entails_subsets
        by (smt (verit, ccfv_SIG) Un_absorb1 Un_assoc Un_left_commute image_Un
          neg_ext_sound_cons_rel.entails_subsets subset_refl sup.cobounded1)
      have subs_MJ: ‹Pos ` (ℳ'_of J' proj⇩J J) ∪
        fml_ext ` (fset (A_of (𝒥'_of J'))) ⊆ Pos ` (ℳ' proj⇩J J) ∪ fml_ext ` (total_strip J)›
        using J'_in A_of_J'_in using enabled_projection_def unfolding ℳ'_def by auto
      have subs_N: ‹Pos ` F_of ` (𝒩'_of J') ⊆ Pos ` F_of ` 𝒩'›
        using J'_in unfolding 𝒩'_def by blast
      show ‹sound_cons.entails_neg (fml_ext ` total_strip J ∪ Pos ` (ℳ' proj⇩J J))
        (Pos ` F_of ` 𝒩')›
        using neg_ext_sound_cons_rel.entails_subsets[OF subs_MJ subs_N entails_one]
        by (simp add: Un_commute)
    qed

    ultimately
    show ‹∃ℳ' 𝒩'. ℳ' ⊆ ℳ ∧ 𝒩' ⊆ 𝒩 ∧ finite ℳ' ∧ finite 𝒩' ∧ ℳ' ⊨s⇩A⇩F 𝒩'›
      by blast
  qed
qed
  
interpretation AF_sound_cons_rel: consequence_relation "to_AF bot" AF_entails_sound
  by (rule AF_ext_sound_cons_rel)

lemma f_of_to_AF [simp]: ‹F_of ` to_AF ` N = N›
  unfolding to_AF_def by force

lemma to_AF_proj_J [simp]: ‹to_AF ` M proj⇩J J = M›
  unfolding to_AF_def enabled_projection_def enabled_def by force

lemma enabled_to_AF_set [simp]: ‹enabled_set (to_AF ` N) J›
  unfolding enabled_set_def enabled_def to_AF_def by simp

lemma pos_not_pos_empty [simp]: ‹{to_V C |C. C ∈ Pos ` N ∧ ¬ is_Pos C} = {}›
  by auto
    
lemma pos_not_pos_simp [simp]:
  ‹{to_V C |C. C ∈ U ∪ Pos ` M ∧ ¬ is_Pos C} = {to_V C |C. C ∈ U ∧ ¬ is_Pos C}›
  by auto

lemma pos_pos_simp [simp]: ‹{to_V C |C. C ∈ Pos ` F_of ` N ∧ is_Pos C} = F_of ` N›
  by force 

lemma proj_F_of [simp]: ‹{C. F_of C ∈ M} proj⇩J J = M›
proof (intro equalityI subsetI)
  fix x
  assume x_in: ‹x ∈ {C. F_of C ∈ M} proj⇩J J›
  define C::"('f,'v) AF" where ‹C = to_AF x›
  then show ‹x ∈ M› 
    using x_in unfolding enabled_projection_def enabled_def to_AF_def by auto 
next
  fix x
  assume x_in: ‹x ∈ M›
  define C::"('f,'v) AF" where ‹C = to_AF x›
  then show ‹x ∈  {C. F_of C ∈ M} proj⇩J J› 
    using x_in unfolding enabled_projection_def enabled_def to_AF_def
    by (metis (mono_tags, lifting) AF.sel(1) AF.sel(2) bot_fset.rep_eq empty_subsetI mem_Collect_eq)
qed 

lemma f_of_F_of [simp]: ‹F_of ` {C. F_of C ∈ M} = M›
proof (intro equalityI subsetI)
  fix x
  assume x_in: ‹x ∈ F_of ` {C. F_of C ∈ M}›
  define C where ‹C = to_AF x›
  then show ‹x ∈ M›
    using x_in by blast 
next
  fix x
  assume x_in: ‹x ∈ M›
  define C where ‹C = to_AF x›
  then show ‹x ∈ F_of ` {C. F_of C ∈ M}›
    using x_in by (smt (z3) AF.sel(1) imageI mem_Collect_eq) 
qed
  
lemma set_on_union_triple_split: ‹{f C |C. C ∈ M ∪ N ∪ g J ∧ l C J} = {f C |C. C ∈ M ∧ l C J} ∪
  {f C |C. C ∈ N ∧ l C J} ∪ {f C |C. C ∈ g J ∧ l C J}›
  by blast 

lemma not_enabled_enabled_empty [simp]:
  ‹{F_of C |C. C ∈ {C. F_of C ∈ Q' ∧ ¬ enabled C J} ∧ enabled C J} = {}›
proof (intro equalityI subsetI)
  fix x
  assume x_in: ‹x ∈ {F_of C |C. C ∈ {C. F_of C ∈ Q' ∧ ¬ enabled C J} ∧ enabled C J}›
  then obtain C where ‹F_of C = x› and c_in: ‹C ∈ {C. F_of C ∈ Q' ∧ ¬ enabled C J}› and
    enab_c: ‹enabled C J›
    by blast
  then have ‹¬ enabled C J› using c_in by blast 
  then have ‹False› using enab_c by auto 
  then show ‹x ∈ {}› by auto 
qed auto

lemma f_of_simp_enabled [simp]: ‹{F_of C |C. F_of C ∈ M ∧ enabled C J} = M›
  unfolding enabled_def
  by (smt (verit, best) AF.sel(1) AF.sel(2) bot_fset.rep_eq empty_subsetI mem_Collect_eq subsetI
      subset_antisym)

lemma f_of_enabled_simp [simp]: ‹F_of ` {C. F_of C ∈ M ∧ enabled C J} = M›
proof -
  have ‹F_of ` {C. F_of C ∈ M ∧ enabled C J} = {F_of C |C. F_of C ∈ M ∧ enabled C J}›
    by blast 
  then show ?thesis by simp
qed

(* Splitting report Lemma 6, 1/2 *)
lemma ‹(to_AF ` M ⊨⇩A⇩F to_AF ` N) ≡ (M ⊨ N)›
  unfolding AF_entails_def by simp

sublocale ext_cons_rel_std: consequence_relation "Pos (to_AF bot)" AF_cons_rel.entails_neg
  using AF_cons_rel.ext_cons_rel .

sublocale sound_cons_rel: consequence_relation "Pos bot" sound_cons.entails_neg
  using sound_cons.ext_cons_rel .

lemma pos_in_pos_simp [simp]: ‹{C. Pos C ∈ Pos ` N} = N› by auto
lemma neg_not_in_pos_simp [simp]: ‹{C. Neg C ∈ Pos ` N} = {}› by auto
lemma neg_in_pos_simp [simp]: ‹{C. Neg C ∈ P ∨ Neg C ∈ Pos ` M} = {C. Neg C ∈ P}› by blast
lemma pos_in_pos_partial_simp [simp]: ‹{C. Pos C ∈ P ∨ Pos C ∈ Pos ` M} = {C. Pos C ∈ P} ∪ M› by auto
    
(* Splitting report Lemma 6, 2/2 *)
lemma ‹(to_AF ` M ⊨s⇩A⇩F to_AF ` N) ≡ (M ⊨s N)›
proof -
  {
    fix M N
    assume m_to_n: ‹M ⊨s N›
    have ‹to_AF ` M ⊨s⇩A⇩F to_AF ` N›
      unfolding AF_entails_sound_def sound_cons.entails_neg_def 
    proof (rule allI, rule impI)
      fix J
      have ‹{C. Pos C ∈ fml_ext ` total_strip J} ∪ M ⊨s N ∪ {C. Neg C ∈ fml_ext ` total_strip J}›
      proof -
        have m_in: ‹M ⊆ {to_V C |C. (C ∈ fml_ext ` total_strip J ∨ C ∈ Pos ` M) ∧ is_Pos C}›
          by force
        show ‹ {C. Pos C ∈ fml_ext ` total_strip J} ∪ M ⊨s
          N ∪ {C. Neg C ∈ fml_ext ` total_strip J}›
          using m_to_n m_in by (meson Un_subset_iff sound_cons.entails_subsets subset_refl)
      qed
      then show ‹{C. Pos C ∈ fml_ext ` total_strip J ∪ Pos ` (to_AF ` M proj⇩J J)} ∪ 
        {C. Neg C ∈ Pos ` F_of ` to_AF ` N} ⊨s {C. Pos C ∈ Pos ` F_of ` to_AF ` N} ∪
        {C. Neg C ∈ fml_ext ` total_strip J ∪ Pos ` (to_AF ` M proj⇩J J)}›
        by simp
    qed
  } moreover {
    fix M N
    assume m_af_entails_n: ‹to_AF ` M ⊨s⇩A⇩F to_AF ` N›
    have ‹M ⊆ M' ⟹ N ⊆ N' ⟹ M' ∪ N' = UNIV ⟹ M' ⊨s N'› for M' N'
    proof - 
      fix M' N'
      assume m_in: ‹M ⊆ M'› and
        n_in: ‹N ⊆ N'› and
        union_mnp_is_univ: ‹M' ∪ N' = UNIV›
      {
        assume ‹M' ∩ N' ≠ {}›
        then have ‹M' ⊨s N'›
          using sound_cons.entails_reflexive sound_cons.entails_subsets
          by (meson Int_lower1 Int_lower2 sound_cons.entails_cond_reflexive)
      }
      moreover {
        assume empty_inter_mp_np: ‹M' ∩ N' = {}›
        define Jpos where ‹Jpos = {v. to_V (fml_ext v) ∈ M' ∧ is_Pos v}›
        define Jneg where ‹Jneg = {v |v. to_V (fml_ext v) ∉ M' ∧ ¬ is_Pos v}›
        have total_J_pos_neg: ‹to_V ` (Jpos ∪ Jneg) = UNIV›
        proof
          show ‹to_V ` (Jpos ∪ Jneg) ⊆ UNIV› by simp
        next
          show ‹UNIV ⊆ to_V ` (Jpos ∪ Jneg) ›
          proof
            fix v::"'v"
            define v_p where ‹v_p = Pos v›
            define v_n where ‹v_n = Neg v›
            have ‹v_p ∉ Jpos ⟹ v_n ∈ Jneg›
              unfolding v_p_def v_n_def Jpos_def Jneg_def by simp
            then show ‹v ∈ to_V ` (Jpos ∪ Jneg)›
              unfolding v_p_def v_n_def by force
          qed
        qed
        define Jstrip where ‹Jstrip = Jpos ∪ Jneg›
        have interp_Jstrip: ‹is_interpretation Jstrip›
          unfolding is_interpretation_def
        proof (rule ballI, rule ballI, rule impI, rule ccontr)
          fix v1 v2
          assume v1_in: ‹v1 ∈ Jstrip› and
            v2_in: ‹v2 ∈ Jstrip› and
            v12_eq: ‹to_V v1 = to_V v2› and
            contra: ‹v1 ≠ v2›
          have pos_neg_cases: ‹(v1 ∈ Jpos ∧ v2 ∈ Jneg) ∨ (v1 ∈ Jneg ∧ v2 ∈ Jpos)›
            using v1_in v2_in contra unfolding Jstrip_def Jpos_def Jneg_def
            by (smt (z3) Collect_mono_iff Collect_subset Un_def is_Neg_to_V is_Pos_to_V v12_eq)
          then have ‹to_V (fml_ext v1) ≠ to_V (fml_ext v2)›
            using empty_inter_mp_np unfolding Jneg_def Jpos_def by auto 
          then show ‹False›
            using fml_ext_preserves_val[OF v12_eq] by blast 
        qed
        then obtain Jinterp where Jinterp_is: "strip Jinterp = Jstrip"
          by (metis Rep_propositional_interpretation_cases mem_Collect_eq)
        have ‹total Jinterp›
          unfolding total_def
        proof
          fix v
          define v_p::"'v sign" where "v_p = Pos v"
          define v_n::"'v sign" where "v_n = Neg v"
          have "v_p ∈ Jpos ∨ v_n ∈ Jneg"
            unfolding v_p_def v_n_def Jpos_def Jneg_def by simp
          then have "v_p ∈ Jstrip ∨ v_n ∈ Jstrip"
            unfolding Jstrip_def by fast
          then have ‹v_p ∈⇩J Jinterp ∨ v_n ∈⇩J Jinterp›
            using Jinterp_is unfolding belong_to_def by simp
          then show ‹∃v⇩J. v⇩J ∈⇩J Jinterp ∧ to_V v⇩J = v›
            using v_p_def v_n_def by auto
        qed
        then obtain Jtotal where Jtotal_is: "total_strip Jtotal = Jstrip"
          using Jinterp_is by (metis Rep_total_interpretation_cases mem_Collect_eq)
        have ‹enabled_set (to_AF ` N) Jtotal›
          unfolding enabled_set_def to_AF_def enabled_def using Jtotal_is Jstrip_def Jneg_def
          by simp
        then have ‹fml_ext ` total_strip Jtotal ∪ Pos ` M ⊨s⇩∼ Pos ` N›
          using m_af_entails_n unfolding AF_entails_sound_def by simp
        then have entails_m_n_jtot: ‹{C. Pos C ∈ fml_ext ` total_strip Jtotal} ∪ M  ⊨s
           N ∪ {C. Neg C ∈ fml_ext ` total_strip Jtotal}›
          unfolding sound_cons.entails_neg_def by simp
        have ‹{C. Pos C ∈ fml_ext ` total_strip Jtotal} ⊆ M'›
          unfolding Jtotal_is Jstrip_def Jpos_def Jneg_def
          by (smt (verit, ccfv_threshold) UnE fml_ext_preserves_sign imageE is_Pos.simps(1)
            mem_Collect_eq subsetI to_V.simps(1))
        then have sub_mp: ‹{C. Pos C ∈ fml_ext ` total_strip Jtotal} ∪ M ⊆ M'›
          using m_in by simp
        have ‹{C. Neg C ∈ fml_ext ` total_strip Jtotal} ⊆ N'›
          unfolding Jtotal_is Jstrip_def Jpos_def Jneg_def
        proof -
          have ‹{C. Neg C ∈ fml_ext ` {v. to_V (fml_ext v) ∈ M' ∧ is_Pos v}} = {}›
            using fml_ext_preserves_sign is_Pos.simps(1)
            by (smt (verit, ccfv_SIG) empty_iff imageE is_Pos.simps(2) mem_Collect_eq subsetI
              subset_antisym)
          moreover have ‹{C. Neg C ∈ fml_ext ` {v |v. to_V (fml_ext v) ∉ M' ∧ ¬ is_Pos v}} ⊆ N'›
            using fml_ext_preserves_sign is_Pos.simps(2)
          proof -
            have ‹{C. Neg C ∈ fml_ext ` {v |v. to_V (fml_ext v) ∉ M' ∧ ¬ is_Pos v}} =
              {C. Neg C ∈ fml_ext ` {v |v. to_V (fml_ext v) ∈ N' ∧ ¬ is_Pos v}}›
              using empty_inter_mp_np union_mnp_is_univ by auto 
            also have ‹{C. Neg C ∈ fml_ext ` {v |v. to_V (fml_ext v) ∈ N' ∧ ¬ is_Pos v}} ⊆ N'›
              using fml_ext_preserves_sign is_Pos.simps(2)
              by (smt (verit, best) imageE mem_Collect_eq subsetI to_V.simps(2))      
            finally show ‹{C. Neg C ∈ fml_ext ` {v |v. to_V (fml_ext v) ∉ M' ∧ ¬ is_Pos v}} ⊆ N'› .
          qed
          ultimately show ‹{C. Neg C ∈ fml_ext `
            ({v. to_V (fml_ext v) ∈ M' ∧ is_Pos v} ∪
            {v |v. to_V (fml_ext v) ∉ M' ∧ ¬ is_Pos v})}
            ⊆ N'›
            by blast
        qed
        then have sub_np: ‹N ∪ {C. Neg C ∈ fml_ext ` total_strip Jtotal} ⊆ N'›
          using n_in by blast
        have ‹M' ⊨s N'›
          using sound_cons.entails_subsets[OF sub_mp sub_np entails_m_n_jtot] .
      }
      ultimately show "M' ⊨s N'" by blast
    qed
    then have supsets_entail: ‹∀M' N'. (M' ⊇ M ∧ N' ⊇ N ∧ M' ∪ N' = UNIV) ⟶ M' ⊨s N'›
      by clarsimp
    then have ‹M ⊨s N›
      using sound_cons.entails_supsets by simp
  }
  ultimately show ‹(to_AF ` M ⊨s⇩A⇩F to_AF ` N) ≡ (M ⊨s N)›
    by (smt (verit, best))
qed

lemma strong_entails_bot_cases: ‹𝒩 ∪ {AF.Pair bot A} ⊨s⇩A⇩F {AF.Pair bot B} ⟹
  (∀ J. fset B ⊆ total_strip J ⟶
    (fml_ext ` total_strip J ∪ Pos ` (𝒩 proj⇩J J)) ⊨s⇩∼ {Pos bot} ∨ fset A ⊆ total_strip J)›
proof -
  assume ‹𝒩 ∪ {AF.Pair bot A} ⊨s⇩A⇩F {AF.Pair bot B}›
  then have ‹fset B ⊆ total_strip J ⟹
              (fml_ext ` total_strip J ∪ Pos ` (𝒩 proj⇩J J) ∪ Pos ` ({AF.Pair bot A} proj⇩J J))
              ⊨s⇩∼ {Pos bot}›
    for J
    unfolding AF_entails_sound_def
    by (metis (no_types, lifting) AF.sel(1) AF.sel(2) distrib_proj_singleton enabled_def
         enabled_set_def image_Un image_empty image_insert singletonD sup_assoc)
  then have ‹fset B ⊆ total_strip J ⟹
        ((fml_ext ` total_strip J) ∪ Pos ` (𝒩 proj⇩J J)) ⊨s⇩∼ {Pos bot} ∨ enabled (AF.Pair bot A) J›
    for J 
    by (smt (verit, ccfv_SIG) enabled_projection_def ex_in_conv image_empty
         mem_Collect_eq singletonD sup_bot_right)
  then show ?thesis
    by (simp add: enabled_def)
qed

lemma strong_entails_bot_cases_Union:
  ‹𝒩 ∪ ℳ ⊨s⇩A⇩F {AF.Pair bot B} ⟹ (∀ x ∈ ℳ. F_of x = bot) ⟹
    (∀ J. fset B ⊆ total_strip J ⟶
      (fml_ext ` total_strip J ∪ Pos ` (𝒩 proj⇩J J)) ⊨s⇩∼ {Pos bot} ∨
      (∃ A ∈ A_of ` ℳ. fset A ⊆ total_strip J))›
proof -
  assume 𝒩_union_ℳ_entails_Pair_bot_B: ‹𝒩 ∪ ℳ ⊨s⇩A⇩F {AF.Pair bot B}› and
         ‹∀ x ∈ ℳ. F_of x = bot›
  then show ?thesis
  proof (cases ‹ℳ = {}›)
    case True
    then show ?thesis
      using AF_entails_sound_def 𝒩_union_ℳ_entails_Pair_bot_B enabled_def enabled_set_def
      by auto
  next
    case False
    then show ?thesis
    proof (intro allI impI)
      fix J
      assume B_in_J: ‹fset B ⊆ total_strip J›
      then show ‹(fml_ext ` total_strip J ∪ Pos ` (𝒩 proj⇩J J)) ⊨s⇩∼ {Pos bot} ∨
                    (∃ A ∈ A_of ` ℳ. fset A ⊆ total_strip J)›
      proof (cases ‹∃ A ∈ A_of ` ℳ. fset A ⊆ total_strip J›)
        case True
        then show ?thesis
          by blast
      next
        case False
        then have ‹∀ A ∈ A_of ` ℳ. ¬ fset A ⊆ total_strip J›
          by blast
        then have ‹ℳ proj⇩J J = {}›
          by (simp add: enabled_def enabled_projection_def)
        then show ?thesis
          using 𝒩_union_ℳ_entails_Pair_bot_B[unfolded AF_entails_sound_def, rule_format]
                B_in_J distrib_proj enabled_def enabled_set_def
          by fastforce
      qed
    qed
  qed
qed


lemma AF_entails_sound_right_disjunctive: ‹(∃ 𝒞' ∈ A. ℳ ⊨s⇩A⇩F {𝒞'}) ⟹ ℳ ⊨s⇩A⇩F A›
proof -
  assume ‹∃ 𝒞' ∈ A. ℳ ⊨s⇩A⇩F {𝒞'}›
  then obtain 𝒞' where ‹ℳ ⊨s⇩A⇩F {𝒞'}› and
                       ‹𝒞' ∈ A›
    by blast
  then show ‹ℳ ⊨s⇩A⇩F A›
    by (meson AF_sound_cons_rel.entails_subsets empty_subsetI insert_subset subset_refl)
qed

subsection ‹Local saturation›

text ‹ To fully capture completeness for splitting, we need to use weaker notions of saturation and
 fairness.›

(* Report definition 23 *)
definition locally_saturated :: ‹('f, 'v) AF set ⇒ bool› where
  ‹locally_saturated 𝒩 ≡
    to_AF bot ∈ 𝒩 ∨
    (∃ J :: 'v total_interpretation. J ⊨⇩p 𝒩 ∧ saturated (𝒩 proj⇩J J))›
    (* NOTE: in the paper, the propositional projection is explicit.
     * In our case, it is hidden within the definition for @{const propositional_model}. *)

(* Report definition 26 *)
definition locally_fair :: ‹('f, 'v) AF set infinite_llist ⇒ bool› where
  ‹locally_fair 𝒩i ≡
     (∃ i. to_AF bot ∈ llnth 𝒩i i)
   ∨ (∃ J :: 'v total_interpretation. J ⊨⇩p lim_inf 𝒩i ∧
        Inf_from (lim_inf 𝒩i proj⇩J J) ⊆ (⋃ i. Red⇩I (llnth 𝒩i i proj⇩J J)))›

end (* locale calculus_with_annotated_consrel *)

locale strong_statically_complete_annotated_calculus =  
  calculus_with_annotated_consrel  bot Inf entails entails_sound Red⇩I Red⇩F fml asn
  + S_calculus: calculus "to_AF bot" SInf AF_entails SRed⇩I SRed⇩F
  for
    bot :: "'f" and
    Inf :: ‹'f inference set› and
    entails :: "'f set ⇒ 'f set ⇒ bool" (infix "⊨" 50) and
    entails_sound :: "'f set ⇒ 'f set ⇒ bool" (infix "⊨s" 50) and
    Red⇩I :: "'f set ⇒ 'f inference set" and
    Red⇩F :: "'f set ⇒ 'f set" and
    fml :: ‹'v :: countable ⇒ 'f› and 
    asn :: ‹'f sign ⇒ 'v sign set› and
    SInf :: "('f, 'v) AF inference set" and
    SRed⇩I :: "('f, 'v) AF set ⇒ ('f, 'v) AF inference set" and
    SRed⇩F :: "('f, 'v) AF set ⇒ ('f, 'v) AF set"
  + assumes
    strong_static_completeness: ‹locally_saturated 𝒩 ⟹ 𝒩 ⊨⇩A⇩F {to_AF bot} ⟹ to_AF bot ∈ 𝒩›

locale strong_dynamically_complete_annotated_calculus =  
  calculus_with_annotated_consrel  bot Inf entails entails_sound Red⇩I Red⇩F fml asn
  + S_calculus: calculus "to_AF bot" SInf AF_entails SRed⇩I SRed⇩F
  for
    bot :: "'f" and
    Inf :: ‹'f inference set› and
    entails :: "'f set ⇒ 'f set ⇒ bool" (infix "⊨" 50) and
    entails_sound :: "'f set ⇒ 'f set ⇒ bool" (infix "⊨s" 50) and
    Red⇩I :: "'f set ⇒ 'f inference set" and
    Red⇩F :: "'f set ⇒ 'f set" and
    fml :: ‹'v :: countable ⇒ 'f› and 
    asn :: ‹'f sign ⇒ 'v sign set› and
    SInf :: "('f, 'v) AF inference set" and
    SRed⇩I :: "('f, 'v) AF set ⇒ ('f, 'v) AF inference set" and
    SRed⇩F :: "('f, 'v) AF set ⇒ ('f, 'v) AF set"
  + assumes
    strong_dynamic_completeness: ‹is_derivation S_calculus.derive 𝒩i ⟹ locally_fair 𝒩i ⟹
      llhd 𝒩i ⊨⇩A⇩F {to_AF bot} ⟹ ∃i. to_AF bot ∈ llnth 𝒩i i›


end