Theory CDCL_W_Termination

theory CDCL_W_Termination
imports CDCL_W
begin

context conflict_driven_clause_learning⇩W
begin

subsection ‹Termination›

subsubsection ‹No Relearning of a clause›

text ‹
  Because of the conflict minimisation, this version is less clear than the version without:
  instead of extracting the clause from the conflicting clause, we must take it from the clause
  used to backjump; i.e., the annotation of the first literal of the trail.

  We also prove below that no learned clause is subsumed by a (smaller) clause in the clause set.
›
lemma cdcl⇩W_stgy_no_relearned_clause:
  assumes
    cdcl: ‹backtrack S T› and
    inv: ‹cdcl⇩W_all_struct_inv S› and
    smaller: ‹no_smaller_propa S›
  shows
    ‹mark_of (hd_trail T) ∉# clauses S›
proof (rule ccontr)
  assume n_dist: ‹¬ ?thesis›
  obtain K L :: "'v literal" and
    M1 M2 :: "('v, 'v clause) ann_lit list" and i :: nat and D D' where
    confl_S: "conflicting S = Some (add_mset L D)" and
    decomp: "(Decided K # M1, M2) ∈ set (get_all_ann_decomposition (trail S))" and
    lev_L: "get_level (trail S) L = backtrack_lvl S" and
    max_D_L: "get_level (trail S) L = get_maximum_level (trail S) (add_mset L D')" and
    i: "get_maximum_level (trail S) D' ≡ i" and
    lev_K: "get_level (trail S) K = i + 1" and
    T: "T ∼ cons_trail (Propagated L (add_mset L D'))
        (reduce_trail_to M1
          (add_learned_cls (add_mset L D')
            (update_conflicting None S)))" and
    D_D': ‹D' ⊆# D› and
    ‹clauses S ⊨pm add_mset L D'›
    using cdcl by (auto elim!: rulesE)

  obtain M2' where M2': ‹trail S = (M2' @ M2) @ Decided K # M1›
    using decomp by auto
  have inv_T: ‹cdcl⇩W_all_struct_inv T›
    using cdcl cdcl⇩W_stgy_cdcl⇩W_all_struct_inv inv W_other backtrack bj
      cdcl⇩W_all_struct_inv_inv cdcl⇩W_cdcl⇩W_restart by blast

  have M1_D': ‹M1 ⊨as CNot D'›
    using backtrack_M1_CNot_D'[of S D' ‹i› K M1 M2 L ‹add_mset L D› T
        ‹Propagated L (add_mset L D')›] inv confl_S decomp i T D_D' lev_K lev_L max_D_L
    unfolding cdcl⇩W_all_struct_inv_def cdcl⇩W_conflicting_def cdcl⇩W_M_level_inv_def
    by (auto simp: subset_mset_trans_add_mset)
  have ‹undefined_lit M1 L›
    using inv_T T decomp unfolding cdcl⇩W_all_struct_inv_def cdcl⇩W_M_level_inv_def
    by (auto simp: defined_lit_map)
  moreover have ‹D' + {#L#} ∈# clauses S›
    using n_dist T by (auto simp: clauses_def)
  ultimately show False
    using smaller M1_D' unfolding no_smaller_propa_def M2' by blast
qed

lemma cdcl⇩W_stgy_no_relearned_larger_clause:
  assumes
    cdcl: ‹backtrack S T› and
    inv: ‹cdcl⇩W_all_struct_inv S› and
    smaller: ‹no_smaller_propa S› and
    smaller_conf: ‹no_smaller_confl S› and
    E_subset: ‹E ⊂# mark_of (hd_trail T)›
  shows ‹E ∉# clauses S›
proof (rule ccontr)
  assume n_dist: ‹¬ ?thesis›
  obtain K L :: "'v literal" and
    M1 M2 :: "('v, 'v clause) ann_lit list" and i :: nat and D D' where
    confl_S: "conflicting S = Some (add_mset L D)" and
    decomp: "(Decided K # M1, M2) ∈ set (get_all_ann_decomposition (trail S))" and
    lev_L: "get_level (trail S) L = backtrack_lvl S" and
    max_D_L: "get_level (trail S) L = get_maximum_level (trail S) (add_mset L D')" and
    i: "get_maximum_level (trail S) D' ≡ i" and
    lev_K: "get_level (trail S) K = i + 1" and
    T: "T ∼ cons_trail (Propagated L (add_mset L D'))
        (reduce_trail_to M1
          (add_learned_cls (add_mset L D')
            (update_conflicting None S)))" and
    D_D': ‹D' ⊆# D› and
    ‹clauses S ⊨pm add_mset L D'›
    using cdcl by (auto elim!: rulesE)

  obtain M2' where M2': ‹trail S = (M2' @ M2) @ Decided K # M1›
    using decomp by auto
  have inv_T: ‹cdcl⇩W_all_struct_inv T›
    using cdcl cdcl⇩W_stgy_cdcl⇩W_all_struct_inv inv W_other backtrack bj
      cdcl⇩W_all_struct_inv_inv cdcl⇩W_cdcl⇩W_restart by blast
  have ‹distinct_mset (add_mset L D')›
    using inv_T T unfolding cdcl⇩W_all_struct_inv_def distinct_cdcl⇩W_state_def
    by auto
  then have dist_E: ‹distinct_mset E›
    using distinct_mset_mono_strict[OF E_subset] T by auto

  have M1_D': ‹M1 ⊨as CNot D'›
    using backtrack_M1_CNot_D'[of S D' ‹i› K M1 M2 L ‹add_mset L D› T
        ‹Propagated L (add_mset L D')›] inv confl_S decomp i T D_D' lev_K lev_L max_D_L
    unfolding cdcl⇩W_all_struct_inv_def cdcl⇩W_conflicting_def cdcl⇩W_M_level_inv_def
    by (auto simp: subset_mset_trans_add_mset)
  have undef_L: ‹undefined_lit M1 L›
    using inv_T T decomp unfolding cdcl⇩W_all_struct_inv_def cdcl⇩W_M_level_inv_def
    by (auto simp: defined_lit_map)

  show False
  proof (cases ‹L ∈# E›)
    case True
    then obtain E' where
      E: ‹E = add_mset L E'›
      by (auto dest: multi_member_split)
    then have ‹distinct_mset E'› and ‹L ∉# E'› and E'_E': ‹E' ⊆# D'›
      using dist_E T E_subset by auto
    then have M1_E': ‹M1 ⊨as CNot E'›
      using M1_D' T unfolding true_annots_true_cls_def_iff_negation_in_model
      by (auto dest: multi_member_split[of _ E] mset_subset_eq_insertD)
    have propa:  ‹⋀M' K M L D. trail S = M' @ Decided K # M ⟹
      D + {#L#} ∈# clauses S ⟹ undefined_lit M L ⟹ ¬ M ⊨as CNot D›
      using smaller unfolding no_smaller_propa_def by blast
    show False
      using M1_E' propa[of ‹M2' @ M2› K M1 E', OF M2' _ undef_L] n_dist unfolding E
      by auto
  next
    case False
    then have ‹E ⊆# D'›
      using E_subset T by (auto simp: subset_add_mset_notin_subset)
    then have M1_E: ‹M1 ⊨as CNot E›
      using M1_D' T dist_E E_subset unfolding  true_annots_true_cls_def_iff_negation_in_model
      by (auto dest: multi_member_split[of _ E] mset_subset_eq_insertD)
    have confl:  ‹⋀M' K M L D. trail S = M' @ Decided K # M ⟹
      D ∈# clauses S ⟹ ¬ M ⊨as CNot D›
      using smaller_conf unfolding no_smaller_confl_def by blast
    show False
      using confl[of ‹M2' @ M2› K M1 E, OF M2'] n_dist M1_E
      by auto
  qed
qed

lemma cdcl⇩W_stgy_no_relearned_highest_subres_clause:
  assumes
    cdcl: ‹backtrack S T› and
    inv: ‹cdcl⇩W_all_struct_inv S› and
    smaller: ‹no_smaller_propa S› and
    smaller_conf: ‹no_smaller_confl S› and
    E_subset: ‹mark_of (hd_trail T) = add_mset (lit_of (hd_trail T)) E›
  shows ‹add_mset (- lit_of (hd_trail T)) E ∉# clauses S›
proof (rule ccontr)
  assume n_dist: ‹¬ ?thesis›
  obtain K L :: "'v literal" and
    M1 M2 :: "('v, 'v clause) ann_lit list" and i :: nat and D D' where
    confl_S: "conflicting S = Some (add_mset L D)" and
    decomp: "(Decided K # M1, M2) ∈ set (get_all_ann_decomposition (trail S))" and
    lev_L: "get_level (trail S) L = backtrack_lvl S" and
    max_D_L: "get_level (trail S) L = get_maximum_level (trail S) (add_mset L D')" and
    i: "get_maximum_level (trail S) D' ≡ i" and
    lev_K: "get_level (trail S) K = i + 1" and
    T: "T ∼ cons_trail (Propagated L (add_mset L D'))
        (reduce_trail_to M1
          (add_learned_cls (add_mset L D')
            (update_conflicting None S)))" and
    D_D': ‹D' ⊆# D› and
    ‹clauses S ⊨pm add_mset L D'›
    using cdcl by (auto elim!: rulesE)

  obtain M2' where M2': ‹trail S = (M2' @ M2) @ Decided K # M1›
    using decomp by auto
  have inv_T: ‹cdcl⇩W_all_struct_inv T›
    using cdcl cdcl⇩W_stgy_cdcl⇩W_all_struct_inv inv W_other backtrack bj
      cdcl⇩W_all_struct_inv_inv cdcl⇩W_cdcl⇩W_restart by blast
  have ‹distinct_mset (add_mset L D')›
    using inv_T T unfolding cdcl⇩W_all_struct_inv_def distinct_cdcl⇩W_state_def
    by auto

  have M1_D': ‹M1 ⊨as CNot D'›
    using backtrack_M1_CNot_D'[of S D' ‹i› K M1 M2 L ‹add_mset L D› T
        ‹Propagated L (add_mset L D')›] inv confl_S decomp i T D_D' lev_K lev_L max_D_L
    unfolding cdcl⇩W_all_struct_inv_def cdcl⇩W_conflicting_def cdcl⇩W_M_level_inv_def
    by (auto simp: subset_mset_trans_add_mset)
  have undef_L: ‹undefined_lit M1 L›
    using inv_T T decomp unfolding cdcl⇩W_all_struct_inv_def cdcl⇩W_M_level_inv_def
    by (auto simp: defined_lit_map)
  then have undef_uL: ‹undefined_lit M1 (-L)›
    by auto
  have propa:  ‹⋀M' K M L D. trail S = M' @ Decided K # M ⟹
    D + {#L#} ∈# clauses S ⟹ undefined_lit M L ⟹ ¬ M ⊨as CNot D›
    using smaller unfolding no_smaller_propa_def by blast
  have E[simp]: ‹E = D'›
    using E_subset T by (auto dest: multi_member_split)
  have propa:  ‹⋀M' K M L D. trail S = M' @ Decided K # M ⟹
    D + {#L#} ∈# clauses S ⟹ undefined_lit M L ⟹ ¬ M ⊨as CNot D›
    using smaller unfolding no_smaller_propa_def by blast
  show False
    using T M1_D' propa[of ‹M2' @ M2› K M1 D', OF M2' _ undef_uL] n_dist unfolding E
    by auto
qed


lemma cdcl⇩W_stgy_distinct_mset:
  assumes
    cdcl: ‹cdcl⇩W_stgy S T› and
    inv: "cdcl⇩W_all_struct_inv S" and
    smaller: ‹no_smaller_propa S› and
    dist: ‹distinct_mset (clauses S)›
  shows
    ‹distinct_mset (clauses T)›
proof (rule ccontr)
  assume n_dist: ‹¬ distinct_mset (clauses T)›
  then have ‹backtrack S T›
    using cdcl dist by (auto simp: cdcl⇩W_stgy.simps cdcl⇩W_o.simps cdcl⇩W_bj.simps
        elim: propagateE conflictE decideE skipE resolveE)
  then show False
    using n_dist cdcl⇩W_stgy_no_relearned_clause[of S T] dist
    by (auto simp: inv smaller elim!: rulesE)
qed

text ‹
  This is a more restrictive version of the previous theorem, but is a better bound for an
  implementation that does not do duplication removal (esp. as part of preprocessing).
›
lemma cdcl⇩W_stgy_learned_distinct_mset:
  assumes
    cdcl: ‹cdcl⇩W_stgy S T› and
    inv: "cdcl⇩W_all_struct_inv S" and
    smaller: ‹no_smaller_propa S› and
    dist: ‹distinct_mset (learned_clss S + remdups_mset (init_clss S))›
  shows
    ‹distinct_mset (learned_clss T + remdups_mset (init_clss T))›
proof (rule ccontr)
  assume n_dist: ‹¬ ?thesis›
  then have ‹backtrack S T›
    using cdcl dist by (auto simp: cdcl⇩W_stgy.simps cdcl⇩W_o.simps cdcl⇩W_bj.simps
        elim: propagateE conflictE decideE skipE resolveE)
  then show False
    using n_dist cdcl⇩W_stgy_no_relearned_clause[of S T] dist
    by (auto simp: inv smaller clauses_def elim!: rulesE)
qed

lemma rtranclp_cdcl⇩W_stgy_distinct_mset_clauses:
  assumes
    st: "cdcl⇩W_stgy⇧*⇧* R S" and
    invR: "cdcl⇩W_all_struct_inv R" and
    dist: "distinct_mset (clauses R)" and
    no_smaller: ‹no_smaller_propa R›
  shows "distinct_mset (clauses S)"
  using assms by (induction rule: rtranclp_induct)
    (auto simp: cdcl⇩W_stgy_distinct_mset rtranclp_cdcl⇩W_stgy_no_smaller_propa
      rtranclp_cdcl⇩W_stgy_cdcl⇩W_all_struct_inv)


lemma rtranclp_cdcl⇩W_stgy_distinct_mset_learned_clauses:
  assumes
    st: "cdcl⇩W_stgy⇧*⇧* R S" and
    invR: "cdcl⇩W_all_struct_inv R" and
    dist: "distinct_mset (learned_clss R + remdups_mset (init_clss R))" and
    no_smaller: ‹no_smaller_propa R›
  shows "distinct_mset (learned_clss S + remdups_mset (init_clss S))"
  using assms by (induction rule: rtranclp_induct)
    (auto simp: cdcl⇩W_stgy_learned_distinct_mset rtranclp_cdcl⇩W_stgy_no_smaller_propa
      rtranclp_cdcl⇩W_stgy_cdcl⇩W_all_struct_inv)

lemma cdcl⇩W_stgy_distinct_mset_clauses:
  assumes
    st: "cdcl⇩W_stgy⇧*⇧* (init_state N) S" and
    no_duplicate_clause: "distinct_mset N" and
    no_duplicate_in_clause: "distinct_mset_mset N"
  shows "distinct_mset (clauses S)"
  using rtranclp_cdcl⇩W_stgy_distinct_mset_clauses[OF st] assms
  by (auto simp: cdcl⇩W_all_struct_inv_def distinct_cdcl⇩W_state_def no_smaller_propa_def)

lemma cdcl⇩W_stgy_learned_distinct_mset_new:
  assumes
    cdcl: ‹cdcl⇩W_stgy S T› and
    inv: "cdcl⇩W_all_struct_inv S" and
    smaller: ‹no_smaller_propa S› and
    dist: ‹distinct_mset (learned_clss S - A)›
  shows ‹distinct_mset (learned_clss T - A)›
proof (rule ccontr)
  have [iff]: ‹distinct_mset (add_mset C (learned_clss S) - A) ⟷
     C ∉# (learned_clss S) - A› for C
    using dist distinct_mset_add_mset[of C ‹learned_clss S - A›]
  proof -
    have f1: "learned_clss S - A = remove1_mset C (add_mset C (learned_clss S) - A)"
      by (metis Multiset.diff_right_commute add_mset_remove_trivial)
    have "remove1_mset C (add_mset C (learned_clss S) - A) = add_mset C (learned_clss S) - A ⟶
        distinct_mset (add_mset C (learned_clss S) - A)"
      by (metis (no_types) Multiset.diff_right_commute add_mset_remove_trivial dist)
    then have "¬ distinct_mset (add_mset C (learned_clss S - A)) ∨
        distinct_mset (add_mset C (learned_clss S) - A) ≠ (C ∈# learned_clss S - A)"
      by (metis (full_types) Multiset.diff_right_commute
          distinct_mset_add_mset[of C ‹learned_clss S - A›] add_mset_remove_trivial
          diff_single_trivial insert_DiffM)
    then show ?thesis
      using f1 by (metis (full_types) distinct_mset_add_mset[of C ‹learned_clss S - A›]
          diff_single_trivial dist insert_DiffM)
  qed

  assume n_dist: ‹¬ ?thesis›
  then have ‹backtrack S T›
    using cdcl dist by (auto simp: cdcl⇩W_stgy.simps cdcl⇩W_o.simps cdcl⇩W_bj.simps
        elim: propagateE conflictE decideE skipE resolveE)
  then show False
    using n_dist cdcl⇩W_stgy_no_relearned_clause[of S T]
    by (auto simp: inv smaller clauses_def elim!: rulesE
        dest!: in_diffD)
qed

lemma rtranclp_cdcl⇩W_stgy_distinct_mset_clauses_new_abs:
  assumes
    st: "cdcl⇩W_stgy⇧*⇧* R S" and
    invR: "cdcl⇩W_all_struct_inv R" and
    no_smaller: ‹no_smaller_propa R› and
    ‹distinct_mset (learned_clss R - A)›
  shows "distinct_mset (learned_clss S - A)"
  using assms by (induction rule: rtranclp_induct)
    (auto simp: cdcl⇩W_stgy_distinct_mset rtranclp_cdcl⇩W_stgy_no_smaller_propa
      rtranclp_cdcl⇩W_stgy_cdcl⇩W_all_struct_inv
      cdcl⇩W_stgy_learned_distinct_mset_new)

lemma rtranclp_cdcl⇩W_stgy_distinct_mset_clauses_new:
  assumes
    st: "cdcl⇩W_stgy⇧*⇧* R S" and
    invR: "cdcl⇩W_all_struct_inv R" and
    no_smaller: ‹no_smaller_propa R›
  shows "distinct_mset (learned_clss S - learned_clss R)"
  using assms by (rule rtranclp_cdcl⇩W_stgy_distinct_mset_clauses_new_abs) auto


subsubsection ‹Decrease of a Measure›

fun cdcl⇩W_restart_measure where
"cdcl⇩W_restart_measure S =
  [(3::nat) ^ (card (atms_of_mm (init_clss S))) - card (set_mset (learned_clss S)),
    if conflicting S = None then 1 else 0,
    if conflicting S = None then card (atms_of_mm (init_clss S)) - length (trail S)
    else length (trail S)
    ]"

lemma length_model_le_vars:
  assumes
    "no_strange_atm S" and
    no_d: "no_dup (trail S)" and
    "finite (atms_of_mm (init_clss S))"
  shows "length (trail S) ≤ card (atms_of_mm (init_clss S))"
proof -
  obtain M N U k D where S: "state S = (M, N, U, k, D)" by (cases "state S", auto)
  have "finite (atm_of ` lits_of_l (trail S))"
    using assms(1,3) unfolding S by (auto simp add: finite_subset)
  have "length (trail S) = card (atm_of ` lits_of_l (trail S))"
    using no_dup_length_eq_card_atm_of_lits_of_l no_d by blast
  then show ?thesis using assms(1) unfolding no_strange_atm_def
  by (auto simp add: assms(3) card_mono)
qed

lemma length_model_le_vars_all_inv:
  assumes "cdcl⇩W_all_struct_inv S"
  shows "length (trail S) ≤ card (atms_of_mm (init_clss S))"
  using assms length_model_le_vars[of S] unfolding cdcl⇩W_all_struct_inv_def
  by (auto simp: cdcl⇩W_M_level_inv_decomp)

lemma learned_clss_less_upper_bound:
  fixes S :: 'st
  assumes
    "distinct_cdcl⇩W_state S" and
    "∀s ∈# learned_clss S. ¬tautology s"
  shows "card(set_mset (learned_clss S)) ≤ 3 ^ card (atms_of_mm (learned_clss S))"
proof -
  have "set_mset (learned_clss S) ⊆ simple_clss (atms_of_mm (learned_clss S))"
    apply (rule simplified_in_simple_clss)
    using assms unfolding distinct_cdcl⇩W_state_def by auto
  then have "card(set_mset (learned_clss S))
    ≤ card (simple_clss (atms_of_mm (learned_clss S)))"
    by (simp add: simple_clss_finite card_mono)
  then show ?thesis
    by (meson atms_of_ms_finite simple_clss_card finite_set_mset order_trans)
qed


lemma cdcl⇩W_restart_measure_decreasing:
  fixes S :: 'st
  assumes
    "cdcl⇩W_restart S S'" and
    no_restart:
      "¬(learned_clss S ⊆# learned_clss S' ∧ [] = trail S' ∧ conflicting S' = None)"
    (*no restart*) and
    no_forget: "learned_clss S ⊆# learned_clss S'" (*no forget*) and
    no_relearn: "⋀S'. backtrack S S' ⟹ mark_of (hd_trail S') ∉# learned_clss S"
      and
    alien: "no_strange_atm S" and
    M_level: "cdcl⇩W_M_level_inv S" and
    no_taut: "∀s ∈# learned_clss S. ¬tautology s" and
    no_dup: "distinct_cdcl⇩W_state S" and
    confl: "cdcl⇩W_conflicting S"
  shows "(cdcl⇩W_restart_measure S', cdcl⇩W_restart_measure S) ∈ lexn less_than 3"
  using assms(1) assms(2,3)
proof (induct rule: cdcl⇩W_restart_all_induct)
  case (propagate C L) note conf = this(1) and undef = this(5) and T = this(6)
  have propa: "propagate S (cons_trail (Propagated L C) S)"
    using propagate_rule[OF propagate.hyps(1,2)] propagate.hyps by auto
  then have no_dup': "no_dup (Propagated L C # trail S)"
    using M_level cdcl⇩W_M_level_inv_decomp(2) undef defined_lit_map by auto

  let ?N = "init_clss S"
  have "no_strange_atm (cons_trail (Propagated L C) S)"
    using alien cdcl⇩W_restart.propagate cdcl⇩W_restart_no_strange_atm_inv propa M_level by blast
  then have "atm_of ` lits_of_l (Propagated L C # trail S)
    ⊆ atms_of_mm (init_clss S)"
    using undef unfolding no_strange_atm_def by auto
  then have "card (atm_of ` lits_of_l (Propagated L C # trail S))
    ≤ card (atms_of_mm (init_clss S))"
    by (meson atms_of_ms_finite card_mono finite_set_mset)
  then have "length (Propagated L C # trail S) ≤ card (atms_of_mm ?N)"
    using no_dup_length_eq_card_atm_of_lits_of_l no_dup' by fastforce
  then have H: "card (atms_of_mm (init_clss S)) - length (trail S)
    = Suc (card (atms_of_mm (init_clss S)) - Suc (length (trail S)))"
    by simp
  show ?case using conf T undef by (auto simp: H lexn3_conv)
next
  case (decide L) note conf = this(1) and undef = this(2) and T = this(4)
  moreover {
    have dec: "decide S (cons_trail (Decided L) S)"
      using decide_rule decide.hyps by force
    then have "cdcl⇩W_restart S (cons_trail (Decided L) S)"
      using cdcl⇩W_restart.simps cdcl⇩W_o.intros by blast } note cdcl⇩W_restart = this
  moreover {
    have lev: "cdcl⇩W_M_level_inv (cons_trail (Decided L) S)"
      using cdcl⇩W_restart M_level cdcl⇩W_restart_consistent_inv[OF cdcl⇩W_restart] by auto
    then have no_dup: "no_dup (Decided L # trail S)"
      using undef unfolding cdcl⇩W_M_level_inv_def by auto
    have "no_strange_atm (cons_trail (Decided L) S)"
      using M_level alien calculation(4) cdcl⇩W_restart_no_strange_atm_inv by blast
    then have "length (Decided L # (trail S))
      ≤ card (atms_of_mm (init_clss S))"
      using no_dup undef
      length_model_le_vars[of "cons_trail (Decided L) S"]
      by fastforce }
  ultimately show ?case using conf by (simp add: lexn3_conv)
next
  case (skip L C' M D) note tr = this(1) and conf = this(2) and T = this(5)
  show ?case using conf T by (simp add: tr lexn3_conv)
next
  case conflict
  then show ?case by (simp add: lexn3_conv)
next
  case resolve
  then show ?case using finite by (simp add: lexn3_conv)
next
  case (backtrack L D K i M1 M2 T D') note conf = this(1) and decomp = this(3) and D_D' = this(7)
    and T = this(9)
  let ?D' = ‹add_mset L D'›
  have bt: "backtrack S T"
    using backtrack_rule[OF backtrack.hyps] by auto
  have "?D' ∉# learned_clss S"
    using no_relearn[OF bt] conf T by auto
  then have card_T:
    "card (set_mset ({#?D'#} + learned_clss S)) = Suc (card (set_mset (learned_clss S)))"
    by simp
  have "distinct_cdcl⇩W_state T"
    using bt M_level distinct_cdcl⇩W_state_inv no_dup other cdcl⇩W_o.intros cdcl⇩W_bj.intros by blast
  moreover have "∀s∈#learned_clss T. ¬ tautology s"
    using learned_clss_are_not_tautologies[OF cdcl⇩W_restart.other[OF cdcl⇩W_o.bj[OF
      cdcl⇩W_bj.backtrack[OF bt]]]] M_level no_taut confl by auto
  ultimately have "card (set_mset (learned_clss T)) ≤ 3 ^ card (atms_of_mm (learned_clss T))"
      by (auto simp: learned_clss_less_upper_bound)
    then have H: "card (set_mset ({#?D'#} + learned_clss S))
      ≤ 3 ^ card (atms_of_mm ({#?D'#} + learned_clss S))"
      using T decomp M_level by (simp add: cdcl⇩W_M_level_inv_decomp)
  moreover
    have "atms_of_mm ({#?D'#} + learned_clss S) ⊆ atms_of_mm (init_clss S)"
      using alien conf atms_of_subset_mset_mono[OF D_D'] unfolding no_strange_atm_def
      by auto
    then have card_f: "card (atms_of_mm ({#?D'#} + learned_clss S))
      ≤ card (atms_of_mm (init_clss S))"
      by (meson atms_of_ms_finite card_mono finite_set_mset)
    then have "(3::nat) ^ card (atms_of_mm ({#?D'#} + learned_clss S))
      ≤ 3 ^ card (atms_of_mm (init_clss S))" by simp
  ultimately have "(3::nat) ^ card (atms_of_mm (init_clss S))
    ≥ card (set_mset ({#?D'#} + learned_clss S))"
    using le_trans by blast
  then show ?case using decomp diff_less_mono2 card_T T M_level
    by (auto simp: cdcl⇩W_M_level_inv_decomp lexn3_conv)
next
  case restart
  then show ?case using alien by auto
next
  case (forget C T) note no_forget = this(9)
  then have "C ∈# learned_clss S" and "C ∉# learned_clss T"
    using forget.hyps by auto
  then have "¬ learned_clss S ⊆# learned_clss T"
     by (auto simp add: mset_subset_eqD)
  then show ?case using no_forget by blast
qed

lemma cdcl⇩W_stgy_step_decreasing:
  fixes S T :: 'st
  assumes
    cdcl: ‹cdcl⇩W_stgy S T› and
    struct_inv: ‹cdcl⇩W_all_struct_inv S› and
    smaller: ‹no_smaller_propa S›
  shows "(cdcl⇩W_restart_measure T, cdcl⇩W_restart_measure S) ∈ lexn less_than 3"
proof (rule cdcl⇩W_restart_measure_decreasing)
  show ‹cdcl⇩W_restart S T›
    using cdcl cdcl⇩W_cdcl⇩W_restart cdcl⇩W_stgy_cdcl⇩W by blast
  show ‹¬ (learned_clss S ⊆# learned_clss T ∧ [] = trail T ∧ conflicting T = None)›
    using cdcl by (cases rule: cdcl⇩W_stgy_cases) (auto elim!: rulesE)
  show ‹learned_clss S ⊆# learned_clss T›
    using cdcl by (cases rule: cdcl⇩W_stgy_cases) (auto elim!: rulesE)
  show ‹mark_of (hd_trail S') ∉# learned_clss S› if ‹backtrack S S'› for S'
    using cdcl⇩W_stgy_no_relearned_clause[of S S'] cdcl⇩W_stgy_no_smaller_propa[of S S']
      cdcl struct_inv smaller that unfolding clauses_def
    by (auto elim!: rulesE)
  show ‹no_strange_atm S› and ‹cdcl⇩W_M_level_inv S› and ‹distinct_cdcl⇩W_state S› and
    ‹cdcl⇩W_conflicting S› and ‹∀s∈#learned_clss S. ¬ tautology s›
    using struct_inv unfolding cdcl⇩W_all_struct_inv_def by blast+
qed

lemma empty_trail_no_smaller_propa: ‹trail R = [] ⟹ no_smaller_propa R›
  by (simp add: no_smaller_propa_def)

text ‹Roughly corresponds to \cwref{theo:prop:cdcltermlc}{theorem 2.9.15 page 100}
  but using a different bound (the bound is below)›
lemma tranclp_cdcl⇩W_stgy_decreasing:
  fixes R S T :: 'st
  assumes "cdcl⇩W_stgy⇧+⇧+ R S" and
  tr: "trail R = []" and
  "cdcl⇩W_all_struct_inv R"
  shows "(cdcl⇩W_restart_measure S, cdcl⇩W_restart_measure R) ∈ lexn less_than 3"
  using assms
  apply induction
   using empty_trail_no_smaller_propa cdcl⇩W_stgy_no_relearned_clause cdcl⇩W_stgy_step_decreasing
    apply blast
  using tranclp_into_rtranclp[of cdcl⇩W_stgy R] lexn_transI[OF trans_less_than, of 3]
    rtranclp_cdcl⇩W_stgy_no_smaller_propa unfolding trans_def
  by (meson cdcl⇩W_stgy_step_decreasing empty_trail_no_smaller_propa
      rtranclp_cdcl⇩W_stgy_cdcl⇩W_all_struct_inv)

lemma tranclp_cdcl⇩W_stgy_S0_decreasing:
  fixes R S T :: 'st
  assumes
    pl: "cdcl⇩W_stgy⇧+⇧+ (init_state N) S" and
    no_dup: "distinct_mset_mset N"
  shows "(cdcl⇩W_restart_measure S, cdcl⇩W_restart_measure (init_state N)) ∈ lexn less_than 3"
proof -
  have "cdcl⇩W_all_struct_inv (init_state N)"
    using no_dup unfolding cdcl⇩W_all_struct_inv_def by auto
  then show ?thesis using pl tranclp_cdcl⇩W_stgy_decreasing init_state_trail by blast
qed

lemma wf_tranclp_cdcl⇩W_stgy:
  "wf {(S::'st, init_state N)| S N. distinct_mset_mset N ∧ cdcl⇩W_stgy⇧+⇧+ (init_state N) S}"
  apply (rule wf_wf_if_measure'_notation2[of "lexn less_than 3" _ _ cdcl⇩W_restart_measure])
   apply (simp add: wf wf_lexn)
  using tranclp_cdcl⇩W_stgy_S0_decreasing by blast

text ‹The following theorems is deeply linked with the strategy: It shows that a decision alone
cannot lead to a conflict. This is obvious but I expect this to be a major part of the proof that
the number of learnt clause cannot be larger that \<^term>‹2^n›.›
lemma no_conflict_after_decide:
  assumes
    dec: ‹decide S T› and
    inv: ‹cdcl⇩W_all_struct_inv T› and
    smaller: ‹no_smaller_propa T› and
    smaller_confl: ‹no_smaller_confl T›
  shows ‹¬conflict T U›
proof (rule ccontr)
  assume ‹¬ ?thesis›
  then obtain D where
    D: ‹D ∈# clauses T› and
    confl: ‹trail T ⊨as CNot D›
    by (auto simp: conflict.simps)
  obtain L where
    ‹conflicting S = None› and
    undef: ‹undefined_lit (trail S) L› and
    ‹atm_of L ∈ atms_of_mm (init_clss S)› and
    T: ‹T ∼ cons_trail (Decided L) S›
    using dec by (auto simp: decide.simps)
  have dist: ‹distinct_mset D›
    using inv D unfolding cdcl⇩W_all_struct_inv_def distinct_cdcl⇩W_state_def
    by (auto dest!: multi_member_split simp: clauses_def)
  have L_D: ‹L ∉# D›
    using confl undef T
    by (auto dest!: multi_member_split simp: Decided_Propagated_in_iff_in_lits_of_l)

  show False
  proof (cases ‹-L ∈# D›)
    case True
    have H: ‹trail T = M' @ Decided K # M ⟹
      D + {#L#} ∈# clauses T ⟹ undefined_lit M L ⟹ ¬ M ⊨as CNot D›
      for M K M' D L
      using smaller unfolding no_smaller_propa_def
      by auto
    have ‹trail S ⊨as CNot (remove1_mset (-L) D)›
      using true_annots_CNot_lit_of_notin_skip[of ‹Decided L› ‹trail S› ‹remove1_mset (-L) D›] T True
        dist confl L_D
      by (auto dest: multi_member_split)
    then show False
      using True H[of ‹Nil› L ‹trail S› ‹remove1_mset (-L) D› ‹-L›] T D confl undef
      by auto
  next
    case False
    have H: ‹trail T = M' @ Decided K # M ⟹
      D ∈# clauses T ⟹ ¬ M ⊨as CNot D›
      for M K M' D
      using smaller_confl unfolding no_smaller_confl_def
      by auto
    have ‹trail S ⊨as CNot D›
      using true_annots_CNot_lit_of_notin_skip[of ‹Decided L› ‹trail S› D] T False
        dist confl L_D
      by (auto dest: multi_member_split)
    then show False
      using False H[of ‹Nil› L ‹trail S› D] T D confl undef
      by auto
  qed
qed

abbreviation list_weight_propa_trail :: ‹ ('v literal, 'v literal, 'v literal multiset) annotated_lit list ⇒ bool list› where
‹list_weight_propa_trail M ≡ map is_proped M›

definition comp_list_weight_propa_trail :: ‹nat ⇒  ('v literal, 'v literal, 'v literal multiset) annotated_lit list ⇒ bool list› where
‹comp_list_weight_propa_trail b M ≡ replicate (b - length M) False @ list_weight_propa_trail M›

lemma comp_list_weight_propa_trail_append[simp]:
  ‹comp_list_weight_propa_trail b (M @ M') =
     comp_list_weight_propa_trail (b - length M') M @ list_weight_propa_trail M'›
  by (auto simp: comp_list_weight_propa_trail_def)

lemma comp_list_weight_propa_trail_append_single[simp]:
  ‹comp_list_weight_propa_trail b (M @ [K]) =
    comp_list_weight_propa_trail (b - 1) M @ [is_proped K]›
  by (auto simp: comp_list_weight_propa_trail_def)

lemma comp_list_weight_propa_trail_cons[simp]:
  ‹comp_list_weight_propa_trail b (K # M') =
    comp_list_weight_propa_trail (b - Suc (length M')) [] @ is_proped K # list_weight_propa_trail M'›
  by (auto simp: comp_list_weight_propa_trail_def)

fun of_list_weight :: ‹bool list ⇒ nat› where
  ‹of_list_weight [] = 0›
| ‹of_list_weight (b # xs) = (if b then 1 else 0) + 2 * of_list_weight xs›

lemma of_list_weight_append[simp]:
  ‹of_list_weight (a @ b) = of_list_weight a + 2^(length a) * of_list_weight b›
  by (induction a) auto

lemma of_list_weight_append_single[simp]:
  ‹of_list_weight (a @ [b]) = of_list_weight a + 2^(length a) * (if b then 1 else 0)›
  using of_list_weight_append[of ‹a› ‹[b]›]
  by (auto simp del: of_list_weight_append)

lemma of_list_weight_replicate_False[simp]: ‹of_list_weight (replicate n False) = 0›
  by (induction n) auto

lemma of_list_weight_replicate_True[simp]: ‹of_list_weight (replicate n True) = 2^n - 1›
  apply (induction n)
  subgoal by auto
  subgoal for m
    using power_gt1_lemma[of ‹2 :: nat›]
    by (auto simp add: algebra_simps Suc_diff_Suc)
  done

lemma of_list_weight_le: ‹of_list_weight xs ≤ 2^(length xs) - 1›
proof -
  have ‹of_list_weight xs ≤ of_list_weight (replicate (length xs) True)›
    by (induction xs) auto
  then show ‹?thesis›
    by auto
qed

lemma of_list_weight_lt: ‹of_list_weight xs < 2^(length xs)›
  using of_list_weight_le[of xs]  by (metis One_nat_def Suc_le_lessD
    Suc_le_mono Suc_pred of_list_weight_le zero_less_numeral zero_less_power)

lemma [simp]: ‹of_list_weight (comp_list_weight_propa_trail n []) = 0›
  by (auto simp: comp_list_weight_propa_trail_def)

abbreviation propa_weight
  :: ‹nat ⇒ ('v literal, 'v literal, 'v literal multiset) annotated_lit list ⇒ nat›
where
  ‹propa_weight n M ≡ of_list_weight (comp_list_weight_propa_trail n M)›

lemma length_comp_list_weight_propa_trail[simp]: ‹length (comp_list_weight_propa_trail a M) = max (length M) a›
  by (auto simp: comp_list_weight_propa_trail_def)

lemma (in -)pow2_times_n:
  ‹Suc a ≤ n ⟹ 2 * 2^(n - Suc a) = (2::nat)^ (n - a)›
  ‹Suc a ≤ n ⟹ 2^(n - Suc a) * 2 = (2::nat)^ (n - a)›
  ‹Suc a ≤ n ⟹ 2^(n - Suc a) * b * 2 = (2::nat)^ (n - a) * b›
  ‹Suc a ≤ n ⟹ 2^(n - Suc a) * (b * 2) = (2::nat)^ (n - a) * b›
  ‹Suc a ≤ n ⟹ 2^(n - Suc a) * (2 * b) = (2::nat)^ (n - a) * b›
  ‹Suc a ≤ n ⟹ 2 * b * 2^(n - Suc a) = (2::nat)^ (n - a) * b›
  ‹Suc a ≤ n ⟹ 2 * (b * 2^(n - Suc a)) = (2::nat)^ (n - a) * b›
  apply (simp_all add: Suc_diff_Suc semiring_normalization_rules(27))
  using Suc_diff_le by fastforce+

lemma decide_propa_weight:
  ‹decide S T ⟹ n ≥ length (trail T) ⟹ propa_weight n (trail S) ≤ propa_weight n (trail T)›
  by (auto elim!: decideE simp: comp_list_weight_propa_trail_def
    algebra_simps pow2_times_n)

lemma propagate_propa_weight:
  ‹propagate S T ⟹ n ≥ length (trail T) ⟹ propa_weight n (trail S) < propa_weight n (trail T)›
  by (auto elim!: propagateE simp: comp_list_weight_propa_trail_def
    algebra_simps pow2_times_n)

text ‹
  The theorem below corresponds the bound of \cwref{theo:prop:cdcltermlc}{theorem 2.9.15 page 100}.
  In the current version there is no proof of the bound.

  The following proof contains an immense amount of stupid bookkeeping. The proof itself
  is rather easy and Isabelle makes it extra-complicated.

  Let's consider the sequence \<^text>‹S → ... → T›.
  The bookkeping part:
    ▸ We decompose it into its components \<^text>‹f 0 → f 1 → ... → f n›.
    ▸ Then we extract the backjumps out of it, which are at position \<^text>‹nth_nj 0›,
      \<^text>‹nth_nj 1›, ...
    ▸ Then we extract the conflicts out of it, which are at position \<^text>‹nth_confl 0›,
      \<^text>‹nth_confl 1›, ...

  Then the simple part:
    ▸ each backtrack increases \<^term>‹propa_weight›
    ▸ but \<^term>‹propa_weight› is bounded by \<^term>‹2 ^ (card (atms_of_mm (init_clss S)))›
  Therefore, we get the bound.

  Comments on the proof:
  ▪ The main problem of the proof is the number of inductions in the bookkeeping part.
  ▪ The proof is actually by contradiction to make sure that enough backtrack step exists. This could
    probably be avoided, but without change in the proof.

  Comments on the bound:
  ▪ The proof is very very crude: Any propagation also decreases the bound. The lemma
    @{thm no_conflict_after_decide} above shows that a decision cannot lead immediately to a
    conflict.
  ▪ TODO: can a backtrack could be immediately followed by another conflict
    (if there are several conflicts for the initial backtrack)? If not the bound can be divided by
    two.
›
lemma cdcl_pow2_n_learned_clauses:
  assumes
    cdcl: ‹cdcl⇩W⇧*⇧* S T› and
    confl: ‹conflicting S = None› and
    inv: ‹cdcl⇩W_all_struct_inv S›
  shows ‹size (learned_clss T) ≤ size (learned_clss S) + 2 ^ (card (atms_of_mm (init_clss S)))›
    (is ‹_ ≤ _ + ?b›)
proof (rule ccontr)
  assume ge: ‹¬ ?thesis›
  let ?m = ‹card (atms_of_mm (init_clss S))›
  obtain n :: nat where
    n: ‹(cdcl⇩W^^n) S T›
    using cdcl unfolding rtranclp_power by fast
  then obtain f :: ‹nat ⇒ 'st› where
    f: ‹⋀i. i < n ⟹ cdcl⇩W (f i) (f (Suc i))› and
    [simp]: ‹f 0 = S› and
    [simp]: ‹f n = T›
    using power_ex_decomp[OF n]
    by auto

  have cdcl_st_k: ‹cdcl⇩W⇧*⇧* S (f k)› if ‹k ≤ n› for k
    using that
    apply (induction k)
    subgoal by auto
    subgoal for k using f[of k] by (auto)
    done
  let ?g = ‹λi. size (learned_clss (f i))›
  have ‹?g 0 = size (learned_clss S)›
    by auto
  have g_n: ‹?g n > ?g 0 + 2 ^ (card (atms_of_mm (init_clss S)))›
    using ge by auto
  have g: ‹?g (Suc i) = ?g i ∨ (?g (Suc i) = Suc (?g i) ∧ backtrack (f i) (f (Suc i)))› if ‹i < n›
    for i
    using f[OF that]
    by (cases rule: cdcl⇩W.cases)
      (auto elim: propagateE conflictE decideE backtrackE skipE resolveE
        simp: cdcl⇩W_o.simps cdcl⇩W_bj.simps)
  have g_le: ‹?g i ≤ i + ?g 0› if ‹i ≤ n› for i
    using that
    apply (induction i)
    subgoal by auto
    subgoal for i
      using g[of i]
      by auto
    done
  from this[of n] have n_ge_m: ‹n > ?b›
    using g_n ge by auto
  then have n0: ‹n > 0›
    using not_add_less1 by fastforce
  define nth_bj where
    ‹nth_bj = rec_nat 0 (λ_ j. (LEAST i. i > j ∧ i < n ∧ backtrack (f i) (f (Suc i))))›
  have [simp]: ‹nth_bj 0 = 0›
    by (auto simp: nth_bj_def)
  have nth_bj_Suc: ‹nth_bj (Suc i) = (LEAST x. nth_bj i < x ∧ x < n ∧ backtrack (f x) (f (Suc x)))›
    for i
    by (auto simp: nth_bj_def)

  have between_nth_bj_not_bt:
    ‹¬backtrack (f k) (f (Suc k))›
    if ‹k < n› ‹k > nth_bj i› ‹k < nth_bj (Suc i) › for k i
    using not_less_Least[of k ‹λx. nth_bj i < x ∧ x < n ∧ backtrack (f x) (f (Suc x))›] that
    unfolding nth_bj_Suc[symmetric]
    by auto

  have g_nth_bj_eq:
    ‹?g (Suc k) = ?g k›
    if ‹k < n› ‹k > nth_bj i› ‹k < nth_bj (Suc i)› for k i
    using between_nth_bj_not_bt[OF that(1-3)] f[of k, OF that(1)]
    by (auto elim: propagateE conflictE decideE backtrackE skipE resolveE
        simp: cdcl⇩W_o.simps cdcl⇩W_bj.simps cdcl⇩W.simps)
  have g_nth_bj_eq2:
    ‹?g (Suc k) = ?g (Suc (nth_bj i))›
    if ‹k < n› ‹k > nth_bj i› ‹k < nth_bj (Suc i)› for k i
    using that
    apply (induction k)
    subgoal by blast
    subgoal for k
      using g_nth_bj_eq less_antisym by fastforce
    done
  have [simp]: ‹?g (Suc 0) = ?g 0›
    using confl f[of 0] n0
    by (auto elim: propagateE conflictE decideE backtrackE skipE resolveE
        simp: cdcl⇩W_o.simps cdcl⇩W_bj.simps cdcl⇩W.simps)
  have ‹(?g (nth_bj i) = size (learned_clss S) + (i - 1)) ∧
    nth_bj i < n ∧
    nth_bj i ≥ i ∧
    (i > 0 ⟶ backtrack (f (nth_bj i)) (f (Suc (nth_bj i)))) ∧
    (i > 0 ⟶ ?g (Suc (nth_bj i)) = size (learned_clss S) + i) ∧
    (i > 0 ⟶ nth_bj i > nth_bj (i-1))›
    if ‹i ≤ ?b+1›
    for i
    using that
  proof (induction i)
    case 0
    then show ?case using n0 by auto
  next
    case (Suc i)
    then have IH: ‹?g (nth_bj i) = size (learned_clss S) + (i - 1)›
        ‹0 < i ⟹ backtrack (f (nth_bj i)) (f (Suc (nth_bj i)))›
	‹0 < i ⟹ ?g (Suc (nth_bj i))  = size (learned_clss S) + i› and
      i_le_m: ‹Suc i ≤ ?b+1› and
      le_n: ‹nth_bj i < n› and
      gei: ‹nth_bj i ≥ i›
      by auto
    have ex_larger: ‹∃x>nth_bj i. x < n ∧ backtrack (f x) (f (Suc x))›
    proof (rule ccontr)
      assume ‹¬ ?thesis›
      then have [simp]: ‹n>x ⟹ x>nth_bj i ⟹ ?g (Suc x) = ?g x› for x
        using g[of x] n_ge_m
	by auto
      have eq1: ‹nth_bj i < Suc x ⟹ ¬ nth_bj i < x ⟹ x = nth_bj i› and
         eq2: ‹nth_bj i < x ⟹ ¬ nth_bj i < x - Suc 0 ⟹ nth_bj i = x - Suc 0›
	 for x
        by simp_all
      have ex_larger: ‹n>x ⟹ x>nth_bj i ⟹ ?g (Suc x) = ?g (Suc (nth_bj i))› for x
        apply (induction x)
	subgoal by auto
	subgoal for x
	  by (cases ‹nth_bj i < x›) (auto dest: eq1)
	done
      from this[of ‹n-1›] have g_n_nth_bj: ‹?g n = ?g (Suc (nth_bj i))›
        using n_ge_m i_le_m le_n
	by (cases ‹nth_bj i < n - Suc 0›)
          (auto dest: eq2)
      then have ‹size (learned_clss (f (Suc (nth_bj i)))) < size (learned_clss T)›
        using g_n i_le_m n_ge_m g_le[of ‹Suc (nth_bj i)›] le_n ge
	   ‹?g (nth_bj i) = size (learned_clss S) + (i - 1)›
	using Suc.IH by auto
      then show False
        using g_n i_le_m n_ge_m g_le[of ‹Suc (nth_bj i)›] g_n_nth_bj by auto
    qed

    from LeastI_ex[OF ex_larger]
    have bt: ‹backtrack (f (nth_bj (Suc i))) (f (Suc (nth_bj (Suc i))))› and
      le: ‹nth_bj (Suc i) < n› and
      nth_mono: ‹nth_bj i < nth_bj (Suc i)›
      unfolding nth_bj_Suc[symmetric]
      by auto

    have g_nth_Suc_g_Suc_nth: ‹?g (nth_bj (Suc i)) = ?g (Suc (nth_bj i))›
      using g_nth_bj_eq2[of ‹nth_bj (Suc i) - 1› i] le nth_mono
      apply auto (*TODO proof*)
      by (metis Suc_pred gr0I less_Suc0 less_Suc_eq less_imp_diff_less)
    have H1: ‹size (learned_clss (f (Suc (nth_bj (Suc i))))) =
       1 + size (learned_clss (f (nth_bj (Suc i))))› if ‹i = 0›
      using bt unfolding that
      by (auto simp: that elim: backtrackE)
    have ?case if ‹i > 0›
      using IH that nth_mono le bt gei
      by (auto elim: backtrackE simp: g_nth_Suc_g_Suc_nth)
    moreover have ?case if ‹i = 0›
      using le bt gei nth_mono IH g_nth_bj_eq2[of ‹nth_bj (Suc i) - 1› i]
        g_nth_Suc_g_Suc_nth
      apply (intro conjI)
      subgoal by (simp add: that)
      subgoal by (auto simp: that elim: backtrackE)
      subgoal by (auto simp: that elim: backtrackE)
      subgoal Hk by (auto simp: that elim: backtrackE)
      subgoal using H1 by (auto simp: that elim: backtrackE)
      subgoal using nth_mono by auto
      done
    ultimately show ?case by blast
  qed
  then have
    ‹(?g (nth_bj i) = size (learned_clss S) + (i - 1))› and
    nth_bj_le: ‹nth_bj i < n› and
    nth_bj_ge: ‹nth_bj i ≥ i› and
    bt_nth_bj: ‹i > 0 ⟹ backtrack (f (nth_bj i)) (f (Suc (nth_bj i)))› and
    ‹i > 0 ⟹ ?g (Suc (nth_bj i)) = size (learned_clss S) + i› and
    nth_bj_mono: ‹i > 0 ⟹ nth_bj (i - 1) < nth_bj i›
    if ‹i ≤ ?b+1›
    for i
    using that by blast+
  have
    confl_None: ‹conflicting (f (Suc (nth_bj i))) = None› and
    confl_nth_bj: ‹conflicting (f (nth_bj i)) ≠ None›
    if ‹i ≤ ?b+1› ‹i > 0›
    for i
    using bt_nth_bj[OF that] by (auto simp: backtrack.simps)

  have conflicting_still_conflicting:
    ‹conflicting (f k) ≠ None ⟶ conflicting (f (Suc k)) ≠ None›
    if ‹k < n› ‹k > nth_bj i› ‹k < nth_bj (Suc i)› for k i
    using between_nth_bj_not_bt[OF that] f[OF that(1)]
    by (auto elim: propagateE conflictE decideE backtrackE skipE resolveE
        simp: cdcl⇩W_o.simps cdcl⇩W_bj.simps cdcl⇩W.simps)

  define nth_confl where
    ‹nth_confl n ≡ LEAST i. i > nth_bj n ∧ i < nth_bj (Suc n) ∧ conflict (f i) (f (Suc i))› for n
  have ‹∃i>nth_bj a. i < nth_bj (Suc a) ∧ conflict (f i) (f (Suc i))›
    if a_n: ‹a ≤ ?b› ‹a > 0›
    for a
  proof (rule ccontr)
    assume H: ‹¬ ?thesis›
    have ‹conflicting (f (nth_bj a + Suc i)) = None›
      if ‹nth_bj a + Suc i ≤ nth_bj (Suc a)› for i :: nat
      using that
      apply (induction i)
      subgoal
        using confl_None[of a] a_n n_ge_m by auto
      subgoal for i
        apply (cases ‹Suc (nth_bj a + i) < n›)
        using f[of ‹nth_bj a + Suc i›] H
        apply (auto elim: propagateE conflictE decideE backtrackE skipE resolveE
          simp: cdcl⇩W_o.simps cdcl⇩W_bj.simps cdcl⇩W.simps)[]
	using nth_bj_le[of ‹Suc a›] a_n(1) by auto
      done
    from this[of ‹nth_bj (Suc a) - 1 - nth_bj a›] a_n
    show False
      using nth_bj_mono[of ‹Suc a›] a_n nth_bj_le[of ‹Suc a›] confl_nth_bj[of ‹Suc a›]
      by auto
  qed
  from LeastI_ex[OF this] have nth_bj_le_nth_confl: ‹nth_bj a < nth_confl a› and
    nth_confl: ‹conflict (f (nth_confl a)) (f (Suc (nth_confl a)))› and
    nth_confl_le_nth_bj_Suc: ‹nth_confl a < nth_bj (Suc a)›
    if a_n: ‹a ≤ ?b› ‹a > 0›
    for a
    using that unfolding nth_confl_def[symmetric]
    by blast+
  have nth_confl_conflicting: ‹conflicting (f (Suc (nth_confl a))) ≠ None›
    if a_n: ‹a ≤ ?b› ‹a > 0›
    for a
    using nth_confl[OF a_n]
    by (auto simp: conflict.simps)
  have no_conflict_before_nth_confl: ‹¬conflict (f k) (f (Suc k))›
    if ‹k > nth_bj a› and
      ‹k < nth_confl a› and
      a_n: ‹a ≤ ?b› ‹a > 0›
    for k a
    using not_less_Least[of k ‹λi. i > nth_bj a ∧ i < nth_bj (Suc a) ∧ conflict (f i) (f (Suc i))›] that
    nth_confl_le_nth_bj_Suc[of a]
    unfolding nth_confl_def[symmetric]
    by auto
  have conflicting_after_nth_confl: ‹conflicting (f (Suc (nth_confl a) + k)) ≠ None›
    if a_n: ‹a ≤ ?b› ‹a > 0› and
      k: ‹Suc (nth_confl a) + k < nth_bj (Suc a)›
    for a k
    using k
    apply (induction k)
    subgoal using nth_confl_conflicting[OF a_n] by simp
    subgoal for k
      using conflicting_still_conflicting[of ‹Suc (nth_confl a + k)› a] a_n
        nth_bj_le[of a] nth_bj_le_nth_confl[of a]
      apply (cases ‹Suc (nth_confl a + k) < n›)
      apply auto
       by (metis (no_types, lifting) Suc_le_lessD add.commute le_less less_trans_Suc nth_bj_le
         plus_1_eq_Suc)
    done
  have conflicting_before_nth_confl: ‹conflicting (f (Suc (nth_bj a) + k)) = None›
    if a_n: ‹a ≤ ?b› ‹a > 0› and
      k: ‹Suc (nth_bj a) + k < nth_confl a›
    for a k
    using k
    apply (induction k)
    subgoal using confl_None[of a] a_n by simp
    subgoal for k
      using f[of ‹Suc (nth_bj a) + k›] no_conflict_before_nth_confl[of a ‹Suc (nth_bj a) + k›] a_n
        nth_confl_le_nth_bj_Suc[of a] nth_bj_le[of ‹Suc a›]
      apply (cases ‹Suc (nth_bj a + k) < n›)
      apply (auto elim!: propagateE conflictE decideE backtrackE skipE resolveE
          simp: cdcl⇩W_o.simps cdcl⇩W_bj.simps cdcl⇩W.simps)[]
      by linarith
    done
  have
    ex_trail_decomp: ‹∃M. trail (f (Suc (nth_confl a))) = M @ trail (f (Suc (nth_confl a + k)))›
    if a_n: ‹a ≤ ?b› ‹a > 0› and
      k: ‹Suc (nth_confl a) + k ≤ nth_bj (Suc a)›
    for a k
    using k
  proof (induction k)
    case 0
    then show ‹?case› by auto
  next
    case (Suc k)
    moreover have ‹nth_confl a + k < n›
      proof -
	have "nth_bj (Suc a) < n"
	  by (rule nth_bj_le) (use a_n(1) in simp)
	then show ?thesis
	  using Suc.prems by linarith
      qed
    moreover have ‹∃Ma. M @ trail (f (Suc (nth_confl a + k))) =
            Ma @ tl (trail (f (Suc (nth_confl a + k))))› for M
      by (cases ‹trail (f (Suc (nth_confl a + k)))›) auto
    ultimately show ?case
      using f[of ‹Suc (nth_confl a + k)›] conflicting_after_nth_confl[of a ‹k›, OF a_n] Suc
        between_nth_bj_not_bt[of ‹Suc (nth_confl a + k)› ‹a›]
	nth_bj_le_nth_confl[of a, OF a_n]
      apply (cases ‹Suc (nth_confl a + k) < n›)
      subgoal
        by (auto elim!: propagateE conflictE decideE skipE resolveE
          simp: cdcl⇩W_o.simps cdcl⇩W_bj.simps cdcl⇩W.simps)[]
      subgoal
        by (metis (no_types, lifting) Suc_leD Suc_lessI a_n(1) add.commute add_Suc
	  add_mono_thms_linordered_semiring(1) le_numeral_extra(4) not_le nth_bj_le plus_1_eq_Suc)
      done
  qed
  have propa_weight_decreasing_confl:
    ‹propa_weight n (trail (f (Suc (nth_bj (Suc a))))) > propa_weight n (trail (f (nth_confl a)))›
    if a_n: ‹a ≤ ?b› ‹a > 0› and
      n: ‹n ≥ length (trail (f (nth_confl a)))›
    for a n
  proof -
    have pw0: ‹propa_weight n (trail (f (Suc (nth_confl a)))) =
      propa_weight n (trail (f (nth_confl a)))› and
      [simp]: ‹trail (f (Suc (nth_confl a))) = trail (f (nth_confl a))›
      using nth_confl[OF a_n] by (auto elim!: conflictE)
    have H: ‹nth_bj (Suc a) = Suc (nth_confl a) ∨ nth_bj (Suc a) ≥ Suc (Suc (nth_confl a))›
      using nth_bj_le_nth_confl[of a, OF a_n]
      using a_n(1) nth_confl_le_nth_bj_Suc that(2) by force

    from ex_trail_decomp[of a ‹nth_bj (Suc a) - (1+nth_confl a)›, OF a_n]
    obtain M where
      M: ‹trail (f (Suc (nth_confl a))) = M @ trail (f (nth_bj (Suc a)))›
      apply -
      apply (rule disjE[OF H])
      subgoal
        by auto
      subgoal
        using nth_bj_le_nth_confl[of a, OF a_n] nth_bj_ge[of ‹Suc a›] a_n
	by (auto simp add: numeral_2_eq_2)
      done
    obtain K M1 M2 D D' L where
      decomp: ‹(Decided K # M1, M2)
         ∈ set (get_all_ann_decomposition (trail (f (nth_bj (Suc a)))))› and
      ‹get_maximum_level (trail (f (nth_bj (Suc a)))) (add_mset L D') =
       backtrack_lvl (f (nth_bj (Suc a)))› and
      ‹get_level (trail (f (nth_bj (Suc a)))) L = backtrack_lvl (f (nth_bj (Suc a)))› and
      ‹get_level (trail (f (nth_bj (Suc a)))) K =
       Suc (get_maximum_level (trail (f (nth_bj (Suc a)))) D')› and
      ‹D' ⊆# D› and
      ‹clauses (f (nth_bj (Suc a))) ⊨pm add_mset L D'› and
      st_Suc: ‹f (Suc (nth_bj (Suc a))) ∼
       cons_trail (Propagated L (add_mset L D'))
        (reduce_trail_to M1
          (add_learned_cls (add_mset L D')
            (update_conflicting None (f (nth_bj (Suc a))))))›
      using bt_nth_bj[of ‹Suc a›] a_n
      by (auto elim!: backtrackE)
    obtain M3 where
      tr: ‹trail (f (nth_bj (Suc a))) = M3 @ M2 @ Decided K # M1›
      using decomp by auto
    define M2' where
      ‹M2' = M3 @ M2›
    then have
      tr: ‹trail (f (nth_bj (Suc a))) = M2' @ Decided K # M1›
      using tr by auto
    define M' where
      ‹M' = M @ M2'›
    then have tr2: ‹trail (f (nth_confl a)) = M' @ Decided K # M1›
      using tr M n
      by auto
    have [simp]: ‹max (length M) (n - Suc (length M1 + (length M2')))
      = (n - Suc (length M1 + (length M2')))›
      using tr M st_Suc n by auto
    have [simp]: ‹2 *
      (of_list_weight (list_weight_propa_trail M1) *
       (2 ^ length M2' *
        (2 ^ (n - Suc (length M1 + length M2'))))) =
	 of_list_weight (list_weight_propa_trail M1) * 2 ^ (n - length M1)›
	 using tr M n by (auto simp: algebra_simps field_simps pow2_times_n
	   comm_semiring_1_class.semiring_normalization_rules(26))
    have n_ge: ‹Suc (length M + (length M2' + length M1)) ≤ n›
      using n st_Suc tr M by auto
    have WTF: ‹a < b ⟹ b ≤ c ⟹ a < c› and
      WTF': ‹a ≤ b ⟹ b < c ⟹ a < c› for a b c :: nat
      by auto

    have 3: ‹propa_weight (n - Suc (length M1 + (length M2'))) M
      ≤ 2^(n - Suc (length M1 + length M2')) - 1›
      using of_list_weight_le
      apply auto
      by (metis ‹max (length M) (n - Suc (length M1 + (length M2'))) = n - Suc (length M1 + (length M2'))›
        length_comp_list_weight_propa_trail)
    have 1: ‹of_list_weight (list_weight_propa_trail M2') *
      2 ^ (n - Suc (length M1 + length M2')) < Suc (if M2' = [] then 0
        else 2 ^ (n - Suc (length M1)) - 2 ^ (n - Suc (length M1 + length M2')))›
      apply (cases ‹M2' = []›)
      subgoal by auto
      subgoal
	apply (rule WTF')
	  apply (rule Nat.mult_le_mono1[of ‹of_list_weight (list_weight_propa_trail M2')›,
	  OF of_list_weight_le[of ‹(list_weight_propa_trail M2')›]])
	using of_list_weight_le[of ‹(list_weight_propa_trail M2')›] n M tr
	by (auto simp add: comm_semiring_1_class.semiring_normalization_rules(26)
	  algebra_simps)
      done
    have WTF2:
      ‹a ≤ a' ⟹ b < b' ⟹ a + b < a' + b'› for a b c a' b' c' :: nat
      by auto

    have ‹propa_weight (n - Suc (length M1 + length M2')) M +
    of_list_weight (list_weight_propa_trail M2') *
    2 ^ (n - Suc (length M1 + length M2'))
    < 2 ^ (n - Suc (length M1))›
      apply (rule WTF)
      apply (rule WTF2[OF 3 1])
      using n_ge[unfolded nat_le_iff_add] by (auto simp: ac_simps algebra_simps)
    then have ‹propa_weight n (trail (f (nth_confl a))) < propa_weight n (trail (f (Suc (nth_bj (Suc a)))))›
      using tr2 M st_Suc n tr
      by (auto simp: pow2_times_n algebra_simps
        comm_semiring_1_class.semiring_normalization_rules(26))
    then show ‹?thesis›
      using pw0 by auto
  qed
  have length_trail_le_m: ‹length (trail (f k)) < ?m + 1›
    if ‹k ≤ n›
    for k
  proof -
    have ‹cdcl⇩W_all_struct_inv (f k)›
      using rtranclp_cdcl⇩W_cdcl⇩W_restart[OF cdcl_st_k[OF that]] inv
      rtranclp_cdcl⇩W_all_struct_inv_inv by blast
    then have ‹cdcl⇩W_M_level_inv (f k)› and ‹no_strange_atm (f k)›
      unfolding cdcl⇩W_all_struct_inv_def by blast+
    then have ‹no_dup (trail (f k))› and
      incl: ‹atm_of ` lits_of_l (trail (f k)) ⊆ atms_of_mm (init_clss (f k))›
      unfolding cdcl⇩W_M_level_inv_def no_strange_atm_def
      by auto
    have eq: ‹(atms_of_mm (init_clss (f k))) = (atms_of_mm (init_clss S))›
      using rtranclp_cdcl⇩W_restart_init_clss[OF rtranclp_cdcl⇩W_cdcl⇩W_restart[OF cdcl_st_k[OF that]]]
      by auto
    have ‹length (trail (f k)) = card (atm_of ` lits_of_l (trail (f k)))›
      using ‹no_dup (trail (f k))› no_dup_length_eq_card_atm_of_lits_of_l by blast
    also have ‹card (atm_of ` lits_of_l (trail (f k))) ≤ ?m›
      using card_mono[OF _ incl] eq by auto
    finally show ?thesis
      by linarith
  qed
  have propa_weight_decreasing_propa:
    ‹propa_weight ?m (trail (f (nth_confl a))) ≥ propa_weight ?m (trail (f (Suc (nth_bj a))))›
    if a_n: ‹a ≤ ?b› ‹a > 0›
    for a
  proof -
    have ppa: ‹propa_weight ?m (trail (f (Suc (nth_bj a) + Suc k)))
      ≥ propa_weight ?m (trail (f (Suc (nth_bj a) + k)))›
      if ‹k < nth_confl a - Suc (nth_bj a)›
      for k
    proof -
      have ‹Suc (nth_bj a + k) < n› and ‹Suc (nth_bj a + k) < nth_confl a›
        using that nth_bj_le_nth_confl[OF a_n] nth_confl_le_nth_bj_Suc[OF a_n]
	  nth_bj_le[of ‹Suc a›] a_n
	by auto
      then show ?thesis
        using f[of ‹(Suc (nth_bj a) + k)›] conflicting_before_nth_confl[OF a_n, of ‹k›]
	no_conflict_before_nth_confl[OF _ _ a_n, of ‹Suc (nth_bj a) + k›] that
	length_trail_le_m[of ‹Suc (Suc (nth_bj a) + k)›]
        by (auto elim!: skipE resolveE backtrackE
            simp: cdcl⇩W_o.simps cdcl⇩W_bj.simps cdcl⇩W.simps
	    dest!: propagate_propa_weight[of _ _ ?m]
	      decide_propa_weight[of _ _ ?m])
    qed
    have WTF3: ‹(Suc (nth_bj a + (nth_confl a - Suc (nth_bj a)))) = nth_confl a›
      using a_n(1) nth_bj_le_nth_confl that(2) by fastforce
    have ‹propa_weight ?m (trail (f (Suc (nth_bj a) + k)))
      ≥ propa_weight ?m (trail (f (Suc (nth_bj a))))›
      if ‹k ≤ nth_confl a - Suc (nth_bj a)›
      for k
      using that
      apply (induction k)
      subgoal by auto
      subgoal for k using ppa[of k]
        apply (cases ‹k < nth_confl a - Suc (nth_bj a)›)
	subgoal by auto
	subgoal by linarith
      done
      done
    from this[of ‹nth_confl a - (Suc (nth_bj a))›]
    show ?thesis
      by (auto simp: WTF3)
  qed
  have propa_weight_decreasing_confl:
    ‹propa_weight ?m (trail (f (Suc (nth_bj a))))
      < propa_weight ?m (trail (f (Suc (nth_bj (Suc a)))))›
    if a_n: ‹a ≤ ?b› ‹a > 0›
    for a
  proof -
    have WTF: ‹b < c ⟹ a ≤ b ⟹ a < c› for a b c  :: nat by linarith
    have ‹nth_confl a < n›
      by (metis Suc_le_mono a_n(1) add.commute add_lessD1 less_imp_le nat_le_iff_add
        nth_bj_le nth_confl_le_nth_bj_Suc plus_1_eq_Suc that(2))

    show ?thesis
      apply (rule WTF)
        apply (rule propa_weight_decreasing_confl[OF a_n, of ?m])
	subgoal using length_trail_le_m[of ‹nth_confl a›] ‹nth_confl a < n› by auto
       apply (rule propa_weight_decreasing_propa[OF a_n])
      done
  qed
  have weight1: ‹propa_weight ?m (trail (f (Suc (nth_bj 1)))) ≥ 1›
    using bt_nth_bj[of 1]
    by (auto simp: elim!: backtrackE intro!: trans_le_add1)
  have ‹propa_weight ?m (trail (f (Suc (nth_bj (Suc a))))) ≥
       propa_weight ?m (trail (f (Suc (nth_bj 1)))) + a›
    if a_n: ‹a ≤ ?b›
    for a :: nat
    using that
    apply (induction a)
    subgoal by auto
    subgoal for a
      using propa_weight_decreasing_confl[of ‹Suc a›]
      by auto
    done
  from this[of ‹?b›] have ‹propa_weight ?m (trail (f (Suc (nth_bj (Suc (?b)))))) ≥ 1 + ?b›
    using weight1 by auto
  moreover have
    ‹max (length (trail (f (Suc (nth_bj (Suc ?b)))))) ?m = ?m›
    using length_trail_le_m[of ‹(Suc (nth_bj (Suc ?b)))›] Suc_leI nth_bj_le
    nth_bj_le[of ‹Suc (?b)›] by (auto simp: max_def)
  ultimately show ‹False›
    using of_list_weight_le[of ‹comp_list_weight_propa_trail ?m (trail (f (Suc (nth_bj (Suc ?b)))))›]
    by (simp del: state_eq_init_clss state_eq_trail)
qed

text ‹Application of the previous theorem to an initial state:›
corollary cdcl_pow2_n_learned_clauses2:
  assumes
    cdcl: ‹cdcl⇩W⇧*⇧* (init_state N) T› and
    inv: ‹cdcl⇩W_all_struct_inv (init_state N)›
  shows ‹size (learned_clss T) ≤ 2 ^ (card (atms_of_mm N))›
  using assms cdcl_pow2_n_learned_clauses[of ‹init_state N› T]
  by auto

text ‹A rather obvious theorem, but can be handy when talking about CDCL with inclusion of new rules.›
lemma cdcl⇩W_enlarge_clauses:
  assumes
    ‹cdcl⇩W S S'› and
    ‹trail T = trail S ∧ init_clss T = init_clss S + N' ∧
    learned_clss T = learned_clss S + U' ∧ conflicting T = conflicting S›
  shows ‹∃T'. trail T' = trail S' ∧ init_clss T' = init_clss S' + N' ∧
    learned_clss T' = learned_clss S' + U' ∧ conflicting T' = conflicting S' ∧
    cdcl⇩W T T'›
proof -
  note H = exI[of _ ‹cons_trail (Propagated L C)
        (reduce_trail_to xx_M
          (add_learned_cls _ (update_conflicting None T)))› for xx_M L C]
  show ?thesis
  using assms
  apply induction
  subgoal for S'
    by (auto simp: cdcl⇩W.simps propagate.simps clauses_def elim!: rulesE)
     (metis conflicting_cons_trail init_clss_cons_trail learned_clss_cons_trail state_eq_ref 
      trail_cons_trail)+
  subgoal for S'
    apply (auto simp: cdcl⇩W.simps conflict.simps clauses_def elim!: rulesE)
    apply (metis assms(1) conflicting_update_conflicting init_clss_update_conflicting
      learned_clss_update_conflicting state_eq_ref trail_update_conflicting)+
    done
  subgoal
    apply (induction rule: cdcl⇩W_o.induct)
  subgoal for S'
    apply (auto simp: cdcl⇩W.simps decide.simps clauses_def cdcl⇩W_o.simps elim!: rulesE)
    by (metis assms(1) conflicting_cons_trail_conflicting init_clss_cons_trail
      learned_clss_cons_trail state_eq_ref state_eq_trail trail_cons_trail)
  subgoal for S'
  apply (induction rule: cdcl⇩W_bj.induct)
  subgoal for S'
    by (auto simp: cdcl⇩W.simps skip.simps clauses_def  cdcl⇩W_o.simps cdcl⇩W_bj.simps elim!: rulesE
      intro!: exI[of _ ‹tl_trail T›])
  subgoal for S'
    apply (auto simp: cdcl⇩W.simps resolve.simps clauses_def cdcl⇩W_o.simps cdcl⇩W_bj.simps elim!: rulesE)
    by (metis conflicting_update_conflicting init_clss_tl_trail init_clss_update_conflicting learned_clss_tl_trail learned_clss_update_conflicting state_eq_ref trail_tl_trail trail_update_conflicting)
  subgoal for S'
    apply (clarsimp simp: cdcl⇩W.simps backtrack.simps clauses_def cdcl⇩W_o.simps cdcl⇩W_bj.simps)
    apply (rule_tac xx_M8=M1 and L8=L and C8= ‹add_mset L D'› in H)
    apply (intro conjI)
    apply (auto simp: all_conj_distrib)[4]
    apply (rule disjI2)+
    apply (rule_tac x=L in exI, rule_tac x=D in exI)
    apply (intro conjI refl)
    apply (rule_tac x=K in exI, rule_tac x=M1 in exI)
    apply auto
    apply (rule_tac x=D' in exI)
    by (auto simp: Un_assoc Un_commute ac_simps)
  done
  done
  done
qed

lemma rtranclp_cdcl⇩W_enlarge_clauses:
  assumes ‹trail T = trail S ∧ init_clss T = init_clss S + N' ∧
    learned_clss T = learned_clss S + U' ∧ conflicting T = conflicting S› and
     ‹rtranclp cdcl⇩W S S'›
  shows ‹∃T'. trail T' = trail S' ∧ init_clss T' = init_clss S' + N' ∧
    learned_clss T' = learned_clss S' + U' ∧ conflicting T' = conflicting S' ∧
    cdcl⇩W⇧*⇧* T T'›
  using assms(2,1)
  apply (induction arbitrary: T rule: rtranclp_induct)
  subgoal by auto
  subgoal premises p for T U T'
    using p(3)[of T'] p(1,2,4-)
    by (auto dest!: cdcl⇩W_enlarge_clauses[of T U _ N' U'])
  done

lemma cdcl⇩W_clauses_cong:
  assumes
    ‹cdcl⇩W S S'› and
    ‹trail T = trail S ∧ set_mset (init_clss T) = set_mset (init_clss S) ∧
    set_mset (learned_clss T) = set_mset (learned_clss S) ∧ conflicting T = conflicting S›
  shows ‹∃T'. trail T' = trail S' ∧ set_mset (init_clss T') = set_mset (init_clss S') ∧
      learned_clss T' = learned_clss T + (learned_clss S' - learned_clss S) ∧ conflicting T' = conflicting S' ∧
    cdcl⇩W T T'›
proof -
  note H = exI[of _ ‹cons_trail (Propagated L C)
        (reduce_trail_to xx_M
          (add_learned_cls _ (update_conflicting None T)))› for xx_M L C]
  show ?thesis
  using assms
  apply induction
  subgoal for S'
    by (auto simp: cdcl⇩W.simps propagate.simps clauses_def elim!: rulesE)
     (metis conflicting_cons_trail init_clss_cons_trail learned_clss_cons_trail state_eq_ref 
      trail_cons_trail)+
  subgoal for S'
    apply (auto simp: cdcl⇩W.simps conflict.simps clauses_def elim!: rulesE)
    apply (metis assms(1) conflicting_update_conflicting init_clss_update_conflicting
      learned_clss_update_conflicting state_eq_ref trail_update_conflicting)+
    done
  subgoal
    apply (induction rule: cdcl⇩W_o.induct)
  subgoal for S'
    apply (auto simp: cdcl⇩W.simps decide.simps clauses_def cdcl⇩W_o.simps elim!: rulesE)
    by (metis assms(1) conflicting_cons_trail_conflicting init_clss_cons_trail
      learned_clss_cons_trail state_eq_ref state_eq_trail trail_cons_trail)
  subgoal for S'
  apply (induction rule: cdcl⇩W_bj.induct)
  subgoal for S'
    by (auto simp: cdcl⇩W.simps skip.simps clauses_def  cdcl⇩W_o.simps cdcl⇩W_bj.simps elim!: rulesE
      intro!: exI[of _ ‹tl_trail T›])
  subgoal for S'
    apply (auto simp: cdcl⇩W.simps resolve.simps clauses_def cdcl⇩W_o.simps cdcl⇩W_bj.simps elim!: rulesE)
    by (metis conflicting_update_conflicting init_clss_tl_trail init_clss_update_conflicting learned_clss_tl_trail learned_clss_update_conflicting state_eq_ref trail_tl_trail trail_update_conflicting)
  subgoal for S'
    apply (clarsimp simp: cdcl⇩W.simps backtrack.simps clauses_def cdcl⇩W_o.simps cdcl⇩W_bj.simps)
    apply (rule_tac xx_M8=M1 and L8=L and C8= ‹add_mset L D'› in H)
    apply (intro conjI)
    apply (auto simp: all_conj_distrib)[4]
    apply (rule disjI2)+
    apply (rule_tac x=L in exI, rule_tac x=D in exI)
    apply (intro conjI refl)
    apply (rule_tac x=K in exI, rule_tac x=M1 in exI)
    apply auto
    apply (rule_tac x=D' in exI)
    by (auto simp: Un_assoc Un_commute ac_simps)
  done
  done
  done
qed

lemma cdcl⇩W_learnel_clss_mono: ‹cdcl⇩W S T ⟹ learned_clss S ⊆# learned_clss T›
  by (auto simp: cdcl⇩W.simps cdcl⇩W_o.simps cdcl⇩W_bj.simps elim!: rulesE)

lemma rtranclp_cdcl⇩W_learned_clauses_mono: ‹cdcl⇩W⇧*⇧* S T ⟹ learned_clss S ⊆# learned_clss T›
  by (induction rule: rtranclp_induct)
    (auto dest!: cdcl⇩W_learnel_clss_mono)

lemma rtranclp_cdcl⇩W_clauses_cong:
  assumes ‹trail T = trail S ∧ set_mset (init_clss T) = set_mset (init_clss S) ∧
    set_mset (learned_clss T) = set_mset (learned_clss S) ∧ conflicting T = conflicting S› and
     ‹rtranclp cdcl⇩W S S'›
  shows ‹∃T'. trail T' = trail S' ∧ set_mset (init_clss T) = set_mset (init_clss S) ∧
    learned_clss T' = learned_clss T + (learned_clss S' - learned_clss S) ∧ conflicting T' = conflicting S' ∧
    cdcl⇩W⇧*⇧* T T'›
  using assms(2,1)
  apply (induction arbitrary: T rule: rtranclp_induct)
  subgoal by auto
  subgoal premises p for T U T'
    using p(3)[of T'] p(1,2,4-) rtranclp_cdcl⇩W_learned_clauses_mono[of S T]
    apply (auto dest!: cdcl⇩W_clauses_cong[of T U])
     apply (metis rtranclp_cdcl⇩W_cdcl⇩W_restart rtranclp_cdcl⇩W_restart_init_clss)+
    apply (metis in_multiset_minus_notin_snd mset_subset_eqD mset_subset_eq_add_right
      rtranclp_cdcl⇩W_learned_clauses_mono)
   apply (rule_tac x=T'aa in exI)
   apply auto
   by (smt cdcl⇩W_learnel_clss_mono p(2) subset_mset.add_diff_assoc subset_mset.add_diff_assoc2
     subset_mset.add_diff_inverse union_assoc)
  done

lemma cdcl⇩W_all_struct_inv_clauses_cong:
  assumes
    ‹cdcl⇩W_all_struct_inv S› and
    ‹trail T = trail S ∧ set_mset (init_clss T) = set_mset (init_clss S) ∧
    set_mset (learned_clss T) = set_mset (learned_clss S) ∧ conflicting T = conflicting S›
  shows ‹cdcl⇩W_all_struct_inv T›
  using assms
  by (auto simp: cdcl⇩W_all_struct_inv_def no_strange_atm_def cdcl⇩W_M_level_inv_def
   distinct_cdcl⇩W_state_def cdcl⇩W_conflicting_def clauses_def cdcl⇩W_learned_clause_def
  reasons_in_clauses_def)
end

end