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

section {* Theory: Definitions and Theorems Related to Strands and Intruder Constraints *}
theory StrandsAndConstraints
imports Messages Unification2 IntruderDeduction
begin

subsection {* Constraints, Intruder Strands and Related Definitions *}
datatype (funs\<^sub>s\<^sub>t\<^sub>p: 'a, (* vars\<^sub>s\<^sub>t\<^sub>p: *) 'b) strand_step =
  Send       (trm\<^sub>s\<^sub>t\<^sub>p: "('a,'b) term") ("snd\<langle>_\<rangle>" 80)
| Receive    (trm\<^sub>s\<^sub>t\<^sub>p: "('a,'b) term") ("rcv\<langle>_\<rangle>" 80)
| Equality   (trm\<^sub>s\<^sub>t\<^sub>p: "('a,'b) term") (trm_r\<^sub>s\<^sub>t\<^sub>p: "('a,'b) term") ("_ \<doteq> _" [80,80])
| Inequality (bvars\<^sub>s\<^sub>t\<^sub>p: "'b list") (trm\<^sub>s\<^sub>t\<^sub>p: "('a,'b) term") (trm_r\<^sub>s\<^sub>t\<^sub>p: "('a,'b) term") ("\<nexists>_\<langle>_ \<doteq> _\<rangle>" [80,80])
where
  "trm_r\<^sub>s\<^sub>t\<^sub>p (Send t) = t"
| "trm_r\<^sub>s\<^sub>t\<^sub>p (Receive t) = t"
| "bvars\<^sub>s\<^sub>t\<^sub>p (Send _) = []"
| "bvars\<^sub>s\<^sub>t\<^sub>p (Receive _) = []"
| "bvars\<^sub>s\<^sub>t\<^sub>p (Equality _ _) = []"

definition vars\<^sub>s\<^sub>t\<^sub>p where "vars\<^sub>s\<^sub>t\<^sub>p x \<equiv> FV (trm\<^sub>s\<^sub>t\<^sub>p x) \<union> FV (trm_r\<^sub>s\<^sub>t\<^sub>p x) \<union> set (bvars\<^sub>s\<^sub>t\<^sub>p x)"
declare vars\<^sub>s\<^sub>t\<^sub>p_def[simp]

definition trms\<^sub>s\<^sub>t where "trms\<^sub>s\<^sub>t S \<equiv> trm\<^sub>s\<^sub>t\<^sub>p ` set S \<union> trm_r\<^sub>s\<^sub>t\<^sub>p ` set S"
declare trms\<^sub>s\<^sub>t_def[simp]

type_synonym ('a,'b) strand = "('a,'b) strand_step list"
type_synonym ('a,'b) strands = "('a,'b) strand set"

abbreviation strand_step_prepend (infixr ":" 65) where "(b::('f,'v) strand_step):A \<equiv> b#A"
abbreviation strand_step_append (infixr ":" 65) where "A:(b::('f,'v) strand_step) \<equiv> A@[b]"
abbreviation strand_append (infixr ":" 65) where "(A::('f,'v) strand):B \<equiv> A@B"

definition FV\<^sub>s\<^sub>n\<^sub>d::"('a,'b) strand_step \<Rightarrow> 'b set" where
  "FV\<^sub>s\<^sub>n\<^sub>d x \<equiv> case x of snd\<langle>t\<rangle> \<Rightarrow> FV t | _ \<Rightarrow> {}"

definition FV\<^sub>r\<^sub>c\<^sub>v::"('a,'b) strand_step \<Rightarrow> 'b set" where
  "FV\<^sub>r\<^sub>c\<^sub>v x \<equiv> case x of rcv\<langle>t\<rangle> \<Rightarrow> FV t | _ \<Rightarrow> {}"

definition FV\<^sub>e\<^sub>q::"('a,'b) strand_step \<Rightarrow> 'b set" where
  "FV\<^sub>e\<^sub>q x \<equiv> case x of (s \<doteq> t) \<Rightarrow> FV s \<union> FV t | _ \<Rightarrow> {}"

definition FV_r\<^sub>e\<^sub>q::"('a,'b) strand_step \<Rightarrow> 'b set" where
  "FV_r\<^sub>e\<^sub>q x \<equiv> case x of (s \<doteq> t) \<Rightarrow> FV t | _ \<Rightarrow> {}"

definition FV\<^sub>i\<^sub>n\<^sub>e\<^sub>q::"('a,'b) strand_step \<Rightarrow> 'b set" where
  "FV\<^sub>i\<^sub>n\<^sub>e\<^sub>q x \<equiv> case x of (\<nexists>X\<langle>s \<doteq> t\<rangle>) \<Rightarrow> (FV s \<union> FV t) - set X | _ \<Rightarrow> {}"

fun FV\<^sub>s\<^sub>t\<^sub>p::"('a,'b) strand_step \<Rightarrow> 'b set" where
  "FV\<^sub>s\<^sub>t\<^sub>p (Send t) = FV t"
| "FV\<^sub>s\<^sub>t\<^sub>p (Receive t) = FV t"
| "FV\<^sub>s\<^sub>t\<^sub>p (Equality t t') = FV t \<union> FV t'"
| "FV\<^sub>s\<^sub>t\<^sub>p (Inequality X t t') = FV t \<union> FV t' - set X"

definition FV\<^sub>s\<^sub>t::"('a,'b) strand \<Rightarrow> 'b set" where
  "FV\<^sub>s\<^sub>t S \<equiv> \<Union>(set (map FV\<^sub>s\<^sub>t\<^sub>p S))"

definition vars\<^sub>s\<^sub>t::"('a,'b) strand \<Rightarrow> 'b set" where
  "vars\<^sub>s\<^sub>t S \<equiv> \<Union>(set (map vars\<^sub>s\<^sub>t\<^sub>p S))"

definition bvars\<^sub>s\<^sub>t::"('a,'b) strand \<Rightarrow> 'b set" where
  "bvars\<^sub>s\<^sub>t S \<equiv> \<Union>(set (map (set \<circ> bvars\<^sub>s\<^sub>t\<^sub>p) S))"

fun vars2\<^sub>s\<^sub>t::"('a,'b) strand \<Rightarrow> 'b set" where
  "vars2\<^sub>s\<^sub>t [] = {}"
| "vars2\<^sub>s\<^sub>t (Inequality _ t t'#S) = vars2\<^sub>s\<^sub>t S"
| "vars2\<^sub>s\<^sub>t (x#S) = vars\<^sub>s\<^sub>t\<^sub>p x \<union> vars2\<^sub>s\<^sub>t S"

definition wfvarsoccs\<^sub>s\<^sub>t\<^sub>p where
  "wfvarsoccs\<^sub>s\<^sub>t\<^sub>p x \<equiv> case x of snd\<langle>t\<rangle> \<Rightarrow> FV t | s \<doteq> t \<Rightarrow> FV s | _ \<Rightarrow> {}"

definition wfvarsoccs\<^sub>s\<^sub>t where
  "wfvarsoccs\<^sub>s\<^sub>t S \<equiv> \<Union>set (map wfvarsoccs\<^sub>s\<^sub>t\<^sub>p S)"

definition funs\<^sub>s\<^sub>t::"('a,'b) strand \<Rightarrow> 'a set" where
  "funs\<^sub>s\<^sub>t S \<equiv> \<Union>(set (map funs\<^sub>s\<^sub>t\<^sub>p S))"

fun eqs_rhs\<^sub>s\<^sub>t where
  "eqs_rhs\<^sub>s\<^sub>t [] = {}"
| "eqs_rhs\<^sub>s\<^sub>t (Equality t t'#S) = insert t' (eqs_rhs\<^sub>s\<^sub>t S)"
| "eqs_rhs\<^sub>s\<^sub>t (x#S) = eqs_rhs\<^sub>s\<^sub>t S"

definition subst_apply_strand_step::"('a,'b) strand_step \<Rightarrow> ('a,'b) subst \<Rightarrow> ('a,'b) strand_step"
  (infix "\<cdot>\<^sub>s\<^sub>t\<^sub>p" 51) where
  "s \<cdot>\<^sub>s\<^sub>t\<^sub>p \<theta> \<equiv> (case s of
    snd\<langle>t\<rangle> \<Rightarrow> snd\<langle>t \<cdot> \<theta>\<rangle>
  | rcv\<langle>t\<rangle> \<Rightarrow> rcv\<langle>t \<cdot> \<theta>\<rangle>
  | t \<doteq> t' \<Rightarrow> (t \<cdot> \<theta>) \<doteq> (t' \<cdot> \<theta>)
  | \<nexists>X\<langle>t \<doteq> t'\<rangle> \<Rightarrow> \<nexists>X\<langle>(t \<cdot> (rm_vars (set X) \<theta>)) \<doteq> (t' \<cdot> (rm_vars (set X) \<theta>))\<rangle>)"

definition subst_apply_strand::"('a,'b) strand \<Rightarrow> ('a,'b) subst \<Rightarrow> ('a,'b) strand"
  (infix "\<cdot>\<^sub>s\<^sub>t" 51) where
  "S \<cdot>\<^sub>s\<^sub>t \<theta> \<equiv> map (\<lambda>x. x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<theta>) S"

fun simple::"('a,'b) strand \<Rightarrow> bool" where
  "simple [] = True"
| "simple (rcv\<langle>t\<rangle>#S) = simple S"
| "simple (snd\<langle>Var v\<rangle>#S) = simple S"
| "simple (\<nexists>_\<langle>s \<doteq> t\<rangle>#S) = simple S"
| "simple (_#S) = False"

fun ik\<^sub>s\<^sub>t::"('a,'b) strand \<Rightarrow> ('a,'b) terms" where
  "ik\<^sub>s\<^sub>t [] = {}"
| "ik\<^sub>s\<^sub>t (rcv\<langle>t\<rangle>#S) = insert t (ik\<^sub>s\<^sub>t S)"
| "ik\<^sub>s\<^sub>t (_#S) = ik\<^sub>s\<^sub>t S"

fun wf\<^sub>s\<^sub>t::"'b set \<Rightarrow> ('a,'b) strand \<Rightarrow> bool" where
  "wf\<^sub>s\<^sub>t V [] = True"
| "wf\<^sub>s\<^sub>t V (rcv\<langle>t\<rangle>#S) = (FV t \<subseteq> V \<and> wf\<^sub>s\<^sub>t V S)"
| "wf\<^sub>s\<^sub>t V (snd\<langle>t\<rangle>#S) = wf\<^sub>s\<^sub>t (V \<union> FV t) S"
| "wf\<^sub>s\<^sub>t V (s \<doteq> t#S) = (FV t \<subseteq> V \<and> wf\<^sub>s\<^sub>t (V \<union> FV s) S)"
| "wf\<^sub>s\<^sub>t V (\<nexists>_\<langle>s \<doteq> t\<rangle>#S) = wf\<^sub>s\<^sub>t V S"

definition wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r::"('a,'b) strand \<Rightarrow> ('a,'b) subst \<Rightarrow> bool" where
  "wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S \<theta> \<equiv> (wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<and> wf\<^sub>s\<^sub>t {} S \<and> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<inter> vars\<^sub>s\<^sub>t S = {}
                  \<and> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<inter> bvars\<^sub>s\<^sub>t S = {} \<and> FV\<^sub>s\<^sub>t S \<inter> bvars\<^sub>s\<^sub>t S = {})"

declare FV\<^sub>s\<^sub>n\<^sub>d_def[simp]
declare FV\<^sub>r\<^sub>c\<^sub>v_def[simp]
declare FV\<^sub>e\<^sub>q_def[simp]
declare FV_r\<^sub>e\<^sub>q_def[simp]
declare FV\<^sub>i\<^sub>n\<^sub>e\<^sub>q_def[simp]
declare FV\<^sub>s\<^sub>t_def[simp]
declare vars\<^sub>s\<^sub>t_def[simp]
declare bvars\<^sub>s\<^sub>t_def[simp]
declare wfvarsoccs\<^sub>s\<^sub>t\<^sub>p_def[simp]
declare wfvarsoccs\<^sub>s\<^sub>t_def[simp]
declare subst_apply_strand_step_def[simp]
declare subst_apply_strand_def[simp]
declare wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r_def[simp]

lemmas wf\<^sub>s\<^sub>t_induct = wf\<^sub>s\<^sub>t.induct[case_names Nil ConsRcv ConsSnd ConsEq ConsIneq]
lemmas ik\<^sub>s\<^sub>t_induct = ik\<^sub>s\<^sub>t.induct[case_names Nil ConsRcv ConsSnd ConsEq ConsIneq]
lemmas vars2\<^sub>s\<^sub>t_induct = vars2\<^sub>s\<^sub>t.induct[case_names Nil ConsIneq ConsSnd ConsRcv ConsEq]
lemmas eqs_rhs\<^sub>s\<^sub>t_induct = eqs_rhs\<^sub>s\<^sub>t.induct[case_names Nil ConsEq ConsSnd ConsRcv ConsIneq]
  

subsubsection {* Lexicographical measure on strands *}
definition size\<^sub>s\<^sub>t::"('a,'b) strand \<Rightarrow> nat" where
  "size\<^sub>s\<^sub>t S \<equiv> size_list (\<lambda>x. size (trm\<^sub>s\<^sub>t\<^sub>p x)) S"

definition measure\<^sub>s\<^sub>t::"((('a, 'b) strand \<times> ('a,'b) subst) \<times> ('a, 'b) strand \<times> ('a,'b) subst) set"
where
  "measure\<^sub>s\<^sub>t \<equiv> measures [\<lambda>(S,\<theta>). card (FV\<^sub>s\<^sub>t S), \<lambda>(S,\<theta>). size\<^sub>s\<^sub>t S]"

declare size\<^sub>s\<^sub>t_def[simp]
declare measure\<^sub>s\<^sub>t_def[simp]

lemma measure\<^sub>s\<^sub>t_alt_def:
  "((s,x),(t,y)) \<in> measure\<^sub>s\<^sub>t =
      (card (FV\<^sub>s\<^sub>t s) < card (FV\<^sub>s\<^sub>t t) \<or> (card (FV\<^sub>s\<^sub>t s) = card (FV\<^sub>s\<^sub>t t) \<and> size\<^sub>s\<^sub>t s < size\<^sub>s\<^sub>t t))"
by simp 

lemma measure\<^sub>s\<^sub>t_trans: "trans measure\<^sub>s\<^sub>t" unfolding trans_def by auto


subsubsection {* Some lemmas *}
lemma trms\<^sub>s\<^sub>t_append: "trms\<^sub>s\<^sub>t (A@B) = trms\<^sub>s\<^sub>t A \<union> trms\<^sub>s\<^sub>t B"
by auto

lemma finite_ik\<^sub>s\<^sub>t[simp]: "finite (ik\<^sub>s\<^sub>t S)"
by (induct S rule: ik\<^sub>s\<^sub>t.induct) simp_all

lemma finite_eqs_rhs\<^sub>s\<^sub>t[simp]: "finite (eqs_rhs\<^sub>s\<^sub>t S)"
by (induct S rule: eqs_rhs\<^sub>s\<^sub>t.induct) simp_all

lemma ik\<^sub>s\<^sub>tD[dest]: "t \<in> ik\<^sub>s\<^sub>t S \<Longrightarrow> rcv\<langle>t\<rangle> \<in> set S"
by (induct S rule: ik\<^sub>s\<^sub>t.induct) auto

lemma ik\<^sub>s\<^sub>tD'[dest]: "t \<in> ik\<^sub>s\<^sub>t S \<Longrightarrow> t \<in> trm\<^sub>s\<^sub>t\<^sub>p ` set S"
by (induct S rule: ik\<^sub>s\<^sub>t.induct) auto

lemma ik\<^sub>s\<^sub>tD''[dest]: "t \<in> \<Union>(subterms ` ik\<^sub>s\<^sub>t S) \<Longrightarrow> t \<in> \<Union>(subterms ` (trm\<^sub>s\<^sub>t\<^sub>p ` set S))"
by (induct S rule: ik\<^sub>s\<^sub>t.induct) auto

lemma ik\<^sub>s\<^sub>tD'''[dest]: "t \<in> \<Union>(subterms ` ik\<^sub>s\<^sub>t S) \<Longrightarrow> t \<in> \<Union>(subterms ` (trms\<^sub>s\<^sub>t S))"
by (induct S rule: ik\<^sub>s\<^sub>t.induct) auto

lemma eqs_rhs\<^sub>s\<^sub>tD[dest]: "t \<in> eqs_rhs\<^sub>s\<^sub>t S \<Longrightarrow> \<exists>t'. t' \<doteq> t \<in> set S"
by (induct S rule: eqs_rhs\<^sub>s\<^sub>t.induct) auto

lemma eqs_rhs\<^sub>s\<^sub>tD'[dest]: "t \<in> eqs_rhs\<^sub>s\<^sub>t S \<Longrightarrow> t \<in> trm_r\<^sub>s\<^sub>t\<^sub>p ` set S"
by (induct S rule: eqs_rhs\<^sub>s\<^sub>t.induct) auto

lemma eqs_rhs\<^sub>s\<^sub>tD''[dest]: "t \<in> \<Union>(subterms ` eqs_rhs\<^sub>s\<^sub>t S) \<Longrightarrow> t \<in> \<Union>(subterms ` (trm_r\<^sub>s\<^sub>t\<^sub>p ` set S))"
by (induct S rule: eqs_rhs\<^sub>s\<^sub>t.induct) auto

lemma eqs_rhs\<^sub>s\<^sub>tD'''[dest]: "t \<in> \<Union>(subterms ` eqs_rhs\<^sub>s\<^sub>t S) \<Longrightarrow> t \<in> \<Union>(subterms ` (trms\<^sub>s\<^sub>t S))"
by (induct S rule: eqs_rhs\<^sub>s\<^sub>t.induct) auto

lemma bvars\<^sub>s\<^sub>t_split: "bvars\<^sub>s\<^sub>t (S@S') = bvars\<^sub>s\<^sub>t S \<union> bvars\<^sub>s\<^sub>t S'"
unfolding bvars\<^sub>s\<^sub>t_def by auto

lemma bvars\<^sub>s\<^sub>t_singleton: "bvars\<^sub>s\<^sub>t [x] = set (bvars\<^sub>s\<^sub>t\<^sub>p x)"
unfolding bvars\<^sub>s\<^sub>t_def by auto

lemma strand_subst_hom[iff]:
  "(S@S') \<cdot>\<^sub>s\<^sub>t \<theta> = (S \<cdot>\<^sub>s\<^sub>t \<theta>)@(S' \<cdot>\<^sub>s\<^sub>t \<theta>)" "(x#S) \<cdot>\<^sub>s\<^sub>t \<theta> = (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<theta>)#(S \<cdot>\<^sub>s\<^sub>t \<theta>)"
unfolding subst_apply_strand_def by auto

lemma strand_subst_comp: "FV\<^sub>s\<^sub>e\<^sub>t (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>) \<inter> bvars\<^sub>s\<^sub>t S = {} \<Longrightarrow> S \<cdot>\<^sub>s\<^sub>t \<delta> \<circ>\<^sub>s \<theta> = ((S \<cdot>\<^sub>s\<^sub>t \<delta>) \<cdot>\<^sub>s\<^sub>t \<theta>)"
proof (induction S)
  case (Cons x S)
  hence *: "FV\<^sub>s\<^sub>e\<^sub>t (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>) \<inter> bvars\<^sub>s\<^sub>t S = {}" "FV\<^sub>s\<^sub>e\<^sub>t (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>) \<inter> (set (bvars\<^sub>s\<^sub>t\<^sub>p x)) = {}"
    using bvars\<^sub>s\<^sub>t_split[of "[x]" S] bvars\<^sub>s\<^sub>t_def[of "[x]"] by auto
  hence IH: "S \<cdot>\<^sub>s\<^sub>t \<delta> \<circ>\<^sub>s \<theta> = (S \<cdot>\<^sub>s\<^sub>t \<delta>) \<cdot>\<^sub>s\<^sub>t \<theta>" using Cons.IH by auto
  have "(x#S \<cdot>\<^sub>s\<^sub>t \<delta> \<circ>\<^sub>s \<theta>) = (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta> \<circ>\<^sub>s \<theta>)#(S \<cdot>\<^sub>s\<^sub>t \<delta> \<circ>\<^sub>s \<theta>)" by (metis strand_subst_hom(2))
  hence "... = (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta> \<circ>\<^sub>s \<theta>)#((S \<cdot>\<^sub>s\<^sub>t \<delta>) \<cdot>\<^sub>s\<^sub>t \<theta>)" by (metis IH)
  hence "... = ((x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) \<cdot>\<^sub>s\<^sub>t\<^sub>p \<theta>)#((S \<cdot>\<^sub>s\<^sub>t \<delta>) \<cdot>\<^sub>s\<^sub>t \<theta>)"
    using rm_vars_comp[OF *(2)] by (cases x) simp_all
  thus ?case using IH by auto
qed simp

lemma strand_substI[intro]:
  "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<inter> FV\<^sub>s\<^sub>t S = {} \<Longrightarrow> S \<cdot>\<^sub>s\<^sub>t \<theta> = S"
  "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<inter> vars\<^sub>s\<^sub>t S = {} \<Longrightarrow> S \<cdot>\<^sub>s\<^sub>t \<theta> = S"
proof -
  show "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<inter> vars\<^sub>s\<^sub>t S = {} \<Longrightarrow> S \<cdot>\<^sub>s\<^sub>t \<theta> = S"
  proof (induction S)
    case (Cons x S)
    hence "S \<cdot>\<^sub>s\<^sub>t \<theta> = S" by auto
    moreover have "vars\<^sub>s\<^sub>t\<^sub>p x \<inter> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> = {}" using Cons.prems by auto
    hence "x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<theta> = x" using rm_vars_subst_apply_ident by (cases x) fastforce+
    ultimately show ?case by simp
  qed simp

  show "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<inter> FV\<^sub>s\<^sub>t S = {} \<Longrightarrow> S \<cdot>\<^sub>s\<^sub>t \<theta> = S"
  proof (induction S)
    case (Cons x S)
    hence "S \<cdot>\<^sub>s\<^sub>t \<theta> = S" by auto
    moreover have "FV\<^sub>s\<^sub>t\<^sub>p x \<inter> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> = {}" using Cons.prems by auto
    hence "x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<theta> = x" using rm_vars_subst_apply_ident by (cases x) fastforce+
    ultimately show ?case by simp
  qed simp
qed

lemma strand_substI':
  "FV\<^sub>s\<^sub>t S = {} \<Longrightarrow> S \<cdot>\<^sub>s\<^sub>t \<theta> = S"
  "vars\<^sub>s\<^sub>t S = {} \<Longrightarrow> S \<cdot>\<^sub>s\<^sub>t \<theta> = S"
by (metis inf_bot_right strand_substI)+

lemma ik_union_subset: "\<Union>(P ` ik\<^sub>s\<^sub>t S) \<subseteq> (\<Union>x \<in> (set S). P (trm\<^sub>s\<^sub>t\<^sub>p x))"
by (induct S rule: ik\<^sub>s\<^sub>t.induct) auto

lemma ik_snd_empty[simp]: "ik\<^sub>s\<^sub>t (map Send X) = {}"
by (induct "map Send X" arbitrary: X rule: ik\<^sub>s\<^sub>t.induct) auto

lemma ik_snd_empty'[simp]: "ik\<^sub>s\<^sub>t [snd\<langle>t\<rangle>] = {}" by simp

lemma ik_append[iff]: "ik\<^sub>s\<^sub>t (S@S') = ik\<^sub>s\<^sub>t S \<union> ik\<^sub>s\<^sub>t S'" by (induct S rule: ik\<^sub>s\<^sub>t.induct) auto

lemma ik_cons: "ik\<^sub>s\<^sub>t (x#S) = ik\<^sub>s\<^sub>t [x] \<union> ik\<^sub>s\<^sub>t S" using ik_append[of "[x]" S] by simp

lemma eqs_rhs_append[iff]: "eqs_rhs\<^sub>s\<^sub>t (S@S') = eqs_rhs\<^sub>s\<^sub>t S \<union> eqs_rhs\<^sub>s\<^sub>t S'"
by (induct S rule: eqs_rhs\<^sub>s\<^sub>t.induct) auto

lemma eqs_rcv_map_empty: "eqs_rhs\<^sub>s\<^sub>t (map Receive M) = {}"
by auto

lemma ik_rcv_map: assumes "t \<in> set L" shows "t \<in> ik\<^sub>s\<^sub>t (map Receive L)"
proof -
  { fix L L' 
    have "t \<in> ik\<^sub>s\<^sub>t [rcv\<langle>t\<rangle>]" by auto
    hence "t \<in> ik\<^sub>s\<^sub>t (map Receive L@rcv\<langle>t\<rangle>#map Receive L')" using ik_append by auto
    hence "t \<in> ik\<^sub>s\<^sub>t (map Receive (L@t#L'))" by auto
  }
  thus ?thesis using assms split_list_last by force 
qed

lemma ik_subst: "ik\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>t \<delta>) = ik\<^sub>s\<^sub>t S \<cdot>set \<delta>"
by (induct rule: ik\<^sub>s\<^sub>t_induct) auto

lemma ik_rcv_map': assumes "t \<in> ik\<^sub>s\<^sub>t (map Receive L)" shows "t \<in> set L"
using assms by force

lemma (in intruder_model) ik_trp_union_is_subterm_subset:
  "trp\<^sub>s\<^sub>e\<^sub>t (ik\<^sub>s\<^sub>t S) \<subseteq> (\<Union>x \<in> (set S). subterms (trm\<^sub>s\<^sub>t\<^sub>p x))"
by (induct S rule: ik\<^sub>s\<^sub>t.induct, auto dest: trpD)

lemma (in intruder_model) trp_ik_union_append_subset[simp]:
  "trp\<^sub>s\<^sub>e\<^sub>t (ik\<^sub>s\<^sub>t S) \<subseteq> trp\<^sub>s\<^sub>e\<^sub>t (ik\<^sub>s\<^sub>t (S@S'))"
  "trp\<^sub>s\<^sub>e\<^sub>t (ik\<^sub>s\<^sub>t S) \<subseteq> trp\<^sub>s\<^sub>e\<^sub>t (ik\<^sub>s\<^sub>t (S'@S))"
by simp_all

lemma ik_append_subset[simp]: "ik\<^sub>s\<^sub>t S \<subseteq> ik\<^sub>s\<^sub>t (S@S')" "ik\<^sub>s\<^sub>t S' \<subseteq> ik\<^sub>s\<^sub>t (S@S')"
by (induct S rule: ik\<^sub>s\<^sub>t.induct) auto

lemma eqs_rhs_append_subset[simp]: "eqs_rhs\<^sub>s\<^sub>t S \<subseteq> eqs_rhs\<^sub>s\<^sub>t (S@S')" "eqs_rhs\<^sub>s\<^sub>t S' \<subseteq> eqs_rhs\<^sub>s\<^sub>t (S@S')"
by (induct S rule: eqs_rhs\<^sub>s\<^sub>t.induct) auto

lemma (in intruder_model) trp_ik_union_append_split:
  "trp\<^sub>s\<^sub>e\<^sub>t (ik\<^sub>s\<^sub>t (S@S')) = (trp\<^sub>s\<^sub>e\<^sub>t (ik\<^sub>s\<^sub>t S)) \<union> (\<Union>(trp ` ik\<^sub>s\<^sub>t S'))"
by (induct S rule: ik\<^sub>s\<^sub>t.induct) auto

lemma (in intruder_model) trp_ik_union_rcv_single:
  "trp\<^sub>s\<^sub>e\<^sub>t (ik\<^sub>s\<^sub>t [rcv\<langle>t\<rangle>]) = trp t"
by auto

lemma (in intruder_model) trp_ik_subtermD:
  assumes "t \<in> trp\<^sub>s\<^sub>e\<^sub>t (ik\<^sub>s\<^sub>t S)"
  obtains x where "x \<in> set S" "t \<sqsubseteq> trm\<^sub>s\<^sub>t\<^sub>p x"
using assms ik\<^sub>s\<^sub>tD trpD by auto

lemma (in intruder_model) trp_ik_subterm_exD:
  assumes "t \<in> trp\<^sub>s\<^sub>e\<^sub>t (ik\<^sub>s\<^sub>t S)"
  shows "\<exists>x \<in> set S. t \<sqsubseteq> trm\<^sub>s\<^sub>t\<^sub>p x"
using assms ik\<^sub>s\<^sub>tD trpD by blast


subsection {* Lemmas: Free Variables of Strands *}
lemma FV_trm_snd_rcv: "FV (trm\<^sub>s\<^sub>t\<^sub>p (snd\<langle>t\<rangle>)) = FV t" "FV (trm\<^sub>s\<^sub>t\<^sub>p (rcv\<langle>t\<rangle>)) = FV t" by simp_all

lemma in_strand_FV_subset: "x \<in> set S \<Longrightarrow> vars\<^sub>s\<^sub>t\<^sub>p x \<subseteq> vars\<^sub>s\<^sub>t S" by auto
lemma in_strand_FV_subset_snd: "snd\<langle>t\<rangle> \<in> set S \<Longrightarrow> FV t \<subseteq> \<Union>set (map FV\<^sub>s\<^sub>n\<^sub>d S)" by auto
lemma in_strand_FV_subset_rcv: "rcv\<langle>t\<rangle> \<in> set S \<Longrightarrow> FV t \<subseteq> \<Union>set (map FV\<^sub>r\<^sub>c\<^sub>v S)" by auto

lemma finite_vars\<^sub>s\<^sub>t\<^sub>p[simp]: "finite (vars\<^sub>s\<^sub>t\<^sub>p x)" using finite_FV by auto
lemma finite_bvars\<^sub>s\<^sub>t\<^sub>p[simp]: "finite (set (bvars\<^sub>s\<^sub>t\<^sub>p x))" by rule
lemma finite_FV\<^sub>s\<^sub>n\<^sub>d[simp]: "finite (FV\<^sub>s\<^sub>n\<^sub>d x)" using finite_FV by (cases x) auto
lemma finite_FV\<^sub>r\<^sub>c\<^sub>v[simp]: "finite (FV\<^sub>r\<^sub>c\<^sub>v x)" using finite_FV by (cases x) auto
lemma finite_FV\<^sub>s\<^sub>t\<^sub>p[simp]: "finite (FV\<^sub>s\<^sub>t\<^sub>p x)" using finite_FV by (cases x) auto
lemma finite_vars\<^sub>s\<^sub>t[simp]: "finite (vars\<^sub>s\<^sub>t S)" by simp
lemma finite_vars2\<^sub>s\<^sub>t[simp]: "finite (vars2\<^sub>s\<^sub>t S)" by (induct S rule: vars2\<^sub>s\<^sub>t.induct) auto
lemma finite_bvars\<^sub>s\<^sub>t[simp]: "finite (bvars\<^sub>s\<^sub>t S)" by simp
lemma finite_FV\<^sub>s\<^sub>t[simp]: "finite (FV\<^sub>s\<^sub>t S)" by simp

lemma FV\<^sub>s\<^sub>n\<^sub>dE:
  assumes "v \<in> \<Union>set (map FV\<^sub>s\<^sub>n\<^sub>d S)"
  obtains t where "snd\<langle>t\<rangle> \<in> set S" "v \<in> FV t"
using assms
apply (induct S, simp_all)
by (metis empty_iff strand_step.case_eq_if strand_step.collapse(1))

lemma FV\<^sub>r\<^sub>c\<^sub>vE:
  assumes "v \<in> \<Union>set (map FV\<^sub>r\<^sub>c\<^sub>v S)"
  obtains t where "rcv\<langle>t\<rangle> \<in> set S" "v \<in> FV t"
using assms
apply (induct S, simp_all)
by (metis empty_iff strand_step.case_eq_if strand_step.collapse(2))

lemma vars\<^sub>s\<^sub>t\<^sub>pI[intro]: "x \<in> FV\<^sub>s\<^sub>t\<^sub>p s \<Longrightarrow> x \<in> vars\<^sub>s\<^sub>t\<^sub>p s"
by (induct s rule: FV\<^sub>s\<^sub>t\<^sub>p.induct) auto

lemma vars\<^sub>s\<^sub>tI[intro]: "x \<in> FV\<^sub>s\<^sub>t S \<Longrightarrow> x \<in> vars\<^sub>s\<^sub>t S" using vars\<^sub>s\<^sub>t\<^sub>pI by fastforce

lemma FV\<^sub>s\<^sub>t_subset_vars\<^sub>s\<^sub>t[simp]: "FV\<^sub>s\<^sub>t S \<subseteq> vars\<^sub>s\<^sub>t S" using vars\<^sub>s\<^sub>tI by force

lemma vars\<^sub>s\<^sub>t_is_FV\<^sub>s\<^sub>t_bvars\<^sub>s\<^sub>t: "vars\<^sub>s\<^sub>t S = FV\<^sub>s\<^sub>t S \<union> bvars\<^sub>s\<^sub>t S"
proof (induction S)
  case (Cons x S) thus ?case by (cases x) auto
qed simp

lemma vars_st_snd_map: "vars\<^sub>s\<^sub>t (map Send X) = FV (Fun f X)" by simp
lemma vars_st_rcv_map: "vars\<^sub>s\<^sub>t (map Receive X) = FV (Fun f X)" by simp

lemma vars_snd_rcv_union: "vars\<^sub>s\<^sub>t\<^sub>p x = FV\<^sub>s\<^sub>n\<^sub>d x \<union> FV\<^sub>r\<^sub>c\<^sub>v x \<union> FV\<^sub>e\<^sub>q x \<union> FV\<^sub>i\<^sub>n\<^sub>e\<^sub>q x \<union> set (bvars\<^sub>s\<^sub>t\<^sub>p x)"
by (cases x) simp_all

lemma FV_snd_rcv_union: "FV\<^sub>s\<^sub>t\<^sub>p x = FV\<^sub>s\<^sub>n\<^sub>d x \<union> FV\<^sub>r\<^sub>c\<^sub>v x \<union> FV\<^sub>e\<^sub>q x \<union> FV\<^sub>i\<^sub>n\<^sub>e\<^sub>q x"
by (cases x) simp_all

lemma FV_snd_rcv_empty[simp]: "FV\<^sub>s\<^sub>n\<^sub>d x = {} \<or> FV\<^sub>r\<^sub>c\<^sub>v x = {}" by (cases x) simp_all

lemma vars_snd_rcv_strand[iff]:
  "vars\<^sub>s\<^sub>t (S::('a,'b) strand) =
    (\<Union>set (map FV\<^sub>s\<^sub>n\<^sub>d S)) \<union> (\<Union>set (map FV\<^sub>r\<^sub>c\<^sub>v S)) \<union> (\<Union>set (map FV\<^sub>e\<^sub>q S)) \<union> (\<Union>set (map FV\<^sub>i\<^sub>n\<^sub>e\<^sub>q S))
    \<union> bvars\<^sub>s\<^sub>t S"
unfolding bvars\<^sub>s\<^sub>t_def
proof (induction S)
  case (Cons x S)
  have "\<And>s V. vars\<^sub>s\<^sub>t\<^sub>p (s::('a,'b) strand_step) \<union> V = 
                FV\<^sub>s\<^sub>n\<^sub>d s \<union> FV\<^sub>r\<^sub>c\<^sub>v s \<union> FV\<^sub>e\<^sub>q s \<union> FV\<^sub>i\<^sub>n\<^sub>e\<^sub>q s \<union> set (bvars\<^sub>s\<^sub>t\<^sub>p s) \<union> V"
    by (metis vars_snd_rcv_union)
  thus ?case using Cons.IH by (auto simp add: sup_assoc sup_left_commute)
qed simp

lemma FV_snd_rcv_strand[iff]:
  "FV\<^sub>s\<^sub>t (S::('a,'b) strand) =
    (\<Union>set (map FV\<^sub>s\<^sub>n\<^sub>d S)) \<union> (\<Union>set (map FV\<^sub>r\<^sub>c\<^sub>v S)) \<union> (\<Union>set (map FV\<^sub>e\<^sub>q S)) \<union> (\<Union>set (map FV\<^sub>i\<^sub>n\<^sub>e\<^sub>q S))"
unfolding bvars\<^sub>s\<^sub>t_def
proof (induction S)
  case (Cons x S)
  have "\<And>s V. FV\<^sub>s\<^sub>t\<^sub>p (s::('a,'b) strand_step) \<union> V = 
                FV\<^sub>s\<^sub>n\<^sub>d s \<union> FV\<^sub>r\<^sub>c\<^sub>v s \<union> FV\<^sub>e\<^sub>q s \<union> FV\<^sub>i\<^sub>n\<^sub>e\<^sub>q s \<union> V"
    by (metis FV_snd_rcv_union)
  thus ?case using Cons.IH by (auto simp add: sup_assoc sup_left_commute)
qed simp

lemma vars_snd_rcv_strand2[iff]:
  "vars2\<^sub>s\<^sub>t (S::('a,'b) strand) = (\<Union>set (map FV\<^sub>s\<^sub>n\<^sub>d S)) \<union> (\<Union>set (map FV\<^sub>r\<^sub>c\<^sub>v S)) \<union> (\<Union>set (map FV\<^sub>e\<^sub>q S))"
proof (induction S)
  case (Cons x S) thus ?case by (cases x) auto
qed simp

lemma FV_snd_rcv_strand_subset[simp]:
  "\<Union>set (map FV\<^sub>s\<^sub>n\<^sub>d S) \<subseteq> FV\<^sub>s\<^sub>t S" "\<Union>set (map FV\<^sub>r\<^sub>c\<^sub>v S) \<subseteq> FV\<^sub>s\<^sub>t S"
  "\<Union>set (map FV\<^sub>e\<^sub>q S) \<subseteq> FV\<^sub>s\<^sub>t S" "\<Union>set (map FV\<^sub>i\<^sub>n\<^sub>e\<^sub>q S) \<subseteq> FV\<^sub>s\<^sub>t S"
  "wfvarsoccs\<^sub>s\<^sub>t S \<subseteq> FV\<^sub>s\<^sub>t S"
proof -
  show "\<Union>set (map FV\<^sub>s\<^sub>n\<^sub>d S) \<subseteq> FV\<^sub>s\<^sub>t S" "\<Union>set (map FV\<^sub>r\<^sub>c\<^sub>v S) \<subseteq> FV\<^sub>s\<^sub>t S"
       "\<Union>set (map FV\<^sub>e\<^sub>q S) \<subseteq> FV\<^sub>s\<^sub>t S" "\<Union>set (map FV\<^sub>i\<^sub>n\<^sub>e\<^sub>q S) \<subseteq> FV\<^sub>s\<^sub>t S"
    using FV_snd_rcv_strand[of S] by auto
  show "wfvarsoccs\<^sub>s\<^sub>t S \<subseteq> FV\<^sub>s\<^sub>t S"
  proof (induction S)
    case (Cons x S) thus ?case by (cases x) auto
  qed simp
qed

lemma vars_snd_rcv_strand_subset2[simp]:
  "\<Union>set (map FV\<^sub>s\<^sub>n\<^sub>d S) \<subseteq> vars2\<^sub>s\<^sub>t S" "\<Union>set (map FV\<^sub>r\<^sub>c\<^sub>v S) \<subseteq> vars2\<^sub>s\<^sub>t S"
  "\<Union>set (map FV\<^sub>e\<^sub>q S) \<subseteq> vars2\<^sub>s\<^sub>t S" "wfvarsoccs\<^sub>s\<^sub>t S \<subseteq> vars2\<^sub>s\<^sub>t S"
proof -
  show "\<Union>set (map FV\<^sub>s\<^sub>n\<^sub>d S) \<subseteq> vars2\<^sub>s\<^sub>t S" "\<Union>set (map FV\<^sub>r\<^sub>c\<^sub>v S) \<subseteq> vars2\<^sub>s\<^sub>t S"
       "\<Union>set (map FV\<^sub>e\<^sub>q S) \<subseteq> vars2\<^sub>s\<^sub>t S"
    by auto
  show "wfvarsoccs\<^sub>s\<^sub>t S \<subseteq> vars2\<^sub>s\<^sub>t S"
  proof (induction S)
    case (Cons x S) thus ?case by (cases x) auto
  qed simp
qed

lemma vars2\<^sub>s\<^sub>t_subset_vars\<^sub>s\<^sub>t: "vars2\<^sub>s\<^sub>t S \<subseteq> vars\<^sub>s\<^sub>t S"
by (induct S rule: vars2\<^sub>s\<^sub>t.induct) auto

lemma subst_sends_strand_FV_to_img: "FV\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>t \<delta>) \<subseteq> FV\<^sub>s\<^sub>t S \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>" 
proof (induction S)
  case (Cons x S)
  have *: "FV\<^sub>s\<^sub>t (x#S \<cdot>\<^sub>s\<^sub>t \<delta>) = FV\<^sub>s\<^sub>t\<^sub>p (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) \<union> FV\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>t \<delta>)"
          "FV\<^sub>s\<^sub>t (x#S) \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> = FV\<^sub>s\<^sub>t\<^sub>p x \<union> FV\<^sub>s\<^sub>t S \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>"
    by simp_all
  moreover have "FV\<^sub>s\<^sub>t\<^sub>p (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) \<subseteq> FV\<^sub>s\<^sub>t\<^sub>p x \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>"
    using subst_sends_FV_to_img[of "trm\<^sub>s\<^sub>t\<^sub>p x" \<delta>] subst_sends_FV_to_img[of "trm_r\<^sub>s\<^sub>t\<^sub>p x" \<delta>]
  proof (cases x)
    case (Inequality X t t')
    let ?\<theta> = "rm_vars (set X) \<delta>"
    have "FV (t \<cdot> ?\<theta>) \<subseteq> FV t \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\<theta>" "FV (t' \<cdot> ?\<theta>) \<subseteq> FV t' \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\<theta>"
      using Inequality subst_sends_FV_to_img[of _ ?\<theta>] by simp_all
    hence "FV (t \<cdot> ?\<theta>) \<subseteq> FV t \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>" "FV (t' \<cdot> ?\<theta>) \<subseteq> FV t' \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>"
      using rm_vars_img_subset[of "set X" \<delta>] by auto 
    thus ?thesis using Inequality by auto
  qed auto
  ultimately show ?case using Cons.IH by auto
qed simp

lemma ineq_apply_subst:
  assumes "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<inter> set X = {}"
  shows "(\<nexists>X\<langle>t \<doteq> t'\<rangle>) \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta> = \<nexists>X\<langle>(t \<cdot> \<delta>) \<doteq> (t' \<cdot> \<delta>)\<rangle>"
using rm_vars_apply'[OF assms] by simp

lemma FV_strand_step_subst:
  assumes "P = FV\<^sub>s\<^sub>t\<^sub>p \<or> P = FV\<^sub>r\<^sub>c\<^sub>v \<or> P = FV\<^sub>s\<^sub>n\<^sub>d \<or> P = FV\<^sub>e\<^sub>q \<or> P = FV\<^sub>i\<^sub>n\<^sub>e\<^sub>q"
  and "set (bvars\<^sub>s\<^sub>t\<^sub>p x) \<inter> (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<union> FV\<^sub>s\<^sub>e\<^sub>t (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>)) = {}"
  shows "FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` (P x)) = P (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>)"
proof (cases x)
  case (Send t)
  hence "vars\<^sub>s\<^sub>t\<^sub>p x = FV t" "FV\<^sub>s\<^sub>n\<^sub>d x = FV t" by auto
  thus ?thesis using assms Send subst_apply_FV_unfold[of _ \<delta>] by auto
next
  case (Receive t)
  hence "vars\<^sub>s\<^sub>t\<^sub>p x = FV t" "FV\<^sub>r\<^sub>c\<^sub>v x = FV t" by auto
  thus ?thesis using assms Receive subst_apply_FV_unfold[of _ \<delta>] by auto
next
  case (Equality t t')
  hence "vars\<^sub>s\<^sub>t\<^sub>p x = FV t \<union> FV t'" "FV\<^sub>e\<^sub>q x = FV t \<union> FV t'" by auto
  thus ?thesis using assms Equality subst_apply_FV_unfold[of _ \<delta>] by auto
next
  case (Inequality X t t')
  hence *: "set X \<inter> (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>) = {}"
           "x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta> = \<nexists>X\<langle>(t \<cdot> \<delta>) \<doteq> (t' \<cdot> \<delta>)\<rangle>" 
    using assms ineq_apply_subst[of \<delta> X t t'] by auto
  have "FV\<^sub>i\<^sub>n\<^sub>e\<^sub>q x = FV t \<union> FV t' - set X"
    using Inequality by auto
  hence "FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` FV\<^sub>i\<^sub>n\<^sub>e\<^sub>q x) = FV\<^sub>s\<^sub>e\<^sub>t (\<delta>`(FV t - set X)) \<union> FV\<^sub>s\<^sub>e\<^sub>t (\<delta>`(FV t' - set X))" by auto
  hence "FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` FV\<^sub>i\<^sub>n\<^sub>e\<^sub>q x) = FV\<^sub>s\<^sub>e\<^sub>t (\<delta>`(FV t)) \<union> FV\<^sub>s\<^sub>e\<^sub>t (\<delta>`(FV t')) - set X"
    using *(1) Inequality by force+
  hence "FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` FV\<^sub>i\<^sub>n\<^sub>e\<^sub>q x) = FV (t \<cdot> \<delta>) \<union> FV (t' \<cdot> \<delta>) - set X"
    using subst_apply_FV_unfold[of _ \<delta>] Inequality by simp
  moreover have "FV\<^sub>i\<^sub>n\<^sub>e\<^sub>q (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = (FV (t \<cdot> \<delta>) \<union> FV (t' \<cdot> \<delta>)) - set X"
    using *(2) by auto
  ultimately have "FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` FV\<^sub>i\<^sub>n\<^sub>e\<^sub>q x) = FV\<^sub>i\<^sub>n\<^sub>e\<^sub>q (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>)"
    using assms(1) Inequality subst_apply_FV_unfold[of _ \<delta>] by simp
  thus ?thesis using assms(1) Inequality subst_apply_FV_unfold[of _ \<delta>] by auto
qed

lemma FV_strand_subst:
  assumes "P = FV\<^sub>s\<^sub>t\<^sub>p \<or> P = FV\<^sub>r\<^sub>c\<^sub>v \<or> P = FV\<^sub>s\<^sub>n\<^sub>d \<or> P = FV\<^sub>e\<^sub>q \<or> P = FV\<^sub>i\<^sub>n\<^sub>e\<^sub>q"
  and "bvars\<^sub>s\<^sub>t S \<inter> (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<union> FV\<^sub>s\<^sub>e\<^sub>t (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>)) = {}"
  shows "FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` (\<Union>set (map P S))) = \<Union>set (map P (S \<cdot>\<^sub>s\<^sub>t \<delta>))"
using assms(2)
proof (induction S)
  case (Cons x S)
  hence *: "bvars\<^sub>s\<^sub>t S \<inter> (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>) = {}"
           "set (bvars\<^sub>s\<^sub>t\<^sub>p x) \<inter> (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>) = {}"
    unfolding bvars\<^sub>s\<^sub>t_def by auto
  hence **: "FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` P x) = P (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>)" using FV_strand_step_subst[OF assms(1), of x \<delta>] by auto
  have "FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` (\<Union>set (map P (x#S)))) = FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` P x) \<union> (\<Union>set (map P ((S \<cdot>\<^sub>s\<^sub>t \<delta>))))"
    using Cons unfolding bvars\<^sub>s\<^sub>t_def by auto
  hence "FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` (\<Union>set (map P (x#S)))) = P (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) \<union> FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` (\<Union>set (map P S)))"
    using ** by simp
  thus ?case using Cons.IH[OF *(1)] unfolding bvars\<^sub>s\<^sub>t_def by simp
qed simp

lemma FV_strand_subst2:
  assumes "bvars\<^sub>s\<^sub>t S \<inter> (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<union> FV\<^sub>s\<^sub>e\<^sub>t (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>)) = {}"
  shows "FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` (vars2\<^sub>s\<^sub>t S)) = vars2\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>t \<delta>)"
by (metis (no_types, lifting) assms FV\<^sub>s\<^sub>e\<^sub>t_def vars_snd_rcv_strand2 FV_strand_subst UN_Un image_Un)

lemma FV_strand_subst':
  assumes "bvars\<^sub>s\<^sub>t S \<inter> (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<union> FV\<^sub>s\<^sub>e\<^sub>t (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>)) = {}"
  shows "FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` (FV\<^sub>s\<^sub>t S)) = FV\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>t \<delta>)"
by (metis assms FV_strand_subst FV\<^sub>s\<^sub>t_def)

lemma strand_map_set_subst:
  assumes \<delta>: "bvars\<^sub>s\<^sub>t S \<inter> (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<union> FV\<^sub>s\<^sub>e\<^sub>t (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>)) = {}"
  shows "set (map trm\<^sub>s\<^sub>t\<^sub>p (S \<cdot>\<^sub>s\<^sub>t \<delta>)) = (set (map trm\<^sub>s\<^sub>t\<^sub>p S)) \<cdot>set \<delta>"
        "set (map trm_r\<^sub>s\<^sub>t\<^sub>p (S \<cdot>\<^sub>s\<^sub>t \<delta>)) = (set (map trm_r\<^sub>s\<^sub>t\<^sub>p S)) \<cdot>set \<delta>"
using assms
proof (induction S)
  case Nil
  { case 1 thus ?case by simp }
  { case 2 thus ?case by simp }
next
  case (Cons x S)
  { case 1
    hence *: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<inter> set (bvars\<^sub>s\<^sub>t\<^sub>p x) = {}"
             "set (map trm\<^sub>s\<^sub>t\<^sub>p (S \<cdot>\<^sub>s\<^sub>t \<delta>)) = set (map trm\<^sub>s\<^sub>t\<^sub>p S) \<cdot>set \<delta>"
      using Cons.IH(1) bvars\<^sub>s\<^sub>t_split[of "[x]" S] bvars\<^sub>s\<^sub>t_singleton[of x] by auto 
    hence **: "trm\<^sub>s\<^sub>t\<^sub>p (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = (trm\<^sub>s\<^sub>t\<^sub>p x) \<cdot> \<delta>"
    proof (cases x)
      case (Inequality X t t') thus ?thesis using rm_vars_apply'[of \<delta> "set X"] * by simp 
    qed simp_all
    thus ?case using * by (auto simp add: subst_all_insert)
  }
  { case 2
    hence *: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<inter> set (bvars\<^sub>s\<^sub>t\<^sub>p x) = {}"
             "set (map trm_r\<^sub>s\<^sub>t\<^sub>p (S \<cdot>\<^sub>s\<^sub>t \<delta>)) = set (map trm_r\<^sub>s\<^sub>t\<^sub>p S) \<cdot>set \<delta>"
      using Cons.IH(2) bvars\<^sub>s\<^sub>t_split[of "[x]" S] bvars\<^sub>s\<^sub>t_singleton[of x] by auto 
    hence **: "trm_r\<^sub>s\<^sub>t\<^sub>p (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = (trm_r\<^sub>s\<^sub>t\<^sub>p x) \<cdot> \<delta>"
    proof (cases x)
      case (Inequality X t t') thus ?thesis using rm_vars_apply'[of \<delta> "set X"] * by simp 
    qed simp_all
    thus ?case using * by (auto simp add: subst_all_insert)
  }
qed

lemma subst_apply_FV_subset_strand_trm:
  assumes P: "P = FV\<^sub>s\<^sub>t\<^sub>p \<or> P = FV\<^sub>r\<^sub>c\<^sub>v \<or> P = FV\<^sub>s\<^sub>n\<^sub>d \<or> P = FV\<^sub>e\<^sub>q \<or> P = FV\<^sub>i\<^sub>n\<^sub>e\<^sub>q"
  and FV_sub: "FV t \<subseteq> \<Union>set (map P S) \<union> V"
  and \<delta>: "bvars\<^sub>s\<^sub>t S \<inter> (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<union> FV\<^sub>s\<^sub>e\<^sub>t (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>)) = {}"
  shows "FV (t \<cdot> \<delta>) \<subseteq> \<Union>set (map P (S \<cdot>\<^sub>s\<^sub>t \<delta>)) \<union> FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` V)"
using FV_strand_subst[OF P \<delta>] subst_apply_FV_subset[OF FV_sub, of \<delta>] by auto

lemma subst_apply_FV_subset_strand_trm2:
  assumes FV_sub: "FV t \<subseteq> vars2\<^sub>s\<^sub>t S \<union> V"
  and \<delta>: "bvars\<^sub>s\<^sub>t S \<inter> (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<union> FV\<^sub>s\<^sub>e\<^sub>t (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>)) = {}"
  shows "FV (t \<cdot> \<delta>) \<subseteq> vars2\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>t \<delta>) \<union> FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` V)"
using FV_strand_subst2[OF \<delta>] subst_apply_FV_subset[OF FV_sub, of \<delta>] by auto

lemma subst_apply_FV_subset_strand:
  assumes P: "P = FV\<^sub>s\<^sub>t\<^sub>p \<or> P = FV\<^sub>r\<^sub>c\<^sub>v \<or> P = FV\<^sub>s\<^sub>n\<^sub>d \<or> P = FV\<^sub>e\<^sub>q \<or> P = FV\<^sub>i\<^sub>n\<^sub>e\<^sub>q"
  and P_subset: "P x \<subseteq> \<Union>set (map P S) \<union> V"
  and \<delta>: "bvars\<^sub>s\<^sub>t S \<inter> (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<union> FV\<^sub>s\<^sub>e\<^sub>t (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>)) = {}"
         "set (bvars\<^sub>s\<^sub>t\<^sub>p x) \<inter> (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<union> FV\<^sub>s\<^sub>e\<^sub>t (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>)) = {}"
  shows "P (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) \<subseteq> \<Union>set (map P (S \<cdot>\<^sub>s\<^sub>t \<delta>)) \<union> FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` V)"
proof (cases x)
  case (Send t)
  hence *: "FV\<^sub>s\<^sub>t\<^sub>p x = FV t" "FV\<^sub>s\<^sub>t\<^sub>p (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = FV (t \<cdot> \<delta>)"
           "FV\<^sub>r\<^sub>c\<^sub>v x = {}" "FV\<^sub>r\<^sub>c\<^sub>v (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = {}"
           "FV\<^sub>s\<^sub>n\<^sub>d x = FV t" "FV\<^sub>s\<^sub>n\<^sub>d (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = FV (t \<cdot> \<delta>)"
           "FV\<^sub>e\<^sub>q x = {}" "FV\<^sub>e\<^sub>q (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = {}"
           "FV\<^sub>i\<^sub>n\<^sub>e\<^sub>q x = {}" "FV\<^sub>i\<^sub>n\<^sub>e\<^sub>q (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = {}"
    by auto
  hence **: "(P x = FV t \<and> P (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = FV (t \<cdot> \<delta>)) \<or> (P x = {} \<and> P (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = {})" by (metis P)
  moreover
  { assume "P x = {}" "P (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = {}" hence ?thesis by simp }
  moreover
  { assume "P x = FV t" "P (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = FV (t \<cdot> \<delta>)"
    hence "FV t \<subseteq> \<Union>set (map P S) \<union> V" using P_subset by auto
    hence "FV (t \<cdot> \<delta>) \<subseteq> \<Union>set (map P (S \<cdot>\<^sub>s\<^sub>t \<delta>)) \<union> FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` V)"
      unfolding vars\<^sub>s\<^sub>t_def using P subst_apply_FV_subset_strand_trm assms by blast
    hence ?thesis using \<open>P (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = FV (t \<cdot> \<delta>)\<close> by auto
  }
  ultimately show ?thesis by metis
next
  case (Receive t)
  hence *: "FV\<^sub>s\<^sub>t\<^sub>p x = FV t" "FV\<^sub>s\<^sub>t\<^sub>p (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = FV (t \<cdot> \<delta>)"
           "FV\<^sub>r\<^sub>c\<^sub>v x = FV t" "FV\<^sub>r\<^sub>c\<^sub>v (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = FV (t \<cdot> \<delta>)"
           "FV\<^sub>s\<^sub>n\<^sub>d x = {}" "FV\<^sub>s\<^sub>n\<^sub>d (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = {}"
           "FV\<^sub>e\<^sub>q x = {}" "FV\<^sub>e\<^sub>q (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = {}"
           "FV\<^sub>i\<^sub>n\<^sub>e\<^sub>q x = {}" "FV\<^sub>i\<^sub>n\<^sub>e\<^sub>q (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = {}"
    by auto
  hence **: "(P x = FV t \<and> P (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = FV (t \<cdot> \<delta>)) \<or> (P x = {} \<and> P (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = {})" by (metis P)
  moreover
  { assume "P x = {}" "P (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = {}" hence ?thesis by simp }
  moreover
  { assume "P x = FV t" "P (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = FV (t \<cdot> \<delta>)"
    hence "FV t \<subseteq> \<Union>set (map P S) \<union> V" using P_subset by auto
    hence "FV (t \<cdot> \<delta>) \<subseteq> \<Union>set (map P (S \<cdot>\<^sub>s\<^sub>t \<delta>)) \<union> FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` V)"
      unfolding vars\<^sub>s\<^sub>t_def using P subst_apply_FV_subset_strand_trm assms by blast
    hence ?thesis using \<open>P (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = FV (t \<cdot> \<delta>)\<close> by auto
  }
  ultimately show ?thesis by metis
next
  case (Equality t t')
  hence *: "FV\<^sub>s\<^sub>t\<^sub>p x = FV t \<union> FV t'" "FV\<^sub>s\<^sub>t\<^sub>p (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = FV (t \<cdot> \<delta>) \<union> FV (t' \<cdot> \<delta>)"
           "FV\<^sub>r\<^sub>c\<^sub>v x = {}" "FV\<^sub>r\<^sub>c\<^sub>v (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = {}"
           "FV\<^sub>s\<^sub>n\<^sub>d x = {}" "FV\<^sub>s\<^sub>n\<^sub>d (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = {}"
           "FV\<^sub>e\<^sub>q x = FV t \<union> FV t'" "FV\<^sub>e\<^sub>q (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = FV (t \<cdot> \<delta>) \<union> FV (t' \<cdot> \<delta>)"
           "FV\<^sub>i\<^sub>n\<^sub>e\<^sub>q x = {}" "FV\<^sub>i\<^sub>n\<^sub>e\<^sub>q (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = {}"
    by auto
  hence **: "(P x = FV t \<union> FV t' \<and> P (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = FV (t \<cdot> \<delta>) \<union> FV (t' \<cdot> \<delta>))
            \<or> (P x = {} \<and> P (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = {})"
    by (metis P)
  moreover
  { assume "P x = {}" "P (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = {}" hence ?thesis by simp }
  moreover
  { assume "P x = FV t \<union> FV t'" "P (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = FV (t \<cdot> \<delta>) \<union> FV (t' \<cdot> \<delta>)"
    hence "FV t \<subseteq> \<Union>set (map P S) \<union> V" "FV t' \<subseteq> \<Union>set (map P S) \<union> V" using P_subset by auto
    hence "FV (t \<cdot> \<delta>) \<subseteq> \<Union>set (map P (S \<cdot>\<^sub>s\<^sub>t \<delta>)) \<union> FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` V)"
          "FV (t' \<cdot> \<delta>) \<subseteq> \<Union>set (map P (S \<cdot>\<^sub>s\<^sub>t \<delta>)) \<union> FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` V)"
      unfolding vars\<^sub>s\<^sub>t_def using P subst_apply_FV_subset_strand_trm assms by blast+
    hence ?thesis using \<open>P (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = FV (t \<cdot> \<delta>) \<union> FV (t' \<cdot> \<delta>)\<close> by auto
  }
  ultimately show ?thesis by metis
next
  case (Inequality X t t')
  hence *: "FV\<^sub>s\<^sub>t\<^sub>p x = FV t \<union> FV t' - set X" "FV\<^sub>s\<^sub>t\<^sub>p (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = FV (t \<cdot> \<delta>) \<union> FV (t' \<cdot> \<delta>) - set X"
           "FV\<^sub>r\<^sub>c\<^sub>v x = {}" "FV\<^sub>r\<^sub>c\<^sub>v (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = {}"
           "FV\<^sub>s\<^sub>n\<^sub>d x = {}" "FV\<^sub>s\<^sub>n\<^sub>d (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = {}"
           "FV\<^sub>e\<^sub>q x = {}" "FV\<^sub>e\<^sub>q (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = {}"
           "FV\<^sub>i\<^sub>n\<^sub>e\<^sub>q x = (FV t \<union> FV t') - set X"
           "FV\<^sub>i\<^sub>n\<^sub>e\<^sub>q (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = FV (t \<cdot> \<delta>) \<union> FV (t' \<cdot> \<delta>) - set X"
    using \<delta>(2) ineq_apply_subst[of \<delta> X t t'] by force+
  hence **: "(P x = FV t \<union> FV t' - set X \<and> P (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = FV (t \<cdot> \<delta>) \<union> FV (t' \<cdot> \<delta>) - set X)
            \<or> (P x = {} \<and> P (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = {})"
    by (metis P)
  moreover
  { assume "P x = {}" "P (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = {}" hence ?thesis by simp }
  moreover
  { assume "P x = FV t \<union> FV t' - set X" "P (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = FV (t \<cdot> \<delta>) \<union> FV (t' \<cdot> \<delta>) - set X"
    hence "FV t - set X \<subseteq> \<Union>set (map P S) \<union> V" "FV t' - set X \<subseteq> \<Union>set (map P S) \<union> V"
      using P_subset by auto
    hence "FV (t \<cdot> \<delta>) \<subseteq> \<Union>set (map P (S \<cdot>\<^sub>s\<^sub>t \<delta>)) \<union> FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` (V \<union> set X))"
          "FV (t' \<cdot> \<delta>) \<subseteq> \<Union>set (map P (S \<cdot>\<^sub>s\<^sub>t \<delta>)) \<union> FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` (V \<union> set X))"
      unfolding vars\<^sub>s\<^sub>t_def
      using subst_apply_FV_subset_strand_trm[OF P _ assms(3), of _ "V \<union> set X"] by blast+
    moreover have "FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` set X) = set X" using assms(4) Inequality by force
    ultimately have
          "FV (t \<cdot> \<delta>) - set X \<subseteq> \<Union>set (map P (S \<cdot>\<^sub>s\<^sub>t \<delta>)) \<union> FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` V)"
          "FV (t' \<cdot> \<delta>) - set X \<subseteq> \<Union>set (map P (S \<cdot>\<^sub>s\<^sub>t \<delta>)) \<union> FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` V)"
      by auto
    hence ?thesis using \<open>P (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = FV (t \<cdot> \<delta>) \<union> FV (t' \<cdot> \<delta>) - set X\<close> by auto
  }
  ultimately show ?thesis by metis
qed

lemma subst_apply_FV_subset_strand2:
  assumes P: "P = FV\<^sub>s\<^sub>t\<^sub>p \<or> P = FV\<^sub>r\<^sub>c\<^sub>v \<or> P = FV\<^sub>s\<^sub>n\<^sub>d \<or> P = FV\<^sub>e\<^sub>q \<or> P = FV\<^sub>i\<^sub>n\<^sub>e\<^sub>q \<or> P = FV_r\<^sub>e\<^sub>q"
  and P_subset: "P x \<subseteq> vars2\<^sub>s\<^sub>t S \<union> V"
  and \<delta>: "bvars\<^sub>s\<^sub>t S \<inter> (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<union> FV\<^sub>s\<^sub>e\<^sub>t (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>)) = {}"
         "set (bvars\<^sub>s\<^sub>t\<^sub>p x) \<inter> (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<union> FV\<^sub>s\<^sub>e\<^sub>t (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>)) = {}"
  shows "P (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) \<subseteq> vars2\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>t \<delta>) \<union> FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` V)"
proof (cases x)
  case (Send t)
  hence *: "FV\<^sub>s\<^sub>t\<^sub>p x = FV t" "FV\<^sub>s\<^sub>t\<^sub>p (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = FV (t \<cdot> \<delta>)"
           "FV\<^sub>r\<^sub>c\<^sub>v x = {}" "FV\<^sub>r\<^sub>c\<^sub>v (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = {}"
           "FV\<^sub>s\<^sub>n\<^sub>d x = FV t" "FV\<^sub>s\<^sub>n\<^sub>d (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = FV (t \<cdot> \<delta>)"
           "FV\<^sub>e\<^sub>q x = {}" "FV\<^sub>e\<^sub>q (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = {}"
           "FV\<^sub>i\<^sub>n\<^sub>e\<^sub>q x = {}" "FV\<^sub>i\<^sub>n\<^sub>e\<^sub>q (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = {}"
           "FV_r\<^sub>e\<^sub>q x = {}" "FV_r\<^sub>e\<^sub>q (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = {}"
    by auto
  hence **: "(P x = FV t \<and> P (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = FV (t \<cdot> \<delta>)) \<or> (P x = {} \<and> P (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = {})" by (metis P)
  moreover
  { assume "P x = {}" "P (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = {}" hence ?thesis by simp }
  moreover
  { assume "P x = FV t" "P (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = FV (t \<cdot> \<delta>)"
    hence "FV t \<subseteq> vars2\<^sub>s\<^sub>t S \<union> V" using P_subset by auto
    hence "FV (t \<cdot> \<delta>) \<subseteq> vars2\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>t \<delta>) \<union> FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` V)"
      using P subst_apply_FV_subset_strand_trm2 assms by blast
    hence ?thesis using \<open>P (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = FV (t \<cdot> \<delta>)\<close> by auto
  }
  ultimately show ?thesis by metis
next
  case (Receive t)
  hence *: "FV\<^sub>s\<^sub>t\<^sub>p x = FV t" "FV\<^sub>s\<^sub>t\<^sub>p (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = FV (t \<cdot> \<delta>)"
           "FV\<^sub>r\<^sub>c\<^sub>v x = FV t" "FV\<^sub>r\<^sub>c\<^sub>v (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = FV (t \<cdot> \<delta>)"
           "FV\<^sub>s\<^sub>n\<^sub>d x = {}" "FV\<^sub>s\<^sub>n\<^sub>d (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = {}"
           "FV\<^sub>e\<^sub>q x = {}" "FV\<^sub>e\<^sub>q (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = {}"
           "FV\<^sub>i\<^sub>n\<^sub>e\<^sub>q x = {}" "FV\<^sub>i\<^sub>n\<^sub>e\<^sub>q (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = {}"
           "FV_r\<^sub>e\<^sub>q x = {}" "FV_r\<^sub>e\<^sub>q (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = {}"
    by auto
  hence **: "(P x = FV t \<and> P (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = FV (t \<cdot> \<delta>)) \<or> (P x = {} \<and> P (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = {})" by (metis P)
  moreover
  { assume "P x = {}" "P (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = {}" hence ?thesis by simp }
  moreover
  { assume "P x = FV t" "P (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = FV (t \<cdot> \<delta>)"
    hence "FV t \<subseteq> vars2\<^sub>s\<^sub>t S \<union> V" using P_subset by auto
    hence "FV (t \<cdot> \<delta>) \<subseteq> vars2\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>t \<delta>) \<union> FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` V)"
      using P subst_apply_FV_subset_strand_trm2 assms by blast
    hence ?thesis using \<open>P (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = FV (t \<cdot> \<delta>)\<close> by auto
  }
  ultimately show ?thesis by metis
next
  case (Equality t t')
  hence *: "FV\<^sub>s\<^sub>t\<^sub>p x = FV t \<union> FV t'" "FV\<^sub>s\<^sub>t\<^sub>p (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = FV (t \<cdot> \<delta>) \<union> FV (t' \<cdot> \<delta>)"
           "FV\<^sub>r\<^sub>c\<^sub>v x = {}" "FV\<^sub>r\<^sub>c\<^sub>v (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = {}"
           "FV\<^sub>s\<^sub>n\<^sub>d x = {}" "FV\<^sub>s\<^sub>n\<^sub>d (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = {}"
           "FV\<^sub>e\<^sub>q x = FV t \<union> FV t'" "FV\<^sub>e\<^sub>q (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = FV (t \<cdot> \<delta>) \<union> FV (t' \<cdot> \<delta>)"
           "FV\<^sub>i\<^sub>n\<^sub>e\<^sub>q x = {}" "FV\<^sub>i\<^sub>n\<^sub>e\<^sub>q (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = {}"
           "FV_r\<^sub>e\<^sub>q x = FV t'" "FV_r\<^sub>e\<^sub>q (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = FV (t' \<cdot> \<delta>)"
    by auto
  hence **: "(P x = FV t \<union> FV t' \<and> P (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = FV (t \<cdot> \<delta>) \<union> FV (t' \<cdot> \<delta>))
            \<or> (P x = {} \<and> P (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = {})
            \<or> (P x = FV t' \<and> P (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = FV (t' \<cdot> \<delta>))"
    by (metis P)
  moreover
  { assume "P x = {}" "P (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = {}" hence ?thesis by simp }
  moreover
  { assume "P x = FV t \<union> FV t'" "P (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = FV (t \<cdot> \<delta>) \<union> FV (t' \<cdot> \<delta>)"
    hence "FV t \<subseteq> vars2\<^sub>s\<^sub>t S \<union> V" "FV t' \<subseteq> vars2\<^sub>s\<^sub>t S \<union> V" using P_subset by auto
    hence "FV (t \<cdot> \<delta>) \<subseteq> vars2\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>t \<delta>) \<union> FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` V)"
          "FV (t' \<cdot> \<delta>) \<subseteq> vars2\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>t \<delta>) \<union> FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` V)"
      using P subst_apply_FV_subset_strand_trm2 assms by blast+
    hence ?thesis using \<open>P (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = FV (t \<cdot> \<delta>) \<union> FV (t' \<cdot> \<delta>)\<close> by auto
  }
  moreover
  { assume "P x = FV t'" "P (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = FV (t' \<cdot> \<delta>)"
    hence "FV t' \<subseteq> vars2\<^sub>s\<^sub>t S \<union> V" using P_subset by auto
    hence "FV (t' \<cdot> \<delta>) \<subseteq> vars2\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>t \<delta>) \<union> FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` V)"
      using P subst_apply_FV_subset_strand_trm2 assms by blast+
    hence ?thesis using \<open>P (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = FV (t' \<cdot> \<delta>)\<close> by auto
  }
  ultimately show ?thesis by metis
next
  case (Inequality X t t')
  hence *: "FV\<^sub>s\<^sub>t\<^sub>p x = FV t \<union> FV t' - set X" "FV\<^sub>s\<^sub>t\<^sub>p (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = FV (t \<cdot> \<delta>) \<union> FV (t' \<cdot> \<delta>) - set X"
           "FV\<^sub>r\<^sub>c\<^sub>v x = {}" "FV\<^sub>r\<^sub>c\<^sub>v (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = {}"
           "FV\<^sub>s\<^sub>n\<^sub>d x = {}" "FV\<^sub>s\<^sub>n\<^sub>d (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = {}"
           "FV\<^sub>e\<^sub>q x = {}" "FV\<^sub>e\<^sub>q (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = {}"
           "FV\<^sub>i\<^sub>n\<^sub>e\<^sub>q x = FV t \<union> FV t' - set X" "FV\<^sub>i\<^sub>n\<^sub>e\<^sub>q (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = FV (t \<cdot> \<delta>) \<union> FV (t' \<cdot> \<delta>) - set X"
           "FV_r\<^sub>e\<^sub>q x = {}" "FV_r\<^sub>e\<^sub>q (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = {}"
    using \<delta>(2) ineq_apply_subst[of \<delta> X t t'] by force+
  hence **: "(P x = FV t \<union> FV t' - set X \<and> P (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = FV (t \<cdot> \<delta>) \<union> FV (t' \<cdot> \<delta>) - set X)
            \<or> (P x = {} \<and> P (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = {})"
    by (metis P)
  moreover
  { assume "P x = {}" "P (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = {}" hence ?thesis by simp }
  moreover
  { assume "P x = FV t \<union> FV t' - set X" "P (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = FV (t \<cdot> \<delta>) \<union> FV (t' \<cdot> \<delta>) - set X"
    hence "FV t - set X \<subseteq> vars2\<^sub>s\<^sub>t S \<union> V" "FV t' - set X \<subseteq> vars2\<^sub>s\<^sub>t S \<union> V" using P_subset by auto
    hence "FV (t \<cdot> \<delta>) \<subseteq> vars2\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>t \<delta>) \<union> FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` (V \<union> set X))"
          "FV (t' \<cdot> \<delta>) \<subseteq> vars2\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>t \<delta>) \<union> FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` (V \<union> set X))"
      unfolding vars\<^sub>s\<^sub>t_def
      using subst_apply_FV_subset_strand_trm2[OF _ assms(3), of _ "V \<union> set X"]
      by blast+
    moreover have "FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` set X) = set X" using assms(4) Inequality by force
    ultimately have
          "FV (t \<cdot> \<delta>) - set X \<subseteq> vars2\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>t \<delta>) \<union> FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` V)"
          "FV (t' \<cdot> \<delta>) - set X \<subseteq> vars2\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>t \<delta>) \<union> FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` V)"
      by auto
    hence ?thesis using \<open>P (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = FV (t \<cdot> \<delta>) \<union> FV (t' \<cdot> \<delta>) - set X\<close> by auto
  }
  ultimately show ?thesis by metis
qed

lemma strand_subst_FV_bounded_if_img_bounded:
  assumes "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<subseteq> FV\<^sub>s\<^sub>t S"
  shows "FV\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>t \<delta>) \<subseteq> FV\<^sub>s\<^sub>t S"
using subst_sends_strand_FV_to_img[of S \<delta>] assms by auto

lemma strand_FV_subst_subset_if_elim:
  assumes "elim \<delta> v" and "v \<in> FV\<^sub>s\<^sub>t S \<or> bvars\<^sub>s\<^sub>t S \<inter> (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>) = {}"
  shows "v \<notin> FV\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>t \<delta>)"
proof (cases "v \<in> FV\<^sub>s\<^sub>t S")
  case True thus ?thesis
  proof (induction S)
    case (Cons x S)
    have *: "v \<notin> FV\<^sub>s\<^sub>t\<^sub>p (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>)"
    using assms(1)
    proof (cases x)
      case (Inequality X t t')
      hence "elim (rm_vars (set X) \<delta>) v \<or> v \<in> set X" using assms(1) by blast
      moreover have
          "FV\<^sub>s\<^sub>t\<^sub>p (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = FV (t \<cdot> rm_vars (set X) \<delta>) \<union> FV (t' \<cdot> rm_vars (set X) \<delta>) - set X"
        using Inequality by auto
      ultimately show ?thesis using Inequality by blast
    qed simp_all
    moreover have "v \<notin> FV\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>t \<delta>)" using Cons.IH
    proof (cases "v \<in> FV\<^sub>s\<^sub>t S")
      case False
      moreover have "v \<notin> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>" by (simp add: elim_dest''[OF assms(1)] img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def) 
      ultimately show ?thesis by (meson UnE subsetCE subst_sends_strand_FV_to_img)
    qed simp
    ultimately show ?case by auto
  qed simp
next
  case False
  thus ?thesis using assms FV_strand_subst' unfolding elim_def
    by (metis (mono_tags, hide_lams) FV\<^sub>s\<^sub>e\<^sub>t_def imageE mem_simps(8) subst_apply_term.simps(1))
qed

lemma strand_FV_subst_subset_if_elim':
  assumes "elim \<delta> v" "v \<in> FV\<^sub>s\<^sub>t S" "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<subseteq> FV\<^sub>s\<^sub>t S"
  shows "FV\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>t \<delta>) \<subset> FV\<^sub>s\<^sub>t S"
using strand_FV_subst_subset_if_elim[OF assms(1)] assms(2)
      strand_subst_FV_bounded_if_img_bounded[OF assms(3)]
by blast

lemma FV_ik_is_FV_rcv: " FV\<^sub>s\<^sub>e\<^sub>t (ik\<^sub>s\<^sub>t S) = \<Union>set (map FV\<^sub>r\<^sub>c\<^sub>v S)"
by (induct S rule: ik\<^sub>s\<^sub>t.induct) auto

lemma FV_ik_subset_FV_st[simp]: "FV\<^sub>s\<^sub>e\<^sub>t (ik\<^sub>s\<^sub>t S) \<subseteq> vars2\<^sub>s\<^sub>t S"
by (induct S rule: ik\<^sub>s\<^sub>t.induct) auto

lemma FV_eqs_rhs_subset_FV_st[simp]: "FV\<^sub>s\<^sub>e\<^sub>t (eqs_rhs\<^sub>s\<^sub>t S) \<subseteq> vars2\<^sub>s\<^sub>t S"
by (induct S rule: eqs_rhs\<^sub>s\<^sub>t.induct) auto

lemma FV_ik_subset_FV_st'[simp]: "FV\<^sub>s\<^sub>e\<^sub>t (ik\<^sub>s\<^sub>t S) \<subseteq> FV\<^sub>s\<^sub>t S"
by (induct S rule: ik\<^sub>s\<^sub>t.induct) auto

lemma FV_eqs_rhs_subset_FV_st'[simp]: "FV\<^sub>s\<^sub>e\<^sub>t (eqs_rhs\<^sub>s\<^sub>t S) \<subseteq> FV\<^sub>s\<^sub>t S"
by (induct S rule: eqs_rhs\<^sub>s\<^sub>t.induct) auto

lemma strand_step_id_subst[iff]: "x \<cdot>\<^sub>s\<^sub>t\<^sub>p Var = x" by (cases x) simp_all

lemma strand_id_subst[iff]: "S \<cdot>\<^sub>s\<^sub>t Var = S" using strand_step_id_subst by (induct S) auto

lemma strand_step_subst_FV_union_bound: "FV\<^sub>s\<^sub>t\<^sub>p (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) \<subseteq> FV\<^sub>s\<^sub>t\<^sub>p x \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>"
using subst_sends_strand_FV_to_img[of "[x]" \<delta>] by simp

lemma strand_subst_FV_union_bound[simp]: "FV\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>t \<delta>) \<subseteq> FV\<^sub>s\<^sub>t S \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>"
by (rule subst_sends_strand_FV_to_img)

lemma strand_subst_vars_union_bound[simp]: "vars\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>t \<delta>) \<subseteq> vars\<^sub>s\<^sub>t S \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>"
proof (induction S)
  case (Cons x S)
  moreover have "vars\<^sub>s\<^sub>t\<^sub>p (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) \<subseteq> vars\<^sub>s\<^sub>t\<^sub>p x \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>" using subst_sends_FV_to_img[of _ \<delta>]
  proof (cases x)
    case (Inequality X t t')
    let ?\<delta> = "rm_vars (set X) \<delta>"
    have "vars\<^sub>s\<^sub>t\<^sub>p (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) = FV (t \<cdot> ?\<delta>) \<union> FV (t' \<cdot> ?\<delta>) \<union> set X" "vars\<^sub>s\<^sub>t\<^sub>p x = FV t \<union> FV t' \<union> set X"
      using Inequality by auto
    moreover have "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t ?\<delta> \<subseteq> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>" using rm_vars_img[of "set X" \<delta>] by auto
    hence "FV (t \<cdot> ?\<delta>) \<subseteq> FV t \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>" "FV (t' \<cdot> ?\<delta>) \<subseteq> FV t' \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>"
      using subst_sends_FV_to_img[of _ ?\<delta>] by blast+
    ultimately show ?thesis by auto
  qed auto
  ultimately show ?case by auto
qed simp

lemma strand_vars_split:
  "vars\<^sub>s\<^sub>t (S@S') = vars\<^sub>s\<^sub>t S \<union> vars\<^sub>s\<^sub>t S'" "vars2\<^sub>s\<^sub>t (S@S') = vars2\<^sub>s\<^sub>t S \<union> vars2\<^sub>s\<^sub>t S'"
  "FV\<^sub>s\<^sub>t (S@S') = FV\<^sub>s\<^sub>t S \<union> FV\<^sub>s\<^sub>t S'"
by auto

lemma bvars_subst_ident: "bvars\<^sub>s\<^sub>t S = bvars\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>t \<delta>)"
proof (induction S)
  case (Cons x S) thus ?case by (cases x) auto
qed simp

lemma strand_subst_Idem:
  assumes "Idem \<delta>" "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<subseteq> FV\<^sub>s\<^sub>t S" "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<inter> FV\<^sub>s\<^sub>t S = {}"
          "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<inter> bvars\<^sub>s\<^sub>t S = {}" "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<inter> bvars\<^sub>s\<^sub>t S = {}"
  shows "(S \<cdot>\<^sub>s\<^sub>t \<delta>) \<cdot>\<^sub>s\<^sub>t \<theta> = (S \<cdot>\<^sub>s\<^sub>t \<delta>)"
  and   "(S \<cdot>\<^sub>s\<^sub>t \<delta>) \<cdot>\<^sub>s\<^sub>t (\<theta> \<circ>\<^sub>s \<delta>) = (S \<cdot>\<^sub>s\<^sub>t \<delta>)"
proof -
  from assms(2,3) have "FV\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>t \<delta>) \<inter> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> = {}"
    using strand_subst_FV_union_bound[of S \<delta>] by blast
  thus "(S \<cdot>\<^sub>s\<^sub>t \<delta>) \<cdot>\<^sub>s\<^sub>t \<theta> = (S \<cdot>\<^sub>s\<^sub>t \<delta>)" by blast
  thus "(S \<cdot>\<^sub>s\<^sub>t \<delta>) \<cdot>\<^sub>s\<^sub>t (\<theta> \<circ>\<^sub>s \<delta>) = (S \<cdot>\<^sub>s\<^sub>t \<delta>)"
    by (metis assms(4,5) bvars_subst_ident strand_subst_comp \<open>Idem \<delta>\<close> Idem_def)
qed

lemma strand_subst_img_bound:
  assumes "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<subseteq> FV\<^sub>s\<^sub>t S" "(dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>) \<inter> bvars\<^sub>s\<^sub>t S = {}"
  shows "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<subseteq> FV\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>t \<delta>)"
proof -
  have "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<subseteq> \<Union>set (map FV\<^sub>s\<^sub>t\<^sub>p S)" by (metis (no_types) FV\<^sub>s\<^sub>t_def Un_subset_iff assms(1))
  thus ?thesis unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def FV\<^sub>s\<^sub>t_def
    by (metis FV_set_mono FV_strand_subst Int_commute assms(2) image_Un le_iff_sup)
qed

lemma strand_subst_img_bound':
  assumes "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<subseteq> vars\<^sub>s\<^sub>t S" "(dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>) \<inter> bvars\<^sub>s\<^sub>t S = {}"
  shows "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<subseteq> vars\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>t \<delta>)"
proof -
  have "(dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<union> FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>)) \<inter> vars\<^sub>s\<^sub>t S = dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<union> FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>)"
    using assms(1) unfolding img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by (meson inf.absorb_iff1)
  hence "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<subseteq> FV\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>t \<delta>)"
    using vars_snd_rcv_strand FV_snd_rcv_strand assms(2) img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def
    by (metis (no_types) inf_le2 inf_sup_distrib1 strand_subst_img_bound sup_bot.right_neutral)
  thus "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<subseteq> vars\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>t \<delta>)" by (metis FV_snd_rcv_strand le_supI1 vars_snd_rcv_strand)
qed

lemma strand_subst_all_FV_subset:
  assumes "FV t \<subseteq> FV\<^sub>s\<^sub>t S" "(dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>) \<inter> bvars\<^sub>s\<^sub>t S = {}"
  shows "FV (t \<cdot> \<delta>) \<subseteq> FV\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>t \<delta>)"
using assms by (metis FV_strand_subst' Int_commute subst_apply_FV_subset)

lemma strand_subst_not_dom_fixed: "\<lbrakk>v \<in> FV\<^sub>s\<^sub>t S; v \<notin> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>\<rbrakk> \<Longrightarrow> v \<in> FV\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>t \<delta>)"
proof (induction S)
  case (Cons x S') show ?case
  proof (cases "v \<in> FV\<^sub>s\<^sub>t S'")
    case True thus ?thesis using Cons.IH[OF _ Cons.prems(2)] by auto
  next
    case False
    hence *: "v \<in> FV\<^sub>s\<^sub>t\<^sub>p x" using Cons.prems(1) by simp
    hence "v \<in> FV\<^sub>s\<^sub>t\<^sub>p (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>)" using Cons.prems(2) subst_not_dom_fixed by (cases x) force+
    thus ?thesis by auto
  qed
qed simp

lemma strand_vars_unfold: "v \<in> vars\<^sub>s\<^sub>t S \<Longrightarrow> \<exists>S' x S''. S = S'@x#S'' \<and> v \<in> vars\<^sub>s\<^sub>t\<^sub>p x"
proof (induction S)
  case (Cons x S) thus ?case
  proof (cases "v \<in> vars\<^sub>s\<^sub>t\<^sub>p x")
    case True thus ?thesis by blast
  next
    case False
    hence "v \<in> vars\<^sub>s\<^sub>t S" using Cons.prems by auto
    thus ?thesis using Cons.IH by (metis append_Cons)
  qed
qed simp

lemma strand_FV_unfold: "v \<in> FV\<^sub>s\<^sub>t S \<Longrightarrow> \<exists>S' x S''. S = S'@x#S'' \<and> v \<in> FV\<^sub>s\<^sub>t\<^sub>p x"
proof (induction S)
  case (Cons x S) thus ?case
  proof (cases "v \<in> FV\<^sub>s\<^sub>t\<^sub>p x")
    case True thus ?thesis by blast
  next
    case False
    hence "v \<in> FV\<^sub>s\<^sub>t S" using Cons.prems by auto
    thus ?thesis using Cons.IH by (metis append_Cons)
  qed
qed simp

lemma (in intruder_model) wf_FV_strand_if_in_trp_ik_union:
  "\<lbrakk>t \<in> trp\<^sub>s\<^sub>e\<^sub>t (ik\<^sub>s\<^sub>t S); wf\<^sub>s\<^sub>t V S\<rbrakk>  \<Longrightarrow> FV t \<subseteq> FV\<^sub>s\<^sub>t S \<union> V"
proof (induction S arbitrary: V rule: ik\<^sub>s\<^sub>t_induct)
  case (ConsRcv t' S)
  hence "FV t' \<subseteq> V" "wf\<^sub>s\<^sub>t V S" by auto
  thus ?case using ConsRcv.IH ConsRcv.prems
  proof (cases "t \<in> trp\<^sub>s\<^sub>e\<^sub>t (ik\<^sub>s\<^sub>t S)")
    case False
    hence "t \<sqsubseteq>\<^sub>t\<^sub>r\<^sub>p t'" using \<open>t \<in> \<Union>(trp ` ik\<^sub>s\<^sub>t (rcv\<langle>t'\<rangle>#S))\<close> by simp
    thus ?thesis using \<open>FV t' \<subseteq> V\<close> trpD[THEN subtermeq_vars_subset] by auto
  qed auto
qed auto

lemma (in intruder_model) subterm_if_in_strand_ik:
  "t \<in> trp\<^sub>s\<^sub>e\<^sub>t (ik\<^sub>s\<^sub>t S) \<Longrightarrow> \<exists>t'. rcv\<langle>t'\<rangle> \<in> set S \<and> t \<sqsubseteq> t'"
proof (induction S rule: ik\<^sub>s\<^sub>t_induct)
  case (ConsRcv t' S) thus ?case by (cases "t \<in> trp\<^sub>s\<^sub>e\<^sub>t (ik\<^sub>s\<^sub>t S)", auto dest!: trpD)
qed simp_all

lemma (in intruder_model) FV_subset_if_in_strand_ik:
  "t \<in> trp\<^sub>s\<^sub>e\<^sub>t (ik\<^sub>s\<^sub>t S) \<Longrightarrow> FV t \<subseteq> \<Union>set (map FV\<^sub>r\<^sub>c\<^sub>v S)"
proof -
  assume "t \<in> trp\<^sub>s\<^sub>e\<^sub>t (ik\<^sub>s\<^sub>t S)"
  then obtain t' where "rcv\<langle>t'\<rangle> \<in> set S" "t \<sqsubseteq> t'" by (metis subterm_if_in_strand_ik)
  hence "FV t \<subseteq> FV t'" by (simp add: subtermeq_vars_subset)
  thus ?thesis using in_strand_FV_subset_rcv[OF \<open>rcv\<langle>t'\<rangle> \<in> set S\<close>] by auto
qed

lemma (in intruder_model) FV_subset_if_in_strand_ik':
  "t \<in> trp\<^sub>s\<^sub>e\<^sub>t (ik\<^sub>s\<^sub>t S) \<Longrightarrow> FV t \<subseteq> FV\<^sub>s\<^sub>t S"
using FV_subset_if_in_strand_ik[of t S] FV_snd_rcv_strand_subset(2)[of S] by simp

lemma (in intruder_model) vars_subset_if_in_strand_ik2:
  "t \<in> trp\<^sub>s\<^sub>e\<^sub>t (ik\<^sub>s\<^sub>t S) \<Longrightarrow> FV t \<subseteq> vars2\<^sub>s\<^sub>t S"
using FV_subset_if_in_strand_ik[of t S] vars_snd_rcv_strand_subset2(2)[of S] by simp


subsection {* Lemmas: Simple Strands *}
lemma simple_cons[dest]: "simple (s#S) \<Longrightarrow> simple S"
by (induct s, auto elim: simple.elims(2))

lemma simple_split[dest]:
  assumes "simple (S@S')"
  shows "simple S" "simple S'"
using assms by (induct S, auto elim: simple.elims(2))

lemma simple_append[intro]: "\<lbrakk>simple S; simple S'\<rbrakk> \<Longrightarrow> simple (S@S')"
proof (induction S)
  case (Cons x S)
  hence "simple (S@S')" by auto
  moreover have "simple [x]"
    by (metis Cons.prems(1) list.distinct(1) list.sel(1) simple.elims(2) simple.simps(1,2,3,4))
  hence "\<not>(\<exists>f X. x = snd\<langle>Fun f X\<rangle>) \<and> \<not>(\<exists>s t. x = s \<doteq> t)" by auto
  hence "(\<exists>t. x = rcv\<langle>t\<rangle>) \<or> (\<exists>v. x = snd\<langle>Var v\<rangle>) \<or> (\<exists>X t t'. x = \<nexists>X\<langle>t \<doteq> t'\<rangle>)"
    by (metis strand_step.exhaust_sel term.exhaust) 
  ultimately show ?case by force
qed simp

lemma simple_append_sym[sym]: "simple (S@S') \<Longrightarrow> simple (S'@S)" by auto

lemma not_simple_if_snd_fun: "(\<exists>S' S'' f X. S = S'@snd\<langle>Fun f X\<rangle>#S'') \<Longrightarrow> \<not>simple S"
proof (induction S)
  case (Cons x S)
  then obtain S\<^sub>p\<^sub>r\<^sub>e f X S\<^sub>s\<^sub>u\<^sub>f where "x#S = S\<^sub>p\<^sub>r\<^sub>e@snd\<langle>Fun f X\<rangle>#S\<^sub>s\<^sub>u\<^sub>f" by metis
  thus ?case by (cases "S\<^sub>p\<^sub>r\<^sub>e = []", auto simp add: Cons.IH)
qed simp

lemma simple_prefix_not_simple_suffix: "\<lbrakk>simple S; \<not>simple (S@S')\<rbrakk> \<Longrightarrow> \<not>simple S'" by auto

lemma not_simple_elim:
  assumes "\<not>simple S"
  shows "(\<exists>S' S'' f X. S = S'@snd\<langle>Fun f X\<rangle>#S'' \<and> simple S') \<or> 
         (\<exists>S' S'' t t'. S = S'@t \<doteq> t'#S'' \<and> simple S')"
using assms
proof (induction S rule: List.rev_induct)
  case (snoc x S) thus ?case
  proof (cases "simple S")
    case True
    hence "\<not>simple [x]" using simple_prefix_not_simple_suffix[OF _ snoc.prems] by metis
    hence "(\<exists>f X. x = snd\<langle>Fun f X\<rangle>) \<or> (\<exists>s t. x = s \<doteq> t)"
      using list.inject simple.elims(3) by fastforce
    thus ?thesis using \<open>simple S\<close> by force
  next
    case False
    thus ?thesis using snoc.IH by force
  qed
qed simp

lemma simple_fun_prefix_unique:
  assumes "A = S@snd\<langle>Fun f X\<rangle>#S'" "simple S"
  shows "\<forall>T g Y T'. A = T@snd\<langle>Fun g Y\<rangle>#T' \<and> simple T \<longrightarrow> S = T \<and> f = g \<and> X = Y \<and> S' = T'"
proof -
  { fix T g Y T' assume *: "A = T@snd\<langle>Fun g Y\<rangle>#T'" "simple T"
    { assume "length S < length T" hence False using assms *
        by (metis id_take_nth_drop not_simple_if_snd_fun nth_append nth_append_length)
    }
    moreover
    { assume "length S > length T" hence False using assms *
        by (metis id_take_nth_drop not_simple_if_snd_fun nth_append nth_append_length)
    }
    ultimately have "S = T" using assms * by (meson List.append_eq_append_conv linorder_neqE_nat)
  }
  thus ?thesis using assms(1) by blast
qed

lemma simple_fun_prefix_unique':
  assumes "S = S'@snd\<langle>Fun f X\<rangle>#S''" "simple S'"
  shows "\<exists>!S' f X S''. S = S'@snd\<langle>Fun f X\<rangle>#S'' \<and> simple S'"
proof -
  let ?P = "\<lambda>(T,g,Y,T'). S = T@snd\<langle>Fun g Y\<rangle>#T' \<and> simple T"

  obtain a where "?P a" using assms by blast

  have "\<And>a. ?P a \<Longrightarrow> (\<And>b. ?P b \<Longrightarrow> a = b)" using simple_fun_prefix_unique[of S] by blast
  hence "\<And>b. ?P b \<Longrightarrow> a = b" using \<open>?P a\<close> by simp
  hence "\<exists>!a. ?P a" using ex1I[of ?P] \<open>?P a\<close> by (metis (no_types, lifting))
  thus ?thesis by blast
qed

lemma simple_snd_is_var: "\<lbrakk>snd\<langle>t\<rangle> \<in> set S; simple S\<rbrakk> \<Longrightarrow> \<exists>v. t = Var v"
by (induct S rule: simple.induct) auto


subsection {* Lemmas: Strand Measure *}
lemma measure\<^sub>s\<^sub>t_wellfounded: "wf measure\<^sub>s\<^sub>t" unfolding measure\<^sub>s\<^sub>t_def by simp

lemma strand_size_append[iff]: "size\<^sub>s\<^sub>t (S@S') = size\<^sub>s\<^sub>t S + size\<^sub>s\<^sub>t S'" by (induct S) auto

lemma strand_size_map_fun_lt[simp]:
  "size\<^sub>s\<^sub>t (map Send X) < size (Fun f X)"
  "size\<^sub>s\<^sub>t (map Send X) < size\<^sub>s\<^sub>t [snd\<langle>Fun f X\<rangle>]"
  "size\<^sub>s\<^sub>t (map Send X) < size\<^sub>s\<^sub>t [rcv\<langle>Fun f X\<rangle>]"
by (induct X) auto

lemma strand_size_rm_fun_lt[simp]:
  "size\<^sub>s\<^sub>t (S@S') < size\<^sub>s\<^sub>t (S@snd\<langle>Fun f X\<rangle>#S')"
  "size\<^sub>s\<^sub>t (S@S') < size\<^sub>s\<^sub>t (S@rcv\<langle>Fun f X\<rangle>#S')"
by (induct S) auto

lemma strand_FV_card_map_fun_eq:
  "card (FV\<^sub>s\<^sub>t (S@snd\<langle>Fun f X\<rangle>#S')) = card (FV\<^sub>s\<^sub>t (S@(map Send X)@S'))"
proof -
  have "FV\<^sub>s\<^sub>t (S@snd\<langle>Fun f X\<rangle>#S') = FV\<^sub>s\<^sub>t (S@(map Send X)@S')" by auto
  thus ?thesis by simp
qed

lemma strand_FV_card_rm_fun_le[simp]: "card (FV\<^sub>s\<^sub>t (S@S')) \<le> card (FV\<^sub>s\<^sub>t (S@snd\<langle>Fun f X\<rangle>#S'))"
by (force intro: card_mono)

lemma strand_FV_card_rm_eq_le[simp]: "card (FV\<^sub>s\<^sub>t (S@S')) \<le> card (FV\<^sub>s\<^sub>t (S@t \<doteq> t'#S'))"
by (force intro: card_mono)


subsection {* Lemmas: Well-formed Strands *}
lemma wf_prefix[dest]: "wf\<^sub>s\<^sub>t V (S@S') \<Longrightarrow> wf\<^sub>s\<^sub>t V S"
by (induct S rule: wf\<^sub>s\<^sub>t.induct) auto

lemma wf_vars_mono[simp]: "wf\<^sub>s\<^sub>t V S \<Longrightarrow> wf\<^sub>s\<^sub>t (V \<union> W) S"
proof (induction S arbitrary: V)
  case (Cons x S) thus ?case
  proof (cases x)
    case (Send t)
    hence "wf\<^sub>s\<^sub>t (V \<union> FV t \<union> W) S" using Cons.prems(1) Cons.IH by simp
    thus ?thesis using Send by (simp add: sup_commute sup_left_commute)
  next
    case (Equality t t')
    hence "wf\<^sub>s\<^sub>t (V \<union> FV t \<union> W) S" "FV t' \<subseteq> V \<union> W" using Cons.prems(1) Cons.IH by auto
    thus ?thesis using Equality by (simp add: sup_commute sup_left_commute)
  qed auto
qed simp

lemma wf\<^sub>s\<^sub>tI[intro]: "vars2\<^sub>s\<^sub>t S \<subseteq> V \<Longrightarrow> wf\<^sub>s\<^sub>t V S"
proof (induction S rule: vars2\<^sub>s\<^sub>t_induct)
  case (ConsSnd t S)
  hence "wf\<^sub>s\<^sub>t V S" "V \<union> FV t = V" by auto
  thus ?case by simp
next
  case (ConsEq t t' S)
  hence "wf\<^sub>s\<^sub>t V S" "FV t' \<subseteq> V" by auto
  thus ?case using wf_vars_mono by simp
qed simp_all

lemma wf_append_suffix: "wf\<^sub>s\<^sub>t V S \<Longrightarrow> vars2\<^sub>s\<^sub>t S' \<subseteq> vars2\<^sub>s\<^sub>t S \<union> V \<Longrightarrow> wf\<^sub>s\<^sub>t V (S@S')"
proof (induction V S rule: wf\<^sub>s\<^sub>t_induct)
  case (ConsSnd V t S)
  hence *: "wf\<^sub>s\<^sub>t (V \<union> FV t) S" by simp_all
  hence "vars2\<^sub>s\<^sub>t S' \<subseteq> vars2\<^sub>s\<^sub>t S \<union> (V \<union> FV t)" using ConsSnd.prems(2) by auto
  thus ?case using ConsSnd.IH * by simp
next
  case (ConsRcv V t S)
  hence *: "FV t \<subseteq> V" "wf\<^sub>s\<^sub>t V S" by simp_all
  hence "vars2\<^sub>s\<^sub>t S' \<subseteq> vars2\<^sub>s\<^sub>t S \<union> V" using ConsRcv.prems(2) by auto
  thus ?case using ConsRcv.IH * by simp
next
  case (ConsEq V t t' S)
  hence *: "FV t' \<subseteq> V" "wf\<^sub>s\<^sub>t (V \<union> FV t) S" by simp_all
  hence "vars2\<^sub>s\<^sub>t S' \<subseteq> vars2\<^sub>s\<^sub>t S \<union> (V \<union> FV t)" using ConsEq.prems(2) by auto
  thus ?case using ConsEq.IH * by simp
qed (simp_all add: wf\<^sub>s\<^sub>tI)

lemma wf_send_compose: "wf\<^sub>s\<^sub>t V (S@(map Send X)@S') = wf\<^sub>s\<^sub>t V (S@snd\<langle>Fun f X\<rangle>#S')"
proof (induction S arbitrary: V)
  case Nil thus ?case 
  proof (induction X arbitrary: V)
    case (Cons y Y) thus ?case by (simp add: sup_assoc)
  qed simp
next
  case (Cons s S) thus ?case by (cases s) simp_all
qed

lemma wf_snd_append[iff]: "wf\<^sub>s\<^sub>t V (S@[snd\<langle>t\<rangle>]) = wf\<^sub>s\<^sub>t V S"
by (induct S rule: wf\<^sub>s\<^sub>t.induct) simp_all

lemma wf_snd_append': "wf\<^sub>s\<^sub>t V S \<Longrightarrow> wf\<^sub>s\<^sub>t V (snd\<langle>t\<rangle>#S)"
by simp

lemma wf_rcv_append[dest]: "wf\<^sub>s\<^sub>t V (S@rcv\<langle>t\<rangle>#S') \<Longrightarrow> wf\<^sub>s\<^sub>t V (S@S')"
by (induct S rule: wf\<^sub>s\<^sub>t.induct) simp_all

lemma wf_rcv_append'[intro]: "\<lbrakk>wf\<^sub>s\<^sub>t V (S@S'); FV t \<subseteq> vars2\<^sub>s\<^sub>t S \<union> V\<rbrakk> \<Longrightarrow> wf\<^sub>s\<^sub>t V (S@rcv\<langle>t\<rangle>#S')"
proof (induction S rule: wf\<^sub>s\<^sub>t_induct)
  case (ConsRcv V t' S)
  hence "wf\<^sub>s\<^sub>t V (S@S')" "FV t \<subseteq> vars2\<^sub>s\<^sub>t S \<union> V" by auto
  thus ?case using ConsRcv by auto
next
  case (ConsEq V t' t'' S)
  hence "wf\<^sub>s\<^sub>t (V \<union> FV t') (S@S')" "FV t \<subseteq> vars2\<^sub>s\<^sub>t S \<union> (V \<union> FV t')" by auto
  thus ?case using ConsEq by auto
qed auto

lemma wf_rcv_append''[intro]: "\<lbrakk>wf\<^sub>s\<^sub>t V S; FV t \<subseteq> \<Union>set (map FV\<^sub>s\<^sub>n\<^sub>d S)\<rbrakk> \<Longrightarrow> wf\<^sub>s\<^sub>t V (S@[rcv\<langle>t\<rangle>])"
apply (induct S, simp)
by (metis vars_snd_rcv_strand_subset2(1) append_Nil2 le_supI1 order_trans wf_rcv_append')

lemma wf_rcv_append'''[intro]: "\<lbrakk>wf\<^sub>s\<^sub>t V S; FV t \<subseteq> vars2\<^sub>s\<^sub>t S \<union> V\<rbrakk> \<Longrightarrow> wf\<^sub>s\<^sub>t V (S@[rcv\<langle>t\<rangle>])"
by (simp add: wf_rcv_append'[of _ _ "[]"])

lemma wf_eq_append[dest]: "wf\<^sub>s\<^sub>t V (S@t \<doteq> t'#S') \<Longrightarrow> FV t \<subseteq> vars2\<^sub>s\<^sub>t S \<union> V \<Longrightarrow> wf\<^sub>s\<^sub>t V (S@S')"
proof (induction S rule: wf\<^sub>s\<^sub>t_induct)
  case (Nil V)
  hence "V \<union> FV t = V" "wf\<^sub>s\<^sub>t (V \<union> FV t) S'" by auto
  thus ?case by auto
next
  case (ConsRcv V u S)
  hence "wf\<^sub>s\<^sub>t V (S @ t \<doteq> t' # S')" "FV t \<subseteq> vars2\<^sub>s\<^sub>t S \<union> V" "FV u \<subseteq> V" by auto
  hence "wf\<^sub>s\<^sub>t V (S@S')" using ConsRcv.IH by auto
  thus ?case using \<open>FV u \<subseteq> V\<close> by simp
next
  case (ConsEq V u u' S)
  hence "wf\<^sub>s\<^sub>t (V \<union> FV u) (S@t \<doteq> t'#S')" "FV t \<subseteq> vars2\<^sub>s\<^sub>t S \<union> (V \<union> FV u)" "FV u' \<subseteq> V" by auto
  hence "wf\<^sub>s\<^sub>t (V \<union> FV u) (S@S')" using ConsEq.IH by auto
  thus ?case using \<open>FV u' \<subseteq> V\<close> by simp
qed auto

lemma wf_eq_append'[intro]: "\<lbrakk>wf\<^sub>s\<^sub>t V (S@S'); FV t' \<subseteq> vars2\<^sub>s\<^sub>t S \<union> V\<rbrakk> \<Longrightarrow> wf\<^sub>s\<^sub>t V (S@t \<doteq> t'#S')"
proof (induction S rule: wf\<^sub>s\<^sub>t_induct)
  case (ConsEq V u u' S)
  hence "wf\<^sub>s\<^sub>t (V \<union> FV u) (S@S')" "FV t' \<subseteq> vars2\<^sub>s\<^sub>t S \<union> V \<union> FV u" by auto
  thus ?case using ConsEq by auto
next
  case (ConsRcv V u S)
  hence "wf\<^sub>s\<^sub>t V (S@S')" "FV t' \<subseteq> vars2\<^sub>s\<^sub>t S \<union> V" by auto
  thus ?case using ConsRcv by auto
next
  case (ConsSnd V u S)
  hence "wf\<^sub>s\<^sub>t (V \<union> FV u) (S@S')" "FV t' \<subseteq> vars2\<^sub>s\<^sub>t S \<union> (V \<union> FV u)" by auto
  thus ?case using ConsSnd by auto
qed auto

lemma wf_eq_append''[intro]: "\<lbrakk>wf\<^sub>s\<^sub>t V (S@S'); FV t' \<subseteq> wfvarsoccs\<^sub>s\<^sub>t S \<union> V\<rbrakk> \<Longrightarrow> wf\<^sub>s\<^sub>t V (S@[t \<doteq> t']@S')"
proof (induction S rule: wf\<^sub>s\<^sub>t_induct)
  case (ConsEq V u u' S)
  hence "wf\<^sub>s\<^sub>t (V \<union> FV u) (S@S')" "FV t' \<subseteq> wfvarsoccs\<^sub>s\<^sub>t S \<union> V \<union> FV u" by auto
  thus ?case using ConsEq by auto
next
  case (ConsRcv V u S)
  hence "wf\<^sub>s\<^sub>t V (S@S')" "FV t' \<subseteq> wfvarsoccs\<^sub>s\<^sub>t S \<union> V" by auto
  thus ?case using ConsRcv by auto
next
  case (ConsSnd V u S)
  hence "wf\<^sub>s\<^sub>t (V \<union> FV u) (S@S')" "FV t' \<subseteq> wfvarsoccs\<^sub>s\<^sub>t S \<union> (V \<union> FV u)" by auto
  thus ?case using ConsSnd by auto
qed auto

lemma wf_eq_append'''[intro]: "\<lbrakk>wf\<^sub>s\<^sub>t V S; FV t' \<subseteq> vars2\<^sub>s\<^sub>t S \<union> V\<rbrakk> \<Longrightarrow> wf\<^sub>s\<^sub>t V (S@[t \<doteq> t'])"
by (simp add: wf_eq_append'[of _ _ "[]"])

lemma wf_ineq_append[dest]: "wf\<^sub>s\<^sub>t V (S@\<nexists>X\<langle>t \<doteq> t'\<rangle>#S') \<Longrightarrow> wf\<^sub>s\<^sub>t V (S@S')"
by (induct S rule: wf\<^sub>s\<^sub>t.induct) simp_all

lemma wf_ineq_append'[intro]: "wf\<^sub>s\<^sub>t V (S@S') \<Longrightarrow> wf\<^sub>s\<^sub>t V (S@\<nexists>X\<langle>t \<doteq> t'\<rangle>#S')"
by (induct S rule: wf\<^sub>s\<^sub>t.induct) auto

lemma wf_ineq_append''[intro]: "wf\<^sub>s\<^sub>t V S \<Longrightarrow> wf\<^sub>s\<^sub>t V (S@[\<nexists>X\<langle>t \<doteq> t'\<rangle>])"
by (induct S rule: wf\<^sub>s\<^sub>t.induct) auto

lemma wf_rcv_FV_single[elim]: "wf\<^sub>s\<^sub>t V (rcv\<langle>t\<rangle>#S') \<Longrightarrow> FV t \<subseteq> V"
by simp

lemma wf_append_exec: "wf\<^sub>s\<^sub>t V (S@S') \<Longrightarrow> wf\<^sub>s\<^sub>t (V \<union> wfvarsoccs\<^sub>s\<^sub>t S) S'"
proof (induction S arbitrary: V)
  case (Cons x S V) thus ?case
  proof (cases x)
    case (Send t)
    hence "wf\<^sub>s\<^sub>t (V \<union> FV t \<union> wfvarsoccs\<^sub>s\<^sub>t S) S'" using Cons.prems Cons.IH by simp
    thus ?thesis using Send by (simp add: sup_assoc)
  next
    case (Equality t t')
    hence "wf\<^sub>s\<^sub>t (V \<union> FV t \<union> wfvarsoccs\<^sub>s\<^sub>t S) S'" using Cons.prems Cons.IH by simp
    thus ?thesis using Equality by (simp add: sup_assoc)
  qed auto
qed simp

lemma wf_rcv_FV: "wf\<^sub>s\<^sub>t V (S@rcv\<langle>t\<rangle>#S') \<Longrightarrow> FV t \<subseteq> wfvarsoccs\<^sub>s\<^sub>t S \<union> V"
proof (induction S arbitrary: V)
  case (Cons x S V) thus ?case by (cases x) auto
qed simp

lemma wf_eq_FV: "wf\<^sub>s\<^sub>t V (S@t \<doteq> t'#S') \<Longrightarrow> FV t' \<subseteq> wfvarsoccs\<^sub>s\<^sub>t S \<union> V"
proof (induction S arbitrary: V)
  case (Cons x S V) thus ?case by (cases x) auto
qed simp

lemma wf_simple_FV_occurrence:
  assumes "wf\<^sub>s\<^sub>t {} S" "simple S" "v \<in> vars2\<^sub>s\<^sub>t S"
  shows "\<exists>S\<^sub>p\<^sub>r\<^sub>e S\<^sub>s\<^sub>u\<^sub>f. S = S\<^sub>p\<^sub>r\<^sub>e@snd\<langle>Var v\<rangle>#S\<^sub>s\<^sub>u\<^sub>f \<and> v \<notin> vars2\<^sub>s\<^sub>t S\<^sub>p\<^sub>r\<^sub>e"
using assms
proof (induction S rule: List.rev_induct)
  case (snoc x S)
  from \<open>wf\<^sub>s\<^sub>t {} (S@[x])\<close> have "wf\<^sub>s\<^sub>t {} S" "wf\<^sub>s\<^sub>t (vars2\<^sub>s\<^sub>t S) [x]"
    using wf_append_exec[THEN wf_vars_mono, of "{}" S "[x]" "vars2\<^sub>s\<^sub>t S - wfvarsoccs\<^sub>s\<^sub>t S"]
          vars_snd_rcv_strand_subset2(4)[of S] Diff_partition[of "wfvarsoccs\<^sub>s\<^sub>t S" "vars2\<^sub>s\<^sub>t S"]
    by auto
  from \<open>simple (S@[x])\<close> have "simple S" "simple [x]" by auto

  show ?case
  proof (cases "v \<in> vars2\<^sub>s\<^sub>t S")
    case True thus ?thesis using snoc.IH[OF \<open>wf\<^sub>s\<^sub>t {} S\<close> \<open>simple S\<close>] by fastforce
  next
    case False
    show ?thesis
    proof (cases x)
      case (Receive t)
      hence "FV t \<subseteq> vars2\<^sub>s\<^sub>t S" using \<open>wf\<^sub>s\<^sub>t (vars2\<^sub>s\<^sub>t S) [x]\<close> by simp
      hence "v \<in> vars2\<^sub>s\<^sub>t S" using \<open>v \<in> vars2\<^sub>s\<^sub>t (S@[x])\<close> \<open>x = rcv\<langle>t\<rangle>\<close> by auto
      thus ?thesis using \<open>x = rcv\<langle>t\<rangle>\<close> snoc.IH[OF \<open>wf\<^sub>s\<^sub>t {} S\<close> \<open>simple S\<close>] by fastforce
    next
      case (Send t)
      hence "v \<in> vars\<^sub>s\<^sub>t\<^sub>p x" using \<open>v \<in> vars2\<^sub>s\<^sub>t (S@[x])\<close> False by auto
      from Send obtain w where "t = Var w" using \<open>simple [x]\<close> by (cases t) simp_all
      
      hence "v = w" using \<open>x = snd\<langle>t\<rangle>\<close> \<open>v \<in> vars\<^sub>s\<^sub>t\<^sub>p x\<close> by simp
      thus ?thesis using \<open>x = snd\<langle>t\<rangle>\<close> \<open>v \<notin> vars2\<^sub>s\<^sub>t S\<close> \<open>t = Var w\<close> by auto
    next
      case (Equality t t') thus ?thesis using snoc.prems(2) by auto
    next
      case (Inequality t t') thus ?thesis using False snoc.prems(3) by auto
    qed
  qed
qed simp

lemma (in intruder_model) Unifier_strand_FV_subset:
  assumes g_in_ik: "t \<in> trp\<^sub>s\<^sub>e\<^sub>t (ik\<^sub>s\<^sub>t S)"
  and \<delta>: "Unifier \<delta> (Fun f X) t"
  and disj: "bvars\<^sub>s\<^sub>t S \<inter> (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>) = {}"
  shows "FV (Fun f X \<cdot> \<delta>) \<subseteq> \<Union>set (map FV\<^sub>r\<^sub>c\<^sub>v (S \<cdot>\<^sub>s\<^sub>t \<delta>))"
proof -
  have "FV t \<subseteq> \<Union>set (map FV\<^sub>r\<^sub>c\<^sub>v S)" using FV_subset_if_in_strand_ik[OF g_in_ik] by simp
  hence "FV (t \<cdot> \<delta>) \<subseteq> \<Union>set (map FV\<^sub>r\<^sub>c\<^sub>v (S \<cdot>\<^sub>s\<^sub>t \<delta>))" using FV_strand_subst
    by (metis (no_types) disj FV_strand_subst subst_apply_FV_subset)
  thus ?thesis using \<delta> by simp
qed

lemma wf\<^sub>s\<^sub>t_induct'[consumes 1, case_names Nil ConsSnd ConsRcv ConsEq ConsIneq]:
  fixes S::"('a,'b) strand"
  assumes "wf\<^sub>s\<^sub>t V S"
          "P []"
          "\<And>t S. \<lbrakk>wf\<^sub>s\<^sub>t V S; P S\<rbrakk> \<Longrightarrow> P (S@[snd\<langle>t\<rangle>])"
          "\<And>t S. \<lbrakk>wf\<^sub>s\<^sub>t V S; P S; FV t \<subseteq> V \<union> wfvarsoccs\<^sub>s\<^sub>t S\<rbrakk> \<Longrightarrow> P (S@[rcv\<langle>t\<rangle>])"
          "\<And>t t' S. \<lbrakk>wf\<^sub>s\<^sub>t V S; P S; FV t' \<subseteq> V \<union> wfvarsoccs\<^sub>s\<^sub>t S\<rbrakk> \<Longrightarrow> P (S@[t \<doteq> t'])"
          "\<And>X t t' S. \<lbrakk>wf\<^sub>s\<^sub>t V S; P S\<rbrakk> \<Longrightarrow> P (S@[\<nexists>X\<langle>t \<doteq> t'\<rangle>])"
  shows "P S"
using assms
proof (induction S rule: List.rev_induct)
  case (snoc x S)
  hence *: "wf\<^sub>s\<^sub>t V S" "wf\<^sub>s\<^sub>t (V \<union> wfvarsoccs\<^sub>s\<^sub>t S) [x]"
    by (metis wf_prefix, metis wf_append_exec)
  show ?case
  proof (cases x)
    case (Send t) thus ?thesis using *(1) snoc.prems snoc.IH by auto
  next
    case (Equality t t') thus ?thesis using *(2) snoc.prems snoc.IH by auto
  next
    case (Inequality t t') thus ?thesis using *(2) snoc.prems snoc.IH by auto
  next
    case (Receive t)
    hence "P S" using snoc.prems snoc.IH[OF *(1) \<open>P []\<close>] by auto
    thus ?thesis using \<open>x = rcv\<langle>t\<rangle>\<close> snoc.prems(4)[OF *(1), of t] *(2) by auto
  qed
qed simp

lemma (in intruder_model) wf_subst_apply:
  "wf\<^sub>s\<^sub>t V S \<Longrightarrow> wf\<^sub>s\<^sub>t (FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` V)) (S \<cdot>\<^sub>s\<^sub>t \<delta>)"
proof (induction S arbitrary: V rule: wf\<^sub>s\<^sub>t_induct)
  case (ConsRcv V t S)
  hence "wf\<^sub>s\<^sub>t V (rcv\<langle>t\<rangle>#S)" "FV t \<subseteq> V" by simp_all
  hence "wf\<^sub>s\<^sub>t (FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` V)) (S \<cdot>\<^sub>s\<^sub>t \<delta>)" "FV (t \<cdot> \<delta>) \<subseteq> FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` V)"
    using ConsRcv.IH subst_apply_FV_subset by simp_all
  thus ?case by simp
next
  case (ConsSnd V t S)
  hence "wf\<^sub>s\<^sub>t (V \<union> FV t) S" by simp
  hence "wf\<^sub>s\<^sub>t (FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` (V \<union> FV t))) (S \<cdot>\<^sub>s\<^sub>t \<delta>)" using ConsSnd.IH by metis
  hence "wf\<^sub>s\<^sub>t (FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` V) \<union> (FV (t \<cdot> \<delta>))) (S \<cdot>\<^sub>s\<^sub>t \<delta>)" using subst_apply_FV_union by metis
  thus ?case by simp
next
  case (ConsEq V t t' S)
  hence "wf\<^sub>s\<^sub>t (V \<union> FV t) (rcv\<langle>t\<rangle>#S)" "FV t' \<subseteq> V" by simp_all
  hence "wf\<^sub>s\<^sub>t (FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` (V \<union> FV t))) (S \<cdot>\<^sub>s\<^sub>t \<delta>)" and *: "FV (t' \<cdot> \<delta>) \<subseteq> FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` V)"
    using ConsEq.IH subst_apply_FV_subset by force+
  hence "wf\<^sub>s\<^sub>t (FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` V) \<union> (FV (t \<cdot> \<delta>))) (S \<cdot>\<^sub>s\<^sub>t \<delta>)" using subst_apply_FV_union by metis
  thus ?case using * by simp
qed simp_all

lemma (in intruder_model) wf_unify:
  assumes wf: "wf\<^sub>s\<^sub>t V (S@snd\<langle>Fun f X\<rangle>#S')"
  and g_in_ik: "t \<in> trp\<^sub>s\<^sub>e\<^sub>t (ik\<^sub>s\<^sub>t S)"
  and \<delta>: "Unifier \<delta> (Fun f X) t"
  and disj: "bvars\<^sub>s\<^sub>t (S@snd\<langle>Fun f X\<rangle>#S') \<inter> (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>) = {}"
  shows "wf\<^sub>s\<^sub>t (FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` V)) ((S@S') \<cdot>\<^sub>s\<^sub>t \<delta>)"
using assms
proof (induction S' arbitrary: V rule: List.rev_induct)
  case (snoc x S' V)

  have fun_FV_bound: "FV (Fun f X \<cdot> \<delta>) \<subseteq> \<Union>set (map FV\<^sub>r\<^sub>c\<^sub>v (S \<cdot>\<^sub>s\<^sub>t \<delta>))"
    using snoc.prems(4) bvars\<^sub>s\<^sub>t_split Unifier_strand_FV_subset[OF g_in_ik \<delta>] by auto
  hence "FV (Fun f X \<cdot> \<delta>) \<subseteq> FV\<^sub>s\<^sub>e\<^sub>t (ik\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>t \<delta>))" using FV_ik_is_FV_rcv by metis
  hence "FV (Fun f X \<cdot> \<delta>) \<subseteq> vars2\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>t \<delta>)" using FV_ik_subset_FV_st[of "S \<cdot>\<^sub>s\<^sub>t \<delta>"] by blast
  hence *: "FV ((Fun f X) \<cdot> \<delta>) \<subseteq> vars2\<^sub>s\<^sub>t ((S@S') \<cdot>\<^sub>s\<^sub>t \<delta>)" by auto

  from snoc.prems(1) have "wf\<^sub>s\<^sub>t V (S@snd\<langle>Fun f X\<rangle>#S')"
    using wf_prefix[of V "S@snd\<langle>Fun f X\<rangle>#S'" "[x]"] by simp
  hence **: "wf\<^sub>s\<^sub>t (FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` V)) ((S@S') \<cdot>\<^sub>s\<^sub>t \<delta>)"
    using snoc.IH[OF _ snoc.prems(2,3)] snoc.prems(4) by auto

  from snoc.prems(1) have ***: "wf\<^sub>s\<^sub>t (V \<union> wfvarsoccs\<^sub>s\<^sub>t (S@snd\<langle>Fun f X\<rangle>#S')) [x]"
    using wf_append_exec[of V "(S@snd\<langle>Fun f X\<rangle>#S')" "[x]"] by simp

  from snoc.prems(4) have disj':
      "bvars\<^sub>s\<^sub>t (S@S') \<inter> (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>) = {}"
      "set (bvars\<^sub>s\<^sub>t\<^sub>p x) \<inter> (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>) = {}"
    by auto

  show ?case
  proof (cases x)
    case (Send t)
    thus ?thesis using wf_snd_append[of "FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` V)" "(S@S') \<cdot>\<^sub>s\<^sub>t \<delta>"] ** by auto
  next
    case (Receive t)
    hence "FV\<^sub>s\<^sub>t\<^sub>p x \<subseteq> V \<union> wfvarsoccs\<^sub>s\<^sub>t (S@snd\<langle>Fun f X\<rangle>#S')" using *** by auto
    hence "FV\<^sub>s\<^sub>t\<^sub>p x \<subseteq> V \<union> vars2\<^sub>s\<^sub>t (S@snd\<langle>Fun f X\<rangle>#S')"
      using vars_snd_rcv_strand_subset2(4)[of "S@snd\<langle>Fun f X\<rangle>#S'"] by blast
    hence "FV\<^sub>s\<^sub>t\<^sub>p x \<subseteq> V \<union> FV (Fun f X) \<union> vars2\<^sub>s\<^sub>t (S@S')" by auto
    hence "FV\<^sub>s\<^sub>t\<^sub>p (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) \<subseteq> FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` V) \<union> FV ((Fun f X) \<cdot> \<delta>) \<union> vars2\<^sub>s\<^sub>t ((S@S') \<cdot>\<^sub>s\<^sub>t \<delta>)"
      by (metis (no_types) inf_sup_aci(5) subst_apply_FV_subset_strand2 subst_apply_FV_union disj')
    hence "FV\<^sub>s\<^sub>t\<^sub>p (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) \<subseteq> FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` V) \<union> vars2\<^sub>s\<^sub>t ((S@S') \<cdot>\<^sub>s\<^sub>t \<delta>)" using * by blast
    hence "FV (t \<cdot> \<delta>) \<subseteq> vars2\<^sub>s\<^sub>t ((S@S') \<cdot>\<^sub>s\<^sub>t \<delta>) \<union> FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` V) " using \<open>x = rcv\<langle>t\<rangle>\<close> by auto
    hence "wf\<^sub>s\<^sub>t (FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` V)) (((S@S') \<cdot>\<^sub>s\<^sub>t \<delta>)@[rcv\<langle>t \<cdot> \<delta>\<rangle>])"
      using wf_rcv_append'''[OF **, of "t \<cdot> \<delta>"] by metis
    thus ?thesis using \<open>x = rcv\<langle>t\<rangle>\<close> by auto
  next
    case (Equality s s')
    hence "FV s' \<subseteq> V \<union> wfvarsoccs\<^sub>s\<^sub>t (S@snd\<langle>Fun f X\<rangle>#S')" using *** by auto
    hence "FV s' \<subseteq> V \<union> vars2\<^sub>s\<^sub>t (S@snd\<langle>Fun f X\<rangle>#S')"
      using vars_snd_rcv_strand_subset2(4)[of "S@snd\<langle>Fun f X\<rangle>#S'"] by blast
    hence "FV s' \<subseteq> V \<union> FV (Fun f X) \<union> vars2\<^sub>s\<^sub>t (S@S')" by auto
    moreover have "FV s' = FV_r\<^sub>e\<^sub>q x" "FV (s' \<cdot> \<delta>) = FV_r\<^sub>e\<^sub>q (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>)" using Equality by simp_all
    ultimately have "FV (s' \<cdot> \<delta>) \<subseteq> FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` V) \<union> FV (Fun f X \<cdot> \<delta>) \<union> vars2\<^sub>s\<^sub>t ((S@S') \<cdot>\<^sub>s\<^sub>t \<delta>)"
      using subst_apply_FV_subset_strand2[of FV_r\<^sub>e\<^sub>q x]
      by (metis (no_types) inf_sup_aci(5) subst_apply_FV_union disj')
    hence "FV (s' \<cdot> \<delta>) \<subseteq> FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` V) \<union> vars2\<^sub>s\<^sub>t ((S@S') \<cdot>\<^sub>s\<^sub>t \<delta>)" using * by blast
    hence "FV (s' \<cdot> \<delta>) \<subseteq> vars2\<^sub>s\<^sub>t ((S@S') \<cdot>\<^sub>s\<^sub>t \<delta>) \<union> FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` V)" using \<open>x = s \<doteq> s'\<close> by auto
    hence "wf\<^sub>s\<^sub>t (FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` V)) (((S@S') \<cdot>\<^sub>s\<^sub>t \<delta>)@[(s \<cdot> \<delta>) \<doteq> (s' \<cdot> \<delta>)])"
      using wf_eq_append'''[OF **] by metis
    thus ?thesis using \<open>x = s \<doteq> s'\<close> by auto
  next
    case (Inequality t t') thus ?thesis using wf_ineq_append''[OF **] by simp
  qed
qed (auto dest: wf_subst_apply)

lemma (in intruder_model) wf_equality:
  assumes wf: "wf\<^sub>s\<^sub>t V (S@t \<doteq> t'#S')"
  and \<delta>: "mgu t t' = Some \<delta>"
  and disj: "bvars\<^sub>s\<^sub>t (S@t \<doteq> t'#S') \<inter> (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>) = {}"
  shows "wf\<^sub>s\<^sub>t (FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` V)) ((S@S') \<cdot>\<^sub>s\<^sub>t \<delta>)"
using assms
proof (induction S' arbitrary: V rule: List.rev_induct)
  case Nil thus ?case using wf_prefix[of V S "[t \<doteq> t']"] wf_subst_apply[of V S \<delta>] by auto
next
  case (snoc x S' V)
  hence "FV t' \<subseteq> V \<union> wfvarsoccs\<^sub>s\<^sub>t S"
    using wf_eq_FV[of V, of S t t' "S'@[x]"] by auto
  hence "FV t' \<subseteq> V \<union> vars2\<^sub>s\<^sub>t S"
    using vars_snd_rcv_strand_subset2(4)[of S] by blast
  hence "FV t' \<subseteq> V \<union> vars2\<^sub>s\<^sub>t (S@S')" by auto
  moreover have disj':
      "bvars\<^sub>s\<^sub>t (S@S') \<inter> (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>) = {}"
      "set (bvars\<^sub>s\<^sub>t\<^sub>p x) \<inter> (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>) = {}"
      "bvars\<^sub>s\<^sub>t (S@t \<doteq> t'#S') \<inter> (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>) = {}"
    using snoc.prems(3) by auto
  ultimately have "FV (t' \<cdot> \<delta>) \<subseteq> FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` V) \<union> vars2\<^sub>s\<^sub>t ((S@S') \<cdot>\<^sub>s\<^sub>t \<delta>)"
    by (metis inf_sup_aci(5) subst_apply_FV_subset_strand_trm2)
  moreover have "FV (t \<cdot> \<delta>) = FV (t' \<cdot> \<delta>)"
    by (metis MGU_is_Unifier[OF mgu_gives_MGU[OF \<delta>]])
  ultimately have *: "FV (t \<cdot> \<delta>) \<union> FV (t' \<cdot> \<delta>) \<subseteq> FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` V) \<union> vars2\<^sub>s\<^sub>t ((S@S') \<cdot>\<^sub>s\<^sub>t \<delta>)"
    by simp

  from snoc.prems(1) have "wf\<^sub>s\<^sub>t V (S@t \<doteq> t'#S')" using wf_prefix[of V "S@t \<doteq> t'#S'"] by simp
  hence **: "wf\<^sub>s\<^sub>t (FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` V)) ((S@S') \<cdot>\<^sub>s\<^sub>t \<delta>)" by (metis snoc.IH \<delta> disj'(3))

  from snoc.prems(1) have ***: "wf\<^sub>s\<^sub>t (V \<union> wfvarsoccs\<^sub>s\<^sub>t (S@t \<doteq> t'#S')) [x]"
    using wf_append_exec[of V "(S@t \<doteq> t'#S')" "[x]"] by simp

  show ?case
  proof (cases x)
    case (Send t)
    thus ?thesis using wf_snd_append[of "FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` V)" "(S@S') \<cdot>\<^sub>s\<^sub>t \<delta>"] ** by auto
  next
    case (Receive s)
    hence "FV\<^sub>s\<^sub>t\<^sub>p x \<subseteq> V \<union> wfvarsoccs\<^sub>s\<^sub>t (S@t \<doteq> t'#S')" using *** by auto
    hence "FV\<^sub>s\<^sub>t\<^sub>p x \<subseteq> V \<union> vars2\<^sub>s\<^sub>t (S@t \<doteq> t'#S')"
      using vars_snd_rcv_strand_subset2(4)[of "S@t \<doteq> t'#S'"] by blast
    hence "FV\<^sub>s\<^sub>t\<^sub>p x \<subseteq> V \<union> FV t \<union> FV t' \<union> vars2\<^sub>s\<^sub>t (S@S')" by auto
    hence "FV\<^sub>s\<^sub>t\<^sub>p (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) \<subseteq> FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` V) \<union> FV (t \<cdot> \<delta>) \<union> FV (t' \<cdot> \<delta>) \<union> vars2\<^sub>s\<^sub>t ((S@S') \<cdot>\<^sub>s\<^sub>t \<delta>)"
      using subst_apply_FV_subset_strand2[of FV\<^sub>s\<^sub>t\<^sub>p]
      by (metis (no_types) inf_sup_aci(5) subst_apply_FV_union disj'(1,2))
    hence "FV\<^sub>s\<^sub>t\<^sub>p (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>) \<subseteq> FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` V) \<union> vars2\<^sub>s\<^sub>t ((S@S') \<cdot>\<^sub>s\<^sub>t \<delta>)" using * by blast
    hence "FV (s \<cdot> \<delta>) \<subseteq> vars2\<^sub>s\<^sub>t ((S@S') \<cdot>\<^sub>s\<^sub>t \<delta>) \<union> (FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` V))" using \<open>x = rcv\<langle>s\<rangle>\<close> by auto
    hence "wf\<^sub>s\<^sub>t (FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` V)) (((S@S') \<cdot>\<^sub>s\<^sub>t \<delta>)@[rcv\<langle>s \<cdot> \<delta>\<rangle>])"
      using wf_rcv_append'''[OF **, of "s \<cdot> \<delta>"] by metis
    thus ?thesis using \<open>x = rcv\<langle>s\<rangle>\<close> by auto
  next
    case (Equality s s')
    hence "FV s' \<subseteq> V \<union> wfvarsoccs\<^sub>s\<^sub>t (S@t \<doteq> t'#S')" using *** by auto
    hence "FV s' \<subseteq> V \<union> vars2\<^sub>s\<^sub>t (S@t \<doteq> t'#S')"
      using vars_snd_rcv_strand_subset2(4)[of "S@t \<doteq> t'#S'"] by blast
    hence "FV s' \<subseteq> V \<union> FV t \<union> FV t' \<union> vars2\<^sub>s\<^sub>t (S@S')" by auto
    moreover have "FV s' = FV_r\<^sub>e\<^sub>q x" "FV (s' \<cdot> \<delta>) = FV_r\<^sub>e\<^sub>q (x \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>)" using Equality by simp_all
    ultimately have "FV (s' \<cdot> \<delta>) \<subseteq> FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` V) \<union> FV (t \<cdot> \<delta>) \<union> FV (t' \<cdot> \<delta>) \<union> vars2\<^sub>s\<^sub>t ((S@S') \<cdot>\<^sub>s\<^sub>t \<delta>)"
      using subst_apply_FV_subset_strand2[of FV_r\<^sub>e\<^sub>q x]
      by (metis (no_types) inf_sup_aci(5) subst_apply_FV_union disj'(1,2))
    hence "FV (s' \<cdot> \<delta>) \<subseteq> FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` V) \<union> vars2\<^sub>s\<^sub>t ((S@S') \<cdot>\<^sub>s\<^sub>t \<delta>)" using * by blast
    hence "FV (s' \<cdot> \<delta>) \<subseteq> vars2\<^sub>s\<^sub>t ((S@S') \<cdot>\<^sub>s\<^sub>t \<delta>) \<union> FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` V)" using \<open>x = s \<doteq> s'\<close> by auto
    hence "wf\<^sub>s\<^sub>t (FV\<^sub>s\<^sub>e\<^sub>t (\<delta> ` V)) (((S@S') \<cdot>\<^sub>s\<^sub>t \<delta>)@[(s \<cdot> \<delta>) \<doteq> (s' \<cdot> \<delta>)])"
      using wf_eq_append'''[OF **] by metis
    thus ?thesis using \<open>x = s \<doteq> s'\<close> by auto
  next
    case (Inequality s s') thus ?thesis using wf_ineq_append''[OF **] by simp
  qed
qed

lemma wf_rcv_prefix_ground:
  "wf\<^sub>s\<^sub>t {} ((map Receive M)@S) \<Longrightarrow> vars\<^sub>s\<^sub>t (map Receive M) = {}"
by (induct M) auto

lemma simple_wfvarsoccs\<^sub>s\<^sub>t_is_FV\<^sub>s\<^sub>n\<^sub>d:
  assumes "simple S"
  shows "wfvarsoccs\<^sub>s\<^sub>t S = \<Union>set (map FV\<^sub>s\<^sub>n\<^sub>d S)"
using assms by (induct S rule: simple.induct) auto

lemma wf\<^sub>s\<^sub>t_simple_induct[consumes 2, case_names Nil ConsSnd ConsRcv ConsIneq]:
  fixes S::"('a,'b) strand"
  assumes "wf\<^sub>s\<^sub>t V S" "simple S"
          "P []"
          "\<And>v S. \<lbrakk>wf\<^sub>s\<^sub>t V S; simple S; P S\<rbrakk> \<Longrightarrow> P (S@[snd\<langle>Var v\<rangle>])"
          "\<And>t S. \<lbrakk>wf\<^sub>s\<^sub>t V S; simple S; P S; FV t \<subseteq> V \<union> \<Union>set (map FV\<^sub>s\<^sub>n\<^sub>d S)\<rbrakk> \<Longrightarrow> P (S@[rcv\<langle>t\<rangle>])"
          "\<And>X t t' S. \<lbrakk>wf\<^sub>s\<^sub>t V S; simple S; P S\<rbrakk> \<Longrightarrow> P (S@[\<nexists>X\<langle>t \<doteq> t'\<rangle>])"
  shows "P S"
using assms
proof (induction S rule: wf\<^sub>s\<^sub>t_induct')
  case (ConsSnd t S)
  hence "P S" by auto
  obtain v where "t = Var v" using simple_snd_is_var[OF _ \<open>simple (S@[snd\<langle>t\<rangle>])\<close>] by auto
  thus ?case using ConsSnd.prems(3)[OF \<open>wf\<^sub>s\<^sub>t V S\<close> _ \<open>P S\<close>] \<open>simple (S@[snd\<langle>t\<rangle>])\<close> by auto
next
  case (ConsRcv t S) thus ?case using simple_wfvarsoccs\<^sub>s\<^sub>t_is_FV\<^sub>s\<^sub>n\<^sub>d[of "S@[rcv\<langle>t\<rangle>]"] by auto
qed auto

lemma wf_trm_stp_dom_FV_disjoint:
  "\<lbrakk>wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S \<theta>; t \<in> trm\<^sub>s\<^sub>t\<^sub>p ` set S\<rbrakk> \<Longrightarrow> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<inter> FV t = {}"
unfolding wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r_def by auto

lemma wf_constr_bvars_disj: "wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S \<theta> \<Longrightarrow> (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>) \<inter> bvars\<^sub>s\<^sub>t S = {}"
by auto

lemma wf_constr_bvars_disj':
  assumes "wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S \<theta>" "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<subseteq> FV\<^sub>s\<^sub>t S"
  shows "(dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>) \<inter> bvars\<^sub>s\<^sub>t S = {}" (is ?A)
  and "(dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>) \<inter> bvars\<^sub>s\<^sub>t (S \<cdot>\<^sub>s\<^sub>t \<delta>) = {}" (is ?B)
proof -
  have *: "(dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>) \<inter> bvars\<^sub>s\<^sub>t S = {}" "FV\<^sub>s\<^sub>t S \<inter> bvars\<^sub>s\<^sub>t S = {}"
    using assms(1) by auto
  thus ?A and ?B using assms(2) bvars_subst_ident[of S \<delta>] by blast+
qed

lemma (in intruder_model) wf_trp_ik_dom_FV_disjoint: 
  assumes "wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S \<theta>" "t \<in> trp\<^sub>s\<^sub>e\<^sub>t (ik\<^sub>s\<^sub>t S)"
  shows "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<inter> FV t = {}"
using \<open>wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S \<theta>\<close> FV_subset_if_in_strand_ik'[OF \<open>t \<in> trp\<^sub>s\<^sub>e\<^sub>t (ik\<^sub>s\<^sub>t S)\<close>]
unfolding wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r_def by blast

lemma (in intruder_model) wf_simple_strand_first_snd_var_split:
  assumes "wf\<^sub>s\<^sub>t {} S" "simple S" "\<exists>v \<in> vars2\<^sub>s\<^sub>t S. t \<cdot> \<I> = \<I> v"
  shows "\<exists>v S\<^sub>p\<^sub>r\<^sub>e S\<^sub>s\<^sub>u\<^sub>f. S = S\<^sub>p\<^sub>r\<^sub>e@snd\<langle>Var v\<rangle>#S\<^sub>s\<^sub>u\<^sub>f \<and> t \<cdot> \<I> = \<I> v
                      \<and> \<not>(\<exists>w \<in> vars2\<^sub>s\<^sub>t S\<^sub>p\<^sub>r\<^sub>e. t \<cdot> \<I> = \<I> w)"
using assms
proof (induction S rule: wf\<^sub>s\<^sub>t_simple_induct)
  case (ConsSnd v S) show ?case
  proof (cases "\<exists>w \<in> vars2\<^sub>s\<^sub>t S. t \<cdot> \<I> = \<I> w")
    case True thus ?thesis using ConsSnd.IH by fastforce
  next
    case False thus ?thesis using ConsSnd.prems by auto
  qed
next
  case (ConsRcv t' S)
  have "\<And>v. v \<in> FV t' \<Longrightarrow> v \<in> vars2\<^sub>s\<^sub>t S" using ConsRcv.hyps(3) by auto
  hence "\<exists>v \<in> vars2\<^sub>s\<^sub>t S. t \<cdot> \<I> = \<I> v" using ConsRcv.prems(1) by fastforce
  hence "\<exists>v S\<^sub>p\<^sub>r\<^sub>e S\<^sub>s\<^sub>u\<^sub>f. S = S\<^sub>p\<^sub>r\<^sub>e@snd\<langle>Var v\<rangle>#S\<^sub>s\<^sub>u\<^sub>f \<and> t \<cdot> \<I> = \<I> v \<and> \<not> (\<exists>w\<in>vars2\<^sub>s\<^sub>t S\<^sub>p\<^sub>r\<^sub>e. t \<cdot> \<I> = \<I> w)"
    by (metis ConsRcv.IH)
  thus ?case by fastforce 
next
  case (ConsIneq X s s' S)
  moreover have "vars2\<^sub>s\<^sub>t (S @ [\<nexists>X\<langle>s \<doteq> s'\<rangle>]) = vars2\<^sub>s\<^sub>t S" by auto
  ultimately have
      "\<exists>v S\<^sub>p\<^sub>r\<^sub>e S\<^sub>s\<^sub>u\<^sub>f. S = S\<^sub>p\<^sub>r\<^sub>e@snd\<langle>Var v\<rangle>#S\<^sub>s\<^sub>u\<^sub>f \<and> t \<cdot> \<I> = \<I> v \<and> \<not> (\<exists>w\<in>vars2\<^sub>s\<^sub>t S\<^sub>p\<^sub>r\<^sub>e. t \<cdot> \<I> = \<I> w)"
    by auto
  thus ?case by fastforce
qed simp

lemma (in intruder_model) wf_strand_first_snd_var_split:
  assumes "wf\<^sub>s\<^sub>t {} S" "\<exists>v \<in> vars2\<^sub>s\<^sub>t S. t \<cdot> \<I> \<sqsubseteq> \<I> v"
  shows "\<exists>S\<^sub>p\<^sub>r\<^sub>e S\<^sub>s\<^sub>u\<^sub>f. \<not>(\<exists>w \<in> vars2\<^sub>s\<^sub>t S\<^sub>p\<^sub>r\<^sub>e. t \<cdot> \<I> \<sqsubseteq> \<I> w)
            \<and> ((\<exists>t'. S = S\<^sub>p\<^sub>r\<^sub>e@snd\<langle>t'\<rangle>#S\<^sub>s\<^sub>u\<^sub>f \<and> t \<cdot> \<I> \<sqsubseteq> t' \<cdot> \<I>)
               \<or> (\<exists>t' t''. S = S\<^sub>p\<^sub>r\<^sub>e@t' \<doteq> t''#S\<^sub>s\<^sub>u\<^sub>f \<and> t \<cdot> \<I> \<sqsubseteq> t' \<cdot> \<I>))"
using assms
proof (induction S rule: wf\<^sub>s\<^sub>t_induct')
  case (ConsSnd t' S) show ?case
  proof (cases "\<exists>w \<in> vars2\<^sub>s\<^sub>t S. t \<cdot> \<I> \<sqsubseteq> \<I> w")
    case True
    then obtain S\<^sub>p\<^sub>r\<^sub>e S\<^sub>s\<^sub>u\<^sub>f where
            "\<not>(\<exists>w \<in> vars2\<^sub>s\<^sub>t S\<^sub>p\<^sub>r\<^sub>e. t \<cdot> \<I> \<sqsubseteq> \<I> w)"
            "(\<exists>t'. S = S\<^sub>p\<^sub>r\<^sub>e@snd\<langle>t'\<rangle>#S\<^sub>s\<^sub>u\<^sub>f \<and> t \<cdot> \<I> \<sqsubseteq> t' \<cdot> \<I>) \<or>
             (\<exists>t' t''. S = S\<^sub>p\<^sub>r\<^sub>e@t' \<doteq> t''#S\<^sub>s\<^sub>u\<^sub>f \<and> t \<cdot> \<I> \<sqsubseteq> t' \<cdot> \<I>)"
      using ConsSnd.IH by moura
    thus ?thesis by fastforce
  next
    case False
    then obtain v where v: "v \<in> FV t'" "t \<cdot> \<I> \<sqsubseteq> \<I> v" using ConsSnd.prems by auto
    hence "t \<cdot> \<I> \<sqsubseteq> t' \<cdot> \<I>"
      using subst_mono[of "Var v" t' \<I>] vars_iff_subtermeq[of v t'] subtermeq_trans
      by auto 
    thus ?thesis using False v by auto
  qed
next
  case (ConsRcv t' S)
  have "FV t' \<subseteq> vars2\<^sub>s\<^sub>t S" using ConsRcv.hyps vars_snd_rcv_strand_subset2(4)[of S] by auto
  hence "\<exists>v \<in> vars2\<^sub>s\<^sub>t S. t \<cdot> \<I> \<sqsubseteq> \<I> v" using ConsRcv.prems by auto
  then obtain S\<^sub>p\<^sub>r\<^sub>e S\<^sub>s\<^sub>u\<^sub>f where
            "\<not>(\<exists>w \<in> vars2\<^sub>s\<^sub>t S\<^sub>p\<^sub>r\<^sub>e. t \<cdot> \<I> \<sqsubseteq> \<I> w)"
            "(\<exists>t'. S = S\<^sub>p\<^sub>r\<^sub>e@snd\<langle>t'\<rangle>#S\<^sub>s\<^sub>u\<^sub>f \<and> t \<cdot> \<I> \<sqsubseteq> t' \<cdot> \<I>) \<or>
             (\<exists>t' t''. S = S\<^sub>p\<^sub>r\<^sub>e@t' \<doteq> t''#S\<^sub>s\<^sub>u\<^sub>f \<and> t \<cdot> \<I> \<sqsubseteq> t' \<cdot> \<I>)"
      using ConsRcv.IH by moura
  thus ?case by fastforce
next
  case (ConsEq s s' S)
  have *: "FV s' \<subseteq> vars2\<^sub>s\<^sub>t S" using ConsEq.hyps vars_snd_rcv_strand_subset2(4)[of S] by auto
  show ?case
  proof (cases "\<exists>v \<in> vars2\<^sub>s\<^sub>t S. t \<cdot> \<I> \<sqsubseteq> \<I> v")
    case True
    then obtain S\<^sub>p\<^sub>r\<^sub>e S\<^sub>s\<^sub>u\<^sub>f where
            "\<not>(\<exists>w \<in> vars2\<^sub>s\<^sub>t S\<^sub>p\<^sub>r\<^sub>e. t \<cdot> \<I> \<sqsubseteq> \<I> w)"
            "(\<exists>t'. S = S\<^sub>p\<^sub>r\<^sub>e@snd\<langle>t'\<rangle>#S\<^sub>s\<^sub>u\<^sub>f \<and> t \<cdot> \<I> \<sqsubseteq> t' \<cdot> \<I>) \<or>
             (\<exists>t' t''. S = S\<^sub>p\<^sub>r\<^sub>e@t' \<doteq> t''#S\<^sub>s\<^sub>u\<^sub>f \<and> t \<cdot> \<I> \<sqsubseteq> t' \<cdot> \<I>)"
      using ConsEq.IH by moura
    thus ?thesis by fastforce
  next
    case False
    then obtain v where "v \<in> FV s" "t \<cdot> \<I> \<sqsubseteq> \<I> v" using ConsEq.prems * by auto
    hence "t \<cdot> \<I> \<sqsubseteq> s \<cdot> \<I>"
      using vars_iff_subtermeq[of v s] subst_mono[of "Var v" s \<I>] subtermeq_trans
      by auto
    thus ?thesis using False by fastforce
  qed
next
  case (ConsIneq X s s' S)
  hence "\<exists>v \<in> vars2\<^sub>s\<^sub>t S. t \<cdot> \<I> \<sqsubseteq> \<I> v" by auto
  then obtain S\<^sub>p\<^sub>r\<^sub>e S\<^sub>s\<^sub>u\<^sub>f where
            "\<not>(\<exists>w \<in> vars2\<^sub>s\<^sub>t S\<^sub>p\<^sub>r\<^sub>e. t \<cdot> \<I> \<sqsubseteq> \<I> w)"
            "(\<exists>t'. S = S\<^sub>p\<^sub>r\<^sub>e@snd\<langle>t'\<rangle>#S\<^sub>s\<^sub>u\<^sub>f \<and> t \<cdot> \<I> \<sqsubseteq> t' \<cdot> \<I>) \<or>
             (\<exists>t' t''. S = S\<^sub>p\<^sub>r\<^sub>e@t' \<doteq> t''#S\<^sub>s\<^sub>u\<^sub>f \<and> t \<cdot> \<I> \<sqsubseteq> t' \<cdot> \<I>)"
      using ConsIneq.IH by moura
  thus ?case by fastforce
qed simp


subsection {* Constraint Semantics *}
context intruder_model
begin

subsubsection {* Definitions *}
type_synonym ('a,'b) constrsem = "('a,'b) subst \<Rightarrow> bool"

fun strand_sem_c::"('fun,'var) terms \<Rightarrow> ('fun,'var) strand \<Rightarrow> ('fun,'var) constrsem" ("\<lbrakk>_; _\<rbrakk>\<^sub>c")
where
  "\<lbrakk>M; []\<rbrakk>\<^sub>c = (\<lambda>\<I>. True)"
| "\<lbrakk>M; snd\<langle>t\<rangle>#S\<rbrakk>\<^sub>c = (\<lambda>\<I>. M \<cdot>set \<I> \<turnstile>\<^sub>c t \<cdot> \<I> \<and> \<lbrakk>M; S\<rbrakk>\<^sub>c \<I>)"
| "\<lbrakk>M; rcv\<langle>t\<rangle>#S\<rbrakk>\<^sub>c = \<lbrakk>insert t M; S\<rbrakk>\<^sub>c"
| "\<lbrakk>M; t \<doteq> t'#S\<rbrakk>\<^sub>c = (\<lambda>\<I>. t \<cdot> \<I> = t' \<cdot> \<I> \<and> \<lbrakk>M; S\<rbrakk>\<^sub>c \<I>)"
| "\<lbrakk>M; \<nexists>X\<langle>t \<doteq> t'\<rangle>#S\<rbrakk>\<^sub>c =
        (\<lambda>\<I>. (\<forall>\<delta>. 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>) \<and> \<lbrakk>M; S\<rbrakk>\<^sub>c \<I>)"

definition constr_sem_c ("_ \<Turnstile>\<^sub>c \<langle>_,_\<rangle>") where "\<I> \<Turnstile>\<^sub>c \<langle>S,\<theta>\<rangle> \<equiv> (\<theta> supports \<I> \<and> \<lbrakk>{}; S\<rbrakk>\<^sub>c \<I>)"
abbreviation constr_sem_c' ("_ \<Turnstile>\<^sub>c \<langle>_\<rangle>" 90) where "\<I> \<Turnstile>\<^sub>c \<langle>S\<rangle> \<equiv> \<I> \<Turnstile>\<^sub>c \<langle>S,Var\<rangle>"

fun strand_sem_d::"('fun,'var) terms \<Rightarrow> ('fun,'var) strand \<Rightarrow> ('fun,'var) constrsem" ("\<lbrakk>_; _\<rbrakk>\<^sub>d")
where
  "\<lbrakk>M; []\<rbrakk>\<^sub>d = (\<lambda>\<I>. True)"
| "\<lbrakk>M; snd\<langle>t\<rangle>#S\<rbrakk>\<^sub>d = (\<lambda>\<I>. M \<cdot>set \<I> \<turnstile> t \<cdot> \<I> \<and> \<lbrakk>M; S\<rbrakk>\<^sub>d \<I>)"
| "\<lbrakk>M; rcv\<langle>t\<rangle>#S\<rbrakk>\<^sub>d = \<lbrakk>insert t M; S\<rbrakk>\<^sub>d"
| "\<lbrakk>M; t \<doteq> t'#S\<rbrakk>\<^sub>d = (\<lambda>\<I>. t \<cdot> \<I> = t' \<cdot> \<I> \<and> \<lbrakk>M; S\<rbrakk>\<^sub>d \<I>)"
| "\<lbrakk>M; \<nexists>X\<langle>t \<doteq> t'\<rangle>#S\<rbrakk>\<^sub>d =
        (\<lambda>\<I>. (\<forall>\<delta>. 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>) \<and> \<lbrakk>M; S\<rbrakk>\<^sub>d \<I>)"

definition constr_sem_d ("_ \<Turnstile> \<langle>_,_\<rangle>") where "\<I> \<Turnstile> \<langle>S,\<theta>\<rangle> \<equiv> (\<theta> supports \<I> \<and> \<lbrakk>{}; S\<rbrakk>\<^sub>d \<I>)"
abbreviation constr_sem_d' ("_ \<Turnstile> \<langle>_\<rangle>" 90) where "\<I> \<Turnstile> \<langle>S\<rangle> \<equiv> \<I> \<Turnstile> \<langle>S,Var\<rangle>"

lemmas strand_sem_induct = strand_sem_c.induct[case_names Nil ConsSnd ConsRcv ConsEq ConsIneq]

declare constr_sem_c_def[simp]
declare constr_sem_d_def[simp]

subsubsection {* Lemmas *}
lemma strand_sem_d_mono_ik: "\<lbrakk>M \<subseteq> M'; \<lbrakk>M; S\<rbrakk>\<^sub>d \<theta>\<rbrakk> \<Longrightarrow> \<lbrakk>M'; S\<rbrakk>\<^sub>d \<theta>"
proof (induction M S arbitrary: M' rule: strand_sem_induct)
  case (ConsSnd M t S)
  hence "M \<cdot>set \<theta> \<turnstile> t \<cdot> \<theta>" "\<lbrakk>M'; S\<rbrakk>\<^sub>d \<theta>" by auto
  hence "M' \<cdot>set \<theta> \<turnstile> t \<cdot> \<theta>"
    using ideduct_mono \<open>M \<subseteq> M'\<close>
    by (metis image_mono)
  thus ?case using \<open>\<lbrakk>M'; S\<rbrakk>\<^sub>d \<theta>\<close> by simp
qed auto

lemma strand_sem_d_if_c: "\<I> \<Turnstile>\<^sub>c \<langle>S,\<theta>\<rangle> \<Longrightarrow> \<I> \<Turnstile> \<langle>S,\<theta>\<rangle>"
proof -
  assume *: "\<I> \<Turnstile>\<^sub>c \<langle>S,\<theta>\<rangle>"
  { fix M have "\<lbrakk>M; S\<rbrakk>\<^sub>c \<I> \<Longrightarrow> \<lbrakk>M; S\<rbrakk>\<^sub>d \<I>"
    proof (induction S rule: strand_sem_induct)
      case (ConsSnd M t S)
      hence "M \<cdot>set \<I> \<turnstile>\<^sub>c t \<cdot> \<I>" "\<lbrakk>M; S\<rbrakk>\<^sub>d \<I>" by auto
      thus ?case
        using strand_sem_d.simps(2)[of M t S]
        by auto
    qed auto
  }
  thus ?thesis using * by simp
qed

lemma strand_sem_mono_ik: "\<lbrakk>M \<subseteq> M'; \<lbrakk>M; S\<rbrakk>\<^sub>c \<theta>\<rbrakk> \<Longrightarrow> \<lbrakk>M'; S\<rbrakk>\<^sub>c \<theta>"
proof (induction M S arbitrary: M' rule: strand_sem_induct)
  case (ConsSnd M t S)
  hence "M \<cdot>set \<theta> \<turnstile>\<^sub>c t \<cdot> \<theta>" "\<lbrakk>M'; S\<rbrakk>\<^sub>c \<theta>" by auto
  hence "M' \<cdot>set \<theta> \<turnstile>\<^sub>c t \<cdot> \<theta>"
    using ideduct_synth_mono \<open>M \<subseteq> M'\<close>
    by (metis Union_mono image_mono)
  thus ?case using \<open>\<lbrakk>M'; S\<rbrakk>\<^sub>c \<theta>\<close> by simp
qed auto

lemma strand_sem_split_left[dest]: "\<lbrakk>M; S@S'\<rbrakk>\<^sub>c \<theta> \<Longrightarrow> \<lbrakk>M; S\<rbrakk>\<^sub>c \<theta>"
proof (induct S arbitrary: M)
  case (Cons x S) thus ?case by (cases x) simp_all
qed simp

lemma strand_sem_split_left_d[dest]: "\<lbrakk>M; S@S'\<rbrakk>\<^sub>d \<theta> \<Longrightarrow> \<lbrakk>M; S\<rbrakk>\<^sub>d \<theta>"
proof (induct S arbitrary: M)
  case (Cons x S) thus ?case by (cases x) simp_all
qed simp

lemma strand_sem_split_right[dest]: "\<lbrakk>M; S@S'\<rbrakk>\<^sub>c \<theta> \<Longrightarrow> \<lbrakk>M \<union> ik\<^sub>s\<^sub>t S; S'\<rbrakk>\<^sub>c \<theta>"
proof (induction S arbitrary: M rule: ik\<^sub>s\<^sub>t_induct)
  case (ConsRcv t S M) thus ?case using ConsRcv.IH[of "insert t M"] by simp
qed simp_all

lemma strand_sem_split_right_d[dest]: "\<lbrakk>M; S@S'\<rbrakk>\<^sub>d \<theta> \<Longrightarrow> \<lbrakk>M \<union> ik\<^sub>s\<^sub>t S; S'\<rbrakk>\<^sub>d \<theta>"
proof (induction S arbitrary: M rule: ik\<^sub>s\<^sub>t_induct)
  case (ConsRcv t S M) thus ?case using ConsRcv.IH[of "insert t M"] by simp
qed simp_all

lemma strand_sem_snd_split[dest]:
  "\<lbrakk>\<lbrakk>M; map Send X\<rbrakk>\<^sub>c \<theta>; x \<in> set X\<rbrakk> \<Longrightarrow> \<lbrakk>M; [snd\<langle>x\<rangle>]\<rbrakk>\<^sub>c \<theta>"
by (induct "map Send X" arbitrary: X rule: strand_sem_c.induct) auto

lemma strand_sem_snd_split_d[dest]:
  "\<lbrakk>\<lbrakk>M; map Send X\<rbrakk>\<^sub>d \<theta>; x \<in> set X\<rbrakk> \<Longrightarrow> \<lbrakk>M; [snd\<langle>x\<rangle>]\<rbrakk>\<^sub>d \<theta>"
by (induct "map Send X" arbitrary: X rule: strand_sem_d.induct) auto

lemma strand_sem_snd_split'[dest]:
  "\<lbrakk>\<lbrakk>M; map Send X@S\<rbrakk>\<^sub>c \<theta>; x \<in> set X\<rbrakk> \<Longrightarrow> \<lbrakk>M; snd\<langle>x\<rangle>#S\<rbrakk>\<^sub>c \<theta>"
using strand_sem_snd_split strand_sem_split_right strand_sem_split_left
by (metis ik_snd_empty strand_sem_c.simps(2) sup_bot.right_neutral)

lemma strand_sem_append[intro]: "\<lbrakk>\<lbrakk>M; S\<rbrakk>\<^sub>c \<theta>; \<lbrakk>M \<union> ik\<^sub>s\<^sub>t S; S'\<rbrakk>\<^sub>c \<theta>\<rbrakk> \<Longrightarrow> \<lbrakk>M; S@S'\<rbrakk>\<^sub>c \<theta>"
proof (induction S arbitrary: M)
  case (Cons x S) thus ?case by (cases x) auto
qed simp

lemma strand_sem_append_d[intro]: "\<lbrakk>\<lbrakk>M; S\<rbrakk>\<^sub>d \<theta>; \<lbrakk>M \<union> ik\<^sub>s\<^sub>t S; S'\<rbrakk>\<^sub>d \<theta>\<rbrakk> \<Longrightarrow> \<lbrakk>M; S@S'\<rbrakk>\<^sub>d \<theta>"
proof (induction S arbitrary: M)
  case (Cons x S) thus ?case by (cases x) auto
qed simp

lemma strand_sem_subst:
  assumes "(dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<union> FV\<^sub>s\<^sub>e\<^sub>t (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>)) \<inter> bvars\<^sub>s\<^sub>t S = {}"
  shows "\<lbrakk>M; S\<rbrakk>\<^sub>c (\<delta> \<circ>\<^sub>s \<theta>) \<Longrightarrow> \<lbrakk>M \<cdot>set \<delta>; S \<cdot>\<^sub>s\<^sub>t \<delta>\<rbrakk>\<^sub>c \<theta>"
using assms
proof (induction S arbitrary: \<delta> M rule: strand_sem_induct)
  case (ConsSnd M t S)
  hence "\<lbrakk>M \<cdot>set \<delta>; S \<cdot>\<^sub>s\<^sub>t \<delta>\<rbrakk>\<^sub>c \<theta>" "M \<cdot>set (\<delta> \<circ>\<^sub>s \<theta>) \<turnstile>\<^sub>c t \<cdot> (\<delta> \<circ>\<^sub>s \<theta>)" by auto
  hence "(M \<cdot>set \<delta>) \<cdot>set \<theta> \<turnstile>\<^sub>c (t \<cdot> \<delta>) \<cdot> \<theta>"
    using subst_comp_all[of \<delta> \<theta> M] subst_comp[of t \<delta> \<theta>] by simp
  thus ?case using \<open>\<lbrakk>M \<cdot>set \<delta>; S \<cdot>\<^sub>s\<^sub>t \<delta>\<rbrakk>\<^sub>c \<theta>\<close> unfolding subst_apply_strand_def by simp
next
  case (ConsRcv M t S)
  hence "\<lbrakk>(insert t M) \<cdot>set \<delta>; S \<cdot>\<^sub>s\<^sub>t \<delta>\<rbrakk>\<^sub>c \<theta>" by force
  hence "\<lbrakk>M \<cdot>set \<delta>; rcv\<langle>t \<cdot> \<delta>\<rangle>#(S \<cdot>\<^sub>s\<^sub>t \<delta>)\<rbrakk>\<^sub>c \<theta>" by (simp add: subst_all_insert)
  thus ?case by simp
next
  case (ConsIneq M X t t' S)
  hence *: "\<lbrakk>M \<cdot>set \<delta>; S \<cdot>\<^sub>s\<^sub>t \<delta>\<rbrakk>\<^sub>c \<theta>" and
        **: "\<forall>\<gamma>. dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<gamma> = set X \<and> ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<gamma>) \<longrightarrow> t \<cdot> \<gamma> \<cdot> \<delta> \<cdot> \<theta> \<noteq> t' \<cdot> \<gamma> \<cdot> \<delta> \<cdot> \<theta>" and
        ***: "(dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>) \<inter> set X = {}"
    unfolding bvars\<^sub>s\<^sub>t_def by auto
  hence "\<forall>\<gamma>. dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<gamma> = set X \<and> ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<gamma>)
          \<longrightarrow> (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>) \<inter> (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<gamma> \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<gamma>) = {}"
    by auto
  hence "\<forall>\<gamma>. dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<gamma> = set X \<and> ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<gamma>) \<longrightarrow> \<gamma> \<circ>\<^sub>s \<delta> = \<delta> \<circ>\<^sub>s \<gamma>"
    by (metis subst_comp_eq_if_disjoint_vars)
  hence "\<forall>\<gamma>. dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<gamma> = set X \<and> ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<gamma>) \<longrightarrow> t \<cdot> \<delta> \<cdot> \<gamma> \<cdot> \<theta> \<noteq> t' \<cdot> \<delta> \<cdot> \<gamma> \<cdot> \<theta>"
    using ** by (metis (no_types, hide_lams) subst_comp)
  moreover have "rm_vars (set X) \<delta> = \<delta>" using ConsIneq.prems(2) by force
  ultimately show ?case using * by auto
qed simp_all

lemma strand_sem_subst':
  assumes "(dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<union> FV\<^sub>s\<^sub>e\<^sub>t (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>)) \<inter> bvars\<^sub>s\<^sub>t S = {}"
  shows "\<lbrakk>M \<cdot>set \<delta>; S \<cdot>\<^sub>s\<^sub>t \<delta>\<rbrakk>\<^sub>c \<theta> \<Longrightarrow> \<lbrakk>M; S\<rbrakk>\<^sub>c (\<delta> \<circ>\<^sub>s \<theta>)"
using assms
proof (induction S arbitrary: \<delta> M rule: strand_sem_induct)
  case (ConsSnd M t S)
  hence "\<lbrakk>M \<cdot>set \<delta>; [snd\<langle>t\<rangle>] \<cdot>\<^sub>s\<^sub>t \<delta>\<rbrakk>\<^sub>c \<theta>" "\<lbrakk>M \<cdot>set \<delta>; S \<cdot>\<^sub>s\<^sub>t \<delta>\<rbrakk>\<^sub>c \<theta>" by auto
  hence "\<lbrakk>M; S\<rbrakk>\<^sub>c (\<delta> \<circ>\<^sub>s \<theta>)" using ConsSnd.IH[OF _] ConsSnd.prems(2) by auto
  moreover have "\<lbrakk>M; [snd\<langle>t\<rangle>]\<rbrakk>\<^sub>c (\<delta> \<circ>\<^sub>s \<theta>)"
  proof -
    have "M \<cdot>set \<delta> \<cdot>set \<theta> \<turnstile>\<^sub>c t \<cdot> \<delta> \<cdot> \<theta>" using \<open>\<lbrakk>M \<cdot>set \<delta>; [snd\<langle>t\<rangle>] \<cdot>\<^sub>s\<^sub>t \<delta>\<rbrakk>\<^sub>c \<theta>\<close> by auto
    hence "M \<cdot>set (\<delta> \<circ>\<^sub>s \<theta>) \<turnstile>\<^sub>c t \<cdot> (\<delta> \<circ>\<^sub>s \<theta>)" using subst_comp subst_comp_all by metis
    thus "\<lbrakk>M; [snd\<langle>t\<rangle>]\<rbrakk>\<^sub>c (\<delta> \<circ>\<^sub>s \<theta>)" by auto
  qed
  ultimately show ?case by auto
next
  case (ConsRcv M t S)
  hence "\<lbrakk>(insert t M) \<cdot>set \<delta>; S \<cdot>\<^sub>s\<^sub>t \<delta>\<rbrakk>\<^sub>c \<theta>" by (simp add: subst_all_insert)
  thus ?case using ConsRcv.IH ConsRcv.prems(2) by auto
next
  case (ConsIneq M X t t' S)
  have "rm_vars (set X) \<delta> = \<delta>" using ConsIneq.prems(2) by force
  hence *: "\<lbrakk>M; S\<rbrakk>\<^sub>c (\<delta> \<circ>\<^sub>s \<theta>)" and
        **: "\<forall>\<gamma>. dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<gamma> = set X \<and> ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<gamma>) \<longrightarrow> t \<cdot> \<delta> \<cdot> \<gamma> \<cdot> \<theta> \<noteq> t' \<cdot> \<delta> \<cdot> \<gamma> \<cdot> \<theta>" and
        ***: "(dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>) \<inter> set X = {}"
    using ConsIneq unfolding bvars\<^sub>s\<^sub>t_def by auto
  hence "\<forall>\<gamma>. dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<gamma> = set X \<and> ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<gamma>)
          \<longrightarrow> (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>) \<inter> (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<gamma> \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<gamma>) = {}"
    by auto
  hence "\<forall>\<gamma>. dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<gamma> = set X \<and> ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<gamma>) \<longrightarrow> \<gamma> \<circ>\<^sub>s \<delta> = \<delta> \<circ>\<^sub>s \<gamma>"
    by (metis subst_comp_eq_if_disjoint_vars)
  hence "\<forall>\<gamma>. dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<gamma> = set X \<and> ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<gamma>) \<longrightarrow> t \<cdot> \<gamma> \<cdot> \<delta> \<cdot> \<theta> \<noteq> t' \<cdot> \<gamma> \<cdot> \<delta> \<cdot> \<theta>"
    using ** by (metis (no_types, hide_lams) subst_comp)
  thus ?case using * by auto
next
  case ConsEq thus ?case unfolding bvars\<^sub>s\<^sub>t_def by auto
qed simp_all

lemma strand_sem_subst_d:
  assumes "(dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<union> FV\<^sub>s\<^sub>e\<^sub>t (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>)) \<inter> bvars\<^sub>s\<^sub>t S = {}"
  shows "\<lbrakk>M; S\<rbrakk>\<^sub>d (\<delta> \<circ>\<^sub>s \<theta>) \<Longrightarrow> \<lbrakk>M \<cdot>set \<delta>; S \<cdot>\<^sub>s\<^sub>t \<delta>\<rbrakk>\<^sub>d \<theta>"
using assms
proof (induction S arbitrary: \<delta> M rule: strand_sem_induct)
  case (ConsSnd M t S)
  hence "\<lbrakk>M \<cdot>set \<delta>; S \<cdot>\<^sub>s\<^sub>t \<delta>\<rbrakk>\<^sub>d \<theta>" "M \<cdot>set (\<delta> \<circ>\<^sub>s \<theta>) \<turnstile> t \<cdot> (\<delta> \<circ>\<^sub>s \<theta>)" by auto
  hence "(M \<cdot>set \<delta>) \<cdot>set \<theta> \<turnstile> (t \<cdot> \<delta>) \<cdot> \<theta>"
    using subst_comp_all[of \<delta> \<theta> M] subst_comp[of t \<delta> \<theta>] by simp
  thus ?case using \<open>\<lbrakk>M \<cdot>set \<delta>; S \<cdot>\<^sub>s\<^sub>t \<delta>\<rbrakk>\<^sub>d \<theta>\<close> by simp
next
  case (ConsRcv M t S)
  hence "\<lbrakk>(insert t M) \<cdot>set \<delta>; S \<cdot>\<^sub>s\<^sub>t \<delta>\<rbrakk>\<^sub>d \<theta>" by fastforce
  hence "\<lbrakk>M \<cdot>set \<delta>; rcv\<langle>t \<cdot> \<delta>\<rangle>#(S \<cdot>\<^sub>s\<^sub>t \<delta>)\<rbrakk>\<^sub>d \<theta>" by (simp add: subst_all_insert)
  thus ?case by simp
next
  case (ConsIneq M X t t' S)
  hence *: "\<lbrakk>M \<cdot>set \<delta>; S \<cdot>\<^sub>s\<^sub>t \<delta>\<rbrakk>\<^sub>d \<theta>" and
        **: "\<forall>\<gamma>. dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<gamma> = set X \<and> ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<gamma>) \<longrightarrow> t \<cdot> \<gamma> \<cdot> \<delta> \<cdot> \<theta> \<noteq> t' \<cdot> \<gamma> \<cdot> \<delta> \<cdot> \<theta>" and
        ***: "(dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>) \<inter> set X = {}"
    unfolding bvars\<^sub>s\<^sub>t_def by auto
  hence "\<forall>\<gamma>. dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<gamma> = set X \<and> ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<gamma>)
          \<longrightarrow> (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>) \<inter> (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<gamma> \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<gamma>) = {}"
    by auto
  hence "\<forall>\<gamma>. dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<gamma> = set X \<and> ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<gamma>) \<longrightarrow> \<gamma> \<circ>\<^sub>s \<delta> = \<delta> \<circ>\<^sub>s \<gamma>"
    by (metis subst_comp_eq_if_disjoint_vars)
  hence "\<forall>\<gamma>. dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<gamma> = set X \<and> ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<gamma>) \<longrightarrow> t \<cdot> \<delta> \<cdot> \<gamma> \<cdot> \<theta> \<noteq> t' \<cdot> \<delta> \<cdot> \<gamma> \<cdot> \<theta>"
    using ** by (metis (no_types, hide_lams) subst_comp)
  moreover have "rm_vars (set X) \<delta> = \<delta>" using ConsIneq.prems(2) by force
  ultimately show ?case using * by auto
next
  case ConsEq thus ?case unfolding bvars\<^sub>s\<^sub>t_def by auto
qed simp_all

lemma strand_sem_subst_d':
  assumes "(dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<union> FV\<^sub>s\<^sub>e\<^sub>t (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>)) \<inter> bvars\<^sub>s\<^sub>t S = {}"
  shows "\<lbrakk>M \<cdot>set \<delta>; S \<cdot>\<^sub>s\<^sub>t \<delta>\<rbrakk>\<^sub>d \<theta> \<Longrightarrow> \<lbrakk>M; S\<rbrakk>\<^sub>d (\<delta> \<circ>\<^sub>s \<theta>)"
using assms
proof (induction S arbitrary: \<delta> M rule: strand_sem_induct)
  case (ConsSnd M t S)
  hence "\<lbrakk>M \<cdot>set \<delta>; [snd\<langle>t\<rangle>] \<cdot>\<^sub>s\<^sub>t \<delta>\<rbrakk>\<^sub>d \<theta>" "\<lbrakk>M \<cdot>set \<delta>; S \<cdot>\<^sub>s\<^sub>t \<delta>\<rbrakk>\<^sub>d \<theta>" by auto
  hence "\<lbrakk>M; S\<rbrakk>\<^sub>d (\<delta> \<circ>\<^sub>s \<theta>)" using ConsSnd.IH[OF _] ConsSnd.prems(2) by auto
  moreover have "\<lbrakk>M; [snd\<langle>t\<rangle>]\<rbrakk>\<^sub>d (\<delta> \<circ>\<^sub>s \<theta>)"
  proof -
    have "M \<cdot>set \<delta> \<cdot>set \<theta> \<turnstile> t \<cdot> \<delta> \<cdot> \<theta>" using \<open>\<lbrakk>M \<cdot>set \<delta>; [snd\<langle>t\<rangle>] \<cdot>\<^sub>s\<^sub>t \<delta>\<rbrakk>\<^sub>d \<theta>\<close> by auto
    hence "M \<cdot>set (\<delta> \<circ>\<^sub>s \<theta>) \<turnstile> t \<cdot> (\<delta> \<circ>\<^sub>s \<theta>)" using subst_comp subst_comp_all by metis
    thus "\<lbrakk>M; [snd\<langle>t\<rangle>]\<rbrakk>\<^sub>d (\<delta> \<circ>\<^sub>s \<theta>)" by auto
  qed
  ultimately show ?case by auto
next
  case (ConsRcv M t S)
  hence "\<lbrakk>(insert t M) \<cdot>set \<delta>; S \<cdot>\<^sub>s\<^sub>t \<delta>\<rbrakk>\<^sub>d \<theta>" by (simp add: subst_all_insert)
  thus ?case using ConsRcv.IH ConsRcv.prems(2) by auto
next
  case (ConsIneq M X t t' S)
  have "rm_vars (set X) \<delta> = \<delta>" using ConsIneq.prems(2) by force
  hence *: "\<lbrakk>M; S\<rbrakk>\<^sub>d (\<delta> \<circ>\<^sub>s \<theta>)" and
        **: "\<forall>\<gamma>. dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<gamma> = set X \<and> ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<gamma>) \<longrightarrow> t \<cdot> \<delta> \<cdot> \<gamma> \<cdot> \<theta> \<noteq> t' \<cdot> \<delta> \<cdot> \<gamma> \<cdot> \<theta>" and
        ***: "(dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>) \<inter> set X = {}"
    using ConsIneq by auto
  hence "\<forall>\<gamma>. dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<gamma> = set X \<and> ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<gamma>)
          \<longrightarrow> (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>) \<inter> (dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<gamma> \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<gamma>) = {}"
    by auto
  hence "\<forall>\<gamma>. dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<gamma> = set X \<and> ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<gamma>) \<longrightarrow> \<gamma> \<circ>\<^sub>s \<delta> = \<delta> \<circ>\<^sub>s \<gamma>"
    by (metis subst_comp_eq_if_disjoint_vars)
  hence "\<forall>\<gamma>. dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<gamma> = set X \<and> ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<gamma>) \<longrightarrow> t \<cdot> \<gamma> \<cdot> \<delta> \<cdot> \<theta> \<noteq> t' \<cdot> \<gamma> \<cdot> \<delta> \<cdot> \<theta>"
    using ** by (metis (no_types, hide_lams) subst_comp)
  thus ?case using * by auto
next
  case ConsEq thus ?case unfolding bvars\<^sub>s\<^sub>t_def by auto
qed simp_all

lemma strand_sem_subst_Idem:
  assumes "(dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<union> FV\<^sub>s\<^sub>e\<^sub>t (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>)) \<inter> bvars\<^sub>s\<^sub>t S = {}"
  shows "\<lbrakk>\<lbrakk>M \<cdot>set \<delta>; S \<cdot>\<^sub>s\<^sub>t \<delta>\<rbrakk>\<^sub>c (\<delta> \<circ>\<^sub>s \<theta>); Idem \<delta>\<rbrakk> \<Longrightarrow> \<lbrakk>M; S\<rbrakk>\<^sub>c (\<delta> \<circ>\<^sub>s \<theta>)"
apply (induct "S \<cdot>\<^sub>s\<^sub>t \<delta>" rule: strand_sem_c.induct)
by (metis Idem_def comp_assoc strand_sem_subst'[OF assms])+

lemma strand_sem_subst_comp:
  assumes "(dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<union> FV\<^sub>s\<^sub>e\<^sub>t (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>)) \<inter> bvars\<^sub>s\<^sub>t S = {}"
  and "\<lbrakk>M; S\<rbrakk>\<^sub>c \<delta>" "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<inter> (vars\<^sub>s\<^sub>t S \<union> FV\<^sub>s\<^sub>e\<^sub>t M) = {}"
  shows "\<lbrakk>M; S\<rbrakk>\<^sub>c (\<theta> \<circ>\<^sub>s \<delta>)"
proof -
  from assms(3) have "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<inter> vars\<^sub>s\<^sub>t S = {}" "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<inter> FV\<^sub>s\<^sub>e\<^sub>t M = {}" by auto
  hence "S \<cdot>\<^sub>s\<^sub>t \<theta> = S" "M \<cdot>set \<theta> = M" using strand_substI set_subst_ident[of M \<theta>] by (blast, blast)
  thus ?thesis using assms(2) by (auto simp add: strand_sem_subst'[OF assms(1)])
qed

lemma strand_sem_d_imp_ineqs_neq:
  assumes "\<lbrakk>M; S\<rbrakk>\<^sub>d \<I>" "\<nexists>X\<langle>t \<doteq> t'\<rangle> \<in> set S"
  shows "t \<noteq> t'"
using assms
proof (induction rule: strand_sem_induct)
  case (ConsIneq M Y s s' S) thus ?case
  proof (cases "\<nexists>X\<langle>t \<doteq> t'\<rangle> \<in> set S")
    case False
    hence "X = Y" "t = s" "t' = s'" using ConsIneq by auto
    hence "\<forall>\<theta>. dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> = set X \<and> ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>) \<longrightarrow> t \<cdot> \<theta> \<cdot> \<I> \<noteq> t' \<cdot> \<theta> \<cdot> \<I>"
      using ConsIneq by auto
    then obtain \<theta> where "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> = set X" "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>)" "t \<cdot> \<theta> \<cdot> \<I> \<noteq> t' \<cdot> \<theta> \<cdot> \<I>"
      using interpretation_subst_exists'[of "set X"] by moura
    thus ?thesis by auto
  qed simp
qed simp_all

lemma strand_sem_c_imp_ineqs_neq:
  assumes "\<lbrakk>M; S\<rbrakk>\<^sub>c \<I>" "\<nexists>X\<langle>t \<doteq> t'\<rangle> \<in> set S"
  shows "t \<noteq> t' \<and> (\<forall>\<delta>. 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> \<noteq> t' \<cdot> \<delta> \<and> t \<cdot> \<delta> \<cdot> \<I> \<noteq> t' \<cdot> \<delta> \<cdot> \<I>)"
using assms
proof (induction rule: strand_sem_induct)
  case (ConsIneq M Y s s' S) thus ?case
  proof (cases "\<nexists>X\<langle>t \<doteq> t'\<rangle> \<in> set S")
    case False
    hence "X = Y" "t = s" "t' = s'" using ConsIneq by auto
    hence *: "\<forall>\<theta>. dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> = set X \<and> ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>) \<longrightarrow> t \<cdot> \<theta> \<cdot> \<I> \<noteq> t' \<cdot> \<theta> \<cdot> \<I>"
      using ConsIneq by auto
    then obtain \<theta> where \<theta>: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> = set X" "ground (img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>)" "t \<cdot> \<theta> \<cdot> \<I> \<noteq> t' \<cdot> \<theta> \<cdot> \<I>"
      using interpretation_subst_exists'[of "set X"] by moura
    hence "t \<noteq> t'" by auto
    moreover have "\<And>\<I> \<theta>. t \<cdot> \<theta> \<cdot> \<I> \<noteq> t' \<cdot> \<theta> \<cdot> \<I> \<Longrightarrow> t \<cdot> \<theta> \<noteq> t' \<cdot> \<theta>" by auto
    ultimately show ?thesis using * by auto
  qed simp
qed simp_all

lemma strand_sem_snd_map:
  assumes "\<And>t. t \<in> set X \<Longrightarrow> \<lbrakk>M; [snd\<langle>t\<rangle>]\<rbrakk>\<^sub>c \<I>"
  shows "\<lbrakk>M; map Send X\<rbrakk>\<^sub>c \<I>"
using assms by (induct X) auto

lemma strand_sem_snd_map_d:
  assumes "\<And>t. t \<in> set X \<Longrightarrow> \<lbrakk>M; [snd\<langle>t\<rangle>]\<rbrakk>\<^sub>d \<I>"
  shows "\<lbrakk>M; map Send X\<rbrakk>\<^sub>d \<I>"
using assms by (induct X) auto

lemma strand_sem_rcv_map: "\<lbrakk>M; map Receive X\<rbrakk>\<^sub>c \<I>" by (induct X arbitrary: M) auto

lemma strand_sem_rcv_map_d: "\<lbrakk>M; map Receive X\<rbrakk>\<^sub>d \<I>" by (induct X arbitrary: M) auto

lemma strand_sem_wf_simple_FV_sat:
  assumes "wf\<^sub>s\<^sub>t {} S" "simple S" "\<lbrakk>{}; S\<rbrakk>\<^sub>c \<I>"
  shows "\<And>v. v \<in> vars2\<^sub>s\<^sub>t S \<Longrightarrow> ik\<^sub>s\<^sub>t S \<cdot>set \<I> \<turnstile>\<^sub>c \<I> v"
using assms
proof (induction S rule: wf\<^sub>s\<^sub>t_simple_induct)
  case (ConsRcv t S)
  hence "v \<in> vars2\<^sub>s\<^sub>t S" by fastforce
  moreover have "\<lbrakk>{}; S\<rbrakk>\<^sub>c \<I>" using \<open>\<lbrakk>{}; S@[rcv\<langle>t\<rangle>]\<rbrakk>\<^sub>c \<I>\<close> by blast
  moreover have "ik\<^sub>s\<^sub>t S \<cdot>set \<I> \<subseteq> ik\<^sub>s\<^sub>t (S@[rcv\<langle>t\<rangle>]) \<cdot>set \<I>" by auto
  ultimately show ?case using ConsRcv.IH ideduct_synth_mono by meson
next
  case (ConsIneq X t t' S)
  hence "v \<in> vars2\<^sub>s\<^sub>t S" by fastforce
  moreover have "\<lbrakk>{}; S\<rbrakk>\<^sub>c \<I>" using \<open>\<lbrakk>{}; S@[\<nexists>X\<langle>t \<doteq> t'\<rangle>]\<rbrakk>\<^sub>c \<I>\<close> by blast
  moreover have "ik\<^sub>s\<^sub>t S \<cdot>set \<I> \<subseteq> ik\<^sub>s\<^sub>t (S@[\<nexists>X\<langle>t \<doteq> t'\<rangle>]) \<cdot>set \<I>" by auto
  ultimately show ?case using ConsIneq.IH ideduct_synth_mono by meson
next
  case (ConsSnd w S)
  hence *: "\<lbrakk>{}; S\<rbrakk>\<^sub>c \<I>" "ik\<^sub>s\<^sub>t S \<cdot>set \<I> \<turnstile>\<^sub>c \<I> w" by auto
  have **: "ik\<^sub>s\<^sub>t S \<cdot>set \<I> \<subseteq> ik\<^sub>s\<^sub>t (S@[snd\<langle>Var w\<rangle>]) \<cdot>set \<I>" by simp
  show ?case
  proof (cases "v = w")
    case True thus ?thesis using *(2) ideduct_synth_mono[OF _ **] by meson
  next
    case False
    hence "v \<in> vars2\<^sub>s\<^sub>t S" using ConsSnd.prems(1) by auto
    thus ?thesis using ConsSnd.IH[OF _ *(1)] ideduct_synth_mono[OF _ **] by metis
  qed
qed simp

lemma strand_sem_wf_ik_or_eqs_rhs_fun_subterm:
  assumes "wf\<^sub>s\<^sub>t {} A" "\<lbrakk>{}; A\<rbrakk>\<^sub>c \<I>" "Var x \<in> ik\<^sub>s\<^sub>t A" "\<I> x = Fun f T"
          "t\<^sub>i \<in> set T" "\<not>ik\<^sub>s\<^sub>t A \<cdot>set \<I> \<turnstile>\<^sub>c t\<^sub>i" "interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>"
  obtains S where
    "Fun f S \<in> \<Union>(subterms ` ik\<^sub>s\<^sub>t A) \<or> Fun f S \<in> \<Union>(subterms ` eqs_rhs\<^sub>s\<^sub>t A)"
    "Fun f T = Fun f S \<cdot> \<I>"
proof -
  have "x \<in> vars2\<^sub>s\<^sub>t A" using assms(3) vars_iff_subterm_or_eq by force
  moreover have "Fun f T \<cdot> \<I> = Fun f T"
    by (metis subst_ground_ident interpretation_grounds_all assms(4,7))
  ultimately obtain A\<^sub>p\<^sub>r\<^sub>e A\<^sub>s\<^sub>u\<^sub>f where *:
      "\<not>(\<exists>w \<in> vars2\<^sub>s\<^sub>t A\<^sub>p\<^sub>r\<^sub>e. Fun f T \<sqsubseteq> \<I> w)"
      "(\<exists>t. A = A\<^sub>p\<^sub>r\<^sub>e@snd\<langle>t\<rangle>#A\<^sub>s\<^sub>u\<^sub>f \<and> Fun f T \<sqsubseteq> t \<cdot> \<I>) \<or>
        (\<exists>t t'. A = A\<^sub>p\<^sub>r\<^sub>e@t \<doteq> t'#A\<^sub>s\<^sub>u\<^sub>f \<and> Fun f T \<sqsubseteq> t \<cdot> \<I>)"
    using wf_strand_first_snd_var_split[OF assms(1)] assms(4) subtermeqI' by metis
  moreover
  { fix t assume **: "A = A\<^sub>p\<^sub>r\<^sub>e@snd\<langle>t\<rangle>#A\<^sub>s\<^sub>u\<^sub>f" "Fun f T \<sqsubseteq> t \<cdot> \<I>"
    hence "ik\<^sub>s\<^sub>t A\<^sub>p\<^sub>r\<^sub>e \<cdot>set \<I> \<turnstile>\<^sub>c t \<cdot> \<I>" "\<not>ik\<^sub>s\<^sub>t A\<^sub>p\<^sub>r\<^sub>e \<cdot>set \<I> \<turnstile>\<^sub>c t\<^sub>i"
      using assms(2,6) by (auto intro: ideduct_synth_mono)
    then obtain s where s: "s \<in> ik\<^sub>s\<^sub>t A\<^sub>p\<^sub>r\<^sub>e" "Fun f T \<sqsubseteq> s \<cdot> \<I>"
      using assms(5) **(2) by (induct rule: intruder_synth_induct) auto
    then obtain g S where gS: "Fun g S \<sqsubseteq> s" "Fun f T = Fun g S \<cdot> \<I>"
      using subterm_subst_not_img_subterm[OF s(2)] *(1) by force
    hence ?thesis using that **(1) s(1) by force
  }
  moreover
  { fix t t' assume **: "A = A\<^sub>p\<^sub>r\<^sub>e@t \<doteq> t'#A\<^sub>s\<^sub>u\<^sub>f" "Fun f T \<sqsubseteq> t \<cdot> \<I>"
    with assms(2) have "t \<cdot> \<I> = t' \<cdot> \<I>" by auto
    hence "Fun f T \<sqsubseteq> t' \<cdot> \<I>" using **(2) by auto
    from assms(1) **(1) have "FV t' \<subseteq> vars2\<^sub>s\<^sub>t A\<^sub>p\<^sub>r\<^sub>e"
      using wf_eq_FV[of "{}" A\<^sub>p\<^sub>r\<^sub>e t t' A\<^sub>s\<^sub>u\<^sub>f] vars_snd_rcv_strand_subset2(4)[of A\<^sub>p\<^sub>r\<^sub>e]
      by auto
    then obtain g S where gS: "Fun g S \<sqsubseteq> t'" "Fun f T = Fun g S \<cdot> \<I>"
      using subterm_subst_not_img_subterm[OF \<open>Fun f T \<sqsubseteq> t' \<cdot> \<I>\<close>] *(1) by fastforce
    hence ?thesis using that **(1) by auto
  }
  ultimately show ?thesis by auto
qed


subsection {* Constraint Semantics (slightly modified and equivalent version) *}
fun strand_sem_c'::"('fun,'var) terms \<Rightarrow> ('fun,'var) strand \<Rightarrow> ('fun,'var) constrsem" ("\<lbrakk>_; _\<rbrakk>\<^sub>c'")
where
  "\<lbrakk>M; []\<rbrakk>\<^sub>c' = (\<lambda>\<I>. True)"
| "\<lbrakk>M; snd\<langle>t\<rangle>#S\<rbrakk>\<^sub>c' = (\<lambda>\<I>. M \<turnstile>\<^sub>c t \<cdot> \<I> \<and> \<lbrakk>M; S\<rbrakk>\<^sub>c' \<I>)"
| "\<lbrakk>M; rcv\<langle>t\<rangle>#S\<rbrakk>\<^sub>c' = (\<lambda>\<I>. \<lbrakk>insert (t \<cdot> \<I>) M; S\<rbrakk>\<^sub>c' \<I>)"
| "\<lbrakk>M; t \<doteq> t'#S\<rbrakk>\<^sub>c' = (\<lambda>\<I>. t \<cdot> \<I> = t' \<cdot> \<I> \<and> \<lbrakk>M; S\<rbrakk>\<^sub>c' \<I>)"
| "\<lbrakk>M; \<nexists>X\<langle>t \<doteq> t'\<rangle>#S\<rbrakk>\<^sub>c' =
        (\<lambda>\<I>. (\<forall>\<delta>. 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>) \<and> \<lbrakk>M; S\<rbrakk>\<^sub>c' \<I>)"

fun strand_sem_d'::"('fun,'var) terms \<Rightarrow> ('fun,'var) strand \<Rightarrow> ('fun,'var) constrsem" ("\<lbrakk>_; _\<rbrakk>\<^sub>d'")
where
  "\<lbrakk>M; []\<rbrakk>\<^sub>d' = (\<lambda>\<I>. True)"
| "\<lbrakk>M; snd\<langle>t\<rangle>#S\<rbrakk>\<^sub>d' = (\<lambda>\<I>. M \<turnstile> t \<cdot> \<I> \<and> \<lbrakk>M; S\<rbrakk>\<^sub>d' \<I>)"
| "\<lbrakk>M; rcv\<langle>t\<rangle>#S\<rbrakk>\<^sub>d' = (\<lambda>\<I>. \<lbrakk>insert (t \<cdot> \<I>) M; S\<rbrakk>\<^sub>d' \<I>)"
| "\<lbrakk>M; t \<doteq> t'#S\<rbrakk>\<^sub>d' = (\<lambda>\<I>. t \<cdot> \<I> = t' \<cdot> \<I> \<and> \<lbrakk>M; S\<rbrakk>\<^sub>d' \<I>)"
| "\<lbrakk>M; \<nexists>X\<langle>t \<doteq> t'\<rangle>#S\<rbrakk>\<^sub>d' =
        (\<lambda>\<I>. (\<forall>\<delta>. 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>) \<and> \<lbrakk>M; S\<rbrakk>\<^sub>d' \<I>)"

lemma strand_sem_eq_defs:
  "\<lbrakk>M; \<A>\<rbrakk>\<^sub>c \<I> = \<lbrakk>M \<cdot>set \<I>; \<A>\<rbrakk>\<^sub>c' \<I>"
  "\<lbrakk>M; \<A>\<rbrakk>\<^sub>d \<I> = \<lbrakk>M \<cdot>set \<I>; \<A>\<rbrakk>\<^sub>d' \<I>"
proof -
  have 1: "\<lbrakk>M; \<A>\<rbrakk>\<^sub>c \<I> \<Longrightarrow> \<lbrakk>M \<cdot>set \<I>; \<A>\<rbrakk>\<^sub>c' \<I>"
    by (induct \<A> arbitrary: M rule: strand_sem_induct) force+
  have 2: "\<lbrakk>M \<cdot>set \<I>; \<A>\<rbrakk>\<^sub>c' \<I> \<Longrightarrow> \<lbrakk>M; \<A>\<rbrakk>\<^sub>c \<I>"
    by (induct \<A> arbitrary: M rule: strand_sem_c'.induct) auto
  have 3: "\<lbrakk>M; \<A>\<rbrakk>\<^sub>d \<I> \<Longrightarrow> \<lbrakk>M \<cdot>set \<I>; \<A>\<rbrakk>\<^sub>d' \<I>"
    by (induct \<A> arbitrary: M rule: strand_sem_induct) force+
  have 4: "\<lbrakk>M \<cdot>set \<I>; \<A>\<rbrakk>\<^sub>d' \<I> \<Longrightarrow> \<lbrakk>M; \<A>\<rbrakk>\<^sub>d \<I>"
    by (induct \<A> arbitrary: M rule: strand_sem_d'.induct) auto

  show "\<lbrakk>M; \<A>\<rbrakk>\<^sub>c \<I> = \<lbrakk>M \<cdot>set \<I>; \<A>\<rbrakk>\<^sub>c' \<I>" "\<lbrakk>M; \<A>\<rbrakk>\<^sub>d \<I> = \<lbrakk>M \<cdot>set \<I>; \<A>\<rbrakk>\<^sub>d' \<I>"
    by (metis 1 2, metis 3 4)
qed

end

end