Theory ORD_RES_6

theory ORD_RES_6
  imports
    ORD_RES_5
begin

section ‹ORD-RES-6 (model backjump)›

context simulation_SCLFOL_ground_ordered_resolution begin

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

  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 |∪| U⇩e⇩r). C ≺⇩c D|}) ⟹
    ord_res_6 N (U⇩e⇩r, ℱ, ℳ, Some C) (U⇩e⇩r, ℱ, ℳ', 𝒞')" |

  factoring: "
    ¬ (dom ℳ) ⊫ C ⟹
    linorder_lit.is_maximal_in_mset C L ⟹
    is_pos L ⟹
    ¬ linorder_lit.is_greatest_in_mset C L ⟹
    ℱ' = finsert C ℱ ⟹
    ord_res_6 N (U⇩e⇩r, ℱ, ℳ, Some C) (U⇩e⇩r, ℱ', ℳ, Some (efac C))" |

  resolution_bot: "
    ¬ (dom ℳ) ⊫ C ⟹
    linorder_lit.is_maximal_in_mset C L ⟹
    is_neg L ⟹
    ℳ (atm_of L) = Some D ⟹
    U⇩e⇩r' = finsert (eres D C) U⇩e⇩r ⟹
    eres D C = {#} ⟹
    ℳ' = (λ_. None) ⟹
    ord_res_6 N (U⇩e⇩r, ℱ, ℳ, Some C) (U⇩e⇩r', ℱ, ℳ', Some {#})" |

  resolution_pos: "
    ¬ (dom ℳ) ⊫ C ⟹
    linorder_lit.is_maximal_in_mset C L ⟹
    is_neg L ⟹
    ℳ (atm_of L) = Some D ⟹
    U⇩e⇩r' = finsert (eres D C) U⇩e⇩r ⟹
    eres D C ≠ {#} ⟹
    ℳ' = restrict_map ℳ {A. A ≺⇩t atm_of K} ⟹
    linorder_lit.is_maximal_in_mset (eres D C) K ⟹
    is_pos K ⟹
    ord_res_6 N (U⇩e⇩r, ℱ, ℳ, Some C) (U⇩e⇩r', ℱ, ℳ', Some (eres D C))" |

  resolution_neg: "
    ¬ (dom ℳ) ⊫ C ⟹
    linorder_lit.is_maximal_in_mset C L ⟹
    is_neg L ⟹
    ℳ (atm_of L) = Some D ⟹
    U⇩e⇩r' = finsert (eres D C) U⇩e⇩r ⟹
    eres D C ≠ {#} ⟹
    ℳ' = restrict_map ℳ {A. A ≺⇩t atm_of K} ⟹
    linorder_lit.is_maximal_in_mset (eres D C) K ⟹
    is_neg K ⟹
    ℳ (atm_of K) = Some E ⟹
    ord_res_6 N (U⇩e⇩r, ℱ, ℳ, Some C) (U⇩e⇩r', ℱ, ℳ', Some E)"

inductive ord_res_6_step where
  "ord_res_6 N s s' ⟹ ord_res_6_step (N, s) (N, s')"

lemma tranclp_ord_res_6_step_if_tranclp_ord_res_6:
  "(ord_res_6 N)⇧+⇧+ s s' ⟹ ord_res_6_step⇧+⇧+ (N, s) (N, s')"
  by (induction s' rule: tranclp_induct)
   (auto intro: ord_res_6_step.intros tranclp.intros)

lemma right_unique_ord_res_6: "right_unique (ord_res_6 N)"
proof (rule right_uniqueI)
  fix s s' s''
  assume step1: "ord_res_6 N s s'" and step2: "ord_res_6 N s s''"
  thus "s' = s''"
    by (smt (verit) Pair_inject linorder_lit.Uniq_is_maximal_in_mset option.inject ord_res_6.cases
        the1_equality')
qed

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

inductive ord_res_6_final where
  model_found:
    "ord_res_6_final (N, U⇩e⇩r, ℱ, ℳ, None)" |

  contradiction_found:
    "ord_res_6_final (N, U⇩e⇩r, ℱ, ℳ, Some {#})"

sublocale ord_res_6_semantics: semantics where
  step = ord_res_6_step and
  final = ord_res_6_final
proof unfold_locales
  fix S :: "'f gclause fset ×'f gclause fset × 'f gclause fset ×
    ('f gterm ⇒ 'f gclause option) × 'f gclause option"

  obtain
    N U⇩e⇩r ℱ :: "'f gterm clause fset" and
    ℳ :: "'f gterm ⇒ 'f gclause option" and
    𝒞 :: "'f gclause option" where
    S_def: "S = (N, (U⇩e⇩r, ℱ, ℳ, 𝒞))"
    by (metis prod.exhaust)

  assume "ord_res_6_final S"
  hence "𝒞 = None ∨ 𝒞 = Some {#}"
    by (simp add: S_def ord_res_6_final.simps)
  hence "∄x. ord_res_6 N (U⇩e⇩r, ℱ, ℳ, 𝒞) x"
    by (auto simp: linorder_lit.is_maximal_in_mset_iff elim: ord_res_6.cases)
  thus "finished ord_res_6_step S"
    by (simp add: S_def finished_def ord_res_6_step.simps)
qed

lemma ord_res_6_preserves_invars:
  assumes step: "ord_res_6 N s s'" and invars: "ord_res_5_invars N s"
  shows "ord_res_5_invars N s'"
  using step
proof (cases N s s' rule: ord_res_6.cases)
  case (skip ℳ C 𝒞' ℱ U⇩e⇩r)
  thus ?thesis
    by (metis invars ord_res_5_preserves_invars ord_res_5.skip)
next
  case (production ℳ C L ℳ' 𝒞' ℱ U⇩e⇩r)
  thus ?thesis
    by (metis invars ord_res_5.production ord_res_5_preserves_invars)
next
  case step_hyps: (factoring ℳ C L ℱ' ℱ U⇩e⇩r)

  have "efac C ≠ C"
    by (metis ex1_efac_eq_factoring_chain is_pos_def ex_ground_factoringI step_hyps(4,5,6))
  moreover have "efac C ≼⇩c C"
    by (metis efac_subset subset_implies_reflclp_multp)
  ultimately have "efac C ≺⇩c C"
    by order

  show ?thesis
    unfolding step_hyps(1,2) ord_res_5_invars_def
  proof (intro conjI)
    have "C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)"
      using invars step_hyps
      by (metis next_clause_in_factorized_clause_def ord_res_5_invars_def)
    hence "C |∈| N |∪| U⇩e⇩r"
      using ‹efac C ≠ C›
      by (smt (verit, best) fimage_iff iefac_def ex1_efac_eq_factoring_chain
          factorizable_if_neq_efac)
    hence "efac C |∈| iefac ℱ' |`| (N |∪| U⇩e⇩r)"
      using step_hyps(3-)
      using iefac_def by auto
    thus "next_clause_in_factorized_clause N (U⇩e⇩r, ℱ', ℳ, Some (efac C))"
      unfolding next_clause_in_factorized_clause_def by simp

    have "ℱ |⊆| N |∪| U⇩e⇩r"
      using invars
      unfolding step_hyps(1,2) ord_res_5_invars_def implicitly_factorized_clauses_subset_def
      by metis

    hence "ℱ' |⊆| N |∪| U⇩e⇩r"
      using ‹C |∈| N |∪| U⇩e⇩r› ‹ℱ' = finsert C ℱ› by simp

    thus "implicitly_factorized_clauses_subset N (U⇩e⇩r, ℱ', ℳ, Some (efac C))"
      unfolding implicitly_factorized_clauses_subset_def by simp

    have dom_ℳ_eq: "dom ℳ = ord_res.interp (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) C"
      using invars step_hyps
      by (simp add: model_eq_interp_upto_next_clause_def ord_res_5_invars_def)

    have "efac C |∉| iefac ℱ |`| (N |∪| U⇩e⇩r)"
    proof (rule notI)
      assume "efac C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)"
      show False
      proof (cases "atm_of L ∈ ord_res.production (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) (efac C)")
        assume "atm_of L ∈ ord_res.production (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) (efac C)"
        hence "atm_of L ∈ ord_res.interp (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) C"
          using ‹efac C ≺⇩c C› ord_res.production_subset_if_less_cls by blast
        hence "dom ℳ ⊫ C"
          using step_hyps
          by (metis dom_ℳ_eq linorder_lit.is_maximal_in_mset_iff literal.collapse(1)
              pos_literal_in_imp_true_cls)
        thus False
          using ‹¬ dom ℳ ⊫ C› by contradiction
      next
        assume "atm_of L ∉ ord_res.production (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) (efac C)"
        hence "ord_res.interp (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) (efac C) ⊫ efac C"
          unfolding ord_res.production_unfold mem_Collect_eq
          using ‹efac C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)›
          by (metis Pos_atm_of_iff ‹efac C ≠ C› insert_DiffM
              linorder_lit.is_maximal_in_mset_if_is_greatest_in_mset
              linorder_lit.is_maximal_in_mset_iff linorder_lit.neqE
              obtains_positive_greatest_lit_if_efac_not_ident set_mset_efac step_hyps(4))
        hence "ord_res.interp (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) C ⊫ efac C"
          using ‹C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)› ‹efac C ≺⇩c C› ‹efac C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)›
            ord_res.lift_interp_entails by metis
        hence "ord_res.interp (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) C ⊫ C"
          by (simp add: true_cls_def)
        hence "dom ℳ ⊫ C"
          using dom_ℳ_eq by argo
        thus False
          using ‹¬ dom ℳ ⊫ C› by contradiction
      qed
    qed

    have "iefac ℱ' |`| (N |∪| U⇩e⇩r) = finsert (iefac ℱ' C) (iefac ℱ |`| (N |∪| U⇩e⇩r)) - {|C|}"
    proof (intro fsubset_antisym fsubsetI)
      fix x :: "'f gclause"
      assume "x |∈| iefac ℱ' |`| (N |∪| U⇩e⇩r)"
      thus "x |∈| finsert (iefac ℱ' C) (iefac ℱ |`| (N |∪| U⇩e⇩r)) |-| {|C|}"
        by (smt (verit) ‹efac C ≠ C› factorizable_if_neq_efac fimage_iff finsert_iff fminusI
            fsingletonE iefac_def ex1_efac_eq_factoring_chain step_hyps(7))
    next
      fix x :: "'f gclause"
      assume x_in: "x |∈| finsert (iefac ℱ' C) (iefac ℱ |`| (N |∪| U⇩e⇩r)) |-| {|C|}"
      hence "x = iefac ℱ' C ∨ x |∈| (iefac ℱ |`| (N |∪| U⇩e⇩r)) |-| {|C|}"
        by blast
      thus "x |∈| iefac ℱ' |`| (N |∪| U⇩e⇩r)"
      proof (elim disjE)
        assume "x = iefac ℱ' C"
        thus "x |∈| iefac ℱ' |`| (N |∪| U⇩e⇩r)"
          using ‹C |∈| N |∪| U⇩e⇩r› by blast
      next
        assume "x |∈| iefac ℱ |`| (N |∪| U⇩e⇩r) |-| {|C|}"
        hence "x |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" and "x ≠ C"
          by simp_all
        then obtain x' where "x' |∈| N |∪| U⇩e⇩r" and "x = iefac ℱ x'"
          by auto
        moreover have "x' ≠ C"
          using ‹x ≠ C› ‹x = iefac ℱ x'›
          by (metis ‹efac C |∉| iefac ℱ |`| (N |∪| U⇩e⇩r)› ‹x |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)› iefac_def)
        ultimately show "x |∈| iefac ℱ' |`| (N |∪| U⇩e⇩r)"
          using iefac_def step_hyps(7) by simp
      qed
    qed

    have "ord_res.interp (fset (iefac ℱ' |`| (N |∪| U⇩e⇩r))) (efac C) =
      ord_res.interp (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) (efac C)"
    proof (rule ord_res.interp_swap_clause_set)
      show "{D. D |∈| iefac ℱ' |`| (N |∪| U⇩e⇩r) ∧ D ≺⇩c efac C} =
        {D. D |∈| iefac ℱ |`| (N |∪| U⇩e⇩r) ∧ D ≺⇩c efac C}"
        unfolding ‹iefac ℱ' |`| (N |∪| U⇩e⇩r) = finsert (iefac ℱ' C) (iefac ℱ |`| (N |∪| U⇩e⇩r)) - {|C|}›
        using ‹efac C ≺⇩c C›
        using iefac_def by force
    qed

    also have "… = ord_res.interp (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) C"
    proof -
      have "∀x |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). x ≺⇩c C ⟶
        ord_res_Interp (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) x ⊫ x"
        using invars[unfolded ord_res_5_invars_def step_hyps(1)
            all_smaller_clauses_true_wrt_respective_Interp_def, simplified]
        by simp
      then have "ord_res.production (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) x = {}"
        if "x |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" and "efac C ≺⇩c x" and "x ≺⇩c C" for x
      proof -
        have "x ≼⇩l y ∧ y ≼⇩l z"
          if "X ≼⇩c Y" and "Y ≼⇩c Z" and
            "linorder_lit.is_maximal_in_mset X x" and
            "linorder_lit.is_maximal_in_mset Y y" and
            "linorder_lit.is_maximal_in_mset Z z"
          for x y z X Y Z
          using that
          unfolding linorder_lit.is_maximal_in_mset_iff
          by (metis ord_res.asymp_less_lit ord_res.transp_less_lit linorder_cls.leD
              linorder_lit.leI linorder_lit.multp⇩H⇩O_if_maximal_less_that_maximal multp_eq_multp⇩H⇩O
              that(3) that(4) that(5))

        hence "y = x"
          if "X ≼⇩c Y" and "Y ≼⇩c Z" and
            "linorder_lit.is_maximal_in_mset X x" and
            "linorder_lit.is_maximal_in_mset Y y" and
            "linorder_lit.is_maximal_in_mset Z x"
          for x y X Y Z
          using that
          by (metis linorder_lit.order.ordering_axioms ordering.antisym)

        hence "y = x"
          if "X ≺⇩c Y" and "Y ≺⇩c Z" and
            "linorder_lit.is_maximal_in_mset X x" and
            "linorder_lit.is_maximal_in_mset Y y" and
            "linorder_lit.is_maximal_in_mset Z x"
          for x y X Y Z
          using that by blast

        hence "K = L"
          if "efac C ≺⇩c x" and "x ≺⇩c C" and
            "linorder_lit.is_maximal_in_mset (efac C) L" and
            "linorder_lit.is_maximal_in_mset x K" and
            "linorder_lit.is_maximal_in_mset C L"
          for K
          using that by metis

        hence "K = L"
          if "linorder_lit.is_maximal_in_mset x K"
          for K
          using that
          using ‹ord_res.is_maximal_lit L C›
          using ‹efac C ≺⇩c x› ‹x ≺⇩c C› ex1_efac_eq_factoring_chain
            ord_res.ground_factorings_preserves_maximal_literal by blast

        hence "ord_res.is_maximal_lit L x"
          by (metis linorder_cls.leD linorder_lit.ex_maximal_in_mset mempty_lesseq_cls that(2))

        have "∄A. A ∈ ord_res.production (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) x"
        proof (rule notI , elim exE)
          fix A :: "'f gterm"
          assume "A ∈ ord_res.production (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) x"
          then obtain x' where
            "x |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" and
            "x = add_mset (Pos A) x'" and
            "ord_res.is_strictly_maximal_lit (Pos A) x" and
            "¬ ord_res.interp (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) x ⊫ x"
            by (metis ord_res.mem_productionE)

          have "A ∈ ord_res.interp (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) C"
            using ‹A ∈ ord_res.production (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) x›
              ord_res.production_subset_if_less_cls that(3) by fastforce

          moreover have "L = Pos A"
            using ‹ord_res.is_maximal_lit L x› ‹ord_res.is_strictly_maximal_lit (Pos A) x›
            by (metis Uniq_D linorder_lit.Uniq_is_maximal_in_mset
                linorder_lit.is_maximal_in_mset_if_is_greatest_in_mset)

          moreover have "L ∈# C"
            using step_hyps linorder_lit.is_maximal_in_mset_iff by metis

          ultimately have "ord_res.interp (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) C ⊫ C"
            by auto

          hence "dom ℳ ⊫ C"
            using dom_ℳ_eq by argo

          thus False
            using ‹¬ dom ℳ ⊫ C› by contradiction
        qed

        thus ?thesis
          by simp
      qed

      moreover have "{x. x |∈| iefac ℱ |`| (N |∪| U⇩e⇩r) ∧ x ≺⇩c C} =
        {x. x |∈| iefac ℱ |`| (N |∪| U⇩e⇩r) ∧ x ≺⇩c efac C} ∪
        {x. x |∈| iefac ℱ |`| (N |∪| U⇩e⇩r) ∧ efac C ≺⇩c x ∧ x ≺⇩c C}"
      proof -
        have "{w ∈ NN. w ≺⇩c z} = {w ∈ NN. w ≺⇩c x} ∪ {y ∈ NN. x ≺⇩c y ∧ y ≺⇩c z}"
          if "x ∉ NN" and "x ≺⇩c z" for NN x z
        proof -
          have "{w ∈ NN. w ≺⇩c z} = {w ∈ NN. w ≼⇩c x ∨ x ≺⇩c w ∧ w ≺⇩c z}"
            using that(2) by auto
          also have "… = {w ∈ NN. w ≺⇩c x ∨ x ≺⇩c w ∧ w ≺⇩c z}"
            using that(1) by auto
          also have "… = {w ∈ NN. w ≺⇩c x} ∪ {y ∈ NN. x ≺⇩c y ∧ y ≺⇩c z}"
            by auto
          finally show ?thesis .
        qed
        thus ?thesis
          using ‹efac C ≺⇩c C› ‹efac C |∉| iefac ℱ |`| (N |∪| U⇩e⇩r)› by (simp only:)
      qed

      ultimately show ?thesis
        unfolding ord_res.interp_def by auto
    qed

    finally show "model_eq_interp_upto_next_clause N (U⇩e⇩r, ℱ', ℳ, Some (efac C))"
      unfolding model_eq_interp_upto_next_clause_def
      using dom_ℳ_eq
      by simp

    have "ord_res_Interp (fset (iefac ℱ' |`| (N |∪| U⇩e⇩r))) x ⊫ x"
      if "x |∈| iefac ℱ' |`| (N |∪| U⇩e⇩r)" and "x ≺⇩c efac C" for x
    proof -
      have "x |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)"
        using that
        by (metis ‹iefac ℱ' |`| (N |∪| U⇩e⇩r) = finsert (iefac ℱ' C) (iefac ℱ |`| (N |∪| U⇩e⇩r)) |-| {|C|}›
            finsert_iff fminusE iefac_def linorder_cls.neq_iff)

      moreover have "x ≺⇩c C"
        using ‹x ≺⇩c efac C› ‹efac C ≺⇩c C› by order

      ultimately have "ord_res_Interp (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) x ⊫ x"
        using invars
        unfolding ord_res_5_invars_def
        unfolding all_smaller_clauses_true_wrt_respective_Interp_def step_hyps(1,2)
        by blast

      moreover have "ord_res_Interp (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) x =
        ord_res_Interp (fset (iefac ℱ' |`| (N |∪| U⇩e⇩r))) x"
      proof (rule ord_res.Interp_swap_clause_set)
        show "{D. D |∈| iefac ℱ |`| (N |∪| U⇩e⇩r) ∧ (≺⇩c)⇧=⇧= D x} =
          {D. D |∈| iefac ℱ' |`| (N |∪| U⇩e⇩r) ∧ (≺⇩c)⇧=⇧= D x}"
          unfolding ‹iefac ℱ' |`| (N |∪| U⇩e⇩r) = finsert (iefac ℱ' C) (iefac ℱ |`| (N |∪| U⇩e⇩r)) |-| {|C|}›
          using ‹x ≺⇩c efac C› ‹x ≺⇩c C›
          by (metis (no_types, opaque_lifting) finsertCI finsertE fminusE fminusI fsingleton_iff
              iefac_def linorder_cls.less_le_not_le)
      qed

      ultimately show ?thesis
        by argo
    qed

    thus "all_smaller_clauses_true_wrt_respective_Interp N (U⇩e⇩r, ℱ', ℳ, Some (efac C))"
      unfolding all_smaller_clauses_true_wrt_respective_Interp_def by blast

    have "linorder_lit.is_greatest_in_mset (efac C) L"
      using ‹linorder_lit.is_maximal_in_mset C L›
      by (metis ‹efac C ≠ C› ex1_efac_eq_factoring_chain linorder_lit.Uniq_is_maximal_in_mset
          linorder_lit.is_greatest_in_mset_iff_is_maximal_and_count_eq_one
          ord_res.ground_factorings_preserves_maximal_literal
          obtains_positive_greatest_lit_if_efac_not_ident the1_equality')

    have "A ∈ ord_res.production (fset (iefac ℱ' |`| (N |∪| U⇩e⇩r))) D"
      if "ℳ A = Some D" for A D
    proof -
      have "A ∈ dom ℳ"
        using ‹ℳ A = Some D› by blast

      hence "A ∈ ord_res.interp (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) C"
        using dom_ℳ_eq by argo

      have "A ∈ ord_res.production (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) D"
        using invars ‹ℳ A = Some D›
        unfolding ord_res_5_invars_def step_hyps(1,2)
        unfolding atoms_in_model_were_produced_def
        by simp

      hence "linorder_lit.is_greatest_in_mset D (Pos A)"
        by (metis ord_res.mem_productionE)

      moreover have "Pos A ≺⇩l L"
        using ‹A ∈ ord_res.interp (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) C›
        by (smt (verit, del_insts) UN_E ‹A ∈ ord_res.production (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) D›
            calculation dom_ℳ_eq ord_res.interp_def ord_res.less_lit_simps(1)
            ord_res.totalp_less_lit linorder_cls.less_trans
            linorder_lit.is_maximal_in_mset_if_is_greatest_in_mset
            linorder_lit.is_maximal_in_mset_iff linorder_lit.less_irrefl
            linorder_lit.multp_if_maximal_less_that_maximal mem_Collect_eq
            ord_res.less_trm_iff_less_cls_if_mem_production
            pos_literal_in_imp_true_cls step_hyps(3) step_hyps(4) totalpD)

      ultimately have "D ≺⇩c efac C"
        using ‹linorder_lit.is_greatest_in_mset (efac C) L›
        by (metis ord_res.asymp_less_lit ord_res.transp_less_lit
            linorder_lit.is_maximal_in_mset_if_is_greatest_in_mset
            linorder_lit.multp⇩H⇩O_if_maximal_less_that_maximal multp_eq_multp⇩H⇩O)

      have "ord_res.production (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) D =
        ord_res.production (fset (iefac ℱ' |`| (N |∪| U⇩e⇩r))) D"
      proof (rule ord_res.production_swap_clause_set)
        have "D ≺⇩c C"
          using ‹D ≺⇩c efac C› ‹efac C ≺⇩c C› by order
        thus "{Da. Da |∈| iefac ℱ |`| (N |∪| U⇩e⇩r) ∧ (≺⇩c)⇧=⇧= Da D} =
          {Da. Da |∈| iefac ℱ' |`| (N |∪| U⇩e⇩r) ∧ (≺⇩c)⇧=⇧= Da D}"
          using ‹D ≺⇩c efac C›
          unfolding ‹iefac ℱ' |`| (N |∪| U⇩e⇩r) = finsert (iefac ℱ' C) (iefac ℱ |`| (N |∪| U⇩e⇩r)) |-| {|C|}›
          by (metis (no_types, opaque_lifting) finsertE finsertI2 fminus_iff fsingleton_iff
              iefac_def linorder_cls.leD)
      qed

      thus ?thesis
        using ‹A ∈ ord_res.production (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) D› by argo
    qed

    thus "atoms_in_model_were_produced N (U⇩e⇩r, ℱ', ℳ, Some (efac C))"
      unfolding atoms_in_model_were_produced_def by simp

    have "ℳ A = Some x"
      if "x ≺⇩c efac C" and "A ∈ ord_res.production (fset (iefac ℱ' |`| (N |∪| U⇩e⇩r))) x"
      for x A
    proof -
      have "x ≺⇩c C"
        using ‹x ≺⇩c efac C› ‹efac C ≺⇩c C› by order

      moreover have "A ∈ ord_res.production (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) x"
      proof -
        have "ord_res.production (fset (iefac ℱ' |`| (N |∪| U⇩e⇩r))) x =
          ord_res.production (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) x"
        proof (rule ord_res.production_swap_clause_set)
          show "{D. D |∈| iefac ℱ' |`| (N |∪| U⇩e⇩r) ∧ (≺⇩c)⇧=⇧= D x} = {D. D |∈| iefac ℱ |`| (N |∪| U⇩e⇩r) ∧ (≺⇩c)⇧=⇧= D x}"
            using ‹x ≺⇩c efac C› ‹x ≺⇩c C›
            unfolding ‹iefac ℱ' |`| (N |∪| U⇩e⇩r) = finsert (iefac ℱ' C) (iefac ℱ |`| (N |∪| U⇩e⇩r)) |-| {|C|}›
            by (metis (no_types, opaque_lifting) finsert_iff fminus_iff fsingleton_iff iefac_def
                linorder_cls.dual_order.strict_iff_not)
        qed

        thus ?thesis
          using ‹A ∈ ord_res.production (fset (iefac ℱ' |`| (N |∪| U⇩e⇩r))) x› by argo
      qed

      ultimately show ?thesis
        using invars
        unfolding ord_res_5_invars_def step_hyps(1,2)
        unfolding all_produced_atoms_in_model_def
        by simp
    qed

    thus "all_produced_atoms_in_model N (U⇩e⇩r, ℱ', ℳ, Some (efac C))"
      unfolding all_produced_atoms_in_model_def by simp
  qed
next
  case step_hyps: (resolution_bot ℳ D L C U⇩e⇩r' U⇩e⇩r ℳ' ℱ)
  have "ℱ |⊆| N |∪| U⇩e⇩r"
    using invars
    unfolding step_hyps(1,2) ord_res_5_invars_def implicitly_factorized_clauses_subset_def
    by metis

  hence "ℱ |⊆| N |∪| U⇩e⇩r'"
    using step_hyps by blast

  moreover have "linorder_cls.is_least_in_fset (iefac ℱ |`| (N |∪| U⇩e⇩r')) {#}"
    using step_hyps linorder_cls.is_least_in_fset_iff mempty_lesseq_cls by fastforce

  ultimately show ?thesis
    using step_hyps
    using ord_res_5_invars_initial_state
    by (metis ord_res_5_invars_initial_state)
next
  case step_hyps: (resolution_pos ℳ E L D U⇩e⇩r' U⇩e⇩r ℳ' K ℱ)

  hence
    L_max: "ord_res.is_maximal_lit L E" and
    L_neg: "is_neg L"
    using step_hyps by simp_all

  have ℱ_subset: "ℱ |⊆| N |∪| U⇩e⇩r"
    using invars
    unfolding step_hyps(1,2) ord_res_5_invars_def implicitly_factorized_clauses_subset_def
    by metis

  have "eres D E ≠ E"
    using step_hyps by (metis linorder_lit.Uniq_is_maximal_in_mset the1_equality')

  moreover have "eres D E ≼⇩c E"
    using eres_le .

  ultimately have "eres D E ≺⇩c E"
    by order

  have "∀F. is_least_false_clause (iefac ℱ |`| (N |∪| U⇩e⇩r)) F ⟶ E ≼⇩c F"
    using invars
    unfolding ord_res_5_invars_def step_hyps(1,2)
    using next_clause_lt_least_false_clause[of N "(U⇩e⇩r, ℱ, ℳ, Some E)"]
    by simp

  have E_least_false: "is_least_false_clause (iefac ℱ |`| (N |∪| U⇩e⇩r)) E"
    unfolding is_least_false_clause_def linorder_cls.is_least_in_ffilter_iff
  proof (intro conjI ballI impI)
    show "E |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)"
      using invars
      unfolding ord_res_5_invars_def step_hyps(1,2)
      by (metis next_clause_in_factorized_clause_def)
  next
    have "¬ ord_res.interp (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) E ⊫ E"
      using invars
      unfolding ord_res_5_invars_def step_hyps(1,2)
      using ‹¬ dom ℳ ⊫ E› by (metis model_eq_interp_upto_next_clause_def)

    moreover have "ord_res.production (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) E = {}"
    proof -
      have "∄L. is_pos L ∧ ord_res.is_strictly_maximal_lit L E"
        using ‹ord_res.is_maximal_lit L E› ‹is_neg L›
        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 |∪| U⇩e⇩r))) E ⊫ E"
      by simp
  next
    fix F
    assume F_in: "F |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" and "F ≠ E" and
      F_false: "¬ ord_res_Interp (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) F ⊫ F"

    have "¬ F ≺⇩c E"
      using invars
      unfolding ord_res_5_invars_def step_hyps(1,2)
      unfolding all_smaller_clauses_true_wrt_respective_Interp_def
      using F_in F_false
      by (metis option.inject)

    thus "E ≺⇩c F"
      using ‹F ≠ E› by order
  qed

  have L_prod_by_D: "atm_of L ∈ ord_res.production (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) D"
    using invars
    unfolding ord_res_5_invars_def step_hyps(1,2)
    by (metis atoms_in_model_were_produced_def step_hyps(6))

  hence D_prod: "ord_res.production (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) D ≠ {}"
    by (metis empty_iff)

  have "ord_res.is_maximal_lit (-L) D"
    using L_prod_by_D L_neg
    by (metis linorder_lit.is_maximal_in_mset_if_is_greatest_in_mset literal.collapse(2)
        ord_res.mem_productionE uminus_Neg)

  moreover have "-L ≺⇩l L"
    using L_neg
    by (metis Neg_atm_of_iff atm_of_uminus linorder_lit.not_less_iff_gr_or_eq
        linorder_trm.less_imp_not_eq literal.collapse(1) ord_res.less_lit_simps(4) uminus_not_id)

  ultimately have "D ≺⇩c E"
    using L_max linorder_lit.multp_if_maximal_less_that_maximal by metis

  have "eres D E |∉| iefac ℱ |`| (N |∪| U⇩e⇩r)"
  proof (rule notI)
    assume "eres D E |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)"
    moreover have "¬ (E ≺⇩c eres D E)"
      using ‹eres D E ≺⇩c E› by order
    ultimately have "ord_res_Interp (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) (eres D E) ⊫ eres D E"
      using E_least_false ‹eres D E ≠ E›
      unfolding is_least_false_clause_def linorder_cls.is_least_in_ffilter_iff
      by metis
    then show False
      by (metis (no_types, lifting) D_prod E_least_false clause_true_if_resolved_true
          ex1_eres_eq_full_run_ground_resolution full_run_def is_least_false_clause_def
          linorder_cls.is_least_in_fset_ffilterD(2) rtranclpD)
  qed

  moreover have "efac (eres D E) |∉| iefac ℱ |`| (N |∪| U⇩e⇩r)"
  proof (rule notI)
    have "efac (eres D E) ≼⇩c eres D E"
      by (meson efac_subset subset_implies_reflclp_multp)
    hence "¬ (E ≺⇩c efac (eres D E))"
      using ‹eres D E ≺⇩c E› by order
    moreover assume "efac (eres D E) |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)"
    moreover have "efac (eres D E) ≠ E"
      by (metis ‹eres D E ≺⇩c E› efac_properties_if_not_ident(1) linorder_cls.not_less_iff_gr_or_eq)
    ultimately have "ord_res_Interp (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) (efac (eres D E)) ⊫ efac (eres D E)"
      using E_least_false
      unfolding is_least_false_clause_def linorder_cls.is_least_in_ffilter_iff
      by metis
    hence "ord_res_Interp (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) (eres D E) ⊫ eres D E"
      using ‹efac (eres D E) ≼⇩c eres D E› ord_res.entailed_clause_stays_entailed by fastforce
    hence "ord_res_Interp (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) E ⊫ E"
      using clause_true_if_resolved_true
      by (smt (verit) D_prod ex1_eres_eq_full_run_ground_resolution full_run_def rtranclpD)
    moreover have "¬ ord_res_Interp (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) E ⊫ E"
      using E_least_false is_least_false_clause_def linorder_cls.is_least_in_fset_ffilterD(2)
      by blast
    ultimately show False
      by contradiction
  qed

  ultimately have "eres D E |∉| N |∪| U⇩e⇩r"
    unfolding iefac_def by fastforce

  hence "iefac ℱ (eres D E) = eres D E"
    unfolding iefac_def
    using ℱ_subset by auto

  hence "iefac ℱ |`| (N |∪| U⇩e⇩r') = finsert (eres D E) (iefac ℱ |`| (N |∪| U⇩e⇩r))"
    unfolding ‹U⇩e⇩r' = finsert (eres D E) U⇩e⇩r› by simp

  show ?thesis
    unfolding ord_res_5_invars_def step_hyps(1,2)
  proof (intro conjI)
    have "eres D E |∈| iefac ℱ |`| (N |∪| U⇩e⇩r')"
      unfolding ‹iefac ℱ |`| (N |∪| U⇩e⇩r') = finsert (eres D E) (iefac ℱ |`| (N |∪| U⇩e⇩r))› by simp

    thus "next_clause_in_factorized_clause N (U⇩e⇩r', ℱ, ℳ', Some (eres D E))"
      unfolding next_clause_in_factorized_clause_def by simp

    have "ℱ |⊆| N |∪| U⇩e⇩r'"
      unfolding ‹U⇩e⇩r' = finsert (eres D E) U⇩e⇩r›
      using ‹ℱ |⊆| N |∪| U⇩e⇩r› by blast

    thus "implicitly_factorized_clauses_subset N (U⇩e⇩r', ℱ, ℳ', Some (eres D E))"
      unfolding implicitly_factorized_clauses_subset_def by simp

    have dom_ℳ_eq: "dom ℳ = ord_res.interp (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) E"
      using invars
      unfolding step_hyps(1,2) ord_res_5_invars_def model_eq_interp_upto_next_clause_def
      by metis

    have "∀x ∈# E. ¬ dom ℳ ⊫l x"
      using ‹¬ dom ℳ ⊫ E› by (simp add: true_cls_def)

    moreover have "∀x ∈# D. x ≠ -L ⟶ ¬ dom ℳ ⊫l x"
    proof -
      have "∀x ∈# D. x ≠ -L ⟶ ¬ ord_res.interp (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) D ⊫l x"
        using L_prod_by_D by (metis ord_res.mem_productionE true_cls_def)
      moreover have "∀x ∈# D. x ≠ -L ⟶ atm_of x ≺⇩t atm_of (- L)"
        using ‹ord_res.is_maximal_lit (-L) D› L_neg
        by (smt (verit, best) L_prod_by_D atm_of_eq_atm_of linorder_cls.order_refl
            linorder_trm.antisym_conv1 ord_res.less_trm_if_neg ord_res.lesseq_trm_if_pos)
      ultimately have "∀x ∈# D. x ≠ -L ⟶ ¬ ord_res.interp (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) E ⊫l x"
        using ord_res.interp_fixed_for_smaller_literals[
            OF ‹ord_res.is_maximal_lit (-L) D› _ ‹D ≺⇩c E›]
        by fastforce

      then show ?thesis
        unfolding dom_ℳ_eq[symmetric] .
    qed

    moreover have "K ∈# eres D E"
      using ‹ord_res.is_maximal_lit K (eres D E)›
      using linorder_lit.is_maximal_in_mset_iff by metis

    moreover have "∀x ∈# eres D E. x ∈# D ∨ x ∈# E"
      using lit_in_one_of_resolvents_if_in_eres by metis

    moreover have "∀x ∈# eres D E. x ≠ - L"
    proof (intro ballI notI)
      fix x assume "x ∈# eres D E" "x = - L"
      obtain m A D' E' where
        "ord_res.is_strictly_maximal_lit (Pos A) D" and
        "D = add_mset (Pos A) D'" and
        "E = replicate_mset (Suc m) (Neg A) + E'" and
        "Neg A ∉# E'" and
        "eres D E = repeat_mset (Suc m) D' + E'"
        using ‹eres D E ≠ E›[THEN eres_not_identD] by metis

      have "L = Neg A"
        using ‹ord_res.is_strictly_maximal_lit (Pos A) D›
        by (metis L_neg L_prod_by_D Uniq_D ord_res.mem_productionE
            linorder_lit.Uniq_is_greatest_in_mset literal.collapse(2) uminus_Pos)

      have "x ∈# D' ∨ x ∈# E'"
        using ‹x ∈# eres D E›
        unfolding ‹eres D E = repeat_mset (Suc m) D' + E'›
        by (metis member_mset_repeat_mset_Suc union_iff)
      thus False
      proof (elim disjE)
        assume "x ∈# D'"
        hence "Pos A ∈# D'"
          unfolding ‹x = - L› ‹L = Neg A› by simp
        hence "¬ ord_res.is_strictly_maximal_lit (Pos A) D"
          using ‹D = add_mset (Pos A) D'›
          using linorder_lit.is_greatest_in_mset_iff by auto
        thus False
          using ‹ord_res.is_strictly_maximal_lit (Pos A) D› by contradiction
      next
        assume "x ∈# E'"
        hence "Pos A ∈# E'"
          unfolding ‹x = - L› ‹L = Neg A› by simp
        hence "Pos A ∈# E"
          unfolding ‹E = replicate_mset (Suc m) (Neg A) + E'› by simp
        hence "ord_res.production (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) D ⊫l Pos A"
          using L_prod_by_D ‹L = Neg A› by auto
        hence "ord_res.interp (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) E ⊫l Pos A"
          by (metis ‹L = Neg A› dom_ℳ_eq linorder_lit.is_maximal_in_mset_iff
              neg_literal_notin_imp_true_cls step_hyps(3) step_hyps(4) true_lit_simps(1))
        hence "ord_res.interp (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) E ⊫ E"
          using ‹Pos A ∈# E› by blast
        hence "dom ℳ ⊫ E"
          using dom_ℳ_eq by argo
        thus False
          using ‹¬ dom ℳ ⊫ E› by contradiction
      qed
    qed

    ultimately have "¬ dom ℳ ⊫l K"
      by metis

    have "dom ℳ' = ord_res.interp (fset (iefac ℱ |`| (N |∪| U⇩e⇩r'))) (eres D E)"
    proof (intro subset_antisym subsetI)
      fix A :: "'f gterm"
      assume "A ∈ dom ℳ'"
      hence "A ∈ dom ℳ" and "A ≺⇩t atm_of K"
        unfolding ‹ℳ' = restrict_map ℳ {A. A ≺⇩t atm_of K}› by simp_all

      have "A ∈ ord_res.interp (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) E"
        using ‹A ∈ dom ℳ›
        unfolding ‹dom ℳ = ord_res.interp (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) E› .
      hence "A ∈ ord_res.interp (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) (eres D E)"
        using ord_res.interp_fixed_for_smaller_literals ‹ord_res.is_maximal_lit K (eres D E)›
          ‹A ≺⇩t atm_of K› ‹eres D E ≺⇩c E›
        by metis
      thus "A ∈ ord_res.interp (fset (iefac ℱ |`| (N |∪| U⇩e⇩r'))) (eres D E)"
        unfolding ‹iefac ℱ |`| (N |∪| U⇩e⇩r') = finsert (eres D E) (iefac ℱ |`| (N |∪| U⇩e⇩r))›
        using ord_res.interp_insert_greater_clause_strong by simp
    next
      fix A :: "'f gterm"
      assume "A ∈ ord_res.interp (fset (iefac ℱ |`| (N |∪| U⇩e⇩r'))) (eres D E)"
      hence "A ∈ ord_res.interp (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) (eres D E)"
        unfolding ‹iefac ℱ |`| (N |∪| U⇩e⇩r') = finsert (eres D E) (iefac ℱ |`| (N |∪| U⇩e⇩r))›
        using ord_res.interp_insert_greater_clause_strong by simp
      hence "A ∈ ord_res.interp (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) E"
        using ‹eres D E ≺⇩c E› ord_res.interp_subset_if_less_cls by blast
      hence "A ∈ dom ℳ"
        unfolding ‹dom ℳ = ord_res.interp (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) E› .
      
      moreover have "A ≺⇩t atm_of K"
      proof -
        obtain C where
          "C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" and
          "C ≺⇩c eres D E" and
          A_prod_by_C: "A ∈ ord_res.production (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) C"
          using ‹A ∈ ord_res.interp (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) (eres D E)›
          unfolding ord_res.interp_def by blast

        have "ord_res.is_maximal_lit (Pos A) C"
          using A_prod_by_C ord_res.mem_productionE by blast

        hence "A ≼⇩t atm_of K"
          using ‹ord_res.is_maximal_lit K (eres D E)› ‹C ≺⇩c eres D E›
          by (metis linorder_cls.dual_order.asym linorder_lit.multp_if_maximal_less_that_maximal
              linorder_trm.not_le_imp_less literal.collapse(1) ord_res.less_lit_simps(1)
              step_hyps(11))

        moreover have "A ≠ atm_of K"
          using ‹A ∈ dom ℳ› ‹¬ dom ℳ ⊫l K› ‹is_pos K› by force

        ultimately show ?thesis
          by order
      qed

      ultimately show "A ∈ dom ℳ'"
        unfolding ‹ℳ' = restrict_map ℳ {A. A ≺⇩t atm_of K}› by simp
    qed

    thus "model_eq_interp_upto_next_clause N (U⇩e⇩r', ℱ, ℳ', Some (eres D E))"
      unfolding model_eq_interp_upto_next_clause_def by simp

    have "∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c eres D E ⟶
       ord_res_Interp (iefac ℱ ` (fset N ∪ fset U⇩e⇩r')) C ⊫ C"
      by (smt (verit, ccfv_threshold) E_least_false Uniq_def Uniq_is_least_false_clause
          ‹eres D E ≺⇩c E› ‹iefac ℱ |`| (N |∪| U⇩e⇩r') = finsert (eres D E) (iefac ℱ |`| (N |∪| U⇩e⇩r))›
          finite_fset finsert.rep_eq finsertE finsert_absorb
          fset.set_map ord_res.transp_less_cls
          is_least_false_clause_finsert_smaller_false_clause linorder_cls.max.strict_order_iff
          ord_res.interp_insert_greater_clause ord_res.production_insert_greater_clause transpE
          true_cls_iefac_iff union_fset)

    hence "∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r'). C ≺⇩c eres D E ⟶
       ord_res_Interp (iefac ℱ ` (fset N ∪ fset U⇩e⇩r')) C ⊫ C"
      unfolding ‹eres D E ≺⇩c E› ‹iefac ℱ |`| (N |∪| U⇩e⇩r') = finsert (eres D E) (iefac ℱ |`| (N |∪| U⇩e⇩r))›
      by simp

    thus "all_smaller_clauses_true_wrt_respective_Interp N (U⇩e⇩r', ℱ, ℳ', Some (eres D E))"
      unfolding all_smaller_clauses_true_wrt_respective_Interp_def by simp

    have "A ∈ ord_res.production (fset (iefac ℱ |`| (N |∪| U⇩e⇩r'))) C"
      if "ℳ' A = Some C" for A C
    proof -
      have "ℳ A = Some C" and "A ≺⇩t atm_of K"
        unfolding atomize_conj
        using ‹ℳ' A = Some C› ‹ℳ' = restrict_map ℳ {A. A ≺⇩t atm_of K}›
        by (metis Int_iff domI dom_restrict mem_Collect_eq restrict_in)

      hence A_prod_by_C: "A ∈ ord_res.production (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) C"
        using invars
        unfolding step_hyps(1,2) ord_res_5_invars_def atoms_in_model_were_produced_def
        by metis

      moreover have "ord_res.production (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) C =
        ord_res.production (fset (iefac ℱ |`| (N |∪| U⇩e⇩r'))) C"
      proof (rule ord_res.production_swap_clause_set)
        have "ord_res.is_strictly_maximal_lit (Pos A) C"
          using A_prod_by_C ord_res.mem_productionE by metis
        moreover have "Pos A ≺⇩l K"
          using ‹A ≺⇩t atm_of K›
          by (metis Pos_atm_of_iff ord_res.less_lit_simps(1) step_hyps(11))
        ultimately have "C ≺⇩c eres D E"
          using linorder_lit.multp_if_maximal_less_that_maximal step_hyps(10) by blast
        thus "{D. D |∈| iefac ℱ |`| (N |∪| U⇩e⇩r) ∧ (≺⇩c)⇧=⇧= D C} =
          {D. D |∈| iefac ℱ |`| (N |∪| U⇩e⇩r') ∧ (≺⇩c)⇧=⇧= D C}"
          unfolding ‹iefac ℱ |`| (N |∪| U⇩e⇩r') = finsert (eres D E) (iefac ℱ |`| (N |∪| U⇩e⇩r))›
          by auto
      qed

      ultimately show ?thesis
        by argo
    qed

    thus "atoms_in_model_were_produced N (U⇩e⇩r', ℱ, ℳ', Some (eres D E))"
      unfolding atoms_in_model_were_produced_def by simp

    have "ℳ' A = Some C"
      if "C ≺⇩c eres D E" and A_in: "A ∈ ord_res.production (fset (iefac ℱ |`| (N |∪| U⇩e⇩r'))) C"
      for C A
    proof -
      have "C ≺⇩c E"
        using ‹C ≺⇩c eres D E› ‹eres D E ≺⇩c E› by order

      moreover have A_prod_by_C: "A ∈ ord_res.production (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) C"
      proof -
        have "ord_res.production (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) C =
          ord_res.production (fset (iefac ℱ |`| (N |∪| U⇩e⇩r'))) C"
        proof (rule ord_res.production_swap_clause_set)
          show "{D. D |∈| iefac ℱ |`| (N |∪| U⇩e⇩r) ∧ (≺⇩c)⇧=⇧= D C} =
            {D. D |∈| iefac ℱ |`| (N |∪| U⇩e⇩r') ∧ (≺⇩c)⇧=⇧= D C}"
            unfolding ‹iefac ℱ |`| (N |∪| U⇩e⇩r') = finsert (eres D E) (iefac ℱ |`| (N |∪| U⇩e⇩r))›
            using ‹C ≺⇩c eres D E›
            by (metis (no_types, opaque_lifting) finsert_iff linorder_cls.less_le_not_le)
        qed

        thus ?thesis
          using A_in by argo
      qed

      ultimately have "ℳ A = Some C"
        using invars
        unfolding step_hyps(1,2) ord_res_5_invars_def all_produced_atoms_in_model_def
        by metis

      moreover have "A ≺⇩t atm_of K"
      proof -
        have "A ∈ dom ℳ"
          using ‹ℳ A = Some C› by auto

        have "ord_res.is_maximal_lit (Pos A) C"
          using A_prod_by_C ord_res.mem_productionE by blast

        hence "A ≼⇩t atm_of K"
          using ‹ord_res.is_maximal_lit K (eres D E)› ‹C ≺⇩c eres D E›
          by (metis linorder_cls.dual_order.asym linorder_lit.multp_if_maximal_less_that_maximal
              linorder_trm.not_le_imp_less literal.collapse(1) ord_res.less_lit_simps(1)
              step_hyps(11))

        moreover have "A ≠ atm_of K"
          using ‹A ∈ dom ℳ› ‹¬ dom ℳ ⊫l K› ‹is_pos K› by force

        ultimately show ?thesis
          by order
      qed

      ultimately show "ℳ' A = Some C"
        unfolding ‹ℳ' = restrict_map ℳ {A. A ≺⇩t atm_of K}› by simp
    qed

    thus "all_produced_atoms_in_model N (U⇩e⇩r', ℱ, ℳ', Some (eres D E))"
      unfolding all_produced_atoms_in_model_def by simp
  qed
next
  case step_hyps: (resolution_neg ℳ E L D U⇩e⇩r' U⇩e⇩r ℳ' K C ℱ)

  obtain A⇩L where L_def: "L = Neg A⇩L"
    using ‹is_neg L› by (cases L) simp_all

  have "A⇩L ∈ ord_res.production (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) D"
    using invars ‹ℳ (atm_of L) = Some D›
    unfolding step_hyps(1,2) ord_res_5_invars_def atoms_in_model_were_produced_def
    unfolding L_def literal.sel
    by metis

  hence "D |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" and
    "ord_res.is_strictly_maximal_lit (Pos A⇩L) D" and
    D_false: "¬ ord_res.interp (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) D ⊫ D"
    unfolding atomize_conj by (metis ord_res.mem_productionE)

  obtain A⇩K where K_def: "K = Neg A⇩K"
    using ‹is_neg K› by (cases K) simp_all

  have "A⇩K ∈ ord_res.production (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) C"
    using invars ‹ℳ (atm_of K) = Some C›
    unfolding step_hyps(1,2) ord_res_5_invars_def atoms_in_model_were_produced_def
    unfolding K_def literal.sel
    by metis

  hence "C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" and
    "ord_res.is_strictly_maximal_lit (Pos A⇩K) C" and
    C_false: "¬ ord_res.interp (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) C ⊫ C"
    unfolding atomize_conj by (metis ord_res.mem_productionE)

  have "D ≺⇩c E"
    using ‹ord_res.is_strictly_maximal_lit (Pos A⇩L) D› ‹ord_res.is_maximal_lit L E›[unfolded L_def]
    using linorder_lit.multp_if_maximal_less_that_maximal ord_res.less_lit_simps(2) by blast

  have "eres D E ≠ E"
    using ‹ord_res.is_strictly_maximal_lit (Pos A⇩L) D› ‹ord_res.is_maximal_lit L E›[unfolded L_def]
    by (metis L_def eres_ident_iff ex_ground_resolutionI is_pos_def
        linorder_lit.is_greatest_in_mset_iff_is_maximal_and_count_eq_one
        linorder_lit.multp_if_maximal_less_that_maximal linorder_lit.neq_iff
        linorder_trm.dual_order.asym ord_res.less_lit_simps(4) ground_resolution_def step_hyps(5))

  moreover have "eres D E ≼⇩c E"
    using eres_le .

  ultimately have "eres D E ≺⇩c E"
    by order

  have "iefac ℱ (eres D E) = eres D E"
    by (metis (mono_tags, lifting) Uniq_D efac_spec iefac_def is_pos_def
        linorder_lit.Uniq_is_maximal_in_mset step_hyps(10) step_hyps(11))

  hence "iefac ℱ |`| (N |∪| U⇩e⇩r') = finsert (eres D E) (iefac ℱ |`| (N |∪| U⇩e⇩r))"
    unfolding ‹U⇩e⇩r' = finsert (eres D E) U⇩e⇩r› by simp

  hence "{|C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r'). C ≺⇩c eres D E|} =
    {|C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c eres D E|}"
    by auto

  show ?thesis
    unfolding step_hyps(1,2) ord_res_5_invars_def
  proof (intro conjI)
    have "C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r')"
      using ‹C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)›
      unfolding ‹iefac ℱ |`| (N |∪| U⇩e⇩r') = finsert (eres D E) (iefac ℱ |`| (N |∪| U⇩e⇩r))›
      by simp

    thus "next_clause_in_factorized_clause N (U⇩e⇩r', ℱ, ℳ', Some C)"
      unfolding next_clause_in_factorized_clause_def by simp

    have "ℱ |⊆| N |∪| U⇩e⇩r"
      using invars
      unfolding step_hyps(1,2) ord_res_5_invars_def implicitly_factorized_clauses_subset_def
      by metis

    hence "ℱ |⊆| N |∪| U⇩e⇩r'"
      unfolding ‹U⇩e⇩r' = finsert (eres D E) U⇩e⇩r› by blast

    thus "implicitly_factorized_clauses_subset N (U⇩e⇩r', ℱ, ℳ', Some C)"
      unfolding implicitly_factorized_clauses_subset_def by simp

    have "Pos A⇩K ≺⇩l Neg A⇩K"
      by simp

    hence "C ≺⇩c eres D E"
      using ‹ord_res.is_strictly_maximal_lit (Pos A⇩K) C›
        ‹ord_res.is_maximal_lit K (eres D E)›[unfolded K_def]
      using linorder_lit.multp_if_maximal_less_that_maximal by blast

    have "C ≺⇩c E"
      using ‹C ≺⇩c eres D E› ‹eres D E ≺⇩c E› by order

    have "{|x |∈| iefac ℱ |`| (N |∪| U⇩e⇩r'). x ≺⇩c C|} = {|x |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). x ≺⇩c C|}"
      using ‹C ≺⇩c eres D E›
      unfolding ‹iefac ℱ |`| (N |∪| U⇩e⇩r') = finsert (eres D E) (iefac ℱ |`| (N |∪| U⇩e⇩r))›
      by (metis ffilter_eq_ffilter_minus_singleton finsert_absorb fminus_finsert_absorb
          linorder_cls.less_asym)

    hence "ord_res.interp (fset (iefac ℱ |`| (N |∪| U⇩e⇩r'))) C =
      ord_res.interp (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) C"
      using ‹C ≺⇩c eres D E›
      by (simp add: ‹iefac ℱ |`| (N |∪| U⇩e⇩r') = finsert (eres D E) (iefac ℱ |`| (N |∪| U⇩e⇩r))›
          ord_res.interp_insert_greater_clause)

    have dom_ℳ_eq: "dom ℳ = ord_res.interp (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) E"
      using invars
      unfolding step_hyps(1,2) ord_res_5_invars_def model_eq_interp_upto_next_clause_def
      by metis

    have "∀x ∈# E. ¬ dom ℳ ⊫l x"
      using ‹¬ dom ℳ ⊫ E› by (simp add: true_cls_def)

    moreover have "∀x ∈# D. x ≠ -L ⟶ ¬ dom ℳ ⊫l x"
    proof -
      have "∀x ∈# D. x ≠ -L ⟶ ¬ ord_res.interp (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) D ⊫l x"
        using D_false by blast
      moreover have "∀x ∈# D. x ≠ -L ⟶ atm_of x ≺⇩t atm_of (- L)"
        unfolding L_def uminus_Neg literal.sel
        using ‹ord_res.is_strictly_maximal_lit (Pos A⇩L) D›
        by (metis Pos_atm_of_iff ‹A⇩L ∈ ord_res.production (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) D›
            ord_res.less_trm_if_neg ord_res.lesseq_trm_if_pos reflclp_iff)
      ultimately have "∀x ∈# D. x ≠ -L ⟶ ¬ ord_res.interp (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) E ⊫l x"
        using ord_res.interp_fixed_for_smaller_literals
        using ‹ord_res.is_strictly_maximal_lit (Pos A⇩L) D› ‹D ≺⇩c E›
        using L_def by fastforce
      thus ?thesis
        unfolding dom_ℳ_eq[symmetric] .
    qed

    moreover have "K ∈# eres D E"
      using ‹ord_res.is_maximal_lit K (eres D E)›
      using linorder_lit.is_maximal_in_mset_iff by metis

    moreover have "∀x ∈# eres D E. x ∈# D ∨ x ∈# E"
      using lit_in_one_of_resolvents_if_in_eres by metis

    moreover have "∀x ∈# eres D E. x ≠ - L"
    proof (intro ballI notI)
      fix x assume "x ∈# eres D E" "x = - L"
      obtain m A D' E' where
        "ord_res.is_strictly_maximal_lit (Pos A) D" and
        "D = add_mset (Pos A) D'" and
        "E = replicate_mset (Suc m) (Neg A) + E'" and
        "Neg A ∉# E'" and
        "eres D E = repeat_mset (Suc m) D' + E'"
        using ‹eres D E ≠ E›[THEN eres_not_identD] by metis

      have "L = Neg A"
        using ‹ord_res.is_strictly_maximal_lit (Pos A) D›
        by (metis L_def Uniq_D ‹ord_res.is_strictly_maximal_lit (Pos A⇩L) D›
            linorder_lit.Uniq_is_greatest_in_mset literal.inject(1))

      have "x ∈# D' ∨ x ∈# E'"
        using ‹x ∈# eres D E›
        unfolding ‹eres D E = repeat_mset (Suc m) D' + E'›
        by (metis member_mset_repeat_mset_Suc union_iff)
      thus False
      proof (elim disjE)
        assume "x ∈# D'"
        hence "Pos A ∈# D'"
          unfolding ‹x = - L› ‹L = Neg A› by simp
        hence "¬ ord_res.is_strictly_maximal_lit (Pos A) D"
          using ‹D = add_mset (Pos A) D'›
          using linorder_lit.is_greatest_in_mset_iff by auto
        thus False
          using ‹ord_res.is_strictly_maximal_lit (Pos A) D› by contradiction
      next
        assume "x ∈# E'"
        hence "Pos A ∈# E'"
          unfolding ‹x = - L› ‹L = Neg A› by simp
        hence "Pos A ∈# E"
          unfolding ‹E = replicate_mset (Suc m) (Neg A) + E'› by simp
        hence "ord_res.production (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) D ⊫l Pos A"
          using L_def ‹A⇩L ∈ ord_res.production (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) D› ‹L = Neg A›
          by blast
        hence "ord_res.interp (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) E ⊫l Pos A"
          by (metis ‹L = Neg A› dom_ℳ_eq linorder_lit.is_maximal_in_mset_iff
              neg_literal_notin_imp_true_cls step_hyps(3) step_hyps(4) true_lit_simps(1))
        hence "ord_res.interp (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) E ⊫ E"
          using ‹Pos A ∈# E› by blast
        hence "dom ℳ ⊫ E"
          using dom_ℳ_eq by argo
        thus False
          using ‹¬ dom ℳ ⊫ E› by contradiction
      qed
    qed

    ultimately have "¬ dom ℳ ⊫l K"
      by metis

    have "dom ℳ' = ord_res.interp (fset (iefac ℱ |`| (N |∪| U⇩e⇩r'))) C"
    proof (intro subset_antisym subsetI)
      fix A :: "'f gterm"
      assume "A ∈ dom ℳ'"
      hence "A ∈ dom ℳ" and "A ≺⇩t atm_of K"
        unfolding ‹ℳ' = restrict_map ℳ {A. A ≺⇩t atm_of K}› by simp_all

      have "A ∈ ord_res.interp (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) E"
        using ‹A ∈ dom ℳ›
        unfolding ‹dom ℳ = ord_res.interp (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) E› .
      hence "A ∈ ord_res.interp (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) C"
        using ord_res.interp_fixed_for_smaller_literals ‹ord_res.is_maximal_lit K (eres D E)›
          ‹A ≺⇩t atm_of K› ‹C ≺⇩c E›
        by (smt (verit, del_insts) K_def
            ‹A⇩K ∈ ord_res.production (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) C› ‹eres D E ≺⇩c E›
            literal.sel(2) ord_res.lesser_atoms_in_previous_interp_are_in_final_interp
            ord_res.lesser_atoms_not_in_previous_interp_are_not_in_final_interp_if_productive)
      thus "A ∈ ord_res.interp (fset (iefac ℱ |`| (N |∪| U⇩e⇩r'))) C"
        unfolding ‹iefac ℱ |`| (N |∪| U⇩e⇩r') = finsert (eres D E) (iefac ℱ |`| (N |∪| U⇩e⇩r))›
        using ord_res.interp_insert_greater_clause_strong
        by (simp add: ‹C ≺⇩c eres D E›)
    next
      fix A :: "'f gterm"
      assume "A ∈ ord_res.interp (fset (iefac ℱ |`| (N |∪| U⇩e⇩r'))) C"
      hence "A ∈ ord_res.interp (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) C"
        unfolding ‹iefac ℱ |`| (N |∪| U⇩e⇩r') = finsert (eres D E) (iefac ℱ |`| (N |∪| U⇩e⇩r))›
        using ord_res.interp_insert_greater_clause_strong by (simp add: ‹C ≺⇩c eres D E›)
      hence "A ∈ ord_res.interp (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) E"
        using ‹C ≺⇩c E› ord_res.interp_subset_if_less_cls by blast
      hence "A ∈ dom ℳ"
        unfolding ‹dom ℳ = ord_res.interp (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) E› .

      moreover have "A ≺⇩t atm_of K"
      proof -
        obtain B where
          "B |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" and
          "B ≺⇩c C" and
          A_prod_by_B: "A ∈ ord_res.production (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) B"
          using ‹A ∈ ord_res.interp (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) C›
          unfolding ord_res.interp_def by blast

        have "ord_res.is_maximal_lit (Pos A) B"
          using A_prod_by_B ord_res.mem_productionE by blast

        hence "A ≼⇩t atm_of K"
          using ‹ord_res.is_maximal_lit K (eres D E)› ‹C ≺⇩c eres D E›
          by (metis K_def ‹B ≺⇩c C› asympD
              linorder_cls.less_trans linorder_lit.multp_if_maximal_less_that_maximal
              linorder_trm.le_less_linear literal.sel(2)
              ord_res.asymp_less_cls ord_res.less_lit_simps(4))

        moreover have "A ≠ atm_of K"
          using ‹A ∈ dom ℳ› ‹¬ dom ℳ ⊫l K›
          unfolding K_def
          by (metis ‹A ∈ ord_res.interp (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) C›
              ‹A⇩K ∈ ord_res.production (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) C› atm_of_uminus
              linorder_lit.is_greatest_in_mset_iff literal.sel(1) ord_res.mem_productionE
              pos_literal_in_imp_true_cls uminus_Neg)

        ultimately show ?thesis
          by order
      qed

      ultimately show "A ∈ dom ℳ'"
        unfolding ‹ℳ' = restrict_map ℳ {A. A ≺⇩t atm_of K}› by simp
    qed

    thus "model_eq_interp_upto_next_clause N (U⇩e⇩r', ℱ, ℳ', Some C)"
      unfolding model_eq_interp_upto_next_clause_def by simp

    have "∀x |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). x ≺⇩c E ⟶
      ord_res_Interp (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) x ⊫ x"
      using invars
      unfolding step_hyps(1,2) ord_res_5_invars_def all_smaller_clauses_true_wrt_respective_Interp_def
      by simp

    hence "∀x |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). x ≺⇩c C ⟶
      ord_res_Interp (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) x ⊫ x"
      using ‹C ≺⇩c E› by simp

    moreover have "∀x |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). x ≺⇩c C ⟶
      ord_res_Interp (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) x =
      ord_res_Interp (fset (iefac ℱ |`| (N |∪| U⇩e⇩r'))) x"
      unfolding ‹iefac ℱ |`| (N |∪| U⇩e⇩r') = finsert (eres D E) (iefac ℱ |`| (N |∪| U⇩e⇩r))›
      by (metis (no_types, lifting) ‹C ≺⇩c eres D E› finite_fset finsert.rep_eq
          linorder_cls.dual_order.strict_trans2 ord_res.Interp_insert_greater_clause sup2CI)

    ultimately have "∀x |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). x ≺⇩c C ⟶
      ord_res_Interp (iefac ℱ ` (fset N ∪ fset U⇩e⇩r')) x ⊫ x"
      by simp

    hence "∀x |∈| iefac ℱ |`| (N |∪| U⇩e⇩r'). x ≺⇩c C ⟶
      ord_res_Interp (iefac ℱ ` (fset N ∪ fset U⇩e⇩r')) x ⊫ x"
      unfolding ‹iefac ℱ |`| (N |∪| U⇩e⇩r') = finsert (eres D E) (iefac ℱ |`| (N |∪| U⇩e⇩r))›
      using ‹C ≺⇩c eres D E› by auto

    thus "all_smaller_clauses_true_wrt_respective_Interp N (U⇩e⇩r', ℱ, ℳ', Some C)"
      unfolding all_smaller_clauses_true_wrt_respective_Interp_def
      by simp

    have "A ∈ ord_res.production (fset (iefac ℱ |`| (N |∪| U⇩e⇩r'))) C"
      if "ℳ' A = Some C" for A C
    proof -
      have "ℳ A = Some C" and "A ≺⇩t atm_of K"
        unfolding atomize_conj
        using ‹ℳ' A = Some C› ‹ℳ' = restrict_map ℳ {A. A ≺⇩t atm_of K}›
        by (metis Int_iff domI dom_restrict mem_Collect_eq restrict_in)

      hence A_prod_by_C: "A ∈ ord_res.production (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) C"
        using invars
        unfolding step_hyps(1,2) ord_res_5_invars_def atoms_in_model_were_produced_def
        by metis

      moreover have "ord_res.production (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) C =
        ord_res.production (fset (iefac ℱ |`| (N |∪| U⇩e⇩r'))) C"
      proof (rule ord_res.production_swap_clause_set)
        have "ord_res.is_strictly_maximal_lit (Pos A) C"
          using A_prod_by_C ord_res.mem_productionE by metis
        moreover have "Pos A ≺⇩l K"
          using ‹A ≺⇩t atm_of K›
          by (simp add: K_def)
        ultimately have "C ≺⇩c eres D E"
          using linorder_lit.multp_if_maximal_less_that_maximal step_hyps(10) by blast
        thus "{D. D |∈| iefac ℱ |`| (N |∪| U⇩e⇩r) ∧ (≺⇩c)⇧=⇧= D C} =
          {D. D |∈| iefac ℱ |`| (N |∪| U⇩e⇩r') ∧ (≺⇩c)⇧=⇧= D C}"
          unfolding ‹iefac ℱ |`| (N |∪| U⇩e⇩r') = finsert (eres D E) (iefac ℱ |`| (N |∪| U⇩e⇩r))›
          by auto
      qed

      ultimately show ?thesis
        by argo
    qed

    thus "atoms_in_model_were_produced N (U⇩e⇩r', ℱ, ℳ', Some C)"
      unfolding atoms_in_model_were_produced_def by simp

    have "ℳ' A = Some B"
      if "B ≺⇩c C" and A_in: "A ∈ ord_res.production (fset (iefac ℱ |`| (N |∪| U⇩e⇩r'))) B"
      for B A
    proof -
      have "B ≺⇩c eres D E"
        using ‹B ≺⇩c C› ‹C ≺⇩c eres D E› by order
      hence "B ≺⇩c E"
        using ‹eres D E ≺⇩c E› by order

      moreover have A_prod_by_B: "A ∈ ord_res.production (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) B"
      proof -
        have "ord_res.production (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) B =
          ord_res.production (fset (iefac ℱ |`| (N |∪| U⇩e⇩r'))) B"
        proof (rule ord_res.production_swap_clause_set)
          show "{D. D |∈| iefac ℱ |`| (N |∪| U⇩e⇩r) ∧ (≺⇩c)⇧=⇧= D B} =
            {D. D |∈| iefac ℱ |`| (N |∪| U⇩e⇩r') ∧ (≺⇩c)⇧=⇧= D B}"
            unfolding ‹iefac ℱ |`| (N |∪| U⇩e⇩r') = finsert (eres D E) (iefac ℱ |`| (N |∪| U⇩e⇩r))›
            using ‹B ≺⇩c eres D E›
            by (metis (no_types, opaque_lifting) finsert_iff linorder_cls.less_le_not_le)
        qed

        thus ?thesis
          using A_in by argo
      qed

      ultimately have "ℳ A = Some B"
        using invars
        unfolding step_hyps(1,2) ord_res_5_invars_def all_produced_atoms_in_model_def
        by metis

      moreover have "A ≺⇩t atm_of K"
      proof -
        have "A ∈ dom ℳ"
          using ‹ℳ A = Some B› by auto

        have "ord_res.is_maximal_lit (Pos A) B"
          using A_prod_by_B ord_res.mem_productionE by blast

        hence "A ≼⇩t atm_of K"
          using ‹ord_res.is_maximal_lit K (eres D E)› ‹B ≺⇩c eres D E›
          by (metis K_def asympD linorder_lit.multp_if_maximal_less_that_maximal
              linorder_trm.le_less_linear literal.sel(2) ord_res.asymp_less_cls
              ord_res.less_lit_simps(4))

        moreover have "A ≠ atm_of K"
          using ‹A ∈ dom ℳ› ‹¬ dom ℳ ⊫l K›
          using ‹ℳ A = Some B› step_hyps(12) that(1) by force

        ultimately show ?thesis
          by order
      qed

      ultimately show "ℳ' A = Some B"
        unfolding ‹ℳ' = restrict_map ℳ {A. A ≺⇩t atm_of K}› by simp
    qed

    thus "all_produced_atoms_in_model N (U⇩e⇩r', ℱ, ℳ', Some C)"
      unfolding all_produced_atoms_in_model_def by simp
  qed
qed

lemma rtranclp_ord_res_6_preserves_invars:
  assumes steps: "(ord_res_6 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_6_preserves_invars)

lemma ex_ord_res_6_if_not_final:
  assumes
    not_final: "¬ ord_res_6_final S" and
    invars: "∀N s. S = (N, s) ⟶ ord_res_5_invars N s"
  shows "∃S'. ord_res_6_step S S'"
proof -
  from not_final obtain N U⇩e⇩r ℱ ℳ C where
    S_def: "S = (N, (U⇩e⇩r, ℱ, ℳ, Some C))" and "C ≠ {#}"
    unfolding ord_res_6_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_6 N (U⇩e⇩r, ℱ, ℳ, Some C) s'"
  proof (cases "dom ℳ ⊫ C")
    case True
    thus ?thesis
      using ord_res_6.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_6.production[OF C_false L_max L_pos] by metis
      next
        case L_not_striclty_max: False
        thus ?thesis
          using ord_res_6.factoring[OF C_false L_max L_pos L_not_striclty_max 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 |∪| U⇩e⇩r)) C"
        unfolding is_least_false_clause_def linorder_cls.is_least_in_ffilter_iff
      proof (intro conjI ballI impI)
        show "C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)"
          using invars' by (metis next_clause_in_factorized_clause_def)
      next
        have "¬ ord_res.interp (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) C ⊫ C"
          using invars' C_false by (metis model_eq_interp_upto_next_clause_def)
        moreover have "ord_res.production (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) 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 |∪| U⇩e⇩r))) C ⊫ C"
          by simp
      next
        fix D
        assume D_in: "D |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" and "D ≠ C" and
          C_false: "¬ ord_res_Interp (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) 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 |∪| U⇩e⇩r)" and
        "D ≺⇩c C" and
        "ord_res.is_strictly_maximal_lit (Pos A) D" and
        D_prod: "ord_res.production (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) D = {A}"
        using bex_smaller_productive_clause_if_least_false_clause_has_negative_max_lit
          L_max[unfolded Neg] by metis

      hence "∃DC. ground_resolution D C DC"
        unfolding ground_resolution_def
        using L_max Neg ex_ground_resolutionI by blast

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

      hence "eres D C ≺⇩c C"
        using eres_le[of D C] by order

      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))

      show ?thesis
      proof (cases "eres D C = {#}")
        case True
        then show ?thesis
          using ord_res_6.resolution_bot[OF C_false L_max L_neg ‹ℳ (atm_of L) = Some D›] by metis
      next
        case False
        then obtain K where K_max: "ord_res.is_maximal_lit K (eres D C)"
          using linorder_lit.ex_maximal_in_mset by metis
        show ?thesis
        proof (cases K)
          case K_def: (Pos A⇩K)
          hence "is_pos K"
            by  simp
          thus ?thesis
            using ord_res_6.resolution_pos
            using C_false L_max L_neg ‹ℳ (atm_of L) = Some D› ‹eres D C ≠ {#}› K_max by metis
        next
          case K_def: (Neg A⇩K)
          hence K_neg: "is_neg K"
            by simp

          have "¬ ord_res_Interp (fset (finsert (eres D C) (iefac ℱ |`| (N |∪| U⇩e⇩r)))) (eres D C) ⊫ eres D C"
            by (smt (verit) C_least_false D_prod Interp_insert_unproductive K_max K_neg Uniq_D
                ‹eres D C ≠ C› clause_true_if_resolved_true ex1_eres_eq_full_run_ground_resolution
                finite_fset fset_simps(2) full_run_def insert_not_empty is_least_false_clause_def
                linorder_cls.is_least_in_fset_ffilterD(2) linorder_lit.Uniq_is_maximal_in_mset
                linorder_lit.is_maximal_in_mset_if_is_greatest_in_mset rtranclpD
                unproductive_if_nex_strictly_maximal_pos_lit)

          hence eres_least:
            "is_least_false_clause (finsert (eres D C) (iefac ℱ |`| (N |∪| U⇩e⇩r))) (eres D C)"
            using C_least_false ‹eres D C ≺⇩c C›
            by (metis is_least_false_clause_finsert_smaller_false_clause)

          then obtain E where "E |∈| finsert (eres D C) (iefac ℱ |`| (N |∪| U⇩e⇩r))" and
            "E ≺⇩c eres D C" and
            "ord_res.is_strictly_maximal_lit (Pos A⇩K) E" and
            E_prod: "ord_res.production (fset (finsert (eres D C) (iefac ℱ |`| (N |∪| U⇩e⇩r)))) E = {A⇩K}"
            using bex_smaller_productive_clause_if_least_false_clause_has_negative_max_lit
              K_max K_def
            by  metis

          have "ord_res.production (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) E =
            ord_res.production (fset (finsert (eres D C) (iefac ℱ |`| (N |∪| U⇩e⇩r)))) E"
          proof (rule ord_res.production_swap_clause_set)
            have "eres D C |∉| iefac ℱ |`| (N |∪| U⇩e⇩r)"
            proof (rule notI)
              assume "eres D C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)"
              hence "finsert (eres D C) (iefac ℱ |`| (N |∪| U⇩e⇩r)) = iefac ℱ |`| (N |∪| U⇩e⇩r)"
                by blast
              hence "is_least_false_clause (iefac ℱ |`| (N |∪| U⇩e⇩r)) (eres D C)"
                using eres_least by argo
              thus False
                using C_least_false ‹eres D C ≠ C›
                by (metis Uniq_D Uniq_is_least_false_clause)
            qed

            thus "{D. D |∈| iefac ℱ |`| (N |∪| U⇩e⇩r) ∧ (≺⇩c)⇧=⇧= D E} =
              {Da. Da |∈| finsert (eres D C) (iefac ℱ |`| (N |∪| U⇩e⇩r)) ∧ (≺⇩c)⇧=⇧= Da E}"
              by (metis (mono_tags, lifting) ‹E ≺⇩c eres D C› finsert_iff linorder_cls.leD)
          qed

          also have "… = {A⇩K}"
            using E_prod .

          finally have "ord_res.production (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) E = {A⇩K}" .

          hence "ℳ (atm_of K) = Some E"
            using invars'
            unfolding ord_res_5_invars_def all_produced_atoms_in_model_def
            by (metis K_def ‹E ≺⇩c eres D C› eres_le insertI1 linorder_cls.dual_order.strict_trans1
                literal.sel(2))

          thus ?thesis
            using ord_res_6.resolution_neg
            using C_false L_max L_neg ‹ℳ (atm_of L) = Some D› ‹eres D C ≠ {#}› K_max K_neg by metis
        qed
      qed
    qed
  qed
  thus ?thesis
    using S_def ord_res_6_step.simps by metis
qed

lemma ord_res_6_safe_state_if_invars:
  "safe_state ord_res_6_step ord_res_6_final (N, s)" if invars: "ord_res_5_invars N s" for N s
proof -
  {
    fix S'
    assume "ord_res_6_semantics.eval (N, s) S'" and stuck: "stuck_state ord_res_6_step S'"
    then obtain s' where "S' = (N, s')" and "(ord_res_6 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_6_step.cases prod.inject)
    qed
    hence "ord_res_5_invars N s'"
      using invars rtranclp_ord_res_6_preserves_invars by metis
    hence "¬ ord_res_6_final S' ⟹ ∃S''. ord_res_6_step S' S''"
      using ex_ord_res_6_if_not_final[of S'] ‹S' = (N, s')› by blast
    hence "ord_res_6_final S'"
      using stuck[unfolded stuck_state_def] by argo
  }
  thus ?thesis
    unfolding safe_state_def stuck_state_def by metis
qed

lemma ex_model_build_from_least_clause_to_any_less_than_least_false:
  assumes
    ℱ_subset: "ℱ |⊆| N |∪| U⇩e⇩r" and
    C_least: "linorder_cls.is_least_in_fset (iefac ℱ |`| (N |∪| U⇩e⇩r)) C" and
    D_in: "D |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" and
    D_lt_least_false: "∀E. is_least_false_clause (iefac ℱ |`| (N |∪| U⇩e⇩r)) E ⟶ D ≼⇩c E" and
    "C ≼⇩c D"
  shows "∃ℳ. (ord_res_5 N)⇧*⇧* (U⇩e⇩r, ℱ, Map.empty, Some C) (U⇩e⇩r, ℱ, ℳ, Some D)"
  using ord_res.wfP_less_cls D_in ‹C ≼⇩c D› D_lt_least_false
proof (induction D rule: wfp_induct_rule)
  case (less D)

  have invars: "ord_res_5_invars N (U⇩e⇩r, ℱ, Map.empty, Some C)"
    using ord_res_5_invars_initial_state ℱ_subset C_least by metis

  define clauses_lt_D :: "'f gclause fset" where
    "clauses_lt_D = {|C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c D|}"

  show ?case
  proof (cases "clauses_lt_D = {||}")
    case True
    hence "C = D"
      unfolding clauses_lt_D_def
      using C_least ‹C ≼⇩c D›
      by (metis fempty_iff ffmember_filter linorder_cls.antisym_conv3
          linorder_cls.is_least_in_fset_iff linorder_cls.less_le_not_le)
    thus ?thesis
      by blast
  next
    case False

    obtain x where x_greatest: "linorder_cls.is_greatest_in_fset clauses_lt_D x"
      using False linorder_cls.ex_greatest_in_fset by metis

    have "x ≺⇩c D" and "x |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)"
      using x_greatest by (simp_all add: clauses_lt_D_def linorder_cls.is_greatest_in_fset_iff)

    moreover have "C ≼⇩c x"
      using x_greatest C_least
      by (metis clauses_lt_D_def ffmember_filter linorder_cls.is_greatest_in_fset_iff
          linorder_cls.not_less nbex_less_than_least_in_fset)

    moreover have "⋀E. is_least_false_clause (iefac ℱ |`| (N |∪| U⇩e⇩r)) E ⟹ x ≺⇩c E"
      using ‹x ≺⇩c D› less.prems by force

    ultimately obtain ℳ where
      IH: "(ord_res_5 N)⇧*⇧* (U⇩e⇩r, ℱ, Map.empty, Some C) (U⇩e⇩r, ℱ, ℳ, Some x)"
      using less.IH by blast

    moreover have "∃ℳ'. ord_res_5 N (U⇩e⇩r, ℱ, ℳ, Some x) (U⇩e⇩r, ℱ, ℳ', Some D)"
    proof -
      have "linorder_cls.is_least_in_fset (ffilter ((≺⇩c) x) (iefac ℱ |`| (N |∪| U⇩e⇩r))) D"
        using x_greatest[unfolded clauses_lt_D_def]
        by (smt (verit) ffmember_filter less.prems(1) linorder_cls.is_greatest_in_fset_iff
            linorder_cls.is_least_in_ffilter_iff linorder_cls.not_less_iff_gr_or_eq)
      hence next_clause_eq: "The_optional (linorder_cls.is_least_in_fset
        (ffilter ((≺⇩c) x) (iefac ℱ |`| (N |∪| U⇩e⇩r)))) = Some D"
        by (metis linorder_cls.Uniq_is_least_in_fset The_optional_eq_SomeI)

      have x_true: "ord_res_Interp (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) x ⊫ x"
        using less.prems
        unfolding is_least_false_clause_def linorder_cls.is_least_in_ffilter_iff
        
        by (metis ‹⋀E. is_least_false_clause (iefac ℱ |`| (N |∪| U⇩e⇩r)) E ⟹ x ≺⇩c E› ‹x |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)›
            ex_false_clause_iff finsert_absorb is_least_false_clause_finsert_smaller_false_clause
            linorder_cls.order.irrefl ex_false_clause_def)

      show ?thesis
      proof (cases "dom ℳ ⊫ x")
        case True
        thus ?thesis
          using ord_res_5.skip next_clause_eq by metis
      next
        case False
        hence "¬ ord_res.interp (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) x ⊫ x"
          using rtranclp_ord_res_5_preserves_invars[OF IH invars, unfolded ord_res_5_invars_def,
              simplified]
          by (simp add: model_eq_interp_upto_next_clause_def)

        thus ?thesis
          using ord_res_5.production[OF False] next_clause_eq
          using x_true
          by (metis Un_empty_right linorder_lit.is_maximal_in_mset_if_is_greatest_in_mset
              unproductive_if_nex_strictly_maximal_pos_lit)
      qed
    qed

    ultimately show ?thesis
      by (smt (verit) rtranclp.rtrancl_into_rtrancl)
  qed
qed

lemma full_rtranclp_ord_res_5_run_upto:
  assumes
    "ord_res_6 N (U⇩e⇩r, ℱ, ℳ, Some E) (U⇩e⇩r', ℱ', ℳ', Some D)" and
    invars: "ord_res_5_invars N (U⇩e⇩r', ℱ', ℳ', Some D)" and
    ℳ'_def: "ℳ' = restrict_map ℳ {A. ∃K. linorder_lit.is_maximal_in_mset D K ∧ A ≺⇩t atm_of K}" and
    C_least: "linorder_cls.is_least_in_fset (iefac ℱ' |`| (N |∪| U⇩e⇩r')) C"
  shows "(ord_res_5 N)⇧*⇧* (U⇩e⇩r', ℱ', Map.empty, Some C) (U⇩e⇩r', ℱ', ℳ', Some D)"
proof -
  have D_in: "D |∈| iefac ℱ' |`| (N |∪| U⇩e⇩r')"
    using invars
    by (metis next_clause_in_factorized_clause_def ord_res_5_invars_def)

  have "ℱ' |⊆| N |∪| U⇩e⇩r'"
    using invars
    by (metis implicitly_factorized_clauses_subset_def ord_res_5_invars_def)

  moreover have "C ≼⇩c D"
    using C_least D_in
    by (metis linorder_cls.dual_order.strict_iff_order linorder_cls.is_least_in_fset_iff
        linorder_cls.le_cases)

  moreover have "∀F. is_least_false_clause (iefac ℱ' |`| (N |∪| U⇩e⇩r')) F ⟶ D ≼⇩c F"
    using invars le_least_false_clause by metis

  ultimately obtain ℳ'' where
    steps: "(ord_res_5 N)⇧*⇧* (U⇩e⇩r', ℱ', Map.empty, Some C) (U⇩e⇩r', ℱ', ℳ'', Some D)"
    using C_least D_in
    by (metis ex_model_build_from_least_clause_to_any_less_than_least_false)

  have "ord_res_5_invars N (U⇩e⇩r', ℱ', Map.empty, Some C)"
    using ‹ℱ' |⊆| N |∪| U⇩e⇩r'› C_least ord_res_5_invars_initial_state by metis

  hence "ord_res_5_invars N (U⇩e⇩r', ℱ', ℳ'', Some D)"
    using ‹(ord_res_5 N)⇧*⇧* (U⇩e⇩r', ℱ', λx. None, Some C) (U⇩e⇩r', ℱ', ℳ'', Some D)›
      rtranclp_ord_res_5_preserves_invars by metis

  hence ℳ''_spec:
    "dom ℳ'' = ord_res.interp (fset (iefac ℱ' |`| (N |∪| U⇩e⇩r'))) D"
    "∀A C. ℳ'' A = Some C ⟶ A ∈ ord_res.production (fset (iefac ℱ' |`| (N |∪| U⇩e⇩r'))) C"
    "∀C A. C ≺⇩c D ⟶ A ∈ ord_res.production (fset (iefac ℱ' |`| (N |∪| U⇩e⇩r'))) C ⟶ ℳ'' A = Some C"
    unfolding ord_res_5_invars_def
    unfolding model_eq_interp_upto_next_clause_def atoms_in_model_were_produced_def
      all_produced_atoms_in_model_def
    by metis+

  have "ℳ' = ℳ''"
  proof (cases "D = {#}")
    case True
    have "ℳ' = Map.empty"
    proof -
      have "∄K. ord_res.is_maximal_lit K D ∧ A ≺⇩t atm_of K" for A
        unfolding ‹D = {#}›
        by (simp add: linorder_lit.is_maximal_in_mset_iff)
      hence "{A. ∃K. ord_res.is_maximal_lit K D ∧ A ≺⇩t atm_of K} = {}"
        by simp
      thus ?thesis
        unfolding ℳ'_def by auto
    qed

    also have "Map.empty = ℳ''"
    proof -
      have "ord_res.interp (fset (iefac ℱ' |`| (N |∪| U⇩e⇩r'))) D = {}"
        unfolding ‹D = {#}› by simp
      thus ?thesis
        using ℳ''_spec(1) by simp
    qed

    finally show ?thesis .
  next
    case False
    then obtain K where "ord_res.is_maximal_lit K D"
      using linorder_lit.ex_maximal_in_mset by metis
    hence "{A. ∃K. ord_res.is_maximal_lit K D ∧ A ≺⇩t atm_of K} = {A. A ≺⇩t atm_of K}"
      by (metis (no_types, lifting) linorder_lit.Uniq_is_maximal_in_mset the1_equality')
    hence ℳ'_def': "ℳ' = restrict_map ℳ {A. A ≺⇩t atm_of K}"
      unfolding ℳ'_def by argo

    show ?thesis
    proof (intro ext)
      fix x
      have ℳ'_spec:
        "dom ℳ' = ord_res.interp (fset (iefac ℱ' |`| (N |∪| U⇩e⇩r'))) D"
        "∀A C. ℳ' A = Some C ⟶ A ∈ ord_res.production (fset (iefac ℱ' |`| (N |∪| U⇩e⇩r'))) C"
        "∀C A. C ≺⇩c D ⟶ A ∈ ord_res.production (fset (iefac ℱ' |`| (N |∪| U⇩e⇩r'))) C ⟶ ℳ' A = Some C"
        using invars
        unfolding ord_res_5_invars_def
        unfolding model_eq_interp_upto_next_clause_def atoms_in_model_were_produced_def
          all_produced_atoms_in_model_def
        by metis+

      have "dom ℳ' = dom ℳ''"
        using ℳ'_spec(1) ℳ''_spec(1) by argo

      moreover have "∀A C. ℳ' A = Some C ⟷ ℳ'' A = Some C"
        using ℳ'_spec(2) ℳ''_spec(2)
        by (smt (verit, del_insts) calculation domD domI linorder_cls.less_irrefl linorder_cls.neqE
            ord_res.less_trm_iff_less_cls_if_mem_production)

      ultimately show "ℳ' x = ℳ'' x"
        by (metis domD domIff)
    qed
  qed

  thus ?thesis
    using ‹(ord_res_5 N)⇧*⇧* (U⇩e⇩r', ℱ', Map.empty, Some C) (U⇩e⇩r', ℱ', ℳ'', Some D)› by argo
qed

end

end