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