Theory Strands_and_Constraints

(*  Title:      Strands_and_Constraints.thy
    Author:     Andreas Viktor Hess, DTU
    SPDX-License-Identifier: BSD-3-Clause
*)

section ‹Strands and Symbolic Intruder Constraints›
theory Strands_and_Constraints
imports Messages More_Unification Intruder_Deduction
begin

subsection ‹Constraints, Strands and Related Definitions›
datatype poscheckvariant = Assign (‹assign›) | Check (‹check›)

text ‹
  A strand (or constraint) step is either a message transmission (either a message being sent ‹Send›
  or being received ‹Receive›) or a check on messages (a positive check ‹Equality›---which can be
  either an "assignment" or just a check---or a negative check ‹Inequality›)
›
datatype (funsstp: 'a, varsstp: 'b) strand_step =
  Send       "('a,'b) term list" (‹send⟨_⟩st› 80)
| Receive    "('a,'b) term list" (‹receive⟨_⟩st› 80)
| Equality   poscheckvariant "('a,'b) term" "('a,'b) term" (‹⟨_: _ ≐ _⟩st› [80,80])
| Inequality (bvarsstp: "'b list") "(('a,'b) term × ('a,'b) term) list" (‹∀_⟨∨≠: _⟩st› [80,80])
where
  "bvarsstp (Send _) = []"
| "bvarsstp (Receive _) = []"
| "bvarsstp (Equality _ _ _) = []"

abbreviation "Send1 t ≡ Send [t]"
abbreviation "Receive1 t ≡ Receive [t]"

text ‹
  A strand is a finite sequence of strand steps (constraints and strands share the same datatype)
›
type_synonym ('a,'b) strand = "('a,'b) strand_step list"

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

abbreviation "trmspairs F ≡ ⋃(t,t') ∈ set F. {t,t'}"

fun trmsstp::"('a,'b) strand_step ⇒ ('a,'b) terms" where
  "trmsstp (Send ts) = set ts"
| "trmsstp (Receive ts) = set ts"
| "trmsstp (Equality _ t t') = {t,t'}"
| "trmsstp (Inequality _ F) = trmspairs F"

lemma varsstp_unfold[simp]: "varsstp x = fvset (trmsstp x) ∪ set (bvarsstp x)"
by (cases x) auto

text ‹The set of terms occurring in a strand›
definition trmsst where "trmsst S ≡ ⋃(trmsstp ` set S)"

fun trms_liststp::"('a,'b) strand_step ⇒ ('a,'b) term list" where
  "trms_liststp (Send ts) = ts"
| "trms_liststp (Receive ts) = ts"
| "trms_liststp (Equality _ t t') = [t,t']"
| "trms_liststp (Inequality _ F) = concat (map (λ(t,t'). [t,t']) F)"

text ‹The set of terms occurring in a strand (list variant)›
definition trms_listst where "trms_listst S ≡ remdups (concat (map trms_liststp S))"

text ‹The set of variables occurring in a sent message›
definition fvsnd::"('a,'b) strand_step ⇒ 'b set" where
  "fvsnd x ≡ case x of Send t ⇒ fvset (set t) | _ ⇒ {}"

text ‹The set of variables occurring in a received message›
definition fvrcv::"('a,'b) strand_step ⇒ 'b set" where
  "fvrcv x ≡ case x of Receive t ⇒ fvset (set t) | _ ⇒ {}"

text ‹The set of variables occurring in an equality constraint›
definition fveq::"poscheckvariant ⇒ ('a,'b) strand_step ⇒ 'b set" where
  "fveq ac x ≡ case x of Equality ac' s t ⇒ if ac = ac' then fv s ∪ fv t else {} | _ ⇒ {}"

text ‹The set of variables occurring at the left-hand side of an equality constraint›
definition fv_leq::"poscheckvariant ⇒ ('a,'b) strand_step ⇒ 'b set" where
  "fv_leq ac x ≡ case x of Equality ac' s t ⇒ if ac = ac' then fv s else {} | _ ⇒ {}"

text ‹The set of variables occurring at the right-hand side of an equality constraint›
definition fv_req::"poscheckvariant ⇒ ('a,'b) strand_step ⇒ 'b set" where
  "fv_req ac x ≡ case x of Equality ac' s t ⇒ if ac = ac' then fv t else {} | _ ⇒ {}"

text ‹The free variables of inequality constraints›
definition fvineq::"('a,'b) strand_step ⇒ 'b set" where
  "fvineq x ≡ case x of Inequality X F ⇒ fvpairs F - set X | _ ⇒ {}"

fun fvstp::"('a,'b) strand_step ⇒ 'b set" where
  "fvstp (Send t) = fvset (set t)"
| "fvstp (Receive t) = fvset (set t)"
| "fvstp (Equality _ t t') = fv t ∪ fv t'"
| "fvstp (Inequality X F) = (⋃(t,t') ∈ set F. fv t ∪ fv t') - set X"

text ‹The set of free variables of a strand›
definition fvst::"('a,'b) strand ⇒ 'b set" where
  "fvst S ≡ ⋃(set (map fvstp S))"

text ‹The set of bound variables of a strand›
definition bvarsst::"('a,'b) strand ⇒ 'b set" where
  "bvarsst S ≡ ⋃(set (map (set ∘ bvarsstp) S))"

text ‹The set of all variables occurring in a strand›
definition varsst::"('a,'b) strand ⇒ 'b set" where
  "varsst S ≡ ⋃(set (map varsstp S))"

abbreviation wfrestrictedvarsstp::"('a,'b) strand_step ⇒ 'b set" where
  "wfrestrictedvarsstp x ≡
    case x of Inequality _ _ ⇒ {} | Equality Check _ _ ⇒ {} | _ ⇒ varsstp x"

text ‹The variables of a strand whose occurrences might be restricted by well-formedness constraints›
definition wfrestrictedvarsst::"('a,'b) strand ⇒ 'b set" where
  "wfrestrictedvarsst S ≡ ⋃(set (map wfrestrictedvarsstp S))"

abbreviation wfvarsoccsstp where
  "wfvarsoccsstp x ≡ case x of Send t ⇒ fvset (set t) | Equality Assign s t ⇒ fv s | _ ⇒ {}"

text ‹The variables of a strand that occur in sent messages or in assignments›
definition wfvarsoccsst where
  "wfvarsoccsst S ≡ ⋃(set (map wfvarsoccsstp S))"

text ‹The variables occurring at the right-hand side of assignment steps›
fun assignment_rhsst where
  "assignment_rhsst [] = {}"
| "assignment_rhsst (Equality Assign t t'#S) = insert t' (assignment_rhsst S)"
| "assignment_rhsst (x#S) = assignment_rhsst S"

text ‹The set of function symbols occurring in a strand›
definition funsst::"('a,'b) strand ⇒ 'a set" where
  "funsst S ≡ ⋃(set (map funsstp S))"

fun subst_apply_strand_step::"('a,'b) strand_step ⇒ ('a,'b) subst ⇒ ('a,'b) strand_step"
  (infix ‹⋅stp› 51) where
  "Send t ⋅stp θ = Send (t ⋅list θ)"
| "Receive t ⋅stp θ = Receive (t ⋅list θ)"
| "Equality a t t' ⋅stp θ = Equality a (t ⋅ θ) (t' ⋅ θ)"
| "Inequality X F ⋅stp θ = Inequality X (F ⋅pairs rm_vars (set X) θ)"

text ‹Substitution application for strands›
definition subst_apply_strand::"('a,'b) strand ⇒ ('a,'b) subst ⇒ ('a,'b) strand"
  (infix ‹⋅st› 51) where
  "S ⋅st θ ≡ map (λx. x ⋅stp θ) S"

text ‹The semantics of inequality constraints›
definition
  "ineq_model (ℐ::('a,'b) subst) X F ≡
      (∀δ. subst_domain δ = set X ∧ ground (subst_range δ) ⟶ 
              (∃(t,t') ∈ set F. t ⋅ δ ∘s ℐ ≠ t' ⋅ δ ∘s ℐ))"

fun simplestp where
  "simplestp (Receive t) = True"
| "simplestp (Send [Var v]) = True"
| "simplestp (Inequality X F) = (∃ℐ. ineq_model ℐ X F)"
| "simplestp _ = False"

text ‹Simple constraints›
definition simple where "simple S ≡ list_all simplestp S"

text ‹The intruder knowledge of a constraint›
fun ikst::"('a,'b) strand ⇒ ('a,'b) terms" where
  "ikst [] = {}"
| "ikst (Receive t#S) = set t ∪ (ikst S)"
| "ikst (_#S) = ikst S"

text ‹Strand well-formedness›
fun wfst::"'b set ⇒ ('a,'b) strand ⇒ bool" where
  "wfst V [] = True"
| "wfst V (Receive ts#S) = (fvset (set ts) ⊆ V ∧ wfst V S)"
| "wfst V (Send ts#S) = wfst (V ∪ fvset (set ts)) S"
| "wfst V (Equality Assign s t#S) = (fv t ⊆ V ∧ wfst (V ∪ fv s) S)"
| "wfst V (Equality Check s t#S) = wfst V S"
| "wfst V (Inequality _ _#S) = wfst V S"

text ‹Well-formedness of constraint states›
definition wfconstr::"('a,'b) strand ⇒ ('a,'b) subst ⇒ bool" where
  "wfconstr S θ ≡ (wfsubst θ ∧ wfst {} S ∧ subst_domain θ ∩ varsst S = {} ∧
                  range_vars θ ∩ bvarsst S = {} ∧ fvst S ∩ bvarsst S = {})"

declare trmsst_def[simp]
declare fvsnd_def[simp]
declare fvrcv_def[simp]
declare fveq_def[simp]
declare fv_leq_def[simp]
declare fv_req_def[simp]
declare fvineq_def[simp]
declare fvst_def[simp]
declare varsst_def[simp]
declare bvarsst_def[simp]
declare wfrestrictedvarsst_def[simp]
declare wfvarsoccsst_def[simp]

lemmas wfst_induct = wfst.induct[case_names Nil ConsRcv ConsSnd ConsEq ConsEq2 ConsIneq]
lemmas ikst_induct = ikst.induct[case_names Nil ConsRcv ConsSnd ConsEq ConsIneq]
lemmas assignment_rhsst_induct = assignment_rhsst.induct[case_names Nil ConsEq2 ConsSnd ConsRcv ConsEq ConsIneq]
  

subsubsection ‹Lexicographical measure on strands›
definition sizest::"('a,'b) strand ⇒ nat" where
  "sizest S ≡ size_list (λx. Max (insert 0 (size ` trmsstp x))) S"

definition measurest::"((('a, 'b) strand × ('a,'b) subst) × ('a, 'b) strand × ('a,'b) subst) set"
where
  "measurest ≡ measures [λ(S,θ). card (fvst S), λ(S,θ). sizest S]"

lemma measurest_alt_def:
  "((s,x),(t,y)) ∈ measurest =
      (card (fvst s) < card (fvst t) ∨ (card (fvst s) = card (fvst t) ∧ sizest s < sizest t))"
by (simp add: measurest_def sizest_def)

lemma measurest_trans: "trans measurest"
by (simp add: trans_def measurest_def sizest_def)


subsubsection ‹Some lemmata›
lemma trms_listst_is_trmsst: "trmsst S = set (trms_listst S)"
unfolding trmsst_def trms_listst_def
proof (induction S)
  case (Cons x S) thus ?case by (cases x) auto
qed simp

lemma subst_apply_strand_step_def:
  "s ⋅stp θ = (case s of
    Send t ⇒ Send (t ⋅list θ)
  | Receive t ⇒ Receive (t ⋅list θ)
  | Equality a t t' ⇒ Equality a (t ⋅ θ) (t' ⋅ θ)
  | Inequality X F ⇒ Inequality X (F ⋅pairs rm_vars (set X) θ))"
by (cases s) simp_all

lemma subst_apply_strand_nil[simp]: "[] ⋅st δ = []"
unfolding subst_apply_strand_def by simp

lemma finite_funsstp[simp]: "finite (funsstp x)" by (cases x) auto
lemma finite_funsst[simp]: "finite (funsst S)" unfolding funsst_def by simp
lemma finite_trmspairs[simp]: "finite (trmspairs x)" by (induct x) auto
lemma finite_trmsstp[simp]: "finite (trmsstp x)" by (cases x) auto
lemma finite_varsstp[simp]: "finite (varsstp x)" by auto
lemma finite_bvarsstp[simp]: "finite (set (bvarsstp x))" by rule
lemma finite_fvsnd[simp]: "finite (fvsnd x)" by (cases x) auto
lemma finite_fvrcv[simp]: "finite (fvrcv x)" by (cases x) auto
lemma finite_fvstp[simp]: "finite (fvstp x)" by (cases x) auto
lemma finite_varsst[simp]: "finite (varsst S)" by simp
lemma finite_bvarsst[simp]: "finite (bvarsst S)" by simp
lemma finite_fvst[simp]: "finite (fvst S)" by simp

lemma finite_wfrestrictedvarsstp[simp]: "finite (wfrestrictedvarsstp x)"
by (cases x) (auto split: poscheckvariant.splits)

lemma finite_wfrestrictedvarsst[simp]: "finite (wfrestrictedvarsst S)"
using finite_wfrestrictedvarsstp by auto

lemma finite_wfvarsoccsstp[simp]: "finite (wfvarsoccsstp x)"
by (cases x) (auto split: poscheckvariant.splits)

lemma finite_wfvarsoccsst[simp]: "finite (wfvarsoccsst S)"
using finite_wfvarsoccsstp by auto

lemma finite_ikst[simp]: "finite (ikst S)"
by (induct S rule: ikst.induct) simp_all

lemma finite_assignment_rhsst[simp]: "finite (assignment_rhsst S)"
by (induct S rule: assignment_rhsst.induct) simp_all

lemma ikst_is_rcv_set: "ikst A = {t | ts t. Receive ts ∈ set A ∧ t ∈ set ts}"
by (induct A rule: ikst.induct) auto

lemma ikst_snoc_no_receive_eq:
  assumes "∄ts. a = receive⟨ts⟩st"
  shows "ikst (A@[a]) ⋅set ℐ = ikst A ⋅set ℐ"
using assms unfolding ikst_is_rcv_set
by (metis (no_types, lifting) Un_iff append_Nil2 set_ConsD set_append)

lemma ikstD[dest]: "t ∈ ikst S ⟹ ∃ts. t ∈ set ts ∧ Receive ts ∈ set S"
by (induct S rule: ikst.induct) auto

lemma ikstD'[dest]: "t ∈ ikst S ⟹ t ∈ trmsst S"
by (induct S rule: ikst.induct) auto

lemma ikstD''[dest]: "t ∈ subtermsset (ikst S) ⟹ t ∈ subtermsset (trmsst S)"
by (induct S rule: ikst.induct) auto

lemma ikst_subterm_exD:
  assumes "t ∈ ikst S"
  shows "∃x ∈ set S. t ∈ subtermsset (trmsstp x)"
using assms ikstD by force

lemma assignment_rhsstD[dest]: "t ∈ assignment_rhsst S ⟹ ∃t'. Equality Assign t' t ∈ set S"
by (induct S rule: assignment_rhsst.induct) auto

lemma assignment_rhsstD'[dest]: "t ∈ subtermsset (assignment_rhsst S) ⟹ t ∈ subtermsset (trmsst S)"
by (induct S rule: assignment_rhsst.induct) auto

lemma bvarsst_split: "bvarsst (S@S') = bvarsst S ∪ bvarsst S'"
unfolding bvarsst_def by auto

lemma bvarsst_singleton: "bvarsst [x] = set (bvarsstp x)"
unfolding bvarsst_def by auto

lemma strand_fv_bvars_disjointD:
  assumes "fvst S ∩ bvarsst S = {}" "Inequality X F ∈ set S"
  shows "set X ⊆ bvarsst S" "fvpairs F - set X ⊆ fvst S"
using assms by (induct S) fastforce+

lemma strand_fv_bvars_disjoint_unfold:
  assumes "fvst S ∩ bvarsst S = {}" "Inequality X F ∈ set S" "Inequality Y G ∈ set S"
  shows "set Y ∩ (fvpairs F - set X) = {}"
proof -
  have "set X ⊆ bvarsst S" "set Y ⊆ bvarsst S"
       "fvpairs F - set X ⊆ fvst S" "fvpairs G - set Y ⊆ fvst S"
    using strand_fv_bvars_disjointD[OF assms(1)] assms(2,3) by auto
  thus ?thesis using assms(1) by fastforce
qed

lemma strand_subst_hom[iff]:
  "(S@S') ⋅st θ = (S ⋅st θ)@(S' ⋅st θ)" "(x#S) ⋅st θ = (x ⋅stp θ)#(S ⋅st θ)"
unfolding subst_apply_strand_def by auto

lemma strand_subst_comp: "range_vars δ ∩ bvarsst S = {} ⟹ S ⋅st δ ∘s θ = ((S ⋅st δ) ⋅st θ)"
proof (induction S)
  case (Cons x S)
  have *: "range_vars δ ∩ bvarsst S = {}" "range_vars δ ∩ (set (bvarsstp x)) = {}"
    using Cons bvarsst_split[of "[x]" S] append_Cons inf_sup_absorb
    by (metis (no_types, lifting) Int_iff Un_commute disjoint_iff_not_equal self_append_conv2,
        metis append_self_conv2 bvarsst_singleton inf_bot_right inf_left_commute) 
  hence IH: "S ⋅st δ ∘s θ = (S ⋅st δ) ⋅st θ" using Cons.IH by auto
  have "(x#S ⋅st δ ∘s θ) = (x ⋅stp δ ∘s θ)#(S ⋅st δ ∘s θ)" by (metis strand_subst_hom(2))
  hence "... = (x ⋅stp δ ∘s θ)#((S ⋅st δ) ⋅st θ)" by (metis IH)
  hence "... = ((x ⋅stp δ) ⋅stp θ)#((S ⋅st δ) ⋅st θ)" using rm_vars_comp[OF *(2)]
  proof (induction x)
    case (Inequality X F) thus ?case
      by (induct F) (auto simp add: subst_apply_pairs_def subst_apply_strand_step_def)
  qed (simp_all add: subst_apply_strand_step_def)
  thus ?case using IH by auto
qed (simp add: subst_apply_strand_def)

lemma strand_substI[intro]:
  "subst_domain θ ∩ fvst S = {} ⟹ S ⋅st θ = S"
  "subst_domain θ ∩ varsst S = {} ⟹ S ⋅st θ = S"
proof -
  show "subst_domain θ ∩ varsst S = {} ⟹ S ⋅st θ = S"
  proof (induction S)
    case (Cons x S)
    hence "S ⋅st θ = S" by auto
    moreover have "varsstp x ∩ subst_domain θ = {}" using Cons.prems by auto
    hence "x ⋅stp θ = x"
    proof (induction x)
      case (Send ts) thus ?case by (induct ts) auto
    next
      case (Receive ts) thus ?case by (induct ts) auto
    next
      case (Inequality X F) thus ?case
        by (induct F) (force simp add: subst_apply_pairs_def)+
    qed auto
    ultimately show ?case by simp
  qed (simp add: subst_apply_strand_def)

  show "subst_domain θ ∩ fvst S = {} ⟹ S ⋅st θ = S"
  proof (induction S)
    case (Cons x S)
    hence "S ⋅st θ = S" by auto
    moreover have "fvstp x ∩ subst_domain θ = {}"
      using Cons.prems by auto
    hence "x ⋅stp θ = x"
    proof (induction x)
      case (Send ts) thus ?case by (induct ts) auto
    next
      case (Receive ts) thus ?case by (induct ts) auto
    next
      case (Inequality X F) thus ?case
        by (induct F) (force simp add: subst_apply_pairs_def)+
    qed auto
    ultimately show ?case by simp
  qed (simp add: subst_apply_strand_def)
qed

lemma strand_substI':
  "fvst S = {} ⟹ S ⋅st θ = S"
  "varsst S = {} ⟹ S ⋅st θ = S"
by (metis inf_bot_right strand_substI(1),
    metis inf_bot_right strand_substI(2))

lemma strand_subst_set: "(set (S ⋅st θ)) = ((λx. x ⋅stp θ) ` (set S))"
by (auto simp add: subst_apply_strand_def)

lemma strand_map_inv_set_snd_rcv_subst:
  assumes "finite (M::('a,'b) terms)"
  shows "set ((map Send1 (inv set M)) ⋅st θ) = Send1 ` (M ⋅set θ)" (is ?A)
        "set ((map Receive1 (inv set M)) ⋅st θ) = Receive1 ` (M ⋅set θ)" (is ?B)
proof -
  { fix f::"('a,'b) term ⇒ ('a,'b) strand_step"
    assume f: "f = Send1 ∨ f = Receive1"
    from assms have "set ((map f (inv set M)) ⋅st θ) = f ` (M ⋅set θ)"
    proof (induction rule: finite_induct)
      case empty thus ?case unfolding inv_def by auto
    next
      case (insert m M)
      have "set (map f (inv set (insert m M)) ⋅st θ) =
            insert (f m ⋅stp θ) (set (map f (inv set M) ⋅st θ))"
        by (simp add: insert.hyps(1) inv_set_fset subst_apply_strand_def)
      thus ?case using f insert.IH by auto
    qed
  }
  thus "?A" "?B" by auto
qed

lemma strand_ground_subst_vars_subset:
  assumes "ground (subst_range θ)" shows "varsst (S ⋅st θ) ⊆ varsst S"
proof (induction S)
  case (Cons x S)
  have "varsstp (x ⋅stp θ) ⊆ varsstp x" using ground_subst_fv_subset[OF assms] 
  proof (cases x)
    case (Inequality X F)
    let ?θ = "rm_vars (set X) θ"
    have "fvpairs (F ⋅pairs ?θ) ⊆ fvpairs F"
    proof (induction F)
      case (Cons f F)
      obtain t t' where f: "f = (t,t')" by (metis surj_pair)
      hence "fvpairs (f#F ⋅pairs ?θ) = fv (t ⋅ ?θ) ∪ fv (t' ⋅ ?θ) ∪ fvpairs (F ⋅pairs ?θ)"
            "fvpairs (f#F) = fv t ∪ fv t' ∪ fvpairs F"
        by (auto simp add: subst_apply_pairs_def)
      thus ?case
        using ground_subst_fv_subset[OF ground_subset[OF rm_vars_img_subset assms, of "set X"]]
              Cons.IH
        by (metis (no_types, lifting) Un_mono)
    qed (simp add: subst_apply_pairs_def)
    moreover have
        "varsstp (x ⋅stp θ) = fvpairs (F ⋅pairs rm_vars (set X) θ) ∪ set X"
        "varsstp x = fvpairs F ∪ set X"
      using Inequality
      by (auto simp add: subst_apply_pairs_def)
    ultimately show ?thesis by auto
  qed auto
  thus ?case using Cons.IH by auto
qed (simp add: subst_apply_strand_def)

lemma ik_union_subset: "⋃(P ` ikst S) ⊆ (⋃x ∈ (set S). ⋃(P ` trmsstp x))"
by (induct S rule: ikst.induct) auto

lemma ik_snd_empty[simp]: "ikst (map Send X) = {}"
by (induct "map Send X" arbitrary: X rule: ikst.induct) auto

lemma ik_snd_empty'[simp]: "ikst [Send t] = {}" by simp

lemma ik_append[iff]: "ikst (S@S') = ikst S ∪ ikst S'" by (induct S rule: ikst.induct) auto

lemma ik_cons: "ikst (x#S) = ikst [x] ∪ ikst S" using ik_append[of "[x]" S] by simp

lemma assignment_rhs_append[iff]: "assignment_rhsst (S@S') = assignment_rhsst S ∪ assignment_rhsst S'"
by (induct S rule: assignment_rhsst.induct) auto

lemma eqs_rcv_map_empty: "assignment_rhsst (map Receive M) = {}"
by auto

lemma ik_rcv_map: assumes "ts ∈ set L" shows "set ts ⊆ ikst (map Receive L)"
proof -
  { fix L L' 
    have "set ts ⊆ ikst [Receive ts]" by auto
    hence "set ts ⊆ ikst (map Receive L@Receive ts#map Receive L')" using ik_append by auto
    hence "set ts ⊆ ikst (map Receive (L@ts#L'))" by auto
  }
  thus ?thesis using assms split_list_last by force 
qed

lemma ik_subst: "ikst (S ⋅st δ) = ikst S ⋅set δ"
by (induct rule: ikst_induct) auto

lemma ik_rcv_map': assumes "t ∈ ikst (map Receive L)" shows "∃ts ∈ set L. t ∈ set ts"
using assms by force

lemma ik_append_subset[simp]: "ikst S ⊆ ikst (S@S')" "ikst S' ⊆ ikst (S@S')"
by (induct S rule: ikst.induct) auto

lemma assignment_rhs_append_subset[simp]:
  "assignment_rhsst S ⊆ assignment_rhsst (S@S')"
  "assignment_rhsst S' ⊆ assignment_rhsst (S@S')"
by (induct S rule: assignment_rhsst.induct) auto

lemma trmsst_cons: "trmsst (x#S) = trmsstp x ∪ trmsst S" by simp

lemma trm_strand_subst_cong:
  "t ∈ trmsst S ⟹ t ⋅ δ ∈ trmsst (S ⋅st δ)
    ∨ (∃X F. Inequality X F ∈ set S ∧ t ⋅ rm_vars (set X) δ ∈ trmsst (S ⋅st δ))"
    (is "t ∈ trmsst S ⟹ ?P t δ S")
  "t ∈ trmsst (S ⋅st δ) ⟹ (∃t'. t = t' ⋅ δ ∧ t' ∈ trmsst S)
    ∨ (∃X F. Inequality X F ∈ set S ∧ (∃t' ∈ trmspairs F. t = t' ⋅ rm_vars (set X) δ))"
    (is "t ∈ trmsst (S ⋅st δ) ⟹ ?Q t δ S")
proof -
  show "t ∈ trmsst S ⟹ ?P t δ S"
  proof (induction S)
    case (Cons x S) show ?case
    proof (cases "t ∈ trmsst S")
      case True
      hence "?P t δ S" using Cons by simp
      thus ?thesis
        by (cases x)
           (metis (no_types, lifting) Un_iff list.set_intros(2) strand_subst_hom(2) trmsst_cons)+
    next
      case False
      hence "t ∈ trmsstp x" using Cons.prems by auto
      thus ?thesis
      proof (induction x)
        case (Inequality X F)
        hence "t ⋅ rm_vars (set X) δ ∈ trmsstp (Inequality X F ⋅stp δ)"
          by (induct F) (auto simp add: subst_apply_pairs_def subst_apply_strand_step_def)
        thus ?case by fastforce
      qed (auto simp add: subst_apply_strand_step_def)
    qed
  qed simp

  show "t ∈ trmsst (S ⋅st δ) ⟹ ?Q t δ S"
  proof (induction S)
    case (Cons x S) show ?case
    proof (cases "t ∈ trmsst (S ⋅st δ)")
      case True
      hence "?Q t δ S" using Cons by simp
      thus ?thesis by (cases x) force+
    next
      case False
      hence "t ∈ trmsstp (x ⋅stp δ)" using Cons.prems by auto
      thus ?thesis
      proof (induction x)
        case (Inequality X F)
        hence "t ∈ trmsstp (Inequality X F) ⋅set rm_vars (set X) δ"
          by (induct F) (force simp add: subst_apply_pairs_def)+
        thus ?case by fastforce
      qed (auto simp add: subst_apply_strand_step_def)
    qed
  qed simp
qed


subsection ‹Lemmata: Free Variables of Strands›
lemma fv_trm_snd_rcv[simp]:
  "fvset (trmsstp (Send ts)) = fvset (set ts)" "fvset (trmsstp (Receive ts)) = fvset (set ts)"
by simp_all

lemma in_strand_fv_subset: "x ∈ set S ⟹ varsstp x ⊆ varsst S"
by fastforce

lemma in_strand_fv_subset_snd: "Send ts ∈ set S ⟹ fvset (set ts) ⊆ ⋃(set (map fvsnd S))"
by fastforce

lemma in_strand_fv_subset_rcv: "Receive ts ∈ set S ⟹ fvset (set ts) ⊆ ⋃(set (map fvrcv S))"
by fastforce

lemma fvsndE:
  assumes "v ∈ ⋃(set (map fvsnd S))"
  obtains ts where "send⟨ts⟩st ∈ set S" "v ∈ fvset (set ts)"
proof -
  have "∃ts. send⟨ts⟩st ∈ set S ∧ v ∈ fvset (set ts)"
    by (metis (no_types, lifting) assms UN_E empty_iff set_map strand_step.case_eq_if
              fvsnd_def strand_step.collapse(1))
  thus ?thesis by (metis that)
qed

lemma fvrcvE:
  assumes "v ∈ ⋃(set (map fvrcv S))"
  obtains ts where "receive⟨ts⟩st ∈ set S" "v ∈ fvset (set ts)"
proof -
  have "∃ts. receive⟨ts⟩st ∈ set S ∧ v ∈ fvset (set ts)"
    by (metis (no_types, lifting) assms UN_E empty_iff set_map strand_step.case_eq_if
              fvrcv_def strand_step.collapse(2))
  thus ?thesis by (metis that)
qed

lemma varsstpI[intro]: "x ∈ fvstp s ⟹ x ∈ varsstp s"
by (induct s rule: fvstp.induct) auto

lemma varsstI[intro]: "x ∈ fvst S ⟹ x ∈ varsst S" using varsstpI by fastforce

lemma fvst_subset_varsst[simp]: "fvst S ⊆ varsst S" using varsstI by force

lemma varsst_is_fvst_bvarsst: "varsst S = fvst S ∪ bvarsst S"
proof (induction S)
  case (Cons x S) thus ?case
  proof (induction x)
    case (Inequality X F) thus ?case by (induct F) auto
  qed auto
qed simp

lemma fvstp_is_subterm_trmsstp: "x ∈ fvstp a ⟹ Var x ∈ subtermsset (trmsstp a)" 
using var_is_subterm by (cases a) force+

lemma fvst_is_subterm_trmsst: "x ∈ fvst A ⟹ Var x ∈ subtermsset (trmsst A)"
proof (induction A)
  case (Cons a A) thus ?case using fvstp_is_subterm_trmsstp by (cases "x ∈ fvst A") auto
qed simp

lemma vars_st_snd_map: "varsst (map Send tss) = fvset (Fun f ` set tss)" by auto

lemma vars_st_rcv_map: "varsst (map Receive tss) = fvset (Fun f ` set tss)" by auto

lemma vars_snd_rcv_union:
  "varsstp x = fvsnd x ∪ fvrcv x ∪ fveq assign x ∪ fveq check x ∪ fvineq x ∪ set (bvarsstp x)"
proof (cases x)
  case (Equality ac t t') thus ?thesis by (cases ac) auto
qed auto

lemma fv_snd_rcv_union:
  "fvstp x = fvsnd x ∪ fvrcv x ∪ fveq assign x ∪ fveq check x ∪ fvineq x"
proof (cases x)
  case (Equality ac t t') thus ?thesis by (cases ac) auto
qed auto

lemma fv_snd_rcv_empty[simp]: "fvsnd x = {} ∨ fvrcv x = {}" by (cases x) simp_all

lemma vars_snd_rcv_strand[iff]:
  "varsst (S::('a,'b) strand) =
    (⋃(set (map fvsnd S))) ∪ (⋃(set (map fvrcv S))) ∪ (⋃(set (map (fveq assign) S)))
    ∪ (⋃(set (map (fveq check) S))) ∪ (⋃(set (map fvineq S))) ∪ bvarsst S"
unfolding bvarsst_def
proof (induction S)
  case (Cons x S)
  have "⋀s V. varsstp (s::('a,'b) strand_step) ∪ V = 
                fvsnd s ∪ fvrcv s ∪ fveq assign s ∪ fveq check s ∪ fvineq s ∪ set (bvarsstp s) ∪ 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]:
  "fvst (S::('a,'b) strand) =
    (⋃(set (map fvsnd S))) ∪ (⋃(set (map fvrcv S))) ∪ (⋃(set (map (fveq assign) S)))
    ∪ (⋃(set (map (fveq check) S))) ∪ (⋃(set (map fvineq S)))"
unfolding bvarsst_def
proof (induction S)
  case (Cons x S)
  have "⋀s V. fvstp (s::('a,'b) strand_step) ∪ V = 
                fvsnd s ∪ fvrcv s ∪ fveq assign s ∪ fveq check s ∪ fvineq s ∪ 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]:
  "wfrestrictedvarsst (S::('a,'b) strand) =
    (⋃(set (map fvsnd S))) ∪ (⋃(set (map fvrcv S))) ∪ (⋃(set (map (fveq assign) S)))"
by (induct S) (auto simp add: split: strand_step.split poscheckvariant.split)

lemma fv_snd_rcv_strand_subset[simp]:
  "⋃(set (map fvsnd S)) ⊆ fvst S" "⋃(set (map fvrcv S)) ⊆ fvst S"
  "⋃(set (map (fveq ac) S)) ⊆ fvst S" "⋃(set (map fvineq S)) ⊆ fvst S"
  "wfvarsoccsst S ⊆ fvst S"
proof -
  show "⋃(set (map fvsnd S)) ⊆ fvst S" "⋃(set (map fvrcv S)) ⊆ fvst S" "⋃(set (map fvineq S)) ⊆ fvst S"
    using fv_snd_rcv_strand[of S] by auto
  
  show "⋃(set (map (fveq ac) S)) ⊆ fvst S"
    by (induct S) (auto split: strand_step.split poscheckvariant.split)

  show "wfvarsoccsst S ⊆ fvst S"
    by (induct S) (auto split: strand_step.split poscheckvariant.split)
qed

lemma vars_snd_rcv_strand_subset2[simp]:
  "⋃(set (map fvsnd S)) ⊆ wfrestrictedvarsst S" "⋃(set (map fvrcv S)) ⊆ wfrestrictedvarsst S"
  "⋃(set (map (fveq assign) S)) ⊆ wfrestrictedvarsst S" "wfvarsoccsst S ⊆ wfrestrictedvarsst S"
by (induction S) (auto split: strand_step.split poscheckvariant.split)

lemma wfrestrictedvarsst_subset_varsst: "wfrestrictedvarsst S ⊆ varsst S"
by (induction S) (auto split: strand_step.split poscheckvariant.split)

lemma subst_sends_strand_step_fv_to_img: "fvstp (x ⋅stp δ) ⊆ fvstp x ∪ range_vars δ" 
using subst_sends_fv_to_img[of _ δ]
proof (cases x)
  case (Inequality X F)
  let ?θ = "rm_vars (set X) δ"
  have "fvpairs (F ⋅pairs ?θ) ⊆ fvpairs F ∪ range_vars ?θ"
  proof (induction F)
    case (Cons f F) thus ?case
      using subst_sends_fv_to_img[of _ ?θ]
      by (auto simp add: subst_apply_pairs_def)
  qed (auto simp add: subst_apply_pairs_def)
  hence "fvpairs (F ⋅pairs ?θ) ⊆ fvpairs F ∪ range_vars δ"
    using rm_vars_img_subset[of "set X" δ] fv_set_mono
    unfolding range_vars_alt_def by blast+
  thus ?thesis using Inequality by (auto simp add: subst_apply_strand_step_def)
qed (auto simp add: subst_apply_strand_step_def)

lemma subst_sends_strand_fv_to_img: "fvst (S ⋅st δ) ⊆ fvst S ∪ range_vars δ" 
proof (induction S)
  case (Cons x S)
  have *: "fvst (x#S ⋅st δ) = fvstp (x ⋅stp δ) ∪ fvst (S ⋅st δ)"
          "fvst (x#S) ∪ range_vars δ = fvstp x ∪ fvst S ∪ range_vars δ"
    by auto
  thus ?case using Cons.IH subst_sends_strand_step_fv_to_img[of x δ] by auto
qed simp

lemma ineq_apply_subst:
  assumes "subst_domain δ ∩ set X = {}"
  shows "(Inequality X F) ⋅stp δ = Inequality X (F ⋅pairs δ)"
using rm_vars_apply'[OF assms] by (simp add: subst_apply_strand_step_def)

lemma fv_strand_step_subst:
  assumes "P = fvstp ∨ P = fvrcv ∨ P = fvsnd ∨ P = fveq ac ∨ P = fvineq"
  and "set (bvarsstp x) ∩ (subst_domain δ ∪ range_vars δ) = {}"
  shows "fvset (δ ` (P x)) = P (x ⋅stp δ)"
proof (cases x)
  case (Send ts)
  hence "varsstp x = fvset (set ts)" "fvsnd x = fvset (set ts)" by auto
  thus ?thesis using assms Send subst_apply_fv_unfold[of _ δ] by fastforce
next
  case (Receive ts)
  hence "varsstp x = fvset (set ts)" "fvrcv x = fvset (set ts)" by auto
  thus ?thesis using assms Receive subst_apply_fv_unfold[of _ δ] by fastforce
next
  case (Equality ac' t t') show ?thesis
  proof (cases "ac = ac'")
    case True
    hence "varsstp x = fv t ∪ fv t'" "fveq ac x = fv t ∪ fv t'"
      using Equality
      by auto
    thus ?thesis
      using assms Equality subst_apply_fv_unfold[of _ δ] True
      by auto
  next
    case False
    hence "varsstp x = fv t ∪ fv t'" "fveq ac x = {}"
      using Equality
      by auto
    thus ?thesis
      using assms Equality subst_apply_fv_unfold[of _ δ] False
      by auto
  qed
next
  case (Inequality X F)
  hence 1: "set X ∩ (subst_domain δ ∪ range_vars δ) = {}"
           "x ⋅stp δ = Inequality X (F ⋅pairs δ)"
           "rm_vars (set X) δ = δ"
    using assms ineq_apply_subst[of δ X F] rm_vars_apply'[of δ "set X"]
    unfolding range_vars_alt_def by force+

  have 2: "fvineq x = fvpairs F - set X" using Inequality by auto
  hence "fvset (δ ` fvineq x) = fvset (δ ` fvpairs F) - set X"
    using fvset_subst_img_eq[OF 1(1), of "fvpairs F"] by simp
  hence 3: "fvset (δ ` fvineq x) = fvpairs (F ⋅pairs δ) - set X" by (metis fvpairs_step_subst)
  
  have 4: "fvineq (x ⋅stp δ) = fvpairs (F ⋅pairs δ) - set X" using 1(2) by auto

  show ?thesis
    using assms(1) Inequality subst_apply_fv_unfold[of _ δ] 1(2) 2 3 4
    unfolding fveq_def fvrcv_def fvsnd_def
    by (metis (no_types) Sup_empty image_empty fvpairs.simps fvset.simps
              fvstp.simps(4) strand_step.simps(20))
qed

lemma fv_strand_subst:
  assumes "P = fvstp ∨ P = fvrcv ∨ P = fvsnd ∨ P = fveq ac ∨ P = fvineq"
  and "bvarsst S ∩ (subst_domain δ ∪ range_vars δ) = {}"
  shows "fvset (δ ` (⋃(set (map P S)))) = ⋃(set (map P (S ⋅st δ)))"
using assms(2)
proof (induction S)
  case (Cons x S)
  hence *: "bvarsst S ∩ (subst_domain δ ∪ range_vars δ) = {}"
           "set (bvarsstp x) ∩ (subst_domain δ ∪ range_vars δ) = {}"
    unfolding bvarsst_def by force+
  hence **: "fvset (δ ` P x) = P (x ⋅stp δ)" using fv_strand_step_subst[OF assms(1), of x δ] by auto
  have "fvset (δ ` (⋃(set (map P (x#S))))) = fvset (δ ` P x) ∪ (⋃(set (map P ((S ⋅st δ)))))"
    using Cons unfolding range_vars_alt_def bvarsst_def by force
  hence "fvset (δ ` (⋃(set (map P (x#S))))) = P (x ⋅stp δ) ∪ fvset (δ ` (⋃(set (map P S))))"
    using ** by simp
  thus ?case using Cons.IH[OF *(1)] unfolding bvarsst_def by simp
qed simp

lemma fv_strand_subst2:
  assumes "bvarsst S ∩ (subst_domain δ ∪ range_vars δ) = {}"
  shows "fvset (δ ` (wfrestrictedvarsst S)) = wfrestrictedvarsst (S ⋅st δ)"
by (metis (no_types, lifting) assms fvset.simps vars_snd_rcv_strand2 fv_strand_subst UN_Un image_Un)

lemma fv_strand_subst':
  assumes "bvarsst S ∩ (subst_domain δ ∪ range_vars δ) = {}"
  shows "fvset (δ ` (fvst S)) = fvst (S ⋅st δ)"
by (metis assms fv_strand_subst fvst_def)

lemma fv_trmspairs_is_fvpairs:
  "fvset (trmspairs F) = fvpairs F"
by auto

lemma fvpairs_in_fv_trmspairs: "x ∈ fvpairs F ⟹ x ∈ fvset (trmspairs F)"
using fv_trmspairs_is_fvpairs[of F] by blast

lemma trmsst_append: "trmsst (A@B) = trmsst A ∪ trmsst B"
by auto

lemma trmspairs_subst: "trmspairs (a ⋅pairs θ) = trmspairs a ⋅set θ"
by (auto simp add: subst_apply_pairs_def)

lemma trmspairs_fv_subst_subset:
  "t ∈ trmspairs F ⟹ fv (t ⋅ θ) ⊆ fvpairs (F ⋅pairs θ)"
by (force simp add: subst_apply_pairs_def)

lemma trmspairs_fv_subst_subset':
  fixes t::"('a,'b) term" and θ::"('a,'b) subst"
  assumes "t ∈ subtermsset (trmspairs F)"
  shows "fv (t ⋅ θ) ⊆ fvpairs (F ⋅pairs θ)"
proof -
  { fix x assume "x ∈ fv t"
    hence "x ∈ fvpairs F"
      using fv_subset[OF assms] fv_subterms_set[of "trmspairs F"] fv_trmspairs_is_fvpairs[of F]
      by blast
    hence "fv (θ x) ⊆ fvpairs (F ⋅pairs θ)" using fvpairs_subst_fv_subset by fast
  } thus ?thesis by (meson fv_subst_obtain_var subset_iff) 
qed

lemma trmspairs_funs_term_cases:
  assumes "t ∈ trmspairs (F ⋅pairs θ)" "f ∈ funs_term t"
  shows "(∃u ∈ trmspairs F. f ∈ funs_term u) ∨ (∃x ∈ fvpairs F. f ∈ funs_term (θ x))"
using assms(1)
proof (induction F)
  case (Cons g F)
  obtain s u where g: "g = (s,u)" by (metis surj_pair)
  show ?case
  proof (cases "t ∈ trmspairs (F ⋅pairs θ)")
    case False
    thus ?thesis
      using assms(2) Cons.prems g funs_term_subst[of _ θ]
      by (auto simp add: subst_apply_pairs_def)
  qed (use Cons.IH in fastforce)
qed simp

lemma trmstp_subst: 
  assumes "subst_domain θ ∩ set (bvarsstp a) = {}"
  shows "trmsstp (a ⋅stp θ) = trmsstp a ⋅set θ"
proof -
  have "rm_vars (set (bvarsstp a)) θ = θ" using assms by force
  thus ?thesis
    using assms
    by (auto simp add: subst_apply_pairs_def subst_apply_strand_step_def
             split: strand_step.splits)
qed

lemma trmsst_subst:
  assumes "subst_domain θ ∩ bvarsst A = {}"
  shows "trmsst (A ⋅st θ) = trmsst A ⋅set θ"
using assms
proof (induction A)
  case (Cons a A)
  have 1: "subst_domain θ ∩ bvarsst A = {}" "subst_domain θ ∩ set (bvarsstp a) = {}"
    using Cons.prems by auto
  hence IH: "trmsst A ⋅set θ = trmsst (A ⋅st θ)" using Cons.IH by simp
  
  have "trmsst (a#A) = trmsstp a ∪ trmsst A" by auto
  hence 2: "trmsst (a#A) ⋅set θ = (trmsstp a ⋅set θ) ∪ (trmsst A ⋅set θ)" by (metis image_Un)

  have "trmsst (a#A ⋅st θ) = (trmsstp (a ⋅stp θ)) ∪ trmsst (A ⋅st θ)"
    by (auto simp add: subst_apply_strand_def)
  hence 3: "trmsst (a#A ⋅st θ) = (trmsstp a ⋅set θ) ∪ trmsst (A ⋅st θ)"
    using trmstp_subst[OF 1(2)] by auto
  
  show ?case using IH 2 3 by metis
qed (simp add: subst_apply_strand_def)

lemma strand_map_set_subst:
  assumes δ: "bvarsst S ∩ (subst_domain δ ∪ range_vars δ) = {}"
  shows "⋃(set (map trmsstp (S ⋅st δ))) = (⋃(set (map trmsstp S))) ⋅set δ"
using assms
proof (induction S)
  case (Cons x S)
  hence "bvarsst [x] ∩ subst_domain δ = {}" "bvarsst S ∩ (subst_domain δ ∪ range_vars δ) = {}"
    unfolding bvarsst_def by force+
  hence *: "subst_domain δ ∩ set (bvarsstp x) = {}"
           "⋃(set (map trmsstp (S ⋅st δ))) = ⋃(set (map trmsstp S)) ⋅set δ"
    using Cons.IH(1) bvarsst_singleton[of x] by auto
  hence "trmsstp (x ⋅stp δ) = (trmsstp x) ⋅set δ"
  proof (cases x)
    case (Inequality X F)
    thus ?thesis
      using rm_vars_apply'[of δ "set X"] * 
      by (metis (no_types, lifting) image_cong trmstp_subst)
  qed simp_all
  thus ?case using * subst_all_insert by auto
qed simp

lemma subst_apply_fv_subset_strand_trm:
  assumes P: "P = fvstp ∨ P = fvrcv ∨ P = fvsnd ∨ P = fveq ac ∨ P = fvineq"
  and fv_sub: "fv t ⊆ ⋃(set (map P S)) ∪ V"
  and δ: "bvarsst S ∩ (subst_domain δ ∪ range_vars δ) = {}"
  shows "fv (t ⋅ δ) ⊆ ⋃(set (map P (S ⋅st δ))) ∪ fvset (δ ` V)"
using fv_strand_subst[OF P δ] subst_apply_fv_subset[OF fv_sub, of δ] by force

lemma subst_apply_fv_subset_strand_trm2:
  assumes fv_sub: "fv t ⊆ wfrestrictedvarsst S ∪ V"
  and δ: "bvarsst S ∩ (subst_domain δ ∪ range_vars δ) = {}"
  shows "fv (t ⋅ δ) ⊆ wfrestrictedvarsst (S ⋅st δ) ∪ fvset (δ ` V)"
using fv_strand_subst2[OF δ] subst_apply_fv_subset[OF fv_sub, of δ] by force

lemma subst_apply_fv_subset_strand:
  assumes P: "P = fvstp ∨ P = fvrcv ∨ P = fvsnd ∨ P = fveq ac ∨ P = fvineq"
  and P_subset: "P x ⊆ ⋃(set (map P S)) ∪ V"
  and δ: "bvarsst S ∩ (subst_domain δ ∪ range_vars δ) = {}"
         "set (bvarsstp x) ∩ (subst_domain δ ∪ range_vars δ) = {}"
  shows "P (x ⋅stp δ) ⊆ ⋃(set (map P (S ⋅st δ))) ∪ fvset (δ ` V)"
proof (cases x)
  case (Send ts)
  hence *: "fvstp x = fvset (set ts)" "fvstp (x ⋅stp δ) = fvset (set ts ⋅set δ)"
           "fvrcv x = {}" "fvrcv (x ⋅stp δ) = {}"
           "fvsnd x = fvset (set ts)" "fvsnd (x ⋅stp δ) = fvset (set ts ⋅set δ)"
           "fveq ac x = {}" "fveq ac (x ⋅stp δ) = {}"
           "fvineq x = {}" "fvineq (x ⋅stp δ) = {}"
    by auto
  hence **: "(P x = fvset (set ts) ∧ P (x ⋅stp δ) = fvset (set ts ⋅set δ)) ∨
             (P x = {} ∧ P (x ⋅stp δ) = {})"
    by (metis P)
  moreover
  { assume "P x = {}" "P (x ⋅stp δ) = {}" hence ?thesis by simp }
  moreover
  { assume "P x = fvset (set ts)" "P (x ⋅stp δ) = fvset (set ts ⋅set δ)"
    hence "fvset (set ts) ⊆ ⋃(set (map P S)) ∪ V" using P_subset by auto
    hence "fvset (set ts ⋅set δ) ⊆ ⋃(set (map P (S ⋅st δ))) ∪ fvset (δ ` V)"
      using subst_apply_fv_subset_strand_trm[OF P _ assms(3), of _ V] by fastforce
    hence ?thesis using ‹P (x ⋅stp δ) = fvset (set ts ⋅set δ)› by force
  }
  ultimately show ?thesis by metis
next
  case (Receive ts)
  hence *: "fvstp x = fvset (set ts)" "fvstp (x ⋅stp δ) = fvset (set ts ⋅set δ)"
           "fvrcv x = fvset (set ts)" "fvrcv (x ⋅stp δ) = fvset (set ts ⋅set δ)"
           "fvsnd x = {}" "fvsnd (x ⋅stp δ) = {}"
           "fveq ac x = {}" "fveq ac (x ⋅stp δ) = {}"
           "fvineq x = {}" "fvineq (x ⋅stp δ) = {}"
    by auto
  hence **: "(P x = fvset (set ts) ∧ P (x ⋅stp δ) = fvset (set ts ⋅set δ)) ∨
             (P x = {} ∧ P (x ⋅stp δ) = {})"
    by (metis P)
  moreover
  { assume "P x = {}" "P (x ⋅stp δ) = {}" hence ?thesis by simp }
  moreover
  { assume "P x = fvset (set ts)" "P (x ⋅stp δ) = fvset (set ts ⋅set δ)"
    hence "fvset (set ts) ⊆ ⋃(set (map P S)) ∪ V" using P_subset by auto
    hence "fvset (set ts ⋅set δ) ⊆ ⋃(set (map P (S ⋅st δ))) ∪ fvset (δ ` V)"
      using subst_apply_fv_subset_strand_trm[OF P _ assms(3), of _ V] by fastforce
    hence ?thesis using ‹P (x ⋅stp δ) = fvset (set ts ⋅set δ)› by blast
  }
  ultimately show ?thesis by metis
next
  case (Equality ac' t t') show ?thesis
  proof (cases "ac' = ac")
    case True
    hence *: "fvstp x = fv t ∪ fv t'" "fvstp (x ⋅stp δ) = fv (t ⋅ δ) ∪ fv (t' ⋅ δ)"
             "fvrcv x = {}" "fvrcv (x ⋅stp δ) = {}"
             "fvsnd x = {}" "fvsnd (x ⋅stp δ) = {}"
             "fveq ac x = fv t ∪ fv t'" "fveq ac (x ⋅stp δ) = fv (t ⋅ δ) ∪ fv (t' ⋅ δ)"
             "fvineq x = {}" "fvineq (x ⋅stp δ) = {}"
      using Equality by auto
    hence **: "(P x = fv t ∪ fv t' ∧ P (x ⋅stp δ) = fv (t ⋅ δ) ∪ fv (t' ⋅ δ))
              ∨ (P x = {} ∧ P (x ⋅stp δ) = {})"
      by (metis P)
    moreover
    { assume "P x = {}" "P (x ⋅stp δ) = {}" hence ?thesis by simp }
    moreover
    { assume "P x = fv t ∪ fv t'" "P (x ⋅stp δ) = fv (t ⋅ δ) ∪ fv (t' ⋅ δ)"
      hence "fv t ⊆ ⋃(set (map P S)) ∪ V" "fv t' ⊆ ⋃(set (map P S)) ∪ V" using P_subset by auto
      hence "fv (t ⋅ δ) ⊆ ⋃(set (map P (S ⋅st δ))) ∪ fvset (δ ` V)"
            "fv (t' ⋅ δ) ⊆ ⋃(set (map P (S ⋅st δ))) ∪ fvset (δ ` V)"
        using P subst_apply_fv_subset_strand_trm assms by metis+
      hence ?thesis using ‹P (x ⋅stp δ) = fv (t ⋅ δ) ∪ fv (t' ⋅ δ)› by blast
    }
    ultimately show ?thesis by metis
  next
    case False
    hence *: "fvstp x = fv t ∪ fv t'" "fvstp (x ⋅stp δ) = fv (t ⋅ δ) ∪ fv (t' ⋅ δ)"
             "fvrcv x = {}" "fvrcv (x ⋅stp δ) = {}"
             "fvsnd x = {}" "fvsnd (x ⋅stp δ) = {}"
             "fveq ac x = {}" "fveq ac (x ⋅stp δ) = {}"
             "fvineq x = {}" "fvineq (x ⋅stp δ) = {}"
      using Equality by auto
    hence **: "(P x = fv t ∪ fv t' ∧ P (x ⋅stp δ) = fv (t ⋅ δ) ∪ fv (t' ⋅ δ))
              ∨ (P x = {} ∧ P (x ⋅stp δ) = {})"
      by (metis P)
    moreover
    { assume "P x = {}" "P (x ⋅stp δ) = {}" hence ?thesis by simp }
    moreover
    { assume "P x = fv t ∪ fv t'" "P (x ⋅stp δ) = fv (t ⋅ δ) ∪ fv (t' ⋅ δ)"
      hence "fv t ⊆ ⋃(set (map P S)) ∪ V" "fv t' ⊆ ⋃(set (map P S)) ∪ V" using P_subset by auto
      hence "fv (t ⋅ δ) ⊆ ⋃(set (map P (S ⋅st δ))) ∪ fvset (δ ` V)"
            "fv (t' ⋅ δ) ⊆ ⋃(set (map P (S ⋅st δ))) ∪ fvset (δ ` V)"
        using P subst_apply_fv_subset_strand_trm assms by metis+
      hence ?thesis using ‹P (x ⋅stp δ) = fv (t ⋅ δ) ∪ fv (t' ⋅ δ)› by blast
    }
    ultimately show ?thesis by metis
  qed
next
  case (Inequality X F)
  hence *: "fvstp x = fvpairs F - set X" "fvstp (x ⋅stp δ) = fvpairs (F ⋅pairs δ) - set X"
           "fvrcv x = {}" "fvrcv (x ⋅stp δ) = {}"
           "fvsnd x = {}" "fvsnd (x ⋅stp δ) = {}"
           "fveq ac x = {}" "fveq ac (x ⋅stp δ) = {}"
           "fvineq x = fvpairs F - set X"
           "fvineq (x ⋅stp δ) = fvpairs (F ⋅pairs δ) - set X"
    using δ(2) ineq_apply_subst[of δ X F] by force+
  hence **: "(P x = fvpairs F - set X ∧ P (x ⋅stp δ) = fvpairs (F ⋅pairs δ) - set X)
            ∨ (P x = {} ∧ P (x ⋅stp δ) = {})"
    by (metis P)
  moreover
  { assume "P x = {}" "P (x ⋅stp δ) = {}" hence ?thesis by simp }
  moreover
  { assume "P x = fvpairs F - set X" "P (x ⋅stp δ) = fvpairs (F ⋅pairs δ) - set X"
    hence "fvpairs F - set X ⊆ ⋃(set (map P S)) ∪ V"
      using P_subset by auto
    hence "fvpairs (F ⋅pairs δ) ⊆ ⋃(set (map P (S ⋅st δ))) ∪ fvset (δ ` (V ∪ set X))"
    proof (induction F)
      case (Cons f G)
      hence IH: "fvpairs (G ⋅pairs δ) ⊆ ⋃(set (map P (S ⋅st δ))) ∪ fvset (δ ` (V ∪ set X))"
        by (metis (no_types, lifting) Diff_subset_conv UN_insert le_sup_iff
                  list.simps(15) fvpairs.simps)
      obtain t t' where f: "f = (t,t')" by (metis surj_pair)
      hence "fv t ⊆ ⋃(set (map P S)) ∪ (V ∪ set X)" "fv t' ⊆ ⋃(set (map P S)) ∪ (V ∪ set X)"
        using Cons.prems by auto
      hence "fv (t ⋅ δ) ⊆ ⋃(set (map P (S ⋅st δ))) ∪ fvset (δ ` (V ∪ set X))"
            "fv (t' ⋅ δ) ⊆ ⋃(set (map P (S ⋅st δ))) ∪ fvset (δ ` (V ∪ set X))"
        using subst_apply_fv_subset_strand_trm[OF P _ assms(3)]
        by blast+
      thus ?case using f IH by (auto simp add: subst_apply_pairs_def)
    qed (simp add: subst_apply_pairs_def)
    moreover have "fvset (δ ` set X) = set X" using assms(4) Inequality by force
    ultimately have "fvpairs (F ⋅pairs δ) - set X ⊆ ⋃(set (map P (S ⋅st δ))) ∪ fvset (δ ` V)"
      by auto
    hence ?thesis using ‹P (x ⋅stp δ) = fvpairs (F ⋅pairs δ) - set X› by blast
  }
  ultimately show ?thesis by metis
qed

lemma subst_apply_fv_subset_strand2:
  assumes P: "P = fvstp ∨ P = fvrcv ∨ P = fvsnd ∨ P = fveq ac ∨ P = fvineq ∨ P = fv_req ac"
  and P_subset: "P x ⊆ wfrestrictedvarsst S ∪ V"
  and δ: "bvarsst S ∩ (subst_domain δ ∪ range_vars δ) = {}"
         "set (bvarsstp x) ∩ (subst_domain δ ∪ range_vars δ) = {}"
  shows "P (x ⋅stp δ) ⊆ wfrestrictedvarsst (S ⋅st δ) ∪ fvset (δ ` V)"
proof (cases x)
  case (Send ts)
  hence *: "fvstp x = fvset (set ts)" "fvstp (x ⋅stp δ) = fvset (set ts ⋅set δ)"
           "fvrcv x = {}" "fvrcv (x ⋅stp δ) = {}"
           "fvsnd x = fvset (set ts)" "fvsnd (x ⋅stp δ) = fvset (set ts ⋅set δ)"
           "fveq ac x = {}" "fveq ac (x ⋅stp δ) = {}"
           "fvineq x = {}" "fvineq (x ⋅stp δ) = {}"
           "fv_req ac x = {}" "fv_req ac (x ⋅stp δ) = {}"
    by auto
  hence **: "(P x = fvset (set ts) ∧ P (x ⋅stp δ) = fvset (set ts ⋅set δ)) ∨ (P x = {} ∧ P (x ⋅stp δ) = {})" by (metis P)
  moreover
  { assume "P x = {}" "P (x ⋅stp δ) = {}" hence ?thesis by simp }
  moreover
  { assume "P x = fvset (set ts)" "P (x ⋅stp δ) = fvset (set ts ⋅set δ)"
    hence "fvset (set ts) ⊆ wfrestrictedvarsst S ∪ V" using P_subset by auto
    hence "fvset (set ts ⋅set δ) ⊆ wfrestrictedvarsst (S ⋅st δ) ∪ fvset (δ ` V)"
      using subst_apply_fv_subset_strand_trm2[OF _ assms(3), of _ V] by fastforce
    hence ?thesis using ‹P (x ⋅stp δ) = fvset (set ts ⋅set δ)› by blast
  }
  ultimately show ?thesis by metis
next
  case (Receive ts)
  hence *: "fvstp x = fvset (set ts)" "fvstp (x ⋅stp δ) = fvset (set ts ⋅set δ)"
           "fvrcv x = fvset (set ts)" "fvrcv (x ⋅stp δ) = fvset (set ts ⋅set δ)"
           "fvsnd x = {}" "fvsnd (x ⋅stp δ) = {}"
           "fveq ac x = {}" "fveq ac (x ⋅stp δ) = {}"
           "fvineq x = {}" "fvineq (x ⋅stp δ) = {}"
           "fv_req ac x = {}" "fv_req ac (x ⋅stp δ) = {}"
    by auto
  hence **: "(P x = fvset (set ts) ∧ P (x ⋅stp δ) = fvset (set ts ⋅set δ)) ∨
             (P x = {} ∧ P (x ⋅stp δ) = {})"
    by (metis P)
  moreover
  { assume "P x = {}" "P (x ⋅stp δ) = {}" hence ?thesis by simp }
  moreover
  { assume "P x = fvset (set ts)" "P (x ⋅stp δ) = fvset (set ts ⋅set δ)"
    hence "fvset (set ts) ⊆ wfrestrictedvarsst S ∪ V" using P_subset by auto
    hence "fvset (set ts ⋅set δ) ⊆ wfrestrictedvarsst (S ⋅st δ) ∪ fvset (δ ` V)"
      using subst_apply_fv_subset_strand_trm2[OF _ assms(3), of _ V] by fastforce
    hence ?thesis using ‹P (x ⋅stp δ) = fvset (set ts ⋅set δ)› by blast
  }
  ultimately show ?thesis by metis
next
  case (Equality ac' t t') show ?thesis
  proof (cases "ac' = ac")
    case True
    hence *: "fvstp x = fv t ∪ fv t'" "fvstp (x ⋅stp δ) = fv (t ⋅ δ) ∪ fv (t' ⋅ δ)"
             "fvrcv x = {}" "fvrcv (x ⋅stp δ) = {}"
             "fvsnd x = {}" "fvsnd (x ⋅stp δ) = {}"
             "fveq ac x = fv t ∪ fv t'" "fveq ac (x ⋅stp δ) = fv (t ⋅ δ) ∪ fv (t' ⋅ δ)"
             "fvineq x = {}" "fvineq (x ⋅stp δ) = {}"
             "fv_req ac x = fv t'" "fv_req ac (x ⋅stp δ) = fv (t' ⋅ δ)"
      using Equality by auto
    hence **: "(P x = fv t ∪ fv t' ∧ P (x ⋅stp δ) = fv (t ⋅ δ) ∪ fv (t' ⋅ δ))
              ∨ (P x = {} ∧ P (x ⋅stp δ) = {})
              ∨ (P x = fv t' ∧ P (x ⋅stp δ) = fv (t' ⋅ δ))"
      by (metis P)
    moreover
    { assume "P x = {}" "P (x ⋅stp δ) = {}" hence ?thesis by simp }
    moreover
    { assume "P x = fv t ∪ fv t'" "P (x ⋅stp δ) = fv (t ⋅ δ) ∪ fv (t' ⋅ δ)"
      hence "fv t ⊆ wfrestrictedvarsst S ∪ V" "fv t' ⊆ wfrestrictedvarsst S ∪ V" using P_subset by auto
      hence "fv (t ⋅ δ) ⊆ wfrestrictedvarsst (S ⋅st δ) ∪ fvset (δ ` V)"
            "fv (t' ⋅ δ) ⊆ wfrestrictedvarsst (S ⋅st δ) ∪ fvset (δ ` V)"
        using P subst_apply_fv_subset_strand_trm2 assms by blast+
      hence ?thesis using ‹P (x ⋅stp δ) = fv (t ⋅ δ) ∪ fv (t' ⋅ δ)› by blast
    }
    moreover
    { assume "P x = fv t'" "P (x ⋅stp δ) = fv (t' ⋅ δ)"
      hence "fv t' ⊆ wfrestrictedvarsst S ∪ V" using P_subset by auto
      hence "fv (t' ⋅ δ) ⊆ wfrestrictedvarsst (S ⋅st δ) ∪ fvset (δ ` V)"
        using P subst_apply_fv_subset_strand_trm2 assms by blast+
      hence ?thesis using ‹P (x ⋅stp δ) = fv (t' ⋅ δ)› by blast
    }
    ultimately show ?thesis by metis
  next
    case False
    hence *: "fvstp x = fv t ∪ fv t'" "fvstp (x ⋅stp δ) = fv (t ⋅ δ) ∪ fv (t' ⋅ δ)"
             "fvrcv x = {}" "fvrcv (x ⋅stp δ) = {}"
             "fvsnd x = {}" "fvsnd (x ⋅stp δ) = {}"
             "fveq ac x = {}" "fveq ac (x ⋅stp δ) = {}"
             "fvineq x = {}" "fvineq (x ⋅stp δ) = {}"
             "fv_req ac x = {}" "fv_req ac (x ⋅stp δ) = {}"
      using Equality by auto
    hence **: "(P x = fv t ∪ fv t' ∧ P (x ⋅stp δ) = fv (t ⋅ δ) ∪ fv (t' ⋅ δ))
              ∨ (P x = {} ∧ P (x ⋅stp δ) = {})
              ∨ (P x = fv t' ∧ P (x ⋅stp δ) = fv (t' ⋅ δ))"
      by (metis P)
    moreover
    { assume "P x = {}" "P (x ⋅stp δ) = {}" hence ?thesis by simp }
    moreover
    { assume "P x = fv t ∪ fv t'" "P (x ⋅stp δ) = fv (t ⋅ δ) ∪ fv (t' ⋅ δ)"
      hence "fv t ⊆ wfrestrictedvarsst S ∪ V" "fv t' ⊆ wfrestrictedvarsst S ∪ V"
        using P_subset by auto
      hence "fv (t ⋅ δ) ⊆ wfrestrictedvarsst (S ⋅st δ) ∪ fvset (δ ` V)"
            "fv (t' ⋅ δ) ⊆ wfrestrictedvarsst (S ⋅st δ) ∪ fvset (δ ` V)"
        using P subst_apply_fv_subset_strand_trm2 assms by blast+
      hence ?thesis using ‹P (x ⋅stp δ) = fv (t ⋅ δ) ∪ fv (t' ⋅ δ)› by blast
    }
    moreover
    { assume "P x = fv t'" "P (x ⋅stp δ) = fv (t' ⋅ δ)"
      hence "fv t' ⊆ wfrestrictedvarsst S ∪ V" using P_subset by auto
      hence "fv (t' ⋅ δ) ⊆ wfrestrictedvarsst (S ⋅st δ) ∪ fvset (δ ` V)"
        using P subst_apply_fv_subset_strand_trm2 assms by blast+
      hence ?thesis using ‹P (x ⋅stp δ) = fv (t' ⋅ δ)› by blast
    }
    ultimately show ?thesis by metis
  qed
next
  case (Inequality X F)
  hence *: "fvstp x = fvpairs F - set X" "fvstp (x ⋅stp δ) = fvpairs (F ⋅pairs δ) - set X"
           "fvrcv x = {}" "fvrcv (x ⋅stp δ) = {}"
           "fvsnd x = {}" "fvsnd (x ⋅stp δ) = {}"
           "fveq ac x = {}" "fveq ac (x ⋅stp δ) = {}"
           "fvineq x = fvpairs F - set X" "fvineq (x ⋅stp δ) = fvpairs (F ⋅pairs δ) - set X"
           "fv_req ac x = {}" "fv_req ac (x ⋅stp δ) = {}"
    using δ(2) ineq_apply_subst[of δ X F] by force+
  hence **: "(P x = fvpairs F - set X ∧ P (x ⋅stp δ) = fvpairs (F ⋅pairs δ) - set X)
            ∨ (P x = {} ∧ P (x ⋅stp δ) = {})"
    by (metis P)
  moreover
  { assume "P x = {}" "P (x ⋅stp δ) = {}" hence ?thesis by simp }
  moreover
  { assume "P x = fvpairs F - set X" "P (x ⋅stp δ) = fvpairs (F ⋅pairs δ) - set X"
    hence "fvpairs F - set X ⊆ wfrestrictedvarsst S ∪ V" using P_subset by auto
    hence "fvpairs (F ⋅pairs δ) ⊆ wfrestrictedvarsst (S ⋅st δ) ∪ fvset (δ ` (V ∪ set X))"
    proof (induction F)
      case (Cons f G)
      hence IH: "fvpairs (G ⋅pairs δ) ⊆wfrestrictedvarsst (S ⋅st δ) ∪ fvset (δ ` (V ∪ set X))"
        by (metis (no_types, lifting) Diff_subset_conv UN_insert le_sup_iff
                  list.simps(15) fvpairs.simps)
      obtain t t' where f: "f = (t,t')" by (metis surj_pair)
      hence "fv t ⊆ wfrestrictedvarsst S ∪ (V ∪ set X)" "fv t' ⊆ wfrestrictedvarsst S ∪ (V ∪ set X)"
        using Cons.prems by auto
      hence "fv (t ⋅ δ) ⊆ wfrestrictedvarsst (S ⋅st δ) ∪ fvset (δ ` (V ∪ set X))"
            "fv (t' ⋅ δ) ⊆ wfrestrictedvarsst (S ⋅st δ) ∪ fvset (δ ` (V ∪ set X))"
        using subst_apply_fv_subset_strand_trm2[OF _ assms(3)] P
        by blast+
      thus ?case using f IH by (auto simp add: subst_apply_pairs_def)
    qed (simp add: subst_apply_pairs_def)
    moreover have "fvset (δ ` set X) = set X" using assms(4) Inequality by force
    ultimately have "fvpairs (F ⋅pairs δ) - set X ⊆ wfrestrictedvarsst (S ⋅st δ) ∪ fvset (δ ` V)"
      by fastforce
    hence ?thesis using ‹P (x ⋅stp δ) = fvpairs (F ⋅pairs δ) - set X› by blast
  }
  ultimately show ?thesis by metis
qed

lemma strand_subst_fv_bounded_if_img_bounded:
  assumes "range_vars δ ⊆ fvst S"
  shows "fvst (S ⋅st δ) ⊆ fvst S"
using subst_sends_strand_fv_to_img[of S δ] assms by blast

lemma strand_fv_subst_subset_if_subst_elim:
  assumes "subst_elim δ v" and "v ∈ fvst S ∨ bvarsst S ∩ (subst_domain δ ∪ range_vars δ) = {}"
  shows "v ∉ fvst (S ⋅st δ)"
proof (cases "v ∈ fvst S")
  case True thus ?thesis
  proof (induction S)
    case (Cons x S)
    have *: "v ∉ fvstp (x ⋅stp δ)"
    using assms(1)
    proof (cases x)
      case (Inequality X F)
      hence "subst_elim (rm_vars (set X) δ) v ∨ v ∈ set X" using assms(1) by blast
      moreover have "fvstp (Inequality X F ⋅stp δ) = fvpairs (F ⋅pairs rm_vars (set X) δ) - set X"
        using Inequality by auto
      ultimately have "v ∉ fvstp (Inequality X F ⋅stp δ)"
        by (induct F) (auto simp add: subst_elim_def subst_apply_pairs_def)
      thus ?thesis using Inequality by simp
    qed (simp_all add: subst_elim_def)
    moreover have "v ∉ fvst (S ⋅st δ)" using Cons.IH
    proof (cases "v ∈ fvst S")
      case False
      moreover have "v ∉ range_vars δ"
        by (simp add: subst_elimD''[OF assms(1)] range_vars_alt_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 subst_elim_def
    by (metis (mono_tags, opaque_lifting) fvset.simps imageE mem_simps(8) eval_term.simps(1))
qed

lemma strand_fv_subst_subset_if_subst_elim':
  assumes "subst_elim δ v" "v ∈ fvst S" "range_vars δ ⊆ fvst S"
  shows "fvst (S ⋅st δ) ⊂ fvst S"
using strand_fv_subst_subset_if_subst_elim[OF assms(1)] assms(2)
      strand_subst_fv_bounded_if_img_bounded[OF assms(3)]
by blast

lemma fv_ik_is_fv_rcv: "fvset (ikst S) = ⋃(set (map fvrcv S))"
by (induct S rule: ikst.induct) auto

lemma fv_ik_subset_fv_st[simp]: "fvset (ikst S) ⊆ wfrestrictedvarsst S"
by (induct S rule: ikst.induct) auto

lemma fv_assignment_rhs_subset_fv_st[simp]: "fvset (assignment_rhsst S) ⊆ wfrestrictedvarsst S"
by (induct S rule: assignment_rhsst.induct) force+

lemma fv_ik_subset_fv_st'[simp]: "fvset (ikst S) ⊆ fvst S"
by (induct S rule: ikst.induct) auto

lemma ikst_var_is_fv: "Var x ∈ subtermsset (ikst A) ⟹ x ∈ fvst A"
by (meson fv_ik_subset_fv_st'[of A] fv_subset_subterms subsetCE term.set_intros(3))

lemma fv_assignment_rhs_subset_fv_st'[simp]: "fvset (assignment_rhsst S) ⊆ fvst S"
by (induct S rule: assignment_rhsst.induct) auto

lemma ikst_assignment_rhsst_wfrestrictedvars_subset:
  "fvset (ikst A ∪ assignment_rhsst A) ⊆ wfrestrictedvarsst A"
using fv_ik_subset_fv_st[of A] fv_assignment_rhs_subset_fv_st[of A]
by simp+

lemma strand_step_id_subst[iff]: "x ⋅stp Var = x" by (cases x) auto

lemma strand_id_subst[iff]: "S ⋅st Var = S" using strand_step_id_subst by (induct S) auto

lemma strand_subst_vars_union_bound[simp]: "varsst (S ⋅st δ) ⊆ varsst S ∪ range_vars δ"
proof (induction S)
  case (Cons x S)
  moreover have "varsstp (x ⋅stp δ) ⊆ varsstp x ∪ range_vars δ" using subst_sends_fv_to_img[of _ δ]
  proof (cases x)
    case (Inequality X F)
    define δ' where "δ' ≡ rm_vars (set X) δ"
    have 0: "range_vars δ' ⊆ range_vars δ"
      using rm_vars_img[of "set X" δ]
      by (auto simp add: δ'_def subst_domain_def range_vars_alt_def)

    have "varsstp (x ⋅stp δ) = fvpairs (F ⋅pairs δ') ∪ set X" "varsstp x = fvpairs F ∪ set X"
      using Inequality by (auto simp add: δ'_def)
    moreover have "fvpairs (F ⋅pairs δ') ⊆ fvpairs F ∪ range_vars δ"
    proof (induction F)
      case (Cons f G)
      obtain t t' where f: "f = (t,t')" by atomize_elim auto
      hence "fvpairs (f#G ⋅pairs δ') = fv (t ⋅ δ') ∪ fv (t' ⋅ δ') ∪ fvpairs (G ⋅pairs δ')"
            "fvpairs (f#G) = fv t ∪ fv t' ∪ fvpairs G"
        by (auto simp add: subst_apply_pairs_def)
      thus ?case
        using 0 Cons.IH subst_sends_fv_to_img[of t δ'] subst_sends_fv_to_img[of t' δ']
        unfolding f by auto
    qed (simp add: subst_apply_pairs_def)
    ultimately show ?thesis by auto
  qed auto
  ultimately show ?case by auto
qed simp

lemma strand_vars_split:
  "varsst (S@S') = varsst S ∪ varsst S'"
  "wfrestrictedvarsst (S@S') = wfrestrictedvarsst S ∪ wfrestrictedvarsst S'"
  "fvst (S@S') = fvst S ∪ fvst S'"
by auto

lemma bvars_subst_ident: "bvarsst S = bvarsst (S ⋅st δ)"
unfolding bvarsst_def
by (induct S) (simp_all add: subst_apply_strand_step_def split: strand_step.splits)

lemma strand_subst_subst_idem:
  assumes "subst_idem δ" "subst_domain δ ∪ range_vars δ ⊆ fvst S" "subst_domain θ ∩ fvst S = {}"
          "range_vars δ ∩ bvarsst S = {}" "range_vars θ ∩ bvarsst S = {}"
  shows "(S ⋅st δ) ⋅st θ = (S ⋅st δ)"
  and   "(S ⋅st δ) ⋅st (θ ∘s δ) = (S ⋅st δ)"
proof -
  from assms(2,3) have "fvst (S ⋅st δ) ∩ subst_domain θ = {}"
    using subst_sends_strand_fv_to_img[of S δ] by blast
  thus "(S ⋅st δ) ⋅st θ = (S ⋅st δ)" by blast
  thus "(S ⋅st δ) ⋅st (θ ∘s δ) = (S ⋅st δ)"
    by (metis assms(1,4,5) bvars_subst_ident strand_subst_comp subst_idem_def)
qed

lemma strand_subst_img_bound:
  assumes "subst_domain δ ∪ range_vars δ ⊆ fvst S"
    and "(subst_domain δ ∪ range_vars δ) ∩ bvarsst S = {}"
  shows "range_vars δ ⊆ fvst (S ⋅st δ)"
proof -
  have "subst_domain δ ⊆ ⋃(set (map fvstp S))" by (metis (no_types) fvst_def Un_subset_iff assms(1))
  thus ?thesis
    unfolding range_vars_alt_def fvst_def
    by (metis subst_range.simps fv_set_mono fv_strand_subst Int_commute assms(2) image_Un
              le_iff_sup)
qed

lemma strand_subst_img_bound':
  assumes "subst_domain δ ∪ range_vars δ ⊆ varsst S"
    and "(subst_domain δ ∪ range_vars δ) ∩ bvarsst S = {}"
  shows "range_vars δ ⊆ varsst (S ⋅st δ)"
proof -
  have "(subst_domain δ ∪ fvset (δ ` subst_domain δ)) ∩ varsst S =
        subst_domain δ ∪ fvset (δ ` subst_domain δ)"
    using assms(1) by (metis inf.absorb_iff1 range_vars_alt_def subst_range.simps)
  hence "range_vars δ ⊆ fvst (S ⋅st δ)"
    using vars_snd_rcv_strand fv_snd_rcv_strand assms(2) strand_subst_img_bound
    unfolding range_vars_alt_def
    by (metis (no_types) inf_le2 inf_sup_distrib1 subst_range.simps sup_bot.right_neutral)
  thus "range_vars δ ⊆ varsst (S ⋅st δ)"
    by (metis fv_snd_rcv_strand le_supI1 vars_snd_rcv_strand)
qed

lemma strand_subst_all_fv_subset:
  assumes "fv t ⊆ fvst S" "(subst_domain δ ∪ range_vars δ) ∩ bvarsst S = {}"
  shows "fv (t ⋅ δ) ⊆ fvst (S ⋅st δ)"
using assms by (metis fv_strand_subst' Int_commute subst_apply_fv_subset)

lemma strand_subst_not_dom_fixed:
  assumes "v ∈ fvst S" and "v ∉ subst_domain δ"
  shows "v ∈ fvst (S ⋅st δ)"
using assms
proof (induction S)
  case (Cons x S')
  have 1: "⋀X. v ∉ subst_domain (rm_vars (set X) δ)"
    using Cons.prems(2) rm_vars_dom_subset by force
  
  show ?case
  proof (cases "v ∈ fvst S'")
    case True thus ?thesis using Cons.IH[OF _ Cons.prems(2)] by auto
  next
    case False
    hence 2: "v ∈ fvstp x" using Cons.prems(1) by simp
    hence "v ∈ fvstp (x ⋅stp δ)" using Cons.prems(2) subst_not_dom_fixed
    proof (cases x)
      case (Inequality X F)
      hence "v ∈ fvpairs F - set X" using 2 by simp
      hence "v ∈ fvpairs (F ⋅pairs rm_vars (set X) δ)"
        using subst_not_dom_fixed[OF _ 1]
        by (induct F) (auto simp add: subst_apply_pairs_def)
      thus ?thesis using Inequality 2 by auto
    qed (force simp add: subst_domain_def)+
    thus ?thesis by auto
  qed
qed simp

lemma strand_vars_unfold: "v ∈ varsst S ⟹ ∃S' x S''. S = S'@x#S'' ∧ v ∈ varsstp x"
proof (induction S)
  case (Cons x S) thus ?case
  proof (cases "v ∈ varsstp x")
    case True thus ?thesis by blast
  next
    case False
    hence "v ∈ varsst S" using Cons.prems by auto
    thus ?thesis using Cons.IH by (metis append_Cons)
  qed
qed simp

lemma strand_fv_unfold: "v ∈ fvst S ⟹ ∃S' x S''. S = S'@x#S'' ∧ v ∈ fvstp x"
proof (induction S)
  case (Cons x S) thus ?case
  proof (cases "v ∈ fvstp x")
    case True thus ?thesis by blast
  next
    case False
    hence "v ∈ fvst S" using Cons.prems by auto
    thus ?thesis using Cons.IH by (metis append_Cons)
  qed
qed simp

lemma subterm_if_in_strand_ik:
  "t ∈ ikst S ⟹ ∃ts. Receive ts ∈ set S ∧ t ⊑set set ts"
by (induct S rule: ikst_induct) auto

lemma fv_subset_if_in_strand_ik:
  "t ∈ ikst S ⟹ fv t ⊆ ⋃(set (map fvrcv S))"
proof -
  assume "t ∈ ikst S"
  then obtain ts where "Receive ts ∈ set S" "t ⊑set set ts" by (metis subterm_if_in_strand_ik)
  hence "fv t ⊆ fvset (set ts)" using subtermeq_vars_subset by auto
  thus ?thesis using in_strand_fv_subset_rcv[OF ‹Receive ts ∈ set S›] by auto
qed

lemma fv_subset_if_in_strand_ik':
  "t ∈ ikst S ⟹ fv t ⊆ fvst S"
using fv_subset_if_in_strand_ik[of t S] fv_snd_rcv_strand_subset(2)[of S] by blast

lemma vars_subset_if_in_strand_ik2:
  "t ∈ ikst S ⟹ fv t ⊆ wfrestrictedvarsst S"
using fv_subset_if_in_strand_ik[of t S] vars_snd_rcv_strand_subset2(2)[of S] by blast


subsection ‹Lemmata: Simple Strands›
lemma simple_Cons[dest]: "simple (s#S) ⟹ simple S"
unfolding simple_def by auto

lemma simple_split[dest]:
  assumes "simple (S@S')"
  shows "simple S" "simple S'"
using assms unfolding simple_def by auto

lemma simple_append[intro]: "⟦simple S; simple S'⟧ ⟹ simple (S@S')"
unfolding simple_def by auto

lemma simple_append_sym[sym]: "simple (S@S') ⟹ simple (S'@S)" by auto

lemma not_simple_if_snd_fun: "Fun f T ∈ set ts ⟹ S = S'@Send ts#S'' ⟹ ¬simple S"
by (metis simple_def list.set_cases list_all_append list_all_simps(1) simplestp.simps(5,6))

lemma not_list_all_elim: "¬list_all P A ⟹ ∃B x C. A = B@x#C ∧ ¬P x ∧ list_all P B"
proof (induction A rule: List.rev_induct)
  case (snoc a A)
  show ?case
  proof (cases "list_all P A")
    case True
    thus ?thesis using snoc.prems by auto
  next
    case False
    then obtain B x C where "A = B@x#C" "¬P x" "list_all P B" using snoc.IH[OF False] by auto
    thus ?thesis by auto
  qed
qed simp

lemma not_simplestp_elim:
  assumes "¬simplestp x"
  shows "(∃ts. x = Send ts ∧ (∄y. ts = [Var y])) ∨
         (∃a t t'. x = Equality a t t') ∨
         (∃X F. x = Inequality X F ∧ (∄ℐ. ineq_model ℐ X F))"
using assms by (cases x) (fastforce elim: simplestp.elims)+

lemma not_simple_elim:
  assumes "¬simple S"
  shows "(∃A B ts. S = A@Send ts#B ∧ (∄x. ts = [Var x]) ∧ simple A) ∨ 
         (∃A B a t t'. S = A@Equality a t t'#B ∧ simple A) ∨
         (∃A B X F. S = A@Inequality X F#B ∧ (∄ℐ. ineq_model ℐ X F) ∧ simple A)"
by (metis assms not_list_all_elim not_simplestp_elim simple_def)

lemma simple_snd_is_var: "⟦Send ts ∈ set S; simple S⟧ ⟹ ∃v. ts = [Var v]"
unfolding simple_def
by (metis list_all_append list_all_simps(1) simplestp.elims(2) split_list_first
          strand_step.distinct(1) strand_step.distinct(5) strand_step.inject(1)) 


subsection ‹Lemmata: Strand Measure›
lemma measurest_wellfounded: "wf measurest" unfolding measurest_def by simp

lemma strand_size_append[iff]: "sizest (S@S') = sizest S + sizest S'"
by (induct S) (auto simp add: sizest_def)

lemma strand_size_map_fun_lt[simp]:
  "sizest (map Send1 X) < size (Fun f X)"
  "sizest (map Send1 X) < sizest [Send [Fun f X]]"
  "sizest (map Receive1 X) < sizest [Receive [Fun f X]]"
  "sizest [Send X] < sizest [Send [Fun f X]]"
  "sizest [Receive X] < sizest [Receive [Fun f X]]"
by (induct X) (auto simp add: sizest_def)

lemma strand_size_rm_fun_lt[simp]:
  "sizest (S@S') < sizest (S@Send ts#S')"
  "sizest (S@S') < sizest (S@Receive ts#S')"
by (induct S) (auto simp add: sizest_def)

lemma strand_fv_card_map_fun_eq:
  "card (fvst (S@Send [Fun f X]#S')) = card (fvst (S@(map Send1 X)@S'))"
proof -
  have "fvst (S@Send [Fun f X]#S') = fvst (S@(map Send1 X)@S')" by auto
  thus ?thesis by simp
qed

lemma strand_fv_card_rm_fun_le[simp]: "card (fvst (S@S')) ≤ card (fvst (S@Send [Fun f X]#S'))"
by (force intro: card_mono)

lemma strand_fv_card_rm_eq_le[simp]: "card (fvst (S@S')) ≤ card (fvst (S@Equality a t t'#S'))"
by (force intro: card_mono)


subsection ‹Lemmata: Well-formed Strands›
lemma wf_prefix[dest]: "wfst V (S@S') ⟹ wfst V S"
by (induct S rule: wfst.induct) auto

lemma wf_vars_mono[simp]: "wfst V S ⟹ wfst (V ∪ W) S"
proof (induction S arbitrary: V)
  case (Cons x S) thus ?case
  proof (cases x)
    case (Send ts)
    hence "wfst (V ∪ fvset (set ts) ∪ W) S" using Cons.prems(1) Cons.IH by simp
    thus ?thesis by (metis Send sup_assoc sup_commute wfst.simps(3))
  next
    case (Equality a t t')
    show ?thesis
    proof (cases a)
      case Assign
      hence "wfst (V ∪ fv t ∪ W) S" "fv t' ⊆ V ∪ W" using Equality Cons.prems(1) Cons.IH by auto
      thus ?thesis using Equality Assign by (simp add: sup_commute sup_left_commute)
    next
      case Check thus ?thesis using Equality Cons by auto
    qed
  qed auto
qed simp

lemma wfstI[intro]: "wfrestrictedvarsst S ⊆ V ⟹ wfst V S"
proof (induction S)
  case (Cons x S) thus ?case
  proof (cases x)
    case (Send ts)
    hence "wfst V S" "V ∪ fvset (set ts) = V" using Cons by auto
    thus ?thesis using Send by simp
  next
    case (Equality a t t')
    show ?thesis
    proof (cases a)
      case Assign
      hence "wfst V S" "fv t' ⊆ V" using Equality Cons by auto
      thus ?thesis using wf_vars_mono Equality Assign by simp
    next
      case Check thus ?thesis using Equality Cons by auto
    qed
  qed simp_all
qed simp

lemma wfstI'[intro]: "⋃(fvrcv ` set S) ∪ ⋃(fv_req assign ` set S) ⊆ V ⟹ wfst V S"
proof (induction S)
  case (Cons x S) thus ?case
  proof (cases x)
    case (Equality a t t') thus ?thesis using Cons by (cases a) auto
  qed simp_all
qed simp

lemma wf_append_exec: "wfst V (S@S') ⟹ wfst (V ∪ wfvarsoccsst S) S'"
proof (induction S arbitrary: V)
  case (Cons x S V) thus ?case
  proof (cases x)
    case (Send ts)
    hence "wfst (V ∪ fvset (set ts) ∪ wfvarsoccsst S) S'" using Cons.prems Cons.IH by simp
    thus ?thesis using Send by (auto simp add: sup_assoc)
  next
    case (Equality a t t') show ?thesis
    proof (cases a)
      case Assign
      hence "wfst (V ∪ fv t ∪ wfvarsoccsst S) S'" using Equality Cons.prems Cons.IH by auto
      thus ?thesis using Equality Assign by (auto simp add: sup_assoc)
    next
      case Check
      hence "wfst (V ∪ wfvarsoccsst S) S'" using Equality Cons.prems Cons.IH by auto
      thus ?thesis using Equality Check by (auto simp add: sup_assoc)
    qed
  qed auto
qed simp

lemma wf_append_suffix:
  "wfst V S ⟹ wfrestrictedvarsst S' ⊆ wfrestrictedvarsst S ∪ V ⟹ wfst V (S@S')"
proof (induction V S rule: wfst_induct)
  case (ConsSnd V ts S)
  hence *: "wfst (V ∪ fvset (set ts)) S" by simp_all
  hence "wfrestrictedvarsst S' ⊆ wfrestrictedvarsst S ∪ (V ∪ fvset (set ts))"
    using ConsSnd.prems(2) by fastforce
  thus ?case using ConsSnd.IH * by simp
next
  case (ConsRcv V ts S)
  hence *: "fvset (set ts) ⊆ V" "wfst V S" by simp_all
  hence "wfrestrictedvarsst S' ⊆ wfrestrictedvarsst S ∪ V"
    using ConsRcv.prems(2) by fastforce
  thus ?case using ConsRcv.IH * by simp
next
  case (ConsEq V t t' S)
  hence *: "fv t' ⊆ V" "wfst (V ∪ fv t) S" by simp_all
  moreover have "varsstp (Equality Assign t t') = fv t ∪ fv t'"
    by simp
  moreover have "wfrestrictedvarsst (Equality Assign t t'#S) = fv t ∪ fv t' ∪ wfrestrictedvarsst S"
    by auto
  ultimately have "wfrestrictedvarsst S' ⊆ wfrestrictedvarsst S ∪ (V ∪ fv t)"
    using ConsEq.prems(2) by blast
  thus ?case using ConsEq.IH * by simp
qed (simp_all add: wfstI)

lemma wf_append_suffix':
  assumes "wfst V S"
    and "⋃(fvrcv ` set S') ∪ ⋃(fv_req assign ` set S') ⊆ wfvarsoccsst S ∪ V"
  shows "wfst V (S@S')"
using assms
proof (induction V S rule: wfst_induct)
  case (ConsSnd V ts S)
  hence *: "wfst (V ∪ fvset (set ts)) S" by simp_all
  have "wfvarsoccsst (send⟨ts⟩st#S) = fvset (set ts) ∪ wfvarsoccsst S"
    unfolding wfvarsoccsst_def by simp
  hence "(⋃a∈set S'. fvrcv a) ∪ (⋃a∈set S'. fv_req assign a) ⊆ wfvarsoccsst S ∪ (V ∪ fvset (set ts))"
    using ConsSnd.prems(2) unfolding wfvarsoccsst_def by auto
  thus ?case using ConsSnd.IH[OF *] by auto
next
  case (ConsEq V t t' S)
  hence *: "fv t' ⊆ V" "wfst (V ∪ fv t) S" by simp_all
  have "wfvarsoccsst (⟨assign: t ≐ t'⟩st#S) = fv t ∪ wfvarsoccsst S"
    unfolding wfvarsoccsst_def by simp
  hence "(⋃a∈set S'. fvrcv a) ∪ (⋃a∈set S'. fv_req assign a) ⊆ wfvarsoccsst S ∪ (V ∪ fv t)"
    using ConsEq.prems(2) unfolding wfvarsoccsst_def by auto
  thus ?case using ConsEq.IH[OF *(2)] *(1) by auto
qed (auto simp add: wfstI')

lemma wf_send_compose: "wfst V (S@(map Send1 X)@S') = wfst V (S@Send1 (Fun f X)#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
  proof (cases s)
    case (Equality ac t t') thus ?thesis using Cons by (cases ac) auto
  qed auto
qed

lemma wf_snd_append[iff]: "wfst V (S@[Send t]) = wfst V S"
by (induct S rule: wfst.induct) simp_all

lemma wf_snd_append': "wfst V S ⟹ wfst V (Send t#S)"
by simp

lemma wf_rcv_append[dest]: "wfst V (S@Receive t#S') ⟹ wfst V (S@S')"
by (induct S rule: wfst.induct) simp_all

lemma wf_rcv_append'[intro]:
  "⟦wfst V (S@S'); fvset (set ts) ⊆ wfrestrictedvarsst S ∪ V⟧ ⟹ wfst V (S@Receive ts#S')"
proof (induction S rule: wfst_induct)
  case (ConsRcv V t' S)
  hence "wfst V (S@S')" "fvset (set ts) ⊆ wfrestrictedvarsst S ∪ V" by (simp, fastforce)
  thus ?case using ConsRcv by auto
next
  case (ConsEq V t' t'' S)
  hence "fv t'' ⊆ V" by simp
  moreover have
      "wfrestrictedvarsst (Equality Assign t' t''#S) = fv t' ∪ fv t'' ∪ wfrestrictedvarsst S"
    by auto
  ultimately have "fvset (set ts) ⊆ wfrestrictedvarsst S ∪ (V ∪ fv t')"
    using ConsEq.prems(2) by blast
  thus ?case using ConsEq by auto
qed auto

lemma wf_rcv_append''[intro]:
  "⟦wfst V S; fvset (set ts) ⊆ ⋃(set (map fvsnd S))⟧ ⟹ wfst V (S@[Receive ts])"
by (induct S)
   (simp, metis vars_snd_rcv_strand_subset2(1) append_Nil2 le_supI1 order_trans wf_rcv_append')

lemma wf_rcv_append'''[intro]:
  "⟦wfst V S; fvset (set ts) ⊆ wfrestrictedvarsst S ∪ V⟧ ⟹ wfst V (S@[Receive ts])"
by (simp add: wf_rcv_append'[of _ _ "[]"])

lemma wf_eq_append[dest]:
  "wfst V (S@Equality a t t'#S') ⟹ fv t ⊆ wfrestrictedvarsst S ∪ V ⟹ wfst V (S@S')"
proof (induction S rule: wfst_induct)
  case (Nil V)
  hence "wfst (V ∪ fv t) S'" by (cases a) auto
  moreover have "V ∪ fv t = V" using Nil by auto
  ultimately show ?case by simp
next
  case (ConsRcv V us S)
  hence "wfst V (S @ Equality a t t' # S')" "fv t ⊆ wfrestrictedvarsst S ∪ V" "fvset (set us) ⊆ V"
    by fastforce+
  hence "wfst V (S@S')" using ConsRcv.IH by auto
  thus ?case using ‹fvset (set us) ⊆ V› by simp
next
  case (ConsEq V u u' S)
  hence "wfst (V ∪ fv u) (S@Equality a t t'#S')" "fv t ⊆ wfrestrictedvarsst S ∪ (V ∪ fv u)" "fv u' ⊆ V"
    by auto
  hence "wfst (V ∪ fv u) (S@S')" using ConsEq.IH by auto
  thus ?case using ‹fv u' ⊆ V› by simp
qed auto

lemma wf_eq_append'[intro]:
  "⟦wfst V (S@S'); fv t' ⊆ wfrestrictedvarsst S ∪ V⟧ ⟹ wfst V (S@Equality a t t'#S')"
proof (induction S rule: wfst_induct)
  case Nil thus ?case by (cases a) auto
next
  case (ConsEq V u u' S)
  hence "wfst (V ∪ fv u) (S@S')" "fv t' ⊆ wfrestrictedvarsst S ∪ V ∪ fv u"
    by fastforce+
  thus ?case using ConsEq by auto
next
  case (ConsEq2 V u u' S)
  hence "wfst V (S@S')" by auto
  thus ?case using ConsEq2 by auto
next
  case (ConsRcv V u S)
  hence "wfst V (S@S')" "fv t' ⊆ wfrestrictedvarsst S ∪ V"
    by fastforce+
  thus ?case using ConsRcv by auto
next
  case (ConsSnd V us S)
  hence "wfst (V ∪ fvset (set us)) (S@S')" "fv t' ⊆ wfrestrictedvarsst S ∪ (V ∪ fvset (set us))"
    by fastforce+
  thus ?case using ConsSnd by auto
qed auto

lemma wf_eq_append''[intro]:
  "⟦wfst V (S@S'); fv t' ⊆ wfvarsoccsst S ∪ V⟧ ⟹ wfst V (S@[Equality a t t']@S')"
proof (induction S rule: wfst_induct)
  case Nil thus ?case by (cases a) auto
next
  case (ConsEq V u u' S)
  hence "wfst (V ∪ fv u) (S@S')" "fv t' ⊆ wfvarsoccsst S ∪ V ∪ fv u" by fastforce+
  thus ?case using ConsEq by auto
next
  case (ConsEq2 V u u' S)
  hence "wfst (V ∪ fv u) (S@S')" "fv t' ⊆ wfvarsoccsst S ∪ V ∪ fv u" by fastforce+
  thus ?case using ConsEq2 by auto
next
  case (ConsRcv V u S)
  hence "wfst V (S@S')" "fv t' ⊆ wfvarsoccsst S ∪ V" by fastforce+
  thus ?case using ConsRcv by auto
next
  case (ConsSnd V us S)
  hence "wfst (V ∪ fvset (set us)) (S@S')" "fv t' ⊆ wfvarsoccsst S ∪ (V ∪ fvset (set us))" by auto
  thus ?case using ConsSnd by auto
qed auto

lemma wf_eq_append'''[intro]:
  "⟦wfst V S; fv t' ⊆ wfrestrictedvarsst S ∪ V⟧ ⟹ wfst V (S@[Equality a t t'])"
by (simp add: wf_eq_append'[of _ _ "[]"])

lemma wf_eq_check_append[dest]: "wfst V (S@Equality Check t t'#S') ⟹ wfst V (S@S')"
by (induct S rule: wfst.induct) simp_all

lemma wf_eq_check_append'[intro]: "wfst V (S@S') ⟹ wfst V (S@Equality Check t t'#S')"
by (induct S rule: wfst.induct) auto

lemma wf_eq_check_append''[intro]: "wfst V S ⟹ wfst V (S@[Equality Check t t'])"
by (induct S rule: wfst.induct) auto

lemma wf_ineq_append[dest]: "wfst V (S@Inequality X F#S') ⟹ wfst V (S@S')"
by (induct S rule: wfst.induct) simp_all

lemma wf_ineq_append'[intro]: "wfst V (S@S') ⟹ wfst V (S@Inequality X F#S')"
by (induct S rule: wfst.induct) auto

lemma wf_ineq_append''[intro]: "wfst V S ⟹ wfst V (S@[Inequality X F])"
by (induct S rule: wfst.induct) auto

lemma wf_Receive1_prefix:
  assumes "wfst X S"
    and "fvset (set ts) ⊆ X"
  shows "wfst X (map Receive1 ts@S)"
using assms by (induct ts) simp_all

lemma wf_Send1_prefix:
  assumes "wfst (X ∪ fvset (set ts)) S"
  shows "wfst X (map Send1 ts@S)"
using assms by (induct ts arbitrary: X) (simp, force simp add: Un_assoc)

lemma wf_rcv_fv_single[elim]: "wfst V (Receive ts#S') ⟹ fvset (set ts) ⊆ V"
by simp

lemma wf_rcv_fv: "wfst V (S@Receive ts#S') ⟹ fvset (set ts) ⊆ wfvarsoccsst S ∪ V"
proof (induction S arbitrary: V)
  case (Cons a S) thus ?case by (cases a) (auto split!: poscheckvariant.split)
qed simp

lemma wf_eq_fv: "wfst V (S@Equality Assign t t'#S') ⟹ fv t' ⊆ wfvarsoccsst S ∪ V"
proof (induction S arbitrary: V)
  case (Cons a S) thus ?case by (cases a) (auto split!: poscheckvariant.split)
qed simp

lemma wf_simple_fv_occurrence:
  assumes "wfst {} S" "simple S" "v ∈ wfrestrictedvarsst S"
  shows "∃Spre Ssuf. S = Spre@Send [Var v]#Ssuf ∧ v ∉ wfrestrictedvarsst Spre"
using assms
proof (induction S rule: List.rev_induct)
  case (snoc x S)
  from ‹wfst {} (S@[x])› have "wfst {} S" "wfst (wfrestrictedvarsst S) [x]"
    using wf_append_exec[THEN wf_vars_mono, of "{}" S "[x]" "wfrestrictedvarsst S - wfvarsoccsst S"]
          vars_snd_rcv_strand_subset2(4)[of S]
          Diff_partition[of "wfvarsoccsst S" "wfrestrictedvarsst S"]
    by auto
  from ‹simple (S@[x])› have "simple S" "simplestp x" unfolding simple_def by auto

  show ?case
  proof (cases "v ∈ wfrestrictedvarsst S")
    case False
    show ?thesis
    proof (cases x)
      case (Receive ts)
      hence "fvset (set ts) ⊆ wfrestrictedvarsst S" using ‹wfst (wfrestrictedvarsst S) [x]› by simp
      hence "v ∈ wfrestrictedvarsst S"
        using ‹v ∈ wfrestrictedvarsst (S@[x])› ‹x = Receive ts›
        by auto
      thus ?thesis using ‹x = Receive ts› snoc.IH[OF ‹wfst {} S› ‹simple S›] by fastforce
    next
      case (Send ts)
      hence "v ∈ varsstp x" using ‹v ∈ wfrestrictedvarsst (S@[x])› False by auto
      from Send obtain w where "ts = [Var w]" using ‹simplestp x›
        by (cases ts) (simp, metis in_set_conv_decomp simple_snd_is_var snoc.prems(2))
      hence "v = w" using ‹x = Send ts› ‹v ∈ varsstp x› by simp
      thus ?thesis using ‹x = Send ts› ‹v ∉ wfrestrictedvarsst S› ‹ts = [Var w]› by auto
    next
      case (Equality ac t t') thus ?thesis using snoc.prems(2) unfolding simple_def by auto
    next
      case (Inequality t t') thus ?thesis using False snoc.prems(3) by auto
    qed
  qed (use snoc.IH[OF ‹wfst {} S› ‹simple S›] in fastforce)
qed simp

lemma Unifier_strand_fv_subset:
  assumes g_in_ik: "t ∈ ikst S"
  and δ: "Unifier δ (Fun f X) t"
  and disj: "bvarsst S ∩ (subst_domain δ ∪ range_vars δ) = {}"
  shows "fv (Fun f X ⋅ δ) ⊆ ⋃(set (map fvrcv (S ⋅st δ)))"
by (metis (no_types) fv_subset_if_in_strand_ik[OF g_in_ik]
          disj δ fv_strand_subst subst_apply_fv_subset)

lemma wfst_induct'[consumes 1, case_names Nil ConsSnd ConsRcv ConsEq ConsEq2 ConsIneq]:
  fixes S::"('a,'b) strand"
  assumes "wfst V S"
          "P []"
          "⋀ts S. ⟦wfst V S; P S⟧ ⟹ P (S@[Send ts])"
          "⋀ts S. ⟦wfst V S; P S; fvset (set ts) ⊆ V ∪ wfvarsoccsst S⟧ ⟹ P (S@[Receive ts])"
          "⋀t t' S. ⟦wfst V S; P S; fv t' ⊆ V ∪ wfvarsoccsst S⟧ ⟹ P (S@[Equality Assign t t'])"
          "⋀t t' S. ⟦wfst V S; P S⟧ ⟹ P (S@[Equality Check t t'])"
          "⋀X F S. ⟦wfst V S; P S⟧ ⟹ P (S@[Inequality X F])"
  shows "P S"
using assms
proof (induction S rule: List.rev_induct)
  case (snoc x S)
  hence *: "wfst V S" "wfst (V ∪ wfvarsoccsst S) [x]" by (metis wf_prefix, metis wf_append_exec)
  have IH: "P S" using snoc.IH[OF *(1)] snoc.prems by auto
  note ** = snoc.prems(3,4,5,6,7)[OF *(1) IH] *(2)
  show ?case using **(1,2,4,5,6)
  proof (cases x)
    case (Equality ac t t')
    then show ?thesis using **(3,4,6) by (cases ac) auto
  qed auto
qed simp

lemma wf_subst_apply:
  "wfst V S ⟹ wfst (fvset (δ ` V)) (S ⋅st δ)"
proof (induction S arbitrary: V rule: wfst_induct)
  case (ConsRcv V ts S)
  hence "wfst V S" "fvset (set ts) ⊆ V" by simp_all
  hence "wfst (fvset (δ ` V)) (S ⋅st δ)" "fvset (set ts ⋅set δ) ⊆ fvset (δ ` V)"
    using ConsRcv.IH subst_apply_fv_subset by (simp, force)
  thus ?case by simp
next
  case (ConsSnd V ts S)
  hence "wfst (V ∪ fvset (set ts)) S" by simp
  hence "wfst (fvset (δ ` (V ∪ fvset (set ts)))) (S ⋅st δ)" using ConsSnd.IH by metis
  hence "wfst (fvset (δ ` V) ∪ fvset (δ ` fvset (set ts))) (S ⋅st δ)" by simp
  hence "wfst (fvset (δ ` V) ∪ fvset (set ts ⋅set δ)) (S ⋅st δ)" by (metis subst_apply_fv_unfold_set)
  thus ?case by simp
next
  case (ConsEq V t t' S)
  hence "wfst (V ∪ fv t) S" "fv t' ⊆ V" by auto
  hence "wfst (fvset (δ ` (V ∪ fv t))) (S ⋅st δ)" and *: "fv (t' ⋅ δ) ⊆ fvset (δ ` V)"
    using ConsEq.IH subst_apply_fv_subset by force+
  hence "wfst (fvset (δ ` V) ∪ fv (t ⋅ δ)) (S ⋅st δ)" using subst_apply_fv_union by metis
  thus ?case using * by simp
qed simp_all

lemma wf_unify:
  assumes wf: "wfst V (S@Send [Fun f X]#S')"
  and g_in_ik: "t ∈ ikst S"
  and δ: "Unifier δ (Fun f X) t"
  and disj: "bvarsst (S@Send [Fun f X]#S') ∩ (subst_domain δ ∪ range_vars δ) = {}"
  shows "wfst (fvset (δ ` V)) ((S@S') ⋅st δ)"
using assms
proof (induction S' arbitrary: V rule: List.rev_induct)
  case (snoc x S' V)
  have fun_fv_bound: "fv (Fun f X ⋅ δ) ⊆ ⋃(set (map fvrcv (S ⋅st δ)))"
    using snoc.prems(4) bvarsst_split Unifier_strand_fv_subset[OF g_in_ik δ] by auto
  hence "fv (Fun f X ⋅ δ) ⊆ fvset (ikst (S ⋅st δ))" using fv_ik_is_fv_rcv by metis
  hence "fv (Fun f X ⋅ δ) ⊆ wfrestrictedvarsst (S ⋅st δ)" using fv_ik_subset_fv_st[of "S ⋅st δ"] by blast
  hence *: "fv ((Fun f X) ⋅ δ) ⊆ wfrestrictedvarsst ((S@S') ⋅st δ)" by fastforce

  from snoc.prems(1) have "wfst V (S@Send [Fun f X]#S')"
    using wf_prefix[of V "S@Send [Fun f X]#S'" "[x]"] by simp
  hence **: "wfst (fvset (δ ` V)) ((S@S') ⋅st δ)"
    using snoc.IH[OF _ snoc.prems(2,3)] snoc.prems(4) by auto

  from snoc.prems(1) have ***: "wfst (V ∪ wfvarsoccsst (S@Send [Fun f X]#S')) [x]"
    using wf_append_exec[of V "(S@Send [Fun f X]#S')" "[x]"] by simp

  from snoc.prems(4) have disj':
      "bvarsst (S@S') ∩ (subst_domain δ ∪ range_vars δ) = {}"
      "set (bvarsstp x) ∩ (subst_domain δ ∪ range_vars δ) = {}"
    by auto

  show ?case
  proof (cases x)
    case (Send t)
    thus ?thesis using wf_snd_append[of "fvset (δ ` V)" "(S@S') ⋅st δ"] ** by auto
  next
    case (Receive t)
    hence "fvstp x ⊆ V ∪ wfvarsoccsst (S@Send [Fun f X]#S')" using *** by auto
    hence "fvstp x ⊆ V ∪ wfrestrictedvarsst (S@Send [Fun f X]#S')"
      using vars_snd_rcv_strand_subset2(4)[of "S@Send [Fun f X]#S'"] by blast
    hence "fvstp x ⊆ V ∪ fv (Fun f X) ∪ wfrestrictedvarsst (S@S')" by auto
    hence "fvstp (x ⋅stp δ) ⊆ fvset (δ ` V) ∪ fv ((Fun f X) ⋅ δ) ∪ wfrestrictedvarsst ((S@S') ⋅st δ)"
      by (metis (no_types) inf_sup_aci(5) subst_apply_fv_subset_strand2 subst_apply_fv_union disj')
    hence "fvstp (x ⋅stp δ) ⊆ fvset (δ ` V) ∪ wfrestrictedvarsst ((S@S') ⋅st δ)" using * by blast
    hence "fvset (set t ⋅set δ) ⊆ wfrestrictedvarsst ((S@S') ⋅st δ) ∪ fvset (δ ` V) "
      using ‹x = Receive t› by auto
    hence "wfst (fvset (δ ` V)) (((S@S') ⋅st δ)@[Receive (t ⋅list δ)])"
      using wf_rcv_append'''[OF **, of "t ⋅list δ"] by simp
    thus ?thesis using ‹x = Receive t› by auto
  next
    case (Equality ac s s') show ?thesis
    proof (cases ac)
      case Assign
      hence "fv s' ⊆ V ∪ wfvarsoccsst (S@Send [Fun f X]#S')" using Equality *** by auto
      hence "fv s' ⊆ V ∪ wfrestrictedvarsst (S@Send [Fun f X]#S')"
        using vars_snd_rcv_strand_subset2(4)[of "S@Send [Fun f X]#S'"] by blast
      hence "fv s' ⊆ V ∪ fv (Fun f X) ∪ wfrestrictedvarsst (S@S')" by auto
      moreover have "fv s' = fv_req ac x" "fv (s' ⋅ δ) = fv_req ac (x ⋅stp δ)"
        using Equality by simp_all
      ultimately have "fv (s' ⋅ δ) ⊆ fvset (δ ` V) ∪ fv (Fun f X ⋅ δ) ∪ wfrestrictedvarsst ((S@S') ⋅st δ)"
        using subst_apply_fv_subset_strand2[of "fveq ac" ac x]
        by (metis disj'(1) subst_apply_fv_subset_strand_trm2 subst_apply_fv_union sup_commute)
      hence "fv (s' ⋅ δ) ⊆ fvset (δ ` V) ∪ wfrestrictedvarsst ((S@S') ⋅st δ)" using * by blast
      hence "fv (s' ⋅ δ) ⊆ wfrestrictedvarsst ((S@S') ⋅st δ) ∪ fvset (δ ` V)"
        using ‹x = Equality ac s s'› by auto
      hence "wfst (fvset (δ ` V)) (((S@S') ⋅st δ)@[Equality ac (s ⋅ δ) (s' ⋅ δ)])"
        using wf_eq_append'''[OF **] by metis
      thus ?thesis using ‹x = Equality ac s s'› by auto
    next
      case Check thus ?thesis using wf_eq_check_append''[OF **] Equality by simp
    qed
  next
    case (Inequality t t') thus ?thesis using wf_ineq_append''[OF **] by simp
  qed
qed (auto dest: wf_subst_apply)

lemma wf_equality:
  assumes wf: "wfst V (S@Equality ac t t'#S')"
  and δ: "mgu t t' = Some δ"
  and disj: "bvarsst (S@Equality ac t t'#S') ∩ (subst_domain δ ∪ range_vars δ) = {}"
  shows "wfst (fvset (δ ` V)) ((S@S') ⋅st δ)"
using assms
proof (induction S' arbitrary: V rule: List.rev_induct)
  case Nil thus ?case using wf_prefix[of V S "[Equality ac t t']"] wf_subst_apply[of V S δ] by auto
next
  case (snoc x S' V) show ?case
  proof (cases ac)
    case Assign
    hence "fv t' ⊆ V ∪ wfvarsoccsst S"
      using wf_eq_fv[of V, of S t t' "S'@[x]"] snoc by auto
    hence "fv t' ⊆ V ∪ wfrestrictedvarsst S"
      using vars_snd_rcv_strand_subset2(4)[of S] by blast
    hence "fv t' ⊆ V ∪ wfrestrictedvarsst (S@S')" by force
    moreover have disj':
        "bvarsst (S@S') ∩ (subst_domain δ ∪ range_vars δ) = {}"
        "set (bvarsstp x) ∩ (subst_domain δ ∪ range_vars δ) = {}"
        "bvarsst (S@Equality ac t t'#S') ∩ (subst_domain δ ∪ range_vars δ) = {}"
      using snoc.prems(3) by auto
    ultimately have
        "fv (t' ⋅ δ) ⊆ fvset (δ ` V) ∪ wfrestrictedvarsst ((S@S') ⋅st δ)"
      by (metis inf_sup_aci(5) subst_apply_fv_subset_strand_trm2)
    moreover have "fv (t ⋅ δ) = fv (t' ⋅ δ)"
      by (metis MGU_is_Unifier[OF mgu_gives_MGU[OF δ]])
    ultimately have *:
        "fv (t ⋅ δ) ∪ fv (t' ⋅ δ) ⊆ fvset (δ ` V) ∪ wfrestrictedvarsst ((S@S') ⋅st δ)"
      by simp
  
    from snoc.prems(1) have "wfst V (S@Equality ac t t'#S')"
      using wf_prefix[of V "S@Equality ac t t'#S'"] by simp
    hence **: "wfst (fvset (δ ` V)) ((S@S') ⋅st δ)" by (metis snoc.IH δ disj'(3))
  
    from snoc.prems(1) have ***: "wfst (V ∪ wfvarsoccsst (S@Equality ac t t'#S')) [x]"
      using wf_append_exec[of V "(S@Equality ac t t'#S')" "[x]"] by simp
  
    show ?thesis
    proof (cases x)
      case (Send t)
      thus ?thesis using wf_snd_append[of "fvset (δ ` V)" "(S@S') ⋅st δ"] ** by auto
    next
      case (Receive s)
      hence "fvstp x ⊆ V ∪ wfvarsoccsst (S@Equality ac t t'#S')" using *** by auto
      hence "fvstp x ⊆ V ∪ wfrestrictedvarsst (S@Equality ac t t'#S')"
        using vars_snd_rcv_strand_subset2(4)[of "S@Equality ac t t'#S'"] by blast
      hence "fvstp x ⊆ V ∪ fv t ∪ fv t' ∪ wfrestrictedvarsst (S@S')"
        by (cases ac) auto
      hence "fvstp (x ⋅stp δ) ⊆ fvset (δ ` V) ∪ fv (t ⋅ δ) ∪ fv (t' ⋅ δ) ∪ wfrestrictedvarsst ((S@S') ⋅st δ)"
        using subst_apply_fv_subset_strand2[of fvstp]
        by (metis (no_types) inf_sup_aci(5) subst_apply_fv_union disj'(1,2))
      hence "fvstp (x ⋅stp δ) ⊆ fvset (δ ` V) ∪ wfrestrictedvarsst ((S@S') ⋅st δ)"
        when "ac = Assign"
        using * that by blast
      hence "fvset (set s ⋅set δ) ⊆ wfrestrictedvarsst ((S@S') ⋅st δ) ∪ (fvset (δ ` V))"
        when "ac = Assign"
        using ‹x = Receive s› that by auto
      hence "wfst (fvset (δ ` V)) (((S@S') ⋅st δ)@[Receive (s ⋅list δ)])"
        when "ac = Assign"
        using wf_rcv_append'''[OF **, of "s ⋅list δ"] that by simp
      thus ?thesis using ‹x = Receive s› Assign by auto
    next
      case (Equality ac' s s') show ?thesis
      proof (cases ac')
        case Assign
        hence "fv s' ⊆ V ∪ wfvarsoccsst (S@Equality ac t t'#S')" using *** Equality by auto
        hence "fv s' ⊆ V ∪ wfrestrictedvarsst (S@Equality ac t t'#S')"
          using vars_snd_rcv_strand_subset2(4)[of "S@Equality ac t t'#S'"] by blast
        hence "fv s' ⊆ V ∪ fv t ∪ fv t' ∪ wfrestrictedvarsst (S@S')"
          by (cases ac) auto
        moreover have "fv s' = fv_req ac' x" "fv (s' ⋅ δ) = fv_req ac' (x ⋅stp δ)"
          using Equality by simp_all
        ultimately have
            "fv (s' ⋅ δ) ⊆ fvset (δ ` V) ∪ fv (t ⋅ δ) ∪ fv (t' ⋅ δ) ∪ wfrestrictedvarsst ((S@S') ⋅st δ)"
          using subst_apply_fv_subset_strand2[of "fv_req ac'" ac' x]
          by (metis disj'(1) subst_apply_fv_subset_strand_trm2 subst_apply_fv_union sup_commute)
        hence "fv (s' ⋅ δ) ⊆ fvset (δ ` V) ∪ wfrestrictedvarsst ((S@S') ⋅st δ)"
          using * ‹ac = Assign› by blast
        hence ****:
            "fv (s' ⋅ δ) ⊆ wfrestrictedvarsst ((S@S') ⋅st δ) ∪ fvset (δ ` V)"
          using ‹x = Equality ac' s s'› ‹ac = Assign› by auto
        thus ?thesis
          using ‹x = Equality ac' s s'› ** **** wf_eq_append' ‹ac = Assign›
          by (metis (no_types, lifting) append.assoc append_Nil2 strand_step.case(3)
                strand_subst_hom subst_apply_strand_step_def)
      next
        case Check thus ?thesis using wf_eq_check_append''[OF **] Equality by simp
      qed
    next
      case (Inequality s s') thus ?thesis using wf_ineq_append''[OF **] by simp
    qed
  qed (metis snoc.prems(1) wf_eq_check_append wf_subst_apply)
qed

lemma wf_rcv_prefix_ground:
  "wfst {} ((map Receive M)@S) ⟹ varsst (map Receive M) = {}"
by (induct M) auto

lemma simple_wfvarsoccsst_is_fvsnd:
  assumes "simple S"
  shows "wfvarsoccsst S = ⋃(set (map fvsnd S))"
using assms unfolding simple_def
proof (induction S)
  case (Cons x S) thus ?case by (cases x) auto
qed simp

lemma wfst_simple_induct[consumes 2, case_names Nil ConsSnd ConsRcv ConsIneq]:
  fixes S::"('a,'b) strand"
  assumes "wfst V S" "simple S"
          "P []"
          "⋀v S. ⟦wfst V S; simple S; P S⟧ ⟹ P (S@[Send [Var v]])"
          "⋀ts S. ⟦wfst V S; simple S; P S; fvset (set ts) ⊆ V ∪ ⋃(set (map fvsnd S))⟧ ⟹ P (S@[Receive ts])"
          "⋀X F S. ⟦wfst V S; simple S; P S⟧ ⟹ P (S@[Inequality X F])"
  shows "P S"
using assms
proof (induction S rule: wfst_induct')
  case (ConsSnd t S)
  hence "P S" by auto
  obtain v where "t = [Var v]" using simple_snd_is_var[OF _ ‹simple (S@[Send t])›] by auto
  thus ?case using ConsSnd.prems(3)[OF ‹wfst V S› _ ‹P S›] ‹simple (S@[Send t])› by auto
next
  case (ConsRcv t S) thus ?case using simple_wfvarsoccsst_is_fvsnd[of "S@[Receive t]"] by auto
qed (auto simp add: simple_def)

lemma wf_trm_stp_dom_fv_disjoint:
  "⟦wfconstr S θ; t ∈ trmsst S⟧ ⟹ subst_domain θ ∩ fv t = {}"
unfolding wfconstr_def by force

lemma wf_constr_bvars_disj: "wfconstr S θ ⟹ (subst_domain θ ∪ range_vars θ) ∩ bvarsst S = {}"
unfolding range_vars_alt_def wfconstr_def by fastforce

lemma wf_constr_bvars_disj':
  assumes "wfconstr S θ" "subst_domain δ ∪ range_vars δ ⊆ fvst S"
  shows "(subst_domain δ ∪ range_vars δ) ∩ bvarsst S = {}" (is ?A)
  and "(subst_domain θ ∪ range_vars θ) ∩ bvarsst (S ⋅st δ) = {}" (is ?B)
proof -
  have "(subst_domain θ ∪ range_vars θ) ∩ bvarsst S = {}" "fvst S ∩ bvarsst S = {}"
    using assms(1) unfolding range_vars_alt_def wfconstr_def by fastforce+
  thus ?A and ?B using assms(2) bvars_subst_ident[of S δ] by blast+
qed

lemma (in intruder_model) wf_simple_strand_first_Send_var_split:
  assumes "wfst {} S" "simple S" "∃v ∈ wfrestrictedvarsst S. t ⋅ ℐ = ℐ v"
  shows "∃v Spre Ssuf. S = Spre@Send [Var v]#Ssuf ∧ t ⋅ ℐ = ℐ v
                      ∧ ¬(∃w ∈ wfrestrictedvarsst Spre. t ⋅ ℐ = ℐ w)"
    (is "?P S")
using assms
proof (induction S rule: wfst_simple_induct)
  case (ConsSnd v S) show ?case
  proof (cases "∃w ∈ wfrestrictedvarsst S. t ⋅ ℐ = ℐ 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 "fvset (set t') ⊆ wfrestrictedvarsst S"
    using ConsRcv.hyps(3) vars_snd_rcv_strand_subset2(1) by force
  hence "∃v ∈ wfrestrictedvarsst S. t ⋅ ℐ = ℐ v"
    using ConsRcv.prems(1) by fastforce
  hence "?P S" by (metis ConsRcv.IH)
  thus ?case by fastforce 
next
  case (ConsIneq X F S)
  moreover have "wfrestrictedvarsst (S @ [Inequality X F]) = wfrestrictedvarsst S" by auto
  ultimately have "?P S" by blast
  thus ?case by fastforce
qed simp

lemma (in intruder_model) wf_strand_first_Send_var_split:
  assumes "wfst {} S" "∃v ∈ wfrestrictedvarsst S. t ⋅ ℐ ⊑ ℐ v"
  shows "∃Spre Ssuf. ¬(∃w ∈ wfrestrictedvarsst Spre. t ⋅ ℐ ⊑ ℐ w)
            ∧ ((∃t'. S = Spre@Send t'#Ssuf ∧ t ⋅ ℐ ⊑set set t' ⋅set ℐ)
               ∨ (∃t' t''. S = Spre@Equality Assign t' t''#Ssuf ∧ t ⋅ ℐ ⊑ t' ⋅ ℐ))"
    (is "∃Spre Ssuf. ?P Spre ∧ ?Q S Spre Ssuf")
using assms
proof (induction S rule: wfst_induct')
  case (ConsSnd ts' S) show ?case
  proof (cases "∃w ∈ wfrestrictedvarsst S. t ⋅ ℐ ⊑ ℐ w")
    case True
    then obtain Spre Ssuf where "?P Spre" "?Q S Spre Ssuf"
      using ConsSnd.IH by atomize_elim auto
    thus ?thesis by fastforce
  next
    case False
    then obtain v where v: "v ∈ fvset (set ts')" "t ⋅ ℐ ⊑ ℐ v"
      using ConsSnd.prems by auto
    then obtain t' where t': "t' ∈ set ts'" "v ∈ fv t'" by auto
    have "t ⋅ ℐ ⊑ t' ⋅ ℐ"
      using v(2) t'(2) subst_mono[of "Var v" t' ℐ] vars_iff_subtermeq[of v] term.order_trans
      by auto
    hence "t ⋅ ℐ ⊑set set ts' ⋅set ℐ" using v(1) t'(1) by blast
    thus ?thesis using False v by auto
  qed
next
  case (ConsRcv t' S)
  have "fvset (set t') ⊆ wfrestrictedvarsst S"
    using ConsRcv.hyps vars_snd_rcv_strand_subset2(4)[of S] by blast
  hence "∃v ∈ wfrestrictedvarsst S. t ⋅ ℐ ⊑ ℐ v"
    using ConsRcv.prems by fastforce
  then obtain Spre Ssuf where "?P Spre" "?Q S Spre Ssuf"
    using ConsRcv.IH by atomize_elim auto
  thus ?case by fastforce
next
  case (ConsEq s s' S)
  have *: "fv s' ⊆ wfrestrictedvarsst S"
    using ConsEq.hyps vars_snd_rcv_strand_subset2(4)[of S]
    by blast
  show ?case
  proof (cases "∃v ∈ wfrestrictedvarsst S. t ⋅ ℐ ⊑ ℐ v")
    case True
    then obtain Spre Ssuf where "?P Spre" "?Q S Spre Ssuf"
      using ConsEq.IH by atomize_elim auto
    thus ?thesis by fastforce
  next
    case False
    then obtain v where "v ∈ fv s" "t ⋅ ℐ ⊑ ℐ v" using ConsEq.prems * by auto
    hence "t ⋅ ℐ ⊑ s ⋅ ℐ"
      using vars_iff_subtermeq[of v s] subst_mono[of "Var v" s ℐ] term.order_trans
      by auto
    thus ?thesis using False by fastforce
  qed
next
  case (ConsEq2 s s' S)
  have "wfrestrictedvarsst (S@[Equality Check s s']) = wfrestrictedvarsst S" by auto
  hence "∃v ∈ wfrestrictedvarsst S. t ⋅ ℐ ⊑ ℐ v" using ConsEq2.prems by metis
  then obtain Spre Ssuf where "?P Spre" "?Q S Spre Ssuf"
    using ConsEq2.IH by atomize_elim auto
  thus ?case by fastforce
next
  case (ConsIneq X F S)
  hence "∃v ∈ wfrestrictedvarsst S. t ⋅ ℐ ⊑ ℐ v" by fastforce
  then obtain Spre Ssuf where "?P Spre" "?Q S Spre Ssuf"
    using ConsIneq.IH by atomize_elim auto
  thus ?case by fastforce
qed simp


subsection ‹Constraint Semantics›
context intruder_model
begin

subsubsection ‹Definitions›
text ‹The constraint semantics in which the intruder is limited to composition only›
fun strand_sem_c::"('fun,'var) terms ⇒ ('fun,'var) strand ⇒ ('fun,'var) subst ⇒ bool" (‹⟦_; _⟧c›)
where
  "⟦M; []⟧c = (λℐ. True)"
| "⟦M; Send ts#S⟧c = (λℐ. (∀t ∈ set ts. M ⊢c t ⋅ ℐ) ∧ ⟦M; S⟧c ℐ)"
| "⟦M; Receive ts#S⟧c = (λℐ. ⟦(set ts ⋅set ℐ) ∪ M; S⟧c ℐ)"
| "⟦M; Equality _ t t'#S⟧c = (λℐ. t ⋅ ℐ = t' ⋅ ℐ ∧ ⟦M; S⟧c ℐ)"
| "⟦M; Inequality X F#S⟧c = (λℐ. ineq_model ℐ X F ∧ ⟦M; S⟧c ℐ)"

definition constr_sem_c (‹_ ⊨c ⟨_,_⟩›) where "ℐ ⊨c ⟨S,θ⟩ ≡ (θ supports ℐ ∧ ⟦{}; S⟧c ℐ)"
abbreviation constr_sem_c' (‹_ ⊨c ⟨_⟩› 90) where "ℐ ⊨c ⟨S⟩ ≡ ℐ ⊨c ⟨S,Var⟩"

text ‹The full constraint semantics›
fun strand_sem_d::"('fun,'var) terms ⇒ ('fun,'var) strand ⇒ ('fun,'var) subst ⇒ bool" (‹⟦_; _⟧d›)
where
  "⟦M; []⟧d = (λℐ. True)"
| "⟦M; Send ts#S⟧d = (λℐ. (∀t ∈ set ts. M ⊢ t ⋅ ℐ) ∧ ⟦M; S⟧d ℐ)"
| "⟦M; Receive ts#S⟧d = (λℐ. ⟦(set ts ⋅set ℐ) ∪ M; S⟧d ℐ)"
| "⟦M; Equality _ t t'#S⟧d = (λℐ. t ⋅ ℐ = t' ⋅ ℐ ∧ ⟦M; S⟧d ℐ)"
| "⟦M; Inequality X F#S⟧d = (λℐ. ineq_model ℐ X F ∧ ⟦M; S⟧d ℐ)"

definition constr_sem_d (‹_ ⊨ ⟨_,_⟩›) where "ℐ ⊨ ⟨S,θ⟩ ≡ (θ supports ℐ ∧ ⟦{}; S⟧d ℐ)"
abbreviation constr_sem_d' (‹_ ⊨ ⟨_⟩› 90) where "ℐ ⊨ ⟨S⟩ ≡ ℐ ⊨ ⟨S,Var⟩"

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


subsubsection ‹Lemmata›
lemma strand_sem_d_if_c: "ℐ ⊨c ⟨S,θ⟩ ⟹ ℐ ⊨ ⟨S,θ⟩"
proof -
  assume *: "ℐ ⊨c ⟨S,θ⟩"
  { fix M have "⟦M; S⟧c ℐ ⟹ ⟦M; S⟧d ℐ"
    proof (induction S rule: strand_sem_induct)
      case (ConsSnd M ts S)
      hence "∀t ∈ set ts. M ⊢c t ⋅ ℐ" "⟦M; S⟧d ℐ" by auto
      thus ?case using strand_sem_d.simps(2)[of M _ S] by auto
    qed (auto simp add: ineq_model_def)
  }
  thus ?thesis using * by (simp add: constr_sem_c_def constr_sem_d_def)
qed

lemma strand_sem_mono_ik:
  "⟦M ⊆ M'; ⟦M; S⟧c θ⟧ ⟹ ⟦M'; S⟧c θ" (is "⟦?A'; ?A''⟧ ⟹ ?A")
  "⟦M ⊆ M'; ⟦M; S⟧d θ⟧ ⟹ ⟦M'; S⟧d θ" (is "⟦?B'; ?B''⟧ ⟹ ?B")
proof -
  show "⟦?A'; ?A''⟧ ⟹ ?A"
  proof (induction M S arbitrary: M M' rule: strand_sem_induct)
    case (ConsRcv M ts S)
    thus ?case using ConsRcv.IH[of "(set ts ⋅set θ) ∪ M" "(set ts ⋅set θ) ∪ M'"] by auto
  next
    case (ConsSnd M ts S)
    hence "∀t ∈ set ts. M ⊢c t ⋅ θ" "⟦M'; S⟧c θ" by auto
    hence "∀t ∈ set ts. M' ⊢c t ⋅ θ" using ideduct_synth_mono ‹M ⊆ M'› by metis
    thus ?case using ‹⟦M'; S⟧c θ› by simp
  qed auto

  show "⟦?B'; ?B''⟧ ⟹ ?B"
  proof (induction M S arbitrary: M M' rule: strand_sem_induct)
    case (ConsRcv M ts S)
    thus ?case using ConsRcv.IH[of "(set ts ⋅set θ) ∪ M" "(set ts ⋅set θ) ∪ M'"] by auto
  next
    case (ConsSnd M ts S)
    hence "∀t ∈ set ts. M ⊢ t ⋅ θ" "⟦M'; S⟧d θ" by auto
    hence "∀t ∈ set ts. M' ⊢ t ⋅ θ" using ideduct_mono ‹M ⊆ M'› by metis
    thus ?case using ‹⟦M'; S⟧d θ› by simp
  qed auto
qed

context
begin
private lemma strand_sem_split_left:
  "⟦M; S@S'⟧c θ ⟹ ⟦M; S⟧c θ"
  "⟦M; S@S'⟧d θ ⟹ ⟦M; S⟧d θ"
proof (induct S arbitrary: M)
  case (Cons x S)
  { case 1 thus ?case using Cons by (cases x) simp_all }
  { case 2 thus ?case using Cons by (cases x) simp_all }
qed simp_all

private lemma strand_sem_split_right:
  "⟦M; S@S'⟧c θ ⟹ ⟦M ∪ (ikst S ⋅set θ); S'⟧c θ"
  "⟦M; S@S'⟧d θ ⟹ ⟦M ∪ (ikst S ⋅set θ); S'⟧d θ"
proof (induction S arbitrary: M rule: ikst_induct)
  case (ConsRcv ts S)
  { case 1 thus ?case
      using ConsRcv.IH(1)[of "(set ts ⋅set θ) ∪ M"]
      by (simp add: Un_commute Un_left_commute image_Un)
  }
  { case 2 thus ?case
      using ConsRcv.IH(2)[of "(set ts ⋅set θ) ∪ M"]
      by (simp add: Un_commute Un_left_commute image_Un)
  }
qed simp_all

lemmas strand_sem_split[dest] =
  strand_sem_split_left(1) strand_sem_split_right(1)
  strand_sem_split_left(2) strand_sem_split_right(2)
end

lemma strand_sem_Send_split[dest]:
  "⟦⟦M; map Send T⟧c θ; ts ∈ set T⟧ ⟹ ⟦M; [Send ts]⟧c θ" (is "⟦?A'; ?A''⟧ ⟹ ?A")
  "⟦⟦M; map Send T⟧d θ; ts ∈ set T⟧ ⟹ ⟦M; [Send ts]⟧d θ" (is "⟦?B'; ?B''⟧ ⟹ ?B")
  "⟦⟦M; map Send T@S⟧c θ; ts ∈ set T⟧ ⟹ ⟦M; Send ts#S⟧c θ" (is "⟦?C'; ?C''⟧ ⟹ ?C")
  "⟦⟦M; map Send T@S⟧d θ; ts ∈ set T⟧ ⟹ ⟦M; Send ts#S⟧d θ" (is "⟦?D'; ?D''⟧ ⟹ ?D")
  "⟦⟦M; map Send1 T'⟧c θ; t ∈ set T'⟧ ⟹ ⟦M; [Send1 t]⟧c θ" (is "⟦?E'; ?E''⟧ ⟹ ?E")
  "⟦⟦M; map Send1 T'⟧d θ; t ∈ set T'⟧ ⟹ ⟦M; [Send1 t]⟧d θ" (is "⟦?F'; ?F''⟧ ⟹ ?F")
  "⟦⟦M; map Send1 T'@S⟧c θ; t ∈ set T'⟧ ⟹ ⟦M; Send1 t#S⟧c θ" (is "⟦?G'; ?G''⟧ ⟹ ?G")
  "⟦⟦M; map Send1 T'@S⟧d θ; t ∈ set T'⟧ ⟹ ⟦M; Send1 t#S⟧d θ" (is "⟦?H'; ?H''⟧ ⟹ ?H")
proof -
  show A: "⟦?A'; ?A''⟧ ⟹ ?A" by (induct "map Send T" arbitrary: T rule: strand_sem_c.induct) auto
  show B: "⟦?B'; ?B''⟧ ⟹ ?B" by (induct "map Send T" arbitrary: T rule: strand_sem_d.induct) auto
  show "⟦?C'; ?C''⟧ ⟹ ?C" "⟦?D'; ?D''⟧ ⟹ ?D"
    using list.set_map list.simps(8) set_empty ik_snd_empty sup_bot.right_neutral
    by (metis (no_types, lifting) A strand_sem_split(1,2) strand_sem_c.simps(2),
        metis (no_types, lifting) B strand_sem_split(3,4) strand_sem_d.simps(2))

  show "⟦?E'; ?E''⟧ ⟹ ?E"
    by (induct "map Send1 T'" arbitrary: T' rule: strand_sem_c.induct) auto

  show "⟦?F'; ?F''⟧ ⟹ ?F"
    by (induct "map Send1 T'" arbitrary: T' rule: strand_sem_c.induct) auto

  show "⟦?G'; ?G''⟧ ⟹ ?G"
  proof (induction "map Send1 T'" arbitrary: T' rule: strand_sem_c.induct)
    case (2 M ts S')
    obtain t' T'' where ts: "ts = [t']" "T' = t'#T''" "S' = map Send1 T''"
      using "2.hyps"(2) by blast
    thus ?case using "2.prems" "2.hyps"(1)
    proof (cases "t = t'")
      case True
      have "ikst (map Send1 T') ⋅set θ = {}" by force
      hence "⟦M; [Send1 t]⟧c θ" "⟦M; S⟧c θ" using "2.prems"(1) unfolding ts(2) True by auto
      thus ?thesis by simp
    qed auto
  qed auto

  show "⟦?H'; ?H''⟧ ⟹ ?H"
  proof (induction "map Send1 T'" arbitrary: T' rule: strand_sem_c.induct)
    case (2 M ts S')
    obtain t' T'' where ts: "ts = [t']" "T' = t'#T''" "S' = map Send1 T''"
      using "2.hyps"(2) by blast
    thus ?case using "2.prems" "2.hyps"(1)
    proof (cases "t = t'")
      case True
      have "ikst (map Send1 T') ⋅set θ = {}" by force
      hence "⟦M; [Send1 t]⟧d θ" "⟦M; S⟧d θ" using "2.prems"(1) unfolding ts(2) True by auto
      thus ?thesis by simp
    qed auto
  qed auto
qed

lemma strand_sem_Send_map:
  "(⋀ts. ts ∈ set T ⟹ ⟦M; [Send ts]⟧c ℐ) ⟹ ⟦M; map Send T⟧c ℐ"
  "(⋀ts. ts ∈ set T ⟹ ⟦M; [Send ts]⟧d ℐ) ⟹ ⟦M; map Send T⟧d ℐ"
  "(⋀t. t ∈ set T' ⟹ ⟦M; [Send1 t]⟧c ℐ) ⟹ ⟦M; map Send1 T'⟧c ℐ"
  "(⋀t. t ∈ set T' ⟹ ⟦M; [Send1 t]⟧d ℐ) ⟹ ⟦M; map Send1 T'⟧d ℐ"
  "⟦M; map Send1 T'⟧c ℐ ⟷ ⟦M; [Send T']⟧c ℐ"
  "⟦M; map Send1 T'⟧d ℐ ⟷ ⟦M; [Send T']⟧d ℐ"
proof -
  show "(⋀ts. ts ∈ set T ⟹ ⟦M; [Send ts]⟧c ℐ) ⟹ ⟦M; map Send T⟧c ℐ"
       "(⋀ts. ts ∈ set T ⟹ ⟦M; [Send ts]⟧d ℐ) ⟹ ⟦M; map Send T⟧d ℐ"
    by (induct T) auto

  show "(⋀t. t ∈ set T' ⟹ ⟦M; [Send1 t]⟧c ℐ) ⟹ ⟦M; map Send1 T'⟧c ℐ"
       "(⋀t. t ∈ set T' ⟹ ⟦M; [Send1 t]⟧d ℐ) ⟹ ⟦M; map Send1 T'⟧d ℐ"
    by (induct T') auto

  show "⟦M; map Send1 T'⟧c ℐ ⟷ ⟦M; [Send T']⟧c ℐ"
       "⟦M; map Send1 T'⟧d ℐ ⟷ ⟦M; [Send T']⟧d ℐ"
    by (induct T') auto
qed

lemma strand_sem_Receive_map:
  "⟦M; map Receive T⟧c ℐ" "⟦M; map Receive T⟧d ℐ"
  "⟦M; map Receive1 T'⟧c ℐ" "⟦M; map Receive1 T'⟧d ℐ"
  "⟦M; [Receive T']⟧c ℐ" "⟦M; [Receive T']⟧d ℐ"
proof -
  show "⟦M; map Receive T⟧c ℐ" "⟦M; map Receive T⟧d ℐ" by (induct T arbitrary: M) auto
  show "⟦M; map Receive1 T'⟧c ℐ" "⟦M; map Receive1 T'⟧d ℐ" by (induct T' arbitrary: M) auto
  show "⟦M; [Receive T']⟧c ℐ" "⟦M; [Receive T']⟧d ℐ" by (induct T' arbitrary: M) auto
qed

lemma strand_sem_append[intro]:
  "⟦⟦M; S⟧c θ; ⟦M ∪ (ikst S ⋅set θ); S'⟧c θ⟧ ⟹ ⟦M; S@S'⟧c θ"
  "⟦⟦M; S⟧d θ; ⟦M ∪ (ikst S ⋅set θ); S'⟧d θ⟧ ⟹ ⟦M; S@S'⟧d θ"
proof (induction S arbitrary: M)
  case (Cons x S) 
  { case 1 thus ?case using Cons
    proof (cases x)
      case (Receive ts) thus ?thesis
        using 1 Cons.IH(1)[of "(set ts ⋅set θ) ∪ M"]
              strand_sem_c.simps(3)[of M ts] image_Un[of "λt. t ⋅ θ" "set ts" "ikst S"]
        by (metis (no_types, lifting) ikst.simps(2) Un_assoc Un_commute append_Cons)
    qed auto
  }
  { case 2 thus ?case using Cons
    proof (cases x)
      case (Receive ts) thus ?thesis
        using 2 Cons.IH(2)[of "(set ts ⋅set θ) ∪ M"]
              strand_sem_d.simps(3)[of M ts] image_Un[of "λt. t ⋅ θ" "set ts" "ikst S"]
        by (metis (no_types, lifting) ikst.simps(2) Un_assoc Un_commute append_Cons)
    qed auto
  }
qed simp_all

lemma ineq_model_subst:
  fixes F::"(('a,'b) term × ('a,'b) term) list"
  assumes "(subst_domain δ ∪ range_vars δ) ∩ set X = {}"
    and "ineq_model (δ ∘s θ) X F"
  shows "ineq_model θ X (F ⋅pairs δ)"
proof -
  { fix σ::"('a,'b) subst" and t t'
    assume σ: "subst_domain σ = set X" "ground (subst_range σ)"
        and *: "∃(s,t) ∈ set F. s ⋅ (σ ∘s (δ ∘s θ)) ≠ t ⋅ (σ ∘s (δ ∘s θ))"
    obtain f where f: "f ∈ set F" "fst f ⋅ σ ∘s (δ ∘s θ) ≠ snd f ⋅ σ ∘s (δ ∘s θ)"
      using * by (induct F) force+
    have "σ ∘s (δ ∘s θ) = δ ∘s (σ ∘s θ)"
      by (metis (no_types, lifting) σ subst_compose_assoc assms(1) inf_sup_aci(1)
              subst_comp_eq_if_disjoint_vars sup_inf_absorb range_vars_alt_def) 
    hence "(fst f ⋅ δ) ⋅ σ ∘s θ ≠ (snd f ⋅ δ) ⋅ σ ∘s θ" using f by auto
    moreover have "(fst f ⋅ δ, snd f ⋅ δ) ∈ set (F ⋅pairs δ)"
      using f(1) by (auto simp add: subst_apply_pairs_def)
    ultimately have "∃(s,t) ∈ set (F ⋅pairs δ). s ⋅ (σ ∘s θ) ≠ t ⋅ (σ ∘s θ)"
      using f(1) Bex_set by fastforce
  }
  thus ?thesis using assms unfolding ineq_model_def by simp
qed

lemma ineq_model_subst':
  fixes F::"(('a,'b) term × ('a,'b) term) list"
  assumes "(subst_domain δ ∪ range_vars δ) ∩ set X = {}"
    and "ineq_model θ X (F ⋅pairs δ)"
  shows "ineq_model (δ ∘s θ) X F"
proof -
  { fix σ::"('a,'b) subst" and t t'
    assume σ: "subst_domain σ = set X" "ground (subst_range σ)"
        and *: "∃(s,t) ∈ set (F ⋅pairs δ). s ⋅ (σ ∘s θ) ≠ t ⋅ (σ ∘s θ)"
    obtain f where f: "f ∈ set (F ⋅pairs δ)" "fst f ⋅ σ ∘s θ ≠ snd f ⋅ σ ∘s θ"
      using * by (induct F) auto
    then obtain g where g: "g ∈ set F" "f = g ⋅p δ" by (auto simp add: subst_apply_pairs_def)
    have "σ ∘s (δ ∘s θ) = δ ∘s (σ ∘s θ)"
      by (metis (no_types, lifting) σ subst_compose_assoc assms(1) inf_sup_aci(1)
              subst_comp_eq_if_disjoint_vars sup_inf_absorb range_vars_alt_def) 
    hence "fst g ⋅ σ ∘s (δ ∘s θ) ≠ snd g ⋅ σ ∘s (δ ∘s θ)"
      using f(2) g by (simp add: prod.case_eq_if)
    hence "∃(s,t) ∈ set F. s ⋅ (σ ∘s (δ ∘s θ)) ≠ t ⋅ (σ ∘s (δ ∘s θ))"
      using g Bex_set by fastforce
  }
  thus ?thesis using assms unfolding ineq_model_def by simp
qed

lemma ineq_model_ground_subst:
  fixes F::"(('a,'b) term × ('a,'b) term) list"
  assumes "fvpairs F - set X ⊆ subst_domain δ"
    and "ground (subst_range δ)"
    and "ineq_model δ X F"
  shows "ineq_model (δ ∘s θ) X F"
proof -
  { fix σ::"('a,'b) subst" and t t'
    assume σ: "subst_domain σ = set X" "ground (subst_range σ)"
        and *: "∃(s,t) ∈ set F. s ⋅ (σ ∘s δ) ≠ t ⋅ (σ ∘s δ )"
    obtain f where f: "f ∈ set F" "fst f ⋅ σ ∘s δ ≠ snd f ⋅ σ ∘s δ"
      using * by (induct F) force+
    hence "fv (fst f) ⊆ fvpairs F" "fv (snd f) ⊆ fvpairs F" by auto
    hence "fv (fst f) - set X ⊆ subst_domain δ" "fv (snd f) - set X ⊆ subst_domain δ"
      using assms(1) by auto
    hence "fv (fst f ⋅ σ) ⊆ subst_domain δ" "fv (snd f ⋅ σ) ⊆ subst_domain δ"
      using σ by (simp_all add: range_vars_alt_def subst_fv_unfold_ground_img)
    hence "fv (fst f ⋅ σ ∘s δ) = {}" "fv (snd f ⋅ σ ∘s δ) = {}"
      using assms(2) by (simp_all add: subst_fv_dom_ground_if_ground_img)
    hence "fst f ⋅ σ ∘s (δ ∘s θ) ≠ snd f ⋅ σ ∘s (δ ∘s θ)" using f(2) subst_ground_ident by fastforce 
    hence "∃(s,t) ∈ set F. s ⋅ (σ ∘s (δ ∘s θ)) ≠ t ⋅ (σ ∘s (δ ∘s θ))"
      using f(1) Bex_set by fastforce
  }
  thus ?thesis using assms unfolding ineq_model_def by simp
qed

context
begin
private lemma strand_sem_subst_c:
  assumes "(subst_domain δ ∪ range_vars δ) ∩ bvarsst S = {}"
  shows "⟦M; S⟧c (δ ∘s θ) ⟹ ⟦M; S ⋅st δ⟧c θ"
using assms
proof (induction S arbitrary: δ M rule: strand_sem_induct)
  case (ConsSnd M ts S)
  hence "⟦M; S ⋅st δ⟧c θ" "∀t ∈ set ts. M ⊢c t ⋅ (δ ∘s θ)" by auto
  hence "∀t ∈ set ts. M ⊢c (t ⋅ δ) ⋅ θ"
    using subst_comp_all[of δ θ M] subst_subst_compose[of _ δ θ] by simp
  hence "∀t ∈ set (ts ⋅list δ). M ⊢c t ⋅ θ" by fastforce
  thus ?case
    using ‹⟦M; S ⋅st δ⟧c θ›
    unfolding subst_apply_strand_def 
    by simp
next
  case (ConsRcv M ts S)
  have *: "⟦(set ts ⋅set δ ∘s θ) ∪ M; S⟧c (δ ∘s θ)" using ConsRcv.prems(1) by simp
  have "bvarsst (Receive ts#S) = bvarsst S" by auto
  hence **: "(subst_domain δ ∪ range_vars δ) ∩ bvarsst S = {}" using ConsRcv.prems(2) by blast
  have "⟦M; Receive (ts ⋅list δ)#(S ⋅st δ)⟧c θ"
    using ConsRcv.IH[OF * **] by (metis (no_types) image_set strand_sem_c.simps(3) subst_comp_all)
  thus ?case by simp
next
  case (ConsIneq M X F S)
  hence *: "⟦M; S ⋅st δ⟧c θ" and
        ***: "(subst_domain δ ∪ range_vars δ) ∩ set X = {}" 
    unfolding bvarsst_def ineq_model_def by auto
  have **: "ineq_model (δ ∘s θ) X F"
    using ConsIneq by (auto simp add: subst_compose_assoc ineq_model_def)
  have "∀γ. subst_domain γ = set X ∧ ground (subst_range γ)
          ⟶ (subst_domain δ ∪ range_vars δ) ∩ (subst_domain γ ∪ range_vars γ) = {}"
    using * ** *** unfolding range_vars_alt_def by auto
  hence "∀γ. subst_domain γ = set X ∧ ground (subst_range γ) ⟶ γ ∘s δ = δ ∘s γ"
    by (metis subst_comp_eq_if_disjoint_vars)
  hence "ineq_model θ X (F ⋅pairs δ)"
    using ineq_model_subst[OF *** **]
    by blast
  moreover have "rm_vars (set X) δ = δ" using ConsIneq.prems(2) by force
  ultimately show ?case using * by auto
qed simp_all

private lemma strand_sem_subst_c':
  assumes "(subst_domain δ ∪ range_vars δ) ∩ bvarsst S = {}"
  shows "⟦M; S ⋅st δ⟧c θ ⟹ ⟦M; S⟧c (δ ∘s θ)"
using assms
proof (induction S arbitrary: δ M rule: strand_sem_induct)
  case (ConsSnd M ts S)
  hence "⟦M; [Send ts] ⋅st δ⟧c θ" "⟦M; S ⋅st δ⟧c θ" by auto
  hence "⟦M; S⟧c (δ ∘s θ)" using ConsSnd.IH[OF _] ConsSnd.prems(2) by auto
  moreover have "⟦M; [Send ts]⟧c (δ ∘s θ)"
  proof -
    have "⟦M; [send⟨ts ⋅list δ⟩st]⟧c θ" using ‹⟦M; [Send ts] ⋅st δ⟧c θ› by simp
    hence "∀t ∈ set (ts ⋅list δ). M ⊢c t ⋅ θ" by simp
    hence "∀t ∈ set ts. M ⊢c t ⋅ δ ⋅ θ" by auto
    hence "∀t ∈ set ts. M ⊢c t ⋅ (δ ∘s θ)" using subst_subst_compose by metis
    thus "⟦M; [Send ts]⟧c (δ ∘s θ)" by auto
  qed
  ultimately show ?case by auto
next
  case (ConsRcv M ts S)
  hence "⟦((set ts ⋅set δ ⋅set θ) ∪ M); S ⋅st δ⟧c θ" by (simp add: subst_all_insert)
  hence "⟦((set ts ⋅set δ ∘s θ) ∪ M); S ⋅st δ⟧c θ" by (metis subst_comp_all)
  thus ?case using ConsRcv.IH ConsRcv.prems(2)  by auto
next
  case (ConsIneq M X F S)
  have δ: "rm_vars (set X) δ = δ" using ConsIneq.prems(2) by force
  hence *: "⟦M; S⟧c (δ ∘s θ)"
    and ***: "(subst_domain δ ∪ range_vars δ) ∩ set X = {}"
    using ConsIneq unfolding bvarsst_def ineq_model_def by auto
  have **: "ineq_model θ X (F ⋅pairs δ)"
    using ConsIneq.prems(1) δ by (auto simp add: subst_compose_assoc ineq_model_def)
  have "∀γ. subst_domain γ = set X ∧ ground (subst_range γ)
          ⟶ (subst_domain δ ∪ range_vars δ) ∩ (subst_domain γ ∪ range_vars γ) = {}"
    using * ** *** unfolding range_vars_alt_def by auto
  hence "∀γ. subst_domain γ = set X ∧ ground (subst_range γ) ⟶ γ ∘s δ = δ ∘s γ"
    by (metis subst_comp_eq_if_disjoint_vars)
  hence "ineq_model (δ ∘s θ) X F"
    using ineq_model_subst'[OF *** **]
    by blast
  thus ?case using * by auto
next
  case ConsEq thus ?case unfolding bvarsst_def by auto
qed simp_all

private lemma strand_sem_subst_d:
  assumes "(subst_domain δ ∪ range_vars δ) ∩ bvarsst S = {}"
  shows "⟦M; S⟧d (δ ∘s θ) ⟹ ⟦M; S ⋅st δ⟧d θ"
using assms
proof (induction S arbitrary: δ M rule: strand_sem_induct)
  case (ConsSnd M ts S)
  hence "⟦M; S ⋅st δ⟧d θ" "∀t ∈ set ts. M ⊢ t ⋅ (δ ∘s θ)" by auto
  hence "∀t ∈ set ts. M ⊢ (t ⋅ δ) ⋅ θ"
    using subst_comp_all[of δ θ M] subst_subst_compose[of _ δ θ] by simp
  hence "∀t ∈ set (ts ⋅list δ). M ⊢ t ⋅ θ" by simp
  thus ?case using ‹⟦M; S ⋅st δ⟧d θ› by simp
next
  case (ConsRcv M ts S) 
  have "⟦(set ts ⋅set δ ∘s θ) ∪ M; S⟧d (δ ∘s θ)" using ConsRcv.prems(1) by simp
  hence *: "⟦(set ts ⋅set δ ⋅set θ) ∪ M; S⟧d (δ ∘s θ)" by (metis subst_comp_all)
  have "bvarsst (Receive ts#S) = bvarsst S" by auto
  hence **: "(subst_domain δ ∪ range_vars δ) ∩ bvarsst S = {}" using ConsRcv.prems(2) by blast
  have "⟦M; Receive (ts ⋅list δ)#(S ⋅st δ)⟧d θ" using ConsRcv.IH[OF * **] by simp
  thus ?case by simp
next
  case (ConsIneq M X F S)
  hence *: "⟦M; S ⋅st δ⟧d θ" and
        ***: "(subst_domain δ ∪ range_vars δ) ∩ set X = {}" 
    unfolding bvarsst_def ineq_model_def by auto
  have **: "ineq_model (δ ∘s θ) X F"
    using ConsIneq by (auto simp add: subst_compose_assoc ineq_model_def)
  have "∀γ. subst_domain γ = set X ∧ ground (subst_range γ)
          ⟶ (subst_domain δ ∪ range_vars δ) ∩ (subst_domain γ ∪ range_vars γ) = {}"
    using * ** *** unfolding range_vars_alt_def by auto
  hence "∀γ. subst_domain γ = set X ∧ ground (subst_range γ) ⟶ γ ∘s δ = δ ∘s γ"
    by (metis subst_comp_eq_if_disjoint_vars)
  hence "ineq_model θ X (F ⋅pairs δ)"
    using ineq_model_subst[OF *** **]
    by blast
  moreover have "rm_vars (set X) δ = δ" using ConsIneq.prems(2) by force
  ultimately show ?case using * by auto
next
  case ConsEq thus ?case unfolding bvarsst_def by auto
qed simp_all

private lemma strand_sem_subst_d':
  assumes "(subst_domain δ ∪ range_vars δ) ∩ bvarsst S = {}"
  shows "⟦M; S ⋅st δ⟧d θ ⟹ ⟦M; S⟧d (δ ∘s θ)"
using assms
proof (induction S arbitrary: δ M rule: strand_sem_induct)
  case (ConsSnd M ts S)
  hence "⟦M; [Send ts] ⋅st δ⟧d θ" "⟦M; S ⋅st δ⟧d θ" by auto
  hence "⟦M; S⟧d (δ ∘s θ)" using ConsSnd.IH[OF _] ConsSnd.prems(2) by auto
  moreover have "⟦M; [Send ts]⟧d (δ ∘s θ)"
  proof -
    have "⟦M; [send⟨ts ⋅list δ⟩st]⟧d θ" using ‹⟦M; [Send ts] ⋅st δ⟧d θ› by simp
    hence "∀t ∈ set (ts ⋅list δ). M ⊢ t ⋅ θ" by simp
    hence "∀t ∈ set ts. M ⊢ t ⋅ δ ⋅ θ" by auto
    hence "∀t ∈ set ts. M ⊢ t ⋅ (δ ∘s θ)" using subst_subst_compose by metis
    thus "⟦M; [Send ts]⟧d (δ ∘s θ)" by auto
  qed
  ultimately show ?case by auto
next
  case (ConsRcv M ts S)
  hence "⟦((set ts ⋅set δ ⋅set θ) ∪ M); S ⋅st δ⟧d θ" by (simp add: subst_all_insert)
  hence "⟦((set ts ⋅set δ ∘s θ) ∪ M); S ⋅st δ⟧d θ" by (metis subst_comp_all)
  thus ?case using ConsRcv.IH ConsRcv.prems(2) by auto
next
  case (ConsIneq M X F S)
  have δ: "rm_vars (set X) δ = δ" using ConsIneq.prems(2) by force
  hence *: "⟦M; S⟧d (δ ∘s θ)"
    and ***: "(subst_domain δ ∪ range_vars δ) ∩ set X = {}"
    using ConsIneq unfolding bvarsst_def ineq_model_def by auto
  have **: "ineq_model θ X (F ⋅pairs δ)"
    using ConsIneq.prems(1) δ by (auto simp add: subst_compose_assoc ineq_model_def)
  have "∀γ. subst_domain γ = set X ∧ ground (subst_range γ)
          ⟶ (subst_domain δ ∪ range_vars δ) ∩ (subst_domain γ ∪ range_vars γ) = {}"
    using * ** *** unfolding range_vars_alt_def by auto
  hence "∀γ. subst_domain γ = set X ∧ ground (subst_range γ) ⟶ γ ∘s δ = δ ∘s γ"
    by (metis subst_comp_eq_if_disjoint_vars)
  hence "ineq_model (δ ∘s θ) X F"
    using ineq_model_subst'[OF *** **]
    by blast
  thus ?case using * by auto
next
  case ConsEq thus ?case unfolding bvarsst_def by auto
qed simp_all

lemmas strand_sem_subst =
  strand_sem_subst_c strand_sem_subst_c' strand_sem_subst_d strand_sem_subst_d'
end

lemma strand_sem_subst_subst_idem:
  assumes δ: "(subst_domain δ ∪ range_vars δ) ∩ bvarsst S = {}"
  shows "⟦⟦M; S ⋅st δ⟧c (δ ∘s θ); subst_idem δ⟧ ⟹ ⟦M; S⟧c (δ ∘s θ)"
using strand_sem_subst(2)[OF assms, of M "δ ∘s θ"] subst_compose_assoc[of δ δ θ]
unfolding subst_idem_def by argo

lemma strand_sem_subst_comp:
  assumes "(subst_domain θ ∪ range_vars θ) ∩ bvarsst S = {}"
    and "⟦M; S⟧c δ" "subst_domain θ ∩ (varsst S ∪ fvset M) = {}"
  shows "⟦M; S⟧c (θ ∘s δ)"
proof -
  from assms(3) have "subst_domain θ ∩ varsst S = {}" "subst_domain θ ∩ fvset M = {}" by auto
  hence "S ⋅st θ = S" "M ⋅set θ = M" using strand_substI set_subst_ident[of M θ] by (blast, blast)
  thus ?thesis using assms(2) by (auto simp add: strand_sem_subst(2)[OF assms(1)])
qed

lemma strand_sem_c_imp_ineqs_neq:
  assumes "⟦M; S⟧c ℐ" "Inequality X [(t,t')] ∈ set S"
  shows "t ≠ t' ∧ (∀δ. subst_domain δ = set X ∧ ground (subst_range δ)
                        ⟶ t ⋅ δ ≠ t' ⋅ δ ∧ t ⋅ δ ⋅ ℐ ≠ t' ⋅ δ ⋅ ℐ)"
using assms
proof (induction rule: strand_sem_induct)
  case (ConsIneq M Y F S) thus ?case
  proof (cases "Inequality X [(t,t')] ∈ set S")
    case False
    hence "X = Y" "F = [(t,t')]" using ConsIneq by auto
    hence *: "∀θ. subst_domain θ = set X ∧ ground (subst_range θ) ⟶ t ⋅ θ ⋅ ℐ ≠ t' ⋅ θ ⋅ ℐ"
      using ConsIneq by (auto simp add: ineq_model_def)
    then obtain θ where θ: "subst_domain θ = set X" "ground (subst_range θ)" "t ⋅ θ ⋅ ℐ ≠ t' ⋅ θ ⋅ ℐ"
      using interpretation_subst_exists'[of "set X"] by atomize_elim auto
    hence "t ≠ t'" by auto
    moreover have "⋀ℐ θ. t ⋅ θ ⋅ ℐ ≠ t' ⋅ θ ⋅ ℐ ⟹ t ⋅ θ ≠ t' ⋅ θ" by auto
    ultimately show ?thesis using * by auto
  qed simp
qed simp_all

lemma strand_sem_c_imp_ineq_model:
  assumes "⟦M; S⟧c ℐ" "Inequality X F ∈ set S"
  shows "ineq_model ℐ X F"
using assms by (induct S rule: strand_sem_induct) force+

lemma strand_sem_wf_simple_fv_sat:
  assumes "wfst {} S" "simple S" "⟦{}; S⟧c ℐ"
  shows "⋀v. v ∈ wfrestrictedvarsst S ⟹ ikst S ⋅set ℐ ⊢c ℐ v"
using assms
proof (induction S rule: wfst_simple_induct)
  case (ConsRcv t S)
  have "v ∈ wfrestrictedvarsst S"
    using ConsRcv.hyps(3) ConsRcv.prems(1) vars_snd_rcv_strand2
    by fastforce
  moreover have "⟦{}; S⟧c ℐ" using ‹⟦{}; S@[Receive t]⟧c ℐ› by blast
  moreover have "ikst S ⋅set ℐ ⊆ ikst (S@[Receive t]) ⋅set ℐ" by auto
  ultimately show ?case using ConsRcv.IH ideduct_synth_mono by meson
next
  case (ConsIneq X F S)
  hence "v ∈ wfrestrictedvarsst S" by fastforce
  moreover have "⟦{}; S⟧c ℐ" using ‹⟦{}; S@[Inequality X F]⟧c ℐ› by blast
  moreover have "ikst S ⋅set ℐ ⊆ ikst (S@[Inequality X F]) ⋅set ℐ" by auto
  ultimately show ?case using ConsIneq.IH ideduct_synth_mono by meson
next
  case (ConsSnd w S)
  hence *: "⟦{}; S⟧c ℐ" "ikst S ⋅set ℐ ⊢c ℐ w" by auto
  have **: "ikst S ⋅set ℐ ⊆ ikst (S@[Send [Var w]]) ⋅set ℐ" 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 ∈ wfrestrictedvarsst 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_assignment_rhs_fun_subterm:
  assumes "wfst {} A" "⟦{}; A⟧c ℐ" "Var x ∈ ikst A" "ℐ x = Fun f T"
          "ti ∈ set T" "¬ikst A ⋅set ℐ ⊢c ti" "interpretationsubst ℐ"
  obtains S where
    "Fun f S ∈ subtermsset (ikst A) ∨ Fun f S ∈ subtermsset (assignment_rhsst A)"
    "Fun f T = Fun f S ⋅ ℐ"
proof -
  have "x ∈ wfrestrictedvarsst A"
    by (metis (no_types) assms(3) set_rev_mp term.set_intros(3) vars_subset_if_in_strand_ik2)
  moreover have "Fun f T ⋅ ℐ = Fun f T"
    by (metis subst_ground_ident interpretation_grounds_all assms(4,7))
  ultimately obtain Apre Asuf where *:
      "¬(∃w ∈ wfrestrictedvarsst Apre. Fun f T ⊑ ℐ w)"
      "(∃t. A = Apre@Send t#Asuf ∧ Fun f T ⊑set set t ⋅set ℐ) ∨
       (∃t t'. A = Apre@Equality Assign t t'#Asuf ∧ Fun f T ⊑ t ⋅ ℐ)"
    using wf_strand_first_Send_var_split[OF assms(1)] assms(4) subtermeqI' by metis
  moreover
  { fix ts assume **: "A = Apre@Send ts#Asuf" "Fun f T ⊑set set ts ⋅set ℐ"
    hence ***: "∀t ∈ set ts. ikst Apre ⋅set ℐ ⊢c t ⋅ ℐ" "¬ikst Apre ⋅set ℐ ⊢c ti"
      using assms(2,6) by (auto intro: ideduct_synth_mono)
    then obtain t where t: "t ∈ set ts" "Fun f T ⊑ t ⋅ ℐ" "ikst Apre ⋅set ℐ ⊢c t ⋅ ℐ"
      using **(2) by blast
    obtain s where s: "s ∈ ikst Apre" "Fun f T ⊑ s ⋅ ℐ"
      using t(3,2) ***(2) assms(5) by (induct rule: intruder_synth_induct) auto
    then obtain g S where gS: "Fun g S ⊑ s" "Fun f T = Fun g S ⋅ ℐ"
      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 = Apre@Equality Assign t t'#Asuf" "Fun f T ⊑ t ⋅ ℐ"
    with assms(2) have "t ⋅ ℐ = t' ⋅ ℐ" by auto
    hence "Fun f T ⊑ t' ⋅ ℐ" using **(2) by auto
    from assms(1) **(1) have "fv t' ⊆ wfrestrictedvarsst Apre"
      using wf_eq_fv[of "{}" Apre t t' Asuf] vars_snd_rcv_strand_subset2(4)[of Apre]
      by blast
    then obtain g S where gS: "Fun g S ⊑ t'" "Fun f T = Fun g S ⋅ ℐ"
      using subterm_subst_not_img_subterm[OF ‹Fun f T ⊑ t' ⋅ ℐ›] *(1) by fastforce
    hence ?thesis using that **(1) by auto
  }
  ultimately show ?thesis by auto
qed

lemma ineq_model_not_unif_is_sat_ineq:
  assumes "∄θ. Unifier θ t t'"
  shows "ineq_model ℐ X [(t, t')]"
using assms list.set_intros(1)[of "(t,t')" "[]"]
unfolding ineq_model_def by blast

lemma strand_sem_not_unif_is_sat_ineq:
  assumes "∄θ. Unifier θ t t'"
  shows "⟦M; [Inequality X [(t,t')]]⟧c ℐ" "⟦M; [Inequality X [(t,t')]]⟧d ℐ"
using ineq_model_not_unif_is_sat_ineq[OF assms]
      strand_sem_c.simps(1,5)[of M] strand_sem_d.simps(1,5)[of M]
by presburger+

lemma ineq_model_singleI[intro]:
  assumes "∀δ. subst_domain δ = set X ∧ ground (subst_range δ) ⟶ t ⋅ δ ⋅ ℐ ≠ t' ⋅ δ ⋅ ℐ"
  shows "ineq_model ℐ X [(t,t')]"
using assms unfolding ineq_model_def by auto

lemma ineq_model_singleE:
  assumes "ineq_model ℐ X [(t,t')]"
  shows "∀δ. subst_domain δ = set X ∧ ground (subst_range δ) ⟶ t ⋅ δ ⋅ ℐ ≠ t' ⋅ δ ⋅ ℐ"
using assms unfolding ineq_model_def by auto

lemma ineq_model_single_iff:
  fixes F::"(('a,'b) term × ('a,'b) term) list"
  shows "ineq_model ℐ X F ⟷
         ineq_model ℐ X [(Fun f (Fun c []#map fst F),Fun f (Fun c []#map snd F))]"
    (is "?A ⟷ ?B")
proof -
  let ?P = "λδ f. fst f ⋅ (δ ∘s ℐ) ≠ snd f ⋅ (δ ∘s ℐ)"
  let ?Q = "λδ t t'. t ⋅ (δ ∘s ℐ) ≠ t' ⋅ (δ ∘s ℐ)"
  let ?T = "λg. Fun c []#map g F"
  let ?S = "λδ g. map (λx. x ⋅ (δ ∘s ℐ)) (Fun c []#map g F)"
  let ?t = "Fun f (?T fst)"
  let ?t' = "Fun f (?T snd)"

  have len: "⋀g h. length (?T g) = length (?T h)"
            "⋀g h δ. length (?S δ g) = length (?T h)"
            "⋀g h δ. length (?S δ g) = length (?T h)"
            "⋀g h δ σ. length (?S δ g) = length (?S σ h)"
    by simp_all

  { fix δ::"('a,'b) subst"
    assume δ: "subst_domain δ = set X" "ground (subst_range δ)"
    have "list_ex (?P δ) F ⟷ ?Q δ ?t ?t'"
    proof
      assume "list_ex (?P δ) F"
      then obtain a where a: "a ∈ set F" "?P δ a" by (metis (mono_tags, lifting) Bex_set)
      thus "?Q δ ?t ?t'" by auto
    qed (fastforce simp add: Bex_set)
  } thus ?thesis unfolding ineq_model_def case_prod_unfold by auto
qed


subsection ‹Constraint Semantics (Alternative, Equivalent Version)›
text ‹These are the constraint semantics used in the CSF 2017 paper›
fun strand_sem_c'::"('fun,'var) terms ⇒ ('fun,'var) strand ⇒ ('fun,'var) subst ⇒ bool"  (‹⟦_; _⟧c''›) 
  where
  "⟦M; []⟧c' = (λℐ. True)"
| "⟦M; Send ts#S⟧c' = (λℐ. (∀t ∈ set ts. M ⋅set ℐ ⊢c t ⋅ ℐ) ∧ ⟦M; S⟧c' ℐ)"
| "⟦M; Receive ts#S⟧c' = ⟦set ts ∪ M; S⟧c'"
| "⟦M; Equality _ t t'#S⟧c' = (λℐ. t ⋅ ℐ = t' ⋅ ℐ ∧ ⟦M; S⟧c' ℐ)"
| "⟦M; Inequality X F#S⟧c' = (λℐ. ineq_model ℐ X F ∧ ⟦M; S⟧c' ℐ)"

fun strand_sem_d'::"('fun,'var) terms ⇒ ('fun,'var) strand ⇒ ('fun,'var) subst ⇒ bool" (‹⟦_; _⟧d''›)
where
  "⟦M; []⟧d' = (λℐ. True)"
| "⟦M; Send ts#S⟧d' = (λℐ. (∀t ∈ set ts. M ⋅set ℐ ⊢ t ⋅ ℐ) ∧ ⟦M; S⟧d' ℐ)"
| "⟦M; Receive ts#S⟧d' = ⟦set ts ∪ M; S⟧d'"
| "⟦M; Equality _ t t'#S⟧d' = (λℐ. t ⋅ ℐ = t' ⋅ ℐ ∧ ⟦M; S⟧d' ℐ)"
| "⟦M; Inequality X F#S⟧d' = (λℐ. ineq_model ℐ X F ∧ ⟦M; S⟧d' ℐ)"

lemma strand_sem_eq_defs:
  "⟦M; 𝒜⟧c' ℐ = ⟦M ⋅set ℐ; 𝒜⟧c ℐ"
  "⟦M; 𝒜⟧d' ℐ = ⟦M ⋅set ℐ; 𝒜⟧d ℐ"
proof -
  have 1: "⟦M; 𝒜⟧c' ℐ ⟹ ⟦M ⋅set ℐ; 𝒜⟧c ℐ"
  proof (induction 𝒜 arbitrary: M rule: strand_sem_induct)
    case (ConsRcv M ts S) thus ?case by (fastforce simp add: image_Un[of "λt. t ⋅ ℐ"])
  qed simp_all

  have 2: "⟦M ⋅set ℐ; 𝒜⟧c ℐ ⟹ ⟦M; 𝒜⟧c' ℐ"
  proof (induction 𝒜 arbitrary: M rule: strand_sem_c'.induct)
    case (3 M ts S) thus ?case by (fastforce simp add: image_Un[of "λt. t ⋅ ℐ"])
  qed simp_all

  have 3: "⟦M; 𝒜⟧d' ℐ ⟹ ⟦M ⋅set ℐ; 𝒜⟧d ℐ"
  proof (induction 𝒜 arbitrary: M rule: strand_sem_induct)
    case (ConsRcv M ts S) thus ?case by (fastforce simp add: image_Un[of "λt. t ⋅ ℐ"])
  qed simp_all

  have 4: "⟦M ⋅set ℐ; 𝒜⟧d ℐ ⟹ ⟦M; 𝒜⟧d' ℐ"
  proof (induction 𝒜 arbitrary: M rule: strand_sem_d'.induct)
    case (3 M ts S) thus ?case by (fastforce simp add: image_Un[of "λt. t ⋅ ℐ"])
  qed simp_all

  show "⟦M; 𝒜⟧c' ℐ = ⟦M ⋅set ℐ; 𝒜⟧c ℐ" "⟦M; 𝒜⟧d' ℐ = ⟦M ⋅set ℐ; 𝒜⟧d ℐ"
    by (metis 1 2, metis 3 4)
qed

lemma strand_sem_split'[dest]:
  "⟦M; S@S'⟧c' θ ⟹ ⟦M; S⟧c' θ" 
  "⟦M; S@S'⟧c' θ ⟹ ⟦M ∪ ikst S; S'⟧c' θ"
  "⟦M; S@S'⟧d' θ ⟹ ⟦M; S⟧d' θ"
  "⟦M; S@S'⟧d' θ ⟹ ⟦M ∪ ikst S; S'⟧d' θ"
using strand_sem_eq_defs[of M "S@S'" θ]
      strand_sem_eq_defs[of M S θ]
      strand_sem_eq_defs[of "M ∪ ikst S" S' θ]
      strand_sem_split(2,4)
by (auto simp add: image_Un)

lemma strand_sem_append'[intro]:
  "⟦M; S⟧c' θ ⟹ ⟦M ∪ ikst S; S'⟧c' θ ⟹ ⟦M; S@S'⟧c' θ"
  "⟦M; S⟧d' θ ⟹ ⟦M ∪ ikst S; S'⟧d' θ ⟹ ⟦M; S@S'⟧d' θ"
using strand_sem_eq_defs[of M "S@S'" θ]
      strand_sem_eq_defs[of M S θ]
      strand_sem_eq_defs[of "M ∪ ikst S" S' θ]
by (auto simp add: image_Un)

end

subsection ‹Dual Strands›
fun dualst::"('a,'b) strand ⇒ ('a,'b) strand" where
  "dualst [] = []"
| "dualst (Receive t#S) = Send t#(dualst S)"
| "dualst (Send t#S) = Receive t#(dualst S)"
| "dualst (x#S) = x#(dualst S)"

lemma dualst_append: "dualst (A@B) = (dualst A)@(dualst B)"
by (induct A rule: dualst.induct) auto

lemma dualst_self_inverse: "dualst (dualst S) = S"
proof (induction S)
  case (Cons x S) thus ?case by (cases x) auto
qed simp

lemma dualst_trms_eq: "trmsst (dualst S) = trmsst S"
proof (induction S)
  case (Cons x S) thus ?case by (cases x) auto
qed simp

lemma dualst_fv: "fvst (dualst A) = fvst A"
by (induct A rule: dualst.induct) auto

lemma dualst_bvars: "bvarsst (dualst A) = bvarsst A"
by (induct A rule: dualst.induct) fastforce+


end