diff --git a/thys/Functional_Ordered_Resolution_Prover/Weighted_FO_Ordered_Resolution_Prover.thy b/thys/Functional_Ordered_Resolution_Prover/Weighted_FO_Ordered_Resolution_Prover.thy
--- a/thys/Functional_Ordered_Resolution_Prover/Weighted_FO_Ordered_Resolution_Prover.thy
+++ b/thys/Functional_Ordered_Resolution_Prover/Weighted_FO_Ordered_Resolution_Prover.thy
@@ -1,836 +1,836 @@
 (*  Title:       A Fair Ordered Resolution Prover for First-Order Clauses with Weights
     Author:      Anders Schlichtkrull <andschl at dtu.dk>, 2017
     Author:      Jasmin Blanchette <j.c.blanchette at vu.nl>, 2017
     Maintainer:  Anders Schlichtkrull <andschl at dtu.dk>
 *)
 
 section \<open>A Fair Ordered Resolution Prover for First-Order Clauses with Weights\<close>
 
 text \<open>
 The \<open>weighted_RP\<close> prover introduced below operates on finite multisets of clauses and
 organizes the multiset of processed clauses as a priority queue to ensure that inferences are
 performed in a fair manner, to guarantee completeness.
 \<close>
 
 theory Weighted_FO_Ordered_Resolution_Prover
   imports Ordered_Resolution_Prover.FO_Ordered_Resolution_Prover
 begin
 
 
 subsection \<open>Prover\<close>
 
 type_synonym 'a wclause = "'a clause \<times> nat"
 type_synonym 'a wstate = "'a wclause multiset \<times> 'a wclause multiset \<times> 'a wclause multiset \<times> nat"
 
 fun state_of_wstate :: "'a wstate \<Rightarrow> 'a state" where
   "state_of_wstate (N, P, Q, n) =
    (set_mset (image_mset fst N), set_mset (image_mset fst P), set_mset (image_mset fst Q))"
 
 locale weighted_FO_resolution_prover =
   FO_resolution_prover S subst_atm id_subst comp_subst renamings_apart atm_of_atms mgu less_atm
   for
     S :: "('a :: wellorder) clause \<Rightarrow> 'a clause" and
     subst_atm :: "'a \<Rightarrow> 's \<Rightarrow> 'a" and
     id_subst :: "'s" and
     comp_subst :: "'s \<Rightarrow> 's \<Rightarrow> 's" and
     renamings_apart :: "'a clause list \<Rightarrow> 's list" and
     atm_of_atms :: "'a list \<Rightarrow> 'a" and
     mgu :: "'a set set \<Rightarrow> 's option" and
     less_atm :: "'a \<Rightarrow> 'a \<Rightarrow> bool" +
   fixes
     weight :: "'a clause \<times> nat \<Rightarrow> nat"
   assumes
     weight_mono: "i < j \<Longrightarrow> weight (C, i) < weight (C, j)"
 begin
 
 abbreviation clss_of_wstate :: "'a wstate \<Rightarrow> 'a clause set" where
   "clss_of_wstate St \<equiv> clss_of_state (state_of_wstate St)"
 
 abbreviation N_of_wstate :: "'a wstate \<Rightarrow> 'a clause set" where
   "N_of_wstate St \<equiv> N_of_state (state_of_wstate St)"
 
 abbreviation P_of_wstate :: "'a wstate \<Rightarrow> 'a clause set" where
   "P_of_wstate St \<equiv> P_of_state (state_of_wstate St)"
 
 abbreviation Q_of_wstate :: "'a wstate \<Rightarrow> 'a clause set" where
   "Q_of_wstate St \<equiv> Q_of_state (state_of_wstate St)"
 
 fun wN_of_wstate :: "'a wstate \<Rightarrow> 'a wclause multiset" where
   "wN_of_wstate (N, P, Q, n) = N"
 
 fun wP_of_wstate :: "'a wstate \<Rightarrow> 'a wclause multiset" where
   "wP_of_wstate (N, P, Q, n) = P"
 
 fun wQ_of_wstate :: "'a wstate \<Rightarrow> 'a wclause multiset" where
   "wQ_of_wstate (N, P, Q, n) = Q"
 
 fun n_of_wstate :: "'a wstate \<Rightarrow> nat" where
   "n_of_wstate (N, P, Q, n) = n"
 
 lemma of_wstate_split[simp]:
   "(wN_of_wstate St, wP_of_wstate St, wQ_of_wstate St, n_of_wstate St) = St"
   by (cases St) auto
 
 abbreviation grounding_of_wstate :: "'a wstate \<Rightarrow> 'a clause set" where
   "grounding_of_wstate St \<equiv> grounding_of_state (state_of_wstate St)"
 
 abbreviation Liminf_wstate :: "'a wstate llist \<Rightarrow> 'a state" where
   "Liminf_wstate Sts \<equiv> Liminf_state (lmap state_of_wstate Sts)"
 
 lemma timestamp_le_weight: "n \<le> weight (C, n)"
   by (induct n, simp, metis weight_mono[of k "Suc k" for k] Suc_le_eq le_less le_trans)
 
 inductive weighted_RP :: "'a wstate \<Rightarrow> 'a wstate \<Rightarrow> bool" (infix "\<leadsto>\<^sub>w" 50) where
   tautology_deletion: "Neg A \<in># C \<Longrightarrow> Pos A \<in># C \<Longrightarrow> (N + {#(C, i)#}, P, Q, n) \<leadsto>\<^sub>w (N, P, Q, n)"
 | forward_subsumption: "D \<in># image_mset fst (P + Q) \<Longrightarrow> subsumes D C \<Longrightarrow>
     (N + {#(C, i)#}, P, Q, n) \<leadsto>\<^sub>w (N, P, Q, n)"
 | backward_subsumption_P: "D \<in># image_mset fst N \<Longrightarrow> C \<in># image_mset fst P \<Longrightarrow>
     strictly_subsumes D C \<Longrightarrow> (N, P, Q, n) \<leadsto>\<^sub>w (N, {#(E, k) \<in># P. E \<noteq> C#}, Q, n)"
 | backward_subsumption_Q: "D \<in># image_mset fst N \<Longrightarrow> strictly_subsumes D C \<Longrightarrow>
     (N, P, Q + {#(C, i)#}, n) \<leadsto>\<^sub>w (N, P, Q, n)"
 | forward_reduction: "D + {#L'#} \<in># image_mset fst (P + Q) \<Longrightarrow> - L = L' \<cdot>l \<sigma> \<Longrightarrow> D \<cdot> \<sigma> \<subseteq># C \<Longrightarrow>
     (N + {#(C + {#L#}, i)#}, P, Q, n) \<leadsto>\<^sub>w (N + {#(C, i)#}, P, Q, n)"
 | backward_reduction_P: "D + {#L'#} \<in># image_mset fst N \<Longrightarrow> - L = L' \<cdot>l \<sigma> \<Longrightarrow> D \<cdot> \<sigma> \<subseteq># C \<Longrightarrow>
     (\<forall>j. (C + {#L#}, j) \<in># P \<longrightarrow> j \<le> i) \<Longrightarrow>
     (N, P + {#(C + {#L#}, i)#}, Q, n) \<leadsto>\<^sub>w (N, P + {#(C, i)#}, Q, n)"
 | backward_reduction_Q: "D + {#L'#} \<in># image_mset fst N \<Longrightarrow> - L = L' \<cdot>l \<sigma> \<Longrightarrow> D \<cdot> \<sigma> \<subseteq># C \<Longrightarrow>
     (N, P, Q + {#(C + {#L#}, i)#}, n) \<leadsto>\<^sub>w (N, P + {#(C, i)#}, Q, n)"
 | clause_processing: "(N + {#(C, i)#}, P, Q, n) \<leadsto>\<^sub>w (N, P + {#(C, i)#}, Q, n)"
 | inference_computation: "(\<forall>(D, j) \<in># P. weight (C, i) \<le> weight (D, j)) \<Longrightarrow>
     N = mset_set ((\<lambda>D. (D, n)) ` concls_of
       (inference_system.inferences_between (ord_FO_\<Gamma> S) (set_mset (image_mset fst Q)) C)) \<Longrightarrow>
     ({#}, P + {#(C, i)#}, Q, n) \<leadsto>\<^sub>w (N, {#(D, j) \<in># P. D \<noteq> C#}, Q + {#(C, i)#}, Suc n)"
 
 lemma weighted_RP_imp_RP: "St \<leadsto>\<^sub>w St' \<Longrightarrow> state_of_wstate St \<leadsto> state_of_wstate St'"
 proof (induction rule: weighted_RP.induct)
   case (backward_subsumption_P D N C P Q n)
   show ?case
     by (rule arg_cong2[THEN iffD1, of _ _ _ _ "(\<leadsto>)", OF _ _
           RP.backward_subsumption_P[of D "fst ` set_mset N" C "fst ` set_mset P - {C}"
             "fst ` set_mset Q"]])
       (use backward_subsumption_P in auto)
 next
   case (inference_computation P C i N n Q)
   show ?case
      by (rule arg_cong2[THEN iffD1, of _ _ _ _ "(\<leadsto>)", OF _ _
            RP.inference_computation[of "fst ` set_mset N" "fst ` set_mset Q" C
              "fst ` set_mset P - {C}"]],
          use inference_computation(2) finite_ord_FO_resolution_inferences_between in
            \<open>auto simp: comp_def image_comp inference_system.inferences_between_def\<close>)
 qed (use RP.intros in simp_all)
 
 lemma final_weighted_RP: "\<not> ({#}, {#}, Q, n) \<leadsto>\<^sub>w St"
   by (auto elim: weighted_RP.cases)
 
 context
   fixes
     Sts :: "'a wstate llist"
   assumes
     full_deriv: "full_chain (\<leadsto>\<^sub>w) Sts" and
     empty_P0: "P_of_wstate (lhd Sts) = {}" and
     empty_Q0: "Q_of_wstate (lhd Sts) = {}"
 begin
 
 lemma finite_Sts0: "finite (clss_of_wstate (lhd Sts))"
   by (cases "lhd Sts") auto
 
 lemmas deriv = full_chain_imp_chain[OF full_deriv]
 lemmas lhd_lmap_Sts = llist.map_sel(1)[OF chain_not_lnull[OF deriv]]
 
 lemma deriv_RP: "chain (\<leadsto>) (lmap state_of_wstate Sts)"
   using deriv weighted_RP_imp_RP by (metis chain_lmap)
 
 lemma finite_Sts0_RP: "finite (clss_of_state (lhd (lmap state_of_wstate Sts)))"
   using finite_Sts0 chain_length_pos[OF deriv] by auto
 
 lemma empty_P0_RP: "P_of_state (lhd (lmap state_of_wstate Sts)) = {}"
   using empty_P0 chain_length_pos[OF deriv] by auto
 
 lemma empty_Q0_RP: "Q_of_state (lhd (lmap state_of_wstate Sts)) = {}"
   using empty_Q0 chain_length_pos[OF deriv] by auto
 
 lemmas Sts_thms = deriv_RP finite_Sts0_RP empty_P0_RP empty_Q0_RP
 
 theorem weighted_RP_model:
   "St \<leadsto>\<^sub>w St' \<Longrightarrow> I \<Turnstile>s grounding_of_wstate St' \<longleftrightarrow> I \<Turnstile>s grounding_of_wstate St"
   using RP_model Sts_thms weighted_RP_imp_RP by (simp only: comp_def)
 
 abbreviation S_gQ :: "'a clause \<Rightarrow> 'a clause" where
   "S_gQ \<equiv> S_Q (lmap state_of_wstate Sts)"
 
 interpretation sq: selection S_gQ
-  unfolding S_Q_def[OF deriv_RP] using S_M_selects_subseteq S_M_selects_neg_lits selection_axioms
+  unfolding S_Q_def using S_M_selects_subseteq S_M_selects_neg_lits selection_axioms
   by unfold_locales auto
 
 interpretation gd: ground_resolution_with_selection S_gQ
   by unfold_locales
 
 interpretation src: standard_redundancy_criterion_reductive gd.ord_\<Gamma>
   by unfold_locales
 
 interpretation src: standard_redundancy_criterion_counterex_reducing gd.ord_\<Gamma>
   "ground_resolution_with_selection.INTERP S_gQ"
   by unfold_locales
 
 lemmas ord_\<Gamma>_saturated_upto_def = src.saturated_upto_def
 lemmas ord_\<Gamma>_saturated_upto_complete = src.saturated_upto_complete
 lemmas ord_\<Gamma>_contradiction_Rf = src.contradiction_Rf
 
 theorem weighted_RP_sound:
   assumes "{#} \<in> clss_of_state (Liminf_wstate Sts)"
   shows "\<not> satisfiable (grounding_of_wstate (lhd Sts))"
   by (rule RP_sound[OF deriv_RP assms, unfolded lhd_lmap_Sts])
 
 abbreviation RP_filtered_measure :: "('a wclause \<Rightarrow> bool) \<Rightarrow> 'a wstate \<Rightarrow> nat \<times> nat \<times> nat" where
   "RP_filtered_measure \<equiv> \<lambda>p (N, P, Q, n).
      (sum_mset (image_mset (\<lambda>(C, i). Suc (size C)) {#Di \<in># N + P + Q. p Di#}),
       size {#Di \<in># N. p Di#}, size {#Di \<in># P. p Di#})"
 
 abbreviation RP_combined_measure :: "nat \<Rightarrow> 'a wstate \<Rightarrow> nat \<times> (nat \<times> nat \<times> nat) \<times> (nat \<times> nat \<times> nat)" where
   "RP_combined_measure \<equiv> \<lambda>w St.
      (w + 1 - n_of_wstate St, RP_filtered_measure (\<lambda>(C, i). i \<le> w) St,
       RP_filtered_measure (\<lambda>Ci. True) St)"
 
 abbreviation (input) RP_filtered_relation :: "((nat \<times> nat \<times> nat) \<times> (nat \<times> nat \<times> nat)) set" where
   "RP_filtered_relation \<equiv> natLess <*lex*> natLess <*lex*> natLess"
 
 abbreviation (input) RP_combined_relation :: "((nat \<times> ((nat \<times> nat \<times> nat) \<times> (nat \<times> nat \<times> nat))) \<times>
     (nat \<times> ((nat \<times> nat \<times> nat) \<times> (nat \<times> nat \<times> nat)))) set" where
   "RP_combined_relation \<equiv> natLess <*lex*> RP_filtered_relation <*lex*> RP_filtered_relation"
 
 abbreviation "(fst3 :: 'b * 'c * 'd \<Rightarrow> 'b) \<equiv> fst"
 abbreviation "(snd3 :: 'b * 'c * 'd \<Rightarrow> 'c) \<equiv> \<lambda>x. fst (snd x)"
 abbreviation "(trd3 :: 'b * 'c * 'd \<Rightarrow> 'd) \<equiv> \<lambda>x. snd (snd x)"
 
 lemma
   wf_RP_filtered_relation: "wf RP_filtered_relation" and
   wf_RP_combined_relation: "wf RP_combined_relation"
   unfolding natLess_def using wf_less wf_mult by auto
 
 lemma multiset_sum_of_Suc_f_monotone: "N \<subset># M \<Longrightarrow> (\<Sum>x \<in># N. Suc (f x)) < (\<Sum>x \<in># M. Suc (f x))"
 proof (induction N arbitrary: M)
   case empty
   then obtain y where "y \<in># M"
     by force
   then have "(\<Sum>x \<in># M. 1) = (\<Sum>x \<in># M - {#y#} + {#y#}. 1)"
     by auto
   also have "... = (\<Sum>x \<in># M - {#y#}. 1) + (\<Sum>x \<in># {#y#}. 1)"
     by (metis image_mset_union sum_mset.union)
   also have "... > (0 :: nat)"
     by auto
   finally have "0 < (\<Sum>x \<in># M. Suc (f x))"
     by (fastforce intro: gr_zeroI)
   then show ?case
     using empty by auto
 next
   case (add x N)
   from this(2) have "(\<Sum>y \<in># N. Suc (f y)) < (\<Sum>y \<in># M - {#x#}. Suc (f y))"
     using add(1)[of "M - {#x#}"] by (simp add: insert_union_subset_iff)
   moreover have "add_mset x (remove1_mset x M) = M"
     by (meson add.prems add_mset_remove_trivial_If mset_subset_insertD)
   ultimately show ?case
     by (metis (no_types) add.commute add_less_cancel_right sum_mset.insert)
 qed
 
 lemma multiset_sum_monotone_f':
   assumes "CC \<subset># DD"
   shows "(\<Sum>(C, i) \<in># CC. Suc (f C)) < (\<Sum>(C, i) \<in># DD. Suc (f C))"
   using multiset_sum_of_Suc_f_monotone[OF assms, of "f \<circ> fst"]
   by (metis (mono_tags) comp_apply image_mset_cong2 split_beta)
 
 lemma filter_mset_strict_subset:
   assumes "x \<in># M" and "\<not> p x"
   shows "{#y \<in># M. p y#} \<subset># M"
 proof -
   have subseteq: "{#E \<in># M. p E#} \<subseteq># M"
     by auto
   have "count {#E \<in># M. p E#} x = 0"
     using assms by auto
   moreover have "0 < count M x"
     using assms by auto
   ultimately have lt_count: "count {#y \<in># M. p y#} x < count M x"
     by auto
   then show ?thesis
     using subseteq by (metis less_not_refl2 subset_mset.le_neq_trans)
 qed
 
 lemma weighted_RP_measure_decreasing_N:
   assumes "St \<leadsto>\<^sub>w St'" and "(C, l) \<in># wN_of_wstate St"
   shows "(RP_filtered_measure (\<lambda>Ci. True) St', RP_filtered_measure (\<lambda>Ci. True) St)
     \<in> RP_filtered_relation"
 using assms proof (induction rule: weighted_RP.induct)
   case (backward_subsumption_P D N C' P Q n)
   then obtain i' where  "(C', i') \<in># P"
     by auto
   then have "{#(E, k) \<in># P. E \<noteq> C'#} \<subset># P"
     using filter_mset_strict_subset[of "(C', i')" P "\<lambda>X. \<not>fst X =  C'"]
     by (metis (mono_tags, lifting) filter_mset_cong fst_conv prod.case_eq_if)
   then have "(\<Sum>(C, i) \<in># {#(E, k) \<in># P. E \<noteq> C'#}. Suc (size C)) < (\<Sum>(C, i) \<in># P. Suc (size C))"
     using multiset_sum_monotone_f'[of "{#(E, k) \<in># P. E \<noteq> C'#}" P size] by metis
   then show ?case
     unfolding natLess_def by auto
 qed (auto simp: natLess_def)
 
 lemma weighted_RP_measure_decreasing_P:
   assumes "St \<leadsto>\<^sub>w St'" and "(C, i) \<in># wP_of_wstate St"
   shows "(RP_combined_measure (weight (C, i)) St', RP_combined_measure (weight (C, i)) St)
     \<in> RP_combined_relation"
 using assms proof (induction rule: weighted_RP.induct)
   case (backward_subsumption_P D N C' P Q n)
 
   define St where "St = (N, P, Q, n)"
   define P' where "P' = {#(E, k) \<in># P. E \<noteq> C'#}"
   define St' where "St' = (N, P', Q, n)"
 
   from backward_subsumption_P obtain i' where  "(C', i') \<in># P"
     by auto
   then have P'_sub_P: "P' \<subset># P"
     unfolding P'_def using filter_mset_strict_subset[of "(C', i')" P "\<lambda>Dj. fst Dj \<noteq> C'"]
     by (metis (no_types, lifting) filter_mset_cong fst_conv prod.case_eq_if)
 
   have P'_subeq_P_filter:
     "{#(Ca, ia) \<in># P'. ia \<le> weight (C, i)#} \<subseteq># {#(Ca, ia) \<in># P. ia \<le> weight (C, i)#}"
     using P'_sub_P by (auto intro: multiset_filter_mono)
 
   have "fst3 (RP_combined_measure (weight (C, i)) St')
     \<le> fst3 (RP_combined_measure (weight (C, i)) St)"
     unfolding St'_def St_def by auto
   moreover have "(\<Sum>(C, i) \<in># {#(Ca, ia) \<in># P'. ia \<le> weight (C, i)#}. Suc (size C))
     \<le> (\<Sum>x \<in># {#(Ca, ia) \<in># P. ia \<le> weight (C, i)#}. case x of (C, i) \<Rightarrow> Suc (size C))"
     using P'_subeq_P_filter by (rule sum_image_mset_mono)
   then have "fst3 (snd3 (RP_combined_measure (weight (C, i)) St'))
     \<le> fst3 (snd3 (RP_combined_measure (weight (C, i)) St))"
     unfolding St'_def St_def by auto
   moreover have "snd3 (snd3 (RP_combined_measure (weight (C, i)) St'))
     \<le> snd3 (snd3 (RP_combined_measure (weight (C, i)) St))"
     unfolding St'_def St_def by auto
   moreover from P'_subeq_P_filter have "size {#(Ca, ia) \<in># P'. ia \<le> weight (C, i)#}
     \<le> size {#(Ca, ia) \<in># P. ia \<le> weight (C, i)#}"
     by (simp add: size_mset_mono)
   then have "trd3 (snd3 (RP_combined_measure (weight (C, i)) St'))
     \<le> trd3 (snd3 (RP_combined_measure (weight (C, i)) St))"
     unfolding St'_def St_def unfolding fst_def snd_def by auto
   moreover from P'_sub_P have "(\<Sum>(C, i) \<in># P'. Suc (size C)) < (\<Sum>(C, i) \<in># P. Suc (size C))"
     using multiset_sum_monotone_f'[of "{#(E, k) \<in># P. E \<noteq> C'#}" P size] unfolding P'_def by metis
   then have "fst3 (trd3 (RP_combined_measure (weight (C, i)) St'))
     < fst3 (trd3 (RP_combined_measure (weight (C, i)) St))"
     unfolding P'_def St'_def St_def by auto
   ultimately show ?case
     unfolding natLess_def P'_def St'_def St_def by auto
 next
   case (inference_computation P C' i' N n Q)
   then show ?case
   proof (cases "n \<le> weight (C, i)")
     case True
     then have "weight (C, i) + 1 - n > weight (C, i) + 1 - Suc n"
       by auto
     then show ?thesis
       unfolding natLess_def by auto
   next
     case n_nle_w: False
 
     define St :: "'a wstate" where "St = ({#}, P + {#(C', i')#}, Q, n)"
     define St' :: "'a wstate" where "St' =  (N, {#(D, j) \<in># P. D \<noteq> C'#}, Q + {#(C', i')#}, Suc n)"
     define concls :: "'a wclause set" where
       "concls = (\<lambda>D. (D, n)) ` concls_of (inference_system.inferences_between (ord_FO_\<Gamma> S)
          (fst ` set_mset Q) C')"
 
     have fin: "finite concls"
       unfolding concls_def using finite_ord_FO_resolution_inferences_between by auto
 
     have "{(D, ia) \<in> concls. ia \<le> weight (C, i)} = {}"
       unfolding concls_def using n_nle_w by auto
     then have "{#(D, ia) \<in># mset_set concls. ia \<le> weight (C, i)#} = {#}"
       using fin filter_mset_empty_if_finite_and_filter_set_empty[of concls] by auto
     then have n_low_weight_empty: "{#(D, ia) \<in># N. ia \<le> weight (C, i)#} = {#}"
       unfolding inference_computation unfolding concls_def by auto
 
     have "weight (C', i') \<le> weight (C, i)"
       using inference_computation by auto
     then have i'_le_w_Ci: "i' \<le> weight (C, i)"
       using timestamp_le_weight[of i' C'] by auto
 
     have subs: "{#(D, ia) \<in># N + {#(D, j) \<in># P. D \<noteq> C'#} + (Q + {#(C', i')#}). ia \<le> weight (C, i)#}
       \<subseteq># {#(D, ia) \<in># {#} + (P + {#(C', i')#}) + Q. ia \<le> weight (C, i)#}"
       using n_low_weight_empty by (auto simp: multiset_filter_mono)
 
     have "fst3 (RP_combined_measure (weight (C, i)) St')
       \<le> fst3 (RP_combined_measure (weight (C, i)) St)"
       unfolding St'_def St_def by auto
     moreover have "fst (RP_filtered_measure ((\<lambda>(D, ia). ia \<le> weight (C, i))) St') =
       (\<Sum>(C, i) \<in># {#(D, ia) \<in># N + {#(D, j) \<in># P. D \<noteq> C'#} + (Q + {#(C', i')#}).
          ia \<le> weight (C, i)#}. Suc (size C))"
       unfolding St'_def by auto
     also have "... \<le> (\<Sum>(C, i) \<in># {#(D, ia) \<in># {#} + (P + {#(C', i')#}) + Q. ia \<le> weight (C, i)#}.
       Suc (size C))"
       using subs sum_image_mset_mono by blast
     also have "... = fst (RP_filtered_measure (\<lambda>(D, ia). ia \<le> weight (C, i)) St)"
       unfolding St_def by auto
     finally have "fst3 (snd3 (RP_combined_measure (weight (C, i)) St'))
       \<le> fst3 (snd3 (RP_combined_measure (weight (C, i)) St))"
       by auto
     moreover have "snd3 (snd3 (RP_combined_measure (weight (C, i)) St')) =
       snd3 (snd3 (RP_combined_measure (weight (C, i)) St))"
       unfolding St_def St'_def using n_low_weight_empty by auto
     moreover have "trd3 (snd3 (RP_combined_measure (weight (C, i)) St')) <
       trd3 (snd3 (RP_combined_measure (weight (C, i)) St))"
       unfolding St_def St'_def using i'_le_w_Ci
       by (simp add: le_imp_less_Suc multiset_filter_mono size_mset_mono)
     ultimately show ?thesis
       unfolding natLess_def St'_def St_def lex_prod_def by force
   qed
 qed (auto simp: natLess_def)
 
 lemma preserve_min_or_delete_completely:
   assumes "St \<leadsto>\<^sub>w St'" "(C, i) \<in># wP_of_wstate St"
     "\<forall>k. (C, k) \<in># wP_of_wstate St \<longrightarrow> i \<le> k"
   shows "(C, i) \<in># wP_of_wstate St' \<or> (\<forall>j. (C, j) \<notin># wP_of_wstate St')"
 using assms proof (induction rule: weighted_RP.induct)
   case (backward_reduction_P D L' N L \<sigma> C' P i' Q n)
   show ?case
   proof (cases "C = C' + {#L#}")
     case True_outer: True
     then have C_i_in: "(C, i) \<in># P + {#(C, i')#}"
       using backward_reduction_P by auto
     then have max: "\<And>k. (C, k) \<in># P + {#(C, i')#} \<Longrightarrow> k \<le> i'"
       using backward_reduction_P unfolding True_outer[symmetric] by auto
     then have "count (P + {#(C, i')#}) (C, i') \<ge> 1"
       by auto
     moreover
     {
       assume asm: "count (P + {#(C, i')#}) (C, i') = 1"
       then have nin_P: "(C, i') \<notin># P"
         using not_in_iff by force
       have ?thesis
       proof (cases "(C, i) = (C, i')")
         case True
         then have "i = i'"
           by auto
         then have "\<forall>j. (C, j) \<in># P + {#(C, i')#} \<longrightarrow> j = i'"
           using max backward_reduction_P(6) unfolding True_outer[symmetric] by force
         then show ?thesis
           using True_outer[symmetric] nin_P by auto
       next
         case False
         then show ?thesis
           using C_i_in by auto
       qed
     }
     moreover
     {
       assume "count (P + {#(C, i')#}) (C, i') > 1"
       then have ?thesis
         using C_i_in by auto
     }
     ultimately show ?thesis
       by (cases "count (P + {#(C, i')#}) (C, i') = 1") auto
   next
     case False
     then show ?thesis
       using backward_reduction_P by auto
   qed
 qed auto
 
 lemma preserve_min_P:
   assumes
     "St \<leadsto>\<^sub>w St'" "(C, j) \<in># wP_of_wstate St'" and
     "(C, i) \<in># wP_of_wstate St" and
     "\<forall>k. (C, k) \<in># wP_of_wstate St \<longrightarrow> i \<le> k"
   shows "(C, i) \<in># wP_of_wstate St'"
   using assms preserve_min_or_delete_completely by blast
 
 lemma preserve_min_P_Sts:
   assumes
     "enat (Suc k) < llength Sts" and
     "(C, i) \<in># wP_of_wstate (lnth Sts k)" and
     "(C, j) \<in># wP_of_wstate (lnth Sts (Suc k))" and
     "\<forall>j. (C, j) \<in># wP_of_wstate (lnth Sts k) \<longrightarrow> i \<le> j"
   shows "(C, i) \<in># wP_of_wstate (lnth Sts (Suc k))"
   using deriv assms chain_lnth_rel preserve_min_P by metis
 
 lemma in_lnth_in_Supremum_ldrop:
   assumes "i < llength xs" and "x \<in># (lnth xs i)"
   shows "x \<in> Sup_llist (lmap set_mset (ldrop (enat i) xs))"
   using assms by (metis (no_types) ldrop_eq_LConsD ldropn_0 llist.simps(13) contra_subsetD
       ldrop_enat ldropn_Suc_conv_ldropn lnth_0 lnth_lmap lnth_subset_Sup_llist)
 
 lemma persistent_wclause_in_P_if_persistent_clause_in_P:
   assumes "C \<in> Liminf_llist (lmap P_of_state (lmap state_of_wstate Sts))"
   shows "\<exists>i. (C, i) \<in> Liminf_llist (lmap (set_mset \<circ> wP_of_wstate) Sts)"
 proof -
   obtain t_C where t_C_p:
     "enat t_C < llength Sts"
     "\<And>t. t_C \<le> t \<Longrightarrow> t < llength Sts \<Longrightarrow> C \<in> P_of_state (state_of_wstate (lnth Sts t))"
     using assms unfolding Liminf_llist_def by auto
   then obtain i where i_p:
     "(C, i) \<in># wP_of_wstate (lnth Sts t_C)"
     using t_C_p by (cases "lnth Sts t_C") force
 
   have Ci_in_nth_wP: "\<exists>i. (C, i) \<in># wP_of_wstate (lnth Sts (t_C + t))" if "t_C + t < llength Sts"
     for t
     using that t_C_p(2)[of "t_C + _"] by (cases "lnth Sts (t_C + t)") force
 
   define in_Sup_wP :: "nat \<Rightarrow> bool" where
     "in_Sup_wP = (\<lambda>i. (C, i) \<in> Sup_llist (lmap (set_mset \<circ> wP_of_wstate) (ldrop t_C Sts)))"
 
   have "in_Sup_wP i"
     using i_p assms(1) in_lnth_in_Supremum_ldrop[of t_C "lmap wP_of_wstate Sts" "(C, i)"] t_C_p
     by (simp add: in_Sup_wP_def llist.map_comp)
   then obtain j where j_p: "is_least in_Sup_wP j"
     unfolding in_Sup_wP_def[symmetric] using least_exists by metis
   then have "\<forall>i. (C, i) \<in> Sup_llist (lmap (set_mset \<circ> wP_of_wstate) (ldrop t_C Sts)) \<longrightarrow> j \<le> i"
     unfolding is_least_def in_Sup_wP_def using not_less by blast
   then have j_smallest:
     "\<And>i t. enat (t_C + t) < llength Sts \<Longrightarrow> (C, i) \<in># wP_of_wstate (lnth Sts (t_C + t)) \<Longrightarrow> j \<le> i"
     unfolding comp_def
     by (smt add.commute ldrop_enat ldrop_eq_LConsD ldrop_ldrop ldropn_Suc_conv_ldropn
         plus_enat_simps(1)  lnth_ldropn Sup_llist_def UN_I ldrop_lmap llength_lmap lnth_lmap
         mem_Collect_eq)
   from j_p have "\<exists>t_Cj. t_Cj < llength (ldrop (enat t_C) Sts)
     \<and> (C, j) \<in># wP_of_wstate (lnth (ldrop t_C Sts) t_Cj)"
     unfolding in_Sup_wP_def Sup_llist_def is_least_def by simp
   then obtain t_Cj where j_p:
     "(C,j) \<in># wP_of_wstate (lnth Sts (t_C + t_Cj))"
     "enat (t_C + t_Cj) < llength Sts"
     by (smt add.commute ldrop_enat ldrop_eq_LConsD ldrop_ldrop ldropn_Suc_conv_ldropn
         plus_enat_simps(1) lhd_ldropn)
   have Ci_stays:
     "t_C + t_Cj + t < llength Sts \<Longrightarrow> (C,j) \<in># wP_of_wstate (lnth Sts (t_C + t_Cj + t))" for t
   proof (induction t)
     case 0
     then show ?case
       using j_p by (simp add: add.commute)
   next
     case (Suc t)
     have any_Ck_in_wP: "j \<le> k" if "(C, k) \<in># wP_of_wstate (lnth Sts (t_C + t_Cj + t))" for k
       using that j_p j_smallest Suc
       by (smt Suc_ile_eq add.commute add.left_commute add_Suc less_imp_le plus_enat_simps(1)
           the_enat.simps)
     from Suc have Cj_in_wP: "(C, j) \<in># wP_of_wstate (lnth Sts (t_C + t_Cj + t))"
       by (metis (no_types, hide_lams) Suc_ile_eq add.commute add_Suc_right less_imp_le)
     moreover have "C \<in> P_of_state (state_of_wstate (lnth Sts (Suc (t_C + t_Cj + t))))"
       using t_C_p(2) Suc.prems by auto
     then have "\<exists>k. (C, k) \<in># wP_of_wstate (lnth Sts (Suc (t_C + t_Cj + t)))"
       by (smt Suc.prems Ci_in_nth_wP add.commute add.left_commute add_Suc_right enat_ord_code(4))
     ultimately have "(C, j) \<in># wP_of_wstate (lnth Sts (Suc (t_C + t_Cj + t)))"
       using preserve_min_P_Sts Cj_in_wP any_Ck_in_wP Suc.prems by force
     then have "(C, j) \<in># lnth (lmap wP_of_wstate Sts) (Suc (t_C + t_Cj + t))"
       using Suc.prems by auto
     then show ?case
       by (smt Suc.prems add.commute add_Suc_right lnth_lmap)
   qed
   then have "(\<And>t. t_C + t_Cj \<le> t \<Longrightarrow> t < llength (lmap (set_mset \<circ> wP_of_wstate) Sts) \<Longrightarrow>
     (C, j) \<in># wP_of_wstate (lnth Sts t))"
     using Ci_stays[of "_ - (t_C + t_Cj)"] by (metis le_add_diff_inverse llength_lmap)
   then have "(C, j) \<in> Liminf_llist (lmap (set_mset \<circ> wP_of_wstate) Sts)"
     unfolding Liminf_llist_def using j_p by auto
   then show "\<exists>i. (C, i) \<in> Liminf_llist (lmap (set_mset \<circ> wP_of_wstate) Sts)"
     by auto
 qed
 
 lemma lfinite_not_LNil_nth_llast:
   assumes "lfinite Sts" and "Sts \<noteq> LNil"
   shows "\<exists>i < llength Sts. lnth Sts i = llast Sts \<and> (\<forall>j < llength Sts. j \<le> i)"
 using assms proof (induction rule: lfinite.induct)
   case (lfinite_LConsI xs x)
   then show ?case
   proof (cases "xs = LNil")
     case True
     show ?thesis
       using True zero_enat_def by auto
   next
     case False
     then obtain i where
       i_p: "enat i < llength xs \<and> lnth xs i = llast xs \<and> (\<forall>j < llength xs. j \<le> enat i)"
       using lfinite_LConsI by auto
     then have "enat (Suc i) < llength (LCons x xs)"
       by (simp add: Suc_ile_eq)
     moreover from i_p have "lnth (LCons x xs) (Suc i) = llast (LCons x xs)"
       by (metis gr_implies_not_zero llast_LCons llength_lnull lnth_Suc_LCons)
     moreover from i_p have "\<forall>j < llength (LCons x xs). j \<le> enat (Suc i)"
       by (metis antisym_conv2 eSuc_enat eSuc_ile_mono ileI1 iless_Suc_eq llength_LCons)
     ultimately show ?thesis
       by auto
   qed
 qed auto
 
 lemma fair_if_finite:
   assumes fin: "lfinite Sts"
   shows "fair_state_seq (lmap state_of_wstate Sts)"
 proof (rule ccontr)
   assume unfair: "\<not> fair_state_seq (lmap state_of_wstate Sts)"
 
   have no_inf_from_last: "\<forall>y. \<not> llast Sts \<leadsto>\<^sub>w y"
     using fin full_chain_iff_chain[of "(\<leadsto>\<^sub>w)" Sts] full_deriv by auto
 
   from unfair obtain C where
     "C \<in> Liminf_llist (lmap N_of_state (lmap state_of_wstate Sts))
        \<union> Liminf_llist (lmap P_of_state (lmap state_of_wstate Sts))"
     unfolding fair_state_seq_def Liminf_state_def by auto
   then obtain i where i_p:
     "enat i < llength Sts"
     "\<And>j. i \<le> j \<Longrightarrow> enat j < llength Sts \<Longrightarrow>
      C \<in> N_of_state (state_of_wstate (lnth Sts j)) \<union> P_of_state (state_of_wstate (lnth Sts j))"
     unfolding Liminf_llist_def by auto
 
   have C_in_llast:
     "C \<in> N_of_state (state_of_wstate (llast Sts)) \<union> P_of_state (state_of_wstate (llast Sts))"
   proof -
     obtain l where
       l_p: "enat l < llength Sts \<and> lnth Sts l = llast Sts \<and> (\<forall>j < llength Sts. j \<le> enat l)"
       using fin lfinite_not_LNil_nth_llast i_p(1) by fastforce
     then have
       "C \<in> N_of_state (state_of_wstate (lnth Sts l)) \<union> P_of_state (state_of_wstate (lnth Sts l))"
       using i_p(1) i_p(2)[of l] by auto
     then show ?thesis
       using l_p by auto
   qed
 
   define N :: "'a wclause multiset" where "N = wN_of_wstate (llast Sts)"
   define P :: "'a wclause multiset" where "P = wP_of_wstate (llast Sts)"
   define Q :: "'a wclause multiset" where "Q = wQ_of_wstate (llast Sts)"
   define n :: nat where "n = n_of_wstate (llast Sts)"
 
   {
     assume "N_of_state (state_of_wstate (llast Sts)) \<noteq> {}"
     then obtain D j where "(D, j) \<in># N"
       unfolding N_def by (cases "llast Sts") auto
     then have "llast Sts \<leadsto>\<^sub>w (N - {#(D, j)#}, P + {#(D, j)#}, Q, n)"
       using weighted_RP.clause_processing[of "N - {#(D, j)#}" D j P Q n]
       unfolding N_def P_def Q_def n_def by auto
     then have "\<exists>St'. llast Sts \<leadsto>\<^sub>w St'"
       by auto
   }
   moreover
   {
     assume a: "N_of_state (state_of_wstate (llast Sts)) = {}"
     then have b: "N = {#}"
       unfolding N_def by (cases "llast Sts") auto
     from a have "C \<in> P_of_state (state_of_wstate (llast Sts))"
       using C_in_llast by auto
     then obtain D j where "(D, j) \<in># P"
       unfolding P_def by (cases "llast Sts") auto
     then have "weight (D, j) \<in> weight ` set_mset P"
       by auto
     then have "\<exists>w. is_least (\<lambda>w. w \<in> (weight ` set_mset P)) w"
       using least_exists by auto
     then have "\<exists>D j. (\<forall>(D', j') \<in># P. weight (D, j) \<le> weight (D', j')) \<and> (D, j) \<in># P"
       using assms linorder_not_less unfolding is_least_def by (auto 6 0)
     then obtain D j where
       min: "(\<forall>(D', j') \<in># P. weight (D, j) \<le> weight (D', j'))" and
       Dj_in_p: "(D, j) \<in># P"
       by auto
     from min have min: "(\<forall>(D', j') \<in># P - {#(D, j)#}. weight (D, j) \<le> weight (D', j'))"
       using mset_subset_diff_self[OF Dj_in_p] by auto
 
     define N' where
       "N' = mset_set ((\<lambda>D'. (D', n)) ` concls_of (inference_system.inferences_between (ord_FO_\<Gamma> S)
          (set_mset (image_mset fst Q)) D))"
 
     have "llast Sts \<leadsto>\<^sub>w (N', {#(D', j') \<in># P - {#(D, j)#}. D' \<noteq> D#}, Q + {#(D,j)#}, Suc n)"
       using weighted_RP.inference_computation[of "P - {#(D, j)#}" D j N' n Q, OF min N'_def]
         of_wstate_split[symmetric, of "llast Sts"] Dj_in_p
       unfolding N_def[symmetric] P_def[symmetric] Q_def[symmetric] n_def[symmetric] b by auto
     then have "\<exists>St'. llast Sts \<leadsto>\<^sub>w St'"
       by auto
   }
   ultimately have "\<exists>St'. llast Sts \<leadsto>\<^sub>w St'"
     by auto
   then show False
     using no_inf_from_last by metis
 qed
 
 lemma N_of_state_state_of_wstate_wN_of_wstate:
   assumes "C \<in> N_of_state (state_of_wstate St)"
   shows "\<exists>i. (C, i) \<in># wN_of_wstate St"
   by (smt N_of_state.elims assms eq_fst_iff fstI fst_conv image_iff of_wstate_split set_image_mset
       state_of_wstate.simps)
 
 lemma in_wN_of_wstate_in_N_of_wstate: "(C, i) \<in># wN_of_wstate St \<Longrightarrow> C \<in> N_of_wstate St"
   by (metis (mono_guards_query_query) N_of_state.simps fst_conv image_eqI of_wstate_split
       set_image_mset state_of_wstate.simps)
 
 lemma in_wP_of_wstate_in_P_of_wstate: "(C, i) \<in># wP_of_wstate St \<Longrightarrow> C \<in> P_of_wstate St"
   by (metis (mono_guards_query_query) P_of_state.simps fst_conv image_eqI of_wstate_split
       set_image_mset state_of_wstate.simps)
 
 lemma in_wQ_of_wstate_in_Q_of_wstate: "(C, i) \<in># wQ_of_wstate St \<Longrightarrow> C \<in> Q_of_wstate St"
   by (metis (mono_guards_query_query) Q_of_state.simps fst_conv image_eqI of_wstate_split
       set_image_mset state_of_wstate.simps)
 
 lemma n_of_wstate_weighted_RP_increasing: "St \<leadsto>\<^sub>w St' \<Longrightarrow> n_of_wstate St \<le> n_of_wstate St'"
   by (induction rule: weighted_RP.induct) auto
 
 lemma nth_of_wstate_monotonic:
   assumes "j < llength Sts" and "i \<le> j"
   shows "n_of_wstate (lnth Sts i) \<le> n_of_wstate (lnth Sts j)"
 using assms proof (induction "j - i" arbitrary: i)
   case (Suc x)
   then have "x = j - (i + 1)"
     by auto
   then have "n_of_wstate (lnth Sts (i + 1)) \<le> n_of_wstate (lnth Sts j)"
     using Suc by auto
   moreover have "i < j"
     using Suc by auto
   then have "Suc i < llength Sts"
     using Suc by (metis enat_ord_simps(2) le_less_Suc_eq less_le_trans not_le)
   then have "lnth Sts i \<leadsto>\<^sub>w lnth Sts (Suc i)"
     using deriv chain_lnth_rel[of "(\<leadsto>\<^sub>w)" Sts i] by auto
   then have "n_of_wstate (lnth Sts i) \<le> n_of_wstate (lnth Sts (i + 1))"
     using n_of_wstate_weighted_RP_increasing[of "lnth Sts i" "lnth Sts (i + 1)"] by auto
   ultimately show ?case
     by auto
 qed auto
 
 lemma infinite_chain_relation_measure:
   assumes
     measure_decreasing: "\<And>St St'. P St \<Longrightarrow> R St St' \<Longrightarrow> (m St', m St) \<in> mR" and
     non_infer_chain: "chain R (ldrop (enat k) Sts)" and
     inf: "llength Sts = \<infinity>" and
     P: "\<And>i. P (lnth (ldrop (enat k) Sts) i)"
   shows "chain (\<lambda>x y. (x, y) \<in> mR)\<inverse>\<inverse> (lmap m (ldrop (enat k) Sts))"
 proof (rule lnth_rel_chain)
   show "\<not> lnull (lmap m (ldrop (enat k) Sts))"
     using assms by auto
 next
   from inf have ldrop_inf: "llength (ldrop (enat k) Sts) = \<infinity> \<and> \<not> lfinite (ldrop (enat k) Sts)"
     using inf by (auto simp: llength_eq_infty_conv_lfinite)
   {
     fix j :: "nat"
     define St where "St = lnth (ldrop (enat k) Sts) j"
     define St' where "St' = lnth (ldrop (enat k) Sts) (j + 1)"
     have P': "P St \<and> P St'"
       unfolding St_def St'_def using P by auto
     from ldrop_inf have "R St St'"
       unfolding St_def St'_def
       using non_infer_chain infinite_chain_lnth_rel[of "ldrop (enat k) Sts" R j] by auto
     then have "(m St', m St) \<in> mR"
       using measure_decreasing P' by auto
     then have "(lnth (lmap m (ldrop (enat k) Sts)) (j + 1), lnth (lmap m (ldrop (enat k) Sts)) j)
       \<in> mR"
       unfolding St_def St'_def using lnth_lmap
       by (smt enat.distinct(1) enat_add_left_cancel enat_ord_simps(4) inf ldrop_lmap llength_lmap
           lnth_ldrop plus_enat_simps(3))
   }
   then show "\<forall>j. enat (j + 1) < llength (lmap m (ldrop (enat k) Sts)) \<longrightarrow>
     (\<lambda>x y. (x, y) \<in> mR)\<inverse>\<inverse> (lnth (lmap m (ldrop (enat k) Sts)) j)
       (lnth (lmap m (ldrop (enat k) Sts)) (j + 1))"
     by blast
 qed
 
 theorem weighted_RP_fair: "fair_state_seq (lmap state_of_wstate Sts)"
 proof (rule ccontr)
   assume asm: "\<not> fair_state_seq (lmap state_of_wstate Sts)"
   then have inff: "\<not> lfinite Sts" using fair_if_finite
     by auto
   then have inf: "llength Sts = \<infinity>"
     using llength_eq_infty_conv_lfinite by auto
   from asm obtain C where
     "C \<in> Liminf_llist (lmap N_of_state (lmap state_of_wstate Sts))
        \<union> Liminf_llist (lmap P_of_state (lmap state_of_wstate Sts))"
     unfolding fair_state_seq_def Liminf_state_def by auto
   then show False
   proof
     assume "C \<in> Liminf_llist (lmap N_of_state (lmap state_of_wstate Sts))"
     then obtain x where "enat x < llength Sts"
       "\<forall>xa. x \<le> xa \<and> enat xa < llength Sts \<longrightarrow> C \<in> N_of_state (state_of_wstate (lnth Sts xa))"
       unfolding Liminf_llist_def by auto
     then have "\<exists>k. \<forall>j. k \<le> j \<longrightarrow> (\<exists>i. (C, i) \<in># wN_of_wstate (lnth Sts j))"
       unfolding Liminf_llist_def by (force simp add: inf N_of_state_state_of_wstate_wN_of_wstate)
     then obtain k where k_p:
       "\<And>j. k \<le> j \<Longrightarrow> \<exists>i. (C, i) \<in># wN_of_wstate (lnth Sts j)"
       unfolding Liminf_llist_def
       by auto
     have chain_drop_Sts: "chain (\<leadsto>\<^sub>w) (ldrop k Sts)"
       using deriv inf inff by (simp add: inf_chain_ldropn_chain ldrop_enat)
     have in_N_j: "\<And>j. \<exists>i. (C, i) \<in># wN_of_wstate (lnth (ldrop k Sts) j)"
       using k_p by (simp add: add.commute inf)
     then have "chain (\<lambda>x y. (x, y) \<in> RP_filtered_relation)\<inverse>\<inverse> (lmap (RP_filtered_measure (\<lambda>Ci. True))
       (ldrop k Sts))"
       using inff inf weighted_RP_measure_decreasing_N chain_drop_Sts
         infinite_chain_relation_measure[of "\<lambda>St. \<exists>i. (C, i) \<in># wN_of_wstate St" "(\<leadsto>\<^sub>w)"] by blast
     then show False
       using wfP_iff_no_infinite_down_chain_llist[of "\<lambda>x y. (x, y) \<in> RP_filtered_relation"]
         wf_RP_filtered_relation inff
       by (metis (no_types, lifting) inf_llist_lnth ldrop_enat_inf_llist lfinite_inf_llist
         lfinite_lmap wfPUNIVI wf_induct_rule)
   next
     assume asm: "C \<in> Liminf_llist (lmap P_of_state (lmap state_of_wstate Sts))"
     from asm obtain i where i_p:
       "enat i < llength Sts"
       "\<And>j. i \<le> j \<and> enat j < llength Sts \<Longrightarrow> C \<in> P_of_state (state_of_wstate (lnth Sts j))"
       unfolding Liminf_llist_def by auto
     then obtain i where "(C, i) \<in> Liminf_llist (lmap (set_mset \<circ> wP_of_wstate) Sts)"
       using persistent_wclause_in_P_if_persistent_clause_in_P[of C] using asm inf by auto
     then have "\<exists>l. \<forall>k \<ge> l. (C, i) \<in> (set_mset \<circ> wP_of_wstate) (lnth Sts k)"
       unfolding Liminf_llist_def using inff inf by auto
     then obtain k where k_p:
       "(\<forall>k'\<ge>k. (C, i) \<in> (set_mset \<circ> wP_of_wstate) (lnth Sts k'))"
       by blast
     have Ci_in: "\<forall>k'. (C, i) \<in> (set_mset \<circ> wP_of_wstate) (lnth (ldrop k Sts) k')"
       using k_p lnth_ldrop[of k _ Sts] inf inff by force
     then have Ci_inn: "\<forall>k'. (C, i) \<in># (wP_of_wstate) (lnth (ldrop k Sts) k')"
       by auto
     have "chain (\<leadsto>\<^sub>w) (ldrop k Sts)"
       using deriv inf_chain_ldropn_chain inf inff by (simp add: inf_chain_ldropn_chain ldrop_enat)
     then have "chain (\<lambda>x y. (x, y) \<in> RP_combined_relation)\<inverse>\<inverse>
       (lmap (RP_combined_measure (weight (C, i))) (ldrop k Sts))"
       using inff inf Ci_in weighted_RP_measure_decreasing_P
         infinite_chain_relation_measure[of "\<lambda>St. (C, i) \<in># wP_of_wstate St" "(\<leadsto>\<^sub>w)"
           "RP_combined_measure (weight (C, i))" ]
       by auto
     then show False
       using wfP_iff_no_infinite_down_chain_llist[of "\<lambda>x y. (x, y) \<in> RP_combined_relation"]
         wf_RP_combined_relation inff
       by (smt inf_llist_lnth ldrop_enat_inf_llist lfinite_inf_llist lfinite_lmap wfPUNIVI
           wf_induct_rule)
   qed
 qed
 
 corollary weighted_RP_saturated: "src.saturated_upto (Liminf_llist (lmap grounding_of_wstate Sts))"
   using RP_saturated_if_fair[OF deriv_RP weighted_RP_fair empty_Q0_RP, unfolded llist.map_comp]
   by simp
 
 corollary weighted_RP_complete:
   "\<not> satisfiable (grounding_of_wstate (lhd Sts)) \<Longrightarrow> {#} \<in> Q_of_state (Liminf_wstate Sts)"
   using RP_complete_if_fair[OF deriv_RP weighted_RP_fair empty_Q0_RP, simplified lhd_lmap_Sts] .
 
 end
 
 end
 
 locale weighted_FO_resolution_prover_with_size_timestamp_factors =
   FO_resolution_prover S subst_atm id_subst comp_subst renamings_apart atm_of_atms mgu less_atm
   for
     S :: "('a :: wellorder) clause \<Rightarrow> 'a clause" and
     subst_atm :: "'a \<Rightarrow> 's \<Rightarrow> 'a" and
     id_subst :: "'s" and
     comp_subst :: "'s \<Rightarrow> 's \<Rightarrow> 's" and
     renamings_apart :: "'a literal multiset list \<Rightarrow> 's list" and
     atm_of_atms :: "'a list \<Rightarrow> 'a" and
     mgu :: "'a set set \<Rightarrow> 's option" and
     less_atm :: "'a \<Rightarrow> 'a \<Rightarrow> bool" +
   fixes
     size_atm :: "'a \<Rightarrow> nat" and
     size_factor :: nat and
     timestamp_factor :: nat
   assumes
     timestamp_factor_pos: "timestamp_factor > 0"
 begin
 
 fun weight :: "'a wclause \<Rightarrow> nat" where
   "weight (C, i) = size_factor * size_multiset (size_literal size_atm) C + timestamp_factor * i"
 
 lemma weight_mono: "i < j \<Longrightarrow> weight (C, i) < weight (C, j)"
   using timestamp_factor_pos by simp
 
 declare weight.simps [simp del]
 
 sublocale wrp: weighted_FO_resolution_prover _ _ _ _ _ _ _ _ weight
   by unfold_locales (rule weight_mono)
 
 notation wrp.weighted_RP (infix "\<leadsto>\<^sub>w" 50)
 
 end
 
 end
diff --git a/thys/Ordered_Resolution_Prover/FO_Ordered_Resolution_Prover.thy b/thys/Ordered_Resolution_Prover/FO_Ordered_Resolution_Prover.thy
--- a/thys/Ordered_Resolution_Prover/FO_Ordered_Resolution_Prover.thy
+++ b/thys/Ordered_Resolution_Prover/FO_Ordered_Resolution_Prover.thy
@@ -1,1541 +1,1548 @@
 (*  Title:       An Ordered Resolution Prover for First-Order Clauses
     Author:      Anders Schlichtkrull <andschl at dtu.dk>, 2016, 2017
     Author:      Jasmin Blanchette <j.c.blanchette at vu.nl>, 2014, 2017
     Author:      Dmitriy Traytel <traytel at inf.ethz.ch>, 2014
     Maintainer:  Anders Schlichtkrull <andschl at dtu.dk>
 *)
 
 section \<open>An Ordered Resolution Prover for First-Order Clauses\<close>
 
 theory FO_Ordered_Resolution_Prover
   imports FO_Ordered_Resolution
 begin
 
 text \<open>
 This material is based on Section 4.3 (``A Simple Resolution Prover for First-Order Clauses'') of
 Bachmair and Ganzinger's chapter. Specifically, it formalizes the RP prover defined in Figure 5 and
 its related lemmas and theorems, including Lemmas 4.10 and 4.11 and Theorem 4.13 (completeness).
 \<close>
 
 definition is_least :: "(nat \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> bool" where
   "is_least P n \<longleftrightarrow> P n \<and> (\<forall>n' < n. \<not> P n')"
 
 lemma least_exists: "P n \<Longrightarrow> \<exists>n. is_least P n"
   using exists_least_iff unfolding is_least_def by auto
 
 text \<open>
 The following corresponds to page 42 and 43 of Section 4.3, from the explanation of RP to
 Lemma 4.10.
 \<close>
 
 type_synonym 'a state = "'a clause set \<times> 'a clause set \<times> 'a clause set"
 
 locale FO_resolution_prover =
   FO_resolution subst_atm id_subst comp_subst renamings_apart atm_of_atms mgu less_atm +
   selection S
   for
     S :: "('a :: wellorder) clause \<Rightarrow> 'a clause" and
     subst_atm :: "'a \<Rightarrow> 's \<Rightarrow> 'a" and
     id_subst :: "'s" and
     comp_subst :: "'s \<Rightarrow> 's \<Rightarrow> 's" and
     renamings_apart :: "'a clause list \<Rightarrow> 's list" and
     atm_of_atms :: "'a list \<Rightarrow> 'a" and
     mgu :: "'a set set \<Rightarrow> 's option" and
     less_atm :: "'a \<Rightarrow> 'a \<Rightarrow> bool" +
   assumes
     sel_stable: "\<And>\<rho> C. is_renaming \<rho> \<Longrightarrow> S (C \<cdot> \<rho>) = S C \<cdot> \<rho>" and
     less_atm_ground: "is_ground_atm A \<Longrightarrow> is_ground_atm B \<Longrightarrow> less_atm A B \<Longrightarrow> A < B"
 begin
 
 lemma ground_ord_resolve_ground:
   assumes
     CAs_p: "ground_resolution_with_selection.ord_resolve S CAs DA AAs As E" and
     ground_cas: "is_ground_cls_list CAs" and
     ground_da: "is_ground_cls DA"
   shows "is_ground_cls E"
 proof -
   have a1: "atms_of E \<subseteq> (\<Union>CA \<in> set CAs. atms_of CA) \<union> atms_of DA"
     using ground_resolution_with_selection.ord_resolve_atms_of_concl_subset[OF _ CAs_p]
       ground_resolution_with_selection.intro selection_axioms by blast
   {
     fix L :: "'a literal"
     assume "L \<in># E"
     then have "atm_of L \<in> atms_of E"
       by (meson atm_of_lit_in_atms_of)
     then have "is_ground_atm (atm_of L)"
       using a1 ground_cas ground_da is_ground_cls_imp_is_ground_atm is_ground_cls_list_def
       by auto
   }
   then show ?thesis
     unfolding is_ground_cls_def is_ground_lit_def by simp
 qed
 
 lemma ground_ord_resolve_imp_ord_resolve:
   assumes
     ground_da: \<open>is_ground_cls DA\<close> and
     ground_cas: \<open>is_ground_cls_list CAs\<close> and
     gr: "ground_resolution_with_selection S_G" and
     gr_res: \<open>ground_resolution_with_selection.ord_resolve S_G CAs DA AAs As E\<close>
   shows \<open>\<exists>\<sigma>. ord_resolve S_G CAs DA AAs As \<sigma> E\<close>
 proof (cases rule: ground_resolution_with_selection.ord_resolve.cases[OF gr gr_res])
   case (1 CAs n Cs AAs As D)
   note cas = this(1) and da = this(2) and aas = this(3) and as = this(4) and e = this(5) and
     cas_len = this(6) and cs_len = this(7) and aas_len = this(8) and as_len = this(9) and
     nz = this(10) and casi = this(11) and aas_not_empt = this(12) and as_aas = this(13) and
     eligibility = this(14) and str_max = this(15) and sel_empt = this(16)
 
   have len_aas_len_as: "length AAs = length As"
     using aas_len as_len by auto
 
   from as_aas have "\<forall>i < n. \<forall>A \<in># add_mset (As ! i) (AAs ! i). A = As ! i"
     by simp
   then have "\<forall>i < n. card (set_mset (add_mset (As ! i) (AAs ! i))) \<le> Suc 0"
     using all_the_same by metis
   then have "\<forall>i < length AAs. card (set_mset (add_mset (As ! i) (AAs ! i))) \<le> Suc 0"
     using aas_len by auto
   then have "\<forall>AA \<in> set (map2 add_mset As AAs). card (set_mset AA) \<le> Suc 0"
     using set_map2_ex[of AAs As add_mset, OF len_aas_len_as] by auto
   then have "is_unifiers id_subst (set_mset ` set (map2 add_mset As AAs))"
     unfolding is_unifiers_def is_unifier_def by auto
   moreover have "finite (set_mset ` set (map2 add_mset As AAs))"
     by auto
   moreover have "\<forall>AA \<in> set_mset ` set (map2 add_mset As AAs). finite AA"
     by auto
   ultimately obtain \<sigma> where
     \<sigma>_p: "Some \<sigma> = mgu (set_mset ` set (map2 add_mset As AAs))"
     using mgu_complete by metis
 
   have ground_elig: "ground_resolution_with_selection.eligible S_G As (D + negs (mset As))"
     using eligibility by simp
   have ground_cs: "\<forall>i < n. is_ground_cls (Cs ! i)"
     using cas cas_len cs_len casi ground_cas nth_mem unfolding is_ground_cls_list_def by force
   have ground_set_as: "is_ground_atms (set As)"
     using da ground_da by (metis atms_of_negs is_ground_cls_is_ground_atms_atms_of
         is_ground_cls_union set_mset_mset)
   then have ground_mset_as: "is_ground_atm_mset (mset As)"
     unfolding is_ground_atm_mset_def is_ground_atms_def by auto
   have ground_as: "is_ground_atm_list As"
     using ground_set_as is_ground_atm_list_def is_ground_atms_def by auto
   have ground_d: "is_ground_cls D"
     using ground_da da by simp
 
   from as_len nz have atms:
     "atms_of D \<union> set As \<noteq> {}"
     "finite (atms_of D \<union> set As)"
     by auto
   then have "Max (atms_of D \<union> set As) \<in> atms_of D \<union> set As"
     using Max_in by metis
   then have is_ground_Max: "is_ground_atm (Max (atms_of D \<union> set As))"
     using ground_d ground_mset_as is_ground_cls_imp_is_ground_atm
     unfolding is_ground_atm_mset_def by auto
 
   have "maximal_wrt (Max (atms_of D \<union> set As)) (D + negs (mset As))"
     unfolding maximal_wrt_def
     by clarsimp (metis atms Max_less_iff UnCI ground_d ground_set_as infinite_growing
         is_ground_Max is_ground_atms_def is_ground_cls_imp_is_ground_atm less_atm_ground)
   moreover have
     "Max (atms_of D \<union> set As) \<cdot>a \<sigma> = Max (atms_of D \<union> set As)" and
     "D \<cdot> \<sigma> + negs (mset As \<cdot>am \<sigma>) = D + negs (mset As)"
     using ground_elig is_ground_Max ground_mset_as ground_d by auto
   ultimately have fo_elig: "eligible S_G \<sigma> As (D + negs (mset As))"
     using ground_elig unfolding ground_resolution_with_selection.eligible.simps[OF gr]
       ground_resolution_with_selection.maximal_wrt_def[OF gr] eligible.simps
     by auto
 
   have "\<forall>i < n. strictly_maximal_wrt (As ! i) (Cs ! i)"
     using str_max[unfolded ground_resolution_with_selection.strictly_maximal_wrt_def[OF gr]]
       ground_as[unfolded is_ground_atm_list_def] ground_cs as_len less_atm_ground
     unfolding strictly_maximal_wrt_def by clarsimp (fastforce simp: is_ground_cls_as_atms)+
   then have ll: "\<forall>i < n. strictly_maximal_wrt (As ! i \<cdot>a \<sigma>) (Cs ! i \<cdot> \<sigma>)"
     by (simp add: ground_as ground_cs as_len)
 
   have ground_e: "is_ground_cls E"
     using ground_d ground_cs cs_len unfolding e is_ground_cls_def
     by simp (metis in_mset_sum_list2 in_set_conv_nth)
 
   show ?thesis
     using cas da aas as e ground_e ord_resolve.intros[OF cas_len cs_len aas_len as_len nz casi
         aas_not_empt \<sigma>_p fo_elig ll sel_empt]
     by auto
 qed
 
 fun N_of_state :: "'a state \<Rightarrow> 'a clause set" where
   "N_of_state (N, P, Q) = N"
 
 fun P_of_state :: "'a state \<Rightarrow> 'a clause set" where
   "P_of_state (N, P, Q) = P"
 
 text \<open>
 \<open>O\<close> denotes relation composition in Isabelle, so the formalization uses \<open>Q\<close> instead.
 \<close>
 
 fun Q_of_state :: "'a state \<Rightarrow> 'a clause set" where
   "Q_of_state (N, P, Q) = Q"
 
 abbreviation clss_of_state :: "'a state \<Rightarrow> 'a clause set" where
   "clss_of_state St \<equiv> N_of_state St \<union> P_of_state St \<union> Q_of_state St"
 
 abbreviation grounding_of_state :: "'a state \<Rightarrow> 'a clause set" where
   "grounding_of_state St \<equiv> grounding_of_clss (clss_of_state St)"
 
 interpretation ord_FO_resolution: inference_system "ord_FO_\<Gamma> S" .
 
 text \<open>
 The following inductive predicate formalizes the resolution prover in Figure 5.
 \<close>
 
 inductive RP :: "'a state \<Rightarrow> 'a state \<Rightarrow> bool" (infix "\<leadsto>" 50) where
   tautology_deletion: "Neg A \<in># C \<Longrightarrow> Pos A \<in># C \<Longrightarrow> (N \<union> {C}, P, Q) \<leadsto> (N, P, Q)"
 | forward_subsumption: "D \<in> P \<union> Q \<Longrightarrow> subsumes D C \<Longrightarrow> (N \<union> {C}, P, Q) \<leadsto> (N, P, Q)"
 | backward_subsumption_P: "D \<in> N \<Longrightarrow> strictly_subsumes D C \<Longrightarrow> (N, P \<union> {C}, Q) \<leadsto> (N, P, Q)"
 | backward_subsumption_Q: "D \<in> N \<Longrightarrow> strictly_subsumes D C \<Longrightarrow> (N, P, Q \<union> {C}) \<leadsto> (N, P, Q)"
 | forward_reduction: "D + {#L'#} \<in> P \<union> Q \<Longrightarrow> - L = L' \<cdot>l \<sigma> \<Longrightarrow> D \<cdot> \<sigma> \<subseteq># C \<Longrightarrow>
     (N \<union> {C + {#L#}}, P, Q) \<leadsto> (N \<union> {C}, P, Q)"
 | backward_reduction_P: "D + {#L'#} \<in> N \<Longrightarrow> - L = L' \<cdot>l \<sigma> \<Longrightarrow> D \<cdot> \<sigma> \<subseteq># C \<Longrightarrow>
     (N, P \<union> {C + {#L#}}, Q) \<leadsto> (N, P \<union> {C}, Q)"
 | backward_reduction_Q: "D + {#L'#} \<in> N \<Longrightarrow> - L = L' \<cdot>l \<sigma> \<Longrightarrow> D \<cdot> \<sigma> \<subseteq># C \<Longrightarrow>
     (N, P, Q \<union> {C + {#L#}}) \<leadsto> (N, P \<union> {C}, Q)"
 | clause_processing: "(N \<union> {C}, P, Q) \<leadsto> (N, P \<union> {C}, Q)"
 | inference_computation: "N = concls_of (ord_FO_resolution.inferences_between Q C) \<Longrightarrow>
     ({}, P \<union> {C}, Q) \<leadsto> (N, P, Q \<union> {C})"
 
 lemma final_RP: "\<not> ({}, {}, Q) \<leadsto> St"
   by (auto elim: RP.cases)
 
 definition Sup_state :: "'a state llist \<Rightarrow> 'a state" where
   "Sup_state Sts =
    (Sup_llist (lmap N_of_state Sts), Sup_llist (lmap P_of_state Sts),
     Sup_llist (lmap Q_of_state Sts))"
 
 definition Liminf_state :: "'a state llist \<Rightarrow> 'a state" where
   "Liminf_state Sts =
    (Liminf_llist (lmap N_of_state Sts), Liminf_llist (lmap P_of_state Sts),
     Liminf_llist (lmap Q_of_state Sts))"
 
 context
   fixes Sts Sts' :: "'a state llist"
   assumes Sts: "lfinite Sts" "lfinite Sts'" "\<not> lnull Sts" "\<not> lnull Sts'" "llast Sts' = llast Sts"
 begin
 
 lemma
   N_of_Liminf_state_fin: "N_of_state (Liminf_state Sts') = N_of_state (Liminf_state Sts)" and
   P_of_Liminf_state_fin: "P_of_state (Liminf_state Sts') = P_of_state (Liminf_state Sts)" and
   Q_of_Liminf_state_fin: "Q_of_state (Liminf_state Sts') = Q_of_state (Liminf_state Sts)"
   using Sts by (simp_all add: Liminf_state_def lfinite_Liminf_llist llast_lmap)
 
 lemma Liminf_state_fin: "Liminf_state Sts' = Liminf_state Sts"
   using N_of_Liminf_state_fin P_of_Liminf_state_fin Q_of_Liminf_state_fin
   by (simp add: Liminf_state_def)
 
 end
 
 context
   fixes Sts Sts' :: "'a state llist"
   assumes Sts: "\<not> lfinite Sts" "emb Sts Sts'"
 begin
 
 lemma
   N_of_Liminf_state_inf: "N_of_state (Liminf_state Sts') \<subseteq> N_of_state (Liminf_state Sts)" and
   P_of_Liminf_state_inf: "P_of_state (Liminf_state Sts') \<subseteq> P_of_state (Liminf_state Sts)" and
   Q_of_Liminf_state_inf: "Q_of_state (Liminf_state Sts') \<subseteq> Q_of_state (Liminf_state Sts)"
   using Sts by (simp_all add: Liminf_state_def emb_Liminf_llist_infinite emb_lmap)
 
 lemma clss_of_Liminf_state_inf:
   "clss_of_state (Liminf_state Sts') \<subseteq> clss_of_state (Liminf_state Sts)"
   using N_of_Liminf_state_inf P_of_Liminf_state_inf Q_of_Liminf_state_inf by blast
 
 end
 
 definition fair_state_seq :: "'a state llist \<Rightarrow> bool" where
   "fair_state_seq Sts \<longleftrightarrow> N_of_state (Liminf_state Sts) = {} \<and> P_of_state (Liminf_state Sts) = {}"
 
 text \<open>
 The following formalizes Lemma 4.10.
 \<close>
 
 context
   fixes Sts :: "'a state llist"
-  assumes deriv: "chain (\<leadsto>) Sts"
 begin
 
-lemmas lhd_lmap_Sts = llist.map_sel(1)[OF chain_not_lnull[OF deriv]]
-
 definition S_Q :: "'a clause \<Rightarrow> 'a clause" where
   "S_Q = S_M S (Q_of_state (Liminf_state Sts))"
 
 interpretation sq: selection S_Q
   unfolding S_Q_def using S_M_selects_subseteq S_M_selects_neg_lits selection_axioms
   by unfold_locales auto
 
 interpretation gr: ground_resolution_with_selection S_Q
   by unfold_locales
 
 interpretation sr: standard_redundancy_criterion_reductive gr.ord_\<Gamma>
   by unfold_locales
 
 interpretation sr: standard_redundancy_criterion_counterex_reducing gr.ord_\<Gamma>
   "ground_resolution_with_selection.INTERP S_Q"
   by unfold_locales
 
 text \<open>
 The extension of ordered resolution mentioned in 4.10. We let it consist of all sound rules.
 \<close>
 
 definition ground_sound_\<Gamma>:: "'a inference set" where
   "ground_sound_\<Gamma> = {Infer CC D E | CC D E. (\<forall>I. I \<Turnstile>m CC \<longrightarrow> I \<Turnstile> D \<longrightarrow> I \<Turnstile> E)}"
 
 text \<open>
 We prove that we indeed defined an extension.
 \<close>
 
 lemma gd_ord_\<Gamma>_ngd_ord_\<Gamma>: "gr.ord_\<Gamma> \<subseteq> ground_sound_\<Gamma>"
   unfolding ground_sound_\<Gamma>_def using gr.ord_\<Gamma>_def gr.ord_resolve_sound by fastforce
 
 lemma sound_ground_sound_\<Gamma>: "sound_inference_system ground_sound_\<Gamma>"
   unfolding sound_inference_system_def ground_sound_\<Gamma>_def by auto
 
 lemma sat_preserving_ground_sound_\<Gamma>: "sat_preserving_inference_system ground_sound_\<Gamma>"
   using sound_ground_sound_\<Gamma> sat_preserving_inference_system.intro
     sound_inference_system.\<Gamma>_sat_preserving by blast
 
 definition sr_ext_Ri :: "'a clause set \<Rightarrow> 'a inference set" where
   "sr_ext_Ri N = sr.Ri N \<union> (ground_sound_\<Gamma> - gr.ord_\<Gamma>)"
 
 interpretation sr_ext:
   sat_preserving_redundancy_criterion "ground_sound_\<Gamma>" "sr.Rf" "sr_ext_Ri"
   unfolding sat_preserving_redundancy_criterion_def sr_ext_Ri_def
   using sat_preserving_ground_sound_\<Gamma> redundancy_criterion_standard_extension gd_ord_\<Gamma>_ngd_ord_\<Gamma>
     sr.redundancy_criterion_axioms by auto
 
 lemma strict_subset_subsumption_redundant_clause:
   assumes
     sub: "D \<cdot> \<sigma> \<subset># C" and
     ground_\<sigma>: "is_ground_subst \<sigma>"
   shows "C \<in> sr.Rf (grounding_of_cls D)"
 proof -
   from sub have "\<forall>I. I \<Turnstile> D \<cdot> \<sigma> \<longrightarrow> I \<Turnstile> C"
     unfolding true_cls_def by blast
   moreover have "C > D \<cdot> \<sigma>"
     using sub by (simp add: subset_imp_less_mset)
   moreover have "D \<cdot> \<sigma> \<in> grounding_of_cls D"
     using ground_\<sigma> by (metis (mono_tags) mem_Collect_eq substitution_ops.grounding_of_cls_def)
   ultimately have "set_mset {#D \<cdot> \<sigma>#} \<subseteq> grounding_of_cls D"
     "(\<forall>I. I \<Turnstile>m {#D \<cdot> \<sigma>#} \<longrightarrow> I \<Turnstile> C)"
     "(\<forall>D'. D' \<in># {#D \<cdot> \<sigma>#} \<longrightarrow> D' < C)"
     by auto
   then show ?thesis
     using sr.Rf_def by blast
 qed
 
 lemma strict_subset_subsumption_redundant_clss:
   assumes
     "D \<cdot> \<sigma> \<subset># C" and
     "is_ground_subst \<sigma>" and
     "D \<in> CC"
   shows "C \<in> sr.Rf (grounding_of_clss CC)"
   using assms
 proof -
   have "C \<in> sr.Rf (grounding_of_cls D)"
     using strict_subset_subsumption_redundant_clause assms by auto
   then show ?thesis
     using assms unfolding grounding_of_clss_def
     by (metis (no_types) sr.Rf_mono sup_ge1 SUP_absorb contra_subsetD)
 qed
 
 lemma strict_subset_subsumption_grounding_redundant_clss:
   assumes
     D\<sigma>_subset_C: "D \<cdot> \<sigma> \<subset># C" and
     D_in_St: "D \<in> CC"
   shows "grounding_of_cls C \<subseteq> sr.Rf (grounding_of_clss CC)"
 proof
   fix C\<mu>
   assume "C\<mu> \<in> grounding_of_cls C"
   then obtain \<mu> where
     \<mu>_p: "C\<mu> = C \<cdot> \<mu> \<and> is_ground_subst \<mu>"
     unfolding grounding_of_cls_def by auto
   have D\<sigma>\<mu>C\<mu>: "D \<cdot> \<sigma> \<cdot> \<mu> \<subset># C \<cdot> \<mu>"
     using D\<sigma>_subset_C subst_subset_mono by auto
   then show "C\<mu> \<in> sr.Rf (grounding_of_clss CC)"
     using \<mu>_p strict_subset_subsumption_redundant_clss[of D "\<sigma> \<odot> \<mu>" "C \<cdot> \<mu>"] D_in_St by auto
 qed
 
 lemma subst_cls_eq_grounding_of_cls_subset_eq:
   assumes "D \<cdot> \<sigma> = C"
   shows "grounding_of_cls C \<subseteq> grounding_of_cls D"
 proof
   fix C\<sigma>'
   assume "C\<sigma>' \<in> grounding_of_cls C"
   then obtain \<sigma>' where
     C\<sigma>': "C \<cdot> \<sigma>' = C\<sigma>'" "is_ground_subst \<sigma>'"
     unfolding grounding_of_cls_def by auto
   then have "C \<cdot> \<sigma>' = D \<cdot> \<sigma> \<cdot> \<sigma>' \<and> is_ground_subst (\<sigma> \<odot> \<sigma>')"
     using assms by auto
   then show "C\<sigma>' \<in> grounding_of_cls D"
     unfolding grounding_of_cls_def using C\<sigma>'(1) by force
 qed
 
 lemma derive_if_remove_subsumed:
   assumes
     "D \<in> clss_of_state St" and
     "subsumes D C"
   shows "sr_ext.derive (grounding_of_state St \<union> grounding_of_cls C) (grounding_of_state St)"
 proof -
   from assms obtain \<sigma> where
     "D \<cdot> \<sigma> = C \<or> D \<cdot> \<sigma> \<subset># C"
     by (auto simp: subsumes_def subset_mset_def)
   then have "D \<cdot> \<sigma> = C \<or> D \<cdot> \<sigma> \<subset># C"
     by (simp add: subset_mset_def)
   then show ?thesis
   proof
     assume "D \<cdot> \<sigma> = C"
     then have "grounding_of_cls C \<subseteq> grounding_of_cls D"
       using subst_cls_eq_grounding_of_cls_subset_eq by simp
     then have "(grounding_of_state St \<union> grounding_of_cls C) = grounding_of_state St"
       using assms unfolding grounding_of_clss_def by auto
     then show ?thesis
       by (auto intro: sr_ext.derive.intros)
   next
     assume a: "D \<cdot> \<sigma> \<subset># C"
     then have "grounding_of_cls C \<subseteq> sr.Rf (grounding_of_state St)"
       using strict_subset_subsumption_grounding_redundant_clss assms by auto
     then show ?thesis
       unfolding grounding_of_clss_def by (force intro: sr_ext.derive.intros)
   qed
 qed
 
 lemma reduction_in_concls_of:
   assumes
     "C\<mu> \<in> grounding_of_cls C" and
     "D + {#L'#} \<in> CC" and
     "- L = L' \<cdot>l \<sigma>" and
     "D \<cdot> \<sigma> \<subseteq># C"
   shows "C\<mu> \<in> concls_of (sr_ext.inferences_from (grounding_of_clss (CC \<union> {C + {#L#}})))"
 proof -
   from assms
   obtain \<mu> where
     \<mu>_p: "C\<mu> = C \<cdot> \<mu> \<and> is_ground_subst \<mu>"
     unfolding grounding_of_cls_def by auto
 
   define \<gamma> where
     "\<gamma> = Infer {#(C + {#L#})\<cdot> \<mu>#} ((D + {#L'#}) \<cdot> \<sigma> \<cdot> \<mu>) (C \<cdot> \<mu>)"
 
   have "(D + {#L'#}) \<cdot> \<sigma> \<cdot> \<mu> \<in> grounding_of_clss (CC \<union> {C + {#L#}})"
     unfolding grounding_of_clss_def grounding_of_cls_def
     by (rule UN_I[of "D + {#L'#}"], use assms(2) in simp,
         metis (mono_tags, lifting) \<mu>_p is_ground_comp_subst mem_Collect_eq subst_cls_comp_subst)
   moreover have "(C + {#L#}) \<cdot> \<mu> \<in> grounding_of_clss (CC \<union> {C + {#L#}})"
     using \<mu>_p unfolding  grounding_of_clss_def grounding_of_cls_def by auto
   moreover have
     "\<forall>I. I \<Turnstile> D \<cdot> \<sigma> \<cdot> \<mu> + {#- (L  \<cdot>l \<mu>)#} \<longrightarrow> I \<Turnstile> C  \<cdot> \<mu> + {#L  \<cdot>l \<mu>#} \<longrightarrow> I \<Turnstile> D \<cdot> \<sigma> \<cdot> \<mu> + C \<cdot> \<mu>"
     by auto
   then have "\<forall>I. I \<Turnstile> (D + {#L'#}) \<cdot> \<sigma> \<cdot> \<mu> \<longrightarrow> I \<Turnstile> (C + {#L#}) \<cdot> \<mu> \<longrightarrow> I \<Turnstile> D \<cdot> \<sigma> \<cdot> \<mu> + C \<cdot> \<mu>"
     using assms
     by (metis add_mset_add_single subst_cls_add_mset subst_cls_union subst_minus)
   then have "\<forall>I. I \<Turnstile> (D + {#L'#}) \<cdot> \<sigma> \<cdot> \<mu> \<longrightarrow> I \<Turnstile> (C + {#L#}) \<cdot> \<mu> \<longrightarrow> I \<Turnstile> C \<cdot> \<mu>"
     using assms by (metis (no_types, lifting) subset_mset.le_iff_add subst_cls_union true_cls_union)
   then have "\<forall>I. I \<Turnstile>m {#(D + {#L'#}) \<cdot> \<sigma> \<cdot> \<mu>#} \<longrightarrow> I \<Turnstile> (C + {#L#}) \<cdot> \<mu> \<longrightarrow> I \<Turnstile> C \<cdot> \<mu>"
     by (meson true_cls_mset_singleton)
   ultimately have "\<gamma> \<in> sr_ext.inferences_from (grounding_of_clss (CC \<union> {C + {#L#}}))"
     unfolding sr_ext.inferences_from_def unfolding ground_sound_\<Gamma>_def infer_from_def \<gamma>_def by auto
   then have "C \<cdot> \<mu> \<in> concls_of (sr_ext.inferences_from (grounding_of_clss (CC \<union> {C + {#L#}})))"
     using image_iff unfolding \<gamma>_def by fastforce
   then show "C\<mu> \<in> concls_of (sr_ext.inferences_from (grounding_of_clss (CC \<union> {C + {#L#}})))"
     using \<mu>_p by auto
 qed
 
 lemma reduction_derivable:
   assumes
     "D + {#L'#} \<in> CC" and
     "- L = L' \<cdot>l \<sigma>" and
     "D \<cdot> \<sigma> \<subseteq># C"
   shows "sr_ext.derive (grounding_of_clss (CC \<union> {C + {#L#}})) (grounding_of_clss (CC \<union> {C}))"
 proof -
   from assms have "grounding_of_clss (CC \<union> {C}) - grounding_of_clss (CC \<union> {C + {#L#}})
     \<subseteq> concls_of (sr_ext.inferences_from (grounding_of_clss (CC \<union> {C + {#L#}})))"
     using reduction_in_concls_of unfolding grounding_of_clss_def by auto
   moreover
   have "grounding_of_cls (C + {#L#}) \<subseteq> sr.Rf (grounding_of_clss (CC \<union> {C}))"
     using strict_subset_subsumption_grounding_redundant_clss[of C "id_subst"]
     by auto
   then have "grounding_of_clss (CC \<union> {C + {#L#}}) - grounding_of_clss (CC \<union> {C})
     \<subseteq> sr.Rf (grounding_of_clss (CC \<union> {C}))"
     unfolding grounding_of_clss_def by auto
   ultimately show
     "sr_ext.derive (grounding_of_clss (CC \<union> {C + {#L#}})) (grounding_of_clss (CC \<union> {C}))"
     using sr_ext.derive.intros[of "grounding_of_clss (CC \<union> {C})"
         "grounding_of_clss (CC \<union> {C + {#L#}})"]
     by auto
 qed
 
 text \<open>
 The following corresponds the part of Lemma 4.10 that states we have a theorem proving process:
 \<close>
 
 lemma RP_ground_derive:
   "St \<leadsto> St' \<Longrightarrow> sr_ext.derive (grounding_of_state St) (grounding_of_state St')"
 proof (induction rule: RP.induct)
   case (tautology_deletion A C N P Q)
   {
     fix C\<sigma>
     assume "C\<sigma> \<in> grounding_of_cls C"
     then obtain \<sigma> where
       "C\<sigma> = C \<cdot> \<sigma>"
       unfolding grounding_of_cls_def by auto
     then have "Neg (A \<cdot>a \<sigma>) \<in># C\<sigma> \<and> Pos (A \<cdot>a \<sigma>) \<in># C\<sigma>"
       using tautology_deletion Neg_Melem_subst_atm_subst_cls Pos_Melem_subst_atm_subst_cls by auto
     then have "C\<sigma> \<in> sr.Rf (grounding_of_state (N, P, Q))"
       using sr.tautology_Rf by auto
   }
   then have "grounding_of_state (N \<union> {C}, P, Q) - grounding_of_state (N, P, Q)
     \<subseteq> sr.Rf (grounding_of_state (N, P, Q))"
     unfolding grounding_of_clss_def by auto
   moreover have "grounding_of_state (N, P, Q) - grounding_of_state (N \<union> {C}, P, Q) = {}"
     unfolding grounding_of_clss_def by auto
   ultimately show ?case
     using sr_ext.derive.intros[of "grounding_of_state (N, P, Q)"
       "grounding_of_state (N \<union> {C}, P, Q)"]
     by auto
 next
   case (forward_subsumption D P Q C N)
   then show ?case
     using derive_if_remove_subsumed[of D "(N, P, Q)" C] unfolding grounding_of_clss_def
     by (simp add: sup_commute sup_left_commute)
 next
   case (backward_subsumption_P D N C P Q)
   then show ?case
     using derive_if_remove_subsumed[of D "(N, P, Q)" C] strictly_subsumes_def
     unfolding grounding_of_clss_def by (simp add: sup_commute sup_left_commute)
 next
   case (backward_subsumption_Q D N C P Q)
   then show ?case
     using derive_if_remove_subsumed[of D "(N, P, Q)" C] strictly_subsumes_def
     unfolding grounding_of_clss_def by (simp add: sup_commute sup_left_commute)
 next
   case (forward_reduction D L' P Q L \<sigma> C N)
   then show ?case
     using reduction_derivable[of _ _ "N \<union> P \<union> Q"] by force
 next
   case (backward_reduction_P D L' N L \<sigma> C P Q)
   then show ?case
     using reduction_derivable[of _ _ "N \<union> P \<union> Q"] by force
 next
   case (backward_reduction_Q D L' N L \<sigma> C P Q)
   then show ?case
     using reduction_derivable[of _ _ "N \<union> P \<union> Q"] by force
 next
   case (clause_processing N C P Q)
   then show ?case
     using sr_ext.derive.intros by auto
 next
   case (inference_computation N Q C P)
   {
     fix E\<mu>
     assume "E\<mu> \<in> grounding_of_clss N"
     then obtain \<mu> E where
       E_\<mu>_p: "E\<mu> = E \<cdot> \<mu> \<and> E \<in> N \<and> is_ground_subst \<mu>"
       unfolding grounding_of_clss_def grounding_of_cls_def by auto
     then have E_concl: "E \<in> concls_of (ord_FO_resolution.inferences_between Q C)"
       using inference_computation by auto
     then obtain \<gamma> where
       \<gamma>_p: "\<gamma> \<in> ord_FO_\<Gamma> S \<and> infer_from (Q \<union> {C}) \<gamma> \<and> C \<in># prems_of \<gamma> \<and> concl_of \<gamma> = E"
       unfolding ord_FO_resolution.inferences_between_def by auto
     then obtain CC CAs D AAs As \<sigma> where
       \<gamma>_p2: "\<gamma> = Infer CC D E \<and> ord_resolve_rename S CAs D AAs As \<sigma> E \<and> mset CAs = CC"
       unfolding ord_FO_\<Gamma>_def by auto
     define \<rho> where
       "\<rho> = hd (renamings_apart (D # CAs))"
     define \<rho>s where
       "\<rho>s = tl (renamings_apart (D # CAs))"
     define \<gamma>_ground where
       "\<gamma>_ground = Infer (mset (CAs \<cdot>\<cdot>cl \<rho>s) \<cdot>cm \<sigma> \<cdot>cm \<mu>) (D \<cdot> \<rho> \<cdot> \<sigma> \<cdot> \<mu>) (E \<cdot> \<mu>)"
     have "\<forall>I. I \<Turnstile>m mset (CAs \<cdot>\<cdot>cl \<rho>s) \<cdot>cm \<sigma> \<cdot>cm \<mu> \<longrightarrow> I \<Turnstile> D \<cdot> \<rho> \<cdot> \<sigma> \<cdot> \<mu> \<longrightarrow> I \<Turnstile> E \<cdot> \<mu>"
       using ord_resolve_rename_ground_inst_sound[of _ _ _ _ _ _ _ _ _ _ \<mu>] \<rho>_def \<rho>s_def E_\<mu>_p \<gamma>_p2
       by auto
     then have "\<gamma>_ground \<in> {Infer cc d e | cc d e. \<forall>I. I \<Turnstile>m cc \<longrightarrow> I \<Turnstile> d \<longrightarrow> I \<Turnstile> e}"
       unfolding \<gamma>_ground_def by auto
     moreover have "set_mset (prems_of \<gamma>_ground) \<subseteq> grounding_of_state ({}, P \<union> {C}, Q)"
     proof -
       have "D = C \<or> D \<in> Q"
         unfolding \<gamma>_ground_def using E_\<mu>_p \<gamma>_p2 \<gamma>_p unfolding infer_from_def
         unfolding grounding_of_clss_def grounding_of_cls_def by simp
       then have "D \<cdot> \<rho> \<cdot> \<sigma> \<cdot> \<mu> \<in> grounding_of_cls C \<or> (\<exists>x \<in> Q. D \<cdot> \<rho> \<cdot> \<sigma> \<cdot> \<mu> \<in> grounding_of_cls x)"
         using E_\<mu>_p
         unfolding grounding_of_cls_def
         by (metis (mono_tags, lifting) is_ground_comp_subst mem_Collect_eq subst_cls_comp_subst)
       then have "(D \<cdot> \<rho> \<cdot> \<sigma> \<cdot> \<mu> \<in> grounding_of_cls C \<or>
         (\<exists>x \<in> P. D \<cdot> \<rho> \<cdot> \<sigma> \<cdot> \<mu> \<in> grounding_of_cls x) \<or>
         (\<exists>x \<in> Q. D \<cdot> \<rho> \<cdot> \<sigma> \<cdot> \<mu> \<in> grounding_of_cls x))"
         by metis
       moreover have "\<forall>i < length (CAs \<cdot>\<cdot>cl \<rho>s \<cdot>cl \<sigma> \<cdot>cl \<mu>). ((CAs \<cdot>\<cdot>cl \<rho>s \<cdot>cl \<sigma> \<cdot>cl \<mu>) ! i) \<in>
         {C \<cdot> \<sigma> |\<sigma>. is_ground_subst \<sigma>} \<union>
         ((\<Union>C \<in> P. {C \<cdot> \<sigma> | \<sigma>. is_ground_subst \<sigma>}) \<union> (\<Union>C\<in>Q. {C \<cdot> \<sigma> | \<sigma>. is_ground_subst \<sigma>}))"
       proof (rule, rule)
         fix i
         assume "i < length (CAs \<cdot>\<cdot>cl \<rho>s \<cdot>cl \<sigma> \<cdot>cl \<mu>)"
         then have a: "i < length CAs \<and> i < length \<rho>s"
           by simp
         moreover from a have "CAs ! i \<in> {C} \<union> Q"
           using \<gamma>_p2 \<gamma>_p unfolding infer_from_def
           by (metis (no_types, lifting) Un_subset_iff inference.sel(1) set_mset_union
               sup_commute nth_mem_mset subsetCE)
         ultimately have "(CAs \<cdot>\<cdot>cl \<rho>s \<cdot>cl \<sigma> \<cdot>cl \<mu>) ! i \<in>
           {C \<cdot> \<sigma> |\<sigma>. is_ground_subst \<sigma>} \<or>
           ((CAs \<cdot>\<cdot>cl \<rho>s \<cdot>cl \<sigma> \<cdot>cl \<mu>) ! i \<in> (\<Union>C\<in>P. {C \<cdot> \<sigma> |\<sigma>. is_ground_subst \<sigma>}) \<or>
           (CAs \<cdot>\<cdot>cl \<rho>s \<cdot>cl \<sigma> \<cdot>cl \<mu>) ! i \<in> (\<Union>C \<in> Q. {C \<cdot> \<sigma> | \<sigma>. is_ground_subst \<sigma>}))"
           using E_\<mu>_p \<gamma>_p2 \<gamma>_p
           unfolding \<gamma>_ground_def infer_from_def grounding_of_clss_def grounding_of_cls_def
           apply -
           apply (cases "CAs ! i = C")
           subgoal
             apply (rule disjI1)
             apply (rule Set.CollectI)
             apply (rule_tac x = "(\<rho>s ! i) \<odot> \<sigma> \<odot> \<mu>" in exI)
             using \<rho>s_def using renamings_apart_length by (auto; fail)
           subgoal
             apply (rule disjI2)
             apply (rule disjI2)
             apply (rule_tac a = "CAs ! i" in UN_I)
             subgoal by blast
             subgoal
               apply (rule Set.CollectI)
               apply (rule_tac x = "(\<rho>s ! i) \<odot> \<sigma> \<odot> \<mu>" in exI)
               using \<rho>s_def using renamings_apart_length by (auto; fail)
             done
           done
         then show "(CAs \<cdot>\<cdot>cl \<rho>s \<cdot>cl \<sigma> \<cdot>cl \<mu>) ! i \<in> {C \<cdot> \<sigma> |\<sigma>. is_ground_subst \<sigma>} \<union>
           ((\<Union>C \<in> P. {C \<cdot> \<sigma> |\<sigma>. is_ground_subst \<sigma>}) \<union> (\<Union>C \<in> Q. {C \<cdot> \<sigma> |\<sigma>. is_ground_subst \<sigma>}))"
           by blast
       qed
       then have "\<forall>x \<in># mset (CAs \<cdot>\<cdot>cl \<rho>s \<cdot>cl \<sigma> \<cdot>cl \<mu>). x \<in> {C \<cdot> \<sigma> |\<sigma>. is_ground_subst \<sigma>} \<union>
         ((\<Union>C \<in> P. {C \<cdot> \<sigma> |\<sigma>. is_ground_subst \<sigma>}) \<union> (\<Union>C \<in> Q. {C \<cdot> \<sigma> |\<sigma>. is_ground_subst \<sigma>}))"
         by (metis (lifting) in_set_conv_nth set_mset_mset)
       then have "set_mset (mset (CAs \<cdot>\<cdot>cl \<rho>s) \<cdot>cm \<sigma> \<cdot>cm \<mu>) \<subseteq>
         grounding_of_cls C \<union> grounding_of_clss P \<union> grounding_of_clss Q"
         unfolding grounding_of_cls_def grounding_of_clss_def
         using mset_subst_cls_list_subst_cls_mset by auto
       ultimately show ?thesis
         unfolding \<gamma>_ground_def grounding_of_clss_def by auto
     qed
     ultimately have
       "E \<cdot> \<mu> \<in> concls_of (sr_ext.inferences_from (grounding_of_state ({}, P \<union> {C}, Q)))"
       unfolding sr_ext.inferences_from_def inference_system.inferences_from_def ground_sound_\<Gamma>_def
         infer_from_def
       using \<gamma>_ground_def by (metis (no_types, lifting) imageI inference.sel(3) mem_Collect_eq)
     then have "E\<mu> \<in> concls_of (sr_ext.inferences_from (grounding_of_state ({}, P \<union> {C}, Q)))"
       using E_\<mu>_p by auto
   }
   then have "grounding_of_state (N, P, Q \<union> {C}) - grounding_of_state ({}, P \<union> {C}, Q)
     \<subseteq> concls_of (sr_ext.inferences_from (grounding_of_state ({}, P \<union> {C}, Q)))"
     unfolding grounding_of_clss_def by auto
   moreover have "grounding_of_state ({}, P \<union> {C}, Q) - grounding_of_state (N, P, Q \<union> {C}) = {}"
     unfolding grounding_of_clss_def by auto
   ultimately show ?case
     using sr_ext.derive.intros[of "(grounding_of_state (N, P, Q \<union> {C}))"
         "(grounding_of_state ({}, P \<union> {C}, Q))"] by auto
 qed
 
 text \<open>
 A useful consequence:
 \<close>
 
 theorem RP_model:
   "St \<leadsto> St' \<Longrightarrow> I \<Turnstile>s grounding_of_state St' \<longleftrightarrow> I \<Turnstile>s grounding_of_state St"
 proof (drule RP_ground_derive, erule sr_ext.derive.cases, hypsubst)
   let
     ?gSt = "grounding_of_state St" and
     ?gSt' = "grounding_of_state St'"
 
   assume
     deduct: "?gSt' - ?gSt \<subseteq> concls_of (sr_ext.inferences_from ?gSt)" (is "_ \<subseteq> ?concls") and
     delete: "?gSt - ?gSt' \<subseteq> sr.Rf ?gSt'"
 
   show "I \<Turnstile>s ?gSt' \<longleftrightarrow> I \<Turnstile>s ?gSt"
   proof
     assume bef: "I \<Turnstile>s ?gSt"
     then have "I \<Turnstile>s ?concls"
       unfolding ground_sound_\<Gamma>_def inference_system.inferences_from_def true_clss_def
         true_cls_mset_def
       by (auto simp add: image_def infer_from_def dest!: spec[of _ I])
     then have diff: "I \<Turnstile>s ?gSt' - ?gSt"
       using deduct by (blast intro: true_clss_mono)
     then show "I \<Turnstile>s ?gSt'"
       using bef unfolding true_clss_def by blast
   next
     assume aft: "I \<Turnstile>s ?gSt'"
     have "I \<Turnstile>s ?gSt' \<union> sr.Rf ?gSt'"
       by (rule sr.Rf_model) (smt Diff_eq_empty_iff Diff_subset Un_Diff aft
           standard_redundancy_criterion.Rf_mono sup_bot.right_neutral sup_ge1 true_clss_mono)
     then have "I \<Turnstile>s sr.Rf ?gSt'"
       using true_clss_union by blast
     then have diff: "I \<Turnstile>s ?gSt - ?gSt'"
       using delete by (blast intro: true_clss_mono)
     then show "I \<Turnstile>s ?gSt"
       using aft unfolding true_clss_def by blast
   qed
 qed
 
 text \<open>
 Another formulation of the part of Lemma 4.10 that states we have a theorem proving process:
 \<close>
 
-lemma ground_derive_chain: "chain sr_ext.derive (lmap grounding_of_state Sts)"
-  using deriv RP_ground_derive by (simp add: chain_lmap[of "(\<leadsto>)"])
+lemma ground_derive_chain: "chain (\<leadsto>) Sts \<Longrightarrow> chain sr_ext.derive (lmap grounding_of_state Sts)"
+  using RP_ground_derive by (simp add: chain_lmap[of "(\<leadsto>)"])
 
 text \<open>
 The following is used prove to Lemma 4.11:
 \<close>
 
 lemma in_Sup_llist_in_nth: "C \<in> Sup_llist Gs \<Longrightarrow> \<exists>j. enat j < llength Gs \<and> C \<in> lnth Gs j"
   unfolding Sup_llist_def by auto
     \<comment> \<open>Note: Gs is called Ns in the chapter\<close>
 
 lemma Sup_llist_grounding_of_state_ground:
   assumes "C \<in> Sup_llist (lmap grounding_of_state Sts)"
   shows "is_ground_cls C"
 proof -
   have "\<exists>j. enat j < llength (lmap grounding_of_state Sts)
     \<and> C \<in> lnth (lmap grounding_of_state Sts) j"
     using assms in_Sup_llist_in_nth by fast
   then obtain j where
     "enat j < llength (lmap grounding_of_state Sts)"
     "C \<in> lnth (lmap grounding_of_state Sts) j"
     by blast
   then show ?thesis
     unfolding grounding_of_clss_def grounding_of_cls_def by auto
 qed
 
 lemma Liminf_grounding_of_state_ground:
   "C \<in> Liminf_llist (lmap grounding_of_state Sts) \<Longrightarrow> is_ground_cls C"
   using Liminf_llist_subset_Sup_llist[of "lmap grounding_of_state Sts"]
     Sup_llist_grounding_of_state_ground
   by blast
 
 lemma in_Sup_llist_in_Sup_state:
   assumes "C \<in> Sup_llist (lmap grounding_of_state Sts)"
   shows "\<exists>D \<sigma>. D \<in> clss_of_state (Sup_state Sts) \<and> D \<cdot> \<sigma> = C \<and> is_ground_subst \<sigma>"
 proof -
   from assms obtain i where
     i_p: "enat i < llength Sts \<and> C \<in> lnth (lmap grounding_of_state Sts) i"
     using in_Sup_llist_in_nth by fastforce
   then obtain D \<sigma> where
     "D \<in> clss_of_state (lnth Sts i) \<and> D \<cdot> \<sigma> = C \<and> is_ground_subst \<sigma>"
     using assms unfolding grounding_of_clss_def grounding_of_cls_def by fastforce
   then have "D \<in> clss_of_state (Sup_state Sts) \<and> D \<cdot> \<sigma> = C \<and> is_ground_subst \<sigma>"
     using i_p unfolding Sup_state_def
     by (metis (no_types, lifting) UnCI UnE contra_subsetD N_of_state.simps P_of_state.simps
         Q_of_state.simps llength_lmap lnth_lmap lnth_subset_Sup_llist)
   then show ?thesis
     by auto
 qed
 
 lemma
   N_of_state_Liminf: "N_of_state (Liminf_state Sts) = Liminf_llist (lmap N_of_state Sts)" and
   P_of_state_Liminf: "P_of_state (Liminf_state Sts) = Liminf_llist (lmap P_of_state Sts)"
   unfolding Liminf_state_def by auto
 
 lemma eventually_removed_from_N:
   assumes
     d_in: "D \<in> N_of_state (lnth Sts i)" and
     fair: "fair_state_seq Sts" and
     i_Sts: "enat i < llength Sts"
   shows "\<exists>l. D \<in> N_of_state (lnth Sts l) \<and> D \<notin> N_of_state (lnth Sts (Suc l)) \<and> i \<le> l
     \<and> enat (Suc l) < llength Sts"
 proof (rule ccontr)
   assume a: "\<not> ?thesis"
   have "i \<le> l \<Longrightarrow> enat l < llength Sts \<Longrightarrow> D \<in> N_of_state (lnth Sts l)" for l
     using d_in by (induction l, blast, metis a Suc_ile_eq le_SucE less_imp_le)
   then have "D \<in> Liminf_llist (lmap N_of_state Sts)"
     unfolding Liminf_llist_def using i_Sts by auto
   then show False
     using fair unfolding fair_state_seq_def by (simp add: N_of_state_Liminf)
 qed
 
 lemma eventually_removed_from_P:
   assumes
     d_in: "D \<in> P_of_state (lnth Sts i)" and
     fair: "fair_state_seq Sts" and
     i_Sts: "enat i < llength Sts"
   shows "\<exists>l. D \<in> P_of_state (lnth Sts l) \<and> D \<notin> P_of_state (lnth Sts (Suc l)) \<and> i \<le> l
     \<and> enat (Suc l) < llength Sts"
 proof (rule ccontr)
   assume a: "\<not> ?thesis"
   have "i \<le> l \<Longrightarrow> enat l < llength Sts \<Longrightarrow> D \<in> P_of_state (lnth Sts l)" for l
     using d_in by (induction l, blast, metis a Suc_ile_eq le_SucE less_imp_le)
   then have "D \<in> Liminf_llist (lmap P_of_state Sts)"
     unfolding Liminf_llist_def using i_Sts by auto
   then show False
     using fair unfolding fair_state_seq_def by (simp add: P_of_state_Liminf)
 qed
 
 lemma instance_if_subsumed_and_in_limit:
   assumes
+    deriv: "chain (\<leadsto>) Sts" and
     ns: "Gs = lmap grounding_of_state Sts" and
     c: "C \<in> Liminf_llist Gs - sr.Rf (Liminf_llist Gs)" and
     d: "D \<in> clss_of_state (lnth Sts i)" "enat i < llength Sts" "subsumes D C"
   shows "\<exists>\<sigma>. D \<cdot> \<sigma> = C \<and> is_ground_subst \<sigma>"
 proof -
   let ?Ps = "\<lambda>i. P_of_state (lnth Sts i)"
   let ?Qs = "\<lambda>i. Q_of_state (lnth Sts i)"
 
   have ground_C: "is_ground_cls C"
     using c using Liminf_grounding_of_state_ground ns by auto
 
   have derivns: "chain sr_ext.derive Gs"
     using ground_derive_chain deriv ns by auto
 
   have "\<exists>\<sigma>. D \<cdot> \<sigma> = C"
   proof (rule ccontr)
     assume "\<nexists>\<sigma>. D \<cdot> \<sigma> = C"
     moreover from d(3) obtain \<tau>_proto where
       "D \<cdot> \<tau>_proto \<subseteq># C" unfolding subsumes_def
       by blast
     then obtain \<tau> where
       \<tau>_p: "D \<cdot> \<tau> \<subseteq># C \<and> is_ground_subst \<tau>"
       using ground_C by (metis is_ground_cls_mono make_ground_subst subset_mset.order_refl)
     ultimately have subsub: "D \<cdot> \<tau> \<subset># C"
       using subset_mset.le_imp_less_or_eq by auto
     moreover have "is_ground_subst \<tau>"
       using \<tau>_p by auto
     moreover have "D \<in> clss_of_state (lnth Sts i)"
       using d by auto
     ultimately have "C \<in> sr.Rf (grounding_of_state (lnth Sts i))"
       using strict_subset_subsumption_redundant_clss by auto
     then have "C \<in> sr.Rf (Sup_llist Gs)"
       using d ns by (smt contra_subsetD llength_lmap lnth_lmap lnth_subset_Sup_llist sr.Rf_mono)
     then have "C \<in> sr.Rf (Liminf_llist Gs)"
       unfolding ns using local.sr_ext.Rf_limit_Sup derivns ns by auto
     then show False
       using c by auto
   qed
   then obtain \<sigma> where
     "D \<cdot> \<sigma> = C \<and> is_ground_subst \<sigma>"
     using ground_C by (metis make_ground_subst)
   then show ?thesis
     by auto
 qed
 
 lemma from_Q_to_Q_inf:
   assumes
+    deriv: "chain (\<leadsto>) Sts" and
     fair: "fair_state_seq Sts" and
     ns: "Gs = lmap grounding_of_state Sts" and
     c: "C \<in> Liminf_llist Gs - sr.Rf (Liminf_llist Gs)" and
     d: "D \<in> Q_of_state (lnth Sts i)" "enat i < llength Sts" "subsumes D C" and
     d_least: "\<forall>E \<in> {E. E \<in> (clss_of_state (Sup_state Sts)) \<and> subsumes E C}.
       \<not> strictly_subsumes E D"
   shows "D \<in> Q_of_state (Liminf_state Sts)"
 proof -
   let ?Ps = "\<lambda>i. P_of_state (lnth Sts i)"
   let ?Qs = "\<lambda>i. Q_of_state (lnth Sts i)"
 
   have ground_C: "is_ground_cls C"
     using c using Liminf_grounding_of_state_ground ns by auto
 
   have derivns: "chain sr_ext.derive Gs"
     using ground_derive_chain deriv ns by auto
 
   have "\<exists>\<sigma>. D \<cdot> \<sigma> = C \<and> is_ground_subst \<sigma>"
-    using instance_if_subsumed_and_in_limit c d unfolding ns by blast
+    using instance_if_subsumed_and_in_limit[OF deriv] c d unfolding ns by blast
   then obtain \<sigma> where
     \<sigma>: "D \<cdot> \<sigma> = C" "is_ground_subst \<sigma>"
     by auto
 
   have in_Sts_in_Sts_Suc:
     "\<forall>l \<ge> i. enat (Suc l) < llength Sts \<longrightarrow> D \<in> Q_of_state (lnth Sts l) \<longrightarrow>
        D \<in> Q_of_state (lnth Sts (Suc l))"
   proof (rule, rule, rule, rule)
     fix l
     assume
       len: "i \<le> l" and
       llen: "enat (Suc l) < llength Sts" and
       d_in_q: "D \<in> Q_of_state (lnth Sts l)"
 
     have "lnth Sts l \<leadsto> lnth Sts (Suc l)"
       using llen deriv chain_lnth_rel by blast
     then show "D \<in> Q_of_state (lnth Sts (Suc l))"
     proof (cases rule: RP.cases)
       case (backward_subsumption_Q D' N D_removed P Q)
       moreover
       {
         assume "D_removed = D"
         then obtain D_subsumes where
           D_subsumes_p: "D_subsumes \<in> N \<and> strictly_subsumes D_subsumes D"
           using backward_subsumption_Q by auto
         moreover from D_subsumes_p have "subsumes D_subsumes C"
           using d subsumes_trans unfolding strictly_subsumes_def by blast
         moreover from backward_subsumption_Q have "D_subsumes \<in> clss_of_state (Sup_state Sts)"
           using D_subsumes_p llen
           by (metis (no_types) UnI1 N_of_state.simps llength_lmap lnth_lmap lnth_subset_Sup_llist
               rev_subsetD Sup_state_def)
         ultimately have False
           using d_least unfolding subsumes_def by auto
       }
       ultimately show ?thesis
         using d_in_q by auto
     next
       case (backward_reduction_Q E L' N L \<sigma> D' P Q)
       {
         assume "D' + {#L#} = D"
         then have D'_p: "strictly_subsumes D' D \<and> D' \<in> ?Ps (Suc l)"
           using subset_strictly_subsumes[of D' D] backward_reduction_Q by auto
         then have subc: "subsumes D' C"
           using d(3) subsumes_trans unfolding strictly_subsumes_def by auto
         from D'_p have "D' \<in> clss_of_state (Sup_state Sts)"
           using llen by (metis (no_types) UnI1 P_of_state.simps llength_lmap lnth_lmap
               lnth_subset_Sup_llist subsetCE sup_ge2 Sup_state_def)
         then have False
           using d_least D'_p subc by auto
       }
       then show ?thesis
         using backward_reduction_Q d_in_q by auto
     qed (use d_in_q in auto)
   qed
   have D_in_Sts: "D \<in> Q_of_state (lnth Sts l)" and D_in_Sts_Suc: "D \<in> Q_of_state (lnth Sts (Suc l))"
     if l_i: "l \<ge> i" and enat: "enat (Suc l) < llength Sts" for l
   proof -
     show "D \<in> Q_of_state (lnth Sts l)"
       using l_i enat
       apply (induction "l - i" arbitrary: l)
       subgoal using d by auto
       subgoal using d(1) in_Sts_in_Sts_Suc
         by (metis (no_types, lifting) Suc_ile_eq add_Suc_right add_diff_cancel_left' le_SucE
             le_Suc_ex less_imp_le)
       done
     then show "D \<in> Q_of_state (lnth Sts (Suc l))"
       using l_i enat in_Sts_in_Sts_Suc by blast
   qed
   have "i \<le> x \<Longrightarrow> enat x < llength Sts \<Longrightarrow> D \<in> Q_of_state (lnth Sts x)" for x
     apply (cases x)
     subgoal using d(1) by (auto intro!: exI[of _ i] simp: less_Suc_eq)
     subgoal for x'
       using d(1) D_in_Sts_Suc[of x'] by (cases \<open>i \<le> x'\<close>) (auto simp: not_less_eq_eq)
     done
   then have "D \<in> Liminf_llist (lmap Q_of_state Sts)"
     unfolding Liminf_llist_def by (auto intro!: exI[of _ i] simp: d)
   then show ?thesis
     unfolding Liminf_state_def by auto
 qed
 
 lemma from_P_to_Q:
   assumes
+    deriv: "chain (\<leadsto>) Sts" and
     fair: "fair_state_seq Sts" and
     ns: "Gs = lmap grounding_of_state Sts" and
     c: "C \<in> Liminf_llist Gs - sr.Rf (Liminf_llist Gs)" and
     d: "D \<in> P_of_state (lnth Sts i)" "enat i < llength Sts" "subsumes D C" and
     d_least: "\<forall>E \<in> {E. E \<in> (clss_of_state (Sup_state Sts)) \<and> subsumes E C}.
       \<not> strictly_subsumes E D"
   shows "\<exists>l. D \<in> Q_of_state (lnth Sts l) \<and> enat l < llength Sts"
 proof -
   let ?Ns = "\<lambda>i. N_of_state (lnth Sts i)"
   let ?Ps = "\<lambda>i. P_of_state (lnth Sts i)"
   let ?Qs = "\<lambda>i. Q_of_state (lnth Sts i)"
 
   have ground_C: "is_ground_cls C"
     using c using Liminf_grounding_of_state_ground ns by auto
 
   have derivns: "chain sr_ext.derive Gs"
     using ground_derive_chain deriv ns by auto
 
   have "\<exists>\<sigma>. D \<cdot> \<sigma> = C \<and> is_ground_subst \<sigma>"
-    using instance_if_subsumed_and_in_limit ns c d by blast
+    using instance_if_subsumed_and_in_limit[OF deriv] ns c d by blast
   then obtain \<sigma> where
     \<sigma>: "D \<cdot> \<sigma> = C" "is_ground_subst \<sigma>"
     by auto
 
   obtain l where
     l_p: "D \<in> P_of_state (lnth Sts l) \<and> D \<notin> P_of_state (lnth Sts (Suc l)) \<and> i \<le> l
       \<and> enat (Suc l) < llength Sts"
     using fair using eventually_removed_from_P d unfolding ns by auto
   then have l_Gs: "enat (Suc l) < llength Gs"
     using ns by auto
   from l_p have "lnth Sts l \<leadsto> lnth Sts (Suc l)"
     using deriv using chain_lnth_rel by auto
   then show ?thesis
   proof (cases rule: RP.cases)
     case (backward_subsumption_P D' N D_twin P Q)
     note lrhs = this(1,2) and D'_p = this(3,4)
     then have twins: "D_twin = D" "?Ns (Suc l) = N" "?Ns l = N"  "?Ps (Suc l) = P"
       "?Ps l = P \<union> {D_twin}" "?Qs (Suc l) = Q" "?Qs l = Q"
       using l_p by auto
     note D'_p = D'_p[unfolded twins(1)]
     then have subc: "subsumes D' C"
       unfolding strictly_subsumes_def subsumes_def using \<sigma>
       by (metis subst_cls_comp_subst subst_cls_mono_mset)
     from D'_p have "D' \<in> clss_of_state (Sup_state Sts)"
       unfolding twins(2)[symmetric] using l_p
       by (metis (no_types) UnI1 N_of_state.simps llength_lmap lnth_lmap lnth_subset_Sup_llist
           subsetCE Sup_state_def)
     then have False
       using d_least D'_p subc by auto
     then show ?thesis
       by auto
   next
     case (backward_reduction_P E L' N L \<sigma> D' P Q)
     then have twins: "D' + {#L#} = D" "?Ns (Suc l) = N" "?Ns l = N"  "?Ps (Suc l) = P \<union> {D'}"
       "?Ps l = P \<union> {D' + {#L#}}" "?Qs (Suc l) = Q" "?Qs l = Q"
       using l_p by auto
     then have D'_p: "strictly_subsumes D' D \<and> D' \<in> ?Ps (Suc l)"
       using subset_strictly_subsumes[of D' D] by auto
     then have subc: "subsumes D' C"
       using d(3) subsumes_trans unfolding strictly_subsumes_def by auto
     from D'_p have "D' \<in> clss_of_state (Sup_state Sts)"
       using l_p by (metis (no_types) UnI1 P_of_state.simps llength_lmap lnth_lmap
           lnth_subset_Sup_llist subsetCE sup_ge2 Sup_state_def)
     then have False
       using d_least D'_p subc by auto
     then show ?thesis
       by auto
   next
     case (inference_computation N Q D_twin P)
     then have twins: "D_twin = D" "?Ps (Suc l) = P" "?Ps l = P \<union> {D_twin}"
       "?Qs (Suc l) = Q \<union> {D_twin}" "?Qs l = Q"
       using l_p by auto
     then show ?thesis
       using d \<sigma> l_p by auto
   qed (use l_p in auto)
 qed
 
 lemma variants_sym: "variants D D' \<longleftrightarrow> variants D' D"
   unfolding variants_def by auto
 
 lemma variants_imp_exists_subtitution: "variants D D' \<Longrightarrow> \<exists>\<sigma>. D \<cdot> \<sigma> = D'"
   unfolding variants_iff_subsumes subsumes_def
   by (meson strictly_subsumes_def subset_mset_def strict_subset_subst_strictly_subsumes subsumes_def)
 
 lemma properly_subsume_variants:
   assumes "strictly_subsumes E D" and "variants D D'"
   shows "strictly_subsumes E D'"
 proof -
   from assms obtain \<sigma> \<sigma>' where
     \<sigma>_\<sigma>'_p: "D \<cdot> \<sigma> = D' \<and> D' \<cdot> \<sigma>' = D"
     using variants_imp_exists_subtitution variants_sym by metis
 
   from assms obtain \<sigma>'' where
     "E \<cdot> \<sigma>'' \<subseteq># D"
     unfolding strictly_subsumes_def subsumes_def by auto
   then have "E \<cdot> \<sigma>'' \<cdot> \<sigma> \<subseteq># D \<cdot> \<sigma>"
     using subst_cls_mono_mset by blast
   then have "E \<cdot> (\<sigma>'' \<odot> \<sigma>)  \<subseteq># D'"
     using \<sigma>_\<sigma>'_p by auto
   moreover from assms have n: "(\<nexists>\<sigma>. D \<cdot> \<sigma> \<subseteq># E)"
     unfolding strictly_subsumes_def subsumes_def by auto
   have "\<nexists>\<sigma>. D' \<cdot> \<sigma> \<subseteq># E"
   proof
     assume "\<exists>\<sigma>'''. D' \<cdot> \<sigma>''' \<subseteq># E"
     then obtain \<sigma>''' where
       "D' \<cdot> \<sigma>''' \<subseteq># E"
       by auto
     then have "D \<cdot> (\<sigma> \<odot> \<sigma>''') \<subseteq># E"
       using \<sigma>_\<sigma>'_p by auto
     then show False
       using n by metis
   qed
   ultimately show ?thesis
     unfolding strictly_subsumes_def subsumes_def by metis
 qed
 
 lemma neg_properly_subsume_variants:
   assumes "\<not> strictly_subsumes E D" and "variants D D'"
   shows "\<not> strictly_subsumes E D'"
   using assms properly_subsume_variants variants_sym by auto
 
 lemma from_N_to_P_or_Q:
   assumes
+    deriv: "chain (\<leadsto>) Sts" and
     fair: "fair_state_seq Sts" and
     ns: "Gs = lmap grounding_of_state Sts" and
     c: "C \<in> Liminf_llist Gs - sr.Rf (Liminf_llist Gs)" and
     d: "D \<in> N_of_state (lnth Sts i)" "enat i < llength Sts" "subsumes D C" and
     d_least: "\<forall>E \<in> {E. E \<in> (clss_of_state (Sup_state Sts)) \<and> subsumes E C}. \<not> strictly_subsumes E D"
   shows "\<exists>l D' \<sigma>'. D' \<in> P_of_state (lnth Sts l) \<union> Q_of_state (lnth Sts l) \<and>
     enat l < llength Sts \<and>
     (\<forall>E \<in> {E. E \<in> (clss_of_state (Sup_state Sts)) \<and> subsumes E C}. \<not> strictly_subsumes E D') \<and>
     D' \<cdot> \<sigma>' = C \<and> is_ground_subst \<sigma>' \<and> subsumes D' C"
 proof -
   let ?Ns = "\<lambda>i. N_of_state (lnth Sts i)"
   let ?Ps = "\<lambda>i. P_of_state (lnth Sts i)"
   let ?Qs = "\<lambda>i. Q_of_state (lnth Sts i)"
 
   have ground_C: "is_ground_cls C"
     using c using Liminf_grounding_of_state_ground ns by auto
 
   have derivns: "chain sr_ext.derive Gs"
     using ground_derive_chain deriv ns by auto
 
   have "\<exists>\<sigma>. D \<cdot> \<sigma> = C \<and> is_ground_subst \<sigma>"
-    using instance_if_subsumed_and_in_limit ns c d by blast
+    using instance_if_subsumed_and_in_limit[OF deriv] ns c d by blast
   then obtain \<sigma> where
     \<sigma>: "D \<cdot> \<sigma> = C" "is_ground_subst \<sigma>"
     by auto
 
   from c have no_taut: "\<not> (\<exists>A. Pos A \<in># C \<and> Neg A \<in># C)"
     using sr.tautology_Rf by auto
 
   have "\<exists>l. D \<in> N_of_state (lnth Sts l)
     \<and> D \<notin> N_of_state (lnth Sts (Suc l)) \<and> i \<le> l \<and> enat (Suc l) < llength Sts"
     using fair using eventually_removed_from_N d unfolding ns by auto
   then obtain l where
     l_p: "D \<in> N_of_state (lnth Sts l) \<and> D \<notin> N_of_state (lnth Sts (Suc l)) \<and> i \<le> l
       \<and> enat (Suc l) < llength Sts"
     by auto
   then have l_Gs: "enat (Suc l) < llength Gs"
     using ns by auto
   from l_p have "lnth Sts l \<leadsto> lnth Sts (Suc l)"
     using deriv using chain_lnth_rel by auto
   then show ?thesis
   proof (cases rule: RP.cases)
     case (tautology_deletion A D_twin N P Q)
     then have "D_twin = D"
       using l_p by auto
     then have "Pos (A \<cdot>a \<sigma>) \<in># C \<and> Neg (A \<cdot>a \<sigma>) \<in># C"
       using tautology_deletion(3,4) \<sigma>
       by (metis Melem_subst_cls eql_neg_lit_eql_atm eql_pos_lit_eql_atm)
     then have False
       using no_taut by metis
     then show ?thesis
       by blast
   next
     case (forward_subsumption D' P Q D_twin N)
     note lrhs = this(1,2) and D'_p = this(3,4)
     then have twins: "D_twin = D" "?Ns (Suc l) = N" "?Ns l = N \<union> {D_twin}"  "?Ps (Suc l) = P "
       "?Ps l = P" "?Qs (Suc l) = Q" "?Qs l = Q"
       using l_p by auto
     note D'_p = D'_p[unfolded twins(1)]
     from D'_p(2) have subs: "subsumes D' C"
       using d(3) by (blast intro: subsumes_trans)
     moreover have "D' \<in> clss_of_state (Sup_state Sts)"
       using twins D'_p l_p unfolding Sup_state_def
       by simp (metis (no_types) contra_subsetD llength_lmap lnth_lmap lnth_subset_Sup_llist)
     ultimately have "\<not> strictly_subsumes D' D"
       using d_least by auto
     then have "subsumes D D'"
       unfolding strictly_subsumes_def using D'_p by auto
     then have v: "variants D D'"
       using D'_p unfolding variants_iff_subsumes by auto
     then have mini: "\<forall>E \<in> {E \<in> clss_of_state (Sup_state Sts). subsumes E C}.
       \<not> strictly_subsumes E D'"
       using d_least D'_p neg_properly_subsume_variants[of _ D D'] by auto
 
     from v have "\<exists>\<sigma>'. D' \<cdot> \<sigma>' = C"
       using \<sigma> variants_imp_exists_subtitution variants_sym by (metis subst_cls_comp_subst)
     then have "\<exists>\<sigma>'. D' \<cdot> \<sigma>' = C \<and> is_ground_subst \<sigma>'"
       using ground_C by (meson make_ground_subst refl)
     then obtain \<sigma>' where
       \<sigma>'_p: "D' \<cdot> \<sigma>' = C \<and> is_ground_subst \<sigma>'"
       by metis
 
     show ?thesis
       using D'_p twins l_p subs mini \<sigma>'_p by auto
   next
     case (forward_reduction E L' P Q L \<sigma> D' N)
     then have twins: "D' + {#L#} = D" "?Ns (Suc l) = N \<union> {D'}" "?Ns l = N \<union> {D' + {#L#}}"
       "?Ps (Suc l) = P " "?Ps l = P" "?Qs (Suc l) = Q" "?Qs l = Q"
       using l_p by auto
     then have D'_p: "strictly_subsumes D' D \<and> D' \<in> ?Ns (Suc l)"
       using subset_strictly_subsumes[of D' D] by auto
     then have subc: "subsumes D' C"
       using d(3) subsumes_trans unfolding strictly_subsumes_def by blast
     from D'_p have "D' \<in> clss_of_state (Sup_state Sts)"
       using l_p by (metis (no_types) UnI1 N_of_state.simps llength_lmap lnth_lmap
           lnth_subset_Sup_llist subsetCE Sup_state_def)
     then have False
       using d_least D'_p subc by auto
     then show ?thesis
       by auto
   next
     case (clause_processing N D_twin P Q)
     then have twins:  "D_twin = D" "?Ns (Suc l) = N" "?Ns l = N \<union> {D}"  "?Ps (Suc l) = P \<union> {D}"
       "?Ps l = P" "?Qs (Suc l) = Q" "?Qs l = Q"
       using l_p by auto
     then show ?thesis
       using d \<sigma> l_p d_least by blast
   qed (use l_p in auto)
 qed
 
 lemma eventually_in_Qinf:
   assumes
+    deriv: "chain (\<leadsto>) Sts" and
     D_p: "D \<in> clss_of_state (Sup_state Sts)"
       "subsumes D C" "\<forall>E \<in> {E. E \<in> (clss_of_state (Sup_state Sts)) \<and> subsumes E C}.
        \<not> strictly_subsumes E D" and
     fair: "fair_state_seq Sts" and
     ns: "Gs = lmap grounding_of_state Sts" and
     c: "C \<in> Liminf_llist Gs - sr.Rf (Liminf_llist Gs)" and
     ground_C: "is_ground_cls C"
   shows "\<exists>D' \<sigma>'. D' \<in> Q_of_state (Liminf_state Sts) \<and> D' \<cdot> \<sigma>' = C \<and> is_ground_subst \<sigma>'"
 proof -
   let ?Ns = "\<lambda>i. N_of_state (lnth Sts i)"
   let ?Ps = "\<lambda>i. P_of_state (lnth Sts i)"
   let ?Qs = "\<lambda>i. Q_of_state (lnth Sts i)"
 
   from D_p obtain i where
     i_p: "i < llength Sts" "D \<in> ?Ns i \<or> D \<in> ?Ps i \<or> D \<in> ?Qs i"
     unfolding Sup_state_def
     by simp_all (metis (no_types) in_Sup_llist_in_nth llength_lmap lnth_lmap)
 
   have derivns: "chain sr_ext.derive Gs"
     using ground_derive_chain deriv ns by auto
 
   have "\<exists>\<sigma>. D \<cdot> \<sigma> = C \<and> is_ground_subst \<sigma>"
-    using instance_if_subsumed_and_in_limit[OF ns c] D_p i_p by blast
+    using instance_if_subsumed_and_in_limit[OF deriv ns c] D_p i_p by blast
   then obtain \<sigma> where
     \<sigma>: "D \<cdot> \<sigma> = C" "is_ground_subst \<sigma>"
     by blast
 
   {
     assume a: "D \<in> ?Ns i"
     then obtain D' \<sigma>' l where D'_p:
       "D' \<in> ?Ps l \<union> ?Qs l"
       "D' \<cdot> \<sigma>' = C"
       "enat l < llength Sts"
       "is_ground_subst \<sigma>'"
       "\<forall>E \<in> {E. E \<in> (clss_of_state (Sup_state Sts)) \<and> subsumes E C}. \<not> strictly_subsumes E D'"
       "subsumes D' C"
       using from_N_to_P_or_Q deriv fair ns c i_p(1) D_p(2) D_p(3) by blast
     then obtain l' where
       l'_p: "D' \<in> ?Qs l'" "l' < llength Sts"
-      using from_P_to_Q[OF fair ns c _ D'_p(3) D'_p(6) D'_p(5)] by blast
+      using from_P_to_Q[OF deriv fair ns c _ D'_p(3) D'_p(6) D'_p(5)] by blast
     then have "D' \<in> Q_of_state (Liminf_state Sts)"
-      using from_Q_to_Q_inf[OF fair ns c _ l'_p(2)] D'_p by auto
+      using from_Q_to_Q_inf[OF deriv fair ns c _ l'_p(2)] D'_p by auto
     then have ?thesis
       using D'_p by auto
   }
   moreover
   {
     assume a: "D \<in> ?Ps i"
     then obtain l' where
       l'_p: "D \<in> ?Qs l'" "l' < llength Sts"
-      using from_P_to_Q[OF fair ns c a i_p(1) D_p(2) D_p(3)] by auto
+      using from_P_to_Q[OF deriv fair ns c a i_p(1) D_p(2) D_p(3)] by auto
     then have "D \<in> Q_of_state (Liminf_state Sts)"
-      using from_Q_to_Q_inf[OF fair ns c l'_p(1) l'_p(2)] D_p(3) \<sigma>(1) \<sigma>(2) D_p(2) by auto
+      using from_Q_to_Q_inf[OF deriv fair ns c l'_p(1) l'_p(2)] D_p(3) \<sigma>(1) \<sigma>(2) D_p(2) by auto
     then have ?thesis
       using D_p \<sigma> by auto
   }
   moreover
   {
     assume a: "D \<in> ?Qs i"
     then have "D \<in> Q_of_state (Liminf_state Sts)"
-      using from_Q_to_Q_inf[OF fair ns c a i_p(1)] \<sigma> D_p(2,3) by auto
+      using from_Q_to_Q_inf[OF deriv fair ns c a i_p(1)] \<sigma> D_p(2,3) by auto
     then have ?thesis
       using D_p \<sigma> by auto
   }
   ultimately show ?thesis
     using i_p by auto
 qed
 
 text \<open>
 The following corresponds to Lemma 4.11:
 \<close>
 
 lemma fair_imp_Liminf_minus_Rf_subset_ground_Liminf_state:
   assumes
+    deriv: "chain (\<leadsto>) Sts" and
     fair: "fair_state_seq Sts" and
     ns: "Gs = lmap grounding_of_state Sts"
-  shows "Liminf_llist Gs - sr.Rf (Liminf_llist Gs) \<subseteq> grounding_of_clss (Q_of_state (Liminf_state Sts))"
+  shows "Liminf_llist Gs - sr.Rf (Liminf_llist Gs)
+    \<subseteq> grounding_of_clss (Q_of_state (Liminf_state Sts))"
 proof
   let ?Ns = "\<lambda>i. N_of_state (lnth Sts i)"
   let ?Ps = "\<lambda>i. P_of_state (lnth Sts i)"
   let ?Qs = "\<lambda>i. Q_of_state (lnth Sts i)"
 
   have SQinf: "clss_of_state (Liminf_state Sts) = Liminf_llist (lmap Q_of_state Sts)"
     using fair unfolding fair_state_seq_def Liminf_state_def by auto
 
   fix C
   assume C_p: "C \<in> Liminf_llist Gs - sr.Rf (Liminf_llist Gs)"
   then have "C \<in> Sup_llist Gs"
     using Liminf_llist_subset_Sup_llist[of Gs] by blast
   then obtain D_proto where
     "D_proto \<in> clss_of_state (Sup_state Sts) \<and> subsumes D_proto C"
     using in_Sup_llist_in_Sup_state unfolding ns subsumes_def by blast
   then obtain D where
     D_p: "D \<in> clss_of_state (Sup_state Sts)"
     "subsumes D C"
     "\<forall>E \<in> {E. E \<in> clss_of_state (Sup_state Sts) \<and> subsumes E C}. \<not> strictly_subsumes E D"
     using strictly_subsumes_has_minimum[of "{E. E \<in> clss_of_state (Sup_state Sts) \<and> subsumes E C}"]
     by auto
 
   have ground_C: "is_ground_cls C"
     using C_p using Liminf_grounding_of_state_ground ns by auto
 
   have "\<exists>D' \<sigma>'. D' \<in> Q_of_state (Liminf_state Sts) \<and> D' \<cdot> \<sigma>' = C \<and> is_ground_subst \<sigma>'"
-    using eventually_in_Qinf[of D C Gs] using D_p(1-3) fair ns C_p ground_C by auto
+    using eventually_in_Qinf[of D C Gs] using D_p(1-3) deriv fair ns C_p ground_C by auto
   then obtain D' \<sigma>' where
     D'_p: "D' \<in> Q_of_state (Liminf_state Sts) \<and> D' \<cdot> \<sigma>' = C \<and> is_ground_subst \<sigma>'"
     by blast
   then have "D' \<in> clss_of_state (Liminf_state Sts)"
     by simp
   then have "C \<in> grounding_of_state (Liminf_state Sts)"
     unfolding grounding_of_clss_def grounding_of_cls_def using D'_p by auto
   then show "C \<in> grounding_of_clss (Q_of_state (Liminf_state Sts))"
     using SQinf fair fair_state_seq_def by auto
 qed
 
 text \<open>
 The following corresponds to (one direction of) Theorem 4.13:
 \<close>
 
 lemma ground_subclauses:
   assumes
     "\<forall>i < length CAs. CAs ! i = Cs ! i + poss (AAs ! i)" and
     "length Cs = length CAs" and
     "is_ground_cls_list CAs"
   shows "is_ground_cls_list Cs"
   unfolding is_ground_cls_list_def
   by (metis assms in_set_conv_nth is_ground_cls_list_def is_ground_cls_union)
 
 lemma subseteq_Liminf_state_eventually_always:
   fixes CC
   assumes
     "finite CC" and
     "CC \<noteq> {}" and
     "CC \<subseteq> Q_of_state (Liminf_state Sts)"
   shows "\<exists>j. enat j < llength Sts \<and> (\<forall>j' \<ge> enat j. j' < llength Sts \<longrightarrow> CC \<subseteq> Q_of_state (lnth Sts j'))"
 proof -
   from assms(3) have "\<forall>C \<in> CC. \<exists>j. enat j < llength Sts \<and>
     (\<forall>j' \<ge> enat j. j' < llength Sts \<longrightarrow> C \<in> Q_of_state (lnth Sts j'))"
     unfolding Liminf_state_def Liminf_llist_def by force
   then obtain f where
     f_p: "\<forall>C \<in> CC. f C < llength Sts \<and> (\<forall>j' \<ge> enat (f C). j' < llength Sts \<longrightarrow> C \<in> Q_of_state (lnth Sts j'))"
     by moura
 
   define j :: nat where
     "j = Max (f ` CC)"
 
   have "enat j < llength Sts"
     unfolding j_def using f_p assms(1)
     by (metis (mono_tags) Max_in assms(2) finite_imageI imageE image_is_empty)
   moreover have "\<forall>C j'. C \<in> CC \<longrightarrow> enat j \<le> j' \<longrightarrow> j' < llength Sts \<longrightarrow> C \<in> Q_of_state (lnth Sts j')"
   proof (intro allI impI)
     fix C :: "'a clause" and j' :: nat
     assume a: "C \<in> CC" "enat j \<le> enat j'" "enat j' < llength Sts"
     then have "f C \<le> j'"
       unfolding j_def using assms(1) Max.bounded_iff by auto
     then show "C \<in> Q_of_state (lnth Sts j')"
       using f_p a by auto
   qed
   ultimately show ?thesis
     by auto
 qed
 
 lemma empty_clause_in_Q_of_Liminf_state:
   assumes
-    empty_in: "{#} \<in> Liminf_llist (lmap grounding_of_state Sts)" and
-    fair: "fair_state_seq Sts"
+    deriv: "chain (\<leadsto>) Sts" and
+    fair: "fair_state_seq Sts" and
+    empty_in: "{#} \<in> Liminf_llist (lmap grounding_of_state Sts)"
   shows "{#} \<in> Q_of_state (Liminf_state Sts)"
 proof -
   define Gs :: "'a clause set llist" where
     ns: "Gs = lmap grounding_of_state Sts"
   from empty_in have in_Liminf_not_Rf: "{#} \<in> Liminf_llist Gs - sr.Rf (Liminf_llist Gs)"
     unfolding ns sr.Rf_def by auto
   then have "{#} \<in> grounding_of_clss (Q_of_state (Liminf_state Sts))"
-    using fair_imp_Liminf_minus_Rf_subset_ground_Liminf_state[OF fair ns] by auto
+    using fair_imp_Liminf_minus_Rf_subset_ground_Liminf_state[OF deriv fair ns] by auto
   then show ?thesis
     unfolding grounding_of_clss_def grounding_of_cls_def by auto
 qed
 
 lemma grounding_of_state_Liminf_state_subseteq:
   "grounding_of_state (Liminf_state Sts) \<subseteq> Liminf_llist (lmap grounding_of_state Sts)"
 proof
   fix C :: "'a clause"
   assume "C \<in> grounding_of_state (Liminf_state Sts)"
   then obtain D \<sigma> where
     D_\<sigma>_p: "D \<in> clss_of_state (Liminf_state Sts)" "D \<cdot> \<sigma> = C" "is_ground_subst \<sigma>"
     unfolding grounding_of_clss_def grounding_of_cls_def by auto
   then have ii: "D \<in> Liminf_llist (lmap N_of_state Sts)
     \<or> D \<in> Liminf_llist (lmap P_of_state Sts) \<or> D \<in> Liminf_llist (lmap Q_of_state Sts)"
     unfolding Liminf_state_def by simp
   then have "C \<in> Liminf_llist (lmap grounding_of_clss (lmap N_of_state Sts))
     \<or> C \<in> Liminf_llist (lmap grounding_of_clss (lmap P_of_state Sts))
     \<or> C \<in> Liminf_llist (lmap grounding_of_clss (lmap Q_of_state Sts))"
     unfolding Liminf_llist_def grounding_of_clss_def grounding_of_cls_def
     apply -
     apply (erule disjE)
     subgoal
       apply (rule disjI1)
       using D_\<sigma>_p by auto
     subgoal
       apply (erule HOL.disjE)
       subgoal
         apply (rule disjI2)
         apply (rule disjI1)
         using D_\<sigma>_p by auto
       subgoal
         apply (rule disjI2)
         apply (rule disjI2)
         using D_\<sigma>_p by auto
       done
     done
   then show "C \<in> Liminf_llist (lmap grounding_of_state Sts)"
     unfolding Liminf_llist_def grounding_of_clss_def by auto
 qed
 
 theorem RP_sound:
-  assumes "{#} \<in> clss_of_state (Liminf_state Sts)"
+  assumes
+    deriv: "chain (\<leadsto>) Sts" and
+    "{#} \<in> clss_of_state (Liminf_state Sts)"
   shows "\<not> satisfiable (grounding_of_state (lhd Sts))"
 proof -
   from assms have "{#} \<in> grounding_of_state (Liminf_state Sts)"
     unfolding grounding_of_clss_def by (force intro: ex_ground_subst)
   then have "{#} \<in> Liminf_llist (lmap grounding_of_state Sts)"
     using grounding_of_state_Liminf_state_subseteq by auto
   then have "\<not> satisfiable (Liminf_llist (lmap grounding_of_state Sts))"
     using true_clss_def by auto
   then have "\<not> satisfiable (lhd (lmap grounding_of_state Sts))"
-    using sr_ext.sat_limit_iff ground_derive_chain by blast
+    using sr_ext.sat_limit_iff ground_derive_chain deriv by blast
   then show ?thesis
-    unfolding lhd_lmap_Sts .
+    using chain_not_lnull deriv by fastforce
 qed
 
 theorem RP_saturated_if_fair:
   assumes
+    deriv: "chain (\<leadsto>) Sts" and
     fair: "fair_state_seq Sts" and
     empty_Q0: "Q_of_state (lhd Sts) = {}"
   shows "sr.saturated_upto (Liminf_llist (lmap grounding_of_state Sts))"
 proof -
   define Gs :: "'a clause set llist" where
     ns: "Gs = lmap grounding_of_state Sts"
 
   let ?N = "\<lambda>i. grounding_of_state (lnth Sts i)"
 
   let ?Ns = "\<lambda>i. N_of_state (lnth Sts i)"
   let ?Ps = "\<lambda>i. P_of_state (lnth Sts i)"
   let ?Qs = "\<lambda>i. Q_of_state (lnth Sts i)"
 
   have ground_ns_in_ground_limit_st:
     "Liminf_llist Gs - sr.Rf (Liminf_llist Gs) \<subseteq> grounding_of_clss (Q_of_state (Liminf_state Sts))"
     using fair deriv fair_imp_Liminf_minus_Rf_subset_ground_Liminf_state ns by blast
 
   have derivns: "chain sr_ext.derive Gs"
     using ground_derive_chain deriv ns by auto
 
   {
     fix \<gamma> :: "'a inference"
     assume \<gamma>_p: "\<gamma> \<in> gr.ord_\<Gamma>"
     let ?CC = "side_prems_of \<gamma>"
     let ?DA = "main_prem_of \<gamma>"
     let ?E = "concl_of \<gamma>"
     assume a: "set_mset ?CC \<union> {?DA}
       \<subseteq> Liminf_llist (lmap grounding_of_state Sts)
         - sr.Rf (Liminf_llist (lmap grounding_of_state Sts))"
 
     have ground_ground_Liminf: "is_ground_clss (Liminf_llist (lmap grounding_of_state Sts))"
       using Liminf_grounding_of_state_ground unfolding is_ground_clss_def by auto
 
     have ground_cc: "is_ground_clss (set_mset ?CC)"
       using a ground_ground_Liminf is_ground_clss_def by auto
 
     have ground_da: "is_ground_cls ?DA"
       using a grounding_ground singletonI ground_ground_Liminf
       by (simp add: Liminf_grounding_of_state_ground)
 
     from \<gamma>_p obtain CAs AAs As where
       CAs_p: "gr.ord_resolve CAs ?DA AAs As ?E \<and> mset CAs = ?CC"
       unfolding gr.ord_\<Gamma>_def by auto
 
     have DA_CAs_in_ground_Liminf:
       "{?DA} \<union> set CAs \<subseteq> grounding_of_clss (Q_of_state (Liminf_state Sts))"
       using a CAs_p fair unfolding fair_state_seq_def
       by (metis (no_types, lifting) Un_empty_left ground_ns_in_ground_limit_st a ns set_mset_mset
           subset_trans sup_commute)
 
     then have ground_cas: "is_ground_cls_list CAs"
       using CAs_p unfolding is_ground_cls_list_def by auto
 
     have "\<exists>\<sigma>. ord_resolve S_Q CAs ?DA AAs As \<sigma> ?E"
       by (rule ground_ord_resolve_imp_ord_resolve[OF ground_da ground_cas
             gr.ground_resolution_with_selection_axioms CAs_p[THEN conjunct1]])
     then obtain \<sigma> where
       \<sigma>_p: "ord_resolve S_Q CAs ?DA AAs As \<sigma> ?E"
       by auto
     then obtain \<eta>s' \<eta>' \<eta>2' CAs' DA' AAs' As' \<tau>' E' where s_p:
       "is_ground_subst \<eta>'"
       "is_ground_subst_list \<eta>s'"
       "is_ground_subst \<eta>2'"
       "ord_resolve_rename S CAs' DA' AAs' As' \<tau>' E'"
       "CAs' \<cdot>\<cdot>cl \<eta>s' = CAs"
       "DA' \<cdot> \<eta>' = ?DA"
       "E' \<cdot> \<eta>2' = ?E"
       "{DA'} \<union> set CAs' \<subseteq> Q_of_state (Liminf_state Sts)"
       using ord_resolve_rename_lifting[OF sel_stable, of "Q_of_state (Liminf_state Sts)" CAs ?DA]
         \<sigma>_p[unfolded S_Q_def] selection_axioms DA_CAs_in_ground_Liminf by metis
     from this(8) have "\<exists>j. enat j < llength Sts \<and> (set CAs' \<union> {DA'} \<subseteq> ?Qs j)"
       unfolding Liminf_llist_def
       using subseteq_Liminf_state_eventually_always[of "{DA'} \<union> set CAs'"] by auto
     then obtain j where
       j_p: "is_least (\<lambda>j. enat j < llength Sts \<and> set CAs' \<union> {DA'} \<subseteq> ?Qs j) j"
       using least_exists[of "\<lambda>j. enat j < llength Sts \<and> set CAs' \<union> {DA'} \<subseteq> ?Qs j"] by force
     then have j_p': "enat j < llength Sts" "set CAs' \<union> {DA'} \<subseteq> ?Qs j"
       unfolding is_least_def by auto
     then have jn0: "j \<noteq> 0"
       using empty_Q0 by (metis bot_eq_sup_iff gr_implies_not_zero insert_not_empty llength_lnull
           lnth_0_conv_lhd sup.orderE)
     then have j_adds_CAs': "\<not> set CAs' \<union> {DA'} \<subseteq> ?Qs (j - 1)" "set CAs' \<union> {DA'} \<subseteq> ?Qs j"
       using j_p unfolding is_least_def
        apply (metis (no_types) One_nat_def Suc_diff_Suc Suc_ile_eq diff_diff_cancel diff_zero
           less_imp_le less_one neq0_conv zero_less_diff)
       using j_p'(2) by blast
     have "lnth Sts (j - 1) \<leadsto> lnth Sts j"
       using j_p'(1) jn0 deriv chain_lnth_rel[of _ _ "j - 1"] by force
     then obtain C' where C'_p:
       "?Ns (j - 1) = {}"
       "?Ps (j - 1) = ?Ps j \<union> {C'}"
       "?Qs j = ?Qs (j - 1) \<union> {C'}"
       "?Ns j = concls_of (ord_FO_resolution.inferences_between (?Qs (j - 1)) C')"
       "C' \<in> set CAs' \<union> {DA'}"
       "C' \<notin> ?Qs (j - 1)"
       using j_adds_CAs' by (induction rule: RP.cases) auto
     have "E' \<in> ?Ns j"
     proof -
       have "E' \<in> concls_of (ord_FO_resolution.inferences_between (Q_of_state (lnth Sts (j - 1))) C')"
         unfolding infer_from_def ord_FO_\<Gamma>_def inference_system.inferences_between_def
         apply (rule_tac x = "Infer (mset CAs') DA' E'" in image_eqI)
         subgoal by auto
         subgoal
           unfolding infer_from_def
-          by (rule ord_resolve_rename.cases[OF s_p(4)])
-            (use s_p(4) C'_p(3) C'_p(5) j_p'(2) in force)
+          by (rule ord_resolve_rename.cases[OF s_p(4)]) (use s_p(4) C'_p(3,5) j_p'(2) in force)
         done
       then show ?thesis
         using C'_p(4) by auto
     qed
     then have "E' \<in> clss_of_state (lnth Sts j)"
       using j_p' by auto
     then have "?E \<in> grounding_of_state (lnth Sts j)"
       using s_p(7) s_p(3) unfolding grounding_of_clss_def grounding_of_cls_def by force
     then have "\<gamma> \<in> sr.Ri (grounding_of_state (lnth Sts j))"
       using sr.Ri_effective \<gamma>_p by auto
     then have "\<gamma> \<in> sr_ext_Ri (?N j)"
       unfolding sr_ext_Ri_def by auto
     then have "\<gamma> \<in> sr_ext_Ri (Sup_llist (lmap grounding_of_state Sts))"
       using j_p' contra_subsetD llength_lmap lnth_lmap lnth_subset_Sup_llist sr_ext.Ri_mono by smt
     then have "\<gamma> \<in> sr_ext_Ri (Liminf_llist (lmap grounding_of_state Sts))"
       using sr_ext.Ri_limit_Sup[of Gs] derivns ns by blast
   }
   then have "sr_ext.saturated_upto (Liminf_llist (lmap grounding_of_state Sts))"
     unfolding sr_ext.saturated_upto_def sr_ext.inferences_from_def infer_from_def sr_ext_Ri_def
     by auto
   then show ?thesis
     using gd_ord_\<Gamma>_ngd_ord_\<Gamma> sr.redundancy_criterion_axioms
       redundancy_criterion_standard_extension_saturated_upto_iff[of gr.ord_\<Gamma>]
     unfolding sr_ext_Ri_def by auto
 qed
 
 corollary RP_complete_if_fair:
   assumes
+    deriv: "chain (\<leadsto>) Sts" and
     fair: "fair_state_seq Sts" and
     empty_Q0: "Q_of_state (lhd Sts) = {}" and
     unsat: "\<not> satisfiable (grounding_of_state (lhd Sts))"
   shows "{#} \<in> Q_of_state (Liminf_state Sts)"
 proof -
   have "\<not> satisfiable (Liminf_llist (lmap grounding_of_state Sts))"
-    unfolding sr_ext.sat_limit_iff[OF ground_derive_chain]
-    by (rule unsat[folded lhd_lmap_Sts[of grounding_of_state]])
+    using unsat sr_ext.sat_limit_iff[OF ground_derive_chain] chain_not_lnull deriv by fastforce
   moreover have "sr.saturated_upto (Liminf_llist (lmap grounding_of_state Sts))"
-    by (rule RP_saturated_if_fair[OF fair empty_Q0, simplified])
+    by (rule RP_saturated_if_fair[OF deriv fair empty_Q0, simplified])
   ultimately have "{#} \<in> Liminf_llist (lmap grounding_of_state Sts)"
     using sr.saturated_upto_complete_if by auto
   then show ?thesis
-    using empty_clause_in_Q_of_Liminf_state fair by auto
+    using empty_clause_in_Q_of_Liminf_state[OF deriv fair] by auto
 qed
 
 end
 
 end
 
 end