Theory IsaSAT_Backtrack

theory IsaSAT_Backtrack
  imports IsaSAT_Backtrack_Defs
begin

hide_const (open) NEMonad.ASSERT NEMonad.RETURN NEMonad.SPEC

chapter ‹Backtrack›

text ‹
  The backtrack function is highly complicated and tricky to maintain.
›

section ‹Backtrack with direct extraction of literal if highest level›

paragraph ‹Empty conflict›

definition (in -) empty_conflict_and_extract_clause
  :: ‹(nat,nat) ann_lits ⇒ nat clause ⇒ nat clause_l ⇒
        (nat clause option × nat clause_l × nat) nres›
  where
    ‹empty_conflict_and_extract_clause M D outl =
     SPEC(λ(D, C, n). D = None ∧ mset C = mset outl ∧ C!0 = outl!0 ∧
       (length C > 1 ⟶ highest_lit M (mset (tl C)) (Some (C!1, get_level M (C!1)))) ∧
       (length C > 1 ⟶ n = get_level M (C!1)) ∧
       (length C = 1 ⟶ n = 0)
      )›

definition empty_conflict_and_extract_clause_heur_inv where
  ‹empty_conflict_and_extract_clause_heur_inv M outl =
    (λ(E, C, i). mset (take i C) = mset (take i outl) ∧
            length C = length outl ∧ C ! 0 = outl ! 0 ∧ i ≥ 1 ∧ i ≤ length outl ∧
            (1 < length (take i C) ⟶
                 highest_lit M (mset (tl (take i C)))
                  (Some (C ! 1, get_level M (C ! 1)))))›

definition empty_conflict_and_extract_clause_heur ::
  "nat multiset ⇒ (nat, nat) ann_lits
     ⇒ lookup_clause_rel
       ⇒ nat literal list ⇒ (_ × nat literal list × nat) nres"
  where
    ‹empty_conflict_and_extract_clause_heur 𝒜 M D outl = do {
     let C = replicate (length outl) (outl!0);
     (D, C, _) ← WHILE⇩T⇗empty_conflict_and_extract_clause_heur_inv M outl⇖
         (λ(D, C, i). i < length_uint32_nat outl)
         (λ(D, C, i). do {
           ASSERT(i < length outl);
           ASSERT(i < length C);
           ASSERT(lookup_conflict_remove1_pre (outl ! i, D));
           let D = lookup_conflict_remove1 (outl ! i) D;
           let C = C[i := outl ! i];
           ASSERT(C!i ∈# ℒ⇩a⇩l⇩l 𝒜 ∧ C!1 ∈# ℒ⇩a⇩l⇩l 𝒜 ∧ 1 < length C);
           let C = (if get_level M (C!i) > get_level M (C!1) then swap C 1 i else C);
           ASSERT(i+1 ≤ unat32_max);
           RETURN (D, C, i+1)
         })
        (D, C, 1);
     ASSERT(length outl ≠ 1 ⟶ length C > 1);
     ASSERT(length outl ≠ 1 ⟶ C!1 ∈# ℒ⇩a⇩l⇩l 𝒜);
     RETURN ((True, D), C, if length outl = 1 then 0 else get_level M (C!1))
  }›

lemma empty_conflict_and_extract_clause_heur_empty_conflict_and_extract_clause:
  assumes
    D: ‹D = mset (tl outl)› and
    outl: ‹outl ≠ []› and
    dist: ‹distinct outl› and
    lits: ‹literals_are_in_ℒ⇩i⇩n 𝒜 (mset outl)› and
    DD': ‹(D', D) ∈ lookup_clause_rel 𝒜› and
    consistent: ‹¬ tautology (mset outl)› and
    bounded: ‹isasat_input_bounded 𝒜›
  shows
    ‹empty_conflict_and_extract_clause_heur 𝒜 M D' outl ≤ ⇓ (option_lookup_clause_rel 𝒜 ×⇩r Id ×⇩r Id)
        (empty_conflict_and_extract_clause M D outl)›
proof -
  have size_out: ‹size (mset outl) ≤ 1 + unat32_max div 2›
    using simple_clss_size_upper_div2[OF bounded lits _ consistent]
      ‹distinct outl› by auto
  have empty_conflict_and_extract_clause_alt_def:
    ‹empty_conflict_and_extract_clause M D outl = do {
      (D', outl') ← SPEC (λ(E, F). E = {#} ∧ mset F = D);
      SPEC
        (λ(D, C, n).
            D = None ∧
            mset C = mset outl ∧
            C ! 0 = outl ! 0 ∧
            (1 < length C ⟶
              highest_lit M (mset (tl C)) (Some (C ! 1, get_level M (C ! 1)))) ∧
            (1 < length C ⟶ n = get_level M (C ! 1)) ∧ (length C = 1 ⟶ n = 0))
    }› for M D outl
    unfolding empty_conflict_and_extract_clause_def RES_RES2_RETURN_RES
    by (auto simp: ex_mset)
  define I where
    ‹I ≡ λ(E, C, i). mset (take i C) = mset (take i outl) ∧
       (E, D - mset (take i outl)) ∈ lookup_clause_rel 𝒜 ∧
            length C = length outl ∧ C ! 0 = outl ! 0 ∧ i ≥ 1 ∧ i ≤ length outl ∧
            (1 < length (take i C) ⟶
                 highest_lit M (mset (tl (take i C)))
                  (Some (C ! 1, get_level M (C ! 1))))›
  have I0: ‹I (D', replicate (length outl) (outl ! 0), 1)›
    using assms by (cases outl) (auto simp: I_def)

  have [simp]: ‹ba ≥ 1 ⟹ mset (tl outl) - mset (take ba outl) = mset ((drop ba outl))›
    for ba
    apply (subst append_take_drop_id[of ‹ba - 1›, symmetric])
    using dist
    unfolding mset_append
    by (cases outl; cases ba)
      (auto simp: take_tl drop_Suc[symmetric] remove_1_mset_id_iff_notin dest: in_set_dropD)
  have empty_conflict_and_extract_clause_heur_inv:
    ‹empty_conflict_and_extract_clause_heur_inv M outl
     (D', replicate (length outl) (outl ! 0), 1)›
    using assms
    unfolding empty_conflict_and_extract_clause_heur_inv_def
    by (cases outl) auto
  have I0: ‹I (D', replicate (length outl) (outl ! 0), 1)›
    using assms
    unfolding I_def
    by (cases outl) auto
  have
    C1_L: ‹aa[ba := outl ! ba] ! 1 ∈# ℒ⇩a⇩l⇩l 𝒜› (is ?A1inL) and
    ba_le:  ‹ba + 1 ≤ unat32_max› (is ?ba_le) and
    I_rec: ‹I (lookup_conflict_remove1 (outl ! ba) a,
          if get_level M (aa[ba := outl ! ba] ! 1)
             < get_level M (aa[ba := outl ! ba] ! ba)
          then swap (aa[ba := outl ! ba]) 1 ba
          else aa[ba := outl ! ba],
          ba + 1)› (is ?I) and
    inv: ‹empty_conflict_and_extract_clause_heur_inv M outl
        (lookup_conflict_remove1 (outl ! ba) a,
         if get_level M (aa[ba := outl ! ba] ! 1)
            < get_level M (aa[ba := outl ! ba] ! ba)
         then swap (aa[ba := outl ! ba]) 1 ba
         else aa[ba := outl ! ba],
         ba + 1)› (is ?inv)
    if
      ‹empty_conflict_and_extract_clause_heur_inv M outl s› and
      I: ‹I s› and
      ‹case s of (D, C, i) ⇒ i < length_uint32_nat outl› and
      st:
      ‹s = (a, b)›
      ‹b = (aa, ba)› and
      ba_le: ‹ba < length outl› and
      ‹ba < length aa› and
      ‹lookup_conflict_remove1_pre (outl ! ba, a)›
    for s a b aa ba
  proof -
    have
      mset_aa: ‹mset (take ba aa) = mset (take ba outl)› and
      aD: ‹(a, D - mset (take ba outl)) ∈ lookup_clause_rel 𝒜› and
      l_aa_outl: ‹length aa = length outl› and
      aa0: ‹aa ! 0 = outl ! 0› and
      ba_ge1: ‹1 ≤ ba› and
      ba_lt: ‹ba ≤ length outl› and
      highest: ‹1 < length (take ba aa) ⟶
      highest_lit M (mset (tl (take ba aa)))
        (Some (aa ! 1, get_level M (aa ! 1)))›
      using I unfolding st I_def prod.case
      by auto
    have set_aa_outl:  ‹set (take ba aa) = set (take ba outl)›
      using mset_aa by (blast dest: mset_eq_setD)
    show ?ba_le
      using ba_le assms size_out
      by (auto simp: unat32_max_def)
    have ba_ge1_aa_ge:  ‹ba > 1 ⟹ aa ! 1 ∈ set (take ba aa)›
      using ba_ge1 ba_le l_aa_outl
      by (auto simp: in_set_take_conv_nth intro!: bex_lessI[of _ ‹Suc 0›])
    then have ‹aa[ba := outl ! ba] ! 1 ∈  set outl›
      using ba_le l_aa_outl ba_ge1
      unfolding mset_aa in_multiset_in_set[symmetric]
      by (cases ‹ba > 1›)
        (auto simp: mset_aa dest: in_set_takeD)
    then show ?A1inL
      using literals_are_in_ℒ⇩i⇩n_in_mset_ℒ⇩a⇩l⇩l[OF lits, of ‹aa[ba := outl ! ba] ! 1›] by auto

    define aa2 where ‹aa2 ≡ tl (tl (take ba aa))›
    have tl_take_nth_con:  ‹tl (take ba aa) = aa ! Suc 0 # aa2› if ‹ba > Suc 0›
      using ba_le ba_ge1 that l_aa_outl unfolding aa2_def
      by (cases aa; cases ‹tl aa›; cases ba; cases ‹ba - 1›)
        auto
    have no_tauto_nth:  ‹ i < length outl ⟹ - outl ! ba = outl ! i ⟹ False› for i
      using consistent ba_le nth_mem
      by (force simp: tautology_decomp' uminus_lit_swap)
    have outl_ba__L: ‹outl ! ba ∈# ℒ⇩a⇩l⇩l 𝒜›
      using ba_le literals_are_in_ℒ⇩i⇩n_in_mset_ℒ⇩a⇩l⇩l[OF lits, of ‹outl ! ba›] by auto
    have ‹(lookup_conflict_remove1 (outl ! ba) a,
        remove1_mset (outl ! ba)  (D -(mset (take ba outl)))) ∈ lookup_clause_rel 𝒜›
      by (rule lookup_conflict_remove1[THEN fref_to_Down_unRET_uncurry])
        (use ba_ge1 ba_le aD   outl_ba__L in
          ‹auto simp: D in_set_drop_conv_nth image_image dest: no_tauto_nth
        intro!: bex_geI[of _ ba]›)
    then have ‹(lookup_conflict_remove1 (outl ! ba) a,
      D - mset (take (Suc ba) outl))
      ∈ lookup_clause_rel 𝒜›
      using aD ba_le ba_ge1 ba_ge1_aa_ge aa0
      by (auto simp: take_Suc_conv_app_nth)
    moreover have ‹1 < length
          (take (ba + 1)
            (if get_level M (aa[ba := outl ! ba] ! 1)
                < get_level M (aa[ba := outl ! ba] ! ba)
             then swap (aa[ba := outl ! ba]) 1 ba
             else aa[ba := outl ! ba])) ⟶
      highest_lit M
      (mset
        (tl (take (ba + 1)
              (if get_level M (aa[ba := outl ! ba] ! 1)
                  < get_level M (aa[ba := outl ! ba] ! ba)
               then swap (aa[ba := outl ! ba]) 1 ba
               else aa[ba := outl ! ba]))))
      (Some
        ((if get_level M (aa[ba := outl ! ba] ! 1)
             < get_level M (aa[ba := outl ! ba] ! ba)
          then swap (aa[ba := outl ! ba]) 1 ba
          else aa[ba := outl ! ba]) !
         1,
         get_level M
          ((if get_level M (aa[ba := outl ! ba] ! 1)
               < get_level M (aa[ba := outl ! ba] ! ba)
            then swap (aa[ba := outl ! ba]) 1 ba
            else aa[ba := outl ! ba]) !
           1)))›
      using highest ba_le ba_ge1
      by (cases ‹ba = Suc 0›)
        (auto simp: highest_lit_def take_Suc_conv_app_nth l_aa_outl
          get_maximum_level_add_mset swap_nth_relevant max_def take_update_swap
          swap_only_first_relevant tl_update_swap mset_update nth_tl
          get_maximum_level_remove_non_max_lvl tl_take_nth_con
          aa2_def[symmetric])
    moreover have ‹mset
      (take (ba + 1)
        (if get_level M (aa[ba := outl ! ba] ! 1)
            < get_level M (aa[ba := outl ! ba] ! ba)
          then swap (aa[ba := outl ! ba]) 1 ba
          else aa[ba := outl ! ba])) =
      mset (take (ba + 1) outl)›
      using ba_le ba_ge1 ba_ge1_aa_ge aa0
      unfolding mset_aa
      by (cases ‹ba = 1›)
        (auto simp: take_Suc_conv_app_nth l_aa_outl
          take_swap_relevant swap_only_first_relevant mset_aa set_aa_outl
          mset_update add_mset_remove_trivial_If)
    ultimately show ?I
      using ba_ge1 ba_le
      unfolding I_def prod.simps
      by (auto simp: l_aa_outl aa0)

    then show ?inv
      unfolding empty_conflict_and_extract_clause_heur_inv_def I_def
      by (auto simp: l_aa_outl aa0)
  qed
  have mset_tl_out:  ‹mset (tl outl) - mset outl = {#}›
    by (cases outl) auto
  have H1: ‹WHILE⇩T⇗empty_conflict_and_extract_clause_heur_inv M outl⇖
     (λ(D, C, i). i < length_uint32_nat outl)
     (λ(D, C, i). do {
           _ ← ASSERT (i < length outl);
           _ ← ASSERT (i < length C);
           _ ← ASSERT (lookup_conflict_remove1_pre (outl ! i, D));
           _ ← ASSERT
                (C[i := outl ! i] ! i ∈# ℒ⇩a⇩l⇩l 𝒜 ∧
                 C[i := outl ! i] ! 1 ∈# ℒ⇩a⇩l⇩l 𝒜 ∧
                1 < length (C[i := outl ! i]));
           _ ← ASSERT (i + 1 ≤ unat32_max);
           RETURN
            (lookup_conflict_remove1 (outl ! i) D,
             if get_level M (C[i := outl ! i] ! 1)
                < get_level M (C[i := outl ! i] ! i)
             then swap (C[i := outl ! i]) 1 i
             else C[i := outl ! i],
             i + 1)
         })
     (D', replicate (length outl) (outl ! 0), 1)
    ≤ ⇓ {((E, C, n), (E', F')). (E, E') ∈ lookup_clause_rel 𝒜 ∧ mset C = mset outl ∧
             C ! 0 = outl ! 0 ∧
            (1 < length C ⟶
              highest_lit M (mset (tl C)) (Some (C ! 1, get_level M (C ! 1)))) ∧
            n = length outl ∧
            I (E, C, n)}
          (SPEC (λ(E, F). E = {#} ∧ mset F = D))›
    unfolding conc_fun_RES
    apply (refine_vcg WHILEIT_rule_stronger_inv_RES[where R = ‹measure (λ(_, _, i). length outl - i)›  and
          I' = ‹I›])
    subgoal by auto
    subgoal by (rule empty_conflict_and_extract_clause_heur_inv)
    subgoal by (rule I0)
    subgoal using assms by (cases outl; auto)
    subgoal
      by (auto simp: I_def)
    subgoal for s a b aa ba
      using literals_are_in_ℒ⇩i⇩n_in_ℒ⇩a⇩l⇩l lits
      unfolding lookup_conflict_remove1_pre_def prod.simps
      by (auto simp: I_def empty_conflict_and_extract_clause_heur_inv_def
          lookup_clause_rel_def D atms_of_def)
    subgoal for s a b aa ba
      using literals_are_in_ℒ⇩i⇩n_in_ℒ⇩a⇩l⇩l lits
      unfolding lookup_conflict_remove1_pre_def prod.simps
      by (auto simp: I_def empty_conflict_and_extract_clause_heur_inv_def
          lookup_clause_rel_def D atms_of_def)
    subgoal for s a b aa ba
      by (rule C1_L)
    subgoal for s a b aa ba
      using literals_are_in_ℒ⇩i⇩n_in_ℒ⇩a⇩l⇩l lits
      unfolding lookup_conflict_remove1_pre_def prod.simps
      by (auto simp: I_def empty_conflict_and_extract_clause_heur_inv_def
          lookup_clause_rel_def D atms_of_def)
    subgoal for s a b aa ba
      by (rule ba_le)
    subgoal
      by (rule inv)
    subgoal
      by (rule I_rec)
    subgoal
      by auto
    subgoal for s
      unfolding prod.simps
      apply (cases s)
      apply clarsimp
      apply (intro conjI)
      subgoal
        by (rule ex_mset)
      subgoal
        using assms
        by (auto simp: empty_conflict_and_extract_clause_heur_inv_def I_def mset_tl_out)
      subgoal
        using assms
        by (auto simp: empty_conflict_and_extract_clause_heur_inv_def I_def mset_tl_out)
      subgoal
        using assms
        by (auto simp: empty_conflict_and_extract_clause_heur_inv_def I_def mset_tl_out)
      subgoal
        using assms
        by (auto simp: empty_conflict_and_extract_clause_heur_inv_def I_def mset_tl_out)
      subgoal
        using assms
        by (auto simp: empty_conflict_and_extract_clause_heur_inv_def I_def mset_tl_out)
      done
    done
  have x1b_lall:  ‹x1b ! 1 ∈# ℒ⇩a⇩l⇩l 𝒜›
    if
      inv: ‹(x, x')
      ∈ {((E, C, n), E', F').
          (E, E') ∈ lookup_clause_rel 𝒜 ∧
          mset C = mset outl ∧
          C ! 0 = outl ! 0 ∧
          (1 < length C ⟶
          highest_lit M (mset (tl C)) (Some (C ! 1, get_level M (C ! 1)))) ∧
            n = length outl  ∧
          I (E, C, n)}› and
      ‹x' ∈ {(E, F). E = {#} ∧ mset F = D}› and
      st:
      ‹x' = (x1, x2)›
      ‹x2a = (x1b, x2b)›
      ‹x = (x1a, x2a)› and
      ‹length outl ≠ 1 ⟶ 1 < length x1b› and
      ‹length outl ≠ 1›
    for x x' x1 x2 x1a x2a x1b x2b
  proof -
    have
      ‹(x1a, x1) ∈ lookup_clause_rel 𝒜› and
      ‹mset x1b = mset outl› and
      ‹x1b ! 0 = outl ! 0› and
      ‹Suc 0 < length x1b ⟶
      highest_lit M (mset (tl x1b))
        (Some (x1b ! Suc 0, get_level M (x1b ! Suc 0)))› and
      mset_aa: ‹mset (take x2b x1b) = mset (take x2b outl)› and
      ‹(x1a, D - mset (take x2b outl)) ∈ lookup_clause_rel 𝒜› and
      l_aa_outl: ‹length x1b = length outl› and
      ‹x1b ! 0 = outl ! 0› and
      ba_ge1: ‹Suc 0 ≤ x2b› and
      ba_le: ‹x2b ≤ length outl› and
      ‹Suc 0 < length x1b ∧ Suc 0 < x2b ⟶
     highest_lit M (mset (tl (take x2b x1b)))
      (Some (x1b ! Suc 0, get_level M (x1b ! Suc 0)))›
      using inv unfolding st I_def prod.case st
      by auto

    have set_aa_outl: ‹set (take x2b x1b) = set (take x2b outl)›
      using mset_aa by (blast dest: mset_eq_setD)
    have ba_ge1_aa_ge:  ‹x2b > 1 ⟹ x1b ! 1 ∈ set (take x2b x1b)›
      using ba_ge1 ba_le l_aa_outl
      by (auto simp: in_set_take_conv_nth intro!: bex_lessI[of _ ‹Suc 0›])
    then have ‹x1b ! 1 ∈ set outl›
      using ba_le l_aa_outl ba_ge1 that
      unfolding mset_aa in_multiset_in_set[symmetric]
      by (cases ‹x2b > 1›)
        (auto simp: mset_aa dest: in_set_takeD)
    then show ?thesis
      using literals_are_in_ℒ⇩i⇩n_in_mset_ℒ⇩a⇩l⇩l[OF lits, of ‹x1b ! 1›] by auto
  qed

  show ?thesis
    unfolding empty_conflict_and_extract_clause_heur_def empty_conflict_and_extract_clause_alt_def
      Let_def I_def[symmetric]
    apply (subst empty_conflict_and_extract_clause_alt_def)
    unfolding conc_fun_RES
    apply (refine_vcg WHILEIT_rule_stronger_inv[where R = ‹measure (λ(_, _, i). length outl - i)› and
          I' = ‹I›] H1)
    subgoal using assms by (auto simp: I_def)
    subgoal by (rule x1b_lall)
    subgoal using assms
      by (auto intro!: RETURN_RES_refine simp: option_lookup_clause_rel_def I_def)
    done
qed

lemma isa_empty_conflict_and_extract_clause_heur_empty_conflict_and_extract_clause_heur:
  ‹(uncurry2 isa_empty_conflict_and_extract_clause_heur, uncurry2 (empty_conflict_and_extract_clause_heur 𝒜)) ∈
     trail_pol 𝒜 ×⇩f Id ×⇩f Id →⇩f ⟨Id⟩nres_rel ›
proof -
  have [refine0]: ‹((x2b, replicate (length x2c) (x2c ! 0), 1), x2,
	 replicate (length x2a) (x2a ! 0), 1)
	∈ Id ×⇩f Id ×⇩f Id›
    if
      ‹(x, y) ∈ trail_pol 𝒜 ×⇩f Id ×⇩f Id› and    ‹x1 = (x1a, x2)› and
      ‹y = (x1, x2a)› and
      ‹x1b = (x1c, x2b)› and
      ‹x = (x1b, x2c)›
    for x y x1 x1a x2 x2a x1b x1c x2b x2c
    using that by auto

  show ?thesis
    supply [[goals_limit=1]]
    unfolding isa_empty_conflict_and_extract_clause_heur_def empty_conflict_and_extract_clause_heur_def uncurry_def
    apply (intro frefI nres_relI)
    apply (refine_rcg)
                    apply (assumption+)[5]
    subgoal by auto
    subgoal by auto
    subgoal by auto
    subgoal by auto
    subgoal
      by (rule get_level_pol_pre) auto
    subgoal
      by (rule get_level_pol_pre) auto
    subgoal by auto
    subgoal by auto
    subgoal
      by (auto simp: get_level_get_level_pol[of _ _ 𝒜])
    subgoal by auto
    subgoal
      by (rule get_level_pol_pre) auto
    subgoal by (auto simp: get_level_get_level_pol[of _ _ 𝒜])
    done
qed


definition extract_shorter_conflict_wl_nlit where
  ‹extract_shorter_conflict_wl_nlit K M NU D NE UE =
    SPEC(λD'. D' ≠ None ∧ the D' ⊆# the D ∧ K ∈# the D' ∧
      mset `# ran_mf NU + NE + UE ⊨pm the D')›

definition extract_shorter_conflict_wl_nlit_st
  :: ‹'v twl_st_wl ⇒ 'v twl_st_wl nres›
  where
    ‹extract_shorter_conflict_wl_nlit_st =
     (λ(M, N, D, NE, UE, WS, Q). do {
        let K = -lit_of (hd M);
        D ← extract_shorter_conflict_wl_nlit K M N D NE UE;
        RETURN (M, N, D, NE, UE, WS, Q)})›

definition empty_lookup_conflict_and_highest
  :: ‹'v twl_st_wl ⇒ ('v twl_st_wl × nat) nres›
  where
    ‹empty_lookup_conflict_and_highest  =
     (λ(M, N, D, NE, UE, WS, Q). do {
        let K = -lit_of (hd M);
        let n = get_maximum_level M (remove1_mset K (the D));
        RETURN ((M, N, D, NE, UE, WS, Q), n)})›

definition extract_shorter_conflict_heur where
  ‹extract_shorter_conflict_heur = (λM NU NUE C outl. do {
     let K = lit_of (hd M);
     let C = Some (remove1_mset (-K) (the C));
     C ← iterate_over_conflict (-K) M NU NUE (the C);
     RETURN (Some (add_mset (-K) C))
  })›

definition (in -) empty_cach where
  ‹empty_cach cach = (λ_. SEEN_UNKNOWN)›

definition empty_conflict_and_extract_clause_pre
  :: ‹(((nat,nat) ann_lits × nat clause) × nat clause_l) ⇒ bool› where
  ‹empty_conflict_and_extract_clause_pre =
    (λ((M, D), outl). D = mset (tl outl)  ∧ outl ≠ [] ∧ distinct outl ∧
    ¬tautology (mset outl) ∧ length outl ≤ unat32_max)›

lemma empty_cach_ref_empty_cach:
  ‹isasat_input_bounded 𝒜 ⟹ (RETURN o empty_cach_ref, RETURN o empty_cach) ∈ cach_refinement 𝒜 →⇩f ⟨cach_refinement 𝒜⟩ nres_rel›
  by (intro frefI nres_relI)
    (auto simp: empty_cach_def empty_cach_ref_def cach_refinement_alt_def cach_refinement_list_def
      map_fun_rel_def intro: bounded_included_le)


paragraph ‹Minimisation of the conflict›

lemma the_option_lookup_clause_assn:
  ‹(RETURN o snd, RETURN o the) ∈ [λD. D ≠ None]⇩f option_lookup_clause_rel 𝒜 → ⟨lookup_clause_rel 𝒜⟩nres_rel›
  by (intro frefI nres_relI)
    (auto simp: option_lookup_clause_rel_def)

lemma heuristic_rel_stats_update_heuristics_stats[intro!]:
  ‹heuristic_rel_stats 𝒜 heur ⟹ heuristic_rel_stats 𝒜 (update_propagation_heuristics_stats glue heur)›
  by (auto simp: heuristic_rel_stats_def phase_save_heur_rel_def phase_saving_def
    update_propagation_heuristics_stats_def)

lemma heuristic_rel_update_heuristics[intro!]:
  ‹heuristic_rel 𝒜 heur ⟹ heuristic_rel 𝒜 (update_propagation_heuristics glue heur)›
  by (auto simp: heuristic_rel_def phase_save_heur_rel_def phase_saving_def
    update_propagation_heuristics_def)

lemma valid_arena_update_lbd_and_mark_used:
  assumes arena: ‹valid_arena arena N vdom› and i: ‹i ∈# dom_m N›
  shows ‹valid_arena (update_lbd_and_mark_used i lbd arena) N vdom›
  using assms by (auto intro!: valid_arena_update_lbd valid_arena_mark_used valid_arena_mark_used2
    simp: update_lbd_and_mark_used_def Let_def)

definition remove_last
  :: ‹nat literal ⇒ nat clause option ⇒ nat clause option nres›
  where
    ‹remove_last _ _  = SPEC((=) None)›


paragraph ‹Full function›

lemma get_all_ann_decomposition_get_level:
  assumes
    L': ‹L' = lit_of (hd M')› and
    nd: ‹no_dup M'› and
    decomp: ‹(Decided K # a, M2) ∈ set (get_all_ann_decomposition M')› and
    lev_K: ‹get_level M' K = Suc (get_maximum_level M' (remove1_mset (- L') y))› and
    L: ‹L ∈# remove1_mset (- lit_of (hd M')) y›
  shows ‹get_level a L = get_level M' L›
proof -
  obtain M3 where M3: ‹M' = M3 @ M2 @ Decided K # a›
    using decomp by blast
  from lev_K have lev_L: ‹get_level M' L < get_level M' K›
    using get_maximum_level_ge_get_level[OF L, of M'] unfolding L'[symmetric] by auto
  have [simp]: ‹get_level (M3 @ M2 @ Decided K # a) K = Suc (count_decided a)›
    using nd unfolding M3 by auto
  have undef:‹undefined_lit (M3 @ M2) L›
    using lev_L get_level_skip_end[of ‹M3 @ M2› L ‹Decided K # a›] unfolding M3
    by auto
  then have ‹atm_of L ≠ atm_of K›
    using lev_L unfolding M3 by auto
  then show ?thesis
    using undef unfolding M3 by (auto simp: get_level_cons_if)
qed

definition del_conflict_wl :: ‹'v twl_st_wl ⇒ 'v twl_st_wl› where
  ‹del_conflict_wl = (λ(M, N, D, NE, UE, Q, W). (M, N, None, NE, UE, Q, W))›

lemma [simp]:
  ‹get_clauses_wl (del_conflict_wl S) = get_clauses_wl S›
  by (cases S) (auto simp: del_conflict_wl_def)

lemma lcount_add_clause[simp]: ‹i ∉# dom_m N ⟹
    size (learned_clss_l (fmupd i (C, False) N)) = Suc (size (learned_clss_l N))›
  by (simp add: learned_clss_l_mapsto_upd_notin)

lemma length_watched_le:
  assumes
    prop_inv: ‹correct_watching x1› and
    xb_x'a: ‹(x1a, x1) ∈ twl_st_heur_conflict_ana› and
    x2: ‹x2 ∈# ℒ⇩a⇩l⇩l (all_atms_st x1)›
  shows ‹length (watched_by x1 x2) ≤ length (get_clauses_wl_heur x1a) - MIN_HEADER_SIZE›
proof -
  have ‹correct_watching x1›
    using prop_inv unfolding unit_propagation_outer_loop_wl_inv_def
      unit_propagation_outer_loop_wl_inv_def
    by auto
  then have dist: ‹distinct_watched (watched_by x1 x2)›
    using x2 unfolding all_atms_def[symmetric] all_lits_alt_def[symmetric]
    by (cases x1; auto simp: ℒ⇩a⇩l⇩l_atm_of_all_lits_of_mm correct_watching.simps
        ℒ⇩a⇩l⇩l_all_atms_all_lits
      simp flip: all_lits_alt_def2 all_lits_def all_atms_def all_lits_st_alt_def)
  then have dist: ‹distinct_watched (watched_by x1 x2)›
    using xb_x'a
    by (cases x1; auto simp: ℒ⇩a⇩l⇩l_atm_of_all_lits_of_mm correct_watching.simps)
  have dist_vdom: ‹distinct (get_vdom x1a)›
    using xb_x'a
    by (cases x1)
      (auto simp: twl_st_heur_conflict_ana_def twl_st_heur'_def aivdom_inv_dec_alt_def)
  have x2: ‹x2 ∈# ℒ⇩a⇩l⇩l (all_atms_st x1)›
    using x2 xb_x'a unfolding all_atms_def
    by auto

  have
      valid: ‹valid_arena (get_clauses_wl_heur x1a) (get_clauses_wl x1) (set (get_vdom x1a))›
    using xb_x'a unfolding all_atms_def all_lits_def
    by (cases x1)
     (auto simp: twl_st_heur'_def twl_st_heur_conflict_ana_def)

  have ‹vdom_m (all_atms_st x1) (get_watched_wl x1) (get_clauses_wl x1) ⊆ set (get_vdom x1a)›
    using xb_x'a
    by (cases x1)
      (auto simp: twl_st_heur_conflict_ana_def twl_st_heur'_def all_atms_def[symmetric])
  then have subset: ‹set (map fst (watched_by x1 x2)) ⊆ set (get_vdom x1a)›
    using x2 unfolding vdom_m_def
    by (cases x1)
      (force simp: twl_st_heur'_def twl_st_heur_def simp flip: all_atms_def
        dest!: multi_member_split)
  have watched_incl: ‹mset (map fst (watched_by x1 x2)) ⊆# mset (get_vdom x1a)›
    by (rule distinct_subseteq_iff[THEN iffD1])
      (use dist[unfolded distinct_watched_alt_def] dist_vdom subset in
         ‹simp_all flip: distinct_mset_mset_distinct›)
  have vdom_incl: ‹set (get_vdom x1a) ⊆ {MIN_HEADER_SIZE..< length (get_clauses_wl_heur x1a)}›
    using valid_arena_in_vdom_le_arena[OF valid] arena_dom_status_iff[OF valid] by auto

  have ‹length (get_vdom x1a) ≤ length (get_clauses_wl_heur x1a) - MIN_HEADER_SIZE›
    by (subst distinct_card[OF dist_vdom, symmetric])
      (use card_mono[OF _ vdom_incl] in auto)
  then show ?thesis
    using size_mset_mono[OF watched_incl] xb_x'a
    by (auto intro!: order_trans[of ‹length (watched_by x1 x2)› ‹length (get_vdom x1a)›])
qed

definition single_of_mset where
  ‹single_of_mset D = SPEC(λL. D = mset [L])›

lemma backtrack_wl_D_nlit_backtrack_wl_D:
  ‹(backtrack_wl_D_nlit_heur, backtrack_wl) ∈
  {(S, T). (S, T) ∈ twl_st_heur_conflict_ana ∧ length (get_clauses_wl_heur S) = r ∧
       learned_clss_count S ≤ u} →⇩f
  ⟨{(S, T). (S, T) ∈ twl_st_heur ∧ length (get_clauses_wl_heur S) ≤ MAX_HEADER_SIZE+1 + r + unat32_max div 2 ∧
       learned_clss_count S ≤ Suc u}⟩nres_rel›
  (is ‹_ ∈ ?R →⇩f ⟨?S⟩nres_rel›)
proof -
  have backtrack_wl_D_nlit_heur_alt_def: ‹backtrack_wl_D_nlit_heur S⇩0 =
    do {
      ASSERT(backtrack_wl_D_heur_inv S⇩0);
      ASSERT(fst (get_trail_wl_heur S⇩0) ≠ []);
      L ← lit_of_hd_trail_st_heur S⇩0;
      (S, n, C) ← extract_shorter_conflict_list_heur_st S⇩0;
      ASSERT(get_clauses_wl_heur S = get_clauses_wl_heur S⇩0 ∧
           get_learned_count S = get_learned_count S⇩0);
      S ← find_decomp_wl_st_int n S;
      ASSERT(get_clauses_wl_heur S = get_clauses_wl_heur S⇩0 ∧
           get_learned_count S = get_learned_count S⇩0);

      if size C > 1
      then do {
        let _ = C ! 1;
        S ← propagate_bt_wl_D_heur L C S;
        save_phase_st S
      }
      else do {
        propagate_unit_bt_wl_D_int L S
     }
  }› for S⇩0
    unfolding backtrack_wl_D_nlit_heur_def Let_def
    by auto
  have inv: ‹backtrack_wl_D_heur_inv S'›
    if
      ‹backtrack_wl_inv S› and
      ‹(S', S) ∈ ?R›
    for S S'
    using that unfolding backtrack_wl_D_heur_inv_def
    by (cases S; cases S') (blast intro: exI[of _ S'])
  have shorter:
    ‹extract_shorter_conflict_list_heur_st S'
       ≤ ⇓ {((T', n, C), T). (T', del_conflict_wl T) ∈ twl_st_heur_bt  ∧
              n = get_maximum_level (get_trail_wl T)
                  (remove1_mset (-lit_of(hd (get_trail_wl T))) (the (get_conflict_wl T))) ∧
              mset C = the (get_conflict_wl T) ∧
              get_conflict_wl T ≠ None∧
              equality_except_conflict_wl T S ∧
              get_clauses_wl_heur T' = get_clauses_wl_heur S' ∧
              get_learned_count T' = get_learned_count S' ∧
              (1 < length C ⟶
                highest_lit (get_trail_wl T) (mset (tl C))
                (Some (C ! 1, get_level (get_trail_wl T) (C ! 1)))) ∧
              C ≠ [] ∧ hd C = -lit_of(hd (get_trail_wl T)) ∧
              mset C ⊆# the (get_conflict_wl S) ∧
              distinct_mset (the (get_conflict_wl S)) ∧
              literals_are_in_ℒ⇩i⇩n (all_atms_st S) (the (get_conflict_wl S)) ∧
              literals_are_in_ℒ⇩i⇩n_trail (all_atms_st T) (get_trail_wl T) ∧
              get_conflict_wl S ≠ None ∧
              - lit_of (hd (get_trail_wl S)) ∈# ℒ⇩a⇩l⇩l (all_atms_st S) ∧
              literals_are_ℒ⇩i⇩n (all_atms_st T) T ∧
              n < count_decided (get_trail_wl T) ∧
	            get_trail_wl T ≠ [] ∧
              ¬ tautology (mset C) ∧
              correct_watching S ∧ length (get_clauses_wl_heur T') = length (get_clauses_wl_heur S')}
           (extract_shorter_conflict_wl S)›
    (is ‹_ ≤ ⇓ ?shorter _›)
    if
      inv: ‹backtrack_wl_inv S› and
      S'_S: ‹(S', S) ∈ ?R›
    for S S'
  proof -
    obtain M N D NE UE NEk UEk NS US N0 U0 Q W where
      S: ‹S = (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W)›
      by (cases S)
    let ?M' = ‹get_trail_wl_heur S'›
    let ?arena = ‹get_clauses_wl_heur S'›
    let ?bD' = ‹get_conflict_wl_heur S'›
    let ?W' = ‹get_watched_wl_heur S'›
    let ?vm = ‹get_vmtf_heur S'›
    let ?clvls = ‹get_count_max_lvls_heur S'›
    let ?cach = ‹get_conflict_cach S'›
    let ?outl = ‹get_outlearned_heur S'›
    let ?lcount = ‹get_learned_count S'›
    let ?aivdom = ‹get_aivdom S'›
    let ?b = ‹fst ?bD'›
    let ?D' = ‹snd ?bD'›

    let ?vdom = ‹set (get_vdom_aivdom ?aivdom)›
    have
      M'_M: ‹(?M', M) ∈ trail_pol (all_atms_st S)›  and
      ‹(?W', W) ∈ ⟨Id⟩map_fun_rel (D⇩0 (all_atms_st S))› and
      vm: ‹?vm ∈ bump_heur (all_atms_st S) M› and
      n_d: ‹no_dup M› and
      ‹?clvls ∈ counts_maximum_level M D› and
      cach_empty: ‹cach_refinement_empty (all_atms_st S) ?cach› and
      outl: ‹out_learned M D ?outl› and
      lcount: ‹clss_size_corr N NE UE NEk UEk NS US N0 U0 ?lcount› and
      ‹vdom_m (all_atms_st S) W N ⊆ ?vdom› and
      D': ‹(?bD', D) ∈ option_lookup_clause_rel (all_atms_st S)› and
      arena: ‹valid_arena ?arena N ?vdom› and
      bounded: ‹isasat_input_bounded (all_atms_st S)› and
      aivdom: ‹aivdom_inv_dec ?aivdom (dom_m N)›
      using S'_S unfolding S twl_st_heur_conflict_ana_def
      by (auto simp: S all_atms_def[symmetric])
    obtain T U where
      ℒ⇩i⇩n :‹literals_are_ℒ⇩i⇩n (all_atms_st S) S› and
      S_T: ‹(S, T) ∈ state_wl_l None› and
      corr: ‹correct_watching S› and
      T_U: ‹(T, U) ∈ twl_st_l None› and
      trail_nempty: ‹get_trail_l T ≠ []› and
      not_none: ‹get_conflict_l T ≠ None› and
      struct_invs: ‹twl_struct_invs U› and
      stgy_invs: ‹twl_stgy_invs U› and
      list_invs: ‹twl_list_invs T› and
      not_empty: ‹get_conflict_l T ≠ Some {#}› and
      uL_D: ‹- lit_of (hd (get_trail_wl S)) ∈# the (get_conflict_wl S)› and
      nss: ‹no_step cdcl⇩W_restart_mset.skip (state⇩W_of U)› and
      nsr: ‹no_step cdcl⇩W_restart_mset.resolve (state⇩W_of U)›
      using inv unfolding backtrack_wl_inv_def backtrack_wl_inv_def backtrack_l_inv_def backtrack_inv_def
      apply -
      apply normalize_goal+ by simp
    have D_none: ‹D ≠ None›
      using S_T not_none by (auto simp: S)
    have b: ‹¬?b›
      using D' not_none S_T by (auto simp: option_lookup_clause_rel_def S state_wl_l_def)
    have ‹get_conflict U ≠ Some {#}›
      using struct_invs S_T T_U uL_D by auto
    then have ‹get_learned_clauses0 U = {#}›
      ‹get_init_clauses0 U = {#}›
      using struct_invs
      by (cases U; auto simp: twl_struct_invs_def pcdcl_all_struct_invs_def
        clauses0_inv_def)+
    then have clss0: ‹get_learned_clauses0_wl S = {#}›
      ‹get_init_clauses0_wl S = {#}›
      using S_T T_U by auto
    have all_struct:
      ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (state⇩W_of U)›
      using struct_invs unfolding twl_struct_invs_def pcdcl_all_struct_invs_def
      by auto
    have
      ‹cdcl⇩W_restart_mset.no_strange_atm (state⇩W_of U)› and
      lev_inv: ‹cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv (state⇩W_of U)› and
      ‹∀s∈#learned_clss (state⇩W_of U). ¬ tautology s› and
      dist: ‹cdcl⇩W_restart_mset.distinct_cdcl⇩W_state (state⇩W_of U)› and
      confl: ‹cdcl⇩W_restart_mset.cdcl⇩W_conflicting (state⇩W_of U)› and
      ‹all_decomposition_implies_m  (cdcl⇩W_restart_mset.clauses (state⇩W_of U))
        (get_all_ann_decomposition (trail (state⇩W_of U)))› and
      learned: ‹cdcl⇩W_restart_mset.cdcl⇩W_learned_clause (state⇩W_of U)›
      using all_struct unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
      by fast+
    have n_d: ‹no_dup M›
      using lev_inv S_T T_U unfolding cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
      by (auto simp: twl_st S)
    have M_ℒ⇩i⇩n: ‹literals_are_in_ℒ⇩i⇩n_trail (all_atms_st S) (get_trail_wl S)›
      apply (rule literals_are_ℒ⇩i⇩n_literals_are_ℒ⇩i⇩n_trail[OF S_T struct_invs T_U ℒ⇩i⇩n ]) .
    have dist_D: ‹distinct_mset (the (get_conflict_wl S))›
      using dist not_none S_T T_U unfolding cdcl⇩W_restart_mset.distinct_cdcl⇩W_state_def S
      by (auto simp: twl_st)
    have ‹the (conflicting (state⇩W_of U)) =
      add_mset (- lit_of (cdcl⇩W_restart_mset.hd_trail (state⇩W_of U)))
        {#L ∈# the (conflicting (state⇩W_of U)).  get_level (trail (state⇩W_of U)) L
             < backtrack_lvl (state⇩W_of U)#}›
      apply (rule cdcl⇩W_restart_mset.no_skip_no_resolve_single_highest_level)
      subgoal using nss unfolding S by simp
      subgoal using nsr unfolding S by simp
      subgoal using struct_invs unfolding twl_struct_invs_def 
        pcdcl_all_struct_invs_def state⇩W_of_def[symmetric] S by simp
      subgoal using stgy_invs unfolding twl_stgy_invs_def S by simp
      subgoal using not_none S_T T_U by (simp add: twl_st)
      subgoal using not_empty not_none S_T T_U by (auto simp add: twl_st)
      done
    then have D_filter: ‹the D = add_mset (- lit_of (hd M)) {#L ∈# the D. get_level M L < count_decided M#}›
      using trail_nempty S_T T_U by (simp add: twl_st S)
    have tl_outl_D: ‹mset (tl (?outl[0 := - lit_of (hd M)])) = remove1_mset (?outl[0 := - lit_of (hd M)] ! 0) (the D)›
      using outl S_T T_U not_none
      apply (subst D_filter)
      by (cases ?outl) (auto simp: out_learned_def S)
    let ?D = ‹remove1_mset (- lit_of (hd M)) (the D)›
    have ℒ⇩i⇩n_S: ‹literals_are_in_ℒ⇩i⇩n (all_atms_st S) (the (get_conflict_wl S))›
      apply (rule literals_are_ℒ⇩i⇩n_literals_are_in_ℒ⇩i⇩n_conflict[OF S_T _ T_U])
      using ℒ⇩i⇩n not_none struct_invs not_none S_T T_U by (auto simp: S)
    then have ℒ⇩i⇩n_D: ‹literals_are_in_ℒ⇩i⇩n (all_atms_st S) ?D›
      unfolding S by (auto intro: literals_are_in_ℒ⇩i⇩n_mono)
    have ℒ⇩i⇩n_NU: ‹literals_are_in_ℒ⇩i⇩n_mm (all_atms_st S) (mset `# ran_mf (get_clauses_wl S))›
      (*TODO proof*)
      by (auto simp: all_atms_def all_lits_def literals_are_in_ℒ⇩i⇩n_mm_def
          ℒ⇩a⇩l⇩l_atm_of_all_lits_of_mm all_lits_st_def simp flip: all_lits_st_alt_def)
        (simp add: all_lits_of_mm_union)
    have tauto_confl: ‹¬ tautology (the (get_conflict_wl S))›
      apply (rule conflict_not_tautology[OF S_T _ T_U])
      using struct_invs not_none S_T T_U by (auto simp: twl_st)
    from not_tautology_mono[OF _ this, of ?D] have tauto_D: ‹¬ tautology ?D›
      by (auto simp: S)
    have entailed:
      ‹mset `# ran_mf (get_clauses_wl S) +  (get_unit_learned_clss_wl S + get_unit_init_clss_wl S) +
      (get_subsumed_init_clauses_wl S + get_subsumed_learned_clauses_wl S) +
      (get_init_clauses0_wl S + get_learned_clauses0_wl S)⊨pm
        add_mset (- lit_of (hd (get_trail_wl S)))
           (remove1_mset (- lit_of (hd (get_trail_wl S))) (the (get_conflict_wl S)))›
      using uL_D learned not_none S_T T_U unfolding cdcl⇩W_restart_mset.cdcl⇩W_learned_clause_alt_def
      by (auto simp: ac_simps twl_st get_unit_clauses_wl_alt_def)
    define cach' where ‹cach' = (λ_::nat. SEEN_UNKNOWN)›
    have mini: ‹minimize_and_extract_highest_lookup_conflict (all_atms_st S) (get_trail_wl S) (get_clauses_wl S)
              ?D cach' lbd (?outl[0 := - lit_of (hd M)])
          ≤ ⇓ {((E, s, outl), E'). E = E' ∧ mset (tl outl) = E ∧
                 outl ! 0 = - lit_of (hd M) ∧ E' ⊆# remove1_mset (- lit_of (hd M)) (the D) ∧
                outl ≠ []}
              (iterate_over_conflict (- lit_of (hd M)) (get_trail_wl S)
                (mset `# ran_mf (get_clauses_wl S))
                ((get_unit_learned_clss_wl S + get_unit_init_clss_wl S) +
                 (get_subsumed_learned_clauses_wl S + get_subsumed_init_clauses_wl S) +
                 (get_learned_clauses0_wl S + get_init_clauses0_wl S))
              ?D)› for lbd
      apply (rule minimize_and_extract_highest_lookup_conflict_iterate_over_conflict[of S T U
            ‹?outl [0 := - lit_of (hd M)]›
            ‹remove1_mset _ (the D)› ‹all_atms_st S› cach' ‹-lit_of (hd M)› lbd])
      subgoal using S_T .
      subgoal using T_U .
      subgoal using ‹out_learned M D ?outl› tl_outl_D
        by (auto simp: out_learned_def)
      subgoal using confl not_none S_T T_U unfolding cdcl⇩W_restart_mset.cdcl⇩W_conflicting_def
        by (auto simp: true_annot_CNot_diff twl_st S)
      subgoal
        using dist not_none S_T T_U unfolding cdcl⇩W_restart_mset.distinct_cdcl⇩W_state_def
        by (auto simp: twl_st S)
      subgoal using tauto_D .
      subgoal using M_ℒ⇩i⇩n unfolding S by simp
      subgoal using struct_invs unfolding S by simp
      subgoal using list_invs unfolding S by simp
      subgoal using M_ℒ⇩i⇩n cach_empty S_T T_U
        unfolding cach_refinement_empty_def conflict_min_analysis_inv_def
        by (auto dest: literals_are_in_ℒ⇩i⇩n_trail_in_lits_of_l_atms simp: cach'_def twl_st S)
      subgoal using entailed unfolding S by (simp add: ac_simps)
      subgoal using ℒ⇩i⇩n_D .
      subgoal using ℒ⇩i⇩n_NU .
      subgoal using ‹out_learned M D ?outl› tl_outl_D
        by (auto simp: out_learned_def)
      subgoal using ‹out_learned M D ?outl› tl_outl_D
        by (auto simp: out_learned_def)
      subgoal using bounded unfolding all_atms_def by (simp add: S)
      done
    then have mini: ‹minimize_and_extract_highest_lookup_conflict (all_atms_st S) M N
              ?D cach' lbd (?outl[0 := - lit_of (hd M)])
          ≤ ⇓ {((E, s, outl), E'). E = E' ∧ mset (tl outl) = E ∧
                 outl ! 0 = - lit_of (hd M) ∧ E' ⊆# remove1_mset (- lit_of (hd M)) (the D) ∧
                  outl ≠ []}
              (iterate_over_conflict (- lit_of (hd M)) (get_trail_wl S)
                (mset `# ran_mf N)
                (get_unit_learned_clss_wl S + get_unit_init_clss_wl S +
                (get_subsumed_learned_clauses_wl S + get_subsumed_init_clauses_wl S) +
                 (get_learned_clauses0_wl S + get_init_clauses0_wl S)) ?D)› for lbd
      unfolding S by auto
    have mini: ‹minimize_and_extract_highest_lookup_conflict (all_atms_st S) M N
              ?D cach' lbd (?outl[0 := - lit_of (hd M)])
          ≤ ⇓ {((E, s, outl), E'). E = E' ∧ mset (tl outl) = E ∧
                 outl ! 0 = - lit_of (hd M) ∧ E' ⊆# remove1_mset (- lit_of (hd M)) (the D) ∧
                 outl ≠ []}
              (SPEC (λD'. D' ⊆# ?D ∧  mset `# ran_mf N +
                      (get_unit_learned_clss_wl S + get_unit_init_clss_wl S +
                       (get_subsumed_learned_clauses_wl S + get_subsumed_init_clauses_wl S) +
                      (get_learned_clauses0_wl S + get_init_clauses0_wl S)) ⊨pm add_mset (- lit_of (hd M)) D'))›
        for lbd
      apply (rule order.trans)
       apply (rule mini)
      apply (rule ref_two_step')
      apply (rule order.trans)
       apply (rule iterate_over_conflict_spec)
      subgoal using entailed by (auto simp: S ac_simps)
      subgoal
        using dist not_none S_T T_U unfolding S cdcl⇩W_restart_mset.distinct_cdcl⇩W_state_def
        by (auto simp: twl_st)
      subgoal by (auto simp: ac_simps)
      done
    have uM_ℒ⇩a⇩l⇩l: ‹- lit_of (hd M) ∈# ℒ⇩a⇩l⇩l (all_atms_st S)›
      using M_ℒ⇩i⇩n trail_nempty S_T T_U by (cases M)
        (auto simp: literals_are_in_ℒ⇩i⇩n_trail_Cons uminus_𝒜⇩i⇩n_iff twl_st S)

    have L_D: ‹lit_of (hd M) ∉# the D› and
      tauto_confl':  ‹¬tautology (remove1_mset (- lit_of (hd M)) (the D))›
      using uL_D tauto_confl
      by (auto dest!: multi_member_split simp: S add_mset_eq_add_mset tautology_add_mset)
    then have pre1: ‹D ≠ None ∧ delete_from_lookup_conflict_pre (all_atms_st S) (- lit_of (hd M), the D)›
      using not_none uL_D uM_ℒ⇩a⇩l⇩l S_T T_U unfolding delete_from_lookup_conflict_pre_def
      by (auto simp: twl_st S)
    have pre2: ‹literals_are_in_ℒ⇩i⇩n_trail (all_atms_st S) M ∧ literals_are_in_ℒ⇩i⇩n_mm (all_atms_st S) (mset `# ran_mf N) ≡ True›
      and lits_N: ‹literals_are_in_ℒ⇩i⇩n_mm (all_atms_st S) (mset `# ran_mf N)›
      using M_ℒ⇩i⇩n S_T T_U not_none ℒ⇩i⇩n
      unfolding is_ℒ⇩a⇩l⇩l_def literals_are_in_ℒ⇩i⇩n_mm_def literals_are_ℒ⇩i⇩n_def all_atms_def all_lits_def
        all_lits_st_alt_def[symmetric] all_lits_st_def
      by (auto simp: twl_st S all_lits_of_mm_union)
    have ‹0 < length ?outl›
      using ‹out_learned M D ?outl›
      by (auto simp: out_learned_def)
    have trail_nempty: ‹M ≠ []›
      using trail_nempty S_T T_U
      by (auto simp: twl_st S)

    have lookup_conflict_remove1_pre: ‹lookup_conflict_remove1_pre (-lit_of (hd M), ?D')›
      using D' not_none not_empty S_T uM_ℒ⇩a⇩l⇩l
      unfolding lookup_conflict_remove1_pre_def
      by (cases ‹the D›)
        (auto simp: option_lookup_clause_rel_def lookup_clause_rel_def S
          state_wl_l_def atms_of_def)
    then have lookup_conflict_remove1_pre: ‹lookup_conflict_remove1_pre (-lit_of_last_trail_pol ?M', ?D')›
      by (subst lit_of_last_trail_pol_lit_of_last_trail[THEN fref_to_Down_unRET_Id, of M ?M'])
        (use M'_M trail_nempty in ‹auto simp: lit_of_hd_trail_def›)

    have ‹- lit_of (hd M) ∈# (the D)›
      using uL_D by (auto simp: S)
    then have extract_shorter_conflict_wl_alt_def:
      ‹extract_shorter_conflict_wl (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W) = do {
        _ :: bool list ← SPEC (λ_. True);
        let K = lit_of (hd M);
        let D = (remove1_mset (-K) (the D));
        _ ← RETURN (); ⌦‹vmtf rescoring›
        E' ← (SPEC
          (λ(E'). E' ⊆# add_mset (-K) D ∧ - lit_of (hd M) :#  E' ∧
             mset `# ran_mf N +
             (get_unit_learned_clss_wl S + get_unit_init_clss_wl S +
                (get_subsumed_learned_clauses_wl S + get_subsumed_init_clauses_wl S)) ⊨pm E'));
        D ← RETURN (Some E');
        RETURN  (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W)
      }›
      unfolding extract_shorter_conflict_wl_def
      by (auto simp: RES_RETURN_RES image_iff mset_take_mset_drop_mset' S union_assoc
          Un_commute Let_def Un_assoc sup_left_commute)

    have lookup_clause_rel_unique: ‹(D', a) ∈ lookup_clause_rel 𝒜 ⟹ (D', b) ∈ lookup_clause_rel 𝒜 ⟹ a = b›
      for a b 𝒜
      by (auto simp: lookup_clause_rel_def mset_as_position_right_unique)
    have isa_minimize_and_extract_highest_lookup_conflict:
      ‹isa_minimize_and_extract_highest_lookup_conflict ?M' ?arena
         (lookup_conflict_remove1 (-lit_of (hd M)) ?D') ?cach lbd (?outl[0 := - lit_of (hd M)])
      ≤ ⇓ {((E, s, outl), E').
            (E, mset (tl outl)) ∈ lookup_clause_rel (all_atms_st S) ∧
            mset outl = E' ∧
            outl ! 0 = - lit_of (hd M) ∧
            E' ⊆# the D ∧ outl ≠ [] ∧ distinct outl ∧ literals_are_in_ℒ⇩i⇩n (all_atms_st S) (mset outl) ∧
            ¬tautology (mset outl) ∧
	    (∃cach'. (s, cach') ∈ cach_refinement (all_atms_st S))}
          (SPEC (λE'. E' ⊆# add_mset (- lit_of (hd M)) (remove1_mset (- lit_of (hd M)) (the D)) ∧
              - lit_of (hd M) ∈# E' ∧
              mset `# ran_mf N +
              (get_unit_learned_clss_wl S + get_unit_init_clss_wl S +
                (get_subsumed_learned_clauses_wl S + get_subsumed_init_clauses_wl S) +
                 (get_learned_clauses0_wl S + get_init_clauses0_wl S)) ⊨pm
              E'))›
      (is ‹_ ≤ ⇓ ?minimize (RES ?E)›) for lbd
      apply (rule order_trans)
       apply (rule
          isa_minimize_and_extract_highest_lookup_conflict_minimize_and_extract_highest_lookup_conflict
          [THEN fref_to_Down_curry5,
            of ‹all_atms_st S› M N ‹remove1_mset (-lit_of (hd M)) (the D)› cach' lbd ‹?outl[0 := - lit_of (hd M)]›
            _ _ _ _ _ _ ‹?vdom›])
      subgoal using bounded by (auto simp: S all_atms_def)
      subgoal using tauto_confl' pre2 by auto
      subgoal using D' not_none arena S_T uL_D uM_ℒ⇩a⇩l⇩l not_empty D' L_D b cach_empty M'_M unfolding all_atms_def
        by (auto simp: option_lookup_clause_rel_def S state_wl_l_def image_image cach_refinement_empty_def cach'_def
            intro!: lookup_conflict_remove1[THEN fref_to_Down_unRET_uncurry]
            dest: multi_member_split lookup_clause_rel_unique)
      apply (rule order_trans)
       apply (rule mini[THEN ref_two_step'])
      subgoal
        using uL_D dist_D tauto_D ℒ⇩i⇩n_S ℒ⇩i⇩n_D tauto_D L_D
        by (auto 5 3 simp: conc_fun_chain conc_fun_RES image_iff S union_assoc insert_subset_eq_iff
            neq_Nil_conv literals_are_in_ℒ⇩i⇩n_add_mset tautology_add_mset
            intro: literals_are_in_ℒ⇩i⇩n_mono
            dest: distinct_mset_mono not_tautology_mono
            dest!: multi_member_split)
      done

    have empty_conflict_and_extract_clause_heur: ‹isa_empty_conflict_and_extract_clause_heur ?M' x1 x2a
          ≤ ⇓  ({((E, outl, n), E').
         (E, None) ∈ option_lookup_clause_rel (all_atms_st S) ∧
         mset outl = the E' ∧
         outl ! 0 = - lit_of (hd M) ∧
         the E' ⊆# the D ∧ outl ≠ [] ∧ E' ≠ None ∧
         (1 < length outl ⟶
            highest_lit M (mset (tl outl)) (Some (outl ! 1, get_level M (outl ! 1)))) ∧
         (1 < length outl ⟶ n = get_level M (outl ! 1)) ∧ (length outl = 1 ⟶ n = 0)}) (RETURN (Some E'))›
      (is ‹_ ≤ ⇓ ?empty_conflict _›)
      if
        ‹M ≠ []› and
        ‹- lit_of (hd M) ∈# ℒ⇩a⇩l⇩l (all_atms_st S)› and
        ‹0 < length ?outl› and
        ‹lookup_conflict_remove1_pre (- lit_of (hd M), ?D')› and
        ‹(x, E')  ∈ ?minimize› and
        ‹E' ∈ ?E› and
        ‹x2 = (x1a, x2a)› and
        ‹x = (x1, x2)›
      for x :: ‹(nat × bool option list) ×  (minimize_status list × nat list) × nat literal list› and
        E' :: ‹nat literal multiset› and
        x1 :: ‹nat × bool option list› and
        x2 :: ‹(minimize_status list × nat list) ×  nat literal list› and
        x1a :: ‹minimize_status list × nat list› and
        x2a :: ‹nat literal list›
    proof -
      show ?thesis
        apply (rule order_trans)
         apply (rule isa_empty_conflict_and_extract_clause_heur_empty_conflict_and_extract_clause_heur
            [THEN fref_to_Down_curry2, of _ _ _ M x1 x2a ‹all_atms_st S›])
          apply fast
        subgoal using M'_M by auto
        apply (subst Down_id_eq)
        apply (rule order.trans)
         apply (rule empty_conflict_and_extract_clause_heur_empty_conflict_and_extract_clause[of ‹mset (tl x2a)›])
        subgoal by auto
        subgoal using that by auto
        subgoal using that by auto
        subgoal using that by auto
        subgoal using that by auto
        subgoal using that by auto
        subgoal using bounded unfolding S all_atms_def by simp
        subgoal unfolding empty_conflict_and_extract_clause_def
          using that
          by (auto simp: conc_fun_RES RETURN_def)
        done
    qed
 
    have final: ‹((set_lbd_wl_heur lbd (set_ccach_max_wl_heur (empty_cach_ref x1a) (set_vmtf_wl_heur vm' (set_conflict_wl_heur x1b (set_outl_wl_heur (take 1 x2a) S')))), x2c, x1c),
          (M, N, Da, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W))
          ∈ ?shorter›  (is ‹((?updated_state, _, _), _) ∈ _›)
      if
        ‹M ≠ []› and
        ‹- lit_of (hd M) ∈# ℒ⇩a⇩l⇩l (all_atms_st S)› and
        ‹0 < length ?outl› and
        ‹lookup_conflict_remove1_pre (- lit_of (hd M), ?D')› and
        mini: ‹(x, E')  ∈ ?minimize› and
        ‹E' ∈ ?E› and
        ‹(xa, Da) ∈ ?empty_conflict› and
        st[simp]:
        ‹x2b = (x1c, x2c)›
        ‹x2 = (x1a, x2a)›
        ‹x = (x1, x2)›
        ‹xa = (x1b, x2b)› and
        vm': ‹(vm', uu) ∈ {(c, uu). c ∈ bump_heur (all_atms_st S) M}›
      for x E' x1 x2 x1a x2a xa Da x1b x2b x1c x2c vm' uu lbd
    proof -
      have x1b_None: ‹(x1b, None) ∈ option_lookup_clause_rel (all_atms_st S)›
        using that apply (auto simp: S simp flip: all_atms_def)
        done
      have cach[simp]: ‹cach_refinement_empty (all_atms_st S) (empty_cach_ref x1a)›
        using empty_cach_ref_empty_cach[of ‹all_atms_st S›, THEN fref_to_Down_unRET, of x1a]
          mini bounded
        by (auto simp add: cach_refinement_empty_def empty_cach_def cach'_def S
             simp flip: all_atms_def)

      have
        out: ‹out_learned M None (take (Suc 0) x2a)›  and
        x1c_Da: ‹mset x1c = the Da› and
        Da_None: ‹Da ≠ None› and
        Da_D: ‹the Da ⊆# the D› and
        x1c_D: ‹mset x1c ⊆# the D› and
        x1c: ‹x1c ≠ []› and
        hd_x1c: ‹hd x1c = - lit_of (hd M)› and
        highest: ‹Suc 0 < length x1c ⟹ x2c = get_level M (x1c ! 1) ∧
          highest_lit M (mset (tl x1c))
          (Some (x1c ! Suc 0, get_level M (x1c ! Suc 0)))› and
        highest2: ‹length x1c = Suc 0 ⟹ x2c = 0› and
        ‹E' = mset x2a› and
        ‹- lit_of (M ! 0) ∈ set x2a› and
        ‹(λx. mset (fst x)) ` set_mset (ran_m N) ∪
        (set_mset (get_unit_learned_clss_wl S) ∪ set_mset (get_unit_init_clss_wl S)) ∪
        (set_mset (get_subsumed_learned_clauses_wl S) ∪ set_mset (get_subsumed_init_clauses_wl S) ∪
        (set_mset (get_learned_clauses0_wl S) ∪ set_mset (get_init_clauses0_wl S))) ⊨p
        mset x2a› and
        ‹x2a ! 0 = - lit_of (M ! 0)› and
        ‹x1c ! 0 = - lit_of (M ! 0)› and
        ‹mset x2a ⊆# the D› and
        ‹mset x1c ⊆# the D› and
        ‹x2a ≠ []› and
        x1c_nempty: ‹x1c ≠ []› and
        ‹distinct x2a› and
        Da: ‹Da = Some (mset x1c)› and
        ‹literals_are_in_ℒ⇩i⇩n (all_atms_st S) (mset x2a)› and
        ‹¬ tautology (mset x2a)›
        using that
        unfolding out_learned_def
       	by (auto simp add: hd_conv_nth S ac_simps simp flip: all_atms_def)
      have Da_D': ‹remove1_mset (- lit_of (hd M)) (the Da) ⊆# remove1_mset (- lit_of (hd M)) (the D)›
        using Da_D mset_le_subtract by blast

      have K: ‹cdcl⇩W_restart_mset.cdcl⇩W_stgy_invariant (state⇩W_of U)›
        using stgy_invs unfolding twl_stgy_invs_def by fast
      have ‹get_maximum_level M {#L ∈# the D. get_level M L < count_decided M#}
        < count_decided M›
        using cdcl⇩W_restart_mset.no_skip_no_resolve_level_get_maximum_lvl_le[OF nss nsr all_struct K]
          not_none not_empty confl trail_nempty S_T T_U
        unfolding get_maximum_level_def by (auto simp: twl_st S)
      then have
        ‹get_maximum_level M (remove1_mset (- lit_of (hd M)) (the D)) < count_decided M›
        by (subst D_filter) auto
      then have max_lvl_le:
        ‹get_maximum_level M (remove1_mset (- lit_of (hd M)) (the Da)) < count_decided M›
        using get_maximum_level_mono[OF Da_D', of M] by auto
      have ‹(?updated_state, del_conflict_wl (M, N, Da, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W))
        ∈ twl_st_heur_bt›
        using S'_S x1b_None cach out vm' cach unfolding twl_st_heur_bt_def st
        by (auto simp: twl_st_heur_def del_conflict_wl_def S twl_st_heur_bt_def
            twl_st_heur_conflict_ana_def all_atms_st_def simp del: all_atms_st_def[symmetric])

      moreover have x2c: ‹x2c = get_maximum_level M (remove1_mset (- lit_of (hd M)) (the Da))›
        using highest highest2 x1c_nempty hd_x1c
        by (cases ‹length x1c = Suc 0›; cases x1c)
          (auto simp: highest_lit_def Da mset_tl)
      moreover have ‹literals_are_ℒ⇩i⇩n (all_atms_st S) (M, N, Some (mset x1c), NE, UE, NEk, UEk, NS, US, N0, U0, Q, W)›
        using ℒ⇩i⇩n
        by (auto simp: S x2c literals_are_ℒ⇩i⇩n_def blits_in_ℒ⇩i⇩n_def simp flip: all_atms_def)
      moreover have ‹¬tautology (mset x1c)›
        using tauto_confl  not_tautology_mono[OF x1c_D]
        by (auto simp: S x2c)
      ultimately show ?thesis
        using ℒ⇩i⇩n_S x1c_Da Da_None dist_D D_none x1c_D x1c hd_x1c highest uM_ℒ⇩a⇩l⇩l vm' M_ℒ⇩i⇩n
          max_lvl_le corr trail_nempty unfolding literals_are_ℒ⇩i⇩n_def all_lits_st_alt_def[symmetric]
        by (simp add:  S x2c is_ℒ⇩a⇩l⇩l_def all_lits_st_alt_def[symmetric],
          simp add: all_atms_st_def)
    qed
    have hd_M'_M: ‹lit_of_last_trail_pol ?M' = lit_of (hd M)›
      by (subst lit_of_last_trail_pol_lit_of_last_trail[THEN fref_to_Down_unRET_Id, of M ?M'])
        (use M'_M trail_nempty in ‹auto simp: lit_of_hd_trail_def›)

      have outl_hd_tl: ‹?outl[0 := - lit_of (hd M)] = - lit_of (hd M) # tl (?outl[0 := - lit_of (hd M)])› and
      [simp]: ‹?outl ≠ []›
      using outl unfolding out_learned_def
      by (cases ?outl; auto; fail)+
    have uM_D: ‹- lit_of (hd M) ∈# the D›
      by (subst D_filter) auto
    have mset_outl_D: ‹mset (?outl[0 := - lit_of (hd M)]) = (the D)›
      by (subst outl_hd_tl, subst mset.simps, subst tl_outl_D, subst D_filter)
        (use uM_D D_filter[symmetric] in auto)
    from arg_cong[OF this, of set_mset] have set_outl_D: ‹set (?outl[0 := - lit_of (hd M)]) = set_mset (the D)›
      by auto
    have outl_Lall: ‹∀L∈set (?outl[0 := - lit_of (hd M)]). L ∈# ℒ⇩a⇩l⇩l (all_atms_st S)›
      using ℒ⇩i⇩n_S unfolding set_outl_D
      by (auto simp: S all_lits_of_m_add_mset
          all_atms_def literals_are_in_ℒ⇩i⇩n_def literals_are_in_ℒ⇩i⇩n_in_mset_ℒ⇩a⇩l⇩l
          dest: multi_member_split)

    have vmtf_mark_to_rescore_also_reasons:
      ‹isa_vmtf_mark_to_rescore_also_reasons ?M' ?arena (?outl[0 := - lit_of (hd M)]) K ?vm
          ≤ SPEC (λc. (c, ()) ∈ {(c, _). c ∈ bump_heur (all_atms_st S) M})›
      if
        ‹M ≠ []› and
        ‹literals_are_in_ℒ⇩i⇩n_trail (all_atms_st S) M› and
        ‹- lit_of (hd M) ∈# ℒ⇩a⇩l⇩l (all_atms_st S)› and
        ‹0 < length ?outl› and
        ‹lookup_conflict_remove1_pre (- lit_of (hd M), ?D')›
      for K
    proof -
      have outl_Lall: ‹∀L∈set (?outl[0 := - lit_of (hd M)]). L ∈# ℒ⇩a⇩l⇩l (all_atms_st S)›
        using ℒ⇩i⇩n_S unfolding set_outl_D
        by (auto simp: S all_lits_of_m_add_mset
            all_atms_def literals_are_in_ℒ⇩i⇩n_def literals_are_in_ℒ⇩i⇩n_in_mset_ℒ⇩a⇩l⇩l
            dest: multi_member_split)
      have ‹distinct (?outl[0 := - lit_of (hd M)])› using dist_D by(auto simp: S mset_outl_D[symmetric])
      then have length_outl: ‹length ?outl ≤ unat32_max›
        using bounded tauto_confl ℒ⇩i⇩n_S simple_clss_size_upper_div2[OF bounded, of ‹mset (?outl[0 := - lit_of (hd M)])›]
        by (auto simp: out_learned_def S  mset_outl_D[symmetric] unat32_max_def simp flip: all_atms_def)
      have lit_annots: ‹∀L∈set (?outl[0 := - lit_of (hd M)]).
        ∀C. Propagated (- L) C ∈ set M ⟶
           C ≠ 0 ⟶
           C ∈# dom_m N ∧
           (∀C∈set [C..<C + arena_length ?arena C]. arena_lit ?arena C ∈# ℒ⇩a⇩l⇩l (all_atms_st S))›
        unfolding set_outl_D
        apply (intro ballI allI impI conjI)
        subgoal
          using list_invs S_T unfolding twl_list_invs_def
          by (auto simp: S)
        subgoal for L C i
          using list_invs S_T arena lits_N literals_are_in_ℒ⇩i⇩n_mm_in_ℒ⇩a⇩l⇩l[of ‹(all_atms_st S)› N C ‹i - C›]
          unfolding twl_list_invs_def
          by (auto simp: S arena_lifting all_atms_def[symmetric])
        done
      show ?thesis
        apply (cases ?vm)
        apply (rule order.trans,
            rule isa_vmtf_mark_to_rescore_also_reasons_vmtf_mark_to_rescore_also_reasons[of ‹all_atms_st S›,
              THEN fref_to_Down_curry4,
              of _ _ _ K ?vm M ?arena ‹?outl[0 := - lit_of (hd M)]› K ?vm])
        subgoal using bounded S by (auto simp: all_atms_def)
        subgoal using vm arena M'_M by (auto simp:)[]
        apply (rule order.trans, rule ref_two_step')
        apply (rule vmtf_mark_to_rescore_also_reasons_spec[OF _ arena _ _ outl_Lall lit_annots])
        subgoal using vm by auto
        subgoal using length_outl by auto
        subgoal using bounded by auto
        subgoal by (auto simp: conc_fun_RES S all_atms_def)
        done
    qed

(*TODO: needed because extract_shorter_conflict_wl_alt_def does not contain N0 + U0*)
    have ‹get_conflict U ≠ Some {#}›
      using struct_invs confl S_T T_U uL_D by auto
    then have ‹get_learned_clauses0 U = {#}›
      ‹get_init_clauses0 U = {#}›
      using struct_invs
      by (cases U; auto simp: twl_struct_invs_def pcdcl_all_struct_invs_def
        clauses0_inv_def)+
    then have clss0: ‹get_learned_clauses0_wl S = {#}›
      ‹get_init_clauses0_wl S = {#}›
      using S_T T_U by auto
    have GG[refine0]:‹⇓ {((E, s, outl), E').
       (E, mset (tl outl)) ∈ lookup_clause_rel (all_atms_st S) ∧
       mset outl = E' ∧
       outl ! 0 = - lit_of (hd M) ∧
       E' ⊆# the D ∧
       outl ≠ [] ∧
       distinct outl ∧
       literals_are_in_ℒ⇩i⇩n (all_atms_st S) (mset outl) ∧
       ¬ tautology (mset outl) ∧ (∃cach'. (s, cach') ∈ cach_refinement (all_atms_st S))}
     (SPEC
       (λE'. E' ⊆# add_mset (- lit_of (hd M)) (remove1_mset (- lit_of (hd M)) (the D)) ∧
             - lit_of (hd M) ∈# E' ∧
             mset `# ran_mf N +
             (get_unit_learned_clss_wl S + get_unit_init_clss_wl S +
              (get_subsumed_learned_clauses_wl S + get_subsumed_init_clauses_wl S) +
              (get_learned_clauses0_wl S + get_init_clauses0_wl S)) ⊨pm
             E'))
    ≤ ⇓ {((E, s, outl), E').
       (E, mset (tl outl)) ∈ lookup_clause_rel (all_atms_st S) ∧
       mset outl = E' ∧
       outl ! 0 = - lit_of (hd M) ∧
       E' ⊆# the D ∧
       outl ≠ [] ∧
       distinct outl ∧
       literals_are_in_ℒ⇩i⇩n (all_atms_st S) (mset outl) ∧
       ¬ tautology (mset outl) ∧ (∃cach'. (s, cach') ∈ cach_refinement (all_atms_st S))}
       (SPEC
         (λE'. E' ⊆# add_mset (- lit_of (hd M)) (remove1_mset (- lit_of (hd M)) (the D)) ∧
               - lit_of (hd M) ∈# E' ∧
               mset `# ran_mf N +
               (get_unit_learned_clss_wl S + get_unit_init_clss_wl S +
                (get_subsumed_learned_clauses_wl S + get_subsumed_init_clauses_wl S)) ⊨pm
  E'))›
      by (rule ref_two_step') (use clss0 in auto)
    show ?thesis
      supply [[goals_limit=1]]
      unfolding extract_shorter_conflict_list_heur_st_def
        empty_conflict_and_extract_clause_def S prod.simps
      apply (rewrite at  ‹let _ = list_update _ _ _ in _ ›Let_def)
      apply (rewrite at  ‹let _ =  get_trail_wl_heur S' in _ ›Let_def)
      apply (rewrite at  ‹let _ =  get_clauses_wl_heur S' in _ ›Let_def)
      apply (rewrite at  ‹let _ =  get_outlearned_heur S' in _ ›Let_def)
      apply (rewrite at  ‹let _ =  get_vmtf_heur S' in _ ›Let_def)
      apply (rewrite at  ‹let _ =  get_lbd S' in _ ›Let_def)
      apply (rewrite at  ‹let _ =  get_conflict_wl_heur S' in _ ›Let_def)
      apply (rewrite at  ‹let _ =  get_conflict_cach S' in _ ›Let_def)
      apply (rewrite at  ‹let _ = empty_cach_ref _ in _ › Let_def)
      unfolding hd_M'_M
      apply (subst case_prod_beta)
      apply (subst extract_shorter_conflict_wl_alt_def)
      apply (refine_vcg isa_minimize_and_extract_highest_lookup_conflict[THEN order_trans]
          empty_conflict_and_extract_clause_heur)
      subgoal
        apply (subst (2) Down_id_eq[symmetric], rule mark_lbd_from_list_heur_correctness[of _ M
          ‹(all_atms_st S)›])
        apply (use outl_Lall in ‹auto simp: M'_M literals_are_in_ℒ⇩i⇩n_def
            in_all_lits_of_m_ain_atms_of_iff in_ℒ⇩a⇩l⇩l_atm_of_𝒜⇩i⇩n›)
         by (cases ?outl) auto
      subgoal using trail_nempty using M'_M by (auto simp: trail_pol_def ann_lits_split_reasons_def)
      subgoal using ‹0 < length ?outl› .
      subgoal unfolding hd_M'_M[symmetric] by (rule lookup_conflict_remove1_pre)
        apply (rule vmtf_mark_to_rescore_also_reasons; assumption?)
      subgoal using trail_nempty .
      subgoal using pre2  by (auto simp: S all_atms_def)
      subgoal using uM_ℒ⇩a⇩l⇩l by (auto simp: S all_atms_def)
      subgoal premises p
        using bounded p by (auto simp: S empty_cach_ref_pre_def cach_refinement_alt_def
          intro!: IsaSAT_Lookup_Conflict.bounded_included_le simp: all_atms_def simp del: isasat_input_bounded_def
          intro: true_clss_cls_subsetI)
      subgoal by auto
      subgoal using bounded pre2
        by (auto dest!: simple_clss_size_upper_div2 simp: unat32_max_def S all_atms_def[symmetric]
            simp del: isasat_input_bounded_def)
      subgoal using trail_nempty by fast
      subgoal using uM_ℒ⇩a⇩l⇩l .
      apply (assumption)+
      subgoal
        using trail_nempty uM_ℒ⇩a⇩l⇩l
        unfolding S[symmetric]
        by (auto dest!: simp: clss0)
      apply assumption+
      subgoal for lbd uu vm uua x E' x1 x2 x1a x2a xa Da a b aa ba
        using trail_nempty uM_ℒ⇩a⇩l⇩l apply -
        unfolding S[symmetric] all_lits_alt_def[symmetric]
        by (rule final[unfolded clss0 Multiset.empty_neutral])
      done
  qed

  have find_decomp_wl_nlit: ‹find_decomp_wl_st_int n T
      ≤ ⇓  {(U, U''). (U, U'') ∈ twl_st_heur_bt ∧ equality_except_trail_wl U'' T' ∧
       (∃K M2. (Decided K # (get_trail_wl U''), M2) ∈ set (get_all_ann_decomposition (get_trail_wl T')) ∧
          get_level (get_trail_wl T') K = get_maximum_level (get_trail_wl T') (the (get_conflict_wl T') - {#-lit_of (hd (get_trail_wl T'))#}) + 1 ∧
          get_clauses_wl_heur U = get_clauses_wl_heur S ∧
          get_learned_count U = get_learned_count S) ∧
	  (get_trail_wl U'', get_vmtf_heur U) ∈ (Id ×⇩f Id)¯ ``
	    (Collect (find_decomp_w_ns_prop (all_atms_st T') (get_trail_wl T') n (get_vmtf_heur T)))}
          (find_decomp_wl LK' T')›
    (is ‹_ ≤  ⇓ ?find_decomp _›)
    if
      ‹(S, S') ∈ ?R› and
      ‹backtrack_wl_inv S'› and
      ‹backtrack_wl_D_heur_inv S› and
      TT': ‹(TnC, T') ∈ ?shorter S' S› and
      [simp]: ‹nC = (n, C)› and
      [simp]: ‹TnC = (T, nC)› and
       KK': ‹(LK, LK') ∈ {(L, L'). L = L' ∧ L = lit_of (hd (get_trail_wl S'))}›
    for S S' TnC T' T nC n C LK LK'
  proof -
    obtain M N D NE UE NEk UEk NS US N0 U0 Q W where
      T': ‹T' = (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W)›
      by (cases T')

    let ?M' = ‹get_trail_wl_heur T›
    let ?arena = ‹get_clauses_wl_heur T›
    let ?D' = ‹get_conflict_wl_heur T›
    let ?W' = ‹get_watched_wl_heur T›
    let ?vm = ‹get_vmtf_heur T›
    let ?clvls = ‹get_count_max_lvls_heur T›
    let ?cach = ‹get_conflict_cach T›
    let ?outl = ‹get_outlearned_heur T›
    let ?lcount = ‹get_learned_count T›
    let ?aivdom = ‹get_aivdom T›

    let ?vdom = ‹set (get_vdom_aivdom ?aivdom)›
    (* obtain M' W' vm clvls cach lbd outl stats arena D' Q' heur vdom lcount opts old_arena where
     *   T: ‹T = (M', arena, D', Q', W', vm, clvls, cach, lbd, outl, stats, heur, vdom, lcount,
     *      opts, old_arena)›
     *   using TT' by (cases T) (auto simp: twl_st_heur_bt_def T' del_conflict_wl_def) *)
    have
      vm: ‹?vm ∈ bump_heur (all_atms_st T') M› and
      M'M: ‹(?M', M) ∈ trail_pol (all_atms_st T')› and
      lits_trail: ‹literals_are_in_ℒ⇩i⇩n_trail (all_atms_st T') (get_trail_wl T')›
      using TT' by (auto simp: twl_st_heur_bt_def del_conflict_wl_def all_atms_st_def
          all_atms_def[symmetric] T' all_lits_st_alt_def[symmetric])

    have [simp]:
       ‹LK' = lit_of (hd (get_trail_wl T'))›
       ‹LK = LK'›
       using KK' TT' by (auto simp: equality_except_conflict_wl_get_trail_wl)

    have n: ‹n = get_maximum_level M (remove1_mset (- lit_of (hd M)) (mset C))› and
      eq: ‹equality_except_conflict_wl T' S'› and
      ‹the D = mset C› ‹D ≠ None› and
      clss_eq: ‹get_clauses_wl_heur S = ?arena› and
      n: ‹n < count_decided (get_trail_wl T')› and
      bounded: ‹isasat_input_bounded (all_atms_st T')› and
      T_T': ‹(T, del_conflict_wl T') ∈ twl_st_heur_bt› and
      n2: ‹n = get_maximum_level M (remove1_mset (- lit_of (hd M)) (the D))› and
      lcount: ‹get_learned_count T = get_learned_count S›
      using TT' KK' by (auto simp: T' twl_st_heur_bt_def del_conflict_wl_def all_atms_st_def
          T' all_lits_st_alt_def[symmetric] simp flip: all_atms_def
          simp del: isasat_input_bounded_def)
    have [simp]: ‹get_trail_wl S' = M›
      using eq ‹the D = mset C› ‹D ≠ None› by (cases S'; auto simp: T')
    have [simp]: ‹get_clauses_wl_heur S = ?arena›
      using TT' by (auto simp: T')

    have n_d: ‹no_dup M›
      using M'M unfolding trail_pol_def by auto

    have [simp]: ‹NO_MATCH [] M ⟹ out_learned M None ai ⟷ out_learned [] None ai› for M ai
      by (auto simp: out_learned_def)

    show ?thesis
      unfolding T' find_decomp_wl_st_int_def prod.case Let_def
      apply (rule bind_refine_res)
       prefer 2
       apply (rule order.trans)
        apply (rule isa_find_decomp_wl_imp_find_decomp_wl_imp[THEN fref_to_Down_curry2, of M n ?vm
            _ _ _ ‹all_atms_st T'›])
      subgoal using n by (auto simp: T')
      subgoal using M'M vm by auto
       apply (rule order.trans)
        apply (rule ref_two_step')
        apply (rule find_decomp_wl_imp_le_find_decomp_wl')
      subgoal using vm .
      subgoal using lits_trail by (auto simp: T')
      subgoal using n by (auto simp: T')
      subgoal using n_d .
      subgoal using bounded .
      subgoal using n by (auto simp: T')
      unfolding find_decomp_w_ns_def conc_fun_RES
       apply (rule order.refl)
      using T_T' n_d lcount (*TODO Tune proof*)
      apply (cases ‹get_vmtf_heur T›)
      apply (auto simp: find_decomp_wl_def twl_st_heur_bt_def T' del_conflict_wl_def
          dest: no_dup_appendD
          simp flip: all_atms_def n2
          intro!: RETURN_RES_refine
          intro: )
      by (auto dest: no_dup_appendD intro:  simp: T' all_atms_st_def)
  qed

  have fst_find_lit_of_max_level_wl: ‹RETURN (C ! 1)
      ≤ ⇓ Id
          (find_lit_of_max_level_wl U' LK')›
    if
      ‹(S, S') ∈ ?R› and
      ‹backtrack_wl_inv S'› and
      ‹backtrack_wl_D_heur_inv S› and
      TT': ‹(TnC, T') ∈ ?shorter S' S› and
      [simp]: ‹nC = (n, C)› and
      [simp]: ‹TnC = (T, nC)› and
      find_decomp: ‹(U, U') ∈ ?find_decomp S T' n› and
      size_C: ‹1 < length C› and
      size_conflict_U': ‹1 < size (the (get_conflict_wl U'))› and
       KK': ‹(LK, LK') ∈ {(L, L'). L = L' ∧ L = lit_of (hd (get_trail_wl S'))}›
    for S S' TnC T' T nC n C U U' LK LK'
  proof -
    obtain M N NE UE Q W NEk UEk NS US N0 U0 where
      T': ‹T' = (M, N, Some (mset C), NE, UE, NEk, UEk, NS, US, N0, U0, Q, W)› and
      ‹C ≠ []›
      using ‹(TnC, T') ∈ ?shorter S' S› ‹1 < length C› find_decomp
      apply (cases U'; cases T'; cases S')
      by (auto simp: find_lit_of_max_level_wl_def)

    obtain M' K M2 where
      U': ‹U' = (M', N, Some (mset C), NE, UE, NEk, UEk, NS, US, N0, U0, Q, W)› and
      decomp: ‹(Decided K # M', M2) ∈ set (get_all_ann_decomposition M)› and
      lev_K: ‹get_level M K = Suc (get_maximum_level M (remove1_mset (- lit_of (hd M)) (the (Some (mset C)))))›
      using ‹(TnC, T') ∈ ?shorter S' S› ‹1 < length C› find_decomp
      by (cases U'; cases S')
        (auto simp: find_lit_of_max_level_wl_def T' all_atms_st_def)

    have [simp]:
       ‹LK' = lit_of (hd (get_trail_wl T'))›
       ‹LK = LK'›
       using KK' TT' by (auto simp: equality_except_conflict_wl_get_trail_wl)

    have n_d: ‹no_dup (get_trail_wl S')›
      using ‹(S, S') ∈ ?R›
      by (auto simp: twl_st_heur_conflict_ana_def trail_pol_def)

    have [simp]: ‹get_trail_wl S' = get_trail_wl T'›
      using ‹(TnC, T') ∈ ?shorter S' S› ‹1 < length C› find_decomp
      by (cases T'; cases S'; auto simp: find_lit_of_max_level_wl_def U'; fail)+
    have [simp]: ‹remove1_mset (- lit_of (hd M)) (mset C) = mset (tl C)›
      apply (subst mset_tl)
      using ‹(TnC, T') ∈ ?shorter S' S›
      by (auto simp: find_lit_of_max_level_wl_def U' highest_lit_def T')

    have n_d: ‹no_dup M›
      using ‹(TnC, T') ∈ ?shorter S' S› n_d unfolding T'
      by (cases S') auto

    have nempty[iff]: ‹remove1_mset (- lit_of (hd M)) (the (Some(mset C))) ≠ {#}›
      using U' T' find_decomp size_C by (cases C) (auto simp: remove1_mset_empty_iff)
    have H[simp]: ‹aa ∈# remove1_mset (- lit_of (hd M)) (the (Some(mset C))) ⟹
       get_level M' aa = get_level M aa› for aa
      apply (rule get_all_ann_decomposition_get_level[of ‹lit_of (hd M)› _ K _ M2 ‹the (Some(mset C))›])
      subgoal ..
      subgoal by (rule n_d)
      subgoal by (rule decomp)
      subgoal by (rule lev_K)
      subgoal by simp
      done

    have ‹get_maximum_level M (remove1_mset (- lit_of (hd M)) (mset C)) =
       get_maximum_level M' (remove1_mset (- lit_of (hd M)) (mset C))›
      by (rule get_maximum_level_cong) auto
    then show ?thesis
      using ‹(TnC, T') ∈ ?shorter S' S› ‹1 < length C› hd_conv_nth[OF ‹C ≠ []›, symmetric]
      by (auto simp: find_lit_of_max_level_wl_def U' highest_lit_def T')
  qed

  have propagate_bt_wl_D_heur: ‹propagate_bt_wl_D_heur LK C U
      ≤ ⇓ ?S (propagate_bt_wl LK' L' U')›
    if
      SS': ‹(S, S') ∈ ?R› and
      ‹backtrack_wl_inv S'› and
      ‹backtrack_wl_D_heur_inv S› and
      ‹(TnC, T') ∈ ?shorter S' S› and
      [simp]: ‹nC = (n, C)› and
      [simp]: ‹TnC = (T, nC)› and
      find_decomp: ‹(U, U') ∈ ?find_decomp S T' n› and
      le_C: ‹1 < length C› and
      ‹1 < size (the (get_conflict_wl U'))› and
      C_L': ‹(C ! 1, L') ∈ nat_lit_lit_rel› and
      KK': ‹(LK, LK') ∈ {(L, L'). L = L' ∧ L = lit_of (hd (get_trail_wl S'))}›
    for S S' TnC T' T nC n C U U' L' LK LK'
  proof -

    have
      TT': ‹(T, del_conflict_wl T') ∈ twl_st_heur_bt› and
      n: ‹n = get_maximum_level (get_trail_wl T')
          (remove1_mset (- lit_of (hd (get_trail_wl T'))) (mset C))› and
      T_C: ‹get_conflict_wl T' = Some (mset C)› and
      T'S': ‹equality_except_conflict_wl T' S'› and
      C_nempty: ‹C ≠ []› and
      hd_C: ‹hd C = - lit_of (hd (get_trail_wl T'))› and
      highest: ‹highest_lit (get_trail_wl T') (mset (tl C))
         (Some (C ! Suc 0, get_level (get_trail_wl T') (C ! Suc 0)))› and
      incl: ‹mset C ⊆# the (get_conflict_wl S')› and
      dist_S': ‹distinct_mset (the (get_conflict_wl S'))› and
      list_confl_S': ‹literals_are_in_ℒ⇩i⇩n (all_atms_st S') (the (get_conflict_wl S'))› and
      ‹get_conflict_wl S' ≠ None› and
      uM_ℒ⇩a⇩l⇩l: ‹-lit_of (hd (get_trail_wl S')) ∈# ℒ⇩a⇩l⇩l (all_atms_st S')› and
      lits: ‹literals_are_ℒ⇩i⇩n (all_atms_st T') T'› and
      tr_nempty: ‹get_trail_wl T' ≠ []› and
      r: ‹length (get_clauses_wl_heur S) = r› ‹length (get_clauses_wl_heur T) = r›
        ‹get_learned_count T = get_learned_count S› ‹learned_clss_count S ≤ u› and
      corr: ‹correct_watching S'›
      using ‹(TnC, T') ∈ ?shorter S' S›  ‹1 < length C› ‹(S, S') ∈ ?R›
      by auto

    obtain K M2 where
      UU': ‹(U, U') ∈ twl_st_heur_bt› and
      U'U': ‹equality_except_trail_wl U' T'› and
      lev_K: ‹get_level (get_trail_wl T') K = Suc (get_maximum_level (get_trail_wl T')
           (remove1_mset (- lit_of (hd (get_trail_wl T')))
             (the (get_conflict_wl T'))))› and
      decomp: ‹(Decided K # get_trail_wl U', M2) ∈ set (get_all_ann_decomposition (get_trail_wl T'))› and
      r': ‹length (get_clauses_wl_heur U) = r› 
        ‹get_learned_count U = get_learned_count T›
        ‹learned_clss_count U ≤ u› and
      S_arena: ‹get_clauses_wl_heur U = get_clauses_wl_heur S›
      using find_decomp r get_learned_count_learned_clss_countD2[of U T]
        get_learned_count_learned_clss_countD2[of T S]
      by (auto dest: )

    obtain M N NE UE NEk UEk Q NS US N0 U0 W where
      T': ‹T' = (M, N, Some (mset C), NE, UE, NEk, UEk, NS, US, N0, U0, Q, W)› and
      ‹C ≠ []›
      using TT' T_C ‹1 < length C›
      apply (cases T'; cases S')
      by (auto simp: find_lit_of_max_level_wl_def)
    obtain D where
      S': ‹S' = (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W)›
      using T'S' ‹1 < length C›
      apply (cases S')
      by (auto simp: find_lit_of_max_level_wl_def T' del_conflict_wl_def)

    obtain M1 where
      U': ‹U' = (M1, N, Some (mset C), NE, UE, NEk, UEk, NS, US, N0, U0, Q, W)› and
      lits_confl: ‹literals_are_in_ℒ⇩i⇩n (all_atms_st S') (mset C)› and
      ‹mset C ⊆# the (get_conflict_wl S')› and
      tauto: ‹¬ tautology (mset C)›
      using ‹(TnC, T') ∈ ?shorter S' S› ‹1 < length C› find_decomp
      apply (cases U')
      by (auto simp: find_lit_of_max_level_wl_def T' intro: literals_are_in_ℒ⇩i⇩n_mono)

    let ?M1' = ‹get_trail_wl_heur U›
    let ?arena = ‹get_clauses_wl_heur U›
    let ?D' = ‹get_conflict_wl_heur U›
    let ?W' = ‹get_watched_wl_heur U›
    let ?vm' = ‹get_vmtf_heur U›
    let ?clvls = ‹get_count_max_lvls_heur U›
    let ?cach = ‹get_conflict_cach U›
    let ?outl = ‹get_outlearned_heur U›
    let ?lcount = ‹get_learned_count U›
    let ?heur = ‹get_heur U›
    let ?lbd = ‹get_lbd U›
    let ?aivdom = ‹get_aivdom U›

    let ?vdom = ‹set (get_vdom_aivdom ?aivdom)›
    (* obtain M1' vm' W' clvls cach lbd outl stats heur vdom lcount arena D'
     *     Q' opts
     *   where
     *     U: ‹U = (M1', arena, D', Q', W', vm', clvls, cach, lbd, outl, stats, heur,
     *        vdom, lcount, opts, [])›
     *    *)
    have old: ‹get_old_arena U = []›
      using UU' find_decomp by (cases U) (auto simp: U' T' twl_st_heur_bt_def all_atms_def[symmetric])
    have [simp]:
       ‹LK' = lit_of (hd M)›
       ‹LK = LK'›
       using KK' SS' by (auto simp: equality_except_conflict_wl_get_trail_wl S')
    have
      M1'_M1: ‹(?M1', M1) ∈ trail_pol (all_atms_st U')› and
      W'W: ‹(?W', W) ∈ ⟨Id⟩map_fun_rel (D⇩0 (all_atms_st U'))› and
      vmtf: ‹?vm' ∈ bump_heur (all_atms_st U') M1› and
      n_d_M1: ‹no_dup M1› and
      empty_cach: ‹cach_refinement_empty (all_atms_st U') ?cach› and
      ‹length ?outl = Suc 0› and
      outl: ‹out_learned M1 None ?outl› and
      vdom: ‹vdom_m (all_atms_st U') W N ⊆ ?vdom› and
      lcount: ‹clss_size_corr N NE UE NEk UEk NS US N0 U0 ?lcount› and
      vdom_m: ‹vdom_m (all_atms_st U') W N ⊆ ?vdom› and
      D': ‹(?D', None) ∈ option_lookup_clause_rel (all_atms_st U')› and
      valid: ‹valid_arena ?arena N ?vdom› and
      aivdom: ‹aivdom_inv_dec ?aivdom (dom_m N)› and
      bounded: ‹isasat_input_bounded (all_atms_st U')› and
      nempty: ‹isasat_input_nempty (all_atms_st U')› and
      dist_vdom: ‹distinct (get_vdom_aivdom ?aivdom)› and
      heur: ‹heuristic_rel (all_atms_st U') ?heur› and
      occs: ‹(get_occs U, empty_occs_list (all_atms_st U')) ∈ occurrence_list_ref›
      using UU' by (auto simp: out_learned_def twl_st_heur_bt_def U' all_atms_def[symmetric]
        aivdom_inv_dec_alt_def)
    have [simp]: ‹C ! 1 = L'› ‹C ! 0 = - lit_of (hd M)› and
      n_d: ‹no_dup M›
      using SS' C_L' hd_C ‹C ≠ []› by (auto simp: S' U' T' twl_st_heur_conflict_ana_def hd_conv_nth)
    have undef: ‹undefined_lit M1 (lit_of (hd M))›
      using decomp n_d
      by (auto dest!: get_all_ann_decomposition_exists_prepend simp: T' hd_append U' neq_Nil_conv
          split: if_splits)
    have C_1_neq_hd: ‹C ! Suc 0 ≠ - lit_of (hd M)›
      using distinct_mset_mono[OF incl dist_S'] C_L' ‹1 < length C›  ‹C ! 0 = - lit_of (hd M)›
      by (cases C; cases ‹tl C›) (auto simp del: ‹C ! 0 = - lit_of (hd M)›)
    have H: ‹(RES ((λi. (fmupd i (C, False) N, i)) ` {i. 0 < i ∧ i ∉# dom_m N}) ⤜
                   (λ(N, i).  ASSERT (i ∈# dom_m N) ⤜ (λ_. f N i))) =
          (RES ((λi. (fmupd i (C, False) N, i)) ` {i. 0 < i ∧ i ∉# dom_m N}) ⤜
                   (λ(N, i). f N i))› (is ‹?A = ?B›) for f C N
    proof -
      have ‹?B ≤ ?A›
        by (force intro: ext complete_lattice_class.Sup_subset_mono
          simp: intro_spec_iff bind_RES)
      moreover have ‹?A ≤ ?B›
        by (force intro: ext complete_lattice_class.Sup_subset_mono
          simp: intro_spec_iff bind_RES)
      ultimately show ?thesis by auto
    qed

    have propagate_bt_wl_D_heur_alt_def:
      ‹propagate_bt_wl_D_heur = (λL C S. do {
          let M = get_trail_wl_heur S;
          let vdom = get_aivdom S;
          let N0 = get_clauses_wl_heur S;
          let W0 = get_watched_wl_heur S;
          let lcount = get_learned_count S;
          let heur = get_heur S;
          let stats = get_stats_heur S;
          let lbd = get_lbd S;
          let vm0 = get_vmtf_heur S;
          ASSERT(length (get_vdom_aivdom vdom) ≤ length N0);
          ASSERT(length (get_avdom_aivdom vdom) ≤ length N0);
          ASSERT(nat_of_lit (C!1) < length W0 ∧ nat_of_lit (-L) < length W0);
          ASSERT(length C > 1);
          let L' = C!1;
          ASSERT (length C ≤ unat32_max div 2 + 1);
          vm ← isa_bump_rescore C M vm0;
          glue ← get_LBD lbd;
          let _ = C;
          let b = False;
          ASSERT(isasat_fast S ⟶ append_and_length_fast_code_pre ((b, C), N0));
          ASSERT(isasat_fast S ⟶ clss_size_lcount lcount < snat64_max);
          (N, i) ← fm_add_new b C N0;
          ASSERT(update_lbd_pre ((i, glue), N));
          let N = update_lbd_and_mark_used i glue N;
          ASSERT(isasat_fast S ⟶ length_ll W0 (nat_of_lit (-L)) < snat64_max);
          let W = W0[nat_of_lit (- L) := W0 ! nat_of_lit (- L) @ [(i, L', length C = 2)]];
          ASSERT(isasat_fast S ⟶ length_ll W (nat_of_lit L') < snat64_max);
          let W = W[nat_of_lit L' := W!nat_of_lit L' @ [(i, -L, length C = 2)]];
          lbd ← lbd_empty lbd;
          j ← mop_isa_length_trail M;
          ASSERT(i ≠ DECISION_REASON);
          ASSERT(cons_trail_Propagated_tr_pre ((-L, i), M));
          M ← cons_trail_Propagated_tr (- L) i M;
          vm ← isa_bump_heur_flush M vm;
          heur ← mop_save_phase_heur (atm_of L') (is_neg L') heur;
         let
            S = set_watched_wl_heur W S;
            S = set_learned_count_wl_heur (clss_size_incr_lcount lcount) S;
            S = set_aivdom_wl_heur (add_learned_clause_aivdom i vdom) S;
            S = set_heur_wl_heur (unset_fully_propagated_heur (heuristic_reluctant_tick (update_propagation_heuristics glue heur))) S;
            S = set_stats_wl_heur (add_lbd (word_of_nat glue) stats) S; S = set_trail_wl_heur M S;
            S = set_clauses_wl_heur N S; S = set_literals_to_update_wl_heur j S;
            S = set_count_max_wl_heur 0 S; S = set_vmtf_wl_heur vm S;
            S = set_lbd_wl_heur lbd S in
           do {_ ← log_new_clause_heur S i;
           S ← maybe_mark_added_clause_heur2 S i;
          RETURN S}
      })›
      unfolding propagate_bt_wl_D_heur_def Let_def
      by (auto intro!: ext bind_cong[OF refl])
    have find_new_alt: ‹SPEC
                 (λ(N', i). N' = fmupd i (D'', False) N ∧ 0 < i ∧
                      i ∉# dom_m N ∧
                      (∀L∈#all_lits_of_mm (mset `# ran_mf N + (NE + UE) + (NEk + UEk)  + (NS + US) + (N0 + U0)).
                          i ∉ fst ` set (W L))) = do {

          i ← SPEC
                 (λi. 0 < i ∧
                      i ∉# dom_m N ∧
                      (∀L∈#all_lits_of_mm (mset `# ran_mf N + (NE + UE)  + (NEk + UEk) + (NS + US) + (N0 + U0)).
                          i ∉ fst ` set (W L)));
         N' ← RETURN (fmupd i (D'', False) N);
         RETURN (N', i)
      }› for D''
      by (auto simp: RETURN_def RES_RES_RETURN_RES2
       RES_RES_RETURN_RES)
    have propagate_bt_wl_D_alt_def:
      ‹propagate_bt_wl LK' L' U' = do {
            ASSERT (propagate_bt_wl_pre LK' L' (M1, N, Some (mset C), NE, UE, NEk, UEk, NS, US, N0, U0, Q, W));
            _ ← RETURN (); ⌦‹phase saving›
            _ ← RETURN (); ⌦‹LBD›
            D'' ←
              list_of_mset2 (- LK') L'
               (the (Some (mset C)));
            (N, i) ← SPEC
                 (λ(N', i). N' = fmupd i (D'', False) N ∧ 0 < i ∧
                      i ∉# dom_m N ∧
                      (∀L∈#all_lits_of_mm (mset `# ran_mf N + (NE + UE) + (NEk + UEk) + (NS + US) + (N0 + U0)).
                          i ∉ fst ` set (W L)));
            _ ← RETURN (); ⌦‹lbd empty›
            _ ← RETURN (); ⌦‹lbd empty›
	     M2 ← cons_trail_propagate_l (- LK') i M1;
            _ ← RETURN (); ⌦‹vmtf_flush›
            _ ← RETURN (); ⌦‹heur›
            _ ← RETURN (log_clause (M2,
                N, None, NE, UE, NEk, UEk, NS, US, N0, U0, {#LK'#},
                W(- LK' := W (- LK') @ [(i, L', length D'' = 2)],
                  L' := W L' @ [(i, - LK', length D'' = 2)])) i);
            let S = (M2,
                N, None, NE, UE, NEk, UEk, NS, US, N0, U0, {#LK'#},
                W(- LK' := W (- LK') @ [(i, L', length D'' = 2)],
                  L' := W L' @ [(i, - LK', length D'' = 2)]));
            RETURN S
          }›
      unfolding propagate_bt_wl_def Let_def find_new_alt nres_monad3
        U' H get_fresh_index_wl_def prod.case
        propagate_bt_wl_def Let_def rescore_clause_def
      by (auto simp: U' RES_RES2_RETURN_RES RES_RETURN_RES uminus_𝒜⇩i⇩n_iff
          uncurry_def RES_RES_RETURN_RES length_list_ge2 C_1_neq_hd
          get_fresh_index_def RES_RETURN_RES2 RES_RES_RETURN_RES2 list_of_mset2_def
          cons_trail_propagate_l_def ac_simps
          intro!: bind_cong[OF refl]
          simp flip: all_lits_alt_def2 all_lits_alt_def all_lits_def)

    have [refine0]: ‹SPEC (λ(vm'). vm' ∈ bump_heur 𝒜 M1)
       ≤ ⇓{((vm'), ()). vm' ∈ bump_heur 𝒜 M1 } (RETURN ())› for 𝒜
      by (auto intro!: RES_refine simp: RETURN_def)

    have [refine0]:
      ‹isa_bump_rescore C ?M1' ?vm' ≤ SPEC (λc. (c, ()) ∈ {((vm), _).
         vm ∈ bump_heur (all_atms_st U') M1})›
      apply (rule order.trans)
       apply (rule isa_vmtf_rescore[of ‹all_atms_st U'›, THEN fref_to_Down_curry2, of _ _ _ C M1 ?vm'])
      subgoal using bounded by auto
      subgoal using M1'_M1 vmtf by auto
      apply (rule order.trans)
       apply (rule ref_two_step')
       apply (rule vmtf_rescore_score_clause[THEN fref_to_Down_curry2, of ‹all_atms_st U'› C M1 ?vm'])
      subgoal using vmtf lits_confl bounded by (auto simp: S' U' all_atms_st_def)
      subgoal using vmtf M1'_M1 by auto
      subgoal by (auto simp: rescore_clause_def conc_fun_RES isa_rescore_clause_def)
      done

    have [refine0]: ‹isa_bump_heur_flush Ma vm ≤
         SPEC(λc. (c, ()) ∈ {(vm', _). vm' ∈ bump_heur (all_atms_st U') M2})›
      if vm: ‹vm ∈ bump_heur (all_atms_st U') M1› and
       Ma: ‹(Ma, M2)
       ∈ {(M0, M0'').
         (M0, M0'') ∈ trail_pol (all_atms_st U') ∧
         M0'' = Propagated (- L) i # M1 ∧
         no_dup M0''}›
      for vm i L Ma M2
    proof -
      let ?M1' = ‹cons_trail_Propagated_tr L i ?M1'›
      let ?M1 = ‹Propagated (-L) i # M1›

      have M1'_M1: ‹(Ma, M2) ∈ trail_pol (all_atms_st U')›
        using Ma by auto

      have vm: ‹vm ∈ bump_heur (all_atms_st U') ?M1›
        using vm by (auto simp: dest: isa_vmtf_consD)
      show ?thesis
      	apply (rule order.trans)
        apply (rule isa_bump_heur_flush_isa_bump_flush[THEN fref_to_Down_curry, of ‹all_atms_st U'› ?M1 vm])
        subgoal by (use M1'_M1 Ma bounded vm nempty in auto)
        subgoal by (use M1'_M1 Ma bounded vm nempty in auto)
        subgoal using Ma by (auto simp: isa_bump_flush_def)
      	done
    qed

    have [refine0]: ‹(mop_isa_length_trail ?M1') ≤ ⇓ {(j, _). j = length M1} (RETURN ())›
      by (rule order_trans[OF mop_isa_length_trail_length_u[THEN fref_to_Down_Id_keep, OF _ M1'_M1]])
         (auto simp: conc_fun_RES RETURN_def)
    have [refine0]: ‹get_LBD ?lbd ≤ ⇓ {(_, _). True}(RETURN ())›
      unfolding get_LBD_def by (auto intro!: RES_refine simp: RETURN_def)
    have [refine0]: ‹RETURN C
       ≤ ⇓ Id
          (list_of_mset2 (- LK') L'
            (the (Some (mset C))))›
      using that
      by (auto simp: list_of_mset2_def S')
    have [simp]: ‹0 < header_size D''› for D''
      by (auto simp: header_size_def)
    have [simp]: ‹length ?arena + header_size D'' ∉ ?vdom›
      ‹length ?arena + header_size D'' ∉ vdom_m (all_atms_st U') W N›
      ‹length ?arena + header_size D'' ∉# dom_m N› for D''
      using valid_arena_in_vdom_le_arena(1)[OF valid] vdom
      by (auto 5 1 simp: vdom_m_def)
    have add_new_alt_def: ‹(SPEC
            (λ(N', i).
                N' = fmupd i (D'', False) N ∧
                0 < i ∧
                i ∉# dom_m N ∧
                (∀L∈#all_lits_of_mm (mset `# ran_mf N + (NE + UE)  + (NEk + UEk) + (NS + US) + (N0 + U0)).
                    i ∉ fst ` set (W L)))) =
          (SPEC
            (λ(N', i).
                N' = fmupd i (D'', False) N ∧
                0 < i ∧
                i ∉ vdom_m (all_atms_st U') W N))› for D''
      using lits
      by (auto simp: T' vdom_m_def literals_are_ℒ⇩i⇩n_def is_ℒ⇩a⇩l⇩l_def U' all_atms_def
        all_lits_st_def all_lits_def ac_simps)
    have [refine0]: ‹fm_add_new False C ?arena
       ≤ ⇓ {((arena', i), (N', i')). valid_arena arena' N' (insert i ?vdom) ∧ i = i' ∧
             i ∉# dom_m N ∧ i ∉ ?vdom ∧ length arena' = length ?arena + header_size D'' + length D''}
          (SPEC
            (λ(N', i).
                N' = fmupd i (D'', False) N ∧
                0 < i ∧
                i ∉# dom_m N ∧
                (∀L∈#all_lits_of_mm (mset `# ran_mf N + (NE + UE)  + (NEk + UEk) + (NS + US) + (N0 + U0)).
                    i ∉ fst ` set (W L))))›
      if ‹(C, D'') ∈ Id› for D''
      apply (subst add_new_alt_def)
      apply (rule order_trans)
       apply (rule fm_add_new_append_clause)
      using that valid le_C vdom
      by (auto simp: intro!: RETURN_RES_refine valid_arena_append_clause)
    have [refine0]:
      ‹lbd_empty ?lbd ≤ SPEC (λc. (c, ()) ∈ {(c, _). c = replicate (length ?lbd) False})›
      by (auto simp: lbd_empty_def)

    have ‹literals_are_in_ℒ⇩i⇩n (all_atms_st S') (mset C)›
      using incl list_confl_S' literals_are_in_ℒ⇩i⇩n_mono by blast
    then have C_Suc1_in: ‹C ! Suc 0 ∈# ℒ⇩a⇩l⇩l (all_atms_st S')›
      using ‹1 < length C›
      by (cases C; cases ‹tl C›) (auto simp: literals_are_in_ℒ⇩i⇩n_add_mset)
    then have ‹nat_of_lit (C ! Suc 0) < length ?W'› ‹nat_of_lit (- lit_of (hd (get_trail_wl S'))) < length ?W'› and
     W'_eq:  ‹?W' ! (nat_of_lit (C ! Suc 0)) = W (C! Suc 0)›
        ‹?W' ! (nat_of_lit (- lit_of (hd (get_trail_wl S')))) = W (- lit_of (hd (get_trail_wl S')))›
      using uM_ℒ⇩a⇩l⇩l W'W unfolding map_fun_rel_def by (auto simp: image_image S' U' all_atms_st_def)
    have le_C_ge: ‹length C ≤ unat32_max div 2 + 1›
      using clss_size_unat32_max[OF bounded, of ‹mset C›] ‹literals_are_in_ℒ⇩i⇩n (all_atms_st S') (mset C)› list_confl_S'
        dist_S' incl size_mset_mono[OF incl] distinct_mset_mono[OF incl]
        simple_clss_size_upper_div2[OF bounded _ _ tauto]
      by (auto simp: unat32_max_def S' U' all_atms_def[symmetric] simp: all_atms_st_def)
    have tr_SS': ‹(get_trail_wl_heur S, M) ∈ trail_pol (all_atms_st S')›
      using ‹(S, S') ∈ ?R› unfolding twl_st_heur_conflict_ana_def
      by (auto simp: all_atms_def S')
    let ?NUE_after = ‹NE + NEk + UE + UEk + (NS + US) + N0 + U0›
    let ?NUE_before = ‹(NE + NEk + UE + UEk + (NS + US) + N0 + U0)›

    have All_atms_rew: ‹set_mset (all_atms (fmupd x' (C', b) N) ?NUE_before) =
        set_mset (all_atms N ?NUE_after)› (is ?A)
      ‹trail_pol (all_atms (fmupd x' (C', b) N) ?NUE_before) =
        trail_pol (all_atms N ?NUE_after)› (is ?B)
      ‹bump_heur (all_atms (fmupd x' (C', b) N) ?NUE_before) =
        bump_heur (all_atms N ?NUE_after)› (is ?C)
      ‹option_lookup_clause_rel  (all_atms (fmupd x' (C', b) N) ?NUE_before) =
        option_lookup_clause_rel (all_atms N ?NUE_after)› (is ?D)
      ‹⟨Id⟩map_fun_rel (D⇩0 (all_atms (fmupd x' (C', b) N) ?NUE_before)) =
         ⟨Id⟩map_fun_rel (D⇩0 (all_atms N ?NUE_after))› (is ?E)
      ‹set_mset (ℒ⇩a⇩l⇩l (all_atms (fmupd x' (C', b) N) ?NUE_before)) =
        set_mset (ℒ⇩a⇩l⇩l (all_atms N ?NUE_after))›
      ‹phase_saving ((all_atms (fmupd x' (C', b) N) ?NUE_before)) =
        phase_saving ((all_atms N ?NUE_after))› (is ?F)
      ‹cach_refinement_empty ((all_atms (fmupd x' (C', b) N) ?NUE_before)) =
        cach_refinement_empty ((all_atms N ?NUE_after))› (is ?G) (*cach_refinement_nonull*)
      ‹cach_refinement_nonull ((all_atms (fmupd x' (C', b) N) ?NUE_before)) =
        cach_refinement_nonull ((all_atms N ?NUE_after))› (is ?G2)
      ‹vdom_m ((all_atms (fmupd x' (C', b) N) ?NUE_before)) =
        vdom_m ((all_atms N ?NUE_after))› (is ?H)
      ‹isasat_input_bounded ((all_atms (fmupd x' (C', b) N) ?NUE_before)) =
        isasat_input_bounded ((all_atms N ?NUE_after))› (is ?I)
      ‹isasat_input_nempty ((all_atms (fmupd x' (C', b) N) ?NUE_before)) =
        isasat_input_nempty ((all_atms N ?NUE_after))› (is ?J)
      ‹vdom_m (all_atms N ?NUE_before) W (fmupd x' (C', b) N) =
        insert x' (vdom_m (all_atms N ?NUE_after) W N)› (is ?K)
      ‹heuristic_rel ((all_atms (fmupd x' (C', b) N) ?NUE_before)) =
        heuristic_rel (all_atms N ?NUE_after)› (is ?L)
      ‹empty_occs_list ((all_atms (fmupd x' (C', b) N) ?NUE_before)) =
        empty_occs_list (all_atms N ?NUE_after)› (is ?M)
      if ‹x' ∉# dom_m N› and C: ‹C' = C› for b x' C'
    proof -
      show A: ?A
        using ‹literals_are_in_ℒ⇩i⇩n (all_atms_st S')  (mset C)› that
        by (auto simp: all_atms_def all_lits_def ran_m_mapsto_upd_notin all_lits_of_mm_add_mset
            U' S'  in_ℒ⇩a⇩l⇩l_atm_of_𝒜⇩i⇩n literals_are_in_ℒ⇩i⇩n_def ac_simps all_atms_st_def)
      have  A2: ‹set_mset (ℒ⇩a⇩l⇩l (all_atms (fmupd x' (C, b) N) ?NUE_before)) =
        set_mset (ℒ⇩a⇩l⇩l (all_atms N ?NUE_after))›
        using A unfolding ℒ⇩a⇩l⇩l_def C by (auto simp: A ac_simps)
      then show ‹set_mset (ℒ⇩a⇩l⇩l (all_atms (fmupd x' (C', b) N) ?NUE_before)) =
        set_mset (ℒ⇩a⇩l⇩l (all_atms N ?NUE_after))›
        using A unfolding ℒ⇩a⇩l⇩l_def C by (auto simp: A)
      have A3: ‹set_mset (all_atms (fmupd x' (C, b) N) ?NUE_before) =
        set_mset (all_atms N ?NUE_after)›
        using A unfolding ℒ⇩a⇩l⇩l_def C by (auto simp: A)

      show ?B and ?C and ?D and ?E and ?F and ?G and ?G2 and ?H and ?I and ?J and ?L and ?M
        unfolding trail_pol_def A A2 ann_lits_split_reasons_def isasat_input_bounded_def
          vmtf_def distinct_atoms_rel_def vmtf_ℒ⇩a⇩l⇩l_def atms_of_def
          distinct_hash_atoms_rel_def
          atoms_hash_rel_def A A2 A3 C option_lookup_clause_rel_def
          lookup_clause_rel_def phase_saving_def cach_refinement_empty_def
          cach_refinement_def heuristic_rel_def
          cach_refinement_list_def vdom_m_def
          isasat_input_bounded_def
          isasat_input_nempty_def cach_refinement_nonull_def
          heuristic_rel_def phase_save_heur_rel_def heuristic_rel_stats_def empty_occs_list_def
          isa_vmtf_cong'[OF A, unfolded C]
        unfolding trail_pol_def[symmetric] ann_lits_split_reasons_def[symmetric]
          isasat_input_bounded_def[symmetric]
          vmtf_def[symmetric]
          distinct_atoms_rel_def[symmetric]
          vmtf_ℒ⇩a⇩l⇩l_def[symmetric] atms_of_def[symmetric]
          distinct_hash_atoms_rel_def[symmetric]
          atoms_hash_rel_def[symmetric]
          option_lookup_clause_rel_def[symmetric]
          lookup_clause_rel_def[symmetric]
          phase_saving_def[symmetric] cach_refinement_empty_def[symmetric]
          cach_refinement_def[symmetric] cach_refinement_nonull_def[symmetric]
          cach_refinement_list_def[symmetric]
          vdom_m_def[symmetric]
          isasat_input_bounded_def[symmetric]
          isasat_input_nempty_def[symmetric]
          heuristic_rel_def[symmetric] empty_occs_list_def[symmetric]
          heuristic_rel_def[symmetric] phase_save_heur_rel_def[symmetric] heuristic_rel_stats_def[symmetric]
        apply auto
        done
      show ?K
        using that
        by (auto simp: vdom_m_simps5 vdom_m_def ac_simps)
    qed

    have [refine0]: ‹mop_save_phase_heur (atm_of (C ! 1)) (is_neg (C ! 1)) ?heur
    ≤ SPEC
       (λc. (c, ())
            ∈ {(c, _). heuristic_rel (all_atms_st U') c})›
      using heur uM_ℒ⇩a⇩l⇩l lits_confl le_C
        literals_are_in_ℒ⇩i⇩n_in_mset_ℒ⇩a⇩l⇩l[of ‹all_atms_st S'› ‹mset C› ‹C!1›]
      unfolding mop_save_phase_heur_def
      by (auto intro!: ASSERT_leI save_phase_heur_preI simp: U' S' all_atms_st_def)
    have stuff: ‹?NUE_before = ?NUE_after›
      by auto
    have arena_le: ‹length ?arena + header_size C + length C ≤ MAX_HEADER_SIZE+1 + r + unat32_max div 2›
      using r r' le_C_ge by (auto simp: unat32_max_def header_size_def S')
    have avdom: ‹mset (get_avdom_aivdom ?aivdom) ⊆# mset (get_vdom_aivdom ?aivdom)› and
      ivdom: ‹mset (get_ivdom_aivdom ?aivdom) ⊆# mset (get_vdom_aivdom ?aivdom)›
      using aivdom unfolding aivdom_inv_dec_alt_def by auto
    have vm: ‹vm ∈ bump_heur (all_atms N (NE + UE)) M1 ⟹
       vm ∈ bump_heur (all_atms N (NE + UE)) (Propagated (- lit_of (hd M)) x2a # M1)› for x2a vm
      by (cases vm)
        (auto intro!: isa_vmtf_consD simp:)
    then show ?thesis
      supply [[goals_limit=1]]
      using empty_cach n_d_M1 C_L' W'W outl vmtf undef ‹1 < length C› lits
        uM_ℒ⇩a⇩l⇩l vdom lcount vdom_m dist_vdom heur
      apply (subst propagate_bt_wl_D_alt_def)
      unfolding U' H get_fresh_index_wl_def prod.case
        propagate_bt_wl_D_heur_alt_def rescore_clause_def
      apply (rewrite in ‹let _ = _!1 in _› Let_def)
      apply (rewrite in ‹let _ = update_lbd_and_mark_used _ _ _ in _› Let_def)
      apply (rewrite in ‹let _ = list_update _ (nat_of_lit _) _ in _› Let_def)
      apply (rewrite in ‹let _ = list_update _ (nat_of_lit _) _ in _› Let_def)
      apply (rewrite in ‹let _ = False in _› Let_def)
      apply (rewrite at  ‹let _ =  get_trail_wl_heur _ in _ ›Let_def)
      apply (rewrite at  ‹let _ =  get_clauses_wl_heur _ in _ ›Let_def)
      apply (rewrite at  ‹let _ =  get_vmtf_heur _ in _ ›Let_def)
      apply (rewrite at  ‹let _ =  get_lbd _ in _ ›Let_def)
      apply (rewrite at  ‹let _ =  get_aivdom _ in _ ›Let_def)
      apply (rewrite at  ‹let _ =  get_watched_wl_heur _ in _ ›Let_def)
      apply (rewrite at  ‹let _ = get_learned_count _ in _ › Let_def)
      apply (rewrite at  ‹let _ = get_heur _ in _ › Let_def)
      apply (rewrite at  ‹let _ = get_stats_heur _ in _ › Let_def)
      apply (rewrite at  ‹let _ = set_learned_count_wl_heur _ _ in _ › Let_def)
      apply (rewrite at  ‹let _ = set_aivdom_wl_heur _ _ in _ › Let_def)
      apply (rewrite at  ‹let _ = set_heur_wl_heur _ _ in _ › Let_def)
      apply (rewrite at  ‹let _ = set_stats_wl_heur _ _ in _ › Let_def)
      apply (rewrite at  ‹let _ = set_literals_to_update_wl_heur _ _ in _ › Let_def)
      apply (rewrite at  ‹let _ = set_count_max_wl_heur _ _ in _ › Let_def)
      apply (rewrite at  ‹let _ = set_vmtf_wl_heur _ _ in _ › Let_def)
      apply (rewrite at  ‹let _ = set_lbd_wl_heur _ _ in _ › Let_def)
      apply (rewrite at  ‹let _ = set_clauses_wl_heur _ _ in _ › Let_def)
      apply (rewrite at  ‹let _ = set_trail_wl_heur _ _ in _ › Let_def)
      apply (rewrite at  ‹let _ = set_watched_wl_heur _ _ in _ › Let_def)
      apply (refine_rcg cons_trail_Propagated_tr2[of _ _ _ _ _ _ ‹all_atms_st U'›]
         )
      subgoal using valid by (auto dest!: valid_arena_vdom_subset)
      subgoal  using valid size_mset_mono[OF avdom] by (auto dest!: valid_arena_vdom_subset)
      subgoal using ‹nat_of_lit (C ! Suc 0) < length ?W'› by simp
      subgoal using ‹nat_of_lit (- lit_of (hd (get_trail_wl S'))) < length ?W'›
        by (simp add: S' lit_of_hd_trail_def)
      subgoal using le_C_ge .
      subgoal by (auto simp: append_and_length_fast_code_pre_def isasat_fast_def
        snat64_max_def unat32_max_def)
      subgoal
        using D' C_1_neq_hd vmtf avdom M1'_M1 size_learned_clss_dom_m[of N] valid_arena_size_dom_m_le_arena[OF valid]
        by (auto simp: propagate_bt_wl_D_heur_def twl_st_heur_def lit_of_hd_trail_st_heur_def
          phase_saving_def atms_of_def S' U' lit_of_hd_trail_def all_atms_def[symmetric] isasat_fast_def
          snat64_max_def unat32_max_def)

      subgoal for x uu x1 x2 vm uua_ glue uub D'' xa x'
        by (auto simp: update_lbd_pre_def arena_is_valid_clause_idx_def)
      subgoal using length_watched_le[of S' S ‹-lit_of_hd_trail M›] corr SS' uM_ℒ⇩a⇩l⇩l W'_eq S_arena
         by (auto simp: isasat_fast_def length_ll_def S' lit_of_hd_trail_def simp flip: all_atms_def)
      subgoal using length_watched_le[of S' S ‹C ! Suc 0›] corr SS' W'_eq S_arena C_1_neq_hd C_Suc1_in
         by (auto simp: length_ll_def S' lit_of_hd_trail_def isasat_fast_def simp flip: all_atms_def)
      subgoal using D' C_1_neq_hd vmtf avdom
        by (auto simp: DECISION_REASON_def
            dest: valid_arena_one_notin_vdomD
            intro!: vm)
      subgoal
        using M1'_M1
        by (rule cons_trail_Propagated_tr_pre)
          (use undef uM_ℒ⇩a⇩l⇩l in ‹auto simp: lit_of_hd_trail_def S' U' all_atms_def[symmetric]
            all_atms_st_def›)
      subgoal using M1'_M1 by (auto simp: lit_of_hd_trail_def S' U' all_atms_def[symmetric])
      subgoal using uM_ℒ⇩a⇩l⇩l by (auto simp: S' U' uminus_𝒜⇩i⇩n_iff lit_of_hd_trail_def all_atms_st_def)
      subgoal
        using D' C_1_neq_hd vmtf avdom
        by (auto simp: propagate_bt_wl_D_heur_def twl_st_heur_def lit_of_hd_trail_st_heur_def
            intro!: ASSERT_refine_left ASSERT_leI RES_refine exI[of _ C] valid_arena_update_lbd_and_mark_used
            dest: valid_arena_one_notin_vdomD
            intro!: vm)
      apply assumption
      apply (rule log_new_clause_heur_log_clause)
      subgoal final_rel
        supply All_atms_rew[simp]
        unfolding twl_st_heur_def
        using D' C_1_neq_hd vmtf avdom aivdom M1'_M1 bounded nempty r r' arena_le
          set_mset_mono[OF ivdom] occs
        by (clarsimp_all simp add: propagate_bt_wl_D_heur_def twl_st_heur_def
            Let_def T' U' rescore_clause_def S' map_fun_rel_def
            list_of_mset2_def vmtf_flush_def RES_RES2_RETURN_RES RES_RETURN_RES uminus_𝒜⇩i⇩n_iff
            get_fresh_index_def RES_RETURN_RES2 RES_RES_RETURN_RES2 lit_of_hd_trail_def
            RES_RES_RETURN_RES lbd_empty_def get_LBD_def DECISION_REASON_def
            all_atms_def[symmetric] All_atms_rew learned_clss_count_def all_atms_st_def
            aivdom_inv_dec_intro_add_mset valid_arena_update_lbd_and_mark_used old clss_size_corr_intro(2)
            intro!: valid_arena_update_lbd_and_mark_used aivdom_inv_intro_add_mset
            simp del: isasat_input_bounded_def isasat_input_nempty_def
          dest: valid_arena_one_notin_vdomD
            get_learned_count_learned_clss_countD)
          (auto
          intro!: valid_arena_update_lbd_and_mark_used aivdom_inv_intro_add_mset
          simp: vdom_m_simps5
            simp del: isasat_input_bounded_def isasat_input_nempty_def
           dest: valid_arena_one_notin_vdomD)
      subgoal by auto
      subgoal by auto
      apply (rule maybe_mark_added_clause_heur2_id[unfolded conc_fun_RETURN])
      subgoal
        apply (drule final_rel)
        apply assumption+
        done
      subgoal by auto
      subgoal
        supply All_atms_rew[simp]
        unfolding twl_st_heur_def
        using D' C_1_neq_hd vmtf avdom aivdom M1'_M1 bounded nempty r r' arena_le
          set_mset_mono[OF ivdom]
        by (clarsimp_all simp add: propagate_bt_wl_D_heur_def twl_st_heur_def
            Let_def T' U' rescore_clause_def S' map_fun_rel_def
            list_of_mset2_def vmtf_flush_def RES_RES2_RETURN_RES RES_RETURN_RES uminus_𝒜⇩i⇩n_iff
            get_fresh_index_def RES_RETURN_RES2 RES_RES_RETURN_RES2 lit_of_hd_trail_def
            RES_RES_RETURN_RES lbd_empty_def get_LBD_def DECISION_REASON_def
            all_atms_def[symmetric] All_atms_rew learned_clss_count_def all_atms_st_def
            aivdom_inv_dec_intro_add_mset valid_arena_update_lbd_and_mark_used old clss_size_corr_intro(2)
            intro!: valid_arena_update_lbd_and_mark_used aivdom_inv_intro_add_mset
            simp del: isasat_input_bounded_def isasat_input_nempty_def
          dest: valid_arena_one_notin_vdomD
            get_learned_count_learned_clss_countD)
      done
  qed


  have propagate_unit_bt_wl_D_int: ‹propagate_unit_bt_wl_D_int LK U
      ≤ ⇓ ?S
          (propagate_unit_bt_wl LK' U')›
    if
      SS': ‹(S, S') ∈ ?R› and
      ‹backtrack_wl_inv S'› and
      ‹backtrack_wl_D_heur_inv S› and
      ‹(TnC, T') ∈ ?shorter S' S› and
      [simp]: ‹nC = (n, C)› and
      [simp]: ‹TnC = (T, nC)› and
      find_decomp: ‹(U, U') ∈ ?find_decomp S T' n› and
      ‹¬ 1 < length C› and
      ‹¬ 1 < size (the (get_conflict_wl U'))› and
      KK': ‹(LK, LK') ∈ {(L, L'). L = L' ∧ L = lit_of (hd (get_trail_wl S'))}›
    for S S' TnC T' T nC n C U U' LK LK'
  proof -
    have
      TT': ‹(T, del_conflict_wl T') ∈ twl_st_heur_bt› and
      n: ‹n = get_maximum_level (get_trail_wl T')
          (remove1_mset (- lit_of (hd (get_trail_wl T'))) (mset C))› and
      T_C: ‹get_conflict_wl T' = Some (mset C)› and
      T'S': ‹equality_except_conflict_wl T' S'› and
      ‹C ≠ []› and
      hd_C: ‹hd C = - lit_of (hd (get_trail_wl T'))› and
      incl: ‹mset C ⊆# the (get_conflict_wl S')› and
      dist_S': ‹distinct_mset (the (get_conflict_wl S'))› and
      list_confl_S': ‹literals_are_in_ℒ⇩i⇩n (all_atms_st S') (the (get_conflict_wl S'))› and
      ‹get_conflict_wl S' ≠ None› and
      ‹C ≠ []› and
      uL_M: ‹- lit_of (hd (get_trail_wl S')) ∈# ℒ⇩a⇩l⇩l (all_atms_st S')› and
      tr_nempty: ‹get_trail_wl T' ≠ []›
      using ‹(TnC, T') ∈ ?shorter S' S›  ‹~1 < length C›
      by (auto)
    obtain K M2 where
      UU': ‹(U, U') ∈ twl_st_heur_bt› and
      U'U': ‹equality_except_trail_wl U' T'› and
      lev_K: ‹get_level (get_trail_wl T') K = Suc (get_maximum_level (get_trail_wl T')
           (remove1_mset (- lit_of (hd (get_trail_wl T')))
             (the (get_conflict_wl T'))))› and
      decomp: ‹(Decided K # get_trail_wl U', M2) ∈ set (get_all_ann_decomposition (get_trail_wl T'))› and
      r: ‹length (get_clauses_wl_heur S) = r›
      using find_decomp SS'
      by (auto)

    obtain M N NE UE NEk UEk NS US N0 U0 Q W where
      T': ‹T' = (M, N, Some (mset C), NE, UE, NEk, UEk, NS, US, N0, U0, Q, W)›
      using TT' T_C ‹¬1 < length C›
      apply (cases T'; cases S')
      by (auto simp: find_lit_of_max_level_wl_def)
    obtain D' where
      S': ‹S' = (M, N, D', NE, UE, NEk, UEk, NS, US, N0, U0, Q, W)›
      using T'S'
      apply (cases S')
      by (auto simp: find_lit_of_max_level_wl_def T' del_conflict_wl_def)

    obtain M1 where
      U': ‹U' = (M1, N, Some (mset C), NE, UE, NEk, UEk, NS, US, N0, U0, Q, W)›
      using ‹(TnC, T') ∈ ?shorter S' S› find_decomp
      apply (cases U')
      by (auto simp: find_lit_of_max_level_wl_def T')
    have [simp]:
       ‹LK' = lit_of (hd (get_trail_wl T'))›
       ‹LK = LK'›
       using KK' SS' S' by (auto simp: T')
    let ?M1' = ‹get_trail_wl_heur U›
    let ?arena = ‹get_clauses_wl_heur U›
    let ?D' = ‹get_conflict_wl_heur U›
    let ?W' = ‹get_watched_wl_heur U›
    let ?vm' = ‹get_vmtf_heur U›
    let ?clvls = ‹get_count_max_lvls_heur U›
    let ?cach = ‹get_conflict_cach U›
    let ?outl = ‹get_outlearned_heur U›
    let ?lcount = ‹get_learned_count U›
    let ?heur = ‹get_heur U›
    let ?lbd = ‹get_lbd U›
    let ?aivdom = ‹get_aivdom U›
    have
        r': ‹length (get_clauses_wl_heur U) = r›
            ‹get_learned_count U = get_learned_count S›
            ‹learned_clss_count U ≤ u› and
      old: ‹get_old_arena U = []›
      using SS' UU' find_decomp r ‹(TnC, T') ∈ ?shorter S' S›
        get_learned_count_learned_clss_countD2[of U S]
      by (auto simp: U' T' twl_st_heur_bt_def)
    let ?vdom = ‹set (get_vdom_aivdom ?aivdom)›
    have
      M'M: ‹(?M1', M1) ∈ trail_pol (all_atms_st U')› and
      W'W: ‹(?W', W) ∈ ⟨Id⟩map_fun_rel (D⇩0  (all_atms_st U'))› and
      vmtf: ‹?vm' ∈ bump_heur  (all_atms_st U') M1› and
      n_d_M1: ‹no_dup M1› and
      empty_cach: ‹cach_refinement_empty  (all_atms_st U') ?cach› and
      ‹length ?outl = Suc 0› and
      outl: ‹out_learned M1 None ?outl› and
      lcount: ‹clss_size_corr N NE UE NEk UEk NS US N0 U0 ?lcount› and
      vdom: ‹vdom_m (all_atms_st U') W N ⊆ ?vdom› and
      valid: ‹valid_arena ?arena N ?vdom› and
      D': ‹(?D', None) ∈ option_lookup_clause_rel (all_atms_st U')› and
      bounded: ‹isasat_input_bounded (all_atms_st U')› and
      nempty: ‹isasat_input_nempty (all_atms_st U')› and
      dist_vdom: ‹distinct (get_vdom_aivdom ?aivdom)› and
      aivdom: ‹aivdom_inv_dec ?aivdom (dom_m N)› and
      heur: ‹heuristic_rel (all_atms_st U') ?heur› and
      occs: ‹(get_occs U, empty_occs_list (all_atms_st U')) ∈ occurrence_list_ref›
      using UU' by (auto simp: out_learned_def twl_st_heur_bt_def U' all_atms_def[symmetric]
        aivdom_inv_dec_alt_def)
    have [simp]: ‹C ! 0 = - lit_of (hd M)› and
      n_d: ‹no_dup M›
      using SS' hd_C ‹C ≠ []› by (auto simp: S' U' T' twl_st_heur_conflict_ana_def hd_conv_nth)
    have undef: ‹undefined_lit M1 (lit_of (hd M))›
      using decomp n_d
      by (auto dest!: get_all_ann_decomposition_exists_prepend simp: T' hd_append U' neq_Nil_conv
          split: if_splits)
    have C: ‹C = [- lit_of (hd M)]›
      using ‹C ≠ []› ‹C ! 0 = - lit_of (hd M)› ‹¬1 < length C›
      by (cases C) (auto simp del: ‹C ! 0 = - lit_of (hd M)›)
    have propagate_unit_bt_wl_alt_def:
      ‹propagate_unit_bt_wl = (λL (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W). do {
        ASSERT(L ∈# all_lits_st (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W));
        ASSERT(propagate_unit_bt_wl_pre L (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W));
	_ ← RETURN ();
	_ ← RETURN ();
	_ ← RETURN ();
	_ ← RETURN ();
	M ← cons_trail_propagate_l (-L) 0 M;
        RETURN (M, N, None, NE, UE, NEk, add_mset (the D) UEk, NS, US, N0, U0, {#L#}, W)
      })›
      unfolding propagate_unit_bt_wl_def Let_def by (auto intro!: ext bind_cong[OF refl]
       simp: propagate_unit_bt_wl_pre_def propagate_unit_bt_l_pre_def
         single_of_mset_def RES_RETURN_RES image_iff)

    have [refine0]:
      ‹lbd_empty ?lbd ≤ SPEC (λc. (c, ()) ∈ {(c, _). c = replicate (length ?lbd) False})›
      by (auto simp: lbd_empty_def)
    have [refine0]: ‹mop_isa_length_trail ?M1' ≤  ⇓ {(j, _). j = length M1} (RETURN ())›
      by (rule order_trans, rule mop_isa_length_trail_length_u[THEN fref_to_Down_Id_keep, OF _ M'M])
        (auto simp: RETURN_def conc_fun_RES)

    have [refine0]: ‹isa_bump_heur_flush ?M1' ?vm' ≤
         SPEC(λc. (c, ()) ∈ {(vm', _). vm' ∈ bump_heur (all_atms_st U') M1})›
      for vm i L
    proof -
      show ?thesis
        apply (rule isa_bump_heur_flush_isa_bump_flush[THEN fref_to_Down_curry, of ‹all_atms_st U'› M1 ?vm', THEN order_trans])
        subgoal by (use M'M bounded nempty vmtf in auto)
        subgoal by (use M'M bounded nempty in auto)
        subgoal using M'M by (auto simp: isa_bump_flush_def)
        done
    qed
    have [refine0]: ‹get_LBD ?lbd ≤ SPEC(λc. (c, ()) ∈ UNIV)›
      by (auto simp: get_LBD_def)

    have tr_S: ‹(get_trail_wl_heur S, M) ∈ trail_pol (all_atms_st S')›
      using SS' by (auto simp: S' twl_st_heur_conflict_ana_def all_atms_def)

    have hd_SM: ‹lit_of_last_trail_pol (get_trail_wl_heur S) = lit_of (hd M)›
      unfolding lit_of_hd_trail_def lit_of_hd_trail_st_heur_def
      by (subst lit_of_last_trail_pol_lit_of_last_trail[THEN fref_to_Down_unRET_Id])
        (use M'M tr_S tr_nempty in ‹auto simp: lit_of_hd_trail_def T' S'›)
    have uL_M: ‹- lit_of (hd (get_trail_wl S')) ∈# ℒ⇩a⇩l⇩l (all_atms_st U')›
      using uL_M by (simp add: S' U' all_atms_st_def)
    let ?NE = ‹add_mset {#- lit_of (hd M)#} (NE + NEk + UE + UEk + (NS + US) + N0 + U0)›
    let ?NE_after = ‹(NE + NEk + UE + UEk + (NS + US) + N0 + U0)›
    have All_atms_rew: ‹set_mset (all_atms (N) (?NE)) =
        set_mset (all_atms N ?NE_after)› (is ?A)
      ‹trail_pol (all_atms (N) (?NE)) =
        trail_pol (all_atms N ?NE_after)› (is ?B)
      ‹bump_heur (all_atms (N) (?NE)) =
        bump_heur (all_atms N ?NE_after)› (is ?C)
      ‹option_lookup_clause_rel  (all_atms (N) (?NE)) =
        option_lookup_clause_rel (all_atms N ?NE_after)› (is ?D)
      ‹⟨Id⟩map_fun_rel (D⇩0 (all_atms (N) (?NE))) =
         ⟨Id⟩map_fun_rel (D⇩0 (all_atms N ?NE_after))› (is ?E)
      ‹set_mset (ℒ⇩a⇩l⇩l (all_atms (N) (?NE))) =
        set_mset (ℒ⇩a⇩l⇩l (all_atms N ?NE_after))›
      ‹phase_saving ((all_atms (N) (?NE))) =
        phase_saving ((all_atms N ?NE_after))› (is ?F)
      ‹cach_refinement_empty ((all_atms (N) (?NE))) =
        cach_refinement_empty ((all_atms N ?NE_after))› (is ?G)
      ‹vdom_m ((all_atms (N) (?NE))) =
        vdom_m ((all_atms N ?NE_after))› (is ?H)
      ‹isasat_input_bounded ((all_atms (N) (?NE))) =
        isasat_input_bounded ((all_atms N ?NE_after))› (is ?I)
      ‹isasat_input_nempty ((all_atms (N) (?NE))) =
        isasat_input_nempty ((all_atms N ?NE_after))› (is ?J)
      ‹vdom_m (all_atms N ?NE) W (N) =
        (vdom_m (all_atms N ?NE_after) W N)› (is ?K)
      ‹heuristic_rel ((all_atms (N) (?NE))) =
      heuristic_rel ((all_atms N ?NE_after))› (is ?L)
      ‹empty_occs_list  ((all_atms (N) (?NE))) =
         empty_occs_list ((all_atms N ?NE_after))› (is ?M)
      for b x' C'
    proof -
      show A: ?A
        using  uL_M
        apply (cases ‹hd M›)
        by (auto simp: all_atms_def all_lits_def ran_m_mapsto_upd_notin all_lits_of_mm_add_mset
            U' S'  in_ℒ⇩a⇩l⇩l_atm_of_𝒜⇩i⇩n literals_are_in_ℒ⇩i⇩n_def atm_of_eq_atm_of
            all_lits_of_m_add_mset ac_simps lits_of_def all_atms_st_def)
      have  A2: ‹set_mset (ℒ⇩a⇩l⇩l (all_atms N (?NE))) =
        set_mset (ℒ⇩a⇩l⇩l (all_atms N ?NE_after))›
        using A unfolding ℒ⇩a⇩l⇩l_def C by (auto simp: A)
      then show ‹set_mset (ℒ⇩a⇩l⇩l (all_atms (N) (?NE))) =
        set_mset (ℒ⇩a⇩l⇩l (all_atms N ?NE_after))›
        using A unfolding ℒ⇩a⇩l⇩l_def C by (auto simp: A)
      have A3: ‹set_mset (all_atms N (?NE)) =
        set_mset (all_atms N ?NE_after)›
        using A unfolding ℒ⇩a⇩l⇩l_def C by (auto simp: A)

      show ?B and ?C and ?D and ?E and ?F and ?G and ?H and ?I and ?J and ?K and ?L and ?M
        unfolding trail_pol_def A A2 ann_lits_split_reasons_def isasat_input_bounded_def
          vmtf_def distinct_atoms_rel_def vmtf_ℒ⇩a⇩l⇩l_def atms_of_def
          distinct_hash_atoms_rel_def heuristic_rel_stats_def
          atoms_hash_rel_def A A2 A3 C option_lookup_clause_rel_def
          lookup_clause_rel_def phase_saving_def cach_refinement_empty_def
          cach_refinement_def
          cach_refinement_list_def vdom_m_def
          isasat_input_bounded_def heuristic_rel_def
          isasat_input_nempty_def cach_refinement_nonull_def vdom_m_def
          phase_save_heur_rel_def phase_saving_def empty_occs_list_def
          isa_vmtf_cong'[OF A, unfolded C]
        unfolding trail_pol_def[symmetric] ann_lits_split_reasons_def[symmetric]
          isasat_input_bounded_def[symmetric]
          vmtf_def[symmetric]
          distinct_atoms_rel_def[symmetric]
          vmtf_ℒ⇩a⇩l⇩l_def[symmetric] atms_of_def[symmetric]
          distinct_hash_atoms_rel_def[symmetric]
          atoms_hash_rel_def[symmetric]
          option_lookup_clause_rel_def[symmetric]
          lookup_clause_rel_def[symmetric]
          phase_saving_def[symmetric] cach_refinement_empty_def[symmetric]
          cach_refinement_def[symmetric]
          cach_refinement_list_def[symmetric]
          vdom_m_def[symmetric]
          isasat_input_bounded_def[symmetric] cach_refinement_nonull_def[symmetric]
          isasat_input_nempty_def[symmetric] heuristic_rel_def[symmetric] heuristic_rel_stats_def[symmetric]
          phase_save_heur_rel_def[symmetric] phase_saving_def[symmetric] empty_occs_list_def[symmetric]
          bump_heur_def[symmetric]
        apply auto
        done
    qed
    have stuff: ‹(NE+NEk) + (UE+UEk) + (NS + US) + N0 + U0 = ?NE_after›
      by auto
    have [simp]: ‹clss_size_corr N NE (add_mset C UE) NEk UEk NS US N0 U0
      (clss_size_incr_lcountUE (get_learned_count S))› for C
      using lcount UU' r' unfolding U'
      by (cases S)
       (simp add: twl_st_heur_bt_def clss_size_corr_intro)

    show ?thesis
      using empty_cach n_d_M1 W'W outl vmtf C undef uL_M vdom lcount valid D' aivdom
      unfolding U' propagate_unit_bt_wl_D_int_def prod.simps hd_SM
        propagate_unit_bt_wl_alt_def
      apply (rewrite at ‹let _ = incr_units_since_last_GC (incr_uset _) in _› Let_def)
      apply (rewrite at  ‹let _ =  get_trail_wl_heur _ in _ ›Let_def)
      apply (rewrite at  ‹let _ =  get_clauses_wl_heur _ in _ ›Let_def)
      apply (rewrite at  ‹let _ =  get_vmtf_heur _ in _ ›Let_def)
      apply (rewrite at  ‹let _ =  get_lbd _ in _ ›Let_def)
      apply (rewrite at  ‹let _ =  get_aivdom _ in _ ›Let_def)
      apply (rewrite at  ‹let _ =  get_watched_wl_heur _ in _ ›Let_def)
      apply (rewrite at  ‹let _ = get_learned_count _ in _ › Let_def)
      apply (rewrite at  ‹let _ = get_heur _ in _ › Let_def)
      apply (rewrite at  ‹let _ = get_stats_heur _ in _ › Let_def)
      apply (refine_rcg cons_trail_Propagated_tr2[where 𝒜 = ‹all_atms_st U'›])
      subgoal by (auto simp: DECISION_REASON_def)
      subgoal
        using M'M by (rule cons_trail_Propagated_tr_pre)
           (use undef uL_M in ‹auto simp: hd_SM all_atms_def[symmetric] T'
	    lit_of_hd_trail_def S'›)
     subgoal
       using M'M by (auto simp: U' lit_of_hd_trail_st_heur_def RETURN_def
           single_of_mset_def vmtf_flush_def twl_st_heur_def lbd_empty_def get_LBD_def
           RES_RES2_RETURN_RES RES_RETURN_RES S' uminus_𝒜⇩i⇩n_iff RES_RES_RETURN_RES
           DECISION_REASON_def hd_SM lit_of_hd_trail_st_heur_def
           intro!: ASSERT_refine_left RES_refine exI[of _ ‹-lit_of (hd M)›]
           intro!: vmtf_consD
           simp del: isasat_input_bounded_def isasat_input_nempty_def)
     subgoal
       by (auto simp: U' lit_of_hd_trail_st_heur_def RETURN_def
           single_of_mset_def vmtf_flush_def twl_st_heur_def lbd_empty_def get_LBD_def
           RES_RES2_RETURN_RES RES_RETURN_RES S' uminus_𝒜⇩i⇩n_iff RES_RES_RETURN_RES
           DECISION_REASON_def hd_SM T'
           intro!: ASSERT_refine_left RES_refine exI[of _ ‹-lit_of (hd M)›]
           intro!: vmtf_consD
           simp del: isasat_input_bounded_def isasat_input_nempty_def)
     subgoal
       using bounded nempty dist_vdom r' heur aivdom occs
       by (auto simp: U' lit_of_hd_trail_st_heur_def RETURN_def
           single_of_mset_def vmtf_flush_def twl_st_heur_def lbd_empty_def get_LBD_def
         RES_RES2_RETURN_RES RES_RETURN_RES S' uminus_𝒜⇩i⇩n_iff RES_RES_RETURN_RES
         learned_clss_count_def all_atms_st_def old
           DECISION_REASON_def hd_SM All_atms_rew all_atms_def[symmetric]
           intro!: ASSERT_refine_left RES_refine exI[of _ ‹-lit_of (hd M)›]
           intro!: isa_vmtf_consD
         simp del: isasat_input_bounded_def isasat_input_nempty_def)
       done
  qed

  have trail_nempty: ‹fst (get_trail_wl_heur S) ≠ []›
    if
      ‹(S, S') ∈ ?R› and
      ‹backtrack_wl_inv S'›
    for S S'
  proof -
    show ?thesis
      using that unfolding backtrack_wl_inv_def backtrack_wl_D_heur_inv_def backtrack_l_inv_def backtrack_inv_def
        backtrack_l_inv_def apply -
      by normalize_goal+
        (auto simp:  twl_st_heur_conflict_ana_def trail_pol_def ann_lits_split_reasons_def)
  qed

  have H:
    ‹(x, y) ∈ twl_st_heur_conflict_ana ⟹ fst (get_trail_wl_heur x) ≠ [] ⟷ get_trail_wl y ≠ []› for x y
    by (auto simp: twl_st_heur_conflict_ana_def trail_pol_def ann_lits_split_reasons_def)
  have [refine]: ‹⋀x y. (x, y)
          ∈ {(S, T).
             (S, T) ∈ twl_st_heur_conflict_ana ∧
             length (get_clauses_wl_heur S) = r} ⟹
          lit_of_hd_trail_st_heur x
          ≤ ⇓ {(L, L'). L = L' ∧ L = lit_of (hd (get_trail_wl y))} (mop_lit_hd_trail_wl y)›
    unfolding mop_lit_hd_trail_wl_def lit_of_hd_trail_st_heur_def
    apply refine_rcg
    subgoal for x y
      unfolding mop_lit_hd_trail_wl_pre_def mop_lit_hd_trail_l_pre_def mop_lit_hd_trail_pre_def in_pair_collect_simp
      by normalize_goal+
        (simp add: H)
    subgoal for  x y
      unfolding mop_lit_hd_trail_wl_pre_def mop_lit_hd_trail_l_pre_def mop_lit_hd_trail_pre_def in_pair_collect_simp
      apply normalize_goal+
      apply (subst lit_of_last_trail_pol_lit_of_last_trail[THEN fref_to_Down_unRET_Id, of ‹get_trail_wl y› ‹get_trail_wl_heur x› ‹all_atms_st y›])
      apply (simp_all add: H)
      apply (auto simp:  twl_st_heur_conflict_ana_def mop_lit_hd_trail_wl_pre_def mop_lit_hd_trail_l_pre_def
           mop_lit_hd_trail_pre_def state_wl_l_def twl_st_l_def lit_of_hd_trail_def RETURN_RES_refine_iff)
      done
    done
  have backtrack_wl_alt_def:
    ‹backtrack_wl S =
      do {
        ASSERT(backtrack_wl_inv S);
        L ← mop_lit_hd_trail_wl S;
        S ← extract_shorter_conflict_wl S;
        S ← find_decomp_wl L S;

        if size (the (get_conflict_wl S)) > 1
        then do {
          L' ← find_lit_of_max_level_wl S L;
          S ← propagate_bt_wl L L' S;
          RETURN S
        }
        else do {
          propagate_unit_bt_wl L S
       }
    }› for S
    unfolding backtrack_wl_def while.imonad2
    by auto

  have save_phase_st: ‹(xb, x') ∈ ?S ⟹
       save_phase_st xb
       ≤ SPEC
          (λc. (c, x')
               ∈ {(S, T).
                  (S, T) ∈ twl_st_heur ∧
                  length (get_clauses_wl_heur S)
                  ≤ MAX_HEADER_SIZE+1 + r + unat32_max div 2 ∧
                  learned_clss_count S ≤ Suc u})› for xb x'
    unfolding save_phase_st_def
    by (refine_vcg save_phase_heur_spec[THEN order_trans, of ‹all_atms_st x'›])
      (auto simp: twl_st_heur_def learned_clss_count_def)
  show ?thesis
    supply [[goals_limit=1]]
    apply (intro frefI nres_relI)
    unfolding backtrack_wl_D_nlit_heur_alt_def backtrack_wl_alt_def
    apply (refine_rcg shorter)
    subgoal by (rule inv)
    subgoal by (rule trail_nempty)
    subgoal by auto
    subgoal for x y xa S x1 x2 x1a x2a
      by (auto simp: twl_st_heur_state_simp equality_except_conflict_wl_get_clauses_wl)
    subgoal for x y xa S x1 x2 x1a x2a
      by (auto simp: twl_st_heur_state_simp equality_except_conflict_wl_get_clauses_wl)
    apply (rule find_decomp_wl_nlit; assumption)
    subgoal by (auto simp: twl_st_heur_state_simp equality_except_conflict_wl_get_clauses_wl
          equality_except_trail_wl_get_clauses_wl)
    subgoal by (auto simp: twl_st_heur_state_simp equality_except_conflict_wl_get_clauses_wl
          equality_except_trail_wl_get_clauses_wl)
    subgoal for x y L La xa S x1 x2 x1a x2a Sa Sb
      by (auto simp: twl_st_heur_state_simp equality_except_trail_wl_get_conflict_wl)
    apply (rule fst_find_lit_of_max_level_wl; solves assumption)
    apply (rule propagate_bt_wl_D_heur; assumption)
    apply (rule save_phase_st; assumption)
    apply (rule propagate_unit_bt_wl_D_int; assumption)
    done
qed


end