diff --git a/thys/Saturation_Framework/Calculi.thy b/thys/Saturation_Framework/Calculi.thy
--- a/thys/Saturation_Framework/Calculi.thy
+++ b/thys/Saturation_Framework/Calculi.thy
@@ -1,942 +1,942 @@
 (*  Title:       Calculi of the Saturation Framework
  *   Author:      Sophie Tourret <stourret at mpi-inf.mpg.de>, 2018-2020 *)
 
 section \<open>Calculi\<close>
 
 text \<open>In this section, the section 2.2 to 2.4 of the report are covered. This
   includes results on calculi equipped with a redundancy criterion or with a
   family of redundancy criteria, as well as a proof that various notions of
   redundancy are equivalent\<close>
 
 theory Calculi
   imports
     Consequence_Relations_and_Inference_Systems
     Ordered_Resolution_Prover.Lazy_List_Liminf
     Ordered_Resolution_Prover.Lazy_List_Chain
 begin
 
 subsection \<open>Calculi with a Redundancy Criterion\<close>
 
 locale calculus_with_red_crit = 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_Inf :: "'f set \<Rightarrow> 'f inference set" and
     Red_F :: "'f set \<Rightarrow> 'f set"
   assumes
     Red_Inf_to_Inf: "Red_Inf 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_Inf_of_subset: "N \<subseteq> N' \<Longrightarrow> Red_Inf N \<subseteq> Red_Inf N'" and
     Red_F_of_Red_F_subset: "N' \<subseteq> Red_F N \<Longrightarrow> Red_F N \<subseteq> Red_F (N - N')" and
     Red_Inf_of_Red_F_subset: "N' \<subseteq> Red_F N \<Longrightarrow> Red_Inf N \<subseteq> Red_Inf (N - N')" and
     Red_Inf_of_Inf_to_N: "\<iota> \<in> Inf \<Longrightarrow> concl_of \<iota> \<in> N \<Longrightarrow> \<iota> \<in> Red_Inf N"
 begin
 
 lemma Red_Inf_of_Inf_to_N_subset: "{\<iota> \<in> Inf. concl_of \<iota> \<in> N} \<subseteq> Red_Inf N"
   using Red_Inf_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_Inf N"
 proof -
   have "\<iota> \<in> Red_Inf (Red_F N)" by (simp add: Red_Inf_of_Inf_to_N i_in concl)
   then have i_in_Red: "\<iota> \<in> Red_Inf (N \<union> Red_F N)" by (simp add: Red_Inf_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_Inf ((N \<union> Red_F N) - (Red_F N - N))" using Red_Inf_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_with_red_crit.Red_Inf_of_subset calculus_with_red_crit_axioms sup_bot.right_neutral)
 qed
 
 definition saturated :: "'f set \<Rightarrow> bool" where
   "saturated N \<longleftrightarrow> Inf_from N \<subseteq> Red_Inf N"
 
 definition reduc_saturated :: "'f set \<Rightarrow> bool" where
   "reduc_saturated N \<longleftrightarrow> Inf_from (N - Red_F N) \<subseteq> Red_Inf N"
 
 lemma Red_Inf_without_red_F:
   "Red_Inf (N - Red_F N) = Red_Inf N"
   using Red_Inf_of_subset [of "N - Red_F N" N]
     and Red_Inf_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_Inf N" using saturated unfolding saturated_def by auto
   also have "Red_Inf N \<subseteq> Red_Inf (N - Red_F N)" using Red_Inf_of_Red_F_subset by auto
   finally have "Inf_from (N - Red_F N) \<subseteq> Red_Inf (N - Red_F N)" by auto
   then show ?thesis unfolding saturated_def by auto
 qed
 
 definition Sup_Red_Inf_llist :: "'f set llist \<Rightarrow> 'f inference set" where
   "Sup_Red_Inf_llist D = (\<Union>i \<in> {i. enat i < llength D}. Red_Inf (lnth D i))"
 
 lemma Sup_Red_Inf_unit: "Sup_Red_Inf_llist (LCons X LNil) = Red_Inf X"
   using Sup_Red_Inf_llist_def enat_0_iff(1) by simp
 
 definition fair :: "'f set llist \<Rightarrow> bool" where
   "fair D \<longleftrightarrow> Inf_from (Liminf_llist D) \<subseteq> Sup_Red_Inf_llist D"
 
 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"
 
 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 D" and
     not_in_Liminf: "C \<notin> Liminf_llist D"
   shows
     "\<exists>i \<in> {i. enat (Suc i) < llength D}. C \<in> lnth D i - lnth D (Suc i)"
 proof -
   obtain i where C_D_i: "C \<in> Sup_upto_llist D i" and "i < llength D"
     using elem_Sup_llist_imp_Sup_upto_llist in_Sup by fast
   then obtain j where j: "j \<ge> i \<and> enat j < llength D \<and> C \<notin> lnth D j" using not_in_Liminf
     unfolding Sup_llist_def chain_def Liminf_llist_def by auto
   obtain k where k: "C \<in> lnth D k" "enat k < llength D" "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 D i}"
   define l where "l = Max ?S"
   have \<open>k \<in> {i. i < j \<and> k \<le> i \<and> C \<in> lnth D 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 D i} \<noteq> {}" by auto
   then have l_prop: "l < j \<and> l \<ge> k \<and> C \<in> lnth D l" using Max_in[of ?S, OF _ nempty] unfolding l_def by auto
   then have "C \<in> lnth D l - lnth D (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 D}"
       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) D"
   shows "Sup_llist D - Liminf_llist D \<subseteq> Red_F (Sup_llist D)"
 proof
   fix C
   assume C_in_subset: "C \<in> Sup_llist D - Liminf_llist D"
   {
     fix C i
     assume
       in_ith_elem: "C \<in> lnth D i - lnth D (Suc i)" and
       i: "enat (Suc i) < llength D"
     have "lnth D i \<rhd>Red lnth D (Suc i)" using i deriv in_ith_elem chain_lnth_rel by auto
     then have "C \<in> Red_F (lnth D (Suc i))" using in_ith_elem derive.cases by blast
     then have "C \<in> Red_F (Sup_llist D)" using Red_F_of_subset
       by (meson contra_subsetD i lnth_subset_Sup_llist)
   }
   then show "C \<in> Red_F (Sup_llist D)" using equiv_Sup_Liminf[of C] C_in_subset by fast
 qed
 
 (* lem:redundant-remains-redundant-during-run 1/2 *)
 lemma Red_Inf_subset_Liminf:
   assumes deriv: \<open>chain (\<rhd>Red) D\<close> and
     i: \<open>enat i < llength D\<close>
   shows \<open>Red_Inf (lnth D i) \<subseteq> Red_Inf (Liminf_llist D)\<close>
 proof -
   have Sup_in_diff: \<open>Red_Inf (Sup_llist D) \<subseteq> Red_Inf (Sup_llist D - (Sup_llist D - Liminf_llist D))\<close>
     using Red_Inf_of_Red_F_subset[OF Red_in_Sup] deriv by auto
   also have \<open>Sup_llist D - (Sup_llist D - Liminf_llist D) = Liminf_llist D\<close>
     by (simp add: Liminf_llist_subset_Sup_llist double_diff)
   then have Red_Inf_Sup_in_Liminf: \<open>Red_Inf (Sup_llist D) \<subseteq> Red_Inf (Liminf_llist D)\<close> using Sup_in_diff by auto
   have \<open>lnth D i \<subseteq> Sup_llist D\<close> unfolding Sup_llist_def using i by blast
   then have "Red_Inf (lnth D i) \<subseteq> Red_Inf (Sup_llist D)" using Red_Inf_of_subset
     unfolding Sup_llist_def by auto
   then show ?thesis using Red_Inf_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) D\<close> and
     i: \<open>enat i < llength D\<close>
   shows \<open>Red_F (lnth D i) \<subseteq> Red_F (Liminf_llist D)\<close>
 proof -
   have Sup_in_diff: \<open>Red_F (Sup_llist D) \<subseteq> Red_F (Sup_llist D - (Sup_llist D - Liminf_llist D))\<close>
     using Red_F_of_Red_F_subset[OF Red_in_Sup] deriv by auto
   also have \<open>Sup_llist D - (Sup_llist D - Liminf_llist D) = Liminf_llist D\<close>
     by (simp add: Liminf_llist_subset_Sup_llist double_diff)
   then have Red_F_Sup_in_Liminf: \<open>Red_F (Sup_llist D) \<subseteq> Red_F (Liminf_llist D)\<close>
     using Sup_in_diff by auto
   have \<open>lnth D i \<subseteq> Sup_llist D\<close> unfolding Sup_llist_def using i by blast
   then have "Red_F (lnth D i) \<subseteq> Red_F (Sup_llist D)" 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) D\<close> and
     i: \<open>enat i < llength D\<close>
   shows \<open>lnth D i \<subseteq> Red_F (Liminf_llist D) \<union> Liminf_llist D\<close>
 proof (rule,rule)
   fix C
   assume C: \<open>C \<in> lnth D i\<close>
   and C_not_Liminf: \<open>C \<notin> Liminf_llist D\<close>
   have \<open>C \<in> Sup_llist D\<close> unfolding Sup_llist_def using C i by auto
   then obtain j where j: \<open>C \<in> lnth D j - lnth D (Suc j)\<close> \<open>enat (Suc j) < llength D\<close>
     using equiv_Sup_Liminf[of C D] C_not_Liminf by auto
   then have \<open>C \<in> Red_F (lnth D (Suc j))\<close>
     using deriv by (meson chain_lnth_rel contra_subsetD derive.cases)
   then show \<open>C \<in> Red_F (Liminf_llist D)\<close> using Red_F_subset_Liminf[of D "Suc j"] deriv j(2) by blast
 qed
 
 (* lem:fairness-implies-saturation *)
 lemma fair_implies_Liminf_saturated:
   assumes
     deriv: \<open>chain (\<rhd>Red) D\<close> and
     fair: \<open>fair D\<close>
   shows \<open>saturated (Liminf_llist D)\<close>
   unfolding saturated_def
 proof
   fix \<iota>
   assume \<iota>: \<open>\<iota> \<in> Inf_from (Liminf_llist D)\<close>
   have \<open>\<iota> \<in> Sup_Red_Inf_llist D\<close> using fair \<iota> unfolding fair_def by auto
   then obtain i where i: \<open>enat i < llength D\<close> \<open>\<iota> \<in> Red_Inf (lnth D i)\<close>
     unfolding Sup_Red_Inf_llist_def by auto
   then show \<open>\<iota> \<in> Red_Inf (Liminf_llist D)\<close>
     using deriv i_in_Liminf_or_Red_F[of D i] Red_Inf_subset_Liminf by blast
 qed
 
 end
 
 locale static_refutational_complete_calculus = calculus_with_red_crit +
   assumes static_refutational_complete: "B \<in> Bot \<Longrightarrow> saturated N \<Longrightarrow> N \<Turnstile> {B} \<Longrightarrow> \<exists>B'\<in>Bot. B' \<in> N"
 
 locale dynamic_refutational_complete_calculus = calculus_with_red_crit +
   assumes
-    dynamic_refutational_complete: "B \<in> Bot \<Longrightarrow> chain (\<rhd>Red) D \<Longrightarrow> fair D
-      \<Longrightarrow> lnth D 0 \<Turnstile> {B} \<Longrightarrow> \<exists>i \<in> {i. enat i < llength D}. \<exists>B'\<in>Bot. B' \<in> lnth D i"
+    dynamic_refutational_complete: "B \<in> Bot \<Longrightarrow> chain (\<rhd>Red) D \<Longrightarrow> fair D \<Longrightarrow> lnth D 0 \<Turnstile> {B} \<Longrightarrow>
+      \<exists>i \<in> {i. enat i < llength D}. \<exists>B'\<in>Bot. B' \<in> lnth D i"
 begin
 
 (* lem:dynamic-ref-compl-implies-static *)
 sublocale static_refutational_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 D where "D = LCons N LNil"
   have[simp]: \<open>\<not> lnull D\<close> by (auto simp: D_def)
   have deriv_D: \<open>chain (\<rhd>Red) D\<close> by (simp add: chain.chain_singleton D_def)
   have liminf_is_N: "Liminf_llist D = N" by (simp add: D_def Liminf_llist_LCons)
   have head_D: "N = lnth D 0" by (simp add: D_def)
   have "Sup_Red_Inf_llist D = Red_Inf N" by (simp add: D_def Sup_Red_Inf_unit)
   then have fair_D: "fair D" 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 D i" and \<open>i < llength D\<close>
     using dynamic_refutational_complete[of B D] bot_elem fair_D head_D saturated_N deriv_D refut_N
     by auto
   then have "i = 0"
     by (auto simp: D_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] by auto
 qed
 
 end
 
 (* lem:static-ref-compl-implies-dynamic *)
 sublocale static_refutational_complete_calculus \<subseteq> dynamic_refutational_complete_calculus
 proof
   fix B D
   assume
     bot_elem: \<open>B \<in> Bot\<close> and
     deriv: \<open>chain (\<rhd>Red) D\<close> and
     fair: \<open>fair D\<close> and
     unsat: \<open>lnth D 0 \<Turnstile> {B}\<close>
     have non_empty: \<open>\<not> lnull D\<close> using chain_not_lnull[OF deriv] .
     have subs: \<open>lnth D 0 \<subseteq> Sup_llist D\<close>
       using lhd_subset_Sup_llist[of D] non_empty by (simp add: lhd_conv_lnth)
     have \<open>Sup_llist D \<Turnstile> {B}\<close>
       using unsat subset_entailed[OF subs] entails_trans[of "Sup_llist D" "lnth D 0"] by auto
     then have Sup_no_Red: \<open>Sup_llist D - Red_F (Sup_llist D) \<Turnstile> {B}\<close>
       using bot_elem Red_F_Bot by auto
     have Sup_no_Red_in_Liminf: \<open>Sup_llist D - Red_F (Sup_llist D) \<subseteq> Liminf_llist D\<close>
       using deriv Red_in_Sup by auto
     have Liminf_entails_Bot: \<open>Liminf_llist D \<Turnstile> {B}\<close>
       using Sup_no_Red subset_entailed[OF Sup_no_Red_in_Liminf] entails_trans by blast
     have \<open>saturated (Liminf_llist D)\<close>
       using deriv fair fair_implies_Liminf_saturated unfolding saturated_def by auto
 
    then have \<open>\<exists>B'\<in>Bot. B' \<in> Liminf_llist D\<close>
      using bot_elem static_refutational_complete Liminf_entails_Bot by auto
    then show \<open>\<exists>i\<in>{i. enat i < llength D}. \<exists>B'\<in>Bot. B' \<in> lnth D i\<close>
      unfolding Liminf_llist_def by auto
 qed
 
 subsection \<open>Calculi with a Family of Redundancy Criteria\<close>
 
 locale calculus_with_red_crit_family =
   inference_system Inf + consequence_relation_family Bot Q entails_q
   for
     Bot :: "'f set" and
     Inf :: \<open>'f inference set\<close> and
     Q :: "'q set" and
     entails_q :: "'q \<Rightarrow> 'f set \<Rightarrow> 'f set \<Rightarrow> bool"
   + fixes
     Red_Inf_q :: "'q \<Rightarrow> 'f set \<Rightarrow> 'f inference set" and
     Red_F_q :: "'q \<Rightarrow> 'f set \<Rightarrow> 'f set"
   assumes
     Q_nonempty: "Q \<noteq> {}" and
     all_red_crit: "\<forall>q \<in> Q. calculus_with_red_crit Bot Inf (entails_q q) (Red_Inf_q q) (Red_F_q q)"
 begin
 
 definition Red_Inf_Q :: "'f set \<Rightarrow> 'f inference set" where
   "Red_Inf_Q N = (\<Inter>q \<in> Q. Red_Inf_q q N)"
 
 definition Red_F_Q :: "'f set \<Rightarrow> 'f set" where
   "Red_F_Q N = (\<Inter>q \<in> Q. Red_F_q q N)"
 
 (* lem:intersection-of-red-crit *)
-sublocale inter_red_crit_calculus: calculus_with_red_crit Bot Inf entails_Q Red_Inf_Q Red_F_Q
+sublocale calculus_with_red_crit Bot Inf entails_Q Red_Inf_Q Red_F_Q
   unfolding calculus_with_red_crit_def calculus_with_red_crit_axioms_def
 proof (intro conjI)
   show "consequence_relation Bot entails_Q"
   using intersect_cons_rel_family .
 next
   show "\<forall>N. Red_Inf_Q N \<subseteq> Inf"
     unfolding Red_Inf_Q_def
   proof
     fix N
     show "(\<Inter>q \<in> Q. Red_Inf_q q N) \<subseteq> Inf"
     proof (intro Inter_subset)
       fix Red_Infs
       assume one_red_inf: "Red_Infs \<in> (\<lambda>q. Red_Inf_q q N) ` Q"
       show "Red_Infs \<subseteq> Inf"
         using one_red_inf all_red_crit calculus_with_red_crit.Red_Inf_to_Inf by blast
     next
       show "(\<lambda>q. Red_Inf_q q N) ` Q \<noteq> {}"
         using Q_nonempty by blast
     qed
   qed
 next
   show "\<forall>B N. B \<in> Bot \<longrightarrow> N \<Turnstile>Q {B} \<longrightarrow> N - Red_F_Q N \<Turnstile>Q {B}"
   proof (intro allI impI)
     fix B N
     assume
       B_in: "B \<in> Bot" and
       N_unsat: "N \<Turnstile>Q {B}"
     show "N - Red_F_Q N \<Turnstile>Q {B}" unfolding entails_Q_def Red_F_Q_def
     proof
       fix qi
       assume qi_in: "qi \<in> Q"
       define entails_qi (infix "\<Turnstile>qi" 50) where "entails_qi = entails_q qi"
       have cons_rel_qi: "consequence_relation Bot entails_qi"
         unfolding entails_qi_def using qi_in all_red_crit calculus_with_red_crit.axioms(1) by blast
       define Red_F_qi where "Red_F_qi = Red_F_q qi"
       have red_qi_in_Q: "Red_F_Q N \<subseteq> Red_F_qi N"
         unfolding Red_F_Q_def Red_F_qi_def using qi_in image_iff by blast
-      then have "N - (Red_F_qi N) \<subseteq> N - (Red_F_Q N)" by blast
-      then have entails_1: "(N - Red_F_Q N) \<Turnstile>qi (N - Red_F_qi N)"
+      then have "N - Red_F_qi N \<subseteq> N - Red_F_Q N" by blast
+      then have entails_1: "N - Red_F_Q N \<Turnstile>qi N - Red_F_qi N"
         using qi_in all_red_crit
         unfolding calculus_with_red_crit_def consequence_relation_def entails_qi_def by metis
       have N_unsat_qi: "N \<Turnstile>qi {B}" using qi_in N_unsat unfolding entails_qi_def entails_Q_def
         by simp
-      then have N_unsat_qi: "(N - Red_F_qi N) \<Turnstile>qi {B}"
+      then have N_unsat_qi: "N - Red_F_qi N \<Turnstile>qi {B}"
         using qi_in all_red_crit Red_F_qi_def calculus_with_red_crit.Red_F_Bot[OF _ B_in]
           entails_qi_def
         by fastforce
-      show "(N - (\<Inter>q \<in> Q. Red_F_q q N)) \<Turnstile>qi {B}"
+      show "N - (\<Inter>q \<in> Q. Red_F_q q N) \<Turnstile>qi {B}"
         using consequence_relation.entails_trans[OF cons_rel_qi entails_1 N_unsat_qi]
         unfolding Red_F_Q_def .
     qed
   qed
 next
   show "\<forall>N1 N2. N1 \<subseteq> N2 \<longrightarrow> Red_F_Q N1 \<subseteq> Red_F_Q N2"
   proof (intro allI impI)
     fix N1 :: "'f set"
     and N2 :: "'f set"
     assume
       N1_in_N2: "N1 \<subseteq> N2"
     show "Red_F_Q N1 \<subseteq> Red_F_Q N2"
     proof
       fix C
       assume "C \<in> Red_F_Q N1"
       then have "\<forall>qi \<in> Q. C \<in> Red_F_q qi N1" unfolding Red_F_Q_def by blast
       then have "\<forall>qi \<in> Q. C \<in> Red_F_q qi N2"
         using N1_in_N2 all_red_crit calculus_with_red_crit.axioms(2)
           calculus_with_red_crit.Red_F_of_subset by blast
       then show "C \<in> Red_F_Q N2" unfolding Red_F_Q_def by blast
     qed
   qed
 next
   show "\<forall>N1 N2. N1 \<subseteq> N2 \<longrightarrow> Red_Inf_Q N1 \<subseteq> Red_Inf_Q N2"
   proof (intro allI impI)
     fix N1 :: "'f set"
     and N2 :: "'f set"
     assume
       N1_in_N2: "N1 \<subseteq> N2"
     show "Red_Inf_Q N1 \<subseteq> Red_Inf_Q N2"
     proof
       fix \<iota>
       assume "\<iota> \<in> Red_Inf_Q N1"
       then have "\<forall>qi \<in> Q. \<iota> \<in> Red_Inf_q qi N1" unfolding Red_Inf_Q_def by blast
       then have "\<forall>qi \<in> Q. \<iota> \<in> Red_Inf_q qi N2"
         using N1_in_N2 all_red_crit calculus_with_red_crit.axioms(2)
           calculus_with_red_crit.Red_Inf_of_subset by blast
       then show "\<iota> \<in> Red_Inf_Q N2" unfolding Red_Inf_Q_def by blast
     qed
   qed
 next
   show "\<forall>N2 N1. N2 \<subseteq> Red_F_Q N1 \<longrightarrow> Red_F_Q N1 \<subseteq> Red_F_Q (N1 - N2)"
   proof (intro allI impI)
     fix N2 N1
     assume N2_in_Red_N1: "N2 \<subseteq> Red_F_Q N1"
     show "Red_F_Q N1 \<subseteq> Red_F_Q (N1 - N2)"
     proof
       fix C
       assume "C \<in> Red_F_Q N1"
       then have "\<forall>qi \<in> Q. C \<in> Red_F_q qi N1" unfolding Red_F_Q_def by blast
       moreover have "\<forall>qi \<in> Q. N2 \<subseteq> Red_F_q qi N1" using N2_in_Red_N1 unfolding Red_F_Q_def by blast
       ultimately have "\<forall>qi \<in> Q. C \<in> Red_F_q qi (N1 - N2)"
         using all_red_crit calculus_with_red_crit.axioms(2)
           calculus_with_red_crit.Red_F_of_Red_F_subset
         by blast
       then show "C \<in> Red_F_Q (N1 - N2)" unfolding Red_F_Q_def by blast
     qed
   qed
 next
   show "\<forall>N2 N1. N2 \<subseteq> Red_F_Q N1 \<longrightarrow> Red_Inf_Q N1 \<subseteq> Red_Inf_Q (N1 - N2)"
   proof (intro allI impI)
     fix N2 N1
     assume N2_in_Red_N1: "N2 \<subseteq> Red_F_Q N1"
     show "Red_Inf_Q N1 \<subseteq> Red_Inf_Q (N1 - N2)"
     proof
       fix \<iota>
       assume "\<iota> \<in> Red_Inf_Q N1"
       then have "\<forall>qi \<in> Q. \<iota> \<in> Red_Inf_q qi N1" unfolding Red_Inf_Q_def by blast
       moreover have "\<forall>qi \<in> Q. N2 \<subseteq> Red_F_q qi N1" using N2_in_Red_N1 unfolding Red_F_Q_def by blast
       ultimately have "\<forall>qi \<in> Q. \<iota> \<in> Red_Inf_q qi (N1 - N2)"
         using all_red_crit calculus_with_red_crit.axioms(2)
           calculus_with_red_crit.Red_Inf_of_Red_F_subset by blast
       then show "\<iota> \<in> Red_Inf_Q (N1 - N2)" unfolding Red_Inf_Q_def by blast
     qed
   qed
 next
   show "\<forall>\<iota> N. \<iota> \<in> Inf \<longrightarrow> concl_of \<iota> \<in> N \<longrightarrow> \<iota> \<in> Red_Inf_Q N"
   proof (intro allI impI)
     fix \<iota> N
     assume
       i_in: "\<iota> \<in> Inf" and
       concl_in: "concl_of \<iota> \<in> N"
     then have "\<forall>qi \<in> Q. \<iota> \<in> Red_Inf_q qi N"
       using all_red_crit calculus_with_red_crit.axioms(2) calculus_with_red_crit.Red_Inf_of_Inf_to_N by blast
     then show "\<iota> \<in> Red_Inf_Q N" unfolding Red_Inf_Q_def by blast
   qed
 qed
 
 (* lem:satur-wrt-intersection-of-red *)
 lemma sat_int_to_sat_q: "calculus_with_red_crit.saturated Inf Red_Inf_Q N \<longleftrightarrow>
   (\<forall>qi \<in> Q. calculus_with_red_crit.saturated Inf (Red_Inf_q qi) N)" for N
 proof
   fix N
   assume inter_sat: "calculus_with_red_crit.saturated Inf Red_Inf_Q N"
   show "\<forall>qi \<in> Q. calculus_with_red_crit.saturated Inf (Red_Inf_q qi) N"
   proof
     fix qi
     assume qi_in: "qi \<in> Q"
     then interpret one: calculus_with_red_crit Bot Inf "entails_q qi" "Red_Inf_q qi" "Red_F_q qi"
       by (metis all_red_crit)
     show "one.saturated N"
       using qi_in inter_sat
-      unfolding one.saturated_def inter_red_crit_calculus.saturated_def Red_Inf_Q_def by blast
+      unfolding one.saturated_def saturated_def Red_Inf_Q_def by blast
   qed
 next
   fix N
   assume all_sat: "\<forall>qi \<in> Q. calculus_with_red_crit.saturated Inf (Red_Inf_q qi) N"
-  show "inter_red_crit_calculus.saturated N"
-    unfolding inter_red_crit_calculus.saturated_def Red_Inf_Q_def
+  show "saturated N"
+    unfolding saturated_def Red_Inf_Q_def
   proof
     fix \<iota>
     assume \<iota>_in: "\<iota> \<in> Inf_from N"
     have "\<forall>Red_Inf_qi \<in> Red_Inf_q ` Q. \<iota> \<in> Red_Inf_qi N"
     proof
       fix Red_Inf_qi
       assume red_inf_in: "Red_Inf_qi \<in> Red_Inf_q ` Q"
       then obtain qi where
         qi_in: "qi \<in> Q" and
         red_inf_qi_def: "Red_Inf_qi = Red_Inf_q qi" by blast
       then interpret one: calculus_with_red_crit Bot Inf "entails_q qi" "Red_Inf_q qi" "Red_F_q qi"
         by (metis all_red_crit)
       have "one.saturated N" using qi_in all_sat red_inf_qi_def by blast
       then show "\<iota> \<in> Red_Inf_qi N" unfolding one.saturated_def using \<iota>_in red_inf_qi_def by blast
     qed
     then show "\<iota> \<in> (\<Inter>q \<in> Q. Red_Inf_q q N)" by blast
   qed
 qed
 
 (* lem:checking-static-ref-compl-for-intersections *)
 lemma stat_ref_comp_from_bot_in_sat:
   "(\<forall>N. calculus_with_red_crit.saturated Inf Red_Inf_Q N \<and> (\<forall>B \<in> Bot. B \<notin> N) \<longrightarrow>
       (\<exists>B \<in> Bot. \<exists>qi \<in> Q. \<not> entails_q qi N {B})) \<Longrightarrow>
    static_refutational_complete_calculus Bot Inf entails_Q Red_Inf_Q Red_F_Q"
 proof (rule ccontr)
   assume
     N_saturated: "\<forall>N. (calculus_with_red_crit.saturated Inf Red_Inf_Q N \<and> (\<forall>B \<in> Bot. B \<notin> N)) \<longrightarrow>
       (\<exists>B \<in> Bot. \<exists>qi \<in> Q. \<not> entails_q qi N {B})" and
     no_stat_ref_comp: "\<not> static_refutational_complete_calculus Bot Inf (\<Turnstile>Q) Red_Inf_Q Red_F_Q"
   obtain N1 B1 where B1_in:
     "B1 \<in> Bot" and N1_saturated: "calculus_with_red_crit.saturated Inf Red_Inf_Q N1" and
     N1_unsat: "N1 \<Turnstile>Q {B1}" and no_B_in_N1: "\<forall>B \<in> Bot. B \<notin> N1"
-    using no_stat_ref_comp by (metis inter_red_crit_calculus.calculus_with_red_crit_axioms
+    using no_stat_ref_comp by (metis calculus_with_red_crit_axioms
         static_refutational_complete_calculus.intro
         static_refutational_complete_calculus_axioms.intro)
   obtain B2 qi where
     qi_in: "qi \<in> Q" and
     no_qi: "\<not> entails_q qi N1 {B2}"
     using N_saturated N1_saturated no_B_in_N1 by auto
   have "N1 \<Turnstile>Q {B2}" using N1_unsat B1_in intersect_cons_rel_family
     unfolding consequence_relation_def by metis
   then have "entails_q qi N1 {B2}" unfolding entails_Q_def using qi_in by blast
   then show False using no_qi by simp
 qed
 
 end
 
 subsection \<open>Families of Calculi with a Family of Redundancy Criteria\<close>
 
 locale calculus_family_with_red_crit_family =
   inference_system_family Q Inf_q + consequence_relation_family Bot Q entails_q
   for
     Bot :: "'f set" and
     Q :: "'q set" and
     Inf_q :: \<open>'q \<Rightarrow> 'f inference set\<close> and
     entails_q :: "'q \<Rightarrow> 'f set \<Rightarrow> 'f set \<Rightarrow> bool"
   + fixes
     Red_Inf_q :: "'q \<Rightarrow> 'f set \<Rightarrow> 'f inference set" and
     Red_F_q :: "'q \<Rightarrow> 'f set \<Rightarrow> 'f set"
   assumes
     Q_nonempty: "Q \<noteq> {}" and
     all_red_crit:
       "\<forall>q \<in> Q. calculus_with_red_crit Bot (Inf_q q) (entails_q q) (Red_Inf_q q) (Red_F_q q)"
 
 subsection \<open>Variations on a Theme\<close>
 
 locale calculus_with_reduced_red_crit = calculus_with_red_crit Bot Inf entails Red_Inf 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_Inf :: "'f set \<Rightarrow> 'f inference set" and
     Red_F :: "'f set \<Rightarrow> 'f set"
  + assumes
    inf_in_red_inf: "Inf_from2 UNIV (Red_F N) \<subseteq> Red_Inf 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_Inf_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_from2_def
     by blast
 qed
 
 end
 
 locale reduc_static_refutational_complete_calculus = calculus_with_red_crit +
   assumes reduc_static_refutational_complete:
     "B \<in> Bot \<Longrightarrow> reduc_saturated N \<Longrightarrow> N \<Turnstile> {B} \<Longrightarrow> \<exists>B'\<in>Bot. B' \<in> N"
 
 locale reduc_static_refutational_complete_reduc_calculus = calculus_with_reduced_red_crit +
   assumes reduc_static_refutational_complete:
     "B \<in> Bot \<Longrightarrow> reduc_saturated N \<Longrightarrow> N \<Turnstile> {B} \<Longrightarrow> \<exists>B'\<in>Bot. B' \<in> N"
 begin
 
 sublocale reduc_static_refutational_complete_calculus
   by (simp add: calculus_with_red_crit_axioms reduc_static_refutational_complete
     reduc_static_refutational_complete_calculus_axioms.intro
     reduc_static_refutational_complete_calculus_def)
 
 (* cor:reduced-rc-implies-st-ref-comp-equiv-reduced-st-ref-comp 1/2 *)
 sublocale static_refutational_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 reduc_static_refutational_complete[OF bot_elem reduc_saturated_N refut_N] .
 qed
 
 end
 
 context calculus_with_reduced_red_crit
 begin
 
 (* cor:reduced-rc-implies-st-ref-comp-equiv-reduced-st-ref-comp 2/2 *)
 lemma stat_ref_comp_imp_red_stat_ref_comp:
   "static_refutational_complete_calculus Bot Inf entails Red_Inf Red_F \<Longrightarrow>
    reduc_static_refutational_complete_calculus Bot Inf entails Red_Inf Red_F"
 proof
   fix B N
   assume
     stat_ref_comp: "static_refutational_complete_calculus Bot Inf (\<Turnstile>) Red_Inf 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 static_refutational_complete_calculus.static_refutational_complete[OF stat_ref_comp
       bot_elem reduc_saturated_N refut_N] .
 qed
 
 end
 
 context calculus_with_red_crit
 begin
 
 definition Red_Red_Inf :: "'f set \<Rightarrow> 'f inference set" where
   "Red_Red_Inf N = Red_Inf N \<union> Inf_from2 UNIV (Red_F N)"
 
 lemma reduced_calc_is_calc: "calculus_with_red_crit Bot Inf entails Red_Red_Inf Red_F"
 proof
   fix N
   show "Red_Red_Inf N \<subseteq> Inf"
     unfolding Red_Red_Inf_def Inf_from2_def Inf_from_def using Red_Inf_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_from2 UNIV (Red_F N) \<subseteq> Inf_from2 UNIV (Red_F N')"
     unfolding Inf_from2_def by auto
   then show "Red_Red_Inf N \<subseteq> Red_Red_Inf N'"
     unfolding Red_Red_Inf_def using Red_Inf_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_from2 UNIV (Red_F N) \<subseteq> Inf_from2 UNIV (Red_F (N - N'))"
     unfolding Inf_from2_def by auto
   then show "Red_Red_Inf N \<subseteq> Red_Red_Inf (N - N')"
     unfolding Red_Red_Inf_def using Red_Inf_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_Inf N"
     by (simp add: Red_Inf_of_Inf_to_N Red_Red_Inf_def)
 qed
 
 lemma inf_subs_reduced_red_inf: "Inf_from2 UNIV (Red_F N) \<subseteq> Red_Red_Inf N"
   unfolding Red_Red_Inf_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: "calculus_with_reduced_red_crit Bot Inf entails Red_Red_Inf Red_F"
   using inf_subs_reduced_red_inf reduced_calc_is_calc
   by (simp add: calculus_with_reduced_red_crit.intro calculus_with_reduced_red_crit_axioms_def)
 
 interpretation reduc_calc: calculus_with_reduced_red_crit Bot Inf entails Red_Red_Inf 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_Inf_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_Inf N"
       using i_in red_sat_n unfolding reduc_saturated_def Inf_from2_def Inf_from_def Red_Red_Inf_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_Inf N"
       using i_in red_sat_n unfolding Inf_from_def reduc_calc.saturated_def Red_Red_Inf_def Inf_from2_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_Inf_without_red_F)
 
 (* thm:reduced-stat-ref-compl 1/3 (i) \<longleftrightarrow> (iii) *)
 theorem stat_is_stat_red: "static_refutational_complete_calculus Bot Inf entails Red_Inf Red_F \<longleftrightarrow>
   static_refutational_complete_calculus Bot Inf entails Red_Red_Inf Red_F"
 proof
   assume
     stat_ref1: "static_refutational_complete_calculus Bot Inf entails Red_Inf Red_F"
   show "static_refutational_complete_calculus Bot Inf entails Red_Red_Inf Red_F"
     using reduc_calc.calculus_with_red_crit_axioms
     unfolding static_refutational_complete_calculus_def static_refutational_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 static_refutational_complete_calculus.static_refutational_complete)
     qed
   qed
 next
   assume
     stat_ref3: "static_refutational_complete_calculus Bot Inf entails Red_Red_Inf Red_F"
   show "static_refutational_complete_calculus Bot Inf entails Red_Inf Red_F"
     unfolding static_refutational_complete_calculus_def static_refutational_complete_calculus_axioms_def
     using calculus_with_red_crit_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 static_refutational_complete_calculus.static_refutational_complete)
     qed
   qed
 qed
 
 (* thm:reduced-stat-ref-compl 2/3 (iv) \<longleftrightarrow> (iii) *)
 theorem red_stat_red_is_stat_red: "reduc_static_refutational_complete_calculus Bot Inf entails Red_Red_Inf Red_F \<longleftrightarrow>
   static_refutational_complete_calculus Bot Inf entails Red_Red_Inf Red_F"
   using reduc_calc.stat_ref_comp_imp_red_stat_ref_comp
   by (metis reduc_calc.sat_eq_reduc_sat reduc_static_refutational_complete_calculus.axioms(2)
     reduc_static_refutational_complete_calculus_axioms_def reduced_calc_is_calc
     static_refutational_complete_calculus.intro static_refutational_complete_calculus_axioms.intro)
 
 (* thm:reduced-stat-ref-compl 3/3 (ii) \<longleftrightarrow> (iii) *)
 theorem red_stat_is_stat_red: "reduc_static_refutational_complete_calculus Bot Inf entails Red_Inf Red_F \<longleftrightarrow>
   static_refutational_complete_calculus Bot Inf entails Red_Red_Inf Red_F"
   using reduc_calc.calculus_with_red_crit_axioms calculus_with_red_crit_axioms red_sat_eq_red_calc_sat
   unfolding static_refutational_complete_calculus_def static_refutational_complete_calculus_axioms_def
     reduc_static_refutational_complete_calculus_def reduc_static_refutational_complete_calculus_axioms_def
   by blast
 
 definition Sup_Red_F_llist :: "'f set llist \<Rightarrow> 'f set" where
 "Sup_Red_F_llist D = (\<Union>i \<in> {i. enat i < llength D}. Red_F (lnth D i))"
 
 lemma Sup_Red_F_unit: "Sup_Red_F_llist (LCons X LNil) = Red_F X"
 using Sup_Red_F_llist_def enat_0_iff(1) by simp
 
 lemma sup_red_f_in_red_liminf: "chain derive D \<Longrightarrow> Sup_Red_F_llist D \<subseteq> Red_F (Liminf_llist D)"
 proof
   fix N
   assume
     deriv: "chain derive D" and
     n_in_sup: "N \<in> Sup_Red_F_llist D"
   obtain i0 where i_smaller: "enat i0 < llength D" and n_in: "N \<in> Red_F (lnth D i0)"
     using n_in_sup unfolding Sup_Red_F_llist_def by blast
   have "Red_F (lnth D i0) \<subseteq> Red_F (Liminf_llist D)"
     using i_smaller by (simp add: deriv Red_F_subset_Liminf)
   then show "N \<in> Red_F (Liminf_llist D)"
     using n_in by fast
 qed
 
 lemma sup_red_inf_in_red_liminf: "chain derive D \<Longrightarrow> Sup_Red_Inf_llist D \<subseteq> Red_Inf (Liminf_llist D)"
 proof
   fix \<iota>
   assume
     deriv: "chain derive D" and
     i_in_sup: "\<iota> \<in> Sup_Red_Inf_llist D"
   obtain i0 where i_smaller: "enat i0 < llength D" and n_in: "\<iota> \<in> Red_Inf (lnth D i0)"
     using i_in_sup unfolding Sup_Red_Inf_llist_def by blast
   have "Red_Inf (lnth D i0) \<subseteq> Red_Inf (Liminf_llist D)"
     using i_smaller by (simp add: deriv Red_Inf_subset_Liminf)
   then show "\<iota> \<in> Red_Inf (Liminf_llist D)"
     using n_in by fast
 qed
 
 definition reduc_fair :: "'f set llist \<Rightarrow> bool" where
   "reduc_fair D \<longleftrightarrow> Inf_from (Liminf_llist D - (Sup_Red_F_llist D)) \<subseteq> Sup_Red_Inf_llist D"
 
 (* lem:red-fairness-implies-red-saturation *)
 lemma reduc_fair_imp_Liminf_reduc_sat: "chain derive D \<Longrightarrow> reduc_fair D \<Longrightarrow> reduc_saturated (Liminf_llist D)"
   unfolding reduc_saturated_def
 proof -
   fix D
   assume
     deriv: "chain derive D" and
     red_fair: "reduc_fair D"
   have "Inf_from (Liminf_llist D - Red_F (Liminf_llist D)) \<subseteq> Inf_from (Liminf_llist D - Sup_Red_F_llist D)"
     using sup_red_f_in_red_liminf[OF deriv] unfolding Inf_from_def by blast
   then have "Inf_from (Liminf_llist D - Red_F (Liminf_llist D)) \<subseteq> Sup_Red_Inf_llist D"
     using red_fair unfolding reduc_fair_def by simp
   then show "Inf_from (Liminf_llist D - Red_F (Liminf_llist D)) \<subseteq> Red_Inf (Liminf_llist D)"
     using sup_red_inf_in_red_liminf[OF deriv] by fast
 qed
 
 end
 
 locale reduc_dynamic_refutational_complete_calculus = calculus_with_red_crit +
   assumes
     reduc_dynamic_refutational_complete: "B \<in> Bot \<Longrightarrow> chain derive D \<Longrightarrow> reduc_fair D
       \<Longrightarrow> lnth D 0 \<Turnstile> {B} \<Longrightarrow> \<exists>i \<in> {i. enat i < llength D}. \<exists> B'\<in>Bot. B' \<in> lnth D i"
 begin
 
 sublocale reduc_static_refutational_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 D where "D = LCons N LNil"
   have[simp]: \<open>\<not> lnull D\<close> by (auto simp: D_def)
   have deriv_D: \<open>chain (\<rhd>Red) D\<close> by (simp add: chain.chain_singleton D_def)
   have liminf_is_N: "Liminf_llist D = N" by (simp add: D_def Liminf_llist_LCons)
   have head_D: "N = lnth D 0" by (simp add: D_def)
   have "Sup_Red_F_llist D = Red_F N" by (simp add: D_def Sup_Red_F_unit)
   moreover have "Sup_Red_Inf_llist D = Red_Inf N" by (simp add: D_def Sup_Red_Inf_unit)
   ultimately have fair_D: "reduc_fair D"
     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 D i" and \<open>i < llength D\<close>
     using reduc_dynamic_refutational_complete[of B D] bot_elem fair_D head_D saturated_N deriv_D refut_N
     by auto
   then have "i = 0"
     by (auto simp: D_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] by auto
 qed
 
 end
 
 sublocale reduc_static_refutational_complete_calculus \<subseteq> reduc_dynamic_refutational_complete_calculus
 proof
   fix B D
   assume
     bot_elem: \<open>B \<in> Bot\<close> and
     deriv: \<open>chain (\<rhd>Red) D\<close> and
     fair: \<open>reduc_fair D\<close> and
     unsat: \<open>(lnth D 0) \<Turnstile> {B}\<close>
     have non_empty: \<open>\<not> lnull D\<close> using chain_not_lnull[OF deriv] .
     have subs: \<open>(lnth D 0) \<subseteq> Sup_llist D\<close>
       using lhd_subset_Sup_llist[of D] non_empty by (simp add: lhd_conv_lnth)
     have \<open>Sup_llist D \<Turnstile> {B}\<close>
       using unsat subset_entailed[OF subs] entails_trans[of "Sup_llist D" "lnth D 0"] by auto
     then have Sup_no_Red: \<open>Sup_llist D - Red_F (Sup_llist D) \<Turnstile> {B}\<close>
       using bot_elem Red_F_Bot by auto
     have Sup_no_Red_in_Liminf: \<open>Sup_llist D - Red_F (Sup_llist D) \<subseteq> Liminf_llist D\<close>
       using deriv Red_in_Sup by auto
     have Liminf_entails_Bot: \<open>Liminf_llist D \<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 D)\<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 D\<close>
      using bot_elem reduc_static_refutational_complete Liminf_entails_Bot
      by auto
    then show \<open>\<exists>i\<in>{i. enat i < llength D}. \<exists>B'\<in>Bot. B' \<in> lnth D i\<close>
      unfolding Liminf_llist_def by auto
 qed
 
 context calculus_with_red_crit
 begin
 
 lemma dyn_equiv_stat: "dynamic_refutational_complete_calculus Bot Inf entails Red_Inf Red_F =
   static_refutational_complete_calculus Bot Inf entails Red_Inf Red_F"
 proof
   assume "dynamic_refutational_complete_calculus Bot Inf entails Red_Inf Red_F"
   then interpret dynamic_refutational_complete_calculus Bot Inf entails Red_Inf Red_F
     by simp
   show "static_refutational_complete_calculus Bot Inf entails Red_Inf Red_F"
     by (simp add: static_refutational_complete_calculus_axioms)
 next
   assume "static_refutational_complete_calculus Bot Inf entails Red_Inf Red_F"
   then interpret static_refutational_complete_calculus Bot Inf entails Red_Inf Red_F
     by simp
   show "dynamic_refutational_complete_calculus Bot Inf entails Red_Inf Red_F"
     by (simp add: dynamic_refutational_complete_calculus_axioms)
 qed
 
 lemma red_dyn_equiv_red_stat: "reduc_dynamic_refutational_complete_calculus Bot Inf entails Red_Inf Red_F =
   reduc_static_refutational_complete_calculus Bot Inf entails Red_Inf Red_F"
 proof
   assume "reduc_dynamic_refutational_complete_calculus Bot Inf entails Red_Inf Red_F"
   then interpret reduc_dynamic_refutational_complete_calculus Bot Inf entails Red_Inf Red_F
     by simp
   show "reduc_static_refutational_complete_calculus Bot Inf entails Red_Inf Red_F"
     by (simp add: reduc_static_refutational_complete_calculus_axioms)
 next
   assume "reduc_static_refutational_complete_calculus Bot Inf entails Red_Inf Red_F"
   then interpret reduc_static_refutational_complete_calculus Bot Inf entails Red_Inf Red_F
     by simp
   show "reduc_dynamic_refutational_complete_calculus Bot Inf entails Red_Inf Red_F"
     by (simp add: reduc_dynamic_refutational_complete_calculus_axioms)
 qed
 
 interpretation reduc_calc: calculus_with_reduced_red_crit Bot Inf entails Red_Red_Inf Red_F
   by (fact reduc_calc)
 
 (* thm:reduced-dyn-ref-compl 1/3 (v) \<longleftrightarrow> (vii) *)
 theorem dyn_ref_eq_dyn_ref_red:
   "dynamic_refutational_complete_calculus Bot Inf entails Red_Inf Red_F \<longleftrightarrow>
    dynamic_refutational_complete_calculus Bot Inf entails Red_Red_Inf 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:
   "reduc_dynamic_refutational_complete_calculus Bot Inf entails Red_Red_Inf Red_F \<longleftrightarrow>
    dynamic_refutational_complete_calculus Bot Inf entails Red_Red_Inf 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:
   "reduc_dynamic_refutational_complete_calculus Bot Inf entails Red_Inf Red_F \<longleftrightarrow>
    dynamic_refutational_complete_calculus Bot Inf entails Red_Red_Inf 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/Labeled_Lifting_to_Non_Ground_Calculi.thy b/thys/Saturation_Framework/Labeled_Lifting_to_Non_Ground_Calculi.thy
--- a/thys/Saturation_Framework/Labeled_Lifting_to_Non_Ground_Calculi.thy
+++ b/thys/Saturation_Framework/Labeled_Lifting_to_Non_Ground_Calculi.thy
@@ -1,430 +1,426 @@
 (*  Title:       Labeled Lifting to Non-Ground Calculi of the Saturation Framework
  *  Author:      Sophie Tourret <stourret at mpi-inf.mpg.de>, 2019-2020 *)
 
 section \<open>Labeled Liftings\<close>
 
 text \<open>This section formalizes the extension of the lifting results to labeled
   calculi. This corresponds to section 3.4 of the report.\<close>
 
 theory Labeled_Lifting_to_Non_Ground_Calculi
   imports Lifting_to_Non_Ground_Calculi
 begin
 
 subsection \<open>Labeled Lifting with a Family of Well-founded Orderings\<close>
 
 locale labeled_lifting_w_wf_ord_family =
   lifting_with_wf_ordering_family Bot_F Inf_F Bot_G entails_G Inf_G Red_Inf_G Red_F_G \<G>_F \<G>_Inf Prec_F
   for
     Bot_F :: "'f set" and
     Inf_F :: "'f inference set" and
     Bot_G :: "'g set" and
     entails_G :: "'g set \<Rightarrow> 'g set \<Rightarrow> bool"  (infix "\<Turnstile>G" 50) and
     Inf_G :: "'g inference set" and
     Red_Inf_G :: "'g set \<Rightarrow> 'g inference set" and
     Red_F_G :: "'g set \<Rightarrow> 'g set" and
     \<G>_F :: "'f \<Rightarrow> 'g set" and
     \<G>_Inf :: "'f inference \<Rightarrow> 'g inference set option" and
     Prec_F :: "'g \<Rightarrow> 'f \<Rightarrow> 'f \<Rightarrow> bool" (infix "\<sqsubset>" 50)
   + fixes
     Inf_FL :: \<open>('f \<times> 'l) inference set\<close>
   assumes
     Inf_F_to_Inf_FL: \<open>\<iota>\<^sub>F \<in> Inf_F \<Longrightarrow> length (Ll :: 'l list) = length (prems_of \<iota>\<^sub>F) \<Longrightarrow>
       \<exists>L0. Infer (zip (prems_of \<iota>\<^sub>F) Ll) (concl_of \<iota>\<^sub>F, L0) \<in> Inf_FL\<close> and
     Inf_FL_to_Inf_F: \<open>\<iota>\<^sub>F\<^sub>L \<in> Inf_FL \<Longrightarrow> Infer (map fst (prems_of \<iota>\<^sub>F\<^sub>L)) (fst (concl_of \<iota>\<^sub>F\<^sub>L)) \<in> Inf_F\<close>
 begin
 
 definition to_F :: \<open>('f \<times> 'l) inference \<Rightarrow> 'f inference\<close> where
   \<open>to_F \<iota>\<^sub>F\<^sub>L = Infer (map fst (prems_of \<iota>\<^sub>F\<^sub>L)) (fst (concl_of \<iota>\<^sub>F\<^sub>L))\<close>
 
 definition Bot_FL :: \<open>('f \<times> 'l) set\<close> where \<open>Bot_FL = Bot_F \<times> UNIV\<close>
 
 definition \<G>_F_L :: \<open>('f \<times> 'l) \<Rightarrow> 'g set\<close> where \<open>\<G>_F_L CL = \<G>_F (fst CL)\<close>
 
 definition \<G>_Inf_L :: \<open>('f \<times> 'l) inference \<Rightarrow> 'g inference set option\<close> where \<open>\<G>_Inf_L \<iota>\<^sub>F\<^sub>L = \<G>_Inf (to_F \<iota>\<^sub>F\<^sub>L)\<close>
 
 (* lem:labeled-grounding-function *)
 sublocale labeled_standard_lifting: standard_lifting
   where
     Bot_F = Bot_FL and
     Inf_F = Inf_FL and
     \<G>_F = \<G>_F_L and
     \<G>_Inf = \<G>_Inf_L
 proof
   show "Bot_FL \<noteq> {}"
     unfolding Bot_FL_def using Bot_F_not_empty by simp
 next
   show "B\<in>Bot_FL \<Longrightarrow> \<G>_F_L B \<noteq> {}" for B
     unfolding \<G>_F_L_def Bot_FL_def using Bot_map_not_empty by auto
 next
   show "B\<in>Bot_FL \<Longrightarrow> \<G>_F_L B \<subseteq> Bot_G" for B
     unfolding \<G>_F_L_def Bot_FL_def using Bot_map by force
 next
   fix CL
   show "\<G>_F_L CL \<inter> Bot_G \<noteq> {} \<longrightarrow> CL \<in> Bot_FL"
     unfolding \<G>_F_L_def Bot_FL_def using Bot_cond
     by (metis SigmaE UNIV_I UNIV_Times_UNIV mem_Sigma_iff prod.sel(1))
 next
   fix \<iota>
   assume
     i_in: \<open>\<iota> \<in> Inf_FL\<close> and
     ground_not_none: \<open>\<G>_Inf_L \<iota> \<noteq> None\<close>
   then show "the (\<G>_Inf_L \<iota>) \<subseteq> Red_Inf_G (\<G>_F_L (concl_of \<iota>))"
     unfolding \<G>_Inf_L_def \<G>_F_L_def to_F_def using inf_map Inf_FL_to_Inf_F by fastforce
 qed
 
 abbreviation Labeled_Empty_Order :: \<open> ('f \<times> 'l) \<Rightarrow> ('f \<times> 'l) \<Rightarrow> bool\<close> where
   "Labeled_Empty_Order C1 C2 \<equiv> False"
 
 sublocale labeled_lifting_w_empty_ord_family :
   lifting_with_wf_ordering_family Bot_FL Inf_FL Bot_G entails_G Inf_G Red_Inf_G Red_F_G
     \<G>_F_L \<G>_Inf_L "\<lambda>g. Labeled_Empty_Order"
 proof
   show "po_on Labeled_Empty_Order UNIV"
     unfolding po_on_def by (simp add: transp_onI wfp_on_imp_irreflp_on)
   show "wfp_on Labeled_Empty_Order UNIV"
     unfolding wfp_on_def by simp
 qed
 
 notation "labeled_standard_lifting.entails_\<G>" (infix "\<Turnstile>\<G>L" 50)
 
 (* lem:labeled-consequence *)
 lemma labeled_entailment_lifting: "NL1 \<Turnstile>\<G>L NL2 \<longleftrightarrow> fst ` NL1 \<Turnstile>\<G> fst ` NL2"
   unfolding labeled_standard_lifting.entails_\<G>_def \<G>_F_L_def entails_\<G>_def by auto
 
 lemma red_inf_impl: "\<iota> \<in> labeled_lifting_w_empty_ord_family.Red_Inf_\<G> NL \<Longrightarrow> to_F \<iota> \<in> Red_Inf_\<G> (fst ` NL)"
   unfolding labeled_lifting_w_empty_ord_family.Red_Inf_\<G>_def Red_Inf_\<G>_def \<G>_Inf_L_def \<G>_F_L_def to_F_def
   using Inf_FL_to_Inf_F by auto
 
 (* lem:labeled-saturation *)
 lemma labeled_saturation_lifting:
-  "labeled_lifting_w_empty_ord_family.lifted_calculus_with_red_crit.saturated NL \<Longrightarrow>
-    empty_order_lifting.lifted_calculus_with_red_crit.saturated (fst ` NL)"
-  unfolding labeled_lifting_w_empty_ord_family.lifted_calculus_with_red_crit.saturated_def
-    empty_order_lifting.lifted_calculus_with_red_crit.saturated_def
-    labeled_standard_lifting.Non_ground.Inf_from_def Non_ground.Inf_from_def
+  "labeled_lifting_w_empty_ord_family.saturated NL \<Longrightarrow> empty_order_lifting.saturated (fst ` NL)"
+  unfolding labeled_lifting_w_empty_ord_family.saturated_def empty_order_lifting.saturated_def
+    labeled_standard_lifting.Inf_from_def Inf_from_def
 proof clarify
   fix \<iota>
   assume
     subs_Red_Inf: "{\<iota> \<in> Inf_FL. set (prems_of \<iota>) \<subseteq> NL} \<subseteq> labeled_lifting_w_empty_ord_family.Red_Inf_\<G> NL" and
     i_in: "\<iota> \<in> Inf_F" and
     i_prems: "set (prems_of \<iota>) \<subseteq> fst ` NL"
   define Lli where "Lli i = (SOME x. ((prems_of \<iota>)!i,x) \<in> NL)" for i
   have [simp]:"((prems_of \<iota>)!i,Lli i) \<in> NL" if "i < length (prems_of \<iota>)" for i
     using that i_prems unfolding Lli_def by (metis nth_mem someI_ex DomainE Domain_fst subset_eq)
   define Ll where "Ll = map Lli [0..<length (prems_of \<iota>)]"
   have Ll_length: "length Ll = length (prems_of \<iota>)" unfolding Ll_def by auto
   have subs_NL: "set (zip (prems_of \<iota>) Ll) \<subseteq> NL" unfolding Ll_def by (auto simp:in_set_zip)
   obtain L0 where L0: "Infer (zip (prems_of \<iota>) Ll) (concl_of \<iota>, L0) \<in> Inf_FL"
     using Inf_F_to_Inf_FL[OF i_in Ll_length] ..
   define \<iota>_FL where "\<iota>_FL = Infer (zip (prems_of \<iota>) Ll) (concl_of \<iota>, L0)"
   then have "set (prems_of \<iota>_FL) \<subseteq> NL" using subs_NL by simp
   then have "\<iota>_FL \<in> {\<iota> \<in> Inf_FL. set (prems_of \<iota>) \<subseteq> NL}" unfolding \<iota>_FL_def using L0 by blast
   then have "\<iota>_FL \<in> labeled_lifting_w_empty_ord_family.Red_Inf_\<G> NL" using subs_Red_Inf by fast
   moreover have "\<iota> = to_F \<iota>_FL" unfolding to_F_def \<iota>_FL_def using Ll_length by (cases \<iota>) auto
   ultimately show "\<iota> \<in> Red_Inf_\<G> (fst ` NL)" by (auto intro:red_inf_impl)
 qed
 
 (* lem:labeled-static-ref-compl *)
 lemma stat_ref_comp_to_labeled_sta_ref_comp: "static_refutational_complete_calculus Bot_F Inf_F (\<Turnstile>\<G>) Red_Inf_\<G> Red_F_\<G> \<Longrightarrow>
   static_refutational_complete_calculus Bot_FL Inf_FL (\<Turnstile>\<G>L)
     labeled_lifting_w_empty_ord_family.Red_Inf_\<G> labeled_lifting_w_empty_ord_family.Red_F_\<G>"
   unfolding static_refutational_complete_calculus_def
 proof (rule conjI impI; clarify)
   interpret calculus_with_red_crit Bot_FL Inf_FL labeled_standard_lifting.entails_\<G>
     labeled_lifting_w_empty_ord_family.Red_Inf_\<G> labeled_lifting_w_empty_ord_family.Red_F_\<G>
-    by (simp add:
-      labeled_lifting_w_empty_ord_family.lifted_calculus_with_red_crit.calculus_with_red_crit_axioms)
+    by (simp add: labeled_lifting_w_empty_ord_family.calculus_with_red_crit_axioms)
   show "calculus_with_red_crit Bot_FL Inf_FL (\<Turnstile>\<G>L) labeled_lifting_w_empty_ord_family.Red_Inf_\<G>
     labeled_lifting_w_empty_ord_family.Red_F_\<G>"
     by standard
 next
   assume
     calc: "calculus_with_red_crit Bot_F Inf_F (\<Turnstile>\<G>) Red_Inf_\<G> Red_F_\<G>" and
     static: "static_refutational_complete_calculus_axioms Bot_F Inf_F (\<Turnstile>\<G>) Red_Inf_\<G>"
   show "static_refutational_complete_calculus_axioms Bot_FL Inf_FL (\<Turnstile>\<G>L)
     labeled_lifting_w_empty_ord_family.Red_Inf_\<G>"
     unfolding static_refutational_complete_calculus_axioms_def
   proof (intro conjI impI allI)
     fix Bl :: \<open>'f \<times> 'l\<close> and Nl :: \<open>('f \<times> 'l) set\<close>
     assume
       Bl_in: \<open>Bl \<in> Bot_FL\<close> and
-      Nl_sat: \<open>labeled_lifting_w_empty_ord_family.lifted_calculus_with_red_crit.saturated Nl\<close> and
+      Nl_sat: \<open>labeled_lifting_w_empty_ord_family.saturated Nl\<close> and
       Nl_entails_Bl: \<open>Nl \<Turnstile>\<G>L {Bl}\<close>
-    have static_axioms: "B \<in> Bot_F \<longrightarrow> empty_order_lifting.lifted_calculus_with_red_crit.saturated N \<longrightarrow>
-      N \<Turnstile>\<G> {B} \<longrightarrow> (\<exists>B'\<in>Bot_F. B' \<in> N)" for B N
+    have static_axioms: "B \<in> Bot_F \<longrightarrow> empty_order_lifting.saturated N \<longrightarrow> N \<Turnstile>\<G> {B} \<longrightarrow>
+      (\<exists>B'\<in>Bot_F. B' \<in> N)" for B N
       using static[unfolded static_refutational_complete_calculus_axioms_def] by fast
     define B where "B = fst Bl"
     have B_in: "B \<in> Bot_F" using Bl_in Bot_FL_def B_def SigmaE by force
     define N where "N = fst ` Nl"
-    have N_sat: "empty_order_lifting.lifted_calculus_with_red_crit.saturated N"
+    have N_sat: "empty_order_lifting.saturated N"
       using N_def Nl_sat labeled_saturation_lifting by blast
     have N_entails_B: "N \<Turnstile>\<G> {B}"
       using Nl_entails_Bl unfolding labeled_entailment_lifting N_def B_def by force
     have "\<exists>B' \<in> Bot_F. B' \<in> N" using B_in N_sat N_entails_B static_axioms[of B N] by blast
     then obtain B' where in_Bot: "B' \<in> Bot_F" and in_N: "B' \<in> N" by force
     then have "B' \<in> fst ` Bot_FL" unfolding Bot_FL_def by fastforce
     obtain Bl' where in_Nl: "Bl' \<in> Nl" and fst_Bl': "fst Bl' = B'"
       using in_N unfolding N_def by blast
     have "Bl' \<in> Bot_FL" unfolding Bot_FL_def using fst_Bl' in_Bot vimage_fst by fastforce
     then show \<open>\<exists>Bl'\<in>Bot_FL. Bl' \<in> Nl\<close> using in_Nl by blast
   qed
 qed
 
 end
 
 subsection \<open>Labeled Lifting with a Family of Redundancy Criteria\<close>
 
 locale labeled_lifting_with_red_crit_family = no_labels: standard_lifting_with_red_crit_family Inf_F
   Bot_G Q Inf_G_q entails_q Red_Inf_q Red_F_q Bot_F \<G>_F_q \<G>_Inf_q "\<lambda>g. Empty_Order"
   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 :: "'q \<Rightarrow> 'g inference set" and
     Red_Inf_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>_Inf_q :: "'q \<Rightarrow> 'f inference \<Rightarrow> 'g inference set option"
   + fixes
     Inf_FL :: \<open>('f \<times> 'l) inference set\<close>
   assumes
     Inf_F_to_Inf_FL:
       \<open>\<iota>\<^sub>F \<in> Inf_F \<Longrightarrow> length (Ll :: 'l list) = length (prems_of \<iota>\<^sub>F) \<Longrightarrow>
        \<exists>L0. Infer (zip (prems_of \<iota>\<^sub>F) Ll) (concl_of \<iota>\<^sub>F, L0) \<in> Inf_FL\<close> and
     Inf_FL_to_Inf_F: \<open>\<iota>\<^sub>F\<^sub>L \<in> Inf_FL \<Longrightarrow> Infer (map fst (prems_of \<iota>\<^sub>F\<^sub>L)) (fst (concl_of \<iota>\<^sub>F\<^sub>L)) \<in> Inf_F\<close>
 begin
 
 definition to_F :: \<open>('f \<times> 'l) inference \<Rightarrow> 'f inference\<close> where
   \<open>to_F \<iota>\<^sub>F\<^sub>L = Infer (map fst (prems_of \<iota>\<^sub>F\<^sub>L)) (fst (concl_of \<iota>\<^sub>F\<^sub>L))\<close>
 
 definition Bot_FL :: \<open>('f \<times> 'l) set\<close> where \<open>Bot_FL = Bot_F \<times> UNIV\<close>
 
 definition \<G>_F_L_q :: \<open>'q \<Rightarrow> ('f \<times> 'l) \<Rightarrow> 'g set\<close> where \<open>\<G>_F_L_q q CL = \<G>_F_q q (fst CL)\<close>
 
 definition \<G>_Inf_L_q :: \<open>'q \<Rightarrow> ('f \<times> 'l) inference \<Rightarrow> 'g inference set option\<close> where
   \<open>\<G>_Inf_L_q q \<iota>\<^sub>F\<^sub>L = \<G>_Inf_q q (to_F \<iota>\<^sub>F\<^sub>L)\<close>
 
 definition \<G>_set_L_q :: "'q \<Rightarrow> ('f \<times> 'l) set \<Rightarrow> 'g set" where
   "\<G>_set_L_q q N = \<Union> (\<G>_F_L_q q ` N)"
 
 definition Red_Inf_\<G>_L_q :: "'q \<Rightarrow> ('f \<times> 'l) set \<Rightarrow> ('f \<times> 'l) inference set" where
   "Red_Inf_\<G>_L_q q N = {\<iota> \<in> Inf_FL. ((\<G>_Inf_L_q q \<iota>) \<noteq> None \<and> the (\<G>_Inf_L_q q \<iota>) \<subseteq> Red_Inf_q q (\<G>_set_L_q q N))
     \<or> ((\<G>_Inf_L_q q \<iota> = None) \<and> \<G>_F_L_q q (concl_of \<iota>) \<subseteq> (\<G>_set_L_q q N \<union> Red_F_q q (\<G>_set_L_q q N)))}"
 
 definition Red_Inf_\<G>_L_Q :: "('f \<times> 'l) set \<Rightarrow> ('f \<times> 'l) inference set" where
   "Red_Inf_\<G>_L_Q N = (\<Inter>q \<in> Q. Red_Inf_\<G>_L_q q N)"
 
 abbreviation Labeled_Empty_Order :: \<open> ('f \<times> 'l) \<Rightarrow> ('f \<times> 'l) \<Rightarrow> bool\<close> where
   "Labeled_Empty_Order C1 C2 \<equiv> False"
 
 definition Red_F_\<G>_empty_L_q :: "'q \<Rightarrow> ('f \<times> 'l) set \<Rightarrow> ('f \<times> 'l) set" where
   "Red_F_\<G>_empty_L_q q N = {C. \<forall>D \<in> \<G>_F_L_q q C. D \<in> Red_F_q q (\<G>_set_L_q q N) \<or>
     (\<exists>E \<in> N. Labeled_Empty_Order E C \<and> D \<in> \<G>_F_L_q q E)}"
 
 definition Red_F_\<G>_empty_L :: "('f \<times> 'l) set \<Rightarrow> ('f \<times> 'l) set" where
   "Red_F_\<G>_empty_L N = (\<Inter>q \<in> Q. Red_F_\<G>_empty_L_q q N)"
 
 definition entails_\<G>_L_q :: "'q \<Rightarrow> ('f \<times> 'l) set \<Rightarrow> ('f \<times> 'l) set \<Rightarrow> bool" where
   "entails_\<G>_L_q q N1 N2 \<longleftrightarrow> entails_q q (\<G>_set_L_q q N1) (\<G>_set_L_q q N2)"
 
 lemma lifting_q:
   assumes "q \<in> Q"
   shows "labeled_lifting_w_wf_ord_family Bot_F Inf_F Bot_G (entails_q q) (Inf_G_q q) (Red_Inf_q q)
     (Red_F_q q) (\<G>_F_q q) (\<G>_Inf_q q) (\<lambda>g. Empty_Order) Inf_FL"
   using assms no_labels.standard_lifting_family Inf_F_to_Inf_FL Inf_FL_to_Inf_F
   by (simp add: labeled_lifting_w_wf_ord_family_axioms_def labeled_lifting_w_wf_ord_family_def)
 
 lemma lifted_q:
   assumes q_in: "q \<in> Q"
   shows "standard_lifting Bot_FL Inf_FL Bot_G (Inf_G_q q) (entails_q q) (Red_Inf_q q) (Red_F_q q)
     (\<G>_F_L_q q) (\<G>_Inf_L_q q)"
 proof -
   interpret q_lifting: labeled_lifting_w_wf_ord_family Bot_F Inf_F Bot_G "entails_q q" "Inf_G_q q"
     "Red_Inf_q q" "Red_F_q q" "\<G>_F_q q" "\<G>_Inf_q q" "\<lambda>g. Empty_Order" Inf_FL
     using lifting_q[OF q_in] .
   have "\<G>_F_L_q q = q_lifting.\<G>_F_L"
     unfolding \<G>_F_L_q_def q_lifting.\<G>_F_L_def by simp
   moreover have "\<G>_Inf_L_q q = q_lifting.\<G>_Inf_L"
     unfolding \<G>_Inf_L_q_def q_lifting.\<G>_Inf_L_def to_F_def q_lifting.to_F_def by simp
   moreover have "Bot_FL = q_lifting.Bot_FL"
     unfolding Bot_FL_def q_lifting.Bot_FL_def by simp
   ultimately show ?thesis
     using q_lifting.labeled_standard_lifting.standard_lifting_axioms by simp
 qed
 
 lemma ord_fam_lifted_q:
   assumes q_in: "q \<in> Q"
   shows "lifting_with_wf_ordering_family Bot_FL Inf_FL Bot_G (entails_q q) (Inf_G_q q) (Red_Inf_q q)
     (Red_F_q q) (\<G>_F_L_q q) (\<G>_Inf_L_q q) (\<lambda>g. Empty_Order)"
 proof -
   interpret standard_q_lifting: standard_lifting Bot_FL Inf_FL Bot_G "Inf_G_q q" "entails_q q"
     "Red_Inf_q q" "Red_F_q q" "\<G>_F_L_q q" "\<G>_Inf_L_q q"
     using lifted_q[OF q_in] .
   have "minimal_element Labeled_Empty_Order UNIV"
     by (simp add: minimal_element.intro po_on_def transp_onI wfp_on_imp_irreflp_on)
   then show ?thesis
     using standard_q_lifting.standard_lifting_axioms
     by (simp add: lifting_with_wf_ordering_family_axioms.intro lifting_with_wf_ordering_family_def)
 qed
 
 lemma all_lifted_red_crit:
   assumes q_in: "q \<in> Q"
   shows "calculus_with_red_crit Bot_FL Inf_FL (entails_\<G>_L_q q) (Red_Inf_\<G>_L_q q)
     (Red_F_\<G>_empty_L_q q)"
 proof -
   interpret ord_q_lifting: lifting_with_wf_ordering_family Bot_FL Inf_FL Bot_G "entails_q q"
     "Inf_G_q q" "Red_Inf_q q" "Red_F_q q" "\<G>_F_L_q q" "\<G>_Inf_L_q q" "\<lambda>g. Empty_Order"
     using ord_fam_lifted_q[OF q_in] .
   have "entails_\<G>_L_q q = ord_q_lifting.entails_\<G>"
     unfolding entails_\<G>_L_q_def \<G>_set_L_q_def ord_q_lifting.entails_\<G>_def by simp
   moreover have "Red_Inf_\<G>_L_q q = ord_q_lifting.Red_Inf_\<G>"
     unfolding Red_Inf_\<G>_L_q_def ord_q_lifting.Red_Inf_\<G>_def \<G>_set_L_q_def by simp
   moreover have "Red_F_\<G>_empty_L_q q = ord_q_lifting.Red_F_\<G>"
     unfolding Red_F_\<G>_empty_L_q_def ord_q_lifting.Red_F_\<G>_def \<G>_set_L_q_def by simp
   ultimately show ?thesis
-    using ord_q_lifting.lifted_calculus_with_red_crit.calculus_with_red_crit_axioms by argo
+    using ord_q_lifting.calculus_with_red_crit_axioms by argo
 qed
 
 lemma all_lifted_cons_rel:
   assumes q_in: "q \<in> Q"
   shows "consequence_relation Bot_FL (entails_\<G>_L_q q)"
 proof -
   interpret q_red_crit: calculus_with_red_crit Bot_FL Inf_FL "entails_\<G>_L_q q" "Red_Inf_\<G>_L_q q"
     "Red_F_\<G>_empty_L_q q"
     using all_lifted_red_crit[OF q_in] .
   show ?thesis
     using q_red_crit.consequence_relation_axioms .
 qed
 
 sublocale labeled_cons_rel_family: consequence_relation_family Bot_FL Q entails_\<G>_L_q
   using all_lifted_cons_rel no_labels.lifted_calc_w_red_crit_family.bot_not_empty
   by (simp add: Bot_FL_def consequence_relation_family_def
       no_labels.lifted_calc_w_red_crit_family.Q_nonempty)
 
 sublocale with_labels: calculus_with_red_crit_family Bot_FL Inf_FL Q entails_\<G>_L_q Red_Inf_\<G>_L_q
   Red_F_\<G>_empty_L_q
   using calculus_with_red_crit_family.intro[OF labeled_cons_rel_family.consequence_relation_family_axioms]
     all_lifted_cons_rel
   by (meson calculus_with_red_crit_family_axioms.intro
       labeled_lifting_with_red_crit_family.all_lifted_red_crit
       labeled_lifting_with_red_crit_family_axioms no_labels.lifted_calc_w_red_crit_family.Q_nonempty)
 
 notation no_labels.entails_\<G>_Q (infix "\<Turnstile>\<inter>\<G>" 50)
 
 abbreviation entails_\<G>_L_Q :: "('f \<times> 'l) set \<Rightarrow> ('f \<times> 'l) set \<Rightarrow> bool" (infix "\<Turnstile>\<inter>\<G>L" 50) where
   "(\<Turnstile>\<inter>\<G>L) \<equiv> labeled_cons_rel_family.entails_Q"
 
 lemmas entails_\<G>_L_Q_def = labeled_cons_rel_family.entails_Q_def
 
 (* lem:labeled-consequence-intersection *)
 lemma labeled_entailment_lifting: "NL1 \<Turnstile>\<inter>\<G>L NL2 \<longleftrightarrow> fst ` NL1 \<Turnstile>\<inter>\<G> fst ` NL2"
   unfolding no_labels.entails_\<G>_Q_def no_labels.entails_\<G>_q_def no_labels.\<G>_set_q_def
     entails_\<G>_L_Q_def entails_\<G>_L_q_def \<G>_set_L_q_def \<G>_F_L_q_def
   by force
 
 lemma red_inf_impl: "\<iota> \<in> with_labels.Red_Inf_Q NL \<Longrightarrow>
   to_F \<iota> \<in> no_labels.empty_ord_lifted_calc_w_red_crit_family.Red_Inf_Q (fst ` NL)"
   unfolding no_labels.empty_ord_lifted_calc_w_red_crit_family.Red_Inf_Q_def with_labels.Red_Inf_Q_def
 proof clarify
   fix X Xa q
   assume
     q_in: "q \<in> Q" and
     i_in_inter: "\<iota> \<in> (\<Inter>q \<in> Q. Red_Inf_\<G>_L_q q NL)"
   have i_in_q: "\<iota> \<in> Red_Inf_\<G>_L_q q NL" using q_in i_in_inter image_eqI by blast
   then have i_in: "\<iota> \<in> Inf_FL" unfolding Red_Inf_\<G>_L_q_def by blast
   have to_F_in: "to_F \<iota> \<in> Inf_F" unfolding to_F_def using Inf_FL_to_Inf_F[OF i_in] .
   have rephrase1: "(\<Union>CL\<in>NL. \<G>_F_q q (fst CL)) = (\<Union> (\<G>_F_q q ` fst ` NL))" by blast
   have rephrase2: "fst (concl_of \<iota>) = concl_of (to_F \<iota>)"
     unfolding concl_of_def to_F_def by simp
   have subs_red: "(\<G>_Inf_L_q q \<iota> \<noteq> None \<and> the (\<G>_Inf_L_q q \<iota>) \<subseteq> Red_Inf_q q (\<G>_set_L_q q NL))
     \<or> (\<G>_Inf_L_q q \<iota> = None \<and> \<G>_F_L_q q (concl_of \<iota>) \<subseteq> \<G>_set_L_q q NL \<union> Red_F_q q (\<G>_set_L_q q NL))"
     using i_in_q unfolding Red_Inf_\<G>_L_q_def by blast
   then have to_F_subs_red: "(\<G>_Inf_q q (to_F \<iota>) \<noteq> None \<and>
       the (\<G>_Inf_q q (to_F \<iota>)) \<subseteq> Red_Inf_q q (no_labels.\<G>_set_q q (fst ` NL)))
     \<or> (\<G>_Inf_q q (to_F \<iota>) = None \<and>
       \<G>_F_q q (concl_of (to_F \<iota>)) \<subseteq> (no_labels.\<G>_set_q q (fst ` NL) \<union> Red_F_q q (no_labels.\<G>_set_q q (fst ` NL))))"
     unfolding \<G>_Inf_L_q_def \<G>_set_L_q_def no_labels.\<G>_set_q_def \<G>_F_L_q_def
     using rephrase1 rephrase2 by metis
   then show "to_F \<iota> \<in> no_labels.Red_Inf_\<G>_q q (fst ` NL)"
     using to_F_in unfolding no_labels.Red_Inf_\<G>_q_def by simp
 qed
 
 (* lem:labeled-saturation-intersection *)
-lemma labeled_family_saturation_lifting: "with_labels.inter_red_crit_calculus.saturated NL \<Longrightarrow>
-  no_labels.lifted_calc_w_red_crit_family.inter_red_crit_calculus.saturated (fst ` NL)"
-  unfolding with_labels.inter_red_crit_calculus.saturated_def
-    no_labels.lifted_calc_w_red_crit_family.inter_red_crit_calculus.saturated_def
-    with_labels.Inf_from_def no_labels.Non_ground.Inf_from_def
+lemma labeled_family_saturation_lifting: "with_labels.saturated NL \<Longrightarrow>
+  no_labels.lifted_calc_w_red_crit_family.saturated (fst ` NL)"
+  unfolding with_labels.saturated_def no_labels.lifted_calc_w_red_crit_family.saturated_def
+    with_labels.Inf_from_def no_labels.Inf_from_def
 proof clarify
   fix \<iota>F
   assume
     labeled_sat: "{\<iota> \<in> Inf_FL. set (prems_of \<iota>) \<subseteq> NL} \<subseteq> with_labels.Red_Inf_Q NL" and
     iF_in: "\<iota>F \<in> Inf_F" and
     iF_prems: "set (prems_of \<iota>F) \<subseteq> fst ` NL"
   define Lli where "Lli i = (SOME x. ((prems_of \<iota>F)!i,x) \<in> NL)" for i
   have [simp]:"((prems_of \<iota>F)!i,Lli i) \<in> NL" if "i < length (prems_of \<iota>F)" for i
     using that iF_prems nth_mem someI_ex unfolding Lli_def by (metis DomainE Domain_fst subset_eq)
   define Ll where "Ll = map Lli [0..<length (prems_of \<iota>F)]"
   have Ll_length: "length Ll = length (prems_of \<iota>F)" unfolding Ll_def by auto
   have subs_NL: "set (zip (prems_of \<iota>F) Ll) \<subseteq> NL" unfolding Ll_def by (auto simp:in_set_zip)
   obtain L0 where L0: "Infer (zip (prems_of \<iota>F) Ll) (concl_of \<iota>F, L0) \<in> Inf_FL"
     using Inf_F_to_Inf_FL[OF iF_in Ll_length] ..
   define \<iota>FL where "\<iota>FL = Infer (zip (prems_of \<iota>F) Ll) (concl_of \<iota>F, L0)"
   then have "set (prems_of \<iota>FL) \<subseteq> NL" using subs_NL by simp
   then have "\<iota>FL \<in> {\<iota> \<in> Inf_FL. set (prems_of \<iota>) \<subseteq> NL}" unfolding \<iota>FL_def using L0 by blast
   then have "\<iota>FL \<in> with_labels.Red_Inf_Q NL" using labeled_sat by fast
   moreover have "\<iota>F = to_F \<iota>FL" unfolding to_F_def \<iota>FL_def using Ll_length by (cases \<iota>F) auto
   ultimately show "\<iota>F \<in> no_labels.empty_ord_lifted_calc_w_red_crit_family.Red_Inf_Q (fst ` NL)"
     by (auto intro:red_inf_impl)
 qed
 
 (* thm:labeled-static-ref-compl-intersection *)
 theorem labeled_static_ref: "static_refutational_complete_calculus Bot_F Inf_F (\<Turnstile>\<inter>\<G>)
-  no_labels.empty_ord_lifted_calc_w_red_crit_family.Red_Inf_Q
-  no_labels.empty_ord_lifted_calc_w_red_crit_family.Red_F_Q
-  \<Longrightarrow> static_refutational_complete_calculus Bot_FL Inf_FL (\<Turnstile>\<inter>\<G>L) with_labels.Red_Inf_Q with_labels.Red_F_Q"
+    no_labels.empty_ord_lifted_calc_w_red_crit_family.Red_Inf_Q
+    no_labels.empty_ord_lifted_calc_w_red_crit_family.Red_F_Q \<Longrightarrow>
+  static_refutational_complete_calculus Bot_FL Inf_FL (\<Turnstile>\<inter>\<G>L) with_labels.Red_Inf_Q
+    with_labels.Red_F_Q"
   unfolding static_refutational_complete_calculus_def
 proof (rule conjI impI; clarify)
   show "calculus_with_red_crit Bot_FL Inf_FL (\<Turnstile>\<inter>\<G>L) with_labels.Red_Inf_Q with_labels.Red_F_Q"
     by unfold_locales
 next
   assume
     calc: "calculus_with_red_crit Bot_F Inf_F (\<Turnstile>\<inter>\<G>)
       no_labels.empty_ord_lifted_calc_w_red_crit_family.Red_Inf_Q
       no_labels.empty_ord_lifted_calc_w_red_crit_family.Red_F_Q" and
     static: "static_refutational_complete_calculus_axioms Bot_F Inf_F (\<Turnstile>\<inter>\<G>)
       no_labels.empty_ord_lifted_calc_w_red_crit_family.Red_Inf_Q"
   show "static_refutational_complete_calculus_axioms Bot_FL Inf_FL (\<Turnstile>\<inter>\<G>L) with_labels.Red_Inf_Q"
     unfolding static_refutational_complete_calculus_axioms_def
   proof (intro conjI impI allI)
     fix Bl :: \<open>'f \<times> 'l\<close> and Nl :: \<open>('f \<times> 'l) set\<close>
     assume
       Bl_in: \<open>Bl \<in> Bot_FL\<close> and
-      Nl_sat: \<open>with_labels.inter_red_crit_calculus.saturated Nl\<close> and
+      Nl_sat: \<open>with_labels.saturated Nl\<close> and
       Nl_entails_Bl: \<open>Nl \<Turnstile>\<inter>\<G>L {Bl}\<close>
-    have static_axioms: "B \<in> Bot_F \<longrightarrow>
-      no_labels.lifted_calc_w_red_crit_family.inter_red_crit_calculus.saturated N \<longrightarrow>
+    have static_axioms: "B \<in> Bot_F \<longrightarrow> no_labels.lifted_calc_w_red_crit_family.saturated N \<longrightarrow>
       N \<Turnstile>\<inter>\<G> {B} \<longrightarrow> (\<exists>B'\<in>Bot_F. B' \<in> N)" for B N
       using static[unfolded static_refutational_complete_calculus_axioms_def] by fast
     define B where "B = fst Bl"
     have B_in: "B \<in> Bot_F" using Bl_in Bot_FL_def B_def SigmaE by force
     define N where "N = fst ` Nl"
-    have N_sat: "no_labels.lifted_calc_w_red_crit_family.inter_red_crit_calculus.saturated N"
+    have N_sat: "no_labels.lifted_calc_w_red_crit_family.saturated N"
       using N_def Nl_sat labeled_family_saturation_lifting by blast
     have N_entails_B: "N \<Turnstile>\<inter>\<G> {B}"
       using Nl_entails_Bl unfolding labeled_entailment_lifting N_def B_def by force
     have "\<exists>B' \<in> Bot_F. B' \<in> N" using B_in N_sat N_entails_B static_axioms[of B N] by blast
     then obtain B' where in_Bot: "B' \<in> Bot_F" and in_N: "B' \<in> N" by force
     then have "B' \<in> fst ` Bot_FL" unfolding Bot_FL_def by fastforce
     obtain Bl' where in_Nl: "Bl' \<in> Nl" and fst_Bl': "fst Bl' = B'"
       using in_N unfolding N_def by blast
     have "Bl' \<in> Bot_FL" unfolding Bot_FL_def using fst_Bl' in_Bot vimage_fst by fastforce
     then show \<open>\<exists>Bl'\<in>Bot_FL. Bl' \<in> Nl\<close> using in_Nl by blast
   qed
 qed
 
 end
 
 end
diff --git a/thys/Saturation_Framework/Lifting_to_Non_Ground_Calculi.thy b/thys/Saturation_Framework/Lifting_to_Non_Ground_Calculi.thy
--- a/thys/Saturation_Framework/Lifting_to_Non_Ground_Calculi.thy
+++ b/thys/Saturation_Framework/Lifting_to_Non_Ground_Calculi.thy
@@ -1,866 +1,861 @@
 (*  Title:       Lifting to Non-Ground Calculi of the Saturation Framework
  *  Author:      Sophie Tourret <stourret at mpi-inf.mpg.de>, 2018-2020 *)
 
 section \<open>Lifting to Non-ground Calculi\<close>
 
 text \<open>The section 3.1 to 3.3 of the report are covered by the current section.
   Various forms of lifting are proven correct. These allow to obtain the dynamic
   refutational completeness of a non-ground calculus from the static refutational
   completeness of its ground counterpart.\<close>
 
 theory Lifting_to_Non_Ground_Calculi
   imports
     Calculi
     Well_Quasi_Orders.Minimal_Elements
 begin
 
 subsection \<open>Standard Lifting\<close>
 
-locale standard_lifting = Non_ground: inference_system Inf_F +
-  Ground: calculus_with_red_crit Bot_G Inf_G entails_G Red_Inf_G Red_F_G
+locale standard_lifting = inference_system Inf_F +
+  ground: calculus_with_red_crit Bot_G Inf_G entails_G Red_Inf_G Red_F_G
   for
     Bot_F :: \<open>'f set\<close> and
     Inf_F :: \<open>'f inference set\<close> and
     Bot_G :: \<open>'g set\<close> and
     Inf_G ::  \<open>'g inference set\<close> and
     entails_G ::  \<open>'g set  \<Rightarrow> 'g set  \<Rightarrow> bool\<close> (infix "\<Turnstile>G" 50) and
     Red_Inf_G :: \<open>'g set \<Rightarrow> 'g inference set\<close> and
     Red_F_G :: \<open>'g set \<Rightarrow> 'g set\<close>
   + fixes
     \<G>_F :: \<open>'f \<Rightarrow> 'g set\<close> and
     \<G>_Inf :: \<open>'f inference \<Rightarrow> 'g inference set option\<close>
   assumes
     Bot_F_not_empty: "Bot_F \<noteq> {}" and
     Bot_map_not_empty: \<open>B \<in> Bot_F \<Longrightarrow> \<G>_F B \<noteq> {}\<close> and
     Bot_map: \<open>B \<in> Bot_F \<Longrightarrow> \<G>_F B \<subseteq> Bot_G\<close> and
     Bot_cond: \<open>\<G>_F C \<inter> Bot_G \<noteq> {} \<longrightarrow> C \<in> Bot_F\<close> and
     inf_map: \<open>\<iota> \<in> Inf_F \<Longrightarrow> \<G>_Inf \<iota> \<noteq> None \<Longrightarrow> the (\<G>_Inf \<iota>) \<subseteq> Red_Inf_G (\<G>_F (concl_of \<iota>))\<close>
 begin
 
 abbreviation \<G>_set :: \<open>'f set \<Rightarrow> 'g set\<close> where
   \<open>\<G>_set N \<equiv> \<Union> (\<G>_F ` N)\<close>
 
 lemma \<G>_subset: \<open>N1 \<subseteq> N2 \<Longrightarrow> \<G>_set N1 \<subseteq> \<G>_set N2\<close> by auto
 
 definition entails_\<G>  :: \<open>'f set \<Rightarrow> 'f set \<Rightarrow> bool\<close> (infix "\<Turnstile>\<G>" 50) where
   \<open>N1 \<Turnstile>\<G> N2 \<longleftrightarrow> \<G>_set N1 \<Turnstile>G \<G>_set N2\<close>
 
 lemma subs_Bot_G_entails:
   assumes
     not_empty: \<open>sB \<noteq> {}\<close> and
     in_bot: \<open>sB \<subseteq> Bot_G\<close>
   shows \<open>sB \<Turnstile>G N\<close>
 proof -
   have \<open>\<exists>B. B \<in> sB\<close> using not_empty by auto
   then obtain B where B_in: \<open>B \<in> sB\<close> by auto
-  then have r_trans: \<open>{B} \<Turnstile>G N\<close> using Ground.bot_entails_all in_bot by auto
-  have l_trans: \<open>sB \<Turnstile>G {B}\<close> using B_in Ground.subset_entailed by auto
-  then show ?thesis using r_trans Ground.entails_trans[of sB "{B}"] by auto
+  then have r_trans: \<open>{B} \<Turnstile>G N\<close> using ground.bot_entails_all in_bot by auto
+  have l_trans: \<open>sB \<Turnstile>G {B}\<close> using B_in ground.subset_entailed by auto
+  then show ?thesis using r_trans ground.entails_trans[of sB "{B}"] by auto
 qed
 
 (* lem:derived-consequence-relation *)
 sublocale lifted_consequence_relation: consequence_relation
   where Bot=Bot_F and entails=entails_\<G>
 proof
   show "Bot_F \<noteq> {}" using Bot_F_not_empty .
 next
   show \<open>B\<in>Bot_F \<Longrightarrow> {B} \<Turnstile>\<G> N\<close> for B N
   proof -
     assume \<open>B \<in> Bot_F\<close>
     then show \<open>{B} \<Turnstile>\<G> N\<close>
-      using Bot_map Ground.bot_entails_all[of _ "\<G>_set N"] subs_Bot_G_entails Bot_map_not_empty
+      using Bot_map ground.bot_entails_all[of _ "\<G>_set N"] subs_Bot_G_entails Bot_map_not_empty
       unfolding entails_\<G>_def
       by auto
   qed
 next
   fix N1 N2 :: \<open>'f set\<close>
   assume
     \<open>N2 \<subseteq> N1\<close>
-  then show \<open>N1 \<Turnstile>\<G> N2\<close> using entails_\<G>_def \<G>_subset Ground.subset_entailed by auto
+  then show \<open>N1 \<Turnstile>\<G> N2\<close> using entails_\<G>_def \<G>_subset ground.subset_entailed by auto
 next
   fix N1 N2
   assume
     N1_entails_C: \<open>\<forall>C \<in> N2. N1 \<Turnstile>\<G> {C}\<close>
-  show \<open>N1 \<Turnstile>\<G> N2\<close> using Ground.all_formulas_entailed N1_entails_C entails_\<G>_def
-    by (smt UN_E UN_I Ground.entail_set_all_formulas singletonI)
+  show \<open>N1 \<Turnstile>\<G> N2\<close> using ground.all_formulas_entailed N1_entails_C entails_\<G>_def
+    by (smt UN_E UN_I ground.entail_set_all_formulas singletonI)
 next
   fix N1 N2 N3
   assume
     \<open>N1 \<Turnstile>\<G> N2\<close> and \<open>N2 \<Turnstile>\<G> N3\<close>
-  then show \<open>N1 \<Turnstile>\<G> N3\<close> using entails_\<G>_def Ground.entails_trans by blast
+  then show \<open>N1 \<Turnstile>\<G> N3\<close> using entails_\<G>_def ground.entails_trans by blast
 qed
 
 end
 
 subsection \<open>Strong Standard Lifting\<close>
 
 (* rmk:strong-standard-lifting *)
-locale strong_standard_lifting = Non_ground: inference_system Inf_F +
-  Ground: calculus_with_red_crit Bot_G Inf_G entails_G Red_Inf_G Red_F_G
+locale strong_standard_lifting = inference_system Inf_F +
+  ground: calculus_with_red_crit Bot_G Inf_G entails_G Red_Inf_G Red_F_G
   for
     Bot_F :: \<open>'f set\<close> and
     Inf_F :: \<open>'f inference set\<close> and
     Bot_G :: \<open>'g set\<close> and
     Inf_G ::  \<open>'g inference set\<close> and
     entails_G ::  \<open>'g set  \<Rightarrow> 'g set  \<Rightarrow> bool\<close> (infix "\<Turnstile>G" 50) and
     Red_Inf_G :: \<open>'g set \<Rightarrow> 'g inference set\<close> and
     Red_F_G :: \<open>'g set \<Rightarrow> 'g set\<close>
   + fixes
     \<G>_F :: \<open>'f \<Rightarrow> 'g set\<close> and
     \<G>_Inf :: \<open>'f inference \<Rightarrow> 'g inference set option\<close>
   assumes
     Bot_F_not_empty: "Bot_F \<noteq> {}" and
     Bot_map_not_empty: \<open>B \<in> Bot_F \<Longrightarrow> \<G>_F B \<noteq> {}\<close> and
     Bot_map: \<open>B \<in> Bot_F \<Longrightarrow> \<G>_F B \<subseteq> Bot_G\<close> and
     Bot_cond: \<open>\<G>_F C \<inter> Bot_G \<noteq> {} \<longrightarrow> C \<in> Bot_F\<close> and
     strong_inf_map: \<open>\<iota> \<in> Inf_F \<Longrightarrow> \<G>_Inf \<iota> \<noteq> None \<Longrightarrow> concl_of ` (the (\<G>_Inf \<iota>)) \<subseteq> (\<G>_F (concl_of \<iota>))\<close> and
     inf_map_in_Inf: \<open>\<iota> \<in> Inf_F \<Longrightarrow> \<G>_Inf \<iota> \<noteq> None \<Longrightarrow> the (\<G>_Inf \<iota>) \<subseteq> Inf_G\<close>
 begin
 
 sublocale standard_lifting
 proof
   show "Bot_F \<noteq> {}" using Bot_F_not_empty .
 next
   fix B
   assume b_in: "B \<in> Bot_F"
   show "\<G>_F B \<noteq> {}" using Bot_map_not_empty[OF b_in] .
 next
   fix B
   assume b_in: "B \<in> Bot_F"
   show "\<G>_F B \<subseteq> Bot_G" using Bot_map[OF b_in] .
 next
   show "\<And>C. \<G>_F C \<inter> Bot_G \<noteq> {} \<longrightarrow> C \<in> Bot_F" using Bot_cond .
 next
   fix \<iota>
   assume i_in: "\<iota> \<in> Inf_F" and
     some_g: "\<G>_Inf \<iota> \<noteq> None"
   show "the (\<G>_Inf \<iota>) \<subseteq> Red_Inf_G (\<G>_F (concl_of \<iota>))"
   proof
     fix \<iota>G
     assume ig_in1: "\<iota>G \<in> the (\<G>_Inf \<iota>)"
     then have ig_in2: "\<iota>G \<in> Inf_G" using inf_map_in_Inf[OF i_in some_g] by blast
     show "\<iota>G \<in> Red_Inf_G (\<G>_F (concl_of \<iota>))"
-      using strong_inf_map[OF i_in some_g] Ground.Red_Inf_of_Inf_to_N[OF ig_in2]
+      using strong_inf_map[OF i_in some_g] ground.Red_Inf_of_Inf_to_N[OF ig_in2]
         ig_in1 by blast
   qed
 qed
 
 end
 
 subsection \<open>Lifting with a Family of Well-founded Orderings\<close>
 
 locale lifting_with_wf_ordering_family =
   standard_lifting Bot_F Inf_F Bot_G Inf_G entails_G Red_Inf_G Red_F_G \<G>_F \<G>_Inf
   for
     Bot_F :: \<open>'f set\<close> and
     Inf_F :: \<open>'f inference set\<close> and
     Bot_G :: \<open>'g set\<close> and
     entails_G :: \<open>'g set \<Rightarrow> 'g set \<Rightarrow> bool\<close> (infix "\<Turnstile>G" 50) and
     Inf_G :: \<open>'g inference set\<close> and
     Red_Inf_G :: \<open>'g set \<Rightarrow> 'g inference set\<close> and
     Red_F_G :: \<open>'g set \<Rightarrow> 'g set\<close> and
     \<G>_F :: "'f \<Rightarrow> 'g set" and
     \<G>_Inf :: "'f inference \<Rightarrow> 'g inference set option"
   + fixes
     Prec_F_g :: \<open>'g \<Rightarrow> 'f \<Rightarrow> 'f \<Rightarrow> bool\<close>
   assumes
     all_wf: "minimal_element (Prec_F_g g) UNIV"
 begin
 
 definition Red_Inf_\<G> :: "'f set \<Rightarrow> 'f inference set" where
   \<open>Red_Inf_\<G> N = {\<iota> \<in> Inf_F. (\<G>_Inf \<iota> \<noteq> None \<and> the (\<G>_Inf \<iota>) \<subseteq> Red_Inf_G (\<G>_set N))
     \<or> (\<G>_Inf \<iota> = None \<and> \<G>_F (concl_of \<iota>) \<subseteq> (\<G>_set N \<union> Red_F_G (\<G>_set N)))}\<close>
 
 definition Red_F_\<G> :: "'f set \<Rightarrow> 'f set" where
   \<open>Red_F_\<G> N = {C. \<forall>D \<in> \<G>_F C. D \<in> Red_F_G (\<G>_set N) \<or> (\<exists>E \<in> N. Prec_F_g D E C \<and> D \<in> \<G>_F E)}\<close>
 
 lemma Prec_trans:
   assumes
     \<open>Prec_F_g D A B\<close> and
     \<open>Prec_F_g D B C\<close>
   shows
     \<open>Prec_F_g D A C\<close>
   using minimal_element.po assms unfolding po_on_def transp_on_def by (smt UNIV_I all_wf)
 
 lemma prop_nested_in_set: "D \<in> P C \<Longrightarrow> C \<in> {C. \<forall>D \<in> P C. A D \<or> B C D} \<Longrightarrow> A D \<or> B C D"
   by blast
 
 (* lem:wolog-C'-nonredundant *)
 lemma Red_F_\<G>_equiv_def:
   \<open>Red_F_\<G> N = {C. \<forall>Di \<in> \<G>_F C. Di \<in> Red_F_G (\<G>_set N) \<or>
     (\<exists>E \<in> (N - Red_F_\<G> N). Prec_F_g Di E C \<and> Di \<in> \<G>_F E)}\<close>
 proof (rule; clarsimp)
   fix C D
   assume
     C_in: \<open>C \<in> Red_F_\<G> N\<close> and
     D_in: \<open>D \<in> \<G>_F C\<close> and
     not_sec_case: \<open>\<forall>E \<in> N - Red_F_\<G> N. Prec_F_g D E C \<longrightarrow> D \<notin> \<G>_F E\<close>
   have C_in_unfolded: "C \<in> {C. \<forall>Di \<in> \<G>_F C. Di \<in> Red_F_G (\<G>_set N) \<or>
     (\<exists>E\<in>N. Prec_F_g Di E C \<and> Di \<in> \<G>_F E)}"
     using C_in unfolding Red_F_\<G>_def .
   have neg_not_sec_case: \<open>\<not> (\<exists>E\<in>N - Red_F_\<G> N. Prec_F_g D E C \<and> D \<in> \<G>_F E)\<close>
     using not_sec_case by clarsimp
   have unfol_C_D: \<open>D \<in> Red_F_G (\<G>_set N) \<or> (\<exists>E\<in>N. Prec_F_g D E C \<and> D \<in> \<G>_F E)\<close>
     using prop_nested_in_set[of D \<G>_F C "\<lambda>x. x \<in> Red_F_G (\<Union> (\<G>_F ` N))"
       "\<lambda>x y. \<exists>E \<in> N. Prec_F_g y E x \<and> y \<in> \<G>_F E", OF D_in C_in_unfolded] by blast
   show \<open>D \<in> Red_F_G (\<G>_set N)\<close>
   proof (rule ccontr)
     assume contrad: \<open>D \<notin> Red_F_G (\<G>_set N)\<close>
     have non_empty: \<open>\<exists>E\<in>N. Prec_F_g D E C \<and> D \<in> \<G>_F E\<close> using contrad unfol_C_D by auto
     define B where \<open>B = {E \<in> N. Prec_F_g D E C \<and> D \<in> \<G>_F E}\<close>
     then have B_non_empty: \<open>B \<noteq> {}\<close> using non_empty by auto
     interpret minimal_element "Prec_F_g D" UNIV using all_wf[of D] .
     obtain F :: 'f where F: \<open>F = min_elt B\<close> by auto
     then have D_in_F: \<open>D \<in> \<G>_F F\<close> unfolding B_def using non_empty
       by (smt Sup_UNIV Sup_upper UNIV_I contra_subsetD empty_iff empty_subsetI mem_Collect_eq
         min_elt_mem unfol_C_D)
     have F_prec: \<open>Prec_F_g D F C\<close> using F min_elt_mem[of B, OF _ B_non_empty] unfolding B_def by auto
     have F_not_in: \<open>F \<notin> Red_F_\<G> N\<close>
     proof
       assume F_in: \<open>F \<in> Red_F_\<G> N\<close>
       have unfol_F_D: \<open>D \<in> Red_F_G (\<G>_set N) \<or> (\<exists>G\<in>N. Prec_F_g D G F \<and> D \<in> \<G>_F G)\<close>
         using F_in D_in_F unfolding Red_F_\<G>_def by auto
       then have \<open>\<exists>G\<in>N. Prec_F_g D G F \<and> D \<in> \<G>_F G\<close> using contrad D_in unfolding Red_F_\<G>_def by auto
       then obtain G where G_in: \<open>G \<in> N\<close> and G_prec: \<open>Prec_F_g D G F\<close> and G_map: \<open>D \<in> \<G>_F G\<close> by auto
       have \<open>Prec_F_g D G C\<close> using G_prec F_prec Prec_trans by blast
       then have \<open>G \<in> B\<close> unfolding B_def using G_in G_map by auto
       then show \<open>False\<close> using F G_prec min_elt_minimal[of B G, OF _ B_non_empty] by auto
     qed
     have \<open>F \<in> N\<close> using F by (metis B_def B_non_empty mem_Collect_eq min_elt_mem top_greatest)
     then have \<open>F \<in> N - Red_F_\<G> N\<close> using F_not_in by auto
     then show \<open>False\<close>
       using D_in_F neg_not_sec_case F_prec by blast
   qed
 next
   fix C
   assume only_if: \<open>\<forall>D\<in>\<G>_F C. D \<in> Red_F_G (\<G>_set N) \<or> (\<exists>E\<in>N - Red_F_\<G> N. Prec_F_g D E C \<and> D \<in> \<G>_F E)\<close>
   show \<open>C \<in> Red_F_\<G> N\<close> unfolding Red_F_\<G>_def using only_if by auto
 qed
 
 (* lem:lifting-main-technical *)
 lemma not_red_map_in_map_not_red: \<open>\<G>_set N - Red_F_G (\<G>_set N) \<subseteq> \<G>_set (N - Red_F_\<G> N)\<close>
 proof
   fix D
   assume
     D_hyp: \<open>D \<in> \<G>_set N - Red_F_G (\<G>_set N)\<close>
   interpret minimal_element "Prec_F_g D" UNIV using all_wf[of D] .
   have D_in: \<open>D \<in> \<G>_set N\<close> using D_hyp by blast
   have  D_not_in: \<open>D \<notin> Red_F_G (\<G>_set N)\<close> using D_hyp by blast
   have exist_C: \<open>\<exists>C. C \<in> N \<and> D \<in> \<G>_F C\<close> using D_in by auto
   define B where \<open>B = {C \<in> N. D \<in> \<G>_F C}\<close>
   obtain C where C: \<open>C = min_elt B\<close> by auto
   have C_in_N: \<open>C \<in> N\<close>
     using exist_C by (metis B_def C empty_iff mem_Collect_eq min_elt_mem top_greatest)
   have D_in_C: \<open>D \<in> \<G>_F C\<close>
     using exist_C by (metis B_def C empty_iff mem_Collect_eq min_elt_mem top_greatest)
   have C_not_in: \<open>C \<notin> Red_F_\<G> N\<close>
   proof
     assume C_in: \<open>C \<in> Red_F_\<G> N\<close>
     have \<open>D \<in> Red_F_G (\<G>_set N) \<or> (\<exists>E\<in>N. Prec_F_g D E C \<and> D \<in> \<G>_F E)\<close>
       using C_in D_in_C unfolding Red_F_\<G>_def by auto
     then show \<open>False\<close>
       proof
         assume \<open>D \<in> Red_F_G (\<G>_set N)\<close>
         then show \<open>False\<close> using D_not_in by simp
       next
         assume \<open>\<exists>E\<in>N. Prec_F_g D E C \<and> D \<in> \<G>_F E\<close>
         then show \<open>False\<close>
           using C by (metis (no_types, lifting) B_def UNIV_I empty_iff mem_Collect_eq
               min_elt_minimal top_greatest)
       qed
   qed
   show \<open>D \<in> \<G>_set (N - Red_F_\<G> N)\<close> using D_in_C C_not_in C_in_N by blast
 qed
 
 (* lem:nonredundant-entails-redundant *)
 lemma Red_F_Bot_F: \<open>B \<in> Bot_F \<Longrightarrow> N \<Turnstile>\<G> {B} \<Longrightarrow> N - Red_F_\<G> N \<Turnstile>\<G> {B}\<close>
 proof -
   fix B N
   assume
     B_in: \<open>B \<in> Bot_F\<close> and
     N_entails: \<open>N \<Turnstile>\<G> {B}\<close>
   then have to_bot: \<open>\<G>_set N - Red_F_G (\<G>_set N) \<Turnstile>G \<G>_F B\<close>
-    using Ground.Red_F_Bot Bot_map unfolding entails_\<G>_def
-      by (smt cSup_singleton Ground.entail_set_all_formulas image_insert image_is_empty subsetCE)
+    using ground.Red_F_Bot Bot_map unfolding entails_\<G>_def
+      by (smt cSup_singleton ground.entail_set_all_formulas image_insert image_is_empty subsetCE)
   have from_f: \<open>\<G>_set (N - Red_F_\<G> N) \<Turnstile>G \<G>_set N - Red_F_G (\<G>_set N)\<close>
-    using Ground.subset_entailed[OF not_red_map_in_map_not_red] by blast
-  then have \<open>\<G>_set (N - Red_F_\<G> N) \<Turnstile>G \<G>_F B\<close> using to_bot Ground.entails_trans by blast
+    using ground.subset_entailed[OF not_red_map_in_map_not_red] by blast
+  then have \<open>\<G>_set (N - Red_F_\<G> N) \<Turnstile>G \<G>_F B\<close> using to_bot ground.entails_trans by blast
   then show \<open>N - Red_F_\<G> N \<Turnstile>\<G> {B}\<close> using Bot_map unfolding entails_\<G>_def by simp
 qed
 
 (* lem:redundancy-monotonic-addition 1/2 *)
 lemma Red_F_of_subset_F: \<open>N \<subseteq> N' \<Longrightarrow> Red_F_\<G> N \<subseteq> Red_F_\<G> N'\<close>
-  using Ground.Red_F_of_subset unfolding Red_F_\<G>_def by clarsimp (meson \<G>_subset subsetD)
+  using ground.Red_F_of_subset unfolding Red_F_\<G>_def by clarsimp (meson \<G>_subset subsetD)
 
 (* lem:redundancy-monotonic-addition 2/2 *)
 lemma Red_Inf_of_subset_F: \<open>N \<subseteq> N' \<Longrightarrow> Red_Inf_\<G> N \<subseteq> Red_Inf_\<G> N'\<close>
-  using Collect_mono \<G>_subset subset_iff Ground.Red_Inf_of_subset unfolding Red_Inf_\<G>_def
-  by (smt Ground.Red_F_of_subset Un_iff)
+  using Collect_mono \<G>_subset subset_iff ground.Red_Inf_of_subset unfolding Red_Inf_\<G>_def
+  by (smt ground.Red_F_of_subset Un_iff)
 
 (* lem:redundancy-monotonic-deletion-forms *)
 lemma Red_F_of_Red_F_subset_F: \<open>N' \<subseteq> Red_F_\<G> N \<Longrightarrow> Red_F_\<G> N \<subseteq> Red_F_\<G> (N - N')\<close>
 proof
   fix N N' C
   assume
     N'_in_Red_F_N: \<open>N' \<subseteq> Red_F_\<G> N\<close> and
     C_in_red_F_N: \<open>C \<in> Red_F_\<G> N\<close>
   have lem8: \<open>\<forall>D \<in> \<G>_F C. D \<in> Red_F_G (\<G>_set N) \<or> (\<exists>E \<in> (N - Red_F_\<G> N). Prec_F_g D E C \<and> D \<in> \<G>_F E)\<close>
     using Red_F_\<G>_equiv_def C_in_red_F_N by blast
   show \<open>C \<in> Red_F_\<G> (N - N')\<close> unfolding Red_F_\<G>_def
   proof (rule,rule)
     fix D
     assume \<open>D \<in> \<G>_F C\<close>
     then have \<open>D \<in> Red_F_G (\<G>_set N) \<or> (\<exists>E \<in> (N - Red_F_\<G> N). Prec_F_g D E C \<and> D \<in> \<G>_F E)\<close>
       using lem8 by auto
     then show \<open>D \<in> Red_F_G (\<G>_set (N - N')) \<or> (\<exists>E\<in>N - N'. Prec_F_g D E C \<and> D \<in> \<G>_F E)\<close>
     proof
       assume \<open>D \<in> Red_F_G (\<G>_set N)\<close>
       then have \<open>D \<in> Red_F_G (\<G>_set N - Red_F_G (\<G>_set N))\<close>
-        using Ground.Red_F_of_Red_F_subset[of "Red_F_G (\<G>_set N)" "\<G>_set N"] by auto
+        using ground.Red_F_of_Red_F_subset[of "Red_F_G (\<G>_set N)" "\<G>_set N"] by auto
       then have \<open>D \<in> Red_F_G (\<G>_set (N - Red_F_\<G> N))\<close>
-        using Ground.Red_F_of_subset[OF not_red_map_in_map_not_red[of N]] by auto
+        using ground.Red_F_of_subset[OF not_red_map_in_map_not_red[of N]] by auto
       then have \<open>D \<in> Red_F_G (\<G>_set (N - N'))\<close>
         using N'_in_Red_F_N \<G>_subset[of "N - Red_F_\<G> N" "N - N'"]
-        by (smt DiffE DiffI Ground.Red_F_of_subset subsetCE subsetI)
+        by (smt DiffE DiffI ground.Red_F_of_subset subsetCE subsetI)
       then show ?thesis by blast
     next
       assume \<open>\<exists>E\<in>N - Red_F_\<G> N. Prec_F_g D E C \<and> D \<in> \<G>_F E\<close>
       then obtain E where
         E_in: \<open>E\<in>N - Red_F_\<G> N\<close> and
         E_prec_C: \<open>Prec_F_g D E C\<close> and
         D_in: \<open>D \<in> \<G>_F E\<close>
         by auto
       have \<open>E \<in> N - N'\<close> using E_in N'_in_Red_F_N by blast
       then show ?thesis using E_prec_C D_in by blast
     qed
   qed
 qed
 
 (* lem:redundancy-monotonic-deletion-infs *)
 lemma Red_Inf_of_Red_F_subset_F: \<open>N' \<subseteq> Red_F_\<G> N \<Longrightarrow> Red_Inf_\<G> N \<subseteq> Red_Inf_\<G> (N - N') \<close>
 proof
   fix N N' \<iota>
   assume
     N'_in_Red_F_N: \<open>N' \<subseteq> Red_F_\<G> N\<close> and
     i_in_Red_Inf_N: \<open>\<iota> \<in> Red_Inf_\<G> N\<close>
   have i_in: \<open>\<iota> \<in> Inf_F\<close> using i_in_Red_Inf_N unfolding Red_Inf_\<G>_def by blast
   {
     assume not_none: "\<G>_Inf \<iota> \<noteq> None"
     have \<open>\<forall>\<iota>' \<in> the (\<G>_Inf \<iota>). \<iota>' \<in> Red_Inf_G (\<G>_set N)\<close>
       using not_none i_in_Red_Inf_N unfolding Red_Inf_\<G>_def by auto
     then have \<open>\<forall>\<iota>' \<in> the (\<G>_Inf \<iota>). \<iota>' \<in> Red_Inf_G (\<G>_set N - Red_F_G (\<G>_set N))\<close>
-      using not_none Ground.Red_Inf_of_Red_F_subset by blast
+      using not_none ground.Red_Inf_of_Red_F_subset by blast
     then have ip_in_Red_Inf_G: \<open>\<forall>\<iota>' \<in> the (\<G>_Inf \<iota>). \<iota>' \<in> Red_Inf_G (\<G>_set (N - Red_F_\<G> N))\<close>
-      using not_none Ground.Red_Inf_of_subset[OF not_red_map_in_map_not_red[of N]] by auto
+      using not_none ground.Red_Inf_of_subset[OF not_red_map_in_map_not_red[of N]] by auto
     then have not_none_in: \<open>\<forall>\<iota>' \<in> the (\<G>_Inf \<iota>). \<iota>' \<in> Red_Inf_G (\<G>_set (N - N'))\<close>
       using not_none N'_in_Red_F_N
-      by (meson Diff_mono Ground.Red_Inf_of_subset \<G>_subset subset_iff subset_refl)
+      by (meson Diff_mono ground.Red_Inf_of_subset \<G>_subset subset_iff subset_refl)
     then have "the (\<G>_Inf \<iota>) \<subseteq> Red_Inf_G (\<G>_set (N - N'))" by blast
   }
   moreover {
     assume none: "\<G>_Inf \<iota> = None"
     have ground_concl_subs: "\<G>_F (concl_of \<iota>) \<subseteq> (\<G>_set N \<union> Red_F_G (\<G>_set N))"
       using none i_in_Red_Inf_N unfolding Red_Inf_\<G>_def by blast
     then have d_in_imp12: "D \<in> \<G>_F (concl_of \<iota>) \<Longrightarrow> D \<in> \<G>_set N - Red_F_G (\<G>_set N) \<or> D \<in> Red_F_G (\<G>_set N)"
       by blast
     have d_in_imp1: "D \<in> \<G>_set N - Red_F_G (\<G>_set N) \<Longrightarrow> D \<in> \<G>_set (N - N')"
       using not_red_map_in_map_not_red N'_in_Red_F_N by blast
     have d_in_imp_d_in: "D \<in> Red_F_G (\<G>_set N) \<Longrightarrow> D \<in> Red_F_G (\<G>_set N - Red_F_G (\<G>_set N))"
-      using Ground.Red_F_of_Red_F_subset[of "Red_F_G (\<G>_set N)" "\<G>_set N"] by blast
+      using ground.Red_F_of_Red_F_subset[of "Red_F_G (\<G>_set N)" "\<G>_set N"] by blast
     have g_subs1: "\<G>_set N - Red_F_G (\<G>_set N) \<subseteq> \<G>_set (N - Red_F_\<G> N)"
       using not_red_map_in_map_not_red unfolding Red_F_\<G>_def by auto
     have g_subs2: "\<G>_set (N - Red_F_\<G> N) \<subseteq> \<G>_set (N - N')"
       using N'_in_Red_F_N by blast
     have d_in_imp2: "D \<in> Red_F_G (\<G>_set N) \<Longrightarrow> D \<in> Red_F_G (\<G>_set (N - N'))"
-      using Ground.Red_F_of_subset Ground.Red_F_of_subset[OF g_subs1]
-        Ground.Red_F_of_subset[OF g_subs2] d_in_imp_d_in by blast
+      using ground.Red_F_of_subset ground.Red_F_of_subset[OF g_subs1]
+        ground.Red_F_of_subset[OF g_subs2] d_in_imp_d_in by blast
     have "\<G>_F (concl_of \<iota>) \<subseteq> (\<G>_set (N - N') \<union> Red_F_G (\<G>_set (N - N')))"
       using d_in_imp12 d_in_imp1 d_in_imp2
-      by (smt Ground.Red_F_of_Red_F_subset Ground.Red_F_of_subset UnCI UnE Un_Diff_cancel2
+      by (smt ground.Red_F_of_Red_F_subset ground.Red_F_of_subset UnCI UnE Un_Diff_cancel2
         ground_concl_subs g_subs1 g_subs2 subset_iff)
   }
   ultimately show \<open>\<iota> \<in> Red_Inf_\<G> (N - N')\<close> using i_in unfolding Red_Inf_\<G>_def by auto
 qed
 
 (* lem:concl-contained-implies-red-inf *)
 lemma Red_Inf_of_Inf_to_N_F:
   assumes
     i_in: \<open>\<iota> \<in> Inf_F\<close> and
     concl_i_in: \<open>concl_of \<iota> \<in> N\<close>
   shows
     \<open>\<iota> \<in> Red_Inf_\<G> N \<close>
 proof -
   have \<open>\<iota> \<in> Inf_F \<Longrightarrow> \<G>_Inf \<iota> \<noteq> None \<Longrightarrow> the (\<G>_Inf \<iota>) \<subseteq> Red_Inf_G (\<G>_F (concl_of \<iota>))\<close> using inf_map by simp
   moreover have \<open>Red_Inf_G (\<G>_F (concl_of \<iota>)) \<subseteq> Red_Inf_G (\<G>_set N)\<close>
-    using concl_i_in Ground.Red_Inf_of_subset by blast
+    using concl_i_in ground.Red_Inf_of_subset by blast
   moreover have "\<iota> \<in> Inf_F \<Longrightarrow> \<G>_Inf \<iota> = None \<Longrightarrow> concl_of \<iota> \<in> N \<Longrightarrow> \<G>_F (concl_of \<iota>) \<subseteq> \<G>_set N"
     by blast
   ultimately show ?thesis using i_in concl_i_in unfolding Red_Inf_\<G>_def by auto
 qed
 
 (* thm:FRedsqsubset-is-red-crit and also thm:lifted-red-crit if ordering empty *)
-sublocale lifted_calculus_with_red_crit: calculus_with_red_crit
-  where
-    Bot = Bot_F and Inf = Inf_F and entails = entails_\<G> and
-    Red_Inf = Red_Inf_\<G> and Red_F = Red_F_\<G>
+sublocale calculus_with_red_crit Bot_F Inf_F entails_\<G> Red_Inf_\<G> Red_F_\<G>
 proof
   fix B N N' \<iota>
   show \<open>Red_Inf_\<G> N \<subseteq> Inf_F\<close> unfolding Red_Inf_\<G>_def by blast
   show \<open>B \<in> Bot_F \<Longrightarrow> N \<Turnstile>\<G> {B} \<Longrightarrow> N - Red_F_\<G> N \<Turnstile>\<G> {B}\<close> using Red_F_Bot_F by simp
   show \<open>N \<subseteq> N' \<Longrightarrow> Red_F_\<G> N \<subseteq> Red_F_\<G> N'\<close> using Red_F_of_subset_F by simp
   show \<open>N \<subseteq> N' \<Longrightarrow> Red_Inf_\<G> N \<subseteq> Red_Inf_\<G> N'\<close> using Red_Inf_of_subset_F by simp
   show \<open>N' \<subseteq> Red_F_\<G> N \<Longrightarrow> Red_F_\<G> N \<subseteq> Red_F_\<G> (N - N')\<close> using Red_F_of_Red_F_subset_F by simp
   show \<open>N' \<subseteq> Red_F_\<G> N \<Longrightarrow> Red_Inf_\<G> N \<subseteq> Red_Inf_\<G> (N - N')\<close> using Red_Inf_of_Red_F_subset_F by simp
   show \<open>\<iota> \<in> Inf_F \<Longrightarrow> concl_of \<iota> \<in> N \<Longrightarrow> \<iota> \<in> Red_Inf_\<G> N\<close> using Red_Inf_of_Inf_to_N_F by simp
 qed
 
 lemma grounded_inf_in_ground_inf: "\<iota> \<in> Inf_F \<Longrightarrow> \<G>_Inf \<iota> \<noteq> None \<Longrightarrow> the (\<G>_Inf \<iota>) \<subseteq> Inf_G"
-  using inf_map Ground.Red_Inf_to_Inf by blast
+  using inf_map ground.Red_Inf_to_Inf by blast
 
 (* lem:sat-wrt-finf *)
-lemma sat_imp_ground_sat: "lifted_calculus_with_red_crit.saturated N \<Longrightarrow> Ground.Inf_from (\<G>_set N) \<subseteq>
-  ({\<iota>. \<exists>\<iota>'\<in> Non_ground.Inf_from N. \<G>_Inf \<iota>' \<noteq> None \<and> \<iota> \<in> the (\<G>_Inf \<iota>')} \<union> Red_Inf_G (\<G>_set N)) \<Longrightarrow>
-  Ground.saturated (\<G>_set N)"
+lemma sat_imp_ground_sat: "saturated N \<Longrightarrow> ground.Inf_from (\<G>_set N) \<subseteq>
+  ({\<iota>. \<exists>\<iota>'\<in> Inf_from N. \<G>_Inf \<iota>' \<noteq> None \<and> \<iota> \<in> the (\<G>_Inf \<iota>')} \<union> Red_Inf_G (\<G>_set N)) \<Longrightarrow>
+  ground.saturated (\<G>_set N)"
 proof -
   fix N
   assume
-    sat_n: "lifted_calculus_with_red_crit.saturated N" and
-    inf_grounded_in: "Ground.Inf_from (\<G>_set N) \<subseteq>
-    ({\<iota>. \<exists>\<iota>'\<in> Non_ground.Inf_from N. \<G>_Inf \<iota>' \<noteq> None \<and> \<iota> \<in> the (\<G>_Inf \<iota>')} \<union> Red_Inf_G (\<G>_set N))"
-  show "Ground.saturated (\<G>_set N)" unfolding Ground.saturated_def
+    sat_n: "saturated N" and
+    inf_grounded_in: "ground.Inf_from (\<G>_set N) \<subseteq>
+    ({\<iota>. \<exists>\<iota>'\<in> Inf_from N. \<G>_Inf \<iota>' \<noteq> None \<and> \<iota> \<in> the (\<G>_Inf \<iota>')} \<union> Red_Inf_G (\<G>_set N))"
+  show "ground.saturated (\<G>_set N)" unfolding ground.saturated_def
   proof
     fix \<iota>
-    assume i_in: "\<iota> \<in> Ground.Inf_from (\<G>_set N)"
+    assume i_in: "\<iota> \<in> ground.Inf_from (\<G>_set N)"
     {
-      assume "\<iota> \<in> {\<iota>. \<exists>\<iota>'\<in> Non_ground.Inf_from N. \<G>_Inf \<iota>' \<noteq> None \<and> \<iota> \<in> the (\<G>_Inf \<iota>')}"
-      then obtain \<iota>' where "\<iota>'\<in> Non_ground.Inf_from N" "\<G>_Inf \<iota>' \<noteq> None" "\<iota> \<in> the (\<G>_Inf \<iota>')" by blast
+      assume "\<iota> \<in> {\<iota>. \<exists>\<iota>'\<in> Inf_from N. \<G>_Inf \<iota>' \<noteq> None \<and> \<iota> \<in> the (\<G>_Inf \<iota>')}"
+      then obtain \<iota>' where "\<iota>'\<in> Inf_from N" "\<G>_Inf \<iota>' \<noteq> None" "\<iota> \<in> the (\<G>_Inf \<iota>')" by blast
       then have "\<iota> \<in> Red_Inf_G (\<G>_set N)"
-        using Red_Inf_\<G>_def sat_n unfolding lifted_calculus_with_red_crit.saturated_def by auto
+        using Red_Inf_\<G>_def sat_n unfolding saturated_def by auto
     }
     then show "\<iota> \<in> Red_Inf_G (\<G>_set N)" using inf_grounded_in i_in by blast
   qed
 qed
 
 (* thm:finf-complete *)
 theorem stat_ref_comp_to_non_ground:
   assumes
     stat_ref_G: "static_refutational_complete_calculus Bot_G Inf_G entails_G Red_Inf_G Red_F_G" and
-    sat_n_imp: "\<And>N. lifted_calculus_with_red_crit.saturated N \<Longrightarrow> Ground.Inf_from (\<G>_set N) \<subseteq>
-      {\<iota>. \<exists>\<iota>'\<in> Non_ground.Inf_from N. \<G>_Inf \<iota>' \<noteq> None \<and> \<iota> \<in> the (\<G>_Inf \<iota>')} \<union> Red_Inf_G (\<G>_set N)"
+    sat_n_imp: "\<And>N. saturated N \<Longrightarrow> ground.Inf_from (\<G>_set N) \<subseteq>
+      {\<iota>. \<exists>\<iota>'\<in> Inf_from N. \<G>_Inf \<iota>' \<noteq> None \<and> \<iota> \<in> the (\<G>_Inf \<iota>')} \<union> Red_Inf_G (\<G>_set N)"
   shows
     "static_refutational_complete_calculus Bot_F Inf_F entails_\<G> Red_Inf_\<G> Red_F_\<G>"
 proof
   fix B N
   assume
     b_in: "B \<in> Bot_F" and
-    sat_n: "lifted_calculus_with_red_crit.saturated N" and
+    sat_n: "saturated N" and
     n_entails_bot: "N \<Turnstile>\<G> {B}"
   have ground_n_entails: "\<G>_set N \<Turnstile>G \<G>_F B"
     using n_entails_bot unfolding entails_\<G>_def by simp
   then obtain BG where bg_in1: "BG \<in> \<G>_F B"
     using Bot_map_not_empty[OF b_in] by blast
   then have bg_in: "BG \<in> Bot_G"
     using Bot_map[OF b_in] by blast
   have ground_n_entails_bot: "\<G>_set N \<Turnstile>G {BG}"
-    using ground_n_entails bg_in1 Ground.entail_set_all_formulas by blast
-  have "Ground.Inf_from (\<G>_set N) \<subseteq>
-    {\<iota>. \<exists>\<iota>'\<in> Non_ground.Inf_from N. \<G>_Inf \<iota>' \<noteq> None \<and> \<iota> \<in> the (\<G>_Inf \<iota>')} \<union> Red_Inf_G (\<G>_set N)"
+    using ground_n_entails bg_in1 ground.entail_set_all_formulas by blast
+  have "ground.Inf_from (\<G>_set N) \<subseteq>
+    {\<iota>. \<exists>\<iota>'\<in> Inf_from N. \<G>_Inf \<iota>' \<noteq> None \<and> \<iota> \<in> the (\<G>_Inf \<iota>')} \<union> Red_Inf_G (\<G>_set N)"
     using sat_n_imp[OF sat_n] .
-  have "Ground.saturated (\<G>_set N)"
+  have "ground.saturated (\<G>_set N)"
     using sat_imp_ground_sat[OF sat_n sat_n_imp[OF sat_n]] .
   then have "\<exists>BG'\<in>Bot_G. BG' \<in> (\<G>_set N)"
-    using stat_ref_G Ground.calculus_with_red_crit_axioms bg_in ground_n_entails_bot
+    using stat_ref_G ground.calculus_with_red_crit_axioms bg_in ground_n_entails_bot
     unfolding static_refutational_complete_calculus_def static_refutational_complete_calculus_axioms_def
     by blast
   then show "\<exists>B'\<in> Bot_F. B' \<in> N"
     using bg_in Bot_cond Bot_map_not_empty Bot_cond by blast
 qed
 
 end
 
 abbreviation Empty_Order :: "'f \<Rightarrow> 'f \<Rightarrow> bool" where
   "Empty_Order C1 C2 \<equiv> False"
 
 lemma wf_Empty_Order: "minimal_element Empty_Order UNIV"
   by (simp add: minimal_element.intro po_on_def transp_onI wfp_on_imp_irreflp_on)
 
 lemma any_to_empty_order_lifting:
   "lifting_with_wf_ordering_family Bot_F Inf_F Bot_G entails_G Inf_G Red_Inf_G Red_F_G \<G>_F
     \<G>_Inf Prec_F_g \<Longrightarrow> lifting_with_wf_ordering_family Bot_F Inf_F Bot_G entails_G Inf_G Red_Inf_G
     Red_F_G \<G>_F \<G>_Inf (\<lambda>g. Empty_Order)"
 proof -
   fix Bot_F Inf_F Bot_G entails_G Inf_G Red_Inf_G Red_F_G \<G>_F \<G>_Inf Prec_F_g
   assume lift: "lifting_with_wf_ordering_family Bot_F Inf_F Bot_G entails_G Inf_G Red_Inf_G
     Red_F_G \<G>_F \<G>_Inf Prec_F_g"
   then interpret lift_g:
     lifting_with_wf_ordering_family Bot_F Inf_F Bot_G entails_G Inf_G Red_Inf_G Red_F_G \<G>_F
       \<G>_Inf Prec_F_g
     by auto
   show "lifting_with_wf_ordering_family Bot_F Inf_F Bot_G entails_G Inf_G Red_Inf_G Red_F_G
     \<G>_F \<G>_Inf (\<lambda>g. Empty_Order)"
     by (simp add: wf_Empty_Order lift_g.standard_lifting_axioms
       lifting_with_wf_ordering_family_axioms.intro lifting_with_wf_ordering_family_def)
 qed
 
 locale lifting_equivalence_with_empty_order =
   any_order_lifting: lifting_with_wf_ordering_family Bot_F Inf_F Bot_G entails_G Inf_G Red_Inf_G
     Red_F_G \<G>_F \<G>_Inf Prec_F_g +
   empty_order_lifting: lifting_with_wf_ordering_family Bot_F Inf_F Bot_G entails_G Inf_G Red_Inf_G
     Red_F_G \<G>_F \<G>_Inf "\<lambda>g. Empty_Order"
   for
     \<G>_F :: \<open>'f \<Rightarrow> 'g set\<close> and
     \<G>_Inf :: \<open>'f inference \<Rightarrow> 'g inference set option\<close> and
     Bot_F :: \<open>'f set\<close> and
     Inf_F :: \<open>'f inference set\<close> and
     Bot_G :: \<open>'g set\<close> and
     Inf_G :: \<open>'g inference set\<close> and
     entails_G :: \<open>'g set \<Rightarrow> 'g set \<Rightarrow> bool\<close> (infix "\<Turnstile>G" 50) and
     Red_Inf_G :: \<open>'g set \<Rightarrow> 'g inference set\<close> and
     Red_F_G :: \<open>'g set \<Rightarrow> 'g set\<close> and
     Prec_F_g :: \<open>'g \<Rightarrow> 'f \<Rightarrow> 'f \<Rightarrow> bool\<close>
 
 sublocale lifting_with_wf_ordering_family \<subseteq> lifting_equivalence_with_empty_order
 proof
   show "po_on Empty_Order UNIV"
     unfolding po_on_def by (simp add: transp_onI wfp_on_imp_irreflp_on)
   show "wfp_on Empty_Order UNIV"
     unfolding wfp_on_def by simp
 qed
 
 context lifting_equivalence_with_empty_order
 begin
 
 (* lem:saturation-indep-of-sqsubset *)
 lemma saturated_empty_order_equiv_saturated:
-  "any_order_lifting.lifted_calculus_with_red_crit.saturated N =
-    empty_order_lifting.lifted_calculus_with_red_crit.saturated N" by standard
+  "any_order_lifting.saturated N = empty_order_lifting.saturated N"
+  by (rule refl)
 
 (* lem:static-ref-compl-indep-of-sqsubset *)
 lemma static_empty_order_equiv_static:
   "static_refutational_complete_calculus Bot_F Inf_F any_order_lifting.entails_\<G>
      empty_order_lifting.Red_Inf_\<G> empty_order_lifting.Red_F_\<G> =
    static_refutational_complete_calculus Bot_F Inf_F any_order_lifting.entails_\<G>
      any_order_lifting.Red_Inf_\<G> any_order_lifting.Red_F_\<G>"
   unfolding static_refutational_complete_calculus_def
   by (rule iffI) (standard,(standard)[],simp)+
 
 (* thm:FRedsqsubset-is-dyn-ref-compl *)
 theorem static_to_dynamic:
   "static_refutational_complete_calculus Bot_F Inf_F
     any_order_lifting.entails_\<G> empty_order_lifting.Red_Inf_\<G> empty_order_lifting.Red_F_\<G> =
     dynamic_refutational_complete_calculus Bot_F Inf_F
     any_order_lifting.entails_\<G> any_order_lifting.Red_Inf_\<G> any_order_lifting.Red_F_\<G> "
   (is "?static = ?dynamic")
 proof
   assume ?static
   then have static_general:
     "static_refutational_complete_calculus Bot_F Inf_F any_order_lifting.entails_\<G>
       any_order_lifting.Red_Inf_\<G> any_order_lifting.Red_F_\<G>" (is "?static_gen")
     using static_empty_order_equiv_static by simp
   interpret static_refutational_complete_calculus Bot_F Inf_F any_order_lifting.entails_\<G>
     any_order_lifting.Red_Inf_\<G> any_order_lifting.Red_F_\<G>
     using static_general .
   show "?dynamic" by standard
 next
   assume dynamic_gen: ?dynamic
   interpret dynamic_refutational_complete_calculus Bot_F Inf_F any_order_lifting.entails_\<G>
     any_order_lifting.Red_Inf_\<G> any_order_lifting.Red_F_\<G>
     using dynamic_gen .
   have "static_refutational_complete_calculus Bot_F Inf_F any_order_lifting.entails_\<G>
     any_order_lifting.Red_Inf_\<G> any_order_lifting.Red_F_\<G>"
     by standard
   then show "?static" using static_empty_order_equiv_static by simp
 qed
 
 end
 
 subsection \<open>Lifting with a Family of Redundancy Criteria\<close>
 
-locale standard_lifting_with_red_crit_family = Non_ground: inference_system Inf_F
-  + Ground_family: calculus_family_with_red_crit_family Bot_G Q Inf_G_q entails_q Red_Inf_q Red_F_q
+locale standard_lifting_with_red_crit_family = inference_system Inf_F
+  + ground: calculus_family_with_red_crit_family Bot_G Q Inf_G_q entails_q Red_Inf_q Red_F_q
   for
     Inf_F :: "'f inference set" and
     Bot_G :: "'g set" and
     Q :: "'q set" and
     Inf_G_q :: \<open>'q \<Rightarrow> 'g inference set\<close> and
     entails_q :: "'q \<Rightarrow> 'g set \<Rightarrow> 'g set \<Rightarrow> bool" and
     Red_Inf_q :: "'q \<Rightarrow> 'g set \<Rightarrow> 'g inference set" and
     Red_F_q :: "'q \<Rightarrow> 'g set \<Rightarrow> 'g set"
   + fixes
     Bot_F :: "'f set" and
     \<G>_F_q :: "'q \<Rightarrow> 'f \<Rightarrow> 'g set" and
     \<G>_Inf_q :: "'q \<Rightarrow> 'f inference \<Rightarrow> 'g inference set option" and
     Prec_F_g :: "'g \<Rightarrow> 'f \<Rightarrow> 'f \<Rightarrow> bool"
   assumes
     standard_lifting_family:
       "\<forall>q \<in> Q. lifting_with_wf_ordering_family Bot_F Inf_F Bot_G (entails_q q) (Inf_G_q q)
          (Red_Inf_q q) (Red_F_q q) (\<G>_F_q q) (\<G>_Inf_q q) Prec_F_g"
 begin
 
 definition \<G>_set_q :: "'q \<Rightarrow> 'f set \<Rightarrow> 'g set" where
   "\<G>_set_q q N = \<Union> (\<G>_F_q q ` N)"
 
 definition Red_Inf_\<G>_q :: "'q \<Rightarrow> 'f set \<Rightarrow> 'f inference set" where
   "Red_Inf_\<G>_q q N = {\<iota> \<in> Inf_F. (\<G>_Inf_q q \<iota> \<noteq> None \<and> the (\<G>_Inf_q q \<iota>) \<subseteq> Red_Inf_q q (\<G>_set_q q N))
    \<or> (\<G>_Inf_q q \<iota> = None \<and> \<G>_F_q q (concl_of \<iota>) \<subseteq> (\<G>_set_q q N \<union> Red_F_q q (\<G>_set_q q N)))}"
 
 definition Red_Inf_\<G>_Q :: "'f set \<Rightarrow> 'f inference set" where
   "Red_Inf_\<G>_Q N = (\<Inter>q \<in> Q. Red_Inf_\<G>_q q N)"
 
 definition Red_F_\<G>_empty_q :: "'q \<Rightarrow> 'f set \<Rightarrow> 'f set" where
   "Red_F_\<G>_empty_q q N = {C. \<forall>D \<in> \<G>_F_q q C. D \<in> Red_F_q q (\<G>_set_q q N)}"
 
 definition Red_F_\<G>_empty :: "'f set \<Rightarrow> 'f set" where
   "Red_F_\<G>_empty N = (\<Inter>q \<in> Q. Red_F_\<G>_empty_q q N)"
 
 definition Red_F_\<G>_q_g :: "'q \<Rightarrow> 'f set \<Rightarrow> 'f set" where
   "Red_F_\<G>_q_g q N =
    {C. \<forall>D \<in> \<G>_F_q q C. D \<in> Red_F_q q (\<G>_set_q q N) \<or> (\<exists>E \<in> N. Prec_F_g D E C \<and> D \<in> \<G>_F_q q E)}"
 
 definition Red_F_\<G>_g :: "'f set \<Rightarrow> 'f set" where
   "Red_F_\<G>_g N = (\<Inter>q \<in> Q. Red_F_\<G>_q_g q N)"
 
 definition entails_\<G>_q :: "'q \<Rightarrow> 'f set \<Rightarrow> 'f set \<Rightarrow> bool" where
   "entails_\<G>_q q N1 N2 \<longleftrightarrow> entails_q q (\<G>_set_q q N1) (\<G>_set_q q N2)"
 
 definition entails_\<G>_Q :: "'f set \<Rightarrow> 'f set \<Rightarrow> bool" (infix "\<Turnstile>\<inter>\<G>" 50) where
   "entails_\<G>_Q N1 N2 \<longleftrightarrow> (\<forall>q \<in> Q. entails_\<G>_q q N1 N2)"
 
 lemma red_crit_lifting_family:
   assumes q_in: "q \<in> Q"
   shows "calculus_with_red_crit Bot_F Inf_F (entails_\<G>_q q) (Red_Inf_\<G>_q q) (Red_F_\<G>_q_g q)"
 proof -
   interpret wf_lift:
     lifting_with_wf_ordering_family Bot_F Inf_F Bot_G "entails_q q" "Inf_G_q q" "Red_Inf_q q"
       "Red_F_q q" "\<G>_F_q q" "\<G>_Inf_q q" Prec_F_g
     using standard_lifting_family q_in by metis
   have "entails_\<G>_q q = wf_lift.entails_\<G>"
     unfolding entails_\<G>_q_def wf_lift.entails_\<G>_def \<G>_set_q_def by blast
   moreover have "Red_Inf_\<G>_q q = wf_lift.Red_Inf_\<G>"
     unfolding Red_Inf_\<G>_q_def \<G>_set_q_def wf_lift.Red_Inf_\<G>_def by blast
   moreover have "Red_F_\<G>_q_g q = wf_lift.Red_F_\<G>"
     unfolding Red_F_\<G>_q_g_def \<G>_set_q_def wf_lift.Red_F_\<G>_def by blast
   ultimately show ?thesis
-    using wf_lift.lifted_calculus_with_red_crit.calculus_with_red_crit_axioms by simp
+    using wf_lift.calculus_with_red_crit_axioms by simp
 qed
 
 lemma red_crit_lifting_family_empty_ord:
   assumes q_in: "q \<in> Q"
   shows "calculus_with_red_crit Bot_F Inf_F (entails_\<G>_q q) (Red_Inf_\<G>_q q) (Red_F_\<G>_empty_q q)"
 proof -
   interpret wf_lift:
     lifting_with_wf_ordering_family Bot_F Inf_F Bot_G "entails_q q" "Inf_G_q q" "Red_Inf_q q"
       "Red_F_q q" "\<G>_F_q q" "\<G>_Inf_q q" Prec_F_g
     using standard_lifting_family q_in by metis
   have "entails_\<G>_q q = wf_lift.entails_\<G>"
     unfolding entails_\<G>_q_def wf_lift.entails_\<G>_def \<G>_set_q_def by blast
   moreover have "Red_Inf_\<G>_q q = wf_lift.Red_Inf_\<G>"
     unfolding Red_Inf_\<G>_q_def \<G>_set_q_def wf_lift.Red_Inf_\<G>_def by blast
   moreover have "Red_F_\<G>_empty_q q = wf_lift.empty_order_lifting.Red_F_\<G>"
     unfolding Red_F_\<G>_empty_q_def \<G>_set_q_def wf_lift.empty_order_lifting.Red_F_\<G>_def by blast
   ultimately show ?thesis
-    using wf_lift.empty_order_lifting.lifted_calculus_with_red_crit.calculus_with_red_crit_axioms
-    by simp
+    using wf_lift.empty_order_lifting.calculus_with_red_crit_axioms by simp
 qed
 
 lemma cons_rel_fam_Q_lem: \<open>consequence_relation_family Bot_F Q entails_\<G>_q\<close>
 proof (unfold_locales; (intro ballI)?)
   show "Q \<noteq> {}"
-    by (rule Ground_family.Q_nonempty)
+    by (rule ground.Q_nonempty)
 next
   fix qi
   assume qi_in: "qi \<in> Q"
 
   interpret lift: lifting_with_wf_ordering_family Bot_F Inf_F Bot_G "entails_q qi" "Inf_G_q qi"
     "Red_Inf_q qi" "Red_F_q qi" "\<G>_F_q qi" "\<G>_Inf_q qi" Prec_F_g
     using qi_in by (metis standard_lifting_family)
   have ent_eq: "entails_\<G>_q qi = lift.entails_\<G>"
     unfolding entails_\<G>_q_def lift.entails_\<G>_def \<G>_set_q_def by simp
 
   show "consequence_relation Bot_F (entails_\<G>_q qi)"
   proof
     show "Bot_F \<noteq> {}"
       using qi_in by (simp add: lift.lifted_consequence_relation.bot_not_empty)
   next
     fix B N1
     assume "B \<in> Bot_F"
     then show "entails_\<G>_q qi {B} N1"
       using ent_eq lift.lifted_consequence_relation.bot_entails_all by auto
   next
     fix N2 N1::"'f set"
     assume "N2 \<subseteq> N1"
     then show "entails_\<G>_q qi N1 N2"
       using ent_eq by (simp add: lift.lifted_consequence_relation.subset_entailed)
   next
     fix N1 N2
     assume "\<forall>C\<in> N2. entails_\<G>_q qi N1 {C}"
     then show "entails_\<G>_q qi N1 N2"
       using ent_eq lift.lifted_consequence_relation.all_formulas_entailed by metis
   next
     fix N1 N2 N3
     assume
       "entails_\<G>_q qi N1 N2" and
       "entails_\<G>_q qi N2 N3"
     then show "entails_\<G>_q qi N1 N3"
       using ent_eq lift.lifted_consequence_relation.entails_trans by metis
   qed
 qed
 
 sublocale cons_rel_Q: consequence_relation Bot_F entails_\<G>_Q
 proof -
   interpret cons_rel_fam: consequence_relation_family Bot_F Q entails_\<G>_q
     by (rule cons_rel_fam_Q_lem)
   have "consequence_relation_family.entails_Q Q entails_\<G>_q = entails_\<G>_Q"
     unfolding entails_\<G>_Q_def cons_rel_fam.entails_Q_def by (simp add: entails_\<G>_q_def)
   then show "consequence_relation Bot_F entails_\<G>_Q"
   using consequence_relation_family.intersect_cons_rel_family[OF cons_rel_fam_Q_lem] by simp
 qed
 
 sublocale lifted_calc_w_red_crit_family:
   calculus_with_red_crit_family Bot_F Inf_F Q entails_\<G>_q Red_Inf_\<G>_q Red_F_\<G>_q_g
   using cons_rel_fam_Q_lem red_crit_lifting_family
-  by (simp add: Ground_family.Q_nonempty calculus_with_red_crit_family.intro
+  by (simp add: ground.Q_nonempty calculus_with_red_crit_family.intro
       calculus_with_red_crit_family_axioms_def)
 
 sublocale lifted_calc_w_red_crit:
   calculus_with_red_crit Bot_F Inf_F entails_\<G>_Q Red_Inf_\<G>_Q Red_F_\<G>_g
 proof -
   have "lifted_calc_w_red_crit_family.entails_Q = entails_\<G>_Q"
     unfolding entails_\<G>_Q_def lifted_calc_w_red_crit_family.entails_Q_def by simp
   moreover have "lifted_calc_w_red_crit_family.Red_Inf_Q = Red_Inf_\<G>_Q"
     unfolding Red_Inf_\<G>_Q_def lifted_calc_w_red_crit_family.Red_Inf_Q_def by simp
   moreover have "lifted_calc_w_red_crit_family.Red_F_Q = Red_F_\<G>_g"
     unfolding Red_F_\<G>_g_def lifted_calc_w_red_crit_family.Red_F_Q_def by simp
   ultimately show "calculus_with_red_crit Bot_F Inf_F entails_\<G>_Q Red_Inf_\<G>_Q Red_F_\<G>_g"
-  using lifted_calc_w_red_crit_family.inter_red_crit_calculus.calculus_with_red_crit_axioms by simp
+  using lifted_calc_w_red_crit_family.calculus_with_red_crit_axioms by simp
 qed
 
 sublocale empty_ord_lifted_calc_w_red_crit_family:
   calculus_with_red_crit_family Bot_F Inf_F Q entails_\<G>_q Red_Inf_\<G>_q Red_F_\<G>_empty_q
   using cons_rel_fam_Q_lem red_crit_lifting_family_empty_ord
   by (simp add: calculus_with_red_crit_family.intro calculus_with_red_crit_family_axioms_def
       lifted_calc_w_red_crit_family.Q_nonempty)
 
 lemma inter_calc: "calculus_with_red_crit Bot_F Inf_F entails_\<G>_Q Red_Inf_\<G>_Q Red_F_\<G>_empty"
 proof -
   have "lifted_calc_w_red_crit_family.entails_Q = entails_\<G>_Q"
     unfolding entails_\<G>_Q_def lifted_calc_w_red_crit_family.entails_Q_def by simp
   moreover have "empty_ord_lifted_calc_w_red_crit_family.Red_Inf_Q = Red_Inf_\<G>_Q"
     unfolding Red_Inf_\<G>_Q_def lifted_calc_w_red_crit_family.Red_Inf_Q_def by simp
   moreover have "empty_ord_lifted_calc_w_red_crit_family.Red_F_Q = Red_F_\<G>_empty"
     unfolding Red_F_\<G>_empty_def empty_ord_lifted_calc_w_red_crit_family.Red_F_Q_def by simp
   ultimately show "calculus_with_red_crit Bot_F Inf_F entails_\<G>_Q Red_Inf_\<G>_Q Red_F_\<G>_empty"
-  using empty_ord_lifted_calc_w_red_crit_family.inter_red_crit_calculus.calculus_with_red_crit_axioms
+  using empty_ord_lifted_calc_w_red_crit_family.calculus_with_red_crit_axioms
   by simp
 qed
 
 (* thm:intersect-finf-complete *)
 theorem stat_ref_comp_to_non_ground_fam_inter:
   assumes
     stat_ref_G:
       "\<forall>q \<in> Q. static_refutational_complete_calculus Bot_G (Inf_G_q q) (entails_q q) (Red_Inf_q q)
         (Red_F_q q)" and
     sat_n_imp:
-      "\<And>N. empty_ord_lifted_calc_w_red_crit_family.inter_red_crit_calculus.saturated N \<Longrightarrow>
-         \<exists>q \<in> Q. Ground_family.Inf_from_q q (\<G>_set_q q N) \<subseteq>
-           {\<iota>. \<exists>\<iota>'\<in> Non_ground.Inf_from N. \<G>_Inf_q q \<iota>' \<noteq> None \<and> \<iota> \<in> the (\<G>_Inf_q q \<iota>')}
+      "\<And>N. empty_ord_lifted_calc_w_red_crit_family.saturated N \<Longrightarrow>
+         \<exists>q \<in> Q. ground.Inf_from_q q (\<G>_set_q q N) \<subseteq>
+           {\<iota>. \<exists>\<iota>'\<in> Inf_from N. \<G>_Inf_q q \<iota>' \<noteq> None \<and> \<iota> \<in> the (\<G>_Inf_q q \<iota>')}
            \<union> Red_Inf_q q (\<G>_set_q q N)"
   shows
     "static_refutational_complete_calculus Bot_F Inf_F entails_\<G>_Q Red_Inf_\<G>_Q Red_F_\<G>_empty"
     using inter_calc unfolding static_refutational_complete_calculus_def
       static_refutational_complete_calculus_axioms_def
 proof (standard, clarify)
   fix B N
   assume
     b_in: "B \<in> Bot_F" and
     sat_n: "calculus_with_red_crit.saturated Inf_F Red_Inf_\<G>_Q N" and
     entails_bot: "N \<Turnstile>\<inter>\<G> {B}"
   have "empty_ord_lifted_calc_w_red_crit_family.Red_Inf_Q = Red_Inf_\<G>_Q"
     unfolding Red_Inf_\<G>_Q_def lifted_calc_w_red_crit_family.Red_Inf_Q_def by simp
-  then have empty_ord_sat_n:
-    "empty_ord_lifted_calc_w_red_crit_family.inter_red_crit_calculus.saturated N"
+  then have empty_ord_sat_n: "empty_ord_lifted_calc_w_red_crit_family.saturated N"
     using sat_n unfolding lifted_calc_w_red_crit.saturated_def
-      empty_ord_lifted_calc_w_red_crit_family.inter_red_crit_calculus.saturated_def
+      empty_ord_lifted_calc_w_red_crit_family.saturated_def
     by simp
   then obtain q where
     q_in: "q \<in> Q" and
-    inf_subs: "Ground_family.Inf_from_q q (\<G>_set_q q N) \<subseteq>
-      {\<iota>. \<exists>\<iota>'\<in> Non_ground.Inf_from N. \<G>_Inf_q q \<iota>' \<noteq> None \<and> \<iota> \<in> the (\<G>_Inf_q q \<iota>')}
+    inf_subs: "ground.Inf_from_q q (\<G>_set_q q N) \<subseteq>
+      {\<iota>. \<exists>\<iota>'\<in> Inf_from N. \<G>_Inf_q q \<iota>' \<noteq> None \<and> \<iota> \<in> the (\<G>_Inf_q q \<iota>')}
       \<union> Red_Inf_q q (\<G>_set_q q N)"
     using sat_n_imp[of N] by blast
   interpret q_calc: calculus_with_red_crit Bot_F Inf_F "entails_\<G>_q q" "Red_Inf_\<G>_q q" "Red_F_\<G>_q_g q"
     using lifted_calc_w_red_crit_family.all_red_crit[rule_format, OF q_in] .
   have n_q_sat: "q_calc.saturated N"
     using q_in lifted_calc_w_red_crit_family.sat_int_to_sat_q empty_ord_sat_n by simp
   interpret lifted_q_calc:
     lifting_with_wf_ordering_family Bot_F Inf_F Bot_G "entails_q q" "Inf_G_q q" "Red_Inf_q q"
       "Red_F_q q" "\<G>_F_q q" "\<G>_Inf_q q"
     using q_in by (simp add: standard_lifting_family)
-  have n_lift_sat: "lifted_q_calc.empty_order_lifting.lifted_calculus_with_red_crit.saturated N"
+  have n_lift_sat: "lifted_q_calc.empty_order_lifting.saturated N"
     using n_q_sat unfolding Red_Inf_\<G>_q_def \<G>_set_q_def lifted_q_calc.empty_order_lifting.Red_Inf_\<G>_def
-      lifted_q_calc.lifted_calculus_with_red_crit.saturated_def q_calc.saturated_def by auto
-  have ground_sat_n: "lifted_q_calc.Ground.saturated (\<G>_set_q q N)"
+      lifted_q_calc.saturated_def q_calc.saturated_def by auto
+  have ground_sat_n: "lifted_q_calc.ground.saturated (\<G>_set_q q N)"
     unfolding \<G>_set_q_def
     by (rule lifted_q_calc.sat_imp_ground_sat[OF n_lift_sat[unfolded \<G>_set_q_def]])
-      (use n_lift_sat inf_subs Ground_family.Inf_from_q_def \<G>_set_q_def in auto)
+      (use n_lift_sat inf_subs ground.Inf_from_q_def \<G>_set_q_def in auto)
   have "entails_\<G>_q q N {B}" using q_in entails_bot unfolding entails_\<G>_Q_def by simp
   then have ground_n_entails_bot: "entails_q q (\<G>_set_q q N) (\<G>_set_q q {B})"
     unfolding entails_\<G>_q_def .
   interpret static_refutational_complete_calculus Bot_G "Inf_G_q q" "entails_q q" "Red_Inf_q q"
     "Red_F_q q"
     using stat_ref_G[rule_format, OF q_in] .
   obtain BG where bg_in: "BG \<in> \<G>_F_q q B"
     using lifted_q_calc.Bot_map_not_empty[OF b_in] by blast
   then have "BG \<in> Bot_G" using lifted_q_calc.Bot_map[OF b_in] by blast
   then have "\<exists>BG'\<in>Bot_G. BG' \<in> \<G>_set_q q N"
     using ground_sat_n ground_n_entails_bot static_refutational_complete[of BG, OF _ ground_sat_n]
-      bg_in lifted_q_calc.Ground.entail_set_all_formulas[of "\<G>_set_q q N" "\<G>_set_q q {B}"]
+      bg_in lifted_q_calc.ground.entail_set_all_formulas[of "\<G>_set_q q N" "\<G>_set_q q {B}"]
     unfolding \<G>_set_q_def by simp
   then show "\<exists>B'\<in> Bot_F. B' \<in> N" using lifted_q_calc.Bot_cond unfolding \<G>_set_q_def by blast
 qed
 
 (* lem:intersect-saturation-indep-of-sqsubset *)
-lemma sat_eq_sat_empty_order: "lifted_calc_w_red_crit_family.inter_red_crit_calculus.saturated N =
-  empty_ord_lifted_calc_w_red_crit_family.inter_red_crit_calculus.saturated N"
+lemma sat_eq_sat_empty_order: "lifted_calc_w_red_crit_family.saturated N =
+  empty_ord_lifted_calc_w_red_crit_family.saturated N"
   by (rule refl)
 
 (* lem:intersect-static-ref-compl-indep-of-sqsubset *)
 lemma static_empty_ord_inter_equiv_static_inter:
   "static_refutational_complete_calculus Bot_F Inf_F lifted_calc_w_red_crit_family.entails_Q
     lifted_calc_w_red_crit_family.Red_Inf_Q lifted_calc_w_red_crit_family.Red_F_Q =
   static_refutational_complete_calculus Bot_F Inf_F lifted_calc_w_red_crit_family.entails_Q
     empty_ord_lifted_calc_w_red_crit_family.Red_Inf_Q empty_ord_lifted_calc_w_red_crit_family.Red_F_Q"
   unfolding static_refutational_complete_calculus_def
-  by (simp add: empty_ord_lifted_calc_w_red_crit_family.inter_red_crit_calculus.calculus_with_red_crit_axioms
-    lifted_calc_w_red_crit_family.inter_red_crit_calculus.calculus_with_red_crit_axioms)
+  by (simp add: empty_ord_lifted_calc_w_red_crit_family.calculus_with_red_crit_axioms
+    lifted_calc_w_red_crit_family.calculus_with_red_crit_axioms)
 
 (* thm:intersect-static-ref-compl-is-dyn-ref-compl-with-order *)
 theorem stat_eq_dyn_ref_comp_fam_inter: "static_refutational_complete_calculus Bot_F Inf_F lifted_calc_w_red_crit_family.entails_Q
     empty_ord_lifted_calc_w_red_crit_family.Red_Inf_Q empty_ord_lifted_calc_w_red_crit_family.Red_F_Q =
   dynamic_refutational_complete_calculus Bot_F Inf_F lifted_calc_w_red_crit_family.entails_Q
     lifted_calc_w_red_crit_family.Red_Inf_Q lifted_calc_w_red_crit_family.Red_F_Q"  (is "?static = ?dynamic")
 proof
   assume ?static
   then have static_general: "static_refutational_complete_calculus Bot_F Inf_F
     lifted_calc_w_red_crit_family.entails_Q lifted_calc_w_red_crit_family.Red_Inf_Q
     lifted_calc_w_red_crit_family.Red_F_Q" (is "?static_gen")
     using static_empty_ord_inter_equiv_static_inter
     by simp
   interpret static_refutational_complete_calculus Bot_F Inf_F lifted_calc_w_red_crit_family.entails_Q
     lifted_calc_w_red_crit_family.Red_Inf_Q lifted_calc_w_red_crit_family.Red_F_Q
     using static_general .
   show "?dynamic" by standard
 next
   assume dynamic_gen: ?dynamic
   interpret dynamic_refutational_complete_calculus Bot_F Inf_F lifted_calc_w_red_crit_family.entails_Q
     lifted_calc_w_red_crit_family.Red_Inf_Q lifted_calc_w_red_crit_family.Red_F_Q
     using dynamic_gen .
   have "static_refutational_complete_calculus Bot_F Inf_F lifted_calc_w_red_crit_family.entails_Q
     lifted_calc_w_red_crit_family.Red_Inf_Q lifted_calc_w_red_crit_family.Red_F_Q"
     by standard
   then show "?static" using static_empty_ord_inter_equiv_static_inter by simp
 qed
 
 end
 
 end
diff --git a/thys/Saturation_Framework/Prover_Architectures.thy b/thys/Saturation_Framework/Prover_Architectures.thy
--- a/thys/Saturation_Framework/Prover_Architectures.thy
+++ b/thys/Saturation_Framework/Prover_Architectures.thy
@@ -1,1219 +1,1215 @@
 (*  Title:       Prover Architectures of the Saturation Framework
  *  Author:      Sophie Tourret <stourret at mpi-inf.mpg.de>, 2019-2020 *)
 
 section \<open>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 Prover_Architectures
   imports
     Lambda_Free_RPOs.Lambda_Free_Util
     Labeled_Lifting_to_Non_Ground_Calculi
 begin
 
 subsection \<open>Basis of the Prover Architectures\<close>
 
 locale Prover_Architecture_Basis = labeled_lifting_with_red_crit_family Bot_F Inf_F Bot_G Q
   entails_q Inf_G_q Red_Inf_q Red_F_q \<G>_F_q \<G>_Inf_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_Inf_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>_Inf_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)
   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
     static_ref_comp: "static_refutational_complete_calculus Bot_F Inf_F (\<Turnstile>\<inter>\<G>)
       no_labels.empty_ord_lifted_calc_w_red_crit_family.Red_Inf_Q
       no_labels.empty_ord_lifted_calc_w_red_crit_family.Red_F_Q"
 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
 
 lemma labeled_static_ref_comp:
   "static_refutational_complete_calculus Bot_FL Inf_FL (\<Turnstile>\<inter>\<G>L) with_labels.Red_Inf_Q with_labels.Red_F_Q"
   using labeled_static_ref[OF static_ref_comp] .
 
 lemma standard_labeled_lifting_family:
   assumes q_in: "q \<in> Q"
   shows "lifting_with_wf_ordering_family Bot_FL Inf_FL Bot_G
     (entails_q q) (Inf_G_q q) (Red_Inf_q q) (Red_F_q q) (\<G>_F_L_q q) (\<G>_Inf_L_q q) (\<lambda>g. Prec_FL)"
 proof -
   have "lifting_with_wf_ordering_family Bot_FL Inf_FL Bot_G (entails_q q) (Inf_G_q q)
     (Red_Inf_q q) (Red_F_q q) (\<G>_F_L_q q) (\<G>_Inf_L_q q) (\<lambda>g. Labeled_Empty_Order)"
     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_Inf_q q)
     (Red_F_q q) (\<G>_F_L_q q) (\<G>_Inf_L_q q)"
     using lifted_q[OF q_in] by blast
   then show "lifting_with_wf_ordering_family Bot_FL Inf_FL Bot_G (entails_q q) (Inf_G_q q)
     (Red_Inf_q q) (Red_F_q q) (\<G>_F_L_q q) (\<G>_Inf_L_q q) (\<lambda>g. Prec_FL)"
     using wf_prec_FL
     by (simp add: lifting_with_wf_ordering_family.intro lifting_with_wf_ordering_family_axioms.intro)
 qed
 
 sublocale standard_lifting_with_red_crit_family Inf_FL Bot_G Q Inf_G_q entails_q Red_Inf_q Red_F_q
   Bot_FL \<G>_F_L_q \<G>_Inf_L_q "\<lambda>g. Prec_FL"
-  using standard_labeled_lifting_family
-    no_labels.Ground_family.calculus_family_with_red_crit_family_axioms
+  using standard_labeled_lifting_family no_labels.ground.calculus_family_with_red_crit_family_axioms
   by (simp add: standard_lifting_with_red_crit_family.intro
     standard_lifting_with_red_crit_family_axioms.intro)
 
 lemma entail_equiv: "lifted_calc_w_red_crit_family.entails_Q N1 N2 \<longleftrightarrow> (N1 \<Turnstile>\<inter>\<G>L N2)"
   unfolding lifted_calc_w_red_crit_family.entails_Q_def entails_\<G>_L_Q_def entails_\<G>_L_q_def
     entails_\<G>_q_def \<G>_set_q_def \<G>_set_L_q_def
   by simp
 
 lemma entail_equiv2: "lifted_calc_w_red_crit_family.entails_Q = (\<Turnstile>\<inter>\<G>L)"
   using entail_equiv by auto
 
 lemma red_inf_equiv: "empty_ord_lifted_calc_w_red_crit_family.Red_Inf_Q N = with_labels.Red_Inf_Q N"
   unfolding lifted_calc_w_red_crit_family.Red_Inf_Q_def with_labels.Red_Inf_Q_def Red_Inf_\<G>_q_def
     Red_Inf_\<G>_L_q_def \<G>_set_q_def \<G>_set_L_q_def
   by simp
 
 lemma red_inf_equiv2: "empty_ord_lifted_calc_w_red_crit_family.Red_Inf_Q = with_labels.Red_Inf_Q"
   using red_inf_equiv by auto
 
 lemma empty_red_f_equiv: "empty_ord_lifted_calc_w_red_crit_family.Red_F_Q N = with_labels.Red_F_Q N"
   unfolding empty_ord_lifted_calc_w_red_crit_family.Red_F_Q_def with_labels.Red_F_Q_def
     Red_F_\<G>_empty_q_def Red_F_\<G>_empty_L_q_def \<G>_set_q_def \<G>_set_L_q_def
   by simp
 
 lemma empty_red_f_equiv2: "empty_ord_lifted_calc_w_red_crit_family.Red_F_Q = with_labels.Red_F_Q"
   using empty_red_f_equiv by auto
 
 sublocale static_refutational_complete_calculus Bot_FL Inf_FL
   lifted_calc_w_red_crit_family.entails_Q lifted_calc_w_red_crit_family.Red_Inf_Q
   lifted_calc_w_red_crit_family.Red_F_Q
   using static_empty_ord_inter_equiv_static_inter empty_red_f_equiv2 red_inf_equiv2 entail_equiv2
     labeled_static_ref_comp
   by argo
 
 (* lem:redundant-labeled-inferences *)
 lemma labeled_red_inf_eq_red_inf:
   assumes i_in: "\<iota> \<in> Inf_FL"
   shows "\<iota> \<in> lifted_calc_w_red_crit_family.Red_Inf_Q N \<longleftrightarrow>
     to_F \<iota> \<in> no_labels.empty_ord_lifted_calc_w_red_crit_family.Red_Inf_Q (fst ` N)"
 proof -
   have "\<iota> \<in> lifted_calc_w_red_crit_family.Red_Inf_Q N \<Longrightarrow>
     to_F \<iota> \<in> no_labels.empty_ord_lifted_calc_w_red_crit_family.Red_Inf_Q (fst ` N)"
   proof -
     assume i_in2: "\<iota> \<in> lifted_calc_w_red_crit_family.Red_Inf_Q N"
     then have "X \<in> Red_Inf_\<G>_q ` Q \<Longrightarrow> \<iota> \<in> X N" for X
       unfolding lifted_calc_w_red_crit_family.Red_Inf_Q_def by blast
     obtain X0 where "X0 \<in> Red_Inf_\<G>_q ` Q"
       using with_labels.Q_nonempty by blast
     then obtain q0 where x0_is: "X0 N = Red_Inf_\<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_Inf_\<G>_q q0 (fst ` N)"
       unfolding  y0_is
     proof
       show "to_F ` X0 N \<subseteq> no_labels.Red_Inf_\<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_Inf_\<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>_Inf_L_q q0 \<iota>0_FL) \<noteq> None \<and>
             the (\<G>_Inf_L_q q0 \<iota>0_FL) \<subseteq> Red_Inf_q q0 (\<G>_set_q q0 N))
             \<or> ((\<G>_Inf_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_Inf_\<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>_Inf_q q0 \<iota>0 \<noteq> None" and
             "the (\<G>_Inf_q q0 \<iota>0) \<noteq> {}"
           then obtain \<iota>1 where i1_in: "\<iota>1 \<in> the (\<G>_Inf_q q0 \<iota>0)" by blast
           have "the (\<G>_Inf_q q0 \<iota>0) \<subseteq> Red_Inf_q q0 (no_labels.\<G>_set_q q0 (fst ` N))"
             using subs1 i0_to_i0_FL not_none
             unfolding no_labels.\<G>_set_q_def \<G>_set_q_def \<G>_Inf_L_q_def \<G>_F_L_q_def by auto
         }
         moreover {
           assume
             is_none: "\<G>_Inf_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
             unfolding no_labels.\<G>_set_q_def \<G>_set_q_def \<G>_Inf_L_q_def \<G>_F_L_q_def by simp
         }
         ultimately show "\<iota>0 \<in> no_labels.Red_Inf_\<G>_q q0 (fst ` N)"
           unfolding no_labels.Red_Inf_\<G>_q_def using i0_in3 by auto
        qed
      next
        show "no_labels.Red_Inf_\<G>_q q0 (fst ` N) \<subseteq> to_F ` X0 N"
        proof
          fix \<iota>0
          assume i0_in: "\<iota>0 \<in> no_labels.Red_Inf_\<G>_q q0 (fst ` N)"
          then have i0_in2: "\<iota>0 \<in> Inf_F"
            unfolding no_labels.Red_Inf_\<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>_Inf_L_q q0 \<iota>0_FL) \<noteq> None \<and>
            the (\<G>_Inf_L_q q0 \<iota>0_FL) \<subseteq> Red_Inf_q q0 (\<G>_set_q q0 N))
            \<or> ((\<G>_Inf_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_Inf_\<G>_q_def \<G>_Inf_L_q_def no_labels.\<G>_set_q_def \<G>_set_q_def
              \<G>_F_L_q_def
            by simp
          then have "\<iota>0_FL \<in> Red_Inf_\<G>_q q0 N"
            using i0_FL_in unfolding Red_Inf_\<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_Inf_\<G>_q ` Q \<Longrightarrow> (to_F \<iota>) \<in> Y (fst ` N)" for Y
       using i_in2 no_labels.lifted_calc_w_red_crit_family.Red_Inf_Q_def
         red_inf_equiv2 red_inf_impl by fastforce
     then show "to_F \<iota> \<in> no_labels.empty_ord_lifted_calc_w_red_crit_family.Red_Inf_Q (fst ` N)"
       unfolding lifted_calc_w_red_crit_family.Red_Inf_Q_def
         no_labels.empty_ord_lifted_calc_w_red_crit_family.Red_Inf_Q_def
       by blast
     qed
   moreover have "(to_F \<iota>) \<in> no_labels.empty_ord_lifted_calc_w_red_crit_family.Red_Inf_Q (fst ` N) \<Longrightarrow>
     \<iota> \<in> lifted_calc_w_red_crit_family.Red_Inf_Q N"
   proof -
     assume to_F_in: "to_F \<iota> \<in> no_labels.empty_ord_lifted_calc_w_red_crit_family.Red_Inf_Q (fst ` N)"
     have imp_to_F: "X \<in> no_labels.Red_Inf_\<G>_q ` Q \<Longrightarrow> to_F \<iota> \<in> X (fst ` N)" for X
       using to_F_in unfolding no_labels.empty_ord_lifted_calc_w_red_crit_family.Red_Inf_Q_def
       by blast
     then have to_F_in2: "to_F \<iota> \<in> no_labels.Red_Inf_\<G>_q q (fst ` N)" if "q \<in> Q" for q
       using that by auto
     have "Red_Inf_\<G>_q q N = {\<iota>0_FL \<in> Inf_FL. to_F \<iota>0_FL \<in> no_labels.Red_Inf_\<G>_q q (fst ` N)}" for q
     proof
       show "Red_Inf_\<G>_q q N \<subseteq> {\<iota>0_FL \<in> Inf_FL. to_F \<iota>0_FL \<in> no_labels.Red_Inf_\<G>_q q (fst ` N)}"
       proof
         fix q0 \<iota>1
         assume
           i1_in: "\<iota>1 \<in> Red_Inf_\<G>_q q0 N"
         have i1_in2: "\<iota>1 \<in> Inf_FL"
           using i1_in unfolding Red_Inf_\<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_Inf_\<G>_q q0 (fst ` N)"
           using i1_in to_F_i1_in
           unfolding Red_Inf_\<G>_q_def no_labels.Red_Inf_\<G>_q_def \<G>_Inf_L_q_def \<G>_set_q_def
             no_labels.\<G>_set_q_def \<G>_F_L_q_def
           by force
         show "\<iota>1 \<in> {\<iota>0_FL \<in> Inf_FL. to_F \<iota>0_FL \<in> no_labels.Red_Inf_\<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_Inf_\<G>_q q (fst ` N)} \<subseteq> Red_Inf_\<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_Inf_\<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>_Inf_L_q q0 \<iota>1) \<noteq> None \<and>
           the (\<G>_Inf_L_q q0 \<iota>1) \<subseteq> Red_Inf_q q0 (\<G>_set_q q0 N))
           \<or> ((\<G>_Inf_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_Inf_\<G>_q_def \<G>_Inf_L_q_def \<G>_set_q_def
             no_labels.\<G>_set_q_def \<G>_F_L_q_def
           by auto
         then show "\<iota>1 \<in> Red_Inf_\<G>_q q0 N"
           using i1_in2 unfolding Red_Inf_\<G>_q_def by blast
       qed
     qed
     then have "\<iota> \<in> Red_Inf_\<G>_q q N" if "q \<in> Q" for q
       using that to_F_in2 i_in
       unfolding Red_Inf_\<G>_q_def no_labels.Red_Inf_\<G>_q_def \<G>_Inf_L_q_def \<G>_set_q_def
         no_labels.\<G>_set_q_def \<G>_F_L_q_def
       by auto
     then show "\<iota> \<in> empty_ord_lifted_calc_w_red_crit_family.Red_Inf_Q N"
       unfolding empty_ord_lifted_calc_w_red_crit_family.Red_Inf_Q_def by blast
   qed
   ultimately show ?thesis
     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> lifted_calc_w_red_crit_family.Red_F_Q N\<close>
 proof -
   note assms
   moreover have i: \<open>C \<in> no_labels.Red_F_\<G>_empty (fst ` N) \<Longrightarrow>
     (C, L) \<in> lifted_calc_w_red_crit_family.Red_F_Q 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 "no_labels.\<G>_set_q q (fst ` N) = \<G>_set_q q N" for q
       unfolding no_labels.\<G>_set_q_def \<G>_set_q_def \<G>_F_L_q_def by simp
     then 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 unfolding \<G>_F_L_q_def by simp
     then show ?thesis
       unfolding lifted_calc_w_red_crit_family.Red_F_Q_def Red_F_\<G>_q_g_def by blast
   qed
   moreover have ii: \<open>\<exists>C' \<in> fst ` N. C' \<prec>\<cdot> C \<Longrightarrow> (C, L) \<in> lifted_calc_w_red_crit_family.Red_F_Q 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
       unfolding no_labels.\<G>_set_q_def \<G>_set_q_def \<G>_F_L_q_def
       using that by auto
     then have "(C, L) \<in> Red_F_\<G>_q_g q N" if "q \<in> Q" for q
       unfolding Red_F_\<G>_q_g_def using that c'_l'_in c'_l'_prec by blast
     then show ?thesis
       unfolding lifted_calc_w_red_crit_family.Red_F_Q_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> lifted_calc_w_red_crit_family.Red_F_Q 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> lifted_calc_w_red_crit_family.Red_F_Q 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
         unfolding no_labels.\<G>_set_q_def \<G>_set_q_def \<G>_F_L_q_def using that by auto
       then have "(C, L) \<in> Red_F_\<G>_q_g q N" if "q \<in> Q" for q
         unfolding Red_F_\<G>_q_g_def using that c'_l'_in c'_l'_prec by blast
       then have ?thesis
         unfolding lifted_calc_w_red_crit_family.Red_F_Q_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 Architecture\<close>
 
 locale Given_Clause = Prover_Architecture_Basis Bot_F Inf_F Bot_G Q entails_q Inf_G_q Red_Inf_q
   Red_F_q \<G>_F_q \<G>_Inf_q Inf_FL Equiv_F Prec_F Prec_l
   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_Inf_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>_Inf_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)
   + fixes
     active :: "'l"
   assumes
     inf_have_prems: "\<iota>F \<in> Inf_F \<Longrightarrow> prems_of \<iota>F \<noteq> []" 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"
 begin
 
 lemma labeled_inf_have_prems: "\<iota> \<in> Inf_FL \<Longrightarrow> set (prems_of \<iota>) \<noteq> {}"
   using inf_have_prems Inf_FL_to_Inf_F by fastforce
 
 definition active_subset :: "('f \<times> 'l) set \<Rightarrow> ('f \<times> 'l) set" where
   "active_subset M = {CL \<in> M. snd CL = active}"
 
 definition non_active_subset :: "('f \<times> 'l) set \<Rightarrow> ('f \<times> 'l) set" where
   "non_active_subset M = {CL \<in> M. snd CL \<noteq> active}"
 
 inductive step :: "('f \<times> 'l) set \<Rightarrow> ('f \<times> 'l) set \<Rightarrow> bool" (infix "\<Longrightarrow>GC" 50) where
   process: "N1 = N \<union> M \<Longrightarrow> N2 = N \<union> M' \<Longrightarrow>
     M \<subseteq> lifted_calc_w_red_crit_family.Red_F_Q (N \<union> M') \<Longrightarrow>
     active_subset M' = {} \<Longrightarrow> N1 \<Longrightarrow>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.Non_ground.Inf_from2 (fst ` (active_subset N)) {C} \<subseteq>
-      no_labels.lifted_calc_w_red_crit_family.Red_Inf_Q (fst ` (N \<union> {(C, active)} \<union> M)) \<Longrightarrow>
+    no_labels.Inf_from2 (fst ` (active_subset N)) {C}
+    \<subseteq> no_labels.lifted_calc_w_red_crit_family.Red_Inf_Q (fst ` (N \<union> {(C, active)} \<union> M)) \<Longrightarrow>
     N1 \<Longrightarrow>GC N2"
 
 notation lifted_calc_w_red_crit.derive (infix "\<rhd>RedL" 50)
 
 lemma derive_equiv:
-  "(\<rhd>RedL) = lifted_calc_w_red_crit_family.inter_red_crit_calculus.derive"
+  "(\<rhd>RedL) = lifted_calc_w_red_crit_family.derive"
   unfolding lifted_calc_w_red_crit.derive.simps
-    lifted_calc_w_red_crit_family.inter_red_crit_calculus.derive.simps Red_F_\<G>_g_def
+    lifted_calc_w_red_crit_family.derive.simps Red_F_\<G>_g_def
     lifted_calc_w_red_crit_family.Red_F_Q_def
   by (rule refl)
 
 lemma one_step_equiv: "N1 \<Longrightarrow>GC N2 \<Longrightarrow> N1 \<rhd>RedL N2"
 proof (cases N1 N2 rule: step.cases)
   show "N1 \<Longrightarrow>GC N2 \<Longrightarrow> N1 \<Longrightarrow>GC N2" by blast
 next
   fix N M M'
   assume
     gc_step: "N1 \<Longrightarrow>GC N2" and
     n1_is: "N1 = N \<union> M" and
     n2_is: "N2 = N \<union> M'" and
     m_red: "M \<subseteq> lifted_calc_w_red_crit_family.Red_F_Q (N \<union> M')" and
     active_empty: "active_subset M' = {}"
   have "N1 - N2 \<subseteq> lifted_calc_w_red_crit_family.Red_F_Q N2"
     using n1_is n2_is m_red by auto
   then show "N1 \<rhd>RedL N2"
-    unfolding derive_equiv lifted_calc_w_red_crit_family.inter_red_crit_calculus.derive.simps
-    by blast
+    unfolding derive_equiv lifted_calc_w_red_crit_family.derive.simps by blast
 next
   fix N C L M
   assume
     gc_step: "N1 \<Longrightarrow>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> lifted_calc_w_red_crit_family.Red_F_Q 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> lifted_calc_w_red_crit_family.Red_F_Q N2"
     using empty_red_f_equiv[of N2] by blast
   then show "N1 \<rhd>RedL N2"
-    unfolding derive_equiv lifted_calc_w_red_crit_family.inter_red_crit_calculus.derive.simps
-    by blast
+    unfolding derive_equiv lifted_calc_w_red_crit_family.derive.simps by blast
 qed
 
 (* lem:gc-derivations-are-red-derivations *)
 lemma gc_to_red: "chain (\<Longrightarrow>GC) D \<Longrightarrow> chain (\<rhd>RedL) D"
   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 (\<Longrightarrow>GC) D" and
     init_state: "active_subset (lnth D 0) = {}" and
     final_state: "non_active_subset (Liminf_llist D) = {}"
-  shows "with_labels.inter_red_crit_calculus.fair D"
-  unfolding with_labels.inter_red_crit_calculus.fair_def
+  shows "with_labels.fair D"
+  unfolding with_labels.fair_def
 proof
   fix \<iota>
   assume i_in: "\<iota> \<in> with_labels.Inf_from (Liminf_llist D)"
   have i_in_inf_fl: "\<iota> \<in> Inf_FL" using i_in unfolding with_labels.Inf_from_def by blast
   have "Liminf_llist D = active_subset (Liminf_llist D)"
     using final_state unfolding non_active_subset_def active_subset_def by blast
   then have i_in2: "\<iota> \<in> with_labels.Inf_from (active_subset (Liminf_llist D))" 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 with_labels.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 D \<and>
-      (prems_of \<iota>)!j \<notin> active_subset (lnth D nj) \<and>
-      (\<forall>k. k > nj \<longrightarrow> enat k < llength D \<longrightarrow> (prems_of \<iota>)!j \<in> active_subset (lnth D k)))"
+      prems_of \<iota> ! j \<notin> active_subset (lnth D nj) \<and>
+      (\<forall>k. k > nj \<longrightarrow> enat k < llength D \<longrightarrow> prems_of \<iota> ! j \<in> active_subset (lnth D k)))"
   proof clarify
     fix j
     assume j_in: "j \<in> {0..<m}"
-    then obtain C where c_is: "(C, active) = (prems_of \<iota>)!j"
+    then obtain C where c_is: "(C, active) = prems_of \<iota> ! j"
       using i_in2 unfolding m_def with_labels.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 D"
       using j_in i_in unfolding m_def with_labels.Inf_from_def by force
     then obtain nj where nj_is: "enat nj < llength D" and
       c_in2: "(C, active) \<in> \<Inter> (lnth D ` {k. nj \<le> k \<and> enat k < llength D})"
       unfolding Liminf_llist_def using init_state by blast
     then have c_in3: "\<forall>k. k \<ge> nj \<longrightarrow> enat k < llength D \<longrightarrow> (C, active) \<in> (lnth D k)" by blast
     have nj_pos: "nj > 0" using init_state c_in2 nj_is unfolding active_subset_def by fastforce
     obtain nj_min where nj_min_is: "nj_min = (LEAST nj. enat nj < llength D \<and>
         (C, active) \<in> \<Inter> (lnth D ` {k. nj \<le> k \<and> enat k < llength D}))" by blast
     then have in_allk: "\<forall>k. k \<ge> nj_min \<longrightarrow> enat k < llength D \<longrightarrow> (C, active) \<in> (lnth D 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 D"
       using nj_min_is
       by (smt LeastI_ex \<open>\<And>thesis. (\<And>nj. \<lbrakk>enat nj < llength D;
           (C, active) \<in> \<Inter> (lnth D ` {k. nj \<le> k \<and> enat k < llength D})\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis\<close>)
     have "nj_min > 0"
       using nj_is c_in2 nj_pos nj_min_is
       by (metis (mono_tags, lifting) Collect_empty_eq \<open>(C, active) \<in> Liminf_llist D\<close>
           \<open>Liminf_llist D = active_subset (Liminf_llist D)\<close>
           \<open>\<forall>k\<ge>nj_min. enat k < llength D \<longrightarrow> (C, active) \<in> lnth D 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 D"
       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 D \<longrightarrow> (C, active) \<in> lnth D k"
       using nj_prec_is in_allk by simp
     have notin_njm_prec: "(C, active) \<notin> lnth D njm_prec"
     proof (rule ccontr)
       assume "\<not> (C, active) \<notin> lnth D njm_prec"
       then have absurd_hyp: "(C, active) \<in> lnth D njm_prec" by simp
       have prec_smaller: "enat njm_prec < llength D" using nj_min_is nj_prec_is
         by (smt LeastI_ex Suc_leD \<open>\<And>thesis. (\<And>nj. \<lbrakk>enat nj < llength D;
             (C, active) \<in> \<Inter> (lnth D ` {k. nj \<le> k \<and> enat k < llength D})\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis\<close>
             enat_ord_simps(1) le_eq_less_or_eq le_less_trans)
       have "(C, active) \<in> \<Inter> (lnth D ` {k. njm_prec \<le> k \<and> enat k < llength D})"
       proof -
         {
           fix k
           assume k_in: "njm_prec \<le> k \<and> enat k < llength D"
           have "k = njm_prec \<Longrightarrow> (C, active) \<in> lnth D k" using absurd_hyp by simp
           moreover have "njm_prec < k \<Longrightarrow> (C, active) \<in> lnth D k"
             using nj_prec_is in_allk k_in by simp
           ultimately have "(C, active) \<in> lnth D k" using k_in by fastforce
         }
         then show "(C, active) \<in> \<Inter> (lnth D ` {k. njm_prec \<le> k \<and> enat k < llength D})" by blast
       qed
       then have "enat njm_prec < llength D \<and>
           (C, active) \<in> \<Inter> (lnth D ` {k. njm_prec \<le> k \<and> enat k < llength D})"
         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 D njm_prec)"
       unfolding active_subset_def by blast
-    then show "\<exists>nj. enat (Suc nj) < llength D \<and> (prems_of \<iota>)!j \<notin> active_subset (lnth D nj) \<and>
-        (\<forall>k. k > nj \<longrightarrow> enat k < llength D \<longrightarrow> (prems_of \<iota>)!j \<in> active_subset (lnth D k))"
+    then show "\<exists>nj. enat (Suc nj) < llength D \<and> prems_of \<iota> ! j \<notin> active_subset (lnth D nj) \<and>
+        (\<forall>k. k > nj \<longrightarrow> enat k < llength D \<longrightarrow> prems_of \<iota> ! j \<in> active_subset (lnth D 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 D \<and>
-      (prems_of \<iota>)!j \<notin> active_subset (lnth D nj) \<and>
-      (\<forall>k. k > nj \<longrightarrow> enat k < llength D \<longrightarrow> (prems_of \<iota>)!j \<in> active_subset (lnth D k)))}"
+      prems_of \<iota> ! j \<notin> active_subset (lnth D nj) \<and>
+      (\<forall>k. k > nj \<longrightarrow> enat k < llength D \<longrightarrow> prems_of \<iota> ! j \<in> active_subset (lnth D 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 D" and
       "prems_of \<iota> ! 0 \<notin> active_subset (lnth D n0)" and
       "\<forall>k>n0. enat k < llength D \<longrightarrow> prems_of \<iota> ! 0 \<in> active_subset (lnth D 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 D" and
-    j0_notin: "(prems_of \<iota>)!j0 \<notin> active_subset (lnth D n)" and
-    j0_allin: "(\<forall>k. k > n \<longrightarrow> enat k < llength D \<longrightarrow> (prems_of \<iota>)!j0 \<in> active_subset (lnth D k))"
+    j0_notin: "prems_of \<iota> ! j0 \<notin> active_subset (lnth D n)" and
+    j0_allin: "(\<forall>k. k > n \<longrightarrow> enat k < llength D \<longrightarrow> prems_of \<iota> ! j0 \<in> active_subset (lnth D k))"
     unfolding nj_set_def by blast
-  obtain C0 where C0_is: "(prems_of \<iota>)!j0 = (C0, active)" using j0_in
+  obtain C0 where C0_is: "prems_of \<iota> ! j0 = (C0, active)" using j0_in
     using i_in2 unfolding m_def with_labels.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 D (Suc n))"
     using C0_is j0_allin suc_n_length by (simp add: active_subset_def)
   have C0_notin: "(C0, active) \<notin> (lnth D n)" using C0_is j0_notin unfolding active_subset_def by simp
   have step_n: "lnth D n \<Longrightarrow>GC lnth D (Suc n)"
     using deriv chain_lnth_rel n_in unfolding nj_set_def by blast
   have "\<exists>N C L M. (lnth D n = N \<union> {(C, L)} \<and>
       lnth D (Suc n) = N \<union> {(C, active)} \<union> M \<and> L \<noteq> active \<and>
       active_subset M = {} \<and>
-      no_labels.Non_ground.Inf_from2 (fst ` (active_subset N)) {C} \<subseteq>
-      no_labels.lifted_calc_w_red_crit_family.Red_Inf_Q (fst ` (N \<union> {(C, active)} \<union> M)))"
+      no_labels.Inf_from2 (fst ` (active_subset N)) {C}
+      \<subseteq> no_labels.lifted_calc_w_red_crit_family.Red_Inf_Q (fst ` (N \<union> {(C, active)} \<union> M)))"
   proof -
     have proc_or_infer: "(\<exists>N1 N M N2 M'. lnth D n = N1 \<and> lnth D (Suc n) = N2 \<and> N1 = N \<union> M \<and>
          N2 = N \<union> M' \<and>
          M \<subseteq> lifted_calc_w_red_crit_family.Red_F_Q (N \<union> M') \<and> active_subset M' = {}) \<or>
        (\<exists>N1 N C L N2 M. lnth D n = N1 \<and> lnth D (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.Non_ground.Inf_from2 (fst ` (active_subset N)) {C} \<subseteq>
+         no_labels.Inf_from2 (fst ` (active_subset N)) {C} \<subseteq>
            no_labels.lifted_calc_w_red_crit_family.Red_Inf_Q (fst ` (N \<union> {(C, active)} \<union> M)))"
       using step.simps[of "lnth D n" "lnth D (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.Non_ground.Inf_from2 (fst ` (active_subset N)) {C0} \<subseteq>
-      no_labels.lifted_calc_w_red_crit_family.Red_Inf_Q (fst ` (N \<union> {(C0, active)} \<union> M))" and
+    "no_labels.Inf_from2 (fst ` (active_subset N)) {C0}
+     \<subseteq> no_labels.lifted_calc_w_red_crit_family.Red_Inf_Q (fst ` (N \<union> {(C0, active)} \<union> M))" and
     nth_d_is: "lnth D n = N \<union> {(C0, L)}" and
     suc_nth_d_is: "lnth D (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
+  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"
+      j_not_j0: "prems_of \<iota> ! j \<noteq> prems_of \<iota> ! j0"
     obtain nj where nj_len: "enat (Suc nj) < llength D" and
-      nj_prems: "(prems_of \<iota>)!j \<notin> active_subset (lnth D nj)" and
-      nj_greater: "(\<forall>k. k > nj \<longrightarrow> enat k < llength D \<longrightarrow> (prems_of \<iota>)!j \<in> active_subset (lnth D k))"
+      nj_prems: "prems_of \<iota> ! j \<notin> active_subset (lnth D nj)" and
+      nj_greater: "(\<forall>k. k > nj \<longrightarrow> enat k < llength D \<longrightarrow> prems_of \<iota> ! j \<in> active_subset (lnth D 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)"
+      then have "prems_of \<iota> ! j = (C0, active)"
         using C0_in C0_notin step.simps[of "lnth D n" "lnth D (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 D n))"
+    then have "prems_of \<iota> ! j \<in> (active_subset (lnth D 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)"
+    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> with_labels.Inf_from2 (active_subset N) {(C0, active)}"
     using i_in_inf_fl unfolding with_labels.Inf_from2_def with_labels.Inf_from_def by blast
-  then have "to_F \<iota> \<in> no_labels.Non_ground.Inf_from2 (fst ` (active_subset N)) {C0}"
+  then have "to_F \<iota> \<in> no_labels.Inf_from2 (fst ` (active_subset N)) {C0}"
     unfolding to_F_def with_labels.Inf_from2_def with_labels.Inf_from_def
-      no_labels.Non_ground.Inf_from2_def no_labels.Non_ground.Inf_from_def using Inf_FL_to_Inf_F
+      no_labels.Inf_from2_def no_labels.Inf_from_def using Inf_FL_to_Inf_F
     by force
   then have "to_F \<iota> \<in> no_labels.lifted_calc_w_red_crit_family.Red_Inf_Q (fst ` (lnth D (Suc n)))"
     using suc_nth_d_is inf_from_subs by fastforce
   then have "\<forall>q \<in> Q. (\<G>_Inf_q q (to_F \<iota>) \<noteq> None \<and>
       the (\<G>_Inf_q q (to_F \<iota>)) \<subseteq> Red_Inf_q q (\<Union> (\<G>_F_q q ` fst ` lnth D (Suc n))))
       \<or> (\<G>_Inf_q q (to_F \<iota>) = None \<and>
       \<G>_F_q q (concl_of (to_F \<iota>)) \<subseteq> \<Union> (\<G>_F_q q ` fst ` lnth D (Suc n)) \<union>
         Red_F_q q (\<Union> (\<G>_F_q q ` fst ` lnth D (Suc n))))"
     unfolding to_F_def no_labels.lifted_calc_w_red_crit_family.Red_Inf_Q_def
       no_labels.Red_Inf_\<G>_q_def no_labels.\<G>_set_q_def
       by blast
   then have "\<iota> \<in> with_labels.Red_Inf_Q (lnth D (Suc n))"
     unfolding to_F_def with_labels.Red_Inf_Q_def Red_Inf_\<G>_L_q_def \<G>_Inf_L_q_def \<G>_set_L_q_def
       \<G>_F_L_q_def using i_in_inf_fl by auto
-  then show "\<iota> \<in> with_labels.inter_red_crit_calculus.Sup_Red_Inf_llist D"
-    unfolding with_labels.inter_red_crit_calculus.Sup_Red_Inf_llist_def using suc_n_length by auto
+  then show "\<iota> \<in> with_labels.Sup_Red_Inf_llist D"
+    unfolding with_labels.Sup_Red_Inf_llist_def using suc_n_length by auto
 qed
 
 (* thm:gc-completeness *)
 theorem gc_complete:
   assumes
     deriv: "chain (\<Longrightarrow>GC) D" and
     init_state: "active_subset (lnth D 0) = {}" and
     final_state: "non_active_subset (Liminf_llist D) = {}" and
     b_in: "B \<in> Bot_F" and
     bot_entailed: "no_labels.entails_\<G>_Q (fst ` (lnth D 0)) {B}"
   shows "\<exists>i. enat i < llength D \<and> (\<exists>BL \<in> Bot_FL. BL \<in> (lnth D i))"
 proof -
   have labeled_b_in: "(B, active) \<in> Bot_FL" unfolding Bot_FL_def using b_in by simp
   have labeled_bot_entailed: "entails_\<G>_L_Q (lnth D 0) {(B, active)}"
     using labeled_entailment_lifting bot_entailed by fastforce
-  have "with_labels.inter_red_crit_calculus.fair D" using gc_fair[OF deriv init_state final_state] .
+  have "with_labels.fair D" using gc_fair[OF deriv init_state final_state] .
   then have "\<exists>i \<in> {i. enat i < llength D}. \<exists>BL \<in> Bot_FL. BL \<in> lnth D i"
     using dynamic_refutational_complete labeled_b_in gc_to_red[OF deriv] labeled_bot_entailed
       entail_equiv red_inf_equiv2
     unfolding derive_equiv by auto
   then show ?thesis by blast
 qed
 
 end
 
 subsection \<open>Lazy Given Clause Architecture\<close>
 
 locale Lazy_Given_Clause = Prover_Architecture_Basis Bot_F Inf_F Bot_G Q entails_q Inf_G_q Red_Inf_q
   Red_F_q \<G>_F_q \<G>_Inf_q Inf_FL Equiv_F Prec_F Prec_l
   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_Inf_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>_Inf_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)
   + fixes
     active :: "'l"
   assumes
     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"
 begin
 
 definition active_subset :: "('f \<times> 'l) set \<Rightarrow> ('f \<times> 'l) set" where
   "active_subset M = {CL \<in> M. snd CL = active}"
 
 definition non_active_subset :: "('f \<times> 'l) set \<Rightarrow> ('f \<times> 'l) set" where
   "non_active_subset M = {CL \<in> M. snd CL \<noteq> active}"
 
 inductive step :: "'f inference set \<times> ('f \<times> 'l) set \<Rightarrow>
   'f inference set \<times> ('f \<times> 'l) set \<Rightarrow> bool" (infix "\<Longrightarrow>LGC" 50) where
   process: "N1 = N \<union> M \<Longrightarrow> N2 = N \<union> M' \<Longrightarrow>
     M \<subseteq> lifted_calc_w_red_crit_family.Red_F_Q (N \<union> M') \<Longrightarrow>
     active_subset M' = {} \<Longrightarrow> (T, N1) \<Longrightarrow>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.Non_ground.Inf_from2 (fst ` (active_subset N)) {C} \<Longrightarrow>
+    L \<noteq> active \<Longrightarrow> T' = no_labels.Inf_from2 (fst ` (active_subset N)) {C} \<Longrightarrow>
     (T1, N1) \<Longrightarrow>LGC (T2, N2)" |
   compute_infer: "T1 = T2 \<union> {\<iota>} \<Longrightarrow> N2 = N1 \<union> M \<Longrightarrow> active_subset M = {} \<Longrightarrow>
     \<iota> \<in> no_labels.lifted_calc_w_red_crit_family.Red_Inf_Q (fst ` (N1 \<union> M)) \<Longrightarrow>
     (T1, N1) \<Longrightarrow>LGC (T2, N2)" |
   delete_orphans: "T1 = T2 \<union> T' \<Longrightarrow>
-    T' \<inter> no_labels.Non_ground.Inf_from (fst ` (active_subset N)) = {} \<Longrightarrow> (T1, N) \<Longrightarrow>LGC (T2, N)"
+    T' \<inter> no_labels.Inf_from (fst ` (active_subset N)) = {} \<Longrightarrow> (T1, N) \<Longrightarrow>LGC (T2, N)"
 
-notation lifted_calc_w_red_crit_family.inter_red_crit_calculus.derive (infix "\<rhd>RedL" 50)
+notation lifted_calc_w_red_crit_family.derive (infix "\<rhd>RedL" 50)
 
-lemma premise_free_inf_always_from: "\<iota> \<in> Inf_F \<Longrightarrow> length (prems_of \<iota>) = 0 \<Longrightarrow>
-  \<iota> \<in> no_labels.Non_ground.Inf_from N"
-  unfolding no_labels.Non_ground.Inf_from_def by simp
+lemma premise_free_inf_always_from:
+  "\<iota> \<in> Inf_F \<Longrightarrow> length (prems_of \<iota>) = 0 \<Longrightarrow> \<iota> \<in> no_labels.Inf_from N"
+  unfolding no_labels.Inf_from_def by simp
 
 lemma one_step_equiv: "(T1, N1) \<Longrightarrow>LGC (T2, N2) \<Longrightarrow> N1 \<rhd>RedL N2"
 proof (cases "(T1, N1)" "(T2, N2)" rule: step.cases)
   show "(T1, N1) \<Longrightarrow>LGC (T2, N2) \<Longrightarrow> (T1, N1) \<Longrightarrow>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> lifted_calc_w_red_crit_family.Red_F_Q (N \<union> M')"
   have "N1 - N2 \<subseteq> lifted_calc_w_red_crit_family.Red_F_Q N2"
     using n1_is n2_is m_red by auto
   then show "N1 \<rhd>RedL N2"
-    unfolding lifted_calc_w_red_crit_family.inter_red_crit_calculus.derive.simps by blast
+    unfolding lifted_calc_w_red_crit_family.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> lifted_calc_w_red_crit_family.Red_F_Q N2"
     using red_labeled_clauses by blast
   then have "N1 - N2 \<subseteq> lifted_calc_w_red_crit_family.Red_F_Q N2"
     using empty_red_f_equiv[of N2] using n1_is n2_is by blast
   then show "N1 \<rhd>RedL N2"
-    unfolding lifted_calc_w_red_crit_family.inter_red_crit_calculus.derive.simps by blast
+    unfolding lifted_calc_w_red_crit_family.derive.simps by blast
 next
   fix M
   assume
     n2_is: "N2 = N1 \<union> M"
   have "N1 - N2 \<subseteq> lifted_calc_w_red_crit_family.Red_F_Q N2"
     using n2_is by blast
   then show "N1 \<rhd>RedL N2"
-    unfolding lifted_calc_w_red_crit_family.inter_red_crit_calculus.derive.simps by blast
+    unfolding lifted_calc_w_red_crit_family.derive.simps by blast
 next
   assume n2_is: "N2 = N1"
   have "N1 - N2 \<subseteq> lifted_calc_w_red_crit_family.Red_F_Q N2"
     using n2_is by blast
   then show "N1 \<rhd>RedL N2"
-    unfolding lifted_calc_w_red_crit_family.inter_red_crit_calculus.derive.simps by blast
+    unfolding lifted_calc_w_red_crit_family.derive.simps by blast
 qed
 
 (* lem:lgc-derivations-are-red-derivations *)
 lemma lgc_to_red: "chain (\<Longrightarrow>LGC) D \<Longrightarrow> chain (\<rhd>RedL) (lmap snd D)"
   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 (\<Longrightarrow>LGC) D" and
     init_state: "active_subset (snd (lnth D 0)) = {}" and
     final_state: "non_active_subset (Liminf_llist (lmap snd D)) = {}" and
     no_prems_init_active: "\<forall>\<iota> \<in> Inf_F. length (prems_of \<iota>) = 0 \<longrightarrow> \<iota> \<in> (fst (lnth D 0))" and
     final_schedule: "Liminf_llist (lmap fst D) = {}"
-  shows "with_labels.inter_red_crit_calculus.fair (lmap snd D)"
-  unfolding with_labels.inter_red_crit_calculus.fair_def
+  shows "with_labels.fair (lmap snd D)"
+  unfolding with_labels.fair_def
 proof
   fix \<iota>
   assume i_in: "\<iota> \<in> with_labels.Inf_from (Liminf_llist (lmap snd D))"
   have i_in_inf_fl: "\<iota> \<in> Inf_FL" using i_in unfolding with_labels.Inf_from_def by blast
   have "Liminf_llist (lmap snd D) = active_subset (Liminf_llist (lmap snd D))"
     using final_state unfolding non_active_subset_def active_subset_def by blast
   then have i_in2: "\<iota> \<in> with_labels.Inf_from (active_subset (Liminf_llist (lmap snd D)))"
     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 with_labels.Inf_from_def to_F_def by blast
   have exist_nj: "\<forall>j \<in> {0..<m}. (\<exists>nj. enat (Suc nj) < llength D \<and>
-      (prems_of \<iota>)!j \<notin> active_subset (snd (lnth D nj)) \<and>
-      (\<forall>k. k > nj \<longrightarrow> enat k < llength D \<longrightarrow> (prems_of \<iota>)!j \<in> active_subset (snd (lnth D k))))"
+      prems_of \<iota> ! j \<notin> active_subset (snd (lnth D nj)) \<and>
+      (\<forall>k. k > nj \<longrightarrow> enat k < llength D \<longrightarrow> prems_of \<iota> ! j \<in> active_subset (snd (lnth D k))))"
   proof clarify
     fix j
     assume j_in: "j \<in> {0..<m}"
-    then obtain C where c_is: "(C, active) = (prems_of \<iota>)!j"
+    then obtain C where c_is: "(C, active) = prems_of \<iota> ! j"
       using i_in2 unfolding m_def with_labels.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 D)"
       using j_in i_in unfolding m_def with_labels.Inf_from_def by force
     then obtain nj where nj_is: "enat nj < llength D" and
       c_in2: "(C, active) \<in> \<Inter> (snd ` (lnth D ` {k. nj \<le> k \<and> enat k < llength D}))"
       unfolding Liminf_llist_def using init_state by fastforce
     then have c_in3: "\<forall>k. k \<ge> nj \<longrightarrow> enat k < llength D \<longrightarrow> (C, active) \<in> snd (lnth D k)" by blast
     have nj_pos: "nj > 0" using init_state c_in2 nj_is unfolding active_subset_def by fastforce
     obtain nj_min where nj_min_is: "nj_min = (LEAST nj. enat nj < llength D \<and>
         (C, active) \<in> \<Inter> (snd ` (lnth D ` {k. nj \<le> k \<and> enat k < llength D})))" by blast
     then have in_allk: "\<forall>k. k \<ge> nj_min \<longrightarrow> enat k < llength D \<longrightarrow> (C, active) \<in> snd (lnth D 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 D"
       using nj_min_is
       by (smt LeastI_ex \<open>\<And>thesis. (\<And>nj. \<lbrakk>enat nj < llength D;
           (C, active) \<in> \<Inter> (snd ` (lnth D ` {k. nj \<le> k \<and> enat k < llength D}))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis\<close>)
     have "nj_min > 0"
       using nj_is c_in2 nj_pos nj_min_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 D"
       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 D \<longrightarrow> (C, active) \<in> snd (lnth D k)"
       using nj_prec_is in_allk by simp
     have notin_njm_prec: "(C, active) \<notin> snd (lnth D njm_prec)"
     proof (rule ccontr)
       assume "\<not> (C, active) \<notin> snd (lnth D njm_prec)"
       then have absurd_hyp: "(C, active) \<in> snd (lnth D njm_prec)" by simp
       have prec_smaller: "enat njm_prec < llength D" using nj_min_is nj_prec_is
         by (smt LeastI_ex Suc_leD \<open>\<And>thesis. (\<And>nj. \<lbrakk>enat nj < llength D;
             (C, active) \<in> \<Inter> (snd ` (lnth D ` {k. nj \<le> k \<and> enat k < llength D}))\<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 D ` {k. njm_prec \<le> k \<and> enat k < llength D}))"
       proof -
         {
           fix k
           assume k_in: "njm_prec \<le> k \<and> enat k < llength D"
           have "k = njm_prec \<Longrightarrow> (C, active) \<in> snd (lnth D k)" using absurd_hyp by simp
           moreover have "njm_prec < k \<Longrightarrow> (C, active) \<in> snd (lnth D k)"
             using nj_prec_is in_allk k_in by simp
           ultimately have "(C, active) \<in> snd (lnth D k)" using k_in by fastforce
         }
         then show "(C, active) \<in> \<Inter> (snd ` (lnth D ` {k. njm_prec \<le> k \<and> enat k < llength D}))"
           by blast
       qed
       then have "enat njm_prec < llength D \<and>
           (C, active) \<in> \<Inter> (snd ` (lnth D ` {k. njm_prec \<le> k \<and> enat k < llength D}))"
         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 D njm_prec))"
       unfolding active_subset_def by blast
-    then show "\<exists>nj. enat (Suc nj) < llength D \<and> (prems_of \<iota>)!j \<notin> active_subset (snd (lnth D nj)) \<and>
-        (\<forall>k. k > nj \<longrightarrow> enat k < llength D \<longrightarrow> (prems_of \<iota>)!j \<in> active_subset (snd (lnth D k)))"
+    then show "\<exists>nj. enat (Suc nj) < llength D \<and> prems_of \<iota> ! j \<notin> active_subset (snd (lnth D nj)) \<and>
+        (\<forall>k. k > nj \<longrightarrow> enat k < llength D \<longrightarrow> prems_of \<iota> ! j \<in> active_subset (snd (lnth D 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 D \<and>
-      (prems_of \<iota>)!j \<notin> active_subset (snd (lnth D nj)) \<and>
-      (\<forall>k. k > nj \<longrightarrow> enat k < llength D \<longrightarrow> (prems_of \<iota>)!j \<in> active_subset (snd (lnth D k))))}"
+      prems_of \<iota> ! j \<notin> active_subset (snd (lnth D nj)) \<and>
+      (\<forall>k. k > nj \<longrightarrow> enat k < llength D \<longrightarrow> prems_of \<iota> ! j \<in> active_subset (snd (lnth D k))))}"
   {
     assume m_null: "m = 0"
     then have "enat 0 < llength D \<and> to_F \<iota> \<in> fst (lnth D 0)"
       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 D \<and> to_F \<iota> \<in> fst (lnth D n)"
       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 D" and
         "prems_of \<iota> ! 0 \<notin> active_subset (snd (lnth D n0))" and
         "\<forall>k>n0. enat k < llength D \<longrightarrow> prems_of \<iota> ! 0 \<in> active_subset (snd (lnth D 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 D" and
-      j0_notin: "(prems_of \<iota>)!j0 \<notin> active_subset (snd (lnth D n))" and
+      j0_notin: "prems_of \<iota> ! j0 \<notin> active_subset (snd (lnth D n))" and
       j0_allin: "(\<forall>k. k > n \<longrightarrow> enat k < llength D \<longrightarrow>
-          (prems_of \<iota>)!j0 \<in> active_subset (snd (lnth D k)))"
+          prems_of \<iota> ! j0 \<in> active_subset (snd (lnth D k)))"
       unfolding nj_set_def by blast
-    obtain C0 where C0_is: "(prems_of \<iota>)!j0 = (C0, active)"
+    obtain C0 where C0_is: "prems_of \<iota> ! j0 = (C0, active)"
       using j0_in i_in2 unfolding m_def with_labels.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 D (Suc n)))"
       using C0_is j0_allin suc_n_length by (simp add: active_subset_def)
     have C0_notin: "(C0, active) \<notin> (snd (lnth D n))"
       using C0_is j0_notin unfolding active_subset_def by simp
     have step_n: "lnth D n \<Longrightarrow>LGC lnth D (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 D n = (T1, N1) \<and> lnth D (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.Non_ground.Inf_from2 (fst ` active_subset N) {C}"
+        T' = no_labels.Inf_from2 (fst ` active_subset N) {C}"
       using step.simps[of "lnth D n" "lnth D (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 D n = (T1, N1)" and
       suc_nth_d_is: "lnth D (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.Non_ground.Inf_from2 (fst ` active_subset N) {C0}"
+      tp_is: "T' = no_labels.Inf_from2 (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)"
+    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"
+        j_not_j0: "prems_of \<iota> ! j \<noteq> prems_of \<iota> ! j0"
       obtain nj where nj_len: "enat (Suc nj) < llength D" and
-        nj_prems: "(prems_of \<iota>)!j \<notin> active_subset (snd (lnth D nj))" and
+        nj_prems: "prems_of \<iota> ! j \<notin> active_subset (snd (lnth D nj))" and
         nj_greater: "(\<forall>k. k > nj \<longrightarrow> enat k < llength D \<longrightarrow>
-            (prems_of \<iota>)!j \<in> active_subset (snd (lnth D k)))"
+            prems_of \<iota> ! j \<in> active_subset (snd (lnth D 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)"
+        then have "prems_of \<iota> ! j = (C0, active)"
           using C0_in C0_notin step.simps[of "lnth D n" "lnth D (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 D n)))"
+      then have "prems_of \<iota> ! j \<in> (active_subset (snd (lnth D 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)"
+      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> with_labels.Inf_from2 (active_subset N) {(C0, active)}"
       using i_in_inf_fl prems_i_active unfolding with_labels.Inf_from2_def with_labels.Inf_from_def
       by blast
-    then have "to_F \<iota> \<in> no_labels.Non_ground.Inf_from2 (fst ` (active_subset N)) {C0}"
+    then have "to_F \<iota> \<in> no_labels.Inf_from2 (fst ` (active_subset N)) {C0}"
       unfolding to_F_def with_labels.Inf_from2_def with_labels.Inf_from_def
-        no_labels.Non_ground.Inf_from2_def no_labels.Non_ground.Inf_from_def
+        no_labels.Inf_from2_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 D \<longrightarrow>
-        (prems_of \<iota>)!j \<in> active_subset (snd (lnth D k)))" for j
+        prems_of \<iota> ! j \<in> active_subset (snd (lnth D k)))" for j
     proof (cases "j = j0")
       case True
       assume "j = j0"
       then show "(\<forall>k. k > n \<longrightarrow> enat k < llength D \<longrightarrow>
-          (prems_of \<iota>)!j \<in> active_subset (snd (lnth D k)))" using j0_allin by simp
+          prems_of \<iota> ! j \<in> active_subset (snd (lnth D 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 D" and
-        nj_prems: "(prems_of \<iota>)!j \<notin> active_subset (snd (lnth D nj))" and
+        nj_prems: "prems_of \<iota> ! j \<notin> active_subset (snd (lnth D nj))" and
         nj_greater: "(\<forall>k. k > nj \<longrightarrow> enat k < llength D \<longrightarrow>
-            (prems_of \<iota>)!j \<in> active_subset (snd (lnth D k)))"
+            prems_of \<iota> ! j \<in> active_subset (snd (lnth D 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 D \<longrightarrow>
-          (prems_of \<iota>)!j \<in> active_subset (snd (lnth D k)))"
+          prems_of \<iota> ! j \<in> active_subset (snd (lnth D 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 D \<longrightarrow>
         c \<in> active_subset (snd (lnth D 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 D \<and> to_F \<iota> \<in> fst (lnth D (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 D \<longrightarrow>
           c \<in> active_subset (snd (lnth D 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 D \<and> to_F \<iota> \<in> fst (lnth D 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 D \<longrightarrow> c \<in> active_subset (snd (lnth D k))))"
       by auto
   }
   ultimately obtain n T2 N2 where i_in_suc_n: "to_F \<iota> \<in> fst (lnth D 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 D \<longrightarrow>
                   c \<in> active_subset (snd (lnth D k))))" and
     suc_n_length: "enat n < llength D" and suc_nth_d_is: "lnth D 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 D \<and> to_F \<iota> \<in> (fst (lnth D p)) \<and> to_F \<iota> \<notin> (fst (lnth D (Suc p)))"
   proof (rule ccontr)
     assume
       contra: "\<not> (\<exists>p\<ge>n. enat (Suc p) < llength D \<and> to_F \<iota> \<in> (fst (lnth D p)) \<and>
                      to_F \<iota> \<notin> (fst (lnth D (Suc p))))"
     then have i_in_suc: "p0 \<ge> n \<Longrightarrow> enat (Suc p0) < llength D \<Longrightarrow> to_F \<iota> \<in> (fst (lnth D p0)) \<Longrightarrow>
         to_F \<iota> \<in> (fst (lnth D (Suc p0)))" for p0
       by blast
     have "p0 \<ge> n \<Longrightarrow> enat p0 < llength D \<Longrightarrow> to_F \<iota> \<in> (fst (lnth D 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 D \<Longrightarrow> to_F \<iota> \<in> fst (lnth D p0)" and
         sucsuc_smaller_d: "enat (Suc p0) < llength D"
       have suc_p_bigger_n: "n \<le> p0" using p_bigger_n by simp
       have suc_smaller_d: "enat p0 < llength D"
         using sucsuc_smaller_d Suc_ile_eq dual_order.strict_implies_order by blast
       then have "to_F \<iota> \<in> fst (lnth D 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 D \<longrightarrow> to_F \<iota> \<in> (fst (lnth D j))"
       by presburger
     have "llength (lmap fst D) = llength D" by force
     then have "to_F \<iota> \<in> \<Inter> (lnth (lmap fst D) ` {j. n \<le> j \<and> enat j < llength (lmap fst D)})"
       using i_in_all_bigger_n using Suc_le_D by auto
     then have "to_F \<iota> \<in> Liminf_llist (lmap fst D)"
       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 D" and
     i_in_p: "to_F \<iota> \<in> (fst (lnth D p))" and i_notin_suc_p: "to_F \<iota> \<notin> (fst (lnth D (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 D p \<Longrightarrow>LGC lnth D (Suc p)" using deriv p_smaller_d chain_lnth_rel by blast
   then have "\<exists>T1 T2 \<iota> N2 N1 M. lnth D p = (T1, N1) \<and> lnth D (Suc p) = (T2, N2) \<and>
       T1 = T2 \<union> {\<iota>} \<and> N2 = N1 \<union> M \<and> active_subset M = {} \<and>
       \<iota> \<in> no_labels.empty_ord_lifted_calc_w_red_crit_family.Red_Inf_Q (fst ` (N1 \<union> M))"
   proof -
     have ci_or_do: "(\<exists>T1 T2 \<iota> N2 N1 M. lnth D p = (T1, N1) \<and> lnth D (Suc p) = (T2, N2) \<and>
         T1 = T2 \<union> {\<iota>} \<and> N2 = N1 \<union> M \<and> active_subset M = {} \<and>
         \<iota> \<in> no_labels.empty_ord_lifted_calc_w_red_crit_family.Red_Inf_Q (fst ` (N1 \<union> M))) \<or>
         (\<exists>T1 T2 T' N. lnth D p = (T1, N) \<and> lnth D (Suc p) = (T2, N) \<and>
-        T1 = T2 \<union> T' \<and>
-        T' \<inter> no_labels.Non_ground.Inf_from (fst ` active_subset N) = {})"
+        T1 = T2 \<union> T' \<and> T' \<inter> no_labels.Inf_from (fst ` active_subset N) = {})"
       using step.simps[of "lnth D p" "lnth D (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 D 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 D p)))"
+      then have "prems_of \<iota> ! j \<in> (active_subset (snd (lnth D 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 D p))))"
+      then have "fst (prems_of \<iota> ! j) \<in> (fst ` (active_subset (snd (lnth D p))))"
         by blast
       then show "(prems_of (to_F \<iota>))!j \<in> (fst ` (active_subset (snd (lnth D 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.Non_ground.Inf_from (fst ` active_subset (snd (lnth D p)))"
-      using i_in_F unfolding no_labels.Non_ground.Inf_from_def
+        to_F \<iota> \<in> no_labels.Inf_from (fst ` active_subset (snd (lnth D 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 D p = (T1, N1) \<and> lnth D (Suc p) = (T2, N2) \<and>
         T1 = T2 \<union> {\<iota>} \<and> N2 = N1 \<union> M \<and> active_subset M = {} \<and>
         \<iota> \<in> no_labels.empty_ord_lifted_calc_w_red_crit_family.Red_Inf_Q (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 D p = (T1, N1) \<and> lnth D (Suc p) = (T2, N2) \<and>
         T1 = T2 \<union> {\<iota>} \<and> N2 = N1 \<union> M \<and> active_subset M = {} \<and>
         \<iota> \<in> no_labels.empty_ord_lifted_calc_w_red_crit_family.Red_Inf_Q (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 D p = (T1p, N1p)" and
     suc_p_is: "lnth D (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.empty_ord_lifted_calc_w_red_crit_family.Red_Inf_Q
         (fst ` (N1p \<union> Mp))"
     using i_in_p i_notin_suc_p by fastforce
   have "to_F \<iota> \<in> no_labels.lifted_calc_w_red_crit_family.Red_Inf_Q (fst ` (snd (lnth D (Suc p))))"
     using i_in_red_inf suc_p_is n2p_is by fastforce
   then have "\<forall>q \<in> Q. (\<G>_Inf_q q (to_F \<iota>) \<noteq> None \<and>
       the (\<G>_Inf_q q (to_F \<iota>)) \<subseteq> Red_Inf_q q (\<Union> (\<G>_F_q q ` fst ` snd (lnth D (Suc p)))))
       \<or> (\<G>_Inf_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 D (Suc p))) \<union>
         Red_F_q q (\<Union> (\<G>_F_q q ` fst ` snd (lnth D (Suc p)))))"
     unfolding to_F_def no_labels.lifted_calc_w_red_crit_family.Red_Inf_Q_def
       no_labels.Red_Inf_\<G>_q_def no_labels.\<G>_set_q_def
     by blast
   then have "\<iota> \<in> with_labels.Red_Inf_Q (snd (lnth D (Suc p)))"
     unfolding to_F_def with_labels.Red_Inf_Q_def Red_Inf_\<G>_L_q_def \<G>_Inf_L_q_def \<G>_set_L_q_def
       \<G>_F_L_q_def using i_in_inf_fl by auto
-  then show "\<iota> \<in> with_labels.inter_red_crit_calculus.Sup_Red_Inf_llist (lmap snd D)"
-    unfolding with_labels.inter_red_crit_calculus.Sup_Red_Inf_llist_def
+  then show "\<iota> \<in> with_labels.Sup_Red_Inf_llist (lmap snd D)"
+    unfolding with_labels.Sup_Red_Inf_llist_def
     using suc_n_length p_smaller_d by auto
 qed
 
 (* thm:lgc-completeness *)
 theorem lgc_complete:
   assumes
     deriv: "chain (\<Longrightarrow>LGC) D" and
     init_state: "active_subset (snd (lnth D 0)) = {}" and
     final_state: "non_active_subset (Liminf_llist (lmap snd D)) = {}" and
     no_prems_init_active: "\<forall>\<iota> \<in> Inf_F. length (prems_of \<iota>) = 0 \<longrightarrow> \<iota> \<in> fst (lnth D 0)" and
     final_schedule: "Liminf_llist (lmap fst D) = {}" and
     b_in: "B \<in> Bot_F" and
     bot_entailed: "no_labels.entails_\<G>_Q (fst ` (snd (lnth D 0))) {B}"
   shows "\<exists>i. enat i < llength D \<and> (\<exists>BL \<in> Bot_FL. BL \<in> snd (lnth D i))"
 proof -
   have labeled_b_in: "(B, active) \<in> Bot_FL" unfolding Bot_FL_def using b_in by simp
   have simp_snd_lmap: "lnth (lmap snd D) 0 = snd (lnth D 0)"
     using lnth_lmap[of 0 D snd] chain_length_pos[OF deriv] by (simp add: zero_enat_def)
   have labeled_bot_entailed: "entails_\<G>_L_Q (snd (lnth D 0)) {(B, active)}"
     using labeled_entailment_lifting bot_entailed by fastforce
-  have "with_labels.inter_red_crit_calculus.fair (lmap snd D)"
+  have "with_labels.fair (lmap snd D)"
     using lgc_fair[OF deriv init_state final_state no_prems_init_active final_schedule] .
   then have "\<exists>i \<in> {i. enat i < llength D}. \<exists>BL\<in>Bot_FL. BL \<in> snd (lnth D i)"
     using dynamic_refutational_complete labeled_b_in lgc_to_red[OF deriv]
       labeled_bot_entailed entail_equiv simp_snd_lmap red_inf_equiv2
     by (metis (mono_tags, lifting) llength_lmap lnth_lmap mem_Collect_eq)
   then show ?thesis by blast
 qed
 
 end
 
 end