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⟨ts⟩st)) (tr A D)"
| "tr (receive⟨ts⟩#A) D = map ((#) (receive⟨ts⟩st)) (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) [d←D. d ∉ set Di])@B)
                          (tr A [d←D. 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) [d←D. 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) [d←D. 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⟨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 "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⟨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 "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 [d←D. 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)]) [d←D. d ∉ set Di]"
    by atomize_elim auto
  hence "trmsst A'' ⊆ trmssst A ∪ pair ` setopssst A ∪ pair ` set [d←D. 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⟨ts⟩st#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⟨ts⟩st#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) [d←D. d ∉ set Di])"
    from 7 obtain Di A'' where A'':
        "A' = ?constr Di@A''" "A'' ∈ set (tr A [d←D. d ∉ set Di])"
        "Di ∈ set (subseqs D)"
      by atomize_elim force
    have *: "wf'sst X A" "∀(t',s') ∈ set [d←D. d ∉ set Di]. fv t' ∪ fv s' ⊆ X"
      using 7 by auto
    have **: "P [d←D. 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) [d←D. d ∉ set Di])⟧d ℐ"
proof -
  from assms(2) have
    "⟦M; map (λd. ∀[]⟨∨≠: [(pair (t,s), pair d)]⟩st) [d←D. d ∉ set Di]⟧d ℐ"
  proof (induction D)
    case (Cons d D)
    hence IH: "⟦M; map (λd. ∀[]⟨∨≠: [(pair (t,s), pair d)]⟩st) [d←D . 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; B⟧d ℐ" 
    with assms(1) have "⟦M; (map (λd. ⟨check: (pair (t,s)) ≐ (pair d)⟩st) Di)@B⟧d ℐ"
      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) [d←D. 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) [d←D. 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) Di⟧d ℐ"
       "⟦M; map (λd. ∀[]⟨∨≠: [(pair (t,s), pair d)]⟩st) [d←D. 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) [d←D. 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) [d←D. 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; ?constr⟧d ℐ" using tr_Delete_constr_iff_aux1 by simp
  } moreover {
    assume "⟦M; ?constr⟧d ℐ"
    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) D⟧d ℐ"
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) D⟧d ℐ"
    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) D⟧d ℐ"
           "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) D⟧d ℐ"
      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:
  "(∀G∈set L. ineq_model ℐ X (F@G)) ⟷ ⟦M; map (λG. ∀X⟨∨≠: (F@G)⟩st) L⟧d ℐ" (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 ℐ; A⟧s ℐ ⟷ (∃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 ℐ; A⟧s ℐ"
         "∀(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 ℐ; A⟧s ℐ"
         "∀(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 ℐ; A⟧s ℐ"
         "∀(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 ℐ; A⟧s ℐ"
         "∀(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 ℐ}; A⟧s ℐ"
            "∀(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 [d←D. 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) [d←D. d ∉ set Di']"
    
    have ****: "∀(t,t')∈set [d←D. 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 [d←D. d ∉ set Di']" using Di Di' by auto
    hence *****: "⟦M; set [d←D. d ∉ set Di'] ⋅pset ℐ; A⟧s ℐ"
      using *(1) ** by metis
    obtain A' where A': "A' ∈ set (tr A [d←D. d ∉ set Di'])" "⟦M; A'⟧d ℐ"
      using ConsDel.IH[OF ***** **** *(3,4)] by atomize_elim auto
    hence constr_sat: "⟦M; constr⟧d ℐ"
      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 ℐ; constr⟧d ℐ" "⟦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 ℐ; A⟧s ℐ"
         "∀(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 ℐ; A⟧s ℐ" "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; ?ineqs⟧d ℐ"
      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 ℐ; A⟧s ℐ" 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 ℐ; A⟧s ℐ" 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 ℐ; A⟧s ℐ" 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 ℐ; A⟧s ℐ" 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) [d←D. 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 ℐ; A⟧s ℐ"
      by (metis ConsDel.IH[OF _ 1 2 ConsDel.prems(4)] 3 A'(2))

    have "⟦M; constr Di⟧d ℐ"
      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 ℐ; A⟧s ℐ" 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@B⟧d ℐ" "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; B⟧d ℐ" 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 ℐ; A⟧s ℐ"
      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⟨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
    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⟨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
    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) [d←D. d ∉ set Di]))"
    
    from prems(1) obtain Di A'' where A'':
        "A' = constr Di@A''" "A'' ∈ set (tr A [d←D. 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 [d←D. d ∉ set Di] ⊆ set D"
         "pair ` setopssst A ∪ pair ` set [d←D. d ∉ set Di]
          ⊆ pair ` setopssst (Delete t s#A) ∪ pair ` set D"
      by (auto simp add: setopssst_def)
    hence *: "?P3 A [d←D. d ∉ set Di]" using prems(5) by blast
    have **: "?P1 A [d←D. 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 [d←D. 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:
        "∀d∈set 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⟨∨≠: u⟩st ∈ set A'"
      hence "∀U⟨∨≠: u⟩st ∈ set A'' ∨
             (∃d ∈ set [d←D. 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⟨∨≠: F⟩st]" 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