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⟨tsst"
  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⟨tsst  set S" "v  fvset (set ts)"
proof -
  have "ts. send⟨tsst  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⟨tsst  set S" "v  fvset (set ts)"
proof -
  have "ts. receive⟨tsst  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⟨tsst#S) = fvset (set ts)  wfvarsoccsst S"
    unfolding wfvarsoccsst_def by simp
  hence "(aset S'. fvrcv a)  (aset 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 "(aset S'. fvrcv a)  (aset 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#Sc = (λ. (t  set ts. M c t  )  M; Sc )"
| "M; Receive ts#Sc = (λ. (set ts set )  M; Sc )"
| "M; Equality _ t t'#Sc = (λ. t   = t'    M; Sc )"
| "M; Inequality X F#Sc = (λ. ineq_model  X F  M; Sc )"

definition constr_sem_c ("_ c _,_") where " c S,θ  (θ supports   {}; Sc )"
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#Sd = (λ. (t  set ts. M  t  )  M; Sd )"
| "M; Receive ts#Sd = (λ. (set ts set )  M; Sd )"
| "M; Equality _ t t'#Sd = (λ. t   = t'    M; Sd )"
| "M; Inequality X F#Sd = (λ. ineq_model  X F  M; Sd )"

definition constr_sem_d ("_  _,_") where "  S,θ  (θ supports   {}; Sd )"
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; Sc   M; Sd "
    proof (induction S rule: strand_sem_induct)
      case (ConsSnd M ts S)
      hence "t  set ts. M c t  " "M; Sd " 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; Sc θ  M'; Sc θ" (is "?A'; ?A''  ?A")
  "M  M'; M; Sd θ  M'; Sd θ" (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'; Sc θ" by auto
    hence "t  set ts. M' c t  θ" using ideduct_synth_mono M  M' by metis
    thus ?case using M'; Sc θ 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'; Sd θ" by auto
    hence "t  set ts. M'  t  θ" using ideduct_mono M  M' by metis
    thus ?case using M'; Sd θ by simp
  qed auto
qed

context
begin
private lemma strand_sem_split_left:
  "M; S@S'c θ  M; Sc θ"
  "M; S@S'd θ  M; Sd θ"
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 Tc θ; ts  set T  M; [Send ts]c θ" (is "?A'; ?A''  ?A")
  "M; map Send Td θ; ts  set T  M; [Send ts]d θ" (is "?B'; ?B''  ?B")
  "M; map Send T@Sc θ; ts  set T  M; Send ts#Sc θ" (is "?C'; ?C''  ?C")
  "M; map Send T@Sd θ; ts  set T  M; Send ts#Sd θ" (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'@Sc θ; t  set T'  M; Send1 t#Sc θ" (is "?G'; ?G''  ?G")
  "M; map Send1 T'@Sd θ; t  set T'  M; Send1 t#Sd θ" (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; Sc θ" 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; Sd θ" 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 Tc "
  "(ts. ts  set T  M; [Send ts]d )  M; map Send Td "
  "(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 Tc "
       "(ts. ts  set T  M; [Send ts]d )  M; map Send Td "
    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 Tc " "M; map Receive Td "
  "M; map Receive1 T'c " "M; map Receive1 T'd "
  "M; [Receive T']c " "M; [Receive T']d "
proof -
  show "M; map Receive Tc " "M; map Receive Td " 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; Sc θ; M  (ikst S set θ); S'c θ  M; S@S'c θ"
  "M; Sd θ; 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; Sc (δ 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; Sc (δ 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; Sc (δ 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; Sc (δ 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; Sc (δ 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; Sd (δ 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; Sd (δ s θ)" using ConsRcv.prems(1) by simp
  hence *: "(set ts set δ set θ)  M; Sd (δ 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; Sd (δ 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; Sd (δ 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; Sd (δ 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; Sc (δ 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; Sc δ" "subst_domain θ  (varsst S  fvset M) = {}"
  shows "M; Sc (θ 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; Sc " "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; Sc " "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" "{}; Sc "
  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 "{}; Sc " 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 "{}; Sc " 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 *: "{}; Sc " "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" "{}; Ac " "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#Sc' = (λ. (t  set ts. M set  c t  )  M; Sc' )"
| "M; Receive ts#Sc' = set ts  M; Sc'"
| "M; Equality _ t t'#Sc' = (λ. t   = t'    M; Sc' )"
| "M; Inequality X F#Sc' = (λ. ineq_model  X F  M; Sc' )"

fun strand_sem_d'::"('fun,'var) terms  ('fun,'var) strand  ('fun,'var) subst  bool" ("_; _d''")
where
  "M; []d' = (λ. True)"
| "M; Send ts#Sd' = (λ. (t  set ts. M set   t  )  M; Sd' )"
| "M; Receive ts#Sd' = set ts  M; Sd'"
| "M; Equality _ t t'#Sd' = (λ. t   = t'    M; Sd' )"
| "M; Inequality X F#Sd' = (λ. ineq_model  X F  M; Sd' )"

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; Sc' θ" 
  "M; S@S'c' θ  M  ikst S; S'c' θ"
  "M; S@S'd' θ  M; Sd' θ"
  "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; Sc' θ  M  ikst S; S'c' θ  M; S@S'c' θ"
  "M; Sd' θ  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