(*
(C) Copyright Andreas Viktor Hess, DTU, 2015-2020

All Rights Reserved.

Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions are
met:

- Redistributions of source code must retain the above copyright
  notice, this list of conditions and the following disclaimer.

- Redistributions in binary form must reproduce the above copyright
  notice, this list of conditions and the following disclaimer in the
  documentation and/or other materials provided with the distribution.

- Neither the name of the copyright holder nor the names of its
  contributors may be used to endorse or promote products
  derived from this software without specific prior written
  permission.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
*)

(*  Title:      Typed_Model.thy
    Author:     Andreas Viktor Hess, DTU
*)

section \<open>The Typed Model\<close>
theory Typed_Model
imports Lazy_Intruder
begin

text \<open>Term types\<close>
type_synonym ('f,'v) term_type = "('f,'v) term"

text \<open>Constructors for term types\<close>
abbreviation (input) TAtom::"'v \<Rightarrow> ('f,'v) term_type" where
  "TAtom a \<equiv> Var a"

abbreviation (input) TComp::"['f, ('f,'v) term_type list] \<Rightarrow> ('f,'v) term_type" where
  "TComp f T \<equiv> Fun f T"


text \<open>
  The typed model extends the intruder model with a typing function \<open>\<Gamma>\<close> that assigns types to terms.
\<close>
locale typed_model = intruder_model arity public Ana
  for arity::"'fun \<Rightarrow> nat"
    and public::"'fun \<Rightarrow> bool"
    and Ana::"('fun,'var) term \<Rightarrow> (('fun,'var) term list \<times> ('fun,'var) term list)"
  +
  fixes \<Gamma>::"('fun,'var) term \<Rightarrow> ('fun,'atom::finite) term_type"
  assumes const_type: "\<And>c. arity c = 0 \<Longrightarrow> \<exists>a. \<forall>T. \<Gamma> (Fun c T) = TAtom a"
    and fun_type: "\<And>f T. arity f > 0 \<Longrightarrow> \<Gamma> (Fun f T) = TComp f (map \<Gamma> T)"
    and infinite_typed_consts: "\<And>a. infinite {c. \<Gamma> (Fun c []) = TAtom a \<and> public c}"
    and \<Gamma>_wf: "\<And>t f T. TComp f T \<sqsubseteq> \<Gamma> t \<Longrightarrow> arity f > 0"
              "\<And>x. wf\<^sub>t\<^sub>r\<^sub>m (\<Gamma> (Var x))"
    and no_private_funs[simp]: "\<And>f. arity f > 0 \<Longrightarrow> public f"
begin

subsection \<open>Definitions\<close>
text \<open>The set of atomic types\<close>
abbreviation "\<TT>\<^sub>a \<equiv> UNIV::('atom set)"

text \<open>Well-typed substitutions\<close>
definition wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t where
  "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma> \<equiv> (\<forall>v. \<Gamma> (Var v) = \<Gamma> (\<sigma> v))"

text \<open>The set of sub-message patterns (SMP)\<close>
inductive_set SMP::"('fun,'var) terms \<Rightarrow> ('fun,'var) terms" for M where
  MP[intro]: "t \<in> M \<Longrightarrow> t \<in> SMP M"
| Subterm[intro]: "\<lbrakk>t \<in> SMP M; t' \<sqsubseteq> t\<rbrakk> \<Longrightarrow> t' \<in> SMP M"
| Substitution[intro]: "\<lbrakk>t \<in> SMP M; wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>; wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<delta>)\<rbrakk> \<Longrightarrow> (t \<cdot> \<delta>) \<in> SMP M"
| Ana[intro]: "\<lbrakk>t \<in> SMP M; Ana t = (K,T); k \<in> set K\<rbrakk> \<Longrightarrow> k \<in> SMP M"

text \<open>
  Type-flaw resistance for sets:
  Unifiable sub-message patterns must have the same type (unless they are variables)
\<close>
definition tfr\<^sub>s\<^sub>e\<^sub>t where
  "tfr\<^sub>s\<^sub>e\<^sub>t M \<equiv> (\<forall>s \<in> SMP M - (Var`\<V>). \<forall>t \<in> SMP M - (Var`\<V>). (\<exists>\<delta>. Unifier \<delta> s t) \<longrightarrow> \<Gamma> s = \<Gamma> t)"

text \<open>
  Type-flaw resistance for strand steps:
  - The terms in a satisfiable equality step must have the same types
  - Inequality steps must satisfy the conditions of the "inequality lemma"\<close>
fun tfr\<^sub>s\<^sub>t\<^sub>p where
  "tfr\<^sub>s\<^sub>t\<^sub>p (Equality a t t') = ((\<exists>\<delta>. Unifier \<delta> t t') \<longrightarrow> \<Gamma> t = \<Gamma> t')"
| "tfr\<^sub>s\<^sub>t\<^sub>p (Inequality X F) = (
      (\<forall>x \<in> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F - set X. \<exists>a. \<Gamma> (Var x) = TAtom a) \<or>
      (\<forall>f T. Fun f T \<in> subterms\<^sub>s\<^sub>e\<^sub>t (trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F) \<longrightarrow> T = [] \<or> (\<exists>s \<in> set T. s \<notin> Var ` set X)))"
| "tfr\<^sub>s\<^sub>t\<^sub>p _ = True"

text \<open>
  Type-flaw resistance for strands:
  - The set of terms in strands must be type-flaw resistant
  - The steps of strands must be type-flaw resistant
\<close>
definition tfr\<^sub>s\<^sub>t where
  "tfr\<^sub>s\<^sub>t S \<equiv> tfr\<^sub>s\<^sub>e\<^sub>t (trms\<^sub>s\<^sub>t S) \<and> list_all tfr\<^sub>s\<^sub>t\<^sub>p S"


subsection \<open>Small Lemmata\<close>
lemma tfr\<^sub>s\<^sub>t\<^sub>p_list_all_alt_def:
  "list_all tfr\<^sub>s\<^sub>t\<^sub>p S \<longleftrightarrow>
    ((\<forall>a t t'. Equality a t t' \<in> set S \<and> (\<exists>\<delta>. Unifier \<delta> t t') \<longrightarrow> \<Gamma> t = \<Gamma> t') \<and>
    (\<forall>X F. Inequality X F \<in> set S \<longrightarrow> 
      (\<forall>x \<in> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F - set X. \<exists>a. \<Gamma> (Var x) = TAtom a)
    \<or> (\<forall>f T. Fun f T \<in> subterms\<^sub>s\<^sub>e\<^sub>t (trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F) \<longrightarrow> T = [] \<or> (\<exists>s \<in> set T. s \<notin> Var ` set X))))"
  (is "?P S \<longleftrightarrow> ?Q S")
proof
  show "?P S \<Longrightarrow> ?Q S"
  proof (induction S)
    case (Cons x S) thus ?case by (cases x) auto
  qed simp

  show "?Q S \<Longrightarrow> ?P S"
  proof (induction S)
    case (Cons x S) thus ?case by (cases x) auto
  qed simp
qed


lemma \<Gamma>_wf': "wf\<^sub>t\<^sub>r\<^sub>m t \<Longrightarrow> wf\<^sub>t\<^sub>r\<^sub>m (\<Gamma> t)"
proof (induction t)
  case (Fun f T)
  hence *: "arity f = length T" "\<And>t. t \<in> set T \<Longrightarrow> wf\<^sub>t\<^sub>r\<^sub>m (\<Gamma> t)" unfolding wf\<^sub>t\<^sub>r\<^sub>m_def by auto
  { assume "arity f = 0" hence ?case using const_type[of f] by auto }
  moreover
  { assume "arity f > 0" hence ?case using fun_type[of f] * by force }
  ultimately show ?case by auto 
qed (metis \<Gamma>_wf(2))

lemma fun_type_inv: assumes "\<Gamma> t = TComp f T" shows "arity f > 0" "public f"
using \<Gamma>_wf(1)[of f T t] assms by simp_all

lemma fun_type_inv_wf: assumes "\<Gamma> t = TComp f T" "wf\<^sub>t\<^sub>r\<^sub>m t" shows "arity f = length T"
using \<Gamma>_wf'[OF assms(2)] assms(1) unfolding wf\<^sub>t\<^sub>r\<^sub>m_def by auto

lemma const_type_inv: "\<Gamma> (Fun c X) = TAtom a \<Longrightarrow> arity c = 0"
by (rule ccontr, simp add: fun_type)

lemma const_type_inv_wf: assumes "\<Gamma> (Fun c X) = TAtom a" and "wf\<^sub>t\<^sub>r\<^sub>m (Fun c X)" shows "X = []"
by (metis assms const_type_inv length_0_conv subtermeqI' wf\<^sub>t\<^sub>r\<^sub>m_def)

lemma const_type': "\<forall>c \<in> \<C>. \<exists>a \<in> \<TT>\<^sub>a. \<forall>X. \<Gamma> (Fun c X) = TAtom a" using const_type by simp
lemma fun_type': "\<forall>f \<in> \<Sigma>\<^sub>f. \<forall>X. \<Gamma> (Fun f X) = TComp f (map \<Gamma> X)" using fun_type by simp

lemma infinite_public_consts[simp]: "infinite {c. public c \<and> arity c = 0}"
proof -
  fix a::'atom
  define A where "A \<equiv> {c. \<Gamma> (Fun c []) = TAtom a \<and> public c}"
  define B where "B \<equiv> {c. public c \<and> arity c = 0}"

  have "arity c = 0" when c: "c \<in> A" for c
    using c const_type_inv unfolding A_def by blast
  hence "A \<subseteq> B" unfolding A_def B_def by blast
  hence "infinite B"
    using infinite_typed_consts[of a, unfolded A_def[symmetric]]
    by (metis infinite_super)
  thus ?thesis unfolding B_def by blast
qed

lemma infinite_fun_syms[simp]:
  "infinite {c. public c \<and> arity c > 0} \<Longrightarrow> infinite \<Sigma>\<^sub>f"
  "infinite \<C>" "infinite \<C>\<^sub>p\<^sub>u\<^sub>b" "infinite (UNIV::'fun set)"
by (metis \<Sigma>\<^sub>f_unfold finite_Collect_conjI,
    metis infinite_public_consts finite_Collect_conjI,
    use infinite_public_consts \<C>pub_unfold in \<open>force simp add: Collect_conj_eq\<close>,
    metis UNIV_I finite_subset subsetI infinite_public_consts(1))

lemma id_univ_proper_subset[simp]: "\<Sigma>\<^sub>f \<subset> UNIV" "(\<exists>f. arity f > 0) \<Longrightarrow> \<C> \<subset> UNIV"
by (metis finite.emptyI inf_top.right_neutral top.not_eq_extremum disjoint_fun_syms
          infinite_fun_syms(2) inf_commute)
   (metis top.not_eq_extremum UNIV_I const_arity_eq_zero less_irrefl)

lemma exists_fun_notin_funs_term: "\<exists>f::'fun. f \<notin> funs_term t"
by (metis UNIV_eq_I finite_fun_symbols infinite_fun_syms(4))

lemma exists_fun_notin_funs_terms:
  assumes "finite M" shows "\<exists>f::'fun. f \<notin> \<Union>(funs_term ` M)"
by (metis assms finite_fun_symbols infinite_fun_syms(4) ex_new_if_finite finite_UN)

lemma exists_notin_funs\<^sub>s\<^sub>t: "\<exists>f. f \<notin> funs\<^sub>s\<^sub>t (S::('fun,'var) strand)"
by (metis UNIV_eq_I finite_funs\<^sub>s\<^sub>t infinite_fun_syms(4))

lemma infinite_typed_consts': "infinite {c. \<Gamma> (Fun c []) = TAtom a \<and> public c \<and> arity c = 0}"
proof -
  { fix c assume "\<Gamma> (Fun c []) = TAtom a" "public c"
    hence "arity c = 0" using const_type[of c] fun_type[of c "[]"] by auto
  } hence "{c. \<Gamma> (Fun c []) = TAtom a \<and> public c \<and> arity c = 0} =
           {c. \<Gamma> (Fun c []) = TAtom a \<and> public c}"
    by auto
  thus "infinite {c. \<Gamma> (Fun c []) = TAtom a \<and> public c \<and> arity c = 0}"
    using infinite_typed_consts[of a] by metis
qed

lemma atypes_inhabited: "\<exists>c. \<Gamma> (Fun c []) = TAtom a \<and> wf\<^sub>t\<^sub>r\<^sub>m (Fun c []) \<and> public c \<and> arity c = 0"
proof -
  obtain c where "\<Gamma> (Fun c []) = TAtom a" "public c" "arity c = 0"
    using infinite_typed_consts'(1)[of a] not_finite_existsD by blast
  thus ?thesis using const_type_inv[OF \<open>\<Gamma> (Fun c []) = TAtom a\<close>] unfolding wf\<^sub>t\<^sub>r\<^sub>m_def by auto
qed

lemma atype_ground_term_ex: "\<exists>t. fv t = {} \<and> \<Gamma> t = TAtom a \<and> wf\<^sub>t\<^sub>r\<^sub>m t"
using atypes_inhabited[of a] by force

lemma fun_type_id_eq: "\<Gamma> (Fun f X) = TComp g Y \<Longrightarrow> f = g"
by (metis const_type fun_type neq0_conv "term.inject"(2) "term.simps"(4))

lemma fun_type_length_eq: "\<Gamma> (Fun f X) = TComp g Y \<Longrightarrow> length X = length Y"
by (metis fun_type fun_type_id_eq fun_type_inv(1) length_map term.inject(2))

lemma type_ground_inhabited: "\<exists>t'. fv t' = {} \<and> \<Gamma> t = \<Gamma> t'"
proof -
  { fix \<tau>::"('fun, 'atom) term_type" assume "\<And>f T. Fun f T \<sqsubseteq> \<tau> \<Longrightarrow> 0 < arity f"
    hence "\<exists>t'. fv t' = {} \<and> \<tau> = \<Gamma> t'"
    proof (induction \<tau>)
      case (Fun f T)
      hence "arity f > 0" by auto
    
      from Fun.IH Fun.prems(1) have "\<exists>Y. map \<Gamma> Y = T \<and> (\<forall>x \<in> set Y. fv x = {})"
      proof (induction T)
        case (Cons x X)
        hence "\<And>g Y. Fun g Y \<sqsubseteq> Fun f X \<Longrightarrow> 0 < arity g" by auto
        hence "\<exists>Y. map \<Gamma> Y = X \<and> (\<forall>x\<in>set Y. fv x = {})" using Cons by auto
        moreover have "\<exists>t'. fv t' = {} \<and> x = \<Gamma> t'" using Cons by auto
        ultimately obtain y Y where
            "fv y = {}" "\<Gamma> y = x" "map \<Gamma> Y = X" "\<forall>x\<in>set Y. fv x = {}" 
          using Cons by moura
        hence "map \<Gamma> (y#Y) = x#X \<and> (\<forall>x\<in>set (y#Y). fv x = {})" by auto
        thus ?case by meson 
      qed simp
      then obtain Y where "map \<Gamma> Y = T" "\<forall>x \<in> set Y. fv x = {}" by metis
      hence "fv (Fun f Y) = {}" "\<Gamma> (Fun f Y) = TComp f T" using fun_type[OF \<open>arity f > 0\<close>] by auto
      thus ?case by (metis exI[of "\<lambda>t. fv t = {} \<and> \<Gamma> t = TComp f T" "Fun f Y"])
    qed (metis atype_ground_term_ex)
  }
  thus ?thesis by (metis \<Gamma>_wf(1))
qed

lemma type_wfttype_inhabited:
  assumes "\<And>f T. Fun f T \<sqsubseteq> \<tau> \<Longrightarrow> 0 < arity f" "wf\<^sub>t\<^sub>r\<^sub>m \<tau>"
  shows "\<exists>t. \<Gamma> t = \<tau> \<and> wf\<^sub>t\<^sub>r\<^sub>m t"
using assms
proof (induction \<tau>)
  case (Fun f Y)
  have IH: "\<exists>t. \<Gamma> t = y \<and> wf\<^sub>t\<^sub>r\<^sub>m t" when y: "y \<in> set Y " for y
  proof -
    have "wf\<^sub>t\<^sub>r\<^sub>m y"
      using Fun y unfolding wf\<^sub>t\<^sub>r\<^sub>m_def
      by (metis Fun_param_is_subterm term.le_less_trans) 
    moreover have "Fun g Z \<sqsubseteq> y \<Longrightarrow> 0 < arity g" for g Z
      using Fun y by auto
    ultimately show ?thesis using Fun.IH[OF y] by auto
  qed

  from Fun have "arity f = length Y" "arity f > 0" unfolding wf\<^sub>t\<^sub>r\<^sub>m_def by force+
  moreover from IH have "\<exists>X. map \<Gamma> X = Y \<and> (\<forall>x \<in> set X. wf\<^sub>t\<^sub>r\<^sub>m x)"
    by (induct Y, simp_all, metis list.simps(9) set_ConsD)
  ultimately show ?case by (metis fun_type length_map wf_trmI)
qed (use atypes_inhabited wf\<^sub>t\<^sub>r\<^sub>m_def in blast)

lemma type_pgwt_inhabited: "wf\<^sub>t\<^sub>r\<^sub>m t \<Longrightarrow> \<exists>t'. \<Gamma> t = \<Gamma> t' \<and> public_ground_wf_term t'"
proof -
  assume "wf\<^sub>t\<^sub>r\<^sub>m t"
  { fix \<tau> assume "\<Gamma> t = \<tau>"
    hence "\<exists>t'. \<Gamma> t = \<Gamma> t' \<and> public_ground_wf_term t'" using \<open>wf\<^sub>t\<^sub>r\<^sub>m t\<close>
    proof (induction \<tau> arbitrary: t)
      case (Var a t)
      then obtain c where "\<Gamma> t = \<Gamma> (Fun c [])" "arity c = 0" "public c"
        using const_type_inv[of _ "[]" a] infinite_typed_consts(1)[of a]  not_finite_existsD
        by force
      thus ?case using PGWT[OF \<open>public c\<close>, of "[]"] by auto
    next
      case (Fun f Y t)
      have *: "arity f > 0" "public f" "arity f = length Y"
        using fun_type_inv[OF \<open>\<Gamma> t = TComp f Y\<close>] fun_type_inv_wf[OF \<open>\<Gamma> t = TComp f Y\<close> \<open>wf\<^sub>t\<^sub>r\<^sub>m t\<close>]
        by auto
      have "\<And>y. y \<in> set Y \<Longrightarrow> \<exists>t'. y = \<Gamma> t' \<and> public_ground_wf_term t'"
        using Fun.prems(1) Fun.IH \<Gamma>_wf(1)[of _ _ t] \<Gamma>_wf'[OF \<open>wf\<^sub>t\<^sub>r\<^sub>m t\<close>] type_wfttype_inhabited
        by (metis Fun_param_is_subterm term.order_trans wf_trm_subtermeq) 
      hence "\<exists>X. map \<Gamma> X = Y \<and> (\<forall>x \<in> set X. public_ground_wf_term x)"
        by (induct Y, simp_all, metis list.simps(9) set_ConsD)
      then obtain X where X: "map \<Gamma> X = Y" "\<And>x. x \<in> set X \<Longrightarrow> public_ground_wf_term x" by moura
      hence "arity f = length X" using *(3) by auto
      have "\<Gamma> t = \<Gamma> (Fun f X)" "public_ground_wf_term (Fun f X)"
        using fun_type[OF *(1), of X] Fun.prems(1) X(1) apply simp
        using PGWT[OF *(2) \<open>arity f = length X\<close> X(2)] by metis
      thus ?case by metis
    qed
  }
  thus ?thesis using \<open>wf\<^sub>t\<^sub>r\<^sub>m t\<close> by auto
qed

lemma pgwt_type_map: 
  assumes "public_ground_wf_term t"
  shows "\<Gamma> t = TAtom a \<Longrightarrow> \<exists>f. t = Fun f []" "\<Gamma> t = TComp g Y \<Longrightarrow> \<exists>X. t = Fun g X \<and> map \<Gamma> X = Y"
proof -
  let ?A = "\<Gamma> t = TAtom a \<longrightarrow> (\<exists>f. t = Fun f [])"
  let ?B = "\<Gamma> t = TComp g Y \<longrightarrow> (\<exists>X. t = Fun g X \<and> map \<Gamma> X = Y)"
  have "?A \<and> ?B"
  proof (cases "\<Gamma> t")
    case (Var a)
    obtain f X where "t = Fun f X" "arity f = length X"
      using pgwt_fun[OF assms(1)] pgwt_arity[OF assms(1)] by fastforce+
    thus ?thesis using const_type_inv \<open>\<Gamma> t = TAtom a\<close> by auto
  next
    case (Fun g Y)
    obtain f X where *: "t = Fun f X" using pgwt_fun[OF assms(1)] by force
    hence "f = g" "map \<Gamma> X = Y"
      using fun_type_id_eq \<open>\<Gamma> t = TComp g Y\<close> fun_type[OF fun_type_inv(1)[OF \<open>\<Gamma> t = TComp g Y\<close>]]
      by fastforce+
    thus ?thesis using *(1) \<open>\<Gamma> t = TComp g Y\<close> by auto 
  qed
  thus "\<Gamma> t = TAtom a \<Longrightarrow> \<exists>f. t = Fun f []" "\<Gamma> t = TComp g Y \<Longrightarrow> \<exists>X. t = Fun g X \<and> map \<Gamma> X = Y"
    by auto
qed 

lemma wt_subst_Var[simp]: "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t Var" by (metis wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def)

lemma wt_subst_trm: "(\<And>v. v \<in> fv t \<Longrightarrow> \<Gamma> (Var v) = \<Gamma> (\<theta> v)) \<Longrightarrow> \<Gamma> t = \<Gamma> (t \<cdot> \<theta>)"
proof (induction t)
  case (Fun f X)
  hence *: "\<And>x. x \<in> set X \<Longrightarrow> \<Gamma> x = \<Gamma> (x \<cdot> \<theta>)" by auto
  show ?case
  proof (cases "f \<in> \<Sigma>\<^sub>f")
    case True
    hence "\<forall>X. \<Gamma> (Fun f X) = TComp f (map \<Gamma> X)" using fun_type' by auto
    thus ?thesis using * by auto
  next
    case False
    hence "\<exists>a \<in> \<TT>\<^sub>a. \<forall>X. \<Gamma> (Fun f X) = TAtom a" using const_type' by auto
    thus ?thesis by auto
  qed
qed auto

lemma wt_subst_trm': "\<lbrakk>wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>; \<Gamma> s = \<Gamma> t\<rbrakk> \<Longrightarrow> \<Gamma> (s \<cdot> \<sigma>) = \<Gamma> (t \<cdot> \<sigma>)"
by (metis wt_subst_trm wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def)

lemma wt_subst_trm'': "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma> \<Longrightarrow> \<Gamma> t = \<Gamma> (t \<cdot> \<sigma>)"
by (metis wt_subst_trm wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def)

lemma wt_subst_compose:
  assumes "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>" shows "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\<theta> \<circ>\<^sub>s \<delta>)"
proof -
  have "\<And>v. \<Gamma> (\<theta> v) = \<Gamma> (\<theta> v \<cdot> \<delta>)" using wt_subst_trm \<open>wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>\<close> unfolding wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by metis
  moreover have "\<And>v. \<Gamma> (Var v) = \<Gamma> (\<theta> v)" using \<open>wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>\<close> unfolding wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by metis
  ultimately have "\<And>v. \<Gamma> (Var v) = \<Gamma> (\<theta> v \<cdot> \<delta>)" by metis
  thus ?thesis unfolding wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def subst_compose_def by metis
qed

lemma wt_subst_TAtom_Var_cases:
  assumes \<theta>: "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<theta>)"
  and x: "\<Gamma> (Var x) = TAtom a"
  shows "(\<exists>y. \<theta> x = Var y) \<or> (\<exists>c. \<theta> x = Fun c [])"
proof (cases "(\<exists>y. \<theta> x = Var y)")
  case False
  then obtain c T where c: "\<theta> x = Fun c T"
    by (cases "\<theta> x") simp_all
  hence "wf\<^sub>t\<^sub>r\<^sub>m (Fun c T)"
    using \<theta>(2) by fastforce
  hence "T = []"
    using const_type_inv_wf[of c T a] x c wt_subst_trm''[OF \<theta>(1), of "Var x"]
    by fastforce
  thus ?thesis
    using c by blast
qed simp

lemma wt_subst_TAtom_fv:
  assumes \<theta>: "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>" "\<forall>x. wf\<^sub>t\<^sub>r\<^sub>m (\<theta> x)"
  and "\<forall>x \<in> fv t - X. \<exists>a. \<Gamma> (Var x) = TAtom a"
  shows "\<forall>x \<in> fv (t \<cdot> \<theta>) - fv\<^sub>s\<^sub>e\<^sub>t (\<theta> ` X). \<exists>a. \<Gamma> (Var x) = TAtom a"
using assms(3)
proof (induction t)
  case (Var x) thus ?case
  proof (cases "x \<in> X")
    case False
    with Var obtain a where "\<Gamma> (Var x) = TAtom a" by moura
    hence *: "\<Gamma> (\<theta> x) = TAtom a" "wf\<^sub>t\<^sub>r\<^sub>m (\<theta> x)" using \<theta> unfolding wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto
    show ?thesis
    proof (cases "\<theta> x")
      case (Var y) thus ?thesis using * by auto
    next
      case (Fun f T)
      hence "T = []" using * const_type_inv[of f T a] unfolding wf\<^sub>t\<^sub>r\<^sub>m_def by auto
      thus ?thesis using Fun by auto
    qed
  qed auto
qed fastforce

lemma wt_subst_TAtom_subterms_subst:
  assumes "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>" "\<forall>x \<in> fv t. \<exists>a. \<Gamma> (Var x) = TAtom a" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (\<theta> ` fv t)"
  shows "subterms (t \<cdot> \<theta>) = subterms t \<cdot>\<^sub>s\<^sub>e\<^sub>t \<theta>"
using assms(2,3)
proof (induction t)
  case (Var x)
  obtain a where a: "\<Gamma> (Var x) = TAtom a" using Var.prems(1) by moura
  hence "\<Gamma> (\<theta> x) = TAtom a" using wt_subst_trm''[OF assms(1), of "Var x"] by simp
  hence "(\<exists>y. \<theta> x = Var y) \<or> (\<exists>c. \<theta> x = Fun c [])"
    using const_type_inv_wf Var.prems(2) by (cases "\<theta> x") auto
  thus ?case by auto
next
  case (Fun f T)
  have "subterms (t \<cdot> \<theta>) = subterms t \<cdot>\<^sub>s\<^sub>e\<^sub>t \<theta>" when "t \<in> set T" for t
    using that Fun.prems(1,2) Fun.IH[OF that]
    by auto
  thus ?case by auto
qed

lemma wt_subst_TAtom_subterms_set_subst: 
  assumes "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>" "\<forall>x \<in> fv\<^sub>s\<^sub>e\<^sub>t M. \<exists>a. \<Gamma> (Var x) = TAtom a" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (\<theta> ` fv\<^sub>s\<^sub>e\<^sub>t M)"
  shows "subterms\<^sub>s\<^sub>e\<^sub>t (M \<cdot>\<^sub>s\<^sub>e\<^sub>t \<theta>) = subterms\<^sub>s\<^sub>e\<^sub>t M \<cdot>\<^sub>s\<^sub>e\<^sub>t \<theta>"
proof
  show "subterms\<^sub>s\<^sub>e\<^sub>t (M \<cdot>\<^sub>s\<^sub>e\<^sub>t \<theta>) \<subseteq> subterms\<^sub>s\<^sub>e\<^sub>t M \<cdot>\<^sub>s\<^sub>e\<^sub>t \<theta>"
  proof
    fix t assume "t \<in> subterms\<^sub>s\<^sub>e\<^sub>t (M \<cdot>\<^sub>s\<^sub>e\<^sub>t \<theta>)"
    then obtain s where s: "s \<in> M" "t \<in> subterms (s \<cdot> \<theta>)" by auto
    thus "t \<in> subterms\<^sub>s\<^sub>e\<^sub>t M \<cdot>\<^sub>s\<^sub>e\<^sub>t \<theta>"
      using assms(2,3) wt_subst_TAtom_subterms_subst[OF assms(1), of s]
      by auto
  qed

  show "subterms\<^sub>s\<^sub>e\<^sub>t M \<cdot>\<^sub>s\<^sub>e\<^sub>t \<theta> \<subseteq> subterms\<^sub>s\<^sub>e\<^sub>t (M \<cdot>\<^sub>s\<^sub>e\<^sub>t \<theta>)"
  proof
    fix t assume "t \<in> subterms\<^sub>s\<^sub>e\<^sub>t M \<cdot>\<^sub>s\<^sub>e\<^sub>t \<theta>"
    then obtain s where s: "s \<in> M" "t \<in> subterms s \<cdot>\<^sub>s\<^sub>e\<^sub>t \<theta>" by auto
    thus "t \<in> subterms\<^sub>s\<^sub>e\<^sub>t (M \<cdot>\<^sub>s\<^sub>e\<^sub>t \<theta>)"
      using assms(2,3) wt_subst_TAtom_subterms_subst[OF assms(1), of s]
      by auto
  qed
qed

lemma wt_subst_subst_upd:
  assumes "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>"
    and "\<Gamma> (Var x) = \<Gamma> t"
  shows "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\<theta>(x := t))"
using assms unfolding wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def
by (metis fun_upd_other fun_upd_same)

lemma wt_subst_const_fv_type_eq:
  assumes "\<forall>x \<in> fv t. \<exists>a. \<Gamma> (Var x) = TAtom a"
    and \<delta>: "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<delta>)"
  shows "\<forall>x \<in> fv (t \<cdot> \<delta>). \<exists>y \<in> fv t. \<Gamma> (Var x) = \<Gamma> (Var y)"
using assms(1)
proof (induction t)
  case (Var x)
  then obtain a where a: "\<Gamma> (Var x) = TAtom a" by moura
  show ?case
  proof (cases "\<delta> x")
    case (Fun f T)
    hence "wf\<^sub>t\<^sub>r\<^sub>m (Fun f T)" "\<Gamma> (Fun f T) = TAtom a"
      using a wt_subst_trm''[OF \<delta>(1), of "Var x"] \<delta>(2) by fastforce+
    thus ?thesis using const_type_inv_wf Fun by fastforce
  qed (use a wt_subst_trm''[OF \<delta>(1), of "Var x"] in simp)
qed fastforce

lemma TComp_term_cases:
  assumes "wf\<^sub>t\<^sub>r\<^sub>m t" "\<Gamma> t = TComp f T"
  shows "(\<exists>v. t = Var v) \<or> (\<exists>T'. t = Fun f T' \<and> T = map \<Gamma> T' \<and> T' \<noteq> [])"
proof (cases "\<exists>v. t = Var v")
  case False
  then obtain T' where T': "t = Fun f T'" "T = map \<Gamma> T'"
    using assms fun_type[OF fun_type_inv(1)[OF assms(2)]] fun_type_id_eq
    by (cases t) force+
  thus ?thesis using assms fun_type_inv(1) fun_type_inv_wf by fastforce
qed metis

lemma TAtom_term_cases:
  assumes "wf\<^sub>t\<^sub>r\<^sub>m t" "\<Gamma> t = TAtom \<tau>"
  shows "(\<exists>v. t = Var v) \<or> (\<exists>f. t = Fun f [])"
using assms const_type_inv unfolding wf\<^sub>t\<^sub>r\<^sub>m_def by (cases t) auto

lemma subtermeq_imp_subtermtypeeq:
  assumes "wf\<^sub>t\<^sub>r\<^sub>m t" "s \<sqsubseteq> t"
  shows "\<Gamma> s \<sqsubseteq> \<Gamma> t"
using assms(2,1)
proof (induction t)
  case (Fun f T) thus ?case
  proof (cases "s = Fun f T")
    case False
    then obtain x where x: "x \<in> set T" "s \<sqsubseteq> x" using Fun.prems(1) by auto
    hence "wf\<^sub>t\<^sub>r\<^sub>m x" using wf_trm_subtermeq[OF Fun.prems(2)] Fun_param_is_subterm[of _ T f] by auto
    hence "\<Gamma> s \<sqsubseteq> \<Gamma> x" using Fun.IH[OF x] by simp
    moreover have "arity f > 0" using x fun_type_inv_wf Fun.prems
      by (metis length_pos_if_in_set term.order_refl wf\<^sub>t\<^sub>r\<^sub>m_def)
    ultimately show ?thesis using x Fun.prems fun_type[of f T] by auto
  qed simp
qed simp

lemma subterm_funs_term_in_type:
  assumes "wf\<^sub>t\<^sub>r\<^sub>m t" "Fun f T \<sqsubseteq> t" "\<Gamma> (Fun f T) = TComp f (map \<Gamma> T)"
  shows "f \<in> funs_term (\<Gamma> t)"
using assms(2,1,3)
proof (induction t)
  case (Fun f' T')
  hence [simp]: "wf\<^sub>t\<^sub>r\<^sub>m (Fun f T)" by (metis wf_trm_subtermeq)
  { fix a assume \<tau>: "\<Gamma> (Fun f' T') = TAtom a"
    hence "Fun f T = Fun f' T'" using Fun TAtom_term_cases subtermeq_Var_const by metis
    hence False using Fun.prems(3) \<tau> by simp
  }
  moreover
  { fix g S assume \<tau>: "\<Gamma> (Fun f' T') = TComp g S"
    hence "g = f'" "S = map \<Gamma> T'"
      using Fun.prems(2) fun_type_id_eq[OF \<tau>] fun_type[OF fun_type_inv(1)[OF \<tau>]]
      by auto
    hence \<tau>': "\<Gamma> (Fun f' T') = TComp f' (map \<Gamma> T')" using \<tau> by auto
    hence "g \<in> funs_term (\<Gamma> (Fun f' T'))" using \<tau> by auto
    moreover {
      assume "Fun f T \<noteq> Fun f' T'"
      then obtain x where "x \<in> set T'" "Fun f T \<sqsubseteq> x" using Fun.prems(1) by auto
      hence "f \<in> funs_term (\<Gamma> x)"
        using Fun.IH[OF _ _ _ Fun.prems(3), of x] wf_trm_subtermeq[OF \<open>wf\<^sub>t\<^sub>r\<^sub>m (Fun f' T')\<close>, of x]
        by force
      moreover have "\<Gamma> x \<in> set (map \<Gamma> T')" using \<tau>' \<open>x \<in> set T'\<close> by auto
      ultimately have "f \<in> funs_term (\<Gamma> (Fun f' T'))" using \<tau>' by auto
    }
    ultimately have ?case by (cases "Fun f T = Fun f' T'") (auto simp add: \<open>g = f'\<close>)
  }
  ultimately show ?case by (cases "\<Gamma> (Fun f' T')") auto
qed simp

lemma wt_subst_fv_termtype_subterm:
  assumes "x \<in> fv (\<theta> y)"
    and "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>"
    and "wf\<^sub>t\<^sub>r\<^sub>m (\<theta> y)"
  shows "\<Gamma> (Var x) \<sqsubseteq> \<Gamma> (Var y)"
using subtermeq_imp_subtermtypeeq[OF assms(3) var_is_subterm[OF assms(1)]]
      wt_subst_trm''[OF assms(2), of "Var y"]
by auto

lemma wt_subst_fv\<^sub>s\<^sub>e\<^sub>t_termtype_subterm:
  assumes "x \<in> fv\<^sub>s\<^sub>e\<^sub>t (\<theta> ` Y)"
    and "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>"
    and "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<theta>)"
  shows "\<exists>y \<in> Y. \<Gamma> (Var x) \<sqsubseteq> \<Gamma> (Var y)"
using wt_subst_fv_termtype_subterm[OF _ assms(2), of x] assms(1,3)
by fastforce

lemma funs_term_type_iff:
  assumes t: "wf\<^sub>t\<^sub>r\<^sub>m t"
    and f: "arity f > 0"
  shows "f \<in> funs_term (\<Gamma> t) \<longleftrightarrow> (f \<in> funs_term t \<or> (\<exists>x \<in> fv t. f \<in> funs_term (\<Gamma> (Var x))))"
    (is "?P t \<longleftrightarrow> ?Q t")
using t
proof (induction t)
  case (Fun g T)
  hence IH: "?P s \<longleftrightarrow> ?Q s" when "s \<in> set T" for s
    using that wf_trm_subterm[OF _ Fun_param_is_subterm]
    by blast
  have 0: "arity g = length T" using Fun.prems unfolding wf\<^sub>t\<^sub>r\<^sub>m_def by auto
  show ?case
  proof (cases "f = g")
    case True thus ?thesis using fun_type[OF f] by simp
  next
    case False
    have "?P (Fun g T) \<longleftrightarrow> (\<exists>s \<in> set T. ?P s)"
    proof
      assume *: "?P (Fun g T)"
      hence "\<Gamma> (Fun g T) = TComp g (map \<Gamma> T)"
        using const_type[of g] fun_type[of g] by force
      thus "\<exists>s \<in> set T. ?P s" using False * by force
    next
      assume *: "\<exists>s \<in> set T. ?P s"
      hence "\<Gamma> (Fun g T) = TComp g (map \<Gamma> T)"
        using 0 const_type[of g] fun_type[of g] by force
      thus "?P (Fun g T)" using False * by force
    qed
    thus ?thesis using False f IH by auto
  qed
qed simp

lemma funs_term_type_iff':
  assumes M: "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s M"
    and f: "arity f > 0"
  shows "f \<in> \<Union>(funs_term ` \<Gamma> ` M) \<longleftrightarrow>
        (f \<in> \<Union>(funs_term ` M) \<or> (\<exists>x \<in> fv\<^sub>s\<^sub>e\<^sub>t M. f \<in> funs_term (\<Gamma> (Var x))))" (is "?A \<longleftrightarrow> ?B")
proof
  assume ?A
  then obtain t where "t \<in> M" "wf\<^sub>t\<^sub>r\<^sub>m t" "f \<in> funs_term (\<Gamma> t)" using M by moura
  thus ?B using funs_term_type_iff[OF _ f, of t] by auto
next
  assume ?B
  then obtain t where "t \<in> M" "wf\<^sub>t\<^sub>r\<^sub>m t" "f \<in> funs_term t \<or> (\<exists>x \<in> fv t. f \<in> funs_term (\<Gamma> (Var x)))"
    using M by auto
  thus ?A using funs_term_type_iff[OF _ f, of t] by blast
qed

lemma Ana_subterm_type:
  assumes "Ana t = (K,M)"
    and "wf\<^sub>t\<^sub>r\<^sub>m t"
    and "m \<in> set M"
  shows "\<Gamma> m \<sqsubseteq> \<Gamma> t"
proof -
  have "m \<sqsubseteq> t" using Ana_subterm[OF assms(1)] assms(3) by auto
  thus ?thesis using subtermeq_imp_subtermtypeeq[OF assms(2)] by simp
qed

lemma wf_trm_TAtom_subterms:
  assumes "wf\<^sub>t\<^sub>r\<^sub>m t" "\<Gamma> t = TAtom \<tau>"
  shows "subterms t = {t}"
using assms const_type_inv unfolding wf\<^sub>t\<^sub>r\<^sub>m_def by (cases t) force+

lemma wf_trm_TComp_subterm:
  assumes "wf\<^sub>t\<^sub>r\<^sub>m s" "t \<sqsubset> s"
  obtains f T where "\<Gamma> s = TComp f T"
proof (cases s)
  case (Var x) thus ?thesis using \<open>t \<sqsubset> s\<close> by simp
next
  case (Fun g S)
  hence "length S > 0" using assms Fun_subterm_inside_params[of t g S] by auto
  hence "arity g > 0" by (metis \<open>wf\<^sub>t\<^sub>r\<^sub>m s\<close> \<open>s = Fun g S\<close> term.order_refl wf\<^sub>t\<^sub>r\<^sub>m_def) 
  thus ?thesis using fun_type \<open>s = Fun g S\<close> that by auto
qed

lemma SMP_empty[simp]: "SMP {} = {}"
proof (rule ccontr)
  assume "SMP {} \<noteq> {}"
  then obtain t where "t \<in> SMP {}" by auto
  thus False by (induct t rule: SMP.induct) auto
qed

lemma SMP_I:
  assumes "s \<in> M" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>" "t \<sqsubseteq> s \<cdot> \<delta>" "\<And>v. wf\<^sub>t\<^sub>r\<^sub>m (\<delta> v)"
  shows "t \<in> SMP M"
using SMP.Substitution[OF SMP.MP[OF assms(1)] assms(2)] SMP.Subterm[of "s \<cdot> \<delta>" M t] assms(3,4)
by (cases "t = s \<cdot> \<delta>") simp_all

lemma SMP_wf_trm:
  assumes "t \<in> SMP M" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s M"
  shows "wf\<^sub>t\<^sub>r\<^sub>m t"
using assms(1)
by (induct t rule: SMP.induct)
   (use assms(2) in blast,
    use wf_trm_subtermeq in blast,
    use wf_trm_subst in blast,
    use Ana_keys_wf' in blast)

lemma SMP_ikI[intro]: "t \<in> ik\<^sub>s\<^sub>t S \<Longrightarrow> t \<in> SMP (trms\<^sub>s\<^sub>t S)" by force

lemma MP_setI[intro]: "x \<in> set S \<Longrightarrow> trms\<^sub>s\<^sub>t\<^sub>p x \<subseteq> trms\<^sub>s\<^sub>t S" by force

lemma SMP_setI[intro]: "x \<in> set S \<Longrightarrow> trms\<^sub>s\<^sub>t\<^sub>p x \<subseteq> SMP (trms\<^sub>s\<^sub>t S)" by force

lemma SMP_subset_I:
  assumes M: "\<forall>t \<in> M. \<exists>s \<delta>. s \<in> N \<and> wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<and> wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<delta>) \<and> t = s \<cdot> \<delta>"
  shows "SMP M \<subseteq> SMP N"
proof
  fix t show "t \<in> SMP M \<Longrightarrow> t \<in> SMP N"
  proof (induction t rule: SMP.induct)
    case (MP t)
    then obtain s \<delta> where s: "s \<in> N" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<delta>)" "t = s \<cdot> \<delta>"
      using M by moura
    show ?case using SMP_I[OF s(1,2), of "s \<cdot> \<delta>"] s(3,4) wf_trm_subst_range_iff by fast
  qed (auto intro!: SMP.Substitution[of _ N])
qed

lemma SMP_union: "SMP (A \<union> B) = SMP A \<union> SMP B"
proof
  show "SMP (A \<union> B) \<subseteq> SMP A \<union> SMP B"
  proof
    fix t assume "t \<in> SMP (A \<union> B)"
    thus "t \<in> SMP A \<union> SMP B" by (induct rule: SMP.induct) blast+
  qed

  { fix t assume "t \<in> SMP A" hence "t \<in> SMP (A \<union> B)" by (induct rule: SMP.induct) blast+ }
  moreover { fix t assume "t \<in> SMP B" hence "t \<in> SMP (A \<union> B)" by (induct rule: SMP.induct) blast+ }
  ultimately show "SMP A \<union> SMP B \<subseteq> SMP (A \<union> B)" by blast
qed

lemma SMP_append[simp]: "SMP (trms\<^sub>s\<^sub>t (S@S')) = SMP (trms\<^sub>s\<^sub>t S) \<union> SMP (trms\<^sub>s\<^sub>t S')" (is "?A = ?B")
using SMP_union by simp

lemma SMP_mono: "A \<subseteq> B \<Longrightarrow> SMP A \<subseteq> SMP B"
proof -
  assume "A \<subseteq> B"
  then obtain C where "B = A \<union> C" by moura
  thus "SMP A \<subseteq> SMP B" by (simp add: SMP_union)
qed

lemma SMP_Union: "SMP (\<Union>m \<in> M. f m) = (\<Union>m \<in> M. SMP (f m))"
proof
  show "SMP (\<Union>m\<in>M. f m) \<subseteq> (\<Union>m\<in>M. SMP (f m))"
  proof
    fix t assume "t \<in> SMP (\<Union>m\<in>M. f m)"
    thus "t \<in> (\<Union>m\<in>M. SMP (f m))" by (induct t rule: SMP.induct) force+
  qed
  show "(\<Union>m\<in>M. SMP (f m)) \<subseteq> SMP (\<Union>m\<in>M. f m)"
  proof
    fix t assume "t \<in> (\<Union>m\<in>M. SMP (f m))"
    then obtain m where "m \<in> M" "t \<in> SMP (f m)" by moura
    thus "t \<in> SMP (\<Union>m\<in>M. f m)" using SMP_mono[of "f m" "\<Union>m\<in>M. f m"] by auto
  qed
qed

lemma SMP_singleton_ex:
  "t \<in> SMP M \<Longrightarrow> (\<exists>m \<in> M. t \<in> SMP {m})"
  "m \<in> M \<Longrightarrow> t \<in> SMP {m} \<Longrightarrow> t \<in> SMP M"
using SMP_Union[of "\<lambda>t. {t}" M] by auto

lemma SMP_Cons: "SMP (trms\<^sub>s\<^sub>t (x#S)) = SMP (trms\<^sub>s\<^sub>t [x]) \<union> SMP (trms\<^sub>s\<^sub>t S)"
using SMP_append[of "[x]" S] by auto

lemma SMP_Nil[simp]: "SMP (trms\<^sub>s\<^sub>t []) = {}" 
proof -
  { fix t assume "t \<in> SMP (trms\<^sub>s\<^sub>t [])" hence False by induct auto }
  thus ?thesis by blast
qed

lemma SMP_subset_union_eq: assumes "M \<subseteq> SMP N" shows "SMP N = SMP (M \<union> N)"
proof -
  { fix t assume "t \<in> SMP (M \<union> N)" hence "t \<in> SMP N"
      using assms by (induction rule: SMP.induct) blast+
  }
  thus ?thesis using SMP_union by auto
qed

lemma SMP_subterms_subset: "subterms\<^sub>s\<^sub>e\<^sub>t M \<subseteq> SMP M"
proof
  fix t assume "t \<in> subterms\<^sub>s\<^sub>e\<^sub>t M"
  then obtain m where "m \<in> M" "t \<sqsubseteq> m" by auto
  thus "t \<in> SMP M" using SMP_I[of _ _ Var] by auto
qed

lemma SMP_SMP_subset: "N \<subseteq> SMP M \<Longrightarrow> SMP N \<subseteq> SMP M"
by (metis SMP_mono SMP_subset_union_eq Un_commute Un_upper2)

lemma wt_subst_rm_vars: "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<Longrightarrow> wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (rm_vars X \<delta>)"
using rm_vars_dom unfolding wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto

lemma wt_subst_SMP_subset:
  assumes "trms\<^sub>s\<^sub>t S \<subseteq> SMP S'" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<delta>)"
  shows "trms\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>t \<delta>) \<subseteq> SMP S'"
proof
  fix t assume *: "t \<in> trms\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>t \<delta>)"
  show "t \<in> SMP S'" using trm_strand_subst_cong(2)[OF *]
  proof
    assume "\<exists>t'. t = t' \<cdot> \<delta> \<and> t' \<in> trms\<^sub>s\<^sub>t S"
    thus "t \<in> SMP S'" using assms SMP.Substitution by auto
  next
    assume "\<exists>X F. Inequality X F \<in> set S \<and> (\<exists>t'\<in>trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F. t = t' \<cdot> rm_vars (set X) \<delta>)"
    then obtain X F t' where **:
        "Inequality X F \<in> set S" "t'\<in>trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F" "t = t' \<cdot> rm_vars (set X) \<delta>"
      by force
    then obtain s where s: "s \<in> trms\<^sub>s\<^sub>t\<^sub>p (Inequality X F)" "t = s \<cdot> rm_vars (set X) \<delta>" by moura
    hence "s \<in> SMP (trms\<^sub>s\<^sub>t S)" using **(1) by force
    hence "t \<in> SMP (trms\<^sub>s\<^sub>t S)"
      using SMP.Substitution[OF _ wt_subst_rm_vars[OF assms(2)] wf_trms_subst_rm_vars'[OF assms(3)]]
      unfolding s(2) by blast
    thus "t \<in> SMP S'" by (metis SMP_union SMP_subset_union_eq UnCI assms(1))
  qed
qed

lemma MP_subset_SMP: "\<Union>(trms\<^sub>s\<^sub>t\<^sub>p ` set S) \<subseteq> SMP (trms\<^sub>s\<^sub>t S)" "trms\<^sub>s\<^sub>t S \<subseteq> SMP (trms\<^sub>s\<^sub>t S)" "M \<subseteq> SMP M"
by auto

lemma SMP_fun_map_snd_subset: "SMP (trms\<^sub>s\<^sub>t (map Send X)) \<subseteq> SMP (trms\<^sub>s\<^sub>t [Send (Fun f X)])"
proof
  fix t assume "t \<in> SMP (trms\<^sub>s\<^sub>t (map Send X))" thus "t \<in> SMP (trms\<^sub>s\<^sub>t [Send (Fun f X)])"
  proof (induction t rule: SMP.induct)
    case (MP t)
    hence "t \<in> set X" by auto
    hence "t \<sqsubset> Fun f X" by (metis subtermI')
    thus ?case using SMP.Subterm[of "Fun f X" "trms\<^sub>s\<^sub>t [Send (Fun f X)]" t] using SMP.MP by auto
  qed blast+
qed

lemma SMP_wt_subst_subset:
  assumes "t \<in> SMP (M \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>)" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<I>)"
  shows "t \<in> SMP M"
using assms wf_trm_subst_range_iff[of \<I>] by (induct t rule: SMP.induct) blast+

lemma SMP_wt_instances_subset:
  assumes "\<forall>t \<in> M. \<exists>s \<in> N. \<exists>\<delta>. t = s \<cdot> \<delta> \<and> wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<and> wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<delta>)"
    and "t \<in> SMP M"
  shows "t \<in> SMP N"
proof -
  obtain m where m: "m \<in> M" "t \<in> SMP {m}" using SMP_singleton_ex(1)[OF assms(2)] by blast
  then obtain n \<delta> where n: "n \<in> N" "m = n \<cdot> \<delta>" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<delta>)"
    using assms(1) by fast

  have "t \<in> SMP (N \<cdot>\<^sub>s\<^sub>e\<^sub>t \<delta>)" using n(1,2) SMP_singleton_ex(2)[of m "N \<cdot>\<^sub>s\<^sub>e\<^sub>t \<delta>", OF _ m(2)] by fast
  thus ?thesis using SMP_wt_subst_subset[OF _ n(3,4)] by blast
qed

lemma SMP_consts:
  assumes "\<forall>t \<in> M. \<exists>c. t = Fun c []"
    and "\<forall>t \<in> M. Ana t = ([], [])"
  shows "SMP M = M"
proof
  show "SMP M \<subseteq> M"
  proof
    fix t show "t \<in> SMP M \<Longrightarrow> t \<in> M"
      apply (induction t rule: SMP.induct)
      by (use assms in auto)
  qed
qed auto

lemma SMP_subterms_eq:
  "SMP (subterms\<^sub>s\<^sub>e\<^sub>t M) = SMP M"
proof
  show "SMP M \<subseteq> SMP (subterms\<^sub>s\<^sub>e\<^sub>t M)" using SMP_mono[of M "subterms\<^sub>s\<^sub>e\<^sub>t M"] by blast
  show "SMP (subterms\<^sub>s\<^sub>e\<^sub>t M) \<subseteq> SMP M"
  proof
    fix t show "t \<in> SMP (subterms\<^sub>s\<^sub>e\<^sub>t M) \<Longrightarrow> t \<in> SMP M" by (induction t rule: SMP.induct) blast+
  qed
qed

lemma SMP_funs_term:
  assumes t: "t \<in> SMP M" "f \<in> funs_term t \<or> (\<exists>x \<in> fv t. f \<in> funs_term (\<Gamma> (Var x)))"
    and f: "arity f > 0"
    and M: "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s M"
    and Ana_f: "\<And>s K T. Ana s = (K,T) \<Longrightarrow> f \<in> \<Union>(funs_term ` set K) \<Longrightarrow> f \<in> funs_term s"
  shows "f \<in> \<Union>(funs_term ` M) \<or> (\<exists>x \<in> fv\<^sub>s\<^sub>e\<^sub>t M. f \<in> funs_term (\<Gamma> (Var x)))"
using t
proof (induction t rule: SMP.induct)
  case (Subterm t t')
  thus ?case by (metis UN_I vars_iff_subtermeq funs_term_subterms_eq(1) term.order_trans)
next
  case (Substitution t \<delta>)
  show ?case
    using M SMP_wf_trm[OF Substitution.hyps(1)] wf_trm_subst[of \<delta> t, OF Substitution.hyps(3)]
          funs_term_type_iff[OF _ f] wt_subst_trm''[OF Substitution.hyps(2), of t]
          Substitution.prems Substitution.IH
    by metis
next
  case (Ana t K T t')
  thus ?case
    using Ana_f[OF Ana.hyps(2)] Ana_keys_fv[OF Ana.hyps(2)]
    by fastforce
qed auto

lemma id_type_eq:
  assumes "\<Gamma> (Fun f X) = \<Gamma> (Fun g Y)"
  shows "f \<in> \<C> \<Longrightarrow> g \<in> \<C>" "f \<in> \<Sigma>\<^sub>f \<Longrightarrow> g \<in> \<Sigma>\<^sub>f"
using assms const_type' fun_type' id_union_univ(1)
by (metis UNIV_I UnE "term.distinct"(1))+

lemma fun_type_arg_cong:
  assumes "f \<in> \<Sigma>\<^sub>f" "g \<in> \<Sigma>\<^sub>f" "\<Gamma> (Fun f (x#X)) = \<Gamma> (Fun g (y#Y))"
  shows "\<Gamma> x = \<Gamma> y" "\<Gamma> (Fun f X) = \<Gamma> (Fun g Y)"
using assms fun_type' by auto

lemma fun_type_arg_cong':
  assumes "f \<in> \<Sigma>\<^sub>f" "g \<in> \<Sigma>\<^sub>f" "\<Gamma> (Fun f (X@x#X')) = \<Gamma> (Fun g (Y@y#Y'))" "length X = length Y"
  shows "\<Gamma> x = \<Gamma> y"
using assms
proof (induction X arbitrary: Y)
  case Nil thus ?case using fun_type_arg_cong(1)[of f g x X' y Y'] by auto
next
  case (Cons x' X Y'')
  then obtain y' Y where "Y'' = y'#Y" by (metis length_Suc_conv)
  hence "\<Gamma> (Fun f (X@x#X')) = \<Gamma> (Fun g (Y@y#Y'))" "length X = length Y"
    using Cons.prems(3,4) fun_type_arg_cong(2)[OF Cons.prems(1,2), of x' "X@x#X'"] by auto
  thus ?thesis using Cons.IH[OF Cons.prems(1,2)] by auto
qed

lemma fun_type_param_idx: "\<Gamma> (Fun f T) = Fun g S \<Longrightarrow> i < length T \<Longrightarrow> \<Gamma> (T ! i) = S ! i"
by (metis fun_type fun_type_id_eq fun_type_inv(1) nth_map term.inject(2))

lemma fun_type_param_ex:
  assumes "\<Gamma> (Fun f T) = Fun g (map \<Gamma> S)" "t \<in> set S"
  shows "\<exists>s \<in> set T. \<Gamma> s = \<Gamma> t"
using fun_type_length_eq[OF assms(1)] length_map[of \<Gamma> S] assms(2)
      fun_type_param_idx[OF assms(1)] nth_map in_set_conv_nth
by metis

lemma tfr_stp_all_split:
  "list_all tfr\<^sub>s\<^sub>t\<^sub>p (x#S) \<Longrightarrow> list_all tfr\<^sub>s\<^sub>t\<^sub>p [x]"
  "list_all tfr\<^sub>s\<^sub>t\<^sub>p (x#S) \<Longrightarrow> list_all tfr\<^sub>s\<^sub>t\<^sub>p S"
  "list_all tfr\<^sub>s\<^sub>t\<^sub>p (S@S') \<Longrightarrow> list_all tfr\<^sub>s\<^sub>t\<^sub>p S"
  "list_all tfr\<^sub>s\<^sub>t\<^sub>p (S@S') \<Longrightarrow> list_all tfr\<^sub>s\<^sub>t\<^sub>p S'"
  "list_all tfr\<^sub>s\<^sub>t\<^sub>p (S@x#S') \<Longrightarrow> list_all tfr\<^sub>s\<^sub>t\<^sub>p (S@S')"
by fastforce+

lemma tfr_stp_all_append:
  assumes "list_all tfr\<^sub>s\<^sub>t\<^sub>p S" "list_all tfr\<^sub>s\<^sub>t\<^sub>p S'"
  shows "list_all tfr\<^sub>s\<^sub>t\<^sub>p (S@S')"
using assms by fastforce

lemma tfr_stp_all_wt_subst_apply:
  assumes "list_all tfr\<^sub>s\<^sub>t\<^sub>p S"
    and \<theta>: "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<theta>)"
           "bvars\<^sub>s\<^sub>t S \<inter> range_vars \<theta> = {}"
  shows "list_all tfr\<^sub>s\<^sub>t\<^sub>p (S \<cdot>\<^sub>s\<^sub>t \<theta>)"
using assms(1,4)
proof (induction S)
  case (Cons x S)
  hence IH: "list_all tfr\<^sub>s\<^sub>t\<^sub>p (S \<cdot>\<^sub>s\<^sub>t \<theta>)"
    using tfr_stp_all_split(2)[of x S]
    unfolding range_vars_alt_def by fastforce
  thus ?case
  proof (cases x)
    case (Equality a t t')
    hence "(\<exists>\<delta>. Unifier \<delta> t t') \<longrightarrow> \<Gamma> t = \<Gamma> t'" using Cons.prems by auto
    hence "(\<exists>\<delta>. Unifier \<delta> (t \<cdot> \<theta>) (t' \<cdot> \<theta>)) \<longrightarrow> \<Gamma> (t \<cdot> \<theta>) = \<Gamma> (t' \<cdot> \<theta>)"
      by (metis Unifier_comp' wt_subst_trm'[OF assms(2)])
    moreover have "(x#S) \<cdot>\<^sub>s\<^sub>t \<theta> = Equality a (t \<cdot> \<theta>) (t' \<cdot> \<theta>)#(S \<cdot>\<^sub>s\<^sub>t \<theta>)"
      using \<open>x = Equality a t t'\<close> by auto
    ultimately show ?thesis using IH by auto
  next
    case (Inequality X F)
    let ?\<sigma> = "rm_vars (set X) \<theta>"
    let ?G = "F \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s ?\<sigma>"

    let ?P = "\<lambda>F X. \<forall>x \<in> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F - set X. \<exists>a. \<Gamma> (Var x) = TAtom a"
    let ?Q = "\<lambda>F X.
      \<forall>f T. Fun f T \<in> subterms\<^sub>s\<^sub>e\<^sub>t (trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F) \<longrightarrow> T = [] \<or> (\<exists>s \<in> set T. s \<notin> Var ` set X)"

    have 0: "set X \<inter> range_vars ?\<sigma> = {}"
      using Cons.prems(2) Inequality rm_vars_img_subset[of "set X"]
      by (auto simp add: subst_domain_def range_vars_alt_def)

    have 1: "?P F X \<or> ?Q F X" using Inequality Cons.prems by simp

    have 2: "fv\<^sub>s\<^sub>e\<^sub>t (?\<sigma> ` set X) = set X" by auto

    have "?P ?G X" when "?P F X" using that
    proof (induction F)
      case (Cons g G)
      obtain t t' where g: "g = (t,t')" by (metis surj_pair)
      
      have "\<forall>x \<in> (fv (t \<cdot> ?\<sigma>) \<union> fv (t' \<cdot> ?\<sigma>)) - set X. \<exists>a. \<Gamma> (Var x) = Var a"
      proof -
        have *: "\<forall>x \<in> fv t - set X. \<exists>a. \<Gamma> (Var x) = Var a"
               "\<forall>x \<in> fv t' - set X. \<exists>a. \<Gamma> (Var x) = Var a"
          using g Cons.prems by simp_all

        have **: "\<forall>x. wf\<^sub>t\<^sub>r\<^sub>m (?\<sigma> x)"
          using \<theta>(2) wf_trm_subst_range_iff[of \<theta>] wf_trm_subst_rm_vars'[of \<theta> _ "set X"] by simp

        show ?thesis
          using wt_subst_TAtom_fv[OF wt_subst_rm_vars[OF \<theta>(1)] ** *(1)]
                wt_subst_TAtom_fv[OF wt_subst_rm_vars[OF \<theta>(1)] ** *(2)]
                wt_subst_trm'[OF wt_subst_rm_vars[OF \<theta>(1), of "set X"]] 2
          by blast
      qed
      moreover have "\<forall>x\<in>fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s (G \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s ?\<sigma>) - set X. \<exists>a. \<Gamma> (Var x) = Var a"
        using Cons by auto
      ultimately show ?case using g by (auto simp add: subst_apply_pairs_def)
    qed (simp add: subst_apply_pairs_def)
    hence "?P ?G X \<or> ?Q ?G X"
      using 1 ineq_subterm_inj_cond_subst[OF 0, of "trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F"] trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s_subst[of F ?\<sigma>]
      by presburger
    moreover have "(x#S) \<cdot>\<^sub>s\<^sub>t \<theta> = Inequality X (F \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s ?\<sigma>)#(S \<cdot>\<^sub>s\<^sub>t \<theta>)"
      using \<open>x = Inequality X F\<close> by auto
    ultimately show ?thesis using IH by simp
  qed auto
qed simp

lemma tfr_stp_all_same_type:
  "list_all tfr\<^sub>s\<^sub>t\<^sub>p (S@Equality a t t'#S') \<Longrightarrow> Unifier \<delta> t t' \<Longrightarrow> \<Gamma> t = \<Gamma> t'"
by force+

lemma tfr_subset:
  "\<And>A B. tfr\<^sub>s\<^sub>e\<^sub>t (A \<union> B) \<Longrightarrow> tfr\<^sub>s\<^sub>e\<^sub>t A"
  "\<And>A B. tfr\<^sub>s\<^sub>e\<^sub>t B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> tfr\<^sub>s\<^sub>e\<^sub>t A"
  "\<And>A B. tfr\<^sub>s\<^sub>e\<^sub>t B \<Longrightarrow> SMP A \<subseteq> SMP B \<Longrightarrow> tfr\<^sub>s\<^sub>e\<^sub>t A"
proof -
  show 1: "tfr\<^sub>s\<^sub>e\<^sub>t (A \<union> B) \<Longrightarrow> tfr\<^sub>s\<^sub>e\<^sub>t A" for A B
    using SMP_union[of A B] unfolding tfr\<^sub>s\<^sub>e\<^sub>t_def by simp

  fix A B assume B: "tfr\<^sub>s\<^sub>e\<^sub>t B"

  show "A \<subseteq> B \<Longrightarrow> tfr\<^sub>s\<^sub>e\<^sub>t A"
  proof -
    assume "A \<subseteq> B"
    then obtain C where "B = A \<union> C" by moura
    thus ?thesis using B 1 by blast
  qed

  show "SMP A \<subseteq> SMP B \<Longrightarrow> tfr\<^sub>s\<^sub>e\<^sub>t A"
  proof -
    assume "SMP A \<subseteq> SMP B"
    then obtain C where "SMP B = SMP A \<union> C" by moura
    thus ?thesis using B unfolding tfr\<^sub>s\<^sub>e\<^sub>t_def by blast
  qed
qed

lemma tfr_empty[simp]: "tfr\<^sub>s\<^sub>e\<^sub>t {}"
unfolding tfr\<^sub>s\<^sub>e\<^sub>t_def by simp

lemma tfr_consts_mono:
  assumes "\<forall>t \<in> M. \<exists>c. t = Fun c []"
    and "\<forall>t \<in> M. Ana t = ([], [])"
    and "tfr\<^sub>s\<^sub>e\<^sub>t N"
  shows "tfr\<^sub>s\<^sub>e\<^sub>t (N \<union> M)"
proof -
  { fix s t
    assume *: "s \<in> SMP (N \<union> M) - range Var" "t \<in> SMP (N \<union> M) - range Var" "\<exists>\<delta>. Unifier \<delta> s t"
    hence **: "is_Fun s" "is_Fun t" "s \<in> SMP N \<or> s \<in> M" "t \<in> SMP N \<or> t \<in> M"
      using assms(3) SMP_consts[OF assms(1,2)] SMP_union[of N M] by auto
    moreover have "\<Gamma> s = \<Gamma> t" when "s \<in> SMP N" "t \<in> SMP N"
      using that assms(3) *(3) **(1,2) unfolding tfr\<^sub>s\<^sub>e\<^sub>t_def by blast
    moreover have "\<Gamma> s = \<Gamma> t" when st: "s \<in> M" "t \<in> M"
    proof -
      obtain c d where "s = Fun c []" "t = Fun d []" using st assms(1) by moura
      hence "s = t" using *(3) by fast
      thus ?thesis by metis
    qed
    moreover have "\<Gamma> s = \<Gamma> t" when st: "s \<in> SMP N" "t \<in> M"
    proof -
      obtain c where "t = Fun c []" using st assms(1) by moura
      hence "s = t" using *(3) **(1,2) by auto
      thus ?thesis by metis
    qed
    moreover have "\<Gamma> s = \<Gamma> t" when st: "s \<in> M" "t \<in> SMP N"
    proof -
      obtain c where "s = Fun c []" using st assms(1) by moura
      hence "s = t" using *(3) **(1,2) by auto
      thus ?thesis by metis
    qed
    ultimately have "\<Gamma> s = \<Gamma> t" by metis
  } thus ?thesis by (metis tfr\<^sub>s\<^sub>e\<^sub>t_def)
qed

lemma dual\<^sub>s\<^sub>t_tfr\<^sub>s\<^sub>t\<^sub>p: "list_all tfr\<^sub>s\<^sub>t\<^sub>p S \<Longrightarrow> list_all tfr\<^sub>s\<^sub>t\<^sub>p (dual\<^sub>s\<^sub>t S)"
proof (induction S)
  case (Cons x S)
  have "list_all tfr\<^sub>s\<^sub>t\<^sub>p S" using Cons.prems by simp
  hence IH: "list_all tfr\<^sub>s\<^sub>t\<^sub>p (dual\<^sub>s\<^sub>t S)" using Cons.IH by metis
  from Cons show ?case
  proof (cases x)
    case (Equality a t t')
    hence "(\<exists>\<delta>. Unifier \<delta> t t') \<Longrightarrow> \<Gamma> t = \<Gamma> t'" using Cons by auto
    thus ?thesis using Equality IH by fastforce
  next
    case (Inequality X F)
    have "set (dual\<^sub>s\<^sub>t (x#S)) = insert x (set (dual\<^sub>s\<^sub>t S))" using Inequality by auto
    moreover have "(\<forall>x \<in> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F - set X. \<exists>a. \<Gamma> (Var x) = Var a) \<or>
            (\<forall>f T. Fun f T \<in> subterms\<^sub>s\<^sub>e\<^sub>t (trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F) \<longrightarrow> T = [] \<or> (\<exists>s \<in> set T. s \<notin> Var ` set X))" 
      using Cons.prems Inequality by auto
    ultimately show ?thesis using Inequality IH by auto
  qed auto
qed simp

lemma subst_var_inv_wt:
  assumes "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>"
  shows "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (subst_var_inv \<delta> X)"
using assms f_inv_into_f[of _ \<delta> X]
unfolding wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def subst_var_inv_def
by presburger

lemma subst_var_inv_wf_trms:
  "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range (subst_var_inv \<delta> X))"
using f_inv_into_f[of _ \<delta> X]
unfolding wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def subst_var_inv_def
by auto

lemma unify_list_wt_if_same_type:
  assumes "Unification.unify E B = Some U" "\<forall>(s,t) \<in> set E. wf\<^sub>t\<^sub>r\<^sub>m s \<and> wf\<^sub>t\<^sub>r\<^sub>m t \<and> \<Gamma> s = \<Gamma> t"
  and "\<forall>(v,t) \<in> set B. \<Gamma> (Var v) = \<Gamma> t"
  shows "\<forall>(v,t) \<in> set U. \<Gamma> (Var v) = \<Gamma> t"
using assms
proof (induction E B arbitrary: U rule: Unification.unify.induct)
  case (2 f X g Y E B U)
  hence "wf\<^sub>t\<^sub>r\<^sub>m (Fun f X)" "wf\<^sub>t\<^sub>r\<^sub>m (Fun g Y)" "\<Gamma> (Fun f X) = \<Gamma> (Fun g Y)" by auto

  from "2.prems"(1) obtain E' where *: "decompose (Fun f X) (Fun g Y) = Some E'"
    and [simp]: "f = g" "length X = length Y" "E' = zip X Y"
    and **: "Unification.unify (E'@E) B = Some U"
    by (auto split: option.splits)
  
  have "\<forall>(s,t) \<in> set E'. wf\<^sub>t\<^sub>r\<^sub>m s \<and> wf\<^sub>t\<^sub>r\<^sub>m t \<and> \<Gamma> s = \<Gamma> t"
  proof -
    { fix s t assume "(s,t) \<in> set E'"
      then obtain X' X'' Y' Y'' where "X = X'@s#X''" "Y = Y'@t#Y''" "length X' = length Y'"
        using zip_arg_subterm_split[of s t X Y] \<open>E' = zip X Y\<close> by metis
      hence "\<Gamma> (Fun f (X'@s#X'')) = \<Gamma> (Fun g (Y'@t#Y''))" by (metis \<open>\<Gamma> (Fun f X) = \<Gamma> (Fun g Y)\<close>)
      
      from \<open>E' = zip X Y\<close> have "\<forall>(s,t) \<in> set E'. s \<sqsubset> Fun f X \<and> t \<sqsubset> Fun g Y"
        using zip_arg_subterm[of _ _ X Y] by blast
      with \<open>(s,t) \<in> set E'\<close> have "wf\<^sub>t\<^sub>r\<^sub>m s" "wf\<^sub>t\<^sub>r\<^sub>m t"
        using wf_trm_subterm \<open>wf\<^sub>t\<^sub>r\<^sub>m (Fun f X)\<close> \<open>wf\<^sub>t\<^sub>r\<^sub>m (Fun g Y)\<close> by (blast,blast)
      moreover have "f \<in> \<Sigma>\<^sub>f"
      proof (rule ccontr)
        assume "f \<notin> \<Sigma>\<^sub>f"
        hence "f \<in> \<C>" "arity f = 0" using const_arity_eq_zero[of f] by simp_all
        thus False using \<open>wf\<^sub>t\<^sub>r\<^sub>m (Fun f X)\<close> * \<open>(s,t) \<in> set E'\<close> unfolding wf\<^sub>t\<^sub>r\<^sub>m_def by auto
      qed
      hence "\<Gamma> s = \<Gamma> t"
        using fun_type_arg_cong' \<open>f \<in> \<Sigma>\<^sub>f\<close> \<open>\<Gamma> (Fun f (X'@s#X'')) = \<Gamma> (Fun g (Y'@t#Y''))\<close>
              \<open>length X' = length Y'\<close> \<open>f = g\<close>
        by metis
      ultimately have "wf\<^sub>t\<^sub>r\<^sub>m s" "wf\<^sub>t\<^sub>r\<^sub>m t" "\<Gamma> s = \<Gamma> t" by metis+
    }
    thus ?thesis by blast
  qed
  moreover have "\<forall>(s,t) \<in> set E. wf\<^sub>t\<^sub>r\<^sub>m s \<and> wf\<^sub>t\<^sub>r\<^sub>m t \<and> \<Gamma> s = \<Gamma> t" using "2.prems"(2) by auto
  ultimately show ?case using "2.IH"[OF * ** _ "2.prems"(3)] by fastforce
next
  case (3 v t E B U)
  hence "\<Gamma> (Var v) = \<Gamma> t" "wf\<^sub>t\<^sub>r\<^sub>m t" by auto
  hence "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (subst v t)"
      and *: "\<forall>(v, t) \<in> set ((v,t)#B). \<Gamma> (Var v) = \<Gamma> t"
             "\<And>t t'. (t,t') \<in> set E \<Longrightarrow> \<Gamma> t = \<Gamma> t'"
    using "3.prems"(2,3) unfolding wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def subst_def by auto

  show ?case
  proof (cases "t = Var v")
    assume "t = Var v" thus ?case using 3 by auto
  next
    assume "t \<noteq> Var v"
    hence "v \<notin> fv t" using "3.prems"(1) by auto
    hence **: "Unification.unify (subst_list (subst v t) E) ((v, t)#B) = Some U"
      using Unification.unify.simps(3)[of v t E B] "3.prems"(1) \<open>t \<noteq> Var v\<close> by auto
    
    have "\<forall>(s, t) \<in> set (subst_list (subst v t) E). wf\<^sub>t\<^sub>r\<^sub>m s \<and> wf\<^sub>t\<^sub>r\<^sub>m t"
      using wf_trm_subst_singleton[OF _ \<open>wf\<^sub>t\<^sub>r\<^sub>m t\<close>] "3.prems"(2)
      unfolding subst_list_def subst_def by auto
    moreover have "\<forall>(s, t) \<in> set (subst_list (subst v t) E). \<Gamma> s = \<Gamma> t"
      using *(2)[THEN wt_subst_trm'[OF \<open>wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (subst v t)\<close>]] by (simp add: subst_list_def)
    ultimately show ?thesis using "3.IH"(2)[OF \<open>t \<noteq> Var v\<close> \<open>v \<notin> fv t\<close> ** _ *(1)] by auto
  qed
next
  case (4 f X v E B U)
  hence "\<Gamma> (Var v) = \<Gamma> (Fun f X)" "wf\<^sub>t\<^sub>r\<^sub>m (Fun f X)" by auto
  hence "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (subst v (Fun f X))"
      and *: "\<forall>(v, t) \<in> set ((v,(Fun f X))#B). \<Gamma> (Var v) = \<Gamma> t"
             "\<And>t t'. (t,t') \<in> set E \<Longrightarrow> \<Gamma> t = \<Gamma> t'"
    using "4.prems"(2,3) unfolding wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def subst_def by auto

  have "v \<notin> fv (Fun f X)" using "4.prems"(1) by force
  hence **: "Unification.unify (subst_list (subst v (Fun f X)) E) ((v, (Fun f X))#B) = Some U"
    using Unification.unify.simps(3)[of v "Fun f X" E B] "4.prems"(1) by auto
  
  have "\<forall>(s, t) \<in> set (subst_list (subst v (Fun f X)) E). wf\<^sub>t\<^sub>r\<^sub>m s \<and> wf\<^sub>t\<^sub>r\<^sub>m t"
    using wf_trm_subst_singleton[OF _ \<open>wf\<^sub>t\<^sub>r\<^sub>m (Fun f X)\<close>] "4.prems"(2)
    unfolding subst_list_def subst_def by auto
  moreover have "\<forall>(s, t) \<in> set (subst_list (subst v (Fun f X)) E). \<Gamma> s = \<Gamma> t"
    using *(2)[THEN wt_subst_trm'[OF \<open>wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (subst v (Fun f X))\<close>]] by (simp add: subst_list_def)
  ultimately show ?case using "4.IH"[OF \<open>v \<notin> fv (Fun f X)\<close> ** _ *(1)] by auto
qed auto

lemma mgu_wt_if_same_type:
  assumes "mgu s t = Some \<sigma>" "wf\<^sub>t\<^sub>r\<^sub>m s" "wf\<^sub>t\<^sub>r\<^sub>m t" "\<Gamma> s = \<Gamma> t"
  shows "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>"
proof -
  let ?fv_disj = "\<lambda>v t S. \<not>(\<exists>(v',t') \<in> S - {(v,t)}. (insert v (fv t)) \<inter> (insert v' (fv t')) \<noteq> {})"

  from assms(1) obtain \<sigma>' where "Unification.unify [(s,t)] [] = Some \<sigma>'" "subst_of \<sigma>' = \<sigma>"
    by (auto split: option.splits)
  hence "\<forall>(v,t) \<in> set \<sigma>'. \<Gamma> (Var v) = \<Gamma> t" "distinct (map fst \<sigma>')"
    using assms(2,3,4) unify_list_wt_if_same_type unify_list_distinct[of "[(s,t)]"] by auto
  thus "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>" using \<open>subst_of \<sigma>' = \<sigma>\<close> unfolding wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def
  proof (induction \<sigma>' arbitrary: \<sigma> rule: List.rev_induct)
    case (snoc tt \<sigma>' \<sigma>)
    then obtain v t where tt: "tt = (v,t)" by (metis surj_pair)
    hence \<sigma>: "\<sigma> = subst v t \<circ>\<^sub>s subst_of \<sigma>'" using snoc.prems(3) by simp
    
    have "\<forall>(v,t) \<in> set \<sigma>'. \<Gamma> (Var v) = \<Gamma> t" "distinct (map fst \<sigma>')" using snoc.prems(1,2) by auto
    then obtain \<sigma>'' where \<sigma>'': "subst_of \<sigma>' = \<sigma>''" "\<forall>v. \<Gamma> (Var v) = \<Gamma> (\<sigma>'' v)" by (metis snoc.IH)
    hence "\<Gamma> t = \<Gamma> (t \<cdot> \<sigma>'')" for t using wt_subst_trm by blast
    hence "\<Gamma> (Var v) = \<Gamma> (\<sigma>'' v)" "\<Gamma> t = \<Gamma> (t \<cdot> \<sigma>'')" using \<sigma>''(2) by auto
    moreover have "\<Gamma> (Var v) = \<Gamma> t" using snoc.prems(1) tt by simp
    moreover have \<sigma>2: "\<sigma> = Var(v := t) \<circ>\<^sub>s \<sigma>'' " using \<sigma> \<sigma>''(1) unfolding subst_def by simp
    ultimately have "\<Gamma> (Var v) = \<Gamma> (\<sigma> v)" unfolding subst_compose_def by simp

    have "subst_domain (subst v t) \<subseteq> {v}" unfolding subst_def by (auto simp add: subst_domain_def)
    hence *: "subst_domain \<sigma> \<subseteq> insert v (subst_domain \<sigma>'')"
      using tt \<sigma> \<sigma>''(1) snoc.prems(2) subst_domain_compose[of _ \<sigma>'']
      by (auto simp add: subst_domain_def)
    
    have "v \<notin> set (map fst \<sigma>')" using tt snoc.prems(2) by auto
    hence "v \<notin> subst_domain \<sigma>''" using \<sigma>''(1) subst_of_dom_subset[of \<sigma>'] by auto

    { fix w assume "w \<in> subst_domain \<sigma>''"
      hence "\<sigma> w = \<sigma>'' w" using \<sigma>2 \<sigma>''(1) \<open>v \<notin> subst_domain \<sigma>''\<close> unfolding subst_compose_def by auto
      hence "\<Gamma> (Var w) = \<Gamma> (\<sigma> w)" using \<sigma>''(2) by simp
    }
    thus ?case using \<open>\<Gamma> (Var v) = \<Gamma> (\<sigma> v)\<close> * by force
  qed simp
qed

lemma wt_Unifier_if_Unifier:
  assumes s_t: "wf\<^sub>t\<^sub>r\<^sub>m s" "wf\<^sub>t\<^sub>r\<^sub>m t" "\<Gamma> s = \<Gamma> t"
    and \<delta>: "Unifier \<delta> s t"
  shows "\<exists>\<theta>. Unifier \<theta> s t \<and> wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<and> wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<theta>)"
using mgu_always_unifies[OF \<delta>] mgu_gives_MGU[THEN MGU_is_Unifier[of s _ t]]
      mgu_wt_if_same_type[OF _ s_t] mgu_wf_trm[OF _ s_t(1,2)] wf_trm_subst_range_iff
by fast

end


subsection \<open>Automatically Proving Type-Flaw Resistance\<close>
subsubsection \<open>Definitions: Variable Renaming\<close>
abbreviation "max_var t \<equiv> Max (insert 0 (snd ` fv t))"
abbreviation "max_var_set X \<equiv> Max (insert 0 (snd ` X))"

definition "var_rename n v \<equiv> Var (fst v, snd v + Suc n)"
definition "var_rename_inv n v \<equiv> Var (fst v, snd v - Suc n)"


subsubsection \<open>Definitions: Computing a Finite Representation of the Sub-Message Patterns\<close>
text \<open>A sufficient requirement for a term to be a well-typed instance of another term\<close>
definition is_wt_instance_of_cond where
  "is_wt_instance_of_cond \<Gamma> t s \<equiv> (
    \<Gamma> t = \<Gamma> s \<and> (case mgu t s of
      None \<Rightarrow> False
    | Some \<delta> \<Rightarrow> inj_on \<delta> (fv t) \<and> (\<forall>x \<in> fv t. is_Var (\<delta> x))))"

definition has_all_wt_instances_of where
  "has_all_wt_instances_of \<Gamma> N M \<equiv> \<forall>t \<in> N. \<exists>s \<in> M. is_wt_instance_of_cond \<Gamma> t s"

text \<open>This function computes a finite representation of the set of sub-message patterns\<close>
definition SMP0 where
  "SMP0 Ana \<Gamma> M \<equiv> let
      f = \<lambda>t. Fun (the_Fun (\<Gamma> t)) (map Var (zip (args (\<Gamma> t)) [0..<length (args (\<Gamma> t))]));
      g = \<lambda>M'. map f (filter (\<lambda>t. is_Var t \<and> is_Fun (\<Gamma> t)) M')@
               concat (map (fst \<circ> Ana) M')@concat (map subterms_list M');
      h = remdups \<circ> g
    in while (\<lambda>A. set (h A) \<noteq> set A) h M"

text \<open>These definitions are useful to refine an SMP representation set\<close>
fun generalize_term where
  "generalize_term _ _ n (Var x) = (Var x, n)"
| "generalize_term \<Gamma> p n (Fun f T) = (let \<tau> = \<Gamma> (Fun f T)
    in if p \<tau> then (Var (\<tau>, n), Suc n)
       else let (T',n') = foldr (\<lambda>t (S,m). let (t',m') = generalize_term \<Gamma> p m t in (t'#S,m'))
                                T ([],n)
            in (Fun f T', n'))"

definition generalize_terms where
  "generalize_terms \<Gamma> p \<equiv> map (fst \<circ> generalize_term \<Gamma> p 0)"

definition remove_superfluous_terms where
  "remove_superfluous_terms \<Gamma> T \<equiv>
    let
      f = \<lambda>S t R. \<exists>s \<in> set S - R. s \<noteq> t \<and> is_wt_instance_of_cond \<Gamma> t s;
      g = \<lambda>S t (U,R). if f S t R then (U, insert t R) else (t#U, R);
      h = \<lambda>S. remdups (fst (foldr (g S) S ([],{})))
    in while (\<lambda>S. h S \<noteq> S) h T"


subsubsection \<open>Definitions: Checking Type-Flaw Resistance\<close>
definition is_TComp_var_instance_closed where
  "is_TComp_var_instance_closed \<Gamma> M \<equiv> \<forall>x \<in> fv\<^sub>s\<^sub>e\<^sub>t (set M). is_Fun (\<Gamma> (Var x)) \<longrightarrow>
      list_ex (\<lambda>t. is_Fun t \<and> \<Gamma> t = \<Gamma> (Var x) \<and> list_all is_Var (args t) \<and> distinct (args t)) M"

definition finite_SMP_representation where
  "finite_SMP_representation arity Ana \<Gamma> M \<equiv>
    list_all (wf\<^sub>t\<^sub>r\<^sub>m' arity) M \<and>
    has_all_wt_instances_of \<Gamma> (subterms\<^sub>s\<^sub>e\<^sub>t (set M)) (set M) \<and>
    has_all_wt_instances_of \<Gamma> (\<Union>((set \<circ> fst \<circ> Ana) ` set M)) (set M) \<and>
    is_TComp_var_instance_closed \<Gamma> M"

definition comp_tfr\<^sub>s\<^sub>e\<^sub>t where
  "comp_tfr\<^sub>s\<^sub>e\<^sub>t arity Ana \<Gamma> M \<equiv>
    finite_SMP_representation arity Ana \<Gamma> M \<and>
    (let \<delta> = var_rename (max_var_set (fv\<^sub>s\<^sub>e\<^sub>t (set M)))
     in \<forall>s \<in> set M. \<forall>t \<in> set M. is_Fun s \<and> is_Fun t \<and> \<Gamma> s \<noteq> \<Gamma> t \<longrightarrow> mgu s (t \<cdot> \<delta>) = None)"

fun comp_tfr\<^sub>s\<^sub>t\<^sub>p where
  "comp_tfr\<^sub>s\<^sub>t\<^sub>p \<Gamma> (\<langle>_: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t) = (mgu t t' \<noteq> None \<longrightarrow> \<Gamma> t = \<Gamma> t')"
| "comp_tfr\<^sub>s\<^sub>t\<^sub>p \<Gamma> (\<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t) = (
    (\<forall>x \<in> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F - set X. is_Var (\<Gamma> (Var x))) \<or>
    (\<forall>u \<in> subterms\<^sub>s\<^sub>e\<^sub>t (trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F).
      is_Fun u \<longrightarrow> (args u = [] \<or> (\<exists>s \<in> set (args u). s \<notin> Var ` set X))))"
| "comp_tfr\<^sub>s\<^sub>t\<^sub>p _ _ = True"

definition comp_tfr\<^sub>s\<^sub>t where
  "comp_tfr\<^sub>s\<^sub>t arity Ana \<Gamma> M S \<equiv>
    list_all (comp_tfr\<^sub>s\<^sub>t\<^sub>p \<Gamma>) S \<and>
    list_all (wf\<^sub>t\<^sub>r\<^sub>m' arity) (trms_list\<^sub>s\<^sub>t S) \<and>
    has_all_wt_instances_of \<Gamma> (trms\<^sub>s\<^sub>t S) (set M) \<and>
    comp_tfr\<^sub>s\<^sub>e\<^sub>t arity Ana \<Gamma> M"


subsubsection \<open>Small Lemmata\<close>
lemma less_Suc_max_var_set:
  assumes z: "z \<in> X"
    and X: "finite X"
  shows "snd z < Suc (max_var_set X)"
proof -
  have "snd z \<in> snd ` X" using z by simp
  hence "snd z \<le> Max (insert 0 (snd ` X))" using X by simp
  thus ?thesis using X by simp
qed

lemma (in typed_model) finite_SMP_representationD:
  assumes "finite_SMP_representation arity Ana \<Gamma> M"
  shows "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (set M)"
    and "has_all_wt_instances_of \<Gamma> (subterms\<^sub>s\<^sub>e\<^sub>t (set M)) (set M)"
    and "has_all_wt_instances_of \<Gamma> (\<Union>((set \<circ> fst \<circ> Ana) ` set M)) (set M)"
    and "is_TComp_var_instance_closed \<Gamma> M"
using assms unfolding finite_SMP_representation_def list_all_iff wf\<^sub>t\<^sub>r\<^sub>m_code by blast+

lemma (in typed_model) is_wt_instance_of_condD:
  assumes t_instance_s: "is_wt_instance_of_cond \<Gamma> t s"
  obtains \<delta> where
    "\<Gamma> t = \<Gamma> s" "mgu t s = Some \<delta>"
    "inj_on \<delta> (fv t)" "\<delta> ` (fv t) \<subseteq> range Var"
using t_instance_s unfolding is_wt_instance_of_cond_def Let_def by (cases "mgu t s") fastforce+

lemma (in typed_model) is_wt_instance_of_condD':
  assumes t_wf_trm: "wf\<^sub>t\<^sub>r\<^sub>m t"
    and s_wf_trm: "wf\<^sub>t\<^sub>r\<^sub>m s"
    and t_instance_s: "is_wt_instance_of_cond \<Gamma> t s"
  shows "\<exists>\<delta>. wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<and> wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<delta>) \<and> t = s \<cdot> \<delta>"
proof -
  obtain \<delta> where s:
      "\<Gamma> t = \<Gamma> s" "mgu t s = Some \<delta>"
      "inj_on \<delta> (fv t)" "\<delta> ` (fv t) \<subseteq> range Var"
    by (metis is_wt_instance_of_condD[OF t_instance_s])

  have 0: "wf\<^sub>t\<^sub>r\<^sub>m t" "wf\<^sub>t\<^sub>r\<^sub>m s" using s(1) t_wf_trm s_wf_trm by auto

  note 1 = mgu_wt_if_same_type[OF s(2) 0 s(1)]

  note 2 = conjunct1[OF mgu_gives_MGU[OF s(2)]]

  show ?thesis
    using s(1) inj_var_ran_unifiable_has_subst_match[OF 2 s(3,4)]
          wt_subst_compose[OF 1 subst_var_inv_wt[OF 1, of "fv t"]]
          wf_trms_subst_compose[OF mgu_wf_trms[OF s(2) 0] subst_var_inv_wf_trms[of \<delta> "fv t"]]
    by auto
qed

lemma (in typed_model) is_wt_instance_of_condD'':
  assumes s_wf_trm: "wf\<^sub>t\<^sub>r\<^sub>m s"
    and t_instance_s: "is_wt_instance_of_cond \<Gamma> t s"
    and t_var: "t = Var x"
  shows "\<exists>y. s = Var y \<and> \<Gamma> (Var y) = \<Gamma> (Var x)"
proof -
  obtain \<delta> where \<delta>: "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>" and s: "Var x = s \<cdot> \<delta>"
    using is_wt_instance_of_condD'[OF _ s_wf_trm t_instance_s] t_var by auto
  obtain y where y: "s = Var y" using s by (cases s) auto
  show ?thesis using wt_subst_trm''[OF \<delta>] s y by metis
qed

lemma (in typed_model) has_all_wt_instances_ofD:
  assumes N_instance_M: "has_all_wt_instances_of \<Gamma> N M"
    and t_in_N: "t \<in> N"
  obtains s \<delta> where
    "s \<in> M" "\<Gamma> t = \<Gamma> s" "mgu t s = Some \<delta>"
    "inj_on \<delta> (fv t)" "\<delta> ` (fv t) \<subseteq> range Var"
by (metis t_in_N N_instance_M is_wt_instance_of_condD has_all_wt_instances_of_def)

lemma (in typed_model) has_all_wt_instances_ofD':
  assumes N_wf_trms: "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s N"
    and M_wf_trms: "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s M"
    and N_instance_M: "has_all_wt_instances_of \<Gamma> N M"
    and t_in_N: "t \<in> N"
  shows "\<exists>\<delta>. wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<and> wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<delta>) \<and> t \<in> M \<cdot>\<^sub>s\<^sub>e\<^sub>t \<delta>"
using assms is_wt_instance_of_condD' unfolding has_all_wt_instances_of_def by fast

lemma (in typed_model) has_all_wt_instances_ofD'':
  assumes N_wf_trms: "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s N"
    and M_wf_trms: "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s M"
    and N_instance_M: "has_all_wt_instances_of \<Gamma> N M"
    and t_in_N: "Var x \<in> N"
  shows "\<exists>y. Var y \<in> M \<and> \<Gamma> (Var y) = \<Gamma> (Var x)"
using assms is_wt_instance_of_condD'' unfolding has_all_wt_instances_of_def by fast
  
lemma (in typed_model) has_all_instances_of_if_subset:
  assumes "N \<subseteq> M"
  shows "has_all_wt_instances_of \<Gamma> N M"
using assms inj_onI mgu_same_empty
unfolding has_all_wt_instances_of_def is_wt_instance_of_cond_def
by (smt option.case_eq_if option.discI option.sel subsetD term.discI(1) term.inject(1))

lemma (in typed_model) SMP_I':
  assumes N_wf_trms: "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s N"
    and M_wf_trms: "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s M"
    and N_instance_M: "has_all_wt_instances_of \<Gamma> N M"
    and t_in_N: "t \<in> N"
  shows "t \<in> SMP M"
using has_all_wt_instances_ofD'[OF N_wf_trms M_wf_trms N_instance_M t_in_N]
      SMP.Substitution[OF SMP.MP[of _ M]]
by blast


subsubsection \<open>Lemma: Proving Type-Flaw Resistance\<close>
locale typed_model' = typed_model arity public Ana \<Gamma>
  for arity::"'fun \<Rightarrow> nat"
    and public::"'fun \<Rightarrow> bool"
    and Ana::"('fun,(('fun,'atom::finite) term_type \<times> nat)) term
              \<Rightarrow> (('fun,(('fun,'atom) term_type \<times> nat)) term list
                 \<times> ('fun,(('fun,'atom) term_type \<times> nat)) term list)"
    and \<Gamma>::"('fun,(('fun,'atom) term_type \<times> nat)) term \<Rightarrow> ('fun,'atom) term_type"
  +
  assumes \<Gamma>_Var_fst: "\<And>\<tau> n m. \<Gamma> (Var (\<tau>,n)) = \<Gamma> (Var (\<tau>,m))"
    and Ana_const: "\<And>c T. arity c = 0 \<Longrightarrow> Ana (Fun c T) = ([],[])"
    and Ana_subst'_or_Ana_keys_subterm:
      "(\<forall>f T \<delta> K R. Ana (Fun f T) = (K,R) \<longrightarrow> Ana (Fun f T \<cdot> \<delta>) = (K \<cdot>\<^sub>l\<^sub>i\<^sub>s\<^sub>t \<delta>,R \<cdot>\<^sub>l\<^sub>i\<^sub>s\<^sub>t \<delta>)) \<or>
       (\<forall>t K R k. Ana t = (K,R) \<longrightarrow> k \<in> set K \<longrightarrow> k \<sqsubset> t)"
begin

lemma var_rename_inv_comp: "t \<cdot> (var_rename n \<circ>\<^sub>s var_rename_inv n) = t"
proof (induction t)
  case (Fun f T)
  hence "map (\<lambda>t. t \<cdot> var_rename n \<circ>\<^sub>s var_rename_inv n) T = T" by (simp add: map_idI) 
  thus ?case by (metis subst_apply_term.simps(2)) 
qed (simp add: var_rename_def var_rename_inv_def)

lemma var_rename_fv_disjoint:
  "fv s \<inter> fv (t \<cdot> var_rename (max_var s)) = {}"
proof -
  have 1: "\<forall>v \<in> fv s. snd v \<le> max_var s" by simp
  have 2: "\<forall>v \<in> fv (t \<cdot> var_rename n). snd v > n" for n unfolding var_rename_def by (induct t) auto
  show ?thesis using 1 2 by force
qed

lemma var_rename_fv_set_disjoint:
  assumes "finite M" "s \<in> M"
  shows "fv s \<inter> fv (t \<cdot> var_rename (max_var_set (fv\<^sub>s\<^sub>e\<^sub>t M))) = {}"
proof -
  have 1: "\<forall>v \<in> fv s. snd v \<le> max_var_set (fv\<^sub>s\<^sub>e\<^sub>t M)" using assms
  proof (induction M rule: finite_induct)
    case (insert t M) thus ?case
    proof (cases "t = s")
      case False
      hence "\<forall>v \<in> fv s. snd v \<le> max_var_set (fv\<^sub>s\<^sub>e\<^sub>t M)" using insert by simp
      moreover have "max_var_set (fv\<^sub>s\<^sub>e\<^sub>t M) \<le> max_var_set (fv\<^sub>s\<^sub>e\<^sub>t (insert t M))"
        using insert.hyps(1) insert.prems
        by force
      ultimately show ?thesis by auto
    qed simp
  qed simp

  have 2: "\<forall>v \<in> fv (t \<cdot> var_rename n). snd v > n" for n unfolding var_rename_def by (induct t) auto

  show ?thesis using 1 2 by force
qed

lemma var_rename_fv_set_disjoint':
  assumes "finite M"
  shows "fv\<^sub>s\<^sub>e\<^sub>t M \<inter> fv\<^sub>s\<^sub>e\<^sub>t (N \<cdot>\<^sub>s\<^sub>e\<^sub>t var_rename (max_var_set (fv\<^sub>s\<^sub>e\<^sub>t M))) = {}"
using var_rename_fv_set_disjoint[OF assms] by auto

lemma var_rename_is_renaming[simp]:
  "subst_range (var_rename n) \<subseteq> range Var"
  "subst_range (var_rename_inv n) \<subseteq> range Var"
unfolding var_rename_def var_rename_inv_def by auto

lemma var_rename_wt[simp]:
  "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (var_rename n)"
  "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (var_rename_inv n)"
by (auto simp add: var_rename_def var_rename_inv_def wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def \<Gamma>_Var_fst)

lemma var_rename_wt':
  assumes "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>" "s = m \<cdot> \<delta>"
  shows "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (var_rename_inv n \<circ>\<^sub>s \<delta>)" "s = m \<cdot> var_rename n \<cdot> var_rename_inv n \<circ>\<^sub>s \<delta>"
using assms(2) wt_subst_compose[OF var_rename_wt(2)[of n] assms(1)] var_rename_inv_comp[of m n]
by force+

lemma var_rename_wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s_range[simp]:
  "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range (var_rename n))"
  "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range (var_rename_inv n))"
using var_rename_is_renaming by fastforce+

lemma Fun_range_case:
  "(\<forall>f T. Fun f T \<in> M \<longrightarrow> P f T) \<longleftrightarrow> (\<forall>u \<in> M. case u of Fun f T \<Rightarrow> P f T | _ \<Rightarrow> True)"
  "(\<forall>f T. Fun f T \<in> M \<longrightarrow> P f T) \<longleftrightarrow> (\<forall>u \<in> M. is_Fun u \<longrightarrow> P (the_Fun u) (args u))"
by (auto split: "term.splits")

lemma is_TComp_var_instance_closedD:
  assumes x: "\<exists>y \<in> fv\<^sub>s\<^sub>e\<^sub>t (set M). \<Gamma> (Var x) = \<Gamma> (Var y)" "\<Gamma> (Var x) = TComp f T"
    and closed: "is_TComp_var_instance_closed \<Gamma> M"
  shows "\<exists>g U. Fun g U \<in> set M \<and> \<Gamma> (Fun g U) = \<Gamma> (Var x) \<and> (\<forall>u \<in> set U. is_Var u) \<and> distinct U"
using assms unfolding is_TComp_var_instance_closed_def list_all_iff list_ex_iff by fastforce

lemma is_TComp_var_instance_closedD':
  assumes "\<exists>y \<in> fv\<^sub>s\<^sub>e\<^sub>t (set M). \<Gamma> (Var x) = \<Gamma> (Var y)" "TComp f T \<sqsubseteq> \<Gamma> (Var x)"
    and closed: "is_TComp_var_instance_closed \<Gamma> M"
    and wf: "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (set M)"
  shows "\<exists>g U. Fun g U \<in> set M \<and> \<Gamma> (Fun g U) = TComp f T \<and> (\<forall>u \<in> set U. is_Var u) \<and> distinct U"
using assms(1,2)
proof (induction "\<Gamma> (Var x)" arbitrary: x)
  case (Fun g U)
  note IH = Fun.hyps(1)
  have g: "arity g > 0" "public g" using Fun.hyps(2) fun_type_inv[of "Var x"] \<Gamma>_Var_fst by simp_all
  then obtain V where V:
      "Fun g V \<in> set M" "\<Gamma> (Fun g V) = \<Gamma> (Var x)" "\<forall>v \<in> set V. \<exists>x. v = Var x"
      "distinct V" "length U = length V"
    using is_TComp_var_instance_closedD[OF Fun.prems(1) Fun.hyps(2)[symmetric] closed(1)]
    by (metis Fun.hyps(2) fun_type_id_eq fun_type_length_eq is_VarE)
  hence U: "U = map \<Gamma> V" using fun_type[OF g(1), of V] Fun.hyps(2) by simp
  hence 1: "\<Gamma> v \<in> set U" when v: "v \<in> set V" for v using v by simp

  have 2: "\<exists>y \<in> fv\<^sub>s\<^sub>e\<^sub>t (set M). \<Gamma> (Var z) = \<Gamma> (Var y)" when z: "Var z \<in> set V" for z
    using V(1) fv_subset_subterms Fun_param_in_subterms[OF z] by fastforce

  show ?case
  proof (cases "TComp f T = \<Gamma> (Var x)")
    case False
    then obtain u where u: "u \<in> set U" "TComp f T \<sqsubseteq> u"
      using Fun.prems(2) Fun.hyps(2) by moura
    then obtain y where y: "Var y \<in> set V" "\<Gamma> (Var y) = u" using U V(3) \<Gamma>_Var_fst by auto
    show ?thesis using IH[OF _ 2[OF y(1)]] u y(2) by metis
  qed (use V in fastforce)
qed simp

lemma TComp_var_instance_wt_subst_exists:
  assumes gT: "\<Gamma> (Fun g T) = TComp g (map \<Gamma> U)" "wf\<^sub>t\<^sub>r\<^sub>m (Fun g T)"
    and U: "\<forall>u \<in> set U. \<exists>y. u = Var y" "distinct U"
  shows "\<exists>\<theta>. wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<and> wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<theta>) \<and> Fun g T = Fun g U \<cdot> \<theta>"
proof -
  define the_i where "the_i \<equiv> \<lambda>y. THE x. x < length U \<and> U ! x = Var y"
  define \<theta> where \<theta>: "\<theta> \<equiv> \<lambda>y. if Var y \<in> set U then T ! the_i y else Var y"

  have g: "arity g > 0" using gT(1,2) fun_type_inv(1) by blast

  have UT: "length U = length T" using fun_type_length_eq gT(1) by fastforce

  have 1: "the_i y < length U \<and> U ! the_i y = Var y" when y: "Var y \<in> set U" for y
    using theI'[OF distinct_Ex1[OF U(2) y]] unfolding the_i_def by simp

  have 2: "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>"
    using \<theta> 1 gT(1) fun_type[OF g] UT
    unfolding wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def
    by (metis (no_types, lifting) nth_map term.inject(2))

  have "\<forall>i<length T. U ! i \<cdot> \<theta> = T ! i"
    using \<theta> 1 U(1) UT distinct_Ex1[OF U(2)] in_set_conv_nth
    by (metis (no_types, lifting) subst_apply_term.simps(1))
  hence "T = map (\<lambda>t. t \<cdot> \<theta>) U" by (simp add: UT nth_equalityI)
  hence 3: "Fun g T = Fun g U \<cdot> \<theta>" by simp

  have "subst_range \<theta> \<subseteq> set T" using \<theta> 1 U(1) UT by (auto simp add: subst_domain_def)
  hence 4: "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<theta>)" using gT(2) wf_trm_param by auto

  show ?thesis by (metis 2 3 4)
qed

lemma TComp_var_instance_closed_has_Var:
  assumes closed: "is_TComp_var_instance_closed \<Gamma> M"
    and wf_M: "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (set M)"
    and wf_\<delta>x: "wf\<^sub>t\<^sub>r\<^sub>m (\<delta> x)"
    and y_ex: "\<exists>y \<in> fv\<^sub>s\<^sub>e\<^sub>t (set M). \<Gamma> (Var x) = \<Gamma> (Var y)"
    and t: "t \<sqsubseteq> \<delta> x"
    and \<delta>_wt: "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>"
  shows "\<exists>y \<in> fv\<^sub>s\<^sub>e\<^sub>t (set M). \<Gamma> (Var y) = \<Gamma> t"
proof (cases "\<Gamma> (Var x)")
  case (Var a)
  hence "t = \<delta> x"
    using t wf_\<delta>x \<delta>_wt
    by (metis (full_types) const_type_inv_wf fun_if_subterm subtermeq_Var_const(2) wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def)
  thus ?thesis using y_ex wt_subst_trm''[OF \<delta>_wt, of "Var x"] by fastforce
next
  case (Fun f T)
  hence \<Gamma>_\<delta>x: "\<Gamma> (\<delta> x) = TComp f T" using wt_subst_trm''[OF \<delta>_wt, of "Var x"] by auto

  show ?thesis
  proof (cases "t = \<delta> x")
    case False
    hence t_subt_\<delta>x: "t \<sqsubset> \<delta> x" using t(1) \<Gamma>_\<delta>x by fastforce

    obtain T' where T': "\<delta> x = Fun f T'" using \<Gamma>_\<delta>x t_subt_\<delta>x fun_type_id_eq by (cases "\<delta> x") auto
    
    obtain g S where gS: "Fun g S \<sqsubseteq> \<delta> x" "t \<in> set S" using Fun_ex_if_subterm[OF t_subt_\<delta>x] by blast
  
    have gS_wf: "wf\<^sub>t\<^sub>r\<^sub>m (Fun g S)" by (rule wf_trm_subtermeq[OF wf_\<delta>x gS(1)])
    hence "arity g > 0" using gS(2) by (metis length_pos_if_in_set wf_trm_arity) 
    hence gS_\<Gamma>: "\<Gamma> (Fun g S) = TComp g (map \<Gamma> S)" using fun_type by blast
  
    obtain h U where hU:
        "Fun h U \<in> set M" "\<Gamma> (Fun h U) = Fun g (map \<Gamma> S)" "\<forall>u \<in> set U. is_Var u"
      using is_TComp_var_instance_closedD'[OF y_ex _ closed wf_M]
            subtermeq_imp_subtermtypeeq[OF wf_\<delta>x] gS \<Gamma>_\<delta>x Fun gS_\<Gamma>
      by metis
  
    obtain y where y: "Var y \<in> set U" "\<Gamma> (Var y) = \<Gamma> t"
      using hU(3) fun_type_param_ex[OF hU(2) gS(2)] by fast
  
    have "y \<in> fv\<^sub>s\<^sub>e\<^sub>t (set M)" using hU(1) y(1) by force
    thus ?thesis using y(2) closed by metis
  qed (metis y_ex Fun \<Gamma>_\<delta>x)
qed

lemma TComp_var_instance_closed_has_Fun:
  assumes closed: "is_TComp_var_instance_closed \<Gamma> M"
    and wf_M: "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (set M)"
    and wf_\<delta>x: "wf\<^sub>t\<^sub>r\<^sub>m (\<delta> x)"
    and y_ex: "\<exists>y \<in> fv\<^sub>s\<^sub>e\<^sub>t (set M). \<Gamma> (Var x) = \<Gamma> (Var y)"
    and t: "t \<sqsubseteq> \<delta> x"
    and \<delta>_wt: "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>"
    and t_\<Gamma>: "\<Gamma> t = TComp g T"
    and t_fun: "is_Fun t"
  shows "\<exists>m \<in> set M. \<exists>\<theta>. wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<and> wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<theta>) \<and> t = m \<cdot> \<theta> \<and> is_Fun m"
proof -
  obtain T'' where T'': "t = Fun g T''" using t_\<Gamma> t_fun fun_type_id_eq by blast

  have g: "arity g > 0" using t_\<Gamma> fun_type_inv[of t] by simp_all

  have "TComp g T \<sqsubseteq> \<Gamma> (Var x)" using \<delta>_wt t t_\<Gamma>
    by (metis wf_\<delta>x subtermeq_imp_subtermtypeeq wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def) 
  then obtain U where U:
      "Fun g U \<in> set M" "\<Gamma> (Fun g U) = TComp g T" "\<forall>u \<in> set U. \<exists>y. u = Var y"
      "distinct U" "length T'' = length U"
    using is_TComp_var_instance_closedD'[OF y_ex _ closed wf_M]
    by (metis t_\<Gamma> T'' fun_type_id_eq fun_type_length_eq is_VarE)
  hence UT': "T = map \<Gamma> U" using fun_type[OF g, of U] by simp

  show ?thesis
    using TComp_var_instance_wt_subst_exists UT' T'' U(1,3,4) t t_\<Gamma> wf_\<delta>x wf_trm_subtermeq
    by (metis term.disc(2))
qed

lemma TComp_var_and_subterm_instance_closed_has_subterms_instances:
  assumes M_var_inst_cl: "is_TComp_var_instance_closed \<Gamma> M"
    and M_subterms_cl: "has_all_wt_instances_of \<Gamma> (subterms\<^sub>s\<^sub>e\<^sub>t (set M)) (set M)"
    and M_wf: "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (set M)"
    and t: "t \<sqsubseteq>\<^sub>s\<^sub>e\<^sub>t set M"
    and s: "s \<sqsubseteq> t \<cdot> \<delta>"
    and \<delta>: "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<delta>)"
  shows "\<exists>m \<in> set M. \<exists>\<theta>. wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<and> wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<theta>) \<and> s = m \<cdot> \<theta>"
using subterm_subst_unfold[OF s]
proof
  assume "\<exists>s'. s' \<sqsubseteq> t \<and> s = s' \<cdot> \<delta>"
  then obtain s' where s': "s' \<sqsubseteq> t" "s = s' \<cdot> \<delta>" by blast
  then obtain \<theta> where \<theta>: "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<theta>)" "s' \<in> set M \<cdot>\<^sub>s\<^sub>e\<^sub>t \<theta>"
    using t has_all_wt_instances_ofD'[OF wf_trms_subterms[OF M_wf] M_wf M_subterms_cl]
          term.order_trans[of s' t]
    by blast
  then obtain m where m: "m \<in> set M" "s' = m \<cdot> \<theta>" by blast

  have "s = m \<cdot> (\<theta> \<circ>\<^sub>s \<delta>)" using s'(2) m(2) by simp
  thus ?thesis
    using m(1) wt_subst_compose[OF \<theta>(1) \<delta>(1)] wf_trms_subst_compose[OF \<theta>(2) \<delta>(2)] by blast
next
  assume "\<exists>x \<in> fv t. s \<sqsubset> \<delta> x"
  then obtain x where x: "x \<in> fv t" "s \<sqsubset> \<delta> x" "s \<sqsubseteq> \<delta> x" by blast

  note 0 = TComp_var_instance_closed_has_Var[OF M_var_inst_cl M_wf]
  note 1 = has_all_wt_instances_ofD''[OF wf_trms_subterms[OF M_wf] M_wf M_subterms_cl]

  have \<delta>x_wf: "wf\<^sub>t\<^sub>r\<^sub>m (\<delta> x)" and s_wf_trm: "wf\<^sub>t\<^sub>r\<^sub>m s"
    using \<delta>(2) wf_trm_subterm[OF _ x(2)] by fastforce+

  have x_fv_ex: "\<exists>y \<in> fv\<^sub>s\<^sub>e\<^sub>t (set M). \<Gamma> (Var x) = \<Gamma> (Var y)"
    using x(1) s fv_subset_subterms[OF t] by auto

  obtain y where y: "y \<in> fv\<^sub>s\<^sub>e\<^sub>t (set M)" "\<Gamma> (Var y) = \<Gamma> s"
    using 0[of \<delta> x s, OF \<delta>x_wf x_fv_ex x(3) \<delta>(1)] by metis
  then obtain z where z: "Var z \<in> set M" "\<Gamma> (Var z) = \<Gamma> s"
    using 1[of y] vars_iff_subtermeq_set[of y "set M"] by metis

  define \<theta> where "\<theta> \<equiv> Var(z := s)::('fun, ('fun, 'atom) term \<times> nat) subst"

  have "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<theta>)" "s = Var z \<cdot> \<theta>"
    using z(2) s_wf_trm unfolding \<theta>_def wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by force+
  thus ?thesis using z(1) by blast
qed

context
begin
private lemma SMP_D_aux1:
  assumes "t \<in> SMP (set M)"
    and closed: "has_all_wt_instances_of \<Gamma> (subterms\<^sub>s\<^sub>e\<^sub>t (set M)) (set M)"
                "is_TComp_var_instance_closed \<Gamma> M"
    and wf_M: "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (set M)"
  shows "\<forall>x \<in> fv t. \<exists>y \<in> fv\<^sub>s\<^sub>e\<^sub>t (set M). \<Gamma> (Var y) = \<Gamma> (Var x)"
using assms(1)
proof (induction t rule: SMP.induct)
  case (MP t) show ?case
  proof
    fix x assume x: "x \<in> fv t"
    hence "Var x \<in> subterms\<^sub>s\<^sub>e\<^sub>t (set M)" using MP.hyps vars_iff_subtermeq by fastforce
    then obtain \<delta> s where \<delta>: "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<delta>)"
        and s: "s \<in> set M" "Var x = s \<cdot> \<delta>"
      using has_all_wt_instances_ofD'[OF wf_trms_subterms[OF wf_M] wf_M closed(1)] by blast
    then obtain y where y: "s = Var y" by (cases s) auto
    thus "\<exists>y \<in> fv\<^sub>s\<^sub>e\<^sub>t (set M). \<Gamma> (Var y) = \<Gamma> (Var x)"
      using s wt_subst_trm''[OF \<delta>(1), of "Var y"] by force
  qed
next
  case (Subterm t t')
  hence "fv t' \<subseteq> fv t" using subtermeq_vars_subset by auto
  thus ?case using Subterm.IH by auto
next
  case (Substitution t \<delta>)
  note IH = Substitution.IH
  show ?case
  proof
    fix x assume x: "x \<in> fv (t \<cdot> \<delta>)"
    then obtain y where y: "y \<in> fv t" "\<Gamma> (Var x) \<sqsubseteq> \<Gamma> (Var y)"
      using Substitution.hyps(2,3)
      by (metis subst_apply_img_var subtermeqI' subtermeq_imp_subtermtypeeq
                vars_iff_subtermeq wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def wf_trm_subst_rangeD)
    let ?P = "\<lambda>x. \<exists>y \<in> fv\<^sub>s\<^sub>e\<^sub>t (set M). \<Gamma> (Var y) = \<Gamma> (Var x)"
    show "?P x" using y IH
    proof (induction "\<Gamma> (Var y)" arbitrary: y t)
      case (Var a)
      hence "\<Gamma> (Var x) = \<Gamma> (Var y)" by auto
      thus ?case using Var(2,4) by auto
    next
      case (Fun f T)
      obtain z where z: "\<exists>w \<in> fv\<^sub>s\<^sub>e\<^sub>t (set M). \<Gamma> (Var z) = \<Gamma> (Var w)" "\<Gamma> (Var z) = \<Gamma> (Var y)"
        using Fun.prems(1,3) by blast
      show ?case
      proof (cases "\<Gamma> (Var x) = \<Gamma> (Var y)")
        case True thus ?thesis using Fun.prems by auto
      next
        case False
        then obtain \<tau> where \<tau>: "\<tau> \<in> set T" "\<Gamma> (Var x) \<sqsubseteq> \<tau>" using Fun.prems(2) Fun.hyps(2) by auto
        then obtain U where U:
            "Fun f U \<in> set M" "\<Gamma> (Fun f U) = \<Gamma> (Var z)" "\<forall>u \<in> set U. \<exists>v. u = Var v" "distinct U"
          using is_TComp_var_instance_closedD'[OF z(1) _ closed(2) wf_M] Fun.hyps(2) z(2)
          by (metis fun_type_id_eq subtermeqI' is_VarE)
        hence 1: "\<forall>x \<in> fv (Fun f U). \<exists>y \<in> fv\<^sub>s\<^sub>e\<^sub>t (set M). \<Gamma> (Var y) = \<Gamma> (Var x)" by force

        have "arity f > 0" using U(2) z(2) Fun.hyps(2) fun_type_inv(1) by metis
        hence "\<Gamma> (Fun f U) = TComp f (map \<Gamma> U)" using fun_type by auto
        then obtain u where u: "Var u \<in> set U" "\<Gamma> (Var u) = \<tau>"
          using \<tau>(1) U(2,3) z(2) Fun.hyps(2) by auto
        show ?thesis
          using Fun.hyps(1)[of u "Fun f U"] u \<tau> 1
          by force
      qed
    qed
  qed
next
  case (Ana t K T k)
  have "fv k \<subseteq> fv t" using Ana_keys_fv[OF Ana.hyps(2)] Ana.hyps(3) by auto
  thus ?case using Ana.IH by auto
qed

private lemma SMP_D_aux2:
  fixes t::"('fun, ('fun, 'atom) term \<times> nat) term"
  assumes t_SMP: "t \<in> SMP (set M)"
    and t_Var: "\<exists>x. t = Var x"
    and M_SMP_repr: "finite_SMP_representation arity Ana \<Gamma> M"
  shows "\<exists>m \<in> set M. \<exists>\<delta>. wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<and> wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<delta>) \<and> t = m \<cdot> \<delta>"
proof -
  have M_wf: "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (set M)" 
      and M_var_inst_cl: "is_TComp_var_instance_closed \<Gamma> M"
      and M_subterms_cl: "has_all_wt_instances_of \<Gamma> (subterms\<^sub>s\<^sub>e\<^sub>t (set M)) (set M)"
      and M_Ana_cl: "has_all_wt_instances_of \<Gamma> (\<Union>((set \<circ> fst \<circ> Ana) ` set M)) (set M)"
    using finite_SMP_representationD[OF M_SMP_repr] by blast+

  have M_Ana_wf: "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (\<Union> ((set \<circ> fst \<circ> Ana) ` set M))"
  proof
    fix k assume "k \<in> \<Union>((set \<circ> fst \<circ> Ana) ` set M)"
    then obtain m where m: "m \<in> set M" "k \<in> set (fst (Ana m))" by force
    thus "wf\<^sub>t\<^sub>r\<^sub>m k" using M_wf Ana_keys_wf'[of m "fst (Ana m)" _ k] surjective_pairing by blast
  qed

  note 0 = has_all_wt_instances_ofD'[OF wf_trms_subterms[OF M_wf] M_wf M_subterms_cl]
  note 1 = has_all_wt_instances_ofD'[OF M_Ana_wf M_wf M_Ana_cl]

  obtain x y where x: "t = Var x" and y: "y \<in> fv\<^sub>s\<^sub>e\<^sub>t (set M)" "\<Gamma> (Var y) = \<Gamma> (Var x)"
    using t_Var SMP_D_aux1[OF t_SMP M_subterms_cl M_var_inst_cl M_wf] by fastforce
  then obtain m \<delta> where m: "m \<in> set M" "m \<cdot> \<delta> = Var y" and \<delta>: "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>"
    using 0[of "Var y"] vars_iff_subtermeq_set[of y "set M"] by fastforce
  obtain z where z: "m = Var z" using m(2) by (cases m) auto

  define \<theta> where "\<theta> \<equiv> Var(z := Var x)::('fun, ('fun, 'atom) term \<times> nat) subst"

  have "\<Gamma> (Var z) = \<Gamma> (Var x)" using y(2) m(2) z wt_subst_trm''[OF \<delta>, of m] by argo
  hence "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<theta>)" unfolding \<theta>_def wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by force+
  moreover have "t = m \<cdot> \<theta>" using x z unfolding \<theta>_def by simp
  ultimately show ?thesis using m(1) by blast
qed

private lemma SMP_D_aux3:
  assumes hyps: "t' \<sqsubseteq> t" and wf_t: "wf\<^sub>t\<^sub>r\<^sub>m t" and prems: "is_Fun t'"
    and IH:
      "((\<exists>f. t = Fun f []) \<and> (\<exists>m \<in> set M. \<exists>\<delta>. wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<and> wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<delta>) \<and> t = m \<cdot> \<delta>)) \<or>
       (\<exists>m \<in> set M. \<exists>\<delta>. wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<and> wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<delta>) \<and> t = m \<cdot> \<delta> \<and> is_Fun m)"
    and M_SMP_repr: "finite_SMP_representation arity Ana \<Gamma> M"
  shows "((\<exists>f. t' = Fun f []) \<and> (\<exists>m \<in> set M. \<exists>\<delta>. wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<and> wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<delta>) \<and> t' = m \<cdot> \<delta>)) \<or>
         (\<exists>m \<in> set M. \<exists>\<delta>. wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<and> wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<delta>) \<and> t' = m \<cdot> \<delta> \<and> is_Fun m)"
proof (cases "\<exists>f. t = Fun f [] \<or> t' = Fun f []")
  case True
  have M_wf: "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (set M)" 
    and M_var_inst_cl: "is_TComp_var_instance_closed \<Gamma> M"
    and M_subterms_cl: "has_all_wt_instances_of \<Gamma> (subterms\<^sub>s\<^sub>e\<^sub>t (set M)) (set M)"
    and M_Ana_cl: "has_all_wt_instances_of \<Gamma> (\<Union>((set \<circ> fst \<circ> Ana) ` set M)) (set M)"
  using finite_SMP_representationD[OF M_SMP_repr] by blast+

  note 0 = has_all_wt_instances_ofD'[OF wf_trms_subterms[OF M_wf] M_wf M_subterms_cl]
  note 1 = TComp_var_instance_closed_has_Fun[OF M_var_inst_cl M_wf]
  note 2 = TComp_var_and_subterm_instance_closed_has_subterms_instances[
            OF M_var_inst_cl M_subterms_cl M_wf]

  have wf_t': "wf\<^sub>t\<^sub>r\<^sub>m t'" using hyps wf_t wf_trm_subterm by blast

  obtain c where "t = Fun c [] \<or> t' = Fun c []" using True by moura
  thus ?thesis
  proof
    assume c: "t' = Fun c []"
    show ?thesis
    proof (cases "\<exists>f. t = Fun f []")
      case True
      hence "t = t'" using c hyps by force
      thus ?thesis using IH by fast
    next
      case False
      note F = this
      then obtain m \<delta> where m: "m \<in> set M" "t = m \<cdot> \<delta>"
          and \<delta>: "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<delta>)"
        using IH by blast

      show ?thesis using subterm_subst_unfold[OF hyps[unfolded m(2)]]
      proof
        assume "\<exists>m'. m' \<sqsubseteq> m \<and> t' = m' \<cdot> \<delta>"
        then obtain m' where m': "m' \<sqsubseteq> m" "t' = m' \<cdot> \<delta>" by moura
        obtain n \<theta> where n: "n \<in> set M" "m' = n \<cdot> \<theta>" and \<theta>: "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<theta>)"
          using 0[of m'] m(1) m'(1) by blast
        have "t' = n \<cdot> (\<theta> \<circ>\<^sub>s \<delta>)" using m'(2) n(2) by auto
        thus ?thesis
          using c n(1) wt_subst_compose[OF \<theta>(1) \<delta>(1)] wf_trms_subst_compose[OF \<theta>(2) \<delta>(2)] by blast
      next
        assume "\<exists>x \<in> fv m. t' \<sqsubset> \<delta> x"
        then obtain x where x: "x \<in> fv m" "t' \<sqsubset> \<delta> x" "t' \<sqsubseteq> \<delta> x" by moura
        have \<delta>x_wf: "wf\<^sub>t\<^sub>r\<^sub>m (\<delta> x)" using \<delta>(2) by fastforce
        
        have x_fv_ex: "\<exists>y \<in> fv\<^sub>s\<^sub>e\<^sub>t (set M). \<Gamma> (Var x) = \<Gamma> (Var y)" using x m by auto

        show ?thesis
        proof (cases "\<Gamma> t'")
          case (Var a)
          show ?thesis
            using c m 2[OF _ hyps[unfolded m(2)] \<delta>]
            by fast
        next
          case (Fun g S)
          show ?thesis
            using c 1[of \<delta> x t', OF \<delta>x_wf x_fv_ex x(3) \<delta>(1) Fun]
            by blast
        qed
      qed
    qed
  qed (use IH hyps in simp)
next
  case False
  note F = False
  then obtain m \<delta> where m:
      "m \<in> set M" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>" "t = m \<cdot> \<delta>" "is_Fun m" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<delta>)"
    using IH by moura
  obtain f T where fT: "t' = Fun f T" "arity f > 0" "\<Gamma> t' = TComp f (map \<Gamma> T)"
    using F prems fun_type wf_trm_subtermeq[OF wf_t hyps]
    by (metis is_FunE length_greater_0_conv subtermeqI' wf\<^sub>t\<^sub>r\<^sub>m_def)

  have closed: "has_all_wt_instances_of \<Gamma> (subterms\<^sub>s\<^sub>e\<^sub>t (set M)) (set M)"
               "is_TComp_var_instance_closed \<Gamma> M"
    using M_SMP_repr unfolding finite_SMP_representation_def by metis+

  have M_wf: "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (set M)" 
    using finite_SMP_representationD[OF M_SMP_repr] by blast

  show ?thesis
  proof (cases "\<exists>x \<in> fv m. t' \<sqsubseteq> \<delta> x")
    case True
    then obtain x where x: "x \<in> fv m" "t' \<sqsubseteq> \<delta> x" by moura
    have 1: "x \<in> fv\<^sub>s\<^sub>e\<^sub>t (set M)" using m(1) x(1) by auto
    have 2: "is_Fun (\<delta> x)" using prems x(2) by auto
    have 3: "wf\<^sub>t\<^sub>r\<^sub>m (\<delta> x)" using m(5) by (simp add: wf_trm_subst_rangeD)
    have "\<not>(\<exists>f. \<delta> x = Fun f [])" using F x(2) by auto
    hence "\<exists>f T. \<Gamma> (Var x) = TComp f T" using 2 3 m(2)
      by (metis (no_types) fun_type is_FunE length_greater_0_conv subtermeqI' wf\<^sub>t\<^sub>r\<^sub>m_def wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def)
    moreover have "\<exists>f T. \<Gamma> t' = Fun f T"
      using False prems wf_trm_subtermeq[OF wf_t hyps]
      by (metis (no_types) fun_type is_FunE length_greater_0_conv subtermeqI' wf\<^sub>t\<^sub>r\<^sub>m_def)
    ultimately show ?thesis
      using TComp_var_instance_closed_has_Fun 1 x(2) m(2) prems closed 3 M_wf
      by metis
  next
    case False
    then obtain m' where m': "m' \<sqsubseteq> m" "t' = m' \<cdot> \<delta>" "is_Fun m'"
      using hyps m(3) subterm_subst_not_img_subterm
      by blast
    then obtain \<theta> m'' where \<theta>: "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<theta>)" "m'' \<in> set M" "m' = m'' \<cdot> \<theta>"
      using m(1) has_all_wt_instances_ofD'[OF wf_trms_subterms[OF M_wf] M_wf closed(1)] by blast
    hence t'_m'': "t' = m'' \<cdot> \<theta> \<circ>\<^sub>s \<delta>" using m'(2) by fastforce

    note \<theta>\<delta> = wt_subst_compose[OF \<theta>(1) m(2)] wf_trms_subst_compose[OF \<theta>(2) m(5)]

    show ?thesis
    proof (cases "is_Fun m''")
      case True thus ?thesis using \<theta>(3,4) m'(2,3) m(4) fT t'_m'' \<theta>\<delta> by blast
    next
      case False
      then obtain x where x: "m'' = Var x" by moura
      hence "\<exists>y \<in> fv\<^sub>s\<^sub>e\<^sub>t (set M). \<Gamma> (Var x) = \<Gamma> (Var y)" "t' \<sqsubseteq> (\<theta> \<circ>\<^sub>s \<delta>) x"
            "\<Gamma> (Var x) = Fun f (map \<Gamma> T)" "wf\<^sub>t\<^sub>r\<^sub>m ((\<theta> \<circ>\<^sub>s \<delta>) x)"
        using \<theta>\<delta> t'_m'' \<theta>(3) fv_subset[OF \<theta>(3)] fT(3) subst_apply_term.simps(1)[of x "\<theta> \<circ>\<^sub>s \<delta>"]
              wt_subst_trm''[OF \<theta>\<delta>(1), of "Var x"]
        by (fastforce, blast, argo, fastforce)
      thus ?thesis
        using x TComp_var_instance_closed_has_Fun[
                of M "\<theta> \<circ>\<^sub>s \<delta>" x t' f "map \<Gamma> T", OF closed(2) M_wf _ _ _ \<theta>\<delta>(1) fT(3) prems]
        by blast
    qed
  qed
qed

lemma SMP_D:
  assumes "t \<in> SMP (set M)" "is_Fun t"
    and M_SMP_repr: "finite_SMP_representation arity Ana \<Gamma> M"
  shows "((\<exists>f. t = Fun f []) \<and> (\<exists>m \<in> set M. \<exists>\<delta>. wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<and> wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<delta>) \<and> t = m \<cdot> \<delta>)) \<or>
         (\<exists>m \<in> set M. \<exists>\<delta>. wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<and> wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<delta>) \<and> t = m \<cdot> \<delta> \<and> is_Fun m)"
proof -
  have wf_M: "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (set M)"
      and closed: "has_all_wt_instances_of \<Gamma> (subterms\<^sub>s\<^sub>e\<^sub>t (set M)) (set M)"
                  "has_all_wt_instances_of \<Gamma> (\<Union>((set \<circ> fst \<circ> Ana) ` set M)) (set M)"
                  "is_TComp_var_instance_closed \<Gamma> M"
    using finite_SMP_representationD[OF M_SMP_repr] by blast+

  show ?thesis using assms(1,2)
  proof (induction t rule: SMP.induct)
    case (MP t)
    moreover have "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t Var" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range Var)" "t = t \<cdot> Var" by simp_all
    ultimately show ?case by blast 
  next
    case (Subterm t t')
    hence t_fun: "is_Fun t" by auto
    note * = Subterm.hyps(2) SMP_wf_trm[OF Subterm.hyps(1) wf_M(1)]
             Subterm.prems Subterm.IH[OF t_fun] M_SMP_repr
    show ?case by (rule SMP_D_aux3[OF *])
  next
    case (Substitution t \<delta>)
    have wf: "wf\<^sub>t\<^sub>r\<^sub>m t" by (metis Substitution.hyps(1) wf_M(1) SMP_wf_trm)
    hence wf': "wf\<^sub>t\<^sub>r\<^sub>m (t \<cdot> \<delta>)" using Substitution.hyps(3) wf_trm_subst by blast
    show ?case
    proof (cases "\<Gamma> t")
      case (Var a)
      hence 1: "\<Gamma> (t \<cdot> \<delta>) = TAtom a" using Substitution.hyps(2) by (metis wt_subst_trm'') 
      then obtain c where c: "t \<cdot> \<delta> = Fun c []"
        using TAtom_term_cases[OF wf' 1] Substitution.prems by fastforce
      hence "(\<exists>x. t = Var x) \<or> t = t \<cdot> \<delta>" by (cases t) auto
      thus ?thesis
      proof
        assume t_Var: "\<exists>x. t = Var x"
        then obtain x where x: "t = Var x" "\<delta> x = Fun c []" "\<Gamma> (Var x) = TAtom a"
          using c 1 wt_subst_trm''[OF Substitution.hyps(2), of t] by force
        
        obtain m \<theta> where m: "m \<in> set M" "t = m \<cdot> \<theta>" and \<theta>: "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<theta>)"
          using SMP_D_aux2[OF Substitution.hyps(1) t_Var M_SMP_repr] by moura

        have "m \<cdot> (\<theta> \<circ>\<^sub>s \<delta>) = Fun c []" using c m(2) by auto
        thus ?thesis
          using c m(1) wt_subst_compose[OF \<theta>(1) Substitution.hyps(2)]
                wf_trms_subst_compose[OF \<theta>(2) Substitution.hyps(3)]
          by metis
      qed (use c Substitution.IH in auto)
    next
      case (Fun f T)
      hence 1: "\<Gamma> (t \<cdot> \<delta>) = TComp f T" using Substitution.hyps(2) by (metis wt_subst_trm'')
      have 2: "\<not>(\<exists>f. t = Fun f [])" using Fun TComp_term_cases[OF wf] by auto
      obtain T'' where T'': "t \<cdot> \<delta> = Fun f T''"
        using 1 2 fun_type_id_eq Fun Substitution.prems
        by fastforce
      have f: "arity f > 0" "public f" using fun_type_inv[OF 1] by metis+
  
      show ?thesis
      proof (cases t)
        case (Fun g U)
        then obtain m \<theta> where m:
            "m \<in> set M" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>" "t = m \<cdot> \<theta>" "is_Fun m" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<theta>)"
          using Substitution.IH Fun 2 by moura
        have "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\<theta> \<circ>\<^sub>s \<delta>)" "t \<cdot> \<delta> = m \<cdot> (\<theta> \<circ>\<^sub>s \<delta>)" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range (\<theta> \<circ>\<^sub>s \<delta>))"
          using wt_subst_compose[OF m(2) Substitution.hyps(2)] m(3)
                wf_trms_subst_compose[OF m(5) Substitution.hyps(3)]
          by auto
        thus ?thesis using m(1,4) by metis
      next
        case (Var x)
        then obtain y where y: "y \<in> fv\<^sub>s\<^sub>e\<^sub>t (set M)" "\<Gamma> (Var y) = \<Gamma> (Var x)"
          using SMP_D_aux1[OF Substitution.hyps(1) closed(1,3) wf_M] Fun
          by moura
        hence 3: "\<Gamma> (Var y) = TComp f T" using Var Fun \<Gamma>_Var_fst by simp
        
        obtain h V where V:
            "Fun h V \<in> set M" "\<Gamma> (Fun h V) = \<Gamma> (Var y)" "\<forall>u \<in> set V. \<exists>z. u = Var z" "distinct V"
          by (metis is_VarE is_TComp_var_instance_closedD[OF _ 3 closed(3)] y(1))
        moreover have "length T'' = length V" using 3 V(2) fun_type_length_eq 1 T'' by metis
        ultimately have TV: "T = map \<Gamma> V"
          by (metis fun_type[OF f(1)] 3 fun_type_id_eq term.inject(2))
  
        obtain \<theta> where \<theta>: "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<theta>)" "t \<cdot> \<delta> = Fun h V \<cdot> \<theta>"
          using TComp_var_instance_wt_subst_exists 1 3 T'' TV V(2,3,4) wf'
          by (metis fun_type_id_eq)
  
        have 9: "\<Gamma> (Fun h V) = \<Gamma> (\<delta> x)" using y(2) Substitution.hyps(2) V(2) 1 3 Var by auto
  
        show ?thesis using Var \<theta> 9 V(1) by force
      qed
    qed
  next
    case (Ana t K T k)
    have 1: "is_Fun t" using Ana.hyps(2,3) by auto
    then obtain f U where U: "t = Fun f U" by moura
  
    have 2: "fv k \<subseteq> fv t" using Ana_keys_fv[OF Ana.hyps(2)] Ana.hyps(3) by auto
  
    have wf_t: "wf\<^sub>t\<^sub>r\<^sub>m t"
      using SMP_wf_trm[OF Ana.hyps(1)] wf\<^sub>t\<^sub>r\<^sub>m_code wf_M
      by auto
    hence wf_k: "wf\<^sub>t\<^sub>r\<^sub>m k"
      using Ana_keys_wf'[OF Ana.hyps(2)] wf\<^sub>t\<^sub>r\<^sub>m_code Ana.hyps(3)
      by auto
  
    have wf_M_keys: "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (\<Union>((set \<circ> fst \<circ> Ana) ` set M))"
    proof
      fix t assume "t \<in> (\<Union>((set \<circ> fst \<circ> Ana) ` set M))"
      then obtain s where s: "s \<in> set M" "t \<in> (set \<circ> fst \<circ> Ana) s" by blast
      obtain K R where KR: "Ana s = (K,R)" by (metis surj_pair)
      hence "t \<in> set K" using s(2) by simp
      thus "wf\<^sub>t\<^sub>r\<^sub>m t" using Ana_keys_wf'[OF KR] wf_M s(1) by blast
    qed
  
    show ?case using Ana_subst'_or_Ana_keys_subterm
    proof
      assume "\<forall>t K T k. Ana t = (K, T) \<longrightarrow> k \<in> set K \<longrightarrow> k \<sqsubset> t"
      hence *: "k \<sqsubseteq> t" using Ana.hyps(2,3) by auto
      show ?thesis by (rule SMP_D_aux3[OF * wf_t Ana.prems Ana.IH[OF 1] M_SMP_repr])
    next
      assume Ana_subst':
          "\<forall>f T \<delta> K M. Ana (Fun f T) = (K, M) \<longrightarrow> Ana (Fun f T \<cdot> \<delta>) = (K \<cdot>\<^sub>l\<^sub>i\<^sub>s\<^sub>t \<delta>, M \<cdot>\<^sub>l\<^sub>i\<^sub>s\<^sub>t \<delta>)"
  
      have "arity f > 0" using Ana_const[of f U] U Ana.hyps(2,3) by fastforce
      hence "U \<noteq> []" using wf_t U unfolding wf\<^sub>t\<^sub>r\<^sub>m_def by force
      then obtain m \<delta> where m: "m \<in> set M" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<delta>)" "t = m \<cdot> \<delta>" "is_Fun m"
        using Ana.IH[OF 1] U by auto
      hence "Ana (t \<cdot> \<delta>) = (K \<cdot>\<^sub>l\<^sub>i\<^sub>s\<^sub>t \<delta>,T \<cdot>\<^sub>l\<^sub>i\<^sub>s\<^sub>t \<delta>)" using Ana_subst' U Ana.hyps(2) by auto
      obtain Km Tm where Ana_m: "Ana m = (Km,Tm)" by moura
      hence "Ana (m \<cdot> \<delta>) = (Km \<cdot>\<^sub>l\<^sub>i\<^sub>s\<^sub>t \<delta>,Tm \<cdot>\<^sub>l\<^sub>i\<^sub>s\<^sub>t \<delta>)"
        using Ana_subst' U m(4) is_FunE[OF m(5)] Ana.hyps(2)
        by metis
      then obtain km where km: "km \<in> set Km" "k = km \<cdot> \<delta>" using Ana.hyps(2,3) m(4) by auto
      then obtain \<theta> km' where \<theta>: "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<theta>)"
          and km': "km' \<in> set M" "km = km' \<cdot> \<theta>"
        using Ana_m m(1) has_all_wt_instances_ofD'[OF wf_M_keys wf_M closed(2), of km] by force
  
      have k\<theta>\<delta>: "k = km' \<cdot> \<theta> \<circ>\<^sub>s \<delta>" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\<theta> \<circ>\<^sub>s \<delta>)" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range (\<theta> \<circ>\<^sub>s \<delta>))"
        using km(2) km' wt_subst_compose[OF \<theta>(1) m(2)] wf_trms_subst_compose[OF \<theta>(2) m(3)]
        by auto
  
      show ?case
      proof (cases "is_Fun km'")
        case True thus ?thesis using k\<theta>\<delta> km'(1) by blast
      next
        case False
        note F = False
        then obtain x where x: "km' = Var x" by auto
        hence 3: "x \<in> fv\<^sub>s\<^sub>e\<^sub>t (set M)" using fv_subset[OF km'(1)] by auto
        obtain kf kT where kf: "k = Fun kf kT" using Ana.prems by auto
        show ?thesis
        proof (cases "kT = []")
          case True thus ?thesis using k\<theta>\<delta>(1) k\<theta>\<delta>(2) k\<theta>\<delta>(3) kf km'(1) by blast
        next
          case False
          hence 4: "arity kf > 0" using wf_k kf TAtom_term_cases const_type by fastforce
          then obtain kT' where kT': "\<Gamma> k = TComp kf kT'" by (simp add: fun_type kf) 
          then obtain V where V:
              "Fun kf V \<in> set M" "\<Gamma> (Fun kf V) = \<Gamma> (Var x)" "\<forall>u \<in> set V. \<exists>v. u = Var v"
              "distinct V" "is_Fun (Fun kf V)"
            using is_TComp_var_instance_closedD[OF _ _ closed(3), of x]
                  x m(2) k\<theta>\<delta>(1) 3 wt_subst_trm''[OF k\<theta>\<delta>(2)]
            by (metis fun_type_id_eq term.disc(2) is_VarE)
          have 5: "kT' = map \<Gamma> V"
            using fun_type[OF 4] x kT' k\<theta>\<delta> m(2) V(2)
            by (metis term.inject(2) wt_subst_trm'')
          thus ?thesis
            using TComp_var_instance_wt_subst_exists wf_k kf 4 V(3,4) kT' V(1,5)
            by metis
        qed
      qed
    qed
  qed
qed

lemma SMP_D':
  fixes M
  defines "\<delta> \<equiv> var_rename (max_var_set (fv\<^sub>s\<^sub>e\<^sub>t (set M)))"
  assumes M_SMP_repr: "finite_SMP_representation arity Ana \<Gamma> M"
    and s: "s \<in> SMP (set M)" "is_Fun s" "\<nexists>f. s = Fun f []"
    and t: "t \<in> SMP (set M)" "is_Fun t" "\<nexists>f. t = Fun f []"
  obtains \<sigma> s0 \<theta> t0
  where "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<sigma>)" "s0 \<in> set M" "is_Fun s0" "s = s0 \<cdot> \<sigma>" "\<Gamma> s = \<Gamma> s0"
    and "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<theta>)" "t0 \<in> set M" "is_Fun t0" "t = t0 \<cdot> \<delta> \<cdot> \<theta>" "\<Gamma> t = \<Gamma> t0"
proof -
  obtain \<sigma> s0 where
      s0: "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<sigma>)" "s0 \<in> set M" "s = s0 \<cdot> \<sigma>" "is_Fun s0"
    using s(3) SMP_D[OF s(1,2) M_SMP_repr] unfolding \<delta>_def by metis

  obtain \<theta> t0 where t0:
      "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<theta>)" "t0 \<in> set M" "t = t0 \<cdot> \<delta> \<cdot> \<theta>" "is_Fun t0"
    using t(3) SMP_D[OF t(1,2) M_SMP_repr] var_rename_wt'[of _ t]
          wf_trms_subst_compose_Var_range(1)[OF _ var_rename_is_renaming(2)]
    unfolding \<delta>_def by metis

  have "\<Gamma> s = \<Gamma> s0" "\<Gamma> t = \<Gamma> (t0 \<cdot> \<delta>)" "\<Gamma> (t0 \<cdot> \<delta>) = \<Gamma> t0"
    using s0 t0 wt_subst_trm'' by (metis, metis, metis \<delta>_def var_rename_wt(1))
  thus ?thesis using s0 t0 that by simp
qed

lemma SMP_D'':
  fixes t::"('fun, ('fun, 'atom) term \<times> nat) term"
  assumes t_SMP: "t \<in> SMP (set M)"
    and M_SMP_repr: "finite_SMP_representation arity Ana \<Gamma> M"
  shows "\<exists>m \<in> set M. \<exists>\<delta>. wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<and> wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<delta>) \<and> t = m \<cdot> \<delta>"
proof (cases "(\<exists>x. t = Var x) \<or> (\<exists>c. t = Fun c [])")
  case True
  have M_wf: "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (set M)" 
      and M_var_inst_cl: "is_TComp_var_instance_closed \<Gamma> M"
      and M_subterms_cl: "has_all_wt_instances_of \<Gamma> (subterms\<^sub>s\<^sub>e\<^sub>t (set M)) (set M)"
      and M_Ana_cl: "has_all_wt_instances_of \<Gamma> (\<Union>((set \<circ> fst \<circ> Ana) ` set M)) (set M)"
    using finite_SMP_representationD[OF M_SMP_repr] by blast+

  have M_Ana_wf: "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (\<Union> ((set \<circ> fst \<circ> Ana) ` set M))"
  proof
    fix k assume "k \<in> \<Union>((set \<circ> fst \<circ> Ana) ` set M)"
    then obtain m where m: "m \<in> set M" "k \<in> set (fst (Ana m))" by force
    thus "wf\<^sub>t\<^sub>r\<^sub>m k" using M_wf Ana_keys_wf'[of m "fst (Ana m)" _ k] surjective_pairing by blast
  qed

  show ?thesis using True
  proof
    assume "\<exists>x. t = Var x"
    then obtain x y where x: "t = Var x" and y: "y \<in> fv\<^sub>s\<^sub>e\<^sub>t (set M)" "\<Gamma> (Var y) = \<Gamma> (Var x)"
      using SMP_D_aux1[OF t_SMP M_subterms_cl M_var_inst_cl M_wf] by fastforce
    then obtain m \<delta> where m: "m \<in> set M" "m \<cdot> \<delta> = Var y" and \<delta>: "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>"
      using has_all_wt_instances_ofD'[OF wf_trms_subterms[OF M_wf] M_wf M_subterms_cl, of "Var y"]
            vars_iff_subtermeq_set[of y "set M"]
      by fastforce

    obtain z where z: "m = Var z" using m(2) by (cases m) auto

    define \<theta> where "\<theta> \<equiv> Var(z := Var x)::('fun, ('fun, 'atom) term \<times> nat) subst"

    have "\<Gamma> (Var z) = \<Gamma> (Var x)" using y(2) m(2) z wt_subst_trm''[OF \<delta>, of m] by argo
    hence "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<theta>)" unfolding \<theta>_def wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by force+
    moreover have "t = m \<cdot> \<theta>" using x z unfolding \<theta>_def by simp
    ultimately show ?thesis using m(1) by blast
  qed (use SMP_D[OF t_SMP _ M_SMP_repr] in blast)
qed (use SMP_D[OF t_SMP _ M_SMP_repr] in blast)
end

lemma tfr\<^sub>s\<^sub>e\<^sub>t_if_comp_tfr\<^sub>s\<^sub>e\<^sub>t:
  assumes "comp_tfr\<^sub>s\<^sub>e\<^sub>t arity Ana \<Gamma> M"
  shows "tfr\<^sub>s\<^sub>e\<^sub>t (set M)"
proof -
  let ?\<delta> = "var_rename (max_var_set (fv\<^sub>s\<^sub>e\<^sub>t (set M)))"
  have M_SMP_repr: "finite_SMP_representation arity Ana \<Gamma> M"
    by (metis comp_tfr\<^sub>s\<^sub>e\<^sub>t_def assms)

  have M_finite: "finite (set M)"
    using assms card_gt_0_iff unfolding comp_tfr\<^sub>s\<^sub>e\<^sub>t_def by blast

  show ?thesis
  proof (unfold tfr\<^sub>s\<^sub>e\<^sub>t_def; intro ballI impI)
    fix s t assume "s \<in> SMP (set M) - Var`\<V>" "t \<in> SMP (set M) - Var`\<V>"
    hence st: "s \<in> SMP (set M)" "is_Fun s" "t \<in> SMP (set M)" "is_Fun t" by auto
    have "\<not>(\<exists>\<delta>. Unifier \<delta> s t)" when st_type_neq: "\<Gamma> s \<noteq> \<Gamma> t"
    proof (cases "\<exists>f. s = Fun f [] \<or> t = Fun f []")
      case False
      then obtain \<sigma> s0 \<theta> t0 where
            s0: "s0 \<in> set M" "is_Fun s0" "s = s0 \<cdot> \<sigma>" "\<Gamma> s = \<Gamma> s0"
        and t0: "t0 \<in> set M" "is_Fun t0" "t = t0 \<cdot> ?\<delta> \<cdot> \<theta>" "\<Gamma> t = \<Gamma> t0"
        using SMP_D'[OF M_SMP_repr st(1,2) _ st(3,4)] by metis
      hence "\<not>(\<exists>\<delta>. Unifier \<delta> s0 (t0 \<cdot> ?\<delta>))"
        using assms mgu_None_is_subst_neq st_type_neq wt_subst_trm''[OF var_rename_wt(1)]
        unfolding comp_tfr\<^sub>s\<^sub>e\<^sub>t_def Let_def by metis
      thus ?thesis
        using vars_term_disjoint_imp_unifier[OF var_rename_fv_set_disjoint[OF M_finite]] s0(1) t0(1)
        unfolding s0(3) t0(3) by (metis (no_types, opaque_lifting) subst_subst_compose)
    qed (use st_type_neq st(2,4) in auto)
    thus "\<Gamma> s = \<Gamma> t" when "\<exists>\<delta>. Unifier \<delta> s t" by (metis that)
  qed
qed

lemma tfr\<^sub>s\<^sub>e\<^sub>t_if_comp_tfr\<^sub>s\<^sub>e\<^sub>t':
  assumes "let N = SMP0 Ana \<Gamma> M in set M \<subseteq> set N \<and> comp_tfr\<^sub>s\<^sub>e\<^sub>t arity Ana \<Gamma> N"
  shows "tfr\<^sub>s\<^sub>e\<^sub>t (set M)"
by (rule tfr_subset(2)[
          OF tfr\<^sub>s\<^sub>e\<^sub>t_if_comp_tfr\<^sub>s\<^sub>e\<^sub>t[OF conjunct2[OF assms[unfolded Let_def]]]
             conjunct1[OF assms[unfolded Let_def]]])

lemma tfr\<^sub>s\<^sub>t\<^sub>p_is_comp_tfr\<^sub>s\<^sub>t\<^sub>p: "tfr\<^sub>s\<^sub>t\<^sub>p a = comp_tfr\<^sub>s\<^sub>t\<^sub>p \<Gamma> a"
proof (cases a)
  case (Equality ac t t')
  thus ?thesis
    using mgu_always_unifies[of t _ t'] mgu_gives_MGU[of t t']
    by auto
next
  case (Inequality X F)
  thus ?thesis
    using tfr\<^sub>s\<^sub>t\<^sub>p.simps(2)[of X F]
          comp_tfr\<^sub>s\<^sub>t\<^sub>p.simps(2)[of \<Gamma> X F]
          Fun_range_case(2)[of "subterms\<^sub>s\<^sub>e\<^sub>t (trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F)"] 
    unfolding is_Var_def
    by auto
qed auto

lemma tfr\<^sub>s\<^sub>t_if_comp_tfr\<^sub>s\<^sub>t:
  assumes "comp_tfr\<^sub>s\<^sub>t arity Ana \<Gamma> M S"
  shows "tfr\<^sub>s\<^sub>t S"
unfolding tfr\<^sub>s\<^sub>t_def
proof
  have comp_tfr\<^sub>s\<^sub>e\<^sub>t_M: "comp_tfr\<^sub>s\<^sub>e\<^sub>t arity Ana \<Gamma> M"
    using assms unfolding comp_tfr\<^sub>s\<^sub>t_def by blast
  
  have wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s_M: "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (set M)"
      and wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s_S: "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (trms\<^sub>s\<^sub>t S)"
      and S_trms_instance_M: "has_all_wt_instances_of \<Gamma> (trms\<^sub>s\<^sub>t S) (set M)"
    using assms wf\<^sub>t\<^sub>r\<^sub>m_code trms_list\<^sub>s\<^sub>t_is_trms\<^sub>s\<^sub>t
    unfolding comp_tfr\<^sub>s\<^sub>t_def comp_tfr\<^sub>s\<^sub>e\<^sub>t_def finite_SMP_representation_def list_all_iff
    by blast+

  show "tfr\<^sub>s\<^sub>e\<^sub>t (trms\<^sub>s\<^sub>t S)"
    using tfr_subset(3)[OF tfr\<^sub>s\<^sub>e\<^sub>t_if_comp_tfr\<^sub>s\<^sub>e\<^sub>t[OF comp_tfr\<^sub>s\<^sub>e\<^sub>t_M] SMP_SMP_subset]
          SMP_I'[OF wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s_S wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s_M S_trms_instance_M]
    by blast

  have "list_all (comp_tfr\<^sub>s\<^sub>t\<^sub>p \<Gamma>) S" by (metis assms comp_tfr\<^sub>s\<^sub>t_def)
  thus "list_all tfr\<^sub>s\<^sub>t\<^sub>p S" by (induct S) (simp_all add: tfr\<^sub>s\<^sub>t\<^sub>p_is_comp_tfr\<^sub>s\<^sub>t\<^sub>p)
qed

lemma tfr\<^sub>s\<^sub>t_if_comp_tfr\<^sub>s\<^sub>t':
  assumes "comp_tfr\<^sub>s\<^sub>t arity Ana \<Gamma> (SMP0 Ana \<Gamma> (trms_list\<^sub>s\<^sub>t S)) S"
  shows "tfr\<^sub>s\<^sub>t S"
by (rule tfr\<^sub>s\<^sub>t_if_comp_tfr\<^sub>s\<^sub>t[OF assms])



subsubsection \<open>Lemmata for Checking Ground SMP (GSMP) Disjointness\<close>
context
begin
private lemma ground_SMP_disjointI_aux1:
  fixes M::"('fun, ('fun, 'atom) term \<times> nat) term set"
  assumes f_def: "f \<equiv> \<lambda>M. {t \<cdot> \<delta> | t \<delta>. t \<in> M \<and> wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<and> wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<delta>) \<and> fv (t \<cdot> \<delta>) = {}}"
    and g_def: "g \<equiv> \<lambda>M. {t \<in> M. fv t = {}}"
  shows "f (SMP M) = g (SMP M)"
proof
  have "t \<in> f (SMP M)" when t: "t \<in> SMP M" "fv t = {}" for t
  proof -
    define \<delta> where "\<delta> \<equiv> Var::('fun, ('fun, 'atom) term \<times> nat) subst"
    have "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<delta>)" "t = t \<cdot> \<delta>"
      using subst_apply_term_empty[of t] that(2) wt_subst_Var wf_trm_subst_range_Var
      unfolding \<delta>_def by auto
    thus ?thesis using SMP.Substitution[OF t(1), of \<delta>] t(2) unfolding f_def by fastforce
  qed
  thus "g (SMP M) \<subseteq> f (SMP M)" unfolding g_def by blast
qed (use f_def g_def in blast)

private lemma ground_SMP_disjointI_aux2:
  fixes M::"('fun, ('fun, 'atom) term \<times> nat) term list"
  assumes f_def: "f \<equiv> \<lambda>M. {t \<cdot> \<delta> | t \<delta>. t \<in> M \<and> wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<and> wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<delta>) \<and> fv (t \<cdot> \<delta>) = {}}"
    and M_SMP_repr: "finite_SMP_representation arity Ana \<Gamma> M"
  shows "f (set M) = f (SMP (set M))"
proof
  have M_wf: "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (set M)" 
      and M_var_inst_cl: "is_TComp_var_instance_closed \<Gamma> M"
      and M_subterms_cl: "has_all_wt_instances_of \<Gamma> (subterms\<^sub>s\<^sub>e\<^sub>t (set M)) (set M)"
      and M_Ana_cl: "has_all_wt_instances_of \<Gamma> (\<Union>((set \<circ> fst \<circ> Ana) ` set M)) (set M)"
    using finite_SMP_representationD[OF M_SMP_repr] by blast+

  show "f (SMP (set M)) \<subseteq> f (set M)"
  proof
    fix t assume "t \<in> f (SMP (set M))"
    then obtain s \<delta> where s: "t = s \<cdot> \<delta>" "s \<in> SMP (set M)" "fv (s \<cdot> \<delta>) = {}"
        and \<delta>: "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<delta>)"
      unfolding f_def by blast

    have t_wf: "wf\<^sub>t\<^sub>r\<^sub>m t" using SMP_wf_trm[OF s(2) M_wf] s(1) wf_trm_subst[OF \<delta>(2)] by blast 

    obtain m \<theta> where m: "m \<in> set M" "s = m \<cdot> \<theta>" and \<theta>: "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<theta>)"
      using SMP_D''[OF s(2) M_SMP_repr] by blast

    have "t = m \<cdot> (\<theta> \<circ>\<^sub>s \<delta>)" "fv (m \<cdot> (\<theta> \<circ>\<^sub>s \<delta>)) = {}" using s(1,3) m(2) by simp_all
    thus "t \<in> f (set M)"
      using m(1) wt_subst_compose[OF \<theta>(1) \<delta>(1)] wf_trms_subst_compose[OF \<theta>(2) \<delta>(2)]
      unfolding f_def by blast
  qed
qed (auto simp add: f_def)

private lemma ground_SMP_disjointI_aux3:
  fixes A B C::"('fun, ('fun, 'atom) term \<times> nat) term set"
  defines "P \<equiv> \<lambda>t s. \<exists>\<delta>. wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<and> wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<delta>) \<and> Unifier \<delta> t s"
  assumes f_def: "f \<equiv> \<lambda>M. {t \<cdot> \<delta> | t \<delta>. t \<in> M \<and> wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<and> wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<delta>) \<and> fv (t \<cdot> \<delta>) = {}}"
    and Q_def: "Q \<equiv> \<lambda>t. intruder_synth' public arity {} t"
    and R_def: "R \<equiv> \<lambda>t. \<exists>u \<in> C. is_wt_instance_of_cond \<Gamma> t u"
    and AB: "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s A" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s B" "fv\<^sub>s\<^sub>e\<^sub>t A \<inter> fv\<^sub>s\<^sub>e\<^sub>t B = {}"
    and C: "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s C"
    and ABC: "\<forall>t \<in> A. \<forall>s \<in> B. P t s \<longrightarrow> (Q t \<and> Q s) \<or> (R t \<and> R s)"
  shows "f A \<inter> f B \<subseteq> f C \<union> {m. {} \<turnstile>\<^sub>c m}"
proof
  fix t assume "t \<in> f A \<inter> f B"
  then obtain ta tb \<delta>a \<delta>b where
          ta: "t = ta \<cdot> \<delta>a" "ta \<in> A" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>a" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<delta>a)" "fv (ta \<cdot> \<delta>a) = {}"
      and tb: "t = tb \<cdot> \<delta>b" "tb \<in> B" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>b" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<delta>b)" "fv (tb \<cdot> \<delta>b) = {}"
    unfolding f_def by blast

  have ta_tb_wf: "wf\<^sub>t\<^sub>r\<^sub>m ta" "wf\<^sub>t\<^sub>r\<^sub>m tb" "fv ta \<inter> fv tb = {}" "\<Gamma> ta = \<Gamma> tb"
    using ta(1,2) tb(1,2) AB fv_subset_subterms
          wt_subst_trm''[OF ta(3), of ta] wt_subst_trm''[OF tb(3), of tb]
    by (fast, fast, blast, simp)

  obtain \<theta> where \<theta>: "Unifier \<theta> ta tb" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<theta>)"
    using vars_term_disjoint_imp_unifier[OF ta_tb_wf(3), of \<delta>a \<delta>b]
          ta(1) tb(1) wt_Unifier_if_Unifier[OF ta_tb_wf(1,2,4)]
    by blast
  hence "(Q ta \<and> Q tb) \<or> (R ta \<and> R tb)" using ABC ta(2) tb(2) unfolding P_def by blast+
  thus "t \<in> f C \<union> {m. {} \<turnstile>\<^sub>c m}"
  proof
    show "Q ta \<and> Q tb \<Longrightarrow> ?thesis"
      using ta(1) pgwt_ground[of ta] pgwt_is_empty_synth[of ta] subst_ground_ident[of ta \<delta>a]
      unfolding Q_def f_def intruder_synth_code[symmetric] by simp
  next
    assume "R ta \<and> R tb"
    then obtain ua \<sigma>a where ua: "ta = ua \<cdot> \<sigma>a" "ua \<in> C" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>a" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<sigma>a)"
      using \<theta> ABC ta_tb_wf(1,2) ta(2) tb(2) C is_wt_instance_of_condD'
      unfolding P_def R_def by metis
  
    have "t = ua \<cdot> (\<sigma>a \<circ>\<^sub>s \<delta>a)" "fv t = {}"
      using ua(1) ta(1,5) tb(1,5) by auto
    thus ?thesis
      using ua(2) wt_subst_compose[OF ua(3) ta(3)] wf_trms_subst_compose[OF ua(4) ta(4)]
      unfolding f_def by blast
  qed
qed

lemma ground_SMP_disjointI:
  fixes A B::"('fun, ('fun, 'atom) term \<times> nat) term list" and C
  defines "f \<equiv> \<lambda>M. {t \<cdot> \<delta> | t \<delta>. t \<in> M \<and> wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<and> wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<delta>) \<and> fv (t \<cdot> \<delta>) = {}}"
    and "g \<equiv> \<lambda>M. {t \<in> M. fv t = {}}"
    and "Q \<equiv> \<lambda>t. intruder_synth' public arity {} t"
    and "R \<equiv> \<lambda>t. \<exists>u \<in> C. is_wt_instance_of_cond \<Gamma> t u"
  assumes AB_fv_disj: "fv\<^sub>s\<^sub>e\<^sub>t (set A) \<inter> fv\<^sub>s\<^sub>e\<^sub>t (set B) = {}"
    and A_SMP_repr: "finite_SMP_representation arity Ana \<Gamma> A"
    and B_SMP_repr: "finite_SMP_representation arity Ana \<Gamma> B"
    and C_wf: "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s C"
    and ABC: "\<forall>t \<in> set A. \<forall>s \<in> set B. \<Gamma> t = \<Gamma> s \<and> mgu t s \<noteq> None \<longrightarrow> (Q t \<and> Q s) \<or> (R t \<and> R s)"
  shows "g (SMP (set A)) \<inter> g (SMP (set B)) \<subseteq> f C \<union> {m. {} \<turnstile>\<^sub>c m}"
proof -
  have AB_wf: "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (set A)" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (set B)"
    using A_SMP_repr B_SMP_repr
    unfolding finite_SMP_representation_def wf\<^sub>t\<^sub>r\<^sub>m_code list_all_iff
    by blast+

  let ?P = "\<lambda>t s. \<exists>\<delta>. wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<and> wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<delta>) \<and> Unifier \<delta> t s"
  have ABC': "\<forall>t \<in> set A. \<forall>s \<in> set B. ?P t s \<longrightarrow> (Q t \<and> Q s) \<or> (R t \<and> R s)"
    by (metis (no_types) ABC mgu_None_is_subst_neq wt_subst_trm'')

  show ?thesis
    using ground_SMP_disjointI_aux1[OF f_def g_def, of "set A"]
          ground_SMP_disjointI_aux1[OF f_def g_def, of "set B"]
          ground_SMP_disjointI_aux2[OF f_def A_SMP_repr]
          ground_SMP_disjointI_aux2[OF f_def B_SMP_repr]
          ground_SMP_disjointI_aux3[OF f_def Q_def R_def AB_wf AB_fv_disj C_wf ABC']
    by argo
qed

end

end

end