Theory IsaSAT_Restart_Reduce

theory IsaSAT_Restart_Reduce
imports IsaSAT_Restart IsaSAT_Restart_Reduce_Defs
begin

definition find_local_restart_target_level where
  ‹find_local_restart_target_level M _ = SPEC(λi. i ≤ count_decided M)›

lemma find_local_restart_target_level_alt_def:
  ‹find_local_restart_target_level M vm = do {
      (b, i) ← SPEC(λ(b::bool, i). i ≤ count_decided M);
       RETURN i
    }›
  unfolding find_local_restart_target_level_def by (auto simp: RES_RETURN_RES2 uncurry_def)


lemma find_local_restart_target_level_int_find_local_restart_target_level:
   ‹(uncurry find_local_restart_target_level_int, uncurry find_local_restart_target_level) ∈
     [λ(M, vm). vm ∈ bump_heur 𝒜 M]f trail_pol 𝒜 ×r Id → ⟨nat_rel⟩nres_rel›
  unfolding find_local_restart_target_level_int_def find_local_restart_target_level_alt_def
    uncurry_def Let_def
  apply (intro frefI nres_relI)
  apply clarify
  subgoal for a aa ab ac ad b ba ae bb
    unfolding access_focused_vmtf_array_def nres_monad3 bind_to_let_conv Let_def
    apply (refine_rcg WHILEIT_rule[where R = ‹measure (λ(brk, i). (If brk 0 1) + length b - i)›]
        assert.ASSERT_leI)
    subgoal by auto
    subgoal
      unfolding find_local_restart_target_level_int_inv_def
      by (auto simp: trail_pol_alt_def control_stack_length_count_dec)
    subgoal by auto
    subgoal by (auto simp: trail_pol_alt_def intro: control_stack_le_length_M)
    subgoal for s x1 x2
      by (subgoal_tac ‹a ! (b ! x2) ∈# ℒall 𝒜›)
        (auto simp: trail_pol_alt_def rev_map lits_of_def rev_nth
            vmtf_def atms_of_def bump_heur_def bump_get_heuristics_def
          intro!: literals_are_in_ℒin_trail_in_lits_of_l)
    subgoal by (auto simp: find_local_restart_target_level_int_inv_def)
    subgoal by (auto simp: trail_pol_alt_def control_stack_length_count_dec
          find_local_restart_target_level_int_inv_def)
    subgoal by auto
    done
  done

lemma find_local_restart_target_level_st_alt_def:
  ‹find_local_restart_target_level_st = (λS. do {
      find_local_restart_target_level_int (get_trail_wl_heur S) (get_vmtf_heur S)})›
 apply (intro ext)
  by (auto simp: find_local_restart_target_level_st_def)

lemma cdcl_twl_local_restart_wl_D_spec_int:
  ‹cdcl_twl_local_restart_wl_spec (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W) ≥ ( do {
      ASSERT(∃last_GC last_Restart. restart_abs_wl_pre (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W) last_GC last_Restart False);
      i ← SPEC(λ_. True);
      if i
      then RETURN (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W)
      else do {
        (M, Q') ← SPEC(λ(M', Q'). (∃K M2. (Decided K # M', M2) ∈ set (get_all_ann_decomposition M) ∧
              Q' = {#}) ∨ (M' = M ∧ Q' = Q));
        RETURN (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q', W)
     }
   })›
proof -
  have If_Res: ‹(if i then (RETURN f) else (RES g)) = (RES (if i then {f} else g))› for i f g
    by auto
  show ?thesis
    unfolding cdcl_twl_local_restart_wl_spec_def prod.case RES_RETURN_RES2 If_Res
    by refine_vcg
      (auto simp: If_Res RES_RETURN_RES2 RES_RES_RETURN_RES uncurry_def
        image_iff split:if_splits)
qed

lemma cdcl_twl_local_restart_wl_D_heur_cdcl_twl_local_restart_wl_D_spec:
  ‹(cdcl_twl_local_restart_wl_D_heur, cdcl_twl_local_restart_wl_spec) ∈
    twl_st_heur''''u r u →f ⟨twl_st_heur''''u r u⟩nres_rel›
proof -
  have K: ‹(do {
    j ← mop_isa_length_trail (get_trail_wl_heur S);
    RES {f j}
    }) = (do {
    ASSERT (isa_length_trail_pre (get_trail_wl_heur S));
    RES {f (isa_length_trail (get_trail_wl_heur S))}})› for S :: isasat and f
    by (cases S) (auto simp: mop_isa_length_trail_def)
  have K2: ‹(case S of
               (a, b) ⇒ RES (Φ a b)) =
        (RES (case S of (a, b) ⇒ Φ a b))› for S
  by (cases S) auto

  have [dest]: ‹av = None› ‹out_learned a av am ⟹ out_learned x1 av am›
    if ‹restart_abs_wl_pre (a, au, av, aw, ax, NEk, UEk, NS, US, N0, U0, ay, bd) last_GC last_Restart False›
    for a au av aw ax ay bd x1 am NEk UEk NS US last_GC last_Restart N0 U0
    using that
    unfolding restart_abs_wl_pre_def restart_abs_l_pre_def
      restart_prog_pre_def
    by (auto simp: twl_st_l_def state_wl_l_def out_learned_def)
  have [refine0]:
    ‹find_local_restart_target_level_int (get_trail_wl_heur S) (get_vmtf_heur S) ≤
      ⇓ {(i, b). b = (i = count_decided (get_trail_wl T)) ∧
          i ≤ count_decided (get_trail_wl T)} (SPEC (λ_. True))›
    if ‹(S, T) ∈ twl_st_heur› for S T
    apply (rule find_local_restart_target_level_int_find_local_restart_target_level[THEN
         fref_to_Down_curry, THEN order_trans, of ‹all_atms_st T› ‹get_trail_wl T› ‹get_vmtf_heur S›])
    subgoal using that unfolding twl_st_heur_def by auto
    subgoal using that unfolding twl_st_heur_def by auto
    subgoal by (auto simp: find_local_restart_target_level_def conc_fun_RES)
    done
  have H:
      ‹set_mset (all_atms_st S) =
           set_mset (all_init_atms_st S)› (is ?A)
      ‹set_mset (all_atms_st S) =
           set_mset (all_atms (get_clauses_wl S) (get_unit_clauses_wl S + get_subsumed_init_clauses_wl S + get_init_clauses0_wl S))›
           (is ?B)
      ‹get_conflict_wl S = None› (is ?C)
     if pre: ‹restart_abs_wl_pre S last_GC last_Restart False›
       for S last_GC last_Restart
  proof -
    obtain T U where
      ST: ‹(S, T) ∈ state_wl_l None› and
      ‹correct_watching S› and
      ‹blits_in_ℒin S› and
      TU: ‹(T, U) ∈ twl_st_l None› and
      struct: ‹twl_struct_invs U› and
      ‹twl_list_invs T› and
      ‹clauses_to_update_l T = {#}› and
      ‹twl_stgy_invs U› and
      confl: ‹get_conflict U = None›
      using pre unfolding restart_abs_wl_pre_def restart_abs_l_pre_def restart_prog_pre_def apply -
      by blast

   show ?C
     using ST TU confl by auto

   have alien: ‹cdclW_restart_mset.no_strange_atm (stateW_of U)›
     using struct unfolding twl_struct_invs_def cdclW_restart_mset.cdclW_all_struct_inv_def
       pcdcl_all_struct_invs_def stateW_of_def
     by fast+
   then show ?A and ?B
      subgoal A
        using ST TU unfolding set_eq_iff in_set_all_atms_iff
          in_set_all_atms_iff in_set_all_init_atms_iff get_unit_clauses_wl_alt_def
          using literals_are_ℒin'_literals_are_ℒin_iff(3) struct by blast
      subgoal
        using ST TU alien unfolding set_eq_iff in_set_all_atms_iff all_atms_st_def
          in_set_all_atms_iff in_set_all_init_atms_iff get_unit_clauses_wl_alt_def
        apply (subst all_clss_lf_ran_m[symmetric])
        apply (subst all_clss_lf_ran_m[symmetric])
        unfolding image_mset_union
        by (auto simp: cdclW_restart_mset.no_strange_atm_def twl_st twl_st_l in_set_all_atms_iff
          in_set_all_init_atms_iff)
     done
  qed
  have P: ‹P›
    if
      ST: ‹(S, bt, bu, bv, bw, bx, NEk, UEk, NS, US, N0, U0, by, bz)
       ∈ twl_st_heur› and
      ‹∃last_GC last_Restart. restart_abs_wl_pre (bt, bu, bv, bw, bx, NEk, UEk, NS, US, N0, U0, by, bz) last_GC last_Restart False› and
      ‹restart_abs_wl_heur_pre
	S
	False› and
      lvl: ‹(lvl, i)
       ∈ {(i, b).
	  b = (i = count_decided (get_trail_wl (bt, bu, bv, bw, bx, NEk, UEk, NS, US, N0, U0, by, bz))) ∧
	  i ≤ count_decided (get_trail_wl (bt, bu, bv, bw, bx, NEk, UEk, NS, US, N0, U0, by, bz))}› and
      ‹i ∈ {_. True}› and
      ‹lvl ≠ count_decided_st_heur S› and
      i: ‹¬ i› and
    H: ‹
      isa_find_decomp_wl_imp (get_trail_wl_heur S) lvl (get_vmtf_heur S)
	≤ ⇓ {(a, b). (a,b) ∈ trail_pol (all_atms_st (bt, bu, bv, bw, bx, NEk, UEk, NS, US, N0, U0, by, bz)) ×f Id}
	    (find_decomp_w_ns (all_atms_st (bt, bu, bv, bw, bx, NEk, UEk, NS, US, N0, U0, by, bz)) bt lvl vm0) ⟹ P›
    for a aa ab ac ad b ae af ag ba ah ai aj ak al am bb an bc ao aq bd ar as at'
       au av aw be ax ay az bf bg bh bi bj bk bl bm bn bo bp bq bt bu bv aqbd
       bw bx "by" bz lvl i x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e x1f x2f S
       x1g x2g x1h x2h x1i x2i P NS US last_GC last_Restart N0 U0 NEk UEk heur heur2 stats M' stats42
  proof -
    let ?𝒜 = ‹all_atms_st (bt, bu, bv, bw, bx, NEk, UEk, NS, US, N0, U0, by, bz)›
    let ?bo = ‹get_vdom_aivdom (get_aivdom S)›
    let ?ae = ‹get_clauses_wl_heur S›
    let ?heur = ‹get_heur S›
    let ?vm = ‹get_vmtf_heur S›
    have
      tr: ‹(get_trail_wl_heur S, bt) ∈ trail_pol ?𝒜› and
      ‹valid_arena ?ae bu (set ?bo)› and
      vm: ‹?vm ∈ bump_heur ?𝒜 bt› and (*
      ‹(heur, bv)
       ∈ option_lookup_clause_rel ?𝒜› and
      ‹by = {#- lit_of x. x ∈# mset (drop ah (rev bt))#}› and
      ‹(ai, bz) ∈ ⟨Id⟩map_fun_rel (D0 ?𝒜)› and
      ‹no_dup bt› and
      ‹ao ∈ counts_maximum_level bt bv› and
      ‹cach_refinement_empty ?𝒜 aqbd› and
      ‹out_learned bt bv as› and
      ‹clss_size_corr bu bw bx NEk UEk NS US N0 U0 bp› and
      ‹vdom_m ?𝒜 bz bu ⊆ set ?bo› and
      ‹∀L∈#ℒall ?𝒜. nat_of_lit L ≤ unat32_max› and
      ‹?𝒜 ≠ {#}› and*)
      bounded: ‹isasat_input_bounded ?𝒜› and
      heur: ‹heuristic_rel ?𝒜 ?heur›
      using ST unfolding twl_st_heur_def all_atms_def
      by (auto)

    have n_d: ‹no_dup bt›
      using tr by (auto simp: trail_pol_def)
    show ?thesis
      apply (rule H)
      apply (rule isa_find_decomp_wl_imp_find_decomp_wl_imp[THEN fref_to_Down_curry2, THEN order_trans,
        of bt lvl ‹get_vmtf_heur S› _ _ _ ‹?𝒜›])
      subgoal using lvl i by auto
      subgoal using vm tr by auto
      apply (subst (3) Down_id_eq[symmetric])
      apply (rule order_trans)
      apply (rule ref_two_step')
      apply (rule find_decomp_wl_imp_find_decomp_wl'[THEN fref_to_Down_curry2, of _ bt lvl ‹get_vmtf_heur S›])
      subgoal
        using that(1-8) vm bounded n_d tr
	by (auto simp: find_decomp_w_ns_pre_def dest: trail_pol_literals_are_in_ℒin_trail)
      subgoal by auto
        using ST
        by (auto simp: find_decomp_w_ns_def conc_fun_RES twl_st_heur_def)
  qed
  note cong =  trail_pol_cong heuristic_rel_cong
      option_lookup_clause_rel_cong D0_cong isa_vmtf_cong
      cach_refinement_empty_cong vdom_m_cong isasat_input_nempty_cong
      isasat_input_bounded_cong heuristic_rel_cong

  show ?thesis
    supply [[goals_limit=1]]
    unfolding cdcl_twl_local_restart_wl_D_heur_def
    unfolding
      find_decomp_wl_st_int_def find_local_restart_target_level_def incr_restart_stat_def
       empty_Q_def find_local_restart_target_level_st_def nres_monad_laws
    apply (intro frefI nres_relI)
    apply clarify
    apply (rule ref_two_step)
    prefer 2
     apply (rule cdcl_twl_local_restart_wl_D_spec_int)
    unfolding bind_to_let_conv RES_RETURN_RES2 nres_monad_laws Let_def
    apply (refine_vcg)
    subgoal unfolding restart_abs_wl_heur_pre_def by blast
    apply assumption
    subgoal by (simp add: twl_st_heur_count_decided_st_alt_def)
    subgoal by (auto simp: twl_st_heur_def count_decided_st_heur_def trail_pol_def)

    apply (rule P)
    apply assumption+
      apply (rule refine_generalise1)
      apply assumption
    subgoal for a aa ab ac ad b ae af ag ba ah ai aj ak al az
      unfolding RETURN_def RES_RES2_RETURN_RES RES_RES13_RETURN_RES find_decomp_w_ns_def conc_fun_RES
        RES_RES13_RETURN_RES K2 K
      apply (auto simp: intro_spec_iff intro!: ASSERT_leI isa_length_trail_pre)
      apply (auto simp: isa_length_trail_length_u[THEN fref_to_Down_unRET_Id]
        intro: trail_pol_no_dup)
      apply (frule twl_st_heur_change_subsumed_clauses[where US' = ba and NS' = ag and
        lcount' = ‹get_learned_count a›])
      apply (solves ‹auto dest: H(2)›)[]
      apply (solves ‹auto simp: twl_st_heur_def›)[]
      apply (frule H(2))
      apply (frule H(3))
	apply (clarsimp simp: twl_st_heur_def)
	apply (rule_tac x=afa in exI)
	apply (auto simp: isa_length_trail_length_u[THEN fref_to_Down_unRET_Id] learned_clss_count_def
          all_atms_st_def
	  intro: trail_pol_no_dup)
      done
    done
qed



lemma distinct_mset_union_iff:
  ‹distinct_mset (xs + ys) = (distinct_mset xs ∧ distinct_mset ys ∧ set_mset xs ∩ set_mset ys = {})›
  by (induction xs) (auto)

lemma aivdom_inv_dec_remove_deleted_clauses_from_avdom:
  ‹aivdom_inv_dec avdom0 (dom_m N) ⟹
  mset (take a (get_avdom_aivdom ba)) ⊆# mset (get_avdom_aivdom avdom0) ⟹
    mset (take a (get_avdom_aivdom ba)) ∩# dom_m N = mset (get_avdom_aivdom avdom0) ∩# dom_m N ⟹
    get_vdom_aivdom ba = get_vdom_aivdom avdom0 ⟹
    get_ivdom_aivdom ba = get_ivdom_aivdom avdom0 ⟹
  mset (get_tvdom_aivdom ba) ⊆# mset (get_avdom_aivdom avdom0) ⟹
  mset (take a (get_avdom_aivdom ba)) ∩# dom_m N = mset (get_avdom_aivdom avdom0) ∩# dom_m N ⟹
  aivdom_inv_dec (take_avdom_aivdom a ba) (dom_m N)›
 supply [simp del] = distinct_finite_set_mset_subseteq_iff
 using distinct_mset_mono[of ‹mset (take a (get_avdom_aivdom ba))› ‹mset (get_avdom_aivdom avdom0)›]
 apply (auto simp: aivdom_inv_dec_alt_def2 distinct_mset_mono intro: distinct_take
   simp flip: distinct_subseteq_iff)
 apply auto
 apply (metis UnE comp_apply in_mono inter_iff set_mset_comp_mset)
 apply (subst distinct_subseteq_iff[symmetric])
 apply (auto dest: distinct_mset_mono)
 by (metis mset_subset_eqD set_mset_mset subsetD)

lemma remove_deleted_clauses_from_avdom:
  assumes ‹aivdom_inv_dec avdom0 (dom_m N)›
  shows ‹remove_deleted_clauses_from_avdom N avdom0 ≤ SPEC(λaivdom. aivdom_inv_dec aivdom (dom_m N) ∧
     get_vdom_aivdom aivdom = get_vdom_aivdom avdom0∧
     get_ivdom_aivdom aivdom = get_ivdom_aivdom avdom0∧
    mset (get_tvdom_aivdom aivdom) ⊆# mset (get_avdom_aivdom avdom0) ∧
   (∀C ∈ set (get_tvdom_aivdom aivdom). C ∈# dom_m N ∧ ¬irred N C ∧ length (N ∝ C) ≠ 2))›
proof -
  have dist_avdom: ‹distinct (get_avdom_aivdom avdom0)›
    using assms by (auto simp: aivdom_inv_dec_alt_def2)
  have I0: ‹remove_deleted_clauses_from_avdom_inv N avdom0 (0, 0, empty_tvdom avdom0)›
    unfolding remove_deleted_clauses_from_avdom_inv_def by auto
  have ISuc_keep:
    ‹x ⟹ remove_deleted_clauses_from_avdom_inv N avdom0
    (a+1, aa + 1, push_to_tvdom (get_avdom_aivdom ba ! aa) (swap_avdom_aivdom ba a aa))› (is ‹_ ⟹ ?A›) and
    ISuc_keep_no:
    ‹remove_deleted_clauses_from_avdom_inv N avdom0
    (a+1, aa + 1,  (swap_avdom_aivdom ba a aa))› (is ?B)
    if
      ‹remove_deleted_clauses_from_avdom_inv N avdom0 s› and
      ‹case s of (i, j, avdom) ⇒ j < length (get_avdom_aivdom avdom0)› and
      ‹s = (a, b)› and
      ‹b = (aa, ba)› and
      ‹get_avdom_aivdom ba ! aa ∈# dom_m N› and
      irred: ‹x ⟶ ¬ irred N (get_avdom_aivdom ba ! aa) ∧ length (N ∝ (get_avdom_aivdom ba ! aa)) ≠ 2›
    for ba aa s a b x
  proof -
    have [simp]: ‹aa < length (get_avdom_aivdom ba) ⟹
      add_mset (get_avdom_aivdom ba ! aa) (mset (take aa (get_avdom_aivdom ba)) + mset (drop (Suc aa) (get_avdom_aivdom ba))) =
      mset (get_avdom_aivdom ba)›
      using that apply -
      apply (subst (4)append_take_drop_id[symmetric, of ‹get_avdom_aivdom ba› aa])
      apply (subst mset_append)
      by (auto simp flip: Cons_nth_drop_Suc)
    have 1: ‹distinct (take a (get_avdom_aivdom ba) @ drop aa (get_avdom_aivdom ba))›
      using assms that
        distinct_mset_mono[of ‹mset (take a (get_avdom_aivdom ba) @ drop aa (get_avdom_aivdom ba))›
        ‹mset (get_avdom_aivdom avdom0)›]
      by (auto simp: aivdom_inv_dec_alt_def2 remove_deleted_clauses_from_avdom_inv_def distinct_mset_union_iff)
    have 2: ‹a = aa  ⟹distinct (get_avdom_aivdom ba)›
      by (metis ‹distinct (take a (get_avdom_aivdom ba) @ drop aa (get_avdom_aivdom ba))› append_take_drop_id)

    show ‹x ⟹ ?A›
      using assms that dist_avdom 1 2 apply -
      apply (cases ‹Suc a ≤ aa›)
      unfolding remove_deleted_clauses_from_avdom_inv_def prod.simps
      apply (auto simp: drop_swap_irrelevant swap_only_first_relevant Suc_le_eq take_update_last remove_deleted_clauses_from_avdom_inv_def
        intro: subset_mset.dual_order.trans 
        simp flip:  take_Suc_conv_app_nth Cons_nth_drop_Suc)
      apply (auto simp: take_Suc_conv_app_nth)
      done
    show ?B
      using 1 2  assms that dist_avdom 
      apply (cases ‹Suc a ≤ aa›)
      unfolding remove_deleted_clauses_from_avdom_inv_def prod.simps
      apply (auto simp: drop_swap_irrelevant swap_only_first_relevant Suc_le_eq take_update_last remove_deleted_clauses_from_avdom_inv_def
        intro: subset_mset.dual_order.trans 
        simp flip:  take_Suc_conv_app_nth Cons_nth_drop_Suc)
      apply (auto simp: take_Suc_conv_app_nth)
      done
qed
  have ISuc_nokeep:
    ‹remove_deleted_clauses_from_avdom_inv N avdom0
    (a, aa + 1, ba)› (is ?A)
    if
      ‹remove_deleted_clauses_from_avdom_inv N avdom0 s› and
      ‹case s of (i, j, avdom) ⇒ j < length (get_avdom_aivdom avdom0)› and
      ‹s = (a, b)› and
      ‹b = (aa, ba)› and
      ‹get_avdom_aivdom ba ! aa ∉# dom_m N›
    for ba aa s a b
  proof -
    have ‹aa < length (get_avdom_aivdom ba) ⟹
      add_mset (get_avdom_aivdom ba ! aa) (mset (take aa (get_avdom_aivdom ba)) + mset (drop (Suc aa) (get_avdom_aivdom ba))) =
      mset (get_avdom_aivdom ba)›
      using that apply -
      apply (subst (4)append_take_drop_id[symmetric, of ‹get_avdom_aivdom ba› aa])
      apply (subst mset_append)
      by (auto simp flip: Cons_nth_drop_Suc)
    have ‹distinct (take a (get_avdom_aivdom ba) @ drop aa (get_avdom_aivdom ba))›
      using assms that
        distinct_mset_mono[of ‹mset (take a (get_avdom_aivdom ba) @ drop aa (get_avdom_aivdom ba))›
        ‹mset (get_avdom_aivdom avdom0)›]
      by (auto simp: aivdom_inv_dec_alt_def2 remove_deleted_clauses_from_avdom_inv_def distinct_mset_union_iff)
    moreover have ‹a = aa  ⟹distinct (get_avdom_aivdom ba)›
      by (metis ‹distinct (take a (get_avdom_aivdom ba) @ drop aa (get_avdom_aivdom ba))› append_take_drop_id)

    ultimately show ?A
      using assms that dist_avdom apply -
      apply (cases ‹Suc a ≤ aa›)
      unfolding remove_deleted_clauses_from_avdom_inv_def prod.simps
      by (auto simp: drop_swap_irrelevant swap_only_first_relevant Suc_le_eq take_update_last remove_deleted_clauses_from_avdom_inv_def
        intro: subset_mset.dual_order.trans subset_mset_trans_add_mset
        simp flip:  take_Suc_conv_app_nth Cons_nth_drop_Suc)
  qed

  show ?thesis
    using assms
    unfolding remove_deleted_clauses_from_avdom_def Let_def is_candidate_for_removal_def
    apply (refine_vcg WHILEIT_rule[where R = ‹measure (λ(i, j, avdom). length (get_avdom_aivdom avdom) - j)›])
    subgoal by auto
    subgoal by (rule I0)
    subgoal by (auto simp: remove_deleted_clauses_from_avdom_inv_def)
    subgoal supply [[unify_trace_failure]] by (rule ISuc_keep)
    subgoal by auto
    subgoal by (rule ISuc_keep_no)
    subgoal by auto
    subgoal by (rule ISuc_nokeep)
    subgoal by (auto simp: aivdom_inv_dec_alt_def)
    subgoal by (auto simp: remove_deleted_clauses_from_avdom_inv_def)
    subgoal by (force intro!: aivdom_inv_dec_remove_deleted_clauses_from_avdom
      simp: remove_deleted_clauses_from_avdom_inv_def simp flip: distinct_subseteq_iff)
    subgoal by (auto simp: remove_deleted_clauses_from_avdom_inv_def)
    subgoal by (auto simp: remove_deleted_clauses_from_avdom_inv_def)
    subgoal by (force simp: remove_deleted_clauses_from_avdom_inv_def simp flip: distinct_subseteq_iff)
    subgoal by (auto simp: remove_deleted_clauses_from_avdom_inv_def)
    done
qed

(*TODO Move*)
lemma arena_status_mark_unused[simp]:
  ‹arena_status (mark_unused arena C) D = arena_status arena D›
  by (auto simp: arena_status_def mark_unused_def LBD_SHIFT_def
    nth_list_update')


lemma isa_is_candidate_for_removal_is_candidate_for_removal:
  assumes
    valid: ‹valid_arena arena N vdom› and
    C: ‹(C, C') ∈ nat_rel› and
    MM': ‹(M, M') ∈ trail_pol 𝒜› and
    𝒜: ‹set_mset (all_atms N NUE) = set_mset 𝒜›
  shows ‹isa_is_candidate_for_removal M C arena ≤ ⇓ bool_rel (is_candidate_for_removal C' N)›
proof -
  have [simp]: ‹C ∈# dom_m N ⟹ N ∝ C ≠ []› and
    C'[simp]: ‹C' = C›
    using valid C by (auto simp: valid_arena_nempty)
  have 1: ‹C ∈# dom_m N ⟹ atm_of (arena_lit arena C) ∈# 𝒜›
    using valid 𝒜
    by (cases ‹N ∝ C›)
     (auto simp: arena_act_pre_def arena_is_valid_clause_idx_def
      arena_lifting arena_dom_status_iff(1)
      arena_lit_pre_def all_atms_def all_lits_def
      ran_m_def all_lits_of_mm_add_mset all_lits_of_m_add_mset
      simp flip: arena_lifting
      dest: valid_arena_nempty
      dest!: multi_member_split)
  have 2: ‹C ∈# dom_m N ⟹  (arena_lit arena C) ∈# ℒall 𝒜›
    using 1 by (cases ‹arena_lit arena C›) (auto simp: ℒall_add_mset dest!: multi_member_split)
  have [simp]: ‹get_clause_LBD_pre arena C›  ‹arena_act_pre arena C›
    ‹arena_is_valid_clause_vdom arena C› ‹marked_as_used_pre arena C›
    if ‹C ∈# dom_m N›
    using valid that by (auto simp: get_clause_LBD_pre_def arena_is_valid_clause_idx_def
      arena_act_pre_def arena_is_valid_clause_vdom_def marked_as_used_pre_def)
  show ?thesis
    using 1 2 valid MM'
    unfolding isa_is_candidate_for_removal_def is_candidate_for_removal_def
      get_the_propagation_reason_pol_def mop_arena_lbd_def
      mop_arena_status_def mop_marked_as_used_def Let_def
    by (refine_vcg mop_arena_lit(1)
      mop_arena_length[THEN fref_to_Down_curry, THEN order_trans,of N C _ C vdom])
     (auto simp:
      arena_lifting arena_dom_status_iff(1) trail_pol_alt_def
      ann_lits_split_reasons_def
      intro: exI[of _ ‹C::nat›] exI[of _ vdom]
      dest: valid_arena_nempty)
qed


lemma isa_gather_candidates_for_reduction_remove_deleted_clauses_from_avdom:
  ‹valid_arena arena N (set vdom) ⟹ mset (get_avdom_aivdom avdom0) ⊆# mset vdom ⟹
  (M, M') ∈ trail_pol 𝒜 ⟹ set_mset (all_atms N NUE) = set_mset 𝒜 ⟹
  length (get_avdom_aivdom avdom0) ≤ length (get_vdom_aivdom avdom0) ⟹
  distinct vdom ⟹
  isa_gather_candidates_for_reduction M arena avdom0 ≤
  ⇓{((arena', st), st'). (st, st') ∈ Id ∧ length arena' = length arena ∧ valid_arena arena' N (set vdom)}
  (remove_deleted_clauses_from_avdom N avdom0)›
  unfolding isa_gather_candidates_for_reduction_def remove_deleted_clauses_from_avdom_def Let_def
  apply (refine_vcg WHILEIT_refine[where R= ‹{((arena', st), st'). (st, st') ∈ Id ∧ length arena' = length arena ∧ valid_arena arena' N (set vdom)}›]
    )
  subgoal by (auto dest!: valid_arena_vdom_le(2) size_mset_mono simp: distinct_card)
  subgoal by auto
  subgoal by (auto simp: remove_deleted_clauses_from_avdom_inv_def)
  subgoal by (auto simp: remove_deleted_clauses_from_avdom_inv_def)
  subgoal by auto
  subgoal by auto
  subgoal for x x' x1 x2 x1a x2a x1b x2b x1c x2c unfolding arena_is_valid_clause_vdom_def
    apply (auto intro!: exI[of _ N] exI[of _ ‹set vdom›] dest!: mset_eq_setD dest: mset_le_add_mset
      simp: Cons_nth_drop_Suc[symmetric] remove_deleted_clauses_from_avdom_inv_def)
    by (meson in_multiset_in_set mset_subset_eqD union_single_eq_member)
  subgoal by auto
  subgoal by auto
  subgoal by (auto simp: remove_deleted_clauses_from_avdom_inv_def)
  subgoal
    apply (auto simp: arena_lifting arena_dom_status_iff(1) Cons_nth_drop_Suc[symmetric] remove_deleted_clauses_from_avdom_inv_def
      dest!: mset_eq_setD dest: mset_le_add_mset)
    by (metis arena_dom_status_iff(1) mset_subset_eqD set_mset_mset union_single_eq_member)
  subgoal by (auto simp: arena_act_pre_def arena_is_valid_clause_idx_def)
    apply (rule isa_is_candidate_for_removal_is_candidate_for_removal; assumption?; auto intro!: valid_arena_mark_unused; fail)
  subgoal by auto
  subgoal by (auto intro!: valid_arena_mark_unused)
  subgoal by (auto intro!: valid_arena_mark_unused)
  subgoal by (auto intro!: valid_arena_mark_unused)
  subgoal by (auto intro!: valid_arena_mark_unused)
  subgoal by (auto intro!: valid_arena_mark_unused)
  done

(*TODO Move*)
lemma bind_result_subst_iff:
  ‹P ≤ ⇓ {(a,b). (f a, b) ∈ R} g ⟷
  do {
  a ← P;
  RETURN (f a)
  } ≤ ⇓ R g›
  by (cases P; cases g)
   (auto simp: RETURN_def RES_RES_RETURN_RES conc_fun_RES)

lemma isa_isa_gather_candidates_for_reduction_remove_deleted_clauses_from_avdom2:
  assumes ‹valid_arena arena N (set (get_vdom_aivdom avdom))›
    ‹aivdom_inv_dec avdom (dom_m N)› and
    MM': ‹(M, M') ∈ trail_pol 𝒜› and
    𝒜: ‹set_mset (all_atms N NUE) = set_mset 𝒜›
 shows
  ‹isa_gather_candidates_for_reduction M arena avdom ≤
   (SPEC (λ(arena', aivdom). aivdom_inv_dec aivdom (dom_m N) ∧
     get_vdom_aivdom aivdom = get_vdom_aivdom avdom∧
     get_ivdom_aivdom aivdom = get_ivdom_aivdom avdom∧
     mset (get_tvdom_aivdom aivdom) ⊆# mset (get_avdom_aivdom avdom) ∧
   valid_arena arena' N (set (get_vdom_aivdom avdom)) ∧
   length arena' = length arena ∧
   (∀C ∈ set (get_tvdom_aivdom aivdom). C ∈# dom_m N ∧ ¬irred N C ∧ length (N ∝ C) ≠ 2)))›
proof -
  have i: ‹mset (get_avdom_aivdom avdom) ⊆# mset (get_vdom_aivdom avdom)›
    ‹distinct (get_vdom_aivdom avdom)›
    ‹length (get_avdom_aivdom avdom) ≤ length (get_vdom_aivdom avdom)›
    using assms(2) by (auto simp: aivdom_inv_dec_alt_def dest: size_mset_mono)
  have H: ‹aivdom_inv (get_vdom_aivdom avdom, get_avdom_aivdom avdom, get_ivdom_aivdom avdom, get_tvdom_aivdom avdom) (dom_m N)›
    using assms(2) by (cases avdom) (auto simp: aivdom_inv_dec_def simp del: aivdom_inv.simps)
  show ?thesis
    apply (rule order_trans)
    apply (rule isa_gather_candidates_for_reduction_remove_deleted_clauses_from_avdom)
    apply (rule assms i)+
    apply (rule order_trans)
    apply (rule ref_two_step'[OF remove_deleted_clauses_from_avdom])
    apply (rule assms)
    apply (auto simp: conc_fun_RES)
    done
qed

lemma mset_inter_eqD: ‹x1m ∩# af = xa ∩# af ⟹
    set_mset x1m ∩ set_mset (af) = set_mset xa ∩ set_mset af› for x1m af xa
    by auto
      (metis Int_iff comp_apply set_mset_comp_mset set_mset_inter)+

lemma aivdom_inv_cong2:
  ‹mset vdom = mset vdom' ⟹ mset avdom = mset avdom' ⟹ mset ivdom = mset ivdom' ⟹ mset tvdom = mset tvdom' ⟹
    aivdom_inv (vdom, avdom, ivdom, tvdom) b ⟹ aivdom_inv (vdom', avdom', ivdom', tvdom') b›
  by (auto 3 3 simp: dest: same_mset_distinct_iff mset_eq_setD)

lemma aivdom_inv_dec_cong2:
  ‹aivdom_inv_dec aivdom b ⟹ mset (get_vdom_aivdom aivdom) = mset (get_vdom_aivdom aivdom') ⟹
  mset (get_avdom_aivdom aivdom) = mset (get_avdom_aivdom aivdom') ⟹
  mset (get_ivdom_aivdom aivdom) = mset (get_ivdom_aivdom aivdom') ⟹ 
  mset (get_tvdom_aivdom aivdom) = mset (get_tvdom_aivdom aivdom') ⟹ aivdom_inv_dec aivdom' b›
  using aivdom_inv_cong2[of ‹get_vdom_aivdom aivdom› ‹get_vdom_aivdom aivdom'›
    ‹get_avdom_aivdom aivdom› ‹get_avdom_aivdom aivdom'›
     ‹get_ivdom_aivdom aivdom› ‹get_ivdom_aivdom aivdom'› 
     ‹get_tvdom_aivdom aivdom› ‹get_tvdom_aivdom aivdom'› b]
  by (cases aivdom; cases aivdom') (auto simp: aivdom_inv_dec_def simp del: aivdom_inv.simps)

lemma sort_clauses_by_score_reorder:
  assumes
    ‹valid_arena arena N (set (get_vdom_aivdom vdom))› and
    ‹aivdom_inv_dec vdom (dom_m N)›
  shows ‹sort_clauses_by_score arena vdom
      ≤ SPEC
      (λvdom'.
       mset (get_avdom_aivdom vdom) = mset (get_avdom_aivdom vdom') ∧
       mset (get_vdom_aivdom vdom) = mset (get_vdom_aivdom vdom') ∧
       mset (get_ivdom_aivdom vdom) = mset (get_ivdom_aivdom vdom') ∧
       mset (get_tvdom_aivdom vdom) = mset (get_tvdom_aivdom vdom') ∧
    aivdom_inv_dec vdom' (dom_m N))›
proof -
  have ‹set (get_avdom_aivdom vdom) ⊆ set (get_vdom_aivdom vdom)›
    using assms(2)
    by (auto simp: aivdom_inv_dec_alt_def)
  then show ?thesis
    using assms
    unfolding sort_clauses_by_score_def
    apply refine_vcg
    unfolding valid_sort_clause_score_pre_def arena_is_valid_clause_vdom_def
      get_clause_LBD_pre_def arena_is_valid_clause_idx_def arena_act_pre_def
      valid_sort_clause_score_pre_at_def
    apply (auto simp: valid_sort_clause_score_pre_def twl_st_heur_restart_ana_def arena_dom_status_iff(2-)
      arena_dom_status_iff(1)[symmetric] in_set_conv_nth
      arena_act_pre_def get_clause_LBD_pre_def arena_is_valid_clause_idx_def twl_st_heur_restart_def
      intro:  aivdom_inv_dec_cong2 dest!: set_mset_mono mset_subset_eqD)
    using arena_dom_status_iff(1) apply force
    using arena_dom_status_iff(1) by (smt (verit, best) aivdom_inv_dec_alt_def mset_subset_eqD nth_mem set_mset_mset)
qed

lemma specify_left_RES:
  assumes "m ≤ RES Φ"
  assumes "⋀x. x ∈ Φ ⟹ f x ≤ M"  
  shows "do { x ← m; f x } ≤ M"
  using assms by (auto simp: pw_le_iff refine_pw_simps)  

lemma sort_vdom_heur_reorder_vdom_wl:
  ‹(sort_vdom_heur, reorder_vdom_wl) ∈ twl_st_heur_restart_ana r →f ⟨{(S, T). (S, T) ∈ twl_st_heur_restart_ana r ∧
  (∀C ∈ set (get_tvdom S). C ∈# dom_m (get_clauses_wl T) ∧ ¬irred (get_clauses_wl T) C ∧
    length (get_clauses_wl T ∝ C) ≠ 2)}⟩nres_rel›
proof -
   have mark_to_delete_clauses_wl_pre_same_atms: ‹set_mset (all_atms_st T) = set_mset (all_init_atms_st T)›
    if ‹mark_to_delete_clauses_wl_pre T› for T
    using that unfolding mark_to_delete_clauses_wl_pre_def mark_to_delete_clauses_l_pre_def apply -
    apply normalize_goal+
    by (rule literals_are_ℒin'_literals_are_ℒin_iff(3)[symmetric]) assumption+

  show ?thesis
    unfolding reorder_vdom_wl_def sort_vdom_heur_def Let_def
    apply (intro frefI nres_relI)
    apply refine_rcg
    subgoal by (auto simp: twl_st_heur_restart_ana_def twl_st_heur_restart_def aivdom_inv_dec_alt_def
      dest!: valid_arena_vdom_subset size_mset_mono)
    subgoal by (auto simp: twl_st_heur_restart_ana_def twl_st_heur_restart_def aivdom_inv_dec_alt_def
      dest!: valid_arena_vdom_subset size_mset_mono)
      apply (rule specify_left_RES)
      apply (rule_tac  N = ‹get_clauses_wl y› and M' = ‹get_trail_wl y› and
        𝒜 = ‹all_init_atms_st y› and
        NUE = ‹get_unit_clauses_wl y + get_subsumed_clauses_wl y + get_clauses0_wl y› in
        isa_isa_gather_candidates_for_reduction_remove_deleted_clauses_from_avdom2[unfolded conc_fun_RES])
    subgoal for x y
      by (case_tac y; auto simp: twl_st_heur_restart_ana_def twl_st_heur_restart_def mem_Collect_eq prod.case)
    subgoal for x y
      by (case_tac y; auto simp: twl_st_heur_restart_ana_def twl_st_heur_restart_def
        mem_Collect_eq prod.case)
    subgoal for x y
      by (case_tac y; auto simp: twl_st_heur_restart_ana_def twl_st_heur_restart_def mem_Collect_eq prod.case all_init_atms_st_def)
    subgoal for x y
      unfolding all_atms_st_def[symmetric]
      by (rule mark_to_delete_clauses_wl_pre_same_atms)
    apply (subst case_prod_beta)
    apply (subst assert_bind_spec_conv, intro conjI)
    subgoal for x y
      unfolding valid_sort_clause_score_pre_def arena_is_valid_clause_vdom_def
        get_clause_LBD_pre_def arena_is_valid_clause_idx_def arena_act_pre_def
      by (intro impI ballI)
       (auto intro!: exI[of _ ‹get_clauses_wl y›] exI[of _ ‹set (get_vdom x)›]
         simp: valid_sort_clause_score_pre_def twl_st_heur_restart_ana_def arena_dom_status_iff(2-)
        arena_dom_status_iff(1)[symmetric]
        arena_act_pre_def get_clause_LBD_pre_def arena_is_valid_clause_idx_def twl_st_heur_restart_def)
    apply (subst assert_bind_spec_conv, intro conjI)
    subgoal by auto
    apply (subst assert_bind_spec_conv, intro conjI)
    subgoal by (auto simp: twl_st_heur_restart_ana_def twl_st_heur_restart_def aivdom_inv_dec_alt_def
      dest!: valid_arena_vdom_subset size_mset_mono)
    subgoal for x y x1
      apply (rewrite at ‹_ ≤ ⌑› Down_id_eq[symmetric])
      apply (rule bind_refine_spec)
      prefer 2
      apply (rule sort_clauses_by_score_reorder[of _  ‹get_clauses_wl y›])
      subgoal
       by (clarsimp simp: twl_st_heur_restart_ana_def twl_st_heur_restart_def dest: mset_eq_setD)
     subgoal
       by (case_tac ‹x1›; case_tac ‹get_content (snd x1)›) simp
      subgoal
        by (auto 5 3 simp: twl_st_heur_restart_ana_def twl_st_heur_restart_def intro: aivdom_inv_dec_cong2
          dest: mset_eq_setD)
      done
    done
qed

lemma (in -) insort_inner_clauses_by_score_invI:
   ‹valid_sort_clause_score_pre a ba ⟹
       mset ba = mset a2' ⟹
       a1' < length a2' ⟹
       valid_sort_clause_score_pre_at a (a2' ! a1')›
  unfolding valid_sort_clause_score_pre_def all_set_conv_nth valid_sort_clause_score_pre_at_def
  by (metis in_mset_conv_nth)+


lemma sort_clauses_by_score_invI:
  ‹valid_sort_clause_score_pre a b ⟹
       mset b = mset a2' ⟹ valid_sort_clause_score_pre a a2'›
  using mset_eq_setD unfolding valid_sort_clause_score_pre_def by blast


lemma valid_sort_clause_score_pre_swap:
  ‹valid_sort_clause_score_pre a b ⟹ x < length b ⟹
       ba < length b ⟹ valid_sort_clause_score_pre a (swap b x ba)›
  by (auto simp: valid_sort_clause_score_pre_def)


lemma mark_to_delete_clauses_wl_post_alt_def:
  ‹mark_to_delete_clauses_wl_post S0 S ⟷
    (∃T0 T.
        (S0, T0) ∈ state_wl_l None ∧
        (S, T) ∈ state_wl_l None ∧
        blits_in_ℒin S0 ∧
        blits_in_ℒin S ∧
       get_unkept_learned_clss_wl S = {#} ∧
       get_subsumed_learned_clauses_wl S = {#} ∧
       get_learned_clauses0_wl S = {#} ∧
        (∃U0 U. (T0, U0) ∈ twl_st_l None ∧
               (T, U) ∈ twl_st_l None ∧
               remove_one_annot_true_clause** T0 T ∧
               twl_list_invs T0 ∧
               twl_struct_invs U0 ∧
               twl_list_invs T ∧
               twl_struct_invs U ∧
               get_conflict_l T0 = None ∧
	       clauses_to_update_l T0 = {#}) ∧
        correct_watching S0 ∧ correct_watching S)›
  unfolding mark_to_delete_clauses_wl_post_def mark_to_delete_clauses_l_post_def
    mark_to_delete_clauses_l_pre_def
  apply (rule iffI; normalize_goal+)
  subgoal for T0 T U0
    apply (rule exI[of _ T0])
    apply (rule exI[of _ T])
    apply (intro conjI)
    apply auto[7]
    apply (rule exI[of _ U0])
    apply auto
    using rtranclp_remove_one_annot_true_clause_cdcl_twl_restart_l2[of T0 T U0]
      rtranclp_cdcl_twl_restart_l_list_invs[of T0]
    apply (auto dest: )
     using rtranclp_cdcl_twl_restart_l_list_invs by blast
  subgoal for T0 T U0 U
    apply (rule exI[of _ T0])
    apply (rule exI[of _ T])
    apply (intro conjI)
    apply auto[3]
    apply (rule exI[of _ U0])
    apply auto
    done
  done

lemma mark_to_delete_clauses_wl_D_heur_pre_alt_def:
  ‹(∃S'. (S, S') ∈ twl_st_heur ∧ mark_to_delete_clauses_wl_pre S') ⟹
  mark_to_delete_clauses_wl_D_heur_pre S› (is ‹?pre ⟹ ?A›) and
    mark_to_delete_clauses_wl_D_heur_pre_twl_st_heur:
      ‹mark_to_delete_clauses_wl_pre T ⟹
        (S, T) ∈ twl_st_heur ⟹ (S, T) ∈ twl_st_heur_restart› (is ‹_ ⟹ _ ⟹ ?B›) and
    mark_to_delete_clauses_wl_post_twl_st_heur:
      ‹mark_to_delete_clauses_wl_post T0 T ⟹
        (S, T) ∈ twl_st_heur_restart ⟹ (clss_size_resetUS0_st S, T) ∈ twl_st_heur› (is ‹_ ⟹ ?Cpre ⟹ ?C›)
proof -
  note cong = trail_pol_cong heuristic_rel_cong
      option_lookup_clause_rel_cong D0_cong isa_vmtf_cong phase_saving_cong
      cach_refinement_empty_cong vdom_m_cong isasat_input_nempty_cong
      isasat_input_bounded_cong empty_occs_list_cong

  show ?A if ?pre
    using that apply -
    supply [[goals_limit=1]]
    unfolding mark_to_delete_clauses_wl_D_heur_pre_def mark_to_delete_clauses_wl_pre_def
      mark_to_delete_clauses_l_pre_def
    apply normalize_goal+
    subgoal for T U V
      using literals_are_ℒin'_literals_are_ℒin_iff(3)[of T U V]
        cong[of ‹all_atms_st T› ‹all_init_atms_st T›]
	vdom_m_cong[of ‹all_atms_st T› ‹all_init_atms_st T› ‹get_watched_wl T› ‹get_clauses_wl T›]
      apply -
      apply (rule exI[of _ T])
      apply (intro conjI) defer
      apply (rule exI[of _ U])
      apply (intro conjI) defer
      apply (rule exI[of _ V])
      apply (simp_all del: isasat_input_nempty_def isasat_input_bounded_def)
      apply (cases S; cases T)
      by (auto simp add: twl_st_heur_def twl_st_heur_restart_def all_init_atms_st_def
        intro: clss_size_corr_restart_clss_size_corr(1)
        simp del: isasat_input_nempty_def)
    done
  show ‹mark_to_delete_clauses_wl_pre T ⟹ (S, T) ∈ twl_st_heur ⟹ ?B›
    supply [[goals_limit=1]]
    unfolding mark_to_delete_clauses_wl_D_heur_pre_def mark_to_delete_clauses_wl_pre_def
      mark_to_delete_clauses_l_pre_def mark_to_delete_clauses_wl_pre_def
    apply normalize_goal+
    subgoal for U V
      using literals_are_ℒin'_literals_are_ℒin_iff(3)[of T U V]
        cong[of ‹all_atms_st T› ‹all_init_atms_st T›]
	vdom_m_cong[of ‹all_atms_st T› ‹all_init_atms_st T› ‹get_watched_wl T› ‹get_clauses_wl T›]
      apply -
      apply (simp_all del: isasat_input_nempty_def isasat_input_bounded_def)
      apply (cases S; cases T)
      by (auto simp add: twl_st_heur_def twl_st_heur_restart_def all_init_atms_st_def all_atms_st_def
        intro: clss_size_corr_restart_clss_size_corr(1)
        simp del: isasat_input_nempty_def)
    done
  show  ‹mark_to_delete_clauses_wl_post T0 T ⟹ ?Cpre ⟹ ?C›
    supply [[goals_limit=1]]
    unfolding mark_to_delete_clauses_wl_post_alt_def
    apply normalize_goal+
    subgoal for U0 U V0 V
      using literals_are_ℒin'_literals_are_ℒin_iff(3)[of T U V]
        cong[of ‹all_init_atms_st T› ‹all_atms_st T›]
	vdom_m_cong[of ‹all_init_atms_st T› ‹all_atms_st T› ‹get_watched_wl T› ‹get_clauses_wl T›]
      apply -
      apply (simp_all del: isasat_input_nempty_def isasat_input_bounded_def)
      apply (cases S; cases T)
      by (auto simp add: twl_st_heur_def twl_st_heur_restart_def all_init_atms_st_def all_atms_st_def
        clss_size_resetUS0_st_def
        simp del: isasat_input_nempty_def
        intro: clss_size_corr_restart_clss_size_corr(2))
    done
qed


lemma find_largest_lbd_and_size:
  assumes
    ‹(S,T) ∈ twl_st_heur_restart_ana' r u›
  shows ‹find_largest_lbd_and_size l S ≤SPEC (λ_. True)›
proof -
  have arena: ‹valid_arena (get_clauses_wl_heur S) (get_clauses_wl T) (set (get_vdom S))› and
    avdom: ‹aivdom_inv_dec (get_aivdom S) (dom_m (get_clauses_wl T))›
    using assms unfolding twl_st_heur_restart_ana_def twl_st_heur_restart_def by auto

  have [intro!]: ‹clause_not_marked_to_delete_heur_pre (S, get_tvdom S ! i)›
    ‹¬ ¬ clause_not_marked_to_delete_heur S (get_tvdom S ! i) ⟹ get_clause_LBD_pre (get_clauses_wl_heur S) (get_tvdom S ! i)›
    ‹¬ ¬ clause_not_marked_to_delete_heur S (get_tvdom S ! i) ⟹ arena_is_valid_clause_idx (get_clauses_wl_heur S) (get_tvdom S ! i)›
    if ‹i < length (get_tvdom S)›
    for i
    using arena avdom multi_member_split[of ‹get_tvdom S ! i› ‹mset (get_tvdom S)›] that
      arena_dom_status_iff(1)[OF arena, of ‹get_tvdom S ! i›]
    unfolding clause_not_marked_to_delete_heur_pre_def arena_is_valid_clause_vdom_def
      aivdom_inv_dec_alt_def get_clause_LBD_pre_def arena_is_valid_clause_idx_def
      clause_not_marked_to_delete_heur_def
    by (auto intro!: exI[of _ ‹get_clauses_wl T›] exI[of _ ‹set (get_vdom S)›]
      simp: arena_lifting)
  have le: ‹length (get_tvdom S) ≤ length (get_clauses_wl_heur S)›
    using avdom valid_arena_vdom_le[OF arena] unfolding aivdom_inv_dec_alt_def by (auto simp: distinct_card dest: size_mset_mono)

  show ?thesis
    unfolding find_largest_lbd_and_size_def mop_clause_not_marked_to_delete_heur_def nres_monad3
      mop_arena_lbd_st_def mop_arena_lbd_def mop_arena_length_st_def mop_arena_length_def
    apply (refine_vcg WHILEIT_rule[where R = ‹measure (λ(i, _, _). length (get_tvdom S) - i)›])
    subgoal by (rule le)
    subgoal by auto
    subgoal by auto
    subgoal by auto
    subgoal by (auto simp: access_tvdom_at_pre_def)
    subgoal by auto
    subgoal by auto
    subgoal by auto
    subgoal by auto
    subgoal by auto
    subgoal by auto
    subgoal by auto
    subgoal by auto
    done
qed

lemma mark_to_delete_clauses_wl_D_heur_alt_def:
    ‹mark_to_delete_clauses_wl_D_heur  = (λS0. do {
          ASSERT (mark_to_delete_clauses_wl_D_heur_pre S0);
          S ← sort_vdom_heur S0;
          _ ← RETURN (get_tvdom S);
          l ← number_clss_to_keep S;
          (lbd, sze) ← find_largest_lbd_and_size l S;
          ASSERT
               (length (get_tvdom S) ≤ length (get_clauses_wl_heur S0));
          (i, T) ←
            WHILET⇗λ_. True⇖ (λ(i, S). i < length (get_tvdom S))
             (λ(i, T). do {
                   ASSERT (i < length (get_tvdom T));
                   ASSERT (access_tvdom_at_pre T i);
                   ASSERT
                        (clause_not_marked_to_delete_heur_pre
                          (T, get_tvdom T ! i));
                   b ← mop_clause_not_marked_to_delete_heur T
                        (get_tvdom T ! i);
                   if ¬b then RETURN (i, delete_index_vdom_heur i T)
                   else do {
                          ASSERT
                               (access_lit_in_clauses_heur_pre
                                 ((T, get_tvdom T ! i), 0));
                          ASSERT
                               (length (get_clauses_wl_heur T)
                                ≤ length (get_clauses_wl_heur S0));
                          ASSERT
                               (length (get_tvdom T)
                                ≤ length (get_clauses_wl_heur T));
                          L ← mop_access_lit_in_clauses_heur T
                               (get_tvdom T ! i) 0;
                          D ← get_the_propagation_reason_pol
                               (get_trail_wl_heur T) L;
                          ASSERT
                               (arena_is_valid_clause_idx
                                 (get_clauses_wl_heur T) (get_tvdom T ! i));
                          let can_del = (D ≠ Some (get_tvdom T ! i) ∧
                             arena_length (get_clauses_wl_heur T) (get_tvdom T ! i) ≠ 2);
                          if can_del
                          then do {
                                wasted ← mop_arena_length_st T (get_tvdom T ! i);
                                _ ← log_del_clause_heur T (get_tvdom T ! i);
                                 ASSERT(mark_garbage_pre
                                   (get_clauses_wl_heur T, get_tvdom T ! i) ∧
                                   1 ≤ clss_size_lcount (get_learned_count T) ∧ i < length (get_tvdom T));
                                 RETURN
                                  (i, mark_garbage_heur3 (get_tvdom T ! i) i (incr_wasted_st (of_nat wasted) T))
                               }
                          else do {
                                 RETURN (i + 1, T)
                               }
                        }
                 })
             (l, S);
          ASSERT
               (length (get_tvdom T) ≤ length (get_clauses_wl_heur S0));
         incr_reduction_stat (set_stats_size_limit_st lbd sze T)
        })›
    unfolding mark_to_delete_clauses_wl_D_heur_def
      mop_arena_lbd_def mop_arena_status_def mop_arena_length_def
      mop_marked_as_used_def bind_to_let_conv Let_def
      nres_monad3 mop_mark_garbage_heur3_def mop_mark_unused_st_heur_def
      incr_wasted_st_twl_st
    by (auto intro!: ext bind_cong[OF refl])


lemma mark_to_delete_clauses_GC_wl_D_heur_alt_def:
    ‹mark_to_delete_clauses_GC_wl_D_heur  = (λS0. do {
          ASSERT (mark_to_delete_clauses_GC_wl_D_heur_pre S0);
          S ← sort_vdom_heur S0;
          _ ← RETURN (get_tvdom S);
          l ← number_clss_to_keep S;
          (lbd, sze) ← find_largest_lbd_and_size l S;
          ASSERT
               (length (get_tvdom S) ≤ length (get_clauses_wl_heur S0));
          (i, T) ←
            WHILET⇗λ_. True⇖ (λ(i, S). i < length (get_tvdom S))
             (λ(i, T). do {
                   ASSERT (i < length (get_tvdom T));
                   ASSERT (access_tvdom_at_pre T i);
                   ASSERT
                        (clause_not_marked_to_delete_heur_pre
                          (T, get_tvdom T ! i));
                   b ← mop_clause_not_marked_to_delete_heur T
                        (get_tvdom T ! i);
                   if ¬b then RETURN (i, delete_index_vdom_heur i T)
                   else do {
                          ASSERT
                               (access_lit_in_clauses_heur_pre
                                 ((T, get_tvdom T ! i), 0));
                          ASSERT
                               (length (get_clauses_wl_heur T)
                                ≤ length (get_clauses_wl_heur S0));
                          ASSERT
                               (length (get_tvdom T)
                                ≤ length (get_clauses_wl_heur T));
                          ASSERT
                               (arena_is_valid_clause_idx
                                 (get_clauses_wl_heur T) (get_tvdom T ! i));
                          let can_del = (arena_length (get_clauses_wl_heur T) (get_tvdom T ! i) ≠ 2);
                          if can_del
                          then do {
                                wasted ← mop_arena_length_st T (get_tvdom T ! i);
                                _ ← log_del_clause_heur T (get_tvdom T ! i);
                                 ASSERT(mark_garbage_pre
                                   (get_clauses_wl_heur T, get_tvdom T ! i) ∧
                                   1 ≤ clss_size_lcount (get_learned_count T)∧ i < length (get_tvdom T));
                                 RETURN
                                  (i, mark_garbage_heur3 (get_tvdom T ! i) i (incr_wasted_st (of_nat wasted) T))
                               }
                          else do {
                                 RETURN
                                  (i + 1, T)
                               }
                        }
                 })
             (l, S);
          ASSERT
               (length (get_tvdom T) ≤ length (get_clauses_wl_heur S0));
          incr_restart_stat (set_stats_size_limit_st lbd sze T)
        })›
    unfolding mark_to_delete_clauses_GC_wl_D_heur_def
      mop_arena_lbd_def mop_arena_status_def mop_arena_length_def
      mop_marked_as_used_def bind_to_let_conv Let_def
      nres_monad3 mop_mark_garbage_heur3_def mop_mark_unused_st_heur_def
      incr_wasted_st_twl_st
    by (auto intro!: ext intro!: bind_cong[OF refl])

lemma learned_clss_count_mark_garbage_heur3:
  ‹clss_size_lcount (get_learned_count xs) ≥ Suc 0 ⟹ learned_clss_count (mark_garbage_heur3 C i xs) = (learned_clss_count xs) - 1› and
  learned_clss_count_incr_st[simp]:
  ‹learned_clss_count (incr_wasted_st b xs) = learned_clss_count xs›
  by (cases xs; auto simp: mark_garbage_heur3_def incr_wasted_st_def learned_clss_count_def; fail)+

lemma mark_to_delete_clauses_wl_D_heur_mark_to_delete_clauses_wl_D:
  ‹(mark_to_delete_clauses_wl_D_heur, mark_to_delete_clauses_wl) ∈
     twl_st_heur_restart_ana' r u →f ⟨twl_st_heur_restart_ana' r u⟩nres_rel›
proof -
  have mark_to_delete_clauses_wl_D_alt_def:
    ‹mark_to_delete_clauses_wl  = (λS0. do {
      ASSERT(mark_to_delete_clauses_wl_pre S0);
      S ← reorder_vdom_wl S0;
      xs ← collect_valid_indices_wl S;
      l ← SPEC(λ_::nat. True);
      _ ← SPEC(λ_::nat×nat. True);
      (_, S, _) ← WHILET⇗mark_to_delete_clauses_wl_inv S xs⇖
        (λ(i, T, xs). i < length xs)
        (λ(i, T, xs). do {
          b ← RETURN (xs!i ∈# dom_m (get_clauses_wl T));
          if ¬b then RETURN (i, T, delete_index_and_swap xs i)
          else do {
            ASSERT(0 < length (get_clauses_wl T∝(xs!i)));
	    ASSERT (get_clauses_wl T ∝ (xs ! i) ! 0 ∈# ℒall (all_init_atms_st T));
            K ← RETURN (get_clauses_wl T ∝ (xs ! i) ! 0);
            b ← RETURN (); ― ‹propagation reason›
            can_del ← SPEC(λb. b ⟶
              (Propagated (get_clauses_wl T∝(xs!i)!0) (xs!i) ∉ set (get_trail_wl T)) ∧
               ¬irred (get_clauses_wl T) (xs!i) ∧ length (get_clauses_wl T ∝ (xs!i)) ≠ 2);
            ASSERT(i < length xs);
            if can_del
            then do{
              _  ← RETURN (length (get_clauses_wl T ∝ (xs!i)));
              _ ← RETURN (log_clause T (xs!i));
              RETURN (i, mark_garbage_wl (xs!i) T, delete_index_and_swap xs i)}
            else
              RETURN (i+1, T, xs)
          }
        })
        (l, S, xs);
      remove_all_learned_subsumed_clauses_wl S
    })›
    unfolding mark_to_delete_clauses_wl_def reorder_vdom_wl_def bind_to_let_conv Let_def nres_monad3
      summarize_ASSERT_conv
    by (force intro!: ext)

  have mono: ‹g = g' ⟹ do {f; g} = do {f; g'}›
     ‹(⋀x. h x = h' x) ⟹ do {x ← f; h x} = do {x ← f; h' x}› for f f' :: ‹_ nres› and g g' and h h'
    by auto
  have mark_to_delete_clauses_wl_pre_same_atms: ‹set_mset (all_atms_st T) = set_mset (all_init_atms_st T)›
    if ‹mark_to_delete_clauses_wl_pre T› for T
    using that unfolding mark_to_delete_clauses_wl_pre_def mark_to_delete_clauses_l_pre_def apply -
    apply normalize_goal+
    by (rule literals_are_ℒin'_literals_are_ℒin_iff(3)[symmetric]) assumption+
  have mark_to_delete_clauses_wl_D_heur_pre_cong:
    ‹aivdom_inv_dec vdom' (dom_m (get_clauses_wl S')) ⟹
    mset (get_vdom_aivdom (get_aivdom T)) = mset (get_vdom_aivdom vdom') ⟹
     (T, S') ∈ twl_st_heur_restart ⟹
    mark_to_delete_clauses_wl_pre S' ⟹
    mark_to_delete_clauses_wl_D_heur_pre T ⟹
    valid_arena N'' (get_clauses_wl S') (set (get_vdom_aivdom (get_aivdom T))) ⟹
    mark_to_delete_clauses_wl_D_heur_pre (set_clauses_wl_heur N'' (set_aivdom_wl_heur vdom' T))›
    for M' N' D' j W' vm clvls cach lbd outl stats fast_ema slow_ema avdom avdom'
      ccount lcount heur old_arena ivdom opts S' vdom' N'' T
    using mset_eq_setD[of ‹get_vdom_aivdom (get_aivdom T)› ‹get_vdom_aivdom vdom'›, symmetric] apply -
    unfolding mark_to_delete_clauses_wl_D_heur_pre_def apply normalize_goal+
    by (rule_tac x=S' in exI)
     (clarsimp simp: twl_st_heur_restart_def dest: mset_eq_setD intro: )

  have [refine0]:
    ‹sort_vdom_heur S ≤ ⇓ {(U, V). (U, V) ∈ twl_st_heur_restart_ana' r u ∧ V = T ∧
         (mark_to_delete_clauses_wl_pre T ⟶ mark_to_delete_clauses_wl_pre V) ∧
          (mark_to_delete_clauses_wl_D_heur_pre S ⟶ mark_to_delete_clauses_wl_D_heur_pre U) ∧
         (∀C∈set (get_tvdom U). ¬irred (get_clauses_wl V) C ∧ length (get_clauses_wl V ∝ C) ≠ 2)}
         (reorder_vdom_wl T)› (is ‹_ ≤ ⇓?sort _›)
    if ‹(S, T) ∈ twl_st_heur_restart_ana' r u› and ‹mark_to_delete_clauses_wl_pre T› for S T
    supply [simp del] = EQ_def
    using that unfolding reorder_vdom_wl_def sort_vdom_heur_def Let_def
    apply (refine_rcg ASSERT_leI)
    subgoal by (auto simp: twl_st_heur_restart_ana_def twl_st_heur_restart_def aivdom_inv_dec_alt_def
      dest!: valid_arena_vdom_subset size_mset_mono)
    subgoal by (auto simp: twl_st_heur_restart_ana_def twl_st_heur_restart_def aivdom_inv_dec_alt_def
      dest!: valid_arena_vdom_subset size_mset_mono)
      apply (rule specify_left_RES)
      apply (rule_tac  N = ‹get_clauses_wl T› and M' = ‹get_trail_wl T› and
        𝒜 = ‹all_init_atms_st T› and
        NUE = ‹get_unit_clauses_wl T + get_subsumed_clauses_wl T + get_clauses0_wl T› in
     isa_isa_gather_candidates_for_reduction_remove_deleted_clauses_from_avdom2[unfolded conc_fun_RES])
    subgoal
      by (case_tac T; auto simp: twl_st_heur_restart_ana_def twl_st_heur_restart_def mem_Collect_eq prod.case)
    subgoal
      by (case_tac T; auto simp: twl_st_heur_restart_ana_def twl_st_heur_restart_def mem_Collect_eq prod.case)
    subgoal
      by (case_tac T; auto simp: twl_st_heur_restart_ana_def twl_st_heur_restart_def mem_Collect_eq prod.case
        all_init_atms_st_def)
    subgoal
      unfolding all_atms_st_def[symmetric]
      by (rule mark_to_delete_clauses_wl_pre_same_atms)
    apply (subst case_prod_beta)
    apply (intro ASSERT_leI)
    subgoal
      unfolding valid_sort_clause_score_pre_def arena_is_valid_clause_vdom_def
        get_clause_LBD_pre_def arena_is_valid_clause_idx_def arena_act_pre_def
      by (auto simp: valid_sort_clause_score_pre_def twl_st_heur_restart_ana_def arena_dom_status_iff(1)[symmetric]
        arena_act_pre_def get_clause_LBD_pre_def arena_is_valid_clause_idx_def twl_st_heur_restart_def aivdom_inv_dec_alt_def
        intro!: exI[of _ ‹get_clauses_wl T›] exI[of _ ‹set (get_vdom S)›]
        dest: set_mset_mono mset_subset_eqD)
    subgoal by (auto simp: EQ_def)
    subgoal
      by (cases T)
       (clarsimp simp add: twl_st_heur_restart_ana_def valid_arena_vdom_subset twl_st_heur_restart_def aivdom_inv_dec_alt_def case_prod_beta split: 
        dest!: size_mset_mono valid_arena_vdom_subset)
    subgoal  for arena_aivdom
      apply (rewrite at ‹_ ≤ ⌑› Down_id_eq[symmetric])
      apply (rule bind_refine_spec)
      prefer 2
      apply (rule sort_clauses_by_score_reorder[of _ ‹get_clauses_wl T›])
      subgoal
        by (auto simp: twl_st_heur_restart_ana_def twl_st_heur_restart_def dest: mset_eq_setD)
      subgoal
        by (cases ‹arena_aivdom›; cases ‹get_content (snd arena_aivdom)›)
         (simp add: twl_st_heur_restart_ana_def twl_st_heur_restart_def)
      subgoal
        apply auto
        apply (auto simp: learned_clss_count_def (* twl_st_heur_restart_ana_def twl_st_heur_restart_def *)
          intro: mark_to_delete_clauses_wl_D_heur_pre_cong
          intro: aivdom_inv_cong2
          dest: mset_eq_setD)
          apply (auto 4 3 simp: twl_st_heur_restart_ana_def twl_st_heur_restart_def 
            intro: aivdom_inv_cong2 dest: mset_eq_setD; fail)[]
          apply (rule mark_to_delete_clauses_wl_D_heur_pre_cong)
          apply assumption+
          apply (auto simp: twl_st_heur_restart_ana_def twl_st_heur_restart_def)
          done
          done
        done

  have [refine0]: ‹RETURN (get_tvdom x) ≤ ⇓ {(xs, xs'). xs = xs' ∧ xs = get_tvdom x ∧
    (∀C∈set (get_tvdom x). ¬irred (get_clauses_wl y) C ∧ length (get_clauses_wl y ∝ C) ≠ 2)}
    (collect_valid_indices_wl y)›
    (is ‹_ ≤ ⇓ ?indices _›)
    if
      ‹(x, y) ∈ ?sort S T› and
      ‹mark_to_delete_clauses_wl_D_heur_pre x›
    for x y S T
  proof -
    show ?thesis using that by (auto simp: collect_valid_indices_wl_def simp: RETURN_RES_refine_iff)
  qed

  have init:
    ‹(u', xs) ∈ ?indices S Sa ⟹
    (l, la) ∈ nat_rel ⟹
    (S, Sa) ∈ twl_st_heur_restart_ana' r u ⟹
    ((l, S), la, Sa, xs) ∈  nat_rel ×f
    {(Sa', (T, xs)). (Sa', T) ∈ twl_st_heur_restart_ana' r u ∧ xs = get_tvdom Sa' ∧
    set (get_tvdom Sa') ⊆ set (get_tvdom S) ∧
      (∀C∈set (get_tvdom Sa'). ¬irred (get_clauses_wl T) C ∧ length (get_clauses_wl T ∝ C) ≠ 2)}›
    (is ‹_ ⟹ _ ⟹ _ ⟹ _ ∈ ?R›)
    for x y S Sa xs l la u'
    by auto

  define reason_rel where
    ‹reason_rel K x1a ≡ {(C, _ :: unit).
          (C ≠ None) = (Propagated K (the C) ∈ set (get_trail_wl x1a)) ∧
          (C = None) = (Decided K ∈ set (get_trail_wl x1a) ∨
             K ∉ lits_of_l (get_trail_wl x1a)) ∧
         (∀C1. (Propagated K C1 ∈ set (get_trail_wl x1a) ⟶ C1 = the C))}› for K :: ‹nat literal› and x1a
  have get_the_propagation_reason:
    ‹get_the_propagation_reason_pol (get_trail_wl_heur x2b) L
        ≤ SPEC (λD. (D, ()) ∈ reason_rel K x1a)›
  if
    ‹(x, y) ∈ twl_st_heur_restart_ana' r u› and
    ‹mark_to_delete_clauses_wl_pre y› and
    ‹mark_to_delete_clauses_wl_D_heur_pre x› and
    ‹(S, Sa) ∈ ?sort x y› and
    ‹(ys, xs) ∈ ?indices S Sa› and
    ‹(l, la) ∈ nat_rel› and
    ‹la ∈ {_. True}› and
    xa_x': ‹(xa, x') ∈ ?R S› and
    ‹case xa of (i, S) ⇒ i < length (get_tvdom S)› and
    ‹case x' of (i, T, xs) ⇒ i < length xs› and
    ‹x1b < length (get_tvdom x2b)› and
    ‹access_tvdom_at_pre x2b x1b› and
    dom: ‹(b, ba)
       ∈ {(b, b').
          (b, b') ∈ bool_rel ∧
          b = (x2a ! x1 ∈# dom_m (get_clauses_wl x1a))}›
      ‹¬ ¬ b›
      ‹¬ ¬ ba› and
    ‹0 < length (get_clauses_wl x1a ∝ (x2a ! x1))› and
    ‹access_lit_in_clauses_heur_pre ((x2b, get_tvdom x2b ! x1b), 0)› and
    st:
      ‹x2 = (x1a, x2a)›
      ‹x' = (x1, x2)›
      ‹xa = (x1b, x2b)› and
    L: ‹get_clauses_wl x1a ∝ (x2a ! x1) ! 0 ∈# ℒall (all_init_atms_st x1a)› and
    L': ‹(L, K)
    ∈ {(L, L').
       (L, L') ∈ nat_lit_lit_rel ∧
       L' = get_clauses_wl x1a ∝ (x2a ! x1) ! 0}›
    for x y S Sa xs' xs l la xa x' x1 x2 x1a x2a x1' x2' x3 x1b ys x2b L K b ba
  proof -
    have L: ‹arena_lit (get_clauses_wl_heur x2b) (x2a ! x1) ∈# ℒall (all_init_atms_st x1a)›
      using L that by (auto dest!: twl_st_heur_restart(2) simp: st arena_lifting dest: twl_st_heur_restart_anaD)

    show ?thesis
      apply (rule order.trans)
      apply (rule get_the_propagation_reason_pol[THEN fref_to_Down_curry,
        of ‹all_init_atms_st x1a› ‹get_trail_wl x1a›
	  ‹arena_lit (get_clauses_wl_heur x2b) (get_tvdom x2b ! x1b + 0)›])
      subgoal
        using xa_x' L L' by (auto simp add: twl_st_heur_restart_def st)
      subgoal
        using xa_x' L' dom by (auto simp add: twl_st_heur_restart_ana_def twl_st_heur_restart_def st arena_lifting
          all_init_atms_st_def get_unit_init_clss_wl_alt_def)
      using that unfolding get_the_propagation_reason_def reason_rel_def apply -
      by (auto simp: twl_st_heur_restart lits_of_def get_the_propagation_reason_def
          conc_fun_RES
        dest!: twl_st_heur_restart_anaD dest: twl_st_heur_restart(2)  twl_st_heur_restart_same_annotD imageI[of _ _ lit_of])
  qed

  have already_deleted:
    ‹((x1b,  delete_index_vdom_heur x1b x2b), x1, x1a, delete_index_and_swap x2a x1) ∈ ?R S›
    if
      ‹(x, y) ∈ twl_st_heur_restart_ana' r u› and
      ‹mark_to_delete_clauses_wl_D_heur_pre x› and
      ‹(S, Sa) ∈ ?sort x y› and
      ‹(l, la) ∈ nat_rel› and
      ‹la ∈ {_. True}› and
      xx: ‹(xa, x') ∈ ?R S› and
      nempty: ‹case xa of (i, S) ⇒ i < length (get_tvdom S)› and
      ‹case x' of (i, T, xs) ⇒ i < length xs› and
      st:
      ‹x2 = (x1a, x2a)›
      ‹x' = (x1, x2)›
      ‹xa = (x1b, x2b)› and
      le: ‹x1b < length (get_tvdom x2b)› and
      ‹access_tvdom_at_pre x2b x1b› and
      ba: ‹(b, ba) ∈ {(b, b'). (b, b') ∈ bool_rel ∧ b = (x2a ! x1 ∈# dom_m (get_clauses_wl x1a))}›
        ‹¬ba›
    for x y S xs l la xa x' xz x1 x2 x1a x2a x2b x2c x2d ys x1b Sa ba b
  proof -
    show ?thesis
      using xx nempty le ba unfolding st
      by (cases ‹get_tvdom x2b› rule: rev_cases)
       (auto 4 3 simp: twl_st_heur_restart_ana_def delete_index_vdom_heur_def
          twl_st_heur_restart_def mark_garbage_heur_def mark_garbage_wl_def
          learned_clss_l_l_fmdrop size_remove1_mset_If learned_clss_count_def
          aivdom_inv_removed_inactive
        intro: valid_arena_extra_information_mark_to_delete'
        intro!: aivdom_inv_dec_removed_inactive_tvdom
        dest!: in_set_butlastD in_vdom_m_fmdropD
        elim!: in_set_upd_cases)
  qed

  have mop_clause_not_marked_to_delete_heur:
    ‹mop_clause_not_marked_to_delete_heur x2b (get_tvdom x2b ! x1b)
        ≤ SPEC
           (λc. (c, x2a ! x1 ∈# dom_m (get_clauses_wl x1a))
                ∈ {(b, b'). (b,b') ∈ bool_rel ∧ (b ⟷ x2a ! x1 ∈# dom_m (get_clauses_wl x1a))})›
    if
      ‹(xa, x') ∈ ?R S› and
      ‹case xa of (i, S) ⇒ i < length (get_tvdom S)› and
      ‹case x' of (i, T, xs) ⇒ i < length xs› and
      ‹mark_to_delete_clauses_wl_inv Sa xs x'› and
      ‹x2 = (x1a, x2a)› and
      ‹x' = (x1, x2)› and
      ‹xa = (x1b, x2b)› and
      ‹clause_not_marked_to_delete_heur_pre (x2b, get_tvdom x2b ! x1b)›
    for x y S Sa uu xs l la xa x' x1 x2 x1a x2a x1b x2b
    unfolding mop_clause_not_marked_to_delete_heur_def
    apply refine_vcg
    subgoal
      using that by blast
    subgoal
      using that by (auto simp: twl_st_heur_restart arena_lifting dest: twl_st_heur_restart(2) dest!: twl_st_heur_restart_anaD)
    done

  have mop_access_lit_in_clauses_heur:
    ‹mop_access_lit_in_clauses_heur x2b (get_tvdom x2b ! x1b) 0
        ≤ SPEC
           (λc. (c, get_clauses_wl x1a ∝ (x2a ! x1) ! 0)
                ∈ {(L, L'). (L, L') ∈ nat_lit_lit_rel ∧ L' = get_clauses_wl x1a ∝ (x2a ! x1) ! 0})›
    if
      ‹(x, y) ∈ twl_st_heur_restart_ana' r u› and
      ‹mark_to_delete_clauses_wl_pre y› and
      ‹mark_to_delete_clauses_wl_D_heur_pre x› and
      ‹(S, Sa) ∈ ?sort x y› and
      ‹(uu, xs) ∈ ?indices S Sa› and
      ‹(l, la) ∈ nat_rel› and
      ‹la ∈ {uu. True}› and
      ‹length (get_tvdom S) ≤ length (get_clauses_wl_heur x)› and
      ‹(xa, x') ∈ ?R S› and
      ‹case xa of (i, S) ⇒ i < length (get_tvdom S)› and
      ‹case x' of (i, T, xs) ⇒ i < length xs› and
      ‹mark_to_delete_clauses_wl_inv Sa xs x'› and
      ‹x2 = (x1a, x2a)› and
      ‹x' = (x1, x2)› and
      ‹xa = (x1b, x2b)› and
      ‹x1b < length (get_tvdom x2b)› and
      ‹access_tvdom_at_pre x2b x1b› and
      ‹clause_not_marked_to_delete_heur_pre (x2b, get_tvdom x2b ! x1b)› and
      ‹(b, ba)
       ∈ {(b, b').
          (b, b') ∈ bool_rel ∧
          b = (x2a ! x1 ∈# dom_m (get_clauses_wl x1a))}› and
      ‹¬ ¬ b› and
      ‹¬ ¬ ba› and
      ‹0 < length (get_clauses_wl x1a ∝ (x2a ! x1))› and
      ‹get_clauses_wl x1a ∝ (x2a ! x1) ! 0
       ∈# ℒall (all_init_atms_st x1a)› and
      pre: ‹access_lit_in_clauses_heur_pre ((x2b, get_tvdom x2b ! x1b), 0)›
     for x y S Sa uu xs l la xa x' x1 x2 x1a x2a x1b x2b b ba
  unfolding mop_access_lit_in_clauses_heur_def mop_arena_lit2_def
  apply refine_vcg
  subgoal using pre unfolding access_lit_in_clauses_heur_pre_def by simp
  subgoal using that by (auto dest!: twl_st_heur_restart_anaD twl_st_heur_restart_valid_arena simp: arena_lifting)
  done

  have incr_restart_stat: ‹incr_reduction_stat (set_stats_size_limit_st lbd sze T)
    ≤ ⇓ (twl_st_heur_restart_ana' r u) (remove_all_learned_subsumed_clauses_wl S)›
    if ‹(T, S) ∈ twl_st_heur_restart_ana' r u› for S T i u  lbd sze
    using that
    by (cases S; cases T)
      (auto simp: conc_fun_RES incr_restart_stat_def learned_clss_count_def set_stats_size_limit_st_def
        twl_st_heur_restart_ana_def twl_st_heur_restart_def
      remove_all_learned_subsumed_clauses_wl_def clss_size_corr_def incr_reduction_stat_def
      clss_size_lcountUE_def clss_size_lcountUS_def clss_size_def
      clss_size_resetUS_def clss_size_lcount_def clss_size_lcountU0_def 
        RES_RETURN_RES)

  have only_irred: ‹¬ irred (get_clauses_wl x1a) (x2a ! x1)› (is ?A) and
    get_learned_count_ge: ‹Suc 0 ≤ clss_size_lcount (get_learned_count x2b)› (is ?B)
    if
      ‹(x, y) ∈ twl_st_heur_restart_ana' r u› and
      ‹mark_to_delete_clauses_wl_pre y› and
      ‹mark_to_delete_clauses_wl_D_heur_pre x› and
      ‹(S, Sa) ∈ ?sort x y› and
      indices: ‹(uu, xs) ∈ ?indices S Sa› and
      ‹(l, la) ∈ nat_rel› and
      ‹la ∈ {_. True}› and
      ‹length (get_tvdom S) ≤ length (get_clauses_wl_heur x)› and
      xx: ‹(xa, x') ∈ ?R S› and
      ‹case xa of (i, S) ⇒ i < length (get_tvdom S)› and
      ‹case x' of (i, T, xs) ⇒ i < length xs› and
      ‹mark_to_delete_clauses_wl_inv Sa xs x'› and
      st: ‹x2 = (x1a, x2a)› ‹x' = (x1, x2)› ‹xa = (x1b, x2b)› and
      ‹x1b < length (get_tvdom x2b)› and
      ‹access_tvdom_at_pre x2b x1b› and
      ‹clause_not_marked_to_delete_heur_pre (x2b, get_tvdom x2b ! x1b)› and
      dom: ‹(b, ba) ∈ {(b, b'). (b, b') ∈ bool_rel ∧ b = (x2a ! x1 ∈# dom_m (get_clauses_wl x1a))}›
        ‹¬ ¬ b›
        ‹¬ ¬ ba› and
      ‹0 < length (get_clauses_wl x1a ∝ (x2a ! x1))› and
      ‹get_clauses_wl x1a ∝ (x2a ! x1) ! 0 ∈# ℒall (all_init_atms_st x1a)› and
      ‹access_lit_in_clauses_heur_pre ((x2b, get_tvdom x2b ! x1b), 0)› and
      ‹length (get_clauses_wl_heur x2b) ≤ length (get_clauses_wl_heur x)› and
      ‹length (get_tvdom x2b) ≤ length (get_clauses_wl_heur x2b)› and
      ‹(L, K) ∈ {(L, L'). (L, L') ∈ nat_lit_lit_rel ∧ L' = get_clauses_wl x1a ∝ (x2a ! x1) ! 0}› and
      ‹(D, bb) ∈ reason_rel K x1a› and
      ‹arena_is_valid_clause_idx (get_clauses_wl_heur x2b) (get_tvdom x2b ! x1b)› and
      ‹D ≠ Some (get_tvdom x2b ! x1b) ∧ arena_length (get_clauses_wl_heur x2b) (get_tvdom x2b ! x1b) ≠ 2›
      for x y S Sa uu xs l la xa x' x1 x2 x1a x2a x1b x2b b ba L K D bb
    proof -
      have ‹get_tvdom x2b ! x1 ∈ set (get_tvdom x2b)› and
        x: ‹(x2b, x1a) ∈ twl_st_heur_restart_ana r›
      using that by (auto dest: simp: arena_lifting twl_st_heur_restart)
    then show ?A
      using indices xx
      by (auto dest: twl_st_heur_restart_anaD twl_st_heur_restart_valid_arena
        simp: arena_lifting twl_st_heur_restart st)
    then show ?B
      using dom x by (auto simp: twl_st_heur_restart_ana_def twl_st_heur_restart_def ran_m_def
        dest!: multi_member_split
        dest!: clss_size_corr_restart_rew)
  qed
  have length_filter_le: ‹((x1b, mark_garbage_heur3 (get_tvdom x2b ! x1b) x1b (incr_wasted_st (word_of_nat wasted) x2b)), x1,
  mark_garbage_wl (x2a ! x1) x1a, delete_index_and_swap x2a x1)
    ∈ ?R S›
    if H:
      ‹(x, y) ∈ twl_st_heur_restart_ana' r u›
      ‹mark_to_delete_clauses_wl_pre y›
      ‹mark_to_delete_clauses_wl_D_heur_pre x›
      ‹(S, Sa) ∈ ?sort x y›
      ‹(uu, xs) ∈ ?indices S Sa›
      ‹(l, la) ∈ nat_rel›
      ‹la ∈ {_. True}›
      ‹length (get_tvdom S) ≤ length (get_clauses_wl_heur x)›
      ‹(xa, x') ∈ ?R S›
      ‹case xa of (i, S) ⇒ i < length (get_tvdom S)›
      ‹case x' of (i, T, xs) ⇒ i < length xs›
      ‹mark_to_delete_clauses_wl_inv Sa xs x'›
      ‹x2 = (x1a, x2a)›
      ‹x' = (x1, x2)›
      ‹xa = (x1b, x2b)›
      ‹x1b < length (get_tvdom x2b)›
      ‹access_tvdom_at_pre x2b x1b›
      ‹clause_not_marked_to_delete_heur_pre (x2b, get_tvdom x2b ! x1b)›
      ‹(b, ba) ∈ {(b, b'). (b, b') ∈ bool_rel ∧ b = (x2a ! x1 ∈# dom_m (get_clauses_wl x1a))}›
      ‹¬ ¬ b›
      ‹¬ ¬ ba›
      ‹0 < length (get_clauses_wl x1a ∝ (x2a ! x1))›
      ‹get_clauses_wl x1a ∝ (x2a ! x1) ! 0 ∈# ℒall (all_init_atms_st x1a)›
      ‹access_lit_in_clauses_heur_pre ((x2b, get_tvdom x2b ! x1b), 0)›
      ‹length (get_clauses_wl_heur x2b) ≤ length (get_clauses_wl_heur x)›
      ‹length (get_tvdom x2b) ≤ length (get_clauses_wl_heur x2b)›
      ‹(L, K) ∈ {(L, L'). (L, L') ∈ nat_lit_lit_rel ∧ L' = get_clauses_wl x1a ∝ (x2a ! x1) ! 0}›
      ‹(D, bb) ∈ reason_rel K x1a›
      ‹arena_is_valid_clause_idx (get_clauses_wl_heur x2b) (get_tvdom x2b ! x1b)›
      ‹(D ≠ Some (get_tvdom x2b ! x1b) ∧ arena_length (get_clauses_wl_heur x2b) (get_tvdom x2b ! x1b) ≠ 2, can_del)
    ∈ bool_rel›
      ‹x1 < length x2a›
      ‹D ≠ Some (get_tvdom x2b ! x1b) ∧ arena_length (get_clauses_wl_heur x2b) (get_tvdom x2b ! x1b) ≠ 2›
      can_del
    for x y S Sa xs l la xa x' x1 x2 x1a x2a x1b x2b b ba can_del D L K bb uu wasted
  proof -
      have [simp]: ‹mark_garbage_heur3 i C (incr_wasted_st b S) = incr_wasted_st b (mark_garbage_heur3 i C S)› for i C S b
        by (cases S; auto simp: mark_garbage_heur3_def incr_wasted_st_def)
      have ‹mark_garbage_pre (get_clauses_wl_heur x2b, get_tvdom x2b ! x1b)›
        ‹x1b < length (get_tvdom x2b)›
        using that
        unfolding prod.simps mark_garbage_pre_def
          arena_is_valid_clause_vdom_def arena_is_valid_clause_idx_def apply -
        by (rule exI[of _ ‹get_clauses_wl x1a›], rule exI[of _ ‹set (get_vdom x2b)›])
         (auto simp: twl_st_heur_restart twl_st_heur_restart_ana_def dest: twl_st_heur_restart_valid_arena)
      moreover have 0: ‹Suc 0 ≤ clss_size_lcount (get_learned_count x2b)›
         ‹¬ irred (get_clauses_wl x1a) (x2a ! x1)› 
        using get_learned_count_ge[OF that(1-29,32)] only_irred[OF that(1-29,32)] by auto
      moreover have ‹(mark_garbage_heur3 (get_tvdom x2b ! x1) x1
        (incr_wasted_st (word_of_nat wasted) x2b),
        mark_garbage_wl (get_tvdom x2b ! x1) x1a)
        ∈ twl_st_heur_restart_ana r›
        by (use that 0 in
          ‹auto intro!: incr_wasted_st mark_garbage_heur_wl_ana simp: twl_st_heur_restart
          learned_clss_count_mark_garbage_heur3
          dest: twl_st_heur_restart_valid_arena twl_st_heur_restart_anaD›)
      moreover have ‹learned_clss_count
        (mark_garbage_heur3 (get_tvdom x2b ! x1) x1
        (incr_wasted_st (word_of_nat wasted) x2b))
        ≤ u›
        by (use that 0 in
          ‹auto intro!: incr_wasted_st mark_garbage_heur_wl_ana simp: twl_st_heur_restart
          learned_clss_count_mark_garbage_heur3
          dest: twl_st_heur_restart_valid_arena twl_st_heur_restart_anaD›)
      moreover have ‹xb ∈ set (get_tvdom S)›
        if ‹xb ∈ set (butlast ((get_tvdom x2b)[x1 := last (get_tvdom x2b)]))› for xb
      proof -
        have ‹xb ∈ set (get_tvdom x2b)›
          using that H by (auto dest!: in_set_butlastD)
            (metis Misc.last_in_set in_set_upd_eq len_greater_imp_nonempty)
        then show ?thesis
          using H by auto
      qed
      moreover have K: ‹¬irred (get_clauses_wl (mark_garbage_wl (get_tvdom x2b ! x1) x1a)) C›  ‹C ≠ get_tvdom x2b ! x1›
        if ‹C ∈ set (butlast ((get_tvdom x2b)[x1 := last (get_tvdom x2b)]))› for C
      proof -
        have a: ‹distinct (get_tvdom x2b)› ‹x1 < length (get_tvdom x2b)›
          using  H(9-15) by (auto simp: twl_st_heur_restart_ana_def
            twl_st_heur_restart_def aivdom_inv_dec_alt_def)
        then have 1: ‹get_tvdom x2b = take x1 (get_tvdom x2b) @ get_tvdom x2b ! x1 # drop (Suc x1) (get_tvdom x2b)›
          by (subst append_take_drop_id[of x1, symmetric], subst Cons_nth_drop_Suc[symmetric])
           auto
        have ‹set (delete_index_and_swap (get_tvdom x2b) x1) =
          set (get_tvdom x2b) - {get_tvdom x2b!x1}›
          using a
          apply (subst (asm) (2)1, subst (asm) (1)1)
          apply (subst (2)1, subst (1)1)
          apply (cases ‹drop (Suc x1) (get_tvdom x2b)› rule: rev_cases)
          by (auto simp: nth_append list_update_append1 list_update_append2 butlast_append
            dest: in_set_butlastD)
        then show [simp]: ‹C ≠ get_tvdom x2b ! x1›
          using that by auto
        show  ‹¬irred (get_clauses_wl (mark_garbage_wl (get_tvdom x2b ! x1) x1a)) C›
          using that H
          apply (cases x1a)
          apply (auto simp: mark_garbage_wl_def)
          by (metis Misc.last_in_set in_set_butlastD in_set_upd_cases len_greater_imp_nonempty)
      qed
      moreover have ‹length (get_clauses_wl (mark_garbage_wl (get_tvdom x2b ! x1) x1a) ∝ C) ≠ 2›
        if ‹C ∈ set (butlast ((get_tvdom x2b)[x1 := last (get_tvdom x2b)]))› for C
      proof -
        have ‹C ∈ set (get_tvdom x2b)› ‹C ≠ get_tvdom x2b ! x1›
          using K(2)[OF that] that
          apply (auto simp: mark_garbage_wl_def)
          using in_set_delete_index_and_swapD by fastforce
        then show ?thesis
          using H
          by (cases x1a)
           (auto simp: mark_garbage_wl_def)
      qed
      ultimately show ?thesis
        using that supply [[goals_limit=1]]
        by (auto intro!: )
  qed
  have mop_arena_length_st: ‹mop_arena_length_st x2b (get_tvdom x2b ! x1b)
    ≤ SPEC
    (λc. (c, length (get_clauses_wl x1a ∝ (x2a ! x1))) ∈ nat_rel)› 
    if H:
      ‹(x, y) ∈ twl_st_heur_restart_ana' r u›
      ‹mark_to_delete_clauses_wl_pre y›
      ‹mark_to_delete_clauses_wl_D_heur_pre x›
      ‹(S, Sa) ∈ ?sort x y›
      ‹(uu, xs) ∈ ?indices S Sa›
      ‹(l, la) ∈ nat_rel›
      ‹la ∈ {_. True}›
      ‹length (get_tvdom S) ≤ length (get_clauses_wl_heur x)›
      ‹(xa, x') ∈ ?R S›
      ‹case xa of (i, S) ⇒ i < length (get_tvdom S)›
      ‹case x' of (i, T, xs) ⇒ i < length xs›
      ‹mark_to_delete_clauses_wl_inv Sa xs x'›
      ‹x2 = (x1a, x2a)›
      ‹x' = (x1, x2)›
      ‹xa = (x1b, x2b)›
      ‹x1b < length (get_tvdom x2b)›
      ‹access_tvdom_at_pre x2b x1b›
      ‹clause_not_marked_to_delete_heur_pre (x2b, get_tvdom x2b ! x1b)›
      ‹(b, ba) ∈ {(b, b'). (b, b') ∈ bool_rel ∧ b = (x2a ! x1 ∈# dom_m (get_clauses_wl x1a))}›
      ‹¬ ¬ b›
      ‹¬ ¬ ba›
      ‹0 < length (get_clauses_wl x1a ∝ (x2a ! x1))›
      ‹get_clauses_wl x1a ∝ (x2a ! x1) ! 0 ∈# ℒall (all_init_atms_st x1a)›
      ‹access_lit_in_clauses_heur_pre ((x2b, get_tvdom x2b ! x1b), 0)›
      ‹length (get_clauses_wl_heur x2b) ≤ length (get_clauses_wl_heur x)›
      ‹length (get_tvdom x2b) ≤ length (get_clauses_wl_heur x2b)›
      ‹(L, K) ∈ {(L, L'). (L, L') ∈ nat_lit_lit_rel ∧ L' = get_clauses_wl x1a ∝ (x2a ! x1) ! 0}›
      ‹(D, bb) ∈ reason_rel K x1a›
      ‹arena_is_valid_clause_idx (get_clauses_wl_heur x2b) (get_tvdom x2b ! x1b)›
      ‹(D ≠ Some (get_tvdom x2b ! x1b) ∧ arena_length (get_clauses_wl_heur x2b) (get_tvdom x2b ! x1b) ≠ 2, can_del)
    ∈ bool_rel›
      ‹x1 < length x2a›
      ‹D ≠ Some (get_tvdom x2b ! x1b) ∧ arena_length (get_clauses_wl_heur x2b) (get_tvdom x2b ! x1b) ≠ 2›
      can_del
    for x y S Sa xs l la xa x' x1 x2 x1a x2a x1b x2b b ba can_del D L K bb uu
    unfolding mop_arena_length_st_def
    apply (rule mop_arena_length[THEN fref_to_Down_curry, THEN order_trans,
      of ‹get_clauses_wl x1a› ‹get_tvdom x2b ! x1b› _ _ ‹set (get_vdom x2b)›])
    using that by (auto simp: twl_st_heur_restart_ana_def twl_st_heur_restart_def)
  show ?thesis
    supply sort_vdom_heur_def[simp] twl_st_heur_restart_anaD[dest] [[goals_limit=1]]
    unfolding mark_to_delete_clauses_wl_D_heur_alt_def mark_to_delete_clauses_wl_D_alt_def
      access_lit_in_clauses_heur_def
    apply (intro frefI nres_relI)
    apply (refine_vcg sort_vdom_heur_reorder_vdom_wl[THEN fref_to_Down] incr_restart_stat find_largest_lbd_and_size)
    subgoal
      unfolding mark_to_delete_clauses_wl_D_heur_pre_def by fast
    apply assumption
    subgoal by auto
    subgoal for x y S T unfolding number_clss_to_keep_def by (cases S) (auto)
    apply (solves auto)
    subgoal by (auto simp: twl_st_heur_restart_ana_def twl_st_heur_restart_def aivdom_inv_dec_alt_def
       dest!: valid_arena_vdom_subset size_mset_mono)
    apply (rule init; solves auto)
    subgoal by auto
    subgoal by auto
    subgoal by (auto simp: access_tvdom_at_pre_def)
    subgoal for x y S Sa u xs l la _ _ x1 x2 xb x' x1c x2c x1a x2a x1b x2b
      unfolding clause_not_marked_to_delete_heur_pre_def arena_is_valid_clause_vdom_def
        prod.simps
      by (rule exI[of _ ‹get_clauses_wl (fst x2c)›], rule exI[of _ ‹set (get_vdom x2b)›])
         (auto simp: twl_st_heur_restart
        intro!: twl_st_heur_restart_valid_arena[simplified]
        dest: twl_st_heur_restart_get_tvdom_nth_get_vdom[simplified])
    apply (rule mop_clause_not_marked_to_delete_heur; assumption)
    subgoal for x y S Sa uu xs l la xa x' x1 x2 x1a x2a x1b x2b
      by (auto simp: twl_st_heur_restart)
    subgoal
      by (rule already_deleted)
    subgoal for x y S Sa u xs l la _ _ x1 x2 xb x' x1c x2c x1a x2a x1b x2b
      unfolding access_lit_in_clauses_heur_pre_def prod.simps arena_lit_pre_def
        arena_is_valid_clause_idx_and_access_def
      by (rule bex_leI[of _ ‹get_tvdom x2b ! x1b›], simp add: aivdom_inv_dec_alt_def,
        rule exI[of _ ‹get_clauses_wl (fst x2c)›])
        (auto simp: twl_st_heur_restart_ana_def twl_st_heur_restart_def aivdom_inv_dec_alt_def)
    subgoal by (auto simp: twl_st_heur_restart_ana_def twl_st_heur_restart_def dest!: valid_arena_vdom_subset size_mset_mono)
    subgoal premises p using p(7-)
      by (auto simp: twl_st_heur_restart_ana_def twl_st_heur_restart_def aivdom_inv_dec_alt_def
        dest!: valid_arena_vdom_subset size_mset_mono)
      apply (rule mop_access_lit_in_clauses_heur; assumption)
      apply (rule get_the_propagation_reason; assumption)
    subgoal for x y S Sa u xs l la _ _ x1 x2 xb x' x1c x2c x1a x2a x1b x2b
      unfolding prod.simps
        arena_is_valid_clause_vdom_def arena_is_valid_clause_idx_def
      by (rule exI[of _ ‹get_clauses_wl (fst x2c)›], rule exI[of _ ‹set (get_vdom x2b)›])
        (auto simp: twl_st_heur_restart dest:twl_st_heur_restart_get_avdom_nth_get_vdom
        intro!: twl_st_heur_restart_valid_arena[simplified])
    subgoal
      unfolding marked_as_used_pre_def
      by (auto simp: twl_st_heur_restart reason_rel_def)
    subgoal for x y S Sa uu xs l la xa x' x1 x2 x1a x2a x1b x2b b ba L K D bb
      by (rule only_irred)
    subgoal
      by (auto dest!: twl_st_heur_restart_anaD twl_st_heur_restart_valid_arena simp: arena_lifting)
    subgoal by fast
    apply (rule mop_arena_length_st; assumption)
    apply (rule log_del_clause_heur_log_clause[where r=r and u=u])
    subgoal by auto
    subgoal by auto
    subgoal by auto
    subgoal for x y S Sa u xs l la _ _ x1 x2 xb x' x1c x2c x1a x2a x1b x2b
      unfolding prod.simps mark_garbage_pre_def
        arena_is_valid_clause_vdom_def arena_is_valid_clause_idx_def apply -
      by (rule exI[of _ ‹get_clauses_wl (fst x2c)›], rule exI[of _ ‹set (get_vdom x2b)›])
       (auto simp: twl_st_heur_restart twl_st_heur_restart_ana_def dest: twl_st_heur_restart_valid_arena)
    subgoal premises that
      using get_learned_count_ge[OF that(2-8,12-15,17-33)] that(32-)
      using only_irred[OF that(2-8,12-15,17-33)]
      by auto
    subgoal for x y S Sa _ xs l la xa x' x1 x2 x1a x2a x1b x2b
      by (rule length_filter_le)
   subgoal for x y
      unfolding valid_sort_clause_score_pre_def arena_is_valid_clause_vdom_def
        get_clause_LBD_pre_def arena_is_valid_clause_idx_def arena_act_pre_def
      by (force simp: valid_sort_clause_score_pre_def twl_st_heur_restart_ana_def arena_dom_status_iff
        arena_act_pre_def get_clause_LBD_pre_def arena_is_valid_clause_idx_def twl_st_heur_restart_def
         intro!: exI[of _ ‹get_clauses_wl T›] dest!: set_mset_mono mset_subset_eqD)
    subgoal for x y S Sa uu xs l la xa x' x1 x2 x1a x2a x1c x2c b ba L x2b
      using size_mset_mono[of ‹mset (get_tvdom x2b)› ‹mset (get_vdom x2b)›]
      by (clarsimp simp: twl_st_heur_restart_ana_def twl_st_heur_restart_def aivdom_inv_dec_alt_def
        dest!: valid_arena_vdom_subset)
    subgoal
      by auto
    done
qed

lemma cdcl_twl_mark_clauses_to_delete_alt_def:
  ‹cdcl_twl_mark_clauses_to_delete S = do {
  _ ← ASSERT (mark_to_delete_clauses_wl_D_heur_pre S);
  T ← mark_to_delete_clauses_wl_D_heur S;
  RETURN (schedule_next_reduction_st (clss_size_resetUS0_st T))
  }›
  unfolding cdcl_twl_mark_clauses_to_delete_def IsaSAT_Profile.start_def IsaSAT_Profile.stop_def
  by auto

lemma learned_clss_count_clss_size_resetUS0_st_le:
  ‹learned_clss_count (clss_size_resetUS0_st T) ≤ learned_clss_count T› and
  clss_size_resetUS0_st_simp[simp]:
  ‹get_clauses_wl_heur (clss_size_resetUS0_st T) = get_clauses_wl_heur T›
  by (cases T;clarsimp simp: clss_size_resetUS0_st_def learned_clss_count_def
    clss_size_lcountUS_def clss_size_lcountU0_def clss_size_lcountUE_def
    clss_size_resetUS_def clss_size_resetU0_def clss_size_resetUE_def clss_size_lcountUEk_def
    clss_size_lcount_def
    split: prod.splits)+

lemma learned_clss_count_schedule_next_reduction_st_le:
  ‹learned_clss_count (schedule_next_reduction_st T) = learned_clss_count T› and
  schedule_next_reduction_st_simp[simp]:
  ‹get_clauses_wl_heur (schedule_next_reduction_st T) = get_clauses_wl_heur T›
  by (solves ‹cases T;clarsimp simp: schedule_next_reduction_st_def learned_clss_count_def Let_def
     schedule_next_reduce_st_def›)+

lemma schedule_next_reduction_sttwl_st_heur:
   ‹(S,T)∈twl_st_heur ⟹ (schedule_next_reduction_st S, T) ∈ twl_st_heur›
  by (auto simp: twl_st_heur_def schedule_next_reduction_st_def Let_def
    schedule_next_reduce_st_def)

lemma cdcl_twl_mark_clauses_to_delete_cdcl_twl_full_restart_wl_prog_D:
  ‹(cdcl_twl_mark_clauses_to_delete, cdcl_twl_full_restart_wl_prog) ∈
     twl_st_heur''''u r u →f ⟨twl_st_heur''''u r u⟩nres_rel›
  unfolding cdcl_twl_mark_clauses_to_delete_alt_def cdcl_twl_full_restart_wl_prog_def
  apply (intro frefI nres_relI)
  apply (refine_vcg
    mark_to_delete_clauses_wl_D_heur_mark_to_delete_clauses_wl_D[THEN fref_to_Down])
  subgoal
    by (rule mark_to_delete_clauses_wl_D_heur_pre_alt_def) fast
  apply (rule twl_st_heur_restartD2)
  subgoal
    by (rule mark_to_delete_clauses_wl_D_heur_pre_twl_st_heur) auto
  subgoal for x y T Ta
    using learned_clss_count_clss_size_resetUS0_st_le[of T]
      learned_clss_count_schedule_next_reduction_st_le[of ‹clss_size_resetUS0_st T›]
    by (auto simp: mark_to_delete_clauses_wl_post_twl_st_heur twl_st_heur_restart_anaD
        schedule_next_reduction_sttwl_st_heur)
     (auto simp: twl_st_heur_restart_ana_def)
  done

lemma cdcl_twl_restart_wl_heur_cdcl_twl_restart_wl_D_prog:
  ‹(cdcl_twl_restart_wl_heur, cdcl_twl_restart_wl_prog) ∈
    twl_st_heur''''u r u →f ⟨twl_st_heur''''u r u⟩nres_rel›
  unfolding cdcl_twl_restart_wl_prog_def cdcl_twl_restart_wl_heur_def
  by (intro frefI nres_relI)
    (refine_rcg lhs_step_If
    cdcl_twl_local_restart_wl_D_heur_cdcl_twl_local_restart_wl_D_spec[THEN fref_to_Down]
    cdcl_twl_mark_clauses_to_delete_cdcl_twl_full_restart_wl_prog_D[THEN fref_to_Down])

lemma mark_to_delete_clauses_wl_D_heur_mark_to_delete_clauses_GC_wl_D:
  ‹(mark_to_delete_clauses_GC_wl_D_heur, mark_to_delete_clauses_GC_wl) ∈
     twl_st_heur_restart_ana' r u →f
      ⟨twl_st_heur_restart_ana' r u⟩nres_rel›
proof -
  have H: ‹mark_to_delete_clauses_GC_wl_pre S ∧ mark_to_delete_clauses_wl_pre S ⟷
    mark_to_delete_clauses_GC_wl_pre S› for S
   unfolding mark_to_delete_clauses_GC_wl_pre_def mark_to_delete_clauses_wl_pre_def
   mark_to_delete_clauses_l_GC_pre_def mark_to_delete_clauses_l_pre_def
   by blast
  have mark_to_delete_clauses_GC_wl_D_alt_def:
    ‹mark_to_delete_clauses_GC_wl  = (λS0. do {
      ASSERT(mark_to_delete_clauses_GC_wl_pre S0);
      S ← reorder_vdom_wl S0;
      xs ← collect_valid_indices_wl S;
      l ← SPEC (λ_::nat. True);
      _ ← SPEC (λ_::nat×nat. True);
      (_, S, _) ← WHILET⇗mark_to_delete_clauses_GC_wl_inv S xs⇖
        (λ(i, T, xs). i < length xs)
        (λ(i, T, xs). do {
          b ← RETURN (xs!i ∈# dom_m (get_clauses_wl T));
          if ¬b then RETURN (i, T, delete_index_and_swap xs i)
          else do {
            ASSERT(0 < length (get_clauses_wl T∝(xs!i)));
	    ASSERT (get_clauses_wl T ∝ (xs ! i) ! 0 ∈# ℒall (all_init_atms_st T));
            can_del ← SPEC(λb. b ⟶
              (¬irred (get_clauses_wl T) (xs!i) ∧ length (get_clauses_wl T ∝ (xs!i)) ≠ 2));
            ASSERT(i < length xs);
            if can_del
            then
              RETURN (i, mark_garbage_wl (xs!i) T, delete_index_and_swap xs i)
            else
              RETURN (i+1, T, xs)
          }
        })
        (l, S, xs);
      remove_all_learned_subsumed_clauses_wl S
    })›
   unfolding mark_to_delete_clauses_GC_wl_def reorder_vdom_wl_def bind_to_let_conv Let_def
     nres_monad3 summarize_ASSERT_conv H
   by (auto intro!: ext bind_cong[OF refl])


  have mono: ‹g = g' ⟹ do {f; g} = do {f; g'}›
     ‹(⋀x. h x = h' x) ⟹ do {x ← f; h x} = do {x ← f; h' x}› for f f' :: ‹_ nres› and g g' and h h'
    by auto
  have mark_to_delete_clauses_wl_pre_same_atms: ‹set_mset (all_atms_st T) = set_mset (all_init_atms_st T)›
    if ‹mark_to_delete_clauses_wl_pre T› for T
    using that unfolding mark_to_delete_clauses_wl_pre_def mark_to_delete_clauses_l_pre_def apply -
    apply normalize_goal+
    by (rule literals_are_ℒin'_literals_are_ℒin_iff(3)[symmetric]) assumption+

  have mark_to_delete_clauses_wl_D_heur_pre_cong:
    ‹aivdom_inv_dec vdom' (dom_m (get_clauses_wl S')) ⟹
    mset (get_vdom_aivdom (get_aivdom T)) = mset (get_vdom_aivdom vdom') ⟹
     (T, S') ∈ twl_st_heur_restart ⟹
    mark_to_delete_clauses_GC_wl_pre S' ⟹
    mark_to_delete_clauses_GC_wl_D_heur_pre T ⟹
    valid_arena N'' (get_clauses_wl S') (set (get_vdom_aivdom (get_aivdom T))) ⟹
    mark_to_delete_clauses_GC_wl_D_heur_pre (set_clauses_wl_heur N'' (set_aivdom_wl_heur vdom' T))›
    for M' N' D' j W' vm clvls cach lbd outl stats fast_ema slow_ema avdom avdom'
      ccount lcount heur old_arena ivdom opts S' vdom' N'' T
    using mset_eq_setD[of ‹get_vdom_aivdom (get_aivdom T)› ‹get_vdom_aivdom vdom'›, symmetric] apply -
    unfolding mark_to_delete_clauses_GC_wl_D_heur_pre_def
    by (rule_tac x=S' in exI)
     (clarsimp simp: twl_st_heur_restart_def dest: mset_eq_setD intro: )

   have mark_to_delete_clauses_wl_pre_same_atms: ‹set_mset (all_atms_st T) = set_mset (all_init_atms_st T)›
    if ‹mark_to_delete_clauses_GC_wl_pre T› for T
    using that unfolding mark_to_delete_clauses_GC_wl_pre_def mark_to_delete_clauses_l_pre_def
      mark_to_delete_clauses_l_GC_pre_def apply -
    apply normalize_goal+
    by (rule literals_are_ℒin'_literals_are_ℒin_iff(3)[symmetric]) assumption+

  have [refine0]:
    ‹sort_vdom_heur S ≤ ⇓ {(U, V). (U, V) ∈ twl_st_heur_restart_ana' r u ∧ V = T ∧
         (mark_to_delete_clauses_GC_wl_pre T ⟶ mark_to_delete_clauses_GC_wl_pre V) ∧
          (mark_to_delete_clauses_GC_wl_D_heur_pre S ⟶ mark_to_delete_clauses_GC_wl_D_heur_pre U) ∧
         (∀C∈set (get_tvdom U). ¬irred (get_clauses_wl V) C)}
         (reorder_vdom_wl T)› (is ‹_ ≤ ⇓?sort _›)
    if ‹(S, T) ∈ twl_st_heur_restart_ana' r u› and ‹mark_to_delete_clauses_GC_wl_pre T› for S T
    supply [simp del] = EQ_def
    using that unfolding reorder_vdom_wl_def sort_vdom_heur_def Let_def
    apply (refine_rcg ASSERT_leI)
    subgoal by (auto simp: twl_st_heur_restart_ana_def twl_st_heur_restart_def aivdom_inv_dec_alt_def
      dest!: valid_arena_vdom_subset size_mset_mono)
    subgoal by (auto simp: twl_st_heur_restart_ana_def twl_st_heur_restart_def aivdom_inv_dec_alt_def
      dest!: valid_arena_vdom_subset size_mset_mono)
      apply (rule specify_left_RES)
      apply (rule_tac  N = ‹get_clauses_wl T› and M' = ‹get_trail_wl T› and
        𝒜 = ‹all_init_atms_st T› and
        NUE = ‹get_unit_clauses_wl T + get_subsumed_clauses_wl T + get_clauses0_wl T› in
     isa_isa_gather_candidates_for_reduction_remove_deleted_clauses_from_avdom2[unfolded conc_fun_RES])
    subgoal
      by (case_tac T; auto simp: twl_st_heur_restart_ana_def twl_st_heur_restart_def mem_Collect_eq prod.case)
    subgoal
      by (case_tac T; auto simp: twl_st_heur_restart_ana_def twl_st_heur_restart_def mem_Collect_eq prod.case)
    subgoal
      by (case_tac T; auto simp: twl_st_heur_restart_ana_def twl_st_heur_restart_def mem_Collect_eq prod.case
        all_init_atms_st_def)
    subgoal
      unfolding all_atms_st_def[symmetric]
      by (rule mark_to_delete_clauses_wl_pre_same_atms)
    apply (subst case_prod_beta)
    apply (intro ASSERT_leI)
    subgoal for arena_aivdom
      unfolding valid_sort_clause_score_pre_def arena_is_valid_clause_vdom_def
        get_clause_LBD_pre_def arena_is_valid_clause_idx_def arena_act_pre_def
      by (auto simp: valid_sort_clause_score_pre_def twl_st_heur_restart_ana_def arena_dom_status_iff(1)[symmetric]
        arena_act_pre_def get_clause_LBD_pre_def arena_is_valid_clause_idx_def twl_st_heur_restart_def aivdom_inv_dec_alt_def
        intro!: exI[of _ ‹get_clauses_wl T›] exI[of _ ‹set (get_vdom S)›]
        dest: set_mset_mono mset_subset_eqD)
    subgoal by (auto simp: EQ_def)
    subgoal
      by (cases T)
       (clarsimp simp add: twl_st_heur_restart_ana_def valid_arena_vdom_subset twl_st_heur_restart_def aivdom_inv_dec_alt_def case_prod_beta split: 
        dest!: size_mset_mono valid_arena_vdom_subset)
    subgoal for arena_aivdom
      apply (rewrite at ‹_ ≤ ⌑› Down_id_eq[symmetric])
      apply (rule bind_refine_spec)
      prefer 2
      apply (rule sort_clauses_by_score_reorder[of _ ‹get_clauses_wl T›])
      subgoal
        by (auto simp: twl_st_heur_restart_ana_def twl_st_heur_restart_def dest: mset_eq_setD)
      subgoal
        by (cases ‹arena_aivdom›; cases ‹get_content (snd arena_aivdom)›)
         (simp add: twl_st_heur_restart_ana_def twl_st_heur_restart_def)
      subgoal
        apply auto
        apply (auto simp: learned_clss_count_def (* twl_st_heur_restart_ana_def twl_st_heur_restart_def *)
          intro: mark_to_delete_clauses_wl_D_heur_pre_cong
          intro: aivdom_inv_cong2
          dest: mset_eq_setD)
          apply (auto 4 3 simp: twl_st_heur_restart_ana_def twl_st_heur_restart_def 
            intro: aivdom_inv_cong2 dest: mset_eq_setD; fail)[]
          apply (rule mark_to_delete_clauses_wl_D_heur_pre_cong)
          apply assumption+
          apply (auto simp: twl_st_heur_restart_ana_def twl_st_heur_restart_def)
          done
          done
        done

  have [refine0]: ‹RETURN (get_tvdom x) ≤ ⇓ {(xs, xs'). xs = xs' ∧ xs = get_tvdom x ∧
       (∀C∈set (get_tvdom x). ¬irred (get_clauses_wl y) C)} (collect_valid_indices_wl y)›
    (is ‹_ ≤ ⇓ ?indices _›)
    if
      ‹(x, y) ∈ ?sort S T› and
      ‹mark_to_delete_clauses_GC_wl_D_heur_pre x›
    for x y S T
  proof -
    show ?thesis using that by (auto simp: collect_valid_indices_wl_def simp: RETURN_RES_refine_iff)
  qed

  have init:
    ‹(u', xs) ∈ ?indices S Sa ⟹
    (l, la) ∈ nat_rel ⟹
    (S, Sa) ∈ twl_st_heur_restart_ana' r u ⟹
    ((l, S), la, Sa, xs) ∈  nat_rel ×f
    {(Sa', (T, xs)). (Sa', T) ∈ twl_st_heur_restart_ana' r u ∧ xs = get_tvdom Sa' ∧
    set (get_tvdom Sa') ⊆ set (get_tvdom S) ∧ (∀C∈set (get_tvdom Sa'). ¬irred (get_clauses_wl T) C)}›
    (is ‹_ ⟹ _ ⟹ _ ⟹ _ ∈ ?R›)
       for x y S Sa xs l la u'
    by auto

  define reason_rel where
    ‹reason_rel K x1a ≡ {(C, _ :: unit).
          (C ≠ None) = (Propagated K (the C) ∈ set (get_trail_wl x1a)) ∧
          (C = None) = (Decided K ∈ set (get_trail_wl x1a) ∨
             K ∉ lits_of_l (get_trail_wl x1a)) ∧
         (∀C1. (Propagated K C1 ∈ set (get_trail_wl x1a) ⟶ C1 = the C))}› for K :: ‹nat literal› and x1a


  have already_deleted:
    ‹((x1b,  delete_index_vdom_heur x1b x2b), x1, x1a, delete_index_and_swap x2a x1) ∈ ?R S›
    if
      ‹(x, y) ∈ twl_st_heur_restart_ana' r u› and
      ‹mark_to_delete_clauses_GC_wl_D_heur_pre x› and
      ‹(S, Sa) ∈ ?sort x y› and
      ‹(l, la) ∈ nat_rel› and
      ‹la ∈ {_. True}› and
      xx: ‹(xa, x') ∈ ?R S› and
      nempty: ‹case xa of (i, S) ⇒ i < length (get_tvdom S)› and
      ‹case x' of (i, T, xs) ⇒ i < length xs› and
      st:
      ‹x2 = (x1a, x2a)›
      ‹x' = (x1, x2)›
      ‹xa = (x1b, x2b)› and
      le: ‹x1b < length (get_tvdom x2b)› and
      ‹access_tvdom_at_pre x2b x1b› and
      ba: ‹(b, ba) ∈ {(b, b'). (b, b') ∈ bool_rel ∧ b = (x2a ! x1 ∈# dom_m (get_clauses_wl x1a))}›
        ‹¬ba›
    for x y S xs l la xa x' xz x1 x2 x1a x2a x2b x2c x2d ys x1b Sa ba b
  proof -
    show ?thesis
      using xx nempty le ba unfolding st
      by (cases ‹get_tvdom x2b› rule: rev_cases)
       (auto 4 3 simp: twl_st_heur_restart_ana_def delete_index_vdom_heur_def
          twl_st_heur_restart_def mark_garbage_heur_def mark_garbage_wl_def
          learned_clss_l_l_fmdrop size_remove1_mset_If learned_clss_count_def
          aivdom_inv_removed_inactive
        intro: valid_arena_extra_information_mark_to_delete'
        intro!: aivdom_inv_dec_removed_inactive_tvdom
        dest!: in_set_butlastD in_vdom_m_fmdropD
        elim!: in_set_upd_cases)
  qed

  have mop_clause_not_marked_to_delete_heur:
    ‹mop_clause_not_marked_to_delete_heur x2b (get_tvdom x2b ! x1b)
        ≤ SPEC
           (λc. (c, x2a ! x1 ∈# dom_m (get_clauses_wl x1a))
                ∈ {(b, b'). (b,b') ∈ bool_rel ∧ (b ⟷ x2a ! x1 ∈# dom_m (get_clauses_wl x1a))})›
    if
      ‹(xa, x') ∈ ?R S› and
      ‹case xa of (i, S) ⇒ i < length (get_tvdom S)› and
      ‹case x' of (i, T, xs) ⇒ i < length xs› and
      ‹mark_to_delete_clauses_GC_wl_inv Sa xs x'› and
      ‹x2 = (x1a, x2a)› and
      ‹x' = (x1, x2)› and
      ‹xa = (x1b, x2b)› and
      ‹clause_not_marked_to_delete_heur_pre (x2b, get_tvdom x2b ! x1b)›
    for x y S Sa uu xs l la xa x' x1 x2 x1a x2a x1b x2b
    unfolding mop_clause_not_marked_to_delete_heur_def
    apply refine_vcg
    subgoal
      using that by blast
    subgoal
      using that by (auto simp: twl_st_heur_restart arena_lifting dest: twl_st_heur_restart(2) dest!: twl_st_heur_restart_anaD)
    done
  have incr_reduction_stat: ‹incr_restart_stat (set_stats_size_limit_st lbd sze T)
    ≤ ⇓ (twl_st_heur_restart_ana' r u) (remove_all_learned_subsumed_clauses_wl S)›
    if ‹(T, S) ∈ twl_st_heur_restart_ana' r u› for S T i u lbd sze
    using that
    by (cases S; cases T)
      (auto simp: conc_fun_RES incr_restart_stat_def learned_clss_count_def set_stats_size_limit_st_def
        twl_st_heur_restart_ana_def twl_st_heur_restart_def
      remove_all_learned_subsumed_clauses_wl_def clss_size_corr_def
      clss_size_lcountUE_def clss_size_lcountUS_def clss_size_def
      clss_size_resetUS_def clss_size_lcount_def clss_size_lcountU0_def incr_reduction_stat_def
        RES_RETURN_RES)

  have only_irred: ‹¬ irred (get_clauses_wl x1a) (x2a ! x1)› (is ?A) and
    get_learned_count_ge: ‹Suc 0 ≤ clss_size_lcount (get_learned_count x2b)› (is ?B)
    if
      ‹(x, y) ∈ twl_st_heur_restart_ana' r u› and
      ‹mark_to_delete_clauses_GC_wl_pre y› and
      ‹mark_to_delete_clauses_GC_wl_D_heur_pre x› and
      ‹(S, Sa) ∈ ?sort x y› and
      indices: ‹(uu, xs) ∈ ?indices S Sa› and
      ‹(l, la) ∈ nat_rel› and
      ‹la ∈ {_. True}› and
      ‹length (get_tvdom S) ≤ length (get_clauses_wl_heur x)› and
      xx: ‹(xa, x') ∈ ?R S› and
      ‹case xa of (i, S) ⇒ i < length (get_tvdom S)› and
      ‹case x' of (i, T, xs) ⇒ i < length xs› and
      ‹mark_to_delete_clauses_GC_wl_inv Sa xs x'› and
      st: ‹x2 = (x1a, x2a)› ‹x' = (x1, x2)› ‹xa = (x1b, x2b)› and
      ‹x1b < length (get_tvdom x2b)› and
      ‹access_tvdom_at_pre x2b x1b› and
      ‹clause_not_marked_to_delete_heur_pre (x2b, get_tvdom x2b ! x1b)› and
      dom: ‹(b, ba) ∈ {(b, b'). (b, b') ∈ bool_rel ∧ b = (x2a ! x1 ∈# dom_m (get_clauses_wl x1a))}›
        ‹¬ ¬ b›
        ‹¬ ¬ ba› and
      ‹0 < length (get_clauses_wl x1a ∝ (x2a ! x1))› and
      ‹get_clauses_wl x1a ∝ (x2a ! x1) ! 0 ∈# ℒall (all_init_atms_st x1a)› and
      ‹access_lit_in_clauses_heur_pre ((x2b, get_tvdom x2b ! x1b), 0)› and
      ‹length (get_clauses_wl_heur x2b) ≤ length (get_clauses_wl_heur x)› and
      ‹length (get_tvdom x2b) ≤ length (get_clauses_wl_heur x2b)› and
      ‹arena_is_valid_clause_idx (get_clauses_wl_heur x2b) (get_tvdom x2b ! x1b)›
      for x y S Sa uu xs l la xa x' x1 x2 x1a x2a x1b x2b b ba L K D bb
    proof -
      have ‹get_tvdom x2b ! x1 ∈ set (get_tvdom x2b)› and
        x: ‹(x2b, x1a) ∈ twl_st_heur_restart_ana r›
      using that by (auto dest: simp: arena_lifting twl_st_heur_restart)
    then show ?A
      using indices xx
      by (auto dest: twl_st_heur_restart_anaD twl_st_heur_restart_valid_arena
        simp: arena_lifting twl_st_heur_restart st)
    then show ?B
      using dom x by (auto simp: twl_st_heur_restart_ana_def twl_st_heur_restart_def ran_m_def
        dest!: multi_member_split
        dest!: clss_size_corr_restart_rew)
  qed
  have length_filter_le: ‹⇓ nat_rel ((RETURN ∘ (λc. length (get_clauses_wl x1a ∝ c))) (get_tvdom x2b ! x1b))
     ≤ SPEC
        (λwasted.
         do {
        _ ← log_del_clause_heur x2b (get_tvdom x2b ! x1b);
        _ ← ASSERT
          (mark_garbage_pre (get_clauses_wl_heur x2b, get_tvdom x2b ! x1b) ∧
           1 ≤ clss_size_lcount (get_learned_count x2b) ∧ x1b < length (get_tvdom x2b));
        RETURN (x1b, mark_garbage_heur3 (get_tvdom x2b ! x1b) x1b (incr_wasted_st (word_of_nat wasted) x2b))
         } ≤ SPEC
           (λc. (c, x1, mark_garbage_wl (x2a ! x1) x1a, delete_index_and_swap x2a x1) ∈ ?R S))›
    if H:
      ‹(x, y) ∈ twl_st_heur_restart_ana' r u›
      ‹mark_to_delete_clauses_GC_wl_pre y›
      ‹mark_to_delete_clauses_GC_wl_D_heur_pre x›
      ‹(S, Sa) ∈ ?sort x y›
      ‹(uu, xs) ∈ ?indices S Sa›
      ‹(l, la) ∈ nat_rel›
      ‹la ∈ {_. True}›
      ‹length (get_tvdom S) ≤ length (get_clauses_wl_heur x)›
      ‹(xa, x') ∈ ?R S›
      ‹case xa of (i, S) ⇒ i < length (get_tvdom S)›
      ‹case x' of (i, T, xs) ⇒ i < length xs›
      ‹mark_to_delete_clauses_GC_wl_inv Sa xs x'›
      ‹x2 = (x1a, x2a)›
      ‹x' = (x1, x2)›
      ‹xa = (x1b, x2b)›
      ‹x1b < length (get_tvdom x2b)›
      ‹access_tvdom_at_pre x2b x1b›
      ‹clause_not_marked_to_delete_heur_pre (x2b, get_tvdom x2b ! x1b)›
      ‹(b, ba) ∈ {(b, b'). (b, b') ∈ bool_rel ∧ b = (x2a ! x1 ∈# dom_m (get_clauses_wl x1a))}›
      ‹¬ ¬ b›
      ‹¬ ¬ ba›
      ‹0 < length (get_clauses_wl x1a ∝ (x2a ! x1))›
      ‹get_clauses_wl x1a ∝ (x2a ! x1) ! 0 ∈# ℒall (all_init_atms_st x1a)›
      ‹access_lit_in_clauses_heur_pre ((x2b, get_tvdom x2b ! x1b), 0)›
      ‹length (get_clauses_wl_heur x2b) ≤ length (get_clauses_wl_heur x)›
      ‹length (get_tvdom x2b) ≤ length (get_clauses_wl_heur x2b)›
      ‹arena_is_valid_clause_idx (get_clauses_wl_heur x2b) (get_tvdom x2b ! x1b)›
      ‹(arena_length (get_clauses_wl_heur x2b) (get_tvdom x2b ! x1b) ≠ 2, can_del)
    ∈ bool_rel›
      ‹x1 < length x2a›
      ‹arena_length (get_clauses_wl_heur x2b) (get_tvdom x2b ! x1b) ≠ 2›
      can_del
    for x y S Sa xs l la xa x' x1 x2 x1a x2a x1b x2b b ba can_del D L K bb uu
  proof -
      have [simp]: ‹mark_garbage_heur3 i C (incr_wasted_st b S) = incr_wasted_st b (mark_garbage_heur3 i C S)› for i C S b
        by (cases S; auto simp: mark_garbage_heur3_def incr_wasted_st_def)
      have ‹mark_garbage_pre (get_clauses_wl_heur x2b, get_tvdom x2b ! x1b)›
        ‹x1b < length (get_tvdom x2b)›
        using that
        unfolding prod.simps mark_garbage_pre_def
          arena_is_valid_clause_vdom_def arena_is_valid_clause_idx_def apply -
        by (rule exI[of _ ‹get_clauses_wl x1a›], rule exI[of _ ‹set (get_vdom x2b)›])
         (auto simp: twl_st_heur_restart twl_st_heur_restart_ana_def dest: twl_st_heur_restart_valid_arena)
      moreover have 0: ‹Suc 0 ≤ clss_size_lcount (get_learned_count x2b)›
         ‹¬ irred (get_clauses_wl x1a) (x2a ! x1)› 
        using get_learned_count_ge[OF that(1-27)] only_irred[OF that(1-27)] by auto
      moreover have ‹(mark_garbage_heur3 (get_tvdom x2b ! x1) x1
        (incr_wasted_st (word_of_nat (length (get_clauses_wl x1a ∝ (get_tvdom x2b ! x1)))) x2b),
        mark_garbage_wl (get_tvdom x2b ! x1) x1a)
        ∈ twl_st_heur_restart_ana r›
        by (use that 0 in
          ‹auto intro!: incr_wasted_st mark_garbage_heur_wl_ana simp: twl_st_heur_restart
          learned_clss_count_mark_garbage_heur3
          dest: twl_st_heur_restart_valid_arena twl_st_heur_restart_anaD›)
      moreover have ‹learned_clss_count
        (mark_garbage_heur3 (get_tvdom x2b ! x1) x1
        (incr_wasted_st (word_of_nat (length (get_clauses_wl x1a ∝ (get_tvdom x2b ! x1)))) x2b))
        ≤ u›
        by (use that 0 in
          ‹auto intro!: incr_wasted_st mark_garbage_heur_wl_ana simp: twl_st_heur_restart
          learned_clss_count_mark_garbage_heur3
          dest: twl_st_heur_restart_valid_arena twl_st_heur_restart_anaD›)
      moreover have ‹xb ∈ set (get_tvdom S)›
        if ‹xb ∈ set (butlast ((get_tvdom x2b)[x1 := last (get_tvdom x2b)]))› for xb
      proof -
        have ‹xb ∈ set (get_tvdom x2b)›
          using that H by (auto dest!: in_set_butlastD)
            (metis Misc.last_in_set in_set_upd_eq len_greater_imp_nonempty)
        then show ?thesis
          using H by auto
      qed
      moreover have ‹¬irred (get_clauses_wl (mark_garbage_wl (get_tvdom x2b ! x1) x1a)) C›
        if ‹C ∈ set (butlast ((get_tvdom x2b)[x1 := last (get_tvdom x2b)]))› for C
      proof -
        have a: ‹distinct (get_tvdom x2b)› ‹x1 < length (get_tvdom x2b)›
          using  H(9-15) by (auto simp: twl_st_heur_restart_ana_def
            twl_st_heur_restart_def aivdom_inv_dec_alt_def)
        then have 1: ‹get_tvdom x2b = take x1 (get_tvdom x2b) @ get_tvdom x2b ! x1 # drop (Suc x1) (get_tvdom x2b)›
          by (subst append_take_drop_id[of x1, symmetric], subst Cons_nth_drop_Suc[symmetric])
           auto
        have ‹set (delete_index_and_swap (get_tvdom x2b) x1) =
          set (get_tvdom x2b) - {get_tvdom x2b!x1}›
          using a
          apply (subst (asm) (2)1, subst (asm) (1)1)
          apply (subst (2)1, subst (1)1)
          apply (cases ‹drop (Suc x1) (get_tvdom x2b)› rule: rev_cases)
          by (auto simp: nth_append list_update_append1 list_update_append2 butlast_append
            dest: in_set_butlastD)
        then have [simp]: ‹C ≠ get_tvdom x2b ! x1›
          using that by auto
        show ?thesis
          using that H
          apply (cases x1a)
          apply (auto simp: mark_garbage_wl_def)
          by (metis Misc.last_in_set in_set_butlastD in_set_upd_cases len_greater_imp_nonempty)
      qed
      ultimately show ?thesis apply -
        using that
        apply (auto intro!: ASSERT_leI)
        apply (subst bind_rule_complete)
        apply (rule order_trans)
        apply (rule log_del_clause_heur_log_clause[where r=r and u=u])
        by auto
  qed
  show ?thesis
    supply sort_vdom_heur_def[simp] twl_st_heur_restart_anaD[dest] [[goals_limit=1]]
    unfolding mark_to_delete_clauses_GC_wl_D_heur_alt_def mark_to_delete_clauses_GC_wl_D_alt_def
      access_lit_in_clauses_heur_def
    apply (intro frefI nres_relI)
    apply (refine_vcg sort_vdom_heur_reorder_vdom_wl[THEN fref_to_Down] incr_reduction_stat find_largest_lbd_and_size)
    subgoal
      unfolding mark_to_delete_clauses_GC_wl_D_heur_pre_def by fast
    apply assumption
    subgoal by auto
    subgoal for x y S T unfolding number_clss_to_keep_def by (cases S) (auto)
    apply (solves auto)
    subgoal by (auto simp: twl_st_heur_restart_ana_def twl_st_heur_restart_def aivdom_inv_dec_alt_def
       dest!: valid_arena_vdom_subset size_mset_mono)
    apply (rule init; solves auto)
    subgoal by auto
    subgoal by auto
    subgoal by (auto simp: access_tvdom_at_pre_def)
    subgoal for x y S Sa u xs l la _ _ x1 x2 xb x' x1c x2c x1a x2a x1b x2b
      unfolding clause_not_marked_to_delete_heur_pre_def arena_is_valid_clause_vdom_def
        prod.simps
      by (rule exI[of _ ‹get_clauses_wl (fst x2c)›], rule exI[of _ ‹set (get_vdom x2b)›])
         (auto simp: twl_st_heur_restart
          intro!: twl_st_heur_restart_valid_arena[simplified]
          dest: twl_st_heur_restart_get_tvdom_nth_get_vdom[simplified])
    apply (rule mop_clause_not_marked_to_delete_heur; assumption)
    subgoal for x y S Sa uu xs l la xa x' x1 x2 x1a x2a x1b x2b
      by (auto simp: twl_st_heur_restart)
    subgoal
      by (rule already_deleted)
    subgoal for x y S Sa u xs l la _ _ x1 x2 xb x' x1c x2c x1a x2a x1b x2b
      unfolding access_lit_in_clauses_heur_pre_def prod.simps arena_lit_pre_def
        arena_is_valid_clause_idx_and_access_def
      by (rule bex_leI[of _ ‹get_tvdom x2b ! x1b›], simp add: aivdom_inv_dec_alt_def,
        rule exI[of _ ‹get_clauses_wl (fst x2c)›])
        (auto simp: twl_st_heur_restart_ana_def twl_st_heur_restart_def aivdom_inv_dec_alt_def)
    subgoal by (auto simp: twl_st_heur_restart_ana_def twl_st_heur_restart_def dest!: valid_arena_vdom_subset size_mset_mono)
    subgoal premises p using p(7-)
      by (auto simp: twl_st_heur_restart_ana_def twl_st_heur_restart_def aivdom_inv_dec_alt_def
        dest!: valid_arena_vdom_subset size_mset_mono)
    subgoal for x y S Sa u xs l la _ _ x1 x2 xb x' x1c x2c x1a x2a x1b x2b
      unfolding prod.simps
        arena_is_valid_clause_vdom_def arena_is_valid_clause_idx_def
      by (rule exI[of _ ‹get_clauses_wl (fst x2c)›], rule exI[of _ ‹set (get_vdom x2b)›])
        (auto simp: twl_st_heur_restart intro!: twl_st_heur_restart_valid_arena[simplified]
        dest: twl_st_heur_restart_get_avdom_nth_get_vdom)
    subgoal
      unfolding marked_as_used_pre_def
      by (auto simp: twl_st_heur_restart reason_rel_def)
    subgoal
      by (auto dest!: twl_st_heur_restart_anaD twl_st_heur_restart_valid_arena[simplified]
        simp: arena_lifting)
    subgoal by fast
    subgoal for x y S Sa u xs l la _ _ x1 x2 xb x' x1c x2c x1a x2a x1b x2b
      unfolding mop_arena_length_st_def
      apply (rule mop_arena_length[THEN fref_to_Down_curry, THEN order_trans,
        of ‹get_clauses_wl x1a› ‹get_tvdom x2b ! x1b› _ _ ‹set (get_vdom x2b)›])
      subgoal
        by auto
      subgoal
        by (auto simp: twl_st_heur_restart_valid_arena[simplified])
      subgoal
        by (rule length_filter_le)
     done
   subgoal for x y
      unfolding valid_sort_clause_score_pre_def arena_is_valid_clause_vdom_def
        get_clause_LBD_pre_def arena_is_valid_clause_idx_def arena_act_pre_def
      by (force simp: valid_sort_clause_score_pre_def twl_st_heur_restart_ana_def arena_dom_status_iff
        arena_act_pre_def get_clause_LBD_pre_def arena_is_valid_clause_idx_def twl_st_heur_restart_def
         intro!: exI[of _ ‹get_clauses_wl T›] dest!: set_mset_mono mset_subset_eqD)
    subgoal for x y S Sa uu xs l la xa x' x1 x2 x1a x2a x1c x2c b ba L x2b
      using size_mset_mono[of ‹mset (get_tvdom x2b)› ‹mset (get_vdom x2b)›]
      by (clarsimp simp: twl_st_heur_restart_ana_def twl_st_heur_restart_def aivdom_inv_dec_alt_def
        dest!: valid_arena_vdom_subset)
    subgoal
      by auto
    done
qed



definition isasat_GC_entry :: ‹_› where
‹isasat_GC_entry 𝒜 vdom0 arena_old W'  = {((arenao, (arena, aivdom)), (No, N)). valid_arena arenao No vdom0 ∧ valid_arena arena N (set (get_vdom_aivdom aivdom)) ∧ vdom_m 𝒜 W' No ⊆ vdom0 ∧ dom_m N = mset (get_vdom_aivdom aivdom) ∧
  arena_is_packed arena N ∧
  aivdom_inv_strong_dec aivdom (dom_m N) ∧
  length arenao = length arena_old ∧
    move_is_packed arenao No arena N}›

definition isasat_GC_refl :: ‹_› where
‹isasat_GC_refl 𝒜 vdom0 arena_old = {((arenao, (arena, aivdom), W), (No, N, W')). valid_arena arenao No vdom0 ∧ valid_arena arena N (set (get_vdom_aivdom aivdom)) ∧
     (W, W') ∈ ⟨Id⟩map_fun_rel (D0 𝒜) ∧ vdom_m 𝒜 W' No ⊆ vdom0 ∧ dom_m N = mset (get_vdom_aivdom aivdom) ∧
  arena_is_packed arena N ∧ aivdom_inv_strong_dec aivdom (dom_m N) ∧
  length arenao = length arena_old ∧
    (∀L ∈# ℒall 𝒜. length (W' L) ≤ length arenao) ∧move_is_packed arenao No arena N}›

lemma move_is_packed_empty[simp]: ‹valid_arena arena N vdom ⟹ move_is_packed arena N [] fmempty›
  by (auto simp: move_is_packed_def valid_arena_ge_length_clauses)

lemma move_is_packed_append:
  assumes
    dom: ‹C ∈# dom_m x1a› and
    E: ‹length E = length (x1a ∝ C) + header_size (x1a ∝ C)› ‹(fst E') = (x1a ∝ C)›
     ‹n = header_size (x1a ∝ C)› and
    valid: ‹valid_arena x1d x2a D'› and
    packed: ‹move_is_packed x1c x1a x1d x2a›
  shows ‹move_is_packed (extra_information_mark_to_delete x1c C)
          (fmdrop C x1a)
          (x1d @ E)
          (fmupd (length x1d + n) E' x2a)›
proof -
  have [simp]: ‹(∑x∈#remove1_mset C
          (dom_m
            x1a). length
                   (fst (the (if x = C then None
                              else fmlookup x1a x))) +
                  header_size
                   (fst (the (if x = C then None
                              else fmlookup x1a x)))) =
     (∑x∈#remove1_mset C
          (dom_m
            x1a). length
                   (x1a ∝ x) +
                  header_size
                   (x1a ∝ x))›
   by (rule sum_mset_cong)
    (use distinct_mset_dom[of x1a] in ‹auto dest!: simp: distinct_mset_remove1_All›)
  have [simp]: ‹(length x1d + header_size (x1a ∝ C)) ∉# (dom_m x2a)›
    using valid arena_lifting(2) by blast
  have [simp]: ‹(∑x∈#(dom_m x2a). length
                    (fst (the (if length x1d + header_size (x1a ∝ C) = x
                               then Some E'
                               else fmlookup x2a x))) +
                   header_size
                    (fst (the (if length x1d + header_size (x1a ∝ C) = x
                               then Some E'
                               else fmlookup x2a x)))) =
    (∑x∈#dom_m x2a. length
                    (x2a ∝ x) +
                   header_size
                    (x2a ∝ x))›
   by (rule sum_mset_cong)
    (use distinct_mset_dom[of x2a] in ‹auto dest!: simp: distinct_mset_remove1_All›)
  show ?thesis
    using packed dom E
    by (auto simp: move_is_packed_def split: if_splits dest!: multi_member_split)
qed
(*
lemma aivdom_inv_intro_add_mset_irred:
  ‹C ∉# d ⟹ C ∉ set vdom ⟹ aivdom_inv (vdom, avdom, ivdom, tvdom) d ⟹ aivdom_inv (vdom @ [C], avdom, ivdom @ [C], tvdom) (add_mset C d)›
  unfolding aivdom_inv_alt_def
  by (cases ‹C ∈ (set avdom ∪ set ivdom)›)
   (auto dest: subset_mset_imp_subset_add_mset)
*)
lemma isasat_GC_clauses_prog_copy_wl_entry:
  assumes ‹valid_arena arena N vdom0› and
    ‹valid_arena arena' N' (set (get_vdom_aivdom aivdom))› and
    vdom: ‹vdom_m 𝒜 W N ⊆ vdom0› and
    L: ‹atm_of A ∈# 𝒜› and
    L'_L: ‹(A', A) ∈ nat_lit_lit_rel› and
    W: ‹(W' , W) ∈ ⟨Id⟩map_fun_rel (D0 𝒜)› and
    ‹dom_m N' = mset (get_vdom_aivdom aivdom)› and
   ‹arena_is_packed arena' N'› and
    ivdom: ‹aivdom_inv_strong_dec aivdom (dom_m N')› and
    r: ‹length arena = r› and
    le: ‹∀L ∈# ℒall 𝒜. length (W L) ≤ length arena› and
    packed: ‹move_is_packed arena N arena' N'›
  shows ‹isasat_GC_clauses_prog_copy_wl_entry arena W' A' (arena', aivdom)
     ≤ ⇓ (isasat_GC_entry 𝒜 vdom0 arena W)
         (cdcl_GC_clauses_prog_copy_wl_entry N (W A) A N')›
     (is ‹_ ≤ ⇓ (?R) _›)
proof -
  have A: ‹A' = A› and K[simp]: ‹W' ! nat_of_lit A = W A›
    using L'_L L W apply auto
    by (cases A) (auto simp: map_fun_rel_def ℒall_add_mset dest!: multi_member_split)
  have A_le: ‹nat_of_lit A < length W'›
    using W L by (cases A; auto simp: map_fun_rel_def ℒall_add_mset dest!: multi_member_split)
  have length_slice: ‹C ∈# dom_m x1a ⟹ valid_arena x1c x1a vdom' ⟹
      length
     (Misc.slice (C - header_size (x1a ∝ C))
       (C + arena_length x1c C) x1c) =
    arena_length x1c C + header_size (x1a ∝ C)› for x1c x1a C vdom'
     using arena_lifting(1-4,10)[of x1c x1a vdom' C]
    by (auto simp: header_size_def slice_len_min_If min_def split: if_splits)
  show ?thesis
    unfolding isasat_GC_clauses_prog_copy_wl_entry_def cdcl_GC_clauses_prog_copy_wl_entry_def prod.case A
    arena_header_size_def[symmetric]
    apply (refine_vcg ASSERT_leI WHILET_refine[where R = ‹nat_rel ×r ?R›])
    subgoal using A_le by (auto simp: isasat_GC_entry_def)
    subgoal using le L K by (cases A) (auto dest!: multi_member_split simp: ℒall_add_mset)
    subgoal using assms by (auto simp: isasat_GC_entry_def)
    subgoal using W L by auto
    subgoal by auto
    subgoal for x x' x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d
      using vdom L
      unfolding arena_is_valid_clause_vdom_def K isasat_GC_entry_def
      by (cases A)
        (force dest!: multi_member_split simp: vdom_m_def ℒall_add_mset)+
    subgoal
      using vdom L
      unfolding arena_is_valid_clause_vdom_def K isasat_GC_entry_def
      by (subst arena_dom_status_iff)
        (cases A ; auto dest!: multi_member_split simp: arena_lifting arena_dom_status_iff
            vdom_m_def ℒall_add_mset; fail)+
   subgoal
     unfolding arena_is_valid_clause_idx_def isasat_GC_entry_def
     by auto
   subgoal unfolding isasat_GC_entry_def move_is_packed_def arena_is_packed_def
       by (auto simp: valid_arena_header_size arena_lifting dest!: multi_member_split)
   subgoal using r by (auto simp: isasat_GC_entry_def)
   subgoal by (auto dest: valid_arena_header_size simp: arena_lifting dest!: valid_arena_vdom_subset multi_member_split simp: arena_header_size_def isasat_GC_entry_def aivdom_inv_strong_dec_alt_def
    split: if_splits)
   subgoal by (auto simp: isasat_GC_entry_def aivdom_inv_strong_dec_alt_def dest!: size_mset_mono)
   subgoal by (auto simp: isasat_GC_entry_def aivdom_inv_strong_dec_alt_def dest!: size_mset_mono)
   subgoal by (auto simp: isasat_GC_entry_def aivdom_inv_strong_dec_alt_def dest!: size_mset_mono)
   subgoal 
     by (force simp: isasat_GC_entry_def dest: arena_lifting(2))
   subgoal by (auto simp: arena_header_size_def)
   subgoal for x x' x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d D
     using valid_arena_in_vdom_le_arena(1)[of x1d x2a ‹set (get_vdom_aivdom x2d)› D] apply -
(*TODO slow*)
     by (rule order_trans[OF fm_mv_clause_to_new_arena])
      (force intro: valid_arena_extra_information_mark_to_delete'
         simp: arena_lifting remove_1_mset_id_iff_notin
            mark_garbage_pre_def isasat_GC_entry_def min_def
            valid_arena_header_size
       simp del: aivdom_inv.simps
       dest: in_vdom_m_fmdropD arena_lifting(2)
       intro!: arena_is_packed_append_valid subset_mset_trans_add_mset
       aivdom_inv_dec_intro_init_strong_add_mset aivdom_inv_dec_intro_learned_strong_add_mset
       move_is_packed_append length_slice aivdom_inv_intro_add_mset)+
   subgoal
     by auto
   subgoal
     by auto
   done
 qed

lemma isasat_GC_clauses_prog_single_wl:
  assumes
    ‹(X, X') ∈ isasat_GC_refl 𝒜 vdom0 arena0› and
    X: ‹X = (arena, (arena', aivdom), W)› ‹X' = (N, N', W')› and
    L: ‹A ∈# 𝒜› and
    st: ‹(A, A') ∈ Id› and
    st': ‹narena = (arena', aivdom)› and
    ae: ‹length arena0 = length arena› and
    le_all: ‹∀L ∈# ℒall 𝒜. length (W' L) ≤ length arena›
  shows ‹isasat_GC_clauses_prog_single_wl arena narena  W A
     ≤ ⇓ (isasat_GC_refl 𝒜 vdom0 arena0)
         (cdcl_GC_clauses_prog_single_wl N W' A' N')›
     (is ‹_ ≤ ⇓ ?R _›)
proof -
  let ?vdom = ‹get_vdom_aivdom aivdom›
  have H:
    ‹valid_arena arena N vdom0›
    ‹valid_arena arena' N' (set ?vdom)› and
    vdom: ‹vdom_m 𝒜 W' N ⊆ vdom0› and
    L: ‹A ∈# 𝒜› and
    eq: ‹A' = A› and
    WW': ‹(W, W') ∈ ⟨Id⟩map_fun_rel (D0 𝒜)› and
    vdom_dom: ‹dom_m N' = mset ?vdom› and
    packed: ‹arena_is_packed arena' N'› and
    aivdom: ‹aivdom_inv_strong_dec aivdom (dom_m N')› and
    packed2: ‹move_is_packed arena N arena' N'› and
    incl: ‹vdom_m 𝒜 W' N ⊆ vdom0›
    using assms X st by (auto simp: isasat_GC_refl_def)

  have vdom2: ‹vdom_m 𝒜 W' x1 ⊆ vdom0 ⟹ vdom_m 𝒜 (W'(L := [])) x1 ⊆ vdom0› for x1 L
    by (force simp: vdom_m_def dest!: multi_member_split)
  have vdom_m_upd: ‹x ∈ vdom_m 𝒜 (W(Pos A := [], Neg A := [])) N ⟹ x ∈ vdom_m 𝒜 W N› for x W A N
    by (auto simp: image_iff vdom_m_def dest: multi_member_split)
  have vdom_m3: ‹x ∈ vdom_m 𝒜 W a ⟹ dom_m a ⊆# dom_m b ⟹ dom_m b ⊆# dom_m c ⟹x ∈ vdom_m 𝒜 W c› for a b c W x
    unfolding vdom_m_def by auto
  have W: ‹(W[2 * A := [], Suc (2 * A) := []], W'(Pos A := [], Neg A := []))
       ∈ ⟨Id⟩map_fun_rel (D0 𝒜)› for A
    using WW' unfolding map_fun_rel_def
    apply clarify
    apply (intro conjI)
    apply auto[]
    apply (drule multi_member_split)
    apply (case_tac L)
    apply (auto dest!: multi_member_split)
    done
  have le: ‹nat_of_lit (Pos A) < length W› ‹nat_of_lit (Neg A) < length W›
    using WW' L by (auto dest!: multi_member_split simp: map_fun_rel_def ℒall_add_mset)
  have [refine0]: ‹RETURN (Pos A) ≤ ⇓ Id (RES {Pos A, Neg A})› by auto
  have vdom_upD:‹ x ∈ vdom_m 𝒜 (W'(Pos A := [], Neg A := [])) xd ⟹ x ∈  vdom_m 𝒜 (λa. if a = Pos A then [] else W' a) xd›
    for W' a A x xd
    by (auto simp: vdom_m_def)
  show ?thesis
    unfolding isasat_GC_clauses_prog_single_wl_def
      cdcl_GC_clauses_prog_single_wl_def eq st' isasat_GC_refl_def
    apply (refine_vcg
      isasat_GC_clauses_prog_copy_wl_entry[where r= ‹length arena› and 𝒜 = 𝒜])
    subgoal using le by auto
    subgoal using le by auto
    apply (rule H(1); fail)
    apply (rule H(2); fail)
    subgoal using incl by auto
    subgoal using L by auto
    subgoal using WW' by auto
    subgoal using vdom_dom by blast
    subgoal using packed by blast
    subgoal using aivdom by blast
    subgoal by blast
    subgoal using le_all by auto
    subgoal using packed2 by auto
    subgoal using ae by (auto simp: isasat_GC_entry_def)
    apply (solves ‹auto simp: isasat_GC_entry_def›)
    apply (solves ‹auto simp: isasat_GC_entry_def›)
    apply (rule vdom2; auto)
    supply isasat_GC_entry_def[simp]
    subgoal using WW' by (auto simp: map_fun_rel_def dest!: multi_member_split simp: ℒall_add_mset)
    subgoal using L by auto
    subgoal using L by auto
    subgoal using WW' by (auto simp: map_fun_rel_def dest!: multi_member_split simp: ℒall_add_mset)
    subgoal using WW' by (auto simp: map_fun_rel_def dest!: multi_member_split simp: ℒall_add_mset)
    subgoal using WW' le_all by (auto simp: map_fun_rel_def dest!: multi_member_split simp: ℒall_add_mset)
    subgoal using WW' le_all by (auto simp: map_fun_rel_def dest!: multi_member_split simp: ℒall_add_mset)
    subgoal using WW' le_all by (auto simp: map_fun_rel_def dest!: multi_member_split simp: ℒall_add_mset)
    subgoal using WW' le_all by (auto simp: map_fun_rel_def dest!: multi_member_split simp: ℒall_add_mset)
    subgoal using W ae le_all aivdom by (auto simp: dest!: vdom_upD)
    done
qed

definition cdcl_GC_clauses_prog_wl2  where
  ‹cdcl_GC_clauses_prog_wl2 = (λN0 𝒜0 WS. do {
    𝒜 ← SPEC(λ𝒜. set_mset 𝒜 = set_mset 𝒜0);
    (_, (N, N', WS)) ← WHILET⇗cdcl_GC_clauses_prog_wl_inv 𝒜 N0⇖
      (λ(ℬ, _). ℬ ≠ {#})
      (λ(ℬ, (N, N', WS)). do {
        ASSERT(ℬ ≠ {#});
        A ← SPEC (λA. A ∈# ℬ);
        (N, N', WS) ← cdcl_GC_clauses_prog_single_wl N WS A N';
        RETURN (remove1_mset A ℬ, (N, N', WS))
      })
      (𝒜, (N0, fmempty, WS));
    RETURN (N, N', WS)
  })›


lemma cdcl_GC_clauses_prog_wl_inv_cong_empty:
  ‹set_mset 𝒜 = set_mset ℬ ⟹
  cdcl_GC_clauses_prog_wl_inv 𝒜 N ({#}, x) ⟹ cdcl_GC_clauses_prog_wl_inv ℬ N ({#}, x)›
  by (auto simp: cdcl_GC_clauses_prog_wl_inv_def)

lemma isasat_GC_clauses_prog_wl2:
  assumes ‹valid_arena arenao No vdom0› and
    ‹valid_arena arena N (set vdom)› and
    vdom: ‹vdom_m 𝒜 W' No ⊆ vdom0› and
    vmtf: ‹ns ∈ bump_heur 𝒜 M› and
    nempty: ‹𝒜 ≠ {#}› and
    W_W': ‹(W, W') ∈ ⟨Id⟩map_fun_rel (D0 𝒜)› and
    bounded: ‹isasat_input_bounded 𝒜› and old: ‹old_arena = []› and
    le_all: ‹∀L ∈# ℒall 𝒜. length (W' L) ≤ length arenao›
 shows
    ‹isasat_GC_clauses_prog_wl2 ns (arenao, (old_arena, empty_aivdom aivdom), W)
        ≤ ⇓ ({((arenao', (arena, aivdom), W), (No', N, W')). valid_arena arenao' No' vdom0 ∧
                valid_arena arena N (set (get_vdom_aivdom aivdom)) ∧
       (W, W') ∈ ⟨Id⟩map_fun_rel (D0 𝒜) ∧ vdom_m 𝒜 W' No' ⊆ vdom0 ∧
        cdcl_GC_clauses_prog_wl_inv 𝒜 No ({#}, No', N, W') ∧ dom_m N = mset (get_vdom_aivdom aivdom) ∧
         arena_is_packed arena N ∧ aivdom_inv_strong_dec aivdom (dom_m N) ∧
       length arenao' = length arenao})
         (cdcl_GC_clauses_prog_wl2 No 𝒜 W')›
proof -
  define f where
    ‹f A ≡ (λ(arenao, arena, W). isasat_GC_clauses_prog_single_wl arenao arena W A)› for A :: nat
  let ?R = ‹{((𝒜', arenao', (arena, vdom), W), (𝒜'', No', N, W')). 𝒜' = 𝒜'' ∧
      ((arenao', (arena, vdom), W), (No', N, W')) ∈ isasat_GC_refl 𝒜 vdom0 arenao ∧
      length arenao' = length arenao}›
  have H: ‹(X, X') ∈ ?R ⟹ X = (x1, x2) ⟹ x2 = (x3, x4) ⟹ x4 = (x5, x6) ⟹
     X' = (x1', x2') ⟹ x2' = (x3', x4') ⟹ x4' = (x5', x6') ⟹
     ((x3, (fst x5, (snd x5)), x6), (x3', x5', x6')) ∈ isasat_GC_refl 𝒜 vdom0 arenao›
    for X X' A B x1 x1' x2 x2' x3 x3' x4 x4' x5 x5' x6 x6' x0 x0' x x'
     supply [[show_types]]
    by auto
  have isasat_GC_clauses_prog_wl_alt_def:
    ‹isasat_GC_clauses_prog_wl2 n x0 = iterate_over_VMTF f (λx. length (fst x) = length (fst x0)) (fst (bump_get_heuristics n), Some (bumped_vmtf_array_fst n)) x0›
    (is ‹?A = ?B›)
    for n x0
  proof -
    have [refine0]: ‹((Some (fst (snd (snd (bump_get_heuristics n)))), x0),
      snd (fst (bump_get_heuristics n), Some (fst ((snd (snd (bump_get_heuristics n)))))), x0) ∈ Id›
      ‹((snd (fst (bump_get_heuristics n), Some (fst ((snd (snd (bump_get_heuristics n)))))), x0),
         Some (fst (snd ((snd (bump_get_heuristics n))))), x0) ∈ Id›
      ‹a=a' ⟹ b=b' ⟹ c=c' ⟹ d=d' ⟹ isasat_GC_clauses_prog_single_wl a b c d ≤ ⇓Id (isasat_GC_clauses_prog_single_wl a' b' c' d')›
      for a' b' c' d' a b c d
      by auto
    have ‹?A ≤ ⇓Id ?B›
      unfolding f_def isasat_GC_clauses_prog_wl2_def iterate_over_VMTF_def
        bumped_vmtf_array_fst_def access_focused_vmtf_array_def nres_monad3
        case_prod_beta
      by refine_rcg (solves ‹(auto simp: length_bumped_vmtf_array_def)›)+
    moreover have ‹?B ≤ ⇓Id ?A›
      unfolding f_def isasat_GC_clauses_prog_wl2_def iterate_over_VMTF_def
        bumped_vmtf_array_fst_def access_focused_vmtf_array_def nres_monad3
        case_prod_beta
      by refine_vcg (solves ‹(auto simp: length_bumped_vmtf_array_def)›)+
    ultimately show ?thesis
      by auto
  qed
  have empty[simp]: ‹aivdom_inv_dec (AIvdom ([], [], [], [])) {#}›
    by (auto simp: aivdom_inv_dec_alt_def)
  obtain M' where vmtf': ‹(fst (bump_get_heuristics ns), fst (snd (bump_get_heuristics ns)),
    bumped_vmtf_array_fst  ns, fst (snd (snd (snd (bump_get_heuristics ns)))), snd (snd (snd (snd (bump_get_heuristics ns))))) ∈ vmtf 𝒜 M'› and
    ‹M' = M ∨ M' = get_unit_trail M›
    using vmtf unfolding bump_heur_def
    by (cases ‹bump_get_heuristics ns›) (auto simp: bump_get_heuristics_def bumped_vmtf_array_fst_def
      split: if_splits)
  show ?thesis
    unfolding isasat_GC_clauses_prog_wl_alt_def prod.case f_def[symmetric] old
    apply (rule order_trans[OF iterate_over_VMTF_iterate_over_ℒall[OF vmtf' nempty bounded, 
      where I' = ‹λ_ x. length (fst x) = length (fst (arenao, ([], empty_aivdom aivdom), W))›]])
    subgoal by auto
    unfolding Down_id_eq iterate_over_ℒall_def cdcl_GC_clauses_prog_wl2_def f_def
    apply (refine_vcg WHILEIT_refine_with_invariant_and_break[where R = ?R]
            isasat_GC_clauses_prog_single_wl)
    subgoal by fast
    subgoal using assms by (auto simp: valid_arena_empty isasat_GC_refl_def)
    subgoal by auto
    subgoal by auto
    subgoal by auto
    subgoal by auto
    apply (rule H; assumption; fail)
    apply (rule refl)+
    subgoal by (auto simp add: cdcl_GC_clauses_prog_wl_inv_def)
    subgoal by auto
    subgoal by auto
    subgoal using le_all by (auto simp: isasat_GC_refl_def split: prod.splits)
    subgoal by (auto simp: isasat_GC_refl_def)
    subgoal by (auto simp: isasat_GC_refl_def
      dest: cdcl_GC_clauses_prog_wl_inv_cong_empty)
    done
qed


lemma cdcl_GC_clauses_prog_wl_alt_def:
  ‹cdcl_GC_clauses_prog_wl = (λ(M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, WS). do {
    ASSERT(cdcl_GC_clauses_pre_wl (M, N, D, NE, UE, NEk, UEk,NS, US, N0, U0, Q, WS));
    (N, N', WS) ← cdcl_GC_clauses_prog_wl2 N (all_init_atms N (NE+NEk+NS+N0)) WS;
    RETURN (M, N', D, NE, UE, NEk, UEk,NS, US, N0, U0, Q, WS)
  })›
proof -
   have [refine0]: ‹(x1c, x1) ∈ Id ⟹ RES (set_mset x1c)
       ≤ ⇓ Id  (RES (set_mset x1))› for x1 x1c
     by auto
   have [refine0]: ‹(xa, x') ∈ Id ⟹
       x2a = (x1b, x2b) ⟹
       x2 = (x1a, x2a) ⟹
       x' = (x1, x2) ⟹
       x2d = (x1e, x2e) ⟹
       x2c = (x1d, x2d) ⟹
       xa = (x1c, x2c) ⟹
       (A, Aa) ∈ Id ⟹
       cdcl_GC_clauses_prog_single_wl x1d x2e A x1e
       ≤ ⇓ Id
          (cdcl_GC_clauses_prog_single_wl x1a x2b Aa x1b)›
      for 𝒜 x xa x' x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e A aaa Aa
      by auto
   show ?thesis
     unfolding cdcl_GC_clauses_prog_wl_def cdcl_GC_clauses_prog_wl2_def
       while.imonad3

     apply (intro ext)
     apply (clarsimp simp add: while.imonad3)
     apply (subst dual_order.eq_iff[of ‹(_ :: _ nres)›])
     apply (intro conjI)
     subgoal
       by (rewrite at ‹_ ≤ ⌑› Down_id_eq[symmetric])
        (refine_rcg WHILEIT_refine[where R = Id], auto simp add: all_init_atms_st_def)
     subgoal
       by (rewrite at ‹_ ≤ ⌑› Down_id_eq[symmetric])
        (refine_rcg WHILEIT_refine[where R = Id], auto simp add: all_init_atms_st_def)
     done
qed


lemma length_watched_le'':
  assumes
    xb_x'a: ‹(x1a, x1) ∈ twl_st_heur_restart› and
    prop_inv: ‹correct_watching'_nobin x1›
  shows ‹∀x2 ∈# ℒall (all_init_atms_st x1). length (watched_by x1 x2) ≤ length (get_clauses_wl_heur x1a)›
proof
  fix x2
  assume x2: ‹x2 ∈# ℒall (all_init_atms_st x1)›
  have ‹correct_watching'_nobin 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
    by (cases x1; auto simp: ℒall_all_init_atms correct_watching'_nobin.simps
      simp flip: all_init_lits_def all_init_lits_alt_def)
  then have dist: ‹distinct_watched (watched_by x1 x2)›
    using xb_x'a
    by (cases x1; auto simp: ℒall_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_restart_def aivdom_inv_dec_alt_def)
  have x2: ‹x2 ∈# ℒall (all_init_atms_st x1)›
    using x2 xb_x'a unfolding all_init_atms_def all_init_lits_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_restart_def)

  have ‹vdom_m (all_init_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_restart_def all_atms_def[symmetric] all_init_atms_st_def)
  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_restart_def simp flip: all_init_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)›
    by (subst distinct_card[OF dist_vdom, symmetric])
      (use card_mono[OF _ vdom_incl] in auto)
  then show ‹length (watched_by x1 x2) ≤ length (get_clauses_wl_heur x1a)›
    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

lemma length_watched_le''':
  assumes
    xb_x'a: ‹(x1a, x1) ∈ twl_st_heur_restart› and
    prop_inv: ‹no_lost_clause_in_WL x1›
  shows ‹∀x2 ∈# ℒall (all_init_atms_st x1). length (watched_by x1 x2) ≤ length (get_clauses_wl_heur x1a)›
proof
  fix x2
  assume x2: ‹x2 ∈# ℒall (all_init_atms_st x1)›
  have dist: ‹distinct_watched (watched_by x1 x2)›
    using x2 prop_inv
    by (cases x1; auto simp: ℒall_all_init_atms no_lost_clause_in_WL_def
      simp flip: all_init_lits_def all_init_lits_alt_def)
  then have dist: ‹distinct_watched (watched_by x1 x2)›
    using xb_x'a
    by (cases x1; auto simp: ℒall_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_restart_def aivdom_inv_dec_alt_def)
  have x2: ‹x2 ∈# ℒall (all_init_atms_st x1)›
    using x2 xb_x'a unfolding all_init_atms_def all_init_lits_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_restart_def)

  have ‹vdom_m (all_init_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_restart_def all_atms_def[symmetric] all_init_atms_st_def)
  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_restart_def simp flip: all_init_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)›
    by (subst distinct_card[OF dist_vdom, symmetric])
      (use card_mono[OF _ vdom_incl] in auto)
  then show ‹length (watched_by x1 x2) ≤ length (get_clauses_wl_heur x1a)›
    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 twl_st_heur_restart_strong_aivdom :: ‹(isasat × nat twl_st_wl) set› where
[unfolded Let_def]: ‹twl_st_heur_restart_strong_aivdom =
  {(S, T).
  let M' = get_trail_wl_heur S; N' = get_clauses_wl_heur S; D' = get_conflict_wl_heur S;
    W' = get_watched_wl_heur S; j = literals_to_update_wl_heur S; outl = get_outlearned_heur S;
    cach = get_conflict_cach S; clvls = get_count_max_lvls_heur S;
    vm = get_vmtf_heur S;
    vdom = get_aivdom S; heur = get_heur S; old_arena = get_old_arena S;
    lcount = get_learned_count S; occs = get_occs S in
    let M = get_trail_wl T; N = get_clauses_wl T;  D = get_conflict_wl T;
      Q = literals_to_update_wl T;
      W = get_watched_wl T; N0 = get_init_clauses0_wl T; U0 = get_learned_clauses0_wl T;
      NS = get_subsumed_init_clauses_wl T; US = get_subsumed_learned_clauses_wl T;
      NEk = get_kept_unit_init_clss_wl T; UEk = get_kept_unit_learned_clss_wl T;
      NE = get_unkept_unit_init_clss_wl T; UE = get_unkept_unit_learned_clss_wl T in
    (M', M) ∈ trail_pol (all_init_atms N (NE+NEk+NS+N0)) ∧
    valid_arena N' N (set (get_vdom_aivdom vdom)) ∧
    (D', D) ∈ option_lookup_clause_rel (all_init_atms N (NE+NEk+NS+N0)) ∧
    (D = None ⟶ j ≤ length M) ∧
    Q = uminus `# lit_of `# mset (drop j (rev M)) ∧
    (W', W) ∈ ⟨Id⟩map_fun_rel (D0 (all_init_atms N (NE+NEk+NS+N0))) ∧
    vm ∈ bump_heur (all_init_atms N (NE+NEk+NS+N0)) M ∧
    no_dup M ∧
    clvls ∈ counts_maximum_level M D ∧
    cach_refinement_empty (all_init_atms N (NE+NEk+NS+N0)) cach ∧
    out_learned M D outl ∧
    clss_size_corr_restart N NE {#} NEk UEk NS {#} N0 {#} lcount ∧
    vdom_m (all_init_atms N (NE+NEk+NS+N0)) W N ⊆ set (get_vdom_aivdom vdom) ∧
    aivdom_inv_strong_dec vdom (dom_m N) ∧
    isasat_input_bounded (all_init_atms N (NE+NEk+NS+N0)) ∧
    isasat_input_nempty (all_init_atms N (NE+NEk+NS+N0)) ∧
    old_arena = [] ∧
      heuristic_rel (all_init_atms N (NE+NEk+NS+N0)) heur ∧
    (occs, empty_occs_list (all_init_atms N (NE+NEk+NS+N0))) ∈ occurrence_list_ref
  }›

lemma isasat_GC_clauses_prog_wl:
  ‹(isasat_GC_clauses_prog_wl, cdcl_GC_clauses_prog_wl) ∈
   {(S, T). (S, T) ∈ twl_st_heur_restart ∧ learned_clss_count S ≤ u} →f
   ⟨{(S, T). (S, T) ∈ twl_st_heur_restart_strong_aivdom ∧ arena_is_packed (get_clauses_wl_heur S) (get_clauses_wl T) ∧
      learned_clss_count S ≤ u}⟩nres_rel›
  (is ‹_ ∈ ?T →f _›)
proof-
  have [refine0]: ‹⋀x1 x1a x1b x1c x1d x1e x2e x1f x1g x1h x1i x1j x1m x1n x1o x1p x2n x2o x1q
       x1r x1s x1t x1u x1v x1w x1x x1y x1z x1aa x1ab x2ab NS US NEk UEk stats S.
       (S,
        x1, x1a, x1b, x1c, x1d, NEk, UEk, NS, US, x1e, x2e)
       ∈ ?T ⟹
       valid_arena (get_clauses_wl_heur S) (x1a) (set (get_vdom S))›
     unfolding twl_st_heur_restart_def
     by auto
  have [refine0]: ‹⋀x1 x1a x1b x1c x1d x1e x2e x1f x1g x1h x1i x1j x1m x1n x1o x1p x2n x2o x1q
       x1r x1s x1t x1u x1v x1w x1x x1y x1z x1aa x1ab x2ab NS US N0 U0 NEk UEk S.
       (S,
        x1, x1a, x1b, x1c, x1d, NEk, UEk, NS, US, N0, U0, x1e, x2e)
       ∈ ?T ⟹
       isasat_input_bounded (all_init_atms x1a (x1c + NEk + NS + N0))›
     unfolding twl_st_heur_restart_def
     by (auto simp: all_init_atms_st_def)
  have [refine0]: ‹⋀x1 x1a x1b x1c x1d x1e x2e x1f x1g x1h x1i x1j x1m x1n x1o x1p x2n x2o x1q
       x1r x1s x1t x1u x1v x1w x1x x1y x1z x1aa x1ab x2ab NS US N0 U0 NEk UEk S.
       (S,
        x1, x1a, x1b, x1c, x1d, NEk, UEk,NS, US, N0, U0, x1e, x2e)
       ∈ ?T ⟹
       vdom_m (all_init_atms x1a (x1c+NEk+NS+N0)) x2e x1a ⊆ set (get_vdom S)›
     unfolding twl_st_heur_restart_def
     by auto
  have [refine0]: ‹⋀x1 x1a x1b x1c x1d x1e x2e x1f x1g x1h x1i x1j x1m x1n x1o x1p x2n x2o x1q
       x1r x1s x1t x1u x1v x1w x1x x1y x1z x1aa x1ab x2ab NS US N0 U0 NEk UEk S.
       (S,
        x1, x1a, x1b, x1c, x1d, NEk, UEk,NS, US, N0, U0, x1e, x2e)
       ∈ ?T ⟹
       all_init_atms x1a (x1c+NEk+NS+N0) ≠ {#}›
     unfolding twl_st_heur_restart_def
     by auto
  have [refine0]: ‹⋀a b c x1 x1a x1b x1c x1d x1e x2e x1f x1g x1h x1i x1j x1m x1n x1o x1p x2n x2o x1q
       x1r x1s x1t x1u x1v x1w x1x x1y x1z x1aa x1ab x2ab NS US N0 U0 NEk UEk S.
       (S, x1, x1a, x1b, x1c, x1d, NEk, UEk, NS, US, N0, U0, x1e, x2e) ∈ ?T ⟹
       get_vmtf_heur S ∈ bump_heur (all_init_atms x1a (x1c+NEk+NS+N0)) x1›
       ‹⋀x1 x1a x1b x1c x1d x1e x2e x1f x1g x1h x1i x1j x1m x1n x1o x1p x2n x2o x1q
       x1r x1s x1t x1u x1v x1w x1x x1y x1z x1aa x1ab x2ab NS US N0 U0 NEk UEk S.
       (S,
        x1, x1a, x1b, x1c, x1d, NEk, UEk, NS, US, N0, U0, x1e, x2e)
       ∈ ?T ⟹ (get_watched_wl_heur S, x2e) ∈ ⟨Id⟩map_fun_rel (D0 (all_init_atms x1a (x1c+NEk+NS+N0)))›
    unfolding twl_st_heur_restart_def distinct_atoms_rel_def distinct_hash_atoms_rel_def
      all_init_atms_st_def
    by (case_tac ‹get_vmtf_heur S›; auto; fail)+
  have H: ‹vdom_m (all_init_atms x1a x1c) x2ad x1ad ⊆ set x2af›
    if
       empty: ‹∀A∈#all_init_atms x1a x1c. x2ad (Pos A) = [] ∧ x2ad (Neg A) = []› and
      rem: ‹GC_remap** (x1a, Map.empty, fmempty) (fmempty, m, x1ad)› and
      ‹dom_m x1ad = mset x2af›
    for m :: ‹nat ⇒ nat option› and y :: ‹nat literal multiset› and x :: ‹nat› and
      x1 x1a x1b x1c x1d x1e x2e x1f x1g x1h x1i x1j x1m x1n x1o x1p x2n x2o x1q
         x1r x1s x1t x1u x1v x1w x1x x1y x1z x1aa x1ab x2ab x1ac x1ad x2ad x1ae
         x1ag x2af x2ag
  proof -
    have ‹xa ∈# ℒall (all_init_atms x1a x1c) ⟹ x2ad xa = []› for xa
      using empty by (cases xa) (auto simp: in_ℒall_atm_of_𝒜in)
    then show ?thesis
      using ‹dom_m x1ad = mset x2af›
      by (auto simp: vdom_m_def)
  qed
  have H': ‹mset x2ag ⊆# mset x1ah ⟹ x ∈ set x2ag ⟹ x ∈ set x1ah› for x2ag x1ah x
    by (auto dest: mset_eq_setD)
  have [iff]: ‹ (∃UEa :: 'v clauses. size UE = size UEa)› for UE :: ‹'v clauses›
    by auto
  show ?thesis
    supply [[goals_limit=1]]
    unfolding isasat_GC_clauses_prog_wl_def cdcl_GC_clauses_prog_wl_alt_def take_0 Let_def
    apply (intro frefI nres_relI)
    apply (refine_vcg isasat_GC_clauses_prog_wl2[where 𝒜 = ‹all_init_atms _ _›]; remove_dummy_vars)
    subgoal
      by (clarsimp simp add: twl_st_heur_restart_def
        cdcl_GC_clauses_prog_wl_inv_def H H'
        rtranclp_GC_remap_all_init_atms
        rtranclp_GC_remap_learned_clss_l)
    subgoal
      unfolding cdcl_GC_clauses_pre_wl_def mem_Collect_eq prod.simps
        no_lost_clause_in_WL_alt_def
      apply normalize_goal+
      by (drule length_watched_le''')
        (clarsimp_all simp add: twl_st_heur_restart_def
          cdcl_GC_clauses_prog_wl_inv_def H H'
          rtranclp_GC_remap_all_init_atms all_init_atms_st_def
        rtranclp_GC_remap_learned_clss_l
        dest!: )
    subgoal
      by (clarsimp simp add: twl_st_heur_restart_def twl_st_heur_restart_strong_aivdom_def clss_size_corr_restart_def
        cdcl_GC_clauses_prog_wl_inv_def H H' clss_size_def
        rtranclp_GC_remap_all_init_atms learned_clss_count_def aivdom_inv_dec_def
        rtranclp_GC_remap_learned_clss_l)
    done
qed

definition cdcl_remap_st :: ‹'v twl_st_wl ⇒ 'v twl_st_wl nres› where
‹cdcl_remap_st = (λ(M, N0, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, WS).
  SPEC (λ(M', N', D', NE', UE', NEk', UEk', NS', US', N0', U0', Q', WS').
         (M', D', NE', UE', NEk', UEk', NS', US', N0', U0', Q') = (M, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q) ∧
         (∃m. GC_remap** (N0, (λ_. None), fmempty) (fmempty, m, N')) ∧
         0 ∉# dom_m N'))›

lemma cdcl_GC_clauses_wl_D_alt_def:
  ‹cdcl_GC_clauses_wl = (λS. do {
    ASSERT(cdcl_GC_clauses_pre_wl S);
    let b = True;
    if b then do {
      S ← cdcl_remap_st S;
      S ← rewatch_spec S;
      RETURN S
    }
    else remove_all_learned_subsumed_clauses_wl S})›
  supply [[goals_limit=1]]
  unfolding cdcl_GC_clauses_wl_def
  by (fastforce intro!: ext simp: RES_RES_RETURN_RES2 cdcl_remap_st_def RES_RES13_RETURN_RES_bound
      RES_RES11_RETURN_RES uncurry_def image_iff
      RES_RETURN_RES_RES2 RES_RETURN_RES RES_RES2_RETURN_RES rewatch_spec_def
      rewatch_spec_def remove_all_learned_subsumed_clauses_wl_def
      literals_are_ℒin'_empty blits_in_ℒin'_restart_wl_spec0'
      all_init_lits_alt_def[symmetric]
    intro!: bind_cong_nres intro: literals_are_ℒin'_empty)

lemma cdcl_GC_clauses_prog_wl2_st:
  assumes ‹(T, S) ∈ state_wl_l None›
  ‹cdcl_GC_clauses_pre S ∧
    no_lost_clause_in_WL T ∧
    literals_are_ℒin' T› and
    ‹get_clauses_wl T = N0'›
  shows
    ‹cdcl_GC_clauses_prog_wl T ≤
       ⇓ {((M', N'', D', NE', UE', NEk', UEk', NS', US', N0', U0', Q', WS'), (N, N')).
       (M', D', NE', UE', NEk', UEk', NS', US', N0', U0', Q') = (get_trail_wl T, get_conflict_wl T, get_unkept_unit_init_clss_wl T,
           get_unkept_unit_learned_clss_wl T, get_kept_unit_init_clss_wl T,
           get_kept_unit_learned_clss_wl T, get_subsumed_init_clauses_wl T, get_subsumed_learned_clauses_wl T,
           get_init_clauses0_wl T, get_learned_clauses0_wl T,
           literals_to_update_wl T) ∧ N'' = N ∧
           (∀L∈#all_init_lits_of_wl T. WS' L = []) ∧
           all_init_lits_of_wl T = all_init_lits N (NE'+NEk'+NS'+N0') ∧
           (∃m. GC_remap** (get_clauses_wl T, Map.empty, fmempty)
               (fmempty, m, N))}
      (SPEC(λ(N'::(nat, 'a literal list × bool) fmap, m).
         GC_remap** (N0', (λ_. None), fmempty) (fmempty, m, N') ∧
    0 ∉# dom_m N'))›
  using assms apply -
  apply (rule order_trans)
  apply (rule order_trans)
    prefer 2
  apply (rule cdcl_GC_clauses_prog_wl2[of ‹get_trail_wl T› ‹get_clauses_wl T› ‹get_conflict_wl T›
    ‹get_unkept_unit_init_clss_wl T› ‹get_unkept_unit_learned_clss_wl T›
    ‹get_kept_unit_init_clss_wl T› ‹get_kept_unit_learned_clss_wl T›  ‹get_subsumed_init_clauses_wl T›
    ‹get_subsumed_learned_clauses_wl T› ‹get_init_clauses0_wl T› ‹get_learned_clauses0_wl T› ‹literals_to_update_wl T›
    ‹get_watched_wl T› S N0'])
  apply (cases T; auto simp: all_init_atms_st_def; fail)+
  apply (auto 5 3 simp: all_init_lits_of_wl_def all_init_lits_def ac_simps
      get_unit_init_clss_wl_alt_def
    dest: rtranclp_GC_remap_init_clss_l_old_new intro!: RES_refine)
  done

abbreviation isasat_GC_clauses_rel where
  ‹isasat_GC_clauses_rel y u ≡ {(S, T). (S, T) ∈ twl_st_heur_restart_strong_aivdom ∧
           (∀L∈#all_init_lits_of_wl y. get_watched_wl T L = [])∧
           get_trail_wl T = get_trail_wl y ∧
           get_conflict_wl T = get_conflict_wl y ∧
           get_unkept_unit_init_clss_wl T = get_unkept_unit_init_clss_wl y ∧
           get_kept_unit_init_clss_wl T = get_kept_unit_init_clss_wl y ∧
           get_unkept_unit_learned_clss_wl T = get_unkept_unit_learned_clss_wl y ∧
           get_kept_unit_learned_clss_wl T = get_kept_unit_learned_clss_wl y ∧
           get_subsumed_init_clauses_wl T = get_subsumed_init_clauses_wl y ∧
           get_subsumed_learned_clauses_wl T = get_subsumed_learned_clauses_wl y ∧
           get_init_clauses0_wl T = get_init_clauses0_wl y ∧
           get_learned_clauses0_wl T = get_learned_clauses0_wl y ∧
           learned_clss_count S ≤ u ∧
           (∃m. GC_remap** (get_clauses_wl y, (λ_. None), fmempty) (fmempty, m, get_clauses_wl T)) ∧
           arena_is_packed (get_clauses_wl_heur S) (get_clauses_wl T)}›


lemma isasat_GC_clauses_prog_wl_cdcl_remap_st:
  assumes
    ‹(x, y) ∈ twl_st_heur_restart'''u r u› and
    ‹cdcl_GC_clauses_pre_wl y›
  shows ‹isasat_GC_clauses_prog_wl x ≤ ⇓ (isasat_GC_clauses_rel y u) (cdcl_remap_st y)›
proof -
  have xy: ‹(x, y) ∈ {(S, T). (S, T) ∈ twl_st_heur_restart ∧ learned_clss_count S ≤ u}›
    using assms(1) by auto
  have H: ‹isasat_GC_clauses_rel y u=
    {(S, T). (S, T) ∈ twl_st_heur_restart_strong_aivdom ∧ arena_is_packed (get_clauses_wl_heur S) (get_clauses_wl T) ∧ 
           learned_clss_count S ≤ u} O
    {(S, T). S = T ∧ (∀L∈#all_init_lits_of_wl y. get_watched_wl T L = [])∧
           get_trail_wl T = get_trail_wl y ∧
           get_conflict_wl T = get_conflict_wl y ∧
           get_unkept_unit_init_clss_wl T = get_unkept_unit_init_clss_wl y ∧
           get_kept_unit_init_clss_wl T = get_kept_unit_init_clss_wl y ∧
           get_unkept_unit_learned_clss_wl T = get_unkept_unit_learned_clss_wl y ∧
           get_kept_unit_learned_clss_wl T = get_kept_unit_learned_clss_wl y ∧
           get_subsumed_init_clauses_wl T = get_subsumed_init_clauses_wl y ∧
           get_subsumed_learned_clauses_wl T = get_subsumed_learned_clauses_wl y ∧
           get_init_clauses0_wl T = get_init_clauses0_wl y ∧
           get_learned_clauses0_wl T = get_learned_clauses0_wl y ∧
           (∃m. GC_remap** (get_clauses_wl y, (λ_. None), fmempty) (fmempty, m, get_clauses_wl T))}›
    by blast
  show ?thesis
    using assms apply -
    apply (rule order_trans[OF isasat_GC_clauses_prog_wl[THEN fref_to_Down]])
    subgoal by fast
    apply (rule xy)
    unfolding conc_fun_chain[symmetric] H
    apply (rule ref_two_step')
    unfolding cdcl_GC_clauses_pre_wl_def
    apply normalize_goal+
    apply (rule order_trans[OF cdcl_GC_clauses_prog_wl2_st])
    apply assumption
    subgoal for xa
      using assms(2) by (simp add: correct_watching'_nobin_clauses_pointed_to
        cdcl_GC_clauses_pre_wl_def)
    apply (rule refl)
    subgoal by (auto simp: cdcl_remap_st_def conc_fun_RES split: prod.splits)
    done
qed

inductive_cases GC_remapE: ‹GC_remap (a, aa, b) (ab, ac, ba)›
lemma rtranclp_GC_remap_ran_m_remap:
  ‹GC_remap** (old, m, new) (old', m', new')  ⟹ C ∈# dom_m old ⟹ C ∉# dom_m old' ⟹
         m' C ≠ None ∧
         fmlookup new' (the (m' C)) = fmlookup old C›
  apply (induction rule: rtranclp_induct[of r ‹(_, _, _)› ‹(_, _, _)›, split_format(complete), of for r])
  subgoal by auto
  subgoal for a aa b ab ac ba
    apply (cases ‹C ∉# dom_m a›)
    apply (auto dest: GC_remap_ran_m_remap GC_remap_ran_m_no_rewrite_map
       GC_remap_ran_m_no_rewrite)
    apply (metis GC_remap_ran_m_no_rewrite_fmap GC_remap_ran_m_no_rewrite_map in_dom_m_lookup_iff option.sel)
    using GC_remap_ran_m_remap rtranclp_GC_remap_ran_m_no_rewrite by fastforce
  done

lemma GC_remap_ran_m_exists_earlier:
  ‹GC_remap (old, m, new) (old', m', new')  ⟹ C ∈# dom_m new' ⟹ C ∉# dom_m new ⟹
         ∃D. m' D = Some C ∧ D ∈# dom_m old ∧
         fmlookup new' C = fmlookup old D›
  by (induction rule: GC_remap.induct[split_format(complete)]) auto


lemma rtranclp_GC_remap_ran_m_exists_earlier:
  ‹GC_remap** (old, m, new) (old', m', new')  ⟹ C ∈# dom_m new' ⟹ C ∉# dom_m new ⟹
         ∃D. m' D = Some C ∧ D ∈# dom_m old ∧
         fmlookup new' C = fmlookup old D›
  apply (induction rule: rtranclp_induct[of r ‹(_, _, _)› ‹(_, _, _)›, split_format(complete), of for r])
  apply (auto dest: GC_remap_ran_m_exists_earlier)
  apply (case_tac ‹C ∈# dom_m b›)
  apply (auto elim!: GC_remapE split: if_splits)
  apply blast
  using rtranclp_GC_remap_ran_m_no_new_map rtranclp_GC_remap_ran_m_no_rewrite
  by (metis fst_conv)


lemma watchlist_put_binaries_first_one_correct_watching:
  assumes ‹∃W'. correct_watching''' ℬ (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W') ∧ (W,W') ∈ ⟨Id⟩map_fun_rel (D0 𝒜)› ‹L < length W›
  shows ‹watchlist_put_binaries_first_one W L ≤ ⇓{(a,b). (a,b)∈⟨Id⟩map_fun_rel (D0 𝒜) ∧ length a = length W ∧ (∀K. mset (a ! K) = mset (W ! K))} (SPEC (λW. correct_watching''' ℬ (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W)))›
proof -
  obtain W' where W': ‹correct_watching''' ℬ(M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W') ∧ (W,W') ∈ ⟨Id⟩map_fun_rel (D0 𝒜)›
    using assms by fast
  let ?R = ‹measure (λ(i, j, _). length (W ! L) - i)›
  have R[refine]: ‹wf ?R›
    by auto
  have H: ‹(∀K. mset (Wa ! K) = mset (W ! K)) ⟷ (∀K. mset (Wa ! K) = mset (W ! K)) ∧ (∀K. set (Wa ! K) = set (W ! K)) ∧ 
   (∀K. distinct_watched (Wa ! K) ⟷ distinct_watched (W ! K))› for W Wa
   by (auto dest: mset_eq_setD simp del: distinct_mset_mset_distinct
    simp flip: distinct_mset_mset_distinct)

  show ?thesis
    using assms(2) W'
    unfolding watchlist_put_binaries_first_one_def conc_fun_SPEC apply -
    apply (refine_vcg )
    subgoal by auto
    subgoal by auto
    subgoal by auto
    subgoal by auto
    subgoal by auto
    subgoal by auto
    subgoal by (auto simp: nth_list_update)
    subgoal by auto
    subgoal by auto
    subgoal by auto
    subgoal by auto
    subgoal by auto
    subgoal by auto
    subgoal by auto
    subgoal by auto
    subgoal for s a b aa ba
      apply (subst (asm) H)
      apply (rule_tac x= ‹λL. if L ∈#ℒall 𝒜 then ba ! nat_of_lit L else W' L› in exI)
      apply (auto simp: correct_watching'''.simps all_blits_are_in_problem_init.simps 
        map_fun_rel_def dest: mset_eq_setD split: if_splits)
      done
    done
qed

lemma watchlist_put_binaries_first:
  assumes ‹correct_watching''' ℬ (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W')›
    ‹(W,W') ∈ ⟨Id⟩map_fun_rel (D0 𝒜)›
  shows ‹watchlist_put_binaries_first W ≤ ⇓(⟨Id⟩map_fun_rel (D0 𝒜)) (SPEC (λW. correct_watching''' ℬ (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W)))›
proof -
  let ?R = ‹measure (λ(i, _). length W - i)›
  have [refine]: ‹wf ?R›
    by auto
  note [refine_vcg del] = WHILEIT_rule
  show ?thesis
    unfolding watchlist_put_binaries_first_def conc_fun_SPEC apply -
    apply (refine_vcg
          watchlist_put_binaries_first_one_correct_watching[where 𝒜=𝒜 and ℬ=ℬ and M=M and
          N=N and D=D and NE=NE and UE=UE and NEk=NEk and UEk=UEk and NS=NS and US=US
          and N0=N0 and U0=U0 and Q=Q, THEN order_trans]
      WHILEIT_rule_stronger_inv[where
      I' = ‹λ(i, W). ∃W'. (W,W')∈⟨Id⟩map_fun_rel (D0 𝒜)∧
        correct_watching''' ℬ (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W')›])
    subgoal by auto
    subgoal by auto
    subgoal using assms by fast
    subgoal by auto
    subgoal by fast
    subgoal by (auto simp: conc_fun_RES)
    subgoal by fast
    done
qed

lemma rewatch_heur_st_correct_watching:
  assumes
    pre: ‹cdcl_GC_clauses_pre_wl y› and
    S_T: ‹(S, T) ∈ isasat_GC_clauses_rel y u›
  shows ‹rewatch_heur_and_reorder_st (empty_US_heur S) ≤ ⇓ (twl_st_heur_restart'''u (length (get_clauses_wl_heur S)) u)
    (rewatch_spec (T))›
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) auto
  let ?vdom = ‹get_aivdom S›
  let ?N' = ‹get_clauses_wl_heur S›
  let ?W' = ‹get_watched_wl_heur S›

  have
    valid: ‹valid_arena ?N' N (set (get_vdom_aivdom ?vdom))› and
    W: ‹(?W', W) ∈ ⟨Id⟩map_fun_rel (D0 (all_init_atms_st T))› and
    empty: ‹⋀L. L ∈# all_init_lits_of_wl y ⟹ W L = []› and
    NUE:‹get_unkept_unit_init_clss_wl y = NE ›
      ‹get_unkept_unit_learned_clss_wl y = UE›
      ‹get_kept_unit_init_clss_wl y = NEk›
      ‹get_kept_unit_learned_clss_wl y = UEk›
      ‹get_trail_wl y = M›
      ‹get_subsumed_init_clauses_wl y = NS›
      ‹get_subsumed_learned_clauses_wl y = US›
      ‹get_init_clauses0_wl y = N0›
      ‹get_learned_clauses0_wl y = U0› and
    avdom:  ‹aivdom_inv_strong_dec (?vdom) (dom_m N)› and
    tvdom: ‹get_tvdom_aivdom ?vdom = get_vdom_aivdom ?vdom›
    using assms by (auto simp: twl_st_heur_restart_strong_aivdom_def T all_init_atms_st_def
      aivdom_inv_strong_dec_alt_def)
  have
    dist: ‹distinct (get_vdom_aivdom ?vdom)› and
    dom_m_vdom: ‹set_mset (dom_m N) ⊆ set (get_vdom_aivdom ?vdom)›
    using avdom valid unfolding aivdom_inv_strong_dec_alt_def
      apply (cases ?vdom; cases ‹IsaSAT_VDom.get_aivdom ?vdom›; use avdom in auto)
      apply (cases ?vdom; cases ‹IsaSAT_VDom.get_aivdom ?vdom›; use avdom valid in ‹auto simp: aivdom_inv_strong_dec_alt_def
        simp del: distinct_finite_set_mset_subseteq_iff›)
      by (metis (no_types, opaque_lifting) UnE mset_subset_eqD set_mset_mset subsetD)

  obtain m where
    m: ‹GC_remap** (get_clauses_wl y, Map.empty, fmempty)
             (fmempty, m, N)›
    using assms by (auto simp: twl_st_heur_restart_def T)
  obtain x xa xb where
    y_x: ‹(y, x) ∈ Id› ‹x = y› and
    lits_y: ‹literals_are_ℒin' y› and
    x_xa: ‹(x, xa) ∈ state_wl_l None› and
    ‹no_lost_clause_in_WL x› and
    xa_xb: ‹(xa, xb) ∈ twl_st_l None› and
    ‹twl_list_invs xa› and
    struct_invs: ‹twl_struct_invs xb› and
    ‹get_conflict_l xa = None› and
    ‹clauses_to_update_l xa = {#}› and
    ‹count_decided (get_trail_l xa) = 0› and
    ‹∀L∈set (get_trail_l xa). mark_of L = 0›
    using pre
    unfolding cdcl_GC_clauses_pre_wl_def
      cdcl_GC_clauses_pre_def
    by blast
  have [iff]:
    ‹distinct_mset (mset (watched_l C) + mset (unwatched_l C)) ⟷ distinct C› for C
    unfolding mset_append[symmetric]
    by auto

  have ‹twl_st_inv xb›
    using xa_xb struct_invs
    by (auto simp: twl_struct_invs_def
      cdclW_restart_mset.cdclW_all_struct_inv_def)
  then have A:
    ‹⋀C. C ∈# dom_m (get_clauses_wl x) ⟹ distinct (get_clauses_wl x ∝ C) ∧ 2 ≤ length (get_clauses_wl x ∝ C)›
    using xa_xb x_xa
    by (cases x; cases ‹irred (get_clauses_wl x) C›)
      (auto simp: twl_struct_invs_def twl_st_inv.simps
        twl_st_l_def state_wl_l_def ran_m_def conj_disj_distribR
        Collect_disj_eq Collect_conv_if
      dest!: multi_member_split
      split: if_splits)
  have struct_wf:
    ‹C ∈# dom_m N ⟹ distinct (N ∝ C) ∧ 2 ≤ length (N ∝ C)› for C
    using rtranclp_GC_remap_ran_m_exists_earlier[OF m, of ‹C›] A y_x
    by (auto simp: T dest: )

  have eq_UnD: ‹A = A' ∪ A'' ⟹ A' ⊆ A› for A A' A''
      by blast

  have eq3: ‹all_init_lits_of_wl y = all_init_lits N (NE+NEk+NS+N0)›
    using rtranclp_GC_remap_init_clss_l_old_new[OF m] NUE
    by (auto simp: all_init_lits_def all_init_lits_of_wl_def ac_simps
      get_unit_init_clss_wl_alt_def)
  moreover have ‹all_lits_st y = all_lits_st T›
    using rtranclp_GC_remap_init_clss_l_old_new[OF m] rtranclp_GC_remap_learned_clss_l_old_new[OF m]
      NUE
      apply (cases y)
    apply (auto simp: all_init_lits_def T NUE all_lits_def all_lits_st_def)
    by (metis all_clss_l_ran_m all_lits_def)
  moreover have ‹set_mset (all_init_lits_of_wl y) = set_mset (all_lits_st T)›
    by (smt ‹⋀thesis. (⋀x xa xb. ⟦(y, x) ∈ Id; x = y; literals_are_ℒin' y; (x, xa) ∈ state_wl_l None; no_lost_clause_in_WL x; (xa, xb) ∈ twl_st_l None; twl_list_invs xa; twl_struct_invs xb; get_conflict_l xa = None; clauses_to_update_l xa = {#}; count_decided (get_trail_l xa) = 0; ∀L∈set (get_trail_l xa). mark_of L = 0⟧ ⟹ thesis) ⟹ thesis› calculation(2) literals_are_ℒin'_literals_are_ℒin_iff(4))
  ultimately have lits: ‹literals_are_in_ℒin_mm (all_init_atms_st (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W))
    (mset `# ran_mf N)›
    using literals_are_ℒin'_literals_are_ℒin_iff(3)[OF x_xa xa_xb struct_invs] lits_y
      rtranclp_GC_remap_init_clss_l_old_new[OF m]
      rtranclp_GC_remap_learned_clss_l_old_new[OF m]
    unfolding literals_are_in_ℒin_mm_def all_init_lits_alt_def[symmetric] ℒall_all_init_atms_all_init_lits
     all_init_atms_st_def
    by (auto simp: T all_lits_st_def all_lits_def all_lits_of_mm_union)

  have eq: ‹set_mset (ℒall (all_init_atms N (NE+NEk+NS+N0))) = set_mset (all_init_lits_of_wl y)›
    unfolding eq3 ℒall_all_init_atms_all_init_lits ..
  then have vd: ‹vdom_m (all_init_atms_st (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W)) W N ⊆ set_mset (dom_m N)›
    using empty dom_m_vdom
    by (auto simp: vdom_m_def all_init_atms_st_def)
  have ‹{#i ∈# clause_to_update L (M, N, get_conflict_wl y, NE, UE, NEk, UEk, NS, US, N0, U0, {#}, {#}).
         i ∈# dom_m N#} =
       {#i ∈# clause_to_update L (M, N, get_conflict_wl y, NE, UE, NEk, UEk, NS, US, N0, U0, {#}, {#}).
         True#}› for L
       by (rule filter_mset_cong2)  (auto simp: clause_to_update_def)
  then have corr2: ‹correct_watching'''
        ({#mset (fst x). x ∈# init_clss_l (get_clauses_wl y)#} + NE+NEk + NS+N0)
        (M, N, get_conflict_wl y, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W'a) ⟹
       correct_watching' (M, N, get_conflict_wl y, NE, UE,NEk, UEk, NS, US, N0, U0, Q, W'a)› for W'a
     using rtranclp_GC_remap_init_clss_l_old_new[OF m]
     by (auto simp: correct_watching'''.simps correct_watching'.simps all_init_lits_of_wl_def
       ac_simps)
  have eq2: ‹all_init_lits (get_clauses_wl y) (NE+NEk+NS+N0) = all_init_lits N (NE+NEk+NS+N0)›
    using rtranclp_GC_remap_init_clss_l_old_new[OF m]
    by (auto simp: T all_init_lits_def NUE
      ℒall_all_init_atms_all_init_lits)
  have ‹i ∈# dom_m N ⟹ set (N ∝ i) ⊆ set_mset (all_init_lits N (NE+NEk+NS+N0))› for i
    using lits by (auto dest!: multi_member_split split_list
      simp: literals_are_in_ℒin_mm_def ran_m_def all_init_atms_st_def
        all_lits_of_mm_add_mset all_lits_of_m_add_mset
        ℒall_all_init_atms_all_init_lits)
  then have blit2: ‹correct_watching'''
        ({#mset x. x ∈# init_clss_lf (get_clauses_wl y)#} + NE + NEk + NS + N0)
        (M, N, get_conflict_wl y, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W'a) ⟹
        blits_in_ℒin' (M, N, get_conflict_wl y, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W'a)› for W'a
      using rtranclp_GC_remap_init_clss_l_old_new[OF m]
      unfolding  correct_watching'''.simps  blits_in_ℒin'_def eq2
        ℒall_all_init_atms_all_init_lits all_init_lits_alt_def[symmetric] all_init_lits_of_wl_def
      by (fastforce simp add: all_init_lits_def blits_in_ℒin'_def ac_simps
        get_unit_init_clss_wl_alt_def NUE dest!: multi_member_split)
  have ‹correct_watching'''
        ({#mset x. x ∈# init_clss_lf (get_clauses_wl y)#} + (NE+NEk + NS+N0))
        (M, N, get_conflict_wl y, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W'a) ⟹
        vdom_m (all_init_atms N (NE+NEk+NS+N0)) W'a N ⊆ set_mset (dom_m N)› for W'a
      using rtranclp_GC_remap_init_clss_l_old_new[OF m]
      unfolding  correct_watching'''.simps  blits_in_ℒin'_def eq2
        ℒall_all_init_atms_all_init_lits all_init_lits_alt_def[symmetric]
      by (auto simp add: all_init_lits_def blits_in_ℒin'_def vdom_m_def NUE all_init_atms_def
          ℒall_atm_of_all_lits_of_mm
        simp flip: all_lits_st_alt_def
        dest!: multi_member_split)
    then have st:
      ‹(x, W'a) ∈ ⟨Id⟩map_fun_rel (D0 (all_init_atms_st (M, N, get_conflict_wl y, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W))) ⟹
     correct_watching'''
         ({#mset x. x ∈# init_clss_lf (get_clauses_wl y)#} +  (NE + (NEk + (NS + N0))))
        (M, N, get_conflict_wl y, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W'a) ⟹
      (set_watched_wl_heur x 
       (set_learned_count_wl_heur (clss_size_resetUS0 (get_learned_count S)) S),
        M, N, get_conflict_wl y, NE, {#}, NEk, UEk, NS, {#}, N0, {#}, Q, W'a)
       ∈ twl_st_heur_restart› for W'a m x
      using S_T dom_m_vdom
      by (auto simp: T twl_st_heur_restart_def all_init_atms_st_def y_x NUE ac_simps
        twl_st_heur_restart_strong_aivdom_def aivdom_inv_strong_dec_def2)
  have Su: ‹learned_clss_count S ≤ u›
    using S_T by auto
  have truc: ‹xa ∈# all_learned_lits_of_wl (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W'a) ⟹
       xa ∈# all_init_lits_of_wl (M, N, D, NE, {#}, NEk, UEk, NS, {#}, N0, {#}, Q, W'a)› for W'a M D xa
    using lits_y eq3 rtranclp_GC_remap_learned_clss_l[OF m]
    unfolding literals_are_ℒin'_def all_init_lits_def NUE all_learned_lits_of_wl_def
      all_learned_lits_of_wl_def all_init_lits_of_wl_def
      all_lits_of_mm_union all_init_lits_def  ℒall_all_init_atms_all_init_lits
    by (auto simp: ac_simps all_lits_of_mm_union get_unit_init_clss_wl_alt_def
      NUE get_unit_learned_clss_wl_alt_def)

  show ?thesis
    supply [[goals_limit=1]]
    using assms
    unfolding rewatch_heur_st_def T empty_US_heur_def rewatch_heur_and_reorder_st_def rewatch_heur_and_reorder_def
      Let_def prod.case tvdom isasat_state_simp nres_monad3
    apply clarify
    apply (rule ASSERT_leI)
    subgoal by (auto dest!: valid_arena_vdom_subset simp: twl_st_heur_restart_strong_aivdom_def aivdom_inv_strong_dec_alt_def)
    apply (rule bind_refine_res)
    prefer 2
    apply (rule order.trans)
    apply (rule rewatch_heur_rewatch[OF valid _ dist dom_m_vdom W[unfolded T, simplified] lits])
    apply (solves simp)
    apply (rule vd)
    apply (rule order_trans[OF ref_two_step'])
    apply (rule rewatch_correctness[where M=M and N=N and NE=NE and UE=UE and C=D and Q=Q and
        NS=NS and US=US and N0=N0 and U0=U0 and UEk=UEk and NEk=NEk and W=W])
    apply (rule empty[unfolded all_init_lits_of_wl_def]; assumption)
    apply (rule struct_wf; assumption)
    subgoal using lits eq2 by (auto simp: literals_are_in_ℒin_mm_def all_init_atms_def all_init_lits_def
      ℒall_atm_of_all_lits_of_mm all_init_atms_st_def ac_simps get_unit_init_clss_wl_alt_def
       simp del: all_init_atms_def[symmetric])
    apply (subst conc_fun_RES)
    apply (rule order.refl)
    subgoal for m x
      apply clarify
      subgoal for W'
      apply (rule bind_refine_res)
        prefer 2
      apply (rule order.trans)
      apply (rule watchlist_put_binaries_first[where M=M and N=N and NE=NE and UE=UE and Q=Q and
        NS=NS and US=US and N0=N0 and U0=U0 and UEk=UEk and NEk=NEk and D=D and W= ‹x› and W'=W'
        and ℬ = ‹(mset `# get_init_clss_wl y + get_unit_init_clss_wl y +
        get_subsumed_init_clauses_wl y +
        get_init_clauses0_wl y)›])
      apply auto[2]
      apply (subst conc_fun_RES)
      apply (rule order.refl)
      apply clarify
      using Su
      apply (auto simp: rewatch_spec_def RETURN_RES_refine_iff NUE learned_clss_count_def
        literals_are_in_ℒin_mm_def literals_are_ℒin'_def add.assoc get_unit_init_clss_wl_alt_def
        intro: corr2 blit2 st dest: truc intro!: )
      apply (rule_tac x=xa in exI)
      apply (auto simp: rewatch_spec_def RETURN_RES_refine_iff NUE learned_clss_count_def
        literals_are_in_ℒin_mm_def literals_are_ℒin'_def add.assoc get_unit_init_clss_wl_alt_def
        intro: corr2 blit2 st dest: truc intro!: )
      done
    done
  done
qed

lemma GC_remap_dom_m_subset:
  ‹GC_remap (old, m, new) (old', m', new') ⟹ dom_m old' ⊆# dom_m old›
  by (induction rule: GC_remap.induct[split_format(complete)]) (auto dest!: multi_member_split)

lemma rtranclp_GC_remap_dom_m_subset:
  ‹rtranclp GC_remap (old, m, new) (old', m', new') ⟹ dom_m old' ⊆# dom_m old›
  apply (induction rule: rtranclp_induct[of r ‹(_, _, _)› ‹(_, _, _)›, split_format(complete), of for r])
  subgoal by auto
  subgoal for old1 m1 new1 old2 m2 new2
    using GC_remap_dom_m_subset[of old1 m1 new1 old2 m2 new2] by auto
  done

lemma GC_remap_mapping_unchanged:
  ‹GC_remap (old, m, new) (old', m', new') ⟹ C ∈ dom m ⟹ m' C = m C›
  by (induction rule: GC_remap.induct[split_format(complete)]) auto

lemma rtranclp_GC_remap_mapping_unchanged:
  ‹GC_remap** (old, m, new) (old', m', new') ⟹ C ∈ dom m ⟹ m' C = m C›
  apply (induction rule: rtranclp_induct[of r ‹(_, _, _)› ‹(_, _, _)›, split_format(complete), of for r])
  subgoal by auto
  subgoal for old1 m1 new1 old2 m2 new2
    using GC_remap_mapping_unchanged[of old1 m1 new1 old2 m2 new2, of C]
    by (auto dest: GC_remap_mapping_unchanged simp: dom_def intro!: image_mset_cong2)
  done


lemma GC_remap_mapping_dom_extended:
  ‹GC_remap (old, m, new) (old', m', new') ⟹ dom m' = dom m ∪ set_mset (dom_m old - dom_m old')›
  by (induction rule: GC_remap.induct[split_format(complete)]) (auto dest!: multi_member_split)

lemma rtranclp_GC_remap_mapping_dom_extended:
  ‹GC_remap** (old, m, new) (old', m', new') ⟹ dom m' = dom m ∪ set_mset (dom_m old - dom_m old')›
  apply (induction rule: rtranclp_induct[of r ‹(_, _, _)› ‹(_, _, _)›, split_format(complete), of for r])
  subgoal by auto
  subgoal for old1 m1 new1 old2 m2 new2
    using GC_remap_mapping_dom_extended[of old1 m1 new1 old2 m2 new2]
    GC_remap_dom_m_subset[of old1 m1 new1 old2 m2 new2]
    rtranclp_GC_remap_dom_m_subset[of old m new old1 m1 new1]
    by (auto dest: GC_remap_mapping_dom_extended simp: dom_def mset_subset_eq_exists_conv)
  done

lemma GC_remap_dom_m:
  ‹GC_remap (old, m, new) (old', m', new') ⟹ dom_m new' = dom_m new + the `# m' `# (dom_m old - dom_m old')›
  by (induction rule: GC_remap.induct[split_format(complete)]) (auto dest!: multi_member_split)

lemma rtranclp_GC_remap_dom_m:
  ‹rtranclp GC_remap (old, m, new) (old', m', new') ⟹ dom_m new' = dom_m new + the `# m' `# (dom_m old - dom_m old')›
  apply (induction rule: rtranclp_induct[of r ‹(_, _, _)› ‹(_, _, _)›, split_format(complete), of for r])
  subgoal by auto
  subgoal for old1 m1 new1 old2 m2 new2
    using GC_remap_dom_m[of old1 m1 new1 old2 m2 new2] GC_remap_dom_m_subset[of old1 m1 new1 old2 m2 new2]
    rtranclp_GC_remap_dom_m_subset[of old m new old1 m1 new1]
    GC_remap_mapping_unchanged[of old1 m1 new1 old2 m2 new2]
    rtranclp_GC_remap_mapping_dom_extended[of old m new old1 m1 new1]
    by (auto dest: simp: mset_subset_eq_exists_conv intro!: image_mset_cong2)
  done

lemma isasat_GC_clauses_rel_packed_le:
  assumes
    xy: ‹(x, y) ∈ twl_st_heur_restart''' r› and
    ST: ‹(S, T) ∈ isasat_GC_clauses_rel y u›
  shows ‹length (get_clauses_wl_heur S) ≤ length (get_clauses_wl_heur x)› and
     ‹∀C ∈ set (get_tvdom S). C < length (get_clauses_wl_heur x)›
proof -
  obtain m where
    ‹(S, T) ∈ twl_st_heur_restart_strong_aivdom› and
    ‹∀L∈#all_init_lits_of_wl y. get_watched_wl T L = []› and
    ‹get_trail_wl T = get_trail_wl y› and
    ‹get_conflict_wl T = get_conflict_wl y› and
    ‹get_kept_unit_init_clss_wl T = get_kept_unit_init_clss_wl y› and
    ‹get_kept_unit_learned_clss_wl T = get_kept_unit_learned_clss_wl y› and
    ‹get_unkept_unit_init_clss_wl T = get_unkept_unit_init_clss_wl y› and
    ‹get_unkept_unit_learned_clss_wl T = get_unkept_unit_learned_clss_wl y› and
    remap: ‹GC_remap** (get_clauses_wl y, Map.empty, fmempty)
      (fmempty, m, get_clauses_wl T)› and
    packed: ‹arena_is_packed (get_clauses_wl_heur S) (get_clauses_wl T)›
     using ST by auto
  have ‹valid_arena (get_clauses_wl_heur x) (get_clauses_wl y) (set (get_vdom x))›
    using xy unfolding twl_st_heur_restart_def by (cases x; cases y) auto
  from valid_arena_ge_length_clauses[OF this]
  have ‹(∑C∈#dom_m (get_clauses_wl  y). length (get_clauses_wl y ∝ C) +
              header_size (get_clauses_wl y ∝ C)) ≤ length (get_clauses_wl_heur x)›
   (is ‹?A ≤ _›) .
  moreover have ‹?A = (∑C∈#dom_m (get_clauses_wl T). length (get_clauses_wl T ∝ C) +
              header_size (get_clauses_wl T ∝ C))›
    using rtranclp_GC_remap_ran_m_remap[OF remap]
    by (auto simp: rtranclp_GC_remap_dom_m[OF remap] intro!: sum_mset_cong)
  ultimately show le: ‹length (get_clauses_wl_heur S) ≤ length (get_clauses_wl_heur x)›
    using packed unfolding arena_is_packed_def by simp

  have ‹valid_arena (get_clauses_wl_heur S) (get_clauses_wl T) (set (get_vdom S))›
    using ST unfolding twl_st_heur_restart_strong_aivdom_def by (cases S; cases T) auto
  moreover have ‹set (get_tvdom S) ⊆ set (get_vdom S)›
    using ST by (auto simp: twl_st_heur_restart_strong_aivdom_def
      aivdom_inv_strong_dec_alt_def)
  ultimately show ‹∀C ∈ set (get_tvdom S). C < length (get_clauses_wl_heur x)›
    using le
    by (auto dest: valid_arena_in_vdom_le_arena)
qed

lemma isasat_GC_clauses_wl_D:
  ‹(isasat_GC_clauses_wl_D b, cdcl_GC_clauses_wl)
    ∈ twl_st_heur_restart'''u r u →f ⟨twl_st_heur_restart''''u r u⟩nres_rel›
  apply (intro frefI nres_relI)
  unfolding prod_rel_fst_snd_iff
    isasat_GC_clauses_wl_D_def cdcl_GC_clauses_wl_D_alt_def uncurry_def
  apply (refine_vcg isasat_GC_clauses_prog_wl_cdcl_remap_st[where r=r]
    rewatch_heur_st_correct_watching)
  subgoal unfolding isasat_GC_clauses_pre_wl_D_def by blast
  subgoal by fast
  apply assumption
  subgoal by (rule isasat_GC_clauses_rel_packed_le) fast+
  subgoal by (rule isasat_GC_clauses_rel_packed_le(2)) fast+
  apply assumption+
  subgoal by (auto)
  subgoal by (auto)
  done

end