diff --git a/thys/Ordered_Resolution_Prover/Abstract_Substitution.thy b/thys/Ordered_Resolution_Prover/Abstract_Substitution.thy
--- a/thys/Ordered_Resolution_Prover/Abstract_Substitution.thy
+++ b/thys/Ordered_Resolution_Prover/Abstract_Substitution.thy
@@ -1,1209 +1,1267 @@
 (*  Title:       Abstract Substitutions
     Author:      Dmitriy Traytel <traytel at inf.ethz.ch>, 2014
     Author:      Jasmin Blanchette <j.c.blanchette at vu.nl>, 2014, 2017
     Author:      Anders Schlichtkrull <andschl at dtu.dk>, 2016, 2017
     Maintainer:  Anders Schlichtkrull <andschl at dtu.dk>
 *)
 
 section \<open>Abstract Substitutions\<close>
 
 theory Abstract_Substitution
   imports Clausal_Logic Map2
 begin
 
 text \<open>
 Atoms and substitutions are abstracted away behind some locales, to avoid having a direct dependency
 on the IsaFoR library.
 
 Conventions: \<open>'s\<close> substitutions, \<open>'a\<close> atoms.
 \<close>
 
 
 subsection \<open>Library\<close>
 
 lemma f_Suc_decr_eventually_const:
   fixes f :: "nat \<Rightarrow> nat"
   assumes leq: "\<forall>i. f (Suc i) \<le> f i"
   shows "\<exists>l. \<forall>l' \<ge> l. f l' = f (Suc l')"
 proof (rule ccontr)
   assume a: "\<nexists>l. \<forall>l' \<ge> l. f l' = f (Suc l')"
   have "\<forall>i. \<exists>i'. i' > i \<and> f i' < f i"
   proof
     fix i
     from a have "\<exists>l' \<ge> i. f l' \<noteq> f (Suc l')"
       by auto
     then obtain l' where
       l'_p: "l' \<ge> i \<and> f l' \<noteq> f (Suc l')"
       by metis
     then have "f l' > f (Suc l')"
       using leq le_eq_less_or_eq by auto
     moreover have "f i \<ge> f l'"
       using leq l'_p by (induction l' arbitrary: i) (blast intro: lift_Suc_antimono_le)+
     ultimately show "\<exists>i' > i. f i' < f i"
       using l'_p less_le_trans by blast
   qed
   then obtain g_sm :: "nat \<Rightarrow> nat" where
     g_sm_p: "\<forall>i. g_sm i > i \<and> f (g_sm i) < f i"
     by metis
 
   define c :: "nat \<Rightarrow> nat" where
     "\<And>n. c n = (g_sm ^^ n) 0"
 
   have "f (c i) > f (c (Suc i))" for i
     by (induction i) (auto simp: c_def g_sm_p)
   then have "\<forall>i. (f \<circ> c) i > (f \<circ> c) (Suc i)"
     by auto
   then have "\<exists>fc :: nat \<Rightarrow> nat. \<forall>i. fc i > fc (Suc i)"
     by metis
   then show False
     using wf_less_than by (simp add: wf_iff_no_infinite_down_chain)
 qed
 
 
 subsection \<open>Substitution Operators\<close>
 
 locale substitution_ops =
   fixes
     subst_atm :: "'a \<Rightarrow> 's \<Rightarrow> 'a" and
     id_subst :: 's and
     comp_subst :: "'s \<Rightarrow> 's \<Rightarrow> 's"
 begin
 
 abbreviation subst_atm_abbrev :: "'a \<Rightarrow> 's \<Rightarrow> 'a" (infixl "\<cdot>a" 67) where
   "subst_atm_abbrev \<equiv> subst_atm"
 
 abbreviation comp_subst_abbrev :: "'s \<Rightarrow> 's \<Rightarrow> 's" (infixl "\<odot>" 67) where
   "comp_subst_abbrev \<equiv> comp_subst"
 
 definition comp_substs :: "'s list \<Rightarrow> 's list \<Rightarrow> 's list" (infixl "\<odot>s" 67) where
   "\<sigma>s \<odot>s \<tau>s = map2 comp_subst \<sigma>s \<tau>s"
 
 definition subst_atms :: "'a set \<Rightarrow> 's \<Rightarrow> 'a set" (infixl "\<cdot>as" 67) where
   "AA \<cdot>as \<sigma> = (\<lambda>A. A \<cdot>a \<sigma>) ` AA"
 
 definition subst_atmss :: "'a set set \<Rightarrow> 's \<Rightarrow> 'a set set" (infixl "\<cdot>ass" 67) where
   "AAA \<cdot>ass \<sigma> = (\<lambda>AA. AA \<cdot>as \<sigma>) ` AAA"
 
 definition subst_atm_list :: "'a list \<Rightarrow> 's \<Rightarrow> 'a list" (infixl "\<cdot>al" 67) where
   "As \<cdot>al \<sigma> = map (\<lambda>A. A \<cdot>a \<sigma>) As"
 
 definition subst_atm_mset :: "'a multiset \<Rightarrow> 's \<Rightarrow> 'a multiset" (infixl "\<cdot>am" 67) where
   "AA \<cdot>am \<sigma> = image_mset (\<lambda>A. A \<cdot>a \<sigma>) AA"
 
 definition
   subst_atm_mset_list :: "'a multiset list \<Rightarrow> 's \<Rightarrow> 'a multiset list" (infixl "\<cdot>aml" 67)
 where
   "AAA \<cdot>aml \<sigma> = map (\<lambda>AA. AA \<cdot>am \<sigma>) AAA"
 
 definition
   subst_atm_mset_lists :: "'a multiset list \<Rightarrow> 's list \<Rightarrow> 'a multiset list" (infixl "\<cdot>\<cdot>aml" 67)
 where
   "AAs \<cdot>\<cdot>aml \<sigma>s = map2 (\<cdot>am) AAs \<sigma>s"
 
 definition subst_lit :: "'a literal \<Rightarrow> 's \<Rightarrow> 'a literal" (infixl "\<cdot>l" 67) where
   "L \<cdot>l \<sigma> = map_literal (\<lambda>A. A \<cdot>a \<sigma>) L"
 
 lemma atm_of_subst_lit[simp]: "atm_of (L \<cdot>l \<sigma>) = atm_of L \<cdot>a \<sigma>"
   unfolding subst_lit_def by (cases L) simp+
 
 definition subst_cls :: "'a clause \<Rightarrow> 's \<Rightarrow> 'a clause" (infixl "\<cdot>" 67) where
   "AA \<cdot> \<sigma> = image_mset (\<lambda>A. A \<cdot>l \<sigma>) AA"
 
 definition subst_clss :: "'a clause set \<Rightarrow> 's \<Rightarrow> 'a clause set" (infixl "\<cdot>cs" 67) where
   "AA \<cdot>cs \<sigma> = (\<lambda>A. A \<cdot> \<sigma>) ` AA"
 
 definition subst_cls_list :: "'a clause list \<Rightarrow> 's \<Rightarrow> 'a clause list" (infixl "\<cdot>cl" 67) where
   "Cs \<cdot>cl \<sigma> = map (\<lambda>A. A \<cdot> \<sigma>) Cs"
 
 definition subst_cls_lists :: "'a clause list \<Rightarrow> 's list \<Rightarrow> 'a clause list" (infixl "\<cdot>\<cdot>cl" 67) where
   "Cs \<cdot>\<cdot>cl \<sigma>s = map2 (\<cdot>) Cs \<sigma>s"
 
 definition subst_cls_mset :: "'a clause multiset \<Rightarrow> 's \<Rightarrow> 'a clause multiset" (infixl "\<cdot>cm" 67) where
   "CC \<cdot>cm \<sigma> = image_mset (\<lambda>A. A \<cdot> \<sigma>) CC"
 
 lemma subst_cls_add_mset[simp]: "add_mset L C \<cdot> \<sigma> = add_mset (L \<cdot>l \<sigma>) (C \<cdot> \<sigma>)"
   unfolding subst_cls_def by simp
 
 lemma subst_cls_mset_add_mset[simp]: "add_mset C CC \<cdot>cm \<sigma> = add_mset (C \<cdot> \<sigma>) (CC \<cdot>cm \<sigma>)"
   unfolding subst_cls_mset_def by simp
 
 definition generalizes_atm :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where
   "generalizes_atm A B \<longleftrightarrow> (\<exists>\<sigma>. A \<cdot>a \<sigma> = B)"
 
 definition strictly_generalizes_atm :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where
   "strictly_generalizes_atm A B \<longleftrightarrow> generalizes_atm A B \<and> \<not> generalizes_atm B A"
 
 definition generalizes_lit :: "'a literal \<Rightarrow> 'a literal \<Rightarrow> bool" where
   "generalizes_lit L M \<longleftrightarrow> (\<exists>\<sigma>. L \<cdot>l \<sigma> = M)"
 
 definition strictly_generalizes_lit :: "'a literal \<Rightarrow> 'a literal \<Rightarrow> bool" where
   "strictly_generalizes_lit L M \<longleftrightarrow> generalizes_lit L M \<and> \<not> generalizes_lit M L"
 
 definition generalizes :: "'a clause \<Rightarrow> 'a clause \<Rightarrow> bool" where
   "generalizes C D \<longleftrightarrow> (\<exists>\<sigma>. C \<cdot> \<sigma> = D)"
 
 definition strictly_generalizes :: "'a clause \<Rightarrow> 'a clause \<Rightarrow> bool" where
   "strictly_generalizes C D \<longleftrightarrow> generalizes C D \<and> \<not> generalizes D C"
 
 definition subsumes :: "'a clause \<Rightarrow> 'a clause \<Rightarrow> bool" where
   "subsumes C D \<longleftrightarrow> (\<exists>\<sigma>. C \<cdot> \<sigma> \<subseteq># D)"
 
 definition strictly_subsumes :: "'a clause \<Rightarrow> 'a clause \<Rightarrow> bool" where
   "strictly_subsumes C D \<longleftrightarrow> subsumes C D \<and> \<not> subsumes D C"
 
 definition variants :: "'a clause \<Rightarrow> 'a clause \<Rightarrow> bool" where
   "variants C D \<longleftrightarrow> generalizes C D \<and> generalizes D C"
 
 definition is_renaming :: "'s \<Rightarrow> bool" where
   "is_renaming \<sigma> \<longleftrightarrow> (\<exists>\<tau>. \<sigma> \<odot> \<tau> = id_subst)"
 
 definition is_renaming_list :: "'s list \<Rightarrow> bool" where
   "is_renaming_list \<sigma>s \<longleftrightarrow> (\<forall>\<sigma> \<in> set \<sigma>s. is_renaming \<sigma>)"
 
 definition inv_renaming :: "'s \<Rightarrow> 's" where
   "inv_renaming \<sigma> = (SOME \<tau>. \<sigma> \<odot> \<tau> = id_subst)"
 
 definition is_ground_atm :: "'a \<Rightarrow> bool" where
   "is_ground_atm A \<longleftrightarrow> (\<forall>\<sigma>. A = A \<cdot>a \<sigma>)"
 
 definition is_ground_atms :: "'a set \<Rightarrow> bool" where
   "is_ground_atms AA = (\<forall>A \<in> AA. is_ground_atm A)"
 
 definition is_ground_atm_list :: "'a list \<Rightarrow> bool" where
   "is_ground_atm_list As \<longleftrightarrow> (\<forall>A \<in> set As. is_ground_atm A)"
 
 definition is_ground_atm_mset :: "'a multiset \<Rightarrow> bool" where
   "is_ground_atm_mset AA \<longleftrightarrow> (\<forall>A. A \<in># AA \<longrightarrow> is_ground_atm A)"
 
 definition is_ground_lit :: "'a literal \<Rightarrow> bool" where
   "is_ground_lit L \<longleftrightarrow> is_ground_atm (atm_of L)"
 
 definition is_ground_cls :: "'a clause \<Rightarrow> bool" where
   "is_ground_cls C \<longleftrightarrow> (\<forall>L. L \<in># C \<longrightarrow> is_ground_lit L)"
 
 definition is_ground_clss :: "'a clause set \<Rightarrow> bool" where
   "is_ground_clss CC \<longleftrightarrow> (\<forall>C \<in> CC. is_ground_cls C)"
 
 definition is_ground_cls_list :: "'a clause list \<Rightarrow> bool" where
   "is_ground_cls_list CC \<longleftrightarrow> (\<forall>C \<in> set CC. is_ground_cls C)"
 
 definition is_ground_subst :: "'s \<Rightarrow> bool" where
   "is_ground_subst \<sigma> \<longleftrightarrow> (\<forall>A. is_ground_atm (A \<cdot>a \<sigma>))"
 
 definition is_ground_subst_list :: "'s list \<Rightarrow> bool" where
   "is_ground_subst_list \<sigma>s \<longleftrightarrow> (\<forall>\<sigma> \<in> set \<sigma>s. is_ground_subst \<sigma>)"
 
 definition grounding_of_cls :: "'a clause \<Rightarrow> 'a clause set" where
   "grounding_of_cls C = {C \<cdot> \<sigma> |\<sigma>. is_ground_subst \<sigma>}"
 
 definition grounding_of_clss :: "'a clause set \<Rightarrow> 'a clause set" where
   "grounding_of_clss CC = (\<Union>C \<in> CC. grounding_of_cls C)"
 
 definition is_unifier :: "'s \<Rightarrow> 'a set \<Rightarrow> bool" where
   "is_unifier \<sigma> AA \<longleftrightarrow> card (AA \<cdot>as \<sigma>) \<le> 1"
 
 definition is_unifiers :: "'s \<Rightarrow> 'a set set \<Rightarrow> bool" where
   "is_unifiers \<sigma> AAA \<longleftrightarrow> (\<forall>AA \<in> AAA. is_unifier \<sigma> AA)"
 
 definition is_mgu :: "'s \<Rightarrow> 'a set set \<Rightarrow> bool" where
   "is_mgu \<sigma> AAA \<longleftrightarrow> is_unifiers \<sigma> AAA \<and> (\<forall>\<tau>. is_unifiers \<tau> AAA \<longrightarrow> (\<exists>\<gamma>. \<tau> = \<sigma> \<odot> \<gamma>))"
 
 definition var_disjoint :: "'a clause list \<Rightarrow> bool" where
   "var_disjoint Cs \<longleftrightarrow>
    (\<forall>\<sigma>s. length \<sigma>s = length Cs \<longrightarrow> (\<exists>\<tau>. \<forall>i < length Cs. \<forall>S. S \<subseteq># Cs ! i \<longrightarrow> S \<cdot> \<sigma>s ! i = S \<cdot> \<tau>))"
 
 end
 
 
 subsection \<open>Substitution Lemmas\<close>
 
 locale substitution = substitution_ops subst_atm id_subst comp_subst
   for
     subst_atm :: "'a \<Rightarrow> 's \<Rightarrow> 'a" and
     id_subst :: 's and
     comp_subst :: "'s \<Rightarrow> 's \<Rightarrow> 's" +
   fixes
     renamings_apart :: "'a clause list \<Rightarrow> 's list" and
     atm_of_atms :: "'a list \<Rightarrow> 'a"
   assumes
     subst_atm_id_subst[simp]: "A \<cdot>a id_subst = A" and
     subst_atm_comp_subst[simp]: "A \<cdot>a (\<sigma> \<odot> \<tau>) = (A \<cdot>a \<sigma>) \<cdot>a \<tau>" and
     subst_ext: "(\<And>A. A \<cdot>a \<sigma> = A \<cdot>a \<tau>) \<Longrightarrow> \<sigma> = \<tau>" and
     make_ground_subst: "is_ground_cls (C \<cdot> \<sigma>) \<Longrightarrow> \<exists>\<tau>. is_ground_subst \<tau> \<and>C \<cdot> \<tau> = C \<cdot> \<sigma>" and
     wf_strictly_generalizes_atm: "wfP strictly_generalizes_atm" and
     renamings_apart_length:  "length (renamings_apart Cs) = length Cs" and
     renamings_apart_renaming: "\<rho> \<in> set (renamings_apart Cs) \<Longrightarrow> is_renaming \<rho>" and
     renamings_apart_var_disjoint: "var_disjoint (Cs \<cdot>\<cdot>cl (renamings_apart Cs))" and
     atm_of_atms_subst:
       "\<And>As Bs. atm_of_atms As \<cdot>a \<sigma> = atm_of_atms Bs \<longleftrightarrow> map (\<lambda>A. A \<cdot>a \<sigma>) As = Bs"
 begin
 
 lemma subst_ext_iff: "\<sigma> = \<tau> \<longleftrightarrow> (\<forall>A. A \<cdot>a \<sigma> = A \<cdot>a \<tau>)"
   by (blast intro: subst_ext)
 
 
 subsubsection \<open>Identity Substitution\<close>
 
 lemma id_subst_comp_subst[simp]: "id_subst \<odot> \<sigma> = \<sigma>"
   by (rule subst_ext) simp
 
 lemma comp_subst_id_subst[simp]: "\<sigma> \<odot> id_subst = \<sigma>"
   by (rule subst_ext) simp
 
 lemma id_subst_comp_substs[simp]: "replicate (length \<sigma>s) id_subst \<odot>s \<sigma>s = \<sigma>s"
   using comp_substs_def by (induction \<sigma>s) auto
 
 lemma comp_substs_id_subst[simp]: "\<sigma>s \<odot>s replicate (length \<sigma>s) id_subst = \<sigma>s"
   using comp_substs_def by (induction \<sigma>s) auto
 
 lemma subst_atms_id_subst[simp]: "AA \<cdot>as id_subst = AA"
   unfolding subst_atms_def by simp
 
 lemma subst_atmss_id_subst[simp]: "AAA \<cdot>ass id_subst = AAA"
   unfolding subst_atmss_def by simp
 
 lemma subst_atm_list_id_subst[simp]: "As \<cdot>al id_subst = As"
   unfolding subst_atm_list_def by auto
 
 lemma subst_atm_mset_id_subst[simp]: "AA \<cdot>am id_subst = AA"
   unfolding subst_atm_mset_def by simp
 
 lemma subst_atm_mset_list_id_subst[simp]: "AAs \<cdot>aml id_subst = AAs"
   unfolding subst_atm_mset_list_def by simp
 
 lemma subst_atm_mset_lists_id_subst[simp]: "AAs \<cdot>\<cdot>aml replicate (length AAs) id_subst = AAs"
   unfolding subst_atm_mset_lists_def by (induct AAs) auto
 
 lemma subst_lit_id_subst[simp]: "L \<cdot>l id_subst = L"
   unfolding subst_lit_def by (simp add: literal.map_ident)
 
 lemma subst_cls_id_subst[simp]: "C \<cdot> id_subst = C"
   unfolding subst_cls_def by simp
 
 lemma subst_clss_id_subst[simp]: "CC \<cdot>cs id_subst = CC"
   unfolding subst_clss_def by simp
 
 lemma subst_cls_list_id_subst[simp]: "Cs \<cdot>cl id_subst = Cs"
   unfolding subst_cls_list_def by simp
 
 lemma subst_cls_lists_id_subst[simp]: "Cs \<cdot>\<cdot>cl replicate (length Cs) id_subst = Cs"
   unfolding subst_cls_lists_def by (induct Cs) auto
 
 lemma subst_cls_mset_id_subst[simp]: "CC \<cdot>cm id_subst = CC"
   unfolding subst_cls_mset_def by simp
 
 
 subsubsection \<open>Associativity of Composition\<close>
 
 lemma comp_subst_assoc[simp]: "\<sigma> \<odot> (\<tau> \<odot> \<gamma>) = \<sigma> \<odot> \<tau> \<odot> \<gamma>"
   by (rule subst_ext) simp
 
 
 subsubsection \<open>Compatibility of Substitution and Composition\<close>
 
 lemma subst_atms_comp_subst[simp]: "AA \<cdot>as (\<tau> \<odot> \<sigma>) = AA \<cdot>as \<tau> \<cdot>as \<sigma>"
   unfolding subst_atms_def by auto
 
 lemma subst_atmss_comp_subst[simp]: "AAA \<cdot>ass (\<tau> \<odot> \<sigma>) = AAA \<cdot>ass \<tau> \<cdot>ass \<sigma>"
   unfolding subst_atmss_def by auto
 
 lemma subst_atm_list_comp_subst[simp]: "As \<cdot>al (\<tau> \<odot> \<sigma>) = As \<cdot>al \<tau> \<cdot>al \<sigma>"
   unfolding subst_atm_list_def by auto
 
 lemma subst_atm_mset_comp_subst[simp]: "AA \<cdot>am (\<tau> \<odot> \<sigma>) = AA \<cdot>am \<tau> \<cdot>am \<sigma>"
   unfolding subst_atm_mset_def by auto
 
 lemma subst_atm_mset_list_comp_subst[simp]: "AAs \<cdot>aml (\<tau> \<odot> \<sigma>) = (AAs \<cdot>aml \<tau>) \<cdot>aml \<sigma>"
   unfolding subst_atm_mset_list_def by auto
 
 lemma subst_atm_mset_lists_comp_substs[simp]: "AAs \<cdot>\<cdot>aml (\<tau>s \<odot>s \<sigma>s) = AAs \<cdot>\<cdot>aml \<tau>s \<cdot>\<cdot>aml \<sigma>s"
   unfolding subst_atm_mset_lists_def comp_substs_def map_zip_map map_zip_map2 map_zip_assoc
   by (simp add: split_def)
 
 lemma subst_lit_comp_subst[simp]: "L \<cdot>l (\<tau> \<odot> \<sigma>) = L \<cdot>l \<tau> \<cdot>l \<sigma>"
   unfolding subst_lit_def by (auto simp: literal.map_comp o_def)
 
 lemma subst_cls_comp_subst[simp]: "C \<cdot> (\<tau> \<odot> \<sigma>) = C \<cdot> \<tau> \<cdot> \<sigma>"
   unfolding subst_cls_def by auto
 
 lemma subst_clsscomp_subst[simp]: "CC \<cdot>cs (\<tau> \<odot> \<sigma>) = CC \<cdot>cs \<tau> \<cdot>cs \<sigma>"
   unfolding subst_clss_def by auto
 
 lemma subst_cls_list_comp_subst[simp]: "Cs \<cdot>cl (\<tau> \<odot> \<sigma>) = Cs \<cdot>cl \<tau> \<cdot>cl \<sigma>"
   unfolding subst_cls_list_def by auto
 
 lemma subst_cls_lists_comp_substs[simp]: "Cs \<cdot>\<cdot>cl (\<tau>s \<odot>s \<sigma>s) = Cs \<cdot>\<cdot>cl \<tau>s \<cdot>\<cdot>cl \<sigma>s"
   unfolding subst_cls_lists_def comp_substs_def map_zip_map map_zip_map2 map_zip_assoc
   by (simp add: split_def)
 
 lemma subst_cls_mset_comp_subst[simp]: "CC \<cdot>cm (\<tau> \<odot> \<sigma>) = CC \<cdot>cm \<tau> \<cdot>cm \<sigma>"
   unfolding subst_cls_mset_def by auto
 
 
 subsubsection \<open>``Commutativity'' of Membership and Substitution\<close>
 
 lemma Melem_subst_atm_mset[simp]: "A \<in># AA \<cdot>am \<sigma> \<longleftrightarrow> (\<exists>B. B \<in># AA \<and> A = B \<cdot>a \<sigma>)"
   unfolding subst_atm_mset_def by auto
 
 lemma Melem_subst_cls[simp]: "L \<in># C \<cdot> \<sigma> \<longleftrightarrow> (\<exists>M. M \<in># C \<and> L = M \<cdot>l \<sigma>)"
   unfolding subst_cls_def by auto
 
 lemma Melem_subst_cls_mset[simp]: "AA \<in># CC \<cdot>cm \<sigma> \<longleftrightarrow> (\<exists>BB. BB \<in># CC \<and> AA = BB \<cdot> \<sigma>)"
   unfolding subst_cls_mset_def by auto
 
 
 subsubsection \<open>Signs and Substitutions\<close>
 
 lemma subst_lit_is_neg[simp]: "is_neg (L \<cdot>l \<sigma>) = is_neg L"
   unfolding subst_lit_def by auto
 
 lemma subst_lit_is_pos[simp]: "is_pos (L \<cdot>l \<sigma>) = is_pos L"
   unfolding subst_lit_def by auto
 
 lemma subst_minus[simp]: "(- L) \<cdot>l \<mu> = - (L  \<cdot>l \<mu>)"
   by (simp add: literal.map_sel subst_lit_def uminus_literal_def)
 
 
 subsubsection \<open>Substitution on Literal(s)\<close>
 
 lemma eql_neg_lit_eql_atm[simp]: "(Neg A' \<cdot>l \<eta>) = Neg A \<longleftrightarrow> A' \<cdot>a \<eta> = A"
   by (simp add: subst_lit_def)
 
 lemma eql_pos_lit_eql_atm[simp]: "(Pos A' \<cdot>l \<eta>) = Pos A \<longleftrightarrow> A' \<cdot>a \<eta> = A"
   by (simp add: subst_lit_def)
 
 lemma subst_cls_negs[simp]: "(negs AA) \<cdot> \<sigma> = negs (AA \<cdot>am \<sigma>)"
   unfolding subst_cls_def subst_lit_def subst_atm_mset_def by auto
 
 lemma subst_cls_poss[simp]: "(poss AA) \<cdot> \<sigma> = poss (AA \<cdot>am \<sigma>)"
   unfolding subst_cls_def subst_lit_def subst_atm_mset_def by auto
 
 lemma atms_of_subst_atms: "atms_of C \<cdot>as \<sigma> = atms_of (C \<cdot> \<sigma>)"
 proof -
   have "atms_of (C \<cdot> \<sigma>) = set_mset (image_mset atm_of (image_mset (map_literal (\<lambda>A. A \<cdot>a \<sigma>)) C))"
     unfolding subst_cls_def subst_atms_def subst_lit_def atms_of_def by auto
   also have "... = set_mset (image_mset (\<lambda>A. A \<cdot>a \<sigma>) (image_mset atm_of C))"
     by simp (meson literal.map_sel)
   finally show "atms_of C \<cdot>as \<sigma> = atms_of (C \<cdot> \<sigma>)"
     unfolding subst_atms_def atms_of_def by auto
 qed
 
 lemma in_image_Neg_is_neg[simp]: "L \<cdot>l \<sigma> \<in> Neg ` AA \<Longrightarrow> is_neg L"
   by (metis bex_imageD literal.disc(2) literal.map_disc_iff subst_lit_def)
 
 lemma subst_lit_in_negs_subst_is_neg: "L \<cdot>l \<sigma> \<in># (negs AA) \<cdot> \<tau> \<Longrightarrow> is_neg L"
   by simp
 
 lemma subst_lit_in_negs_is_neg: "L \<cdot>l \<sigma> \<in># negs AA \<Longrightarrow> is_neg L"
   by simp
 
 
 subsubsection \<open>Substitution on Empty\<close>
 
 lemma subst_atms_empty[simp]: "{} \<cdot>as \<sigma> = {}"
   unfolding subst_atms_def by auto
 
 lemma subst_atmss_empty[simp]: "{} \<cdot>ass \<sigma> = {}"
   unfolding subst_atmss_def by auto
 
 lemma comp_substs_empty_iff[simp]: "\<sigma>s \<odot>s \<eta>s = [] \<longleftrightarrow> \<sigma>s = [] \<or> \<eta>s = []"
   using comp_substs_def map2_empty_iff by auto
 
 lemma subst_atm_list_empty[simp]: "[] \<cdot>al \<sigma> = []"
   unfolding subst_atm_list_def by auto
 
 lemma subst_atm_mset_empty[simp]: "{#} \<cdot>am \<sigma> = {#}"
   unfolding subst_atm_mset_def by auto
 
 lemma subst_atm_mset_list_empty[simp]: "[] \<cdot>aml \<sigma> = []"
   unfolding subst_atm_mset_list_def by auto
 
 lemma subst_atm_mset_lists_empty[simp]: "[] \<cdot>\<cdot>aml \<sigma>s = []"
   unfolding subst_atm_mset_lists_def by auto
 
 lemma subst_cls_empty[simp]: "{#} \<cdot> \<sigma> = {#}"
   unfolding subst_cls_def by auto
 
 lemma subst_clss_empty[simp]: "{} \<cdot>cs \<sigma> = {}"
   unfolding subst_clss_def by auto
 
 lemma subst_cls_list_empty[simp]: "[] \<cdot>cl \<sigma> = []"
   unfolding subst_cls_list_def by auto
 
 lemma subst_cls_lists_empty[simp]: "[] \<cdot>\<cdot>cl \<sigma>s = []"
   unfolding subst_cls_lists_def by auto
 
 lemma subst_scls_mset_empty[simp]: "{#} \<cdot>cm \<sigma> = {#}"
   unfolding subst_cls_mset_def by auto
 
 lemma subst_atms_empty_iff[simp]: "AA \<cdot>as \<eta> = {} \<longleftrightarrow> AA = {}"
   unfolding subst_atms_def by auto
 
 lemma subst_atmss_empty_iff[simp]: "AAA \<cdot>ass \<eta> = {} \<longleftrightarrow> AAA = {}"
   unfolding subst_atmss_def by auto
 
 lemma subst_atm_list_empty_iff[simp]: "As \<cdot>al \<eta> = [] \<longleftrightarrow> As = []"
   unfolding subst_atm_list_def by auto
 
 lemma subst_atm_mset_empty_iff[simp]: "AA \<cdot>am \<eta> = {#} \<longleftrightarrow> AA = {#}"
   unfolding subst_atm_mset_def by auto
 
 lemma subst_atm_mset_list_empty_iff[simp]: "AAs \<cdot>aml \<eta> = [] \<longleftrightarrow> AAs = []"
   unfolding subst_atm_mset_list_def by auto
 
 lemma subst_atm_mset_lists_empty_iff[simp]: "AAs \<cdot>\<cdot>aml \<eta>s = [] \<longleftrightarrow> (AAs = [] \<or> \<eta>s = [])"
   using map2_empty_iff subst_atm_mset_lists_def by auto
 
 lemma subst_cls_empty_iff[simp]: "C \<cdot> \<eta> = {#} \<longleftrightarrow> C = {#}"
   unfolding subst_cls_def by auto
 
 lemma subst_clss_empty_iff[simp]: "CC \<cdot>cs \<eta> = {} \<longleftrightarrow> CC = {}"
   unfolding subst_clss_def by auto
 
 lemma subst_cls_list_empty_iff[simp]: "Cs \<cdot>cl \<eta> = [] \<longleftrightarrow> Cs = []"
   unfolding subst_cls_list_def by auto
 
 lemma subst_cls_lists_empty_iff[simp]: "Cs \<cdot>\<cdot>cl \<eta>s = [] \<longleftrightarrow> Cs = [] \<or> \<eta>s = []"
   using map2_empty_iff subst_cls_lists_def by auto
 
 lemma subst_cls_mset_empty_iff[simp]: "CC \<cdot>cm \<eta> = {#} \<longleftrightarrow> CC = {#}"
   unfolding subst_cls_mset_def by auto
 
 
 subsubsection \<open>Substitution on a Union\<close>
 
 lemma subst_atms_union[simp]: "(AA \<union> BB) \<cdot>as \<sigma> = AA \<cdot>as \<sigma> \<union> BB \<cdot>as \<sigma>"
   unfolding subst_atms_def by auto
 
 lemma subst_atmss_union[simp]: "(AAA \<union> BBB) \<cdot>ass \<sigma> = AAA \<cdot>ass \<sigma> \<union> BBB \<cdot>ass \<sigma>"
   unfolding subst_atmss_def by auto
 
 lemma subst_atm_list_append[simp]: "(As @ Bs) \<cdot>al \<sigma> = As \<cdot>al \<sigma> @ Bs \<cdot>al \<sigma>"
   unfolding subst_atm_list_def by auto
 
 lemma subst_atm_mset_union[simp]: "(AA + BB) \<cdot>am \<sigma> = AA \<cdot>am \<sigma> + BB \<cdot>am \<sigma>"
   unfolding subst_atm_mset_def by auto
 
 lemma subst_atm_mset_list_append[simp]: "(AAs @ BBs) \<cdot>aml \<sigma> = AAs \<cdot>aml \<sigma> @ BBs \<cdot>aml \<sigma>"
   unfolding subst_atm_mset_list_def by auto
 
 lemma subst_cls_union[simp]: "(C + D) \<cdot> \<sigma> = C \<cdot> \<sigma> + D \<cdot> \<sigma>"
   unfolding subst_cls_def by auto
 
 lemma subst_clss_union[simp]: "(CC \<union> DD) \<cdot>cs \<sigma> = CC \<cdot>cs \<sigma> \<union> DD \<cdot>cs \<sigma>"
   unfolding subst_clss_def by auto
 
 lemma subst_cls_list_append[simp]: "(Cs @ Ds) \<cdot>cl \<sigma> = Cs \<cdot>cl \<sigma> @ Ds \<cdot>cl \<sigma>"
   unfolding subst_cls_list_def by auto
 
 lemma subst_cls_lists_append[simp]:
   "length Cs = length \<sigma>s \<Longrightarrow> length Cs' = length \<sigma>s' \<Longrightarrow>
    (Cs @ Cs') \<cdot>\<cdot>cl (\<sigma>s @ \<sigma>s') = Cs \<cdot>\<cdot>cl \<sigma>s @ Cs' \<cdot>\<cdot>cl \<sigma>s'"
   unfolding subst_cls_lists_def by auto
 
 lemma subst_cls_mset_union[simp]: "(CC + DD) \<cdot>cm \<sigma> = CC \<cdot>cm \<sigma> + DD \<cdot>cm \<sigma>"
   unfolding subst_cls_mset_def by auto
 
 
 subsubsection \<open>Substitution on a Singleton\<close>
 
 lemma subst_atms_single[simp]: "{A} \<cdot>as \<sigma> = {A \<cdot>a \<sigma>}"
   unfolding subst_atms_def by auto
 
 lemma subst_atmss_single[simp]: "{AA} \<cdot>ass \<sigma> = {AA \<cdot>as \<sigma>}"
   unfolding subst_atmss_def by auto
 
 lemma subst_atm_list_single[simp]: "[A] \<cdot>al \<sigma> = [A \<cdot>a \<sigma>]"
   unfolding subst_atm_list_def by auto
 
 lemma subst_atm_mset_single[simp]: "{#A#} \<cdot>am \<sigma> = {#A \<cdot>a \<sigma>#}"
   unfolding subst_atm_mset_def by auto
 
 lemma subst_atm_mset_list[simp]: "[AA] \<cdot>aml \<sigma> = [AA \<cdot>am \<sigma>]"
   unfolding subst_atm_mset_list_def by auto
 
 lemma subst_cls_single[simp]: "{#L#} \<cdot> \<sigma> = {#L \<cdot>l \<sigma>#}"
   by simp
 
 lemma subst_clss_single[simp]: "{C} \<cdot>cs \<sigma> = {C \<cdot> \<sigma>}"
   unfolding subst_clss_def by auto
 
 lemma subst_cls_list_single[simp]: "[C] \<cdot>cl \<sigma> = [C \<cdot> \<sigma>]"
   unfolding subst_cls_list_def by auto
 
 lemma subst_cls_lists_single[simp]: "[C] \<cdot>\<cdot>cl [\<sigma>] = [C \<cdot> \<sigma>]"
   unfolding subst_cls_lists_def by auto
 
 lemma subst_cls_mset_single[simp]: "{#C#} \<cdot>cm \<sigma> = {#C \<cdot> \<sigma>#}"
   by simp
 
 
 subsubsection \<open>Substitution on @{term Cons}\<close>
 
 lemma subst_atm_list_Cons[simp]: "(A # As) \<cdot>al \<sigma> = A \<cdot>a \<sigma> # As \<cdot>al \<sigma>"
   unfolding subst_atm_list_def by auto
 
 lemma subst_atm_mset_list_Cons[simp]: "(A # As) \<cdot>aml \<sigma> = A \<cdot>am \<sigma> # As \<cdot>aml \<sigma>"
   unfolding subst_atm_mset_list_def by auto
 
 lemma subst_atm_mset_lists_Cons[simp]: "(C # Cs) \<cdot>\<cdot>aml (\<sigma> # \<sigma>s) = C \<cdot>am \<sigma> # Cs \<cdot>\<cdot>aml \<sigma>s"
   unfolding subst_atm_mset_lists_def by auto
 
 lemma subst_cls_list_Cons[simp]: "(C # Cs) \<cdot>cl \<sigma> = C \<cdot> \<sigma> # Cs \<cdot>cl \<sigma>"
   unfolding subst_cls_list_def by auto
 
 lemma subst_cls_lists_Cons[simp]: "(C # Cs) \<cdot>\<cdot>cl (\<sigma> # \<sigma>s) = C \<cdot> \<sigma> # Cs \<cdot>\<cdot>cl \<sigma>s"
   unfolding subst_cls_lists_def by auto
 
 
 subsubsection \<open>Substitution on @{term tl}\<close>
 
 lemma subst_atm_list_tl[simp]: "tl (As \<cdot>al \<sigma>) = tl As \<cdot>al \<sigma>"
   by (cases As) auto
 
 lemma subst_atm_mset_list_tl[simp]: "tl (AAs \<cdot>aml \<sigma>) = tl AAs \<cdot>aml \<sigma>"
   by (cases AAs) auto
 
 lemma subst_cls_list_tl[simp]: "tl (Cs \<cdot>cl \<sigma>) = tl Cs \<cdot>cl \<sigma>"
   by (cases Cs) auto
 
 lemma subst_cls_lists_tl[simp]: "length Cs = length \<sigma>s \<Longrightarrow> tl (Cs \<cdot>\<cdot>cl \<sigma>s) = tl Cs \<cdot>\<cdot>cl tl \<sigma>s"
   by (cases Cs; cases \<sigma>s) auto
 
 
 subsubsection \<open>Substitution on @{term nth}\<close>
 
 lemma comp_substs_nth[simp]:
   "length \<tau>s = length \<sigma>s \<Longrightarrow> i < length \<tau>s \<Longrightarrow> (\<tau>s \<odot>s \<sigma>s) ! i = (\<tau>s ! i) \<odot> (\<sigma>s ! i)"
   by (simp add: comp_substs_def)
 
 lemma subst_atm_list_nth[simp]: "i < length As \<Longrightarrow> (As \<cdot>al \<tau>) ! i = As ! i \<cdot>a \<tau>"
   unfolding subst_atm_list_def using less_Suc_eq_0_disj nth_map by force
 
 lemma subst_atm_mset_list_nth[simp]: "i < length AAs \<Longrightarrow> (AAs \<cdot>aml \<eta>) ! i = (AAs ! i) \<cdot>am \<eta>"
   unfolding subst_atm_mset_list_def by auto
 
 lemma subst_atm_mset_lists_nth[simp]:
   "length AAs = length \<sigma>s \<Longrightarrow> i < length AAs \<Longrightarrow> (AAs \<cdot>\<cdot>aml \<sigma>s) ! i = (AAs ! i) \<cdot>am (\<sigma>s ! i)"
   unfolding subst_atm_mset_lists_def by auto
 
 lemma subst_cls_list_nth[simp]: "i < length Cs \<Longrightarrow> (Cs \<cdot>cl \<tau>) ! i = (Cs ! i) \<cdot> \<tau>"
   unfolding subst_cls_list_def using less_Suc_eq_0_disj nth_map by (induction Cs) auto
 
 lemma subst_cls_lists_nth[simp]:
   "length Cs = length \<sigma>s \<Longrightarrow> i < length Cs \<Longrightarrow> (Cs \<cdot>\<cdot>cl \<sigma>s) ! i = (Cs ! i) \<cdot> (\<sigma>s ! i)"
   unfolding subst_cls_lists_def by auto
 
 
 subsubsection \<open>Substitution on Various Other Functions\<close>
 
 lemma subst_clss_image[simp]: "image f X \<cdot>cs \<sigma> = {f x \<cdot> \<sigma> | x. x \<in> X}"
   unfolding subst_clss_def by auto
 
 lemma subst_cls_mset_image_mset[simp]: "image_mset f X \<cdot>cm \<sigma> = {# f x \<cdot> \<sigma>. x \<in># X #}"
   unfolding subst_cls_mset_def by auto
 
 lemma mset_subst_atm_list_subst_atm_mset[simp]: "mset (As \<cdot>al \<sigma>) = mset (As) \<cdot>am \<sigma>"
   unfolding subst_atm_list_def subst_atm_mset_def by auto
 
 lemma mset_subst_cls_list_subst_cls_mset: "mset (Cs \<cdot>cl \<sigma>) = (mset Cs) \<cdot>cm \<sigma>"
   unfolding subst_cls_mset_def subst_cls_list_def by auto
 
 lemma sum_list_subst_cls_list_subst_cls[simp]: "sum_list (Cs \<cdot>cl \<eta>) = sum_list Cs \<cdot> \<eta>"
   unfolding subst_cls_list_def by (induction Cs) auto
 
 lemma set_mset_subst_cls_mset_subst_clss: "set_mset (CC \<cdot>cm \<mu>) = (set_mset CC) \<cdot>cs \<mu>"
   by (simp add: subst_cls_mset_def subst_clss_def)
 
 lemma Neg_Melem_subst_atm_subst_cls[simp]: "Neg A \<in># C \<Longrightarrow> Neg (A \<cdot>a \<sigma>) \<in># C \<cdot> \<sigma> "
   by (metis Melem_subst_cls eql_neg_lit_eql_atm)
 
 lemma Pos_Melem_subst_atm_subst_cls[simp]: "Pos A \<in># C \<Longrightarrow> Pos (A \<cdot>a \<sigma>) \<in># C \<cdot> \<sigma> "
   by (metis Melem_subst_cls eql_pos_lit_eql_atm)
 
 lemma in_atms_of_subst[simp]: "B \<in> atms_of C \<Longrightarrow> B \<cdot>a \<sigma> \<in> atms_of (C \<cdot> \<sigma>)"
   by (metis atms_of_subst_atms image_iff subst_atms_def)
 
 
 subsubsection \<open>Renamings\<close>
 
 lemma is_renaming_id_subst[simp]: "is_renaming id_subst"
   unfolding is_renaming_def by simp
 
 lemma is_renamingD: "is_renaming \<sigma> \<Longrightarrow> (\<forall>A1 A2. A1 \<cdot>a \<sigma> = A2 \<cdot>a \<sigma> \<longleftrightarrow> A1 = A2)"
   by (metis is_renaming_def subst_atm_comp_subst subst_atm_id_subst)
 
 lemma inv_renaming_cancel_r[simp]: "is_renaming r \<Longrightarrow> r \<odot> inv_renaming r = id_subst"
   unfolding inv_renaming_def is_renaming_def by (metis (mono_tags) someI_ex)
 
 lemma inv_renaming_cancel_r_list[simp]:
   "is_renaming_list rs \<Longrightarrow> rs \<odot>s map inv_renaming rs = replicate (length rs) id_subst"
   unfolding is_renaming_list_def by (induction rs) (auto simp add: comp_substs_def)
 
 lemma Nil_comp_substs[simp]: "[] \<odot>s s = []"
   unfolding comp_substs_def by auto
 
 lemma comp_substs_Nil[simp]: "s \<odot>s [] = []"
   unfolding comp_substs_def by auto
 
 lemma is_renaming_idempotent_id_subst: "is_renaming r \<Longrightarrow> r \<odot> r = r \<Longrightarrow> r = id_subst"
   by (metis comp_subst_assoc comp_subst_id_subst inv_renaming_cancel_r)
 
 lemma is_renaming_left_id_subst_right_id_subst:
   "is_renaming r \<Longrightarrow> s \<odot> r = id_subst \<Longrightarrow> r \<odot> s = id_subst"
   by (metis comp_subst_assoc comp_subst_id_subst is_renaming_def)
 
 lemma is_renaming_closure: "is_renaming r1 \<Longrightarrow> is_renaming r2 \<Longrightarrow> is_renaming (r1 \<odot> r2)"
   unfolding is_renaming_def by (metis comp_subst_assoc comp_subst_id_subst)
 
 lemma is_renaming_inv_renaming_cancel_atm[simp]: "is_renaming \<rho> \<Longrightarrow> A \<cdot>a \<rho> \<cdot>a inv_renaming \<rho> = A"
   by (metis inv_renaming_cancel_r subst_atm_comp_subst subst_atm_id_subst)
 
 lemma is_renaming_inv_renaming_cancel_atms[simp]: "is_renaming \<rho> \<Longrightarrow> AA \<cdot>as \<rho> \<cdot>as inv_renaming \<rho> = AA"
   by (metis inv_renaming_cancel_r subst_atms_comp_subst subst_atms_id_subst)
 
 lemma is_renaming_inv_renaming_cancel_atmss[simp]: "is_renaming \<rho> \<Longrightarrow> AAA \<cdot>ass \<rho> \<cdot>ass inv_renaming \<rho> = AAA"
   by (metis inv_renaming_cancel_r subst_atmss_comp_subst subst_atmss_id_subst)
 
 lemma is_renaming_inv_renaming_cancel_atm_list[simp]: "is_renaming \<rho> \<Longrightarrow> As \<cdot>al \<rho> \<cdot>al inv_renaming \<rho> = As"
   by (metis inv_renaming_cancel_r subst_atm_list_comp_subst subst_atm_list_id_subst)
 
 lemma is_renaming_inv_renaming_cancel_atm_mset[simp]: "is_renaming \<rho> \<Longrightarrow> AA \<cdot>am \<rho> \<cdot>am inv_renaming \<rho> = AA"
   by (metis inv_renaming_cancel_r subst_atm_mset_comp_subst subst_atm_mset_id_subst)
 
 lemma is_renaming_inv_renaming_cancel_atm_mset_list[simp]: "is_renaming \<rho> \<Longrightarrow> (AAs \<cdot>aml \<rho>) \<cdot>aml inv_renaming \<rho> = AAs"
   by (metis inv_renaming_cancel_r subst_atm_mset_list_comp_subst subst_atm_mset_list_id_subst)
 
 lemma is_renaming_list_inv_renaming_cancel_atm_mset_lists[simp]:
   "length AAs = length \<rho>s \<Longrightarrow> is_renaming_list \<rho>s \<Longrightarrow> AAs \<cdot>\<cdot>aml \<rho>s \<cdot>\<cdot>aml map inv_renaming \<rho>s = AAs"
   by (metis inv_renaming_cancel_r_list subst_atm_mset_lists_comp_substs
       subst_atm_mset_lists_id_subst)
 
 lemma is_renaming_inv_renaming_cancel_lit[simp]: "is_renaming \<rho> \<Longrightarrow> (L \<cdot>l \<rho>) \<cdot>l inv_renaming \<rho> = L"
   by (metis inv_renaming_cancel_r subst_lit_comp_subst subst_lit_id_subst)
 
 lemma is_renaming_inv_renaming_cancel_cls[simp]: "is_renaming \<rho> \<Longrightarrow> C  \<cdot> \<rho> \<cdot> inv_renaming \<rho> = C"
   by (metis inv_renaming_cancel_r subst_cls_comp_subst subst_cls_id_subst)
 
 lemma is_renaming_inv_renaming_cancel_clss[simp]:
   "is_renaming \<rho> \<Longrightarrow> CC \<cdot>cs \<rho> \<cdot>cs inv_renaming \<rho> = CC"
   by (metis inv_renaming_cancel_r subst_clss_id_subst subst_clsscomp_subst)
 
 lemma is_renaming_inv_renaming_cancel_cls_list[simp]:
   "is_renaming \<rho> \<Longrightarrow> Cs \<cdot>cl \<rho> \<cdot>cl inv_renaming \<rho> = Cs"
   by (metis inv_renaming_cancel_r subst_cls_list_comp_subst subst_cls_list_id_subst)
 
 lemma is_renaming_list_inv_renaming_cancel_cls_list[simp]:
   "length Cs = length \<rho>s \<Longrightarrow> is_renaming_list \<rho>s \<Longrightarrow> Cs \<cdot>\<cdot>cl \<rho>s \<cdot>\<cdot>cl map inv_renaming \<rho>s = Cs"
   by (metis inv_renaming_cancel_r_list subst_cls_lists_comp_substs subst_cls_lists_id_subst)
 
 lemma is_renaming_inv_renaming_cancel_cls_mset[simp]:
   "is_renaming \<rho> \<Longrightarrow> CC \<cdot>cm \<rho> \<cdot>cm inv_renaming \<rho> = CC"
   by (metis inv_renaming_cancel_r subst_cls_mset_comp_subst subst_cls_mset_id_subst)
 
 
 subsubsection \<open>Monotonicity\<close>
 
 lemma subst_cls_mono: "set_mset C \<subseteq> set_mset D \<Longrightarrow> set_mset (C \<cdot> \<sigma>) \<subseteq> set_mset (D \<cdot> \<sigma>)"
   by force
 
 lemma subst_cls_mono_mset: "C \<subseteq># D \<Longrightarrow> C \<cdot> \<sigma> \<subseteq># D \<cdot> \<sigma>"
   unfolding subst_clss_def by (metis mset_subset_eq_exists_conv subst_cls_union)
 
 lemma subst_subset_mono: "D \<subset># C \<Longrightarrow> D \<cdot> \<sigma> \<subset># C \<cdot> \<sigma>"
   unfolding subst_cls_def by (simp add: image_mset_subset_mono)
 
 
 subsubsection \<open>Size after Substitution\<close>
 
 lemma size_subst[simp]: "size (D \<cdot> \<sigma>) = size D"
   unfolding subst_cls_def by auto
 
 lemma subst_atm_list_length[simp]: "length (As \<cdot>al \<sigma>) = length As"
   unfolding subst_atm_list_def by auto
 
 lemma length_subst_atm_mset_list[simp]: "length (AAs \<cdot>aml \<eta>) = length AAs"
   unfolding subst_atm_mset_list_def by auto
 
 lemma subst_atm_mset_lists_length[simp]: "length (AAs \<cdot>\<cdot>aml \<sigma>s) = min (length AAs) (length \<sigma>s)"
   unfolding subst_atm_mset_lists_def by auto
 
 lemma subst_cls_list_length[simp]: "length (Cs \<cdot>cl \<sigma>) = length Cs"
   unfolding subst_cls_list_def by auto
 
 lemma comp_substs_length[simp]: "length (\<tau>s \<odot>s \<sigma>s) = min (length \<tau>s) (length \<sigma>s)"
   unfolding comp_substs_def by auto
 
 lemma subst_cls_lists_length[simp]: "length (Cs \<cdot>\<cdot>cl \<sigma>s) = min (length Cs) (length \<sigma>s)"
   unfolding subst_cls_lists_def by auto
 
 
 subsubsection \<open>Variable Disjointness\<close>
 
 lemma var_disjoint_clauses:
   assumes "var_disjoint Cs"
   shows "\<forall>\<sigma>s. length \<sigma>s = length Cs \<longrightarrow> (\<exists>\<tau>. Cs \<cdot>\<cdot>cl \<sigma>s = Cs \<cdot>cl \<tau>)"
 proof clarify
   fix \<sigma>s :: "'s list"
   assume a: "length \<sigma>s = length Cs"
   then obtain \<tau> where "\<forall>i < length Cs. \<forall>S. S \<subseteq># Cs ! i \<longrightarrow> S \<cdot> \<sigma>s ! i = S \<cdot> \<tau>"
     using assms unfolding var_disjoint_def by blast
   then have "\<forall>i < length Cs. (Cs ! i) \<cdot> \<sigma>s ! i = (Cs ! i) \<cdot> \<tau>"
     by auto
   then have "Cs \<cdot>\<cdot>cl \<sigma>s = Cs \<cdot>cl \<tau>"
     using a by (auto intro: nth_equalityI)
   then show "\<exists>\<tau>. Cs \<cdot>\<cdot>cl \<sigma>s = Cs \<cdot>cl \<tau>"
     by auto
 qed
 
 
 subsubsection \<open>Ground Expressions and Substitutions\<close>
 
 lemma ex_ground_subst: "\<exists>\<sigma>. is_ground_subst \<sigma>"
   using make_ground_subst[of "{#}"]
   by (simp add: is_ground_cls_def)
 
 lemma is_ground_cls_list_Cons[simp]:
   "is_ground_cls_list (C # Cs) = (is_ground_cls C \<and> is_ground_cls_list Cs)"
   unfolding is_ground_cls_list_def by auto
 
 
 paragraph \<open>Ground union\<close>
 
 lemma is_ground_atms_union[simp]: "is_ground_atms (AA \<union> BB) \<longleftrightarrow> is_ground_atms AA \<and> is_ground_atms BB"
   unfolding is_ground_atms_def by auto
 
 lemma is_ground_atm_mset_union[simp]:
   "is_ground_atm_mset (AA + BB) \<longleftrightarrow> is_ground_atm_mset AA \<and> is_ground_atm_mset BB"
   unfolding is_ground_atm_mset_def by auto
 
 lemma is_ground_cls_union[simp]: "is_ground_cls (C + D) \<longleftrightarrow> is_ground_cls C \<and> is_ground_cls D"
   unfolding is_ground_cls_def by auto
 
 lemma is_ground_clss_union[simp]:
   "is_ground_clss (CC \<union> DD) \<longleftrightarrow> is_ground_clss CC \<and> is_ground_clss DD"
   unfolding is_ground_clss_def by auto
 
 lemma is_ground_cls_list_is_ground_cls_sum_list[simp]:
   "is_ground_cls_list Cs \<Longrightarrow> is_ground_cls (sum_list Cs)"
   by (meson in_mset_sum_list2 is_ground_cls_def is_ground_cls_list_def)
 
 
 paragraph \<open>Grounding monotonicity\<close>
 
 lemma is_ground_cls_mono: "C \<subseteq># D \<Longrightarrow> is_ground_cls D \<Longrightarrow> is_ground_cls C"
   unfolding is_ground_cls_def by (metis set_mset_mono subsetD)
 
 lemma is_ground_clss_mono: "CC \<subseteq> DD \<Longrightarrow> is_ground_clss DD \<Longrightarrow> is_ground_clss CC"
   unfolding is_ground_clss_def by blast
 
 lemma grounding_of_clss_mono: "CC \<subseteq> DD \<Longrightarrow> grounding_of_clss CC \<subseteq> grounding_of_clss DD"
   using grounding_of_clss_def by auto
 
 lemma sum_list_subseteq_mset_is_ground_cls_list[simp]:
   "sum_list Cs \<subseteq># sum_list Ds \<Longrightarrow> is_ground_cls_list Ds \<Longrightarrow> is_ground_cls_list Cs"
   by (meson in_mset_sum_list is_ground_cls_def is_ground_cls_list_is_ground_cls_sum_list
       is_ground_cls_mono is_ground_cls_list_def)
 
 
 paragraph \<open>Substituting on ground expression preserves ground\<close>
 
 lemma is_ground_comp_subst[simp]: "is_ground_subst \<sigma> \<Longrightarrow> is_ground_subst (\<tau> \<odot> \<sigma>)"
   unfolding is_ground_subst_def is_ground_atm_def by auto
 
 lemma ground_subst_ground_atm[simp]: "is_ground_subst \<sigma> \<Longrightarrow> is_ground_atm (A \<cdot>a \<sigma>)"
   by (simp add: is_ground_subst_def)
 
 lemma ground_subst_ground_lit[simp]: "is_ground_subst \<sigma> \<Longrightarrow> is_ground_lit (L \<cdot>l \<sigma>)"
   unfolding is_ground_lit_def subst_lit_def by (cases L) auto
 
 lemma ground_subst_ground_cls[simp]: "is_ground_subst \<sigma> \<Longrightarrow> is_ground_cls (C \<cdot> \<sigma>)"
   unfolding is_ground_cls_def by auto
 
 lemma ground_subst_ground_clss[simp]: "is_ground_subst \<sigma> \<Longrightarrow> is_ground_clss (CC \<cdot>cs \<sigma>)"
   unfolding is_ground_clss_def subst_clss_def by auto
 
 lemma ground_subst_ground_cls_list[simp]: "is_ground_subst \<sigma> \<Longrightarrow> is_ground_cls_list (Cs \<cdot>cl \<sigma>)"
   unfolding is_ground_cls_list_def subst_cls_list_def by auto
 
 lemma ground_subst_ground_cls_lists[simp]:
   "\<forall>\<sigma> \<in> set \<sigma>s. is_ground_subst \<sigma> \<Longrightarrow> is_ground_cls_list (Cs \<cdot>\<cdot>cl \<sigma>s)"
   unfolding is_ground_cls_list_def subst_cls_lists_def by (auto simp: set_zip)
 
+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
 
 paragraph \<open>Substituting on ground expression has no effect\<close>
 
 lemma is_ground_subst_atm[simp]: "is_ground_atm A \<Longrightarrow> A \<cdot>a \<sigma> = A"
   unfolding is_ground_atm_def by simp
 
 lemma is_ground_subst_atms[simp]: "is_ground_atms AA \<Longrightarrow> AA \<cdot>as \<sigma> = AA"
   unfolding is_ground_atms_def subst_atms_def image_def by auto
 
 lemma is_ground_subst_atm_mset[simp]: "is_ground_atm_mset AA \<Longrightarrow> AA \<cdot>am \<sigma> = AA"
   unfolding is_ground_atm_mset_def subst_atm_mset_def by auto
 
 lemma is_ground_subst_atm_list[simp]: "is_ground_atm_list As \<Longrightarrow> As \<cdot>al \<sigma> = As"
   unfolding is_ground_atm_list_def subst_atm_list_def by (auto intro: nth_equalityI)
 
 lemma is_ground_subst_atm_list_member[simp]:
   "is_ground_atm_list As \<Longrightarrow> i < length As \<Longrightarrow> As ! i \<cdot>a \<sigma> = As ! i"
   unfolding is_ground_atm_list_def by auto
 
 lemma is_ground_subst_lit[simp]: "is_ground_lit L \<Longrightarrow> L \<cdot>l \<sigma> = L"
   unfolding is_ground_lit_def subst_lit_def by (cases L) simp_all
 
 lemma is_ground_subst_cls[simp]: "is_ground_cls C \<Longrightarrow> C \<cdot> \<sigma> = C"
   unfolding is_ground_cls_def subst_cls_def by simp
 
 lemma is_ground_subst_clss[simp]: "is_ground_clss CC \<Longrightarrow> CC \<cdot>cs \<sigma> = CC"
   unfolding is_ground_clss_def subst_clss_def image_def by auto
 
 lemma is_ground_subst_cls_lists[simp]:
   assumes "length P = length Cs" and "is_ground_cls_list Cs"
   shows "Cs \<cdot>\<cdot>cl P = Cs"
   using assms by (metis is_ground_cls_list_def is_ground_subst_cls min.idem nth_equalityI nth_mem
       subst_cls_lists_nth subst_cls_lists_length)
 
 lemma is_ground_subst_lit_iff: "is_ground_lit L \<longleftrightarrow> (\<forall>\<sigma>. L = L \<cdot>l \<sigma>)"
   using is_ground_atm_def is_ground_lit_def subst_lit_def by (cases L) auto
 
 lemma is_ground_subst_cls_iff: "is_ground_cls C \<longleftrightarrow> (\<forall>\<sigma>. C = C \<cdot> \<sigma>)"
   by (metis ex_ground_subst ground_subst_ground_cls is_ground_subst_cls)
 
 
 paragraph \<open>Members of ground expressions are ground\<close>
 
 lemma is_ground_cls_as_atms: "is_ground_cls C \<longleftrightarrow> (\<forall>A \<in> atms_of C. is_ground_atm A)"
   by (auto simp: atms_of_def is_ground_cls_def is_ground_lit_def)
 
 lemma is_ground_cls_imp_is_ground_lit: "L \<in># C \<Longrightarrow> is_ground_cls C \<Longrightarrow> is_ground_lit L"
   by (simp add: is_ground_cls_def)
 
 lemma is_ground_cls_imp_is_ground_atm: "A \<in> atms_of C \<Longrightarrow> is_ground_cls C \<Longrightarrow> is_ground_atm A"
   by (simp add: is_ground_cls_as_atms)
 
 lemma is_ground_cls_is_ground_atms_atms_of[simp]: "is_ground_cls C \<Longrightarrow> is_ground_atms (atms_of C)"
   by (simp add: is_ground_cls_imp_is_ground_atm is_ground_atms_def)
 
 lemma grounding_ground: "C \<in> grounding_of_clss M \<Longrightarrow> is_ground_cls C"
   unfolding grounding_of_clss_def grounding_of_cls_def by auto
 
 lemma in_subset_eq_grounding_of_clss_is_ground_cls[simp]:
   "C \<in> CC \<Longrightarrow> CC \<subseteq> grounding_of_clss DD \<Longrightarrow> is_ground_cls C"
   unfolding grounding_of_clss_def grounding_of_cls_def by auto
 
 lemma is_ground_cls_empty[simp]: "is_ground_cls {#}"
   unfolding is_ground_cls_def by simp
 
 lemma grounding_of_cls_ground: "is_ground_cls C \<Longrightarrow> grounding_of_cls C = {C}"
   unfolding grounding_of_cls_def by (simp add: ex_ground_subst)
 
 lemma grounding_of_cls_empty[simp]: "grounding_of_cls {#} = {{#}}"
   by (simp add: grounding_of_cls_ground)
 
 
 paragraph \<open>Grounding idempotence\<close>
 
 lemma grounding_of_grounding_of_cls: "E \<in> grounding_of_cls D \<Longrightarrow> D \<in> grounding_of_cls C \<Longrightarrow> E = D"
   using grounding_of_cls_def by auto
 
 
 subsubsection \<open>Subsumption\<close>
 
 lemma subsumes_empty_left[simp]: "subsumes {#} C"
   unfolding subsumes_def subst_cls_def by simp
 
 lemma strictly_subsumes_empty_left[simp]: "strictly_subsumes {#} C \<longleftrightarrow> C \<noteq> {#}"
   unfolding strictly_subsumes_def subsumes_def subst_cls_def by simp
 
 
 subsubsection \<open>Unifiers\<close>
 
 lemma card_le_one_alt: "finite X \<Longrightarrow> card X \<le> 1 \<longleftrightarrow> X = {} \<or> (\<exists>x. X = {x})"
   by (induct rule: finite_induct) auto
 
 lemma is_unifier_subst_atm_eqI:
   assumes "finite AA"
   shows "is_unifier \<sigma> AA \<Longrightarrow> A \<in> AA \<Longrightarrow> B \<in> AA \<Longrightarrow> A \<cdot>a \<sigma> = B \<cdot>a \<sigma>"
   unfolding is_unifier_def subst_atms_def card_le_one_alt[OF finite_imageI[OF assms]]
   by (metis equals0D imageI insert_iff)
 
 lemma is_unifier_alt:
   assumes "finite AA"
   shows "is_unifier \<sigma> AA \<longleftrightarrow> (\<forall>A \<in> AA. \<forall>B \<in> AA. A \<cdot>a \<sigma> = B \<cdot>a \<sigma>)"
   unfolding is_unifier_def subst_atms_def card_le_one_alt[OF finite_imageI[OF assms(1)]]
   by (rule iffI, metis empty_iff insert_iff insert_image, blast)
 
 lemma is_unifiers_subst_atm_eqI:
   assumes "finite AA" "is_unifiers \<sigma> AAA" "AA \<in> AAA" "A \<in> AA" "B \<in> AA"
   shows "A \<cdot>a \<sigma> = B \<cdot>a \<sigma>"
   by (metis assms is_unifiers_def is_unifier_subst_atm_eqI)
 
 theorem is_unifiers_comp:
   "is_unifiers \<sigma> (set_mset ` set (map2 add_mset As Bs) \<cdot>ass \<eta>) \<longleftrightarrow>
    is_unifiers (\<eta> \<odot> \<sigma>) (set_mset ` set (map2 add_mset As Bs))"
   unfolding is_unifiers_def is_unifier_def subst_atmss_def by auto
 
 
 subsubsection \<open>Most General Unifier\<close>
 
 lemma is_mgu_is_unifiers: "is_mgu \<sigma> AAA \<Longrightarrow> is_unifiers \<sigma> AAA"
   using is_mgu_def by blast
 
 lemma is_mgu_is_most_general: "is_mgu \<sigma> AAA \<Longrightarrow> is_unifiers \<tau> AAA \<Longrightarrow> \<exists>\<gamma>. \<tau> = \<sigma> \<odot> \<gamma>"
   using is_mgu_def by blast
 
 lemma is_unifiers_is_unifier: "is_unifiers \<sigma> AAA \<Longrightarrow> AA \<in> AAA \<Longrightarrow> is_unifier \<sigma> AA"
   using is_unifiers_def by simp
 
 
 subsubsection \<open>Generalization and Subsumption\<close>
 
+lemma variants_sym: "variants D D' \<longleftrightarrow> variants D' D"
+  unfolding variants_def by auto
+
 lemma variants_iff_subsumes: "variants C D \<longleftrightarrow> subsumes C D \<and> subsumes D C"
 proof
   assume "variants C D"
   then show "subsumes C D \<and> subsumes D C"
     unfolding variants_def generalizes_def subsumes_def by (metis subset_mset.order.refl)
 next
   assume sub: "subsumes C D \<and> subsumes D C"
   then have "size C = size D"
     unfolding subsumes_def by (metis antisym size_mset_mono size_subst)
   then show "variants C D"
     using sub unfolding subsumes_def variants_def generalizes_def
     by (metis leD mset_subset_size size_mset_mono size_subst
         subset_mset.order.not_eq_order_implies_strict)
 qed
 
 lemma wf_strictly_generalizes: "wfP strictly_generalizes"
 proof -
   {
     assume "\<exists>C_at. \<forall>i. strictly_generalizes (C_at (Suc i)) (C_at i)"
     then obtain C_at :: "nat \<Rightarrow> 'a clause" where
       sg_C: "\<And>i. strictly_generalizes (C_at (Suc i)) (C_at i)"
       by blast
 
     define n :: nat where
       "n = size (C_at 0)"
 
     have sz_C: "size (C_at i) = n" for i
     proof (induct i)
       case (Suc i)
       then show ?case
         using sg_C[of i] unfolding strictly_generalizes_def generalizes_def subst_cls_def
         by (metis size_image_mset)
     qed (simp add: n_def)
 
     obtain \<sigma>_at :: "nat \<Rightarrow> 's" where
       C_\<sigma>: "\<And>i. image_mset (\<lambda>L. L \<cdot>l \<sigma>_at i) (C_at (Suc i)) = C_at i"
       using sg_C[unfolded strictly_generalizes_def generalizes_def subst_cls_def] by metis
 
     define Ls_at :: "nat \<Rightarrow> 'a literal list" where
       "Ls_at = rec_nat (SOME Ls. mset Ls = C_at 0)
          (\<lambda>i Lsi. SOME Ls. mset Ls = C_at (Suc i) \<and> map (\<lambda>L. L \<cdot>l \<sigma>_at i) Ls = Lsi)"
 
     have
       Ls_at_0: "Ls_at 0 = (SOME Ls. mset Ls = C_at 0)" and
       Ls_at_Suc: "\<And>i. Ls_at (Suc i) =
         (SOME Ls. mset Ls = C_at (Suc i) \<and> map (\<lambda>L. L \<cdot>l \<sigma>_at i) Ls = Ls_at i)"
       unfolding Ls_at_def by simp+
 
     have mset_Lt_at_0: "mset (Ls_at 0) = C_at 0"
       unfolding Ls_at_0 by (rule someI_ex) (metis list_of_mset_exi)
 
     have "mset (Ls_at (Suc i)) = C_at (Suc i) \<and> map (\<lambda>L. L \<cdot>l \<sigma>_at i) (Ls_at (Suc i)) = Ls_at i"
       for i
     proof (induct i)
       case 0
       then show ?case
         by (simp add: Ls_at_Suc, rule someI_ex,
             metis C_\<sigma> image_mset_of_subset_list mset_Lt_at_0)
     next
       case Suc
       then show ?case
         by (subst (1 2) Ls_at_Suc) (rule someI_ex, metis C_\<sigma> image_mset_of_subset_list)
     qed
     note mset_Ls = this[THEN conjunct1] and Ls_\<sigma> = this[THEN conjunct2]
 
     have len_Ls: "\<And>i. length (Ls_at i) = n"
       by (metis mset_Ls mset_Lt_at_0 not0_implies_Suc size_mset sz_C)
 
     have is_pos_Ls: "\<And>i j. j < n \<Longrightarrow> is_pos (Ls_at (Suc i) ! j) \<longleftrightarrow> is_pos (Ls_at i ! j)"
       using Ls_\<sigma> len_Ls by (metis literal.map_disc_iff nth_map subst_lit_def)
 
     have Ls_\<tau>_strict_lit: "\<And>i \<tau>. map (\<lambda>L. L \<cdot>l \<tau>) (Ls_at i) \<noteq> Ls_at (Suc i)"
       by (metis C_\<sigma> mset_Ls Ls_\<sigma> mset_map sg_C generalizes_def strictly_generalizes_def
           subst_cls_def)
 
     have Ls_\<tau>_strict_tm:
       "map ((\<lambda>t. t \<cdot>a \<tau>) \<circ> atm_of) (Ls_at i) \<noteq> map atm_of (Ls_at (Suc i))" for i \<tau>
     proof -
       obtain j :: nat where
         j_lt: "j < n" and
         j_\<tau>: "Ls_at i ! j \<cdot>l \<tau> \<noteq> Ls_at (Suc i) ! j"
         using Ls_\<tau>_strict_lit[of \<tau> i] len_Ls
         by (metis (no_types, lifting) length_map list_eq_iff_nth_eq nth_map)
 
       have "atm_of (Ls_at i ! j) \<cdot>a \<tau> \<noteq> atm_of (Ls_at (Suc i) ! j)"
         using j_\<tau> is_pos_Ls[OF j_lt]
         by (metis (mono_guards) literal.expand literal.map_disc_iff literal.map_sel subst_lit_def)
       then show ?thesis
         using j_lt len_Ls by (metis nth_map o_apply)
     qed
 
     define tm_at :: "nat \<Rightarrow> 'a" where
       "\<And>i. tm_at i = atm_of_atms (map atm_of (Ls_at i))"
 
     have "\<And>i. generalizes_atm (tm_at (Suc i)) (tm_at i)"
       unfolding tm_at_def generalizes_atm_def atm_of_atms_subst
       using Ls_\<sigma>[THEN arg_cong, of "map atm_of"] by (auto simp: comp_def)
     moreover have "\<And>i. \<not> generalizes_atm (tm_at i) (tm_at (Suc i))"
       unfolding tm_at_def generalizes_atm_def atm_of_atms_subst by (simp add: Ls_\<tau>_strict_tm)
     ultimately have "\<And>i. strictly_generalizes_atm (tm_at (Suc i)) (tm_at i)"
       unfolding strictly_generalizes_atm_def by blast
     then have False
       using wf_strictly_generalizes_atm[unfolded wfP_def wf_iff_no_infinite_down_chain] by blast
   }
   then show "wfP (strictly_generalizes :: 'a clause \<Rightarrow> _ \<Rightarrow> _)"
     unfolding wfP_def by (blast intro: wf_iff_no_infinite_down_chain[THEN iffD2])
 qed
 
 lemma strict_subset_subst_strictly_subsumes: "C \<cdot> \<eta> \<subset># D \<Longrightarrow> strictly_subsumes C D"
   by (metis leD mset_subset_size size_mset_mono size_subst strictly_subsumes_def
       subset_mset.dual_order.strict_implies_order substitution_ops.subsumes_def)
 
 lemma generalizes_refl: "generalizes C C"
   unfolding generalizes_def by (rule exI[of _ id_subst]) auto
 
 lemma generalizes_trans: "generalizes C D \<Longrightarrow> generalizes D E \<Longrightarrow> generalizes C E"
   unfolding generalizes_def using subst_cls_comp_subst by blast
 
 lemma subsumes_refl: "subsumes C C"
   unfolding subsumes_def by (rule exI[of _ id_subst]) auto
 
 lemma subsumes_trans: "subsumes C D \<Longrightarrow> subsumes D E \<Longrightarrow> subsumes C E"
   unfolding subsumes_def
   by (metis (no_types) subset_mset.order.trans subst_cls_comp_subst subst_cls_mono_mset)
 
 lemma strictly_generalizes_irrefl: "\<not> strictly_generalizes C C"
   unfolding strictly_generalizes_def by blast
 
 lemma strictly_generalizes_antisym: "strictly_generalizes C D \<Longrightarrow> \<not> strictly_generalizes D C"
   unfolding strictly_generalizes_def by blast
 
 lemma strictly_generalizes_trans:
   "strictly_generalizes C D \<Longrightarrow> strictly_generalizes D E \<Longrightarrow> strictly_generalizes C E"
   unfolding strictly_generalizes_def using generalizes_trans by blast
 
 lemma strictly_subsumes_irrefl: "\<not> strictly_subsumes C C"
   unfolding strictly_subsumes_def by blast
 
 lemma strictly_subsumes_antisym: "strictly_subsumes C D \<Longrightarrow> \<not> strictly_subsumes D C"
   unfolding strictly_subsumes_def by blast
 
 lemma strictly_subsumes_trans:
   "strictly_subsumes C D \<Longrightarrow> strictly_subsumes D E \<Longrightarrow> strictly_subsumes C E"
   unfolding strictly_subsumes_def using subsumes_trans by blast
 
 lemma subset_strictly_subsumes: "C \<subset># D \<Longrightarrow> strictly_subsumes C D"
   using strict_subset_subst_strictly_subsumes[of C id_subst] by auto
 
 lemma strictly_generalizes_neq: "strictly_generalizes D' D \<Longrightarrow> D' \<noteq> D \<cdot> \<sigma>"
   unfolding strictly_generalizes_def generalizes_def by blast
 
 lemma strictly_subsumes_neq: "strictly_subsumes D' D \<Longrightarrow> D' \<noteq> D \<cdot> \<sigma>"
   unfolding strictly_subsumes_def subsumes_def by blast
 
 lemma strictly_subsumes_has_minimum:
   assumes "CC \<noteq> {}"
   shows "\<exists>C \<in> CC. \<forall>D \<in> CC. \<not> strictly_subsumes D C"
 proof (rule ccontr)
   assume "\<not> (\<exists>C \<in> CC. \<forall>D\<in>CC. \<not> strictly_subsumes D C)"
   then have "\<forall>C \<in> CC. \<exists>D \<in> CC. strictly_subsumes D C"
     by blast
   then obtain f where
     f_p: "\<forall>C \<in> CC. f C \<in> CC \<and> strictly_subsumes (f C) C"
     by metis
   from assms obtain C where
     C_p: "C \<in> CC"
     by auto
 
   define c :: "nat \<Rightarrow> 'a clause" where
     "\<And>n. c n = (f ^^ n) C"
 
   have incc: "c i \<in> CC" for i
     by (induction i) (auto simp: c_def f_p C_p)
   have ps: "\<forall>i. strictly_subsumes (c (Suc i)) (c i)"
     using incc f_p unfolding c_def by auto
   have "\<forall>i. size (c i) \<ge> size (c (Suc i))"
     using ps unfolding strictly_subsumes_def subsumes_def by (metis size_mset_mono size_subst)
   then have lte: "\<forall>i. (size \<circ> c) i \<ge> (size \<circ> c) (Suc i)"
     unfolding comp_def .
   then have "\<exists>l. \<forall>l' \<ge> l. size (c l') = size (c (Suc l'))"
     using f_Suc_decr_eventually_const comp_def by auto
   then obtain l where
     l_p: "\<forall>l' \<ge> l. size (c l') = size (c (Suc l'))"
     by metis
   then have "\<forall>l' \<ge> l. strictly_generalizes (c (Suc l')) (c l')"
     using ps unfolding strictly_generalizes_def generalizes_def
     by (metis size_subst less_irrefl strictly_subsumes_def mset_subset_size subset_mset_def
         subsumes_def strictly_subsumes_neq)
   then have "\<forall>i. strictly_generalizes (c (Suc i + l)) (c (i + l))"
     unfolding strictly_generalizes_def generalizes_def by auto
   then have "\<exists>f. \<forall>i. strictly_generalizes (f (Suc i)) (f i)"
     by (rule exI[of _ "\<lambda>x. c (x + l)"])
   then show False
     using wf_strictly_generalizes
       wf_iff_no_infinite_down_chain[of "{(x, y). strictly_generalizes x y}"]
     unfolding wfP_def by auto
 qed
 
 lemma wf_strictly_subsumes: "wfP strictly_subsumes"
   using strictly_subsumes_has_minimum by (metis equals0D wfP_eq_minimal)
 
+lemma variants_imp_exists_substitution: "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 strictly_subsumes_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_substitution 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_strictly_subsumes_variants:
+  assumes "\<not> strictly_subsumes E D" and "variants D D'"
+  shows "\<not> strictly_subsumes E D'"
+  using assms strictly_subsumes_variants variants_sym by auto
+
 end
 
 
 subsection \<open>Most General Unifiers\<close>
 
 locale mgu = substitution subst_atm id_subst comp_subst renamings_apart atm_of_atms
   for
     subst_atm :: "'a \<Rightarrow> 's \<Rightarrow> 'a" and
     id_subst :: 's and
     comp_subst :: "'s \<Rightarrow> 's \<Rightarrow> 's" and
     atm_of_atms :: "'a list \<Rightarrow> 'a" and
     renamings_apart :: "'a literal multiset list \<Rightarrow> 's list" +
   fixes
     mgu :: "'a set set \<Rightarrow> 's option"
   assumes
     mgu_sound: "finite AAA \<Longrightarrow> (\<forall>AA \<in> AAA. finite AA) \<Longrightarrow> mgu AAA = Some \<sigma> \<Longrightarrow> is_mgu \<sigma> AAA" and
     mgu_complete:
       "finite AAA \<Longrightarrow> (\<forall>AA \<in> AAA. finite AA) \<Longrightarrow> is_unifiers \<sigma> AAA \<Longrightarrow> \<exists>\<tau>. mgu AAA = Some \<tau>"
 begin
 
 lemmas is_unifiers_mgu = mgu_sound[unfolded is_mgu_def, THEN conjunct1]
 lemmas is_mgu_most_general = mgu_sound[unfolded is_mgu_def, THEN conjunct2]
 
 lemma mgu_unifier:
   assumes
     aslen: "length As = n" and
     aaslen: "length AAs = n" and
     mgu: "Some \<sigma> = mgu (set_mset ` set (map2 add_mset As AAs))" and
     i_lt: "i < n" and
     a_in: "A \<in># AAs ! i"
   shows "A \<cdot>a \<sigma> = As ! i \<cdot>a \<sigma>"
 proof -
   from mgu have "is_mgu \<sigma> (set_mset ` set (map2 add_mset As AAs))"
     using mgu_sound by auto
   then have "is_unifiers \<sigma> (set_mset ` set (map2 add_mset As AAs))"
     using is_mgu_is_unifiers by auto
   then have "is_unifier \<sigma> (set_mset (add_mset (As ! i) (AAs ! i)))"
     using i_lt aslen aaslen unfolding is_unifiers_def is_unifier_def
     by simp (metis length_zip min.idem nth_mem nth_zip prod.case set_mset_add_mset_insert)
   then show ?thesis
     using aslen aaslen a_in is_unifier_subst_atm_eqI
     by (metis finite_set_mset insertCI set_mset_add_mset_insert)
 qed
 
 end
 
 end
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,1301 +1,1414 @@
 (*  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>)"
+    less_atm_stable: "less_atm A B \<Longrightarrow> less_atm (A \<cdot>a \<sigma>) (B \<cdot>a \<sigma>)" and
+    less_atm_ground: "is_ground_atm A \<Longrightarrow> is_ground_atm B \<Longrightarrow> less_atm A B \<Longrightarrow> A < B"
 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
 
 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
 
 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
 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
     "\<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
 
 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>"
   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
       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
         \<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
     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 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"
     "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"
     "length \<eta>s = 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
     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
     fix i
     show "i<length (Cs0' \<cdot>cl \<eta>) \<Longrightarrow> (Cs0' \<cdot>cl \<eta>) ! i = Cs ! i"
     proof -
       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
     fix i
     show "i<length (AAs0' \<cdot>aml \<eta>) \<Longrightarrow> (AAs0' \<cdot>aml \<eta>) ! i = AAs ! i"
     proof -
       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>"
 
   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>)"
       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
 
   have \<open>length \<eta>s0 = 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> \<open>length CAs0 = length CAs\<close> \<open>length \<eta>s0 = length CAs\<close>
     by blast
 qed
 
+lemma ground_ord_resolve_ground:
+  assumes
+    select: "selection S" and
+    CAs_p: "ground_resolution_with_selection.ord_resolve S CAs DA AAs As E" and
+    ground_cas: "is_ground_cls_list CAs" and
+    ground_da: "is_ground_cls DA"
+  shows "is_ground_cls E"
+proof -
+  have a1: "atms_of E \<subseteq> (\<Union>CA \<in> set CAs. atms_of CA) \<union> atms_of DA"
+    using ground_resolution_with_selection.ord_resolve_atms_of_concl_subset[OF _ CAs_p]
+      ground_resolution_with_selection.intro[OF select] by blast
+  {
+    fix L :: "'a literal"
+    assume "L \<in># E"
+    then have "atm_of L \<in> atms_of E"
+      by (meson atm_of_lit_in_atms_of)
+    then have "is_ground_atm (atm_of L)"
+      using a1 ground_cas ground_da is_ground_cls_imp_is_ground_atm is_ground_cls_list_def
+      by auto
+  }
+  then show ?thesis
+    unfolding is_ground_cls_def is_ground_lit_def by simp
+qed
+
+lemma ground_ord_resolve_imp_ord_resolve:
+  assumes
+    ground_da: \<open>is_ground_cls DA\<close> and
+    ground_cas: \<open>is_ground_cls_list CAs\<close> and
+    gr: "ground_resolution_with_selection S_G" and
+    gr_res: \<open>ground_resolution_with_selection.ord_resolve S_G CAs DA AAs As E\<close>
+  shows \<open>\<exists>\<sigma>. ord_resolve S_G CAs DA AAs As \<sigma> E\<close>
+proof (cases rule: ground_resolution_with_selection.ord_resolve.cases[OF gr gr_res])
+  case (1 CAs n Cs AAs As D)
+  note cas = this(1) and da = this(2) and aas = this(3) and as = this(4) and e = this(5) and
+    cas_len = this(6) and cs_len = this(7) and aas_len = this(8) and as_len = this(9) and
+    nz = this(10) and casi = this(11) and aas_not_empt = this(12) and as_aas = this(13) and
+    eligibility = this(14) and str_max = this(15) and sel_empt = this(16)
+
+  have len_aas_len_as: "length AAs = length As"
+    using aas_len as_len by auto
+
+  from as_aas have "\<forall>i < n. \<forall>A \<in># add_mset (As ! i) (AAs ! i). A = As ! i"
+    by simp
+  then have "\<forall>i < n. card (set_mset (add_mset (As ! i) (AAs ! i))) \<le> Suc 0"
+    using all_the_same by metis
+  then have "\<forall>i < length AAs. card (set_mset (add_mset (As ! i) (AAs ! i))) \<le> Suc 0"
+    using aas_len by auto
+  then have "\<forall>AA \<in> set (map2 add_mset As AAs). card (set_mset AA) \<le> Suc 0"
+    using set_map2_ex[of AAs As add_mset, OF len_aas_len_as] by auto
+  then have "is_unifiers id_subst (set_mset ` set (map2 add_mset As AAs))"
+    unfolding is_unifiers_def is_unifier_def by auto
+  moreover have "finite (set_mset ` set (map2 add_mset As AAs))"
+    by auto
+  moreover have "\<forall>AA \<in> set_mset ` set (map2 add_mset As AAs). finite AA"
+    by auto
+  ultimately obtain \<sigma> where
+    \<sigma>_p: "Some \<sigma> = mgu (set_mset ` set (map2 add_mset As AAs))"
+    using mgu_complete by metis
+
+  have ground_elig: "ground_resolution_with_selection.eligible S_G As (D + negs (mset As))"
+    using eligibility by simp
+  have ground_cs: "\<forall>i < n. is_ground_cls (Cs ! i)"
+    using cas cas_len cs_len casi ground_cas nth_mem unfolding is_ground_cls_list_def by force
+  have ground_set_as: "is_ground_atms (set As)"
+    using da ground_da by (metis atms_of_negs is_ground_cls_is_ground_atms_atms_of
+        is_ground_cls_union set_mset_mset)
+  then have ground_mset_as: "is_ground_atm_mset (mset As)"
+    unfolding is_ground_atm_mset_def is_ground_atms_def by auto
+  have ground_as: "is_ground_atm_list As"
+    using ground_set_as is_ground_atm_list_def is_ground_atms_def by auto
+  have ground_d: "is_ground_cls D"
+    using ground_da da by simp
+
+  from as_len nz have atms:
+    "atms_of D \<union> set As \<noteq> {}"
+    "finite (atms_of D \<union> set As)"
+    by auto
+  then have "Max (atms_of D \<union> set As) \<in> atms_of D \<union> set As"
+    using Max_in by metis
+  then have is_ground_Max: "is_ground_atm (Max (atms_of D \<union> set As))"
+    using ground_d ground_mset_as is_ground_cls_imp_is_ground_atm
+    unfolding is_ground_atm_mset_def by auto
+
+  have "maximal_wrt (Max (atms_of D \<union> set As)) (D + negs (mset As))"
+    unfolding maximal_wrt_def
+    by clarsimp (metis atms Max_less_iff UnCI ground_d ground_set_as infinite_growing
+        is_ground_Max is_ground_atms_def is_ground_cls_imp_is_ground_atm less_atm_ground)
+  moreover have
+    "Max (atms_of D \<union> set As) \<cdot>a \<sigma> = Max (atms_of D \<union> set As)" and
+    "D \<cdot> \<sigma> + negs (mset As \<cdot>am \<sigma>) = D + negs (mset As)"
+    using ground_elig is_ground_Max ground_mset_as ground_d by auto
+  ultimately have fo_elig: "eligible S_G \<sigma> As (D + negs (mset As))"
+    using ground_elig unfolding ground_resolution_with_selection.eligible.simps[OF gr]
+      ground_resolution_with_selection.maximal_wrt_def[OF gr] eligible.simps
+    by auto
+
+  have "\<forall>i < n. strictly_maximal_wrt (As ! i) (Cs ! i)"
+    using str_max[unfolded ground_resolution_with_selection.strictly_maximal_wrt_def[OF gr]]
+      ground_as[unfolded is_ground_atm_list_def] ground_cs as_len less_atm_ground
+    unfolding strictly_maximal_wrt_def by clarsimp (fastforce simp: is_ground_cls_as_atms)+
+  then have ll: "\<forall>i < n. strictly_maximal_wrt (As ! i \<cdot>a \<sigma>) (Cs ! i \<cdot> \<sigma>)"
+    by (simp add: ground_as ground_cs as_len)
+
+  have ground_e: "is_ground_cls E"
+    using ground_d ground_cs cs_len unfolding e is_ground_cls_def
+    by simp (metis in_mset_sum_list2 in_set_conv_nth)
+
+  show ?thesis
+    using cas da aas as e ground_e ord_resolve.intros[OF cas_len cs_len aas_len as_len nz casi
+        aas_not_empt \<sigma>_p fo_elig ll sel_empt]
+    by auto
+qed
+
 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,1548 +1,1359 @@
 (*  Title:       An Ordered Resolution Prover for First-Order Clauses
     Author:      Anders Schlichtkrull <andschl at dtu.dk>, 2016, 2017
     Author:      Jasmin Blanchette <j.c.blanchette at vu.nl>, 2014, 2017
     Author:      Dmitriy Traytel <traytel at inf.ethz.ch>, 2014
     Maintainer:  Anders Schlichtkrull <andschl at dtu.dk>
 *)
 
 section \<open>An Ordered Resolution Prover for First-Order Clauses\<close>
 
 theory FO_Ordered_Resolution_Prover
   imports FO_Ordered_Resolution
 begin
 
 text \<open>
 This material is based on Section 4.3 (``A Simple Resolution Prover for First-Order Clauses'') of
 Bachmair and Ganzinger's chapter. Specifically, it formalizes the RP prover defined in Figure 5 and
 its related lemmas and theorems, including Lemmas 4.10 and 4.11 and Theorem 4.13 (completeness).
 \<close>
 
 definition is_least :: "(nat \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> bool" where
   "is_least P n \<longleftrightarrow> P n \<and> (\<forall>n' < n. \<not> P n')"
 
 lemma least_exists: "P n \<Longrightarrow> \<exists>n. is_least P n"
   using exists_least_iff unfolding is_least_def by auto
 
 text \<open>
 The following corresponds to page 42 and 43 of Section 4.3, from the explanation of RP to
 Lemma 4.10.
 \<close>
 
 type_synonym 'a state = "'a clause set \<times> 'a clause set \<times> 'a clause set"
 
 locale FO_resolution_prover =
   FO_resolution subst_atm id_subst comp_subst renamings_apart atm_of_atms mgu less_atm +
   selection S
   for
     S :: "('a :: wellorder) clause \<Rightarrow> 'a clause" and
     subst_atm :: "'a \<Rightarrow> 's \<Rightarrow> 'a" and
     id_subst :: "'s" and
     comp_subst :: "'s \<Rightarrow> 's \<Rightarrow> 's" and
     renamings_apart :: "'a clause list \<Rightarrow> 's list" and
     atm_of_atms :: "'a list \<Rightarrow> 'a" and
     mgu :: "'a set set \<Rightarrow> 's option" and
     less_atm :: "'a \<Rightarrow> 'a \<Rightarrow> bool" +
   assumes
-    sel_stable: "\<And>\<rho> C. is_renaming \<rho> \<Longrightarrow> S (C \<cdot> \<rho>) = S C \<cdot> \<rho>" and
-    less_atm_ground: "is_ground_atm A \<Longrightarrow> is_ground_atm B \<Longrightarrow> less_atm A B \<Longrightarrow> A < B"
+    sel_stable: "\<And>\<rho> C. is_renaming \<rho> \<Longrightarrow> S (C \<cdot> \<rho>) = S C \<cdot> \<rho>"
 begin
 
-lemma ground_ord_resolve_ground:
-  assumes
-    CAs_p: "ground_resolution_with_selection.ord_resolve S CAs DA AAs As E" and
-    ground_cas: "is_ground_cls_list CAs" and
-    ground_da: "is_ground_cls DA"
-  shows "is_ground_cls E"
-proof -
-  have a1: "atms_of E \<subseteq> (\<Union>CA \<in> set CAs. atms_of CA) \<union> atms_of DA"
-    using ground_resolution_with_selection.ord_resolve_atms_of_concl_subset[OF _ CAs_p]
-      ground_resolution_with_selection.intro selection_axioms by blast
-  {
-    fix L :: "'a literal"
-    assume "L \<in># E"
-    then have "atm_of L \<in> atms_of E"
-      by (meson atm_of_lit_in_atms_of)
-    then have "is_ground_atm (atm_of L)"
-      using a1 ground_cas ground_da is_ground_cls_imp_is_ground_atm is_ground_cls_list_def
-      by auto
-  }
-  then show ?thesis
-    unfolding is_ground_cls_def is_ground_lit_def by simp
-qed
-
-lemma ground_ord_resolve_imp_ord_resolve:
-  assumes
-    ground_da: \<open>is_ground_cls DA\<close> and
-    ground_cas: \<open>is_ground_cls_list CAs\<close> and
-    gr: "ground_resolution_with_selection S_G" and
-    gr_res: \<open>ground_resolution_with_selection.ord_resolve S_G CAs DA AAs As E\<close>
-  shows \<open>\<exists>\<sigma>. ord_resolve S_G CAs DA AAs As \<sigma> E\<close>
-proof (cases rule: ground_resolution_with_selection.ord_resolve.cases[OF gr gr_res])
-  case (1 CAs n Cs AAs As D)
-  note cas = this(1) and da = this(2) and aas = this(3) and as = this(4) and e = this(5) and
-    cas_len = this(6) and cs_len = this(7) and aas_len = this(8) and as_len = this(9) and
-    nz = this(10) and casi = this(11) and aas_not_empt = this(12) and as_aas = this(13) and
-    eligibility = this(14) and str_max = this(15) and sel_empt = this(16)
-
-  have len_aas_len_as: "length AAs = length As"
-    using aas_len as_len by auto
-
-  from as_aas have "\<forall>i < n. \<forall>A \<in># add_mset (As ! i) (AAs ! i). A = As ! i"
-    by simp
-  then have "\<forall>i < n. card (set_mset (add_mset (As ! i) (AAs ! i))) \<le> Suc 0"
-    using all_the_same by metis
-  then have "\<forall>i < length AAs. card (set_mset (add_mset (As ! i) (AAs ! i))) \<le> Suc 0"
-    using aas_len by auto
-  then have "\<forall>AA \<in> set (map2 add_mset As AAs). card (set_mset AA) \<le> Suc 0"
-    using set_map2_ex[of AAs As add_mset, OF len_aas_len_as] by auto
-  then have "is_unifiers id_subst (set_mset ` set (map2 add_mset As AAs))"
-    unfolding is_unifiers_def is_unifier_def by auto
-  moreover have "finite (set_mset ` set (map2 add_mset As AAs))"
-    by auto
-  moreover have "\<forall>AA \<in> set_mset ` set (map2 add_mset As AAs). finite AA"
-    by auto
-  ultimately obtain \<sigma> where
-    \<sigma>_p: "Some \<sigma> = mgu (set_mset ` set (map2 add_mset As AAs))"
-    using mgu_complete by metis
-
-  have ground_elig: "ground_resolution_with_selection.eligible S_G As (D + negs (mset As))"
-    using eligibility by simp
-  have ground_cs: "\<forall>i < n. is_ground_cls (Cs ! i)"
-    using cas cas_len cs_len casi ground_cas nth_mem unfolding is_ground_cls_list_def by force
-  have ground_set_as: "is_ground_atms (set As)"
-    using da ground_da by (metis atms_of_negs is_ground_cls_is_ground_atms_atms_of
-        is_ground_cls_union set_mset_mset)
-  then have ground_mset_as: "is_ground_atm_mset (mset As)"
-    unfolding is_ground_atm_mset_def is_ground_atms_def by auto
-  have ground_as: "is_ground_atm_list As"
-    using ground_set_as is_ground_atm_list_def is_ground_atms_def by auto
-  have ground_d: "is_ground_cls D"
-    using ground_da da by simp
-
-  from as_len nz have atms:
-    "atms_of D \<union> set As \<noteq> {}"
-    "finite (atms_of D \<union> set As)"
-    by auto
-  then have "Max (atms_of D \<union> set As) \<in> atms_of D \<union> set As"
-    using Max_in by metis
-  then have is_ground_Max: "is_ground_atm (Max (atms_of D \<union> set As))"
-    using ground_d ground_mset_as is_ground_cls_imp_is_ground_atm
-    unfolding is_ground_atm_mset_def by auto
-
-  have "maximal_wrt (Max (atms_of D \<union> set As)) (D + negs (mset As))"
-    unfolding maximal_wrt_def
-    by clarsimp (metis atms Max_less_iff UnCI ground_d ground_set_as infinite_growing
-        is_ground_Max is_ground_atms_def is_ground_cls_imp_is_ground_atm less_atm_ground)
-  moreover have
-    "Max (atms_of D \<union> set As) \<cdot>a \<sigma> = Max (atms_of D \<union> set As)" and
-    "D \<cdot> \<sigma> + negs (mset As \<cdot>am \<sigma>) = D + negs (mset As)"
-    using ground_elig is_ground_Max ground_mset_as ground_d by auto
-  ultimately have fo_elig: "eligible S_G \<sigma> As (D + negs (mset As))"
-    using ground_elig unfolding ground_resolution_with_selection.eligible.simps[OF gr]
-      ground_resolution_with_selection.maximal_wrt_def[OF gr] eligible.simps
-    by auto
-
-  have "\<forall>i < n. strictly_maximal_wrt (As ! i) (Cs ! i)"
-    using str_max[unfolded ground_resolution_with_selection.strictly_maximal_wrt_def[OF gr]]
-      ground_as[unfolded is_ground_atm_list_def] ground_cs as_len less_atm_ground
-    unfolding strictly_maximal_wrt_def by clarsimp (fastforce simp: is_ground_cls_as_atms)+
-  then have ll: "\<forall>i < n. strictly_maximal_wrt (As ! i \<cdot>a \<sigma>) (Cs ! i \<cdot> \<sigma>)"
-    by (simp add: ground_as ground_cs as_len)
-
-  have ground_e: "is_ground_cls E"
-    using ground_d ground_cs cs_len unfolding e is_ground_cls_def
-    by simp (metis in_mset_sum_list2 in_set_conv_nth)
-
-  show ?thesis
-    using cas da aas as e ground_e ord_resolve.intros[OF cas_len cs_len aas_len as_len nz casi
-        aas_not_empt \<sigma>_p fo_elig ll sel_empt]
-    by auto
-qed
-
 fun N_of_state :: "'a state \<Rightarrow> 'a clause set" where
   "N_of_state (N, P, Q) = N"
 
 fun P_of_state :: "'a state \<Rightarrow> 'a clause set" where
   "P_of_state (N, P, Q) = P"
 
 text \<open>
 \<open>O\<close> denotes relation composition in Isabelle, so the formalization uses \<open>Q\<close> instead.
 \<close>
 
 fun Q_of_state :: "'a state \<Rightarrow> 'a clause set" where
   "Q_of_state (N, P, Q) = Q"
 
 abbreviation clss_of_state :: "'a state \<Rightarrow> 'a clause set" where
   "clss_of_state St \<equiv> N_of_state St \<union> P_of_state St \<union> Q_of_state St"
 
 abbreviation grounding_of_state :: "'a state \<Rightarrow> 'a clause set" where
   "grounding_of_state St \<equiv> grounding_of_clss (clss_of_state St)"
 
 interpretation ord_FO_resolution: inference_system "ord_FO_\<Gamma> S" .
 
 text \<open>
 The following inductive predicate formalizes the resolution prover in Figure 5.
 \<close>
 
 inductive RP :: "'a state \<Rightarrow> 'a state \<Rightarrow> bool" (infix "\<leadsto>" 50) where
   tautology_deletion: "Neg A \<in># C \<Longrightarrow> Pos A \<in># C \<Longrightarrow> (N \<union> {C}, P, Q) \<leadsto> (N, P, Q)"
 | forward_subsumption: "D \<in> P \<union> Q \<Longrightarrow> subsumes D C \<Longrightarrow> (N \<union> {C}, P, Q) \<leadsto> (N, P, Q)"
 | backward_subsumption_P: "D \<in> N \<Longrightarrow> strictly_subsumes D C \<Longrightarrow> (N, P \<union> {C}, Q) \<leadsto> (N, P, Q)"
 | backward_subsumption_Q: "D \<in> N \<Longrightarrow> strictly_subsumes D C \<Longrightarrow> (N, P, Q \<union> {C}) \<leadsto> (N, P, Q)"
 | forward_reduction: "D + {#L'#} \<in> P \<union> Q \<Longrightarrow> - L = L' \<cdot>l \<sigma> \<Longrightarrow> D \<cdot> \<sigma> \<subseteq># C \<Longrightarrow>
     (N \<union> {C + {#L#}}, P, Q) \<leadsto> (N \<union> {C}, P, Q)"
 | backward_reduction_P: "D + {#L'#} \<in> N \<Longrightarrow> - L = L' \<cdot>l \<sigma> \<Longrightarrow> D \<cdot> \<sigma> \<subseteq># C \<Longrightarrow>
     (N, P \<union> {C + {#L#}}, Q) \<leadsto> (N, P \<union> {C}, Q)"
 | backward_reduction_Q: "D + {#L'#} \<in> N \<Longrightarrow> - L = L' \<cdot>l \<sigma> \<Longrightarrow> D \<cdot> \<sigma> \<subseteq># C \<Longrightarrow>
     (N, P, Q \<union> {C + {#L#}}) \<leadsto> (N, P \<union> {C}, Q)"
 | clause_processing: "(N \<union> {C}, P, Q) \<leadsto> (N, P \<union> {C}, Q)"
 | inference_computation: "N = concls_of (ord_FO_resolution.inferences_between Q C) \<Longrightarrow>
     ({}, P \<union> {C}, Q) \<leadsto> (N, P, Q \<union> {C})"
 
 lemma final_RP: "\<not> ({}, {}, Q) \<leadsto> St"
   by (auto elim: RP.cases)
 
 definition Sup_state :: "'a state llist \<Rightarrow> 'a state" where
   "Sup_state Sts =
    (Sup_llist (lmap N_of_state Sts), Sup_llist (lmap P_of_state Sts),
     Sup_llist (lmap Q_of_state Sts))"
 
 definition Liminf_state :: "'a state llist \<Rightarrow> 'a state" where
   "Liminf_state Sts =
    (Liminf_llist (lmap N_of_state Sts), Liminf_llist (lmap P_of_state Sts),
     Liminf_llist (lmap Q_of_state Sts))"
 
 context
   fixes Sts Sts' :: "'a state llist"
   assumes Sts: "lfinite Sts" "lfinite Sts'" "\<not> lnull Sts" "\<not> lnull Sts'" "llast Sts' = llast Sts"
 begin
 
 lemma
   N_of_Liminf_state_fin: "N_of_state (Liminf_state Sts') = N_of_state (Liminf_state Sts)" and
   P_of_Liminf_state_fin: "P_of_state (Liminf_state Sts') = P_of_state (Liminf_state Sts)" and
   Q_of_Liminf_state_fin: "Q_of_state (Liminf_state Sts') = Q_of_state (Liminf_state Sts)"
   using Sts by (simp_all add: Liminf_state_def lfinite_Liminf_llist llast_lmap)
 
 lemma Liminf_state_fin: "Liminf_state Sts' = Liminf_state Sts"
   using N_of_Liminf_state_fin P_of_Liminf_state_fin Q_of_Liminf_state_fin
   by (simp add: Liminf_state_def)
 
 end
 
 context
   fixes Sts Sts' :: "'a state llist"
   assumes Sts: "\<not> lfinite Sts" "emb Sts Sts'"
 begin
 
 lemma
   N_of_Liminf_state_inf: "N_of_state (Liminf_state Sts') \<subseteq> N_of_state (Liminf_state Sts)" and
   P_of_Liminf_state_inf: "P_of_state (Liminf_state Sts') \<subseteq> P_of_state (Liminf_state Sts)" and
   Q_of_Liminf_state_inf: "Q_of_state (Liminf_state Sts') \<subseteq> Q_of_state (Liminf_state Sts)"
   using Sts by (simp_all add: Liminf_state_def emb_Liminf_llist_infinite emb_lmap)
 
 lemma clss_of_Liminf_state_inf:
   "clss_of_state (Liminf_state Sts') \<subseteq> clss_of_state (Liminf_state Sts)"
   using N_of_Liminf_state_inf P_of_Liminf_state_inf Q_of_Liminf_state_inf by blast
 
 end
 
 definition fair_state_seq :: "'a state llist \<Rightarrow> bool" where
   "fair_state_seq Sts \<longleftrightarrow> N_of_state (Liminf_state Sts) = {} \<and> P_of_state (Liminf_state Sts) = {}"
 
 text \<open>
 The following formalizes Lemma 4.10.
 \<close>
 
 context
   fixes Sts :: "'a state llist"
 begin
 
 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"
+  sat_preserving_redundancy_criterion ground_sound_\<Gamma> sr.Rf sr_ext_Ri
   unfolding sat_preserving_redundancy_criterion_def sr_ext_Ri_def
   using sat_preserving_ground_sound_\<Gamma> redundancy_criterion_standard_extension gd_ord_\<Gamma>_ngd_ord_\<Gamma>
     sr.redundancy_criterion_axioms by auto
 
 lemma strict_subset_subsumption_redundant_clause:
   assumes
     sub: "D \<cdot> \<sigma> \<subset># C" and
     ground_\<sigma>: "is_ground_subst \<sigma>"
   shows "C \<in> sr.Rf (grounding_of_cls D)"
 proof -
   from sub have "\<forall>I. I \<Turnstile> D \<cdot> \<sigma> \<longrightarrow> I \<Turnstile> C"
     unfolding true_cls_def by blast
   moreover have "C > D \<cdot> \<sigma>"
     using sub by (simp add: subset_imp_less_mset)
   moreover have "D \<cdot> \<sigma> \<in> grounding_of_cls D"
     using ground_\<sigma> by (metis (mono_tags) mem_Collect_eq substitution_ops.grounding_of_cls_def)
   ultimately have "set_mset {#D \<cdot> \<sigma>#} \<subseteq> grounding_of_cls D"
     "(\<forall>I. I \<Turnstile>m {#D \<cdot> \<sigma>#} \<longrightarrow> I \<Turnstile> C)"
     "(\<forall>D'. D' \<in># {#D \<cdot> \<sigma>#} \<longrightarrow> D' < C)"
     by auto
   then show ?thesis
     using sr.Rf_def by blast
 qed
 
 lemma strict_subset_subsumption_redundant_clss:
   assumes
     "D \<cdot> \<sigma> \<subset># C" and
     "is_ground_subst \<sigma>" and
     "D \<in> CC"
   shows "C \<in> sr.Rf (grounding_of_clss CC)"
   using assms
 proof -
   have "C \<in> sr.Rf (grounding_of_cls D)"
     using strict_subset_subsumption_redundant_clause assms by auto
   then show ?thesis
     using assms unfolding grounding_of_clss_def
     by (metis (no_types) sr.Rf_mono sup_ge1 SUP_absorb contra_subsetD)
 qed
 
 lemma strict_subset_subsumption_grounding_redundant_clss:
   assumes
     D\<sigma>_subset_C: "D \<cdot> \<sigma> \<subset># C" and
     D_in_St: "D \<in> CC"
   shows "grounding_of_cls C \<subseteq> sr.Rf (grounding_of_clss CC)"
 proof
   fix C\<mu>
   assume "C\<mu> \<in> grounding_of_cls C"
   then obtain \<mu> where
     \<mu>_p: "C\<mu> = C \<cdot> \<mu> \<and> is_ground_subst \<mu>"
     unfolding grounding_of_cls_def by auto
   have D\<sigma>\<mu>C\<mu>: "D \<cdot> \<sigma> \<cdot> \<mu> \<subset># C \<cdot> \<mu>"
     using D\<sigma>_subset_C subst_subset_mono by auto
   then show "C\<mu> \<in> sr.Rf (grounding_of_clss CC)"
     using \<mu>_p strict_subset_subsumption_redundant_clss[of D "\<sigma> \<odot> \<mu>" "C \<cdot> \<mu>"] D_in_St by auto
 qed
 
-lemma subst_cls_eq_grounding_of_cls_subset_eq:
-  assumes "D \<cdot> \<sigma> = C"
-  shows "grounding_of_cls C \<subseteq> grounding_of_cls D"
-proof
-  fix C\<sigma>'
-  assume "C\<sigma>' \<in> grounding_of_cls C"
-  then obtain \<sigma>' where
-    C\<sigma>': "C \<cdot> \<sigma>' = C\<sigma>'" "is_ground_subst \<sigma>'"
-    unfolding grounding_of_cls_def by auto
-  then have "C \<cdot> \<sigma>' = D \<cdot> \<sigma> \<cdot> \<sigma>' \<and> is_ground_subst (\<sigma> \<odot> \<sigma>')"
-    using assms by auto
-  then show "C\<sigma>' \<in> grounding_of_cls D"
-    unfolding grounding_of_cls_def using C\<sigma>'(1) by force
-qed
-
 lemma derive_if_remove_subsumed:
   assumes
     "D \<in> clss_of_state St" and
     "subsumes D C"
   shows "sr_ext.derive (grounding_of_state St \<union> grounding_of_cls C) (grounding_of_state St)"
 proof -
   from assms obtain \<sigma> where
     "D \<cdot> \<sigma> = C \<or> D \<cdot> \<sigma> \<subset># C"
     by (auto simp: subsumes_def subset_mset_def)
   then have "D \<cdot> \<sigma> = C \<or> D \<cdot> \<sigma> \<subset># C"
     by (simp add: subset_mset_def)
   then show ?thesis
   proof
     assume "D \<cdot> \<sigma> = C"
     then have "grounding_of_cls C \<subseteq> grounding_of_cls D"
       using subst_cls_eq_grounding_of_cls_subset_eq by simp
     then have "(grounding_of_state St \<union> grounding_of_cls C) = grounding_of_state St"
       using assms unfolding grounding_of_clss_def by auto
     then show ?thesis
       by (auto intro: sr_ext.derive.intros)
   next
     assume a: "D \<cdot> \<sigma> \<subset># C"
     then have "grounding_of_cls C \<subseteq> sr.Rf (grounding_of_state St)"
       using strict_subset_subsumption_grounding_redundant_clss assms by auto
     then show ?thesis
       unfolding grounding_of_clss_def by (force intro: sr_ext.derive.intros)
   qed
 qed
 
 lemma reduction_in_concls_of:
   assumes
     "C\<mu> \<in> grounding_of_cls C" and
     "D + {#L'#} \<in> CC" and
     "- L = L' \<cdot>l \<sigma>" and
     "D \<cdot> \<sigma> \<subseteq># C"
   shows "C\<mu> \<in> concls_of (sr_ext.inferences_from (grounding_of_clss (CC \<union> {C + {#L#}})))"
 proof -
   from assms
   obtain \<mu> where
     \<mu>_p: "C\<mu> = C \<cdot> \<mu> \<and> is_ground_subst \<mu>"
     unfolding grounding_of_cls_def by auto
 
   define \<gamma> where
-    "\<gamma> = Infer {#(C + {#L#})\<cdot> \<mu>#} ((D + {#L'#}) \<cdot> \<sigma> \<cdot> \<mu>) (C \<cdot> \<mu>)"
+    "\<gamma> = Infer {#(C + {#L#}) \<cdot> \<mu>#} ((D + {#L'#}) \<cdot> \<sigma> \<cdot> \<mu>) (C \<cdot> \<mu>)"
 
   have "(D + {#L'#}) \<cdot> \<sigma> \<cdot> \<mu> \<in> grounding_of_clss (CC \<union> {C + {#L#}})"
     unfolding grounding_of_clss_def grounding_of_cls_def
     by (rule UN_I[of "D + {#L'#}"], use assms(2) in simp,
         metis (mono_tags, lifting) \<mu>_p is_ground_comp_subst mem_Collect_eq subst_cls_comp_subst)
   moreover have "(C + {#L#}) \<cdot> \<mu> \<in> grounding_of_clss (CC \<union> {C + {#L#}})"
     using \<mu>_p unfolding  grounding_of_clss_def grounding_of_cls_def by auto
   moreover have
     "\<forall>I. I \<Turnstile> D \<cdot> \<sigma> \<cdot> \<mu> + {#- (L  \<cdot>l \<mu>)#} \<longrightarrow> I \<Turnstile> C  \<cdot> \<mu> + {#L  \<cdot>l \<mu>#} \<longrightarrow> I \<Turnstile> D \<cdot> \<sigma> \<cdot> \<mu> + C \<cdot> \<mu>"
     by auto
   then have "\<forall>I. I \<Turnstile> (D + {#L'#}) \<cdot> \<sigma> \<cdot> \<mu> \<longrightarrow> I \<Turnstile> (C + {#L#}) \<cdot> \<mu> \<longrightarrow> I \<Turnstile> D \<cdot> \<sigma> \<cdot> \<mu> + C \<cdot> \<mu>"
     using assms
     by (metis add_mset_add_single subst_cls_add_mset subst_cls_union subst_minus)
   then have "\<forall>I. I \<Turnstile> (D + {#L'#}) \<cdot> \<sigma> \<cdot> \<mu> \<longrightarrow> I \<Turnstile> (C + {#L#}) \<cdot> \<mu> \<longrightarrow> I \<Turnstile> C \<cdot> \<mu>"
     using assms by (metis (no_types, lifting) subset_mset.le_iff_add subst_cls_union true_cls_union)
   then have "\<forall>I. I \<Turnstile>m {#(D + {#L'#}) \<cdot> \<sigma> \<cdot> \<mu>#} \<longrightarrow> I \<Turnstile> (C + {#L#}) \<cdot> \<mu> \<longrightarrow> I \<Turnstile> C \<cdot> \<mu>"
     by (meson true_cls_mset_singleton)
   ultimately have "\<gamma> \<in> sr_ext.inferences_from (grounding_of_clss (CC \<union> {C + {#L#}}))"
     unfolding sr_ext.inferences_from_def unfolding ground_sound_\<Gamma>_def infer_from_def \<gamma>_def by auto
   then have "C \<cdot> \<mu> \<in> concls_of (sr_ext.inferences_from (grounding_of_clss (CC \<union> {C + {#L#}})))"
     using image_iff unfolding \<gamma>_def by fastforce
   then show "C\<mu> \<in> concls_of (sr_ext.inferences_from (grounding_of_clss (CC \<union> {C + {#L#}})))"
     using \<mu>_p by auto
 qed
 
 lemma reduction_derivable:
   assumes
     "D + {#L'#} \<in> CC" and
     "- L = L' \<cdot>l \<sigma>" and
     "D \<cdot> \<sigma> \<subseteq># C"
   shows "sr_ext.derive (grounding_of_clss (CC \<union> {C + {#L#}})) (grounding_of_clss (CC \<union> {C}))"
 proof -
   from assms have "grounding_of_clss (CC \<union> {C}) - grounding_of_clss (CC \<union> {C + {#L#}})
     \<subseteq> concls_of (sr_ext.inferences_from (grounding_of_clss (CC \<union> {C + {#L#}})))"
     using reduction_in_concls_of unfolding grounding_of_clss_def by auto
   moreover
   have "grounding_of_cls (C + {#L#}) \<subseteq> sr.Rf (grounding_of_clss (CC \<union> {C}))"
     using strict_subset_subsumption_grounding_redundant_clss[of C "id_subst"]
     by auto
   then have "grounding_of_clss (CC \<union> {C + {#L#}}) - grounding_of_clss (CC \<union> {C})
     \<subseteq> sr.Rf (grounding_of_clss (CC \<union> {C}))"
     unfolding grounding_of_clss_def by auto
   ultimately show
     "sr_ext.derive (grounding_of_clss (CC \<union> {C + {#L#}})) (grounding_of_clss (CC \<union> {C}))"
     using sr_ext.derive.intros[of "grounding_of_clss (CC \<union> {C})"
         "grounding_of_clss (CC \<union> {C + {#L#}})"]
     by auto
 qed
 
 text \<open>
 The following corresponds the part of Lemma 4.10 that states we have a theorem proving process:
 \<close>
 
 lemma RP_ground_derive:
   "St \<leadsto> St' \<Longrightarrow> sr_ext.derive (grounding_of_state St) (grounding_of_state St')"
 proof (induction rule: RP.induct)
   case (tautology_deletion A C N P Q)
   {
     fix C\<sigma>
     assume "C\<sigma> \<in> grounding_of_cls C"
     then obtain \<sigma> where
       "C\<sigma> = C \<cdot> \<sigma>"
       unfolding grounding_of_cls_def by auto
     then have "Neg (A \<cdot>a \<sigma>) \<in># C\<sigma> \<and> Pos (A \<cdot>a \<sigma>) \<in># C\<sigma>"
       using tautology_deletion Neg_Melem_subst_atm_subst_cls Pos_Melem_subst_atm_subst_cls by auto
     then have "C\<sigma> \<in> sr.Rf (grounding_of_state (N, P, Q))"
       using sr.tautology_Rf by auto
   }
   then have "grounding_of_state (N \<union> {C}, P, Q) - grounding_of_state (N, P, Q)
     \<subseteq> sr.Rf (grounding_of_state (N, P, Q))"
     unfolding grounding_of_clss_def by auto
   moreover have "grounding_of_state (N, P, Q) - grounding_of_state (N \<union> {C}, P, Q) = {}"
     unfolding grounding_of_clss_def by auto
   ultimately show ?case
     using sr_ext.derive.intros[of "grounding_of_state (N, P, Q)"
       "grounding_of_state (N \<union> {C}, P, Q)"]
     by auto
 next
   case (forward_subsumption D P Q C N)
   then show ?case
     using derive_if_remove_subsumed[of D "(N, P, Q)" C] unfolding grounding_of_clss_def
     by (simp add: sup_commute sup_left_commute)
 next
   case (backward_subsumption_P D N C P Q)
   then show ?case
     using derive_if_remove_subsumed[of D "(N, P, Q)" C] strictly_subsumes_def
     unfolding grounding_of_clss_def by (simp add: sup_commute sup_left_commute)
 next
   case (backward_subsumption_Q D N C P Q)
   then show ?case
     using derive_if_remove_subsumed[of D "(N, P, Q)" C] strictly_subsumes_def
     unfolding grounding_of_clss_def by (simp add: sup_commute sup_left_commute)
 next
   case (forward_reduction D L' P Q L \<sigma> C N)
   then show ?case
     using reduction_derivable[of _ _ "N \<union> P \<union> Q"] by force
 next
   case (backward_reduction_P D L' N L \<sigma> C P Q)
   then show ?case
     using reduction_derivable[of _ _ "N \<union> P \<union> Q"] by force
 next
   case (backward_reduction_Q D L' N L \<sigma> C P Q)
   then show ?case
     using reduction_derivable[of _ _ "N \<union> P \<union> Q"] by force
 next
   case (clause_processing N C P Q)
   then show ?case
     using sr_ext.derive.intros by auto
 next
   case (inference_computation N Q C P)
   {
     fix E\<mu>
     assume "E\<mu> \<in> grounding_of_clss N"
     then obtain \<mu> E where
       E_\<mu>_p: "E\<mu> = E \<cdot> \<mu> \<and> E \<in> N \<and> is_ground_subst \<mu>"
       unfolding grounding_of_clss_def grounding_of_cls_def by auto
     then have E_concl: "E \<in> concls_of (ord_FO_resolution.inferences_between Q C)"
       using inference_computation by auto
     then obtain \<gamma> where
       \<gamma>_p: "\<gamma> \<in> ord_FO_\<Gamma> S \<and> infer_from (Q \<union> {C}) \<gamma> \<and> C \<in># prems_of \<gamma> \<and> concl_of \<gamma> = E"
       unfolding ord_FO_resolution.inferences_between_def by auto
     then obtain CC CAs D AAs As \<sigma> where
       \<gamma>_p2: "\<gamma> = Infer CC D E \<and> ord_resolve_rename S CAs D AAs As \<sigma> E \<and> mset CAs = CC"
       unfolding ord_FO_\<Gamma>_def by auto
     define \<rho> where
       "\<rho> = hd (renamings_apart (D # CAs))"
     define \<rho>s where
       "\<rho>s = tl (renamings_apart (D # CAs))"
     define \<gamma>_ground where
       "\<gamma>_ground = Infer (mset (CAs \<cdot>\<cdot>cl \<rho>s) \<cdot>cm \<sigma> \<cdot>cm \<mu>) (D \<cdot> \<rho> \<cdot> \<sigma> \<cdot> \<mu>) (E \<cdot> \<mu>)"
     have "\<forall>I. I \<Turnstile>m mset (CAs \<cdot>\<cdot>cl \<rho>s) \<cdot>cm \<sigma> \<cdot>cm \<mu> \<longrightarrow> I \<Turnstile> D \<cdot> \<rho> \<cdot> \<sigma> \<cdot> \<mu> \<longrightarrow> I \<Turnstile> E \<cdot> \<mu>"
       using ord_resolve_rename_ground_inst_sound[of _ _ _ _ _ _ _ _ _ _ \<mu>] \<rho>_def \<rho>s_def E_\<mu>_p \<gamma>_p2
       by auto
     then have "\<gamma>_ground \<in> {Infer cc d e | cc d e. \<forall>I. I \<Turnstile>m cc \<longrightarrow> I \<Turnstile> d \<longrightarrow> I \<Turnstile> e}"
       unfolding \<gamma>_ground_def by auto
     moreover have "set_mset (prems_of \<gamma>_ground) \<subseteq> grounding_of_state ({}, P \<union> {C}, Q)"
     proof -
       have "D = C \<or> D \<in> Q"
         unfolding \<gamma>_ground_def using E_\<mu>_p \<gamma>_p2 \<gamma>_p unfolding infer_from_def
         unfolding grounding_of_clss_def grounding_of_cls_def by simp
       then have "D \<cdot> \<rho> \<cdot> \<sigma> \<cdot> \<mu> \<in> grounding_of_cls C \<or> (\<exists>x \<in> Q. D \<cdot> \<rho> \<cdot> \<sigma> \<cdot> \<mu> \<in> grounding_of_cls x)"
         using E_\<mu>_p
         unfolding grounding_of_cls_def
         by (metis (mono_tags, lifting) is_ground_comp_subst mem_Collect_eq subst_cls_comp_subst)
       then have "(D \<cdot> \<rho> \<cdot> \<sigma> \<cdot> \<mu> \<in> grounding_of_cls C \<or>
         (\<exists>x \<in> P. D \<cdot> \<rho> \<cdot> \<sigma> \<cdot> \<mu> \<in> grounding_of_cls x) \<or>
         (\<exists>x \<in> Q. D \<cdot> \<rho> \<cdot> \<sigma> \<cdot> \<mu> \<in> grounding_of_cls x))"
         by metis
-      moreover have "\<forall>i < length (CAs \<cdot>\<cdot>cl \<rho>s \<cdot>cl \<sigma> \<cdot>cl \<mu>). ((CAs \<cdot>\<cdot>cl \<rho>s \<cdot>cl \<sigma> \<cdot>cl \<mu>) ! i) \<in>
+      moreover have "\<forall>i < length (CAs \<cdot>\<cdot>cl \<rho>s \<cdot>cl \<sigma> \<cdot>cl \<mu>). (CAs \<cdot>\<cdot>cl \<rho>s \<cdot>cl \<sigma> \<cdot>cl \<mu>) ! i \<in>
         {C \<cdot> \<sigma> |\<sigma>. is_ground_subst \<sigma>} \<union>
         ((\<Union>C \<in> P. {C \<cdot> \<sigma> | \<sigma>. is_ground_subst \<sigma>}) \<union> (\<Union>C\<in>Q. {C \<cdot> \<sigma> | \<sigma>. is_ground_subst \<sigma>}))"
       proof (rule, rule)
         fix i
         assume "i < length (CAs \<cdot>\<cdot>cl \<rho>s \<cdot>cl \<sigma> \<cdot>cl \<mu>)"
         then have a: "i < length CAs \<and> i < length \<rho>s"
           by simp
         moreover from a have "CAs ! i \<in> {C} \<union> Q"
           using \<gamma>_p2 \<gamma>_p unfolding infer_from_def
           by (metis (no_types, lifting) Un_subset_iff inference.sel(1) set_mset_union
               sup_commute nth_mem_mset subsetCE)
         ultimately have "(CAs \<cdot>\<cdot>cl \<rho>s \<cdot>cl \<sigma> \<cdot>cl \<mu>) ! i \<in>
           {C \<cdot> \<sigma> |\<sigma>. is_ground_subst \<sigma>} \<or>
           ((CAs \<cdot>\<cdot>cl \<rho>s \<cdot>cl \<sigma> \<cdot>cl \<mu>) ! i \<in> (\<Union>C\<in>P. {C \<cdot> \<sigma> |\<sigma>. is_ground_subst \<sigma>}) \<or>
           (CAs \<cdot>\<cdot>cl \<rho>s \<cdot>cl \<sigma> \<cdot>cl \<mu>) ! i \<in> (\<Union>C \<in> Q. {C \<cdot> \<sigma> | \<sigma>. is_ground_subst \<sigma>}))"
           using E_\<mu>_p \<gamma>_p2 \<gamma>_p
           unfolding \<gamma>_ground_def infer_from_def grounding_of_clss_def grounding_of_cls_def
           apply -
           apply (cases "CAs ! i = C")
           subgoal
             apply (rule disjI1)
             apply (rule Set.CollectI)
             apply (rule_tac x = "(\<rho>s ! i) \<odot> \<sigma> \<odot> \<mu>" in exI)
             using \<rho>s_def using renamings_apart_length by (auto; fail)
           subgoal
             apply (rule disjI2)
             apply (rule disjI2)
             apply (rule_tac a = "CAs ! i" in UN_I)
             subgoal by blast
             subgoal
               apply (rule Set.CollectI)
               apply (rule_tac x = "(\<rho>s ! i) \<odot> \<sigma> \<odot> \<mu>" in exI)
               using \<rho>s_def using renamings_apart_length by (auto; fail)
             done
           done
         then show "(CAs \<cdot>\<cdot>cl \<rho>s \<cdot>cl \<sigma> \<cdot>cl \<mu>) ! i \<in> {C \<cdot> \<sigma> |\<sigma>. is_ground_subst \<sigma>} \<union>
           ((\<Union>C \<in> P. {C \<cdot> \<sigma> |\<sigma>. is_ground_subst \<sigma>}) \<union> (\<Union>C \<in> Q. {C \<cdot> \<sigma> |\<sigma>. is_ground_subst \<sigma>}))"
           by blast
       qed
       then have "\<forall>x \<in># mset (CAs \<cdot>\<cdot>cl \<rho>s \<cdot>cl \<sigma> \<cdot>cl \<mu>). x \<in> {C \<cdot> \<sigma> |\<sigma>. is_ground_subst \<sigma>} \<union>
         ((\<Union>C \<in> P. {C \<cdot> \<sigma> |\<sigma>. is_ground_subst \<sigma>}) \<union> (\<Union>C \<in> Q. {C \<cdot> \<sigma> |\<sigma>. is_ground_subst \<sigma>}))"
         by (metis (lifting) in_set_conv_nth set_mset_mset)
       then have "set_mset (mset (CAs \<cdot>\<cdot>cl \<rho>s) \<cdot>cm \<sigma> \<cdot>cm \<mu>) \<subseteq>
         grounding_of_cls C \<union> grounding_of_clss P \<union> grounding_of_clss Q"
         unfolding grounding_of_cls_def grounding_of_clss_def
         using mset_subst_cls_list_subst_cls_mset by auto
       ultimately show ?thesis
         unfolding \<gamma>_ground_def grounding_of_clss_def by auto
     qed
     ultimately have
       "E \<cdot> \<mu> \<in> concls_of (sr_ext.inferences_from (grounding_of_state ({}, P \<union> {C}, Q)))"
       unfolding sr_ext.inferences_from_def inference_system.inferences_from_def ground_sound_\<Gamma>_def
         infer_from_def
-      using \<gamma>_ground_def by (metis (no_types, lifting) imageI inference.sel(3) mem_Collect_eq)
+      using \<gamma>_ground_def by (metis (mono_tags, lifting) image_eqI inference.sel(3) mem_Collect_eq)
     then have "E\<mu> \<in> concls_of (sr_ext.inferences_from (grounding_of_state ({}, P \<union> {C}, Q)))"
       using E_\<mu>_p by auto
   }
   then have "grounding_of_state (N, P, Q \<union> {C}) - grounding_of_state ({}, P \<union> {C}, Q)
     \<subseteq> concls_of (sr_ext.inferences_from (grounding_of_state ({}, P \<union> {C}, Q)))"
     unfolding grounding_of_clss_def by auto
   moreover have "grounding_of_state ({}, P \<union> {C}, Q) - grounding_of_state (N, P, Q \<union> {C}) = {}"
     unfolding grounding_of_clss_def by auto
   ultimately show ?case
     using sr_ext.derive.intros[of "(grounding_of_state (N, P, Q \<union> {C}))"
         "(grounding_of_state ({}, P \<union> {C}, Q))"] by auto
 qed
 
 text \<open>
 A useful consequence:
 \<close>
 
-theorem RP_model:
-  "St \<leadsto> St' \<Longrightarrow> I \<Turnstile>s grounding_of_state St' \<longleftrightarrow> I \<Turnstile>s grounding_of_state St"
+theorem RP_model: "St \<leadsto> St' \<Longrightarrow> I \<Turnstile>s grounding_of_state St' \<longleftrightarrow> I \<Turnstile>s grounding_of_state St"
 proof (drule RP_ground_derive, erule sr_ext.derive.cases, hypsubst)
   let
     ?gSt = "grounding_of_state St" and
     ?gSt' = "grounding_of_state St'"
 
   assume
     deduct: "?gSt' - ?gSt \<subseteq> concls_of (sr_ext.inferences_from ?gSt)" (is "_ \<subseteq> ?concls") and
     delete: "?gSt - ?gSt' \<subseteq> sr.Rf ?gSt'"
 
   show "I \<Turnstile>s ?gSt' \<longleftrightarrow> I \<Turnstile>s ?gSt"
   proof
     assume bef: "I \<Turnstile>s ?gSt"
     then have "I \<Turnstile>s ?concls"
       unfolding ground_sound_\<Gamma>_def inference_system.inferences_from_def true_clss_def
         true_cls_mset_def
       by (auto simp add: image_def infer_from_def dest!: spec[of _ I])
     then have diff: "I \<Turnstile>s ?gSt' - ?gSt"
       using deduct by (blast intro: true_clss_mono)
     then show "I \<Turnstile>s ?gSt'"
       using bef unfolding true_clss_def by blast
   next
     assume aft: "I \<Turnstile>s ?gSt'"
     have "I \<Turnstile>s ?gSt' \<union> sr.Rf ?gSt'"
       by (rule sr.Rf_model) (smt Diff_eq_empty_iff Diff_subset Un_Diff aft
           standard_redundancy_criterion.Rf_mono sup_bot.right_neutral sup_ge1 true_clss_mono)
     then have "I \<Turnstile>s sr.Rf ?gSt'"
       using true_clss_union by blast
     then have diff: "I \<Turnstile>s ?gSt - ?gSt'"
       using delete by (blast intro: true_clss_mono)
     then show "I \<Turnstile>s ?gSt"
       using aft unfolding true_clss_def by blast
   qed
 qed
 
 text \<open>
 Another formulation of the part of Lemma 4.10 that states we have a theorem proving process:
 \<close>
 
 lemma ground_derive_chain: "chain (\<leadsto>) Sts \<Longrightarrow> chain sr_ext.derive (lmap grounding_of_state Sts)"
   using RP_ground_derive by (simp add: chain_lmap[of "(\<leadsto>)"])
 
 text \<open>
 The following is used prove to Lemma 4.11:
 \<close>
 
-lemma in_Sup_llist_in_nth: "C \<in> Sup_llist Gs \<Longrightarrow> \<exists>j. enat j < llength Gs \<and> C \<in> lnth Gs j"
-  unfolding Sup_llist_def by auto
-    \<comment> \<open>Note: Gs is called Ns in the chapter\<close>
-
 lemma Sup_llist_grounding_of_state_ground:
   assumes "C \<in> Sup_llist (lmap grounding_of_state Sts)"
   shows "is_ground_cls C"
 proof -
   have "\<exists>j. enat j < llength (lmap grounding_of_state Sts)
     \<and> C \<in> lnth (lmap grounding_of_state Sts) j"
-    using assms in_Sup_llist_in_nth by fast
-  then obtain j where
-    "enat j < llength (lmap grounding_of_state Sts)"
-    "C \<in> lnth (lmap grounding_of_state Sts) j"
-    by blast
+    using assms Sup_llist_imp_exists_index by fast
   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
+    using Sup_llist_imp_exists_index by fastforce
   then obtain D \<sigma> where
     "D \<in> clss_of_state (lnth Sts i) \<and> D \<cdot> \<sigma> = C \<and> is_ground_subst \<sigma>"
     using assms unfolding grounding_of_clss_def grounding_of_cls_def by fastforce
   then have "D \<in> clss_of_state (Sup_state Sts) \<and> D \<cdot> \<sigma> = C \<and> is_ground_subst \<sigma>"
     using i_p unfolding Sup_state_def
     by (metis (no_types, lifting) UnCI UnE contra_subsetD N_of_state.simps P_of_state.simps
         Q_of_state.simps llength_lmap lnth_lmap lnth_subset_Sup_llist)
   then show ?thesis
     by auto
 qed
 
 lemma
   N_of_state_Liminf: "N_of_state (Liminf_state Sts) = Liminf_llist (lmap N_of_state Sts)" and
   P_of_state_Liminf: "P_of_state (Liminf_state Sts) = Liminf_llist (lmap P_of_state Sts)"
   unfolding Liminf_state_def by auto
 
 lemma eventually_removed_from_N:
   assumes
     d_in: "D \<in> N_of_state (lnth Sts i)" and
     fair: "fair_state_seq Sts" and
     i_Sts: "enat i < llength Sts"
   shows "\<exists>l. D \<in> N_of_state (lnth Sts l) \<and> D \<notin> N_of_state (lnth Sts (Suc l)) \<and> i \<le> l
     \<and> enat (Suc l) < llength Sts"
 proof (rule ccontr)
   assume a: "\<not> ?thesis"
   have "i \<le> l \<Longrightarrow> enat l < llength Sts \<Longrightarrow> D \<in> N_of_state (lnth Sts l)" for l
     using d_in by (induction l, blast, metis a Suc_ile_eq le_SucE less_imp_le)
   then have "D \<in> Liminf_llist (lmap N_of_state Sts)"
     unfolding Liminf_llist_def using i_Sts by auto
   then show False
     using fair unfolding fair_state_seq_def by (simp add: N_of_state_Liminf)
 qed
 
 lemma eventually_removed_from_P:
   assumes
     d_in: "D \<in> P_of_state (lnth Sts i)" and
     fair: "fair_state_seq Sts" and
     i_Sts: "enat i < llength Sts"
   shows "\<exists>l. D \<in> P_of_state (lnth Sts l) \<and> D \<notin> P_of_state (lnth Sts (Suc l)) \<and> i \<le> l
     \<and> enat (Suc l) < llength Sts"
 proof (rule ccontr)
   assume a: "\<not> ?thesis"
   have "i \<le> l \<Longrightarrow> enat l < llength Sts \<Longrightarrow> D \<in> P_of_state (lnth Sts l)" for l
     using d_in by (induction l, blast, metis a Suc_ile_eq le_SucE less_imp_le)
   then have "D \<in> Liminf_llist (lmap P_of_state Sts)"
     unfolding Liminf_llist_def using i_Sts by auto
   then show False
     using fair unfolding fair_state_seq_def by (simp add: P_of_state_Liminf)
 qed
 
 lemma instance_if_subsumed_and_in_limit:
   assumes
     deriv: "chain (\<leadsto>) Sts" and
     ns: "Gs = lmap grounding_of_state Sts" and
     c: "C \<in> Liminf_llist Gs - sr.Rf (Liminf_llist Gs)" and
     d: "D \<in> clss_of_state (lnth Sts i)" "enat i < llength Sts" "subsumes D C"
   shows "\<exists>\<sigma>. D \<cdot> \<sigma> = C \<and> is_ground_subst \<sigma>"
 proof -
   let ?Ps = "\<lambda>i. P_of_state (lnth Sts i)"
   let ?Qs = "\<lambda>i. Q_of_state (lnth Sts i)"
 
   have ground_C: "is_ground_cls C"
     using c using Liminf_grounding_of_state_ground ns by auto
 
   have derivns: "chain sr_ext.derive Gs"
     using ground_derive_chain deriv ns by auto
 
   have "\<exists>\<sigma>. D \<cdot> \<sigma> = C"
   proof (rule ccontr)
     assume "\<nexists>\<sigma>. D \<cdot> \<sigma> = C"
     moreover from d(3) obtain \<tau>_proto where
       "D \<cdot> \<tau>_proto \<subseteq># C" unfolding subsumes_def
       by blast
     then obtain \<tau> where
       \<tau>_p: "D \<cdot> \<tau> \<subseteq># C \<and> is_ground_subst \<tau>"
       using ground_C by (metis is_ground_cls_mono make_ground_subst subset_mset.order_refl)
     ultimately have subsub: "D \<cdot> \<tau> \<subset># C"
       using subset_mset.le_imp_less_or_eq by auto
     moreover have "is_ground_subst \<tau>"
       using \<tau>_p by auto
     moreover have "D \<in> clss_of_state (lnth Sts i)"
       using d by auto
     ultimately have "C \<in> sr.Rf (grounding_of_state (lnth Sts i))"
       using strict_subset_subsumption_redundant_clss by auto
     then have "C \<in> sr.Rf (Sup_llist Gs)"
       using d ns by (smt contra_subsetD llength_lmap lnth_lmap lnth_subset_Sup_llist sr.Rf_mono)
     then have "C \<in> sr.Rf (Liminf_llist Gs)"
       unfolding ns using local.sr_ext.Rf_limit_Sup derivns ns by auto
     then show False
       using c by auto
   qed
   then obtain \<sigma> where
     "D \<cdot> \<sigma> = C \<and> is_ground_subst \<sigma>"
     using ground_C by (metis make_ground_subst)
   then show ?thesis
     by auto
 qed
 
 lemma from_Q_to_Q_inf:
   assumes
     deriv: "chain (\<leadsto>) Sts" and
     fair: "fair_state_seq Sts" and
     ns: "Gs = lmap grounding_of_state Sts" and
     c: "C \<in> Liminf_llist Gs - sr.Rf (Liminf_llist Gs)" and
     d: "D \<in> Q_of_state (lnth Sts i)" "enat i < llength Sts" "subsumes D C" and
     d_least: "\<forall>E \<in> {E. E \<in> (clss_of_state (Sup_state Sts)) \<and> subsumes E C}.
       \<not> strictly_subsumes E D"
   shows "D \<in> Q_of_state (Liminf_state Sts)"
 proof -
   let ?Ps = "\<lambda>i. P_of_state (lnth Sts i)"
   let ?Qs = "\<lambda>i. Q_of_state (lnth Sts i)"
 
   have ground_C: "is_ground_cls C"
     using c using Liminf_grounding_of_state_ground ns by auto
 
   have derivns: "chain sr_ext.derive Gs"
     using ground_derive_chain deriv ns by auto
 
   have "\<exists>\<sigma>. D \<cdot> \<sigma> = C \<and> is_ground_subst \<sigma>"
     using instance_if_subsumed_and_in_limit[OF deriv] c d unfolding ns by blast
   then obtain \<sigma> where
     \<sigma>: "D \<cdot> \<sigma> = C" "is_ground_subst \<sigma>"
     by auto
 
   have in_Sts_in_Sts_Suc:
     "\<forall>l \<ge> i. enat (Suc l) < llength Sts \<longrightarrow> D \<in> Q_of_state (lnth Sts l) \<longrightarrow>
        D \<in> Q_of_state (lnth Sts (Suc l))"
   proof (rule, rule, rule, rule)
     fix l
     assume
       len: "i \<le> l" and
       llen: "enat (Suc l) < llength Sts" and
       d_in_q: "D \<in> Q_of_state (lnth Sts l)"
 
     have "lnth Sts l \<leadsto> lnth Sts (Suc l)"
       using llen deriv chain_lnth_rel by blast
     then show "D \<in> Q_of_state (lnth Sts (Suc l))"
     proof (cases rule: RP.cases)
       case (backward_subsumption_Q D' N D_removed P Q)
       moreover
       {
         assume "D_removed = D"
         then obtain D_subsumes where
           D_subsumes_p: "D_subsumes \<in> N \<and> strictly_subsumes D_subsumes D"
           using backward_subsumption_Q by auto
         moreover from D_subsumes_p have "subsumes D_subsumes C"
           using d subsumes_trans unfolding strictly_subsumes_def by blast
         moreover from backward_subsumption_Q have "D_subsumes \<in> clss_of_state (Sup_state Sts)"
           using D_subsumes_p llen
           by (metis (no_types) UnI1 N_of_state.simps llength_lmap lnth_lmap lnth_subset_Sup_llist
               rev_subsetD Sup_state_def)
         ultimately have False
           using d_least unfolding subsumes_def by auto
       }
       ultimately show ?thesis
         using d_in_q by auto
     next
       case (backward_reduction_Q E L' N L \<sigma> D' P Q)
       {
         assume "D' + {#L#} = D"
         then have D'_p: "strictly_subsumes D' D \<and> D' \<in> ?Ps (Suc l)"
           using subset_strictly_subsumes[of D' D] backward_reduction_Q by auto
         then have subc: "subsumes D' C"
           using d(3) subsumes_trans unfolding strictly_subsumes_def by auto
         from D'_p have "D' \<in> clss_of_state (Sup_state Sts)"
           using llen by (metis (no_types) UnI1 P_of_state.simps llength_lmap lnth_lmap
               lnth_subset_Sup_llist subsetCE sup_ge2 Sup_state_def)
         then have False
           using d_least D'_p subc by auto
       }
       then show ?thesis
         using backward_reduction_Q d_in_q by auto
     qed (use d_in_q in auto)
   qed
   have D_in_Sts: "D \<in> Q_of_state (lnth Sts l)" and D_in_Sts_Suc: "D \<in> Q_of_state (lnth Sts (Suc l))"
     if l_i: "l \<ge> i" and enat: "enat (Suc l) < llength Sts" for l
   proof -
     show "D \<in> Q_of_state (lnth Sts l)"
       using l_i enat
       apply (induction "l - i" arbitrary: l)
       subgoal using d by auto
       subgoal using d(1) in_Sts_in_Sts_Suc
         by (metis (no_types, lifting) Suc_ile_eq add_Suc_right add_diff_cancel_left' le_SucE
             le_Suc_ex less_imp_le)
       done
     then show "D \<in> Q_of_state (lnth Sts (Suc l))"
       using l_i enat in_Sts_in_Sts_Suc by blast
   qed
   have "i \<le> x \<Longrightarrow> enat x < llength Sts \<Longrightarrow> D \<in> Q_of_state (lnth Sts x)" for x
     apply (cases x)
     subgoal using d(1) by (auto intro!: exI[of _ i] simp: less_Suc_eq)
     subgoal for x'
       using d(1) D_in_Sts_Suc[of x'] by (cases \<open>i \<le> x'\<close>) (auto simp: not_less_eq_eq)
     done
   then have "D \<in> Liminf_llist (lmap Q_of_state Sts)"
     unfolding Liminf_llist_def by (auto intro!: exI[of _ i] simp: d)
   then show ?thesis
     unfolding Liminf_state_def by auto
 qed
 
 lemma from_P_to_Q:
   assumes
     deriv: "chain (\<leadsto>) Sts" and
     fair: "fair_state_seq Sts" and
     ns: "Gs = lmap grounding_of_state Sts" and
     c: "C \<in> Liminf_llist Gs - sr.Rf (Liminf_llist Gs)" and
     d: "D \<in> P_of_state (lnth Sts i)" "enat i < llength Sts" "subsumes D C" and
     d_least: "\<forall>E \<in> {E. E \<in> (clss_of_state (Sup_state Sts)) \<and> subsumes E C}.
       \<not> strictly_subsumes E D"
   shows "\<exists>l. D \<in> Q_of_state (lnth Sts l) \<and> enat l < llength Sts"
 proof -
   let ?Ns = "\<lambda>i. N_of_state (lnth Sts i)"
   let ?Ps = "\<lambda>i. P_of_state (lnth Sts i)"
   let ?Qs = "\<lambda>i. Q_of_state (lnth Sts i)"
 
   have ground_C: "is_ground_cls C"
     using c using Liminf_grounding_of_state_ground ns by auto
 
   have derivns: "chain sr_ext.derive Gs"
     using ground_derive_chain deriv ns by auto
 
   have "\<exists>\<sigma>. D \<cdot> \<sigma> = C \<and> is_ground_subst \<sigma>"
     using instance_if_subsumed_and_in_limit[OF deriv] ns c d by blast
   then obtain \<sigma> where
     \<sigma>: "D \<cdot> \<sigma> = C" "is_ground_subst \<sigma>"
     by auto
 
   obtain l where
     l_p: "D \<in> P_of_state (lnth Sts l) \<and> D \<notin> P_of_state (lnth Sts (Suc l)) \<and> i \<le> l
       \<and> enat (Suc l) < llength Sts"
     using fair using eventually_removed_from_P d unfolding ns by auto
   then have l_Gs: "enat (Suc l) < llength Gs"
     using ns by auto
   from l_p have "lnth Sts l \<leadsto> lnth Sts (Suc l)"
     using deriv using chain_lnth_rel by auto
   then show ?thesis
   proof (cases rule: RP.cases)
     case (backward_subsumption_P D' N D_twin P Q)
     note lrhs = this(1,2) and D'_p = this(3,4)
     then have twins: "D_twin = D" "?Ns (Suc l) = N" "?Ns l = N"  "?Ps (Suc l) = P"
       "?Ps l = P \<union> {D_twin}" "?Qs (Suc l) = Q" "?Qs l = Q"
       using l_p by auto
     note D'_p = D'_p[unfolded twins(1)]
     then have subc: "subsumes D' C"
       unfolding strictly_subsumes_def subsumes_def using \<sigma>
       by (metis subst_cls_comp_subst subst_cls_mono_mset)
     from D'_p have "D' \<in> clss_of_state (Sup_state Sts)"
       unfolding twins(2)[symmetric] using l_p
       by (metis (no_types) UnI1 N_of_state.simps llength_lmap lnth_lmap lnth_subset_Sup_llist
           subsetCE Sup_state_def)
     then have False
       using d_least D'_p subc by auto
     then show ?thesis
       by auto
   next
     case (backward_reduction_P E L' N L \<sigma> D' P Q)
     then have twins: "D' + {#L#} = D" "?Ns (Suc l) = N" "?Ns l = N"  "?Ps (Suc l) = P \<union> {D'}"
       "?Ps l = P \<union> {D' + {#L#}}" "?Qs (Suc l) = Q" "?Qs l = Q"
       using l_p by auto
     then have D'_p: "strictly_subsumes D' D \<and> D' \<in> ?Ps (Suc l)"
       using subset_strictly_subsumes[of D' D] by auto
     then have subc: "subsumes D' C"
       using d(3) subsumes_trans unfolding strictly_subsumes_def by auto
     from D'_p have "D' \<in> clss_of_state (Sup_state Sts)"
       using l_p by (metis (no_types) UnI1 P_of_state.simps llength_lmap lnth_lmap
           lnth_subset_Sup_llist subsetCE sup_ge2 Sup_state_def)
     then have False
       using d_least D'_p subc by auto
     then show ?thesis
       by auto
   next
     case (inference_computation N Q D_twin P)
     then have twins: "D_twin = D" "?Ps (Suc l) = P" "?Ps l = P \<union> {D_twin}"
       "?Qs (Suc l) = Q \<union> {D_twin}" "?Qs l = Q"
       using l_p by auto
     then show ?thesis
       using d \<sigma> l_p by auto
   qed (use l_p in auto)
 qed
 
-lemma variants_sym: "variants D D' \<longleftrightarrow> variants D' D"
-  unfolding variants_def by auto
-
-lemma variants_imp_exists_subtitution: "variants D D' \<Longrightarrow> \<exists>\<sigma>. D \<cdot> \<sigma> = D'"
-  unfolding variants_iff_subsumes subsumes_def
-  by (meson strictly_subsumes_def subset_mset_def strict_subset_subst_strictly_subsumes subsumes_def)
-
-lemma properly_subsume_variants:
-  assumes "strictly_subsumes E D" and "variants D D'"
-  shows "strictly_subsumes E D'"
-proof -
-  from assms obtain \<sigma> \<sigma>' where
-    \<sigma>_\<sigma>'_p: "D \<cdot> \<sigma> = D' \<and> D' \<cdot> \<sigma>' = D"
-    using variants_imp_exists_subtitution variants_sym by metis
-
-  from assms obtain \<sigma>'' where
-    "E \<cdot> \<sigma>'' \<subseteq># D"
-    unfolding strictly_subsumes_def subsumes_def by auto
-  then have "E \<cdot> \<sigma>'' \<cdot> \<sigma> \<subseteq># D \<cdot> \<sigma>"
-    using subst_cls_mono_mset by blast
-  then have "E \<cdot> (\<sigma>'' \<odot> \<sigma>)  \<subseteq># D'"
-    using \<sigma>_\<sigma>'_p by auto
-  moreover from assms have n: "(\<nexists>\<sigma>. D \<cdot> \<sigma> \<subseteq># E)"
-    unfolding strictly_subsumes_def subsumes_def by auto
-  have "\<nexists>\<sigma>. D' \<cdot> \<sigma> \<subseteq># E"
-  proof
-    assume "\<exists>\<sigma>'''. D' \<cdot> \<sigma>''' \<subseteq># E"
-    then obtain \<sigma>''' where
-      "D' \<cdot> \<sigma>''' \<subseteq># E"
-      by auto
-    then have "D \<cdot> (\<sigma> \<odot> \<sigma>''') \<subseteq># E"
-      using \<sigma>_\<sigma>'_p by auto
-    then show False
-      using n by metis
-  qed
-  ultimately show ?thesis
-    unfolding strictly_subsumes_def subsumes_def by metis
-qed
-
-lemma neg_properly_subsume_variants:
-  assumes "\<not> strictly_subsumes E D" and "variants D D'"
-  shows "\<not> strictly_subsumes E D'"
-  using assms properly_subsume_variants variants_sym by auto
-
 lemma from_N_to_P_or_Q:
   assumes
     deriv: "chain (\<leadsto>) Sts" and
     fair: "fair_state_seq Sts" and
     ns: "Gs = lmap grounding_of_state Sts" and
     c: "C \<in> Liminf_llist Gs - sr.Rf (Liminf_llist Gs)" and
     d: "D \<in> N_of_state (lnth Sts i)" "enat i < llength Sts" "subsumes D C" and
     d_least: "\<forall>E \<in> {E. E \<in> (clss_of_state (Sup_state Sts)) \<and> subsumes E C}. \<not> strictly_subsumes E D"
   shows "\<exists>l D' \<sigma>'. D' \<in> P_of_state (lnth Sts l) \<union> Q_of_state (lnth Sts l) \<and>
     enat l < llength Sts \<and>
     (\<forall>E \<in> {E. E \<in> (clss_of_state (Sup_state Sts)) \<and> subsumes E C}. \<not> strictly_subsumes E D') \<and>
     D' \<cdot> \<sigma>' = C \<and> is_ground_subst \<sigma>' \<and> subsumes D' C"
 proof -
   let ?Ns = "\<lambda>i. N_of_state (lnth Sts i)"
   let ?Ps = "\<lambda>i. P_of_state (lnth Sts i)"
   let ?Qs = "\<lambda>i. Q_of_state (lnth Sts i)"
 
   have ground_C: "is_ground_cls C"
     using c using Liminf_grounding_of_state_ground ns by auto
 
   have derivns: "chain sr_ext.derive Gs"
     using ground_derive_chain deriv ns by auto
 
   have "\<exists>\<sigma>. D \<cdot> \<sigma> = C \<and> is_ground_subst \<sigma>"
     using instance_if_subsumed_and_in_limit[OF deriv] ns c d by blast
   then obtain \<sigma> where
     \<sigma>: "D \<cdot> \<sigma> = C" "is_ground_subst \<sigma>"
     by auto
 
   from c have no_taut: "\<not> (\<exists>A. Pos A \<in># C \<and> Neg A \<in># C)"
     using sr.tautology_Rf by auto
 
   have "\<exists>l. D \<in> N_of_state (lnth Sts l)
     \<and> D \<notin> N_of_state (lnth Sts (Suc l)) \<and> i \<le> l \<and> enat (Suc l) < llength Sts"
     using fair using eventually_removed_from_N d unfolding ns by auto
   then obtain l where
     l_p: "D \<in> N_of_state (lnth Sts l) \<and> D \<notin> N_of_state (lnth Sts (Suc l)) \<and> i \<le> l
       \<and> enat (Suc l) < llength Sts"
     by auto
   then have l_Gs: "enat (Suc l) < llength Gs"
     using ns by auto
   from l_p have "lnth Sts l \<leadsto> lnth Sts (Suc l)"
     using deriv using chain_lnth_rel by auto
   then show ?thesis
   proof (cases rule: RP.cases)
     case (tautology_deletion A D_twin N P Q)
     then have "D_twin = D"
       using l_p by auto
     then have "Pos (A \<cdot>a \<sigma>) \<in># C \<and> Neg (A \<cdot>a \<sigma>) \<in># C"
       using tautology_deletion(3,4) \<sigma>
       by (metis Melem_subst_cls eql_neg_lit_eql_atm eql_pos_lit_eql_atm)
     then have False
       using no_taut by metis
     then show ?thesis
       by blast
   next
     case (forward_subsumption D' P Q D_twin N)
     note lrhs = this(1,2) and D'_p = this(3,4)
     then have twins: "D_twin = D" "?Ns (Suc l) = N" "?Ns l = N \<union> {D_twin}"  "?Ps (Suc l) = P "
       "?Ps l = P" "?Qs (Suc l) = Q" "?Qs l = Q"
       using l_p by auto
     note D'_p = D'_p[unfolded twins(1)]
     from D'_p(2) have subs: "subsumes D' C"
       using d(3) by (blast intro: subsumes_trans)
     moreover have "D' \<in> clss_of_state (Sup_state Sts)"
       using twins D'_p l_p unfolding Sup_state_def
       by simp (metis (no_types) contra_subsetD llength_lmap lnth_lmap lnth_subset_Sup_llist)
     ultimately have "\<not> strictly_subsumes D' D"
       using d_least by auto
     then have "subsumes D D'"
       unfolding strictly_subsumes_def using D'_p by auto
     then have v: "variants D D'"
       using D'_p unfolding variants_iff_subsumes by auto
     then have mini: "\<forall>E \<in> {E \<in> clss_of_state (Sup_state Sts). subsumes E C}.
       \<not> strictly_subsumes E D'"
-      using d_least D'_p neg_properly_subsume_variants[of _ D D'] by auto
+      using d_least D'_p neg_strictly_subsumes_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)
+      using \<sigma> variants_imp_exists_substitution variants_sym by (metis subst_cls_comp_subst)
     then have "\<exists>\<sigma>'. D' \<cdot> \<sigma>' = C \<and> is_ground_subst \<sigma>'"
       using ground_C by (meson make_ground_subst refl)
     then obtain \<sigma>' where
       \<sigma>'_p: "D' \<cdot> \<sigma>' = C \<and> is_ground_subst \<sigma>'"
       by metis
 
     show ?thesis
       using D'_p twins l_p subs mini \<sigma>'_p by auto
   next
     case (forward_reduction E L' P Q L \<sigma> D' N)
     then have twins: "D' + {#L#} = D" "?Ns (Suc l) = N \<union> {D'}" "?Ns l = N \<union> {D' + {#L#}}"
       "?Ps (Suc l) = P " "?Ps l = P" "?Qs (Suc l) = Q" "?Qs l = Q"
       using l_p by auto
     then have D'_p: "strictly_subsumes D' D \<and> D' \<in> ?Ns (Suc l)"
       using subset_strictly_subsumes[of D' D] by auto
     then have subc: "subsumes D' C"
       using d(3) subsumes_trans unfolding strictly_subsumes_def by blast
     from D'_p have "D' \<in> clss_of_state (Sup_state Sts)"
       using l_p by (metis (no_types) UnI1 N_of_state.simps llength_lmap lnth_lmap
           lnth_subset_Sup_llist subsetCE Sup_state_def)
     then have False
       using d_least D'_p subc by auto
     then show ?thesis
       by auto
   next
     case (clause_processing N D_twin P Q)
     then have twins:  "D_twin = D" "?Ns (Suc l) = N" "?Ns l = N \<union> {D}"  "?Ps (Suc l) = P \<union> {D}"
       "?Ps l = P" "?Qs (Suc l) = Q" "?Qs l = Q"
       using l_p by auto
     then show ?thesis
       using d \<sigma> l_p d_least by blast
   qed (use l_p in auto)
 qed
 
 lemma eventually_in_Qinf:
   assumes
     deriv: "chain (\<leadsto>) Sts" and
     D_p: "D \<in> clss_of_state (Sup_state Sts)"
       "subsumes D C" "\<forall>E \<in> {E. E \<in> (clss_of_state (Sup_state Sts)) \<and> subsumes E C}.
        \<not> strictly_subsumes E D" and
     fair: "fair_state_seq Sts" and
     ns: "Gs = lmap grounding_of_state Sts" and
     c: "C \<in> Liminf_llist Gs - sr.Rf (Liminf_llist Gs)" and
     ground_C: "is_ground_cls C"
   shows "\<exists>D' \<sigma>'. D' \<in> Q_of_state (Liminf_state Sts) \<and> D' \<cdot> \<sigma>' = C \<and> is_ground_subst \<sigma>'"
 proof -
   let ?Ns = "\<lambda>i. N_of_state (lnth Sts i)"
   let ?Ps = "\<lambda>i. P_of_state (lnth Sts i)"
   let ?Qs = "\<lambda>i. Q_of_state (lnth Sts i)"
 
   from D_p obtain i where
     i_p: "i < llength Sts" "D \<in> ?Ns i \<or> D \<in> ?Ps i \<or> D \<in> ?Qs i"
     unfolding Sup_state_def
-    by simp_all (metis (no_types) in_Sup_llist_in_nth llength_lmap lnth_lmap)
+    by simp_all (metis (no_types) Sup_llist_imp_exists_index llength_lmap lnth_lmap)
 
   have derivns: "chain sr_ext.derive Gs"
     using ground_derive_chain deriv ns by auto
 
   have "\<exists>\<sigma>. D \<cdot> \<sigma> = C \<and> is_ground_subst \<sigma>"
     using instance_if_subsumed_and_in_limit[OF deriv ns c] D_p i_p by blast
   then obtain \<sigma> where
     \<sigma>: "D \<cdot> \<sigma> = C" "is_ground_subst \<sigma>"
     by blast
 
   {
     assume a: "D \<in> ?Ns i"
     then obtain D' \<sigma>' l where D'_p:
       "D' \<in> ?Ps l \<union> ?Qs l"
       "D' \<cdot> \<sigma>' = C"
       "enat l < llength Sts"
       "is_ground_subst \<sigma>'"
       "\<forall>E \<in> {E. E \<in> (clss_of_state (Sup_state Sts)) \<and> subsumes E C}. \<not> strictly_subsumes E D'"
       "subsumes D' C"
       using from_N_to_P_or_Q deriv fair ns c i_p(1) D_p(2) D_p(3) by blast
     then obtain l' where
       l'_p: "D' \<in> ?Qs l'" "l' < llength Sts"
       using from_P_to_Q[OF deriv fair ns c _ D'_p(3) D'_p(6) D'_p(5)] by blast
     then have "D' \<in> Q_of_state (Liminf_state Sts)"
       using from_Q_to_Q_inf[OF deriv fair ns c _ l'_p(2)] D'_p by auto
     then have ?thesis
       using D'_p by auto
   }
   moreover
   {
     assume a: "D \<in> ?Ps i"
     then obtain l' where
       l'_p: "D \<in> ?Qs l'" "l' < llength Sts"
       using from_P_to_Q[OF deriv fair ns c a i_p(1) D_p(2) D_p(3)] by auto
     then have "D \<in> Q_of_state (Liminf_state Sts)"
       using from_Q_to_Q_inf[OF deriv fair ns c l'_p(1) l'_p(2)] D_p(3) \<sigma>(1) \<sigma>(2) D_p(2) by auto
     then have ?thesis
       using D_p \<sigma> by auto
   }
   moreover
   {
     assume a: "D \<in> ?Qs i"
     then have "D \<in> Q_of_state (Liminf_state Sts)"
       using from_Q_to_Q_inf[OF deriv fair ns c a i_p(1)] \<sigma> D_p(2,3) by auto
     then have ?thesis
       using D_p \<sigma> by auto
   }
   ultimately show ?thesis
     using i_p by auto
 qed
 
 text \<open>
 The following corresponds to Lemma 4.11:
 \<close>
 
 lemma fair_imp_Liminf_minus_Rf_subset_ground_Liminf_state:
   assumes
     deriv: "chain (\<leadsto>) Sts" and
     fair: "fair_state_seq Sts" and
     ns: "Gs = lmap grounding_of_state Sts"
   shows "Liminf_llist Gs - sr.Rf (Liminf_llist Gs)
     \<subseteq> grounding_of_clss (Q_of_state (Liminf_state Sts))"
 proof
   let ?Ns = "\<lambda>i. N_of_state (lnth Sts i)"
   let ?Ps = "\<lambda>i. P_of_state (lnth Sts i)"
   let ?Qs = "\<lambda>i. Q_of_state (lnth Sts i)"
 
   have SQinf: "clss_of_state (Liminf_state Sts) = Liminf_llist (lmap Q_of_state Sts)"
     using fair unfolding fair_state_seq_def Liminf_state_def by auto
 
   fix C
   assume C_p: "C \<in> Liminf_llist Gs - sr.Rf (Liminf_llist Gs)"
   then have "C \<in> Sup_llist Gs"
     using Liminf_llist_subset_Sup_llist[of Gs] by blast
   then obtain D_proto where
     "D_proto \<in> clss_of_state (Sup_state Sts) \<and> subsumes D_proto C"
     using in_Sup_llist_in_Sup_state unfolding ns subsumes_def by blast
   then obtain D where
     D_p: "D \<in> clss_of_state (Sup_state Sts)"
     "subsumes D C"
     "\<forall>E \<in> {E. E \<in> clss_of_state (Sup_state Sts) \<and> subsumes E C}. \<not> strictly_subsumes E D"
     using strictly_subsumes_has_minimum[of "{E. E \<in> clss_of_state (Sup_state Sts) \<and> subsumes E C}"]
     by auto
 
   have ground_C: "is_ground_cls C"
     using C_p using Liminf_grounding_of_state_ground ns by auto
 
   have "\<exists>D' \<sigma>'. D' \<in> Q_of_state (Liminf_state Sts) \<and> D' \<cdot> \<sigma>' = C \<and> is_ground_subst \<sigma>'"
     using eventually_in_Qinf[of D C Gs] using D_p(1-3) deriv fair ns C_p ground_C by auto
   then obtain D' \<sigma>' where
     D'_p: "D' \<in> Q_of_state (Liminf_state Sts) \<and> D' \<cdot> \<sigma>' = C \<and> is_ground_subst \<sigma>'"
     by blast
   then have "D' \<in> clss_of_state (Liminf_state Sts)"
     by simp
   then have "C \<in> grounding_of_state (Liminf_state Sts)"
     unfolding grounding_of_clss_def grounding_of_cls_def using D'_p by auto
   then show "C \<in> grounding_of_clss (Q_of_state (Liminf_state Sts))"
     using SQinf fair fair_state_seq_def by auto
 qed
 
 text \<open>
 The following corresponds to (one direction of) Theorem 4.13:
 \<close>
 
-lemma ground_subclauses:
-  assumes
-    "\<forall>i < length CAs. CAs ! i = Cs ! i + poss (AAs ! i)" and
-    "length Cs = length CAs" and
-    "is_ground_cls_list CAs"
-  shows "is_ground_cls_list Cs"
-  unfolding is_ground_cls_list_def
-  by (metis assms in_set_conv_nth is_ground_cls_list_def is_ground_cls_union)
-
 lemma subseteq_Liminf_state_eventually_always:
   fixes CC
   assumes
     "finite CC" and
     "CC \<noteq> {}" and
     "CC \<subseteq> Q_of_state (Liminf_state Sts)"
   shows "\<exists>j. enat j < llength Sts \<and> (\<forall>j' \<ge> enat j. j' < llength Sts \<longrightarrow> CC \<subseteq> Q_of_state (lnth Sts j'))"
 proof -
   from assms(3) have "\<forall>C \<in> CC. \<exists>j. enat j < llength Sts \<and>
     (\<forall>j' \<ge> enat j. j' < llength Sts \<longrightarrow> C \<in> Q_of_state (lnth Sts j'))"
     unfolding Liminf_state_def Liminf_llist_def by force
   then obtain f where
     f_p: "\<forall>C \<in> CC. f C < llength Sts \<and> (\<forall>j' \<ge> enat (f C). j' < llength Sts \<longrightarrow> C \<in> Q_of_state (lnth Sts j'))"
     by moura
 
   define j :: nat where
     "j = Max (f ` CC)"
 
   have "enat j < llength Sts"
     unfolding j_def using f_p assms(1)
     by (metis (mono_tags) Max_in assms(2) finite_imageI imageE image_is_empty)
   moreover have "\<forall>C j'. C \<in> CC \<longrightarrow> enat j \<le> j' \<longrightarrow> j' < llength Sts \<longrightarrow> C \<in> Q_of_state (lnth Sts j')"
   proof (intro allI impI)
     fix C :: "'a clause" and j' :: nat
     assume a: "C \<in> CC" "enat j \<le> enat j'" "enat j' < llength Sts"
     then have "f C \<le> j'"
       unfolding j_def using assms(1) Max.bounded_iff by auto
     then show "C \<in> Q_of_state (lnth Sts j')"
       using f_p a by auto
   qed
   ultimately show ?thesis
     by auto
 qed
 
 lemma empty_clause_in_Q_of_Liminf_state:
   assumes
     deriv: "chain (\<leadsto>) Sts" and
     fair: "fair_state_seq Sts" and
     empty_in: "{#} \<in> Liminf_llist (lmap grounding_of_state Sts)"
   shows "{#} \<in> Q_of_state (Liminf_state Sts)"
 proof -
   define Gs :: "'a clause set llist" where
     ns: "Gs = lmap grounding_of_state Sts"
   from empty_in have in_Liminf_not_Rf: "{#} \<in> Liminf_llist Gs - sr.Rf (Liminf_llist Gs)"
     unfolding ns sr.Rf_def by auto
   then have "{#} \<in> grounding_of_clss (Q_of_state (Liminf_state Sts))"
     using fair_imp_Liminf_minus_Rf_subset_ground_Liminf_state[OF deriv fair ns] by auto
   then show ?thesis
     unfolding grounding_of_clss_def grounding_of_cls_def by auto
 qed
 
 lemma grounding_of_state_Liminf_state_subseteq:
   "grounding_of_state (Liminf_state Sts) \<subseteq> Liminf_llist (lmap grounding_of_state Sts)"
 proof
   fix C :: "'a clause"
   assume "C \<in> grounding_of_state (Liminf_state Sts)"
   then obtain D \<sigma> where
     D_\<sigma>_p: "D \<in> clss_of_state (Liminf_state Sts)" "D \<cdot> \<sigma> = C" "is_ground_subst \<sigma>"
     unfolding grounding_of_clss_def grounding_of_cls_def by auto
   then have ii: "D \<in> Liminf_llist (lmap N_of_state Sts)
     \<or> D \<in> Liminf_llist (lmap P_of_state Sts) \<or> D \<in> Liminf_llist (lmap Q_of_state Sts)"
     unfolding Liminf_state_def by simp
   then have "C \<in> Liminf_llist (lmap grounding_of_clss (lmap N_of_state Sts))
     \<or> C \<in> Liminf_llist (lmap grounding_of_clss (lmap P_of_state Sts))
     \<or> C \<in> Liminf_llist (lmap grounding_of_clss (lmap Q_of_state Sts))"
     unfolding Liminf_llist_def grounding_of_clss_def grounding_of_cls_def
+    using D_\<sigma>_p
     apply -
     apply (erule disjE)
     subgoal
       apply (rule disjI1)
       using D_\<sigma>_p by auto
     subgoal
-      apply (erule HOL.disjE)
+      apply (erule disjE)
       subgoal
         apply (rule disjI2)
         apply (rule disjI1)
         using D_\<sigma>_p by auto
       subgoal
         apply (rule disjI2)
         apply (rule disjI2)
         using D_\<sigma>_p by auto
       done
     done
   then show "C \<in> Liminf_llist (lmap grounding_of_state Sts)"
     unfolding Liminf_llist_def grounding_of_clss_def by auto
 qed
 
 theorem RP_sound:
   assumes
     deriv: "chain (\<leadsto>) Sts" and
     "{#} \<in> clss_of_state (Liminf_state Sts)"
   shows "\<not> satisfiable (grounding_of_state (lhd Sts))"
 proof -
   from assms have "{#} \<in> grounding_of_state (Liminf_state Sts)"
     unfolding grounding_of_clss_def by (force intro: ex_ground_subst)
   then have "{#} \<in> Liminf_llist (lmap grounding_of_state Sts)"
     using grounding_of_state_Liminf_state_subseteq by auto
   then have "\<not> satisfiable (Liminf_llist (lmap grounding_of_state Sts))"
     using true_clss_def by auto
   then have "\<not> satisfiable (lhd (lmap grounding_of_state Sts))"
     using sr_ext.sat_limit_iff ground_derive_chain deriv by blast
   then show ?thesis
     using chain_not_lnull deriv by fastforce
 qed
 
 theorem RP_saturated_if_fair:
   assumes
     deriv: "chain (\<leadsto>) Sts" and
     fair: "fair_state_seq Sts" and
     empty_Q0: "Q_of_state (lhd Sts) = {}"
   shows "sr.saturated_upto (Liminf_llist (lmap grounding_of_state Sts))"
 proof -
   define Gs :: "'a clause set llist" where
     ns: "Gs = lmap grounding_of_state Sts"
 
   let ?N = "\<lambda>i. grounding_of_state (lnth Sts i)"
 
   let ?Ns = "\<lambda>i. N_of_state (lnth Sts i)"
   let ?Ps = "\<lambda>i. P_of_state (lnth Sts i)"
   let ?Qs = "\<lambda>i. Q_of_state (lnth Sts i)"
 
   have ground_ns_in_ground_limit_st:
     "Liminf_llist Gs - sr.Rf (Liminf_llist Gs) \<subseteq> grounding_of_clss (Q_of_state (Liminf_state Sts))"
     using fair deriv fair_imp_Liminf_minus_Rf_subset_ground_Liminf_state ns by blast
 
   have derivns: "chain sr_ext.derive Gs"
     using ground_derive_chain deriv ns by auto
 
   {
     fix \<gamma> :: "'a inference"
     assume \<gamma>_p: "\<gamma> \<in> gr.ord_\<Gamma>"
     let ?CC = "side_prems_of \<gamma>"
     let ?DA = "main_prem_of \<gamma>"
     let ?E = "concl_of \<gamma>"
     assume a: "set_mset ?CC \<union> {?DA}
       \<subseteq> Liminf_llist (lmap grounding_of_state Sts)
         - sr.Rf (Liminf_llist (lmap grounding_of_state Sts))"
 
     have ground_ground_Liminf: "is_ground_clss (Liminf_llist (lmap grounding_of_state Sts))"
       using Liminf_grounding_of_state_ground unfolding is_ground_clss_def by auto
 
     have ground_cc: "is_ground_clss (set_mset ?CC)"
       using a ground_ground_Liminf is_ground_clss_def by auto
 
     have ground_da: "is_ground_cls ?DA"
       using a grounding_ground singletonI ground_ground_Liminf
       by (simp add: Liminf_grounding_of_state_ground)
 
     from \<gamma>_p obtain CAs AAs As where
       CAs_p: "gr.ord_resolve CAs ?DA AAs As ?E \<and> mset CAs = ?CC"
       unfolding gr.ord_\<Gamma>_def by auto
 
     have DA_CAs_in_ground_Liminf:
       "{?DA} \<union> set CAs \<subseteq> grounding_of_clss (Q_of_state (Liminf_state Sts))"
       using a CAs_p fair unfolding fair_state_seq_def
       by (metis (no_types, lifting) Un_empty_left ground_ns_in_ground_limit_st a ns set_mset_mset
           subset_trans sup_commute)
 
     then have ground_cas: "is_ground_cls_list CAs"
       using CAs_p unfolding is_ground_cls_list_def by auto
 
     have "\<exists>\<sigma>. ord_resolve S_Q CAs ?DA AAs As \<sigma> ?E"
       by (rule ground_ord_resolve_imp_ord_resolve[OF ground_da ground_cas
             gr.ground_resolution_with_selection_axioms CAs_p[THEN conjunct1]])
     then obtain \<sigma> where
       \<sigma>_p: "ord_resolve S_Q CAs ?DA AAs As \<sigma> ?E"
       by auto
     then obtain \<eta>s' \<eta>' \<eta>2' CAs' DA' AAs' As' \<tau>' E' where s_p:
       "is_ground_subst \<eta>'"
       "is_ground_subst_list \<eta>s'"
       "is_ground_subst \<eta>2'"
       "ord_resolve_rename S CAs' DA' AAs' As' \<tau>' E'"
       "CAs' \<cdot>\<cdot>cl \<eta>s' = CAs"
       "DA' \<cdot> \<eta>' = ?DA"
       "E' \<cdot> \<eta>2' = ?E"
       "{DA'} \<union> set CAs' \<subseteq> Q_of_state (Liminf_state Sts)"
       using ord_resolve_rename_lifting[OF sel_stable, of "Q_of_state (Liminf_state Sts)" CAs ?DA]
         \<sigma>_p[unfolded S_Q_def] selection_axioms DA_CAs_in_ground_Liminf by metis
     from this(8) have "\<exists>j. enat j < llength Sts \<and> (set CAs' \<union> {DA'} \<subseteq> ?Qs j)"
       unfolding Liminf_llist_def
       using subseteq_Liminf_state_eventually_always[of "{DA'} \<union> set CAs'"] by auto
     then obtain j where
       j_p: "is_least (\<lambda>j. enat j < llength Sts \<and> set CAs' \<union> {DA'} \<subseteq> ?Qs j) j"
       using least_exists[of "\<lambda>j. enat j < llength Sts \<and> set CAs' \<union> {DA'} \<subseteq> ?Qs j"] by force
     then have j_p': "enat j < llength Sts" "set CAs' \<union> {DA'} \<subseteq> ?Qs j"
       unfolding is_least_def by auto
     then have jn0: "j \<noteq> 0"
       using empty_Q0 by (metis bot_eq_sup_iff gr_implies_not_zero insert_not_empty llength_lnull
           lnth_0_conv_lhd sup.orderE)
     then have j_adds_CAs': "\<not> set CAs' \<union> {DA'} \<subseteq> ?Qs (j - 1)" "set CAs' \<union> {DA'} \<subseteq> ?Qs j"
       using j_p unfolding is_least_def
        apply (metis (no_types) One_nat_def Suc_diff_Suc Suc_ile_eq diff_diff_cancel diff_zero
           less_imp_le less_one neq0_conv zero_less_diff)
       using j_p'(2) by blast
     have "lnth Sts (j - 1) \<leadsto> lnth Sts j"
       using j_p'(1) jn0 deriv chain_lnth_rel[of _ _ "j - 1"] by force
     then obtain C' where C'_p:
       "?Ns (j - 1) = {}"
       "?Ps (j - 1) = ?Ps j \<union> {C'}"
       "?Qs j = ?Qs (j - 1) \<union> {C'}"
       "?Ns j = concls_of (ord_FO_resolution.inferences_between (?Qs (j - 1)) C')"
       "C' \<in> set CAs' \<union> {DA'}"
       "C' \<notin> ?Qs (j - 1)"
       using j_adds_CAs' by (induction rule: RP.cases) auto
     have "E' \<in> ?Ns j"
     proof -
       have "E' \<in> concls_of (ord_FO_resolution.inferences_between (Q_of_state (lnth Sts (j - 1))) C')"
         unfolding infer_from_def ord_FO_\<Gamma>_def inference_system.inferences_between_def
         apply (rule_tac x = "Infer (mset CAs') DA' E'" in image_eqI)
         subgoal by auto
         subgoal
           unfolding infer_from_def
           by (rule ord_resolve_rename.cases[OF s_p(4)]) (use s_p(4) C'_p(3,5) j_p'(2) in force)
         done
       then show ?thesis
         using C'_p(4) by auto
     qed
     then have "E' \<in> clss_of_state (lnth Sts j)"
       using j_p' by auto
     then have "?E \<in> grounding_of_state (lnth Sts j)"
       using s_p(7) s_p(3) unfolding grounding_of_clss_def grounding_of_cls_def by force
     then have "\<gamma> \<in> sr.Ri (grounding_of_state (lnth Sts j))"
       using sr.Ri_effective \<gamma>_p by auto
     then have "\<gamma> \<in> sr_ext_Ri (?N j)"
       unfolding sr_ext_Ri_def by auto
     then have "\<gamma> \<in> sr_ext_Ri (Sup_llist (lmap grounding_of_state Sts))"
       using j_p' contra_subsetD llength_lmap lnth_lmap lnth_subset_Sup_llist sr_ext.Ri_mono by smt
     then have "\<gamma> \<in> sr_ext_Ri (Liminf_llist (lmap grounding_of_state Sts))"
       using sr_ext.Ri_limit_Sup[of Gs] derivns ns by blast
   }
   then have "sr_ext.saturated_upto (Liminf_llist (lmap grounding_of_state Sts))"
     unfolding sr_ext.saturated_upto_def sr_ext.inferences_from_def infer_from_def sr_ext_Ri_def
     by auto
   then show ?thesis
     using gd_ord_\<Gamma>_ngd_ord_\<Gamma> sr.redundancy_criterion_axioms
       redundancy_criterion_standard_extension_saturated_upto_iff[of gr.ord_\<Gamma>]
     unfolding sr_ext_Ri_def by auto
 qed
 
 corollary RP_complete_if_fair:
   assumes
     deriv: "chain (\<leadsto>) Sts" and
     fair: "fair_state_seq Sts" and
     empty_Q0: "Q_of_state (lhd Sts) = {}" and
     unsat: "\<not> satisfiable (grounding_of_state (lhd Sts))"
   shows "{#} \<in> Q_of_state (Liminf_state Sts)"
 proof -
   have "\<not> satisfiable (Liminf_llist (lmap grounding_of_state Sts))"
     using unsat sr_ext.sat_limit_iff[OF ground_derive_chain] chain_not_lnull deriv by fastforce
   moreover have "sr.saturated_upto (Liminf_llist (lmap grounding_of_state Sts))"
     by (rule RP_saturated_if_fair[OF deriv fair empty_Q0, simplified])
   ultimately have "{#} \<in> Liminf_llist (lmap grounding_of_state Sts)"
     using sr.saturated_upto_complete_if by auto
   then show ?thesis
     using empty_clause_in_Q_of_Liminf_state[OF deriv fair] by auto
 qed
 
 end
 
 end
 
 end
diff --git a/thys/Ordered_Resolution_Prover/Lazy_List_Liminf.thy b/thys/Ordered_Resolution_Prover/Lazy_List_Liminf.thy
--- a/thys/Ordered_Resolution_Prover/Lazy_List_Liminf.thy
+++ b/thys/Ordered_Resolution_Prover/Lazy_List_Liminf.thy
@@ -1,215 +1,218 @@
 (*  Title:       Liminf of Lazy Lists
     Author:      Jasmin Blanchette <j.c.blanchette at vu.nl>, 2014, 2017
     Author:      Dmitriy Traytel <traytel at inf.ethz.ch>, 2014
     Maintainer:  Jasmin Blanchette <j.c.blanchette at vu.nl>
 *)
 
 section \<open>Liminf of Lazy Lists\<close>
 
 theory Lazy_List_Liminf
   imports Coinductive.Coinductive_List
 begin
 
 text \<open>
 Lazy lists, as defined in the \emph{Archive of Formal Proofs}, provide finite and infinite lists in
 one type, defined coinductively. The present theory introduces the concept of the union of all
 elements of a lazy list of sets and the limit of such a lazy list. The definitions are stated more
 generally in terms of lattices. The basis for this theory is Section 4.1 (``Theorem Proving
 Processes'') of Bachmair and Ganzinger's chapter.
 \<close>
 
 definition Sup_llist :: "'a set llist \<Rightarrow> 'a set" where
   "Sup_llist Xs = (\<Union>i \<in> {i. enat i < llength Xs}. lnth Xs i)"
 
-lemma lnth_subset_Sup_llist: "enat i < llength xs \<Longrightarrow> lnth xs i \<subseteq> Sup_llist xs"
+lemma lnth_subset_Sup_llist: "enat i < llength Xs \<Longrightarrow> lnth Xs i \<subseteq> Sup_llist Xs"
+  unfolding Sup_llist_def by auto
+
+lemma Sup_llist_imp_exists_index: "x \<in> Sup_llist Xs \<Longrightarrow> \<exists>i. enat i < llength Xs \<and> x \<in> lnth Xs i"
   unfolding Sup_llist_def by auto
 
 lemma Sup_llist_LNil[simp]: "Sup_llist LNil = {}"
   unfolding Sup_llist_def by auto
 
 lemma Sup_llist_LCons[simp]: "Sup_llist (LCons X Xs) = X \<union> Sup_llist Xs"
   unfolding Sup_llist_def
 proof (intro subset_antisym subsetI)
   fix x
   assume "x \<in> (\<Union>i \<in> {i. enat i < llength (LCons X Xs)}. lnth (LCons X Xs) i)"
   then obtain i where len: "enat i < llength (LCons X Xs)" and nth: "x \<in> lnth (LCons X Xs) i"
     by blast
   from nth have "x \<in> X \<or> i > 0 \<and> x \<in> lnth Xs (i - 1)"
     by (metis lnth_LCons' neq0_conv)
   then have "x \<in> X \<or> (\<exists>i. enat i < llength Xs \<and> x \<in> lnth Xs i)"
     by (metis len Suc_pred' eSuc_enat iless_Suc_eq less_irrefl llength_LCons not_less order_trans)
   then show "x \<in> X \<union> (\<Union>i \<in> {i. enat i < llength Xs}. lnth Xs i)"
     by blast
 qed ((auto)[], metis i0_lb lnth_0 zero_enat_def, metis Suc_ile_eq lnth_Suc_LCons)
 
 lemma lhd_subset_Sup_llist: "\<not> lnull Xs \<Longrightarrow> lhd Xs \<subseteq> Sup_llist Xs"
   by (cases Xs) simp_all
 
 definition Sup_upto_llist :: "'a set llist \<Rightarrow> nat \<Rightarrow> 'a set" where
   "Sup_upto_llist Xs j = (\<Union>i \<in> {i. enat i < llength Xs \<and> i \<le> j}. lnth Xs i)"
 
 lemma Sup_upto_llist_0[simp]: "Sup_upto_llist Xs 0 = (if 0 < llength Xs then lnth Xs 0 else {})"
   unfolding Sup_upto_llist_def image_def by (simp add: enat_0)
 
 lemma Sup_upto_llist_Suc[simp]:
   "Sup_upto_llist Xs (Suc j) =
    Sup_upto_llist Xs j \<union> (if enat (Suc j) < llength Xs then lnth Xs (Suc j) else {})"
   unfolding Sup_upto_llist_def image_def by (auto intro: le_SucI elim: le_SucE)
 
 lemma Sup_upto_llist_mono: "j \<le> k \<Longrightarrow> Sup_upto_llist Xs j \<subseteq> Sup_upto_llist Xs k"
   unfolding Sup_upto_llist_def by auto
 
 lemma Sup_upto_llist_subset_Sup_llist: "j \<le> k \<Longrightarrow> Sup_upto_llist Xs j \<subseteq> Sup_llist Xs"
   unfolding Sup_llist_def Sup_upto_llist_def by auto
 
 lemma elem_Sup_llist_imp_Sup_upto_llist:
 	"x \<in> Sup_llist Xs \<Longrightarrow> \<exists>j < llength Xs. x \<in> Sup_upto_llist Xs j"
   unfolding Sup_llist_def Sup_upto_llist_def by blast
 
 lemma lnth_subset_Sup_upto_llist: "enat j < llength Xs \<Longrightarrow> lnth Xs j \<subseteq> Sup_upto_llist Xs j"
   unfolding Sup_upto_llist_def by auto
 
 lemma finite_Sup_llist_imp_Sup_upto_llist:
   assumes "finite X" and "X \<subseteq> Sup_llist Xs"
   shows "\<exists>k. X \<subseteq> Sup_upto_llist Xs k"
   using assms
 proof induct
   case (insert x X)
   then have x: "x \<in> Sup_llist Xs" and X: "X \<subseteq> Sup_llist Xs"
     by simp+
   from x obtain k where k: "x \<in> Sup_upto_llist Xs k"
     using elem_Sup_llist_imp_Sup_upto_llist by fast
   from X obtain k' where k': "X \<subseteq> Sup_upto_llist Xs k'"
     using insert.hyps(3) by fast
   have "insert x X \<subseteq> Sup_upto_llist Xs (max k k')"
     using k k'
     by (metis insert_absorb insert_subset Sup_upto_llist_mono max.cobounded2 max.commute
         order.trans)
   then show ?case
     by fast
 qed simp
 
 definition Liminf_llist :: "'a set llist \<Rightarrow> 'a set" where
   "Liminf_llist Xs =
    (\<Union>i \<in> {i. enat i < llength Xs}. \<Inter>j \<in> {j. i \<le> j \<and> enat j < llength Xs}. lnth Xs j)"
 
 lemma Liminf_llist_LNil[simp]: "Liminf_llist LNil = {}"
   unfolding Liminf_llist_def by simp
 
 lemma Liminf_llist_LCons:
   "Liminf_llist (LCons X Xs) = (if lnull Xs then X else Liminf_llist Xs)" (is "?lhs = ?rhs")
 proof (cases "lnull Xs")
   case nnull: False
   show ?thesis
   proof
     {
       fix x
       assume "\<exists>i. enat i \<le> llength Xs
         \<and> (\<forall>j. i \<le> j \<and> enat j \<le> llength Xs \<longrightarrow> x \<in> lnth (LCons X Xs) j)"
       then have "\<exists>i. enat (Suc i) \<le> llength Xs
         \<and> (\<forall>j. Suc i \<le> j \<and> enat j \<le> llength Xs \<longrightarrow> x \<in> lnth (LCons X Xs) j)"
         by (cases "llength Xs",
             metis not_lnull_conv[THEN iffD1, OF nnull] Suc_le_D eSuc_enat eSuc_ile_mono
               llength_LCons not_less_eq_eq zero_enat_def zero_le,
             metis Suc_leD enat_ord_code(3))
       then have "\<exists>i. enat i < llength Xs \<and> (\<forall>j. i \<le> j \<and> enat j < llength Xs \<longrightarrow> x \<in> lnth Xs j)"
         by (metis Suc_ile_eq Suc_n_not_le_n lift_Suc_mono_le lnth_Suc_LCons nat_le_linear)
     }
     then show "?lhs \<subseteq> ?rhs"
       by (simp add: Liminf_llist_def nnull) (rule subsetI, simp)
 
     {
       fix x
       assume "\<exists>i. enat i < llength Xs \<and> (\<forall>j. i \<le> j \<and> enat j < llength Xs \<longrightarrow> x \<in> lnth Xs j)"
       then obtain i where
         i: "enat i < llength Xs" and
         j: "\<forall>j. i \<le> j \<and> enat j < llength Xs \<longrightarrow> x \<in> lnth Xs j"
         by blast
 
       have "enat (Suc i) \<le> llength Xs"
         using i by (simp add: Suc_ile_eq)
       moreover have "\<forall>j. Suc i \<le> j \<and> enat j \<le> llength Xs \<longrightarrow> x \<in> lnth (LCons X Xs) j"
         using Suc_ile_eq Suc_le_D j by force
       ultimately have "\<exists>i. enat i \<le> llength Xs \<and> (\<forall>j. i \<le> j \<and> enat j \<le> llength Xs \<longrightarrow>
         x \<in> lnth (LCons X Xs) j)"
         by blast
     }
     then show "?rhs \<subseteq> ?lhs"
       by (simp add: Liminf_llist_def nnull) (rule subsetI, simp)
   qed
 qed (simp add: Liminf_llist_def enat_0_iff(1))
 
 lemma lfinite_Liminf_llist: "lfinite Xs \<Longrightarrow> Liminf_llist Xs = (if lnull Xs then {} else llast Xs)"
 proof (induction rule: lfinite_induct)
   case (LCons xs)
   then obtain y ys where
     xs: "xs = LCons y ys"
     by (meson not_lnull_conv)
   show ?case
     unfolding xs by (simp add: Liminf_llist_LCons LCons.IH[unfolded xs, simplified] llast_LCons)
 qed (simp add: Liminf_llist_def)
 
 lemma Liminf_llist_ltl: "\<not> lnull (ltl Xs) \<Longrightarrow> Liminf_llist Xs = Liminf_llist (ltl Xs)"
   by (metis Liminf_llist_LCons lhd_LCons_ltl lnull_ltlI)
 
 lemma Liminf_llist_subset_Sup_llist: "Liminf_llist Xs \<subseteq> Sup_llist Xs"
   unfolding Liminf_llist_def Sup_llist_def by fast
 
 lemma image_Liminf_llist_subset: "f ` Liminf_llist Ns \<subseteq> Liminf_llist (lmap ((`) f) Ns)"
   unfolding Liminf_llist_def by auto
 
 lemma Liminf_llist_imp_exists_index:
   "x \<in> Liminf_llist Xs \<Longrightarrow> \<exists>i. enat i < llength Xs \<and> x \<in> lnth Xs i"
   unfolding Liminf_llist_def by auto
 
 lemma Liminf_llist_lmap_image:
   assumes f_inj: "inj_on f (Sup_llist (lmap g xs))"
   shows "Liminf_llist (lmap (\<lambda>x. f ` g x) xs) = f ` Liminf_llist (lmap g xs)" (is "?lhs = ?rhs")
 proof
   show "?lhs \<subseteq> ?rhs"
   proof
     fix x
     assume "x \<in> Liminf_llist (lmap (\<lambda>x. f ` g x) xs)"
     then obtain i where
       i_lt: "enat i < llength xs" and
       x_in_fgj: "\<forall>j. i \<le> j \<longrightarrow> enat j < llength xs \<longrightarrow> x \<in> f ` g (lnth xs j)"
       unfolding Liminf_llist_def by auto
 
     have ex_in_gi: "\<exists>y. y \<in> g (lnth xs i) \<and> x = f y"
       using f_inj i_lt x_in_fgj unfolding inj_on_def Sup_llist_def by auto
     have "\<exists>y. \<forall>j. i \<le> j \<longrightarrow> enat j < llength xs \<longrightarrow> y \<in> g (lnth xs j) \<and> x = f y"
       apply (rule exI[of _ "SOME y. y \<in> g (lnth xs i) \<and> x = f y"])
       using someI_ex[OF ex_in_gi] x_in_fgj f_inj i_lt x_in_fgj unfolding inj_on_def Sup_llist_def
       by simp (metis (no_types, lifting) imageE)
     then show "x \<in> f ` Liminf_llist (lmap g xs)"
       using i_lt unfolding Liminf_llist_def by auto
   qed
 next
   show "?rhs \<subseteq> ?lhs"
     using image_Liminf_llist_subset[of f "lmap g xs", unfolded llist.map_comp] by auto
 qed
 
 lemma Liminf_llist_lmap_union:
   assumes "\<forall>x \<in> lset xs. \<forall>Y \<in> lset xs. g x \<inter> h Y = {}"
   shows "Liminf_llist (lmap (\<lambda>x. g x \<union> h x) xs) =
     Liminf_llist (lmap g xs) \<union> Liminf_llist (lmap h xs)" (is "?lhs = ?rhs")
 proof (intro equalityI subsetI)
   fix x
   assume x_in: "x \<in> ?lhs"
   then obtain i where
     i_lt: "enat i < llength xs" and
     j: "\<forall>j. i \<le> j \<and> enat j < llength xs \<longrightarrow> x \<in> g (lnth xs j) \<or> x \<in> h (lnth xs j)"
     using x_in[unfolded Liminf_llist_def, simplified] by blast
 
   then have "(\<exists>i'. enat i' < llength xs \<and> (\<forall>j. i' \<le> j \<and> enat j < llength xs \<longrightarrow> x \<in> g (lnth xs j)))
      \<or> (\<exists>i'. enat i' < llength xs \<and> (\<forall>j. i' \<le> j \<and> enat j < llength xs \<longrightarrow> x \<in> h (lnth xs j)))"
     using assms[unfolded disjoint_iff_not_equal] by (metis in_lset_conv_lnth)
   then show "x \<in> ?rhs"
     unfolding Liminf_llist_def by simp
 next
   fix x
   show "x \<in> ?rhs \<Longrightarrow> x \<in> ?lhs"
     using assms unfolding Liminf_llist_def by auto
 qed
 
 end