diff --git a/thys/Ordered_Resolution_Prover/Lazy_List_Chain.thy b/thys/Ordered_Resolution_Prover/Lazy_List_Chain.thy
--- a/thys/Ordered_Resolution_Prover/Lazy_List_Chain.thy
+++ b/thys/Ordered_Resolution_Prover/Lazy_List_Chain.thy
@@ -1,628 +1,628 @@
 (*  Title:       Relational Chains over Lazy Lists
     Author:      Jasmin Blanchette <j.c.blanchette at vu.nl>, 2014, 2017
     Author:      Dmitriy Traytel <traytel at inf.ethz.ch>, 2017
     Author:      Anders Schlichtkrull <andschl at dtu.dk>, 2017
     Maintainer:  Anders Schlichtkrull <andschl at dtu.dk>
 *)
 
 section \<open>Relational Chains over Lazy Lists\<close>
 
 theory Lazy_List_Chain
   imports "HOL-Library.BNF_Corec" Lazy_List_Liminf
 begin
 
 text \<open>
 A chain is a lazy lists of elements such that all pairs of consecutive elements are related by a
 given relation. A full chain is either an infinite chain or a finite chain that cannot be extended.
 The inspiration for this theory is Section 4.1 (``Theorem Proving Processes'') of Bachmair and
 Ganzinger's chapter.
 \<close>
 
 
 subsection \<open>Chains\<close>
 
 coinductive chain :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a llist \<Rightarrow> bool" for R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where
-	chain_singleton: "chain R (LCons x LNil)"
+  chain_singleton: "chain R (LCons x LNil)"
 | chain_cons: "chain R xs \<Longrightarrow> R x (lhd xs) \<Longrightarrow> chain R (LCons x xs)"
 
 lemma
   chain_LNil[simp]: "\<not> chain R LNil" and
   chain_not_lnull: "chain R xs \<Longrightarrow> \<not> lnull xs"
   by (auto elim: chain.cases)
 
 lemma chain_lappend:
   assumes
     r_xs: "chain R xs" and
     r_ys: "chain R ys" and
     mid: "R (llast xs) (lhd ys)"
   shows "chain R (lappend xs ys)"
 proof (cases "lfinite xs")
   case True
   then show ?thesis
     using r_xs mid
   proof (induct rule: lfinite.induct)
     case (lfinite_LConsI xs x)
     note fin = this(1) and ih = this(2) and r_xxs = this(3) and mid = this(4)
     show ?case
     proof (cases "xs = LNil")
       case True
       then show ?thesis
         using r_ys mid by simp (rule chain_cons)
     next
       case xs_nnil: False
       have r_xs: "chain R xs"
         by (metis chain.simps ltl_simps(2) r_xxs xs_nnil)
       have mid': "R (llast xs) (lhd ys)"
         by (metis llast_LCons lnull_def mid xs_nnil)
       have start: "R x (lhd (lappend xs ys))"
         by (metis (no_types) chain.simps lhd_LCons lhd_lappend chain_not_lnull ltl_simps(2) r_xxs
             xs_nnil)
       show ?thesis
         unfolding lappend_code(2) using ih[OF r_xs mid'] start by (rule chain_cons)
     qed
   qed simp
 qed (simp add: r_xs lappend_inf)
 
 lemma chain_length_pos: "chain R xs \<Longrightarrow> llength xs > 0"
   by (cases xs) simp+
 
 lemma chain_ldropn:
   assumes "chain R xs" and "enat n < llength xs"
   shows "chain R (ldropn n xs)"
   using assms
   by (induct n arbitrary: xs, simp,
       metis chain.cases ldrop_eSuc_ltl ldropn_LNil ldropn_eq_LNil ltl_simps(2) not_less)
 
 lemma inf_chain_ldropn_chain: "chain R xs \<Longrightarrow> \<not> lfinite xs \<Longrightarrow> chain R (ldropn n xs)"
   using chain.simps[of R xs] by (simp add: chain_ldropn not_lfinite_llength)
 
 lemma inf_chain_ltl_chain: "chain R xs \<Longrightarrow> \<not> lfinite xs \<Longrightarrow> chain R (ltl xs)"
   by (metis inf_chain_ldropn_chain ldropn_0 ldropn_ltl)
 
 lemma chain_lnth_rel:
   assumes
     chain: "chain R xs" and
     len: "enat (Suc j) < llength xs"
   shows "R (lnth xs j) (lnth xs (Suc j))"
 proof -
   define ys where "ys = ldropn j xs"
   have "llength ys > 1"
     unfolding ys_def using len
     by (metis One_nat_def funpow_swap1 ldropn_0 ldropn_def ldropn_eq_LNil ldropn_ltl not_less
         one_enat_def)
   obtain y0 y1 ys' where
     ys: "ys = LCons y0 (LCons y1 ys')"
     unfolding ys_def by (metis Suc_ile_eq ldropn_Suc_conv_ldropn len less_imp_not_less not_less)
   have "chain R ys"
     unfolding ys_def using Suc_ile_eq chain chain_ldropn len less_imp_le by blast
   then have "R y0 y1"
     unfolding ys by (auto elim: chain.cases)
   then show ?thesis
     using ys_def unfolding ys by (metis ldropn_Suc_conv_ldropn ldropn_eq_LConsD llist.inject)
 qed
 
 lemma infinite_chain_lnth_rel:
   assumes "\<not> lfinite c" and "chain r c"
   shows "r (lnth c i) (lnth c (Suc i))"
   using assms chain_lnth_rel lfinite_conv_llength_enat by force
 
 lemma lnth_rel_chain:
   assumes
     "\<not> lnull xs" and
     "\<forall>j. enat (j + 1) < llength xs \<longrightarrow> R (lnth xs j) (lnth xs (j + 1))"
   shows "chain R xs"
   using assms
 proof (coinduction arbitrary: xs rule: chain.coinduct)
   case chain
   note nnul = this(1) and nth_chain = this(2)
 
   show ?case
   proof (cases "lnull (ltl xs)")
     case True
     have "xs = LCons (lhd xs) LNil"
       using nnul True by (simp add: llist.expand)
     then show ?thesis
       by blast
   next
     case nnul': False
     moreover have "xs = LCons (lhd xs) (ltl xs)"
       using nnul by simp
     moreover have
       "\<forall>j. enat (j + 1) < llength (ltl xs) \<longrightarrow> R (lnth (ltl xs) j) (lnth (ltl xs) (j + 1))"
       using nnul nth_chain
       by (metis Suc_eq_plus1 ldrop_eSuc_ltl ldropn_Suc_conv_ldropn ldropn_eq_LConsD lnth_ltl)
     moreover have "R (lhd xs) (lhd (ltl xs))"
       using nnul' nnul nth_chain[rule_format, of 0, simplified]
       by (metis ldropn_0 ldropn_Suc_conv_ldropn ldropn_eq_LConsD lhd_LCons_ltl lhd_conv_lnth
           lnth_Suc_LCons ltl_simps(2))
     ultimately show ?thesis
       by blast
   qed
 qed
 
 lemma chain_lmap:
   assumes "\<forall>x y. R x y \<longrightarrow> R' (f x) (f y)" and "chain R xs"
   shows "chain R' (lmap f xs)"
   using assms
 proof (coinduction arbitrary: xs)
   case chain
   then have "(\<exists>y. xs = LCons y LNil) \<or> (\<exists>ys x. xs = LCons x ys \<and> chain R ys \<and> R x (lhd ys))"
     using chain.simps[of R xs] by auto
   then show ?case
   proof
     assume "\<exists>ys x. xs = LCons x ys \<and> chain R ys \<and> R x (lhd ys)"
     then have "\<exists>ys x. lmap f xs = LCons x ys \<and>
       (\<exists>xs. ys = lmap f xs \<and> (\<forall>x y. R x y \<longrightarrow> R' (f x) (f y)) \<and> chain R xs) \<and> R' x (lhd ys)"
       using chain
       by (metis (no_types) lhd_LCons llist.distinct(1) llist.exhaust_sel llist.map_sel(1)
           lmap_eq_LNil chain_not_lnull ltl_lmap ltl_simps(2))
     then show ?thesis
       by auto
   qed auto
 qed
 
 lemma chain_mono:
   assumes "\<forall>x y. R x y \<longrightarrow> R' x y" and "chain R xs"
   shows "chain R' xs"
   using assms by (rule chain_lmap[of _ _ "\<lambda>x. x", unfolded llist.map_ident])
 
 lemma lfinite_chain_imp_rtranclp_lhd_llast: "lfinite xs \<Longrightarrow> chain R xs \<Longrightarrow> R\<^sup>*\<^sup>* (lhd xs) (llast xs)"
 proof (induct rule: lfinite.induct)
   case (lfinite_LConsI xs x)
   note fin_xs = this(1) and ih = this(2) and r_x_xs = this(3)
   show ?case
   proof (cases "xs = LNil")
     case xs_nnil: False
     then have r_xs: "chain R xs"
       using r_x_xs by (blast elim: chain.cases)
     then show ?thesis
       using ih[OF r_xs] xs_nnil r_x_xs
       by (metis chain.cases converse_rtranclp_into_rtranclp lhd_LCons llast_LCons chain_not_lnull
           ltl_simps(2))
   qed simp
 qed simp
 
 lemma tranclp_imp_exists_finite_chain_list:
   "R\<^sup>+\<^sup>+ x y \<Longrightarrow> \<exists>xs. chain R (llist_of (x # xs @ [y]))"
 proof (induct rule: tranclp.induct)
   case (r_into_trancl x y)
   then have "chain R (llist_of (x # [] @ [y]))"
     by (auto intro: chain.intros)
   then show ?case
     by blast
 next
   case (trancl_into_trancl x y z)
   note rstar_xy = this(1) and ih = this(2) and r_yz = this(3)
 
   obtain xs where
     xs: "chain R (llist_of (x # xs @ [y]))"
     using ih by blast
   define ys where
     "ys = xs @ [y]"
 
   have "chain R (llist_of (x # ys @ [z]))"
     unfolding ys_def using r_yz chain_lappend[OF xs chain_singleton, of z]
     by (auto simp: lappend_llist_of_LCons llast_LCons)
   then show ?case
     by blast
 qed
 
 inductive_cases chain_consE: "chain R (LCons x xs)"
 inductive_cases chain_nontrivE: "chain R (LCons x (LCons y xs))"
 
 
 subsection \<open>A Coinductive Puzzle\<close>
 
 primrec prepend where
   "prepend [] ys = ys"
 | "prepend (x # xs) ys = LCons x (prepend xs ys)"
 
 lemma lnull_prepend[simp]: "lnull (prepend xs ys) = (xs = [] \<and> lnull ys)"
   by (induct xs) auto
 
 lemma lhd_prepend[simp]: "lhd (prepend xs ys) = (if xs \<noteq> [] then hd xs else lhd ys)"
   by (induct xs) auto
 
 lemma prepend_LNil[simp]: "prepend xs LNil = llist_of xs"
   by (induct xs) auto
 
 lemma lfinite_prepend[simp]: "lfinite (prepend xs ys) \<longleftrightarrow> lfinite ys"
   by (induct xs) auto
 
 lemma llength_prepend[simp]: "llength (prepend xs ys) = length xs + llength ys"
   by (induct xs) (auto simp: enat_0 iadd_Suc eSuc_enat[symmetric])
 
 lemma llast_prepend[simp]: "\<not> lnull ys \<Longrightarrow> llast (prepend xs ys) = llast ys"
   by (induct xs) (auto simp: llast_LCons)
 
 lemma prepend_prepend: "prepend xs (prepend ys zs) = prepend (xs @ ys) zs"
   by (induct xs) auto
 
 lemma chain_prepend:
   "chain R (llist_of zs) \<Longrightarrow> last zs = lhd xs \<Longrightarrow> chain R xs \<Longrightarrow> chain R (prepend zs (ltl xs))"
   by (induct zs; cases xs)
     (auto split: if_splits simp: lnull_def[symmetric] intro!: chain_cons elim!: chain_consE)
 
 lemma lmap_prepend[simp]: "lmap f (prepend xs ys) = prepend (map f xs) (lmap f ys)"
   by (induct xs) auto
 
 lemma lset_prepend[simp]: "lset (prepend xs ys) = set xs \<union> lset ys"
   by (induct xs) auto
 
 lemma prepend_LCons: "prepend xs (LCons y ys) = prepend (xs @ [y]) ys"
   by (induct xs) auto
 
 lemma lnth_prepend:
   "lnth (prepend xs ys) i = (if i < length xs then nth xs i else lnth ys (i - length xs))"
   by (induct xs arbitrary: i) (auto simp: lnth_LCons' nth_Cons')
 
 theorem lfinite_less_induct[consumes 1, case_names less]:
   assumes fin: "lfinite xs"
     and step: "\<And>xs. lfinite xs \<Longrightarrow> (\<And>zs. llength zs < llength xs \<Longrightarrow> P zs) \<Longrightarrow> P xs"
   shows "P xs"
 using fin proof (induct "the_enat (llength xs)" arbitrary: xs rule: less_induct)
   case (less xs)
   show ?case
     using less(2) by (intro step[OF less(2)] less(1))
       (auto dest!: lfinite_llength_enat simp: eSuc_enat elim!: less_enatE llength_eq_enat_lfiniteD)
 qed
 
 theorem lfinite_prepend_induct[consumes 1, case_names LNil prepend]:
   assumes "lfinite xs"
     and LNil: "P LNil"
     and prepend: "\<And>xs. lfinite xs \<Longrightarrow> (\<And>zs. (\<exists>ys. xs = prepend ys zs \<and> ys \<noteq> []) \<Longrightarrow> P zs) \<Longrightarrow> P xs"
   shows "P xs"
 using assms(1) proof (induct xs rule: lfinite_less_induct)
   case (less xs)
   from less(1) show ?case
     by (cases xs)
       (force simp: LNil neq_Nil_conv dest: lfinite_llength_enat intro!: prepend[of "LCons _ _"] intro: less)+
 qed
 
 coinductive emb :: "'a llist \<Rightarrow> 'a llist \<Rightarrow> bool" where
   "lfinite xs \<Longrightarrow> emb LNil xs"
 | "emb xs ys \<Longrightarrow> emb (LCons x xs) (prepend zs (LCons x ys))"
 
 inductive_cases emb_LConsE: "emb (LCons z zs) ys"
 inductive_cases emb_LNil1E: "emb LNil ys"
 inductive_cases emb_LNil2E: "emb xs LNil"
 
 lemma emb_lfinite:
   assumes "emb xs ys"
   shows "lfinite ys \<longleftrightarrow> lfinite xs"
 proof
   assume "lfinite xs"
   then show "lfinite ys" using assms
     by (induct xs arbitrary: ys rule: lfinite_induct)
       (auto simp: lnull_def neq_LNil_conv elim!: emb_LNil1E emb_LConsE)
 next
   assume "lfinite ys"
   then show "lfinite xs" using assms
   proof (induction ys arbitrary: xs rule: lfinite_less_induct)
     case (less ys)
     from less.prems \<open>lfinite ys\<close> show ?case
       by (cases xs)
         (auto simp: eSuc_enat elim!: emb_LNil1E emb_LConsE less.IH[rotated]
           dest!: lfinite_llength_enat)
   qed
 qed
 
 inductive prepend_cong1 for X where
   prepend_cong1_base: "X xs \<Longrightarrow> prepend_cong1 X xs"
 | prepend_cong1_prepend: "prepend_cong1 X ys \<Longrightarrow> prepend_cong1 X (prepend xs ys)"
 
 lemma emb_prepend_coinduct[rotated, case_names emb]:
   assumes "(\<And>x1 x2. X x1 x2 \<Longrightarrow>
     (\<exists>xs. x1 = LNil \<and> x2 = xs \<and> lfinite xs)
      \<or> (\<exists>xs ys x zs. x1 = LCons x xs \<and> x2 = prepend zs (LCons x ys)
        \<and> (prepend_cong1 (X xs) ys \<or> emb xs ys)))" (is "\<And>x1 x2. X x1 x2 \<Longrightarrow> ?bisim x1 x2")
   shows "X x1 x2 \<Longrightarrow> emb x1 x2"
 proof (erule emb.coinduct[OF prepend_cong1_base])
   fix xs zs
   assume "prepend_cong1 (X xs) zs"
   then show "?bisim xs zs"
     by (induct zs rule: prepend_cong1.induct) (erule assms, force simp: prepend_prepend)
 qed
 
 context
 begin
 
 private coinductive chain' for R where
   "chain' R (LCons x LNil)"
 | "chain R (llist_of (x # zs @ [lhd xs])) \<Longrightarrow>
    chain' R xs \<Longrightarrow> chain' R (LCons x (prepend zs xs))"
 
 private lemma chain_imp_chain': "chain R xs \<Longrightarrow> chain' R xs"
 proof (coinduction arbitrary: xs rule: chain'.coinduct)
   case chain'
   then show ?case
   proof (cases rule: chain.cases)
     case (chain_cons zs z)
     then show ?thesis
       by (intro disjI2 exI[of _ z] exI[of _ "[]"] exI[of _ "zs"])
         (auto intro: chain.intros)
   qed simp
 qed
 
 private lemma chain'_imp_chain: "chain' R xs \<Longrightarrow> chain R xs"
 proof (coinduction arbitrary: xs rule: chain.coinduct)
   case chain
   then show ?case
   proof (cases rule: chain'.cases)
     case (2 y zs ys)
     then show ?thesis
       by (intro disjI2 exI[of _ "prepend zs ys"] exI[of _ y])
         (force dest!: neq_Nil_conv[THEN iffD1] elim: chain.cases chain_nontrivE
           intro: chain'.intros)
   qed simp
 qed
 
 private lemma chain_chain': "chain = chain'"
   unfolding fun_eq_iff by (metis chain_imp_chain' chain'_imp_chain)
 
 lemma chain_prepend_coinduct[case_names chain]:
   "X x \<Longrightarrow> (\<And>x. X x \<Longrightarrow>
     (\<exists>z. x = LCons z LNil) \<or>
     (\<exists>y xs zs. x = LCons y (prepend zs xs) \<and>
       (X xs \<or> chain R xs) \<and> chain R (llist_of (y # zs @ [lhd xs])))) \<Longrightarrow> chain R x"
   by (subst chain_chain', erule chain'.coinduct) (force simp: chain_chain')
 
 end
 
 context
   fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
 begin
 
 private definition pick where
   "pick x y = (SOME xs. chain R (llist_of (x # xs @ [y])))"
 
 private lemma pick[simp]:
   assumes "R\<^sup>+\<^sup>+ x y"
   shows "chain R (llist_of (x # pick x y @ [y]))"
   unfolding pick_def using tranclp_imp_exists_finite_chain_list[THEN someI_ex, OF assms] by auto
 
 private friend_of_corec prepend where
   "prepend xs ys = (case xs of [] \<Rightarrow>
     (case ys of LNil \<Rightarrow> LNil | LCons x xs \<Rightarrow> LCons x xs) | x # xs' \<Rightarrow> LCons x (prepend xs' ys))"
   by (simp split: list.splits llist.splits) transfer_prover
 
 private corec wit where
   "wit xs = (case xs of LCons x (LCons y xs) \<Rightarrow>
      LCons x (prepend (pick x y) (wit (LCons y xs))) | _ \<Rightarrow> xs)"
 
 private lemma
   wit_LNil[simp]: "wit LNil = LNil" and
   wit_lsingleton[simp]: "wit (LCons x LNil) = LCons x LNil" and
   wit_LCons2: "wit (LCons x (LCons y xs)) =
      (LCons x (prepend (pick x y) (wit (LCons y xs))))"
   by (subst wit.code; auto)+
 
 private lemma lnull_wit[simp]: "lnull (wit xs) \<longleftrightarrow> lnull xs"
   by (subst wit.code) (auto split: llist.splits simp: Let_def)
 
 private lemma lhd_wit[simp]: "chain R\<^sup>+\<^sup>+ xs \<Longrightarrow> lhd (wit xs) = lhd xs"
   by (erule chain.cases; subst wit.code) (auto split: llist.splits simp: Let_def)
 
 private lemma LNil_eq_iff_lnull: "LNil = xs \<longleftrightarrow> lnull xs"
   by (cases xs) auto
 
 lemma emb_wit[simp]: "chain R\<^sup>+\<^sup>+ xs \<Longrightarrow> emb xs (wit xs)"
 proof (coinduction arbitrary: xs rule: emb_prepend_coinduct)
   case (emb xs)
   then show ?case
   proof (cases rule: chain.cases)
     case (chain_cons zs z)
     then show ?thesis
       by (subst (2) wit.code)
         (auto split: llist.splits intro!: exI[of _ "[]"] exI[of _ "_ :: _ llist"]
           prepend_cong1_prepend[OF prepend_cong1_base])
   qed (auto intro!: exI[of _ LNil] exI[of _ "[]"] emb.intros)
 qed
 
 private lemma lfinite_wit[simp]:
   assumes "chain R\<^sup>+\<^sup>+ xs"
   shows "lfinite (wit xs) \<longleftrightarrow> lfinite xs"
   using emb_wit emb_lfinite assms by blast
 
 private lemma llast_wit[simp]:
   assumes "chain R\<^sup>+\<^sup>+ xs"
   shows "llast (wit xs) = llast xs"
 proof (cases "lfinite xs")
   case True
   from this assms show ?thesis
   proof (induct rule: lfinite.induct)
     case (lfinite_LConsI xs x)
     then show ?case
       by (cases xs) (auto simp: wit_LCons2 llast_LCons elim: chain_nontrivE)
   qed auto
 qed (auto simp: llast_linfinite assms)
 
 lemma chain_tranclp_imp_exists_chain:
   "chain R\<^sup>+\<^sup>+ xs \<Longrightarrow>
    \<exists>ys. chain R ys \<and> emb xs ys \<and> lhd ys = lhd xs \<and> llast ys = llast xs"
 proof (intro exI[of _ "wit xs"] conjI, coinduction arbitrary: xs rule: chain_prepend_coinduct)
   case chain
   then show ?case
     by (subst (1 2) wit.code) (erule chain.cases; force split: llist.splits dest: pick)
 qed auto
 
 lemma emb_lset_mono[rotated]: "x \<in> lset xs \<Longrightarrow> emb xs ys \<Longrightarrow> x \<in> lset ys"
   by (induct x xs arbitrary: ys rule: llist.set_induct) (auto elim!: emb_LConsE)
 
 lemma emb_Ball_lset_antimono:
   assumes "emb Xs Ys"
   shows "\<forall>Y \<in> lset Ys. x \<in> Y \<Longrightarrow> \<forall>X \<in> lset Xs. x \<in> X"
   using emb_lset_mono[OF assms] by blast
 
 lemma emb_lfinite_antimono[rotated]: "lfinite ys \<Longrightarrow> emb xs ys \<Longrightarrow> lfinite xs"
   by (induct ys arbitrary: xs rule: lfinite_prepend_induct)
     (force elim!: emb_LNil2E simp: LNil_eq_iff_lnull prepend_LCons elim: emb.cases)+
 
 lemma emb_Liminf_llist_mono_aux:
   assumes "emb Xs Ys" and "\<not> lfinite Xs" and "\<not> lfinite Ys" and "\<forall>j\<ge>i. x \<in> lnth Ys j"
   shows "\<forall>j\<ge>i. x \<in> lnth Xs j"
 using assms proof (induct i arbitrary: Xs Ys rule: less_induct)
   case (less i)
   then show ?case
   proof (cases i)
     case 0
     then show ?thesis
       using emb_Ball_lset_antimono[OF less(2), of x] less(5)
       unfolding Ball_def in_lset_conv_lnth simp_thms
         not_lfinite_llength[OF less(3)] not_lfinite_llength[OF less(4)] enat_ord_code subset_eq
       by blast
   next
     case [simp]: (Suc nat)
     from less(2,3) obtain xs as b bs where
       [simp]: "Xs = LCons b xs" "Ys = prepend as (LCons b bs)" and "emb xs bs"
       by (auto elim: emb.cases)
     have IH: "\<forall>k\<ge>j. x \<in> lnth xs k" if "\<forall>k\<ge>j. x \<in> lnth bs k" "j < i" for j
       using that less(1)[OF _ \<open>emb xs bs\<close>] less(3,4) by auto
     from less(5) have "\<forall>k\<ge>i - length as - 1. x \<in> lnth xs k"
       by (intro IH allI)
         (drule spec[of _ "_ + length as + 1"], auto simp: lnth_prepend lnth_LCons')
     then show ?thesis
       by (auto simp: lnth_LCons')
   qed
 qed
 
 lemma emb_Liminf_llist_infinite:
   assumes "emb Xs Ys" and "\<not> lfinite Xs"
   shows "Liminf_llist Ys \<subseteq> Liminf_llist Xs"
 proof -
   from assms have "\<not> lfinite Ys"
     using emb_lfinite_antimono by blast
   with assms show ?thesis
     unfolding Liminf_llist_def by (auto simp: not_lfinite_llength dest: emb_Liminf_llist_mono_aux)
 qed
 
 lemma emb_lmap: "emb xs ys \<Longrightarrow> emb (lmap f xs) (lmap f ys)"
 proof (coinduction arbitrary: xs ys rule: emb.coinduct)
   case emb
   show ?case
   proof (cases xs)
     case xs: (LCons x xs')
 
     obtain ysa0 and zs0 where
       ys: "ys = prepend zs0 (LCons x ysa0)" and
       emb': "emb xs' ysa0"
       using emb_LConsE[OF emb[unfolded xs]] by metis
 
     let ?xa = "f x"
     let ?xsa = "lmap f xs'"
     let ?zs = "map f zs0"
     let ?ysa = "lmap f ysa0"
 
     have "lmap f xs = LCons ?xa ?xsa"
       unfolding xs by simp
     moreover have "lmap f ys = prepend ?zs (LCons ?xa ?ysa)"
       unfolding ys by simp
     moreover have "\<exists>xsa ysa. ?xsa = lmap f xsa \<and> ?ysa = lmap f ysa \<and> emb xsa ysa"
       using emb' by blast
     ultimately show ?thesis
       by blast
   qed (simp add: emb_lfinite[OF emb])
 qed
 
 end
 
 lemma chain_inf_llist_if_infinite_chain_function:
   assumes "\<forall>i. r (f (Suc i)) (f i)"
   shows "\<not> lfinite (inf_llist f) \<and> chain r\<inverse>\<inverse> (inf_llist f)"
   using assms by (simp add: lnth_rel_chain)
 
 lemma infinite_chain_function_iff_infinite_chain_llist:
   "(\<exists>f. \<forall>i. r (f (Suc i)) (f i)) \<longleftrightarrow> (\<exists>c. \<not> lfinite c \<and> chain r\<inverse>\<inverse> c)"
   using chain_inf_llist_if_infinite_chain_function infinite_chain_lnth_rel by blast
 
 lemma wfP_iff_no_infinite_down_chain_llist: "wfP r \<longleftrightarrow> (\<nexists>c. \<not> lfinite c \<and> chain r\<inverse>\<inverse> c)"
 proof -
   have "wfP r \<longleftrightarrow>  wf {(x, y). r x y}"
     unfolding wfP_def by auto
   also have "\<dots> \<longleftrightarrow> (\<nexists>f. \<forall>i. (f (Suc i), f i) \<in> {(x, y). r x y})"
     using wf_iff_no_infinite_down_chain by blast
   also have "\<dots> \<longleftrightarrow> (\<nexists>f. \<forall>i. r (f (Suc i)) (f i))"
     by auto
   also have "\<dots> \<longleftrightarrow> (\<nexists>c. \<not>lfinite c \<and> chain r\<inverse>\<inverse> c)"
     using infinite_chain_function_iff_infinite_chain_llist by blast
   finally show ?thesis
     by auto
 qed
 
 
 subsection \<open>Full Chains\<close>
 
 coinductive full_chain :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a llist \<Rightarrow> bool" for R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where
-	full_chain_singleton: "(\<forall>y. \<not> R x y) \<Longrightarrow> full_chain R (LCons x LNil)"
+  full_chain_singleton: "(\<forall>y. \<not> R x y) \<Longrightarrow> full_chain R (LCons x LNil)"
 | full_chain_cons: "full_chain R xs \<Longrightarrow> R x (lhd xs) \<Longrightarrow> full_chain R (LCons x xs)"
 
 lemma
   full_chain_LNil[simp]: "\<not> full_chain R LNil" and
   full_chain_not_lnull: "full_chain R xs \<Longrightarrow> \<not> lnull xs"
   by (auto elim: full_chain.cases)
 
 lemma full_chain_ldropn:
   assumes full: "full_chain R xs" and "enat n < llength xs"
   shows "full_chain R (ldropn n xs)"
   using assms
   by (induct n arbitrary: xs, simp,
       metis full_chain.cases ldrop_eSuc_ltl ldropn_LNil ldropn_eq_LNil ltl_simps(2) not_less)
 
 lemma full_chain_iff_chain:
   "full_chain R xs \<longleftrightarrow> chain R xs \<and> (lfinite xs \<longrightarrow> (\<forall>y. \<not> R (llast xs) y))"
 proof (intro iffI conjI impI allI; (elim conjE)?)
   assume full: "full_chain R xs"
 
   show chain: "chain R xs"
     using full by (coinduction arbitrary: xs) (auto elim: full_chain.cases)
 
   {
     fix y
     assume "lfinite xs"
     then obtain n where
       suc_n: "Suc n = llength xs"
       by (metis chain chain_length_pos lessE less_enatE lfinite_conv_llength_enat)
 
     have "full_chain R (ldropn n xs)"
       by (rule full_chain_ldropn[OF full]) (use suc_n Suc_ile_eq in force)
     moreover have "ldropn n xs = LCons (llast xs) LNil"
       using suc_n by (metis enat_le_plus_same(2) enat_ord_simps(2) gen_llength_def
           ldropn_Suc_conv_ldropn ldropn_all lessI llast_ldropn llast_singleton llength_code)
     ultimately show "\<not> R (llast xs) y"
       by (auto elim: full_chain.cases)
   }
 next
   assume
     "chain R xs" and
     "lfinite xs \<longrightarrow> (\<forall>y. \<not> R (llast xs) y)"
   then show "full_chain R xs"
     by (coinduction arbitrary: xs) (erule chain.cases, simp, metis lfinite_LConsI llast_LCons)
 qed
 
 lemma full_chain_imp_chain: "full_chain R xs \<Longrightarrow> chain R xs"
   using full_chain_iff_chain by blast
 
 lemma full_chain_length_pos: "full_chain R xs \<Longrightarrow> llength xs > 0"
   by (fact chain_length_pos[OF full_chain_imp_chain])
 
 lemma full_chain_lnth_rel:
   "full_chain R xs \<Longrightarrow> enat (Suc j) < llength xs \<Longrightarrow> R (lnth xs j) (lnth xs (Suc j))"
   by (fact chain_lnth_rel[OF full_chain_imp_chain])
 
 inductive_cases full_chain_consE: "full_chain R (LCons x xs)"
 inductive_cases full_chain_nontrivE: "full_chain R (LCons x (LCons y xs))"
 
 lemma full_chain_tranclp_imp_exists_full_chain:
   assumes full: "full_chain R\<^sup>+\<^sup>+ xs"
   shows "\<exists>ys. full_chain R ys \<and> emb xs ys \<and> lhd ys = lhd xs \<and> llast ys = llast xs"
 proof -
   obtain ys where ys:
     "chain R ys" "emb xs ys" "lhd ys = lhd xs" "llast ys = llast xs"
     using full_chain_imp_chain[OF full] chain_tranclp_imp_exists_chain by blast
   have "full_chain R ys"
     using ys(1,4) emb_lfinite[OF ys(2)] full unfolding full_chain_iff_chain by auto
   then show ?thesis
     using ys(2-4) by auto
 qed
 
 end
diff --git a/thys/Ordered_Resolution_Prover/Lazy_List_Liminf.thy b/thys/Ordered_Resolution_Prover/Lazy_List_Liminf.thy
--- a/thys/Ordered_Resolution_Prover/Lazy_List_Liminf.thy
+++ b/thys/Ordered_Resolution_Prover/Lazy_List_Liminf.thy
@@ -1,283 +1,373 @@
-(*  Title:       Liminf of Lazy Lists
-    Author:      Jasmin Blanchette <j.c.blanchette at vu.nl>, 2014, 2017
+(*  Title:       Supremum and Liminf of Lazy Lists
+    Author:      Jasmin Blanchette <j.c.blanchette at vu.nl>, 2014, 2017, 2020
     Author:      Dmitriy Traytel <traytel at inf.ethz.ch>, 2014
     Maintainer:  Jasmin Blanchette <j.c.blanchette at vu.nl>
 *)
 
-section \<open>Liminf of Lazy Lists\<close>
+section \<open>Supremum and Liminf of Lazy Lists\<close>
 
 theory Lazy_List_Liminf
   imports Coinductive.Coinductive_List
 begin
 
 text \<open>
 Lazy lists, as defined in the \emph{Archive of Formal Proofs}, provide finite and infinite lists in
 one type, defined coinductively. The present theory introduces the concept of the union of all
 elements of a lazy list of sets and the limit of such a lazy list. The definitions are stated more
 generally in terms of lattices. The basis for this theory is Section 4.1 (``Theorem Proving
 Processes'') of Bachmair and Ganzinger's chapter.
 \<close>
 
+
+subsection \<open>Library\<close>
+
+lemma less_llength_ltake: "i < llength (ltake k Xs) \<longleftrightarrow> i < k \<and> i < llength Xs"
+  by simp
+
+
+subsection \<open>Supremum\<close>
+
 definition Sup_llist :: "'a set llist \<Rightarrow> 'a set" where
   "Sup_llist Xs = (\<Union>i \<in> {i. enat i < llength Xs}. lnth Xs i)"
 
 lemma lnth_subset_Sup_llist: "enat i < llength Xs \<Longrightarrow> lnth Xs i \<subseteq> Sup_llist Xs"
   unfolding Sup_llist_def by auto
 
 lemma Sup_llist_imp_exists_index: "x \<in> Sup_llist Xs \<Longrightarrow> \<exists>i. enat i < llength Xs \<and> x \<in> lnth Xs i"
   unfolding Sup_llist_def by auto
 
 lemma exists_index_imp_Sup_llist: "enat i < llength Xs \<Longrightarrow> x \<in> lnth Xs i \<Longrightarrow> x \<in> Sup_llist Xs"
   unfolding Sup_llist_def by auto
 
 lemma Sup_llist_LNil[simp]: "Sup_llist LNil = {}"
   unfolding Sup_llist_def by auto
 
 lemma Sup_llist_LCons[simp]: "Sup_llist (LCons X Xs) = X \<union> Sup_llist Xs"
   unfolding Sup_llist_def
 proof (intro subset_antisym subsetI)
   fix x
   assume "x \<in> (\<Union>i \<in> {i. enat i < llength (LCons X Xs)}. lnth (LCons X Xs) i)"
   then obtain i where len: "enat i < llength (LCons X Xs)" and nth: "x \<in> lnth (LCons X Xs) i"
     by blast
   from nth have "x \<in> X \<or> i > 0 \<and> x \<in> lnth Xs (i - 1)"
     by (metis lnth_LCons' neq0_conv)
   then have "x \<in> X \<or> (\<exists>i. enat i < llength Xs \<and> x \<in> lnth Xs i)"
     by (metis len Suc_pred' eSuc_enat iless_Suc_eq less_irrefl llength_LCons not_less order_trans)
   then show "x \<in> X \<union> (\<Union>i \<in> {i. enat i < llength Xs}. lnth Xs i)"
     by blast
 qed ((auto)[], metis i0_lb lnth_0 zero_enat_def, metis Suc_ile_eq lnth_Suc_LCons)
 
 lemma lhd_subset_Sup_llist: "\<not> lnull Xs \<Longrightarrow> lhd Xs \<subseteq> Sup_llist Xs"
   by (cases Xs) simp_all
 
-definition Sup_upto_llist :: "'a set llist \<Rightarrow> nat \<Rightarrow> 'a set" where
-  "Sup_upto_llist Xs j = (\<Union>i \<in> {i. enat i < llength Xs \<and> i \<le> j}. lnth Xs i)"
 
-lemma Sup_upto_llist_0[simp]: "Sup_upto_llist Xs 0 = (if 0 < llength Xs then lnth Xs 0 else {})"
-  unfolding Sup_upto_llist_def image_def by (simp add: enat_0)
+subsection \<open>Supremum up-to\<close>
+
+definition Sup_upto_llist :: "'a set llist \<Rightarrow> enat \<Rightarrow> 'a set" where
+  "Sup_upto_llist Xs j = (\<Union>i \<in> {i. enat i < llength Xs \<and> enat i \<le> j}. lnth Xs i)"
+
+lemma Sup_upto_llist_eq_Sup_llist_ltake: "Sup_upto_llist Xs j = Sup_llist (ltake (eSuc j) Xs)"
+  unfolding Sup_upto_llist_def Sup_llist_def
+  by (smt Collect_cong Sup.SUP_cong iless_Suc_eq lnth_ltake less_llength_ltake mem_Collect_eq)
+
+lemma Sup_upto_llist_0[simp]:
+  "Sup_upto_llist Xs (enat 0) = (if 0 < llength Xs then lnth Xs 0 else {})"
+  unfolding Sup_upto_llist_def image_def by (simp add: enat_0[symmetric])
 
 lemma Sup_upto_llist_Suc[simp]:
-  "Sup_upto_llist Xs (Suc j) =
-   Sup_upto_llist Xs j \<union> (if enat (Suc j) < llength Xs then lnth Xs (Suc j) else {})"
+  "Sup_upto_llist Xs (enat (Suc j)) =
+   Sup_upto_llist Xs (enat j) \<union> (if enat (Suc j) < llength Xs then lnth Xs (Suc j) else {})"
   unfolding Sup_upto_llist_def image_def by (auto intro: le_SucI elim: le_SucE)
 
+lemma Sup_upto_llist_infinity[simp]: "Sup_upto_llist Xs \<infinity> = Sup_llist Xs"
+  unfolding Sup_upto_llist_def Sup_llist_def by simp
+
+lemma Sup_upto_llist_eSuc[simp]:
+  "Sup_upto_llist Xs (eSuc j) =
+   (case j of
+      enat k \<Rightarrow> Sup_upto_llist Xs (enat (Suc k))
+    | \<infinity> \<Rightarrow> Sup_llist Xs)"
+  by (auto simp: eSuc_enat split: enat.split)
+
 lemma Sup_upto_llist_mono: "j \<le> k \<Longrightarrow> Sup_upto_llist Xs j \<subseteq> Sup_upto_llist Xs k"
   unfolding Sup_upto_llist_def by auto
 
-lemma Sup_upto_llist_subset_Sup_llist: "j \<le> k \<Longrightarrow> Sup_upto_llist Xs j \<subseteq> Sup_llist Xs"
+lemma Sup_upto_llist_subset_Sup_llist: "Sup_upto_llist Xs j \<subseteq> Sup_llist Xs"
   unfolding Sup_llist_def Sup_upto_llist_def by auto
 
 lemma elem_Sup_llist_imp_Sup_upto_llist:
-	"x \<in> Sup_llist Xs \<Longrightarrow> \<exists>j < llength Xs. x \<in> Sup_upto_llist Xs j"
+  "x \<in> Sup_llist Xs \<Longrightarrow> \<exists>j < llength Xs. x \<in> Sup_upto_llist Xs (enat j)"
   unfolding Sup_llist_def Sup_upto_llist_def by blast
 
-lemma lnth_subset_Sup_upto_llist: "enat j < llength Xs \<Longrightarrow> lnth Xs j \<subseteq> Sup_upto_llist Xs j"
+lemma lnth_subset_Sup_upto_llist: "j < llength Xs \<Longrightarrow> lnth Xs j \<subseteq> Sup_upto_llist Xs j"
   unfolding Sup_upto_llist_def by auto
 
 lemma finite_Sup_llist_imp_Sup_upto_llist:
   assumes "finite X" and "X \<subseteq> Sup_llist Xs"
-  shows "\<exists>k. X \<subseteq> Sup_upto_llist Xs k"
+  shows "\<exists>k. X \<subseteq> Sup_upto_llist Xs (enat k)"
   using assms
 proof induct
   case (insert x X)
   then have x: "x \<in> Sup_llist Xs" and X: "X \<subseteq> Sup_llist Xs"
     by simp+
-  from x obtain k where k: "x \<in> Sup_upto_llist Xs k"
+  from x obtain k where k: "x \<in> Sup_upto_llist Xs (enat k)"
     using elem_Sup_llist_imp_Sup_upto_llist by fast
-  from X obtain k' where k': "X \<subseteq> Sup_upto_llist Xs k'"
+  from X obtain k' where k': "X \<subseteq> Sup_upto_llist Xs (enat k')"
     using insert.hyps(3) by fast
   have "insert x X \<subseteq> Sup_upto_llist Xs (max k k')"
-    using k k'
-    by (metis insert_absorb insert_subset Sup_upto_llist_mono max.cobounded2 max.commute
-        order.trans)
+    using k k' by (metis (mono_tags) Sup_upto_llist_mono enat_ord_simps(1) insert_subset
+      max.cobounded1 max.cobounded2 subset_iff)
   then show ?case
     by fast
 qed simp
 
+
+subsection \<open>Liminf\<close>
+
 definition Liminf_llist :: "'a set llist \<Rightarrow> 'a set" where
   "Liminf_llist Xs =
    (\<Union>i \<in> {i. enat i < llength Xs}. \<Inter>j \<in> {j. i \<le> j \<and> enat j < llength Xs}. lnth Xs j)"
 
 lemma Liminf_llist_LNil[simp]: "Liminf_llist LNil = {}"
   unfolding Liminf_llist_def by simp
 
 lemma Liminf_llist_LCons:
   "Liminf_llist (LCons X Xs) = (if lnull Xs then X else Liminf_llist Xs)" (is "?lhs = ?rhs")
 proof (cases "lnull Xs")
   case nnull: False
   show ?thesis
   proof
     {
       fix x
       assume "\<exists>i. enat i \<le> llength Xs
         \<and> (\<forall>j. i \<le> j \<and> enat j \<le> llength Xs \<longrightarrow> x \<in> lnth (LCons X Xs) j)"
       then have "\<exists>i. enat (Suc i) \<le> llength Xs
         \<and> (\<forall>j. Suc i \<le> j \<and> enat j \<le> llength Xs \<longrightarrow> x \<in> lnth (LCons X Xs) j)"
         by (cases "llength Xs",
             metis not_lnull_conv[THEN iffD1, OF nnull] Suc_le_D eSuc_enat eSuc_ile_mono
               llength_LCons not_less_eq_eq zero_enat_def zero_le,
             metis Suc_leD enat_ord_code(3))
       then have "\<exists>i. enat i < llength Xs \<and> (\<forall>j. i \<le> j \<and> enat j < llength Xs \<longrightarrow> x \<in> lnth Xs j)"
         by (metis Suc_ile_eq Suc_n_not_le_n lift_Suc_mono_le lnth_Suc_LCons nat_le_linear)
     }
     then show "?lhs \<subseteq> ?rhs"
       by (simp add: Liminf_llist_def nnull) (rule subsetI, simp)
 
     {
       fix x
       assume "\<exists>i. enat i < llength Xs \<and> (\<forall>j. i \<le> j \<and> enat j < llength Xs \<longrightarrow> x \<in> lnth Xs j)"
       then obtain i where
         i: "enat i < llength Xs" and
         j: "\<forall>j. i \<le> j \<and> enat j < llength Xs \<longrightarrow> x \<in> lnth Xs j"
         by blast
 
       have "enat (Suc i) \<le> llength Xs"
         using i by (simp add: Suc_ile_eq)
       moreover have "\<forall>j. Suc i \<le> j \<and> enat j \<le> llength Xs \<longrightarrow> x \<in> lnth (LCons X Xs) j"
         using Suc_ile_eq Suc_le_D j by force
       ultimately have "\<exists>i. enat i \<le> llength Xs \<and> (\<forall>j. i \<le> j \<and> enat j \<le> llength Xs \<longrightarrow>
         x \<in> lnth (LCons X Xs) j)"
         by blast
     }
     then show "?rhs \<subseteq> ?lhs"
       by (simp add: Liminf_llist_def nnull) (rule subsetI, simp)
   qed
 qed (simp add: Liminf_llist_def enat_0_iff(1))
 
 lemma lfinite_Liminf_llist: "lfinite Xs \<Longrightarrow> Liminf_llist Xs = (if lnull Xs then {} else llast Xs)"
 proof (induction rule: lfinite_induct)
   case (LCons xs)
   then obtain y ys where
     xs: "xs = LCons y ys"
     by (meson not_lnull_conv)
   show ?case
     unfolding xs by (simp add: Liminf_llist_LCons LCons.IH[unfolded xs, simplified] llast_LCons)
 qed (simp add: Liminf_llist_def)
 
 lemma Liminf_llist_ltl: "\<not> lnull (ltl Xs) \<Longrightarrow> Liminf_llist Xs = Liminf_llist (ltl Xs)"
   by (metis Liminf_llist_LCons lhd_LCons_ltl lnull_ltlI)
 
 lemma Liminf_llist_subset_Sup_llist: "Liminf_llist Xs \<subseteq> Sup_llist Xs"
   unfolding Liminf_llist_def Sup_llist_def by fast
 
 lemma image_Liminf_llist_subset: "f ` Liminf_llist Ns \<subseteq> Liminf_llist (lmap ((`) f) Ns)"
   unfolding Liminf_llist_def by auto
 
 lemma Liminf_llist_imp_exists_index:
   "x \<in> Liminf_llist Xs \<Longrightarrow> \<exists>i. enat i < llength Xs \<and> x \<in> lnth Xs i"
   unfolding Liminf_llist_def by auto
 
 lemma not_Liminf_llist_imp_exists_index:
   "\<not> lnull Xs \<Longrightarrow> x \<notin> Liminf_llist Xs \<Longrightarrow> enat i < llength Xs \<Longrightarrow>
    (\<exists>j. i \<le> j \<and> enat j < llength Xs \<and> x \<notin> lnth Xs j)"
   unfolding Liminf_llist_def by auto
 
 lemma finite_subset_Liminf_llist_imp_exists_index:
   assumes
     nnil: "\<not> lnull Xs" and
     fin: "finite X" and
     in_lim: "X \<subseteq> Liminf_llist Xs"
-  shows "\<exists>i. enat i < llength Xs \<and> X \<subseteq> \<Inter> (lnth Xs ` {j. i \<le> j \<and> enat j < llength Xs})"
+  shows "\<exists>i. enat i < llength Xs \<and> X \<subseteq> (\<Inter>j \<in> {j. i \<le> j \<and> enat j < llength Xs}. lnth Xs j)"
 proof -
   show ?thesis
   proof (cases "X = {}")
     case True
     then show ?thesis
       using nnil by (auto intro: exI[of _ 0] simp: zero_enat_def[symmetric])
   next
     case nemp: False
 
     have in_lim':
-      "\<forall>x \<in> X. \<exists>i. enat i < llength Xs \<and> x \<in> \<Inter> (lnth Xs ` {j. i \<le> j \<and> enat j < llength Xs})"
+      "\<forall>x \<in> X. \<exists>i. enat i < llength Xs \<and> x \<in> (\<Inter>j \<in> {j. i \<le> j \<and> enat j < llength Xs}. lnth Xs j)"
       using in_lim[unfolded Liminf_llist_def] in_mono by fastforce
     obtain i_of where
       i_of_lt: "\<forall>x \<in> X. enat (i_of x) < llength Xs" and
-      in_inter: "\<forall>x \<in> X. x \<in> \<Inter> (lnth Xs ` {j. i_of x \<le> j \<and> enat j < llength Xs})"
+      in_inter: "\<forall>x \<in> X. x \<in> (\<Inter>j \<in> {j. i_of x \<le> j \<and> enat j < llength Xs}. lnth Xs j)"
       using bchoice[OF in_lim'] by blast
 
     define i_max where
       "i_max = Max (i_of ` X)"
 
     have "i_max \<in> i_of ` X"
       by (simp add: fin i_max_def nemp)
     then obtain x_max where
       x_max_in: "x_max \<in> X" and
       i_max_is: "i_max = i_of x_max"
       unfolding i_max_def by blast
     have le_i_max: "\<forall>x \<in> X. i_of x \<le> i_max"
       unfolding i_max_def by (simp add: fin)
     have "enat i_max < llength Xs"
       using i_of_lt x_max_in i_max_is by auto
-    moreover have "X \<subseteq> \<Inter> (lnth Xs ` {j. i_max \<le> j \<and> enat j < llength Xs})"
+    moreover have "X \<subseteq> (\<Inter>j \<in> {j. i_max \<le> j \<and> enat j < llength Xs}. lnth Xs j)"
     proof
       fix x
       assume x_in: "x \<in> X"
-      then have x_in_inter: "x \<in> \<Inter> (lnth Xs ` {j. i_of x \<le> j \<and> enat j < llength Xs})"
+      then have x_in_inter: "x \<in> (\<Inter>j \<in> {j. i_of x \<le> j \<and> enat j < llength Xs}. lnth Xs j)"
         using in_inter by auto
       moreover have "{j. i_max \<le> j \<and> enat j < llength Xs}
         \<subseteq> {j. i_of x \<le> j \<and> enat j < llength Xs}"
         using x_in le_i_max by auto
-      ultimately show "x \<in> \<Inter> (lnth Xs ` {j. i_max \<le> j \<and> enat j < llength Xs})"
+      ultimately show "x \<in> (\<Inter>j \<in> {j. i_max \<le> j \<and> enat j < llength Xs}. lnth Xs j)"
         by auto
     qed
     ultimately show ?thesis
       by auto
   qed
 qed
 
 lemma Liminf_llist_lmap_image:
   assumes f_inj: "inj_on f (Sup_llist (lmap g xs))"
   shows "Liminf_llist (lmap (\<lambda>x. f ` g x) xs) = f ` Liminf_llist (lmap g xs)" (is "?lhs = ?rhs")
 proof
   show "?lhs \<subseteq> ?rhs"
   proof
     fix x
     assume "x \<in> Liminf_llist (lmap (\<lambda>x. f ` g x) xs)"
     then obtain i where
       i_lt: "enat i < llength xs" and
       x_in_fgj: "\<forall>j. i \<le> j \<longrightarrow> enat j < llength xs \<longrightarrow> x \<in> f ` g (lnth xs j)"
       unfolding Liminf_llist_def by auto
 
     have ex_in_gi: "\<exists>y. y \<in> g (lnth xs i) \<and> x = f y"
       using f_inj i_lt x_in_fgj unfolding inj_on_def Sup_llist_def by auto
     have "\<exists>y. \<forall>j. i \<le> j \<longrightarrow> enat j < llength xs \<longrightarrow> y \<in> g (lnth xs j) \<and> x = f y"
       apply (rule exI[of _ "SOME y. y \<in> g (lnth xs i) \<and> x = f y"])
       using someI_ex[OF ex_in_gi] x_in_fgj f_inj i_lt x_in_fgj unfolding inj_on_def Sup_llist_def
       by simp (metis (no_types, lifting) imageE)
     then show "x \<in> f ` Liminf_llist (lmap g xs)"
       using i_lt unfolding Liminf_llist_def by auto
   qed
 next
   show "?rhs \<subseteq> ?lhs"
     using image_Liminf_llist_subset[of f "lmap g xs", unfolded llist.map_comp] by auto
 qed
 
 lemma Liminf_llist_lmap_union:
   assumes "\<forall>x \<in> lset xs. \<forall>Y \<in> lset xs. g x \<inter> h Y = {}"
   shows "Liminf_llist (lmap (\<lambda>x. g x \<union> h x) xs) =
     Liminf_llist (lmap g xs) \<union> Liminf_llist (lmap h xs)" (is "?lhs = ?rhs")
 proof (intro equalityI subsetI)
   fix x
   assume x_in: "x \<in> ?lhs"
   then obtain i where
     i_lt: "enat i < llength xs" and
     j: "\<forall>j. i \<le> j \<and> enat j < llength xs \<longrightarrow> x \<in> g (lnth xs j) \<or> x \<in> h (lnth xs j)"
     using x_in[unfolded Liminf_llist_def, simplified] by blast
 
   then have "(\<exists>i'. enat i' < llength xs \<and> (\<forall>j. i' \<le> j \<and> enat j < llength xs \<longrightarrow> x \<in> g (lnth xs j)))
      \<or> (\<exists>i'. enat i' < llength xs \<and> (\<forall>j. i' \<le> j \<and> enat j < llength xs \<longrightarrow> x \<in> h (lnth xs j)))"
     using assms[unfolded disjoint_iff_not_equal] by (metis in_lset_conv_lnth)
   then show "x \<in> ?rhs"
     unfolding Liminf_llist_def by simp
 next
   fix x
   show "x \<in> ?rhs \<Longrightarrow> x \<in> ?lhs"
     using assms unfolding Liminf_llist_def by auto
 qed
 
 lemma Liminf_set_filter_commute:
   "Liminf_llist (lmap (\<lambda>X. {x \<in> X. p x}) Xs) = {x \<in> Liminf_llist Xs. p x}"
   unfolding Liminf_llist_def by force
 
+
+subsection \<open>Liminf up-to\<close>
+
+definition Liminf_upto_llist :: "'a set llist \<Rightarrow> enat \<Rightarrow> 'a set" where
+  "Liminf_upto_llist Xs k =
+   (\<Union>i \<in> {i. enat i < llength Xs \<and> enat i \<le> k}.
+      \<Inter>j \<in> {j. i \<le> j \<and> enat j < llength Xs \<and> enat j \<le> k}. lnth Xs j)"
+
+lemma Liminf_upto_llist_eq_Liminf_llist_ltake:
+  "Liminf_upto_llist Xs j = Liminf_llist (ltake (eSuc j) Xs)"
+  unfolding Liminf_upto_llist_def Liminf_llist_def
+  by (smt Collect_cong Sup.SUP_cong iless_Suc_eq lnth_ltake less_llength_ltake mem_Collect_eq)
+
+lemma Liminf_upto_llist_nat[simp]:
+  "Liminf_upto_llist Xs (enat k) =
+   (if lnull Xs then {} else if enat k < llength Xs then lnth Xs k else llast Xs)"
+proof (cases "lnull Xs")
+  case nil: True
+  then show ?thesis
+    unfolding Liminf_upto_llist_def by simp
+next
+  case nnil: False
+  show ?thesis
+  proof (cases "enat k < llength Xs")
+    case k_lt: True
+    then show ?thesis
+      unfolding Liminf_upto_llist_def by force
+  next
+    case k_ge: False
+    then obtain j where
+      j: "eSuc (enat j) = llength Xs"
+      by (metis eSuc_enat_iff enat_ile le_less_linear lhd_LCons_ltl llength_LCons nnil)
+
+    have fin: "lfinite Xs"
+      using k_ge not_lfinite_llength by fastforce
+    have le_k: "enat i < llength Xs \<and> i \<le> k \<longleftrightarrow> enat i < llength Xs" for i
+      using k_ge linear order_le_less_subst2 by fastforce
+    have "Liminf_upto_llist Xs (enat k) = llast Xs"
+      using j nnil lfinite_Liminf_llist[OF fin] nnil
+      unfolding Liminf_upto_llist_def Liminf_llist_def using llast_conv_lnth[OF j[symmetric]]
+      by (simp add: le_k)
+    then show ?thesis
+      using k_ge nnil by simp
+  qed
+qed
+
+lemma Liminf_upto_llist_infinity[simp]: "Liminf_upto_llist Xs \<infinity> = Liminf_llist Xs"
+  unfolding Liminf_upto_llist_def Liminf_llist_def by simp
+
+lemma Liminf_upto_llist_eSuc[simp]:
+  "Liminf_upto_llist Xs (eSuc j) =
+   (case j of
+      enat k \<Rightarrow> Liminf_upto_llist Xs (enat (Suc k))
+    | \<infinity> \<Rightarrow> Liminf_llist Xs)"
+  by (auto simp: eSuc_enat split: enat.split)
+
+lemma elem_Liminf_llist_imp_Liminf_upto_llist:
+  "x \<in> Liminf_llist Xs \<Longrightarrow>
+   \<exists>i < llength Xs. \<forall>j. i \<le> j \<and> j < llength Xs \<longrightarrow> x \<in> Liminf_upto_llist Xs (enat j)"
+  unfolding Liminf_llist_def Liminf_upto_llist_def using enat_ord_simps(1) by force
+
 end
diff --git a/thys/Ordered_Resolution_Prover/Proving_Process.thy b/thys/Ordered_Resolution_Prover/Proving_Process.thy
--- a/thys/Ordered_Resolution_Prover/Proving_Process.thy
+++ b/thys/Ordered_Resolution_Prover/Proving_Process.thy
@@ -1,335 +1,336 @@
 (*  Title:       Theorem Proving Processes
     Author:      Jasmin Blanchette <j.c.blanchette at vu.nl>, 2014, 2017
     Author:      Dmitriy Traytel <traytel at inf.ethz.ch>, 2014
     Author:      Anders Schlichtkrull <andschl at dtu.dk>, 2017
     Maintainer:  Anders Schlichtkrull <andschl at dtu.dk>
 *)
 
 section \<open>Theorem Proving Processes\<close>
 
 theory Proving_Process
   imports Unordered_Ground_Resolution Lazy_List_Chain
 begin
 
 text \<open>
 This material corresponds to Section 4.1 (``Theorem Proving Processes'') of Bachmair and Ganzinger's
 chapter.
 
 The locale assumptions below capture conditions R1 to R3 of Definition 4.1.
 \<open>Rf\<close> denotes $\mathcal{R}_{\mathcal{F}}$; \<open>Ri\<close> denotes $\mathcal{R}_{\mathcal{I}}$.
 \<close>
 
 locale redundancy_criterion = inference_system +
   fixes
     Rf :: "'a clause set \<Rightarrow> 'a clause set" and
     Ri :: "'a clause set \<Rightarrow> 'a inference set"
   assumes
     Ri_subset_\<Gamma>: "Ri N \<subseteq> \<Gamma>" and
     Rf_mono: "N \<subseteq> N' \<Longrightarrow> Rf N \<subseteq> Rf N'" and
     Ri_mono: "N \<subseteq> N' \<Longrightarrow> Ri N \<subseteq> Ri N'" and
     Rf_indep: "N' \<subseteq> Rf N \<Longrightarrow> Rf N \<subseteq> Rf (N - N')" and
     Ri_indep: "N' \<subseteq> Rf N \<Longrightarrow> Ri N \<subseteq> Ri (N - N')" and
     Rf_sat: "satisfiable (N - Rf N) \<Longrightarrow> satisfiable N"
 begin
 
 definition saturated_upto :: "'a clause set \<Rightarrow> bool" where
   "saturated_upto N \<longleftrightarrow> inferences_from (N - Rf N) \<subseteq> Ri N"
 
 inductive "derive" :: "'a clause set \<Rightarrow> 'a clause set \<Rightarrow> bool" (infix "\<triangleright>" 50) where
   deduction_deletion: "N - M \<subseteq> concls_of (inferences_from M) \<Longrightarrow> M - N \<subseteq> Rf N \<Longrightarrow> M \<triangleright> N"
 
 lemma derive_subset: "M \<triangleright> N \<Longrightarrow> N \<subseteq> M \<union> concls_of (inferences_from M)"
   by (meson Diff_subset_conv derive.cases)
 
 end
 
 locale sat_preserving_redundancy_criterion =
   sat_preserving_inference_system "\<Gamma> :: ('a :: wellorder) inference set" + redundancy_criterion
 begin
 
 lemma deriv_sat_preserving:
   assumes
     deriv: "chain (\<triangleright>) Ns" and
     sat_n0: "satisfiable (lhd Ns)"
   shows "satisfiable (Sup_llist Ns)"
 proof -
   have ns0: "lnth Ns 0 = lhd Ns"
     using deriv by (metis chain_not_lnull lhd_conv_lnth)
   have len_ns: "llength Ns > 0"
     using deriv by (case_tac Ns) simp+
   {
     fix DD
     assume fin: "finite DD" and sset_lun: "DD \<subseteq> Sup_llist Ns"
-    then obtain k where dd_sset: "DD \<subseteq> Sup_upto_llist Ns k"
+    then obtain k where
+      dd_sset: "DD \<subseteq> Sup_upto_llist Ns (enat k)"
       using finite_Sup_llist_imp_Sup_upto_llist by blast
     have "satisfiable (Sup_upto_llist Ns k)"
     proof (induct k)
       case 0
       then show ?case
         using len_ns ns0 sat_n0 unfolding Sup_upto_llist_def true_clss_def by auto
     next
       case (Suc k)
       show ?case
       proof (cases "enat (Suc k) \<ge> llength Ns")
         case True
-        then have "Sup_upto_llist Ns k = Sup_upto_llist Ns (Suc k)"
-          unfolding Sup_upto_llist_def using le_Suc_eq not_less by blast
+        then have "Sup_upto_llist Ns (enat k) = Sup_upto_llist Ns (enat (Suc k))"
+          unfolding Sup_upto_llist_def using le_Suc_eq by auto
         then show ?thesis
           using Suc by simp
       next
         case False
         then have "lnth Ns k \<triangleright> lnth Ns (Suc k)"
           using deriv by (auto simp: chain_lnth_rel)
         then have "lnth Ns (Suc k) \<subseteq> lnth Ns k \<union> concls_of (inferences_from (lnth Ns k))"
           by (rule derive_subset)
         moreover have "lnth Ns k \<subseteq> Sup_upto_llist Ns k"
           unfolding Sup_upto_llist_def using False Suc_ile_eq linear by blast
         ultimately have "lnth Ns (Suc k)
           \<subseteq> Sup_upto_llist Ns k \<union> concls_of (inferences_from (Sup_upto_llist Ns k))"
           by clarsimp (metis UnCI UnE image_Un inferences_from_mono le_iff_sup)
         moreover have "Sup_upto_llist Ns (Suc k) = Sup_upto_llist Ns k \<union> lnth Ns (Suc k)"
           unfolding Sup_upto_llist_def using False by (force elim: le_SucE)
         moreover have
           "satisfiable (Sup_upto_llist Ns k \<union> concls_of (inferences_from (Sup_upto_llist Ns k)))"
           using Suc \<Gamma>_sat_preserving unfolding sat_preserving_inference_system_def by simp
         ultimately show ?thesis
           by (metis le_iff_sup true_clss_union)
       qed
     qed
     then have "satisfiable DD"
       using dd_sset unfolding Sup_upto_llist_def by (blast intro: true_clss_mono)
   }
   then show ?thesis
     using ground_resolution_without_selection.clausal_logic_compact[THEN iffD1] by metis
 qed
 
 text \<open>
 This corresponds to Lemma 4.2:
 \<close>
 
 lemma
   assumes deriv: "chain (\<triangleright>) Ns"
   shows
     Rf_Sup_subset_Rf_Liminf: "Rf (Sup_llist Ns) \<subseteq> Rf (Liminf_llist Ns)" and
     Ri_Sup_subset_Ri_Liminf: "Ri (Sup_llist Ns) \<subseteq> Ri (Liminf_llist Ns)" and
     sat_limit_iff: "satisfiable (Liminf_llist Ns) \<longleftrightarrow> satisfiable (lhd Ns)"
 proof -
   {
     fix C i j
     assume
       c_in: "C \<in> lnth Ns i" and
       c_ni: "C \<notin> Rf (Sup_llist Ns)" and
       j: "j \<ge> i" and
       j': "enat j < llength Ns"
     from c_ni have c_ni': "\<And>i. enat i < llength Ns \<Longrightarrow> C \<notin> Rf (lnth Ns i)"
       using Rf_mono lnth_subset_Sup_llist Sup_llist_def by (blast dest: contra_subsetD)
     have "C \<in> lnth Ns j"
     using j j'
     proof (induct j)
       case 0
       then show ?case
         using c_in by blast
     next
       case (Suc k)
       then show ?case
       proof (cases "i < Suc k")
         case True
         have "i \<le> k"
           using True by linarith
         moreover have "enat k < llength Ns"
           using Suc.prems(2) Suc_ile_eq by (blast intro: dual_order.strict_implies_order)
         ultimately have c_in_k: "C \<in> lnth Ns k"
           using Suc.hyps by blast
         have rel: "lnth Ns k \<triangleright> lnth Ns (Suc k)"
           using Suc.prems deriv by (auto simp: chain_lnth_rel)
         then show ?thesis
           using c_in_k c_ni' Suc.prems(2) by cases auto
       next
         case False
         then show ?thesis
           using Suc c_in by auto
       qed
     qed
   }
   then have lu_ll: "Sup_llist Ns - Rf (Sup_llist Ns) \<subseteq> Liminf_llist Ns"
     unfolding Sup_llist_def Liminf_llist_def by blast
   have rf: "Rf (Sup_llist Ns - Rf (Sup_llist Ns)) \<subseteq> Rf (Liminf_llist Ns)"
     using lu_ll Rf_mono by simp
   have ri: "Ri (Sup_llist Ns - Rf (Sup_llist Ns)) \<subseteq> Ri (Liminf_llist Ns)"
     using lu_ll Ri_mono by simp
   show "Rf (Sup_llist Ns) \<subseteq> Rf (Liminf_llist Ns)"
     using rf Rf_indep by blast
   show "Ri (Sup_llist Ns) \<subseteq> Ri (Liminf_llist Ns)"
     using ri Ri_indep by blast
 
   show "satisfiable (Liminf_llist Ns) \<longleftrightarrow> satisfiable (lhd Ns)"
   proof
     assume "satisfiable (lhd Ns)"
     then have "satisfiable (Sup_llist Ns)"
       using deriv deriv_sat_preserving by simp
     then show "satisfiable (Liminf_llist Ns)"
       using true_clss_mono[OF Liminf_llist_subset_Sup_llist] by blast
   next
     assume "satisfiable (Liminf_llist Ns)"
     then have "satisfiable (Sup_llist Ns - Rf (Sup_llist Ns))"
       using true_clss_mono[OF lu_ll] by blast
     then have "satisfiable (Sup_llist Ns)"
       using Rf_sat by blast
     then show "satisfiable (lhd Ns)"
       using deriv true_clss_mono lhd_subset_Sup_llist chain_not_lnull by metis
   qed
 qed
 
 lemma
   assumes "chain (\<triangleright>) Ns"
   shows
     Rf_limit_Sup: "Rf (Liminf_llist Ns) = Rf (Sup_llist Ns)" and
     Ri_limit_Sup: "Ri (Liminf_llist Ns) = Ri (Sup_llist Ns)"
   using assms
   by (auto simp: Rf_Sup_subset_Rf_Liminf Rf_mono Ri_Sup_subset_Ri_Liminf Ri_mono
       Liminf_llist_subset_Sup_llist subset_antisym)
 
 end
 
 text \<open>
 The assumption below corresponds to condition R4 of Definition 4.1.
 \<close>
 
 locale effective_redundancy_criterion = redundancy_criterion +
   assumes Ri_effective: "\<gamma> \<in> \<Gamma> \<Longrightarrow> concl_of \<gamma> \<in> N \<union> Rf N \<Longrightarrow> \<gamma> \<in> Ri N"
 begin
 
 definition fair_clss_seq :: "'a clause set llist \<Rightarrow> bool" where
   "fair_clss_seq Ns \<longleftrightarrow> (let N' = Liminf_llist Ns - Rf (Liminf_llist Ns) in
      concls_of (inferences_from N' - Ri N') \<subseteq> Sup_llist Ns \<union> Rf (Sup_llist Ns))"
 
 end
 
 locale sat_preserving_effective_redundancy_criterion =
   sat_preserving_inference_system "\<Gamma> :: ('a :: wellorder) inference set" +
   effective_redundancy_criterion
 begin
 
 sublocale sat_preserving_redundancy_criterion
   ..
 
 text \<open>
 The result below corresponds to Theorem 4.3.
 \<close>
 
 theorem fair_derive_saturated_upto:
   assumes
     deriv: "chain (\<triangleright>) Ns" and
     fair: "fair_clss_seq Ns"
   shows "saturated_upto (Liminf_llist Ns)"
   unfolding saturated_upto_def
 proof
   fix \<gamma>
   let ?N' = "Liminf_llist Ns - Rf (Liminf_llist Ns)"
   assume \<gamma>: "\<gamma> \<in> inferences_from ?N'"
   show "\<gamma> \<in> Ri (Liminf_llist Ns)"
   proof (cases "\<gamma> \<in> Ri ?N'")
     case True
     then show ?thesis
       using Ri_mono by blast
   next
     case False
     have "concls_of (inferences_from ?N' - Ri ?N') \<subseteq> Sup_llist Ns \<union> Rf (Sup_llist Ns)"
       using fair unfolding fair_clss_seq_def Let_def .
     then have "concl_of \<gamma> \<in> Sup_llist Ns \<union> Rf (Sup_llist Ns)"
       using False \<gamma> by auto
     moreover
     {
       assume "concl_of \<gamma> \<in> Sup_llist Ns"
       then have "\<gamma> \<in> Ri (Sup_llist Ns)"
         using \<gamma> Ri_effective inferences_from_def by blast
       then have "\<gamma> \<in> Ri (Liminf_llist Ns)"
         using deriv Ri_Sup_subset_Ri_Liminf by fast
     }
     moreover
     {
       assume "concl_of \<gamma> \<in> Rf (Sup_llist Ns)"
       then have "concl_of \<gamma> \<in> Rf (Liminf_llist Ns)"
         using deriv Rf_Sup_subset_Rf_Liminf by blast
       then have "\<gamma> \<in> Ri (Liminf_llist Ns)"
         using \<gamma> Ri_effective inferences_from_def by auto
     }
     ultimately show "\<gamma> \<in> Ri (Liminf_llist Ns)"
       by blast
   qed
 qed
 
 end
 
 text \<open>
 This corresponds to the trivial redundancy criterion defined on page 36 of
 Section 4.1.
 \<close>
 
 locale trivial_redundancy_criterion = inference_system
 begin
 
 definition Rf :: "'a clause set \<Rightarrow> 'a clause set" where
   "Rf _ = {}"
 
 definition Ri :: "'a clause set \<Rightarrow> 'a inference set" where
   "Ri N = {\<gamma>. \<gamma> \<in> \<Gamma> \<and> concl_of \<gamma> \<in> N}"
 
 sublocale effective_redundancy_criterion \<Gamma> Rf Ri
   by unfold_locales (auto simp: Rf_def Ri_def)
 
 lemma saturated_upto_iff: "saturated_upto N \<longleftrightarrow> concls_of (inferences_from N) \<subseteq> N"
   unfolding saturated_upto_def inferences_from_def Rf_def Ri_def by auto
 
 end
 
 text \<open>
 The following lemmas corresponds to the standard extension of a redundancy criterion defined on
 page 38 of Section 4.1.
 \<close>
 
 lemma redundancy_criterion_standard_extension:
   assumes "\<Gamma> \<subseteq> \<Gamma>'" and "redundancy_criterion \<Gamma> Rf Ri"
   shows "redundancy_criterion \<Gamma>' Rf (\<lambda>N. Ri N \<union> (\<Gamma>' - \<Gamma>))"
   using assms unfolding redundancy_criterion_def by (intro conjI) ((auto simp: rev_subsetD)[5], sat)
 
 lemma redundancy_criterion_standard_extension_saturated_upto_iff:
   assumes "\<Gamma> \<subseteq> \<Gamma>'" and "redundancy_criterion \<Gamma> Rf Ri"
   shows "redundancy_criterion.saturated_upto \<Gamma> Rf Ri M \<longleftrightarrow>
     redundancy_criterion.saturated_upto \<Gamma>' Rf (\<lambda>N. Ri N \<union> (\<Gamma>' - \<Gamma>)) M"
   using assms redundancy_criterion.saturated_upto_def redundancy_criterion.saturated_upto_def
     redundancy_criterion_standard_extension
   unfolding inference_system.inferences_from_def by blast
 
 lemma redundancy_criterion_standard_extension_effective:
   assumes "\<Gamma> \<subseteq> \<Gamma>'" and "effective_redundancy_criterion \<Gamma> Rf Ri"
   shows "effective_redundancy_criterion \<Gamma>' Rf (\<lambda>N. Ri N \<union> (\<Gamma>' - \<Gamma>))"
   using assms redundancy_criterion_standard_extension[of \<Gamma>]
   unfolding effective_redundancy_criterion_def effective_redundancy_criterion_axioms_def by auto
 
 lemma redundancy_criterion_standard_extension_fair_iff:
   assumes "\<Gamma> \<subseteq> \<Gamma>'" and "effective_redundancy_criterion \<Gamma> Rf Ri"
   shows "effective_redundancy_criterion.fair_clss_seq \<Gamma>' Rf (\<lambda>N. Ri N \<union> (\<Gamma>' - \<Gamma>)) Ns \<longleftrightarrow>
     effective_redundancy_criterion.fair_clss_seq \<Gamma> Rf Ri Ns"
   using assms redundancy_criterion_standard_extension_effective[of \<Gamma> \<Gamma>' Rf Ri]
     effective_redundancy_criterion.fair_clss_seq_def[of \<Gamma> Rf Ri Ns]
     effective_redundancy_criterion.fair_clss_seq_def[of \<Gamma>' Rf "(\<lambda>N. Ri N \<union> (\<Gamma>' - \<Gamma>))" Ns]
   unfolding inference_system.inferences_from_def Let_def by auto
 
 theorem redundancy_criterion_standard_extension_fair_derive_saturated_upto:
   assumes
     subs: "\<Gamma> \<subseteq> \<Gamma>'" and
     red: "redundancy_criterion \<Gamma> Rf Ri" and
     red': "sat_preserving_effective_redundancy_criterion \<Gamma>' Rf (\<lambda>N. Ri N \<union> (\<Gamma>' - \<Gamma>))" and
     deriv: "chain (redundancy_criterion.derive \<Gamma>' Rf) Ns" and
     fair: "effective_redundancy_criterion.fair_clss_seq \<Gamma>' Rf (\<lambda>N. Ri N \<union> (\<Gamma>' - \<Gamma>)) Ns"
   shows "redundancy_criterion.saturated_upto \<Gamma> Rf Ri (Liminf_llist Ns)"
 proof -
   have "redundancy_criterion.saturated_upto \<Gamma>' Rf (\<lambda>N. Ri N \<union> (\<Gamma>' - \<Gamma>)) (Liminf_llist Ns)"
     by (rule sat_preserving_effective_redundancy_criterion.fair_derive_saturated_upto
         [OF red' deriv fair])
   then show ?thesis
     by (rule redundancy_criterion_standard_extension_saturated_upto_iff[THEN iffD2, OF subs red])
 qed
 
 end
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,950 +1,950 @@
 (*  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 fair :: "'f set llist \<Rightarrow> bool" where
   "fair D \<longleftrightarrow> Inf_from (Liminf_llist D) \<subseteq> Sup_llist (lmap Red_Inf 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"
+  obtain i where C_D_i: "C \<in> Sup_upto_llist D (enat i)" and "enat 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
+  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_upto_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_llist (lmap Red_Inf 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_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"
 begin
 
 lemma dynamic_refutational_complete_Liminf:
   fixes B D
   assumes
     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>
   shows \<open>\<exists>B'\<in>Bot. B' \<in> Liminf_llist D\<close>
 proof -
   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 show ?thesis
     using bot_elem static_refutational_complete Liminf_entails_Bot by auto
 qed
 
 end
 
 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"
 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_llist (lmap Red_Inf D) = Red_Inf N" by (simp add: D_def)
   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
     \<open>B \<in> Bot\<close> and
     \<open>chain (\<rhd>Red) D\<close> and
     \<open>fair D\<close> and
     \<open>lnth D 0 \<Turnstile> {B}\<close>
   then have \<open>\<exists>B'\<in>Bot. B' \<in> Liminf_llist D\<close>
     by (rule dynamic_refutational_complete_Liminf)
   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 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"
         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}"
         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}"
         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 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 "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 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
 
 lemma sup_red_f_in_red_liminf:
   "chain derive D \<Longrightarrow> Sup_llist (lmap Red_F D) \<subseteq> Red_F (Liminf_llist D)"
 proof
   fix N
   assume
     deriv: "chain derive D" and
     n_in_sup: "N \<in> Sup_llist (lmap Red_F D)"
   obtain i0 where i_smaller: "enat i0 < llength D" and n_in: "N \<in> Red_F (lnth D i0)"
     using n_in_sup by (metis Sup_llist_imp_exists_index llength_lmap lnth_lmap)
   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_llist (lmap Red_Inf D) \<subseteq> Red_Inf (Liminf_llist D)"
 proof
   fix \<iota>
   assume
     deriv: "chain derive D" and
     i_in_sup: "\<iota> \<in> Sup_llist (lmap Red_Inf 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_llist_def by auto
   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_llist (lmap Red_F D)) \<subseteq> Sup_llist (lmap Red_Inf 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_llist (lmap Red_F 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_llist (lmap Red_Inf 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_llist (lmap Red_F D) = Red_F N" by (simp add: D_def)
   moreover have "Sup_llist (lmap Red_Inf D) = Red_Inf N" by (simp add: D_def)
   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