Theory CDCL.Pragmatic_CDCL_Restart

theory Pragmatic_CDCL_Restart
imports Pragmatic_CDCL
begin

section ‹Restarts›
text ‹

  While refactoring the code (or more precisely, creating the PCDCL version with restarts), I
  realised that the restarts as specified in my thesis are not exactly as I want to have them and
  not how they are implemented in SAT solvers. The problem is that I introduced both restart and
  garbage collection at the same time, but they have a different termination criterion:

    ▪ Restarts are always applicable as long you have learned at least one clause since the last
    restart.
    ▪ GC must be applied after longer and longer time intervals.


  In the version from the thesis, I use the second criterion to justify termination for both
  criteria. Due to the implementation, it did not really make a difference for small number of
  conflicts, but limited the ability to restart after many conflicts have been generated. I don't
  know if performance will change, as I already observed that changing the restart heuristic can
  have dramatic effects, but fixing it is always better, because it only gives more freedom to
  the implementation (including to not change anything).

  The first criterion does not allow deleting clauses (including the useless US component as I did
  previously). The termination in both cases comes from non-relearning of clauses.

  The proofs changed dramatically (and become much more messy) but that was expected, because the
  base calculus has changed a lot (new clauses can be learned).

  Another difference is that after restarting, I allow anything following a CDCL run to
  happen. Proving that this terminates is delayed to the concrete implementation (e.g., vivification
  or HBR) and does not matter of the overall termination proof (but is obviously important in
  when generating code!).

›
inductive pcdcl_restart :: ‹'v prag_st ⇒ 'v prag_st ⇒ bool› where
restart_trail:
   ‹pcdcl_restart (M, N, U, None, NE, UE, NS, US, N0, U0)
        (M', N', U', None, NE + NE', UE'', NS, {#}, N0, {#})›
  if
    ‹(Decided K # M', M2) ∈ set (get_all_ann_decomposition M)› and
    ‹U' + UE' ⊆# U› and
    ‹N = N' + NE'› and
    ‹∀E∈#NE'+UE'. ∃L∈#E. L ∈ lits_of_l M' ∧ get_level M' L = 0›
    ‹∀L E. Propagated L E ∈ set M' ⟶ E ∈# (N + U') + NE + UE''›
    ‹UE'' ⊆# UE + UE'›|
restart_clauses:
   ‹pcdcl_restart (M, N, U, None, NE, UE, NS, US, N0, U0)
      (M, N', U', None, NE + NE', UE'', NS, US', N0, {#})›
  if
    ‹U' + UE' ⊆# U› and
    ‹N = N' + NE'› and
    ‹∀E∈#NE'+UE'. ∃L∈#E. L ∈ lits_of_l M ∧ get_level M L = 0›
    ‹∀L E. Propagated L E ∈ set M ⟶ E ∈# (N + U') + NE + UE''›
    ‹UE'' ⊆# UE + UE'›
    ‹US' = {#}›


inductive pcdcl_restart_only :: ‹'v prag_st ⇒ 'v prag_st ⇒ bool› where
restart_trail:
   ‹pcdcl_restart_only (M, N, U, None, NE, UE, NS, US, N0, U0)
        (M', N, U, None, NE, UE, NS, US, N0, U0)›
  if
    ‹(Decided K # M', M2) ∈ set (get_all_ann_decomposition M) ∨ M = M'›


(*TODO Taken from Misc*)
lemma mset_le_incr_right1:
  "a⊆#(b::'a multiset) ⟹ a⊆#b+c" using mset_subset_eq_mono_add[of a b "{#}" c, simplified] .

lemma pcdcl_restart_cdclW_stgy:
  fixes S V :: ‹'v prag_st›
  assumes
    ‹pcdcl_restart S V› and
    ‹pcdcl_all_struct_invs S› and
    ‹cdclW_restart_mset.cdclW_stgy_invariant (state_of S)› and
    ‹cdclW_restart_mset.no_smaller_propa (state_of S)›
  shows
    ‹∃T. cdclW_restart_mset.restart (state_of S) T ∧ cdclW_restart_mset.cdclW_stgy** T (state_of V) ∧
      cdclW_restart_mset.cdclW_restart** (state_of S) (state_of V)›
  using assms
proof (induction rule: pcdcl_restart.induct)
  case (restart_trail K M' M2 M U' UE' U N N' NE' NE UE'' UE NS US N0 U0)
  note decomp = this(1) and learned = this(2) and N = this(3) and
    has_true = this(4) and kept = this(5) and UE'' = this(6) and inv = this(7) and stgy_invs = this(8) and
    smaller_propa = this(9)
  let ?S = ‹(M, N, U, None, NE, UE, NS, US, N0, U0)›
  let ?T = ‹([], N + NE + NS + N0,  U' + UE'', None)›
  let ?V = ‹(M', N, U', None, NE, UE'', NS, {#}, N0, {#})›
  have incl: ‹U' + UE'' ⊆# U + UE + US + U0›
    by (smt (verit, ccfv_SIG) UE'' learned mset_subset_eq_add_left subset_mset.add_left_mono
      subset_mset.dual_order.trans union_assoc union_commute)
  then have restart: ‹cdclW_restart_mset.restart (state_of ?S) ?T›
    using learned UE''
    by (auto simp: cdclW_restart_mset.restart.simps state_def clauses_def
      intro: mset_le_incr_right1)
  have struct_invs:
      ‹cdclW_restart_mset.cdclW_all_struct_inv (state_of ?S)›
    using inv unfolding  pcdcl_all_struct_invs_def by auto

  have drop_M_M': ‹drop (length M - length M') M = M'›
    using decomp by (auto)
  have ‹cdclW_restart_mset.cdclW_stgy** ?T
      (drop (length M - length M') M, N + NE + NS + N0,
        U' + UE'', None)› for n
    apply (rule after_fast_restart_replay[of M ‹N + NE + NS + N0›
          ‹U+UE+US+U0› _
          ‹U' + UE''›])
    subgoal using struct_invs by simp
    subgoal using stgy_invs by simp
    subgoal using smaller_propa by simp
    subgoal using kept unfolding drop_M_M' by (auto simp add: ac_simps)
    subgoal using incl by simp
    done
  then have st: ‹cdclW_restart_mset.cdclW_stgy** ?T (state_of ?V)›
    unfolding drop_M_M' by (simp add: ac_simps)
  moreover have ‹cdclW_restart_mset.cdclW_restart** (state_of ?S) (state_of ?V)›
    using restart st
    by (auto dest!: cdclW_restart_mset.cdclW_rf.intros cdclW_restart_mset.cdclW_restart.intros
          cdclW_restart_mset.rtranclp_cdclW_stgy_rtranclp_cdclW_restart)
  ultimately show ?case
    using restart unfolding N state_of.simps image_mset_union add.assoc state_of.simps
      add.commute[of ‹NE'›]
    by fast
next
  case (restart_clauses U' UE' U N N' NE' M NE UE'' UE US' NS US N0 U0)
  note learned = this(1) and N = this(2) and has_true = this(3) and kept = this(4) and
    UE'' = this(5) and US = this(6) and inv = this(7) and stgy_invs = this(8) and
    smaller_propa = this(9)
  let ?S = ‹(M, N, U, None, NE, UE, NS, US, N0, U0) :: 'v prag_st›
  let ?T = ‹([] :: ('v, 'v clause) ann_lits, N + NE + NS + N0, U' + UE'' + US', None)›
  let ?V = ‹(M, N, U', None, NE, UE'', NS, US', N0, {#}) :: 'v prag_st›
  have incl: ‹U' + UE''  ⊆# U + UE + US + U0›
    by (smt (verit, ccfv_SIG) UE'' learned mset_subset_eq_add_left subset_mset.add_left_mono
      subset_mset.dual_order.trans union_assoc union_commute)
  then have restart: ‹cdclW_restart_mset.restart (state_of ?S) ?T›
    using learned US
    by (auto simp: cdclW_restart_mset.restart.simps state_def clauses_def cdclW_restart_mset_state
        intro: mset_le_incr_right1
        split: if_splits)

  have struct_invs:
      ‹cdclW_restart_mset.cdclW_all_struct_inv (state_of ?S)›
    using inv unfolding pcdcl_all_struct_invs_def by auto


  have ‹cdclW_restart_mset.cdclW_stgy** ?T
      (drop (length M - length M) M, N + NE+NS+N0,
        U' + UE''+US', None)› for n
    apply (rule after_fast_restart_replay[of M ‹N + NE+NS+N0›
           ‹U+UE+US+U0› _
          ‹U' + UE''+US'›])
    subgoal using struct_invs by simp
    subgoal using stgy_invs by simp
    subgoal using smaller_propa by simp
    subgoal using kept by (auto simp add: ac_simps)
    subgoal using incl US by (auto intro: mset_le_incr_right1)
    done
  then have st: ‹cdclW_restart_mset.cdclW_stgy** ?T (state_of ?V)›
    by (simp add: ac_simps)
  moreover have ‹cdclW_restart_mset.cdclW_restart** (state_of ?S) (state_of ?V)›
    using restart st
    by (auto dest!: cdclW_restart_mset.cdclW_rf.intros cdclW_restart_mset.cdclW_restart.intros
          cdclW_restart_mset.rtranclp_cdclW_stgy_rtranclp_cdclW_restart)
  ultimately show ?case
    using restart unfolding N state_of.simps image_mset_union add.assoc add.commute[of ‹NE'›]
    by fast
qed

lemma pcdcl_restart_cdclW:
  assumes
    ‹pcdcl_restart S V› and
    ‹pcdcl_all_struct_invs S›
  shows
    ‹∃T. cdclW_restart_mset.restart (state_of S) T ∧ cdclW_restart_mset.cdclW** T (state_of V)›
  using assms
proof (induction rule: pcdcl_restart.induct)
  case (restart_trail K M' M2 M U' UE' U N N' NE' NE UE'' UE NS US N0 U0)
  note decomp = this(1) and learned = this(2) and N = this(3) and
    has_true = this(4) and kept = this(5) and UE'' = this(6) and inv = this(7)
  let ?S = ‹(M, N, U, None, NE, UE, NS, US, N0, U0)›
  let ?T = ‹([], N + NE + NS + N0, U' + UE'' , None)›
  let ?V = ‹(M', N, U', None, NE, UE'', NS, {#}, N0, {#})›
  have incl: ‹U' + UE''  ⊆# U + UE + US + U0›
    by (smt (verit, ccfv_SIG) UE'' learned mset_subset_eq_add_left subset_mset.add_left_mono
      subset_mset.dual_order.trans union_assoc union_commute)
  then have restart: ‹cdclW_restart_mset.restart (state_of ?S) ?T›
    using learned
    by (auto simp: cdclW_restart_mset.restart.simps state_def clauses_def cdclW_restart_mset_state
        intro: mset_le_incr_right1)
  have struct_invs:
      ‹cdclW_restart_mset.cdclW_all_struct_inv (state_of ?S)› 
    using inv unfolding pcdcl_all_struct_invs_def by auto
  have drop_M_M': ‹drop (length M - length M') M = M'›
    using decomp by (auto)
  have ‹cdclW_restart_mset.cdclW** ?T
      (drop (length M - length M') M,  N + NE + NS + N0,
          U' + UE'', None)› for n
    apply (rule after_fast_restart_replay_no_stgy[of M
      ‹N + NE + NS+N0› ‹U+UE+US+U0› _
          ‹U' + UE''›])
    subgoal using struct_invs by simp
    subgoal using kept unfolding drop_M_M' by (auto simp add: ac_simps)
    subgoal using incl by fast
    done
  then have st: ‹cdclW_restart_mset.cdclW** ?T (state_of ?V)›
    unfolding drop_M_M' by (simp add: ac_simps)
  then show ?case
    using restart by (auto simp: ac_simps N)
next
  case (restart_clauses U' UE' U N N' NE' M NE UE'' UE US' NS US N0 U0)
  note learned = this(1) and N = this(2) and has_true = this(3) and kept = this(4) and
    UE'' = this(5) and US = this(6) and inv = this(7)
  let ?S = ‹(M, N, U, None, NE, UE,NS, US, N0, U0)›
  let ?T = ‹([], N + NE + NS+N0, U' + UE'' + US', None)›
  let ?V = ‹(M, N, U', None, NE, UE'', NS, US', N0, {#})›
  have incl: ‹U' + UE''  ⊆# U + UE + US + U0›
    by (smt (verit, ccfv_SIG) UE'' learned mset_subset_eq_add_left subset_mset.add_left_mono
      subset_mset.dual_order.trans union_assoc union_commute)
  then have restart: ‹cdclW_restart_mset.restart (state_of ?S) ?T›
    using learned US
    by (auto simp: cdclW_restart_mset.restart.simps state_def clauses_def cdclW_restart_mset_state
        intro: mset_le_incr_right1 split: if_splits)
  have struct_invs:
      ‹cdclW_restart_mset.cdclW_all_struct_inv (state_of ?S)› 
    using inv unfolding pcdcl_all_struct_invs_def by fast+

  have ‹cdclW_restart_mset.cdclW** ?T
      (drop (length M - length M) M, N + NE+NS+N0,
        U' + UE''+US', None)› for n
    apply (rule after_fast_restart_replay_no_stgy[of M ‹N + NE+NS+N0›
           ‹U+UE+US+U0› _
          ‹U' + UE''+US'›])
    subgoal using struct_invs by simp
    subgoal using kept by (auto simp add: ac_simps)
    subgoal using incl US by auto
    done
  then have st: ‹cdclW_restart_mset.cdclW** ?T (state_of ?V)›
    by (simp add: ac_simps)
  then show ?case
    using restart by (auto simp: ac_simps N)
qed

lemma mset_sum_eq_add_msetD: "A + B = add_mset C D ⟹ C ∈# A ∨ C ∈# B"
  by (metis union_iff union_single_eq_member)


lemma (in -) pcdcl_restart_pcdcl_all_struct_invs:
  fixes S V :: ‹'v prag_st›
  assumes
    ‹pcdcl_restart S V› and
    ‹pcdcl_all_struct_invs S›
  shows 
    ‹pcdcl_all_struct_invs V›
  using assms pcdcl_restart_cdclW[OF assms(1,2)] apply -
  apply normalize_goal+
  subgoal for T
    using cdclW_restart_mset.rtranclp_cdclW_all_struct_inv_inv[of ‹state_of S› ‹state_of V›]
        cdclW_restart_mset.rtranclp_cdclW_cdclW_restart[of T ‹state_of V›]
        cdclW_restart_mset.rtranclp_cdclW_cdclW_restart
       converse_rtranclp_into_rtranclp[of cdclW_restart_mset.cdclW_restart ‹state_of S› T ‹state_of V›] apply -
    apply (cases rule: pcdcl_restart.cases, assumption)
    subgoal
      using get_all_ann_decomposition_lvl0_still[of _ _ _ ‹pget_trail S›]
      apply (auto simp: pcdcl_all_struct_invs_def dest!: cdclW_restart_mset.cdclW_rf.restart
        cdclW_restart_mset.rf)
      apply (auto 7 3 simp: entailed_clss_inv_def clauses0_inv_def psubsumed_invs_def
        dest!: multi_member_split  mset_subset_eq_insertD mset_sum_eq_add_msetD)
      done
    subgoal
      apply (auto simp: pcdcl_all_struct_invs_def dest!: cdclW_restart_mset.cdclW_rf.restart
        cdclW_restart_mset.rf)
      apply (auto 7 3 simp: entailed_clss_inv_def clauses0_inv_def psubsumed_invs_def
        dest!: multi_member_split  mset_subset_eq_insertD mset_sum_eq_add_msetD)
      done
    done
  done

lemma (in conflict_driven_clause_learning_with_adding_init_clauseW) restart_no_smaller_propa:
  ‹restart S T ⟹ no_smaller_propa S ⟹ no_smaller_propa T›
  by (induction rule: restart.induct)
   (auto simp: restart.simps no_smaller_propa_def state_prop)

text ‹The next theorem does not use the existence of the decomposition to prove
a much stronger version.›
lemma (in -) pcdcl_restart_no_smaller_propa:
  fixes S V :: ‹'v prag_st›
  assumes
    ‹pcdcl_restart S V› and
    ‹pcdcl_all_struct_invs S› and
    ‹cdclW_restart_mset.cdclW_stgy_invariant (state_of S)› and
    ‹cdclW_restart_mset.no_smaller_propa (state_of S)›
  shows 
    ‹cdclW_restart_mset.no_smaller_propa (state_of V)›
  using assms pcdcl_restart_cdclW_stgy[OF assms(1,2,3,4)]
    pcdcl_restart_pcdcl_all_struct_invs[OF assms(1,2)] apply -
  apply normalize_goal+
	subgoal for T
    using cdclW_restart_mset.restart_no_smaller_propa[of ‹state_of S› T]
      cdclW_restart_mset.rtranclp_cdclW_stgy_no_smaller_propa[of T ‹state_of V›]
      cdclW_restart_mset.cdclW_all_struct_inv_inv[of ‹state_of S› T,
      OF cdclW_restart_mset.cdclW_restart.rf,
      OF cdclW_restart_mset.cdclW_rf.restart]
    by (auto simp: pcdcl_all_struct_invs_def)
  done



lemma pcdcl_restart_no_smaller_propa':
  fixes S V :: ‹'v prag_st›
  assumes
    ‹pcdcl_restart S V› and
    ‹cdclW_restart_mset.no_smaller_propa (state_of S)›
  shows 
    ‹cdclW_restart_mset.no_smaller_propa (state_of V)›
  using assms
  by (induction rule: pcdcl_restart.induct)
   (force simp: cdclW_restart_mset.no_smaller_propa_def clauses_def
      dest!: get_all_ann_decomposition_exists_prepend)+

lemma pcdcl_restart_only_cdclW_stgy:
  fixes S V :: ‹'v prag_st›
  assumes
    ‹pcdcl_restart_only S V› and
    ‹pcdcl_all_struct_invs S› and
    ‹cdclW_restart_mset.cdclW_stgy_invariant (state_of S)› and
    ‹cdclW_restart_mset.no_smaller_propa (state_of S)›
  shows
    ‹∃T. cdclW_restart_mset.restart (state_of S) T ∧ cdclW_restart_mset.cdclW_stgy** T (state_of V) ∧
      cdclW_restart_mset.cdclW_restart** (state_of S) (state_of V)›
  using assms
proof (induction rule: pcdcl_restart_only.induct)
  case (restart_trail K M' M2 M N U NE UE NS US N0 U0)
  note decomp = this(1) and inv = this(2) and stgy_invs = this(3) and
    smaller_propa = this(4)
  let ?S = ‹(M, N, U, None, NE, UE, NS, US, N0, U0)›
  let ?T = ‹([], N + NE + NS + N0,  U + UE + US + U0, None)›
  let ?V = ‹(M', N, U, None, NE, UE, NS, US, N0, U0)›
  have restart: ‹cdclW_restart_mset.restart (state_of ?S) ?T›
    by (auto simp: cdclW_restart_mset.restart.simps state_def clauses_def cdclW_restart_mset_state
        intro: mset_le_incr_right1)
  have reas: ‹cdclW_restart_mset.reasons_in_clauses (state_of ?S)›
    using inv unfolding cdclW_restart_mset.cdclW_all_struct_inv_def
      cdclW_restart_mset.cdclW_learned_clause_def pcdcl_all_struct_invs_def
      by auto
  have struct_invs:
      ‹cdclW_restart_mset.cdclW_all_struct_inv (state_of ?S)›
    using inv unfolding  pcdcl_all_struct_invs_def by auto

  have drop_M_M': ‹drop (length M - length M') M = M'›
    using decomp by (auto)
  have ‹cdclW_restart_mset.cdclW_stgy** ?T
      (drop (length M - length M') M, N + NE + NS + N0, U + UE + US + U0, None)› for n
    apply (rule after_fast_restart_replay[of M ‹N + NE + NS + N0›
          ‹U+UE+US+U0› _
          ‹U+UE+US+U0›])
    subgoal using struct_invs by simp
    subgoal using stgy_invs by simp
    subgoal using smaller_propa by simp
    subgoal using reas unfolding cdclW_restart_mset.reasons_in_clauses_def
      by (auto simp: clauses_def get_all_mark_of_propagated_alt_def dest!: in_set_dropD)
    subgoal by auto
    done
  then have st: ‹cdclW_restart_mset.cdclW_stgy** ?T (state_of ?V)›
    unfolding drop_M_M' by (simp add: ac_simps)
  moreover have ‹cdclW_restart_mset.cdclW_restart** (state_of ?S) (state_of ?V)›
    using restart st
    by (auto dest!: cdclW_restart_mset.cdclW_rf.intros cdclW_restart_mset.cdclW_restart.intros
          cdclW_restart_mset.rtranclp_cdclW_stgy_rtranclp_cdclW_restart)
  ultimately show ?case
    using restart unfolding state_of.simps image_mset_union add.assoc state_of.simps
      add.commute[of ‹NE'›]
    by fast
qed

lemma pcdcl_restart_only_cdclW:
  assumes
    ‹pcdcl_restart_only S V› and
    ‹pcdcl_all_struct_invs S›
  shows
    ‹∃T. cdclW_restart_mset.restart (state_of S) T ∧ cdclW_restart_mset.cdclW** T (state_of V)›
  using assms
proof (induction rule: pcdcl_restart_only.induct)
  case (restart_trail K M' M2 M N U NE UE NS US N0 U0)
  note decomp = this(1) and inv = this(2)
  let ?S = ‹(M, N, U, None, NE, UE, NS, US, N0, U0)›
  let ?T = ‹([], N + NE + NS+N0, U + UE + US+U0, None)›
  let ?V = ‹(M', N, U, None, NE, UE + US, NS, {#}, N0, U0)›
  have restart: ‹cdclW_restart_mset.restart (state_of ?S) ?T›
    by (auto simp: cdclW_restart_mset.restart.simps state_def clauses_def cdclW_restart_mset_state
        intro: mset_le_incr_right1)
  have struct_invs:
      ‹cdclW_restart_mset.cdclW_all_struct_inv (state_of ?S)› 
    using inv unfolding pcdcl_all_struct_invs_def by auto
  then have reas: ‹cdclW_restart_mset.reasons_in_clauses (state_of ?S)›
    unfolding cdclW_restart_mset.cdclW_all_struct_inv_def
      cdclW_restart_mset.cdclW_learned_clause_def
      by auto
  have drop_M_M': ‹drop (length M - length M') M = M'›
    using decomp by (auto)
  have ‹cdclW_restart_mset.cdclW** ?T
      (drop (length M - length M') M,  N + NE + NS+N0,
          U + UE+ US+U0, None)› for n
    apply (rule after_fast_restart_replay_no_stgy[of M
      ‹N + NE + NS+N0› ‹U+UE+US+U0› _
          ‹U + UE + US+U0›])
    subgoal using struct_invs by simp
    subgoal using reas unfolding cdclW_restart_mset.reasons_in_clauses_def
      by (auto simp: clauses_def get_all_mark_of_propagated_alt_def dest!: in_set_dropD)
    subgoal by (auto intro: mset_le_incr_right1)
    done
  then have st: ‹cdclW_restart_mset.cdclW** ?T (state_of ?V)›
    unfolding drop_M_M' by (simp add: ac_simps)
  then show ?case
    using restart by (auto simp: ac_simps)
qed

lemma pcdcl_restart_only_pcdcl_all_struct_invs:
  fixes S V :: ‹'v prag_st›
  assumes
    ‹pcdcl_restart_only S V› and
    ‹pcdcl_all_struct_invs S›
  shows 
    ‹pcdcl_all_struct_invs V›
  using assms pcdcl_restart_only_cdclW[OF assms] apply -
  apply normalize_goal+
  subgoal for T
    using cdclW_restart_mset.rtranclp_cdclW_all_struct_inv_inv[of ‹state_of S› ‹state_of V›]
      cdclW_restart_mset.rtranclp_cdclW_cdclW_restart[of T ‹state_of V›]
      cdclW_restart_mset.rtranclp_cdclW_cdclW_restart
      converse_rtranclp_into_rtranclp[of cdclW_restart_mset.cdclW_restart ‹state_of S› T ‹state_of V›] apply -
    apply (cases rule: pcdcl_restart_only.cases, assumption)
    subgoal
      using get_all_ann_decomposition_lvl0_still[of _ _ _ ‹pget_trail S›]
      apply (auto simp: pcdcl_all_struct_invs_def dest!: cdclW_restart_mset.cdclW_rf.restart
        cdclW_restart_mset.rf)
      by (auto 7 3 simp: entailed_clss_inv_def clauses0_inv_def psubsumed_invs_def
        dest!: multi_member_split)
    done
  done

definition pcdcl_final_state :: ‹'v prag_st ⇒ bool› where
  ‹pcdcl_final_state S ⟷ no_step pcdcl_core S ∨
     (count_decided (pget_trail S) = 0 ∧ pget_conflict S ≠ None)›

context twl_restart_ops
begin
text ‹
  The following definition diverges from our previous attempt... mostly because we barely used it
  anyway. The problem was that we need to stop in final states which was not covered in the previous
  form.

  The main issue is the termination of the calculus. Between two restarts we
  allow very abstract inprocessing that makes it possible to add clauses.
  However, this means that we can add the same clause over and over and that
  have reached the bound (or subsume these clauses).

  TODO: add a forget rule in term‹pcdcl_stgy› instead of having it in restart.

  The state is defined as an accumulator: The first component is the state we had after the last
  full restart (or the beginning of the search). We tried to make do without it, but the problem
  is managing to express the condition
  term‹size (pget_all_learned_clss T) - size (pget_all_learned_clss R) > f n› without it. In a fast
  attempt, we completely oversaw that issue and had (in the current notations)
  term‹size (pget_all_learned_clss T) - size (pget_all_learned_clss S) > f n›. This has, however,
  a very different semantics and allows much fewer restarts.


  One minor drawback is that we compare the number of clauses to the number of clauses after
  inprocessing instead of before inprocessing. The problem is that inprocessing could add the
  clause several times. I am not certain how to avoid that problem. An obvious solution is to
  ensure that no already-present clause is added (or at least that all duplicates have been removed)
  but it is not clear how to implement that inprocessing is not done until fixpoint.
 ›
type_synonym (in -)'v prag_st_restart = ‹'v prag_st × 'v prag_st × 'v prag_st × nat × nat × bool›

abbreviation (in -)current_state :: ‹'v prag_st_restart ⇒ 'v prag_st› where
  ‹current_state S ≡ fst (snd (snd S))›

abbreviation (in -)current_number :: ‹'v prag_st_restart ⇒ nat› where
  ‹current_number S ≡ fst (snd (snd (snd (snd S))))›

abbreviation (in -)current_restart_count :: ‹'v prag_st_restart ⇒ nat› where
  ‹current_restart_count S ≡ fst (snd (snd (snd S)))›

abbreviation (in -)last_GC_state :: ‹'v prag_st_restart ⇒ 'v prag_st› where
  ‹last_GC_state S ≡ fst S›

abbreviation (in -)last_restart_state :: ‹'v prag_st_restart ⇒ 'v prag_st› where
  ‹last_restart_state S ≡ fst (snd S)›

abbreviation (in -)restart_continue :: ‹'v prag_st_restart ⇒ bool› where
  ‹restart_continue S ≡ snd (snd (snd (snd (snd S))))›

text ‹As inprocessing, we allow a slightly different set of rules, including restart. Remember that
the termination below takes the inprocessing as a granted (terminated) process. And without 
restrictions, the inprocessing does not terminate (it can restart).

On limitation of the following system is that term‹pcdcl_inprocessing› is not allowed to derive the
empty clause. We tried to lift this limitation, but finally decided against it. The main problem is
that the regularity and the termination gets lost due to that rule.

The right place to handle the special case is later when reaching the final state in our or wherever
the predicate is used.

›

inductive (in -)pcdcl_inprocessing :: ‹'v prag_st ⇒ 'v prag_st ⇒ bool›
where
  ‹pcdcl S T ⟹ pcdcl_inprocessing S T› |
  ‹pcdcl_restart S T ⟹ pcdcl_inprocessing S T›

inductive pcdcl_stgy_restart
  :: ‹'v prag_st_restart ⇒ 'v prag_st_restart ⇒ bool›
where
step:
  ‹pcdcl_stgy_restart (R, S, T, m, n, True)  (R, S, T', m, n, True)›
  if
    ‹pcdcl_tcore_stgy T T'› |
restart_step:
  ‹pcdcl_stgy_restart (R, S, T, m, n, True)  (W, W, W, m, Suc n, True)›
  if
    ‹size (pget_all_learned_clss T) - size (pget_all_learned_clss R) > f n› and
    ‹pcdcl_inprocessing** T V›
    (*‹pcdcl_restart U V› and*)
    ‹cdclW_restart_mset.no_smaller_propa (state_of V)› and
    ‹pcdcl_stgy** V W› |
restart_noGC_step:
  ‹pcdcl_stgy_restart (R, S, T, m, n, True)  (R, U, U, Suc m, n, True)›
  if
    ‹size (pget_all_learned_clss T) > size (pget_all_learned_clss S)› and
    ‹pcdcl_restart_only T U› |
restart_full:
 ‹pcdcl_stgy_restart (R, S, T, m, n, True)  (R, S, T, m, n, False)›
 if
    ‹pcdcl_final_state T›

end


lemma (in -) pcdcl_tcore_conflict_final_state_still:
  assumes
    ‹pcdcl_tcore S T› and
    ‹count_decided (pget_trail S) = 0 ∧ pget_conflict S ≠ None›
    shows ‹count_decided (pget_trail T) = 0 ∧ pget_conflict T ≠ None ∧
       pget_all_learned_clss S = pget_all_learned_clss T›
  using assms
  by (auto simp: pcdcl_tcore.simps pcdcl_core.simps cdcl_conflict.simps cdcl_propagate.simps
    cdcl_decide.simps cdcl_skip.simps cdcl_resolve.simps cdcl_backtrack.simps cdcl_subsumed.simps
    cdcl_backtrack_unit.simps cdcl_flush_unit.simps)


lemma (in -) rtranclp_pcdcl_tcore_conflict_final_state_still:
  assumes
    ‹pcdcl_tcore** S T› and
    ‹count_decided (pget_trail S) = 0 ∧ pget_conflict S ≠ None›
  shows
    ‹count_decided (pget_trail T) = 0 ∧ pget_conflict T ≠ None ∧
    pget_all_learned_clss S = pget_all_learned_clss T›
  using assms
  by (induction rule: rtranclp_induct) (auto simp: pcdcl_tcore_conflict_final_state_still)

lemma pcdcl_tcore_no_core_no_learned:
  assumes ‹pcdcl_tcore S T› and
    ‹no_step pcdcl_core S›
  shows ‹pget_all_learned_clss S = pget_all_learned_clss T›
  using assms
  by (cases T)
    (auto simp: pcdcl_tcore.simps cdcl_subsumed.simps cdcl_flush_unit.simps pcdcl_core.simps
      dest: pcdcl_core.intros(6) elim!:  cdcl_backtrack_unit_is_backtrack[of S])

lemma (in -) pcdcl_tcore_no_step_final_state_still:
  assumes
    ‹pcdcl_tcore S T› and
    ‹no_step pcdcl_core S›
  shows ‹no_step pcdcl_core T›
proof -
  have ‹cdcl_subsumed S T ∨ cdcl_backtrack_unit S T ∨ cdcl_flush_unit S T›
    using assms unfolding pcdcl_tcore.simps by fast
  then have dist: ‹cdcl_subsumed S T ∨ cdcl_flush_unit S T›
    using assms(2) cdcl_backtrack_unit_is_backtrack pcdcl_core.intros(6) by blast
  then have ‹∃U. cdcl_resolve T U ⟹ ∃T. cdcl_resolve S T›
    by (metis cdcl_flush_unit_unchanged cdcl_resolve_is_resolve resolve_is_cdcl_resolve
      state_of_cdcl_subsumed)
  moreover have ‹∃U. cdcl_skip T U ⟹ ∃T. cdcl_skip S T›
    using dist
    by (metis cdcl_flush_unit_unchanged cdcl_skip_is_skip skip_is_cdcl_skip
      state_of_cdcl_subsumed)
   moreover have ‹∃U. cdcl_backtrack T U ⟹ ∃T. cdcl_backtrack S T›
    using dist
    by (metis backtrack_is_cdcl_backtrack cdcl_backtrack_is_backtrack cdcl_flush_unit_unchanged
      state_of_cdcl_subsumed)
   moreover have ‹∃U. cdcl_conflict T U ⟹ ∃T. cdcl_conflict S T›
    using dist
    by (cases S)
     (auto simp: pcdcl_tcore.simps pcdcl_core.simps cdcl_conflict.simps cdcl_propagate.simps
        cdcl_decide.simps cdcl_skip.simps cdcl_resolve.simps cdcl_backtrack.simps cdcl_subsumed.simps
        cdcl_backtrack_unit.simps cdcl_flush_unit.simps)
   moreover have ‹∃U. cdcl_propagate T U ⟹ ∃T. cdcl_propagate S T›
    using dist
    by (cases S)
      (auto 5 3 simp: pcdcl_tcore.simps pcdcl_core.simps cdcl_conflict.simps cdcl_propagate.simps
        cdcl_decide.simps cdcl_skip.simps cdcl_resolve.simps cdcl_backtrack.simps cdcl_subsumed.simps
        cdcl_backtrack_unit.simps cdcl_flush_unit.simps)
   moreover have ‹∃U. cdcl_decide T U ⟹ ∃T. cdcl_decide S T›
    using dist
    by (cases S)
      (auto simp: pcdcl_tcore.simps pcdcl_core.simps cdcl_conflict.simps cdcl_propagate.simps
        cdcl_decide.simps cdcl_skip.simps cdcl_resolve.simps cdcl_backtrack.simps cdcl_subsumed.simps
        cdcl_backtrack_unit.simps cdcl_flush_unit.simps)
   ultimately have ‹pcdcl_core T S' ⟹ False› for S'
     using assms(2) unfolding pcdcl_core.simps
     by (elim disjE) metis+
   then show ?thesis
     by blast
qed

lemma (in -) rtranclp_pcdcl_tcore_no_step_final_state_still:
  assumes
    ‹pcdcl_tcore** S T› and
    ‹no_step pcdcl_core S›
  shows ‹no_step pcdcl_core T›
  using assms by (induction rule: rtranclp_induct) (blast dest!: pcdcl_tcore_no_step_final_state_still)+

lemma rtranclp_pcdcl_tcore_no_core_no_learned:
  assumes ‹pcdcl_tcore** S T› and
    ‹no_step pcdcl_core S›
  shows ‹pget_all_learned_clss S = pget_all_learned_clss T›
  using assms rtranclp_pcdcl_tcore_no_step_final_state_still[OF assms]
  by (induction rule: rtranclp_induct)
    (simp_all add: pcdcl_tcore_no_core_no_learned rtranclp_pcdcl_tcore_no_step_final_state_still)


lemma no_step_pcdcl_core_stgy_pcdcl_coreD:
   ‹no_step pcdcl_core_stgy S ⟹ no_step pcdcl_core S›
  using pcdcl_core.simps pcdcl_core_stgy.simps by blast

lemma rtranclp_pcdcl_tcore_stgy_no_core_no_learned:
  assumes ‹pcdcl_tcore_stgy** S T› and
    ‹no_step pcdcl_core S›
  shows ‹pget_all_learned_clss S = pget_all_learned_clss T›
  using rtranclp_pcdcl_tcore_stgy_pcdcl_tcoreD[OF assms(1)] assms(2)
  by (blast intro: rtranclp_pcdcl_tcore_no_core_no_learned)

inductive pcdcl_stgy_only_restart for S where
 restart_noGC_step:
  ‹pcdcl_stgy_only_restart (S) (U)›
  if
    ‹pcdcl_tcore_stgy++ S T› and
    ‹size (pget_all_learned_clss T) > size (pget_all_learned_clss S)› and
    ‹pcdcl_restart_only T U›

lemma restart_noGC_stepI:
  ‹pcdcl_stgy_only_restart (S) (U)›
  if
    ‹pcdcl_tcore_stgy** S T› and
    ‹size (pget_all_learned_clss T) > size (pget_all_learned_clss S)› and
    ‹pcdcl_restart_only T U›
  using restart_noGC_step[of S T U]
  by (metis not_less_iff_gr_or_eq restart_noGC_step rtranclpD that(1) that(2) that(3))

lemma pcdcl_tcore_stgy_step_or_unchanged:
   ‹pcdcl_tcore_stgy S T ⟹ pcdcl_core_stgy** S T ∨ state_of S = state_of T ∨
   (∃T'. cdcl_backtrack S T' ∧ state_of T' = state_of T)›
  apply (induction rule: pcdcl_tcore_stgy.induct)
  apply (auto simp: state_of_cdcl_subsumed cdcl_flush_unit_unchanged)[3]
  using cdcl_backtrack_unit_is_backtrack cdcl_flush_unit_unchanged by blast

lemma pcdcl_tcore_stgy_cdclW_stgy:
   ‹pcdcl_tcore_stgy S T ⟹ pcdcl_all_struct_invs S ⟹
    cdclW_restart_mset.cdclW_stgy** (state_of S) (state_of T)›
  using rtranclp_pcdcl_core_stgy_is_cdcl_stgy[of S T]
  apply (auto dest!: pcdcl_tcore_stgy_step_or_unchanged simp: pcdcl_all_struct_invs_def)
  by (metis pcdcl_core_stgy.intros(6) pcdcl_core_stgy_is_cdcl_stgy r_into_rtranclp
    state_of.simps)

lemma rtranclp_pcdcl_tcore_stgy_cdclW_stgy:
   ‹pcdcl_tcore_stgy** S T ⟹ pcdcl_all_struct_invs S ⟹
    cdclW_restart_mset.cdclW_stgy** (state_of S) (state_of T)›
  apply (induction rule: rtranclp_induct)
  subgoal by auto
  subgoal for T U
    by (smt pcdcl_tcore_pcdcl_all_struct_invs pcdcl_tcore_stgy_cdclW_stgy
      pcdcl_tcore_stgy_pcdcl_tcoreD rtranclp.rtrancl_into_rtrancl rtranclp_induct)
  done

lemma [simp]: ‹learned_clss (state_of S) = pget_all_learned_clss S›
  by (cases S) auto

lemma
  pcdcl_tcore_stgy_init_learned:
    ‹pcdcl_tcore_stgy S T ⟹ pget_init_learned_clss S ⊆# pget_init_learned_clss T› and
  pcdcl_tcore_stgy_psubsumed_learned_clauses:
    ‹pcdcl_tcore_stgy S T ⟹ psubsumed_learned_clauses S ⊆# psubsumed_learned_clauses T›and
  pcdcl_tcore_stgy_plearned_clauses0:
    ‹pcdcl_tcore_stgy S T ⟹ plearned_clauses0 S ⊆# plearned_clauses0 T›
  by (auto simp: pcdcl_tcore_stgy.simps pcdcl_core_stgy.simps cdcl_conflict.simps
    cdcl_propagate.simps cdcl_decide.simps cdcl_backtrack_unit.simps cdcl_skip.simps
    cdcl_resolve.simps cdcl_backtrack.simps cdcl_subsumed.simps cdcl_flush_unit.simps)

lemma
  rtranclp_pcdcl_tcore_stgy_init_learned:
    ‹pcdcl_tcore_stgy** S T ⟹ pget_init_learned_clss S ⊆# pget_init_learned_clss T› and
  rtranclp_pcdcl_tcore_stgy_psubsumed_learned_clauses:
    ‹pcdcl_tcore_stgy** S T ⟹ psubsumed_learned_clauses S ⊆# psubsumed_learned_clauses T› and
  rtranclp_pcdcl_tcore_stgy_plearned_clauses0:
    ‹pcdcl_tcore_stgy** S T ⟹ plearned_clauses0 S ⊆# plearned_clauses0 T›
  by (induction rule: rtranclp_induct)
    (auto dest: pcdcl_tcore_stgy_init_learned pcdcl_tcore_stgy_psubsumed_learned_clauses
      pcdcl_tcore_stgy_plearned_clauses0)

lemma
  pcdcl_stgy_only_restart_init_learned:
    ‹pcdcl_stgy_only_restart S T ⟹ pget_init_learned_clss S ⊆# pget_init_learned_clss T› and
  pcdcl_stgy_only_restart_psubsumed_learned_clauses:
    ‹pcdcl_stgy_only_restart S T ⟹ psubsumed_learned_clauses S ⊆# psubsumed_learned_clauses T› and
  pcdcl_stgy_only_restart_plearned_clauses0:
    ‹pcdcl_stgy_only_restart S T ⟹ plearned_clauses0 S ⊆# plearned_clauses0 T›
  by (auto simp: pcdcl_stgy_only_restart.simps pcdcl_restart_only.simps
    dest!: tranclp_into_rtranclp dest: rtranclp_pcdcl_tcore_stgy_init_learned
    rtranclp_pcdcl_tcore_stgy_psubsumed_learned_clauses rtranclp_pcdcl_tcore_stgy_plearned_clauses0)


lemma cdcl_twl_stgy_restart_new:
  assumes
    ‹pcdcl_stgy_only_restart S U› and
    invs: ‹pcdcl_all_struct_invs S› and
    propa: ‹cdclW_restart_mset.no_smaller_propa (state_of S)› and
    dist: ‹distinct_mset (pget_learned_clss S - A)›
 shows ‹distinct_mset (pget_learned_clss U - A)›
  using assms(1)
proof cases
  case (restart_noGC_step T) note st = this(1) and res = this(3)
  have ‹cdclW_restart_mset.cdclW_stgy** (state_of S) (state_of T)›
    using rtranclp_pcdcl_tcore_stgy_cdclW_stgy[of S T] invs st
    unfolding pcdcl_all_struct_invs_def
    by (auto dest!: tranclp_into_rtranclp)

  then have dist: ‹distinct_mset (learned_clss (state_of T) - (A + pget_init_learned_clss S +
      psubsumed_learned_clauses S + plearned_clauses0 S))›
   apply (rule cdclW_restart_mset.rtranclp_cdclW_stgy_distinct_mset_clauses_new_abs)
   subgoal using invs unfolding pcdcl_all_struct_invs_def by fast
   subgoal using propa unfolding pcdcl_all_struct_invs_def by fast
   subgoal using dist by (cases S) simp
   done
 have [simp]: ‹pget_all_learned_clss U = pget_all_learned_clss T›
   by (use res in ‹auto simp: pcdcl_restart_only.simps›)
 have ‹distinct_mset (learned_clss (state_of U) - (A + pget_init_learned_clss U +
    psubsumed_learned_clauses U + plearned_clauses0 U))›
   apply (rule distinct_mset_mono[OF _ dist])
   by (simp add: assms(1) diff_le_mono2_mset pcdcl_stgy_only_restart_init_learned
     pcdcl_stgy_only_restart_psubsumed_learned_clauses subset_mset.add_mono
     pcdcl_stgy_only_restart_plearned_clauses0)
 then show ‹?thesis›
   using res by (auto simp add: pcdcl_restart_only.simps)
qed


lemma cdcl_twl_stgy_restart_new':
  assumes
    ‹pcdcl_stgy_only_restart S U› and
    invs: ‹pcdcl_all_struct_invs S› and
    propa: ‹cdclW_restart_mset.no_smaller_propa (state_of S)› and
    dist: ‹distinct_mset (pget_all_learned_clss S - A)›
 shows ‹distinct_mset (pget_all_learned_clss U - A)›
  using assms(1)
proof cases
  case (restart_noGC_step T) note st = this(1) and res = this(3)
  have ‹cdclW_restart_mset.cdclW_stgy** (state_of S) (state_of T)›
    using rtranclp_pcdcl_tcore_stgy_cdclW_stgy[of S T] invs st
    unfolding pcdcl_all_struct_invs_def
    by (auto dest!: tranclp_into_rtranclp)

  then have dist: ‹distinct_mset (learned_clss (state_of T) - (A))›
    apply (rule cdclW_restart_mset.rtranclp_cdclW_stgy_distinct_mset_clauses_new_abs)
    subgoal using invs unfolding pcdcl_all_struct_invs_def by fast
    subgoal using propa unfolding pcdcl_all_struct_invs_def by fast
    subgoal using dist by (cases S) simp
    done
  have [simp]: ‹pget_all_learned_clss U = pget_all_learned_clss T›
    by (use res in ‹auto simp: pcdcl_restart_only.simps›)
  have ‹distinct_mset (learned_clss (state_of U) - A)›
    apply (rule distinct_mset_mono[OF _ dist])
    by (simp add: assms(1) diff_le_mono2_mset pcdcl_stgy_only_restart_init_learned
      pcdcl_stgy_only_restart_psubsumed_learned_clauses subset_mset.add_mono)
  then show ‹?thesis›
    using res by (auto simp add: pcdcl_restart_only.simps)
qed


lemma pcdcl_stgy_only_restart_all_struct_invs:
  ‹pcdcl_stgy_only_restart S T ⟹ pcdcl_all_struct_invs S ⟹ pcdcl_all_struct_invs T›
  using pcdcl_restart_only_pcdcl_all_struct_invs[of S]
  apply (auto simp: pcdcl_stgy_only_restart.simps dest!: tranclp_into_rtranclp)
  by (metis pcdcl_restart_only_pcdcl_all_struct_invs rtranclp_pcdcl_all_struct_invs
    rtranclp_pcdcl_stgy_pcdcl rtranclp_pcdcl_tcore_stgy_pcdcl_stgy')


lemma rtranclp_pcdcl_stgy_only_restart_all_struct_invs:
  ‹pcdcl_stgy_only_restart** S T ⟹ pcdcl_all_struct_invs S ⟹ pcdcl_all_struct_invs T›
  by (induction rule: rtranclp_induct) (auto dest!: pcdcl_stgy_only_restart_all_struct_invs)

lemma pcdcl_tcore_stgy_all_struct_invs:
  ‹pcdcl_tcore_stgy S T ⟹ pcdcl_all_struct_invs S ⟹ pcdcl_all_struct_invs T›
  using pcdcl_tcore_pcdcl_all_struct_invs pcdcl_tcore_stgy_pcdcl_tcoreD by blast

lemma rtranclp_pcdcl_tcore_stgy_all_struct_invs:
  ‹pcdcl_tcore_stgy** S T ⟹ pcdcl_all_struct_invs S ⟹ pcdcl_all_struct_invs T›
  by (simp add: pcdcl_tcore_stgy_all_struct_invs rtranclp_induct)

lemma pcdcl_restart_only_no_smaller_propa:
  ‹pcdcl_restart_only S T ⟹ pcdcl_all_struct_invs S ⟹
  cdclW_restart_mset.no_smaller_propa (state_of S) ⟹
  cdclW_restart_mset.no_smaller_propa (state_of T)›
  by (fastforce simp: pcdcl_restart_only.simps cdclW_restart_mset.no_smaller_propa_def
    clauses_def)

lemma pcdcl_stgy_only_restart_no_smaller_propa:
  ‹pcdcl_stgy_only_restart S T ⟹ pcdcl_all_struct_invs S ⟹
  cdclW_restart_mset.no_smaller_propa (state_of S) ⟹
  cdclW_restart_mset.no_smaller_propa (state_of T)›
  using pcdcl_restart_only_pcdcl_all_struct_invs[of _ T]
    rtranclp_pcdcl_tcore_stgy_no_smaller_propa[of S]
    rtranclp_pcdcl_tcore_stgy_all_struct_invs[of S]
    pcdcl_restart_only_no_smaller_propa[of _ T]
  by (auto simp: pcdcl_stgy_only_restart.simps dest!: tranclp_into_rtranclp)

lemma rtranclp_pcdcl_stgy_only_restart_no_smaller_propa:
  ‹pcdcl_stgy_only_restart** S T ⟹ pcdcl_all_struct_invs S ⟹ cdclW_restart_mset.no_smaller_propa (state_of S) ⟹
  cdclW_restart_mset.no_smaller_propa (state_of T)›
  apply (induction rule: rtranclp_induct)
   apply auto[]
  using pcdcl_stgy_only_restart_no_smaller_propa rtranclp_pcdcl_stgy_only_restart_all_struct_invs
  by blast

lemma rtranclp_cdcl_twl_stgy_restart_new_abs:
  assumes
    ‹pcdcl_stgy_only_restart** S T› and
    invs: ‹pcdcl_all_struct_invs S› and
    propa: ‹cdclW_restart_mset.no_smaller_propa (state_of S)› and
    dist: ‹distinct_mset (pget_learned_clss S - A)›
  shows ‹distinct_mset (pget_learned_clss T - A)›
  using assms apply (induction)
  subgoal by auto
  subgoal for T U
    using cdcl_twl_stgy_restart_new[of T U A] rtranclp_pcdcl_stgy_only_restart_all_struct_invs[of S T]
    by (auto dest: rtranclp_pcdcl_stgy_only_restart_no_smaller_propa)
  done

lemma rtranclp_cdcl_twl_stgy_restart_new_abs':
  assumes
    ‹pcdcl_stgy_only_restart** S T› and
    invs: ‹pcdcl_all_struct_invs S› and
    propa: ‹cdclW_restart_mset.no_smaller_propa (state_of S)› and
    dist: ‹distinct_mset (pget_all_learned_clss S - A)›
  shows ‹distinct_mset (pget_all_learned_clss T - A)›
  using assms apply (induction)
  subgoal by auto
  subgoal for T U
    using cdcl_twl_stgy_restart_new'[of T U A] rtranclp_pcdcl_stgy_only_restart_all_struct_invs[of S T]
    by (auto dest: rtranclp_pcdcl_stgy_only_restart_no_smaller_propa)
  done

lemma pcdcl_tcore_stgy_pget_all_learned_clss_mono:
  ‹pcdcl_tcore_stgy S T ⟹ size (pget_all_learned_clss S) ≤ size (pget_all_learned_clss T)›
  by (auto simp: pcdcl_tcore_stgy.simps pcdcl_core_stgy.simps cdcl_conflict.simps
    cdcl_propagate.simps cdcl_decide.simps cdcl_backtrack_unit.simps cdcl_skip.simps
    cdcl_resolve.simps cdcl_backtrack.simps cdcl_subsumed.simps cdcl_flush_unit.simps)

lemma rtranclp_pcdcl_tcore_stgy_pget_all_learned_clss_mono:
  ‹pcdcl_tcore_stgy** S T ⟹ size (pget_all_learned_clss S) ≤ size (pget_all_learned_clss T)›
  by (induction rule: rtranclp_induct) (auto dest!: pcdcl_tcore_stgy_pget_all_learned_clss_mono)

lemma pcdcl_stgy_only_restart_pget_all_learned_clss_mono:
  ‹pcdcl_stgy_only_restart S T ⟹ size (pget_all_learned_clss S) ≤ size (pget_all_learned_clss T)›
  by (induction rule: pcdcl_stgy_only_restart.induct)
   (auto dest!: tranclp_into_rtranclp rtranclp_pcdcl_tcore_stgy_pget_all_learned_clss_mono
    simp: pcdcl_restart_only.simps)

lemma [simp]: ‹init_clss (state_of S) = pget_all_init_clss S›
  by (cases S) auto

lemma pcdcl_tcore_stgy_pget_all_init_clss:
  ‹pcdcl_tcore_stgy S T ⟹ pget_all_init_clss S = pget_all_init_clss T›
  by (auto simp: pcdcl_tcore_stgy.simps pcdcl_core_stgy.simps cdcl_conflict.simps
    cdcl_propagate.simps cdcl_decide.simps cdcl_backtrack_unit.simps cdcl_skip.simps
    cdcl_resolve.simps cdcl_backtrack.simps cdcl_subsumed.simps cdcl_flush_unit.simps)

lemma rtranclp_pcdcl_tcore_stgy_pget_all_init_clss:
  ‹pcdcl_tcore_stgy** S T ⟹ pget_all_init_clss S = pget_all_init_clss T›
  by (induction rule: rtranclp_induct) (auto dest!: pcdcl_tcore_stgy_pget_all_init_clss)

text ‹TODO: Move›
lemma card_simple_clss_with_tautology:
  assumes ‹finite N›
  shows ‹finite {C. atms_of C ⊆ N ∧ distinct_mset C}› and
    ‹card {C. atms_of C ⊆ N ∧ distinct_mset C} ≤ 4 ^ card N›
proof -
  have [simp]: ‹finite x› if ‹atm_of ` x ⊆ N› for x
  proof -
    have ‹x ⊆ Pos ` N ∪ Neg ` N›
      using that by (smt in_set_image_subsetD literal.exhaust_sel subsetI sup_ge1 sup_ge2)
    then show ‹?thesis›
      using assms by (meson finite_UnI finite_imageI finite_subset)
  qed

  have eq: ‹card {C. atms_of C ⊆ N ∧ distinct_mset C} = card (set_mset ` {C. atms_of C ⊆ N ∧ distinct_mset C})›
    (is ‹card ?A = card ?B›)
    if [simp]: ‹finite {C. atms_of C ⊆ N ∧ distinct_mset C}›
    apply (subst eq_sym_conv)
    apply (subst inj_on_iff_eq_card[symmetric])
    apply (auto simp: inj_on_def distinct_set_mset_eq_iff)
    done
  moreover have eq'[symmetric]: ‹?B = {C. atm_of ` C ⊆ N}› (is ‹_  = ?C›)
    apply (auto simp: atms_of_def image_iff distinct_mset_mset_set intro: exI[of _ ‹mset_set _›])
    apply (rule_tac x = ‹mset_set x› in exI)
    by (auto simp: distinct_mset_mset_set)

  moreover {
    have subst: ‹?C ⊆ (λ(a,b). a ∪ b) ` (Pow (Pos ` N) × Pow (Neg ` N))›
      apply (rule, subst image_iff)
        apply (rule_tac x = ‹({L. L ∈ x ∧ is_pos L}, {L. L ∈ x ∧ is_neg L})› in bexI)
        apply (auto simp: is_pos_def)
      by (metis image_iff image_subset_iff literal.exhaust_sel)

    then have ‹finite ?C›
      by (rule finite_subset)
        (auto intro!: finite_imageI finite_cartesian_product simp: assms)
     note _ = this and subst
  } note H = this(1,2)
  ultimately show [iff]: ‹finite {C. atms_of C ⊆ N ∧ distinct_mset C}›
    apply simp
    by (metis (no_types, lifting) distinct_set_mset_eq_iff finite_imageD inj_on_def mem_Collect_eq)

  have H''[simp]: ‹card ((λx. case x of (x, xa) ⇒ x ∪ xa) ` (A × insert a ` B)) =
    card ((λx. case x of (x, xa) ⇒ x ∪ xa) ` (A × B))›
    if ‹finite A› ‹finite B› ‹a ∉ ⋃A› ‹a ∉ ⋃B› for A B a
  proof -
    have 1: ‹((λx. case x of (x, xa) ⇒ x ∪ xa) ` (A × insert a ` B)) =
      insert a `  ((λx. case x of (x, xa) ⇒ x ∪ xa) ` (A × B))›
      by (rule; rule; clarsimp simp: image_iff)
    show ‹card ((λx. case x of (x, xa) ⇒ x ∪ xa) ` (A × insert a ` B)) =
      card  ((λx. case x of (x, xa) ⇒ x ∪ xa) ` (A × B))› 
      unfolding 1
      by (subst inj_on_iff_eq_card[symmetric])
        (use that in ‹auto simp: inj_on_def›)
  qed

  have H'[simp]: ‹card ((λx. case x of (x, xa) ⇒ x ∪ xa) ` (insert a ` A × B)) =
    card ((λx. case x of (x, xa) ⇒ x ∪ xa) ` (A × B))›
    if ‹finite A› ‹finite B› ‹a ∉ ⋃A› ‹a ∉ ⋃B› for A B a
  proof -
    have 1: ‹((λx. case x of (x, xa) ⇒ x ∪ xa) ` (insert a ` A × B)) =
      insert a `  ((λx. case x of (x, xa) ⇒ x ∪ xa) ` (A × B))›
      by (rule; rule; clarsimp simp: image_iff)
    show ‹card ((λx. case x of (x, xa) ⇒ x ∪ xa) ` (insert a ` A × B)) =
      card  ((λx. case x of (x, xa) ⇒ x ∪ xa) ` (A × B))› 
      unfolding 1
      by (subst inj_on_iff_eq_card[symmetric])
        (use that in ‹auto simp: inj_on_def›)
  qed
  have ‹card {C. atms_of C ⊆ N ∧ distinct_mset C} ≤ card ((λ(a,b). a ∪ b) ` (Pow (Pos ` N) × Pow (Neg ` N)))›
    apply (subst eq)
    apply (auto simp flip: eq')
    apply (rule card_mono[OF _ H(2)])
    by (auto intro!: finite_imageI finite_cartesian_product simp: assms)
  also have ‹... ≤ 4 ^ card N›
    using assms
    apply (induction N rule: finite_induct)
    apply (auto simp: Pow_insert insert_Times_insert Sigma_Un_distrib1 Sigma_Un_distrib2
      image_Un card_Un_disjoint)
    apply (subst card_Un_disjoint)
    apply auto
    apply (subst card_Un_disjoint)
    apply auto
    apply (subst card_Un_disjoint)
    apply auto
    apply (subst H')
    apply auto
    apply (subst H')
    apply auto
    apply (subst H'')
    apply auto
    apply (subst H'')
    apply auto
    done
  finally show ‹card {C. atms_of C ⊆ N ∧ distinct_mset C} ≤ 4 ^ card N›
    .
qed


lemma pcdcl_stgy_only_restart_pget_all_init_clss:
  ‹pcdcl_stgy_only_restart S T ⟹ pget_all_init_clss S = pget_all_init_clss T›
  by (induction rule: pcdcl_stgy_only_restart.induct)
   (auto dest!: tranclp_into_rtranclp rtranclp_pcdcl_tcore_stgy_pget_all_init_clss
    simp: pcdcl_restart_only.simps)

lemma rtranclp_pcdcl_stgy_only_restart_pget_all_init_clss:
  ‹pcdcl_stgy_only_restart** S T ⟹ pget_all_init_clss S = pget_all_init_clss T›
  by (induction rule: rtranclp_induct)
   (auto dest: pcdcl_stgy_only_restart_pget_all_init_clss)

lemma
  assumes ‹pcdcl_stgy_only_restart** S T› and
    ‹pcdcl_all_struct_invs S› and
    ‹cdclW_restart_mset.no_smaller_propa (state_of S)›
  shows
    rtranclp_pcdcl_stgy_only_restart_distinct_mset:
      ‹distinct_mset (pget_all_learned_clss T - pget_all_learned_clss S)› and
    rtranclp_pcdcl_stgy_only_restart_bound:
      ‹card (set_mset (pget_all_learned_clss T - pget_all_learned_clss S))
      ≤ 4 ^ (card (atms_of_mm (pget_all_init_clss S)))› and
    rtranclp_pcdcl_stgy_only_restart_bound_size:
      ‹size (pget_all_learned_clss T - pget_all_learned_clss S)
      ≤ 4 ^ (card (atms_of_mm (pget_all_init_clss S)))›
proof -
  from assms(1) show dist: ‹distinct_mset (pget_all_learned_clss T - pget_all_learned_clss S)›
    by (rule rtranclp_cdcl_twl_stgy_restart_new_abs'[of ‹S› ‹T› ‹pget_all_learned_clss S›])
      (auto simp: assms)

  let ?N = ‹atms_of_mm (pget_all_init_clss S)›
  have fin_N: ‹finite ?N›
    by auto
  have ‹pcdcl_all_struct_invs T›
    using assms(1) assms(2) rtranclp_pcdcl_stgy_only_restart_all_struct_invs by blast
  then have ‹set_mset (pget_all_learned_clss T) ⊆ {C. atms_of C ⊆ ?N ∧ distinct_mset C}›
    by (auto simp: pcdcl_all_struct_invs_def cdclW_restart_mset.cdclW_all_struct_inv_def
      simple_clss_def cdclW_restart_mset.distinct_cdclW_state_def
      cdclW_restart_mset.no_strange_atm_def
      rtranclp_pcdcl_stgy_only_restart_pget_all_init_clss[OF assms(1)]
      dest!: multi_member_split)
  from card_mono[OF _ this] have ‹card (set_mset (pget_all_learned_clss T)) ≤ 4 ^ (card ?N)›
    using card_simple_clss_with_tautology[OF fin_N] by simp
  then show ‹card (set_mset (pget_all_learned_clss T - pget_all_learned_clss S)) ≤ 4 ^ (card ?N)›
    by (meson card_mono finite_set_mset in_diffD le_trans subsetI)
  then show ‹size (pget_all_learned_clss T - pget_all_learned_clss S)
      ≤ 4 ^ (card (atms_of_mm (pget_all_init_clss S)))›
    by (subst (asm) distinct_mset_size_eq_card[symmetric])
      (auto simp: dist)
qed

lemma wf_pcdcl_stgy_only_restart:
  ‹wf {(T, S :: 'v prag_st). pcdcl_all_struct_invs S ∧
    cdclW_restart_mset.no_smaller_propa (state_of S) ∧ pcdcl_stgy_only_restart S T}›
proof (rule ccontr)
  assume ‹¬ ?thesis›
  then obtain g :: ‹nat ⇒ 'v prag_st› where
    g: ‹⋀i. pcdcl_stgy_only_restart (g i) (g (Suc i))› and
    inv: ‹⋀i. pcdcl_all_struct_invs (g i)›and
    inv': ‹⋀i. cdclW_restart_mset.no_smaller_propa (state_of (g i))›
    unfolding wf_iff_no_infinite_down_chain by fast
  have ‹pget_all_init_clss (g (Suc i)) = pget_all_init_clss (g i)› for i
    using pcdcl_stgy_only_restart_pget_all_init_clss[OF g[of i]] by auto
  then have [simp]: ‹NO_MATCH 0 i ⟹ pget_all_init_clss (g i) = pget_all_init_clss (g 0)› for i
    by (induction i) auto
  have star: ‹pcdcl_stgy_only_restart** (g 0) (g i)› for i
    by (induction i)
      (use g in ‹auto intro: rtranclp.intros›)

  let ?U = ‹pget_all_learned_clss (g 0)›
  define i j where
    ‹i ≡ 4 ^ (card (atms_of_mm (pget_all_init_clss (g 0)))) + size (pget_all_learned_clss (g 0)) + 1› and
    ‹j ≡ i + size (pget_all_learned_clss (g 0))›
  have ‹size (pget_all_learned_clss (g (Suc i))) > size (pget_all_learned_clss (g i))› for i
    using g[of i] by (auto simp: pcdcl_stgy_only_restart.simps pcdcl_restart_only.simps
      dest!: tranclp_into_rtranclp rtranclp_pcdcl_tcore_stgy_pget_all_learned_clss_mono)
  then have ‹size (pget_all_learned_clss (g i)) ≥ i› for i
    by (induction i) (auto simp add: Suc_leI le_less_trans)
  from this[of j] have ‹size (pget_all_learned_clss (g j) - pget_all_learned_clss (g 0)) ≥ i›
    unfolding i_def j_def
    by (meson add_le_imp_le_diff diff_size_le_size_Diff le_trans)
  moreover have ‹size (pget_all_learned_clss (g j) - pget_all_learned_clss (g 0))
    ≤ i - 1› for j
    using rtranclp_pcdcl_stgy_only_restart_bound_size[OF star[of j] inv inv'] by (auto simp: i_def)
  ultimately show False
    using not_less_eq_eq by (metis Suc_eq_plus1 add_diff_cancel_right' i_def)
qed


lemma pcdcl_core_stgy_pget_all_init_clss:
  ‹pcdcl_core_stgy S T ⟹ atms_of_mm (pget_all_init_clss S) =
    atms_of_mm (pget_all_init_clss T)›
  by (auto simp: pcdcl_tcore_stgy.simps pcdcl_core_stgy.simps cdcl_conflict.simps
    cdcl_propagate.simps cdcl_decide.simps cdcl_backtrack_unit.simps cdcl_skip.simps
    cdcl_resolve.simps cdcl_backtrack.simps cdcl_subsumed.simps cdcl_flush_unit.simps)

lemma cdcl_unitres_true_all_init_clss:
  ‹cdcl_unitres_true S T ⟹ (pget_all_init_clss S) = (pget_all_init_clss T)›
  by (induction rule: cdcl_unitres_true.induct) auto

lemma pcdcl_stgy_pget_all_init_clss:
  ‹pcdcl_stgy S T ⟹ pcdcl_all_struct_invs S ⟹ atms_of_mm (pget_all_init_clss S) =
    atms_of_mm (pget_all_init_clss T)›
  by (induction rule: pcdcl_stgy.induct)
    (auto dest!: tranclp_into_rtranclp rtranclp_pcdcl_tcore_stgy_pget_all_init_clss
    simp: pcdcl_restart.simps pcdcl_core_stgy_pget_all_init_clss cdcl_inp_propagate.simps
    cdcl_inp_conflict.simps pcdcl_all_struct_invs_def
    cdclW_restart_mset.cdclW_all_struct_inv_def
    cdclW_restart_mset.no_strange_atm_def
    cdcl_learn_clause.simps cdcl_resolution.simps cdcl_subsumed.simps cdcl_flush_unit.simps
    cdcl_unitres_true_all_init_clss)

lemma rtranclp_pcdcl_stgy_pget_all_init_clss:
  ‹pcdcl_stgy** S T ⟹ pcdcl_all_struct_invs S ⟹
  atms_of_mm (pget_all_init_clss S) = atms_of_mm (pget_all_init_clss T)›
  by (induction rule: rtranclp_induct)
   (auto dest: pcdcl_stgy_pget_all_init_clss rtranclp_pcdcl_all_struct_invs
    dest!: rtranclp_pcdcl_stgy_pcdcl)

lemma pcdcl_tcore_pget_all_init_clss:
  ‹pcdcl_tcore S T ⟹ pget_all_init_clss S = pget_all_init_clss T›
  by (auto simp: pcdcl_tcore.simps pcdcl_core.simps cdcl_conflict.simps
    cdcl_propagate.simps cdcl_decide.simps cdcl_backtrack_unit.simps cdcl_skip.simps
    cdcl_resolve.simps cdcl_backtrack.simps cdcl_subsumed.simps cdcl_flush_unit.simps)

lemma rtranclp_pcdcl_tcore_pget_all_init_clss:
  ‹pcdcl_tcore** S T ⟹ pget_all_init_clss S = pget_all_init_clss T›
  by (induction rule: rtranclp_induct) (auto dest!: pcdcl_tcore_pget_all_init_clss)

lemma pcdcl_core_pget_all_init_clss:
  ‹pcdcl_core S T ⟹ pget_all_init_clss S = pget_all_init_clss T›
  by (auto simp: pcdcl_core.simps pcdcl_core.simps cdcl_conflict.simps
    cdcl_propagate.simps cdcl_decide.simps cdcl_backtrack_unit.simps cdcl_skip.simps
    cdcl_resolve.simps cdcl_backtrack.simps cdcl_subsumed.simps cdcl_flush_unit.simps)

lemma rtranclp_pcdcl_core_pget_all_init_clss:
  ‹pcdcl_core** S T ⟹ pget_all_init_clss S = pget_all_init_clss T›
  by (induction rule: rtranclp_induct) (auto dest!: pcdcl_core_pget_all_init_clss)

lemma pcdcl_pget_all_init_clss:
  ‹pcdcl S T ⟹ pcdcl_all_struct_invs S ⟹  atms_of_mm (pget_all_init_clss S) =
    atms_of_mm (pget_all_init_clss T)›
  by (induction rule: pcdcl.induct)
   (auto dest!: tranclp_into_rtranclp rtranclp_pcdcl_tcore_pget_all_init_clss
      pcdcl_core_pget_all_init_clss
    simp: pcdcl_restart.simps pcdcl_core_stgy_pget_all_init_clss cdcl_inp_propagate.simps
        cdcl_inp_conflict.simps
    cdcl_learn_clause.simps cdcl_resolution.simps cdcl_subsumed.simps cdcl_flush_unit.simps
    cdcl_unitres_true_all_init_clss cdcl_pure_literal_remove.simps
    cdcl_inp_conflict.simps pcdcl_all_struct_invs_def
    cdclW_restart_mset.cdclW_all_struct_inv_def cdcl_promote_false.simps
    cdclW_restart_mset.no_strange_atm_def
    dest!: multi_member_split)

lemma rtranclp_pcdcl_pget_all_init_clss:
  ‹pcdcl** S T ⟹ pcdcl_all_struct_invs S ⟹  atms_of_mm (pget_all_init_clss S) =
  atms_of_mm (pget_all_init_clss T)›
  by (induction rule: rtranclp_induct)
   (auto dest!: pcdcl_pget_all_init_clss rtranclp_pcdcl_all_struct_invs)


lemma pcdcl_inprocessing_pget_all_init_clss:
  ‹pcdcl_inprocessing S T ⟹ pcdcl_all_struct_invs S ⟹
    atms_of_mm (pget_all_init_clss T) = atms_of_mm (pget_all_init_clss S)›
  by (induction rule: pcdcl_inprocessing.induct)
   (auto dest!: rtranclp_pcdcl_stgy_pget_all_init_clss rtranclp_pcdcl_pget_all_init_clss pcdcl_pget_all_init_clss
    simp: pcdcl_restart.simps pcdcl_restart_only.simps)

lemma pcdcl_inprocessing_pcdcl_all_struct_invs:
  ‹pcdcl_inprocessing S T ⟹ pcdcl_all_struct_invs S ⟹ pcdcl_all_struct_invs T›
  by (cases rule: pcdcl_inprocessing.cases, assumption)
    (blast dest: pcdcl_all_struct_invs pcdcl_restart_pcdcl_all_struct_invs)+

lemma rtranclp_pcdcl_inprocessing_pcdcl_all_struct_invs:
  ‹pcdcl_inprocessing** S T ⟹ pcdcl_all_struct_invs S ⟹ pcdcl_all_struct_invs T›
  by (induction rule: rtranclp_induct)
    (blast dest: pcdcl_inprocessing_pcdcl_all_struct_invs)+

lemma rtranclp_pcdcl_inprocessing_pget_all_init_clss:
  ‹pcdcl_inprocessing** S T ⟹ pcdcl_all_struct_invs S ⟹atms_of_mm (pget_all_init_clss T) = atms_of_mm (pget_all_init_clss S)›
  by (induction rule: rtranclp_induct)
   (auto dest!: pcdcl_inprocessing_pget_all_init_clss
    dest: pcdcl_inprocessing_pget_all_init_clss rtranclp_pcdcl_inprocessing_pcdcl_all_struct_invs)

context twl_restart_ops
begin
lemma pcdcl_stgy_restart_pget_all_init_clss:
  ‹pcdcl_stgy_restart S T ⟹ pcdcl_all_struct_invs (current_state S) ⟹
    atms_of_mm (pget_all_init_clss (last_restart_state S)) = atms_of_mm (pget_all_init_clss (current_state S)) ⟹
    atms_of_mm (pget_all_init_clss (last_GC_state S)) = atms_of_mm (pget_all_init_clss (current_state S)) ⟹
  atms_of_mm (pget_all_init_clss (current_state T)) = atms_of_mm (pget_all_init_clss (current_state S)) ∧
  atms_of_mm (pget_all_init_clss (last_restart_state T)) = atms_of_mm (pget_all_init_clss (current_state S)) ∧
  atms_of_mm (pget_all_init_clss (last_GC_state T)) = atms_of_mm (pget_all_init_clss (current_state S))›
  apply (induction rule: pcdcl_stgy_restart.induct)
  apply (simp add: pcdcl_tcore_stgy_pget_all_init_clss)
  apply simp
  apply (metis (full_types) pcdcl_inprocessing.intros(2) pcdcl_inprocessing_pcdcl_all_struct_invs
    pcdcl_inprocessing_pget_all_init_clss rtranclp_pcdcl_inprocessing_pcdcl_all_struct_invs
    rtranclp_pcdcl_inprocessing_pget_all_init_clss rtranclp_pcdcl_stgy_pget_all_init_clss)
  apply simp
  apply (smt pcdcl_restart_only.cases pget_all_init_clss.simps)
  apply simp
  done

definition pcdcl_stgy_restart_inv :: ‹'v prag_st_restart ⇒ bool› where
  ‹pcdcl_stgy_restart_inv = (λ(Q, R, S, m, n). pcdcl_all_struct_invs Q ∧
  cdclW_restart_mset.no_smaller_propa (state_of Q) ∧
  pcdcl_stgy_only_restart** Q R ∧ pcdcl_tcore_stgy** R S)›

lemma pcdcl_stgy_restart_inv_alt_def:
  ‹pcdcl_stgy_restart_inv = (λ(Q, R, S, m, n). pcdcl_all_struct_invs Q ∧
  cdclW_restart_mset.no_smaller_propa (state_of Q) ∧ pcdcl_all_struct_invs R ∧
  cdclW_restart_mset.no_smaller_propa (state_of R) ∧  pcdcl_all_struct_invs S ∧
  cdclW_restart_mset.no_smaller_propa (state_of S) ∧
  pcdcl_stgy_only_restart** Q R ∧ pcdcl_tcore_stgy** R S)›
  (is ‹_ = ?P›)
proof -
  have pcdcl_stgy_restart_inv_alt_def:
    ‹pcdcl_stgy_restart_inv (Q, R, S, m, n) ⟷ ?P (Q, R, S, m, n)› for Q R S m n
    unfolding pcdcl_stgy_restart_inv_def
    by (auto simp add: rtranclp_pcdcl_stgy_only_restart_all_struct_invs
      rtranclp_pcdcl_stgy_only_restart_all_struct_invs rtranclp_pcdcl_tcore_stgy_all_struct_invs
      dest: rtranclp_pcdcl_stgy_only_restart_no_smaller_propa rtranclp_pcdcl_tcore_stgy_no_smaller_propa)
  then show ?thesis
    by blast
qed

lemma no_smaller_propa_lvl0:
  ‹count_decided (pget_trail U) = 0 ⟹ cdclW_restart_mset.no_smaller_propa (state_of U)›
  by (auto simp add: cdclW_restart_mset.no_smaller_propa_def)

lemma pcdcl_stgy_restart_pcdcl_stgy_restart_inv:
  assumes ‹pcdcl_stgy_restart S T›‹pcdcl_stgy_restart_inv S›
  shows ‹pcdcl_stgy_restart_inv T›
  using assms apply -
  apply (induction rule: pcdcl_stgy_restart.induct)
  subgoal
    by (auto simp add: pcdcl_stgy_restart_inv_def dest!: tranclp_into_rtranclp
    dest: pcdcl_restart_only_pcdcl_all_struct_invs rtranclp_pcdcl_tcore_stgy_all_struct_invs
    rtranclp_pcdcl_stgy_pcdcl pcdcl_restart_pcdcl_all_struct_invs rtranclp_pcdcl_all_struct_invs
      rtranclp_pcdcl_stgy_only_restart_all_struct_invs rtranclp_pcdcl_tcore_stgy_no_smaller_propa
      rtranclp_pcdcl_stgy_only_restart_no_smaller_propa pcdcl_restart_no_smaller_propa'
      rtranclp_pcdcl_stgy_no_smaller_propa)
  subgoal for T R n U W S m
    apply (subst (asm) pcdcl_stgy_restart_inv_alt_def)
    unfolding pcdcl_stgy_restart_inv_def prod.case
    apply normalize_goal+
    apply (rule conjI)
    using pcdcl_restart_pcdcl_all_struct_invs rtranclp_pcdcl_all_struct_invs rtranclp_pcdcl_inprocessing_pcdcl_all_struct_invs
      rtranclp_pcdcl_stgy_pcdcl apply blast
    apply simp
    using pcdcl_restart_no_smaller_propa' pcdcl_restart_pcdcl_all_struct_invs rtranclp_pcdcl_stgy_no_smaller_propa
      rtranclp_pcdcl_inprocessing_pcdcl_all_struct_invs
    by blast
  subgoal for T S U R n
    apply (subst (asm) pcdcl_stgy_restart_inv_alt_def)
    unfolding pcdcl_stgy_restart_inv_def prod.case
    apply normalize_goal+
    apply (rule conjI)
    apply simp
    apply (rule conjI)
    apply simp
    apply (rule conjI)
    apply (metis (no_types, lifting) Nitpick.rtranclp_unfold nat_neq_iff
      pcdcl_stgy_only_restart.restart_noGC_step rtranclp.simps)
    apply blast
    done
  subgoal for T R S n
    unfolding pcdcl_stgy_restart_inv_def prod.case
    by auto
  done


lemma rtranclp_pcdcl_stgy_restart_pcdcl_stgy_restart_inv:
  assumes ‹pcdcl_stgy_restart** S T›‹pcdcl_stgy_restart_inv S›
  shows ‹pcdcl_stgy_restart_inv T›
  using assms
  by (induction rule: rtranclp_induct)
    (auto dest!: pcdcl_stgy_restart_pcdcl_stgy_restart_inv)

lemma pcdcl_stgy_restart_current_number:
  ‹pcdcl_stgy_restart S T ⟹ current_number S ≤ current_number T›
  by (induction rule: pcdcl_stgy_restart.induct) auto

lemma rtranclp_pcdcl_stgy_restart_current_number:
  ‹pcdcl_stgy_restart** S T ⟹ current_number S ≤ current_number T›
  by (induction rule: rtranclp_induct) (auto dest: pcdcl_stgy_restart_current_number)

lemma pcdcl_stgy_restart_no_GC_either:
  ‹pcdcl_stgy_restart S T ⟹ pcdcl_stgy_restart_inv S ⟹
  current_number T = current_number S ⟹
  (last_restart_state T = current_state T ∧ pcdcl_stgy_only_restart (last_restart_state S) (current_state T)) ∨
  (last_restart_state S = last_restart_state T ∧ pcdcl_tcore_stgy (current_state S) (current_state T)) ∨
  (last_restart_state S = last_restart_state T ∧ (current_state S) = (current_state T)  ∧ ¬restart_continue T)›
  using pcdcl_stgy_restart_pcdcl_stgy_restart_inv[of S T]
  apply simp
  apply (induction rule: pcdcl_stgy_restart.induct)
  subgoal
    by (simp add: pcdcl_stgy_restart_inv_def case_prod_beta)
  subgoal
    by (simp add: pcdcl_stgy_restart_inv_def case_prod_beta)
  subgoal for T S U R m n
    using restart_noGC_stepI[of S T U]
    by (auto simp add: pcdcl_stgy_restart_inv_def)
  subgoal for T R S m n
    using restart_noGC_stepI[of S T U]
    by (auto simp add: pcdcl_stgy_restart_inv_def)
  done

lemma rtranclp_pcdcl_stgy_restart_decomp:
  ‹pcdcl_stgy_restart** S T ⟹ pcdcl_stgy_restart_inv S ⟹
  current_number T = current_number S ⟹ pcdcl_stgy_only_restart** (current_state S) (last_restart_state S) ⟹
  pcdcl_stgy_only_restart** (current_state S) (last_restart_state T) ∧ pcdcl_tcore_stgy** (last_restart_state T) (current_state T)›
  apply (induction rule: rtranclp_induct)
  subgoal
    by (simp add: pcdcl_stgy_restart_inv_def case_prod_beta)
  subgoal for T U
    using rtranclp_pcdcl_stgy_restart_current_number[of S T] pcdcl_stgy_restart_current_number[of T U]
      pcdcl_stgy_restart_no_GC_either[of T U] rtranclp_pcdcl_stgy_restart_pcdcl_stgy_restart_inv[of S T]
    by (auto)
  done

lemma
  assumes ‹pcdcl_stgy_restart** S T› and
    inv: ‹pcdcl_stgy_restart_inv S› and
    ‹current_number T = current_number S› and
    ‹pcdcl_stgy_only_restart** (current_state S) (last_restart_state S)› and
    ‹distinct_mset (pget_all_learned_clss (current_state S) - A)›
  shows
    rtranclp_pcdcl_stgy_restart_distinct_mset:
    ‹distinct_mset (pget_all_learned_clss (current_state T) - A)› (is ?dist) and
    rtranclp_pcdcl_stgyrestart_bound:
      ‹card (set_mset (pget_all_learned_clss (current_state T) - A))
      ≤ 4 ^ (card (atms_of_mm (pget_all_init_clss (current_state S))))› (is ?A) and
    rtranclp_pcdcl_stgy_restart_bound_size:
      ‹size (pget_all_learned_clss (current_state T) - A)
      ≤ 4 ^ (card (atms_of_mm (pget_all_init_clss (current_state S))))› (is ?B)
proof -
  let ?S = ‹current_state S›
  let ?T = ‹last_restart_state T›
  let ?U = ‹current_state T›
  have ST: ‹pcdcl_stgy_only_restart** ?S ?T› and
    TU: ‹pcdcl_tcore_stgy** ?T ?U›
    using rtranclp_pcdcl_stgy_restart_decomp[OF assms(1-4)] by fast+

  have inv_T: ‹pcdcl_stgy_restart_inv T›
    using assms(1) inv rtranclp_pcdcl_stgy_restart_pcdcl_stgy_restart_inv by blast
  have dist: ‹distinct_mset (pget_all_learned_clss ?T - A)›
    by (rule rtranclp_cdcl_twl_stgy_restart_new_abs'[OF ST])
     (use inv in ‹auto simp: pcdcl_stgy_restart_inv_def assms(5)
       rtranclp_pcdcl_tcore_stgy_all_struct_invs
      dest: rtranclp_pcdcl_stgy_only_restart_all_struct_invs
      rtranclp_pcdcl_stgy_only_restart_no_smaller_propa rtranclp_pcdcl_tcore_stgy_no_smaller_propa›)

  have inv_T': ‹pcdcl_all_struct_invs ?T›
    by (smt ST inv pcdcl_stgy_restart_inv_alt_def rtranclp_pcdcl_stgy_only_restart_all_struct_invs
      split_beta)
  then have ‹cdclW_restart_mset.cdclW_stgy** (state_of ?T) (state_of ?U)›
    using rtranclp_pcdcl_tcore_stgy_cdclW_stgy[OF TU]
    unfolding pcdcl_all_struct_invs_def
    by (auto dest!: tranclp_into_rtranclp)

  then have dist: ‹distinct_mset (learned_clss (state_of ?U) - (A))›
    apply (rule cdclW_restart_mset.rtranclp_cdclW_stgy_distinct_mset_clauses_new_abs)
    subgoal using inv_T' unfolding pcdcl_all_struct_invs_def by fast
    subgoal using inv_T unfolding pcdcl_stgy_restart_inv_alt_def by auto
    subgoal using dist by (cases S) simp
    done
  then show ‹?dist›
    by auto

  have SU: ‹pget_all_init_clss ?U = pget_all_init_clss ?S›
    by (metis ST TU rtranclp_pcdcl_stgy_only_restart_pget_all_init_clss rtranclp_pcdcl_tcore_stgy_pget_all_init_clss)
  let ?N = ‹atms_of_mm (pget_all_init_clss ?U)›
  have fin_N: ‹finite ?N›
    by auto
  have inv_U: ‹pcdcl_all_struct_invs ?U›
    using TU inv_T' rtranclp_pcdcl_tcore_stgy_all_struct_invs by blast
  then have ‹set_mset (pget_all_learned_clss ?U) ⊆ {C. atms_of C ⊆ ?N ∧ distinct_mset C}›
    by (auto simp: pcdcl_all_struct_invs_def cdclW_restart_mset.cdclW_all_struct_inv_def
      simple_clss_def cdclW_restart_mset.distinct_cdclW_state_def
      cdclW_restart_mset.no_strange_atm_def
      dest!: multi_member_split)
  from card_mono[OF _ this] have ‹card (set_mset (pget_all_learned_clss ?U)) ≤ 4 ^ (card ?N)›
    using card_simple_clss_with_tautology[OF fin_N] by simp
  then show ?A
    unfolding SU
    by (meson card_mono finite_set_mset in_diffD le_trans subsetI)
  then show ?B
    unfolding SU
    by (subst (asm) distinct_mset_size_eq_card[symmetric])
      (use dist in auto)
qed

lemma pcdcl_stgy_restart_mono:
  ‹pcdcl_stgy_restart S T ⟹ current_number S = current_number T ⟹
  pget_all_learned_clss (current_state S) ⊆# pget_all_learned_clss (current_state T)›
  by (induction rule: pcdcl_stgy_restart.induct)
   (auto simp: pcdcl_tcore_stgy.simps pcdcl_core_stgy.simps
    cdcl_conflict.simps cdcl_propagate.simps cdcl_decide.simps
    cdcl_skip.simps cdcl_resolve.simps cdcl_backtrack.simps
    cdcl_subsumed.simps cdcl_flush_unit.simps cdcl_backtrack_unit.simps
    pcdcl_restart_only.simps)

lemma rtranclp_pcdcl_stgy_restart_mono:
  ‹pcdcl_stgy_restart** S T ⟹current_number S = current_number T ⟹
  pget_all_learned_clss (current_state S) ⊆# pget_all_learned_clss (current_state T)›
  apply (induction rule: rtranclp_induct)
  subgoal by auto
  subgoal for T U
    using pcdcl_stgy_restart_mono[of T U]
      rtranclp_pcdcl_stgy_restart_current_number[of S T] pcdcl_stgy_restart_current_number[of T U]
    by auto
  done

end



text ‹

The termination proof contains the usual boilerplate that hide the real argument. The idea of the
proof is to consider an infinite chain of term‹pcdcl_stgy_restart›. From it:

   ▪ We know that have eventually to do a restart, as term‹pcdcl_tcore_stgy› terminates.

   ▪ Then, if there are no GC, as we will eventually restart we can extract a sequence of
   term‹pcdcl_stgy_only_restart›. That terminates, so we have to eventually GC.

  ▪ Finally, as term‹f› is unbounded, at some we have learned more clauses that admissible.

The proof is make more complicated by the extraction of the subsequences: we derive the subsequence
of indices term‹f'›, then by induction we prove properties on the subsequence.

›
context twl_restart
begin

theorem wf_pcdcl_twl_stgy_restart:
  ‹wf {(T, S :: 'v prag_st_restart). pcdcl_stgy_restart_inv S ∧ pcdcl_stgy_restart S T}›
proof (rule ccontr)
  assume ‹¬ ?thesis›
  then obtain g :: ‹nat ⇒ 'v prag_st_restart› where
    g: ‹⋀i. pcdcl_stgy_restart (g i) (g (Suc i))› and
    restart_inv: ‹⋀i. pcdcl_stgy_restart_inv (g i)›
    unfolding wf_iff_no_infinite_down_chain
    by fast
  then have
    inv: ‹⋀i. pcdcl_all_struct_invs (last_restart_state (g i))› and
    inv_c: ‹⋀i. pcdcl_all_struct_invs (current_state (g i))› and
    inv': ‹⋀i. cdclW_restart_mset.no_smaller_propa (state_of (last_restart_state (g i)))› and
    inv'_c: ‹⋀i. cdclW_restart_mset.no_smaller_propa (state_of (current_state (g i)))› and
    rest_decomp: ‹⋀i. pcdcl_tcore_stgy** (last_restart_state (g i)) (current_state (g i))› and
    rest_decomp2: ‹⋀i. pcdcl_stgy_only_restart** (last_GC_state (g i)) (last_restart_state (g i))›
    unfolding pcdcl_stgy_restart_inv_alt_def
    by (simp_all add: prod.case_eq_if)


  have [simp]: ‹NO_MATCH True c ⟹ g i = (a, a', a'', b, b', c) ⟷ g i = (a, a', a'', b, b', True) ∧ c = True›
    for i a b c a' a'' b'
    using g[of i]
    by (auto simp: pcdcl_stgy_restart.simps)
  have H: ‹restart_continue (g i) = True› for i
    by (cases ‹g i›) auto

  have n_mono: ‹current_number (g (Suc i)) = Suc (current_number (g i)) ∨
    current_number (g (Suc i)) = current_number (g i)› for i
    using g[of i] by (auto simp: pcdcl_stgy_restart.simps)
  have n_mono': ‹current_restart_count (g (Suc i)) = Suc (current_restart_count (g i)) ∨
    current_restart_count (g (Suc i)) = current_restart_count (g i)› for i
    using g[of i] by (auto simp: pcdcl_stgy_restart.simps)
  have will_eventually_Restart: ‹∃i>j. current_restart_count (g (Suc i)) ≠ current_restart_count (g i)›
    if no_GC: ‹⋀i. i > j ⟹ current_number (g (Suc i)) = (current_number (g i))›
    for j
  proof (rule ccontr)
    assume mono: ‹¬ ?thesis›
    have neq: ‹current_restart_count (g (Suc i)) = current_restart_count (g (Suc j))› if ‹i ≥ j› for i
      using that
      apply (induction rule:nat_induct_at_least)
      using le_Suc_eq mono n_mono apply auto[1]
      by (metis Suc_leD le_imp_less_Suc le_SucI mono n_mono)

    define f where ‹f i = current_state (g (Suc i + j))› for i
    have
      g: ‹pcdcl_tcore_stgy (f i) (f (Suc i))› and
      inv: ‹pcdcl_all_struct_invs (f i)› and
      inv': ‹cdclW_restart_mset.no_smaller_propa (state_of (f i))› for i
      defer
      using g[of ‹Suc (i+j)›] inv[of ‹Suc (i+j)›] inv'[of ‹Suc (i+j)›] neq[of ‹i+j›]
        neq[of ‹Suc (i+j)›] H[of ‹i+j+1›] inv_c[of ‹Suc (i+j)›] inv'_c[of ‹Suc (i+j)›]
      apply (auto simp: f_def pcdcl_stgy_restart.simps
        pcdcl_stgy_only_restart.simps Suc_le_eq pcdcl_stgy_restart.cases)[2]
      using g[of ‹Suc (i+j)›] inv[of ‹Suc (i+j)›] inv'[of ‹Suc (i+j)›] neq[of ‹i+j›]
        neq[of ‹Suc (i+j)›] H[of ‹i+j+1›]
      apply (cases rule: pcdcl_stgy_restart.cases)
      subgoal for T T' R S n
        by (auto simp: f_def pcdcl_stgy_only_restart.restart_noGC_step
          pcdcl_stgy_restart.simps pcdcl_stgy_only_restart.simps Suc_le_eq)
      subgoal for T R n U V S
        using no_GC[of ‹Suc (i + j)›]
        by (auto simp: f_def pcdcl_stgy_only_restart.restart_noGC_step
          pcdcl_stgy_restart.simps pcdcl_stgy_only_restart.simps Suc_le_eq)
      subgoal for T R n U V S
        by (auto simp: f_def pcdcl_stgy_only_restart.restart_noGC_step
          pcdcl_stgy_restart.simps pcdcl_stgy_only_restart.simps Suc_le_eq)
      subgoal
        by simp
      done
    then show False
      using wf_pcdcl_tcore_stgy unfolding wf_iff_no_infinite_down_chain by blast
  qed
  have will_eventually_GC: ‹∃i>j. current_number (g (Suc i)) = Suc (current_number (g i))› for j
  proof (rule ccontr)
    assume mono: ‹¬ ?thesis›
    have neq: ‹current_number (g (Suc i)) = current_number (g (Suc j))› if ‹i ≥ Suc j› for i
      using that
      apply (induction rule:nat_induct_at_least)
      using le_Suc_eq mono n_mono apply auto[1]
      by (metis Suc_leD le_imp_less_Suc le_SucI mono n_mono)

    define f' where
      ‹f' ≡ rec_nat (Suc j)
         (λ_ n. LEAST i. i > n ∧ current_restart_count (g (Suc i)) = Suc (current_restart_count (g i)))›
    then have [simp]: ‹f' 0 = Suc j› and f_Suc: ‹f' (Suc n) = (LEAST i. i > f' n ∧ current_restart_count (g (Suc i)) =
        Suc (current_restart_count (g i)))› for n
      by auto
    let ?f' = ‹λi. g (f' i)›
    have will_eventually_Restart:
      ‹j' > j ⟹ ∃ia>j'. current_restart_count (g (Suc ia)) ≠ (current_restart_count (g ia))› for j'
      by (rule will_eventually_Restart)
       (use less_trans mono n_mono in blast)
    have will_eventually_Restart:
      ‹∃ia>j'. current_restart_count (g (Suc ia)) = Suc (current_restart_count (g ia))› if ‹j' > j› for j'
      using will_eventually_Restart[of j', OF that] apply - apply normalize_goal+
      subgoal for x
        apply (rule_tac x=x in exI)
        using n_mono'[of x] mono[of ] that
        by auto
      done
    have
      f': ‹current_restart_count (g (Suc (f' (Suc i)))) = Suc (current_restart_count (g (f' (Suc i)))) ∧
        f' i < f' (Suc i) ∧ f' i > j› for i
      apply (induction i)
      subgoal
        using will_eventually_Restart[of ‹Suc j›]
          wellorder_class.LeastI_ex[of ‹λj'. j' > Suc j ∧ current_restart_count (g (Suc j')) = Suc (current_restart_count (g j'))›]
        unfolding f_Suc[symmetric]  ‹f' 0 = Suc j›[symmetric]
        by (auto)
      subgoal for i
        using will_eventually_Restart[of ‹f' (Suc i)›]
          wellorder_class.LeastI_ex[of ‹λj. j > f' (Suc i) ∧ current_restart_count (g (Suc j)) = Suc (current_restart_count (g j))›]
        unfolding f_Suc[symmetric, of ]
        by (auto)
      done
    then have
      f': ‹current_restart_count (g (Suc (f' (Suc i)))) = Suc (current_restart_count (g (f' (Suc i))))› and
      fii: ‹f' i < f' (Suc i)› and
      fj: ‹f' i > j› for i
      by fast+

    have same_res: ‹k < f' (Suc i) ⟹ k > f' i ⟹ last_restart_state (g (Suc (k))) = last_restart_state (g (k))› for i k
      using wellorder_class.not_less_Least[of ‹k› ‹λj. j > f' (i) ∧ current_restart_count (g (Suc j)) = Suc (current_restart_count (g j))›]
        g[of k] neq[of k] fj[of i] neq[of k] neq[of ‹k - 1›] unfolding f_Suc[symmetric]
      by (cases ‹Suc j ≤ k - Suc 0›) (auto elim!: pcdcl_stgy_restart.cases)
    have f'_less_diff[iff]: ‹¬ f' i < f' (Suc i) - Suc 0 ⟷ f' i = f' (Suc i) - Suc 0› for i
      using fii[of i] by auto
    have same_res': ‹k < f' (Suc i) ⟹ k > f' i ⟹ last_restart_state (g (Suc (k))) = last_restart_state (g (Suc (f' i)))› for i k
      apply (induction "k - f' i" arbitrary: k)
      subgoal by auto
      subgoal premises p for x k
        using p(1)[of ‹k - 1›] p(2-)
        by (cases k; cases ‹f' i < k›)
          (auto simp: same_res less_Suc_eq_le Suc_diff_le order_class.order.order_iff_strict)
      done

    have tcore_stgy: ‹k < f' (Suc i) ⟹ k > f' i ⟹ pcdcl_tcore_stgy (current_state (g k)) (current_state (g (Suc k)))› for i k
      using same_res[of k i] neq[of ‹k›] fj[of i] g[of ‹k›] mono neq[of ‹k - 1›]
      by (subgoal_tac ‹Suc j ≤ k - Suc 0›)
        (auto simp: pcdcl_stgy_restart.simps elim: pcdcl_restart_only.cases)

    have tcore_stgy: ‹k ≤ f' (Suc i) ⟹ k ≥ Suc (f' i) ⟹ pcdcl_tcore_stgy** (current_state (g (Suc (f' i)))) (current_state (g k))› for i k
      apply (induction "k - Suc (f' i)" arbitrary: k)
      subgoal by auto
      subgoal premises p for x k
        using p(1)[of ‹k-1›] p(2-) tcore_stgy[of ‹k-1› i]
        by (cases k; cases ‹f' i < k›)
          (force simp: same_res less_Suc_eq_le Suc_diff_le order_class.order.order_iff_strict)+
      done
    have fii0: ‹(f' i) ≤ f' (Suc i) - Suc 0› for i
      using fii[of i] fj[of i] by auto
    have curr_last: ‹current_state (g (Suc (f' (Suc i)))) = last_restart_state (g (Suc (f' (Suc i))))› for i
      using f'[of i] g[of ‹f' (Suc i)›]
      by (auto elim!: pcdcl_stgy_restart.cases)
    have tcore_stgy': ‹Suc (f' i) ≤ f' (Suc i) - Suc 0 ⟹pcdcl_tcore_stgy** (current_state (g (Suc (f' i)))) (current_state (g (f' (Suc i) - 1)))› for i
      using tcore_stgy[of ‹f' (Suc i) - 1› i] fii[of i] fii0[of i]
      by (auto)
    have [iff]: ‹f' (Suc i) < f' (Suc i) - Suc 0 ⟷ False › for i
      using fii[of i] by (cases ‹f' (Suc i)›) auto
    have tcore_stgy: ‹pcdcl_tcore_stgy** (current_state (g (Suc (f' i)))) (current_state (g (f' (Suc i))))› for i
      using tcore_stgy[of ‹f' (Suc i)› i] fii[of i] fii0[of i]
      by (auto)
    moreover have
      ‹size (pget_all_learned_clss (current_state (g (Suc (f' (Suc i)))))) < size (pget_all_learned_clss (current_state (g (f' (Suc (Suc i))))))› and
      ‹pcdcl_restart_only (current_state (g (f' (Suc (Suc i))))) (current_state (g (Suc (f' (Suc (Suc i))))))› for i
      defer
      subgoal SS
        using f'[of ‹Suc i›] g[of ‹f' (Suc (Suc i))›] curr_last[of i, symmetric]
          same_res'[of ‹f' (Suc i)› ‹Suc i›]
          rtranclp_pcdcl_tcore_stgy_pget_all_learned_clss_mono[OF tcore_stgy[of ‹Suc i›]]
        apply (auto elim!: pcdcl_stgy_restart.cases simp: )
        done
      subgoal
        using f'[of ‹Suc i›] g[of ‹f' (Suc (Suc i))›] curr_last[of i, symmetric]
          same_res'[of ‹f' (Suc (Suc i)) - 1› ‹Suc (i)›] fii[of ‹Suc i›]
          rtranclp_pcdcl_tcore_stgy_pget_all_learned_clss_mono[OF tcore_stgy[of ‹Suc i›]]
        by (cases ‹f' (Suc i) < f' (Suc (Suc i)) - Suc 0›)
          (auto elim!: pcdcl_stgy_restart.cases simp: pcdcl_restart_only.simps)
      done
    ultimately have ‹pcdcl_stgy_only_restart (current_state (g (Suc (f' (Suc i))))) (current_state (g (Suc (f' (Suc (Suc i))))))› for i
      by (rule restart_noGC_stepI)
    moreover have ‹pcdcl_all_struct_invs (current_state (g (Suc (f' (Suc i))))) ∧
      cdclW_restart_mset.no_smaller_propa (state_of (current_state (g (Suc (f' (Suc i))))))› for i
      using inv'_c inv_c by auto
    ultimately show False
      using wf_pcdcl_stgy_only_restart unfolding wf_iff_no_infinite_down_chain
      by fast
  qed


  define f' where ‹f' ≡ rec_nat 0 (λ_ n. LEAST i. i > n ∧ current_number (g (Suc i)) = Suc (current_number (g i)))›
  then have [simp]: ‹f' 0 = 0› and f_Suc: ‹f' (Suc n) = (LEAST i. i > f' n ∧ current_number (g (Suc i)) =
      Suc (current_number (g i)))› for n
    by auto
  let ?f' = ‹λi. g (f' i)›
  have
    f': ‹current_number (g (Suc (f' (Suc i)))) = Suc (current_number (g (f' (Suc i))))› and
    fii: ‹f' i < f' (Suc i)› for i
    using will_eventually_GC[of ‹f' i›]
      wellorder_class.LeastI_ex[of ‹λj. j > f' i ∧ current_number (g (Suc j)) = Suc (current_number (g j))›]
    unfolding f_Suc[symmetric, of i]
    by (auto)

  have H: ‹f' (Suc i) + k < f' (Suc (Suc i)) ⟹ k > 0 ⟹
    current_number (g (Suc (f' (Suc i) + k))) =  current_number (g (f' (Suc i) + k))› for k i
    using not_less_Least[of ‹f' (Suc i) + k›
      ‹λj. j > f' ((Suc i)) ∧ current_number (g (Suc j)) = Suc (current_number (g j))›]
      g[of ‹f' (Suc i) + k›] unfolding f_Suc[symmetric]
    by (auto simp: pcdcl_stgy_restart.simps)

  have in_between: ‹f' (Suc i) + k < f' (Suc (Suc i)) ⟹
    current_number (g (Suc (f' (Suc i) + k))) =  current_number (g (Suc (f' (Suc i))))› for k i
    apply (induction k)
    subgoal
      using H[of i 1] by auto
    subgoal for k
      using H[of i ‹Suc k›]
      by auto
    done

  have Hc: ‹f' (Suc i) + Suc k ≤ f' (Suc (Suc i)) ⟹
    last_GC_state (g (Suc (f' (Suc i) + k))) = last_restart_state (g (Suc (f' (Suc i))))› for k i
    apply (induction k)
    subgoal using f'[of i] g[of ‹f' (Suc i)›]
      by (auto simp: pcdcl_stgy_restart.simps)
    subgoal for k
      using H[of i ‹Suc k›] g[of ‹f' (Suc i) + Suc k›] unfolding f_Suc[symmetric]
      by (auto simp: pcdcl_stgy_restart.simps)
    done

  have [simp]: ‹f' (Suc (Suc i)) ≥ Suc (Suc 0)› for i
    by (metis (full_types) antisym_conv fii not_le not_less_eq_eq zero_less_Suc)

  have in_between_last_GC_state: ‹
    last_GC_state (g ((f' (Suc (Suc i))))) =  last_restart_state (g (Suc (f' (Suc i))))› for i
    apply (cases ‹f' (Suc (Suc i)) ≥ Suc (Suc (f' (Suc i)))›)
    using Hc[of i ‹f' (Suc (Suc i)) - f' (Suc i) - Suc (0)›] fii[of ‹Suc i›] fii[of i]
    by (auto simp: Suc_diff_Suc antisym_conv not_less_eq_eq)

  have f'_steps: ‹current_number (g ((f' (Suc (Suc i))))) = 1 + current_number (g ((f' (Suc i))))› for i
    using f'[of ‹Suc i›] f'[of ‹i›] in_between[of i ‹f' (Suc (Suc i)) - f' (Suc i) - 1›]
    apply (cases ‹f' (Suc (Suc i)) - Suc (f' (Suc i)) = 0›)
    apply auto
    by (metis Suc_lessI f' fii leD)
  have snd_f'_0: ‹current_number (g ((f' (Suc (Suc i))))) =  Suc i + current_number (g ((f' (Suc 0))))› for i
    apply (induction i)
    subgoal
      using f'_steps[of 0] by auto
    subgoal for i
      using f'_steps[of ‹Suc i›]
      by auto
    done
  have gstar: ‹j ≥ i ⟹ pcdcl_stgy_restart** (g i) (g j)› for i j
    apply (induction "j - i" arbitrary: i j)
    subgoal by auto
    subgoal
      by (metis (no_types, lifting) Suc_diff_Suc Suc_leI diff_Suc_1 g r_into_rtranclp
        rtranclp.rtrancl_into_rtrancl rtranclp_idemp zero_less_Suc zero_less_diff)
    done
  have f'star: ‹pcdcl_stgy_restart** (g (f' i + 1)) (?f' (Suc i))› for i
    by (rule gstar)
     (use fii in ‹auto simp: Suc_leI›)

  have curr_last[simp]: ‹(current_state (g (Suc (f' (Suc i))))) = (last_restart_state (g (Suc (f' (Suc i)))))› for i
    using g[of ‹f' (Suc i)›] f'[of i]
      by (auto simp: pcdcl_stgy_restart.simps)
  have size_clss:
     ‹size (pget_all_learned_clss (current_state (g (f' (Suc (Suc i))))) - pget_all_learned_clss (current_state (g (Suc (f' (Suc i))))))
    ≤ 4 ^ card (atms_of_mm (pget_all_init_clss (current_state (g (f' (Suc i) + 1)))))› for i
    by (rule rtranclp_pcdcl_stgy_restart_bound_size[OF f'star])
      (auto simp: restart_inv f' f'_steps)

  have ‹atms_of_mm (pget_all_init_clss (fst (g (Suc i)))) = atms_of_mm (pget_all_init_clss (fst (g i)))› for i
    using pcdcl_stgy_restart_pget_all_init_clss[OF g[of i]]
    by (metis inv_c rest_decomp rest_decomp2 rtranclp_pcdcl_stgy_only_restart_pget_all_init_clss
      rtranclp_pcdcl_tcore_stgy_pget_all_init_clss)
  then have atms_init[simp]: ‹NO_MATCH 0 i ⟹
      atms_of_mm (pget_all_init_clss (fst (g i))) = atms_of_mm (pget_all_init_clss (fst (g 0)))› for i
    by (induction i) auto
  {
     fix i
    have
      bound: ‹f (current_number (?f' (Suc (Suc i)))) + size (pget_all_learned_clss (last_GC_state (?f' (Suc (Suc i)))))
         < size (pget_all_learned_clss (current_state (?f' (Suc (Suc i)))))›
      using g[of ‹f' (Suc (Suc i))›] f'(1)[of ‹Suc i›]
      by (auto elim!: pcdcl_stgy_restart.cases)
    then have ‹f (current_number (?f' (Suc (Suc i)))) < size (pget_all_learned_clss (current_state (?f' (Suc (Suc i))))) - size (pget_all_learned_clss (last_GC_state (?f' (Suc (Suc i)))))›
      by linarith
    also have ‹... ≤ size (pget_all_learned_clss (current_state (?f' (Suc (Suc i)))) - pget_all_learned_clss (last_GC_state (?f' (Suc (Suc i)))))›
      using diff_size_le_size_Diff by blast
    also have ‹... ≤ 4 ^ card (atms_of_mm (pget_all_init_clss (current_state (g (f' (Suc i) + 1)))))›
      using size_clss[of i]
      by (auto simp: f'_steps f' in_between_last_GC_state)

  finally have
    bound: ‹f (current_number (?f' (Suc (Suc i)))) < 4 ^ card (atms_of_mm (pget_all_init_clss (current_state (g 0))))›
    apply auto
    by (metis NO_MATCH_def atms_init rest_decomp rest_decomp2
      rtranclp_pcdcl_stgy_only_restart_pget_all_init_clss rtranclp_pcdcl_tcore_stgy_pget_all_init_clss)
  } note bound = this[]
  moreover have ‹unbounded (λn. f (current_number (g (f' (Suc (Suc n))))))›
    unfolding bounded_def
    apply clarsimp
    subgoal for b
      using not_bounded_nat_exists_larger[OF f, of b ‹((current_number (g (f' (Suc (Suc 0))))))›] apply -
      apply normalize_goal+
      apply (rename_tac n, rule_tac x = ‹n - (Suc (current_number (g (f' ((Suc 0))))))› in exI)
      by (auto simp: snd_f'_0 intro: exI[of _ ‹_ - (Suc (current_number (g (f' ((Suc 0))))))›])
    done
  ultimately show False
    using le_eq_less_or_eq unfolding bounded_def by blast
qed

end

end