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

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:      TypedModel.thy
    Author:     Andreas Viktor Hess, DTU
*)

section {* Theory: The Typed Model *}
theory TypedModel
imports LazyIntruder
begin


subsection {* Term types and well-formed types *}

type_synonym ('f,'v) term_type = "('f,'v) term"

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"


locale typed_model = intruder_model arity public Ana
  for arity::"'fun::countable \<Rightarrow> nat"
    and public::"'fun \<Rightarrow> bool"
    and Ana::"('fun,'var::countable) term \<Rightarrow> (('fun,'var) terms \<times> ('fun,'var) terms)"
  +
  fixes \<Gamma>::"('fun,'var) term \<Rightarrow> ('fun,'atom::finite) term_type"
  assumes const_type: "\<And>c. arity c = 0 \<Longrightarrow> \<exists>a. \<forall>X. \<Gamma> (Fun c X) = TAtom a"
    and fun_type: "\<And>f X. arity f > 0 \<Longrightarrow> \<Gamma> (Fun f X) = TComp f (map \<Gamma> X)"
    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))"
begin

lemma infinite_typed_consts': "\<And>a. infinite {c. \<Gamma> (Fun c []) = TAtom a \<and> public c \<and> arity c = 0}"
proof -
  fix a
  { 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 \<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))

subsection {* Definitions *}
abbreviation "\<TT>\<^sub>a \<equiv> UNIV::('atom set)"

(* Well-typed substitutions *)
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))"

(* Sub-message patterns *)
inductive_set SMP\<^sub>s\<^sub>t::"('fun,'var) terms \<Rightarrow> ('fun,'var) terms" for M where
  MP[intro]: "t \<in> M \<Longrightarrow> t \<in> SMP\<^sub>s\<^sub>t M"
| Subterm[intro]: "\<lbrakk>t \<in> SMP\<^sub>s\<^sub>t M; t' \<sqsubset> t\<rbrakk> \<Longrightarrow> t' \<in> SMP\<^sub>s\<^sub>t M"
| Substitution[intro]: "\<lbrakk>t \<in> SMP\<^sub>s\<^sub>t M; wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>; \<And>v. wf\<^sub>t\<^sub>r\<^sub>m (\<delta> v)\<rbrakk> \<Longrightarrow> (t \<cdot> \<delta>) \<in> SMP\<^sub>s\<^sub>t M"
| Ana[intro]: "\<lbrakk>t \<in> SMP\<^sub>s\<^sub>t M; Ana t = (K,T); t' \<in> K\<rbrakk> \<Longrightarrow> t' \<in> SMP\<^sub>s\<^sub>t M"

(* Type-flaw resistance *)
abbreviation tfr\<^sub>s\<^sub>t where
  "tfr\<^sub>s\<^sub>t M \<equiv>
      (\<forall>s \<in> SMP\<^sub>s\<^sub>t M - (Var`\<V>). \<forall>t \<in> SMP\<^sub>s\<^sub>t M - (Var`\<V>). (\<exists>\<delta>. Unifier \<delta> s t) \<longrightarrow> \<Gamma> s = \<Gamma> t)
    \<and> (\<forall>x \<in> M. wf\<^sub>t\<^sub>r\<^sub>m x)"

(* (In)equalities must have the same type, and all variables in inequalities must
   additionally have atomic type *)
abbreviation eqs_tfr\<^sub>s\<^sub>t where
  "eqs_tfr\<^sub>s\<^sub>t S \<equiv>
      (\<forall>t t'. t \<doteq> t' \<in> set S \<and> (\<exists>\<delta>. Unifier \<delta> t t') \<longrightarrow> \<Gamma> t = \<Gamma> t') \<and>
      (\<forall>X t t'. \<nexists>X\<langle>t \<doteq> t'\<rangle> \<in> set S \<longrightarrow> (\<forall>x \<in> set X \<union> FV t \<union> FV t'. \<exists>a. \<Gamma> (Var x) = TAtom a))"


subsection {* Small Lemmata *}
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': "\<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 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 tatom_set_finite: "finite \<TT>\<^sub>a" by (fact Finite_Set.finite_class.finite)

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 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 (Var a) thus ?case using atypes_inhabited wf\<^sub>t\<^sub>r\<^sub>m_def by blast
next
  case (Fun f Y)
  hence "\<And>y. y \<in> set Y \<Longrightarrow> wf\<^sub>t\<^sub>r\<^sub>m y" unfolding wf\<^sub>t\<^sub>r\<^sub>m_def
    by (metis Fun_param_is_subterm subtermeq_subterm_trans subtermseq_if_subterms) 
  moreover have "\<And>y. y \<in> set Y \<Longrightarrow> (\<And>g Z. Fun g Z \<sqsubseteq> y \<Longrightarrow> 0 < arity g)"
    using Fun by auto
  ultimately have IH: "\<And>y. y \<in> set Y \<Longrightarrow> \<exists>t. \<Gamma> t = y \<and> wf\<^sub>t\<^sub>r\<^sub>m t" using Fun.IH by auto

  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

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 subterm_def subtermeq_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_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_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. \<exists>a. \<Gamma> (Var x) = TAtom a"
  shows "\<forall>x \<in> FV (t \<cdot> \<theta>). \<exists>a. \<Gamma> (Var x) = TAtom a"
using assms(3)
proof (induction t)
  case (Var x)
  then 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 ?case
  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

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')"
using assms fun_type[OF fun_type_inv(1)[OF assms(2)]] fun_type_id_eq 
by (cases t) force+

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 subtermeq_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 blast
    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 wf_trm_TAtom_subterms: "\<lbrakk>wf\<^sub>t\<^sub>r\<^sub>m t; \<Gamma> t = TAtom \<tau>\<rbrakk> \<Longrightarrow> subterms t = {t}"
using const_type_inv wf\<^sub>t\<^sub>r\<^sub>m_def by (cases t) fastforce+

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> subtermeq_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_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\<^sub>s\<^sub>t M"
using SMP\<^sub>s\<^sub>t.Substitution[OF SMP\<^sub>s\<^sub>t.MP[OF assms(1)] assms(2)] SMP\<^sub>s\<^sub>t.Subterm[of "s \<cdot> \<delta>" M t] assms(3,4)
unfolding subtermeq_def by (cases "t = s \<cdot> \<delta>") simp_all

lemma SMP_wf_trm:
  assumes "t \<in> SMP\<^sub>s\<^sub>t M" "\<And>m. m \<in> M \<Longrightarrow> wf\<^sub>t\<^sub>r\<^sub>m m"
  shows "wf\<^sub>t\<^sub>r\<^sub>m t"
using assms(1)
proof (induction t rule: SMP\<^sub>s\<^sub>t.induct)
  case MP thus ?case using assms(2) by simp
next
  case Subterm thus ?case using wf_trm_subterm by simp
next
  case Substitution thus ?case using wf_trm_subst by auto
next
  case Ana thus ?case using Ana_keys_wf' by auto
qed

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

lemma SMP_ik_trpI[intro]: "t \<in> trp\<^sub>s\<^sub>e\<^sub>t (ik\<^sub>s\<^sub>t S) \<Longrightarrow> t \<in> SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S)"
proof -
  assume "t \<in> trp\<^sub>s\<^sub>e\<^sub>t (ik\<^sub>s\<^sub>t S)"
  then obtain t' where "t' \<in> ik\<^sub>s\<^sub>t S" "t \<sqsubseteq> t'" using trpD by blast
  hence "t' \<in> SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S)" by auto

  show "t \<in> SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S)"
  proof (cases "t = t'")
    case True thus ?thesis using SMP_ikI unfolding trms\<^sub>s\<^sub>t_def by (auto simp add: \<open>t' \<in> ik\<^sub>s\<^sub>t S\<close>)
  next
    case False
    hence "t \<sqsubset> t'" using \<open>t \<sqsubseteq> t'\<close> by simp
    thus ?thesis using SMP\<^sub>s\<^sub>t.Subterm[OF \<open>t' \<in> SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S)\<close>] by metis
  qed
qed

lemma MP_setI[intro]: "x \<in> set S \<Longrightarrow> trm\<^sub>s\<^sub>t\<^sub>p x \<in> trms\<^sub>s\<^sub>t S" unfolding trms\<^sub>s\<^sub>t_def by blast

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

lemma SMP_append[simp]: "SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t (S@S')) = SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S) \<union> SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S')"
proof
  { fix t assume "t \<in> SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t (S@S'))"
    hence "t \<in> SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S) \<union> SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S')" by induct auto }
  thus "SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t (S@S')) \<subseteq> SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S) \<union> SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S')" by blast

  { fix t assume "t \<in> SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S)" hence "t \<in> SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t (S@S'))" by induct auto }
  moreover { fix t assume "t \<in> SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S')" hence "t \<in> SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t (S@S'))" by induct auto }
  ultimately show "SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S) \<union> SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S') \<subseteq> SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t (S@S'))" by blast
qed

lemma SMP_append': "SMP\<^sub>s\<^sub>t (A \<union> B) = SMP\<^sub>s\<^sub>t A \<union> SMP\<^sub>s\<^sub>t B"
proof
  { fix t assume "t \<in> SMP\<^sub>s\<^sub>t (A \<union> B)"
    hence "t \<in> SMP\<^sub>s\<^sub>t A \<union> SMP\<^sub>s\<^sub>t B" by induct auto }
  thus "SMP\<^sub>s\<^sub>t (A \<union> B) \<subseteq> SMP\<^sub>s\<^sub>t A \<union> SMP\<^sub>s\<^sub>t B" by blast

  { fix t assume "t \<in> SMP\<^sub>s\<^sub>t A" hence "t \<in> SMP\<^sub>s\<^sub>t (A \<union> B)" by induct auto }
  moreover { fix t assume "t \<in> SMP\<^sub>s\<^sub>t B" hence "t \<in> SMP\<^sub>s\<^sub>t (A \<union> B)" by induct auto }
  ultimately show "SMP\<^sub>s\<^sub>t A \<union> SMP\<^sub>s\<^sub>t B \<subseteq> SMP\<^sub>s\<^sub>t (A \<union> B)" by blast
qed

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

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

lemma trms\<^sub>s\<^sub>t_cons: "trms\<^sub>s\<^sub>t (x#S) = {trm\<^sub>s\<^sub>t\<^sub>p x} \<union> {trm_r\<^sub>s\<^sub>t\<^sub>p x} \<union> trms\<^sub>s\<^sub>t S" by simp

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

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

lemma trm_strand_subst_cong:
  "t \<in> trms\<^sub>s\<^sub>t S \<Longrightarrow> t \<cdot> \<delta> \<in> trms\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>t \<delta>)
    \<or> (\<exists>X t' t''. \<nexists>X\<langle>t' \<doteq> t''\<rangle> \<in> set S \<and> t \<cdot> rm_vars (set X) \<delta> \<in> trms\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>t \<delta>))"
  "t \<in> trms\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>t \<delta>) \<Longrightarrow> (\<exists>t'. t = t' \<cdot> \<delta> \<and> t' \<in> trms\<^sub>s\<^sub>t S)
    \<or> (\<exists>X t' t''. \<nexists>X\<langle>t' \<doteq> t''\<rangle> \<in> set S \<and> (t = t' \<cdot> rm_vars (set X) \<delta> \<or> t = t'' \<cdot> rm_vars (set X) \<delta>))"
proof -
  let ?P = "\<lambda>t \<delta> S. t \<cdot> \<delta> \<in> trms\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>t \<delta>)
    \<or> (\<exists>X t' t''. \<nexists>X\<langle>t' \<doteq> t''\<rangle> \<in> set S \<and> t \<cdot> rm_vars (set X) \<delta> \<in> trms\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>t \<delta>))"
  let ?Q = "\<lambda>t \<delta> S. (\<exists>t'. t = t' \<cdot> \<delta> \<and> t' \<in> trms\<^sub>s\<^sub>t S)
    \<or> (\<exists>X t' t''. \<nexists>X\<langle>t' \<doteq> t''\<rangle> \<in> set S \<and> (t = t' \<cdot> rm_vars (set X) \<delta> \<or> t = t'' \<cdot> rm_vars (set X) \<delta>))"

  show "t \<in> trms\<^sub>s\<^sub>t S \<Longrightarrow> ?P t \<delta> S"
  proof (induction S)
    case (Cons x S) show ?case
    proof (cases "t \<in> trms\<^sub>s\<^sub>t S")
      case True
      hence "?P t \<delta> S" using Cons by simp
      thus ?thesis
      apply (cases x)
      by (metis (no_types, lifting) Un_iff list.set_intros(2) strand_subst_hom(2) trms\<^sub>s\<^sub>t_cons)+
    next
      case False
      hence **: "t = trm\<^sub>s\<^sub>t\<^sub>p x \<or> t = trm_r\<^sub>s\<^sub>t\<^sub>p x" using Cons.prems by auto
      thus ?thesis
      proof (cases x)
        case (Inequality X s s')
        hence "t \<cdot> rm_vars (set X) \<delta> = trm\<^sub>s\<^sub>t\<^sub>p (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) \<or> t \<cdot> rm_vars (set X) \<delta> = trm_r\<^sub>s\<^sub>t\<^sub>p (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>)"
          using ** by auto
        moreover have "\<nexists>X\<langle>s \<doteq> s'\<rangle> \<in> set (x#S)" using Inequality by simp
        ultimately show ?thesis using Inequality by force
      qed auto
    qed
  qed simp

  show "t \<in> trms\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>t \<delta>) \<Longrightarrow> ?Q t \<delta> S"
  proof (induction S)
    case (Cons x S) show ?case
    proof (cases "t \<in> trms\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>t \<delta>)")
      case True
      hence "?Q t \<delta> S" using Cons by simp
      thus ?thesis by (cases x) auto
    next
      case False
      hence **: "t = trm\<^sub>s\<^sub>t\<^sub>p (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) \<or> t = trm_r\<^sub>s\<^sub>t\<^sub>p (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>)" using Cons.prems by auto
      thus ?thesis
      proof (cases x)
        case (Inequality X s s')
        hence "t = trm\<^sub>s\<^sub>t\<^sub>p x \<cdot> rm_vars (set X) \<delta> \<or> t = trm_r\<^sub>s\<^sub>t\<^sub>p x \<cdot> rm_vars (set X) \<delta>"
          using ** by auto
        moreover have "\<nexists>X\<langle>s \<doteq> s'\<rangle> \<in> set (x#S)" using Inequality by simp
        ultimately show ?thesis using Inequality by auto
      qed auto
    qed
  qed simp
qed

lemma wf_trm_subst_rm_vars: "wf\<^sub>t\<^sub>r\<^sub>m (\<delta> v) \<Longrightarrow> wf\<^sub>t\<^sub>r\<^sub>m (rm_vars X \<delta> v)"
by auto

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 SMP_mono:
  assumes "A \<subseteq> B"
  shows "SMP\<^sub>s\<^sub>t A \<subseteq> SMP\<^sub>s\<^sub>t B"
proof
  fix t assume "t \<in> SMP\<^sub>s\<^sub>t A" thus "t \<in> SMP\<^sub>s\<^sub>t B" using assms by (induct t rule: SMP\<^sub>s\<^sub>t.induct) auto
qed

lemma wt_subst_SMP_subset:
  assumes "trms\<^sub>s\<^sub>t S \<subseteq> SMP\<^sub>s\<^sub>t S'" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>" "\<And>v. wf\<^sub>t\<^sub>r\<^sub>m (\<delta> v)"
  shows "trms\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>t \<delta>) \<subseteq> SMP\<^sub>s\<^sub>t S'"
proof
  fix t assume *: "t \<in> trms\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>t \<delta>)"
  { fix t' assume "t = t' \<cdot> \<delta>" "t' \<in> trms\<^sub>s\<^sub>t S"
    hence "t \<in> SMP\<^sub>s\<^sub>t S'" using assms SMP\<^sub>s\<^sub>t.Substitution by auto
  } moreover {
    fix X t' t''
    assume "\<nexists>X\<langle>t' \<doteq> t''\<rangle> \<in> set S" "t = t' \<cdot> rm_vars (set X) \<delta> \<or> t = t'' \<cdot> rm_vars (set X) \<delta>"
    hence "t \<in> SMP\<^sub>s\<^sub>t S'"
      using assms(1,3) SMP\<^sub>s\<^sub>t.Substitution[OF _ wt_subst_rm_vars[OF assms(2), of "set X"]]
            wf_trm_subst_rm_vars
      by auto
  } ultimately show "t \<in> SMP\<^sub>s\<^sub>t S'" using trm_strand_subst_cong(2)[OF *] by blast
qed

lemma MP_singleton: "trms\<^sub>s\<^sub>t [x] = {trm\<^sub>s\<^sub>t\<^sub>p x} \<union> {trm_r\<^sub>s\<^sub>t\<^sub>p x}" by simp

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

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

lemma SMP_wt_subst_subset:
  assumes "t \<in> SMP\<^sub>s\<^sub>t (M \<cdot>set \<I>)" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>" "\<forall>v. wf\<^sub>t\<^sub>r\<^sub>m (\<I> v)"
  shows "t \<in> SMP\<^sub>s\<^sub>t M"
using assms by (induct t rule: SMP\<^sub>s\<^sub>t.induct) 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 eqs_tfr_cons_split:
  assumes "eqs_tfr\<^sub>s\<^sub>t (x#S)"
  shows "eqs_tfr\<^sub>s\<^sub>t [x]" "eqs_tfr\<^sub>s\<^sub>t S"
using assms by fastforce+

lemma eqs_tfr_append_split:
  assumes "eqs_tfr\<^sub>s\<^sub>t (S@S')"
  shows "eqs_tfr\<^sub>s\<^sub>t S" "eqs_tfr\<^sub>s\<^sub>t S'"
using assms by fastforce+

lemma eqs_tfr_append_split':
  assumes "eqs_tfr\<^sub>s\<^sub>t (S@x#S')"
  shows "eqs_tfr\<^sub>s\<^sub>t (S@S')"
using assms by fastforce

lemma eqs_tfr_append:
  assumes "eqs_tfr\<^sub>s\<^sub>t S" "eqs_tfr\<^sub>s\<^sub>t S'"
  shows "eqs_tfr\<^sub>s\<^sub>t (S@S')"
using assms by fastforce

lemma eqs_tfr_wt_subst_apply:
  assumes "eqs_tfr\<^sub>s\<^sub>t S" and \<theta>: "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>" "\<And>x. wf\<^sub>t\<^sub>r\<^sub>m (\<theta> x)"
  shows "eqs_tfr\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>t \<theta>)"
using assms(1)
proof (induction S)
  case (Cons x S)
  hence IH: "eqs_tfr\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>t \<theta>)" using eqs_tfr_cons_split(2)[of x S] by fastforce
  thus ?case
  proof (cases x)
    case (Equality 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> = ((t \<cdot> \<theta>) \<doteq> (t' \<cdot> \<theta>))#(S \<cdot>\<^sub>s\<^sub>t \<theta>)" using \<open>x = t \<doteq> t'\<close> by auto
    ultimately show ?thesis using IH by auto
  next
    case (Inequality X t t')
    hence "\<forall>x \<in> set X \<union> FV t \<union> FV t'. \<exists>a. \<Gamma> (Var x) = TAtom a"
      using Cons.prems by fastforce+
    hence "\<forall>x \<in> set X \<union> FV (t \<cdot> rm_vars (set X) \<theta>) \<union> FV (t' \<cdot> rm_vars (set X) \<theta>). \<exists>a. \<Gamma> (Var x) = TAtom a"
      using wt_subst_TAtom_FV[OF wt_subst_rm_vars[OF \<theta>(1), of "set X"]]
            wt_subst_trm'[OF wt_subst_rm_vars[OF \<theta>(1), of "set X"]]
            wf_trm_subst_rm_vars[of \<theta> _ "set X"] \<theta>(2)
      by blast
    moreover have "(x#S) \<cdot>\<^sub>s\<^sub>t \<theta> = \<nexists>X\<langle>(t \<cdot> rm_vars (set X) \<theta>) \<doteq> (t' \<cdot> rm_vars (set X) \<theta>)\<rangle>#(S \<cdot>\<^sub>s\<^sub>t \<theta>)"
      using \<open>x = \<nexists>X\<langle>t \<doteq> t'\<rangle>\<close> by auto
    ultimately show ?thesis using IH by simp
  qed auto
qed simp

lemma eqs_tfr_same_type:
  "eqs_tfr\<^sub>s\<^sub>t (S@t \<doteq> t'#S') \<Longrightarrow> Unifier \<delta> t t' \<Longrightarrow> \<Gamma> t = \<Gamma> t'"
by force+

lemma tfr_union_subset: "tfr\<^sub>s\<^sub>t (A \<union> B) \<Longrightarrow> tfr\<^sub>s\<^sub>t A"
using assms SMP_append'[of A B] by simp

subsection {* Well-typedness and type-flaw resistance preservation *}
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
    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
  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 "\<And>t. \<Gamma> t = \<Gamma> (t \<cdot> \<sigma>'')" 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 "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (subst v t) \<subseteq> {v}" unfolding subst_def by auto
    hence *: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma> \<subseteq> insert v (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>'')"
      using tt \<sigma> \<sigma>''(1) snoc.prems(2) subst_dom_comp_subset[of _ \<sigma>''] by auto
    
    have "v \<notin> set (map fst \<sigma>')" using tt snoc.prems(2) by auto
    hence "v \<notin> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>''" using \<sigma>''(1) subst_of_dom_subset[of \<sigma>'] by auto

    { fix w assume "w \<in> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>''"
      hence "\<sigma> w = \<sigma>'' w" using \<sigma>2 \<sigma>''(1) \<open>v \<notin> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<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 LI_preserves_eqs_tfr_single:
  assumes "(S,\<theta>) \<leadsto> (S',\<theta>')" "wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S \<theta>" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>" "\<And>v. wf\<^sub>t\<^sub>r\<^sub>m (\<theta> v)"
  and "eqs_tfr\<^sub>s\<^sub>t S" "tfr\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S)"
  shows "eqs_tfr\<^sub>s\<^sub>t S'"
using assms
proof (induction rule: LI_rel.induct)
  case (Compose S X f S' \<theta>)
  { fix t t' assume *: "t \<doteq> t' \<in> set (S@map Send X@S')" "\<exists>\<delta>. Unifier \<delta> t t'"
    hence "t \<doteq> t' \<in> set (S@S')" by auto
    hence "\<Gamma> t = \<Gamma> t'" using Compose.prems(4) *(2) by simp
  } moreover {
    fix Y t t' assume "\<nexists>Y\<langle>t \<doteq> t'\<rangle> \<in> set (S@map Send X@S')"
    hence "\<nexists>Y\<langle>t \<doteq> t'\<rangle> \<in> set (S@S')" by auto
    hence "\<forall>x\<in>set Y \<union> FV t \<union> FV t'. \<exists>a. \<Gamma> (Var x) = Var a" using Compose.prems(4) by auto
  } ultimately show ?case by metis
next
  case (Unify S f Y \<delta> X S' \<theta>)
  have "eqs_tfr\<^sub>s\<^sub>t (S@S')" using eqs_tfr_append_split'[OF Unify.prems(4)] by metis

  have "wf\<^sub>t\<^sub>r\<^sub>m (Fun f X)" using Unify.prems(5) by simp
  moreover have "wf\<^sub>t\<^sub>r\<^sub>m (Fun f Y)"
  proof -
    obtain x where True "x \<in> set S" "Fun f Y \<sqsubseteq> trm\<^sub>s\<^sub>t\<^sub>p x" "wf\<^sub>t\<^sub>r\<^sub>m (trm\<^sub>s\<^sub>t\<^sub>p x)"
      using Unify.hyps(2) Unify.prems(5) by auto
    thus ?thesis
      using wf_trm_subterm[OF \<open>wf\<^sub>t\<^sub>r\<^sub>m (trm\<^sub>s\<^sub>t\<^sub>p x)\<close>, of "Fun f Y"] 
      by (cases "Fun f Y = trm\<^sub>s\<^sub>t\<^sub>p x", auto)
  qed
  moreover have
      "Fun f X \<in> SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t (S@snd\<langle>Fun f X\<rangle>#S'))" "Fun f Y \<in> SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t (S@snd\<langle>Fun f X\<rangle>#S'))"
    using SMP_append[of S "snd\<langle>Fun f X\<rangle>#S'"] SMP_Cons[of "snd\<langle>Fun f X\<rangle>" S']
          SMP_ikI[OF Unify.hyps(2)]
    by auto
  hence "\<Gamma> (Fun f X) = \<Gamma> (Fun f Y)"
    using Unify.prems(5) mgu_gives_MGU[OF Unify.hyps(3)[symmetric]]
    by blast
  ultimately have "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>" using mgu_wt_if_same_type[OF Unify.hyps(3)[symmetric]] by metis
  moreover have "\<And>x. wf\<^sub>t\<^sub>r\<^sub>m (\<delta> x)"
    by (rule mgu_wf_trm[OF Unify.hyps(3)[symmetric] \<open>wf\<^sub>t\<^sub>r\<^sub>m (Fun f X)\<close> \<open>wf\<^sub>t\<^sub>r\<^sub>m (Fun f Y)\<close>])
  ultimately show ?case using eqs_tfr_wt_subst_apply[OF \<open>eqs_tfr\<^sub>s\<^sub>t (S@S')\<close>] by metis
next
  case (Equality S \<delta> t t' S' \<theta>)
  have "eqs_tfr\<^sub>s\<^sub>t (S@S')" "\<Gamma> t = \<Gamma> t'"
    using eqs_tfr_same_type[of S t t' S']
          eqs_tfr_append_split'[of S _ S']
          MGU_is_Unifier[OF mgu_gives_MGU[OF Equality.hyps(2)[symmetric]]]
          Equality.prems(4)
    by blast+
  moreover have "wf\<^sub>t\<^sub>r\<^sub>m t" "wf\<^sub>t\<^sub>r\<^sub>m t'" using Equality.prems(5) by auto
  ultimately have "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>"
    using mgu_wt_if_same_type[OF Equality.hyps(2)[symmetric]]
    by metis
  moreover have "\<And>x. wf\<^sub>t\<^sub>r\<^sub>m (\<delta> x)"
    by (rule mgu_wf_trm[OF Equality.hyps(2)[symmetric] \<open>wf\<^sub>t\<^sub>r\<^sub>m t\<close> \<open>wf\<^sub>t\<^sub>r\<^sub>m t'\<close>])
  ultimately show ?case using eqs_tfr_wt_subst_apply[OF \<open>eqs_tfr\<^sub>s\<^sub>t (S@S')\<close>] by metis
qed

lemma LI_in_SMP_subset_single:
  assumes "(S,\<theta>) \<leadsto> (S',\<theta>')" "wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S \<theta>" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>" "tfr\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S)" "eqs_tfr\<^sub>s\<^sub>t S"
  and "trms\<^sub>s\<^sub>t S \<subseteq> SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S'')" "\<And>v. wf\<^sub>t\<^sub>r\<^sub>m (\<theta> v)"
  shows "trms\<^sub>s\<^sub>t S' \<subseteq> SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S'')"
using assms
proof (induction rule: LI_rel.induct)
  case (Compose S X f S' \<theta>)
  hence "SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t [snd\<langle>Fun f X\<rangle>]) \<subseteq> SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S'')"
  proof -
    have *: "\<And>S S'. SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S \<union> trms\<^sub>s\<^sub>t S') = SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t (S @ S'))"
      using SMP_append SMP_append' by presburger
    hence **: "SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t ((S@snd\<langle>Fun f X\<rangle>#S')@S'')) = SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S'')"
      by (metis (no_types) Compose.prems(5) SMP_subset_union_eq)
    have "SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S'') \<subseteq> SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S'')" by simp
    thus ?thesis by (metis (no_types) * ** SMP_Cons SMP_append' Un_subset_iff)
  qed
  thus ?case using Compose.prems(5) by force
next
  case (Unify S f Y \<delta> X S' \<theta>)
  have "Fun f X \<in> SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t (S@snd\<langle>Fun f X\<rangle>#S'))" by auto
  moreover have "MGU \<delta> (Fun f X) (Fun f Y)"
    by (metis mgu_gives_MGU[OF Unify.hyps(3)[symmetric]])
  moreover have
        "\<And>x. x \<in> set S \<Longrightarrow> wf\<^sub>t\<^sub>r\<^sub>m (trm\<^sub>s\<^sub>t\<^sub>p x)" "wf\<^sub>t\<^sub>r\<^sub>m (Fun f X)"
    using Unify.prems(1,2,3) by force+
  moreover have "Fun f Y \<in> SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t (S@snd\<langle>Fun f X\<rangle>#S'))"
    by (meson SMP_ikI Unify.hyps(2) contra_subsetD ik_append_subset(1))
  ultimately have "wf\<^sub>t\<^sub>r\<^sub>m (Fun f Y)" "\<Gamma> (Fun f X) = \<Gamma> (Fun f Y)"
    using trp_ik_subterm_exD[OF trpI[OF \<open>Fun f Y \<in> ik\<^sub>s\<^sub>t S\<close>]] \<open>tfr\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t (S@snd\<langle>Fun f X\<rangle>#S'))\<close>
    by (metis subterm_def wf_trm_subterm, blast)
  hence "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>" by (metis mgu_wt_if_same_type[OF Unify.hyps(3)[symmetric] \<open>wf\<^sub>t\<^sub>r\<^sub>m (Fun f X)\<close>])
  moreover have "\<And>v. wf\<^sub>t\<^sub>r\<^sub>m (\<delta> v)"
    by (fact mgu_wf_trm[OF Unify.hyps(3)[symmetric] \<open>wf\<^sub>t\<^sub>r\<^sub>m (Fun f X)\<close> \<open>wf\<^sub>t\<^sub>r\<^sub>m (Fun f Y)\<close>])
  ultimately have "trms\<^sub>s\<^sub>t ((S@snd\<langle>Fun f X\<rangle>#S') \<cdot>\<^sub>s\<^sub>t \<delta>) \<subseteq> SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S'')"
    using SMP\<^sub>s\<^sub>t.Substitution Unify.prems(5) wt_subst_SMP_subset by metis
  thus ?case by auto
next
  case (Equality S \<delta> t t' S' \<theta>)
  hence "\<Gamma> t = \<Gamma> t'"
    using eqs_tfr_same_type MGU_is_Unifier[OF mgu_gives_MGU[OF Equality.hyps(2)[symmetric]]]
    by metis
  moreover have "t \<in> SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t (S@t \<doteq> t'#S'))" "t' \<in> SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t (S@t \<doteq> t'#S'))"
    using Equality.prems(1) by auto
  moreover have "MGU \<delta> t t'" using mgu_gives_MGU[OF Equality.hyps(2)[symmetric]] by metis
  moreover have "\<And>x. x \<in> set S \<Longrightarrow> wf\<^sub>t\<^sub>r\<^sub>m (trm\<^sub>s\<^sub>t\<^sub>p x)" "wf\<^sub>t\<^sub>r\<^sub>m t" "wf\<^sub>t\<^sub>r\<^sub>m t'"
     using Equality.prems(1,2,3) by force+
  ultimately have "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>" by (metis mgu_wt_if_same_type[OF Equality.hyps(2)[symmetric] \<open>wf\<^sub>t\<^sub>r\<^sub>m t\<close>])
  moreover have "\<And>v. wf\<^sub>t\<^sub>r\<^sub>m (\<delta> v)"
    by (fact mgu_wf_trm[OF Equality.hyps(2)[symmetric] \<open>wf\<^sub>t\<^sub>r\<^sub>m t\<close> \<open>wf\<^sub>t\<^sub>r\<^sub>m t'\<close>])
  ultimately have "trms\<^sub>s\<^sub>t ((S@t \<doteq> t'#S') \<cdot>\<^sub>s\<^sub>t \<delta>) \<subseteq> SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S'')"
    using SMP\<^sub>s\<^sub>t.Substitution Equality.prems wt_subst_SMP_subset by metis
  thus ?case by auto
qed

lemma LI_preserves_tfr_single:
  assumes "(S,\<theta>) \<leadsto> (S',\<theta>')" "wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S \<theta>" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>" "\<And>v. wf\<^sub>t\<^sub>r\<^sub>m (\<theta> v)" "tfr\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S)"
           "eqs_tfr\<^sub>s\<^sub>t S"
  shows "tfr\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S')"
using assms
proof (induction rule: LI_rel.induct)
  case (Compose S X f S' \<theta>)
  let ?SMPmap = "SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t (S@map Send X@S')) - (Var`\<V>)"
  have "?SMPmap \<subseteq> SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t (S@snd\<langle>Fun f X\<rangle>#S')) - (Var`\<V>)"
    using SMP_fun_map_snd_subset[of X f]
          SMP_append[of "map Send X" S'] SMP_Cons[of "snd\<langle>Fun f X\<rangle>" S']
          SMP_append[of S "snd\<langle>Fun f X\<rangle>#S'"] SMP_append[of S "map Send X@S'"]
    by auto
  hence "\<forall>s \<in> ?SMPmap. \<forall>t \<in> ?SMPmap. (\<exists>\<delta>. Unifier \<delta> s t) \<longrightarrow> \<Gamma> s = \<Gamma> t"
    using Compose by (meson subsetCE)
  thus ?case
    using LI_preserves_trm_wf[OF r_into_rtrancl[OF LI_rel.Compose[OF Compose.hyps]], of S']
          Compose.prems(4)
    unfolding trms\<^sub>s\<^sub>t_def by blast
next
  case (Unify S f Y \<delta> X S' \<theta>)
  let ?SMP\<delta> = "SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t (S@S' \<cdot>\<^sub>s\<^sub>t \<delta>)) - (Var`\<V>)"

  have "SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t (S@S' \<cdot>\<^sub>s\<^sub>t \<delta>)) \<subseteq> SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t (S@snd\<langle>Fun f X\<rangle>#S'))"
  proof
    fix s assume "s \<in> SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t (S@S' \<cdot>\<^sub>s\<^sub>t \<delta>))" thus "s \<in> SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t (S@snd\<langle>Fun f X\<rangle>#S'))"
      using LI_in_SMP_subset_single[
              OF LI_rel.Unify[OF Unify.hyps] Unify.prems(1,2,4,5)
                 MP_subset_SMP(2)[of "S@snd\<langle>Fun f X\<rangle>#S'"] Unify.prems(3)]
      by (metis SMP_append' SMP_subset_union_eq Un_iff)
  qed
  hence "\<forall>s \<in> ?SMP\<delta>. \<forall>t \<in> ?SMP\<delta>. (\<exists>\<delta>. Unifier \<delta> s t) \<longrightarrow> \<Gamma> s = \<Gamma> t"
    using Unify.prems(4) by (meson Diff_iff subsetCE)
  thus ?case
    using LI_preserves_trm_wf[OF r_into_rtrancl[OF LI_rel.Unify[OF Unify.hyps]], of S']
          Unify.prems(4)
    unfolding trms\<^sub>s\<^sub>t_def by blast
next
  case (Equality S \<delta> t t' S' \<theta>)
  let ?SMP\<delta> = "SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t (S@S' \<cdot>\<^sub>s\<^sub>t \<delta>)) - (Var`\<V>)"

  have "SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t (S@S' \<cdot>\<^sub>s\<^sub>t \<delta>)) \<subseteq> SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t (S@t \<doteq> t'#S'))"
  proof
    fix s assume "s \<in> SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t (S@S' \<cdot>\<^sub>s\<^sub>t \<delta>))" thus "s \<in> SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t (S@t \<doteq> t'#S'))"
      using LI_in_SMP_subset_single[
              OF LI_rel.Equality[OF Equality.hyps] Equality.prems(1,2,4,5)
                 MP_subset_SMP(2)[of "S@t \<doteq> t'#S'"] Equality.prems(3)]
      by (metis SMP_append' SMP_subset_union_eq Un_iff)
  qed
  hence "\<forall>s \<in> ?SMP\<delta>. \<forall>t \<in> ?SMP\<delta>. (\<exists>\<delta>. Unifier \<delta> s t) \<longrightarrow> \<Gamma> s = \<Gamma> t"
    using Equality.prems by (meson Diff_iff subsetCE)
  thus ?case
    using LI_preserves_trm_wf[OF r_into_rtrancl[OF LI_rel.Equality[OF Equality.hyps]], of S']
          Equality.prems
    unfolding trms\<^sub>s\<^sub>t_def by blast
qed

lemma LI_preserves_welltypedness_single:
  assumes "(S,\<theta>) \<leadsto> (S',\<theta>')" "wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S \<theta>" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>" "\<forall>v. wf\<^sub>t\<^sub>r\<^sub>m (\<theta> v)"
  and "tfr\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S)" "eqs_tfr\<^sub>s\<^sub>t S"
  shows "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>' \<and> (\<forall>v. wf\<^sub>t\<^sub>r\<^sub>m (\<theta>' v))"
using assms
proof (induction rule: LI_rel.induct)
  case (Unify S f Y \<delta> X S' \<theta>)
  have "wf\<^sub>t\<^sub>r\<^sub>m (Fun f X)" using Unify.prems(4) by simp
  moreover have "wf\<^sub>t\<^sub>r\<^sub>m (Fun f Y)"
  proof -
    obtain x where True "x \<in> set S" "Fun f Y \<sqsubseteq> trm\<^sub>s\<^sub>t\<^sub>p x" "wf\<^sub>t\<^sub>r\<^sub>m (trm\<^sub>s\<^sub>t\<^sub>p x)"
      using Unify.hyps(2) Unify.prems(4) by auto
    thus ?thesis
      using wf_trm_subterm[OF \<open>wf\<^sub>t\<^sub>r\<^sub>m (trm\<^sub>s\<^sub>t\<^sub>p x)\<close>, of "Fun f Y"] 
      by (cases "Fun f Y = trm\<^sub>s\<^sub>t\<^sub>p x", auto)
  qed
  moreover have
      "Fun f X \<in> SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t (S@snd\<langle>Fun f X\<rangle>#S'))" "Fun f Y \<in> SMP\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t (S@snd\<langle>Fun f X\<rangle>#S'))"
    using SMP_append[of S "snd\<langle>Fun f X\<rangle>#S'"] SMP_Cons[of "snd\<langle>Fun f X\<rangle>" S']
          SMP_ikI[OF Unify.hyps(2)]
    by auto
  hence "\<Gamma> (Fun f X) = \<Gamma> (Fun f Y)"
    using Unify.prems(4) mgu_gives_MGU[OF Unify.hyps(3)[symmetric]]
    by blast
  ultimately have "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>" using mgu_wt_if_same_type[OF Unify.hyps(3)[symmetric]] by metis

  have "\<forall>v. wf\<^sub>t\<^sub>r\<^sub>m (\<delta> v)"
    by (meson mgu_wf_trm[OF Unify.hyps(3)[symmetric] \<open>wf\<^sub>t\<^sub>r\<^sub>m (Fun f X)\<close> \<open>wf\<^sub>t\<^sub>r\<^sub>m (Fun f Y)\<close>])
  hence "\<forall>v. wf\<^sub>t\<^sub>r\<^sub>m ((\<theta> \<circ>\<^sub>s \<delta>) v)"
    unfolding subst_compose_def
    by (simp add: wf_trm_subst \<open>\<forall>v. wf\<^sub>t\<^sub>r\<^sub>m (\<theta> v)\<close>) 
  thus ?case by (metis wt_subst_compose[OF \<open>wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>\<close> \<open>wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>\<close>])
next
  case (Equality S \<delta> t t' S' \<theta>)
  have "wf\<^sub>t\<^sub>r\<^sub>m t" "wf\<^sub>t\<^sub>r\<^sub>m t'" using Equality.prems(4) by simp_all
  moreover have "\<Gamma> t = \<Gamma> t'"
    using \<open>eqs_tfr\<^sub>s\<^sub>t (S@t \<doteq> t'#S')\<close> MGU_is_Unifier[OF mgu_gives_MGU[OF Equality.hyps(2)[symmetric]]]
    by auto
  ultimately have "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>" using mgu_wt_if_same_type[OF Equality.hyps(2)[symmetric]] by metis

  have "\<forall>v. wf\<^sub>t\<^sub>r\<^sub>m (\<delta> v)"
    by (meson mgu_wf_trm[OF Equality.hyps(2)[symmetric] \<open>wf\<^sub>t\<^sub>r\<^sub>m t\<close> \<open>wf\<^sub>t\<^sub>r\<^sub>m t'\<close>])
  hence "\<forall>v. wf\<^sub>t\<^sub>r\<^sub>m ((\<theta> \<circ>\<^sub>s \<delta>) v)"
    unfolding subst_compose_def
    by (simp add: wf_trm_subst \<open>\<forall>v. wf\<^sub>t\<^sub>r\<^sub>m (\<theta> v)\<close>) 
  thus ?case by (metis wt_subst_compose[OF \<open>wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>\<close> \<open>wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>\<close>])
qed metis

lemma LI_preserves_welltypedness:
  assumes "(S,\<theta>) \<leadsto>\<^sup>* (S',\<theta>')" "wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S \<theta>" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>" "\<forall>v. wf\<^sub>t\<^sub>r\<^sub>m (\<theta> v)"
  and "tfr\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S)" "eqs_tfr\<^sub>s\<^sub>t S"
  shows "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>' \<and> (\<forall>v. wf\<^sub>t\<^sub>r\<^sub>m (\<theta>' v))"
using assms
proof (induction S \<theta> rule: converse_rtrancl_induct2)
  case (step S1 \<theta>1 S2 \<theta>2)
  hence "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>2 \<and> (\<forall>v. wf\<^sub>t\<^sub>r\<^sub>m (\<theta>2 v))" using LI_preserves_welltypedness_single by presburger
  moreover have "wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S2 \<theta>2"
    by (fact LI_preserves_wellformedness[OF r_into_rtrancl[OF step.hyps(1)] step.prems(1)])
  moreover have "tfr\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S2)"
    using LI_preserves_tfr_single[OF step.hyps(1)] step.prems by presburger
  moreover have "eqs_tfr\<^sub>s\<^sub>t S2"
    using LI_preserves_eqs_tfr_single[OF step.hyps(1)] step.prems by fastforce
  ultimately show ?case using step.IH by presburger
qed simp

lemma LI_preserves_tfr:
  assumes "(S,\<theta>) \<leadsto>\<^sup>* (S',\<theta>')" "wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S \<theta>" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>" "\<forall>v. wf\<^sub>t\<^sub>r\<^sub>m (\<theta> v)"
  and "tfr\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S)" "eqs_tfr\<^sub>s\<^sub>t S"
  shows "tfr\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S')" "eqs_tfr\<^sub>s\<^sub>t S'"
using assms
proof (induction S \<theta> rule: converse_rtrancl_induct2)
  case refl
  { case 1 thus ?case by blast }
  { case 2 thus ?case by blast }
next
  case (step S1 \<theta>1 S2 \<theta>2)
  { case 1
    have "wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S2 \<theta>2" "tfr\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S2)" "eqs_tfr\<^sub>s\<^sub>t S2"
      apply (fact LI_preserves_wellformedness[OF r_into_rtrancl[OF step.hyps(1)] "1.prems"(1)])
      apply (metis LI_preserves_tfr_single[OF step.hyps(1) "1.prems"(1,2)] "1.prems"(3,4,5))
      by (metis LI_preserves_eqs_tfr_single[OF step.hyps(1) "1.prems"(1,2)] "1.prems"(3,4,5))
    moreover have "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>2" "\<forall>v. wf\<^sub>t\<^sub>r\<^sub>m (\<theta>2 v)"
      using LI_preserves_welltypedness[OF r_into_rtrancl[OF step.hyps(1)] "1.prems"]
      by simp_all
    ultimately show ?case using step.IH by presburger
  }
  { case 2
    have "wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S2 \<theta>2" "tfr\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S2)" "eqs_tfr\<^sub>s\<^sub>t S2"
      apply (fact LI_preserves_wellformedness[OF r_into_rtrancl[OF step.hyps(1)] "2.prems"(1)])
      apply (metis LI_preserves_tfr_single[OF step.hyps(1) "2.prems"(1,2)] "2.prems"(3,4,5))
      by (metis LI_preserves_eqs_tfr_single[OF step.hyps(1) "2.prems"(1,2)] "2.prems"(3,4,5))
    moreover have "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>2" "\<forall>v. wf\<^sub>t\<^sub>r\<^sub>m (\<theta>2 v)"
      using LI_preserves_welltypedness[OF r_into_rtrancl[OF step.hyps(1)] "2.prems"]
      by simp_all
    ultimately show ?case using step.IH by presburger
  }
qed


subsection {* Well-typed satisfiable if simple *}
(* Proving the existence of a well-typed, but not bijective, interpretation *)
definition wt_interpretation_nonunique::"('fun,'var) subst" where
  "wt_interpretation_nonunique v \<equiv> (SOME t. \<Gamma> (Var v) = \<Gamma> t \<and> public_ground_wf_term t)"

lemma wt_interpretation_nonunique_properties:
  "wt_interpretation_nonunique v = t \<Longrightarrow> \<Gamma> (Var v) = \<Gamma> t \<and> public_ground_wf_term t"
using someI_ex[of "\<lambda>t. \<Gamma> (Var v) = \<Gamma> t \<and> public_ground_wf_term t",
               OF type_pgwt_inhabited[of "Var v"]]
unfolding wt_interpretation_nonunique_def wf\<^sub>t\<^sub>r\<^sub>m_def by simp

lemma wt_interpretation_exists: 
  obtains \<I>::"('fun,'var) subst"
  where "interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>" "img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I> \<subseteq> public_ground_wf_terms"
proof -
  have "\<And>v. wt_interpretation_nonunique v \<noteq> Var v"
    using wt_interpretation_nonunique_properties pgwt_ground by force
  hence "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t wt_interpretation_nonunique = UNIV" by auto
  moreover have "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t wt_interpretation_nonunique)" unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def
    by (simp add: wt_interpretation_nonunique_properties pgwt_ground)
  ultimately have "interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t wt_interpretation_nonunique" by metis
  moreover have "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t wt_interpretation_nonunique"
    unfolding wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def using wt_interpretation_nonunique_properties by simp
  moreover have "img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t wt_interpretation_nonunique \<subseteq> public_ground_wf_terms"
    unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by (auto simp add: wt_interpretation_nonunique_properties)
  ultimately show ?thesis using that by auto
qed

lemma wt_bij_finite_tatom_subst_exists_single:
  assumes "finite (S::'var set)" "finite (T::('fun,'var) terms)"
  and "\<And>x. x \<in> S \<Longrightarrow> \<Gamma> (Var x) = TAtom a"
  shows "\<exists>\<sigma>::('fun,'var) subst. dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma> = S
                      \<and> bij_betw \<sigma> (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>) (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>)
                      \<and> img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma> \<subseteq> ((\<lambda>c. Fun c []) `  {c. \<Gamma> (Fun c []) = TAtom a \<and>
                                                            public c \<and> arity c = 0}) - T
                      \<and> wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>
                      \<and> (\<forall>x. wf\<^sub>t\<^sub>r\<^sub>m (\<sigma> x))"
proof -
  let ?U = "{c. \<Gamma> (Fun c []) = TAtom a \<and> public c \<and> arity c = 0}"

  obtain \<sigma> where \<sigma>:
      "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma> = S" "bij_betw \<sigma> (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>) (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>)"
      "img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma> \<subseteq> ((\<lambda>c. Fun c []) ` ?U) - T"
    using bij_finite_const_subst_exists'[OF assms(1,2) infinite_typed_consts'[of a]]
    by auto

  { fix x assume "x \<notin> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>" hence "\<Gamma> (Var x) = \<Gamma> (\<sigma> x)" by auto }
  moreover
  { fix x assume "x \<in> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>"
    hence "\<exists>c \<in> ?U. \<sigma> x = Fun c [] \<and> arity c = 0" using \<sigma> by auto
    hence "\<Gamma> (\<sigma> x) = TAtom a" "wf\<^sub>t\<^sub>r\<^sub>m (\<sigma> x)" using assms(3) const_type wf_trmI[of "[]"] by auto
    hence "\<Gamma> (Var x) = \<Gamma> (\<sigma> x)" "wf\<^sub>t\<^sub>r\<^sub>m (\<sigma> x)" using assms(3) \<sigma>(1) by force+
  }
  ultimately have "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>" "\<forall>x. wf\<^sub>t\<^sub>r\<^sub>m (\<sigma> x)" unfolding wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by force+
  thus ?thesis using \<sigma> by auto
qed

lemma wt_bij_finite_tatom_subst_exists:
  assumes "finite (S::'var set)" "finite (T::('fun,'var) terms)"
  and "\<And>x. x \<in> S \<Longrightarrow> \<exists>a. \<Gamma> (Var x) = TAtom a"
  shows "\<exists>\<sigma>::('fun,'var) subst. dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma> = S
                      \<and> bij_betw \<sigma> (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>) (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>)
                      \<and> img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma> \<subseteq> ((\<lambda>c. Fun c []) `  \<C>\<^sub>p\<^sub>u\<^sub>b) - T
                      \<and> wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>
                      \<and> (\<forall>x. wf\<^sub>t\<^sub>r\<^sub>m (\<sigma> x))"
using assms
proof (induction rule: finite_induct)
  case empty
  have "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t Var = {}"
       "bij_betw Var (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t Var) (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t Var)"
       "img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t Var \<subseteq> ((\<lambda>c. Fun c []) `  \<C>\<^sub>p\<^sub>u\<^sub>b) - T"
       "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t Var"
       "\<forall>x. wf\<^sub>t\<^sub>r\<^sub>m (Var x)"
    unfolding bij_betw_def img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def
    by auto
  thus ?case by auto
next
  case (insert x S)
  then obtain a where a: "\<Gamma> (Var x) = TAtom a" by fastforce

  from insert obtain \<sigma> where \<sigma>:
      "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma> = S" "bij_betw \<sigma> (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>) (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>)"
      "img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma> \<subseteq> ((\<lambda>c. Fun c []) `  \<C>\<^sub>p\<^sub>u\<^sub>b) - T" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>"
      "\<forall>x. wf\<^sub>t\<^sub>r\<^sub>m (\<sigma> x)"
    by auto

  let ?S' = "{y \<in> S. \<Gamma> (Var y) = TAtom a}"
  let ?T' = "T \<union> img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>"

  have *: "finite (insert x ?S')" using insert by simp
  have **: "finite ?T'" using insert.prems(1) insert.hyps(1) \<sigma>(1) unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by simp
  have ***: "\<And>y. y \<in> insert x ?S' \<Longrightarrow> \<Gamma> (Var y) = TAtom a" using a by auto

  obtain \<delta> where \<delta>:
      "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> = insert x ?S'" "bij_betw \<delta> (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>) (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>)"
      "img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<subseteq> ((\<lambda>c. Fun c []) `  \<C>\<^sub>p\<^sub>u\<^sub>b) - ?T'" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>" "\<forall>x. wf\<^sub>t\<^sub>r\<^sub>m (\<delta> x)"
    using wt_bij_finite_tatom_subst_exists_single[OF * ** ***] const_type_inv[of _ "[]" a]
    unfolding \<C>\<^sub>p\<^sub>u\<^sub>b_def \<C>_def \<Sigma>n_def by blast

  obtain \<theta> where \<theta>: "\<theta> \<equiv> \<lambda>y. if x = y then \<delta> y else \<sigma> y" by simp

  have x_dom: "x \<notin> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>" "x \<in> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>" "x \<in> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>"
    using insert.hyps(2) \<sigma>(1) \<delta>(1) \<theta> by auto
  moreover have ground_imgs: "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>)" "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>)"
    using pgwt_ground \<sigma>(3) \<delta>(3) by auto
  ultimately have x_img: "\<sigma> x \<notin> img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>" "\<delta> x \<in> img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>" using ground_subst_dom_iff_img by auto

  have "ground (insert (\<delta> x) (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>))" using ground_imgs x_dom by auto
  have \<theta>_dom: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> = insert x (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>)" using \<delta>(1) \<theta> by auto
  have \<theta>_img: "img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> = insert (\<delta> x) (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>)"
  proof
    show "img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<subseteq> insert (\<delta> x) (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>)"
    proof
      fix t assume "t \<in> img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>"
      then obtain y where "y \<in> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>" "t = \<theta> y" unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto
      thus "t \<in> insert (\<delta> x) (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>)" using \<theta> by auto
    qed
    show "insert (\<delta> x) (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>) \<subseteq> img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>"
    proof
      fix t assume t: "t \<in> insert (\<delta> x) (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>)"
      hence "FV t = {}" using ground_imgs x_img(2) by auto
      hence "t \<noteq> Var x" by auto
      show "t \<in> img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>"
      proof (cases "t = \<delta> x")
        case True thus ?thesis using subst_imgI \<theta> \<open>t \<noteq> Var x\<close> by metis
      next
        case False
        hence "t \<in> img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>" using t by auto
        then obtain y where "\<sigma> y \<in> img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>" "t = \<sigma> y" unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto
        hence "y \<in> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>" "t \<noteq> Var y" using ground_subst_dom_iff_img[OF ground_imgs(1)] by auto
        hence "x \<noteq> y" using x_dom by auto
        hence "\<theta> y = \<sigma> y" unfolding \<theta> by auto
        thus ?thesis using \<open>t \<noteq> Var y\<close> \<open>t = \<sigma> y\<close> subst_imgI[of \<theta> y] by auto
      qed
    qed
  qed
  hence \<theta>_ground_img: "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>)" using ground_imgs x_img by auto

  have "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> = insert x S" using \<theta>_dom \<sigma>(1) by auto
  moreover have "bij_betw \<theta> (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>) (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>)"
  proof (intro bij_betwI')
    fix y z assume *: "y \<in> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>" "z \<in> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>"
    hence "FV (\<theta> y) = {}" "FV (\<theta> z) = {}" using \<theta>_ground_img by auto
    { assume "\<theta> y = \<theta> z" hence "y = z"
      proof (cases "\<theta> y \<in> img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma> \<and> \<theta> z \<in> img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>")
        case True
        hence **: "y \<in> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>" "z \<in> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>"
          using \<theta> \<theta>_dom x_img(2) \<delta>(3) True
          by (metis *(1) DiffE Un_upper2 insertE subsetCE,
              metis *(2) DiffE Un_upper2 insertE subsetCE)
        hence "y \<noteq> x" "z \<noteq> x" using x_dom by auto
        hence "\<theta> y = \<sigma> y" "\<theta> z = \<sigma> z" using \<theta> by auto
        thus ?thesis using \<open>\<theta> y = \<theta> z\<close> \<sigma>(2) ** unfolding bij_betw_def inj_on_def by auto
      qed (metis \<theta> * \<open>\<theta> y = \<theta> z\<close> \<theta>_dom ground_imgs(1) ground_subst_dom_iff_img insertE)
    }
    thus "(\<theta> y = \<theta> z) = (y = z)" by auto
  next
    fix y assume "y \<in> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>" thus "\<theta> y \<in> img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>" by auto
  next
    fix t assume "t \<in> img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>" thus "\<exists>z \<in> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>. t = \<theta> z" unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto
  qed
  moreover have "img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<subseteq> (\<lambda>c. Fun c []) ` \<C>\<^sub>p\<^sub>u\<^sub>b - T"
    using \<sigma>(3) \<delta>(3) \<theta> unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto
  moreover have "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>" using \<sigma>(4) \<delta>(4) \<theta> unfolding wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto
  moreover have "\<forall>x. wf\<^sub>t\<^sub>r\<^sub>m (\<theta> x)" using \<theta> \<sigma>(5) \<delta>(5) by simp
  ultimately show ?case by blast
qed

lemma strand_FV_bvars_disjointD:
  assumes "FV\<^sub>s\<^sub>t S \<inter> bvars\<^sub>s\<^sub>t S = {}" "\<nexists>X\<langle>t \<doteq> t'\<rangle> \<in> set S"
  shows "set X \<subseteq> bvars\<^sub>s\<^sub>t S" "(FV t \<union> FV t') - set X \<subseteq> FV\<^sub>s\<^sub>t S"
using assms by (induct S) auto

lemma strand_FV_bvars_disjoint_unfold:
  assumes "FV\<^sub>s\<^sub>t S \<inter> bvars\<^sub>s\<^sub>t S = {}" "\<nexists>X\<langle>t \<doteq> t'\<rangle> \<in> set S" "\<nexists>Y\<langle>u \<doteq> u'\<rangle> \<in> set S"
  shows "set Y \<inter> ((FV t \<union> FV t') - set X) = {}"
proof -
  have "set X \<subseteq> bvars\<^sub>s\<^sub>t S" "set Y \<subseteq> bvars\<^sub>s\<^sub>t S"
       "(FV t \<union> FV t') - set X \<subseteq> FV\<^sub>s\<^sub>t S" "(FV u \<union> FV u') - set Y \<subseteq> FV\<^sub>s\<^sub>t S"
    using strand_FV_bvars_disjointD[OF assms(1)] assms(2,3) by auto
  thus ?thesis using assms(1) by auto
qed

theorem wt_sat_if_simple:
  assumes "simple S" "wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S \<theta>" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>" "\<forall>v. wf\<^sub>t\<^sub>r\<^sub>m (\<theta> v)"
  and \<I>': "\<forall>X t t' \<delta>. \<nexists>X\<langle>t \<doteq> t'\<rangle> \<in> set S \<longrightarrow> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> = set X \<and> ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>)
                                        \<longrightarrow> t \<cdot> \<delta> \<cdot> \<I>' \<noteq> t' \<cdot> \<delta> \<cdot> \<I>'"
         "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>')"
         "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>' = {x \<in> vars\<^sub>s\<^sub>t S. \<exists>X t t'. \<nexists>X\<langle>t \<doteq> t'\<rangle> \<in> set S \<and> x \<in> FV t \<union> FV t' \<and> x \<notin> set X}"
  and eqs_tfr: "eqs_tfr\<^sub>s\<^sub>t S"
  shows "\<exists>\<I>. interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I> \<and> \<I> \<Turnstile>\<^sub>c \<langle>S, \<theta>\<rangle> \<and> wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I> \<and> (\<forall>x. wf\<^sub>t\<^sub>r\<^sub>m (\<I> x))"
proof -
  from \<open>wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S \<theta>\<close> have "wf\<^sub>s\<^sub>t {} S" "Idem \<theta>" and S_\<theta>_disj: "\<And>v. v \<in> vars\<^sub>s\<^sub>t S \<Longrightarrow> \<theta> v = Var v"
    using IdemI[of \<theta>] by auto
  
  obtain \<I>::"('fun,'var) subst"
    where \<I>: "interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>" "img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I> \<subseteq> public_ground_wf_terms"
    using wt_interpretation_exists by blast
  hence \<I>_deduct: "\<And>x M. M \<turnstile>\<^sub>c \<I> x" and \<I>_wf_trm: "\<forall>x. wf\<^sub>t\<^sub>r\<^sub>m (\<I> x)"
    using pgwt_deducible pgwt_wellformed by fastforce+

  let ?P = "\<lambda>\<delta> X. dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> = set X \<and> ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>)"
  let ?Sineqsvars = "{x \<in> vars\<^sub>s\<^sub>t S. \<exists>X t t'. \<nexists>X\<langle>t \<doteq> t'\<rangle> \<in> set S \<and> x \<in> FV t \<union> FV t' \<and> x \<notin> set X}"
  let ?Strms = "\<Union>(subterms ` trms\<^sub>s\<^sub>t S)"
  have *: "finite ?Sineqsvars" "finite ?Strms" "\<And>x. x \<in> ?Sineqsvars \<Longrightarrow> \<exists>a. \<Gamma> (Var x) = TAtom a"
    using eqs_tfr by auto

  have "FV\<^sub>s\<^sub>t S \<inter> bvars\<^sub>s\<^sub>t S = {}" using \<open>wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S \<theta>\<close> unfolding wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r_def by metis
  hence ineqs_vars_not_bound: "\<forall>X t t' x. \<nexists>X\<langle>t \<doteq> t'\<rangle> \<in> set S \<longrightarrow> x \<in> ?Sineqsvars \<longrightarrow> x \<notin> set X"
    using strand_FV_bvars_disjoint_unfold by blast

  obtain \<sigma>::"('fun,'var) subst"
    where \<sigma>_FV_dom: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma> = ?Sineqsvars"
    and \<sigma>_bij_dom_img: "bij_betw \<sigma> (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>) (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>)"
    and \<sigma>_fresh_pub_consts_img: "img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma> \<subseteq> ((\<lambda>c. Fun c []) `  \<C>\<^sub>p\<^sub>u\<^sub>b) - ?Strms"
    and \<sigma>_wt: "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>"
    and \<sigma>_wf_trm: "\<forall>x. wf\<^sub>t\<^sub>r\<^sub>m (\<sigma> x)"
    using wt_bij_finite_tatom_subst_exists[OF *] by blast

  have "img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma> \<subseteq> public_ground_wf_terms - ?Strms"
      and \<sigma>_pgwt_img: "img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma> \<subseteq> public_ground_wf_terms"
    using \<sigma>_fresh_pub_consts_img pgwt_is_empty_synth public_const_deduct(2) by auto

  have \<sigma>_img_ground: "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>)" using \<sigma>_pgwt_img pgwt_ground by auto
  hence "inj \<sigma>"
    using \<sigma>_bij_dom_img subst_inj_is_bij_betw_dom_img_if_ground_img unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto

  have "\<forall>t \<in> img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>. \<exists>c. t = Fun c []" using \<sigma>_fresh_pub_consts_img by auto

  have \<sigma>_ineqs_FV_dom: "\<And>X t t'. \<nexists>X\<langle>t \<doteq> t'\<rangle> \<in> set S \<Longrightarrow> FV t \<union> FV t' - set X \<subseteq> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>"
    using \<sigma>_FV_dom by fastforce

  have "\<And>X t t'. \<nexists>X\<langle>t \<doteq> t'\<rangle> \<in> set S \<Longrightarrow> \<forall>u \<in> img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>. u \<notin> subterms t \<union> subterms t'"
    using \<sigma>_pgwt_img PGWT[of _ "[]"] \<open>img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma> \<subseteq> public_ground_wf_terms - ?Strms\<close> by force
  moreover have "\<forall>X t t'. \<nexists>X\<langle>t \<doteq> t'\<rangle> \<in> set S \<longrightarrow> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma> \<inter> set X = {}"
    using ineqs_vars_not_bound \<sigma>_FV_dom by fastforce
  moreover have "\<forall>X t t' \<delta>. \<nexists>X\<langle>t \<doteq> t'\<rangle> \<in> set S \<longrightarrow> FV t \<union> FV t' - set X \<subseteq> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>'"
    using \<I>'(3) ineqs_vars_not_bound by fastforce
  moreover have "\<forall>X t t'. \<nexists>X\<langle>t \<doteq> t'\<rangle> \<in> set S \<longrightarrow> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>' \<inter> set X = {}"
    using \<I>'(3) ineqs_vars_not_bound by blast
  moreover have "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>' = dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>" using \<I>'(3) \<sigma>_FV_dom by metis
  ultimately have \<sigma>_ineqs_neq: "\<And>X t t' \<delta>. \<nexists>X\<langle>t \<doteq> t'\<rangle> \<in> set S \<Longrightarrow> ?P \<delta> X \<Longrightarrow> t \<cdot> \<delta> \<cdot> \<sigma> \<noteq> t' \<cdot> \<delta> \<cdot> \<sigma>"
    using \<I>'(1,2) sat_ineq_inj_const_subst[OF \<open>inj \<sigma>\<close> \<open>\<forall>t \<in> img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>. \<exists>c. t = Fun c []\<close>]
    by meson

  from \<sigma>_ineqs_FV_dom have \<sigma>_ineqs_FV_dom':
      "\<And>X t t' \<delta>. \<nexists>X\<langle>t \<doteq> t'\<rangle> \<in> set S \<Longrightarrow> ?P \<delta> X \<Longrightarrow> FV (t \<cdot> \<delta>) \<union> FV (t' \<cdot> \<delta>) \<subseteq> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>"
    by (simp add: Un_Diff subst_FV_unfold_ground_img)
  hence \<sigma>_ineqs_ground:
      "\<And>X t t' \<delta>. \<nexists>X\<langle>t \<doteq> t'\<rangle> \<in> set S \<Longrightarrow> ?P \<delta> X \<Longrightarrow> FV (t \<cdot> \<delta> \<cdot> \<sigma>) = {}"
      "\<And>X t t' \<delta>. \<nexists>X\<langle>t \<doteq> t'\<rangle> \<in> set S \<Longrightarrow> ?P \<delta> X \<Longrightarrow> FV (t' \<cdot> \<delta> \<cdot> \<sigma>) = {}"
    using subst_FV_dom_ground_if_ground_img \<sigma>_img_ground
    by (metis Un_subset_iff)+
 
  from \<sigma>_pgwt_img \<sigma>_ineqs_neq have \<sigma>_deduct: "\<And>x M. x \<in> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma> \<Longrightarrow> M \<turnstile>\<^sub>c \<sigma> x"
    using pgwt_deducible by fastforce

  { fix M::"('fun,'var) terms"
    have "\<lbrakk>M; S\<rbrakk>\<^sub>c (\<theta> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<I>)" using \<open>wf\<^sub>s\<^sub>t {} S\<close> \<open>simple S\<close> S_\<theta>_disj \<sigma>_ineqs_neq \<sigma>_ineqs_FV_dom'
    proof (induction S arbitrary: M rule: wf\<^sub>s\<^sub>t_simple_induct)
      case (ConsSnd v S)
      hence S_sat: "\<lbrakk>M; S\<rbrakk>\<^sub>c (\<theta> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<I>)" and "\<theta> v = Var v" by auto
      have "\<And>M. M \<turnstile>\<^sub>c Var v \<cdot> (\<theta> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<I>)"
      proof (cases "\<sigma> v = Var v")
        case True thus "\<And>M. M \<turnstile>\<^sub>c Var v \<cdot> (\<theta> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<I>)" using \<I>_deduct \<open>\<theta> v = Var v\<close> by auto
      next
        case False
        hence "v \<in> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>" "Var v \<cdot> (\<theta> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<I>) = \<sigma> v"
          using \<sigma>_pgwt_img \<open>\<theta> v = Var v\<close> pgwt_ground by auto
        thus "\<And>M. M \<turnstile>\<^sub>c Var v \<cdot> (\<theta> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<I>)" by (metis \<sigma>_deduct)
      qed
      thus ?case using strand_sem_append[OF S_sat] by (metis strand_sem_c.simps(1,2))
    next
      case (ConsIneq X t t' S)
      from ConsIneq.prems(1) have "t \<cdot> \<theta> = t" "t' \<cdot> \<theta> = t'" by auto
      hence *: "\<And>\<delta>. ?P \<delta> X \<Longrightarrow> t \<cdot> \<delta> \<cdot> \<theta> = t \<cdot> \<delta>" "\<And>\<delta>. ?P \<delta> X \<Longrightarrow> t' \<cdot> \<delta> \<cdot> \<theta> = t' \<cdot> \<delta>"
        by (metis ground_subst_FV_subset subst_apply_term_empty vars_term_subset_subst_eq)+
      from ConsIneq have "\<And>\<delta>. ?P \<delta> X \<Longrightarrow> t \<cdot> \<delta> \<cdot> \<sigma> \<noteq> t' \<cdot> \<delta> \<cdot> \<sigma>"
          and IH: "\<lbrakk>M; S\<rbrakk>\<^sub>c (\<theta> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<I>)"
        by (meson in_set_conv_decomp, fastforce)
      moreover have "\<And>\<delta>. ?P \<delta> X \<Longrightarrow> FV (t \<cdot> \<delta> \<cdot> \<sigma>) = {}" "\<And>\<delta>. ?P \<delta> X \<Longrightarrow> FV (t' \<cdot> \<delta> \<cdot> \<sigma>) = {}"
        using ConsIneq.prems(3)[of X t t'] subst_FV_dom_ground_if_ground_img[OF _ \<sigma>_img_ground]
        by auto
      ultimately have "\<And>\<delta>. ?P \<delta> X \<Longrightarrow> t \<cdot> \<delta> \<cdot> \<sigma> \<cdot> \<I> \<noteq> t' \<cdot> \<delta> \<cdot> \<sigma> \<cdot> \<I>"
        by (simp add: subst_ground_ident)
      hence "\<And>\<delta>. ?P \<delta> X \<Longrightarrow> t \<cdot> \<delta> \<cdot> (\<theta> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<I>) \<noteq> t' \<cdot> \<delta> \<cdot> (\<theta> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<I>)"
        using * by simp
      thus ?case using IH by auto
    qed auto
  }
  moreover have "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t (\<theta> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<I>)"
    by (metis wt_subst_compose \<open>wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>\<close> \<open>wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<sigma>\<close> \<open>wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>\<close>)
  moreover have "\<forall>x. wf\<^sub>t\<^sub>r\<^sub>m ((\<theta> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<I>) x)"
    using assms(4) \<I>_wf_trm \<sigma>_wf_trm by (simp add: subst_compose_def wf_trm_subst)
  ultimately show ?thesis
    using interpretation_comp(1)[OF \<open>interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>\<close>, of "\<theta> \<circ>\<^sub>s \<sigma>"]
          Idem_support[OF \<open>Idem \<theta>\<close>, of "\<sigma> \<circ>\<^sub>s \<I>"] comp_assoc
    unfolding constr_sem_c_def by metis
qed


subsection {* The typing result *}
theorem wt_attack_if_tfr_attack:
  assumes "interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>" "\<I> \<Turnstile>\<^sub>c \<langle>S, \<theta>\<rangle>" "wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S \<theta>"
  and "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>" "tfr\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S)" "eqs_tfr\<^sub>s\<^sub>t S"
  and "\<forall>v. wf\<^sub>t\<^sub>r\<^sub>m (\<theta> v)"
  shows "\<exists>\<I>\<^sub>\<tau>. interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>\<^sub>\<tau> \<and> \<I>\<^sub>\<tau> \<Turnstile>\<^sub>c \<langle>S, \<theta>\<rangle> \<and> wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>\<^sub>\<tau> \<and> (\<forall>x. wf\<^sub>t\<^sub>r\<^sub>m (\<I>\<^sub>\<tau> x))"
proof -
  obtain S' \<theta>' where *: "simple S'" "(S,\<theta>) \<leadsto>\<^sup>* (S',\<theta>')" "\<lbrakk>{}; S'\<rbrakk>\<^sub>c \<I>"
    using LI_completeness[OF assms(3,2)] unfolding constr_sem_c_def
    by (meson in_subterms_refl)
  have **: "wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S' \<theta>'" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>'" "eqs_tfr\<^sub>s\<^sub>t S'" "\<forall>v. wf\<^sub>t\<^sub>r\<^sub>m (\<theta>' v)"
    using LI_preserves_welltypedness[OF *(2) assms(3,4,7)] assms(5,6)
          LI_preserves_wellformedness[OF *(2) assms(3)]
          LI_preserves_tfr[OF *(2) assms(3,4,7,5,6)]
    apply (blast,blast,blast)
    by (metis LI_preserves_welltypedness[OF *(2) assms(3,4,7)] assms(5,6))

  def A \<equiv> "{x \<in> vars\<^sub>s\<^sub>t S'. \<exists>X t t'. \<nexists>X\<langle>t \<doteq> t'\<rangle> \<in> set S' \<and> x \<in> FV t \<union> FV t' \<and> x \<notin> set X}"
  def B \<equiv> "UNIV - A"

  let ?\<I> = "rm_vars B \<I>"

  have gr\<I>: "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>)" "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\<I>)"
    using assms(1) rm_vars_img_subset[of B \<I>] by auto

  { fix X t t' and \<delta>::"('fun,'var) subst"
    assume "\<nexists>X\<langle>t \<doteq> t'\<rangle> \<in> set S'" "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> = set X" "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>)"
    hence "t \<cdot> \<delta> \<cdot> \<I> \<noteq> t' \<cdot> \<delta> \<cdot> \<I>" using strand_sem_c_imp_ineqs_neq[OF *(3)] by auto
    hence "t \<cdot> \<delta> \<cdot> ?\<I> \<noteq> t' \<cdot> \<delta> \<cdot> ?\<I>"
      using Unifier_ground_rm_vars[OF gr\<I>(1), of "t \<cdot> \<delta>" B "t' \<cdot> \<delta>"]
      by auto
  } moreover have "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I> = UNIV" using assms(1) by metis
  hence "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\<I> = A" using rm_vars_dom[of B \<I>] B_def by blast
  ultimately obtain \<I>\<^sub>\<tau> where "interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>\<^sub>\<tau>" "\<I>\<^sub>\<tau> \<Turnstile>\<^sub>c \<langle>S', \<theta>'\<rangle>" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>\<^sub>\<tau>" "\<forall>x. wf\<^sub>t\<^sub>r\<^sub>m (\<I>\<^sub>\<tau> x)"
    using wt_sat_if_simple[OF *(1) **(1,2,4) _ gr\<I>(2) _ **(3)] A_def by moura
  thus ?thesis using LI_soundness[OF assms(3) *(2)] by metis
qed

corollary secure_if_wt_secure:
  assumes "\<not>(\<exists>\<I>\<^sub>\<tau>. interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>\<^sub>\<tau> \<and> \<I>\<^sub>\<tau> \<Turnstile>\<^sub>c \<langle>S, \<theta>\<rangle> \<and> wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>\<^sub>\<tau>)"
  and     "wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S \<theta>" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>" "tfr\<^sub>s\<^sub>t (trms\<^sub>s\<^sub>t S)" "eqs_tfr\<^sub>s\<^sub>t S"
  and     "\<forall>v. wf\<^sub>t\<^sub>r\<^sub>m (\<theta> v)"
  shows "\<not>(\<exists>\<I>. interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I> \<and> \<I> \<Turnstile>\<^sub>c \<langle>S, \<theta>\<rangle>)"
using wt_attack_if_tfr_attack[OF _ _ assms(2,3,4,5)] assms(1,6) by blast

end

end