diff --git a/thys/FOL_Seq_Calc3/Completeness.thy b/thys/FOL_Seq_Calc3/Completeness.thy
--- a/thys/FOL_Seq_Calc3/Completeness.thy
+++ b/thys/FOL_Seq_Calc3/Completeness.thy
@@ -1,281 +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
+    Basic: \<open>\<^bold>\<ddagger>P ts \<in> A \<Longrightarrow> \<^bold>\<ddagger>P 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>
+    UniA: \<open>\<^bold>\<forall>p \<in> A \<Longrightarrow> \<forall>t. \<langle>t\<rangle>p \<in> A\<close> and
+    UniB: \<open>\<^bold>\<forall>p \<in> B \<Longrightarrow> \<exists>t. \<langle>t\<rangle>p \<in> B\<close>
 
-abbreviation \<open>M A \<equiv> \<lbrakk>\<^bold>#, \<^bold>\<dagger>, \<lambda>n ts. \<^bold>\<ddagger>n ts \<in> A\<rbrakk>\<close>
+abbreviation \<open>M A \<equiv> \<lbrakk>\<^bold>#, \<^bold>\<dagger>, \<lambda>P ts. \<^bold>\<ddagger>P 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
+lemma size_sub_fm [simp]: \<open>size (sub_fm s p) = size p\<close>
+  by (induct p arbitrary: s) 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>
+    case (Pre P ts)
+    show \<open>\<^bold>\<ddagger>P ts \<in> A \<Longrightarrow> M A (\<^bold>\<ddagger>P ts)\<close> \<open>\<^bold>\<ddagger>P ts \<in> B \<Longrightarrow> \<not> M A (\<^bold>\<ddagger>P 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)+
+    have \<open>\<langle>t\<rangle>p \<in> A \<Longrightarrow> M A (\<langle>t\<rangle>p)\<close> \<open>\<langle>t\<rangle>p \<in> B \<Longrightarrow> \<not> M A (\<langle>t\<rangle>p)\<close> for t
+      using Uni 2 by (metis fm.size(8) in_measure lessI less_add_same_cancel1 size_sub_fm)+
     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>
+  shows \<open>(\<^bold>\<ddagger>P ts [\<in>] A \<Longrightarrow> \<^bold>\<ddagger>P ts [\<in>] A')\<close> \<open>\<^bold>\<ddagger>P ts [\<in>] B \<Longrightarrow> \<^bold>\<ddagger>P 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>
+    \<open>\<^bold>\<ddagger>P ts [\<in>] lhs (shd steps) \<Longrightarrow> \<^bold>\<ddagger>P ts [\<in>] lhsd (sdrop m steps)\<close>
+    \<open>\<^bold>\<ddagger>P ts [\<in>] rhs (shd steps) \<Longrightarrow> \<^bold>\<ddagger>P 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>
+  fix P ts
+  assume \<open>\<^bold>\<ddagger>P ts \<in> treeA steps\<close>
+  then obtain m where m: \<open>\<^bold>\<ddagger>P 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>
+  assume \<open>\<^bold>\<ddagger>P ts \<in> treeB steps\<close>
+  then obtain k where k: \<open>\<^bold>\<ddagger>P 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>
+  have \<open>\<^bold>\<ddagger>P 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>
+  moreover have \<open>\<^bold>\<ddagger>P 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>
+  ultimately have \<open>enabled (Axiom P 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>
+  then obtain j' where \<open>takenAtStep (Axiom P 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>
+  show \<open>\<forall>t. \<langle>t\<rangle>p \<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>
+    then have \<open>fst (shd (stl ?s)) |\<in>| {| (\<langle>t\<rangle>p # 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>
+    then have \<open>\<langle>t\<rangle>p [\<in>] lhs (shd (stl ?s))\<close>
       by auto
-    then have \<open>p\<langle>t/0\<rangle> \<in> treeA (stl ?s)\<close>
+    then have \<open>\<langle>t\<rangle>p \<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>
+    then show \<open>\<langle>t\<rangle>p \<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>
+        {| (lhsd ?s, \<langle>\<^bold>#(fresh (lhsd ?s @ rhsd ?s))\<rangle>p # 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>
+  then have \<open>\<exists>t. \<langle>t\<rangle>p [\<in>] rhs (shd (stl ?s))\<close>
     by auto
-  then have \<open>\<exists>t. p\<langle>t/0\<rangle> \<in> treeB (stl ?s)\<close>
+  then have \<open>\<exists>t. \<langle>t\<rangle>p \<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>
+  then show \<open>\<exists>t. \<langle>t\<rangle>p \<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/Fair_Stream.thy b/thys/FOL_Seq_Calc3/Fair_Stream.thy
--- a/thys/FOL_Seq_Calc3/Fair_Stream.thy
+++ b/thys/FOL_Seq_Calc3/Fair_Stream.thy
@@ -1,89 +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>
+  \<open>fair_stream f \<equiv> 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/Main.hs b/thys/FOL_Seq_Calc3/Main.hs
--- a/thys/FOL_Seq_Calc3/Main.hs
+++ b/thys/FOL_Seq_Calc3/Main.hs
@@ -1,61 +1,59 @@
 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
--- a/thys/FOL_Seq_Calc3/Prover.thy
+++ b/thys/FOL_Seq_Calc3/Prover.thy
@@ -1,48 +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
+| \<open>eff (Axiom P ts) (A, B) = (if \<^bold>\<ddagger>P ts [\<in>] A \<and> \<^bold>\<ddagger>P 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>
+    Some {| (\<langle>t\<rangle>p # 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>
+    Some {| (A, \<langle>\<^bold>#(fresh (A @ B))\<rangle>p # 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/Semantics.thy b/thys/FOL_Seq_Calc3/Semantics.thy
--- a/thys/FOL_Seq_Calc3/Semantics.thy
+++ b/thys/FOL_Seq_Calc3/Semantics.thy
@@ -1,87 +1,66 @@
 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>
+| \<open>\<lbrakk>E, F, G\<rbrakk> (\<^bold>\<forall>p) = (\<forall>x. \<lbrakk>x \<Zsemi> E, 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>
+subsection \<open>Substitution\<close>
 
-lemma lift_lemma [simp]: \<open>\<lparr>E\<langle>0:x\<rangle>, F\<rparr> (\<^bold>\<up>t) = \<lparr>E, F\<rparr> t\<close>
+lemma add_env_semantics [simp]: \<open>\<lparr>E, F\<rparr> ((t \<Zsemi> s) n) = (\<lparr>E, F\<rparr> t \<Zsemi> \<lambda>m. \<lparr>E, F\<rparr> (s m)) n\<close>
+  by (induct n) simp_all
+
+lemma lift_lemma [simp]: \<open>\<lparr>x \<Zsemi> E, F\<rparr> (lift_tm 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>
+lemma sub_tm_semantics [simp]: \<open>\<lparr>E, F\<rparr> (sub_tm s t) = \<lparr>\<lambda>n. \<lparr>E, F\<rparr> (s n), 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)
+lemma sub_fm_semantics [simp]: \<open>\<lbrakk>E, F, G\<rbrakk> (sub_fm s p) = \<lbrakk>\<lambda>n. \<lparr>E, F\<rparr> (s n), F, G\<rbrakk> p\<close>
+  by (induct p arbitrary: E s) (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 add_upd_commute [simp]: \<open>(y \<Zsemi> E(n := x)) m = ((y \<Zsemi> E)(Suc n := x)) m\<close>
+  by (induct m) simp_all
 
 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>
+  have \<open>?case = ((\<forall>y. \<lbrakk>\<lambda>m. (y \<Zsemi> E(n := x)) m, F, G\<rbrakk> p) = (\<forall>y. \<lbrakk>y \<Zsemi> E, 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
+  then show ?case
+    using Uni by simp
 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
--- a/thys/FOL_Seq_Calc3/Soundness.thy
+++ b/thys/FOL_Seq_Calc3/Soundness.thy
@@ -1,51 +1,53 @@
 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>
+  then have \<open>sc (E, F, G) (\<langle>t\<rangle>p # 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
+  from 8 have \<open>sc (E(?n := x), F, G) (A, \<langle>\<^bold>#?n\<rangle>p # 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)
+      (\<forall>x. \<lbrakk>(x \<Zsemi> \<lambda>m. (E(?n := x)) m), 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 fastforce
+  then have \<open>(\<forall>p [\<in>] A. \<lbrakk>E, F, G\<rbrakk> p) \<longrightarrow>
+      (\<forall>x. \<lbrakk>((x \<Zsemi> E)(Suc ?n := x)), F, G\<rbrakk> p) \<or> (\<exists>q [\<in>] B [\<div>] \<^bold>\<forall>p. \<lbrakk>E, F, G\<rbrakk> q)\<close>
+    unfolding add_upd_commute by blast
   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>
+  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
--- a/thys/FOL_Seq_Calc3/Syntax.thy
+++ b/thys/FOL_Seq_Calc3/Syntax.thy
@@ -1,93 +1,97 @@
 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>
+subsubsection \<open>Substitution\<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 add_env (infix \<open>\<Zsemi>\<close> 0) where
+  \<open>(t \<Zsemi> s) 0 = t\<close>
+| \<open>(t \<Zsemi> s) (Suc n) = s n\<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>
+primrec lift_tm where
+  \<open>lift_tm (\<^bold>#n) = \<^bold>#(n+1)\<close>
+| \<open>lift_tm (\<^bold>\<dagger>f ts) = \<^bold>\<dagger>f (map lift_tm ts)\<close>
+
+primrec sub_tm where
+  \<open>sub_tm s (\<^bold>#n) = s n\<close>
+| \<open>sub_tm s (\<^bold>\<dagger>f ts) = \<^bold>\<dagger>f (map (sub_tm s) ts)\<close>
+
+primrec sub_fm where
+  \<open>sub_fm s \<^bold>\<bottom> = \<^bold>\<bottom>\<close>
+| \<open>sub_fm s (\<^bold>\<ddagger>P ts) = \<^bold>\<ddagger>P (map (sub_tm s) ts)\<close>
+| \<open>sub_fm s (p \<^bold>\<longrightarrow> q) = sub_fm s p \<^bold>\<longrightarrow> sub_fm s q\<close>
+| \<open>sub_fm s (\<^bold>\<forall>p) = \<^bold>\<forall>(sub_fm (\<^bold>#0 \<Zsemi> \<lambda>n. lift_tm (s n)) p)\<close>
+
+abbreviation inst_single (\<open>\<langle>_\<rangle>\<close>) where
+  \<open>\<langle>t\<rangle>p \<equiv> sub_fm (t \<Zsemi> \<^bold>#) p\<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