Theory Ground_Ordered_Resolution

theory Ground_Ordered_Resolution
  imports
    Saturation_Framework.Calculus
    Saturation_Framework_Extensions.Clausal_Calculus
    Isabelle_2024_Compatibility
    Superposition_Calculus.Ground_Ctxt_Extra
    Superposition_Calculus.HOL_Extra
    Superposition_Calculus.Transitive_Closure_Extra
    Min_Max_Least_Greatest.Min_Max_Least_Greatest_FSet
    Min_Max_Least_Greatest.Min_Max_Least_Greatest_Multiset
    Superposition_Calculus.Multiset_Extra
    Superposition_Calculus.Relation_Extra
begin

hide_type Inference_System.inference
hide_const
  Inference_System.Infer
  Inference_System.prems_of
  Inference_System.concl_of
  Inference_System.main_prem_of

primrec mset_lit :: "'a literal ⇒ 'a multiset" where
  "mset_lit (Pos A) = {#A#}" |
  "mset_lit (Neg A) = {#A, A#}"

type_synonym 't atom = "'t"


section ‹Ground Resolution Calculus›

locale ground_ordered_resolution_calculus =
  fixes
    less_trm :: "'f gterm ⇒ 'f gterm ⇒ bool" (infix "≺⇩t" 50) and
    select :: "'f gterm atom clause ⇒ 'f gterm atom clause"
  assumes
    transp_less_trm[simp]: "transp (≺⇩t)" and
    asymp_less_trm[intro]: "asymp (≺⇩t)" and
    wfP_less_trm[intro]: "wfP (≺⇩t)" and
    totalp_less_trm[intro]: "totalp (≺⇩t)" and
    less_trm_compatible_with_gctxt[simp]: "⋀ctxt t t'. t ≺⇩t t' ⟹ ctxt⟨t⟩⇩G ≺⇩t ctxt⟨t'⟩⇩G" and
    less_trm_if_subterm[simp]: "⋀t ctxt. ctxt ≠ □⇩G ⟹ t ≺⇩t ctxt⟨t⟩⇩G" and
    select_subset: "⋀C. select C ⊆# C" and
    select_negative_lits: "⋀C L. L ∈# select C ⟹ is_neg L"
begin

lemma irreflp_on_less_trm[simp]: "irreflp_on A (≺⇩t)"
  by (metis asympD asymp_less_trm irreflp_onI)

abbreviation lesseq_trm (infix "≼⇩t" 50) where
  "lesseq_trm ≡ (≺⇩t)⇧=⇧="

lemma lesseq_trm_if_subtermeq: "t ≼⇩t ctxt⟨t⟩⇩G"
  using less_trm_if_subterm
  by (metis gctxt_ident_iff_eq_GHole reflclp_iff)

definition less_lit ::
  "'f gterm atom literal ⇒ 'f gterm atom literal ⇒ bool" (infix "≺⇩l" 50) where
  "less_lit L1 L2 ≡ multp (≺⇩t) (mset_lit L1) (mset_lit L2)"

abbreviation lesseq_lit (infix "≼⇩l" 50) where
  "lesseq_lit ≡ (≺⇩l)⇧=⇧="

abbreviation less_cls ::
  "'f gterm atom clause ⇒ 'f gterm atom clause ⇒ bool" (infix "≺⇩c" 50) where
  "less_cls ≡ multp (≺⇩l)"

abbreviation lesseq_cls (infix "≼⇩c" 50) where
  "lesseq_cls ≡ (≺⇩c)⇧=⇧="

lemma transp_on_less_lit[simp]: "transp_on A (≺⇩l)"
  by (smt (verit, best) less_lit_def transpE transp_less_trm transp_multp transp_onI)

corollary transp_less_lit: "transp (≺⇩l)"
  by simp

lemma transp_less_cls[simp]: "transp (≺⇩c)"
  by (simp add: transp_multp)

lemma asymp_on_less_lit[simp]: "asymp_on A (≺⇩l)"
  by (metis asympD asymp_less_trm asymp_multp⇩H⇩O asymp_onI less_lit_def multp_eq_multp⇩H⇩O
      transp_less_trm)

corollary asymp_less_lit[simp]: "asymp (≺⇩l)"
  by simp

lemma asymp_less_cls[simp]: "asymp (≺⇩c)"
  by (simp add: asymp_multp⇩H⇩O multp_eq_multp⇩H⇩O)

lemma irreflp_on_less_lit[simp]: "irreflp_on A (≺⇩l)"
  by (simp only: asymp_on_less_lit irreflp_on_if_asymp_on)

lemma wfP_less_lit[simp]: "wfP (≺⇩l)"
  unfolding less_lit_def
  using wfP_less_trm wfp_multp wfp_if_convertible_to_wfp by meson

lemma wfP_less_cls[simp]: "wfP (≺⇩c)"
  using wfP_less_lit wfp_multp by blast

lemma totalp_on_less_lit[simp]: "totalp_on A (≺⇩l)"
proof (rule totalp_onI)
  fix L1 L2 :: "'f gterm atom literal"
  assume "L1 ≠ L2"

  show "L1 ≺⇩l L2 ∨ L2 ≺⇩l L1"
    unfolding less_lit_def
  proof (rule totalp_multp[THEN totalpD])
    show "totalp (≺⇩t)"
      using totalp_less_trm .
  next
    show "transp (≺⇩t)"
      using transp_less_trm .
  next
    show "mset_lit L1 ≠ mset_lit L2"
      using ‹L1 ≠ L2›
      by (cases L1; cases L2) (auto simp add: add_eq_conv_ex)
  qed
qed

corollary totalp_less_lit: "totalp (≺⇩l)"
  by simp

lemma totalp_less_cls[simp]: "totalp (≺⇩c)"
proof (rule totalp_multp)
  show "totalp (≺⇩l)"
    by simp
next
  show "transp (≺⇩l)"
    by simp
qed

interpretation term_order: linorder lesseq_trm less_trm
proof unfold_locales
  show "⋀x y. (x ≺⇩t y) = (x ≼⇩t y ∧ ¬ y ≼⇩t x)"
    by (metis asympD asymp_less_trm reflclp_iff)
next
  show "⋀x. x ≼⇩t x"
    by simp
next
  show "⋀x y z. x ≼⇩t y ⟹ y ≼⇩t z ⟹ x ≼⇩t z"
    by (meson transpE transp_less_trm transp_on_reflclp)
next
  show "⋀x y. x ≼⇩t y ⟹ y ≼⇩t x ⟹ x = y"
    by (metis asympD asymp_less_trm reflclp_iff)
next
  show "⋀x y. x ≼⇩t y ∨ y ≼⇩t x"
    by (metis reflclp_iff totalpD totalp_less_trm)
qed

interpretation literal_order: linorder lesseq_lit less_lit
proof unfold_locales
  show "⋀x y. (x ≺⇩l y) = (x ≼⇩l y ∧ ¬ y ≼⇩l x)"
    by (metis asympD asymp_less_lit reflclp_iff)
next
  show "⋀x. x ≼⇩l x"
    by simp
next
  show "⋀x y z. x ≼⇩l y ⟹ y ≼⇩l z ⟹ x ≼⇩l z"
    by (meson transpE transp_less_lit transp_on_reflclp)
next
  show "⋀x y. x ≼⇩l y ⟹ y ≼⇩l x ⟹ x = y"
    by (metis asympD asymp_less_lit reflclp_iff)
next
  show "⋀x y. x ≼⇩l y ∨ y ≼⇩l x"
    by (metis reflclp_iff totalpD totalp_less_lit)
qed

interpretation clause_order: linorder lesseq_cls less_cls
proof unfold_locales
  show "⋀x y. (x ≺⇩c y) = (x ≼⇩c y ∧ ¬ y ≼⇩c x)"
    by (metis asympD asymp_less_cls reflclp_iff)
next
  show "⋀x. x ≼⇩c x"
    by simp
next
  show "⋀x y z. x ≼⇩c y ⟹ y ≼⇩c z ⟹ x ≼⇩c z"
    by (meson transpE transp_less_cls transp_on_reflclp)
next
  show "⋀x y. x ≼⇩c y ⟹ y ≼⇩c x ⟹ x = y"
    by (metis asympD asymp_less_cls reflclp_iff)
next
  show "⋀x y. x ≼⇩c y ∨ y ≼⇩c x"
    by (metis reflclp_iff totalpD totalp_less_cls)
qed

lemma less_lit_simps[simp]:
  "Pos A⇩1 ≺⇩l Pos A⇩2 ⟷ A⇩1 ≺⇩t A⇩2"
  "Pos A⇩1 ≺⇩l Neg A⇩2 ⟷ A⇩1 ≼⇩t A⇩2"
  "Neg A⇩1 ≺⇩l Neg A⇩2 ⟷ A⇩1 ≺⇩t A⇩2"
  "Neg A⇩1 ≺⇩l Pos A⇩2 ⟷ A⇩1 ≺⇩t A⇩2"
  by (auto simp add: less_lit_def)


subsection ‹Ground Rules›

abbreviation is_maximal_lit :: "'f gterm literal ⇒ 'f gterm clause ⇒ bool" where
  "is_maximal_lit L M ≡ is_maximal_in_mset_wrt (≺⇩l) M L"

abbreviation is_strictly_maximal_lit :: "'f gterm literal ⇒ 'f gterm clause ⇒ bool" where
  "is_strictly_maximal_lit L M ≡ is_greatest_in_mset_wrt (≺⇩l) M L"

inductive ground_resolution ::
  "'f gterm atom clause ⇒ 'f gterm atom clause ⇒ 'f gterm atom clause ⇒ bool"
where
  ground_resolutionI: "
    P⇩1 = add_mset (Neg t) P⇩1' ⟹
    P⇩2 = add_mset (Pos t) P⇩2' ⟹
    P⇩2 ≺⇩c P⇩1 ⟹
    select P⇩1 = {#} ∧ is_maximal_lit (Neg t) P⇩1 ∨ Neg t ∈# select P⇩1 ⟹
    select P⇩2 = {#} ⟹
    is_strictly_maximal_lit (Pos t) P⇩2 ⟹
    C = P⇩1' + P⇩2' ⟹
    ground_resolution P⇩1 P⇩2 C"

inductive ground_factoring :: "'f gterm atom clause ⇒ 'f gterm atom clause ⇒ bool" where
  ground_factoringI: "
    P = add_mset (Pos t) (add_mset (Pos t) P') ⟹
    select P = {#} ⟹
    is_maximal_lit (Pos t) P ⟹
    C = add_mset (Pos t) P' ⟹
    ground_factoring P C"


subsection ‹Ground Layer›

definition G_Inf :: "'f gterm atom clause inference set" where
  "G_Inf =
    {Infer [P⇩2, P⇩1] C | P⇩2 P⇩1 C. ground_resolution P⇩1 P⇩2 C} ∪
    {Infer [P] C | P C. ground_factoring P C}"

abbreviation G_Bot :: "'f gterm atom clause set" where
  "G_Bot ≡ {{#}}"

definition G_entails :: "'f gterm atom clause set ⇒ 'f gterm atom clause set ⇒ bool" where
  "G_entails N⇩1 N⇩2 ⟷ (∀(I :: 'f gterm set). I ⊫s N⇩1 ⟶ I ⊫s N⇩2)"


subsection ‹Correctness›

lemma soundness_ground_resolution:
  assumes
    step: "ground_resolution P1 P2 C"
  shows "G_entails {P1, P2} {C}"
  using step
proof (cases P1 P2 C rule: ground_resolution.cases)
  case (ground_resolutionI t P⇩1' P⇩2')

  show ?thesis
    unfolding G_entails_def true_clss_singleton
    unfolding true_clss_insert
  proof (intro allI impI, elim conjE)
    fix I :: "'f gterm set"
    assume "I ⊫ P1" and "I ⊫ P2"
    then obtain K1 K2 :: "'f gterm atom literal" where
      "K1 ∈# P1" and "I ⊫l K1" and "K2 ∈# P2" and "I ⊫l K2"
      by (auto simp: true_cls_def)

    show "I ⊫ C"
    proof (cases "K1 = Neg t")
      case K1_def: True
      hence "I ⊫l Neg t"
        using ‹I ⊫l K1› by simp

      show ?thesis
      proof (cases "K2 = Pos t")
        case K2_def: True
        hence "I ⊫l Pos t"
          using ‹I ⊫l K2› by simp
        hence False
          using ‹I ⊫l Neg t› by simp
        thus ?thesis ..
      next
        case False
        hence "K2 ∈# P⇩2'"
          using ‹K2 ∈# P2›
          unfolding ground_resolutionI by simp
        hence "I ⊫ P⇩2'"
          using ‹I ⊫l K2› by blast
        thus ?thesis
          unfolding ground_resolutionI by simp
      qed
    next
      case False
      hence "K1 ∈# P⇩1'"
        using ‹K1 ∈# P1›
        unfolding ground_resolutionI by simp
      hence "I ⊫ P⇩1'"
        using ‹I ⊫l K1› by blast
      thus ?thesis
        unfolding ground_resolutionI by simp
    qed
  qed
qed

lemma soundness_ground_factoring:
  assumes step: "ground_factoring P C"
  shows "G_entails {P} {C}"
  using step
proof (cases P C rule: ground_factoring.cases)
  case (ground_factoringI t P')
  show ?thesis
    unfolding G_entails_def true_clss_singleton
  proof (intro allI impI)
    fix I :: "'f gterm set"
    assume "I ⊫ P"
    then obtain K :: "'f gterm atom literal" where
      "K ∈# P" and "I ⊫l K"
      by (auto simp: true_cls_def)

    show "I ⊫ C"
    proof (cases "K = Pos t")
      case True
      hence "I ⊫l Pos t"
        using ‹I ⊫l K› by metis
      thus ?thesis
        unfolding ground_factoringI
        by (metis true_cls_add_mset)
    next
      case False
      hence "K ∈# P'"
        using ‹K ∈# P›
        unfolding ground_factoringI
        by auto
      hence "K ∈# C"
        unfolding ground_factoringI
        by simp
      thus ?thesis
        using ‹I ⊫l K› by blast
    qed
  qed
qed

interpretation G: sound_inference_system G_Inf G_Bot G_entails
proof unfold_locales
  show "G_Bot ≠ {}"
    by simp
next
  show "⋀B N. B ∈ G_Bot ⟹ G_entails {B} N"
    by (simp add: G_entails_def)
next
  show "⋀N2 N1. N2 ⊆ N1 ⟹ G_entails N1 N2"
    by (auto simp: G_entails_def elim!: true_clss_mono[rotated])
next
  fix N1 N2 assume ball_G_entails: "∀C ∈ N2. G_entails N1 {C}"
  show "G_entails N1 N2"
    unfolding G_entails_def
  proof (intro allI impI)
    fix I :: "'f gterm set"
    assume "I ⊫s N1"
    hence "∀C ∈ N2. I ⊫s {C}"
      using ball_G_entails by (simp add: G_entails_def)
    then show "I ⊫s N2"
      by (simp add: true_clss_def)
  qed
next
  show "⋀N1 N2 N3. G_entails N1 N2 ⟹ G_entails N2 N3 ⟹ G_entails N1 N3"
    using G_entails_def by simp
next
  show "⋀ι. ι ∈ G_Inf ⟹ G_entails (set (prems_of ι)) {concl_of ι}"
    unfolding G_Inf_def
    using soundness_ground_resolution
    using soundness_ground_factoring
    by (auto simp: G_entails_def)
qed


subsection ‹Redundancy Criterion›

lemma ground_resolution_smaller_conclusion:
  assumes
    step: "ground_resolution P1 P2 C"
  shows "C ≺⇩c P1"
  using step
proof (cases P1 P2 C rule: ground_resolution.cases)
  case (ground_resolutionI t P⇩1' P⇩2')
  have "∀k∈#P⇩2'. k ≺⇩l Pos t"
    using ‹is_strictly_maximal_lit (Pos t) P2› ‹P2 = add_mset (Pos t) P⇩2'›
    by (simp add: literal_order.is_greatest_in_mset_iff)
  moreover have "⋀A. Pos A ≺⇩l Neg A"
    by (simp add: less_lit_def)
  ultimately have "∀k∈#P⇩2'. k ≺⇩l Neg t"
    by (metis transp_def transp_less_lit)
  hence "P⇩2' ≺⇩c {#Neg t#}"
    using one_step_implies_multp[of "{#Neg t#}" P⇩2' "(≺⇩l)" "{#}"] by simp
  hence "P⇩2' + P⇩1' ≺⇩c add_mset (Neg t) P⇩1'"
    using multp_cancel[of "(≺⇩l)" P⇩1' P⇩2' "{#Neg t#}"] by simp
  thus ?thesis
    unfolding ground_resolutionI
    by (simp only: add.commute)
qed

lemma ground_factoring_smaller_conclusion:
  assumes step: "ground_factoring P C"
  shows "C ≺⇩c P"
  using step
proof (cases P C rule: ground_factoring.cases)
  case (ground_factoringI t P')
  then show ?thesis
    by (metis add_mset_add_single mset_subset_eq_exists_conv multi_self_add_other_not_self
        multp_subset_supersetI totalpD totalp_less_cls transp_less_lit)
qed

interpretation G: calculus_with_finitary_standard_redundancy G_Inf G_Bot G_entails "(≺⇩c)"
proof unfold_locales
  show "transp (≺⇩c)"
    using transp_less_cls .
next
  show "wfP (≺⇩c)"
    using wfP_less_cls .
next
  show "⋀ι. ι ∈ G_Inf ⟹ prems_of ι ≠ []"
    by (auto simp: G_Inf_def)
next
  fix ι
  have "concl_of ι ≺⇩c main_prem_of ι"
    if ι_def: "ι = Infer [P⇩2, P⇩1] C" and
      infer: "ground_resolution P⇩1 P⇩2 C"
    for P⇩2 P⇩1 C
    unfolding ι_def
    using infer
    using ground_resolution_smaller_conclusion
    by simp

  moreover have "concl_of ι ≺⇩c main_prem_of ι"
    if ι_def: "ι = Infer [P] C" and
      infer: "ground_factoring P C"
    for P C
    unfolding ι_def
    using infer
    using ground_factoring_smaller_conclusion
    by simp

  ultimately show "ι ∈ G_Inf ⟹ concl_of ι ≺⇩c main_prem_of ι"
    unfolding G_Inf_def
    by fast
qed


subsection ‹Refutational Completeness›

context
  fixes N :: "'f gterm atom clause set"
begin

function production :: "'f gterm atom clause ⇒ 'f gterm set" where
  "production C = {A | A C'.
    C ∈ N ∧
    C = add_mset (Pos A) C' ∧
    select C = {#} ∧
    is_strictly_maximal_lit (Pos A) C ∧
    ¬ (⋃D ∈ {D ∈ N. D ≺⇩c C}. production D) ⊫ C}"
  by simp_all

termination production
proof (relation "{(x, y). x ≺⇩c y}")
  show "wf {(x, y). x ≺⇩c y}"
    using wfP_less_cls
    by (simp add: wfp_def)
next
  show "⋀C D. D ∈ {D ∈ N. D ≺⇩c C} ⟹ (D, C) ∈ {(x, y). x ≺⇩c y}"
    by simp
qed

declare production.simps[simp del]

end

lemma Uniq_striclty_maximal_lit_in_ground_cls:
  "∃⇩≤⇩1L. is_strictly_maximal_lit L C"
proof (rule Uniq_is_greatest_in_mset_wrt)
  show "transp_on (set_mset C) (≺⇩l)"
    by (auto intro: transp_on_subset transp_less_lit)
next
  show "asymp_on (set_mset C) (≺⇩l)"
    by (auto intro: asymp_on_subset asymp_less_lit)
next
  show "totalp_on (set_mset C) (≺⇩l)"
    by (auto intro: totalp_on_subset totalp_less_lit)
qed

lemma production_eq_empty_or_singleton:
  "production N C = {} ∨ (∃A. production N C = {A})"
proof -
  have "∃⇩≤⇩1A. is_strictly_maximal_lit (Pos A) C"
    using Uniq_striclty_maximal_lit_in_ground_cls
    by (metis (mono_tags, lifting) Uniq_def literal.inject(1))
  hence "∃⇩≤⇩1A. ∃C'. C = add_mset (Pos A) C' ∧ is_strictly_maximal_lit (Pos A) C"
    by (simp add: Uniq_def)
  hence Uniq_production: "∃⇩≤⇩1A. ∃C'.
    C ∈ N ∧
    C = add_mset (Pos A) C' ∧
    select C = {#} ∧
    is_strictly_maximal_lit (Pos A) C ∧
    ¬ (⋃D ∈ {D ∈ N. D ≺⇩c C}. production N D) ⊫ C"
    using Uniq_antimono'
    by (smt (verit) Uniq_def Uniq_prodI case_prod_conv)
  show ?thesis
    unfolding production.simps[of N C]
    using Collect_eq_if_Uniq[OF Uniq_production]
    by (smt (verit, best) Collect_cong Collect_empty_eq Uniq_def Uniq_production case_prod_conv
        insertCI mem_Collect_eq)
qed

lemma production_eq_singleton_if_atom_in_production:
  assumes "A ∈ production N C"
  shows "production N C = {A}"
  using assms production_eq_empty_or_singleton
  by force

definition interp where
  "interp N C ≡ (⋃D ∈ {D ∈ N. D ≺⇩c C}. production N D)"

lemma interp_mempty[simp]: "interp N {#} = {}"
proof -
  have "∄C. C ≺⇩c {#}"
    by (metis clause_order.order.asym subset_implies_multp subset_mset.gr_zeroI)
  hence "{D ∈ N. D ≺⇩c {#}} = {}"
    by simp
  thus ?thesis
    unfolding interp_def by auto
qed

lemma production_unfold: "production N C = {A | A C'.
    C ∈ N ∧
    C = add_mset (Pos A) C' ∧
    select C = {#} ∧
    is_strictly_maximal_lit (Pos A) C ∧
    ¬ interp N C ⊫ C}"
  by (simp add: production.simps[of N C] interp_def)

lemma production_unfold': "production N C = {A | A.
    C ∈ N ∧
    select C = {#} ∧
    is_strictly_maximal_lit (Pos A) C ∧
    ¬ interp N C ⊫ C}"
  unfolding production_unfold
  by (metis (mono_tags, lifting) literal_order.explode_greatest_in_mset)

lemma mem_productionE:
  assumes C_prod: "A ∈ production N C"
  obtains C' where
    "C ∈ N" and
    "C = add_mset (Pos A) C'" and
    "select C = {#}" and
    "is_strictly_maximal_lit (Pos A) C" and
    "¬ interp N C ⊫ C"
  using C_prod
  unfolding production.simps[of N C] mem_Collect_eq Let_def interp_def
  by (metis (no_types, lifting))

lemma production_subset_if_less_cls: "C ≺⇩c D ⟹ production N C ⊆ interp N D"
  unfolding interp_def
  using production_unfold by blast

lemma Uniq_production_eq_singleton: "∃⇩≤⇩1 C. production N C = {A}"
proof (rule Uniq_I)
  fix C D
  assume "production N C = {A}"
  hence "A ∈ production N C"
    by simp
  then obtain C' where
    "C ∈ N"
    "C = add_mset (Pos A) C'"
    "is_strictly_maximal_lit (Pos A) C"
    "¬ interp N C ⊫ C"
    by (auto elim!: mem_productionE)

  assume "production N D = {A}"
  hence "A ∈ production N D"
    by simp
  then obtain D' where
    "D ∈ N"
    "D = add_mset (Pos A) D'"
    "is_strictly_maximal_lit (Pos A) D"
    "¬ interp N D ⊫ D"
    by (auto elim!: mem_productionE)

  have "¬ (C ≺⇩c D)"
  proof (rule notI)
    assume "C ≺⇩c D"
    hence "production N C ⊆ interp N D"
      using production_subset_if_less_cls by metis
    hence "A ∈ interp N D"
      unfolding ‹production N C = {A}› by simp
    hence "interp N D ⊫ D"
      unfolding ‹D = add_mset (Pos A) D'› by simp
    with ‹¬ interp N D ⊫ D› show False
      by metis
  qed

  moreover have "¬ (D ≺⇩c C)"
  proof (rule notI)
    assume "D ≺⇩c C"
    hence "production N D ⊆ interp N C"
      using production_subset_if_less_cls by metis
    hence "A ∈ interp N C"
      unfolding ‹production N D = {A}› by simp
    hence "interp N C ⊫ C"
      unfolding ‹C = add_mset (Pos A) C'› by simp
    with ‹¬ interp N C ⊫ C› show False
      by metis
  qed

  ultimately show "C = D"
    by order
qed

lemma singleton_eq_CollectD: "{x} = {y. P y} ⟹ P x"
  by blast

lemma subset_Union_mem_CollectI: "P x ⟹ f x ⊆ (⋃y ∈ {z. P z}. f y)"
  by blast

lemma interp_subset_if_less_cls: "C ≺⇩c D ⟹ interp N C ⊆ interp N D"
  by (smt (verit, best) UN_iff mem_Collect_eq interp_def subsetI transpD transp_less_cls)

lemma interp_subset_if_less_cls': "C ≺⇩c D ⟹ interp N C ⊆ interp N D ∪ production N D"
  using interp_subset_if_less_cls by blast

lemma split_Union_production:
  assumes D_in: "D ∈ N"
  shows "(⋃C ∈ N. production N C) =
    interp N D ∪ production N D ∪ (⋃C ∈ {C ∈ N. D ≺⇩c C}. production N C)"
proof -
  have "N = {C ∈ N. C ≺⇩c D} ∪ {D} ∪ {C ∈ N. D ≺⇩c C}"
  proof (rule partition_set_around_element)
    show "totalp_on N (≺⇩c)"
      using totalp_less_cls totalp_on_subset by blast
  next
    show "D ∈ N"
      using D_in by simp
  qed
  hence "(⋃C ∈ N. production N C) =
      (⋃C ∈ {C ∈ N. C ≺⇩c D}. production N C) ∪ production N D ∪ (⋃C ∈ {C ∈ N. D ≺⇩c C}. production N C)"
    by auto
  thus "(⋃C ∈ N. production N C) =
    interp N D ∪ production N D ∪ (⋃C ∈ {C ∈ N. D ≺⇩c C}. production N C)"
    by (simp add: interp_def)
qed

lemma split_Union_production':
  assumes D_in: "D ∈ N"
  shows "(⋃C ∈ N. production N C) = interp N D ∪ (⋃C ∈ {C ∈ N. D ≼⇩c C}. production N C)"
  using split_Union_production[OF D_in] D_in by auto

lemma split_interp:
  assumes "C ∈ N" and D_in: "D ∈ N" and "D ≺⇩c C"
  shows "interp N C = interp N D ∪ (⋃C' ∈ {C' ∈ N. D ≼⇩c C' ∧ C' ≺⇩c C}. production N C')"
proof -
  have "{D ∈ N. D ≺⇩c C} =
        {y ∈ {D ∈ N. D ≺⇩c C}. y ≺⇩c D} ∪ {D} ∪ {y ∈ {D ∈ N. D ≺⇩c C}. D ≺⇩c y}"
  proof (rule partition_set_around_element)
    show "totalp_on {D ∈ N. D ≺⇩c C} (≺⇩c)"
      using totalp_less_cls totalp_on_subset by blast
  next
    from D_in ‹D ≺⇩c C› show "D ∈ {D ∈ N. D ≺⇩c C}"
      by simp
  qed
  also have "… = {x ∈ N. x ≺⇩c C ∧ x ≺⇩c D} ∪ {D} ∪ {x ∈ N. D ≺⇩c x ∧ x ≺⇩c C}"
    by auto
  also have "… = {x ∈ N. x ≺⇩c D} ∪ {D} ∪ {x ∈ N. D ≺⇩c x ∧ x ≺⇩c C}"
    using ‹D ≺⇩c C› transp_less_cls
    by (metis (no_types, opaque_lifting) transpD)
  finally have Collect_N_lt_C: "{x ∈ N. x ≺⇩c C} = {x ∈ N. x ≺⇩c D} ∪ {x ∈ N. D ≼⇩c x ∧ x ≺⇩c C}"
    by auto

  have "interp N C = (⋃C' ∈ {D ∈ N. D ≺⇩c C}. production N C')"
    by (simp add: interp_def)
  also have "… = (⋃C' ∈ {x ∈ N. x ≺⇩c D}. production N C') ∪ (⋃C' ∈ {x ∈ N. D ≼⇩c x ∧ x ≺⇩c C}. production N C')"
    unfolding Collect_N_lt_C by simp
  finally show "interp N C = interp N D ∪ ⋃ (production N ` {C' ∈ N. D ≼⇩c C' ∧ C' ≺⇩c C})"
    unfolding interp_def by simp
qed

lemma less_imp_Interp_subseteq_interp: "C ≺⇩c D ⟹ interp N C ∪ production N C ⊆ interp N D"
  using interp_subset_if_less_cls production_subset_if_less_cls
  by (simp add: interp_def)

lemma not_interp_to_Interp_imp_le: "A ∉ interp N C ⟹ A ∈ interp N D ∪ production N D ⟹ C ≼⇩c D"
  using less_imp_Interp_subseteq_interp
  by (metis (mono_tags, opaque_lifting) subsetD sup2CI totalpD totalp_less_cls)

lemma produces_imp_in_interp:
  assumes "Neg A ∈# C" and D_prod: "A ∈ production N D"
  shows "A ∈ interp N C"
proof -
  from D_prod have "Pos A ∈# D" and "is_strictly_maximal_lit (Pos A) D"
    by (auto elim: mem_productionE)

  have "D ≺⇩c C"
  proof (rule multp_if_maximal_of_lhs_is_less)
    show "Pos A ∈# D"
      using ‹Pos A ∈# D› .
  next
    show "Neg A ∈# C"
      using ‹Neg A ∈# C› .
  next
    show "Pos A ≺⇩l Neg A"
      by (simp add: less_lit_def subset_implies_multp)
  next
    show "is_maximal_lit (Pos A) D"
      using ‹is_strictly_maximal_lit (Pos A) D› by auto
  qed simp_all
  hence "¬ (≺⇩c)⇧=⇧= C D"
    by (metis asympD asymp_less_cls reflclp_iff)
  thus ?thesis
  proof (rule contrapos_np)
    from D_prod show  "A ∉ interp N C ⟹ (≺⇩c)⇧=⇧= C D"
      using not_interp_to_Interp_imp_le by simp
  qed
qed

lemma neg_notin_Interp_not_produce:
  "Neg A ∈# C ⟹ A ∉ interp N D ∪ production N D ⟹ C ≼⇩c D ⟹ A ∉ production N D''"
  using interp_subset_if_less_cls'
  by (metis Un_iff produces_imp_in_interp reflclp_iff sup.orderE)

lemma lift_interp_entails:
  assumes
    D_in: "D ∈ N" and
    D_entailed: "interp N D ⊫ D" and
    C_in: "C ∈ N" and
    D_lt_C: "D ≺⇩c C"
  shows "interp N C ⊫ D"
proof -
  from D_entailed obtain L A where
    L_in: "L ∈# D" and
    L_eq_disj_L_eq: "L = Pos A ∧ A ∈ interp N D ∨ L = Neg A ∧ A ∉ interp N D"
    unfolding true_cls_def true_lit_iff by metis

  have "interp N D ⊆ interp N C"
    using interp_subset_if_less_cls[OF D_lt_C] .

  from L_eq_disj_L_eq show "interp N C ⊫ D"
  proof (elim disjE conjE)
    assume "L = Pos A" and "A ∈ interp N D"
    thus "interp N C ⊫ D"
      using L_in ‹interp N D ⊆ interp N C› by auto
  next
    assume "L = Neg A" and "A ∉ interp N D"
    hence "A ∉ interp N C"
      using neg_notin_Interp_not_produce
      by (smt (verit, ccfv_threshold) L_in UN_E interp_def produces_imp_in_interp)
    thus "interp N C ⊫ D"
      using L_in ‹L = Neg A› by blast
  qed
qed

lemma lift_interp_entails_to_interp_production_entails:
  assumes
    C_in: "C ∈ N" and
    D_in: "D ∈ N" and
    C_lt_D: "D ≺⇩c C" and
    D_entailed: "interp N C ⊫ D"
  shows "interp N C ∪ production N C ⊫ D"
proof -
  from D_entailed obtain L A where
    L_in: "L ∈# D" and
    L_eq_disj_L_eq: "L = Pos A ∧ A ∈ interp N C ∨ L = Neg A ∧ A ∉ interp N C"
    unfolding true_cls_def true_lit_iff by metis

  from L_eq_disj_L_eq show "interp N C ∪ production N C ⊫ D"
  proof (elim disjE conjE)
    assume "L = Pos A" and "A ∈ interp N C"
    thus "interp N C ∪ production N C ⊫ D"
      using L_in by blast
  next
    assume "L = Neg A" and "A ∉ interp N C"
    hence "A ∉ interp N C ∪ production N C"
      using neg_notin_Interp_not_produce
      by (metis (no_types, opaque_lifting) C_lt_D L_in Un_iff interp_subset_if_less_cls
          produces_imp_in_interp subsetD)
    thus "interp N C ∪ production N C ⊫ D"
      using L_in ‹L = Neg A› by blast
  qed
qed

lemma lift_entailment_to_Union:
  fixes N D
  assumes
    D_in: "D ∈ N" and
    R⇩D_entails_D: "interp N D ⊫ D"
  shows
    "(⋃C ∈ N. production N C) ⊫ D"
  using lift_interp_entails
  by (smt (verit, best) D_in R⇩D_entails_D UN_iff produces_imp_in_interp split_Union_production'
      subsetD sup_ge1 true_cls_def true_lit_iff)


lemma
  assumes
    "D ≼⇩c C" and
    C_prod: "A ∈ production N C" and
    L_in: "L ∈# D"
  shows
    lesseq_trm_if_pos: "is_pos L ⟹ atm_of L ≼⇩t A" and
    less_trm_if_neg: "is_neg L ⟹ atm_of L ≺⇩t A"
proof -
  from C_prod obtain C' where
    C_def: "C = add_mset (Pos A) C'" and
    C_max_lit: "is_strictly_maximal_lit (Pos A) C"
    by (auto elim: mem_productionE)

  have "Pos A ≺⇩l L" if "is_pos L" and "¬ atm_of L ≼⇩t A"
  proof -
    from that(2) have "A ≺⇩t atm_of L"
      using totalp_less_trm[THEN totalpD] by auto
    hence "multp (≺⇩t) {#A#} {#atm_of L#}"
      by (smt (verit, del_insts) add.right_neutral empty_iff insert_iff one_step_implies_multp
          set_mset_add_mset_insert set_mset_empty transpD transp_less_trm union_mset_add_mset_right)
    with that(1) show "Pos A ≺⇩l L"
      by (cases L) (simp_all add: less_lit_def)
  qed

  moreover have "Pos A ≺⇩l L" if "is_neg L" and "¬ atm_of L ≺⇩t A"
  proof -
    from that(2) have "A ≼⇩t atm_of L"
      using totalp_less_trm[THEN totalpD] by auto
    hence "multp (≺⇩t) {#A#} {#atm_of L, atm_of L#}"
      by (smt (z3) add_mset_add_single add_mset_remove_trivial add_mset_remove_trivial_iff
          empty_not_add_mset insert_DiffM insert_noteq_member one_step_implies_multp reflclp_iff
          transp_def transp_less_trm union_mset_add_mset_left union_mset_add_mset_right)
    with that(1) show "Pos A ≺⇩l L"
      by (cases L) (simp_all add: less_lit_def)
  qed

  moreover have False if "Pos A ≺⇩l L"
  proof -
    have "C ≺⇩c D"
    proof (rule multp_if_maximal_of_lhs_is_less)
      show "Pos A ∈# C"
        by (simp add: C_def)
    next
      show "L ∈# D"
        using L_in by simp
    next
      show "is_maximal_lit (Pos A) C"
        using C_max_lit by auto
    next
      show "Pos A ≺⇩l L"
        using that by simp
    qed simp_all
    with ‹D ≼⇩c C› show False
      by (metis asympD reflclp_iff wfp_imp_asymp wfP_less_cls)
  qed

  ultimately show "is_pos L ⟹ atm_of L ≼⇩t A" and "is_neg L ⟹ atm_of L ≺⇩t A"
    by metis+
qed

lemma less_trm_iff_less_cls_if_mem_production:
  assumes C_prod: "A⇩C ∈ production N C" and D_prod: "A⇩D ∈ production N D"
  shows "A⇩C ≺⇩t A⇩D ⟷ C ≺⇩c D"
proof -
  from C_prod obtain C' where
    "C ∈ N" and
    C_def: "C = add_mset (Pos A⇩C) C'" and
    "is_strictly_maximal_lit (Pos A⇩C) C"
    by (elim mem_productionE) simp
  hence "∀L ∈# C'. L ≺⇩l Pos A⇩C"
    by (simp add: literal_order.is_greatest_in_mset_iff)

  from D_prod obtain D' where
    "D ∈ N" and
    D_def: "D = add_mset (Pos A⇩D) D'" and
    "is_strictly_maximal_lit (Pos A⇩D) D"
    by (elim mem_productionE) simp
  hence "∀L ∈# D'. L ≺⇩l Pos A⇩D"
    by (simp add: literal_order.is_greatest_in_mset_iff)

  show ?thesis
  proof (rule iffI)
    assume "A⇩C ≺⇩t A⇩D"
    hence "Pos A⇩C ≺⇩l Pos A⇩D"
      by (simp add: less_lit_def)
    moreover hence "∀L ∈# C'. L ≺⇩l Pos A⇩D"
      using ‹∀L ∈# C'. L ≺⇩l Pos A⇩C›
      by (meson transp_less_lit transpD)
    ultimately show "C ≺⇩c D"
      using one_step_implies_multp[of D C _ "{#}"]
      by (simp add: D_def C_def)
  next
    assume "C ≺⇩c D"
    hence "production N C ⊆ (⋃ (production N ` {x ∈ N. x ≺⇩c D}))"
      using ‹C ∈ N› by auto
    hence "A⇩C ∈ (⋃ (production N ` {x ∈ N. x ≺⇩c D}))"
      using C_prod by auto
    hence "A⇩C ≠ A⇩D"
      by (metis D_prod interp_def mem_productionE true_cls_add_mset true_lit_iff)
    moreover have "¬ (A⇩D ≺⇩t A⇩C)"
      by (metis C_def D_prod ‹C ≺⇩c D› asympD asymp_less_trm lesseq_trm_if_pos literal.disc(1)
          literal.sel(1) reflclp_iff union_single_eq_member)
    ultimately show "A⇩C ≺⇩t A⇩D"
      using totalp_less_trm[THEN totalpD]
      using C_def D_def by auto
  qed
qed

lemma false_cls_if_productive_production:
  assumes C_prod: "A ∈ production N C" and "D ∈ N" and "C ≺⇩c D"
  shows "¬ interp N D ⊫ C - {#Pos A#}"
proof -
  from C_prod obtain C' where
    C_in: "C ∈ N" and
    C_def: "C = add_mset (Pos A) C'" and
    "select C = {#}" and
    Pox_A_max: "is_strictly_maximal_lit (Pos A) C" and
    "¬ interp N C ⊫ C"
    by (rule mem_productionE) blast

  from ‹D ∈ N› ‹C ≺⇩c D› have "A ∈ interp N D"
    using C_prod production_subset_if_less_cls by auto

  from ‹D ∈ N› have "interp N D ⊆ (⋃D ∈ N. production N D)"
    by (auto simp: interp_def)

  have "¬ interp N D ⊫ C'"
    unfolding true_cls_def Set.bex_simps
  proof (intro ballI)
    fix L assume L_in: "L ∈# C'"
    hence "L ∈# C"
      by (simp add: C_def)

    have "C' ≺⇩c C"
      by (simp add: C_def subset_implies_multp)
    hence "C' ≼⇩c C"
      by order

    show "¬ interp N D ⊫l L"
    proof (cases L)
      case (Pos A⇩L)
      moreover have "A⇩L ∉ interp N D"
      proof -
        have "∀y∈#C'. y ≺⇩l Pos A"
          using Pox_A_max
          by (simp add: C_def literal_order.is_greatest_in_mset_iff)
        with Pos have "A⇩L ∉ insert A (interp N C)"
          using L_in ‹¬ interp N C ⊫ C› C_def
          by blast

        moreover have "A⇩L ∉ (⋃D' ∈ {D' ∈ N. C ≺⇩c D' ∧ D' ≺⇩c D}. production N D')"
        proof -
          have "A⇩L ≼⇩t A"
            using Pos lesseq_trm_if_pos[OF ‹C' ≼⇩c C› C_prod ‹L ∈# C'›]
            by simp
          thus ?thesis
            using less_trm_iff_less_cls_if_mem_production
            using C_prod calculation interp_def by fastforce
        qed

        moreover have "interp N D =
          insert A (interp N C) ∪ (⋃D' ∈ {D' ∈ N. C ≺⇩c D' ∧ D' ≺⇩c D}. production N D')"
        proof -
          have "interp N D = (⋃D' ∈ {D' ∈ N. D' ≺⇩c D}. production N D')"
            by (simp only: interp_def)
          also have "… = (⋃D' ∈ {D' ∈ {y ∈ N. y ≺⇩c C} ∪ {C} ∪ {y ∈ N. C ≺⇩c y}. D' ≺⇩c D}. production N D')"
            using partition_set_around_element[of N "(≺⇩c)", OF _ ‹C ∈ N›]
              totalp_on_subset[OF totalp_less_cls, simplified]
            by simp
          also have "… = (⋃D' ∈ {y ∈ N. y ≺⇩c C ∧ y ≺⇩c D} ∪ {C} ∪ {y ∈ N. C ≺⇩c y ∧ y ≺⇩c D}. production N D')"
            using ‹C ≺⇩c D› by auto
          also have "… = (⋃D' ∈ {y ∈ N. y ≺⇩c C} ∪ {C} ∪ {y ∈ N. C ≺⇩c y ∧ y ≺⇩c D}. production N D')"
            by (metis (no_types, opaque_lifting) assms(3) transpD transp_less_cls)
          also have "… = interp N C ∪ production N C ∪ (⋃D' ∈ {y ∈ N. C ≺⇩c y ∧ y ≺⇩c D}. production N D')"
            by (auto simp: interp_def)
          finally show ?thesis
            using C_prod
            by (metis (no_types, lifting) empty_iff insertE insert_is_Un
                production_eq_empty_or_singleton sup_commute)
        qed

        ultimately show ?thesis
          by simp
      qed
      ultimately show ?thesis
        by simp
    next
      case (Neg A⇩L)
      moreover have "A⇩L ∈ interp N D"
        using Neg ‹L ∈# C› ‹C ≺⇩c D› ‹¬ interp N C ⊫ C› interp_subset_if_less_cls
        by blast
      ultimately show ?thesis
        by simp
    qed
  qed
  thus "¬ interp N D ⊫ C - {#Pos A#}"
    by (simp add: C_def)
qed

lemma production_subset_Union_production:
  "⋀C N. C ∈ N ⟹ production N C ⊆ (⋃D ∈ N. production N D)"
  by auto

lemma interp_subset_Union_production:
  "⋀C N. C ∈ N ⟹ interp N C ⊆ (⋃D ∈ N. production N D)"
  by (simp add: split_Union_production')

lemma model_construction:
  fixes
    N :: "'f gterm atom clause set" and
    C :: "'f gterm atom clause"
  assumes "G.saturated N" and "{#} ∉ N" and C_in: "C ∈ N"
  shows
    "production N C = {} ⟷ interp N C ⊫ C"
    "(⋃D ∈ N. production N D) ⊫ C"
    "D ∈ N ⟹ C ≺⇩c D ⟹ interp N D ⊫ C"
  unfolding atomize_conj atomize_imp
  using wfP_less_cls C_in
proof (induction C arbitrary: D rule: wfp_induct_rule)
  case (less C)
  note IH = less.IH

  from ‹{#} ∉ N› ‹C ∈ N› have "C ≠ {#}"
    by metis

  define I :: "'f gterm set" where
    "I = interp N C"

  have i: "interp N C ⊫ C ⟷ (production N C = {})"
  proof (rule iffI)
    show "interp N C ⊫ C ⟹ production N C = {}"
      by (smt (z3) Collect_empty_eq interp_def production.elims)
  next
    assume "production N C = {}"
    show "interp N C ⊫ C"
    proof (cases "∃A. Neg A ∈# C ∧ (Neg A ∈# select C ∨ select C = {#} ∧ is_maximal_lit (Neg A) C)")
      case ex_neg_lit_sel_or_max: True
      then obtain A where
        "Neg A ∈# C" and
        sel_or_max: "Neg A ∈# select C ∨ select C = {#} ∧ is_maximal_lit (Neg A) C"
        by metis
      then obtain C' where
        C_def: "C = add_mset (Neg A) C'"
        by (metis mset_add)

      show ?thesis
      proof (cases "A ∈ interp N C")
        case True
        then obtain D where
          "A ∈ production N D" and "D ∈ N" and "D ≺⇩c C"
          unfolding interp_def by auto
        then obtain D' where
          D_def: "D = add_mset (Pos A) D'" and
          sel_D: "select D = {#}" and
          max_t_t': "is_strictly_maximal_lit (Pos A) D" and
          "¬ interp N D ⊫ D"
          by (elim mem_productionE) fast

        have reso: "ground_resolution C D (C' + D')"
        proof (rule ground_resolutionI)
          show "C = add_mset (Neg A) C'"
            by (simp add: C_def)
        next
          show "D = add_mset (Pos A) D'"
            by (simp add: D_def)
        next
          show "D ≺⇩c C"
            using ‹D ≺⇩c C› .
        next
          show "select C = {#} ∧ is_maximal_lit (Neg A) C ∨ Neg A ∈# select C"
            using sel_or_max by auto
        next
          show "select D = {#}"
            using sel_D by blast
        next
          show "is_strictly_maximal_lit (Pos A) D"
            using max_t_t' .
        qed simp_all

        define ι :: "'f gterm clause inference" where
          "ι = Infer [D, C] (C' + D')"

        have "ι ∈ G_Inf"
          using reso
          by (auto simp only: ι_def G_Inf_def)

        moreover have "⋀t. t ∈ set (prems_of ι) ⟹ t ∈ N"
          using ‹C ∈ N› ‹D ∈ N›
          by (auto simp add: ι_def)

        ultimately have "ι ∈ G.Inf_from N"
          by (auto simp: G.Inf_from_def)
        hence "ι ∈ G.Red_I N"
          using ‹G.saturated N›
          by (auto simp: G.saturated_def)
        then obtain DD where
          DD_subset: "DD ⊆ N" and
          "finite DD" and
          DD_entails_CD: "G_entails (insert D DD) {C' + D'}" and
          ball_DD_lt_C: "∀D∈DD. D ≺⇩c C"
          unfolding G.Red_I_def G.redundant_infer_def mem_Collect_eq
          by (auto simp: ι_def)

        moreover have "∀D∈ insert D DD. interp N C ⊫ D"
          using IH[THEN conjunct2, THEN conjunct2, rule_format, of _ C]
          using ‹C ∈ N› ‹D ∈ N› ‹D ≺⇩c C› DD_subset ball_DD_lt_C
          by (metis in_mono insert_iff)

        ultimately have "interp N C ⊫ C' + D'"
          using DD_entails_CD
          unfolding G_entails_def
          by (simp add: I_def true_clss_def)

        moreover have "¬ interp N D ⊫ D'"
          using ‹¬ interp N D ⊫ D›
          using D_def by force

        moreover have "D' ≺⇩c D"
          unfolding D_def
          by (simp add: subset_implies_multp)

        moreover have "¬ interp N C ⊫ D'"
          using false_cls_if_productive_production[OF _ ‹C ∈ N› ‹D ≺⇩c C›]
          by (metis D_def ‹A ∈ production N D› remove1_mset_add_mset_If)

        ultimately show "interp N C ⊫ C"
          unfolding C_def by fast
      next
        case False
        thus ?thesis
          using ‹Neg A ∈# C›
          by (auto simp add: true_cls_def)
      qed
    next
      case False
      hence "select C = {#}"
        using select_subset select_negative_lits
        by (metis (no_types, opaque_lifting) Neg_atm_of_iff mset_subset_eqD multiset_nonemptyE)
        
      from False obtain A where Pos_A_in: "Pos A ∈# C" and max_Pos_A: "is_maximal_lit (Pos A) C"
        using ex_maximal_in_mset_wrt[OF transp_on_less_lit asymp_on_less_lit ‹C ≠ {#}›]
        using is_maximal_in_mset_wrt_iff[OF transp_on_less_lit asymp_on_less_lit]
        by (metis Neg_atm_of_iff ‹select C = {#}› is_pos_def)
      then obtain C' where C_def: "C = add_mset (Pos A) C'"
        by (meson mset_add)

      show ?thesis
      proof (cases "interp N C ⊫ C'")
        case True
        then show ?thesis
          using C_def by force
      next
        case False
        show ?thesis
        proof (cases "is_strictly_maximal_lit (Pos A) C")
          case strictly_maximal: True
          then show ?thesis
            using ‹production N C = {}› ‹select C = {#}› less.prems
            unfolding production_unfold[of N C] Collect_empty_eq
            using C_def by blast
        next
          case False
          hence "count C (Pos A) ≥ 2"
            using max_Pos_A
            by (simp add: literal_order.count_ge_2_if_maximal_in_mset_and_not_greatest_in_mset)
          then obtain C' where C_def: "C = add_mset (Pos A) (add_mset (Pos A) C')"
            by (metis two_le_countE)

          define ι :: "'f gterm clause inference" where
            "ι = Infer [C] (add_mset (Pos A) C')"

          have eq_fact: "ground_factoring C (add_mset (Pos A) C')"
          proof (rule ground_factoringI)
            show "C = add_mset (Pos A) (add_mset (Pos A) C')"
              by (simp add: C_def)
          next
            show "select C = {#}"
              using ‹select C = {#}› .
          next
            show "is_maximal_lit (Pos A) C"
              using max_Pos_A .
          qed simp_all
          hence "ι ∈ G_Inf"
            by (auto simp: ι_def G_Inf_def)

          moreover have "⋀t. t ∈ set (prems_of ι) ⟹ t ∈ N"
            using ‹C ∈ N›
            by (auto simp add: ι_def)

          ultimately have "ι ∈ G.Inf_from N"
            by (auto simp: G.Inf_from_def)
          hence "ι ∈ G.Red_I N"
            using ‹G.saturated N›
            by (auto simp: G.saturated_def)
          then obtain DD where
            DD_subset: "DD ⊆ N" and
            "finite DD" and
            DD_entails_concl: "G_entails DD {add_mset (Pos A) C'}" and
            ball_DD_lt_C: "∀D∈DD. D ≺⇩c C"
            unfolding G.Red_I_def G.redundant_infer_def mem_Collect_eq
            by (auto simp: ι_def)

          moreover have "∀D∈DD. interp N C ⊫ D"
            using IH[THEN conjunct2, THEN conjunct2, rule_format, of _ C]
            using ‹C ∈ N› DD_subset ball_DD_lt_C
            by blast

          ultimately have "interp N C ⊫ add_mset (Pos A) C'"
            using DD_entails_concl
            unfolding G_entails_def
            by (simp add: I_def true_clss_def)
          then show ?thesis
            by (simp add: C_def joinI_right pair_imageI)
        qed
      qed
    qed
  qed

  moreover have iia: "(⋃ (production N ` N)) ⊫ C"
    using production_eq_empty_or_singleton[of N C]
  proof (elim disjE exE)
    assume "production N C = {}"
    hence "interp N C ⊫ C"
      by (simp only: i)
    thus ?thesis
      using lift_entailment_to_Union[OF ‹C ∈ N›] by argo
  next
    fix A
    assume "production N C = {A}"
    hence prod: "A ∈ production N C"
      by simp

    from prod have "Pos A ∈# C"
      unfolding production.simps[of N C] mem_Collect_eq
      by force

    moreover from prod have "A ∈ ⋃ (production N ` N)"
      using ‹C ∈ N› production_subset_Union_production
      by fast
    
    ultimately show ?thesis
      by blast
  qed

  moreover have iib: "interp N D ⊫ C" if "D ∈ N" and "C ≺⇩c D"
    using production_eq_empty_or_singleton[of N C, folded ]
  proof (elim disjE exE)
    assume "production N C = {}"
    hence "interp N C ⊫ C"
      unfolding i by simp
    thus ?thesis
      using lift_interp_entails[OF ‹C ∈ N› _ that] by argo
  next
    fix A assume "production N C = {A}"
    thus ?thesis
      by (metis Un_insert_right insertCI insert_subset less_imp_Interp_subseteq_interp
          mem_productionE pos_literal_in_imp_true_cls that(2) union_single_eq_member)
  qed

  ultimately show ?case
    by argo
qed

lemma
  assumes "clause_order.is_least_in_fset N C" and "A ∈ production (fset N) C"
  shows "⋀A'. A' ≺⇩t A ⟹ A' ∉ (⋃D ∈ fset N. production (fset N) D)"
  using assms less_trm_iff_less_cls_if_mem_production clause_order.is_least_in_fset_iff by auto

lemma lesser_atoms_not_in_previous_interp_are_not_in_final_interp_if_productive:
  assumes "A ∈ production (fset N) C"
  shows "⋀A'. A' ≺⇩t A ⟹ A' ∉ interp (fset N) C ⟹ A' ∉ (⋃D ∈ fset N. production (fset N) D)"
  using assms production_subset_if_less_cls less_trm_iff_less_cls_if_mem_production by fastforce

lemma lesser_atoms_not_in_previous_interp_are_not_in_final_interp_if_not_productive:
  assumes "literal_order.is_maximal_in_mset C L" and "production (fset N) C = {}"
  shows "⋀A'. A' ≺⇩t atm_of L ⟹ A' ∉ interp (fset N) C ⟹ A' ∉ (⋃D ∈ fset N. production (fset N) D)"
  using assms
  by (metis (no_types, lifting) UN_E UnCI less_trm_if_neg lesseq_trm_if_pos
      literal_order.is_maximal_in_mset_iff term_order.less_imp_not_less term_order.not_le
      not_interp_to_Interp_imp_le)

lemma lesser_atoms_not_in_previous_interp_are_not_in_final_interp:
  fixes A
  assumes
    L_max: "literal_order.is_maximal_in_mset C L" and
    A_less: "A ≺⇩t atm_of L" and
    A_no_in: "A ∉ interp (fset N) C"
  shows "A ∉ (⋃D ∈ fset N. production (fset N) D)"
proof (cases "production (fset N) C = {}")
  case True
  thus ?thesis
    using L_max A_less A_no_in
    using lesser_atoms_not_in_previous_interp_are_not_in_final_interp_if_not_productive
    by metis
next
  case False
  then obtain A' where C_produces_A': "A' ∈ production (fset N) C"
    by auto
  hence "is_strictly_maximal_lit (Pos A') C"
    unfolding production_unfold mem_Collect_eq by metis
  hence "literal_order.is_maximal_in_mset C (Pos A')"
    using literal_order.is_maximal_in_mset_if_is_greatest_in_mset by metis
  hence "L = Pos A'"
    using L_max
    by (metis Uniq_D literal_order.Uniq_is_maximal_in_mset)
  hence "atm_of L ∈ production (fset N) C"
    using C_produces_A' by simp
  thus ?thesis
    using L_max A_less A_no_in
    using lesser_atoms_not_in_previous_interp_are_not_in_final_interp_if_productive
    by metis
qed

lemma lesser_atoms_in_previous_interp_are_in_final_interp:
  fixes A
  assumes
    L_max: "literal_order.is_maximal_in_mset C L" and
    A_less: "A ≺⇩t atm_of L" and
    A_in: "A ∈ interp N C"
  shows "A ∈ (⋃D ∈ N. production N D)"
  using A_in interp_def by fastforce

lemma interp_fixed_for_smaller_literals:
  fixes A
  assumes
    L_max: "literal_order.is_maximal_in_mset C L" and
    A_less: "A ≺⇩t atm_of L" and
    "C ≺⇩c D"
  shows "A ∈ interp N C ⟷ A ∈ interp N D"
proof (rule iffI)
  show "A ∈ interp N C ⟹ A ∈ interp N D"
    using assms(3) interp_subset_if_less_cls by auto
next
  assume "A ∈ interp N D"

  then obtain E where "A ∈ production N E" and "E ∈ N" and "E ≺⇩c D"
    unfolding interp_def by auto

  hence "literal_order.is_greatest_in_mset E (Pos A)"
    by (auto elim: mem_productionE)

  moreover have "Pos A ≺⇩l L"
    by (metis A_less Neg_atm_of_iff less_lit_simps(1) less_lit_simps(2)
        literal_order.dual_order.strict_trans term_order.order_eq_iff literal.collapse(1))

  ultimately have "E ≺⇩c C"
    using L_max
    using literal_order.multp⇩H⇩O_if_maximal_less_that_maximal multp⇩D⇩M_imp_multp multp⇩H⇩O_imp_multp⇩D⇩M
    by blast

  hence "production N E ⊆ interp N C"
    by (simp add: production_subset_if_less_cls)

  thus "A ∈ interp N C"
    using ‹A ∈ production N E› by auto
qed

lemma neg_lits_not_in_model_stay_out_of_model:
  assumes
    L_in: "L ∈# C" and
    L_neg: "is_neg L" and
    atm_L_not_in: "atm_of L ∉ interp N C"
  shows "atm_of L ∉ (⋃D ∈ N. production N D)"
  using assms produces_imp_in_interp by force

lemma neg_lits_already_in_model_stay_in_model:
  assumes
    L_in: "L ∈# C" and
    L_neg: "is_neg L" and
    atm_L_not_in: "atm_of L ∈ interp N C"
  shows "atm_of L ∈ (⋃D ∈ N. production N D)"
  using atm_L_not_in interp_def by auto

lemma image_eq_imageI:
  assumes "⋀x. x ∈ X ⟹ f x = g x"
  shows "f ` X = g ` X"
  using assms by auto

lemma production_swap_clause_set:
  assumes
    agree: "{D ∈ N1. D ≼⇩c C} = {D ∈ N2. D ≼⇩c C}"
  shows "production N1 C = production N2 C"
  using agree
proof (induction C rule: wfp_induct_rule[OF wfP_less_cls])
  case hyps: (1 C)
  from hyps have AAA: "C ∈ N1 ⟷ C ∈ N2"
    by auto

  from hyps have "{D ∈ N1. D ≺⇩c C} = {D ∈ N2. D ≺⇩c C}"
    by blast

  have "production N1 ` {D ∈ N2. D ≺⇩c C} = production N2 ` {D ∈ N2. D ≺⇩c C}"
  proof (rule image_eq_imageI)
    fix x assume "x ∈ {D ∈ N2. D ≺⇩c C}"
    hence "x ∈ N2" and "x ≺⇩c C"
      by simp_all
    moreover have "{D ∈ N1. (≺⇩c)⇧=⇧= D x} = {D ∈ N2. (≺⇩c)⇧=⇧= D x}"
      using hyps.prems ‹x ≺⇩c C› clause_order.order.strict_trans1 by blast
    ultimately show "production N1 x = production N2 x"
      using hyps.IH[rule_format, of x] by metis
  qed
  hence BBB: "interp N1 C = interp N2 C"
    unfolding interp_def ‹{D ∈ N1. D ≺⇩c C} = {D ∈ N2. D ≺⇩c C}›
    by argo

  show ?case
    unfolding production_unfold
    unfolding AAA BBB
    by simp
qed

lemma interp_swap_clause_set:
  assumes agree: "{D ∈ N1. D ≺⇩c C} = {D ∈ N2. D ≺⇩c C}"
  shows "interp N1 C = interp N2 C"
proof -
  have BBB: "production N1 ` {D ∈ N2. D ≺⇩c C} = production N2 ` {D ∈ N2. D ≺⇩c C}"
  proof (intro image_eq_imageI production_swap_clause_set)
    fix x
    assume "x ∈ {D ∈ N2. D ≺⇩c C}"
    thus "{D ∈ N1. (≺⇩c)⇧=⇧= D x} = {D ∈ N2. (≺⇩c)⇧=⇧= D x}"
      using agree clause_order.le_less_trans by blast
  qed

  show ?thesis
    unfolding interp_def
    unfolding agree BBB
    by argo
qed

definition interp' where
  "interp' N ≡ (⋃C ∈ N. production N C)"

lemma interp_eq_interp': "interp N D = interp' {C ∈ N. C ≺⇩c D}"
proof -
  have "interp N D = interp {C ∈ N. C ≺⇩c D} D"
  proof (rule interp_swap_clause_set)
    show "{Da ∈ N. Da ≺⇩c D} = {Da ∈ {C ∈ N. C ≺⇩c D}. Da ≺⇩c D}"
      by blast
  qed

  also have "… = interp' {C ∈ N. C ≺⇩c D}"
    unfolding interp_def interp'_def by blast

  finally show ?thesis .
qed

lemma production_unfold'': "production N C = {A | A.
    C ∈ N ∧ select C = {#} ∧
    is_strictly_maximal_lit (Pos A) C ∧
    ¬ interp' {B ∈ N. B ≺⇩c C} ⊫ C}"
  unfolding production_unfold interp_eq_interp'
  using literal_order.explode_greatest_in_mset
  by metis

lemma Interp_swap_clause_set:
  assumes agree: "{D ∈ N1. D ≼⇩c C} = {D ∈ N2. D ≼⇩c C}"
  shows "interp N1 C ∪ production N1 C = interp N2 C ∪ production N2 C"
  using production_swap_clause_set[OF agree]
  using interp_swap_clause_set
  using agree
  by blast

lemma production_insert_greater_clause:
  assumes "C ≺⇩c D"
  shows "production (insert D N) C = production N C"
proof (rule production_swap_clause_set)
  show "{Da ∈ insert D N. (≺⇩c)⇧=⇧= Da C} = {D ∈ N. (≺⇩c)⇧=⇧= D C}"
    using ‹C ≺⇩c D› by auto
qed

lemma interp_insert_greater_clause_strong:
  assumes "C ≼⇩c D"
  shows "interp (insert D N) C = interp N C"
proof (rule interp_swap_clause_set)
  show "{x ∈ insert D N. x ≺⇩c C} = {x ∈ N. x ≺⇩c C}"
    using ‹C ≼⇩c D› by auto
qed

lemma interp_insert_greater_clause:
  assumes "C ≺⇩c D"
  shows "interp (insert D N) C = interp N C"
proof (rule interp_swap_clause_set)
  show "{x ∈ insert D N. x ≺⇩c C} = {x ∈ N. x ≺⇩c C}"
    using ‹C ≺⇩c D› by auto
qed

lemma Interp_insert_greater_clause:
  assumes "C ≺⇩c D"
  shows "interp (insert D N) C ∪ production (insert D N) C = interp N C ∪ production N C"
proof (rule Interp_swap_clause_set)
  show "{Da ∈ insert D N. (≺⇩c)⇧=⇧= Da C} = {D ∈ N. (≺⇩c)⇧=⇧= D C}"
    using ‹C ≺⇩c D› by auto
qed

lemma production_add_irrelevant_clause_to_set0:
  assumes
    fin: "finite N" and
    D_irrelevant: "E ∈ N" "E ⊂# D" "set_mset D = set_mset E" and
    no_select: "select E = {#}"
  shows "production (insert D N) D = {}"
proof -
  from D_irrelevant have "E ≺⇩c D"
    using subset_implies_multp by metis
  hence prod_E_subset: "production (insert D N) E ⊆ interp (insert D N) D"
    using production_subset_if_less_cls by metis

  show ?thesis
  proof (cases "production (insert D N) E = {}")
    case True
    hence "(∄A. is_strictly_maximal_lit (Pos A) E) ∨ interp (insert D N) E ⊫ E"
      unfolding production_unfold
      using no_select
      by (smt (verit, del_insts) Collect_empty_eq ‹E ∈ N› diff_single_eq_union insertI2
          literal_order.is_greatest_in_mset_iff)
    hence "(∄A. is_strictly_maximal_lit (Pos A) D) ∨ interp (insert D N) D ⊫ D"
    proof (elim disjE)
      assume "∄A. is_strictly_maximal_lit (Pos A) E"
      hence "∄A. is_strictly_maximal_lit (Pos A) D"
      proof (rule contrapos_nn)
        show "∃A. is_strictly_maximal_lit (Pos A) D ⟹ ∃A. is_strictly_maximal_lit (Pos A) E"
          using ‹E ⊂# D› ‹set_mset D = set_mset E›
          unfolding literal_order.is_greatest_in_mset_iff
          by (metis (no_types, opaque_lifting) add_mset_remove_trivial_eq
              insert_union_subset_iff)
      qed
      thus ?thesis ..
    next
      assume "interp (insert D N) E ⊫ E"
      hence "interp (insert D N) D ⊫ D"
        using lift_interp_entails ‹E ∈ N› ‹E ≺⇩c D›
        by (metis ‹set_mset D = set_mset E› insert_iff true_cls_def)
      thus ?thesis ..
    qed
    thus ?thesis
      unfolding production_unfold by auto
  next
    case False
    hence "interp (insert D N) D ⊫ D"
      using prod_E_subset
      by (metis ‹set_mset D = set_mset E› mem_productionE production_eq_empty_or_singleton
          insertCI insert_subset literal_order.is_greatest_in_mset_iff
          pos_literal_in_imp_true_cls)
    thus ?thesis
      unfolding production_unfold by simp
  qed
qed

lemma production_add_irrelevant_clause_to_set:
  assumes
    fin: "finite N" and
    C_in: "C ∈ N" and
    D_irrelevant: "∃E ∈ N. E ⊂# D ∧ set_mset D = set_mset E" and
    no_select: "⋀C. select C = {#}"
  shows "production (insert D N) C = production N C"
    using wfP_less_cls C_in
proof (induction C rule: wfp_induct_rule)
  case (less C)
  hence C_in_iff: "C ∈ insert D N ⟷ C ∈ N"
    by simp
  
  have interp_insert_eq: "interp (insert D N) C = interp N C"
  proof (cases "D ≺⇩c C")
    case True
    hence "{x ∈ insert D N. x ≺⇩c C} = insert D {x ∈ N. x ≺⇩c C}"
      by auto
    hence "⋃ (production (insert D N) ` {x ∈ insert D N. x ≺⇩c C}) =
      production (insert D N) D ∪ ⋃ (production (insert D N) ` {D ∈ N. D ≺⇩c C})"
      by simp
    also have "… = ⋃ (production (insert D N) ` {D ∈ N. D ≺⇩c C})"
      using production_add_irrelevant_clause_to_set0
      using D_irrelevant fin no_select by force
    also have "… = ⋃ (production N ` {D ∈ N. D ≺⇩c C})"
      using less.IH by simp
    finally show ?thesis
      unfolding interp_def .
  next
    case False
    then show ?thesis
      unfolding interp_def
      by (smt (verit, best) Collect_cong image_eq_imageI insert_iff less.IH mem_Collect_eq)
  qed

  show ?case
    unfolding production_unfold C_in_iff interp_insert_eq by argo
qed

lemma production_add_irrelevant_clauses_to_set0:
  assumes
    fin: "finite N" "finite N'" and
    D_in: "D ∈ N'" and
    irrelevant: "∀D ∈ N'. ∃E ∈ N. E ⊂# D ∧ set_mset D = set_mset E" and
    no_select: "⋀C. select C = {#}"
  shows "production (N ∪ N') D = {}"
  using ‹finite N'› D_in irrelevant
proof (induction N' rule: finite_induct)
  case empty
  hence False
    by simp
  thus ?case ..
next
  case (insert x F)
  then show ?case
    using production_add_irrelevant_clause_to_set0
    by (metis UnCI fin(1) finite_Un finite_insert production_add_irrelevant_clause_to_set no_select)
qed

lemma production_add_irrelevant_clauses_to_set:
  assumes
    fin: "finite N" "finite N'" and
    C_in: "C ∈ N" and
    irrelevant: "∀D ∈ N'. ∃E ∈ N. E ⊂# D ∧ set_mset D = set_mset E" and
    no_select: "⋀C. select C = {#}"
  shows "production (N ∪ N') C = production N C"
  using ‹finite N'› irrelevant
proof (induction N' rule: finite_induct)
  case empty
  show ?case
    by simp
next
  case (insert x F)
  then show ?case
    using production_add_irrelevant_clause_to_set
    by (metis C_in UnI1 Un_insert_right fin(1) finite_Un insertCI no_select)
qed

lemma interp_add_irrelevant_clauses_to_set:
  assumes
    fin: "finite N" "finite N'" and
    C_in: "C ∈ N" and
    irrelevant: "∀D ∈ N'. ∃E ∈ N. E ⊂# D ∧ set_mset D = set_mset E" and
    no_select: "⋀C. select C = {#}"
  shows "interp (N ∪ N') C = interp N C"
proof -
  have "interp (N ∪ N') C = ⋃ (production (N ∪ N') ` {D ∈ N ∪ N'. D ≺⇩c C})"
    unfolding interp_def ..
  also have "… = ⋃ (production (N ∪ N') ` {D ∈ N. D ≺⇩c C} ∪
    production (N ∪ N') ` {D ∈ N'. D ≺⇩c C})"
    by auto
  also have "… = ⋃ (production (N ∪ N') ` {D ∈ N. D ≺⇩c C})"
    using production_add_irrelevant_clauses_to_set0[OF fin _ irrelevant no_select] by simp
  also have "… = ⋃ (production N ` {D ∈ N. D ≺⇩c C})"
    using production_add_irrelevant_clauses_to_set[OF fin _ _ no_select] irrelevant
    using subset_mset.less_le by fastforce
  also have "… = interp N C"
    unfolding interp_def ..
  finally show ?thesis .
qed

lemma interp_add_irrelevant_clauses_to_set':
  assumes
    fin: "finite N" "finite N'" and
    C_in: "C ∈ N" and
    irrelevant: "∀D ∈ N'. ∃E ∈ N. E ⊆# D ∧ set_mset D = set_mset E" and
    no_select: "⋀C. select C = {#}"
  shows "interp (N ∪ N') C = interp N C"
proof -
  define N'' where
    "N'' = N' - N"

  from fin(2) have "finite N''"
    unfolding N''_def by simp

  moreover from irrelevant have "∀D ∈ N''. ∃E ∈ N. E ⊂# D ∧ set_mset E = set_mset D"
    unfolding N''_def
    by (metis Diff_iff subset_mset.le_less)

  moreover have "N ∪ N' = N ∪ N''"
    unfolding N''_def by simp

  ultimately show ?thesis
    using assms interp_add_irrelevant_clauses_to_set by metis
qed

lemma lesser_entailed_clause_stays_entailed':
  assumes "C ≼⇩c D" and D_lt: "D ≺⇩c E" and C_entailed: "interp N D ∪ production N D ⊫ C"
  shows "interp N E ⊫ C"
proof -
  from C_entailed obtain L where "L ∈# C" and "interp N D ∪ production N D ⊫l L"
    by (auto simp: true_cls_def)

  show ?thesis
  proof (cases L)
    case (Pos A)
    hence "A ∈ interp N D ∪ production N D"
      using ‹interp N D ∪ production N D ⊫l L› by simp
    moreover from D_lt have "interp N D ∪ production N D ⊆ interp N E"
      using less_imp_Interp_subseteq_interp by blast
    ultimately have "A ∈ interp N E"
      by auto
    thus ?thesis
      using Pos ‹L ∈# C› by auto
  next
    case (Neg A)
    then show ?thesis
      using neg_lits_not_in_model_stay_out_of_model
      by (smt (verit, best) UN_E Un_iff ‹L ∈# C› ‹interp N D ∪ production N D ⊫l L› assms(1)
          interp_def clause_order.antisym_conv neg_literal_notin_imp_true_cls
          not_interp_to_Interp_imp_le produces_imp_in_interp true_lit_simps(2))
  qed
qed

lemma lesser_entailed_clause_stays_entailed:
  assumes C_le: "C ≼⇩c D" and D_lt: "D ≺⇩c E" and C_entailed: "interp N D ∪ production N D ⊫ C"
  shows "interp N E ∪ production N E ⊫ C"
proof -
  from C_entailed obtain L where "L ∈# C" and "interp N D ∪ production N D ⊫l L"
    by (auto simp: true_cls_def)

  show ?thesis
  proof (cases L)
    case (Pos A)
    hence "A ∈ interp N D ∪ production N D"
      using ‹interp N D ∪ production N D ⊫l L› by simp
    moreover from D_lt have "interp N D ∪ production N D ⊆ interp N E ∪ production N E"
      using less_imp_Interp_subseteq_interp by blast
    ultimately have "A ∈ interp N E ∪ production N E"
      by auto
    thus ?thesis
      using Pos ‹L ∈# C› by auto
  next
    case (Neg A)
    then show ?thesis
      using neg_lits_not_in_model_stay_out_of_model
      by (smt (verit, best) UN_E Un_iff ‹L ∈# C› ‹interp N D ∪ production N D ⊫l L› assms(1)
          interp_def clause_order.antisym_conv neg_literal_notin_imp_true_cls
          not_interp_to_Interp_imp_le produces_imp_in_interp true_lit_simps(2))
  qed
qed

lemma entailed_clause_stays_entailed':
  assumes C_lt: "C ≺⇩c D" and C_entailed: "interp N C ∪ production N C ⊫ C"
  shows "interp N D ⊫ C"
  using lesser_entailed_clause_stays_entailed'[OF clause_order.order_refl assms] .

lemma entailed_clause_stays_entailed:
  assumes C_lt: "C ≺⇩c D" and C_entailed: "interp N C ∪ production N C ⊫ C"
  shows "interp N D ∪ production N D ⊫ C"
  using lesser_entailed_clause_stays_entailed[OF clause_order.order_refl assms] .

lemma multp_if_all_left_smaller: "M2 ≠ {#} ⟹ ∀k∈#M1. ∃j∈#M2. R k j ⟹ multp R M1 M2"
  using one_step_implies_multp
  by (metis add_0)

lemma
  fixes
    P1 :: "'f gterm" and
    C1 :: "'f gterm clause" and
    N :: "'f gterm clause set"
  defines
    "C1 ≡ {#Neg P1#}" and
    "N ≡ {C1}"
  assumes
    no_select: "⋀C. select C = {#}"
  shows
    False
proof -
  have "interp N C1 = {}"
    unfolding interp_def N_def by simp
  have "production N C1 = {}"
    unfolding production_unfold ‹interp N C1 = {}› C1_def by simp
  hence "interp N C1 ∪ production N C1 ⊫ C1"
    unfolding ‹interp N C1 = {}› ‹production N C1 = {}›
    by (simp add: C1_def)
  oops

lemma
  fixes
    P1 P2 :: "'f gterm" and
    C1 :: "'f gterm clause" and
    N :: "'f gterm clause set"
  defines
    "C1 ≡ {#Pos P1, Neg P2#}" and
    "N ≡ {C1}"
  assumes
    term_order: "P1 ≺⇩t P2" and
    no_select: "⋀C. select C = {#}"
  shows False
proof -
  have lit_order: "Pos P1 ≺⇩l Neg P1" "Neg P1 ≺⇩l Pos P2" "Pos P2 ≺⇩l Neg P2"
    using term_order by simp_all
  have "interp N C1 = {}"
    unfolding interp_def N_def by simp
  have "production N C1 = {}"
    unfolding production_unfold
    using C1_def ‹interp N C1 = {}› by simp
  hence "interp N C1 ∪ production N C1 ⊫ C1"
    unfolding ‹interp N C1 = {}› ‹production N C1 = {}›
    by (simp add: C1_def)
  oops

  


lemma
  fixes
    P1 P2 P3 P4 :: "'f gterm" and
    C1 C2 C3 C4 C5 :: "'f gterm clause" and
    N :: "'f gterm clause set"
  defines
    "C1 ≡ {#Neg P1, Neg P2#}" and
    "C2 ≡ {#Pos P2, Neg P3#}" and
    "C3 ≡ {#Pos P1, Pos P2, Pos P4#}" and
    "C4 ≡ {#Pos P2, Pos P3, Pos P4#}" and
    "C5 ≡ {#Pos P2, Neg P4#}" and
    "N ≡ {C1, C2, C3, C4, C5}"
  assumes
    term_order: "P1 ≺⇩t P2" "P2 ≺⇩t P3" "P3 ≺⇩t P4" and
    no_select: "⋀C. select C = {#}"
  shows
    "C1 ≺⇩c C2" "C2 ≺⇩c C3" "C3 ≺⇩c C4" "C4 ≺⇩c C5"
proof -
  have lit_order: "Pos P1 ≺⇩l Neg P1" "Neg P1 ≺⇩l Pos P2" "Pos P2 ≺⇩l Neg P2" "Neg P2 ≺⇩l Pos P3"
    "Pos P3 ≺⇩l Neg P3" "Neg P3 ≺⇩l Pos P4" "Pos P4 ≺⇩l Neg P4"
    using term_order by simp_all

  show "C1 ≺⇩c C2"
    unfolding C1_def C2_def
  proof (rule multp_if_all_left_smaller)
    show "{#Pos P2, Neg P3#} ≠ {#}"
      by simp
  next
    show "∀k∈#{#Neg P1, Neg P2#}. ∃j∈#{#Pos P2, Neg P3#}. k ≺⇩l j"
      using lit_order by simp
  qed

  moreover show "C2 ≺⇩c C3"
    unfolding C2_def C3_def
  proof (rule multp_if_all_left_smaller)
    show "{#Pos P1, Pos P2, Pos P4#} ≠ {#}"
      by simp
  next
    show "∀k∈#{#Pos P2, Neg P3#}. ∃j∈#{#Pos P1, Pos P2, Pos P4#}. k ≺⇩l j"
      using lit_order by auto
  qed

  moreover show "C3 ≺⇩c C4"
  proof -
    have "{#Pos P1, Pos P2#} ≺⇩c {#Pos P2, Pos P3#}"
    proof (rule multp_if_all_left_smaller)
      show "{#Pos P2, Pos P3#} ≠ {#}"
        by simp
    next
      show "∀k∈#{#Pos P1, Pos P2#}. ∃j∈#{#Pos P2, Pos P3#}. k ≺⇩l j"
        using lit_order by simp
    qed
    thus ?thesis
      unfolding C3_def C4_def
      by (smt (verit, ccfv_SIG) add_mset_commute irreflp_on_less_lit multp_cancel_add_mset
          transp_less_lit)
  qed

  moreover show "C4 ≺⇩c C5"
    unfolding C4_def C5_def
  proof (rule multp_if_all_left_smaller)
    show "{#Pos P2, Neg P4#} ≠ {#}"
      by simp
  next
    show "∀k∈#{#Pos P2, Pos P3, Pos P4#}. ∃j∈#{#Pos P2, Neg P4#}. k ≺⇩l j"
      using lit_order by auto
  qed

  note cls_order = calculation this

  have "interp N C1 = {}"
    unfolding interp_def N_def
    using cls_order
    by (smt (verit, best) Collect_empty_eq bot_fset.rep_eq ccSUP_empty finsertCI fset_simps(2)
        clause_order.dual_order.strict_implies_not_eq clause_order.is_minimal_in_fset_finsertI
        clause_order.is_minimal_in_fset_iff singletonD)
  hence "production N C1 = {}"
    unfolding production_unfold C1_def by simp
  hence "interp N C1 ∪ production N C1 ⊫ C1"
    unfolding ‹interp N C1 = {}› ‹production N C1 = {}›
    unfolding C1_def
    unfolding true_cls_def true_lit_def
    by (simp add: C1_def)

  have "{D ∈ N. D ≺⇩c C2} = {C1}"
    unfolding N_def
    using cls_order by auto
  hence "interp N C2 = interp N C1 ∪ production N C1"
    unfolding ‹interp N C1 = {}›
    unfolding interp_def
    by simp
  hence "interp N C2 = {}"
    unfolding ‹interp N C1 = {}› ‹production N C1 = {}› by simp
  hence "production N C2 = {}"
    unfolding production_unfold
    by (simp add: C2_def)
  hence "interp N C2 ∪ production N C2 ⊫ C2"
    using ‹interp N C2 = {}›
    by (simp add: C2_def)

  have "{D ∈ N. D ≺⇩c C3} = {C1, C2}"
    unfolding N_def
    using cls_order by auto
  hence "interp N C3 = interp N C2 ∪ production N C2"
    unfolding ‹interp N C2 = {}›
    unfolding interp_def
    by (simp add: ‹production N C1 = {}›)
  hence "interp N C3 = {}"
    unfolding ‹interp N C2 = {}› ‹production N C2 = {}› by simp
  have "production N C3 = {P4}"
  proof -
    have "C3 ∈ N"
      by (simp add: N_def)
    moreover have "∃C3'. C3 = add_mset (Pos P4) C3'"
      by (auto simp: C3_def)
    moreover have "is_strictly_maximal_lit (Pos P4) C3"
      unfolding C3_def literal_order.is_greatest_in_mset_iff
      using lit_order by auto
    moreover have "¬ interp N C3 ⊫ C3"
      unfolding ‹interp N C3 = {}›
      unfolding C3_def
      by simp
    ultimately have "P4 ∈ production N C3"
      unfolding production_unfold
      using no_select
      by simp
    thus ?thesis
      using production_eq_empty_or_singleton by fastforce
  qed
  hence "interp N C3 ∪ production N C3 ⊫ C3"
    using ‹interp N C3 = {}›
    by (simp add: C3_def)

  have "{D ∈ N. D ≺⇩c C4} = {C1, C2, C3}"
    unfolding N_def
    using cls_order by auto
  hence "interp N C4 = interp N C3 ∪ production N C3"
    unfolding ‹interp N C3 = interp N C2 ∪ production N C2›
    unfolding ‹interp N C2 = interp N C1 ∪ production N C1›
    unfolding ‹interp N C1 = {}›
    unfolding interp_def
    by auto
  hence "interp N C4 = {P4}"
    using ‹interp N C3 = {}› ‹production N C3 = {P4}› by simp
  hence "interp N C4 ⊫ C4"
    using C4_def by simp
  hence "production N C4 = {}"
    unfolding production_unfold by simp
  hence "interp N C4 ∪ production N C4 ⊫ C4"
    using ‹interp N C4 = {P4}›
    by (simp add: C4_def)

  have "{D ∈ N. D ≺⇩c C5} = {C1, C2, C3, C4}"
    unfolding N_def
    using cls_order by auto
  hence "interp N C5 = interp N C4 ∪ production N C4"
    unfolding ‹interp N C4 = interp N C3 ∪ production N C3›
    unfolding ‹interp N C3 = interp N C2 ∪ production N C2›
    unfolding ‹interp N C2 = interp N C1 ∪ production N C1›
    unfolding ‹interp N C1 = {}›
    unfolding interp_def
    by auto
  hence "interp N C5 = {P4}"
    using ‹interp N C4 = {P4}› ‹production N C4 = {}› by simp
  have "production N C5 = {}"
  proof -
    have "is_strictly_maximal_lit (Neg P4) C5"
      unfolding C5_def literal_order.is_greatest_in_mset_iff
      using lit_order by auto
    hence "⋀A. ¬ is_strictly_maximal_lit (Pos A) C5"
      by (meson Uniq_D literal_order.Uniq_is_greatest_in_mset literal.distinct(1))
    thus ?thesis
      unfolding production_unfold by simp
  qed
  hence "¬ interp N C5 ∪ production N C5 ⊫ C5"
    unfolding ‹interp N C5 = {P4}› ‹production N C5 = {}›
    unfolding C5_def
    using term_order
    by simp
qed 
  

interpretation G: statically_complete_calculus G_Bot G_Inf G_entails G.Red_I G.Red_F
proof unfold_locales
  fix B :: "'f gterm atom clause" and N :: "'f gterm atom clause set"
  assume "B ∈ G_Bot" and "G.saturated N"
  hence "B = {#}"
    by simp

  assume "G_entails N {B}"
  hence "{#} ∈ N"
    unfolding ‹B = {#}›
  proof (rule contrapos_pp)
    assume "{#} ∉ N"

    define I :: "'f gterm set" where
      "I = (⋃D ∈ N. production N D)"

    show "¬ G_entails N G_Bot"
      unfolding G_entails_def not_all not_imp
    proof (intro exI conjI)
      show "I ⊫s N"
        unfolding I_def
        using model_construction(2)[OF ‹G.saturated N› ‹{#} ∉ N›]
        by (simp add: true_clss_def)
    next
      show "¬ I ⊫s G_Bot"
        by simp
    qed
  qed
  thus "∃B'∈G_Bot. B' ∈ N"
    by auto
qed

end

end