Theory ORD_RES_8

theory ORD_RES_8
  imports
    Background
    Implicit_Exhaustive_Factorization
    Exhaustive_Resolution
    Clause_Could_Propagate
begin

section ‹ORD-RES-8 (atom-guided literal trail construction)›

type_synonym 'f ord_res_8_state =
  "'f gclause fset ×'f gclause fset × 'f gclause fset × ('f gliteral × 'f gclause option) list"

context simulation_SCLFOL_ground_ordered_resolution begin

inductive ord_res_8 where
  decide_neg: "
    ¬ (∃C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). trail_false_cls Γ C) ⟹
    linorder_trm.is_least_in_fset {|A⇩2 |∈| atms_of_clss (N |∪| U⇩e⇩r).
      ∀A⇩1 |∈| trail_atms Γ. A⇩1 ≺⇩t A⇩2|} A ⟹
    ¬ (∃C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). clause_could_propagate Γ C (Pos A)) ⟹
    Γ' = (Neg A, None) # Γ ⟹
    ord_res_8 N (U⇩e⇩r, ℱ, Γ) (U⇩e⇩r, ℱ, Γ')" |

  propagate: "
    ¬ (∃C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). trail_false_cls Γ C) ⟹
    linorder_trm.is_least_in_fset {|A⇩2 |∈| atms_of_clss (N |∪| U⇩e⇩r).
      ∀A⇩1 |∈| trail_atms Γ. A⇩1 ≺⇩t A⇩2|} A ⟹
    linorder_cls.is_least_in_fset {|C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r).
      clause_could_propagate Γ C (Pos A)|} C ⟹
    linorder_lit.is_greatest_in_mset C (Pos A) ⟹
    Γ' = (Pos A, Some C) # Γ ⟹
    ord_res_8 N (U⇩e⇩r, ℱ, Γ) (U⇩e⇩r, ℱ, Γ')" |

  factorize: "
    ¬ (∃C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). trail_false_cls Γ C) ⟹
    linorder_trm.is_least_in_fset {|A⇩2 |∈| atms_of_clss (N |∪| U⇩e⇩r).
      ∀A⇩1 |∈| trail_atms Γ. A⇩1 ≺⇩t A⇩2|} A ⟹
    linorder_cls.is_least_in_fset {|C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r).
      clause_could_propagate Γ C (Pos A)|} C ⟹
    ¬ linorder_lit.is_greatest_in_mset C (Pos A) ⟹
    ℱ' = finsert C ℱ ⟹
    ord_res_8 N (U⇩e⇩r, ℱ, Γ) (U⇩e⇩r, ℱ', Γ)" |

  resolution: "
    linorder_cls.is_least_in_fset {|D |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). trail_false_cls Γ D|} D ⟹
    linorder_lit.is_maximal_in_mset D (Neg A) ⟹
    map_of Γ (Pos A) = Some (Some C) ⟹
    U⇩e⇩r' = finsert (eres C D) U⇩e⇩r ⟹
    Γ' = dropWhile (λLn. ∀K.
      linorder_lit.is_maximal_in_mset (eres C D) K ⟶ atm_of K ≼⇩t atm_of (fst Ln)) Γ ⟹
    ord_res_8 N (U⇩e⇩r, ℱ, Γ) (U⇩e⇩r', ℱ, Γ')"

lemma right_unique_ord_res_8:
  fixes N :: "'f gclause fset"
  shows "right_unique (ord_res_8 N)"
proof (rule right_uniqueI)
  fix x y z
  assume step1: "ord_res_8 N x y" and step2: "ord_res_8 N x z"
  show "y = z"
    using step1
  proof (cases N x y rule: ord_res_8.cases)
    case step1_hyps: (decide_neg ℱ U⇩e⇩r Γ A Γ')
    show ?thesis
      using step2 unfolding ‹x = (U⇩e⇩r, ℱ, Γ)›
    proof (cases N "(U⇩e⇩r, ℱ, Γ)" z rule: ord_res_8.cases)
      case (decide_neg A Γ')
      with step1_hyps show ?thesis
        by (metis (no_types, lifting) linorder_trm.dual_order.asym linorder_trm.is_least_in_fset_iff)
    next
      case (propagate A2 C2 Γ2')
      with step1_hyps have False
        by (metis (no_types, lifting) linorder_cls.is_least_in_fset_ffilterD(1)
            linorder_cls.is_least_in_fset_ffilterD(2) linorder_trm.dual_order.asym
            linorder_trm.is_least_in_fset_iff)
      thus ?thesis ..
    next
      case (factorize A2 C2 ℱ2')
      with step1_hyps have False
        by (metis (no_types, lifting) linorder_cls.is_least_in_fset_ffilterD(1)
            linorder_cls.is_least_in_fset_ffilterD(2) linorder_trm.dual_order.asym
            linorder_trm.is_least_in_fset_iff)
      thus ?thesis ..
    next
      case (resolution D2 A2 C2 U⇩e⇩r2' Γ2')
      with step1_hyps have False
        by (metis linorder_cls.is_least_in_ffilter_iff)
      thus ?thesis ..
    qed
  next
    case step1_hyps: (propagate ℱ U⇩e⇩r Γ A C Γ')
    show ?thesis
      using step2 unfolding ‹x = (U⇩e⇩r, ℱ, Γ)›
    proof (cases N "(U⇩e⇩r, ℱ, Γ)" z rule: ord_res_8.cases)
      case (decide_neg A2 Γ2')
      with step1_hyps have False
        by (metis (no_types, lifting) linorder_cls.is_least_in_fset_ffilterD(1)
            linorder_cls.is_least_in_fset_ffilterD(2) linorder_trm.dual_order.asym
            linorder_trm.is_least_in_fset_iff)
      thus ?thesis ..
    next
      case (propagate A2 C2 Γ2')
      with step1_hyps show ?thesis
        by (metis (no_types, lifting) linorder_cls.Uniq_is_least_in_fset
            linorder_trm.dual_order.asym linorder_trm.is_least_in_fset_iff The_optional_eq_SomeI)
    next
      case (factorize A2 C2 ℱ2')
      with step1_hyps have False
        by (metis (no_types, lifting) linorder_cls.Uniq_is_least_in_fset
            linorder_trm.Uniq_is_least_in_fset the1_equality')
      thus ?thesis ..
    next
      case (resolution D2 A2 C2 U⇩e⇩r2' Γ2')
      with step1_hyps have False
        by (metis linorder_cls.is_least_in_ffilter_iff)
      thus ?thesis ..
    qed
  next
    case step1_hyps: (factorize ℱ U⇩e⇩r Γ A C ℱ')
    show ?thesis
      using step2 unfolding ‹x = (U⇩e⇩r, ℱ, Γ)›
    proof (cases N "(U⇩e⇩r, ℱ, Γ)" z rule: ord_res_8.cases)
      case (decide_neg A2 Γ2')
      with step1_hyps have False
        by (metis (no_types, lifting) linorder_cls.is_least_in_fset_ffilterD(1)
            linorder_cls.is_least_in_fset_ffilterD(2) linorder_trm.dual_order.asym
            linorder_trm.is_least_in_fset_iff)
      thus ?thesis ..
    next
      case (propagate A2 C2 Γ2')
      with step1_hyps have False
        by (metis (no_types, lifting) linorder_cls.Uniq_is_least_in_fset
            linorder_trm.Uniq_is_least_in_fset the1_equality')
      thus ?thesis ..
    next
      case (factorize A2 C2 ℱ2')
      with step1_hyps show ?thesis
        by (metis (no_types, lifting) linorder_cls.Uniq_is_least_in_fset
            linorder_trm.Uniq_is_least_in_fset the1_equality')
    next
      case (resolution D2 A2 C2 U⇩e⇩r2' Γ2')
      with step1_hyps have False
        by (metis linorder_cls.is_least_in_ffilter_iff)
      thus ?thesis ..
    qed
  next
    case step1_hyps: (resolution Γ ℱ U⇩e⇩r D A C U⇩e⇩r' Γ')
    show ?thesis
      using step2 unfolding ‹x = (U⇩e⇩r, ℱ, Γ)›
    proof (cases N "(U⇩e⇩r, ℱ, Γ)" z rule: ord_res_8.cases)
      case (decide_neg A Γ')
      with step1_hyps have False
        by (metis (no_types, opaque_lifting) linorder_cls.is_least_in_ffilter_iff)
      thus ?thesis ..
    next
      case (propagate A C Γ')
      with step1_hyps have False
        by (metis (no_types, opaque_lifting) linorder_cls.is_least_in_ffilter_iff)
      thus ?thesis ..
    next
      case (factorize A C ℱ')
      with step1_hyps have False
        by (metis (no_types, opaque_lifting) linorder_cls.is_least_in_ffilter_iff)
      thus ?thesis ..
    next
      case step2_hyps: (resolution D2 A2 C2 U⇩e⇩r2' Γ2')
      have "D2 = D"
        using ‹linorder_cls.is_least_in_fset (ffilter (trail_false_cls Γ) (iefac ℱ |`| (N |∪| U⇩e⇩r))) D›
        using ‹linorder_cls.is_least_in_fset (ffilter (trail_false_cls Γ) (iefac ℱ |`| (N |∪| U⇩e⇩r))) D2›
        by (metis linorder_cls.Uniq_is_least_in_fset Uniq_D)

      have "A2 = A"
        using ‹linorder_lit.is_maximal_in_mset D (Neg A)›
        using ‹linorder_lit.is_maximal_in_mset D2 (Neg A2)›
        unfolding ‹D2 = D›
        by (metis Uniq_D linorder_lit.Uniq_is_maximal_in_mset literal.sel(2))

      have "C2 = C"
        using step1_hyps(5) step2_hyps(4)
        unfolding ‹A2 = A›
        by simp

      show ?thesis
        unfolding ‹y = (U⇩e⇩r', ℱ, Γ')› ‹z = (U⇩e⇩r2', ℱ, Γ2')› prod.inject
      proof (intro conjI)
        show "U⇩e⇩r' = U⇩e⇩r2'"
          unfolding ‹U⇩e⇩r' = finsert (eres C D) U⇩e⇩r› ‹U⇩e⇩r2' = finsert (eres C2 D2) U⇩e⇩r›
          unfolding ‹D2 = D› ‹C2 = C› ..
      next
        show "ℱ = ℱ" ..
      next
        show "Γ' = Γ2'"
          using step1_hyps(7) step2_hyps(6)
          unfolding ‹D2 = D› ‹C2 = C›
          by argo
      qed
    qed
  qed
qed

inductive ord_res_8_final :: "'f ord_res_8_state ⇒ bool" where
  model_found: "
    ¬ (∃A |∈| atms_of_clss (N |∪| U⇩e⇩r). A |∉| trail_atms Γ) ⟹
    ¬ (∃C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). trail_false_cls Γ C) ⟹
    ord_res_8_final (N, U⇩e⇩r, ℱ, Γ)" |

  contradiction_found: "
    {#} |∈| iefac ℱ |`| (N |∪| U⇩e⇩r) ⟹
    ord_res_8_final (N, U⇩e⇩r, ℱ, Γ)"

sublocale ord_res_8_semantics: semantics where
  step = "constant_context ord_res_8" and
  final = ord_res_8_final
proof unfold_locales
  fix S :: "'f ord_res_8_state"

  obtain
    N U⇩e⇩r ℱ :: "'f gterm clause fset" and
    Γ :: "('f gterm literal × 'f gterm literal multiset option) list" where
    S_def: "S = (N, U⇩e⇩r, ℱ, Γ)"
    by (metis prod.exhaust)

  assume "ord_res_8_final S"

  hence "∄x. ord_res_8 N (U⇩e⇩r, ℱ, Γ) x"
    unfolding S_def
  proof (cases "(N, U⇩e⇩r, ℱ, Γ)" rule: ord_res_8_final.cases)
    case model_found

    have "∄A. linorder_trm.is_least_in_fset {|A⇩2 |∈| atms_of_clss (N |∪| U⇩e⇩r).
      ∀A⇩1 |∈| trail_atms Γ. A⇩1 ≺⇩t A⇩2|} A"
      using ‹¬ (∃A|∈|atms_of_clss (N |∪| U⇩e⇩r). A |∉| trail_atms Γ)›
      using linorder_trm.is_least_in_ffilter_iff by fastforce

    moreover have "∄C. linorder_cls.is_least_in_fset
      (ffilter (trail_false_cls Γ) (iefac ℱ |`| (N |∪| U⇩e⇩r))) C"
      using ‹¬ fBex (iefac ℱ |`| (N |∪| U⇩e⇩r)) (trail_false_cls Γ)›
      by (metis linorder_cls.is_least_in_ffilter_iff)

    ultimately show ?thesis
      unfolding ord_res_8.simps by blast
  next
    case contradiction_found

    hence "∃C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). trail_false_cls Γ C"
      using trail_false_cls_mempty by metis

    moreover have "∄D A. linorder_cls.is_least_in_fset (ffilter (trail_false_cls Γ)
      (iefac ℱ |`| (N |∪| U⇩e⇩r))) D ∧ ord_res.is_maximal_lit (Neg A) D"
      by (metis empty_iff linorder_cls.is_least_in_ffilter_iff linorder_cls.leD
          linorder_lit.is_maximal_in_mset_iff local.contradiction_found(1) mempty_lesseq_cls
          set_mset_empty trail_false_cls_mempty)

    ultimately show ?thesis
      unfolding ord_res_8.simps by blast
  qed

  thus "finished (constant_context ord_res_8) S"
    by (simp add: S_def finished_def constant_context.simps)
qed

definition trail_is_sorted where
  "trail_is_sorted N s ⟷
    (∀U⇩e⇩r ℱ Γ. s = (U⇩e⇩r, ℱ, Γ) ⟶
      sorted_wrt (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) Γ)"

lemma ord_res_8_preserves_trail_is_sorted:
  assumes
    step: "ord_res_8 N s s'" and
    invar: "trail_is_sorted N s"
  shows "trail_is_sorted N s'"
  using step
proof (cases N s s' rule: ord_res_8.cases)
  case step_hyps: (decide_neg ℱ U⇩e⇩r Γ A Γ')

  have "∀x |∈| trail_atms Γ. x ≺⇩t A"
    using step_hyps unfolding linorder_trm.is_least_in_ffilter_iff by simp

  hence "∀x ∈ set Γ. atm_of (fst x) ≺⇩t A"
    by (simp add: fset_trail_atms)

  moreover have "sorted_wrt (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) Γ"
    using invar by (simp add: ‹s = (U⇩e⇩r, ℱ, Γ)› trail_is_sorted_def)

  ultimately have "sorted_wrt (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) Γ'"
    by (simp add: ‹Γ' = (Neg A, None) # Γ›)

  thus ?thesis
    by (simp add: ‹s' = (U⇩e⇩r, ℱ, Γ')› trail_is_sorted_def)
next
  case step_hyps: (propagate ℱ U⇩e⇩r Γ A C Γ')

  have "∀x |∈| trail_atms Γ. x ≺⇩t A"
    using step_hyps unfolding linorder_trm.is_least_in_ffilter_iff by simp

  hence "∀x ∈ set Γ. atm_of (fst x) ≺⇩t A"
    by (simp add: fset_trail_atms)

  moreover have "sorted_wrt (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) Γ"
    using invar by (simp add: ‹s = (U⇩e⇩r, ℱ, Γ)› trail_is_sorted_def)

  ultimately have "sorted_wrt (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) Γ'"
    by (simp add: ‹Γ' = (Pos A, Some C) # Γ›)

  thus ?thesis
    by (simp add: ‹s' = (U⇩e⇩r, ℱ, Γ')› trail_is_sorted_def)
next
  case (factorize ℱ U⇩e⇩r Γ A C ℱ')

  have "sorted_wrt (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) Γ"
    using invar by (simp add: ‹s = (U⇩e⇩r, ℱ, Γ)› trail_is_sorted_def)

  thus ?thesis
    by (simp add: ‹s' = (U⇩e⇩r, ℱ', Γ)› trail_is_sorted_def)
next
  case step_hyps: (resolution Γ ℱ U⇩e⇩r D A C U⇩e⇩r' Γ')

  have "sorted_wrt (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) Γ"
    using invar by (simp add: ‹s = (U⇩e⇩r, ℱ, Γ)› trail_is_sorted_def)

  hence "sorted_wrt (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) Γ'"
    unfolding step_hyps(7) by (rule sorted_wrt_dropWhile)

  thus ?thesis
    by (simp add: ‹s' = (U⇩e⇩r', ℱ, Γ')› trail_is_sorted_def)
qed

inductive trail_annotations_invars
  for N :: "'f gterm literal multiset fset"
  where
    Nil:
      "trail_annotations_invars N (U⇩e⇩r, ℱ, [])" |
    Cons_None:
      "trail_annotations_invars N (U⇩e⇩r, ℱ, (L, None) # Γ)"
      if "trail_annotations_invars N (U⇩e⇩r, ℱ, Γ)" |
    Cons_Some:
      "trail_annotations_invars N (U⇩e⇩r, ℱ, (L, Some D) # Γ)"
      if "linorder_lit.is_greatest_in_mset D L" and
         "D |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" and
         "trail_false_cls Γ {#K ∈# D. K ≠ L#}" and
         "linorder_cls.is_least_in_fset
           {|D |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). clause_could_propagate Γ D L|} D" and
         "trail_annotations_invars N (U⇩e⇩r, ℱ, Γ)"

lemma
  assumes
    "linorder_lit.is_greatest_in_mset C L" and
    "trail_false_cls Γ {#K ∈# C. K ≠ L#}" and
    "¬ trail_defined_cls Γ C"
  shows "clause_could_propagate Γ C L"
  unfolding clause_could_propagate_iff
proof (intro conjI)
  show "linorder_lit.is_maximal_in_mset C L"
    using ‹linorder_lit.is_greatest_in_mset C L›
    by (metis linorder_lit.is_maximal_in_mset_if_is_greatest_in_mset)

  hence "L ∈# C"
    unfolding linorder_lit.is_maximal_in_mset_iff ..

  show "∀K ∈# C. K ≠ L ⟶ trail_false_lit Γ K"
    using ‹trail_false_cls Γ {#K ∈# C. K ≠ L#}›
    unfolding trail_false_cls_def
    by simp

  hence "∀K ∈# C. K ≠ L ⟶ trail_defined_lit Γ K"
    using trail_defined_lit_iff_true_or_false by metis

  thus "¬ trail_defined_lit Γ L"
    using ‹¬ trail_defined_cls Γ C› ‹L ∈# C›
    unfolding trail_defined_cls_def
    by metis
qed

lemma propagating_clause_in_clauses:
  assumes "trail_annotations_invars N (U⇩e⇩r, ℱ, Γ)" and "map_of Γ L = Some (Some C)"
  shows "C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)"
  using assms
proof (induction "(U⇩e⇩r, ℱ, Γ)" arbitrary: Γ rule: trail_annotations_invars.induct)
  case Nil
  hence False
    by simp
  thus ?case ..
next
  case (Cons_None Γ K)
  thus ?case
    by (metis map_of_Cons_code(2) option.discI option.inject)
next
  case (Cons_Some D K Γ)
  thus ?case
    by (metis map_of_Cons_code(2) option.inject)
qed

lemma trail_annotations_invars_mono_wrt_trail_suffix:
  assumes "suffix Γ' Γ" "trail_annotations_invars N (U⇩e⇩r, ℱ, Γ)"
  shows "trail_annotations_invars N (U⇩e⇩r, ℱ, Γ')"
  using assms(2,1)
proof (induction "(U⇩e⇩r, ℱ, Γ)" arbitrary: Γ Γ' rule: trail_annotations_invars.induct)
  case Nil
  thus ?case
    by (simp add: trail_annotations_invars.Nil)
next
  case (Cons_None Γ L)
  have "Γ' = (L, None) # Γ ∨ suffix Γ' Γ"
    using Cons_None.prems unfolding suffix_Cons .
  thus ?case
    using Cons_None.hyps
    by (metis trail_annotations_invars.Cons_None)
next
  case (Cons_Some C L Γ)
  have "Γ' = (L, Some C) # Γ ∨ suffix Γ' Γ"
    using Cons_Some.prems unfolding suffix_Cons .
  then show ?case
    using Cons_Some.hyps
    by (metis trail_annotations_invars.Cons_Some)
qed

lemma ord_res_8_preserves_trail_annotations_invars:
  assumes
    step: "ord_res_8 N s s'" and
    invars:
      "trail_annotations_invars N s"
      "trail_is_sorted N s"
  shows "trail_annotations_invars N s'"
  using step
proof (cases N s s' rule: ord_res_8.cases)
  case step_hyps: (decide_neg ℱ U⇩e⇩r Γ A Γ')
  show ?thesis
    unfolding ‹s' = (U⇩e⇩r, ℱ, Γ')› ‹Γ' = (Neg A, None) # Γ›
  proof (rule trail_annotations_invars.Cons_None)
    show "trail_annotations_invars N (U⇩e⇩r, ℱ, Γ)"
      using invars(1) by (simp add: ‹s = (U⇩e⇩r, ℱ, Γ)›)
  qed
next
  case step_hyps: (propagate ℱ U⇩e⇩r Γ A C Γ')
  show ?thesis
    unfolding ‹s' = (U⇩e⇩r, ℱ, Γ')› ‹Γ' = (Pos A, Some C) # Γ›
  proof (rule trail_annotations_invars.Cons_Some)
    show "ord_res.is_strictly_maximal_lit (Pos A) C"
      using step_hyps by argo
  next
    show "C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)"
      using step_hyps(5)
      by (simp add: linorder_cls.is_least_in_fset_iff)
  next
    show "trail_false_cls Γ {#K ∈# C. K ≠ Pos A#}"
      using step_hyps(5)
      by (simp add: linorder_cls.is_least_in_fset_iff clause_could_propagate_def)
  next
    show "linorder_cls.is_least_in_fset
      {|C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). clause_could_propagate Γ C (Pos A)|} C"
      using step_hyps by argo
  next
    show "trail_annotations_invars N (U⇩e⇩r, ℱ, Γ)"
      using invars(1) by (simp add: ‹s = (U⇩e⇩r, ℱ, Γ)›)
  qed
next
  case step_hyps: (factorize ℱ U⇩e⇩r Γ A E ℱ')

  hence "efac E ≠ E"
    by (metis (no_types, lifting) ex1_efac_eq_factoring_chain ex_ground_factoringI
        linorder_cls.is_least_in_ffilter_iff clause_could_propagate_iff)

  moreover have "clause_could_propagate Γ E (Pos A)"
    using step_hyps unfolding linorder_cls.is_least_in_ffilter_iff by metis

  ultimately have "ord_res.is_strictly_maximal_lit (Pos A) (efac E)"
    unfolding clause_could_propagate_def
    using ex1_efac_eq_factoring_chain ex_ground_factoringI
      ord_res.ground_factorings_preserves_maximal_literal by blast

  have "ℱ |⊆| ℱ'"
    unfolding ‹ℱ' = finsert E ℱ› by auto

  have "trail_annotations_invars N (U⇩e⇩r, ℱ, Γ)"
    using invars(1) by (simp add: ‹s = (U⇩e⇩r, ℱ, Γ)›)

  moreover have "∀A⇩1 |∈| trail_atms Γ. A⇩1 ≺⇩t A"
    using step_hyps unfolding linorder_trm.is_least_in_ffilter_iff by blast

  ultimately show ?thesis
    unfolding ‹s' = (U⇩e⇩r, ℱ', Γ)›
  proof (induction "(U⇩e⇩r, ℱ, Γ)" arbitrary: Γ rule: trail_annotations_invars.induct)
    case Nil
    show ?case
      by (simp add: trail_annotations_invars.Nil)
  next
    case (Cons_None Γ L)
    show ?case
    proof (rule trail_annotations_invars.Cons_None)
      have "∀A⇩1 |∈| trail_atms Γ. A⇩1 ≺⇩t A"
        using Cons_None.prems by (simp add: fset_trail_atms)

      thus "trail_annotations_invars N (U⇩e⇩r, ℱ', Γ)"
        using Cons_None.hyps by argo
    qed
  next
    case (Cons_Some C L Γ)

    have
      "clause_could_propagate Γ C L" and
      C_least: "∀y|∈|iefac ℱ |`| (N |∪| U⇩e⇩r). y ≠ C ⟶ clause_could_propagate Γ y L ⟶ C ≺⇩c y"
      using Cons_Some.hyps(4) unfolding linorder_cls.is_least_in_ffilter_iff by metis+

    hence "ord_res.is_maximal_lit L C"
      unfolding clause_could_propagate_def by argo

    show ?case
    proof (rule trail_annotations_invars.Cons_Some)
      show "ord_res.is_strictly_maximal_lit L C"
        using ‹ord_res.is_strictly_maximal_lit L C› .

      have "efac C = C"
        using Cons_Some
        by (metis (no_types, opaque_lifting) efac_spec is_pos_def linorder_lit.Uniq_is_maximal_in_mset
            linorder_lit.is_greatest_in_mset_iff_is_maximal_and_count_eq_one
            nex_strictly_maximal_pos_lit_if_neq_efac the1_equality')

      hence "C |∈| iefac ℱ' |`| (N |∪| U⇩e⇩r)"
        using ‹C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)› ‹ℱ |⊆| ℱ'›
        by (smt (verit, best) assms fimage_iff fsubsetD iefac_def)

      show "C |∈| iefac ℱ' |`| (N |∪| U⇩e⇩r)"
        using ‹C |∈| iefac ℱ' |`| (N |∪| U⇩e⇩r)› .

      show "trail_false_cls Γ {#x ∈# C. x ≠ L#}"
        using ‹trail_false_cls Γ {#x ∈# C. x ≠ L#}› .

      show "linorder_cls.is_least_in_fset
        {|C |∈| iefac ℱ' |`| (N |∪| U⇩e⇩r). clause_could_propagate Γ C L|} C"
        unfolding linorder_cls.is_least_in_ffilter_iff
      proof (intro conjI ballI impI)
        show "C |∈| iefac ℱ' |`| (N |∪| U⇩e⇩r)"
          using ‹C |∈| iefac ℱ' |`| (N |∪| U⇩e⇩r)› .
      next
        show "clause_could_propagate Γ C L"
          using ‹clause_could_propagate Γ C L› .
      next
        fix D :: "'f gterm literal multiset"
        assume "D |∈| iefac ℱ' |`| (N |∪| U⇩e⇩r)" and "D ≠ C" and "clause_could_propagate Γ D L"

        have "atm_of L ≺⇩t A"
          using Cons_Some.prems by (simp add: fset_trail_atms)

        hence "L ≺⇩l Pos A"
          by (cases L) simp_all

        moreover have "ord_res.is_maximal_lit L D"
          using ‹clause_could_propagate Γ D L› unfolding clause_could_propagate_iff by metis

        ultimately have "D ≺⇩c efac E"
          using ‹ord_res.is_strictly_maximal_lit (Pos A) (efac E)›
          by (metis linorder_lit.is_maximal_in_mset_if_is_greatest_in_mset
              linorder_lit.multp_if_maximal_less_that_maximal)

        hence "D |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)"
          using ‹D |∈| iefac ℱ' |`| (N |∪| U⇩e⇩r)›
          unfolding ‹ℱ' = finsert E ℱ›
          using iefac_def by force
          
        thus "C ≺⇩c D"
          using C_least ‹D ≠ C› ‹clause_could_propagate Γ D L› by metis
      qed

      have "∀A⇩1 |∈| trail_atms Γ. A⇩1 ≺⇩t A"
        using Cons_Some.prems by (simp add: fset_trail_atms)

      thus "trail_annotations_invars N (U⇩e⇩r, ℱ', Γ)"
        using Cons_Some.hyps by argo
    qed
  qed
next
  case step_hyps: (resolution Γ ℱ U⇩e⇩r E A D U⇩e⇩r' Γ')

  show ?thesis
  proof (cases "eres D E = {#}")
    case True
    hence "∄K. ord_res.is_maximal_lit K (eres D E)"
      by (simp add: linorder_lit.is_maximal_in_mset_iff)
    hence "Γ' = []"
      unfolding step_hyps by simp
    thus ?thesis
      unfolding ‹s' = (U⇩e⇩r', ℱ, Γ')›
      using trail_annotations_invars.Nil by metis
  next
    case False

    then obtain K where eres_max_lit: "linorder_lit.is_maximal_in_mset (eres D E) K"
      using linorder_lit.ex_maximal_in_mset by metis

    have Γ'_eq: "Γ' = dropWhile (λLn. atm_of K ≼⇩t atm_of (fst Ln)) Γ"
      unfolding step_hyps(7)
    proof (rule dropWhile_cong)
      show "Γ = Γ" ..
    next
      fix x :: "'f gterm literal × 'f gterm literal multiset option"
      assume "x ∈ set Γ"
      show "(∀K. ord_res.is_maximal_lit K (eres D E) ⟶ atm_of K ≼⇩t atm_of (fst x)) =
        (atm_of K ≼⇩t atm_of (fst x))"
        unfolding case_prod_beta
        using eres_max_lit
        by (metis Uniq_D linorder_lit.Uniq_is_maximal_in_mset)
    qed

    have "trail_annotations_invars N (U⇩e⇩r, ℱ, Γ)"
      using invars(1) by (simp add: ‹s = (U⇩e⇩r, ℱ, Γ)›)

    moreover have "suffix Γ' Γ"
      unfolding step_hyps
      using suffix_dropWhile by metis

    moreover have "∀Ln ∈ set Γ'. ¬ (atm_of K ≼⇩t atm_of (fst Ln))"
      unfolding Γ'_eq
    proof (rule ball_set_dropWhile_if_sorted_wrt_and_monotone_on)
      have "sorted_wrt (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) Γ"
        using invars(2)
        by (simp add: ‹s = (U⇩e⇩r, ℱ, Γ)› trail_is_sorted_def sorted_wrt_map)

      thus "sorted_wrt (λx y. fst y ≺⇩l fst x) Γ"
      proof (rule sorted_wrt_mono_rel[rotated])
        show "⋀x y. atm_of (fst y) ≺⇩t atm_of (fst x) ⟹ fst y ≺⇩l fst x"
          by (metis (no_types, lifting) linorder_lit.antisym_conv3 linorder_trm.dual_order.asym
              literal.exhaust_sel ord_res.less_lit_simps(1) ord_res.less_lit_simps(3)
              ord_res.less_lit_simps(4))
      qed
    next
      show "monotone_on (set Γ) (λx y. fst y ≺⇩l fst x) (λLn y. y ≤ Ln)
     (λLn. atm_of K ≼⇩t atm_of (fst Ln))"
        apply (simp add: monotone_on_def)
        by (smt (verit, best) Neg_atm_of_iff Pos_atm_of_iff linorder_lit.order.asym
            linorder_trm.less_linear linorder_trm.order.strict_trans ord_res.less_lit_simps(1)
            ord_res.less_lit_simps(3) ord_res.less_lit_simps(4))
    qed

    ultimately show ?thesis
      unfolding ‹s' = (U⇩e⇩r', ℱ, Γ')›
    proof (induction "(U⇩e⇩r, ℱ, Γ)" arbitrary: Γ Γ' rule: trail_annotations_invars.induct)
      case Nil
      thus ?case
        by (simp add: trail_annotations_invars.Nil)
    next
      case (Cons_None Γ L)
      thus ?case
        by (metis insert_iff list.simps(15) suffix_Cons suffix_order.dual_order.refl
            trail_annotations_invars.Cons_None)
    next
      case (Cons_Some C L Γ)

      have
        "clause_could_propagate Γ C L" and
        C_least: "∀y|∈|iefac ℱ |`| (N |∪| U⇩e⇩r). y ≠ C ⟶ clause_could_propagate Γ y L ⟶ C ≺⇩c y"
        using Cons_Some.hyps(4) unfolding linorder_cls.is_least_in_ffilter_iff by metis+

      hence C_max_lit: "ord_res.is_maximal_lit L C"
        unfolding clause_could_propagate_def by argo

      obtain Γ'' where "(L, Some C) # Γ = Γ'' @ Γ'"
        using Cons_Some.prems by (auto elim: suffixE)

      show ?case
      proof (cases Γ'')
        case Nil
        hence "Γ' = (L, Some C) # Γ"
          using ‹(L, Some C) # Γ = Γ'' @ Γ'› by simp

        show ?thesis
          unfolding ‹Γ' = (L, Some C) # Γ›
        proof (rule trail_annotations_invars.Cons_Some)
          show "ord_res.is_strictly_maximal_lit L C"
            using ‹ord_res.is_strictly_maximal_lit L C› .

          show "C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r')"
            using ‹C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)› ‹U⇩e⇩r' = finsert (eres D E) U⇩e⇩r› by simp

          show "trail_false_cls Γ {#K ∈# C. K ≠ L#}"
            using ‹trail_false_cls Γ {#K ∈# C. K ≠ L#}› .

          show "linorder_cls.is_least_in_fset {|C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r'). clause_could_propagate Γ C L|} C"
            unfolding linorder_cls.is_least_in_ffilter_iff
          proof (intro conjI ballI impI)
            show "C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r')"
              using ‹C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r')› .
          next
            show "clause_could_propagate Γ C L"
              using Cons_Some.hyps(4) unfolding linorder_cls.is_least_in_ffilter_iff by metis
          next
            fix x :: "'f gterm literal multiset"
            assume "x |∈| iefac ℱ |`| (N |∪| U⇩e⇩r')"
              and "x ≠ C"
              and "clause_could_propagate Γ x L"

            have "linorder_lit.is_maximal_in_mset x L"
              using ‹clause_could_propagate Γ x L› unfolding clause_could_propagate_def by argo

            moreover have "L ≺⇩l K"
              using ‹∀Ln ∈ set Γ'. ¬ (atm_of K ≼⇩t atm_of (fst Ln))›
              unfolding ‹Γ' = (L, Some C) # Γ›
              apply simp
              by (metis Neg_atm_of_iff linorder_lit.antisym_conv3 linorder_trm.less_linear
                  literal.collapse(1) ord_res.less_lit_simps(1) ord_res.less_lit_simps(3)
                  ord_res.less_lit_simps(4))

            ultimately have "set_mset x ≠ set_mset (eres D E)"
              using eres_max_lit
              by (metis linorder_lit.is_maximal_in_mset_iff linorder_lit.neq_iff)

            hence "x ≠ iefac ℱ (eres D E)"
              using iefac_def by auto

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

            then show "C ≺⇩c x"
              using C_least ‹x ≠ C› ‹clause_could_propagate Γ x L› by metis
          qed

          show "trail_annotations_invars N (U⇩e⇩r', ℱ, Γ)"
            using Cons_Some
            by (simp add: ‹Γ' = (L, Some C) # Γ›)
        qed
      next
        case (Cons a list)
        then show ?thesis
          by (metis Cons_Some.hyps(6) Cons_Some.prems ‹(L, Some C) # Γ = Γ'' @ Γ'› empty_iff
              list.set(1) list.set_intros(1) self_append_conv2 suffix_Cons)
      qed
    qed
  qed
qed

definition trail_is_lower_set where
  "trail_is_lower_set N s ⟷
    (∀U⇩e⇩r ℱ Γ. s = (U⇩e⇩r, ℱ, Γ) ⟶
      linorder_trm.is_lower_fset (trail_atms Γ) (atms_of_clss (N |∪| U⇩e⇩r)))"

lemma atoms_not_in_clause_set_undefined_if_trail_is_sorted_lower_set:
  assumes invar: "trail_is_lower_set N (U⇩e⇩r, ℱ, Γ)"
  shows "∀A. A |∉| atms_of_clss (N |∪| U⇩e⇩r) ⟶ A |∉| trail_atms Γ"
  using invar[unfolded trail_is_lower_set_def, simplified]
  by (metis Un_iff linorder_trm.is_lower_set_iff sup.absorb2)

lemma ord_res_8_preserves_atoms_in_trail_lower_set:
  assumes
    step: "ord_res_8 N s s'" and
    invars:
      "trail_is_lower_set N s"
      "trail_annotations_invars N s"
      "trail_is_sorted N s"
  shows "trail_is_lower_set N s'"
  using step
proof (cases N s s' rule: ord_res_8.cases)
  case step_hyps: (decide_neg ℱ U⇩e⇩r Γ A Γ')

  have
    A_in: "A |∈| atms_of_clss (N |∪| U⇩e⇩r)" and
    A_gt: "∀x |∈| trail_atms Γ. x ≺⇩t A" and
    A_least: "∀x |∈| atms_of_clss (N |∪| U⇩e⇩r). (∀w |∈| trail_atms Γ. w ≺⇩t x) ⟶ x ≠ A ⟶ A ≺⇩t x"
    using step_hyps unfolding linorder_trm.is_least_in_ffilter_iff by simp_all

  have "trail_atms Γ' = finsert A (trail_atms Γ)"
    using step_hyps by simp

  have
    inv1: "sorted_wrt (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) Γ" and
    inv2: "linorder_trm.is_lower_fset (trail_atms Γ) (atms_of_clss (N |∪| U⇩e⇩r))"
    using invars(1,3)
    by (simp_all only: ‹s = (U⇩e⇩r, ℱ, Γ)› trail_is_lower_set_def trail_is_sorted_def)

  have "sorted_wrt (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) Γ'"
    unfolding ‹Γ' = (Neg A, None) # Γ› list.map sorted_wrt.simps
  proof (intro conjI ballI)
    fix x
    assume "x ∈ set Γ"
    hence "atm_of (fst x) |∈| trail_atms Γ"
      by (auto simp: fset_trail_atms)
    hence "atm_of (fst x) ≺⇩t atm_of (Neg A)"
      using A_gt by simp
    thus "atm_of (fst x) ≺⇩t atm_of (fst (Neg A, None))"
      unfolding comp_def prod.sel .
  next
    show "sorted_wrt (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) Γ"
      using inv1 .
  qed

  moreover have "linorder_trm.is_lower_fset (trail_atms Γ') (atms_of_clss (N |∪| U⇩e⇩r))"
    unfolding ‹trail_atms Γ' = finsert A (trail_atms Γ)› finsert.rep_eq
  proof (rule linorder_trm.is_lower_set_insertI)
    show "A |∈| atms_of_clss (N |∪| U⇩e⇩r)"
      using A_in .
  next
    show "∀w |∈| atms_of_clss (N |∪| U⇩e⇩r). w ≺⇩t A ⟶ w |∈| trail_atms Γ"
      using A_least inv2
      by (metis linorder_trm.is_lower_set_iff linorder_trm.not_less_iff_gr_or_eq)
  next
    show "linorder_trm.is_lower_fset (trail_atms Γ)
     (atms_of_clss (N |∪| U⇩e⇩r))"
      using inv2 .
  qed

  ultimately show ?thesis
    by (simp add: ‹s' = (U⇩e⇩r, ℱ, Γ')› trail_is_lower_set_def)
next
  case step_hyps: (propagate ℱ U⇩e⇩r Γ A C Γ')

  have
    A_in: "A |∈| atms_of_clss (N |∪| U⇩e⇩r)" and
    A_gt: "∀x |∈| trail_atms Γ. x ≺⇩t A" and
    A_least: "∀x |∈| atms_of_clss (N |∪| U⇩e⇩r). (∀w |∈| trail_atms Γ. w ≺⇩t x) ⟶ x ≠ A ⟶ A ≺⇩t x"
    using step_hyps unfolding linorder_trm.is_least_in_ffilter_iff by simp_all

  have "trail_atms Γ' = finsert A (trail_atms Γ)"
    using step_hyps by simp

  have
    inv1: "sorted_wrt (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) Γ" and
    inv2: "linorder_trm.is_lower_fset (trail_atms Γ) (atms_of_clss (N |∪| U⇩e⇩r))"
    using invars(1,3)
    by (simp_all only: ‹s = (U⇩e⇩r, ℱ, Γ)› trail_is_lower_set_def trail_is_sorted_def)

  have "sorted_wrt (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) Γ'"
    unfolding ‹Γ' = (Pos A, Some C) # Γ› list.map sorted_wrt.simps
  proof (intro conjI ballI)
    fix x
    assume "x ∈ set Γ"
    hence "atm_of (fst x) |∈| trail_atms Γ"
      by (auto simp: fset_trail_atms)
    hence "atm_of (fst x) ≺⇩t atm_of (Pos A)"
      using A_gt by simp
    thus "atm_of (fst x) ≺⇩t atm_of (fst (Pos A, Some C))"
      unfolding comp_def prod.sel .
  next
    show "sorted_wrt (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) Γ"
      using inv1 .
  qed

  moreover have "linorder_trm.is_lower_fset (trail_atms Γ') (atms_of_clss (N |∪| U⇩e⇩r))"
    unfolding ‹trail_atms Γ' = finsert A (trail_atms Γ)› finsert.rep_eq
  proof (rule linorder_trm.is_lower_set_insertI)
    show "A |∈| atms_of_clss (N |∪| U⇩e⇩r)"
      using A_in .
  next
    show "∀w|∈|atms_of_clss (N |∪| U⇩e⇩r). w ≺⇩t A ⟶ w |∈| trail_atms Γ"
      using A_least inv2
      by (metis linorder_trm.is_lower_set_iff linorder_trm.not_less_iff_gr_or_eq)
  next
    show "linorder_trm.is_lower_fset (trail_atms Γ) (atms_of_clss (N |∪| U⇩e⇩r))"
      using inv2 .
  qed

  ultimately show ?thesis
    by (simp add: ‹s' = (U⇩e⇩r, ℱ, Γ')› trail_is_lower_set_def)
next
  case (factorize ℱ U⇩e⇩r Γ A C ℱ')
  thus ?thesis
    using invars(1) by (simp add: trail_is_lower_set_def fset_trail_atms)
next
  case step_hyps: (resolution Γ ℱ U⇩e⇩r D A C U⇩e⇩r' Γ')

  have "suffix Γ' Γ"
    using step_hyps suffix_dropWhile by blast

  then obtain Γ'' where "Γ = Γ'' @ Γ'"
    unfolding suffix_def by metis

  have "atms_of_clss (N |∪| U⇩e⇩r') = atms_of_clss (finsert (eres C D) (N |∪| U⇩e⇩r))"
    unfolding ‹U⇩e⇩r' = finsert (eres C D) U⇩e⇩r› by simp
  also have "… = atms_of_cls (eres C D) |∪| atms_of_clss (N |∪| U⇩e⇩r)"
    unfolding atms_of_clss_finsert ..
  also have "… = atms_of_clss (N |∪| U⇩e⇩r)"
  proof -
    have "∀A |∈| atms_of_cls (eres C D). A |∈| atms_of_cls C ∨ A |∈| atms_of_cls D"
      using lit_in_one_of_resolvents_if_in_eres
      by (smt (verit, best) atms_of_cls_def fimage_iff fset_fset_mset)

    moreover have "C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)"
      using invars(2)[unfolded ‹s = (U⇩e⇩r, ℱ, Γ)›] step_hyps(5)
      by (metis propagating_clause_in_clauses)

    moreover have "D |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)"
      using linorder_cls.is_least_in_ffilter_iff step_hyps(3) by blast

    ultimately have "∀A |∈| atms_of_cls (eres C D). A |∈| atms_of_clss (iefac ℱ |`| (N |∪| U⇩e⇩r))"
      by (metis atms_of_clss_finsert funion_iff mk_disjoint_finsert)

    hence "∀A |∈| atms_of_cls (eres C D). A |∈| atms_of_clss (N |∪| U⇩e⇩r)"
      unfolding atms_of_clss_fimage_iefac .

    thus ?thesis
      by blast
  qed
  finally have "atms_of_clss (N |∪| U⇩e⇩r') = atms_of_clss (N |∪| U⇩e⇩r)" .

  have
    inv1: "sorted_wrt (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) Γ" and
    inv2: "linorder_trm.is_lower_fset (trail_atms Γ) (atms_of_clss (N |∪| U⇩e⇩r))"
    using invars(1,3)
    by (simp_all only: ‹s = (U⇩e⇩r, ℱ, Γ)› trail_is_lower_set_def trail_is_sorted_def)

  have "sorted_wrt (λx y. y ≺⇩t x) (map (atm_of ∘ fst) Γ)"
    using inv1 by (simp add: sorted_wrt_map)

  hence "sorted_wrt (λx y. y ≺⇩t x) (map (atm_of ∘ fst) Γ'' @ map (atm_of ∘ fst) Γ')"
    by (simp add: ‹Γ = Γ'' @ Γ'›)

  moreover have "linorder_trm.is_lower_set (set (map (atm_of ∘ fst) Γ'' @ map (atm_of ∘ fst) Γ'))
    (fset (atms_of_clss (N |∪| U⇩e⇩r)))"
    using inv2 ‹Γ = Γ'' @ Γ'›
    by (metis image_comp list.set_map map_append fset_trail_atms)

  ultimately have "linorder_trm.is_lower_fset (trail_atms Γ') (atms_of_clss (N |∪| U⇩e⇩r'))"
    using linorder_trm.sorted_and_lower_set_appendD_right
    using ‹atms_of_clss (N |∪| U⇩e⇩r') = atms_of_clss (N |∪| U⇩e⇩r)›
    by (metis (no_types, lifting) image_comp list.set_map fset_trail_atms)

  thus ?thesis
    by (simp add: ‹s' = (U⇩e⇩r', ℱ, Γ')› trail_is_lower_set_def)
qed

definition false_cls_is_mempty_or_has_neg_max_lit where
  "false_cls_is_mempty_or_has_neg_max_lit N s ⟷
    (∀U⇩e⇩r ℱ Γ. s = (U⇩e⇩r, ℱ, Γ) ⟶ (∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r).
      trail_false_cls Γ C ⟶ C = {#} ∨ (∃A. linorder_lit.is_maximal_in_mset C (Neg A))))"

lemma ord_res_8_preserves_false_cls_is_mempty_or_has_neg_max_lit:
  assumes
    step: "ord_res_8 N s s'" and
    invars:
      "false_cls_is_mempty_or_has_neg_max_lit N s"
      "trail_is_lower_set N s"
      "trail_is_sorted N s"
  shows "false_cls_is_mempty_or_has_neg_max_lit N s'"
  using step
proof (cases N s s' rule: ord_res_8.cases)
  case step_hyps: (decide_neg ℱ U⇩e⇩r Γ A Γ')

  have Γ_lower: "linorder_trm.is_lower_fset (trail_atms Γ) (atms_of_clss (N |∪| U⇩e⇩r))"
    using ‹trail_is_lower_set N s›[unfolded trail_is_lower_set_def,
        rule_format, OF ‹s = (U⇩e⇩r, ℱ, Γ)›] .

  have Γ_sorted: "sorted_wrt (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) Γ"
    using ‹trail_is_sorted N s›[unfolded trail_is_sorted_def,
        rule_format, OF ‹s = (U⇩e⇩r, ℱ, Γ)›] .

  have "trail_consistent Γ"
    using trail_consistent_if_sorted_wrt_atoms[OF Γ_sorted] .

  hence "trail_consistent Γ'"
    unfolding ‹Γ' = (Neg A, None) # Γ›
  proof (rule trail_consistent.Cons [rotated])
    show "¬ trail_defined_lit Γ (Neg A)"
      unfolding trail_defined_lit_iff_trail_defined_atm
      using linorder_trm.is_least_in_fset_ffilterD(2) linorder_trm.less_irrefl step_hyps(4)
        trail_defined_lit_iff_trail_defined_atm by force
  qed

  have atm_defined_iff_lt_A: "x |∈| trail_atms Γ ⟷ x ≺⇩t A"
    if x_in: "x |∈| atms_of_clss (N |∪| U⇩e⇩r)" for x
  proof (rule iffI)
    assume "x |∈| trail_atms Γ"
    thus "x ≺⇩t A"
      using step_hyps(4)
      unfolding linorder_trm.is_least_in_ffilter_iff
      by blast
  next
    assume "x ≺⇩t A"
    thus "x |∈| trail_atms Γ"
      using step_hyps(4)[unfolded linorder_trm.is_least_in_ffilter_iff]
      using Γ_lower[unfolded linorder_trm.is_lower_set_iff]
      by (metis linorder_trm.dual_order.asym linorder_trm.neq_iff x_in)
  qed

  have "¬ trail_false_cls Γ' C" if C_in: "C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" for C
  proof -
    have "¬ trail_false_cls Γ C"
      using C_in step_hyps(3) by metis
    hence "trail_true_cls Γ C ∨ ¬ trail_defined_cls Γ C"
      using trail_true_or_false_cls_if_defined by metis
    thus "¬ trail_false_cls Γ' C"
    proof (elim disjE)
      assume "trail_true_cls Γ C"
      hence "trail_true_cls Γ' C"
        unfolding ‹Γ' = (Neg A, None) # Γ› trail_true_cls_def
        by (metis image_insert insert_iff list.set(2) trail_true_lit_def)
      thus "¬ trail_false_cls Γ' C"
        using ‹trail_consistent Γ'›
        by (metis not_trail_true_cls_and_trail_false_cls)
    next
      assume "¬ trail_defined_cls Γ C"
      then obtain L where L_max: "ord_res.is_maximal_lit L C"
        by (metis ‹¬ trail_false_cls Γ C› linorder_lit.ex_maximal_in_mset trail_false_cls_mempty)

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

      have "atm_of L |∈| atms_of_clss (N |∪| U⇩e⇩r)"
        using C_in ‹L ∈# C› by (metis atm_of_in_atms_of_clssI)

      show "¬ trail_false_cls Γ' C"
      proof (cases "atm_of L = A")
        case True

        have "¬ trail_defined_lit Γ (Pos A)"
          using step_hyps(4)
          unfolding trail_defined_lit_iff_trail_defined_atm linorder_trm.is_least_in_ffilter_iff
          by auto

        hence "(∃K ∈# C. K ≠ Pos A ∧ ¬ trail_false_lit Γ K) ∨
          ¬ ord_res.is_maximal_lit (Pos A) C"
          using step_hyps(5) C_in
          unfolding clause_could_propagate_iff
          unfolding bex_simps de_Morgan_conj not_not by blast

        thus ?thesis
        proof (elim disjE bexE conjE)
          fix K :: "'f gterm literal"
          assume "K ∈# C" and "K ≠ Pos A" and "¬ trail_false_lit Γ K"
          thus "¬ trail_false_cls Γ' C"
            by (smt (verit) fst_conv image_iff insertE list.simps(15) step_hyps(6)
                trail_false_cls_def trail_false_lit_def uminus_Pos uminus_lit_swap)
        next
          assume "¬ ord_res.is_maximal_lit (Pos A) C"

          hence "L = Neg A"
            using ‹atm_of L = A› L_max by (metis literal.exhaust_sel)

          thus "¬ trail_false_cls Γ' C"
            unfolding ‹Γ' = (Neg A, None) # Γ›
            unfolding trail_false_cls_def trail_false_lit_def
            using ‹L ∈# C›[unfolded ‹L = Neg A›]
            by (metis ‹¬ trail_defined_cls Γ C› fst_conv image_insert insertE list.simps(15)
                trail_defined_cls_def trail_defined_lit_def uminus_lit_swap uminus_not_id')
        qed
      next
        case False

        moreover have "¬ atm_of L ≺⇩t A"
        proof (rule notI)
          assume "atm_of L ≺⇩t A"
          moreover have "∀K ∈# C. atm_of K ≼⇩t atm_of L"
            using L_max linorder_lit.is_maximal_in_mset_iff
            by (metis Neg_atm_of_iff linorder_trm.le_less_linear linorder_trm.linear
                literal.collapse(1) ord_res.less_lit_simps(1) ord_res.less_lit_simps(2)
                ord_res.less_lit_simps(3) ord_res.less_lit_simps(4))
          ultimately have "∀K ∈# C. atm_of K ≺⇩t A"
            by (metis linorder_trm.antisym_conv1 linorder_trm.dual_order.strict_trans)
          moreover have "∀K ∈# C. atm_of K |∈| atms_of_clss (N |∪| U⇩e⇩r)"
            using C_in by (metis atm_of_in_atms_of_clssI)
          ultimately have "∀K ∈# C. atm_of K |∈| trail_atms Γ"
            using atm_defined_iff_lt_A by metis
          hence "∀K ∈# C. trail_defined_lit Γ K"
            using trail_defined_lit_iff_trail_defined_atm by metis
          hence "trail_defined_cls Γ C"
            unfolding trail_defined_cls_def by argo
          thus False
            using ‹¬ trail_defined_cls Γ C› by contradiction
        qed

        ultimately have "A ≺⇩t atm_of L"
          by order

        hence "atm_of L |∉| trail_atms Γ'"
          unfolding ‹Γ' = (Neg A, None) # Γ›
          unfolding trail_atms.simps prod.sel literal.sel
          using atm_defined_iff_lt_A[OF ‹atm_of L |∈| atms_of_clss (N |∪| U⇩e⇩r)›]
          using ‹¬ atm_of L ≺⇩t A› by simp

        hence "¬ trail_defined_lit Γ' L"
          using trail_defined_lit_iff_trail_defined_atm by blast

        hence "¬ trail_false_lit Γ' L"
          using trail_defined_lit_iff_true_or_false by blast

        thus "¬ trail_false_cls Γ' C"
          unfolding trail_false_cls_def
          using ‹L ∈# C› by metis
      qed
    qed
  qed

  hence "∀C|∈|iefac ℱ |`| (N |∪| U⇩e⇩r). trail_false_cls Γ' C ⟶
    C = {#} ∨ (∃A. ord_res.is_maximal_lit (Neg A) C)"
    by metis

  thus ?thesis
    unfolding false_cls_is_mempty_or_has_neg_max_lit_def ‹s' = (U⇩e⇩r, ℱ, Γ')› by simp
next
  case step_hyps: (propagate ℱ U⇩e⇩r Γ A C Γ')

  have "E = {#} ∨ (∃A. ord_res.is_maximal_lit (Neg A) E)"
    if E_in: "E |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" and E_false: "trail_false_cls Γ' E" for E
  proof (cases "A ∈ atm_of ` set_mset E")
    case True
    have "¬ trail_false_cls Γ E"
      using ‹¬ fBex (iefac ℱ |`| (N |∪| U⇩e⇩r)) (trail_false_cls Γ)› E_in by metis

    hence "Neg A ∈# E"
      using E_false[unfolded ‹Γ' = (Pos A, Some C) # Γ›]
      by (metis subtrail_falseI uminus_Pos)

    have "atm_of L |∈| trail_atms Γ'" if "L ∈# E" for L
      using E_false ‹L ∈# E›
      by (simp add: atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set fset_trail_atms
          trail_false_cls_def trail_false_lit_def)

    moreover have "x ≺⇩t A" if "x |∈| trail_atms Γ" for x
      using step_hyps(4) that
      by (simp add: linorder_trm.is_least_in_ffilter_iff)

    ultimately have "atm_of L ≼⇩t A" if "L ∈# E" for L
      unfolding ‹Γ' = (Pos A, Some C) # Γ› trail_atms.simps prod.sel literal.sel
      using ‹L ∈# E› by blast

    hence "L ≼⇩l Neg A" if "L ∈# E" for L
      using ‹L ∈# E›
      by (metis linorder_lit.leI linorder_trm.leD literal.collapse(1) literal.collapse(2)
          ord_res.less_lit_simps(3) ord_res.less_lit_simps(4))

    hence "∃A. ord_res.is_maximal_lit (Neg A) E"
      using ‹Neg A ∈# E›
      by (metis ‹¬ trail_false_cls Γ E› linorder_lit.ex_maximal_in_mset
          linorder_lit.is_maximal_in_mset_iff reflclp_iff trail_false_cls_mempty)

    thus ?thesis ..
  next
    case False
    hence "trail_false_cls Γ E"
      using E_false[unfolded ‹Γ' = (Pos A, Some C) # Γ›]
      by (metis atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set literal.sel(1) subtrail_falseI)

    moreover have "¬ trail_false_cls Γ E"
      using ‹¬ fBex (iefac ℱ |`| (N |∪| U⇩e⇩r)) (trail_false_cls Γ)› E_in by metis

    ultimately have False
      by contradiction

    thus ?thesis ..
  qed

  thus ?thesis
    unfolding false_cls_is_mempty_or_has_neg_max_lit_def ‹s' = (U⇩e⇩r, ℱ, Γ')› by simp
next
  case step_hyps: (factorize ℱ U⇩e⇩r Γ A C ℱ')

  have "trail_false_cls Γ (iefac ℱ C) ⟷ trail_false_cls Γ C" if "C |∈| N |∪| U⇩e⇩r" for ℱ C
    using that by (simp add: iefac_def trail_false_cls_def)

  hence "∀C|∈|iefac ℱ' |`| (N |∪| U⇩e⇩r).
    trail_false_cls Γ C ⟶ C = {#} ∨ (∃A. ord_res.is_maximal_lit (Neg A) C)"
    using step_hyps(3) by force

  thus ?thesis
    by (simp add: ‹s' = (U⇩e⇩r, ℱ', Γ)› false_cls_is_mempty_or_has_neg_max_lit_def)
next
  case step_hyps: (resolution Γ ℱ U⇩e⇩r D A C U⇩e⇩r' Γ')

  have false_wrt_Γ_if_false_wrt_Γ': "trail_false_cls Γ E" if "trail_false_cls Γ' E" for E
    using that
    unfolding step_hyps(7) trail_false_cls_def trail_false_lit_def
    using image_iff set_dropWhileD by fastforce

  have "iefac ℱ E = {#} ∨ (∃A. ord_res.is_maximal_lit (Neg A) (iefac ℱ E))"
    if "E |∈| N |∪| U⇩e⇩r'" "trail_false_cls Γ' (iefac ℱ E)" for E
  proof (cases "E = eres C D")
    case True

    show ?thesis
    proof (cases "eres C D = {#}")
      case True
      thus ?thesis
        by (simp add: ‹E = eres C D›)
    next
      case False
      then obtain K where K_max: "ord_res.is_maximal_lit K (eres C D)"
        using linorder_lit.ex_maximal_in_mset by metis

      have "Γ' = dropWhile (λx. atm_of K ≼⇩t atm_of (fst x)) Γ"
        unfolding step_hyps(7)
      proof (rule dropWhile_cong)
        show "Γ = Γ" ..
      next
        fix Ln :: "'f gterm literal × 'f gterm literal multiset option"
        obtain L annot where "Ln = (L, annot)"
          by force
        have "(∀K. ord_res.is_maximal_lit K (eres C D) ⟶ atm_of K ≼⇩t atm_of L) ⟷
          (atm_of K ≼⇩t atm_of L)"
          using K_max by (metis linorder_lit.Uniq_is_maximal_in_mset the1_equality')
        thus "(∀K. ord_res.is_maximal_lit K (eres C D) ⟶ atm_of K ≼⇩t atm_of (fst Ln)) ⟷
          (atm_of K ≼⇩t atm_of (fst Ln))"
          unfolding ‹Ln = (L, annot)› prod.case prod.sel .
      qed

      have "K ∈# eres C D"
        using K_max linorder_lit.is_maximal_in_mset_iff by metis

      moreover have "¬ trail_defined_lit Γ' K"
      proof -
        have "sorted_wrt (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) Γ"
          using invars[unfolded ‹s = (U⇩e⇩r, ℱ, Γ)› trail_is_sorted_def]
          by (simp add: sorted_wrt_map)

        have "∀Ln ∈ set Γ'. ¬ (atm_of K ≼⇩t atm_of (fst Ln))"
          unfolding ‹Γ' = dropWhile (λx. atm_of K ≼⇩t atm_of (fst x)) Γ›
        proof (rule ball_set_dropWhile_if_sorted_wrt_and_monotone_on)
          show "sorted_wrt (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) Γ"
            using invars[unfolded ‹s = (U⇩e⇩r, ℱ, Γ)› trail_is_sorted_def]
            by (simp add: sorted_wrt_map)
        next
          show "monotone_on (set Γ) (λx y. atm_of (fst y) ≺⇩t atm_of (fst x)) (≥)
            (λx. atm_of K ≼⇩t atm_of (fst x))"
            by (rule monotone_onI) auto
        qed

        hence "∀Ln ∈ set Γ'. atm_of (fst Ln) ≺⇩t atm_of K"
          by auto

        hence "atm_of K |∉| trail_atms Γ'"
          by (smt (verit, best) fset_trail_atms image_iff linorder_trm.dual_order.asym)

        thus ?thesis
          using trail_defined_lit_iff_trail_defined_atm by metis
      qed

      ultimately have "¬ trail_false_cls Γ' (eres C D)"
        using trail_defined_lit_iff_true_or_false trail_false_cls_def by metis

      hence "¬ trail_false_cls Γ' E"
        unfolding ‹E = eres C D› .

      hence "¬ trail_false_cls Γ' (iefac ℱ E)"
        unfolding trail_false_cls_def by (metis iefac_def set_mset_efac)

      thus ?thesis
        using ‹trail_false_cls Γ' (iefac ℱ E)›
        by contradiction
    qed
  next
    case False
    hence "E |∈| N |∪| U⇩e⇩r"
      using step_hyps(6) that(1) by force

    moreover hence "iefac ℱ E ≠ {#}"
      using step_hyps(3-)
      by (metis (no_types, opaque_lifting) empty_iff linorder_cls.is_least_in_ffilter_iff
          linorder_cls.not_less linorder_lit.is_maximal_in_mset_iff mempty_lesseq_cls rev_fimage_eqI
          set_mset_empty trail_false_cls_mempty)

    moreover have "trail_false_cls Γ (iefac ℱ E)"
      using ‹trail_false_cls Γ' (iefac ℱ E)› false_wrt_Γ_if_false_wrt_Γ' by metis

    ultimately have "∃A. ord_res.is_maximal_lit (Neg A) (iefac ℱ E)"
      using invars(1)[unfolded ‹s = (U⇩e⇩r, ℱ, Γ)› false_cls_is_mempty_or_has_neg_max_lit_def]
      by auto

    thus ?thesis ..
  qed

  thus ?thesis
    by (simp add: ‹s' = (U⇩e⇩r', ℱ, Γ')› false_cls_is_mempty_or_has_neg_max_lit_def)
qed


definition decided_literals_all_neg where
  "decided_literals_all_neg N s ⟷
    (∀U⇩e⇩r ℱ Γ. s = (U⇩e⇩r, ℱ, Γ) ⟶
      (∀Ln ∈ set Γ. ∀L. Ln = (L, None) ⟶ is_neg L))"

lemma ord_res_8_preserves_decided_literals_all_neg:
  assumes
    step: "ord_res_8 N s s'" and
    invar: "decided_literals_all_neg N s"
  shows "decided_literals_all_neg N s'"
  using step
proof (cases N s s' rule: ord_res_8.cases)
  case (decide_neg ℱ U⇩e⇩r Γ A Γ')

  have "∀Ln∈set Γ. ∀L. Ln = (L, None) ⟶ is_neg L"
    using invar by (simp add: ‹s = (U⇩e⇩r, ℱ, Γ)› decided_literals_all_neg_def)

  hence "∀Ln∈set Γ'. ∀L. Ln = (L, None) ⟶ is_neg L"
    unfolding ‹Γ' = (Neg A, None) # Γ› by simp

  thus ?thesis
    by (simp add: ‹s' = (U⇩e⇩r, ℱ, Γ')› decided_literals_all_neg_def)
next
  case (propagate ℱ U⇩e⇩r Γ A C Γ')

  have "∀Ln∈set Γ. ∀L. Ln = (L, None) ⟶ is_neg L"
    using invar by (simp add: ‹s = (U⇩e⇩r, ℱ, Γ)› decided_literals_all_neg_def)

  hence "∀Ln∈set Γ'. ∀L. Ln = (L, None) ⟶ is_neg L"
    unfolding ‹Γ' = (Pos A, Some C) # Γ› by simp

  thus ?thesis
    by (simp add: ‹s' = (U⇩e⇩r, ℱ, Γ')› decided_literals_all_neg_def)
next
  case (factorize ℱ U⇩e⇩r Γ A C ℱ')

  have "∀Ln∈set Γ. ∀L. Ln = (L, None) ⟶ is_neg L"
    using invar by (simp add: ‹s = (U⇩e⇩r, ℱ, Γ)› decided_literals_all_neg_def)

  thus ?thesis
    by (simp add: ‹s' = (U⇩e⇩r, ℱ', Γ)› decided_literals_all_neg_def)
next
  case step_hyps: (resolution Γ ℱ U⇩e⇩r D A C U⇩e⇩r' Γ')

  have "∀Ln∈set Γ. ∀L. Ln = (L, None) ⟶ is_neg L"
    using invar by (simp add: ‹s = (U⇩e⇩r, ℱ, Γ)› decided_literals_all_neg_def)

  moreover have "set Γ' ⊆ set Γ"
    unfolding ‹Γ' = dropWhile _ Γ›
    by (meson set_mono_suffix suffix_dropWhile)

  ultimately have "∀Ln∈set Γ'. ∀L. Ln = (L, None) ⟶ is_neg L"
    by blast

  thus ?thesis
    by (simp add: ‹s' = (U⇩e⇩r', ℱ, Γ')› decided_literals_all_neg_def)
qed

definition ord_res_8_invars where
  "ord_res_8_invars N s ⟷
    trail_is_sorted N s ∧
    trail_is_lower_set N s ∧
    false_cls_is_mempty_or_has_neg_max_lit N s ∧
    trail_annotations_invars N s ∧
    decided_literals_all_neg N s"

lemma ord_res_8_preserves_invars:
  assumes
    step: "ord_res_8 N s s'" and
    invars: "ord_res_8_invars N s"
  shows "ord_res_8_invars N s'"
  using invars
  unfolding ord_res_8_invars_def
  using
    ord_res_8_preserves_trail_is_sorted[OF step]
    ord_res_8_preserves_atoms_in_trail_lower_set[OF step]
    ord_res_8_preserves_false_cls_is_mempty_or_has_neg_max_lit[OF step]
    ord_res_8_preserves_trail_annotations_invars[OF step]
    ord_res_8_preserves_decided_literals_all_neg[OF step]
  by metis

lemma rtranclp_ord_res_8_preserves_invars:
  assumes
    step: "(ord_res_8 N)⇧*⇧* s s'" and
    invars: "ord_res_8_invars N s"
  shows "ord_res_8_invars N s'"
  using step invars ord_res_8_preserves_invars
  by (smt (verit, del_insts) rtranclp_induct)

lemma tranclp_ord_res_8_preserves_invars:
  assumes
    step: "(ord_res_8 N)⇧+⇧+ s s'" and
    invars: "ord_res_8_invars N s"
  shows "ord_res_8_invars N s'"
  using step invars ord_res_8_preserves_invars
  by (smt (verit, del_insts) tranclp_induct)


lemma ex_ord_res_8_if_not_final:
  assumes
    not_final: "¬ ord_res_8_final (N, s)" and
    invars: "ord_res_8_invars N s"
  shows "∃s'. ord_res_8 N s s'"
proof -
  obtain U⇩e⇩r ℱ Γ where "s = (U⇩e⇩r, ℱ, Γ)"
    by (metis surj_pair)

  note invars' = invars[unfolded ‹s = (U⇩e⇩r, ℱ, Γ)› ord_res_8_invars_def]
  
  have
    undef_atm_or_false_cls: "
      (∃x |∈| atms_of_clss (N |∪| U⇩e⇩r). x |∉| trail_atms Γ) ∧
        ¬ (∃x |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). trail_false_cls Γ x)∨
      (∃x |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). trail_false_cls Γ x)" and
    "{#} |∉| iefac ℱ |`| (N |∪| U⇩e⇩r)"
    unfolding atomize_conj
    using not_final[unfolded ord_res_8_final.simps] ‹s = (U⇩e⇩r, ℱ, Γ)› by metis

  show ?thesis
    using undef_atm_or_false_cls
  proof (elim disjE conjE)
    assume
      ex_undef_atm: "∃x |∈| atms_of_clss (N |∪| U⇩e⇩r). x |∉| trail_atms Γ" and
      no_conflict: "¬ (∃x|∈|iefac ℱ |`| (N |∪| U⇩e⇩r). trail_false_cls Γ x)"

    moreover have "{|A⇩2 |∈| atms_of_clss (N |∪| U⇩e⇩r). ∀A⇩1 |∈| trail_atms Γ. A⇩1 ≺⇩t A⇩2|} ≠ {||}"
    proof -
      obtain A⇩2 :: "'f gterm" where
        A⇩2_in: "A⇩2 |∈| atms_of_clss (N |∪| U⇩e⇩r)" and
        A⇩2_undef: "A⇩2 |∉| trail_atms Γ"
        using ex_undef_atm by metis

      have "A⇩1 ≺⇩t A⇩2" if A⇩1_in: "A⇩1 |∈| trail_atms Γ" for A⇩1 :: "'f gterm"
      proof -
        have "A⇩1 ≠ A⇩2"
          using A⇩1_in A⇩2_undef by metis

        moreover have "linorder_trm.is_lower_fset (trail_atms Γ) (atms_of_clss (N |∪| U⇩e⇩r))"
          using invars'[unfolded trail_is_lower_set_def, simplified] by argo

        ultimately show ?thesis
          by (meson A⇩2_in A⇩2_undef linorder_trm.is_lower_set_iff linorder_trm.linorder_cases that)
      qed

      thus ?thesis
        using A⇩2_in
        by (smt (verit, ccfv_threshold) femptyE ffmember_filter)
    qed

    ultimately obtain A :: "'f gterm" where
      A_least: "linorder_trm.is_least_in_fset {|A⇩2 |∈| atms_of_clss (N |∪| U⇩e⇩r).
        ∀A⇩1 |∈| trail_atms Γ. A⇩1 ≺⇩t A⇩2|} A"
      using ex_undef_atm linorder_trm.ex_least_in_fset by presburger

    show "∃s'. ord_res_8 N s s'"
    proof (cases "∃C|∈|iefac ℱ |`| (N |∪| U⇩e⇩r). clause_could_propagate Γ C (Pos A)")
      case True
      hence "{|C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). clause_could_propagate Γ C (Pos A)|} ≠ {||}"
        by force

      then obtain C where
        C_least: "linorder_cls.is_least_in_fset
          {|C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). clause_could_propagate Γ C (Pos A)|} C"
        using linorder_cls.ex1_least_in_fset by meson

      show ?thesis
        unfolding ‹s = (U⇩e⇩r, ℱ, Γ)›
        using ord_res_8.propagate[OF no_conflict A_least C_least]
        using ord_res_8.factorize[OF no_conflict A_least C_least]
        by metis
    next
      case False
      thus ?thesis
        unfolding ‹s = (U⇩e⇩r, ℱ, Γ)›
        using ord_res_8.decide_neg[OF no_conflict A_least] by metis
    qed
  next
    assume "∃x|∈|iefac ℱ |`| (N |∪| U⇩e⇩r). trail_false_cls Γ x"
    then obtain D :: "'f gclause" where
      D_least: "linorder_cls.is_least_in_fset
        (ffilter (trail_false_cls Γ) (iefac ℱ |`| (N |∪| U⇩e⇩r))) D"
      by (metis femptyE ffmember_filter linorder_cls.ex_least_in_fset)

    hence "D |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" and "trail_false_cls Γ D"
      unfolding atomize_conj linorder_cls.is_least_in_ffilter_iff by argo

    moreover have "D ≠ {#}"
      using ‹D |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)› ‹{#} |∉| iefac ℱ |`| (N |∪| U⇩e⇩r)› by metis

    ultimately obtain A where Neg_A_max: "linorder_lit.is_maximal_in_mset D (Neg A)"
      using invars' false_cls_is_mempty_or_has_neg_max_lit_def by metis

    hence "trail_false_lit Γ (Neg A)"
      using ‹trail_false_cls Γ D›
      by (metis linorder_lit.is_maximal_in_mset_iff trail_false_cls_def)

    hence "Pos A ∈ fst ` set Γ"
      unfolding trail_false_lit_def by simp

    hence "∃C. (Pos A, Some C) ∈ set Γ"
      using invars'[unfolded decided_literals_all_neg_def, simplified]
      by fastforce

    then obtain C :: "'f gclause" where
      "map_of Γ (Pos A) = Some (Some C)"
      by (metis invars' is_pos_def map_of_SomeD not_Some_eq decided_literals_all_neg_def
          weak_map_of_SomeI)

    thus "∃s'. ord_res_8 N s s'"
      unfolding ‹s = (U⇩e⇩r, ℱ, Γ)›
      using ord_res_8.resolution D_least Neg_A_max by blast
  qed
qed

lemma ord_res_8_safe_state_if_invars:
  fixes N s
  assumes invars: "ord_res_8_invars N s"
  shows "safe_state (constant_context ord_res_8) ord_res_8_final (N, s)"
  using safe_state_constant_context_if_invars[where
      ℛ = ord_res_8 and ℱ = ord_res_8_final and ℐ = ord_res_8_invars]
  using ord_res_8_preserves_invars ex_ord_res_8_if_not_final invars by metis

end

end