Theory Non_Redundancy

theory Non_Redundancy
  imports
    SCL_FOL
    Trail_Induced_Ordering
    Initial_Literals_Generalize_Learned_Literals
    Multiset_Order_Extra
begin

context scl_fol_calculus begin

section ‹Reasonable Steps›

lemma reasonable_scl_sound_state:
  "reasonable_scl N β S S'  sound_state N β S  sound_state N β S'"
  using scl_preserves_sound_state reasonable_scl_def by blast

lemma reasonable_run_sound_state:
  "(reasonable_scl N β)** S S'  sound_state N β S  sound_state N β S'"
  by (smt (verit, best) reasonable_scl_sound_state rtranclp_induct)


subsection ‹Invariants›


subsubsection ‹No Conflict After Decide›

inductive no_conflict_after_decide for N β U where
  Nil[simp]: "no_conflict_after_decide N β U []" |
  Cons: "(is_decision_lit Ln  (S'. conflict N β (Ln # Γ, U, None) S')) 
    no_conflict_after_decide N β U Γ  no_conflict_after_decide N β U (Ln # Γ)"

definition no_conflict_after_decide' where
  "no_conflict_after_decide' N β S = no_conflict_after_decide N β (state_learned S) (state_trail S)"

lemma no_conflict_after_decide'_initial_state[simp]: "no_conflict_after_decide' N β initial_state"
  by (simp add: no_conflict_after_decide'_def no_conflict_after_decide.Nil)

lemma propagate_preserves_no_conflict_after_decide':
  assumes "propagate N β S S'" and "no_conflict_after_decide' N β S"
  shows "no_conflict_after_decide' N β S'"
  using assms
  by (auto simp: no_conflict_after_decide'_def propagate_lit_def is_decision_lit_def
      elim!: propagate.cases intro!: no_conflict_after_decide.Cons)

lemma decide_preserves_no_conflict_after_decide':
  assumes "decide N β S S'" and "S''. conflict N β S' S''" and "no_conflict_after_decide' N β S"
  shows "no_conflict_after_decide' N β S'"
  using assms
  by (auto simp: no_conflict_after_decide'_def decide_lit_def is_decision_lit_def
      elim!: decide.cases intro!: no_conflict_after_decide.Cons)

lemma conflict_preserves_no_conflict_after_decide':
  assumes "conflict N β S S'" and "no_conflict_after_decide' N β S"
  shows "no_conflict_after_decide' N β S'"
  using assms
  by (auto simp: no_conflict_after_decide'_def elim: conflict.cases)

lemma skip_preserves_no_conflict_after_decide':
  assumes "skip N β S S'" and "no_conflict_after_decide' N β S"
  shows "no_conflict_after_decide' N β S'"
  using assms
  by (auto simp: no_conflict_after_decide'_def
      elim!: skip.cases elim: no_conflict_after_decide.cases)

lemma factorize_preserves_no_conflict_after_decide':
  assumes "factorize N β S S'" and "no_conflict_after_decide' N β S"
  shows "no_conflict_after_decide' N β S'"
  using assms
  by (auto simp: no_conflict_after_decide'_def elim: factorize.cases)

lemma resolve_preserves_no_conflict_after_decide':
  assumes "resolve N β S S'" and "no_conflict_after_decide' N β S"
  shows "no_conflict_after_decide' N β S'"
  using assms
  by (auto simp: no_conflict_after_decide'_def elim: resolve.cases)

lemma learning_clause_without_conflict_preserves_nex_conflict:
  fixes N :: "('f, 'v) Term.term clause fset"
  assumes "γ. is_ground_cls (C  γ)  trail_false_cls Γ (C  γ)"
  shows "S'. conflict N β (Γ, U, None) S'  S'. conflict N β (Γ, finsert C U, None) S'"
proof (elim contrapos_nn exE)
  fix S'
  assume "conflict N β (Γ, finsert C U, None :: ('f, 'v) closure option) S'"
  then show "S'. conflict N β (Γ, U, None) S'"
  proof (cases N β "(Γ, finsert C U, None :: ('f, 'v) closure option)" S' rule: conflict.cases)
    case (conflictI D γ)
    then show ?thesis
      using assms conflict.intros by blast
  qed
qed

lemma backtrack_preserves_no_conflict_after_decide':
  assumes step: "backtrack N β S S'" and invar: "no_conflict_after_decide' N β S"
  shows "no_conflict_after_decide' N β S'"
  using step
proof (cases N β S S' rule: backtrack.cases)
  case (backtrackI Γ Γ' Γ'' K L σ D U)
  have "no_conflict_after_decide N β U (Γ' @ Γ'')"
    using invar
    unfolding backtrackI(1,2,3) no_conflict_after_decide'_def
    by (auto simp: decide_lit_def elim: no_conflict_after_decide.cases)
  hence "no_conflict_after_decide N β U Γ''"
    by (induction Γ') (auto elim: no_conflict_after_decide.cases)
  hence "no_conflict_after_decide N β (finsert (add_mset L D) U) Γ''"
    using backtrackI(5)
  proof (induction Γ'')
    case Nil
    show ?case
      by (auto intro: no_conflict_after_decide.Nil)
  next
    case (Cons Ln Γ'')
    hence "γ. is_ground_cls (add_mset L D  γ)  trail_false_cls (Ln # Γ'') (add_mset L D  γ)"
      by metis
    hence "γ. is_ground_cls (add_mset L D  γ)  trail_false_cls Γ'' (add_mset L D  γ)"
      by (metis (no_types, opaque_lifting) image_insert insert_iff list.set(2) trail_false_cls_def
          trail_false_lit_def)
    hence 1: "no_conflict_after_decide N β (finsert (add_mset L D) U) Γ''"
      by (rule Cons.IH)

    show ?case
    proof (intro no_conflict_after_decide.Cons impI)
      assume "is_decision_lit Ln"
      with Cons.hyps have "S'. conflict N β (Ln # Γ'', U, None) S'"
        by simp
      then show "S'. conflict N β (Ln # Γ'', finsert (add_mset L D) U, None) S'"
        using learning_clause_without_conflict_preserves_nex_conflict
        using γ. is_ground_cls (add_mset L D  γ)  trail_false_cls (Ln # Γ'') (add_mset L D  γ)
        by blast
    next
      show "no_conflict_after_decide N β (finsert (add_mset L D) U) Γ''"
        using 1 .
    qed
  qed
  thus ?thesis
    unfolding backtrackI(1,2) no_conflict_after_decide'_def by simp
qed

lemma reasonable_scl_preserves_no_conflict_after_decide':
  assumes "reasonable_scl N β S S'" and "no_conflict_after_decide' N β S"
  shows "no_conflict_after_decide' N β S'"
  using assms unfolding reasonable_scl_def scl_def
  using propagate_preserves_no_conflict_after_decide' decide_preserves_no_conflict_after_decide'
    conflict_preserves_no_conflict_after_decide' skip_preserves_no_conflict_after_decide'
    factorize_preserves_no_conflict_after_decide' resolve_preserves_no_conflict_after_decide'
    backtrack_preserves_no_conflict_after_decide'
  by metis


subsection ‹Miscellaneous Lemmas›

lemma before_reasonable_conflict:
  assumes conf: "conflict N β S1 S2" and
    invars: "learned_nonempty S1" "trail_propagated_or_decided' N β S1"
      "no_conflict_after_decide' N β S1"
  shows "{#} |∈| N  (S0. propagate N β S0 S1)"
  using before_conflict[OF conf invars(1,2)]
proof (elim disjE exE)
  fix S0 assume "decide N β S0 S1"
  hence False
  proof (cases N β S0 S1 rule: decide.cases)
    case (decideI L γ Γ U)
    with invars(3) have "no_conflict_after_decide N β U (trail_decide Γ (L ⋅l γ))"
      by (simp add: no_conflict_after_decide'_def)
    hence "S'. conflict N β (trail_decide Γ (L ⋅l γ), U, None) S'"
      by (rule no_conflict_after_decide.cases) (simp_all add: decide_lit_def is_decision_lit_def)
    then show ?thesis
      using conf unfolding decideI(1,2) by metis
  qed
  thus ?thesis ..
qed auto


section ‹Regular Steps›

lemma regular_scl_if_conflict[simp]: "conflict N β S S'  regular_scl N β S S'"
  by (simp add: regular_scl_def)

lemma regular_scl_if_skip[simp]: "skip N β S S'  regular_scl N β S S'"
  by (auto simp: regular_scl_def reasonable_scl_def scl_def elim: conflict.cases skip.cases)

lemma regular_scl_if_factorize[simp]: "factorize N β S S'  regular_scl N β S S'"
  by (auto simp: regular_scl_def reasonable_scl_def scl_def elim: conflict.cases factorize.cases)

lemma regular_scl_if_resolve[simp]: "resolve N β S S'  regular_scl N β S S'"
  by (auto simp: regular_scl_def reasonable_scl_def scl_def elim: conflict.cases resolve.cases)

lemma regular_scl_if_backtrack[simp]: "backtrack N β S S'  regular_scl N β S S'"
  by (smt (verit) backtrack.cases decide_well_defined(6) option.discI regular_scl_def conflict.simps
      reasonable_scl_def scl_def state_conflict_simp)

lemma regular_scl_sound_state: "regular_scl N β S S'  sound_state N β S  sound_state N β S'"
  by (rule reasonable_scl_sound_state[OF reasonable_if_regular])

lemma regular_run_sound_state:
  "(regular_scl N β)** S S'  sound_state N β S  sound_state N β S'"
  by (smt (verit, best) regular_scl_sound_state rtranclp_induct)


subsection ‹Invariants›


subsubsection ‹Almost No Conflict With Trail›

inductive no_conflict_with_trail for N β U where
  Nil: "(S'. conflict N β ([], U, None) S')  no_conflict_with_trail N β U []" |
  Cons: "(S'. conflict N β (Ln # Γ, U, None) S') 
    no_conflict_with_trail N β U Γ  no_conflict_with_trail N β U (Ln # Γ)"

lemma nex_conflict_if_no_conflict_with_trail:
  assumes "no_conflict_with_trail N β U Γ"
  shows "S'. conflict N β (Γ, U, None) S'"
  using assms by (auto elim: no_conflict_with_trail.cases)

lemma nex_conflict_if_no_conflict_with_trail':
  assumes "no_conflict_with_trail N β U Γ"
  shows "S'. conflict N β ([], U, None) S'"
  using assms
  by (induction Γ rule: no_conflict_with_trail.induct) simp_all

lemma no_conflict_after_decide_if_no_conflict_with_trail:
  "no_conflict_with_trail N β U Γ  no_conflict_after_decide N β U Γ"
  by (induction Γ rule: no_conflict_with_trail.induct)
    (simp_all add: no_conflict_after_decide.Cons)

lemma not_trail_false_cls_if_no_conflict_with_trail:
  "no_conflict_with_trail N β U Γ  D |∈| N |∪| U  D  {#}  is_ground_cls (D  γ) 
    ¬ trail_false_cls Γ (D  γ)"
proof (induction Γ rule: no_conflict_with_trail.induct)
  case Nil
  thus ?case by simp
next
  case (Cons Ln Γ)
  hence "¬ trail_false_cls (Ln # Γ) (D  γ)"
    by (metis fst_conv not_trail_false_ground_cls_if_no_conflict state_conflict_simp
        state_learned_simp state_trail_def)
  thus ?case
    by simp
qed

definition almost_no_conflict_with_trail where
  "almost_no_conflict_with_trail N β S 
    {#} |∈| N  state_trail S = [] 
    no_conflict_with_trail N β (state_learned S)
      (case state_trail S of []  [] | Ln # Γ  if is_decision_lit Ln then Ln # Γ else Γ)"

lemma nex_conflict_if_no_conflict_with_trail'':
  assumes no_conf: "state_conflict S = None" and "{#} |∉| N" and "learned_nonempty S"
    "no_conflict_with_trail N β (state_learned S) (state_trail S)"
  shows "S'. conflict N β S S'"
proof -
  from no_conf obtain Γ U where S_def: "S = (Γ, U, None)"
    by (metis state_simp)

  from learned_nonempty S have "{#} |∉| U"
    by (simp add: S_def learned_nonempty_def)

  show ?thesis
    using assms(4)
    unfolding S_def state_proj_simp
  proof (cases N β U Γ rule: no_conflict_with_trail.cases)
    case Nil
    then show "S'. conflict N β (Γ, U, None) S'"
      using {#} |∉| N {#} |∉| U
      by (auto simp: trail_false_cls_def elim: conflict.cases)
  next
    case (Cons Ln Γ')
    then show "S'. conflict N β (Γ, U, None) S'"
      by (auto intro: no_conflict_tail_trail)
  qed
qed

lemma no_conflict_with_trail_if_nex_conflict:
  assumes no_conf: "S'. conflict N β S S'" "state_conflict S = None"
  shows "no_conflict_with_trail N β (state_learned S) (state_trail S)"
proof -
  from no_conf(2) obtain Γ U where S_def: "S = (Γ, U, None)"
    by (metis state_simp)

  show ?thesis
    using no_conf(1)
    unfolding S_def state_proj_simp
  proof (induction Γ)
    case Nil
    thus ?case by (simp add: no_conflict_with_trail.Nil)
  next
    case (Cons Ln Γ)
    have "a. conflict N β (Γ, U, None) a"
      by (rule no_conflict_tail_trail[OF Cons.prems])
    hence "no_conflict_with_trail N β U Γ"
      by (rule Cons.IH)
    then show ?case
      using Cons.prems
      by (auto intro: no_conflict_with_trail.Cons)
  qed
qed

lemma almost_no_conflict_with_trail_if_no_conflict_with_trail:
  "no_conflict_with_trail N β U Γ  almost_no_conflict_with_trail N β (Γ, U, Cl)"
  by (cases Γ) (auto simp: almost_no_conflict_with_trail_def elim: no_conflict_with_trail.cases)

lemma almost_no_conflict_with_trail_initial_state[simp]:
  "almost_no_conflict_with_trail N β initial_state"
  by (cases "{#} |∈| N") (auto simp: almost_no_conflict_with_trail_def trail_false_cls_def
      elim!: conflict.cases intro: no_conflict_with_trail.Nil)

lemma propagate_preserves_almost_no_conflict_with_trail:
  assumes step: "propagate N β S S'" and reg_step: "regular_scl N β S S'"
  shows "almost_no_conflict_with_trail N β S'"
  using reg_step[unfolded regular_scl_def]
proof (elim disjE conjE)
  assume "conflict N β S S'"
  with step have False
    using conflict_well_defined by blast
  thus ?thesis ..
next
  assume no_conf: "S'. conflict N β S S'" and "reasonable_scl N β S S'"
  from step show ?thesis
  proof (cases N β S S' rule: propagate.cases)
    case step_hyps: (propagateI C U L C' γ C0 C1 Γ μ)
    have "no_conflict_with_trail N β U Γ"
      by (rule no_conflict_with_trail_if_nex_conflict[OF no_conf,
            unfolded step_hyps state_proj_simp, OF refl])
    thus ?thesis
      unfolding step_hyps(1,2)
      by (simp add: almost_no_conflict_with_trail_def propagate_lit_def is_decision_lit_def)
  qed
qed

lemma decide_preserves_almost_no_conflict_with_trail:
  assumes step: "decide N β S S'" and reg_step: "regular_scl N β S S'"
  shows "almost_no_conflict_with_trail N β S'"
proof -
  from reg_step have res_step: "reasonable_scl N β S S'"
    by (rule reasonable_if_regular)

  from step obtain Γ U where S'_def: "S' = (Γ, U, None)"
    by (auto elim: decide.cases)

  have "no_conflict_with_trail N β (state_learned S') (state_trail S')"
  proof (rule no_conflict_with_trail_if_nex_conflict)
    show "S''. conflict N β S' S''"
      using step res_step[unfolded reasonable_scl_def] by argo
  next
    show "state_conflict S' = None"
      by (simp add: S'_def)
  qed
  thus ?thesis
    unfolding S'_def
    by (simp add: almost_no_conflict_with_trail_if_no_conflict_with_trail)
qed

lemma almost_no_conflict_with_trail_conflict_not_relevant:
  "almost_no_conflict_with_trail N β (Γ, U, Cl1) 
   almost_no_conflict_with_trail N β (Γ, U, Cl2)"
  by (simp add: almost_no_conflict_with_trail_def)

lemma conflict_preserves_almost_no_conflict_with_trail:
  assumes step: "conflict N β S S'" and invar: "almost_no_conflict_with_trail N β S"
  shows "almost_no_conflict_with_trail N β S'"
proof -
  from step obtain Γ U Cl where "S = (Γ, U, None)" and "S' = (Γ, U, Some Cl)"
    by (auto elim: conflict.cases)
  with invar show ?thesis
    using almost_no_conflict_with_trail_conflict_not_relevant by metis
qed

lemma skip_preserves_almost_no_conflict_with_trail:
  assumes step: "skip N β S S'" and invar: "almost_no_conflict_with_trail N β S"
  shows "almost_no_conflict_with_trail N β S'"
  using step
proof (cases N β S S' rule: skip.cases)
  case step_hyps: (skipI L D σ n Γ U)
  have "no_conflict_with_trail N β U (if is_decision_lit (L, n) then (L, n) # Γ else Γ)"
    using invar unfolding step_hyps(1,2) by (simp add: almost_no_conflict_with_trail_def)
  hence "no_conflict_with_trail N β U Γ"
    by (cases "is_decision_lit (L, n)") (auto elim: no_conflict_with_trail.cases)
  then show ?thesis
    unfolding step_hyps(1,2)
    by (rule almost_no_conflict_with_trail_if_no_conflict_with_trail)
qed

lemma factorize_preserves_almost_no_conflict_with_trail:
  assumes step: "factorize N β S S'" and invar: "almost_no_conflict_with_trail N β S"
  shows "almost_no_conflict_with_trail N β S'"
proof -
  from step obtain Γ U Cl1 Cl2 where "S = (Γ, U, Some Cl1)" and "S' = (Γ, U, Some Cl2)"
    by (auto elim: factorize.cases)
  with invar show ?thesis
    using almost_no_conflict_with_trail_conflict_not_relevant by metis
qed

lemma resolve_preserves_almost_no_conflict_with_trail:
  assumes step: "resolve N β S S'" and invar: "almost_no_conflict_with_trail N β S"
  shows "almost_no_conflict_with_trail N β S'"
proof -
  from step obtain Γ U Cl1 Cl2 where "S = (Γ, U, Some Cl1)" and "S' = (Γ, U, Some Cl2)"
    by (auto elim: resolve.cases)
  with invar show ?thesis
    using almost_no_conflict_with_trail_conflict_not_relevant by metis
qed

lemma backtrack_preserves_almost_no_conflict_with_trail:
  assumes step: "backtrack N β S S'" and invar: "almost_no_conflict_with_trail N β S"
  shows "almost_no_conflict_with_trail N β S'"
  using step
proof (cases N β S S' rule: backtrack.cases)
  case step_hyps: (backtrackI Γ Γ' Γ'' K L σ D U)
  from invar have "no_conflict_with_trail N β U ((- (L ⋅l σ), None) # Γ' @ Γ'')"
    by (simp add: step_hyps almost_no_conflict_with_trail_def decide_lit_def is_decision_lit_def)
  hence "no_conflict_with_trail N β U (Γ' @ Γ'')"
    by (auto elim: no_conflict_with_trail.cases)
  hence "no_conflict_with_trail N β U Γ''"
    by (induction Γ') (auto elim: no_conflict_with_trail.cases)
  then have "no_conflict_with_trail N β (finsert (add_mset L D) U) Γ''"
    by (metis learning_clause_without_conflict_preserves_nex_conflict
        nex_conflict_if_no_conflict_with_trail no_conflict_with_trail_if_nex_conflict
        state_conflict_simp state_learned_simp state_trail_simp step_hyps(5))
  thus ?thesis
    unfolding step_hyps(1,2)
    by (rule almost_no_conflict_with_trail_if_no_conflict_with_trail)
qed

lemma regular_scl_preserves_almost_no_conflict_with_trail:
  assumes "regular_scl N β S S'" and "almost_no_conflict_with_trail N β S"
  shows "almost_no_conflict_with_trail N β S'"
  using assms
  using propagate_preserves_almost_no_conflict_with_trail decide_preserves_almost_no_conflict_with_trail
    conflict_preserves_almost_no_conflict_with_trail skip_preserves_almost_no_conflict_with_trail
    factorize_preserves_almost_no_conflict_with_trail resolve_preserves_almost_no_conflict_with_trail
    backtrack_preserves_almost_no_conflict_with_trail
  by (metis scl_def reasonable_if_regular scl_if_reasonable)


subsubsection ‹Backtrack Follows Regular Conflict Resolution›


lemma before_conflict_in_regular_run:
  assumes
    reg_run: "(regular_scl N β)** initial_state S1" and
    conf: "conflict N β S1 S2" and
    "{#} |∉| N"
  shows "S0. (regular_scl N β)** initial_state S0  regular_scl N β S0 S1  (propagate N β S0 S1)"
proof -
  from reg_run conf show ?thesis
  proof (induction S1 arbitrary: S2 rule: rtranclp_induct)
    case base
    with {#} |∉| N have False
      by (meson fempty_iff funion_iff mempty_in_iff_ex_conflict)
    thus ?case ..
  next
    case (step S0 S1)
    from step.hyps(1) have "learned_nonempty S0"
      by (induction S0 rule: rtranclp_induct)
        (simp_all add: scl_preserves_learned_nonempty[OF scl_if_reasonable[OF
              reasonable_if_regular]])
    with step.hyps(2) have "learned_nonempty S1"
      by (simp add: scl_preserves_learned_nonempty[OF scl_if_reasonable[OF reasonable_if_regular]])

    from step.hyps(1) have "trail_propagated_or_decided' N β S0"
      by (induction S0 rule: rtranclp_induct)
        (simp_all add: scl_preserves_trail_propagated_or_decided[OF scl_if_reasonable[OF
              reasonable_if_regular]])
    with step.hyps(2) have "trail_propagated_or_decided' N β S1"
      by (simp add: scl_preserves_trail_propagated_or_decided[OF scl_if_reasonable[OF
              reasonable_if_regular]])

    from step.hyps(1) have "almost_no_conflict_with_trail N β S0"
      by (induction S0 rule: rtranclp_induct)
        (simp_all add: regular_scl_preserves_almost_no_conflict_with_trail)
    with step.hyps(2) have "almost_no_conflict_with_trail N β S1"
      by (simp add: regular_scl_preserves_almost_no_conflict_with_trail)

    show ?case
    proof (intro exI conjI)
      show "(regular_scl N β)** initial_state S0"
        using step.hyps by simp
    next
      show "regular_scl N β S0 S1"
        using step.hyps by simp
    next
      from step.prems obtain Γ U C γ where
        S1_def: "S1 = (Γ, U, None)" and
        S2_def: "S2 = (Γ, U, Some (C, γ))" and
        C_in: "C |∈| N |∪| U" and
        ground_conf: "is_ground_cls (C  γ)" and
        tr_false_conf: "trail_false_cls Γ (C  γ)"
        unfolding conflict.simps by auto
      with step.hyps have "¬ conflict N β S0 S1" and "reasonable_scl N β S0 S1"
        unfolding regular_scl_def by (simp_all add: conflict.simps)
      with step.prems have "scl N β S0 S1" and "¬ decide N β S0 S1"
        unfolding reasonable_scl_def by blast+
      moreover from step.prems have "¬ backtrack N β S0 S1"
      proof (cases Γ)
        case Nil
        then show ?thesis
        using {#} |∉| N almost_no_conflict_with_trail N β S1 step.prems
        by (auto simp: S1_def almost_no_conflict_with_trail_def elim: no_conflict_with_trail.cases)
      next
        case (Cons Ln Γ')
        have "C  {#}"
          using {#} |∉| N
          by (metis C_in S1_def learned_nonempty S1 funionE learned_nonempty_def state_proj_simp(2))

        from Cons have "¬ is_decision_lit Ln"
          using ¬ decide N β S0 S1[unfolded S1_def]
          by (metis (mono_tags, lifting) S1_def almost_no_conflict_with_trail N β S1
              almost_no_conflict_with_trail_def list.discI list.simps(5)
              nex_conflict_if_no_conflict_with_trail state_learned_simp state_trail_simp step.prems)
        with {#} |∉| N have "no_conflict_with_trail N β U Γ'"
          using almost_no_conflict_with_trail N β S1
          by (simp add: Cons S1_def almost_no_conflict_with_trail_def)
        with Cons show ?thesis
          unfolding S1_def
          using {#} |∉| N
          by (smt (verit) S2_def almost_no_conflict_with_trail N β S0 learned_nonempty S1
              almost_no_conflict_with_trail_def backtrack.simps conflict.cases finsert_iff funionE
              funion_finsert_right learned_nonempty_def list.case(2) list.sel(3) list.simps(3)
              no_conflict_with_trail.simps not_trail_false_cls_if_no_conflict_with_trail
              state_learned_simp state_trail_simp step.prems suffixI decide_lit_def
              trail_false_cls_if_trail_false_suffix)
      qed
      ultimately show "propagate N β S0 S1"
        by (simp add: scl_def S1_def skip.simps conflict.simps factorize.simps resolve.simps)
    qed
  qed
qed

definition regular_conflict_resolution where
  "regular_conflict_resolution N β S  {#} |∉| N 
    (case state_conflict S of
      None  (regular_scl N β)** initial_state S |
      Some _  (S0 S1 S2 S3. (regular_scl N β)** initial_state S0 
        propagate N β S0 S1  regular_scl N β S0 S1 
        conflict N β S1 S2  regular_scl N β S1 S2 
        (factorize N β)** S2 S3  (regular_scl N β)** S2 S3 
        (S3 = S  (S4. resolve N β S3 S4  (skip N β  factorize N β  resolve N β)** S4 S))))"

lemma regular_conflict_resolution_initial_state[simp]:
  "regular_conflict_resolution N β initial_state"
  by (simp add: regular_conflict_resolution_def)

lemma propagate_preserves_regular_conflict_resolution:
  assumes step: "propagate N β S S'" and reg_step: "regular_scl N β S S'" and
    invar: "regular_conflict_resolution N β S"
  shows "regular_conflict_resolution N β S'"
proof -
  from step have "state_conflict S = None" and "state_conflict S' = None"
    by (auto elim: propagate.cases)

  show ?thesis
    unfolding regular_conflict_resolution_def state_conflict S' = None
    unfolding option.case
  proof (rule impI)
    assume "{#} |∉| N"
    with invar have "(regular_scl N β)** initial_state S"
      unfolding regular_conflict_resolution_def state_conflict S = None by simp
    thus "(regular_scl N β)** initial_state S'"
      using reg_step by (rule rtranclp.rtrancl_into_rtrancl)
  qed
qed

lemma decide_preserves_regular_conflict_resolution:
  assumes step: "decide N β S S'" and reg_step: "regular_scl N β S S'" and
    invar: "regular_conflict_resolution N β S"
  shows "regular_conflict_resolution N β S'"
proof -
  from step have "state_conflict S = None" and "state_conflict S' = None"
    by (auto elim: decide.cases)

  show ?thesis
    unfolding regular_conflict_resolution_def state_conflict S' = None
    unfolding option.case
  proof (rule impI)
    assume "{#} |∉| N"
    with invar have "(regular_scl N β)** initial_state S"
      unfolding regular_conflict_resolution_def state_conflict S = None by simp
    thus "(regular_scl N β)** initial_state S'"
      using reg_step by (rule rtranclp.rtrancl_into_rtrancl)
  qed
qed

lemma conflict_preserves_regular_conflict_resolution:
  assumes step: "conflict N β S S'" and reg_step: "regular_scl N β S S'" and
    invar: "regular_conflict_resolution N β S"
  shows "regular_conflict_resolution N β S'"
proof -
  from step obtain C γ where "state_conflict S = None" and "state_conflict S' = Some (C, γ)"
    by (auto elim!: conflict.cases)

  show ?thesis
    unfolding regular_conflict_resolution_def state_conflict S' = Some (C, γ)
    unfolding option.cases
  proof (rule impI)
    assume "{#} |∉| N"
    with invar have reg_run: "(regular_scl N β)** initial_state S"
      unfolding regular_conflict_resolution_def state_conflict S = None by simp

    from {#} |∉| N obtain S0 where
      "(regular_scl N β)** initial_state S0" "propagate N β S0 S" "regular_scl N β S0 S"
      using before_conflict_in_regular_run[OF reg_run step] by metis

    with step show "S0 S1 S2 S3. (regular_scl N β)** initial_state S0 
      propagate N β S0 S1  regular_scl N β S0 S1 
      conflict N β S1 S2  regular_scl N β S1 S2 
      (factorize N β)** S2 S3  (regular_scl N β)** S2 S3 
      (S3 = S'  (S4. resolve N β S3 S4  (skip N β  factorize N β  resolve N β)** S4 S'))"
      using regular_scl_if_conflict
      by blast
  qed
qed

lemma
  assumes "almost_no_conflict_with_trail N β S" and "{#} |∉| N"
  shows "no_conflict_after_decide' N β S"
proof -
  obtain U Γ Cl where S_def: "S = (Γ, U, Cl)"
    by (metis state_simp)

  show ?thesis
  proof (cases Γ)
    case Nil
    thus ?thesis
      by (simp add: S_def no_conflict_after_decide'_def)
  next
    case (Cons Ln Γ')
    with assms have no_conf_with_trail:
      "no_conflict_with_trail N β U (if is_decision_lit Ln then Ln # Γ' else Γ')"
      by (simp add: S_def almost_no_conflict_with_trail_def)

    show ?thesis
      using no_conf_with_trail
      by (cases "is_decision_lit Ln")
        (simp_all add: S_def Cons no_conflict_after_decide'_def no_conflict_after_decide.Cons
          no_conflict_after_decide_if_no_conflict_with_trail)
  qed
qed

lemma mempty_not_in_learned_if_almost_no_conflict_with_trail:
  "almost_no_conflict_with_trail N β S  {#} |∉| N  {#} |∉| state_learned S"
  unfolding almost_no_conflict_with_trail_def
  using nex_conflict_if_no_conflict_with_trail'[folded mempty_in_iff_ex_conflict]
  by simp

lemma skip_preserves_regular_conflict_resolution:
  assumes step: "skip N β S S'" and reg_step: "regular_scl N β S S'" and
    invar: "regular_conflict_resolution N β S"
  shows "regular_conflict_resolution N β S'"
proof -
  from step obtain C γ where
    "state_conflict S = Some (C, γ)" and "state_conflict S' = Some (C, γ)"
    by (auto elim!: skip.cases)

  show ?thesis
    unfolding regular_conflict_resolution_def state_conflict S' = Some (C, γ)
    unfolding option.cases
  proof (intro impI)
    assume "{#} |∉| N"
    with invar obtain S0 S1 S2 S3 where
      reg_run: "(regular_scl N β)** initial_state S0" and
      propa: "propagate N β S0 S1" "regular_scl N β S0 S1" and
      confl: "conflict N β S1 S2" "regular_scl N β S1 S2" and
      facto: "(factorize N β)** S2 S3" "(regular_scl N β)** S2 S3" and
      maybe_reso: "S3 = S  (S4. resolve N β S3 S4  (skip N β  factorize N β  resolve N β)** S4 S)"
      unfolding regular_conflict_resolution_def state_conflict S = Some (C, γ)
      unfolding option.cases
      by metis

    from reg_run have "(regular_scl N β)** initial_state S1"
      using regular_scl N β S0 S1 by simp
    hence "(regular_scl N β)** initial_state S2"
      using regular_scl N β S1 S2 by simp
    hence "(regular_scl N β)** initial_state S3"
      using (regular_scl N β)** S2 S3 by simp

    from (factorize N β)** S2 S3 have "state_trail S3 = state_trail S2"
      by (induction S3 rule: rtranclp_induct) (auto elim: factorize.cases)
    also from conflict N β S1 S2 have " = state_trail S1"
      by (auto elim: conflict.cases)
    finally have "state_trail S3 = state_trail S1"
      by assumption

    from (factorize N β)** S2 S3 have "state_learned S3 = state_learned S2"
    proof (induction S3 rule: rtranclp_induct)
      case base
      show ?case by simp
    next
      case (step y z)
      thus ?case
        by (elim factorize.cases) simp
    qed
    also from conflict N β S1 S2 have " = state_learned S1"
      by (auto elim: conflict.cases)
    finally have "state_learned S3 = state_learned S1"
      by assumption

    from propagate N β S0 S1 have "state_learned S1 = state_learned S0"
      by (auto elim: propagate.cases)

    from propagate N β S0 S1 obtain L C γ where
      "state_trail S1 = trail_propagate (state_trail S0) L C γ"
      by (auto elim: propagate.cases)

    from (regular_scl N β)** initial_state S3 have "almost_no_conflict_with_trail N β S3"
      using regular_scl_preserves_almost_no_conflict_with_trail
      by (induction S3 rule: rtranclp_induct) simp_all

    show "S0 S1 S2 S3. (regular_scl N β)** initial_state S0 
      propagate N β S0 S1  regular_scl N β S0 S1 
      conflict N β S1 S2  regular_scl N β S1 S2 
      (factorize N β)** S2 S3  (regular_scl N β)** S2 S3 
      (S3 = S'  (S4. resolve N β S3 S4  (skip N β  factorize N β  resolve N β)** S4 S'))"
      using reg_run propa confl facto
    proof (intro impI exI conjI)
      show "S3 = S'  (S4. resolve N β S3 S4  (skip N β  factorize N β  resolve N β)** S4 S')"
        using maybe_reso
      proof (elim disjE exE conjE)
        fix S4 assume "resolve N β S3 S4" and "(skip N β  factorize N β  resolve N β)** S4 S"
        with step have "S4. resolve N β S3 S4  (skip N β  factorize N β  resolve N β)** S4 S'"
          by (meson rtranclp.rtrancl_into_rtrancl sup2CI)
        thus ?thesis ..
      next
        assume "S3 = S"
        with almost_no_conflict_with_trail N β S3 {#} |∉| N
        have no_conf_with_trail: "no_conflict_with_trail N β (state_learned S)
          (case state_trail S of []  [] | Ln # Γ  if is_decision_lit Ln then Ln # Γ else Γ)"
          by (simp add: almost_no_conflict_with_trail_def)
        hence "{#} |∉| state_learned S"
          using nex_conflict_if_no_conflict_with_trail'[folded mempty_in_iff_ex_conflict]
          by simp

        from no_conf_with_trail
        have no_conf_with_trail': "no_conflict_with_trail N β (state_learned S1) (state_trail S0)"
          using S3 = S state_trail S3 = state_trail S1
            state_learned S3 = state_learned S1
            state_trail S1 = trail_propagate (state_trail S0) L C γ
          by (simp add: propagate_lit_def is_decision_lit_def)

        have "D γD. state_conflict S2 = Some (D, γD)  - (L ⋅l γ) ∈# D  γD"
          using conflict N β S1 S2
        proof (cases N β S1 S2 rule: conflict.cases)
          case (conflictI D U γD Γ)
          hence "trail_false_cls (trail_propagate (state_trail S0) L C γ) (D  γD)"
            using state_trail S1 = trail_propagate (state_trail S0) L C γ
            by simp

          moreover from no_conf_with_trail' have "¬ trail_false_cls (state_trail S0) (D  γD)"
            unfolding state_learned S1 = state_learned S0
          proof (rule not_trail_false_cls_if_no_conflict_with_trail)
            show "D |∈| N |∪| state_learned S0"
              using state_learned S1 = state_learned S0 local.conflictI(1) local.conflictI(3)
              by fastforce
          next
            have "{#} |∉| U"
              using {#} |∉| state_learned S S3 = S state_learned S3 = state_learned S1
              unfolding conflictI(1,2)
              by simp
            thus "D  {#}"
              using {#} |∉| N D |∈| N |∪| U
              by auto
          next
            show "is_ground_cls (D  γD)"
              by (rule is_ground_cls (D  γD))
          qed

          ultimately have "- (L ⋅l γ) ∈# D  γD"
            by (metis subtrail_falseI propagate_lit_def)

          moreover have "state_conflict S2 = Some (D, γD)"
            unfolding conflictI(1,2) by simp

          ultimately show ?thesis
            by metis
        qed
        then obtain D γD where "state_conflict S2 = Some (D, γD)" and "- (L ⋅l γ) ∈# D  γD"
          by metis

        with (factorize N β)** S2 S3
        have "D' γD'. state_conflict S3 = Some (D', γD')  - (L ⋅l γ) ∈# D'  γD'"
        proof (induction S3 arbitrary: rule: rtranclp_induct)
          case base
          thus ?case by simp
        next
          case (step y z)
          then obtain D' γD' where "state_conflict y = Some (D', γD')" and "- (L ⋅l γ) ∈# D'  γD'"
            by auto
          then show ?case
            using step.hyps(2)
            by (metis conflict_set_after_factorization)
        qed
        with step have False
          using state_trail S3 = state_trail S1
          unfolding S3 = S state_trail S1 = trail_propagate (state_trail S0) L C γ
          by (auto simp add: propagate_lit_def elim!: skip.cases)
        thus ?thesis ..
      qed
    qed
  qed
qed

lemma factorize_preserves_regular_conflict_resolution:
  assumes step: "factorize N β S S'" and reg_step: "regular_scl N β S S'" and
    invar: "regular_conflict_resolution N β S"
  shows "regular_conflict_resolution N β S'"
proof -
  from step obtain C γ C' γ' where
    "state_conflict S = Some (C, γ)" and "state_conflict S' = Some (C', γ')"
    by (auto elim!: factorize.cases)

  show ?thesis
    unfolding regular_conflict_resolution_def state_conflict S' = Some (C', γ')
    unfolding option.cases
  proof (intro impI)
    assume "{#} |∉| N"
    with invar obtain S0 S1 S2 S3 where
      reg_run: "(regular_scl N β)** initial_state S0" and
      propa: "propagate N β S0 S1" "regular_scl N β S0 S1" and
      confl: "conflict N β S1 S2" "regular_scl N β S1 S2" and
      facto: "(factorize N β)** S2 S3" "(regular_scl N β)** S2 S3" and
      maybe_reso: "S3 = S  (S4. resolve N β S3 S4  (skip N β  factorize N β  resolve N β)** S4 S)"
      unfolding regular_conflict_resolution_def state_conflict S = Some (C, γ)
      unfolding option.cases
      by metis

    show "S0 S1 S2 S3. (regular_scl N β)** initial_state S0 
      propagate N β S0 S1  regular_scl N β S0 S1 
      conflict N β S1 S2  regular_scl N β S1 S2 
      (factorize N β)** S2 S3  (regular_scl N β)** S2 S3 
      (S3 = S'  (S4. resolve N β S3 S4  (skip N β  factorize N β  resolve N β)** S4 S'))"
      using maybe_reso
    proof (elim disjE exE conjE)
      assume "S3 = S"
      show ?thesis
        using reg_run propa confl
      proof (intro exI conjI)
        show "(factorize N β)** S2 S'"
          using (factorize N β)** S2 S3 step
          by (simp add: S3 = S)
      next
        show "(regular_scl N β)** S2 S'"
          using (regular_scl N β)** S2 S3 reg_step
          by (simp add: S3 = S)
      next
        show "S' = S'  (S4. resolve N β S' S4  (skip N β  factorize N β  resolve N β)** S4 S')"
          by simp
      qed
    next
      fix S4 assume hyps: "resolve N β S3 S4" "(skip N β  factorize N β  resolve N β)** S4 S"
      show ?thesis
        using reg_run propa confl facto
      proof (intro exI conjI)
        show "S3 = S'  (S4. resolve N β S3 S4  (skip N β  factorize N β  resolve N β)** S4 S')"
          using hyps step
          by (meson rtranclp.rtrancl_into_rtrancl sup2CI)
      qed
    qed
  qed
qed

lemma resolve_preserves_regular_conflict_resolution:
  assumes step: "resolve N β S S'" and reg_step: "regular_scl N β S S'" and
    invar: "regular_conflict_resolution N β S"
  shows "regular_conflict_resolution N β S'"
proof -
  from step obtain C γ C' γ' where
    "state_conflict S = Some (C, γ)" and "state_conflict S' = Some (C', γ')"
    by (auto elim!: resolve.cases)

  show ?thesis
    unfolding regular_conflict_resolution_def state_conflict S' = Some (C', γ')
    unfolding option.cases
  proof (intro impI)
    from step have "state_conflict S  None"
      by (auto elim: resolve.cases)

    assume "{#} |∉| N"
    with invar obtain S0 S1 S2 S3 where
      reg_run: "(regular_scl N β)** initial_state S0" and
      "propagate N β S0 S1" "regular_scl N β S0 S1" and
      "conflict N β S1 S2" "regular_scl N β S1 S2" and
      "(factorize N β)** S2 S3" "(regular_scl N β)** S2 S3" and
      maybe_reso: "S3 = S  (S4. resolve N β S3 S4  (skip N β  factorize N β  resolve N β)** S4 S)"
      unfolding regular_conflict_resolution_def state_conflict S = Some (C, γ)
      unfolding option.cases
      by metis

    then show "S0 S1 S2 S3. (regular_scl N β)** initial_state S0 
      propagate N β S0 S1  regular_scl N β S0 S1 
      conflict N β S1 S2  regular_scl N β S1 S2 
      (factorize N β)** S2 S3  (regular_scl N β)** S2 S3 
      (S3 = S'  (S4. resolve N β S3 S4  (skip N β  factorize N β  resolve N β)** S4 S'))"
    proof (intro exI conjI)
      show "S3 = S'  (S4. resolve N β S3 S4  (skip N β  factorize N β  resolve N β)** S4 S')"
        using maybe_reso step
        by (metis (no_types, opaque_lifting) rtranclp.rtrancl_into_rtrancl rtranclp.rtrancl_refl
            sup2I2)
    qed
  qed
qed

lemma backtrack_preserves_regular_conflict_resolution:
  assumes step: "backtrack N β S S'" and reg_step: "regular_scl N β S S'" and
    invar: "regular_conflict_resolution N β S"
  shows "regular_conflict_resolution N β S'"
proof -
  from step obtain C γ where
    "state_conflict S = Some (C, γ)" and "state_conflict S' = None"
    by (auto elim!: backtrack.cases)

  show ?thesis
    unfolding regular_conflict_resolution_def state_conflict S' = None
    unfolding option.case
  proof (rule impI)
    assume "{#} |∉| N"
    with invar obtain S0 S1 S2 S3 where
      reg_run: "(regular_scl N β)** initial_state S0" and
      propa: "propagate N β S0 S1" "regular_scl N β S0 S1" and
      confl: "conflict N β S1 S2" "regular_scl N β S1 S2" and
      facto: "(factorize N β)** S2 S3" "(regular_scl N β)** S2 S3" and
      maybe_reso: "S3 = S  (S4. resolve N β S3 S4  (skip N β  factorize N β  resolve N β)** S4 S)"
      unfolding regular_conflict_resolution_def state_conflict S = Some (C, γ)
      unfolding option.cases
      by metis

    from reg_run propa(2) confl(2) facto(2) have reg_run_S3: "(regular_scl N β)** initial_state S3"
      by simp

    show "(regular_scl N β)** initial_state S'"
      using maybe_reso
    proof (elim disjE exE conjE)
      show "S3 = S  (regular_scl N β)** initial_state S'"
        using reg_run_S3 reg_step by simp
    next
      fix S4 assume hyps: "resolve N β S3 S4" "(skip N β  factorize N β  resolve N β)** S4 S"
      have "(regular_scl N β)** initial_state S4"
        using reg_run_S3 regular_scl_if_resolve[OF hyps(1)]
        by (rule rtranclp.rtrancl_into_rtrancl)
      also have "(regular_scl N β)** S4 S"
        using hyps(2)
        by (rule mono_rtranclp[rule_format, rotated]) auto
      also have "(regular_scl N β)** S S'"
        using reg_step by simp
      finally show "(regular_scl N β)** initial_state S'"
        by assumption
    qed
  qed
qed

lemma regular_scl_preserves_regular_conflict_resolution:
  assumes reg_step: "regular_scl N β S S'" and
    invars: "regular_conflict_resolution N β S"
  shows "regular_conflict_resolution N β S'"
  using assms
  using propagate_preserves_regular_conflict_resolution decide_preserves_regular_conflict_resolution
    conflict_preserves_regular_conflict_resolution skip_preserves_regular_conflict_resolution
    factorize_preserves_regular_conflict_resolution resolve_preserves_regular_conflict_resolution
    backtrack_preserves_regular_conflict_resolution
  by (metis regular_scl_def reasonable_scl_def scl_def)

subsection ‹Miscellaneous Lemmas›

lemma mempty_not_in_initial_clauses_if_non_empty_regular_conflict:
  assumes "state_conflict S = Some (C, γ)" and "C  {#}" and
    invars: "almost_no_conflict_with_trail N β S" "sound_state N β S" "ground_false_closures S"
  shows "{#} |∉| N"
proof -
  from assms(1) obtain Γ U where S_def: "S = (Γ, U, Some (C, γ))"
    by (metis state_simp)

  from assms(2) obtain L C' where C_def: "C = add_mset L C'"
    using multi_nonempty_split by metis

  from invars(3) have "trail_false_cls Γ (C  γ)"
    by (simp add: S_def ground_false_closures_def)
  then obtain Ln Γ' where "Γ = Ln # Γ'"
    by (metis assms(2) neq_Nil_conv not_trail_false_Nil(2) subst_cls_empty_iff)
  with invars(1) have "no_conflict_with_trail N β U (if is_decision_lit Ln then Ln # Γ' else Γ')"
    by (simp add: S_def almost_no_conflict_with_trail_def)
  hence "S'. conflict N β ([], U, None) S'"
    by (rule nex_conflict_if_no_conflict_with_trail')
  hence "{#} |∉| N |∪| U"
    unfolding mempty_in_iff_ex_conflict[symmetric] by assumption
  thus ?thesis
    by simp
qed

lemma mempty_not_in_initial_clauses_if_regular_run_reaches_non_empty_conflict:
  assumes "(regular_scl N β)** initial_state S" and "state_conflict S = Some (C, γ)" and "C  {#}"
  shows "{#} |∉| N"
proof (rule notI)
  from assms(2) have "initial_state  S" by fastforce
  then obtain S' where
    reg_scl_init_S': "regular_scl N β initial_state S'" and "(regular_scl N β)** S' S"
    by (metis assms(1) converse_rtranclpE)

  assume "{#} |∈| N"
  hence "conflict N β initial_state ([], {||}, Some ({#}, Var))"
    by (rule conflict_initial_state_if_mempty_in_intial_clauses)
  hence conf_init: "regular_scl N β initial_state ([], {||}, Some ({#}, Var))"
    using regular_scl_def by blast
  then obtain γ where S'_def: "S' = ([], {||}, Some ({#}, γ))"
    using reg_scl_init_S'
    unfolding regular_scl_def
    using conflict N β initial_state ([], {||}, Some ({#}, Var))
      conflict_initial_state_only_with_mempty
    by blast

  have "S'. scl N β ([], {||}, Some ({#}, γ)) S'" for γ
    using no_more_step_if_conflict_mempty by simp
  hence "S'. regular_scl N β ([], {||}, Some ({#}, γ)) S'" for γ
    using scl_if_reasonable[OF reasonable_if_regular] by blast
  hence "S = S'"
    using (regular_scl N β)** S' S
    unfolding S'_def
    by (metis converse_rtranclpE)
  with assms(2,3) show False by (simp add: S'_def)
qed

lemma before_regular_backtrack:
  assumes
    backt: "backtrack N β S S'" and
    invars: "sound_state N β S" "almost_no_conflict_with_trail N β S"
      "regular_conflict_resolution N β S" "ground_false_closures S"
  shows "S0 S1 S2 S3 S4. (regular_scl N β)** initial_state S0 
    propagate N β S0 S1  regular_scl N β S0 S1 
    conflict N β S1 S2  (factorize N β)** S2 S3  resolve N β S3 S4 
    (skip N β  factorize N β  resolve N β)** S4 S"
proof -
  from backt obtain L C γ where conflict_S: "state_conflict S = Some (add_mset L C, γ)"
    by (auto elim: backtrack.cases)
  
  have "{#} |∉| N"
  proof (rule mempty_not_in_initial_clauses_if_non_empty_regular_conflict)
    show "state_conflict S = Some (add_mset L C, γ)"
      by (rule state_conflict S = Some (add_mset L C, γ))
  next
    show "add_mset L C  {#}"
      by simp
  next
    show "almost_no_conflict_with_trail N β S"
      by (rule almost_no_conflict_with_trail N β S)
  next
    show "sound_state N β S"
      by (rule sound_state N β S)
  next
    show "ground_false_closures S"
      by (rule ground_false_closures S)
  qed

  then obtain S0 S1 S2 S3 where
    reg_run: "(regular_scl N β)** initial_state S0" and
    propa: "propagate N β S0 S1" "regular_scl N β S0 S1" and
    confl: "conflict N β S1 S2" and
    fact: "(factorize N β)** S2 S3" and
    maybe_resolution: "S3 = S 
      (S4. resolve N β S3 S4  (skip N β  factorize N β  resolve N β)** S4 S)"
    using regular_conflict_resolution N β S state_conflict S = Some (add_mset L C, γ)
    unfolding regular_conflict_resolution_def conflict_S option.case
    by metis

  have "S3  S"
  proof (rule notI)
    from (factorize N β)** S2 S3 have "state_trail S3 = state_trail S2"
      by (induction S3 rule: rtranclp_induct) (auto elim: factorize.cases)
    also from conflict N β S1 S2 have " = state_trail S1"
      by (auto elim: conflict.cases)
    finally have "state_trail S3 = state_trail S1"
      by assumption
    from propagate N β S0 S1 obtain L C γ where
      "state_trail S1 = trail_propagate (state_trail S0) L C γ"
      by (auto elim: propagate.cases)

    from (factorize N β)** S2 S3 have "state_learned S3 = state_learned S2"
    proof (induction S3 rule: rtranclp_induct)
      case base
      show ?case by simp
    next
      case (step y z)
      thus ?case
        by (elim factorize.cases) simp
    qed
    also from conflict N β S1 S2 have " = state_learned S1"
      by (auto elim: conflict.cases)
    finally have "state_learned S3 = state_learned S1"
      by assumption

    from propagate N β S0 S1 have "state_learned S1 = state_learned S0"
      by (auto elim: propagate.cases)

    assume "S3 = S"
    hence no_conf_with_trail: "no_conflict_with_trail N β (state_learned S0) (state_trail S0)"
      using almost_no_conflict_with_trail N β S {#} |∉| N
        state_trail S1 = trail_propagate (state_trail S0) L C γ state_trail S3 = state_trail S1
        state_learned S3 = state_learned S1 state_learned S1 = state_learned S0
      by (simp add: almost_no_conflict_with_trail_def propagate_lit_def is_decision_lit_def)
    hence "{#} |∉| state_learned S0"
      using nex_conflict_if_no_conflict_with_trail'[folded mempty_in_iff_ex_conflict] by simp

    have "D γD. state_conflict S2 = Some (D, γD)  - (L ⋅l γ) ∈# D  γD"
      using conflict N β S1 S2
    proof (cases N β S1 S2 rule: conflict.cases)
      case (conflictI D U γD Γ)
      hence "trail_false_cls (trail_propagate (state_trail S0) L C γ) (D  γD)"
        using state_trail S1 = trail_propagate (state_trail S0) L C γ
        by simp

      moreover from no_conf_with_trail have "¬ trail_false_cls (state_trail S0) (D  γD)"
      proof (rule not_trail_false_cls_if_no_conflict_with_trail)
        show "D |∈| N |∪| state_learned S0"
          using state_learned S1 = state_learned S0 local.conflictI(1) local.conflictI(3)
          by fastforce
      next
        have "{#} |∉| U"
          using {#} |∉| state_learned S0 S3 = S state_learned S3 = state_learned S1
            state_learned S1 = state_learned S0
          unfolding conflictI(1,2)
          by simp
        thus "D  {#}"
          using {#} |∉| N D |∈| N |∪| U
          by auto
      next
        show "is_ground_cls (D  γD)"
          by (rule is_ground_cls (D  γD))
      qed

      ultimately have "- (L ⋅l γ) ∈# D  γD"
        by (metis subtrail_falseI propagate_lit_def)

      moreover have "state_conflict S2 = Some (D, γD)"
        unfolding conflictI(1,2) by simp

      ultimately show ?thesis
        by metis
    qed
    then obtain D γD where "state_conflict S2 = Some (D, γD)" and "- (L ⋅l γ) ∈# D  γD"
      by metis
    with (factorize N β)** S2 S3
    have "D' γD'. state_conflict S3 = Some (D', γD')  - (L ⋅l γ) ∈# D'  γD'"
    proof (induction S3 arbitrary: rule: rtranclp_induct)
      case base
      thus ?case by simp
    next
      case (step y z)
      then obtain D' γD' where "state_conflict y = Some (D', γD')" and "- (L ⋅l γ) ∈# D'  γD'"
        by auto
      then show ?case
        using step.hyps(2)
        by (metis conflict_set_after_factorization)
    qed
    with backt S3 = S show False
      using state_trail S3 = state_trail S1
      unfolding S3 = S state_trail S1 = trail_propagate (state_trail S0) L C γ
      by (auto simp add: decide_lit_def propagate_lit_def elim!: backtrack.cases)
  qed
  with maybe_resolution obtain S4 where
    "resolve N β S3 S4" and "(skip N β  factorize N β  resolve N β)** S4 S"
    by metis
  show ?thesis
  proof (intro exI conjI)
    show "(regular_scl N β)** initial_state S0"
      by (rule (regular_scl N β)** initial_state S0)
  next
    show "propagate N β S0 S1"
      by (rule propagate N β S0 S1)
  next
    show "regular_scl N β S0 S1"
      by (rule propa(2))
  next
    show "conflict N β S1 S2"
      by (rule conflict N β S1 S2)
  next
    show "(factorize N β)** S2 S3"
      by (rule (factorize N β)** S2 S3)
  next
    show "resolve N β S3 S4"
      by (rule resolve N β S3 S4)
  next
    show "(skip N β  factorize N β  resolve N β)** S4 S"
      by (rule (skip N β  factorize N β  resolve N β)** S4 S)
  qed
qed


section ‹Resolve in Regular Runs›

lemma resolve_if_conflict_follows_propagate:
  assumes
    no_conf: "S1. conflict N β S0 S1" and
    propa: "propagate N β S0 S1" and
    conf: "conflict N β S1 S2"
  shows "S3. resolve N β S2 S3"
  using propa
proof (cases N β S0 S1 rule: propagate.cases)
  case (propagateI C U L C' γ C0 C1 Γ μ)
  hence S0_def: "S0 = (Γ, U, None)"
    by simp

  from conf obtain γD D where
    S2_def: "S2 = (trail_propagate Γ (L ⋅l μ) (C0  μ) γ, U, Some (D, γD))" and
    D_in: "D |∈| N |∪| U" and
    gr_D_γD: "is_ground_cls (D  γD)" and
    tr_false_Γ_L_μ: "trail_false_cls (trail_propagate Γ (L ⋅l μ) (C0  μ) γ) (D  γD)"
    by (elim conflict.cases) (unfold propagateI(1,2), blast)

  from no_conf have "¬ trail_false_cls Γ (D  γD)"
    using gr_D_γD D_in not_trail_false_ground_cls_if_no_conflict[of N β _ D γD]
    using S0_def by force
  with tr_false_Γ_L_μ have "- (L ⋅l μ ⋅l γ) ∈# D  γD"
    unfolding propagate_lit_def by (metis subtrail_falseI)
  then obtain D' L' where D_def: "D = add_mset L' D'" and 1: "L ⋅l μ ⋅l γ = - (L' ⋅l γD)"
    by (metis Melem_subst_cls multi_member_split uminus_of_uminus_id)

  define ρ where
    "ρ = renaming_wrt {add_mset L C0  μ}"

  have "is_renaming ρ"
    by (metis ρ_def finite.emptyI finite.insertI is_renaming_renaming_wrt)
  hence "x. is_Var (ρ x)" and "inj ρ"
    by (simp_all add: is_renaming_iff)

  have disjoint_vars: "C. vars_cls (C  ρ)  vars_cls (add_mset L C0  μ) = {}"
    by (simp add: ρ_def vars_cls_subst_renaming_disj)

  have "μ'. Unification.mgu (atm_of L' ⋅a ρ) (atm_of L ⋅a μ) = Some μ'"
  proof (rule ex_mgu_if_subst_eq_subst_and_disj_vars)
    have "vars_lit L'  subst_domain γD"
      using gr_D_γD[unfolded D_def]
      by (simp add: vars_lit_subset_subst_domain_if_grounding is_ground_cls_imp_is_ground_lit)
    hence "atm_of L' ⋅a ρ ⋅a rename_subst_domain ρ γD = atm_of L' ⋅a γD"
      by (rule renaming_cancels_rename_subst_domain[OF x. is_Var (ρ x) inj ρ])
    then show "atm_of L' ⋅a ρ ⋅a rename_subst_domain ρ γD = atm_of L ⋅a μ ⋅a γ"
      using 1 by (metis atm_of_subst_lit atm_of_uminus)
  next
    show "vars_term (atm_of L' ⋅a ρ)  vars_term (atm_of L ⋅a μ) = {}"
      using disjoint_vars[of "{#L'#}"] by auto
  qed
  then obtain μ' where imgu_μ': "is_imgu μ' {{atm_of L' ⋅a ρ, atm_of (L ⋅l μ)}}"
    using is_imgu_if_mgu_eq_Some by auto

  let ?Γprop = "trail_propagate Γ (L ⋅l μ) (C0  μ) γ"
  let ?γreso = "λx. if x  vars_cls (add_mset L' D'  ρ) then rename_subst_domain ρ γD x else γ x"

  have "resolve N β
    (?Γprop, U, Some (add_mset L' D', γD))
    (?Γprop, U, Some ((D'  ρ + C0  μ  Var)  μ', ?γreso))"
  proof (rule resolveI[OF refl])
    show "L ⋅l μ ⋅l γ = - (L' ⋅l γD)"
      by (rule 1)
  next
    show "is_renaming ρ"
      by (metis ρ_def finite.emptyI finite.insertI is_renaming_renaming_wrt)
  next
    show "vars_cls (add_mset L' D'  ρ)  vars_cls (add_mset (L ⋅l μ) (C0  μ)  Var) = {}"
      using disjoint_vars[of "add_mset L' D'"] by simp
  next
    show "is_imgu μ' {{atm_of L' ⋅a ρ, atm_of (L ⋅l μ) ⋅a Var}}"
      using imgu_μ' by simp
  next
    show "is_grounding_merge ?γreso
     (vars_cls (add_mset L' D'  ρ)) (rename_subst_domain ρ γD)
     (vars_cls (add_mset (L ⋅l μ) (C0  μ)  Var)) (rename_subst_domain Var γ)"
      using is_grounding_merge_if_mem_then_else
      by (metis rename_subst_domain_Var_lhs)
  qed simp_all
  thus ?thesis
    unfolding S2_def D_def by metis
qed

lemma factorize_preserves_resolvability:
  assumes reso: "resolve N β S1 S2" and fact: "factorize N β S1 S3" and
    invar: "ground_closures S1"
  shows "S4. resolve N β S3 S4"
  using reso
proof (cases N β S1 S2 rule: resolve.cases)
  case (resolveI Γ Γ' K D γD L γC ρC ρD C μ γ U)

  from fact[unfolded resolveI(1,2)] obtain LL' LL CC μL where
    S1_def: "S1 = (Γ, U, Some (add_mset LL' (add_mset LL CC), γC))" and
    S3_def: "S3 = (Γ, U, Some (add_mset LL CC  μL, γC))" and
    "LL ⋅l γC = LL' ⋅l γC" and
    imgu_μL: "is_imgu μL {{atm_of LL, atm_of LL'}}"
    by (auto simp: S1 = (Γ, U, Some (add_mset L C, γC)) elim: factorize.cases)

  from invar have
    ground_conf: "is_ground_cls (add_mset L C  γC)"
    unfolding resolveI(1,2)
    by (simp_all add: ground_closures_def)

  have "add_mset L C = add_mset LL' (add_mset LL CC)"
    using resolveI(1) S1_def by simp

  from imgu_μL have "μL  γC = γC"
    using LL ⋅l γC = LL' ⋅l γC
    by (auto simp: is_imgu_def is_unifiers_def is_unifier_alt intro!: subst_atm_of_eqI)

  have "L ⋅l μL ∈# add_mset LL CC  μL"
  proof (cases "L = LL  L = LL'")
    case True
    moreover have "LL ⋅l μL = LL' ⋅l μL"
      using imgu_μL[unfolded is_imgu_def, THEN conjunct1, unfolded is_unifiers_def, simplified]
      using LL ⋅l γC = LL' ⋅l γC
      by (metis (no_types, opaque_lifting) atm_of_subst_lit finite.emptyI finite.insertI insertCI
          is_unifier_alt literal.expand subst_lit_is_neg)
    ultimately have "L ⋅l μL = LL ⋅l μL"
      by presburger
    thus ?thesis
      by simp
  next
    case False
    hence "L ∈# CC"
      using add_mset L C = add_mset LL' (add_mset LL CC)
      by (metis insert_iff set_mset_add_mset_insert)
    thus ?thesis
      by auto
  qed
  then obtain CCC where "add_mset LL CC  μL = add_mset L CCC  μL"
    by (smt (verit, best) Melem_subst_cls mset_add subst_cls_add_mset)

  define ρρ where
    "ρρ = renaming_wrt {add_mset K D}"

  have ren_ρρ: "is_renaming ρρ"
    by (metis ρρ_def finite.emptyI finite.insertI is_renaming_renaming_wrt)

  have disjoint_vars: "C. vars_cls (C  ρρ)  vars_cls (add_mset K D) = {}"
    by (simp add: ρρ_def vars_cls_subst_renaming_disj)

  have "K ⋅l γD = - (L ⋅l μL ⋅l γC)"
  proof -
    have "L ⋅l μL ⋅l γC = L ⋅l γC"
      using μL  γC = γC
      by (metis subst_lit_comp_subst)
    thus ?thesis
      using resolveI by simp
  qed

  have "μ. Unification.mgu (atm_of L ⋅a μL ⋅a ρρ) (atm_of K) = Some μ"
  proof (rule ex_mgu_if_subst_eq_subst_and_disj_vars)
    show "vars_term (atm_of L ⋅a μL ⋅a ρρ)  vars_lit K = {}"
      using disjoint_vars[of "{#L ⋅l μL#}"] by auto
  next
    have "vars_term (atm_of L ⋅a μL)  subst_domain γC"
      by (metis μL  γC = γC atm_of_subst_lit ground_conf is_ground_cls_add_mset
          subst_cls_add_mset subst_lit_comp_subst vars_lit_subset_subst_domain_if_grounding)
    hence "atm_of L ⋅a μL ⋅a ρρ ⋅a rename_subst_domain ρρ γC = atm_of L ⋅a μL ⋅a γC"
      using ren_ρρ
      by (simp add: is_renaming_iff renaming_cancels_rename_subst_domain)
    thus "atm_of L ⋅a μL ⋅a ρρ ⋅a rename_subst_domain ρρ γC = atm_of K ⋅a γD"
      using K ⋅l γD = - (L ⋅l μL ⋅l γC)
      by (metis atm_of_subst_lit atm_of_uminus)
  qed
  then obtain μμ where imgu_μμ: "is_imgu μμ {{atm_of L ⋅a μL ⋅a ρρ, atm_of K}}"
    using is_imgu_if_mgu_eq_Some by auto

  show ?thesis
    unfolding S3_def add_mset LL CC  μL = add_mset L CCC  μL
    using resolve.resolveI[OF Γ = trail_propagate Γ' K D γD K ⋅l γD = - (L ⋅l μL ⋅l γC) ren_ρρ
        is_renaming_id_subst, unfolded subst_atm_id_subst subst_cls_id_subst atm_of_subst_lit,
        OF disjoint_vars imgu_μμ is_grounding_merge_if_mem_then_else, of N β U  "CCC  μL"]
    by auto
qed

text ‹The following lemma corresponds to Lemma 7 in the paper.›

lemma no_backtrack_after_conflict_if:
  assumes conf: "conflict N β S1 S2" and trail_S2: "state_trail S1 = trail_propagate Γ L C γ"
  shows "S4. backtrack N β S2 S4"
proof -
  from trail_S2 conf have "state_trail S2 = trail_propagate Γ L C γ"
    unfolding conflict.simps by auto
  then show ?thesis
    unfolding backtrack.simps propagate_lit_def decide_lit_def
    by auto
qed

lemma skip_state_trail: "skip N β S S'  suffix (state_trail S') (state_trail S)"
  by (auto simp: suffix_def elim: skip.cases)

lemma factorize_state_trail: "factorize N β S S'  state_trail S' = state_trail S"
  by (auto elim: factorize.cases)

lemma resolve_state_trail: "resolve N β S S'  state_trail S' = state_trail S"
  by (auto elim: resolve.cases)

lemma mempty_not_in_initial_clauses_if_run_leads_to_trail:
  assumes
    reg_run: "(regular_scl N β)** initial_state S1" and
    trail_lit: "state_trail S1 = Lc # Γ"
  shows "{#} |∉| N"
proof (rule notI)
  assume "{#} |∈| N"
  then obtain γ where "conflict N β initial_state ([], {||}, Some ({#}, γ))"
    using conflict_initial_state_if_mempty_in_intial_clauses by auto
  moreover hence "S'. local.scl N β ([], {||}, Some ({#}, γ)) S'" for γ
    using no_more_step_if_conflict_mempty by simp
  ultimately show False
    using trail_lit
    by (metis (no_types, opaque_lifting) conflict_initial_state_only_with_mempty converse_rtranclpE
        list.discI prod.sel(1) reasonable_if_regular reg_run regular_scl_def scl_if_reasonable
        state_trail_def)
qed

(*
after conflict, one can apply factorize arbitrarily often,
but resolve must be applied at least once.

Prove this lemma!
conflict in reg run ⟹ ALL following runs have the following shape:
  factorize* then resolve then (skip or factorize or resolve)*
*)

lemma conflict_with_literal_gets_resolved:
  assumes
    trail_lit: "state_trail S1 = Lc # Γ" and
    conf: "conflict N β S1 S2" and
    resolution: "(skip N β  factorize N β  resolve N β)** S2 Sn" and
    backtrack: "Sn'. backtrack N β Sn Sn'" and
    mempty_not_in_init_clss: "{#} |∉| N" and
    invars: "learned_nonempty S1" "trail_propagated_or_decided' N β S1" "no_conflict_after_decide' N β S1"
  shows "¬ is_decision_lit Lc  strict_suffix (state_trail Sn) (state_trail S1)"
proof -
  obtain S0 where propa: "propagate N β S0 S1"
    using mempty_not_in_init_clss before_reasonable_conflict[OF conf learned_nonempty S1
        trail_propagated_or_decided' N β S1 no_conflict_after_decide' N β S1] by metis

  from trail_lit propa have "¬ is_decision_lit Lc"
    by (auto simp: propagate_lit_def is_decision_lit_def elim!: propagate.cases)

  show ?thesis
  proof (rule conjI)
    show "¬ is_decision_lit Lc"
      by (rule ¬ is_decision_lit Lc)
  next
    show "strict_suffix (state_trail Sn) (state_trail S1)"
      unfolding strict_suffix_def
    proof (rule conjI)
      from conf have "state_trail S2 = state_trail S1"
        by (auto elim: conflict.cases)
      moreover from resolution have "suffix (state_trail Sn) (state_trail S2)"
      proof (induction Sn rule: rtranclp_induct)
        case base
        thus ?case
          by simp
      next
        case (step y z)
        from step.hyps(2) have "suffix (state_trail z) (state_trail y)"
          by (auto simp: suffix_def factorize_state_trail resolve_state_trail
              dest: skip_state_trail)
        with step.IH show ?case
          by (auto simp: suffix_def)
      qed
      ultimately show "suffix (state_trail Sn) (state_trail S1)"
        by simp
    next
      from backtrack ¬ is_decision_lit Lc show "state_trail Sn  state_trail S1"
        unfolding trail_lit
        by (auto simp: decide_lit_def is_decision_lit_def elim!: backtrack.cases)
    qed
  qed
qed


section ‹Clause Redundancy›

definition ground_redundant where
  "ground_redundant lt N C  {D  N. lt D C} ⊫e {C}"

definition redundant where
  "redundant lt N C 
    (C'  grounding_of_cls C. ground_redundant lt (grounding_of_clss N) C')"

lemma "redundant lt N C  (C' grounding_of_cls C. {D'  grounding_of_clss N. lt D' C'} ⊫e {C'})"
  by (simp add: redundant_def ground_redundant_def)

lemma ground_redundant_iff:
  "ground_redundant lt N C  (M  N. M ⊫e {C}  (D  M. lt D C))"
proof (rule iffI)
  assume red: "ground_redundant lt N C"
  show "MN. M ⊫e {C}  (DM. lt D C)"
  proof (intro exI conjI)
    show "{D  N. lt D C}  N"
      by simp
  next
    show "{D  N. lt D C} ⊫e {C}"
      using red by (simp add: ground_redundant_def)
  next
    show "D{D  N. lt D C}. lt D C"
      by simp
  qed
next
  assume "MN. M ⊫e {C}  (DM. lt D C)"
  then show "ground_redundant lt N C"
    unfolding ground_redundant_def
    by (smt (verit, ccfv_SIG) mem_Collect_eq subset_iff true_clss_mono)
qed

lemma ground_redundant_is_ground_standard_redundancy:
  fixes lt
  defines "Red_F𝒢  λN. {C. ground_redundant lt N C}"
  shows "Red_F𝒢 N = {C. M  N. M ⊫e {C}  (D  M. lt D C)}"
  by (auto simp: Red_F𝒢_def ground_redundant_iff)

lemma redundant_is_standard_redundancy:
  fixes lt 𝒢F 𝒢Fs Red_F𝒢 Red_F
  defines
    "𝒢F  grounding_of_cls" and
    "𝒢Fs  grounding_of_clss" and
    "Red_F𝒢  λN. {C. ground_redundant lt N C}" and
    "Red_F  λN. {C. redundant lt N C}"
  shows "Red_F N = {C. D  𝒢F C. D  Red_F𝒢 (𝒢Fs N)}"
  using Red_F_def Red_F𝒢_def 𝒢Fs_def 𝒢F_def redundant_def by auto

lemma ground_redundant_if_strict_subset:
  assumes "D  N" and "D ⊂# C"
  shows "ground_redundant (multpHO R) N C"
  using assms
  unfolding ground_redundant_def
  by (metis (mono_tags, lifting) CollectI strict_subset_implies_multpHO subset_mset.less_le
      true_clss_def true_clss_singleton true_clss_subclause)

lemma redundant_if_strict_subset:
  assumes "D  N" and "D ⊂# C"
  shows "redundant (multpHO R) N C"
  unfolding redundant_def
proof (rule ballI)
  fix C' assume "C'  grounding_of_cls C"
  then obtain γ where "C' = C  γ" and "is_ground_subst γ"
    by (auto simp: grounding_of_cls_def)

  show "ground_redundant (multpHO R) (grounding_of_clss N) C'"
  proof (rule ground_redundant_if_strict_subset)
    from D  N show "D  γ  grounding_of_clss N"
      using is_ground_subst γ
      by (auto simp: grounding_of_clss_def grounding_of_cls_def)
  next
    from D ⊂# C show "D  γ ⊂# C'"
      by (simp add: C' = C  γ subst_subset_mono)
  qed
qed

lemma redundant_if_strict_subsumes:
  assumes "D  σ ⊂# C" and "D  N"
  shows "redundant (multpHO R) N C"
  unfolding redundant_def
proof (rule ballI)
  fix C' assume "C'  grounding_of_cls C"
  then obtain γ where "C' = C  γ" and "is_ground_subst γ"
    by (auto simp: grounding_of_cls_def)

  show "ground_redundant (multpHO R) (grounding_of_clss N) C'"
  proof (rule ground_redundant_if_strict_subset)
    from D  N show "D  σ  γ  grounding_of_clss N"
      using is_ground_subst γ
      by (metis (no_types, lifting) UN_iff ground_subst_ground_cls grounding_of_cls_ground
          grounding_of_clss_def insert_subset subst_cls_comp_subst
          subst_cls_eq_grounding_of_cls_subset_eq)
  next
    from D  σ ⊂# C show "D  σ  γ ⊂# C'"
      by (simp add: C' = C  γ subst_subset_mono)
  qed
qed

lemma ground_redundant_mono_strong:
  "ground_redundant R N C  (x. x  N  R x C  S x C)  ground_redundant S N C"
  unfolding ground_redundant_def
  by (simp add: true_clss_def)

lemma redundant_mono_strong:
  "redundant R N C 
    (x y. x  grounding_of_clss N  y  grounding_of_cls C  R x y  S x y) 
  redundant S N C"
  by (auto simp: redundant_def
      intro: ground_redundant_mono_strong[of R "grounding_of_clss N" _ S])

lemma redundant_multp_if_redundant_strict_subset:
  "redundant (⊂#) N C  redundant (multpHO R) N C"
  by (auto intro: strict_subset_implies_multpHO elim!: redundant_mono_strong)

lemma redundant_multp_if_redundant_subset:
  "redundant (⊂#) N C  redundant (multp (trail_less_ex lt Ls)) N C"
  by (auto intro: subset_implies_multp elim!: redundant_mono_strong)

lemma not_bex_subset_mset_if_not_ground_redundant:
  assumes "is_ground_cls C" and "is_ground_clss N"
  shows "¬ ground_redundant (⊂#) N C  ¬ (D  N. D ⊂# C)"
  using assms unfolding ground_redundant_def
  apply (simp add: true_cls_def true_clss_def)
  apply (elim exE conjE)
  apply (rule ballI)
  subgoal premises prems for I D
    using prems(3)[rule_format, of D] prems(1,2,4-)
    apply simp
    by (meson mset_subset_eqD subset_mset.nless_le)
  done


section ‹Trail-Induced Ordering›

subsection ‹Miscellaneous Lemmas›

lemma pairwise_distinct_if_trail_consistent:
  fixes Γ
  defines "Ls  (map fst Γ)"
  shows "trail_consistent Γ 
    i < length Ls. j < length Ls. i  j  Ls ! i  Ls ! j  Ls ! i  - (Ls ! j)"
  unfolding Ls_def
proof (induction Γ rule: trail_consistent.induct)
  case Nil
  show ?case by simp
next
  case (Cons Γ L u)
  from Cons.hyps have L_distinct:
    "x < length (map fst Γ). map fst Γ ! x  L"
    "x < length (map fst Γ). map fst Γ ! x  - L"
    unfolding trail_defined_lit_def de_Morgan_disj
    unfolding image_set in_set_conv_nth not_ex de_Morgan_conj disj_not1
    by simp_all
  show ?case
    unfolding list.map prod.sel
  proof (intro allI impI)
    fix i j :: nat
    assume i_lt: "i < length (L # map fst Γ)" and j_lt: "j < length (L # map fst Γ)" and "i  j"
    show
      "(L # map fst Γ) ! i  (L # map fst Γ) ! j 
       (L # map fst Γ) ! i  - (L # map fst Γ) ! j"
    proof (cases i)
      case 0
      thus ?thesis
        using L_distinct i  j j < length (L # map fst Γ)
        using gr0_conv_Suc by auto
    next
      case (Suc k)
      then show ?thesis
        apply simp
        using i_lt j_lt i  j L_distinct Cons.IH[rule_format]
        using less_Suc_eq_0_disj by force
    qed
  qed
qed


subsection ‹Strict Partial Order›

lemma irreflp_trail_less_if_trail_consistant:
  "trail_consistent Γ  irreflp (trail_less (map fst Γ))"
  using irreflp_trail_less[OF
      Clausal_Logic.uminus_not_id'
      Clausal_Logic.uminus_of_uminus_id
      pairwise_distinct_if_trail_consistent]
  by assumption

lemma transp_trail_less_if_trail_consistant:
  "trail_consistent Γ  transp (trail_less (map fst Γ))"
  using transp_trail_less[OF
      Clausal_Logic.uminus_not_id'
      Clausal_Logic.uminus_of_uminus_id
      pairwise_distinct_if_trail_consistent]
  by assumption

lemma asymp_trail_less_if_trail_consistant:
  "trail_consistent Γ  asymp (trail_less (map fst Γ))"
  using asymp_trail_less[OF
      Clausal_Logic.uminus_not_id'
      Clausal_Logic.uminus_of_uminus_id
      pairwise_distinct_if_trail_consistent]
  by assumption


subsection ‹Properties›

lemma trail_defined_lit_if_trail_term_less:
  assumes "trail_term_less (map (atm_of o fst) Γ) (atm_of L) (atm_of K)"
  shows "trail_defined_lit Γ L" "trail_defined_lit Γ K"
proof -
  from assms have "atm_of L  set (map (atm_of o fst) Γ)" and "atm_of K  set (map (atm_of o fst) Γ)"
    by (auto simp: trail_term_less_def)
  hence "atm_of L  atm_of ` fst ` set Γ" and "atm_of K  atm_of ` fst ` set Γ"
    by auto
  hence "L  fst ` set Γ  - L  fst ` set Γ" and "K  fst ` set Γ  - K  fst ` set Γ"
    by (simp_all add: atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set)
  thus "trail_defined_lit Γ L" and "trail_defined_lit Γ K"
    by (simp_all add: trail_defined_lit_def)
qed

lemma trail_defined_cls_if_lt_defined:
  assumes consistent_Γ: "trail_consistent Γ" and
    C_lt_D: "multpHO (lit_less (trail_term_less (map (atm_of o fst) Γ))) C D" and
    tr_def_D: "trail_defined_cls Γ D" and
    lit_less_preserves_term_order: "R L1 L2. lit_less R L1 L2  R== (atm_of L1) (atm_of L2)"
  shows "trail_defined_cls Γ C"
proof -
  from multpHO_implies_one_step[OF C_lt_D]
  obtain I J K where D_def: "D = I + J" and C_def: "C = I + K" and "J  {#}" and
    *: "k∈#K. x∈#J. lit_less (trail_term_less (map (atm_of o fst) Γ)) k x"
    by auto

  show ?thesis
    unfolding trail_defined_cls_def
  proof (rule ballI)
    fix L assume L_in: "L ∈# C"
    show "trail_defined_lit Γ L"
    proof (cases "L ∈# I")
      case True
      then show ?thesis
        using tr_def_D D_def
        by (simp add: trail_defined_cls_def)
    next
      case False
      with C_def L_in have "L ∈# K" by fastforce
      then obtain L' where L'_in: "L'∈#J" and "lit_less (trail_term_less (map (atm_of o fst) Γ)) L L'"
        using * by blast
      hence "(trail_term_less (map (atm_of o fst) Γ))== (atm_of L) (atm_of L')"
        using lit_less_preserves_term_order by metis
      thus ?thesis
        using trail_defined_lit_if_trail_term_less(1)
        by (metis (mono_tags, lifting) D_def L'_in atm_of_eq_atm_of sup2E tr_def_D
            trail_defined_cls_def trail_defined_lit_iff_defined_uminus union_iff)
    qed
  qed
qed


section ‹Dynamic Non-Redundancy›

lemma regular_run_if_skip_factorize_resolve_run:
  assumes "(skip N β  factorize N β  resolve N β)** S S'"
  shows "(regular_scl N β)** S S'"
  using assms
proof (induction S' rule: rtranclp_induct)
  case base
  show ?case by simp
next
  case (step S' S'')
  from step.hyps(2) have "scl N β S' S''"
    unfolding scl_def by blast
  with step.hyps(2) have "reasonable_scl N β S' S''"
    using reasonable_scl_def decide_well_defined(4) decide_well_defined(5) skip_well_defined(2)
    by fast
  moreover from step.hyps(2) have "¬ Ex (conflict N β S')"
    apply simp
    by (smt (verit, best) conflict.cases factorize.simps option.distinct(1) resolve.simps skip.simps
        state_conflict_simp)
  ultimately have "regular_scl N β S' S''"
    by (simp add: regular_scl_def)
  with step.IH show ?case
    by simp
qed

lemma not_trail_true_and_false_lit:
  "trail_consistent Γ  ¬ (trail_true_lit Γ L  trail_false_lit Γ L)"
  apply (simp add: trail_true_lit_def trail_false_lit_def)
  by (metis (no_types, lifting) in_set_conv_nth list.set_map pairwise_distinct_if_trail_consistent
      uminus_not_id')

lemma not_trail_true_and_false_cls:
  "trail_consistent Γ  ¬ (trail_true_cls Γ C  trail_false_cls Γ C)"
  using not_trail_true_and_false_lit
  by (metis trail_false_cls_def trail_true_cls_def)

fun standard_lit_less where
  "standard_lit_less R (Pos t1) (Pos t2) = R t1 t2" |
  "standard_lit_less R (Pos t1) (Neg t2) = R== t1 t2" |
  "standard_lit_less R (Neg t1) (Pos t2) = R t1 t2" |
  "standard_lit_less R (Neg t1) (Neg t2) = R t1 t2"

lemma