Theory CDCL.CDCL_W_Merge

(* Title: Merging some rules of Weidenbach's CDCL
    Author: Mathias Fleury <mathias.fleury@mpi-inf.mpg.de>
*)

section ‹Merging backjump rules›

theory CDCL_W_Merge
imports CDCL_W
begin

text ‹Before showing that Weidenbach's CDCL is included in NOT's CDCL, we need to work on a variant
  of Weidenbach's calculus: NOT's backjump assumes the existence of a clause that is suitable to
  backjump. This clause is obtained in W's CDCL by applying:
    ▸ @{term conflict_driven_clause_learning⇩W.conflict} to find the conflict
    ▸ the conflict is analysed by repetitive application of
      @{term conflict_driven_clause_learning⇩W.resolve} and
      @{term conflict_driven_clause_learning⇩W.skip},
    ▸ finally @{term conflict_driven_clause_learning⇩W.backtrack} is used to backtrack.

  We show that this new calculus has the same final states than Weidenbach's CDCL if the calculus
  starts in a state such that the invariant holds and no conflict has been found yet. The latter
  condition holds for initial states.›

subsection ‹Inclusion of the States›

context conflict_driven_clause_learning⇩W
begin

declare cdcl⇩W_restart.intros[intro] cdcl⇩W_bj.intros[intro] cdcl⇩W_o.intros[intro]
state_prop [simp del]

lemma backtrack_no_cdcl⇩W_bj:
  assumes cdcl: "cdcl⇩W_bj T U"
  shows "¬backtrack V T"
  using cdcl
  apply (induction rule: cdcl⇩W_bj.induct)
    apply (elim skipE, force elim!: backtrackE simp: cdcl⇩W_M_level_inv_def)
   apply (elim resolveE, force elim!: backtrackE simp: cdcl⇩W_M_level_inv_def)
  apply standard
  apply (elim backtrackE)
  apply (force simp add: cdcl⇩W_M_level_inv_decomp)
  done

text ‹@{term skip_or_resolve} corresponds to the ∗‹analyze› function in the code of MiniSAT.›
inductive skip_or_resolve :: "'st ⇒ 'st ⇒ bool" where
s_or_r_skip[intro]: "skip S T ⟹ skip_or_resolve S T" |
s_or_r_resolve[intro]: "resolve S T ⟹ skip_or_resolve S T"

lemma rtranclp_cdcl⇩W_bj_skip_or_resolve_backtrack:
  assumes "cdcl⇩W_bj⇧*⇧* S U"
  shows "skip_or_resolve⇧*⇧* S U ∨ (∃T. skip_or_resolve⇧*⇧* S T ∧ backtrack T U)"
  using assms
proof induction
  case base
  then show ?case by simp
next
  case (step U V) note st = this(1) and bj = this(2) and IH = this(3)
  consider
      (SU) "S = U"
    | (SUp) "cdcl⇩W_bj⇧+⇧+ S U"
    using st unfolding rtranclp_unfold by blast
  then show ?case
  proof cases
    case SUp
    have "⋀T. skip_or_resolve⇧*⇧* S T ⟹ cdcl⇩W_restart⇧*⇧* S T"
      using mono_rtranclp[of skip_or_resolve cdcl⇩W_restart]
      by (blast intro: skip_or_resolve.cases)
    then have "skip_or_resolve⇧*⇧* S U"
      using bj IH backtrack_no_cdcl⇩W_bj by meson
    then show ?thesis
      using bj by (auto simp: cdcl⇩W_bj.simps dest!: skip_or_resolve.intros)
  next
    case SU
    then show ?thesis
      using bj by (auto simp: cdcl⇩W_bj.simps dest!: skip_or_resolve.intros)
  qed
qed

lemma rtranclp_skip_or_resolve_rtranclp_cdcl⇩W_restart:
  "skip_or_resolve⇧*⇧* S T ⟹ cdcl⇩W_restart⇧*⇧* S T"
  by (induction rule: rtranclp_induct)
    (auto dest!: cdcl⇩W_bj.intros cdcl⇩W_restart.intros cdcl⇩W_o.intros simp: skip_or_resolve.simps)

definition backjump_l_cond :: "'v clause ⇒ 'v clause ⇒ 'v literal ⇒ 'st ⇒ 'st ⇒ bool" where
"backjump_l_cond ≡ λC C' L S T. True"

lemma wf_skip_or_resolve:
  "wf {(T, S). skip_or_resolve S T}"
proof -
  have "skip_or_resolve x y ⟹ length (trail y) < length (trail x)" for x y
    by (auto simp: skip_or_resolve.simps elim!: skipE resolveE)
  then show ?thesis
    using wfP_if_measure[of "λ_. True" skip_or_resolve "λS. length (trail S)"]
    by meson
qed

definition inv⇩N⇩O⇩T :: "'st ⇒ bool" where
"inv⇩N⇩O⇩T ≡ λS. no_dup (trail S)"

declare inv⇩N⇩O⇩T_def[simp]
end

context conflict_driven_clause_learning⇩W
begin

subsection ‹More lemmas about Conflict, Propagate and Backjumping›

subsubsection ‹Termination›

lemma cdcl⇩W_bj_measure:
  assumes "cdcl⇩W_bj S T"
  shows "length (trail S) + (if conflicting S = None then 0 else 1)
    > length (trail T) + (if conflicting T = None then 0 else 1)"
  using assms by (induction rule: cdcl⇩W_bj.induct) (force elim!: backtrackE skipE resolveE)+

lemma wf_cdcl⇩W_bj:
  "wf {(b,a). cdcl⇩W_bj a b}"
  apply (rule wfP_if_measure[of "λ_. True"
      _ "λT. length (trail T) + (if conflicting T = None then 0 else 1)", simplified])
  using cdcl⇩W_bj_measure by simp

lemma cdcl⇩W_bj_exists_normal_form:
  shows "∃T. full cdcl⇩W_bj S T"
  using wf_exists_normal_form_full[OF wf_cdcl⇩W_bj] .

lemma rtranclp_skip_state_decomp:
  assumes "skip⇧*⇧* S T"
  shows
    "∃M. trail S = M @ trail T ∧ (∀m∈set M. ¬is_decided m)"
    "init_clss S = init_clss T"
    "learned_clss S = learned_clss T"
    "backtrack_lvl S = backtrack_lvl T"
    "conflicting S = conflicting T"
  using assms by (induction rule: rtranclp_induct) (auto elim!: skipE)


subsubsection ‹Analysing is confluent›

lemma backtrack_reduce_trail_to_state_eq:
  assumes
    V_T: ‹V ∼ tl_trail T› and
    decomp: ‹(Decided K # M1, M2) ∈ set (get_all_ann_decomposition (trail V))›
  shows ‹reduce_trail_to M1 (add_learned_cls E (update_conflicting None V))
    ∼ reduce_trail_to M1 (add_learned_cls E (update_conflicting None T))›
proof -
  let ?f = ‹λT. add_learned_cls E (update_conflicting None T)›
  have [simp]: ‹length (trail T) ≠ length M1› ‹trail T ≠ []›
    using decomp V_T by (cases ‹trail T›; auto)+
  have ‹reduce_trail_to M1 (?f V) ∼ reduce_trail_to M1 (?f (tl_trail T))›
    apply (rule reduce_trail_to_state_eq)
    using V_T by (simp_all add: add_learned_cls_state_eq update_conflicting_state_eq)
  moreover {
    have ‹add_learned_cls E (update_conflicting None (tl_trail T)) ∼
      tl_trail (add_learned_cls E (update_conflicting None T))›
      apply (rule state_eq_trans[OF state_eq_sym[THEN iffD1], of
            ‹add_learned_cls E (tl_trail (update_conflicting None T))›])
       apply (auto simp: tl_trail_update_conflicting tl_trail_add_learned_cls_commute
          update_conflicting_state_eq add_learned_cls_state_eq tl_trail_state_eq; fail)[]
      apply (rule state_eq_trans[OF state_eq_sym[THEN iffD1], of
            ‹add_learned_cls E (tl_trail (update_conflicting None T))›])
       apply (auto simp: tl_trail_update_conflicting tl_trail_add_learned_cls_commute
          update_conflicting_state_eq add_learned_cls_state_eq tl_trail_state_eq; fail)[]
      apply (rule state_eq_trans[OF state_eq_sym[THEN iffD1], of
            ‹tl_trail (add_learned_cls E (update_conflicting None T))›])
       apply (auto simp: tl_trail_update_conflicting tl_trail_add_learned_cls_commute
          update_conflicting_state_eq add_learned_cls_state_eq tl_trail_state_eq)
      done
    note _ = reduce_trail_to_state_eq[OF this, of M1 M1]}
  ultimately show ‹reduce_trail_to M1 (?f V) ∼ reduce_trail_to M1 (?f T)›
    by (subst (2) reduce_trail_to.simps)
      (auto simp: tl_trail_update_conflicting tl_trail_add_learned_cls_commute intro: state_eq_trans)
qed

lemma rtranclp_skip_backtrack_reduce_trail_to_state_eq:
  assumes
    V_T: ‹skip⇧*⇧* T V› and
    decomp: ‹(Decided K # M1, M2) ∈ set (get_all_ann_decomposition (trail V))›
  shows ‹reduce_trail_to M1 (add_learned_cls E (update_conflicting None T))
    ∼ reduce_trail_to M1 (add_learned_cls E (update_conflicting None V))›
  using V_T decomp
proof (induction arbitrary: M2 rule: rtranclp_induct)
  case base
  then show ?case by auto
next
  case (step U V) note st = this(1) and skip = this(2) and IH = this(3) and decomp = this(4)
  obtain M2' where
    decomp': ‹(Decided K # M1, M2') ∈ set (get_all_ann_decomposition (trail U))›
    using get_all_ann_decomposition_exists_prepend[OF decomp] skip
    by atomize (auto elim!: rulesE simp del: get_all_ann_decomposition.simps
        simp: Decided_cons_in_get_all_ann_decomposition_append_Decided_cons
        append_Cons[symmetric] append_assoc[symmetric]
        simp del: append_Cons append_assoc)
  show ?case
    using backtrack_reduce_trail_to_state_eq[OF _ decomp, of U E] skip IH[OF decomp']
    by (auto elim!: skipE simp del: get_all_ann_decomposition.simps intro: state_eq_trans')
qed

paragraph ‹Backjumping after skipping or jump directly›
lemma rtranclp_skip_backtrack_backtrack:
  assumes
    "skip⇧*⇧* S T" and
    "backtrack T W" and
    "cdcl⇩W_all_struct_inv S"
  shows "backtrack S W"
  using assms
proof induction
  case base
  then show ?case by simp
next
  case (step T V) note st = this(1) and skip = this(2) and IH = this(3) and bt = this(4) and
    inv = this(5)
  have "skip⇧*⇧* S V"
    using st skip by auto
  then have "cdcl⇩W_all_struct_inv V"
    using rtranclp_mono[of skip cdcl⇩W_restart] assms(3) rtranclp_cdcl⇩W_all_struct_inv_inv mono_rtranclp
    by (auto dest!: bj other cdcl⇩W_bj.skip)
  then have "cdcl⇩W_M_level_inv V"
    unfolding cdcl⇩W_all_struct_inv_def by auto
  then obtain K i M1 M2 L D D' where
    conf: "conflicting V = Some (add_mset L D)" and
    decomp: "(Decided K # M1, M2) ∈ set (get_all_ann_decomposition (trail V))" and
    lev_L: "get_level (trail V) L = backtrack_lvl V" and
    max: "get_level (trail V) L = get_maximum_level (trail V) (add_mset L D')" and
    max_D: "get_maximum_level (trail V) D' ≡ i" and
    lev_k: "get_level (trail V) K = Suc i" and
    W: "W ∼ cons_trail (Propagated L (add_mset L D'))
                (reduce_trail_to M1
                  (add_learned_cls (add_mset L D')
                    (update_conflicting None V)))" and
    D_D': ‹D' ⊆# D› and
    NU_D': ‹clauses V ⊨pm add_mset L D'›
    using bt inv by (elim backtrackE) metis
  obtain L' C' M E where
    tr: "trail T = Propagated L' C' # M" and
    raw: "conflicting T = Some E" and
    LE: "-L' ∉# E" and
    E: "E ≠ {#}" and
    V: "V ∼ tl_trail T"
    using skip by (elim skipE) metis
  let ?M = "Propagated L' C' # M"
  have tr_M: "trail T = ?M"
    using tr V by auto
  have MT: "M = tl (trail T)" and MV: "M = trail V"
    using tr V by auto
  have DE[simp]: "E = add_mset L D"
    using V conf raw by auto
  have "cdcl⇩W_restart⇧*⇧* S T"
    using bj cdcl⇩W_bj.skip mono_rtranclp[of skip cdcl⇩W_restart S T] other st by meson
  then have inv': "cdcl⇩W_all_struct_inv T"
    using rtranclp_cdcl⇩W_all_struct_inv_inv inv by blast
  have M_lev: "cdcl⇩W_M_level_inv T" using inv' unfolding cdcl⇩W_all_struct_inv_def by auto
  then have n_d': "no_dup ?M"
    using tr_M unfolding cdcl⇩W_M_level_inv_def by auto
  let ?k = "backtrack_lvl T"
  have [simp]:
    "backtrack_lvl V = ?k"
    using V tr_M by simp
  have "?k > 0"
    using decomp M_lev V tr unfolding cdcl⇩W_M_level_inv_def by auto
  then have "atm_of L ∈ atm_of ` lits_of_l (trail V)"
    using lev_L get_level_ge_0_atm_of_in[of 0 "trail V" L] by auto
  then have L_L': "atm_of L ≠ atm_of L'"
    using n_d' unfolding lits_of_def MV by (auto simp: defined_lit_map)
  have L'_M: "undefined_lit M L'"
    using n_d' unfolding lits_of_def by auto
  have "?M ⊨as CNot D"
    using inv' raw unfolding cdcl⇩W_conflicting_def cdcl⇩W_all_struct_inv_def tr_M by auto
  then have "L' ∉# D"
    using L_L' L'_M unfolding true_annots_true_cls true_clss_def
    by (auto simp: uminus_lit_swap atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set defined_lit_map
      lits_of_def dest!: in_diffD)
  have [simp]: "trail (reduce_trail_to M1 T) = M1"
    using decomp tr W V by auto
  have "skip⇧*⇧* S V"
    using st skip by auto
  have "no_dup (trail S)"
    using inv unfolding cdcl⇩W_all_struct_inv_def cdcl⇩W_M_level_inv_def by auto
  then have [simp]: "init_clss S = init_clss V" and [simp]: "learned_clss S = learned_clss V"
    using rtranclp_skip_state_decomp[OF ‹skip⇧*⇧* S V›] V by auto
  have V_T: ‹V ∼ tl_trail T›
    using skip by (auto elim: rulesE)
  have
    W_S: "W ∼ cons_trail (Propagated L (add_mset L D')) (reduce_trail_to M1
     (add_learned_cls (add_mset L D') (update_conflicting None T)))"
    apply (rule state_eq_trans[OF W])
    unfolding DE
    apply (rule cons_trail_state_eq)
    apply (rule backtrack_reduce_trail_to_state_eq)
    using V decomp by auto
  have atm_of_L'_D': "atm_of L' ∉ atms_of D'"
    by (metis DE LE ‹D' ⊆# D› ‹L' ∉# D› atm_of_in_atm_of_set_in_uminus atms_of_def insert_iff
        mset_subset_eqD set_mset_add_mset_insert)

  obtain M2' where
    decomp': "(Decided K # M1, M2') ∈ set (get_all_ann_decomposition (trail T))"
    using decomp V unfolding tr_M MV by (cases "hd (get_all_ann_decomposition (trail V))",
      cases "get_all_ann_decomposition (trail V)") auto
  moreover from L_L' have "get_level ?M L = ?k"
      using lev_L V tr_M by (auto split: if_split_asm)
  moreover have "get_level ?M L = get_maximum_level ?M (add_mset L D')"
    using count_decided_ge_get_maximum_level[of ‹trail V› D'] calculation(2) lev_L max MV atm_of_L'_D'
    unfolding get_maximum_level_add_mset
    by auto
  moreover have "i = get_maximum_level ?M D'"
    using max_D MV atm_of_L'_D' by auto
  moreover have "atm_of L' ≠ atm_of K"
    using inv' get_all_ann_decomposition_exists_prepend[OF decomp]
    unfolding cdcl⇩W_all_struct_inv_def cdcl⇩W_M_level_inv_def tr MV by (auto simp: defined_lit_map)
  ultimately have "backtrack T W"
    apply -
    apply (rule backtrack_rule[of T L D K M1 M2' D' i])
    unfolding tr_M[symmetric]
    subgoal using raw by (simp; fail)
    subgoal by (simp; fail)
    subgoal by (simp; fail)
    subgoal by (simp; fail)
    subgoal by (simp; fail)
    subgoal using lev_k tr unfolding MV[symmetric] by (auto; fail)[]
    subgoal using D_D' by (simp; fail)
    subgoal using NU_D' V_T by (simp; fail)
    subgoal using W_S lev_k by (auto; fail)[]
    done
  then show ?thesis using IH inv by blast
qed


text ‹See also theorem @{thm [source] rtranclp_skip_backtrack_backtrack}›
lemma rtranclp_skip_backtrack_backtrack_end:
  assumes
    skip: "skip⇧*⇧* S T" and
    bt: "backtrack S W" and
    inv: "cdcl⇩W_all_struct_inv S"
  shows "backtrack T W"
  using assms
proof -
  have M_lev: "cdcl⇩W_M_level_inv S "
    using bt inv unfolding cdcl⇩W_all_struct_inv_def by (auto elim!: backtrackE)
  then obtain K i M1 M2 L D D' where
    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
    lev_l_D: "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 = Suc i" and
    W: "W ∼ 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
    NU_D': ‹clauses S ⊨pm add_mset L D'›
    using bt by (elim backtrackE) metis
  let ?D = "add_mset L D"
  let ?D' = "add_mset L D'"

  have [simp]: "no_dup (trail S)"
    using M_lev by (auto simp: cdcl⇩W_M_level_inv_decomp)
  have "cdcl⇩W_all_struct_inv T"
    using mono_rtranclp[of skip cdcl⇩W_restart] by (smt bj cdcl⇩W_bj.skip inv local.skip other
      rtranclp_cdcl⇩W_all_struct_inv_inv)
  then have [simp]: "no_dup (trail T)"
    unfolding cdcl⇩W_all_struct_inv_def cdcl⇩W_M_level_inv_def by auto
  (* M⇩T is a proxy to allow auto to unfold T*)
  obtain MS M⇩T where M: "trail S = MS @ M⇩T" and M⇩T: "M⇩T = trail T" and nm: "∀m∈set MS. ¬is_decided m"
    using rtranclp_skip_state_decomp(1)[OF skip] S by auto
  have T: "state_butlast T = (M⇩T, init_clss S, learned_clss S, Some (add_mset L D))" and
    bt_S_T: "backtrack_lvl S = backtrack_lvl T" and
    clss_S_T: ‹clauses S = clauses T›
    using M⇩T rtranclp_skip_state_decomp[of S T] skip S by (auto simp: clauses_def)

  have "cdcl⇩W_all_struct_inv T"
    apply (rule rtranclp_cdcl⇩W_all_struct_inv_inv[OF _ inv])
    using bj cdcl⇩W_bj.skip local.skip other rtranclp_mono[of skip cdcl⇩W_restart] by blast
  then have "M⇩T ⊨as CNot ?D"
    unfolding cdcl⇩W_all_struct_inv_def cdcl⇩W_conflicting_def using T by auto
  then have "∀L'∈#?D. defined_lit M⇩T L'"
    using Decided_Propagated_in_iff_in_lits_of_l
    by (auto dest: true_annots_CNot_definedD)
  moreover have "no_dup (trail S)"
    using inv unfolding cdcl⇩W_all_struct_inv_def cdcl⇩W_M_level_inv_def by auto
  ultimately have undef_D: "∀L'∈#?D. undefined_lit MS L'"
    unfolding M by (auto dest: defined_lit_no_dupD)
  then have H: "⋀L'. L'∈# D ⟹ get_level (trail S) L' = get_level M⇩T L'"
     "get_level (trail S) L = get_level M⇩T L"
    unfolding M by (auto simp: lits_of_def)
  have [simp]: "get_maximum_level (trail S) D = get_maximum_level M⇩T D"
    using ‹M⇩T ⊨as CNot (add_mset L D)› M nm undef_D by (auto simp: get_maximum_level_skip_beginning)

  have lev_l': "get_level M⇩T L = backtrack_lvl S"
    using lev_l nm by (auto simp: H)
  have [simp]: "trail (reduce_trail_to M1 T) = M1"
    by (metis (no_types) M M⇩T append_assoc get_all_ann_decomposition_exists_prepend[OF decomp] nm
        reduce_trail_to_trail_tl_trail_decomp beginning_not_decided_invert)
  obtain c where c: ‹M⇩T = c @ Decided K # M1›
    using nm decomp by (auto dest!: get_all_ann_decomposition_exists_prepend
        simp: M⇩T[symmetric] M append_assoc[symmetric]
        simp del: append_assoc
        dest!: beginning_not_decided_invert)
  obtain c'' where
    c'': ‹(Decided K # M1, c'') ∈ set (get_all_ann_decomposition (c @ Decided K # M1))›
    using Decided_cons_in_get_all_ann_decomposition_append_Decided_cons[of K M1]  by blast
  have W: "W ∼ cons_trail (Propagated L (add_mset L D')) (reduce_trail_to M1
    (add_learned_cls (add_mset L D') (update_conflicting None T)))"
    apply (rule state_eq_trans[OF W])
    apply (rule cons_trail_state_eq)
    apply (rule rtranclp_skip_backtrack_reduce_trail_to_state_eq[of _ _ K M1])
    using skip apply (simp; fail)
    using c'' by (auto simp: M⇩T[symmetric] M c)
  have max_trail_S_MT_L_D': ‹get_maximum_level (trail S) ?D' = get_maximum_level M⇩T ?D'›
    by (rule get_maximum_level_cong) (use H D_D' in auto)
  then have lev_l_D': "get_level M⇩T L = get_maximum_level M⇩T ?D'"
    using lev_l_D H by auto
  have i': "i = get_maximum_level M⇩T D'"
    unfolding i[symmetric]
    by (rule get_maximum_level_cong) (use H D_D' in auto)
  have "Decided K # M1 ∈ set (map fst (get_all_ann_decomposition (trail S)))"
    using Set.imageI[OF decomp, of fst] by auto
  then have "Decided K # M1 ∈ set (map fst (get_all_ann_decomposition M⇩T))"
    using fst_get_all_ann_decomposition_prepend_not_decided[OF nm] unfolding M by auto
  then obtain M2' where decomp': "(Decided K # M1, M2') ∈ set (get_all_ann_decomposition M⇩T)"
    by auto
  moreover {
    have "undefined_lit MS K"
      using ‹no_dup (trail S)› decomp' unfolding M M⇩T
      by (auto simp: lits_of_def defined_lit_map no_dup_def)
    then have "get_level (trail T) K = get_level (trail S) K"
      unfolding M M⇩T by auto }
  ultimately show "backtrack T W"
    apply -
    apply (rule backtrack.intros[of T L D K M1 M2' D' i])
    subgoal using T by auto
    subgoal using T by auto
    subgoal using T lev_l' lev_l_D' bt_S_T by auto
    subgoal using T lev_l_D' bt_S_T by auto
    subgoal using i' W lev_K unfolding M⇩T[symmetric] clss_S_T by auto
    subgoal using lev_K unfolding M⇩T[symmetric] clss_S_T by auto
    subgoal using D_D' .
    subgoal using NU_D' unfolding clss_S_T .
    subgoal using W unfolding i'[symmetric] by auto
    done
qed

lemma cdcl⇩W_bj_decomp_resolve_skip_and_bj:
  assumes "cdcl⇩W_bj⇧*⇧* S T"
  shows "(skip_or_resolve⇧*⇧* S T
    ∨ (∃U. skip_or_resolve⇧*⇧* S U ∧ backtrack U T))"
  using assms
proof induction
  case base
  then show ?case by simp
next
  case (step T U) note st = this(1) and bj = this(2) and IH = this(3)
  have IH: "skip_or_resolve⇧*⇧* S T"
  proof -
    { assume "∃U. skip_or_resolve⇧*⇧* S U ∧ backtrack U T"
      then obtain V where
        bt: "backtrack V T" and
        "skip_or_resolve⇧*⇧* S V"
        by blast
      then have "cdcl⇩W_restart⇧*⇧* S V"
        using rtranclp_skip_or_resolve_rtranclp_cdcl⇩W_restart by blast
      with bj bt have False using backtrack_no_cdcl⇩W_bj by simp
    }
    then show ?thesis using IH by blast
  qed
  show ?case
    using bj
    proof (cases rule: cdcl⇩W_bj.cases)
      case backtrack
      then show ?thesis using IH by blast
    qed (metis (no_types, lifting) IH rtranclp.simps skip_or_resolve.simps)+
qed


subsection ‹CDCL with Merging›

inductive cdcl⇩W_merge_restart :: "'st ⇒ 'st ⇒ bool" where
fw_r_propagate: "propagate S S' ⟹ cdcl⇩W_merge_restart S S'" |
fw_r_conflict: "conflict S T ⟹ full cdcl⇩W_bj T U ⟹ cdcl⇩W_merge_restart S U" |
fw_r_decide: "decide S S' ⟹ cdcl⇩W_merge_restart S S'"|
fw_r_rf: "cdcl⇩W_rf S S' ⟹ cdcl⇩W_merge_restart S S'"

lemma rtranclp_cdcl⇩W_bj_rtranclp_cdcl⇩W_restart:
  "cdcl⇩W_bj⇧*⇧* S T ⟹ cdcl⇩W_restart⇧*⇧* S T"
  using mono_rtranclp[of cdcl⇩W_bj cdcl⇩W_restart] by blast

lemma cdcl⇩W_merge_restart_cdcl⇩W_restart:
  assumes "cdcl⇩W_merge_restart S T"
  shows "cdcl⇩W_restart⇧*⇧* S T"
  using assms
proof induction
  case (fw_r_conflict S T U) note confl = this(1) and bj = this(2)
  have "cdcl⇩W_restart S T" using confl by (simp add: cdcl⇩W_restart.intros r_into_rtranclp)
  moreover
    have "cdcl⇩W_bj⇧*⇧* T U" using bj unfolding full_def by auto
    then have "cdcl⇩W_restart⇧*⇧* T U" using rtranclp_cdcl⇩W_bj_rtranclp_cdcl⇩W_restart by blast
  ultimately show ?case by auto
qed (simp_all add: cdcl⇩W_o.intros cdcl⇩W_restart.intros r_into_rtranclp)

lemma cdcl⇩W_merge_restart_conflicting_true_or_no_step:
  assumes "cdcl⇩W_merge_restart S T"
  shows "conflicting T = None ∨ no_step cdcl⇩W_restart T"
  using assms
proof induction
  case (fw_r_conflict S T U) note confl = this(1) and n_s = this(2)
  { fix D V
    assume "cdcl⇩W_restart U V" and "conflicting U = Some D"
    then have False
      using n_s unfolding full_def
      by (induction rule: cdcl⇩W_restart_all_rules_induct)
        (auto dest!: cdcl⇩W_bj.intros elim: decideE propagateE conflictE forgetE restartE)
  }
  then show ?case by (cases "conflicting U") fastforce+
qed (auto simp add: cdcl⇩W_rf.simps elim: propagateE decideE restartE forgetE)

inductive cdcl⇩W_merge :: "'st ⇒ 'st ⇒ bool" where
fw_propagate: "propagate S S' ⟹ cdcl⇩W_merge S S'" |
fw_conflict: "conflict S T ⟹ full cdcl⇩W_bj T U ⟹ cdcl⇩W_merge S U" |
fw_decide: "decide S S' ⟹ cdcl⇩W_merge S S'"|
fw_forget: "forget S S' ⟹ cdcl⇩W_merge S S'"

lemma cdcl⇩W_merge_cdcl⇩W_merge_restart:
  "cdcl⇩W_merge S T ⟹ cdcl⇩W_merge_restart S T"
  by (meson cdcl⇩W_merge.cases cdcl⇩W_merge_restart.simps forget)

lemma rtranclp_cdcl⇩W_merge_tranclp_cdcl⇩W_merge_restart:
  "cdcl⇩W_merge⇧*⇧* S T ⟹ cdcl⇩W_merge_restart⇧*⇧* S T"
  using rtranclp_mono[of cdcl⇩W_merge cdcl⇩W_merge_restart] cdcl⇩W_merge_cdcl⇩W_merge_restart by blast

lemma cdcl⇩W_merge_rtranclp_cdcl⇩W_restart:
  "cdcl⇩W_merge S T ⟹ cdcl⇩W_restart⇧*⇧* S T"
  using cdcl⇩W_merge_cdcl⇩W_merge_restart cdcl⇩W_merge_restart_cdcl⇩W_restart by blast

lemma rtranclp_cdcl⇩W_merge_rtranclp_cdcl⇩W_restart:
  "cdcl⇩W_merge⇧*⇧* S T ⟹ cdcl⇩W_restart⇧*⇧* S T"
  using rtranclp_mono[of cdcl⇩W_merge "cdcl⇩W_restart⇧*⇧*"] cdcl⇩W_merge_rtranclp_cdcl⇩W_restart by auto

lemma cdcl⇩W_all_struct_inv_tranclp_cdcl⇩W_merge_tranclp_cdcl⇩W_merge_cdcl⇩W_all_struct_inv:
  assumes
    inv: "cdcl⇩W_all_struct_inv b"
    "cdcl⇩W_merge⇧+⇧+ b a"
  shows "(λS T. cdcl⇩W_all_struct_inv S ∧ cdcl⇩W_merge S T)⇧+⇧+ b a"
  using assms(2)
proof induction
  case base
  then show ?case using inv by auto
next
  case (step c d) note st = this(1) and fw = this(2) and IH = this(3)
  have "cdcl⇩W_all_struct_inv c"
    using tranclp_into_rtranclp[OF st] cdcl⇩W_merge_rtranclp_cdcl⇩W_restart assms(1)
    rtranclp_cdcl⇩W_all_struct_inv_inv rtranclp_mono[of cdcl⇩W_merge "cdcl⇩W_restart⇧*⇧*"] by fastforce
  then have "(λS T. cdcl⇩W_all_struct_inv S ∧ cdcl⇩W_merge S T)⇧+⇧+ c d"
    using fw by auto
  then show ?case using IH by auto
qed

lemma backtrack_is_full1_cdcl⇩W_bj:
  assumes bt: "backtrack S T"
  shows "full1 cdcl⇩W_bj S T"
  using bt backtrack_no_cdcl⇩W_bj unfolding full1_def by blast

lemma rtrancl_cdcl⇩W_conflicting_true_cdcl⇩W_merge_restart:
  assumes "cdcl⇩W_restart⇧*⇧* S V" and inv: "cdcl⇩W_M_level_inv S" and "conflicting S = None"
  shows "(cdcl⇩W_merge_restart⇧*⇧* S V ∧ conflicting V = None)
    ∨ (∃T U. cdcl⇩W_merge_restart⇧*⇧* S T ∧ conflicting V ≠ None ∧ conflict T U ∧ cdcl⇩W_bj⇧*⇧* U V)"
  using assms
proof induction
  case base
  then show ?case by simp
next
  case (step U V) note st = this(1) and cdcl⇩W_restart = this(2) and IH = this(3)[OF this(4-)] and
    confl[simp] = this(5) and inv = this(4)
  from cdcl⇩W_restart
  show ?case
  proof cases
    case propagate
    moreover have "conflicting U = None" and "conflicting V = None"
      using propagate propagate by (auto elim: propagateE)
    ultimately show ?thesis using IH cdcl⇩W_merge_restart.fw_r_propagate[of U V] by auto
  next
    case conflict
    moreover have "conflicting U = None" and "conflicting V ≠ None"
      using conflict by (auto elim!: conflictE)
    ultimately show ?thesis using IH by auto
  next
    case other
    then show ?thesis
    proof cases
      case decide
      then show ?thesis using IH cdcl⇩W_merge_restart.fw_r_decide[of U V] by (auto elim: decideE)
    next
      case bj
      then consider
        (s_or_r) "skip_or_resolve U V" |
        (bt) "backtrack U V"
        by (auto simp: cdcl⇩W_bj.simps)
      then show ?thesis
      proof cases
        case s_or_r
        have f1: "cdcl⇩W_bj⇧+⇧+ U V"
          by (simp add: local.bj tranclp.r_into_trancl)
        obtain T T' :: 'st where
          f2: "cdcl⇩W_merge_restart⇧*⇧* S U
                ∨ cdcl⇩W_merge_restart⇧*⇧* S T ∧ conflicting U ≠ None
                  ∧ conflict T T' ∧ cdcl⇩W_bj⇧*⇧* T' U"
          using IH confl by blast
        have "conflicting V ≠ None ∧ conflicting U ≠ None"
          using ‹skip_or_resolve U V›
          by (auto simp: skip_or_resolve.simps elim!: skipE resolveE)
        then show ?thesis
          by (metis (full_types) IH f1 rtranclp_trans tranclp_into_rtranclp)
      next
        case bt
        then have "conflicting U ≠ None" by (auto elim: backtrackE)
        then obtain T T' where
          "cdcl⇩W_merge_restart⇧*⇧* S T" and
          "conflicting U ≠ None" and
          "conflict T T'" and
          "cdcl⇩W_bj⇧*⇧* T' U"
          using IH confl by meson
        have invU: "cdcl⇩W_M_level_inv U"
          using inv rtranclp_cdcl⇩W_restart_consistent_inv step.hyps(1) by blast
        then have "conflicting V = None"
          using ‹backtrack U V› inv by (auto elim: backtrackE simp: cdcl⇩W_M_level_inv_decomp)
        have "full cdcl⇩W_bj T' V"
          apply (rule rtranclp_fullI[of cdcl⇩W_bj T' U V])
          using ‹cdcl⇩W_bj⇧*⇧* T' U› apply fast
          using ‹backtrack U V› backtrack_is_full1_cdcl⇩W_bj invU unfolding full1_def full_def
          by blast
        then show ?thesis
          using cdcl⇩W_merge_restart.fw_r_conflict[of T T' V] ‹conflict T T'›
            ‹cdcl⇩W_merge_restart⇧*⇧* S T› ‹conflicting V = None› by auto
      qed
    qed
  next
    case rf
    moreover have "conflicting U = None" and "conflicting V = None"
      using rf by (auto simp: cdcl⇩W_rf.simps elim: restartE forgetE)
    ultimately show ?thesis using IH cdcl⇩W_merge_restart.fw_r_rf[of U V] by auto
  qed
qed

lemma no_step_cdcl⇩W_restart_no_step_cdcl⇩W_merge_restart:
  "no_step cdcl⇩W_restart S ⟹ no_step cdcl⇩W_merge_restart S"
  by (auto simp: cdcl⇩W_restart.simps cdcl⇩W_merge_restart.simps cdcl⇩W_o.simps cdcl⇩W_bj.simps)

lemma no_step_cdcl⇩W_merge_restart_no_step_cdcl⇩W_restart:
  assumes
    "conflicting S = None" and
    "cdcl⇩W_M_level_inv S" and
    "no_step cdcl⇩W_merge_restart S"
  shows "no_step cdcl⇩W_restart S"
proof -
  { fix S'
    assume "conflict S S'"
    then have "cdcl⇩W_restart S S'" using cdcl⇩W_restart.conflict by auto
    then have "cdcl⇩W_M_level_inv S'"
      using assms(2) cdcl⇩W_restart_consistent_inv by blast
    then obtain S'' where "full cdcl⇩W_bj S' S''"
      using cdcl⇩W_bj_exists_normal_form[of S'] by auto
    then have False
      using ‹conflict S S'› assms(3) fw_r_conflict by blast
  }
  then show ?thesis
    using assms unfolding cdcl⇩W_restart.simps cdcl⇩W_merge_restart.simps cdcl⇩W_o.simps cdcl⇩W_bj.simps
    by (auto elim: skipE resolveE backtrackE conflictE decideE restartE)
qed

lemma cdcl⇩W_merge_restart_no_step_cdcl⇩W_bj:
  assumes
    "cdcl⇩W_merge_restart S T"
  shows "no_step cdcl⇩W_bj T"
  using assms
  by (induction rule: cdcl⇩W_merge_restart.induct)
   (force simp: cdcl⇩W_bj.simps cdcl⇩W_rf.simps cdcl⇩W_merge_restart.simps full_def
     elim!: rulesE)+

lemma rtranclp_cdcl⇩W_merge_restart_no_step_cdcl⇩W_bj:
  assumes
    "cdcl⇩W_merge_restart⇧*⇧* S T" and
    "conflicting S = None"
  shows "no_step cdcl⇩W_bj T"
  using assms unfolding rtranclp_unfold
  apply (elim disjE)
   apply (force simp: cdcl⇩W_bj.simps cdcl⇩W_rf.simps elim!: rulesE)
  by (auto simp: tranclp_unfold_end simp: cdcl⇩W_merge_restart_no_step_cdcl⇩W_bj)

text ‹If @{term "conflicting S ≠ None"}, we cannot say anything.

  Remark that this theorem does not say anything about well-foundedness: even if you know that one
  relation is well-founded, it only states that the normal forms are shared.
  ›
lemma conflicting_true_full_cdcl⇩W_restart_iff_full_cdcl⇩W_merge:
  assumes confl: "conflicting S = None" and lev: "cdcl⇩W_M_level_inv S"
  shows "full cdcl⇩W_restart S V ⟷ full cdcl⇩W_merge_restart S V"
proof
  assume full: "full cdcl⇩W_merge_restart S V"
  then have st: "cdcl⇩W_restart⇧*⇧* S V"
    using rtranclp_mono[of cdcl⇩W_merge_restart "cdcl⇩W_restart⇧*⇧*"] cdcl⇩W_merge_restart_cdcl⇩W_restart
    unfolding full_def by auto

  have n_s: "no_step cdcl⇩W_merge_restart V"
    using full unfolding full_def by auto
  have n_s_bj: "no_step cdcl⇩W_bj V"
    using rtranclp_cdcl⇩W_merge_restart_no_step_cdcl⇩W_bj confl full unfolding full_def by auto
  have "⋀S'. conflict V S' ⟹ cdcl⇩W_M_level_inv S'"
    using cdcl⇩W_restart.conflict cdcl⇩W_restart_consistent_inv lev rtranclp_cdcl⇩W_restart_consistent_inv st by blast
  then have "⋀S'. conflict V S' ⟹ False"
    using n_s n_s_bj cdcl⇩W_bj_exists_normal_form cdcl⇩W_merge_restart.simps by meson
  then have n_s_cdcl⇩W_restart: "no_step cdcl⇩W_restart V"
    using n_s n_s_bj by (auto simp: cdcl⇩W_restart.simps cdcl⇩W_o.simps cdcl⇩W_merge_restart.simps)
  then show "full cdcl⇩W_restart S V" using st unfolding full_def by auto
next
  assume full: "full cdcl⇩W_restart S V"
  have "no_step cdcl⇩W_merge_restart V"
    using full no_step_cdcl⇩W_restart_no_step_cdcl⇩W_merge_restart unfolding full_def by blast
  moreover {
    consider
      (fw) "cdcl⇩W_merge_restart⇧*⇧* S V" and "conflicting V = None" |
      (bj) T U where
        "cdcl⇩W_merge_restart⇧*⇧* S T" and
        "conflicting V ≠ None" and
        "conflict T U" and
        "cdcl⇩W_bj⇧*⇧* U V"
      using full rtrancl_cdcl⇩W_conflicting_true_cdcl⇩W_merge_restart confl lev unfolding full_def
      by meson
    then have "cdcl⇩W_merge_restart⇧*⇧* S V"
    proof cases
      case fw
      then show ?thesis by fast
    next
      case (bj T U)
      have "no_step cdcl⇩W_bj V"
        using full unfolding full_def by (meson cdcl⇩W_o.bj other)
      then have "full cdcl⇩W_bj U V"
        using ‹ cdcl⇩W_bj⇧*⇧* U V› unfolding full_def by auto
      then have "cdcl⇩W_merge_restart T V"
        using ‹conflict T U› cdcl⇩W_merge_restart.fw_r_conflict by blast
      then show ?thesis using ‹cdcl⇩W_merge_restart⇧*⇧* S T› by auto
    qed }
  ultimately show "full cdcl⇩W_merge_restart S V" unfolding full_def by fast
qed

lemma init_state_true_full_cdcl⇩W_restart_iff_full_cdcl⇩W_merge:
  shows "full cdcl⇩W_restart (init_state N) V ⟷ full cdcl⇩W_merge_restart (init_state N) V"
  by (rule conflicting_true_full_cdcl⇩W_restart_iff_full_cdcl⇩W_merge) auto


subsection ‹CDCL with Merge and Strategy›

subsubsection ‹The intermediate step›

inductive cdcl⇩W_s' :: "'st ⇒ 'st ⇒ bool" for S :: 'st where
conflict': "conflict S S' ⟹ cdcl⇩W_s' S S'" |
propagate': "propagate S S' ⟹ cdcl⇩W_s' S S'" |
decide': "no_step conflict S ⟹ no_step propagate S ⟹ decide S S' ⟹ cdcl⇩W_s' S S'" |
bj': "full1 cdcl⇩W_bj S S' ⟹ cdcl⇩W_s' S S'"

inductive_cases cdcl⇩W_s'E: "cdcl⇩W_s' S T"

lemma rtranclp_cdcl⇩W_bj_full1_cdclp_cdcl⇩W_stgy:
  "cdcl⇩W_bj⇧*⇧* S S' ⟹ cdcl⇩W_stgy⇧*⇧* S S'"
proof (induction rule: converse_rtranclp_induct)
  case base
  then show ?case by simp
next
  case (step T U) note st = this(2) and bj = this(1) and IH = this(3)
  have n_s: "no_step conflict T" "no_step propagate T"
    using bj by (auto simp add: cdcl⇩W_bj.simps elim!: rulesE)
  consider
      (U) "U = S'"
    | (U') U' where "cdcl⇩W_bj U U'" and "cdcl⇩W_bj⇧*⇧* U' S'"
    using st by (metis converse_rtranclpE)
  then show ?case
  proof cases
    case U
    then show ?thesis
      using n_s cdcl⇩W_o.bj local.bj other' by (meson r_into_rtranclp)
  next
    case U' note U' = this(1)
    have "no_step conflict U" "no_step propagate U"
      using U' by (fastforce simp: cdcl⇩W_bj.simps elim!: rulesE)+
    then have "cdcl⇩W_stgy T U"
      using n_s cdcl⇩W_stgy.simps local.bj cdcl⇩W_o.bj by meson
    then show ?thesis using IH by auto
  qed
qed

lemma cdcl⇩W_s'_is_rtranclp_cdcl⇩W_stgy:
  "cdcl⇩W_s' S T ⟹ cdcl⇩W_stgy⇧*⇧* S T"
  by (induction rule: cdcl⇩W_s'.induct)
    (auto simp: full1_def
     dest: tranclp_into_rtranclp rtranclp_cdcl⇩W_bj_full1_cdclp_cdcl⇩W_stgy cdcl⇩W_stgy.intros)

lemma cdcl⇩W_stgy_cdcl⇩W_s'_no_step:
  assumes "cdcl⇩W_stgy S U" and "cdcl⇩W_all_struct_inv S" and "no_step cdcl⇩W_bj U"
  shows "cdcl⇩W_s' S U"
  using assms apply (cases rule: cdcl⇩W_stgy.cases)
  using bj'[of S U] by (auto intro: cdcl⇩W_s'.intros simp: cdcl⇩W_o.simps full1_def)

lemma rtranclp_cdcl⇩W_stgy_connected_to_rtranclp_cdcl⇩W_s':
  assumes "cdcl⇩W_stgy⇧*⇧* S U" and inv: "cdcl⇩W_M_level_inv S"
  shows "cdcl⇩W_s'⇧*⇧* S U ∨ (∃T. cdcl⇩W_s'⇧*⇧* S T ∧ cdcl⇩W_bj⇧+⇧+ T U ∧ conflicting U ≠ None)"
  using assms(1)
proof induction
  case base
  then show ?case by simp
next
  case (step T V) note st = this(1) and o = this(2) and IH = this(3)
  from o show ?case
  proof cases
    case conflict'
    then have "cdcl⇩W_s'⇧*⇧* S T"
      using IH by (auto elim: conflictE)
    moreover have f2: "cdcl⇩W_s'⇧*⇧* T V"
      using cdcl⇩W_s'.conflict' conflict' by blast
    ultimately show ?thesis by auto
  next
    case propagate'
    then have "cdcl⇩W_s'⇧*⇧* S T"
      using IH by (auto elim: propagateE)
    moreover have f2: "cdcl⇩W_s'⇧*⇧* T V"
      using cdcl⇩W_s'.propagate' propagate' by blast
    ultimately show ?thesis by auto
  next
    case other' note o = this(3) and n_s = this(1,2) and full = this(3)
    then show ?thesis
      using o
    proof (cases rule: cdcl⇩W_o_rule_cases)
      case decide
      then have "cdcl⇩W_s'⇧*⇧* S T"
        using IH by (auto elim: rulesE)
      then show ?thesis
        by (meson decide decide' full n_s rtranclp.rtrancl_into_rtrancl)
    next
      case backtrack
      consider
        (s') "cdcl⇩W_s'⇧*⇧* S T" |
        (bj) S' where "cdcl⇩W_s'⇧*⇧* S S'" and "cdcl⇩W_bj⇧+⇧+ S' T" and "conflicting T ≠ None"
        using IH by blast
      then show ?thesis
      proof cases
        case s'
        moreover {
          have "cdcl⇩W_M_level_inv T"
            using inv local.step(1) rtranclp_cdcl⇩W_stgy_consistent_inv by auto
          then have "full1 cdcl⇩W_bj T V"
            using backtrack_is_full1_cdcl⇩W_bj backtrack by blast
          then have "cdcl⇩W_s' T V"
            using full bj' n_s by blast }
        ultimately show ?thesis by auto
      next
        case (bj S') note S_S' = this(1) and bj_T = this(2)
        moreover {
          have "cdcl⇩W_M_level_inv T"
            using inv local.step(1) rtranclp_cdcl⇩W_stgy_consistent_inv by auto
          then have "full1 cdcl⇩W_bj T V"
            using backtrack_is_full1_cdcl⇩W_bj backtrack by blast
          then have "full1 cdcl⇩W_bj S' V"
            using bj_T unfolding full1_def by fastforce }
        ultimately have "cdcl⇩W_s' S' V" by (simp add: cdcl⇩W_s'.bj')
        then show ?thesis using S_S' by auto
      qed
    next
      case skip
      then have confl_V: "conflicting V ≠ None"
        using skip by (auto elim: rulesE)
      have "cdcl⇩W_bj T V"
        using local.skip by blast
      then show ?thesis
        using confl_V step.IH by auto
    next
      case resolve
      have confl_V: "conflicting V ≠ None"
        using resolve by (auto elim!: rulesE)
      have "cdcl⇩W_bj T V"
        using local.resolve by blast
      then show ?thesis
        using confl_V step.IH by auto
    qed
  qed
qed

lemma n_step_cdcl⇩W_stgy_iff_no_step_cdcl⇩W_restart_cl_cdcl⇩W_o:
  assumes inv: "cdcl⇩W_all_struct_inv S"
  shows "no_step cdcl⇩W_s' S ⟷ no_step cdcl⇩W_stgy S" (is "?S' S ⟷ ?C S")
proof
  assume "?C S"
  then show "?S' S"
    by (auto simp: cdcl⇩W_s'.simps full1_def tranclp_unfold_begin cdcl⇩W_stgy.simps)
next
  assume n_s: "?S' S"
  then show "?C S"
    by (metis bj' cdcl⇩W_bj_exists_normal_form cdcl⇩W_o.cases cdcl⇩W_s'.intros
      cdcl⇩W_stgy.cases decide' full_unfold)
qed

lemma cdcl⇩W_s'_tranclp_cdcl⇩W_restart:
   assumes "cdcl⇩W_s' S S'" shows "cdcl⇩W_restart⇧+⇧+ S S'"
   using assms
proof (cases rule: cdcl⇩W_s'.cases)
  case conflict'
  then show ?thesis by blast
next
  case propagate'
  then show ?thesis by blast
next
  case decide'
  then show ?thesis
    using cdcl⇩W_stgy.simps cdcl⇩W_stgy_tranclp_cdcl⇩W_restart by (meson cdcl⇩W_o.simps)
next
  case bj'
  then show ?thesis
    by (metis cdcl⇩W_s'.bj' cdcl⇩W_s'_is_rtranclp_cdcl⇩W_stgy full1_def
      rtranclp_cdcl⇩W_stgy_rtranclp_cdcl⇩W_restart rtranclp_unfold tranclp_unfold_begin)
qed

lemma tranclp_cdcl⇩W_s'_tranclp_cdcl⇩W_restart:
  "cdcl⇩W_s'⇧+⇧+ S S' ⟹ cdcl⇩W_restart⇧+⇧+ S S'"
  apply (induct rule: tranclp.induct)
   using cdcl⇩W_s'_tranclp_cdcl⇩W_restart apply blast
  by (meson cdcl⇩W_s'_tranclp_cdcl⇩W_restart tranclp_trans)

lemma rtranclp_cdcl⇩W_s'_rtranclp_cdcl⇩W_restart:
   "cdcl⇩W_s'⇧*⇧* S S' ⟹ cdcl⇩W_restart⇧*⇧* S S'"
  using rtranclp_unfold[of cdcl⇩W_s' S S'] tranclp_cdcl⇩W_s'_tranclp_cdcl⇩W_restart[of S S'] by auto

lemma full_cdcl⇩W_stgy_iff_full_cdcl⇩W_s':
  assumes inv: "cdcl⇩W_all_struct_inv S"
  shows "full cdcl⇩W_stgy S T ⟷ full cdcl⇩W_s' S T" (is "?S ⟷ ?S'")
proof
  assume ?S'
  then have "cdcl⇩W_restart⇧*⇧* S T"
    using rtranclp_cdcl⇩W_s'_rtranclp_cdcl⇩W_restart[of S T] unfolding full_def by blast
  then have inv': "cdcl⇩W_all_struct_inv T"
    using rtranclp_cdcl⇩W_all_struct_inv_inv inv by blast
  have "cdcl⇩W_stgy⇧*⇧* S T"
    using ‹?S'› unfolding full_def
      using cdcl⇩W_s'_is_rtranclp_cdcl⇩W_stgy rtranclp_mono[of cdcl⇩W_s' "cdcl⇩W_stgy⇧*⇧*"] by auto
  then show ?S
    using ‹?S'› inv' n_step_cdcl⇩W_stgy_iff_no_step_cdcl⇩W_restart_cl_cdcl⇩W_o unfolding full_def
    by blast
next
  assume ?S
  then have inv_T: "cdcl⇩W_all_struct_inv T"
    by (metis assms full_def rtranclp_cdcl⇩W_all_struct_inv_inv
      rtranclp_cdcl⇩W_stgy_rtranclp_cdcl⇩W_restart)
  consider
    (s') "cdcl⇩W_s'⇧*⇧* S T" |
    (st) S' where "cdcl⇩W_s'⇧*⇧* S S'" and "cdcl⇩W_bj⇧+⇧+ S' T" and "conflicting T ≠ None"
    using rtranclp_cdcl⇩W_stgy_connected_to_rtranclp_cdcl⇩W_s'[of S T] inv ‹?S›
    unfolding full_def cdcl⇩W_all_struct_inv_def
    by blast
  then show ?S'
  proof cases
    case s'
    then show ?thesis
      using ‹full cdcl⇩W_stgy S T› unfolding full_def
      by (metis inv_T n_step_cdcl⇩W_stgy_iff_no_step_cdcl⇩W_restart_cl_cdcl⇩W_o)
  next
    case (st S') note st = this(1) and bj = this(2) and confl = this(3)
    have "no_step cdcl⇩W_bj T"
      using ‹?S› cdcl⇩W_stgy.conflict' cdcl⇩W_stgy.intros(2) other' unfolding full_def by blast
    then have "full1 cdcl⇩W_bj S' T"
      using bj unfolding full1_def by blast
    then have "cdcl⇩W_s' S' T"
      using cdcl⇩W_s'.bj'[of S' T] by blast
    then have "cdcl⇩W_s'⇧*⇧* S T"
      using st(1) by auto
    moreover have "no_step cdcl⇩W_s' T"
      using inv_T ‹full cdcl⇩W_stgy S T› n_step_cdcl⇩W_stgy_iff_no_step_cdcl⇩W_restart_cl_cdcl⇩W_o
      unfolding full_def by blast
    ultimately show ?thesis
      unfolding full_def by blast
  qed
qed

end

end