Theory Stateful_Typing

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

section ‹Extending the Typing Result to Stateful Constraints›

theory Stateful_Typing
imports Typing_Result Stateful_Strands
begin

text ‹\label{sec:Stateful-Typing}Locale setup›
locale stateful_typed_model = typed_model arity public Ana Γ
  for arity::"'fun  nat"
    and public::"'fun  bool"
    and Ana::"('fun,'var) term  (('fun,'var) term list × ('fun,'var) term list)"
    and Γ::"('fun,'var) term  ('fun,'atom::finite) term_type"
  +
  fixes Pair::"'fun"
  assumes Pair_arity: "arity Pair = 2"
  and Ana_subst': "f T δ K M. Ana (Fun f T) = (K,M)  Ana (Fun f T  δ) = (K list δ,M list δ)"
begin

lemma Ana_invar_subst'[simp]: "Ana_invar_subst 𝒮"
using Ana_subst' unfolding Ana_invar_subst_def by force

definition pair where
  "pair d  case d of (t,t')  Fun Pair [t,t']"

fun trpairs::
  "(('fun,'var) term × ('fun,'var) term) list 
   ('fun,'var) dbstatelist 
   (('fun,'var) term × ('fun,'var) term) list list"
where
  "trpairs [] D = [[]]"
| "trpairs ((s,t)#F) D =
    concat (map (λd. map ((#) (pair (s,t), pair d)) (trpairs F D)) D)"

text ‹
  A translation/reduction tr› from stateful constraints to (lists of) "non-stateful" constraints.
  The output represents a finite disjunction of constraints whose models constitute exactly the
  models of the input constraint. The typing result for "non-stateful" constraints is later lifted
  to the stateful setting through this reduction procedure.
›
fun tr::"('fun,'var) stateful_strand  ('fun,'var) dbstatelist  ('fun,'var) strand list"
where
  "tr [] D = [[]]"
| "tr (send⟨ts#A) D = map ((#) (send⟨tsst)) (tr A D)"
| "tr (receive⟨ts#A) D = map ((#) (receive⟨tsst)) (tr A D)"
| "tr (ac: t  t'#A) D = map ((#) (ac: t  t'st)) (tr A D)"
| "tr (insert⟨t,s#A) D = tr A (List.insert (t,s) D)"
| "tr (delete⟨t,s#A) D =
    concat (map (λDi. map (λB. (map (λd. check: (pair (t,s))  (pair d)st) Di)@
                               (map (λd. []⟨∨≠: [(pair (t,s), pair d)]st) [dD. d  set Di])@B)
                          (tr A [dD. d  set Di]))
                (subseqs D))"
| "tr (ac: t  s#A) D =
    concat (map (λB. map (λd. ac: (pair (t,s))  (pair d)st#B) D) (tr A D))"
| "tr (X⟨∨≠: F ∨∉: F'#A) D =
    map ((@) (map (λG. X⟨∨≠: (F@G)st) (trpairs F' D))) (tr A D)"

text ‹Type-flaw resistance of stateful constraint steps›
fun tfrsstp where
  "tfrsstp (Equality _ t t') = ((δ. Unifier δ t t')  Γ t = Γ t')"
| "tfrsstp (NegChecks X F F') = (
    (F' = []  (x  fvpairs F-set X. a. Γ (Var x) = TAtom a)) 
    (f T. Fun f T  subtermsset (trmspairs F  pair ` set F') 
              T = []  (s  set T. s  Var ` set X)))"
| "tfrsstp _ = True"

text ‹Type-flaw resistance of stateful constraints›
definition tfrsst where "tfrsst S  tfrset (trmssst S  pair ` setopssst S)  list_all tfrsstp S"



subsection ‹Minor Lemmata›
lemma pair_in_pair_image_iff:
  "pair (s,t)  pair ` P  (s,t)  P"
unfolding pair_def by fast

lemma subst_apply_pairs_pair_image_subst:
  "pair ` set (F pairs θ) = pair ` set F set θ"
unfolding subst_apply_pairs_def pair_def by (induct F) auto

lemma Ana_subst_subterms_cases:
  fixes θ::"('fun,'var) subst"
  assumes t: "t set M set θ"
    and s: "s  set (snd (Ana t))"
  shows "(u  subtermsset M. t = u  θ  s  set (snd (Ana u)) set θ)  (x  fvset M. t  θ x)"
proof (cases "t  subtermsset M set θ")
  case True
  then obtain u where u: "u  subtermsset M" "t = u  θ" by blast
  show ?thesis
  proof (cases u)
    case (Var x)
    hence "x  fvset M" using fv_subset_subterms[OF u(1)] by simp
    thus ?thesis using u(2) Var by fastforce
  next
    case (Fun f T)
    hence "set (snd (Ana t)) = set (snd (Ana u)) set θ"
      using Ana_subst'[of f T _ _ θ] u(2) by (cases "Ana u") auto
    thus ?thesis using s u by blast
  qed
qed (use s t subtermsset_subst in blast)

lemma Ana_snd_subst_nth_inv:
  fixes θ::"('fun,'var) subst" and f ts
  defines "R  snd (Ana (Fun f ts  θ))"
  assumes r: "r = R ! i" "i < length R"
  shows "r = snd (Ana (Fun f ts)) ! i  θ"
proof -
  obtain K R where "Ana (Fun f ts) = (K,R)" by (metis surj_pair)
  thus ?thesis using Ana_subst'[of f ts K R θ] r unfolding R_def by auto
qed

lemma Ana_snd_subst_inv:
  fixes θ::"('fun,'var) subst"
  assumes r: "r  set (snd (Ana (Fun f ts  θ)))"
  shows "t  set (snd (Ana (Fun f ts))). r = t  θ"
proof -
  obtain K R where "Ana (Fun f ts) = (K,R)" by (metis surj_pair)
  thus ?thesis using Ana_subst'[of f ts K R θ] r by auto
qed


lemma fun_pair_eq[dest]: "pair d = pair d'  d = d'"
proof -
  obtain t s t' s' where "d = (t,s)" "d' = (t',s')" by atomize_elim auto
  thus "pair d = pair d'  d = d'" unfolding pair_def by simp
qed

lemma fun_pair_subst: "pair d  δ = pair (d p δ)"
using surj_pair[of d] unfolding pair_def by force  

lemma fun_pair_subst_set: "pair ` M set δ = pair ` (M pset δ)"
proof
  show "pair ` M set δ  pair ` (M pset δ)"
    using fun_pair_subst[of _ δ] by fastforce

  show "pair ` (M pset δ)  pair ` M set δ"
  proof
    fix t assume t: "t  pair ` (M pset δ)"
    then obtain p where p: "p  M" "t = pair (p p δ)" by blast
    thus "t  pair ` M set δ" using fun_pair_subst[of p δ] by force
  qed
qed

lemma fun_pair_eq_subst: "pair d  δ = pair d'  θ  d p δ = d' p θ"
by (metis fun_pair_subst fun_pair_eq[of "d p δ" "d' p θ"])

lemma setopssst_pair_image_cons[simp]:
  "pair ` setopssst (x#S) = pair ` setopssstp x  pair ` setopssst S"
  "pair ` setopssst (send⟨ts#S) = pair ` setopssst S"
  "pair ` setopssst (receive⟨ts#S) = pair ` setopssst S"
  "pair ` setopssst (ac: t  t'#S) = pair ` setopssst S"
  "pair ` setopssst (insert⟨t,s#S) = {pair (t,s)}  pair ` setopssst S"
  "pair ` setopssst (delete⟨t,s#S) = {pair (t,s)}  pair ` setopssst S"
  "pair ` setopssst (ac: t  s#S) = {pair (t,s)}  pair ` setopssst S"
  "pair ` setopssst (X⟨∨≠: F ∨∉: G#S) = pair ` set G  pair ` setopssst S"
unfolding setopssst_def by auto

lemma setopssst_pair_image_subst_cons[simp]:
  "pair ` setopssst (x#S sst θ) = pair ` setopssstp (x sstp θ)  pair ` setopssst (S sst θ)"
  "pair ` setopssst (send⟨ts#S sst θ) = pair ` setopssst (S sst θ)"
  "pair ` setopssst (receive⟨ts#S sst θ) = pair ` setopssst (S sst θ)"
  "pair ` setopssst (ac: t  t'#S sst θ) = pair ` setopssst (S sst θ)"
  "pair ` setopssst (insert⟨t,s#S sst θ) = {pair (t,s)  θ}  pair ` setopssst (S sst θ)"
  "pair ` setopssst (delete⟨t,s#S sst θ) = {pair (t,s)  θ}  pair ` setopssst (S sst θ)"
  "pair ` setopssst (ac: t  s#S sst θ) = {pair (t,s)  θ}  pair ` setopssst (S sst θ)"
  "pair ` setopssst (X⟨∨≠: F ∨∉: G#S sst θ) =
    pair ` set (G pairs rm_vars (set X) θ)  pair ` setopssst (S sst θ)"
using subst_sst_cons[of _ S θ] unfolding setopssst_def pair_def by auto

lemma setopssst_are_pairs: "t  pair ` setopssst A  s s'. t = pair (s,s')"
proof (induction A)
  case (Cons a A) thus ?case
    by (cases a) (auto simp add: setopssst_def)
qed (simp add: setopssst_def)

lemma fun_pair_wftrm: "wftrm t  wftrm t'  wftrm (pair (t,t'))"
using Pair_arity unfolding wftrm_def pair_def by auto

lemma wftrms_pairs: "wftrms (trmspairs F)  wftrms (pair ` set F)"
using fun_pair_wftrm by blast

lemma wf_fun_pair_ineqs_map:
  assumes "wfst X A"
  shows "wfst X (map (λd. Y⟨∨≠: [(pair (t, s), pair d)]st) D@A)"
using assms by (induct D) auto

lemma wf_fun_pair_negchecks_map:
  assumes "wfst X A"
  shows "wfst X (map (λG. Y⟨∨≠: (F@G)st) M@A)"
using assms by (induct M) auto

lemma wf_fun_pair_eqs_ineqs_map:
  fixes A::"('fun,'var) strand"
  assumes "wfst X A" "Di  set (subseqs D)" "(t,t')  set D. fv t  fv t'  X"
  shows "wfst X ((map (λd. check: (pair (t,s))  (pair d)st) Di)@
                 (map (λd. []⟨∨≠: [(pair (t,s), pair d)]st) [dD. d  set Di])@A)"
proof -
  let ?c1 = "map (λd. check: (pair (t,s))  (pair d)st) Di"
  let ?c2 = "map (λd. []⟨∨≠: [(pair (t,s), pair d)]st) [dD. d  set Di]"
  have 1: "wfst X (?c2@A)" using wf_fun_pair_ineqs_map[OF assms(1)] by simp
  have 2: "(t,t')  set Di. fv t  fv t'  X" 
    using assms(2,3) by (meson contra_subsetD subseqs_set_subset(1))
  have "wfst X (?c1@B)" when "wfst X B" for B::"('fun,'var) strand"
    using 2 that by (induct Di) auto
  thus ?thesis using 1 by simp
qed

lemma trmssst_wt_subst_ex:
  assumes θ: "wtsubst θ" "wftrms (subst_range θ)"
    and t: "t  trmssst (S sst θ)"
  shows "s δ. s  trmssst S  wtsubst δ  wftrms (subst_range δ)  t = s  δ"
using t
proof (induction S)
  case (Cons s S) thus ?case
  proof (cases "t  trmssst (S sst θ)")
    case False
    hence "t  trmssstp (s sstp θ)"
      using Cons.prems trmssst_subst_cons[of s S θ]
      by auto
    then obtain u where u: "u  trmssstp s" "t = u  rm_vars (set (bvarssstp s)) θ"
      using trmssstp_subst'' by blast
    thus ?thesis
      using trmssst_subst_cons[of s S θ]
            wt_subst_rm_vars[OF θ(1), of "set (bvarssstp s)"]
            wf_trms_subst_rm_vars'[OF θ(2), of "set (bvarssstp s)"]
      by fastforce
  qed auto
qed simp

lemma setopssst_wt_subst_ex:
  assumes θ: "wtsubst θ" "wftrms (subst_range θ)"
    and t: "t  pair ` setopssst (S sst θ)"
  shows "s δ. s  pair ` setopssst S  wtsubst δ  wftrms (subst_range δ)  t = s  δ"
using t
proof (induction S)
  case (Cons x S) thus ?case
  proof (cases x)
    case (Insert t' s)
    hence "t = pair (t',s)  θ  t  pair ` setopssst (S sst θ)"
      using Cons.prems subst_sst_cons[of _ S θ]
      unfolding pair_def by (force simp add: setopssst_def)
    thus ?thesis
      using Insert Cons.IH θ by (cases "t = pair (t', s)  θ") (fastforce, auto)
  next
    case (Delete t' s)
    hence "t = pair (t',s)  θ  t  pair ` setopssst (S sst θ)"
      using Cons.prems subst_sst_cons[of _ S θ]
      unfolding pair_def by (force simp add: setopssst_def)
    thus ?thesis
      using Delete Cons.IH θ by (cases "t = pair (t', s)  θ") (fastforce, auto)
  next
    case (InSet ac t' s)
    hence "t = pair (t',s)  θ  t  pair ` setopssst (S sst θ)"
      using Cons.prems subst_sst_cons[of _ S θ]
      unfolding pair_def by (force simp add: setopssst_def)
    thus ?thesis
      using InSet Cons.IH θ by (cases "t = pair (t', s)  θ") (fastforce, auto)
  next
    case (NegChecks X F F')
    hence "t  pair ` set (F' pairs rm_vars (set X) θ)  t  pair ` setopssst (S sst θ)"
      using Cons.prems subst_sst_cons[of _ S θ]
      unfolding pair_def by (force simp add: setopssst_def)
    thus ?thesis
    proof
      assume "t  pair ` set (F' pairs rm_vars (set X) θ)"
      then obtain s where s: "t = s  rm_vars (set X) θ" "s  pair ` set F'"
        using subst_apply_pairs_pair_image_subst[of F' "rm_vars (set X) θ"] by auto
      thus ?thesis
        using NegChecks setopssst_pair_image_cons(8)[of X F F' S]
              wt_subst_rm_vars[OF θ(1), of "set X"]
              wf_trms_subst_rm_vars'[OF θ(2), of "set X"]
        by fast
    qed (use Cons.IH in auto)
  qed (auto simp add: setopssst_def subst_sst_cons[of _ S θ])
qed (simp add: setopssst_def)

lemma setopssst_wftrms:
  "wftrms (trmssst A)  wftrms (pair ` setopssst A)"
  "wftrms (trmssst A)  wftrms (trmssst A  pair ` setopssst A)"
proof -
  show "wftrms (trmssst A)  wftrms (pair ` setopssst A)"
  proof (induction A)
    case (Cons a A)
    hence 0: "wftrms (trmssstp a)" "wftrms (pair ` setopssst A)" by auto
    thus ?case
    proof (cases a)
      case (NegChecks X F F')
      hence "wftrms (trmspairs F')" using 0 by simp
      thus ?thesis using NegChecks wftrms_pairs[of F'] 0 by (auto simp add: setopssst_def)
    qed (auto simp add: setopssst_def dest: fun_pair_wftrm)
  qed (auto simp add: setopssst_def)
  thus "wftrms (trmssst A)  wftrms (trmssst A  pair ` setopssst A)" by fast
qed

lemma SMP_MP_split:
  assumes "t  SMP M"
    and M: "m  M. is_Fun m"
  shows "(δ. wtsubst δ  wftrms (subst_range δ)  t  M set δ) 
         t  SMP ((subtermsset M  ((set  fst  Ana) ` M)) - M)"
  (is "?P t  ?Q t")
using assms(1)
proof (induction t rule: SMP.induct)
  case (MP t)
  have "wtsubst Var" "wftrms (subst_range Var)" "M set Var = M" by simp_all
  thus ?case using MP by metis
next
  case (Subterm t t')
  show ?case using Subterm.IH
  proof
    assume "?P t"
    then obtain s δ where s: "s  M" "t = s  δ" and δ: "wtsubst δ" "wftrms (subst_range δ)" by auto
    then obtain f T where fT: "s = Fun f T" using M by fast

    have "(s'. s'  s  t' = s'  δ)  (x  fv s. t'  δ x)"
      using subterm_subst_unfold[OF Subterm.hyps(2)[unfolded s(2)]] by blast
    thus ?thesis
    proof
      assume "s'. s'  s  t' = s'  δ"
      then obtain s' where s': "s'  s" "t' = s'  δ" by fast
      show ?thesis
      proof (cases "s'  M")
        case True thus ?thesis using s' δ by blast
      next
        case False
        hence "s'  (subtermsset M  ((set  fst  Ana) ` M)) - M" using s'(1) s(1) by force
        thus ?thesis using SMP.Substitution[OF SMP.MP[of s'] δ] s' by presburger
      qed
    next
      assume "x  fv s. t'  δ x"
      then obtain x where x: "x  fv s" "t'  δ x" by fast
      have "Var x  M" using M by blast
      hence "Var x  (subtermsset M  ((set  fst  Ana) ` M)) - M"
        using s(1) var_is_subterm[OF x(1)] by blast
      hence "δ x  SMP ((subtermsset M  ((set  fst  Ana) ` M)) - M)"
        using SMP.Substitution[OF SMP.MP[of "Var x"] δ] by auto
      thus ?thesis using SMP.Subterm x(2) by presburger
    qed
  qed (metis SMP.Subterm[OF _ Subterm.hyps(2)])
next
  case (Substitution t δ)
  show ?case using Substitution.IH
  proof
    assume "?P t"
    then obtain θ where "wtsubst θ" "wftrms (subst_range θ)" "t  M set θ" by fast
    hence "wtsubst (θ s δ)" "wftrms (subst_range (θ s δ))" "t  δ  M set (θ s δ)"
      using wt_subst_compose[of θ, OF _ Substitution.hyps(2)]
            wf_trm_subst_compose[of θ _ δ, OF _ wf_trm_subst_rangeD[OF Substitution.hyps(3)]]
            wf_trm_subst_range_iff
      by (argo, blast, auto)
    thus ?thesis by blast
  next
    assume "?Q t" thus ?thesis using SMP.Substitution[OF _ Substitution.hyps(2,3)] by meson
  qed
next
  case (Ana t K T k)
  show ?case using Ana.IH
  proof
    assume "?P t"
    then obtain θ where θ: "wtsubst θ" "wftrms (subst_range θ)" "t  M set θ" by fast
    then obtain s where s: "s  M" "t = s  θ" by auto
    then obtain f S where fT: "s = Fun f S" using M by (cases s) auto
    obtain K' T' where s_Ana: "Ana s = (K', T')" by (metis surj_pair)
    hence "set K = set K' set θ" "set T = set T' set θ"
      using Ana_subst'[of f S K' T'] fT Ana.hyps(2) s(2) by auto
    then obtain k' where k': "k'  set K'" "k = k'  θ" using Ana.hyps(3) by fast
    show ?thesis
    proof (cases "k'  M")
      case True thus ?thesis using k' θ(1,2) by blast
    next
      case False
      hence "k'  (subtermsset M  ((set  fst  Ana) ` M)) - M" using k'(1) s_Ana s(1) by force
      thus ?thesis using SMP.Substitution[OF SMP.MP[of k'] θ(1,2)] k'(2) by presburger
    qed
  next
    assume "?Q t" thus ?thesis using SMP.Ana[OF _ Ana.hyps(2,3)] by meson
  qed
qed

lemma setops_subterm_trms:
  assumes t: "t  pair ` setopssst S"
    and s: "s  t"
  shows "s  subtermsset (trmssst S)"
proof -
  obtain u u' where u: "pair (u,u')  pair ` setopssst S" "t = pair (u,u')"
    using t setopssst_are_pairs[of _ S] by blast
  hence "s  u  s  u'" using s unfolding pair_def by auto
  thus ?thesis using u setopssst_member_iff[of u u' S] unfolding trmssst_def by force
qed

lemma setops_subterms_cases:
  assumes t: "t  subtermsset (pair ` setopssst S)"
  shows "t  subtermsset (trmssst S)  t  pair ` setopssst S"
proof -
  obtain s s' where s: "pair (s,s')  pair ` setopssst S" "t  pair (s,s')"
    using t setopssst_are_pairs[of _ S] by blast
  hence "t  pair ` setopssst S  t  s  t  s'" unfolding pair_def by auto
  thus ?thesis using s setopssst_member_iff[of s s' S] unfolding trmssst_def by force
qed

lemma setops_SMP_cases:
  assumes "t  SMP (pair ` setopssst S)"
    and "p. Ana (pair p) = ([], [])"
  shows "(δ. wtsubst δ  wftrms (subst_range δ)  t  pair ` setopssst S set δ)  t  SMP (trmssst S)"
proof -
  have 0: "((set  fst  Ana) ` pair ` setopssst S) = {}"
  proof (induction S)
    case (Cons x S) thus ?case
      using assms(2) by (cases x) (auto simp add: setopssst_def)
  qed (simp add: setopssst_def)
  
  have 1: "m  pair ` setopssst S. is_Fun m"
  proof (induction S)
    case (Cons x S) thus ?case
      unfolding pair_def by (cases x) (auto simp add: assms(2) setopssst_def)
  qed (simp add: setopssst_def)

  have 2:
      "subtermsset (pair ` setopssst S) 
       ((set  fst  Ana) ` (pair ` setopssst S)) - pair ` setopssst S
         subtermsset (trmssst S)"
    using 0 setops_subterms_cases by fast

  show ?thesis
    using SMP_MP_split[OF assms(1) 1] SMP_mono[OF 2] SMP_subterms_eq[of "trmssst S"]
    by blast
qed

lemma constraint_model_priv_const_in_constr_prefix:
  assumes A: "wfsst A"
    and I: "I s A"
           "interpretationsubst I"
           "wftrms (subst_range I)"
           "wtsubst I"
    and c: "¬public c"
           "arity c = 0"
           "Fun c [] set iksst A set I"
  shows "Fun c [] set trmssst A"
using const_subterms_subst_cases[OF c(3)]
proof
  assume "Fun c [] set iksst A" thus ?thesis using iksst_trmssst_subset by blast 
next
  assume "x  fvset (iksst A). x  subst_domain I  Fun c []  I x"
  then obtain x where x: "x  fvset (iksst A)" "Fun c []  I x" by blast
  
  have 0: "wftrm (I x)" "wf'sst {} A" "Fun c []  I = Fun c []"
    using I A by simp_all

  have 1: "x  wfrestrictedvarssst A"
    using x(1) in_iksst_iff[of _ A] unfolding wfrestrictedvarssst_def by force
  hence 2: "v  wfrestrictedvarssst A. Fun c []  I  I v" using 0(3) x(2) by force


  obtain Apre Asuf where A': "¬(w  wfrestrictedvarssst Apre. Fun c []  I w)"
    "(ts. A = Apre@send⟨ts#Asuf  Fun c [] set set ts set I) 
     (s u. A = Apre@assign: s  u#Asuf  Fun c []  s  I  ¬(Fun c [] set (I ` fv u))) 
     (s u. A = Apre@assign: s  u#Asuf  (Fun c []  s  I  Fun c []  u  I))"
    (is "?X  ?Y  ?Z")
    using wfsst_strand_first_Send_var_split[OF 0(2) 2] by force

  show ?thesis using A'(2)
  proof (elim disjE)
    assume ?X
    then obtain ts where ts: "A = Apre@send⟨ts#Asuf" "Fun c [] set set ts set I" by blast
    hence "I s (Apre@[send⟨ts])"
      using I(1) strand_sem_append_stateful[of "{}" "{}" "Apre@[send⟨ts]" Asuf I] by auto
    hence "(iksst Apre) set I  t  I" when "t  set ts" for t
      using that strand_sem_append_stateful[of "{}" "{}" Apre "[send⟨ts]" I]
            strand_sem_stateful.simps(2)[of _ _ ts "[]"]
      unfolding list_all_iff by force
    hence "Fun c [] set iksst Apre set I"
      using ts(2) c(1) private_fun_deduct_in_ik by fast
    hence "Fun c [] set iksst Apre"
      using A'(1) const_subterms_subst_cases[of c I "iksst Apre"]
            iksst_fv_subset_wfrestrictedvarssst[of Apre]
      by fast
    thus ?thesis
      using iksst_trmssst_subset[of "Apre"] unfolding ts(1) by fastforce
  next
    assume ?Y
    then obtain s u where su:
        "A = Apre@assign: s  u#Asuf" "Fun c []  s  I" "¬(Fun c [] set I ` fv u)"
      by fast
    hence "s  I = u  I"
      using I(1) strand_sem_append_stateful[of "{}" "{}" "Apre@[assign: s  u]" Asuf I]
            strand_sem_append_stateful[of _ _ Apre "[assign: s  u]" I]
      by auto
    hence "Fun c []  u" using su(2,3) const_subterm_subst_var_obtain[of c u I] by auto
    thus ?thesis unfolding su(1) by auto
  next
    assume ?Z
    then obtain s u where su:
        "A = Apre@assign: s  u#Asuf" "Fun c []  s  I  Fun c []  u  I"
      by fast
    hence "(s,u) p I  dbupdsst Apre I {}"
      using I(1) strand_sem_append_stateful[of "{}" "{}" "Apre@[assign: s  u]" Asuf I]
            strand_sem_append_stateful[of _ _ Apre "[assign: s  u]" I]
      unfolding dbsst_def by auto
    then obtain s' u' where su': "insert⟨s',u'  set Apre" "s  I = s'  I" "u  I = u'  I"
      using dbsst_in_cases[of "s  I" "u  I" Apre I "[]"] dbsst_set_is_dbupdsst[of Apre I "[]"]
      by fastforce

    have "fv s'  fv u'  wfrestrictedvarssst Apre"
      using su'(1) unfolding wfrestrictedvarssst_def by force
    hence "Fun c []  s'  Fun c []  u'"
      using su(2) A'(1) su'(2,3)
            const_subterm_subst_cases[of c s' I]
            const_subterm_subst_cases[of c u' I]
      by auto
    thus ?thesis using su'(1) unfolding su(1) by force
  qed
qed

lemma trpairs_empty_case:
  assumes "trpairs F D = []"
  shows "D = []" "F  []"
proof -
  show "F  []" using assms by (auto intro: ccontr)

  have "trpairs F (a#A)  []" for a A
    by (induct F "a#A" rule: trpairs.induct) fastforce+
  thus "D = []" using assms by (cases D) simp_all
qed

lemma trpairs_elem_length_eq:
  assumes "G  set (trpairs F D)"
  shows "length G = length F" 
using assms by (induct F D arbitrary: G rule: trpairs.induct) auto

lemma trpairs_index:
  assumes "G  set (trpairs F D)" "i < length F"
  shows "d  set D. G ! i = (pair (F ! i), pair d)"
using assms
proof (induction F D arbitrary: i G rule: trpairs.induct)
  case (2 s t F D)
  obtain d G' where G:
      "d  set D" "G'  set (trpairs F D)"
      "G = (pair (s,t), pair d)#G'"
    using "2.prems"(1) by atomize_elim auto 
  show ?case
    using "2.IH"[OF G(1,2)] "2.prems"(2) G(1,3)
    by (cases i) auto
qed simp

lemma trpairs_cons:
  assumes "G  set (trpairs F D)" "d  set D"
  shows "(pair (s,t), pair d)#G  set (trpairs ((s,t)#F) D)"
using assms by auto

lemma trpairs_has_pair_lists:
  assumes "G  set (trpairs F D)" "g  set G"
  shows "f  set F. d  set D. g = (pair f, pair d)"
using assms
proof (induction F D arbitrary: G rule: trpairs.induct)
  case (2 s t F D)
  obtain d G' where G:
      "d  set D" "G'  set (trpairs F D)"
      "G = (pair (s,t), pair d)#G'"
    using "2.prems"(1) by atomize_elim auto
  show ?case
    using "2.IH"[OF G(1,2)] "2.prems"(2) G(1,3)
    by (cases "g  set G'") auto
qed simp

lemma trpairs_is_pair_lists:
  assumes "f  set F" "d  set D"
  shows "G  set (trpairs F D). (pair f, pair d)  set G"
  (is "?P F D f d")
proof -
  have "f  set F. d  set D. ?P F D f d"
  proof (induction F D rule: trpairs.induct)
    case (2 s t F D)
    hence IH: "f  set F. d  set D. ?P F D f d" by metis
    moreover have "d  set D. ?P ((s,t)#F) D (s,t) d"
    proof
      fix d assume d: "d  set D"
      then obtain G where G: "G  set (trpairs F D)"
        using trpairs_empty_case(1) by force
      hence "(pair (s, t), pair d)#G  set (trpairs ((s,t)#F) D)"
        using d by auto
      thus "?P ((s,t)#F) D (s,t) d" using d G by auto
    qed
    ultimately show ?case by fastforce
  qed simp
  thus ?thesis by (metis assms)
qed

lemma trpairs_db_append_subset:
  "set (trpairs F D)  set (trpairs F (D@E))" (is ?A)
  "set (trpairs F E)  set (trpairs F (D@E))" (is ?B)
proof -
  show ?A
  proof (induction F D rule: trpairs.induct)
    case (2 s t F D)
    show ?case
    proof
      fix G assume "G  set (trpairs ((s,t)#F) D)"
      then obtain d G' where G':
          "d  set D" "G'  set (trpairs F D)" "G = (pair (s,t), pair d)#G'"
        by atomize_elim auto
      have "d  set (D@E)" "G'  set (trpairs F (D@E))" using "2.IH"[OF G'(1)] G'(1,2) by auto
      thus "G  set (trpairs ((s,t)#F) (D@E))" using G'(3) by auto
    qed
  qed simp

  show ?B
  proof (induction F E rule: trpairs.induct)
    case (2 s t F E)
    show ?case
    proof
      fix G assume "G  set (trpairs ((s,t)#F) E)"
      then obtain d G' where G':
          "d  set E" "G'  set (trpairs F E)" "G = (pair (s,t), pair d)#G'"
        by atomize_elim auto
      have "d  set (D@E)" "G'  set (trpairs F (D@E))" using "2.IH"[OF G'(1)] G'(1,2) by auto
      thus "G  set (trpairs ((s,t)#F) (D@E))" using G'(3) by auto
    qed
  qed simp
qed

lemma trpairs_trms_subset:
  "G  set (trpairs F D)  trmspairs G  pair ` set F  pair ` set D"
proof (induction F D arbitrary: G rule: trpairs.induct)
  case (2 s t F D G)
  obtain d G' where G:
      "d  set D" "G'  set (trpairs F D)" "G = (pair (s,t), pair d)#G'"
    using "2.prems"(1) by atomize_elim auto
 
  show ?case using "2.IH"[OF G(1,2)] G(1,3) by auto
qed simp

lemma trpairs_trms_subset':
  "(trmspairs ` set (trpairs F D))  pair ` set F  pair ` set D"
using trpairs_trms_subset by blast

lemma trpairs_vars_subset:
  "G  set (trpairs F D)  fvpairs G  fvpairs F  fvpairs D"
proof (induction F D arbitrary: G rule: trpairs.induct)
  case (2 s t F D G)
  obtain d G' where G:
      "d  set D" "G'  set (trpairs F D)" "G = (pair (s,t), pair d)#G'"
    using "2.prems"(1) by atomize_elim auto
 
  show ?case using "2.IH"[OF G(1,2)] G(1,3) unfolding pair_def by auto
qed simp

lemma trpairs_vars_subset': "(fvpairs ` set (trpairs F D))  fvpairs F  fvpairs D"
using trpairs_vars_subset[of _ F D] by blast


lemma tr_trms_subset:
  "A'  set (tr A D)  trmsst A'  trmssst A  pair ` setopssst A  pair ` set D"
proof (induction A D arbitrary: A' rule: tr.induct)
  case 1 thus ?case by simp
next
  case (2 t A D)
  then obtain A'' where A'': "A' = send⟨tst#A''" "A''  set (tr A D)" by atomize_elim auto
  hence "trmsst A''  trmssst A  pair ` setopssst A  pair ` set D" by (metis "2.IH")
  thus ?case using A'' by (auto simp add: setopssst_def)
next
  case (3 t A D)
  then obtain A'' where A'': "A' = receive⟨tst#A''" "A''  set (tr A D)" by atomize_elim auto
  hence "trmsst A''  trmssst A  pair ` setopssst A  pair ` set D" by (metis "3.IH")
  thus ?case using A'' by (auto simp add: setopssst_def)
next
  case (4 ac t t' A D)
  then obtain A'' where A'': "A' = ac: t  t'st#A''" "A''  set (tr A D)" by atomize_elim auto
  hence "trmsst A''  trmssst A  pair ` setopssst A  pair ` set D" by (metis "4.IH")
  thus ?case using A'' by (auto simp add: setopssst_def)
next
  case (5 t s A D)
  hence "A'  set (tr A (List.insert (t,s) D))" by simp
  hence "trmsst A'  trmssst A  pair ` setopssst A  pair ` set (List.insert (t, s) D)"
    by (metis "5.IH")
  thus ?case by (auto simp add: setopssst_def)
next
  case (6 t s A D)
  from 6 obtain Di A'' B C where A'':
      "Di  set (subseqs D)" "A''  set (tr A [dD. d  set Di])" "A' = (B@C)@A''"
      "B = map (λd. check: (pair (t,s))  (pair d)st) Di"
      "C = map (λd. Inequality [] [(pair (t,s) , pair d)]) [dD. d  set Di]"
    by atomize_elim auto
  hence "trmsst A''  trmssst A  pair ` setopssst A  pair ` set [dD. d  set Di]"
    by (metis "6.IH")
  hence "trmsst A''  trmssst (Delete t s#A)  pair ` setopssst (Delete t s#A)  pair ` set D"
    by (auto simp add: setopssst_def)
  moreover have "trmsst (B@C)  insert (pair (t,s)) (pair ` set D)"
    using A''(4,5) subseqs_set_subset[OF A''(1)] by auto
  moreover have "pair (t,s)  pair ` setopssst (Delete t s#A)" by (simp add: setopssst_def)
  ultimately show ?case using A''(3) trmsst_append[of "B@C" A'] by auto
next
  case (7 ac t s A D)
  from 7 obtain d A'' where A'':
      "d  set D" "A''  set (tr A D)"
      "A' = ac: (pair (t,s))  (pair d)st#A''"
    by atomize_elim auto
  hence "trmsst A''  trmssst A  pair ` setopssst A  pair ` set D" by (metis "7.IH")
  moreover have "trmsst A' = {pair (t,s), pair d}  trmsst A''"
    using A''(1,3) by auto
  ultimately show ?case using A''(1) by (auto simp add: setopssst_def)
next
  case (8 X F F' A D)
  from 8 obtain A'' where A'':
      "A''  set (tr A D)" "A' = (map (λG. X⟨∨≠: (F@G)st) (trpairs F' D))@A''"
    by atomize_elim auto

  define B where "B  (trmspairs ` set (trpairs F' D))"

  have "trmsst A''  trmssst A  pair ` setopssst A  pair ` set D" by (metis A''(1) "8.IH")
  hence "trmsst A'  B  trmspairs F  trmssst A  pair ` setopssst A  pair ` set D"
    using A'' B_def by auto
  moreover have "B  pair ` set F'  pair ` set D"
    using trpairs_trms_subset'[of F' D] B_def by simp
  moreover have "pair ` setopssst (X⟨∨≠: F ∨∉: F'#A) = pair ` set F'  pair ` setopssst A"
    by (auto simp add: setopssst_def)
  ultimately show ?case by auto
qed

lemma tr_vars_subset:
  assumes "A'  set (tr A D)"
  shows "fvst A'  fvsst A  ((t,t')  set D. fv t  fv t')" (is ?P)
  and "bvarsst A'  bvarssst A" (is ?Q)
proof -
  show ?P using assms
  proof (induction A arbitrary: A' D rule: strand_sem_stateful_induct)
    case (ConsIn A' D ac t s A)
    then obtain A'' d where *:
        "d  set D" "A' = ac: (pair (t,s))  (pair d)st#A''"
        "A''  set (tr A D)"
      by atomize_elim auto
    hence "fvst A''  fvsst A  ((t,t')set D. fv t  fv t')" by (metis ConsIn.IH)
    thus ?case using * unfolding pair_def by auto
  next
    case (ConsDel A' D t s A)
    define Dfv where "Dfv  λD::('fun,'var) dbstatelist. ((t,t')set D. fv t  fv t')"
    define fltD where "fltD  λDi. filter (λd. d  set Di) D"
    define constr where
      "constr  λDi. (map (λd. check: (pair (t,s))  (pair d)st) Di)@
                      (map (λd. []⟨∨≠: [(pair (t,s), pair d)]st) (fltD Di))"
    from ConsDel obtain A'' Di where *:
        "Di  set (subseqs D)" "A' = (constr Di)@A''" "A''  set (tr A (fltD Di))"
      unfolding constr_def fltD_def by atomize_elim auto
    hence "fvst A''  fvsst A  Dfv (fltD Di)"
      unfolding Dfv_def constr_def fltD_def by (metis ConsDel.IH)
    moreover have "Dfv (fltD Di)  Dfv D" unfolding Dfv_def constr_def fltD_def by auto
    moreover have "Dfv Di  Dfv D"
      using subseqs_set_subset(1)[OF *(1)] unfolding Dfv_def constr_def fltD_def by fast
    moreover have "fvst (constr Di)  fv t  fv s  (Dfv Di  Dfv (fltD Di))"
      unfolding Dfv_def constr_def fltD_def pair_def by auto
    moreover have "fvsst (Delete t s#A) = fv t  fv s  fvsst A" by auto
    moreover have "fvst A' = fvst (constr Di)  fvst A''" using * by force
    ultimately have "fvst A'  fvsst (Delete t s#A)  Dfv D" by auto
    thus ?case unfolding Dfv_def fltD_def constr_def by simp
  next
    case (ConsNegChecks A' D X F F' A)
    then obtain A'' where A'':
        "A''  set (tr A D)" "A' = (map (λG. X⟨∨≠: (F@G)st) (trpairs F' D))@A''"
      by atomize_elim auto

    define B where "B  (fvpairs ` set (trpairs F' D))"

    have 1: "fvst (map (λG. X⟨∨≠: (F@G)st) (trpairs F' D))  (B  fvpairs F) - set X"
      unfolding B_def by auto

    have 2: "B  fvpairs F'  fvpairs D"
      using trpairs_vars_subset'[of F' D]
      unfolding B_def by simp

    have "fvst A'  ((fvpairs F'  fvpairs D  fvpairs F) - set X)  fvst A''"
      using 1 2 A''(2) by fastforce
    thus ?case using ConsNegChecks.IH[OF A''(1)] by auto
  qed fastforce+

  show ?Q using assms by (induct A arbitrary: A' D rule: strand_sem_stateful_induct) fastforce+
qed

lemma tr_vars_disj:
  assumes "A'  set (tr A D)" "(t,t')  set D. (fv t  fv t')  bvarssst A = {}"
    and "fvsst A  bvarssst A = {}"
  shows "fvst A'  bvarsst A' = {}"
using assms tr_vars_subset by fast


lemma tfrsstp_alt_def:
  "list_all tfrsstp S =
    ((ac t t'. Equality ac t t'  set S  (δ. Unifier δ t t')  Γ t = Γ t') 
     (X F F'. NegChecks X F F'  set S  (
        (F' = []  (x  fvpairs F-set X. a. Γ (Var x) = TAtom a)) 
        (f T. Fun f T  subtermsset (trmspairs F  pair ` set F') 
                  T = []  (s  set T. s  Var ` set X)))))"
  (is "?P S = ?Q S")
proof
  show "?P S  ?Q S"
  proof (induction S)
    case (Cons x S) thus ?case by (cases x) auto
  qed simp

  show "?Q S  ?P S"
  proof (induction S)
    case (Cons x S) thus ?case by (cases x) auto
  qed simp
qed

lemma tfrsst_Nil[simp]: "tfrsst []"
by (simp add: tfrsst_def setopssst_def)

lemma tfrsst_append: "tfrsst (A@B)  tfrsst A"
proof -
  assume assms: "tfrsst (A@B)"
  let ?M = "trmssst A  pair ` setopssst A"
  let ?N = "trmssst (A@B)  pair ` setopssst (A@B)"
  let ?P = "λt t'. x  fv t  fv t'. a. Γ (Var x) = Var a"
  let ?Q = "λX t t'. X = []  (x  (fv t  fv t')-set X. a. Γ (Var x) = Var a)"
  have *: "SMP ?M - Var`𝒱  SMP ?N - Var`𝒱" "?M  ?N"
    using SMP_mono[of ?M ?N] setopssst_append[of A B]
    by auto
  { fix s t assume **: "tfrset ?N" "s  SMP ?M - Var`𝒱" "t  SMP ?M - Var`𝒱" "(δ. Unifier δ s t)"
    hence "s  SMP ?N - Var`𝒱" "t  SMP ?N - Var`𝒱" using * by auto
    hence "Γ s = Γ t" using **(1,4) unfolding tfrset_def by blast
  } moreover have "t  ?N. wftrm t  t  ?M. wftrm t" using * by blast
  ultimately have "tfrset ?N  tfrset ?M" unfolding tfrset_def by blast
  hence "tfrset ?M" using assms unfolding tfrsst_def by metis
  thus "tfrsst A" using assms unfolding tfrsst_def by simp
qed

lemma tfrsst_append': "tfrsst (A@B)  tfrsst B"
proof -
  assume assms: "tfrsst (A@B)"
  let ?M = "trmssst B  pair ` setopssst B"
  let ?N = "trmssst (A@B)  pair ` setopssst (A@B)"
  let ?P = "λt t'. x  fv t  fv t'. a. Γ (Var x) = Var a"
  let ?Q = "λX t t'. X = []  (x  (fv t  fv t')-set X. a. Γ (Var x) = Var a)"
  have *: "SMP ?M - Var`𝒱  SMP ?N - Var`𝒱" "?M  ?N"
    using SMP_mono[of ?M ?N] setopssst_append[of A B]
    by auto
  { fix s t assume **: "tfrset ?N" "s  SMP ?M - Var`𝒱" "t  SMP ?M - Var`𝒱" "(δ. Unifier δ s t)"
    hence "s  SMP ?N - Var`𝒱" "t  SMP ?N - Var`𝒱" using * by auto
    hence "Γ s = Γ t" using **(1,4) unfolding tfrset_def by blast
  } moreover have "t  ?N. wftrm t  t  ?M. wftrm t" using * by blast
  ultimately have "tfrset ?N  tfrset ?M" unfolding tfrset_def by blast
  hence "tfrset ?M" using assms unfolding tfrsst_def by metis
  thus "tfrsst B" using assms unfolding tfrsst_def by simp
qed

lemma tfrsst_cons: "tfrsst (a#A)  tfrsst A"
using tfrsst_append'[of "[a]" A] by simp

lemma tfrsstp_subst:
  assumes s: "tfrsstp s"
    and θ: "wtsubst θ" "wftrms (subst_range θ)" "set (bvarssstp s)  range_vars θ = {}"
  shows "tfrsstp (s sstp θ)"
proof (cases s)
  case (Equality a t t')
  thus ?thesis
  proof (cases "δ. Unifier δ (t  θ) (t'  θ)")
    case True
    hence "δ. Unifier δ t t'" by (metis subst_subst_compose[of _ θ])
    moreover have "Γ t = Γ (t  θ)" "Γ t' = Γ (t'  θ)" by (metis wt_subst_trm''[OF assms(2)])+
    ultimately have "Γ (t  θ) = Γ (t'  θ)" using s Equality by simp
    thus ?thesis using Equality True by simp
  qed simp
next
  case (NegChecks X F G)
  let ?P = "λF G. G = []  (x  fvpairs F-set X. a. Γ (Var x) = TAtom a)"
  let ?Q = "λF G. f T. Fun f T  subtermsset (trmspairs F  pair ` set G) 
                          T = []  (s  set T. s  Var ` set X)"
  let  = "rm_vars (set X) θ"

  have "?P F G  ?Q F G" using NegChecks assms(1) by simp
  hence "?P (F pairs ) (G pairs )  ?Q (F pairs ) (G pairs )"
  proof
    assume *: "?P F G"
    have "G pairs  = []" using * by simp
    moreover have "a. Γ (Var x) = TAtom a" when x: "x  fvpairs (F pairs ) - set X" for x
    proof -
      obtain t t' where t: "(t,t')  set (F pairs )" "x  fv t  fv t' - set X"
        using x(1) by auto
      then obtain u u' where u: "(u,u')  set F" "u   = t" "u'   = t'"
        unfolding subst_apply_pairs_def by auto
      obtain y where y: "y  fv u  fv u' - set X" "x  fv ( y)"
        using t(2) u(2,3) rm_vars_fv_obtain by fast
      hence a: "a. Γ (Var y) = TAtom a" using u * by auto
      
      have a': "Γ (Var y) = Γ ( y)"
        using wt_subst_trm''[OF wt_subst_rm_vars[OF θ(1), of "set X"], of "Var y"]
        by simp

      have "(z.  y = Var z)  (c.  y = Fun c [])"
      proof (cases " y  subst_range θ")
        case True thus ?thesis
          using a a' θ(2) const_type_inv_wf
          by (cases " y") fastforce+
      qed fastforce
      hence " y = Var x" using y(2) by fastforce
      hence "Γ (Var x) = Γ (Var y)" using a' by simp
      thus ?thesis using a by presburger
    qed
    ultimately show ?thesis by simp
  next
    assume *: "?Q F G"
    have **: "set X  range_vars  = {}"
      using θ(3) NegChecks rm_vars_img_fv_subset[of "set X" θ] by auto
    have "?Q (F pairs ) (G pairs )"
      using ineq_subterm_inj_cond_subst[OF ** *]
            trmspairs_subst[of F "rm_vars (set X) θ"]
            subst_apply_pairs_pair_image_subst[of G "rm_vars (set X) θ"]
      by (metis (no_types, lifting) image_Un)
    thus ?thesis by simp
  qed
  thus ?thesis using NegChecks by simp
qed simp_all

lemma tfrsstp_all_wt_subst_apply:
  assumes S: "list_all tfrsstp S"
    and θ: "wtsubst θ" "wftrms (subst_range θ)" "bvarssst S  range_vars θ = {}"
  shows "list_all tfrsstp (S sst θ)"
proof -
  have "set (bvarssstp s)  range_vars θ = {}" when "s  set S" for s
    using that θ(3) unfolding bvarssst_def range_vars_alt_def by fastforce
  thus ?thesis
    using tfrsstp_subst[OF _ θ(1,2)] S
    unfolding list_all_iff
    by (auto simp add: subst_apply_stateful_strand_def)
qed

lemma tfr_setops_if_tfr_trms:
  assumes "Pair  (funs_term ` SMP (trmssst S))"
    and "p. Ana (pair p) = ([], [])"
    and "s  pair ` setopssst S. t  pair ` setopssst S. (δ. Unifier δ s t)  Γ s = Γ t"
    and "s  pair ` setopssst S. t  pair ` setopssst S.
          (σ θ ρ. wtsubst σ  wtsubst θ  wftrms (subst_range σ)  wftrms (subst_range θ) 
                   Unifier ρ (s  σ) (t  θ))
           (δ. Unifier δ s t)"
    and tfr: "tfrset (trmssst S)"
  shows "tfrset (trmssst S  pair ` setopssst S)"
proof -
  have 0: "t  SMP (trmssst S) - range Var  t  SMP (pair ` setopssst S) - range Var"
    when "t  SMP (trmssst S  pair ` setopssst S) - range Var" for t
    using that SMP_union by blast

  have 1: "s  SMP (trmssst S) - range Var"
      when st: "s  SMP (pair ` setopssst S) - range Var"
               "t  SMP (trmssst S) - range Var"
               "δ. Unifier δ s t"
         for s t
  proof -
    have "(δ. s  pair ` setopssst S set δ)  s  SMP (trmssst S) - range Var"
      using st setops_SMP_cases[of s S] assms(2) by blast
    moreover {
      fix δ assume δ: "s  pair ` setopssst S set δ"
      then obtain s' where s': "s'  pair ` setopssst S" "s = s'  δ" by blast
      then obtain u u' where u: "s' = Fun Pair [u,u']"
        using setopssst_are_pairs[of s'] unfolding pair_def by fast
      hence *: "s = Fun Pair [u  δ, u'  δ]" using δ s' by simp

      obtain f T where fT: "t = Fun f T" using st(2) by (cases t) auto
      hence "f  Pair" using st(2) assms(1) by auto
      hence False using st(3) * fT s' u by fast
    } ultimately show ?thesis by meson
  qed
  
  have 2: "Γ s = Γ t"
      when "s  SMP (trmssst S) - range Var"
           "t  SMP (trmssst S) - range Var"
           "δ. Unifier δ s t"
       for s t
    using that tfr unfolding tfrset_def by blast
  
  have 3: "Γ s = Γ t"
      when st: "s  SMP (pair ` setopssst S) - range Var"
               "t  SMP (pair ` setopssst S) - range Var"
               "δ. Unifier δ s t"
      for s t
  proof -
    let ?P = "λs δ. wtsubst δ  wftrms (subst_range δ)  s  pair ` setopssst S set δ"
    have "(δ. ?P s δ)  s  SMP (trmssst S) - range Var"
         "(δ. ?P t δ)  t  SMP (trmssst S) - range Var"
      using setops_SMP_cases[of _ S] assms(2) st(1,2) by auto
    hence "(δ δ'. ?P s δ  ?P t δ')  Γ s = Γ t" by (metis 1 2 st)
    moreover {
      fix δ δ' assume *: "?P s δ" "?P t δ'"
      then obtain s' t' where **:
          "s'  pair ` setopssst S" "t'  pair ` setopssst S" "s = s'  δ" "t = t'  δ'"
        by blast
      hence "θ. Unifier θ s' t'" using st(3) assms(4) * by blast
      hence "Γ s' = Γ t'" using assms(3) ** by blast
      hence "Γ s = Γ t" using * **(3,4) wt_subst_trm''[of δ s'] wt_subst_trm''[of δ' t'] by argo
    } ultimately show ?thesis by blast
  qed
  
  show ?thesis using 0 1 2 3 unfolding tfrset_def by metis
qed

end


subsection ‹The Typing Result for Stateful Constraints›

subsubsection ‹Correctness of the Constraint Reduction›
context stateful_typed_model
begin

context
begin
private lemma tr_wf':
  assumes "(t,t')  set D. (fv t  fv t')  bvarssst A = {}"
  and "(t,t')  set D. fv t  fv t'  X"
  and "wf'sst X A" "fvsst A  bvarssst A = {}"
  and "A'  set (tr A D)"
  shows "wfst X A'"
proof -
  define P where
    "P = (λ(D::('fun,'var) dbstatelist) (A::('fun,'var) stateful_strand).
          ((t,t')  set D. (fv t  fv t')  bvarssst A = {})  fvsst A  bvarssst A = {})"

  have "P D A" using assms(1,4) by (simp add: P_def)
  with assms(5,3,2) show ?thesis
  proof (induction A arbitrary: A' D X rule: wf'sst.induct)
    case 1 thus ?case by simp
  next
    case (2 X ts A A')
    then obtain A'' where A'': "A' = receive⟨tsst#A''" "A''  set (tr A D)" "fvset (set ts)  X"
      by atomize_elim auto
    have *: "wf'sst X A" "(s,s')  set D. fv s  fv s'  X" "P D A"
      using 2(1,2,3,4) apply (force, force)
      using 2(5) unfolding P_def by force
    show ?case using "2.IH"[OF A''(2) *] A''(1,3) by simp
  next
    case (3 X ts A A')
    then obtain A'' where A'': "A' = send⟨tsst#A''" "A''  set (tr A D)"
      by atomize_elim auto
    have *: "wf'sst (X  fvset (set ts)) A"
            "(s,s')  set D. fv s  fv s'  X  fvset (set ts)" "P D A"
      using 3(1,2,3,4) apply (force, force)
      using 3(5) unfolding P_def by force
    show ?case using "3.IH"[OF A''(2) *] A''(1) by simp
  next
    case (4 X t t' A A')
    then obtain A'' where A'': "A' = assign: t  t'st#A''" "A''  set (tr A D)" "fv t'  X"
      by atomize_elim auto
    have *: "wf'sst (X  fv t) A" "(s,s')  set D. fv s  fv s'  X  fv t" "P D A"
      using 4(1,2,3,4) apply (force, force)
      using 4(5) unfolding P_def by force
    show ?case using "4.IH"[OF A''(2) *] A''(1,3) by simp
  next
    case (5 X t t' A A')
    then obtain A'' where A'': "A' = check: t  t'st#A''" "A''  set (tr A D)"
      by atomize_elim auto
    have *: "wf'sst X A" "P D A"
      using 5(3) apply force
      using 5(5) unfolding P_def by force
    show ?case using "5.IH"[OF A''(2) *(1) 5(4) *(2)] A''(1) by simp
  next
    case (6 X t s A A')
    hence A': "A'  set (tr A (List.insert (t,s) D))" "fv t  X" "fv s  X" by auto
    have *: "wf'sst X A" "(s,s')  set (List.insert (t,s) D). fv s  fv s'  X" using 6 by auto
    have **: "P (List.insert (t,s) D) A" using 6(5) unfolding P_def by force
    show ?case using "6.IH"[OF A'(1) * **] A'(2,3) by simp
  next
    case (7 X t s A A')
    let ?constr = "λDi. (map (λd. check: (pair (t,s))  (pair d)st) Di)@
                        (map (λd. []⟨∨≠: [(pair (t,s), pair d)]st) [dD. d  set Di])"
    from 7 obtain Di A'' where A'':
        "A' = ?constr Di@A''" "A''  set (tr A [dD. d  set Di])"
        "Di  set (subseqs D)"
      by atomize_elim force
    have *: "wf'sst X A" "(t',s')  set [dD. d  set Di]. fv t'  fv s'  X"
      using 7 by auto
    have **: "P [dD. d  set Di] A" using 7 unfolding P_def by force
    have ***: "(t, t')  set D. fv t  fv t'  X" using 7 by auto
    show ?case
      using "7.IH"[OF A''(2) * **] A''(1) wf_fun_pair_eqs_ineqs_map[OF _ A''(3) ***]
      by simp
  next
    case (8 X t s A A')
    then obtain d A'' where A'':
        "A' = assign: (pair (t,s))  (pair d)st#A''"
        "A''  set (tr A D)" "d  set D"
      by atomize_elim auto
    have *: "wf'sst (X  fv t  fv s) A" "(t',s')set D. fv t'  fv s'  X  fv t  fv s" "P D A"
      using 8(1,2,3,4) apply (force, force)
      using 8(5) unfolding P_def by force
    have **: "fv (pair d)  X" using A''(3) "8.prems"(3) unfolding pair_def by fastforce
    have ***: "fv (pair (t,s)) = fv s  fv t" unfolding pair_def by auto
    show ?case using "8.IH"[OF A''(2) *] A''(1) ** *** unfolding pair_def by (simp add: Un_assoc)
  next
    case (9 X t s A A')
    then obtain d A'' where A'':
        "A' = check: (pair (t,s))  (pair d)st#A''"
        "A''  set (tr A D)" "d  set D"
      by atomize_elim auto
    have *: "wf'sst X A""P D A"
      using 9(3) apply force
      using 9(5) unfolding P_def by force
    have **: "fv (pair d)  X" using A''(3) "9.prems"(3) unfolding pair_def by fastforce
    have ***: "fv (pair (t,s)) = fv s  fv t" unfolding pair_def by auto
    show ?case using "9.IH"[OF A''(2) *(1) 9(4) *(2)] A''(1) ** *** by (simp add: Un_assoc)
  next
    case (10 X Y F F' A A')
    from 10 obtain A'' where A'':
        "A' = (map (λG. Y⟨∨≠: (F@G)st) (trpairs F' D))@A''" "A''  set (tr A D)"
      by atomize_elim auto

    have *: "wf'sst X A" "(t',s')  set D. fv t'  fv s'  X" using 10 by auto
    
    have "bvarssst A  bvarssst (Y⟨∨≠: F ∨∉: F'#A)" "fvsst A  fvsst (Y⟨∨≠: F ∨∉: F'#A)" by auto
    hence **:  "P D A" using 10 unfolding P_def by blast

    show ?case using "10.IH"[OF A''(2) * **] A''(1) wf_fun_pair_negchecks_map by simp
  qed
qed

private lemma tr_wftrms:
  assumes "A'  set (tr A [])" "wftrms (trmssst A)"
  shows "wftrms (trmsst A')"
using tr_trms_subset[OF assms(1)] setopssst_wftrms(2)[OF assms(2)]
by auto

lemma tr_wf:
  assumes "A'  set (tr A [])"
    and "wfsst A"
    and "wftrms (trmssst A)" 
  shows "wfst {} A'"
    and "wftrms (trmsst A')"
    and "fvst A'  bvarsst A' = {}"
using tr_wf'[OF _ _ _ _ assms(1)]
      tr_wftrms[OF assms(1,3)]
      tr_vars_disj[OF assms(1)]
      assms(2)
by fastforce+

private lemma fun_pair_ineqs:
  assumes "d p δ p θ  d' p "
  shows "pair d  δ  θ  pair d'  "
proof -
  have "d p (δ s θ)  d' p " using assms subst_pair_compose by metis
  hence "pair d  (δ s θ)  pair d'  " using fun_pair_eq_subst by metis
  thus ?thesis by simp
qed

private lemma tr_Delete_constr_iff_aux1:
  assumes "d  set Di. (t,s) p  = d p "
  and "d  set D - set Di. (t,s) p   d p "
  shows "M; (map (λd. check: (pair (t,s))  (pair d)st) Di)@
             (map (λd. []⟨∨≠: [(pair (t,s), pair d)]st) [dD. d  set Di])d "
proof -
  from assms(2) have
    "M; map (λd. []⟨∨≠: [(pair (t,s), pair d)]st) [dD. d  set Di]d "
  proof (induction D)
    case (Cons d D)
    hence IH: "M; map (λd. []⟨∨≠: [(pair (t,s), pair d)]st) [dD . d  set Di]d " by auto
    thus ?case
    proof (cases "d  set Di")
      case False
      hence "(t,s) p   d p " using Cons by simp
      hence "pair (t,s)    pair d  " using fun_pair_eq_subst by metis
      moreover have "t (δ::('fun,'var) subst). subst_domain δ = {}  t  δ = t" by auto
      ultimately have "δ. subst_domain δ = {}  pair (t,s)  δ    pair d  δ  " by metis
      thus ?thesis using IH by (simp add: ineq_model_def)
    qed simp
  qed simp
  moreover {
    fix B assume "M; Bd " 
    with assms(1) have "M; (map (λd. check: (pair (t,s))  (pair d)st) Di)@Bd "
      unfolding pair_def by (induction Di) auto
  } ultimately show ?thesis by metis
qed

private lemma tr_Delete_constr_iff_aux2:
  assumes "ground M"
  and "M; (map (λd. check: (pair (t,s))  (pair d)st) Di)@
           (map (λd. []⟨∨≠: [(pair (t,s), pair d)]st) [dD. d  set Di])d "
  shows "(d  set Di. (t,s) p  = d p )  (d  set D - set Di. (t,s) p   d p )"
proof -
  let ?c1 = "map (λd. check: (pair (t,s))  (pair d)st) Di"
  let ?c2 = "map (λd. []⟨∨≠: [(pair (t,s), pair d)]st) [dD. d  set Di]"

  have "M set  = M" using assms(1) subst_all_ground_ident by metis
  moreover have "ikst ?c1 = {}" by auto
  ultimately have *:
       "M; map (λd. check: (pair (t,s))  (pair d)st) Did "
       "M; map (λd. []⟨∨≠: [(pair (t,s), pair d)]st) [dD. d  set Di]d "
    using strand_sem_split(3,4)[of M ?c1 ?c2 ] assms(2) by auto
  
  from *(1) have 1: "d  set Di. (t,s) p  = d p " unfolding pair_def by (induct Di) auto
  from *(2) have 2: "d  set D - set Di. (t,s) p   d p "
  proof (induction D arbitrary: Di)
    case (Cons d D) thus ?case
    proof (cases "d  set Di")
      case False
      hence IH: "d  set D - set Di. (t,s) p   d p " using Cons by force
      have "t (δ::('fun,'var) subst). subst_domain δ = {}  ground (subst_range δ)  δ = Var"
        by auto
      moreover have "ineq_model  [] [((pair (t,s)), (pair d))]"
        using False Cons.prems by simp
      ultimately have "pair (t,s)    pair d  " by (simp add: ineq_model_def)
      thus ?thesis using IH unfolding pair_def by force
    qed simp
  qed simp

  show ?thesis by (metis 1 2)
qed

private lemma tr_Delete_constr_iff:
  fixes ::"('fun,'var) subst"
  assumes "ground M"
  shows "set Di pset   {(t,s) p }  (t,s) p   (set D - set Di) pset  
         M; (map (λd. check: (pair (t,s))  (pair d)st) Di)@
             (map (λd. []⟨∨≠: [(pair (t,s), pair d)]st) [dD. d  set Di])d "
proof -
  let ?constr = "(map (λd. check: (pair (t,s))  (pair d)st) Di)@
                 (map (λd. []⟨∨≠: [(pair (t,s), pair d)]st) [dD. d  set Di])"
  { assume "set Di pset   {(t,s) p }" "(t,s) p   (set D - set Di) pset "
    hence "d  set Di. (t,s) p  = d p " "d  set D - set Di. (t,s) p   d p "
      by auto
    hence "M; ?constrd " using tr_Delete_constr_iff_aux1 by simp
  } moreover {
    assume "M; ?constrd "
    hence "d  set Di. (t,s) p  = d p " "d  set D - set Di. (t,s) p   d p "
      using assms tr_Delete_constr_iff_aux2 by auto
    hence "set Di pset   {(t,s) p }  (t,s) p   (set D - set Di) pset " by force
  } ultimately show ?thesis by metis
qed

private lemma tr_NotInSet_constr_iff:
  fixes ::"('fun,'var) subst"
  assumes "(t,t')  set D. (fv t  fv t')  set X = {}"
  shows "(δ. subst_domain δ = set X  ground (subst_range δ)  (t,s) p δ p   set D pset )
           M; map (λd. X⟨∨≠: [(pair (t,s), pair d)]st) Dd "
proof -
  { assume "δ. subst_domain δ = set X  ground (subst_range δ)  (t,s) p δ p   set D pset "
    with assms have "M; map (λd. X⟨∨≠: [(pair (t,s), pair d)]st) Dd "
    proof (induction D)
      case (Cons d D)
      obtain t' s' where d: "d = (t',s')" by atomize_elim auto
      have "M; map (λd. X⟨∨≠: [(pair (t,s), pair d)]st) Dd "
           "map (λd. X⟨∨≠: [(pair (t,s), pair d)]st) (d#D) =
            X⟨∨≠: [(pair (t,s), pair d)]st#map (λd. X⟨∨≠: [(pair (t,s), pair d)]st) D"
        using Cons by auto
      moreover have
          "δ. subst_domain δ = set X  ground (subst_range δ)  pair (t, s)  δ    pair d  "
        using fun_pair_ineqs[of  _  "(t,s)"  d] Cons.prems(2) by auto
      moreover have "(fv t'  fv s')  set X = {}" using Cons.prems(1) d by auto
      hence "δ. subst_domain δ = set X  pair d  δ = pair d" using d unfolding pair_def by auto
      ultimately show ?case by (simp add: ineq_model_def)
    qed simp
  } moreover {
    fix δ::"('fun,'var) subst"
    assume "M; map (λd. X⟨∨≠: [(pair (t,s), pair d)]st) Dd "
      and δ: "subst_domain δ = set X" "ground (subst_range δ)"
    with assms have "(t,s) p δ p   set D pset "
    proof (induction D)
      case (Cons d D)
      obtain t' s' where d: "d = (t',s')" by atomize_elim auto
      have "(t,s) p δ p   set D pset "
           "pair (t,s)  δ    pair d  δ  "
        using Cons d by (auto simp add: ineq_model_def simp del: subst_range.simps)
      moreover have "pair d  δ = pair d"
        using Cons.prems(1) fun_pair_subst[of d δ] d δ(1) unfolding pair_def by auto
      ultimately show ?case unfolding pair_def by force
    qed simp
  } ultimately show ?thesis by metis
qed

lemma tr_NegChecks_constr_iff:
  "(Gset L. ineq_model  X (F@G))  M; map (λG. X⟨∨≠: (F@G)st) Ld " (is ?A)
  "negchecks_model  D X F F'  M; D; [X⟨∨≠: F ∨∉: F']s " (is ?B)
proof -
  show ?A by (induct L) auto
  show ?B by simp
qed

lemma trpairs_sem_equiv:
  fixes ::"('fun,'var) subst"
  assumes "(t,t')  set D. (fv t  fv t')  set X = {}"
  shows "negchecks_model  (set D pset ) X F F' 
         (G  set (trpairs F' D). ineq_model  X (F@G))"
proof -
  define P where
    "P  λδ::('fun,'var) subst. subst_domain δ = set X  ground (subst_range δ)" 

  define Ineq where
    "Ineq  λ(δ::('fun,'var) subst) F. (s,t)  set F. s  δ s   t  δ s "

  define Ineq' where
    "Ineq'  λ(δ::('fun,'var) subst) F. (s,t)  set F. s  δ s   t  "
  
  define Notin where
    "Notin  λ(δ::('fun,'var) subst) D F'. (s,t)  set F'. (s,t) p δ s   set D pset "

  have sublmm:
      "((s,t) p δ s   set D pset )  (list_all (λd. Ineq' δ [(pair (s,t),pair d)]) D)"
    for s t δ D
    unfolding pair_def by (induct D) (auto simp add: Ineq'_def)

  have "Notin δ D F'  (G  set (trpairs F' D). Ineq' δ G)"
    (is "?A  ?B")
    when "P δ" for δ
  proof
    show "?A  ?B"
    proof (induction F' D rule: trpairs.induct)
      case (2 s t F' D)
      show ?case
      proof (cases "Notin δ D F'")
        case False
        hence "(s,t) p δ s   set D pset "
          using "2.prems"
          by (auto simp add: Notin_def)
        hence "pair (s,t)  δ s   pair d  " when "d  set D" for d
          using that sublmm Ball_set[of D "λd. Ineq' δ [(pair (s,t), pair d)]"]
          by (simp add: Ineq'_def)
        moreover have "d  set D. G'. G = (pair (s,t), pair d)#G'"
          when "G  set (trpairs ((s,t)#F') D)" for G
          using that trpairs_index[OF that, of 0] by force
        ultimately show ?thesis by (simp add: Ineq'_def)
      qed (auto dest: "2.IH" simp add: Ineq'_def)
    qed (simp add: Notin_def)

    have "¬?A  ¬?B"
    proof (induction F' D rule: trpairs.induct)
      case (2 s t F' D)
      hence "¬Notin δ D F'" "D  []" unfolding Notin_def by auto
      then obtain G where G: "G  set (trpairs F' D)" "¬Ineq' δ G"
        using "2.IH" by (cases D) auto

      obtain d where d: "d  set D" "pair (s,t)  δ s  = pair d  "
        using "2.prems"
        unfolding pair_def by (auto simp add: Notin_def)
      thus ?case
        using G(2) trpairs_cons[OF G(1) d(1)]
        by (auto simp add: Ineq'_def)
    qed (simp add: Ineq'_def)
    thus "?B  ?A" by metis
  qed
  hence *: "(δ. P δ  Ineq δ F  Notin δ D F') 
            (G  set (trpairs F' D). δ. P δ  Ineq δ F  Ineq' δ G)"
    by auto

  have "t  δ = t"
    when "G  set (trpairs F' D)" "(s,t)  set G" "P δ"
    for δ s t G
    using assms that(3) trpairs_has_pair_lists[OF that(1,2)]
    unfolding pair_def by (fastforce simp add: P_def)
  hence **: "Ineq' δ G = Ineq δ G"
    when "G  set (trpairs F' D)" "P δ"
    for δ G
    using that unfolding Ineq_def Ineq'_def by force

  have ***: "negchecks_model  (set D pset ) X F F'  (δ. P δ  Ineq δ F  Notin δ D F')"
    unfolding P_def Ineq_def Notin_def negchecks_model_def by blast

  have "ineq_model  X (F@G)  (δ. P δ  Ineq δ (F@G))" for G
    unfolding P_def Ineq_def ineq_model_def by blast
  hence ****: "ineq_model  X (F@G)  (δ. P δ  Ineq δ F  Ineq δ G)" for G
    unfolding Ineq_def by fastforce

  show ?thesis
    using * ** *** **** by simp
qed

lemma tr_sem_equiv':
  assumes "(t,t')  set D. (fv t  fv t')  bvarssst A = {}"
    and "fvsst A  bvarssst A = {}"
    and "ground M"
    and : "interpretationsubst "
  shows "M; set D pset ; As   (A'  set (tr A D). M; A'd )" (is "?P  ?Q")
proof
  have ℐ_grounds: "t. fv (t  ) = {}" by (rule interpretation_grounds[OF ])
  have "A'  set (tr A D). M; A'd " when ?P using that assms(1,2,3)
  proof (induction A arbitrary: D rule: strand_sem_stateful_induct)
    case (ConsRcv M D ts A)
    have "(set ts set )  M; set D pset ; As "
         "(t,t')  set D. (fv t  fv t')  bvarssst A = {}"
         "fvsst A  bvarssst A = {}" "ground ((set ts set )  M)"
      using  ConsRcv.prems unfolding fvsst_def bvarssst_def by force+
    then obtain A' where A': "A'  set (tr A D)" "(set ts set )  M; A'd " by (metis ConsRcv.IH)
    thus ?case by auto
  next
    case (ConsSnd M D ts A)
    have "M; set D pset ; As "
         "(t,t')  set D. (fv t  fv t')  bvarssst A = {}"
         "fvsst A  bvarssst A = {}" "ground M"
      and *: "t  set ts. M  t  "
      using  ConsSnd.prems unfolding fvsst_def bvarssst_def by force+
    then obtain A' where A': "A'  set (tr A D)" "M; A'd " by (metis ConsSnd.IH)
    thus ?case using * by auto
  next
    case (ConsEq M D ac t t' A)
    have "M; set D pset ; As "
         "(t,t')  set D. (fv t  fv t')  bvarssst A = {}"
         "fvsst A  bvarssst A = {}" "ground M"
      and *: "t   = t'  "
      using  ConsEq.prems unfolding fvsst_def bvarssst_def by force+
    then obtain A' where A': "A'  set (tr A D)" "M; A'd " by (metis ConsEq.IH)
    thus ?case using * by auto
  next
    case (ConsIns M D t s A)
    have "M; set (List.insert (t,s) D) pset ; As "
         "(t,t')  set (List.insert (t,s) D). (fv t  fv t')  bvarssst A = {}"
         "fvsst A  bvarssst A = {}" "ground M"
      using ConsIns.prems unfolding fvsst_def bvarssst_def by force+
    then obtain A' where A': "A'  set (tr A (List.insert (t,s) D))" "M; A'd "
      by (metis ConsIns.IH)
    thus ?case by auto
  next
    case (ConsDel M D t s A)
    have *: "M; (set D pset ) - {(t,s) p }; As "
            "(t,t')set D. (fv t  fv t')  bvarssst A = {}"
            "fvsst A  bvarssst A = {}" "ground M"
      using ConsDel.prems unfolding fvsst_def bvarssst_def by force+
    then obtain Di where Di:
        "Di  set D" "Di pset   {(t,s) p }" "(t,s) p   (set D - Di) pset "
      using subset_subst_pairs_diff_exists'[of "set D"] by atomize_elim auto
    hence **: "(set D pset ) - {(t,s) p } = (set D - Di) pset " by blast

    obtain Di' where Di': "set Di' = Di" "Di'  set (subseqs D)"
      using subset_sublist_exists[OF Di(1)] by atomize_elim auto
    hence ***: "(set D pset ) - {(t,s) p } = (set [dD. d  set Di'] pset )"
      using Di ** by auto
    
    define constr where "constr 
        map (λd. check: (pair (t,s))  (pair d)st) Di'@
        map (λd. []⟨∨≠: [(pair (t,s), pair d)]st) [dD. d  set Di']"
    
    have ****: "(t,t')set [dD. d  set Di']. (fv t  fv t')  bvarssst A = {}"
      using *(2) Di(1) Di'(1) subseqs_set_subset[OF Di'(2)] by simp
    have "set D - Di = set [dD. d  set Di']" using Di Di' by auto
    hence *****: "M; set [dD. d  set Di'] pset ; As "
      using *(1) ** by metis
    obtain A' where A': "A'  set (tr A [dD. d  set Di'])" "M; A'd "
      using ConsDel.IH[OF ***** **** *(3,4)] by atomize_elim auto
    hence constr_sat: "M; constrd "
      using Di Di' *(1) *** tr_Delete_constr_iff[OF *(4), of  Di' t s D] 
      unfolding constr_def by auto

    have "constr@A'  set (tr (Delete t s#A) D)" using A'(1) Di' unfolding constr_def by auto
    moreover have "ikst constr = {}" unfolding constr_def by auto
    hence "M set ; constrd " "M  (ikst constr set ); A'd "
      using constr_sat A'(2) subst_all_ground_ident[OF *(4)] by simp_all
    ultimately show ?case
      using strand_sem_append(2)[of _ _ ]
            subst_all_ground_ident[OF *(4), of ]
      by metis
  next
    case (ConsIn M D ac t s A)
    have "M; set D pset ; As "
         "(t,t')  set D. (fv t  fv t')  bvarssst A = {}"
         "fvsst A  bvarssst A = {}" "ground M"
      and *: "(t,s) p   set D pset "
      using  ConsIn.prems unfolding fvsst_def bvarssst_def by force+
    then obtain A' where A': "A'  set (tr A D)" "M; A'd " by (metis ConsIn.IH)
    moreover obtain d where "d  set D" "pair (t,s)   = pair d  "
      using * unfolding pair_def by auto
    ultimately show ?case using * by auto
  next
    case (ConsNegChecks M D X F F' A)
    let ?ineqs = "(map (λG. X⟨∨≠: (F@G)st) (trpairs F' D))"
    have 1: "M; set D pset ; As " "ground M" using ConsNegChecks by auto
    have 2: "(t,t')  set D. (fv t  fv t')  bvarssst A = {}" "fvsst A  bvarssst A = {}" 
      using ConsNegChecks.prems(2,3)  unfolding fvsst_def bvarssst_def by fastforce+
    
    have 3: "negchecks_model  (set D pset ) X F F'" using ConsNegChecks.prems(1) by simp
    from 1 2 obtain A' where A': "A'  set (tr A D)" "M; A'd " by (metis ConsNegChecks.IH)
    
    have 4: "(t,t')  set D. (fv t  fv t')  set X = {}"
      using ConsNegChecks.prems(2) unfolding bvarssst_def by auto
    
    have "M; ?ineqsd "
      using 3 trpairs_sem_equiv[OF 4] tr_NegChecks_constr_iff
      by metis
    moreover have "ikst ?ineqs = {}" by auto
    moreover have "M set  = M" using 1(2)  by (simp add: subst_all_ground_ident)
    ultimately show ?case
      using strand_sem_append(2)[of M ?ineqs  A'] A'
      by force
  qed simp
  thus "?P  ?Q" by metis

  have "(A'  set (tr A D). M; A'd )  ?P" using assms(1,2,3)
  proof (induction A arbitrary: D rule: strand_sem_stateful_induct)
    case (ConsRcv M D ts A)
    have "A'  set (tr A D). (set ts set )  M; A'd "
         "(t,t')  set D. (fv t  fv t')  bvarssst A = {}"
         "fvsst A  bvarssst A = {}" "ground ((set ts set )  M)"
      using  ConsRcv.prems unfolding fvsst_def bvarssst_def by force+
    hence "(set ts set )  M; set D pset ; As " by (metis ConsRcv.IH)
    thus ?case by auto
  next
    case (ConsSnd M D ts A)
    have "A'  set (tr A D). M; A'd "
         "(t,t')  set D. (fv t  fv t')  bvarssst A = {}"
         "fvsst A  bvarssst A = {}" "ground M"
      and *: "t  set ts. M  t  "
      using  ConsSnd.prems unfolding fvsst_def bvarssst_def by force+
    hence "M; set D pset ; As " by (metis ConsSnd.IH)
    thus ?case using * by auto
  next
    case (ConsEq M D ac t t' A)
    have "A'  set (tr A D). M; A'd "
         "(t,t')  set D. (fv t  fv t')  bvarssst A = {}"
         "fvsst A  bvarssst A = {}" "ground M"
      and *: "t   = t'  "
      using  ConsEq.prems unfolding fvsst_def bvarssst_def by force+
    hence "M; set D pset ; As " by (metis ConsEq.IH)
    thus ?case using * by auto
  next
    case (ConsIns M D t s A)
    hence "A'  set (tr A (List.insert (t,s) D)). M; A'd "
          "(t,t')  set (List.insert (t,s) D). (fv t  fv t')  bvarssst A = {}"
          "fvsst A  bvarssst A = {}" "ground M"
      unfolding fvsst_def bvarssst_def by auto+
    hence "M; set (List.insert (t,s) D) pset ; As " by (metis ConsIns.IH)
    thus ?case by auto
  next
    case (ConsDel M D t s A)
    define constr where "constr 
      λDi. map (λd. check: (pair (t,s))  (pair d)st) Di@
           map (λd. []⟨∨≠: [(pair (t,s), pair d)]st) [dD. d  set Di]"
    let ?flt = "λDi. filter (λd. d  set Di) D"

    have "Di  set (subseqs D). B'  set (tr A (?flt Di)). B = constr Di@B'"
      when "B  set (tr (delete⟨t,s#A) D)" for B
      using that unfolding constr_def by auto
    then obtain A' Di where A':
        "constr Di@A'  set (tr (Delete t s#A) D)"
        "A'  set (tr A (?flt Di))"
        "Di  set (subseqs D)"
        "M; constr Di@A'd "
      using ConsDel.prems(1) by blast

    have 1: "(t,t')set (?flt Di). (fv t  fv t')  bvarssst A = {}" using ConsDel.prems(2) by auto
    have 2: "fvsst A  bvarssst A = {}" using ConsDel.prems(3) by force+
    have "ikst (constr Di) = {}" unfolding constr_def by auto
    hence 3: "M; A'd "
      using subst_all_ground_ident[OF ConsDel.prems(4)] A'(4)
            strand_sem_split(4)[of M "constr Di" A' ]
      by simp
    have IH: "M; set (?flt Di) pset ; As "
      by (metis ConsDel.IH[OF _ 1 2 ConsDel.prems(4)] 3 A'(2))

    have "M; constr Did "
      using subst_all_ground_ident[OF ConsDel.prems(4)] strand_sem_split(3) A'(4)
      by metis
    hence *: "set Di pset   {(t,s) p }" "(t,s) p   (set D - set Di) pset "
      using tr_Delete_constr_iff[OF ConsDel.prems(4), of  Di t s D] unfolding constr_def by auto
    have 4: "set (?flt Di) pset  = (set D pset ) - {((t,s) p )}"
    proof
      show "set (?flt Di) pset   (set D pset ) - {((t,s) p )}"
      proof
        fix u u' assume u: "(u,u')  set (?flt Di) pset "
        then obtain v v' where v: "(v,v')  set D - set Di" "(v,v') p  = (u,u')" by auto
        hence "(u,u')  (t,s) p " using * by force
        thus "(u,u')   (set D pset ) - {((t,s) p )}"
          using u v * subseqs_set_subset[OF A'(3)] by auto
      qed
      show "(set D pset ) - {((t,s) p )}  set (?flt Di) pset "
        using * subseqs_set_subset[OF A'(3)] by force
    qed

    show ?case using 4 IH by simp
  next
    case (ConsIn M D ac t s A)
    have "A'  set (tr A D). M; A'd "
         "(t,t')  set D. (fv t  fv t')  bvarssst A = {}"
         "fvsst A  bvarssst A = {}" "ground M"
      and *: "(t,s) p   set D pset "
      using ConsIn.prems(1,2,3,4) apply (fastforce, fastforce, fastforce, fastforce)
      using ConsIn.prems(1) tr.simps(7)[of ac t s A D] unfolding pair_def by fastforce
    hence "M; set D pset ; As " by (metis ConsIn.IH)
    moreover obtain d where "d  set D" "pair (t,s)   = pair d  "
      using * unfolding pair_def by auto
    ultimately show ?case using * by auto
  next
    case (ConsNegChecks M D X F F' A)
    let ?ineqs = "(map (λG. X⟨∨≠: (F@G)st) (trpairs F' D))"

    obtain B where B:
        "?ineqs@B  set (tr (NegChecks X F F'#A) D)" "M; ?ineqs@Bd " "B  set (tr A D)"
      using ConsNegChecks.prems(1) by atomize_elim auto
    moreover have "M set  = M"
      using ConsNegChecks.prems(4)  by (simp add: subst_all_ground_ident)
    moreover have "ikst ?ineqs = {}" by auto
    ultimately have "M; Bd " using strand_sem_split(4)[of M ?ineqs B ] by simp
    moreover have "(t,t')set D. (fv t  fv t')  bvarssst A = {}" "fvsst A  bvarssst A = {}"
      using ConsNegChecks.prems(2,3) unfolding fvsst_def bvarssst_def by force+
    ultimately have "M; set D pset ; As "
      by (metis ConsNegChecks.IH B(3) ConsNegChecks.prems(4))
    moreover have "(t, t')set D. (fv t  fv t')  set X = {}"
      using ConsNegChecks.prems(2) unfolding bvarssst_def by force
    ultimately show ?case
      using trpairs_sem_equiv tr_NegChecks_constr_iff
            B(2) strand_sem_split(3)[of M ?ineqs B ] M set  = M
      by simp
  qed simp
  thus "?Q  ?P" by metis
qed

lemma tr_sem_equiv:
  assumes "fvsst A  bvarssst A = {}" and "interpretationsubst "
  shows " s A  (A'  set (tr A []). (  A'))"
using tr_sem_equiv'[OF _ assms(1) _ assms(2), of "[]" "{}"]
unfolding constr_sem_d_def
by auto

end

end


subsubsection ‹Typing Result Locale Definition›

locale stateful_typing_result =
  stateful_typed_model arity public Ana Γ Pair
+ typing_result arity public Ana Γ
  for arity::"'fun  nat"
    and public::"'fun  bool"
    and Ana::"('fun,'var) term  (('fun,'var) term list × ('fun,'var) term list)"
    and Γ::"('fun,'var) term  ('fun,'atom::finite) term_type"
    and Pair::"'fun"


subsubsection ‹Type-Flaw Resistance Preservation of the Constraint Reduction›
context stateful_typing_result
begin

context
begin

private lemma tr_tfrsstp:
  assumes "A'  set (tr A D)" "list_all tfrsstp A"
  and "fvsst A  bvarssst A = {}" (is "?P0 A D")
  and "(t,s)  set D. (fv t  fv s)  bvarssst A = {}" (is "?P1 A D")
  and "t  pair ` setopssst A  pair ` set D. t'  pair ` setopssst A  pair ` set D.
          (δ. Unifier δ t t')  Γ t = Γ t'" (is "?P3 A D")
  shows "list_all tfrstp A'"
proof -
  have sublmm: "list_all tfrsstp A" "?P0 A D" "?P1 A D" "?P3 A D"
    when p: "list_all tfrsstp (a#A)" "?P0 (a#A) D" "?P1 (a#A) D" "?P3 (a#A) D"
    for a A D
    using p(1) apply (simp add: tfrsst_def)
    using p(2) fvsst_cons_subset bvarssst_cons_subset apply fast
    using p(3) bvarssst_cons_subset apply fast
    using p(4) setopssst_cons_subset by fast

  show ?thesis using assms
  proof (induction A D arbitrary: A' rule: tr.induct)
    case 1 thus ?case by simp
  next
    case (2 t A D)
    note prems = "2.prems"
    note IH = "2.IH"
    from prems(1) obtain A'' where A'': "A' = send⟨tst#A''" "A''  set (tr A D)"
      by atomize_elim auto
    have "list_all tfrstp A''" using IH[OF A''(2)] prems(5) sublmm[OF prems(2,3,4,5)] by meson
    thus ?case using A''(1) by simp
  next
    case (3 t A D)
    note prems = "3.prems"
    note IH = "3.IH"
    from prems(1) obtain A'' where A'': "A' = receive⟨tst#A''" "A''  set (tr A D)"
      by atomize_elim auto
    have "list_all tfrstp A''" using IH[OF A''(2)] prems(5) sublmm[OF prems(2,3,4,5)] by meson
    thus ?case using A''(1) by simp
  next
    case (4 ac t t' A D)
    note prems = "4.prems"
    note IH = "4.IH"
    from prems(1) obtain A'' where A'':
        "A' = ac: t  t'st#A''" "A''  set (tr A D)"
      by atomize_elim auto
    have "list_all tfrstp A''" using IH[OF A''(2)] prems(5) sublmm[OF prems(2,3,4,5)] by meson
    moreover have "(δ. Unifier δ t t')  Γ t = Γ t'" using prems(2) by (simp add: tfrsst_def)
    ultimately show ?case using A''(1) by auto
  next
    case (5 t s A D)
    note prems = "5.prems"
    note IH = "5.IH"
    from prems(1) have A': "A'  set (tr A (List.insert (t,s) D))" by simp
  
    have 1: "list_all tfrsstp A" using sublmm[OF prems(2,3,4,5)] by simp
  
    have "pair ` setopssst (Insert t s#A)  pair`set D =
          pair ` setopssst A  pair`set (List.insert (t,s) D)"
      by (simp add: setopssst_def)
    hence 3: "?P3 A (List.insert (t,s) D)" using prems(5) by metis
    moreover have "?P1 A (List.insert (t, s) D)" using prems(3,4) bvarssst_cons_subset[of A] by auto
    ultimately have "list_all tfrstp A'" using IH[OF A' sublmm(1,2)[OF prems(2,3,4,5)] _ 3] by metis
    thus ?case using A'(1) by auto
  next
    case (6 t s A D)
    note prems = "6.prems"
    note IH = "6.IH"
    
    define constr where constr:
      "constr  (λDi. (map (λd. check: (pair (t,s))  (pair d)st) Di)@
                       (map (λd. []⟨∨≠: [(pair (t,s), pair d)]st) [dD. d  set Di]))"
    
    from prems(1) obtain Di A'' where A'':
        "A' = constr Di@A''" "A''  set (tr A [dD. d  set Di])"
        "Di  set (subseqs D)"
      unfolding constr by auto
  
    define Q1 where "Q1  (λ(F::(('fun,'var) term × ('fun,'var) term) list) X.
        x  (fvpairs F) - set X. a. Γ (Var x) = TAtom a)"

    define Q2 where "Q2  (λ(F::(('fun,'var) term × ('fun,'var) term) list) X.
        f T. Fun f T  subtermsset (trmspairs F)  T = []  (s  set T. s  Var ` set X))"
  
    have "set [dD. d  set Di]  set D"
         "pair ` setopssst A  pair ` set [dD. d  set Di]
           pair ` setopssst (Delete t s#A)  pair ` set D"
      by (auto simp add: setopssst_def)
    hence *: "?P3 A [dD. d  set Di]" using prems(5) by blast
    have **: "?P1 A [dD. d  set Di]" using prems(4,5) by auto
    have 1: "list_all tfrstp A''"
      using IH[OF A''(3,2) sublmm(1,2)[OF prems(2,3,4,5)] ** *]
      by metis
  
    have 2: "ac: u  u'st  set A'' 
             (d  set Di. u = pair (t,s)  u' = pair d)"
      when "ac: u  u'st  set A'" for ac u u'
      using that A''(1) unfolding constr by force
    have 3: "Inequality X U  set A'  Inequality X U  set A'' 
             (d  set [dD. d  set Di].
                U = [(pair (t,s), pair d)]  Q2 [(pair (t,s), pair d)] X)"
        for X U
      using A''(1) unfolding Q2_def constr by force
    have 4:
        "dset D. (δ. Unifier δ (pair (t,s)) (pair d))  Γ (pair (t,s)) = Γ (pair d)"
      using prems(5) by (simp add: setopssst_def)
  
    { fix ac u u'
      assume a: "ac: u  u'st  set A'" "δ. Unifier δ u u'"
      hence "ac: u  u'st  set A''  (d  set Di. u = pair (t,s)  u' = pair d)"
        using 2 by metis
      hence "Γ u = Γ u'"
        using 1(1) 4 subseqs_set_subset[OF A''(3)] a(2) tfrstp_list_all_alt_def[of A'']
        by blast
    } moreover {
      fix u U
      assume "U⟨∨≠: ust  set A'"
      hence "U⟨∨≠: ust  set A'' 
             (d  set [dD. d  set Di]. u = [(pair (t,s), pair d)]  Q2 u U)"
        using 3 by metis
      hence "Q1 u U  Q2 u U"
        using 1 4 subseqs_set_subset[OF A''(3)] tfrstp_list_all_alt_def[of A'']
        unfolding Q1_def Q2_def
        by blast
    } ultimately show ?case using tfrstp_list_all_alt_def[of A'] unfolding Q1_def Q2_def by blast
  next
    case (7 ac t s A D)
    note prems = "7.prems"
    note IH = "7.IH"

    from prems(1) obtain d A'' where A'':
        "A' = ac: (pair (t,s))  (pair d)st#A''"
        "A''  set (tr A D)" "d  set D"
      by atomize_elim auto

    have "list_all tfrstp A''"
      using IH[OF A''(2) sublmm(1,2,3)[OF prems(2,3,4,5)] sublmm(4)[OF prems(2,3,4,5)]]
      by metis
    moreover have "(δ. Unifier δ (pair (t,s)) (pair d))  Γ (pair (t,s)) = Γ (pair d)"
      using prems(2,5) A''(3) unfolding tfrsst_def by (simp add: setopssst_def)
    ultimately show ?case using A''(1) by fastforce
  next
    case (8 X F F' A D)
    note prems = "8.prems"
    note IH = "8.IH"

    define constr where "constr = (map (λG. X⟨∨≠: (F@G)st) (trpairs F' D))"

    define Q1 where "Q1  (λ(F::(('fun,'var) term × ('fun,'var) term) list) X.
        x  (fvpairs F) - set X. a. Γ (Var x) = TAtom a)"

    define Q2 where "Q2  (λ(M::('fun,'var) terms) X.
        f T. Fun f T  subtermsset M  T = []  (s  set T. s  Var ` set X))"

    have Q2_subset: "Q2 M' X" when "M'  M" "Q2 M X" for X M M'
      using that unfolding Q2_def by auto

    have Q2_supset: "Q2 (M  M') X" when "Q2 M X" "Q2 M' X" for X M M'
      using that unfolding Q2_def by auto

    from prems(1) obtain A'' where A'': "A' = constr@A''" "A''  set (tr A D)"
      using constr_def by atomize_elim auto

    have 0: "F' = []  constr = [X⟨∨≠: Fst]" unfolding constr_def by simp

    have 1: "list_all tfrstp A''"
      using IH[OF A''(2) sublmm(1,2,3)[OF prems(2,3,4,5)] sublmm(4)[OF prems(2,3,4,5)]]
      by metis

    have 2: "(F' = []  Q1 F X)  Q2 (trmspairs F  pair ` set F') X"
      using prems(2) unfolding Q1_def Q2_def by simp
  
    have 3: "list_all tfrstp constr" when "F' = []" "Q1 F X"
      using that 0 2 tfrstp_list_all_alt_def[of constr] unfolding Q1_def by auto

    { fix c assume "c  set constr"
      hence "G  set (trpairs F' D). c = X⟨∨≠: (F@G)st" unfolding constr_def by force
    } moreover {
      fix G
      assume G: "G  set (trpairs F' D)"
         and c: "X⟨∨≠: (F@G)st  set constr"
         and e: "Q2 (trmspairs F  pair ` set F') X"

      have d_Q2: "Q2 (pair ` set D) X" unfolding Q2_def
      proof (intro allI impI)
        fix f T assume "Fun f T  subtermsset (pair ` set D)"
        then obtain d where d: "d  set D" "Fun f T  subterms (pair d)" by auto
        hence "fv (pair d)  set X = {}" using prems(4) unfolding pair_def by force
        thus "T = []  (s  set T. s  Var ` set X)"
          by (metis fv_disj_Fun_subterm_param_cases d(2))
      qed

      have "trmspairs (F@G)  trmspairs F  pair ` set F'  pair ` set D"
        using trpairs_trms_subset[OF G] by auto
      hence "Q2 (trmspairs (F@G)) X" using Q2_subset[OF _ Q2_supset[OF e d_Q2]] by metis
      hence "tfrstp (X⟨∨≠: (F@G)st)" by (metis Q2_def tfrstp.simps(2))
    } ultimately have 4: "list_all tfrstp constr" when "Q2 (trmspairs F  pair ` set F') X"
      using that Ball_set by blast

    have 5: "list_all tfrstp constr" using 2 3 4 by metis

    show ?case using 1 5 A''(1) by simp
  qed
qed

lemma tr_tfr:
  assumes "A'  set (tr A [])" and "tfrsst A" and "fvsst A  bvarssst A = {}"
  shows "tfrst A'"
proof -
  have *: "trmsst A'  trmssst A  pair ` setopssst A" using tr_trms_subset[OF assms(1)] by simp
  hence "SMP (trmsst A')  SMP (trmssst A  pair ` setopssst A)" using SMP_mono by simp
  moreover have "tfrset (trmssst A  pair ` setopssst A)" using assms(2) unfolding tfrsst_def by fast
  ultimately have 1: "tfrset (trmsst A')" by (metis tfr_subset(2)[OF _ *])

  have **: "list_all tfrsstp A" using assms(2) unfolding tfrsst_def by fast
  have "pair ` setopssst A  SMP (trmssst A  pair ` setopssst A) - Var`𝒱"
    using setopssst_are_pairs unfolding pair_def by auto
  hence ***: "t  pair`setopssst A. t'  pair`setopssst A. (δ. Unifier δ t t')  Γ t = Γ t'"
    using assms(2) unfolding tfrsst_def tfrset_def by blast
  have 2: "list_all tfrstp A'"
    using tr_tfrsstp[OF assms(1) ** assms(3)] *** unfolding pair_def by fastforce

  show ?thesis by (metis 1 2 tfrst_def)
qed

end

end


subsubsection ‹Theorem: The Stateful Typing Result›
context stateful_typing_result
begin

theorem stateful_typing_result:
  assumes "wfsst 𝒜"
    and "tfrsst 𝒜"
    and "wftrms (trmssst 𝒜)"
    and "interpretationsubst "
    and " s 𝒜"
  obtains τ
    where "interpretationsubst τ"
    and "τ s 𝒜"
    and "wtsubst τ"
    and "wftrms (subst_range τ)"
proof -
  obtain 𝒜' where 𝒜':
      "𝒜'  set (tr 𝒜 [])" "  𝒜'"
    using tr_sem_equiv[of 𝒜] assms(1,4,5)
    by auto

  have *: "wfst {} 𝒜'"
          "fvst 𝒜'  bvarsst 𝒜' = {}"
          "tfrst 𝒜'" "wftrms (trmsst 𝒜')"
    using tr_wf[OF 𝒜'(1) assms(1,3)]
          tr_tfr[OF 𝒜'(1) assms(2)] assms(1)
    by metis+

  obtain τ where τ:
      "interpretationsubst τ" "{}; 𝒜'd τ"
      "wtsubst τ" "wftrms (subst_range τ)"
    using wt_attack_if_tfr_attack_d 
          * Ana_invar_subst' assms(4)
          𝒜'(2)
    unfolding constr_sem_d_def
    by atomize_elim auto

  thus ?thesis
    using that tr_sem_equiv[of 𝒜] assms(1,3) 𝒜'(1)
    unfolding constr_sem_d_def
    by auto
qed

end


subsection ‹Proving Type-Flaw Resistance Automatically›
definition pair' where
  "pair' pair_fun d  case d of (t,t')  Fun pair_fun [t,t']"

fun comp_tfrsstp where
  "comp_tfrsstp Γ pair_fun (_: t  t') = (mgu t t'  None  Γ t = Γ t')"
| "comp_tfrsstp Γ pair_fun (X⟨∨≠: F ∨∉: F') = (
    (F' = []  (x  fvpairs F - set X. is_Var (Γ (Var x)))) 
    (u  subtermsset (trmspairs F  pair' pair_fun ` set F').
      is_Fun u  (args u = []  (s  set (args u). s  Var ` set X))))"
| "comp_tfrsstp _ _ _ = True"

definition comp_tfrsst where
  "comp_tfrsst arity Ana Γ pair_fun M S 
    list_all (comp_tfrsstp Γ pair_fun) S 
    list_all (wftrm' arity) (trms_listsst S) 
    has_all_wt_instances_of Γ (trmssst S  pair' pair_fun ` setopssst S) M 
    comp_tfrset arity Ana Γ M"

locale stateful_typed_model' = stateful_typed_model arity public Ana Γ Pair
  for arity::"'fun  nat"
    and public::"'fun  bool"
    and Ana::"('fun,(('fun,'atom::finite) term_type × nat)) term
               (('fun,(('fun,'atom) term_type × nat)) term list
                 × ('fun,(('fun,'atom) term_type × nat)) term list)"
    and Γ::"('fun,(('fun,'atom) term_type × nat)) term  ('fun,'atom) term_type"
    and Pair::"'fun"
  +
  assumes Γ_Var_fst': "τ n m. Γ (Var (τ,n)) = Γ (Var (τ,m))"
    and Ana_const': "c T. arity c = 0  Ana (Fun c T) = ([], [])"
begin

sublocale typed_model'
by (unfold_locales, rule Γ_Var_fst', metis Ana_const', metis Ana_subst')

lemma pair_code:
  "pair d = pair' Pair d"
by (simp add: pair_def pair'_def)

end

locale stateful_typing_result' =
  stateful_typed_model' arity public Ana Γ Pair + stateful_typing_result arity public Ana Γ Pair
  for arity::"'fun  nat"
    and public::"'fun  bool"
    and Ana::"('fun,(('fun,'atom::finite) term_type × nat)) term
               (('fun,(('fun,'atom) term_type × nat)) term list
                 × ('fun,(('fun,'atom) term_type × nat)) term list)"
    and Γ::"('fun,(('fun,'atom) term_type × nat)) term  ('fun,'atom) term_type"
    and Pair::"'fun"
begin

lemma tfrsstp_is_comp_tfrsstp: "tfrsstp a = comp_tfrsstp Γ Pair a"
proof (cases a)
  case (Equality ac t t')
  thus ?thesis
    using mgu_always_unifies[of t _ t'] mgu_gives_MGU[of t t']
    by auto
next
  case (NegChecks X F F')
  thus ?thesis
    using tfrsstp.simps(2)[of X F F']
          comp_tfrsstp.simps(2)[of Γ Pair X F F']
          Fun_range_case(2)[of "subtermsset (trmspairs F  pair ` set F')"]
    unfolding is_Var_def pair_code[symmetric]
    by auto
qed auto

lemma tfrsst_if_comp_tfrsst:
  assumes "comp_tfrsst arity Ana Γ Pair M S"
  shows "tfrsst S"
unfolding tfrsst_def
proof
  have comp_tfrset_M: "comp_tfrset arity Ana Γ M"
    using assms unfolding comp_tfrsst_def by blast

  have SMP_repr_M: "finite_SMP_representation arity Ana Γ M"
    using comp_tfrset_M unfolding comp_tfrset_def by blast
  
  have wftrms_M: "wftrms M"
      and wftrms_S: "wftrms (trmssst S  pair ` setopssst S)"
      and S_trms_instance_M: "has_all_wt_instances_of Γ (trmssst S  pair ` setopssst S) M"
    using assms setopssst_wftrms(2)[of S] trms_listsst_is_trmssst[of S]
          finite_SMP_representationD[OF SMP_repr_M]
    unfolding comp_tfrsst_def comp_tfrset_def list_all_iff pair_code[symmetric] wftrm_code[symmetric]
              finite_SMP_representation_def
    by (meson, argo, argo)

  show "tfrset (trmssst S  pair ` setopssst S)"
    using tfr_subset(3)[OF tfrset_if_comp_tfrset[OF comp_tfrset_M] SMP_SMP_subset]
          SMP_I'[OF wftrms_S wftrms_M S_trms_instance_M]
    by blast

  have "list_all (comp_tfrsstp Γ Pair) S" by (metis assms comp_tfrsst_def)
  thus "list_all tfrsstp S" by (induct S) (simp_all add: tfrsstp_is_comp_tfrsstp)
qed

lemma tfrsst_if_comp_tfrsst':
  fixes S
  defines "M  SMP0 Ana Γ (trms_listsst S@map pair (setops_listsst S))"
  assumes comp_tfr: "comp_tfrsst arity Ana Γ Pair (set M) S"
  shows "tfrsst S"
by (rule tfrsst_if_comp_tfrsst[OF comp_tfr[unfolded M_def]])

end

end