Theory ORD_RES_5

theory ORD_RES_5
  imports
    Background
    Implicit_Exhaustive_Factorization
    Exhaustive_Resolution
begin

section ‹ORD-RES-5 (explicit model construction)›

type_synonym 'f ord_res_5 = "'f gclause fset ×'f gclause fset × 'f gclause fset ×
  ('f gterm ⇒ 'f gclause option) × 'f gclause option"

context simulation_SCLFOL_ground_ordered_resolution begin

inductive ord_res_5 where
  skip: "
    (dom ℳ) ⊫ C ⟹
    𝒞' = The_optional (linorder_cls.is_least_in_fset {|D |∈| iefac ℱ |`| (N |∪| Uer). C ≺c D|}) ⟹
    ord_res_5 N (Uer, ℱ, ℳ, Some C) (Uer, ℱ, ℳ, 𝒞')" |

  production: "
    ¬ (dom ℳ) ⊫ C ⟹
    linorder_lit.is_maximal_in_mset C L ⟹
    is_pos L ⟹
    linorder_lit.is_greatest_in_mset C L ⟹
    ℳ' = ℳ(atm_of L := Some C) ⟹
    𝒞' = The_optional (linorder_cls.is_least_in_fset {|D |∈| iefac ℱ |`| (N |∪| Uer). C ≺c D|}) ⟹
    ord_res_5 N (Uer, ℱ, ℳ, Some C) (Uer, ℱ, ℳ', 𝒞')" |

  factoring: "
    ¬ (dom ℳ) ⊫ C ⟹
    linorder_lit.is_maximal_in_mset C L ⟹
    is_pos L ⟹
    ¬ linorder_lit.is_greatest_in_mset C L ⟹
    ℱ' = finsert C ℱ ⟹
    ℳ' = (λ_. None) ⟹
    𝒞' = The_optional (linorder_cls.is_least_in_fset (iefac ℱ' |`| (N |∪| Uer))) ⟹
    ord_res_5 N (Uer, ℱ, ℳ, Some C) (Uer, ℱ', ℳ', 𝒞')" |

  resolution: "
    ¬ (dom ℳ) ⊫ C ⟹
    linorder_lit.is_maximal_in_mset C L ⟹
    is_neg L ⟹
    ℳ (atm_of L) = Some D ⟹
    Uer' = finsert (eres D C) Uer ⟹
    ℳ' = (λ_. None) ⟹
    𝒞' = The_optional (linorder_cls.is_least_in_fset (iefac ℱ |`| (N |∪| Uer'))) ⟹
    ord_res_5 N (Uer, ℱ, ℳ, Some C) (Uer', ℱ, ℳ', 𝒞')"

inductive ord_res_5_step :: "'f ord_res_5 ⇒ 'f ord_res_5 ⇒ bool" where
  "ord_res_5 N s s' ⟹ ord_res_5_step (N, s) (N, s')"

lemma tranclp_ord_res_5_step_if_tranclp_ord_res_5:
  "(ord_res_5 N)++ s s' ⟹ ord_res_5_step++ (N, s) (N, s')"
  by (induction s' rule: tranclp_induct)
   (auto intro: ord_res_5_step.intros tranclp.intros)

inductive ord_res_5_final :: "'f ord_res_5 ⇒ bool" where
  model_found:
    "ord_res_5_final (N, Uer, ℱ, ℳ, None)" |

  contradiction_found:
    "ord_res_5_final (N, Uer, ℱ, ℳ, Some {#})"

sublocale ord_res_5_semantics: semantics where
  step = ord_res_5_step and
  final = ord_res_5_final
proof unfold_locales
  fix S5 :: "'f gclause fset ×'f gclause fset × 'f gclause fset ×
    ('f gterm ⇒ 'f gclause option) × 'f gclause option"

  obtain
    N Uer ℱ :: "'f gterm clause fset" and
    ℳ :: "'f gterm ⇒ 'f gclause option" and
    𝒞 :: "'f gclause option" where
    S5_def: "S5 = (N, (Uer, ℱ, ℳ, 𝒞))"
    by (metis prod.exhaust)

  assume "ord_res_5_final S5"
  hence "𝒞 = None ∨ 𝒞 = Some {#}"
    by (simp add: S5_def ord_res_5_final.simps)
  hence "∄x. ord_res_5 N (Uer, ℱ, ℳ, 𝒞) x"
    by (auto simp: linorder_lit.is_maximal_in_mset_iff elim: ord_res_5.cases)
  thus "finished ord_res_5_step S5"
    by (simp add: S5_def finished_def ord_res_5_step.simps)
qed

lemma right_unique_ord_res_5: "right_unique (ord_res_5 N)"
proof (rule right_uniqueI)
  fix s s' s''
  assume step1: "ord_res_5 N s s'" and step2: "ord_res_5 N s s''"
  show "s' = s''"
    using step1
  proof (cases N s s' rule: ord_res_5.cases)
    case hyps1: (skip ℳ1 C1 𝒞1' ℱ1 U1er)
    with step2 show ?thesis
      by (cases N s s'' rule: ord_res_5.cases) simp_all
  next
    case hyps1: (production ℳ1 C1 L1 ℳ1' 𝒞1' ℱ1 U1er)
    show ?thesis
      using step2
    proof (cases N s s'' rule: ord_res_5.cases)
      case (skip ℳ2 C2 𝒞2' ℱ2 U2er)
      with hyps1 show ?thesis
        by simp
    next
      case hyps2: (production ℳ2 C2 L2 ℳ2' 𝒞2' ℱ2 U2er)
      have "C1 = C2"
        using hyps1 hyps2 by simp
      hence "L1 = L2"
        using hyps1 hyps2
        by (metis linorder_lit.Uniq_is_maximal_in_mset Uniq_D)
      thus ?thesis
        using hyps1 hyps2 by simp
    next
      case hyps2: (factoring ℳ2 C2 L2 ℱ2 ℱ2' ℳ2' 𝒞2' U2er)
      have "C1 = C2"
        using hyps1 hyps2 by simp
      hence "L1 = L2"
        using hyps1 hyps2
        by (metis linorder_lit.Uniq_is_maximal_in_mset Uniq_D)
      thus ?thesis
        using hyps1 hyps2 by simp
    next
      case hyps2: (resolution ℳ2 C2 L2 D2 U2er' U2er ℳ2' 𝒞2' ℱ2)
      have "C1 = C2"
        using hyps1 hyps2 by simp
      hence "L1 = L2"
        using hyps1 hyps2
        by (metis linorder_lit.Uniq_is_maximal_in_mset Uniq_D)
      thus ?thesis
        using hyps1 hyps2 by simp
    qed
  next
    case hyps1: (factoring ℳ1 C1 L1 ℱ1 ℱ1' ℳ1' 𝒞1' U1er)
    show ?thesis
      using step2
    proof (cases N s s'' rule: ord_res_5.cases)
      case (skip ℳ2 C2 𝒞2' ℱ2 U2er)
      with hyps1 show ?thesis
        by simp
    next
      case hyps2: (production ℳ2 C2 L2 ℳ2' 𝒞2' ℱ2 U2er)
      have "C1 = C2"
        using hyps1 hyps2 by simp
      hence "L1 = L2"
        using hyps1 hyps2
        by (metis linorder_lit.Uniq_is_maximal_in_mset Uniq_D)
      thus ?thesis
        using hyps1 hyps2 by simp
    next
      case hyps2: (factoring ℳ2 C2 L2 ℱ2 ℱ2' ℳ2' 𝒞2' U2er)
      have "C1 = C2"
        using hyps1 hyps2 by simp
      thus ?thesis
        using hyps1 hyps2 by simp
    next
      case hyps2: (resolution ℳ2 C2 L2 D2 U2er' U2er ℳ2' 𝒞2' ℱ2)
      have "C1 = C2"
        using hyps1 hyps2 by simp
      hence "L1 = L2"
        using hyps1 hyps2
        by (metis linorder_lit.Uniq_is_maximal_in_mset Uniq_D)
      hence False
        using hyps1 hyps2 by argo
      thus ?thesis ..
    qed
  next
    case hyps1: (resolution ℳ1 C1 L1 D1 U1er' U1er ℳ1' 𝒞1' ℱ1)
    show ?thesis
      using step2
    proof (cases N s s'' rule: ord_res_5.cases)
      case (skip ℳ2 C2 𝒞2' ℱ2 U2er)
      with hyps1 show ?thesis
        by simp
    next
      case hyps2: (production ℳ2 C2 L2 ℳ2' 𝒞2' ℱ2 U2er)
      have "C1 = C2"
        using hyps1 hyps2 by simp
      hence "L1 = L2"
        using hyps1 hyps2
        by (metis linorder_lit.Uniq_is_maximal_in_mset Uniq_D)
      thus ?thesis
        using hyps1 hyps2 by simp
    next
      case hyps2: (factoring ℳ2 C2 L2 ℱ2 ℱ2' ℳ2' 𝒞2' U2er)
      have "C1 = C2"
        using hyps1 hyps2 by simp
      hence "L1 = L2"
        using hyps1 hyps2
        by (metis Uniq_D linorder_lit.Uniq_is_maximal_in_mset)
      hence False
        using hyps1 hyps2 by argo
      thus ?thesis ..
    next
      case hyps2: (resolution ℳ2 C2 L2 D2 U2er' U2er ℳ2' 𝒞2' ℱ2)
      have "U1er = U2er" "ℱ1 = ℱ2" "ℳ1 = ℳ2" "C1 = C2"
        using hyps1 hyps2 by simp_all
      hence "L1 = L2"
        using hyps1 hyps2
        by (metis Uniq_D linorder_lit.Uniq_is_maximal_in_mset)
      hence "D1 = D2"
        using ‹ℳ1 (atm_of L1) = Some D1› ‹ℳ2 (atm_of L2) = Some D2› ‹ℳ1 = ℳ2›
        by simp

      have "U1er' = U2er'"
        using ‹U1er' = finsert (eres D1 C1) U1er› ‹U2er' = finsert (eres D2 C2) U2er›
          ‹D1 = D2› ‹C1 = C2› ‹U1er = U2er›
        by argo

      moreover have "ℳ1' = ℳ2'"
        using ‹ℳ1' = (λ_. None)› ‹ℳ2' = (λ_. None)›
        by argo

      moreover have "𝒞1' = 𝒞2'"
        using hyps1 hyps2 ‹ℱ1 = ℱ2› ‹U1er' = U2er'› by simp

      ultimately show ?thesis
        using ‹s' = (U1er', ℱ1, ℳ1', 𝒞1')› ‹s'' = (U2er', ℱ2, ℳ2', 𝒞2')›
          ‹ℱ1 = ℱ2›
        by argo
    qed
  qed
qed

lemma right_unique_ord_res_5_step: "right_unique ord_res_5_step"
proof (rule right_uniqueI)
  fix x y z
  show "ord_res_5_step x y ⟹ ord_res_5_step x z ⟹ y = z"
    using right_unique_ord_res_5[THEN right_uniqueD]
    by (elim ord_res_5_step.cases) (metis prod.inject)
qed

definition next_clause_in_factorized_clause where
  "next_clause_in_factorized_clause N s ⟷
    (∀Uer ℱ ℳ C. s = (Uer, ℱ, ℳ, Some C) ⟶ C |∈| iefac ℱ |`| (N |∪| Uer))"

lemma next_clause_in_factorized_clause:
  assumes step: "ord_res_5 N s s'"
  shows "next_clause_in_factorized_clause N s'"
  using step
proof (cases N s s' rule: ord_res_5.cases)
  case (skip ℳ C 𝒞' ℱ Uer)
  thus ?thesis
    unfolding next_clause_in_factorized_clause_def
    by (metis Pair_inject The_optional_eq_SomeD linorder_cls.is_minimal_in_fset_eq_is_least_in_fset
        linorder_cls.is_minimal_in_fset_ffilter_iff)
next
  case (production ℳ C L ℳ' 𝒞' ℱ Uer)
  thus ?thesis
    unfolding next_clause_in_factorized_clause_def
    by (metis Pair_inject The_optional_eq_SomeD linorder_cls.is_minimal_in_fset_eq_is_least_in_fset
        linorder_cls.is_minimal_in_fset_ffilter_iff)
next
  case (factoring ℳ C L ℱ' ℱ ℳ' 𝒞' Uer)
  thus ?thesis
    unfolding next_clause_in_factorized_clause_def
    by (metis Pair_inject The_optional_eq_SomeD linorder_cls.is_least_in_fset_iff)
next
  case (resolution ℳ C L D Uer' Uer ℳ' 𝒞' ℱ)
  thus ?thesis
    unfolding next_clause_in_factorized_clause_def
    by (metis Pair_inject The_optional_eq_SomeD linorder_cls.is_least_in_fset_iff)
qed

definition implicitly_factorized_clauses_subset where
  "implicitly_factorized_clauses_subset N s ⟷
    (∀Uer ℱ ℳ 𝒞. s = (Uer, ℱ, ℳ, 𝒞) ⟶ ℱ |⊆| N |∪| Uer)"

lemma ord_res_5_preserves_implicitly_factorized_clauses_subset:
  assumes
    step: "ord_res_5 N s s'" and
    invars:
      "implicitly_factorized_clauses_subset N s" and
      "next_clause_in_factorized_clause N s"
  shows "implicitly_factorized_clauses_subset N s'"
  using step
proof (cases N s s' rule: ord_res_5.cases)
  case (skip ℳ C 𝒞' ℱ Uer)
  thus ?thesis
    using invars
    by (simp add: implicitly_factorized_clauses_subset_def)
next
  case (production ℳ C L ℳ' 𝒞' ℱ Uer)
  thus ?thesis
    using invars
    by (simp add: implicitly_factorized_clauses_subset_def)
next
  case (factoring ℳ C L ℱ' ℱ ℳ' 𝒞' Uer)
  thus ?thesis
    using invars
    by (smt (verit) Pair_inject assms(3) fimage_iff finsert_fsubset iefac_def
        implicitly_factorized_clauses_subset_def literal.collapse(1)
        next_clause_in_factorized_clause_def ex1_efac_eq_factoring_chain ex_ground_factoringI)
next
  case (resolution ℳ C L D Uer' Uer ℳ' 𝒞' ℱ)
  thus ?thesis
    using invars
    by (simp add: fsubset_funion_eq implicitly_factorized_clauses_subset_def)
qed

lemma interp_eq_Interp_if_least_greater:
  assumes
    C_in: "C |∈| NN" and
    D_least_gt_C: "linorder_cls.is_least_in_fset (ffilter ((≺c) C) NN) D"
  shows "ord_res.interp (fset NN) D = ord_res.interp (fset NN) C ∪ ord_res.production (fset NN) C"
proof -
  have nex_between_C_and_D: "¬ (∃CD |∈| NN. C ≺c CD ∧ CD ≺c D)"
    using D_least_gt_C
    unfolding linorder_cls.is_least_in_ffilter_iff by auto

  have "ord_res.interp (fset NN) D = ord_res.interp (fset {|B |∈| NN. B ≼c C|}) D"
  proof (rule ord_res.interp_swap_clause_set)
    have "NN = {|B |∈| NN. B ≼c C|} |∪| {|E |∈| NN. D ≼c E|}"
      using nex_between_C_and_D by force
    show "{Da. Da |∈| NN ∧ Da ≺c D} = {Da. Da |∈| {|B |∈| NN. (≺c)== B C|} ∧ Da ≺c D}"
      using ‹NN = {|B |∈| NN. (≺c)== B C|} |∪| ffilter ((≺c)== D) NN› linorder_cls.leD by auto
  qed

  also have "… = ⋃ (ord_res.production (fset {|B |∈| NN. (≺c)== B C|}) `
    {Da. Da |∈| {|B |∈| NN. (≺c)== B C|} ∧ Da ≺c D})"
    unfolding ord_res.interp_def ..

  also have "… = ⋃ (ord_res.production (fset {|B |∈| NN. (≺c)== B C|}) `
    {Da ∈ fset NN. (≺c)== Da C ∧ Da ≺c D})"
    by auto

  also have "… = ⋃ (ord_res.production (fset {|B |∈| NN. (≺c)== B C|}) `
    {Da ∈ fset NN. (≺c)== Da C})"
  proof -
    have "{|Da |∈| NN. Da ≼c C ∧ Da ≺c D|} = {|Da |∈| NN. Da ≼c C|}"
      using nex_between_C_and_D
      by (metis (no_types, opaque_lifting) D_least_gt_C linorder_cls.is_least_in_fset_ffilterD(2)
          linorder_cls.le_less_trans)
    thus ?thesis
      by fastforce
  qed

  also have "… = ⋃ (ord_res.production (fset {|B |∈| NN. (≺c)== B C|}) `
    {Da ∈ fset NN. Da ≺c C}) ∪ ord_res.production (fset {|B |∈| NN. (≺c)== B C|}) C"
  proof -
    have "{Da. Da |∈| NN ∧ (≺c)== Da C} = insert C {Da. Da |∈| NN ∧ Da ≺c C}"
      using C_in by auto
    thus ?thesis
      by blast
  qed

  also have "… = ord_res_Interp (fset {|B |∈| NN. (≺c)== B C|}) C"
    unfolding ord_res.interp_def by auto

  also have "… = ord_res_Interp (fset NN) C"
  proof -
    have "ord_res.interp (fset {|B |∈| NN. (≺c)== B C|}) C = ord_res.interp (fset NN) C"
      using ord_res.interp_swap_clause_set[of "fset {|B |∈| NN. (≺c)== B C|}" C "fset NN"]
      by auto

    moreover have "ord_res.production (fset {|B |∈| NN. (≺c)== B C|}) C = ord_res.production (fset NN) C"
      using ord_res.production_swap_clause_set[of "fset {|B |∈| NN. (≺c)== B C|}" C "fset NN"]
      by auto

    ultimately show ?thesis
      by simp
  qed

  finally show ?thesis .
qed

lemma interp_eq_empty_if_least_in_set:
  assumes "linorder_cls.is_least_in_set N C"
  shows "ord_res.interp N C = {}"
  using assms
  unfolding ord_res.interp_def
  unfolding linorder_cls.is_least_in_set_iff
  by auto

definition model_eq_interp_upto_next_clause where
  "model_eq_interp_upto_next_clause N s ⟷
    (∀Uer ℱ ℳ C. s = (Uer, ℱ, ℳ, Some C) ⟶
      dom ℳ = ord_res.interp (fset (iefac ℱ |`| (N |∪| Uer))) C)"

lemma model_eq_interp_upto_next_clause:
  assumes step: "ord_res_5 N s s'" and
    invars:
      "model_eq_interp_upto_next_clause N s"
      "next_clause_in_factorized_clause N s"
  shows "model_eq_interp_upto_next_clause N s'"
  using step
proof (cases N s s' rule: ord_res_5.cases)
  case step_hyps: (skip ℳ C 𝒞' ℱ Uer)

  have "dom ℳ = ord_res.interp (fset (iefac ℱ |`| (N |∪| Uer))) D" if "𝒞' = Some D" for D
  proof -
    have "dom ℳ = ord_res.interp (fset (iefac ℱ |`| (N |∪| Uer))) C"
      using invars(1)[unfolded model_eq_interp_upto_next_clause_def, rule_format,
          OF ‹s = (Uer, ℱ, ℳ, Some C)›] .

    also have "… = ord_res_Interp (fset (iefac ℱ |`| (N |∪| Uer))) C"
    proof -
      have "ord_res.production (fset (iefac ℱ |`| (N |∪| Uer))) C = {}"
        using ‹dom ℳ ⊫ C›
        unfolding invars(1)[unfolded model_eq_interp_upto_next_clause_def, rule_format,
            OF ‹s = (Uer, ℱ, ℳ, Some C)›]
        by (simp add: ord_res.production_unfold)
      thus ?thesis
        by simp
    qed

    also have "… = ord_res.interp (fset (iefac ℱ |`| (N |∪| Uer))) D"
    proof (rule interp_eq_Interp_if_least_greater[symmetric])
      show "C |∈| iefac ℱ |`| (N |∪| Uer)"
        using invars(2)[unfolded next_clause_in_factorized_clause_def, rule_format,
            OF ‹s = (Uer, ℱ, ℳ, Some C)›] .
    next
      show "linorder_cls.is_least_in_fset (ffilter ((≺c) C) (iefac ℱ |`| (N |∪| Uer))) D"
        using step_hyps(3-) that by (metis Some_eq_The_optionalD)
    qed

    finally show ?thesis .
  qed

  thus ?thesis
    using step_hyps by (simp add: model_eq_interp_upto_next_clause_def)
next
  case step_hyps: (production ℳ C L ℳ' 𝒞' ℱ Uer)

  have "dom ℳ' = ord_res.interp (fset (iefac ℱ |`| (N |∪| Uer))) D" if "𝒞' = Some D" for D
  proof -
    have "dom ℳ' = dom ℳ ∪ {atm_of L}"
      unfolding ‹ℳ' = ℳ(atm_of L ↦ C)› by simp

    also have "… = ord_res.interp (fset (iefac ℱ |`| (N |∪| Uer))) C ∪ {atm_of L}"
      unfolding invars(1)[unfolded model_eq_interp_upto_next_clause_def, rule_format,
          OF ‹s = (Uer, ℱ, ℳ, Some C)›] ..

    also have "… = ord_res.interp (fset (iefac ℱ |`| (N |∪| Uer))) C ∪
      ord_res.production (fset (iefac ℱ |`| (N |∪| Uer))) C"
    proof -
      have "¬ ord_res.interp (fset (iefac ℱ |`| (N |∪| Uer))) C ⊫ C"
        using ‹¬ dom ℳ ⊫ C›
        unfolding invars(1)[unfolded model_eq_interp_upto_next_clause_def, rule_format,
            OF ‹s = (Uer, ℱ, ℳ, Some C)›] .
      hence "atm_of L ∈ ord_res.production (fset (iefac ℱ |`| (N |∪| Uer))) C"
        using ‹is_pos L› ‹ord_res.is_strictly_maximal_lit L C›
        using invars(2)[unfolded next_clause_in_factorized_clause_def, rule_format,
            OF ‹s = (Uer, ℱ, ℳ, Some C)›]
        unfolding ord_res.production_unfold mem_Collect_eq
        by (metis linorder_lit.is_greatest_in_mset_iff literal.collapse(1) multi_member_split)
      hence "ord_res.production (fset (iefac ℱ |`| (N |∪| Uer))) C = {atm_of L}"
        by (metis empty_iff insertE ord_res.production_eq_empty_or_singleton)
      thus ?thesis
        by argo
    qed

    also have "… = ord_res.interp (fset (iefac ℱ |`| (N |∪| Uer))) D"
    proof (rule interp_eq_Interp_if_least_greater[symmetric])
      show "C |∈| iefac ℱ |`| (N |∪| Uer)"
        using invars(2)[unfolded next_clause_in_factorized_clause_def, rule_format,
            OF ‹s = (Uer, ℱ, ℳ, Some C)›] .
    next
      show "linorder_cls.is_least_in_fset (ffilter ((≺c) C) (iefac ℱ |`| (N |∪| Uer))) D"
        using step_hyps(3-) that by (metis Some_eq_The_optionalD)
    qed

    finally show ?thesis .
  qed

  thus ?thesis
    using step_hyps by (simp add: model_eq_interp_upto_next_clause_def)
next
  case step_hyps: (factoring ℳ C L ℱ' ℱ ℳ' 𝒞' Uer)

  have "dom ℳ' = ord_res.interp (fset (iefac ℱ' |`| (N |∪| Uer))) D" if "𝒞' = Some D" for D
  proof -
    have "dom ℳ' = {}"
      using step_hyps(3-) by simp
    also have "… = ord_res.interp (fset (iefac ℱ' |`| (N |∪| Uer))) D"
    proof (rule interp_eq_empty_if_least_in_set[symmetric])
      show "linorder_cls.is_least_in_set (fset (iefac ℱ' |`| (N |∪| Uer))) D"
        using step_hyps(3-) that
        by (metis Some_eq_The_optionalD linorder_cls.is_least_in_fset_iff
            linorder_cls.is_least_in_set_iff)
    qed
    finally show ?thesis .
  qed

  thus ?thesis
    using step_hyps by (simp add: model_eq_interp_upto_next_clause_def)
next
  case step_hyps: (resolution ℳ C L D Uer' Uer ℳ' 𝒞' ℱ)

  have "dom ℳ' = ord_res.interp (fset (iefac ℱ |`| (N |∪| Uer'))) D" if "𝒞' = Some D" for D
  proof -
    have "dom ℳ' = {}"
      using step_hyps(3-) by simp
    also have "… = ord_res.interp (fset (iefac ℱ |`| (N |∪| Uer'))) D"
    proof (rule interp_eq_empty_if_least_in_set[symmetric])
      show "linorder_cls.is_least_in_set (fset (iefac ℱ |`| (N |∪| Uer'))) D"
        using step_hyps(3-) that
        by (metis Some_eq_The_optionalD linorder_cls.is_least_in_fset_iff
            linorder_cls.is_least_in_set_iff)
    qed
    finally show ?thesis .
  qed

  thus ?thesis
    using step_hyps by (simp add: model_eq_interp_upto_next_clause_def)
qed

definition all_smaller_clauses_true_wrt_respective_Interp where
  "all_smaller_clauses_true_wrt_respective_Interp N s ⟷
    (∀Uer ℱ ℳ 𝒞. s = (Uer, ℱ, ℳ, 𝒞) ⟶
      (∀C |∈| iefac ℱ |`| (N |∪| Uer). (∀D. 𝒞 = Some D ⟶ C ≺c D) ⟶
        ord_res_Interp (fset (iefac ℱ |`| (N |∪| Uer))) C ⊫ C))"

lemma all_smaller_clauses_true_wrt_respective_Interp:
  assumes step: "ord_res_5 N s s'" and
    invars:
      "all_smaller_clauses_true_wrt_respective_Interp N s"
      "model_eq_interp_upto_next_clause N s"
      "next_clause_in_factorized_clause N s"
  shows "all_smaller_clauses_true_wrt_respective_Interp N s'"
  using step
proof (cases N s s' rule: ord_res_5.cases)
  case step_hyps: (skip ℳ D 𝒞' ℱ Uer)

  have D_true: "ord_res_Interp (fset (iefac ℱ |`| (N |∪| Uer))) D ⊫ D"
    using invars(2) ord_res.production_unfold step_hyps(1) step_hyps(3)
    by (auto simp: model_eq_interp_upto_next_clause_def)

  have "ord_res_Interp (fset (iefac ℱ |`| (N |∪| Uer))) C ⊫ C"
    if "𝒞' = Some E" and C_in: "C |∈| iefac ℱ |`| (N |∪| Uer)" and "C ≺c E" for C E
  proof -
    have "linorder_cls.is_least_in_fset (ffilter ((≺c) D) (iefac ℱ |`| (N |∪| Uer))) E"
      using step_hyps ‹𝒞' = Some E› by (metis Some_eq_The_optionalD)
    hence "C ≼c D"
      using C_in ‹C ≺c E›
      by (metis asympD linorder_cls.is_least_in_ffilter_iff linorder_cls.le_less_linear
          ord_res.asymp_less_cls)
    thus ?thesis
      using D_true
      using invars(1)[unfolded all_smaller_clauses_true_wrt_respective_Interp_def, rule_format,
          OF ‹s = (Uer, ℱ, ℳ, Some D)› C_in] by auto
  qed

  moreover have "ord_res_Interp (fset (iefac ℱ |`| (N |∪| Uer))) C ⊫ C"
    if "𝒞' = None" and C_in: "C |∈| iefac ℱ |`| (N |∪| Uer)" for C
  proof -
    have "∄x. linorder_cls.is_least_in_fset (ffilter ((≺c) D) (iefac ℱ |`| (N |∪| Uer))) x"
      using step_hyps ‹𝒞' = None›
      by (metis (no_types, opaque_lifting) None_eq_The_optionalD linorder_cls.Uniq_is_least_in_fset
          the1_equality')
    hence "¬ (∃x |∈| iefac ℱ |`| (N |∪| Uer). D ≺c x)"
      by (metis femptyE ffmember_filter linorder_cls.ex1_least_in_fset)
    hence "C ≺c D ∨ C = D"
      using C_in by force
    thus ?thesis
    proof (elim disjE)
      assume "C ≺c D"
      then show ?thesis
        using invars(1) ‹s = (Uer, ℱ, ℳ, Some D)› C_in
        by (auto simp: all_smaller_clauses_true_wrt_respective_Interp_def)
    next
      assume "C = D"
      then show ?thesis
        using D_true by argo
    qed
  qed

  ultimately show ?thesis
    using step_hyps
    by (smt (verit, best) all_smaller_clauses_true_wrt_respective_Interp_def old.prod.inject option.exhaust)
next
  case step_hyps: (production ℳ D K ℳ' 𝒞' ℱ Uer)

  have "K ∈# D"
    using step_hyps(3-) by (metis linorder_lit.is_greatest_in_mset_iff)

  have "¬ ord_res.interp (fset (iefac ℱ |`| (N |∪| Uer))) D ⊫ D"
    using ‹¬ dom ℳ ⊫ D›
    unfolding invars(2)[unfolded model_eq_interp_upto_next_clause_def, rule_format,
        OF ‹s = (Uer, ℱ, ℳ, Some D)›] .
  hence "atm_of K ∈ ord_res.production (fset (iefac ℱ |`| (N |∪| Uer))) D"
    using ‹is_pos K› ‹ord_res.is_strictly_maximal_lit K D› ‹K ∈# D›
    using invars(3)[unfolded next_clause_in_factorized_clause_def, rule_format,
        OF ‹s = (Uer, ℱ, ℳ, Some D)›]
    unfolding ord_res.production_unfold mem_Collect_eq
    by (metis literal.collapse(1) multi_member_split)
  hence prod_D_eq: "ord_res.production (fset (iefac ℱ |`| (N |∪| Uer))) D = {atm_of K}"
    by (metis empty_iff insertE ord_res.production_eq_empty_or_singleton)
  hence "ord_res_Interp (fset (iefac ℱ |`| (N |∪| Uer))) D ⊫l K"
    using ‹is_pos K› by force
  hence D_true: "ord_res_Interp (fset (iefac ℱ |`| (N |∪| Uer))) D ⊫ D"
    using ‹K ∈# D› by auto

  have "dom ℳ' = dom ℳ ∪ {atm_of K}"
    unfolding ‹ℳ' = ℳ(atm_of K ↦ D)› by simp

  also have "… = ord_res.interp (fset (iefac ℱ |`| (N |∪| Uer))) D ∪ {atm_of K}"
    unfolding invars(2)[unfolded model_eq_interp_upto_next_clause_def, rule_format,
        OF ‹s = (Uer, ℱ, ℳ, Some D)›] ..

  also have "… = ord_res.interp (fset (iefac ℱ |`| (N |∪| Uer))) D ∪
      ord_res.production (fset (iefac ℱ |`| (N |∪| Uer))) D"
    using prod_D_eq by argo

  finally have dom_ℳ'_eq: "dom ℳ' = ord_res_Interp (fset (iefac ℱ |`| (N |∪| Uer))) D" .

  have "ord_res_Interp (fset (iefac ℱ |`| (N |∪| Uer))) C ⊫ C"
    if "𝒞' = Some E" and C_in: "C |∈| iefac ℱ |`| (N |∪| Uer)" and "C ≺c E" for C E
  proof -
    have "linorder_cls.is_least_in_fset (ffilter ((≺c) D) (iefac ℱ |`| (N |∪| Uer))) E"
      using step_hyps ‹𝒞' = Some E› by (metis Some_eq_The_optionalD)
    hence "C ≼c D"
      using C_in ‹C ≺c E›
      by (metis asympD linorder_cls.is_least_in_ffilter_iff linorder_cls.le_less_linear
          ord_res.asymp_less_cls)
    thus ?thesis
      using D_true
      using invars(1)[unfolded all_smaller_clauses_true_wrt_respective_Interp_def, rule_format,
          OF ‹s = (Uer, ℱ, ℳ, Some D)› C_in] by auto
  qed

  moreover have "ord_res_Interp (fset (iefac ℱ |`| (N |∪| Uer))) C ⊫ C"
    if "𝒞' = None" and C_in: "C |∈| iefac ℱ |`| (N |∪| Uer)" for C
  proof -
    have "∄x. linorder_cls.is_least_in_fset (ffilter ((≺c) D) (iefac ℱ |`| (N |∪| Uer))) x"
      using step_hyps ‹𝒞' = None›
      by (metis (no_types, opaque_lifting) None_eq_The_optionalD linorder_cls.Uniq_is_least_in_fset
          the1_equality')
    hence "¬ (∃x |∈| iefac ℱ |`| (N |∪| Uer). D ≺c x)"
      by (metis femptyE ffmember_filter linorder_cls.ex1_least_in_fset)
    hence "C ≺c D ∨ C = D"
      using C_in by force
    thus ?thesis
    proof (elim disjE)
      assume "C ≺c D"
      then show ?thesis
        using invars(1) ‹s = (Uer, ℱ, ℳ, Some D)› C_in
        by (auto simp: all_smaller_clauses_true_wrt_respective_Interp_def)
    next
      assume "C = D"
      thus ?thesis
        using D_true by argo
    qed
  qed

  ultimately show ?thesis
    unfolding step_hyps(2) all_smaller_clauses_true_wrt_respective_Interp_def
    by (metis prod.inject option.exhaust)
next
  case step_hyps: (factoring ℳ D K ℱ' ℱ ℳ' 𝒞' Uer)
  have "D |∈| iefac ℱ |`| (N |∪| Uer)"
    using invars(2-) ‹s = (Uer, ℱ, ℳ, Some D)›
    by (metis next_clause_in_factorized_clause_def)
  hence "D |∈| N |∪| Uer"
    using step_hyps(3-)
    by (smt (verit, ccfv_threshold) fimage_iff iefac_def literal.collapse(1)
        ex1_efac_eq_factoring_chain ex_ground_factoringI)
  hence "iefac ℱ' D |∈| iefac ℱ' |`| (N |∪| Uer)"
    unfolding ‹ℱ' = finsert D ℱ› by simp
  hence "𝒞' ≠ None"
    using step_hyps(3-)
    by (metis The_optional_eq_NoneD finsert_not_fempty linorder_cls.ex1_least_in_fset set_finsert)
  then obtain E where
    "𝒞' = Some E"
    by auto

  have "¬ (∃C |∈| iefac ℱ' |`| (N |∪| Uer). C ≺c E)"
    using ‹𝒞' = Some E› step_hyps(9)
    by (metis The_optional_eq_SomeD linorder_cls.is_least_in_fset_iff
        linorder_cls.less_imp_not_less)

  thus ?thesis
    unfolding step_hyps(1,2) all_smaller_clauses_true_wrt_respective_Interp_def
    using ‹𝒞' = Some E› by simp
next
  case step_hyps: (resolution ℳ C L D Uer' Uer ℳ' 𝒞' ℱ)
  hence "eres D C |∈| N |∪| Uer'"
    by simp
  hence "iefac ℱ (eres D C) |∈| iefac ℱ |`| (N |∪| Uer')"
    by simp
  hence "𝒞' ≠ None"
    using step_hyps(3-)
    by (metis The_optional_eq_NoneD finsert_not_fempty linorder_cls.ex1_least_in_fset set_finsert)
  then obtain E where
    "𝒞' = Some E"
    by auto

  have "¬ (∃C |∈| iefac ℱ |`| (N |∪| Uer'). C ≺c E)"
    using ‹𝒞' = Some E› step_hyps(9)
    by (metis The_optional_eq_SomeD linorder_cls.is_least_in_fset_iff
        linorder_cls.less_imp_not_less)

  thus ?thesis
    unfolding step_hyps(1,2) all_smaller_clauses_true_wrt_respective_Interp_def
    using ‹𝒞' = Some E› by simp
qed

lemma all_smaller_clauses_true_wrt_model:
  assumes
    invars:
      "all_smaller_clauses_true_wrt_respective_Interp N s"
      "model_eq_interp_upto_next_clause N s"
  shows "∀Uer ℱ ℳ D. s = (Uer, ℱ, ℳ, Some D) ⟶
    (∀C |∈| iefac ℱ |`| (N |∪| Uer). C ≺c D ⟶ dom ℳ ⊫ C)"
proof (intro allI impI ballI)
  fix Uer ℱ ℳ D C
  assume
    s_def: "s = (Uer, ℱ, ℳ, Some D)" and
    C_in: "C |∈| iefac ℱ |`| (N |∪| Uer)" and
    C_lt: "C ≺c D"

  hence C_true: "ord_res_Interp (fset (iefac ℱ |`| (N |∪| Uer))) C ⊫ C"
    using invars(1)[unfolded all_smaller_clauses_true_wrt_respective_Interp_def s_def]
    by auto

  moreover have "dom ℳ = ord_res.interp (fset (iefac ℱ |`| (N |∪| Uer))) D"
    using invars(2) s_def by (metis model_eq_interp_upto_next_clause_def)

  ultimately show "dom ℳ ⊫ C"
    using ord_res.entailed_clause_stays_entailed' C_lt by metis
qed

definition model_eq_sublocale where
  "model_eq_sublocale N s ⟷
    (∀Uer ℱ ℳ. s = (Uer, ℱ, ℳ, None) ⟶
      (let NN = fset (iefac ℱ |`| (N |∪| Uer)) in dom ℳ = ⋃ (ord_res.production NN ` NN)))"

lemma all_smaller_clauses_true_wrt_model_strong:
  assumes
    invars:
      "all_smaller_clauses_true_wrt_respective_Interp N s"
      "model_eq_interp_upto_next_clause N s"
      "model_eq_sublocale N s"
  shows "∀Uer ℱ ℳ 𝒞. s = (Uer, ℱ, ℳ, 𝒞) ⟶
    (∀C |∈| iefac ℱ |`| (N |∪| Uer). (∀D. 𝒞 = Some D ⟶ C ≺c D) ⟶ dom ℳ ⊫ C)"
proof (intro allI impI ballI)
  fix Uer ℱ ℳ 𝒞 C
  assume
    s_def: "s = (Uer, ℱ, ℳ, 𝒞)" and
    C_in: "C |∈| iefac ℱ |`| (N |∪| Uer)" and
    C_lt: "∀D. 𝒞 = Some D ⟶ C ≺c D"
  hence C_true: "ord_res_Interp (fset (iefac ℱ |`| (N |∪| Uer))) C ⊫ C"
    using invars(1) by (metis all_smaller_clauses_true_wrt_respective_Interp_def)

  show "dom ℳ ⊫ C"
  proof (cases 𝒞)
    case 𝒞_def: None
    have "let NN = fset (iefac ℱ |`| (N |∪| Uer)) in dom ℳ = ⋃ (ord_res.production NN ` NN)"
      using invars(3) s_def 𝒞_def
      by (metis model_eq_sublocale_def)
    then show ?thesis
      using C_true
      by (smt (verit, ccfv_SIG) C_in UN_I insertCI linorder_lit.is_greatest_in_mset_iff
          ord_res.lift_entailment_to_Union ord_res.mem_productionE
          ord_res.production_eq_empty_or_singleton pos_literal_in_imp_true_cls
          sup_bot.right_neutral)
  next
    case 𝒞_def: (Some D)
    have "C ≺c D"
      using C_lt 𝒞_def by metis
    moreover have "dom ℳ = ord_res.interp (fset (iefac ℱ |`| (N |∪| Uer))) D"
      using invars(2) s_def 𝒞_def by (metis model_eq_interp_upto_next_clause_def)
    ultimately show ?thesis
      using ord_res.entailed_clause_stays_entailed' C_true by metis
  qed
qed

lemma next_clause_lt_least_false_clause:
  assumes
    invars:
      "all_smaller_clauses_true_wrt_respective_Interp N s"
      "model_eq_interp_upto_next_clause N s"
  shows "∀Uer ℱ ℳ C. s = (Uer, ℱ, ℳ, Some C) ⟶
    (∀D. is_least_false_clause (iefac ℱ |`| (N |∪| Uer)) D ⟶ C ≼c D)"
proof (intro allI impI ballI)
  fix Uer ℱ ℳ C D
  assume
    s_def: "s = (Uer, ℱ, ℳ, Some C)" and
    D_least_false: "is_least_false_clause (iefac ℱ |`| (N |∪| Uer)) D"
  then show "C ≼c D"
    using invars[unfolded model_eq_interp_upto_next_clause_def
        all_smaller_clauses_true_wrt_respective_Interp_def, rule_format, OF s_def, simplified]
    by (metis (no_types, lifting) fimage.rep_eq is_least_false_clause_def
        linorder_cls.is_least_in_fset_ffilterD(1) linorder_cls.is_least_in_fset_ffilterD(2)
        linorder_cls.le_less_linear sup_fset.rep_eq)
qed

definition atoms_in_model_were_produced where
  "atoms_in_model_were_produced N s ⟷
    (∀Uer ℱ ℳ 𝒞. s = (Uer, ℱ, ℳ, 𝒞) ⟶ (∀A C. ℳ A = Some C ⟶
      A ∈ ord_res.production (fset (iefac ℱ |`| (N |∪| Uer))) C))"

lemma atoms_in_model_were_produced:
  assumes step: "ord_res_5 N s s'" and
    invars:
      "atoms_in_model_were_produced N s"
      "model_eq_interp_upto_next_clause N s"
      "next_clause_in_factorized_clause N s"
  shows "atoms_in_model_were_produced N s'"
  using step
proof (cases N s s' rule: ord_res_5.cases)
  case (skip ℳ C 𝒞' ℱ Uer)
  thus ?thesis
    using invars(1) by (simp add: atoms_in_model_were_produced_def)
next
  case (production ℳ C L ℳ' 𝒞' ℱ Uer)
  obtain A where "L = Pos A"
    using ‹is_pos L› by (cases L) simp_all

  have "atm_of L ∈ ord_res.production (fset (iefac ℱ |`| (N |∪| Uer))) C"
    unfolding ord_res.production_unfold mem_Collect_eq
  proof (intro exI conjI)
    show "atm_of L = A"
      unfolding ‹L = Pos A› literal.sel ..
  next
    show "C |∈| iefac ℱ |`| (N |∪| Uer)"
      using invars(3)[unfolded next_clause_in_factorized_clause_def, rule_format,
          OF ‹s = (Uer, ℱ, ℳ, Some C)›] .
  next
    have "L ∈# C"
      using ‹linorder_lit.is_maximal_in_mset C L›
      unfolding linorder_lit.is_maximal_in_mset_iff ..
    thus "C = add_mset (Pos A) (C - {#Pos A#})"
      unfolding ‹L = Pos A› by simp
  next
    show "ord_res.is_strictly_maximal_lit (Pos A) C"
      using ‹ord_res.is_strictly_maximal_lit L C›
      unfolding ‹L = Pos A› .
  next
    show "¬ ord_res.interp (fset (iefac ℱ |`| (N |∪| Uer))) C ⊫ C"
      using ‹¬ dom ℳ ⊫ C›
      unfolding invars(2)[unfolded model_eq_interp_upto_next_clause_def, rule_format,
          OF ‹s = (Uer, ℱ, ℳ, Some C)›] .
  qed simp_all

  thus ?thesis
    using invars(1)
    by (simp add: atoms_in_model_were_produced_def
        ‹s = (Uer, ℱ, ℳ, Some C)› ‹s' = (Uer, ℱ, ℳ', 𝒞')› ‹ℳ' = ℳ(atm_of L ↦ C)›)
qed (simp_all add: atoms_in_model_were_produced_def)

definition all_produced_atoms_in_model where
  "all_produced_atoms_in_model N s ⟷
    (∀Uer ℱ ℳ D. s = (Uer, ℱ, ℳ, Some D) ⟶ (∀C A. C ≺c D ⟶
      A ∈ ord_res.production (fset (iefac ℱ |`| (N |∪| Uer))) C ⟶ ℳ A = Some C))"

lemma all_produced_atoms_in_model:
  assumes step: "ord_res_5 N s s'" and
    invars:
      "all_produced_atoms_in_model N s"
      "model_eq_interp_upto_next_clause N s"
      "next_clause_in_factorized_clause N s"
  shows "all_produced_atoms_in_model N s'"
  using step
proof (cases N s s' rule: ord_res_5.cases)
  case (skip ℳ C 𝒞' ℱ Uer)
  have "ord_res.production (fset (iefac ℱ |`| (N |∪| Uer))) C = {}"
    using invars
    by (metis ex_in_conv model_eq_interp_upto_next_clause_def local.skip(1) local.skip(3)
        ord_res.mem_productionE)
  thus ?thesis
    using invars(1) ‹s = (Uer, ℱ, ℳ, Some C)›
    unfolding all_produced_atoms_in_model_def
    by (smt (verit, del_insts) Pair_inject The_optional_eq_SomeD empty_iff
        linorder_cls.is_least_in_ffilter_iff linorder_cls.not_less_iff_gr_or_eq local.skip(2)
        local.skip(4) ord_res.mem_productionE)
next
  case step_hyps: (production ℳ C L ℳ' 𝒞' ℱ Uer)
  obtain A where "L = Pos A"
    using ‹is_pos L› by (cases L) simp_all

  have "atm_of L ∈ ord_res.production (fset (iefac ℱ |`| (N |∪| Uer))) C"
    unfolding ord_res.production_unfold mem_Collect_eq
  proof (intro exI conjI)
    show "atm_of L = A"
      unfolding ‹L = Pos A› literal.sel ..
  next
    show "C |∈| iefac ℱ |`| (N |∪| Uer)"
      using invars ‹s = (Uer, ℱ, ℳ, Some C)› by (metis next_clause_in_factorized_clause_def)
  next
    have "L ∈# C"
      using ‹linorder_lit.is_maximal_in_mset C L›
      unfolding linorder_lit.is_maximal_in_mset_iff ..
    thus "C = add_mset (Pos A) (C - {#Pos A#})"
      unfolding ‹L = Pos A› by simp
  next
    show "ord_res.is_strictly_maximal_lit (Pos A) C"
      using ‹ord_res.is_strictly_maximal_lit L C›
      unfolding ‹L = Pos A› .
  next
    show "¬ ord_res.interp (fset (iefac ℱ |`| (N |∪| Uer))) C ⊫ C"
      using ‹¬ dom ℳ ⊫ C›
      using invars ‹s = (Uer, ℱ, ℳ, Some C)› by (metis model_eq_interp_upto_next_clause_def)
  qed simp_all

  thus ?thesis
    using invars ‹s = (Uer, ℱ, ℳ, Some C)›
    unfolding all_produced_atoms_in_model_def
    using ‹s' = (Uer, ℱ, ℳ', 𝒞')› ‹ℳ' = ℳ(atm_of L ↦ C)›
    using prod.inject
    by (smt (verit, del_insts) Some_eq_The_optionalD asympD ord_res.mem_productionE
        linorder_cls.antisym_conv3 linorder_cls.is_least_in_ffilter_iff
        linorder_trm.not_less_iff_gr_or_eq step_hyps(8) map_upd_Some_unfold
        ord_res.asymp_less_cls ord_res.less_trm_iff_less_cls_if_mem_production)
next
  case step_hyps: (factoring ℳ C L ℱ' ℱ ℳ' 𝒞' Uer)
  have "¬ (∃C |∈| iefac ℱ' |`| (N |∪| Uer). C ≺c D)" if "𝒞' = Some D" for D
  proof (rule nbex_less_than_least_in_fset)
    show "linorder_cls.is_least_in_fset (iefac ℱ' |`| (N |∪| Uer)) D"
      using step_hyps that by (metis The_optional_eq_SomeD)
  qed
  thus ?thesis
    unfolding all_produced_atoms_in_model_def
    by (metis step_hyps(2) ord_res.mem_productionE prod.inject)
next
  case step_hyps: (resolution ℳ C L D Uer' Uer ℳ' 𝒞' ℱ)
  have "¬ (∃C |∈| iefac ℱ |`| (N |∪| Uer'). C ≺c D)" if "𝒞' = Some D" for D
  proof (rule nbex_less_than_least_in_fset)
    show "linorder_cls.is_least_in_fset (iefac ℱ |`| (N |∪| Uer')) D"
      using step_hyps that by (metis The_optional_eq_SomeD)
  qed
  thus ?thesis
    unfolding all_produced_atoms_in_model_def
    by (metis step_hyps(2) ord_res.mem_productionE prod.inject)
qed


definition ord_res_5_invars where
  "ord_res_5_invars N s ⟷
    next_clause_in_factorized_clause N s ∧
    implicitly_factorized_clauses_subset N s ∧
    model_eq_interp_upto_next_clause N s ∧
    all_smaller_clauses_true_wrt_respective_Interp N s ∧
    atoms_in_model_were_produced N s ∧
    all_produced_atoms_in_model N s"

lemma ord_res_5_invars_initial_state:
  assumes
    ℱ_subset: "ℱ |⊆| N |∪| Uer" and
    C_least: "linorder_cls.is_least_in_fset (iefac ℱ |`| (N |∪| Uer)) C"
  shows "ord_res_5_invars N (Uer, ℱ, Map.empty, Some C)"
  unfolding ord_res_5_invars_def
proof (intro conjI)
  show "next_clause_in_factorized_clause N (Uer, ℱ, λx. None, Some C)"
    unfolding next_clause_in_factorized_clause_def
    using C_least[unfolded linorder_cls.is_least_in_fset_iff] by simp
next
  show "implicitly_factorized_clauses_subset N (Uer, ℱ, λx. None, Some C)"
    unfolding implicitly_factorized_clauses_subset_def
    using ℱ_subset by simp
next
  have "ord_res.interp (iefac ℱ ` (fset N ∪ fset Uer)) C = {}"
    using C_least[unfolded linorder_cls.is_least_in_fset_iff]
    by (simp add: interp_eq_empty_if_least_in_set linorder_cls.is_least_in_set_iff)
  thus "model_eq_interp_upto_next_clause N (Uer, ℱ, λx. None, Some C)"
    unfolding model_eq_interp_upto_next_clause_def by simp
next
  have "¬(∃Ca |∈| iefac ℱ |`| (N |∪| Uer). Ca ≺c C)"
    using C_least[unfolded linorder_cls.is_least_in_fset_iff]
    by (metis linorder_cls.less_asym)
  thus "all_smaller_clauses_true_wrt_respective_Interp N (Uer, ℱ, λx. None, Some C)"
    unfolding all_smaller_clauses_true_wrt_respective_Interp_def by simp
next
  show "atoms_in_model_were_produced N (Uer, ℱ, λx. None, Some C)"
    unfolding atoms_in_model_were_produced_def by simp
next
  have "∀Ca. Ca ≺c C ⟶ Ca |∉| iefac ℱ |`| (N |∪| Uer)"
    using C_least[unfolded linorder_cls.is_least_in_fset_iff]
    by (metis linorder_cls.order.asym)
  thus "all_produced_atoms_in_model N (Uer, ℱ, λx. None, Some C)"
    unfolding all_produced_atoms_in_model_def
    by (simp add: ord_res.production_unfold)
qed

lemma ord_res_5_preserves_invars:
  assumes step: "ord_res_5 N s s'" and invars: "ord_res_5_invars N s"
  shows "ord_res_5_invars N s'"
proof -
  obtain Uer ℱ ℳ 𝒞 where s_def: "s = (Uer, ℱ, ℳ, 𝒞)"
    by (metis prod.exhaust)

  then show ?thesis
    unfolding ord_res_5_invars_def
    using invars[unfolded ord_res_5_invars_def]
    using next_clause_in_factorized_clause[OF step]
      ord_res_5_preserves_implicitly_factorized_clauses_subset[OF step]
      model_eq_interp_upto_next_clause[OF step]
      all_smaller_clauses_true_wrt_respective_Interp[OF step]
      atoms_in_model_were_produced[OF step]
      all_produced_atoms_in_model[OF step]
    by metis
qed

lemma rtranclp_ord_res_5_preserves_invars:
  assumes steps: "(ord_res_5 N)** s s'" and invars: "ord_res_5_invars N s"
  shows "ord_res_5_invars N s'"
  using steps invars
  by (induction s rule: converse_rtranclp_induct) (auto intro: ord_res_5_preserves_invars)

lemma tranclp_ord_res_5_preserves_invars:
  assumes steps: "(ord_res_5 N)++ s s'" and invars: "ord_res_5_invars N s"
  shows "ord_res_5_invars N s'"
  using rtranclp_ord_res_5_preserves_invars
  by (metis invars steps tranclp_into_rtranclp)

lemma le_least_false_clause:
  fixes N s Uer ℱ ℳ C D
  assumes
    invars: "ord_res_5_invars N s" and
    s_def: "s = (Uer, ℱ, ℳ, Some C)" and
    D_least_false: "is_least_false_clause (iefac ℱ |`| (N |∪| Uer)) D"
  shows "C ≼c D"
proof -
  have D_in: "D |∈| iefac ℱ |`| (N |∪| Uer)"
    using D_least_false
    unfolding is_least_false_clause_def linorder_cls.is_least_in_ffilter_iff
    by argo

  show "C ≼c D"
  proof (rule next_clause_lt_least_false_clause[rule_format])
    show "is_least_false_clause (iefac ℱ |`| (N |∪| Uer)) D"
      using D_least_false .
  next
    show "(Uer, ℱ, ℳ, Some C) = (Uer, ℱ, ℳ, Some C)" ..
  next
    show "all_smaller_clauses_true_wrt_respective_Interp N (Uer, ℱ, ℳ, Some C)"
      using invars by (metis s_def ord_res_5_invars_def)
  next
    show "model_eq_interp_upto_next_clause N (Uer, ℱ, ℳ, Some C)"
      using invars by (metis s_def ord_res_5_invars_def)
  qed
qed

lemma ex_ord_res_5_if_not_final:
  assumes
    not_final: "¬ ord_res_5_final S" and
    invars: "∀N s. S = (N, s) ⟶ ord_res_5_invars N s"
  shows "∃S'. ord_res_5_step S S'"
proof -
  from not_final obtain N Uer ℱ ℳ C where
    S_def: "S = (N, (Uer, ℱ, ℳ, Some C))" and "C ≠ {#}"
    unfolding ord_res_5_final.simps de_Morgan_disj not_ex
    by (metis option.exhaust surj_pair)

  note invars' = invars[unfolded ord_res_5_invars_def, rule_format, OF S_def]

  have "∃s'. ord_res_5 N (Uer, ℱ, ℳ, Some C) s'"
  proof (cases "dom ℳ ⊫ C")
    case True
    thus ?thesis
      using ord_res_5.skip by metis
  next
    case C_false: False
    obtain L where L_max: "linorder_lit.is_maximal_in_mset C L"
      using linorder_lit.ex_maximal_in_mset[OF ‹C ≠ {#}›] ..

    show ?thesis
    proof (cases L)
      case (Pos A)
      hence L_pos: "is_pos L"
        by simp
      show ?thesis
      proof (cases "ord_res.is_strictly_maximal_lit L C")
        case True
        then show ?thesis
          using ord_res_5.production[OF C_false L_max L_pos] by metis
      next
        case L_not_striclty_max: False
        thus ?thesis
          using ord_res_5.factoring[OF C_false L_max L_pos L_not_striclty_max _ refl refl] by metis
      qed
    next
      case (Neg A)
      hence L_neg: "is_neg L"
        by simp

      have C_least_false: "is_least_false_clause (iefac ℱ |`| (N |∪| Uer)) C"
        unfolding is_least_false_clause_def linorder_cls.is_least_in_ffilter_iff
      proof (intro conjI ballI impI)
        show "C |∈| iefac ℱ |`| (N |∪| Uer)"
          using invars' by (metis next_clause_in_factorized_clause_def)
      next
        have "¬ ord_res.interp (fset (iefac ℱ |`| (N |∪| Uer))) C ⊫ C"
          using invars' C_false by (metis model_eq_interp_upto_next_clause_def)
        moreover have "ord_res.production (fset (iefac ℱ |`| (N |∪| Uer))) C = {}"
        proof -
          have "∄L. is_pos L ∧ ord_res.is_strictly_maximal_lit L C"
            using L_max L_neg
            by (metis Uniq_D linorder_lit.Uniq_is_maximal_in_mset
                linorder_lit.is_maximal_in_mset_if_is_greatest_in_mset)
          thus ?thesis
            using unproductive_if_nex_strictly_maximal_pos_lit by metis
        qed
        ultimately show "¬ ord_res_Interp (fset (iefac ℱ |`| (N |∪| Uer))) C ⊫ C"
          by simp
      next
        fix D
        assume D_in: "D |∈| iefac ℱ |`| (N |∪| Uer)" and "D ≠ C" and
          C_false: "¬ ord_res_Interp (fset (iefac ℱ |`| (N |∪| Uer))) D ⊫ D"
        have "¬ D ≺c C"
          using C_false
          using invars' D_in
          unfolding all_smaller_clauses_true_wrt_respective_Interp_def
          by auto
        thus "C ≺c D"
          using ‹D ≠ C› by order
      qed
      then obtain D where "D|∈|iefac ℱ |`| (N |∪| Uer)" and
        "D ≺c C" and
        "ord_res.is_strictly_maximal_lit (Pos A) D" and
        D_prod: "ord_res.production (fset (iefac ℱ |`| (N |∪| Uer))) D = {A}"
        using bex_smaller_productive_clause_if_least_false_clause_has_negative_max_lit
          L_max[unfolded Neg] by metis

      have "ℳ (atm_of L) = Some D"
        using invars'
        by (metis Neg ‹D ≺c C› all_produced_atoms_in_model_def D_prod insertI1 literal.sel(2))

      then show ?thesis
        using ord_res_5.resolution[OF C_false L_max L_neg] by metis
    qed
  qed
  thus ?thesis
    using S_def ord_res_5_step.simps by metis
qed

lemma ord_res_5_safe_state_if_invars:
  fixes N s
  assumes invars: "ord_res_5_invars N s"
  shows "safe_state ord_res_5_step ord_res_5_final (N, s)"
proof -
  {
    fix S'
    assume "ord_res_5_semantics.eval (N, s) S'" and stuck: "stuck_state ord_res_5_step S'"
    then obtain s' where "S' = (N, s')" and "(ord_res_5 N)** s s'"
    proof (induction "(N, s)" arbitrary: N s rule: converse_rtranclp_induct)
      case base
      thus ?case by simp
    next
      case (step z)
      thus ?case
        by (smt (verit, ccfv_SIG) converse_rtranclp_into_rtranclp ord_res_5_step.cases prod.inject)
    qed
    hence "ord_res_5_invars N s'"
      using invars rtranclp_ord_res_5_preserves_invars by metis
    hence "¬ ord_res_5_final S' ⟹ ∃S''. ord_res_5_step S' S''"
      using ex_ord_res_5_if_not_final[of S'] ‹S' = (N, s')› by blast
    hence "ord_res_5_final S'"
      using stuck[unfolded stuck_state_def] by argo
  }
  thus ?thesis
    unfolding safe_state_def stuck_state_def by metis
qed

lemma MAGIC1:
  assumes invars: "ord_res_5_invars N (Uer, ℱ, ℳ, 𝒞)"
  shows "∃ℳ' 𝒞'. (ord_res_5 N)** (Uer, ℱ, ℳ, 𝒞) (Uer, ℱ, ℳ', 𝒞') ∧
    (∄ℳ'' 𝒞''. ord_res_5 N (Uer, ℱ, ℳ', 𝒞') (Uer, ℱ, ℳ'', 𝒞''))"
proof -
  define R where
    "R = (λ(ℳ, 𝒞) (ℳ', 𝒞'). ord_res_5 N (Uer, ℱ, ℳ, 𝒞) (Uer, ℱ, ℳ', 𝒞'))"

  define f :: "('f gterm ⇒ 'f gclause option) × 'f gclause option ⇒ 'f gclause fset" where
    "f = (λ(ℳ, 𝒞). case 𝒞 of None ⇒ {||} | Some C ⇒ finsert C {|D |∈| iefac ℱ |`| (N |∪| Uer). C ≼c D|})"

  have "Wellfounded.wfp_on {x'. R** (ℳ, 𝒞) x'} R¯¯"
  proof (rule wfp_on_if_convertible_to_wfp_on)
    have "wfp (|⊂|)"
      by auto
    thus "Wellfounded.wfp_on (f ` {x'. R** (ℳ, 𝒞) x'}) (|⊂|)"
      using Wellfounded.wfp_on_subset subset_UNIV by metis
  next
    fix x y :: "('f gterm ⇒ 'f gclause option) × 'f gclause option"

    obtain ℳx 𝒞x where x_def: "x = (ℳx, 𝒞x)"
      by force

    obtain ℳy 𝒞y where y_def: "y = (ℳy, 𝒞y)"
      by force

    have rtranclp_with_constsD: "(λ(y, z) (y', z'). R (x, y, z) (x, y', z'))** (y, z) (y', z') ⟹
      R** (x, y, z) (x, y', z')" for R x y z y' z'
    proof (induction "(y, z)" arbitrary: y z rule: converse_rtranclp_induct)
      case base
      show ?case
        by simp
    next
      case (step w)
      thus ?case
        by force
    qed 

    assume "x ∈ {x'. R** (ℳ, 𝒞) x'}" and  "y ∈ {x'. R** (ℳ, 𝒞) x'}"
    hence
      "(ord_res_5 N)** (Uer, ℱ, ℳ, 𝒞) (Uer, ℱ, ℳx, 𝒞x)" and
      "(ord_res_5 N)** (Uer, ℱ, ℳ, 𝒞) (Uer, ℱ, ℳy, 𝒞y)"
      unfolding atomize_conj mem_Collect_eq R_def x_def y_def
      by (auto intro: rtranclp_with_constsD)
    hence
      x_invars: "ord_res_5_invars N (Uer, ℱ, ℳx, 𝒞x)" and
      y_invars: "ord_res_5_invars N (Uer, ℱ, ℳy, 𝒞y)"
      using invars by (metis rtranclp_ord_res_5_preserves_invars)+

    assume "R¯¯ y x"
    hence "ord_res_5 N (Uer, ℱ, ℳx, 𝒞x) (Uer, ℱ, ℳy, 𝒞y)"
      unfolding conversep_iff R_def x_def y_def prod.case .
    thus "f y |⊂| f x"
    proof (cases N "(Uer, ℱ, ℳx, 𝒞x)" "(Uer, ℱ, ℳy, 𝒞y)")
      case step_hyps: (skip C)

      have "f y |⊆| {|D |∈| iefac ℱ |`| (N |∪| Uer). C ≺c D|}"
      proof (cases 𝒞y)
        case None
        thus ?thesis
          unfolding f_def y_def prod.case by simp
      next
        case 𝒞y_def: (Some D)

        have D_least: "linorder_cls.is_least_in_fset (ffilter ((≺c) C) (iefac ℱ |`| (N |∪| Uer))) D"
          using step_hyps 𝒞y_def by (metis The_optional_eq_SomeD)
        hence f_y_eq: "f y = {|E |∈| iefac ℱ |`| (N |∪| Uer). D ≼c E|}"
          unfolding f_def y_def prod.case 𝒞y_def option.case linorder_cls.is_least_in_ffilter_iff
          by auto

        show ?thesis
          unfolding f_y_eq subset_ffilter
          using D_least
          unfolding linorder_cls.is_least_in_ffilter_iff
          by auto
      qed

      also have "… |⊂| finsert C {|D |∈| iefac ℱ |`| (N |∪| Uer). C ≼c D|}"
        by auto

      also have "… = f x"
        unfolding f_def x_def y_def prod.case step_hyps option.case by metis

      finally show ?thesis .
    next
      case step_hyps: (production C L)

      have "f y |⊆| {|D |∈| iefac ℱ |`| (N |∪| Uer). C ≺c D|}"
      proof (cases 𝒞y)
        case None
        thus ?thesis
          unfolding f_def y_def prod.case by simp
      next
        case 𝒞y_def: (Some D)

        have D_least: "linorder_cls.is_least_in_fset (ffilter ((≺c) C) (iefac ℱ |`| (N |∪| Uer))) D"
          using step_hyps 𝒞y_def by (metis The_optional_eq_SomeD)
        hence f_y_eq: "f y = {|E |∈| iefac ℱ |`| (N |∪| Uer). D ≼c E|}"
          unfolding f_def y_def prod.case 𝒞y_def option.case linorder_cls.is_least_in_ffilter_iff
          by auto

        show ?thesis
          unfolding f_y_eq subset_ffilter
          using D_least
          unfolding linorder_cls.is_least_in_ffilter_iff
          by auto
      qed

      also have "… |⊂| finsert C {|D |∈| iefac ℱ |`| (N |∪| Uer). C ≼c D|}"
        by auto

      also have "… = f x"
        unfolding f_def x_def y_def prod.case step_hyps option.case by metis

      finally show ?thesis .
    next
      case step_hyps: (factoring C L)

      have "C |∈| iefac ℱ |`| (N |∪| Uer)"
        using x_invars unfolding ‹𝒞x = Some C›
        by (metis next_clause_in_factorized_clause_def ord_res_5_invars_def)
      hence "C |∉| ℱ"
        using step_hyps(3,4,5)
        by (smt (verit, ccfv_SIG) fimage_iff iefac_def literal.collapse(1)
            ex1_efac_eq_factoring_chain ex_ground_factoringI)
      moreover have "C |∈| ℱ"
        using ‹ℱ = finsert C ℱ› by auto
      ultimately have False
        by contradiction
      thus ?thesis ..
    next
      case step_hyps: (resolution C L D)

      have D_productive: "atm_of L ∈ ord_res.production (fset (iefac ℱ |`| (N |∪| Uer))) D"
        using x_invars step_hyps
        by (metis ord_res_5_invars_def atoms_in_model_were_produced_def)

      hence "∃DC. ground_resolution D C DC"
        unfolding ground_resolution_def
        using step_hyps
        by (metis Neg_atm_of_iff ord_res.mem_productionE linorder_cls.le_less_linear
            linorder_lit.is_maximal_in_mset_iff linorder_trm.dual_order.order_iff_strict
            linorder_trm.not_less ord_res.less_trm_if_neg ex_ground_resolutionI)

      hence "eres D C ≠ C"
        unfolding eres_ident_iff by metis

      have "eres D C |∉| Uer"
      proof (rule notI)
        assume "eres D C |∈| Uer"
        hence "iefac ℱ (eres D C) |∈| iefac ℱ |`| (N |∪| Uer)"
          by simp

        moreover have "iefac ℱ (eres D C) ≺c C"
        proof -
          have "iefac ℱ C ≺c D" if "C ≺c D" for ℱ C D
          proof (cases "C |∈| ℱ")
            case True
            hence "iefac ℱ C = efac C"
              by (simp add: iefac_def)
            also have "… ≼c C"
              by (metis efac_subset subset_implies_reflclp_multp)
            also have "… ≺c D"
              using that .
            finally show ?thesis .
          next
            case False
            thus ?thesis
              using that by (simp add: iefac_def)
          qed

          moreover have "eres D C ≺c C"
          proof -
            have "eres D C ≼c C"
              using eres_le by metis
            thus "eres D C ≺c C"
              using ‹eres D C ≠ C› by order
          qed

          ultimately show ?thesis
            by metis
        qed

        ultimately have "ord_res_Interp (fset (iefac ℱ |`| (N |∪| Uer))) (iefac ℱ (eres D C)) ⊫ iefac ℱ (eres D C)"
          using x_invars unfolding ‹𝒞x = Some C›
          unfolding ord_res_5_invars_def all_smaller_clauses_true_wrt_respective_Interp_def by fast
        hence "ord_res.interp (fset (iefac ℱ |`| (N |∪| Uer))) C ⊫ iefac ℱ (eres D C)"
          using ord_res.entailed_clause_stays_entailed' ‹iefac ℱ (eres D C) ≺c C› by metis
        hence "ord_res.interp (fset (iefac ℱ |`| (N |∪| Uer))) C ⊫ eres D C"
        proof (rule true_cls_iff_set_mset_eq[THEN iffD1, rotated])
          show "set_mset (iefac ℱ (eres D C)) = set_mset (eres D C)"
            using iefac_def by auto
        qed
        hence "ord_res.interp (fset (iefac ℱ |`| (N |∪| Uer))) C ⊫ C"
        proof -
          obtain m A D' C' where
            "ord_res.is_strictly_maximal_lit (Pos A) D" and
            D_def: "D = add_mset (Pos A) D'" and
            C_def: "C = replicate_mset (Suc m) (Neg A) + C'" and
            "Neg A ∉# C'" and
            eres_D_C_eq: "eres D C = repeat_mset (Suc m) D' + C'"
            using ‹eres D C ≠ C›[THEN eres_not_identD] by metis

          hence
            "atm_of L = A" and
            D_in: "D |∈| iefac ℱ |`| (N |∪| Uer)" and
            D_false: "¬ ord_res.interp (fset (iefac ℱ |`| (N |∪| Uer))) D ⊫ D"
            unfolding atomize_conj
            using D_productive
            unfolding ord_res.production_unfold mem_Collect_eq
            by (metis linorder_lit.Uniq_is_greatest_in_mset literal.inject(1) the1_equality')

          have D'_false: "¬ ord_res.interp (fset (iefac ℱ |`| (N |∪| Uer))) D ⊫ D'"
            using D_false D_def by fastforce

          have "D ≺c C"
            using ‹∃DC. ground_resolution D C DC› left_premise_lt_right_premise_if_ground_resolution by blast

          let ?I = "ord_res.interp (fset (iefac ℱ |`| (N |∪| Uer))) C"

          assume "?I ⊫ eres D C"
          hence "?I ⊫ D' ∨ ?I ⊫ C'"
            unfolding eres_D_C_eq true_cls_union true_cls_repeat_mset_Suc .

          moreover have "¬ ?I ⊫ D'"
            using ‹D ≺c C›
            by (smt (verit) D_def D_productive ‹ord_res.is_strictly_maximal_lit (Pos A) D›
                diff_single_eq_union ord_res.mem_productionE linorder_lit.is_greatest_in_mset_iff
                ord_res.Uniq_striclty_maximal_lit_in_ground_cls
                ord_res.false_cls_if_productive_production ord_res_5_invars_def
                next_clause_in_factorized_clause_def step_hyps(1) the1_equality' x_invars)

          ultimately show "?I ⊫ C"
            by (simp add: C_def)
        qed
        hence "dom ℳx ⊫ C"
          using x_invars ‹𝒞x = Some C›
          by (metis model_eq_interp_upto_next_clause_def ord_res_5_invars_def)
        thus False
          using ‹¬ dom ℳx ⊫ C› by contradiction
      qed
      hence False
        using ‹Uer = finsert (eres D C) Uer› by auto
      thus ?thesis ..
    qed
  qed

  then obtain ℳ' 𝒞' where "R** (ℳ, 𝒞) (ℳ', 𝒞')" and "∄z. R (ℳ', 𝒞') z"
    using ex_terminating_rtranclp_strong by (metis surj_pair)

  show ?thesis
  proof (intro exI conjI)
    show "(ord_res_5 N)** (Uer, ℱ, ℳ, 𝒞) (Uer, ℱ, ℳ', 𝒞')"
      using ‹R** (ℳ, 𝒞) (ℳ', 𝒞')›
      by (induction "(ℳ, 𝒞)" arbitrary: ℳ 𝒞 rule: converse_rtranclp_induct) (auto simp: R_def)
  next
    show "∄ℳ'' 𝒞''. ord_res_5 N (Uer, ℱ, ℳ', 𝒞') (Uer, ℱ, ℳ'', 𝒞'')"
      using ‹∄z. R (ℳ', 𝒞') z›
      by (simp add: R_def)
  qed
qed

lemma MAGIC2:
  assumes invars: "ord_res_5_invars N (Uer, ℱ, ℳ, Some C)"
  assumes "C ≠ {#}"
  shows "∃s'. ord_res_5 N (Uer, ℱ, ℳ, Some C) s'"
proof (cases "(dom ℳ) ⊫ C")
  case C_true: True
  thus ?thesis
    using ord_res_5.skip by metis
next
  case C_false: False
  obtain L where L_max: "linorder_lit.is_maximal_in_mset C L"
    using ‹C ≠ {#}› linorder_lit.ex_maximal_in_mset by metis

  show ?thesis
  proof (cases L)
    case (Pos A)
    hence L_pos: "is_pos L"
      by simp

    show ?thesis
    proof (cases "linorder_lit.is_greatest_in_mset C L")
      case L_greatest: True
      thus ?thesis
        using C_false L_max L_pos ord_res_5.production by metis
    next
      case L_not_greatest: False
      thus ?thesis
        using C_false L_max L_pos ord_res_5.factoring by metis
    qed
  next
    case (Neg A)
    hence L_neg: "is_neg L"
      by simp

    have "is_least_false_clause (iefac ℱ |`| (N |∪| Uer)) C"
      unfolding is_least_false_clause_def linorder_cls.is_least_in_ffilter_iff
    proof (intro conjI ballI impI)
      show "C |∈| iefac ℱ |`| (N |∪| Uer)"
        using invars unfolding ord_res_5_invars_def next_clause_in_factorized_clause_def by metis
    next
      have "dom ℳ = ord_res.interp (fset (iefac ℱ |`| (N |∪| Uer))) C"
        using invars unfolding ord_res_5_invars_def model_eq_interp_upto_next_clause_def by metis

      moreover have "ord_res.production (fset (iefac ℱ |`| (N |∪| Uer))) C = {}"
      proof -
        have "∄L. is_pos L ∧ ord_res.is_strictly_maximal_lit L C"
          using L_max L_neg
          by (metis Uniq_D linorder_lit.Uniq_is_maximal_in_mset
              linorder_lit.is_maximal_in_mset_if_is_greatest_in_mset)
        thus ?thesis
          using unproductive_if_nex_strictly_maximal_pos_lit by metis
      qed

      ultimately show "¬ ord_res_Interp (fset (iefac ℱ |`| (N |∪| Uer))) C ⊫ C"
        using C_false model_eq_interp_upto_next_clause_def by simp
    next
      fix D
      assume
        "D |∈| iefac ℱ |`| (N |∪| Uer)" and
        "D ≠ C" and
        "¬ ord_res_Interp (fset (iefac ℱ |`| (N |∪| Uer))) D ⊫ D"

      moreover have "∀B |∈| iefac ℱ |`| (N |∪| Uer). B ≺c C ⟶
        ord_res_Interp (fset (iefac ℱ |`| (N |∪| Uer))) B ⊫ B"
        using invars
        unfolding ord_res_5_invars_def all_smaller_clauses_true_wrt_respective_Interp_def
        by simp

      ultimately show "C ≺c D"
        by force
    qed
    then obtain D where "D|∈|iefac ℱ |`| (N |∪| Uer)" and
      "D ≺c C" and
      "ord_res.is_strictly_maximal_lit (Pos A) D" and
      D_prod: "ord_res.production (fset (iefac ℱ |`| (N |∪| Uer))) D = {A}"
      using bex_smaller_productive_clause_if_least_false_clause_has_negative_max_lit
        L_max[unfolded Neg] by metis

    have "ℳ (atm_of L) = Some D"
      using invars
      unfolding ord_res_5_invars_def all_produced_atoms_in_model_def
      by (metis Neg ‹D ≺c C› D_prod insertI1 literal.sel(2))

    thus ?thesis
      using ord_res_5.resolution C_false L_max L_neg by metis
  qed
qed

lemma MAGIC3:
  assumes invars: "ord_res_5_invars N (Uer, ℱ, ℳ, 𝒞)" and
    steps: "(ord_res_5 N)** (Uer, ℱ, ℳ, 𝒞) (Uer, ℱ, ℳ', 𝒞')" and
    no_more_steps: "(∄ℳ'' 𝒞''. ord_res_5 N (Uer, ℱ, ℳ', 𝒞') (Uer, ℱ, ℳ'', 𝒞''))"
  shows "(∀C. 𝒞' = Some C ⟷ is_least_false_clause (iefac ℱ |`| (N |∪| Uer)) C)"
proof -
  have invars': "ord_res_5_invars N (Uer, ℱ, ℳ', 𝒞')"
    using steps invars rtranclp_ord_res_5_preserves_invars by metis

  show ?thesis
  proof (cases 𝒞')
    case None

    moreover have "∄C. is_least_false_clause (iefac ℱ |`| (N |∪| Uer)) C"
    proof (rule notI, elim exE)
      fix C

      have "all_smaller_clauses_true_wrt_respective_Interp N (Uer, ℱ, ℳ', 𝒞')"
        using invars' unfolding ord_res_5_invars_def by metis
      hence "(∀C|∈|iefac ℱ |`| (N |∪| Uer). ord_res_Interp (fset (iefac ℱ |`| (N |∪| Uer))) C ⊫ C)"
        by (simp add: ‹𝒞' = None› all_smaller_clauses_true_wrt_respective_Interp_def)

      moreover assume "is_least_false_clause (iefac ℱ |`| (N |∪| Uer)) C"

      ultimately show False
        unfolding is_least_false_clause_def linorder_cls.is_least_in_ffilter_iff by metis
    qed

    ultimately show ?thesis
      by simp
  next
    case (Some D)

    moreover have "is_least_false_clause (iefac ℱ |`| (N |∪| Uer)) D"
      unfolding is_least_false_clause_def linorder_cls.is_least_in_ffilter_iff
    proof (intro conjI ballI impI)
      show "D |∈| iefac ℱ |`| (N |∪| Uer)"
        using invars' ‹𝒞' = Some D›
        unfolding ord_res_5_invars_def next_clause_in_factorized_clause_def
        by metis
    next
      have "D ≠ {#} ⟹ ∃s'. ord_res_5 N (Uer, ℱ, ℳ', Some D) s'"
        using MAGIC2 invars' ‹𝒞' = Some D› by metis

      thus "¬ ord_res_Interp (fset (iefac ℱ |`| (N |∪| Uer))) D ⊫ D"
        by (smt (verit) Pair_inject Un_empty_right Uniq_D calculation empty_iff invars'
            linorder_lit.Uniq_is_maximal_in_mset
            linorder_lit.is_maximal_in_mset_if_is_greatest_in_mset no_more_steps option.inject
            ord_res_5.cases set_mset_empty model_eq_interp_upto_next_clause_def ord_res_5_invars_def
            true_cls_def unproductive_if_nex_strictly_maximal_pos_lit)
    next
      fix E
      assume
        "E |∈| iefac ℱ |`| (N |∪| Uer)" and
        "E ≠ D" and
        "¬ ord_res_Interp (fset (iefac ℱ |`| (N |∪| Uer))) E ⊫ E"

      moreover have "∀C |∈| iefac ℱ |`| (N |∪| Uer). C ≺c D ⟶
        ord_res_Interp (fset (iefac ℱ |`| (N |∪| Uer))) C ⊫ C"
        using invars' ‹𝒞' = Some D›
        unfolding ord_res_5_invars_def all_smaller_clauses_true_wrt_respective_Interp_def
        by simp

      ultimately show "D ≺c E"
        by force
    qed

    ultimately show ?thesis
      by (metis Uniq_D Uniq_is_least_false_clause option.inject)
  qed
qed

lemma ord_res_5_construct_model_upto_least_false_clause:
  assumes invars: "ord_res_5_invars N (Uer, ℱ, ℳ, 𝒞)"
  shows "∃ℳ' 𝒞'. (ord_res_5 N)** (Uer, ℱ, ℳ, 𝒞) (Uer, ℱ, ℳ', 𝒞') ∧
    (∀C. 𝒞' = Some C ⟷ is_least_false_clause (iefac ℱ |`| (N |∪| Uer)) C)"
  using MAGIC1[OF invars] MAGIC3[OF invars] by metis

end

end