Theory Stateful_Compositionality

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


section ‹Stateful Protocol Compositionality›

theory Stateful_Compositionality
imports Stateful_Typing Parallel_Compositionality Labeled_Stateful_Strands
begin
text‹\label{sec:Stateful-Compositionality}›

subsection ‹Small Lemmata›
lemma (in typed_model) wt_subst_sstp_vars_type_subset:
  fixes a::"('fun,'var) stateful_strand_step"
  assumes "wtsubst δ"
    and "t  subst_range δ. fv t = {}  (x. t = Var x)"
  shows "Γ ` Var ` fvsstp (a sstp δ)  Γ ` Var ` fvsstp a" (is ?A)
    and "Γ ` Var ` set (bvarssstp (a sstp δ)) = Γ ` Var ` set (bvarssstp a)" (is ?B)
    and "Γ ` Var ` varssstp (a sstp δ)  Γ ` Var ` varssstp a" (is ?C)
proof -
  show ?A
  proof
    fix τ assume τ: "τ  Γ ` Var ` fvsstp (a sstp δ)"
    then obtain x where x: "x  fvsstp (a sstp δ)" "Γ (Var x) = τ" by atomize_elim auto
  
    show "τ  Γ ` Var ` fvsstp a"
    proof (cases "x  fvsstp a")
      case False
      hence "y  fvsstp a. δ y = Var x"
      proof (cases a)
        case (NegChecks X F G)
        hence *: "x  fvpairs (F pairs rm_vars (set X) δ)  fvpairs (G pairs rm_vars (set X) δ)"
                 "x  set X"
          using fvsstp_NegCheck(1)[of X "F pairs rm_vars (set X) δ" "G pairs rm_vars (set X) δ"]
                fvsstp_NegCheck(1)[of X F G] False x(1)
          by fastforce+
  
        obtain y where y: "y  fvpairs F  fvpairs G" "x  fv (rm_vars (set X) δ y)"
          using fvpairs_subst_obtain_var[of _ _ "rm_vars (set X) δ"]
                fvpairs_subst_obtain_var[of _ _ "rm_vars (set X) δ"]
                *(1)
          by blast
  
        have "fv (rm_vars (set X) δ z) = {}  (u. rm_vars (set X) δ z = Var u)" for z
          using assms(2) rm_vars_img_subset[of "set X" δ] by blast
        hence "rm_vars (set X) δ y = Var x" using y(2) by fastforce
        hence "y  fvsstp a. rm_vars (set X) δ y = Var x"
          using y fvsstp_NegCheck(1)[of X F G] NegChecks *(2) by fastforce
        thus ?thesis by (metis (full_types) *(2) term.inject(1))
      qed (use assms(2) x(1) subst_apply_img_var'[of x _ δ] in fastforce)+
      then obtain y where y: "y  fvsstp a" "δ y = Var x" by atomize_elim auto
      hence "Γ (Var y) = τ" using x(2) assms(1) by (simp add: wtsubst_def)
      thus ?thesis using y(1) by auto
    qed (use x in auto)
  qed

  show ?B by (metis bvarssstp_subst)

  show ?C
  proof
    fix τ assume τ: "τ  Γ ` Var ` varssstp (a sstp δ)"
    then obtain x where x: "x  varssstp (a sstp δ)" "Γ (Var x) = τ" by atomize_elim auto
  
    show "τ  Γ ` Var ` varssstp a"
    proof (cases "x  varssstp a")
      case False
      hence "y  varssstp a. δ y = Var x"
      proof (cases a)
        case (NegChecks X F G)
        hence *: "x  fvpairs (F pairs rm_vars (set X) δ)  fvpairs (G pairs rm_vars (set X) δ)"
                 "x  set X"
          using varssstp_NegCheck[of X "F pairs rm_vars (set X) δ" "G pairs rm_vars (set X) δ"]
                varssstp_NegCheck[of X F G] False x(1)
          by (fastforce, blast)
  
        obtain y where y: "y  fvpairs F  fvpairs G" "x  fv (rm_vars (set X) δ y)"
          using fvpairs_subst_obtain_var[of _ _ "rm_vars (set X) δ"]
                fvpairs_subst_obtain_var[of _ _ "rm_vars (set X) δ"]
                *(1)
          by blast
  
        have "fv (rm_vars (set X) δ z) = {}  (u. rm_vars (set X) δ z = Var u)" for z
          using assms(2) rm_vars_img_subset[of "set X" δ] by blast
        hence "rm_vars (set X) δ y = Var x" using y(2) by fastforce
        hence "y  varssstp a. rm_vars (set X) δ y = Var x"
          using y varssstp_NegCheck[of X F G] NegChecks by blast
        thus ?thesis by (metis (full_types) *(2) term.inject(1))
      qed (use assms(2) x(1) subst_apply_img_var'[of x _ δ] in fastforce)+
      then obtain y where y: "y  varssstp a" "δ y = Var x" by atomize_elim auto
      hence "Γ (Var y) = τ" using x(2) assms(1) by (simp add: wtsubst_def)
      thus ?thesis using y(1) by auto
    qed (use x in auto)
  qed
qed

lemma (in typed_model) wt_subst_lsst_vars_type_subset:
  fixes A::"('fun,'var,'a) labeled_stateful_strand"
  assumes "wtsubst δ"
    and "t  subst_range δ. fv t = {}  (x. t = Var x)"
  shows "Γ ` Var ` fvlsst (A lsst δ)  Γ ` Var ` fvlsst A" (is ?A)
    and "Γ ` Var ` bvarslsst (A lsst δ) = Γ ` Var ` bvarslsst A" (is ?B)
    and "Γ ` Var ` varslsst (A lsst δ)  Γ ` Var ` varslsst A" (is ?C)
proof -
  have "varslsst (a#A lsst δ) = varssstp (b sstp δ)  varslsst (A lsst δ)"
       "varslsst (a#A) = varssstp b  varslsst A"
       "fvlsst (a#A lsst δ) = fvsstp (b sstp δ)  fvlsst (A lsst δ)"
       "fvlsst (a#A) = fvsstp b  fvlsst A"
       "bvarslsst (a#A lsst δ) = set (bvarssstp (b sstp δ))  bvarslsst (A lsst δ)"
       "bvarslsst (a#A) = set (bvarssstp b)  bvarslsst A"
    when "a = (l,b)" for a l b and A::"('fun,'var,'a) labeled_stateful_strand"
    using that unlabel_Cons(1)[of l b A] unlabel_subst[of "a#A" δ]
          subst_lsst_cons[of a A δ] subst_sst_cons[of b "unlabel A" δ]
          subst_apply_labeled_stateful_strand_step.simps(1)[of l b δ]
          varssst_unlabel_Cons[of l b A] varssst_unlabel_Cons[of l "b sstp δ" "A lsst δ"]
          fvsst_unlabel_Cons[of l b A] fvsst_unlabel_Cons[of l "b sstp δ" "A lsst δ"]
          bvarssst_unlabel_Cons[of l b A] bvarssst_unlabel_Cons[of l "b sstp δ" "A lsst δ"]
    by simp_all
  hence *: "Γ ` Var ` varslsst (a#A lsst δ) =
            Γ ` Var ` varssstp (b sstp δ)  Γ ` Var ` varslsst (A lsst δ)"
           "Γ ` Var ` varslsst (a#A) = Γ ` Var ` varssstp b  Γ ` Var ` varslsst A"
           "Γ ` Var ` fvlsst (a#A lsst δ) =
            Γ ` Var ` fvsstp (b sstp δ)  Γ ` Var ` fvlsst (A lsst δ)"
           "Γ ` Var ` fvlsst (a#A) = Γ ` Var ` fvsstp b  Γ ` Var ` fvlsst A"
           "Γ ` Var ` bvarslsst (a#A lsst δ) =
            Γ ` Var ` set (bvarssstp (b sstp δ))  Γ ` Var ` bvarslsst (A lsst δ)"
           "Γ ` Var ` bvarslsst (a#A) = Γ ` Var ` set (bvarssstp b)  Γ ` Var ` bvarslsst A"
    when "a = (l,b)" for a l b and A::"('fun,'var,'a) labeled_stateful_strand"
    using that by fast+

  have "?A  ?B  ?C"
  proof (induction A)
    case (Cons a A)
    obtain l b where a: "a = (l,b)" by (metis surj_pair)
  
    show ?case
      using Cons.IH wt_subst_sstp_vars_type_subset[OF assms, of b] *[OF a, of A]
      by (metis Un_mono)
  qed simp
  thus ?A ?B ?C by metis+
qed

lemma (in stateful_typed_model) fv_pair_fvpairs_subset:
  assumes "d  set D"
  shows "fv (pair (snd d))  fvpairs (unlabel D)"
using assms unfolding pair_def by (induct D) (auto simp add: unlabel_def)

lemma (in stateful_typed_model) labeled_sat_ineq_lift:
  assumes "M; map (λd. X⟨∨≠: [(pair (t,s), pair (snd d))]st) [ddbproj i D. d  set Di]d "
    (is "?R1 D")
  and "(j,p)  {(i,t,s)}  set D  set Di. (k,q)  {(i,t,s)}  set D  set Di.
          (δ. Unifier δ (pair p) (pair q))  j = k" (is "?R2 D")
  shows "M; map (λd. X⟨∨≠: [(pair (t,s), pair (snd d))]st) [dD. d  set Di]d "
using assms
proof (induction D)
  case (Cons dl D)
  obtain d l where dl: "dl = (l,d)" by (metis surj_pair)

  have 1: "?R1 D"
  proof (cases "i = l")
    case True thus ?thesis
      using Cons.prems(1) dl by (cases "dl  set Di") (auto simp add: dbproj_def)
  next
    case False thus ?thesis using Cons.prems(1) dl by (auto simp add: dbproj_def)
  qed

  have "set D  set (dl#D)" by auto
  hence 2: "?R2 D" using Cons.prems(2) by blast

  have "i  l  dl  set Di  M; [X⟨∨≠: [(pair (t,s), pair (snd dl))]st]d "
    using Cons.prems(1) dl by (auto simp add: ineq_model_def dbproj_def)
  moreover have "δ. Unifier δ (pair (t,s)) (pair d)  i = l"
    using Cons.prems(2) dl by force
  ultimately have 3: "dl  set Di  M; [X⟨∨≠: [(pair (t,s), pair (snd dl))]st]d "
    using strand_sem_not_unif_is_sat_ineq[of "pair (t,s)" "pair d"] dl by fastforce

  show ?case using Cons.IH[OF 1 2] 3 dl by auto
qed simp

lemma (in stateful_typed_model) labeled_sat_ineq_dbproj:
  assumes "M; map (λd. X⟨∨≠: [(pair (t,s), pair (snd d))]st) [dD. d  set Di]d "
    (is "?P D")
  shows "M; map (λd. X⟨∨≠: [(pair (t,s), pair (snd d))]st) [ddbproj i D. d  set Di]d "
    (is "?Q D")
using assms
proof (induction D)
  case (Cons di D)
  obtain d j where di: "di = (j,d)" by (metis surj_pair)

  have "?P D" using Cons.prems by (cases "di  set Di") auto
  hence IH: "?Q D" by (metis Cons.IH)

  show ?case using di IH
  proof (cases "i = j  di  set Di")
    case True
    have 1: "M; [X⟨∨≠: [(pair (t,s), pair (snd di))]st]d "
      using Cons.prems True by auto
    have 2: "dbproj i (di#D) = di#dbproj i D" using True dbproj_Cons(1) di by auto
    show ?thesis using 1 2 IH by auto
  qed (auto simp add: dbproj_def)
qed (simp add: dbproj_def)

lemma (in stateful_typed_model) labeled_sat_ineq_dbproj_sem_equiv:
  assumes "(j,p)  ((λ(t, s). (i, t, s)) ` set F')  set D.
           (k,q)  ((λ(t, s). (i, t, s)) ` set F')  set D.
            (δ. Unifier δ (pair p) (pair q))  j = k"
  and "fvpairs (map snd D)  set X = {}"
  shows "M; map (λG. X⟨∨≠: (F@G)st) (trpairs F' (map snd D))d  
         M; map (λG. X⟨∨≠: (F@G)st) (trpairs F' (map snd (dbproj i D)))d "
proof -
  let ?A = "set (map snd D) pset "
  let ?B = "set (map snd (dbproj i D)) pset "
  let ?C = "set (map snd D) - set (map snd (dbproj i D))"
  let ?F = "(λ(t, s). (i, t, s)) ` set F'"
  let ?P = "λδ. subst_domain δ = set X  ground (subst_range δ)"

  have 1: "(t, t')  set (map snd D). (fv t  fv t')  set X = {}"
          "(t, t')  set (map snd (dbproj i D)). (fv t  fv t')  set X = {}"
    using assms(2) dbproj_subset[of i D] unfolding unlabel_def by force+

  have 2: "?B  ?A" unfolding dbproj_def by auto

  have 3: "¬Unifier δ (pair f) (pair d)"
    when f: "f  set F'" and d: "d  set (map snd D) - set (map snd (dbproj i D))"
    for f d and δ::"('fun,'var) subst"
  proof -
    obtain k where k: "(k,d)  set D - set (dbproj i D)"
      using d by force
    
    have "(i,f)  ((λ(t, s). (i, t, s)) ` set F')  set D"
         "(k,d)  ((λ(t, s). (i, t, s)) ` set F')  set D"
      using f k by auto
    hence "i = k" when "Unifier δ (pair f) (pair d)" for δ
      using assms(1) that by blast
    moreover have "k  i" using k d unfolding dbproj_def by simp
    ultimately show ?thesis by metis
  qed

  have "f p δ  d p δ"
    when "f  set F'" "d  ?C" for f d and δ::"('fun,'var) subst"
    by (metis fun_pair_eq_subst 3[OF that])
  hence "f p (δ s )  ?C pset (δ s )"
    when "f  set F'" for f and δ::"('fun,'var) subst"
    using that by blast
  moreover have "?C pset δ pset  = ?C pset "
    when "?P δ" for δ
    using assms(2) that pairs_substI[of δ "(set (map snd D) - set (map snd (dbproj i D)))"]
    by blast
  ultimately have 4: "f p (δ s )  ?C pset "
    when "f  set F'" "?P δ" for f and δ::"('fun,'var) subst"
    by (metis that subst_pairs_compose)

  { fix f and δ::"('fun,'var) subst"
    assume "f  set F'" "?P δ"
    hence "f p (δ s )  ?C pset " by (metis 4)
    hence "f p (δ s )  ?A - ?B" by force
  } hence 5: "fset F'. δ. ?P δ  f p (δ s )  ?A - ?B" by metis

  show ?thesis
    using negchecks_model_db_subset[OF 2]
          negchecks_model_db_supset[OF 2 5]
          trpairs_sem_equiv[OF 1(1)]
          trpairs_sem_equiv[OF 1(2)]
          tr_NegChecks_constr_iff(1)
          strand_sem_eq_defs(2)
    by (metis (no_types, lifting))
qed

lemma (in stateful_typed_model) labeled_sat_eqs_list_all:
  assumes "(j, p)  {(i,t,s)}  set D. (k,q)  {(i,t,s)}  set D.
              (δ. Unifier δ (pair p) (pair q))  j = k" (is "?P D")
  and "M; map (λd. ac: (pair (t,s))  (pair (snd d))st) Dd " (is "?Q D")
  shows "list_all (λd. fst d = i) D"
using assms
proof (induction D rule: List.rev_induct)
  case (snoc di D)
  obtain d j where di: "di = (j,d)" by (metis surj_pair)
  have "pair (t,s)   = pair d  " using di snoc.prems(2) by auto
  hence "δ. Unifier δ (pair (t,s)) (pair d)" by auto
  hence 1: "i = j" using snoc.prems(1) di by fastforce
  
  have "set D  set (D@[di])" by auto
  hence 2: "?P D" using snoc.prems(1) by blast

  have 3: "?Q D" using snoc.prems(2) by auto
  
  show ?case using di 1 snoc.IH[OF 2 3] by simp
qed simp

lemma (in stateful_typed_model) labeled_sat_eqs_subseqs:
  assumes "Di  set (subseqs D)"
  and "(j, p)  {(i,t,s)}  set D. (k, q)  {(i,t,s)}  set D.
          (δ. Unifier δ (pair p) (pair q))  j = k" (is "?P D")
  and "M; map (λd. ac: (pair (t,s))  (pair (snd d))st) Did "
  shows "Di  set (subseqs (dbproj i D))"
proof -
  have "set Di  set D" by (rule subseqs_subset[OF assms(1)])
  hence "?P Di" using assms(2) by blast
  thus ?thesis using labeled_sat_eqs_list_all[OF _ assms(3)] subseqs_mem_dbproj[OF assms(1)] by simp
qed

lemma (in stateful_typing_result) duallsst_tfrsstp:
  assumes "list_all tfrsstp (unlabel S)"
  shows "list_all tfrsstp (unlabel (duallsst S))"
using assms
proof (induction S)
  case (Cons a S)
  have prems: "tfrsstp (snd a)" "list_all tfrsstp (unlabel S)"
    using Cons.prems unlabel_Cons(2)[of a S] by simp_all
  hence IH: "list_all tfrsstp (unlabel (duallsst S))" by (metis Cons.IH)

  obtain l b where a: "a = (l,b)" by (metis surj_pair)
  with Cons show ?case
  proof (cases b)
    case (Equality c t t')
    hence "duallsst (a#S) = a#duallsst S" by (metis duallsst_Cons(3) a)
    thus ?thesis using a IH prems by fastforce
  next
    case (NegChecks X F G)
    hence "duallsst (a#S) = a#duallsst S" by (metis duallsst_Cons(7) a)
    thus ?thesis using a IH prems by fastforce
  qed auto
qed simp

lemma (in stateful_typed_model) setopssst_unlabel_duallsst_eq:
  "setopssst (unlabel (duallsst A)) = setopssst (unlabel A)"
proof (induction A)
  case (Cons a A)
  obtain l b where a: "a = (l,b)" by (metis surj_pair)
  thus ?case using Cons.IH by (cases b) (simp_all add: setopssst_def)
qed simp


subsection ‹Locale Setup and Definitions›
locale labeled_stateful_typed_model =
  stateful_typed_model arity public Ana Γ Pair
+ labeled_typed_model arity public Ana Γ label_witness1 label_witness2
  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"
  and label_witness1::"'lbl"
  and label_witness2::"'lbl"
begin

definition lpair where
  "lpair lp  case lp of (i,p)  (i,pair p)"

lemma setopslsstp_pair_image[simp]:
  "lpair ` (setopslsstp (i,send⟨ts)) = {}"
  "lpair ` (setopslsstp (i,receive⟨ts)) = {}"
  "lpair ` (setopslsstp (i,ac: t  t')) = {}"
  "lpair ` (setopslsstp (i,insert⟨t,s)) = {(i, pair (t,s))}"
  "lpair ` (setopslsstp (i,delete⟨t,s)) = {(i, pair (t,s))}"
  "lpair ` (setopslsstp (i,ac: t  s)) = {(i, pair (t,s))}"
  "lpair ` (setopslsstp (i,X⟨∨≠: F ∨∉: F')) = ((λ(t,s). (i, pair (t,s))) ` set F')"
unfolding lpair_def by force+

definition par_complsst where
  "par_complsst (𝒜::('fun,'var,'lbl) labeled_stateful_strand) (Secrets::('fun,'var) terms)  
    (l1 l2. l1  l2 
              GSMP_disjoint (trmssst (proj_unl l1 𝒜)  pair ` setopssst (proj_unl l1 𝒜))
                            (trmssst (proj_unl l2 𝒜)  pair ` setopssst (proj_unl l2 𝒜)) Secrets) 
    (s  Secrets. ¬{} c s)  ground Secrets 
    ((i,p)  setopslsst 𝒜. (j,q)  setopslsst 𝒜.
      (δ. Unifier δ (pair p) (pair q))  i = j)"

definition declassifiedlsst where
  "declassifiedlsst 𝒜   {s. {set ts | ts. ⟨⋆, receive⟨ts  set (𝒜 lsst )}  s}"

definition strand_leakslsst ("_ leaks _ under _") where
  "(𝒜::('fun,'var,'lbl) labeled_stateful_strand) leaks Secrets under  
    (t  Secrets - declassifiedlsst 𝒜 . n.  s (proj_unl n 𝒜@[send⟨[t]]))"

type_synonym ('a,'b,'c) labeleddbstate = "('c strand_label × (('a,'b) term × ('a,'b) term)) set"
type_synonym ('a,'b,'c) labeleddbstatelist = "('c strand_label × (('a,'b) term × ('a,'b) term)) list"

definition typing_condsst where
  "typing_condsst 𝒜  wfsst 𝒜  wftrms (trmssst 𝒜)  tfrsst 𝒜"

text ‹
  For proving the compositionality theorem for stateful constraints the idea is to first define a
  variant of the reduction technique that was used to establish the stateful typing result. This
  variant performs database-state projections, and it allows us to reduce the compositionality
  problem for stateful constraints to ordinary constraints.
›
fun trpc::
  "('fun,'var,'lbl) labeled_stateful_strand  ('fun,'var,'lbl) labeleddbstatelist
    ('fun,'var,'lbl) labeled_strand list"
where
  "trpc [] D = [[]]"
| "trpc ((i,send⟨ts)#A) D = map ((#) (i,send⟨tsst)) (trpc A D)"
| "trpc ((i,receive⟨ts)#A) D = map ((#) (i,receive⟨tsst)) (trpc A D)"
| "trpc ((i,ac: t  t')#A) D = map ((#) (i,ac: t  t'st)) (trpc A D)"
| "trpc ((i,insert⟨t,s)#A) D = trpc A (List.insert (i,(t,s)) D)"
| "trpc ((i,delete⟨t,s)#A) D = (
    concat (map (λDi. map (λB. (map (λd. (i,check: (pair (t,s))  (pair (snd d))st)) Di)@
                               (map (λd. (i,[]⟨∨≠: [(pair (t,s), pair (snd d))]st))
                                    [ddbproj i D. d  set Di])@B)
                          (trpc A [dD. d  set Di]))
                (subseqs (dbproj i D))))"
| "trpc ((i,ac: t  s)#A) D =
    concat (map (λB. map (λd. (i,ac: (pair (t,s))  (pair (snd d))st)#B) (dbproj i D)) (trpc A D))"
| "trpc ((i,X⟨∨≠: F ∨∉: F' )#A) D =
    map ((@) (map (λG. (i,X⟨∨≠: (F@G)st)) (trpairs F' (map snd (dbproj i D))))) (trpc A D)"

end

locale labeled_stateful_typing =
  labeled_stateful_typed_model arity public Ana Γ Pair label_witness1 label_witness2
+ stateful_typing_result arity public Ana Γ Pair
  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"
  and label_witness1::"'lbl"
  and label_witness2::"'lbl"
begin

sublocale labeled_typing
by unfold_locales

end


subsection ‹Small Lemmata›
context labeled_stateful_typed_model
begin

lemma declassifiedlsst_alt_def:
  "declassifiedlsst 𝒜  = {s. {set ts | ts. ⟨⋆, receive⟨ts  set 𝒜} set   s}"
proof -
  have 0: "(l, receive⟨ts)  set (𝒜 lsst ) = (ts'. (l, receive⟨ts')  set 𝒜  ts = ts' list )"
    (is "?A 𝒜 = ?B 𝒜")
    for ts l
  proof
    show "?A 𝒜  ?B 𝒜"
    proof (induction 𝒜)
      case (Cons a 𝒜)
      obtain k b where a: "a = (k,b)" by (metis surj_pair)
      show ?case
      proof (cases "?A 𝒜")
        case False
        hence "(l,receive⟨ts) = a lsstp " using Cons.prems subst_lsst_cons[of a 𝒜 ] by auto
        thus ?thesis unfolding a by (cases b) auto
      qed (use Cons.IH in auto)
    qed simp

    show "?B 𝒜  ?A 𝒜"
    proof (induction 𝒜)
      case (Cons a 𝒜)
      obtain k b where a: "a = (k,b)" by (metis surj_pair)
      show ?case
      proof (cases "?B 𝒜")
        case False
        hence "ts'. a = (l, receive⟨ts')  ts = ts' list " using Cons.prems by auto
        thus ?thesis using subst_lsst_cons[of a 𝒜 ] unfolding a by (cases b) auto
      qed (use Cons.IH subst_lsst_cons[of a 𝒜 ] in auto)
    qed simp
  qed

  let ?M = "λA. {set ts |ts. ⟨⋆, receive⟨ts  set A}"

  have 1: "?M (𝒜 lsst ) = ?M 𝒜 set " (is "?A = ?B")
  proof
    show "?A  ?B"
    proof
      fix t assume t: "t  ?A"
      then obtain ts where ts: "t  set ts" "⟨⋆, receive⟨ts  set (𝒜 lsst )" by blast
      thus "t  ?B" using 0[of  ts] by fastforce
    qed
    show "?B  ?A"
    proof
      fix t assume t: "t  ?B"
      then obtain ts where ts: "t  set ts set " "⟨⋆, receive⟨ts  set 𝒜" by blast
      hence "⟨⋆, receive⟨ts list   set (𝒜 lsst )" using 0[of  "ts list "] by blast
      thus "t  ?A" using ts(1) by force
    qed
  qed

  show ?thesis using 1 unfolding declassifiedlsst_def by argo
qed

lemma declassifiedlsst_prefix_subset:
  assumes AB: "prefix A B"
  shows "declassifiedlsst A I  declassifiedlsst B I"
proof
  fix t assume t: "t  declassifiedlsst A I"
  obtain C where C: "B = A@C" using prefixE[OF AB] by metis
  show "t  declassifiedlsst B I"
    using t ideduct_mono[of
              "{set ts |ts. (, receive⟨ts)  set A} set I" t 
              "{set ts |ts. (, receive⟨ts)  set B} set I"]
    unfolding C declassifiedlsst_alt_def by auto
qed

lemma declassifiedlsst_star_receive_supset:
  "{t | t ts. ⟨⋆, receive⟨ts  set 𝒜  t  set ts} set   declassifiedlsst 𝒜 "
unfolding declassifiedlsst_alt_def by (fastforce intro: intruder_deduct.Axiom)

lemma declassifiedlsst_proj_eq:
  "declassifiedlsst A I = declassifiedlsst (proj n A) I"
using proj_mem_iff(2)[of _ A] unfolding declassifiedlsst_alt_def by simp

lemma par_complsst_nil:
  assumes "ground Sec" "s  Sec. s'subterms s. {} c s'  s'  Sec" "s  Sec. ¬{} c s"
  shows "par_complsst [] Sec"
using assms unfolding par_complsst_def by simp

lemma par_complsst_subset:
  assumes A: "par_complsst A Sec"
    and BA: "set B  set A"
  shows "par_complsst B Sec"
proof -
  let ?L = "λn A. trmssst (proj_unl n A)  pair ` setopssst (proj_unl n A)"

  have "?L n B  ?L n A" for n
    using trmssst_mono[OF proj_set_mono(2)[OF BA]] setopssst_mono[OF proj_set_mono(2)[OF BA]]
    by blast
  hence "GSMP_disjoint (?L m B) (?L n B) Sec" when nm: "m  n" for n m::'lbl
    using GSMP_disjoint_subset[of "?L m A" "?L n A" Sec "?L m B" "?L n B"] A nm
    unfolding par_complsst_def by simp
  thus "par_complsst B Sec"
    using A setopslsst_mono[OF BA]
    unfolding par_complsst_def by blast
qed

lemma par_complsst_split:
  assumes "par_complsst (A@B) Sec"
  shows "par_complsst A Sec" "par_complsst B Sec"
using par_complsst_subset[OF assms] by simp_all

lemma par_complsst_proj:
  assumes "par_complsst A Sec"
  shows "par_complsst (proj n A) Sec"
using par_complsst_subset[OF assms] by simp

lemma par_complsst_duallsst:
  assumes A: "par_complsst A S"
  shows "par_complsst (duallsst A) S"
proof (unfold par_complsst_def case_prod_unfold; intro conjI)
  show "ground S" "s  S. ¬{} c s"
    using A unfolding par_complsst_def by fast+

  let ?M = "λl B. (trmslsst (proj l B)  pair ` setopssst (proj_unl l B))"
  let ?P = "λB. l1 l2. l1  l2  GSMP_disjoint (?M l1 B) (?M l2 B) S"
  let ?Q = "λB. p  setopslsst B. q  setopslsst B.
    (δ. Unifier δ (pair (snd p)) (pair (snd q)))  fst p = fst q"

  have "?P A" "?Q A" using A unfolding par_complsst_def case_prod_unfold by blast+
  thus "?P (duallsst A)" "?Q (duallsst A)"
    by (metis setopssst_unlabel_duallsst_eq trmssst_unlabel_duallsst_eq proj_duallsst,
        metis setopslsst_duallsst_eq)
qed

lemma par_complsst_subst:
  assumes A: "par_complsst A S"
    and δ: "wtsubst δ" "wftrms (subst_range δ)" "subst_domain δ  bvarslsst A = {}"
  shows "par_complsst (A lsst δ) S"
proof (unfold par_complsst_def case_prod_unfold; intro conjI)
  show "ground S" "s  S. ¬{} c s"
    using A unfolding par_complsst_def by fast+

  let ?N = "λl B. trmslsst (proj l B)  pair ` setopssst (proj_unl l B)"
  define M where "M  λl (B::('fun,'var,'lbl) labeled_stateful_strand). ?N l B"
  let ?P = "λp q. δ. Unifier δ (pair (snd p)) (pair (snd q))"
  let ?Q = "λB. p  setopslsst B. q  setopslsst B. ?P p q  fst p = fst q"
  let ?R = "λB. l1 l2. l1  l2  GSMP_disjoint (?N l1 B) (?N l2 B) S"

  have d: "bvarslsst (proj l A)  subst_domain δ = {}" for l
    using δ(3) unfolding proj_def bvarssst_def unlabel_def by auto

  have "GSMP_disjoint (M l1 A) (M l2 A) S" when l: "l1  l2" for l1 l2
    using l A unfolding par_complsst_def M_def by presburger
  moreover have "M l (A lsst δ) = (M l A) set δ" for l
    using fun_pair_subst_set[of δ "setopssst (proj_unl l A)", symmetric]
          trmssst_subst[OF d[of l]] setopssst_subst[OF d[of l]] proj_subst[of l A δ]
    unfolding M_def unlabel_subst by auto
  ultimately have "GSMP_disjoint (M l1 (A lsst δ)) (M l2 (A lsst δ)) S" when l: "l1  l2" for l1 l2
    using l GSMP_wt_subst_subset[OF _ δ(1,2), of _ "M l1 A"]
          GSMP_wt_subst_subset[OF _ δ(1,2), of _ "M l2 A"]
    unfolding GSMP_disjoint_def by fastforce
  thus "?R (A lsst δ)" unfolding M_def by blast

  have "?Q A" using A unfolding par_complsst_def by force 
  thus "?Q (A lsst δ)" using δ(3)
  proof (induction A)
    case (Cons a A)
    obtain l b where a: "a = (l,b)" by (metis surj_pair)

    have 0: "bvarslsst (a#A) = set (bvarssstp (snd a))  bvarslsst A"
      unfolding bvarssst_def unlabel_def by simp

    have "?Q A" "subst_domain δ  bvarslsst A = {}"
      using Cons.prems 0 unfolding setopslsst_def by auto
    hence IH: "?Q (A lsst δ)" using Cons.IH unfolding setopslsst_def by blast
    
    have 1: "fst p = fst q"
      when p: "p  setopslsstp (a lsstp δ)"
        and q: "q  setopslsstp (a lsstp δ)"
        and pq: "?P p q"
      for p q
      using a p q pq by (cases b) auto

    have 2: "fst p = fst q"
      when p: "p  setopslsst (A lsst δ)"
        and q: "q  setopslsstp (a lsstp δ)"
        and pq: "?P p q"
      for p q
    proof -
      obtain p' X where p':
          "p'  setopslsst A" "fst p = fst p'" 
          "X  bvarslsst (a#A)" "snd p = snd p' p rm_vars X δ"
        using setopslsst_in_subst[OF p] 0 by blast

      obtain q' Y where q':
          "q'  setopslsstp a" "fst q = fst q'" 
          "Y  bvarslsst (a#A)" "snd q = snd q' p rm_vars Y δ"
        using setopslsstp_in_subst[OF q] 0 by blast

      have "pair (snd p) = pair (snd p')  δ"
           "pair (snd q) = pair (snd q')  δ"
        using fun_pair_subst[of "snd p'" "rm_vars X δ"] fun_pair_subst[of "snd q'" "rm_vars Y δ"]
              p'(3,4) q'(3,4) Cons.prems(2) rm_vars_apply'[of δ X] rm_vars_apply'[of δ Y]
        by fastforce+
      hence "δ. Unifier δ (pair (snd p')) (pair (snd q'))"
        using pq Unifier_comp' by metis
      thus ?thesis using Cons.prems p'(1,2) q'(1,2) by simp
    qed

    show ?case by (metis 1 2 IH Un_iff setopslsst_cons subst_lsst_cons)
  qed simp
qed

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

lemma wf_pair_eqs_ineqs_map':
  fixes A::"('fun,'var,'lbl) labeled_strand"
  assumes "wfst X (unlabel A)"
          "Di  set (subseqs (dbproj i D))"
          "fvpairs (unlabel D)  X"
  shows "wfst X (unlabel (
            (map (λd. (i,check: (pair (t,s))  (pair (snd d))st)) Di)@
            (map (λd. (i,[]⟨∨≠: [(pair (t,s), pair (snd d))]st)) [ddbproj i D. d  set Di])@A))"
proof -
  let ?f = "[ddbproj i D. d  set Di]"
  define c1 where c1: "c1 = map (λd. (i,check: (pair (t,s))  (pair (snd d))st)) Di"
  define c2 where c2: "c2 = map (λd. (i,[]⟨∨≠: [(pair (t,s), pair (snd d))]st)) ?f"
  define c3 where c3: "c3 = map (λd. check: (pair (t,s))  (pair d)st) (unlabel Di)"
  define c4 where c4: "c4 = map (λd. []⟨∨≠: [(pair (t,s), pair d)]st) (unlabel ?f)"
  have ci_eqs: "c3 = unlabel c1" "c4 = unlabel c2" unfolding c1 c2 c3 c4 unlabel_def by auto
  have 1: "wfst X (unlabel (c2@A))"
    using wf_fun_pair_ineqs_map[OF assms(1)] ci_eqs(2) unlabel_append[of c2 A] c4
    by metis
  have 2: "fvpairs (unlabel Di)  X" 
    using assms(3) subseqs_set_subset(1)[OF assms(2)]
    unfolding unlabel_def dbproj_def
    by fastforce
  { fix B::"('fun,'var) strand" assume "wfst X B"
    hence "wfst X (unlabel c1@B)" using 2 unfolding c1 unlabel_def by (induct Di) auto
  } thus ?thesis using 1 unfolding c1 c2 unlabel_def by simp
qed

lemma trmssst_setopssst_wt_instance_ex:
  defines "M  λA. trmslsst A  pair ` setopssst (unlabel A)"
  assumes B: "b  set B. a  set A. δ. b = a lsstp δ  wtsubst δ  wftrms (subst_range δ)"
  shows "t  M B. s  M A. δ. t = s  δ  wtsubst δ  wftrms (subst_range δ)"
proof
  let ?P = "λδ. wtsubst δ  wftrms (subst_range δ)"

  fix t assume "t  M B"
  then obtain b where b: "b  set B" "t  trmssstp (snd b)  pair ` setopssstp (snd b)"
    unfolding M_def unfolding unlabel_def trmssst_def setopssst_def by auto
  then obtain a δ where a: "a  set A" "b = a lsstp δ" and δ: "wtsubst δ" "wftrms (subst_range δ)"
    using B by meson

  note δ' = wt_subst_rm_vars[OF δ(1)] wf_trms_subst_rm_vars'[OF δ(2)]

  have "t  M (A lsst δ)"
    using b(2) a
    unfolding M_def subst_apply_labeled_stateful_strand_def unlabel_def trmssst_def setopssst_def
    by auto
  moreover have "s  M A. δ. t = s  δ  ?P δ" when "t  trmslsst (A lsst δ)"
    using trmssst_unlabel_subst'[OF that] δ' unfolding M_def by blast
  moreover have "s  M A. δ. t = s  δ  ?P δ" when t: "t  pair ` setopssst (unlabel A sst δ)"
  proof -
    obtain p where p: "p  setopssst (unlabel A sst δ)" "t = pair p" using t by blast
    then obtain q X where q: "q  setopssst (unlabel A)" "p = q p rm_vars (set X) δ"
      using setopssst_subst'[OF p(1)] by blast
    hence "t = pair q  rm_vars (set X) δ"
      using fun_pair_subst[of q "rm_vars (set X) δ"] p(2) by presburger
    thus ?thesis using δ'[of "set X"] q(1) unfolding M_def by blast
  qed
  ultimately show "s  M A. δ. t = s  δ  ?P δ" unfolding M_def unlabel_subst by fast
qed

lemma setopslsst_wt_instance_ex:
  assumes B: "b  set B. a  set A. δ. b = a lsstp δ  wtsubst δ  wftrms (subst_range δ)"
  shows "p  setopslsst B. q  setopslsst A. δ.
    fst p = fst q  snd p = snd q p δ  wtsubst δ  wftrms (subst_range δ)"
proof
  let ?P = "λδ. wtsubst δ  wftrms (subst_range δ)"

  fix p assume "p  setopslsst B"
  then obtain b where b: "b  set B" "p  setopslsstp b" unfolding setopslsst_def by blast
  then obtain a δ where a: "a  set A" "b = a lsstp δ" and δ: "wtsubst δ" "wftrms (subst_range δ)"
    using B by meson
  hence p: "p  setopslsst (A lsst δ)"
    using b(2) unfolding setopslsst_def subst_apply_labeled_stateful_strand_def by auto
  
  obtain X q where q:
      "q  setopslsst A" "fst p = fst q" "snd p = snd q p rm_vars X δ"
    using setopslsst_in_subst[OF p] by blast

  show "q  setopslsst A. δ. fst p = fst q  snd p = snd q p δ  ?P δ"
    using q wt_subst_rm_vars[OF δ(1)] wf_trms_subst_rm_vars'[OF δ(2)] by blast
qed

lemma deduct_proj_priv_term_prefix_ex_stateful:
  assumes A: "iksst (proj_unl l A) set I  t"
    and t: "¬{} c t"
  shows "B k s. (k =   k = ln l)  prefix (B@[(k,receive⟨s)]) A 
                 declassifiedlsst ((B@[(k,receive⟨s)])) I = declassifiedlsst A I 
                 iksst (proj_unl l (B@[(k,receive⟨s)])) = iksst (proj_unl l A)"
using A
proof (induction A rule: List.rev_induct)
  case Nil
  have "iksst (proj_unl l []) set I = {}" by auto
  thus ?case using Nil t deducts_eq_if_empty_ik[of t] by argo
next
  case (snoc a A)
  obtain k b where a: "a = (k,b)" by (metis surj_pair)
  let ?P = "k =   k = (ln l)"
  let ?Q = "s. b = receive⟨s"

  have 0: "iksst (proj_unl l (A@[a])) = iksst (proj_unl l A)" when "?P  ¬?Q"
    using that iksst_snoc_no_receive_eq[OF that, of I "proj_unl l A"]
    unfolding iksst_def a by (cases "k =   k = (ln l)") auto

  have 1: "declassifiedlsst (A@[a]) I = declassifiedlsst A I" when "?P  ¬?Q"
    using that snoc.prems unfolding declassifiedlsst_alt_def a
    by (metis (no_types, lifting) UnCI UnE empty_iff insert_iff list.set prod.inject set_append)

  note 2 = snoc.prems snoc.IH 0 1

  show ?case
  proof (cases ?P)
    case True
    note T = this
    thus ?thesis
    proof (cases ?Q)
      case True thus ?thesis using T unfolding a by blast
    qed (use 2 in auto)
  qed (use 2 in auto)
qed

lemma constr_sem_stateful_proj_priv_term_prefix_obtain:
  assumes 𝒜': "prefix 𝒜' 𝒜" "constr_sem_stateful τ (proj_unl n 𝒜'@[send⟨[t]])"
    and t: "t  Sec - declassifiedlsst 𝒜' τ" "¬{} c t" "t  τ = t"
  obtains B k' s where
    "k' =   k' = ln n" "prefix B 𝒜'" "suffix [(k', receive⟨s)] B"
    "declassifiedlsst B τ = declassifiedlsst 𝒜' τ"
    "iklsst (proj n B) = iklsst (proj n 𝒜')"
    "constr_sem_stateful τ (proj_unl n B@[send⟨[t]])"
    "prefix (proj n B) (proj n 𝒜)" "suffix [(k', receive⟨s)] (proj n B)"
    "t  Sec - declassifiedlsst (proj n B) τ"
proof -
  have "iklsst (proj n 𝒜') set τ  t"
    using 𝒜'(2) t(3) strand_sem_append_stateful[of "{}" "{}" "proj_unl n 𝒜'" "[send⟨[t]]" τ]
    by simp
  then obtain B k' s where B:
      "k' =   k' = ln n" "prefix B 𝒜'" "suffix [(k', receive⟨s)] B"
      "declassifiedlsst B τ = declassifiedlsst 𝒜' τ"
      "iklsst (proj n B) = iklsst (proj n 𝒜')"
    using deduct_proj_priv_term_prefix_ex_stateful[OF _ t(2), of τ n 𝒜']
    unfolding suffix_def by blast

  have B': "constr_sem_stateful τ (proj_unl n B@[send⟨[t]])"
    using B(5) 𝒜'(2) strand_sem_append_stateful[of "{}" "{}" "proj_unl n 𝒜'" "[send⟨[t]]" τ]
          strand_sem_append_stateful[of "{}" "{}" "proj_unl n B" _ τ]
          prefix_proj(2)[OF B(2), of n]
    by (metis (no_types, lifting) append_Nil2 prefix_def strand_sem_stateful.simps(2))

  have B'': "prefix (proj n B) (proj n 𝒜)" "suffix [(k', receive⟨s)] (proj n B)"
            "t  Sec - declassifiedlsst (proj n B) τ"
    using 𝒜' t B(1-4) declassifiedlsst_proj_eq[of B τ n]
    unfolding suffix_def prefix_def proj_def by auto

  show ?thesis by (rule that[OF B B' B''])
qed

lemma constr_sem_stateful_star_proj_no_leakage:
  fixes Sec P lbls k
  defines "no_leakage  λ𝒜. τ  s.
      prefix  𝒜  s  Sec - declassifiedlsst  τ  τ s (unlabel @[send⟨[s]])"
  assumes Sec: "ground Sec"
    and 𝒜: "(l,a)  set 𝒜. l = "
  shows "no_leakage 𝒜"
proof (rule ccontr)
  assume "¬no_leakage 𝒜"
  then obtain I B s where B:
      "prefix B 𝒜" "s  Sec - declassifiedlsst B I" "I s (unlabel B@[send⟨[s]])"
    unfolding no_leakage_def by blast

  have 1: "¬({set ts | ts. ⟨⋆, receive⟨ts  set (B lsst I)}  s)"
    using B(2) unfolding declassifiedlsst_def by fast

  have 2: "iklsst (B lsst I)  s"
    using B(2,3) Sec strand_sem_append_stateful[of "{}" "{}" "unlabel B" "[send⟨[s]]" I]
          subst_apply_term_ident[of s I] unlabel_subst[of B] iksst_subst[of "unlabel B"]
    by force

  have "l = " when "(l,c)  set B" for l c
    using that 𝒜 B(1) set_mono_prefix by blast
  hence "l = " when "(l,c)  set (B lsst I)" for l c
    using that unfolding subst_apply_labeled_stateful_strand_def by auto
  hence 3: "iklsst (B lsst I) = ({set ts | ts. ⟨⋆, receive⟨ts  set (B lsst I)})"
    using in_iklsst_iff[of _ "B lsst I"] unfolding iksst_def unlabel_def by auto

  show False using 1 2 3 by force
qed

end

subsection ‹Lemmata: Properties of the Constraint Translation Function›
context labeled_stateful_typed_model
begin

lemma tr_par_labeled_rcv_iff:
  "B  set (trpc A D)  (i, receive⟨tst)  set B  (i, receive⟨t)  set A"
by (induct A D arbitrary: B rule: trpc.induct) auto

lemma tr_par_declassified_eq:
  "B  set (trpc A D)  declassifiedlst B I = declassifiedlsst A I"
using tr_par_labeled_rcv_iff unfolding declassifiedlst_alt_def declassifiedlsst_alt_def by simp

lemma tr_par_ik_eq:
  assumes "B  set (trpc A D)"
  shows "ikst (unlabel B) = iksst (unlabel A)"
proof -
  have "{t. i. (i, receive⟨tst)  set B} = {t. i. (i, receive⟨t)  set A}"
    using tr_par_labeled_rcv_iff[OF assms] by simp
  moreover have
      "C. {t. i. (i, receive⟨tst)  set C} = {t. receive⟨tst  set (unlabel C)}"
      "C. {t. i. (i, receive⟨t)  set C} = {t. receive⟨t  set (unlabel C)}"
    unfolding unlabel_def by force+
  ultimately show ?thesis unfolding iksst_def ikst_is_rcv_set by fast
qed

lemma tr_par_deduct_iff:
  assumes "B  set (trpc A D)"
  shows "ikst (unlabel B) set I  t  iksst (unlabel A) set I  t"
using tr_par_ik_eq[OF assms] by metis

lemma tr_par_vars_subset:
  assumes "A'  set (trpc A D)"
  shows "fvlst A'  fvsst (unlabel A)  fvpairs (unlabel D)" (is ?P)
  and "bvarslst A'  bvarssst (unlabel A)" (is ?Q)
proof -
  show ?P using assms
  proof (induction "unlabel A" arbitrary: A A' D rule: strand_sem_stateful_induct)
    case (ConsIn A' D ac t s AA A A')
    then obtain i B where iB: "A = (i,ac: t  s)#B" "AA = unlabel B"
      unfolding unlabel_def by atomize_elim auto
    then obtain A'' d where *:
        "d  set (dbproj i D)"
        "A' = (i,ac: (pair (t,s))  (pair (snd d))st)#A''"
        "A''  set (trpc B D)"
      using ConsIn.prems(1) by atomize_elim force
    hence "fvlst A''  fvsst (unlabel B)  fvpairs (unlabel D)"
          "fv (pair (snd d))  fvpairs (unlabel D)"
      apply (metis ConsIn.hyps(1)[OF iB(2)])
      using fvpairs_mono[OF dbproj_subset[of i D]]
            fv_pair_fvpairs_subset[OF *(1)]
      by blast
    thus ?case using * iB unfolding pair_def by auto
  next
    case (ConsDel A' D t s AA A A')
    then obtain i B where iB: "A = (i,delete⟨t,s)#B" "AA = unlabel B"
      unfolding unlabel_def by atomize_elim auto

    define fltD1 where "fltD1 = (λDi. filter (λd. d  set Di) D)"
    define fltD2 where "fltD2 = (λDi. filter (λd. d  set Di) (dbproj i D))"
    define constr where "constr =
      (λDi. (map (λd. (i, check: (pair (t,s))  (pair (snd d))st)) Di)@
            (map (λd. (i, []⟨∨≠: [(pair (t,s), pair (snd d))]st)) (fltD2 Di)))"

    from iB obtain A'' Di where *:
        "Di  set (subseqs (dbproj i D))" "A' = (constr Di)@A''" "A''  set (trpc B (fltD1 Di))"
      using ConsDel.prems(1) unfolding constr_def fltD1_def fltD2_def by atomize_elim auto
    hence "fvlst A''  fvsst AA  fvpairs (unlabel (fltD1 Di))"
      unfolding constr_def fltD1_def by (metis ConsDel.hyps(1) iB(2))
    hence 1: "fvlst A''  fvsst AA  fvpairs (unlabel D)"
      using fvpairs_mono[of "unlabel (fltD1 Di)" "unlabel D"]
      unfolding unlabel_def fltD1_def by force
    
    have 2: "fvpairs (unlabel Di)  fvpairs (unlabel (fltD1 Di))  fvpairs (unlabel D)"
      using subseqs_set_subset(1)[OF *(1)]
      unfolding fltD1_def unlabel_def dbproj_def
      by auto

    have 5: "fvlst A' = fvlst (constr Di)  fvlst A''" using * unfolding unlabel_def by force

    have "fvlst (constr Di)  fv t  fv s  fvpairs (unlabel Di)  fvpairs (unlabel (fltD1 Di))"
      unfolding unlabel_def constr_def fltD1_def fltD2_def pair_def dbproj_def by auto
    hence 3: "fvlst (constr Di)  fv t  fv s  fvpairs (unlabel D)" using 2 by blast

    have 4: "fvsst (unlabel A) = fv t  fv s  fvsst AA" using iB by auto
    
    have "fvst (unlabel A')  fvsst (unlabel A)  fvpairs (unlabel D)" using 1 3 4 5 by blast
    thus ?case by metis
  next
    case (ConsNegChecks A' D X F F' AA A A')
    then obtain i B where iB: "A = (i,NegChecks X F F')#B" "AA = unlabel B"
      unfolding unlabel_def by atomize_elim auto

    define D' where "D'  (fvpairs ` set (trpairs F' (unlabel (dbproj i D))))"
    define constr where "constr = map (λG. (i,X⟨∨≠: (F@G)st)) (trpairs F' (map snd (dbproj i D)))"

    from iB obtain A'' where *: "A''  set (trpc B D)" "A' = constr@A''"
      using ConsNegChecks.prems(1) unfolding constr_def by atomize_elim auto
    hence "fvlst A''  fvsst AA  fvpairs (unlabel D)"
      by (metis ConsNegChecks.hyps(1) iB(2))
    hence **: "fvlst A''  fvsst AA  fvpairs (unlabel D)" by auto

    have 1: "fvlst constr  (D'  fvpairs F) - set X"
      unfolding D'_def constr_def unlabel_def by auto

    have "set (unlabel (dbproj i D))  set (unlabel D)" unfolding unlabel_def dbproj_def by auto
    hence 2: "D'  fvpairs F'  fvpairs (unlabel D)"
      using trpairs_vars_subset'[of F' "unlabel (dbproj i D)"] fvpairs_mono
      unfolding D'_def by blast

    have 3: "fvlst A'  ((fvpairs F'  fvpairs F) - set X)  fvpairs (unlabel D)  fvlst A''"
      using 1 2 *(2) unfolding unlabel_def by fastforce

    have 4: "fvsst AA  fvsst (unlabel A)" by (metis ConsNegChecks.hyps(2) fvsst_cons_subset)

    have 5: "fvpairs F'  fvpairs F - set X  fvsst (unlabel A)"
      using ConsNegChecks.hyps(2) unfolding unlabel_def by force

    show ?case using ** 3 4 5 by blast
  qed (fastforce simp add: unlabel_def)+

  show ?Q using assms
    apply (induct "unlabel A" arbitrary: A A' D rule: strand_sem_stateful_induct)
    by (fastforce simp add: unlabel_def)+
qed

lemma tr_par_vars_disj:
  assumes "A'  set (trpc A D)" "fvpairs (unlabel D)  bvarssst (unlabel A) = {}"
  and "fvsst (unlabel A)  bvarssst (unlabel A) = {}"
  shows "fvlst A'  bvarslst A' = {}"
using assms tr_par_vars_subset by fast

lemma tr_par_trms_subset:
  assumes "A'  set (trpc A D)"
  shows "trmslst A'  trmssst (unlabel A)  pair ` setopssst (unlabel A)  pair ` snd ` set D"
using assms
proof (induction A D arbitrary: A' rule: trpc.induct)
  case 1 thus ?case by simp
next
  case (2 i t A D)
  then obtain A'' where A'': "A' = (i,send⟨tst)#A''" "A''  set (trpc A D)" by atomize_elim auto
  hence "trmslst A''  trmssst (unlabel A)  pair ` setopssst (unlabel A)  pair ` snd ` set D"
    by (metis "2.IH")
  thus ?case using A'' by (auto simp add: setopssst_def)
next
  case (3 i t A D)
  then obtain A'' where A'': "A' = (i,receive⟨tst)#A''" "A''  set (trpc A D)"
    by atomize_elim auto
  hence "trmslst A''  trmssst (unlabel A)  pair ` setopssst (unlabel A)  pair ` snd ` set D"
    by (metis "3.IH")
  thus ?case using A'' by (auto simp add: setopssst_def)
next
  case (4 i ac t t' A D)
  then obtain A'' where A'': "A' = (i,ac: t  t'st)#A''" "A''  set (trpc A D)"
    by atomize_elim auto
  hence "trmslst A''  trmssst (unlabel A)  pair ` setopssst (unlabel A)  pair ` snd ` set D"
    by (metis "4.IH")
  thus ?case using A'' by (auto simp add: setopssst_def)
next
  case (5 i t s A D)
  hence "A'  set (trpc A (List.insert (i,t,s) D))" by simp
  hence "trmslst A'  trmssst (unlabel A)  pair ` setopssst (unlabel A) 
                      pair ` snd ` set (List.insert (i,t,s) D)"
    by (metis "5.IH")
  thus ?case by (auto simp add: setopssst_def)
next
  case (6 i t s A D)
  from 6 obtain Di A'' B C where A'':
      "Di  set (subseqs (dbproj i D))" "A''  set (trpc A [dD. d  set Di])" "A' = (B@C)@A''"
      "B = map (λd. (i,check: (pair (t,s))  (pair (snd d))st)) Di"
      "C = map (λd. (i,[]⟨∨≠: [(pair (t,s), pair (snd d))]st)) [ddbproj i D. d  set Di]"
    by atomize_elim auto
  hence "trmslst A''  trmssst (unlabel A)  pair ` setopssst (unlabel A) 
                       pair ` snd ` set [dD. d  set Di]"
    by (metis "6.IH")
  moreover have "set [dD. d  set Di]  set D" using set_filter by auto
  ultimately have
      "trmslst A''  trmssst (unlabel A)  pair ` setopssst (unlabel A)  pair ` snd ` set D"
    by blast
  hence "trmslst A''  trmssst (unlabel ((i,delete⟨t,s)#A)) 
                        pair ` setopssst (unlabel ((i,delete⟨t,s)#A)) 
                        pair ` snd ` set D"
    using setopssst_cons_subset trmssst_cons
    by (auto simp add: setopssst_def)
  moreover have "set Di  set D" "set [ddbproj i D . d  set Di]  set D"
    using subseqs_set_subset[OF A''(1)] unfolding