diff --git a/thys/Lambda_Free_EPO/Chop.thy b/thys/Lambda_Free_EPO/Chop.thy
--- a/thys/Lambda_Free_EPO/Chop.thy
+++ b/thys/Lambda_Free_EPO/Chop.thy
@@ -1,350 +1,342 @@
 (*  Title:       The Chop Operation on Lambda-Free Higher-Order Terms
     Author:      Alexander Bentkamp <a.bentkamp at vu.nl>, 2018
     Maintainer:  Alexander Bentkamp <a.bentkamp at vu.nl>
 *)
 
 section \<open>The Chop Operation on Lambda-Free Higher-Order Terms\<close>
 
 theory Chop
 imports Embeddings
 begin
 
 definition chop :: "('s, 'v) tm \<Rightarrow> ('s, 'v) tm" where
   "chop t = apps (hd (args t)) (tl (args t))"
 
 subsection \<open>Basic properties\<close>
 
 lemma chop_App_Hd: "is_Hd s \<Longrightarrow> chop (App s t) = t" 
   unfolding chop_def args.simps 
   using args_Nil_iff_is_Hd by force
 
 lemma chop_apps: "is_App t \<Longrightarrow> chop (apps t ts) = apps (chop t) ts" 
   unfolding chop_def by (simp add: args_Nil_iff_is_Hd)
 
 lemma vars_chop: "is_App t \<Longrightarrow> vars (chop t) \<union> vars_hd (head t) = vars t" 
   by (induct rule:tm_induct_apps; metis (no_types, lifting) chop_def UN_insert Un_commute list.exhaust_sel list.simps(15)
       args_Nil_iff_is_Hd tm.simps(17) tm_exhaust_apps_sel vars_apps)
 
 lemma ground_chop: "is_App t \<Longrightarrow> ground t \<Longrightarrow> ground (chop t)" 
   using vars_chop by auto
 
-(* TODO: move? *)
-lemma size_apps: "size (apps t ts) = size t + sum_list (map size ts) + length ts"
-  by (induct ts arbitrary:t; simp)
+lemma hsize_chop: "is_App t \<Longrightarrow> (Suc (hsize (chop t))) = hsize t"
+  unfolding hsize_args[of t, symmetric] chop_def hsize_apps
+  by (metis Nil_is_map_conv args_Nil_iff_is_Hd list.exhaust_sel list.map_sel(1) map_tl plus_1_eq_Suc sum_list.Cons)
 
-(* TODO: move? *)
-lemma size_args_plus_num_args: "1 + sum_list (map size (args t)) + num_args t = size t"
-  by (metis One_nat_def size_apps tm.size(3) tm_collapse_apps)
-
-lemma size_chop: "is_App t \<Longrightarrow> Suc (Suc (size (chop t))) = size t"
-  unfolding size_args_plus_num_args[of t, symmetric] chop_def size_apps
-  by (metis Nitpick.size_list_simp(1) ab_semigroup_add_class.add_ac(1) args_Nil_iff_is_Hd plus_1_eq_Suc size_list_conv_sum_list)
-
-lemma size_chop_lt: "is_App t \<Longrightarrow> size (chop t) < size t"
-  by (simp add: Suc_le_lessD less_or_eq_imp_le size_chop)
+lemma hsize_chop_lt: "is_App t \<Longrightarrow> hsize (chop t) < hsize t"
+  by (simp add: Suc_le_lessD less_or_eq_imp_le hsize_chop)
 
 lemma chop_fun:
   assumes "is_App t" "is_App (fun t)" 
   shows "App (chop (fun t)) (arg t) = chop t"  
 proof -
   have "args (fun t) \<noteq> []"
     using assms(2) args_Nil_iff_is_Hd by blast
   then show ?thesis 
     unfolding chop_def
     using assms(1) by (metis (no_types) App_apps args.simps(2) hd_append2 tl_append2 tm.collapse(2))
 qed
 
 subsection \<open>Chop and the Embedding Relation\<close>
 
 lemma emb_step_chop: "is_App t \<Longrightarrow> t \<rightarrow>\<^sub>e\<^sub>m\<^sub>b chop t" 
 proof (induct "num_args t - 1" arbitrary:t)
   case 0
   have nil: "num_args t = 0 \<Longrightarrow> t \<rightarrow>\<^sub>e\<^sub>m\<^sub>b chop t" unfolding chop_def using 0 args_Nil_iff_is_Hd by force
   have single: "\<And>a. args t = [a] \<Longrightarrow> t \<rightarrow>\<^sub>e\<^sub>m\<^sub>b chop t" unfolding chop_def 
     by (metis "0.prems" apps.simps(1) args.elims args_Nil_iff_is_Hd emb_step_arg last.simps last_snoc list.sel(1) list.sel(3) tm.sel(6))
   then show ?case using nil single
     by (metis "0.hyps" length_0_conv length_tl list.exhaust_sel)
 next
   case (Suc x)
   have 1:"apps (Hd (head t)) (butlast (args t)) \<rightarrow>\<^sub>e\<^sub>m\<^sub>b chop (apps (Hd (head t)) (butlast (args t)))"
     using Suc(1)[of "apps (Hd (head t)) (butlast (args t))"]
     by (metis Suc.hyps(2) Suc_eq_plus1 add_diff_cancel_right' args_Nil_iff_is_Hd length_butlast list.size(3) nat.distinct(1) tm_exhaust_apps_sel tm_inject_apps)
   have 2:"App (apps (Hd (head t)) (butlast (args t))) (last (args t)) = t"
     by (simp add: App_apps Suc.prems args_Nil_iff_is_Hd)
   have 3:"App (chop (apps (Hd (head t)) (butlast (args t)))) (last (args t)) = chop t"
   proof -
     have f1: "hd (args t) = hd (butlast (args t))"
       by (metis Suc.hyps(2) Suc.prems append_butlast_last_id args_Nil_iff_is_Hd hd_append2 length_0_conv length_butlast nat.simps(3))
     have "tl (args t) = tl (butlast (args t)) @ [last (args t)]"
       by (metis (no_types) Suc.hyps(2) Suc.prems append_butlast_last_id args_Nil_iff_is_Hd length_0_conv length_butlast nat.simps(3) tl_append2)
     then show ?thesis
       using f1 chop_def 
       by (metis App_apps append_Nil args.simps(1) args_apps)
   qed
   then show ?case using 1 2 3 by (metis context_left)
 qed 
 
 lemma chop_emb_step_at:
   assumes "is_App t"
   shows "chop t = emb_step_at (replicate (num_args (fun t)) Left) Right t"
 using assms proof (induct "num_args (fun t)" arbitrary: t)
   case 0
   then have rep_Nil:"replicate (num_args (fun t)) dir.Left = []" 
     by simp 
   then show ?case unfolding rep_Nil 
     by (metis "0.hyps" "0.prems" emb_step_at_right append_Nil apps.simps(1) args.simps(2) chop_def length_0_conv list.sel(1) list.sel(3) tm.collapse(2)) 
 next
   case (Suc n)
   then show ?case using Suc.hyps(1)[of "fun t"]
     using emb_step_at_left_context args.elims args_Nil_iff_is_Hd chop_fun butlast_snoc diff_Suc_1 length_0_conv length_butlast nat.distinct(1) replicate_Suc tm.collapse(2) tm.sel(4)
     by metis
 qed
 
 lemma emb_step_at_chop:
   assumes emb_step_at: "emb_step_at p Right t = s"
     and pos:"position_of t (p @ [Right])"
     and all_Left: "list_all (\<lambda>x. x = Left) p"
   shows "chop t = s \<or> chop t \<rightarrow>\<^sub>e\<^sub>m\<^sub>b s"
 proof -
   have "is_App t" 
     by (metis emb_step_at_if_position emb_step_at_is_App emb_step_equiv pos)
   have p_replicate: "replicate (length p) Left = p" using replicate_length_same[of p Left]
     by (simp add: Ball_set all_Left)
   show ?thesis
   proof (cases "Suc (length p) = num_args t")
     case True
     then have "p = replicate (num_args (fun t)) Left" using p_replicate 
       by (metis Suc_inject \<open>is_App t\<close> args.elims args_Nil_iff_is_Hd length_append_singleton tm.sel(4))
     then have "chop t = s" unfolding chop_emb_step_at[OF \<open>is_App t\<close>] 
       using pos emb_step_at by blast
     then show ?thesis by blast
   next
     case False
     then have "Suc (length p) < num_args t"
       using pos emb_step_at \<open>is_App t\<close> \<open>list_all (\<lambda>x. x = dir.Left) p\<close>
     proof (induct p arbitrary:t s)
       case Nil
       then show ?case 
         by (metis Suc_lessI args_Nil_iff_is_Hd length_greater_0_conv list.size(3))
     next
       case (Cons a p)
       have "a = Left" 
         using Cons.prems(5) by auto
       have 1:"Suc (length p) \<noteq> num_args (fun t)"  
         by (metis (no_types, lifting) Cons.prems(1) Cons.prems(4) args.elims args_Nil_iff_is_Hd length_Cons length_append_singleton tm.sel(4))
       have 2:"position_of (fun t) (p @ [Right])"   using \<open>position_of t ((a # p) @ [Right])\<close> \<open>is_App t\<close> 
         by (metis (full_types) Cons.prems(5) position_of_left append_Cons list_all_simps(1) tm.collapse(2))
       have 3: "emb_step_at p dir.Right (fun t) = emb_step_at p dir.Right (fun t)" 
         using emb_step_at_left_context[of p Right "fun t" "arg t"] by blast
       have "Suc (length p) < num_args (fun t)" using Cons.hyps[OF 1 2 3] 
         by (metis "2" Cons.prems(5) Nil_is_append_conv list_all_simps(1) not_Cons_self2 position_of.elims(2) tm.discI(2))
       then show ?case 
         by (metis Cons.prems(4) Suc_less_eq2 args.simps(2) length_Cons length_append_singleton tm.collapse(2))
     qed      
     define q where "q = replicate (num_args (fun t) - Suc (length p)) dir.Left"
     have "chop t = emb_step_at (p @ [Left] @ q) dir.Right t"
     proof -
       have "length p + (num_args (fun t) - length p) = num_args (fun t)" 
         using \<open>Suc (length p) < num_args t\<close>
         by (metis Suc_less_eq2 \<open>is_App t\<close> args.simps(2) diff_Suc_1 leD length_butlast nat_le_linear 
             ordered_cancel_comm_monoid_diff_class.add_diff_inverse snoc_eq_iff_butlast tm.collapse(2))
       then have 1:"replicate (num_args (fun t)) dir.Left = p @ replicate (num_args (fun t) - length p) dir.Left" 
         by (metis p_replicate replicate_add)
       have "0 < num_args (fun t) - length p"
         by (metis (no_types) False \<open>is_App t\<close> \<open>length p + (num_args (fun t) - length p) = num_args (fun t)\<close> args.simps(2) length_append_singleton less_Suc_eq less_add_Suc1 tm.collapse(2) zero_less_diff)
       then have "replicate (num_args (fun t) - length p) dir.Left = [Left] @ q" unfolding q_def
         by (metis (no_types) Cons_replicate_eq Nat.diff_cancel Suc_eq_plus1 \<open>length p + (num_args (fun t) - length p) = num_args (fun t)\<close> append_Cons self_append_conv2)
       then show ?thesis using chop_emb_step_at
         using \<open>is_App t\<close> 1
         by (simp add: chop_emb_step_at)
     qed
     then have "chop t \<rightarrow>\<^sub>e\<^sub>m\<^sub>b s"
       using pos merge_emb_step_at[of p Right q Right t] 
       by (metis emb_step_at_if_position opp_simps(1) emb_step_at pos_emb_step_at_opp)
     then show ?thesis by blast
   qed
 qed
 
 lemma emb_step_at_remove_arg:
   assumes emb_step_at: "emb_step_at p Left t = s"
     and pos:"position_of t (p @ [Left])"
     and all_Left: "list_all (\<lambda>x. x = Left) p"
   shows "let i = num_args t - Suc (length p) in 
   head t = head s \<and> i < num_args t \<and> args s = take i (args t) @ drop (Suc i) (args t)"
 proof -
   have "is_App t" 
     by (metis emb_step_at_if_position emb_step_at_is_App emb_step_equiv pos)
   have C1: "head t = head s" 
     using all_Left emb_step_at pos proof (induct p arbitrary:s t)
     case Nil
     then have "s = emb_step_at [] dir.Left (App (fun t) (arg t))"
       by (metis position_of.elims(2) snoc_eq_iff_butlast tm.collapse(2) tm.discI(2))
     then have "s = fun t" by simp
     then show ?case by simp
   next
     case (Cons a p)
     then have "a = Left" by simp
     then have "head (emb_step_at p Left (fun t)) = head t" 
       by (metis Cons.hyps Cons.prems(1) head_fun list.pred_inject(2) position_if_emb_step_at)
     then show ?case using emb_step_at_left_context[of p a "fun t" "arg t"]
       by (metis Cons.prems(2) \<open>a = Left\<close> emb_step_at_is_App head_App tm.collapse(2)) 
   qed
 
   let ?i = "num_args t - Suc (length p)"
 
   have C2:"?i < num_args t" 
     by (simp add: \<open>is_App t\<close> args_Nil_iff_is_Hd)
 
   have C3:"args s = take ?i (args t) @ drop (Suc ?i) (args t)"
     using all_Left pos emb_step_at \<open>is_App t\<close> proof (induct p arbitrary:s t)
     case Nil
     then show ?case using emb_step_at_left[of "fun t" "arg t"]
       by (simp, metis One_nat_def args.simps(2) butlast_conv_take butlast_snoc tm.collapse(2))
   next
     case (Cons a p)
     have "position_of (fun t) (p @ [Left])"
       by (metis (full_types) Cons.prems(1) Cons.prems(2) Cons.prems(4) position_of_left 
           append_Cons list.pred_inject(2) tm.collapse(2))
     then have 0:"args (emb_step_at p Left (fun t))
                    = take (num_args (fun t) - Suc (length p)) (args (fun t)) 
                    @ drop (Suc (num_args (fun t) - Suc (length p))) (args (fun t))"
       using Cons.hyps[of "fun t"] by (metis Cons.prems(1) append_Nil args_Nil_iff_is_Hd drop_Nil 
           emb_step_at_is_App list.size(3) list_all_simps(1) take_0 zero_diff)
     have 1:"s = App (emb_step_at p Left (fun t)) (arg t)" using emb_step_at_left_context[of p Left "fun t" "arg t"] 
       using Cons.prems by auto
     define k where k_def:"k = (num_args (fun t) - Suc (length p))"
     have 2:"take k (args (fun t)) = take (num_args t - Suc (length (a # p))) (args t)"
       by (smt k_def Cons.prems(4) args.elims args_Nil_iff_is_Hd butlast_snoc diff_Suc_eq_diff_pred 
           diff_Suc_less length_Cons length_butlast length_greater_0_conv take_butlast tm.sel(4))
     have k_def': "k = num_args t - Suc (Suc (length p))" using k_def
       by (metis args.simps(2) diff_Suc_Suc length_append_singleton local.Cons(5) tm.collapse(2))
     have 3:"args (fun t) @ [arg t] = args t"
       by (metis Cons.prems(4) args.simps(2) tm.collapse(2))
     have "num_args t > 1" using \<open>position_of t ((a # p) @ [Left])\<close> 
       by (metis "3" \<open>position_of (fun t) (p @ [dir.Left])\<close> args_Nil_iff_is_Hd butlast_snoc emb_step.simps emb_step_at_if_position length_butlast length_greater_0_conv tm.discI(2) zero_less_diff)
     then have "Suc k<num_args t" unfolding k_def'
       using \<open>1 < num_args t\<close> by linarith
     have "\<forall>k< num_args t. drop k (args (fun t)) @ [arg t] = drop k (args t)"
       by (metis (no_types, lifting) \<open>args (fun t) @ [arg t] = args t\<close> drop_butlast drop_eq_Nil last_drop leD snoc_eq_iff_butlast)
     then show ?case using 0 1 2 3 k_def'
       using \<open>Suc k < num_args t\<close> k_def by auto
   qed
   show ?thesis using C1 C2 C3 by simp
 qed
 
 lemma emb_step_cases [consumes 1, case_names chop extended_chop remove_arg under_arg]:
   assumes emb:"t \<rightarrow>\<^sub>e\<^sub>m\<^sub>b s"
     and chop:"chop t = s \<Longrightarrow> P"
     and extended_chop:"chop t \<rightarrow>\<^sub>e\<^sub>m\<^sub>b s \<Longrightarrow> P"
     and remove_arg:"\<And>i. head t = head s \<Longrightarrow> i<num_args t \<Longrightarrow> args s = take i (args t) @ drop (Suc i) (args t) \<Longrightarrow> P"
     and under_arg:"\<And>i. head t = head s \<Longrightarrow> num_args t = num_args s \<Longrightarrow> args t ! i \<rightarrow>\<^sub>e\<^sub>m\<^sub>b args s ! i \<Longrightarrow>
          (\<And>j. j<num_args t \<Longrightarrow> i \<noteq> j \<Longrightarrow> args t ! j = args s ! j) \<Longrightarrow> P"
   shows P
 proof -
   obtain p d where pd_def:"emb_step_at p d t = s" "position_of t (p @ [d])"
     using emb emb_step_equiv' position_if_emb_step_at by metis
   have "is_App t"
     by (metis emb emb_step_at_is_App emb_step_equiv)
   show ?thesis 
   proof (cases "list_all (\<lambda>x. x = Left) p")
     case True
     show ?thesis 
     proof (cases d)
       case Left
       then show P using emb_step_at_remove_arg 
         by (metis True pd_def(1) pd_def(2) remove_arg)
     next
       case Right
       then show P 
         using True chop emb_step_at_chop extended_chop pd_def(1) pd_def(2) by blast
     qed
   next
     case False
     have 1:"num_args t = num_args s" using emb_step_under_args_num_args
       by (metis False pd_def(1))
     have 2:"head t = head s" using emb_step_under_args_head
       by (metis False pd_def(1))
     show ?thesis using 1 2 under_arg emb_step_under_args_emb_step
       by (metis False pd_def(1) pd_def(2))
   qed
 qed
 
 lemma chop_position_of:
   assumes "is_App s"
   shows "position_of s (replicate (num_args (fun s)) dir.Left @ [Right])"
-  by (metis Suc_n_not_le_n assms chop_emb_step_at lessI less_imp_le_nat position_if_emb_step_at size_chop)
+  by (metis Suc_n_not_le_n assms chop_emb_step_at lessI less_imp_le_nat position_if_emb_step_at hsize_chop)
 
 subsection \<open>Chop and Substitutions\<close>
 
 (* TODO: move *)
 lemma Suc_num_args: "is_App t \<Longrightarrow> Suc (num_args (fun t)) = num_args t" 
   by (metis args.simps(2) length_append_singleton tm.collapse(2))
 
 (* TODO: move *)
 lemma fun_subst: "is_App s \<Longrightarrow> subst \<rho> (fun s) = fun (subst \<rho> s)"
   by (metis subst.simps(2) tm.collapse(2) tm.sel(4))
 
 (* TODO: move *)
 lemma args_subst_Hd:
   assumes "is_Hd (subst \<rho> (Hd (head s)))"
   shows  "args (subst \<rho> s) = map (subst \<rho>) (args s)"
   using assms 
   by (metis append_Nil args_Nil_iff_is_Hd args_apps subst_apps tm_exhaust_apps_sel)
 
 lemma chop_subst_emb0:
   assumes "is_App s"
   assumes "chop (subst \<rho> s) \<noteq> subst \<rho> (chop s)"
   shows "emb_step_at (replicate (num_args (fun s)) Left) Right (chop (subst \<rho> s)) = subst \<rho> (chop s)"
 proof -
   have "is_App (subst \<rho> s)"
     by (metis assms(1) subst.simps(2) tm.collapse(2) tm.disc(2))
   have 1:"subst \<rho> (chop s) = emb_step_at (replicate (num_args (fun s)) dir.Left) dir.Right (subst \<rho>  s)"
     using chop_emb_step_at[OF assms(1)] using emb_step_at_subst chop_position_of[OF \<open>is_App s\<close>] 
     by (metis)
   have "num_args (fun s) \<le> num_args (fun (subst \<rho> s))" 
     using fun_subst[OF \<open>is_App s\<close>] 
     by (metis args_subst leI length_append length_map not_add_less2)
   then have "num_args (fun s) < num_args (fun (subst \<rho> s))" 
     using assms(2) "1" \<open>is_App (subst \<rho> s)\<close> chop_emb_step_at le_imp_less_or_eq 
     by fastforce
   then have "num_args s \<le> num_args (fun (subst \<rho> s))" 
     using Suc_num_args[OF \<open>is_App s\<close>] by linarith
   then have  "replicate (num_args (fun s)) dir.Left @
         [opp dir.Right] @ replicate (num_args (fun (subst \<rho> s)) - num_args s) dir.Left =
         replicate (num_args (fun (subst \<rho> s))) dir.Left" 
     unfolding append.simps opp_simps replicate_Suc[symmetric] replicate_add[symmetric]
     using Suc_num_args[OF \<open>is_App s\<close>]
     by (metis add_Suc_shift ordered_cancel_comm_monoid_diff_class.add_diff_inverse)
   then show ?thesis unfolding 1
     unfolding  chop_emb_step_at[OF \<open>is_App (subst \<rho> s)\<close>]
     by (metis merge_emb_step_at)
 qed
 
 lemma chop_subst_emb:
   assumes "is_App s"
   shows "chop (subst \<rho> s) \<unrhd>\<^sub>e\<^sub>m\<^sub>b subst \<rho> (chop s)"
   using chop_subst_emb0
   by (metis assms emb.refl emb_step_equiv emb_step_is_emb)
 
 lemma chop_subst_Hd:
   assumes "is_App s"
   assumes "is_Hd (subst \<rho> (Hd (head s)))"
   shows "chop (subst \<rho> s) = subst \<rho> (chop s)" 
 proof -
   have "is_App (subst \<rho> s)"
     by (metis assms(1) subst.simps(2) tm.collapse(2) tm.disc(2))
   have "num_args (fun s) = num_args (fun (subst \<rho> s))" unfolding fun_subst[OF \<open>is_App s\<close>,symmetric]
     using args_subst_Hd using assms(2) by auto
   then show ?thesis
     unfolding chop_emb_step_at[OF assms(1)] chop_emb_step_at[OF \<open>is_App (subst \<rho> s)\<close>]
     using emb_step_at_subst[OF chop_position_of[OF \<open>is_App s\<close>]]
     by simp
 qed
 
 lemma chop_subst_Sym:
   assumes "is_App s"
   assumes "is_Sym (head s)"
   shows "chop (subst \<rho> s) = subst \<rho> (chop s)" 
   by (metis assms(1) assms(2) chop_subst_Hd ground_imp_subst_iden hd.collapse(2) hd.simps(18) tm.disc(1) tm.simps(17))
 
 end
\ No newline at end of file
diff --git a/thys/Lambda_Free_EPO/Embeddings.thy b/thys/Lambda_Free_EPO/Embeddings.thy
--- a/thys/Lambda_Free_EPO/Embeddings.thy
+++ b/thys/Lambda_Free_EPO/Embeddings.thy
@@ -1,1025 +1,1025 @@
 (*  Title:       The Embedding Relation for Lambda-Free Higher-Order Terms
     Author:      Alexander Bentkamp <a.bentkamp at vu.nl>, 2018
     Maintainer:  Alexander Bentkamp <a.bentkamp at vu.nl>
 *)
 
 section \<open>The Embedding Relation for Lambda-Free Higher-Order Terms\<close>
 
 theory Embeddings
   imports Lambda_Free_RPOs.Lambda_Free_Term Lambda_Free_RPOs.Extension_Orders
 begin
 
 subsection \<open>Positions of terms\<close>
 
 datatype dir = Left | Right
 
 fun position_of :: "('s,'v) tm \<Rightarrow> dir list \<Rightarrow> bool" where
   position_of_Nil: "position_of _ [] = True" |
   position_of_Hd: "position_of (Hd _) (_#_) = False" |
   position_of_left: "position_of (App t s) (Left # ds) = position_of t ds" |
   position_of_right: "position_of (App t s) (Right # ds) = position_of s ds"
 
 definition opp :: "dir \<Rightarrow> dir" where
   "opp d = (if d = Right then Left else Right)"
 
 lemma opp_simps[simp]:
   "opp Right = Left" 
   "opp Left = Right"
   using opp_def by auto
 
 lemma shallower_pos: "position_of t (p @ q @ [dq]) \<Longrightarrow> position_of t (p @ [dp])" 
 proof (induct p arbitrary:t)
   case Nil
   then show ?case 
     apply (cases t)
      apply (metis position_of_Hd Nil_is_append_conv list.exhaust)
     by (metis (full_types) position_of_Nil position_of_left
         position_of_right dir.exhaust self_append_conv2)
 next
   case (Cons a p)
   then show ?case 
     apply (cases a) 
     apply (metis position_of_Hd position_of_left append_Cons args.cases)
     by (metis position_of_Hd position_of_right append_Cons args.cases)
 qed
 
 lemma no_position_replicate_num_args: "\<not> position_of t (replicate (num_args t) Left @ [d])"
 proof (induct "num_args t" arbitrary:t)
   case 0
   have "is_Hd t" 
     using "0.hyps" args_Nil_iff_is_Hd by auto
   then show ?case
     by (metis position_of.elims(2) snoc_eq_iff_butlast tm.discI(2))
 next
   case (Suc n)
   have "is_App t" 
     using Suc.hyps(2) args_Nil_iff_is_Hd by force
   then have "\<not> position_of (fun t) (replicate (num_args (fun t)) dir.Left @ [d])" using Suc.hyps(1)[of "fun t"] 
     by (metis Suc Suc_inject args.elims length_0_conv length_append_singleton nat.distinct(1) tm.sel(4))
   have "\<And>ds. replicate (num_args t) dir.Left @ [d] \<noteq> dir.Right # ds" 
     by (metis \<open>is_App t\<close> args_Nil_iff_is_Hd dir.distinct(1) hd_append hd_replicate length_0_conv list.sel(1) replicate_empty)
   then show ?case using position_of.elims(2)[of t "(replicate (num_args t) dir.Left @ [d])"]
     by (metis position_of_left \<open>\<not> position_of (fun t) (replicate (num_args (fun t)) dir.Left @ [d])\<close> 
     \<open>is_App t\<close> append_Cons args.simps(2) length_append_singleton replicate_Suc tm.collapse(2))
 qed
 
 lemma shorten_position:"position_of t (p @ q) \<Longrightarrow> position_of t p"
 proof (induct q rule: rev_induct)
 case Nil
   then show ?case 
     by simp
 next
   case (snoc x xs)
   then show ?case
     by (metis position_of_Nil append_assoc append_butlast_last_id shallower_pos)
 qed
 
 subsection \<open>Embedding step\<close>
 
 text \<open>Embedding step at a given position. If the position is not present, default to identity.\<close>
 
 fun emb_step_at :: "dir list \<Rightarrow> dir \<Rightarrow> ('s, 'v) tm  \<Rightarrow> ('s, 'v) tm"  where
   emb_step_at_left:"emb_step_at [] Left (App t s) = t"
 | emb_step_at_right:"emb_step_at [] Right (App t s) = s"
 | emb_step_at_left_context:"emb_step_at (Left # p) dir (App t s) = App (emb_step_at p dir t) s"
 | emb_step_at_right_context:"emb_step_at (Right # p) dir (App t s) = App t (emb_step_at p dir s)"
 | emb_step_at_head:"emb_step_at _ _ (Hd h) = Hd h"
 
 abbreviation "emb_step_at' p t == emb_step_at (butlast p) (last p) t"
 
 lemmas emb_step_at_induct = emb_step_at.induct[case_names left right left_context right_context head]
 
 lemma emb_step_at_is_App:"emb_step_at p d u \<noteq> u \<Longrightarrow> is_App u"
   by (metis emb_step_at.simps(5) is_Hd_def)
 
 text \<open>Definition of an embedding step without using positions.\<close>
 
 inductive emb_step (infix "\<rightarrow>\<^sub>e\<^sub>m\<^sub>b" 50) where 
   left: "(App t1 t2) \<rightarrow>\<^sub>e\<^sub>m\<^sub>b t1" |
   right: "(App t1 t2) \<rightarrow>\<^sub>e\<^sub>m\<^sub>b t2" |
   context_left: "t \<rightarrow>\<^sub>e\<^sub>m\<^sub>b s \<Longrightarrow> (App t u) \<rightarrow>\<^sub>e\<^sub>m\<^sub>b (App s u)" |
   context_right: "t \<rightarrow>\<^sub>e\<^sub>m\<^sub>b s \<Longrightarrow> (App u t) \<rightarrow>\<^sub>e\<^sub>m\<^sub>b (App u s)"
 
 text \<open>The two definitions of an embedding step are equivalent:\<close>
 
 lemma emb_step_equiv: "emb_step t s \<longleftrightarrow> (\<exists>p d. emb_step_at p d t = s) \<and> t \<noteq> s"
 proof
   show "t \<rightarrow>\<^sub>e\<^sub>m\<^sub>b s \<Longrightarrow> (\<exists>p d. emb_step_at p d t = s) \<and> t \<noteq> s"
   proof (induct t s rule:emb_step.induct) 
     case left
     then show ?case
       by (metis add_Suc_right emb_step_at.simps(1) leD le_add_same_cancel1 le_imp_less_Suc tm.size(4) zero_order(1))
   next
     case right
     then show ?case
       by (metis add.right_neutral add_le_cancel_left antisym emb_step_at.simps(2) le_add_same_cancel2 le_imp_less_Suc length_greater_0_conv list.size(3) tm.size(4) zero_order(1))
   next
     case (context_left t s)
     obtain p d where "emb_step_at p d t = s" 
       using context_left.hyps(2) by blast
     then have "\<And>u. emb_step_at (Left # p) d (App t u) = App s u"
       by (metis emb_step_at.simps(3))
     then show ?case
       using context_left.hyps(2) by blast
   next
     case (context_right t s)
     obtain p d where "emb_step_at p d t = s" 
       using context_right.hyps(2) by blast
     then have "\<And>u. emb_step_at (Right # p) d (App u t) = App u s"
       by (metis emb_step_at.simps(4))
     then show ?case
       using context_right.hyps(2) by blast
   qed
   show "(\<exists>p d. emb_step_at p d t = s) \<and> t \<noteq> s \<Longrightarrow> t \<rightarrow>\<^sub>e\<^sub>m\<^sub>b s"
   proof -
     assume "(\<exists>p d. emb_step_at p d t = s) \<and> t \<noteq> s"
     then obtain p d where "emb_step_at p d t = s" "t \<noteq> s" by blast
     then show ?thesis
     proof (induct arbitrary:t rule:emb_step_at_induct)
       case (left u1 u2)
       show ?case using left(1)
         apply (rule emb_step_at.elims) 
         using emb_step.left by blast+
     next
       case (right u1 u2)
       show ?case  using right(1)
         apply (rule emb_step_at.elims) 
         using emb_step.right by blast+
     next
       case (left_context u1 u2 t' s')
       show ?case 
         by (metis emb_step_at_left_context emb_step.simps emb_step_at_is_App left_context.hyps left_context.prems(1) left_context.prems(2) 
             tm.collapse(2) tm.inject(2)) 
     next
       case (right_context u1 u2 t' s')
       show ?case 
         by (metis emb_step_at_right_context emb_step.simps emb_step_at_is_App right_context.hyps right_context.prems(1) right_context.prems(2) tm.collapse(2) tm.inject(2))          
     next
       case (head uu uv h)
       show ?case using head(1)
         apply (rule emb_step_at.elims)
         using emb_step.left apply blast
         using emb_step.right apply blast
         apply simp_all
         using head.prems(2) by blast
     qed
   qed
 qed
 
 lemma emb_step_fun: "is_App t \<Longrightarrow> t \<rightarrow>\<^sub>e\<^sub>m\<^sub>b (fun t)"
   by (metis emb_step.intros(1) tm.collapse(2))
 
 lemma emb_step_arg: "is_App t \<Longrightarrow> t \<rightarrow>\<^sub>e\<^sub>m\<^sub>b (arg t)"
   by (metis emb_step.intros(2) tm.collapse(2))
 
-lemma emb_step_size: "t \<rightarrow>\<^sub>e\<^sub>m\<^sub>b s \<Longrightarrow> size t > size s" 
+lemma emb_step_hsize: "t \<rightarrow>\<^sub>e\<^sub>m\<^sub>b s \<Longrightarrow> hsize t > hsize s" 
   by (induction rule: emb_step.induct; simp_all) 
 
 lemma emb_step_vars: "t \<rightarrow>\<^sub>e\<^sub>m\<^sub>b s \<Longrightarrow> vars s \<subseteq> vars t" 
   by (induction rule: emb_step.induct, auto)
 
 lemma emb_step_equiv': "emb_step t s \<longleftrightarrow> (\<exists>p. p \<noteq> [] \<and> emb_step_at' p t = s) \<and> t \<noteq> s"
   using butlast_snoc emb_step_equiv last_snoc
   by (metis snoc_eq_iff_butlast)
 
 lemma position_if_emb_step_at: "emb_step_at p d t = u \<Longrightarrow> t \<noteq> u \<Longrightarrow> position_of t (p @ [d])"
 proof (induct p arbitrary:t u)
   case Nil
   then show ?case by (metis emb_step_at_head position_of_Nil append_self_conv2 list.sel(3) position_of.elims(3))
 next
   case (Cons a p)
   then show ?case  
   proof (cases t)
     case (Hd x)
     then show ?thesis using Cons by simp
   next
     case (App t1 t2)
     then show ?thesis using Cons  apply (cases a) apply simp 
       apply blast 
       by auto
   qed
 qed
 
 lemma emb_step_at_if_position:
   assumes
     "position_of t (p @ [d])"
   shows "t \<rightarrow>\<^sub>e\<^sub>m\<^sub>b emb_step_at p d t" 
   using assms proof (induct p arbitrary:t)
   case Nil
   then show ?case
     by (cases d;cases t;simp add: emb_step.left emb_step.right)
 next
   case (Cons a p)
   then show ?case
     apply (cases a) 
      apply (cases t)  
       apply (simp_all add: context_left context_right)
     apply (cases t) 
     by (simp_all add: context_left context_right)
 qed
 
 subsection \<open>Embedding relation\<close>
 
 text \<open>Definition of an embedding as a sequence of embedding steps at given positions:\<close>
 
 fun emb_at :: "(dir list \<times> dir) list \<Rightarrow> ('s, 'v) tm  \<Rightarrow> ('s, 'v) tm" where
   emb_at_Nil: "emb_at [] t = t" |
   emb_at_Cons: "emb_at ((p,d) # ps) t = emb_step_at p d (emb_at ps t)"
 
 text \<open>Definition of an embedding without using positions:\<close>
 
 inductive emb (infix "\<unrhd>\<^sub>e\<^sub>m\<^sub>b" 50) where
   refl: "t \<unrhd>\<^sub>e\<^sub>m\<^sub>b t" |
   step: "t \<unrhd>\<^sub>e\<^sub>m\<^sub>b u \<Longrightarrow> u \<rightarrow>\<^sub>e\<^sub>m\<^sub>b s \<Longrightarrow> t \<unrhd>\<^sub>e\<^sub>m\<^sub>b s"
 
 abbreviation emb_neq (infix "\<rhd>\<^sub>e\<^sub>m\<^sub>b" 50) where "emb_neq t s \<equiv> t \<unrhd>\<^sub>e\<^sub>m\<^sub>b s \<and> t \<noteq> s"
 
 text \<open>The two definitions coincide:\<close>
 
 lemma emb_equiv: "(t \<unrhd>\<^sub>e\<^sub>m\<^sub>b s) = (\<exists>ps. emb_at ps t = s)"
 proof
   show "\<exists>ps. emb_at ps t = s \<Longrightarrow> t \<unrhd>\<^sub>e\<^sub>m\<^sub>b s"
   proof -
     assume "\<exists>ps. emb_at ps t = s"
     then obtain ps where "emb_at ps t = s"
       by blast
     then show ?thesis 
     proof (induct ps arbitrary:s)
       case Nil
       then show ?case by (simp add: emb.refl)
     next
       case (Cons a ps)
       show ?case 
         using Cons(2) apply (rule emb_at.elims)
        apply simp
        by (metis Cons.hyps emb.simps emb_step_equiv list.inject)
     qed
   qed
 next
   show "t \<unrhd>\<^sub>e\<^sub>m\<^sub>b s \<Longrightarrow> \<exists>ps. emb_at ps t = s"
   proof (induct rule: emb.induct)
     case (refl t)
     then show ?case
       using emb_at_Nil by blast
   next
     case (step t u s)
     then show ?case
       by (metis emb_at_Cons emb_step_equiv)
   qed
 qed
 
 lemma emb_at_trans: "emb_at ps t = u \<Longrightarrow> emb_at qs u = s \<Longrightarrow> emb_at (qs @ ps) t = s"
   by (induct qs arbitrary:s; auto)
 
 lemma emb_trans: "t \<unrhd>\<^sub>e\<^sub>m\<^sub>b u \<Longrightarrow> u \<unrhd>\<^sub>e\<^sub>m\<^sub>b s \<Longrightarrow> t \<unrhd>\<^sub>e\<^sub>m\<^sub>b s"
   by (metis emb_at_trans emb_equiv)
 
 lemma emb_step_is_emb: "t \<rightarrow>\<^sub>e\<^sub>m\<^sub>b s \<Longrightarrow> t \<unrhd>\<^sub>e\<^sub>m\<^sub>b s"
   by (meson emb.simps)
 
-lemma emb_size: "t \<unrhd>\<^sub>e\<^sub>m\<^sub>b s \<Longrightarrow> size t \<ge> size s" 
+lemma emb_hsize: "t \<unrhd>\<^sub>e\<^sub>m\<^sub>b s \<Longrightarrow> hsize t \<ge> hsize s" 
   apply (induction rule: emb.induct)
   apply simp
-  using emb_step_size by fastforce
+  using emb_step_hsize by fastforce
 
 lemma emb_prepend_step: "t \<rightarrow>\<^sub>e\<^sub>m\<^sub>b u \<Longrightarrow> u \<unrhd>\<^sub>e\<^sub>m\<^sub>b s \<Longrightarrow> t \<unrhd>\<^sub>e\<^sub>m\<^sub>b s"
   using emb_step_is_emb emb_trans by blast
 
 lemma sub_emb: "sub s t \<Longrightarrow> t \<unrhd>\<^sub>e\<^sub>m\<^sub>b s"
 proof (induction rule:sub.induct)
   case (sub_refl s)
   then show ?case 
     by (simp add: emb.refl)
 next
   case (sub_fun s t u)
   then show ?case 
     using emb_prepend_step right by blast
 next
   case (sub_arg s t u)
   then show ?case
     using emb_prepend_step left by blast
 qed
 
 lemma sequence_emb_steps: "t \<unrhd>\<^sub>e\<^sub>m\<^sub>b s \<longleftrightarrow> (\<exists>us. us\<noteq>[] \<and> hd us = t \<and> last us = s \<and> (\<forall>i. Suc i < length us \<longrightarrow> us ! i \<rightarrow>\<^sub>e\<^sub>m\<^sub>b us ! Suc i))"
 proof
   show "t \<unrhd>\<^sub>e\<^sub>m\<^sub>b s \<Longrightarrow> \<exists>us. us\<noteq>[] \<and> hd us = t \<and> last us = s \<and> (\<forall>i. Suc i < length us \<longrightarrow> us ! i \<rightarrow>\<^sub>e\<^sub>m\<^sub>b us ! Suc i)"
   proof (induct rule:emb.induct)
     case (refl t)
     then show ?case 
       using Suc_less_eq add.right_neutral add_Suc_right append_Nil last_snoc list.sel(1) list.size(3) list.size(4) not_less_zero
       by auto
   next
     case (step t u s)
     then obtain us where 
       "us \<noteq> []" 
       "hd us = t" 
       "last us = u" 
       "\<forall>i. Suc i < length us \<longrightarrow> us ! i \<rightarrow>\<^sub>e\<^sub>m\<^sub>b us ! Suc i" by blast
     then have "hd (us @ [s]) = t" "last (us @ [s]) = s" by simp_all
     moreover have  "(\<forall>i. Suc i < length (us @ [s]) \<longrightarrow> (us @ [s]) ! i \<rightarrow>\<^sub>e\<^sub>m\<^sub>b (us @ [s]) ! Suc i)" 
       by (metis (mono_tags, lifting) Suc_less_eq \<open>\<forall>i. Suc i < length us \<longrightarrow> us ! i \<rightarrow>\<^sub>e\<^sub>m\<^sub>b us ! Suc i\<close> \<open>last us = u\<close> \<open>us \<noteq> []\<close> 
            append_butlast_last_id length_append_singleton less_antisym nth_append nth_append_length step.hyps(3))
     ultimately show ?case by blast
   qed
   show "\<exists>us. us \<noteq> [] \<and> hd us = t \<and> last us = s \<and> (\<forall>i. Suc i < length us \<longrightarrow> us ! i \<rightarrow>\<^sub>e\<^sub>m\<^sub>b us ! Suc i) \<Longrightarrow> t \<unrhd>\<^sub>e\<^sub>m\<^sub>b s"
   proof -
     assume "\<exists>us. us \<noteq> [] \<and> hd us = t \<and> last us = s \<and> (\<forall>i. Suc i < length us \<longrightarrow> us ! i \<rightarrow>\<^sub>e\<^sub>m\<^sub>b us ! Suc i)"
     then obtain us where "us \<noteq> []" "hd us = t" "last us = s" "\<forall>i. Suc i < length us \<longrightarrow> us ! i \<rightarrow>\<^sub>e\<^sub>m\<^sub>b us ! Suc i" by blast
     then show ?thesis
     proof (induct us arbitrary:t)
       case Nil
       then show ?case by simp
     next
       case (Cons a us)
       then show ?case
         using emb.refl emb_step_is_emb emb_trans hd_conv_nth by fastforce
     qed
   qed
 qed
 
 lemma emb_induct_reverse [consumes 1, case_names refl step]:
   assumes
 emb: "t \<unrhd>\<^sub>e\<^sub>m\<^sub>b s" and
 refl: "\<And>t. P t t" and
 step: "\<And>t u s. t \<rightarrow>\<^sub>e\<^sub>m\<^sub>b u \<Longrightarrow> u \<unrhd>\<^sub>e\<^sub>m\<^sub>b s \<Longrightarrow> P u s \<Longrightarrow> P t s"
 shows 
 "P t s"
 proof -
   obtain us where "us\<noteq>[]" "hd us = t" "last us = s" "\<forall>i. Suc i < length us \<longrightarrow> us ! i \<rightarrow>\<^sub>e\<^sub>m\<^sub>b us ! Suc i"
     using emb sequence_emb_steps by blast
   define us' where "us' == tl us"
   then have "last ([t] @ us') = s" "\<forall>i. i < length us' \<longrightarrow> ([t] @ us') ! i \<rightarrow>\<^sub>e\<^sub>m\<^sub>b ([t] @ us') ! Suc i" 
     using \<open>hd us = t\<close> \<open>last us = s\<close> \<open>us \<noteq> []\<close> apply force 
     using \<open>\<forall>i. Suc i < length us \<longrightarrow> us ! i \<rightarrow>\<^sub>e\<^sub>m\<^sub>b us ! Suc i\<close> \<open>hd us = t\<close> \<open>us \<noteq> []\<close> us'_def by force
   then show ?thesis
   proof (induct us' arbitrary:t)
     case Nil
   then show ?case
     by (simp add: local.refl)
   next
     case (Cons a us')
     then have "P a s" 
       by (metis Suc_mono append_Cons append_Nil last.simps length_Cons list.discI nth_Cons_Suc)
     have "t \<rightarrow>\<^sub>e\<^sub>m\<^sub>b a" 
       using Cons.prems(2) by auto
     have "a \<unrhd>\<^sub>e\<^sub>m\<^sub>b s" unfolding sequence_emb_steps 
       by (metis append_Cons append_Nil last_append list.sel(1) list.simps(3) local.Cons(2) local.Cons(3) nth_Cons_Suc)
     show ?case using step[OF \<open>t \<rightarrow>\<^sub>e\<^sub>m\<^sub>b a\<close> \<open>a \<unrhd>\<^sub>e\<^sub>m\<^sub>b s\<close> \<open>P a s\<close>] .
   qed
 qed
 
 lemma emb_cases_reverse [consumes 1, case_names refl step]: 
   "t \<unrhd>\<^sub>e\<^sub>m\<^sub>b s \<Longrightarrow> (\<And>t'. t = t' \<Longrightarrow> s = t' \<Longrightarrow> P) \<Longrightarrow> (\<And>t' u s'. t = t' \<Longrightarrow> s = s' \<Longrightarrow> t' \<rightarrow>\<^sub>e\<^sub>m\<^sub>b u \<Longrightarrow> u \<unrhd>\<^sub>e\<^sub>m\<^sub>b s' \<Longrightarrow> P) \<Longrightarrow> P"
   by (induct rule:emb_induct_reverse; blast+)
 
 lemma emb_vars: "t \<unrhd>\<^sub>e\<^sub>m\<^sub>b s \<Longrightarrow> vars s \<subseteq> vars t"
   apply (induct rule: emb.induct)
    apply simp
   using emb_step_vars by auto
 
 lemma ground_emb: "t \<unrhd>\<^sub>e\<^sub>m\<^sub>b s \<Longrightarrow> ground t \<Longrightarrow> ground s"
   using emb_vars by blast
 
 lemma arg_emb: "s \<in> set (args t) \<Longrightarrow> t \<unrhd>\<^sub>e\<^sub>m\<^sub>b s" 
   by (simp add: sub_args sub_emb)
 
 lemma emb_step_at_subst:
   assumes
     "position_of t (p @ [d])"
   shows
     "emb_step_at p d (subst \<rho> t) = subst \<rho> (emb_step_at p d t)"
 using assms proof (induction p arbitrary:t)
   case Nil
   then obtain t1 t2 where "t = App t1 t2" 
     using position_of_Hd append_Nil tm.collapse(1) 
     by (metis tm.collapse(2))
   then show ?case 
     by (cases d; simp add: \<open>t = App t1 t2\<close>)
 next
   case (Cons a p)
   then obtain t1 t2 where "t = App t1 t2" 
     using position_of.elims(2) by blast
   then show ?case 
     using Cons.IH Cons.prems by (cases a;auto)
 qed
 
 lemma emb_step_subst: "t \<rightarrow>\<^sub>e\<^sub>m\<^sub>b s \<Longrightarrow> subst \<rho> t \<rightarrow>\<^sub>e\<^sub>m\<^sub>b subst \<rho> s"
   by (induct rule:emb_step.induct;
       simp_all add: emb_step.left emb_step.right context_left context_right)
 
 lemma emb_subst: "t  \<unrhd>\<^sub>e\<^sub>m\<^sub>b s \<Longrightarrow> subst \<rho> t \<unrhd>\<^sub>e\<^sub>m\<^sub>b subst \<rho> s"
   apply (induct rule:emb.induct)
   apply (simp add: emb.refl)
   using emb.step emb_step_subst by blast
 
-lemma emb_size_neq:
+lemma emb_hsize_neq:
   assumes
     "t \<unrhd>\<^sub>e\<^sub>m\<^sub>b s" "t \<noteq> s"
   shows 
-    "size t > size s"
-  by (metis assms(1) assms(2) emb_cases_reverse emb_size emb_step_size leD le_imp_less_or_eq)
+    "hsize t > hsize s"
+  by (metis assms(1) assms(2) emb_cases_reverse emb_hsize emb_step_hsize leD le_imp_less_or_eq)
 
 subsection \<open>How are positions preserved under embedding steps?\<close>
 
 text \<open>Disjunct positions are preserved: For example, [L,R] is a position of f a (g b). When performing
 an embedding step at [R,R] to obtain f a b, the position [L,R] still exists. (More precisely, it even
 contains the same subterm, namely a.)\<close>
 
 lemma pos_emb_step_at_disjunct:
   assumes
 "take (length q) p \<noteq> q"
 "take (length p) q \<noteq> p"
 shows
 "position_of t (p @ [d1]) \<longleftrightarrow> position_of  (emb_step_at q d2 t) (p @ [d1])"
   using assms
 proof (induct "length p + length q" arbitrary:t p q rule:less_induct)
   case less
   then show ?case
   proof (cases "is_Hd t \<or> p = [] \<or> q = []")
     case True
     then show ?thesis
       by (metis emb_step_at_is_App less.prems(1) less.prems(2) list.size(3) take_eq_Nil)
   next
     case False
     then obtain t1 t2 p0 p' q0 q' where "t = App t1 t2" "p = p0 # p'" "q = q0 # q'"
       by (metis list.collapse tm.collapse(2))
     then show ?thesis 
       apply (cases p0; cases q0) 
       using less.hyps less.prems(1) less.prems(2) by auto
   qed
 qed
 
 text \<open>Even if only the last element of a position differs from the position of an embedding step, that
 position is preserved. For example, [L] is a position of f (g b). After performing an embedding step
 at [R,R] to obtain f b, the position [L] still exists. (More precisely, it even
 contains the same subterm, namely f.)\<close>
 
 lemma pos_emb_step_at_opp:
     "position_of t (p@[d1]) \<longleftrightarrow> position_of (emb_step_at (p @ [opp d1] @ q) d2 t) (p@[d1])"
 proof (induct p arbitrary:t)
   case Nil
   then show ?case by (cases t, simp, cases d1, simp_all)
 next
   case (Cons a p)
   then show ?case 
     apply (cases a) 
     apply (metis emb_step_at_left_context position_of_left append_Cons emb_step_at_is_App tm.collapse(2))
     by (metis emb_step_at_right_context position_of_right append_Cons emb_step_at_is_App tm.collapse(2))
 qed
 
 text \<open>Positions are preserved under embedding steps below them:\<close>
 
 lemma pos_emb_step_at_nested:
   shows "position_of (emb_step_at (p @ [d1] @ q) d2 t) (p @ [d1]) \<longleftrightarrow> position_of t (p @ [d1])"
 proof (induct p arbitrary:t)
   case Nil
   then show ?case by (cases t, simp, cases d1, simp_all)
 next
   case (Cons a p)
   then show ?case 
     apply (cases a;cases t) 
     using Cons.hyps Cons.prems by auto 
 qed
 
 subsection "Swapping embedding steps"
 
 text \<open>The order of embedding steps at disjunct position can be changed freely:\<close>
 
 lemma swap_disjunct_emb_step_at:
   assumes
     "length p \<le> length q \<Longrightarrow> take (length p) q \<noteq> p" "length q \<le> length p \<Longrightarrow>take (length q) p \<noteq> q"
   shows
     "emb_step_at q d2 (emb_step_at p d1 t) = emb_step_at p d1 (emb_step_at q d2 t)"
   using assms
 proof (induct "length p + length q" arbitrary:t p q rule:less_induct)
   case less
   then show ?case
   proof (cases "is_Hd t \<or> p = [] \<or> q = []")
     case True
     then show ?thesis
       using emb_step_at_is_App less.prems(1) less.prems(2) list.size(3) take_eq_Nil 
       by (metis le_zero_eq nat_le_linear)
   next
     case False
     then obtain t1 t2 p0 p' q0 q' where "t = App t1 t2" "p = p0 # p'" "q = q0 # q'"
       by (metis list.collapse tm.collapse(2))
     then show ?thesis 
       apply (cases p0; cases q0)
       using less.hyps less.prems(1) less.prems(2) by auto
   qed
 qed
 
 text \<open>An embedding step inside the branch that is removed in a second embedding step is useless. 
 For example, the embedding f (g b) ->emb f b ->emb f can achieved using a single step f (g b) ->emb f.\<close>
 
 lemma merge_emb_step_at:
   "emb_step_at p d1 (emb_step_at (p @ [opp d1] @ q) d2 t) = emb_step_at p d1 t"
 proof (induct p arbitrary:t)
   case Nil
   then show ?case by (cases t, simp, cases d1, simp_all)
 next
   case (Cons a p)
   then show ?case 
     apply (cases a) 
      apply (metis (full_types) emb_step_at_left_context append_Cons emb_step_at_is_App tm.collapse(2))
     by (metis (full_types) emb_step_at_right_context append_Cons emb_step_at_is_App tm.collapse(2))
 qed
 
 text \<open>When swapping two embedding steps of a position below another, one of the positions has to be
 slightly changed:\<close>
 
 lemma swap_nested_emb_step_at:
     "emb_step_at (p @ q) d2 (emb_step_at p d1 t) = emb_step_at p d1 (emb_step_at (p @ [d1] @ q) d2 t)"
 proof (induct p arbitrary:t)
   case Nil
   then show ?case by (cases t, simp, cases d1, simp_all)
 next
   case (Cons a p)
   then show ?case 
     apply (cases a;cases t) 
     using Cons.hyps Cons.prems by auto 
 qed
 
 subsection "Performing embedding steps in order of a given priority"
 
 text \<open>We want to perform all embedding steps first that modify the head or the number of arguments
 of a term. To this end we define the function prio\_emb\_step that performs the embedding step with
 the highest priority possible. The priority is given by a function "prio" from positions to nats, where 
 the lowest number has the highest priority.\<close>
 
 definition prio_emb_pos :: "(dir list \<Rightarrow> nat) \<Rightarrow> ('s,'v) tm \<Rightarrow> ('s,'v) tm \<Rightarrow> dir list" where
   "prio_emb_pos prio t s = (ARG_MIN prio p. p \<noteq> [] \<and> position_of t p \<and> emb_step_at' p t \<unrhd>\<^sub>e\<^sub>m\<^sub>b s)"
 
 definition prio_emb_step :: "(dir list \<Rightarrow> nat) \<Rightarrow> ('s,'v) tm \<Rightarrow> ('s,'v) tm \<Rightarrow> ('s,'v) tm" where
   "prio_emb_step prio t s = emb_step_at' (prio_emb_pos prio t s) t"
 
 lemma prio_emb_posI:
   "t \<unrhd>\<^sub>e\<^sub>m\<^sub>b s \<Longrightarrow> t \<noteq> s \<Longrightarrow> prio_emb_pos prio t s \<noteq> [] \<and> position_of t (prio_emb_pos prio t s) \<and> emb_step_at' (prio_emb_pos prio t s) t \<unrhd>\<^sub>e\<^sub>m\<^sub>b s"
 proof (induct rule:emb_induct_reverse)
   case (refl t)
   then show ?case by simp
 next
   case (step t u s)
   obtain p where 0:"p \<noteq> [] \<and> position_of t p \<and> emb_step_at' p t \<unrhd>\<^sub>e\<^sub>m\<^sub>b s"
     using emb_step_equiv' step.hyps(1) append_butlast_last_id position_if_emb_step_at
     by (metis step.hyps(2))
   then have "prio_emb_pos prio t s \<noteq> [] \<and> position_of t (prio_emb_pos prio t s) \<and> emb_step_at' (prio_emb_pos prio t s) t  \<unrhd>\<^sub>e\<^sub>m\<^sub>b s"
     using prio_emb_pos_def step.hyps(2) arg_min_natI by (metis (mono_tags, lifting))
   then show ?case by blast
 qed
 
 lemma prio_emb_pos_le:
   assumes "p \<noteq> []" "position_of t p" "emb_step_at' p t \<unrhd>\<^sub>e\<^sub>m\<^sub>b s"
   shows "prio (prio_emb_pos prio t s) \<le> prio p"
   by (simp add: arg_min_nat_le assms(1) assms(2) assms(3) prio_emb_pos_def)
 
 text \<open>We want an embedding step sequence in which the priority numbers monotonely increase. We can
 get such a sequence if the priority function assigns greater values to deeper positions.\<close>
 
 lemma prio_emb_pos_increase:
   assumes
     "t \<unrhd>\<^sub>e\<^sub>m\<^sub>b s" "t \<noteq> s" "prio_emb_step prio t s \<noteq> s" and
     valid_prio: "\<And>p q dp dq. prio (p @ [dp]) > prio (q @ [dq]) \<Longrightarrow> take (length p) q \<noteq> p" 
   shows
     "prio (prio_emb_pos prio t s) \<le> prio (prio_emb_pos prio (prio_emb_step prio t s) s)" 
     (is "prio ?p1 \<le> prio ?p2")
 proof (rule ccontr)
   assume contr: "\<not> prio ?p1 \<le> prio ?p2"
   have "take (length (butlast ?p1)) (butlast ?p2) \<noteq> (butlast ?p1)"
     using contr valid_prio
     by (metis append_butlast_last_id assms(1) assms(2) assms(3) not_le_imp_less prio_emb_posI prio_emb_step_def)
   then have butlast_neq: "butlast ?p2 \<noteq> butlast ?p1" 
     by auto
 
   define u where "u = prio_emb_step prio (prio_emb_step prio t s) s"
   then have "u \<unrhd>\<^sub>e\<^sub>m\<^sub>b s"
     by (metis assms(1) assms(2) assms(3) prio_emb_posI prio_emb_step_def)
 
   define p where "p = butlast ?p2"
   define q where "q = drop (Suc (length (butlast ?p2))) (butlast ?p1)"
   define dp where "dp = last ?p2"
   define dq where "dq = last ?p1"
   define f where "f = butlast ?p1 ! length (butlast ?p2)"
 
   have position: "position_of (prio_emb_step prio t s) ?p2" 
     by (metis assms(1) assms(2) assms(3) prio_emb_posI prio_emb_step_def)
 
   show False
   proof (cases "take (length p) (butlast ?p1) = p")
     case True
     have "length (butlast ?p1) \<noteq> length p" using butlast_neq 
       using True p_def by auto
     then have "length (butlast ?p1) > length p" 
       using nat_le_linear True nat_neq_iff by auto
     then have 0:"p @ f # q = butlast ?p1" 
       by (metis True f_def id_take_nth_drop p_def q_def)
     have u1: "u = emb_step_at p dp (emb_step_at (p @ f # q) dq t)"
       unfolding 0 unfolding p_def u_def dp_def dq_def prio_emb_step_def by simp
     show False
     proof (cases "f = dp")
       case True
       then have "u = emb_step_at (p @ q) dq (emb_step_at p dp t)"
         using swap_nested_emb_step_at[of p q dq dp t] u1 by simp
       then have "emb_step_at p dp t \<rightarrow>\<^sub>e\<^sub>m\<^sub>b u \<or> emb_step_at p dp t = u" 
         using emb_step_equiv[of "emb_step_at p dp t" u] by blast
       then have "emb_step_at p dp t \<unrhd>\<^sub>e\<^sub>m\<^sub>b s"
         using \<open>u \<unrhd>\<^sub>e\<^sub>m\<^sub>b s\<close> emb_prepend_step by blast
       then have "position_of t ?p2"
         by (metis position "0" position_of_Nil True append_Cons append_Nil2 append_butlast_last_id 
         append_eq_append_conv_if append_eq_conv_conj dp_def dq_def p_def pos_emb_step_at_nested prio_emb_step_def)
       then show ?thesis 
         using assms(1) assms(2) assms(3) contr dp_def p_def prio_emb_posI 
          prio_emb_pos_le prio_emb_step_def
         by (metis \<open>emb_step_at p dp t \<unrhd>\<^sub>e\<^sub>m\<^sub>b s\<close>)
     next
       case False
       then have "opp dp = f" 
         by (metis dir.exhaust opp_def)
       then have "u = emb_step_at p dp t" 
         by (subst merge_emb_step_at[of p dp q dq t, symmetric], simp add: u1)
       then have "position_of t ?p2"
         by (metis Cons_nth_drop_Suc position_of_Nil True dp_def 
             \<open>length p < length (butlast ?p1)\<close> \<open>opp dp = f\<close> append.assoc append_butlast_last_id 
             append_take_drop_id f_def list.sel(1) p_def pos_emb_step_at_opp position take_hd_drop prio_emb_step_def)
       then show ?thesis 
         by (metis dp_def p_def \<open>u = emb_step_at p dp t\<close> \<open>u \<unrhd>\<^sub>e\<^sub>m\<^sub>b s\<close> assms(1) assms(2) assms(3) contr 
          prio_emb_posI prio_emb_pos_le prio_emb_step_def)
     qed
   next
     case False
     define p' where "p' = butlast ?p1"
     have "take (length p') p \<noteq> p'" 
       using \<open>take (length (butlast ?p1)) (butlast ?p2) \<noteq> butlast ?p1\<close> p'_def p_def by blast
     have "take (length p) p' \<noteq> p" using False p'_def by metis
     have "u = emb_step_at p dp (emb_step_at p' dq t)" 
       unfolding u_def prio_emb_step_def 
       by (simp add: dp_def dq_def p'_def p_def prio_emb_step_def)
     then have "u = emb_step_at p' dq (emb_step_at p dp t)"
       using swap_disjunct_emb_step_at[of p p' dq dp t]
       by (simp add: \<open>take (length p') p \<noteq> p'\<close> \<open>take (length p) p' \<noteq> p\<close>)
     then have "emb_step_at p dp t \<unrhd>\<^sub>e\<^sub>m\<^sub>b s" 
       by (metis \<open>u \<unrhd>\<^sub>e\<^sub>m\<^sub>b s\<close> emb_prepend_step emb_step_equiv)
     have "position_of t (p @ [dp])" using pos_emb_step_at_disjunct
       by (metis \<open>take (length p') p \<noteq> p'\<close> \<open>take (length p) p' \<noteq> p\<close> append_butlast_last_id butlast.simps(1) 
       dp_def list.size(3) p'_def p_def position take_eq_Nil prio_emb_step_def)
     then show ?thesis 
       by (metis False \<open>emb_step_at p dp t \<unrhd>\<^sub>e\<^sub>m\<^sub>b s\<close> append_butlast_last_id butlast.simps(1) contr 
       dp_def list.size(3) p_def take_eq_Nil prio_emb_pos_le)
   qed
 qed
 
 lemma sequence_prio_emb_steps:
   assumes 
     "t \<unrhd>\<^sub>e\<^sub>m\<^sub>b s"
   shows
     "\<exists>us. us\<noteq>[] \<and> hd us = t \<and> last us = s \<and> 
     (\<forall>i. Suc i < length us \<longrightarrow> (prio_emb_step prio (us ! i) s = us ! Suc i \<and> us ! i \<rightarrow>\<^sub>e\<^sub>m\<^sub>b us ! Suc i))"
   using assms   
-proof (induct t rule:measure_induct_rule[of size])
+proof (induct t rule:measure_induct_rule[of hsize])
   case (less t)
   show ?case
   proof (cases "t = s")
     case True
     then show ?thesis by auto
   next
     case False
     then have "prio_emb_pos prio t s \<noteq> []" "emb_step_at' (prio_emb_pos prio t s) t \<unrhd>\<^sub>e\<^sub>m\<^sub>b s"
       using prio_emb_posI less by blast+
     have emb_step1:"t \<rightarrow>\<^sub>e\<^sub>m\<^sub>b emb_step_at' (prio_emb_pos prio t s) t"
       by (simp add: False emb_step_at_if_position less.prems prio_emb_posI)
-    have "size (emb_step_at' (prio_emb_pos prio t s) t) < size t"
-      by (simp add: False emb_step_at_if_position emb_step_size less.prems(1) prio_emb_posI)
+    have "hsize (emb_step_at' (prio_emb_pos prio t s) t) < hsize t"
+      by (simp add: False emb_step_at_if_position emb_step_hsize less.prems(1) prio_emb_posI)
     then obtain us where us_def:
       "us \<noteq> []" 
       "hd us = emb_step_at' (prio_emb_pos prio t s) t" 
       "last us = s" 
       "\<forall>i. Suc i < length us \<longrightarrow> prio_emb_step prio (us ! i) s = us ! Suc i \<and> us ! i \<rightarrow>\<^sub>e\<^sub>m\<^sub>b us ! Suc i"
-      using less(1)[of "emb_step_at' (prio_emb_pos prio t s) t"] emb_step_size 
+      using less(1)[of "emb_step_at' (prio_emb_pos prio t s) t"] emb_step_hsize 
         \<open>emb_step_at' (prio_emb_pos prio t s) t \<unrhd>\<^sub>e\<^sub>m\<^sub>b s\<close> by blast
 
     have "t # us \<noteq> []" " hd (t # us) = t" "last (t # us) = s" using us_def by simp_all
     have
       "\<forall>i. Suc i < length (t # us) \<longrightarrow> (prio_emb_step prio ((t # us) ! i) s = (t # us) ! Suc i \<and> (t # us) ! i \<rightarrow>\<^sub>e\<^sub>m\<^sub>b (t # us) ! Suc i)" 
     proof (rule allI, rule impI)
       fix i assume " Suc i < length (t # us)" 
       show "prio_emb_step prio ((t # us) ! i) s = (t # us) ! Suc i \<and> (t # us) ! i \<rightarrow>\<^sub>e\<^sub>m\<^sub>b (t # us) ! Suc i"
       proof (cases i)
         case 0
         show ?thesis 
           using "0" emb_step1 hd_conv_nth prio_emb_step_def us_def(1) us_def(2) by fastforce 
       next
         case (Suc nat)
         then show ?thesis 
           using \<open>Suc i < length (t # us)\<close> us_def(4) by auto
       qed 
     qed
     then show ?thesis
       using \<open>hd (t # us) = t\<close> \<open>last (t # us) = s\<close> by blast
   qed
 qed
 
 subsection "Embedding steps under arguments"
 
 text \<open>We want to perform positions that modify the head and the umber of arguments first. Formally these
 positions can be characterized as "list\_all (op = Left) p". We show here that embeddings at other positions
 do not modify the head, the number of arguments. Moreover, for each argument, the argument after the step
 is an embedding of the argument before the step. \<close>
 
 lemma emb_step_under_args_head:
   assumes
     "\<not> list_all (\<lambda>x. x = Left) p"
   shows
     "head (emb_step_at p d t) = head t"
   using assms  proof(induction p arbitrary:t)
   case Nil
   then show ?case 
     by simp
 next
   case (Cons a p)
   then show ?case 
   proof (cases t)
     case (Hd x)
     then show ?thesis
       by (metis emb_step_at_head)
   next
     case (App t1 t2)
     then show ?thesis 
     proof (cases a)
       case Left
       then show ?thesis using Cons 
         by (simp add: App)
     next
       case Right
       then show ?thesis
         by (metis App emb_step_at_right_context head_App)
     qed
   qed
 qed
 
 lemma emb_step_under_args_num_args:
   assumes
     "\<not> list_all (\<lambda>x. x = Left) p"
   shows
     "num_args (emb_step_at p d t) = num_args t"
   using assms 
 proof(induction p arbitrary:t)
   case Nil
   then show ?case 
     using list_all_simps(2) by blast
 next
   case (Cons a p)
   then show ?case 
   proof (cases t)
     case (Hd x1)
     then show ?thesis
       by (metis emb_step_at_head)
   next
     case (App t1 t2)
     then show ?thesis unfolding App apply (cases a)
       using App Cons.IH Cons.prems(1) by auto
   qed
 qed
 
 lemma emb_step_under_args_emb_step:
   assumes
    "\<not> list_all (\<lambda>x. x = Left) p"
    "position_of t (p @ [d])"
  obtains i where
    "i < num_args t"
    "args t ! i \<rightarrow>\<^sub>e\<^sub>m\<^sub>b args (emb_step_at p d t) ! i" and
    "\<And>j. j < num_args t \<Longrightarrow> i \<noteq> j \<Longrightarrow> args t ! j = args (emb_step_at p d t) ! j"
   using assms 
 proof(induction p arbitrary:t thesis)
   case Nil
   then show ?case 
     by simp  
 next
   case (Cons a p)
   obtain t1 t2 where App:"t = App t1 t2"
     by (metis Cons.prems(3) emb_step_at_if_position emb_step_at_is_App emb_step_equiv' tm.collapse(2))
   then show ?case
   proof (cases a)
     case Left
     have IH_cond1: "\<not> list_all (\<lambda>x. x = dir.Left) p" 
       using Cons.prems(2) Left by auto
     have IH_cond2: "position_of t1 (p @ [d])" 
       using App Cons.prems(3) Left by auto
     obtain i' where i'_def: 
       "i' < num_args t1"
       "args t1 ! i' \<rightarrow>\<^sub>e\<^sub>m\<^sub>b args (emb_step_at p d t1) ! i'"
       "\<And>j. j < num_args t1 \<Longrightarrow> i' \<noteq> j \<Longrightarrow> args t1 ! j = args (emb_step_at p d t1) ! j"
       using Cons.IH[OF _ IH_cond1 IH_cond2] by blast
     have num_args:"num_args (emb_step_at p d t1) = num_args t1"
       using App Cons.prems(1) Left emb_step_under_args_num_args
       by (simp add: emb_step_under_args_num_args IH_cond1)
     have 1:"i' < num_args t" 
       by (simp add: App i'_def(1) less_SucI)
     have 2:"args t ! i' \<rightarrow>\<^sub>e\<^sub>m\<^sub>b args (emb_step_at (a # p) d t) ! i'" 
       by (simp add: App Left i'_def(1) i'_def(2) nth_append num_args)
     have 3:"\<And>j. j < num_args t \<Longrightarrow> i' \<noteq> j \<Longrightarrow> args t ! j = args (emb_step_at (a # p) d t) ! j"
       by (simp add: App Left i'_def(3) nth_append num_args)
     show ?thesis using Cons.prems(1)[OF 1 2 3] by blast
   next
     case Right
     have 0:"\<And>j. j < num_args t \<Longrightarrow> num_args t - 1 \<noteq> j \<Longrightarrow> args t ! j = args (emb_step_at (a # p) d t) ! j"
       by (metis (no_types, lifting) App Cons.prems(2) emb_step_at_right_context Nitpick.size_list_simp(2) Right args.simps(2) butlast_snoc emb_step_under_args_num_args length_butlast length_tl less_antisym nth_butlast)
     show ?thesis 
       using Cons.prems(1)[of "num_args t - 1"]
       using App Cons.prems(3) Right emb_step_at_if_position 0 by auto
   qed
 qed
 
 lemma emb_step_under_args_emb:
   assumes "\<not> list_all (\<lambda>x. x = Left) p"
    "position_of t (p @ [d])"
   shows
     "\<forall>i. i < num_args t \<longrightarrow> args t ! i \<unrhd>\<^sub>e\<^sub>m\<^sub>b args (emb_step_at p d t) ! i"
   by (metis assms emb.simps emb_step_under_args_emb_step)
 
 lemma position_Left_only_subst:
   assumes "list_all (\<lambda>x. x = Left) p" 
     and "position_of (subst \<rho> w) (p @ [d])"
     and "num_args (subst \<rho> w)  = num_args w"
   shows "position_of w (p @ [d])"
   using assms proof (induct p arbitrary:w)
   case Nil
   then show ?case 
     by (metis position_of_Hd position_of_Nil Hd_head_id append_self_conv2 args.simps(1) length_0_conv list.sel(3) position_of.elims(3))
 next
   case (Cons a p)
   then show ?case 
   proof (cases w)
     case (Hd x)
     then show ?thesis 
       by (metis Cons.prems(2) Cons.prems(3) position_of_Hd Hd_head_id append_Cons args.simps(1) list.size(3))
   next
     case (App w1 w2)
     have "num_args (subst \<rho> w1) = num_args w1" 
       using App Cons.prems(3) by auto
     then show ?thesis
       by (metis (full_types) App Cons.hyps Cons.prems(1) Cons.prems(2) position_of_left 
           append_Cons list.pred_inject(2) subst.simps(2))
   qed 
 qed
 
 subsection \<open>Rearranging embedding steps: first above, then below arguments\<close>
 
 lemma perform_emb_above_vars0:
   assumes 
     "subst \<rho> s \<unrhd>\<^sub>e\<^sub>m\<^sub>b u"
   obtains w where
     "s \<unrhd>\<^sub>e\<^sub>m\<^sub>b w"
     "subst \<rho> w \<unrhd>\<^sub>e\<^sub>m\<^sub>b u"
     "\<forall>w'. w \<rightarrow>\<^sub>e\<^sub>m\<^sub>b w' \<longrightarrow> \<not> subst \<rho> w' \<unrhd>\<^sub>e\<^sub>m\<^sub>b u"
   using assms   
-proof (induct s rule:measure_induct_rule[of size])
+proof (induct s rule:measure_induct_rule[of hsize])
   case (less s)
   show ?case
   proof (cases "\<forall>w'. s \<rightarrow>\<^sub>e\<^sub>m\<^sub>b w' \<longrightarrow> \<not> subst \<rho> w' \<unrhd>\<^sub>e\<^sub>m\<^sub>b u")
     case True
     then show ?thesis  
       using emb.refl less.prems(1)
       using less.prems(2) by blast
   next
     case False
     then show ?thesis 
-      by (meson emb_step_is_emb emb_step_size emb_trans less.hyps less.prems(1))
+      by (meson emb_step_is_emb emb_step_hsize emb_trans less.hyps less.prems(1))
   qed
 qed
   
 lemma emb_only_below_vars:
   assumes 
     "subst \<rho> s \<unrhd>\<^sub>e\<^sub>m\<^sub>b u"
     "s \<unrhd>\<^sub>e\<^sub>m\<^sub>b w"
     "is_Sym (head w)"
     "subst \<rho> w \<unrhd>\<^sub>e\<^sub>m\<^sub>b u"
     "\<forall>w'. w \<rightarrow>\<^sub>e\<^sub>m\<^sub>b w' \<longrightarrow> \<not> subst \<rho> w' \<unrhd>\<^sub>e\<^sub>m\<^sub>b u"
   obtains ws where
     "ws \<noteq> []"
     "hd ws = subst \<rho> w"
     "last ws = u"
     "\<forall>i. Suc i < length ws \<longrightarrow> 
       (\<exists>p d. emb_step_at p d (ws ! i) = ws ! Suc i \<and> \<not> list_all (\<lambda>x. x = Left) p)"
     "\<forall>i. i < length ws \<longrightarrow> head (ws ! i) = head w \<and> num_args (ws ! i) = num_args w"
     "\<forall>i. i < length ws \<longrightarrow> (\<forall>k. k < num_args w \<longrightarrow> args (subst \<rho> w) ! k \<unrhd>\<^sub>e\<^sub>m\<^sub>b args (ws ! i) ! k)"
 proof -
   define prio :: "dir list \<Rightarrow> nat" where "prio = (\<lambda>p. if list_all (\<lambda>x. x = Left) (butlast p) then 0 else 1)"
   obtain ws where ws_def:
     "ws \<noteq> []"
     "hd ws = subst \<rho> w"
     "last ws = u"
     "\<forall>i. Suc i < length ws \<longrightarrow> prio_emb_step prio (ws ! i) u = ws ! Suc i \<and> ws ! i \<rightarrow>\<^sub>e\<^sub>m\<^sub>b ws ! Suc i"
     using \<open>subst \<rho> w \<unrhd>\<^sub>e\<^sub>m\<^sub>b u\<close> sequence_prio_emb_steps by blast
 
   have ws_emb_u:"\<forall>i. Suc i < length ws \<longrightarrow> ws ! i \<noteq> u \<and> ws ! i \<unrhd>\<^sub>e\<^sub>m\<^sub>b u"
   proof (rule allI)
     {
       fix j assume "Suc j < length ws"
       then have "ws ! (length ws - (Suc (Suc j))) \<noteq> u  \<and> ws ! (length ws - (Suc (Suc j))) \<unrhd>\<^sub>e\<^sub>m\<^sub>b u"
       proof (induction j)
         case 0
         have "prio_emb_step prio (ws ! (length ws - Suc (Suc 0))) u = ws ! (length ws - (Suc 0))"
           using "0.prems" Suc_diff_Suc ws_def(4) by auto
         then show ?case 
           using "0.prems" One_nat_def Suc_diff_Suc Suc_lessD diff_Suc_less emb_step_equiv last_conv_nth ws_def(1) ws_def(3) ws_def(4)
           by (metis emb_step_is_emb)
       next
         case (Suc j)
         then have "ws ! (length ws - (Suc (Suc (Suc j)))) \<rightarrow>\<^sub>e\<^sub>m\<^sub>b ws ! (length ws - Suc (Suc j))"
           by (metis Suc_diff_Suc diff_Suc_less length_greater_0_conv ws_def(1) ws_def(4))
-        then show ?case using emb_size_neq
-          by (metis Suc.IH Suc.prems Suc_lessD emb_size emb_step_is_emb emb_trans leD)
+        then show ?case using emb_hsize_neq
+          by (metis Suc.IH Suc.prems Suc_lessD emb_hsize emb_step_is_emb emb_trans leD)
       qed 
     }
     note 0 = this
     fix i
     show "Suc i < length ws \<longrightarrow> ws ! i \<noteq> u \<and> ws ! i \<unrhd>\<^sub>e\<^sub>m\<^sub>b u" using 0[of "length ws - Suc (Suc i)"]
       using Suc_diff_Suc ws_def(1) by auto
   qed
 
   { 
     fix i
     assume "i < length ws"
     then have "head (ws ! i) = head w 
              \<and> num_args (ws ! i) = num_args w
              \<and> (\<forall>k. k < num_args w \<longrightarrow> args (subst \<rho> w) ! k \<unrhd>\<^sub>e\<^sub>m\<^sub>b args (ws ! i) ! k)
              \<and> (Suc i < length ws \<longrightarrow> prio (prio_emb_pos prio (ws ! i) u) = 1)"
     proof (induct i)
       case 0
       have 1:"head (ws ! 0) = head w"
         by (metis assms(3) ground_imp_subst_iden hd.collapse(2) hd.simps(18) hd_conv_nth head_subst tm.sel(1) tm.simps(17) ws_def(1) ws_def(2))
       have 2:"num_args (ws ! 0) = num_args w"
         by (metis (no_types, lifting) append_self_conv2 args_subst assms(3) hd.case_eq_if hd_conv_nth length_map ws_def(1) ws_def(2))
       have 3:"\<forall>k. k < num_args w \<longrightarrow> args (subst \<rho> w) ! k \<unrhd>\<^sub>e\<^sub>m\<^sub>b args (ws ! 0) ! k"
         using emb.refl hd_conv_nth ws_def(1) ws_def(2) by fastforce
       have 4:"(Suc 0 < length ws \<longrightarrow> prio (prio_emb_pos prio (ws ! 0) u) = 1)"
         by (metis \<open>num_args (ws ! 0) = num_args w\<close> prio_def append_butlast_last_id assms(5) emb_step_at_if_position 
         emb_step_at_subst hd_conv_nth position_Left_only_subst prio_emb_posI ws_def(1) ws_def(2) ws_emb_u)
       show ?case using 1 2 3 4 by blast
     next
       case (Suc i)
       then have ih: 
         "prio (prio_emb_pos prio (ws ! i) u) = 1" 
         "head (ws ! i) = head w" 
         "num_args (ws ! i) = num_args w" by simp_all
       have 1:"head (ws ! Suc i) = head w"
         by (metis Suc.prems prio_def emb_step_under_args_head ih(1) ih(2) prio_emb_step_def ws_def(4) zero_neq_one)
       have 2:"num_args (ws ! Suc i) = num_args w"
         by (metis Suc.prems emb_step_under_args_num_args ih(1) ih(3) prio_def prio_emb_step_def ws_def(4) zero_neq_one)
       have "\<forall>k<num_args (ws ! i). args (ws ! i) ! k \<unrhd>\<^sub>e\<^sub>m\<^sub>b args (ws ! Suc i) ! k" 
         using Suc.prems emb_step_under_args_emb ih(1) prio_def prio_emb_step_def ws_def(4) zero_neq_one 
         by (metis (no_types, lifting) append_butlast_last_id prio_emb_posI ws_emb_u)
       then have 3:"\<forall>k. k < num_args w \<longrightarrow> args (subst \<rho> w) ! k \<unrhd>\<^sub>e\<^sub>m\<^sub>b args (ws ! Suc i) ! k"
         using Suc.hyps Suc.prems emb_trans by force
       have "\<And>p q dp dq. prio (q @ [dq]) < prio (p @ [dp]) \<Longrightarrow> take (length p) q \<noteq> p" unfolding prio_def
         using append_take_drop_id list_all_append 
         by (metis (mono_tags, lifting) butlast_snoc gr_implies_not0 less_not_refl2)
       then have 4:"Suc (Suc i) < length ws \<longrightarrow> prio (prio_emb_pos prio (ws ! Suc i) u) = 1"
         by (metis Suc.prems ih(1) not_one_le_zero prio_def prio_emb_pos_increase ws_def(4) ws_emb_u)
       then show ?case using 1 2 3 4 by auto
     qed
   }
   note 1 = this
 
   have "\<forall>i. Suc i < length ws \<longrightarrow> 
       (\<exists>p d. emb_step_at p d (ws ! i) = ws ! Suc i \<and> \<not> list_all (\<lambda>x. x = Left) p)" 
     by (metis "1" Suc_lessD prio_def prio_emb_step_def ws_def(4) zero_neq_one)
 
   then show ?thesis
     using that ws_def(1) ws_def(2) ws_def(3)
     using "1" by blast
 qed
 
 lemma perform_emb_above_vars:
   assumes 
     "subst \<rho> s \<unrhd>\<^sub>e\<^sub>m\<^sub>b u"
   obtains w where
     "s \<unrhd>\<^sub>e\<^sub>m\<^sub>b w"
     "subst \<rho> w \<unrhd>\<^sub>e\<^sub>m\<^sub>b u"
     "is_Sym (head w) \<Longrightarrow> head w = head u \<and> num_args w = num_args u \<and> (\<forall>k. k<num_args w \<longrightarrow> args (subst \<rho> w) ! k \<unrhd>\<^sub>e\<^sub>m\<^sub>b args u ! k)"
 proof -
   obtain w where w_def:
     "s \<unrhd>\<^sub>e\<^sub>m\<^sub>b w" 
     "subst \<rho> w \<unrhd>\<^sub>e\<^sub>m\<^sub>b u" 
     "\<forall>w'. w \<rightarrow>\<^sub>e\<^sub>m\<^sub>b w' \<longrightarrow> \<not> subst \<rho> w' \<unrhd>\<^sub>e\<^sub>m\<^sub>b u" 
     using perform_emb_above_vars0[OF \<open>subst \<rho> s \<unrhd>\<^sub>e\<^sub>m\<^sub>b u\<close>] by metis
   {
     assume "is_Sym (head w)"
     obtain ws where ws_def:
       "ws \<noteq> []" 
       "hd ws = subst \<rho> w" 
       "last ws = u" 
       "\<forall>i. Suc i < length ws \<longrightarrow> (\<exists>p d. emb_step_at p d (ws ! i) = ws ! Suc i \<and> \<not> list_all (\<lambda>x. x = Left) p)"
       "\<forall>i<length ws. head (ws ! i) = head w \<and> num_args (ws ! i) = num_args w"
       "\<forall>i<length ws. \<forall>k<num_args w. args (subst \<rho> w) ! k \<unrhd>\<^sub>e\<^sub>m\<^sub>b args (ws ! i) ! k"
       using emb_only_below_vars[OF \<open>subst \<rho> s \<unrhd>\<^sub>e\<^sub>m\<^sub>b u\<close> \<open>s \<unrhd>\<^sub>e\<^sub>m\<^sub>b w\<close> \<open>is_Sym (head w)\<close> \<open>subst \<rho> w \<unrhd>\<^sub>e\<^sub>m\<^sub>b u\<close> w_def(3)] by metis
     then have "head w = head u \<and> num_args w = num_args u \<and> (\<forall>k. k<num_args w \<longrightarrow> args (subst \<rho> w) ! k \<unrhd>\<^sub>e\<^sub>m\<^sub>b args u ! k)"
       by (metis One_nat_def append_butlast_last_id diff_Suc_1 diff_Suc_less length_append_singleton length_greater_0_conv nth_append_length)
 
   }
   then show ?thesis 
     using that w_def(1) w_def(2) by blast
 qed
 
 
 end
\ No newline at end of file
diff --git a/thys/Lambda_Free_EPO/Lambda_Free_EPO.thy b/thys/Lambda_Free_EPO/Lambda_Free_EPO.thy
--- a/thys/Lambda_Free_EPO/Lambda_Free_EPO.thy
+++ b/thys/Lambda_Free_EPO/Lambda_Free_EPO.thy
@@ -1,1247 +1,1247 @@
 (*  Title:       The Embedding Path Order for Lambda-Free Higher-Order Terms
     Author:      Alexander Bentkamp <a.bentkamp at vu.nl>, 2018
     Maintainer:  Alexander Bentkamp <a.bentkamp at vu.nl>
 *)
 
 section \<open>The Embedding Path Order for Lambda-Free Higher-Order Terms\<close>
 
 theory Lambda_Free_EPO
 imports Chop
 abbrevs ">t" = ">\<^sub>t"
   and "\<ge>t" = "\<ge>\<^sub>t"
 begin
 
 text \<open>
 This theory defines the embedding path order for \<open>\<lambda>\<close>-free
 higher-order terms.
 \<close>
 
 subsection \<open>Setup\<close>
 
 locale epo = ground_heads "(>\<^sub>s)" arity_sym arity_var
     for
       gt_sym :: "'s \<Rightarrow> 's \<Rightarrow> bool" (infix ">\<^sub>s" 50) and
       arity_sym :: "'s \<Rightarrow> enat" and
       arity_var :: "'v \<Rightarrow> enat" +
   fixes
     extf :: "'s \<Rightarrow> (('s, 'v) tm \<Rightarrow> ('s, 'v) tm \<Rightarrow> bool) \<Rightarrow> ('s, 'v) tm list \<Rightarrow> ('s, 'v) tm list \<Rightarrow> bool"
   assumes
     extf_ext_trans_before_irrefl: "ext_trans_before_irrefl (extf f)" and
     extf_ext_compat_list: "ext_compat_list (extf f)"
   assumes extf_ext_compat_snoc: "ext_compat_snoc (extf f)"
   assumes extf_ext_compat_cons: "ext_compat_cons (extf f)"
   assumes extf_ext_snoc: "ext_snoc (extf f)"
   assumes extf_min_empty: "\<not> extf f gt [] ss" (* TODO: seperate definition? *)
 begin
 
 lemma extf_ext_trans: "ext_trans (extf f)"
   by (rule ext_trans_before_irrefl.axioms(1)[OF extf_ext_trans_before_irrefl])
 
 lemma extf_ext: "ext (extf f)"
   by (rule ext_trans.axioms(1)[OF extf_ext_trans])
 
 lemmas extf_mono_strong = ext.mono_strong[OF extf_ext]
 lemmas extf_mono = ext.mono[OF extf_ext, mono]
 lemmas extf_map = ext.map[OF extf_ext]
 lemmas extf_trans = ext_trans.trans[OF extf_ext_trans]
 lemmas extf_irrefl_from_trans =
   ext_trans_before_irrefl.irrefl_from_trans[OF extf_ext_trans_before_irrefl]
 lemmas extf_compat_list = ext_compat_list.compat_list[OF extf_ext_compat_list]
 
 lemmas extf_snoc = ext_snoc.snoc[OF extf_ext_snoc]
 
 lemmas extf_compat_append_right = ext_compat_snoc.compat_append_right[OF extf_ext_compat_snoc]
 lemmas extf_compat_append_left = ext_compat_cons.compat_append_left[OF extf_ext_compat_cons]
 
 lemma extf_ext_insert_arg: "extf f gt (xs @ z # ys) (xs @ ys)" 
   using extf_compat_append_left extf_compat_append_right extf_snoc[of f gt Nil z] 
   by fastforce
 
 subsection \<open>Inductive Definitions\<close>
 
 definition
   chkchop :: "(('s, 'v) tm \<Rightarrow> ('s, 'v) tm \<Rightarrow> bool) \<Rightarrow> ('s, 'v) tm \<Rightarrow> ('s, 'v) tm \<Rightarrow> bool"
 where
   [simp]: "chkchop gt t s \<longleftrightarrow> is_Hd s \<or> gt t (chop s)"
 
 definition
   chkchop_same :: "(('s, 'v) tm \<Rightarrow> ('s, 'v) tm \<Rightarrow> bool) \<Rightarrow> ('s, 'v) tm \<Rightarrow> ('s, 'v) tm \<Rightarrow> bool"
 where
   [simp]: "chkchop_same gt t s \<longleftrightarrow> 
             (if is_Var (head t) 
             then is_Hd t \<or> chkchop gt (chop t) s 
             else chkchop gt t s)"
 
 lemma chkchop_mono[mono]: "gt \<le> gt' \<Longrightarrow> chkchop gt \<le> chkchop gt'"
   using chkchop_def by blast
 
 lemma chkchop_same_mono[mono]: "gt \<le> gt' \<Longrightarrow> chkchop_same gt \<le> chkchop_same gt'"
   using chkchop_same_def by fastforce
 
 inductive gt :: "('s, 'v) tm \<Rightarrow> ('s, 'v) tm \<Rightarrow> bool" (infix ">\<^sub>t" 50) where
   gt_chop: "is_App t \<Longrightarrow> chop t >\<^sub>t s \<or> chop t = s \<Longrightarrow> t >\<^sub>t s"
 | gt_diff: "head t >\<^sub>h\<^sub>d head s \<Longrightarrow> is_Sym (head s) \<Longrightarrow> chkchop (>\<^sub>t) t s \<Longrightarrow> t >\<^sub>t s"
 | gt_same: "head t = head s \<Longrightarrow> chkchop_same (>\<^sub>t) t s \<Longrightarrow>
     (\<forall>f \<in> ground_heads (head t). extf f (>\<^sub>t) (args t) (args s)) \<Longrightarrow> t >\<^sub>t s"
 
 abbreviation ge :: "('s, 'v) tm \<Rightarrow> ('s, 'v) tm \<Rightarrow> bool" (infix "\<ge>\<^sub>t" 50) where
   "t \<ge>\<^sub>t s \<equiv> t >\<^sub>t s \<or> t = s"
 
 inductive gt_chop :: "('s, 'v) tm \<Rightarrow> ('s, 'v) tm \<Rightarrow> bool" where
   gt_chopI: "is_App t \<Longrightarrow> chop t \<ge>\<^sub>t s \<Longrightarrow> gt_chop t s"
 
 inductive gt_diff :: "('s, 'v) tm \<Rightarrow> ('s, 'v) tm \<Rightarrow> bool" where
   gt_diffI: "head t >\<^sub>h\<^sub>d head s \<Longrightarrow> is_Sym (head s) \<Longrightarrow> chkchop (>\<^sub>t) t s \<Longrightarrow> gt_diff t s"
 
 inductive gt_same :: "('s, 'v) tm \<Rightarrow> ('s, 'v) tm \<Rightarrow> bool" where
   gt_sameI: "head t = head s \<Longrightarrow> chkchop_same (>\<^sub>t) t s \<Longrightarrow>
     (\<forall>f \<in> ground_heads (head t). extf f (>\<^sub>t) (args t) (args s)) \<Longrightarrow> gt_same t s"
 
 lemma gt_iff_chop_diff_same: "t >\<^sub>t s \<longleftrightarrow> gt_chop t s \<or> gt_diff t s \<or> gt_same t s"
   by (subst gt.simps) (auto simp: gt_chop.simps gt_diff.simps gt_same.simps)
 
 subsection \<open>Transitivity\<close>
 
 lemma t_gt_chop_t: "is_App t \<Longrightarrow> t >\<^sub>t chop t"
   by (simp add: gt_chop)
 
 lemma gt_imp_vars: "t >\<^sub>t s \<Longrightarrow> vars t \<supseteq> vars s"
 proof (simp only: atomize_imp,
-    rule measure_induct_rule[of "\<lambda>(t, s). size t + size s"
+    rule measure_induct_rule[of "\<lambda>(t, s). hsize t + hsize s"
       "\<lambda>(t, s). t >\<^sub>t s \<longrightarrow> vars t \<supseteq> vars s" "(t, s)", simplified prod.case],
     simp only: split_paired_all prod.case atomize_imp[symmetric])
   fix t s
   assume
-    ih: "\<And>ta sa. size ta + size sa < size t + size s \<Longrightarrow> ta >\<^sub>t sa \<Longrightarrow> vars ta \<supseteq> vars sa" and
+    ih: "\<And>ta sa. hsize ta + hsize sa < hsize t + hsize s \<Longrightarrow> ta >\<^sub>t sa \<Longrightarrow> vars ta \<supseteq> vars sa" and
     t_gt_s: "t >\<^sub>t s"
   show "vars t \<supseteq> vars s"
     using t_gt_s
   proof cases
     case (gt_chop)
     thus ?thesis
       using ih
-      by (metis add_mono_thms_linordered_field(1) le_supI1 order_refl size_chop_lt vars_chop)
+      by (metis add_mono_thms_linordered_field(1) le_supI1 order_refl hsize_chop_lt vars_chop)
   next
     case gt_diff
     show ?thesis 
     proof (cases s)
       case Hd
       thus ?thesis
         using gt_diff(2) 
         by (metis empty_iff hd.collapse(2) hd.simps(18) subsetI tm.sel(1) tm.simps(17))
     next
       case (App s1 s2)
       have "vars (chop s) \<subseteq> vars t" using ih 
-        using App chkchop_def local.gt_diff(3) nat_add_left_cancel_less size_chop_lt tm.disc(2) by blast
+        using App chkchop_def local.gt_diff(3) nat_add_left_cancel_less hsize_chop_lt tm.disc(2) by blast
       thus ?thesis 
         using  App  le_sup_iff local.gt_diff(2) tm.disc(2) vars_chop
         by (metis empty_iff hd.collapse(2) hd.simps(18) subsetI)
     qed
   next
     case gt_same
     thus ?thesis
     proof (cases "head t")
       case (Var x)
       then show ?thesis 
       proof (cases t)
         case (Hd _)
         then show ?thesis using gt_same extf_min_empty[of _ "(>\<^sub>t)" "args s"]
           by simp
       next
         case (App t1 t2)
         then show ?thesis
         proof (cases s)
           case (Hd _)
           then show ?thesis 
             using local.gt_same(1) vars_head_subseteq by fastforce
         next
           case (App s1 s2)
           then have "chop t >\<^sub>t chop s" 
             by (metis Var args.simps(1) chkchop_def chkchop_same_def epo.extf_min_empty 
                 epo_axioms gt_hd_def gt_hd_irrefl hd.disc(1) local.gt_same(2) local.gt_same(3) tm.collapse(1) tm.disc(2))
           then have "vars (chop s) \<subseteq> vars (chop t)" using ih[OF _ \<open>chop t >\<^sub>t chop s\<close>] 
-            by (metis App add_mono_thms_linordered_field(5) args_Nil_iff_is_Hd extf_min_empty gt_hd_def gt_hd_irrefl local.gt_same(3) size_chop_lt tm.disc(2))
+            by (metis App add_mono_thms_linordered_field(5) args_Nil_iff_is_Hd extf_min_empty gt_hd_def gt_hd_irrefl local.gt_same(3) hsize_chop_lt tm.disc(2))
           then show ?thesis using  gt_same(1) vars_chop[of t] vars_chop[of s]
             by (metis App args_Nil_iff_is_Hd extf_min_empty gt_hd_def gt_hd_irrefl le_sup_iff local.gt_same(3) order_refl sup.coboundedI1 tm.disc(2))
         qed
       qed
     next
       case (Sym f)
       then have "chkchop (>\<^sub>t) t s" using gt_same chkchop_same_def by auto
       then show ?thesis 
       proof (cases s)
         case (Hd _)
         then show ?thesis using local.gt_same(1) vars_head_subseteq by force 
       next
         case (App s1 s2)
         then show ?thesis unfolding chkchop_def using vars_chop ih[of t "chop s"] 
           by (metis \<open>chkchop (>\<^sub>t) t s\<close> chkchop_def le_sup_iff local.gt_same(1) 
-              nat_add_left_cancel_less size_chop_lt tm.disc(2) vars_head_subseteq)
+              nat_add_left_cancel_less hsize_chop_lt tm.disc(2) vars_head_subseteq)
       qed
     qed
   qed      
 qed  
 
 lemma gt_trans: "u >\<^sub>t t \<Longrightarrow> t >\<^sub>t s \<Longrightarrow> u >\<^sub>t s"
 proof (simp only: atomize_imp,
-    rule measure_induct_rule[of "\<lambda>(u, t, s). {#size u, size t, size s#}"
+    rule measure_induct_rule[of "\<lambda>(u, t, s). {#hsize u, hsize t, hsize s#}"
         "\<lambda>(u, t, s). u >\<^sub>t t \<longrightarrow> t >\<^sub>t s \<longrightarrow> u >\<^sub>t s" "(u, t, s)",
       simplified prod.case],
     simp only: split_paired_all prod.case atomize_imp[symmetric])
   fix u t s
   assume
-    ih: "\<And>ua ta sa. {#size ua, size ta, size sa#} < {#size u, size t, size s#} \<Longrightarrow>
+    ih: "\<And>ua ta sa. {#hsize ua, hsize ta, hsize sa#} < {#hsize u, hsize t, hsize s#} \<Longrightarrow>
       ua >\<^sub>t ta \<Longrightarrow> ta >\<^sub>t sa \<Longrightarrow> ua >\<^sub>t sa" and
     u_gt_t: "u >\<^sub>t t" and t_gt_s: "t >\<^sub>t s"
 
   have u_gt_s_if_ui: "chop u \<ge>\<^sub>t t \<Longrightarrow> u >\<^sub>t s" if ui_in: "is_App u"
-    using ih[of "chop u" t s, simplified] t_gt_s gt_chop size_chop_lt ui_in by blast
+    using ih[of "chop u" t s, simplified] t_gt_s gt_chop hsize_chop_lt ui_in by blast
 
   show "u >\<^sub>t s"
     using t_gt_s
   proof cases
     case gt_chop
     have u_gt_s_if_chk_u_t: ?thesis if chk_u_t: "chkchop (>\<^sub>t) u t"
       using ih[of u "chop u" s] gt_chop chk_u_t 
-      by (metis add_mset_lt_left_lt add_mset_lt_right_lt chkchop_def ih size_chop_lt)
+      by (metis add_mset_lt_left_lt add_mset_lt_right_lt chkchop_def ih hsize_chop_lt)
     show ?thesis 
       by (metis args_Nil_iff_is_Hd chkchop_def chkchop_same_def 
           epo.extf_min_empty epo_axioms gt.simps gt_hd_def gt_hd_irrefl
           u_gt_s_if_chk_u_t u_gt_s_if_ui u_gt_t)
   next
     case gt_diff_t_s: gt_diff
     show ?thesis
       using u_gt_t
     proof cases
       case gt_chop
       then show ?thesis 
         using u_gt_s_if_ui by blast
     next
       case gt_diff_u_t: gt_diff
       have "head u >\<^sub>h\<^sub>d head s"
         using gt_diff_u_t(1) gt_diff_t_s(1) by (auto intro: gt_hd_trans)
       thus ?thesis
-        using add_mset_lt_left_lt add_mset_lt_right_lt chkchop_def  gt_diff gt_diff_t_s(3) ih size_chop_lt u_gt_t
+        using add_mset_lt_left_lt add_mset_lt_right_lt chkchop_def  gt_diff gt_diff_t_s(3) ih hsize_chop_lt u_gt_t
         by (metis gt_diff_t_s(2))
     next
       case gt_same_u_t: gt_same
       have "head u >\<^sub>h\<^sub>d head s"
         using gt_diff_t_s(1) gt_same_u_t(1) by auto
       thus ?thesis
-        using add_mset_lt_left_lt add_mset_lt_right_lt chkchop_def gt_diff gt_diff_t_s(3) ih size_chop_lt u_gt_t
+        using add_mset_lt_left_lt add_mset_lt_right_lt chkchop_def gt_diff gt_diff_t_s(3) ih hsize_chop_lt u_gt_t
         by (metis gt_diff_t_s(2))
     qed
   next
     case gt_same_t_s: gt_same
     show ?thesis
       using u_gt_t
     proof cases
       case gt_chop
       then show ?thesis 
         using u_gt_s_if_ui by linarith
     next
       case gt_diff_u_t: gt_diff
       have "head u >\<^sub>h\<^sub>d head s"
         using gt_diff_u_t(1) gt_same_t_s(1) by simp
       thus ?thesis
-        using add_mset_lt_left_lt add_mset_lt_right_lt chkchop_def gt_diff gt_same_t_s ih size_chop_lt u_gt_t
+        using add_mset_lt_left_lt add_mset_lt_right_lt chkchop_def gt_diff gt_same_t_s ih hsize_chop_lt u_gt_t
         by (metis chkchop_same_def gt_diff_u_t(2))
     next
       case gt_same_u_t: gt_same
       have hd_u_s: "head u = head s"
         using gt_same_u_t(1) gt_same_t_s(1) by simp
 
       let ?S = "set (args u) \<union> set (args t) \<union> set (args s)"
 
       have gt_trans_args: "\<forall>ua \<in> ?S. \<forall>ta \<in> ?S. \<forall>sa \<in> ?S. ua >\<^sub>t ta \<longrightarrow> ta >\<^sub>t sa \<longrightarrow> ua >\<^sub>t sa"
       proof clarify
         fix sa ta ua
         assume
           ua_in: "ua \<in> ?S" and ta_in: "ta \<in> ?S" and sa_in: "sa \<in> ?S" and
           ua_gt_ta: "ua >\<^sub>t ta" and ta_gt_sa: "ta >\<^sub>t sa"
         show "ua >\<^sub>t sa"
           by (auto intro!: ih[OF Max_lt_imp_lt_mset ua_gt_ta ta_gt_sa])
             (meson ua_in ta_in sa_in Un_iff max.strict_coboundedI1 max.strict_coboundedI2
-               size_in_args)+
+               hsize_in_args)+
       qed
 
       have "\<forall>f \<in> ground_heads (head u). extf f (>\<^sub>t) (args u) (args s)"
       proof (clarify, rule extf_trans[OF _ _ _ gt_trans_args])
         fix f
         assume f_in_grounds: "f \<in> ground_heads (head u)"
         show "extf f (>\<^sub>t) (args u) (args t)"
           using f_in_grounds gt_same_u_t(3) by blast
         show "extf f (>\<^sub>t) (args t) (args s)"
           using f_in_grounds gt_same_t_s(3) unfolding gt_same_u_t(1) by blast
       qed auto
       have "chkchop_same (>\<^sub>t) u s"
       proof (cases "head u")
         case (Var x)
         then show ?thesis
         proof (cases u)
           case (Hd _)
           then show ?thesis 
             using Var by auto
         next
           case (App u1 u2)
           then have "chop u >\<^sub>t chop t" 
             by (metis Var args.simps(1) chkchop_def chkchop_same_def epo.extf_min_empty epo_axioms gt_hd_def gt_hd_irrefl gt_same_t_s(3) gt_same_u_t(2) hd.disc(1) tm.collapse(1) tm.disc(2))
           then show ?thesis
           proof (cases t)
             case (Hd _)
             then show ?thesis 
               using extf_min_empty gt_same_t_s(3) by auto
           next
             case t_App: (App t1 t2)
             then have "is_App s \<Longrightarrow> chop t >\<^sub>t chop s" 
               using gt_same_t_s unfolding chkchop_same_def unfolding chkchop_def using Var hd_u_s by auto
             then have "chkchop (>\<^sub>t) (chop u) s" 
               unfolding chkchop_def using ih[of "chop u" "chop t" "chop s"]
-              by (metis App \<open>chop u >\<^sub>t chop t\<close> t_App add_mset_lt_lt_le less_imp_le mset_lt_single_iff size_chop_lt tm.disc(2))
+              by (metis App \<open>chop u >\<^sub>t chop t\<close> t_App add_mset_lt_lt_le less_imp_le mset_lt_single_iff hsize_chop_lt tm.disc(2))
             then show ?thesis unfolding chkchop_same_def 
               using Var by auto
           qed
         qed
       next
         case (Sym f)
         have "chkchop (>\<^sub>t) u s" 
          proof (cases s)
            case (Hd _)
            then show ?thesis 
              by simp
          next
            case (App s1 s2)
            then have "t >\<^sub>t chop s"
              using Sym gt_same_t_s(1) gt_same_t_s(2) hd_u_s by auto
            then have "u >\<^sub>t chop s" using ih[of u t "chop s"] 
-             by (metis App add_mset_lt_right_lt mset_lt_single_iff size_chop_lt tm.disc(2) u_gt_t)
+             by (metis App add_mset_lt_right_lt mset_lt_single_iff hsize_chop_lt tm.disc(2) u_gt_t)
            then show ?thesis unfolding chkchop_def
              by blast
          qed
         then show ?thesis
           by (simp add: Sym) 
       qed
       thus ?thesis 
         using \<open>\<forall>f\<in>local.ground_heads (head u). extf f (>\<^sub>t) (args u) (args s)\<close> gt_same hd_u_s by blast
     qed
   qed
 qed
 
 subsection \<open>Irreflexivity\<close>
 
 theorem gt_irrefl: "\<not> s >\<^sub>t s"
-proof (standard, induct s rule: measure_induct_rule[of size])
+proof (standard, induct s rule: measure_induct_rule[of hsize])
   case (less s)
   note ih = this(1) and s_gt_s = this(2)
 
   show False
     using s_gt_s
   proof cases
     case gt_chop
     then show False using ih[of "chop s"]
-      by (metis gt.gt_chop gt_trans size_chop_lt)
+      by (metis gt.gt_chop gt_trans hsize_chop_lt)
   next
     case gt_diff
     thus False
       by (cases "head s") (auto simp: gt_hd_irrefl)
   next
     case gt_same
     note in_grounds = this(3)
 
     obtain si where si_in_args: "si \<in> set (args s)" and si_gt_si: "si >\<^sub>t si"
       using in_grounds
       by (metis (full_types) all_not_in_conv extf_irrefl_from_trans ground_heads_nonempty gt_trans)
-    have "size si < size s"
-      by (rule size_in_args[OF si_in_args])
+    have "hsize si < hsize s"
+      by (rule hsize_in_args[OF si_in_args])
     thus False
       by (rule ih[OF _ si_gt_si])
   qed
 qed
 
 lemma gt_antisym: "t >\<^sub>t s \<Longrightarrow> \<not> s >\<^sub>t t"
   using gt_irrefl gt_trans by blast
 
 
 subsection "Compatibility with Embedding Relation"
 
 (* TODO: move? *)
 lemma nth_drop_lemma:
   assumes "length xs = length ys"
 and "k \<le> length xs"
 and "\<And>i. i < length xs \<longrightarrow> i \<ge> k \<longrightarrow> xs ! i = ys ! i"
 shows "drop k xs = drop k ys"
   using assms proof (induct arbitrary:k rule:list_induct2)
   case Nil
   then show ?case by simp
 next
   case (Cons x xs y ys)
   then show ?case proof (cases k)
     case 0
     then have "x # xs =  y # ys" 
       by (metis Cons.hyps(1) Cons.prems(2) leI length_Cons not_less_zero nth_equalityI)
     then show ?thesis 
       by blast
   next
     case (Suc m)
     then have "drop m xs = drop m ys" 
       by (metis Cons.hyps(2) Cons.prems(1) Cons.prems(2) Suc_le_mono Suc_mono length_Cons nth_Cons_Suc)
     then show ?thesis 
       by (simp add: Suc)
   qed
 qed
 
 lemma gt_embedding_step_property:
   assumes "t \<rightarrow>\<^sub>e\<^sub>m\<^sub>b s"
   shows "t >\<^sub>t s"
   using assms 
   apply(simp only: atomize_imp)
-  apply (rule measure_induct_rule[of "\<lambda>(t, s). size t + size s"
+  apply (rule measure_induct_rule[of "\<lambda>(t, s). hsize t + hsize s"
       "\<lambda>(t, s). t \<rightarrow>\<^sub>e\<^sub>m\<^sub>b s \<longrightarrow> t >\<^sub>t s" "(t, s)", simplified prod.case])
 proof(simp only: split_paired_all prod.case atomize_imp[symmetric])
   fix s t :: "('s,'v) tm" 
   assume "t \<rightarrow>\<^sub>e\<^sub>m\<^sub>b s" 
-    and ih: "\<And>tt ss. size tt + size ss < size t + size s \<Longrightarrow> tt \<rightarrow>\<^sub>e\<^sub>m\<^sub>b ss \<Longrightarrow> tt >\<^sub>t ss"
+    and ih: "\<And>tt ss. hsize tt + hsize ss < hsize t + hsize s \<Longrightarrow> tt \<rightarrow>\<^sub>e\<^sub>m\<^sub>b ss \<Longrightarrow> tt >\<^sub>t ss"
   have "is_App t" 
     by (metis \<open>t \<rightarrow>\<^sub>e\<^sub>m\<^sub>b s\<close> emb_step_at_is_App emb_step_equiv)
 
   obtain p d where "emb_step_at p d t = s" "position_of t (p @ [d])"
     using \<open>t \<rightarrow>\<^sub>e\<^sub>m\<^sub>b s\<close> emb_step_equiv by (metis position_if_emb_step_at)
   define q where q_rep_t: "q = replicate (num_args (fun t)) Left"
 
   show "t >\<^sub>t s"
   proof (cases "list_all (\<lambda>x. x = Left) p")
     case True
     show ?thesis
     proof (cases d)
       text \<open>Embedding removes an argument i\<close>
       case Left
       define i where "i = num_args t - Suc (length p)"
       then  have " head t = head s" "i < num_args t" "args s = take i (args t) @ drop (Suc i) (args t)"
         using emb_step_at_remove_arg Left True \<open>emb_step_at p d t = s\<close> \<open>position_of t (p @ [d])\<close> 
         by metis+
       have "is_App s \<Longrightarrow> chop t \<rightarrow>\<^sub>e\<^sub>m\<^sub>b chop s" 
       proof (cases "p = q")
         case True
         assume "is_App s"
         show ?thesis 
         proof -          
           have "Suc (num_args (fun s)) = num_args (fun t)" 
             by (metis One_nat_def Suc_num_args True \<open>args s = take i (args t) @ drop (Suc i) (args t)\<close> \<open>is_App s\<close> \<open>is_App t\<close> append_self_conv2 cancel_comm_monoid_add_class.diff_cancel diff_Suc_1 i_def length_drop length_replicate q_rep_t take_eq_Nil)
           have "emb_step_at (replicate (num_args (fun s)) Left) Right (chop t) =
                 emb_step_at (replicate (num_args (fun s)) Left) Right t" 
             using merge_emb_step_at[of "replicate (num_args (fun s)) Left" Right Nil Right t, unfolded append_Nil2 opp_simps(1) replicate_append_same]
             by (metis \<open>Suc (num_args (fun s)) = num_args (fun t)\<close> \<open>is_App t\<close> chop_emb_step_at replicate_Suc)
           then have "emb_step_at (replicate (num_args (fun s)) dir.Left) dir.Right (chop t) = chop s" unfolding chop_emb_step_at[OF \<open>is_App s\<close>]
             using merge_emb_step_at[of "replicate (num_args (fun s)) Left" Right Nil Left t, unfolded append_Nil2 opp_simps(1) replicate_append_same]
             by (metis Left True \<open>Suc (num_args (fun s)) = num_args (fun t)\<close> \<open>emb_step_at p d t = s\<close> q_rep_t replicate_Suc)
           then show "chop t \<rightarrow>\<^sub>e\<^sub>m\<^sub>b chop s"
-            by (metis \<open>is_App s\<close> \<open>is_App t\<close> \<open>t \<rightarrow>\<^sub>e\<^sub>m\<^sub>b s\<close> emb_step_equiv emb_step_size nat_neq_iff size_chop)
+            by (metis \<open>is_App s\<close> \<open>is_App t\<close> \<open>t \<rightarrow>\<^sub>e\<^sub>m\<^sub>b s\<close> emb_step_equiv emb_step_hsize nat_neq_iff hsize_chop)
         qed
       next
         case False
         assume "is_App s" 
         have p_rep: "p = replicate (length p) Left" 
           by (metis (full_types) \<open>list_all (\<lambda>x. x = Left) p\<close> list_all_iff replicate_length_same)
         have length_p:"length p < num_args t" using no_position_replicate_num_args \<open>position_of t (p @ [d])\<close> 
             replicate_add[of "num_args t" "length p - num_args t" Left]  p_rep q_rep_t
           by (metis Left add_diff_inverse_nat replicate_app_Cons_same replicate_append_same shallower_pos)
         then have "length p \<le> length q" 
           using Suc_num_args \<open>is_App t\<close> q_rep_t by fastforce
         then have "length p < length q"
           using False le_neq_implies_less p_rep q_rep_t by fastforce
         then have "take (Suc (length p)) q = p @ [Left]" 
           by (metis (no_types, lifting) \<open>length p \<le> length q\<close> length_replicate min.orderE nth_replicate p_rep q_rep_t take_Suc_conv_app_nth take_replicate)
         then obtain q' where "q = p @ [Left] @ q'" 
           by (metis append.assoc append_take_drop_id)
         have "Suc (num_args (fun s)) = num_args (fun t)" 
           by (metis (no_types, lifting) Cons_nth_drop_Suc Suc_num_args \<open>args s = take i (args t) @ drop (Suc i) (args t)\<close> \<open>i < num_args t\<close> \<open>is_App s\<close> \<open>is_App t\<close> add_Suc_right append_take_drop_id diff_Suc_1 length_Cons length_append)
         then have "chop s = emb_step_at p dir.Left (chop t)"
           using swap_nested_emb_step_at[of p q' Right Left t] chop_emb_step_at[OF \<open>is_App s\<close>]
             chop_emb_step_at[OF \<open>is_App t\<close>]  
           by (metis (no_types, lifting) Cons_replicate_eq Left \<open>emb_step_at p d t = s\<close> \<open>q = p @ [dir.Left] @ q'\<close> append.assoc append_Cons diff_Suc_1 p_rep q_rep_t replicate_append_same)
         then show "chop t \<rightarrow>\<^sub>e\<^sub>m\<^sub>b chop s" 
           by (metis Left \<open>is_App t\<close> \<open>position_of t (p @ [d])\<close> \<open>q = p @ [dir.Left] @ q'\<close> chop_emb_step_at emb_step_at_if_position pos_emb_step_at_nested q_rep_t)
       qed
       then have "chkchop_same (>\<^sub>t) t s"
       proof (cases "is_Var (head t)")
         case True
         then show ?thesis unfolding chkchop_same_def chkchop_def  using ih[of "chop t" "chop s"] 
-           add_less_mono size_chop_lt \<open>is_App s \<Longrightarrow> chop t \<rightarrow>\<^sub>e\<^sub>m\<^sub>b chop s\<close> by metis
+           add_less_mono hsize_chop_lt \<open>is_App s \<Longrightarrow> chop t \<rightarrow>\<^sub>e\<^sub>m\<^sub>b chop s\<close> by metis
       next
         case False
         then show ?thesis unfolding chkchop_same_def chkchop_def 
-        using \<open>is_App t\<close> add_less_mono gt_chop ih size_chop_lt 
+        using \<open>is_App t\<close> add_less_mono gt_chop ih hsize_chop_lt 
         \<open>is_App s \<Longrightarrow> chop t \<rightarrow>\<^sub>e\<^sub>m\<^sub>b chop s\<close> by metis
       qed
       have "\<forall>f\<in>local.ground_heads (head t). extf f (>\<^sub>t) (args t) (args s)" 
         using extf_ext_insert_arg[of _ _ "take i (args t)" "args t ! i" "drop (Suc i) (args t)"]
         using \<open>args s = take i (args t) @ drop (Suc i) (args t)\<close> \<open>i < num_args t\<close> id_take_nth_drop by fastforce
       then show ?thesis using gt_same \<open>head t = head s\<close> \<open>chkchop_same (>\<^sub>t) t s\<close> by blast
     next
       text \<open>Embedding chops and might remove arguments from the left\<close>
       case Right
       show ?thesis using emb_step_at_chop
-        by (metis Right True \<open>emb_step_at p d t = s\<close> \<open>is_App t\<close> \<open>position_of t (p @ [d])\<close> add_Suc gt_chop ih less_Suc_eq size_chop)
+        by (metis Right True \<open>emb_step_at p d t = s\<close> \<open>is_App t\<close> \<open>position_of t (p @ [d])\<close> add_Suc gt_chop ih less_Suc_eq hsize_chop)
     qed
   next
     text \<open>Embedding operates under one of the arguments\<close>
     case False
     have "num_args t = num_args s" using emb_step_under_args_num_args[OF False] 
       by (metis (no_types) \<open>\<And>t d. num_args (emb_step_at p d t) = num_args t\<close> \<open>emb_step_at p d t = s\<close>)
     then have "is_App s" using \<open>num_args t = num_args s\<close> 
       by (metis args_Nil_iff_is_Hd length_0_conv \<open>is_App t\<close>)
 
     have q_rep_s: "q = replicate (num_args (fun s)) Left"
       by (metis  q_rep_t \<open>is_App s\<close> \<open>is_App t\<close> \<open>num_args t = num_args s\<close> args.simps(2) butlast_snoc length_butlast tm.collapse(2))
 
     have "chop t \<rightarrow>\<^sub>e\<^sub>m\<^sub>b chop s"
     proof (cases "take (num_args (fun t)) p = q")
       case True
       have  "num_args (fun t) < length p"
       proof (rule ccontr)
         assume "\<not> num_args (fun t) < length p"
         then have "num_args (fun t) = length p"  "q = p"
           using True q_rep_t by auto
         then show False using False 
           using list_all_length q_rep_t by fastforce
       qed
 
       have "p ! (num_args (fun t)) = Right" 
       proof (rule ccontr)
         assume "p ! num_args (fun t) \<noteq> Right"
         then have "p ! num_args (fun t) = Left" using dir.exhaust by blast
         then have "take (num_args t) p = replicate (num_args t) Left" using True Suc_num_args[OF \<open>is_App t\<close>] q_rep_t
             take_Suc_conv_app_nth[of "num_args (fun t)" p]
           by (metis \<open>num_args (fun t) < length p\<close> replicate_Suc replicate_append_same)
         then show False 
           by (metis \<open>num_args t = num_args s\<close> \<open>num_args t = num_args s\<close> \<open>position_of t (p @ [d])\<close> 
               append.assoc append_eq_Cons_conv append_take_drop_id no_position_replicate_num_args shallower_pos)
       qed
 
       then obtain q' where "p = q @ [Right] @ q'"
         by (metis Cons_nth_drop_Suc True \<open>num_args (fun t) < length p\<close> append_Cons append_Nil append_eq_conv_conj length_replicate q_rep_t)
       have "emb_step_at (q @ q') d (chop t) = chop s"
         unfolding chop_emb_step_at[OF \<open>is_App t\<close>] chop_emb_step_at[OF \<open>is_App s\<close>] 
         using swap_nested_emb_step_at[of q q' d Right t, unfolded] \<open>emb_step_at p d t = s\<close> \<open>p = q @ [Right] @ q'\<close> 
         q_rep_t q_rep_s by auto
       moreover have "chop t \<noteq> chop s"
-        by (metis \<open>is_App s\<close> \<open>is_App t\<close> \<open>t \<rightarrow>\<^sub>e\<^sub>m\<^sub>b s\<close> emb_step_size nat_less_le size_chop)
+        by (metis \<open>is_App s\<close> \<open>is_App t\<close> \<open>t \<rightarrow>\<^sub>e\<^sub>m\<^sub>b s\<close> emb_step_hsize nat_less_le hsize_chop)
       ultimately show "chop t \<rightarrow>\<^sub>e\<^sub>m\<^sub>b chop s" 
         using emb_step_equiv by blast
     next
       case False
       then have takepq: "take (length q) p \<noteq> q" 
         using q_rep_t by auto
       have takeqp: "length p \<le> length q \<Longrightarrow> take (length p) q \<noteq> p"
         using \<open>\<not> list_all (\<lambda>x. x = Left) p\<close>[unfolded list_all_length]
         using diff_diff_cancel take_replicate length_replicate  nth_replicate q_rep_s by metis
       have "chop s = emb_step_at p d (chop t)" 
         using swap_disjunct_emb_step_at[of p q Right d t, OF takeqp takepq, unfolded \<open>emb_step_at p d t = s\<close>] 
         using \<open>is_App s\<close> \<open>is_App t\<close> chop_emb_step_at q_rep_s q_rep_t
         by (simp add: chop_emb_step_at)
       then show ?thesis 
         by (metis False \<open>is_App t\<close> \<open>position_of t (p @ [d])\<close> chop_emb_step_at emb_step_at_if_position length_replicate nat_le_linear pos_emb_step_at_disjunct q_rep_t take_all takeqp)
     qed
     then have gt1:"chkchop_same (>\<^sub>t) t s"  
     proof (cases "head t")
       case (Var _)
       then have "chop t >\<^sub>t chop s" using ih[of "chop t" "chop s"]
-        by (meson \<open>chop t \<rightarrow>\<^sub>e\<^sub>m\<^sub>b chop s\<close> \<open>is_App s\<close> \<open>is_App t\<close> add_strict_mono size_chop_lt)
+        by (meson \<open>chop t \<rightarrow>\<^sub>e\<^sub>m\<^sub>b chop s\<close> \<open>is_App s\<close> \<open>is_App t\<close> add_strict_mono hsize_chop_lt)
       then show ?thesis  unfolding chkchop_same_def
         by (simp add: Var)
     next
       case (Sym _)
       then show ?thesis unfolding chkchop_same_def using \<open>chop t \<rightarrow>\<^sub>e\<^sub>m\<^sub>b chop s\<close> 
          \<open>is_App t\<close> add_Suc add_Suc_shift chkchop_def gt_trans ih 
-         less_Suc_eq size_chop t_gt_chop_t 
+         less_Suc_eq hsize_chop t_gt_chop_t 
         by (metis (no_types, lifting))
     qed
       have gt2:"head t = head s"  
       by (metis emb_step_under_args_head False \<open>emb_step_at p d t = s\<close>) 
     have gt3:"\<forall>f\<in>local.ground_heads (head t). extf f (>\<^sub>t) (args t) (args s)" 
     proof (rule ballI)
       fix f assume "f\<in>local.ground_heads (head t)"
       obtain i where i_def:
         "i < num_args t"
         "args t ! i \<rightarrow>\<^sub>e\<^sub>m\<^sub>b args (emb_step_at p d t) ! i"
         "\<And>j. j < num_args t \<Longrightarrow> i \<noteq> j \<Longrightarrow> args t ! j = args (emb_step_at p d t) ! j"
         using emb_step_under_args_emb_step[of p t d] 
         using False \<open>position_of t (p @ [d])\<close> by blast
       have compat_list1: "args t ! i >\<^sub>t args s ! i" 
-        by (metis \<open>num_args t = num_args s\<close> \<open>emb_step_at p d t = s\<close>  add_less_mono i_def(1) i_def(2) ih nth_mem size_in_args)
+        by (metis \<open>num_args t = num_args s\<close> \<open>emb_step_at p d t = s\<close>  add_less_mono i_def(1) i_def(2) ih nth_mem hsize_in_args)
       have compat_list2: "args t ! i \<noteq> args s ! i" 
         using emb_step_equiv i_def(2) \<open>emb_step_at p d t = s\<close>  by blast
       have argst:"args t = take i (args t) @ args t ! i # drop (Suc i) (args t)" 
         by (simp add: Cons_nth_drop_Suc i_def(1))
       have argss:"args s = take i (args t) @ args (emb_step_at p d t) ! i # drop (Suc i) (args t)"
       proof -
         have "take i (args t) = take i (args s)" 
           apply (rule nth_take_lemma) 
           using \<open>num_args t = num_args s\<close> i_def(1) i_def(3)[unfolded \<open>emb_step_at p d t = s\<close>] by auto
         moreover have "drop (Suc i) (args t) = drop (Suc i) (args s)" 
           apply (rule nth_drop_lemma) 
             apply (simp add: \<open>num_args t = num_args s\<close>)
            apply (simp add: Suc_le_eq i_def(1))
           using Suc_n_not_le_n \<open>emb_step_at p d t = s\<close> i_def(3) by blast
         ultimately show ?thesis
           using \<open>emb_step_at p d t = s\<close> \<open>num_args t = num_args s\<close> i_def(1) id_take_nth_drop by auto
       qed
       show "extf f (>\<^sub>t) (args t) (args s)"
         using  extf_compat_list[of "args t ! i" "args (emb_step_at p d t) ! i" gt f "take i (args t)"  "drop (Suc i) (args t)"] 
         using \<open>emb_step_at p d t = s\<close> argss argst compat_list1 compat_list2 by force
     qed
     show ?thesis using gt_same using gt1 gt2 gt3 by blast
   qed
 qed  
 
 lemma gt_embedding_property:
   assumes "t \<unrhd>\<^sub>e\<^sub>m\<^sub>b s" "t \<noteq> s"
   shows "t >\<^sub>t s"
   using assms 
 proof (induction)
   case (refl t)
   then show ?case by simp
 next
   case (step t u s)
   then show ?case using gt_embedding_step_property gt_trans by blast
 qed
 
 
 subsection \<open>Subterm Property\<close>
   
 theorem gt_proper_sub: "proper_sub s t \<Longrightarrow> t >\<^sub>t s" 
   using gt_embedding_property sub_emb by blast
 
 lemma
   gt_emb_fun: "App s t >\<^sub>t s" and
   gt_emb_arg: "App s t >\<^sub>t t"
   by (simp_all add: gt_embedding_step_property left right)
 
 
 subsection \<open>Compatibility with Contexts\<close>
 
 lemma gt_fun_imp: "fun t >\<^sub>t s \<Longrightarrow> t >\<^sub>t s" 
   by (metis emb_step_fun gt_embedding_step_property gt_trans tm.disc(2) tm.exhaust_sel tm.sel(3))
 
 lemma gt_arg_imp: "arg t >\<^sub>t s \<Longrightarrow> t >\<^sub>t s" 
   by (metis emb_step_arg gt_embedding_step_property gt_trans tm.disc(2) tm.exhaust_sel tm.sel(5))
 
 lemma gt_compat_fun:
   assumes "t' >\<^sub>t t"
   shows "App s t' >\<^sub>t App s t"
 using assms  apply (simp only:atomize_imp)
-proof (induction rule:measure_induct_rule[of "\<lambda>(t, s). size t + size s" "\<lambda>(t, s). t' >\<^sub>t t \<longrightarrow> App s t' >\<^sub>t App s t" "(t,s)", 
+proof (induction rule:measure_induct_rule[of "\<lambda>(t, s). hsize t + hsize s" "\<lambda>(t, s). t' >\<^sub>t t \<longrightarrow> App s t' >\<^sub>t App s t" "(t,s)", 
   simplified prod.case],
   simp only: split_paired_all prod.case atomize_imp[symmetric])
 
   fix t s ::"('s, 'v) tm" 
-  assume ih:"\<And>ta sa. size ta + size sa < size t + size s \<Longrightarrow> t' >\<^sub>t ta \<Longrightarrow> App sa t' >\<^sub>t App sa ta"
+  assume ih:"\<And>ta sa. hsize ta + hsize sa < hsize t + hsize s \<Longrightarrow> t' >\<^sub>t ta \<Longrightarrow> App sa t' >\<^sub>t App sa ta"
   and t'_gt_t:"t' >\<^sub>t t" 
 
   have t'_ne_t: "t' \<noteq> t"
     using gt_antisym t'_gt_t by blast
   have extf_args_single: "\<forall>f \<in> ground_heads (head s). extf f (>\<^sub>t) (args s @ [t']) (args s @ [t])"
     by (simp add: extf_compat_list t'_gt_t t'_ne_t)
 
   show  "App s t' >\<^sub>t App s t"
   proof (rule gt_same)
     show "head (App s t') = head (App s t)" by simp
     show "\<forall>f\<in>local.ground_heads (head (App s t')). extf f (>\<^sub>t) (args (App s t')) (args (App s t))"
       by (simp add: extf_args_single)
     have 0: "chop (App s t') >\<^sub>t chop (App s t)" 
     proof (cases s)
       case (Hd _)
       then show ?thesis using chop_App_Hd
         by (simp add: chop_App_Hd t'_gt_t)
     next
       case (App s1 s2)
       then show ?thesis using ih[of t "chop s"] chop_fun 
-        by (metis nat_add_left_cancel_less size_chop_lt t'_gt_t tm.disc(2) tm.sel(4) tm.sel(6))
+        by (metis nat_add_left_cancel_less hsize_chop_lt t'_gt_t tm.disc(2) tm.sel(4) tm.sel(6))
     qed
     show "chkchop_same (>\<^sub>t) (App s t') (App s t)"
     proof (cases "is_Var (head (App s t'))")
       case True
       then show ?thesis unfolding chkchop_same_def chkchop_def
         using True 0 by auto
     next
       case False
       have "App s t' >\<^sub>t chop (App s t)" using 0 by (simp add: gt_chop)
       then show ?thesis  unfolding chkchop_same_def chkchop_def 
         using False by auto
     qed
   qed
 qed
 
 theorem gt_compat_arg:
   shows "s' >\<^sub>t s \<Longrightarrow> t' \<ge>\<^sub>t t \<Longrightarrow> App s' t' >\<^sub>t App s t"
-proof (simp only:atomize_imp,induction rule:measure_induct[of "\<lambda>(s',s,t). size s' + size s + size t" "\<lambda>(s',s,t). s' >\<^sub>t s \<longrightarrow> t' \<ge>\<^sub>t t \<longrightarrow> App s' t' >\<^sub>t App s t" "(s',s,t)", simplified prod.case],
+proof (simp only:atomize_imp,induction rule:measure_induct[of "\<lambda>(s',s,t). hsize s' + hsize s + hsize t" "\<lambda>(s',s,t). s' >\<^sub>t s \<longrightarrow> t' \<ge>\<^sub>t t \<longrightarrow> App s' t' >\<^sub>t App s t" "(s',s,t)", simplified prod.case],
     simp only: split_paired_all prod.case atomize_imp[symmetric] atomize_all[symmetric])
   fix s' s t
-  assume ih:"\<And>ab ac ba. size ab + size ac + size ba < size s' + size s + size t \<Longrightarrow> ab >\<^sub>t ac \<Longrightarrow> t' \<ge>\<^sub>t ba \<Longrightarrow> App ab t' >\<^sub>t App ac ba" 
+  assume ih:"\<And>ab ac ba. hsize ab + hsize ac + hsize ba < hsize s' + hsize s + hsize t \<Longrightarrow> ab >\<^sub>t ac \<Longrightarrow> t' \<ge>\<^sub>t ba \<Longrightarrow> App ab t' >\<^sub>t App ac ba" 
     and "s' >\<^sub>t s" and "t' \<ge>\<^sub>t t" 
 
   {
-    fix s''::"('s,'v) tm" assume size_s'':"size s'' \<le> size s'"
+    fix s''::"('s,'v) tm" assume hsize_s'':"hsize s'' \<le> hsize s'"
     assume chkchop_s'_s: "chkchop (>\<^sub>t) s'' s"
     then have "chkchop (>\<^sub>t) (App s'' t') (App s t)" 
     proof (cases "is_Hd s")
       case True
       then show ?thesis using chkchop_s'_s unfolding chkchop_def 
         by (metis \<open>t' \<ge>\<^sub>t t\<close> chop_App_Hd gt_arg_imp gt_emb_arg tm.sel(6))
     next
       case False
       then show ?thesis using chkchop_s'_s unfolding chkchop_def
-        using ih[of s'' "chop s" t] size_s''
-        by (metis \<open>t' \<ge>\<^sub>t t\<close> add_less_mono add_mono_thms_linordered_field(1) chop_fun le_eq_less_or_eq nat_add_left_cancel_less size_chop_lt tm.sel(4) tm.sel(6))
+        using ih[of s'' "chop s" t] hsize_s''
+        by (metis \<open>t' \<ge>\<^sub>t t\<close> add_less_mono add_mono_thms_linordered_field(1) chop_fun le_eq_less_or_eq nat_add_left_cancel_less hsize_chop_lt tm.sel(4) tm.sel(6))
     qed
   }
   note chkchop_compat_arg = this
 
   show "App s' t' >\<^sub>t App s t " using \<open>s' >\<^sub>t s\<close>
   proof (cases rule:gt.cases)
     case gt_chop
     then show ?thesis 
     proof (cases "t = t'")
       case True
       show ?thesis using True gt.gt_chop[of "App s' t'" "App s t"] gt_chop chkchop_compat_arg[of "chop s'"]
-        by (metis add_strict_right_mono chop_fun ih size_chop_lt tm.disc(2) tm.sel(4) tm.sel(6))
+        by (metis add_strict_right_mono chop_fun ih hsize_chop_lt tm.disc(2) tm.sel(4) tm.sel(6))
     next
       case False
       then have "t' >\<^sub>t t"
         using \<open>t' \<ge>\<^sub>t t\<close> by blast
       have "App s' t' >\<^sub>t App (chop s') t'" 
         by (simp add: context_left emb_step_chop gt_embedding_step_property local.gt_chop(1))
       moreover have "... >\<^sub>t App s t"  using ih[of "chop s'" s t]
-        using \<open>t' >\<^sub>t t\<close> gt_compat_fun local.gt_chop(1) local.gt_chop(2) size_chop_lt by fastforce
+        using \<open>t' >\<^sub>t t\<close> gt_compat_fun local.gt_chop(1) local.gt_chop(2) hsize_chop_lt by fastforce
       ultimately show ?thesis using gt_trans by blast
     qed
   next
     case gt_diff
     then show ?thesis 
       using chkchop_compat_arg gt.gt_diff by auto
   next
     case gt_same
     have hd_s'_eq_s: "head s' = head s" 
       by (simp add: local.gt_same(1))
     {
       fix f assume f_gh: "f \<in> ground_heads (head s)"
       have f_s_args: 
         "extf f (>\<^sub>t) (args s') (args s)"
         using local.gt_same(3) f_gh by (simp add: hd_s'_eq_s)
       have f_compat_snoc: 
         "\<And>xs ys x. extf f (>\<^sub>t) ys xs \<Longrightarrow> extf f (>\<^sub>t) (ys @ [x]) (xs @ [x])" 
         by (simp add: extf_compat_append_right)
      
       have f_st_args2:
         "extf f (>\<^sub>t) (args (App s' t)) (args (App s t))"
         by (simp add: f_compat_snoc f_s_args)
       have 0:"\<forall>z\<in>UNIV. \<forall>y\<in>UNIV. \<forall>x\<in>UNIV. z >\<^sub>t y \<longrightarrow> y >\<^sub>t x \<longrightarrow> z >\<^sub>t x" 
         using gt_trans by blast
       then have f_trans:"\<And>xs ys zs. extf f (>\<^sub>t) zs ys \<Longrightarrow> extf f (>\<^sub>t) ys xs \<Longrightarrow> extf f (>\<^sub>t) zs xs" 
         using  extf_trans[of _ UNIV, unfolded lists_UNIV, OF UNIV_I UNIV_I UNIV_I 0] by metis
       have "extf f (>\<^sub>t) (args (App s' t')) (args (App s t))"
       proof (cases "t' = t")
         case True
         then show ?thesis using f_st_args2 by metis
       next
         case False
         have f_st_args1: 
           "extf f (>\<^sub>t) (args (App s' t')) (args (App s' t))"
           using extf_compat_list \<open>t' \<ge>\<^sub>t t\<close> False by simp
         then show ?thesis using f_trans f_st_args1 f_st_args2 by metis
       qed
     }
     note extf_cond = this
     have "chkchop_same (>\<^sub>t) (App s' t') (App s t)" unfolding chkchop_same_def
       using args.simps(1) chop_fun chkchop_compat_arg[of "chop s'", unfolded le_eq_less_or_eq] 
       chkchop_compat_arg[of s'] chkchop_def chkchop_same_def 
-      size_chop_lt   epo.extf_min_empty[OF epo_axioms] gt.gt_same gt_antisym hd_s'_eq_s head_App 
+      hsize_chop_lt   epo.extf_min_empty[OF epo_axioms] gt.gt_same gt_antisym hd_s'_eq_s head_App 
       leI less_irrefl_nat local.gt_same(2) local.gt_same(3) tm.collapse(1) tm.sel(4) tm.sel(6)
       by metis
     then show ?thesis 
       using extf_cond gt.gt_same hd_s'_eq_s by auto
   qed
 qed
 
 theorem gt_compat_fun_strong:
   assumes t'_gt_t: "t' >\<^sub>t t"
   shows "apps s (t' # us) >\<^sub>t apps s (t # us)" 
 proof (induct us rule: rev_induct)
   case Nil
   then show ?case 
   by (simp add: gt_compat_fun t'_gt_t)
 next
   case (snoc x xs)
   then show ?case unfolding App_apps[symmetric] append_Cons[symmetric]
     using gt_compat_arg by blast
 qed
 
 theorem gt_or_eq_compat_App: "s' \<ge>\<^sub>t s \<Longrightarrow> t' \<ge>\<^sub>t t \<Longrightarrow> App s' t' \<ge>\<^sub>t App s t"
   using gt_compat_fun gt_compat_arg by blast
 
 theorem gt_compat_App:
   shows "s' \<ge>\<^sub>t s \<Longrightarrow> t' >\<^sub>t t \<Longrightarrow> App s' t' >\<^sub>t App s t"
   using gt_compat_fun gt_compat_arg by blast
 
 subsection "Stability under Substitutions"
 
 (* TODO: move *)
 lemma extf_map2:
   assumes
     "\<forall>y\<in>set ys \<union> set xs. \<forall>x\<in>set ys \<union> set xs. y >\<^sub>t x \<longrightarrow> (h y) >\<^sub>t (h x)"
     "extf f (>\<^sub>t) ys xs"
   shows
     "extf f (>\<^sub>t) (map h ys) (map h xs)"
   apply (rule extf_map[of "set ys \<union> set xs" ys xs "(>\<^sub>t)" h f])
         apply simp
        apply (simp add: in_listsI)
       apply (simp add: in_listsI)
   using gt_antisym apply blast
   using gt_trans apply blast
   by (simp add: assms)+
 
 (* TODO: move ? *)
 lemma less_multiset_doubletons:
   assumes
     "y <  t \<or>  y <  s"  
     "x <  t \<or>  x <  s" 
   shows 
     "{# y,  x#} < {# t,  s#}" 
   unfolding less_multiset\<^sub>D\<^sub>M
 proof (intro exI)
   let ?X = "{# t,  s#}"
   let ?Y = "{#y, x#}"
   show "?X \<noteq> {#} \<and> ?X \<subseteq># {#t, s#} \<and> {#y, x#} = {#t, s#} - ?X + ?Y \<and> (\<forall>k. k \<in># ?Y \<longrightarrow> (\<exists>a. a \<in># ?X \<and> k < a))"
     using add_eq_conv_diff assms(1) assms(2) by auto
 qed
 
 theorem gt_sus: 
   assumes \<rho>_wary: "wary_subst \<rho>"
   assumes ghd: "\<And>x. ground_heads (Var x) = UNIV" (* This condition is only needed for gt_same, not for gt_diff ! *)
   shows "t >\<^sub>t s \<Longrightarrow> subst \<rho> t >\<^sub>t subst \<rho> s"
-proof (simp only:atomize_imp,induction rule:measure_induct[of "\<lambda>(t,s). {# size t, size s #}" "\<lambda>(t,s). t >\<^sub>t s \<longrightarrow> subst \<rho> t >\<^sub>t subst \<rho> s" "(t,s)", simplified prod.case],
+proof (simp only:atomize_imp,induction rule:measure_induct[of "\<lambda>(t,s). {# hsize t, hsize s #}" "\<lambda>(t,s). t >\<^sub>t s \<longrightarrow> subst \<rho> t >\<^sub>t subst \<rho> s" "(t,s)", simplified prod.case],
     simp only: split_paired_all prod.case atomize_imp[symmetric] atomize_all[symmetric])
   fix t s
   assume ih:"\<And>tt ss.
-               {# size tt, size ss #} < {# size t, size s #} \<Longrightarrow>
+               {# hsize tt, hsize ss #} < {# hsize t, hsize s #} \<Longrightarrow>
                tt >\<^sub>t ss \<Longrightarrow> subst \<rho> tt >\<^sub>t subst \<rho> ss" 
     and "t >\<^sub>t s" 
   show "subst \<rho> t >\<^sub>t subst \<rho> s" using \<open>t >\<^sub>t s\<close>
   proof (cases)
     case t_gt_s_chop: gt_chop
     then show ?thesis 
       using emb_step_subst emb_step_chop[OF t_gt_s_chop(1)] gt_embedding_step_property 
-       emb_step_size gt_trans ih[of "chop t" s] by (metis add_mset_lt_left_lt)
+       emb_step_hsize gt_trans ih[of "chop t" s] by (metis add_mset_lt_left_lt)
   next
     case t_gt_s_diff: gt_diff
     have gt_diff1: "head (subst \<rho> t) >\<^sub>h\<^sub>d head (subst \<rho> s)" 
       by (meson assms gt_hd_def subsetCE t_gt_s_diff(1) wary_subst_ground_heads)
     have gt_diff2: "is_Sym (head (subst \<rho> s))"
       by (metis ground_imp_subst_iden hd.collapse(2) hd.simps(18) head_subst t_gt_s_diff(2) tm.sel(1) tm.simps(17))
     have gt_diff3: "chkchop (>\<^sub>t) (subst \<rho> t) (subst \<rho> s)"    
     proof (cases s)
       case (Hd _)
       then show ?thesis 
         using t_gt_s_diff unfolding chkchop_def 
         by (metis ground_imp_subst_iden hd.collapse(2) hd.simps(18) tm.disc(1) tm.sel(1) tm.simps(17))
     next
       case s_App: (App s1 s2)
       then show ?thesis using t_gt_s_diff unfolding chkchop_def
-        using ih[of t "chop s"] chop_subst_Sym size_chop_lt tm.disc(2)
+        using ih[of t "chop s"] chop_subst_Sym hsize_chop_lt tm.disc(2)
         by (metis add_mset_lt_left_lt add_mset_lt_right_lt)
     qed
     show ?thesis
       using gt_diff gt_diff1 gt_diff2 gt_diff3 by blast
   next
     case t_gt_s_same: gt_same
     have gt_same1: "head (subst \<rho> t) = head (subst \<rho> s)" 
       by (simp add: t_gt_s_same(1))
 
     have extf_map_ts:"\<forall>f\<in>ground_heads (head t). extf f (>\<^sub>t) (map (subst \<rho>) (args t)) (map (subst \<rho>) (args s))"
     proof -
       have ih_args: "\<forall>y\<in>set (args t) \<union> set (args s). \<forall>x\<in>set (args t) \<union> set (args s). y >\<^sub>t x \<longrightarrow> subst \<rho> y >\<^sub>t subst \<rho> x"
-        by (metis Un_iff less_multiset_doubletons size_in_args ih)
+        by (metis Un_iff less_multiset_doubletons hsize_in_args ih)
       have "\<forall>f\<in>ground_heads (head t). extf f (>\<^sub>t) (args t) (args s)"  
         using ghd t_gt_s_same(3) by metis
       then show ?thesis
         using extf_map[of "set (args t) \<union> set (args s)" "args t" "args s" gt "subst \<rho>"]
         using gt_irrefl gt_trans ih_args by blast
     qed
 
     show ?thesis
     proof (cases "head t")
       case (Var x1)
       then have "is_Var (head t)" by simp
       {
         fix u :: "('s, 'v) tm"
-        assume "ground_heads (head u) \<subseteq> ground_heads (head t)" "size u \<le> size (subst \<rho> (Hd (head t)))"
+        assume "ground_heads (head u) \<subseteq> ground_heads (head t)" "hsize u \<le> hsize (subst \<rho> (Hd (head t)))"
         then have "apps u (map (subst \<rho>) (args t)) >\<^sub>t apps u (map (subst \<rho>) (args s))" 
-        proof (induct "size u" arbitrary:u rule:less_induct)
+        proof (induct "hsize u" arbitrary:u rule:less_induct)
           case less
           then show ?case 
           proof (cases u)
             case u_Hd: (Hd _)
             then have "args u = []" 
               by simp
             then show ?thesis 
             proof (cases s)
               case s_Hd: (Hd _)
               show ?thesis 
                 apply (rule gt_same) 
                 using extf_map_ts  args_Nil_iff_is_Hd s_Hd u_Hd \<open>args u = []\<close> less by fastforce+
             next
               case s_App: (App _ _)
               then have "is_App t" 
                 by (metis args_Nil_iff_is_Hd extf_min_empty gt_hd_def gt_hd_irrefl t_gt_s_same(3))
   
               have "chop t >\<^sub>t chop s" 
                 using \<open>is_App t\<close> \<open>is_Var (head t)\<close> s_App t_gt_s_same(2) by auto
               then have "subst \<rho> (chop t) >\<^sub>t subst \<rho> (chop s)" using ih
-                by (metis \<open>is_App t\<close> less_multiset_doubletons s_App size_chop_lt tm.disc(2))
+                by (metis \<open>is_App t\<close> less_multiset_doubletons s_App hsize_chop_lt tm.disc(2))
   
               define ut where "ut = apps u (map (subst \<rho>) (args t))"
               define us where "us = apps u (map (subst \<rho>) (args s))"
               have 0:"\<And>ss. args (apps u ss) = ss" 
                 using  \<open>args u = []\<close> by simp
               have chop_us: "chop us = subst \<rho> (chop s)" 
                 unfolding chop_def subst_apps us_def 0 using hd_map
                 by (metis (no_types, lifting) args_Nil_iff_is_Hd map_tl s_App tm.disc(2))
               have chop_ut: "chop ut = subst \<rho> (chop t)"
                 unfolding chop_def subst_apps ut_def 0 using \<open>is_App t\<close> 
                 by (simp add: args_Nil_iff_is_Hd hd_map map_tl)
   
               have "head ut = head us" 
                 by (simp add: us_def ut_def)
               moreover have "chkchop_same (>\<^sub>t) ut us" unfolding chkchop_def chkchop_same_def 
                 by (metis "0" UNIV_witness \<open>is_Var (head t)\<close> \<open>subst \<rho> (chop t) >\<^sub>t subst \<rho> (chop s)\<close> 
                     args.simps(1) chop_us chop_ut extf_map_ts extf_min_empty 
                     ghd gt_chop is_Var_def tm.collapse(1) ut_def)
               moreover have "\<forall>f\<in>local.ground_heads (head ut). extf f (>\<^sub>t) (args ut) (args us)" 
                 using extf_map_ts less us_def ut_def using "0" by auto
               ultimately show "ut >\<^sub>t us" 
                 using gt_same by blast
             qed
           next
             case u_app: (App _ _)
             let ?ut = "apps u (map (subst \<rho>) (args t))"
             let ?us = "apps u (map (subst \<rho>) (args s))"
             have 1:"head ?ut = head ?ut" 
               by simp
             have "apps (chop u) (map (subst \<rho>) (args t)) >\<^sub>t apps (chop u) (map (subst \<rho>) (args s))"
-              using less.hyps[of "chop u"] size_chop_lt 
+              using less.hyps[of "chop u"] hsize_chop_lt 
               by (metis Var dual_order.trans ghd less.prems(2) less_or_eq_imp_le subset_UNIV tm.disc(2) u_app)
             then have "chop ?ut >\<^sub>t chop ?us" 
               by (simp add: chop_apps u_app)
             then have 2:"chkchop_same (>\<^sub>t) ?ut ?us" unfolding chkchop_same_def chkchop_def 
               by (metis UNIV_I \<open>is_Var (head t)\<close> args_Nil_iff_is_Hd args_apps extf_compat_append_left 
                   extf_map_ts extf_min_empty ghd gt_chop is_Var_def)
             have 3:"\<forall>f\<in>local.ground_heads (head ?ut). extf f (>\<^sub>t) (args ?ut) (args ?us)"
               using extf_compat_append_left extf_map_ts less.prems(1) by auto
             show ?thesis using gt_same 1 2 3 by simp
           qed
         qed
       }
       note inner_induction = this
       show ?thesis using inner_induction[of "subst \<rho> (Hd (head t))", unfolded subst_apps[symmetric]]
         by (metis Var ghd order_refl subset_UNIV t_gt_s_same(1) tm_collapse_apps)
     next
       case (Sym _)
       then have "is_Sym (head (subst \<rho> t))" "head (subst \<rho> t) = head t"
         by simp_all
       then have "chkchop_same (>\<^sub>t) t s"
         using t_gt_s_same unfolding chkchop_same_def chkchop_def
         using Sym by metis
       then have gt_same2: "chkchop_same (>\<^sub>t) (subst \<rho> t) (subst \<rho> s)" unfolding chkchop_same_def chkchop_def
          using ih[of t "chop s"] 
          by (metis (no_types, lifting) Sym \<open>head (subst \<rho> t) = head t\<close> \<open>is_Sym (head (subst \<rho> t))\<close> 
              add_mset_commute add_mset_lt_left_lt chop_subst_Sym ground_imp_subst_iden hd.simps(18) 
-             size_chop_lt t_gt_s_same(1) tm.collapse(1) tm.simps(17))
+             hsize_chop_lt t_gt_s_same(1) tm.collapse(1) tm.simps(17))
       have gt_same3: "\<forall>f\<in>local.ground_heads (head (subst \<rho> t)). extf f (>\<^sub>t) (args (subst \<rho> t)) (args (subst \<rho> s))"
         using \<open>head (subst \<rho> t) = head t\<close> extf_compat_append_left extf_map_ts t_gt_s_same(1) by auto
       show ?thesis using gt_same gt_same1 gt_same2 gt_same3 by blast
     qed
   qed
 qed
 
 
 subsection \<open>Totality on Ground Terms\<close>
 
 theorem gt_total_ground:
   assumes extf_total: "\<And>f. ext_total (extf f)"
   shows "ground t \<Longrightarrow> ground s \<Longrightarrow> t >\<^sub>t s \<or> s >\<^sub>t t \<or> t = s"
 proof (simp only: atomize_imp,
-    rule measure_induct_rule[of "\<lambda>(t, s). size t + size s"
+    rule measure_induct_rule[of "\<lambda>(t, s). hsize t + hsize s"
       "\<lambda>(t, s). ground t \<longrightarrow> ground s \<longrightarrow> t >\<^sub>t s \<or> s >\<^sub>t t \<or> t = s" "(t, s)", simplified prod.case],
     simp only: split_paired_all prod.case atomize_imp[symmetric])
   fix t s :: "('s, 'v) tm"
   assume
-    ih: "\<And>ta sa. size ta + size sa < size t + size s \<Longrightarrow> ground ta \<Longrightarrow> ground sa \<Longrightarrow>
+    ih: "\<And>ta sa. hsize ta + hsize sa < hsize t + hsize s \<Longrightarrow> ground ta \<Longrightarrow> ground sa \<Longrightarrow>
       ta >\<^sub>t sa \<or> sa >\<^sub>t ta \<or> ta = sa" and
     gr_t: "ground t" and gr_s: "ground s"
 
   let ?case = "t >\<^sub>t s \<or> s >\<^sub>t t \<or> t = s"
 
   have "chkchop (>\<^sub>t) t s \<or> s >\<^sub>t t"
     unfolding chkchop_def tm.case_eq_if using ih[of t "fun s"] ih[of t "arg s"]
-    by (metis gr_s gr_t gt_chop gt_imp_vars ih nat_add_left_cancel_less size_chop_lt subset_empty)
+    by (metis gr_s gr_t gt_chop gt_imp_vars ih nat_add_left_cancel_less hsize_chop_lt subset_empty)
   moreover have "chkchop (>\<^sub>t) s t \<or> t >\<^sub>t s"
     unfolding chkchop_def tm.case_eq_if using ih[of "fun t" s] ih[of "arg t" s]
-    by (metis add_less_cancel_right gr_s gr_t gt_chop gt_imp_vars ih size_chop_lt subset_empty)
+    by (metis add_less_cancel_right gr_s gr_t gt_chop gt_imp_vars ih hsize_chop_lt subset_empty)
   moreover
   {
     assume
       chkembs_t_s: "chkchop (>\<^sub>t) t s" and
       chkembs_s_t: "chkchop (>\<^sub>t) s t"
 
     obtain g where g: "head t = Sym g"
       using gr_t by (metis ground_head hd.collapse(2))
     obtain f where f: "head s = Sym f"
       using gr_s by (metis ground_head hd.collapse(2))
 
     {
       assume g_gt_f: "g >\<^sub>s f"
       have "t >\<^sub>t s"
         using chkembs_t_s f g g_gt_f gt_diff gt_sym_imp_hd by auto
     }
     moreover
     {
       assume f_gt_g: "f >\<^sub>s g"
       have "s >\<^sub>t t" 
         using chkembs_s_t f f_gt_g g gt_diff gt_sym_imp_hd by auto
     }
     moreover
     {
       assume g_eq_f: "g = f"
       hence hd_t: "head t = head s"
         using g f by auto
 
       let ?ts = "args t"
       let ?ss = "args s"
 
       have gr_ts: "\<forall>ta \<in> set ?ts. ground ta"
         using ground_args[OF _ gr_t] by blast
       have gr_ss: "\<forall>sa \<in> set ?ss. ground sa"
         using ground_args[OF _ gr_s] by blast
 
       {
         assume ts_eq_ss: "?ts = ?ss"
         have "t = s"
           using hd_t ts_eq_ss by (rule tm_expand_apps)
       }
       moreover
       {
         assume ts_gt_ss: "extf g (>\<^sub>t) ?ts ?ss"
         have "t >\<^sub>t s"
           using chkembs_t_s g gt_same hd_t ts_gt_ss by auto
       }
       moreover
       {
         assume ss_gt_ts: "extf g (>\<^sub>t) ?ss ?ts"
         have "s >\<^sub>t t"
           using chkembs_s_t f g_eq_f gt_same hd_t ss_gt_ts by auto
       }
       ultimately have ?case
         using ih gr_ss gr_ts
           ext_total.total[OF extf_total, rule_format, of "set ?ts" "set ?ss" "(>\<^sub>t)" ?ts ?ss g]
-        by (metis add_strict_mono in_listsI size_in_args)
+        by (metis add_strict_mono in_listsI hsize_in_args)
     }
     ultimately have ?case
       using gt_sym_total by blast
   }
   ultimately show ?case
     by fast
 qed
 
 subsection \<open>Well-foundedness\<close>
 
 abbreviation gtg :: "('s, 'v) tm \<Rightarrow> ('s, 'v) tm \<Rightarrow> bool" (infix ">\<^sub>t\<^sub>g" 50) where
   "(>\<^sub>t\<^sub>g) \<equiv> \<lambda>t s. ground t \<and> t >\<^sub>t s"
 
 theorem gt_wf:
   assumes ghd_UNIV: "\<And>x. ground_heads_var x = UNIV"
   assumes extf_wf: "\<And>f. ext_wf (extf f)"
   shows "wfP (\<lambda>s t. t >\<^sub>t s)"
 proof -
   have ground_wfP: "wfP (\<lambda>s t. t >\<^sub>t\<^sub>g s)"
     unfolding wfP_iff_no_inf_chain
   proof
     assume "\<exists>f. inf_chain (>\<^sub>t\<^sub>g) f"
     then obtain t where t_bad: "bad (>\<^sub>t\<^sub>g) t"
       unfolding inf_chain_def bad_def by blast
 
-    let ?ff = "worst_chain (>\<^sub>t\<^sub>g) (\<lambda>t s. size t > size s)"
+    let ?ff = "worst_chain (>\<^sub>t\<^sub>g) (\<lambda>t s. hsize t > hsize s)"
     let ?U_of = "\<lambda>i. {u. (?ff i) \<rhd>\<^sub>e\<^sub>m\<^sub>b u}"
 
-    note wf_sz = wf_app[OF wellorder_class.wf, of size, simplified]
+    note wf_sz = wf_app[OF wellorder_class.wf, of hsize, simplified]
 
     define U where "U = (\<Union>i. ?U_of i)"
 
     have gr: "\<And>i. ground (?ff i)"
       using worst_chain_bad[OF wf_sz t_bad, unfolded inf_chain_def] by fast
     have gr_u: "\<And>u. u \<in> U \<Longrightarrow> ground u" unfolding U_def
       using gr ground_emb by fastforce
 
     have "\<not> bad (>\<^sub>t\<^sub>g) u" if u_in: "u \<in> ?U_of i" for u i
     proof
       let ?ti = "?ff i"
 
       assume u_bad: "bad (>\<^sub>t\<^sub>g) u"
-      have sz_u: "size u < size ?ti"
-        using emb_size_neq u_in by blast
+      have sz_u: "hsize u < hsize ?ti"
+        using emb_hsize_neq u_in by blast
 
       show False
       proof (cases i)
         case 0
         thus False
           using sz_u min_worst_chain_0[OF wf_sz u_bad] by simp
       next
         case Suc
         hence "?ff (i - 1) >\<^sub>t ?ff i"
           using worst_chain_pred[OF wf_sz t_bad] by simp
         moreover have "?ff i >\<^sub>t u"
           using gt_embedding_property u_in by blast
         ultimately have "?ff (i - 1) >\<^sub>t u"
           by (rule gt_trans)
         thus False
           using Suc sz_u min_worst_chain_Suc[OF wf_sz u_bad] gr by fastforce
       qed
     qed
     hence u_good: "\<And>u. u \<in> U \<Longrightarrow> \<not> bad (>\<^sub>t\<^sub>g) u"
       unfolding U_def by blast
 
     have bad_diff_same: "inf_chain (\<lambda>t s. ground t \<and> (gt_diff t s \<or> gt_same t s)) ?ff"
       unfolding inf_chain_def
     proof (intro allI conjI)
       fix i
 
       show "ground (?ff i)"
         by (rule gr)
 
       have gt: "?ff i >\<^sub>t ?ff (Suc i)"
         using worst_chain_pred[OF wf_sz t_bad] by blast
 
       have "\<not> gt_chop (?ff i) (?ff (Suc i))" 
       proof
         assume a: "gt_chop (?ff i) (?ff (Suc i))"
         then have "chop (?ff i) \<in> ?U_of i" 
           by (metis (mono_tags, lifting) emb_step_chop emb_step_is_emb gt_chop gt_chop.cases gt_irrefl mem_Collect_eq)
         then have  uij_in:"chop (?ff i) \<in> U" unfolding U_def by fast
 
         have "\<And>n. ?ff n >\<^sub>t ?ff (Suc n)"
           by (rule worst_chain_pred[OF wf_sz t_bad, THEN conjunct2])
         hence uij_gt_i_plus_3: "chop (?ff i) >\<^sub>t ?ff (Suc (Suc i))"
           using gt_trans by (metis (mono_tags, lifting) a gt_chop.cases)
 
         have "inf_chain (>\<^sub>t\<^sub>g) (\<lambda>j. if j = 0 then chop (?ff i) else ?ff (Suc (i + j)))"
           unfolding inf_chain_def
           by (auto intro!: gr gr_u[OF uij_in] uij_gt_i_plus_3 worst_chain_pred[OF wf_sz t_bad])
         hence "bad (>\<^sub>t\<^sub>g) (chop (?ff i))"
           unfolding bad_def by fastforce
         thus False
           using u_good[OF uij_in] by sat
       qed
       thus "gt_diff (?ff i) (?ff (Suc i)) \<or> gt_same (?ff i) (?ff (Suc i))"
         using gt unfolding gt_iff_chop_diff_same by sat
     qed
 
     have "wf {(s, t). ground s \<and> ground t \<and> sym (head t) >\<^sub>s sym (head s)}"
       using gt_sym_wf unfolding wfP_def wf_iff_no_infinite_down_chain by fast
     moreover have "{(s, t). ground t \<and> gt_diff t s}
       \<subseteq> {(s, t). ground s \<and> ground t \<and> sym (head t) >\<^sub>s sym (head s)}"
     proof (clarsimp, intro conjI)
       fix s t
       assume gr_t: "ground t" and gt_diff_t_s: "gt_diff t s"
       thus gr_s: "ground s"
         using gt_iff_chop_diff_same gt_imp_vars by fastforce
 
       show "sym (head t) >\<^sub>s sym (head s)"
         using gt_diff_t_s ground_head[OF gr_s] ground_head[OF gr_t]
         by (cases; cases "head s"; cases "head t") (auto simp: gt_hd_def)
     qed
     ultimately have wf_diff: "wf {(s, t). ground t \<and> gt_diff t s}"
       by (rule wf_subset)
 
     have diff_O_same: "{(s, t). ground t \<and> gt_diff t s} O {(s, t). ground t \<and> gt_same t s}
       \<subseteq> {(s, t). ground t \<and> gt_diff t s}"
       unfolding gt_diff.simps gt_same.simps
       by clarsimp (metis chkchop_def chkchop_same_def gt_same gt_trans)
 
     have diff_same_as_union: "{(s, t). ground t \<and> (gt_diff t s \<or> gt_same t s)} =
       {(s, t). ground t \<and> gt_diff t s} \<union> {(s, t). ground t \<and> gt_same t s}"
       by auto
 
     obtain k where bad_same: "inf_chain (\<lambda>t s. ground t \<and> gt_same t s) (\<lambda>i. ?ff (i + k))"
       using wf_infinite_down_chain_compatible[OF wf_diff _ diff_O_same, of ?ff] bad_diff_same
       unfolding inf_chain_def diff_same_as_union[symmetric] by auto
     hence hd_sym: "\<And>i. is_Sym (head (?ff (i + k)))"
       unfolding inf_chain_def by (simp add: ground_head)
 
     define f where "f = sym (head (?ff k))"
 
     have hd_eq_f: "head (?ff (i + k)) = Sym f" for i
     proof (induct i)
       case 0
       thus ?case
         by (auto simp: f_def hd.collapse(2)[OF hd_sym, of 0, simplified])
     next
       case (Suc ia)
       thus ?case
         using bad_same unfolding inf_chain_def gt_same.simps by simp
     qed
 
     let ?gtu = "\<lambda>t s. t \<in> U \<and> t >\<^sub>t s"
     thm UnionI CollectI
     have "t \<in> set (args (?ff i)) \<Longrightarrow> t \<in> U" for t i
       unfolding U_def apply (rule UnionI[of "?U_of i"]) 
-      using arg_emb CollectI arg_emb size_in_args by fast+
+      using arg_emb CollectI arg_emb hsize_in_args by fast+
     moreover have "\<And>i. extf f (>\<^sub>t\<^sub>g) (args (?ff (i + k))) (args (?ff (Suc i + k)))"
       using bad_same hd_eq_f unfolding  inf_chain_def gt_same.simps f_def hd.collapse(2)[OF ground_head, OF gr]
       using extf_mono_strong[of _ _ "(>\<^sub>t)" "(\<lambda>t s. ground t \<and> t >\<^sub>t s)" ] ground_hd_in_ground_heads 
       by (metis (no_types, lifting) ground_args)
     ultimately have "\<And>i. extf f ?gtu (args (?ff (i + k))) (args (?ff (Suc i + k)))"
       using extf_mono_strong[of _ _ "(\<lambda>t s. ground t \<and> t >\<^sub>t s)" "\<lambda>t s. t \<in> U \<and> t >\<^sub>t s"] unfolding U_def by blast
     hence "inf_chain (extf f ?gtu) (\<lambda>i. args (?ff (i + k)))"
       unfolding inf_chain_def by blast
     hence nwf_ext: "\<not> wfP (\<lambda>xs ys. extf f ?gtu ys xs)"
       unfolding wfP_iff_no_inf_chain by fast
 
     have gtu_le_gtg: "?gtu \<le> (>\<^sub>t\<^sub>g)"
       by (auto intro!: gr_u)
 
     have "wfP (\<lambda>s t. ?gtu t s)"
       unfolding wfP_iff_no_inf_chain
     proof (intro notI, elim exE)
       fix f
       assume bad_f: "inf_chain ?gtu f"
       hence bad_f0: "bad ?gtu (f 0)"
         by (rule inf_chain_bad)
 
       have "f 0 \<in> U"
         using bad_f unfolding inf_chain_def by blast
       hence good_f0: "\<not> bad ?gtu (f 0)"
         using u_good bad_f inf_chain_bad inf_chain_subset[OF _ gtu_le_gtg] by blast
 
       show False
         using bad_f0 good_f0 by sat
     qed
     hence wf_ext: "wfP (\<lambda>xs ys. extf f ?gtu ys xs)"
       by (rule ext_wf.wf[OF extf_wf, rule_format])
 
     show False
       using nwf_ext wf_ext by blast
   qed
 
   let ?subst = "subst grounding_\<rho>"
 
   have "wfP (\<lambda>s t. ?subst t >\<^sub>t\<^sub>g ?subst s)"
     by (rule wfP_app[OF ground_wfP])
   hence "wfP (\<lambda>s t. ?subst t >\<^sub>t ?subst s)"
     by (simp add: ground_grounding_\<rho>)
   thus ?thesis
     using gt_sus ghd_UNIV ground_heads.simps(1) wary_grounding_\<rho> wfP_eq_minimal
     by (metis (no_types, lifting))
 qed
 
 end
 
 end
diff --git a/thys/Lambda_Free_RPOs/Lambda_Free_Term.thy b/thys/Lambda_Free_RPOs/Lambda_Free_Term.thy
--- a/thys/Lambda_Free_RPOs/Lambda_Free_Term.thy
+++ b/thys/Lambda_Free_RPOs/Lambda_Free_Term.thy
@@ -1,565 +1,597 @@
 (*  Title:       Lambda-Free Higher-Order Terms
     Author:      Jasmin Blanchette <jasmin.blanchette at inria.fr>, 2016
     Maintainer:  Jasmin Blanchette <jasmin.blanchette at inria.fr>
 *)
 
 section \<open>Lambda-Free Higher-Order Terms\<close>
 
 theory Lambda_Free_Term
 imports Lambda_Free_Util
 abbrevs ">s" = ">\<^sub>s"
   and ">h" = ">\<^sub>h\<^sub>d"
   and "\<le>\<ge>h" = "\<le>\<ge>\<^sub>h\<^sub>d"
 begin
 
 text \<open>
 This theory defines \<open>\<lambda>\<close>-free higher-order terms and related locales.
 \<close>
 
 
 subsection \<open>Precedence on Symbols\<close>
 
 locale gt_sym =
   fixes
     gt_sym :: "'s \<Rightarrow> 's \<Rightarrow> bool" (infix ">\<^sub>s" 50)
   assumes
     gt_sym_irrefl: "\<not> f >\<^sub>s f" and
     gt_sym_trans: "h >\<^sub>s g \<Longrightarrow> g >\<^sub>s f \<Longrightarrow> h >\<^sub>s f" and
     gt_sym_total: "f >\<^sub>s g \<or> g >\<^sub>s f \<or> g = f" and
     gt_sym_wf: "wfP (\<lambda>f g. g >\<^sub>s f)"
 begin
 
 lemma gt_sym_antisym: "f >\<^sub>s g \<Longrightarrow> \<not> g >\<^sub>s f"
   by (metis gt_sym_irrefl gt_sym_trans)
 
 end
 
 subsection \<open>Heads\<close>
 
 datatype (plugins del: size) (syms_hd: 's, vars_hd: 'v) hd =
   is_Var: Var (var: 'v)
 | Sym (sym: 's)
 
 abbreviation is_Sym :: "('s, 'v) hd \<Rightarrow> bool" where
   "is_Sym \<zeta> \<equiv> \<not> is_Var \<zeta>"
 
 lemma finite_vars_hd[simp]: "finite (vars_hd \<zeta>)"
   by (cases \<zeta>) auto
 
 lemma finite_syms_hd[simp]: "finite (syms_hd \<zeta>)"
   by (cases \<zeta>) auto
 
 
 subsection \<open>Terms\<close>
 
 consts head0 :: 'a
 
 datatype (syms: 's, vars: 'v) tm =
   is_Hd: Hd (head: "('s, 'v) hd")
 | App ("fun": "('s, 'v) tm") (arg: "('s, 'v) tm")
 where
   "head (App s _) = head0 s"
 | "fun (Hd \<zeta>) = Hd \<zeta>"
 | "arg (Hd \<zeta>) = Hd \<zeta>"
 
 overloading head0 \<equiv> "head0 :: ('s, 'v) tm \<Rightarrow> ('s, 'v) hd"
 begin
 
 primrec head0 :: "('s, 'v) tm \<Rightarrow> ('s, 'v) hd" where
   "head0 (Hd \<zeta>) = \<zeta>"
 | "head0 (App s _) = head0 s"
 
 end
 
 lemma head_App[simp]: "head (App s t) = head s"
   by (cases s) auto
 
 declare tm.sel(2)[simp del]
 
 lemma head_fun[simp]: "head (fun s) = head s"
   by (cases s) auto
 
 abbreviation ground :: "('s, 'v) tm \<Rightarrow> bool" where
   "ground t \<equiv> vars t = {}"
 
 abbreviation is_App :: "('s, 'v) tm \<Rightarrow> bool" where
   "is_App s \<equiv> \<not> is_Hd s"
 
 lemma
   size_fun_lt: "is_App s \<Longrightarrow> size (fun s) < size s" and
   size_arg_lt: "is_App s \<Longrightarrow> size (arg s) < size s"
   by (cases s; simp)+
 
 lemma
   finite_vars[simp]: "finite (vars s)" and
   finite_syms[simp]: "finite (syms s)"
   by (induct s) auto
 
 lemma
   vars_head_subseteq: "vars_hd (head s) \<subseteq> vars s" and
   syms_head_subseteq: "syms_hd (head s) \<subseteq> syms s"
   by (induct s) auto
 
 fun args :: "('s, 'v) tm \<Rightarrow> ('s, 'v) tm list" where
   "args (Hd _) = []"
 | "args (App s t) = args s @ [t]"
 
 lemma set_args_fun: "set (args (fun s)) \<subseteq> set (args s)"
   by (cases s) auto
 
 lemma arg_in_args: "is_App s \<Longrightarrow> arg s \<in> set (args s)"
   by (cases s rule: tm.exhaust) auto
 
 lemma
   vars_args_subseteq: "si \<in> set (args s) \<Longrightarrow> vars si \<subseteq> vars s" and
   syms_args_subseteq: "si \<in> set (args s) \<Longrightarrow> syms si \<subseteq> syms s"
   by (induct s) auto
 
 lemma args_Nil_iff_is_Hd: "args s = [] \<longleftrightarrow> is_Hd s"
   by (cases s) auto
 
 abbreviation num_args :: "('s, 'v) tm \<Rightarrow> nat" where
   "num_args s \<equiv> length (args s)"
 
 lemma size_ge_num_args: "size s \<ge> num_args s"
   by (induct s) auto
 
 lemma Hd_head_id: "num_args s = 0 \<Longrightarrow> Hd (head s) = s"
   by (metis args.cases args.simps(2) length_0_conv snoc_eq_iff_butlast tm.collapse(1) tm.disc(1))
 
 lemma one_arg_imp_Hd: "num_args s = 1 \<Longrightarrow> s = App t u \<Longrightarrow> t = Hd (head t)"
   by (simp add: Hd_head_id)
 
 lemma size_in_args: "s \<in> set (args t) \<Longrightarrow> size s < size t"
   by (induct t) auto
 
 primrec apps :: "('s, 'v) tm \<Rightarrow> ('s, 'v) tm list \<Rightarrow> ('s, 'v) tm" where
   "apps s [] = s"
 | "apps s (t # ts) = apps (App s t) ts"
 
 lemma
   vars_apps[simp]: "vars (apps s ss) = vars s \<union> (\<Union>s \<in> set ss. vars s)" and
   syms_apps[simp]: "syms (apps s ss) = syms s \<union> (\<Union>s \<in> set ss. syms s)" and
   head_apps[simp]: "head (apps s ss) = head s" and
   args_apps[simp]: "args (apps s ss) = args s @ ss" and
   is_App_apps[simp]: "is_App (apps s ss) \<longleftrightarrow> args (apps s ss) \<noteq> []" and
   fun_apps_Nil[simp]: "fun (apps s []) = fun s" and
   fun_apps_Cons[simp]: "fun (apps (App s sa) ss) = apps s (butlast (sa # ss))" and
   arg_apps_Nil[simp]: "arg (apps s []) = arg s" and
   arg_apps_Cons[simp]: "arg (apps (App s sa) ss) = last (sa # ss)"
   by (induct ss arbitrary: s sa) (auto simp: args_Nil_iff_is_Hd)
 
 lemma apps_append[simp]: "apps s (ss @ ts) = apps (apps s ss) ts"
   by (induct ss arbitrary: s ts) auto
 
 lemma App_apps: "App (apps s ts) t = apps s (ts @ [t])"
   by simp
 
 lemma tm_inject_apps[iff, induct_simp]: "apps (Hd \<zeta>) ss = apps (Hd \<xi>) ts \<longleftrightarrow> \<zeta> = \<xi> \<and> ss = ts"
   by (metis args_apps head_apps same_append_eq tm.sel(1))
 
 lemma tm_collapse_apps[simp]: "apps (Hd (head s)) (args s) = s"
   by (induct s) auto
 
 lemma tm_expand_apps: "head s = head t \<Longrightarrow> args s = args t \<Longrightarrow> s = t"
   by (metis tm_collapse_apps)
 
 lemma tm_exhaust_apps_sel[case_names apps]: "(s = apps (Hd (head s)) (args s) \<Longrightarrow> P) \<Longrightarrow> P"
   by (atomize_elim, induct s) auto
 
 lemma tm_exhaust_apps[case_names apps]: "(\<And>\<zeta> ss. s = apps (Hd \<zeta>) ss \<Longrightarrow> P) \<Longrightarrow> P"
   by (metis tm_collapse_apps)
 
 lemma tm_induct_apps[case_names apps]:
   assumes "\<And>\<zeta> ss. (\<And>s. s \<in> set ss \<Longrightarrow> P s) \<Longrightarrow> P (apps (Hd \<zeta>) ss)"
   shows "P s"
   using assms
   by (induct s taking: size rule: measure_induct_rule) (metis size_in_args tm_collapse_apps)
 
 lemma
   ground_fun: "ground s \<Longrightarrow> ground (fun s)" and
   ground_arg: "ground s \<Longrightarrow> ground (arg s)"
   by (induct s) auto
 
 lemma ground_head: "ground s \<Longrightarrow> is_Sym (head s)"
   by (cases s rule: tm_exhaust_apps) (auto simp: is_Var_def)
 
 lemma ground_args: "t \<in> set (args s) \<Longrightarrow> ground s \<Longrightarrow> ground t"
   by (induct s rule: tm_induct_apps) auto
 
 primrec vars_mset :: "('s, 'v) tm \<Rightarrow> 'v multiset" where
   "vars_mset (Hd \<zeta>) = mset_set (vars_hd \<zeta>)"
 | "vars_mset (App s t) = vars_mset s + vars_mset t"
 
 lemma set_vars_mset[simp]: "set_mset (vars_mset t) = vars t"
   by (induct t) auto
 
 lemma vars_mset_empty_iff[iff]: "vars_mset s = {#} \<longleftrightarrow> ground s"
   by (induct s) (auto simp: mset_set_empty_iff)
 
 lemma vars_mset_fun[intro]: "vars_mset (fun t) \<subseteq># vars_mset t"
   by (cases t) auto
 
 lemma vars_mset_arg[intro]: "vars_mset (arg t) \<subseteq># vars_mset t"
   by (cases t) auto
 
 
+subsection \<open>hsize\<close>
+
+text \<open>The hsize of a term is the number of heads (Syms or Vars) in a term.\<close>
+
+primrec hsize :: "('s, 'v) tm \<Rightarrow> nat" where
+  "hsize (Hd \<zeta>) = 1"
+| "hsize (App s t) = hsize s + hsize t"
+
+lemma hsize_size: "hsize t * 2 = size t + 1"
+  by (induct t) auto
+
+lemma hsize_pos[simp]: "hsize t > 0"
+  by (induction t; simp)
+
+lemma hsize_fun_lt: "is_App s \<Longrightarrow> hsize (fun s) < hsize s"
+  by (cases s; simp)
+
+lemma hsize_arg_lt: "is_App s \<Longrightarrow> hsize (arg s) < hsize s"
+  by (cases s; simp)
+  
+lemma hsize_ge_num_args: "hsize s \<ge> hsize s"
+  by (induct s) auto
+
+lemma hsize_in_args: "s \<in> set (args t) \<Longrightarrow> hsize s < hsize t"
+  by (induct t) auto
+
+lemma hsize_apps: "hsize (apps t ts) = hsize t + sum_list (map hsize ts)"
+  by (induct ts arbitrary:t; simp)
+
+lemma hsize_args: "1 + sum_list (map hsize (args t)) = hsize t"
+  by (metis hsize.simps(1) hsize_apps tm_collapse_apps)
+
 subsection \<open>Substitutions\<close>
 
 primrec subst :: "('v \<Rightarrow> ('s, 'v) tm) \<Rightarrow> ('s, 'v) tm \<Rightarrow> ('s, 'v) tm" where
   "subst \<rho> (Hd \<zeta>) = (case \<zeta> of Var x \<Rightarrow> \<rho> x | Sym f \<Rightarrow> Hd (Sym f))"
 | "subst \<rho> (App s t) = App (subst \<rho> s) (subst \<rho> t)"
 
 lemma subst_apps[simp]: "subst \<rho> (apps s ts) = apps (subst \<rho> s) (map (subst \<rho>) ts)"
   by (induct ts arbitrary: s) auto
 
 lemma head_subst[simp]: "head (subst \<rho> s) = head (subst \<rho> (Hd (head s)))"
   by (cases s rule: tm_exhaust_apps) (auto split: hd.split)
 
 lemma args_subst[simp]:
   "args (subst \<rho> s) = (case head s of Var x \<Rightarrow> args (\<rho> x) | Sym f \<Rightarrow> []) @ map (subst \<rho>) (args s)"
   by (cases s rule: tm_exhaust_apps) (auto split: hd.split)
 
 lemma ground_imp_subst_iden: "ground s \<Longrightarrow> subst \<rho> s = s"
   by (induct s) (auto split: hd.split)
 
 lemma vars_mset_subst[simp]: "vars_mset (subst \<rho> s) = (\<Union># {#vars_mset (\<rho> x). x \<in># vars_mset s#})"
 proof (induct s)
   case (Hd \<zeta>)
   show ?case
     by (cases \<zeta>) auto
 qed auto
 
 lemma vars_mset_subst_subseteq:
   "vars_mset t \<supseteq># vars_mset s \<Longrightarrow> vars_mset (subst \<rho> t) \<supseteq># vars_mset (subst \<rho> s)"
   unfolding vars_mset_subst
   by (metis (no_types) add_diff_cancel_right' diff_subset_eq_self image_mset_union sum_mset.union
     subset_mset.add_diff_inverse)
 
 lemma vars_subst_subseteq: "vars t \<supseteq> vars s \<Longrightarrow> vars (subst \<rho> t) \<supseteq> vars (subst \<rho> s)"
   unfolding set_vars_mset[symmetric] vars_mset_subst by auto
 
 
 subsection \<open>Subterms\<close>
 
 inductive sub :: "('s, 'v) tm \<Rightarrow> ('s, 'v) tm \<Rightarrow> bool" where
   sub_refl: "sub s s"
 | sub_fun: "sub s t \<Longrightarrow> sub s (App u t)"
 | sub_arg: "sub s t \<Longrightarrow> sub s (App t u)"
 
 inductive_cases sub_HdE[simplified, elim]: "sub s (Hd \<xi>)"
 inductive_cases sub_AppE[simplified, elim]: "sub s (App t u)"
 inductive_cases sub_Hd_HdE[simplified, elim]: "sub (Hd \<zeta>) (Hd \<xi>)"
 inductive_cases sub_Hd_AppE[simplified, elim]: "sub (Hd \<zeta>) (App t u)"
 
 lemma in_vars_imp_sub: "x \<in> vars s \<longleftrightarrow> sub (Hd (Var x)) s"
   by induct (auto intro: sub.intros elim: hd.set_cases(2))
 
 lemma sub_args: "s \<in> set (args t) \<Longrightarrow> sub s t"
   by (induct t) (auto intro: sub.intros)
 
 lemma sub_size: "sub s t \<Longrightarrow> size s \<le> size t"
   by induct auto
 
 lemma sub_subst: "sub s t \<Longrightarrow> sub (subst \<rho> s) (subst \<rho> t)"
 proof (induct t)
   case (Hd \<zeta>)
   thus ?case
     by (cases \<zeta>; blast intro: sub.intros)
 qed (auto intro: sub.intros del: sub_AppE elim!: sub_AppE)
 
 abbreviation proper_sub :: "('s, 'v) tm \<Rightarrow> ('s, 'v) tm \<Rightarrow> bool" where
   "proper_sub s t \<equiv> sub s t \<and> s \<noteq> t"
 
 lemma proper_sub_Hd[simp]: "\<not> proper_sub s (Hd \<zeta>)"
   using sub.cases by blast
 
 lemma proper_sub_subst:
   assumes psub: "proper_sub s t"
   shows "proper_sub (subst \<rho> s) (subst \<rho> t)"
 proof (cases t)
   case Hd
   thus ?thesis
     using psub by simp
 next
   case t: (App t1 t2)
   have "sub s t1 \<or> sub s t2"
     using t psub by blast
   hence "sub (subst \<rho> s) (subst \<rho> t1) \<or> sub (subst \<rho> s) (subst \<rho> t2)"
     using sub_subst by blast
   thus ?thesis
     unfolding t by (auto intro: sub.intros dest: sub_size)
 qed
 
 
 subsection \<open>Maximum Arities\<close>
 
 locale arity =
   fixes
     arity_sym :: "'s \<Rightarrow> enat" and
     arity_var :: "'v \<Rightarrow> enat"
 begin
 
 primrec arity_hd :: "('s, 'v) hd \<Rightarrow> enat" where
   "arity_hd (Var x) = arity_var x"
 | "arity_hd (Sym f) = arity_sym f"
 
 definition arity :: "('s, 'v) tm \<Rightarrow> enat" where
   "arity s = arity_hd (head s) - num_args s"
 
 lemma arity_simps[simp]:
   "arity (Hd \<zeta>) = arity_hd \<zeta>"
   "arity (App s t) = arity s - 1"
   by (auto simp: arity_def enat_diff_diff_eq add.commute eSuc_enat plus_1_eSuc(1))
 
 lemma arity_apps[simp]: "arity (apps s ts) = arity s - length ts"
 proof (induct ts arbitrary: s)
   case (Cons t ts)
   thus ?case
     by (case_tac "arity s"; simp add: one_enat_def)
 qed simp
 
 inductive wary :: "('s, 'v) tm \<Rightarrow> bool" where
   wary_Hd[intro]: "wary (Hd \<zeta>)"
 | wary_App[intro]: "wary s \<Longrightarrow> wary t \<Longrightarrow> num_args s < arity_hd (head s) \<Longrightarrow> wary (App s t)"
 
 inductive_cases wary_HdE: "wary (Hd \<zeta>)"
 inductive_cases wary_AppE: "wary (App s t)"
 inductive_cases wary_binaryE[simplified]: "wary (App (App s t) u)"
 
 lemma wary_fun[intro]: "wary t \<Longrightarrow> wary (fun t)"
   by (cases t) (auto elim: wary.cases)
 
 lemma wary_arg[intro]: "wary t \<Longrightarrow> wary (arg t)"
   by (cases t) (auto elim: wary.cases)
 
 lemma wary_args: "s \<in> set (args t) \<Longrightarrow> wary t \<Longrightarrow> wary s"
   by (induct t arbitrary: s, simp)
    (metis Un_iff args.simps(2) wary.cases insert_iff length_pos_if_in_set
       less_numeral_extra(3) list.set(2) list.size(3) set_append tm.distinct(1) tm.inject(2))
 
 lemma wary_sub: "sub s t \<Longrightarrow> wary t \<Longrightarrow> wary s"
   by (induct rule: sub.induct) (auto elim: wary.cases)
 
 lemma wary_inf_ary: "(\<And>\<zeta>. arity_hd \<zeta> = \<infinity>) \<Longrightarrow> wary s"
   by induct auto
 
 lemma wary_num_args_le_arity_head: "wary s \<Longrightarrow> num_args s \<le> arity_hd (head s)"
   by (induct rule: wary.induct) (auto simp: zero_enat_def[symmetric] Suc_ile_eq)
 
 lemma wary_apps:
   "wary s \<Longrightarrow> (\<And>sa. sa \<in> set ss \<Longrightarrow> wary sa) \<Longrightarrow> length ss \<le> arity s \<Longrightarrow> wary (apps s ss)"
 proof (induct ss arbitrary: s)
   case (Cons sa ss)
   note ih = this(1) and wary_s = this(2) and wary_ss = this(3) and nargs_s_sa_ss = this(4)
   show ?case
     unfolding apps.simps
   proof (rule ih)
     have "wary sa"
       using wary_ss by simp
     moreover have " enat (num_args s) < arity_hd (head s)"
       by (metis (mono_tags) One_nat_def add.comm_neutral arity_def diff_add_zero enat_ord_simps(1)
         idiff_enat_enat less_one list.size(4) nargs_s_sa_ss not_add_less2
         order.not_eq_order_implies_strict wary_num_args_le_arity_head wary_s)
     ultimately show "wary (App s sa)"
       by (rule wary_App[OF wary_s])
   next
     show "\<And>sa. sa \<in> set ss \<Longrightarrow> wary sa"
       using wary_ss by simp
   next
     show "length ss \<le> arity (App s sa)"
     proof (cases "arity s")
       case enat
       thus ?thesis
         using nargs_s_sa_ss by (simp add: one_enat_def)
     qed simp
   qed
 qed simp
 
 lemma wary_cases_apps[consumes 1, case_names apps]:
   assumes
     wary_t: "wary t" and
     apps: "\<And>\<zeta> ss. t = apps (Hd \<zeta>) ss \<Longrightarrow> (\<And>sa. sa \<in> set ss \<Longrightarrow> wary sa) \<Longrightarrow> length ss \<le> arity_hd \<zeta> \<Longrightarrow> P"
   shows P
   using apps
 proof (atomize_elim, cases t rule: tm_exhaust_apps)
   case t: (apps \<zeta> ss)
   show "\<exists>\<zeta> ss. t = apps (Hd \<zeta>) ss \<and> (\<forall>sa. sa \<in> set ss \<longrightarrow> wary sa) \<and> enat (length ss) \<le> arity_hd \<zeta>"
     by (rule exI[of _ \<zeta>], rule exI[of _ ss])
       (auto simp: t wary_args[OF _ wary_t] wary_num_args_le_arity_head[OF wary_t, unfolded t, simplified])
 qed
 
 lemma arity_hd_head: "wary s \<Longrightarrow> arity_hd (head s) = arity s + num_args s"
   by (simp add: arity_def enat_sub_add_same wary_num_args_le_arity_head)
 
 lemma arity_head_ge: "arity_hd (head s) \<ge> arity s"
   by (induct s) (auto intro: enat_le_imp_minus_le)
 
 inductive wary_fo :: "('s, 'v) tm \<Rightarrow> bool" where
   wary_foI[intro]: "is_Hd s \<or> is_Sym (head s) \<Longrightarrow> length (args s) = arity_hd (head s) \<Longrightarrow>
     (\<forall>t \<in> set (args s). wary_fo t) \<Longrightarrow> wary_fo s"
 
 lemma wary_fo_args: "s \<in> set (args t) \<Longrightarrow> wary_fo t \<Longrightarrow> wary_fo s"
   by (induct t arbitrary: s rule: tm_induct_apps, simp)
     (metis args.simps(1) args_apps self_append_conv2 wary_fo.cases)
 
 lemma wary_fo_arg: "wary_fo (App s t) \<Longrightarrow> wary_fo t"
   by (erule wary_fo.cases) auto
 
 end
 
 
 subsection \<open>Potential Heads of Ground Instances of Variables\<close>
 
 locale ground_heads = gt_sym "(>\<^sub>s)" + arity arity_sym arity_var
     for
       gt_sym :: "'s \<Rightarrow> 's \<Rightarrow> bool" (infix ">\<^sub>s" 50) and
       arity_sym :: "'s \<Rightarrow> enat" and
       arity_var :: "'v \<Rightarrow> enat" +
   fixes
     ground_heads_var :: "'v \<Rightarrow> 's set"
   assumes
     ground_heads_var_arity: "f \<in> ground_heads_var x \<Longrightarrow> arity_sym f \<ge> arity_var x" and
     ground_heads_var_nonempty: "ground_heads_var x \<noteq> {}"
 begin
 
 primrec ground_heads :: "('s, 'v) hd \<Rightarrow> 's set" where
   "ground_heads (Var x) = ground_heads_var x"
 | "ground_heads (Sym f) = {f}"
 
 lemma ground_heads_arity: "f \<in> ground_heads \<zeta> \<Longrightarrow> arity_sym f \<ge> arity_hd \<zeta>"
   by (cases \<zeta>) (auto simp: ground_heads_var_arity)
 
 lemma ground_heads_nonempty[simp]: "ground_heads \<zeta> \<noteq> {}"
   by (cases \<zeta>) (auto simp: ground_heads_var_nonempty)
 
 lemma sym_in_ground_heads: "is_Sym \<zeta> \<Longrightarrow> sym \<zeta> \<in> ground_heads \<zeta>"
   by (metis ground_heads.simps(2) hd.collapse(2) hd.set_sel(1) hd.simps(16))
 
 lemma ground_hd_in_ground_heads: "ground s \<Longrightarrow> sym (head s) \<in> ground_heads (head s)"
   by (simp add: ground_head sym_in_ground_heads)
 
 lemma some_ground_head_arity: "arity_sym (SOME f. f \<in> ground_heads (Var x)) \<ge> arity_var x"
   by (simp add: ground_heads_var_arity ground_heads_var_nonempty some_in_eq)
 
 definition wary_subst :: "('v \<Rightarrow> ('s, 'v) tm) \<Rightarrow> bool" where
   "wary_subst \<rho> \<longleftrightarrow>
    (\<forall>x. wary (\<rho> x) \<and> arity (\<rho> x) \<ge> arity_var x \<and> ground_heads (head (\<rho> x)) \<subseteq> ground_heads_var x)"
 
 definition strict_wary_subst :: "('v \<Rightarrow> ('s, 'v) tm) \<Rightarrow> bool" where
   "strict_wary_subst \<rho> \<longleftrightarrow>
    (\<forall>x. wary (\<rho> x) \<and> arity (\<rho> x) \<in> {arity_var x, \<infinity>}
     \<and> ground_heads (head (\<rho> x)) \<subseteq> ground_heads_var x)"
 
 lemma strict_imp_wary_subst: "strict_wary_subst \<rho> \<Longrightarrow> wary_subst \<rho>"
   unfolding strict_wary_subst_def wary_subst_def using eq_iff by force
 
 lemma wary_subst_wary:
   assumes wary_\<rho>: "wary_subst \<rho>" and wary_s: "wary s"
   shows "wary (subst \<rho> s)"
   using wary_s
 proof (induct s rule: tm.induct)
   case (App s t)
   note wary_st = this(3)
   from wary_st have wary_s: "wary s"
     by (rule wary_AppE)
   from wary_st have wary_t: "wary t"
     by (rule wary_AppE)
   from wary_st have nargs_s_lt: "num_args s < arity_hd (head s)"
     by (rule wary_AppE)
 
   note wary_\<rho>s = App(1)[OF wary_s]
   note wary_\<rho>t = App(2)[OF wary_t]
 
   note wary_\<rho>x = wary_\<rho>[unfolded wary_subst_def, rule_format, THEN conjunct1]
   note ary_\<rho>x = wary_\<rho>[unfolded wary_subst_def, rule_format, THEN conjunct2]
 
   have "num_args (\<rho> x) + num_args s < arity_hd (head (\<rho> x))" if hd_s: "head s = Var x" for x
   proof -
     have ary_hd_s: "arity_hd (head s) = arity_var x"
       using hd_s arity_hd.simps(1) by presburger
     hence "num_args s \<le> arity (\<rho> x)"
       by (metis (no_types) wary_num_args_le_arity_head ary_\<rho>x dual_order.trans wary_s)
     hence "num_args s + num_args (\<rho> x) \<le> arity_hd (head (\<rho> x))"
       by (metis (no_types) arity_hd_head[OF wary_\<rho>x] add_right_mono plus_enat_simps(1))
     thus ?thesis
       using ary_hd_s by (metis (no_types) add.commute add_diff_cancel_left' ary_\<rho>x arity_def
         idiff_enat_enat leD nargs_s_lt order.not_eq_order_implies_strict)
   qed
   hence nargs_\<rho>s: "num_args (subst \<rho> s) < arity_hd (head (subst \<rho> s))"
     using nargs_s_lt by (auto split: hd.split)
 
   show ?case
     by simp (rule wary_App[OF wary_\<rho>s wary_\<rho>t nargs_\<rho>s])
 qed (auto simp: wary_\<rho>[unfolded wary_subst_def] split: hd.split)
 
 lemmas strict_wary_subst_wary = wary_subst_wary[OF strict_imp_wary_subst]
 
 lemma wary_subst_ground_heads:
   assumes wary_\<rho>: "wary_subst \<rho>"
   shows "ground_heads (head (subst \<rho> s)) \<subseteq> ground_heads (head s)"
 proof (induct s rule: tm_induct_apps)
   case (apps \<zeta> ss)
   show ?case
   proof (cases \<zeta>)
     case x: (Var x)
     thus ?thesis
       using wary_\<rho> wary_subst_def x by auto
   qed auto
 qed
 
 lemmas strict_wary_subst_ground_heads = wary_subst_ground_heads[OF strict_imp_wary_subst]
 
 definition grounding_\<rho> :: "'v \<Rightarrow> ('s, 'v) tm" where
   "grounding_\<rho> x = (let s = Hd (Sym (SOME f. f \<in> ground_heads_var x)) in
      apps s (replicate (the_enat (arity s - arity_var x)) s))"
 
 lemma ground_grounding_\<rho>: "ground (subst grounding_\<rho> s)"
   by (induct s) (auto simp: Let_def grounding_\<rho>_def elim: hd.set_cases(2) split: hd.split)
 
 lemma strict_wary_grounding_\<rho>: "strict_wary_subst grounding_\<rho>"
   unfolding strict_wary_subst_def
 proof (intro allI conjI)
   fix x
 
   define f where "f = (SOME f. f \<in> ground_heads_var x)"
   define s :: "('s, 'v) tm" where "s = Hd (Sym f)"
 
   have wary_s: "wary s"
     unfolding s_def by (rule wary_Hd)
   have ary_s_ge_x: "arity s \<ge> arity_var x"
     unfolding s_def f_def using some_ground_head_arity by simp
   have gr\<rho>_x: "grounding_\<rho> x = apps s (replicate (the_enat (arity s - arity_var x)) s)"
     unfolding grounding_\<rho>_def Let_def f_def[symmetric] s_def[symmetric] by (rule refl)
 
   show "wary (grounding_\<rho> x)"
     unfolding gr\<rho>_x by (auto intro!: wary_s wary_apps[OF wary_s] enat_the_enat_minus_le)
   show "arity (grounding_\<rho> x) \<in> {arity_var x, \<infinity>}"
     unfolding gr\<rho>_x using ary_s_ge_x by (cases "arity s"; cases "arity_var x"; simp)
   show "ground_heads (head (grounding_\<rho> x)) \<subseteq> ground_heads_var x"
     unfolding gr\<rho>_x s_def f_def by (simp add: some_in_eq ground_heads_var_nonempty)
 qed
 
 lemmas wary_grounding_\<rho> = strict_wary_grounding_\<rho>[THEN strict_imp_wary_subst]
 
 definition gt_hd :: "('s, 'v) hd \<Rightarrow> ('s, 'v) hd \<Rightarrow> bool" (infix ">\<^sub>h\<^sub>d" 50) where
   "\<xi> >\<^sub>h\<^sub>d \<zeta> \<longleftrightarrow> (\<forall>g \<in> ground_heads \<xi>. \<forall>f \<in> ground_heads \<zeta>. g >\<^sub>s f)"
 
 definition comp_hd :: "('s, 'v) hd \<Rightarrow> ('s, 'v) hd \<Rightarrow> bool" (infix "\<le>\<ge>\<^sub>h\<^sub>d" 50) where
   "\<xi> \<le>\<ge>\<^sub>h\<^sub>d \<zeta> \<longleftrightarrow> \<xi> = \<zeta> \<or> \<xi> >\<^sub>h\<^sub>d \<zeta> \<or> \<zeta> >\<^sub>h\<^sub>d \<xi>"
 
 lemma gt_hd_irrefl: "\<not> \<zeta> >\<^sub>h\<^sub>d \<zeta>"
   unfolding gt_hd_def using gt_sym_irrefl by (meson ex_in_conv ground_heads_nonempty)
 
 lemma gt_hd_trans: "\<chi> >\<^sub>h\<^sub>d \<xi> \<Longrightarrow> \<xi> >\<^sub>h\<^sub>d \<zeta> \<Longrightarrow> \<chi> >\<^sub>h\<^sub>d \<zeta>"
   unfolding gt_hd_def using gt_sym_trans by (meson ex_in_conv ground_heads_nonempty)
 
 lemma gt_sym_imp_hd: "g >\<^sub>s f \<Longrightarrow> Sym g >\<^sub>h\<^sub>d Sym f"
   unfolding gt_hd_def by simp
 
 lemma not_comp_hd_imp_Var: "\<not> \<xi> \<le>\<ge>\<^sub>h\<^sub>d \<zeta> \<Longrightarrow> is_Var \<zeta> \<or> is_Var \<xi>"
   using gt_sym_total by (cases \<zeta>; cases \<xi>; auto simp: comp_hd_def gt_hd_def)
 
 end
 
 end