Theory Exhaustive_Resolution

theory Exhaustive_Resolution
  imports Background
begin

section ‹Function for full resolution›

context simulation_SCLFOL_ground_ordered_resolution begin

definition ground_resolution where
  "ground_resolution D C CD = ord_res.ground_resolution C D CD"

lemma Uniq_ground_resolution: "∃⇩≤⇩1DC. ground_resolution D C DC"
  by (simp add: ground_resolution_def ord_res.unique_ground_resolution)

lemma ground_resolution_terminates: "wfP (ground_resolution D)¯¯"
proof (rule wfp_if_convertible_to_wfp)
  show "wfP (≺⇩c)"
    using ord_res.wfP_less_cls .
next
  show "⋀x y. (ground_resolution D)¯¯ x y ⟹ x ≺⇩c y"
  unfolding ground_resolution_def conversep_iff
  using ord_res.ground_resolution_smaller_conclusion by metis
qed

lemma not_ground_resolution_mempty_left: "¬ ground_resolution {#} C x"
  by (auto simp: ground_resolution_def elim: ord_res.ground_resolution.cases)

lemma not_ground_resolution_mempty_right: "¬ ground_resolution C {#} x"
  by (auto simp: ground_resolution_def elim: ord_res.ground_resolution.cases)

lemma not_tranclp_ground_resolution_mempty_left: "¬ (ground_resolution {#})⇧+⇧+ C x"
  by (metis not_ground_resolution_mempty_left tranclpD)

lemma not_tranclp_ground_resolution_mempty_right: "¬ (ground_resolution C)⇧+⇧+ {#} x"
  by (metis not_ground_resolution_mempty_right tranclpD)

lemma left_premise_lt_right_premise_if_ground_resolution:
  "ground_resolution D C DC ⟹ D ≺⇩c C"
  by (auto simp: ground_resolution_def elim: ord_res.ground_resolution.cases)

lemma left_premise_lt_right_premise_if_tranclp_ground_resolution:
  "(ground_resolution D)⇧+⇧+ C DC ⟹ D ≺⇩c C"
  by (induction DC rule: tranclp_induct)
    (auto simp add: left_premise_lt_right_premise_if_ground_resolution)

lemma resolvent_lt_right_premise_if_ground_resolution:
  "ground_resolution D C DC ⟹ DC ≺⇩c C"
  by (simp add: ground_resolution_def ord_res.ground_resolution_smaller_conclusion)

lemma resolvent_lt_right_premise_if_tranclp_ground_resolution:
  "(ground_resolution D)⇧+⇧+ C DC ⟹ DC ≺⇩c C"
proof (induction DC rule: tranclp_induct)
  case (base y)
  thus ?case
    by (simp add: resolvent_lt_right_premise_if_ground_resolution)
next
  case (step y z)
  have "z ≺⇩c y"
    using step.hyps resolvent_lt_right_premise_if_ground_resolution by metis
  thus ?case
    using step.IH by order
qed


text ‹Exhaustive resolution›

definition eres where
  "eres D C = (THE DC. full_run (ground_resolution D) C DC)"

text ‹The function \<^const>‹eres› performs exhaustive resolution between its two input clauses. The
  first clause is repeatedly used, while the second clause is only use to start the resolution
  chain.›

lemma eres_ident_iff: "eres D C = C ⟷ (∄DC. ground_resolution D C DC)"
proof (rule iffI)
  assume "eres D C = C"
  thus "∄DC. ground_resolution D C DC"
    unfolding eres_def
    by (metis Uniq_full_run Uniq_ground_resolution full_run_def ground_resolution_terminates
        ex1_full_run the1_equality')
next
  assume stuck: "∄DC. ground_resolution D C DC"
  have "(ground_resolution D)⇧*⇧* C C"
    by auto

  with stuck have "full_run (ground_resolution D) C C"
    unfolding full_run_def by argo

  moreover have Uniq: "∃⇩≤⇩1 y. full_run (ground_resolution D) C y"
    by (metis Uniq_ground_resolution Uniq_full_run)

  ultimately show "eres D C = C"
    unfolding eres_def by (metis the1_equality')
qed

lemma
  assumes
    step1: "ground_resolution D C DC" and
    stuck: "∄DDC. ground_resolution D DC DDC"
  shows "eres D C = DC"
proof -
  from step1 have "(ground_resolution D)⇧*⇧* C DC"
    by auto

  with stuck have "full_run (ground_resolution D) C DC"
    unfolding full_run_def by argo

  moreover have Uniq: "∃⇩≤⇩1 y. full_run (ground_resolution D) C y"
    by (metis Uniq_ground_resolution Uniq_full_run)

  ultimately show ?thesis
    unfolding eres_def by (metis the1_equality')
qed

lemma
  assumes
    step1: "ground_resolution D C DC" and
    step2: "ground_resolution D DC DDC" and
    stuck: "∄DDDC. ground_resolution D DDC DDDC"
  shows "eres D C = DDC"
proof -
  from step1 have "(ground_resolution D)⇧*⇧* C DC"
    by auto

  with step2 have "(ground_resolution D)⇧*⇧* C DDC"
    by (metis rtranclp.simps)

  with stuck have "full_run (ground_resolution D) C DDC"
    unfolding full_run_def by argo

  moreover have Uniq: "∃⇩≤⇩1 y. full_run (ground_resolution D) C y"
    by (metis Uniq_ground_resolution Uniq_full_run)

  ultimately show ?thesis
    unfolding eres_def by (metis the1_equality')
qed

lemma
  assumes
    step1: "ground_resolution D C DC" and
    step2: "ground_resolution D DC DDC" and
    step3: "ground_resolution D DDC DDDC" and
    stuck: "∄DDDDC. ground_resolution D DDDC DDDDC"
  shows "eres D C = DDDC"
proof -
  from step1 have "(ground_resolution D)⇧*⇧* C DC"
    by auto

  with step2 have "(ground_resolution D)⇧*⇧* C DDC"
    by (metis rtranclp.simps)

  with step3 have "(ground_resolution D)⇧*⇧* C DDDC"
    by (metis rtranclp.simps)

  with stuck have "full_run (ground_resolution D) C DDDC"
    unfolding full_run_def by argo

  moreover have Uniq: "∃⇩≤⇩1 y. full_run (ground_resolution D) C y"
    by (metis Uniq_ground_resolution Uniq_full_run)

  ultimately show ?thesis
    unfolding eres_def by (metis the1_equality')
qed

lemma eres_mempty_left[simp]: "eres {#} C = C"
  unfolding eres_def
  by (metis Uniq_full_run Uniq_ground_resolution full_run_def not_ground_resolution_mempty_left
      rtranclp.rtrancl_refl the1_equality')

lemma eres_mempty_right[simp]: "eres C {#} = {#}"
  unfolding eres_def
  by (metis Uniq_full_run Uniq_ground_resolution full_run_def not_ground_resolution_mempty_right
      rtranclp.rtrancl_refl the1_equality')

lemma ex1_eres_eq_full_run_ground_resolution: "∃!DC. eres D C = DC ∧ full_run (ground_resolution D) C DC"
  using ex1_full_run[of "ground_resolution D" C]
  by (metis Uniq_ground_resolution eres_def ground_resolution_terminates theI')

lemma eres_le: "eres D C ≼⇩c C"
proof -
  have "full_run (ground_resolution D) C (eres D C)"
    using ex1_eres_eq_full_run_ground_resolution by metis
  thus ?thesis
  proof (rule full_run_preserves_invariant)
    show "C ≼⇩c C"
      by simp
  next
    show "⋀x y. ground_resolution D x y ⟹ x ≼⇩c C ⟹ y ≼⇩c C"
      unfolding ground_resolution_def
      using ord_res.ground_resolution_smaller_conclusion by fastforce
  qed
qed

lemma clause_lt_clause_if_max_lit_comp:
  assumes E_max_lit: "linorder_lit.is_maximal_in_mset E L" and L_neg: "is_neg L" and
    D_max_lit: "linorder_lit.is_maximal_in_mset D (- L)"
  shows "D ≺⇩c E"
proof -
  have "- L ≺⇩l L"
    using L_neg by (cases L) simp_all

  thus ?thesis
    using D_max_lit E_max_lit
    by (metis linorder_lit.multp_if_maximal_less_that_maximal)
qed

lemma eres_lt_if:
  assumes E_max_lit: "ord_res.is_maximal_lit L E" and L_neg: "is_neg L" and
    D_max_lit: "linorder_lit.is_greatest_in_mset D (- L)"
  shows "eres D E ≺⇩c E"
proof -
  have "eres D E ≠ E"
    unfolding eres_ident_iff not_not ground_resolution_def
  proof (rule ex_ground_resolutionI)
    show "ord_res.is_maximal_lit (Neg (atm_of L)) E"
      using E_max_lit L_neg by (cases L) simp_all
  next
    show "D ≺⇩c E"
      using E_max_lit D_max_lit L_neg
      by (metis clause_lt_clause_if_max_lit_comp
          linorder_lit.is_maximal_in_mset_if_is_greatest_in_mset)
  next
    show "ord_res.is_strictly_maximal_lit (Pos (atm_of L)) D"
      using D_max_lit ‹is_neg L›
      by (cases L) simp_all
  qed

  thus "eres D E ≺⇩c E"
    using eres_le[of D E] by order
qed

lemma eres_eq_after_ground_resolution:
  assumes "ground_resolution D C DC"
  shows "eres D C = eres D DC"
  using assms
  by (metis (no_types, opaque_lifting) Uniq_def Uniq_full_run Uniq_ground_resolution
      converse_rtranclpE ex1_eres_eq_full_run_ground_resolution full_run_def)

lemma eres_eq_after_rtranclp_ground_resolution:
  assumes "(ground_resolution D)⇧*⇧* C DC"
  shows "eres D C = eres D DC"
  using assms
  by (induction DC rule: rtranclp_induct) (simp_all add: eres_eq_after_ground_resolution)

lemma eres_eq_after_tranclp_ground_resolution:
  assumes "(ground_resolution D)⇧+⇧+ C DC"
  shows "eres D C = eres D DC"
  using assms
  by (induction DC rule: tranclp_induct) (simp_all add: eres_eq_after_ground_resolution)

lemma resolvable_if_neq_eres:
  assumes "C ≠ eres D C"
  shows "∃!DC. ground_resolution D C DC"
  using assms ex1_eres_eq_full_run_ground_resolution
  by (metis (no_types, opaque_lifting) Uniq_def Uniq_full_run Uniq_ground_resolution full_run_def
      rtranclp.rtrancl_refl)

lemma nex_maximal_pos_lit_if_resolvable:
  assumes "ground_resolution D C DC"
  shows "∄L. is_pos L ∧ ord_res.is_maximal_lit L C"
  using assms unfolding ground_resolution_def
  by (metis Uniq_D empty_iff is_pos_def linorder_lit.Uniq_is_maximal_in_mset
      literal.simps(4) ord_res.ground_resolution.cases set_mset_empty)

corollary nex_strictly_maximal_pos_lit_if_resolvable:
  assumes "ground_resolution D C DC"
  shows "∄L. is_pos L ∧ ord_res.is_strictly_maximal_lit L C"
  using assms nex_maximal_pos_lit_if_resolvable by blast

corollary nex_maximal_pos_lit_if_neq_eres:
  assumes "C ≠ eres D C"
  shows "∄L. is_pos L ∧ ord_res.is_maximal_lit L C"
  using assms resolvable_if_neq_eres nex_maximal_pos_lit_if_resolvable by metis

corollary nex_strictly_maximal_pos_lit_if_neq_eres:
  assumes "C ≠ eres D C"
  shows "∄L. is_pos L ∧ ord_res.is_strictly_maximal_lit L C"
  using assms resolvable_if_neq_eres nex_strictly_maximal_pos_lit_if_resolvable by metis

lemma ground_resolutionD:
  assumes "ground_resolution D C DC"
  shows "∃m A D' C'.
    linorder_lit.is_greatest_in_mset D (Pos A) ∧
    linorder_lit.is_maximal_in_mset C (Neg A) ∧
    D = add_mset (Pos A) D' ∧
    C = replicate_mset (Suc m) (Neg A) + C' ∧ Neg A ∉# C' ∧
    DC = D' + replicate_mset m (Neg A) + C'"
  using assms
  unfolding ground_resolution_def
proof (cases C D DC rule: ord_res.ground_resolution.cases)
  case (ground_resolutionI A C' D')

  then obtain m where "count C (Neg A) = Suc m"
    by simp

  define C'' where
    "C'' = {#L ∈# C. L ≠ Neg A#}"

  have "C = replicate_mset (Suc m) (Neg A) + C''"
    using ‹count C (Neg A) = Suc m› C''_def
    by (metis filter_eq_replicate_mset union_filter_mset_complement)

  show ?thesis
  proof (intro exI conjI)
    show "linorder_lit.is_greatest_in_mset D (Pos A)"
      using ‹linorder_lit.is_greatest_in_mset D (Pos A)› .
  next
    show "linorder_lit.is_maximal_in_mset C (Neg A)"
      using ground_resolutionI by simp
  next
    show "D = add_mset (Pos A) D'"
      using ‹D = add_mset (Pos A) D'› .
  next
    show "C = replicate_mset (Suc m) (Neg A) + C''"
      using ‹C = replicate_mset (Suc m) (Neg A) + C''› .
  next
    show "Neg A ∉# C''"
      by (simp add: C''_def)
  next
    show "DC = D' + replicate_mset m (Neg A) + C''"
      using ‹DC = C' + D'› ‹C = add_mset (Neg A) C'› ‹C = replicate_mset (Suc m) (Neg A) + C''›
      by simp
  qed
qed

lemma relpowp_ground_resolutionD:
  assumes "n ≠ 0" and "(ground_resolution D ^^ n) C DnC"
  shows "∃m A D' C'. Suc m ≥ n ∧
    linorder_lit.is_greatest_in_mset D (Pos A) ∧
    linorder_lit.is_maximal_in_mset C (Neg A) ∧
    D = add_mset (Pos A) D' ∧
    C = replicate_mset (Suc m) (Neg A) + C' ∧ Neg A ∉# C' ∧
    DnC = repeat_mset n D' + replicate_mset (Suc m - n) (Neg A) + C'"
  using assms
proof (induction n arbitrary: C)
  case 0
  hence False
    by simp
  thus ?case ..
next
  case (Suc n')
  then obtain DC where
    "ground_resolution D C DC" and "(ground_resolution D ^^ n') DC DnC"
    by (metis relpowp_Suc_E2)

  then obtain m A D' C' where
    "linorder_lit.is_greatest_in_mset D (Pos A)" and
    "linorder_lit.is_maximal_in_mset C (Neg A)"
    "D = add_mset (Pos A) D'" and
    "C = replicate_mset (Suc m) (Neg A) + C'" and
    "Neg A ∉# C'" and
    "DC = D' + replicate_mset m (Neg A) + C'"
    using ‹ground_resolution D C DC›[THEN ground_resolutionD] by metis

  have "Neg A ∉# D'"
    using ‹linorder_lit.is_greatest_in_mset D (Pos A)›
    unfolding ‹D = add_mset (Pos A) D'›
    unfolding linorder_lit.is_greatest_in_mset_iff
    by auto

  show ?case
  proof (cases n')
    case 0
    hence "DnC = DC"
      using ‹(ground_resolution D ^^ n') DC DnC› by simp

    show ?thesis
      unfolding 0 ‹DnC = DC›
      unfolding repeat_mset_Suc repeat_mset_0 empty_neutral
      unfolding diff_Suc_Suc minus_nat.diff_0
      using ‹C = replicate_mset (Suc m) (Neg A) + C'› ‹D = add_mset (Pos A) D'›
        ‹DC = D' + replicate_mset m (Neg A) + C'› ‹Neg A ∉# C'›
        ‹linorder_lit.is_greatest_in_mset D (Pos A)› ‹linorder_lit.is_maximal_in_mset C (Neg A)›
      using linorder_lit.is_greatest_in_mset_iff
      by blast
  next
    case (Suc n'')
    hence "n' ≠ 0"
      by presburger
    then obtain m' A' D'' DC' where "n' ≤ Suc m'" and
       "ord_res.is_strictly_maximal_lit (Pos A') D" and
       "ord_res.is_maximal_lit (Neg A') DC" and
       "D = add_mset (Pos A') D''" and
       "DC = replicate_mset (Suc m') (Neg A') + DC'" and
       "Neg A' ∉# DC'" and
       "DnC = repeat_mset n' D'' + replicate_mset (Suc m' - n') (Neg A') + DC'"
      using Suc.IH[OF _ ‹(ground_resolution D ^^ n') DC DnC›]
      by metis

    have "A' = A"
      using ‹ord_res.is_strictly_maximal_lit (Pos A') D› ‹ord_res.is_strictly_maximal_lit (Pos A) D›
      by (meson Uniq_D linorder_lit.Uniq_is_maximal_in_mset
          linorder_lit.is_maximal_in_mset_if_is_greatest_in_mset literal.inject(1))

    hence "D'' = D'"
      using ‹D = add_mset (Pos A') D''› ‹D = add_mset (Pos A) D'› by auto

    have "m = Suc m'"
      using ‹DC = D' + replicate_mset m (Neg A) + C'› ‹DC = replicate_mset (Suc m') (Neg A') + DC'›
        ‹Neg A ∉# D'› ‹Neg A ∉# C'› ‹Neg A' ∉# DC'›
      unfolding ‹A' = A›
      by (metis add_0 count_eq_zero_iff count_replicate_mset count_union union_commute)

    hence "DC' = D' + C'"
      using ‹DC = D' + replicate_mset m (Neg A) + C'› ‹DC = replicate_mset (Suc m') (Neg A') + DC'›
      by (simp add: ‹A' = A›)

    show ?thesis
    proof (intro exI conjI)
      show "Suc n' ≤ Suc (Suc m')"
        using ‹n' ≤ Suc m'› by presburger
    next
      show "ord_res.is_strictly_maximal_lit (Pos A) D"
        using ‹ord_res.is_strictly_maximal_lit (Pos A) D› .
    next
      show "ord_res.is_maximal_lit (Neg A) C"
        using ‹ord_res.is_maximal_lit (Neg A) C› by metis
    next
      show "D = add_mset (Pos A) D'"
        using ‹D = add_mset (Pos A) D'› .
    next
      show "C = replicate_mset (Suc (Suc m')) (Neg A) + C'"
        using ‹C = replicate_mset (Suc m) (Neg A) + C'› ‹m = Suc m'› by argo
    next
      show "Neg A ∉# C'"
        using ‹Neg A ∉# C'› .
    next
      show "DnC = repeat_mset (Suc n') D' + replicate_mset (Suc (Suc m') - Suc n') (Neg A) + C'"
        using ‹DnC = repeat_mset n' D'' + replicate_mset (Suc m' - n') (Neg A') + DC'›
        unfolding ‹A' = A› ‹D'' = D'› diff_Suc_Suc ‹DC' = D' + C'›
        by simp
    qed
  qed
qed


lemma tranclp_ground_resolutionD:
  assumes "(ground_resolution D)⇧+⇧+ C DnC"
  shows "∃n m A D' C'. Suc m ≥ Suc n ∧
    linorder_lit.is_greatest_in_mset D (Pos A) ∧
    linorder_lit.is_maximal_in_mset C (Neg A) ∧
    D = add_mset (Pos A) D' ∧
    C = replicate_mset (Suc m) (Neg A) + C' ∧ Neg A ∉# C' ∧
    DnC = repeat_mset (Suc n) D' + replicate_mset (Suc m - Suc n) (Neg A) + C'"
proof -
  from assms obtain n :: nat where
    "(ground_resolution D ^^ Suc n) C DnC"
    by (metis Suc_pred tranclp_power)
  thus ?thesis
    using assms relpowp_ground_resolutionD
    by (meson nat.discI)
qed

lemma eres_not_identD:
  assumes "eres D C ≠ C"
  shows "∃m A D' C'.
    linorder_lit.is_greatest_in_mset D (Pos A) ∧
    linorder_lit.is_maximal_in_mset C (Neg A) ∧
    D = add_mset (Pos A) D' ∧
    C = replicate_mset (Suc m) (Neg A) + C' ∧ Neg A ∉# C' ∧
    eres D C = repeat_mset (Suc m) D' + C'"
proof -
  have "⋀n. Suc n ≠ 0"
    by presburger

  obtain n where
    steps: "(ground_resolution D ^^ Suc n) C (eres D C)" and
    stuck: "∄x. ground_resolution D (eres D C) x"
    using ‹eres D C ≠ C› ex1_eres_eq_full_run_ground_resolution
    by (metis full_run_def gr0_conv_Suc rtranclpD tranclp_power)

  obtain m A D' C' where
    "Suc n ≤ Suc m" and
    D_max_lit: "ord_res.is_strictly_maximal_lit (Pos A) D" and
    C_max_lit: "ord_res.is_maximal_lit (Neg A) C" and
    D_eq: "D = add_mset (Pos A) D'" and
    C_eq: "C = replicate_mset (Suc m) (Neg A) + C'" and
    "Neg A ∉# C'" and
    eres_eq: "eres D C = repeat_mset (Suc n) D' + replicate_mset (Suc m - Suc n) (Neg A) + C'"
    using relpowp_ground_resolutionD[of "Suc n", OF ‹Suc n ≠ 0› steps] by metis

  from stuck have "count (eres D C) (Neg A) = 0"
  proof (rule contrapos_np)
    assume "count (eres D C) (Neg A) ≠ 0"
    then obtain ERES' where "eres D C = add_mset (Neg A) ERES'"
      by (meson count_eq_zero_iff mset_add)

    moreover have "ord_res.is_maximal_lit (Neg A) (eres D C)"
      unfolding linorder_lit.is_maximal_in_mset_iff
    proof (intro conjI ballI impI)
      show "Neg A ∈# eres D C"
        unfolding ‹eres D C = add_mset (Neg A) ERES'› by simp
    next
      fix L
      assume "L ∈# eres D C" and "L ≠ Neg A"
      hence "L ∈# repeat_mset (Suc n) D' ∨ L ∈# C'"
        unfolding eres_eq
        by (metis Zero_not_Suc count_replicate_mset in_countE union_iff)
      thus "¬ Neg A ≺⇩l L"
      proof (elim disjE)
        assume "L ∈# repeat_mset (Suc n) D'"
        hence "L ∈# D'"
          using member_mset_repeat_msetD by metis
        hence "L ≺⇩l Pos A"
          using D_max_lit
          unfolding D_eq linorder_lit.is_greatest_in_mset_iff by simp
        also have "Pos A ≺⇩l Neg A"
          by simp
        finally show ?thesis
          by order
      next
        assume "L ∈# C'"
        thus ?thesis
          using C_eq ‹L ≠ Neg A› C_max_lit linorder_lit.is_maximal_in_mset_iff by auto
      qed
    qed

    moreover have "D ≺⇩c eres D C"
      using D_max_lit
      using ‹ord_res.is_maximal_lit (Neg A) (eres D C)›
      using linorder_lit.multp⇩H⇩O_if_maximal_less_that_maximal[of D "Pos A" "eres D C" "Neg A", simplified]
      using multp⇩D⇩M_imp_multp multp⇩H⇩O_imp_multp⇩D⇩M by blast

    ultimately show "∃x. ground_resolution D (eres D C) x"
      unfolding ground_resolution_def
      using D_eq D_max_lit
      using ord_res.ground_resolutionI[of "eres D C" A ERES' D D' "ERES' + D'"]
      by metis
  qed

  hence "m = n"
    using ‹eres D C = repeat_mset (Suc n) D' + replicate_mset (Suc m - Suc n) (Neg A) + C'›
    using ‹Suc n ≤ Suc m› by auto

  show ?thesis
  proof (intro exI conjI)
    show "ord_res.is_strictly_maximal_lit (Pos A) D"
      using D_max_lit .
  next
    show "ord_res.is_maximal_lit (Neg A) C"
      using C_max_lit .
  next
    show "D = add_mset (Pos A) D'"
      using D_eq .
  next
    show "C = replicate_mset (Suc m) (Neg A) + C'"
      using C_eq .
  next
    show "Neg A ∉# C'"
      using ‹Neg A ∉# C'› .
  next
    show "eres D C = repeat_mset (Suc m) D' + C'"
      using eres_eq unfolding ‹m = n› by simp
  qed
qed

lemma lit_in_one_of_resolvents_if_in_eres:
  fixes L :: "'f gterm literal" and C D :: "'f gclause"
  assumes "L ∈# eres C D"
  shows "L ∈# C ∨ L ∈# D"
proof (cases "eres C D = D")
  assume "eres C D = D"
  thus "L ∈# C ∨ L ∈# D"
    using ‹L ∈# eres C D› by argo
next
  assume "eres C D ≠ D"
  thus "L ∈# C ∨ L ∈# D"
    using ‹L ∈# eres C D›
    by (metis eres_not_identD member_mset_repeat_msetD repeat_mset_distrib_add_mset union_iff)
qed

lemma strong_lit_in_one_of_resolvents_if_in_eres:
  fixes L :: "'f gterm literal" and C D :: "'f gclause"
  assumes
    D_max_lit: "linorder_lit.is_maximal_in_mset D L" and
    K_in: "K ∈# eres C D"
  shows "K ∈# C ∧ K ≠ -L ∨ K ∈# D"
proof (cases "eres C D = D")
  assume "eres C D = D"
  thus "K ∈# C ∧ K ≠ -L ∨ K ∈# D"
    using K_in by argo
next
  assume "eres C D ≠ D"
  then obtain m :: nat and A :: "'f gterm" and C' D' :: "'f gterm literal multiset" where
    C_max_lit: "ord_res.is_strictly_maximal_lit (Pos A) C" and
    D_max_lit': "ord_res.is_maximal_lit (Neg A) D" and
    C_eq: "C = add_mset (Pos A) C'" and
    D_eq: "D = replicate_mset (Suc m) (Neg A) + D'" and
    "Neg A ∉# D'" and
    "eres C D = repeat_mset (Suc m) C' + D'"
    using eres_not_identD by metis

  have L_eq: "L = Neg A"
    using D_max_lit D_max_lit' by (metis Uniq_D linorder_lit.Uniq_is_maximal_in_mset)

  have "K ∈# repeat_mset (Suc m) C' + D'"
    using K_in unfolding ‹eres C D = repeat_mset (Suc m) C' + D'› .

  hence "K ∈# repeat_mset (Suc m) C' ∨ K ∈# D'"
    unfolding Multiset.union_iff .

  hence "K ∈# C' ∨ K ∈# D'"
    unfolding member_mset_repeat_mset_Suc .

  thus "K ∈# C ∧ K ≠ -L ∨ K ∈# D"
  proof (elim disjE)
    assume "K ∈# C'"

    hence "K ∈# C ∧ K ≠ - L"
      using C_max_lit
      unfolding C_eq L_eq linorder_lit.is_greatest_in_mset_iff by auto

    thus "K ∈# C ∧ K ≠ - L ∨ K ∈# D" ..
  next
    assume "K ∈# D'"

    hence "K ∈# D"
      unfolding D_eq by simp

    thus "K ∈# C ∧ K ≠ - L ∨ K ∈# D" ..
  qed
qed

lemma stronger_lit_in_one_of_resolvents_if_in_eres:
  fixes K L :: "'f gterm literal" and C D :: "'f gclause"
  assumes "eres C D ≠ D" and
    D_max_lit: "linorder_lit.is_maximal_in_mset D L" and
    K_in_eres: "K ∈# eres C D"
  shows "K ∈# C ∧ K ≠ - L ∨ K ∈# D ∧ K ≠ L "
proof -
  obtain m :: nat and A :: "'f gterm" and C' D' :: "'f gterm literal multiset" where
    C_max_lit: "ord_res.is_strictly_maximal_lit (Pos A) C" and
    C_def: "C = add_mset (Pos A) C'" and
    "D = replicate_mset (Suc m) (Neg A) + D'" and
    "Neg A ∉# D'" and
    "eres C D = repeat_mset (Suc m) C' + D'"
    using ‹eres C D ≠ D›[THEN eres_not_identD] by metis

  have "L = Neg A"
    using assms(1) D_max_lit C_max_lit
    by (metis ground_resolutionD linorder_lit.Uniq_is_greatest_in_mset
        linorder_lit.Uniq_is_maximal_in_mset resolvable_if_neq_eres the1_equality' uminus_Pos)

  have "K ∈# repeat_mset (Suc m) C' + D'"
    using K_in_eres unfolding ‹eres C D = repeat_mset (Suc m) C' + D'› .

  hence "K ∈# repeat_mset (Suc m) C' ∨ K ∈# D'"
    unfolding Multiset.union_iff .

  hence "K ∈# C' ∨ K ∈# D'"
    unfolding member_mset_repeat_mset_Suc .

  thus "K ∈# C ∧ K ≠ - L ∨ K ∈# D ∧ K ≠ L "
  proof (elim disjE)
    assume "K ∈# C'"

    hence "K ∈# C ∧ K ≠ - L"
      using C_max_lit[unfolded linorder_lit.is_greatest_in_mset_iff]
      unfolding ‹C = add_mset (Pos A) C'› ‹L = Neg A›
      by auto

    thus ?thesis
      by argo
  next
    assume "K ∈# D'"

    hence "K ∈# D ∧ K ≠ L "
      unfolding ‹D = replicate_mset (Suc m) (Neg A) +  D'› ‹L = Neg A›
      using ‹Neg A ∉# D'›
      by auto

    thus ?thesis
      by argo
  qed
qed

lemma lit_in_eres_lt_greatest_lit_in_grestest_resolvant:
  fixes K L :: "'f gterm literal" and C D :: "'f gclause"
  assumes "eres C D ≠ D" and
    D_max_lit: "linorder_lit.is_maximal_in_mset D L" and
    "- L ∉# D" and
    K_in_eres: "K ∈# eres C D"
  shows "atm_of K ≺⇩t atm_of L"
proof -
  obtain m :: nat and A :: "'f gterm" and C' D' :: "'f gterm literal multiset" where
    C_max_lit: "ord_res.is_strictly_maximal_lit (Pos A) C" and
    C_def: "C = add_mset (Pos A) C'" and
    "D = replicate_mset (Suc m) (Neg A) + D'" and
    "Neg A ∉# D'" and
    "eres C D = repeat_mset (Suc m) C' + D'"
    using ‹eres C D ≠ D›[THEN eres_not_identD] by metis

  have "L = Neg A"
    using assms(1) D_max_lit C_max_lit
    by (metis ground_resolutionD linorder_lit.Uniq_is_greatest_in_mset
        linorder_lit.Uniq_is_maximal_in_mset resolvable_if_neq_eres the1_equality' uminus_Pos)

  have "K ∈# repeat_mset (Suc m) C' + D'"
    using K_in_eres unfolding ‹eres C D = repeat_mset (Suc m) C' + D'› .

  hence "K ∈# repeat_mset (Suc m) C' ∨ K ∈# D'"
    unfolding Multiset.union_iff .

  hence "K ∈# C' ∨ K ∈# D'"
    unfolding member_mset_repeat_mset_Suc .

  thus "atm_of K ≺⇩t atm_of L"
  proof (elim disjE)
    assume "K ∈# C'"
    hence "K ≺⇩l Pos A"
      using C_max_lit C_def ‹L = Neg A›
      unfolding linorder_lit.is_greatest_in_mset_iff
      by simp
    thus "atm_of K ≺⇩t atm_of L"
      unfolding ‹L = Neg A› literal.sel
      by (cases K) simp_all
  next
    assume "K ∈# D'"
    hence "K ≺⇩l Neg A"
      by (metis D_max_lit ‹D = replicate_mset (Suc m) (Neg A) + D'› ‹L = Neg A› ‹Neg A ∉# D'›
          linorder_lit.is_maximal_in_mset_iff linorder_lit.neqE union_iff)

    moreover have "K ≠ Pos A"
      using ‹- L ∉# D›
      using ‹D = replicate_mset (Suc m) (Neg A) + D'› ‹K ∈# D'› ‹L = Neg A› by fastforce

    ultimately have "K ≺⇩l Pos A"
      by (metis linorder_lit.less_asym linorder_lit.less_linear literal.exhaust
          ord_res.less_lit_simps(1) ord_res.less_lit_simps(3) ord_res.less_lit_simps(4))

    thus "atm_of K ≺⇩t atm_of L"
      unfolding ‹L = Neg A› literal.sel
      by (cases K) simp_all
  qed
qed

lemma eres_entails_resolvent:
  fixes C D :: "'f gterm clause"
  assumes "(ground_resolution C)⇧+⇧+ D⇩0 D"
  shows "{eres C D⇩0} ⊫e {D}"
  unfolding true_clss_singleton
proof (intro allI impI)
  have "eres C D⇩0 = eres C D"
    using assms eres_eq_after_tranclp_ground_resolution by metis

  obtain n m :: nat and A :: "'f gterm" and C' D⇩0' :: "'f gterm clause" where
    "Suc n ≤ Suc m" and
    "ord_res.is_strictly_maximal_lit (Pos A) C" and
    "ord_res.is_maximal_lit (Neg A) D⇩0" and
    "C = add_mset (Pos A) C'" and
    "D⇩0 = replicate_mset (Suc m) (Neg A) + D⇩0'" and
    "Neg A ∉# D⇩0'" and
    "D = repeat_mset (Suc n) C' + replicate_mset (Suc m - Suc n) (Neg A) + D⇩0'"
    using ‹(ground_resolution C)⇧+⇧+ D⇩0 D›[THEN tranclp_ground_resolutionD] by metis

  fix I :: "'f gterm set"
  assume "I ⊫ eres C D⇩0"
  show "I ⊫ D"
  proof (cases "eres C D⇩0 = D")
    case True
    thus ?thesis
      using ‹I ⊫ eres C D⇩0› by argo
  next
    case False
    then obtain k :: nat and D' :: "'f gterm clause" where
      "ord_res.is_strictly_maximal_lit (Pos A) C" and
      "C = add_mset (Pos A) C'" and
      "D = replicate_mset (Suc k) (Neg A) + D'" and
      "Neg A ∉# D'" and
      "eres C D = repeat_mset (Suc k) C' + D'"
      unfolding ‹eres C D⇩0 = eres C D›
      using eres_not_identD
      using ‹ord_res.is_strictly_maximal_lit (Pos A) C› ‹C = add_mset (Pos A) C'›
      by (metis Uniq_D add_mset_remove_trivial linorder_lit.Uniq_is_greatest_in_mset literal.sel(1))

    have "I ⊫ repeat_mset (Suc k) C' + D'"
      using ‹I ⊫ eres C D⇩0›
      unfolding ‹eres C D⇩0 = eres C D› ‹eres C D = repeat_mset (Suc k) C' + D'› .

    hence "I ⊫ D' ∨ I ⊫ repeat_mset (Suc k) C'"
      by auto

    thus "I ⊫ D"
    proof (elim disjE)
      assume "I ⊫ D'"
      thus "I ⊫ D"
        unfolding ‹D = replicate_mset (Suc k) (Neg A) + D'›
        by simp
    next
      assume "I ⊫ repeat_mset (Suc k) C'"
      thus "I ⊫ D"
        using ‹D = replicate_mset (Suc k) (Neg A) + D'›
        using ‹D = repeat_mset (Suc n) C' + replicate_mset (Suc m - Suc n) (Neg A) + D⇩0'›
        by (metis member_mset_repeat_msetD repeat_mset_Suc true_cls_def true_cls_union)
    qed
  qed
qed



lemma clause_true_if_resolved_true:
  assumes
    "(ground_resolution D)⇧+⇧+ C DC" and
    D_productive: "ord_res.production N D ≠ {}" and
    C_true: "ord_res_Interp N DC ⊫ DC"
  shows "ord_res_Interp N C ⊫ C"
proof -
  obtain n where
    steps: "(ground_resolution D ^^ Suc n) C DC"
    using ‹(ground_resolution D)⇧+⇧+ C DC›
    by (metis less_not_refl not0_implies_Suc tranclp_power)

  obtain m A D' C' where
    "n ≤ m" and
    "ord_res.is_strictly_maximal_lit (Pos A) D" and
    "ord_res.is_maximal_lit (Neg A) C" and
    "D = add_mset (Pos A) D'" and
    "C = replicate_mset (Suc m) (Neg A) + C'" and
    "Neg A ∉# C'" and
    "DC = repeat_mset (Suc n) D' + replicate_mset (m - n) (Neg A) + C'"
    using relpowp_ground_resolutionD[OF Suc_not_Zero steps]
    by (metis diff_Suc_Suc Suc_le_mono)

  have "Neg A ∉# D'"
    by (metis ‹D = add_mset (Pos A) D'› ‹ord_res.is_strictly_maximal_lit (Pos A) D›
        ord_res.less_lit_simps(4) linorder_lit.is_greatest_in_mset_iff linorder_trm.eq_refl
        linorder_trm.leD remove1_mset_add_mset_If)

  have "DC ≺⇩c C"
  proof (cases "m = n")
    case True
    show ?thesis
    proof (intro one_step_implies_multp[of _ _ _ "{#}", simplified] ballI)
      show "C ≠ {#}"
        by (simp add: ‹C = replicate_mset (Suc m) (Neg A) + C'›)
    next
      fix L
      assume "L ∈# DC"
      hence "L ∈# D' ∨ L ∈# C'"
        unfolding ‹DC = repeat_mset (Suc n) D' + replicate_mset (m - n) (Neg A) + C'› ‹m = n›
        using member_mset_repeat_msetD by fastforce
      hence "L ≺⇩l Neg A"
        using ‹ord_res.is_strictly_maximal_lit (Pos A) D› ‹ord_res.is_maximal_lit (Neg A) C›
        unfolding ‹D = add_mset (Pos A) D'› ‹C = replicate_mset (Suc m) (Neg A) + C'›
        unfolding linorder_lit.is_maximal_in_mset_iff linorder_lit.is_greatest_in_mset_iff
        by (metis ‹Neg A ∉# C'› add_mset_remove_trivial ord_res.less_lit_simps(4)
            linorder_lit.antisym_conv3 linorder_lit.dual_order.strict_trans
            linorder_trm.dual_order.asym union_iff)

      moreover have "Neg A ∈# C"
        by (simp add: ‹C = replicate_mset (Suc m) (Neg A) + C'›)

      ultimately show "∃K ∈# C. L ≺⇩l K"
        by metis
    qed
  next
    case False
    hence "n < m"
      using ‹n ≤ m› by presburger

    have "multp⇩H⇩O (≺⇩l) DC C"
    proof (rule linorder_lit.multp⇩H⇩O_if_same_maximal_and_count_lt)
      show "ord_res.is_maximal_lit (Neg A) DC"
        unfolding linorder_lit.is_maximal_in_mset_iff
      proof (intro conjI ballI impI)
        show "Neg A ∈# DC"
          unfolding ‹DC = repeat_mset (Suc n) D' + replicate_mset (m - n) (Neg A) + C'›
          using ‹n < m› by simp
      next
        fix L
        assume "L ∈# DC" and "L ≠ Neg A"
        hence "L ∈# D' ∨ L ∈# C'"
          unfolding ‹DC = repeat_mset (Suc n) D' + replicate_mset (m - n) (Neg A) + C'›
          by (metis in_replicate_mset member_mset_repeat_msetD union_iff)
        thus "¬ Neg A ≺⇩l L"
          using ‹ord_res.is_strictly_maximal_lit (Pos A) D› ‹ord_res.is_maximal_lit (Neg A) C›
          unfolding ‹D = add_mset (Pos A) D'› ‹C = replicate_mset (Suc m) (Neg A) + C'›
          unfolding linorder_lit.is_maximal_in_mset_iff linorder_lit.is_greatest_in_mset_iff
          by (metis ‹L ≠ Neg A› add_mset_diff_bothsides diff_zero
              linorder_lit.dual_order.strict_trans linorder_trm.less_irrefl
              ord_res.less_lit_simps(4) union_iff)
      qed
    next
      show "ord_res.is_maximal_lit (Neg A) C"
        using ‹ord_res.is_maximal_lit (Neg A) C› .
    next
      have "count DC (Neg A) = count (repeat_mset (Suc n) D') (Neg A) +
      count (replicate_mset (m - n) (Neg A)) (Neg A) + count C' (Neg A)"
        unfolding ‹DC = repeat_mset (Suc n) D' + replicate_mset (m - n) (Neg A) + C'› by simp
      also have "… = count D' (Neg A) * Suc n + count {#Neg A#} (Neg A) * (m - n) + count C' (Neg A)"
        by simp
      also have "… = 0 * Suc n + 1 * (m - n) + 0"
        by (simp add: ‹Neg A ∉# C'› ‹Neg A ∉# D'› count_eq_zero_iff)
      also have "… = m - n"
        by presburger
      also have "… < Suc m"
        by presburger
      also have "… = 1 * Suc m + 0"
        by presburger
      also have "… = count {#Neg A#} (Neg A) * Suc m + count C' (Neg A)"
        by (simp add: ‹Neg A ∉# C'› count_eq_zero_iff)
      also have "… = count (replicate_mset (Suc m) (Neg A)) (Neg A) + count C' (Neg A)"
        by simp
      also have "… = count C (Neg A)"
        unfolding ‹C = replicate_mset (Suc m) (Neg A) + C'› by simp
      finally show "count DC (Neg A) < count C (Neg A)" .
    qed
    thus ?thesis
      by (simp add: multp⇩D⇩M_imp_multp multp⇩H⇩O_imp_multp⇩D⇩M)
  qed

  with C_true have "ord_res_Interp N C ⊫ DC"
    using ord_res.entailed_clause_stays_entailed by metis

  thus "ord_res_Interp N C ⊫ C"
    unfolding true_cls_def
  proof (elim bexE)
    fix L
    assume
      L_in: "L ∈# DC" and
      L_true: "ord_res_Interp N C ⊫l L"

    from L_in have "L ∈# D' ∨ L = Neg A ∨ L ∈# C'"
      unfolding ‹DC = repeat_mset (Suc n) D' + replicate_mset (m - n) (Neg A) + C'›
      by (metis in_replicate_mset member_mset_repeat_msetD union_iff)

    moreover have "L ∉# D'"
    proof (rule notI)
      assume "L ∈# D'"

      moreover have "¬ ord_res.interp N (add_mset (Pos A) D') ⊫ add_mset (Pos A) D'"
        using D_productive[unfolded ‹D = add_mset (Pos A) D'›]
        unfolding ord_res.production_unfold
        by fast

      ultimately have "¬ ord_res.interp N (add_mset (Pos A) D') ⊫l L"
        by auto

      have "L ≺⇩l Pos A"
        using ‹D = add_mset (Pos A) D'› ‹L ∈# D'› ‹ord_res.is_strictly_maximal_lit (Pos A) D›
          linorder_lit.is_greatest_in_mset_iff by fastforce

      have "¬ ord_res_Interp N C ⊫l L"
      proof (cases L)
        case (Pos B)
        hence "B ∉ ord_res.interp N (add_mset (Pos A) D')"
          using ‹¬ ord_res.interp N (add_mset (Pos A) D') ⊫l L› by simp

        moreover have "add_mset (Pos A) D' ≺⇩c C"
          by (metis ‹D = add_mset (Pos A) D'› ‹⋀thesis. (⋀m A D' C'. ⟦n ≤ m; ord_res.is_strictly_maximal_lit (Pos A) D; ord_res.is_maximal_lit (Neg A) C; D = add_mset (Pos A) D'; C = replicate_mset (Suc m) (Neg A) + C'; Neg A ∉# C'; DC = repeat_mset (Suc n) D' + replicate_mset (m - n) (Neg A) + C'⟧ ⟹ thesis) ⟹ thesis› linorder_lit.is_maximal_in_mset_if_is_greatest_in_mset linorder_lit.multp⇩H⇩O_if_maximal_less_that_maximal multp⇩D⇩M_imp_multp multp⇩H⇩O_imp_multp⇩D⇩M ord_res.less_lit_simps(2) reflclp_iff)

        ultimately have "B ∉ ord_res.interp N C"
          using ‹L ≺⇩l Pos A›[unfolded Pos, simplified]
          using ord_res.interp_fixed_for_smaller_literals
          by (metis ‹D = add_mset (Pos A) D'› ‹ord_res.is_strictly_maximal_lit (Pos A) D›
              linorder_lit.is_maximal_in_mset_if_is_greatest_in_mset literal.sel(1))

        moreover have "B ∉ ord_res.production N C"
          by (metis Uniq_D ‹ord_res.is_maximal_lit (Neg A) C› ground_ordered_resolution_calculus.mem_productionE linorder_lit.Uniq_is_maximal_in_mset linorder_lit.is_maximal_in_mset_if_is_greatest_in_mset literal.simps(4) ord_res.ground_ordered_resolution_calculus_axioms)

        ultimately show ?thesis
          unfolding Pos by simp
      next
        case (Neg B)
        hence "B ∈ ord_res.interp N (add_mset (Pos A) D')"
          using ‹¬ ord_res.interp N (add_mset (Pos A) D') ⊫l L› by simp

        moreover have "add_mset (Pos A) D' ≺⇩c C"
          by (metis ‹D = add_mset (Pos A) D'› ‹⋀thesis. (⋀m A D' C'. ⟦n ≤ m; ord_res.is_strictly_maximal_lit (Pos A) D; ord_res.is_maximal_lit (Neg A) C; D = add_mset (Pos A) D'; C = replicate_mset (Suc m) (Neg A) + C'; Neg A ∉# C'; DC = repeat_mset (Suc n) D' + replicate_mset (m - n) (Neg A) + C'⟧ ⟹ thesis) ⟹ thesis› linorder_lit.is_maximal_in_mset_if_is_greatest_in_mset linorder_lit.multp⇩H⇩O_if_maximal_less_that_maximal multp⇩D⇩M_imp_multp multp⇩H⇩O_imp_multp⇩D⇩M ord_res.less_lit_simps(2) reflclp_iff)

        ultimately have "B ∈ ord_res.interp N C"
          by (metis Un_iff ord_res.not_interp_to_Interp_imp_le linorder_cls.leD)

        then show ?thesis
          unfolding Neg
          by simp
      qed

      with L_true show False
        by contradiction
    qed

    ultimately have "L ∈# C"
      unfolding ‹C = replicate_mset (Suc m) (Neg A) + C'› by simp

    with L_true show "∃L ∈# C. ord_res_Interp N C ⊫l L"
      by metis
  qed
qed

lemma clause_true_if_eres_true:
  assumes
    "(ground_resolution D1)⇧+⇧+ D2 C" and
    "C ≠ eres D1 C" and
    eres_C_true: "ord_res_Interp N (eres D1 C) ⊫ eres D1 C"
  shows "ord_res_Interp N C ⊫ C"
proof -
  obtain n where
    steps: "(ground_resolution D1 ^^ Suc n) D2 C"
    using ‹(ground_resolution D1)⇧+⇧+ D2 C›
    by (metis less_not_refl not0_implies_Suc tranclp_power)

  obtain m A D' C' where
    "n ≤ m" and
    "ord_res.is_strictly_maximal_lit (Pos A) D1" and
    "ord_res.is_maximal_lit (Neg A) D2" and
    "D1 = add_mset (Pos A) D'" and
    "D2 = replicate_mset (Suc m) (Neg A) + C'" and
    "Neg A ∉# C'" and
    "C = repeat_mset (Suc n) D' + replicate_mset (m - n) (Neg A) + C'"
    using relpowp_ground_resolutionD[OF Suc_not_Zero steps]
    by (metis diff_Suc_Suc Suc_le_mono)

  have "Neg A ∉# D'"
    by (metis ‹D1 = add_mset (Pos A) D'› ‹ord_res.is_strictly_maximal_lit (Pos A) D1›
        ord_res.less_lit_simps(4) linorder_lit.is_greatest_in_mset_iff linorder_trm.eq_refl
        linorder_trm.leD remove1_mset_add_mset_If)

  obtain m' C'' where
    "C = replicate_mset (Suc m') (Neg A) + C''" and
    "Neg A ∉# C''" and
    "eres D1 C = repeat_mset (Suc m') D' + C''"
    using ‹C ≠ eres D1 C› eres_not_identD
    using ‹ord_res.is_strictly_maximal_lit (Pos A) D1› linorder_lit.Uniq_is_greatest_in_mset
    using ‹D1 = add_mset (Pos A) D'›
    by (metis Uniq_D add_mset_remove_trivial literal.inject(1))

  have "m - n = Suc m'"
  proof -
    have "count C (Neg A) = count (repeat_mset (Suc n) D') (Neg A) +
              count (replicate_mset (m - n) (Neg A)) (Neg A) + count C' (Neg A)"
      using ‹C = repeat_mset (Suc n) D' + replicate_mset (m - n) (Neg A) + C'› by simp
    also have "… = count D' (Neg A) * Suc n + count {#Neg A#} (Neg A) * (m - n) +
              count C' (Neg A)"
      by simp
    also have "… = 0 * Suc n + 1 * (m - n) + 0"
      using ‹Neg A ∉# D'› ‹Neg A ∉# C'› by (simp add: count_eq_zero_iff)
    also have "… = m - n"
      by presburger
    finally have "count C (Neg A) = m - n" .

    have "count C (Neg A) = count (replicate_mset (Suc m') (Neg A)) (Neg A) +
              count C'' (Neg A)"
      using ‹C = replicate_mset (Suc m') (Neg A) + C''› by simp
    also have "… = count {#Neg A#} (Neg A) * Suc m' + count C'' (Neg A)"
      by simp
    also have "… = 1 * Suc m' + 0"
      using ‹Neg A ∉# C''› by (simp add: count_eq_zero_iff)
    also have "… = Suc m'"
      by presburger
    finally have "count C (Neg A) = Suc m'" .

    show ?thesis
      using ‹count C (Neg A) = m - n› ‹count C (Neg A) = Suc m'› by argo
  qed

  hence "C'' = repeat_mset (Suc n) D' + C'"
    using ‹C = repeat_mset (Suc n) D' + replicate_mset (m - n) (Neg A) + C'›
      ‹C = replicate_mset (Suc m') (Neg A) + C''›
    by simp

  hence eres_D1_C_eq: "eres D1 C = repeat_mset (Suc m' + Suc n) D' + C'"
    using ‹eres D1 C = repeat_mset (Suc m') D' + C''› by simp

  have "ord_res_Interp N (eres D1 C) ⊫ eres D1 C"
    using eres_C_true .

  moreover have "eres D1 C ≺⇩c C"
    using eres_le[of D1 C] ‹C ≠ eres D1 C› by order

  ultimately have "ord_res_Interp N C ⊫ eres D1 C"
    using ord_res.entailed_clause_stays_entailed by metis

  thus "ord_res_Interp N C ⊫ C"
    unfolding true_cls_def
  proof (elim bexE)
    fix L
    assume
      L_in: "L ∈# eres D1 C" and
      L_true: "ord_res_Interp N C ⊫l L"

    from L_in have "L ∈# D' ∨ L ∈# C'"
      unfolding eres_D1_C_eq
      using member_mset_repeat_msetD by fastforce
    hence "L ∈# C"
      by (auto simp: ‹C = repeat_mset (Suc n) D' + replicate_mset (m - n) (Neg A) + C'›)
    with L_true show "∃L ∈# C. ord_res_Interp N C ⊫l L"
      by metis
  qed
qed

end

end