diff --git a/thys/Ordered_Resolution_Prover/FO_Ordered_Resolution.thy b/thys/Ordered_Resolution_Prover/FO_Ordered_Resolution.thy
--- a/thys/Ordered_Resolution_Prover/FO_Ordered_Resolution.thy
+++ b/thys/Ordered_Resolution_Prover/FO_Ordered_Resolution.thy
@@ -1,1297 +1,1309 @@
 (*  Title:       First-Order Ordered Resolution Calculus with Selection
     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
+    Author:      Sophie Tourret <stourret at mpi-inf.mpg.de>, 2020
     Maintainer:  Anders Schlichtkrull <andschl at dtu.dk>
 *)
 
 section \<open>First-Order Ordered Resolution Calculus with Selection\<close>
 
 theory FO_Ordered_Resolution
   imports Abstract_Substitution Ordered_Ground_Resolution Standard_Redundancy
 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 ordered resolution calculus for
 first-order standard clauses presented in Figure 4 and its related lemmas and theorems, including
 soundness and Lemma 4.12 (the lifting lemma).
 
 The following corresponds to pages 41--42 of Section 4.3, until Figure 5 and its explanation.
 \<close>
 
 locale FO_resolution = mgu subst_atm id_subst comp_subst atm_of_atms renamings_apart mgu
   for
     subst_atm :: "'a :: wellorder \<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" +
   fixes
     less_atm :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   assumes
     less_atm_stable: "less_atm A B \<Longrightarrow> less_atm (A \<cdot>a \<sigma>) (B \<cdot>a \<sigma>)"
 begin
 
 
 subsection \<open>Library\<close>
 
 lemma Bex_cartesian_product: "(\<exists>xy \<in> A \<times> B. P xy) \<equiv> (\<exists>x \<in> A. \<exists>y \<in> B. P (x, y))"
   by simp
 
 (* FIXME: Move to "Multiset.thy" *)
 lemma length_sorted_list_of_multiset[simp]: "length (sorted_list_of_multiset A) = size A"
   by (metis mset_sorted_list_of_multiset size_mset)
 
 (* FIXME: move? or avoid? *)
 lemma eql_map_neg_lit_eql_atm:
   assumes "map (\<lambda>L. L \<cdot>l \<eta>) (map Neg As') = map Neg As"
   shows "As' \<cdot>al \<eta> = As"
   using assms by (induction As' arbitrary: As) auto
 
 lemma instance_list:
   assumes "negs (mset As) = SDA' \<cdot> \<eta>"
   shows "\<exists>As'. negs (mset As') = SDA' \<and> As' \<cdot>al \<eta> = As"
 proof -
   from assms have negL: "\<forall>L \<in># SDA'. is_neg L"
     using Melem_subst_cls subst_lit_in_negs_is_neg by metis
 
   from assms have "{#L \<cdot>l \<eta>. L \<in># SDA'#} = mset (map Neg As)"
     using subst_cls_def by auto
   then have "\<exists>NAs'. map (\<lambda>L. L \<cdot>l \<eta>) NAs' = map Neg As \<and> mset NAs' = SDA'"
     using image_mset_of_subset_list[of "\<lambda>L. L \<cdot>l \<eta>" SDA' "map Neg As"] by auto
   then obtain As' where As'_p:
     "map (\<lambda>L. L \<cdot>l \<eta>) (map Neg As') = map Neg As \<and> mset (map Neg As') = SDA'"
     by (metis (no_types, lifting) Neg_atm_of_iff negL ex_map_conv set_mset_mset)
 
   have "negs (mset As') = SDA'"
     using As'_p by auto
   moreover have "map (\<lambda>L. L \<cdot>l \<eta>) (map Neg As') = map Neg As"
     using As'_p by auto
   then have "As' \<cdot>al \<eta> = As"
     using eql_map_neg_lit_eql_atm by auto
   ultimately show ?thesis
     by blast
 qed
 
 
 context
   fixes S :: "'a clause \<Rightarrow> 'a clause"
 begin
 
 
 subsection \<open>Calculus\<close>
 
 text \<open>
 The following corresponds to Figure 4.
 \<close>
 
 definition maximal_wrt :: "'a \<Rightarrow> 'a literal multiset \<Rightarrow> bool" where
   "maximal_wrt A C \<longleftrightarrow> (\<forall>B \<in> atms_of C. \<not> less_atm A B)"
 
 definition strictly_maximal_wrt :: "'a \<Rightarrow> 'a literal multiset \<Rightarrow> bool" where
   "strictly_maximal_wrt A C \<equiv> \<forall>B \<in> atms_of C. A \<noteq> B \<and> \<not> less_atm A B"
 
 lemma strictly_maximal_wrt_maximal_wrt: "strictly_maximal_wrt A C \<Longrightarrow> maximal_wrt A C"
   unfolding maximal_wrt_def strictly_maximal_wrt_def by auto
 
 (* FIXME: use hd instead of ! 0 *)
 inductive eligible :: "'s \<Rightarrow> 'a list \<Rightarrow> 'a clause \<Rightarrow> bool" where
   eligible:
     "S DA = negs (mset As) \<or> S DA = {#} \<and> length As = 1 \<and> maximal_wrt (As ! 0 \<cdot>a \<sigma>) (DA \<cdot> \<sigma>) \<Longrightarrow>
      eligible \<sigma> As DA"
 
 inductive
   ord_resolve
   :: "'a clause list \<Rightarrow> 'a clause \<Rightarrow> 'a multiset list \<Rightarrow> 'a list \<Rightarrow> 's \<Rightarrow> 'a clause \<Rightarrow> bool"
 where
   ord_resolve:
     "length CAs = n \<Longrightarrow>
      length Cs = n \<Longrightarrow>
      length AAs = n \<Longrightarrow>
      length As = n \<Longrightarrow>
      n \<noteq> 0 \<Longrightarrow>
      (\<forall>i < n. CAs ! i = Cs ! i + poss (AAs ! i)) \<Longrightarrow>
      (\<forall>i < n. AAs ! i \<noteq> {#}) \<Longrightarrow>
      Some \<sigma> = mgu (set_mset ` set (map2 add_mset As AAs)) \<Longrightarrow>
      eligible \<sigma> As (D + negs (mset As)) \<Longrightarrow>
      (\<forall>i < n. strictly_maximal_wrt (As ! i \<cdot>a \<sigma>) (Cs ! i \<cdot> \<sigma>)) \<Longrightarrow>
      (\<forall>i < n. S (CAs ! i) = {#}) \<Longrightarrow>
      ord_resolve CAs (D + negs (mset As)) AAs As \<sigma> ((\<Union># (mset Cs) + D) \<cdot> \<sigma>)"
 
 inductive
   ord_resolve_rename
   :: "'a clause list \<Rightarrow> 'a clause \<Rightarrow> 'a multiset list \<Rightarrow> 'a list \<Rightarrow> 's \<Rightarrow> 'a clause \<Rightarrow> bool"
 where
   ord_resolve_rename:
     "length CAs = n \<Longrightarrow>
      length AAs = n \<Longrightarrow>
      length As = n \<Longrightarrow>
      (\<forall>i < n. poss (AAs ! i) \<subseteq># CAs ! i) \<Longrightarrow>
      negs (mset As) \<subseteq># DA \<Longrightarrow>
      \<rho> = hd (renamings_apart (DA # CAs)) \<Longrightarrow>
      \<rho>s = tl (renamings_apart (DA # CAs)) \<Longrightarrow>
      ord_resolve (CAs \<cdot>\<cdot>cl \<rho>s) (DA \<cdot> \<rho>) (AAs \<cdot>\<cdot>aml \<rho>s) (As \<cdot>al \<rho>) \<sigma> E \<Longrightarrow>
      ord_resolve_rename CAs DA AAs As \<sigma> E"
 
 lemma ord_resolve_empty_main_prem: "\<not> ord_resolve Cs {#} AAs As \<sigma> E"
   by (simp add: ord_resolve.simps)
 
 lemma ord_resolve_rename_empty_main_prem: "\<not> ord_resolve_rename Cs {#} AAs As \<sigma> E"
   by (simp add: ord_resolve_empty_main_prem ord_resolve_rename.simps)
 
 
 subsection \<open>Soundness\<close>
 
 text \<open>
 Soundness is not discussed in the chapter, but it is an important property.
 \<close>
 
 lemma ord_resolve_ground_inst_sound:
   assumes
     res_e: "ord_resolve CAs DA AAs As \<sigma> E" and
     cc_inst_true: "I \<Turnstile>m mset CAs \<cdot>cm \<sigma> \<cdot>cm \<eta>" and
     d_inst_true: "I \<Turnstile> DA \<cdot> \<sigma> \<cdot> \<eta>" and
     ground_subst_\<eta>: "is_ground_subst \<eta>"
   shows "I \<Turnstile> E \<cdot> \<eta>"
   using res_e
 proof (cases rule: ord_resolve.cases)
   case (ord_resolve n Cs D)
   note da = this(1) and e = this(2) and cas_len = this(3) and cs_len = this(4) and
     aas_len = this(5) and as_len = this(6) and cas = this(8) and mgu = this(10) and
     len = this(1)
 
   have len: "length CAs = length As"
     using as_len cas_len by auto
   have "is_ground_subst (\<sigma> \<odot> \<eta>)"
     using ground_subst_\<eta> by (rule is_ground_comp_subst)
   then have cc_true: "I \<Turnstile>m mset CAs \<cdot>cm \<sigma> \<cdot>cm \<eta>" and d_true: "I \<Turnstile> DA \<cdot> \<sigma> \<cdot> \<eta>"
     using cc_inst_true d_inst_true by auto
 
   from mgu have unif: "\<forall>i < n. \<forall>A\<in>#AAs ! i. A \<cdot>a \<sigma> = As ! i \<cdot>a \<sigma>"
     using mgu_unifier as_len aas_len by blast
 
   show "I \<Turnstile> E \<cdot> \<eta>"
   proof (cases "\<forall>A \<in> set As. A \<cdot>a \<sigma> \<cdot>a \<eta> \<in> I")
     case True
     then have "\<not> I \<Turnstile> negs (mset As) \<cdot> \<sigma> \<cdot> \<eta>"
       unfolding true_cls_def[of I] by auto
     then have "I \<Turnstile> D \<cdot> \<sigma> \<cdot> \<eta>"
       using d_true da by auto
     then show ?thesis
       unfolding e by auto
   next
     case False
     then obtain i where a_in_aa: "i < length CAs" and a_false: "(As ! i) \<cdot>a \<sigma> \<cdot>a \<eta> \<notin> I"
       using da len by (metis in_set_conv_nth)
     define C where "C \<equiv> Cs ! i"
     define BB where "BB \<equiv> AAs ! i"
     have c_cf': "C \<subseteq># \<Union># (mset CAs)"
       unfolding C_def using a_in_aa cas cas_len
       by (metis less_subset_eq_Union_mset mset_subset_eq_add_left subset_mset.order.trans)
     have c_in_cc: "C + poss BB \<in># mset CAs"
       using C_def BB_def a_in_aa cas_len in_set_conv_nth cas by fastforce
     {
       fix B
       assume "B \<in># BB"
       then have "B \<cdot>a \<sigma> = (As ! i) \<cdot>a \<sigma>"
         using unif a_in_aa cas_len unfolding BB_def by auto
     }
     then have "\<not> I \<Turnstile> poss BB \<cdot> \<sigma> \<cdot> \<eta>"
       using a_false by (auto simp: true_cls_def)
     moreover have "I \<Turnstile> (C + poss BB) \<cdot> \<sigma> \<cdot> \<eta>"
       using c_in_cc cc_true true_cls_mset_true_cls[of I "mset CAs \<cdot>cm \<sigma> \<cdot>cm \<eta>"] by force
     ultimately have "I \<Turnstile> C \<cdot> \<sigma> \<cdot> \<eta>"
       by simp
     then show ?thesis
       unfolding e subst_cls_union using c_cf' C_def a_in_aa cas_len cs_len
       by (metis (no_types, lifting) mset_subset_eq_add_left nth_mem_mset set_mset_mono sum_mset.remove true_cls_mono subst_cls_mono)
   qed
 qed
 
 text \<open>
-The previous lemma is not only used to prove soundness, but also the following lemma which is 
+The previous lemma is not only used to prove soundness, but also the following lemma which is
 used to prove Lemma 4.10.
 \<close>
 
 lemma ord_resolve_rename_ground_inst_sound:
   assumes
     "ord_resolve_rename CAs DA AAs As \<sigma> E" and
     "\<rho>s = tl (renamings_apart (DA # CAs))" and
     "\<rho> = hd (renamings_apart (DA # CAs))" and
     "I \<Turnstile>m (mset (CAs \<cdot>\<cdot>cl \<rho>s)) \<cdot>cm \<sigma> \<cdot>cm \<eta>" and
     "I \<Turnstile> DA \<cdot> \<rho> \<cdot> \<sigma> \<cdot> \<eta>" and
     "is_ground_subst \<eta>"
   shows "I \<Turnstile> E \<cdot> \<eta>"
   using assms by (cases rule: ord_resolve_rename.cases) (fast intro: ord_resolve_ground_inst_sound)
 
 text \<open>
 Here follows the soundness theorem for the resolution rule.
 \<close>
 
 theorem ord_resolve_sound:
  assumes
    res_e: "ord_resolve CAs DA AAs As \<sigma> E" and
    cc_d_true: "\<And>\<sigma>. is_ground_subst \<sigma> \<Longrightarrow> I \<Turnstile>m (mset CAs + {#DA#}) \<cdot>cm \<sigma>" and
    ground_subst_\<eta>: "is_ground_subst \<eta>"
  shows "I \<Turnstile> E \<cdot> \<eta>"
 proof (use res_e in \<open>cases rule: ord_resolve.cases\<close>)
   case (ord_resolve n Cs D)
   note da = this(1) and e = this(2) and cas_len = this(3) and cs_len = this(4)
     and aas_len = this(5) and as_len = this(6) and cas = this(8) and mgu = this(10)
   have ground_subst_\<sigma>_\<eta>: "is_ground_subst (\<sigma> \<odot> \<eta>)"
     using ground_subst_\<eta> by (rule is_ground_comp_subst)
   have cas_true: "I \<Turnstile>m mset CAs \<cdot>cm \<sigma> \<cdot>cm \<eta>"
     using cc_d_true ground_subst_\<sigma>_\<eta> by fastforce
   have da_true: "I \<Turnstile> DA \<cdot> \<sigma> \<cdot> \<eta>"
     using cc_d_true ground_subst_\<sigma>_\<eta> by fastforce
   show "I \<Turnstile> E \<cdot> \<eta>"
     using ord_resolve_ground_inst_sound[OF res_e cas_true da_true] ground_subst_\<eta> by auto
 qed
 
 lemma subst_sound:
-  assumes 
+  assumes
     "\<And>\<sigma>. is_ground_subst \<sigma> \<Longrightarrow> I \<Turnstile> (C \<cdot> \<sigma>)" and
     "is_ground_subst \<eta>"
   shows "I \<Turnstile> (C \<cdot> \<rho>) \<cdot> \<eta>"
-  using assms is_ground_comp_subst subst_cls_comp_subst by metis 
+  using assms is_ground_comp_subst subst_cls_comp_subst by metis
 
 lemma subst_sound_scl:
   assumes
     len: "length P = length CAs" and
     true_cas: "\<And>\<sigma>. is_ground_subst \<sigma> \<Longrightarrow> I \<Turnstile>m (mset CAs) \<cdot>cm \<sigma>" and
-    ground_subst_\<eta>: "is_ground_subst \<eta>" 
+    ground_subst_\<eta>: "is_ground_subst \<eta>"
   shows "I \<Turnstile>m mset (CAs \<cdot>\<cdot>cl P) \<cdot>cm \<eta>"
 proof -
   from true_cas have "\<And>CA. CA\<in># mset CAs \<Longrightarrow> (\<And>\<sigma>. is_ground_subst \<sigma> \<Longrightarrow> I \<Turnstile> CA \<cdot> \<sigma>)"
     unfolding true_cls_mset_def by force
   then have "\<forall>i < length CAs. \<forall>\<sigma>. is_ground_subst \<sigma> \<longrightarrow> (I \<Turnstile> CAs ! i \<cdot> \<sigma>)"
     using in_set_conv_nth by auto
   then have true_cp: "\<forall>i < length CAs. \<forall>\<sigma>. is_ground_subst \<sigma> \<longrightarrow> I \<Turnstile> CAs ! i \<cdot> P ! i \<cdot> \<sigma>"
     using subst_sound len by auto
 
   {
     fix CA
     assume "CA \<in># mset (CAs \<cdot>\<cdot>cl P)"
     then obtain i where
       i_x: "i < length (CAs \<cdot>\<cdot>cl P)" "CA = (CAs \<cdot>\<cdot>cl P) ! i"
       by (metis in_mset_conv_nth)
     then have "\<forall>\<sigma>. is_ground_subst \<sigma> \<longrightarrow> I \<Turnstile> CA \<cdot> \<sigma>"
       using true_cp unfolding subst_cls_lists_def by (simp add: len)
   }
   then show ?thesis
     using assms unfolding true_cls_mset_def by auto
 qed
 
 text \<open>
 Here follows the soundness theorem for the resolution rule with renaming.
 \<close>
 
 lemma ord_resolve_rename_sound:
   assumes
     res_e: "ord_resolve_rename CAs DA AAs As \<sigma> E" and
     cc_d_true: "\<And>\<sigma>. is_ground_subst \<sigma> \<Longrightarrow> I \<Turnstile>m ((mset CAs) + {#DA#}) \<cdot>cm \<sigma>" and
     ground_subst_\<eta>: "is_ground_subst \<eta>"
   shows "I \<Turnstile> E \<cdot> \<eta>"
   using res_e
 proof (cases rule: ord_resolve_rename.cases)
   case (ord_resolve_rename n \<rho> \<rho>s)
   note \<rho>s = this(7) and res = this(8)
   have len: "length \<rho>s = length CAs"
     using \<rho>s renamings_apart_length by auto
   have "\<And>\<sigma>. is_ground_subst \<sigma> \<Longrightarrow> I \<Turnstile>m (mset (CAs \<cdot>\<cdot>cl \<rho>s) + {#DA \<cdot> \<rho>#}) \<cdot>cm \<sigma>"
     using subst_sound_scl[OF len, of I] subst_sound cc_d_true by auto
   then show "I \<Turnstile> E \<cdot> \<eta>"
     using ground_subst_\<eta> ord_resolve_sound[OF res] by simp
 qed
 
 
 subsection \<open>Other Basic Properties\<close>
 
 lemma ord_resolve_unique:
   assumes
     "ord_resolve CAs DA AAs As \<sigma> E" and
     "ord_resolve CAs DA AAs As \<sigma>' E'"
   shows "\<sigma> = \<sigma>' \<and> E = E'"
   using assms
 proof (cases rule: ord_resolve.cases[case_product ord_resolve.cases], intro conjI)
   case (ord_resolve_ord_resolve CAs n Cs AAs As \<sigma>'' DA CAs' n' Cs' AAs' As' \<sigma>''' DA')
   note res = this(1-17) and res' = this(18-34)
 
   show \<sigma>: "\<sigma> = \<sigma>'"
     using res(3-5,14) res'(3-5,14) by (metis option.inject)
 
   have "Cs = Cs'"
     using res(1,3,7,8,12) res'(1,3,7,8,12) by (metis add_right_imp_eq nth_equalityI)
   moreover have "DA = DA'"
     using res(2,4) res'(2,4) by fastforce
   ultimately show "E = E'"
     using res(5,6) res'(5,6) \<sigma> by blast
 qed
 
 lemma ord_resolve_rename_unique:
   assumes
     "ord_resolve_rename CAs DA AAs As \<sigma> E" and
     "ord_resolve_rename CAs DA AAs As \<sigma>' E'"
   shows "\<sigma> = \<sigma>' \<and> E = E'"
   using assms unfolding ord_resolve_rename.simps using ord_resolve_unique by meson
 
 lemma ord_resolve_max_side_prems: "ord_resolve CAs DA AAs As \<sigma> E \<Longrightarrow> length CAs \<le> size DA"
   by (auto elim!: ord_resolve.cases)
 
 lemma ord_resolve_rename_max_side_prems:
   "ord_resolve_rename CAs DA AAs As \<sigma> E \<Longrightarrow> length CAs \<le> size DA"
   by (elim ord_resolve_rename.cases, drule ord_resolve_max_side_prems, simp add: renamings_apart_length)
 
 
 subsection \<open>Inference System\<close>
 
 definition ord_FO_\<Gamma> :: "'a inference set" where
   "ord_FO_\<Gamma> = {Infer (mset CAs) DA E | CAs DA AAs As \<sigma> E. ord_resolve_rename CAs DA AAs As \<sigma> E}"
 
 interpretation ord_FO_resolution: inference_system ord_FO_\<Gamma> .
 
 lemma exists_compose: "\<exists>x. P (f x) \<Longrightarrow> \<exists>y. P y"
   by meson
 
 lemma finite_ord_FO_resolution_inferences_between:
   assumes fin_cc: "finite CC"
   shows "finite (ord_FO_resolution.inferences_between CC C)"
 proof -
   let ?CCC = "CC \<union> {C}"
 
   define all_AA where "all_AA = (\<Union>D \<in> ?CCC. atms_of D)"
   define max_ary where "max_ary = Max (size ` ?CCC)"
   define CAS where "CAS = {CAs. CAs \<in> lists ?CCC \<and> length CAs \<le> max_ary}"
   define AS where "AS = {As. As \<in> lists all_AA \<and> length As \<le> max_ary}"
   define AAS where "AAS = {AAs. AAs \<in> lists (mset ` AS) \<and> length AAs \<le> max_ary}"
 
   note defs = all_AA_def max_ary_def CAS_def AS_def AAS_def
 
   let ?infer_of =
     "\<lambda>CAs DA AAs As. Infer (mset CAs) DA (THE E. \<exists>\<sigma>. ord_resolve_rename CAs DA AAs As \<sigma> E)"
 
   let ?Z = "{\<gamma> | CAs DA AAs As \<sigma> E \<gamma>. \<gamma> = Infer (mset CAs) DA E
     \<and> ord_resolve_rename CAs DA AAs As \<sigma> E \<and> infer_from ?CCC \<gamma> \<and> C \<in># prems_of \<gamma>}"
   let ?Y = "{Infer (mset CAs) DA E | CAs DA AAs As \<sigma> E.
     ord_resolve_rename CAs DA AAs As \<sigma> E \<and> set CAs \<union> {DA} \<subseteq> ?CCC}"
   let ?X = "{?infer_of CAs DA AAs As | CAs DA AAs As. CAs \<in> CAS \<and> DA \<in> ?CCC \<and> AAs \<in> AAS \<and> As \<in> AS}"
   let ?W = "CAS \<times> ?CCC \<times> AAS \<times> AS"
 
   have fin_w: "finite ?W"
     unfolding defs using fin_cc by (simp add: finite_lists_length_le lists_eq_set)
 
   have "?Z \<subseteq> ?Y"
     by (force simp: infer_from_def)
   also have "\<dots> \<subseteq> ?X"
   proof -
     {
       fix CAs DA AAs As \<sigma> E
       assume
         res_e: "ord_resolve_rename CAs DA AAs As \<sigma> E" and
         da_in: "DA \<in> ?CCC" and
         cas_sub: "set CAs \<subseteq> ?CCC"
 
       have "E = (THE E. \<exists>\<sigma>. ord_resolve_rename CAs DA AAs As \<sigma> E)
         \<and> CAs \<in> CAS \<and> AAs \<in> AAS \<and> As \<in> AS" (is "?e \<and> ?cas \<and> ?aas \<and> ?as")
       proof (intro conjI)
         show ?e
           using res_e ord_resolve_rename_unique by (blast intro: the_equality[symmetric])
       next
         show ?cas
           unfolding CAS_def max_ary_def using cas_sub
             ord_resolve_rename_max_side_prems[OF res_e] da_in fin_cc
           by (auto simp add: Max_ge_iff)
       next
         show ?aas
           using res_e
         proof (cases rule: ord_resolve_rename.cases)
           case (ord_resolve_rename n \<rho> \<rho>s)
           note len_cas = this(1) and len_aas = this(2) and len_as = this(3) and
             aas_sub = this(4) and as_sub = this(5) and res_e' = this(8)
 
           show ?thesis
             unfolding AAS_def
           proof (clarify, intro conjI)
             show "AAs \<in> lists (mset ` AS)"
               unfolding AS_def image_def
             proof clarsimp
               fix AA
               assume "AA \<in> set AAs"
               then obtain i where
                 i_lt: "i < n" and
                 aa: "AA = AAs ! i"
                 by (metis in_set_conv_nth len_aas)
 
               have casi_in: "CAs ! i \<in> ?CCC"
                 using i_lt len_cas cas_sub nth_mem by blast
 
               have pos_aa_sub: "poss AA \<subseteq># CAs ! i"
                 using aa aas_sub i_lt by blast
               then have "set_mset AA \<subseteq> atms_of (CAs ! i)"
                 by (metis atms_of_poss lits_subseteq_imp_atms_subseteq set_mset_mono)
               also have aa_sub: "\<dots> \<subseteq> all_AA"
                 unfolding all_AA_def using casi_in by force
               finally have aa_sub: "set_mset AA \<subseteq> all_AA"
                 .
 
               have "size AA = size (poss AA)"
                 by simp
               also have "\<dots> \<le> size (CAs ! i)"
                 by (rule size_mset_mono[OF pos_aa_sub])
               also have "\<dots> \<le> max_ary"
                 unfolding max_ary_def using fin_cc casi_in by auto
               finally have sz_aa: "size AA \<le> max_ary"
                 .
 
               let ?As' = "sorted_list_of_multiset AA"
 
               have "?As' \<in> lists all_AA"
                 using aa_sub by auto
               moreover have "length ?As' \<le> max_ary"
                 using sz_aa by simp
               moreover have "AA = mset ?As'"
                 by simp
               ultimately show "\<exists>xa. xa \<in> lists all_AA \<and> length xa \<le> max_ary \<and> AA = mset xa"
                 by blast
             qed
           next
             have "length AAs = length As"
               unfolding len_aas len_as ..
             also have "\<dots> \<le> size DA"
               using as_sub size_mset_mono by fastforce
             also have "\<dots> \<le> max_ary"
               unfolding max_ary_def using fin_cc da_in by auto
             finally show "length AAs \<le> max_ary"
               .
           qed
         qed
       next
         show ?as
           unfolding AS_def
         proof (clarify, intro conjI)
           have "set As \<subseteq> atms_of DA"
             using res_e[simplified ord_resolve_rename.simps]
             by (metis atms_of_negs lits_subseteq_imp_atms_subseteq set_mset_mono set_mset_mset)
           also have "\<dots> \<subseteq> all_AA"
             unfolding all_AA_def using da_in by blast
           finally show "As \<in> lists all_AA"
             unfolding lists_eq_set by simp
         next
           have "length As \<le> size DA"
             using res_e[simplified ord_resolve_rename.simps]
               ord_resolve_rename_max_side_prems[OF res_e] by auto
           also have "size DA \<le> max_ary"
             unfolding max_ary_def using fin_cc da_in by auto
           finally show "length As \<le> max_ary"
             .
         qed
       qed
     }
     then show ?thesis
       by simp fast
   qed
   also have "\<dots> \<subseteq> (\<lambda>(CAs, DA, AAs, As). ?infer_of CAs DA AAs As) ` ?W"
     unfolding image_def Bex_cartesian_product by fast
   finally show ?thesis
     unfolding inference_system.inferences_between_def ord_FO_\<Gamma>_def mem_Collect_eq
     by (fast intro: rev_finite_subset[OF finite_imageI[OF fin_w]])
 qed
 
 lemma ord_FO_resolution_inferences_between_empty_empty:
   "ord_FO_resolution.inferences_between {} {#} = {}"
   unfolding ord_FO_resolution.inferences_between_def inference_system.inferences_between_def
     infer_from_def ord_FO_\<Gamma>_def
   using ord_resolve_rename_empty_main_prem by auto
 
 
 subsection \<open>Lifting\<close>
 
 text \<open>
 The following corresponds to the passage between Lemmas 4.11 and 4.12.
 \<close>
 
 context
   fixes M :: "'a clause set"
   assumes select: "selection S"
 begin
 
 interpretation selection
   by (rule select)
 
 definition S_M :: "'a literal multiset \<Rightarrow> 'a literal multiset" where
   "S_M C =
    (if C \<in> grounding_of_clss M then
       (SOME C'. \<exists>D \<sigma>. D \<in> M \<and> C = D \<cdot> \<sigma> \<and> C' = S D \<cdot> \<sigma> \<and> is_ground_subst \<sigma>)
     else
       S C)"
 
 lemma S_M_grounding_of_clss:
   assumes "C \<in> grounding_of_clss M"
   obtains D \<sigma> where
     "D \<in> M \<and> C = D \<cdot> \<sigma> \<and> S_M C = S D \<cdot> \<sigma> \<and> is_ground_subst \<sigma>"
 proof (atomize_elim, unfold S_M_def eqTrueI[OF assms] if_True, rule someI_ex)
   from assms show "\<exists>C' D \<sigma>. D \<in> M \<and> C = D \<cdot> \<sigma> \<and> C' = S D \<cdot> \<sigma> \<and> is_ground_subst \<sigma>"
     by (auto simp: grounding_of_clss_def grounding_of_cls_def)
 qed
 
 lemma S_M_not_grounding_of_clss: "C \<notin> grounding_of_clss M \<Longrightarrow> S_M C = S C"
   unfolding S_M_def by simp
 
 lemma S_M_selects_subseteq: "S_M C \<subseteq># C"
   by (metis S_M_grounding_of_clss S_M_not_grounding_of_clss S_selects_subseteq subst_cls_mono_mset)
 
 lemma S_M_selects_neg_lits: "L \<in># S_M C \<Longrightarrow> is_neg L"
   by (metis Melem_subst_cls S_M_grounding_of_clss S_M_not_grounding_of_clss S_selects_neg_lits
       subst_lit_is_neg)
 
 end
 
 end
 
 text \<open>
 The following corresponds to Lemma 4.12:
 \<close>
 
 lemma map2_add_mset_map:
   assumes "length AAs' = n" and "length As' = n"
   shows "map2 add_mset (As' \<cdot>al \<eta>) (AAs' \<cdot>aml \<eta>) = map2 add_mset As' AAs' \<cdot>aml \<eta>"
   using assms
 proof (induction n arbitrary: AAs' As')
   case (Suc n)
   then have "map2 add_mset (tl (As' \<cdot>al \<eta>)) (tl (AAs' \<cdot>aml \<eta>)) = map2 add_mset (tl As') (tl AAs') \<cdot>aml \<eta>"
     by simp
   moreover
   have Succ: "length (As' \<cdot>al \<eta>) = Suc n" "length (AAs' \<cdot>aml \<eta>) = Suc n"
     using Suc(3) Suc(2) by auto
   then have "length (tl (As' \<cdot>al \<eta>)) = n" "length (tl (AAs' \<cdot>aml \<eta>)) = n"
     by auto
   then have "length (map2 add_mset (tl (As' \<cdot>al \<eta>)) (tl (AAs' \<cdot>aml \<eta>))) = n"
     "length (map2 add_mset (tl As') (tl AAs') \<cdot>aml \<eta>) = n"
     using Suc(2,3) by auto
   ultimately have "\<forall>i < n. tl (map2 add_mset ( (As' \<cdot>al \<eta>)) ((AAs' \<cdot>aml \<eta>))) ! i =
     tl (map2 add_mset (As') (AAs') \<cdot>aml \<eta>) ! i"
     using Suc(2,3) Succ by (simp add: map2_tl map_tl subst_atm_mset_list_def del: subst_atm_list_tl)
   moreover have nn: "length (map2 add_mset ((As' \<cdot>al \<eta>)) ((AAs' \<cdot>aml \<eta>))) = Suc n"
     "length (map2 add_mset (As') (AAs') \<cdot>aml \<eta>) = Suc n"
     using Succ Suc by auto
   ultimately have "\<forall>i. i < Suc n \<longrightarrow> i > 0 \<longrightarrow>
     map2 add_mset (As' \<cdot>al \<eta>) (AAs' \<cdot>aml \<eta>) ! i = (map2 add_mset As' AAs' \<cdot>aml \<eta>) ! i"
     by (auto simp: subst_atm_mset_list_def gr0_conv_Suc subst_atm_mset_def)
   moreover have "add_mset (hd As' \<cdot>a \<eta>) (hd AAs' \<cdot>am \<eta>) = add_mset (hd As') (hd AAs') \<cdot>am \<eta>"
     unfolding subst_atm_mset_def by auto
   then have "(map2 add_mset (As' \<cdot>al \<eta>) (AAs' \<cdot>aml \<eta>)) ! 0  = (map2 add_mset (As') (AAs') \<cdot>aml \<eta>) ! 0"
     using Suc by (simp add: Succ(2) subst_atm_mset_def)
   ultimately have "\<forall>i < Suc n. (map2 add_mset (As' \<cdot>al \<eta>) (AAs' \<cdot>aml \<eta>)) ! i =
     (map2 add_mset (As') (AAs') \<cdot>aml \<eta>) ! i"
     using Suc by auto
   then show ?case
     using nn list_eq_iff_nth_eq by metis
 qed auto
 
 lemma maximal_wrt_subst: "maximal_wrt (A \<cdot>a \<sigma>) (C \<cdot> \<sigma>) \<Longrightarrow> maximal_wrt A C"
   unfolding maximal_wrt_def using in_atms_of_subst less_atm_stable by blast
 
 lemma strictly_maximal_wrt_subst: "strictly_maximal_wrt (A \<cdot>a \<sigma>) (C \<cdot> \<sigma>) \<Longrightarrow> strictly_maximal_wrt A C"
   unfolding strictly_maximal_wrt_def using in_atms_of_subst less_atm_stable by blast
 
 lemma ground_resolvent_subset:
   assumes
     gr_cas: "is_ground_cls_list CAs" and
     gr_da: "is_ground_cls DA" and
     res_e: "ord_resolve S CAs DA AAs As \<sigma> E"
   shows "E \<subseteq># \<Union># (mset CAs) + DA"
   using res_e
 proof (cases rule: ord_resolve.cases)
   case (ord_resolve n Cs D)
   note da = this(1) and e = this(2) and cas_len = this(3) and cs_len = this(4)
     and aas_len = this(5) and as_len = this(6) and cas = this(8) and mgu = this(10)
   then have cs_sub_cas: "\<Union># (mset Cs) \<subseteq># \<Union># (mset CAs)"
     using subseteq_list_Union_mset cas_len cs_len by force
   then have cs_sub_cas: "\<Union># (mset Cs) \<subseteq># \<Union># (mset CAs)"
     using subseteq_list_Union_mset cas_len cs_len by force
   then have gr_cs: "is_ground_cls_list Cs"
     using gr_cas by simp
   have d_sub_da: "D \<subseteq># DA"
     by (simp add: da)
   then have gr_d: "is_ground_cls D"
     using gr_da is_ground_cls_mono by auto
 
   have "is_ground_cls (\<Union># (mset Cs) + D)"
     using gr_cs gr_d by auto
   with e have "E = \<Union># (mset Cs) + D"
     by auto
   then show ?thesis
     using cs_sub_cas d_sub_da by (auto simp: subset_mset.add_mono)
 qed
 
 lemma ord_resolve_obtain_clauses:
   assumes
     res_e: "ord_resolve (S_M S M) CAs DA AAs As \<sigma> E" and
     select: "selection S" and
     grounding: "{DA} \<union> set CAs \<subseteq> grounding_of_clss M" and
     n: "length CAs = n" and
     d: "DA = D + negs (mset As)" and
     c: "(\<forall>i < n. CAs ! i = Cs ! i + poss (AAs ! i))" "length Cs = n" "length AAs = n"
   obtains DA0 \<eta>0 CAs0 \<eta>s0 As0 AAs0 D0 Cs0 where
     "length CAs0 = n"
     "length \<eta>s0 = n"
     "DA0 \<in> M"
     "DA0 \<cdot> \<eta>0 = DA"
     "S DA0 \<cdot> \<eta>0 = S_M S M DA"
     "\<forall>CA0 \<in> set CAs0. CA0 \<in> M"
     "CAs0 \<cdot>\<cdot>cl \<eta>s0 = CAs"
     "map S CAs0 \<cdot>\<cdot>cl \<eta>s0 = map (S_M S M) CAs"
     "is_ground_subst \<eta>0"
     "is_ground_subst_list \<eta>s0"
     "As0  \<cdot>al \<eta>0 = As"
     "AAs0 \<cdot>\<cdot>aml \<eta>s0 = AAs"
     "length As0 = n"
     "D0 \<cdot> \<eta>0 = D"
     "DA0 = D0 + (negs (mset As0))"
     "S_M S M (D + negs (mset As)) \<noteq> {#} \<Longrightarrow> negs (mset As0) = S DA0"
     "length Cs0 = n"
     "Cs0 \<cdot>\<cdot>cl \<eta>s0 = Cs"
     "\<forall>i < n. CAs0 ! i = Cs0 ! i + poss (AAs0 ! i)"
     "length AAs0 = n"
   using res_e
 proof (cases rule: ord_resolve.cases)
   case (ord_resolve n_twin Cs_twins D_twin)
   note da = this(1) and e = this(2) and cas = this(8) and mgu = this(10) and eligible = this(11)
   from ord_resolve have "n_twin = n" "D_twin = D"
     using n d by auto
   moreover have "Cs_twins = Cs"
     using c cas n calculation(1) \<open>length Cs_twins = n_twin\<close> by (auto simp add: nth_equalityI)
   ultimately
   have nz: "n \<noteq> 0" and cs_len: "length Cs = n" and aas_len: "length AAs = n" and as_len: "length As = n"
     and da: "DA = D + negs (mset As)" and eligible: "eligible (S_M S M) \<sigma> As (D + negs (mset As))"
     and cas: "\<forall>i<n. CAs ! i = Cs ! i + poss (AAs ! i)"
     using ord_resolve by force+
 
   note n = \<open>n \<noteq> 0\<close> \<open>length CAs = n\<close> \<open>length Cs = n\<close> \<open>length AAs = n\<close> \<open>length As = n\<close>
 
   interpret S: selection S by (rule select)
 
   \<comment> \<open>Obtain FO side premises\<close>
   have "\<forall>CA \<in> set CAs. \<exists>CA0 \<eta>c0. CA0 \<in> M \<and> CA0 \<cdot> \<eta>c0 = CA \<and> S CA0 \<cdot> \<eta>c0 = S_M S M CA \<and> is_ground_subst \<eta>c0"
     using grounding S_M_grounding_of_clss select by (metis (no_types) le_supE subset_iff)
   then have "\<forall>i < n. \<exists>CA0 \<eta>c0. CA0 \<in> M \<and> CA0 \<cdot> \<eta>c0 = (CAs ! i) \<and> S CA0 \<cdot> \<eta>c0 = S_M S M (CAs ! i) \<and> is_ground_subst \<eta>c0"
     using n by force
   then obtain \<eta>s0f CAs0f where f_p:
     "\<forall>i < n. CAs0f i \<in> M"
     "\<forall>i < n. (CAs0f i) \<cdot> (\<eta>s0f i) = (CAs ! i)"
     "\<forall>i < n. S (CAs0f i)  \<cdot> (\<eta>s0f i) = S_M S M (CAs ! i)"
     "\<forall>i < n. is_ground_subst (\<eta>s0f i)"
     using n by (metis (no_types))
 
   define \<eta>s0 where
     "\<eta>s0 = map \<eta>s0f [0 ..<n]"
   define CAs0 where
     "CAs0 = map CAs0f [0 ..<n]"
 
   have "length \<eta>s0 = n" "length CAs0 = n"
     unfolding \<eta>s0_def CAs0_def by auto
   note n = \<open>length \<eta>s0 = n\<close> \<open>length CAs0 = n\<close> n
 
   \<comment> \<open>The properties we need of the FO side premises\<close>
   have CAs0_in_M: "\<forall>CA0 \<in> set CAs0. CA0 \<in> M"
     unfolding CAs0_def using f_p(1) by auto
   have CAs0_to_CAs: "CAs0 \<cdot>\<cdot>cl \<eta>s0 = CAs"
     unfolding CAs0_def \<eta>s0_def using f_p(2)  by (auto simp: n intro: nth_equalityI)
   have SCAs0_to_SMCAs: "(map S CAs0) \<cdot>\<cdot>cl \<eta>s0 = map (S_M S M) CAs"
     unfolding CAs0_def \<eta>s0_def using f_p(3) n by (force intro: nth_equalityI)
   have sub_ground: "\<forall>\<eta>c0 \<in> set \<eta>s0. is_ground_subst \<eta>c0"
     unfolding \<eta>s0_def using f_p n by force
   then have "is_ground_subst_list \<eta>s0"
     using n unfolding is_ground_subst_list_def by auto
 
   \<comment> \<open>Split side premises CAs0 into Cs0 and AAs0\<close>
   obtain AAs0 Cs0 where AAs0_Cs0_p:
    "AAs0 \<cdot>\<cdot>aml \<eta>s0 = AAs" "length Cs0 = n" "Cs0 \<cdot>\<cdot>cl \<eta>s0 = Cs"
    "\<forall>i < n. CAs0 ! i = Cs0 ! i + poss (AAs0 ! i)" "length AAs0 = n"
   proof -
     have "\<forall>i < n. \<exists>AA0. AA0 \<cdot>am \<eta>s0 ! i = AAs ! i \<and> poss AA0 \<subseteq># CAs0 ! i"
     proof (rule, rule)
       fix i
       assume "i < n"
       have "CAs0 ! i \<cdot> \<eta>s0 ! i = CAs ! i"
         using \<open>i < n\<close> \<open>CAs0 \<cdot>\<cdot>cl \<eta>s0 = CAs\<close> n by force
       moreover have "poss (AAs ! i) \<subseteq># CAs !i"
         using \<open>i < n\<close> cas by auto
       ultimately obtain poss_AA0 where
         nn: "poss_AA0 \<cdot> \<eta>s0 ! i = poss (AAs ! i) \<and> poss_AA0 \<subseteq># CAs0 ! i"
         using cas image_mset_of_subset unfolding subst_cls_def by metis
       then have l: "\<forall>L \<in># poss_AA0. is_pos L"
         unfolding subst_cls_def by (metis Melem_subst_cls imageE literal.disc(1)
             literal.map_disc_iff set_image_mset subst_cls_def subst_lit_def)
 
       define AA0 where
         "AA0 = image_mset atm_of poss_AA0"
 
       have na: "poss AA0 = poss_AA0"
         using l unfolding AA0_def by auto
       then have "AA0 \<cdot>am \<eta>s0 ! i = AAs ! i"
         using nn by (metis (mono_tags) literal.inject(1) multiset.inj_map_strong subst_cls_poss)
       moreover have "poss AA0 \<subseteq># CAs0 ! i"
         using na nn by auto
       ultimately show "\<exists>AA0. AA0 \<cdot>am \<eta>s0 ! i = AAs ! i \<and> poss AA0 \<subseteq># CAs0 ! i"
         by blast
     qed
-    then obtain AAs0f where 
+    then obtain AAs0f where
       AAs0f_p: "\<forall>i < n. AAs0f i \<cdot>am \<eta>s0 ! i = AAs ! i \<and> (poss (AAs0f i)) \<subseteq># CAs0 ! i"
       by metis
 
     define AAs0 where "AAs0 = map AAs0f [0 ..<n]"
 
     then have "length AAs0 = n"
       by auto
     note n = n \<open>length AAs0 = n\<close>
 
     from AAs0_def have "\<forall>i < n. AAs0 ! i \<cdot>am \<eta>s0 ! i = AAs ! i"
       using AAs0f_p by auto
     then have AAs0_AAs: "AAs0 \<cdot>\<cdot>aml \<eta>s0 = AAs"
       using n by (auto intro: nth_equalityI)
 
     from AAs0_def have AAs0_in_CAs0: "\<forall>i < n. poss (AAs0 ! i) \<subseteq># CAs0 ! i"
       using AAs0f_p by auto
 
     define Cs0 where
       "Cs0 = map2 (-) CAs0 (map poss AAs0)"
 
     have "length Cs0 = n"
       using Cs0_def n by auto
     note n = n \<open>length Cs0 = n\<close>
 
     have "\<forall>i < n. CAs0 ! i = Cs0 ! i + poss (AAs0 ! i)"
       using AAs0_in_CAs0 Cs0_def n by auto
     then have "Cs0 \<cdot>\<cdot>cl \<eta>s0 = Cs"
       using \<open>CAs0 \<cdot>\<cdot>cl \<eta>s0 = CAs\<close> AAs0_AAs cas n by (auto intro: nth_equalityI)
 
     show ?thesis
-      using that 
+      using that
         \<open>AAs0 \<cdot>\<cdot>aml \<eta>s0 = AAs\<close> \<open>Cs0 \<cdot>\<cdot>cl \<eta>s0 = Cs\<close> \<open>\<forall>i < n. CAs0 ! i = Cs0 ! i + poss (AAs0 ! i)\<close>
         \<open>length AAs0 = n\<close> \<open>length Cs0 = n\<close>
       by blast
   qed
 
   \<comment> \<open>Obtain FO main premise\<close>
   have "\<exists>DA0 \<eta>0. DA0 \<in> M \<and> DA = DA0 \<cdot> \<eta>0 \<and> S DA0 \<cdot> \<eta>0 = S_M S M DA \<and> is_ground_subst \<eta>0"
     using grounding S_M_grounding_of_clss select by (metis le_supE singletonI subsetCE)
-  then obtain DA0 \<eta>0 where 
+  then obtain DA0 \<eta>0 where
     DA0_\<eta>0_p: "DA0 \<in> M \<and> DA = DA0 \<cdot> \<eta>0 \<and> S DA0 \<cdot> \<eta>0 = S_M S M DA \<and> is_ground_subst \<eta>0"
     by auto
   \<comment> \<open>The properties we need of the FO main premise\<close>
   have DA0_in_M: "DA0 \<in> M"
     using DA0_\<eta>0_p by auto
   have DA0_to_DA: "DA0 \<cdot> \<eta>0 = DA"
     using DA0_\<eta>0_p by auto
   have SDA0_to_SMDA: "S DA0 \<cdot> \<eta>0 = S_M S M DA"
     using DA0_\<eta>0_p by auto
   have "is_ground_subst \<eta>0"
     using DA0_\<eta>0_p by auto
 
   \<comment> \<open>Split main premise DA0 into D0 and As0\<close>
   obtain D0 As0 where D0As0_p:
      "As0  \<cdot>al \<eta>0 = As" "length As0 = n" "D0 \<cdot> \<eta>0 = D" "DA0 = D0 + (negs (mset As0))"
     "S_M S M (D + negs (mset As)) \<noteq> {#} \<Longrightarrow> negs (mset As0) = S DA0"
   proof -
     {
       assume a: "S_M S M (D + negs (mset As)) = {#} \<and> length As = (Suc 0)
         \<and> maximal_wrt (As ! 0 \<cdot>a \<sigma>) ((D + negs (mset As)) \<cdot> \<sigma>)"
       then have as: "mset As = {#As ! 0#}"
         by (auto intro: nth_equalityI)
       then have "negs (mset As) = {#Neg (As ! 0)#}"
         by (simp add: \<open>mset As = {#As ! 0#}\<close>)
       then have "DA = D + {#Neg (As ! 0)#}"
         using da by auto
       then obtain L where "L \<in># DA0 \<and> L \<cdot>l \<eta>0 = Neg (As ! 0)"
         using DA0_to_DA by (metis Melem_subst_cls mset_subset_eq_add_right single_subset_iff)
       then have "Neg (atm_of L) \<in># DA0 \<and> Neg (atm_of L) \<cdot>l \<eta>0 = Neg (As ! 0)"
         by (metis Neg_atm_of_iff literal.sel(2) subst_lit_is_pos)
       then have "[atm_of L] \<cdot>al \<eta>0 = As \<and> negs (mset [atm_of L]) \<subseteq># DA0"
         using as subst_lit_def by auto
       then have "\<exists>As0. As0 \<cdot>al \<eta>0 = As \<and> negs (mset As0) \<subseteq># DA0
         \<and> (S_M S M (D + negs (mset As)) \<noteq> {#} \<longrightarrow> negs (mset As0) = S DA0)"
         using a by blast
     }
     moreover
     {
       assume "S_M S M (D + negs (mset As)) = negs (mset As)"
       then have "negs (mset As) = S DA0 \<cdot> \<eta>0"
         using da \<open>S DA0 \<cdot> \<eta>0 = S_M S M DA\<close> by auto
       then have "\<exists>As0. negs (mset As0) = S DA0 \<and> As0 \<cdot>al \<eta>0 = As"
         using instance_list[of As "S DA0" \<eta>0] S.S_selects_neg_lits by auto
       then have "\<exists>As0. As0 \<cdot>al \<eta>0 = As \<and> negs (mset As0) \<subseteq># DA0
         \<and> (S_M S M (D + negs (mset As)) \<noteq> {#} \<longrightarrow> negs (mset As0) = S DA0)"
         using S.S_selects_subseteq by auto
     }
     ultimately have "\<exists>As0. As0 \<cdot>al \<eta>0 = As \<and> (negs (mset As0)) \<subseteq># DA0
       \<and> (S_M S M (D + negs (mset As)) \<noteq> {#} \<longrightarrow> negs (mset As0) = S DA0)"
       using eligible unfolding eligible.simps by auto
     then obtain As0 where
       As0_p: "As0 \<cdot>al \<eta>0 = As \<and> negs (mset As0) \<subseteq># DA0
       \<and> (S_M S M (D + negs (mset As)) \<noteq> {#} \<longrightarrow> negs (mset As0) = S DA0)"
       by blast
     then have "length As0 = n"
       using as_len by auto
     note n = n this
 
     have "As0 \<cdot>al \<eta>0 = As"
       using As0_p by auto
 
     define D0 where
       "D0 = DA0 - negs (mset As0)"
     then have "DA0 = D0 + negs (mset As0)"
       using As0_p by auto
     then have "D0 \<cdot> \<eta>0 = D"
       using DA0_to_DA da As0_p by auto
 
     have "S_M S M (D + negs (mset As)) \<noteq> {#} \<Longrightarrow> negs (mset As0) = S DA0"
       using As0_p by blast
     then show ?thesis
       using that \<open>As0 \<cdot>al \<eta>0 = As\<close> \<open>D0 \<cdot> \<eta>0= D\<close> \<open>DA0 = D0 +  (negs (mset As0))\<close> \<open>length As0 = n\<close>
       by metis
   qed
 
   show ?thesis
     using that[OF n(2,1) DA0_in_M  DA0_to_DA SDA0_to_SMDA CAs0_in_M CAs0_to_CAs SCAs0_to_SMCAs
         \<open>is_ground_subst \<eta>0\<close> \<open>is_ground_subst_list \<eta>s0\<close> \<open>As0  \<cdot>al \<eta>0 = As\<close>
         \<open>AAs0 \<cdot>\<cdot>aml \<eta>s0 = AAs\<close>
         \<open>length As0 = n\<close>
         \<open>D0 \<cdot> \<eta>0 = D\<close>
         \<open>DA0 = D0 + (negs (mset As0))\<close>
         \<open>S_M S M (D + negs (mset As)) \<noteq> {#} \<Longrightarrow> negs (mset As0) = S DA0\<close>
         \<open>length Cs0 = n\<close>
         \<open>Cs0 \<cdot>\<cdot>cl \<eta>s0 = Cs\<close>
         \<open>\<forall>i < n. CAs0 ! i = Cs0 ! i + poss (AAs0 ! i)\<close>
         \<open>length AAs0 = n\<close>]
     by auto
 qed
 
 lemma
   assumes "Pos A \<in># C"
   shows "A \<in> atms_of C"
   using assms
   by (simp add: atm_iff_pos_or_neg_lit)
 
 lemma ord_resolve_rename_lifting:
   assumes
     sel_stable: "\<And>\<rho> C. is_renaming \<rho> \<Longrightarrow> S (C \<cdot> \<rho>) = S C \<cdot> \<rho>" and
     res_e: "ord_resolve (S_M S M) CAs DA AAs As \<sigma> E" and
     select: "selection S" and
     grounding: "{DA} \<union> set CAs \<subseteq> grounding_of_clss M"
   obtains \<eta>s \<eta> \<eta>2 CAs0 DA0 AAs0 As0 E0 \<tau> where
     "is_ground_subst \<eta>"
     "is_ground_subst_list \<eta>s"
     "is_ground_subst \<eta>2"
     "ord_resolve_rename S CAs0 DA0 AAs0 As0 \<tau> E0"
-    (* In the previous proofs we have CAs and DA on lhs of equality... which is better? *)
-    "CAs0 \<cdot>\<cdot>cl \<eta>s = CAs" "DA0 \<cdot> \<eta> = DA" "E0 \<cdot> \<eta>2 = E" 
+    "CAs0 \<cdot>\<cdot>cl \<eta>s = CAs" "DA0 \<cdot> \<eta> = DA" "E0 \<cdot> \<eta>2 = E"
     "{DA0} \<union> set CAs0 \<subseteq> M"
+    "length CAs0 = length CAs"
   using res_e
 proof (cases rule: ord_resolve.cases)
   case (ord_resolve n Cs D)
   note da = this(1) and e = this(2) and cas_len = this(3) and cs_len = this(4) and
     aas_len = this(5) and as_len = this(6) and nz = this(7) and cas = this(8) and
     aas_not_empt = this(9) and mgu = this(10) and eligible = this(11) and str_max = this(12) and
     sel_empt = this(13)
 
   have sel_ren_list_inv:
     "\<And>\<rho>s Cs. length \<rho>s = length Cs \<Longrightarrow> is_renaming_list \<rho>s \<Longrightarrow> map S (Cs \<cdot>\<cdot>cl \<rho>s) = map S Cs \<cdot>\<cdot>cl \<rho>s"
     using sel_stable unfolding is_renaming_list_def by (auto intro: nth_equalityI)
 
   note n = \<open>n \<noteq> 0\<close> \<open>length CAs = n\<close> \<open>length Cs = n\<close> \<open>length AAs = n\<close> \<open>length As = n\<close>
 
   interpret S: selection S by (rule select)
 
   obtain DA0 \<eta>0 CAs0 \<eta>s0 As0 AAs0 D0 Cs0 where as0:
     "length CAs0 = n"
     "length \<eta>s0 = n"
     "DA0 \<in> M"
     "DA0 \<cdot> \<eta>0 = DA"
     "S DA0 \<cdot> \<eta>0 = S_M S M DA"
     "\<forall>CA0 \<in> set CAs0. CA0 \<in> M"
     "CAs0 \<cdot>\<cdot>cl \<eta>s0 = CAs"
     "map S CAs0 \<cdot>\<cdot>cl \<eta>s0 = map (S_M S M) CAs"
     "is_ground_subst \<eta>0"
     "is_ground_subst_list \<eta>s0"
     "As0 \<cdot>al \<eta>0 = As"
     "AAs0 \<cdot>\<cdot>aml \<eta>s0 = AAs"
     "length As0 = n"
     "D0 \<cdot> \<eta>0 = D"
     "DA0 = D0 + (negs (mset As0))"
     "S_M S M (D + negs (mset As)) \<noteq> {#} \<Longrightarrow> negs (mset As0) = S DA0"
     "length Cs0 = n"
     "Cs0 \<cdot>\<cdot>cl \<eta>s0 = Cs"
     "\<forall>i < n. CAs0 ! i = Cs0 ! i + poss (AAs0 ! i)"
     "length AAs0 = n"
     using ord_resolve_obtain_clauses[of S M CAs DA, OF res_e select grounding n(2) \<open>DA = D + negs (mset As)\<close>
       \<open>\<forall>i<n. CAs ! i = Cs ! i + poss (AAs ! i)\<close> \<open>length Cs = n\<close> \<open>length AAs = n\<close>, of thesis] by blast
 
   note n = \<open>length CAs0 = n\<close> \<open>length \<eta>s0 = n\<close> \<open>length As0 = n\<close> \<open>length AAs0 = n\<close> \<open>length Cs0 = n\<close> n
 
   have "length (renamings_apart (DA0 # CAs0)) = Suc n"
     using n renamings_apart_length by auto
 
   note n = this n
 
   define \<rho> where
     "\<rho> = hd (renamings_apart (DA0 # CAs0))"
   define \<rho>s where
     "\<rho>s = tl (renamings_apart (DA0 # CAs0))"
   define DA0' where
     "DA0' = DA0 \<cdot> \<rho>"
   define D0' where
     "D0' = D0 \<cdot> \<rho>"
   define As0' where
     "As0' = As0 \<cdot>al \<rho>"
   define CAs0' where
     "CAs0' = CAs0 \<cdot>\<cdot>cl \<rho>s"
   define Cs0' where
     "Cs0' = Cs0 \<cdot>\<cdot>cl \<rho>s"
   define AAs0' where
     "AAs0' = AAs0 \<cdot>\<cdot>aml \<rho>s"
   define \<eta>0' where
     "\<eta>0' = inv_renaming \<rho> \<odot> \<eta>0"
   define \<eta>s0' where
     "\<eta>s0' = map inv_renaming \<rho>s \<odot>s \<eta>s0"
 
   have renames_DA0: "is_renaming \<rho>"
     using renamings_apart_length renamings_apart_renaming unfolding \<rho>_def
     by (metis length_greater_0_conv list.exhaust_sel list.set_intros(1) list.simps(3))
 
   have renames_CAs0: "is_renaming_list \<rho>s"
     using renamings_apart_length renamings_apart_renaming unfolding \<rho>s_def
     by (metis is_renaming_list_def length_greater_0_conv list.set_sel(2) list.simps(3))
 
   have "length \<rho>s = n"
     unfolding \<rho>s_def using n by auto
   note n = n \<open>length \<rho>s = n\<close>
   have "length As0' = n"
     unfolding As0'_def using n by auto
   have "length CAs0' = n"
     using as0(1) n unfolding CAs0'_def by auto
   have "length Cs0' = n"
     unfolding Cs0'_def using n by auto
   have "length AAs0' = n"
     unfolding AAs0'_def using n by auto
   have "length \<eta>s0' = n"
     using as0(2) n unfolding \<eta>s0'_def by auto
   note n = \<open>length CAs0' = n\<close> \<open>length \<eta>s0' = n\<close> \<open>length As0' = n\<close> \<open>length AAs0' = n\<close> \<open>length Cs0' = n\<close> n
 
   have DA0'_DA: "DA0' \<cdot> \<eta>0' = DA"
     using as0(4) unfolding \<eta>0'_def DA0'_def using renames_DA0 by simp
   have D0'_D: "D0' \<cdot> \<eta>0' = D"
     using as0(14) unfolding \<eta>0'_def D0'_def using renames_DA0 by simp
   have As0'_As: "As0' \<cdot>al \<eta>0' = As"
     using as0(11) unfolding \<eta>0'_def As0'_def using renames_DA0 by auto
   have "S DA0' \<cdot> \<eta>0' = S_M S M DA"
     using as0(5) unfolding \<eta>0'_def DA0'_def using renames_DA0 sel_stable by auto
   have CAs0'_CAs: "CAs0' \<cdot>\<cdot>cl \<eta>s0' = CAs"
     using as0(7) unfolding CAs0'_def \<eta>s0'_def using renames_CAs0 n by auto
   have Cs0'_Cs: "Cs0' \<cdot>\<cdot>cl \<eta>s0' = Cs"
     using as0(18) unfolding Cs0'_def \<eta>s0'_def using renames_CAs0 n by auto
   have AAs0'_AAs: "AAs0' \<cdot>\<cdot>aml \<eta>s0' = AAs"
     using as0(12) unfolding \<eta>s0'_def AAs0'_def using renames_CAs0 using n by auto
   have "map S CAs0' \<cdot>\<cdot>cl \<eta>s0' = map (S_M S M) CAs"
     unfolding CAs0'_def \<eta>s0'_def using as0(8) n renames_CAs0 sel_ren_list_inv by auto
 
   have DA0'_split: "DA0' = D0' + negs (mset As0')"
     using as0(15) DA0'_def D0'_def As0'_def by auto
   then have D0'_subset_DA0': "D0' \<subseteq># DA0'"
     by auto
   from DA0'_split have negs_As0'_subset_DA0': "negs (mset As0') \<subseteq># DA0'"
     by auto
 
   have CAs0'_split: "\<forall>i<n. CAs0' ! i = Cs0' ! i + poss (AAs0' ! i)"
     using as0(19) CAs0'_def Cs0'_def AAs0'_def n by auto
   then have "\<forall>i<n. Cs0' ! i \<subseteq># CAs0' ! i"
     by auto
   from CAs0'_split have poss_AAs0'_subset_CAs0': "\<forall>i<n. poss (AAs0' ! i) \<subseteq># CAs0' ! i"
     by auto
   then have AAs0'_in_atms_of_CAs0': "\<forall>i < n. \<forall>A\<in>#AAs0' ! i. A \<in> atms_of (CAs0' ! i)"
     by (auto simp add: atm_iff_pos_or_neg_lit)
 
   have as0':
     "S_M S M (D + negs (mset As)) \<noteq> {#} \<Longrightarrow> negs (mset As0') = S DA0'"
   proof -
     assume a: "S_M S M (D + negs (mset As)) \<noteq> {#}"
     then have "negs (mset As0) \<cdot> \<rho> = S DA0 \<cdot> \<rho>"
       using as0(16) unfolding \<rho>_def by metis
     then show "negs (mset As0') = S DA0'"
       using  As0'_def DA0'_def using sel_stable[of \<rho> DA0] renames_DA0 by auto
   qed
 
   have vd: "var_disjoint (DA0' # CAs0')"
     unfolding DA0'_def CAs0'_def using renamings_apart_var_disjoint
     unfolding \<rho>_def \<rho>s_def
     by (metis length_greater_0_conv list.exhaust_sel n(6) substitution.subst_cls_lists_Cons
         substitution_axioms zero_less_Suc)
 
   \<comment> \<open>Introduce ground substitution\<close>
   from vd DA0'_DA CAs0'_CAs have "\<exists>\<eta>. \<forall>i < Suc n. \<forall>S. S \<subseteq># (DA0' # CAs0') ! i \<longrightarrow> S \<cdot> (\<eta>0'#\<eta>s0') ! i = S \<cdot> \<eta>"
     unfolding var_disjoint_def using n by auto
   then obtain \<eta> where \<eta>_p: "\<forall>i < Suc n. \<forall>S. S \<subseteq># (DA0' # CAs0') ! i \<longrightarrow> S \<cdot> (\<eta>0'#\<eta>s0') ! i = S \<cdot> \<eta>"
     by auto
   have \<eta>_p_lit: "\<forall>i < Suc n. \<forall>L. L \<in># (DA0' # CAs0') ! i \<longrightarrow> L \<cdot>l (\<eta>0'#\<eta>s0') ! i = L \<cdot>l \<eta>"
   proof (rule, rule, rule, rule)
     fix i :: "nat" and L :: "'a literal"
     assume a:
       "i < Suc n"
       "L \<in># (DA0' # CAs0') ! i"
     then have "\<forall>S. S \<subseteq># (DA0' # CAs0') ! i \<longrightarrow> S \<cdot> (\<eta>0' # \<eta>s0') ! i = S \<cdot> \<eta>"
       using \<eta>_p by auto
     then have "{# L #} \<cdot> (\<eta>0' # \<eta>s0') ! i = {# L #} \<cdot> \<eta>"
       using a by (meson single_subset_iff)
     then show "L \<cdot>l (\<eta>0' # \<eta>s0') ! i = L \<cdot>l \<eta>" by auto
   qed
   have \<eta>_p_atm: "\<forall>i < Suc n. \<forall>A. A \<in> atms_of ((DA0' # CAs0') ! i) \<longrightarrow> A \<cdot>a (\<eta>0'#\<eta>s0') ! i = A \<cdot>a \<eta>"
   proof (rule, rule, rule, rule)
     fix i :: "nat" and A :: "'a"
     assume a:
       "i < Suc n"
       "A \<in> atms_of ((DA0' # CAs0') ! i)"
     then obtain L where L_p: "atm_of L = A \<and> L \<in># (DA0' # CAs0') ! i"
       unfolding atms_of_def by auto
     then have "L \<cdot>l (\<eta>0'#\<eta>s0') ! i = L \<cdot>l \<eta>"
       using \<eta>_p_lit a by auto
     then show "A \<cdot>a (\<eta>0' # \<eta>s0') ! i = A \<cdot>a \<eta>"
       using L_p unfolding subst_lit_def by (cases L) auto
   qed
 
   have DA0'_DA: "DA0' \<cdot> \<eta> = DA"
     using DA0'_DA \<eta>_p by auto
   have "D0' \<cdot> \<eta> = D" using \<eta>_p D0'_D n D0'_subset_DA0' by auto
   have "As0' \<cdot>al \<eta> = As"
   proof (rule nth_equalityI)
     show "length (As0' \<cdot>al \<eta>) = length As"
       using n by auto
   next
-    show "(As0' \<cdot>al \<eta>) ! i = As ! i" if a: "i < length (As0' \<cdot>al \<eta>)" for i
+    fix i
+    show "i<length (As0' \<cdot>al \<eta>) \<Longrightarrow> (As0' \<cdot>al \<eta>) ! i = As ! i"
     proof -
+      assume a: "i < length (As0' \<cdot>al \<eta>)"
       have A_eq: "\<forall>A. A \<in> atms_of DA0' \<longrightarrow> A \<cdot>a \<eta>0' = A \<cdot>a \<eta>"
         using \<eta>_p_atm n by force
       have "As0' ! i \<in> atms_of DA0'"
         using negs_As0'_subset_DA0' unfolding atms_of_def
         using a n by force
       then have "As0' ! i \<cdot>a \<eta>0' = As0' ! i \<cdot>a \<eta>"
          using A_eq by simp
       then show "(As0' \<cdot>al \<eta>) ! i = As ! i"
         using As0'_As \<open>length As0' = n\<close> a by auto
     qed
   qed
 
+  interpret selection
+    by (rule select)
+
   have "S DA0' \<cdot> \<eta> = S_M S M DA"
     using \<open>S DA0' \<cdot> \<eta>0' = S_M S M DA\<close> \<eta>_p S.S_selects_subseteq by auto
 
   from \<eta>_p have \<eta>_p_CAs0': "\<forall>i < n. (CAs0' ! i) \<cdot> (\<eta>s0' ! i) = (CAs0'! i) \<cdot> \<eta>"
     using n by auto
   then have "CAs0' \<cdot>\<cdot>cl \<eta>s0' = CAs0' \<cdot>cl \<eta>"
     using n by (auto intro: nth_equalityI)
   then have CAs0'_\<eta>_fo_CAs: "CAs0' \<cdot>cl \<eta> = CAs"
     using CAs0'_CAs \<eta>_p n by auto
 
   from \<eta>_p have "\<forall>i < n. S (CAs0' ! i) \<cdot> \<eta>s0' ! i = S (CAs0' ! i) \<cdot> \<eta>"
     using S.S_selects_subseteq n by auto
   then have "map S CAs0' \<cdot>\<cdot>cl \<eta>s0' = map S CAs0' \<cdot>cl \<eta>"
     using n by (auto intro: nth_equalityI)
   then have SCAs0'_\<eta>_fo_SMCAs: "map S CAs0' \<cdot>cl \<eta> = map (S_M S M) CAs"
     using \<open>map S CAs0' \<cdot>\<cdot>cl \<eta>s0' = map (S_M S M) CAs\<close> by auto
 
   have "Cs0' \<cdot>cl \<eta> = Cs"
   proof (rule nth_equalityI)
     show "length (Cs0' \<cdot>cl \<eta>) = length Cs"
       using n by auto
   next
-    show "(Cs0' \<cdot>cl \<eta>) ! i = Cs ! i" if "i < length (Cs0' \<cdot>cl \<eta>)" for i
+    fix i
+    show "i<length (Cs0' \<cdot>cl \<eta>) \<Longrightarrow> (Cs0' \<cdot>cl \<eta>) ! i = Cs ! i"
     proof -
-      have a: "i < n"
-        using that n by force
+      assume "i < length (Cs0' \<cdot>cl \<eta>)"
+      then have a: "i < n"
+        using n by force
       have "(Cs0' \<cdot>\<cdot>cl \<eta>s0') ! i = Cs ! i"
         using Cs0'_Cs a n by force
       moreover
       have \<eta>_p_CAs0': "\<forall>S. S \<subseteq># CAs0' ! i \<longrightarrow> S \<cdot> \<eta>s0' ! i = S \<cdot> \<eta>"
         using \<eta>_p a by force
       have "Cs0' ! i \<cdot> \<eta>s0' ! i = (Cs0' \<cdot>cl \<eta>) ! i"
         using \<eta>_p_CAs0' \<open>\<forall>i<n. Cs0' ! i \<subseteq># CAs0' ! i\<close> a n by force
       then have "(Cs0' \<cdot>\<cdot>cl \<eta>s0') ! i = (Cs0' \<cdot>cl \<eta>) ! i "
         using a n by force
       ultimately show "(Cs0' \<cdot>cl \<eta>) ! i = Cs ! i"
         by auto
     qed
   qed
 
   have AAs0'_AAs: "AAs0' \<cdot>aml \<eta> = AAs"
   proof (rule nth_equalityI)
     show "length (AAs0' \<cdot>aml \<eta>) = length AAs"
       using n by auto
   next
-    show "(AAs0' \<cdot>aml \<eta>) ! i = AAs ! i" if a: "i < length (AAs0' \<cdot>aml \<eta>)" for i
+    fix i
+    show "i<length (AAs0' \<cdot>aml \<eta>) \<Longrightarrow> (AAs0' \<cdot>aml \<eta>) ! i = AAs ! i"
     proof -
-      have "i < n"
-        using that n by force
+      assume a: "i < length (AAs0' \<cdot>aml \<eta>)"
+      then have "i < n"
+        using n by force
       then have "\<forall>A. A \<in> atms_of ((DA0' # CAs0') ! Suc i) \<longrightarrow> A \<cdot>a (\<eta>0' # \<eta>s0') ! Suc i = A \<cdot>a \<eta>"
         using \<eta>_p_atm n by force
       then have A_eq: "\<forall>A. A \<in> atms_of (CAs0' ! i) \<longrightarrow> A \<cdot>a \<eta>s0' ! i = A \<cdot>a \<eta>"
         by auto
       have AAs_CAs0': "\<forall>A \<in># AAs0' ! i. A \<in> atms_of (CAs0' ! i)"
         using AAs0'_in_atms_of_CAs0' unfolding atms_of_def
         using a n by force
       then have "AAs0' ! i \<cdot>am  \<eta>s0' ! i = AAs0' ! i \<cdot>am \<eta>"
         unfolding subst_atm_mset_def using A_eq unfolding subst_atm_mset_def by auto
       then show "(AAs0' \<cdot>aml \<eta>) ! i = AAs ! i"
          using AAs0'_AAs \<open>length AAs0' = n\<close> \<open>length \<eta>s0' = n\<close> a by auto
     qed
   qed
 
   \<comment> \<open>Obtain MGU and substitution\<close>
   obtain \<tau> \<phi> where \<tau>\<phi>:
     "Some \<tau> = mgu (set_mset ` set (map2 add_mset As0' AAs0'))"
     "\<tau> \<odot> \<phi> = \<eta> \<odot> \<sigma>"
   proof -
     have uu: "is_unifiers \<sigma> (set_mset ` set (map2 add_mset (As0' \<cdot>al \<eta>) (AAs0' \<cdot>aml \<eta>)))"
       using mgu mgu_sound is_mgu_def unfolding \<open>AAs0' \<cdot>aml \<eta> = AAs\<close> using \<open>As0' \<cdot>al \<eta> = As\<close> by auto
     have \<eta>\<sigma>uni: "is_unifiers (\<eta> \<odot> \<sigma>) (set_mset ` set (map2 add_mset As0' AAs0'))"
     proof -
       have "set_mset ` set (map2 add_mset As0' AAs0' \<cdot>aml \<eta>) =
         set_mset ` set (map2 add_mset As0' AAs0') \<cdot>ass \<eta>"
         unfolding subst_atmss_def subst_atm_mset_list_def using subst_atm_mset_def subst_atms_def
         by (simp add: image_image subst_atm_mset_def subst_atms_def)
       then have "is_unifiers \<sigma> (set_mset ` set (map2 add_mset As0' AAs0') \<cdot>ass \<eta>)"
         using uu by (auto simp: n map2_add_mset_map)
       then show ?thesis
         using is_unifiers_comp by auto
     qed
     then obtain \<tau> where
       \<tau>_p: "Some \<tau> = mgu (set_mset ` set (map2 add_mset As0' AAs0'))"
       using mgu_complete
       by (metis (mono_tags, hide_lams) List.finite_set finite_imageI finite_set_mset image_iff)
     moreover then obtain \<phi> where \<phi>_p: "\<tau> \<odot> \<phi> = \<eta> \<odot> \<sigma>"
       by (metis (mono_tags, hide_lams) finite_set \<eta>\<sigma>uni finite_imageI finite_set_mset image_iff
           mgu_sound set_mset_mset substitution_ops.is_mgu_def) (* should be simpler *)
     ultimately show thesis
       using that by auto
   qed
 
   \<comment> \<open>Lifting eligibility\<close>
   have eligible0': "eligible S \<tau> As0' (D0' + negs (mset As0'))"
   proof -
     have "S_M S M (D + negs (mset As)) = negs (mset As) \<or> S_M S M (D + negs (mset As)) = {#} \<and>
       length As = 1 \<and> maximal_wrt (As ! 0 \<cdot>a \<sigma>) ((D + negs (mset As)) \<cdot> \<sigma>)"
       using eligible unfolding eligible.simps by auto
     then show ?thesis
     proof
       assume "S_M S M (D + negs (mset As)) = negs (mset As)"
       then have "S_M S M (D + negs (mset As)) \<noteq> {#}"
         using n by force
       then have "S (D0' + negs (mset As0')) = negs (mset As0')"
         using as0' DA0'_split by auto
       then show ?thesis
         unfolding eligible.simps[simplified]  by auto
     next
       assume asm: "S_M S M (D + negs (mset As)) = {#} \<and> length As = 1 \<and>
         maximal_wrt (As ! 0 \<cdot>a \<sigma>) ((D + negs (mset As)) \<cdot> \<sigma>)"
       then have "S (D0' + negs (mset As0')) = {#}"
         using \<open>D0' \<cdot> \<eta> = D\<close>[symmetric] \<open>As0' \<cdot>al \<eta> = As\<close>[symmetric] \<open>S (DA0') \<cdot> \<eta> = S_M S M (DA)\<close>
           da DA0'_split subst_cls_empty_iff by metis
       moreover from asm have l: "length As0' = 1"
         using \<open>As0' \<cdot>al \<eta> = As\<close> by auto
       moreover from asm have "maximal_wrt (As0' ! 0 \<cdot>a (\<tau> \<odot> \<phi>)) ((D0' + negs (mset As0')) \<cdot> (\<tau> \<odot> \<phi>))"
         using \<open>As0' \<cdot>al \<eta> = As\<close> \<open>D0' \<cdot> \<eta> = D\<close> using l \<tau>\<phi> by auto
       then have "maximal_wrt (As0' ! 0 \<cdot>a \<tau> \<cdot>a \<phi>) ((D0' + negs (mset As0')) \<cdot> \<tau> \<cdot> \<phi>)"
         by auto
       then have "maximal_wrt (As0' ! 0 \<cdot>a \<tau>) ((D0' + negs (mset As0')) \<cdot> \<tau>)"
         using maximal_wrt_subst by blast
       ultimately show ?thesis
         unfolding eligible.simps[simplified] by auto
     qed
   qed
 
   \<comment> \<open>Lifting maximality\<close>
   have maximality: "\<forall>i < n. strictly_maximal_wrt (As0' ! i \<cdot>a \<tau>) (Cs0' ! i \<cdot> \<tau>)"
     (* Reformulate in list notation? *)
   proof -
     from str_max have "\<forall>i < n. strictly_maximal_wrt ((As0' \<cdot>al \<eta>) ! i \<cdot>a \<sigma>) ((Cs0' \<cdot>cl \<eta>) ! i \<cdot> \<sigma>)"
       using \<open>As0' \<cdot>al \<eta> = As\<close>  \<open>Cs0' \<cdot>cl \<eta> = Cs\<close> by simp
     then have "\<forall>i < n. strictly_maximal_wrt (As0' ! i \<cdot>a (\<tau> \<odot> \<phi>)) (Cs0' ! i \<cdot> (\<tau> \<odot> \<phi>))"
       using n \<tau>\<phi> by simp
     then have "\<forall>i < n. strictly_maximal_wrt (As0' ! i \<cdot>a \<tau> \<cdot>a \<phi>) (Cs0' ! i \<cdot> \<tau> \<cdot> \<phi>)"
       by auto
     then show "\<forall>i < n. strictly_maximal_wrt (As0' ! i \<cdot>a \<tau>) (Cs0' ! i \<cdot> \<tau>)"
       using strictly_maximal_wrt_subst \<tau>\<phi> by blast
   qed
 
   \<comment> \<open>Lifting nothing being selected\<close>
   have nothing_selected: "\<forall>i < n. S (CAs0' ! i) = {#}"
   proof -
     have "\<forall>i < n. (map S CAs0' \<cdot>cl \<eta>) ! i = map (S_M S M) CAs ! i"
       by (simp add: \<open>map S CAs0' \<cdot>cl \<eta> = map (S_M S M) CAs\<close>)
     then have "\<forall>i < n. S (CAs0' ! i) \<cdot> \<eta> = S_M S M (CAs ! i)"
       using n by auto
     then have "\<forall>i < n. S (CAs0' ! i)  \<cdot> \<eta> = {#}"
       using sel_empt \<open>\<forall>i < n.  S (CAs0' ! i) \<cdot> \<eta> = S_M S M (CAs ! i)\<close> by auto
     then show "\<forall>i < n. S (CAs0' ! i) = {#}"
       using subst_cls_empty_iff by blast
   qed
 
   \<comment> \<open>Lifting AAs0's non-emptiness\<close>
   have "\<forall>i < n. AAs0' ! i \<noteq> {#}"
     using n aas_not_empt \<open>AAs0' \<cdot>aml \<eta> = AAs\<close> by auto
 
   \<comment> \<open>Resolve the lifted clauses\<close>
   define E0' where
-    "E0' = (\<Union># (mset Cs0') + D0') \<cdot> \<tau>"
+    "E0' = ((\<Union># (mset Cs0')) + D0') \<cdot> \<tau>"
 
   have res_e0': "ord_resolve S CAs0' DA0' AAs0' As0' \<tau> E0'"
     using ord_resolve.intros[of CAs0' n Cs0' AAs0' As0' \<tau> S D0',
       OF _ _ _ _ _ _ \<open>\<forall>i < n. AAs0' ! i \<noteq> {#}\<close> \<tau>\<phi>(1) eligible0'
         \<open>\<forall>i < n. strictly_maximal_wrt (As0' ! i \<cdot>a \<tau>) (Cs0' ! i \<cdot> \<tau>)\<close> \<open>\<forall>i < n. S (CAs0' ! i) = {#}\<close>]
     unfolding E0'_def using DA0'_split n \<open>\<forall>i<n. CAs0' ! i = Cs0' ! i + poss (AAs0' ! i)\<close> by blast
 
   \<comment> \<open>Prove resolvent instantiates to ground resolvent\<close>
   have e0'\<phi>e: "E0' \<cdot> \<phi> = E"
   proof -
-    have "E0' \<cdot> \<phi> = (\<Union># (mset Cs0') + D0') \<cdot> (\<tau> \<odot> \<phi>)"
+    have "E0' \<cdot> \<phi> = ((\<Union># (mset Cs0')) + D0') \<cdot> (\<tau> \<odot> \<phi>)"
       unfolding E0'_def by auto
     also have "\<dots> = (\<Union># (mset Cs0') + D0') \<cdot> (\<eta> \<odot> \<sigma>)"
       using \<tau>\<phi> by auto
     also have "\<dots> = (\<Union># (mset Cs) + D) \<cdot> \<sigma>"
       using \<open>Cs0' \<cdot>cl \<eta> = Cs\<close> \<open>D0' \<cdot> \<eta> = D\<close> by auto
     also have "\<dots> = E"
       using e by auto
     finally show e0'\<phi>e: "E0' \<cdot> \<phi> = E"
       .
   qed
 
   \<comment> \<open>Replace @{term \<phi>} with a true ground substitution\<close>
   obtain \<eta>2 where
     ground_\<eta>2: "is_ground_subst \<eta>2" "E0' \<cdot> \<eta>2 = E"
   proof -
     have "is_ground_cls_list CAs" "is_ground_cls DA"
       using grounding grounding_ground unfolding is_ground_cls_list_def by auto
     then have "is_ground_cls E"
       using res_e ground_resolvent_subset by (force intro: is_ground_cls_mono)
     then show thesis
       using that e0'\<phi>e make_ground_subst by auto
   qed
 
+  have \<open>length CAs0 = length CAs\<close> using n by simp
 
   \<comment> \<open>Wrap up the proof\<close>
   have "ord_resolve S (CAs0 \<cdot>\<cdot>cl \<rho>s) (DA0 \<cdot> \<rho>) (AAs0 \<cdot>\<cdot>aml \<rho>s) (As0 \<cdot>al \<rho>) \<tau> E0'"
     using res_e0' As0'_def \<rho>_def AAs0'_def \<rho>s_def DA0'_def \<rho>_def CAs0'_def \<rho>s_def by simp
   moreover have "\<forall>i<n. poss (AAs0 ! i) \<subseteq># CAs0 ! i"
     using as0(19) by auto
   moreover have "negs (mset As0) \<subseteq># DA0"
     using local.as0(15) by auto
   ultimately have "ord_resolve_rename S CAs0 DA0 AAs0 As0 \<tau> E0'"
     using ord_resolve_rename[of CAs0 n AAs0 As0 DA0 \<rho> \<rho>s S \<tau> E0'] \<rho>_def \<rho>s_def n by auto
   then show thesis
     using that[of \<eta>0 \<eta>s0 \<eta>2 CAs0 DA0] \<open>is_ground_subst \<eta>0\<close> \<open>is_ground_subst_list \<eta>s0\<close>
       \<open>is_ground_subst \<eta>2\<close> \<open>CAs0 \<cdot>\<cdot>cl \<eta>s0 = CAs\<close> \<open>DA0 \<cdot> \<eta>0 = DA\<close> \<open>E0' \<cdot> \<eta>2 = E\<close> \<open>DA0 \<in> M\<close>
-      \<open>\<forall>CA \<in> set CAs0. CA \<in> M\<close> by blast
+      \<open>\<forall>CA \<in> set CAs0. CA \<in> M\<close> \<open>length CAs0 = length CAs\<close>
+  by blast
 qed
 
 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,1545 +1,1544 @@
 (*  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>
 
-(* FIXME: Used only twice, really -- inline? *)
 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
 
 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"
 
 definition clss_of_state :: "'a state \<Rightarrow> 'a clause set" where
   "clss_of_state St = 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)"
   unfolding clss_of_state_def
   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" and
-    empty_Q0: "Q_of_state (lhd Sts) = {}" 
+    empty_Q0: "Q_of_state (lhd Sts) = {}"
     (* FIXME: make hypothesis empty_Q0 more local---and is it really needed? *)
 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, lifting) mem_Collect_eq substitution_ops.grounding_of_cls_def)
-  ultimately have "set_mset {#D \<cdot> \<sigma>#} \<subseteq> grounding_of_cls D" 
+  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 clss_of_state_def 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 
+  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 
+    using \<mu>_p strict_subset_subsumption_redundant_clss[of D "\<sigma> \<odot> \<mu>" "C \<cdot> \<mu>"] D_in_St
     unfolding clss_of_state_def 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  
+  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 clss_of_state_def 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 clss_of_state_def grounding_of_clss_def by (force intro: sr_ext.derive.intros)
   qed
 qed
 
 (* FIXME: better name *)
 lemma reduction_in_concls_of:
-  assumes 
+  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 
+  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 
+    unfolding grounding_of_clss_def grounding_of_cls_def
     by (rule UN_I[of "D + {#L'#}"], use assms(2) clss_of_state_def 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) 
+    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#}}) 
+  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 clss_of_state_def 
+    using reduction_in_concls_of unfolding grounding_of_clss_def clss_of_state_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}) 
+  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 clss_of_state_def 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})" 
+    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 clss_of_state_def grounding_of_clss_def by auto
   moreover have "grounding_of_state (N, P, Q) - grounding_of_state (N \<union> {C}, P, Q) = {}"
     unfolding clss_of_state_def 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 clss_of_state_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 clss_of_state_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 clss_of_state_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"] unfolding clss_of_state_def 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"] unfolding clss_of_state_def 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"] unfolding clss_of_state_def by force
 next
   case (clause_processing N C P Q)
   then show ?case
     unfolding clss_of_state_def 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 clss_of_state_def grounding_of_clss_def
         unfolding 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 
+        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> 
+      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> 
+      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 
+          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> 
+        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>}))"
           unfolding \<gamma>_ground_def using E_\<mu>_p \<gamma>_p2 \<gamma>_p unfolding infer_from_def
           unfolding clss_of_state_def grounding_of_clss_def
           unfolding 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 apply (auto;fail)
             done
           subgoal
             apply (rule disjI2)
             apply (rule disjI2)
             apply (rule_tac a="CAs ! i" in UN_I)
             subgoal
               apply blast
               done
             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 apply (auto;fail)
               done
             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> 
+        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> 
+      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> 
+      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 clss_of_state_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) 
+  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 clss_of_state_def grounding_of_clss_def by auto
   moreover have "grounding_of_state ({}, P \<union> {C}, Q) - grounding_of_state (N, P, Q \<union> {C}) = {}"
     unfolding clss_of_state_def grounding_of_clss_def by auto
   ultimately show ?case
-    using sr_ext.derive.intros[of "(grounding_of_state (N, P, Q \<union> {C}))" 
+    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) (metis aft sr.Rf_mono[OF Un_upper1] Diff_eq_empty_iff Diff_subset
           Un_Diff true_clss_mono true_clss_union)
     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>
 
 (* FIXME: rename *)
 lemma RP_ground_derive_chain:
   "chain sr_ext.derive (lmap grounding_of_state Sts)"
   using deriv 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 metis
   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 clss_of_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
 
 (* FIXME: come up with a better name *)
 lemma instance_if_subsumed_and_in_limit:
   assumes
     ns: "Gs = lmap grounding_of_state Sts" and
     c: "C \<in> Liminf_llist Gs - sr.Rf (Liminf_llist Gs)" and
     (* FIXME: use clss_of_state below *)
-    d: "D \<in> N_of_state (lnth Sts i) \<union> P_of_state (lnth Sts i) \<union> Q_of_state (lnth Sts i)" 
+    d: "D \<in> N_of_state (lnth Sts i) \<union> P_of_state (lnth Sts i) \<union> Q_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 RP_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 unfolding clss_of_state_def 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 (metis 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
     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 RP_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
   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 clss_of_state_def N_of_state.simps llength_lmap lnth_lmap 
+          by (metis (no_types) UnI1 clss_of_state_def 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 clss_of_state_def 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
     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 RP_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
   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" 
+    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 clss_of_state_def 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'}" 
+    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 clss_of_state_def 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}" 
+    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
     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> 
+  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 RP_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
   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 " 
+    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 clss_of_state_def 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#}}" 
+    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 clss_of_state_def 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}" 
+    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
     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
     (* We could also, we guess, in this proof obtain a D with property D_p(3) from one with only properties D_p(2,3). *)
     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 clss_of_state_def 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 RP_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
   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
     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
     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
     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
     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
     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
     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))"
 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 clss_of_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) D_p(2) D_p(3) 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 add: clss_of_state_def)
   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 clss_of_state_def 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> 
+  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"
   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
   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 clss_of_state_def 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> 
+  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 clss_of_state_def  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 clss_of_state_def grounding_of_clss_def by auto
 qed
 
 theorem RP_sound:
   assumes "{#} \<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 RP_ground_derive_chain by metis
   then show ?thesis
     unfolding lhd_lmap_Sts .
 qed
 
-lemma ground_ord_resolve_ground: 
-  assumes 
+lemma ground_ord_resolve_ground:
+  assumes
     CAs_p: "gr.ord_resolve 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 gr.ord_resolve_atms_of_concl_subset[of CAs DA _ _ E] CAs_p by auto
   {
     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
 
 theorem RP_saturated_if_fair:
   assumes fair: "fair_state_seq 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 RP_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} 
+    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 unfolding clss_of_state_def using fair unfolding fair_state_seq_def
       by (metis (no_types, lifting) Un_empty_left ground_ns_in_ground_limit_st a clss_of_state_def
           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
 
     then have ground_e: "is_ground_cls ?E"
       using ground_ord_resolve_ground CAs_p ground_da by auto
 
     have "\<exists>AAs As \<sigma>. ord_resolve (S_M S (Q_of_state (Liminf_state Sts))) CAs ?DA AAs As \<sigma> ?E"
       using CAs_p[THEN conjunct1]
     proof (cases rule: gr.ord_resolve.cases)
       case (ord_resolve n Cs D)
       note DA = this(1) and e = this(2) and cas_len = this(3) and cs_len = this(4) and
         aas_len = this(5) and as_len = this(6) and nz = this(7) and cas = this(8) and
         aas_not_empt = this(9) and as_aas = this(10) and eligibility = this(11) and
         str_max = this(12) and sel_empt = this(13)
 
       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"
         using ord_resolve 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: "gr.eligible As (D + negs (mset As))"
         using ord_resolve by simp
       have ground_cs: "\<forall>i < n. is_ground_cls (Cs ! i)"
         using ord_resolve(8) ord_resolve(3,4) ground_cas
         using ground_subclauses[of CAs Cs AAs] unfolding is_ground_cls_list_def by auto
       have ground_set_as: "is_ground_atms (set As)"
         using ord_resolve(1) ground_da
         by (metis atms_of_negs is_ground_cls_union set_mset_mset is_ground_cls_is_ground_atms_atms_of)
       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 ord_resolve by simp
 
       from as_len nz have "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
       then have Max\<sigma>_is_Max: "\<forall>\<sigma>. Max (atms_of D \<union> set As) \<cdot>a \<sigma> = Max (atms_of D \<union> set As)"
         by auto
 
       have ann1: "maximal_wrt (Max (atms_of D \<union> set As)) (D + negs (mset As))"
         unfolding maximal_wrt_def
         by clarsimp (metis Max_less_iff UnCI \<open>atms_of D \<union> set As \<noteq> {}\<close>
             \<open>finite (atms_of D \<union> set As)\<close> ground_d ground_set_as infinite_growing is_ground_Max
             is_ground_atms_def is_ground_cls_imp_is_ground_atm less_atm_ground)
 
       from ground_elig have ann2:
         "Max (atms_of D \<union> set As) \<cdot>a \<sigma> = Max (atms_of D \<union> set As)"
         "D \<cdot> \<sigma> + negs (mset As \<cdot>am \<sigma>) = D + negs (mset As)"
         using is_ground_Max ground_mset_as ground_d by auto
 
       from ground_elig have fo_elig:
         "eligible (S_M S (Q_of_state (Liminf_state Sts))) \<sigma> As (D + negs (mset As))"
         unfolding gr.eligible.simps eligible.simps gr.maximal_wrt_def using ann1 ann2
         by (auto simp: S_Q_def)
 
       have l: "\<forall>i < n. gr.strictly_maximal_wrt (As ! i) (Cs ! i)"
         using ord_resolve by simp
       then have "\<forall>i < n. strictly_maximal_wrt (As ! i) (Cs ! i)"
         unfolding gr.strictly_maximal_wrt_def strictly_maximal_wrt_def
         using ground_as[unfolded is_ground_atm_list_def] ground_cs as_len less_atm_ground
         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 m: "\<forall>i < n. S_Q (CAs ! i) = {#}"
         using ord_resolve by simp
 
       have ground_e: "is_ground_cls (\<Union># (mset Cs) + D)"
         using ground_d ground_cs ground_e e by simp
       show ?thesis
         using ord_resolve.intros[OF cas_len cs_len aas_len as_len nz cas aas_not_empt \<sigma>_p fo_elig ll] m DA e ground_e
         unfolding S_Q_def by auto
     qed
     then obtain AAs As \<sigma> where
       \<sigma>_p: "ord_resolve (S_M S (Q_of_state (Liminf_state Sts))) 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 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 unfolding inference_system.inferences_between_def
         apply (rule_tac x = "Infer (mset CAs') DA' E'" in image_eqI)
         subgoal by auto
         subgoal
           using s_p(4)
           unfolding infer_from_def
           apply (rule ord_resolve_rename.cases)
           using s_p(4)
           using C'_p(3) C'_p(5) j_p'(2) apply force
           done
         done
       then show ?thesis
         using C'_p(4) by auto
     qed
     then have "E' \<in> clss_of_state (lnth Sts j)"
       using j_p' unfolding clss_of_state_def 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 metis
     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
     fair: "fair_state_seq 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 RP_ground_derive_chain]
     by (rule unsat[folded lhd_lmap_Sts[of grounding_of_state]])
   moreover have "sr.saturated_upto (Liminf_llist (lmap grounding_of_state Sts))"
     by (rule RP_saturated_if_fair[OF fair, 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
 qed
 
 end
 
 end
 
 end
diff --git a/thys/Ordered_Resolution_Prover/Lazy_List_Chain.thy b/thys/Ordered_Resolution_Prover/Lazy_List_Chain.thy
--- a/thys/Ordered_Resolution_Prover/Lazy_List_Chain.thy
+++ b/thys/Ordered_Resolution_Prover/Lazy_List_Chain.thy
@@ -1,618 +1,618 @@
 (*  Title:       Relational Chains over Lazy Lists
     Author:      Jasmin Blanchette <j.c.blanchette at vu.nl>, 2014, 2017
     Author:      Dmitriy Traytel <traytel at inf.ethz.ch>, 2017
     Author:      Anders Schlichtkrull <andschl at dtu.dk>, 2017
     Maintainer:  Anders Schlichtkrull <andschl at dtu.dk>
 *)
 
 section \<open>Relational Chains over Lazy Lists\<close>
 
 theory Lazy_List_Chain
   imports "HOL-Library.BNF_Corec" Lazy_List_Liminf
 begin
 
 text \<open>
 A chain is a lazy lists of elements such that all pairs of consecutive elements are related by a
 given relation. A full chain is either an infinite chain or a finite chain that cannot be extended.
 The inspiration for this theory is Section 4.1 (``Theorem Proving Processes'') of Bachmair and
 Ganzinger's chapter.
 \<close>
 
 
 subsection \<open>Chains\<close>
 
 coinductive chain :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a llist \<Rightarrow> bool" for R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where
 	chain_singleton: "chain R (LCons x LNil)"
 | chain_cons: "chain R xs \<Longrightarrow> R x (lhd xs) \<Longrightarrow> chain R (LCons x xs)"
 
 lemma
   chain_LNil[simp]: "\<not> chain R LNil" and
   chain_not_lnull: "chain R xs \<Longrightarrow> \<not> lnull xs"
   by (auto elim: chain.cases)
 
 lemma chain_lappend:
   assumes
     r_xs: "chain R xs" and
     r_ys: "chain R ys" and
     mid: "R (llast xs) (lhd ys)"
   shows "chain R (lappend xs ys)"
 proof (cases "lfinite xs")
   case True
   then show ?thesis
     using r_xs mid
   proof (induct rule: lfinite.induct)
     case (lfinite_LConsI xs x)
     note fin = this(1) and ih = this(2) and r_xxs = this(3) and mid = this(4)
     show ?case
     proof (cases "xs = LNil")
       case True
       then show ?thesis
         using r_ys mid by simp (rule chain_cons)
     next
       case xs_nnil: False
       have r_xs: "chain R xs"
         by (metis chain.simps ltl_simps(2) r_xxs xs_nnil)
       have mid': "R (llast xs) (lhd ys)"
         by (metis llast_LCons lnull_def mid xs_nnil)
       have start: "R x (lhd (lappend xs ys))"
         by (metis (no_types) chain.simps lhd_LCons lhd_lappend chain_not_lnull ltl_simps(2) r_xxs
             xs_nnil)
       show ?thesis
         unfolding lappend_code(2) using ih[OF r_xs mid'] start by (rule chain_cons)
     qed
   qed simp
 qed (simp add: r_xs lappend_inf)
 
 lemma chain_length_pos: "chain R xs \<Longrightarrow> llength xs > 0"
   by (cases xs) simp+
 
 lemma chain_ldropn:
   assumes "chain R xs" and "enat n < llength xs"
   shows "chain R (ldropn n xs)"
   using assms
   by (induct n arbitrary: xs, simp,
       metis chain.cases ldrop_eSuc_ltl ldropn_LNil ldropn_eq_LNil ltl_simps(2) not_less)
 
 lemma chain_lnth_rel:
   assumes
     chain: "chain R xs" and
     len: "enat (Suc j) < llength xs"
   shows "R (lnth xs j) (lnth xs (Suc j))"
 proof -
   define ys where "ys = ldropn j xs"
   have "llength ys > 1"
     unfolding ys_def using len
     by (metis One_nat_def funpow_swap1 ldropn_0 ldropn_def ldropn_eq_LNil ldropn_ltl not_less
         one_enat_def)
   obtain y0 y1 ys' where
     ys: "ys = LCons y0 (LCons y1 ys')"
     unfolding ys_def by (metis Suc_ile_eq ldropn_Suc_conv_ldropn len less_imp_not_less not_less)
   have "chain R ys"
     unfolding ys_def using Suc_ile_eq chain chain_ldropn len less_imp_le by blast
   then have "R y0 y1"
     unfolding ys by (auto elim: chain.cases)
   then show ?thesis
     using ys_def unfolding ys by (metis ldropn_Suc_conv_ldropn ldropn_eq_LConsD llist.inject)
 qed
 
 lemma infinite_chain_lnth_rel:
   assumes "\<not> lfinite c" and "chain r c"
   shows "r (lnth c i) (lnth c (Suc i))"
   using assms chain_lnth_rel lfinite_conv_llength_enat by force
 
 lemma lnth_rel_chain:
   assumes
     "\<not> lnull xs" and
     "\<forall>j. enat (j + 1) < llength xs \<longrightarrow> R (lnth xs j) (lnth xs (j + 1))"
   shows "chain R xs"
   using assms
 proof (coinduction arbitrary: xs rule: chain.coinduct)
   case chain
   note nnul = this(1) and nth_chain = this(2)
 
   show ?case
   proof (cases "lnull (ltl xs)")
     case True
     have "xs = LCons (lhd xs) LNil"
       using nnul True by (simp add: llist.expand)
     then show ?thesis
       by blast
   next
     case nnul': False
     moreover have "xs = LCons (lhd xs) (ltl xs)"
       using nnul by simp
     moreover have
       "\<forall>j. enat (j + 1) < llength (ltl xs) \<longrightarrow> R (lnth (ltl xs) j) (lnth (ltl xs) (j + 1))"
       using nnul nth_chain
       by (metis Suc_eq_plus1 ldrop_eSuc_ltl ldropn_Suc_conv_ldropn ldropn_eq_LConsD lnth_ltl)
     moreover have "R (lhd xs) (lhd (ltl xs))"
       using nnul' nnul nth_chain[rule_format, of 0, simplified]
       by (metis ldropn_0 ldropn_Suc_conv_ldropn ldropn_eq_LConsD lhd_LCons_ltl lhd_conv_lnth
           lnth_Suc_LCons ltl_simps(2))
     ultimately show ?thesis
       by blast
   qed
 qed
 
 lemma chain_lmap:
   assumes "\<forall>x y. R x y \<longrightarrow> R' (f x) (f y)" and "chain R xs"
   shows "chain R' (lmap f xs)"
   using assms
 proof (coinduction arbitrary: xs)
   case chain
   then have "(\<exists>y. xs = LCons y LNil) \<or> (\<exists>ys x. xs = LCons x ys \<and> chain R ys \<and> R x (lhd ys))"
     using chain.simps[of R xs] by auto
   then show ?case
   proof
     assume "\<exists>ys x. xs = LCons x ys \<and> chain R ys \<and> R x (lhd ys)"
     then have "\<exists>ys x. lmap f xs = LCons x ys \<and>
       (\<exists>xs. ys = lmap f xs \<and> (\<forall>x y. R x y \<longrightarrow> R' (f x) (f y)) \<and> chain R xs) \<and> R' x (lhd ys)"
       using chain
       by (metis (no_types) lhd_LCons llist.distinct(1) llist.exhaust_sel llist.map_sel(1)
           lmap_eq_LNil chain_not_lnull ltl_lmap ltl_simps(2))
     then show ?thesis
       by auto
   qed auto
 qed
 
 lemma chain_mono:
   assumes "\<forall>x y. R x y \<longrightarrow> R' x y" and "chain R xs"
   shows "chain R' xs"
   using assms by (rule chain_lmap[of _ _ "\<lambda>x. x", unfolded llist.map_ident])
 
 lemma lfinite_chain_imp_rtranclp_lhd_llast: "lfinite xs \<Longrightarrow> chain R xs \<Longrightarrow> R\<^sup>*\<^sup>* (lhd xs) (llast xs)"
 proof (induct rule: lfinite.induct)
   case (lfinite_LConsI xs x)
   note fin_xs = this(1) and ih = this(2) and r_x_xs = this(3)
   show ?case
   proof (cases "xs = LNil")
     case xs_nnil: False
     then have r_xs: "chain R xs"
       using r_x_xs by (blast elim: chain.cases)
     then show ?thesis
       using ih[OF r_xs] xs_nnil r_x_xs
       by (metis chain.cases converse_rtranclp_into_rtranclp lhd_LCons llast_LCons chain_not_lnull
           ltl_simps(2))
   qed simp
 qed simp
 
 lemma tranclp_imp_exists_finite_chain_list:
   "R\<^sup>+\<^sup>+ x y \<Longrightarrow> \<exists>xs. chain R (llist_of (x # xs @ [y]))"
 proof (induct rule: tranclp.induct)
   case (r_into_trancl x y)
   then have "chain R (llist_of (x # [] @ [y]))"
     by (auto intro: chain.intros)
   then show ?case
     by blast
 next
   case (trancl_into_trancl x y z)
   note rstar_xy = this(1) and ih = this(2) and r_yz = this(3)
 
   obtain xs where
     xs: "chain R (llist_of (x # xs @ [y]))"
     using ih by blast
   define ys where
     "ys = xs @ [y]"
 
   have "chain R (llist_of (x # ys @ [z]))"
     unfolding ys_def using r_yz chain_lappend[OF xs chain_singleton, of z]
     by (auto simp: lappend_llist_of_LCons llast_LCons)
   then show ?case
     by blast
 qed
 
 inductive_cases chain_consE: "chain R (LCons x xs)"
 inductive_cases chain_nontrivE: "chain R (LCons x (LCons y xs))"
 
 primrec prepend where
   "prepend [] ys = ys"
 | "prepend (x # xs) ys = LCons x (prepend xs ys)"
 
 lemma lnull_prepend[simp]: "lnull (prepend xs ys) = (xs = [] \<and> lnull ys)"
   by (induct xs) auto
 
 lemma lhd_prepend[simp]: "lhd (prepend xs ys) = (if xs \<noteq> [] then hd xs else lhd ys)"
   by (induct xs) auto
 
 lemma prepend_LNil[simp]: "prepend xs LNil = llist_of xs"
   by (induct xs) auto
 
 lemma lfinite_prepend[simp]: "lfinite (prepend xs ys) \<longleftrightarrow> lfinite ys"
   by (induct xs) auto
 
 lemma llength_prepend[simp]: "llength (prepend xs ys) = length xs + llength ys"
   by (induct xs) (auto simp: enat_0 iadd_Suc eSuc_enat[symmetric])
 
 lemma llast_prepend[simp]: "\<not> lnull ys \<Longrightarrow> llast (prepend xs ys) = llast ys"
   by (induct xs) (auto simp: llast_LCons)
 
 lemma prepend_prepend: "prepend xs (prepend ys zs) = prepend (xs @ ys) zs"
   by (induct xs) auto
 
 lemma chain_prepend:
   "chain R (llist_of zs) \<Longrightarrow> last zs = lhd xs \<Longrightarrow> chain R xs \<Longrightarrow> chain R (prepend zs (ltl xs))"
   by (induct zs; cases xs)
     (auto split: if_splits simp: lnull_def[symmetric] intro!: chain_cons elim!: chain_consE)
 
 lemma lmap_prepend[simp]: "lmap f (prepend xs ys) = prepend (map f xs) (lmap f ys)"
   by (induct xs) auto
 
 lemma lset_prepend[simp]: "lset (prepend xs ys) = set xs \<union> lset ys"
   by (induct xs) auto
 
 lemma prepend_LCons: "prepend xs (LCons y ys) = prepend (xs @ [y]) ys"
   by (induct xs) auto
 
 lemma lnth_prepend:
   "lnth (prepend xs ys) i = (if i < length xs then nth xs i else lnth ys (i - length xs))"
   by (induct xs arbitrary: i) (auto simp: lnth_LCons' nth_Cons')
 
 theorem lfinite_less_induct[consumes 1, case_names less]:
   assumes fin: "lfinite xs"
     and step: "\<And>xs. lfinite xs \<Longrightarrow> (\<And>zs. llength zs < llength xs \<Longrightarrow> P zs) \<Longrightarrow> P xs"
   shows "P xs"
 using fin proof (induct "the_enat (llength xs)" arbitrary: xs rule: less_induct)
   case (less xs)
   show ?case
     using less(2) by (intro step[OF less(2)] less(1))
       (auto dest!: lfinite_llength_enat simp: eSuc_enat elim!: less_enatE llength_eq_enat_lfiniteD)
 qed
 
 theorem lfinite_prepend_induct[consumes 1, case_names LNil prepend]:
   assumes "lfinite xs"
     and LNil: "P LNil"
     and prepend: "\<And>xs. lfinite xs \<Longrightarrow> (\<And>zs. (\<exists>ys. xs = prepend ys zs \<and> ys \<noteq> []) \<Longrightarrow> P zs) \<Longrightarrow> P xs"
   shows "P xs"
 using assms(1) proof (induct xs rule: lfinite_less_induct)
   case (less xs)
   from less(1) show ?case
     by (cases xs)
       (force simp: LNil neq_Nil_conv dest: lfinite_llength_enat intro!: prepend[of "LCons _ _"] intro: less)+
 qed
 
 coinductive emb :: "'a llist \<Rightarrow> 'a llist \<Rightarrow> bool" where
   "lfinite xs \<Longrightarrow> emb LNil xs"
 | "emb xs ys \<Longrightarrow> emb (LCons x xs) (prepend zs (LCons x ys))"
 
 inductive_cases emb_LConsE: "emb (LCons z zs) ys"
 inductive_cases emb_LNil1E: "emb LNil ys"
 inductive_cases emb_LNil2E: "emb xs LNil"
 
 lemma emb_lfinite:
   assumes "emb xs ys"
   shows "lfinite ys \<longleftrightarrow> lfinite xs"
 proof
   assume "lfinite xs"
   then show "lfinite ys" using assms
     by (induct xs arbitrary: ys rule: lfinite_induct)
       (auto simp: lnull_def neq_LNil_conv elim!: emb_LNil1E emb_LConsE)
 next
   assume "lfinite ys"
   then show "lfinite xs" using assms
   proof (induction ys arbitrary: xs rule: lfinite_less_induct)
     case (less ys)
     from less.prems \<open>lfinite ys\<close> show ?case
       by (cases xs)
         (auto simp: eSuc_enat elim!: emb_LNil1E emb_LConsE less.IH[rotated] dest!: lfinite_llength_enat)
   qed
 qed
 
 inductive prepend_cong1 for X where
   prepend_cong1_base: "X xs \<Longrightarrow> prepend_cong1 X xs"
 | prepend_cong1_prepend: "prepend_cong1 X ys \<Longrightarrow> prepend_cong1 X (prepend xs ys)"
 
 lemma emb_prepend_coinduct[rotated, case_names emb]:
   assumes "(\<And>x1 x2. X x1 x2 \<Longrightarrow>
     (\<exists>xs. x1 = LNil \<and> x2 = xs \<and> lfinite xs)
      \<or> (\<exists>xs ys x zs. x1 = LCons x xs \<and> x2 = prepend zs (LCons x ys)
        \<and> (prepend_cong1 (X xs) ys \<or> emb xs ys)))" (is "\<And>x1 x2. X x1 x2 \<Longrightarrow> ?bisim x1 x2")
   shows "X x1 x2 \<Longrightarrow> emb x1 x2"
 proof (erule emb.coinduct[OF prepend_cong1_base])
   fix xs zs
   assume "prepend_cong1 (X xs) zs"
   then show "?bisim xs zs"
     by (induct zs rule: prepend_cong1.induct) (erule assms, force simp: prepend_prepend)
 qed
 
 context
 begin
 
 private coinductive chain' for R where
   "chain' R (LCons x LNil)"
 | "chain R (llist_of (x # zs @ [lhd xs])) \<Longrightarrow>
    chain' R xs \<Longrightarrow> chain' R (LCons x (prepend zs xs))"
 
 private lemma chain_imp_chain': "chain R xs \<Longrightarrow> chain' R xs"
 proof (coinduction arbitrary: xs rule: chain'.coinduct)
   case chain'
   then show ?case
   proof (cases rule: chain.cases)
     case (chain_cons zs z)
     then show ?thesis
       by (intro disjI2 exI[of _ z] exI[of _ "[]"] exI[of _ "zs"])
         (auto intro: chain.intros)
   qed simp
 qed
 
 private lemma chain'_imp_chain: "chain' R xs \<Longrightarrow> chain R xs"
 proof (coinduction arbitrary: xs rule: chain.coinduct)
   case chain
   then show ?case
   proof (cases rule: chain'.cases)
     case (2 y zs ys)
     then show ?thesis
       by (intro disjI2 exI[of _ "prepend zs ys"] exI[of _ y])
         (force dest!: neq_Nil_conv[THEN iffD1] elim: chain.cases chain_nontrivE
           intro: chain'.intros)
   qed simp
 qed
 
 private lemma chain_chain': "chain = chain'"
   unfolding fun_eq_iff by (metis chain_imp_chain' chain'_imp_chain)
 
 lemma chain_prepend_coinduct[case_names chain]:
   "X x \<Longrightarrow> (\<And>x. X x \<Longrightarrow>
     (\<exists>z. x = LCons z LNil) \<or>
     (\<exists>y xs zs. x = LCons y (prepend zs xs) \<and>
       (X xs \<or> chain R xs) \<and> chain R (llist_of (y # zs @ [lhd xs])))) \<Longrightarrow> chain R x"
   by (subst chain_chain', erule chain'.coinduct) (force simp: chain_chain')
 
 end
 
 context
   fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
 begin
 
 private definition pick where
   "pick x y = (SOME xs. chain R (llist_of (x # xs @ [y])))"
 
 private lemma pick[simp]:
   assumes "R\<^sup>+\<^sup>+ x y"
   shows "chain R (llist_of (x # pick x y @ [y]))"
   unfolding pick_def using tranclp_imp_exists_finite_chain_list[THEN someI_ex, OF assms] by auto
 
 private friend_of_corec prepend where
-  "prepend xs ys = (case xs of [] \<Rightarrow> 
+  "prepend xs ys = (case xs of [] \<Rightarrow>
     (case ys of LNil \<Rightarrow> LNil | LCons x xs \<Rightarrow> LCons x xs) | x # xs' \<Rightarrow> LCons x (prepend xs' ys))"
   by (simp split: list.splits llist.splits) transfer_prover
 
 private corec wit where
   "wit xs = (case xs of LCons x (LCons y xs) \<Rightarrow>
      LCons x (prepend (pick x y) (wit (LCons y xs))) | _ \<Rightarrow> xs)"
 
 private lemma
   wit_LNil[simp]: "wit LNil = LNil" and
   wit_lsingleton[simp]: "wit (LCons x LNil) = LCons x LNil" and
   wit_LCons2: "wit (LCons x (LCons y xs)) =
      (LCons x (prepend (pick x y) (wit (LCons y xs))))"
   by (subst wit.code; auto)+
 
 private lemma lnull_wit[simp]: "lnull (wit xs) \<longleftrightarrow> lnull xs"
   by (subst wit.code) (auto split: llist.splits simp: Let_def)
 
 private lemma lhd_wit[simp]: "chain R\<^sup>+\<^sup>+ xs \<Longrightarrow> lhd (wit xs) = lhd xs"
   by (erule chain.cases; subst wit.code) (auto split: llist.splits simp: Let_def)
 
 private lemma LNil_eq_iff_lnull: "LNil = xs \<longleftrightarrow> lnull xs"
   by (cases xs) auto
 
 lemma emb_wit[simp]: "chain R\<^sup>+\<^sup>+ xs \<Longrightarrow> emb xs (wit xs)"
 proof (coinduction arbitrary: xs rule: emb_prepend_coinduct)
   case (emb xs)
   then show ?case
   proof (cases rule: chain.cases)
     case (chain_cons zs z)
     then show ?thesis
       by (subst (2) wit.code)
         (auto split: llist.splits intro!: exI[of _ "[]"] exI[of _ "_ :: _ llist"]
           prepend_cong1_prepend[OF prepend_cong1_base])
   qed (auto intro!: exI[of _ LNil] exI[of _ "[]"] emb.intros)
 qed
 
 private lemma lfinite_wit[simp]:
   assumes "chain R\<^sup>+\<^sup>+ xs"
   shows "lfinite (wit xs) \<longleftrightarrow> lfinite xs"
   using emb_wit emb_lfinite assms by blast
 
 private lemma llast_wit[simp]:
   assumes "chain R\<^sup>+\<^sup>+ xs"
   shows "llast (wit xs) = llast xs"
 proof (cases "lfinite xs")
   case True
   from this assms show ?thesis
   proof (induct rule: lfinite.induct)
     case (lfinite_LConsI xs x)
     then show ?case
       by (cases xs) (auto simp: wit_LCons2 llast_LCons elim: chain_nontrivE)
   qed auto
 qed (auto simp: llast_linfinite assms)
 
 lemma chain_tranclp_imp_exists_chain:
   "chain R\<^sup>+\<^sup>+ xs \<Longrightarrow>
    \<exists>ys. chain R ys \<and> emb xs ys \<and> lhd ys = lhd xs \<and> llast ys = llast xs"
 proof (intro exI[of _ "wit xs"] conjI, coinduction arbitrary: xs rule: chain_prepend_coinduct)
   case chain
   then show ?case
     by (subst (1 2) wit.code) (erule chain.cases; force split: llist.splits dest: pick)
 qed auto
 
 lemma emb_lset_mono[rotated]: "x \<in> lset xs \<Longrightarrow> emb xs ys \<Longrightarrow> x \<in> lset ys"
   by (induct x xs arbitrary: ys rule: llist.set_induct) (auto elim!: emb_LConsE)
 
 lemma emb_Ball_lset_antimono:
   assumes "emb Xs Ys"
   shows "\<forall>Y \<in> lset Ys. x \<in> Y \<Longrightarrow> \<forall>X \<in> lset Xs. x \<in> X"
   using emb_lset_mono[OF assms] by blast
 
 lemma emb_lfinite_antimono[rotated]: "lfinite ys \<Longrightarrow> emb xs ys \<Longrightarrow> lfinite xs"
   by (induct ys arbitrary: xs rule: lfinite_prepend_induct)
     (force elim!: emb_LNil2E simp: LNil_eq_iff_lnull prepend_LCons elim: emb.cases)+
 
 lemma emb_Liminf_llist_mono_aux:
   assumes "emb Xs Ys" and "\<not> lfinite Xs" and "\<not> lfinite Ys" and "\<forall>j\<ge>i. x \<in> lnth Ys j"
   shows "\<forall>j\<ge>i. x \<in> lnth Xs j"
 using assms proof (induct i arbitrary: Xs Ys rule: less_induct)
   case (less i)
   then show ?case
   proof (cases i)
     case 0
     then show ?thesis
       using emb_Ball_lset_antimono[OF less(2), of x] less(5)
       unfolding Ball_def in_lset_conv_lnth simp_thms
         not_lfinite_llength[OF less(3)] not_lfinite_llength[OF less(4)] enat_ord_code subset_eq
       by blast
   next
     case [simp]: (Suc nat)
     from less(2,3) obtain xs as b bs where
       [simp]: "Xs = LCons b xs" "Ys = prepend as (LCons b bs)" and "emb xs bs"
       by (auto elim: emb.cases)
     have IH: "\<forall>k\<ge>j. x \<in> lnth xs k" if "\<forall>k\<ge>j. x \<in> lnth bs k" "j < i" for j
       using that less(1)[OF _ \<open>emb xs bs\<close>] less(3,4) by auto
     from less(5) have "\<forall>k\<ge>i - length as - 1. x \<in> lnth xs k"
       by (intro IH allI)
         (drule spec[of _ "_ + length as + 1"], auto simp: lnth_prepend lnth_LCons')
     then show ?thesis
       by (auto simp: lnth_LCons')
   qed
 qed
 
 lemma emb_Liminf_llist_infinite:
   assumes "emb Xs Ys" and "\<not> lfinite Xs"
   shows "Liminf_llist Ys \<subseteq> Liminf_llist Xs"
 proof -
   from assms have "\<not> lfinite Ys"
     using emb_lfinite_antimono by blast
   with assms show ?thesis
     unfolding Liminf_llist_def by (auto simp: not_lfinite_llength dest: emb_Liminf_llist_mono_aux)
 qed
 
 lemma emb_lmap: "emb xs ys \<Longrightarrow> emb (lmap f xs) (lmap f ys)"
 proof (coinduction arbitrary: xs ys rule: emb.coinduct)
   case emb
   show ?case
   proof (cases xs)
     case xs: (LCons x xs')
 
     obtain ysa0 and zs0 where
       ys: "ys = prepend zs0 (LCons x ysa0)" and
       emb': "emb xs' ysa0"
       using emb_LConsE[OF emb[unfolded xs]] by metis
 
     let ?xa = "f x"
     let ?xsa = "lmap f xs'"
     let ?zs = "map f zs0"
     let ?ysa = "lmap f ysa0"
 
     have "lmap f xs = LCons ?xa ?xsa"
       unfolding xs by simp
     moreover have "lmap f ys = prepend ?zs (LCons ?xa ?ysa)"
       unfolding ys by simp
     moreover have "\<exists>xsa ysa. ?xsa = lmap f xsa \<and> ?ysa = lmap f ysa \<and> emb xsa ysa"
       using emb' by blast
     ultimately show ?thesis
       by blast
   qed (simp add: emb_lfinite[OF emb])
 qed
 
 end
 
 lemma chain_inf_llist_if_infinite_chain_function:
   assumes "\<forall>i. r (f (Suc i)) (f i)"
   shows "\<not> lfinite (inf_llist f) \<and> chain r\<inverse>\<inverse> (inf_llist f)"
   using assms by (simp add: lnth_rel_chain)
 
 lemma infinite_chain_function_iff_infinite_chain_llist:
   "(\<exists>f. \<forall>i. r (f (Suc i)) (f i)) \<longleftrightarrow> (\<exists>c. \<not> lfinite c \<and> chain r\<inverse>\<inverse> c)"
   using chain_inf_llist_if_infinite_chain_function infinite_chain_lnth_rel by blast
 
 lemma wfP_iff_no_infinite_down_chain_llist: "wfP r \<longleftrightarrow> (\<nexists>c. \<not> lfinite c \<and> chain r\<inverse>\<inverse> c)"
 proof -
   have "wfP r \<longleftrightarrow>  wf {(x, y). r x y}"
     unfolding wfP_def by auto
   also have "\<dots> \<longleftrightarrow> (\<nexists>f. \<forall>i. (f (Suc i), f i) \<in> {(x, y). r x y})"
     using wf_iff_no_infinite_down_chain by blast
   also have "\<dots> \<longleftrightarrow> (\<nexists>f. \<forall>i. r (f (Suc i)) (f i))"
     by auto
   also have "\<dots> \<longleftrightarrow> (\<nexists>c. \<not>lfinite c \<and> chain r\<inverse>\<inverse> c)"
     using infinite_chain_function_iff_infinite_chain_llist by blast
   finally show ?thesis
     by auto
 qed
 
 
 subsection \<open>Full Chains\<close>
 
 coinductive full_chain :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a llist \<Rightarrow> bool" for R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where
 	full_chain_singleton: "(\<forall>y. \<not> R x y) \<Longrightarrow> full_chain R (LCons x LNil)"
 | full_chain_cons: "full_chain R xs \<Longrightarrow> R x (lhd xs) \<Longrightarrow> full_chain R (LCons x xs)"
 
 lemma
   full_chain_LNil[simp]: "\<not> full_chain R LNil" and
   full_chain_not_lnull: "full_chain R xs \<Longrightarrow> \<not> lnull xs"
   by (auto elim: full_chain.cases)
 
 lemma full_chain_ldropn:
   assumes full: "full_chain R xs" and "enat n < llength xs"
   shows "full_chain R (ldropn n xs)"
   using assms
   by (induct n arbitrary: xs, simp,
       metis full_chain.cases ldrop_eSuc_ltl ldropn_LNil ldropn_eq_LNil ltl_simps(2) not_less)
 
 lemma full_chain_iff_chain:
   "full_chain R xs \<longleftrightarrow> chain R xs \<and> (lfinite xs \<longrightarrow> (\<forall>y. \<not> R (llast xs) y))"
 proof (intro iffI conjI impI allI; (elim conjE)?)
   assume full: "full_chain R xs"
 
   show chain: "chain R xs"
     using full by (coinduction arbitrary: xs) (auto elim: full_chain.cases)
 
   {
     fix y
     assume "lfinite xs"
     then obtain n where
       suc_n: "Suc n = llength xs"
       by (metis chain chain_length_pos lessE less_enatE lfinite_conv_llength_enat)
 
     have "full_chain R (ldropn n xs)"
       by (rule full_chain_ldropn[OF full]) (use suc_n Suc_ile_eq in force)
     moreover have "ldropn n xs = LCons (llast xs) LNil"
       using suc_n by (metis enat_le_plus_same(2) enat_ord_simps(2) gen_llength_def
           ldropn_Suc_conv_ldropn ldropn_all lessI llast_ldropn llast_singleton llength_code)
     ultimately show "\<not> R (llast xs) y"
       by (auto elim: full_chain.cases)
   }
 next
   assume
     "chain R xs" and
     "lfinite xs \<longrightarrow> (\<forall>y. \<not> R (llast xs) y)"
   then show "full_chain R xs"
     by (coinduction arbitrary: xs) (erule chain.cases, simp, metis lfinite_LConsI llast_LCons)
 qed
 
 lemma full_chain_imp_chain: "full_chain R xs \<Longrightarrow> chain R xs"
   using full_chain_iff_chain by blast
 
 lemma full_chain_length_pos: "full_chain R xs \<Longrightarrow> llength xs > 0"
   by (fact chain_length_pos[OF full_chain_imp_chain])
 
 lemma full_chain_lnth_rel:
   "full_chain R xs \<Longrightarrow> enat (Suc j) < llength xs \<Longrightarrow> R (lnth xs j) (lnth xs (Suc j))"
   by (fact chain_lnth_rel[OF full_chain_imp_chain])
 
 inductive_cases full_chain_consE: "full_chain R (LCons x xs)"
 inductive_cases full_chain_nontrivE: "full_chain R (LCons x (LCons y xs))"
 
 lemma full_chain_tranclp_imp_exists_full_chain:
   assumes full: "full_chain R\<^sup>+\<^sup>+ xs"
   shows "\<exists>ys. full_chain R ys \<and> emb xs ys \<and> lhd ys = lhd xs \<and> llast ys = llast xs"
 proof -
   obtain ys where ys:
     "chain R ys" "emb xs ys" "lhd ys = lhd xs" "llast ys = llast xs"
     using full_chain_imp_chain[OF full] chain_tranclp_imp_exists_chain by blast
   have "full_chain R ys"
     using ys(1,4) emb_lfinite[OF ys(2)] full unfolding full_chain_iff_chain by auto
   then show ?thesis
     using ys(2-4) by auto
 qed
 
 end
diff --git a/thys/Ordered_Resolution_Prover/Standard_Redundancy.thy b/thys/Ordered_Resolution_Prover/Standard_Redundancy.thy
--- a/thys/Ordered_Resolution_Prover/Standard_Redundancy.thy
+++ b/thys/Ordered_Resolution_Prover/Standard_Redundancy.thy
@@ -1,339 +1,339 @@
 (*  Title:       The Standard Redundancy Criterion
     Author:      Jasmin Blanchette <j.c.blanchette at vu.nl>, 2014, 2017
     Author:      Dmitriy Traytel <traytel at inf.ethz.ch>, 2014
     Author:      Anders Schlichtkrull <andschl at dtu.dk>, 2017
     Maintainer:  Anders Schlichtkrull <andschl at dtu.dk>
 *)
 
 section \<open>The Standard Redundancy Criterion\<close>
 
 theory Standard_Redundancy
   imports Proving_Process
 begin
 
 text \<open>
 This material is based on Section 4.2.2 (``The Standard Redundancy Criterion'') of Bachmair and
 Ganzinger's chapter.
 \<close>
 
 locale standard_redundancy_criterion =
   inference_system \<Gamma> for \<Gamma> :: "('a :: wellorder) inference set"
 begin
 
 definition redundant_infer :: "'a clause set \<Rightarrow> 'a inference \<Rightarrow> bool" where
   "redundant_infer N \<gamma> \<equiv>
    \<exists>DD. set_mset DD \<subseteq> N \<and> (\<forall>I. I \<Turnstile>m DD + side_prems_of \<gamma> \<longrightarrow> I \<Turnstile> concl_of \<gamma>)
       \<and> (\<forall>D. D \<in># DD \<longrightarrow> D < main_prem_of \<gamma>)"
 
 definition Rf :: "'a clause set \<Rightarrow> 'a clause set" where
   "Rf N = {C. \<exists>DD. set_mset DD \<subseteq> N \<and> (\<forall>I. I \<Turnstile>m DD \<longrightarrow> I \<Turnstile> C) \<and> (\<forall>D. D \<in># DD \<longrightarrow> D < C)}"
 
 definition Ri :: "'a clause set \<Rightarrow> 'a inference set" where
   "Ri N = {\<gamma> \<in> \<Gamma>. redundant_infer N \<gamma>}"
 
 lemma tautology_Rf:
   assumes "Pos A \<in># C"
   assumes "Neg A \<in># C"
   shows "C \<in> Rf N"
 proof -
   have "set_mset {#} \<subseteq> N \<and> (\<forall>I. I \<Turnstile>m {#} \<longrightarrow> I \<Turnstile> C) \<and> (\<forall>D. D \<in># {#} \<longrightarrow> D < C)"
     using assms by auto
   then show "C \<in> Rf N"
     unfolding Rf_def by blast
 qed
 
 lemma tautology_redundant_infer:
   assumes
     pos: "Pos A \<in># concl_of \<iota>" and
     neg: "Neg A \<in># concl_of \<iota>"
   shows "redundant_infer N \<iota>"
   by (metis empty_iff empty_subsetI neg pos pos_neg_in_imp_true redundant_infer_def set_mset_empty)
 
 lemma contradiction_Rf: "{#} \<in> N \<Longrightarrow> Rf N = UNIV - {{#}}"
   unfolding Rf_def by force
 
 text \<open>
 The following results correspond to Lemma 4.5. The lemma \<open>wlog_non_Rf\<close> generalizes the core of
 the argument.
 \<close>
 
 lemma Rf_mono: "N \<subseteq> N' \<Longrightarrow> Rf N \<subseteq> Rf N'"
   unfolding Rf_def by auto
 
 lemma wlog_non_Rf:
   assumes ex: "\<exists>DD. set_mset DD \<subseteq> N \<and> (\<forall>I. I \<Turnstile>m DD + CC \<longrightarrow> I \<Turnstile> E) \<and> (\<forall>D'. D' \<in># DD \<longrightarrow> D' < D)"
   shows "\<exists>DD. set_mset DD \<subseteq> N - Rf N \<and> (\<forall>I. I \<Turnstile>m DD + CC \<longrightarrow> I \<Turnstile> E) \<and> (\<forall>D'. D' \<in># DD \<longrightarrow> D' < D)"
 proof -
   from ex obtain DD0 where
     dd0: "DD0 \<in> {DD. set_mset DD \<subseteq> N \<and> (\<forall>I. I \<Turnstile>m DD + CC \<longrightarrow> I \<Turnstile> E) \<and> (\<forall>D'. D' \<in># DD \<longrightarrow> D' < D)}"
     by blast
   have "\<exists>DD. set_mset DD \<subseteq> N \<and> (\<forall>I. I \<Turnstile>m DD + CC \<longrightarrow> I \<Turnstile> E) \<and> (\<forall>D'. D' \<in># DD \<longrightarrow> D' < D) \<and>
       (\<forall>DD'. set_mset DD' \<subseteq> N \<and> (\<forall>I. I \<Turnstile>m DD' + CC \<longrightarrow> I \<Turnstile> E) \<and> (\<forall>D'. D' \<in># DD' \<longrightarrow> D' < D) \<longrightarrow>
     DD \<le> DD')"
     using wf_eq_minimal[THEN iffD1, rule_format, OF wf_less_multiset dd0]
     unfolding not_le[symmetric] by blast
   then obtain DD where
     dd_subs_n: "set_mset DD \<subseteq> N" and
     ddcc_imp_e: "\<forall>I. I \<Turnstile>m DD + CC \<longrightarrow> I \<Turnstile> E" and
     dd_lt_d: "\<forall>D'. D' \<in># DD \<longrightarrow> D' < D" and
     d_min: "\<forall>DD'. set_mset DD' \<subseteq> N \<and> (\<forall>I. I \<Turnstile>m DD' + CC \<longrightarrow> I \<Turnstile> E) \<and> (\<forall>D'. D' \<in># DD' \<longrightarrow> D' < D) \<longrightarrow>
       DD \<le> DD'"
     by blast
 
   have "\<forall>Da. Da \<in># DD \<longrightarrow> Da \<notin> Rf N"
   proof clarify
     fix Da
     assume
       da_in_dd: "Da \<in># DD" and
       da_rf: "Da \<in> Rf N"
 
     from da_rf obtain DD' where
       dd'_subs_n: "set_mset DD' \<subseteq> N" and
       dd'_imp_da: "\<forall>I. I \<Turnstile>m DD' \<longrightarrow> I \<Turnstile> Da" and
       dd'_lt_da: "\<forall>D'. D' \<in># DD' \<longrightarrow> D' < Da"
       unfolding Rf_def by blast
 
     define DDa where
       "DDa = DD - {#Da#} + DD'"
 
     have "set_mset DDa \<subseteq> N"
       unfolding DDa_def using dd_subs_n dd'_subs_n
       by (meson contra_subsetD in_diffD subsetI union_iff)
     moreover have "\<forall>I. I \<Turnstile>m DDa + CC \<longrightarrow> I \<Turnstile> E"
       using dd'_imp_da ddcc_imp_e da_in_dd unfolding DDa_def true_cls_mset_def
       by (metis in_remove1_mset_neq union_iff)
     moreover have "\<forall>D'. D' \<in># DDa \<longrightarrow> D' < D"
       using dd_lt_d dd'_lt_da da_in_dd unfolding DDa_def
       by (metis insert_DiffM2 order.strict_trans union_iff)
     moreover have "DDa < DD"
       unfolding DDa_def
       by (meson da_in_dd dd'_lt_da mset_lt_single_right_iff single_subset_iff union_le_diff_plus)
     ultimately show False
       using d_min unfolding less_eq_multiset_def by (auto intro!: antisym)
   qed
   then show ?thesis
     using dd_subs_n ddcc_imp_e dd_lt_d by auto
 qed
 
 lemma Rf_imp_ex_non_Rf:
   assumes "C \<in> Rf N"
   shows "\<exists>CC. set_mset CC \<subseteq> N - Rf N \<and> (\<forall>I. I \<Turnstile>m CC \<longrightarrow> I \<Turnstile> C) \<and> (\<forall>C'. C' \<in># CC \<longrightarrow> C' < C)"
   using assms by (auto simp: Rf_def intro: wlog_non_Rf[of _ "{#}", simplified])
 
 lemma Rf_subs_Rf_diff_Rf: "Rf N \<subseteq> Rf (N - Rf N)"
 proof
   fix C
   assume c_rf: "C \<in> Rf N"
   then obtain CC where
     cc_subs: "set_mset CC \<subseteq> N - Rf N" and
     cc_imp_c: "\<forall>I. I \<Turnstile>m CC \<longrightarrow> I \<Turnstile> C" and
     cc_lt_c: "\<forall>C'. C' \<in># CC \<longrightarrow> C' < C"
     using Rf_imp_ex_non_Rf by blast
   have "\<forall>D. D \<in># CC \<longrightarrow> D \<notin> Rf N"
     using cc_subs by (simp add: subset_iff)
   then have cc_nr:
     "\<And>C DD. C \<in># CC \<Longrightarrow> set_mset DD \<subseteq> N \<Longrightarrow> \<forall>I. I \<Turnstile>m DD \<longrightarrow> I \<Turnstile> C \<Longrightarrow> \<exists>D. D \<in># DD \<and> ~ D < C"
       unfolding Rf_def by auto metis
   have "set_mset CC \<subseteq> N"
     using cc_subs by auto
-  then have "set_mset CC \<subseteq> 
+  then have "set_mset CC \<subseteq>
     N - {C. \<exists>DD. set_mset DD \<subseteq> N \<and> (\<forall>I. I \<Turnstile>m DD \<longrightarrow> I \<Turnstile> C) \<and> (\<forall>D. D \<in># DD \<longrightarrow> D < C)}"
     using cc_nr by auto
   then show "C \<in> Rf (N - Rf N)"
     using cc_imp_c cc_lt_c unfolding Rf_def by auto
 qed
 
 lemma Rf_eq_Rf_diff_Rf: "Rf N = Rf (N - Rf N)"
   by (metis Diff_subset Rf_mono Rf_subs_Rf_diff_Rf subset_antisym)
 
 text \<open>
 The following results correspond to Lemma 4.6.
 \<close>
 
 lemma Ri_mono: "N \<subseteq> N' \<Longrightarrow> Ri N \<subseteq> Ri N'"
   unfolding Ri_def redundant_infer_def by auto
 
 lemma Ri_subs_Ri_diff_Rf: "Ri N \<subseteq> Ri (N - Rf N)"
 proof
   fix \<gamma>
   assume \<gamma>_ri: "\<gamma> \<in> Ri N"
   then obtain CC D E where \<gamma>: "\<gamma> = Infer CC D E"
     by (cases \<gamma>)
   have cc: "CC = side_prems_of \<gamma>" and d: "D = main_prem_of \<gamma>" and e: "E = concl_of \<gamma>"
     unfolding \<gamma> by simp_all
   obtain DD where
     "set_mset DD \<subseteq> N" and "\<forall>I. I \<Turnstile>m DD + CC \<longrightarrow> I \<Turnstile> E" and "\<forall>C. C \<in># DD \<longrightarrow> C < D"
     using \<gamma>_ri unfolding Ri_def redundant_infer_def cc d e by blast
   then obtain DD' where
     "set_mset DD' \<subseteq> N - Rf N" and "\<forall>I. I \<Turnstile>m DD' + CC \<longrightarrow> I \<Turnstile> E" and "\<forall>D'. D' \<in># DD' \<longrightarrow> D' < D"
     using wlog_non_Rf by atomize_elim blast
   then show "\<gamma> \<in> Ri (N - Rf N)"
     using \<gamma>_ri unfolding Ri_def redundant_infer_def d cc e by blast
 qed
 
 lemma Ri_eq_Ri_diff_Rf: "Ri N = Ri (N - Rf N)"
   by (metis Diff_subset Ri_mono Ri_subs_Ri_diff_Rf subset_antisym)
 
 lemma Ri_subset_\<Gamma>: "Ri N \<subseteq> \<Gamma>"
   unfolding Ri_def by blast
 
 lemma Rf_indep: "N' \<subseteq> Rf N \<Longrightarrow> Rf N \<subseteq> Rf (N - N')"
   by (metis Diff_cancel Diff_eq_empty_iff Diff_mono Rf_eq_Rf_diff_Rf Rf_mono)
 
 lemma Ri_indep: "N' \<subseteq> Rf N \<Longrightarrow> Ri N \<subseteq> Ri (N - N')"
   by (metis Diff_mono Ri_eq_Ri_diff_Rf Ri_mono order_refl)
 
 lemma Rf_model:
   assumes "I \<Turnstile>s N - Rf N"
   shows "I \<Turnstile>s N"
 proof -
   have "I \<Turnstile>s Rf (N - Rf N)"
     unfolding true_clss_def
     by (subst Rf_def, simp add: true_cls_mset_def, metis assms subset_eq true_clss_def)
   then have "I \<Turnstile>s Rf N"
     using Rf_subs_Rf_diff_Rf true_clss_mono by blast
   then show ?thesis
     using assms by (metis Un_Diff_cancel true_clss_union)
 qed
 
 lemma Rf_sat: "satisfiable (N - Rf N) \<Longrightarrow> satisfiable N"
   by (metis Rf_model)
 
 text \<open>
 The following corresponds to Theorem 4.7:
 \<close>
 
 sublocale redundancy_criterion \<Gamma> Rf Ri
   by unfold_locales (rule Ri_subset_\<Gamma>, (elim Rf_mono Ri_mono Rf_indep Ri_indep Rf_sat)+)
 
 end
 
 locale standard_redundancy_criterion_reductive =
   standard_redundancy_criterion + reductive_inference_system
 begin
 
 text \<open>
 The following corresponds to Theorem 4.8:
 \<close>
 
 lemma Ri_effective:
   assumes
     in_\<gamma>: "\<gamma> \<in> \<Gamma>" and
     concl_of_in_n_un_rf_n: "concl_of \<gamma> \<in> N \<union> Rf N"
   shows "\<gamma> \<in> Ri N"
 proof -
   obtain CC D E where
     \<gamma>: "\<gamma> = Infer CC D E"
     by (cases \<gamma>)
   then have cc: "CC = side_prems_of \<gamma>" and d: "D = main_prem_of \<gamma>" and e: "E = concl_of \<gamma>"
     unfolding \<gamma> by simp_all
   note e_in_n_un_rf_n = concl_of_in_n_un_rf_n[folded e]
 
   {
     assume "E \<in> N"
     moreover have "E < D"
       using \<Gamma>_reductive e d in_\<gamma> by auto
     ultimately have
       "set_mset {#E#} \<subseteq> N" and "\<forall>I. I \<Turnstile>m {#E#} + CC \<longrightarrow> I \<Turnstile> E" and "\<forall>D'. D' \<in># {#E#} \<longrightarrow> D' < D"
       by simp_all
     then have "redundant_infer N \<gamma>"
       using redundant_infer_def cc d e by blast
   }
   moreover
   {
     assume "E \<in> Rf N"
     then obtain DD where
       dd_sset: "set_mset DD \<subseteq> N" and
       dd_imp_e: "\<forall>I. I \<Turnstile>m DD \<longrightarrow> I \<Turnstile> E" and
       dd_lt_e: "\<forall>C'. C' \<in># DD \<longrightarrow> C' < E"
       unfolding Rf_def by blast
     from dd_lt_e have "\<forall>Da. Da \<in># DD \<longrightarrow> Da < D"
       using d e in_\<gamma> \<Gamma>_reductive less_trans by blast
     then have "redundant_infer N \<gamma>"
       using redundant_infer_def dd_sset dd_imp_e cc d e by blast
   }
   ultimately show "\<gamma> \<in> Ri N"
     using in_\<gamma> e_in_n_un_rf_n unfolding Ri_def by blast
 qed
 
 sublocale effective_redundancy_criterion \<Gamma> Rf Ri
   unfolding effective_redundancy_criterion_def
   by (intro conjI redundancy_criterion_axioms, unfold_locales, rule Ri_effective)
 
 lemma contradiction_Rf: "{#} \<in> N \<Longrightarrow> Ri N = \<Gamma>"
   unfolding Ri_def redundant_infer_def using \<Gamma>_reductive le_multiset_empty_right
   by (force intro: exI[of _ "{#{#}#}"] le_multiset_empty_left)
 
 end
 
 locale standard_redundancy_criterion_counterex_reducing =
   standard_redundancy_criterion + counterex_reducing_inference_system
 begin
 
 text \<open>
 The following result corresponds to Theorem 4.9.
 \<close>
 
 lemma saturated_upto_complete_if:
   assumes
     satur: "saturated_upto N" and
     unsat: "\<not> satisfiable N"
   shows "{#} \<in> N"
 proof (rule ccontr)
   assume ec_ni_n: "{#} \<notin> N"
 
   define M where
     "M = N - Rf N"
 
   have ec_ni_m: "{#} \<notin> M"
     unfolding M_def using ec_ni_n by fast
 
   have "I_of M \<Turnstile>s M"
   proof (rule ccontr)
     assume "\<not> I_of M \<Turnstile>s M"
     then obtain D where
       d_in_m: "D \<in> M" and
       d_cex: "\<not> I_of M \<Turnstile> D" and
       d_min: "\<And>C. C \<in> M \<Longrightarrow> C < D \<Longrightarrow> I_of M \<Turnstile> C"
       using ex_min_counterex by meson
     then obtain \<gamma> CC E where
       \<gamma>: "\<gamma> = Infer CC D E" and
       cc_subs_m: "set_mset CC \<subseteq> M" and
       cc_true: "I_of M \<Turnstile>m CC" and
       \<gamma>_in: "\<gamma> \<in> \<Gamma>" and
       e_cex: "\<not> I_of M \<Turnstile> E" and
       e_lt_d: "E < D"
       using \<Gamma>_counterex_reducing[OF ec_ni_m] not_less by metis
     have cc: "CC = side_prems_of \<gamma>" and d: "D = main_prem_of \<gamma>" and e: "E = concl_of \<gamma>"
       unfolding \<gamma> by simp_all
     have "\<gamma> \<in> Ri N"
       by (rule subsetD[OF satur[unfolded saturated_upto_def inferences_from_def infer_from_def]])
         (simp add: \<gamma>_in d_in_m cc_subs_m cc[symmetric] d[symmetric] M_def[symmetric])
     then have "\<gamma> \<in> Ri M"
       unfolding M_def using Ri_indep by fast
     then obtain DD where
       dd_subs_m: "set_mset DD \<subseteq> M" and
       dd_cc_imp_d: "\<forall>I. I \<Turnstile>m DD + CC \<longrightarrow> I \<Turnstile> E" and
       dd_lt_d: "\<forall>C. C \<in># DD \<longrightarrow> C < D"
       unfolding Ri_def redundant_infer_def cc d e by blast
     from dd_subs_m dd_lt_d have "I_of M \<Turnstile>m DD"
       using d_min unfolding true_cls_mset_def by (metis contra_subsetD)
     then have "I_of M \<Turnstile> E"
       using dd_cc_imp_d cc_true by auto
     then show False
       using e_cex by auto
   qed
   then have "I_of M \<Turnstile>s N"
     using M_def Rf_model by blast
   then show False
     using unsat by blast
 qed
 
 theorem saturated_upto_complete:
   assumes "saturated_upto N"
   shows "\<not> satisfiable N \<longleftrightarrow> {#} \<in> N"
   using assms saturated_upto_complete_if true_clss_def by auto
 
 end
 
 end