diff --git a/thys/Saturation_Framework/Calculus.thy b/thys/Saturation_Framework/Calculus.thy
--- a/thys/Saturation_Framework/Calculus.thy
+++ b/thys/Saturation_Framework/Calculus.thy
@@ -1,409 +1,409 @@
 (*  Title:       Calculi Based on a Redundancy Criterion
  *  Author:      Sophie Tourret <stourret at mpi-inf.mpg.de>, 2018-2020 *)
 
 section \<open>Calculi Based on a Redundancy Criterion\<close>
 
 text \<open>This section introduces the most basic notions upon which the framework is
   built: consequence relations and inference systems. It also defines the notion
   of a family of consequence relations and of redundancy criteria. This
   corresponds to sections 2.1 and 2.2 of the report.\<close>
 
 theory Calculus
   imports
     Ordered_Resolution_Prover.Lazy_List_Liminf
     Ordered_Resolution_Prover.Lazy_List_Chain
 begin
 
 
 subsection \<open>Consequence Relations\<close>
 
 locale consequence_relation =
   fixes
     Bot :: "'f set" and
     entails :: "'f set \<Rightarrow> 'f set \<Rightarrow> bool" (infix "\<Turnstile>" 50)
   assumes
     bot_not_empty: "Bot \<noteq> {}" and
     bot_entails_all: "B \<in> Bot \<Longrightarrow> {B} \<Turnstile> N1" and
     subset_entailed: "N2 \<subseteq> N1 \<Longrightarrow> N1 \<Turnstile> N2" and
     all_formulas_entailed: "(\<forall>C \<in> N2. N1 \<Turnstile> {C}) \<Longrightarrow> N1 \<Turnstile> N2" and
     entails_trans[trans]: "N1 \<Turnstile> N2 \<Longrightarrow> N2 \<Turnstile> N3 \<Longrightarrow> N1 \<Turnstile> N3"
 begin
 
 lemma entail_set_all_formulas: "N1 \<Turnstile> N2 \<longleftrightarrow> (\<forall>C \<in> N2. N1 \<Turnstile> {C})"
   by (meson all_formulas_entailed empty_subsetI insert_subset subset_entailed entails_trans)
 
 lemma entail_union: "N \<Turnstile> N1 \<and> N \<Turnstile> N2 \<longleftrightarrow> N \<Turnstile> N1 \<union> N2"
   using entail_set_all_formulas[of N N1] entail_set_all_formulas[of N N2]
     entail_set_all_formulas[of N "N1 \<union> N2"] by blast
 
 lemma entail_unions: "(\<forall>i \<in> I. N \<Turnstile> Ni i) \<longleftrightarrow> N \<Turnstile> \<Union> (Ni ` I)"
   using entail_set_all_formulas[of N "\<Union> (Ni ` I)"] entail_set_all_formulas[of N]
     Complete_Lattices.UN_ball_bex_simps(2)[of Ni I "\<lambda>C. N \<Turnstile> {C}", symmetric]
   by meson
 
 lemma entail_all_bot: "(\<exists>B \<in> Bot. N \<Turnstile> {B}) \<Longrightarrow> (\<forall>B' \<in> Bot. N \<Turnstile> {B'})"
   using bot_entails_all entails_trans by blast
 
 lemma entails_trans_strong: "N1 \<Turnstile> N2 \<Longrightarrow> N1 \<union> N2 \<Turnstile> N3 \<Longrightarrow> N1 \<Turnstile> N3"
   by (meson entail_union entails_trans order_refl subset_entailed)
 
 end
 
 
 subsection \<open>Families of Consequence Relations\<close>
 
 locale consequence_relation_family =
   fixes
     Bot :: "'f set" and
     Q :: "'q set" and
     entails_q :: "'q \<Rightarrow> ('f set \<Rightarrow> 'f set \<Rightarrow> bool)"
   assumes
     Q_nonempty: "Q \<noteq> {}" and
     q_cons_rel: "\<forall>q \<in> Q. consequence_relation Bot (entails_q q)"
 begin
 
 lemma bot_not_empty: "Bot \<noteq> {}"
   using Q_nonempty consequence_relation.bot_not_empty consequence_relation_family.q_cons_rel
     consequence_relation_family_axioms by blast
 
 definition entails :: "'f set \<Rightarrow> 'f set \<Rightarrow> bool" (infix "\<Turnstile>Q" 50) where
   "N1 \<Turnstile>Q N2 \<longleftrightarrow> (\<forall>q \<in> Q. entails_q q N1 N2)"
 
 (* lem:intersection-of-conseq-rel *)
 lemma intersect_cons_rel_family: "consequence_relation Bot entails"
   unfolding consequence_relation_def entails_def
   by (intro conjI bot_not_empty) (metis consequence_relation_def q_cons_rel)+
 
 end
 
 
 subsection \<open>Inference Systems\<close>
 
 datatype 'f inference =
   Infer (prems_of: "'f list") (concl_of: "'f")
 
 locale inference_system =
   fixes
     Inf :: \<open>'f inference set\<close>
 begin
 
 definition Inf_from :: "'f set \<Rightarrow> 'f inference set" where
   "Inf_from N = {\<iota> \<in> Inf. set (prems_of \<iota>) \<subseteq> N}"
 
 definition Inf_between :: "'f set \<Rightarrow> 'f set \<Rightarrow> 'f inference set" where
   "Inf_between N M = Inf_from (N \<union> M) - Inf_from (N - M)"
 
 lemma Inf_if_Inf_from: "\<iota> \<in> Inf_from N \<Longrightarrow> \<iota> \<in> Inf"
   unfolding Inf_from_def by simp
 
 lemma Inf_if_Inf_between: "\<iota> \<in> Inf_between N M \<Longrightarrow> \<iota> \<in> Inf"
   unfolding Inf_between_def Inf_from_def by simp
 
 lemma Inf_between_alt:
   "Inf_between N M = {\<iota> \<in> Inf. \<iota> \<in> Inf_from (N \<union> M) \<and> set (prems_of \<iota>) \<inter> M \<noteq> {}}"
   unfolding Inf_from_def Inf_between_def by auto
 
 lemma Inf_from_mono: "N \<subseteq> N' \<Longrightarrow> Inf_from N \<subseteq> Inf_from N'"
   unfolding Inf_from_def by auto
 
 lemma Inf_between_mono: "N \<subseteq> N' \<Longrightarrow> M \<subseteq> M' \<Longrightarrow> Inf_between N M \<subseteq> Inf_between N' M'"
   unfolding Inf_between_alt using Inf_from_mono[of "N \<union> M" "N' \<union> M'"] by auto
 
 end
 
 
 subsection \<open>Families of Inference Systems\<close>
 
 locale inference_system_family =
   fixes
     Q :: "'q set" and
     Inf_q :: "'q \<Rightarrow> 'f inference set"
   assumes
     Q_nonempty: "Q \<noteq> {}"
 begin
 
 definition Inf_from_q :: "'q \<Rightarrow> 'f set \<Rightarrow> 'f inference set" where
   "Inf_from_q q = inference_system.Inf_from (Inf_q q)"
 
 definition Inf_between_q :: "'q \<Rightarrow> 'f set \<Rightarrow> 'f set \<Rightarrow> 'f inference set" where
   "Inf_between_q q = inference_system.Inf_between (Inf_q q)"
 
 lemma Inf_between_q_alt:
   "Inf_between_q q N M = {\<iota> \<in> Inf_q q. \<iota> \<in> Inf_from_q q (N \<union> M) \<and> set (prems_of \<iota>) \<inter> M \<noteq> {}}"
   unfolding Inf_from_q_def Inf_between_q_def inference_system.Inf_between_alt by auto
 
 end
 
 
 subsection \<open>Calculi Based on a Single Redundancy Criterion\<close>
 
 locale calculus = inference_system Inf + consequence_relation Bot entails
   for
     Bot :: "'f set" and
     Inf :: \<open>'f inference set\<close> and
     entails :: "'f set \<Rightarrow> 'f set \<Rightarrow> bool" (infix "\<Turnstile>" 50)
   + fixes
     Red_I :: "'f set \<Rightarrow> 'f inference set" and
     Red_F :: "'f set \<Rightarrow> 'f set"
   assumes
     Red_I_to_Inf: "Red_I N \<subseteq> Inf" and
     Red_F_Bot: "B \<in> Bot \<Longrightarrow> N \<Turnstile> {B} \<Longrightarrow> N - Red_F N \<Turnstile> {B}" and
     Red_F_of_subset: "N \<subseteq> N' \<Longrightarrow> Red_F N \<subseteq> Red_F N'" and
     Red_I_of_subset: "N \<subseteq> N' \<Longrightarrow> Red_I N \<subseteq> Red_I N'" and
     Red_F_of_Red_F_subset: "N' \<subseteq> Red_F N \<Longrightarrow> Red_F N \<subseteq> Red_F (N - N')" and
     Red_I_of_Red_F_subset: "N' \<subseteq> Red_F N \<Longrightarrow> Red_I N \<subseteq> Red_I (N - N')" and
     Red_I_of_Inf_to_N: "\<iota> \<in> Inf \<Longrightarrow> concl_of \<iota> \<in> N \<Longrightarrow> \<iota> \<in> Red_I N"
 begin
 
 lemma Red_I_of_Inf_to_N_subset: "{\<iota> \<in> Inf. concl_of \<iota> \<in> N} \<subseteq> Red_I N"
   using Red_I_of_Inf_to_N by blast
 
 (* lem:red-concl-implies-red-inf *)
 lemma red_concl_to_red_inf:
   assumes
     i_in: "\<iota> \<in> Inf" and
     concl: "concl_of \<iota> \<in> Red_F N"
   shows "\<iota> \<in> Red_I N"
 proof -
   have "\<iota> \<in> Red_I (Red_F N)" by (simp add: Red_I_of_Inf_to_N i_in concl)
   then have i_in_Red: "\<iota> \<in> Red_I (N \<union> Red_F N)" by (simp add: Red_I_of_Inf_to_N concl i_in)
   have red_n_subs: "Red_F N \<subseteq> Red_F (N \<union> Red_F N)" by (simp add: Red_F_of_subset)
   then have "\<iota> \<in> Red_I ((N \<union> Red_F N) - (Red_F N - N))" using Red_I_of_Red_F_subset i_in_Red
     by (meson Diff_subset subsetCE subset_trans)
   then show ?thesis by (metis Diff_cancel Diff_subset Un_Diff Un_Diff_cancel contra_subsetD
     calculus.Red_I_of_subset calculus_axioms sup_bot.right_neutral)
 qed
 
 definition saturated :: "'f set \<Rightarrow> bool" where
   "saturated N \<longleftrightarrow> Inf_from N \<subseteq> Red_I N"
 
 definition reduc_saturated :: "'f set \<Rightarrow> bool" where
   "reduc_saturated N \<longleftrightarrow> Inf_from (N - Red_F N) \<subseteq> Red_I N"
 
 lemma Red_I_without_red_F:
   "Red_I (N - Red_F N) = Red_I N"
   using Red_I_of_subset [of "N - Red_F N" N]
     and Red_I_of_Red_F_subset [of "Red_F N" N] by blast
 
 lemma saturated_without_red_F:
   assumes saturated: "saturated N"
   shows "saturated (N - Red_F N)"
 proof -
   have "Inf_from (N - Red_F N) \<subseteq> Inf_from N" unfolding Inf_from_def by auto
   also have "Inf_from N \<subseteq> Red_I N" using saturated unfolding saturated_def by auto
   also have "Red_I N \<subseteq> Red_I (N - Red_F N)" using Red_I_of_Red_F_subset by auto
   finally have "Inf_from (N - Red_F N) \<subseteq> Red_I (N - Red_F N)" by auto
   then show ?thesis unfolding saturated_def by auto
 qed
 
 definition fair :: "'f set llist \<Rightarrow> bool" where
   "fair Ns \<longleftrightarrow> Inf_from (Liminf_llist Ns) \<subseteq> Sup_llist (lmap Red_I Ns)"
 
-inductive "derive" :: "'f set \<Rightarrow> 'f set \<Rightarrow> bool" (infix "\<rhd>Red" 50) where
-  derive: "M - N \<subseteq> Red_F N \<Longrightarrow> M \<rhd>Red N"
+inductive "derive" :: "'f set \<Rightarrow> 'f set \<Rightarrow> bool" (infix "\<rhd>" 50) where
+  derive: "M - N \<subseteq> Red_F N \<Longrightarrow> M \<rhd> N"
 
 lemma gt_Max_notin: \<open>finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> x > Max A \<Longrightarrow> x \<notin> A\<close> by auto
 
 lemma equiv_Sup_Liminf:
   assumes
     in_Sup: "C \<in> Sup_llist Ns" and
     not_in_Liminf: "C \<notin> Liminf_llist Ns"
   shows
     "\<exists>i \<in> {i. enat (Suc i) < llength Ns}. C \<in> lnth Ns i - lnth Ns (Suc i)"
 proof -
   obtain i where C_D_i: "C \<in> Sup_upto_llist Ns (enat i)" and "enat i < llength Ns"
     using elem_Sup_llist_imp_Sup_upto_llist in_Sup by fast
   then obtain j where j: "j \<ge> i \<and> enat j < llength Ns \<and> C \<notin> lnth Ns j"
     using not_in_Liminf unfolding Sup_upto_llist_def chain_def Liminf_llist_def by auto
   obtain k where k: "C \<in> lnth Ns k" "enat k < llength Ns" "k \<le> i" using C_D_i
     unfolding Sup_upto_llist_def by auto
   let ?S = "{i. i < j \<and> i \<ge> k \<and> C \<in> lnth Ns i}"
   define l where "l = Max ?S"
   have \<open>k \<in> {i. i < j \<and> k \<le> i \<and> C \<in> lnth Ns i}\<close> using k j by (auto simp: order.order_iff_strict)
   then have nempty: "{i. i < j \<and> k \<le> i \<and> C \<in> lnth Ns i} \<noteq> {}" by auto
   then have l_prop: "l < j \<and> l \<ge> k \<and> C \<in> lnth Ns l" using Max_in[of ?S, OF _ nempty]
     unfolding l_def by auto
   then have "C \<in> lnth Ns l - lnth Ns (Suc l)" using j gt_Max_notin[OF _ nempty, of "Suc l"]
     unfolding l_def[symmetric] by (auto intro: Suc_lessI)
   then show ?thesis
   proof (rule bexI[of _ l])
     show "l \<in> {i. enat (Suc i) < llength Ns}"
       using l_prop j
       by (clarify, metis Suc_leI dual_order.order_iff_strict enat_ord_simps(2) less_trans)
   qed
 qed
 
 (* lem:nonpersistent-is-redundant *)
 lemma Red_in_Sup:
-  assumes deriv: "chain (\<rhd>Red) Ns"
+  assumes deriv: "chain (\<rhd>) Ns"
   shows "Sup_llist Ns - Liminf_llist Ns \<subseteq> Red_F (Sup_llist Ns)"
 proof
   fix C
   assume C_in_subset: "C \<in> Sup_llist Ns - Liminf_llist Ns"
   {
     fix C i
     assume
       in_ith_elem: "C \<in> lnth Ns i - lnth Ns (Suc i)" and
       i: "enat (Suc i) < llength Ns"
-    have "lnth Ns i \<rhd>Red lnth Ns (Suc i)" using i deriv in_ith_elem chain_lnth_rel by auto
+    have "lnth Ns i \<rhd> lnth Ns (Suc i)" using i deriv in_ith_elem chain_lnth_rel by auto
     then have "C \<in> Red_F (lnth Ns (Suc i))" using in_ith_elem derive.cases by blast
     then have "C \<in> Red_F (Sup_llist Ns)" using Red_F_of_subset
       by (meson contra_subsetD i lnth_subset_Sup_llist)
   }
   then show "C \<in> Red_F (Sup_llist Ns)" using equiv_Sup_Liminf[of C] C_in_subset by fast
 qed
 
 (* lem:redundant-remains-redundant-during-run 1/2 *)
 lemma Red_I_subset_Liminf:
-  assumes deriv: \<open>chain (\<rhd>Red) Ns\<close> and
+  assumes deriv: \<open>chain (\<rhd>) Ns\<close> and
     i: \<open>enat i < llength Ns\<close>
   shows \<open>Red_I (lnth Ns i) \<subseteq> Red_I (Liminf_llist Ns)\<close>
 proof -
   have Sup_in_diff: \<open>Red_I (Sup_llist Ns) \<subseteq> Red_I (Sup_llist Ns - (Sup_llist Ns - Liminf_llist Ns))\<close>
     using Red_I_of_Red_F_subset[OF Red_in_Sup] deriv by auto
   also have \<open>Sup_llist Ns - (Sup_llist Ns - Liminf_llist Ns) = Liminf_llist Ns\<close>
     by (simp add: Liminf_llist_subset_Sup_llist double_diff)
   then have Red_I_Sup_in_Liminf: \<open>Red_I (Sup_llist Ns) \<subseteq> Red_I (Liminf_llist Ns)\<close>
     using Sup_in_diff by auto
   have \<open>lnth Ns i \<subseteq> Sup_llist Ns\<close> unfolding Sup_llist_def using i by blast
   then have "Red_I (lnth Ns i) \<subseteq> Red_I (Sup_llist Ns)" using Red_I_of_subset
     unfolding Sup_llist_def by auto
   then show ?thesis using Red_I_Sup_in_Liminf by auto
 qed
 
 (* lem:redundant-remains-redundant-during-run 2/2 *)
 lemma Red_F_subset_Liminf:
- assumes deriv: \<open>chain (\<rhd>Red) Ns\<close> and
+  assumes deriv: \<open>chain (\<rhd>) Ns\<close> and
     i: \<open>enat i < llength Ns\<close>
   shows \<open>Red_F (lnth Ns i) \<subseteq> Red_F (Liminf_llist Ns)\<close>
 proof -
   have Sup_in_diff: \<open>Red_F (Sup_llist Ns) \<subseteq> Red_F (Sup_llist Ns - (Sup_llist Ns - Liminf_llist Ns))\<close>
     using Red_F_of_Red_F_subset[OF Red_in_Sup] deriv by auto
   also have \<open>Sup_llist Ns - (Sup_llist Ns - Liminf_llist Ns) = Liminf_llist Ns\<close>
     by (simp add: Liminf_llist_subset_Sup_llist double_diff)
   then have Red_F_Sup_in_Liminf: \<open>Red_F (Sup_llist Ns) \<subseteq> Red_F (Liminf_llist Ns)\<close>
     using Sup_in_diff by auto
   have \<open>lnth Ns i \<subseteq> Sup_llist Ns\<close> unfolding Sup_llist_def using i by blast
   then have "Red_F (lnth Ns i) \<subseteq> Red_F (Sup_llist Ns)" using Red_F_of_subset
     unfolding Sup_llist_def by auto
   then show ?thesis using Red_F_Sup_in_Liminf by auto
 qed
 
 (* lem:N-i-is-persistent-or-redundant *)
 lemma i_in_Liminf_or_Red_F:
   assumes
-    deriv: \<open>chain (\<rhd>Red) Ns\<close> and
+    deriv: \<open>chain (\<rhd>) Ns\<close> and
     i: \<open>enat i < llength Ns\<close>
   shows \<open>lnth Ns i \<subseteq> Red_F (Liminf_llist Ns) \<union> Liminf_llist Ns\<close>
 proof (rule,rule)
   fix C
   assume C: \<open>C \<in> lnth Ns i\<close>
   and C_not_Liminf: \<open>C \<notin> Liminf_llist Ns\<close>
   have \<open>C \<in> Sup_llist Ns\<close> unfolding Sup_llist_def using C i by auto
   then obtain j where j: \<open>C \<in> lnth Ns j - lnth Ns (Suc j)\<close> \<open>enat (Suc j) < llength Ns\<close>
     using equiv_Sup_Liminf[of C Ns] C_not_Liminf by auto
   then have \<open>C \<in> Red_F (lnth Ns (Suc j))\<close>
     using deriv by (meson chain_lnth_rel contra_subsetD derive.cases)
   then show \<open>C \<in> Red_F (Liminf_llist Ns)\<close> using Red_F_subset_Liminf[of Ns "Suc j"] deriv j(2) by blast
 qed
 
 (* lem:fairness-implies-saturation *)
 lemma fair_implies_Liminf_saturated:
   assumes
-    deriv: \<open>chain (\<rhd>Red) Ns\<close> and
+    deriv: \<open>chain (\<rhd>) Ns\<close> and
     fair: \<open>fair Ns\<close>
   shows \<open>saturated (Liminf_llist Ns)\<close>
   unfolding saturated_def
 proof
   fix \<iota>
   assume \<iota>: \<open>\<iota> \<in> Inf_from (Liminf_llist Ns)\<close>
   have \<open>\<iota> \<in> Sup_llist (lmap Red_I Ns)\<close> using fair \<iota> unfolding fair_def by auto
   then obtain i where i: \<open>enat i < llength Ns\<close> \<open>\<iota> \<in> Red_I (lnth Ns i)\<close>
     unfolding Sup_llist_def by auto
   then show \<open>\<iota> \<in> Red_I (Liminf_llist Ns)\<close>
     using deriv i_in_Liminf_or_Red_F[of Ns i] Red_I_subset_Liminf by blast
 qed
 
 end
 
 locale statically_complete_calculus = calculus +
   assumes statically_complete: "B \<in> Bot \<Longrightarrow> saturated N \<Longrightarrow> N \<Turnstile> {B} \<Longrightarrow> \<exists>B'\<in>Bot. B' \<in> N"
 begin
 
 lemma dynamically_complete_Liminf:
   fixes B Ns
   assumes
     bot_elem: \<open>B \<in> Bot\<close> and
-    deriv: \<open>chain (\<rhd>Red) Ns\<close> and
+    deriv: \<open>chain (\<rhd>) Ns\<close> and
     fair: \<open>fair Ns\<close> and
     unsat: \<open>lhd Ns \<Turnstile> {B}\<close>
   shows \<open>\<exists>B'\<in>Bot. B' \<in> Liminf_llist Ns\<close>
 proof -
   note lhd_is = lhd_conv_lnth[OF chain_not_lnull[OF deriv]]
   have non_empty: \<open>\<not> lnull Ns\<close> using chain_not_lnull[OF deriv] .
   have subs: \<open>lhd Ns \<subseteq> Sup_llist Ns\<close>
     using lhd_subset_Sup_llist[of Ns] non_empty by (simp add: lhd_conv_lnth)
   have \<open>Sup_llist Ns \<Turnstile> {B}\<close>
     using unsat subset_entailed[OF subs] entails_trans[of "Sup_llist Ns" "lhd Ns"] by auto
   then have Sup_no_Red: \<open>Sup_llist Ns - Red_F (Sup_llist Ns) \<Turnstile> {B}\<close>
     using bot_elem Red_F_Bot by auto
   have Sup_no_Red_in_Liminf: \<open>Sup_llist Ns - Red_F (Sup_llist Ns) \<subseteq> Liminf_llist Ns\<close>
     using deriv Red_in_Sup by auto
   have Liminf_entails_Bot: \<open>Liminf_llist Ns \<Turnstile> {B}\<close>
     using Sup_no_Red subset_entailed[OF Sup_no_Red_in_Liminf] entails_trans by blast
   have \<open>saturated (Liminf_llist Ns)\<close>
     using deriv fair fair_implies_Liminf_saturated unfolding saturated_def by auto
   then show ?thesis
     using bot_elem statically_complete Liminf_entails_Bot by auto
 qed
 
 end
 
 locale dynamically_complete_calculus = calculus +
   assumes
-    dynamically_complete: "B \<in> Bot \<Longrightarrow> chain (\<rhd>Red) Ns \<Longrightarrow> fair Ns \<Longrightarrow> lhd Ns \<Turnstile> {B} \<Longrightarrow>
+    dynamically_complete: "B \<in> Bot \<Longrightarrow> chain (\<rhd>) Ns \<Longrightarrow> fair Ns \<Longrightarrow> lhd Ns \<Turnstile> {B} \<Longrightarrow>
       \<exists>i \<in> {i. enat i < llength Ns}. \<exists>B'\<in>Bot. B' \<in> lnth Ns i"
 begin
 
 (* lem:dynamic-ref-compl-implies-static *)
 sublocale statically_complete_calculus
 proof
   fix B N
   assume
     bot_elem: \<open>B \<in> Bot\<close> and
     saturated_N: "saturated N" and
     refut_N: "N \<Turnstile> {B}"
   define Ns where "Ns = LCons N LNil"
   have[simp]: \<open>\<not> lnull Ns\<close> by (auto simp: Ns_def)
-  have deriv_Ns: \<open>chain (\<rhd>Red) Ns\<close> by (simp add: chain.chain_singleton Ns_def)
+  have deriv_Ns: \<open>chain (\<rhd>) Ns\<close> by (simp add: chain.chain_singleton Ns_def)
   have liminf_is_N: "Liminf_llist Ns = N" by (simp add: Ns_def Liminf_llist_LCons)
   have head_Ns: "N = lhd Ns" by (simp add: Ns_def)
   have "Sup_llist (lmap Red_I Ns) = Red_I N" by (simp add: Ns_def)
   then have fair_Ns: "fair Ns" using saturated_N by (simp add: fair_def saturated_def liminf_is_N)
   obtain i B' where B'_is_bot: \<open>B' \<in> Bot\<close> and B'_in: "B' \<in> lnth Ns i" and \<open>i < llength Ns\<close>
     using dynamically_complete[of B Ns] bot_elem fair_Ns head_Ns saturated_N deriv_Ns refut_N
     by auto
   then have "i = 0"
     by (auto simp: Ns_def enat_0_iff)
   show \<open>\<exists>B'\<in>Bot. B' \<in> N\<close>
     using B'_is_bot B'_in unfolding \<open>i = 0\<close> head_Ns[symmetric] Ns_def by auto
 qed
 
 end
 
 (* lem:static-ref-compl-implies-dynamic *)
 sublocale statically_complete_calculus \<subseteq> dynamically_complete_calculus
 proof
   fix B Ns
   assume
     \<open>B \<in> Bot\<close> and
-    \<open>chain (\<rhd>Red) Ns\<close> and
+    \<open>chain (\<rhd>) Ns\<close> and
     \<open>fair Ns\<close> and
     \<open>lhd Ns \<Turnstile> {B}\<close>
   then have \<open>\<exists>B'\<in>Bot. B' \<in> Liminf_llist Ns\<close>
     by (rule dynamically_complete_Liminf)
   then show \<open>\<exists>i\<in>{i. enat i < llength Ns}. \<exists>B'\<in>Bot. B' \<in> lnth Ns i\<close>
     unfolding Liminf_llist_def by auto
 qed
 
 end
diff --git a/thys/Saturation_Framework/Calculus_Variations.thy b/thys/Saturation_Framework/Calculus_Variations.thy
--- a/thys/Saturation_Framework/Calculus_Variations.thy
+++ b/thys/Saturation_Framework/Calculus_Variations.thy
@@ -1,435 +1,435 @@
 (*  Title:       Variations on a Theme
  *  Author:      Sophie Tourret <stourret at mpi-inf.mpg.de>, 2018-2020 *)
 
 section \<open>Variations on a Theme\<close>
 
 text \<open>In this section, section 2.4 of the report is covered, demonstrating
   that various notions of redundancy are equivalent.\<close>
 
 theory Calculus_Variations
   imports Calculus
 begin
 
 locale reduced_calculus = calculus Bot Inf entails Red_I Red_F
   for
     Bot :: "'f set" and
     Inf :: \<open>'f inference set\<close> and
     entails :: "'f set \<Rightarrow> 'f set \<Rightarrow> bool" (infix "\<Turnstile>" 50) and
     Red_I :: "'f set \<Rightarrow> 'f inference set" and
     Red_F :: "'f set \<Rightarrow> 'f set"
  + assumes
    inf_in_red_inf: "Inf_between UNIV (Red_F N) \<subseteq> Red_I N"
 begin
 
 (* lem:reduced-rc-implies-sat-equiv-reduced-sat *)
 lemma sat_eq_reduc_sat: "saturated N \<longleftrightarrow> reduc_saturated N"
 proof
   fix N
   assume "saturated N"
   then show "reduc_saturated N"
     using Red_I_without_red_F saturated_without_red_F
     unfolding saturated_def reduc_saturated_def
     by blast
 next
   fix N
   assume red_sat_n: "reduc_saturated N"
   show "saturated N" unfolding saturated_def
     using red_sat_n inf_in_red_inf unfolding reduc_saturated_def Inf_from_def Inf_between_def
     by blast
 qed
 
 end
 
 locale reducedly_statically_complete_calculus = calculus +
   assumes reducedly_statically_complete:
     "B \<in> Bot \<Longrightarrow> reduc_saturated N \<Longrightarrow> N \<Turnstile> {B} \<Longrightarrow> \<exists>B'\<in>Bot. B' \<in> N"
 
 locale reducedly_statically_complete_reduced_calculus = reduced_calculus +
   assumes reducedly_statically_complete:
     "B \<in> Bot \<Longrightarrow> reduc_saturated N \<Longrightarrow> N \<Turnstile> {B} \<Longrightarrow> \<exists>B'\<in>Bot. B' \<in> N"
 begin
 
 sublocale reducedly_statically_complete_calculus
   by (simp add: calculus_axioms reducedly_statically_complete
     reducedly_statically_complete_calculus_axioms.intro
     reducedly_statically_complete_calculus_def)
 
 (* cor:reduced-rc-implies-st-ref-comp-equiv-reduced-st-ref-comp 1/2 *)
 sublocale statically_complete_calculus
 proof
   fix B N
   assume
     bot_elem: \<open>B \<in> Bot\<close> and
     saturated_N: "saturated N" and
     refut_N: "N \<Turnstile> {B}"
   have reduc_saturated_N: "reduc_saturated N" using saturated_N sat_eq_reduc_sat by blast
   show "\<exists>B'\<in>Bot. B' \<in> N" using reducedly_statically_complete[OF bot_elem reduc_saturated_N refut_N] .
 qed
 
 end
 
 context reduced_calculus
 begin
 
 (* cor:reduced-rc-implies-st-ref-comp-equiv-reduced-st-ref-comp 2/2 *)
 lemma stat_ref_comp_imp_red_stat_ref_comp:
   "statically_complete_calculus Bot Inf entails Red_I Red_F \<Longrightarrow>
    reducedly_statically_complete_calculus Bot Inf entails Red_I Red_F"
 proof
   fix B N
   assume
     stat_ref_comp: "statically_complete_calculus Bot Inf (\<Turnstile>) Red_I Red_F" and
     bot_elem: \<open>B \<in> Bot\<close> and
     saturated_N: "reduc_saturated N" and
     refut_N: "N \<Turnstile> {B}"
   have reduc_saturated_N: "saturated N" using saturated_N sat_eq_reduc_sat by blast
   show "\<exists>B'\<in>Bot. B' \<in> N"
     using statically_complete_calculus.statically_complete[OF stat_ref_comp
       bot_elem reduc_saturated_N refut_N] .
 qed
 
 end
 
 context calculus
 begin
 
 definition Red_Red_I :: "'f set \<Rightarrow> 'f inference set" where
   "Red_Red_I N = Red_I N \<union> Inf_between UNIV (Red_F N)"
 
 lemma reduced_calc_is_calc: "calculus Bot Inf entails Red_Red_I Red_F"
 proof
   fix N
   show "Red_Red_I N \<subseteq> Inf"
     unfolding Red_Red_I_def Inf_between_def Inf_from_def using Red_I_to_Inf by auto
 next
   fix B N
   assume
     b_in: "B \<in> Bot" and
     n_entails: "N \<Turnstile> {B}"
   show "N - Red_F N \<Turnstile> {B}"
     by (simp add: Red_F_Bot b_in n_entails)
 next
   fix N N' :: "'f set"
   assume "N \<subseteq> N'"
   then show "Red_F N \<subseteq> Red_F N'" by (simp add: Red_F_of_subset)
 next
   fix N N' :: "'f set"
   assume n_in: "N \<subseteq> N'"
   then have "Inf_from (UNIV - (Red_F N')) \<subseteq> Inf_from (UNIV - (Red_F N))"
     using Red_F_of_subset[OF n_in] unfolding Inf_from_def by auto
   then have "Inf_between UNIV (Red_F N) \<subseteq> Inf_between UNIV (Red_F N')"
     unfolding Inf_between_def by auto
   then show "Red_Red_I N \<subseteq> Red_Red_I N'"
     unfolding Red_Red_I_def using Red_I_of_subset[OF n_in] by blast
 next
   fix N N' :: "'f set"
   assume "N' \<subseteq> Red_F N"
   then show "Red_F N \<subseteq> Red_F (N - N')" by (simp add: Red_F_of_Red_F_subset)
 next
   fix N N' :: "'f set"
   assume np_subs: "N' \<subseteq> Red_F N"
   have "Red_F N \<subseteq> Red_F (N - N')" by (simp add: Red_F_of_Red_F_subset np_subs)
   then have "Inf_from (UNIV - (Red_F (N - N'))) \<subseteq> Inf_from (UNIV - (Red_F N))"
     by (metis Diff_subset Red_F_of_subset eq_iff)
   then have "Inf_between UNIV (Red_F N) \<subseteq> Inf_between UNIV (Red_F (N - N'))"
     unfolding Inf_between_def by auto
   then show "Red_Red_I N \<subseteq> Red_Red_I (N - N')"
     unfolding Red_Red_I_def using Red_I_of_Red_F_subset[OF np_subs] by blast
 next
   fix \<iota> N
   assume "\<iota> \<in> Inf"
     "concl_of \<iota> \<in> N"
   then show "\<iota> \<in> Red_Red_I N"
     by (simp add: Red_I_of_Inf_to_N Red_Red_I_def)
 qed
 
 lemma inf_subs_reduced_red_inf: "Inf_between UNIV (Red_F N) \<subseteq> Red_Red_I N"
   unfolding Red_Red_I_def by simp
 
 (* lem:red'-is-reduced-redcrit *)
 text \<open>The following is a lemma and not a sublocale as was previously used in similar cases.
   Here, a sublocale cannot be used because it would create an infinitely descending
   chain of sublocales. \<close>
 lemma reduc_calc: "reduced_calculus Bot Inf entails Red_Red_I Red_F"
   using inf_subs_reduced_red_inf reduced_calc_is_calc
   by (simp add: reduced_calculus.intro reduced_calculus_axioms_def)
 
 interpretation reduc_calc: reduced_calculus Bot Inf entails Red_Red_I Red_F
   by (fact reduc_calc)
 
 (* lem:saturation-red-vs-red'-1 *)
 lemma sat_imp_red_calc_sat: "saturated N \<Longrightarrow> reduc_calc.saturated N"
   unfolding saturated_def reduc_calc.saturated_def Red_Red_I_def by blast
 
 (* lem:saturation-red-vs-red'-2 1/2 (i) \<longleftrightarrow> (ii) *)
 lemma red_sat_eq_red_calc_sat: "reduc_saturated N \<longleftrightarrow> reduc_calc.saturated N"
 proof
   assume red_sat_n: "reduc_saturated N"
   show "reduc_calc.saturated N"
     unfolding reduc_calc.saturated_def
   proof
     fix \<iota>
     assume i_in: "\<iota> \<in> Inf_from N"
     show "\<iota> \<in> Red_Red_I N"
       using i_in red_sat_n
       unfolding reduc_saturated_def Inf_between_def Inf_from_def Red_Red_I_def by blast
   qed
 next
   assume red_sat_n: "reduc_calc.saturated N"
   show "reduc_saturated N"
     unfolding reduc_saturated_def
   proof
     fix \<iota>
     assume i_in: "\<iota> \<in> Inf_from (N - Red_F N)"
     show "\<iota> \<in> Red_I N"
       using i_in red_sat_n
       unfolding Inf_from_def reduc_calc.saturated_def Red_Red_I_def Inf_between_def by blast
   qed
 qed
 
 (* lem:saturation-red-vs-red'-2 2/2 (i) \<longleftrightarrow> (iii) *)
 lemma red_sat_eq_sat: "reduc_saturated N \<longleftrightarrow> saturated (N - Red_F N)"
   unfolding reduc_saturated_def saturated_def by (simp add: Red_I_without_red_F)
 
 (* thm:reduced-stat-ref-compl 1/3 (i) \<longleftrightarrow> (iii) *)
 theorem stat_is_stat_red: "statically_complete_calculus Bot Inf entails Red_I Red_F \<longleftrightarrow>
   statically_complete_calculus Bot Inf entails Red_Red_I Red_F"
 proof
   assume
     stat_ref1: "statically_complete_calculus Bot Inf entails Red_I Red_F"
   show "statically_complete_calculus Bot Inf entails Red_Red_I Red_F"
     using reduc_calc.calculus_axioms
     unfolding statically_complete_calculus_def statically_complete_calculus_axioms_def
   proof
     show "\<forall>B N. B \<in> Bot \<longrightarrow> reduc_calc.saturated N \<longrightarrow> N \<Turnstile> {B} \<longrightarrow> (\<exists>B'\<in>Bot. B' \<in> N)"
     proof (clarify)
       fix B N
       assume
         b_in: "B \<in> Bot" and
         n_sat: "reduc_calc.saturated N" and
         n_imp_b: "N \<Turnstile> {B}"
       have "saturated (N - Red_F N)" using red_sat_eq_red_calc_sat[of N] red_sat_eq_sat[of N] n_sat by blast
       moreover have "(N - Red_F N) \<Turnstile> {B}" using n_imp_b b_in by (simp add: reduc_calc.Red_F_Bot)
       ultimately show "\<exists>B'\<in>Bot. B'\<in> N"
         using stat_ref1 by (meson DiffD1 b_in statically_complete_calculus.statically_complete)
     qed
   qed
 next
   assume
     stat_ref3: "statically_complete_calculus Bot Inf entails Red_Red_I Red_F"
   show "statically_complete_calculus Bot Inf entails Red_I Red_F"
     unfolding statically_complete_calculus_def statically_complete_calculus_axioms_def
     using calculus_axioms
   proof
     show "\<forall>B N. B \<in> Bot \<longrightarrow> saturated N \<longrightarrow> N \<Turnstile> {B} \<longrightarrow> (\<exists>B'\<in>Bot. B' \<in> N)"
     proof clarify
       fix B N
       assume
         b_in: "B \<in> Bot" and
         n_sat: "saturated N" and
         n_imp_b: "N \<Turnstile> {B}"
       then show "\<exists>B'\<in> Bot. B' \<in> N"
         using stat_ref3 sat_imp_red_calc_sat[OF n_sat]
         by (meson statically_complete_calculus.statically_complete)
     qed
   qed
 qed
 
 (* thm:reduced-stat-ref-compl 2/3 (iv) \<longleftrightarrow> (iii) *)
 theorem red_stat_red_is_stat_red:
   "reducedly_statically_complete_calculus Bot Inf entails Red_Red_I Red_F \<longleftrightarrow>
    statically_complete_calculus Bot Inf entails Red_Red_I Red_F"
   using reduc_calc.stat_ref_comp_imp_red_stat_ref_comp
   by (metis reduc_calc.sat_eq_reduc_sat reducedly_statically_complete_calculus.axioms(2)
     reducedly_statically_complete_calculus_axioms_def reduced_calc_is_calc
     statically_complete_calculus.intro statically_complete_calculus_axioms.intro)
 
 (* thm:reduced-stat-ref-compl 3/3 (ii) \<longleftrightarrow> (iii) *)
 theorem red_stat_is_stat_red:
   "reducedly_statically_complete_calculus Bot Inf entails Red_I Red_F \<longleftrightarrow>
    statically_complete_calculus Bot Inf entails Red_Red_I Red_F"
   using reduc_calc.calculus_axioms calculus_axioms red_sat_eq_red_calc_sat
   unfolding statically_complete_calculus_def statically_complete_calculus_axioms_def
     reducedly_statically_complete_calculus_def reducedly_statically_complete_calculus_axioms_def
   by blast
 
 lemma sup_red_f_in_red_liminf:
   "chain derive Ns \<Longrightarrow> Sup_llist (lmap Red_F Ns) \<subseteq> Red_F (Liminf_llist Ns)"
 proof
   fix N
   assume
     deriv: "chain derive Ns" and
     n_in_sup: "N \<in> Sup_llist (lmap Red_F Ns)"
   obtain i0 where i_smaller: "enat i0 < llength Ns" and n_in: "N \<in> Red_F (lnth Ns i0)"
     using n_in_sup by (metis Sup_llist_imp_exists_index llength_lmap lnth_lmap)
   have "Red_F (lnth Ns i0) \<subseteq> Red_F (Liminf_llist Ns)"
     using i_smaller by (simp add: deriv Red_F_subset_Liminf)
   then show "N \<in> Red_F (Liminf_llist Ns)"
     using n_in by fast
 qed
 
 lemma sup_red_inf_in_red_liminf:
   "chain derive Ns \<Longrightarrow> Sup_llist (lmap Red_I Ns) \<subseteq> Red_I (Liminf_llist Ns)"
 proof
   fix \<iota>
   assume
     deriv: "chain derive Ns" and
     i_in_sup: "\<iota> \<in> Sup_llist (lmap Red_I Ns)"
   obtain i0 where i_smaller: "enat i0 < llength Ns" and n_in: "\<iota> \<in> Red_I (lnth Ns i0)"
     using i_in_sup unfolding Sup_llist_def by auto
   have "Red_I (lnth Ns i0) \<subseteq> Red_I (Liminf_llist Ns)"
     using i_smaller by (simp add: deriv Red_I_subset_Liminf)
   then show "\<iota> \<in> Red_I (Liminf_llist Ns)"
     using n_in by fast
 qed
 
 definition reduc_fair :: "'f set llist \<Rightarrow> bool" where
   "reduc_fair Ns \<longleftrightarrow>
    Inf_from (Liminf_llist Ns - Sup_llist (lmap Red_F Ns)) \<subseteq> Sup_llist (lmap Red_I Ns)"
 
 (* lem:red-fairness-implies-red-saturation *)
 lemma reduc_fair_imp_Liminf_reduc_sat:
   "chain derive Ns \<Longrightarrow> reduc_fair Ns \<Longrightarrow> reduc_saturated (Liminf_llist Ns)"
   unfolding reduc_saturated_def
 proof -
   fix Ns
   assume
     deriv: "chain derive Ns" and
     red_fair: "reduc_fair Ns"
   have "Inf_from (Liminf_llist Ns - Red_F (Liminf_llist Ns))
     \<subseteq> Inf_from (Liminf_llist Ns - Sup_llist (lmap Red_F Ns))"
     using sup_red_f_in_red_liminf[OF deriv] unfolding Inf_from_def by blast
   then have "Inf_from (Liminf_llist Ns - Red_F (Liminf_llist Ns)) \<subseteq> Sup_llist (lmap Red_I Ns)"
     using red_fair unfolding reduc_fair_def by simp
   then show "Inf_from (Liminf_llist Ns - Red_F (Liminf_llist Ns)) \<subseteq> Red_I (Liminf_llist Ns)"
     using sup_red_inf_in_red_liminf[OF deriv] by fast
 qed
 
 end
 
 locale reducedly_dynamically_complete_calculus = calculus +
   assumes
     reducedly_dynamically_complete: "B \<in> Bot \<Longrightarrow> chain derive Ns \<Longrightarrow> reduc_fair Ns \<Longrightarrow>
       lhd Ns \<Turnstile> {B} \<Longrightarrow> \<exists>i \<in> {i. enat i < llength Ns}. \<exists> B'\<in>Bot. B' \<in> lnth Ns i"
 begin
 
 sublocale reducedly_statically_complete_calculus
 proof
   fix B N
   assume
     bot_elem: \<open>B \<in> Bot\<close> and
     saturated_N: "reduc_saturated N" and
     refut_N: "N \<Turnstile> {B}"
   define Ns where "Ns = LCons N LNil"
   have[simp]: \<open>\<not> lnull Ns\<close> by (auto simp: Ns_def)
-  have deriv_D: \<open>chain (\<rhd>Red) Ns\<close> by (simp add: chain.chain_singleton Ns_def)
+  have deriv_D: \<open>chain (\<rhd>) Ns\<close> by (simp add: chain.chain_singleton Ns_def)
   have liminf_is_N: "Liminf_llist Ns = N" by (simp add: Ns_def Liminf_llist_LCons)
   have head_D: "N = lhd Ns" by (simp add: Ns_def)
   have "Sup_llist (lmap Red_F Ns) = Red_F N" by (simp add: Ns_def)
   moreover have "Sup_llist (lmap Red_I Ns) = Red_I N" by (simp add: Ns_def)
   ultimately have fair_D: "reduc_fair Ns"
     using saturated_N liminf_is_N unfolding reduc_fair_def reduc_saturated_def
     by (simp add: reduc_fair_def reduc_saturated_def liminf_is_N)
   obtain i B' where B'_is_bot: \<open>B' \<in> Bot\<close> and B'_in: "B' \<in> lnth Ns i" and \<open>i < llength Ns\<close>
     using reducedly_dynamically_complete[of B Ns] bot_elem fair_D head_D saturated_N deriv_D refut_N
     by auto
   then have "i = 0"
     by (auto simp: Ns_def enat_0_iff)
   show \<open>\<exists>B'\<in>Bot. B' \<in> N\<close>
     using B'_is_bot B'_in unfolding \<open>i = 0\<close> head_D[symmetric] Ns_def by auto
 qed
 
 end
 
 sublocale reducedly_statically_complete_calculus \<subseteq> reducedly_dynamically_complete_calculus
 proof
   fix B Ns
   assume
     bot_elem: \<open>B \<in> Bot\<close> and
-    deriv: \<open>chain (\<rhd>Red) Ns\<close> and
+    deriv: \<open>chain (\<rhd>) Ns\<close> and
     fair: \<open>reduc_fair Ns\<close> and
     unsat: \<open>lhd Ns \<Turnstile> {B}\<close>
     have non_empty: \<open>\<not> lnull Ns\<close> using chain_not_lnull[OF deriv] .
     have subs: \<open>lhd Ns \<subseteq> Sup_llist Ns\<close>
       using lhd_subset_Sup_llist[of Ns] non_empty by (simp add: lhd_conv_lnth)
     have \<open>Sup_llist Ns \<Turnstile> {B}\<close>
       using unsat subset_entailed[OF subs] entails_trans[of "Sup_llist Ns" "lhd Ns"] by auto
     then have Sup_no_Red: \<open>Sup_llist Ns - Red_F (Sup_llist Ns) \<Turnstile> {B}\<close>
       using bot_elem Red_F_Bot by auto
     have Sup_no_Red_in_Liminf: \<open>Sup_llist Ns - Red_F (Sup_llist Ns) \<subseteq> Liminf_llist Ns\<close>
       using deriv Red_in_Sup by auto
     have Liminf_entails_Bot: \<open>Liminf_llist Ns \<Turnstile> {B}\<close>
       using Sup_no_Red subset_entailed[OF Sup_no_Red_in_Liminf] entails_trans by blast
     have \<open>reduc_saturated (Liminf_llist Ns)\<close>
     using deriv fair reduc_fair_imp_Liminf_reduc_sat unfolding reduc_saturated_def
       by auto
    then have \<open>\<exists>B'\<in>Bot. B' \<in> Liminf_llist Ns\<close>
      using bot_elem reducedly_statically_complete Liminf_entails_Bot
      by auto
    then show \<open>\<exists>i\<in>{i. enat i < llength Ns}. \<exists>B'\<in>Bot. B' \<in> lnth Ns i\<close>
      unfolding Liminf_llist_def by auto
 qed
 
 context calculus
 begin
 
 lemma dyn_equiv_stat: "dynamically_complete_calculus Bot Inf entails Red_I Red_F =
   statically_complete_calculus Bot Inf entails Red_I Red_F"
 proof
   assume "dynamically_complete_calculus Bot Inf entails Red_I Red_F"
   then interpret dynamically_complete_calculus Bot Inf entails Red_I Red_F
     by simp
   show "statically_complete_calculus Bot Inf entails Red_I Red_F"
     by (simp add: statically_complete_calculus_axioms)
 next
   assume "statically_complete_calculus Bot Inf entails Red_I Red_F"
   then interpret statically_complete_calculus Bot Inf entails Red_I Red_F
     by simp
   show "dynamically_complete_calculus Bot Inf entails Red_I Red_F"
     by (simp add: dynamically_complete_calculus_axioms)
 qed
 
 lemma red_dyn_equiv_red_stat:
   "reducedly_dynamically_complete_calculus Bot Inf entails Red_I Red_F =
    reducedly_statically_complete_calculus Bot Inf entails Red_I Red_F"
 proof
   assume "reducedly_dynamically_complete_calculus Bot Inf entails Red_I Red_F"
   then interpret reducedly_dynamically_complete_calculus Bot Inf entails Red_I Red_F
     by simp
   show "reducedly_statically_complete_calculus Bot Inf entails Red_I Red_F"
     by (simp add: reducedly_statically_complete_calculus_axioms)
 next
   assume "reducedly_statically_complete_calculus Bot Inf entails Red_I Red_F"
   then interpret reducedly_statically_complete_calculus Bot Inf entails Red_I Red_F
     by simp
   show "reducedly_dynamically_complete_calculus Bot Inf entails Red_I Red_F"
     by (simp add: reducedly_dynamically_complete_calculus_axioms)
 qed
 
 interpretation reduc_calc: reduced_calculus Bot Inf entails Red_Red_I Red_F
   by (fact reduc_calc)
 
 (* thm:reduced-dyn-ref-compl 1/3 (v) \<longleftrightarrow> (vii) *)
 theorem dyn_ref_eq_dyn_ref_red:
   "dynamically_complete_calculus Bot Inf entails Red_I Red_F \<longleftrightarrow>
    dynamically_complete_calculus Bot Inf entails Red_Red_I Red_F"
   using dyn_equiv_stat stat_is_stat_red reduc_calc.dyn_equiv_stat by meson
 
 (* thm:reduced-dyn-ref-compl 2/3 (viii) \<longleftrightarrow> (vii) *)
 theorem red_dyn_ref_red_eq_dyn_ref_red:
   "reducedly_dynamically_complete_calculus Bot Inf entails Red_Red_I Red_F \<longleftrightarrow>
    dynamically_complete_calculus Bot Inf entails Red_Red_I Red_F"
   using red_dyn_equiv_red_stat dyn_equiv_stat red_stat_red_is_stat_red
   by (simp add: reduc_calc.dyn_equiv_stat reduc_calc.red_dyn_equiv_red_stat)
 
 (* thm:reduced-dyn-ref-compl 3/3 (vi) \<longleftrightarrow> (vii) *)
 theorem red_dyn_ref_eq_dyn_ref_red:
   "reducedly_dynamically_complete_calculus Bot Inf entails Red_I Red_F \<longleftrightarrow>
    dynamically_complete_calculus Bot Inf entails Red_Red_I Red_F"
   using red_dyn_equiv_red_stat dyn_equiv_stat red_stat_is_stat_red
     reduc_calc.dyn_equiv_stat reduc_calc.red_dyn_equiv_red_stat
   by blast
 
 end
 
 end
diff --git a/thys/Saturation_Framework/Given_Clause_Architectures.thy b/thys/Saturation_Framework/Given_Clause_Architectures.thy
--- a/thys/Saturation_Framework/Given_Clause_Architectures.thy
+++ b/thys/Saturation_Framework/Given_Clause_Architectures.thy
@@ -1,1174 +1,1174 @@
 (*  Title:       Given Clause Prover Architectures
  *  Author:      Sophie Tourret <stourret at mpi-inf.mpg.de>, 2019-2020 *)
 
 section \<open>Given Clause Prover Architectures\<close>
 
 text \<open>This section covers all the results presented in the section 4 of the report.
   This is where abstract architectures of provers are defined and proven
   dynamically refutationally complete.\<close>
 
 theory Given_Clause_Architectures
   imports
     Lambda_Free_RPOs.Lambda_Free_Util
     Labeled_Lifting_to_Non_Ground_Calculi
 begin
 
 
 subsection \<open>Basis of the Given Clause Prover Architectures\<close>
 
 locale given_clause_basis = std?: labeled_lifting_intersection Bot_F Inf_F Bot_G Q
   entails_q Inf_G_q Red_I_q Red_F_q \<G>_F_q \<G>_I_q Inf_FL
   for
     Bot_F :: "'f set"
     and Inf_F :: "'f inference set"
     and Bot_G :: "'g set"
     and Q :: "'q set"
     and entails_q :: "'q \<Rightarrow> 'g set \<Rightarrow> 'g set \<Rightarrow> bool"
     and Inf_G_q :: \<open>'q \<Rightarrow> 'g inference set\<close>
     and Red_I_q :: "'q \<Rightarrow> 'g set \<Rightarrow> 'g inference set"
     and Red_F_q :: "'q \<Rightarrow> 'g set \<Rightarrow> 'g set"
     and \<G>_F_q :: "'q \<Rightarrow> 'f \<Rightarrow> 'g set"
     and \<G>_I_q :: "'q \<Rightarrow> 'f inference \<Rightarrow> 'g inference set option"
     and Inf_FL :: \<open>('f \<times> 'l) inference set\<close>
   + fixes
     Equiv_F :: "'f \<Rightarrow> 'f \<Rightarrow> bool" (infix "\<doteq>" 50) and
     Prec_F :: "'f \<Rightarrow> 'f \<Rightarrow> bool" (infix "\<prec>\<cdot>" 50) and
     Prec_l :: "'l \<Rightarrow> 'l \<Rightarrow> bool" (infix "\<sqsubset>l" 50) and
     active :: "'l"
   assumes
     equiv_equiv_F: "equivp (\<doteq>)" and
     wf_prec_F: "minimal_element (\<prec>\<cdot>) UNIV" and
     wf_prec_l: "minimal_element (\<sqsubset>l) UNIV" and
     compat_equiv_prec: "C1 \<doteq> D1 \<Longrightarrow> C2 \<doteq> D2 \<Longrightarrow> C1 \<prec>\<cdot> C2 \<Longrightarrow> D1 \<prec>\<cdot> D2" and
     equiv_F_grounding: "q \<in> Q \<Longrightarrow> C1 \<doteq> C2 \<Longrightarrow> \<G>_F_q q C1 \<subseteq> \<G>_F_q q C2" and
     prec_F_grounding: "q \<in> Q \<Longrightarrow> C2 \<prec>\<cdot> C1 \<Longrightarrow> \<G>_F_q q C1 \<subseteq> \<G>_F_q q C2" and
     active_minimal: "l2 \<noteq> active \<Longrightarrow> active \<sqsubset>l l2" and
     at_least_two_labels: "\<exists>l2. active \<sqsubset>l l2" and
     inf_never_active: "\<iota> \<in> Inf_FL \<Longrightarrow> snd (concl_of \<iota>) \<noteq> active" and
     static_ref_comp: "statically_complete_calculus Bot_F Inf_F (\<Turnstile>\<inter>\<G>)
       no_labels.Red_I_\<G> no_labels.Red_F_\<G>_empty"
 begin
 
 abbreviation Prec_eq_F :: "'f \<Rightarrow> 'f \<Rightarrow> bool" (infix "\<preceq>\<cdot>" 50) where
   "C \<preceq>\<cdot> D \<equiv> C \<doteq> D \<or> C \<prec>\<cdot> D"
 
 definition Prec_FL :: "('f \<times> 'l) \<Rightarrow> ('f \<times> 'l) \<Rightarrow> bool" (infix "\<sqsubset>" 50) where
   "Cl1 \<sqsubset> Cl2 \<longleftrightarrow> fst Cl1 \<prec>\<cdot> fst Cl2 \<or> (fst Cl1 \<doteq> fst Cl2 \<and> snd Cl1 \<sqsubset>l snd Cl2)"
 
 lemma irrefl_prec_F: "\<not> C \<prec>\<cdot> C"
   by (simp add: minimal_element.po[OF wf_prec_F, unfolded po_on_def irreflp_on_def])
 
 lemma trans_prec_F: "C1 \<prec>\<cdot> C2 \<Longrightarrow> C2 \<prec>\<cdot> C3 \<Longrightarrow> C1 \<prec>\<cdot> C3"
   by (auto intro: minimal_element.po[OF wf_prec_F, unfolded po_on_def transp_on_def, THEN conjunct2,
         simplified, rule_format])
 
 lemma wf_prec_FL: "minimal_element (\<sqsubset>) UNIV"
 proof
   show "po_on (\<sqsubset>) UNIV" unfolding po_on_def
   proof
     show "irreflp_on (\<sqsubset>) UNIV" unfolding irreflp_on_def Prec_FL_def
     proof
       fix Cl
       assume a_in: "Cl \<in> (UNIV::('f \<times> 'l) set)"
       have "\<not> (fst Cl \<prec>\<cdot> fst Cl)" using wf_prec_F minimal_element.min_elt_ex by force
       moreover have "\<not> (snd Cl \<sqsubset>l snd Cl)" using wf_prec_l minimal_element.min_elt_ex by force
       ultimately show "\<not> (fst Cl \<prec>\<cdot> fst Cl \<or> fst Cl \<doteq> fst Cl \<and> snd Cl \<sqsubset>l snd Cl)" by blast
     qed
   next
     show "transp_on (\<sqsubset>) UNIV" unfolding transp_on_def Prec_FL_def
     proof (simp, intro allI impI)
       fix C1 l1 C2 l2 C3 l3
       assume trans_hyp: "(C1 \<prec>\<cdot> C2 \<or> C1 \<doteq> C2 \<and> l1 \<sqsubset>l l2) \<and> (C2 \<prec>\<cdot> C3 \<or> C2 \<doteq> C3 \<and> l2 \<sqsubset>l l3)"
       have "C1 \<prec>\<cdot> C2 \<Longrightarrow> C2 \<doteq> C3 \<Longrightarrow> C1 \<prec>\<cdot> C3"
         using compat_equiv_prec by (metis equiv_equiv_F equivp_def)
       moreover have "C1 \<doteq> C2 \<Longrightarrow> C2 \<prec>\<cdot> C3 \<Longrightarrow> C1 \<prec>\<cdot> C3"
         using compat_equiv_prec by (metis equiv_equiv_F equivp_def)
       moreover have "l1 \<sqsubset>l l2 \<Longrightarrow> l2 \<sqsubset>l l3 \<Longrightarrow> l1 \<sqsubset>l l3"
         using wf_prec_l unfolding minimal_element_def po_on_def transp_on_def by (meson UNIV_I)
       moreover have "C1 \<doteq> C2 \<Longrightarrow> C2 \<doteq> C3 \<Longrightarrow> C1 \<doteq> C3"
         using equiv_equiv_F by (meson equivp_transp)
       ultimately show "C1 \<prec>\<cdot> C3 \<or> C1 \<doteq> C3 \<and> l1 \<sqsubset>l l3" using trans_hyp
         using trans_prec_F by blast
     qed
   qed
 next
   show "wfp_on (\<sqsubset>) UNIV" unfolding wfp_on_def
   proof
     assume contra: "\<exists>f. \<forall>i. f i \<in> UNIV \<and> f (Suc i) \<sqsubset> f i"
     then obtain f where
       f_suc: "\<forall>i. f (Suc i) \<sqsubset> f i"
       by blast
 
     define R :: "(('f \<times> 'l) \<times> ('f \<times> 'l)) set" where
       "R = {(Cl1, Cl2). fst Cl1 \<prec>\<cdot> fst Cl2}"
     define S :: "(('f \<times> 'l) \<times> ('f \<times> 'l)) set" where
       "S = {(Cl1, Cl2). fst Cl1 \<doteq> fst Cl2 \<and> snd Cl1 \<sqsubset>l snd Cl2}"
 
     obtain k where
       f_chain: "\<forall>i. (f (Suc (i + k)), f (i + k)) \<in> S"
     proof (atomize_elim, rule wf_infinite_down_chain_compatible[of R f S])
       show "wf R"
         unfolding R_def using wf_app[OF wf_prec_F[unfolded minimal_element_def, THEN conjunct2,
               unfolded wfp_on_UNIV wfP_def]]
         by force
     next
       show "\<forall>i. (f (Suc i), f i) \<in> R \<union> S"
         using f_suc unfolding R_def S_def Prec_FL_def by blast
     next
       show "R O S \<subseteq> R"
         unfolding R_def S_def using compat_equiv_prec equiv_equiv_F equivp_reflp by fastforce
     qed
 
     define g where
       "\<And>i. g i = f (i + k)"
 
     have g_chain: "\<forall>i. (g (Suc i), g i) \<in> S"
       unfolding g_def using f_chain by simp
     have wf_s: "wf S"
       unfolding S_def
       by (rule wf_subset[OF wf_app[OF wf_prec_l[unfolded minimal_element_def, THEN conjunct2,
                 unfolded wfp_on_UNIV wfP_def], of snd]])
         fast
     show False
       using g_chain[unfolded S_def]
         wf_s[unfolded S_def, folded wfP_def wfp_on_UNIV, unfolded wfp_on_def]
       by auto
   qed
 qed
 
 definition active_subset :: "('f \<times> 'l) set \<Rightarrow> ('f \<times> 'l) set" where
   "active_subset M = {CL \<in> M. snd CL = active}"
 
 definition passive_subset :: "('f \<times> 'l) set \<Rightarrow> ('f \<times> 'l) set" where
   "passive_subset M = {CL \<in> M. snd CL \<noteq> active}"
 
 lemma active_subset_insert[simp]:
   "active_subset (insert Cl N) = (if snd Cl = active then {Cl} else {}) \<union> active_subset N"
   unfolding active_subset_def by auto
 
 lemma active_subset_union[simp]: "active_subset (M \<union> N) = active_subset M \<union> active_subset N"
   unfolding active_subset_def by auto
 
 lemma passive_subset_insert[simp]:
   "passive_subset (insert Cl N) = (if snd Cl \<noteq> active then {Cl} else {}) \<union> passive_subset N"
   unfolding passive_subset_def by auto
 
 lemma passive_subset_union[simp]: "passive_subset (M \<union> N) = passive_subset M \<union> passive_subset N"
   unfolding passive_subset_def by auto
 
 sublocale std?: statically_complete_calculus Bot_FL Inf_FL "(\<Turnstile>\<inter>\<G>L)" Red_I Red_F
   using labeled_static_ref[OF static_ref_comp] .
 
 lemma labeled_tiebreaker_lifting:
   assumes q_in: "q \<in> Q"
   shows "tiebreaker_lifting Bot_FL Inf_FL Bot_G (entails_q q) (Inf_G_q q)
     (Red_I_q q) (Red_F_q q) (\<G>_F_L_q q) (\<G>_I_L_q q) (\<lambda>g. Prec_FL)"
 proof -
   have "tiebreaker_lifting Bot_FL Inf_FL Bot_G (entails_q q) (Inf_G_q q)
     (Red_I_q q) (Red_F_q q) (\<G>_F_L_q q) (\<G>_I_L_q q) (\<lambda>g Cl Cl'. False)"
     using ord_fam_lifted_q[OF q_in] .
   then have "standard_lifting Bot_FL Inf_FL Bot_G (Inf_G_q q) (entails_q q) (Red_I_q q)
     (Red_F_q q) (\<G>_F_L_q q) (\<G>_I_L_q q)"
     using lifted_q[OF q_in] by blast
   then show "tiebreaker_lifting Bot_FL Inf_FL Bot_G (entails_q q) (Inf_G_q q)
     (Red_I_q q) (Red_F_q q) (\<G>_F_L_q q) (\<G>_I_L_q q) (\<lambda>g. Prec_FL)"
     using wf_prec_FL by (simp add: tiebreaker_lifting.intro tiebreaker_lifting_axioms.intro)
 qed
 
 sublocale lifting_intersection Inf_FL Bot_G Q Inf_G_q entails_q Red_I_q Red_F_q
   Bot_FL \<G>_F_L_q \<G>_I_L_q "\<lambda>g. Prec_FL"
   using labeled_tiebreaker_lifting unfolding lifting_intersection_def
   by (simp add: lifting_intersection_axioms.intro
       no_labels.ground.consequence_relation_family_axioms
       no_labels.ground.inference_system_family_axioms)
 
-notation derive (infix "\<rhd>RedL" 50)
+notation derive (infix "\<rhd>L" 50)
 
 lemma std_Red_I_eq: "std.Red_I = Red_I_\<G>"
   unfolding Red_I_\<G>_q_def Red_I_\<G>_L_q_def by simp
 
 lemma std_Red_F_eq: "std.Red_F = Red_F_\<G>_empty"
   unfolding Red_F_\<G>_empty_q_def Red_F_\<G>_empty_L_q_def by simp
 
 sublocale statically_complete_calculus Bot_FL Inf_FL "(\<Turnstile>\<inter>\<G>L)" Red_I Red_F
   by unfold_locales (use statically_complete std_Red_I_eq in auto)
 
 (* lem:redundant-labeled-inferences *)
 lemma labeled_red_inf_eq_red_inf:
   assumes i_in: "\<iota> \<in> Inf_FL"
   shows "\<iota> \<in> Red_I N \<longleftrightarrow> to_F \<iota> \<in> no_labels.Red_I_\<G> (fst ` N)"
 proof
   assume i_in2: "\<iota> \<in> Red_I N"
   then have "X \<in> Red_I_\<G>_q ` Q \<Longrightarrow> \<iota> \<in> X N" for X
     unfolding Red_I_def by blast
   obtain X0 where "X0 \<in> Red_I_\<G>_q ` Q"
     using Q_nonempty by blast
   then obtain q0 where x0_is: "X0 N = Red_I_\<G>_q q0 N" by blast
   then obtain Y0 where y0_is: "Y0 (fst ` N) = to_F ` (X0 N)" by auto
   have "Y0 (fst ` N) = no_labels.Red_I_\<G>_q q0 (fst ` N)"
     unfolding  y0_is
   proof
     show "to_F ` X0 N \<subseteq> no_labels.Red_I_\<G>_q q0 (fst ` N)"
     proof
       fix \<iota>0
       assume i0_in: "\<iota>0 \<in> to_F ` X0 N"
       then have i0_in2: "\<iota>0 \<in> to_F ` Red_I_\<G>_q q0 N"
         using x0_is by argo
       then obtain \<iota>0_FL where i0_FL_in: "\<iota>0_FL \<in> Inf_FL" and i0_to_i0_FL: "\<iota>0 = to_F \<iota>0_FL" and
         subs1: "((\<G>_I_L_q q0 \<iota>0_FL) \<noteq> None \<and>
             the (\<G>_I_L_q q0 \<iota>0_FL) \<subseteq> Red_I_q q0 (\<G>_set_q q0 N))
             \<or> ((\<G>_I_L_q q0 \<iota>0_FL = None) \<and>
             \<G>_F_L_q q0 (concl_of \<iota>0_FL) \<subseteq> \<G>_set_q q0 N \<union> Red_F_q q0 (\<G>_set_q q0 N))"
         unfolding Red_I_\<G>_q_def by blast
       have concl_swap: "fst (concl_of \<iota>0_FL) = concl_of \<iota>0"
         unfolding concl_of_def i0_to_i0_FL to_F_def by simp
       have i0_in3: "\<iota>0 \<in> Inf_F"
         using i0_to_i0_FL Inf_FL_to_Inf_F[OF i0_FL_in] unfolding to_F_def by blast
       {
         assume
           not_none: "\<G>_I_q q0 \<iota>0 \<noteq> None" and
           "the (\<G>_I_q q0 \<iota>0) \<noteq> {}"
         then obtain \<iota>1 where i1_in: "\<iota>1 \<in> the (\<G>_I_q q0 \<iota>0)" by blast
         have "the (\<G>_I_q q0 \<iota>0) \<subseteq> Red_I_q q0 (no_labels.\<G>_set_q q0 (fst ` N))"
           using subs1 i0_to_i0_FL not_none by auto
       }
       moreover {
         assume
           is_none: "\<G>_I_q q0 \<iota>0 = None"
         then have "\<G>_F_q q0 (concl_of \<iota>0) \<subseteq> no_labels.\<G>_set_q q0 (fst ` N)
             \<union> Red_F_q q0 (no_labels.\<G>_set_q q0 (fst ` N))"
           using subs1 i0_to_i0_FL concl_swap by simp
       }
       ultimately show "\<iota>0 \<in> no_labels.Red_I_\<G>_q q0 (fst ` N)"
         unfolding no_labels.Red_I_\<G>_q_def using i0_in3 by auto
     qed
   next
     show "no_labels.Red_I_\<G>_q q0 (fst ` N) \<subseteq> to_F ` X0 N"
     proof
       fix \<iota>0
       assume i0_in: "\<iota>0 \<in> no_labels.Red_I_\<G>_q q0 (fst ` N)"
       then have i0_in2: "\<iota>0 \<in> Inf_F"
         unfolding no_labels.Red_I_\<G>_q_def by blast
       obtain \<iota>0_FL where i0_FL_in: "\<iota>0_FL \<in> Inf_FL" and i0_to_i0_FL: "\<iota>0 = to_F \<iota>0_FL"
         using Inf_F_to_Inf_FL[OF i0_in2] unfolding to_F_def
         by (metis Ex_list_of_length fst_conv inference.exhaust_sel inference.inject map_fst_zip)
       have concl_swap: "fst (concl_of \<iota>0_FL) = concl_of \<iota>0"
         unfolding concl_of_def i0_to_i0_FL to_F_def by simp
       have subs1: "((\<G>_I_L_q q0 \<iota>0_FL) \<noteq> None \<and>
            the (\<G>_I_L_q q0 \<iota>0_FL) \<subseteq> Red_I_q q0 (\<G>_set_q q0 N))
            \<or> ((\<G>_I_L_q q0 \<iota>0_FL = None) \<and>
            \<G>_F_L_q q0 (concl_of \<iota>0_FL) \<subseteq> (\<G>_set_q q0 N \<union> Red_F_q q0 (\<G>_set_q q0 N)))"
         using i0_in i0_to_i0_FL concl_swap unfolding no_labels.Red_I_\<G>_q_def by simp
       then have "\<iota>0_FL \<in> Red_I_\<G>_q q0 N"
         using i0_FL_in unfolding Red_I_\<G>_q_def by simp
       then show "\<iota>0 \<in> to_F ` X0 N"
         using x0_is i0_to_i0_FL i0_in2 by blast
     qed
   qed
   then have "Y \<in> no_labels.Red_I_\<G>_q ` Q \<Longrightarrow> to_F \<iota> \<in> Y (fst ` N)" for Y
     using i_in2 no_labels.Red_I_def std_Red_I_eq red_inf_impl by force
   then show "to_F \<iota> \<in> no_labels.Red_I_\<G> (fst ` N)"
     unfolding Red_I_def no_labels.Red_I_\<G>_def by blast
 next
   assume to_F_in: "to_F \<iota> \<in> no_labels.Red_I_\<G> (fst ` N)"
   have imp_to_F: "X \<in> no_labels.Red_I_\<G>_q ` Q \<Longrightarrow> to_F \<iota> \<in> X (fst ` N)" for X
     using to_F_in unfolding no_labels.Red_I_\<G>_def by blast
   then have to_F_in2: "to_F \<iota> \<in> no_labels.Red_I_\<G>_q q (fst ` N)" if "q \<in> Q" for q
     using that by auto
   have "Red_I_\<G>_q q N = {\<iota>0_FL \<in> Inf_FL. to_F \<iota>0_FL \<in> no_labels.Red_I_\<G>_q q (fst ` N)}" for q
   proof
     show "Red_I_\<G>_q q N \<subseteq> {\<iota>0_FL \<in> Inf_FL. to_F \<iota>0_FL \<in> no_labels.Red_I_\<G>_q q (fst ` N)}"
     proof
       fix q0 \<iota>1
       assume
         i1_in: "\<iota>1 \<in> Red_I_\<G>_q q0 N"
       have i1_in2: "\<iota>1 \<in> Inf_FL"
         using i1_in unfolding Red_I_\<G>_q_def by blast
       then have to_F_i1_in: "to_F \<iota>1 \<in> Inf_F"
         using Inf_FL_to_Inf_F unfolding to_F_def by simp
       have concl_swap: "fst (concl_of \<iota>1) = concl_of (to_F \<iota>1)"
         unfolding concl_of_def to_F_def by simp
       then have i1_to_F_in: "to_F \<iota>1 \<in> no_labels.Red_I_\<G>_q q0 (fst ` N)"
         using i1_in to_F_i1_in unfolding Red_I_\<G>_q_def no_labels.Red_I_\<G>_q_def by force
       show "\<iota>1 \<in> {\<iota>0_FL \<in> Inf_FL. to_F \<iota>0_FL \<in> no_labels.Red_I_\<G>_q q0 (fst ` N)}"
         using i1_in2 i1_to_F_in by blast
     qed
   next
     show "{\<iota>0_FL \<in> Inf_FL. to_F \<iota>0_FL \<in> no_labels.Red_I_\<G>_q q (fst ` N)} \<subseteq> Red_I_\<G>_q q N"
     proof
       fix q0 \<iota>1
       assume
         i1_in: "\<iota>1 \<in> {\<iota>0_FL \<in> Inf_FL. to_F \<iota>0_FL \<in> no_labels.Red_I_\<G>_q q0 (fst ` N)}"
       then have i1_in2: "\<iota>1 \<in> Inf_FL" by blast
       then have to_F_i1_in: "to_F \<iota>1 \<in> Inf_F"
         using Inf_FL_to_Inf_F unfolding to_F_def by simp
       have concl_swap: "fst (concl_of \<iota>1) = concl_of (to_F \<iota>1)"
         unfolding concl_of_def to_F_def by simp
       then have "((\<G>_I_L_q q0 \<iota>1) \<noteq> None \<and> the (\<G>_I_L_q q0 \<iota>1) \<subseteq> Red_I_q q0 (\<G>_set_q q0 N))
         \<or> (\<G>_I_L_q q0 \<iota>1 = None \<and>
           \<G>_F_L_q q0 (concl_of \<iota>1) \<subseteq> \<G>_set_q q0 N \<union> Red_F_q q0 (\<G>_set_q q0 N))"
         using i1_in unfolding no_labels.Red_I_\<G>_q_def by auto
       then show "\<iota>1 \<in> Red_I_\<G>_q q0 N"
         using i1_in2 unfolding Red_I_\<G>_q_def by blast
     qed
   qed
   then have "\<iota> \<in> Red_I_\<G>_q q N" if "q \<in> Q" for q
     using that to_F_in2 i_in unfolding Red_I_\<G>_q_def no_labels.Red_I_\<G>_q_def by auto
   then show "\<iota> \<in> Red_I_\<G> N"
     unfolding Red_I_\<G>_def by blast
 qed
 
 (* lem:redundant-labeled-formulas *)
 lemma red_labeled_clauses:
   assumes \<open>C \<in> no_labels.Red_F_\<G>_empty (fst ` N) \<or>
     (\<exists>C' \<in> fst ` N. C' \<prec>\<cdot> C) \<or> (\<exists>(C', L') \<in> N. L' \<sqsubset>l L \<and> C' \<preceq>\<cdot> C)\<close>
   shows \<open>(C, L) \<in> Red_F N\<close>
 proof -
   note assms
   moreover have i: \<open>C \<in> no_labels.Red_F_\<G>_empty (fst ` N) \<Longrightarrow> (C, L) \<in> Red_F N\<close>
   proof -
     assume "C \<in> no_labels.Red_F_\<G>_empty (fst ` N)"
     then have "C \<in> no_labels.Red_F_\<G>_empty_q q (fst ` N)" if "q \<in> Q" for q
       unfolding no_labels.Red_F_\<G>_empty_def using that by fast
     then have g_in_red: "\<G>_F_q q C \<subseteq> Red_F_q q (no_labels.\<G>_set_q q (fst ` N))" if "q \<in> Q" for q
       unfolding no_labels.Red_F_\<G>_empty_q_def using that by blast
     have "\<G>_F_L_q q (C, L) \<subseteq> Red_F_q q (\<G>_set_q q N)" if "q \<in> Q" for q
       using that g_in_red by simp
     then show ?thesis
       unfolding Red_F_def Red_F_\<G>_q_def by blast
   qed
   moreover have ii: \<open>\<exists>C' \<in> fst ` N. C' \<prec>\<cdot> C \<Longrightarrow> (C, L) \<in> Red_F N\<close>
   proof -
     assume "\<exists>C' \<in> fst ` N. C' \<prec>\<cdot> C"
     then obtain C' where c'_in: "C' \<in> fst ` N" and c_prec_c': "C' \<prec>\<cdot> C" by blast
     obtain L' where c'_l'_in: "(C', L') \<in> N" using c'_in by auto
     have c'_l'_prec: "(C', L') \<sqsubset> (C, L)"
       using c_prec_c' unfolding Prec_FL_def by simp
     have c_in_c'_g: "\<G>_F_q q C \<subseteq> \<G>_F_q q C'" if "q \<in> Q" for q
       using prec_F_grounding[OF that c_prec_c'] by presburger
     then have "\<G>_F_L_q q (C, L) \<subseteq> \<G>_F_L_q q (C', L')" if "q \<in> Q" for q
       using that by auto
     then have "(C, L) \<in> Red_F_\<G>_q q N" if "q \<in> Q" for q
       unfolding Red_F_\<G>_q_def using that c'_l'_in c'_l'_prec by blast
     then show ?thesis
       unfolding Red_F_def by blast
   qed
   moreover have iii: \<open>\<exists>(C', L') \<in> N. L' \<sqsubset>l L \<and> C' \<preceq>\<cdot> C \<Longrightarrow> (C, L) \<in> Red_F N\<close>
   proof -
     assume "\<exists>(C', L') \<in> N. L' \<sqsubset>l L \<and> C' \<preceq>\<cdot> C"
     then obtain C' L' where c'_l'_in: "(C', L') \<in> N" and l'_sub_l: "L' \<sqsubset>l L" and c'_sub_c: "C' \<preceq>\<cdot> C"
       by fast
     have "(C, L) \<in> Red_F N" if "C' \<prec>\<cdot> C"
       using that c'_l'_in ii by fastforce
     moreover {
       assume equiv_c_c': "C \<doteq> C'"
       then have equiv_c'_c: "C' \<doteq> C"
         using equiv_equiv_F by (simp add: equivp_symp)
       then have c'_l'_prec: "(C', L') \<sqsubset> (C, L)"
         using l'_sub_l unfolding Prec_FL_def by simp
       have "\<G>_F_q q C = \<G>_F_q q C'" if "q \<in> Q" for q
         using that equiv_F_grounding equiv_c_c' equiv_c'_c by (simp add: set_eq_subset)
       then have "\<G>_F_L_q q (C, L) = \<G>_F_L_q q (C', L')" if "q \<in> Q" for q
         using that by auto
       then have "(C, L) \<in> Red_F_\<G>_q q N" if "q \<in> Q" for q
         unfolding Red_F_\<G>_q_def using that c'_l'_in c'_l'_prec by blast
       then have ?thesis
         unfolding Red_F_def by blast
     }
     ultimately show ?thesis
       using c'_sub_c equiv_equiv_F equivp_symp by fastforce
   qed
   ultimately show ?thesis
     by blast
 qed
 
 end
   
   
 subsection \<open>Given Clause Procedure\<close>
 
 locale given_clause = given_clause_basis Bot_F Inf_F Bot_G Q entails_q Inf_G_q Red_I_q
   Red_F_q \<G>_F_q \<G>_I_q Inf_FL Equiv_F Prec_F Prec_l active
   for
     Bot_F :: "'f set" and
     Inf_F :: "'f inference set" and
     Bot_G :: "'g set" and
     Q :: "'q set" and
     entails_q :: "'q \<Rightarrow> 'g set \<Rightarrow> 'g set \<Rightarrow> bool" and
     Inf_G_q :: \<open>'q \<Rightarrow> 'g inference set\<close> and
     Red_I_q :: "'q \<Rightarrow> 'g set \<Rightarrow> 'g inference set" and
     Red_F_q :: "'q \<Rightarrow> 'g set \<Rightarrow> 'g set" and
     \<G>_F_q :: "'q \<Rightarrow> 'f \<Rightarrow> 'g set"  and
     \<G>_I_q :: "'q \<Rightarrow> 'f inference \<Rightarrow> 'g inference set option" and
     Inf_FL :: \<open>('f \<times> 'l) inference set\<close> and
     Equiv_F :: "'f \<Rightarrow> 'f \<Rightarrow> bool" (infix "\<doteq>" 50) and
     Prec_F :: "'f \<Rightarrow> 'f \<Rightarrow> bool" (infix "\<prec>\<cdot>" 50) and
     Prec_l :: "'l \<Rightarrow> 'l \<Rightarrow> bool" (infix "\<sqsubset>l" 50) and
     active :: 'l +
   assumes
     inf_have_prems: "\<iota>F \<in> Inf_F \<Longrightarrow> prems_of \<iota>F \<noteq> []"
 begin
   
 lemma labeled_inf_have_prems: "\<iota> \<in> Inf_FL \<Longrightarrow> prems_of \<iota> \<noteq> []"
   using inf_have_prems Inf_FL_to_Inf_F by fastforce
 
 inductive step :: "('f \<times> 'l) set \<Rightarrow> ('f \<times> 'l) set \<Rightarrow> bool" (infix "\<leadsto>GC" 50) where
   process: "N1 = N \<union> M \<Longrightarrow> N2 = N \<union> M' \<Longrightarrow> M \<subseteq> Red_F (N \<union> M') \<Longrightarrow>
     active_subset M' = {} \<Longrightarrow> N1 \<leadsto>GC N2"
 | infer: "N1 = N \<union> {(C, L)} \<Longrightarrow> N2 = N \<union> {(C, active)} \<union> M \<Longrightarrow> L \<noteq> active \<Longrightarrow>
     active_subset M = {} \<Longrightarrow>
     no_labels.Inf_between (fst ` (active_subset N)) {C}
     \<subseteq> no_labels.Red_I (fst ` (N \<union> {(C, active)} \<union> M)) \<Longrightarrow>
     N1 \<leadsto>GC N2"
   
-lemma one_step_equiv: "N1 \<leadsto>GC N2 \<Longrightarrow> N1 \<rhd>RedL N2"
+lemma one_step_equiv: "N1 \<leadsto>GC N2 \<Longrightarrow> N1 \<rhd>L N2"
 proof (cases N1 N2 rule: step.cases)
   show "N1 \<leadsto>GC N2 \<Longrightarrow> N1 \<leadsto>GC N2" by blast
 next
   fix N M M'
   assume
     gc_step: "N1 \<leadsto>GC N2" and
     n1_is: "N1 = N \<union> M" and
     n2_is: "N2 = N \<union> M'" and
     m_red: "M \<subseteq> Red_F (N \<union> M')" and
     active_empty: "active_subset M' = {}"
   have "N1 - N2 \<subseteq> Red_F N2"
     using n1_is n2_is m_red by auto
-  then show "N1 \<rhd>RedL N2"
+  then show "N1 \<rhd>L N2"
     unfolding derive.simps by blast
 next
   fix N C L M
   assume
     gc_step: "N1 \<leadsto>GC N2" and
     n1_is: "N1 = N \<union> {(C, L)}" and
     not_active: "L \<noteq> active" and
     n2_is: "N2 = N \<union> {(C, active)} \<union> M" and
     active_empty: "active_subset M = {}"
   have "(C, active) \<in> N2" using n2_is by auto
   moreover have "C \<preceq>\<cdot> C" using equiv_equiv_F by (metis equivp_def)
   moreover have "active \<sqsubset>l L" using active_minimal[OF not_active] .
   ultimately have "{(C, L)} \<subseteq> Red_F N2"
     using red_labeled_clauses by blast
   moreover have "N1 - N2 = {} \<or> N1 - N2 = {(C, L)}" using n1_is n2_is by blast
   ultimately have "N1 - N2 \<subseteq> Red_F N2"
     using std_Red_F_eq by blast
-  then show "N1 \<rhd>RedL N2"
+  then show "N1 \<rhd>L N2"
     unfolding derive.simps by blast
 qed
 
 (* lem:gc-derivations-are-red-derivations *)
-lemma gc_to_red: "chain (\<leadsto>GC) Ns \<Longrightarrow> chain (\<rhd>RedL) Ns"
+lemma gc_to_red: "chain (\<leadsto>GC) Ns \<Longrightarrow> chain (\<rhd>L) Ns"
   using one_step_equiv Lazy_List_Chain.chain_mono by blast
 
 lemma (in-) all_ex_finite_set: "(\<forall>(j::nat)\<in>{0..<m}. \<exists>(n::nat). P j n) \<Longrightarrow>
   (\<forall>n1 n2. \<forall>j\<in>{0..<m}. P j n1 \<longrightarrow> P j n2 \<longrightarrow> n1 = n2) \<Longrightarrow> finite {n. \<exists>j \<in> {0..<m}. P j n}" for m P
 proof -
   fix m::nat and P:: "nat \<Rightarrow> nat \<Rightarrow> bool"
   assume
     allj_exn: "\<forall>j\<in>{0..<m}. \<exists>n. P j n" and
     uniq_n: "\<forall>n1 n2. \<forall>j\<in>{0..<m}. P j n1 \<longrightarrow> P j n2 \<longrightarrow> n1 = n2"
   have "{n. \<exists>j \<in> {0..<m}. P j n} = (\<Union>((\<lambda>j. {n. P j n}) ` {0..<m}))" by blast
   then have imp_finite: "(\<forall>j\<in>{0..<m}. finite {n. P j n}) \<Longrightarrow> finite {n. \<exists>j \<in> {0..<m}. P j n}"
     using finite_UN[of "{0..<m}" "\<lambda>j. {n. P j n}"] by simp
   have "\<forall>j\<in>{0..<m}. \<exists>!n. P j n" using allj_exn uniq_n by blast
   then have "\<forall>j\<in>{0..<m}. finite {n. P j n}" by (metis bounded_nat_set_is_finite lessI mem_Collect_eq)
   then show "finite {n. \<exists>j \<in> {0..<m}. P j n}" using imp_finite by simp
 qed
 
 (* lem:fair-gc-derivations *)
 lemma gc_fair:
   assumes
     deriv: "chain (\<leadsto>GC) Ns" and
     init_state: "active_subset (lhd Ns) = {}" and
     final_state: "passive_subset (Liminf_llist Ns) = {}"
   shows "fair Ns"
   unfolding fair_def
 proof
   fix \<iota>
   assume i_in: "\<iota> \<in> Inf_from (Liminf_llist Ns)"
   note lhd_is = lhd_conv_lnth[OF chain_not_lnull[OF deriv]]
   have i_in_inf_fl: "\<iota> \<in> Inf_FL" using i_in unfolding Inf_from_def by blast
   have "Liminf_llist Ns = active_subset (Liminf_llist Ns)"
     using final_state unfolding passive_subset_def active_subset_def by blast
   then have i_in2: "\<iota> \<in> Inf_from (active_subset (Liminf_llist Ns))" using i_in by simp
   define m where "m = length (prems_of \<iota>)"
   then have m_def_F: "m = length (prems_of (to_F \<iota>))" unfolding to_F_def by simp
   have i_in_F: "to_F \<iota> \<in> Inf_F"
     using i_in Inf_FL_to_Inf_F unfolding Inf_from_def to_F_def by blast
   then have m_pos: "m > 0" using m_def_F using inf_have_prems by blast
   have exist_nj: "\<forall>j \<in> {0..<m}. (\<exists>nj. enat (Suc nj) < llength Ns \<and>
       prems_of \<iota> ! j \<notin> active_subset (lnth Ns nj) \<and>
       (\<forall>k. k > nj \<longrightarrow> enat k < llength Ns \<longrightarrow> prems_of \<iota> ! j \<in> active_subset (lnth Ns k)))"
   proof clarify
     fix j
     assume j_in: "j \<in> {0..<m}"
     then obtain C where c_is: "(C, active) = prems_of \<iota> ! j"
       using i_in2 unfolding m_def Inf_from_def active_subset_def
       by (smt Collect_mem_eq Collect_mono_iff atLeastLessThan_iff nth_mem old.prod.exhaust snd_conv)
     then have "(C, active) \<in> Liminf_llist Ns"
       using j_in i_in unfolding m_def Inf_from_def by force
     then obtain nj where nj_is: "enat nj < llength Ns" and
       c_in2: "(C, active) \<in> \<Inter> (lnth Ns ` {k. nj \<le> k \<and> enat k < llength Ns})"
       unfolding Liminf_llist_def using init_state by blast
     then have c_in3: "\<forall>k. k \<ge> nj \<longrightarrow> enat k < llength Ns \<longrightarrow> (C, active) \<in> lnth Ns k" by blast
     have nj_pos: "nj > 0" using init_state c_in2 nj_is
       unfolding active_subset_def lhd_is by force
     obtain nj_min where nj_min_is: "nj_min = (LEAST nj. enat nj < llength Ns \<and>
         (C, active) \<in> \<Inter> (lnth Ns ` {k. nj \<le> k \<and> enat k < llength Ns}))" by blast
     then have in_allk: "\<forall>k. k \<ge> nj_min \<longrightarrow> enat k < llength Ns \<longrightarrow> (C, active) \<in> (lnth Ns k)"
       using c_in3 nj_is c_in2
       by (metis (mono_tags, lifting) INT_E LeastI_ex mem_Collect_eq)
     have njm_smaller_D: "enat nj_min < llength Ns"
       using nj_min_is
       by (smt LeastI_ex \<open>\<And>thesis. (\<And>nj. \<lbrakk>enat nj < llength Ns;
           (C, active) \<in> \<Inter> (lnth Ns ` {k. nj \<le> k \<and> enat k < llength Ns})\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis\<close>)
     have "nj_min > 0"
       using nj_is c_in2 nj_pos nj_min_is lhd_is
       by (metis (mono_tags, lifting) Collect_empty_eq \<open>(C, active) \<in> Liminf_llist Ns\<close>
           \<open>Liminf_llist Ns = active_subset (Liminf_llist Ns)\<close>
           \<open>\<forall>k\<ge>nj_min. enat k < llength Ns \<longrightarrow> (C, active) \<in> lnth Ns k\<close> active_subset_def init_state
           linorder_not_less mem_Collect_eq zero_enat_def chain_length_pos[OF deriv])
     then obtain njm_prec where nj_prec_is: "Suc njm_prec = nj_min" using gr0_conv_Suc by auto
     then have njm_prec_njm: "njm_prec < nj_min" by blast
     then have njm_prec_njm_enat: "enat njm_prec < enat nj_min" by simp
     have njm_prec_smaller_d: "njm_prec < llength Ns"
       using HOL.no_atp(15)[OF njm_smaller_D njm_prec_njm_enat] .
     have njm_prec_all_suc: "\<forall>k>njm_prec. enat k < llength Ns \<longrightarrow> (C, active) \<in> lnth Ns k"
       using nj_prec_is in_allk by simp
     have notin_njm_prec: "(C, active) \<notin> lnth Ns njm_prec"
     proof (rule ccontr)
       assume "\<not> (C, active) \<notin> lnth Ns njm_prec"
       then have absurd_hyp: "(C, active) \<in> lnth Ns njm_prec" by simp
       have prec_smaller: "enat njm_prec < llength Ns" using nj_min_is nj_prec_is
         by (smt LeastI_ex Suc_leD \<open>\<And>thesis. (\<And>nj. \<lbrakk>enat nj < llength Ns;
             (C, active) \<in> \<Inter> (lnth Ns ` {k. nj \<le> k \<and> enat k < llength Ns})\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis\<close>
             enat_ord_simps(1) le_eq_less_or_eq le_less_trans)
       have "(C, active) \<in> \<Inter> (lnth Ns ` {k. njm_prec \<le> k \<and> enat k < llength Ns})"
       proof -
         {
           fix k
           assume k_in: "njm_prec \<le> k \<and> enat k < llength Ns"
           have "k = njm_prec \<Longrightarrow> (C, active) \<in> lnth Ns k" using absurd_hyp by simp
           moreover have "njm_prec < k \<Longrightarrow> (C, active) \<in> lnth Ns k"
             using nj_prec_is in_allk k_in by simp
           ultimately have "(C, active) \<in> lnth Ns k" using k_in by fastforce
         }
         then show "(C, active) \<in> \<Inter> (lnth Ns ` {k. njm_prec \<le> k \<and> enat k < llength Ns})" by blast
       qed
       then have "enat njm_prec < llength Ns \<and>
           (C, active) \<in> \<Inter> (lnth Ns ` {k. njm_prec \<le> k \<and> enat k < llength Ns})"
         using prec_smaller by blast
       then show False
         using nj_min_is nj_prec_is Orderings.wellorder_class.not_less_Least njm_prec_njm by blast
     qed
     then have notin_active_subs_njm_prec: "(C, active) \<notin> active_subset (lnth Ns njm_prec)"
       unfolding active_subset_def by blast
     then show "\<exists>nj. enat (Suc nj) < llength Ns \<and> prems_of \<iota> ! j \<notin> active_subset (lnth Ns nj) \<and>
         (\<forall>k. k > nj \<longrightarrow> enat k < llength Ns \<longrightarrow> prems_of \<iota> ! j \<in> active_subset (lnth Ns k))"
       using c_is njm_prec_all_suc njm_prec_smaller_d by (metis (mono_tags, lifting)
           active_subset_def mem_Collect_eq nj_prec_is njm_smaller_D snd_conv)
   qed
   define nj_set where "nj_set = {nj. (\<exists>j\<in>{0..<m}. enat (Suc nj) < llength Ns \<and>
       prems_of \<iota> ! j \<notin> active_subset (lnth Ns nj) \<and>
       (\<forall>k. k > nj \<longrightarrow> enat k < llength Ns \<longrightarrow> prems_of \<iota> ! j \<in> active_subset (lnth Ns k)))}"
   then have nj_not_empty: "nj_set \<noteq> {}"
   proof -
     have zero_in: "0 \<in> {0..<m}" using m_pos by simp
     then obtain n0 where "enat (Suc n0) < llength Ns" and
       "prems_of \<iota> ! 0 \<notin> active_subset (lnth Ns n0)" and
       "\<forall>k>n0. enat k < llength Ns \<longrightarrow> prems_of \<iota> ! 0 \<in> active_subset (lnth Ns k)"
       using exist_nj by fast
     then have "n0 \<in> nj_set" unfolding nj_set_def using zero_in by blast
     then show "nj_set \<noteq> {}" by auto
   qed
   have nj_finite: "finite nj_set"
     using all_ex_finite_set[OF exist_nj]
     by (metis (no_types, lifting) Suc_ile_eq dual_order.strict_implies_order
         linorder_neqE_nat nj_set_def)
       (* the n below in the n-1 from the pen-and-paper proof *)
   have "\<exists>n \<in> nj_set. \<forall>nj \<in> nj_set. nj \<le> n"
     using nj_not_empty nj_finite using Max_ge Max_in by blast
   then obtain n where n_in: "n \<in> nj_set" and n_bigger: "\<forall>nj \<in> nj_set. nj \<le> n" by blast
   then obtain j0 where j0_in: "j0 \<in> {0..<m}" and suc_n_length: "enat (Suc n) < llength Ns" and
     j0_notin: "prems_of \<iota> ! j0 \<notin> active_subset (lnth Ns n)" and
     j0_allin: "(\<forall>k. k > n \<longrightarrow> enat k < llength Ns \<longrightarrow> prems_of \<iota> ! j0 \<in> active_subset (lnth Ns k))"
     unfolding nj_set_def by blast
   obtain C0 where C0_is: "prems_of \<iota> ! j0 = (C0, active)" using j0_in
     using i_in2 unfolding m_def Inf_from_def active_subset_def
     by (smt Collect_mem_eq Collect_mono_iff atLeastLessThan_iff nth_mem old.prod.exhaust snd_conv)
   then have C0_prems_i: "(C0, active) \<in> set (prems_of \<iota>)" using in_set_conv_nth j0_in m_def by force
   have C0_in: "(C0, active) \<in> (lnth Ns (Suc n))"
     using C0_is j0_allin suc_n_length by (simp add: active_subset_def)
   have C0_notin: "(C0, active) \<notin> (lnth Ns n)" using C0_is j0_notin unfolding active_subset_def by simp
   have step_n: "lnth Ns n \<leadsto>GC lnth Ns (Suc n)"
     using deriv chain_lnth_rel n_in unfolding nj_set_def by blast
   have "\<exists>N C L M. (lnth Ns n = N \<union> {(C, L)} \<and>
       lnth Ns (Suc n) = N \<union> {(C, active)} \<union> M \<and> L \<noteq> active \<and> active_subset M = {} \<and>
       no_labels.Inf_between (fst ` (active_subset N)) {C}
       \<subseteq> no_labels.Red_I (fst ` (N \<union> {(C, active)} \<union> M)))"
   proof -
     have proc_or_infer: "(\<exists>N1 N M N2 M'. lnth Ns n = N1 \<and> lnth Ns (Suc n) = N2 \<and> N1 = N \<union> M \<and>
          N2 = N \<union> M' \<and> M \<subseteq> Red_F (N \<union> M') \<and> active_subset M' = {}) \<or>
        (\<exists>N1 N C L N2 M. lnth Ns n = N1 \<and> lnth Ns (Suc n) = N2 \<and> N1 = N \<union> {(C, L)} \<and>
          N2 = N \<union> {(C, active)} \<union> M \<and> L \<noteq> active \<and> active_subset M = {} \<and>
          no_labels.Inf_between (fst ` (active_subset N)) {C} \<subseteq>
            no_labels.Red_I (fst ` (N \<union> {(C, active)} \<union> M)))"
       using step.simps[of "lnth Ns n" "lnth Ns (Suc n)"] step_n by blast
     show ?thesis
       using C0_in C0_notin proc_or_infer j0_in C0_is
       by (smt Un_iff active_subset_def mem_Collect_eq snd_conv sup_bot.right_neutral)
   qed
   then obtain N M L where inf_from_subs:
     "no_labels.Inf_between (fst ` (active_subset N)) {C0}
      \<subseteq> no_labels.Red_I (fst ` (N \<union> {(C0, active)} \<union> M))" and
     nth_d_is: "lnth Ns n = N \<union> {(C0, L)}" and
     suc_nth_d_is: "lnth Ns (Suc n) = N \<union> {(C0, active)} \<union> M" and
     l_not_active: "L \<noteq> active"
     using C0_in C0_notin j0_in C0_is using active_subset_def by fastforce
   have "j \<in> {0..<m} \<Longrightarrow> prems_of \<iota> ! j \<noteq> prems_of \<iota> ! j0 \<Longrightarrow> prems_of \<iota> ! j \<in> (active_subset N)" for j
   proof -
     fix j
     assume j_in: "j \<in> {0..<m}" and
       j_not_j0: "prems_of \<iota> ! j \<noteq> prems_of \<iota> ! j0"
     obtain nj where nj_len: "enat (Suc nj) < llength Ns" and
       nj_prems: "prems_of \<iota> ! j \<notin> active_subset (lnth Ns nj)" and
       nj_greater: "(\<forall>k. k > nj \<longrightarrow> enat k < llength Ns \<longrightarrow> prems_of \<iota> ! j \<in> active_subset (lnth Ns k))"
       using exist_nj j_in by blast
     then have "nj \<in> nj_set" unfolding nj_set_def using j_in by blast
     moreover have "nj \<noteq> n"
     proof (rule ccontr)
       assume "\<not> nj \<noteq> n"
       then have "prems_of \<iota> ! j = (C0, active)"
         using C0_in C0_notin step.simps[of "lnth Ns n" "lnth Ns (Suc n)"] step_n
         by (smt Un_iff nth_d_is suc_nth_d_is l_not_active active_subset_def insertCI insertE lessI
             mem_Collect_eq nj_greater nj_prems snd_conv suc_n_length)
       then show False using j_not_j0 C0_is by simp
     qed
     ultimately have "nj < n" using n_bigger by force
     then have "prems_of \<iota> ! j \<in> (active_subset (lnth Ns n))"
       using nj_greater n_in Suc_ile_eq dual_order.strict_implies_order unfolding nj_set_def by blast
     then show "prems_of \<iota> ! j \<in> (active_subset N)"
       using nth_d_is l_not_active unfolding active_subset_def by force
   qed
   then have "set (prems_of \<iota>) \<subseteq> active_subset N \<union> {(C0, active)}"
     using C0_prems_i C0_is m_def
     by (metis Un_iff atLeast0LessThan in_set_conv_nth insertCI lessThan_iff subrelI)
   moreover have "\<not> (set (prems_of \<iota>) \<subseteq> active_subset N - {(C0, active)})" using C0_prems_i by blast
   ultimately have "\<iota> \<in> Inf_between (active_subset N) {(C0, active)}"
     using i_in_inf_fl unfolding Inf_between_def Inf_from_def by blast
   then have "to_F \<iota> \<in> no_labels.Inf_between (fst ` (active_subset N)) {C0}"
     unfolding to_F_def Inf_between_def Inf_from_def
       no_labels.Inf_between_def no_labels.Inf_from_def using Inf_FL_to_Inf_F
     by force
   then have "to_F \<iota> \<in> no_labels.Red_I (fst ` (lnth Ns (Suc n)))"
     using suc_nth_d_is inf_from_subs by fastforce
   then have "\<forall>q \<in> Q. (\<G>_I_q q (to_F \<iota>) \<noteq> None \<and>
       the (\<G>_I_q q (to_F \<iota>)) \<subseteq> Red_I_q q (\<Union> (\<G>_F_q q ` fst ` lnth Ns (Suc n))))
       \<or> (\<G>_I_q q (to_F \<iota>) = None \<and>
       \<G>_F_q q (concl_of (to_F \<iota>)) \<subseteq> \<Union> (\<G>_F_q q ` fst ` lnth Ns (Suc n)) \<union>
         Red_F_q q (\<Union> (\<G>_F_q q ` fst ` lnth Ns (Suc n))))"
     unfolding to_F_def no_labels.Red_I_def no_labels.Red_I_\<G>_q_def by blast
   then have "\<iota> \<in> Red_I_\<G> (lnth Ns (Suc n))"
     using i_in_inf_fl unfolding Red_I_\<G>_def Red_I_\<G>_q_def by (simp add: to_F_def)
   then show "\<iota> \<in> Sup_llist (lmap Red_I_\<G> Ns)"
     unfolding Sup_llist_def using suc_n_length by auto
 qed
 
 theorem gc_complete_Liminf:
   assumes
     deriv: "chain (\<leadsto>GC) Ns" and
     init_state: "active_subset (lhd Ns) = {}" and
     final_state: "passive_subset (Liminf_llist Ns) = {}" and
     b_in: "B \<in> Bot_F" and
     bot_entailed: "no_labels.entails_\<G> (fst ` lhd Ns) {B}"
   shows "\<exists>BL \<in> Bot_FL. BL \<in> Liminf_llist Ns"
 proof -
   note lhd_is = lhd_conv_lnth[OF chain_not_lnull[OF deriv]]
   have labeled_b_in: "(B, active) \<in> Bot_FL" using b_in by simp
   have labeled_bot_entailed: "entails_\<G>_L (lhd Ns) {(B, active)}"
     using labeled_entailment_lifting bot_entailed lhd_is by fastforce
   have fair: "fair Ns" using gc_fair[OF deriv init_state final_state] .
   then show ?thesis
     using dynamically_complete_Liminf[OF labeled_b_in gc_to_red[OF deriv] fair
         labeled_bot_entailed]
     by blast
 qed
 
 (* thm:gc-completeness *)
 theorem gc_complete:
   assumes
     deriv: "chain (\<leadsto>GC) Ns" and
     init_state: "active_subset (lhd Ns) = {}" and
     final_state: "passive_subset (Liminf_llist Ns) = {}" and
     b_in: "B \<in> Bot_F" and
     bot_entailed: "no_labels.entails_\<G> (fst ` lhd Ns) {B}"
   shows "\<exists>i. enat i < llength Ns \<and> (\<exists>BL \<in> Bot_FL. BL \<in> lnth Ns i)"
 proof -
   note lhd_is = lhd_conv_lnth[OF chain_not_lnull[OF deriv]]
   have "\<exists>BL\<in>Bot_FL. BL \<in> Liminf_llist Ns"
     using assms by (rule gc_complete_Liminf)
   then show ?thesis
     unfolding Liminf_llist_def by auto
 qed
 
 end
 
 
 subsection \<open>Lazy Given Clause Procedure\<close>
 
 locale lazy_given_clause = given_clause_basis Bot_F Inf_F Bot_G Q entails_q Inf_G_q Red_I_q
   Red_F_q \<G>_F_q \<G>_I_q Inf_FL Equiv_F Prec_F Prec_l active
   for
     Bot_F :: "'f set" and
     Inf_F :: "'f inference set" and
     Bot_G :: "'g set" and
     Q :: "'q set" and
     entails_q :: "'q \<Rightarrow> 'g set \<Rightarrow> 'g set \<Rightarrow> bool" and
     Inf_G_q :: \<open>'q \<Rightarrow> 'g inference set\<close> and
     Red_I_q :: "'q \<Rightarrow> 'g set \<Rightarrow> 'g inference set" and
     Red_F_q :: "'q \<Rightarrow> 'g set \<Rightarrow> 'g set" and
     \<G>_F_q :: "'q \<Rightarrow> 'f \<Rightarrow> 'g set"  and
     \<G>_I_q :: "'q \<Rightarrow> 'f inference \<Rightarrow> 'g inference set option" and
     Inf_FL :: \<open>('f \<times> 'l) inference set\<close> and
     Equiv_F :: "'f \<Rightarrow> 'f \<Rightarrow> bool" (infix "\<doteq>" 50) and
     Prec_F :: "'f \<Rightarrow> 'f \<Rightarrow> bool" (infix "\<prec>\<cdot>" 50) and
     Prec_l :: "'l \<Rightarrow> 'l \<Rightarrow> bool" (infix "\<sqsubset>l" 50) and
     active :: 'l
 begin
 
 inductive step :: "'f inference set \<times> ('f \<times> 'l) set \<Rightarrow>
   'f inference set \<times> ('f \<times> 'l) set \<Rightarrow> bool" (infix "\<leadsto>LGC" 50) where
   process: "N1 = N \<union> M \<Longrightarrow> N2 = N \<union> M' \<Longrightarrow> M \<subseteq> Red_F (N \<union> M') \<Longrightarrow>
     active_subset M' = {} \<Longrightarrow> (T, N1) \<leadsto>LGC (T, N2)" |
   schedule_infer: "T2 = T1 \<union> T' \<Longrightarrow> N1 = N \<union> {(C, L)} \<Longrightarrow> N2 = N \<union> {(C, active)} \<Longrightarrow>
     L \<noteq> active \<Longrightarrow> T' = no_labels.Inf_between (fst ` (active_subset N)) {C} \<Longrightarrow>
     (T1, N1) \<leadsto>LGC (T2, N2)" |
   compute_infer: "T1 = T2 \<union> {\<iota>} \<Longrightarrow> N2 = N1 \<union> M \<Longrightarrow> active_subset M = {} \<Longrightarrow>
     \<iota> \<in> no_labels.Red_I (fst ` (N1 \<union> M)) \<Longrightarrow> (T1, N1) \<leadsto>LGC (T2, N2)" |
   delete_orphans: "T1 = T2 \<union> T' \<Longrightarrow>
     T' \<inter> no_labels.Inf_from (fst ` (active_subset N)) = {} \<Longrightarrow> (T1, N) \<leadsto>LGC (T2, N)"
 
 lemma premise_free_inf_always_from: "\<iota> \<in> Inf_F \<Longrightarrow> prems_of \<iota> = [] \<Longrightarrow> \<iota> \<in> no_labels.Inf_from N"
   unfolding no_labels.Inf_from_def by simp
 
-lemma one_step_equiv: "(T1, N1) \<leadsto>LGC (T2, N2) \<Longrightarrow> N1 \<rhd>RedL N2"
+lemma one_step_equiv: "(T1, N1) \<leadsto>LGC (T2, N2) \<Longrightarrow> N1 \<rhd>L N2"
 proof (cases "(T1, N1)" "(T2, N2)" rule: step.cases)
   show "(T1, N1) \<leadsto>LGC (T2, N2) \<Longrightarrow> (T1, N1) \<leadsto>LGC (T2, N2)" by blast
 next
   fix N M M'
   assume
     n1_is: "N1 = N \<union> M" and
     n2_is: "N2 = N \<union> M'" and
     m_red: "M \<subseteq> Red_F (N \<union> M')"
   have "N1 - N2 \<subseteq> Red_F N2"
     using n1_is n2_is m_red by auto
-  then show "N1 \<rhd>RedL N2"
+  then show "N1 \<rhd>L N2"
     unfolding derive.simps by blast
 next
   fix N C L M
   assume
     n1_is: "N1 = N \<union> {(C, L)}" and
     not_active: "L \<noteq> active" and
     n2_is: "N2 = N \<union> {(C, active)}"
   have "(C, active) \<in> N2" using n2_is by auto
   moreover have "C \<preceq>\<cdot> C" by (metis equivp_def equiv_equiv_F)
   moreover have "active \<sqsubset>l L" using active_minimal[OF not_active] .
   ultimately have "{(C, L)} \<subseteq> Red_F N2"
     using red_labeled_clauses by blast
   then have "N1 - N2 \<subseteq> Red_F N2"
     using std_Red_F_eq using n1_is n2_is by blast
-  then show "N1 \<rhd>RedL N2"
+  then show "N1 \<rhd>L N2"
     unfolding derive.simps by blast
 next
   fix M
   assume
     n2_is: "N2 = N1 \<union> M"
   have "N1 - N2 \<subseteq> Red_F N2"
     using n2_is by blast
-  then show "N1 \<rhd>RedL N2"
+  then show "N1 \<rhd>L N2"
     unfolding derive.simps by blast
 next
   assume n2_is: "N2 = N1"
   have "N1 - N2 \<subseteq> Red_F N2"
     using n2_is by blast
-  then show "N1 \<rhd>RedL N2"
+  then show "N1 \<rhd>L N2"
     unfolding derive.simps by blast
 qed
 
 (* lem:lgc-derivations-are-red-derivations *)
-lemma lgc_to_red: "chain (\<leadsto>LGC) Ns \<Longrightarrow> chain (\<rhd>RedL) (lmap snd Ns)"
+lemma lgc_to_red: "chain (\<leadsto>LGC) Ns \<Longrightarrow> chain (\<rhd>L) (lmap snd Ns)"
   using one_step_equiv Lazy_List_Chain.chain_mono by (smt chain_lmap prod.collapse)
 
 (* lem:fair-lgc-derivations *)
 lemma lgc_fair:
   assumes
     deriv: "chain (\<leadsto>LGC) Ns" and
     init_state: "active_subset (snd (lhd Ns)) = {}" and
     final_state: "passive_subset (Liminf_llist (lmap snd Ns)) = {}" and
     no_prems_init_active: "\<forall>\<iota> \<in> Inf_F. prems_of \<iota> = [] \<longrightarrow> \<iota> \<in> fst (lhd Ns)" and
     final_schedule: "Liminf_llist (lmap fst Ns) = {}"
   shows "fair (lmap snd Ns)"
   unfolding fair_def
 proof
   fix \<iota>
   assume i_in: "\<iota> \<in> Inf_from (Liminf_llist (lmap snd Ns))"
   note lhd_is = lhd_conv_lnth[OF chain_not_lnull[OF deriv]]
   have i_in_inf_fl: "\<iota> \<in> Inf_FL" using i_in unfolding Inf_from_def by blast
   have "Liminf_llist (lmap snd Ns) = active_subset (Liminf_llist (lmap snd Ns))"
     using final_state unfolding passive_subset_def active_subset_def by blast
   then have i_in2: "\<iota> \<in> Inf_from (active_subset (Liminf_llist (lmap snd Ns)))"
     using i_in by simp
   define m where "m = length (prems_of \<iota>)"
   then have m_def_F: "m = length (prems_of (to_F \<iota>))" unfolding to_F_def by simp
   have i_in_F: "to_F \<iota> \<in> Inf_F"
     using i_in Inf_FL_to_Inf_F unfolding Inf_from_def to_F_def by blast
   have exist_nj: "\<forall>j \<in> {0..<m}. (\<exists>nj. enat (Suc nj) < llength Ns \<and>
       prems_of \<iota> ! j \<notin> active_subset (snd (lnth Ns nj)) \<and>
       (\<forall>k. k > nj \<longrightarrow> enat k < llength Ns \<longrightarrow> prems_of \<iota> ! j \<in> active_subset (snd (lnth Ns k))))"
   proof clarify
     fix j
     assume j_in: "j \<in> {0..<m}"
     then obtain C where c_is: "(C, active) = prems_of \<iota> ! j"
       using i_in2 unfolding m_def Inf_from_def active_subset_def
       by (smt Collect_mem_eq Collect_mono_iff atLeastLessThan_iff nth_mem old.prod.exhaust snd_conv)
     then have "(C, active) \<in> Liminf_llist (lmap snd Ns)"
       using j_in i_in unfolding m_def Inf_from_def by force
     then obtain nj where nj_is: "enat nj < llength Ns" and
       c_in2: "(C, active) \<in> \<Inter> (snd ` (lnth Ns ` {k. nj \<le> k \<and> enat k < llength Ns}))"
       unfolding Liminf_llist_def using init_state by fastforce
     then have c_in3: "\<forall>k. k \<ge> nj \<longrightarrow> enat k < llength Ns \<longrightarrow> (C, active) \<in> snd (lnth Ns k)" by blast
     have nj_pos: "nj > 0" using init_state c_in2 nj_is unfolding active_subset_def lhd_is by fastforce
     obtain nj_min where nj_min_is: "nj_min = (LEAST nj. enat nj < llength Ns \<and>
         (C, active) \<in> \<Inter> (snd ` (lnth Ns ` {k. nj \<le> k \<and> enat k < llength Ns})))" by blast
     then have in_allk: "\<forall>k. k \<ge> nj_min \<longrightarrow> enat k < llength Ns \<longrightarrow> (C, active) \<in> snd (lnth Ns k)"
       using c_in3 nj_is c_in2 INT_E LeastI_ex
       by (smt INT_iff INT_simps(10) c_is image_eqI mem_Collect_eq)
     have njm_smaller_D: "enat nj_min < llength Ns"
       using nj_min_is
       by (smt LeastI_ex \<open>\<And>thesis. (\<And>nj. \<lbrakk>enat nj < llength Ns;
           (C, active) \<in> \<Inter> (snd ` (lnth Ns ` {k. nj \<le> k \<and> enat k < llength Ns}))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis\<close>)
     have "nj_min > 0"
       using nj_is c_in2 nj_pos nj_min_is lhd_is
       by (metis (mono_tags, lifting) active_subset_def emptyE in_allk init_state mem_Collect_eq
           not_less snd_conv zero_enat_def chain_length_pos[OF deriv])
     then obtain njm_prec where nj_prec_is: "Suc njm_prec = nj_min" using gr0_conv_Suc by auto
     then have njm_prec_njm: "njm_prec < nj_min" by blast
     then have njm_prec_njm_enat: "enat njm_prec < enat nj_min" by simp
     have njm_prec_smaller_d: "njm_prec < llength Ns"
       using HOL.no_atp(15)[OF njm_smaller_D njm_prec_njm_enat] .
     have njm_prec_all_suc: "\<forall>k>njm_prec. enat k < llength Ns \<longrightarrow> (C, active) \<in> snd (lnth Ns k)"
       using nj_prec_is in_allk by simp
     have notin_njm_prec: "(C, active) \<notin> snd (lnth Ns njm_prec)"
     proof (rule ccontr)
       assume "\<not> (C, active) \<notin> snd (lnth Ns njm_prec)"
       then have absurd_hyp: "(C, active) \<in> snd (lnth Ns njm_prec)" by simp
       have prec_smaller: "enat njm_prec < llength Ns" using nj_min_is nj_prec_is
         by (smt LeastI_ex Suc_leD \<open>\<And>thesis. (\<And>nj. \<lbrakk>enat nj < llength Ns;
             (C, active) \<in> \<Inter> (snd ` (lnth Ns ` {k. nj \<le> k \<and> enat k < llength Ns}))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis\<close>
             enat_ord_simps(1) le_eq_less_or_eq le_less_trans)
       have "(C, active) \<in> \<Inter> (snd ` (lnth Ns ` {k. njm_prec \<le> k \<and> enat k < llength Ns}))"
       proof -
         {
           fix k
           assume k_in: "njm_prec \<le> k \<and> enat k < llength Ns"
           have "k = njm_prec \<Longrightarrow> (C, active) \<in> snd (lnth Ns k)" using absurd_hyp by simp
           moreover have "njm_prec < k \<Longrightarrow> (C, active) \<in> snd (lnth Ns k)"
             using nj_prec_is in_allk k_in by simp
           ultimately have "(C, active) \<in> snd (lnth Ns k)" using k_in by fastforce
         }
         then show "(C, active) \<in> \<Inter> (snd ` (lnth Ns ` {k. njm_prec \<le> k \<and> enat k < llength Ns}))"
           by blast
       qed
       then have "enat njm_prec < llength Ns \<and>
           (C, active) \<in> \<Inter> (snd ` (lnth Ns ` {k. njm_prec \<le> k \<and> enat k < llength Ns}))"
         using prec_smaller by blast
       then show False
         using nj_min_is nj_prec_is Orderings.wellorder_class.not_less_Least njm_prec_njm by blast
     qed
     then have notin_active_subs_njm_prec: "(C, active) \<notin> active_subset (snd (lnth Ns njm_prec))"
       unfolding active_subset_def by blast
     then show "\<exists>nj. enat (Suc nj) < llength Ns \<and> prems_of \<iota> ! j \<notin> active_subset (snd (lnth Ns nj)) \<and>
         (\<forall>k. k > nj \<longrightarrow> enat k < llength Ns \<longrightarrow> prems_of \<iota> ! j \<in> active_subset (snd (lnth Ns k)))"
       using c_is njm_prec_all_suc njm_prec_smaller_d by (metis (mono_tags, lifting)
           active_subset_def mem_Collect_eq nj_prec_is njm_smaller_D snd_conv)
   qed
   define nj_set where "nj_set = {nj. (\<exists>j\<in>{0..<m}. enat (Suc nj) < llength Ns \<and>
       prems_of \<iota> ! j \<notin> active_subset (snd (lnth Ns nj)) \<and>
       (\<forall>k. k > nj \<longrightarrow> enat k < llength Ns \<longrightarrow> prems_of \<iota> ! j \<in> active_subset (snd (lnth Ns k))))}"
   {
     assume m_null: "m = 0"
     then have "enat 0 < llength Ns \<and> to_F \<iota> \<in> fst (lhd Ns)"
       using no_prems_init_active i_in_F m_def_F zero_enat_def chain_length_pos[OF deriv] by auto
     then have "\<exists>n. enat n < llength Ns \<and> to_F \<iota> \<in> fst (lnth Ns n)"
       unfolding lhd_is by blast
   }
   moreover {
     assume m_pos: "m > 0"
     have nj_not_empty: "nj_set \<noteq> {}"
     proof -
       have zero_in: "0 \<in> {0..<m}" using m_pos by simp
       then obtain n0 where "enat (Suc n0) < llength Ns" and
         "prems_of \<iota> ! 0 \<notin> active_subset (snd (lnth Ns n0))" and
         "\<forall>k>n0. enat k < llength Ns \<longrightarrow> prems_of \<iota> ! 0 \<in> active_subset (snd (lnth Ns k))"
         using exist_nj by fast
       then have "n0 \<in> nj_set" unfolding nj_set_def using zero_in by blast
       then show "nj_set \<noteq> {}" by auto
     qed
     have nj_finite: "finite nj_set"
       using all_ex_finite_set[OF exist_nj] by (metis (no_types, lifting) Suc_ile_eq
           dual_order.strict_implies_order linorder_neqE_nat nj_set_def)
     have "\<exists>n \<in> nj_set. \<forall>nj \<in> nj_set. nj \<le> n"
       using nj_not_empty nj_finite using Max_ge Max_in by blast
     then obtain n where n_in: "n \<in> nj_set" and n_bigger: "\<forall>nj \<in> nj_set. nj \<le> n" by blast
     then obtain j0 where j0_in: "j0 \<in> {0..<m}" and suc_n_length: "enat (Suc n) < llength Ns" and
       j0_notin: "prems_of \<iota> ! j0 \<notin> active_subset (snd (lnth Ns n))" and
       j0_allin: "(\<forall>k. k > n \<longrightarrow> enat k < llength Ns \<longrightarrow>
           prems_of \<iota> ! j0 \<in> active_subset (snd (lnth Ns k)))"
       unfolding nj_set_def by blast
     obtain C0 where C0_is: "prems_of \<iota> ! j0 = (C0, active)"
       using j0_in i_in2 unfolding m_def Inf_from_def active_subset_def
       by (smt Collect_mem_eq Collect_mono_iff atLeastLessThan_iff nth_mem old.prod.exhaust snd_conv)
     then have C0_prems_i: "(C0, active) \<in> set (prems_of \<iota>)" using in_set_conv_nth j0_in m_def by force
     have C0_in: "(C0, active) \<in> (snd (lnth Ns (Suc n)))"
       using C0_is j0_allin suc_n_length by (simp add: active_subset_def)
     have C0_notin: "(C0, active) \<notin> (snd (lnth Ns n))"
       using C0_is j0_notin unfolding active_subset_def by simp
     have step_n: "lnth Ns n \<leadsto>LGC lnth Ns (Suc n)"
       using deriv chain_lnth_rel n_in unfolding nj_set_def by blast
     have is_scheduled: "\<exists>T2 T1 T' N1 N C L N2. lnth Ns n = (T1, N1) \<and> lnth Ns (Suc n) = (T2, N2) \<and>
         T2 = T1 \<union> T' \<and> N1 = N \<union> {(C, L)} \<and> N2 = N \<union> {(C, active)} \<and> L \<noteq> active \<and>
         T' = no_labels.Inf_between (fst ` active_subset N) {C}"
       using step.simps[of "lnth Ns n" "lnth Ns (Suc n)"] step_n C0_in C0_notin
       unfolding active_subset_def by fastforce
     then obtain T2 T1 T' N1 N L N2 where nth_d_is: "lnth Ns n = (T1, N1)" and
       suc_nth_d_is: "lnth Ns (Suc n) = (T2, N2)" and t2_is: "T2 = T1 \<union> T'" and
       n1_is: "N1 = N \<union> {(C0, L)}" "N2 = N \<union> {(C0, active)}" and
       l_not_active: "L \<noteq> active" and
       tp_is: "T' = no_labels.Inf_between (fst ` active_subset N) {C0}"
       using C0_in C0_notin j0_in C0_is using active_subset_def by fastforce
     have "j \<in> {0..<m} \<Longrightarrow> prems_of \<iota> ! j \<noteq> prems_of \<iota> ! j0 \<Longrightarrow> prems_of \<iota> ! j \<in> (active_subset N)"
       for j
     proof -
       fix j
       assume j_in: "j \<in> {0..<m}" and
         j_not_j0: "prems_of \<iota> ! j \<noteq> prems_of \<iota> ! j0"
       obtain nj where nj_len: "enat (Suc nj) < llength Ns" and
         nj_prems: "prems_of \<iota> ! j \<notin> active_subset (snd (lnth Ns nj))" and
         nj_greater: "(\<forall>k. k > nj \<longrightarrow> enat k < llength Ns \<longrightarrow>
             prems_of \<iota> ! j \<in> active_subset (snd (lnth Ns k)))"
         using exist_nj j_in by blast
       then have "nj \<in> nj_set" unfolding nj_set_def using j_in by blast
       moreover have "nj \<noteq> n"
       proof (rule ccontr)
         assume "\<not> nj \<noteq> n"
         then have "prems_of \<iota> ! j = (C0, active)"
           using C0_in C0_notin step.simps[of "lnth Ns n" "lnth Ns (Suc n)"] step_n
             active_subset_def is_scheduled nj_greater nj_prems suc_n_length by auto
         then show False using j_not_j0 C0_is by simp
       qed
       ultimately have "nj < n" using n_bigger by force
       then have "prems_of \<iota> ! j \<in> (active_subset (snd (lnth Ns n)))"
         using nj_greater n_in Suc_ile_eq dual_order.strict_implies_order
         unfolding nj_set_def by blast
       then show "prems_of \<iota> ! j \<in> (active_subset N)"
         using nth_d_is l_not_active n1_is unfolding active_subset_def by force
     qed
     then have prems_i_active: "set (prems_of \<iota>) \<subseteq> active_subset N \<union> {(C0, active)}"
       using C0_prems_i C0_is m_def
       by (metis Un_iff atLeast0LessThan in_set_conv_nth insertCI lessThan_iff subrelI)
     moreover have "\<not> (set (prems_of \<iota>) \<subseteq> active_subset N - {(C0, active)})" using C0_prems_i by blast
     ultimately have "\<iota> \<in> Inf_between (active_subset N) {(C0, active)}"
       using i_in_inf_fl prems_i_active unfolding Inf_between_def Inf_from_def by blast
     then have "to_F \<iota> \<in> no_labels.Inf_between (fst ` (active_subset N)) {C0}"
       unfolding to_F_def Inf_between_def Inf_from_def
         no_labels.Inf_between_def no_labels.Inf_from_def
       using Inf_FL_to_Inf_F by force
     then have i_in_t2: "to_F \<iota> \<in> T2" using tp_is t2_is by simp
     have "j \<in> {0..<m} \<Longrightarrow> (\<forall>k. k > n \<longrightarrow> enat k < llength Ns \<longrightarrow>
         prems_of \<iota> ! j \<in> active_subset (snd (lnth Ns k)))" for j
     proof (cases "j = j0")
       case True
       assume "j = j0"
       then show "(\<forall>k. k > n \<longrightarrow> enat k < llength Ns \<longrightarrow>
           prems_of \<iota> ! j \<in> active_subset (snd (lnth Ns k)))" using j0_allin by simp
     next
       case False
       assume j_in: "j \<in> {0..<m}" and
         "j \<noteq> j0"
       obtain nj where nj_len: "enat (Suc nj) < llength Ns" and
         nj_prems: "prems_of \<iota> ! j \<notin> active_subset (snd (lnth Ns nj))" and
         nj_greater: "(\<forall>k. k > nj \<longrightarrow> enat k < llength Ns \<longrightarrow>
             prems_of \<iota> ! j \<in> active_subset (snd (lnth Ns k)))"
         using exist_nj j_in by blast
       then have "nj \<in> nj_set" unfolding nj_set_def using j_in by blast
       then show "(\<forall>k. k > n \<longrightarrow> enat k < llength Ns \<longrightarrow>
           prems_of \<iota> ! j \<in> active_subset (snd (lnth Ns k)))"
         using nj_greater n_bigger by auto
     qed
     then have allj_allk: "(\<forall>c\<in> set (prems_of \<iota>). (\<forall>k. k > n \<longrightarrow> enat k < llength Ns \<longrightarrow>
         c \<in> active_subset (snd (lnth Ns k))))"
       using m_def by (metis atLeast0LessThan in_set_conv_nth lessThan_iff)
     have "\<forall>c\<in> set (prems_of \<iota>). snd c = active"
       using prems_i_active unfolding active_subset_def by auto
     then have ex_n_i_in: "\<exists>n. enat (Suc n) < llength Ns \<and> to_F \<iota> \<in> fst (lnth Ns (Suc n)) \<and>
         (\<forall>c\<in> set (prems_of \<iota>). snd c = active) \<and>
         (\<forall>c\<in> set (prems_of \<iota>). (\<forall>k. k > n \<longrightarrow> enat k < llength Ns \<longrightarrow>
           c \<in> active_subset (snd (lnth Ns k))))"
       using allj_allk i_in_t2 suc_nth_d_is fstI n_in nj_set_def
       by auto
     then have "\<exists>n. enat n < llength Ns \<and> to_F \<iota> \<in> fst (lnth Ns n) \<and>
         (\<forall>c\<in> set (prems_of \<iota>). snd c = active) \<and> (\<forall>c\<in> set (prems_of \<iota>). (\<forall>k. k \<ge> n \<longrightarrow>
           enat k < llength Ns \<longrightarrow> c \<in> active_subset (snd (lnth Ns k))))"
       by auto
   }
   ultimately obtain n T2 N2 where i_in_suc_n: "to_F \<iota> \<in> fst (lnth Ns n)" and
     all_prems_active_after: "m > 0 \<Longrightarrow> (\<forall>c\<in> set (prems_of \<iota>). (\<forall>k. k \<ge> n \<longrightarrow> enat k < llength Ns \<longrightarrow>
                   c \<in> active_subset (snd (lnth Ns k))))" and
     suc_n_length: "enat n < llength Ns" and suc_nth_d_is: "lnth Ns n = (T2, N2)"
     by (metis less_antisym old.prod.exhaust zero_less_Suc)
   then have i_in_t2: "to_F \<iota> \<in> T2" by simp
   have "\<exists>p\<ge>n. enat (Suc p) < llength Ns \<and> to_F \<iota> \<in> (fst (lnth Ns p)) \<and> to_F \<iota> \<notin> (fst (lnth Ns (Suc p)))"
   proof (rule ccontr)
     assume
       contra: "\<not> (\<exists>p\<ge>n. enat (Suc p) < llength Ns \<and> to_F \<iota> \<in> (fst (lnth Ns p)) \<and>
                      to_F \<iota> \<notin> (fst (lnth Ns (Suc p))))"
     then have i_in_suc: "p0 \<ge> n \<Longrightarrow> enat (Suc p0) < llength Ns \<Longrightarrow> to_F \<iota> \<in> (fst (lnth Ns p0)) \<Longrightarrow>
         to_F \<iota> \<in> (fst (lnth Ns (Suc p0)))" for p0
       by blast
     have "p0 \<ge> n \<Longrightarrow> enat p0 < llength Ns \<Longrightarrow> to_F \<iota> \<in> (fst (lnth Ns p0))" for p0
     proof (induction rule: nat_induct_at_least)
       case base
       then show ?case using i_in_t2 suc_nth_d_is
         by simp
     next
       case (Suc p0)
       assume p_bigger_n: "n \<le> p0" and
         induct_hyp: "enat p0 < llength Ns \<Longrightarrow> to_F \<iota> \<in> fst (lnth Ns p0)" and
         sucsuc_smaller_d: "enat (Suc p0) < llength Ns"
       have suc_p_bigger_n: "n \<le> p0" using p_bigger_n by simp
       have suc_smaller_d: "enat p0 < llength Ns"
         using sucsuc_smaller_d Suc_ile_eq dual_order.strict_implies_order by blast
       then have "to_F \<iota> \<in> fst (lnth Ns p0)" using induct_hyp by blast
       then show ?case using i_in_suc[OF suc_p_bigger_n sucsuc_smaller_d] by blast
     qed
     then have i_in_all_bigger_n: "\<forall>j. j \<ge> n \<and> enat j < llength Ns \<longrightarrow> to_F \<iota> \<in> (fst (lnth Ns j))"
       by presburger
     have "llength (lmap fst Ns) = llength Ns" by force
     then have "to_F \<iota> \<in> \<Inter> (lnth (lmap fst Ns) ` {j. n \<le> j \<and> enat j < llength (lmap fst Ns)})"
       using i_in_all_bigger_n using Suc_le_D by auto
     then have "to_F \<iota> \<in> Liminf_llist (lmap fst Ns)"
       unfolding Liminf_llist_def using suc_n_length by auto
     then show False using final_schedule by fast
   qed
   then obtain p where p_greater_n: "p \<ge> n" and p_smaller_d: "enat (Suc p) < llength Ns" and
     i_in_p: "to_F \<iota> \<in> (fst (lnth Ns p))" and i_notin_suc_p: "to_F \<iota> \<notin> (fst (lnth Ns (Suc p)))"
     by blast
   have p_neq_n: "Suc p \<noteq> n" using i_notin_suc_p i_in_suc_n by blast
   have step_p: "lnth Ns p \<leadsto>LGC lnth Ns (Suc p)" using deriv p_smaller_d chain_lnth_rel by blast
   then have "\<exists>T1 T2 \<iota> N2 N1 M. lnth Ns p = (T1, N1) \<and> lnth Ns (Suc p) = (T2, N2) \<and>
       T1 = T2 \<union> {\<iota>} \<and> N2 = N1 \<union> M \<and> active_subset M = {} \<and>
       \<iota> \<in> no_labels.Red_I_\<G> (fst ` (N1 \<union> M))"
   proof -
     have ci_or_do: "(\<exists>T1 T2 \<iota> N2 N1 M. lnth Ns p = (T1, N1) \<and> lnth Ns (Suc p) = (T2, N2) \<and>
         T1 = T2 \<union> {\<iota>} \<and> N2 = N1 \<union> M \<and> active_subset M = {} \<and>
         \<iota> \<in> no_labels.Red_I_\<G> (fst ` (N1 \<union> M))) \<or>
         (\<exists>T1 T2 T' N. lnth Ns p = (T1, N) \<and> lnth Ns (Suc p) = (T2, N) \<and>
         T1 = T2 \<union> T' \<and> T' \<inter> no_labels.Inf_from (fst ` active_subset N) = {})"
       using step.simps[of "lnth Ns p" "lnth Ns (Suc p)"] step_p i_in_p i_notin_suc_p by fastforce
     then have p_greater_n_strict: "n < Suc p"
       using suc_nth_d_is p_greater_n i_in_t2 i_notin_suc_p le_eq_less_or_eq by force
     have "m > 0 \<Longrightarrow> j \<in> {0..<m} \<Longrightarrow> prems_of (to_F \<iota>) ! j \<in> fst ` active_subset (snd (lnth Ns p))"
       for j
     proof -
       fix j
       assume
         m_pos: "m > 0" and
         j_in: "j \<in> {0..<m}"
       then have "prems_of \<iota> ! j \<in> (active_subset (snd (lnth Ns p)))"
         using all_prems_active_after[OF m_pos] p_smaller_d m_def p_greater_n p_neq_n
         by (meson Suc_ile_eq atLeastLessThan_iff dual_order.strict_implies_order nth_mem
             p_greater_n_strict)
       then have "fst (prems_of \<iota> ! j) \<in> fst ` active_subset (snd (lnth Ns p))"
         by blast
       then show "prems_of (to_F \<iota>) ! j \<in> fst ` active_subset (snd (lnth Ns p))"
         unfolding to_F_def using j_in m_def by simp
     qed
     then have prems_i_active_p: "m > 0 \<Longrightarrow>
         to_F \<iota> \<in> no_labels.Inf_from (fst ` active_subset (snd (lnth Ns p)))"
       using i_in_F unfolding no_labels.Inf_from_def
       by (smt atLeast0LessThan in_set_conv_nth lessThan_iff m_def_F mem_Collect_eq subsetI)
     have "m = 0 \<Longrightarrow> (\<exists>T1 T2 \<iota> N2 N1 M. lnth Ns p = (T1, N1) \<and> lnth Ns (Suc p) = (T2, N2) \<and>
         T1 = T2 \<union> {\<iota>} \<and> N2 = N1 \<union> M \<and> active_subset M = {} \<and>
         \<iota> \<in> no_labels.Red_I_\<G> (fst ` (N1 \<union> M)))"
       using ci_or_do premise_free_inf_always_from[of "to_F \<iota>" "fst ` active_subset _", OF i_in_F]
         m_def i_in_p i_notin_suc_p m_def_F by auto
     then show "(\<exists>T1 T2 \<iota> N2 N1 M. lnth Ns p = (T1, N1) \<and> lnth Ns (Suc p) = (T2, N2) \<and>
         T1 = T2 \<union> {\<iota>} \<and> N2 = N1 \<union> M \<and> active_subset M = {} \<and>
         \<iota> \<in> no_labels.Red_I_\<G> (fst ` (N1 \<union> M)))"
       using ci_or_do i_in_p i_notin_suc_p prems_i_active_p unfolding active_subset_def by force
   qed
   then obtain T1p T2p N1p N2p Mp where  "lnth Ns p = (T1p, N1p)" and
     suc_p_is: "lnth Ns (Suc p) = (T2p, N2p)" and "T1p = T2p \<union> {to_F \<iota>}" and "T2p \<inter> {to_F \<iota>} = {}" and
     n2p_is: "N2p = N1p \<union> Mp"and "active_subset Mp = {}" and
     i_in_red_inf: "to_F \<iota> \<in> no_labels.Red_I_\<G>
         (fst ` (N1p \<union> Mp))"
     using i_in_p i_notin_suc_p by fastforce
   have "to_F \<iota> \<in> no_labels.Red_I (fst ` (snd (lnth Ns (Suc p))))"
     using i_in_red_inf suc_p_is n2p_is by fastforce
   then have "\<forall>q \<in> Q. (\<G>_I_q q (to_F \<iota>) \<noteq> None \<and>
       the (\<G>_I_q q (to_F \<iota>)) \<subseteq> Red_I_q q (\<Union> (\<G>_F_q q ` fst ` snd (lnth Ns (Suc p)))))
       \<or> (\<G>_I_q q (to_F \<iota>) = None \<and>
       \<G>_F_q q (concl_of (to_F \<iota>)) \<subseteq> \<Union> (\<G>_F_q q ` fst ` snd (lnth Ns (Suc p))) \<union>
         Red_F_q q (\<Union> (\<G>_F_q q ` fst ` snd (lnth Ns (Suc p)))))"
     unfolding to_F_def no_labels.Red_I_def no_labels.Red_I_\<G>_q_def by blast
   then have "\<iota> \<in> Red_I_\<G> (snd (lnth Ns (Suc p)))"
     using i_in_inf_fl unfolding Red_I_\<G>_def Red_I_\<G>_q_def by (simp add: to_F_def)
   then show "\<iota> \<in> Sup_llist (lmap Red_I_\<G> (lmap snd Ns))"
     unfolding Sup_llist_def using suc_n_length p_smaller_d by auto
 qed
 
 theorem lgc_complete_Liminf:
   assumes
     deriv: "chain (\<leadsto>LGC) Ns" and
     init_state: "active_subset (snd (lhd Ns)) = {}" and
     final_state: "passive_subset (Liminf_llist (lmap snd Ns)) = {}" and
     no_prems_init_active: "\<forall>\<iota> \<in> Inf_F. prems_of \<iota> = [] \<longrightarrow> \<iota> \<in> fst (lhd Ns)" and
     final_schedule: "Liminf_llist (lmap fst Ns) = {}" and
     b_in: "B \<in> Bot_F" and
     bot_entailed: "no_labels.entails_\<G> (fst ` snd (lhd Ns)) {B}"
   shows "\<exists>BL \<in> Bot_FL. BL \<in> Liminf_llist (lmap snd Ns)"
 proof -
   have labeled_b_in: "(B, active) \<in> Bot_FL" using b_in by simp
   have simp_snd_lmap: "lhd (lmap snd Ns) = snd (lhd Ns)"
     by (rule llist.map_sel(1)[OF chain_not_lnull[OF deriv]])
   have labeled_bot_entailed: "entails_\<G>_L (snd (lhd Ns)) {(B, active)}"
     using labeled_entailment_lifting bot_entailed by fastforce
   have "fair (lmap snd Ns)"
     using lgc_fair[OF deriv init_state final_state no_prems_init_active final_schedule] .
   then show ?thesis
     using dynamically_complete_Liminf labeled_b_in lgc_to_red[OF deriv]
       labeled_bot_entailed simp_snd_lmap std_Red_I_eq
     by presburger
 qed
 
 (* thm:lgc-completeness *)
 theorem lgc_complete:
   assumes
     deriv: "chain (\<leadsto>LGC) Ns" and
     init_state: "active_subset (snd (lhd Ns)) = {}" and
     final_state: "passive_subset (Liminf_llist (lmap snd Ns)) = {}" and
     no_prems_init_active: "\<forall>\<iota> \<in> Inf_F. prems_of \<iota> = [] \<longrightarrow> \<iota> \<in> fst (lhd Ns)" and
     final_schedule: "Liminf_llist (lmap fst Ns) = {}" and
     b_in: "B \<in> Bot_F" and
     bot_entailed: "no_labels.entails_\<G> (fst ` snd (lhd Ns)) {B}"
   shows "\<exists>i. enat i < llength Ns \<and> (\<exists>BL \<in> Bot_FL. BL \<in> snd (lnth Ns i))"
 proof -
   have "\<exists>BL\<in>Bot_FL. BL \<in> Liminf_llist (lmap snd Ns)"
     using assms by (rule lgc_complete_Liminf)
   then show ?thesis
     unfolding Liminf_llist_def by auto
 qed
 
 end
 
 end
diff --git a/thys/Saturation_Framework_Extensions/FO_Ordered_Resolution_Prover_Revisited.thy b/thys/Saturation_Framework_Extensions/FO_Ordered_Resolution_Prover_Revisited.thy
--- a/thys/Saturation_Framework_Extensions/FO_Ordered_Resolution_Prover_Revisited.thy
+++ b/thys/Saturation_Framework_Extensions/FO_Ordered_Resolution_Prover_Revisited.thy
@@ -1,1054 +1,1038 @@
 (*  Title:       Application of the Saturation Framework to Bachmair and Ganzinger's RP
     Author:      Sophie Tourret <stourret at mpi-inf.mpg.de>, 2018-2020
     Author:      Jasmin Blanchette <j.c.blanchette at vu.nl>, 2020
 *)
 
 section \<open>Application of the Saturation Framework to Bachmair and Ganzinger's \textsf{RP}\<close>
 
 theory FO_Ordered_Resolution_Prover_Revisited
   imports
     Ordered_Resolution_Prover.FO_Ordered_Resolution_Prover
     Saturation_Framework.Given_Clause_Architectures
     Clausal_Calculus
     Soundness
 begin
 
 text \<open>The main results about Bachmair and Ganzinger's \textsf{RP} prover, as established in
 Section 4.3 of their \emph{Handbook} chapter and formalized by Schlichtkrull et al., are re-proved
 here using the saturation framework of Waldmann et al.\<close>
 
 
 subsection \<open>Setup\<close>
 
 no_notation true_lit (infix "\<Turnstile>l" 50)
 no_notation true_cls (infix "\<Turnstile>" 50)
 no_notation true_clss (infix "\<Turnstile>s" 50)
 no_notation true_cls_mset (infix "\<Turnstile>m" 50)
 
 hide_type (open) Inference_System.inference
 
 hide_const (open) Inference_System.Infer Inference_System.main_prem_of
   Inference_System.side_prems_of Inference_System.prems_of Inference_System.concl_of
   Inference_System.concls_of Inference_System.infer_from
 
 type_synonym 'a old_inference = "'a Inference_System.inference"
 
 abbreviation "old_Infer \<equiv> Inference_System.Infer"
 abbreviation "old_side_prems_of \<equiv> Inference_System.side_prems_of"
 abbreviation "old_main_prem_of \<equiv> Inference_System.main_prem_of"
 abbreviation "old_concl_of \<equiv> Inference_System.concl_of"
 abbreviation "old_prems_of \<equiv> Inference_System.prems_of"
 abbreviation "old_concls_of \<equiv> Inference_System.concls_of"
 abbreviation "old_infer_from \<equiv> Inference_System.infer_from"
 
 lemmas old_infer_from_def = Inference_System.infer_from_def
 
 
 subsection \<open>Library\<close>
 
 lemma set_zip_replicate_right[simp]:
   "set (zip xs (replicate (length xs) y)) = (\<lambda>x. (x, y)) ` set xs"
   by (induct xs) auto
 
 
 subsection \<open>Ground Layer\<close>
 
 context FO_resolution_prover
 begin
 
 no_notation RP (infix "\<leadsto>" 50)
 notation RP (infix "\<leadsto>RP" 50)
 
 interpretation gr: ground_resolution_with_selection "S_M S M"
   using selection_axioms by unfold_locales (fact S_M_selects_subseteq S_M_selects_neg_lits)+
 
 definition G_Inf :: "'a clause set \<Rightarrow> 'a clause inference set" where
   "G_Inf M = {Infer (CAs @ [DA]) E |CAs DA AAs As E. gr.ord_resolve M CAs DA AAs As E}"
 
 lemma G_Inf_have_prems: "\<iota> \<in> G_Inf M \<Longrightarrow> prems_of \<iota> \<noteq> []"
   unfolding G_Inf_def by auto
 
 lemma G_Inf_reductive: "\<iota> \<in> G_Inf M \<Longrightarrow> concl_of \<iota> < main_prem_of \<iota>"
   unfolding G_Inf_def by (auto dest: gr.ord_resolve_reductive)
 
 interpretation G: sound_inference_system "G_Inf M" "{{#}}" "(\<TTurnstile>e)"
 proof
   fix \<iota>
   assume i_in: "\<iota> \<in> G_Inf M"
   moreover
   {
     fix I
     assume I_ent_prems: "I \<TTurnstile>s set (prems_of \<iota>)"
     obtain CAs AAs As where
       the_inf: "gr.ord_resolve M CAs (main_prem_of \<iota>) AAs As (concl_of \<iota>)" and
       CAs: "CAs = side_prems_of \<iota>"
       using i_in unfolding G_Inf_def by auto
     then have "I \<TTurnstile> concl_of \<iota>"
       using gr.ord_resolve_sound[of M CAs "main_prem_of \<iota>" AAs As "concl_of \<iota>" I]
       by (metis I_ent_prems G_Inf_have_prems i_in insert_is_Un set_mset_mset set_prems_of
           true_clss_insert true_clss_set_mset)
   }
   ultimately show "set (inference.prems_of \<iota>) \<TTurnstile>e {concl_of \<iota>}"
     by simp
 qed
 
 interpretation G: clausal_counterex_reducing_inference_system "G_Inf M" "gr.INTERP M"
 proof
   fix N D
   assume
     "{#} \<notin> N" and
     "D \<in> N" and
     "\<not> gr.INTERP M N \<TTurnstile> D" and
     "\<And>C. C \<in> N \<Longrightarrow> \<not> gr.INTERP M N \<TTurnstile> C \<Longrightarrow> D \<le> C"
   then obtain CAs AAs As E where
     cas_in: "set CAs \<subseteq> N" and
     n_mod_cas: "gr.INTERP M N \<TTurnstile>m mset CAs" and
     ca_prod: "\<And>CA. CA \<in> set CAs \<Longrightarrow> gr.production M N CA \<noteq> {}" and
     e_res: "gr.ord_resolve M CAs D AAs As E" and
     n_nmod_e: "\<not> gr.INTERP M N \<TTurnstile> E" and
     e_lt_d: "E < D"
     using gr.ord_resolve_counterex_reducing by blast
   define \<iota> where
     "\<iota> = Infer (CAs @ [D]) E"
 
   have "\<iota> \<in> G_Inf M"
     unfolding \<iota>_def G_Inf_def using e_res by auto
   moreover have "prems_of \<iota> \<noteq> []"
     unfolding \<iota>_def by simp
   moreover have "main_prem_of \<iota> = D"
     unfolding \<iota>_def by simp
   moreover have "set (side_prems_of \<iota>) \<subseteq> N"
     unfolding \<iota>_def using cas_in by simp
   moreover have "gr.INTERP M N \<TTurnstile>s set (side_prems_of \<iota>)"
     unfolding \<iota>_def using n_mod_cas ca_prod by (simp add: gr.productive_imp_INTERP true_clss_def)
   moreover have "\<not> gr.INTERP M N \<TTurnstile> concl_of \<iota>"
     unfolding \<iota>_def using n_nmod_e by simp
   moreover have "concl_of \<iota> < D"
     unfolding \<iota>_def using e_lt_d by simp
   ultimately show "\<exists>\<iota> \<in> G_Inf M. prems_of \<iota> \<noteq> [] \<and> main_prem_of \<iota> = D \<and> set (side_prems_of \<iota>) \<subseteq> N \<and>
     gr.INTERP M N \<TTurnstile>s set (side_prems_of \<iota>) \<and> \<not> gr.INTERP M N \<TTurnstile> concl_of \<iota> \<and> concl_of \<iota> < D"
     by blast
 qed
 
 interpretation G: clausal_counterex_reducing_calculus_with_standard_redundancy "G_Inf M"
   "gr.INTERP M"
   by (unfold_locales, fact G_Inf_have_prems, fact G_Inf_reductive)
 
 interpretation G: statically_complete_calculus "{{#}}" "G_Inf M" "(\<TTurnstile>e)" "G.Red_I M" G.Red_F
   by unfold_locales (use G.clausal_saturated_complete in blast)
 
 
 subsection \<open>First-Order Layer\<close>
 
 abbreviation \<G>_F :: \<open>'a clause \<Rightarrow> 'a clause set\<close> where
   \<open>\<G>_F \<equiv> grounding_of_cls\<close>
 
 abbreviation \<G>_Fs :: \<open>'a clause set \<Rightarrow> 'a clause set\<close> where
   \<open>\<G>_Fs \<equiv> grounding_of_clss\<close>
 
 lemmas \<G>_F_def = grounding_of_cls_def
 lemmas \<G>_Fs_def = grounding_of_clss_def
 
 definition \<G>_I :: \<open>'a clause set \<Rightarrow> 'a clause inference \<Rightarrow> 'a clause inference set\<close> where
   \<open>\<G>_I M \<iota> = {Infer (prems_of \<iota> \<cdot>\<cdot>cl \<rho>s) (concl_of \<iota> \<cdot> \<rho>) |\<rho> \<rho>s.
      is_ground_subst_list \<rho>s \<and> is_ground_subst \<rho>
      \<and> Infer (prems_of \<iota> \<cdot>\<cdot>cl \<rho>s) (concl_of \<iota> \<cdot> \<rho>) \<in> G_Inf M}\<close>
 
 abbreviation
   \<G>_I_opt :: \<open>'a clause set \<Rightarrow> 'a clause inference \<Rightarrow> 'a clause inference set option\<close>
 where
   \<open>\<G>_I_opt M \<iota> \<equiv> Some (\<G>_I M \<iota>)\<close>
 
 definition F_Inf :: "'a clause inference set" where
   "F_Inf = {Infer (CAs @ [DA]) E | CAs DA AAs As \<sigma> E. ord_resolve_rename S CAs DA AAs As \<sigma> E}"
 
 lemma F_Inf_have_prems: "\<iota> \<in> F_Inf \<Longrightarrow> prems_of \<iota> \<noteq> []"
   unfolding F_Inf_def by force
 
 interpretation F: lifting_intersection F_Inf "{{#}}" UNIV G_Inf "\<lambda>N. (\<TTurnstile>e)" G.Red_I "\<lambda>N. G.Red_F"
   "{{#}}" "\<lambda>N. \<G>_F" \<G>_I_opt "\<lambda>D C C'. False"
 proof (unfold_locales; (intro ballI)?)
   show "UNIV \<noteq> {}"
     by (rule UNIV_not_empty)
 next
   show "consequence_relation {{#}} (\<TTurnstile>e)"
     by (fact consequence_relation_axioms)
 next
   show "\<And>M. tiebreaker_lifting {{#}} F_Inf {{#}} (\<TTurnstile>e) (G_Inf M) (G.Red_I M) G.Red_F \<G>_F (\<G>_I_opt M)
     (\<lambda>D C C'. False)"
   proof
     fix M \<iota>
     show "the (\<G>_I_opt M \<iota>) \<subseteq> G.Red_I M (\<G>_F (concl_of \<iota>))"
       unfolding option.sel
     proof
       fix \<iota>'
       assume "\<iota>' \<in> \<G>_I M \<iota>"
       then obtain \<rho> \<rho>s where
         \<iota>': "\<iota>' = Infer (prems_of \<iota> \<cdot>\<cdot>cl \<rho>s) (concl_of \<iota> \<cdot> \<rho>)" and
         \<rho>_gr: "is_ground_subst \<rho>" and
         \<rho>_infer: "Infer (prems_of \<iota> \<cdot>\<cdot>cl \<rho>s) (concl_of \<iota> \<cdot> \<rho>) \<in> G_Inf M"
         unfolding \<G>_I_def by blast
 
       show "\<iota>' \<in> G.Red_I M (\<G>_F (concl_of \<iota>))"
         unfolding G.Red_I_def G.redundant_infer_def mem_Collect_eq using \<iota>' \<rho>_gr \<rho>_infer
         by (metis inference.sel(2) G_Inf_reductive empty_iff ground_subst_ground_cls
             grounding_of_cls_ground insert_iff subst_cls_eq_grounding_of_cls_subset_eq
             true_clss_union)
     qed
   qed (auto simp: \<G>_F_def ex_ground_subst)
 qed
 
 notation F.entails_\<G> (infix "\<TTurnstile>\<G>e" 50)
 
 lemma F_entails_\<G>_iff: "N1 \<TTurnstile>\<G>e N2 \<longleftrightarrow> \<Union> (\<G>_F ` N1) \<TTurnstile>e \<Union> (\<G>_F ` N2)"
   unfolding F.entails_\<G>_def by simp
 
-lemma true_Union_grounding_of_cls_iff_true_all_interps_ground_substs:
+lemma true_Union_grounding_of_cls_iff:
   "I \<TTurnstile>s (\<Union>C \<in> N. {C \<cdot> \<sigma> |\<sigma>. is_ground_subst \<sigma>}) \<longleftrightarrow> (\<forall>\<sigma>. is_ground_subst \<sigma> \<longrightarrow> I \<TTurnstile>s N \<cdot>cs \<sigma>)"
   unfolding true_clss_def subst_clss_def by blast
 
 interpretation F: sound_inference_system F_Inf "{{#}}" "(\<TTurnstile>\<G>e)"
 proof
   fix \<iota>
   assume i_in: "\<iota> \<in> F_Inf"
   moreover
   {
     fix I \<eta>
     assume
       I_entails_prems: "\<forall>\<sigma>. is_ground_subst \<sigma> \<longrightarrow> I \<TTurnstile>s set (prems_of \<iota>) \<cdot>cs \<sigma>" and
       \<eta>_gr: "is_ground_subst \<eta>"
     obtain CAs AAs As \<sigma> where
       the_inf: "ord_resolve_rename S CAs (main_prem_of \<iota>) AAs As \<sigma> (concl_of \<iota>)" and
       CAs: "CAs = side_prems_of \<iota>"
       using i_in unfolding F_Inf_def by auto
     have prems: "mset (prems_of \<iota>) = mset (side_prems_of \<iota>) + {#main_prem_of \<iota>#}"
       by (metis (no_types) F_Inf_have_prems[OF i_in] add.right_neutral append_Cons append_Nil2
           append_butlast_last_id mset.simps(2) mset_rev mset_single_iff_right rev_append
           rev_is_Nil_conv union_mset_add_mset_right)
     have "I \<TTurnstile> concl_of \<iota> \<cdot> \<eta>"
       using ord_resolve_rename_sound[OF the_inf, of I \<eta>, OF _ \<eta>_gr]
       unfolding CAs prems[symmetric] using I_entails_prems
       by (metis set_mset_mset set_mset_subst_cls_mset_subst_clss true_clss_set_mset)
   }
   ultimately show "set (inference.prems_of \<iota>) \<TTurnstile>\<G>e {concl_of \<iota>}"
-    unfolding F.entails_\<G>_def \<G>_F_def
-      true_Union_grounding_of_cls_iff_true_all_interps_ground_substs
-    by auto
+    unfolding F.entails_\<G>_def \<G>_F_def true_Union_grounding_of_cls_iff by auto
 qed
 
-lemma G_Inf_overapproximates_F_Inf:
-  "\<iota>\<^sub>0 \<in> G.Inf_from M (\<Union> (\<G>_F ` M)) \<Longrightarrow> \<exists>\<iota> \<in> F.Inf_from M. \<iota>\<^sub>0 \<in> \<G>_I M \<iota>"
+lemma G_Inf_overapprox_F_Inf: "\<iota>\<^sub>0 \<in> G.Inf_from M (\<Union> (\<G>_F ` M)) \<Longrightarrow> \<exists>\<iota> \<in> F.Inf_from M. \<iota>\<^sub>0 \<in> \<G>_I M \<iota>"
 proof -
   assume \<iota>\<^sub>0_in: "\<iota>\<^sub>0 \<in> G.Inf_from M (\<Union> (\<G>_F ` M))"
   have prems_\<iota>\<^sub>0_in: "set (prems_of \<iota>\<^sub>0) \<subseteq> \<Union> (\<G>_F ` M)"
     using \<iota>\<^sub>0_in unfolding G.Inf_from_def by simp
   note \<iota>\<^sub>0_G_Inf = G.Inf_if_Inf_from[OF \<iota>\<^sub>0_in]
   then obtain CAs DA AAs As E where
     gr_res: \<open>gr.ord_resolve M CAs DA AAs As E\<close> and
     \<iota>\<^sub>0_is: \<open>\<iota>\<^sub>0 = Infer (CAs @ [DA]) E\<close>
     unfolding G_Inf_def by auto
 
   have CAs_in: \<open>set CAs \<subseteq> set (prems_of \<iota>\<^sub>0)\<close>
     by (simp add: \<iota>\<^sub>0_is subsetI)
   then have ground_CAs: \<open>is_ground_cls_list CAs\<close>
     using prems_\<iota>\<^sub>0_in union_grounding_of_cls_ground is_ground_cls_list_def is_ground_clss_def by auto
   have DA_in: \<open>DA \<in> set (prems_of \<iota>\<^sub>0)\<close>
     using \<iota>\<^sub>0_is by simp
   then have ground_DA: \<open>is_ground_cls DA\<close>
     using prems_\<iota>\<^sub>0_in union_grounding_of_cls_ground is_ground_clss_def by auto
   obtain \<sigma> where
     grounded_res: \<open>ord_resolve (S_M S M) CAs DA AAs As \<sigma> E\<close>
     using ground_ord_resolve_imp_ord_resolve[OF ground_DA ground_CAs
         gr.ground_resolution_with_selection_axioms gr_res] by auto
   have prems_ground: \<open>{DA} \<union> set CAs \<subseteq> \<G>_Fs M\<close>
     using prems_\<iota>\<^sub>0_in CAs_in DA_in unfolding \<G>_Fs_def by fast
 
   obtain \<eta>s \<eta> \<eta>2 CAs0 DA0 AAs0 As0 E0 \<tau> where
     ground_n: "is_ground_subst \<eta>" and
     ground_ns: "is_ground_subst_list \<eta>s" and
     ground_n2: "is_ground_subst \<eta>2" and
     ngr_res: "ord_resolve_rename S CAs0 DA0 AAs0 As0 \<tau> E0" and
     CAs0_is: "CAs0 \<cdot>\<cdot>cl \<eta>s = CAs" and
     DA0_is: "DA0 \<cdot> \<eta> = DA" and
     E0_is: "E0 \<cdot> \<eta>2 = E"  and
     prems_in: "{DA0} \<union> set CAs0 \<subseteq> M" and
     len_CAs0: "length CAs0 = length CAs" and
     len_ns: "length \<eta>s = length CAs"
     using ord_resolve_rename_lifting[OF _ grounded_res selection_axioms prems_ground] sel_stable
     by smt
 
   have "length CAs0 = length \<eta>s"
     using len_CAs0 len_ns by simp
   then have \<iota>\<^sub>0_is': "\<iota>\<^sub>0 = Infer ((CAs0 @ [DA0]) \<cdot>\<cdot>cl (\<eta>s @ [\<eta>])) (E0 \<cdot> \<eta>2)"
     unfolding \<iota>\<^sub>0_is by (auto simp: CAs0_is[symmetric] DA0_is[symmetric] E0_is[symmetric])
 
   define \<iota> :: "'a clause inference" where
     "\<iota> = Infer (CAs0 @ [DA0]) E0"
 
   have i_F_Inf: \<open>\<iota> \<in> F_Inf\<close>
     unfolding \<iota>_def F_Inf_def using ngr_res by auto
-
   have "\<exists>\<rho> \<rho>s. \<iota>\<^sub>0 = Infer ((CAs0 @ [DA0]) \<cdot>\<cdot>cl \<rho>s) (E0 \<cdot> \<rho>) \<and> is_ground_subst_list \<rho>s
     \<and> is_ground_subst \<rho> \<and> Infer ((CAs0 @ [DA0]) \<cdot>\<cdot>cl \<rho>s) (E0 \<cdot> \<rho>) \<in> G_Inf M"
     by (rule exI[of _ \<eta>2], rule exI[of _ "\<eta>s @ [\<eta>]"], use ground_ns in
         \<open>auto intro: ground_n ground_n2 \<iota>\<^sub>0_G_Inf[unfolded \<iota>\<^sub>0_is']
            simp: \<iota>\<^sub>0_is' is_ground_subst_list_def\<close>)
   then have \<open>\<iota>\<^sub>0 \<in> \<G>_I M \<iota>\<close>
     unfolding \<G>_I_def \<iota>_def CAs0_is[symmetric] DA0_is[symmetric] E0_is[symmetric] by simp
   moreover have \<open>\<iota> \<in> F.Inf_from M\<close>
     using prems_in i_F_Inf unfolding F.Inf_from_def \<iota>_def by simp
   ultimately show ?thesis
     by blast
 qed
 
 interpretation F: statically_complete_calculus "{{#}}" F_Inf "(\<TTurnstile>\<G>e)" F.Red_I_\<G> F.Red_F_\<G>_empty
 proof (rule F.stat_ref_comp_to_non_ground_fam_inter; clarsimp; (intro exI)?)
   show "\<And>M. statically_complete_calculus {{#}} (G_Inf M) (\<TTurnstile>e) (G.Red_I M) G.Red_F"
     by (fact G.statically_complete_calculus_axioms)
 next
   fix N
   assume "F.saturated N"
   show "F.ground.Inf_from_q N (\<Union> (\<G>_F ` N)) \<subseteq> {\<iota>. \<exists>\<iota>' \<in> F.Inf_from N. \<iota> \<in> \<G>_I N \<iota>'}
     \<union> G.Red_I N (\<Union> (\<G>_F ` N))"
-    using G_Inf_overapproximates_F_Inf unfolding F.ground.Inf_from_q_def \<G>_I_def by fastforce
+    using G_Inf_overapprox_F_Inf unfolding F.ground.Inf_from_q_def \<G>_I_def by fastforce
 qed
 
 
 subsection \<open>Labeled First-Order or Given Clause Layer\<close>
 
-datatype label =
-  New
-| Processed
-| Old
+datatype label = New | Processed | Old
 
 definition FL_Infer_of :: "'a clause inference \<Rightarrow> ('a clause \<times> label) inference set" where
   "FL_Infer_of \<iota> = {Infer Cls (D, New) |Cls D. \<iota> = Infer (map fst Cls) D}"
 
 definition FL_Inf :: "('a clause \<times> label) inference set" where
   "FL_Inf = (\<Union>\<iota> \<in> F_Inf. FL_Infer_of \<iota>)"
 
 abbreviation F_Equiv :: "'a clause \<Rightarrow> 'a clause \<Rightarrow> bool" (infix "\<doteq>" 50) where
   "C \<doteq> D \<equiv> generalizes C D \<and> generalizes D C"
 
 abbreviation F_Prec :: "'a clause \<Rightarrow> 'a clause \<Rightarrow> bool" (infix "\<prec>\<cdot>" 50) where
   "C \<prec>\<cdot> D \<equiv> strictly_generalizes C D"
 
 fun L_Prec :: "label \<Rightarrow> label \<Rightarrow> bool" (infix "\<sqsubset>l" 50) where
   "Old \<sqsubset>l l \<longleftrightarrow> l \<noteq> Old"
 | "Processed \<sqsubset>l l \<longleftrightarrow> l = New"
 | "New \<sqsubset>l l \<longleftrightarrow> False"
 
 lemma irrefl_L_Prec: "\<not> l \<sqsubset>l l"
   by (cases l) auto
 
 lemma trans_L_Prec: "l1 \<sqsubset>l l2 \<Longrightarrow> l2 \<sqsubset>l l3 \<Longrightarrow> l1 \<sqsubset>l l3"
   by (cases l1; cases l2; cases l3) auto
 
 lemma wf_L_Prec: "wfP (\<sqsubset>l)"
   by (metis L_Prec.elims(2) L_Prec.simps(3) not_accp_down wfP_accp_iff)
 
 interpretation FL: given_clause "{{#}}" F_Inf "{{#}}" UNIV "\<lambda>N. (\<TTurnstile>e)" G_Inf G.Red_I
   "\<lambda>N. G.Red_F" "\<lambda>N. \<G>_F" \<G>_I_opt FL_Inf "(\<doteq>)" "(\<prec>\<cdot>)" "(\<sqsubset>l)" Old
 proof (unfold_locales; (intro ballI)?)
   show "equivp (\<doteq>)"
     unfolding equivp_def by (meson generalizes_refl generalizes_trans)
 next
   show "po_on (\<prec>\<cdot>) UNIV"
     unfolding po_on_def irreflp_on_def transp_on_def
     using strictly_generalizes_irrefl strictly_generalizes_trans by auto
 next
   show "wfp_on (\<prec>\<cdot>) UNIV"
     unfolding wfp_on_UNIV by (metis wf_strictly_generalizes)
 next
   show "po_on (\<sqsubset>l) UNIV"
     unfolding po_on_def irreflp_on_def transp_on_def using irrefl_L_Prec trans_L_Prec by blast
 next
   show "wfp_on (\<sqsubset>l) UNIV"
     unfolding wfp_on_UNIV by (rule wf_L_Prec)
 next
   fix C1 D1 C2 D2
   assume
     "C1 \<doteq> D1"
     "C2 \<doteq> D2"
     "C1 \<prec>\<cdot> C2"
   then show "D1 \<prec>\<cdot> D2"
     by (smt antisym size_mset_mono size_subst strictly_generalizes_def generalizes_def
         generalizes_trans)
 next
   fix N C1 C2
   assume "C1 \<doteq> C2"
   then show "\<G>_F C1 \<subseteq> \<G>_F C2"
     unfolding generalizes_def \<G>_F_def by clarsimp (metis is_ground_comp_subst subst_cls_comp_subst)
 next
   fix N C2 C1
   assume "C2 \<prec>\<cdot> C1"
   then show "\<G>_F C1 \<subseteq> \<G>_F C2"
     unfolding strictly_generalizes_def generalizes_def \<G>_F_def
     by clarsimp (metis is_ground_comp_subst subst_cls_comp_subst)
 next
   show "\<exists>l. L_Prec Old l"
     using L_Prec.simps(1) by blast
 qed (auto simp: FL_Inf_def FL_Infer_of_def F_Inf_have_prems)
 
 notation FL.Prec_FL (infix "\<sqsubset>" 50)
 notation FL.entails_\<G>_L (infix "\<TTurnstile>\<G>Le" 50)
-notation FL.derive (infix "\<rhd>RedL" 50)
+notation FL.derive (infix "\<rhd>L" 50)
 notation FL.step (infix "\<leadsto>GC" 50)
 
 lemma FL_Red_F_eq:
   "FL.Red_F N =
    {C. \<forall>D \<in> \<G>_F (fst C). D \<in> G.Red_F (\<Union> (\<G>_F ` fst ` N)) \<or> (\<exists>E \<in> N. E \<sqsubset> C \<and> D \<in> \<G>_F (fst E))}"
   unfolding FL.Red_F_def FL.Red_F_\<G>_q_def by auto
 
 lemma mem_FL_Red_F_because_G_Red_F:
   "(\<forall>D \<in> \<G>_F (fst Cl). D \<in> G.Red_F (\<Union> (\<G>_F ` fst ` N))) \<Longrightarrow> Cl \<in> FL.Red_F N"
   unfolding FL_Red_F_eq by auto
 
 lemma mem_FL_Red_F_because_Prec_FL:
   "(\<forall>D \<in> \<G>_F (fst Cl). \<exists>El \<in> N. El \<sqsubset> Cl \<and> D \<in> \<G>_F (fst El)) \<Longrightarrow> Cl \<in> FL.Red_F N"
   unfolding FL_Red_F_eq by auto
 
 interpretation FL: compact_consequence_relation FL.Bot_FL "(\<TTurnstile>\<G>Le)"
 proof
   fix CCl
   assume unsat: "CCl \<TTurnstile>\<G>Le FL.Bot_FL"
 
   let ?bot = "({#}, undefined)"
 
   have "CCl \<TTurnstile>\<G>Le {?bot}"
     using unsat by (metis (lifting) FL.entail_set_all_formulas UNIV_I insertI1 mem_Sigma_iff)
   then have "\<not> satisfiable (\<Union>CL \<in> CCl. \<G>_F (fst CL))"
     unfolding FL.labeled_entailment_lifting F_entails_\<G>_iff by auto
   then obtain DD where
     d_sub: "DD \<subseteq> (\<Union>Cl \<in> CCl. \<G>_F (fst Cl))" and
     d_fin: "finite DD" and
     d_unsat: "\<forall>I. \<not> I \<TTurnstile>s DD"
     unfolding clausal_logic_compact[of "\<Union>CL \<in> CCl. \<G>_F (fst CL)"] by blast
 
   define CCl' :: "('a clause \<times> label) set" where
     "CCl' = {SOME Cl. Cl \<in> CCl \<and> D \<in> \<G>_F (fst Cl) |D. D \<in> DD}"
 
   have ex_in_cl: "\<exists>Cl. Cl \<in> CCl \<and> D \<in> \<G>_F (fst Cl)" if "D \<in> DD" for D
     using that d_sub by blast
   then have d_sub': "DD \<subseteq> (\<Union>Cl \<in> CCl'. \<G>_F (fst Cl))"
     using ex_in_cl unfolding CCl'_def by clarsimp (metis (lifting) eq_fst_iff ex_in_cl someI_ex)
   have "CCl' \<subseteq> CCl"
     unfolding CCl'_def using someI_ex[OF ex_in_cl] by blast
   moreover have "finite CCl'"
     unfolding CCl'_def using d_fin by simp
   moreover have "CCl' \<TTurnstile>\<G>Le FL.Bot_FL"
     unfolding CCl'_def using d_unsat ex_in_cl d_sub' CCl'_def
     by (metis (no_types, lifting) FL.entails_\<G>_L_def subsetD true_clss_def)
   ultimately show "\<exists>CCl' \<subseteq> CCl. finite CCl' \<and> CCl' \<TTurnstile>\<G>Le FL.Bot_FL"
     by blast
 qed
 
 interpretation FL: refutationally_compact_calculus FL.Bot_FL FL_Inf "(\<TTurnstile>\<G>Le)" FL.Red_I
   FL.Red_F
   ..
 
 
 subsection \<open>Resolution Prover Layer\<close>
 
 interpretation sq: selection "S_Q Sts"
   unfolding S_Q_def using S_M_selects_subseteq S_M_selects_neg_lits selection_axioms
   by unfold_locales auto
 
 interpretation gd: ground_resolution_with_selection "S_Q Sts"
   by unfold_locales
 
-interpretation src: standard_redundancy_criterion_reductive "gd.ord_\<Gamma> Sts"
-  by unfold_locales
-
 interpretation src: standard_redundancy_criterion_counterex_reducing "gd.ord_\<Gamma> Sts"
   "ground_resolution_with_selection.INTERP (S_Q Sts)"
   by unfold_locales
 
 definition lclss_of_state :: "'a state \<Rightarrow> ('a clause \<times> label) set" where
   "lclss_of_state St =
    (\<lambda>C. (C, New)) ` N_of_state St \<union> (\<lambda>C. (C, Processed)) ` P_of_state St
    \<union> (\<lambda>C. (C, Old)) ` Q_of_state St"
 
 lemma image_hd_lclss_of_state[simp]: "fst ` lclss_of_state St = clss_of_state St"
   unfolding lclss_of_state_def by (auto simp: image_Un image_comp)
 
 lemma insert_lclss_of_state[simp]:
   "insert (C, New) (lclss_of_state (N, P, Q)) = lclss_of_state (N \<union> {C}, P, Q)"
   "insert (C, Processed) (lclss_of_state (N, P, Q)) = lclss_of_state (N, P \<union> {C}, Q)"
   "insert (C, Old) (lclss_of_state (N, P, Q)) = lclss_of_state (N, P, Q \<union> {C})"
   unfolding lclss_of_state_def image_def by auto
 
 lemma union_lclss_of_state[simp]:
   "lclss_of_state (N1, P1, Q1) \<union> lclss_of_state (N2, P2, Q2) =
    lclss_of_state (N1 \<union> N2, P1 \<union> P2, Q1 \<union> Q2)"
   unfolding lclss_of_state_def by auto
 
 lemma mem_lclss_of_state[simp]:
   "(C, New) \<in> lclss_of_state (N, P, Q) \<longleftrightarrow> C \<in> N"
   "(C, Processed) \<in> lclss_of_state (N, P, Q) \<longleftrightarrow> C \<in> P"
   "(C, Old) \<in> lclss_of_state (N, P, Q) \<longleftrightarrow> C \<in> Q"
   unfolding lclss_of_state_def image_def by auto
 
 lemma lclss_Liminf_commute:
   "Liminf_llist (lmap lclss_of_state Sts) = lclss_of_state (Liminf_state Sts)"
 proof -
   have \<open>Liminf_llist (lmap lclss_of_state Sts) =
     (\<lambda>C. (C, New)) ` Liminf_llist (lmap N_of_state Sts) \<union>
     (\<lambda>C. (C, Processed)) ` Liminf_llist (lmap P_of_state Sts) \<union>
     (\<lambda>C. (C, Old)) ` Liminf_llist (lmap Q_of_state Sts)\<close>
     unfolding lclss_of_state_def using Liminf_llist_lmap_union Liminf_llist_lmap_image
     by (smt Pair_inject Un_iff disjoint_iff_not_equal imageE inj_onI label.simps(1,3,5)
         llist.map_cong)
  then show ?thesis
    unfolding lclss_of_state_def Liminf_state_def by auto
 qed
 
 lemma GC_tautology_step:
   assumes tauto: "Neg A \<in># C" "Pos A \<in># C"
   shows "lclss_of_state (N \<union> {C}, P, Q) \<leadsto>GC lclss_of_state (N, P, Q)"
 proof -
   have c\<theta>_red: "C\<theta> \<in> G.Red_F (\<Union>D \<in> N'. \<G>_F (fst D))" if in_g: "C\<theta> \<in> \<G>_F C"
     for N' :: "('a clause \<times> label) set" and C\<theta>
   proof -
     obtain \<theta> where
       "C\<theta> = C \<cdot> \<theta>"
        using in_g unfolding \<G>_F_def by blast
     then have "Neg (A \<cdot>a \<theta>) \<in># C\<theta>" and "Pos (A \<cdot>a \<theta>) \<in># C\<theta>"
       using tauto Neg_Melem_subst_atm_subst_cls Pos_Melem_subst_atm_subst_cls by auto
     then have "{} \<TTurnstile>e {C\<theta>}"
       unfolding true_clss_def true_cls_def true_lit_def if_distrib_fun
       by (metis literal.disc literal.sel singletonD)
     then show ?thesis
       unfolding G.Red_F_def by auto
   qed
 
   show ?thesis
   proof (rule FL.step.process[of _ "lclss_of_state (N, P, Q)" "{(C, New)}" _ "{}"])
     show \<open>{(C, New)} \<subseteq> FL.Red_F_\<G> (lclss_of_state (N, P, Q) \<union> {})\<close>
       using mem_FL_Red_F_because_G_Red_F c\<theta>_red[of _ "lclss_of_state (N, P, Q)"]
       unfolding lclss_of_state_def by auto
   qed (auto simp: lclss_of_state_def FL.active_subset_def)
 qed
 
 lemma GC_subsumption_step:
   assumes
     d_in: "Dl \<in> N" and
     d_sub_c: "strictly_subsumes (fst Dl) (fst Cl) \<or> subsumes (fst Dl) (fst Cl) \<and> snd Dl \<sqsubset>l snd Cl"
   shows "N \<union> {Cl} \<leadsto>GC N"
 proof -
   have d_sub'_c: "Cl \<in> FL.Red_F {Dl} \<or> Dl \<sqsubset> Cl"
   proof (cases "size (fst Dl) = size (fst Cl)")
     case True
       assume sizes_eq: \<open>size (fst Dl) = size (fst Cl)\<close>
       have \<open>size (fst Dl) = size (fst Cl) \<Longrightarrow>
         strictly_subsumes (fst Dl) (fst Cl) \<or> subsumes (fst Dl) (fst Cl) \<and> snd Dl \<sqsubset>l snd Cl \<Longrightarrow>
         Dl \<sqsubset> Cl\<close>
         unfolding FL.Prec_FL_def
         unfolding generalizes_def strictly_generalizes_def strictly_subsumes_def subsumes_def
         by (metis size_subst subset_mset.order_refl subseteq_mset_size_eql)
     then have "Dl \<sqsubset> Cl"
       using sizes_eq d_sub_c by auto
     then show ?thesis
       by (rule disjI2)
   next
     case False
     then have d_ssub_c: "strictly_subsumes (fst Dl) (fst Cl)"
       using d_sub_c unfolding strictly_subsumes_def subsumes_def
       by (metis size_subst strict_subset_subst_strictly_subsumes strictly_subsumes_antisym
           subset_mset.antisym_conv2)
     have "Cl \<in> FL.Red_F {Dl}"
     proof (rule mem_FL_Red_F_because_G_Red_F)
       show \<open>\<forall>D \<in> \<G>_F (fst Cl). D \<in> G.Red_F (\<Union> (\<G>_F ` fst ` {Dl}))\<close>
         using d_ssub_c unfolding G.Red_F_def strictly_subsumes_def subsumes_def \<G>_F_def
       proof clarsimp
         fix \<sigma> \<sigma>'
         assume
           fst_not_in: \<open>\<forall>\<sigma>. \<not> fst Cl \<cdot> \<sigma> \<subseteq># fst Dl\<close> and
           fst_in: \<open>fst Dl \<cdot> \<sigma> \<subseteq># fst Cl\<close> and
           gr_sig: \<open>is_ground_subst \<sigma>'\<close>
         have \<open>{fst Dl \<cdot> \<sigma> \<cdot> \<sigma>'} \<subseteq> {fst Dl \<cdot> \<sigma> |\<sigma>. is_ground_subst \<sigma>}\<close>
           using gr_sig
           by (metis (mono_tags, lifting) is_ground_comp_subst mem_Collect_eq singletonD subsetI
               subst_cls_comp_subst)
         moreover have \<open>\<forall>I. I \<TTurnstile>s {fst Dl \<cdot> \<sigma> \<cdot> \<sigma>'} \<longrightarrow> I \<TTurnstile> fst Cl \<cdot> \<sigma>'\<close>
           using fst_in
           by (meson subst_cls_mono_mset true_clss_insert true_clss_subclause)
         moreover have \<open>\<forall>D \<in> {fst Dl \<cdot> \<sigma> \<cdot> \<sigma>'}. D < fst Cl \<cdot> \<sigma>'\<close>
           using fst_not_in fst_in gr_sig
         proof clarify
           show \<open>\<forall>\<sigma>. \<not> fst Cl \<cdot> \<sigma> \<subseteq># fst Dl \<Longrightarrow> fst Dl \<cdot> \<sigma> \<subseteq># fst Cl \<Longrightarrow> is_ground_subst \<sigma>' \<Longrightarrow>
             fst Dl \<cdot> \<sigma> \<cdot> \<sigma>' < fst Cl \<cdot> \<sigma>'\<close>
             by (metis False size_subst subset_imp_less_mset subset_mset.le_less subst_subset_mono)
         qed
         ultimately show \<open>\<exists>DD \<subseteq> {fst Dl \<cdot> \<sigma> |\<sigma>. is_ground_subst \<sigma>}.
            (\<forall>I. I \<TTurnstile>s DD \<longrightarrow> I \<TTurnstile> fst Cl \<cdot> \<sigma>') \<and> (\<forall>D \<in> DD. D < fst Cl \<cdot> \<sigma>')\<close>
           by blast
       qed
     qed
     then show ?thesis
       by (rule disjI1)
   qed
   show ?thesis
   proof (rule FL.step.process[of _ N "{Cl}" _ "{}"], simp+)
     show \<open>Cl \<in> FL.Red_F_\<G> N\<close>
       using d_sub'_c unfolding FL_Red_F_eq
     proof -
       have \<open>\<And>D. D \<in> \<G>_F (fst Cl) \<Longrightarrow> \<forall>E \<in> N. E \<sqsubset> Cl \<longrightarrow> D \<notin> \<G>_F (fst E) \<Longrightarrow>
         \<forall>D \<in> \<G>_F (fst Cl). D \<in> G.Red_F (\<G>_F (fst Dl)) \<or> Dl \<sqsubset> Cl \<and> D \<in> \<G>_F (fst Dl) \<Longrightarrow>
         D \<in> G.Red_F (\<Union>a \<in> N. \<G>_F (fst a))\<close>
         by (metis (no_types, lifting) G.Red_F_of_subset SUP_upper d_in subset_iff)
       moreover have \<open>\<And>D. D \<in> \<G>_F (fst Cl) \<Longrightarrow> \<forall>E \<in> N. E \<sqsubset> Cl \<longrightarrow> D \<notin> \<G>_F (fst E) \<Longrightarrow> Dl \<sqsubset> Cl \<Longrightarrow>
         D \<in> G.Red_F (\<Union>a \<in> N. \<G>_F (fst a))\<close>
         by (smt FL.Prec_FL_def FL.equiv_F_grounding FL.prec_F_grounding UNIV_witness d_in in_mono)
       ultimately show \<open>Cl \<in> {C. \<forall>D \<in> \<G>_F (fst C). D \<in> G.Red_F (\<Union> (\<G>_F ` fst ` {Dl})) \<or>
         (\<exists>E \<in> {Dl}. E \<sqsubset> C \<and> D \<in> \<G>_F (fst E))} \<or> Dl \<sqsubset> Cl \<Longrightarrow>
         Cl \<in> {C. \<forall>D \<in> \<G>_F (fst C). D \<in> G.Red_F (\<Union> (\<G>_F ` fst ` N)) \<or>
         (\<exists>E \<in> N. E \<sqsubset> C \<and> D \<in> \<G>_F (fst E))}\<close>
         by auto
     qed
   qed (simp add: FL.active_subset_def)
 qed
 
 lemma GC_reduction_step:
   assumes
     young: "snd Dl \<noteq> Old" and
     d_sub_c: "fst Dl \<subset># fst Cl"
   shows "N \<union> {Cl} \<leadsto>GC N \<union> {Dl}"
 proof (rule FL.step.process[of _ N "{Cl}" _ "{Dl}"])
   have "Cl \<in> FL.Red_F {Dl}"
   proof (rule mem_FL_Red_F_because_G_Red_F)
     show \<open>\<forall>D \<in> \<G>_F (fst Cl). D \<in> G.Red_F (\<Union> (\<G>_F ` fst ` {Dl}))\<close>
       using d_sub_c unfolding G.Red_F_def strictly_subsumes_def subsumes_def \<G>_F_def
     proof clarsimp
       fix \<sigma>
       assume \<open>is_ground_subst \<sigma>\<close>
       then have \<open>{fst Dl \<cdot> \<sigma>} \<subseteq> {fst Dl \<cdot> \<sigma> |\<sigma>. is_ground_subst \<sigma>}\<close>
         by blast
       moreover have \<open>fst Dl \<cdot> \<sigma> < fst Cl \<cdot> \<sigma>\<close>
         using subst_subset_mono[OF d_sub_c, of \<sigma>] by (simp add: subset_imp_less_mset)
       moreover have \<open>\<forall>I. I \<TTurnstile> fst Dl \<cdot> \<sigma> \<longrightarrow> I \<TTurnstile> fst Cl \<cdot> \<sigma>\<close>
         using subst_subset_mono[OF d_sub_c] true_clss_subclause by fast
       ultimately show \<open>\<exists>DD \<subseteq> {fst Dl \<cdot> \<sigma> |\<sigma>. is_ground_subst \<sigma>}. (\<forall>I. I \<TTurnstile>s DD \<longrightarrow> I \<TTurnstile> fst Cl \<cdot> \<sigma>)
         \<and> (\<forall>D \<in> DD. D < fst Cl \<cdot> \<sigma>)\<close>
         by blast
     qed
   qed
   then show "{Cl} \<subseteq> FL.Red_F (N \<union> {Dl})"
     using FL.Red_F_of_subset by blast
 qed (auto simp: FL.active_subset_def young)
 
 lemma GC_processing_step: "N \<union> {(C, New)} \<leadsto>GC N \<union> {(C, Processed)}"
 proof (rule FL.step.process[of _ N "{(C, New)}" _ "{(C, Processed)}"])
   have "(C, New) \<in> FL.Red_F {(C, Processed)}"
     by (rule mem_FL_Red_F_because_Prec_FL) (simp add: FL.Prec_FL_def generalizes_refl)
   then show "{(C, New)} \<subseteq> FL.Red_F (N \<union> {(C, Processed)})"
     using FL.Red_F_of_subset by blast
 qed (auto simp: FL.active_subset_def)
 
 lemma old_inferences_between_eq_new_inferences_between:
   "old_concl_of ` inference_system.inferences_between (ord_FO_\<Gamma> S) N C =
    concl_of ` F.Inf_between N {C}" (is "?rp = ?f")
 proof (intro set_eqI iffI)
   fix E
   assume e_in: "E \<in> old_concl_of ` inference_system.inferences_between (ord_FO_\<Gamma> S) N C"
 
   obtain CAs DA AAs As \<sigma> where
     e_res: "ord_resolve_rename S CAs DA AAs As \<sigma> E" and
     cd_sub: "set CAs \<union> {DA} \<subseteq> N \<union> {C}" and
     c_in: "C \<in> set CAs \<union> {DA}"
     using e_in unfolding inference_system.inferences_between_def infer_from_def ord_FO_\<Gamma>_def by auto
 
   show "E \<in> concl_of ` F.Inf_between N {C}"
     unfolding F.Inf_between_alt F.Inf_from_def
   proof -
     have \<open>Infer (CAs @ [DA]) E \<in> F_Inf \<and> set (prems_of (Infer (CAs @ [DA]) E)) \<subseteq> insert C N \<and>
       C \<in> set (prems_of (Infer (CAs @ [DA]) E)) \<and> E = concl_of (Infer (CAs @ [DA]) E)\<close>
       using e_res cd_sub c_in F_Inf_def by auto
     then show \<open>E \<in> concl_of ` {\<iota> \<in> F_Inf. \<iota> \<in> {\<iota> \<in> F_Inf. set (prems_of \<iota>) \<subseteq> N \<union> {C}} \<and>
       set (prems_of \<iota>) \<inter> {C} \<noteq> {}}\<close>
-      by (smt Un_insert_right boolean_algebra_cancel.sup0 disjoint_insert(2) mem_Collect_eq
-          image_def)
+      by (smt Un_insert_right boolean_algebra_cancel.sup0 disjoint_insert mem_Collect_eq image_def)
   qed
 next
   fix E
   assume e_in: "E \<in> concl_of ` F.Inf_between N {C}"
 
   obtain CAs DA AAs As \<sigma> where
     e_res: "ord_resolve_rename S CAs DA AAs As \<sigma> E" and
     cd_sub: "set CAs \<union> {DA} \<subseteq> N \<union> {C}" and
     c_in: "C \<in> set CAs \<union> {DA}"
     using e_in unfolding F.Inf_between_alt F.Inf_from_def F_Inf_def inference_system.Inf_between_alt
       inference_system.Inf_from_def
     by (auto simp: image_def Bex_def)
 
   show "E \<in> old_concl_of ` inference_system.inferences_between (ord_FO_\<Gamma> S) N C"
     unfolding inference_system.inferences_between_def infer_from_def ord_FO_\<Gamma>_def
     using e_res cd_sub c_in
     by (clarsimp simp: image_def Bex_def, rule_tac x = "old_Infer (mset CAs) DA E" in exI, auto)
 qed
 
 lemma GC_inference_step:
   assumes
     young: "l \<noteq> Old" and
     no_active: "FL.active_subset M = {}" and
     m_sup: "fst ` M \<supseteq> old_concl_of ` inference_system.inferences_between (ord_FO_\<Gamma> S)
       (fst ` FL.active_subset N) C"
   shows "N \<union> {(C, l)} \<leadsto>GC N \<union> {(C, Old)} \<union> M"
 proof (rule FL.step.infer[of _ N C l _ M])
   have m_sup': "fst ` M \<supseteq> concl_of ` F.Inf_between (fst ` FL.active_subset N) {C}"
     using m_sup unfolding old_inferences_between_eq_new_inferences_between .
 
   show "F.Inf_between (fst ` FL.active_subset N) {C} \<subseteq> F.Red_I (fst ` (N \<union> {(C, Old)} \<union> M))"
   proof
     fix \<iota>
     assume \<iota>_in_if2: "\<iota> \<in> F.Inf_between (fst ` FL.active_subset N) {C}"
     note \<iota>_in = F.Inf_if_Inf_between[OF \<iota>_in_if2]
     have "concl_of \<iota> \<in> fst ` M"
       using m_sup' \<iota>_in_if2 m_sup' by (auto simp: image_def Collect_mono_iff F.Inf_between_alt)
     then have "concl_of \<iota> \<in> fst ` (N \<union> {(C, Old)} \<union> M)"
       by auto
     then show "\<iota> \<in> F.Red_I_\<G> (fst ` (N \<union> {(C, Old)} \<union> M))"
       by (rule F.Red_I_of_Inf_to_N[OF \<iota>_in])
   qed
 qed (use young no_active in auto)
 
 lemma RP_step_imp_GC_step: "St \<leadsto>RP St' \<Longrightarrow> lclss_of_state St \<leadsto>GC lclss_of_state St'"
 proof (induction rule: RP.induct)
   case (tautology_deletion A C N P Q)
   then show ?case
     by (rule GC_tautology_step)
 next
   case (forward_subsumption D P Q C N)
   note d_in = this(1) and d_sub_c = this(2)
   show ?case
   proof (cases "D \<in> P")
     case True
     then show ?thesis
       using GC_subsumption_step[of "(D, Processed)" "lclss_of_state (N, P, Q)" "(C, New)"] d_sub_c
       by auto
   next
     case False
     then have "D \<in> Q"
       using d_in by simp
     then show ?thesis
       using GC_subsumption_step[of "(D, Old)" "lclss_of_state (N, P, Q)" "(C, New)"] d_sub_c by auto
   qed
 next
   case (backward_subsumption_P D N C P Q)
   note d_in = this(1) and d_ssub_c = this(2)
   then show ?case
     using GC_subsumption_step[of "(D, New)" "lclss_of_state (N, P, Q)" "(C, Processed)"] d_ssub_c
     by auto
 next
   case (backward_subsumption_Q D N C P Q)
   note d_in = this(1) and d_ssub_c = this(2)
   then show ?case
     using GC_subsumption_step[of "(D, New)" "lclss_of_state (N, P, Q)" "(C, Old)"] d_ssub_c by auto
 next
   case (forward_reduction D L' P Q L \<sigma> C N)
   show ?case
     using GC_reduction_step[of "(C, New)" "(C + {#L#}, New)" "lclss_of_state (N, P, Q)"] by auto
 next
   case (backward_reduction_P D L' N L \<sigma> C P Q)
   show ?case
     using GC_reduction_step[of "(C, Processed)" "(C + {#L#}, Processed)" "lclss_of_state (N, P, Q)"]
     by auto
 next
   case (backward_reduction_Q D L' N L \<sigma> C P Q)
   show ?case
     using GC_reduction_step[of "(C, Processed)" "(C + {#L#}, Old)" "lclss_of_state (N, P, Q)"]
     by auto
 next
   case (clause_processing N C P Q)
   show ?case
     using GC_processing_step[of "lclss_of_state (N, P, Q)" C] by auto
 next
   case (inference_computation N Q C P)
   note n = this(1)
   show ?case
   proof -
     have \<open>FL.active_subset (lclss_of_state (N, {}, {})) = {}\<close>
       unfolding n by (auto simp: FL.active_subset_def)
     moreover have \<open>old_concls_of (inference_system.inferences_between (ord_FO_\<Gamma> S)
       (fst ` FL.active_subset (lclss_of_state ({}, P, Q))) C) \<subseteq> N\<close>
       unfolding n inference_system.inferences_between_def image_def mem_Collect_eq
         lclss_of_state_def infer_from_def
       by (auto simp: FL.active_subset_def)
     ultimately have \<open>lclss_of_state ({}, insert C P, Q) \<leadsto>GC lclss_of_state (N, P, insert C Q)\<close>
       using GC_inference_step[of Processed "lclss_of_state (N, {}, {})"
         "lclss_of_state ({}, P, Q)" C, simplified] by blast
     then show ?case
       by (auto simp: FL.active_subset_def)
   qed
 qed
 
 lemma RP_derivation_imp_GC_derivation: "chain (\<leadsto>RP) Sts \<Longrightarrow> chain (\<leadsto>GC) (lmap lclss_of_state Sts)"
   using chain_lmap RP_step_imp_GC_step by blast
 
-lemma RP_step_imp_derive_step: "St \<leadsto>RP St' \<Longrightarrow> lclss_of_state St \<rhd>RedL lclss_of_state St'"
+lemma RP_step_imp_derive_step: "St \<leadsto>RP St' \<Longrightarrow> lclss_of_state St \<rhd>L lclss_of_state St'"
   by (rule FL.one_step_equiv) (rule RP_step_imp_GC_step)
 
 lemma RP_derivation_imp_derive_derivation:
-  "chain (\<leadsto>RP) Sts \<Longrightarrow> chain (\<rhd>RedL) (lmap lclss_of_state Sts)"
+  "chain (\<leadsto>RP) Sts \<Longrightarrow> chain (\<rhd>L) (lmap lclss_of_state Sts)"
   using chain_lmap RP_step_imp_derive_step by blast
 
 theorem RP_sound_new_statement:
   assumes
     deriv: "chain (\<leadsto>RP) Sts" and
     bot_in: "{#} \<in> clss_of_state (Liminf_state Sts)"
   shows "clss_of_state (lhd Sts) \<TTurnstile>\<G>e {{#}}"
 proof -
   have "clss_of_state (Liminf_state Sts) \<TTurnstile>\<G>e {{#}}"
     using F.subset_entailed bot_in by auto
   then have "fst ` Liminf_llist (lmap lclss_of_state Sts) \<TTurnstile>\<G>e {{#}}"
     by (metis image_hd_lclss_of_state lclss_Liminf_commute)
   then have "Liminf_llist (lmap lclss_of_state Sts) \<TTurnstile>\<G>Le FL.Bot_FL"
     using FL.labeled_entailment_lifting by simp
   then have "lhd (lmap lclss_of_state Sts) \<TTurnstile>\<G>Le FL.Bot_FL"
   proof -
     assume \<open>FL.entails_\<G> (Liminf_llist (lmap lclss_of_state Sts)) ({{#}} \<times> UNIV)\<close>
-    moreover have \<open>chain (\<rhd>RedL) (lmap lclss_of_state Sts)\<close>
+    moreover have \<open>chain (\<rhd>L) (lmap lclss_of_state Sts)\<close>
       using deriv RP_derivation_imp_derive_derivation by simp
     moreover have \<open>chain FL.entails_\<G> (lmap lclss_of_state Sts)\<close>
       by (smt F_entails_\<G>_iff FL.labeled_entailment_lifting RP_model chain_lmap deriv \<G>_Fs_def
         image_hd_lclss_of_state)
     ultimately show \<open>FL.entails_\<G> (lhd (lmap lclss_of_state Sts)) ({{#}} \<times> UNIV)\<close>
       using FL.unsat_limit_iff by blast
   qed
   then have "lclss_of_state (lhd Sts) \<TTurnstile>\<G>Le FL.Bot_FL"
     using chain_not_lnull deriv by fastforce
   then show ?thesis
     unfolding FL.entails_\<G>_L_def F.entails_\<G>_def lclss_of_state_def by auto
 qed
 
 theorem RP_saturated_if_fair_new_statement:
   assumes
     deriv: "chain (\<leadsto>RP) Sts" and
     init: "FL.active_subset (lclss_of_state (lhd Sts)) = {}" and
     final: "FL.passive_subset (Liminf_llist (lmap lclss_of_state Sts)) = {}"
   shows "FL.saturated (Liminf_llist (lmap lclss_of_state Sts))"
 proof -
   note nnil = chain_not_lnull[OF deriv]
   have gc_deriv: "chain (\<leadsto>GC) (lmap lclss_of_state Sts)"
     by (rule RP_derivation_imp_GC_derivation[OF deriv])
   show ?thesis
     using nnil init final
-      FL.fair_implies_Liminf_saturated[OF FL.gc_to_red[OF gc_deriv] FL.gc_fair[OF gc_deriv]]
-    by simp
+      FL.fair_implies_Liminf_saturated[OF FL.gc_to_red[OF gc_deriv] FL.gc_fair[OF gc_deriv]] by simp
 qed
 
 corollary RP_complete_if_fair_new_statement:
   assumes
     deriv: "chain (\<leadsto>RP) Sts" and
     init: "FL.active_subset (lclss_of_state (lhd Sts)) = {}" and
     final: "FL.passive_subset (Liminf_llist (lmap lclss_of_state Sts)) = {}" and
     unsat: "grounding_of_state (lhd Sts) \<TTurnstile>e {{#}}"
   shows "{#} \<in> Q_of_state (Liminf_state Sts)"
 proof -
   note nnil = chain_not_lnull[OF deriv]
   note len = chain_length_pos[OF deriv]
   have gc_deriv: "chain (\<leadsto>GC) (lmap lclss_of_state Sts)"
     by (rule RP_derivation_imp_GC_derivation[OF deriv])
 
   have hd_lcls: "fst ` lhd (lmap lclss_of_state Sts) = lhd (lmap clss_of_state Sts)"
     using len zero_enat_def by auto
   have hd_unsat: "fst ` lhd (lmap lclss_of_state Sts) \<TTurnstile>\<G>e {{#}}"
     unfolding hd_lcls F_entails_\<G>_iff unfolding true_clss_def using unsat unfolding \<G>_Fs_def
     by (metis (no_types, lifting) chain_length_pos gc_deriv gr.ex_min_counterex i0_less
         llength_eq_0 llength_lmap llength_lmap llist.map_sel(1) true_cls_empty true_clss_singleton)
   have "\<exists>BL \<in> {{#}} \<times> UNIV. BL \<in> Liminf_llist (lmap lclss_of_state Sts)"
     by (rule FL.gc_complete_Liminf[OF gc_deriv,of "{#}"])
       (use final hd_unsat in \<open>auto simp: init nnil\<close>)
   then show ?thesis
     unfolding Liminf_state_def lclss_Liminf_commute
     using final[unfolded FL.passive_subset_def] Liminf_state_def lclss_Liminf_commute by fastforce
 qed
 
 
 subsection \<open>Alternative Derivation of Previous \textsf{RP} Results\<close>
 
 lemma old_fair_imp_new_fair:
   assumes
     nnul: "\<not> lnull Sts" and
     fair: "fair_state_seq Sts" and
     empty_Q0: "Q_of_state (lhd Sts) = {}"
   shows
     "FL.active_subset (lclss_of_state (lhd Sts)) = {}" and
     "FL.passive_subset (Liminf_llist (lmap lclss_of_state Sts)) = {}"
 proof -
   show "FL.active_subset (lclss_of_state (lhd Sts)) = {}"
     using nnul empty_Q0 unfolding FL.active_subset_def by (cases Sts) auto
 next
   show "FL.passive_subset (Liminf_llist (lmap lclss_of_state Sts)) = {}"
     using fair
     unfolding fair_state_seq_def FL.passive_subset_def lclss_Liminf_commute lclss_of_state_def
     by auto
 qed
 
 lemma old_redundant_infer_iff:
   "src.redundant_infer N \<gamma> \<longleftrightarrow>
    (\<exists>DD. DD \<subseteq> N \<and> DD \<union> set_mset (old_side_prems_of \<gamma>) \<TTurnstile>e {old_concl_of \<gamma>}
       \<and> (\<forall>D \<in> DD. D < old_main_prem_of \<gamma>))"
   (is "?lhs \<longleftrightarrow> ?rhs")
 proof
-  assume ?lhs
-  then show ?rhs
-    unfolding src.redundant_infer_def by auto
-next
   assume ?rhs
   then obtain DD0 where
     "DD0 \<subseteq> N" and
     "DD0 \<union> set_mset (old_side_prems_of \<gamma>) \<TTurnstile>e {old_concl_of \<gamma>}" and
     "\<forall>D \<in> DD0. D < old_main_prem_of \<gamma>"
     by blast
   then obtain DD where
     fin_dd: "finite DD" and
     dd_in: "DD \<subseteq> N" and
     dd_un: "DD \<union> set_mset (old_side_prems_of \<gamma>) \<TTurnstile>e {old_concl_of \<gamma>}" and
     all_dd: "\<forall>D \<in> DD. D < old_main_prem_of \<gamma>"
     using entails_concl_compact_union[of "{old_concl_of \<gamma>}" DD0 "set_mset (old_side_prems_of \<gamma>)"]
     by fast
   show ?lhs
     unfolding src.redundant_infer_def using fin_dd dd_in dd_un all_dd
     by simp (metis finite_set_mset_mset_set true_clss_set_mset)
-qed
+qed (auto simp: src.redundant_infer_def)
 
 definition old_infer_of :: "'a clause inference \<Rightarrow> 'a old_inference" where
   "old_infer_of \<iota> = old_Infer (mset (side_prems_of \<iota>)) (main_prem_of \<iota>) (concl_of \<iota>)"
 
 lemma new_redundant_infer_imp_old_redundant_infer:
   "G.redundant_infer N \<iota> \<Longrightarrow> src.redundant_infer N (old_infer_of \<iota>)"
   unfolding old_redundant_infer_iff G.redundant_infer_def old_infer_of_def by simp
 
 lemma saturated_imp_saturated_RP:
   assumes
     satur: "FL.saturated (Liminf_llist (lmap lclss_of_state Sts))" and
     no_passive: "FL.passive_subset (Liminf_llist (lmap lclss_of_state Sts)) = {}"
   shows "src.saturated_upto Sts (grounding_of_state (Liminf_state Sts))"
 proof -
   define Q where
     "Q = Liminf_llist (lmap Q_of_state Sts)"
   define Ql where
     "Ql = (\<lambda>C. (C, Old)) ` Q"
   define G where
     "G = \<Union> (\<G>_F ` Q)"
 
   have n_empty: "N_of_state (Liminf_state Sts) = {}" and
     p_empty: "P_of_state (Liminf_state Sts) = {}"
     using no_passive[unfolded FL.passive_subset_def] Liminf_state_def lclss_Liminf_commute
     by fastforce+
   then have limuls_eq: "Liminf_llist (lmap lclss_of_state Sts) = Ql"
     unfolding Ql_def Q_def using Liminf_state_def lclss_Liminf_commute lclss_of_state_def by auto
   have clst_eq: "clss_of_state (Liminf_state Sts) = Q"
     unfolding n_empty p_empty Q_def by (auto simp: Liminf_state_def)
   have gflimuls_eq: "(\<Union>Cl \<in> Ql. \<G>_F (fst Cl)) = G"
     unfolding Ql_def G_def by auto
 
   have "gd.inferences_from Sts G \<subseteq> src.Ri Sts G"
   proof
     fix \<gamma>
     assume \<gamma>_inf: "\<gamma> \<in> gd.inferences_from Sts G"
 
     obtain \<iota> where
       \<iota>_inff: "\<iota> \<in> G.Inf_from Q G" and
       \<gamma>: "\<gamma> = old_infer_of \<iota>"
       using \<gamma>_inf
       unfolding gd.inferences_from_def old_infer_from_def G.Inf_from_def old_infer_of_def
     proof (atomize_elim, clarify)
       assume
         g_is: \<open>\<gamma> \<in> gd.ord_\<Gamma> Sts\<close> and
         prems_in: \<open>set_mset (old_side_prems_of \<gamma> + {#old_main_prem_of \<gamma>#}) \<subseteq> G\<close>
       obtain CAs DA AAs As E where main_in: \<open>DA \<in> G\<close> and side_in: \<open>set CAs \<subseteq> G\<close> and
         g_is2: \<open>\<gamma> = old_Infer (mset CAs) DA E\<close> and
         ord_res: \<open>gd.ord_resolve Sts CAs DA AAs As E\<close>
         using g_is prems_in unfolding gd.ord_\<Gamma>_def by auto
       define \<iota>_\<gamma> where "\<iota>_\<gamma> = Infer (CAs @ [DA]) E"
       then have \<open>\<iota>_\<gamma> \<in> G_Inf Q\<close>  using Q_of_state.simps g_is g_is2 ord_res Liminf_state_def S_Q_def
         unfolding gd.ord_\<Gamma>_def G_Inf_def Q_def by auto
       moreover have \<open>set (prems_of \<iota>_\<gamma>) \<subseteq> G\<close>
         using g_is2 prems_in unfolding \<iota>_\<gamma>_def by simp
       moreover have \<open>\<gamma> = old_Infer (mset (side_prems_of \<iota>_\<gamma>)) (main_prem_of \<iota>_\<gamma>) (concl_of \<iota>_\<gamma>)\<close>
         using g_is2 unfolding \<iota>_\<gamma>_def by simp
       ultimately show
         \<open>\<exists>\<iota>. \<iota> \<in> {\<iota> \<in> G_Inf Q. set (prems_of \<iota>) \<subseteq> G} \<and> \<gamma> = old_Infer (mset (side_prems_of \<iota>))
          (main_prem_of \<iota>) (concl_of \<iota>)\<close>
         by blast
     qed
     obtain \<iota>' where
       \<iota>'_inff: "\<iota>' \<in> F.Inf_from Q" and
       \<iota>_in_\<iota>': "\<iota> \<in> \<G>_I Q \<iota>'"
-      using G_Inf_overapproximates_F_Inf \<iota>_inff unfolding G_def by blast
+      using G_Inf_overapprox_F_Inf \<iota>_inff unfolding G_def by blast
 
     note \<iota>'_inf = F.Inf_if_Inf_from[OF \<iota>'_inff]
 
     let ?olds = "replicate (length (prems_of \<iota>')) Old"
 
     obtain \<iota>'' and l0 where
       \<iota>'': "\<iota>'' = Infer (zip (prems_of \<iota>') ?olds) (concl_of \<iota>', l0)" and
       \<iota>''_inf: "\<iota>'' \<in> FL_Inf"
       using FL.Inf_F_to_Inf_FL[OF \<iota>'_inf, of ?olds, simplified] by blast
 
     have "set (prems_of \<iota>'') \<subseteq> Ql"
       using \<iota>'_inff[unfolded F.Inf_from_def, simplified] unfolding \<iota>'' Ql_def by auto
     then have "\<iota>'' \<in> FL.Inf_from Ql"
       unfolding FL.Inf_from_def using \<iota>''_inf by simp
     moreover have "\<iota>' = FL.to_F \<iota>''"
       unfolding \<iota>'' unfolding FL.to_F_def by simp
     ultimately have "\<iota> \<in> G.Red_I Q G"
       using \<iota>_in_\<iota>'
         FL.sat_inf_imp_ground_red_fam_inter[OF satur, unfolded limuls_eq gflimuls_eq, simplified]
       by blast
     then have "G.redundant_infer G \<iota>"
       unfolding G.Red_I_def by auto
     then have \<gamma>_red: "src.redundant_infer G \<gamma>"
       unfolding \<gamma> by (rule new_redundant_infer_imp_old_redundant_infer)
     moreover have "\<gamma> \<in> gd.ord_\<Gamma> Sts"
       using \<gamma>_inf gd.inferences_from_def by blast
     ultimately show "\<gamma> \<in> src.Ri Sts G"
       unfolding src.Ri_def by auto
   qed
   then show ?thesis
     unfolding G_def clst_eq src.saturated_upto_def
     by clarsimp (smt Diff_subset gd.inferences_from_mono subset_eq \<G>_Fs_def)
 qed
 
 theorem RP_sound_old_statement:
   assumes
     deriv: "chain (\<leadsto>RP) Sts" and
     bot_in: "{#} \<in> clss_of_state (Liminf_state Sts)"
   shows "\<not> satisfiable (grounding_of_state (lhd Sts))"
   using RP_sound_new_statement[OF deriv bot_in] unfolding F_entails_\<G>_iff \<G>_Fs_def by simp
 
 text \<open>The theorem below is stated differently than the original theorem in \textsf{RP}:
 The grounding of the limit might be a strict subset of the limit of the groundings. Because
 saturation is neither monotone nor antimonotone, the two results are incomparable. See also
 @{thm [source] grounding_of_state_Liminf_state_subseteq}.\<close>
 
 theorem RP_saturated_if_fair_old_statement_altered:
   assumes
     deriv: "chain (\<leadsto>RP) Sts" and
     fair: "fair_state_seq Sts" and
     empty_Q0: "Q_of_state (lhd Sts) = {}"
   shows "src.saturated_upto Sts (grounding_of_state (Liminf_state Sts))"
 proof -
   note fair' = old_fair_imp_new_fair[OF chain_not_lnull[OF deriv] fair empty_Q0]
   show ?thesis
     by (rule saturated_imp_saturated_RP[OF _ fair'(2)], rule RP_saturated_if_fair_new_statement)
       (rule deriv fair')+
 qed
 
 corollary RP_complete_if_fair_old_statement:
   assumes
     deriv: "chain (\<leadsto>RP) Sts" and
     fair: "fair_state_seq Sts" and
     empty_Q0: "Q_of_state (lhd Sts) = {}" and
     unsat: "\<not> satisfiable (grounding_of_state (lhd Sts))"
   shows "{#} \<in> Q_of_state (Liminf_state Sts)"
 proof (rule RP_complete_if_fair_new_statement)
   show \<open>\<G>_Fs (N_of_state (lhd Sts) \<union> P_of_state (lhd Sts) \<union> Q_of_state (lhd Sts)) \<TTurnstile>e {{#}}\<close>
     using unsat unfolding F_entails_\<G>_iff by auto
 qed (rule deriv old_fair_imp_new_fair[OF chain_not_lnull[OF deriv] fair empty_Q0])+
 
 end
 
 end
diff --git a/thys/Saturation_Framework_Extensions/Soundness.thy b/thys/Saturation_Framework_Extensions/Soundness.thy
--- a/thys/Saturation_Framework_Extensions/Soundness.thy
+++ b/thys/Saturation_Framework_Extensions/Soundness.thy
@@ -1,156 +1,156 @@
 (*  Title:       Soundness
     Author:      Sophie Tourret <stourret at mpi-inf.mpg.de>, 2020
     Author:      Jasmin Blanchette <j.c.blanchette at vu.nl>, 2014, 2017, 2020
     Author:      Dmitriy Traytel <traytel at inf.ethz.ch>, 2014
     Author:      Anders Schlichtkrull <andschl at dtu.dk>, 2017
 *)
 
 section \<open>Soundness\<close>
 
 theory Soundness
   imports Saturation_Framework.Calculus
 begin
 
 text \<open>
 Although consistency-preservation usually suffices, soundness is a more precise concept and is
 sometimes useful.
 \<close>
 
 locale sound_inference_system = inference_system + consequence_relation +
   assumes
     sound: \<open>\<iota> \<in> Inf \<Longrightarrow> set (prems_of \<iota>) \<Turnstile> {concl_of \<iota>}\<close>
 begin
 
 lemma Inf_consist_preserving:
   assumes n_cons: "\<not> N \<Turnstile> Bot"
   shows "\<not> N \<union> concl_of ` Inf_from N \<Turnstile> Bot"
 proof -
   have "N \<Turnstile> concl_of ` Inf_from N"
     using sound unfolding Inf_from_def image_def Bex_def mem_Collect_eq
     by (smt all_formulas_entailed entails_trans mem_Collect_eq subset_entailed)
   then show ?thesis
     using n_cons entails_trans_strong by blast
 qed
 
 end
 
 text \<open>
 Assuming compactness of the consequence relation, the limit of a derivation based on a redundancy
 criterion is satisfiable if and only if the initial set is satisfiable. This material is partly
 based on Section 4.1 of Bachmair and Ganzinger's \emph{Handbook} chapter, but adapted to the
 saturation framework of Waldmann et al.
 \<close>
 
 locale compact_consequence_relation = consequence_relation +
   assumes
     entails_compact: "CC \<Turnstile> Bot \<Longrightarrow> \<exists>CC' \<subseteq> CC. finite CC' \<and> CC' \<Turnstile> Bot"
 begin
 
 lemma chain_entails_derive_consist_preserving:
   assumes
     ent: "chain (\<Turnstile>) Ns" and
     n0_sat: "\<not> lhd Ns \<Turnstile> Bot"
   shows "\<not> Sup_llist Ns \<Turnstile> Bot"
 proof -
   have bot_sat: "\<not> {} \<Turnstile> Bot"
     using n0_sat by (meson empty_subsetI entails_trans subset_entailed)
 
   {
     fix DD
     assume fin: "finite DD" and sset_lun: "DD \<subseteq> Sup_llist Ns"
     then obtain k where
       dd_sset: "DD \<subseteq> Sup_upto_llist Ns (enat k)"
       using finite_Sup_llist_imp_Sup_upto_llist by blast
     have "\<not> Sup_upto_llist Ns (enat k) \<Turnstile> Bot"
     proof (induct k)
       case 0
       then show ?case
         unfolding Sup_upto_llist_def
         using lhd_conv_lnth[OF chain_not_lnull[OF ent], symmetric] n0_sat bot_sat by auto
     next
       case (Suc k)
       show ?case
       proof (cases "enat (Suc k) \<ge> llength Ns")
         case True
         then have "Sup_upto_llist Ns (enat k) = Sup_upto_llist Ns (enat (Suc k))"
           unfolding Sup_upto_llist_def using le_Suc_eq by auto
         then show ?thesis
           using Suc by simp
       next
         case False
         then have entail_succ: "lnth Ns k \<Turnstile> lnth Ns (Suc k)"
           using ent chain_lnth_rel by fastforce
         from False have lt: "enat (Suc k) < llength Ns \<and> enat k < llength Ns"
           by (meson Suc_ile_eq le_cases not_le)
         have "{i. enat i < llength Ns \<and> i \<le> Suc k} =
           {i. enat i < llength Ns \<and> i \<le> k} \<union> {i. enat i < llength Ns \<and> i = Suc k}" by auto
         then have "Sup_upto_llist Ns (enat (Suc k)) =
           Sup_upto_llist Ns (enat k) \<union> lnth Ns (Suc k)"
           using lt unfolding Sup_upto_llist_def enat_ord_code(1) by blast
         moreover have "Sup_upto_llist Ns k \<Turnstile> lnth Ns (Suc k)"
           using entail_succ subset_entailed [of "lnth Ns k" "Sup_upto_llist Ns k"] lt
           unfolding Sup_upto_llist_def by (simp add: entail_succ UN_upper entails_trans)
         ultimately have "Sup_upto_llist Ns k \<Turnstile> Sup_upto_llist Ns (Suc k)"
           using entail_union subset_entailed by fastforce
         then show ?thesis using Suc.hyps using entails_trans by blast
       qed
     qed
     then have "\<not> DD \<Turnstile> Bot"
       using dd_sset entails_trans subset_entailed unfolding Sup_upto_llist_def by blast
   }
   then show ?thesis
     using entails_compact by auto
 qed
 
 end
 
 locale refutationally_compact_calculus = calculus + compact_consequence_relation
 begin
 
 text \<open>
 The next three lemmas correspond to Lemma 4.2:
 \<close>
 
 lemma Red_F_Sup_subset_Red_F_Liminf:
-  "chain (\<rhd>Red) Ns \<Longrightarrow> Red_F (Sup_llist Ns) \<subseteq> Red_F (Liminf_llist Ns)"
+  "chain (\<rhd>) Ns \<Longrightarrow> Red_F (Sup_llist Ns) \<subseteq> Red_F (Liminf_llist Ns)"
   by (metis Liminf_llist_subset_Sup_llist Red_in_Sup Un_absorb1 calculus.Red_F_of_Red_F_subset
       calculus_axioms double_diff sup_ge2)
 
 lemma Red_I_Sup_subset_Red_I_Liminf:
-  "chain (\<rhd>Red) Ns \<Longrightarrow> Red_I (Sup_llist Ns) \<subseteq> Red_I (Liminf_llist Ns)"
+  "chain (\<rhd>) Ns \<Longrightarrow> Red_I (Sup_llist Ns) \<subseteq> Red_I (Liminf_llist Ns)"
   by (metis Liminf_llist_subset_Sup_llist Red_I_of_Red_F_subset Red_in_Sup double_diff subset_refl)
 
 lemma unsat_limit_iff:
   assumes
-    chain_red: "chain (\<rhd>Red) Ns" and
+    chain_red: "chain (\<rhd>) Ns" and
     chain_ent: "chain (\<Turnstile>) Ns"
   shows "Liminf_llist Ns \<Turnstile> Bot \<longleftrightarrow> lhd Ns \<Turnstile> Bot"
 proof
   assume "Liminf_llist Ns \<Turnstile> Bot"
   then have "Sup_llist Ns \<Turnstile> Bot"
     using Liminf_llist_subset_Sup_llist by (metis entails_trans subset_entailed)
   then show "lhd Ns \<Turnstile> Bot"
     using chain_ent chain_entails_derive_consist_preserving by blast
 next
   assume "lhd Ns \<Turnstile> Bot"
   then have "Sup_llist Ns \<Turnstile> Bot"
     by (meson chain_ent chain_not_lnull entails_trans lhd_subset_Sup_llist subset_entailed)
   then have "Sup_llist Ns - Red_F (Sup_llist Ns) \<Turnstile> Bot"
     using Red_F_Bot entail_set_all_formulas by blast
   then show "Liminf_llist Ns \<Turnstile> Bot"
     using entails_trans subset_entailed by (smt Diff_iff Red_in_Sup chain_red subset_eq)
 qed
 
 text \<open>Some easy consequences:\<close>
 
-lemma Red_F_limit_Sup: "chain (\<rhd>Red) Ns \<Longrightarrow> Red_F (Liminf_llist Ns) = Red_F (Sup_llist Ns)"
+lemma Red_F_limit_Sup: "chain (\<rhd>) Ns \<Longrightarrow> Red_F (Liminf_llist Ns) = Red_F (Sup_llist Ns)"
   by (metis Liminf_llist_subset_Sup_llist Red_F_of_Red_F_subset Red_F_of_subset Red_in_Sup
       double_diff order_refl subset_antisym)
 
-lemma Red_I_limit_Sup: "chain (\<rhd>Red) Ns \<Longrightarrow> Red_I (Liminf_llist Ns) = Red_I (Sup_llist Ns)"
+lemma Red_I_limit_Sup: "chain (\<rhd>) Ns \<Longrightarrow> Red_I (Liminf_llist Ns) = Red_I (Sup_llist Ns)"
   by (metis Liminf_llist_subset_Sup_llist Red_I_of_Red_F_subset Red_I_of_subset Red_in_Sup
       double_diff order_refl subset_antisym)
 
 end
 
 end