Theory Strands_and_Constraints

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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


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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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


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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

lemma vars_snd_rcv_strand[iff]:
  "varsst (S::('a,'b) strand) =
    (⋃(set (map fvsnd S))) ∪ (⋃(set (map fvrcv S))) ∪ (⋃(set (map (fveq assign) S)))
    ∪ (⋃(set (map (fveq check) S))) ∪ (⋃(set (map fvineq S))) ∪ bvarsst S"
unfolding bvarsst_def
proof (induction S)
  case (Cons x S)
  have "⋀s V. varsstp (s::('a,'b) strand_step) ∪ V = 
                fvsnd s ∪ fvrcv s ∪ fveq assign s ∪ fveq check s ∪ fvineq s ∪ set (bvarsstp s) ∪ V"
    by (metis vars_snd_rcv_union)
  thus ?case using Cons.IH by (auto simp add: sup_assoc sup_left_commute)
qed simp

lemma fv_snd_rcv_strand[iff]:
  "fvst (S::('a,'b) strand) =
    (⋃(set (map fvsnd S))) ∪ (⋃(set (map fvrcv S))) ∪ (⋃(set (map (fveq assign) S)))
    ∪ (⋃(set (map (fveq check) S))) ∪ (⋃(set (map fvineq S)))"
unfolding bvarsst_def
proof (induction S)
  case (Cons x S)
  have "⋀s V. fvstp (s::('a,'b) strand_step) ∪ V = 
                fvsnd s ∪ fvrcv s ∪ fveq assign s ∪ fveq check s ∪ fvineq s ∪ V"
    by (metis fv_snd_rcv_union)
  thus ?case using Cons.IH by (auto simp add: sup_assoc sup_left_commute)
qed simp

lemma vars_snd_rcv_strand2[iff]:
  "wfrestrictedvarsst (S::('a,'b) strand) =
    (⋃(set (map fvsnd S))) ∪ (⋃(set (map fvrcv S))) ∪ (⋃(set (map (fveq assign) S)))"
by (induct S) (auto simp add: split: strand_step.split poscheckvariant.split)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

lemma subst_apply_fv_subset_strand:
  assumes P: "P = fvstp ∨ P = fvrcv ∨ P = fvsnd ∨ P = fveq ac ∨ P = fvineq"
  and P_subset: "P x ⊆ ⋃(set (map P S)) ∪ V"
  and δ: "bvarsst S ∩ (subst_domain δ ∪ range_vars δ) = {}"
         "set (bvarsstp x) ∩ (subst_domain δ ∪ range_vars δ) = {}"
  shows "P (x ⋅stp δ) ⊆ ⋃(set (map P (S ⋅st δ))) ∪ fvset (δ ` V)"
proof (cases x)
  case (Send ts)
  hence *: "fvstp x = fvset (set ts)" "fvstp (x ⋅stp δ) = fvset (set ts ⋅set δ)"
           "fvrcv x = {}" "fvrcv (x ⋅stp δ) = {}"
           "fvsnd x = fvset (set ts)" "fvsnd (x ⋅stp δ) = fvset (set ts ⋅set δ)"
           "fveq ac x = {}" "fveq ac (x ⋅stp δ) = {}"
           "fvineq x = {}" "fvineq (x ⋅stp δ) = {}"
    by auto
  hence **: "(P x = fvset (set ts) ∧ P (x ⋅stp δ) = fvset (set ts ⋅set δ)) ∨
             (P x = {} ∧ P (x ⋅stp δ) = {})"
    by (metis P)
  moreover
  { assume "P x = {}" "P (x ⋅stp δ) = {}" hence ?thesis by simp }
  moreover
  { assume "P x = fvset (set ts)" "P (x ⋅stp δ) = fvset (set ts ⋅set δ)"
    hence "fvset (set ts) ⊆ ⋃(set (map P S)) ∪ V" using P_subset by auto
    hence "fvset (set ts ⋅set δ) ⊆ ⋃(set (map P (S ⋅st δ))) ∪ fvset (δ ` V)"
      using subst_apply_fv_subset_strand_trm[OF P _ assms(3), of _ V] by fastforce
    hence ?thesis using ‹P (x ⋅stp δ) = fvset (set ts ⋅set δ)› by force
  }
  ultimately show ?thesis by metis
next
  case (Receive ts)
  hence *: "fvstp x = fvset (set ts)" "fvstp (x ⋅stp δ) = fvset (set ts ⋅set δ)"
           "fvrcv x = fvset (set ts)" "fvrcv (x ⋅stp δ) = fvset (set ts ⋅set δ)"
           "fvsnd x = {}" "fvsnd (x ⋅stp δ) = {}"
           "fveq ac x = {}" "fveq ac (x ⋅stp δ) = {}"
           "fvineq x = {}" "fvineq (x ⋅stp δ) = {}"
    by auto
  hence **: "(P x = fvset (set ts) ∧ P (x ⋅stp δ) = fvset (set ts ⋅set δ)) ∨
             (P x = {} ∧ P (x ⋅stp δ) = {})"
    by (metis P)
  moreover
  { assume "P x = {}" "P (x ⋅stp δ) = {}" hence ?thesis by simp