diff --git a/thys/FOL_Seq_Calc3/Completeness.thy b/thys/FOL_Seq_Calc3/Completeness.thy
new file mode 100644
--- /dev/null
+++ b/thys/FOL_Seq_Calc3/Completeness.thy
@@ -0,0 +1,281 @@
+section \<open>Completeness\<close>
+
+theory Completeness imports Prover Semantics begin
+
+subsection \<open>Hintikka Counter Model\<close>
+
+locale Hintikka =
+  fixes A B :: \<open>fm set\<close>
+  assumes
+    Basic: \<open>\<^bold>\<ddagger>n ts \<in> A \<Longrightarrow> \<^bold>\<ddagger>n ts \<in> B \<Longrightarrow> False\<close> and
+    FlsA: \<open>\<^bold>\<bottom> \<notin> A\<close> and
+    ImpA: \<open>p \<^bold>\<longrightarrow> q \<in> A \<Longrightarrow> p \<in> B \<or> q \<in> A\<close> and
+    ImpB: \<open>p \<^bold>\<longrightarrow> q \<in> B \<Longrightarrow> p \<in> A \<and> q \<in> B\<close> and
+    UniA: \<open>\<^bold>\<forall>p \<in> A \<Longrightarrow> \<forall>t. p\<langle>t/0\<rangle> \<in> A\<close> and
+    UniB: \<open>\<^bold>\<forall>p \<in> B \<Longrightarrow> \<exists>t. p\<langle>t/0\<rangle> \<in> B\<close>
+
+abbreviation \<open>M A \<equiv> \<lbrakk>\<^bold>#, \<^bold>\<dagger>, \<lambda>n ts. \<^bold>\<ddagger>n ts \<in> A\<rbrakk>\<close>
+
+lemma id_tm [simp]: \<open>\<lparr>\<^bold>#, \<^bold>\<dagger>\<rparr> t = t\<close>
+  by (induct t) (auto cong: map_cong)
+
+lemma size_sub [simp]: \<open>size (p\<langle>t/i\<rangle>) = size p\<close>
+  by (induct p arbitrary: i t) auto
+
+theorem Hintikka_counter_model:
+  assumes \<open>Hintikka A B\<close>
+  shows \<open>(p \<in> A \<longrightarrow> M A p) \<and> (p \<in> B \<longrightarrow> \<not> M A p)\<close>
+proof (induct p rule: wf_induct [where r=\<open>measure size\<close>])
+  case 1
+  then show ?case ..
+next
+  case (2 x)
+  then show ?case
+  proof (cases x; safe del: notI)
+    case Falsity
+    show \<open>\<^bold>\<bottom> \<in> A \<Longrightarrow> M A \<^bold>\<bottom>\<close> \<open>\<^bold>\<bottom> \<in> B \<Longrightarrow> \<not> M A \<^bold>\<bottom>\<close>
+      using Hintikka.FlsA assms by simp_all
+  next
+    case (Pre n ts)
+    show \<open>\<^bold>\<ddagger>n ts \<in> A \<Longrightarrow> M A (\<^bold>\<ddagger>n ts)\<close> \<open>\<^bold>\<ddagger>n ts \<in> B \<Longrightarrow> \<not> M A (\<^bold>\<ddagger>n ts)\<close>
+      using Hintikka.Basic assms by (auto cong: map_cong)
+  next
+    case (Imp p q)
+    show \<open>p \<^bold>\<longrightarrow> q \<in> A \<Longrightarrow> M A (p \<^bold>\<longrightarrow> q)\<close> \<open>p \<^bold>\<longrightarrow> q \<in> B \<Longrightarrow> \<not> M A (p \<^bold>\<longrightarrow> q)\<close>
+      using assms Hintikka.ImpA[of A B p q] Hintikka.ImpB[of A B p q] Imp 2 by auto
+  next
+    case (Uni p)
+    have \<open>p\<langle>t/0\<rangle> \<in> A \<Longrightarrow> M A (p\<langle>t/0\<rangle>)\<close> \<open>p\<langle>t/0\<rangle> \<in> B \<Longrightarrow> \<not> M A (p\<langle>t/0\<rangle>)\<close> for t
+      using Uni 2 by (metis fm.size(8) in_measure lessI less_add_same_cancel1 size_sub)+
+    then show \<open>\<^bold>\<forall>p \<in> A \<Longrightarrow> M A (\<^bold>\<forall>p)\<close> \<open>\<^bold>\<forall>p \<in> B \<Longrightarrow> \<not> M A (\<^bold>\<forall>p)\<close>
+      using assms Hintikka.UniA[of A B p] Hintikka.UniB[of A B p] by auto
+  qed
+qed
+
+subsection \<open>Escape Paths Form Hintikka Sets\<close>
+
+lemma sset_sdrop: \<open>sset (sdrop n s) \<subseteq> sset s\<close>
+  by (induct n arbitrary: s) (auto intro: stl_sset in_mono)
+
+lemma epath_sdrop: \<open>epath steps \<Longrightarrow> epath (sdrop n steps)\<close>
+  by (induct n) (auto elim: epath.cases)
+
+lemma eff_preserves_Pre:
+  assumes \<open>effStep ((A, B), r) ss\<close> \<open>(A', B') |\<in>| ss\<close>
+  shows \<open>(\<^bold>\<ddagger>n ts [\<in>] A \<Longrightarrow> \<^bold>\<ddagger>n ts [\<in>] A')\<close> \<open>\<^bold>\<ddagger>n ts [\<in>] B \<Longrightarrow> \<^bold>\<ddagger>n ts [\<in>] B'\<close>
+  using assms by (induct r \<open>(A, B)\<close> rule: eff.induct) (auto split: if_splits)
+
+lemma epath_eff:
+  assumes \<open>epath steps\<close> \<open>effStep (shd steps) ss\<close>
+  shows \<open>fst (shd (stl steps)) |\<in>| ss\<close>
+  using assms by (auto elim: epath.cases)
+
+abbreviation \<open>lhs s \<equiv> fst (fst s)\<close>
+abbreviation \<open>rhs s \<equiv> snd (fst s)\<close>
+abbreviation \<open>lhsd s \<equiv> lhs (shd s)\<close>
+abbreviation \<open>rhsd s \<equiv> rhs (shd s)\<close>
+
+lemma epath_Pre_sdrop:
+  assumes \<open>epath steps\<close> shows
+    \<open>\<^bold>\<ddagger>n ts [\<in>] lhs (shd steps) \<Longrightarrow> \<^bold>\<ddagger>n ts [\<in>] lhsd (sdrop m steps)\<close>
+    \<open>\<^bold>\<ddagger>n ts [\<in>] rhs (shd steps) \<Longrightarrow> \<^bold>\<ddagger>n ts [\<in>] rhsd (sdrop m steps)\<close>
+  using assms eff_preserves_Pre
+  by (induct m arbitrary: steps) (simp; metis (no_types, lifting) epath.cases surjective_pairing)+
+
+lemma Saturated_sdrop:
+  assumes \<open>Saturated steps\<close>
+  shows \<open>Saturated (sdrop n steps)\<close>
+  using assms unfolding Saturated_def saturated_def by (simp add: alw_iff_sdrop)
+
+definition treeA :: \<open>(sequent \<times> rule) stream \<Rightarrow> fm set\<close> where
+  \<open>treeA steps \<equiv> \<Union>s \<in> sset steps. set (lhs s)\<close>
+
+definition treeB :: \<open>(sequent \<times> rule) stream \<Rightarrow> fm set\<close> where
+  \<open>treeB steps \<equiv> \<Union>s \<in> sset steps. set (rhs s)\<close>
+
+lemma treeA_snth: \<open>p \<in> treeA steps \<Longrightarrow> \<exists>n. p [\<in>] lhsd (sdrop n steps)\<close>
+  unfolding treeA_def using sset_range[of steps] by simp
+
+lemma treeB_snth: \<open>p \<in> treeB steps \<Longrightarrow> \<exists>n. p [\<in>] rhsd (sdrop n steps)\<close>
+  unfolding treeB_def using sset_range[of steps] by simp
+
+lemma treeA_sdrop: \<open>treeA (sdrop n steps) \<subseteq> treeA steps\<close>
+  unfolding treeA_def by (induct n) (simp, metis SUP_subset_mono order_refl sset_sdrop)
+
+lemma treeB_sdrop: \<open>treeB (sdrop n steps) \<subseteq> treeB steps\<close>
+  unfolding treeB_def by (induct n) (simp, metis SUP_subset_mono order_refl sset_sdrop)
+
+lemma enabled_ex_taken:
+  assumes \<open>epath steps\<close> \<open>Saturated steps\<close> \<open>enabled r (fst (shd steps))\<close>
+  shows \<open>\<exists>k. takenAtStep r (shd (sdrop k steps))\<close>
+  using assms unfolding Saturated_def saturated_def UNIV_rules by (auto simp: ev_iff_sdrop)
+
+lemma Hintikka_epath:
+  assumes \<open>epath steps\<close> \<open>Saturated steps\<close>
+  shows \<open>Hintikka (treeA steps) (treeB steps)\<close>
+proof
+  fix n ts
+  assume \<open>\<^bold>\<ddagger>n ts \<in> treeA steps\<close>
+  then obtain m where m: \<open>\<^bold>\<ddagger>n ts [\<in>] lhsd (sdrop m steps)\<close>
+    using treeA_snth by auto
+
+  assume \<open>\<^bold>\<ddagger>n ts \<in> treeB steps\<close>
+  then obtain k where k: \<open>\<^bold>\<ddagger>n ts [\<in>] rhsd (sdrop k steps)\<close>
+    using treeB_snth by auto
+
+  let ?j = \<open>m + k\<close>
+  let ?jstep = \<open>shd (sdrop ?j steps)\<close>
+
+  have \<open>\<^bold>\<ddagger>n ts [\<in>] lhs ?jstep\<close>
+    using assms m epath_sdrop epath_Pre_sdrop by (metis (no_types, lifting) sdrop_add)
+  moreover have \<open>\<^bold>\<ddagger>n ts [\<in>] rhs ?jstep\<close>
+    using assms k epath_sdrop epath_Pre_sdrop by (metis (no_types, lifting) add.commute sdrop_add)
+  ultimately have \<open>enabled (Axiom n ts) (fst ?jstep)\<close>
+    unfolding enabled_def by (metis eff.simps(2) prod.exhaust_sel)
+  then obtain j' where \<open>takenAtStep (Axiom n ts) (shd (sdrop j' steps))\<close>
+    using enabled_ex_taken[OF epath_sdrop[OF assms(1)] Saturated_sdrop[OF assms(2)]] by auto
+  then have \<open>eff (snd (shd (sdrop j' steps))) (fst (shd (sdrop j' steps))) = None\<close>
+    using assms(1) epath_sdrop epath_eff
+    by (metis (no_types, lifting) eff.simps(2) epath.simps equalsffemptyD surjective_pairing)
+  then show False
+    using assms(1) epath_sdrop by (metis epath.cases option.discI)
+next
+  show \<open>\<^bold>\<bottom> \<notin> treeA steps\<close>
+  proof
+    assume \<open>\<^bold>\<bottom> \<in> treeA steps\<close>
+    then have \<open>\<exists>j. enabled FlsL (fst (shd (sdrop j steps)))\<close>
+      unfolding enabled_def using treeA_snth by (metis eff.simps(3) prod.exhaust_sel sdrop_simps(1))
+    then obtain j where \<open>takenAtStep FlsL (shd (sdrop j steps))\<close> (is \<open>takenAtStep _ (shd ?steps)\<close>)
+      using enabled_ex_taken[OF epath_sdrop[OF assms(1)] Saturated_sdrop[OF assms(2)]] by auto
+    then have \<open>eff (snd (shd ?steps)) (fst (shd ?steps)) = None\<close>
+      using assms(1) epath_sdrop epath_eff
+      by (metis (no_types, lifting) eff.simps(3) epath.simps equalsffemptyD surjective_pairing)
+    then show False
+      using assms(1) epath_sdrop by (metis epath.cases option.discI)
+  qed
+next
+  fix p q
+  assume \<open>p \<^bold>\<longrightarrow> q \<in> treeA steps\<close>
+  then have \<open>\<exists>k. enabled (ImpL p q) (fst (shd (sdrop k steps)))\<close>
+    unfolding enabled_def using treeA_snth by (metis eff.simps(5) prod.exhaust_sel sdrop_simps(1))
+  then obtain j where \<open>takenAtStep (ImpL p q) (shd (sdrop j steps))\<close> (is \<open>takenAtStep _ (shd ?s)\<close>)
+    using enabled_ex_taken[OF epath_sdrop[OF assms(1)] Saturated_sdrop[OF assms(2)]] by auto
+  then have \<open>fst (shd (stl ?s)) |\<in>|
+      {| (lhsd ?s [\<div>] (p \<^bold>\<longrightarrow> q), p # rhsd ?s), (q # lhsd ?s [\<div>] (p \<^bold>\<longrightarrow> q), rhsd ?s) |}\<close>
+    using assms(1) epath_sdrop epath_eff
+    by (metis (no_types, lifting) eff.simps(5) epath.cases option.distinct(1) prod.collapse)
+  then have \<open>p [\<in>] rhs (shd (stl ?s)) \<or> q [\<in>] lhs (shd (stl ?s))\<close>
+    by auto
+  then have \<open>p \<in> treeB (stl ?s) \<or> q \<in> treeA (stl ?s)\<close>
+    unfolding treeA_def treeB_def by (meson UN_I shd_sset)
+  then show \<open>p \<in> treeB steps \<or> q \<in> treeA steps\<close>
+    using treeA_sdrop treeB_sdrop by (metis sdrop_simps(2) subsetD)
+next
+  fix p q
+  assume \<open>p \<^bold>\<longrightarrow> q \<in> treeB steps\<close>
+  then have \<open>\<exists>k. enabled (ImpR p q) (fst (shd (sdrop k steps)))\<close>
+    unfolding enabled_def using treeB_snth by (metis eff.simps(6) prod.exhaust_sel sdrop_simps(1))
+  then obtain j where \<open>takenAtStep (ImpR p q) (shd (sdrop j steps))\<close> (is \<open>takenAtStep _ (shd ?s)\<close>)
+    using enabled_ex_taken[OF epath_sdrop[OF assms(1)] Saturated_sdrop[OF assms(2)]] by auto
+  then have \<open>fst (shd (stl ?s)) |\<in>| {| (p # lhsd ?s, q # rhsd ?s [\<div>] (p \<^bold>\<longrightarrow> q)) |}\<close>
+    using assms(1) epath_sdrop epath_eff
+    by (metis (no_types, lifting) eff.simps(6) epath.cases option.distinct(1) prod.collapse)
+  then have \<open>p [\<in>] lhs (shd (stl ?s)) \<and> q [\<in>] rhs (shd (stl ?s))\<close>
+    by auto
+  then have \<open>p \<in> treeA (stl ?s) \<and> q \<in> treeB (stl ?s)\<close>
+    unfolding treeA_def treeB_def by (meson UN_I shd_sset)
+  then show \<open>p \<in> treeA steps \<and> q \<in> treeB steps\<close>
+    using treeA_sdrop treeB_sdrop by (metis sdrop_simps(2) subsetD)
+next
+  fix p
+  assume *: \<open>\<^bold>\<forall>p \<in> treeA steps\<close>
+  show \<open>\<forall>t. p\<langle>t/0\<rangle> \<in> treeA steps\<close>
+  proof
+    fix t
+    from * have \<open>\<exists>k. enabled (UniL t p) (fst (shd (sdrop k steps)))\<close>
+      unfolding enabled_def using treeA_snth by (metis eff.simps(7) prod.exhaust_sel sdrop_simps(1))
+    then obtain j where \<open>takenAtStep (UniL t p) (shd (sdrop j steps))\<close>(is \<open>takenAtStep _ (shd ?s)\<close>)
+      using enabled_ex_taken[OF epath_sdrop[OF assms(1)] Saturated_sdrop[OF assms(2)]] by auto
+    then have \<open>fst (shd (stl ?s)) |\<in>| {| (p\<langle>t/0\<rangle> # lhsd ?s, rhsd ?s) |}\<close>
+      using assms(1) epath_sdrop epath_eff
+      by (metis (no_types, lifting) eff.simps(7) epath.cases option.distinct(1) prod.collapse)
+    then have \<open>p\<langle>t/0\<rangle> [\<in>] lhs (shd (stl ?s))\<close>
+      by auto
+    then have \<open>p\<langle>t/0\<rangle> \<in> treeA (stl ?s)\<close>
+      unfolding treeA_def by (meson UN_I shd_sset)
+    then show \<open>p\<langle>t/0\<rangle> \<in> treeA steps\<close>
+      using treeA_sdrop by (metis sdrop_simps(2) subsetD)
+  qed
+next
+  fix p
+  assume *: \<open>\<^bold>\<forall>p \<in> treeB steps\<close>
+  then have \<open>\<exists>k. enabled (UniR p) (fst (shd (sdrop k steps)))\<close>
+    unfolding enabled_def using treeB_snth by (metis eff.simps(8) prod.exhaust_sel sdrop_simps(1))
+  then obtain j where \<open>takenAtStep (UniR p) (shd (sdrop j steps))\<close>(is \<open>takenAtStep _ (shd ?s)\<close>)
+    using enabled_ex_taken[OF epath_sdrop[OF assms(1)] Saturated_sdrop[OF assms(2)]] by auto
+  then have \<open>fst (shd (stl ?s)) |\<in>|
+        {| (lhsd ?s, p\<langle>\<^bold>#(fresh (lhsd ?s @ rhsd ?s))/0\<rangle> # rhsd ?s [\<div>] \<^bold>\<forall>p) |}\<close>
+    using assms(1) epath_sdrop epath_eff
+    by (metis (no_types, lifting) eff.simps(8) epath.cases option.distinct(1) prod.collapse)
+  then have \<open>\<exists>t. p\<langle>t/0\<rangle> [\<in>] rhs (shd (stl ?s))\<close>
+    by auto
+  then have \<open>\<exists>t. p\<langle>t/0\<rangle> \<in> treeB (stl ?s)\<close>
+    unfolding treeB_def by (meson UN_I shd_sset)
+  then show \<open>\<exists>t. p\<langle>t/0\<rangle> \<in> treeB steps\<close>
+    using treeB_sdrop by (metis sdrop_simps(2) subsetD)
+qed
+
+subsection \<open>Completeness\<close>
+
+lemma fair_stream_rules: \<open>Fair_Stream.fair rules\<close>
+  unfolding rules_def using fair_stream surj_rule_of_nat .
+
+lemma fair_rules: \<open>fair rules\<close>
+  using fair_stream_rules unfolding Fair_Stream.fair_def fair_def alw_iff_sdrop ev_holds_sset
+  by (metis dual_order.refl le_Suc_ex sdrop_snth snth_sset)
+
+lemma epath_prover:
+  fixes A B :: \<open>fm list\<close>
+  defines \<open>t \<equiv> prover (A, B)\<close>
+  shows \<open>(fst (root t) = (A, B) \<and> wf t \<and> tfinite t) \<or>
+    (\<exists>steps. fst (shd steps) = (A, B) \<and> epath steps \<and> Saturated steps)\<close> (is \<open>?A \<or> ?B\<close>)
+proof -
+  { assume \<open>\<not> ?A\<close>
+    with assms have \<open>\<not> tfinite (mkTree rules (A, B))\<close>
+      unfolding prover_def using wf_mkTree fair_rules by simp
+    then obtain steps where \<open>ipath (mkTree rules (A, B)) steps\<close> using Konig by blast
+    with assms have \<open>fst (shd steps) = (A, B) \<and> epath steps \<and> Saturated steps\<close>
+      by (metis (no_types, lifting) fair_rules UNIV_I fst_conv ipath.cases
+          ipath_mkTree_Saturated mkTree.simps(1) wf_ipath_epath wf_mkTree)
+    then have ?B by blast
+  }
+  then show ?thesis by blast
+qed
+
+lemma epath_countermodel:
+  assumes \<open>fst (shd steps) = (A, B)\<close> \<open>epath steps\<close> \<open>Saturated steps\<close>
+  shows \<open>\<exists>(E :: _ \<Rightarrow> tm) F G. \<not> sc (E, F, G) (A, B)\<close>
+proof -
+  have \<open>Hintikka (treeA steps) (treeB steps)\<close> (is \<open>Hintikka ?A ?B\<close>)
+    using assms Hintikka_epath assms by simp
+  moreover have \<open>\<forall>p [\<in>] A. p \<in> ?A\<close> \<open>\<forall>p [\<in>] B. p \<in> ?B\<close>
+    using assms shd_sset unfolding treeA_def treeB_def by fastforce+
+  ultimately have \<open>\<forall>p [\<in>] A. M ?A p\<close> \<open>\<forall>p [\<in>] B. \<not> M ?A p\<close>
+    using Hintikka_counter_model assms by blast+
+  then show ?thesis
+    by auto
+qed
+
+theorem prover_completeness:
+  assumes \<open>\<forall>(E :: _ \<Rightarrow> tm) F G. sc (E, F, G) (A, B)\<close>
+  defines \<open>t \<equiv> prover (A, B)\<close>
+  shows \<open>fst (root t) = (A, B) \<and> wf t \<and> tfinite t\<close>
+  using assms epath_prover epath_countermodel by blast
+
+corollary
+  assumes \<open>\<forall>(E :: _ \<Rightarrow> tm) F G. \<lbrakk>E, F, G\<rbrakk> p\<close>
+  defines \<open>t \<equiv> prover ([], [p])\<close>
+  shows \<open>fst (root t) = ([], [p]) \<and> wf t \<and> tfinite t\<close>
+  using assms prover_completeness by simp
+
+end
diff --git a/thys/FOL_Seq_Calc3/Encoding.thy b/thys/FOL_Seq_Calc3/Encoding.thy
new file mode 100644
--- /dev/null
+++ b/thys/FOL_Seq_Calc3/Encoding.thy
@@ -0,0 +1,115 @@
+section \<open>Encoding\<close>
+
+theory Encoding imports "HOL-Library.Nat_Bijection" Syntax begin
+
+abbreviation infix_sum_encode (infixr \<open>$\<close> 100) where
+  \<open>c $ x \<equiv> sum_encode (c x)\<close>
+
+lemma lt_sum_encode_Inr: \<open>n < Inr $ n\<close>
+  unfolding sum_encode_def by simp
+
+lemma sum_prod_decode_lt [simp]: \<open>sum_decode n = Inr b \<Longrightarrow> (x, y) = prod_decode b \<Longrightarrow> y < Suc n\<close>
+  by (metis le_prod_encode_2 less_Suc_eq lt_sum_encode_Inr order_le_less_trans
+      prod_decode_inverse sum_decode_inverse)
+
+lemma sum_prod_decode_lt_Suc [simp]:
+  \<open>sum_decode n = Inr b \<Longrightarrow> (Suc x, y) = prod_decode b \<Longrightarrow> x < Suc n\<close>
+  by (metis dual_order.strict_trans le_prod_encode_1 lessI linorder_not_less lt_sum_encode_Inr
+      not_less_eq prod_decode_inverse sum_decode_inverse)
+
+lemma lt_list_encode: \<open>n [\<in>] ns \<Longrightarrow> n < list_encode ns\<close>
+proof (induct ns)
+  case (Cons m ns)
+  then show ?case
+    using le_prod_encode_1 le_prod_encode_2
+    by (metis dual_order.strict_trans1 le_imp_less_Suc less_SucI list_encode.simps(2) set_ConsD)
+qed simp
+
+lemma prod_Suc_list_decode_lt [simp]:
+  \<open>(x, Suc y) = prod_decode n \<Longrightarrow> y' [\<in>] (list_decode y) \<Longrightarrow> y' < n\<close>
+  by (metis Suc_le_lessD lt_list_encode le_prod_encode_2 list_decode_inverse order_less_trans
+      prod_decode_inverse)
+
+subsection \<open>Terms\<close>
+
+primrec nat_of_tm :: \<open>tm \<Rightarrow> nat\<close> where
+  \<open>nat_of_tm (\<^bold>#n) = prod_encode (n, 0)\<close>
+| \<open>nat_of_tm (\<^bold>\<dagger>f ts) = prod_encode (f, Suc (list_encode (map nat_of_tm ts)))\<close>
+
+function tm_of_nat :: \<open>nat \<Rightarrow> tm\<close> where
+  \<open>tm_of_nat n = (case prod_decode n of
+    (n, 0) \<Rightarrow> \<^bold>#n
+  | (f, Suc ts) \<Rightarrow> \<^bold>\<dagger>f (map tm_of_nat (list_decode ts)))\<close>
+  by pat_completeness auto
+termination by (relation \<open>measure id\<close>) simp_all
+
+lemma tm_nat: \<open>tm_of_nat (nat_of_tm t) = t\<close>
+  by (induct t) (simp_all add: map_idI)
+
+lemma surj_tm_of_nat: \<open>surj tm_of_nat\<close>
+  unfolding surj_def using tm_nat by metis
+
+subsection \<open>Formulas\<close>
+
+primrec nat_of_fm :: \<open>fm \<Rightarrow> nat\<close> where
+  \<open>nat_of_fm \<^bold>\<bottom> = 0\<close>
+| \<open>nat_of_fm (\<^bold>\<ddagger>P ts) = Suc (Inl $ prod_encode (P, list_encode (map nat_of_tm ts)))\<close>
+| \<open>nat_of_fm (p \<^bold>\<longrightarrow> q) = Suc (Inr $ prod_encode (Suc (nat_of_fm p), nat_of_fm q))\<close>
+| \<open>nat_of_fm (\<^bold>\<forall>p) = Suc (Inr $ prod_encode (0, nat_of_fm p))\<close>
+
+function fm_of_nat :: \<open>nat \<Rightarrow> fm\<close> where
+  \<open>fm_of_nat 0 = \<^bold>\<bottom>\<close>
+| \<open>fm_of_nat (Suc n) = (case sum_decode n of
+    Inl n \<Rightarrow> let (P, ts) = prod_decode n in \<^bold>\<ddagger>P (map tm_of_nat (list_decode ts))
+  | Inr n \<Rightarrow> (case prod_decode n of
+      (Suc p, q) \<Rightarrow> fm_of_nat p \<^bold>\<longrightarrow> fm_of_nat q
+    | (0, p) \<Rightarrow> \<^bold>\<forall>(fm_of_nat p)))\<close>
+  by pat_completeness auto
+termination by (relation \<open>measure id\<close>) simp_all
+
+lemma fm_nat: \<open>fm_of_nat (nat_of_fm p) = p\<close>
+  using tm_nat by (induct p) (simp_all add: map_idI)
+
+lemma surj_fm_of_nat: \<open>surj fm_of_nat\<close>
+  unfolding surj_def using fm_nat by metis
+
+subsection \<open>Rules\<close>
+
+text \<open>Pick a large number to help encode the Idle rule, so that we never hit it in practice.\<close>
+
+definition idle_nat :: nat where
+  \<open>idle_nat \<equiv> 4294967295\<close>
+
+primrec nat_of_rule :: \<open>rule \<Rightarrow> nat\<close> where
+  \<open>nat_of_rule Idle = Inl $ prod_encode (0, idle_nat)\<close>
+| \<open>nat_of_rule (Axiom n ts) = Inl $ prod_encode (Suc n, Suc (list_encode (map nat_of_tm ts)))\<close>
+| \<open>nat_of_rule FlsL = Inl $ prod_encode (0, 0)\<close>
+| \<open>nat_of_rule FlsR = Inl $ prod_encode (0, Suc 0)\<close>
+| \<open>nat_of_rule (ImpL p q) = Inr $ prod_encode (Inl $ nat_of_fm p, Inl $ nat_of_fm q)\<close>
+| \<open>nat_of_rule (ImpR p q) = Inr $ prod_encode (Inr $ nat_of_fm p, nat_of_fm q)\<close>
+| \<open>nat_of_rule (UniL t p) = Inr $ prod_encode (Inl $ nat_of_tm t, Inr $ nat_of_fm p)\<close>
+| \<open>nat_of_rule (UniR p) = Inl $ prod_encode (Suc (nat_of_fm p), 0)\<close>
+
+fun rule_of_nat :: \<open>nat \<Rightarrow> rule\<close> where
+  \<open>rule_of_nat n = (case sum_decode n of
+    Inl n \<Rightarrow> (case prod_decode n of
+      (0, 0) \<Rightarrow> FlsL
+    | (0, Suc 0) \<Rightarrow> FlsR
+    | (0, n2) \<Rightarrow> if n2 = idle_nat then Idle else
+      let (p, q) = prod_decode n2 in ImpR (fm_of_nat p) (fm_of_nat q)
+    | (Suc n, Suc ts) \<Rightarrow> Axiom n (map tm_of_nat (list_decode ts))
+    | (Suc p, 0) \<Rightarrow> UniR (fm_of_nat p))
+  | Inr n \<Rightarrow> (let (n1, n2) = prod_decode n in
+    case sum_decode n1 of
+      Inl n1 \<Rightarrow> (case sum_decode n2 of
+        Inl q \<Rightarrow> ImpL (fm_of_nat n1) (fm_of_nat q)
+      | Inr p \<Rightarrow> UniL (tm_of_nat n1) (fm_of_nat p))
+    | Inr p \<Rightarrow> ImpR (fm_of_nat p) (fm_of_nat n2)))\<close>
+
+lemma rule_nat: \<open>rule_of_nat (nat_of_rule r) = r\<close>
+  using tm_nat fm_nat by (cases r) (simp_all add: map_idI idle_nat_def)
+
+lemma surj_rule_of_nat: \<open>surj rule_of_nat\<close>
+  unfolding surj_def using rule_nat by metis
+
+end
diff --git a/thys/FOL_Seq_Calc3/Export.thy b/thys/FOL_Seq_Calc3/Export.thy
new file mode 100644
--- /dev/null
+++ b/thys/FOL_Seq_Calc3/Export.thy
@@ -0,0 +1,61 @@
+section \<open>Export\<close>
+
+theory Export imports Prover begin
+
+definition \<open>prove_sequent \<equiv> i.mkTree eff rules\<close>
+definition \<open>prove \<equiv> \<lambda>p. prove_sequent ([], [p])\<close>
+
+declare Stream.smember_code [code del]
+lemma [code]: \<open>Stream.smember x (y ## s) = (x = y \<or> Stream.smember x s)\<close>
+  unfolding Stream.smember_def by auto
+
+code_printing
+  constant the \<rightharpoonup> (Haskell) "(\\x -> case x of { Just y -> y })"
+  | constant Option.is_none \<rightharpoonup> (Haskell) "(\\x -> case x of { Just y -> False; Nothing -> True })"
+
+code_identifier
+  code_module Product_Type \<rightharpoonup> (Haskell) Arith
+  | code_module Orderings \<rightharpoonup> (Haskell) Arith
+  | code_module Arith \<rightharpoonup> (Haskell) Prover
+  | code_module MaybeExt \<rightharpoonup> (Haskell) Prover
+  | code_module List \<rightharpoonup> (Haskell) Prover
+  | code_module Nat_Bijection \<rightharpoonup> (Haskell) Prover
+  | code_module Syntax \<rightharpoonup> (Haskell) Prover
+  | code_module Encoding \<rightharpoonup> (Haskell) Prover
+  | code_module HOL \<rightharpoonup> (Haskell) Prover
+  | code_module Set \<rightharpoonup> (Haskell) Prover
+  | code_module FSet \<rightharpoonup> (Haskell) Prover
+  | code_module Stream \<rightharpoonup> (Haskell) Prover
+  | code_module Fair_Stream \<rightharpoonup> (Haskell) Prover
+  | code_module Sum_Type \<rightharpoonup> (Haskell) Prover
+  | code_module Abstract_Completeness \<rightharpoonup> (Haskell) Prover
+  | code_module Export \<rightharpoonup> (Haskell) Prover
+
+export_code open prove in Haskell
+
+text \<open>
+To export the Haskell code run:
+\begin{verbatim}
+  > isabelle build -e -D .
+\end{verbatim}
+
+To compile the exported code run:
+\begin{verbatim}
+  > ghc -O2 -i./program Main.hs
+\end{verbatim}
+
+To prove a formula, supply it using raw constructor names, e.g.:
+\begin{verbatim}
+  > ./Main "Imp (Pre 0 []) (Imp (Pre 1 []) (Pre 0 []))"
+  |- (P) --> ((Q) --> (P))
+  + ImpR on P and (Q) --> (P)
+  P |- (Q) --> (P)
+  + ImpR on Q and P
+  Q, P |- P
+ + Axiom on P
+\end{verbatim}
+
+The output is pretty-printed.
+\<close>
+
+end
diff --git a/thys/FOL_Seq_Calc3/Fair_Stream.thy b/thys/FOL_Seq_Calc3/Fair_Stream.thy
new file mode 100644
--- /dev/null
+++ b/thys/FOL_Seq_Calc3/Fair_Stream.thy
@@ -0,0 +1,89 @@
+section \<open>Fair Streams\<close>
+
+theory Fair_Stream imports "HOL-Library.Stream" begin
+
+definition upt_lists :: \<open>nat list stream\<close> where
+  \<open>upt_lists \<equiv> smap (upt 0) (stl nats)\<close>
+
+definition fair_nats :: \<open>nat stream\<close> where
+  \<open>fair_nats \<equiv> flat upt_lists\<close>
+
+definition fair :: \<open>'a stream \<Rightarrow> bool\<close> where
+  \<open>fair s \<equiv> \<forall>x \<in> sset s. \<forall>m. \<exists>n \<ge> m. s !! n = x\<close>
+
+lemma upt_lists_snth: \<open>x \<le> n \<Longrightarrow> x \<in> set (upt_lists !! n)\<close>
+  unfolding upt_lists_def by auto
+
+lemma all_ex_upt_lists: \<open>\<exists>n \<ge> m. x \<in> set (upt_lists !! n)\<close>
+  using upt_lists_snth by (meson dual_order.strict_trans1 gt_ex nle_le)
+
+lemma upt_lists_ne: \<open>\<forall>xs \<in> sset upt_lists. xs \<noteq> []\<close>
+  unfolding upt_lists_def by (simp add: sset_range)
+
+lemma sset_flat_stl: \<open>sset (flat (stl s)) \<subseteq> sset (flat s)\<close>
+proof (cases s)
+  case (SCons x xs)
+  then show ?thesis
+    by (cases x) (simp add: stl_sset subsetI, auto)
+qed
+
+lemma flat_snth_nth:
+  assumes \<open>x = s !! n ! m\<close> \<open>m < length (s !! n)\<close> \<open>\<forall>xs \<in> sset s. xs \<noteq> []\<close>
+  shows \<open>\<exists>n' \<ge> n. x = flat s !! n'\<close>
+  using assms
+proof (induct n arbitrary: s)
+  case 0
+  then show ?case
+    using flat_snth by fastforce
+next
+  case (Suc n)
+  have \<open>?case = (\<exists>n' \<ge> n. x = flat s !! Suc n')\<close>
+    by (metis Suc_le_D Suc_le_mono)
+  also have \<open>\<dots> = (\<exists>n' \<ge> n. x = stl (flat s) !! n')\<close>
+    by simp
+  finally have \<open>?case = (\<exists>n' \<ge> n. x = (tl (shd s) @- flat (stl s)) !! n')\<close>
+    using Suc.prems flat_unfold by (simp add: shd_sset)
+  then have ?case if \<open>\<exists>n' \<ge> n. x = flat (stl s) !! n'\<close>
+    using that by (metis (no_types, opaque_lifting) add.commute add_diff_cancel_left'
+        dual_order.trans le_add2 shift_snth_ge)
+  moreover {
+    have \<open>x = stl s !! n ! m\<close> \<open> m < length (stl s !! n)\<close>
+      using Suc.prems by simp_all
+    moreover have \<open>\<forall>xs \<in> sset (stl s). xs \<noteq> []\<close>
+      using Suc.prems by (cases s) simp_all
+    ultimately have \<open>\<exists>n' \<ge> n. x = flat (stl s) !! n'\<close>
+      using Suc.hyps by blast }
+  ultimately show ?case .
+qed
+
+lemma all_ex_fair_nats: \<open>\<exists>n \<ge> m. fair_nats !! n = x\<close>
+proof -
+  have \<open>\<exists>n \<ge> m. x \<in> set (upt_lists !! n)\<close>
+    using all_ex_upt_lists .
+  then have \<open>\<exists>n \<ge> m. \<exists>k < length (upt_lists !! n). upt_lists !! n ! k = x\<close>
+    by (simp add: in_set_conv_nth)
+  then obtain n k where \<open>m \<le> n\<close> \<open>k < length (upt_lists !! n)\<close> \<open>upt_lists !! n ! k = x\<close>
+    by blast
+  then obtain n' where \<open>n \<le> n'\<close> \<open>x = flat upt_lists !! n'\<close>
+    using flat_snth_nth upt_lists_ne by metis
+  moreover have \<open>m \<le> n'\<close>
+    using \<open>m \<le> n\<close> \<open>n \<le> n'\<close> by simp
+  ultimately show ?thesis
+    unfolding fair_nats_def by blast
+qed
+
+lemma fair_surj:
+  assumes \<open>surj f\<close>
+  shows \<open>fair (smap f fair_nats)\<close>
+  using assms unfolding fair_def by (metis UNIV_I all_ex_fair_nats imageE snth_smap)
+
+definition fair_stream :: \<open>(nat \<Rightarrow> 'a) \<Rightarrow> 'a stream\<close> where
+  \<open>fair_stream f = smap f fair_nats\<close>
+
+theorem fair_stream: \<open>surj f \<Longrightarrow> fair (fair_stream f)\<close>
+  unfolding fair_stream_def using fair_surj .
+
+theorem UNIV_stream: \<open>surj f \<Longrightarrow> sset (fair_stream f) = UNIV\<close>
+  unfolding fair_stream_def using all_ex_fair_nats by (metis sset_range stream.set_map surjI)
+
+end
diff --git a/thys/FOL_Seq_Calc3/List_Syntax.thy b/thys/FOL_Seq_Calc3/List_Syntax.thy
new file mode 100644
--- /dev/null
+++ b/thys/FOL_Seq_Calc3/List_Syntax.thy
@@ -0,0 +1,64 @@
+section \<open>List Syntax\<close>
+
+theory List_Syntax imports Main begin
+
+abbreviation list_member_syntax :: \<open>'a \<Rightarrow> 'a list \<Rightarrow> bool\<close> (\<open>_ [\<in>] _\<close> [51, 51] 50) where
+  \<open>x [\<in>] A \<equiv> x \<in> set A\<close>
+
+abbreviation list_not_member_syntax :: \<open>'a \<Rightarrow> 'a list \<Rightarrow> bool\<close> (\<open>_ [\<notin>] _\<close> [51, 51] 50) where
+  \<open>x [\<notin>] A \<equiv> x \<notin> set A\<close>
+
+abbreviation list_subset_syntax :: \<open>'a list \<Rightarrow> 'a list \<Rightarrow> bool\<close> (\<open>_ [\<subset>] _\<close> [51, 51] 50) where
+  \<open>A [\<subset>] B \<equiv> set A \<subset> set B\<close>
+
+abbreviation list_subset_eq_syntax :: \<open>'a list \<Rightarrow> 'a list \<Rightarrow> bool\<close> (\<open>_ [\<subseteq>] _\<close> [51, 51] 50) where
+  \<open>A [\<subseteq>] B \<equiv> set A \<subseteq> set B\<close>
+
+abbreviation removeAll_syntax :: \<open>'a list \<Rightarrow> 'a \<Rightarrow> 'a list\<close> (infix \<open>[\<div>]\<close> 75) where
+  \<open>A [\<div>] x \<equiv> removeAll x A\<close>
+
+syntax (ASCII)
+  "_BallList"       :: \<open>pttrn \<Rightarrow> 'a list \<Rightarrow> bool \<Rightarrow> bool\<close>  (\<open>(3ALL (_/[:]_)./ _)\<close> [0, 0, 10] 10)
+  "_BexList"        :: \<open>pttrn \<Rightarrow> 'a list \<Rightarrow> bool \<Rightarrow> bool\<close>  (\<open>(3EX (_/[:]_)./ _)\<close> [0, 0, 10] 10)
+  "_Bex1List"       :: \<open>pttrn \<Rightarrow> 'a list \<Rightarrow> bool \<Rightarrow> bool\<close>  (\<open>(3EX! (_/[:]_)./ _)\<close> [0, 0, 10] 10)
+  "_BleastList"     :: \<open>id \<Rightarrow> 'a list \<Rightarrow> bool \<Rightarrow> 'a\<close>       (\<open>(3LEAST (_/[:]_)./ _)\<close> [0, 0, 10] 10)
+
+syntax (input)
+  "_BallList"       :: \<open>pttrn \<Rightarrow> 'a list \<Rightarrow> bool \<Rightarrow> bool\<close>  (\<open>(3! (_/[:]_)./ _)\<close> [0, 0, 10] 10)
+  "_BexList"        :: \<open>pttrn \<Rightarrow> 'a list \<Rightarrow> bool \<Rightarrow> bool\<close>  (\<open>(3? (_/[:]_)./ _)\<close> [0, 0, 10] 10)
+  "_Bex1List"       :: \<open>pttrn \<Rightarrow> 'a list \<Rightarrow> bool \<Rightarrow> bool\<close>  (\<open>(3?! (_/[:]_)./ _)\<close> [0, 0, 10] 10)
+
+syntax
+  "_BallList"       :: \<open>pttrn \<Rightarrow> 'a list \<Rightarrow> bool \<Rightarrow> bool\<close>  (\<open>(3\<forall>(_/[\<in>]_)./ _)\<close> [0, 0, 10] 10)
+  "_BexList"        :: \<open>pttrn \<Rightarrow> 'a list \<Rightarrow> bool \<Rightarrow> bool\<close>  (\<open>(3\<exists>(_/[\<in>]_)./ _)\<close> [0, 0, 10] 10)
+  "_Bex1List"       :: \<open>pttrn \<Rightarrow> 'a list \<Rightarrow> bool \<Rightarrow> bool\<close>  (\<open>(3\<exists>!(_/[\<in>]_)./ _)\<close> [0, 0, 10] 10)
+  "_BleastList"     :: \<open>id \<Rightarrow> 'a list \<Rightarrow> bool \<Rightarrow> 'a\<close>       (\<open>(3LEAST(_/[\<in>]_)./ _)\<close> [0, 0, 10] 10)
+
+translations
+  "\<forall>x[\<in>]A. P" \<rightleftharpoons> "CONST Ball (CONST set A) (\<lambda>x. P)"
+  "\<exists>x[\<in>]A. P" \<rightleftharpoons> "CONST Bex (CONST set A) (\<lambda>x. P)"
+  "\<exists>!x[\<in>]A. P" \<rightharpoonup> "\<exists>!x. x [\<in>] A \<and> P"
+  "LEAST x[:]A. P" \<rightharpoonup> "LEAST x. x [\<in>] A \<and> P"
+
+syntax (ASCII output)
+  "_setlessAllList" :: \<open>[idt, 'a, bool] \<Rightarrow> bool\<close>  (\<open>(3ALL _[<]_./ _)\<close> [0, 0, 10] 10)
+  "_setlessExList"  :: \<open>[idt, 'a, bool] \<Rightarrow> bool\<close>  (\<open>(3EX _[<]_./ _)\<close> [0, 0, 10] 10)
+  "_setleAllList"   :: \<open>[idt, 'a, bool] \<Rightarrow> bool\<close>  (\<open>(3ALL _[<=]_./ _)\<close> [0, 0, 10] 10)
+  "_setleExList"    :: \<open>[idt, 'a, bool] \<Rightarrow> bool\<close>  (\<open>(3EX _[<=]_./ _)\<close> [0, 0, 10] 10)
+  "_setleEx1List"   :: \<open>[idt, 'a, bool] \<Rightarrow> bool\<close>  (\<open>(3EX! _[<=]_./ _)\<close> [0, 0, 10] 10)
+
+syntax
+  "_setlessAllList" :: \<open>[idt, 'a, bool] \<Rightarrow> bool\<close>   (\<open>(3\<forall>_[\<subset>]_./ _)\<close> [0, 0, 10] 10)
+  "_setlessExList"  :: \<open>[idt, 'a, bool] \<Rightarrow> bool\<close>   (\<open>(3\<exists>_[\<subset>]_./ _)\<close> [0, 0, 10] 10)
+  "_setleAllList"   :: \<open>[idt, 'a, bool] \<Rightarrow> bool\<close>   (\<open>(3\<forall>_[\<subseteq>]_./ _)\<close> [0, 0, 10] 10)
+  "_setleExList"    :: \<open>[idt, 'a, bool] \<Rightarrow> bool\<close>   (\<open>(3\<exists>_[\<subseteq>]_./ _)\<close> [0, 0, 10] 10)
+  "_setleEx1List"   :: \<open>[idt, 'a, bool] \<Rightarrow> bool\<close>   (\<open>(3\<exists>!_[\<subseteq>]_./ _)\<close> [0, 0, 10] 10)
+
+translations
+  "\<forall>A[\<subset>]B. P" \<rightharpoonup> "\<forall>A. A [\<subset>] B \<longrightarrow> P"
+  "\<exists>A[\<subset>]B. P" \<rightharpoonup> "\<exists>A. A [\<subset>] B \<and> P"
+  "\<forall>A[\<subseteq>]B. P" \<rightharpoonup> "\<forall>A. A [\<subseteq>] B \<longrightarrow> P"
+  "\<exists>A[\<subseteq>]B. P" \<rightharpoonup> "\<exists>A. A [\<subseteq>] B \<and> P"
+  "\<exists>!A[\<subseteq>]B. P" \<rightharpoonup> "\<exists>!A. A [\<subseteq>] B \<and> P"
+
+end
diff --git a/thys/FOL_Seq_Calc3/Main.hs b/thys/FOL_Seq_Calc3/Main.hs
new file mode 100644
--- /dev/null
+++ b/thys/FOL_Seq_Calc3/Main.hs
@@ -0,0 +1,61 @@
+import Prelude
+import Data.Char (chr, ord)
+import Data.List (intersperse)
+import System.Environment
+
+import Arith
+import Prover
+
+instance Show Arith.Nat where
+  show (Nat n) = show n
+
+charFrom :: Char -> Arith.Nat -> Char
+charFrom c n = chr (ord c + fromInteger (Arith.integer_of_nat n))
+
+instance Show Tm where
+  show (Var n) = show n
+  show (Fun f []) = charFrom 'a' f : ""
+  show (Fun f ts) = charFrom 'f' f : "(" ++ concat (intersperse ", " (map show ts)) ++ ")"
+
+instance Show Fm where
+  show Falsity = "Falsity"
+  show (Pre p []) = charFrom 'P' p : ""
+  show (Pre p ts) = charFrom 'P' p : "(" ++ concat (intersperse ", " (map show ts)) ++ ")"
+  show (Imp p q) = "(" ++ show p ++ ") --> (" ++ show q ++ ")"
+  show (Uni p) = "forall " ++ show p
+
+showRule :: Rule -> String
+showRule (Axiom n ts) = "Axiom on " ++ show (Pre n ts)
+showRule FlsL = "FlsL"
+showRule FlsR = "FlsR"
+showRule Idle = "Idle"
+showRule (ImpL p q) = "ImpL on " ++ show p ++ " and " ++ show q
+showRule (ImpR p q) = "ImpR on " ++ show p ++ " and " ++ show q
+showRule (UniL t p) = "UniL on " ++ show t ++ " and " ++ show p
+showRule (UniR p) = "UniR on " ++ show p
+
+showFms :: [Fm] -> String
+showFms ps = concat (intersperse ", " (map show ps))
+
+showTree :: Int -> Tree (([Fm], [Fm]), Rule) -> String
+showTree n (Node ((l, r), rule) (Abs_fset (Set ts))) =
+  let inc = if length ts > 1 then 2 else 0 in
+  replicate n ' ' ++ showFms l ++ " |- " ++ showFms r ++ "\n" ++
+  replicate n ' ' ++ " + " ++ showRule rule ++ "\n" ++
+  concat (map (showTree (n + inc)) ts)
+
+-- deriving instance Read Arith.Nat
+
+instance Read Arith.Nat where
+  readsPrec d s = map (\(n, s) -> (Arith.Nat n, s)) (readsPrec d s :: [(Integer, String)])
+
+deriving instance Read Tm
+deriving instance Read Fm
+
+main :: IO ()
+main = do
+  args <- getArgs
+  let p = read (head args) :: Fm
+  let res = prove p
+  putStrLn (showTree 0 res)
+
diff --git a/thys/FOL_Seq_Calc3/Prover.thy b/thys/FOL_Seq_Calc3/Prover.thy
new file mode 100644
--- /dev/null
+++ b/thys/FOL_Seq_Calc3/Prover.thy
@@ -0,0 +1,48 @@
+section \<open>Prover\<close>
+
+theory Prover imports "Abstract_Completeness.Abstract_Completeness" Encoding Fair_Stream begin
+
+function eff :: \<open>rule \<Rightarrow> sequent \<Rightarrow> (sequent fset) option\<close> where
+  \<open>eff Idle (A, B) =
+    Some {| (A, B) |}\<close>
+| \<open>eff (Axiom n ts) (A, B) = (if \<^bold>\<ddagger>n ts [\<in>] A \<and> \<^bold>\<ddagger>n ts [\<in>] B then
+    Some {||} else None)\<close>
+| \<open>eff FlsL (A, B) = (if \<^bold>\<bottom> [\<in>] A then
+    Some {||} else None)\<close>
+| \<open>eff FlsR (A, B) = (if \<^bold>\<bottom> [\<in>] B then
+    Some {| (A, B [\<div>] \<^bold>\<bottom>) |} else None)\<close>
+| \<open>eff (ImpL p q) (A, B) = (if (p \<^bold>\<longrightarrow> q) [\<in>] A then
+    Some {| (A [\<div>] (p \<^bold>\<longrightarrow> q), p # B), (q # A [\<div>] (p \<^bold>\<longrightarrow> q), B) |} else None)\<close>
+| \<open>eff (ImpR p q) (A, B) = (if (p \<^bold>\<longrightarrow> q) [\<in>] B then
+    Some {| (p # A, q # B [\<div>] (p \<^bold>\<longrightarrow> q)) |} else None)\<close>
+| \<open>eff (UniL t p) (A, B) = (if \<^bold>\<forall>p [\<in>] A then
+    Some {| (p\<langle>t/0\<rangle> # A, B) |} else None)\<close>
+| \<open>eff (UniR p) (A, B) = (if \<^bold>\<forall>p [\<in>] B then
+    Some {| (A, p\<langle>\<^bold>#(fresh (A @ B))/0\<rangle> # B [\<div>] \<^bold>\<forall>p) |} else None)\<close>
+  by pat_completeness auto
+termination by (relation \<open>measure size\<close>) standard
+
+definition rules :: \<open>rule stream\<close> where
+  \<open>rules \<equiv> fair_stream rule_of_nat\<close>
+
+lemma UNIV_rules: \<open>sset rules = UNIV\<close>
+  unfolding rules_def using UNIV_stream surj_rule_of_nat .
+
+interpretation RuleSystem \<open>\<lambda>r s ss. eff r s = Some ss\<close> rules UNIV
+  by unfold_locales (auto simp: UNIV_rules intro: exI[of _ Idle])
+
+lemma per_rules':
+  assumes \<open>enabled r (A, B)\<close> \<open>\<not> enabled r (A', B')\<close> \<open>eff r' (A, B) = Some ss'\<close> \<open>(A', B') |\<in>| ss'\<close>
+  shows \<open>r' = r\<close>
+  using assms by (cases r r' rule: rule.exhaust[case_product rule.exhaust])
+    (unfold enabled_def, auto split: if_splits)
+
+lemma per_rules: \<open>per r\<close>
+  unfolding per_def UNIV_rules using per_rules' by fast
+
+interpretation PersistentRuleSystem \<open>\<lambda>r s ss. eff r s = Some ss\<close> rules UNIV
+  using per_rules by unfold_locales
+
+definition \<open>prover \<equiv> mkTree rules\<close>
+
+end
diff --git a/thys/FOL_Seq_Calc3/ROOT b/thys/FOL_Seq_Calc3/ROOT
new file mode 100644
--- /dev/null
+++ b/thys/FOL_Seq_Calc3/ROOT
@@ -0,0 +1,23 @@
+chapter AFP
+
+session FOL_Seq_Calc3 (AFP) = "HOL-Library" +
+  options [timeout = 300]
+  sessions
+    Abstract_Soundness
+    Abstract_Completeness
+  theories
+    List_Syntax
+    Fair_Stream
+    Syntax
+    Semantics
+    Encoding
+    Prover
+    Export
+    Soundness
+    Completeness
+    Result
+  document_files
+    "root.tex"
+    "root.bib"
+  export_files (in "./program") [3] "*:**.hs" 
+
diff --git a/thys/FOL_Seq_Calc3/Result.thy b/thys/FOL_Seq_Calc3/Result.thy
new file mode 100644
--- /dev/null
+++ b/thys/FOL_Seq_Calc3/Result.thy
@@ -0,0 +1,17 @@
+section \<open>Result\<close>
+
+theory Result imports Soundness Completeness begin
+
+theorem prover_soundness_completeness:
+  fixes A B :: \<open>fm list\<close>
+  defines \<open>t \<equiv> prover (A, B)\<close>
+  shows \<open>tfinite t \<and> wf t \<longleftrightarrow> (\<forall>(E :: _ \<Rightarrow> tm) F G. sc (E, F, G) (A, B))\<close>
+  using assms prover_soundness prover_completeness unfolding prover_def by fastforce
+
+corollary
+  fixes p :: fm
+  defines \<open>t \<equiv> prover ([], [p])\<close>
+  shows \<open>tfinite t \<and> wf t \<longleftrightarrow> (\<forall>(E :: _ \<Rightarrow> tm) F G. \<lbrakk>E, F, G\<rbrakk> p)\<close>
+  using assms prover_soundness_completeness by simp
+
+end
diff --git a/thys/FOL_Seq_Calc3/Semantics.thy b/thys/FOL_Seq_Calc3/Semantics.thy
new file mode 100644
--- /dev/null
+++ b/thys/FOL_Seq_Calc3/Semantics.thy
@@ -0,0 +1,87 @@
+section \<open>Semantics\<close>
+
+theory Semantics imports Syntax begin
+
+subsection \<open>Shift\<close>
+
+definition shift :: \<open>(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a\<close>
+  (\<open>_\<langle>_:_\<rangle>\<close> [90, 0, 0] 91) where
+  \<open>E\<langle>n:x\<rangle> = (\<lambda>m. if m < n then E m else if m = n then x else E (m-1))\<close>
+
+lemma shift_eq [simp]: \<open>n = m \<Longrightarrow> (E\<langle>n:x\<rangle>) m = x\<close>
+  by (simp add: shift_def)
+
+lemma shift_gt [simp]: \<open>m < n \<Longrightarrow> (E\<langle>n:x\<rangle>) m = E m\<close>
+  by (simp add: shift_def)
+
+lemma shift_lt [simp]: \<open>n < m \<Longrightarrow> (E\<langle>n:x\<rangle>) m = E (m-1)\<close>
+  by (simp add: shift_def)
+
+lemma shift_commute [simp]: \<open>E\<langle>n:y\<rangle>\<langle>0:x\<rangle> = E\<langle>0:x\<rangle>\<langle>n+1:y\<rangle>\<close>
+proof
+  fix m
+  show \<open>(E\<langle>n:y\<rangle>\<langle>0:x\<rangle>) m = (E\<langle>0:x\<rangle>\<langle>n+1:y\<rangle>) m\<close>
+    unfolding shift_def by (cases m) simp_all
+qed
+
+subsection \<open>Definition\<close>
+
+type_synonym 'a var_denot = \<open>nat \<Rightarrow> 'a\<close>
+type_synonym 'a fun_denot = \<open>nat \<Rightarrow> 'a list \<Rightarrow> 'a\<close>
+type_synonym 'a pre_denot = \<open>nat \<Rightarrow> 'a list \<Rightarrow> bool\<close>
+
+primrec semantics_tm :: \<open>'a var_denot \<Rightarrow> 'a fun_denot \<Rightarrow> tm \<Rightarrow> 'a\<close> (\<open>\<lparr>_, _\<rparr>\<close>) where
+  \<open>\<lparr>E, F\<rparr> (\<^bold>#n) = E n\<close>
+| \<open>\<lparr>E, F\<rparr> (\<^bold>\<dagger>f ts) = F f (map \<lparr>E, F\<rparr> ts)\<close>
+
+primrec semantics_fm :: \<open>'a var_denot \<Rightarrow> 'a fun_denot \<Rightarrow> 'a pre_denot \<Rightarrow> fm \<Rightarrow> bool\<close>
+  (\<open>\<lbrakk>_, _, _\<rbrakk>\<close>) where
+  \<open>\<lbrakk>_, _, _\<rbrakk> \<^bold>\<bottom> = False\<close>
+| \<open>\<lbrakk>E, F, G\<rbrakk> (\<^bold>\<ddagger>P ts) = G P (map \<lparr>E, F\<rparr> ts)\<close>
+| \<open>\<lbrakk>E, F, G\<rbrakk> (p \<^bold>\<longrightarrow> q) = (\<lbrakk>E, F, G\<rbrakk> p \<longrightarrow> \<lbrakk>E, F, G\<rbrakk> q)\<close>
+| \<open>\<lbrakk>E, F, G\<rbrakk> (\<^bold>\<forall>p) = (\<forall>x. \<lbrakk>E\<langle>0:x\<rangle>, F, G\<rbrakk> p)\<close>
+
+fun sc :: \<open>('a var_denot \<times> 'a fun_denot \<times> 'a pre_denot) \<Rightarrow> sequent \<Rightarrow> bool\<close> where
+  \<open>sc (E, F, G) (A, B) = ((\<forall>p [\<in>] A. \<lbrakk>E, F, G\<rbrakk> p) \<longrightarrow> (\<exists>q [\<in>] B. \<lbrakk>E, F, G\<rbrakk> q))\<close>
+
+subsection \<open>Instantiation\<close>
+
+lemma lift_lemma [simp]: \<open>\<lparr>E\<langle>0:x\<rangle>, F\<rparr> (\<^bold>\<up>t) = \<lparr>E, F\<rparr> t\<close>
+  by (induct t) (auto cong: map_cong)
+
+lemma inst_tm_semantics [simp]: \<open>\<lparr>E, F\<rparr> (t\<llangle>s/m\<rrangle>) = \<lparr>E\<langle>m:\<lparr>E, F\<rparr> s\<rangle>, F\<rparr> t\<close>
+  by (induct t) (auto cong: map_cong)
+
+lemma inst_fm_semantics [simp]: \<open>\<lbrakk>E, F, G\<rbrakk> (p\<langle>t/m\<rangle>) = \<lbrakk>E\<langle>m:\<lparr>E, F\<rparr> t\<rangle>, F, G\<rbrakk> p\<close>
+  by (induct p arbitrary: E m t) (auto cong: map_cong)
+
+subsection \<open>Variables\<close>
+
+lemma upd_vars_tm [simp]: \<open>n [\<notin>] vars_tm t \<Longrightarrow> \<lparr>E(n := x), F\<rparr> t = \<lparr>E, F\<rparr> t\<close>
+  by (induct t) (auto cong: map_cong)
+
+lemma shift_upd_commute: \<open>m \<le> n \<Longrightarrow> (E(n := x)\<langle>m:y\<rangle>) = ((E\<langle>m:y\<rangle>)(Suc n := x))\<close>
+  unfolding shift_def by fastforce
+
+lemma upd_vars_fm [simp]: \<open>max_list (vars_fm p) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p = \<lbrakk>E, F, G\<rbrakk> p\<close>
+proof (induct p arbitrary: E n)
+  case (Pre P ts)
+  moreover have \<open>max_list (concat (map vars_tm ts)) < n\<close>
+    using Pre.prems max_list_concat by simp
+  then have \<open>n [\<notin>] concat (map vars_tm ts)\<close>
+    using max_list_in by blast
+  then have \<open>\<forall>t [\<in>] ts. n [\<notin>] vars_tm t\<close>
+    by simp
+  ultimately show ?case
+    using upd_vars_tm by (metis list.map_cong semantics_fm.simps(2))
+next
+  case (Uni p)
+  have \<open>?case = ((\<forall>y. \<lbrakk>E(n := x)\<langle>0:y\<rangle>, F, G\<rbrakk> p) = (\<forall>y. \<lbrakk>E\<langle>0:y\<rangle>, F, G\<rbrakk> p))\<close>
+    by (simp add: fun_upd_def)
+  also have \<open>\<dots> = ((\<forall>y. \<lbrakk>(E\<langle>0:y\<rangle>)(n + 1 := x), F, G\<rbrakk> p) = (\<forall>y. \<lbrakk>E\<langle>0:y\<rangle>, F, G\<rbrakk> p))\<close>
+    by (simp add: shift_upd_commute)
+  finally show ?case
+    using Uni by fastforce
+qed (auto simp: max_list_append cong: map_cong)
+
+end
diff --git a/thys/FOL_Seq_Calc3/Soundness.thy b/thys/FOL_Seq_Calc3/Soundness.thy
new file mode 100644
--- /dev/null
+++ b/thys/FOL_Seq_Calc3/Soundness.thy
@@ -0,0 +1,51 @@
+section \<open>Soundness\<close>
+
+theory Soundness imports "Abstract_Soundness.Finite_Proof_Soundness" Prover Semantics begin
+
+lemma eff_sound:
+  fixes E :: \<open>_ \<Rightarrow> 'a\<close>
+  assumes \<open>eff r (A, B) = Some ss\<close> \<open>\<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>(E :: _ \<Rightarrow> 'a). sc (E, F, G) (A, B))\<close>
+  shows \<open>sc (E, F, G) (A, B)\<close>
+  using assms
+proof (induct r \<open>(A, B)\<close> rule: eff.induct)
+  case (5 p q)
+  then have \<open>sc (E, F, G) (A [\<div>] (p \<^bold>\<longrightarrow> q), p # B)\<close> \<open>sc (E, F, G) (q # A [\<div>] (p \<^bold>\<longrightarrow> q), B)\<close>
+    by (metis eff.simps(5) finsertCI option.inject option.simps(3))+
+  then show ?case
+    using "5.prems"(1) by (force split: if_splits)
+next
+  case (7 t p)
+  then have \<open>sc (E, F, G) (p\<langle>t/0\<rangle> # A, B)\<close>
+    by (metis eff.simps(7) finsert_iff option.inject option.simps(3))
+  then show ?case
+    using "7.prems"(1) by (fastforce split: if_splits)
+next
+  case (8 p)
+  let ?n = \<open>fresh (A @ B)\<close>
+  have A: \<open>\<forall>p [\<in>] A. max_list (vars_fm p) < ?n\<close> and B: \<open>\<forall>p [\<in>] B. max_list (vars_fm p) < ?n\<close>
+    unfolding fresh_def using max_list_vars_fms max_list_mono vars_fms_member
+    by (metis Un_iff le_imp_less_Suc set_append)+
+  from 8 have \<open>sc (E(?n := x), F, G) (A, p\<langle>\<^bold>#?n/0\<rangle> # B [\<div>] \<^bold>\<forall> p)\<close> for x
+    by (metis eff.simps(8) finsert_iff option.inject option.simps(3))
+  then have \<open>(\<forall>p [\<in>] A. \<lbrakk>E, F, G\<rbrakk> p) \<longrightarrow>
+      (\<forall>x. \<lbrakk>(E\<langle>0:x\<rangle>)(Suc ?n := x), F, G\<rbrakk> p) \<or> (\<exists>q [\<in>] B [\<div>] \<^bold>\<forall> p. \<lbrakk>E, F, G\<rbrakk> q)\<close>
+    using A B upd_vars_fm by (auto simp: shift_upd_commute)
+  moreover have \<open>max_list (vars_fm p) < ?n\<close>
+    using B "8.prems"(1) by (metis eff.simps(8) option.distinct(1) vars_fm.simps(4))
+  ultimately have \<open>sc (E, F, G) (A, \<^bold>\<forall>p # (B [\<div>] \<^bold>\<forall> p))\<close>
+    by auto
+  moreover have \<open>\<^bold>\<forall>p [\<in>] B\<close>
+    using "8.prems"(1) by (simp split: if_splits)
+  ultimately show ?case
+    by (metis (full_types) Diff_iff sc.simps set_ConsD set_removeAll)
+qed (fastforce split: if_splits)+
+
+interpretation Soundness \<open>\<lambda>r s ss. eff r s = Some ss\<close> rules UNIV sc
+  unfolding Soundness_def using eff_sound by fast
+
+theorem prover_soundness:
+  assumes \<open>tfinite t\<close> and \<open>wf t\<close>
+  shows \<open>sc (E, F, G) (fst (root t))\<close>
+  using assms soundness by fast
+
+end
diff --git a/thys/FOL_Seq_Calc3/Syntax.thy b/thys/FOL_Seq_Calc3/Syntax.thy
new file mode 100644
--- /dev/null
+++ b/thys/FOL_Seq_Calc3/Syntax.thy
@@ -0,0 +1,93 @@
+section \<open>Syntax\<close>
+
+theory Syntax imports List_Syntax begin
+
+subsection \<open>Terms and Formulas\<close>
+
+datatype tm
+  = Var nat (\<open>\<^bold>#\<close>)
+  | Fun nat \<open>tm list\<close> (\<open>\<^bold>\<dagger>\<close>)
+
+datatype fm
+  = Falsity (\<open>\<^bold>\<bottom>\<close>)
+  | Pre nat \<open>tm list\<close> (\<open>\<^bold>\<ddagger>\<close>)
+  | Imp fm fm (infixr \<open>\<^bold>\<longrightarrow>\<close> 55)
+  | Uni fm (\<open>\<^bold>\<forall>\<close>)
+
+type_synonym sequent = \<open>fm list \<times> fm list\<close>
+
+subsubsection \<open>Instantiation\<close>
+
+primrec lift_tm :: \<open>tm \<Rightarrow> tm\<close> (\<open>\<^bold>\<up>\<close>) where
+  \<open>\<^bold>\<up>(\<^bold>#n) = \<^bold>#(n+1)\<close>
+| \<open>\<^bold>\<up>(\<^bold>\<dagger>f ts) = \<^bold>\<dagger>f (map \<^bold>\<up> ts)\<close>
+
+primrec inst_tm :: \<open>tm \<Rightarrow> tm \<Rightarrow> nat \<Rightarrow> tm\<close> (\<open>_'\<llangle>_'/_'\<rrangle>\<close> [90, 0, 0] 91) where
+  \<open>(\<^bold>#n)\<llangle>s/m\<rrangle> = (if n < m then \<^bold>#n else if n = m then s else \<^bold>#(n-1))\<close>
+| \<open>(\<^bold>\<dagger>f ts)\<llangle>s/m\<rrangle> = \<^bold>\<dagger>f (map (\<lambda>t. t\<llangle>s/m\<rrangle>) ts)\<close>
+
+primrec inst_fm :: \<open>fm \<Rightarrow> tm \<Rightarrow> nat \<Rightarrow> fm\<close> (\<open>_'\<langle>_'/_'\<rangle>\<close> [90, 0, 0] 91) where
+  \<open>\<^bold>\<bottom>\<langle>_/_\<rangle> = \<^bold>\<bottom>\<close>
+| \<open>(\<^bold>\<ddagger>P ts)\<langle>s/m\<rangle> = \<^bold>\<ddagger>P (map (\<lambda>t. t\<llangle>s/m\<rrangle>) ts)\<close>
+| \<open>(p \<^bold>\<longrightarrow> q)\<langle>s/m\<rangle> = (p\<langle>s/m\<rangle> \<^bold>\<longrightarrow> q\<langle>s/m\<rangle>)\<close>
+| \<open>(\<^bold>\<forall>p)\<langle>s/m\<rangle> = \<^bold>\<forall>(p\<langle>\<^bold>\<up>s/m+1\<rangle>)\<close>
+
+subsubsection \<open>Variables\<close>
+
+primrec vars_tm :: \<open>tm \<Rightarrow> nat list\<close> where
+  \<open>vars_tm (\<^bold>#n) = [n]\<close>
+| \<open>vars_tm (\<^bold>\<dagger>_ ts) = concat (map vars_tm ts)\<close>
+
+primrec vars_fm :: \<open>fm \<Rightarrow> nat list\<close> where
+  \<open>vars_fm \<^bold>\<bottom> = []\<close>
+| \<open>vars_fm (\<^bold>\<ddagger>_ ts) = concat (map vars_tm ts)\<close>
+| \<open>vars_fm (p \<^bold>\<longrightarrow> q) = vars_fm p @ vars_fm q\<close>
+| \<open>vars_fm (\<^bold>\<forall>p) = vars_fm p\<close>
+
+primrec max_list :: \<open>nat list \<Rightarrow> nat\<close> where
+  \<open>max_list [] = 0\<close>
+| \<open>max_list (x # xs) = max x (max_list xs)\<close>
+
+definition max_var_fm :: \<open>fm \<Rightarrow> nat\<close> where
+  \<open>max_var_fm p = max_list (vars_fm p)\<close>
+
+lemma max_list_append: \<open>max_list (xs @ ys) = max (max_list xs) (max_list ys)\<close>
+  by (induct xs) auto
+
+lemma max_list_concat: \<open>xs [\<in>] xss \<Longrightarrow> max_list xs \<le> max_list (concat xss)\<close>
+  by (induct xss) (auto simp: max_list_append)
+
+lemma max_list_in: \<open>max_list xs < n \<Longrightarrow> n [\<notin>] xs\<close>
+  by (induct xs) auto
+
+definition vars_fms :: \<open>fm list \<Rightarrow> nat list\<close> where
+  \<open>vars_fms A \<equiv> concat (map vars_fm A)\<close>
+
+lemma vars_fms_member: \<open>p [\<in>] A \<Longrightarrow> vars_fm p [\<subseteq>] vars_fms A\<close>
+  unfolding vars_fms_def by (induct A) auto
+
+lemma max_list_mono: \<open>A [\<subseteq>] B \<Longrightarrow> max_list A \<le> max_list B\<close>
+  by (induct A) (simp, metis linorder_not_le list.set_intros(1) max.absorb2 max.absorb3
+      max_list.simps(2) max_list_in set_subset_Cons subset_code(1))
+
+lemma max_list_vars_fms:
+  assumes \<open>max_list (vars_fms A) \<le> n\<close> \<open>p [\<in>] A\<close>
+  shows \<open>max_list (vars_fm p) \<le> n\<close>
+  using assms max_list_mono vars_fms_member by (meson dual_order.trans)
+
+definition fresh :: \<open>fm list \<Rightarrow> nat\<close> where
+  \<open>fresh A \<equiv> Suc (max_list (vars_fms A))\<close>
+
+subsection \<open>Rules\<close>
+
+datatype rule
+  = Idle
+  | Axiom nat \<open>tm list\<close>
+  | FlsL
+  | FlsR
+  | ImpL fm fm
+  | ImpR fm fm
+  | UniL tm fm
+  | UniR fm
+
+end
diff --git a/thys/FOL_Seq_Calc3/document/root.bib b/thys/FOL_Seq_Calc3/document/root.bib
new file mode 100644
--- /dev/null
+++ b/thys/FOL_Seq_Calc3/document/root.bib
@@ -0,0 +1,35 @@
+@article{Abstract-Completeness-AFP,
+  author  = {Jasmin Christian Blanchette and Andrei Popescu and Dmitriy Traytel},
+  title   = {Abstract Completeness},
+  journal = {Archive of Formal Proofs},
+  month   = apr,
+  year    = 2014,
+  note    = {\url{https://isa-afp.org/entries/Abstract_Completeness.html},
+            Formal proof development},
+  ISSN    = {2150-914x},
+}
+
+@article{FOL-Seq-Calc2-AFP,
+  author  = {Asta Halkjær From and Frederik Krogsdal Jacobsen},
+  title   = {A Sequent Calculus Prover for First-Order Logic with Functions},
+  journal = {Archive of Formal Proofs},
+  month   = jan,
+  year    = 2022,
+  note    = {\url{https://isa-afp.org/entries/FOL_Seq_Calc2.html},
+            Formal proof development},
+  ISSN    = {2150-914x},
+}
+
+@article{BlanchettePT17,
+  author    = {Jasmin Christian Blanchette and
+               Andrei Popescu and
+               Dmitriy Traytel},
+  title     = {Soundness and Completeness Proofs by Coinductive Methods},
+  journal   = {Journal of Automated Reasoning},
+  volume    = {58},
+  number    = {1},
+  pages     = {149--179},
+  year      = {2017},
+  doi       = {10.1007/s10817-016-9391-3}
+}
+
diff --git a/thys/FOL_Seq_Calc3/document/root.tex b/thys/FOL_Seq_Calc3/document/root.tex
new file mode 100644
--- /dev/null
+++ b/thys/FOL_Seq_Calc3/document/root.tex
@@ -0,0 +1,60 @@
+\documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
+\usepackage{isabelle,isabellesym}
+
+% this should be the last package used
+\usepackage{pdfsetup}
+
+% urls in roman style, theory text in math-similar italics
+\urlstyle{rm}
+\isabellestyle{it}
+
+% for uniform font size
+% \renewcommand{\isastyle}{\isastyleminor}
+
+\begin{document}
+
+\title{A Naive Prover for First-Order Logic}
+\author{Asta Halkjær From}
+\maketitle
+
+\begin{abstract}
+	The AFP entry Abstract Completeness by Blanchette, Popescu and Traytel~\cite{Abstract-Completeness-AFP} formalizes the core of Beth/Hintikka-style completeness proofs for first-order logic and can be used to formalize executable sequent calculus provers.
+	In the Journal of Automated Reasoning~\cite{BlanchettePT17}, the authors instantiate the framework with a sequent calculus for first-order logic and prove its completeness.
+	Their use of an infinite set of proof rules indexed by formulas yields very direct arguments.
+	A fair stream of these rules controls the prover, making its definition remarkably simple.
+	The AFP entry, however, only contains a toy example for propositional logic.
+	The AFP entry A Sequent Calculus Prover for First-Order Logic with Functions by From and Jacobsen~\cite{FOL-Seq-Calc2-AFP} also uses the framework, but uses a finite set of generic rules resulting in a more sophisticated prover with more complicated proofs.
+
+	This entry contains an executable sequent calculus prover for first-order logic with functions in the style presented by Blanchette et al.
+	The prover can be exported to Haskell and this entry includes formalized proofs of its soundness and completeness.
+	The proofs are simpler than those for the prover by From and Jacobsen~\cite{FOL-Seq-Calc2-AFP} but the performance of the prover is significantly worse.
+
+	The included theory \isa{Fair-Stream} first proves that the sequence of natural numbers 0, 0, 1, 0, 1, 2, etc.\ is fair.
+	It then proves that mapping any surjective function across the sequence preserves fairness.
+	This method of obtaining a fair stream of rules is similar to the one given by Blanchette et al.~\cite{BlanchettePT17}.
+	The concrete functions from natural numbers to terms, formulas and rules are defined using the \isa{Nat-Bijection} theory in the HOL-Library.
+\end{abstract}
+
+\newpage
+
+\tableofcontents
+
+\newpage
+
+% sane default for proof documents
+\parindent 0pt\parskip 0.5ex
+
+% generated text of all theories
+\input{session}
+
+% optional bibliography
+\bibliographystyle{abbrv}
+\bibliography{root}
+
+\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End:
diff --git a/thys/ROOTS b/thys/ROOTS
--- a/thys/ROOTS
+++ b/thys/ROOTS
@@ -1,672 +1,673 @@
 ADS_Functor
 AI_Planning_Languages_Semantics
 AODV
 AVL-Trees
 AWN
 Abortable_Linearizable_Modules
 Abs_Int_ITP2012
 Abstract-Hoare-Logics
 Abstract-Rewriting
 Abstract_Completeness
 Abstract_Soundness
 Ackermanns_not_PR
 Actuarial_Mathematics
 Adaptive_State_Counting
 Affine_Arithmetic
 Aggregation_Algebras
 Akra_Bazzi
 Algebraic_Numbers
 Algebraic_VCs
 Allen_Calculus
 Amicable_Numbers
 Amortized_Complexity
 AnselmGod
 Applicative_Lifting
 Approximation_Algorithms
 Architectural_Design_Patterns
 Aristotles_Assertoric_Syllogistic
 Arith_Prog_Rel_Primes
 ArrowImpossibilityGS
 Attack_Trees
 Auto2_HOL
 Auto2_Imperative_HOL
 AutoFocus-Stream
 Automated_Stateful_Protocol_Verification
 Automatic_Refinement
 AxiomaticCategoryTheory
 BDD
 BD_Security_Compositional
 BNF_CC
 BNF_Operations
 BTree
 Banach_Steinhaus
 Belief_Revision
 Bell_Numbers_Spivey
 BenOr_Kozen_Reif
 Berlekamp_Zassenhaus
 Bernoulli
 Bertrands_Postulate
 Bicategory
 BinarySearchTree
 Binding_Syntax_Theory
 Binomial-Heaps
 Binomial-Queues
 BirdKMP
 Blue_Eyes
 Bondy
 Boolean_Expression_Checkers
 Bounded_Deducibility_Security
 Buchi_Complementation
 Budan_Fourier
 Buffons_Needle
 Buildings
 BytecodeLogicJmlTypes
 C2KA_DistributedSystems
 CAVA_Automata
 CAVA_LTL_Modelchecker
 CCS
 CISC-Kernel
 CRDT
 CSP_RefTK
 CYK
 CZH_Elementary_Categories
 CZH_Foundations
 CZH_Universal_Constructions
 CakeML
 CakeML_Codegen
 Call_Arity
 Card_Equiv_Relations
 Card_Multisets
 Card_Number_Partitions
 Card_Partitions
 Cartan_FP
 Case_Labeling
 Catalan_Numbers
 Category
 Category2
 Category3
 Cauchy
 Cayley_Hamilton
 Certification_Monads
 Chandy_Lamport
 Chord_Segments
 Circus
 Clean
 ClockSynchInst
 Closest_Pair_Points
 CoCon
 CoSMeDis
 CoSMed
 CofGroups
 Coinductive
 Coinductive_Languages
 Collections
 Combinatorics_Words
 Combinatorics_Words_Graph_Lemma
 Combinatorics_Words_Lyndon
 Comparison_Sort_Lower_Bound
 Compiling-Exceptions-Correctly
 Complete_Non_Orders
 Completeness
 Complex_Bounded_Operators
 Complex_Geometry
 Complx
 ComponentDependencies
 ConcurrentGC
 ConcurrentIMP
 Concurrent_Ref_Alg
 Concurrent_Revisions
 Conditional_Simplification
 Conditional_Transfer_Rule
 Consensus_Refined
 Constructive_Cryptography
 Constructive_Cryptography_CM
 Constructor_Funs
 Containers
 CoreC++
 Core_DOM
 Core_SC_DOM
 Correctness_Algebras
 Cotangent_PFD_Formula
 Count_Complex_Roots
 CryptHOL
 CryptoBasedCompositionalProperties
 Cubic_Quartic_Equations
 DFS_Framework
 DOM_Components
 DPT-SAT-Solver
 DataRefinementIBP
 Datatype_Order_Generator
 Decl_Sem_Fun_PL
 Decreasing-Diagrams
 Decreasing-Diagrams-II
 Dedekind_Real
 Deep_Learning
 Delta_System_Lemma
 Density_Compiler
 Dependent_SIFUM_Refinement
 Dependent_SIFUM_Type_Systems
 Depth-First-Search
 Derangements
 Deriving
 Descartes_Sign_Rule
 Design_Theory
 Dict_Construction
 Differential_Dynamic_Logic
 Differential_Game_Logic
 Dijkstra_Shortest_Path
 Diophantine_Eqns_Lin_Hom
 Dirichlet_L
 Dirichlet_Series
 DiscretePricing
 Discrete_Summation
 DiskPaxos
 Dominance_CHK
 DynamicArchitectures
 Dynamic_Tables
 E_Transcendental
 Echelon_Form
 EdmondsKarp_Maxflow
 Efficient-Mergesort
 Elliptic_Curves_Group_Law
 Encodability_Process_Calculi
 Epistemic_Logic
 Equivalence_Relation_Enumeration
 Ergodic_Theory
 Error_Function
 Euler_MacLaurin
 Euler_Partition
 Eval_FO
 Example-Submission
 Extended_Finite_State_Machine_Inference
 Extended_Finite_State_Machines
 FFT
 FLP
 FOL-Fitting
 FOL_Axiomatic
 FOL_Harrison
 FOL_Seq_Calc1
 FOL_Seq_Calc2
+FOL_Seq_Calc3
 Factor_Algebraic_Polynomial
 Factored_Transition_System_Bounding
 Falling_Factorial_Sum
 Farkas
 FeatherweightJava
 Featherweight_OCL
 Fermat3_4
 FileRefinement
 FinFun
 Finger-Trees
 Finite-Map-Extras
 Finite_Automata_HF
 Finitely_Generated_Abelian_Groups
 First_Order_Terms
 First_Welfare_Theorem
 Fishburn_Impossibility
 Fisher_Yates
 Flow_Networks
 Floyd_Warshall
 Flyspeck-Tame
 FocusStreamsCaseStudies
 Forcing
 Formal_Puiseux_Series
 Formal_SSA
 Formula_Derivatives
 Foundation_of_geometry
 Fourier
 FO_Theory_Rewriting
 Free-Boolean-Algebra
 Free-Groups
 Fresh_Identifiers
 FunWithFunctions
 FunWithTilings
 Functional-Automata
 Functional_Ordered_Resolution_Prover
 Furstenberg_Topology
 GPU_Kernel_PL
 Gabow_SCC
 GaleStewart_Games
 Gale_Shapley
 Game_Based_Crypto
 Gauss-Jordan-Elim-Fun
 Gauss_Jordan
 Gauss_Sums
 Gaussian_Integers
 GenClock
 General-Triangle
 Generalized_Counting_Sort
 Generic_Deriving
 Generic_Join
 GewirthPGCProof
 Girth_Chromatic
 GoedelGod
 Goedel_HFSet_Semantic
 Goedel_HFSet_Semanticless
 Goedel_Incompleteness
 Goodstein_Lambda
 GraphMarkingIBP
 Graph_Saturation
 Graph_Theory
 Green
 Groebner_Bases
 Groebner_Macaulay
 Gromov_Hyperbolicity
 Grothendieck_Schemes
 Group-Ring-Module
 HOL-CSP
 HOLCF-Prelude
 HRB-Slicing
 Hahn_Jordan_Decomposition
 Heard_Of
 Hello_World
 HereditarilyFinite
 Hermite
 Hermite_Lindemann
 Hidden_Markov_Models
 Higher_Order_Terms
 Hoare_Time
 Hood_Melville_Queue
 HotelKeyCards
 Huffman
 Hybrid_Logic
 Hybrid_Multi_Lane_Spatial_Logic
 Hybrid_Systems_VCs
 HyperCTL
 Hyperdual
 IEEE_Floating_Point
 IFC_Tracking
 IMAP-CRDT
 IMO2019
 IMP2
 IMP2_Binary_Heap
 IMP_Compiler
 IP_Addresses
 Imperative_Insertion_Sort
 Impossible_Geometry
 Incompleteness
 Incredible_Proof_Machine
 Independence_CH
 Inductive_Confidentiality
 Inductive_Inference
 InfPathElimination
 InformationFlowSlicing
 InformationFlowSlicing_Inter
 Integration
 Interpolation_Polynomials_HOL_Algebra
 Interpreter_Optimizations
 Interval_Arithmetic_Word32
 Intro_Dest_Elim
 Iptables_Semantics
 Irrational_Series_Erdos_Straus
 Irrationality_J_Hancl
 Irrationals_From_THEBOOK
 IsaGeoCoq
 Isabelle_C
 Isabelle_Marries_Dirac
 Isabelle_Meta_Model
 Jacobson_Basic_Algebra
 Jinja
 JinjaDCI
 JinjaThreads
 JiveDataStoreModel
 Jordan_Hoelder
 Jordan_Normal_Form
 KAD
 KAT_and_DRA
 KBPs
 KD_Tree
 Key_Agreement_Strong_Adversaries
 Kleene_Algebra
 Knights_Tour
 Knot_Theory
 Knuth_Bendix_Order
 Knuth_Morris_Pratt
 Koenigsberg_Friendship
 Kruskal
 Kuratowski_Closure_Complement
 LLL_Basis_Reduction
 LLL_Factorization
 LOFT
 LTL
 LTL_Master_Theorem
 LTL_Normal_Form
 LTL_to_DRA
 LTL_to_GBA
 Lam-ml-Normalization
 LambdaAuth
 LambdaMu
 Lambda_Free_EPO
 Lambda_Free_KBOs
 Lambda_Free_RPOs
 Lambert_W
 Landau_Symbols
 Laplace_Transform
 Latin_Square
 LatticeProperties
 Launchbury
 Laws_of_Large_Numbers
 Lazy-Lists-II
 Lazy_Case
 Lehmer
 Lifting_Definition_Option
 Lifting_the_Exponent
 LightweightJava
 LinearQuantifierElim
 Linear_Inequalities
 Linear_Programming
 Linear_Recurrences
 Liouville_Numbers
 List-Index
 List-Infinite
 List_Interleaving
 List_Inversions
 List_Update
 LocalLexing
 Localization_Ring
 Locally-Nameless-Sigma
 Logging_Independent_Anonymity
 Lowe_Ontological_Argument
 Lower_Semicontinuous
 Lp
 LP_Duality
 Lucas_Theorem
 MDP-Algorithms
 MDP-Rewards
 MFMC_Countable
 MFODL_Monitor_Optimized
 MFOTL_Monitor
 MSO_Regex_Equivalence
 Markov_Models
 Marriage
 Mason_Stothers
 Matrices_for_ODEs
 Matrix
 Matrix_Tensor
 Matroids
 Max-Card-Matching
 Median_Method
 Median_Of_Medians_Selection
 Menger
 Mereology
 Mersenne_Primes
 Metalogic_ProofChecker
 MiniML
 MiniSail
 Minimal_SSA
 Minkowskis_Theorem
 Minsky_Machines
 Modal_Logics_for_NTS
 Modular_Assembly_Kit_Security
 Modular_arithmetic_LLL_and_HNF_algorithms
 Monad_Memo_DP
 Monad_Normalisation
 MonoBoolTranAlgebra
 MonoidalCategory
 Monomorphic_Monad
 MuchAdoAboutTwo
 Multi_Party_Computation
 Multirelations
 Myhill-Nerode
 Name_Carrying_Type_Inference
 Nash_Williams
 Nat-Interval-Logic
 Native_Word
 Nested_Multisets_Ordinals
 Network_Security_Policy_Verification
 Neumann_Morgenstern_Utility
 No_FTL_observers
 Nominal2
 Noninterference_CSP
 Noninterference_Concurrent_Composition
 Noninterference_Generic_Unwinding
 Noninterference_Inductive_Unwinding
 Noninterference_Ipurge_Unwinding
 Noninterference_Sequential_Composition
 NormByEval
 Nullstellensatz
 Octonions
 OpSets
 Open_Induction
 Optics
 Optimal_BST
 Orbit_Stabiliser
 Order_Lattice_Props
 Ordered_Resolution_Prover
 Ordinal
 Ordinal_Partitions
 Ordinals_and_Cardinals
 Ordinary_Differential_Equations
 PAC_Checker
 PAL
 PCF
 PLM
 POPLmark-deBruijn
 PSemigroupsConvolution
 Padic_Ints
 Pairing_Heap
 Paraconsistency
 Parity_Game
 Partial_Function_MR
 Partial_Order_Reduction
 Password_Authentication_Protocol
 Pell
 Perfect-Number-Thm
 Perron_Frobenius
 Physical_Quantities
 Pi_Calculus
 Pi_Transcendental
 Planarity_Certificates
 Poincare_Bendixson
 Poincare_Disc
 Polynomial_Factorization
 Polynomial_Interpolation
 Polynomials
 Pop_Refinement
 Posix-Lexing
 Possibilistic_Noninterference
 Power_Sum_Polynomials
 Pratt_Certificate
 Presburger-Automata
 Prim_Dijkstra_Simple
 Prime_Distribution_Elementary
 Prime_Harmonic_Series
 Prime_Number_Theorem
 Priority_Queue_Braun
 Priority_Search_Trees
 Probabilistic_Noninterference
 Probabilistic_Prime_Tests
 Probabilistic_System_Zoo
 Probabilistic_Timed_Automata
 Probabilistic_While
 Program-Conflict-Analysis
 Progress_Tracking
 Projective_Geometry
 Projective_Measurements
 Promela
 Proof_Strategy_Language
 PropResPI
 Propositional_Proof_Systems
 Prpu_Maxflow
 PseudoHoops
 Psi_Calculi
 Ptolemys_Theorem
 Public_Announcement_Logic
 QHLProver
 QR_Decomposition
 Quantales
 Quasi_Borel_Spaces
 Quaternions
 Quick_Sort_Cost
 RIPEMD-160-SPARK
 ROBDD
 RSAPSS
 Ramsey-Infinite
 Random_BSTs
 Random_Graph_Subgraph_Threshold
 Randomised_BSTs
 Randomised_Social_Choice
 Rank_Nullity_Theorem
 Real_Impl
 Real_Power
 Recursion-Addition
 Recursion-Theory-I
 Refine_Imperative_HOL
 Refine_Monadic
 RefinementReactive
 Regex_Equivalence
 Registers
 Regression_Test_Selection
 Regular-Sets
 Regular_Algebras
 Regular_Tree_Relations
 Relation_Algebra
 Relational-Incorrectness-Logic
 Relational_Disjoint_Set_Forests
 Relational_Forests
 Relational_Method
 Relational_Minimum_Spanning_Trees
 Relational_Paths
 Rep_Fin_Groups
 ResiduatedTransitionSystem
 Residuated_Lattices
 Resolution_FOL
 Rewriting_Z
 Ribbon_Proofs
 Robbins-Conjecture
 Robinson_Arithmetic
 Root_Balanced_Tree
 Roth_Arithmetic_Progressions
 Routing
 Roy_Floyd_Warshall
 SATSolverVerification
 SC_DOM_Components
 SDS_Impossibility
 SIFPL
 SIFUM_Type_Systems
 SPARCv8
 Safe_Distance
 Safe_OCL
 Saturation_Framework
 Saturation_Framework_Extensions
 Schutz_Spacetime
 Secondary_Sylow
 Security_Protocol_Refinement
 Selection_Heap_Sort
 SenSocialChoice
 Separata
 Separation_Algebra
 Separation_Logic_Imperative_HOL
 SequentInvertibility
 Shadow_DOM
 Shadow_SC_DOM
 Shivers-CFA
 ShortestPath
 Show
 Sigma_Commit_Crypto
 Signature_Groebner
 Simpl
 Simple_Firewall
 Simplex
 Simplicial_complexes_and_boolean_functions
 SimplifiedOntologicalArgument
 Skew_Heap
 Skip_Lists
 Slicing
 Sliding_Window_Algorithm
 Smith_Normal_Form
 Smooth_Manifolds
 Sort_Encodings
 Source_Coding_Theorem
 SpecCheck
 Special_Function_Bounds
 Splay_Tree
 Sqrt_Babylonian
 Stable_Matching
 Statecharts
 Stateful_Protocol_Composition_and_Typing
 Stellar_Quorums
 Stern_Brocot
 Stewart_Apollonius
 Stirling_Formula
 Stochastic_Matrices
 Stone_Algebras
 Stone_Kleene_Relation_Algebras
 Stone_Relation_Algebras
 Store_Buffer_Reduction
 Stream-Fusion
 Stream_Fusion_Code
 Strong_Security
 Sturm_Sequences
 Sturm_Tarski
 Stuttering_Equivalence
 Subresultants
 Subset_Boolean_Algebras
 SumSquares
 Sunflowers
 SuperCalc
 Surprise_Paradox
 Symmetric_Polynomials
 Syntax_Independent_Logic
 Szemeredi_Regularity
 Szpilrajn
 TESL_Language
 TLA
 Tail_Recursive_Functions
 Tarskis_Geometry
 Taylor_Models
 Three_Circles
 Timed_Automata
 Topological_Semantics
 Topology
 TortoiseHare
 Transcendence_Series_Hancl_Rucki
 Transformer_Semantics
 Transition_Systems_and_Automata
 Transitive-Closure
 Transitive-Closure-II
 Transitive_Models
 Treaps
 Tree-Automata
 Tree_Decomposition
 Triangle
 Trie
 Twelvefold_Way
 Tycon
 Types_Tableaus_and_Goedels_God
 Types_To_Sets_Extension
 UPF
 UPF_Firewall
 UTP
 Universal_Hash_Families
 Universal_Turing_Machine
 UpDown_Scheme
 Valuation
 Van_Emde_Boas_Trees
 Van_der_Waerden
 VectorSpace
 VeriComp
 Verified-Prover
 Verified_SAT_Based_AI_Planning
 VerifyThis2018
 VerifyThis2019
 Vickrey_Clarke_Groves
 Virtual_Substitution
 VolpanoSmith
 VYDRA_MDL
 WHATandWHERE_Security
 WOOT_Strong_Eventual_Consistency
 WebAssembly
 Weight_Balanced_Trees
 Weighted_Path_Order
 Well_Quasi_Orders
 Wetzels_Problem
 Winding_Number_Eval
 Word_Lib
 WorkerWrapper
 X86_Semantics
 XML
 Youngs_Inequality
 ZFC_in_HOL
 Zeta_3_Irrational
 Zeta_Function
 pGCL