diff --git a/thys/Functional_Ordered_Resolution_Prover/Deterministic_FO_Ordered_Resolution_Prover.thy b/thys/Functional_Ordered_Resolution_Prover/Deterministic_FO_Ordered_Resolution_Prover.thy
--- a/thys/Functional_Ordered_Resolution_Prover/Deterministic_FO_Ordered_Resolution_Prover.thy
+++ b/thys/Functional_Ordered_Resolution_Prover/Deterministic_FO_Ordered_Resolution_Prover.thy
@@ -1,1778 +1,1753 @@
 (*  Title:       A Deterministic Ordered Resolution Prover for First-Order Clauses
     Author:      Jasmin Blanchette <j.c.blanchette at vu.nl>, 2017
     Author:      Anders Schlichtkrull <andschl at dtu.dk>, 2018
     Maintainer:  Anders Schlichtkrull <andschl at dtu.dk>
 *)
 
 section \<open>A Deterministic Ordered Resolution Prover for First-Order Clauses\<close>
 
 text \<open>
 The \<open>deterministic_RP\<close> prover introduced below is a deterministic program that works on finite
 lists, committing to a strategy for assigning priorities to clauses. However, it is not fully
 executable: It abstracts over operations on atoms and employs logical specifications instead of
 executable functions for auxiliary notions.
 \<close>
 
 theory Deterministic_FO_Ordered_Resolution_Prover
-  imports Polynomial_Factorization.Missing_List Weighted_FO_Ordered_Resolution_Prover
+  imports
+    Polynomial_Factorization.Missing_List
+    Weighted_FO_Ordered_Resolution_Prover
+    Lambda_Free_RPOs.Lambda_Free_Util
 begin
 
 
 subsection \<open>Library\<close>
 
 lemma apfst_fst_snd: "apfst f x = (f (fst x), snd x)"
   by (rule apfst_conv[of _ "fst x" "snd x" for x, unfolded prod.collapse])
 
 lemma apfst_comp_rpair_const: "apfst f \<circ> (\<lambda>x. (x, y)) = (\<lambda>x. (x, y)) \<circ> f"
   by (simp add: comp_def)
 
 (* TODO: Move to Isabelle's "List.thy"? *)
 lemma length_remove1_less[termination_simp]: "x \<in> set xs \<Longrightarrow> length (remove1 x xs) < length xs"
   by (induct xs) auto
 
-(* TODO: Move to "Multiset_More.thy". *)
-lemma subset_mset_imp_subset_add_mset: "A \<subseteq># B \<Longrightarrow> A \<subseteq># add_mset x B"
-  by (metis add_mset_diff_bothsides diff_subset_eq_self multiset_inter_def subset_mset.inf.absorb2)
-
-(* TODO: Move to "Multiset_More.thy"? *)
-lemma subseq_mset_subseteq_mset: "subseq xs ys \<Longrightarrow> mset xs \<subseteq># mset ys"
-proof (induct xs arbitrary: ys)
-  case (Cons x xs)
-  note Outer_Cons = this
-  then show ?case
-  proof (induct ys)
-    case (Cons y ys)
-    have "subseq xs ys"
-      by (metis Cons.prems(2) subseq_Cons' subseq_Cons2_iff)
-    then show ?case
-      using Cons by (metis mset.simps(2) mset_subset_eq_add_mset_cancel subseq_Cons2_iff
-          subset_mset_imp_subset_add_mset)
-  qed simp
-qed simp
-
 lemma map_filter_neq_eq_filter_map:
   "map f (filter (\<lambda>y. f x \<noteq> f y) xs) = filter (\<lambda>z. f x \<noteq> z) (map f xs)"
   by (induct xs) auto
 
 lemma mset_map_remdups_gen:
   "mset (map f (remdups_gen f xs)) = mset (remdups_gen (\<lambda>x. x) (map f xs))"
   by (induct f xs rule: remdups_gen.induct) (auto simp: map_filter_neq_eq_filter_map)
 
 lemma mset_remdups_gen_ident: "mset (remdups_gen (\<lambda>x. x) xs) = mset_set (set xs)"
 proof -
   have "f = (\<lambda>x. x) \<Longrightarrow> mset (remdups_gen f xs) = mset_set (set xs)" for f
   proof (induct f xs rule: remdups_gen.induct)
     case (2 f x xs)
     note ih = this(1) and f = this(2)
     show ?case
       unfolding f remdups_gen.simps ih[OF f, unfolded f] mset.simps
       by (metis finite_set list.simps(15) mset_set.insert_remove removeAll_filter_not_eq
           remove_code(1) remove_def)
   qed simp
   then show ?thesis
     by simp
 qed
 
-(* FIXME: This is a clone of "Lambda_Free_RPOs". *)
-lemma wf_app: "wf r \<Longrightarrow> wf {(x, y). (f x, f y) \<in> r}"
-  unfolding wf_eq_minimal by (intro allI, drule spec[of _ "f ` Q" for Q]) fast
-
-(* FIXME: This is a clone of "Lambda_Free_RPOs". *)
-lemma wfP_app: "wfP p \<Longrightarrow> wfP (\<lambda>x y. p (f x) (f y))"
-  unfolding wfP_def by (rule wf_app[of "{(x, y). p x y}" f, simplified])
-
 (* TODO: Move to Isabelle? *)
 lemma funpow_fixpoint: "f x = x \<Longrightarrow> (f ^^ n) x = x"
   by (induct n) auto
 
 lemma rtranclp_imp_eq_image: "(\<forall>x y. R x y \<longrightarrow> f x = f y) \<Longrightarrow> R\<^sup>*\<^sup>* x y \<Longrightarrow> f x = f y"
   by (erule rtranclp.induct) auto
 
 lemma tranclp_imp_eq_image: "(\<forall>x y. R x y \<longrightarrow> f x = f y) \<Longrightarrow> R\<^sup>+\<^sup>+ x y \<Longrightarrow> f x = f y"
   by (erule tranclp.induct) auto
 
 
 subsection \<open>Prover\<close>
 
 type_synonym 'a lclause = "'a literal list"
 type_synonym 'a dclause = "'a lclause \<times> nat"
 type_synonym 'a dstate = "'a dclause list \<times> 'a dclause list \<times> 'a dclause list \<times> nat"
 
 locale deterministic_FO_resolution_prover =
   weighted_FO_resolution_prover_with_size_timestamp_factors S subst_atm id_subst comp_subst
     renamings_apart atm_of_atms mgu less_atm size_atm timestamp_factor size_factor
   for
     S :: "('a :: wellorder) clause \<Rightarrow> 'a clause" and
     subst_atm :: "'a \<Rightarrow> 's \<Rightarrow> 'a" and
     id_subst :: "'s" and
     comp_subst :: "'s \<Rightarrow> 's \<Rightarrow> 's" and
     renamings_apart :: "'a literal multiset list \<Rightarrow> 's list" and
     atm_of_atms :: "'a list \<Rightarrow> 'a" and
     mgu :: "'a set set \<Rightarrow> 's option" and
     less_atm :: "'a \<Rightarrow> 'a \<Rightarrow> bool" and
     size_atm :: "'a \<Rightarrow> nat" and
     timestamp_factor :: nat and
     size_factor :: nat +
   assumes
     S_empty: "S C = {#}"
 begin
 
 lemma less_atm_irrefl: "\<not> less_atm A A"
   using ex_ground_subst less_atm_ground less_atm_stable unfolding is_ground_subst_def by blast
 
 fun wstate_of_dstate :: "'a dstate \<Rightarrow> 'a wstate" where
   "wstate_of_dstate (N, P, Q, n) =
    (mset (map (apfst mset) N), mset (map (apfst mset) P), mset (map (apfst mset) Q), n)"
 
 fun state_of_dstate :: "'a dstate \<Rightarrow> 'a state" where
   "state_of_dstate (N, P, Q, _) =
    (set (map (mset \<circ> fst) N), set (map (mset \<circ> fst) P), set (map (mset \<circ> fst) Q))"
 
 abbreviation clss_of_dstate :: "'a dstate \<Rightarrow> 'a clause set" where
   "clss_of_dstate St \<equiv> clss_of_state (state_of_dstate St)"
 
 fun is_final_dstate :: "'a dstate \<Rightarrow> bool" where
   "is_final_dstate (N, P, Q, n) \<longleftrightarrow> N = [] \<and> P = []"
 
 declare is_final_dstate.simps [simp del]
 
 abbreviation rtrancl_weighted_RP (infix "\<leadsto>\<^sub>w\<^sup>*" 50) where
   "(\<leadsto>\<^sub>w\<^sup>*) \<equiv> (\<leadsto>\<^sub>w)\<^sup>*\<^sup>*"
 
 abbreviation trancl_weighted_RP (infix "\<leadsto>\<^sub>w\<^sup>+" 50) where
   "(\<leadsto>\<^sub>w\<^sup>+) \<equiv> (\<leadsto>\<^sub>w)\<^sup>+\<^sup>+"
 
 definition is_tautology :: "'a lclause \<Rightarrow> bool" where
   "is_tautology C \<longleftrightarrow> (\<exists>A \<in> set (map atm_of C). Pos A \<in> set C \<and> Neg A \<in> set C)"
 
 definition subsume :: "'a lclause list \<Rightarrow> 'a lclause \<Rightarrow> bool" where
   "subsume Ds C \<longleftrightarrow> (\<exists>D \<in> set Ds. subsumes (mset D) (mset C))"
 
 definition strictly_subsume :: "'a lclause list \<Rightarrow> 'a lclause \<Rightarrow> bool" where
   "strictly_subsume Ds C \<longleftrightarrow> (\<exists>D \<in> set Ds. strictly_subsumes (mset D) (mset C))"
 
 definition is_reducible_on :: "'a literal \<Rightarrow> 'a lclause \<Rightarrow> 'a literal \<Rightarrow> 'a lclause \<Rightarrow> bool" where
   "is_reducible_on M D L C \<longleftrightarrow> subsumes (mset D + {#- M#}) (mset C + {#L#})"
 
 definition is_reducible_lit :: "'a lclause list \<Rightarrow> 'a lclause \<Rightarrow> 'a literal \<Rightarrow> bool" where
   "is_reducible_lit Ds C L \<longleftrightarrow>
    (\<exists>D \<in> set Ds. \<exists>L' \<in> set D. \<exists>\<sigma>. - L = L' \<cdot>l \<sigma> \<and> mset (remove1 L' D) \<cdot> \<sigma> \<subseteq># mset C)"
 
 primrec reduce :: "'a lclause list \<Rightarrow> 'a lclause \<Rightarrow> 'a lclause \<Rightarrow> 'a lclause" where
   "reduce _ _ [] = []"
 | "reduce Ds C (L # C') =
    (if is_reducible_lit Ds (C @ C') L then reduce Ds C C' else L # reduce Ds (L # C) C')"
 
 abbreviation is_irreducible :: "'a lclause list \<Rightarrow> 'a lclause \<Rightarrow> bool" where
   "is_irreducible Ds C \<equiv> reduce Ds [] C = C"
 
 abbreviation is_reducible :: "'a lclause list \<Rightarrow> 'a lclause \<Rightarrow> bool" where
   "is_reducible Ds C \<equiv> reduce Ds [] C \<noteq> C"
 
 definition reduce_all :: "'a lclause \<Rightarrow> 'a dclause list \<Rightarrow> 'a dclause list" where
   "reduce_all D = map (apfst (reduce [D] []))"
 
 fun reduce_all2 :: "'a lclause \<Rightarrow> 'a dclause list \<Rightarrow> 'a dclause list \<times> 'a dclause list" where
   "reduce_all2 _ [] = ([], [])"
 | "reduce_all2 D (Ci # Cs) =
    (let
       (C, i) = Ci;
       C' = reduce [D] [] C
     in
       (if C' = C then apsnd else apfst) (Cons (C', i)) (reduce_all2 D Cs))"
 
 fun remove_all :: "'b list \<Rightarrow> 'b list \<Rightarrow> 'b list" where
   "remove_all xs [] = xs"
 | "remove_all xs (y # ys) = (if y \<in> set xs then remove_all (remove1 y xs) ys else remove_all xs ys)"
 
 lemma remove_all_mset_minus: "mset ys \<subseteq># mset xs \<Longrightarrow> mset (remove_all xs ys) = mset xs - mset ys"
 proof (induction ys arbitrary: xs)
   case (Cons y ys)
   show ?case
   proof (cases "y \<in> set xs")
     case y_in: True
     then have subs: "mset ys \<subseteq># mset (remove1 y xs)"
       using Cons(2) by (simp add: insert_subset_eq_iff)
     show ?thesis
       using y_in Cons subs by auto
   next
     case False
     then show ?thesis
       using Cons by auto
   qed
 qed auto
 
 definition resolvent :: "'a lclause \<Rightarrow> 'a \<Rightarrow>'a lclause \<Rightarrow> 'a lclause \<Rightarrow> 'a lclause" where
   "resolvent D A CA Ls =
    map (\<lambda>M. M \<cdot>l (the (mgu {insert A (atms_of (mset Ls))}))) (remove_all CA Ls @ D)"
 
 definition resolvable :: "'a \<Rightarrow> 'a lclause \<Rightarrow> 'a lclause \<Rightarrow> 'a lclause \<Rightarrow> bool" where
   "resolvable A D CA Ls \<longleftrightarrow>
    (let \<sigma> = (mgu {insert A (atms_of (mset Ls))}) in
         \<sigma> \<noteq> None
       \<and> Ls \<noteq> []
       \<and> maximal_wrt (A \<cdot>a the \<sigma>) ((add_mset (Neg A) (mset D)) \<cdot> the \<sigma>)
       \<and> strictly_maximal_wrt (A \<cdot>a the \<sigma>) ((mset CA - mset Ls) \<cdot> the \<sigma>)
       \<and> (\<forall>L \<in> set Ls. is_pos L))"
 
 definition resolve_on :: "'a \<Rightarrow> 'a lclause \<Rightarrow> 'a lclause \<Rightarrow> 'a lclause list" where
   "resolve_on A D CA = map (resolvent D A CA) (filter (resolvable A D CA) (subseqs CA))"
 
 definition resolve :: "'a lclause \<Rightarrow> 'a lclause \<Rightarrow> 'a lclause list" where
   "resolve C D =
    concat (map (\<lambda>L.
      (case L of
         Pos A \<Rightarrow> []
       | Neg A \<Rightarrow>
         if maximal_wrt A (mset D) then
           resolve_on A (remove1 L D) C
         else
           [])) D)"
 
 definition resolve_rename :: "'a lclause \<Rightarrow> 'a lclause \<Rightarrow> 'a lclause list" where
   "resolve_rename C D =
    (let \<sigma>s = renamings_apart [mset D, mset C] in
       resolve (map (\<lambda>L. L \<cdot>l last \<sigma>s) C) (map (\<lambda>L. L \<cdot>l hd \<sigma>s) D))"
 
 definition resolve_rename_either_way :: "'a lclause \<Rightarrow> 'a lclause \<Rightarrow> 'a lclause list" where
   "resolve_rename_either_way C D = resolve_rename C D @ resolve_rename D C"
 
 fun select_min_weight_clause :: "'a dclause \<Rightarrow> 'a dclause list \<Rightarrow> 'a dclause" where
   "select_min_weight_clause Ci [] = Ci"
 | "select_min_weight_clause Ci (Dj # Djs) =
    select_min_weight_clause
      (if weight (apfst mset Dj) < weight (apfst mset Ci) then Dj else Ci) Djs"
 
 lemma select_min_weight_clause_in: "select_min_weight_clause P0 P \<in> set (P0 # P)"
   by (induct P arbitrary: P0) auto
 
 function remdups_clss :: "'a dclause list \<Rightarrow> 'a dclause list" where
   "remdups_clss [] = []"
 | "remdups_clss (Ci # Cis) =
    (let
       Ci' = select_min_weight_clause Ci Cis
     in
       Ci' # remdups_clss (filter (\<lambda>(D, _). mset D \<noteq> mset (fst Ci')) (Ci # Cis)))"
   by pat_completeness auto
   termination
     apply (relation "measure length")
      apply (rule wf_measure)
     by (metis (mono_tags) in_measure length_filter_less prod.case_eq_if select_min_weight_clause_in)
 
 declare remdups_clss.simps(2) [simp del]
 
 fun deterministic_RP_step :: "'a dstate \<Rightarrow> 'a dstate" where
   "deterministic_RP_step (N, P, Q, n) =
    (if \<exists>Ci \<in> set (P @ Q). fst Ci = [] then
       ([], [], remdups_clss P @ Q, n + length (remdups_clss P))
     else
       (case N of
         [] \<Rightarrow>
         (case P of
            [] \<Rightarrow> (N, P, Q, n)
          | P0 # P' \<Rightarrow>
            let
              (C, i) = select_min_weight_clause P0 P';
              N = map (\<lambda>D. (D, n)) (remdups_gen mset (resolve_rename C C
                @ concat (map (resolve_rename_either_way C \<circ> fst) Q)));
              P = filter (\<lambda>(D, j). mset D \<noteq> mset C) P;
              Q = (C, i) # Q;
              n = Suc n
            in
              (N, P, Q, n))
       | (C, i) # N \<Rightarrow>
         let
           C = reduce (map fst (P @ Q)) [] C
         in
           if C = [] then
             ([], [], [([], i)], Suc n)
           else if is_tautology C \<or> subsume (map fst (P @ Q)) C then
             (N, P, Q, n)
           else
             let
               P = reduce_all C P;
               (back_to_P, Q) = reduce_all2 C Q;
               P = back_to_P @ P;
               Q = filter (Not \<circ> strictly_subsume [C] \<circ> fst) Q;
               P = filter (Not \<circ> strictly_subsume [C] \<circ> fst) P;
               P = (C, i) # P
             in
               (N, P, Q, n)))"
 
 declare deterministic_RP_step.simps [simp del]
 
 partial_function (option) deterministic_RP :: "'a dstate \<Rightarrow> 'a lclause list option" where
   "deterministic_RP St =
    (if is_final_dstate St then
       let (_, _, Q, _) = St in Some (map fst Q)
     else
       deterministic_RP (deterministic_RP_step St))"
 
 lemma is_final_dstate_imp_not_weighted_RP: "is_final_dstate St \<Longrightarrow> \<not> wstate_of_dstate St \<leadsto>\<^sub>w St'"
   using wrp.final_weighted_RP
   by (cases St) (auto intro: wrp.final_weighted_RP simp: is_final_dstate.simps)
 
 lemma is_final_dstate_funpow_imp_deterministic_RP_neq_None:
   "is_final_dstate ((deterministic_RP_step ^^ k) St) \<Longrightarrow> deterministic_RP St \<noteq> None"
 proof (induct k arbitrary: St)
   case (Suc k)
   note ih = this(1) and final_Sk = this(2)[simplified, unfolded funpow_swap1]
   show ?case
     using ih[OF final_Sk] by (subst deterministic_RP.simps) (simp add: prod.case_eq_if)
 qed (subst deterministic_RP.simps, simp add: prod.case_eq_if)
 
 lemma is_reducible_lit_mono_cls:
   "mset C \<subseteq># mset C' \<Longrightarrow> is_reducible_lit Ds C L \<Longrightarrow> is_reducible_lit Ds C' L"
   unfolding is_reducible_lit_def by (blast intro: subset_mset.order.trans)
 
 lemma is_reducible_lit_mset_iff:
   "mset C = mset C' \<Longrightarrow> is_reducible_lit Ds C' L \<longleftrightarrow> is_reducible_lit Ds C L"
   by (metis is_reducible_lit_mono_cls subset_mset.order_refl)
 
 lemma is_reducible_lit_remove1_Cons_iff:
   assumes "L \<in> set C'"
   shows "is_reducible_lit Ds (C @ remove1 L (M # C')) L \<longleftrightarrow>
     is_reducible_lit Ds (M # C @ remove1 L C') L"
   using assms by (subst is_reducible_lit_mset_iff, auto)
 
 lemma reduce_mset_eq: "mset C = mset C' \<Longrightarrow> reduce Ds C E = reduce Ds C' E"
 proof (induct E arbitrary: C C')
   case (Cons L E)
   note ih = this(1) and mset_eq = this(2)
   have
     mset_lc_eq: "mset (L # C) = mset (L # C')" and
     mset_ce_eq: "mset (C @ E) = mset (C' @ E)"
     using mset_eq by simp+
   show ?case
     using ih[OF mset_eq] ih[OF mset_lc_eq] by (simp add: is_reducible_lit_mset_iff[OF mset_ce_eq])
 qed simp
 
 lemma reduce_rotate[simp]: "reduce Ds (C @ [L]) E = reduce Ds (L # C) E"
   by (rule reduce_mset_eq) simp
 
 lemma mset_reduce_subset: "mset (reduce Ds C E) \<subseteq># mset E"
   by (induct E arbitrary: C) (auto intro: subset_mset_imp_subset_add_mset)
 
 lemma reduce_idem: "reduce Ds C (reduce Ds C E) = reduce Ds C E"
   by (induct E arbitrary: C)
     (auto intro!: mset_reduce_subset
       dest!: is_reducible_lit_mono_cls[of "C @ reduce Ds (L # C) E" "C @ E" Ds L for L E C,
         rotated])
 
 lemma is_reducible_lit_imp_is_reducible:
   "L \<in> set C' \<Longrightarrow> is_reducible_lit Ds (C @ remove1 L C') L \<Longrightarrow> reduce Ds C C' \<noteq> C'"
 proof (induct C' arbitrary: C)
   case (Cons M C')
   note ih = this(1) and l_in = this(2) and l_red = this(3)
 
   show ?case
   proof (cases "is_reducible_lit Ds (C @ C') M")
     case True
     then show ?thesis
       by simp (metis mset.simps(2) mset_reduce_subset multi_self_add_other_not_self
           subset_mset.eq_iff subset_mset_imp_subset_add_mset)
   next
     case m_irred: False
     have
       "L \<in> set C'" and
       "is_reducible_lit Ds (M # C @ remove1 L C') L"
       using l_in l_red m_irred is_reducible_lit_remove1_Cons_iff by auto
     then show ?thesis
       by (simp add: ih[of "M # C"] m_irred)
   qed
 qed simp
 
 lemma is_reducible_imp_is_reducible_lit:
   "reduce Ds C C' \<noteq> C' \<Longrightarrow> \<exists>L \<in> set C'. is_reducible_lit Ds (C @ remove1 L C') L"
 proof (induct C' arbitrary: C)
   case (Cons M C')
   note ih = this(1) and mc'_red = this(2)
 
   show ?case
   proof (cases "is_reducible_lit Ds (C @ C') M")
     case m_irred: False
     show ?thesis
       using ih[of "M # C"] mc'_red[simplified, simplified m_irred, simplified] m_irred
         is_reducible_lit_remove1_Cons_iff
       by auto
   qed simp
 qed simp
 
 lemma is_irreducible_iff_nexists_is_reducible_lit:
   "reduce Ds C C' = C' \<longleftrightarrow> \<not> (\<exists>L \<in> set C'. is_reducible_lit Ds (C @ remove1 L C') L)"
   using is_reducible_imp_is_reducible_lit is_reducible_lit_imp_is_reducible by blast
 
 lemma is_irreducible_mset_iff: "mset E = mset E' \<Longrightarrow> reduce Ds C E = E \<longleftrightarrow> reduce Ds C E' = E'"
   unfolding is_irreducible_iff_nexists_is_reducible_lit
   by (metis (full_types) is_reducible_lit_mset_iff mset_remove1 set_mset_mset union_code)
 
 lemma select_min_weight_clause_min_weight:
   assumes "Ci = select_min_weight_clause P0 P"
   shows "weight (apfst mset Ci) = Min ((weight \<circ> apfst mset) ` set (P0 # P))"
   using assms
 proof (induct P arbitrary: P0 Ci)
   case (Cons P1 P)
   note ih = this(1) and ci = this(2)
 
   show ?case
   proof (cases "weight (apfst mset P1) < weight (apfst mset P0)")
     case True
     then have min: "Min ((weight \<circ> apfst mset) ` set (P0 # P1 # P)) =
       Min ((weight \<circ> apfst mset) ` set (P1 # P))"
       by (simp add: min_def)
     show ?thesis
       unfolding min by (rule ih[of Ci P1]) (simp add: ih[of Ci P1] ci True)
   next
     case False
     have "Min ((weight \<circ> apfst mset) ` set (P0 # P1 # P)) =
       Min ((weight \<circ> apfst mset) ` set (P1 # P0 # P))"
       by (rule arg_cong[of _ _ Min]) auto
     then have min: "Min ((weight \<circ> apfst mset) ` set (P0 # P1 # P)) =
       Min ((weight \<circ> apfst mset) ` set (P0 # P))"
       by (simp add: min_def) (use False eq_iff in fastforce)
     show ?thesis
       unfolding min by (rule ih[of Ci P0]) (simp add: ih[of Ci P1] ci False)
   qed
 qed simp
 
 lemma remdups_clss_Nil_iff: "remdups_clss Cs = [] \<longleftrightarrow> Cs = []"
   by (cases Cs, simp, hypsubst, subst remdups_clss.simps(2), simp add: Let_def)
 
 lemma empty_N_if_Nil_in_P_or_Q:
   assumes nil_in: "[] \<in> fst ` set (P @ Q)"
   shows "wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], P, Q, n)"
 proof (induct N)
   case ih: (Cons N0 N)
   have "wstate_of_dstate (N0 # N, P, Q, n) \<leadsto>\<^sub>w wstate_of_dstate (N, P, Q, n)"
     by (rule arg_cong2[THEN iffD1, of _ _ _ _ "(\<leadsto>\<^sub>w)", OF _ _
           wrp.forward_subsumption[of "{#}" "mset (map (apfst mset) P)" "mset (map (apfst mset) Q)"
             "mset (fst N0)" "mset (map (apfst mset) N)" "snd N0" n]])
       (use nil_in in \<open>force simp: image_def apfst_fst_snd\<close>)+
   then show ?case
     using ih by (rule converse_rtranclp_into_rtranclp)
 qed simp
 
 lemma remove_strictly_subsumed_clauses_in_P:
   assumes
     c_in: "C \<in> fst ` set N" and
     p_nsubs: "\<forall>D \<in> fst ` set P. \<not> strictly_subsume [C] D"
   shows "wstate_of_dstate (N, P @ P', Q, n)
     \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) P', Q, n)"
   using p_nsubs
 proof (induct "length P'" arbitrary: P P' rule: less_induct)
   case less
   note ih = this(1) and p_nsubs = this(2)
 
   show ?case
   proof (cases "length P'")
     case Suc
 
     let ?Dj = "hd P'"
     let ?P'' = "tl P'"
     have p': "P' = hd P' # tl P'"
       using Suc by (metis length_Suc_conv list.distinct(1) list.exhaust_sel)
 
     show ?thesis
     proof (cases "strictly_subsume [C] (fst ?Dj)")
       case subs: True
 
       have p_filtered: "{#(E, k) \<in># image_mset (apfst mset) (mset P). E \<noteq> mset (fst ?Dj)#} =
         image_mset (apfst mset) (mset P)"
         by (rule filter_mset_cong[OF refl, of _ _ "\<lambda>_. True", simplified],
             use subs p_nsubs in \<open>auto simp: strictly_subsume_def\<close>)
       have "{#(E, k) \<in># image_mset (apfst mset) (mset P'). E \<noteq> mset (fst ?Dj)#} =
         {#(E, k) \<in># image_mset (apfst mset) (mset ?P''). E \<noteq> mset (fst ?Dj)#}"
         by (subst (2) p') (simp add: case_prod_beta)
       also have "\<dots> =
         image_mset (apfst mset) (mset (filter (\<lambda>(E, l). mset E \<noteq> mset (fst ?Dj)) ?P''))"
-        by (auto simp: image_mset_filter_swap[symmetric] mset_filter case_prod_beta)
+        by (auto simp: image_mset_filter_swap[symmetric] case_prod_beta)
       finally have p'_filtered:
         "{#(E, k) \<in># image_mset (apfst mset) (mset P'). E \<noteq> mset (fst ?Dj)#} =
         image_mset (apfst mset) (mset (filter (\<lambda>(E, l). mset E \<noteq> mset (fst ?Dj)) ?P''))"
         .
 
       have "wstate_of_dstate (N, P @ P', Q, n)
         \<leadsto>\<^sub>w wstate_of_dstate (N, P @ filter (\<lambda>(E, l). mset E \<noteq> mset (fst ?Dj)) ?P'', Q, n)"
         by (rule arg_cong2[THEN iffD1, of _ _ _ _ "(\<leadsto>\<^sub>w)", OF _ _
               wrp.backward_subsumption_P[of "mset C" "mset (map (apfst mset) N)" "mset (fst ?Dj)"
                 "mset (map (apfst mset) (P @ P'))" "mset (map (apfst mset) Q)" n]],
           use c_in subs in \<open>auto simp add: p_filtered p'_filtered arg_cong[OF p', of set]
             strictly_subsume_def\<close>)
       also have "\<dots>
         \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) P', Q, n)"
         apply (rule arg_cong2[THEN iffD1, of _ _ _ _ "(\<leadsto>\<^sub>w\<^sup>*)", OF _ _
               ih[of "filter (\<lambda>(E, l). mset E \<noteq> mset (fst ?Dj)) ?P''" P]])
            apply simp_all
           apply (subst (3) p')
         using subs
           apply (simp add: case_prod_beta)
           apply (rule arg_cong[of _ _ "\<lambda>x. image_mset (apfst mset) x"])
         apply (metis (no_types, hide_lams) strictly_subsume_def)
          apply (subst (3) p')
          apply (subst list.size)
          apply (metis (no_types, lifting) less_Suc0 less_add_same_cancel1 linorder_neqE_nat
             not_add_less1 sum_length_filter_compl trans_less_add1)
         using p_nsubs by fast
       ultimately show ?thesis
         by (rule converse_rtranclp_into_rtranclp)
     next
       case nsubs: False
       show ?thesis
         apply (rule arg_cong2[THEN iffD1, of _ _ _ _ "(\<leadsto>\<^sub>w\<^sup>*)", OF _ _
               ih[of ?P'' "P @ [?Dj]"]])
         using nsubs p_nsubs
            apply (simp_all add: arg_cong[OF p', of mset] arg_cong[OF p', of "filter f" for f])
         apply (subst (1 2) p')
         by simp
     qed
   qed simp
 qed
 
 lemma remove_strictly_subsumed_clauses_in_Q:
   assumes c_in: "C \<in> fst ` set N"
   shows "wstate_of_dstate (N, P, Q @ Q', n)
     \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P, Q @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) Q', n)"
 proof (induct Q' arbitrary: Q)
   case ih: (Cons Dj Q')
   have "wstate_of_dstate (N, P, Q @ Dj # Q', n) \<leadsto>\<^sub>w\<^sup>*
     wstate_of_dstate (N, P, Q @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) [Dj] @ Q', n)"
   proof (cases "strictly_subsume [C] (fst Dj)")
     case subs: True
     have "wstate_of_dstate (N, P, Q @ Dj # Q', n) \<leadsto>\<^sub>w wstate_of_dstate (N, P, Q @ Q', n)"
       by (rule arg_cong2[THEN iffD1, of _ _ _ _ "(\<leadsto>\<^sub>w)", OF _ _
             wrp.backward_subsumption_Q[of "mset C" "mset (map (apfst mset) N)" "mset (fst Dj)"
               "mset (map (apfst mset) P)" "mset (map (apfst mset) (Q @ Q'))" "snd Dj" n]])
         (use c_in subs in \<open>auto simp: apfst_fst_snd strictly_subsume_def\<close>)
     then show ?thesis
       by auto
   qed simp
   then show ?case
     using ih[of "Q @ filter (Not \<circ> strictly_subsume [C] \<circ> fst) [Dj]"] by force
 qed simp
 
 lemma reduce_clause_in_P:
   assumes
     c_in: "C \<in> fst ` set N" and
     p_irred: "\<forall>(E, k) \<in> set (P @ P'). k > j \<longrightarrow> is_irreducible [C] E"
   shows "wstate_of_dstate (N, P @ (D @ D', j) # P', Q, n)
     \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ (D @ reduce [C] D D', j) # P', Q, n)"
 proof (induct D' arbitrary: D)
   case ih: (Cons L D')
   show ?case
   proof (cases "is_reducible_lit [C] (D @ D') L")
     case l_red: True
     then obtain L' :: "'a literal" and \<sigma> :: 's where
       l'_in: "L' \<in> set C" and
       not_l: "- L = L' \<cdot>l \<sigma>" and
       subs: "mset (remove1 L' C) \<cdot> \<sigma> \<subseteq># mset (D @ D')"
       unfolding is_reducible_lit_def by force
 
     have ldd'_red: "is_reducible [C] (L # D @ D')"
       apply (rule is_reducible_lit_imp_is_reducible)
       using l_red by auto
 
     have lt_imp_neq: "\<forall>(E, k) \<in> set (P @ P'). j < k \<longrightarrow> mset E \<noteq> mset (L # D @ D')"
       using p_irred ldd'_red is_irreducible_mset_iff by fast
 
     have "wstate_of_dstate (N, P @ (D @ L # D', j) # P', Q, n)
       \<leadsto>\<^sub>w wstate_of_dstate (N, P @ (D @ D', j) # P', Q, n)"
       apply (rule arg_cong2[THEN iffD1, of _ _ _ _ "(\<leadsto>\<^sub>w)", OF _ _
             wrp.backward_reduction_P[of "mset C - {#L'#}" L' "mset (map (apfst mset) N)" L \<sigma>
               "mset (D @ D')" "mset (map (apfst mset) (P @ P'))" j "mset (map (apfst mset) Q)" n]])
       using l'_in not_l subs c_in lt_imp_neq by (simp_all add: case_prod_beta) force+
     then show ?thesis
       using ih[of D] l_red by simp
   next
     case False
     then show ?thesis
       using ih[of "D @ [L]"] by simp
   qed
 qed simp
 
 lemma reduce_clause_in_Q:
   assumes
     c_in: "C \<in> fst ` set N" and
     p_irred: "\<forall>(E, k) \<in> set P. k > j \<longrightarrow> is_irreducible [C] E" and
     d'_red: "reduce [C] D D' \<noteq> D'"
   shows "wstate_of_dstate (N, P, Q @ (D @ D', j) # Q', n)
     \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, (D @ reduce [C] D D', j) # P, Q @ Q', n)"
   using d'_red
 proof (induct D' arbitrary: D)
   case (Cons L D')
   note ih = this(1) and ld'_red = this(2)
   then show ?case
   proof (cases "is_reducible_lit [C] (D @ D') L")
     case l_red: True
     then obtain L' :: "'a literal" and \<sigma> :: 's where
       l'_in: "L' \<in> set C" and
       not_l: "- L = L' \<cdot>l \<sigma>" and
       subs: "mset (remove1 L' C) \<cdot> \<sigma> \<subseteq># mset (D @ D')"
       unfolding is_reducible_lit_def by force
 
     have "wstate_of_dstate (N, P, Q @ (D @ L # D', j) # Q', n)
       \<leadsto>\<^sub>w wstate_of_dstate (N, (D @ D', j) # P, Q @ Q', n)"
       by (rule arg_cong2[THEN iffD1, of _ _ _ _ "(\<leadsto>\<^sub>w)", OF _ _
             wrp.backward_reduction_Q[of "mset C - {#L'#}" L' "mset (map (apfst mset) N)" L \<sigma>
               "mset (D @ D')" "mset (map (apfst mset) P)" "mset (map (apfst mset) (Q @ Q'))" j n]],
           use l'_in not_l subs c_in in auto)
     then show ?thesis
       using l_red p_irred reduce_clause_in_P[OF c_in, of "[]" P j D D' "Q @ Q'" n] by simp
   next
     case l_nred: False
     then have d'_red: "reduce [C] (D @ [L]) D' \<noteq> D'"
       using ld'_red by simp
     show ?thesis
       using ih[OF d'_red] l_nred by simp
   qed
 qed simp
 
 lemma reduce_clauses_in_P:
   assumes
     c_in: "C \<in> fst ` set N" and
     p_irred: "\<forall>(E, k) \<in> set P. is_irreducible [C] E"
   shows "wstate_of_dstate (N, P @ P', Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ reduce_all C P', Q, n)"
   unfolding reduce_all_def
   using p_irred
 proof (induct "length P'" arbitrary: P P')
   case (Suc l)
   note ih = this(1) and suc_l = this(2) and p_irred = this(3)
 
   have p'_nnil: "P' \<noteq> []"
     using suc_l by auto
 
   define j :: nat where
     "j = Max (snd ` set P')"
 
   obtain Dj :: "'a dclause" where
     dj_in: "Dj \<in> set P'" and
     snd_dj: "snd Dj = j"
     using Max_in[of "snd ` set P'", unfolded image_def, simplified]
     by (metis image_def j_def length_Suc_conv list.set_intros(1) suc_l)
 
   have "\<forall>k \<in> snd ` set P'. k \<le> j"
     unfolding j_def using p'_nnil by simp
   then have j_max: "\<forall>(E, k) \<in> set P'. j \<ge> k"
     unfolding image_def by fastforce
 
   obtain P1' P2' :: "'a dclause list"  where
     p': "P' = P1' @ Dj # P2'"
     using split_list[OF dj_in] by blast
 
   have "wstate_of_dstate (N, P @ P1' @ Dj # P2', Q, n)
      \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ P1' @ apfst (reduce [C] []) Dj # P2', Q, n)"
     unfolding append_assoc[symmetric]
     apply (subst (1 2) surjective_pairing[of Dj, unfolded snd_dj])
     apply (simp only: apfst_conv)
     apply (rule reduce_clause_in_P[of _ _ _ _ _ "[]", unfolded append_Nil, OF c_in])
     using p_irred j_max[unfolded p'] by (force simp: case_prod_beta)
   moreover have "wstate_of_dstate (N, P @ P1' @ apfst (reduce [C] []) Dj # P2', Q, n)
      \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, P @ map (apfst (reduce [C] [])) (P1' @ Dj # P2'), Q, n)"
     apply (rule arg_cong2[THEN iffD1, of _ _ _ _ "(\<leadsto>\<^sub>w\<^sup>*)", OF _ _
           ih[of "P1' @ P2'" "apfst (reduce [C] []) Dj # P"]])
     using suc_l reduce_idem p_irred unfolding p' by (auto simp: case_prod_beta)
   ultimately show ?case
     unfolding p' by simp
 qed simp
 
 lemma reduce_clauses_in_Q:
   assumes
     c_in: "C \<in> fst ` set N" and
     p_irred: "\<forall>(E, k) \<in> set P. is_irreducible [C] E"
   shows "wstate_of_dstate (N, P, Q @ Q', n)
     \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, fst (reduce_all2 C Q') @ P, Q @ snd (reduce_all2 C Q'), n)"
   using p_irred
 proof (induct Q' arbitrary: P Q)
   case (Cons Dj Q')
   note ih = this(1) and p_irred = this(2)
   show ?case
   proof (cases "is_irreducible [C] (fst Dj)")
     case True
     then show ?thesis
       using ih[of _ "Q @ [Dj]"] p_irred by (simp add: case_prod_beta)
   next
     case d_red: False
     have "wstate_of_dstate (N, P, Q @ Dj # Q', n)
       \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (N, (reduce [C] [] (fst Dj), snd Dj) # P, Q @ Q', n)"
       using p_irred reduce_clause_in_Q[of _ _ P "snd Dj" "[]" _ Q Q' n, OF c_in _ d_red]
       by (cases Dj) force
     then show ?thesis
       using ih[of "(reduce [C] [] (fst Dj), snd Dj) # P" Q] d_red p_irred reduce_idem
       by (force simp: case_prod_beta)
   qed
 qed simp
 
 lemma eligible_iff:
   "eligible S \<sigma> As DA \<longleftrightarrow> As = [] \<or> length As = 1 \<and> maximal_wrt (hd As \<cdot>a \<sigma>) (DA \<cdot> \<sigma>)"
   unfolding eligible.simps S_empty by (fastforce dest: hd_conv_nth)
 
 lemma ord_resolve_one_side_prem:
   "ord_resolve S CAs DA AAs As \<sigma> E \<Longrightarrow> length CAs = 1 \<and> length AAs = 1 \<and> length As = 1"
   by (force elim!: ord_resolve.cases simp: eligible_iff)
 
 lemma ord_resolve_rename_one_side_prem:
   "ord_resolve_rename S CAs DA AAs As \<sigma> E \<Longrightarrow> length CAs = 1 \<and> length AAs = 1 \<and> length As = 1"
   by (force elim!: ord_resolve_rename.cases dest: ord_resolve_one_side_prem)
 
 abbreviation Bin_ord_resolve :: "'a clause \<Rightarrow> 'a clause \<Rightarrow> 'a clause set" where
   "Bin_ord_resolve C D \<equiv> {E. \<exists>AA A \<sigma>. ord_resolve S [C] D [AA] [A] \<sigma> E}"
 
 abbreviation Bin_ord_resolve_rename :: "'a clause \<Rightarrow> 'a clause \<Rightarrow> 'a clause set" where
   "Bin_ord_resolve_rename C D \<equiv> {E. \<exists>AA A \<sigma>. ord_resolve_rename S [C] D [AA] [A] \<sigma> E}"
 
 lemma resolve_on_eq_UNION_Bin_ord_resolve:
   "mset ` set (resolve_on A D CA) =
    {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E}"
 proof
   {
     fix E :: "'a literal list"
     assume "E \<in> set (resolve_on A D CA)"
     then have "E \<in> resolvent D A CA ` {Ls. subseq Ls CA \<and> resolvable A D CA Ls}"
       unfolding resolve_on_def by simp
     then obtain Ls where Ls_p: "resolvent D A CA Ls = E" "subseq Ls CA \<and> resolvable A D CA Ls"
       by auto
     define \<sigma> where "\<sigma> = the (mgu {insert A (atms_of (mset Ls))})"
     then have \<sigma>_p:
       "mgu {insert A (atms_of (mset Ls))} = Some \<sigma>"
       "Ls \<noteq> []"
       "eligible S \<sigma> [A] (add_mset (Neg A) (mset D))"
       "strictly_maximal_wrt (A \<cdot>a \<sigma>) ((mset CA - mset Ls) \<cdot> \<sigma>)"
       "\<forall>L \<in> set Ls. is_pos L"
       using Ls_p unfolding resolvable_def unfolding Let_def eligible.simps using S_empty by auto
     from \<sigma>_p have \<sigma>_p2: "the (mgu {insert A (atms_of (mset Ls))}) = \<sigma>"
       by auto
     have Ls_sub_CA: "mset Ls \<subseteq># mset CA"
       using subseq_mset_subseteq_mset Ls_p by auto
     then have "mset (resolvent D A CA Ls) = sum_list [mset CA - mset Ls] \<cdot> \<sigma> + mset D \<cdot> \<sigma>"
       unfolding resolvent_def \<sigma>_p2 subst_cls_def using remove_all_mset_minus[of Ls CA] by auto
     moreover
     have "length [mset CA - mset Ls] = Suc 0"
       by auto
     moreover
     have "\<forall>L \<in> set Ls. is_pos L"
       using \<sigma>_p(5) list_all_iff[of is_pos] by auto
     then have "{#Pos (atm_of x). x \<in># mset Ls#} = mset Ls"
       by (induction Ls) auto
     then have "mset CA = [mset CA - mset Ls] ! 0 + {#Pos (atm_of x). x \<in># mset Ls#}"
       using Ls_sub_CA by auto
     moreover
     have "Ls \<noteq> []"
       using \<sigma>_p by -
     moreover
     have "Some \<sigma> = mgu {insert A (atm_of ` set Ls)}"
       using \<sigma>_p unfolding atms_of_def by auto
     moreover
     have "eligible S \<sigma> [A] (add_mset (Neg A) (mset D))"
       using \<sigma>_p by -
     moreover
     have "strictly_maximal_wrt (A \<cdot>a \<sigma>) ([mset CA - mset Ls] ! 0 \<cdot> \<sigma>)"
       using \<sigma>_p(4) by auto
     moreover have "S (mset CA) = {#}"
       by (simp add: S_empty)
     ultimately have "\<exists>Cs. mset (resolvent D A CA Ls) = sum_list Cs \<cdot> \<sigma> + mset D \<cdot> \<sigma>
         \<and> length Cs = Suc 0 \<and> mset CA = Cs ! 0 + {#Pos (atm_of x). x \<in># mset Ls#}
         \<and> Ls \<noteq> [] \<and> Some \<sigma> = mgu {insert A (atm_of ` set Ls)}
         \<and> eligible S \<sigma> [A] (add_mset (Neg A) (mset D)) \<and> strictly_maximal_wrt (A \<cdot>a \<sigma>) (Cs ! 0 \<cdot> \<sigma>)
         \<and> S (mset CA) = {#}"
       by blast
     then have "ord_resolve S [mset CA] (add_mset (Neg A) (mset D)) [image_mset atm_of (mset Ls)] [A]
       \<sigma> (mset (resolvent D A CA Ls))"
       unfolding ord_resolve.simps by auto
     then have "\<exists>AA \<sigma>. ord_resolve S [mset CA] (add_mset (Neg A) (mset D)) [AA] [A] \<sigma> (mset E)"
       using Ls_p by auto
   }
   then show "mset ` set (resolve_on A D CA)
     \<subseteq> {E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E}"
     by auto
 next
   {
     fix E AA \<sigma>
     assume "ord_resolve S [mset CA] (add_mset (Neg A) (mset D)) [AA] [A] \<sigma> E"
     then obtain Cs where res': "E = sum_list Cs \<cdot> \<sigma> + mset D \<cdot> \<sigma>"
       "length Cs = Suc 0"
       "mset CA = Cs ! 0 + poss AA"
       "AA \<noteq> {#}"
       "Some \<sigma> = mgu {insert A (set_mset AA)}"
       "eligible S \<sigma> [A] (add_mset (Neg A) (mset D))"
       "strictly_maximal_wrt (A \<cdot>a \<sigma>) (Cs ! 0 \<cdot> \<sigma>)"
       "S (Cs ! 0 + poss AA) = {#}"
       unfolding ord_resolve.simps by auto
     moreover define C where "C = Cs ! 0"
     ultimately have res:
       "E = sum_list Cs \<cdot> \<sigma> + mset D \<cdot> \<sigma>"
       "mset CA = C + poss AA"
       "AA \<noteq> {#}"
       "Some \<sigma> = mgu {insert A (set_mset AA)}"
       "eligible S \<sigma> [A] (add_mset (Neg A) (mset D))"
       "strictly_maximal_wrt (A \<cdot>a \<sigma>) (C \<cdot> \<sigma>)"
       "S (C + poss AA) = {#}"
       unfolding ord_resolve.simps by auto
     from this(1) have
       "E = C \<cdot> \<sigma> + mset D \<cdot> \<sigma>"
       unfolding C_def using res'(2) by (cases Cs) auto
     note res' = this res(2-7)
     have "\<exists>Al. mset Al = AA \<and> subseq (map Pos Al) CA"
       using res(2)
     proof (induction CA arbitrary: AA C)
       case Nil
       then show ?case by auto
     next
       case (Cons L CA)
       then show ?case
       proof (cases "L \<in># poss AA ")
         case True
         then have pos_L: "is_pos L"
           by auto
         have rem: "\<And>A'. Pos A' \<in># poss AA \<Longrightarrow>
           remove1_mset (Pos A') (C + poss AA) = C + poss (remove1_mset A' AA)"
           by (induct AA) auto
         have "mset CA = C + (poss (AA - {#atm_of L#}))"
           using True Cons(2)
           by (metis add_mset_remove_trivial rem literal.collapse(1) mset.simps(2) pos_L)
         then have "\<exists>Al. mset Al = remove1_mset (atm_of L) AA \<and> subseq (map Pos Al) CA"
           using Cons(1)[of _ "((AA - {#atm_of L#}))"] by metis
         then obtain Al where
           "mset Al = remove1_mset (atm_of L) AA \<and> subseq (map Pos Al) CA"
           by auto
         then have
           "mset (atm_of L # Al) = AA" and
           "subseq (map Pos (atm_of L # Al)) (L # CA)"
           using True by (auto simp add: pos_L)
         then show ?thesis
           by blast
       next
         case False
         then have "mset CA = remove1_mset L C + poss AA"
           using Cons(2)
           by (metis Un_iff add_mset_remove_trivial mset.simps(2) set_mset_union single_subset_iff
               subset_mset.add_diff_assoc2 union_single_eq_member)
         then have "\<exists>Al. mset Al = AA \<and> subseq (map Pos Al) CA"
           using Cons(1)[of "C - {#L#}" AA] Cons(2) by auto
         then show ?thesis
           by auto
       qed
     qed
     then obtain Al where Al_p: "mset Al = AA" "subseq (map Pos Al) CA"
       by auto
 
     define Ls :: "'a lclause" where "Ls = map Pos Al"
     have diff: "mset CA - mset Ls = C"
       unfolding Ls_def using res(2) Al_p(1) by auto
     have ls_subq_ca: "subseq Ls CA"
       unfolding Ls_def using Al_p by -
     moreover
     {
       have "\<exists>y. mgu {insert A (atms_of (mset Ls))} = Some y"
         unfolding Ls_def using res(4) Al_p by (metis atms_of_poss mset_map)
       moreover have "Ls \<noteq> []"
         using Al_p(1) Ls_def res'(3) by auto
       moreover have \<sigma>_p: "the (mgu {insert A (set Al)}) = \<sigma>"
         using res'(4) Al_p(1) by (metis option.sel  set_mset_mset)
       then have "eligible S (the (mgu {insert A (atms_of (mset Ls))})) [A]
         (add_mset (Neg A) (mset D))"
         unfolding Ls_def using res  by auto
       moreover have "strictly_maximal_wrt (A \<cdot>a the (mgu {insert A (atms_of (mset Ls))}))
         ((mset CA - mset Ls) \<cdot> the (mgu {insert A (atms_of (mset Ls))}))"
         unfolding Ls_def using res \<sigma>_p Al_p by auto
       moreover have "\<forall>L \<in> set Ls. is_pos L"
         by (simp add: Ls_def)
       ultimately have "resolvable A D CA Ls"
         unfolding resolvable_def unfolding eligible.simps using S_empty by simp
     }
     moreover have ls_sub_ca: "mset Ls \<subseteq># mset CA"
       using ls_subq_ca subseq_mset_subseteq_mset[of Ls CA] by simp
     have "{#x \<cdot>l \<sigma>. x \<in># mset CA - mset Ls#} + {#M \<cdot>l \<sigma>. M \<in># mset D#} = C \<cdot> \<sigma> + mset D \<cdot> \<sigma>"
       using diff unfolding subst_cls_def by simp
     then have "{#x \<cdot>l \<sigma>. x \<in># mset CA - mset Ls#} + {#M \<cdot>l \<sigma>. M \<in># mset D#} = E"
       using res'(1) by auto
     then have "{#M \<cdot>l \<sigma>. M \<in># mset (remove_all CA Ls)#} + {#M \<cdot>l \<sigma> . M \<in># mset D#} = E"
       using remove_all_mset_minus[of Ls CA] ls_sub_ca by auto
     then have "mset (resolvent D A CA Ls) = E"
       unfolding resolvable_def Let_def resolvent_def using Al_p(1) Ls_def atms_of_poss res'(4)
       by (metis image_mset_union mset_append mset_map option.sel)
     ultimately have "E \<in> mset ` set (resolve_on A D CA)"
       unfolding resolve_on_def by auto
   }
   then show "{E. \<exists>AA \<sigma>. ord_resolve S [mset CA] ({#Neg A#} + mset D) [AA] [A] \<sigma> E}
     \<subseteq> mset ` set (resolve_on A D CA)"
     by auto
 qed
 
 lemma set_resolve_eq_UNION_set_resolve_on:
   "set (resolve C D) =
    (\<Union>L \<in> set D.
       (case L of
          Pos _ \<Rightarrow> {}
        | Neg A \<Rightarrow> if maximal_wrt A (mset D) then set (resolve_on A (remove1 L D) C) else {}))"
   unfolding resolve_def by (fastforce split: literal.splits if_splits)
 
 lemma resolve_eq_Bin_ord_resolve: "mset ` set (resolve C D) = Bin_ord_resolve (mset C) (mset D)"
   unfolding set_resolve_eq_UNION_set_resolve_on
   apply (unfold image_UN literal.case_distrib if_distrib)
   apply (subst resolve_on_eq_UNION_Bin_ord_resolve)
   apply (rule order_antisym)
    apply (force split: literal.splits if_splits)
   apply (clarsimp split: literal.splits if_splits)
   apply (rule_tac x = "Neg A" in bexI)
    apply (rule conjI)
     apply blast
    apply clarify
    apply (rule conjI)
     apply clarify
     apply (rule_tac x = AA in exI)
     apply (rule_tac x = \<sigma> in exI)
     apply (frule ord_resolve.simps[THEN iffD1])
     apply force
    apply (drule ord_resolve.simps[THEN iffD1])
    apply (clarsimp simp: eligible_iff simp del: subst_cls_add_mset subst_cls_union)
    apply (drule maximal_wrt_subst)
    apply sat
   apply (drule ord_resolve.simps[THEN iffD1])
   using set_mset_mset by fastforce
 
 lemma poss_in_map_clauseD:
   "poss AA \<subseteq># map_clause f C \<Longrightarrow> \<exists>AA0. poss AA0 \<subseteq># C \<and> AA = {#f A. A \<in># AA0#}"
 proof (induct AA arbitrary: C)
   case (add A AA)
   note ih = this(1) and aaa_sub = this(2)
 
   have "Pos A \<in># map_clause f C"
     using aaa_sub by auto
   then obtain A0 where
     pa0_in: "Pos A0 \<in># C" and
     a: "A = f A0"
     by clarify (metis literal.distinct(1) literal.exhaust literal.inject(1) literal.simps(9,10))
 
   have "poss AA \<subseteq># map_clause f (C - {#Pos A0#})"
     using pa0_in aaa_sub[unfolded a] by (simp add: image_mset_remove1_mset_if insert_subset_eq_iff)
   then obtain AA0 where
     paa0_sub: "poss AA0 \<subseteq># C - {#Pos A0#}" and
     aa: "AA = image_mset f AA0"
     using ih by meson
 
   have "poss (add_mset A0 AA0) \<subseteq># C"
     using pa0_in paa0_sub by (simp add: insert_subset_eq_iff)
   moreover have "add_mset A AA = image_mset f (add_mset A0 AA0)"
     unfolding a aa by simp
   ultimately show ?case
     by blast
 qed simp
 
 lemma poss_subset_filterD:
   "poss AA \<subseteq># {#L \<cdot>l \<rho>. L \<in># mset C#} \<Longrightarrow> \<exists>AA0. poss AA0 \<subseteq># mset C \<and> AA = AA0 \<cdot>am \<rho>"
   unfolding subst_atm_mset_def subst_lit_def by (rule poss_in_map_clauseD)
 
 lemma neg_in_map_literalD: "Neg A \<in> map_literal f ` D \<Longrightarrow> \<exists>A0. Neg A0 \<in> D \<and> A = f A0"
   unfolding image_def by (clarify, case_tac x, auto)
 
 lemma neg_in_filterD: "Neg A \<in># {#L \<cdot>l \<rho>'. L \<in># mset D#} \<Longrightarrow> \<exists>A0. Neg A0 \<in># mset D \<and> A = A0 \<cdot>a \<rho>'"
   unfolding subst_lit_def image_def by (rule neg_in_map_literalD) simp
 
 lemma resolve_rename_eq_Bin_ord_resolve_rename:
   "mset ` set (resolve_rename C D) = Bin_ord_resolve_rename (mset C) (mset D)"
 proof (intro order_antisym subsetI)
   let ?\<rho>s = "renamings_apart [mset D, mset C]"
   define \<rho>' :: 's where
     "\<rho>' = hd ?\<rho>s"
   define \<rho> :: 's where
     "\<rho> = last ?\<rho>s"
 
   have tl_\<rho>s: "tl ?\<rho>s = [\<rho>]"
     unfolding \<rho>_def
     using renamings_apart_length Nitpick.size_list_simp(2) Suc_length_conv last.simps
     by (smt length_greater_0_conv list.sel(3))
 
   {
     fix E
     assume e_in: "E \<in> mset ` set (resolve_rename C D)"
 
     from e_in obtain AA :: "'a multiset" and A :: 'a and \<sigma> :: 's where
       aa_sub: "poss AA \<subseteq># mset C \<cdot> \<rho>" and
       a_in: "Neg A \<in># mset D \<cdot> \<rho>'" and
       res_e: "ord_resolve S [mset C \<cdot> \<rho>] {#L \<cdot>l \<rho>'. L \<in># mset D#} [AA] [A] \<sigma> E"
       unfolding \<rho>'_def \<rho>_def
       apply atomize_elim
       using e_in unfolding resolve_rename_def Let_def resolve_eq_Bin_ord_resolve
       apply clarsimp
       apply (frule ord_resolve_one_side_prem)
       apply (frule ord_resolve.simps[THEN iffD1])
       apply (rule_tac x = AA in exI)
       apply (clarsimp simp: subst_cls_def)
       apply (rule_tac x = A in exI)
       by (metis (full_types) Melem_subst_cls set_mset_mset subst_cls_def union_single_eq_member)
 
     obtain AA0 :: "'a multiset" where
       aa0_sub: "poss AA0 \<subseteq># mset C" and
       aa: "AA = AA0 \<cdot>am \<rho>"
       using aa_sub
       apply atomize_elim
       apply (rule ord_resolve.cases[OF res_e])
       by (rule poss_subset_filterD[OF aa_sub[unfolded subst_cls_def]])
 
     obtain A0 :: 'a where
       a0_in: "Neg A0 \<in> set D" and
       a: "A = A0 \<cdot>a \<rho>'"
       apply atomize_elim
       apply (rule ord_resolve.cases[OF res_e])
       using neg_in_filterD[OF a_in[unfolded subst_cls_def]] by simp
 
     show "E \<in> Bin_ord_resolve_rename (mset C) (mset D)"
       unfolding ord_resolve_rename.simps
       using res_e
       apply clarsimp
       apply (rule_tac x = AA0 in exI)
       apply (intro conjI)
        apply (rule aa0_sub)
       apply (rule_tac x = A0 in exI)
       apply (intro conjI)
        apply (rule a0_in)
       apply (rule_tac x = \<sigma> in exI)
       unfolding aa a \<rho>'_def[symmetric] \<rho>_def[symmetric] tl_\<rho>s by (simp add: subst_cls_def)
   }
   {
     fix E
     assume e_in: "E \<in> Bin_ord_resolve_rename (mset C) (mset D)"
     show "E \<in> mset ` set (resolve_rename C D)"
       using e_in
       unfolding resolve_rename_def Let_def resolve_eq_Bin_ord_resolve ord_resolve_rename.simps
       apply clarsimp
       apply (rule_tac x = "AA \<cdot>am \<rho>" in exI)
       apply (rule_tac x = "A \<cdot>a \<rho>'" in exI)
       apply (rule_tac x = \<sigma> in exI)
       unfolding tl_\<rho>s \<rho>'_def \<rho>_def by (simp add: subst_cls_def subst_cls_lists_def)
   }
 qed
 
 lemma bin_ord_FO_\<Gamma>_def:
   "ord_FO_\<Gamma> S = {Infer {#CA#} DA E | CA DA AA A \<sigma> E. ord_resolve_rename S [CA] DA [AA] [A] \<sigma> E}"
   unfolding ord_FO_\<Gamma>_def
   apply (rule order.antisym)
    apply clarify
    apply (frule ord_resolve_rename_one_side_prem)
    apply simp
    apply (metis Suc_length_conv length_0_conv)
   by blast
 
 lemma ord_FO_\<Gamma>_side_prem: "\<gamma> \<in> ord_FO_\<Gamma> S \<Longrightarrow> side_prems_of \<gamma> = {#THE D. D \<in># side_prems_of \<gamma>#}"
   unfolding bin_ord_FO_\<Gamma>_def by clarsimp
 
 lemma ord_FO_\<Gamma>_infer_from_Collect_eq:
   "{\<gamma> \<in> ord_FO_\<Gamma> S. infer_from (DD \<union> {C}) \<gamma> \<and> C \<in># prems_of \<gamma>} =
    {\<gamma> \<in> ord_FO_\<Gamma> S. \<exists>D \<in> DD \<union> {C}. prems_of \<gamma> = {#C, D#}}"
   unfolding infer_from_def
   apply (rule set_eq_subset[THEN iffD2])
   apply (rule conjI)
    apply clarify
    apply (subst (asm) (1 2) ord_FO_\<Gamma>_side_prem, assumption, assumption)
    apply (subst (1) ord_FO_\<Gamma>_side_prem, assumption)
    apply force
   apply clarify
   apply (subst (asm) (1) ord_FO_\<Gamma>_side_prem, assumption)
   apply (subst (1 2) ord_FO_\<Gamma>_side_prem, assumption)
   by force
 
 lemma inferences_between_eq_UNION: "inference_system.inferences_between (ord_FO_\<Gamma> S) Q C =
   inference_system.inferences_between (ord_FO_\<Gamma> S) {C} C
   \<union> (\<Union>D \<in> Q. inference_system.inferences_between (ord_FO_\<Gamma> S) {D} C)"
   unfolding ord_FO_\<Gamma>_infer_from_Collect_eq inference_system.inferences_between_def by auto
 
 lemma concls_of_inferences_between_singleton_eq_Bin_ord_resolve_rename:
   "concls_of (inference_system.inferences_between (ord_FO_\<Gamma> S) {D} C) =
    Bin_ord_resolve_rename C C \<union> Bin_ord_resolve_rename C D \<union> Bin_ord_resolve_rename D C"
 proof (intro order_antisym subsetI)
   fix E
   assume e_in: "E \<in> concls_of (inference_system.inferences_between (ord_FO_\<Gamma> S) {D} C)"
   then show "E \<in> Bin_ord_resolve_rename C C \<union> Bin_ord_resolve_rename C D
     \<union> Bin_ord_resolve_rename D C"
     unfolding inference_system.inferences_between_def ord_FO_\<Gamma>_infer_from_Collect_eq
       bin_ord_FO_\<Gamma>_def infer_from_def by (fastforce simp: add_mset_eq_add_mset)
 qed (force simp: inference_system.inferences_between_def infer_from_def ord_FO_\<Gamma>_def)
 
 lemma concls_of_inferences_between_eq_Bin_ord_resolve_rename:
   "concls_of (inference_system.inferences_between (ord_FO_\<Gamma> S) Q C) =
    Bin_ord_resolve_rename C C \<union> (\<Union>D \<in> Q. Bin_ord_resolve_rename C D \<union> Bin_ord_resolve_rename D C)"
   by (subst inferences_between_eq_UNION)
     (auto simp: image_Un image_UN concls_of_inferences_between_singleton_eq_Bin_ord_resolve_rename)
 
 lemma resolve_rename_either_way_eq_congls_of_inferences_between:
   "mset ` set (resolve_rename C C) \<union> (\<Union>D \<in> Q. mset ` set (resolve_rename_either_way C D)) =
    concls_of (inference_system.inferences_between (ord_FO_\<Gamma> S) (mset ` Q) (mset C))"
   by (simp add: resolve_rename_either_way_def image_Un resolve_rename_eq_Bin_ord_resolve_rename
       concls_of_inferences_between_eq_Bin_ord_resolve_rename UN_Un_distrib)
 
 lemma compute_inferences:
   assumes
     ci_in: "(C, i) \<in> set P" and
     ci_min: "\<forall>(D, j) \<in># mset (map (apfst mset) P). weight (mset C, i) \<le> weight (D, j)"
   shows
     "wstate_of_dstate ([], P, Q, n) \<leadsto>\<^sub>w
      wstate_of_dstate (map (\<lambda>D. (D, n)) (remdups_gen mset (resolve_rename C C @
          concat (map (resolve_rename_either_way C \<circ> fst) Q))),
        filter (\<lambda>(D, j). mset D \<noteq> mset C) P, (C, i) # Q, Suc n)"
     (is "_ \<leadsto>\<^sub>w wstate_of_dstate (?N, _)")
 proof -
   have ms_ci_in: "(mset C, i) \<in># image_mset (apfst mset) (mset P)"
     using ci_in by force
 
   show ?thesis
     apply (rule arg_cong2[THEN iffD1, of _ _ _ _ "(\<leadsto>\<^sub>w)", OF _ _
           wrp.inference_computation[of "mset (map (apfst mset) P) - {#(mset C, i)#}" "mset C" i
             "mset (map (apfst mset) ?N)" n "mset (map (apfst mset) Q)"]])
        apply (simp add: add_mset_remove_trivial_eq[THEN iffD2, OF ms_ci_in, symmetric])
     using ms_ci_in
       apply (simp add: ci_in image_mset_remove1_mset_if)
       apply (smt apfst_conv case_prodE case_prodI2 case_prod_conv filter_mset_cong
         image_mset_filter_swap mset_filter)
      apply (metis ci_min in_diffD)
     apply (simp only: list.map_comp apfst_comp_rpair_const)
     apply (simp only: list.map_comp[symmetric])
     apply (subst mset_map)
     apply (unfold mset_map_remdups_gen mset_remdups_gen_ident)
     apply (subst image_mset_mset_set)
      apply (simp add: inj_on_def)
     apply (subst mset_set_eq_iff)
       apply simp
      apply (simp add: finite_ord_FO_resolution_inferences_between)
     apply (rule arg_cong[of _ _ "\<lambda>N. (\<lambda>D. (D, n)) ` N"])
     apply (simp only: map_concat list.map_comp image_comp)
     using resolve_rename_either_way_eq_congls_of_inferences_between[of C "fst ` set Q", symmetric]
     by (simp add: image_comp comp_def image_UN)
 qed
 
 lemma nonfinal_deterministic_RP_step:
   assumes
     nonfinal: "\<not> is_final_dstate St" and
     step: "St' = deterministic_RP_step St"
   shows "wstate_of_dstate St \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate St'"
 proof -
   obtain N P Q :: "'a dclause list" and n :: nat where
     st: "St = (N, P, Q, n)"
     by (cases St) blast
   note step = step[unfolded st deterministic_RP_step.simps, simplified]
 
   show ?thesis
   proof (cases "\<exists>Ci \<in> set P \<union> set Q. fst Ci = []")
     case nil_in: True
     note step = step[simplified nil_in, simplified]
 
     have nil_in': "[] \<in> fst ` set (P @ Q)"
       using nil_in by (force simp: image_def)
 
     have star: "[] \<in> fst ` set (P @ Q) \<Longrightarrow>
       wstate_of_dstate (N, P, Q, n)
       \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P))"
     proof (induct "length (remdups_clss P)" arbitrary: N P Q n)
       case 0
       note len_p = this(1) and nil_in' = this(2)
 
       have p_nil: "P = []"
         using len_p remdups_clss_Nil_iff by simp
       have "wstate_of_dstate (N, [], Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], Q, n)"
         by (rule empty_N_if_Nil_in_P_or_Q[OF nil_in'[unfolded p_nil]])
       then show ?case
         unfolding p_nil by simp
     next
       case (Suc k)
       note ih = this(1) and suc_k = this(2) and nil_in' = this(3)
 
       have "P \<noteq> []"
         using suc_k remdups_clss_Nil_iff by force
       hence p_cons: "P = hd P # tl P"
         by simp
 
       obtain C :: "'a lclause" and i :: nat where
         ci: "(C, i) = select_min_weight_clause (hd P) (tl P)"
         by (metis prod.exhaust)
 
       have ci_in: "(C, i) \<in> set P"
         unfolding ci using p_cons select_min_weight_clause_in[of "hd P" "tl P"] by simp
       have ci_min: "\<forall>(D, j) \<in># mset (map (apfst mset) P). weight (mset C, i) \<le> weight (D, j)"
         by (subst p_cons) (simp add: select_min_weight_clause_min_weight[OF ci, simplified])
 
       let ?P' = "filter (\<lambda>(D, j). mset D \<noteq> mset C) P"
 
       have ms_p'_ci_q_eq: "mset (remdups_clss ?P' @ (C, i) # Q) = mset (remdups_clss P @ Q)"
         apply (subst (2) p_cons)
         apply (subst remdups_clss.simps(2))
         by (auto simp: Let_def case_prod_beta p_cons[symmetric] ci[symmetric])
       then have len_p: "length (remdups_clss P) = length (remdups_clss ?P') + 1"
         by (smt Suc_eq_plus1_left add.assoc add_right_cancel length_Cons length_append
             mset_eq_length)
 
       have "wstate_of_dstate (N, P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], P, Q, n)"
         by (rule empty_N_if_Nil_in_P_or_Q[OF nil_in'])
       also obtain N' :: "'a dclause list" where
         "\<dots> \<leadsto>\<^sub>w wstate_of_dstate (N', ?P', (C, i) # Q, Suc n)"
         by (atomize_elim, rule exI, rule compute_inferences[OF ci_in], use ci_min in fastforce)
       also have "\<dots> \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [], remdups_clss P @ Q, n + length (remdups_clss P))"
         apply (rule arg_cong2[THEN iffD1, of _ _ _ _ "(\<leadsto>\<^sub>w\<^sup>*)", OF _ _
             ih[of ?P' "(C, i) # Q" N' "Suc n"], OF refl])
         using ms_p'_ci_q_eq suc_k nil_in' ci_in
           apply (simp_all add: len_p)
          apply (metis (no_types) apfst_conv image_mset_add_mset)
         by force
       finally show ?case
         .
     qed
     show ?thesis
       unfolding st step using star[OF nil_in'] nonfinal[unfolded st is_final_dstate.simps]
       by cases simp_all
   next
     case nil_ni: False
     note step = step[simplified nil_ni, simplified]
     show ?thesis
     proof (cases N)
       case n_nil: Nil
       note step = step[unfolded n_nil, simplified]
       show ?thesis
       proof (cases P)
         case Nil
         then have False
           using n_nil nonfinal[unfolded st] by (simp add: is_final_dstate.simps)
         then show ?thesis
           using step by simp
       next
         case p_cons: (Cons P0 P')
         note step = step[unfolded p_cons list.case, folded p_cons]
 
         obtain C :: "'a lclause" and i :: nat where
           ci: "(C, i) = select_min_weight_clause P0 P'"
           by (metis prod.exhaust)
         note step = step[unfolded select, simplified]
 
         have ci_in: "(C, i) \<in> set P"
           by (rule select_min_weight_clause_in[of P0 P', folded ci p_cons])
 
         show ?thesis
           unfolding st n_nil step p_cons[symmetric] ci[symmetric] prod.case
           by (rule tranclp.r_into_trancl, rule compute_inferences[OF ci_in])
             (simp add: select_min_weight_clause_min_weight[OF ci, simplified] p_cons)
       qed
     next
       case n_cons: (Cons Ci N')
       note step = step[unfolded n_cons, simplified]
 
       obtain C :: "'a lclause" and i :: nat where
         ci: "Ci = (C, i)"
         by (cases Ci) simp
       note step = step[unfolded ci, simplified]
 
       define C' :: "'a lclause" where
         "C' = reduce (map fst P @ map fst Q) [] C"
       note step = step[unfolded ci C'_def[symmetric], simplified]
 
       have "wstate_of_dstate ((E @ C, i) # N', P, Q, n)
            \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ((E @ reduce (map fst P @ map fst Q) E C, i) # N', P, Q, n)" for E
         unfolding C'_def
       proof (induct C arbitrary: E)
         case (Cons L C)
         note ih = this(1)
         show ?case
         proof (cases "is_reducible_lit (map fst P @ map fst Q) (E @ C) L")
           case l_red: True
           then have red_lc:
             "reduce (map fst P @ map fst Q) E (L # C) = reduce (map fst P @ map fst Q) E C"
             by simp
           obtain D D' :: "'a literal list" and L' :: "'a literal" and \<sigma> :: 's where
             "D \<in> set (map fst P @ map fst Q)" and
             "D' = remove1 L' D" and
             "L' \<in> set D" and
             "- L = L' \<cdot>l \<sigma>" and
             "mset D' \<cdot> \<sigma> \<subseteq># mset (E @ C)"
             using l_red unfolding is_reducible_lit_def comp_def by blast
           then have \<sigma>:
             "mset D' + {#L'#} \<in> set (map (mset \<circ> fst) (P @ Q))"
             "- L = L' \<cdot>l \<sigma> \<and> mset D' \<cdot> \<sigma> \<subseteq># mset (E @ C)"
             unfolding is_reducible_lit_def by (auto simp: comp_def)
           have "wstate_of_dstate ((E @ L # C, i) # N', P, Q, n)
               \<leadsto>\<^sub>w wstate_of_dstate ((E @ C, i) # N', P, Q, n)"
             by (rule arg_cong2[THEN iffD1, of _ _ _ _ "(\<leadsto>\<^sub>w)", OF _ _
                   wrp.forward_reduction[of "mset D'" L' "mset (map (apfst mset) P)"
                     "mset (map (apfst mset) Q)" L \<sigma> "mset (E @ C)" "mset (map (apfst mset) N')"
                     i n]])
               (use \<sigma> in \<open>auto simp: comp_def\<close>)
           then show ?thesis
             unfolding red_lc using ih[of E] by (rule converse_rtranclp_into_rtranclp)
         next
           case False
           then show ?thesis
             using ih[of "L # E"] by simp
         qed
       qed simp
       then have red_C:
         "wstate_of_dstate ((C, i) # N', P, Q, n) \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ((C', i) # N', P, Q, n)"
         unfolding C'_def by (metis self_append_conv2)
 
       have proc_C: "wstate_of_dstate ((C', i) # N', P', Q', n')
           \<leadsto>\<^sub>w wstate_of_dstate (N', (C', i) # P', Q', n')" for P' Q' n'
         by (rule arg_cong2[THEN iffD1, of _ _ _ _ "(\<leadsto>\<^sub>w)", OF _ _
               wrp.clause_processing[of "mset (map (apfst mset) N')" "mset C'" i
                 "mset (map (apfst mset) P')" "mset (map (apfst mset) Q')" n']],
             simp+)
 
       show ?thesis
       proof (cases "C' = []")
         case True
         note c'_nil = this
         note step = step[simplified c'_nil, simplified]
 
         have
           filter_p: "filter (Not \<circ> strictly_subsume [[]] \<circ> fst) P = []" and
           filter_q: "filter (Not \<circ> strictly_subsume [[]] \<circ> fst) Q = []"
           using nil_ni unfolding strictly_subsume_def filter_empty_conv find_None_iff by force+
 
         note red_C[unfolded c'_nil]
         also have "wstate_of_dstate (([], i) # N', P, Q, n)
             \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (([], i) # N', [], Q, n)"
           by (rule arg_cong2[THEN iffD1, of _ _ _ _ "(\<leadsto>\<^sub>w\<^sup>*)", OF _ _
                 remove_strictly_subsumed_clauses_in_P[of "[]" _ "[]", unfolded append_Nil],
                 OF refl])
             (auto simp: filter_p)
         also have "\<dots> \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (([], i) # N', [], [], n)"
           by (rule arg_cong2[THEN iffD1, of _ _ _ _ "(\<leadsto>\<^sub>w\<^sup>*)", OF _ _
                 remove_strictly_subsumed_clauses_in_Q[of "[]" _ _ "[]", unfolded append_Nil],
                 OF refl])
             (auto simp: filter_q)
         also note proc_C[unfolded c'_nil, THEN tranclp.r_into_trancl[of "(\<leadsto>\<^sub>w)"]]
         also have "wstate_of_dstate (N', [([], i)], [], n)
             \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ([], [([], i)], [], n)"
           by (rule empty_N_if_Nil_in_P_or_Q) simp
         also have "\<dots> \<leadsto>\<^sub>w wstate_of_dstate ([], [], [([], i)], Suc n)"
           by (rule arg_cong2[THEN iffD1, of _ _ _ _ "(\<leadsto>\<^sub>w)", OF _ _
                 wrp.inference_computation[of "{#}" "{#}" i "{#}" n "{#}"]])
             (auto simp: ord_FO_resolution_inferences_between_empty_empty)
         finally show ?thesis
           unfolding step st n_cons ci .
       next
         case c'_nnil: False
         note step = step[simplified c'_nnil, simplified]
         show ?thesis
         proof (cases "is_tautology C' \<or> subsume (map fst P @ map fst Q) C'")
           case taut_or_subs: True
           note step = step[simplified taut_or_subs, simplified]
 
           have "wstate_of_dstate ((C', i) # N', P, Q, n) \<leadsto>\<^sub>w wstate_of_dstate (N', P, Q, n)"
           proof (cases "is_tautology C'")
             case True
             then obtain A :: 'a where
               neg_a: "Neg A \<in> set C'" and pos_a: "Pos A \<in> set C'"
               unfolding is_tautology_def by blast
             show ?thesis
               by (rule arg_cong2[THEN iffD1, of _ _ _ _ "(\<leadsto>\<^sub>w)", OF _ _
                     wrp.tautology_deletion[of A "mset C'" "mset (map (apfst mset) N')" i
                       "mset (map (apfst mset) P)" "mset (map (apfst mset) Q)" n]])
                 (use neg_a pos_a in simp_all)
           next
             case False
             then have "subsume (map fst P @ map fst Q) C'"
               using taut_or_subs by blast
             then obtain D :: "'a lclause" where
               d_in: "D \<in> set (map fst P @ map fst Q)" and
               subs: "subsumes (mset D) (mset C')"
               unfolding subsume_def by blast
             show ?thesis
               by (rule arg_cong2[THEN iffD1, of _ _ _ _ "(\<leadsto>\<^sub>w)", OF _ _
                     wrp.forward_subsumption[of "mset D" "mset (map (apfst mset) P)"
                       "mset (map (apfst mset) Q)" "mset C'" "mset (map (apfst mset) N')" i n]],
                   use d_in subs in \<open>auto simp: subsume_def\<close>)
           qed
           then show ?thesis
             unfolding step st n_cons ci using red_C by (rule rtranclp_into_tranclp1[rotated])
         next
           case not_taut_or_subs: False
           note step = step[simplified not_taut_or_subs, simplified]
 
           define P' :: "('a literal list \<times> nat) list" where
             "P' = reduce_all C' P"
 
           obtain back_to_P Q' :: "'a dclause list" where
             red_Q: "(back_to_P, Q') = reduce_all2 C' Q"
             by (metis prod.exhaust)
           note step = step[unfolded red_Q[symmetric], simplified]
 
           define Q'' :: "('a literal list \<times> nat) list" where
             "Q'' = filter (Not \<circ> strictly_subsume [C'] \<circ> fst) Q'"
           define P'' :: "('a literal list \<times> nat) list" where
             "P'' = filter (Not \<circ> strictly_subsume [C'] \<circ> fst) (back_to_P @ P')"
           note step = step[unfolded P'_def[symmetric] Q''_def[symmetric] P''_def[symmetric],
               simplified]
 
           note red_C
           also have "wstate_of_dstate ((C', i) # N', P, Q, n)
               \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ((C', i) # N', P', Q, n)"
             unfolding P'_def by (rule reduce_clauses_in_P[of _ _ "[]", unfolded append_Nil]) simp+
           also have "\<dots> \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ((C', i) # N', back_to_P @ P', Q', n)"
             unfolding P'_def
             by (rule reduce_clauses_in_Q[of C' _ _ "[]" Q, folded red_Q,
                   unfolded append_Nil prod.sel])
               (auto intro: reduce_idem simp: reduce_all_def)
           also have "\<dots> \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ((C', i) # N', back_to_P @ P', Q'', n)"
             unfolding Q''_def
             by (rule remove_strictly_subsumed_clauses_in_Q[of _ _ _ "[]", unfolded append_Nil])
               simp
           also have "\<dots> \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate ((C', i) # N', P'', Q'', n)"
             unfolding P''_def
             by (rule remove_strictly_subsumed_clauses_in_P[of _ _ "[]", unfolded append_Nil]) auto
           also note proc_C[THEN tranclp.r_into_trancl[of "(\<leadsto>\<^sub>w)"]]
           finally show ?thesis
             unfolding step st n_cons ci P''_def by simp
         qed
       qed
     qed
   qed
 qed
 
 lemma final_deterministic_RP_step: "is_final_dstate St \<Longrightarrow> deterministic_RP_step St = St"
   by (cases St) (auto simp: deterministic_RP_step.simps is_final_dstate.simps)
 
 lemma deterministic_RP_SomeD:
   assumes "deterministic_RP (N, P, Q, n) = Some R"
   shows "\<exists>N' P' Q' n'. (\<exists>k. (deterministic_RP_step ^^ k) (N, P, Q, n) = (N', P', Q', n'))
     \<and> is_final_dstate (N', P', Q', n') \<and> R = map fst Q'"
 proof (induct rule: deterministic_RP.raw_induct[OF _ assms])
   case (1 self_call St R)
   note ih = this(1) and step = this(2)
 
   obtain N P Q :: "'a dclause list" and n :: nat where
     st: "St = (N, P, Q, n)"
     by (cases St) blast
   note step = step[unfolded st, simplified]
 
   show ?case
   proof (cases "is_final_dstate (N, P, Q, n)")
     case True
     then have "(deterministic_RP_step ^^ 0) (N, P, Q, n) = (N, P, Q, n)
       \<and> is_final_dstate (N, P, Q, n) \<and> R = map fst Q"
       using step by simp
     then show ?thesis
       unfolding st by blast
   next
     case nonfinal: False
     note step = step[simplified nonfinal, simplified]
 
     obtain N' P' Q' :: "'a dclause list" and n' k :: nat where
       "(deterministic_RP_step ^^ k) (deterministic_RP_step (N, P, Q, n)) = (N', P', Q', n')" and
       "is_final_dstate (N', P', Q', n')"
       "R = map fst Q'"
       using ih[OF step] by blast
     then show ?thesis
       unfolding st funpow_Suc_right[symmetric, THEN fun_cong, unfolded comp_apply] by blast
   qed
 qed
 
 context
   fixes
     N0 :: "'a dclause list" and
     n0 :: nat and
     R :: "'a lclause list"
 begin
 
 abbreviation St0 :: "'a dstate" where
   "St0 \<equiv> (N0, [], [], n0)"
 
 abbreviation grounded_N0 where
   "grounded_N0 \<equiv> grounding_of_clss (set (map (mset \<circ> fst) N0))"
 
 abbreviation grounded_R :: "'a clause set" where
   "grounded_R \<equiv> grounding_of_clss (set (map mset R))"
 
 primcorec derivation_from :: "'a dstate \<Rightarrow> 'a dstate llist" where
   "derivation_from St =
    LCons St (if is_final_dstate St then LNil else derivation_from (deterministic_RP_step St))"
 
 abbreviation Sts :: "'a dstate llist" where
   "Sts \<equiv> derivation_from St0"
 
 abbreviation wSts :: "'a wstate llist" where
   "wSts \<equiv> lmap wstate_of_dstate Sts"
 
 lemma full_deriv_wSts_trancl_weighted_RP: "full_chain (\<leadsto>\<^sub>w\<^sup>+) wSts"
 proof -
   have "Sts' = derivation_from St0' \<Longrightarrow> full_chain (\<leadsto>\<^sub>w\<^sup>+) (lmap wstate_of_dstate Sts')"
     for St0' Sts'
   proof (coinduction arbitrary: St0' Sts' rule: full_chain.coinduct)
     case sts': full_chain
     show ?case
     proof (cases "is_final_dstate St0'")
       case True
       then have "ltl (lmap wstate_of_dstate Sts') = LNil"
         unfolding sts' by simp
       then have "lmap wstate_of_dstate Sts' = LCons (wstate_of_dstate St0') LNil"
         unfolding sts' by (subst derivation_from.code, subst (asm) derivation_from.code, auto)
       moreover have "\<And>St''. \<not> wstate_of_dstate St0' \<leadsto>\<^sub>w St''"
         using True by (rule is_final_dstate_imp_not_weighted_RP)
       ultimately show ?thesis
         by (meson tranclpD)
     next
       case nfinal: False
       have "lmap wstate_of_dstate Sts' =
         LCons (wstate_of_dstate St0') (lmap wstate_of_dstate (ltl Sts'))"
         unfolding sts' by (subst derivation_from.code) simp
       moreover have "ltl Sts' = derivation_from (deterministic_RP_step St0')"
         unfolding sts' using nfinal by (subst derivation_from.code) simp
       moreover have "wstate_of_dstate St0' \<leadsto>\<^sub>w\<^sup>+ wstate_of_dstate (lhd (ltl Sts'))"
         unfolding sts' using nonfinal_deterministic_RP_step[OF nfinal refl] nfinal
         by (subst derivation_from.code) simp
       ultimately show ?thesis
         by fastforce
     qed
   qed
   then show ?thesis
     by blast
 qed
 
 lemmas deriv_wSts_trancl_weighted_RP = full_chain_imp_chain[OF full_deriv_wSts_trancl_weighted_RP]
 
 definition sswSts :: "'a wstate llist" where
   "sswSts = (SOME wSts'.
      full_chain (\<leadsto>\<^sub>w) wSts' \<and> emb wSts wSts' \<and> lhd wSts' = lhd wSts \<and> llast wSts' = llast wSts)"
 
 lemma sswSts:
   "full_chain (\<leadsto>\<^sub>w) sswSts \<and> emb wSts sswSts \<and> lhd sswSts = lhd wSts \<and> llast sswSts = llast wSts"
   unfolding sswSts_def
   by (rule someI_ex[OF full_chain_tranclp_imp_exists_full_chain[OF
           full_deriv_wSts_trancl_weighted_RP]])
 
 lemmas full_deriv_sswSts_weighted_RP = sswSts[THEN conjunct1]
 lemmas emb_sswSts = sswSts[THEN conjunct2, THEN conjunct1]
 lemmas lfinite_sswSts_iff = emb_lfinite[OF emb_sswSts]
 lemmas lhd_sswSts = sswSts[THEN conjunct2, THEN conjunct2, THEN conjunct1]
 lemmas llast_sswSts = sswSts[THEN conjunct2, THEN conjunct2, THEN conjunct2]
 
 lemmas deriv_sswSts_weighted_RP = full_chain_imp_chain[OF full_deriv_sswSts_weighted_RP]
 
 lemma not_lnull_sswSts: "\<not> lnull sswSts"
   using deriv_sswSts_weighted_RP by (cases rule: chain.cases) auto
 
 lemma empty_ssgP0: "wrp.P_of_wstate (lhd sswSts) = {}"
   unfolding lhd_sswSts by (subst derivation_from.code) simp
 
 lemma empty_ssgQ0: "wrp.Q_of_wstate (lhd sswSts) = {}"
   unfolding lhd_sswSts by (subst derivation_from.code) simp
 
 lemmas sswSts_thms = full_deriv_sswSts_weighted_RP empty_ssgP0 empty_ssgQ0
 
 abbreviation S_ssgQ :: "'a clause \<Rightarrow> 'a clause" where
   "S_ssgQ \<equiv> wrp.S_gQ sswSts"
 
 abbreviation ord_\<Gamma> :: "'a inference set" where
   "ord_\<Gamma> \<equiv> ground_resolution_with_selection.ord_\<Gamma> S_ssgQ"
 
 abbreviation Rf :: "'a clause set \<Rightarrow> 'a clause set" where
   "Rf \<equiv> standard_redundancy_criterion.Rf"
 
 abbreviation Ri :: "'a clause set \<Rightarrow> 'a inference set" where
   "Ri \<equiv> standard_redundancy_criterion.Ri ord_\<Gamma>"
 
 abbreviation saturated_upto :: "'a clause set \<Rightarrow> bool" where
   "saturated_upto \<equiv> redundancy_criterion.saturated_upto ord_\<Gamma> Rf Ri"
 
 context
   assumes drp_some: "deterministic_RP St0 = Some R"
 begin
 
 lemma lfinite_Sts: "lfinite Sts"
 proof (induct rule: deterministic_RP.raw_induct[OF _ drp_some])
   case (1 self_call St St')
   note ih = this(1) and step = this(2)
   show ?case
     using step by (subst derivation_from.code, auto intro: ih)
 qed
 
 lemma lfinite_wSts: "lfinite wSts"
   by (rule lfinite_lmap[THEN iffD2, OF lfinite_Sts])
 
 lemmas lfinite_sswSts = lfinite_sswSts_iff[THEN iffD2, OF lfinite_wSts]
 
 theorem
   deterministic_RP_saturated: "saturated_upto grounded_R" (is ?saturated) and
   deterministic_RP_model: "I \<Turnstile>s grounded_N0 \<longleftrightarrow> I \<Turnstile>s grounded_R" (is ?model)
 proof -
   obtain N' P' Q' :: "'a dclause list" and n' k :: nat where
     k_steps: "(deterministic_RP_step ^^ k) St0 = (N', P', Q', n')" (is "_ = ?Stk") and
     final: "is_final_dstate (N', P', Q', n')" and
     r: "R = map fst Q'"
     using deterministic_RP_SomeD[OF drp_some] by blast
 
   have wrp: "wstate_of_dstate St0 \<leadsto>\<^sub>w\<^sup>* wstate_of_dstate (llast Sts)"
     using lfinite_chain_imp_rtranclp_lhd_llast
     by (metis (no_types) deriv_sswSts_weighted_RP derivation_from.disc_iff derivation_from.simps(2)
         lfinite_Sts lfinite_sswSts llast_lmap llist.map_sel(1) sswSts)
 
   have last_sts: "llast Sts = ?Stk"
   proof -
     have "(deterministic_RP_step ^^ k') St0' = ?Stk \<Longrightarrow> llast (derivation_from St0') = ?Stk"
       for St0' k'
     proof (induct k' arbitrary: St0')
       case 0
       then show ?case
         using final by (subst derivation_from.code) simp
     next
       case (Suc k')
       note ih = this(1) and suc_k'_steps = this(2)
       show ?case
       proof (cases "is_final_dstate St0'")
         case True
         then show ?thesis
           using ih[of "deterministic_RP_step St0'"] suc_k'_steps final_deterministic_RP_step
             funpow_fixpoint[of deterministic_RP_step]
           by auto
       next
         case False
         then show ?thesis
           using ih[of "deterministic_RP_step St0'"] suc_k'_steps
           by (subst derivation_from.code) (simp add: llast_LCons funpow_swap1[symmetric])
       qed
     qed
     then show ?thesis
       using k_steps by blast
   qed
 
   have fin_gr_fgsts: "lfinite (lmap wrp.grounding_of_wstate sswSts)"
     by (rule lfinite_lmap[THEN iffD2, OF lfinite_sswSts])
 
   have lim_last: "Liminf_llist (lmap wrp.grounding_of_wstate sswSts) =
     wrp.grounding_of_wstate (llast sswSts)"
     unfolding lfinite_Liminf_llist[OF fin_gr_fgsts] llast_lmap[OF lfinite_sswSts not_lnull_sswSts]
     using not_lnull_sswSts by simp
 
   have gr_st0: "wrp.grounding_of_wstate (wstate_of_dstate St0) = grounded_N0"
     unfolding comp_def by simp
 
   have "?saturated \<and> ?model"
   proof (cases "[] \<in> set R")
     case True
     then have emp_in: "{#} \<in> grounded_R"
       unfolding grounding_of_clss_def grounding_of_cls_def by (auto intro: ex_ground_subst)
 
     have "grounded_R \<subseteq> wrp.grounding_of_wstate (llast sswSts)"
       unfolding r llast_sswSts
       by (simp add: last_sts llast_lmap[OF lfinite_Sts] grounding_of_clss_def)
     then have gr_last_st: "grounded_R \<subseteq> wrp.grounding_of_wstate (wstate_of_dstate (llast Sts))"
       by (simp add: lfinite_Sts llast_lmap llast_sswSts)
 
     have gr_r_fls: "\<not> I \<Turnstile>s grounded_R"
       using emp_in unfolding true_clss_def by force
     then have gr_last_fls: "\<not> I \<Turnstile>s wrp.grounding_of_wstate (wstate_of_dstate (llast Sts))"
       using gr_last_st unfolding true_clss_def by auto
 
     have ?saturated
       unfolding wrp.ord_\<Gamma>_saturated_upto_def[OF sswSts_thms]
         wrp.ord_\<Gamma>_contradiction_Rf[OF sswSts_thms emp_in] inference_system.inferences_from_def
       by auto
     moreover have ?model
       unfolding gr_r_fls[THEN eq_False[THEN iffD2]]
       by (rule rtranclp_imp_eq_image[of "(\<leadsto>\<^sub>w)" "\<lambda>St. I \<Turnstile>s wrp.grounding_of_wstate St", OF _ wrp,
             unfolded gr_st0 gr_last_fls[THEN eq_False[THEN iffD2]]])
         (use wrp.weighted_RP_model[OF sswSts_thms] in blast)
     ultimately show ?thesis
       by blast
   next
     case False
     then have gr_last: "wrp.grounding_of_wstate (llast sswSts) = grounded_R"
       using final unfolding r llast_sswSts
       by (simp add: last_sts llast_lmap[OF lfinite_Sts] comp_def is_final_dstate.simps)
     then have gr_last_st: "wrp.grounding_of_wstate (wstate_of_dstate (llast Sts)) = grounded_R"
       by (simp add: lfinite_Sts llast_lmap llast_sswSts)
 
     have ?saturated
       using wrp.weighted_RP_saturated[OF sswSts_thms, unfolded gr_last lim_last] by auto
     moreover have ?model
       by (rule rtranclp_imp_eq_image[of "(\<leadsto>\<^sub>w)" "\<lambda>St. I \<Turnstile>s wrp.grounding_of_wstate St", OF _ wrp,
             unfolded gr_st0 gr_last_st])
         (use wrp.weighted_RP_model[OF sswSts_thms] in blast)
     ultimately show ?thesis
       by blast
   qed
   then show ?saturated and ?model
     by blast+
 qed
 
 corollary deterministic_RP_refutation:
   "\<not> satisfiable grounded_N0 \<longleftrightarrow> {#} \<in> grounded_R" (is "?lhs \<longleftrightarrow> ?rhs")
 proof
   assume ?rhs
   then have "\<not> satisfiable grounded_R"
     unfolding true_clss_def true_cls_def by force
   then show ?lhs
     using deterministic_RP_model[THEN iffD1] by blast
 next
   assume ?lhs
   then have "\<not> satisfiable grounded_R"
     using deterministic_RP_model[THEN iffD2] by blast
   then show ?rhs
     unfolding wrp.ord_\<Gamma>_saturated_upto_complete[OF sswSts_thms deterministic_RP_saturated] .
 qed
 
 end
 
 context
   assumes drp_none: "deterministic_RP St0 = None"
 begin
 
 theorem deterministic_RP_complete: "satisfiable grounded_N0"
 proof (rule ccontr)
   assume unsat: "\<not> satisfiable grounded_N0"
 
   have unsat_wSts0: "\<not> satisfiable (wrp.grounding_of_wstate (lhd wSts))"
     using unsat by (subst derivation_from.code) (simp add: comp_def)
 
   have bot_in_ss: "{#} \<in> Q_of_state (wrp.Liminf_wstate sswSts)"
     by (rule wrp.weighted_RP_complete[OF sswSts_thms unsat_wSts0[folded lhd_sswSts]])
   have bot_in_lim: "{#} \<in> Q_of_state (wrp.Liminf_wstate wSts)"
   proof (cases "lfinite Sts")
     case fin: True
     have "wrp.Liminf_wstate sswSts = wrp.Liminf_wstate wSts"
       by (rule Liminf_state_fin, simp_all add: fin lfinite_sswSts_iff not_lnull_sswSts,
           subst (1 2) llast_lmap,
           simp_all add: lfinite_sswSts_iff fin not_lnull_sswSts llast_sswSts)
     then show ?thesis
       using bot_in_ss by simp
   next
     case False
     then show ?thesis
       using bot_in_ss Q_of_Liminf_state_inf[OF _ emb_lmap[OF emb_sswSts]] by auto
   qed
   then obtain k :: nat where
     k_lt: "enat k < llength Sts" and
     emp_in: "{#} \<in> wrp.Q_of_wstate (lnth wSts k)"
     unfolding Liminf_state_def Liminf_llist_def by auto
   have emp_in: "{#} \<in> Q_of_state (state_of_dstate ((deterministic_RP_step ^^ k) St0))"
   proof -
     have "enat k < llength Sts' \<Longrightarrow> Sts' = derivation_from St0' \<Longrightarrow>
       {#} \<in> wrp.Q_of_wstate (lnth (lmap wstate_of_dstate Sts') k) \<Longrightarrow>
       {#} \<in> Q_of_state (state_of_dstate ((deterministic_RP_step ^^ k) St0'))" for St0' Sts' k
     proof (induction k arbitrary: St0' Sts')
       case 0
       then show ?case
         by (subst (asm) derivation_from.code, cases St0', auto simp: comp_def)
     next
       case (Suc k)
       note ih = this(1) and sk_lt = this(2) and sts' = this(3) and emp_in_sk = this(4)
 
       have k_lt: "enat k < llength (ltl Sts')"
         using sk_lt by (cases Sts') (auto simp: Suc_ile_eq)
       moreover have "ltl Sts' = derivation_from (deterministic_RP_step St0')"
         using sts' k_lt by (cases Sts') auto
       moreover have "{#} \<in> wrp.Q_of_wstate (lnth (lmap wstate_of_dstate (ltl Sts')) k)"
         using emp_in_sk k_lt by (cases Sts') auto
       ultimately show ?case
         using ih[of "ltl Sts'" "deterministic_RP_step St0'"] by (simp add: funpow_swap1)
     qed
     then show ?thesis
       using k_lt emp_in by blast
   qed
   have "deterministic_RP St0 \<noteq> None"
     by (rule is_final_dstate_funpow_imp_deterministic_RP_neq_None[of "Suc k"],
         cases "(deterministic_RP_step ^^ k) St0",
         use emp_in in \<open>force simp: deterministic_RP_step.simps is_final_dstate.simps\<close>)
   then show False
     using drp_none ..
 qed
 
 end
 
 end
 
 end
 
 end
diff --git a/thys/Functional_Ordered_Resolution_Prover/ROOT b/thys/Functional_Ordered_Resolution_Prover/ROOT
--- a/thys/Functional_Ordered_Resolution_Prover/ROOT
+++ b/thys/Functional_Ordered_Resolution_Prover/ROOT
@@ -1,16 +1,17 @@
 chapter AFP
 
 session Functional_Ordered_Resolution_Prover (AFP) = "HOL-Library" +
   options [timeout = 600]
   sessions
     First_Order_Terms
+    Lambda_Free_RPOs
     Nested_Multisets_Ordinals
+    Open_Induction
     Ordered_Resolution_Prover
-    Open_Induction
     Polynomial_Factorization
   theories
     Deterministic_FO_Ordered_Resolution_Prover
     IsaFoR_Term
     Executable_Subsumption
   document_files
     "root.tex"
diff --git a/thys/Functional_Ordered_Resolution_Prover/Weighted_FO_Ordered_Resolution_Prover.thy b/thys/Functional_Ordered_Resolution_Prover/Weighted_FO_Ordered_Resolution_Prover.thy
--- a/thys/Functional_Ordered_Resolution_Prover/Weighted_FO_Ordered_Resolution_Prover.thy
+++ b/thys/Functional_Ordered_Resolution_Prover/Weighted_FO_Ordered_Resolution_Prover.thy
@@ -1,889 +1,836 @@
 (*  Title:       A Fair Ordered Resolution Prover for First-Order Clauses with Weights
     Author:      Anders Schlichtkrull <andschl at dtu.dk>, 2017
     Author:      Jasmin Blanchette <j.c.blanchette at vu.nl>, 2017
     Maintainer:  Anders Schlichtkrull <andschl at dtu.dk>
 *)
 
 section \<open>A Fair Ordered Resolution Prover for First-Order Clauses with Weights\<close>
 
 text \<open>
 The \<open>weighted_RP\<close> prover introduced below operates on finite multisets of clauses and
 organizes the multiset of processed clauses as a priority queue to ensure that inferences are
 performed in a fair manner, to guarantee completeness.
 \<close>
 
 theory Weighted_FO_Ordered_Resolution_Prover
   imports Ordered_Resolution_Prover.FO_Ordered_Resolution_Prover
 begin
 
 
-subsection \<open>Library\<close>
-
-(* TODO: Move to "Coinductive"? *)
-lemma ldrop_Suc_conv_ltl: "ldrop (enat (Suc k)) xs = ltl (ldrop (enat k) xs)"
-  by (metis eSuc_enat ldrop_eSuc_conv_ltl)
-
-(* TODO: Move to "Coinductive"? *)
-lemma lhd_ldrop':
-  assumes "enat k < llength xs"
-  shows "lhd (ldrop (enat k) xs) = lnth xs k"
-  using assms by (simp add: lhd_ldrop)
-
-(* TODO: Move to "Multiset_More.thy". *)
-lemma filter_mset_empty_if_finite_and_filter_set_empty:
-  assumes
-    "{x \<in> X. P x} = {}" and
-    "finite X"
-  shows "{#x \<in># mset_set X. P x#} = {#}"
-proof -
-  have empty_empty: "\<And>Y. set_mset Y = {} \<Longrightarrow> Y = {#}"
-    by auto
-  from assms have "set_mset {#x \<in># mset_set X. P x#} = {}"
-    by auto
-  then show ?thesis
-    by (rule empty_empty)
-qed
-
-(* TODO: Move to "Lazy_List_Chain.thy". *)
-lemma inf_chain_ltl_chain: "chain R xs \<Longrightarrow> llength xs = \<infinity> \<Longrightarrow> chain R (ltl xs)"
-  unfolding chain.simps[of R xs] llength_eq_infty_conv_lfinite
-  by (metis lfinite_code(1) lfinite_ltl llist.sel(3))
-
-(* TODO: Move to "Lazy_List_Chain.thy". *)
-lemma inf_chain_ldrop_chain:
-  assumes
-    chain: "chain R xs" and
-    inf: "\<not> lfinite xs"
-  shows "chain R (ldrop (enat k) xs)"
-proof (induction k)
-  case 0
-  then show ?case
-    using zero_enat_def chain by auto
-next
-  case (Suc k)
-  have "llength (ldrop (enat k) xs) = \<infinity>"
-    using inf by (simp add: not_lfinite_llength)
-  with Suc have "chain R (ltl (ldrop (enat k) xs))"
-    using inf_chain_ltl_chain[of R "(ldrop (enat k) xs)"] by auto
-  then show ?case
-    using ldrop_Suc_conv_ltl[of k xs] by auto
-qed
-
-
 subsection \<open>Prover\<close>
 
 type_synonym 'a wclause = "'a clause \<times> nat"
 type_synonym 'a wstate = "'a wclause multiset \<times> 'a wclause multiset \<times> 'a wclause multiset \<times> nat"
 
 fun state_of_wstate :: "'a wstate \<Rightarrow> 'a state" where
   "state_of_wstate (N, P, Q, n) =
    (set_mset (image_mset fst N), set_mset (image_mset fst P), set_mset (image_mset fst Q))"
 
 locale weighted_FO_resolution_prover =
   FO_resolution_prover S subst_atm id_subst comp_subst renamings_apart atm_of_atms mgu less_atm
   for
     S :: "('a :: wellorder) clause \<Rightarrow> 'a clause" and
     subst_atm :: "'a \<Rightarrow> 's \<Rightarrow> 'a" and
     id_subst :: "'s" and
     comp_subst :: "'s \<Rightarrow> 's \<Rightarrow> 's" and
     renamings_apart :: "'a clause list \<Rightarrow> 's list" and
     atm_of_atms :: "'a list \<Rightarrow> 'a" and
     mgu :: "'a set set \<Rightarrow> 's option" and
     less_atm :: "'a \<Rightarrow> 'a \<Rightarrow> bool" +
   fixes
     weight :: "'a clause \<times> nat \<Rightarrow> nat"
   assumes
     weight_mono: "i < j \<Longrightarrow> weight (C, i) < weight (C, j)"
 begin
 
 abbreviation clss_of_wstate :: "'a wstate \<Rightarrow> 'a clause set" where
   "clss_of_wstate St \<equiv> clss_of_state (state_of_wstate St)"
 
 abbreviation N_of_wstate :: "'a wstate \<Rightarrow> 'a clause set" where
   "N_of_wstate St \<equiv> N_of_state (state_of_wstate St)"
 
 abbreviation P_of_wstate :: "'a wstate \<Rightarrow> 'a clause set" where
   "P_of_wstate St \<equiv> P_of_state (state_of_wstate St)"
 
 abbreviation Q_of_wstate :: "'a wstate \<Rightarrow> 'a clause set" where
   "Q_of_wstate St \<equiv> Q_of_state (state_of_wstate St)"
 
 fun wN_of_wstate :: "'a wstate \<Rightarrow> 'a wclause multiset" where
   "wN_of_wstate (N, P, Q, n) = N"
 
 fun wP_of_wstate :: "'a wstate \<Rightarrow> 'a wclause multiset" where
   "wP_of_wstate (N, P, Q, n) = P"
 
 fun wQ_of_wstate :: "'a wstate \<Rightarrow> 'a wclause multiset" where
   "wQ_of_wstate (N, P, Q, n) = Q"
 
 fun n_of_wstate :: "'a wstate \<Rightarrow> nat" where
   "n_of_wstate (N, P, Q, n) = n"
 
 lemma of_wstate_split[simp]:
   "(wN_of_wstate St, wP_of_wstate St, wQ_of_wstate St, n_of_wstate St) = St"
   by (cases St) auto
 
 abbreviation grounding_of_wstate :: "'a wstate \<Rightarrow> 'a clause set" where
   "grounding_of_wstate St \<equiv> grounding_of_state (state_of_wstate St)"
 
 abbreviation Liminf_wstate :: "'a wstate llist \<Rightarrow> 'a state" where
   "Liminf_wstate Sts \<equiv> Liminf_state (lmap state_of_wstate Sts)"
 
 lemma timestamp_le_weight: "n \<le> weight (C, n)"
   by (induct n, simp, metis weight_mono[of k "Suc k" for k] Suc_le_eq le_less le_trans)
 
 inductive weighted_RP :: "'a wstate \<Rightarrow> 'a wstate \<Rightarrow> bool" (infix "\<leadsto>\<^sub>w" 50) where
   tautology_deletion: "Neg A \<in># C \<Longrightarrow> Pos A \<in># C \<Longrightarrow> (N + {#(C, i)#}, P, Q, n) \<leadsto>\<^sub>w (N, P, Q, n)"
 | forward_subsumption: "D \<in># image_mset fst (P + Q) \<Longrightarrow> subsumes D C \<Longrightarrow>
     (N + {#(C, i)#}, P, Q, n) \<leadsto>\<^sub>w (N, P, Q, n)"
 | backward_subsumption_P: "D \<in># image_mset fst N \<Longrightarrow> C \<in># image_mset fst P \<Longrightarrow>
     strictly_subsumes D C \<Longrightarrow> (N, P, Q, n) \<leadsto>\<^sub>w (N, {#(E, k) \<in># P. E \<noteq> C#}, Q, n)"
 | backward_subsumption_Q: "D \<in># image_mset fst N \<Longrightarrow> strictly_subsumes D C \<Longrightarrow>
     (N, P, Q + {#(C, i)#}, n) \<leadsto>\<^sub>w (N, P, Q, n)"
 | forward_reduction: "D + {#L'#} \<in># image_mset fst (P + Q) \<Longrightarrow> - L = L' \<cdot>l \<sigma> \<Longrightarrow> D \<cdot> \<sigma> \<subseteq># C \<Longrightarrow>
     (N + {#(C + {#L#}, i)#}, P, Q, n) \<leadsto>\<^sub>w (N + {#(C, i)#}, P, Q, n)"
 | backward_reduction_P: "D + {#L'#} \<in># image_mset fst N \<Longrightarrow> - L = L' \<cdot>l \<sigma> \<Longrightarrow> D \<cdot> \<sigma> \<subseteq># C \<Longrightarrow>
     (\<forall>j. (C + {#L#}, j) \<in># P \<longrightarrow> j \<le> i) \<Longrightarrow>
     (N, P + {#(C + {#L#}, i)#}, Q, n) \<leadsto>\<^sub>w (N, P + {#(C, i)#}, Q, n)"
 | backward_reduction_Q: "D + {#L'#} \<in># image_mset fst N \<Longrightarrow> - L = L' \<cdot>l \<sigma> \<Longrightarrow> D \<cdot> \<sigma> \<subseteq># C \<Longrightarrow>
     (N, P, Q + {#(C + {#L#}, i)#}, n) \<leadsto>\<^sub>w (N, P + {#(C, i)#}, Q, n)"
 | clause_processing: "(N + {#(C, i)#}, P, Q, n) \<leadsto>\<^sub>w (N, P + {#(C, i)#}, Q, n)"
 | inference_computation: "(\<forall>(D, j) \<in># P. weight (C, i) \<le> weight (D, j)) \<Longrightarrow>
     N = mset_set ((\<lambda>D. (D, n)) ` concls_of
       (inference_system.inferences_between (ord_FO_\<Gamma> S) (set_mset (image_mset fst Q)) C)) \<Longrightarrow>
     ({#}, P + {#(C, i)#}, Q, n) \<leadsto>\<^sub>w (N, {#(D, j) \<in># P. D \<noteq> C#}, Q + {#(C, i)#}, Suc n)"
 
 lemma weighted_RP_imp_RP: "St \<leadsto>\<^sub>w St' \<Longrightarrow> state_of_wstate St \<leadsto> state_of_wstate St'"
 proof (induction rule: weighted_RP.induct)
   case (backward_subsumption_P D N C P Q n)
   show ?case
     by (rule arg_cong2[THEN iffD1, of _ _ _ _ "(\<leadsto>)", OF _ _
           RP.backward_subsumption_P[of D "fst ` set_mset N" C "fst ` set_mset P - {C}"
             "fst ` set_mset Q"]])
       (use backward_subsumption_P in auto)
 next
   case (inference_computation P C i N n Q)
   show ?case
      by (rule arg_cong2[THEN iffD1, of _ _ _ _ "(\<leadsto>)", OF _ _
            RP.inference_computation[of "fst ` set_mset N" "fst ` set_mset Q" C
              "fst ` set_mset P - {C}"]],
          use inference_computation(2) finite_ord_FO_resolution_inferences_between in
            \<open>auto simp: comp_def image_comp inference_system.inferences_between_def\<close>)
 qed (use RP.intros in simp_all)
 
 lemma final_weighted_RP: "\<not> ({#}, {#}, Q, n) \<leadsto>\<^sub>w St"
   by (auto elim: weighted_RP.cases)
 
 context
   fixes
     Sts :: "'a wstate llist"
   assumes
     full_deriv: "full_chain (\<leadsto>\<^sub>w) Sts" and
     empty_P0: "P_of_wstate (lhd Sts) = {}" and
     empty_Q0: "Q_of_wstate (lhd Sts) = {}"
 begin
 
 lemma finite_Sts0: "finite (clss_of_wstate (lhd Sts))"
   by (cases "lhd Sts") auto
 
 lemmas deriv = full_chain_imp_chain[OF full_deriv]
 lemmas lhd_lmap_Sts = llist.map_sel(1)[OF chain_not_lnull[OF deriv]]
 
 lemma deriv_RP: "chain (\<leadsto>) (lmap state_of_wstate Sts)"
   using deriv weighted_RP_imp_RP by (metis chain_lmap)
 
 lemma finite_Sts0_RP: "finite (clss_of_state (lhd (lmap state_of_wstate Sts)))"
   using finite_Sts0 chain_length_pos[OF deriv] by auto
 
 lemma empty_P0_RP: "P_of_state (lhd (lmap state_of_wstate Sts)) = {}"
   using empty_P0 chain_length_pos[OF deriv] by auto
 
 lemma empty_Q0_RP: "Q_of_state (lhd (lmap state_of_wstate Sts)) = {}"
   using empty_Q0 chain_length_pos[OF deriv] by auto
 
 lemmas Sts_thms = deriv_RP finite_Sts0_RP empty_P0_RP empty_Q0_RP
 
 theorem weighted_RP_model:
   "St \<leadsto>\<^sub>w St' \<Longrightarrow> I \<Turnstile>s grounding_of_wstate St' \<longleftrightarrow> I \<Turnstile>s grounding_of_wstate St"
   using RP_model Sts_thms weighted_RP_imp_RP by (simp only: comp_def)
 
 abbreviation S_gQ :: "'a clause \<Rightarrow> 'a clause" where
   "S_gQ \<equiv> S_Q (lmap state_of_wstate Sts)"
 
 interpretation sq: selection S_gQ
   unfolding S_Q_def[OF deriv_RP] using S_M_selects_subseteq S_M_selects_neg_lits selection_axioms
   by unfold_locales auto
 
 interpretation gd: ground_resolution_with_selection S_gQ
   by unfold_locales
 
 interpretation src: standard_redundancy_criterion_reductive gd.ord_\<Gamma>
   by unfold_locales
 
 interpretation src: standard_redundancy_criterion_counterex_reducing gd.ord_\<Gamma>
   "ground_resolution_with_selection.INTERP S_gQ"
   by unfold_locales
 
 lemmas ord_\<Gamma>_saturated_upto_def = src.saturated_upto_def
 lemmas ord_\<Gamma>_saturated_upto_complete = src.saturated_upto_complete
 lemmas ord_\<Gamma>_contradiction_Rf = src.contradiction_Rf
 
 theorem weighted_RP_sound:
   assumes "{#} \<in> clss_of_state (Liminf_wstate Sts)"
   shows "\<not> satisfiable (grounding_of_wstate (lhd Sts))"
   by (rule RP_sound[OF deriv_RP assms, unfolded lhd_lmap_Sts])
 
 abbreviation RP_filtered_measure :: "('a wclause \<Rightarrow> bool) \<Rightarrow> 'a wstate \<Rightarrow> nat \<times> nat \<times> nat" where
   "RP_filtered_measure \<equiv> \<lambda>p (N, P, Q, n).
      (sum_mset (image_mset (\<lambda>(C, i). Suc (size C)) {#Di \<in># N + P + Q. p Di#}),
       size {#Di \<in># N. p Di#}, size {#Di \<in># P. p Di#})"
 
 abbreviation RP_combined_measure :: "nat \<Rightarrow> 'a wstate \<Rightarrow> nat \<times> (nat \<times> nat \<times> nat) \<times> (nat \<times> nat \<times> nat)" where
   "RP_combined_measure \<equiv> \<lambda>w St.
      (w + 1 - n_of_wstate St, RP_filtered_measure (\<lambda>(C, i). i \<le> w) St,
       RP_filtered_measure (\<lambda>Ci. True) St)"
 
 abbreviation (input) RP_filtered_relation :: "((nat \<times> nat \<times> nat) \<times> (nat \<times> nat \<times> nat)) set" where
   "RP_filtered_relation \<equiv> natLess <*lex*> natLess <*lex*> natLess"
 
 abbreviation (input) RP_combined_relation :: "((nat \<times> ((nat \<times> nat \<times> nat) \<times> (nat \<times> nat \<times> nat))) \<times>
     (nat \<times> ((nat \<times> nat \<times> nat) \<times> (nat \<times> nat \<times> nat)))) set" where
   "RP_combined_relation \<equiv> natLess <*lex*> RP_filtered_relation <*lex*> RP_filtered_relation"
 
 abbreviation "(fst3 :: 'b * 'c * 'd \<Rightarrow> 'b) \<equiv> fst"
 abbreviation "(snd3 :: 'b * 'c * 'd \<Rightarrow> 'c) \<equiv> \<lambda>x. fst (snd x)"
 abbreviation "(trd3 :: 'b * 'c * 'd \<Rightarrow> 'd) \<equiv> \<lambda>x. snd (snd x)"
 
 lemma
   wf_RP_filtered_relation: "wf RP_filtered_relation" and
   wf_RP_combined_relation: "wf RP_combined_relation"
   unfolding natLess_def using wf_less wf_mult by auto
 
 lemma multiset_sum_of_Suc_f_monotone: "N \<subset># M \<Longrightarrow> (\<Sum>x \<in># N. Suc (f x)) < (\<Sum>x \<in># M. Suc (f x))"
 proof (induction N arbitrary: M)
   case empty
   then obtain y where "y \<in># M"
     by force
   then have "(\<Sum>x \<in># M. 1) = (\<Sum>x \<in># M - {#y#} + {#y#}. 1)"
     by auto
   also have "... = (\<Sum>x \<in># M - {#y#}. 1) + (\<Sum>x \<in># {#y#}. 1)"
     by (metis image_mset_union sum_mset.union)
   also have "... > (0 :: nat)"
     by auto
   finally have "0 < (\<Sum>x \<in># M. Suc (f x))"
     by (fastforce intro: gr_zeroI)
   then show ?case
     using empty by auto
 next
   case (add x N)
   from this(2) have "(\<Sum>y \<in># N. Suc (f y)) < (\<Sum>y \<in># M - {#x#}. Suc (f y))"
     using add(1)[of "M - {#x#}"] by (simp add: insert_union_subset_iff)
   moreover have "add_mset x (remove1_mset x M) = M"
     by (meson add.prems add_mset_remove_trivial_If mset_subset_insertD)
   ultimately show ?case
     by (metis (no_types) add.commute add_less_cancel_right sum_mset.insert)
 qed
 
 lemma multiset_sum_monotone_f':
   assumes "CC \<subset># DD"
   shows "(\<Sum>(C, i) \<in># CC. Suc (f C)) < (\<Sum>(C, i) \<in># DD. Suc (f C))"
   using multiset_sum_of_Suc_f_monotone[OF assms, of "f \<circ> fst"]
   by (metis (mono_tags) comp_apply image_mset_cong2 split_beta)
 
 lemma filter_mset_strict_subset:
   assumes "x \<in># M" and "\<not> p x"
   shows "{#y \<in># M. p y#} \<subset># M"
 proof -
   have subseteq: "{#E \<in># M. p E#} \<subseteq># M"
     by auto
   have "count {#E \<in># M. p E#} x = 0"
     using assms by auto
   moreover have "0 < count M x"
     using assms by auto
   ultimately have lt_count: "count {#y \<in># M. p y#} x < count M x"
     by auto
   then show ?thesis
     using subseteq by (metis less_not_refl2 subset_mset.le_neq_trans)
 qed
 
 lemma weighted_RP_measure_decreasing_N:
   assumes "St \<leadsto>\<^sub>w St'" and "(C, l) \<in># wN_of_wstate St"
   shows "(RP_filtered_measure (\<lambda>Ci. True) St', RP_filtered_measure (\<lambda>Ci. True) St)
     \<in> RP_filtered_relation"
 using assms proof (induction rule: weighted_RP.induct)
   case (backward_subsumption_P D N C' P Q n)
   then obtain i' where  "(C', i') \<in># P"
     by auto
   then have "{#(E, k) \<in># P. E \<noteq> C'#} \<subset># P"
     using filter_mset_strict_subset[of "(C', i')" P "\<lambda>X. \<not>fst X =  C'"]
     by (metis (mono_tags, lifting) filter_mset_cong fst_conv prod.case_eq_if)
   then have "(\<Sum>(C, i) \<in># {#(E, k) \<in># P. E \<noteq> C'#}. Suc (size C)) < (\<Sum>(C, i) \<in># P. Suc (size C))"
     using multiset_sum_monotone_f'[of "{#(E, k) \<in># P. E \<noteq> C'#}" P size] by metis
   then show ?case
     unfolding natLess_def by auto
 qed (auto simp: natLess_def)
 
 lemma weighted_RP_measure_decreasing_P:
   assumes "St \<leadsto>\<^sub>w St'" and "(C, i) \<in># wP_of_wstate St"
   shows "(RP_combined_measure (weight (C, i)) St', RP_combined_measure (weight (C, i)) St)
     \<in> RP_combined_relation"
 using assms proof (induction rule: weighted_RP.induct)
   case (backward_subsumption_P D N C' P Q n)
 
   define St where "St = (N, P, Q, n)"
   define P' where "P' = {#(E, k) \<in># P. E \<noteq> C'#}"
   define St' where "St' = (N, P', Q, n)"
 
   from backward_subsumption_P obtain i' where  "(C', i') \<in># P"
     by auto
   then have P'_sub_P: "P' \<subset># P"
     unfolding P'_def using filter_mset_strict_subset[of "(C', i')" P "\<lambda>Dj. fst Dj \<noteq> C'"]
     by (metis (no_types, lifting) filter_mset_cong fst_conv prod.case_eq_if)
 
   have P'_subeq_P_filter:
     "{#(Ca, ia) \<in># P'. ia \<le> weight (C, i)#} \<subseteq># {#(Ca, ia) \<in># P. ia \<le> weight (C, i)#}"
     using P'_sub_P by (auto intro: multiset_filter_mono)
 
   have "fst3 (RP_combined_measure (weight (C, i)) St')
     \<le> fst3 (RP_combined_measure (weight (C, i)) St)"
     unfolding St'_def St_def by auto
   moreover have "(\<Sum>(C, i) \<in># {#(Ca, ia) \<in># P'. ia \<le> weight (C, i)#}. Suc (size C))
     \<le> (\<Sum>x \<in># {#(Ca, ia) \<in># P. ia \<le> weight (C, i)#}. case x of (C, i) \<Rightarrow> Suc (size C))"
     using P'_subeq_P_filter by (rule sum_image_mset_mono)
   then have "fst3 (snd3 (RP_combined_measure (weight (C, i)) St'))
     \<le> fst3 (snd3 (RP_combined_measure (weight (C, i)) St))"
     unfolding St'_def St_def by auto
   moreover have "snd3 (snd3 (RP_combined_measure (weight (C, i)) St'))
     \<le> snd3 (snd3 (RP_combined_measure (weight (C, i)) St))"
     unfolding St'_def St_def by auto
   moreover from P'_subeq_P_filter have "size {#(Ca, ia) \<in># P'. ia \<le> weight (C, i)#}
     \<le> size {#(Ca, ia) \<in># P. ia \<le> weight (C, i)#}"
     by (simp add: size_mset_mono)
   then have "trd3 (snd3 (RP_combined_measure (weight (C, i)) St'))
     \<le> trd3 (snd3 (RP_combined_measure (weight (C, i)) St))"
     unfolding St'_def St_def unfolding fst_def snd_def by auto
   moreover from P'_sub_P have "(\<Sum>(C, i) \<in># P'. Suc (size C)) < (\<Sum>(C, i) \<in># P. Suc (size C))"
     using multiset_sum_monotone_f'[of "{#(E, k) \<in># P. E \<noteq> C'#}" P size] unfolding P'_def by metis
   then have "fst3 (trd3 (RP_combined_measure (weight (C, i)) St'))
     < fst3 (trd3 (RP_combined_measure (weight (C, i)) St))"
     unfolding P'_def St'_def St_def by auto
   ultimately show ?case
     unfolding natLess_def P'_def St'_def St_def by auto
 next
   case (inference_computation P C' i' N n Q)
   then show ?case
   proof (cases "n \<le> weight (C, i)")
     case True
     then have "weight (C, i) + 1 - n > weight (C, i) + 1 - Suc n"
       by auto
     then show ?thesis
       unfolding natLess_def by auto
   next
     case n_nle_w: False
 
     define St :: "'a wstate" where "St = ({#}, P + {#(C', i')#}, Q, n)"
     define St' :: "'a wstate" where "St' =  (N, {#(D, j) \<in># P. D \<noteq> C'#}, Q + {#(C', i')#}, Suc n)"
     define concls :: "'a wclause set" where
       "concls = (\<lambda>D. (D, n)) ` concls_of (inference_system.inferences_between (ord_FO_\<Gamma> S)
          (fst ` set_mset Q) C')"
 
     have fin: "finite concls"
       unfolding concls_def using finite_ord_FO_resolution_inferences_between by auto
 
     have "{(D, ia) \<in> concls. ia \<le> weight (C, i)} = {}"
       unfolding concls_def using n_nle_w by auto
     then have "{#(D, ia) \<in># mset_set concls. ia \<le> weight (C, i)#} = {#}"
       using fin filter_mset_empty_if_finite_and_filter_set_empty[of concls] by auto
     then have n_low_weight_empty: "{#(D, ia) \<in># N. ia \<le> weight (C, i)#} = {#}"
       unfolding inference_computation unfolding concls_def by auto
 
     have "weight (C', i') \<le> weight (C, i)"
       using inference_computation by auto
     then have i'_le_w_Ci: "i' \<le> weight (C, i)"
       using timestamp_le_weight[of i' C'] by auto
 
     have subs: "{#(D, ia) \<in># N + {#(D, j) \<in># P. D \<noteq> C'#} + (Q + {#(C', i')#}). ia \<le> weight (C, i)#}
       \<subseteq># {#(D, ia) \<in># {#} + (P + {#(C', i')#}) + Q. ia \<le> weight (C, i)#}"
       using n_low_weight_empty by (auto simp: multiset_filter_mono)
 
     have "fst3 (RP_combined_measure (weight (C, i)) St')
       \<le> fst3 (RP_combined_measure (weight (C, i)) St)"
       unfolding St'_def St_def by auto
     moreover have "fst (RP_filtered_measure ((\<lambda>(D, ia). ia \<le> weight (C, i))) St') =
       (\<Sum>(C, i) \<in># {#(D, ia) \<in># N + {#(D, j) \<in># P. D \<noteq> C'#} + (Q + {#(C', i')#}).
          ia \<le> weight (C, i)#}. Suc (size C))"
       unfolding St'_def by auto
     also have "... \<le> (\<Sum>(C, i) \<in># {#(D, ia) \<in># {#} + (P + {#(C', i')#}) + Q. ia \<le> weight (C, i)#}.
       Suc (size C))"
       using subs sum_image_mset_mono by blast
     also have "... = fst (RP_filtered_measure (\<lambda>(D, ia). ia \<le> weight (C, i)) St)"
       unfolding St_def by auto
     finally have "fst3 (snd3 (RP_combined_measure (weight (C, i)) St'))
       \<le> fst3 (snd3 (RP_combined_measure (weight (C, i)) St))"
       by auto
     moreover have "snd3 (snd3 (RP_combined_measure (weight (C, i)) St')) =
       snd3 (snd3 (RP_combined_measure (weight (C, i)) St))"
       unfolding St_def St'_def using n_low_weight_empty by auto
     moreover have "trd3 (snd3 (RP_combined_measure (weight (C, i)) St')) <
       trd3 (snd3 (RP_combined_measure (weight (C, i)) St))"
       unfolding St_def St'_def using i'_le_w_Ci
       by (simp add: le_imp_less_Suc multiset_filter_mono size_mset_mono)
     ultimately show ?thesis
       unfolding natLess_def St'_def St_def lex_prod_def by force
   qed
 qed (auto simp: natLess_def)
 
 lemma preserve_min_or_delete_completely:
   assumes "St \<leadsto>\<^sub>w St'" "(C, i) \<in># wP_of_wstate St"
     "\<forall>k. (C, k) \<in># wP_of_wstate St \<longrightarrow> i \<le> k"
   shows "(C, i) \<in># wP_of_wstate St' \<or> (\<forall>j. (C, j) \<notin># wP_of_wstate St')"
 using assms proof (induction rule: weighted_RP.induct)
   case (backward_reduction_P D L' N L \<sigma> C' P i' Q n)
   show ?case
   proof (cases "C = C' + {#L#}")
     case True_outer: True
     then have C_i_in: "(C, i) \<in># P + {#(C, i')#}"
       using backward_reduction_P by auto
     then have max: "\<And>k. (C, k) \<in># P + {#(C, i')#} \<Longrightarrow> k \<le> i'"
       using backward_reduction_P unfolding True_outer[symmetric] by auto
     then have "count (P + {#(C, i')#}) (C, i') \<ge> 1"
       by auto
     moreover
     {
       assume asm: "count (P + {#(C, i')#}) (C, i') = 1"
       then have nin_P: "(C, i') \<notin># P"
         using not_in_iff by force
       have ?thesis
       proof (cases "(C, i) = (C, i')")
         case True
         then have "i = i'"
           by auto
         then have "\<forall>j. (C, j) \<in># P + {#(C, i')#} \<longrightarrow> j = i'"
           using max backward_reduction_P(6) unfolding True_outer[symmetric] by force
         then show ?thesis
           using True_outer[symmetric] nin_P by auto
       next
         case False
         then show ?thesis
           using C_i_in by auto
       qed
     }
     moreover
     {
       assume "count (P + {#(C, i')#}) (C, i') > 1"
       then have ?thesis
         using C_i_in by auto
     }
     ultimately show ?thesis
       by (cases "count (P + {#(C, i')#}) (C, i') = 1") auto
   next
     case False
     then show ?thesis
       using backward_reduction_P by auto
   qed
 qed auto
 
 lemma preserve_min_P:
   assumes
     "St \<leadsto>\<^sub>w St'" "(C, j) \<in># wP_of_wstate St'" and
     "(C, i) \<in># wP_of_wstate St" and
     "\<forall>k. (C, k) \<in># wP_of_wstate St \<longrightarrow> i \<le> k"
   shows "(C, i) \<in># wP_of_wstate St'"
   using assms preserve_min_or_delete_completely by blast
 
 lemma preserve_min_P_Sts:
   assumes
     "enat (Suc k) < llength Sts" and
     "(C, i) \<in># wP_of_wstate (lnth Sts k)" and
     "(C, j) \<in># wP_of_wstate (lnth Sts (Suc k))" and
     "\<forall>j. (C, j) \<in># wP_of_wstate (lnth Sts k) \<longrightarrow> i \<le> j"
   shows "(C, i) \<in># wP_of_wstate (lnth Sts (Suc k))"
   using deriv assms chain_lnth_rel preserve_min_P by metis
 
 lemma in_lnth_in_Supremum_ldrop:
   assumes "i < llength xs" and "x \<in># (lnth xs i)"
   shows "x \<in> Sup_llist (lmap set_mset (ldrop (enat i) xs))"
   using assms by (metis (no_types) ldrop_eq_LConsD ldropn_0 llist.simps(13) contra_subsetD
       ldrop_enat ldropn_Suc_conv_ldropn lnth_0 lnth_lmap lnth_subset_Sup_llist)
 
 lemma persistent_wclause_in_P_if_persistent_clause_in_P:
   assumes "C \<in> Liminf_llist (lmap P_of_state (lmap state_of_wstate Sts))"
   shows "\<exists>i. (C, i) \<in> Liminf_llist (lmap (set_mset \<circ> wP_of_wstate) Sts)"
 proof -
   obtain t_C where t_C_p:
     "enat t_C < llength Sts"
     "\<And>t. t_C \<le> t \<Longrightarrow> t < llength Sts \<Longrightarrow> C \<in> P_of_state (state_of_wstate (lnth Sts t))"
     using assms unfolding Liminf_llist_def by auto
   then obtain i where i_p:
     "(C, i) \<in># wP_of_wstate (lnth Sts t_C)"
     using t_C_p by (cases "lnth Sts t_C") force
 
   have Ci_in_nth_wP: "\<exists>i. (C, i) \<in># wP_of_wstate (lnth Sts (t_C + t))" if "t_C + t < llength Sts"
     for t
     using that t_C_p(2)[of "t_C + _"] by (cases "lnth Sts (t_C + t)") force
 
   define in_Sup_wP :: "nat \<Rightarrow> bool" where
     "in_Sup_wP = (\<lambda>i. (C, i) \<in> Sup_llist (lmap (set_mset \<circ> wP_of_wstate) (ldrop t_C Sts)))"
 
   have "in_Sup_wP i"
     using i_p assms(1) in_lnth_in_Supremum_ldrop[of t_C "lmap wP_of_wstate Sts" "(C, i)"] t_C_p
     by (simp add: in_Sup_wP_def llist.map_comp)
   then obtain j where j_p: "is_least in_Sup_wP j"
     unfolding in_Sup_wP_def[symmetric] using least_exists by metis
   then have "\<forall>i. (C, i) \<in> Sup_llist (lmap (set_mset \<circ> wP_of_wstate) (ldrop t_C Sts)) \<longrightarrow> j \<le> i"
     unfolding is_least_def in_Sup_wP_def using not_less by blast
   then have j_smallest:
     "\<And>i t. enat (t_C + t) < llength Sts \<Longrightarrow> (C, i) \<in># wP_of_wstate (lnth Sts (t_C + t)) \<Longrightarrow> j \<le> i"
     unfolding comp_def
     by (smt add.commute ldrop_enat ldrop_eq_LConsD ldrop_ldrop ldropn_Suc_conv_ldropn
         plus_enat_simps(1)  lnth_ldropn Sup_llist_def UN_I ldrop_lmap llength_lmap lnth_lmap
         mem_Collect_eq)
   from j_p have "\<exists>t_Cj. t_Cj < llength (ldrop (enat t_C) Sts)
     \<and> (C, j) \<in># wP_of_wstate (lnth (ldrop t_C Sts) t_Cj)"
     unfolding in_Sup_wP_def Sup_llist_def is_least_def by simp
   then obtain t_Cj where j_p:
     "(C,j) \<in># wP_of_wstate (lnth Sts (t_C + t_Cj))"
     "enat (t_C + t_Cj) < llength Sts"
     by (smt add.commute ldrop_enat ldrop_eq_LConsD ldrop_ldrop ldropn_Suc_conv_ldropn
         plus_enat_simps(1) lhd_ldropn)
   have Ci_stays:
     "t_C + t_Cj + t < llength Sts \<Longrightarrow> (C,j) \<in># wP_of_wstate (lnth Sts (t_C + t_Cj + t))" for t
   proof (induction t)
     case 0
     then show ?case
       using j_p by (simp add: add.commute)
   next
     case (Suc t)
     have any_Ck_in_wP: "j \<le> k" if "(C, k) \<in># wP_of_wstate (lnth Sts (t_C + t_Cj + t))" for k
       using that j_p j_smallest Suc
       by (smt Suc_ile_eq add.commute add.left_commute add_Suc less_imp_le plus_enat_simps(1)
           the_enat.simps)
     from Suc have Cj_in_wP: "(C, j) \<in># wP_of_wstate (lnth Sts (t_C + t_Cj + t))"
       by (metis (no_types, hide_lams) Suc_ile_eq add.commute add_Suc_right less_imp_le)
     moreover have "C \<in> P_of_state (state_of_wstate (lnth Sts (Suc (t_C + t_Cj + t))))"
       using t_C_p(2) Suc.prems by auto
     then have "\<exists>k. (C, k) \<in># wP_of_wstate (lnth Sts (Suc (t_C + t_Cj + t)))"
       by (smt Suc.prems Ci_in_nth_wP add.commute add.left_commute add_Suc_right enat_ord_code(4))
     ultimately have "(C, j) \<in># wP_of_wstate (lnth Sts (Suc (t_C + t_Cj + t)))"
       using preserve_min_P_Sts Cj_in_wP any_Ck_in_wP Suc.prems by force
     then have "(C, j) \<in># lnth (lmap wP_of_wstate Sts) (Suc (t_C + t_Cj + t))"
       using Suc.prems by auto
     then show ?case
       by (smt Suc.prems add.commute add_Suc_right lnth_lmap)
   qed
   then have "(\<And>t. t_C + t_Cj \<le> t \<Longrightarrow> t < llength (lmap (set_mset \<circ> wP_of_wstate) Sts) \<Longrightarrow>
     (C, j) \<in># wP_of_wstate (lnth Sts t))"
     using Ci_stays[of "_ - (t_C + t_Cj)"] by (metis le_add_diff_inverse llength_lmap)
   then have "(C, j) \<in> Liminf_llist (lmap (set_mset \<circ> wP_of_wstate) Sts)"
     unfolding Liminf_llist_def using j_p by auto
   then show "\<exists>i. (C, i) \<in> Liminf_llist (lmap (set_mset \<circ> wP_of_wstate) Sts)"
     by auto
 qed
 
 lemma lfinite_not_LNil_nth_llast:
   assumes "lfinite Sts" and "Sts \<noteq> LNil"
   shows "\<exists>i < llength Sts. lnth Sts i = llast Sts \<and> (\<forall>j < llength Sts. j \<le> i)"
 using assms proof (induction rule: lfinite.induct)
   case (lfinite_LConsI xs x)
   then show ?case
   proof (cases "xs = LNil")
     case True
     show ?thesis
       using True zero_enat_def by auto
   next
     case False
     then obtain i where
       i_p: "enat i < llength xs \<and> lnth xs i = llast xs \<and> (\<forall>j < llength xs. j \<le> enat i)"
       using lfinite_LConsI by auto
     then have "enat (Suc i) < llength (LCons x xs)"
       by (simp add: Suc_ile_eq)
     moreover from i_p have "lnth (LCons x xs) (Suc i) = llast (LCons x xs)"
       by (metis gr_implies_not_zero llast_LCons llength_lnull lnth_Suc_LCons)
     moreover from i_p have "\<forall>j < llength (LCons x xs). j \<le> enat (Suc i)"
       by (metis antisym_conv2 eSuc_enat eSuc_ile_mono ileI1 iless_Suc_eq llength_LCons)
     ultimately show ?thesis
       by auto
   qed
 qed auto
 
 lemma fair_if_finite:
   assumes fin: "lfinite Sts"
   shows "fair_state_seq (lmap state_of_wstate Sts)"
 proof (rule ccontr)
   assume unfair: "\<not> fair_state_seq (lmap state_of_wstate Sts)"
 
   have no_inf_from_last: "\<forall>y. \<not> llast Sts \<leadsto>\<^sub>w y"
     using fin full_chain_iff_chain[of "(\<leadsto>\<^sub>w)" Sts] full_deriv by auto
 
   from unfair obtain C where
     "C \<in> Liminf_llist (lmap N_of_state (lmap state_of_wstate Sts))
        \<union> Liminf_llist (lmap P_of_state (lmap state_of_wstate Sts))"
     unfolding fair_state_seq_def Liminf_state_def by auto
   then obtain i where i_p:
     "enat i < llength Sts"
     "\<And>j. i \<le> j \<Longrightarrow> enat j < llength Sts \<Longrightarrow>
      C \<in> N_of_state (state_of_wstate (lnth Sts j)) \<union> P_of_state (state_of_wstate (lnth Sts j))"
     unfolding Liminf_llist_def by auto
 
   have C_in_llast:
     "C \<in> N_of_state (state_of_wstate (llast Sts)) \<union> P_of_state (state_of_wstate (llast Sts))"
   proof -
     obtain l where
       l_p: "enat l < llength Sts \<and> lnth Sts l = llast Sts \<and> (\<forall>j < llength Sts. j \<le> enat l)"
       using fin lfinite_not_LNil_nth_llast i_p(1) by fastforce
     then have
       "C \<in> N_of_state (state_of_wstate (lnth Sts l)) \<union> P_of_state (state_of_wstate (lnth Sts l))"
       using i_p(1) i_p(2)[of l] by auto
     then show ?thesis
       using l_p by auto
   qed
 
   define N :: "'a wclause multiset" where "N = wN_of_wstate (llast Sts)"
   define P :: "'a wclause multiset" where "P = wP_of_wstate (llast Sts)"
   define Q :: "'a wclause multiset" where "Q = wQ_of_wstate (llast Sts)"
   define n :: nat where "n = n_of_wstate (llast Sts)"
 
   {
     assume "N_of_state (state_of_wstate (llast Sts)) \<noteq> {}"
     then obtain D j where "(D, j) \<in># N"
       unfolding N_def by (cases "llast Sts") auto
     then have "llast Sts \<leadsto>\<^sub>w (N - {#(D, j)#}, P + {#(D, j)#}, Q, n)"
       using weighted_RP.clause_processing[of "N - {#(D, j)#}" D j P Q n]
       unfolding N_def P_def Q_def n_def by auto
     then have "\<exists>St'. llast Sts \<leadsto>\<^sub>w St'"
       by auto
   }
   moreover
   {
     assume a: "N_of_state (state_of_wstate (llast Sts)) = {}"
     then have b: "N = {#}"
       unfolding N_def by (cases "llast Sts") auto
     from a have "C \<in> P_of_state (state_of_wstate (llast Sts))"
       using C_in_llast by auto
     then obtain D j where "(D, j) \<in># P"
       unfolding P_def by (cases "llast Sts") auto
     then have "weight (D, j) \<in> weight ` set_mset P"
       by auto
     then have "\<exists>w. is_least (\<lambda>w. w \<in> (weight ` set_mset P)) w"
       using least_exists by auto
     then have "\<exists>D j. (\<forall>(D', j') \<in># P. weight (D, j) \<le> weight (D', j')) \<and> (D, j) \<in># P"
       using assms linorder_not_less unfolding is_least_def by (auto 6 0)
     then obtain D j where
       min: "(\<forall>(D', j') \<in># P. weight (D, j) \<le> weight (D', j'))" and
       Dj_in_p: "(D, j) \<in># P"
       by auto
     from min have min: "(\<forall>(D', j') \<in># P - {#(D, j)#}. weight (D, j) \<le> weight (D', j'))"
       using mset_subset_diff_self[OF Dj_in_p] by auto
 
     define N' where
       "N' = mset_set ((\<lambda>D'. (D', n)) ` concls_of (inference_system.inferences_between (ord_FO_\<Gamma> S)
          (set_mset (image_mset fst Q)) D))"
 
     have "llast Sts \<leadsto>\<^sub>w (N', {#(D', j') \<in># P - {#(D, j)#}. D' \<noteq> D#}, Q + {#(D,j)#}, Suc n)"
       using weighted_RP.inference_computation[of "P - {#(D, j)#}" D j N' n Q, OF min N'_def]
         of_wstate_split[symmetric, of "llast Sts"] Dj_in_p
       unfolding N_def[symmetric] P_def[symmetric] Q_def[symmetric] n_def[symmetric] b by auto
     then have "\<exists>St'. llast Sts \<leadsto>\<^sub>w St'"
       by auto
   }
   ultimately have "\<exists>St'. llast Sts \<leadsto>\<^sub>w St'"
     by auto
   then show False
     using no_inf_from_last by metis
 qed
 
 lemma N_of_state_state_of_wstate_wN_of_wstate:
   assumes "C \<in> N_of_state (state_of_wstate St)"
   shows "\<exists>i. (C, i) \<in># wN_of_wstate St"
   by (smt N_of_state.elims assms eq_fst_iff fstI fst_conv image_iff of_wstate_split set_image_mset
       state_of_wstate.simps)
 
 lemma in_wN_of_wstate_in_N_of_wstate: "(C, i) \<in># wN_of_wstate St \<Longrightarrow> C \<in> N_of_wstate St"
   by (metis (mono_guards_query_query) N_of_state.simps fst_conv image_eqI of_wstate_split
       set_image_mset state_of_wstate.simps)
 
 lemma in_wP_of_wstate_in_P_of_wstate: "(C, i) \<in># wP_of_wstate St \<Longrightarrow> C \<in> P_of_wstate St"
   by (metis (mono_guards_query_query) P_of_state.simps fst_conv image_eqI of_wstate_split
       set_image_mset state_of_wstate.simps)
 
 lemma in_wQ_of_wstate_in_Q_of_wstate: "(C, i) \<in># wQ_of_wstate St \<Longrightarrow> C \<in> Q_of_wstate St"
   by (metis (mono_guards_query_query) Q_of_state.simps fst_conv image_eqI of_wstate_split
       set_image_mset state_of_wstate.simps)
 
 lemma n_of_wstate_weighted_RP_increasing: "St \<leadsto>\<^sub>w St' \<Longrightarrow> n_of_wstate St \<le> n_of_wstate St'"
   by (induction rule: weighted_RP.induct) auto
 
 lemma nth_of_wstate_monotonic:
   assumes "j < llength Sts" and "i \<le> j"
   shows "n_of_wstate (lnth Sts i) \<le> n_of_wstate (lnth Sts j)"
 using assms proof (induction "j - i" arbitrary: i)
   case (Suc x)
   then have "x = j - (i + 1)"
     by auto
   then have "n_of_wstate (lnth Sts (i + 1)) \<le> n_of_wstate (lnth Sts j)"
     using Suc by auto
   moreover have "i < j"
     using Suc by auto
   then have "Suc i < llength Sts"
     using Suc by (metis enat_ord_simps(2) le_less_Suc_eq less_le_trans not_le)
   then have "lnth Sts i \<leadsto>\<^sub>w lnth Sts (Suc i)"
     using deriv chain_lnth_rel[of "(\<leadsto>\<^sub>w)" Sts i] by auto
   then have "n_of_wstate (lnth Sts i) \<le> n_of_wstate (lnth Sts (i + 1))"
     using n_of_wstate_weighted_RP_increasing[of "lnth Sts i" "lnth Sts (i + 1)"] by auto
   ultimately show ?case
     by auto
 qed auto
 
 lemma infinite_chain_relation_measure:
   assumes
     measure_decreasing: "\<And>St St'. P St \<Longrightarrow> R St St' \<Longrightarrow> (m St', m St) \<in> mR" and
     non_infer_chain: "chain R (ldrop (enat k) Sts)" and
     inf: "llength Sts = \<infinity>" and
     P: "\<And>i. P (lnth (ldrop (enat k) Sts) i)"
   shows "chain (\<lambda>x y. (x, y) \<in> mR)\<inverse>\<inverse> (lmap m (ldrop (enat k) Sts))"
 proof (rule lnth_rel_chain)
   show "\<not> lnull (lmap m (ldrop (enat k) Sts))"
     using assms by auto
 next
   from inf have ldrop_inf: "llength (ldrop (enat k) Sts) = \<infinity> \<and> \<not> lfinite (ldrop (enat k) Sts)"
     using inf by (auto simp: llength_eq_infty_conv_lfinite)
   {
     fix j :: "nat"
     define St where "St = lnth (ldrop (enat k) Sts) j"
     define St' where "St' = lnth (ldrop (enat k) Sts) (j + 1)"
     have P': "P St \<and> P St'"
       unfolding St_def St'_def using P by auto
     from ldrop_inf have "R St St'"
       unfolding St_def St'_def
       using non_infer_chain infinite_chain_lnth_rel[of "ldrop (enat k) Sts" R j] by auto
     then have "(m St', m St) \<in> mR"
       using measure_decreasing P' by auto
     then have "(lnth (lmap m (ldrop (enat k) Sts)) (j + 1), lnth (lmap m (ldrop (enat k) Sts)) j)
       \<in> mR"
       unfolding St_def St'_def using lnth_lmap
       by (smt enat.distinct(1) enat_add_left_cancel enat_ord_simps(4) inf ldrop_lmap llength_lmap
           lnth_ldrop plus_enat_simps(3))
   }
   then show "\<forall>j. enat (j + 1) < llength (lmap m (ldrop (enat k) Sts)) \<longrightarrow>
     (\<lambda>x y. (x, y) \<in> mR)\<inverse>\<inverse> (lnth (lmap m (ldrop (enat k) Sts)) j)
       (lnth (lmap m (ldrop (enat k) Sts)) (j + 1))"
     by blast
 qed
 
 theorem weighted_RP_fair: "fair_state_seq (lmap state_of_wstate Sts)"
 proof (rule ccontr)
   assume asm: "\<not> fair_state_seq (lmap state_of_wstate Sts)"
   then have inff: "\<not> lfinite Sts" using fair_if_finite
     by auto
   then have inf: "llength Sts = \<infinity>"
     using llength_eq_infty_conv_lfinite by auto
   from asm obtain C where
     "C \<in> Liminf_llist (lmap N_of_state (lmap state_of_wstate Sts))
        \<union> Liminf_llist (lmap P_of_state (lmap state_of_wstate Sts))"
     unfolding fair_state_seq_def Liminf_state_def by auto
   then show False
   proof
     assume "C \<in> Liminf_llist (lmap N_of_state (lmap state_of_wstate Sts))"
     then obtain x where "enat x < llength Sts"
       "\<forall>xa. x \<le> xa \<and> enat xa < llength Sts \<longrightarrow> C \<in> N_of_state (state_of_wstate (lnth Sts xa))"
       unfolding Liminf_llist_def by auto
     then have "\<exists>k. \<forall>j. k \<le> j \<longrightarrow> (\<exists>i. (C, i) \<in># wN_of_wstate (lnth Sts j))"
       unfolding Liminf_llist_def by (force simp add: inf N_of_state_state_of_wstate_wN_of_wstate)
     then obtain k where k_p:
       "\<And>j. k \<le> j \<Longrightarrow> \<exists>i. (C, i) \<in># wN_of_wstate (lnth Sts j)"
       unfolding Liminf_llist_def
       by auto
     have chain_drop_Sts: "chain (\<leadsto>\<^sub>w) (ldrop k Sts)"
-      using deriv inf inff inf_chain_ldrop_chain by auto
+      using deriv inf inff by (simp add: inf_chain_ldropn_chain ldrop_enat)
     have in_N_j: "\<And>j. \<exists>i. (C, i) \<in># wN_of_wstate (lnth (ldrop k Sts) j)"
       using k_p by (simp add: add.commute inf)
     then have "chain (\<lambda>x y. (x, y) \<in> RP_filtered_relation)\<inverse>\<inverse> (lmap (RP_filtered_measure (\<lambda>Ci. True))
       (ldrop k Sts))"
       using inff inf weighted_RP_measure_decreasing_N chain_drop_Sts
         infinite_chain_relation_measure[of "\<lambda>St. \<exists>i. (C, i) \<in># wN_of_wstate St" "(\<leadsto>\<^sub>w)"] by blast
     then show False
       using wfP_iff_no_infinite_down_chain_llist[of "\<lambda>x y. (x, y) \<in> RP_filtered_relation"]
         wf_RP_filtered_relation inff
       by (metis (no_types, lifting) inf_llist_lnth ldrop_enat_inf_llist lfinite_inf_llist
         lfinite_lmap wfPUNIVI wf_induct_rule)
   next
     assume asm: "C \<in> Liminf_llist (lmap P_of_state (lmap state_of_wstate Sts))"
     from asm obtain i where i_p:
       "enat i < llength Sts"
       "\<And>j. i \<le> j \<and> enat j < llength Sts \<Longrightarrow> C \<in> P_of_state (state_of_wstate (lnth Sts j))"
       unfolding Liminf_llist_def by auto
     then obtain i where "(C, i) \<in> Liminf_llist (lmap (set_mset \<circ> wP_of_wstate) Sts)"
       using persistent_wclause_in_P_if_persistent_clause_in_P[of C] using asm inf by auto
     then have "\<exists>l. \<forall>k \<ge> l. (C, i) \<in> (set_mset \<circ> wP_of_wstate) (lnth Sts k)"
       unfolding Liminf_llist_def using inff inf by auto
     then obtain k where k_p:
       "(\<forall>k'\<ge>k. (C, i) \<in> (set_mset \<circ> wP_of_wstate) (lnth Sts k'))"
       by blast
     have Ci_in: "\<forall>k'. (C, i) \<in> (set_mset \<circ> wP_of_wstate) (lnth (ldrop k Sts) k')"
       using k_p lnth_ldrop[of k _ Sts] inf inff by force
     then have Ci_inn: "\<forall>k'. (C, i) \<in># (wP_of_wstate) (lnth (ldrop k Sts) k')"
       by auto
     have "chain (\<leadsto>\<^sub>w) (ldrop k Sts)"
-      using deriv inf_chain_ldrop_chain inf inff by auto
+      using deriv inf_chain_ldropn_chain inf inff by (simp add: inf_chain_ldropn_chain ldrop_enat)
     then have "chain (\<lambda>x y. (x, y) \<in> RP_combined_relation)\<inverse>\<inverse>
       (lmap (RP_combined_measure (weight (C, i))) (ldrop k Sts))"
       using inff inf Ci_in weighted_RP_measure_decreasing_P
         infinite_chain_relation_measure[of "\<lambda>St. (C, i) \<in># wP_of_wstate St" "(\<leadsto>\<^sub>w)"
           "RP_combined_measure (weight (C, i))" ]
       by auto
     then show False
       using wfP_iff_no_infinite_down_chain_llist[of "\<lambda>x y. (x, y) \<in> RP_combined_relation"]
         wf_RP_combined_relation inff
       by (smt inf_llist_lnth ldrop_enat_inf_llist lfinite_inf_llist lfinite_lmap wfPUNIVI
           wf_induct_rule)
   qed
 qed
 
 corollary weighted_RP_saturated: "src.saturated_upto (Liminf_llist (lmap grounding_of_wstate Sts))"
   using RP_saturated_if_fair[OF deriv_RP weighted_RP_fair empty_Q0_RP, unfolded llist.map_comp]
   by simp
 
 corollary weighted_RP_complete:
   "\<not> satisfiable (grounding_of_wstate (lhd Sts)) \<Longrightarrow> {#} \<in> Q_of_state (Liminf_wstate Sts)"
   using RP_complete_if_fair[OF deriv_RP weighted_RP_fair empty_Q0_RP, simplified lhd_lmap_Sts] .
 
 end
 
 end
 
 locale weighted_FO_resolution_prover_with_size_timestamp_factors =
   FO_resolution_prover S subst_atm id_subst comp_subst renamings_apart atm_of_atms mgu less_atm
   for
     S :: "('a :: wellorder) clause \<Rightarrow> 'a clause" and
     subst_atm :: "'a \<Rightarrow> 's \<Rightarrow> 'a" and
     id_subst :: "'s" and
     comp_subst :: "'s \<Rightarrow> 's \<Rightarrow> 's" and
     renamings_apart :: "'a literal multiset list \<Rightarrow> 's list" and
     atm_of_atms :: "'a list \<Rightarrow> 'a" and
     mgu :: "'a set set \<Rightarrow> 's option" and
     less_atm :: "'a \<Rightarrow> 'a \<Rightarrow> bool" +
   fixes
     size_atm :: "'a \<Rightarrow> nat" and
     size_factor :: nat and
     timestamp_factor :: nat
   assumes
     timestamp_factor_pos: "timestamp_factor > 0"
 begin
 
 fun weight :: "'a wclause \<Rightarrow> nat" where
   "weight (C, i) = size_factor * size_multiset (size_literal size_atm) C + timestamp_factor * i"
 
 lemma weight_mono: "i < j \<Longrightarrow> weight (C, i) < weight (C, j)"
   using timestamp_factor_pos by simp
 
 declare weight.simps [simp del]
 
 sublocale wrp: weighted_FO_resolution_prover _ _ _ _ _ _ _ _ weight
   by unfold_locales (rule weight_mono)
 
 notation wrp.weighted_RP (infix "\<leadsto>\<^sub>w" 50)
 
 end
 
 end
diff --git a/thys/Nested_Multisets_Ordinals/Multiset_More.thy b/thys/Nested_Multisets_Ordinals/Multiset_More.thy
--- a/thys/Nested_Multisets_Ordinals/Multiset_More.thy
+++ b/thys/Nested_Multisets_Ordinals/Multiset_More.thy
@@ -1,993 +1,1027 @@
 (*  Title:       More about Multisets
     Author:      Mathias Fleury <mathias.fleury at mpi-inf.mpg.de>, 2015
     Author:      Jasmin Blanchette <blanchette at in.tum.de>, 2014, 2015
     Author:      Anders Schlichtkrull <andschl at dtu.dk>, 2017
     Author:      Dmitriy Traytel <traytel at in.tum.de>, 2014
     Maintainer:  Mathias Fleury <mathias.fleury at mpi-inf.mpg.de>
 *)
 
 section \<open>More about Multisets\<close>
 
 theory Multiset_More
-imports "HOL-Library.Multiset_Order"
+  imports
+    "HOL-Library.Multiset_Order"
+    "HOL-Library.Sublist"
 begin
 
 text \<open>
 Isabelle's theory of finite multisets is not as developed as other areas, such as lists and sets.
 The present theory introduces some missing concepts and lemmas. Some of it is expected to move to
 Isabelle's library.
 \<close>
 
 
 subsection \<open>Basic Setup\<close>
 
 declare
   diff_single_trivial [simp]
   in_image_mset [iff]
   image_mset.compositionality [simp]
 
   (*To have the same rules as the set counter-part*)
   mset_subset_eqD[dest, intro?] (*@{thm subsetD}*)
 
   Multiset.in_multiset_in_set[simp]
   inter_add_left1[simp]
   inter_add_left2[simp]
   inter_add_right1[simp]
   inter_add_right2[simp]
 
   sum_mset_sum_list[simp]
 
 
 subsection \<open>Lemmas about Intersection, Union and Pointwise Inclusion\<close>
 
+lemma subset_mset_imp_subset_add_mset: "A \<subseteq># B \<Longrightarrow> A \<subseteq># add_mset x B"
+  by (metis add_mset_diff_bothsides diff_subset_eq_self multiset_inter_def subset_mset.inf.absorb2)
+
 lemma subset_add_mset_notin_subset_mset: \<open>A \<subseteq># add_mset b B \<Longrightarrow> b \<notin># A \<Longrightarrow> A \<subseteq># B\<close>
   by (simp add: subset_mset.le_iff_sup)
 
 lemma subset_msetE: "\<lbrakk>A \<subset># B; \<lbrakk>A \<subseteq># B; \<not> B \<subseteq># A\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
   by (simp add: subset_mset.less_le_not_le)
 
 lemma Diff_triv_mset: "M \<inter># N = {#} \<Longrightarrow> M - N = M"
   by (metis diff_intersect_left_idem diff_zero)
 
 lemma diff_intersect_sym_diff: "(A - B) \<inter># (B - A) = {#}"
   unfolding multiset_inter_def
 proof -
   have "A - (B - (B - A)) = A - B"
     by (metis diff_intersect_right_idem multiset_inter_def)
   then show "A - B - (A - B - (B - A)) = {#}"
     by (metis diff_add diff_cancel diff_subset_eq_self subset_mset.diff_add)
 qed
 
 declare subset_msetE [elim!]
 
+lemma subseq_mset_subseteq_mset: "subseq xs ys \<Longrightarrow> mset xs \<subseteq># mset ys"
+proof (induct xs arbitrary: ys)
+  case (Cons x xs)
+  note Outer_Cons = this
+  then show ?case
+  proof (induct ys)
+    case (Cons y ys)
+    have "subseq xs ys"
+      by (metis Cons.prems(2) subseq_Cons' subseq_Cons2_iff)
+    then show ?case
+      using Cons by (metis mset.simps(2) mset_subset_eq_add_mset_cancel subseq_Cons2_iff
+          subset_mset_imp_subset_add_mset)
+  qed simp
+qed simp
+
 
 subsection \<open>Lemmas about Filter and Image\<close>
 
 lemma count_image_mset_ge_count: "count (image_mset f A) (f b) \<ge> count A b"
   by (induction A) auto
 
 lemma count_image_mset_inj:
   assumes \<open>inj f\<close>
   shows \<open>count (image_mset f M) (f x) = count M x\<close>
   by (induct M) (use assms in \<open>auto simp: inj_on_def\<close>)
 
 lemma count_image_mset_le_count_inj_on:
   "inj_on f (set_mset M) \<Longrightarrow> count (image_mset f M) y \<le> count M (inv_into (set_mset M) f y)"
 proof (induct M)
   case (add x M)
   note ih = this(1) and inj_xM = this(2)
 
   have inj_M: "inj_on f (set_mset M)"
     using inj_xM by simp
 
   show ?case
   proof (cases "x \<in># M")
     case x_in_M: True
     show ?thesis
     proof (cases "y = f x")
       case y_eq_fx: True
       show ?thesis
         using x_in_M ih[OF inj_M] unfolding y_eq_fx by (simp add: inj_M insert_absorb)
     next
       case y_ne_fx: False
       show ?thesis
         using x_in_M ih[OF inj_M] y_ne_fx insert_absorb by fastforce
     qed
   next
     case x_ni_M: False
     show ?thesis
     proof (cases "y = f x")
       case y_eq_fx: True
       have "f x \<notin># image_mset f M"
         using x_ni_M inj_xM by force
       thus ?thesis
         unfolding y_eq_fx
         by (metis (no_types) inj_xM count_add_mset count_greater_eq_Suc_zero_iff count_inI
           image_mset_add_mset inv_into_f_f union_single_eq_member)
     next
       case y_ne_fx: False
       show ?thesis
       proof (rule ccontr)
         assume neg_conj: "\<not> count (image_mset f (add_mset x M)) y
           \<le> count (add_mset x M) (inv_into (set_mset (add_mset x M)) f y)"
 
         have cnt_y: "count (add_mset (f x) (image_mset f M)) y = count (image_mset f M) y"
           using y_ne_fx by simp
 
         have "inv_into (set_mset M) f y \<in># add_mset x M \<Longrightarrow>
           inv_into (set_mset (add_mset x M)) f (f (inv_into (set_mset M) f y)) =
           inv_into (set_mset M) f y"
           by (meson inj_xM inv_into_f_f)
         hence "0 < count (image_mset f (add_mset x M)) y \<Longrightarrow>
           count M (inv_into (set_mset M) f y) = 0 \<or> x = inv_into (set_mset M) f y"
           using neg_conj cnt_y ih[OF inj_M]
           by (metis (no_types) count_add_mset count_greater_zero_iff count_inI f_inv_into_f
             image_mset_add_mset set_image_mset)
         thus False
           using neg_conj cnt_y x_ni_M ih[OF inj_M]
           by (metis (no_types) count_greater_zero_iff count_inI eq_iff image_mset_add_mset
             less_imp_le)
       qed
     qed
   qed
 qed simp
 
 lemma mset_filter_compl: "mset (filter p xs) + mset (filter (Not \<circ> p) xs) = mset xs"
-  by (induction xs) (auto simp: mset_filter ac_simps)
+  by (induction xs) (auto simp: ac_simps)
 
 text \<open>Near duplicate of @{thm [source] filter_eq_replicate_mset}: @{thm filter_eq_replicate_mset}.\<close>
 
 lemma filter_mset_eq: "filter_mset ((=) L) A = replicate_mset (count A L) L"
   by (auto simp: multiset_eq_iff)
 
 lemma filter_mset_cong[fundef_cong]:
   assumes "M = M'" "\<And>a. a \<in># M \<Longrightarrow> P a = Q a"
   shows "filter_mset P M = filter_mset Q M"
 proof -
   have "M - filter_mset Q M = filter_mset (\<lambda>a. \<not>Q a) M"
     by (metis multiset_partition add_diff_cancel_left')
   then show ?thesis
     by (auto simp: filter_mset_eq_conv assms)
 qed
 
 lemma image_mset_filter_swap: "image_mset f {# x \<in># M. P (f x)#} = {# x \<in># image_mset f M. P x#}"
   by (induction M) auto
 
 lemma image_mset_cong2:
   "(\<And>x. x \<in># M \<Longrightarrow> f x = g x) \<Longrightarrow> M = N \<Longrightarrow> image_mset f M = image_mset g N"
   by (hypsubst, rule image_mset_cong)
 
 lemma filter_mset_empty_conv: \<open>(filter_mset P M = {#}) = (\<forall>L\<in>#M. \<not> P L)\<close>
   by (induction M) auto
 
 lemma multiset_filter_mono2: \<open>filter_mset P A \<subseteq># filter_mset Q A \<longleftrightarrow> (\<forall>a\<in>#A. P a \<longrightarrow> Q a)\<close>
   by (induction A) (auto intro: subset_mset.order.trans)
 
 lemma image_filter_cong:
   assumes \<open>\<And>C. C \<in># M \<Longrightarrow> P C \<Longrightarrow> f C = g C\<close>
   shows \<open>{#f C. C \<in># {#C \<in># M. P C#}#} = {#g C | C\<in># M. P C#}\<close>
   using assms by (induction M) auto
 
 lemma image_mset_filter_swap2: \<open>{#C \<in># {#P x. x \<in># D#}. Q C #} = {#P x. x \<in># {#C| C \<in># D. Q (P C)#}#}\<close>
   by (simp add: image_mset_filter_swap)
 
 declare image_mset_cong2 [cong]
 
+lemma filter_mset_empty_if_finite_and_filter_set_empty:
+  assumes
+    "{x \<in> X. P x} = {}" and
+    "finite X"
+  shows "{#x \<in># mset_set X. P x#} = {#}"
+proof -
+  have empty_empty: "\<And>Y. set_mset Y = {} \<Longrightarrow> Y = {#}"
+    by auto
+  from assms have "set_mset {#x \<in># mset_set X. P x#} = {}"
+    by auto
+  then show ?thesis
+    by (rule empty_empty)
+qed
+
 
 subsection \<open>Lemmas about Sum\<close>
 
 lemma sum_image_mset_sum_map[simp]: "sum_mset (image_mset f (mset xs)) = sum_list (map f xs)"
   by (metis mset_map sum_mset_sum_list)
 
 lemma sum_image_mset_mono:
   fixes f :: "'a \<Rightarrow> 'b::canonically_ordered_monoid_add"
   assumes sub: "A \<subseteq># B"
   shows "(\<Sum>m \<in># A. f m) \<le> (\<Sum>m \<in># B. f m)"
   by (metis image_mset_union le_iff_add sub subset_mset.add_diff_inverse sum_mset.union)
 
 lemma sum_image_mset_mono_mem:
   "n \<in># M \<Longrightarrow> f n \<le> (\<Sum>m \<in># M. f m)" for f :: "'a \<Rightarrow> 'b::canonically_ordered_monoid_add"
   using le_iff_add multi_member_split by fastforce
 
 lemma count_sum_mset_if_1_0: \<open>count M a = (\<Sum>x\<in>#M. if x = a then 1 else 0)\<close>
   by (induction M) auto
 
 lemma sum_mset_dvd:
   fixes k :: "'a::comm_semiring_1_cancel"
   assumes "\<forall>m \<in># M. k dvd f m"
   shows "k dvd (\<Sum>m \<in># M. f m)"
   using assms by (induct M) auto
 
 lemma sum_mset_distrib_div_if_dvd:
   fixes k :: "'a::unique_euclidean_semiring"
   assumes "\<forall>m \<in># M. k dvd f m"
   shows "(\<Sum>m \<in># M. f m) div k = (\<Sum>m \<in># M. f m div k)"
   using assms by (induct M) (auto simp: div_plus_div_distrib_dvd_left)
 
 
 subsection \<open>Lemmas about Remove\<close>
 
 lemma set_mset_minus_replicate_mset[simp]:
   "n \<ge> count A a \<Longrightarrow> set_mset (A - replicate_mset n a) = set_mset A - {a}"
   "n < count A a \<Longrightarrow> set_mset (A - replicate_mset n a) = set_mset A"
   unfolding set_mset_def by (auto split: if_split simp: not_in_iff)
 
 abbreviation removeAll_mset :: "'a \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" where
   "removeAll_mset C M \<equiv> M - replicate_mset (count M C) C"
 
 lemma mset_removeAll[simp, code]: "removeAll_mset C (mset L) = mset (removeAll C L)"
   by (induction L) (auto simp: ac_simps multiset_eq_iff split: if_split_asm)
 
 lemma removeAll_mset_filter_mset: "removeAll_mset C M = filter_mset ((\<noteq>) C) M"
   by (induction M) (auto simp: ac_simps multiset_eq_iff)
 
 abbreviation remove1_mset :: "'a \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" where
   "remove1_mset C M \<equiv> M - {#C#}"
 
 lemma removeAll_subseteq_remove1_mset: "removeAll_mset x M \<subseteq># remove1_mset x M"
   by (auto simp: subseteq_mset_def)
 
 lemma in_remove1_mset_neq:
   assumes ab: "a \<noteq> b"
   shows "a \<in># remove1_mset b C \<longleftrightarrow> a \<in># C"
   by (metis assms diff_single_trivial in_diffD insert_DiffM insert_noteq_member)
 
 lemma size_mset_removeAll_mset_le_iff: "size (removeAll_mset x M) < size M \<longleftrightarrow> x \<in># M"
   by (auto intro: count_inI mset_subset_size simp: subset_mset_def multiset_eq_iff)
 
 lemma size_remove1_mset_If: \<open>size (remove1_mset x M) = size M - (if x \<in># M then 1 else 0)\<close>
   by (auto simp: size_Diff_subset_Int)
 
 lemma size_mset_remove1_mset_le_iff: "size (remove1_mset x M) < size M \<longleftrightarrow> x \<in># M"
   using less_irrefl
   by (fastforce intro!: mset_subset_size elim: in_countE simp: subset_mset_def multiset_eq_iff)
 
 lemma remove_1_mset_id_iff_notin: "remove1_mset a M = M \<longleftrightarrow> a \<notin># M"
   by (meson diff_single_trivial multi_drop_mem_not_eq)
 
 lemma id_remove_1_mset_iff_notin: "M = remove1_mset a M \<longleftrightarrow> a \<notin># M"
   using remove_1_mset_id_iff_notin by metis
 
 lemma remove1_mset_eqE:
   "remove1_mset L x1 = M \<Longrightarrow>
     (L \<in># x1 \<Longrightarrow> x1 = M + {#L#} \<Longrightarrow> P) \<Longrightarrow>
     (L \<notin># x1 \<Longrightarrow> x1 = M \<Longrightarrow> P) \<Longrightarrow>
   P"
   by (cases "L \<in># x1") auto
 
 lemma image_filter_ne_mset[simp]:
   "image_mset f {#x \<in># M. f x \<noteq> y#} = removeAll_mset y (image_mset f M)"
   by (induction M) simp_all
 
 lemma image_mset_remove1_mset_if:
   "image_mset f (remove1_mset a M) =
    (if a \<in># M then remove1_mset (f a) (image_mset f M) else image_mset f M)"
   by (auto simp: image_mset_Diff)
 
 lemma filter_mset_neq: "{#x \<in># M. x \<noteq> y#} = removeAll_mset y M"
   by (metis add_diff_cancel_left' filter_eq_replicate_mset multiset_partition)
 
 lemma filter_mset_neq_cond: "{#x \<in># M. P x \<and> x \<noteq> y#} = removeAll_mset y {# x\<in>#M. P x#}"
   by (metis filter_filter_mset filter_mset_neq)
 
 lemma remove1_mset_add_mset_If:
   "remove1_mset L (add_mset L' C) = (if L = L' then C else remove1_mset L C + {#L'#})"
   by (auto simp: multiset_eq_iff)
 
 lemma minus_remove1_mset_if:
   "A - remove1_mset b B = (if b \<in># B \<and> b \<in># A \<and> count A b \<ge> count B b then {#b#} + (A - B) else A - B)"
   by (auto simp: multiset_eq_iff count_greater_zero_iff[symmetric]
     simp del: count_greater_zero_iff)
 
 lemma add_mset_eq_add_mset_ne:
   "a \<noteq> b \<Longrightarrow> add_mset a A = add_mset b B \<longleftrightarrow> a \<in># B \<and> b \<in># A \<and> A = add_mset b (B - {#a#})"
   by (metis (no_types, lifting) diff_single_eq_union diff_union_swap multi_self_add_other_not_self
     remove_1_mset_id_iff_notin union_single_eq_diff)
 
 lemma add_mset_eq_add_mset: \<open>add_mset a M = add_mset b M' \<longleftrightarrow>
   (a = b \<and> M = M') \<or> (a \<noteq> b \<and> b \<in># M \<and> add_mset a (M - {#b#}) = M')\<close>
   by (metis add_mset_eq_add_mset_ne add_mset_remove_trivial union_single_eq_member)
 
 (* TODO move to Multiset: could replace add_mset_remove_trivial_eq? *)
 lemma add_mset_remove_trivial_iff: \<open>N = add_mset a (N - {#b#}) \<longleftrightarrow> a \<in># N \<and> a = b\<close>
   by (metis add_left_cancel add_mset_remove_trivial insert_DiffM2 single_eq_single
       size_mset_remove1_mset_le_iff union_single_eq_member)
 
 lemma trivial_add_mset_remove_iff: \<open>add_mset a (N - {#b#}) = N \<longleftrightarrow> a \<in># N \<and> a = b\<close>
   by (subst eq_commute) (fact add_mset_remove_trivial_iff)
 
 lemma remove1_single_empty_iff[simp]: \<open>remove1_mset L {#L'#} = {#} \<longleftrightarrow> L = L'\<close>
   using add_mset_remove_trivial_iff by fastforce
 
 lemma add_mset_less_imp_less_remove1_mset:
   assumes xM_lt_N: "add_mset x M < N"
   shows "M < remove1_mset x N"
 proof -
   have "M < N"
     using assms le_multiset_right_total mset_le_trans by blast
   then show ?thesis
     by (metis add_less_cancel_right add_mset_add_single diff_single_trivial insert_DiffM2 xM_lt_N)
 qed
 
 
 subsection \<open>Lemmas about Replicate\<close>
 
 lemma replicate_mset_minus_replicate_mset_same[simp]:
   "replicate_mset m x - replicate_mset n x = replicate_mset (m - n) x"
   by (induct m arbitrary: n, simp, metis left_diff_repeat_mset_distrib' repeat_mset_replicate_mset)
 
 lemma replicate_mset_subset_iff_lt[simp]: "replicate_mset m x \<subset># replicate_mset n x \<longleftrightarrow> m < n"
   by (induct n m rule: diff_induct) (auto intro: subset_mset.gr_zeroI)
 
 lemma replicate_mset_subseteq_iff_le[simp]: "replicate_mset m x \<subseteq># replicate_mset n x \<longleftrightarrow> m \<le> n"
   by (induct n m rule: diff_induct) auto
 
 lemma replicate_mset_lt_iff_lt[simp]: "replicate_mset m x < replicate_mset n x \<longleftrightarrow> m < n"
   by (induct n m rule: diff_induct) (auto intro: subset_mset.gr_zeroI gr_zeroI)
 
 lemma replicate_mset_le_iff_le[simp]: "replicate_mset m x \<le> replicate_mset n x \<longleftrightarrow> m \<le> n"
   by (induct n m rule: diff_induct) auto
 
 lemma replicate_mset_eq_iff[simp]:
   "replicate_mset m x = replicate_mset n y \<longleftrightarrow> m = n \<and> (m \<noteq> 0 \<longrightarrow> x = y)"
   by (cases m; cases n; simp)
     (metis in_replicate_mset insert_noteq_member size_replicate_mset union_single_eq_diff)
 
 lemma replicate_mset_plus: "replicate_mset (a + b) C = replicate_mset a C + replicate_mset b C"
   by (induct a) (auto simp: ac_simps)
 
 lemma mset_replicate_replicate_mset: "mset (replicate n L) = replicate_mset n L"
   by (induction n) auto
 
 lemma set_mset_single_iff_replicate_mset: "set_mset U = {a} \<longleftrightarrow> (\<exists>n > 0. U = replicate_mset n a)"
   by (rule, metis count_greater_zero_iff count_replicate_mset insertI1 multi_count_eq singletonD
     zero_less_iff_neq_zero, force)
 
 lemma ex_replicate_mset_if_all_elems_eq:
   assumes "\<forall>x \<in># M. x = y"
   shows "\<exists>n. M = replicate_mset n y"
   using assms by (metis count_replicate_mset mem_Collect_eq multiset_eqI neq0_conv set_mset_def)
 
 
 subsection \<open>Multiset and Set Conversions\<close>
 
 lemma count_mset_set_if: "count (mset_set A) a = (if a \<in> A \<and> finite A then 1 else 0)"
   by auto
 
 lemma mset_set_set_mset_empty_mempty[iff]: "mset_set (set_mset D) = {#} \<longleftrightarrow> D = {#}"
   by (simp add: mset_set_empty_iff)
 
 lemma count_mset_set_le_one: "count (mset_set A) x \<le> 1"
   by (simp add: count_mset_set_if)
 
 lemma mset_set_set_mset_subseteq[simp]: "mset_set (set_mset A) \<subseteq># A"
   by (simp add: mset_set_set_mset_msubset)
 
 lemma mset_sorted_list_of_set[simp]: "mset (sorted_list_of_set A) = mset_set A"
   by (metis mset_sorted_list_of_multiset sorted_list_of_mset_set)
 
 lemma sorted_sorted_list_of_multiset[simp]:
   "sorted (sorted_list_of_multiset (M :: 'a::linorder multiset))"
   by (metis mset_sorted_list_of_multiset sorted_list_of_multiset_mset sorted_sort)
 
 lemma mset_take_subseteq: "mset (take n xs) \<subseteq># mset xs"
   apply (induct xs arbitrary: n)
    apply simp
   by (case_tac n) simp_all
 
 lemma sorted_list_of_multiset_eq_Nil[simp]: "sorted_list_of_multiset M = [] \<longleftrightarrow> M = {#}"
   by (metis mset_sorted_list_of_multiset sorted_list_of_multiset_empty)
 
 
 subsection \<open>Duplicate Removal\<close>
 
 (* TODO: use abbreviation? *)
 definition remdups_mset :: "'v multiset \<Rightarrow> 'v multiset" where
   "remdups_mset S = mset_set (set_mset S)"
 
 lemma set_mset_remdups_mset[simp]: \<open>set_mset (remdups_mset A) = set_mset A\<close>
   unfolding remdups_mset_def by auto
 
 lemma count_remdups_mset_eq_1: "a \<in># remdups_mset A \<longleftrightarrow> count (remdups_mset A) a = 1"
   unfolding remdups_mset_def by (auto simp: count_eq_zero_iff intro: count_inI)
 
 lemma remdups_mset_empty[simp]: "remdups_mset {#} = {#}"
   unfolding remdups_mset_def by auto
 
 lemma remdups_mset_singleton[simp]: "remdups_mset {#a#} = {#a#}"
   unfolding remdups_mset_def by auto
 
 lemma remdups_mset_eq_empty[iff]: "remdups_mset D = {#} \<longleftrightarrow> D = {#}"
   unfolding remdups_mset_def by blast
 
 lemma remdups_mset_singleton_sum[simp]:
   "remdups_mset (add_mset a A) = (if a \<in># A then remdups_mset A else add_mset a (remdups_mset A))"
   unfolding remdups_mset_def by (simp_all add: insert_absorb)
 
 lemma mset_remdups_remdups_mset[simp]: "mset (remdups D) = remdups_mset (mset D)"
   by (induction D) (auto simp add: ac_simps)
 
 declare mset_remdups_remdups_mset[symmetric, code]
 
 definition distinct_mset :: "'a multiset \<Rightarrow> bool" where
   "distinct_mset S \<longleftrightarrow> (\<forall>a. a \<in># S \<longrightarrow> count S a = 1)"
 
 lemma distinct_mset_count_less_1: "distinct_mset S \<longleftrightarrow> (\<forall>a. count S a \<le> 1)"
   using eq_iff nat_le_linear unfolding distinct_mset_def by fastforce
 
 lemma distinct_mset_empty[simp]: "distinct_mset {#}"
   unfolding distinct_mset_def by auto
 
 lemma distinct_mset_singleton: "distinct_mset {#a#}"
   unfolding distinct_mset_def by auto
 
 lemma distinct_mset_union:
   assumes dist: "distinct_mset (A + B)"
   shows "distinct_mset A"
   unfolding distinct_mset_count_less_1
 proof (rule allI)
   fix a
   have \<open>count A a \<le> count (A + B) a\<close> by auto
   moreover have \<open>count (A + B) a \<le> 1\<close>
     using dist unfolding distinct_mset_count_less_1 by auto
   ultimately show \<open>count A a \<le> 1\<close>
     by simp
 qed
 
 lemma distinct_mset_minus[simp]: "distinct_mset A \<Longrightarrow> distinct_mset (A - B)"
   by (metis diff_subset_eq_self mset_subset_eq_exists_conv distinct_mset_union)
 
 lemma count_remdups_mset_If: \<open>count (remdups_mset A) a = (if a \<in># A then 1 else 0)\<close>
   unfolding remdups_mset_def by auto
 
 lemma distinct_mset_rempdups_union_mset:
   assumes "distinct_mset A" and "distinct_mset B"
   shows "A \<union># B = remdups_mset (A + B)"
   using assms nat_le_linear unfolding remdups_mset_def
   by (force simp add: multiset_eq_iff max_def count_mset_set_if distinct_mset_def not_in_iff)
 
 lemma distinct_mset_add_mset[simp]: "distinct_mset (add_mset a L) \<longleftrightarrow> a \<notin># L \<and> distinct_mset L"
   unfolding distinct_mset_def
   apply (rule iffI)
    apply (auto split: if_split_asm; fail)[]
   by (auto simp: not_in_iff; fail)
 
 lemma distinct_mset_size_eq_card: "distinct_mset C \<Longrightarrow> size C = card (set_mset C)"
   by (induction C) auto
 
 lemma distinct_mset_add:
   "distinct_mset (L + L') \<longleftrightarrow> distinct_mset L \<and> distinct_mset L' \<and> L \<inter># L' = {#}"
   by (induction L arbitrary: L') auto
 
 lemma distinct_mset_set_mset_ident[simp]: "distinct_mset M \<Longrightarrow> mset_set (set_mset M) = M"
   by (induction M) auto
 
 lemma distinct_finite_set_mset_subseteq_iff[iff]:
   assumes "distinct_mset M" "finite N"
   shows "set_mset M \<subseteq> N \<longleftrightarrow> M \<subseteq># mset_set N"
   by (metis assms distinct_mset_set_mset_ident finite_set_mset msubset_mset_set_iff)
 
 lemma distinct_mem_diff_mset:
   assumes dist: "distinct_mset M" and mem: "x \<in> set_mset (M - N)"
   shows "x \<notin> set_mset N"
 proof -
   have "count M x = 1"
     using dist mem by (meson distinct_mset_def in_diffD)
   then show ?thesis
     using mem by (metis count_greater_eq_one_iff in_diff_count not_less)
 qed
 
 lemma distinct_set_mset_eq:
   assumes "distinct_mset M" "distinct_mset N" "set_mset M = set_mset N"
   shows "M = N"
   using assms distinct_mset_set_mset_ident by fastforce
 
 lemma distinct_mset_union_mset[simp]:
   \<open>distinct_mset (D \<union># C) \<longleftrightarrow> distinct_mset D \<and> distinct_mset C\<close>
   unfolding distinct_mset_count_less_1 by force
 
 lemma distinct_mset_inter_mset:
   "distinct_mset C \<Longrightarrow> distinct_mset (C \<inter># D)"
   "distinct_mset D \<Longrightarrow> distinct_mset (C \<inter># D)"
   by (simp_all add: multiset_inter_def,
     metis distinct_mset_minus multiset_inter_commute multiset_inter_def)
 
 lemma distinct_mset_remove1_All: "distinct_mset C \<Longrightarrow> remove1_mset L C = removeAll_mset L C"
   by (auto simp: multiset_eq_iff distinct_mset_count_less_1)
 
 lemma distinct_mset_size_2: "distinct_mset {#a, b#} \<longleftrightarrow> a \<noteq> b"
   by auto
 
 lemma distinct_mset_filter: "distinct_mset M \<Longrightarrow> distinct_mset {# L \<in># M. P L#}"
   by (simp add: distinct_mset_def)
 
 lemma distinct_mset_mset_distinct[simp]: \<open>distinct_mset (mset xs) = distinct xs\<close>
   by (induction xs) auto
 
 lemma distinct_image_mset_inj:
   \<open>inj_on f (set_mset M) \<Longrightarrow> distinct_mset (image_mset f M) \<longleftrightarrow> distinct_mset M\<close>
   by (induction M) (auto simp: inj_on_def)
 
 
 subsection \<open>Repeat Operation\<close>
 
 lemma repeat_mset_compower: "repeat_mset n A = (((+) A) ^^ n) {#}"
   by (induction n) auto
 
 lemma repeat_mset_prod: "repeat_mset (m * n) A = (((+) (repeat_mset n A)) ^^ m) {#}"
   by (induction m) (auto simp: repeat_mset_distrib)
 
 
 subsection \<open>Cartesian Product\<close>
 
 text \<open>Definition of the cartesian products over multisets. The construction mimics of the cartesian
   product on sets and use the same theorem names (adding only the suffix \<open>_mset\<close> to Sigma
   and Times). See file @{file \<open>~~/src/HOL/Product_Type.thy\<close>}\<close>
 
 definition Sigma_mset :: "'a multiset \<Rightarrow> ('a \<Rightarrow> 'b multiset) \<Rightarrow> ('a \<times> 'b) multiset" where
   "Sigma_mset A B \<equiv> \<Union># {#{#(a, b). b \<in># B a#}. a \<in># A #}"
 
 abbreviation Times_mset :: "'a multiset \<Rightarrow> 'b multiset \<Rightarrow> ('a \<times> 'b) multiset" (infixr "\<times>#" 80) where
   "Times_mset A B \<equiv> Sigma_mset A (\<lambda>_. B)"
 
 hide_const (open) Times_mset
 
 text \<open>Contrary to the set version @{term \<open>SIGMA x:A. B\<close>}, we use the non-ASCII symbol \<open>\<in>#\<close>.\<close>
 
 syntax
   "_Sigma_mset" :: "[pttrn, 'a multiset, 'b multiset] => ('a * 'b) multiset"
   ("(3SIGMAMSET _\<in>#_./ _)" [0, 0, 10] 10)
 translations
   "SIGMAMSET x\<in>#A. B" == "CONST Sigma_mset A (\<lambda>x. B)"
 
 text \<open>Link between the multiset and the set cartesian product:\<close>
 
 lemma Times_mset_Times: "set_mset (A \<times># B) = set_mset A \<times> set_mset B"
   unfolding Sigma_mset_def by auto
 
 lemma Sigma_msetI [intro!]: "\<lbrakk>a \<in># A; b \<in># B a\<rbrakk> \<Longrightarrow> (a, b) \<in># Sigma_mset A B"
   by (unfold Sigma_mset_def) auto
 
 lemma Sigma_msetE[elim!]: "\<lbrakk>c \<in># Sigma_mset A B; \<And>x y. \<lbrakk>x \<in># A; y \<in># B x; c = (x, y)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
   by (unfold Sigma_mset_def) auto
 
 text \<open>Elimination of @{term "(a, b) \<in># A \<times># B"} -- introduces no eigenvariables.\<close>
 
 lemma Sigma_msetD1: "(a, b) \<in># Sigma_mset A B \<Longrightarrow> a \<in># A"
   by blast
 
 lemma Sigma_msetD2: "(a, b) \<in># Sigma_mset A B \<Longrightarrow> b \<in># B a"
   by blast
 
 lemma Sigma_msetE2: "\<lbrakk>(a, b) \<in># Sigma_mset A B; \<lbrakk>a \<in># A; b \<in># B a\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
   by blast
 
 lemma Sigma_mset_cong:
   "\<lbrakk>A = B; \<And>x. x \<in># B \<Longrightarrow> C x = D x\<rbrakk> \<Longrightarrow> (SIGMAMSET x \<in># A. C x) = (SIGMAMSET x \<in># B. D x)"
   by (metis (mono_tags, lifting) Sigma_mset_def image_mset_cong)
 
 lemma count_sum_mset: "count (\<Union># M) b = (\<Sum>P \<in># M. count P b)"
   by (induction M) auto
 
 lemma Sigma_mset_plus_distrib1[simp]: "Sigma_mset (A + B) C = Sigma_mset A C + Sigma_mset B C"
   unfolding Sigma_mset_def by auto
 
 lemma Sigma_mset_plus_distrib2[simp]:
   "Sigma_mset A (\<lambda>i. B i + C i) = Sigma_mset A B + Sigma_mset A C"
   unfolding Sigma_mset_def by (induction A) (auto simp: multiset_eq_iff)
 
 lemma Times_mset_single_left: "{#a#} \<times># B = image_mset (Pair a) B"
   unfolding Sigma_mset_def by auto
 
 lemma Times_mset_single_right: "A \<times># {#b#} = image_mset (\<lambda>a. Pair a b) A"
   unfolding Sigma_mset_def by (induction A) auto
 
 lemma Times_mset_single_single[simp]: "{#a#} \<times># {#b#} = {#(a, b)#}"
   unfolding Sigma_mset_def by simp
 
 lemma count_image_mset_Pair:
   "count (image_mset (Pair a) B) (x, b) = (if x = a then count B b else 0)"
   by (induction B) auto
 
 lemma count_Sigma_mset: "count (Sigma_mset A B) (a, b) = count A a * count (B a) b"
   by (induction A) (auto simp: Sigma_mset_def count_image_mset_Pair)
 
 lemma Sigma_mset_empty1[simp]: "Sigma_mset {#} B = {#}"
   unfolding Sigma_mset_def by auto
 
 lemma Sigma_mset_empty2[simp]: "A \<times># {#} = {#}"
   by (auto simp: multiset_eq_iff count_Sigma_mset)
 
 lemma Sigma_mset_mono:
   assumes "A \<subseteq># C" and "\<And>x. x \<in># A \<Longrightarrow> B x \<subseteq># D x"
   shows "Sigma_mset A B \<subseteq># Sigma_mset C D"
 proof -
   have "count A a * count (B a) b \<le> count C a * count (D a) b" for a b
     using assms unfolding subseteq_mset_def by (metis count_inI eq_iff mult_eq_0_iff mult_le_mono)
   then show ?thesis
     by (auto simp: subseteq_mset_def count_Sigma_mset)
 qed
 
 lemma mem_Sigma_mset_iff[iff]: "((a,b) \<in># Sigma_mset A B) = (a \<in># A \<and> b \<in># B a)"
   by blast
 
 lemma mem_Times_mset_iff: "x \<in># A \<times># B \<longleftrightarrow> fst x \<in># A \<and> snd x \<in># B"
   by (induct x) simp
 
 lemma Sigma_mset_empty_iff: "(SIGMAMSET i\<in>#I. X i) = {#} \<longleftrightarrow> (\<forall>i\<in>#I. X i = {#})"
   by (auto simp: Sigma_mset_def)
 
 lemma Times_mset_subset_mset_cancel1: "x \<in># A \<Longrightarrow> (A \<times># B \<subseteq># A \<times># C) = (B \<subseteq># C)"
   by (auto simp: subseteq_mset_def count_Sigma_mset)
 
 lemma Times_mset_subset_mset_cancel2: "x \<in># C \<Longrightarrow> (A \<times># C \<subseteq># B \<times># C) = (A \<subseteq># B)"
   by (auto simp: subseteq_mset_def count_Sigma_mset)
 
 lemma Times_mset_eq_cancel2: "x \<in># C \<Longrightarrow> (A \<times># C = B \<times># C) = (A = B)"
   by (auto simp: multiset_eq_iff count_Sigma_mset dest!: in_countE)
 
 lemma split_paired_Ball_mset_Sigma_mset[simp]:
   "(\<forall>z\<in>#Sigma_mset A B. P z) \<longleftrightarrow> (\<forall>x\<in>#A. \<forall>y\<in>#B x. P (x, y))"
   by blast
 
 lemma split_paired_Bex_mset_Sigma_mset[simp]:
   "(\<exists>z\<in>#Sigma_mset A B. P z) \<longleftrightarrow> (\<exists>x\<in>#A. \<exists>y\<in>#B x. P (x, y))"
   by blast
 
 lemma sum_mset_if_eq_constant:
   "(\<Sum>x\<in>#M. if a = x then (f x) else 0) = (((+) (f a)) ^^ (count M a)) 0"
   by (induction M) (auto simp: ac_simps)
 
 lemma iterate_op_plus: "(((+) k) ^^ m) 0 = k * m"
   by (induction m) auto
 
 lemma untion_image_mset_Pair_distribute:
   "\<Union>#{#image_mset (Pair x) (C x). x \<in># J - I#} =
    \<Union># {#image_mset (Pair x) (C x). x \<in># J#} - \<Union>#{#image_mset (Pair x) (C x). x \<in># I#}"
   by (auto simp: multiset_eq_iff count_sum_mset count_image_mset_Pair sum_mset_if_eq_constant
     iterate_op_plus diff_mult_distrib2)
 
 lemma Sigma_mset_Un_distrib1: "Sigma_mset (I \<union># J) C = Sigma_mset I C \<union># Sigma_mset J C"
   by (auto simp: Sigma_mset_def sup_subset_mset_def untion_image_mset_Pair_distribute)
 
 lemma Sigma_mset_Un_distrib2: "(SIGMAMSET i\<in>#I. A i \<union># B i) = Sigma_mset I A \<union># Sigma_mset I B"
   by (auto simp: multiset_eq_iff count_sum_mset count_image_mset_Pair sum_mset_if_eq_constant
     Sigma_mset_def diff_mult_distrib2 iterate_op_plus max_def not_in_iff)
 
 lemma Sigma_mset_Int_distrib1: "Sigma_mset (I \<inter># J) C = Sigma_mset I C \<inter># Sigma_mset J C"
   by (auto simp: multiset_eq_iff count_sum_mset count_image_mset_Pair sum_mset_if_eq_constant
     Sigma_mset_def iterate_op_plus min_def not_in_iff)
 
 lemma Sigma_mset_Int_distrib2: "(SIGMAMSET i\<in>#I. A i \<inter># B i) = Sigma_mset I A \<inter># Sigma_mset I B"
   by (auto simp: multiset_eq_iff count_sum_mset count_image_mset_Pair sum_mset_if_eq_constant
     Sigma_mset_def iterate_op_plus min_def not_in_iff)
 
 lemma Sigma_mset_Diff_distrib1: "Sigma_mset (I - J) C = Sigma_mset I C - Sigma_mset J C"
   by (auto simp: multiset_eq_iff count_sum_mset count_image_mset_Pair sum_mset_if_eq_constant
     Sigma_mset_def iterate_op_plus min_def not_in_iff diff_mult_distrib2)
 
 lemma Sigma_mset_Diff_distrib2: "(SIGMAMSET i\<in>#I. A i - B i) = Sigma_mset I A - Sigma_mset I B"
   by (auto simp: multiset_eq_iff count_sum_mset count_image_mset_Pair sum_mset_if_eq_constant
     Sigma_mset_def iterate_op_plus min_def not_in_iff diff_mult_distrib)
 
 lemma Sigma_mset_Union: "Sigma_mset (\<Union>#X) B = (\<Union># (image_mset (\<lambda>A. Sigma_mset A B) X))"
   by (auto simp: multiset_eq_iff count_sum_mset count_image_mset_Pair sum_mset_if_eq_constant
     Sigma_mset_def iterate_op_plus min_def not_in_iff sum_mset_distrib_left)
 
 lemma Times_mset_Un_distrib1: "(A \<union># B) \<times># C = A \<times># C \<union># B \<times># C"
   by (fact Sigma_mset_Un_distrib1)
 
 lemma Times_mset_Int_distrib1: "(A \<inter># B) \<times># C = A \<times># C \<inter># B \<times># C"
   by (fact Sigma_mset_Int_distrib1)
 
 lemma Times_mset_Diff_distrib1: "(A - B) \<times># C = A \<times># C - B \<times># C"
   by (fact Sigma_mset_Diff_distrib1)
 
 lemma Times_mset_empty[simp]: "A \<times># B = {#} \<longleftrightarrow> A = {#} \<or> B = {#}"
   by (auto simp: Sigma_mset_empty_iff)
 
 lemma Times_insert_left: "A \<times># add_mset x B = A \<times># B + image_mset (\<lambda>a. Pair a x) A"
   unfolding add_mset_add_single[of x B] Sigma_mset_plus_distrib2
   by (simp add: Times_mset_single_right)
 
 lemma Times_insert_right: "add_mset a A \<times># B = A \<times># B + image_mset (Pair a) B"
   unfolding add_mset_add_single[of a A] Sigma_mset_plus_distrib1
   by (simp add: Times_mset_single_left)
 
 lemma fst_image_mset_times_mset [simp]:
   "image_mset fst (A \<times># B) = (if B = {#} then {#} else repeat_mset (size B) A)"
   by (induct B) (auto simp: Times_mset_single_right ac_simps Times_insert_left)
 
 lemma snd_image_mset_times_mset [simp]:
   "image_mset snd (A \<times># B) = (if A = {#} then {#} else repeat_mset (size A) B)"
   by (induct B) (auto simp add: Times_mset_single_right Times_insert_left image_mset_const_eq)
 
 lemma product_swap_mset: "image_mset prod.swap (A \<times># B) = B \<times># A"
   by (induction A) (auto simp add: Times_mset_single_left Times_mset_single_right
       Times_insert_right Times_insert_left)
 
 context
 begin
 
 qualified definition product_mset :: "'a multiset \<Rightarrow> 'b multiset \<Rightarrow> ('a \<times> 'b) multiset" where
   [code_abbrev]: "product_mset A B = A \<times># B"
 
 lemma member_product_mset: "x \<in># product_mset A B \<longleftrightarrow> x \<in># A \<times># B"
   by (simp add: Multiset_More.product_mset_def)
 
 end
 
 lemma count_Sigma_mset_abs_def: "count (Sigma_mset A B) = (\<lambda>(a, b) \<Rightarrow> count A a * count (B a) b)"
   by (auto simp: fun_eq_iff count_Sigma_mset)
 
 lemma Times_mset_image_mset1: "image_mset f A \<times># B = image_mset (\<lambda>(a, b). (f a, b)) (A \<times># B)"
   by (induct B) (auto simp: Times_insert_left)
 
 lemma Times_mset_image_mset2: "A \<times># image_mset f B = image_mset (\<lambda>(a, b). (a, f b)) (A \<times># B)"
   by (induct A) (auto simp: Times_insert_right)
 
 lemma sum_le_singleton: "A \<subseteq> {x} \<Longrightarrow> sum f A = (if x \<in> A then f x else 0)"
   by (auto simp: subset_singleton_iff elim: finite_subset)
 
 lemma Times_mset_assoc: "(A \<times># B) \<times># C = image_mset (\<lambda>(a, b, c). ((a, b), c)) (A \<times># B \<times># C)"
   by (auto simp: multiset_eq_iff count_Sigma_mset count_image_mset vimage_def Times_mset_Times
       Int_commute count_eq_zero_iff intro!: trans[OF _ sym[OF sum_le_singleton[of _ "(_, _, _)"]]]
       cong: sum.cong if_cong)
 
 
 subsection \<open>Transfer Rules\<close>
 
 lemma plus_multiset_transfer[transfer_rule]:
   "(rel_fun (rel_mset R) (rel_fun (rel_mset R) (rel_mset R))) (+) (+)"
   by (unfold rel_fun_def rel_mset_def)
     (force dest: list_all2_appendI intro: exI[of _ "_ @ _"] conjI[rotated])
 
 lemma minus_multiset_transfer[transfer_rule]:
   assumes [transfer_rule]: "bi_unique R"
   shows "(rel_fun (rel_mset R) (rel_fun (rel_mset R) (rel_mset R))) (-) (-)"
 proof (unfold rel_fun_def rel_mset_def, safe)
   fix xs ys xs' ys'
   assume [transfer_rule]: "list_all2 R xs ys" "list_all2 R xs' ys'"
   have "list_all2 R (fold remove1 xs' xs) (fold remove1 ys' ys)"
     by transfer_prover
   moreover have "mset (fold remove1 xs' xs) = mset xs - mset xs'"
     by (induct xs' arbitrary: xs) auto
   moreover have "mset (fold remove1 ys' ys) = mset ys - mset ys'"
     by (induct ys' arbitrary: ys) auto
   ultimately show "\<exists>xs'' ys''.
     mset xs'' = mset xs - mset xs' \<and> mset ys'' = mset ys - mset ys' \<and> list_all2 R xs'' ys''"
     by blast
 qed
 
 declare rel_mset_Zero[transfer_rule]
 
 lemma count_transfer[transfer_rule]:
   assumes "bi_unique R"
   shows "(rel_fun (rel_mset R) (rel_fun R (=))) count count"
 unfolding rel_fun_def rel_mset_def proof safe
   fix x y xs ys
   assume "list_all2 R xs ys" "R x y"
   then show "count (mset xs) x = count (mset ys) y"
   proof (induct xs ys rule: list.rel_induct)
     case (Cons x' xs y' ys)
     then show ?case
       using assms unfolding bi_unique_alt_def2 by (auto simp: rel_fun_def)
   qed simp
 qed
 
 lemma subseteq_multiset_transfer[transfer_rule]:
   assumes [transfer_rule]: "bi_unique R" "right_total R"
   shows "(rel_fun (rel_mset R) (rel_fun (rel_mset R) (=)))
     (\<lambda>M N. filter_mset (Domainp R) M \<subseteq># filter_mset (Domainp R) N) (\<subseteq>#)"
 proof -
   have count_filter_mset_less:
     "(\<forall>a. count (filter_mset (Domainp R) M) a \<le> count (filter_mset (Domainp R) N) a) \<longleftrightarrow>
      (\<forall>a \<in> {x. Domainp R x}. count M a \<le> count N a)" for M and N by auto
   show ?thesis unfolding subseteq_mset_def count_filter_mset_less
     by transfer_prover
 qed
 
 lemma sum_mset_transfer[transfer_rule]:
   "R 0 0 \<Longrightarrow> rel_fun R (rel_fun R R) (+) (+) \<Longrightarrow> (rel_fun (rel_mset R) R) sum_mset sum_mset"
   using sum_list_transfer[of R] unfolding rel_fun_def rel_mset_def by auto
 
 lemma Sigma_mset_transfer[transfer_rule]:
   "(rel_fun (rel_mset R) (rel_fun (rel_fun R (rel_mset S)) (rel_mset (rel_prod R S))))
      Sigma_mset Sigma_mset"
   by (unfold Sigma_mset_def) transfer_prover
 
 
 subsection \<open>Even More about Multisets\<close>
 
 subsubsection \<open>Multisets and Functions\<close>
 
 lemma range_image_mset:
   assumes "set_mset Ds \<subseteq> range f"
   shows "Ds \<in> range (image_mset f)"
 proof -
   have "\<forall>D. D \<in># Ds \<longrightarrow> (\<exists>C. f C = D)"
     using assms by blast
   then obtain f_i where
     f_p: "\<forall>D. D \<in># Ds \<longrightarrow> (f (f_i D) = D)"
     by metis
   define Cs where
     "Cs \<equiv> image_mset f_i Ds"
   from f_p Cs_def have "image_mset f Cs = Ds"
     by auto
   then show ?thesis
     by blast
 qed
 
 
 subsubsection \<open>Multisets and Lists\<close>
 
 lemma length_sorted_list_of_multiset[simp]: "length (sorted_list_of_multiset A) = size A"
   by (metis mset_sorted_list_of_multiset size_mset)
 
 definition list_of_mset :: "'a multiset \<Rightarrow> 'a list" where
   "list_of_mset m = (SOME l. m = mset l)"
 
 lemma list_of_mset_exi: "\<exists>l. m = mset l"
   using ex_mset by metis
 
 lemma mset_list_of_mset [simp]: "mset (list_of_mset m) = m"
   by (metis (mono_tags, lifting) ex_mset list_of_mset_def someI_ex)
 
 lemma length_list_of_mset[simp]: "length (list_of_mset A) = size A"
   unfolding list_of_mset_def by (metis (mono_tags) ex_mset size_mset someI_ex)
 
 lemma range_mset_map:
   assumes "set_mset Ds \<subseteq> range f"
   shows "Ds \<in> range (\<lambda>Cl. mset (map f Cl))"
 proof -
   have "Ds \<in> range (image_mset f)"
     by (simp add: assms range_image_mset)
   then obtain Cs where Cs_p: "image_mset f Cs = Ds"
     by auto
   define Cl where "Cl = list_of_mset Cs"
   then have "mset Cl = Cs"
     by auto
   then have "image_mset f (mset Cl) = Ds"
     using Cs_p by auto
   then have "mset (map f Cl) = Ds"
     by auto
   then show ?thesis
     by auto
 qed
 
 lemma list_of_mset_empty[iff]: "list_of_mset m = [] \<longleftrightarrow> m = {#}"
   by (metis (mono_tags, lifting) ex_mset list_of_mset_def mset_zero_iff_right someI_ex)
 
 lemma in_mset_conv_nth: "(x \<in># mset xs) = (\<exists>i<length xs. xs ! i = x)"
   by (auto simp: in_set_conv_nth)
 
 lemma in_mset_sum_list:
   assumes "L \<in># LL"
   assumes "LL \<in> set Ci"
   shows "L \<in># sum_list Ci"
   using assms by (induction Ci) auto
 
 lemma in_mset_sum_list2:
   assumes "L \<in># sum_list Ci"
   obtains LL where
     "LL \<in> set Ci"
     "L \<in># LL"
   using assms by (induction Ci) auto
 
 lemma subseteq_list_Union_mset:
   assumes "length Ci = n"
   assumes "length CAi = n"
   assumes "\<forall>i<n.  Ci ! i \<subseteq># CAi ! i "
   shows "\<Union># (mset Ci) \<subseteq># \<Union># (mset CAi)"
   using assms proof (induction n arbitrary: Ci CAi)
   case 0
   then show ?case by auto
 next
   case (Suc n)
   from Suc have "\<forall>i<n. tl Ci ! i \<subseteq># tl CAi ! i"
     by (simp add: nth_tl)
   hence "\<Union>#(mset (tl Ci)) \<subseteq># \<Union>#(mset (tl CAi))" using Suc by auto
   moreover
   have "hd Ci \<subseteq># hd CAi" using Suc
     by (metis hd_conv_nth length_greater_0_conv zero_less_Suc)
   ultimately
   show "\<Union>#(mset Ci) \<subseteq># \<Union>#(mset CAi)"
     using Suc by (cases Ci; cases CAi) (auto intro: subset_mset.add_mono)
 qed
 
 
 subsubsection \<open>More on Multisets and Functions\<close>
 
 lemma subseteq_mset_size_eql: "X \<subseteq># Y \<Longrightarrow> size Y = size X \<Longrightarrow> X = Y"
   using mset_subset_size subset_mset_def by fastforce
 
 lemma image_mset_of_subset_list:
   assumes "image_mset \<eta> C' = mset lC"
   shows "\<exists>qC'. map \<eta> qC' = lC \<and> mset qC' = C'"
   using assms apply (induction lC arbitrary: C')
   subgoal by simp
   subgoal by (fastforce dest!: msed_map_invR intro: exI[of _ \<open>_ # _\<close>])
   done
 
 lemma image_mset_of_subset:
   assumes "A \<subseteq># image_mset \<eta> C'"
   shows "\<exists>A'. image_mset \<eta> A' = A \<and> A' \<subseteq># C'"
 proof -
   define C where "C = image_mset \<eta> C'"
 
   define lA where "lA = list_of_mset A"
   define lD where "lD = list_of_mset (C-A)"
   define lC where "lC = lA @ lD"
 
   have "mset lC = C"
     using C_def assms unfolding lD_def lC_def lA_def by auto
   then have "\<exists>qC'. map \<eta> qC' = lC \<and> mset qC' = C'"
     using assms image_mset_of_subset_list unfolding C_def by metis
   then obtain qC' where qC'_p: "map \<eta> qC' = lC \<and> mset qC' = C'"
     by auto
   let ?lA' = "take (length lA) qC'"
   have m: "map \<eta> ?lA' = lA"
     using qC'_p lC_def
     by (metis append_eq_conv_conj take_map)
   let ?A' = "mset ?lA'"
 
   have "image_mset \<eta> ?A' = A"
     using m using lA_def
     by (metis (full_types) ex_mset list_of_mset_def mset_map someI_ex)
   moreover have "?A' \<subseteq># C'"
     using qC'_p unfolding lA_def
     using mset_take_subseteq by blast
   ultimately show ?thesis by blast
 qed
 
 lemma all_the_same: "\<forall>x \<in># X. x = y \<Longrightarrow> card (set_mset X) \<le> Suc 0"
   by (metis card.empty card.insert card_mono finite.intros(1) finite_insert le_SucI singletonI subsetI)
 
 lemma Melem_subseteq_Union_mset[simp]:
   assumes "x \<in># T"
   shows "x \<subseteq># \<Union>#T"
   using assms sum_mset.remove by force
 
 lemma Melem_subset_eq_sum_list[simp]:
   assumes "x \<in># mset T"
   shows "x \<subseteq># sum_list T"
   using assms by (metis mset_subset_eq_add_left sum_mset.remove sum_mset_sum_list)
 
 lemma less_subset_eq_Union_mset[simp]:
   assumes "i < length CAi"
   shows "CAi ! i \<subseteq># \<Union>#(mset CAi)"
 proof -
   from assms have "CAi ! i \<in># mset CAi"
     by auto
   then show ?thesis
     by auto
 qed
 
 lemma less_subset_eq_sum_list[simp]:
   assumes "i < length CAi"
   shows "CAi ! i \<subseteq># sum_list CAi"
 proof -
   from assms have "CAi ! i \<in># mset CAi"
     by auto
   then show ?thesis
     by auto
 qed
 
 
 subsubsection \<open>More on Multiset Order\<close>
 
 lemma less_multiset_doubletons:
   assumes
     "y <  t \<or>  y <  s"  
     "x <  t \<or>  x <  s" 
   shows 
     "{# y,  x#} < {# t,  s#}" 
   unfolding less_multiset\<^sub>D\<^sub>M
 proof (intro exI)
   let ?X = "{# t,  s#}"
   let ?Y = "{#y, x#}"
   show "?X \<noteq> {#} \<and> ?X \<subseteq># {#t, s#} \<and> {#y, x#} = {#t, s#} - ?X + ?Y \<and> (\<forall>k. k \<in># ?Y \<longrightarrow> (\<exists>a. a \<in># ?X \<and> k < a))"
     using add_eq_conv_diff assms(1) assms(2) by auto
 qed
 
 end
diff --git a/thys/Ordered_Resolution_Prover/Lazy_List_Chain.thy b/thys/Ordered_Resolution_Prover/Lazy_List_Chain.thy
--- a/thys/Ordered_Resolution_Prover/Lazy_List_Chain.thy
+++ b/thys/Ordered_Resolution_Prover/Lazy_List_Chain.thy
@@ -1,618 +1,628 @@
 (*  Title:       Relational Chains over Lazy Lists
     Author:      Jasmin Blanchette <j.c.blanchette at vu.nl>, 2014, 2017
     Author:      Dmitriy Traytel <traytel at inf.ethz.ch>, 2017
     Author:      Anders Schlichtkrull <andschl at dtu.dk>, 2017
     Maintainer:  Anders Schlichtkrull <andschl at dtu.dk>
 *)
 
 section \<open>Relational Chains over Lazy Lists\<close>
 
 theory Lazy_List_Chain
   imports "HOL-Library.BNF_Corec" Lazy_List_Liminf
 begin
 
 text \<open>
 A chain is a lazy lists of elements such that all pairs of consecutive elements are related by a
 given relation. A full chain is either an infinite chain or a finite chain that cannot be extended.
 The inspiration for this theory is Section 4.1 (``Theorem Proving Processes'') of Bachmair and
 Ganzinger's chapter.
 \<close>
 
 
 subsection \<open>Chains\<close>
 
 coinductive chain :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a llist \<Rightarrow> bool" for R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where
 	chain_singleton: "chain R (LCons x LNil)"
 | chain_cons: "chain R xs \<Longrightarrow> R x (lhd xs) \<Longrightarrow> chain R (LCons x xs)"
 
 lemma
   chain_LNil[simp]: "\<not> chain R LNil" and
   chain_not_lnull: "chain R xs \<Longrightarrow> \<not> lnull xs"
   by (auto elim: chain.cases)
 
 lemma chain_lappend:
   assumes
     r_xs: "chain R xs" and
     r_ys: "chain R ys" and
     mid: "R (llast xs) (lhd ys)"
   shows "chain R (lappend xs ys)"
 proof (cases "lfinite xs")
   case True
   then show ?thesis
     using r_xs mid
   proof (induct rule: lfinite.induct)
     case (lfinite_LConsI xs x)
     note fin = this(1) and ih = this(2) and r_xxs = this(3) and mid = this(4)
     show ?case
     proof (cases "xs = LNil")
       case True
       then show ?thesis
         using r_ys mid by simp (rule chain_cons)
     next
       case xs_nnil: False
       have r_xs: "chain R xs"
         by (metis chain.simps ltl_simps(2) r_xxs xs_nnil)
       have mid': "R (llast xs) (lhd ys)"
         by (metis llast_LCons lnull_def mid xs_nnil)
       have start: "R x (lhd (lappend xs ys))"
         by (metis (no_types) chain.simps lhd_LCons lhd_lappend chain_not_lnull ltl_simps(2) r_xxs
             xs_nnil)
       show ?thesis
         unfolding lappend_code(2) using ih[OF r_xs mid'] start by (rule chain_cons)
     qed
   qed simp
 qed (simp add: r_xs lappend_inf)
 
 lemma chain_length_pos: "chain R xs \<Longrightarrow> llength xs > 0"
   by (cases xs) simp+
 
 lemma chain_ldropn:
   assumes "chain R xs" and "enat n < llength xs"
   shows "chain R (ldropn n xs)"
   using assms
   by (induct n arbitrary: xs, simp,
       metis chain.cases ldrop_eSuc_ltl ldropn_LNil ldropn_eq_LNil ltl_simps(2) not_less)
 
+lemma inf_chain_ldropn_chain: "chain R xs \<Longrightarrow> \<not> lfinite xs \<Longrightarrow> chain R (ldropn n xs)"
+  using chain.simps[of R xs] by (simp add: chain_ldropn not_lfinite_llength)
+
+lemma inf_chain_ltl_chain: "chain R xs \<Longrightarrow> \<not> lfinite xs \<Longrightarrow> chain R (ltl xs)"
+  by (metis inf_chain_ldropn_chain ldropn_0 ldropn_ltl)
+
 lemma chain_lnth_rel:
   assumes
     chain: "chain R xs" and
     len: "enat (Suc j) < llength xs"
   shows "R (lnth xs j) (lnth xs (Suc j))"
 proof -
   define ys where "ys = ldropn j xs"
   have "llength ys > 1"
     unfolding ys_def using len
     by (metis One_nat_def funpow_swap1 ldropn_0 ldropn_def ldropn_eq_LNil ldropn_ltl not_less
         one_enat_def)
   obtain y0 y1 ys' where
     ys: "ys = LCons y0 (LCons y1 ys')"
     unfolding ys_def by (metis Suc_ile_eq ldropn_Suc_conv_ldropn len less_imp_not_less not_less)
   have "chain R ys"
     unfolding ys_def using Suc_ile_eq chain chain_ldropn len less_imp_le by blast
   then have "R y0 y1"
     unfolding ys by (auto elim: chain.cases)
   then show ?thesis
     using ys_def unfolding ys by (metis ldropn_Suc_conv_ldropn ldropn_eq_LConsD llist.inject)
 qed
 
 lemma infinite_chain_lnth_rel:
   assumes "\<not> lfinite c" and "chain r c"
   shows "r (lnth c i) (lnth c (Suc i))"
   using assms chain_lnth_rel lfinite_conv_llength_enat by force
 
 lemma lnth_rel_chain:
   assumes
     "\<not> lnull xs" and
     "\<forall>j. enat (j + 1) < llength xs \<longrightarrow> R (lnth xs j) (lnth xs (j + 1))"
   shows "chain R xs"
   using assms
 proof (coinduction arbitrary: xs rule: chain.coinduct)
   case chain
   note nnul = this(1) and nth_chain = this(2)
 
   show ?case
   proof (cases "lnull (ltl xs)")
     case True
     have "xs = LCons (lhd xs) LNil"
       using nnul True by (simp add: llist.expand)
     then show ?thesis
       by blast
   next
     case nnul': False
     moreover have "xs = LCons (lhd xs) (ltl xs)"
       using nnul by simp
     moreover have
       "\<forall>j. enat (j + 1) < llength (ltl xs) \<longrightarrow> R (lnth (ltl xs) j) (lnth (ltl xs) (j + 1))"
       using nnul nth_chain
       by (metis Suc_eq_plus1 ldrop_eSuc_ltl ldropn_Suc_conv_ldropn ldropn_eq_LConsD lnth_ltl)
     moreover have "R (lhd xs) (lhd (ltl xs))"
       using nnul' nnul nth_chain[rule_format, of 0, simplified]
       by (metis ldropn_0 ldropn_Suc_conv_ldropn ldropn_eq_LConsD lhd_LCons_ltl lhd_conv_lnth
           lnth_Suc_LCons ltl_simps(2))
     ultimately show ?thesis
       by blast
   qed
 qed
 
 lemma chain_lmap:
   assumes "\<forall>x y. R x y \<longrightarrow> R' (f x) (f y)" and "chain R xs"
   shows "chain R' (lmap f xs)"
   using assms
 proof (coinduction arbitrary: xs)
   case chain
   then have "(\<exists>y. xs = LCons y LNil) \<or> (\<exists>ys x. xs = LCons x ys \<and> chain R ys \<and> R x (lhd ys))"
     using chain.simps[of R xs] by auto
   then show ?case
   proof
     assume "\<exists>ys x. xs = LCons x ys \<and> chain R ys \<and> R x (lhd ys)"
     then have "\<exists>ys x. lmap f xs = LCons x ys \<and>
       (\<exists>xs. ys = lmap f xs \<and> (\<forall>x y. R x y \<longrightarrow> R' (f x) (f y)) \<and> chain R xs) \<and> R' x (lhd ys)"
       using chain
       by (metis (no_types) lhd_LCons llist.distinct(1) llist.exhaust_sel llist.map_sel(1)
           lmap_eq_LNil chain_not_lnull ltl_lmap ltl_simps(2))
     then show ?thesis
       by auto
   qed auto
 qed
 
 lemma chain_mono:
   assumes "\<forall>x y. R x y \<longrightarrow> R' x y" and "chain R xs"
   shows "chain R' xs"
   using assms by (rule chain_lmap[of _ _ "\<lambda>x. x", unfolded llist.map_ident])
 
 lemma lfinite_chain_imp_rtranclp_lhd_llast: "lfinite xs \<Longrightarrow> chain R xs \<Longrightarrow> R\<^sup>*\<^sup>* (lhd xs) (llast xs)"
 proof (induct rule: lfinite.induct)
   case (lfinite_LConsI xs x)
   note fin_xs = this(1) and ih = this(2) and r_x_xs = this(3)
   show ?case
   proof (cases "xs = LNil")
     case xs_nnil: False
     then have r_xs: "chain R xs"
       using r_x_xs by (blast elim: chain.cases)
     then show ?thesis
       using ih[OF r_xs] xs_nnil r_x_xs
       by (metis chain.cases converse_rtranclp_into_rtranclp lhd_LCons llast_LCons chain_not_lnull
           ltl_simps(2))
   qed simp
 qed simp
 
 lemma tranclp_imp_exists_finite_chain_list:
   "R\<^sup>+\<^sup>+ x y \<Longrightarrow> \<exists>xs. chain R (llist_of (x # xs @ [y]))"
 proof (induct rule: tranclp.induct)
   case (r_into_trancl x y)
   then have "chain R (llist_of (x # [] @ [y]))"
     by (auto intro: chain.intros)
   then show ?case
     by blast
 next
   case (trancl_into_trancl x y z)
   note rstar_xy = this(1) and ih = this(2) and r_yz = this(3)
 
   obtain xs where
     xs: "chain R (llist_of (x # xs @ [y]))"
     using ih by blast
   define ys where
     "ys = xs @ [y]"
 
   have "chain R (llist_of (x # ys @ [z]))"
     unfolding ys_def using r_yz chain_lappend[OF xs chain_singleton, of z]
     by (auto simp: lappend_llist_of_LCons llast_LCons)
   then show ?case
     by blast
 qed
 
 inductive_cases chain_consE: "chain R (LCons x xs)"
 inductive_cases chain_nontrivE: "chain R (LCons x (LCons y xs))"
 
+
+subsection \<open>A Coinductive Puzzle\<close>
+
 primrec prepend where
   "prepend [] ys = ys"
 | "prepend (x # xs) ys = LCons x (prepend xs ys)"
 
 lemma lnull_prepend[simp]: "lnull (prepend xs ys) = (xs = [] \<and> lnull ys)"
   by (induct xs) auto
 
 lemma lhd_prepend[simp]: "lhd (prepend xs ys) = (if xs \<noteq> [] then hd xs else lhd ys)"
   by (induct xs) auto
 
 lemma prepend_LNil[simp]: "prepend xs LNil = llist_of xs"
   by (induct xs) auto
 
 lemma lfinite_prepend[simp]: "lfinite (prepend xs ys) \<longleftrightarrow> lfinite ys"
   by (induct xs) auto
 
 lemma llength_prepend[simp]: "llength (prepend xs ys) = length xs + llength ys"
   by (induct xs) (auto simp: enat_0 iadd_Suc eSuc_enat[symmetric])
 
 lemma llast_prepend[simp]: "\<not> lnull ys \<Longrightarrow> llast (prepend xs ys) = llast ys"
   by (induct xs) (auto simp: llast_LCons)
 
 lemma prepend_prepend: "prepend xs (prepend ys zs) = prepend (xs @ ys) zs"
   by (induct xs) auto
 
 lemma chain_prepend:
   "chain R (llist_of zs) \<Longrightarrow> last zs = lhd xs \<Longrightarrow> chain R xs \<Longrightarrow> chain R (prepend zs (ltl xs))"
   by (induct zs; cases xs)
     (auto split: if_splits simp: lnull_def[symmetric] intro!: chain_cons elim!: chain_consE)
 
 lemma lmap_prepend[simp]: "lmap f (prepend xs ys) = prepend (map f xs) (lmap f ys)"
   by (induct xs) auto
 
 lemma lset_prepend[simp]: "lset (prepend xs ys) = set xs \<union> lset ys"
   by (induct xs) auto
 
 lemma prepend_LCons: "prepend xs (LCons y ys) = prepend (xs @ [y]) ys"
   by (induct xs) auto
 
 lemma lnth_prepend:
   "lnth (prepend xs ys) i = (if i < length xs then nth xs i else lnth ys (i - length xs))"
   by (induct xs arbitrary: i) (auto simp: lnth_LCons' nth_Cons')
 
 theorem lfinite_less_induct[consumes 1, case_names less]:
   assumes fin: "lfinite xs"
     and step: "\<And>xs. lfinite xs \<Longrightarrow> (\<And>zs. llength zs < llength xs \<Longrightarrow> P zs) \<Longrightarrow> P xs"
   shows "P xs"
 using fin proof (induct "the_enat (llength xs)" arbitrary: xs rule: less_induct)
   case (less xs)
   show ?case
     using less(2) by (intro step[OF less(2)] less(1))
       (auto dest!: lfinite_llength_enat simp: eSuc_enat elim!: less_enatE llength_eq_enat_lfiniteD)
 qed
 
 theorem lfinite_prepend_induct[consumes 1, case_names LNil prepend]:
   assumes "lfinite xs"
     and LNil: "P LNil"
     and prepend: "\<And>xs. lfinite xs \<Longrightarrow> (\<And>zs. (\<exists>ys. xs = prepend ys zs \<and> ys \<noteq> []) \<Longrightarrow> P zs) \<Longrightarrow> P xs"
   shows "P xs"
 using assms(1) proof (induct xs rule: lfinite_less_induct)
   case (less xs)
   from less(1) show ?case
     by (cases xs)
       (force simp: LNil neq_Nil_conv dest: lfinite_llength_enat intro!: prepend[of "LCons _ _"] intro: less)+
 qed
 
 coinductive emb :: "'a llist \<Rightarrow> 'a llist \<Rightarrow> bool" where
   "lfinite xs \<Longrightarrow> emb LNil xs"
 | "emb xs ys \<Longrightarrow> emb (LCons x xs) (prepend zs (LCons x ys))"
 
 inductive_cases emb_LConsE: "emb (LCons z zs) ys"
 inductive_cases emb_LNil1E: "emb LNil ys"
 inductive_cases emb_LNil2E: "emb xs LNil"
 
 lemma emb_lfinite:
   assumes "emb xs ys"
   shows "lfinite ys \<longleftrightarrow> lfinite xs"
 proof
   assume "lfinite xs"
   then show "lfinite ys" using assms
     by (induct xs arbitrary: ys rule: lfinite_induct)
       (auto simp: lnull_def neq_LNil_conv elim!: emb_LNil1E emb_LConsE)
 next
   assume "lfinite ys"
   then show "lfinite xs" using assms
   proof (induction ys arbitrary: xs rule: lfinite_less_induct)
     case (less ys)
     from less.prems \<open>lfinite ys\<close> show ?case
       by (cases xs)
-        (auto simp: eSuc_enat elim!: emb_LNil1E emb_LConsE less.IH[rotated] dest!: lfinite_llength_enat)
+        (auto simp: eSuc_enat elim!: emb_LNil1E emb_LConsE less.IH[rotated]
+          dest!: lfinite_llength_enat)
   qed
 qed
 
 inductive prepend_cong1 for X where
   prepend_cong1_base: "X xs \<Longrightarrow> prepend_cong1 X xs"
 | prepend_cong1_prepend: "prepend_cong1 X ys \<Longrightarrow> prepend_cong1 X (prepend xs ys)"
 
 lemma emb_prepend_coinduct[rotated, case_names emb]:
   assumes "(\<And>x1 x2. X x1 x2 \<Longrightarrow>
     (\<exists>xs. x1 = LNil \<and> x2 = xs \<and> lfinite xs)
      \<or> (\<exists>xs ys x zs. x1 = LCons x xs \<and> x2 = prepend zs (LCons x ys)
        \<and> (prepend_cong1 (X xs) ys \<or> emb xs ys)))" (is "\<And>x1 x2. X x1 x2 \<Longrightarrow> ?bisim x1 x2")
   shows "X x1 x2 \<Longrightarrow> emb x1 x2"
 proof (erule emb.coinduct[OF prepend_cong1_base])
   fix xs zs
   assume "prepend_cong1 (X xs) zs"
   then show "?bisim xs zs"
     by (induct zs rule: prepend_cong1.induct) (erule assms, force simp: prepend_prepend)
 qed
 
 context
 begin
 
 private coinductive chain' for R where
   "chain' R (LCons x LNil)"
 | "chain R (llist_of (x # zs @ [lhd xs])) \<Longrightarrow>
    chain' R xs \<Longrightarrow> chain' R (LCons x (prepend zs xs))"
 
 private lemma chain_imp_chain': "chain R xs \<Longrightarrow> chain' R xs"
 proof (coinduction arbitrary: xs rule: chain'.coinduct)
   case chain'
   then show ?case
   proof (cases rule: chain.cases)
     case (chain_cons zs z)
     then show ?thesis
       by (intro disjI2 exI[of _ z] exI[of _ "[]"] exI[of _ "zs"])
         (auto intro: chain.intros)
   qed simp
 qed
 
 private lemma chain'_imp_chain: "chain' R xs \<Longrightarrow> chain R xs"
 proof (coinduction arbitrary: xs rule: chain.coinduct)
   case chain
   then show ?case
   proof (cases rule: chain'.cases)
     case (2 y zs ys)
     then show ?thesis
       by (intro disjI2 exI[of _ "prepend zs ys"] exI[of _ y])
         (force dest!: neq_Nil_conv[THEN iffD1] elim: chain.cases chain_nontrivE
           intro: chain'.intros)
   qed simp
 qed
 
 private lemma chain_chain': "chain = chain'"
   unfolding fun_eq_iff by (metis chain_imp_chain' chain'_imp_chain)
 
 lemma chain_prepend_coinduct[case_names chain]:
   "X x \<Longrightarrow> (\<And>x. X x \<Longrightarrow>
     (\<exists>z. x = LCons z LNil) \<or>
     (\<exists>y xs zs. x = LCons y (prepend zs xs) \<and>
       (X xs \<or> chain R xs) \<and> chain R (llist_of (y # zs @ [lhd xs])))) \<Longrightarrow> chain R x"
   by (subst chain_chain', erule chain'.coinduct) (force simp: chain_chain')
 
 end
 
 context
   fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
 begin
 
 private definition pick where
   "pick x y = (SOME xs. chain R (llist_of (x # xs @ [y])))"
 
 private lemma pick[simp]:
   assumes "R\<^sup>+\<^sup>+ x y"
   shows "chain R (llist_of (x # pick x y @ [y]))"
   unfolding pick_def using tranclp_imp_exists_finite_chain_list[THEN someI_ex, OF assms] by auto
 
 private friend_of_corec prepend where
   "prepend xs ys = (case xs of [] \<Rightarrow>
     (case ys of LNil \<Rightarrow> LNil | LCons x xs \<Rightarrow> LCons x xs) | x # xs' \<Rightarrow> LCons x (prepend xs' ys))"
   by (simp split: list.splits llist.splits) transfer_prover
 
 private corec wit where
   "wit xs = (case xs of LCons x (LCons y xs) \<Rightarrow>
      LCons x (prepend (pick x y) (wit (LCons y xs))) | _ \<Rightarrow> xs)"
 
 private lemma
   wit_LNil[simp]: "wit LNil = LNil" and
   wit_lsingleton[simp]: "wit (LCons x LNil) = LCons x LNil" and
   wit_LCons2: "wit (LCons x (LCons y xs)) =
      (LCons x (prepend (pick x y) (wit (LCons y xs))))"
   by (subst wit.code; auto)+
 
 private lemma lnull_wit[simp]: "lnull (wit xs) \<longleftrightarrow> lnull xs"
   by (subst wit.code) (auto split: llist.splits simp: Let_def)
 
 private lemma lhd_wit[simp]: "chain R\<^sup>+\<^sup>+ xs \<Longrightarrow> lhd (wit xs) = lhd xs"
   by (erule chain.cases; subst wit.code) (auto split: llist.splits simp: Let_def)
 
 private lemma LNil_eq_iff_lnull: "LNil = xs \<longleftrightarrow> lnull xs"
   by (cases xs) auto
 
 lemma emb_wit[simp]: "chain R\<^sup>+\<^sup>+ xs \<Longrightarrow> emb xs (wit xs)"
 proof (coinduction arbitrary: xs rule: emb_prepend_coinduct)
   case (emb xs)
   then show ?case
   proof (cases rule: chain.cases)
     case (chain_cons zs z)
     then show ?thesis
       by (subst (2) wit.code)
         (auto split: llist.splits intro!: exI[of _ "[]"] exI[of _ "_ :: _ llist"]
           prepend_cong1_prepend[OF prepend_cong1_base])
   qed (auto intro!: exI[of _ LNil] exI[of _ "[]"] emb.intros)
 qed
 
 private lemma lfinite_wit[simp]:
   assumes "chain R\<^sup>+\<^sup>+ xs"
   shows "lfinite (wit xs) \<longleftrightarrow> lfinite xs"
   using emb_wit emb_lfinite assms by blast
 
 private lemma llast_wit[simp]:
   assumes "chain R\<^sup>+\<^sup>+ xs"
   shows "llast (wit xs) = llast xs"
 proof (cases "lfinite xs")
   case True
   from this assms show ?thesis
   proof (induct rule: lfinite.induct)
     case (lfinite_LConsI xs x)
     then show ?case
       by (cases xs) (auto simp: wit_LCons2 llast_LCons elim: chain_nontrivE)
   qed auto
 qed (auto simp: llast_linfinite assms)
 
 lemma chain_tranclp_imp_exists_chain:
   "chain R\<^sup>+\<^sup>+ xs \<Longrightarrow>
    \<exists>ys. chain R ys \<and> emb xs ys \<and> lhd ys = lhd xs \<and> llast ys = llast xs"
 proof (intro exI[of _ "wit xs"] conjI, coinduction arbitrary: xs rule: chain_prepend_coinduct)
   case chain
   then show ?case
     by (subst (1 2) wit.code) (erule chain.cases; force split: llist.splits dest: pick)
 qed auto
 
 lemma emb_lset_mono[rotated]: "x \<in> lset xs \<Longrightarrow> emb xs ys \<Longrightarrow> x \<in> lset ys"
   by (induct x xs arbitrary: ys rule: llist.set_induct) (auto elim!: emb_LConsE)
 
 lemma emb_Ball_lset_antimono:
   assumes "emb Xs Ys"
   shows "\<forall>Y \<in> lset Ys. x \<in> Y \<Longrightarrow> \<forall>X \<in> lset Xs. x \<in> X"
   using emb_lset_mono[OF assms] by blast
 
 lemma emb_lfinite_antimono[rotated]: "lfinite ys \<Longrightarrow> emb xs ys \<Longrightarrow> lfinite xs"
   by (induct ys arbitrary: xs rule: lfinite_prepend_induct)
     (force elim!: emb_LNil2E simp: LNil_eq_iff_lnull prepend_LCons elim: emb.cases)+
 
 lemma emb_Liminf_llist_mono_aux:
   assumes "emb Xs Ys" and "\<not> lfinite Xs" and "\<not> lfinite Ys" and "\<forall>j\<ge>i. x \<in> lnth Ys j"
   shows "\<forall>j\<ge>i. x \<in> lnth Xs j"
 using assms proof (induct i arbitrary: Xs Ys rule: less_induct)
   case (less i)
   then show ?case
   proof (cases i)
     case 0
     then show ?thesis
       using emb_Ball_lset_antimono[OF less(2), of x] less(5)
       unfolding Ball_def in_lset_conv_lnth simp_thms
         not_lfinite_llength[OF less(3)] not_lfinite_llength[OF less(4)] enat_ord_code subset_eq
       by blast
   next
     case [simp]: (Suc nat)
     from less(2,3) obtain xs as b bs where
       [simp]: "Xs = LCons b xs" "Ys = prepend as (LCons b bs)" and "emb xs bs"
       by (auto elim: emb.cases)
     have IH: "\<forall>k\<ge>j. x \<in> lnth xs k" if "\<forall>k\<ge>j. x \<in> lnth bs k" "j < i" for j
       using that less(1)[OF _ \<open>emb xs bs\<close>] less(3,4) by auto
     from less(5) have "\<forall>k\<ge>i - length as - 1. x \<in> lnth xs k"
       by (intro IH allI)
         (drule spec[of _ "_ + length as + 1"], auto simp: lnth_prepend lnth_LCons')
     then show ?thesis
       by (auto simp: lnth_LCons')
   qed
 qed
 
 lemma emb_Liminf_llist_infinite:
   assumes "emb Xs Ys" and "\<not> lfinite Xs"
   shows "Liminf_llist Ys \<subseteq> Liminf_llist Xs"
 proof -
   from assms have "\<not> lfinite Ys"
     using emb_lfinite_antimono by blast
   with assms show ?thesis
     unfolding Liminf_llist_def by (auto simp: not_lfinite_llength dest: emb_Liminf_llist_mono_aux)
 qed
 
 lemma emb_lmap: "emb xs ys \<Longrightarrow> emb (lmap f xs) (lmap f ys)"
 proof (coinduction arbitrary: xs ys rule: emb.coinduct)
   case emb
   show ?case
   proof (cases xs)
     case xs: (LCons x xs')
 
     obtain ysa0 and zs0 where
       ys: "ys = prepend zs0 (LCons x ysa0)" and
       emb': "emb xs' ysa0"
       using emb_LConsE[OF emb[unfolded xs]] by metis
 
     let ?xa = "f x"
     let ?xsa = "lmap f xs'"
     let ?zs = "map f zs0"
     let ?ysa = "lmap f ysa0"
 
     have "lmap f xs = LCons ?xa ?xsa"
       unfolding xs by simp
     moreover have "lmap f ys = prepend ?zs (LCons ?xa ?ysa)"
       unfolding ys by simp
     moreover have "\<exists>xsa ysa. ?xsa = lmap f xsa \<and> ?ysa = lmap f ysa \<and> emb xsa ysa"
       using emb' by blast
     ultimately show ?thesis
       by blast
   qed (simp add: emb_lfinite[OF emb])
 qed
 
 end
 
 lemma chain_inf_llist_if_infinite_chain_function:
   assumes "\<forall>i. r (f (Suc i)) (f i)"
   shows "\<not> lfinite (inf_llist f) \<and> chain r\<inverse>\<inverse> (inf_llist f)"
   using assms by (simp add: lnth_rel_chain)
 
 lemma infinite_chain_function_iff_infinite_chain_llist:
   "(\<exists>f. \<forall>i. r (f (Suc i)) (f i)) \<longleftrightarrow> (\<exists>c. \<not> lfinite c \<and> chain r\<inverse>\<inverse> c)"
   using chain_inf_llist_if_infinite_chain_function infinite_chain_lnth_rel by blast
 
 lemma wfP_iff_no_infinite_down_chain_llist: "wfP r \<longleftrightarrow> (\<nexists>c. \<not> lfinite c \<and> chain r\<inverse>\<inverse> c)"
 proof -
   have "wfP r \<longleftrightarrow>  wf {(x, y). r x y}"
     unfolding wfP_def by auto
   also have "\<dots> \<longleftrightarrow> (\<nexists>f. \<forall>i. (f (Suc i), f i) \<in> {(x, y). r x y})"
     using wf_iff_no_infinite_down_chain by blast
   also have "\<dots> \<longleftrightarrow> (\<nexists>f. \<forall>i. r (f (Suc i)) (f i))"
     by auto
   also have "\<dots> \<longleftrightarrow> (\<nexists>c. \<not>lfinite c \<and> chain r\<inverse>\<inverse> c)"
     using infinite_chain_function_iff_infinite_chain_llist by blast
   finally show ?thesis
     by auto
 qed
 
 
 subsection \<open>Full Chains\<close>
 
 coinductive full_chain :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a llist \<Rightarrow> bool" for R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where
 	full_chain_singleton: "(\<forall>y. \<not> R x y) \<Longrightarrow> full_chain R (LCons x LNil)"
 | full_chain_cons: "full_chain R xs \<Longrightarrow> R x (lhd xs) \<Longrightarrow> full_chain R (LCons x xs)"
 
 lemma
   full_chain_LNil[simp]: "\<not> full_chain R LNil" and
   full_chain_not_lnull: "full_chain R xs \<Longrightarrow> \<not> lnull xs"
   by (auto elim: full_chain.cases)
 
 lemma full_chain_ldropn:
   assumes full: "full_chain R xs" and "enat n < llength xs"
   shows "full_chain R (ldropn n xs)"
   using assms
   by (induct n arbitrary: xs, simp,
       metis full_chain.cases ldrop_eSuc_ltl ldropn_LNil ldropn_eq_LNil ltl_simps(2) not_less)
 
 lemma full_chain_iff_chain:
   "full_chain R xs \<longleftrightarrow> chain R xs \<and> (lfinite xs \<longrightarrow> (\<forall>y. \<not> R (llast xs) y))"
 proof (intro iffI conjI impI allI; (elim conjE)?)
   assume full: "full_chain R xs"
 
   show chain: "chain R xs"
     using full by (coinduction arbitrary: xs) (auto elim: full_chain.cases)
 
   {
     fix y
     assume "lfinite xs"
     then obtain n where
       suc_n: "Suc n = llength xs"
       by (metis chain chain_length_pos lessE less_enatE lfinite_conv_llength_enat)
 
     have "full_chain R (ldropn n xs)"
       by (rule full_chain_ldropn[OF full]) (use suc_n Suc_ile_eq in force)
     moreover have "ldropn n xs = LCons (llast xs) LNil"
       using suc_n by (metis enat_le_plus_same(2) enat_ord_simps(2) gen_llength_def
           ldropn_Suc_conv_ldropn ldropn_all lessI llast_ldropn llast_singleton llength_code)
     ultimately show "\<not> R (llast xs) y"
       by (auto elim: full_chain.cases)
   }
 next
   assume
     "chain R xs" and
     "lfinite xs \<longrightarrow> (\<forall>y. \<not> R (llast xs) y)"
   then show "full_chain R xs"
     by (coinduction arbitrary: xs) (erule chain.cases, simp, metis lfinite_LConsI llast_LCons)
 qed
 
 lemma full_chain_imp_chain: "full_chain R xs \<Longrightarrow> chain R xs"
   using full_chain_iff_chain by blast
 
 lemma full_chain_length_pos: "full_chain R xs \<Longrightarrow> llength xs > 0"
   by (fact chain_length_pos[OF full_chain_imp_chain])
 
 lemma full_chain_lnth_rel:
   "full_chain R xs \<Longrightarrow> enat (Suc j) < llength xs \<Longrightarrow> R (lnth xs j) (lnth xs (Suc j))"
   by (fact chain_lnth_rel[OF full_chain_imp_chain])
 
 inductive_cases full_chain_consE: "full_chain R (LCons x xs)"
 inductive_cases full_chain_nontrivE: "full_chain R (LCons x (LCons y xs))"
 
 lemma full_chain_tranclp_imp_exists_full_chain:
   assumes full: "full_chain R\<^sup>+\<^sup>+ xs"
   shows "\<exists>ys. full_chain R ys \<and> emb xs ys \<and> lhd ys = lhd xs \<and> llast ys = llast xs"
 proof -
   obtain ys where ys:
     "chain R ys" "emb xs ys" "lhd ys = lhd xs" "llast ys = llast xs"
     using full_chain_imp_chain[OF full] chain_tranclp_imp_exists_chain by blast
   have "full_chain R ys"
     using ys(1,4) emb_lfinite[OF ys(2)] full unfolding full_chain_iff_chain by auto
   then show ?thesis
     using ys(2-4) by auto
 qed
 
 end