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 dbproj_def by auto
  hence "trmsst (unlabel B)  insert (pair (t, s)) (pair ` snd ` set D)"
        "trmsst (unlabel C)  insert (pair (t, s)) (pair ` snd ` set D)"
    using A''(4,5) unfolding unlabel_def by auto
  hence "trmsst (unlabel (B@C))  insert (pair (t,s)) (pair ` snd ` set D)"
    using unlabel_append[of B C] by auto
  moreover have "pair (t,s)  pair ` setopssst (delete⟨t,s#unlabel A)" by (simp add: setopssst_def)
  ultimately show ?case
    using A''(3) trmsst_append[of "unlabel (B@C)" "unlabel A'"] unlabel_append[of "B@C" A'']
    by (auto simp add: setopssst_def)
next
  case (7 i ac t s A D)
  from 7 obtain d A'' where A'':
      "d  set (dbproj i D)" "A''  set (trpc A D)"
      "A' = (i,ac: (pair (t,s))  (pair (snd d))st)#A''"
    by atomize_elim force
  hence "trmslst A''  trmssst (unlabel A)  pair ` setopssst (unlabel A) 
                       pair ` snd ` set D"
    by (metis "7.IH")
  moreover have "trmsst (unlabel A') = {pair (t,s), pair (snd d)}  trmsst (unlabel A'')"
    using A''(1,3) by auto
  ultimately show ?case using A''(1) unfolding dbproj_def by (auto simp add: setopssst_def)
next
  case (8 i X F F' A D)
  define constr where "constr = map (λG. (i,X⟨∨≠: (F@G)st)) (trpairs F' (map snd (dbproj i D)))"
  define B where "B  (trmspairs ` set (trpairs F' (map snd (dbproj i D))))"

  from 8 obtain A'' where A'':
      "A''  set (trpc A D)" "A' = constr@A''"
    unfolding constr_def by atomize_elim auto

  have "trmsst (unlabel A'')  trmssst (unlabel A)  pair ` setopssst (unlabel A)  pair`snd`set D"
    by (metis A''(1) "8.IH")
  moreover have "trmsst (unlabel constr)  B  trmspairs F  pair ` snd ` set D"
    unfolding unlabel_def constr_def B_def by auto
  ultimately have "trmsst (unlabel A')  B  trmspairs F  trmssst (unlabel A) 
                                         pair ` setopssst (unlabel A)  pair ` snd ` set D"
    using A'' unlabel_append[of constr A''] by auto
  moreover have "set (dbproj i D)  set D" unfolding dbproj_def by auto
  hence "B  pair ` set F'  pair ` snd ` set D"
    using trpairs_trms_subset'[of F' "map snd (dbproj i D)"]
    unfolding B_def by force
  moreover have
      "pair ` setopssst (unlabel ((i, X⟨∨≠: F ∨∉: F')#A)) =
       pair ` set F'  pair ` setopssst (unlabel A)"
    by auto
  ultimately show ?case by (auto simp add: setopssst_def)
qed

lemma tr_par_wf_trms:
  assumes "A'  set (trpc A [])" "wftrms (trmssst (unlabel A))"
  shows "wftrms (trmslst A')"
using tr_par_trms_subset[OF assms(1)] setopssst_wftrms(2)[OF assms(2)]
by auto

lemma tr_par_wf':
  assumes "fvpairs (unlabel D)  bvarssst (unlabel A) = {}"
  and "fvpairs (unlabel D)  X"
  and "wf'sst X (unlabel A)" "fvsst (unlabel A)  bvarssst (unlabel A) = {}"
  and "A'  set (trpc A D)"
  shows "wflst X A'"
proof -
  define P where
    "P = (λ(D::('fun,'var,'lbl) labeleddbstatelist) (A::('fun,'var,'lbl) labeled_stateful_strand).
          (fvpairs (unlabel D)  bvarssst (unlabel A) = {}) 
          fvsst (unlabel A)  bvarssst (unlabel 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: X A' D)
    case Nil thus ?case by simp
  next
    case (Cons a A)
    obtain i s where i: "a = (i,s)" by (metis surj_pair)
    note prems = Cons.prems
    note IH = Cons.IH
    show ?case
    proof (cases s)
      case (Receive ts)
      note si = Receive i
      then obtain A'' where A'':
          "A' = (i,receive⟨tsst)#A''" "A''  set (trpc A D)" "fvset (set ts)  X"
        using prems unlabel_Cons(1)[of i s A] by atomize_elim auto
      have *: "wf'sst X (unlabel A)"
              "fvpairs (unlabel D)  X"
              "P D A"
        using prems si apply (force, force)
        using prems(4) si unfolding P_def by fastforce
      show ?thesis using IH[OF A''(2) *] A''(1,3) by simp
    next
      case (Send ts)
      note si = Send i
      then obtain A'' where A'': "A' = (i,send⟨tsst)#A''" "A''  set (trpc A D)"
        using prems by atomize_elim auto
      have *: "wf'sst (X  fvset (set ts)) (unlabel A)"
              "fvpairs (unlabel D)  X  fvset (set ts)"
              "P D A"
        using prems si apply (force, force)
        using prems(4) si unfolding P_def by fastforce
      show ?thesis using IH[OF A''(2) *] A''(1) by simp
    next
      case (Equality ac t t')
      note si = Equality i
      then obtain A'' where A'':
          "A' = (i,ac: t  t'st)#A''" "A''  set (trpc A D)"
          "ac = Assign  fv t'  X"
        using prems unlabel_Cons(1)[of i s] by atomize_elim force
      have *: "ac = Assign  wf'sst (X  fv t) (unlabel A)"
              "ac = Check  wf'sst X (unlabel A)"
              "ac = Assign  fvpairs (unlabel D)  X  fv t"
              "ac = Check  fvpairs (unlabel D)  X"
              "P D A"
        using prems si apply (force, force, force, force)
        using prems(4) si unfolding P_def by fastforce
      show ?thesis
        using IH[OF A''(2) *(1,3,5)] IH[OF A''(2) *(2,4,5)] A''(1,3)
        by (cases ac) simp_all
    next
      case (Insert t t')
      note si = Insert i
      hence A': "A'  set (trpc A (List.insert (i,t,t') D))" "fv t  X" "fv t'  X"
        using prems by auto
      have *: "wf'sst X (unlabel A)" "fvpairs (unlabel (List.insert (i,t,t') D))  X"
        using prems si by (auto simp add: unlabel_def)
      have **: "P (List.insert (i,t,t') D) A"
        using prems(4) si
        unfolding P_def unlabel_def
        by fastforce
      show ?thesis using IH[OF A'(1) * **] A'(2,3) by simp
    next
      case (Delete t t')
      note si = Delete i
      define constr where "constr = (λDi.
        (map (λd. (i,check: (pair (t,t'))  (pair (snd d))st)) Di)@
        (map (λd. (i,[]⟨∨≠: [(pair (t,t'), pair (snd d))]st)) [ddbproj i D. d  set Di]))"
      from prems si obtain Di A'' where A'':
          "A' = constr Di@A''" "A''  set (trpc A [dD. d  set Di])"
          "Di  set (subseqs (dbproj i D))"
        unfolding constr_def by auto
      have *: "wf'sst X (unlabel A)"
              "fvpairs (unlabel (filter (λd. d  set Di) D))  X"
        using prems si apply simp
        using prems si by (fastforce simp add: unlabel_def)

      have "fvpairs (unlabel (filter (λd. d  set Di) D))  fvpairs (unlabel D)"
        by (auto simp add: unlabel_def)
      hence **: "P [dD. d  set Di] A"
        using prems si unfolding P_def
        by fastforce

      have ***: "fvpairs (unlabel D)  X" using prems si by auto
      show ?thesis
        using IH[OF A''(2) * **] A''(1) wf_pair_eqs_ineqs_map'[OF _ A''(3) ***]
        unfolding constr_def by simp
    next
      case (InSet ac t t')
      note si = InSet i
      then obtain d A'' where A'':
          "A' = (i,ac: (pair (t,t'))  (pair (snd d))st)#A''"
          "A''  set (trpc A D)"
          "d  set D"
        using prems by (auto simp add: dbproj_def)
      have *:
          "ac = Assign  wf'sst (X  fv t  fv t') (unlabel A)"
          "ac = Check  wf'sst X (unlabel A)"
          "ac = Assign  fvpairs (unlabel D)  X  fv t  fv t'"
          "ac = Check  fvpairs (unlabel D)  X"
          "P D A"
        using prems si apply (force, force, force, force)
        using prems(4) si unfolding P_def by fastforce
      have **: "fv (pair (snd d))  X"
        using A''(3) prems(3) fv_pair_fvpairs_subset
        by fast
      have ***: "fv (pair (t,t')) = fv t  fv t'" unfolding pair_def by auto
      show ?thesis
        using IH[OF A''(2) *(1,3,5)] IH[OF A''(2) *(2,4,5)] A''(1) ** ***
        by (cases ac) (simp_all add: Un_assoc)
    next
      case (NegChecks Y F F')
      note si = NegChecks i
      then obtain A'' where A'':
          "A' = (map (λG. (i,Y⟨∨≠: (F@G)st)) (trpairs F' (map snd (dbproj i D))))@A''"
          "A''  set (trpc A D)"
        using prems by atomize_elim auto

      have *: "wf'sst X (unlabel A)" "fvpairs (unlabel D)  X" using prems si by auto
      
      have "bvarssst (unlabel A)  bvarssst (unlabel ((i,Y⟨∨≠: F ∨∉: F')#A))"
           "fvsst (unlabel A)  fvsst (unlabel ((i,Y⟨∨≠: F ∨∉: F')#A))"
        by auto
      hence **:  "P D A" using prems si unfolding P_def by blast
  
      show ?thesis using IH[OF A''(2) * **] A''(1) wf_pair_negchecks_map' by simp
    qed
  qed
qed

lemma tr_par_wf:
  assumes "A'  set (trpc A [])"
    and "wfsst (unlabel A)"
    and "wftrms (trmslsst A)"
  shows "wflst {} A'"
    and "wftrms (trmslst A')"
    and "fvlst A'  bvarslst A' = {}"
using tr_par_wf'[OF _ _ _ _ assms(1)]
      tr_par_wf_trms[OF assms(1,3)]
      tr_par_vars_disj[OF assms(1)]
      assms(2)
by fastforce+

lemma tr_par_proj:
  assumes "B  set (trpc A D)"
  shows "proj n B  set (trpc (proj n A) (proj n D))"
using assms
proof (induction A D arbitrary: B rule: trpc.induct)
  case (5 i t s S D)
  note prems = "5.prems"
  note IH = "5.IH"
  have IH': "proj n B  set (trpc (proj n S) (proj n (List.insert (i,t,s) D)))"
    using prems IH by auto
  show ?case
  proof (cases "(i = ln n)  (i = )")
    case True thus ?thesis
      using IH' proj_list_insert(1,2)[of n "(t,s)" D] proj_list_Cons(1,2)[of n _ S]
      by auto
  next
    case False
    then obtain m where "i = ln m" "n  m" by (cases i) simp_all
    thus ?thesis
      using IH' proj_list_insert(3)[of n _ "(t,s)" D] proj_list_Cons(3)[of n _ "insert⟨t,s" S]
      by auto
  qed
next
  case (6 i t s S D)
  note prems = "6.prems"
  note IH = "6.IH"
  define constr where "constr = (λDi D.
      (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]))"

  obtain Di B' where B':
      "B = constr Di D@B'"
      "Di  set (subseqs (dbproj i D))"
      "B'  set (trpc S [dD. d  set Di])"
    using prems constr_def by fastforce
  hence "proj n B'  set (trpc (proj n S) (proj n [dD. d  set Di]))" using IH by simp
  hence IH': "proj n B'  set (trpc (proj n S) [dproj n D. d  set Di])" by (metis proj_filter)
  show ?case
  proof (cases "(i = ln n)  (i = )")
    case True
    hence "proj n B = constr Di D@proj n B'" "Di  set (subseqs (dbproj i (proj n D)))"
      using B'(1,2) proj_dbproj(1,2)[of n D] unfolding proj_def constr_def by auto
    moreover have "constr Di (proj n D) = constr Di D"
      using True proj_dbproj(1,2)[of n D] unfolding constr_def by presburger
    ultimately have "proj n B  set (trpc ((i, delete⟨t,s)#proj n S) (proj n D))"
      using IH' unfolding constr_def by force
    thus ?thesis by (metis proj_list_Cons(1,2) True)
  next
    case False
    then obtain m where m: "i = ln m" "n  m" by (cases i) simp_all
    hence *: "(ln n)  i" by simp
    have "proj n B = proj n B'" using B'(1) False unfolding constr_def proj_def by auto
    moreover have "[dproj n D. d  set Di] = proj n D"
      using proj_subseq[OF _ m(2)[symmetric]] m(1) B'(2) by simp
    ultimately show ?thesis using m(1) IH' proj_list_Cons(3)[OF m(2), of _ S] by auto
  qed
next
  case (7 i ac t s S D)
  note prems = "7.prems"
  note IH = "7.IH"
  define constr where "constr = (
    λd::'lbl strand_label × ('fun,'var) term × ('fun,'var) term.
      (i,ac: (pair (t,s))  (pair (snd d))st))"

  obtain d B' where B':
      "B = constr d#B'"
      "d  set (dbproj i D)"
      "B'  set (trpc S D)"
    using prems constr_def by fastforce
  hence IH': "proj n B'  set (trpc (proj n S) (proj n D))" using IH by auto

  show ?case
  proof (cases "(i = ln n)  (i = )")
    case True
    hence "proj n B = constr d#proj n B'" "d  set (dbproj i (proj n D))"
      using B' proj_list_Cons(1,2)[of n _ B']
      unfolding constr_def
      by (force, metis proj_dbproj(1,2))
    hence "proj n B  set (trpc ((i, InSet ac t s)#proj n S) (proj n D))"
      using IH' unfolding constr_def by auto
    thus ?thesis using proj_list_Cons(1,2)[of n _ S] True by metis
  next
    case False
    then obtain m where m: "i = ln m" "n  m" by (cases i) simp_all
    hence "proj n B = proj n B'" using B'(1) proj_list_Cons(3) unfolding constr_def by auto
    thus ?thesis
      using IH' m proj_list_Cons(3)[OF m(2), of "InSet ac t s" S]
      unfolding constr_def
      by auto
  qed
next
  case (8 i X F F' S D)
  note prems = "8.prems"
  note IH = "8.IH"

  define constr where
    "constr = (λD. map (λG. (i,X⟨∨≠: (F@G)st)) (trpairs F' (map snd (dbproj i D))))"
  
  obtain B' where B':
      "B = constr D@B'"
      "B'  set (trpc S D)"
    using prems constr_def by fastforce
  hence IH': "proj n B'  set (trpc (proj n S) (proj n D))" using IH by auto

  show ?case
  proof (cases "(i = ln n)  (i = )")
    case True
    hence "proj n B = constr (proj n D)@proj n B'"
      using B'(1,2) proj_dbproj(1,2)[of n D] unfolding proj_def constr_def by auto
    hence "proj n B  set (trpc ((i, NegChecks X F F')#proj n S) (proj n D))"
      using IH' unfolding constr_def by auto
    thus ?thesis using proj_list_Cons(1,2)[of n _ S] True by metis
  next
    case False
    then obtain m where m: "i = ln m" "n  m" by (cases i) simp_all
    hence "proj n B = proj n B'" using B'(1) unfolding constr_def proj_def by auto
    thus ?thesis
      using IH' m proj_list_Cons(3)[OF m(2), of "NegChecks X F F'" S]
      unfolding constr_def
      by auto
  qed
qed (force simp add: proj_def)+

lemma tr_par_preserves_par_comp:
  assumes "par_complsst A Sec" "A'  set (trpc A [])"
  shows "par_comp A' Sec"
proof -
  let ?M = "λl. trmssst (proj_unl l A)  pair ` setopssst (proj_unl l A)"
  let ?N = "λl. trms_projlst l A'"

  have 0: "l1 l2. l1  l2  GSMP_disjoint (?M l1) (?M l2) Sec"
    using assms(1) unfolding par_complsst_def by simp_all

  { fix l1 l2::'lbl assume *: "l1  l2"
    hence "GSMP_disjoint (?M l1) (?M l2) Sec" using 0(1) by metis
    moreover have "pair ` snd ` set (proj n []) = {}" for n::'lbl unfolding proj_def by simp
    hence "?N l1  ?M l1" "?N l2  ?M l2"
      using tr_par_trms_subset[OF tr_par_proj[OF assms(2)]] by (metis Un_empty_right)+
    ultimately have "GSMP_disjoint (?N l1) (?N l2) Sec"
      using GSMP_disjoint_subset by presburger
  } hence 1: "l1 l2. l1  l2  GSMP_disjoint (trms_projlst l1 A') (trms_projlst l2 A') Sec"
    using 0(1) by metis

  have 2: "ground Sec" "s  Sec. ¬{} c s"
    using assms(1) unfolding par_complsst_def by metis+

  show ?thesis using 1 2 unfolding par_comp_def by metis
qed

lemma tr_preserves_receives:
  assumes "E  set (trpc F D)" "(l, receive⟨t)  set F"
  shows "(l, receive⟨tst)  set E"
using assms by (induct F D arbitrary: E rule: trpc.induct) auto

lemma tr_preserves_last_receive:
  assumes "E  set (trpc F D)" "suffix [(l, receive⟨tst)] E"
  shows "G. suffix ((l, receive⟨t)#G) F  list_all (Not  is_Receive  snd) G"
    (is "G. ?P G F  ?Q G")
using assms
proof (induction F D arbitrary: E rule: trpc.induct)
  case (1 D) thus ?case by simp
next
  case (2 i t' S D)
  note prems = "2.prems"
  note IH = "2.IH"

  obtain E' where E': "E = (i,send⟨t'st)#E'" "E'  set (trpc S D)"
    using prems(1) by auto

  obtain G where G: "?P G S" "?Q G"
    using suffix_Cons'[OF prems(2)[unfolded E'(1)]] IH[OF E'(2)] by blast

  show ?case by (metis suffix_Cons G)
next
  case (3 i t' S D)
  note prems = "3.prems"
  note IH = "3.IH"

  obtain E' where E': "E = (i,receive⟨t'st)#E'" "E'  set (trpc S D)"
    using prems(1) by auto

  show ?case using suffix_Cons'[OF prems(2)[unfolded E'(1)]]
  proof
    assume "suffix [(l, receive⟨tst)] E'"
    then obtain G where G: "?P G S" "?Q G"
      using IH[OF E'(2)] by blast
    show ?thesis by (metis suffix_Cons G)
  next
    assume "(i, receive⟨t'st) = (l, receive⟨tst)  E' = []"
    hence *: "i = l" "t' = t" "E' = []" by simp_all
    show ?thesis
      using tr_preserves_receives[OF E'(2)]
      unfolding * list_all_iff is_Receive_def by fastforce
  qed
next
  case (4 i ac t' t'' S D)
  note prems = "4.prems"
  note IH = "4.IH"

  obtain E' where E': "E = (i,ac: t'  t''st)#E'" "E'  set (trpc S D)"
    using prems(1) by auto

  obtain G where G: "?P G S" "?Q G"
    using suffix_Cons'[OF prems(2)[unfolded E'(1)]] IH[OF E'(2)] by blast

  show ?case by (metis suffix_Cons G)
next
  case (5 i t' s S D)
  note prems = "5.prems"
  note IH = "5.IH"

  have "E  set (trpc S (List.insert (i,t',s) D))" using prems(1) by auto
  thus ?case by (metis IH[OF _ prems(2)] suffix_Cons)
next
  case (6 i t' s S D)
  note prems = "6.prems"
  note IH = "6.IH"

  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))
      (filter (λd. d  set Di) (dbproj i D))))"

  obtain E' Di where E':
      "E = constr Di@E'" "E'  set (trpc S (filter (λd. d  set Di) D))"
      "Di  set (subseqs (dbproj i D))"
    using prems(1) unfolding constr_def by auto

  have "receive⟨tst  snd ` set (constr Di)" unfolding constr_def by force
  hence "¬suffix [(l, receive⟨tst)] (constr Di)" unfolding suffix_def by auto
  hence "1  length E'" using prems(2) E'(1) by (cases E') auto
  hence "suffix [(l, receive⟨tst)] E'"
    using suffix_length_suffix[OF prems(2) suffixI[OF E'(1)]] by simp
  thus ?case by (metis IH[OF E'(3,2)] suffix_Cons)
next
  case (7 i ac t' s S D)
  note prems = "7.prems"
  note IH = "7.IH"

  define constr where "constr = (
    λd::(('lbl strand_label × ('fun,'var) term × ('fun,'var) term)).
      (i,ac: (pair (t',s))  (pair (snd d))st))"
  
  obtain E' d where E': "E = constr d#E'" "E'  set (trpc S D)" "d  set (dbproj i D)"
    using prems(1) unfolding constr_def by auto

  have "receive⟨tst  snd (constr d)" unfolding constr_def by force
  hence "suffix [(l, receive⟨tst)] E'" using prems(2) E'(1) suffix_Cons' by fastforce
  thus ?case by (metis IH[OF E'(2)] suffix_Cons)
next
  case (8 i X G G' S D)
  note prems = "8.prems"
  note IH = "8.IH"

  define constr where
    "constr = map (λH. (i,X⟨∨≠: (G@H)st)) (trpairs G' (map snd (dbproj i D)))"
  
  obtain E' where E': "E = constr@E'" "E'  set (trpc S D)"
    using prems(1) constr_def by auto

  have "receive⟨tst  snd ` set constr" unfolding constr_def by force
  hence "¬suffix [(l, receive⟨tst)] constr" unfolding suffix_def by auto
  hence "1  length E'" using prems(2) E'(1) by (cases E') auto
  hence "suffix [(l, receive⟨tst)] E'"
    using suffix_length_suffix[OF prems(2) suffixI[OF E'(1)]] by simp
  thus ?case by (metis IH[OF E'(2)] suffix_Cons)
qed

lemma tr_leaking_prefix_exists:
  assumes "A'  set (trpc A [])" "prefix B A'" "ikst (proj_unl n B) set   t"
  shows "C D. prefix C B  prefix D A  C  set (trpc D [])  (ikst (proj_unl n C) set   t) 
               (¬{} c t  (l s G. suffix ((l, receive⟨s)#G) D  list_all (Not  is_Receive  snd) G))"
proof -
  let ?P = "λB C C'. B = C@C'  (n t. (n, receive⟨tst)  set C') 
                     (C = []  (n t. suffix [(n,receive⟨tst)] C))"

  have "C C'. ?P B C C'"
  proof (induction B)
    case (Cons b B)
    then obtain C C' n s where *: "?P B C C'" "b = (n,s)" by atomize_elim auto
    show ?case
    proof (cases "C = []")
      case True
      note T = True
      show ?thesis
      proof (cases "t. s = receive⟨tst")
        case True
        hence "?P (b#B) [b] C'" using * T  by auto
        thus ?thesis by metis
      next
        case False
        hence "?P (b#B) [] (b#C')" using * T by auto
        thus ?thesis by metis
      qed
    next
      case False
      hence "?P (b#B) (b#C) C'" using * unfolding suffix_def by auto
      thus ?thesis by metis
    qed
  qed simp
  then obtain C C' where C:
      "B = C@C'" "n t. (n, receive⟨tst)  set C'"
      "C = []  (n t. suffix [(n,receive⟨tst)] C)"
    by atomize_elim auto
  hence 1: "prefix C B" by simp
  hence 2: "prefix C A'" using assms(2) by simp

  have "m t. (m,receive⟨tst)  set B  (m,receive⟨tst)  set C" using C by auto
  hence "t. receive⟨tst  set (proj_unl n B)  receive⟨tst  set (proj_unl n C)"
    unfolding unlabel_def proj_def by force
  hence "ikst (proj_unl n B)  ikst (proj_unl n C)" using ikst_is_rcv_set by blast
  hence 3: "ikst (proj_unl n C) set   t" by (metis ideduct_mono[OF assms(3)] subst_all_mono)

  have "F. prefix F A  E  set (trpc F D)"
    when "suffix [(m, receive⟨tst)] E" "prefix E A'" "A'  set (trpc A D)" for D E m t
    using that
  proof (induction A D arbitrary: A' E rule: trpc.induct)
    case (1 D) thus ?case by simp
  next
    case (2 i t' S D)
    note prems = "2.prems"
    note IH = "2.IH"
    obtain A'' where *: "A' = (i,send⟨t'st)#A''" "A''  set (trpc S D)"
      using prems(3) by auto
    have "E  []" using prems(1) by auto
    then obtain E' where **: "E = (i,send⟨t'st)#E'"
      using *(1) prems(2) by (cases E) auto
    hence "suffix [(m, receive⟨tst)] E'" "prefix E' A''"
      using *(1) prems(1,2) suffix_Cons[of _ _ E'] by auto
    then obtain F where "prefix F S" "E'  set (trpc F D)"
      using *(2) ** IH by metis
    hence "prefix ((i,Send t')#F) ((i,Send t')#S)" "E  set (trpc ((i,Send t')#F) D)"
      using ** by auto
    thus ?case by metis
  next
    case (3 i t' S D)
    note prems = "3.prems"
    note IH = "3.IH"
    obtain A'' where *: "A' = (i,receive⟨t'st)#A''" "A''  set (trpc S D)"
      using prems(3) by auto
    have "E  []" using prems(1) by auto
    then obtain E' where **: "E = (i,receive⟨t'st)#E'"
      using *(1) prems(2) by (cases E) auto
    show ?case
    proof (cases "(m, receive⟨tst) = (i, receive⟨t'st)")
      case True
      note T = True
      show ?thesis
      proof (cases "suffix [(m, receive⟨tst)] E'")
        case True
        hence "suffix [(m, receive⟨tst)] E'" "prefix E' A''"
          using ** *(1) prems(1,2) by auto
        then obtain F where "prefix F S" "E'  set (trpc F D)"
          using *(2) ** IH by metis
        hence "prefix ((i,receive⟨t')#F) ((i,receive⟨t')#S)"
              "E  set (trpc ((i,receive⟨t')#F) D)"
          using ** by auto
        thus ?thesis by metis
      next
        case False
        hence "E' = []"
          using **(1) T prems(1)
                suffix_Cons[of "[(m, receive⟨tst)]" "(m, receive⟨tst)" E']
          by auto
        hence "prefix [(i,receive⟨t')] ((i,receive⟨t') # S)  E  set (trpc [(i,receive⟨t')] D)"
          using * ** prems by auto
        thus ?thesis by metis
      qed
    next
      case False
      hence "suffix [(m, receive⟨tst)] E'" "prefix E' A''"
        using ** *(1) prems(1,2) suffix_Cons[of _ _ E'] by auto
      then obtain F where "prefix F S" "E'  set (trpc F D)" using *(2) ** IH by metis
      hence "prefix ((i,receive⟨t')#F) ((i,receive⟨t')#S)" "E  set (trpc ((i,receive⟨t')#F) D)"
        using ** by auto
      thus ?thesis by metis
    qed
  next
    case (4 i ac t' t'' S D)
    note prems = "4.prems"
    note IH = "4.IH"
    obtain A'' where *: "A' = (i,ac: t'  t''st)#A''" "A''  set (trpc S D)"
      using prems(3) by auto
    have "E  []" using prems(1) by auto
    then obtain E' where **: "E = (i,ac: t'  t''st)#E'"
      using *(1) prems(2) by (cases E) auto
    hence "suffix [(m, receive⟨tst)] E'" "prefix E' A''"
      using *(1) prems(1,2) suffix_Cons[of _ _ E'] by auto
    then obtain F where "prefix F S" "E'  set (trpc F D)"
      using *(2) ** IH by metis
    hence "prefix ((i,Equality ac t' t'')#F) ((i,Equality ac t' t'')#S)"
          "E  set (trpc ((i,Equality ac t' t'')#F) D)"
      using ** by auto
    thus ?case by metis
  next
    case (5 i t' s S D)
    note prems = "5.prems"
    note IH = "5.IH"
    have *: "A'  set (trpc S (List.insert (i,t',s) D))" using prems(3) by auto
    have "E  []" using prems(1) by auto
    hence "suffix [(m, receive⟨tst)] E" "prefix E A'"
      using *(1) prems(1,2) suffix_Cons[of _ _ E] by auto
    then obtain F where "prefix F S" "E  set (trpc F (List.insert (i,t',s) D))"
      using * IH by metis
    hence "prefix ((i,insert⟨t',s)#F) ((i,insert⟨t',s)#S)"
          "E  set (trpc ((i,insert⟨t',s)#F) D)"
      by auto
    thus ?case by metis
  next
    case (6 i t' s S D)
    note prems = "6.prems"
    note IH = "6.IH"

    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))
        (filter (λd. d  set Di) (dbproj i D))))"

    obtain A'' Di where *:
        "A' = constr Di@A''" "A''  set (trpc S (filter (λd. d  set Di) D))"
        "Di  set (subseqs (dbproj i D))"
      using prems(3) constr_def by auto
    have ***:  "(m, receive⟨tst)  set (constr Di)" using constr_def by auto
    have "E  []" using prems(1) by auto
    then obtain E' where **: "E = constr Di@E'"
      using *(1) prems(1,2) ***
      by (metis (mono_tags, lifting) Un_iff list.set_intros(1) prefixI prefix_def
                                     prefix_same_cases set_append suffix_def)
    hence "suffix [(m, receive⟨tst)] E'" "prefix E' A''"
      using *(1) prems(1,2) suffix_append[of "[(m,receive⟨tst)]" "constr Di" E'] ***
      by (metis (no_types, opaque_lifting) Nil_suffix append_Nil2 in_set_conv_decomp rev_exhaust
                                      snoc_suffix_snoc suffix_appendD,
          auto)
    then obtain F where "prefix F S" "E'  set (trpc F (filter (λd. d  set Di) D))"
      using *(2,3) ** IH by metis
    hence "prefix ((i,delete⟨t',s)#F) ((i,delete⟨t',s)#S)"
          "E  set (trpc ((i,delete⟨t',s)#F) D)"
      using *(3) ** constr_def by auto
    thus ?case by metis
  next
    case (7 i ac t' s S D)
    note prems = "7.prems"
    note IH = "7.IH"

    define constr where "constr = (
      λd::(('lbl strand_label × ('fun,'var) term × ('fun,'var) term)).
        (i,ac: (pair (t',s))  (pair (snd d))st))"
    
    obtain A'' d where *: "A' = constr d#A''" "A''  set (trpc S D)" "d  set (dbproj i D)"
      using prems(3) constr_def by auto
    have "E  []" using prems(1) by auto
    then obtain E' where **: "E = constr d#E'" using *(1) prems(2) by (cases E) auto
    hence "suffix [(m, receive⟨tst)] E'" "prefix E' A''"
      using *(1) prems(1,2) suffix_Cons[of _ _ E'] using constr_def by auto
    then obtain F where "prefix F S" "E'  set (trpc F D)" using *(2) ** IH by metis
    hence "prefix ((i,InSet ac t' s)#F) ((i,InSet ac t' s)#S)"
          "E  set (trpc ((i,InSet ac t' s)#F) D)"
      using *(3) ** unfolding constr_def by auto
    thus ?case by metis
  next
    case (8 i X G G' S D)
    note prems = "8.prems"
    note IH = "8.IH"

    define constr where
      "constr = map (λH. (i,X⟨∨≠: (G@H)st)) (trpairs G' (map snd (dbproj i D)))"
    
    obtain A'' where *: "A' = constr@A''" "A''  set (trpc S D)"
      using prems(3) constr_def by auto
    have ***:  "(m, receive⟨tst)  set constr" using constr_def by auto
    have "E  []" using prems(1) by auto
    then obtain E' where **: "E = constr@E'"
      using *(1) prems(1,2) ***
      by (metis (mono_tags, lifting) Un_iff list.set_intros(1) prefixI prefix_def
                                     prefix_same_cases set_append suffix_def)
    hence "suffix [(m, receive⟨tst)] E'" "prefix E' A''"
      using *(1) prems(1,2) suffix_append[of "[(m,receive⟨tst)]" constr E'] ***
      by (metis (no_types, opaque_lifting) Nil_suffix append_Nil2 in_set_conv_decomp rev_exhaust
                                      snoc_suffix_snoc suffix_appendD,
          auto)
    then obtain F where "prefix F S" "E'  set (trpc F D)" using *(2) ** IH by metis
    hence "prefix ((i,NegChecks X G G')#F) ((i,NegChecks X G G')#S)"
          "E  set (trpc ((i,NegChecks X G G')#F) D)"
      using ** constr_def by auto
    thus ?case by metis
  qed
  moreover have "prefix [] A" "[]  set (trpc [] [])" by auto
  moreover have "{} c t" when "C = []" using 3 by (simp add: deducts_eq_if_empty_ik that)
  ultimately have 4:
      "D. prefix D A  C  set (trpc D []) 
           (¬{} c t  (l s G. suffix ((l, receive⟨s)#G) D 
                                  list_all (Not  is_Receive  snd) G))"
    using C(3) assms(1) 2 by (meson tr_preserves_last_receive)

  show ?thesis by (metis 1 3 4)
qed

end

context labeled_stateful_typing
begin


lemma tr_par_tfrsstp:
  assumes "A'  set (trpc A D)" "list_all tfrsstp (unlabel A)"
  and "fvsst (unlabel A)  bvarssst (unlabel A) = {}" (is "?P0 A D")
  and "fvpairs (unlabel D)  bvarssst (unlabel A) = {}" (is "?P1 A D")
  and "t  pair ` setopssst (unlabel A)  pair ` snd ` set D.
       t'  pair ` setopssst (unlabel A)  pair ` snd ` set D.
          (δ. Unifier δ t t')  Γ t = Γ t'" (is "?P3 A D")
  shows "list_all tfrstp (unlabel A')"
proof -
  have sublmm: "list_all tfrsstp (unlabel A)" "?P0 A D" "?P1 A D" "?P3 A D"
    when p: "list_all tfrsstp (unlabel (a#A))" "?P0 (a#A) D" "?P1 (a#A) D" "?P3 (a#A) D"
    for a A D
  proof -
    show "list_all tfrsstp (unlabel A)" using p(1) by (simp add: unlabel_def tfrsst_def)
    show "?P0 A D" using p(2) fvsst_cons_subset unfolding unlabel_def by fastforce
    show "?P1 A D" using p(3) bvarssst_cons_subset unfolding unlabel_def by fastforce
    have "setopssst (unlabel A)  setopssst (unlabel (a#A))"
      using setopssst_cons_subset unfolding unlabel_def by auto
    thus "?P3 A D" using p(4) by blast
  qed

  show ?thesis using assms
  proof (induction A D arbitrary: A' rule: trpc.induct)
    case 1 thus ?case by simp
  next
    case (2 i t A D)
    note prems = "2.prems"
    note IH = "2.IH"
    from prems(1) obtain A'' where A'': "A' = (i,send⟨tst)#A''" "A''  set (trpc A D)" by atomize_elim auto
    have "list_all tfrstp (unlabel 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 i t A D)
    note prems = "3.prems"
    note IH = "3.IH"
    from prems(1) obtain A'' where A'': "A' = (i,receive⟨tst)#A''" "A''  set (trpc A D)" by atomize_elim auto
    have "list_all tfrstp (unlabel 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 i ac t t' A D)
    note prems = "4.prems"
    note IH = "4.IH"
    from prems(1) obtain A'' where A'': "A' = (i,ac: t  t'st)#A''" "A''  set (trpc A D)" by atomize_elim auto
    have "list_all tfrstp (unlabel A'')"
      using IH[OF A''(2)] prems(5) sublmm[OF prems(2,3,4,5)]
      by meson
    thus ?case using A''(1) prems(2) by simp
  next
    case (5 i t s A D)
    note prems = "5.prems"
    note IH = "5.IH"
    from prems(1) have A': "A'  set (trpc A (List.insert (i,t,s) D))" by simp

    have 1: "list_all tfrsstp (unlabel A)" using sublmm[OF prems(2,3,4,5)] by simp
  
    have "pair ` setopssst (unlabel ((i,insert⟨t,s)#A))  pair`snd`set D =
          pair ` setopssst (unlabel A)  pair`snd`set (List.insert (i,t,s) D)"
      by (auto simp add: setopssst_def)
    hence 3: "?P3 A (List.insert (i,t,s) D)" using prems(5) by metis
    moreover have "?P1 A (List.insert (i,t,s) D)"
      using prems(3,4) bvarssst_cons_subset[of "unlabel A" "insert⟨t,s"]
      unfolding unlabel_def
      by fastforce
    ultimately have "list_all tfrstp (unlabel 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 i t s A D)
    note prems = "6.prems"
    note IH = "6.IH"

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

    from prems(1) obtain Di A'' where A'':
        "A' = constr Di@A''" "A''  set (trpc A (filter (λd. d  set Di) D))"
        "Di  set (subseqs (dbproj i D))"
      unfolding constr by fastforce

    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 "pair ` setopssst (unlabel A)  pair`snd`set [dD. d  set Di]
             pair ` setopssst (unlabel ((i,delete⟨t,s)#A))  pair`snd`set D"
      using subseqs_set_subset[OF A''(3)] by (force simp add: setopssst_def)
    moreover have "aM. bM. P a b"
      when "M  N" "aN. bN. P a b"
      for M N::"('fun, 'var) terms" and  P
      using that by blast
    ultimately have *: "?P3 A (filter (λd. d  set Di) D)"
      using prems(5) by presburger

    have **: "?P1 A (filter (λd. d  set Di) D)"
      using prems(4) bvarssst_cons_subset[of "unlabel A" "delete⟨t,s"]
      unfolding unlabel_def by fastforce
      
    have 1: "list_all tfrstp (unlabel 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 (unlabel A'') 
             (d  set Di. u = pair (t,s)  u' = pair (snd d))"
      when "ac: u  u'st  set (unlabel A')" for ac u u'
      using that A''(1) unfolding constr unlabel_def by force
    have 3:
        "X⟨∨≠: ust  set (unlabel A'') 
         (d  set (filter (λd. d  set Di) D). u = [(pair (t,s), pair (snd d))]  Q2 u X)"
      when "X⟨∨≠: ust  set (unlabel A')" for X u
      using that A''(1) unfolding Q2_def constr unlabel_def dbproj_def by force
    have 4: "dset D. (δ. Unifier δ (pair (t,s)) (pair (snd d)))
                        Γ (pair (t,s)) = Γ (pair (snd d))"
      using prems(5) by (simp add: setopssst_def)

    { fix ac u u'
      assume a: "ac: u  u'st  set (unlabel A')" "δ. Unifier δ u u'"
      hence "ac: u  u'st  set (unlabel A'')  (d  set Di. u = pair (t,s)  u' = pair (snd d))"
        using 2 by metis
      moreover {
        assume "ac: u  u'st  set (unlabel A'')"
        hence "tfrstp (ac: u  u'st)"
          using 1 Ball_set_list_all[of "unlabel A''" tfrstp]
          by fast
      } moreover {
        fix d assume "d  set Di" "u = pair (t,s)" "u' = pair (snd d)"
        hence "δ. Unifier δ u u'  Γ u = Γ u'"
          using 4 dbproj_subseq_subset A''(3)
          by fast
        hence "tfrstp (ac: u  u'st)"
          using Ball_set_list_all[of "unlabel A''" tfrstp]
          by simp
        hence "Γ u = Γ u'" using tfrstp_list_all_alt_def[of "unlabel A''"]
          using a(2) unfolding unlabel_def by auto
      } ultimately have "Γ u = Γ u'"
          using tfrstp_list_all_alt_def[of "unlabel A''"] a(2)
          unfolding unlabel_def by auto
    } moreover {
      fix u U
      assume "U⟨∨≠: ust  set (unlabel A')"
      hence "U⟨∨≠: ust  set (unlabel A'') 
             (d  set (filter (λd. d  set Di) D). u = [(pair (t,s), pair (snd 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 "unlabel A''"]
        unfolding Q1_def Q2_def
        by blast
    } ultimately show ?case
      using tfrstp_list_all_alt_def[of "unlabel A'"] unfolding Q1_def Q2_def unlabel_def by blast
  next
    case (7 i ac t s A D)
    note prems = "7.prems"
    note IH = "7.IH"

    from prems(1) obtain d A'' where A'':
        "A' = (i,ac: (pair (t,s))  (pair (snd d))st)#A''"
        "A''  set (trpc A D)"
        "d  set (dbproj i D)"
      by atomize_elim force

    have 1: "list_all tfrstp (unlabel 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: "Γ (pair (t,s)) = Γ (pair (snd d))"
      when "δ. Unifier δ (pair (t,s)) (pair (snd d))"
      using that prems(2,5) A''(3) unfolding tfrsst_def by (simp add: setopssst_def dbproj_def)
    
    show ?case using A''(1) 1 2 by fastforce
  next
    case (8 i X F F' A D)
    note prems = "8.prems"
    note IH = "8.IH"

    define constr where
      "constr = map (λG. (i,X⟨∨≠: (F@G)st)) (trpairs F' (map snd (dbproj i 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 obtain A'' where A'': "A' = constr@A''" "A''  set (trpc A D)"
      using constr_def by atomize_elim auto

    have 0: "constr = [(i,X⟨∨≠: Fst)]" when "F' = []" using that unfolding constr_def by simp

    have 1: "list_all tfrstp (unlabel 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: "F' = []  Q1 F X  list_all tfrstp (unlabel constr)"
      using 0 2 tfrstp_list_all_alt_def[of "unlabel constr"] unfolding Q1_def by auto

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

      have d_Q2: "Q2 (pair ` set (map snd D)) X" unfolding Q2_def
      proof (intro allI impI)
        fix f T assume "Fun f T  subtermsset (pair ` set (map snd D))"
        then obtain d where d: "d  set (map snd D)" "Fun f T  subterms (pair d)" by force
        hence "fv (pair d)  set X = {}"
          using prems(4) unfolding pair_def by (force simp add: unlabel_def)
        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 (map snd D)"
        using trpairs_trms_subset[OF G] unfolding dbproj_def by force
      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:
        "Q2 (trmspairs F  pair ` set F') X  list_all tfrstp (unlabel constr)"
      using Ball_set by blast

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

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

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

  have **: "list_all tfrsstp (unlabel A)" using assms(2) unfolding tfrsst_def by fast
  have "pair ` setopssst (unlabel A) 
        SMP (trmssst (unlabel A)  pair ` setopssst (unlabel A)) - Var`𝒱"
    using setopssst_are_pairs unfolding pair_def by auto
  hence "Γ t = Γ t'"
    when "δ. Unifier δ t t'" "t  pair ` setopssst (unlabel A)" "t'  pair ` setopssst (unlabel A)"
    for t t'
    using that assms(2) unfolding tfrsst_def tfrset_def by blast
  moreover have "fvpairs (unlabel []) = {}" "pair ` snd ` set [] = {}" by auto
  ultimately have 2: "list_all tfrstp (unlabel A')"
    using tr_par_tfrsstp[OF assms(1) ** assms(3)] by simp

  show ?thesis by (metis 1 2 tfrst_def)
qed

lemma tr_par_preserves_typing_cond:
  assumes "par_complsst A Sec" "typing_condsst (unlabel A)" "A'  set (trpc A [])"
  shows "typing_cond (unlabel A')"
proof -
  have "wf'sst {} (unlabel A)"
       "fvsst (unlabel A)  bvarssst (unlabel A) = {}"
       "wftrms (trmssst (unlabel A))"
    using assms(2) unfolding typing_condsst_def by simp_all
  hence 1: "wfst {} (unlabel A')"
           "fvst (unlabel A')  bvarsst (unlabel A') = {}"
           "wftrms (trmsst (unlabel A'))"
           "Ana_invar_subst (ikst (unlabel A')  assignment_rhsst (unlabel A'))"
    using tr_par_wf[OF assms(3)] Ana_invar_subst' by metis+

  have 2: "tfrst (unlabel A')" by (metis tr_par_tfr assms(2,3) typing_condsst_def)

  show ?thesis by (metis 1 2 typing_cond_def)
qed

end



subsection ‹Theorem: Semantic Equivalence of Translation›
context labeled_stateful_typed_model
begin

context
begin

text ‹
  An alternative version of the translation that does not perform database-state projections.
  It is used as an intermediate step in the proof of semantic equivalence/correctness.
›
private fun tr'pc::
  "('fun,'var,'lbl) labeled_stateful_strand  ('fun,'var,'lbl) labeleddbstatelist
    ('fun,'var,'lbl) labeled_strand list"
where
  "tr'pc [] D = [[]]"
| "tr'pc ((i,send⟨ts)#A) D = map ((#) (i,send⟨tsst)) (tr'pc A D)"
| "tr'pc ((i,receive⟨ts)#A) D = map ((#) (i,receive⟨tsst)) (tr'pc A D)"
| "tr'pc ((i,ac: t  t')#A) D = map ((#) (i,ac: t  t'st)) (tr'pc A D)"
| "tr'pc ((i,insert⟨t,s)#A) D = tr'pc A (List.insert (i,(t,s)) D)"
| "tr'pc ((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))
                                    [dD. d  set Di])@B)
                          (tr'pc A [dD. d  set Di]))
                (subseqs D)))"
| "tr'pc ((i,ac: t  s)#A) D =
    concat (map (λB. map (λd. (i,ac: (pair (t,s))  (pair (snd d))st)#B) D) (tr'pc A D))"
| "tr'pc ((i,X⟨∨≠: F ∨∉: F')#A) D =
    map ((@) (map (λG. (i,X⟨∨≠: (F@G)st)) (trpairs F' (map snd D)))) (tr'pc A D)"

subsubsection ‹Part 1›
private lemma tr'_par_iff_unlabel_tr:
  assumes "(i,p)  setopslsst A  set D.
           (j,q)  setopslsst A  set D.
              p = q  i = j"
  shows "(C  set (tr'pc A D). B = unlabel C)  B  set (tr (unlabel A) (unlabel D))"
    (is "?A  ?B")
proof
  { fix C have "C  set (tr'pc A D)  unlabel C  set (tr (unlabel A) (unlabel D))" using assms
    proof (induction A D arbitrary: C rule: tr'pc.induct)
      case (5 i t s S D)
      hence "unlabel C  set (tr (unlabel S) (unlabel (List.insert (i, t, s) D)))"
        by (auto simp add: setopslsst_def)
      moreover have
          "insert (i,t,s) (set D)  setopslsst ((i,insert⟨t,s)#S)  set D"
        by (auto simp add: setopslsst_def)
      hence "(j,p)  insert (i,t,s) (set D). (k,q)  insert (i,t,s) (set D). p = q  j = k"
        using "5.prems"(2) by blast
      hence "unlabel (List.insert (i, t, s) D) = (List.insert (t, s) (unlabel D))"
        using map_snd_list_insert_distrib[of "(i,t,s)" D] unfolding unlabel_def by simp
      ultimately show ?case by auto
    next
      case (6 i t s S D)
      let ?f1 = "λd. check: (pair (t,s))  (pair d)st"
      let ?g1 = "λd. []⟨∨≠: [(pair (t,s), pair d)]st"
      let ?f2 = "λd. (i, ?f1 (snd d))"
      let ?g2 = "λd. (i, ?g1 (snd d))"
  
      define constr1 where "constr1 = (λDi. (map ?f1 Di)@(map ?g1 [dunlabel D. d  set Di]))"
      define constr2 where "constr2 = (λDi. (map ?f2 Di)@(map ?g2 [dD. d  set Di]))"
  
      obtain C' Di where C':
          "Di  set (subseqs D)"
          "C = constr2 Di@C'"
          "C'  set (tr'pc S [dD. d  set Di])"
        using "6.prems"(1) unfolding constr2_def by atomize_elim auto
      
      have 0: "set [dD. d  set Di]  set D"
              "setopslsst S  setopslsst ((i, delete⟨t,s)#S)"
        by (auto simp add: setopslsst_def)
      hence 1:
          "(j, p)  setopslsst S  set [dD. d  set Di].
           (k, q)  setopslsst S  set [dD. d  set Di].
            p = q  j = k"
        using "6.prems"(2) by blast
  
      have "(i,p)  set D  set Di. (j,q)  set D  set Di. p = q  i = j"
        using "6.prems"(2) subseqs_set_subset(1)[OF C'(1)] by blast
      hence 2: "unlabel [dD. d  set Di] = [dunlabel D. d  set (unlabel Di)]"
        using unlabel_filter_eq[of D "set Di"] unfolding unlabel_def by simp
  
      have 3:
          "f g::('a × 'a  'c). A B::(('b × 'a × 'a) list).
              map snd ((map (λd. (i, f (snd d))) A)@(map (λd. (i, g (snd d))) B)) =
              map f (map snd A)@map g (map snd B)"
        by simp
      have "unlabel (constr2 Di) = constr1 (unlabel Di)"
        using 2 3[of ?f1 Di ?g1 "[dD. d  set Di]"]
        by (simp add: constr1_def constr2_def unlabel_def)
      hence 4: "unlabel C = constr1 (unlabel Di)@unlabel C'"
        using C'(2) unlabel_append by metis
  
      have "unlabel Di  set (map unlabel (subseqs D))"
        using C'(1) unfolding unlabel_def by simp
      hence 5: "unlabel Di  set (subseqs (unlabel D))"
        using map_subseqs[of snd D] unfolding unlabel_def by simp
  
      show ?case using "6.IH"[OF C'(1,3) 1] 2 4 5 unfolding constr1_def by auto
    next
      case (7 i ac t s S D)
      obtain C' d  where C':
          "C = (i,ac: (pair (t,s))  (pair (snd d))st)#C'"
          "C'  set (tr'pc S D)" "d  set D"
        using "7.prems"(1) by atomize_elim force
  
      have "setopslsst S  set D  setopslsst ((i,InSet ac t s)#S)  set D"
        by (auto simp add: setopslsst_def)
      hence "(j, p)  setopslsst S  set D.
             (k, q)  setopslsst S  set D.
              p = q  j = k"
        using "7.prems"(2) by blast
      hence "unlabel C'  set (tr (unlabel S) (unlabel D))" using "7.IH"[OF C'(2)] by auto
      thus ?case using C' unfolding unlabel_def by force
    next
      case (8 i X F F' S D)
      obtain C' where C':
          "C = map (λG. (i,X⟨∨≠: (F@G)st)) (trpairs F' (map snd D))@C'"
          "C'  set (tr'pc S D)"
        using "8.prems"(1) by atomize_elim auto
  
      have "setopslsst S  set D  setopslsst ((i,NegChecks X F F')#S)  set D"
        by (auto simp add: setopslsst_def)
      hence "(j, p)  setopslsst S  set D.
             (k, q)  setopslsst S  set D.
              p = q  j = k"
        using "8.prems"(2) by blast
      hence "unlabel C'  set (tr (unlabel S) (unlabel D))" using "8.IH"[OF C'(2)] by auto
      thus ?case using C' unfolding unlabel_def by auto
    qed (auto simp add: setopslsst_def)
  } thus "?A  ?B" by blast

  show "?B  ?A" using assms
  proof (induction A arbitrary: B D)
    case (Cons a A)
    obtain ia sa where a: "a = (ia,sa)" by atomize_elim auto

    have "setopslsst A  setopslsst (a#A)" using a by (cases sa) (auto simp add: setopslsst_def)
    hence 1: "(j, p)  setopslsst A  set D.
              (k, q)  setopslsst A  set D.
                p = q  j = k"
      using Cons.prems(2) by blast

    show ?case
    proof (cases sa)
      case (Send t)
      then obtain B' where B':
          "B = send⟨tst#B'"
          "B'  set (tr (unlabel A) (unlabel D))"
        using Cons.prems(1) a by auto
      thus ?thesis using Cons.IH[OF B'(2) 1] a B'(1) Send by auto
    next
      case (Receive t)
      then obtain B' where B':
          "B = receive⟨tst#B'"
          "B'  set (tr (unlabel A) (unlabel D))"
        using Cons.prems(1) a by auto
      thus ?thesis using Cons.IH[OF B'(2) 1] a B'(1) Receive by auto
    next
      case (Equality ac t t')
      then obtain B' where B':
          "B = ac: t  t'st#B'"
          "B'  set (tr (unlabel A) (unlabel D))"
        using Cons.prems(1) a by auto
      thus ?thesis using Cons.IH[OF B'(2) 1] a B'(1) Equality by auto
    next
      case (Insert t s)
      hence B: "B  set (tr (unlabel A) (List.insert (t,s) (unlabel D)))"
        using Cons.prems(1) a by auto

      let ?P = "λi. List.insert (t,s) (unlabel D) = unlabel (List.insert (i,t,s) D)"

      { obtain j where j: "?P j" "j = ia  (j,t,s)  set D"
          using labeled_list_insert_eq_ex_cases[of "(t,s)" D ia] by atomize_elim auto
        hence "j = ia" using Cons.prems(2) a Insert by (auto simp add: setopslsst_def)
        hence "?P ia" using j(1) by metis
      } hence j: "?P ia" by metis
      
      have 2: "(k1, p)  setopslsst A  set (List.insert (ia,t,s) D).
               (k2, q)  setopslsst A  set (List.insert (ia,t,s) D).
                 p = q  k1 = k2"
        using Cons.prems(2) a Insert by (auto simp add: setopslsst_def)

      show ?thesis using Cons.IH[OF _ 2] j(1) B Insert a by auto
    next
      case (Delete t s)
      define c where "c  (λ(i::'lbl strand_label) Di.
        map (λd. (i,check: (pair (t,s))  (pair (snd d))st)) Di@
        map (λd. (i,[]⟨∨≠: [(pair (t,s), pair (snd d))]st)) [dD. d  set Di])"
      
      define d where "d  (λDi.
        map (λd. check: (pair (t,s))  (pair d)st) Di@
        map (λd. []⟨∨≠: [(pair (t,s), pair d)]st) [dunlabel D. d  set Di])"

      obtain B' Di where B':
          "B = d Di@B'" "Di  set (subseqs (unlabel D))"
          "B'  set (tr (unlabel A) [dunlabel D. d  set Di])"
        using Cons.prems(1) a Delete unfolding d_def by auto

      obtain Di' where Di': "Di'  set (subseqs D)" "unlabel Di' = Di"
        using unlabel_subseqsD[OF B'(2)] by atomize_elim auto

      have 2: "(j, p)  setopslsst A  set [dD. d  set Di'].
               (k, q)  setopslsst A  set [dD. d  set Di'].
                 p = q  j = k"
        using 1 subseqs_subset[OF Di'(1)]
              filter_is_subset[of "λd. d  set Di'"]
        by blast

      have "set Di'  set D" by (rule subseqs_subset[OF Di'(1)])
      hence "(j, p)set D  set Di'. (k, q)set D  set Di'. p = q  j = k"
        using Cons.prems(2) by blast
      hence 3: "[dunlabel D. d  set Di] = unlabel [dD. d  set Di']"
        using Di'(2) unlabel_filter_eq[of D "set Di'"] unfolding unlabel_def by auto
      
      obtain C where C: "C  set (tr'pc A [dD. d  set Di'])" "B' = unlabel C"
        using 3 Cons.IH[OF _ 2] B'(3) by auto
      hence 4: "c ia Di'@C  set (tr'pc (a#A) D)" using Di'(1) a Delete unfolding c_def by auto

      have "unlabel (c ia Di') = d Di" using Di' 3 unfolding c_def d_def unlabel_def by auto
      hence 5: "B = unlabel (c ia Di'@C)" using B'(1) C(2) unlabel_append[of "c ia Di'" C] by simp
      
      show ?thesis using 4 5 by blast
    next
      case (InSet ac t s)
      then obtain B' d where B':
          "B = ac: (pair (t,s))  (pair d)st#B'"
          "B'  set (tr (unlabel A) (unlabel D))"
          "d  set (unlabel D)"
        using Cons.prems(1) a by auto
      thus ?thesis using Cons.IH[OF _ 1] a InSet unfolding unlabel_def by auto
    next
      case (NegChecks X F F')
      then obtain B' where B': 
          "B = map (λG. X⟨∨≠: (F@G)st) (trpairs F' (unlabel D))@B'"
          "B'  set (tr (unlabel A) (unlabel D))"
        using Cons.prems(1) a by auto
      thus ?thesis using Cons.IH[OF _ 1] a NegChecks unfolding unlabel_def by auto
    qed
  qed simp
qed

subsubsection ‹Part 2›
private lemma tr_par_iff_tr'_par:
  assumes "(i,p)  setopslsst A  set D. (j,q)  setopslsst A  set D.
            (δ. Unifier δ (pair p) (pair q))  i = j"
    (is "?R3 A D")
  and "(l,t,s)  set D. (fv t  fv s)  bvarssst (unlabel A) = {}" (is "?R4 A D")
  and "fvsst (unlabel A)  bvarssst (unlabel A) = {}" (is "?R5 A D")
  shows "(B  set (trpc A D). M; unlabel Bd )  (C  set (tr'pc A D). M; unlabel Cd )"
    (is "?P  ?Q")
proof
  { fix B assume "B  set (trpc A D)" "M; unlabel Bd "
    hence ?Q using assms
    proof (induction A D arbitrary: B M rule: trpc.induct)
      case (1 D) thus ?case by simp
    next
      case (2 i ts S D)
      note prems = "2.prems"
      note IH = "2.IH"

      obtain B' where B': "B = (i,send⟨tsst)#B'" "B'  set (trpc S D)"
        using prems(1) by atomize_elim auto
          
      have 1: "M; unlabel B'd " using prems(2) B'(1) by simp
      have 4: "?R3 S D" using prems(3) by (auto simp add: setopslsst_def)
      have 5: "?R4 S D" using prems(4) by force
      have 6: "?R5 S D" using prems(5) by force

      have 7: "t  set ts. M  t  " using prems(2) B'(1) by simp

      obtain C where C: "C  set (tr'pc S D)" "M; unlabel Cd "
        using IH[OF B'(2) 1 4 5 6] by atomize_elim auto
      hence "((i,send⟨tsst)#C)  set (tr'pc ((i,Send ts)#S) D)" "M; unlabel ((i,send⟨tsst)#C)d "
        using 7 by auto
      thus ?case by metis
    next
      case (3 i ts S D)
      note prems = "3.prems"
      note IH = "3.IH"

      obtain B' where B': "B = (i,receive⟨tsst)#B'" "B'  set (trpc S D)" using prems(1) by atomize_elim auto
          
      have 1: "(set ts set )  M; unlabel B'd  " using prems(2) B'(1) by simp
      have 4: "?R3 S D" using prems(3) by (auto simp add: setopslsst_def)
      have 5: "?R4 S D" using prems(4) by force
      have 6: "?R5 S D" using prems(5) by force

      obtain C where C: "C  set (tr'pc S D)" "(set ts set )  M; unlabel Cd "
        using IH[OF B'(2) 1 4 5 6] by atomize_elim auto
      hence "((i,receive⟨tsst)#C)  set (tr'pc ((i,receive⟨ts)#S) D)"
            "(set ts set )  M; unlabel ((i,receive⟨tsst)#C)d "
        by auto
      thus ?case by auto
    next
      case (4 i ac t t' S D)
      note prems = "4.prems"
      note IH = "4.IH"

      obtain B' where B': "B = (i,ac: t  t'st)#B'" "B'  set (trpc S D)"
        using prems(1) by atomize_elim auto
          
      have 1: "M; unlabel B'd  " using prems(2) B'(1) by simp
      have 4: "?R3 S D" using prems(3) by (auto simp add: setopslsst_def)
      have 5: "?R4 S D" using prems(4) by force
      have 6: "?R5 S D" using prems(5) by force

      have 7: "t   = t'  " using prems(2) B'(1) by simp

      obtain C where C: "C  set (tr'pc S D)" "M; unlabel Cd "
        using IH[OF B'(2) 1 4 5 6] by atomize_elim auto
      hence "((i,ac: t  t'st)#C)  set (tr'pc ((i,Equality ac t t')#S) D)"
            "M; unlabel ((i,ac: t  t'st)#C)d "
        using 7 by auto
      thus ?case by metis
    next
      case (5 i t s S D)
      note prems = "5.prems"
      note IH = "5.IH"

      have B: "B  set (trpc S (List.insert (i,t,s) D))" using prems(1) by simp
          
      have 1: "M; unlabel Bd  " using prems(2) B(1) by simp
      have 4: "?R3 S (List.insert (i,t,s) D)" using prems(3) by (auto simp add: setopslsst_def)
      have 5: "?R4 S (List.insert (i,t,s) D)" using prems(4,5) by force
      have 6: "?R5 S D" using prems(5) by force

      show ?case using IH[OF B(1) 1 4 5 6] by simp
    next
      case (6 i t s S D)
      note prems = "6.prems"
      note IH = "6.IH"

      let ?cl1 = "λDi. map (λd. (i,check: (pair (t,s))  (pair (snd d))st)) Di"
      let ?cu1 = "λDi. map (λd. check: (pair (t,s))  (pair (snd d))st) Di"
      let ?cl2 = "λDi. map (λd. (i,[]⟨∨≠: [(pair (t,s), pair (snd d))]st)) [ddbproj i D. dset Di]"
      let ?cu2 = "λDi. map (λd. []⟨∨≠: [(pair (t,s), pair (snd d))]st) [ddbproj i D. dset Di]"

      let ?dl1 = "λDi. map (λd. (i,check: (pair (t,s))  (pair (snd d))st)) Di"
      let ?du1 = "λDi. map (λd. check: (pair (t,s))  (pair (snd d))st) Di"
      let ?dl2 = "λDi. map (λd. (i,[]⟨∨≠: [(pair (t,s), pair (snd d))]st)) [dD. dset Di]"
      let ?du2 = "λDi. map (λd. []⟨∨≠: [(pair (t,s), pair (snd d))]st) [dD. dset Di]"

      define c where c: "c = (λDi. ?cl1 Di@?cl2 Di)"
      define d where d: "d = (λDi. ?dl1 Di@?dl2 Di)"

      obtain B' Di where B':
          "Di  set (subseqs (dbproj i D))" "B = c Di@B'" "B'  set (trpc S [dD. d  set Di])"
        using prems(1) c by atomize_elim auto

      have 0: "ikst (unlabel (c Di)) = {}" "ikst (unlabel (d Di)) = {}"
              "unlabel (?cl1 Di) = ?cu1 Di" "unlabel (?cl2 Di) = ?cu2 Di"
              "unlabel (?dl1 Di) = ?du1 Di" "unlabel (?dl2 Di) = ?du2 Di"
        unfolding c d unlabel_def by force+

      have 1: "M; unlabel B'd  " using prems(2) B'(2) 0(1) unfolding unlabel_def by auto

      { fix j p k q
        assume "(j, p)  setopslsst S  set [dD. d  set Di]"
               "(k, q)  setopslsst S  set [dD. d  set Di]"
        hence "(j, p)  setopslsst ((i, delete⟨t,s)#S)  set D"
              "(k, q)  setopslsst ((i, delete⟨t,s)#S)  set D"
          using dbproj_subseq_subset[OF B'(1)] by (auto simp add: setopslsst_def)
        hence "(δ. Unifier δ (pair p) (pair q))  j = k" using prems(3) by blast
      } hence 4: "?R3 S [dD. d  set Di]" by blast
      
      have 5: "?R4 S (filter (λd. d  set Di) D)" using prems(4) by force
      have 6: "?R5 S D" using prems(5) by force

      obtain C where C: "C  set (tr'pc S [dD . d  set Di])" "M; unlabel Cd "
        using IH[OF B'(1,3) 1 4 5 6] by atomize_elim auto

      have 7: "M; unlabel (c Di)d " "M; unlabel B'd "
        using prems(2) B'(2) 0(1) strand_sem_split(3,4)[of M "unlabel (c Di)" "unlabel B'"]
        unfolding c unlabel_def by auto

      have "M; unlabel (?cl2 Di)d " using 7(1) 0(1) unfolding c unlabel_def by auto 
      hence "M; ?cu2 Did " by (metis 0(4))
      moreover {
        fix j p k q
        assume "(j, p)  {(i, t, s)}  set D  set Di"
               "(k, q)  {(i, t, s)}  set D  set Di"
        hence "(j, p)  setopslsst ((i, delete⟨t,s)#S)  set D"
              "(k, q)  setopslsst ((i, delete⟨t,s)#S)  set D"
          using dbproj_subseq_subset[OF B'(1)] by (auto simp add: setopslsst_def)
        hence "(δ. Unifier δ (pair p) (pair q))  j = k" using prems(3) by blast
      } hence "(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"
        by blast
      ultimately have "M; ?du2 Did " using labeled_sat_ineq_lift by simp
      hence "M; unlabel (?dl2 Di)d " by (metis 0(6))
      moreover have "M; unlabel (?cl1 Di)d " using 7(1) unfolding c unlabel_def by auto
      hence "M; unlabel (?dl1 Di)d " by (metis 0(3,5))
      ultimately have "M; unlabel (d Di)d " using 0(2) unfolding c d unlabel_def by force
      hence 8: "M; unlabel (d Di@C)d " using 0(2) C(2) unfolding unlabel_def by auto

      have 9: "d Di@C  set (tr'pc ((i,delete⟨t,s)#S) D)"
        using C(1) dbproj_subseq_in_subseqs[OF B'(1)]
        unfolding d unlabel_def by auto

      show ?case by (metis 8 9)
    next
      case (7 i ac t s S D)
      note prems = "7.prems"
      note IH = "7.IH"

      obtain B' d where B':
          "B = (i,ac: (pair (t,s))  (pair (snd d))st)#B'"
          "B'  set (trpc S D)" "d  set (dbproj i D)"
        using prems(1) by atomize_elim force

      have 1: "M; unlabel B'd  " using prems(2) B'(1) by simp

      { fix j p k q
        assume "(j,p)  setopslsst S  set D"
               "(k,q)  setopslsst S  set D"
        hence "(j,p)  setopslsst ((i, InSet ac t s)#S)  set D"
              "(k,q)  setopslsst ((i, InSet ac t s)#S)  set D"
          by (auto simp add: setopslsst_def)
        hence "(δ. Unifier δ (pair p) (pair q))  j = k" using prems(3) by blast
      } hence 4: "?R3 S D" by blast

      have 5: "?R4 S D" using prems(4) by force
      have 6: "?R5 S D" using prems(5) by force
      have 7: "pair (t,s)   = pair (snd d)  " using prems(2) B'(1) by simp

      obtain C where C: "C  set (tr'pc S D)" "M; unlabel Cd "
        using IH[OF B'(2) 1 4 5 6] by atomize_elim auto
      hence "((i,ac: (pair (t,s))  (pair (snd d))st)#C)  set (tr'pc ((i,InSet ac t s)#S) D)"
            "M; unlabel ((i,ac: (pair (t,s))  (pair (snd d))st)#C)d "
        using 7 B'(3) unfolding dbproj_def by auto
      thus ?case by metis
    next
      case (8 i X F F' S D)
      note prems = "8.prems"
      note IH = "8.IH"

      let ?cl = "map (λG. (i,X⟨∨≠: (F@G)st)) (trpairs F' (map snd (dbproj i D)))"
      let ?cu = "map (λG. X⟨∨≠: (F@G)st) (trpairs F' (map snd (dbproj i D)))"

      let ?dl = "map (λG. (i,X⟨∨≠: (F@G)st)) (trpairs F' (map snd D))"
      let ?du = "map (λG. X⟨∨≠: (F@G)st) (trpairs F' (map snd D))"

      define c where c: "c = ?cl"
      define d where d: "d = ?dl"

      obtain B' where B': "B = c@B'" "B'  set (trpc S D)" using prems(1) c by atomize_elim auto

      have 0: "ikst (unlabel c) = {}" "ikst (unlabel d) = {}"
              "unlabel ?cl = ?cu" "unlabel ?dl = ?du" 
        unfolding c d unlabel_def by force+

      have "ikst (unlabel c) = {}" unfolding c unlabel_def by force
      hence 1: "M; unlabel B'd  " using prems(2) B'(1) unfolding unlabel_def by auto

      have "setopslsst S  setopslsst ((i, NegChecks X F F')#S)" by (auto simp add: setopslsst_def)
      hence 4: "?R3 S D" using prems(3) by blast

      have 5: "?R4 S D" using prems(4) by force
      have 6: "?R5 S D" using prems(5) by force

      obtain C where C: "C  set (tr'pc S D)" "M; unlabel Cd "
        using IH[OF B'(2) 1 4 5 6] by atomize_elim auto

      have 7: "M; unlabel cd " "M; unlabel B'd "
        using prems(2) B'(1) 0(1) strand_sem_split(3,4)[of M "unlabel c" "unlabel B'"]
        unfolding c unlabel_def by auto

      have 8: "d@C  set (tr'pc ((i,NegChecks X F F')#S) D)"
        using C(1) unfolding d unlabel_def by auto

      have "M; unlabel ?cld " using 7(1) unfolding c unlabel_def by auto 
      hence "M; ?cud " by (metis 0(3))
      moreover {
        fix j p k q
        assume "(j, p)  ((λ(t,s). (i,t,s)) ` set F')  set D"
               "(k, q)  ((λ(t,s). (i,t,s)) ` set F')  set D"
        hence "(j, p)  setopslsst ((i, NegChecks X F F')#S)  set D"
              "(k, q)  setopslsst ((i, NegChecks X F F')#S)  set D"
          by (auto simp add: setopslsst_def)
        hence "(δ. Unifier δ (pair p) (pair q))  j = k" using prems(3) by blast
      } hence "(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"
        by blast
      moreover have "fvpairs (map snd D)  set X = {}"
        using prems(4) by fastforce
      ultimately have "M; ?dud " using labeled_sat_ineq_dbproj_sem_equiv[of i] by simp
      hence "M; unlabel ?dld " by (metis 0(4))
      hence "M; unlabel dd " using 0(2) unfolding c d unlabel_def by force
      hence 9: "M; unlabel (d@C)d " using 0(2) C(2) unfolding unlabel_def by auto

      show ?case by (metis 8 9)
    qed
  } thus "?P  ?Q" by metis

  { fix C assume "C  set (tr'pc A D)" "M; unlabel Cd "
    hence ?P using assms
    proof (induction A D arbitrary: C M rule: tr'pc.induct)
      case (1 D) thus ?case by simp
    next
      case (2 i ts S D)
      note prems = "2.prems"
      note IH = "2.IH"

      obtain C' where C': "C = (i,send⟨tsst)#C'" "C'  set (tr'pc S D)"
        using prems(1) by atomize_elim auto
          
      have 1: "M; unlabel C'd  " using prems(2) C'(1) by simp
      have 4: "?R3 S D" using prems(3) by (auto simp add: setopslsst_def)
      have 5: "?R4 S D" using prems(4) by force
      have 6: "?R5 S D" using prems(5) by force

      have 7: "t  set ts. M  t  " using prems(2) C'(1) by simp

      obtain B where B: "B  set (trpc S D)" "M; unlabel Bd "
        using IH[OF C'(2) 1 4 5 6] by atomize_elim auto
      hence "((i,send⟨tsst)#B)  set (trpc ((i,Send ts)#S) D)"
            "M; unlabel ((i,send⟨tsst)#B)d "
        using 7 by auto
      thus ?case by metis
    next
      case (3 i ts S D)
      note prems = "3.prems"
      note IH = "3.IH"

      obtain C' where C': "C = (i,receive⟨tsst)#C'" "C'  set (tr'pc S D)"
        using prems(1) by atomize_elim auto
          
      have 1: "(set ts set )  M; unlabel C'd  " using prems(2) C'(1) by simp
      have 4: "?R3 S D" using prems(3) by (auto simp add: setopslsst_def)
      have 5: "?R4 S D" using prems(4) by force
      have 6: "?R5 S D" using prems(5) by force

      obtain B where B: "B  set (trpc S D)" "(set ts set )  M; unlabel Bd "
        using IH[OF C'(2) 1 4 5 6] by atomize_elim auto
      hence "((i,receive⟨tsst)#B)  set (trpc ((i,receive⟨ts)#S) D)"
            "(set ts set )  M; unlabel ((i,receive⟨tsst)#B)d "
        by auto
      thus ?case by auto
    next
      case (4 i ac t t' S D)
      note prems = "4.prems"
      note IH = "4.IH"

      obtain C' where C': "C = (i,ac: t  t'st)#C'" "C'  set (tr'pc S D)"
        using prems(1) by atomize_elim auto
          
      have 1: "M; unlabel C'd  " using prems(2) C'(1) by simp
      have 4: "?R3 S D" using prems(3) by (auto simp add: setopslsst_def)
      have 5: "?R4 S D" using prems(4) by force
      have 6: "?R5 S D" using prems(5) by force

      have 7: "t   = t'  " using prems(2) C'(1) by simp

      obtain B where B: "B  set (trpc S D)" "M; unlabel Bd "
        using IH[OF C'(2) 1 4 5 6] by atomize_elim auto
      hence "((i,ac: t  t'st)#B)  set (trpc ((i,Equality ac t t')#S) D)"
            "M; unlabel ((i,ac: t  t'st)#B)d "
        using 7 by auto
      thus ?case by metis
    next
      case (5 i t s S D)
      note prems = "5.prems"
      note IH = "5.IH"

      have C: "C  set (tr'pc S (List.insert (i,t,s) D))" using prems(1) by simp
          
      have 1: "M; unlabel Cd  " using prems(2) C(1) by simp
      have 4: "?R3 S (List.insert (i,t,s) D)" using prems(3) by (auto simp add: setopslsst_def)
      have 5: "?R4 S (List.insert (i,t,s) D)" using prems(4,5) by force
      have 6: "?R5 S (List.insert (i,t,s) D)" using prems(5) by force

      show ?case using IH[OF C(1) 1 4 5 6] by simp
    next
      case (6 i t s S D)
      note prems = "6.prems"
      note IH = "6.IH"

      let ?dl1 = "λDi. map (λd. (i,check: (pair (t,s))  (pair (snd d))st)) Di"
      let ?du1 = "λDi. map (λd. check: (pair (t,s))  (pair (snd d))st) Di"
      let ?dl2 = "λDi. map (λd. (i,[]⟨∨≠: [(pair (t,s), pair (snd d))]st)) [ddbproj i D. dset Di]"
      let ?du2 = "λDi. map (λd. []⟨∨≠: [(pair (t,s), pair (snd d))]st) [ddbproj i D. dset Di]"

      let ?cl1 = "λDi. map (λd. (i,check: (pair (t,s))  (pair (snd d))st)) Di"
      let ?cu1 = "λDi. map (λd. check: (pair (t,s))  (pair (snd d))st) Di"
      let ?cl2 = "λDi. map (λd. (i,[]⟨∨≠: [(pair (t,s), pair (snd d))]st)) [dD. dset Di]"
      let ?cu2 = "λDi. map (λd. []⟨∨≠: [(pair (t,s), pair (snd d))]st) [dD. dset Di]"

      define c where c: "c = (λDi. ?cl1 Di@?cl2 Di)"
      define d where d: "d = (λDi. ?dl1 Di@?dl2 Di)"

      obtain C' Di where C':
          "Di  set (subseqs D)" "C = c Di@C'" "C'  set (tr'pc S [dD. d  set Di])"
        using prems(1) c by atomize_elim auto

      have 0: "ikst (unlabel (c Di)) = {}" "ikst (unlabel (d Di)) = {}"
              "unlabel (?cl1 Di) = ?cu1 Di" "unlabel (?cl2 Di) = ?cu2 Di"
              "unlabel (?dl1 Di) = ?du1 Di" "unlabel (?dl2 Di) = ?du2 Di"
        unfolding c d unlabel_def by force+

      have 1: "M; unlabel C'd  " using prems(2) C'(2) 0(1) unfolding unlabel_def by auto

      { fix j p k q
        assume "(j, p)  setopslsst S  set [dD. d  set Di]"
               "(k, q)  setopslsst S  set [dD. d  set Di]"
        hence "(j, p)  setopslsst ((i, delete⟨t,s)#S)  set D"
              "(k, q)  setopslsst ((i, delete⟨t,s)#S)  set D"
          by (auto simp add: setopslsst_def)
        hence "(δ. Unifier δ (pair p) (pair q))  j = k" using prems(3) by blast
      } hence 4: "?R3 S [dD. d  set Di]" by blast

      have 5: "?R4 S (filter (λd. d  set Di) D)" using prems(4) by force
      have 6: "?R5 S D" using prems(5) by force

      obtain B where B: "B  set (trpc S [dD. d  set Di])" "M; unlabel Bd "
        using IH[OF C'(1,3) 1 4 5 6] by atomize_elim auto

      have 7: "M; unlabel (c Di)d " "M; unlabel C'd "
        using prems(2) C'(2) 0(1) strand_sem_split(3,4)[of M "unlabel (c Di)" "unlabel C'"]
        unfolding c unlabel_def by auto

      { fix j p k q
        assume "(j, p)  {(i, t, s)}  set D"
               "(k, q)  {(i, t, s)}  set D"
        hence "(j, p)  setopslsst ((i, delete⟨t,s)#S)  set D"
              "(k, q)  setopslsst ((i, delete⟨t,s)#S)  set D"
          by (auto simp add: setopslsst_def)
        hence "(δ. Unifier δ (pair p) (pair q))  j = k" using prems(3) by blast
      } hence "(j, p)  {(i, t, s)}  set D.
               (k, q)  {(i, t, s)}  set D.
                (δ. Unifier δ (pair p) (pair q))  j = k"
        by blast
      moreover have "M; unlabel (?cl1 Di)d " using 7(1) unfolding c unlabel_append by auto 
      hence "M; ?cu1 Did " by (metis 0(3))
      ultimately have *: "Di  set (subseqs (dbproj i D))"
        using labeled_sat_eqs_subseqs[OF C'(1)] by simp
      hence 8: "d Di@B  set (trpc ((i,delete⟨t,s)#S) D)"
        using B(1) unfolding d unlabel_def by auto

      have "M; unlabel (?cl2 Di)d " using 7(1) 0(1) unfolding c unlabel_def by auto 
      hence "M; ?cu2 Did " by (metis 0(4))
      hence "M; ?du2 Did " by (metis labeled_sat_ineq_dbproj)
      hence "M; unlabel (?dl2 Di)d " by (metis 0(6))
      moreover have "M; unlabel (?cl1 Di)d " using 7(1) unfolding c unlabel_def by auto 
      hence "M; unlabel (?dl1 Di)d " by (metis 0(3,5))
      ultimately have "M; unlabel (d Di)d " using 0(2) unfolding c d unlabel_def by force
      hence 9: "M; unlabel (d Di@B)d " using 0(2) B(2) unfolding unlabel_def by auto

      show ?case by (metis 8 9)
    next
      case (7 i ac t s S D)
      note prems = "7.prems"
      note IH = "7.IH"

      obtain C' d where C':
          "C = (i,ac: (pair (t,s))  (pair (snd d))st)#C'"
          "C'  set (tr'pc S D)" "d  set D"
        using prems(1) by atomize_elim force
          
      have 1: "M; unlabel C'd  " using prems(2) C'(1) by simp

      { fix j p k q
        assume "(j,p)  setopslsst S  set D"
               "(k,q)  setopslsst S  set D"
        hence "(j,p)  setopslsst ((i, InSet ac t s)#S)  set D"
              "(k,q)  setopslsst ((i, InSet ac t s)#S)  set D"
          by (auto simp add: setopslsst_def)
        hence "(δ. Unifier δ (pair p) (pair q))  j = k" using prems(3) by blast
      } hence 4: "?R3 S D" by blast

      have 5: "?R4 S D" using prems(4) by force
      have 6: "?R5 S D" using prems(5) by force

      obtain B where B: "B  set (trpc S D)" "M; unlabel Bd "
        using IH[OF C'(2) 1 4 5 6] by atomize_elim auto

      have 7: "pair (t,s)   = pair (snd d)  " using prems(2) C'(1) by simp

      have "(i,t,s)  setopslsst ((i, InSet ac t s)#S)  set D"
           "(fst d, snd d)  setopslsst ((i, InSet ac t s)#S)  set D"
        using C'(3) by (auto simp add: setopslsst_def)
      hence "δ. Unifier δ (pair (t,s)) (pair (snd d))  i = fst d"
        using prems(3) by blast
      hence "fst d = i" using 7 by auto
      hence 8: "d  set (dbproj i D)" using C'(3) unfolding dbproj_def by auto

      have 9: "((i,ac: (pair (t,s))  (pair (snd d))st)#B)  set (trpc ((i,InSet ac t s)#S) D)"
        using B 8 by auto
      have 10: "M; unlabel ((i,ac: (pair (t,s))  (pair (snd d))st)#B)d "
        using B 7 8 by auto

      show ?case by (metis 9 10)
    next
      case (8 i X F F' S D)
      note prems = "8.prems"
      note IH = "8.IH"

      let ?dl = "map (λG. (i,X⟨∨≠: (F@G)st)) (trpairs F' (map snd (dbproj i D)))"
      let ?du = "map (λG. X⟨∨≠: (F@G)st) (trpairs F' (map snd (dbproj i D)))"

      let ?cl = "map (λG. (i,X⟨∨≠: (F@G)st)) (trpairs F' (map snd D))"
      let ?cu = "map (λG. X⟨∨≠: (F@G)st) (trpairs F' (map snd D))"

      define c where c: "c = ?cl"
      define d where d: "d = ?dl"

      obtain C' where C': "C = c@C'" "C'  set (tr'pc S D)" using prems(1) c by atomize_elim auto

      have 0: "ikst (unlabel c) = {}" "ikst (unlabel d) = {}"
              "unlabel ?cl = ?cu" "unlabel ?dl = ?du" 
        unfolding c d unlabel_def by force+

      have "ikst (unlabel c) = {}" unfolding c unlabel_def by force
      hence 1: "M; unlabel C'd  " using prems(2) C'(1) unfolding unlabel_def by auto

      have "setopslsst S  setopslsst ((i, NegChecks X F F')#S)" by (auto simp add: setopslsst_def)
      hence 4: "?R3 S D" using prems(3) by blast

      have 5: "?R4 S D" using prems(4) by force
      have 6: "?R5 S D" using prems(5) by force

      obtain B where B: "B  set (trpc S D)" "M; unlabel Bd "
        using IH[OF C'(2) 1 4 5 6] by atomize_elim auto

      have 7: "M; unlabel cd " "M; unlabel C'd "
        using prems(2) C'(1) 0(1) strand_sem_split(3,4)[of M "unlabel c" "unlabel C'"]
        unfolding c unlabel_def by auto

      have 8: "d@B  set (trpc ((i,NegChecks X F F')#S) D)"
        using B(1) unfolding d unlabel_def by auto

      have "M; unlabel ?cld " using 7(1) unfolding c unlabel_def by auto 
      hence "M; ?cud " by (metis 0(3))
      moreover {
        fix j p k q
        assume "(j, p)  ((λ(t,s). (i,t,s)) ` set F')  set D"
               "(k, q)  ((λ(t,s). (i,t,s)) ` set F')  set D"
        hence "(j, p)  setopslsst ((i, NegChecks X F F')#S)  set D"
              "(k, q)  setopslsst ((i, NegChecks X F F')#S)  set D"
          by (auto simp add: setopslsst_def)
        hence "(δ. Unifier δ (pair p) (pair q))  j = k" using prems(3) by blast
      } hence "(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"
        by blast
      moreover have "fvpairs (map snd D)  set X = {}"
        using prems(4) by fastforce
      ultimately have "M; ?dud " using labeled_sat_ineq_dbproj_sem_equiv[of i] by simp
      hence "M; unlabel ?dld " by (metis 0(4))
      hence "M; unlabel dd " using 0(2) unfolding c d unlabel_def by force
      hence 9: "M; unlabel (d@B)d " using 0(2) B(2) unfolding unlabel_def by auto

      show ?case by (metis 8 9)
    qed
  } thus "?Q  ?P" by metis
qed


subsubsection ‹Part 3›
private lemma tr'_par_sem_equiv:
  assumes "(l,t,s)  set D. (fv t  fv s)  bvarssst (unlabel A) = {}"
  and "fvsst (unlabel A)  bvarssst (unlabel A) = {}" "ground M"
  and "(i,p)  setopslsst A  set D. (j,q)  setopslsst A  set D.
        (δ. Unifier δ (pair p) (pair q))  i = j" (is "?R A D")
  and : "interpretationsubst "
  shows "M; set (unlabel D) pset ; unlabel As   (B  set (tr'pc A D). M; unlabel Bd )"
        (is "?P  ?Q")
proof -
  have 1: "(t,s)  set (unlabel D). (fv t  fv s)  bvarssst (unlabel A) = {}"
    using assms(1) unfolding unlabel_def by force

  have 2: "(i,p)  setopslsst A  set D. (j,q)  setopslsst A  set D. p = q  i = j"
    using assms(4) subst_apply_term_empty by blast

  show ?thesis by (metis tr_sem_equiv'[OF 1 assms(2,3) ] tr'_par_iff_unlabel_tr[OF 2])
qed


subsubsection ‹Part 4›
lemma tr_par_sem_equiv:
  assumes "(l,t,s)  set D. (fv t  fv s)  bvarssst (unlabel A) = {}"
  and "fvsst (unlabel A)  bvarssst (unlabel A) = {}" "ground M"
  and "(i,p)  setopslsst A  set D. (j,q)  setopslsst A  set D.
        (δ. Unifier δ (pair p) (pair q))  i = j"
  and : "interpretationsubst "
  shows "M; set (unlabel D) pset ; unlabel As   (B  set (trpc A D). M; unlabel Bd )"
  (is "?P  ?Q")
using tr_par_iff_tr'_par[OF assms(4,1,2), of M ] tr'_par_sem_equiv[OF assms] by metis

end

end


subsection ‹Theorem: The Stateful Compositionality Result, on the Constraint Level›
theorem (in labeled_stateful_typed_model) par_comp_constr_stateful_typed:
  assumes 𝒜: "par_complsst 𝒜 Sec" "fvlsst 𝒜  bvarslsst 𝒜 = {}"
  and : " s unlabel 𝒜" "interpretationsubst " "wtsubst " "wftrms (subst_range )"
  shows "(n.  s proj_unl n 𝒜) 
         (𝒜' l' ts. prefix 𝒜' 𝒜  suffix [(l', receive⟨ts)] 𝒜'  (𝒜' leaks Sec under ))"
proof -
  let ?P = "λn A D.
       (i, p)  setopslsst (proj n A)  set D.
       (j, q)  setopslsst (proj n A)  set D.
          (δ. Unifier δ (pair p) (pair q))  i = j"

  have 1: "(l, t, t')set []. (fv t  fv t')  bvarssst (unlabel 𝒜) = {}"
          "fvsst (unlabel 𝒜)  bvarssst (unlabel 𝒜) = {}" "ground {}"
    using 𝒜(2) by simp_all

  have 2: "n. (l, t, t')set []. (fv t  fv t')  bvarssst (proj_unl n 𝒜) = {}"
          "n. fvsst (proj_unl n 𝒜)  bvarssst (proj_unl n 𝒜) = {}"
    using 1 sst_vars_proj_subset[of _ 𝒜] by fast+

  note 3 = par_complsst_proj[OF 𝒜(1)]

  have 4:
      "{}; set (unlabel []) pset ℐ'; unlabel 𝒜s ℐ' 
        (Bset (trpc 𝒜 []). {}; unlabel Bd ℐ')"
    when ℐ': "interpretationsubst ℐ'" for ℐ'
    using tr_par_sem_equiv[OF 1 _ ℐ'] 𝒜(1)
    unfolding par_complsst_def constr_sem_d_def by auto

  obtain 𝒜' where 𝒜': "𝒜'  set (trpc 𝒜 [])" "  unlabel 𝒜'"
    using 4[OF (2)] (1) unfolding constr_sem_d_def by atomize_elim auto

  have ℐ':
      "(n. (  proj_unl n 𝒜')) 
        (𝒜'' l' ts. prefix 𝒜'' 𝒜'  suffix [(l', receive⟨tsst)] 𝒜'' 
                    (strand_leakslst 𝒜'' Sec ))"
    using par_comp_constr_typed[OF tr_par_preserves_par_comp[OF 𝒜(1) 𝒜'(1)] 𝒜'(2) (2-)] by blast

  show ?thesis
  proof (cases "n. (  proj_unl n 𝒜')")
    case True
    { fix n assume "  proj_unl n 𝒜'"
      hence "{}; {}; unlabel (proj n 𝒜)s "
        using tr_par_proj[OF 𝒜'(1), of n]
              tr_par_sem_equiv[OF 2(1,2) 1(3) _ (2), of n] 3(1)
        unfolding par_complsst_def proj_def constr_sem_d_def by force
    } thus ?thesis using True (1,2,3) (1) by metis
  next
    case False
    then obtain 𝒜''::"('fun,'var,'lbl) labeled_strand" where 𝒜'':
        "prefix 𝒜'' 𝒜'" "strand_leakslst 𝒜'' Sec "
      using ℐ' by blast
    
    have "t  Sec - declassifiedlst 𝒜'' . l.
            (  unlabel (proj l 𝒜''))  ikst (unlabel (proj l 𝒜'')) set   t  "
    proof -
      obtain s m where sm:
          "s  Sec - declassifiedlst 𝒜'' " "{}; proj_unl m 𝒜''@[send⟨[s]st]d "
        using 𝒜'' unfolding strand_leakslst_def constr_sem_d_def by blast

      show ?thesis using strand_sem_split(3,4)[OF sm(2)] sm(1) unfolding constr_sem_d_def by auto
    qed
    then obtain s m where sm:
        "s  Sec - declassifiedlst 𝒜'' "
        "  unlabel (proj m 𝒜'')"
        "ikst (unlabel (proj m 𝒜'')) set   s  "
      by atomize_elim auto
    hence s': "¬{} c s  " "s   = s"
      using 𝒜(1) subst_ground_ident[of s ] unfolding par_complsst_def by auto

    ― ‹
      We now need to show that there is some prefix B› of 𝒜''› that also leaks
      and where B ∈ set (tr C D)› for some prefix C› of 𝒜›
    obtain B::"('fun,'var,'lbl) labeled_strand"
        and C G::"('fun,'var,'lbl) labeled_stateful_strand"
      where BC:
        "prefix B 𝒜'" "prefix C 𝒜" "B  set (trpc C [])"
        "ikst (unlabel (proj m B)) set   s  "
        "prefix B 𝒜''" "l t. suffix ((l, receive⟨t)#G) C"
      and G: "list_all (Not  is_Receive  snd) G"
      using tr_leaking_prefix_exists[OF 𝒜'(1) 𝒜''(1) sm(3)]
            prefix_order.order_trans[OF _ 𝒜''(1)] s'
      by blast
    
    obtain C' where C': "C = C'@G" "l t. suffix [(l, receive⟨t)] C'"
      using BC(6) unfolding suffix_def by (metis append_Cons append_assoc append_self_conv2)

    have "{}; unlabel (proj m B)d "
      using sm(2) BC(5) unfolding prefix_def unlabel_def proj_def constr_sem_d_def by auto
    hence BC': "  proj_unl m B@[send⟨[s]st]"
      using BC(4) unfolding constr_sem_d_def by auto
    have BC'': "s  Sec - declassifiedlst B "
      using BC(5) sm(1) declassified_prefix_subset by auto

    have "n.  s (proj_unl n C'@[Send [s]])"
    proof -
      have 5: "par_complsst (proj n C) Sec" for n
        using 𝒜(1) BC(2) par_complsst_split(1)[THEN par_complsst_proj]
        unfolding prefix_def by auto

      have "fvsst (unlabel 𝒜)  bvarssst (unlabel 𝒜) = {}"
           "fvsst (unlabel C)  fvsst (unlabel 𝒜)"
           "bvarssst (unlabel C)  bvarssst (unlabel 𝒜)"
        using 𝒜(2) BC(2) sst_vars_append_subset(1,2)[of "unlabel C"]
        unfolding prefix_def unlabel_def by auto
      hence "fvsst (proj_unl n C)  bvarssst (proj_unl n C) = {}" for n
        using sst_vars_proj_subset[of _ C] sst_vars_proj_subset[of _ 𝒜]
        by blast
      hence 6:
          "(l, t, t')set []. (fv t  fv t')  bvarssst (proj_unl n C) = {}"
          "fvsst (proj_unl n C)  bvarssst (proj_unl n C) = {}"
          "ground {}"
        for n
      using 2 by auto

      have 7: "?P n C []" for n using 5 unfolding par_complsst_def by simp

      obtain n where n: " s proj_unl n C" "iksst (proj_unl n C) set   s  "
        using s'(2) tr_par_proj[OF BC(3), of m] BC'(1)
              tr_par_sem_equiv[OF 6 7 (2), of m]
              tr_par_deduct_iff[OF tr_par_proj(1)[OF BC(3)], of  m s]
        unfolding proj_def constr_sem_d_def by auto

      have "iksst (proj_unl n C) = iksst (proj_unl n C')"
        using C'(1) G unfolding iksst_def unlabel_def proj_def list_all_iff by fastforce
      hence 8: "iksst (proj_unl n C') set   s  " using n(2) by simp

      have 9: " s proj_unl n C'"
        using n(1) C'(1) strand_sem_append_stateful by simp

      show ?thesis using 8 9 strand_sem_append_stateful by auto
    qed
    moreover have "s  Sec - declassifiedlsst C " by (metis tr_par_declassified_eq BC(3) BC'')
    hence "s  Sec - declassifiedlsst C' "
      using ideduct_mono[of
              "{set ts |ts. ⟨⋆, receive⟨ts  set C'} set " _
              "{set ts |ts. ⟨⋆, receive⟨ts  set (C'@G)} set "]
      unfolding declassifiedlsst_alt_def C'(1) by auto
    moreover have "prefix C' 𝒜" using BC(2) C' unfolding prefix_def by auto
    ultimately show ?thesis using C'(2) unfolding strand_leakslsst_def by meson
  qed
qed

theorem (in labeled_stateful_typing) par_comp_constr_stateful:
  assumes 𝒜: "par_complsst 𝒜 Sec" "typing_condsst (unlabel 𝒜)"
  and : " s unlabel 𝒜" "interpretationsubst "
  shows "τ. interpretationsubst τ  wtsubst τ  wftrms (subst_range τ)  (τ s unlabel 𝒜) 
              ((n. τ s proj_unl n 𝒜) 
               (𝒜' l' ts. prefix 𝒜' 𝒜  suffix [(l', receive⟨ts)] 𝒜'  (𝒜' leaks Sec under τ)))"
proof -
  let ?P = "λn A D.
       (i, p)  setopslsst (proj n A)  set D.
       (j, q)  setopslsst (proj n A)  set D.
          (δ. Unifier δ (pair p) (pair q))  i = j"

  have 1: "(l, t, t')set []. (fv t  fv t')  bvarssst (unlabel 𝒜) = {}"
          "fvsst (unlabel 𝒜)  bvarssst (unlabel 𝒜) = {}" "ground {}"
    using 𝒜(2) unfolding typing_condsst_def by simp_all

  have 2: "n. (l, t, t')set []. (fv t  fv t')  bvarssst (proj_unl n 𝒜) = {}"
          "n. fvsst (proj_unl n 𝒜)  bvarssst (proj_unl n 𝒜) = {}"
    using 1(1,2) sst_vars_proj_subset[of _ 𝒜] by fast+

  have 3: "n. par_complsst (proj n 𝒜) Sec"
    using par_complsst_proj[OF 𝒜(1)] by metis

  have 4:
      "{}; set (unlabel []) pset ℐ'; unlabel 𝒜s ℐ' 
        (Bset (trpc 𝒜 []). {}; unlabel Bd ℐ')"
    when ℐ': "interpretationsubst ℐ'" for ℐ'
    using tr_par_sem_equiv[OF 1 _ ℐ'] 𝒜(1)
    unfolding par_complsst_def constr_sem_d_def by auto

  obtain 𝒜' where 𝒜': "𝒜'  set (trpc 𝒜 [])" "  unlabel 𝒜'"
    using 4[OF (2)] (1) unfolding constr_sem_d_def by atomize_elim auto

  obtain τ where τ:
      "interpretationsubst τ" "wtsubst τ" "wftrms (subst_range τ)" "τ  unlabel 𝒜'"
      "(n. (τ  proj_unl n 𝒜')) 
        (𝒜'' l' ts. prefix 𝒜'' 𝒜'  suffix [(l', receive⟨tsst)] 𝒜'' 
                    (strand_leakslst 𝒜'' Sec τ))"
    using par_comp_constr[OF tr_par_preserves_par_comp[OF 𝒜(1) 𝒜'(1)]
                             tr_par_preserves_typing_cond[OF 𝒜 𝒜'(1)]
                             𝒜'(2) (2)]
    by atomize_elim auto

  have τ': "τ s unlabel 𝒜" using 4[OF τ(1)] 𝒜'(1) τ(4) unfolding constr_sem_d_def by auto

  show ?thesis
  proof (cases "n. (τ  proj_unl n 𝒜')")
    case True
    { fix n assume "τ  proj_unl n 𝒜'"
      hence "{}; {}; unlabel (proj n 𝒜)s τ"
        using tr_par_proj[OF 𝒜'(1), of n]
              tr_par_sem_equiv[OF 2(1,2) 1(3) _ τ(1), of n] 3(1)
        unfolding par_complsst_def proj_def constr_sem_d_def by force
    } thus ?thesis using True τ(1,2,3) τ' by metis
  next
    case False
    then obtain 𝒜''::"('fun,'var,'lbl) labeled_strand" where 𝒜'':
        "prefix 𝒜'' 𝒜'" "strand_leakslst 𝒜'' Sec τ"
      using τ by blast
    moreover {
      fix ts l assume *: "{}; unlabel (proj l 𝒜'')@[send⟨tsst]d τ"
      have "τ  unlabel (proj l 𝒜'')"
           "t  set ts. ikst (unlabel (proj l 𝒜'')) set τ  t  τ"
        using strand_sem_split(3,4)[OF *] unfolding constr_sem_d_def by auto
    } ultimately have "t  Sec - declassifiedlst 𝒜'' τ. l.
            (τ  unlabel (proj l 𝒜''))  ikst (unlabel (proj l 𝒜'')) set τ  t  τ"
      unfolding strand_leakslst_def constr_sem_d_def by force
    then obtain s m where sm:
        "s  Sec - declassifiedlst 𝒜'' τ"
        "τ  unlabel (proj m 𝒜'')"
        "ikst (unlabel (proj m 𝒜'')) set τ  s  τ"
      by atomize_elim auto
    hence s': "¬{} c s  τ" "s  τ = s"
      using 𝒜(1) subst_ground_ident[of s τ] unfolding par_complsst_def by auto

    ― ‹
      We now need to show that there is some prefix B› of 𝒜''› that also leaks
      and where B ∈ set (tr C D)› for some prefix C› of 𝒜›
    obtain B::"('fun,'var,'lbl) labeled_strand"
        and C G::"('fun,'var,'lbl) labeled_stateful_strand"
      where BC:
        "prefix B 𝒜'" "prefix C 𝒜" "B  set (trpc C [])"
        "ikst (unlabel (proj m B)) set τ  s  τ"
        "prefix B 𝒜''" "l t. suffix ((l, receive⟨t)#G) C"
      and G: "list_all (Not  is_Receive  snd) G"
      using tr_leaking_prefix_exists[OF 𝒜'(1) 𝒜''(1) sm(3)]
            prefix_order.order_trans[OF _ 𝒜''(1)] s'
      by blast
    
    obtain C' where C': "C = C'@G" "l t. suffix [(l, receive⟨t)] C'"
      using BC(6) unfolding suffix_def by (metis append_Cons append_assoc append_self_conv2)

    have "{}; unlabel (proj m B)d τ"
      using sm(2) BC(5) unfolding prefix_def unlabel_def proj_def constr_sem_d_def by auto
    hence BC': "τ  proj_unl m B@[send⟨[s]st]"
      using BC(4) unfolding constr_sem_d_def by auto
    have BC'': "s  Sec - declassifiedlst B τ"
      using BC(5) sm(1) declassified_prefix_subset by auto

    have "n. τ s (proj_unl n C'@[Send [s]])"
    proof -
      have 5: "par_complsst (proj n C) Sec" for n
        using 𝒜(1) BC(2) par_complsst_split(1)[THEN par_complsst_proj]
        unfolding prefix_def by auto

      have "fvsst (unlabel 𝒜)  bvarssst (unlabel 𝒜) = {}"
           "fvsst (unlabel C)  fvsst (unlabel 𝒜)"
           "bvarssst (unlabel C)  bvarssst (unlabel 𝒜)"
        using 𝒜(2) BC(2) sst_vars_append_subset(1,2)[of "unlabel C"]
        unfolding typing_condsst_def prefix_def unlabel_def by auto
      hence "fvsst (proj_unl n C)  bvarssst (proj_unl n C) = {}" for n
        using sst_vars_proj_subset[of _ C] sst_vars_proj_subset[of _ 𝒜]
        by blast
      hence 6:
          "(l, t, t')set []. (fv t  fv t')  bvarssst (proj_unl n C) = {}"
          "fvsst (proj_unl n C)  bvarssst (proj_unl n C) = {}"
          "ground {}"
        for n
      using 2 by auto

      have 7: "?P n C []" for n using 5 unfolding par_complsst_def by simp

      obtain n where n: "τ s proj_unl n C" "iksst (proj_unl n C) set τ  s  τ"
        using s'(2) tr_par_proj[OF BC(3), of m] BC'(1)
              tr_par_sem_equiv[OF 6 7 τ(1), of m]
              tr_par_deduct_iff[OF tr_par_proj(1)[OF BC(3)], of τ m s]
        unfolding proj_def constr_sem_d_def by auto

      have "iksst (proj_unl n C) = iksst (proj_unl n C')"
        using C'(1) G unfolding iksst_def unlabel_def proj_def list_all_iff by fastforce
      hence 8: "iksst (proj_unl n C') set τ  s  τ" using n(2) by simp

      have 9: "τ s proj_unl n C'"
        using n(1) C'(1) strand_sem_append_stateful by simp

      show ?thesis using 8 9 strand_sem_append_stateful by auto
    qed
    moreover have "s  Sec - declassifiedlsst C τ" by (metis tr_par_declassified_eq BC(3) BC'')
    hence "s  Sec - declassifiedlsst C' τ"
      using ideduct_mono[of
              "{set ts |ts. ⟨⋆, receive⟨ts  set C'} set τ" _
              "{set ts |ts. ⟨⋆, receive⟨ts  set (C'@G)} set τ"]
      unfolding declassifiedlsst_alt_def C'(1) by auto
    moreover have "prefix C' 𝒜" using BC(2) C' unfolding prefix_def by auto
    ultimately show ?thesis
      using τ(1,2,3) τ' C'(2) unfolding strand_leakslsst_def by meson
  qed
qed


subsection ‹Theorem: The Stateful Compositionality Result, on the Protocol Level›
context labeled_stateful_typing
begin

context
begin

subsubsection ‹Definitions: Labeled Protocols›
text ‹
  We state our result on the level of protocol traces (i.e., the constraints reachable in a
  symbolic execution of the actual protocol). Hence, we do not need to convert protocol strands
  to intruder constraints in the following well-formedness definitions.
›
private definition wflsts::"('fun,'var,'lbl) labeled_strand set  bool" where
  "wflsts 𝒮  (𝒜  𝒮. wflst {} 𝒜)  (𝒜  𝒮. 𝒜'  𝒮. fvlst 𝒜  bvarslst 𝒜' = {})"

private definition wflsts'::
  "('fun,'var,'lbl) labeled_strand set  ('fun,'var,'lbl) labeled_strand  bool"
where
  "wflsts' 𝒮 𝒜  (𝒜'  𝒮. wfst (wfrestrictedvarslst 𝒜) (unlabel 𝒜')) 
                 (𝒜'  𝒮. 𝒜''  𝒮. fvlst 𝒜'  bvarslst 𝒜'' = {}) 
                 (𝒜'  𝒮. fvlst 𝒜'  bvarslst 𝒜 = {}) 
                 (𝒜'  𝒮. fvlst 𝒜  bvarslst 𝒜' = {})"

private definition typing_cond_prot where
  "typing_cond_prot 𝒫 
    wflsts 𝒫 
    tfrset ((trmslst ` 𝒫)) 
    wftrms ((trmslst ` 𝒫)) 
    (𝒜  𝒫. list_all tfrstp (unlabel 𝒜)) 
    Ana_invar_subst ((ikst ` unlabel ` 𝒫)  (assignment_rhsst ` unlabel ` 𝒫))"

private definition par_comp_prot where
  "par_comp_prot 𝒫 Sec 
    (l1 l2. l1  l2 
      GSMP_disjoint (𝒜  𝒫. trms_projlst l1 𝒜) (𝒜  𝒫. trms_projlst l2 𝒜) Sec) 
    ground Sec  (s  Sec. ¬{} c s) 
    typing_cond_prot 𝒫"


subsubsection ‹Lemmata: Labeled Protocols›
private lemma wflsts_eqs_wflsts': "wflsts S = wflsts' S []"
unfolding wflsts_def wflsts'_def unlabel_def by auto

private lemma par_comp_prot_impl_par_comp:
  assumes "par_comp_prot 𝒫 Sec" "𝒜  𝒫"
  shows "par_comp 𝒜 Sec"
proof -
  have *: "l1 l2. l1  l2 
              GSMP_disjoint (𝒜  𝒫. trms_projlst l1 𝒜) (𝒜  𝒫. trms_projlst l2 𝒜) Sec"
    using assms(1) unfolding par_comp_prot_def by metis
  { fix l1 l2::'lbl assume **: "l1  l2"
    hence ***: "GSMP_disjoint (𝒜  𝒫. trms_projlst l1 𝒜) (𝒜  𝒫. trms_projlst l2 𝒜) Sec"
      using * by auto
    have "GSMP_disjoint (trms_projlst l1 𝒜) (trms_projlst l2 𝒜) Sec"
      using GSMP_disjoint_subset[OF ***] assms(2) by auto
  } hence "l1 l2. l1  l2  GSMP_disjoint (trms_projlst l1 𝒜) (trms_projlst l2 𝒜) Sec" by metis
  thus ?thesis using assms unfolding par_comp_prot_def par_comp_def by metis
qed

private lemma typing_cond_prot_impl_typing_cond:
  assumes "typing_cond_prot 𝒫" "𝒜  𝒫"
  shows "typing_cond (unlabel 𝒜)"
proof -
  have 1: "wfst {} (unlabel 𝒜)" "fvlst 𝒜  bvarslst 𝒜 = {}"
    using assms unfolding typing_cond_prot_def wflsts_def by auto

  have "tfrset ((trmslst ` 𝒫))"
       "wftrms ((trmslst ` 𝒫))"
       "trmslst 𝒜  (trmslst ` 𝒫)"
       "SMP (trmslst 𝒜) - Var`𝒱  SMP ((trmslst ` 𝒫)) - Var`𝒱"
    using assms SMP_mono[of "trmslst 𝒜" "(trmslst ` 𝒫)"]
    unfolding typing_cond_prot_def
    by (metis, metis, auto)
  hence 2: "tfrset (trmslst 𝒜)" and 3: "wftrms (trmslst 𝒜)"
    unfolding tfrset_def by (meson subsetD)+

  have 4: "list_all tfrstp (unlabel 𝒜)" using assms unfolding typing_cond_prot_def by auto

  have "subtermsset (ikst (unlabel 𝒜)  assignment_rhsst (unlabel 𝒜)) 
        subtermsset ((ikst ` unlabel ` 𝒫)  (assignment_rhsst ` unlabel ` 𝒫))"
    using assms(2) by auto
  hence 5: "Ana_invar_subst (ikst (unlabel 𝒜)  assignment_rhsst (unlabel 𝒜))"
    using assms SMP_mono unfolding typing_cond_prot_def Ana_invar_subst_def by (meson subsetD)

  show ?thesis using 1 2 3 4 5 unfolding typing_cond_def tfrst_def by blast
qed


subsubsection ‹Theorem: Parallel Compositionality for Labeled Protocols›
private definition component_prot where
  "component_prot n P  (l  P. s  set l. has_LabelN n s  has_LabelS s)"

private definition composed_prot where
  "composed_prot 𝒫i  {𝒜. n. proj n 𝒜  𝒫i n}"

private definition component_secure_prot where
  "component_secure_prot n P Sec attack  (𝒜  P. suffix [(ln n, Send1 (Fun attack []))] 𝒜  
     (τ. (interpretationsubst τ  wtsubst τ  wftrms (subst_range τ)) 
            ¬(τ  proj_unl n 𝒜) 
            (𝒜'. prefix 𝒜' 𝒜 
                    (t  Sec-declassifiedlst 𝒜' τ. ¬(τ  proj_unl n 𝒜'@[Send1 t])))))"

private definition component_leaks where
  "component_leaks n 𝒜 Sec  (𝒜' τ. interpretationsubst τ  wtsubst τ  wftrms (subst_range τ) 
      prefix 𝒜' 𝒜  (t  Sec - declassifiedlst 𝒜' τ. (τ  proj_unl n 𝒜'@[Send1 t])))"

private definition unsat where
  "unsat 𝒜  (. interpretationsubst   ¬(  unlabel 𝒜))"

private theorem par_comp_constr_prot:
  assumes P: "P = composed_prot Pi" "par_comp_prot P Sec" "n. component_prot n (Pi n)"
  and left_secure: "component_secure_prot n (Pi n) Sec attack"
  shows "𝒜  P. suffix [(ln n, Send1 (Fun attack []))] 𝒜 
                  unsat 𝒜  (m. n  m  component_leaks m 𝒜 Sec)"
proof -
  { fix 𝒜 𝒜' assume 𝒜: "𝒜 = 𝒜'@[(ln n, Send1 (Fun attack []))]" "𝒜  P"
    let ?P = "𝒜' τ. interpretationsubst τ  wtsubst τ  wftrms (subst_range τ)  prefix 𝒜' 𝒜 
                   (t  Sec - declassifiedlst 𝒜' τ. m. n  m  (τ  proj_unl m 𝒜'@[Send1 t]))"
    have tcp: "typing_cond_prot P" using P(2) unfolding par_comp_prot_def by simp
    have par_comp: "par_comp 𝒜 Sec" "typing_cond (unlabel 𝒜)"
      using par_comp_prot_impl_par_comp[OF P(2) 𝒜(2)]
            typing_cond_prot_impl_typing_cond[OF tcp 𝒜(2)]
      by metis+
  
    have "unlabel (proj n 𝒜) = proj_unl n 𝒜" "proj_unl n 𝒜 = proj_unl n (proj n 𝒜)"
         "A. A  Pi n  proj n A = A" 
         "proj n 𝒜 = (proj n 𝒜')@[(ln n, Send1 (Fun attack []))]"
      using P(1,3) 𝒜 by (auto simp add: proj_def unlabel_def component_prot_def composed_prot_def)
    moreover have "proj n 𝒜  Pi n"
      using P(1) 𝒜 unfolding composed_prot_def by blast
    moreover {
      fix A assume "prefix A 𝒜"
      hence *: "prefix (proj n A) (proj n 𝒜)" unfolding proj_def prefix_def by force
      hence "proj_unl n A = proj_unl n (proj n A)"
            "I. declassifiedlst A I = declassifiedlst (proj n A) I"
        unfolding proj_def declassifiedlst_alt_def by auto
      hence "B. prefix B (proj n 𝒜)  proj_unl n A = proj_unl n B 
                 (I. declassifiedlst A I = declassifiedlst B I)"
        using * by metis
        
    }
    ultimately have *: 
        "τ. interpretationsubst τ  wtsubst τ  wftrms (subst_range τ) 
                  ¬(τ  proj_unl n 𝒜)  (𝒜'. prefix 𝒜' 𝒜 
                        (t  Sec - declassifiedlst 𝒜' τ. ¬(τ  proj_unl n 𝒜'@[Send1 t])))"
      using left_secure unfolding component_secure_prot_def composed_prot_def suffix_def by metis
    { fix  assume : "interpretationsubst " "  unlabel 𝒜"
      obtain τ where τ:
          "interpretationsubst τ" "wtsubst τ" "wftrms (subst_range τ)"
          "𝒜'. prefix 𝒜' 𝒜  (strand_leakslst 𝒜' Sec τ)"
        using par_comp_constr[OF par_comp (2,1)] * by atomize_elim auto
      hence "𝒜'. prefix 𝒜' 𝒜  (t  Sec - declassifiedlst 𝒜' τ. m.
                  n  m  (τ  proj_unl m 𝒜'@[Send1 t]))"
        using τ(4) * unfolding strand_leakslst_def by metis
      hence ?P using τ(1,2,3) by auto
    } hence "unsat 𝒜  (m. n  m  component_leaks m 𝒜 Sec)"
      by (metis unsat_def component_leaks_def)
  } thus ?thesis unfolding suffix_def by metis
qed

subsubsection ‹Theorem: Parallel Compositionality for Stateful Protocols›
private abbreviation wflsst where
  "wflsst V 𝒜  wf'sst V (unlabel 𝒜)"

text ‹
  We state our result on the level of protocol traces (i.e., the constraints reachable in a
  symbolic execution of the actual protocol). Hence, we do not need to convert protocol strands
  to intruder constraints in the following well-formedness definitions.
›
private definition wflssts::"('fun,'var,'lbl) labeled_stateful_strand set  bool" where
  "wflssts 𝒮  (𝒜  𝒮. wflsst {} 𝒜)  (𝒜  𝒮. 𝒜'  𝒮. fvlsst 𝒜  bvarslsst 𝒜' = {})"

private definition wflssts'::
  "('fun,'var,'lbl) labeled_stateful_strand set  ('fun,'var,'lbl) labeled_stateful_strand  bool"
where
  "wflssts' 𝒮 𝒜  (𝒜'  𝒮. wf'sst (wfrestrictedvarslsst 𝒜) (unlabel 𝒜')) 
                 (𝒜'  𝒮. 𝒜''  𝒮. fvlsst 𝒜'  bvarslsst 𝒜'' = {}) 
                 (𝒜'  𝒮. fvlsst 𝒜'  bvarslsst 𝒜 = {}) 
                 (𝒜'  𝒮. fvlsst 𝒜  bvarslsst 𝒜' = {})"

private definition typing_cond_prot_stateful where
  "typing_cond_prot_stateful 𝒫 
    wflssts 𝒫 
    tfrset ((trmslsst ` 𝒫)  pair ` (setopssst ` unlabel ` 𝒫)) 
    wftrms ((trmslsst ` 𝒫)) 
    (S  𝒫. list_all tfrsstp (unlabel S))"

private definition par_comp_prot_stateful where
  "par_comp_prot_stateful 𝒫 Sec 
    (l1 l2. l1  l2 
      GSMP_disjoint (𝒜  𝒫. trmssst (proj_unl l1 𝒜)  pair ` setopssst (proj_unl l1 𝒜))
                    (𝒜  𝒫. trmssst (proj_unl l2 𝒜)  pair ` setopssst (proj_unl l2 𝒜)) Sec) 
    ground Sec  (s  Sec. ¬{} c s) 
    ((i,p)  𝒜  𝒫. setopslsst 𝒜. (j,q)  𝒜  𝒫. setopslsst 𝒜.
      (δ. Unifier δ (pair p) (pair q))  i = j) 
    typing_cond_prot_stateful 𝒫"

private definition component_secure_prot_stateful where
  "component_secure_prot_stateful n P Sec attack 
    (𝒜  P. suffix [(ln n, Send [Fun attack []])] 𝒜  
     (τ. (interpretationsubst τ  wtsubst τ  wftrms (subst_range τ)) 
            ¬(τ s (proj_unl n 𝒜)) 
            (𝒜'. prefix 𝒜' 𝒜 
                    (t  Sec-declassifiedlsst 𝒜' τ. ¬(τ s (proj_unl n 𝒜'@[Send [t]]))))))"

private definition component_leaks_stateful where
  "component_leaks_stateful n 𝒜 Sec 
    (𝒜' τ. interpretationsubst τ  wtsubst τ  wftrms (subst_range τ)  prefix 𝒜' 𝒜 
             (t  Sec - declassifiedlsst 𝒜' τ. (τ s (proj_unl n 𝒜'@[Send [t]]))))"

private definition unsat_stateful where
  "unsat_stateful 𝒜  (. interpretationsubst   ¬( s unlabel 𝒜))"

private lemma wflssts_eqs_wflssts': "wflssts S = wflssts' S []"
unfolding wflssts_def wflssts'_def unlabel_def wfrestrictedvarssst_def by simp

private lemma par_comp_prot_impl_par_comp_stateful:
  assumes "par_comp_prot_stateful 𝒫 Sec" "𝒜  𝒫"
  shows "par_complsst 𝒜 Sec"
proof -
  have *: 
      "l1 l2. l1  l2 
          GSMP_disjoint (𝒜  𝒫. trmssst (proj_unl l1 𝒜)  pair ` setopssst (proj_unl l1 𝒜))
                        (𝒜  𝒫. trmssst (proj_unl l2 𝒜)  pair ` setopssst (proj_unl l2 𝒜)) Sec"
    using assms(1) unfolding par_comp_prot_stateful_def by argo
  { fix l1 l2::'lbl assume **: "l1  l2"
    hence ***: 
        "GSMP_disjoint (𝒜  𝒫. trmssst (proj_unl l1 𝒜)  pair ` setopssst (proj_unl l1 𝒜))
                       (𝒜  𝒫. trmssst (proj_unl l2 𝒜)  pair ` setopssst (proj_unl l2 𝒜)) Sec"
      using * by auto
    have "GSMP_disjoint (trmssst (proj_unl l1 𝒜)  pair ` setopssst (proj_unl l1 𝒜))
                        (trmssst (proj_unl l2 𝒜)  pair ` setopssst (proj_unl l2 𝒜)) Sec"
      using GSMP_disjoint_subset[OF ***] assms(2) by auto
  } hence "l1 l2. l1  l2 
              GSMP_disjoint (trmssst (proj_unl l1 𝒜)  pair ` setopssst (proj_unl l1 𝒜))
                            (trmssst (proj_unl l2 𝒜)  pair ` setopssst (proj_unl l2 𝒜)) Sec"
    by metis
  moreover have "(i,p)  setopslsst 𝒜. (j,q)  setopslsst 𝒜.
                    (δ. Unifier δ (pair p) (pair q))  i = j"
    using assms(1,2) unfolding par_comp_prot_stateful_def by blast
  ultimately show ?thesis
    using assms
    unfolding par_comp_prot_stateful_def par_complsst_def
    by fast
qed

private lemma typing_cond_prot_impl_typing_cond_stateful:
  assumes "typing_cond_prot_stateful 𝒫" "𝒜  𝒫"
  shows "typing_condsst (unlabel 𝒜)"
proof -
  have 1: "wf'sst {} (unlabel 𝒜)" "fvlsst 𝒜  bvarslsst 𝒜 = {}"
    using assms unfolding typing_cond_prot_stateful_def wflssts_def by auto

  have "tfrset ((trmslsst ` 𝒫)  pair ` (setopssst ` unlabel ` 𝒫))"
       "wftrms ((trmslsst ` 𝒫))"
       "trmslsst 𝒜  (trmslsst ` 𝒫)"
       "SMP (trmslsst 𝒜  pair ` setopssst (unlabel 𝒜)) - Var`𝒱 
        SMP ((trmslsst ` 𝒫)  pair ` (setopssst ` unlabel ` 𝒫)) - Var`𝒱"
    using assms SMP_mono[of "trmslsst 𝒜  pair ` setopssst (unlabel 𝒜)"
                            "(trmslsst ` 𝒫)  pair ` (setopssst ` unlabel ` 𝒫)"]
    unfolding typing_cond_prot_stateful_def
    by (metis, metis, auto)
  hence 2: "tfrset (trmslsst 𝒜  pair ` setopssst (unlabel 𝒜))" and 3: "wftrms (trmslsst 𝒜)"
    unfolding tfrset_def by (meson subsetD)+

  have 4: "list_all tfrsstp (unlabel 𝒜)" using assms unfolding typing_cond_prot_stateful_def by auto

  show ?thesis using 1 2 3 4 unfolding typing_condsst_def tfrsst_def by blast
qed

private theorem par_comp_constr_prot_stateful:
  assumes P: "P = composed_prot Pi" "par_comp_prot_stateful P Sec" "n. component_prot n (Pi n)"
  and left_secure: "component_secure_prot_stateful n (Pi n) Sec attack"
  shows "𝒜  P. suffix [(ln n, Send [Fun attack []])] 𝒜 
                  unsat_stateful 𝒜  (m. n  m  component_leaks_stateful m 𝒜 Sec)"
proof -
  { fix 𝒜 𝒜' assume 𝒜: "𝒜 = 𝒜'@[(ln n, Send [Fun attack []])]" "𝒜  P"
    let ?P = "𝒜' τ. interpretationsubst τ  wtsubst τ  wftrms (subst_range τ)  prefix 𝒜' 𝒜 
                   (t  Sec-declassifiedlsst 𝒜' τ. m. n  m  (τ s (proj_unl m 𝒜'@[Send [t]])))"
    have tcp: "typing_cond_prot_stateful P" using P(2) unfolding par_comp_prot_stateful_def by simp
    have par_comp: "par_complsst 𝒜 Sec" "typing_condsst (unlabel 𝒜)"
      using par_comp_prot_impl_par_comp_stateful[OF P(2) 𝒜(2)]
            typing_cond_prot_impl_typing_cond_stateful[OF tcp 𝒜(2)]
      by metis+
  
    have "unlabel (proj n 𝒜) = proj_unl n 𝒜" "proj_unl n 𝒜 = proj_unl n (proj n 𝒜)"
         "A. A  Pi n  proj n A = A" 
         "proj n 𝒜 = (proj n 𝒜')@[(ln n, Send [Fun attack []])]"
      using P(1,3) 𝒜 by (auto simp add: proj_def unlabel_def component_prot_def composed_prot_def)
    moreover have "proj n 𝒜  Pi n"
      using P(1) 𝒜 unfolding composed_prot_def by blast
    moreover {
      fix A assume "prefix A 𝒜"
      hence *: "prefix (proj n A) (proj n 𝒜)" unfolding proj_def prefix_def by force
      hence "proj_unl n A = proj_unl n (proj n A)"
            "I. declassifiedlsst A I = declassifiedlsst (proj n A) I"
        by (simp, metis declassifiedlsst_proj_eq)
      hence "B. prefix B (proj n 𝒜)  proj_unl n A = proj_unl n B 
                 (I. declassifiedlsst A I = declassifiedlsst B I)"
        using * by metis
    }
    ultimately have *: 
        "τ. interpretationsubst τ  wtsubst τ  wftrms (subst_range τ) 
                  ¬(τ s (proj_unl n 𝒜))  (𝒜'. prefix 𝒜' 𝒜 
                        (t  Sec - declassifiedlsst 𝒜' τ. ¬(τ s (proj_unl n 𝒜'@[Send [t]]))))"
      using left_secure
      unfolding component_secure_prot_stateful_def composed_prot_def suffix_def
      by metis
    { fix  assume : "interpretationsubst " " s unlabel 𝒜"
      obtain τ where τ:
          "interpretationsubst τ" "wtsubst τ" "wftrms (subst_range τ)"
          "𝒜'. prefix 𝒜' 𝒜  (𝒜' leaks Sec under τ)"
        using par_comp_constr_stateful[OF par_comp (2,1)] * by atomize_elim auto
      hence "𝒜'. prefix 𝒜' 𝒜  (t  Sec - declassifiedlsst 𝒜' τ. m.
                  n  m  (τ s (proj_unl m 𝒜'@[Send [t]])))"
        using τ(4) * unfolding strand_leakslsst_def by metis
      hence ?P using τ(1,2,3) by auto
    } hence "unsat_stateful 𝒜  (m. n  m  component_leaks_stateful m 𝒜 Sec)"
      by (metis unsat_stateful_def component_leaks_stateful_def)
  } thus ?thesis unfolding suffix_def by metis
qed

end

end

subsection ‹Automated Compositionality Conditions›
definition comp_GSMP_disjoint where
  "comp_GSMP_disjoint public arity Ana Γ A' B' A B C 
    let  = B set var_rename (max_var_set (fvset A))
    in has_all_wt_instances_of Γ A' A 
       has_all_wt_instances_of Γ B'  
       finite_SMP_representation arity Ana Γ A 
       finite_SMP_representation arity Ana Γ  
       (t  A. s  . Γ t = Γ s  mgu t s  None 
         (intruder_synth' public arity {} t)  (u  C. is_wt_instance_of_cond Γ t u))"

definition comp_par_comp'lsst where
  "comp_par_comp'lsst public arity Ana Γ pair_fun A M C 
    wftrms' arity C 
    ((i,p)  setopslsst A. (j,q)  setopslsst A. if i = j then True else
      (let s = pair' pair_fun p; t = pair' pair_fun q
       in mgu s (t  var_rename (max_var s)) = None))"

definition comp_par_complsst where
  "comp_par_complsst public arity Ana Γ pair_fun A M C 
  let L = remdups (map (the_LabelN  fst) (filter (Not  has_LabelS) A));
      MP0 = λB. trmssst B  (pair' pair_fun) ` setopssst B;
      pr = λl. MP0 (proj_unl l A)
  in length L > 1 
     comp_par_comp'lsst public arity Ana Γ pair_fun A M C 
     wftrms' arity (MP0 (unlabel A)) 
     (i  set L. j  set L. if i = j then True else
        comp_GSMP_disjoint public arity Ana Γ (pr i) (pr j) (M i) (M j) C)"

lemma comp_par_complsstI:
  fixes pair_fun A MP0 pr
  defines "MP0  λB. trmssst B  (pair' pair_fun) ` setopssst B"
    and "pr  λl. MP0 (proj_unl l A)"
  assumes L_def: "L = remdups (map (the_LabelN  fst) (filter (Not  has_LabelS) A))"
    and L_gt: "length L > 1"
    and cpc': "comp_par_comp'lsst public arity Ana Γ pair_fun A M C"
    and MP0_wf: "wftrms' arity (MP0 (unlabel A))"
    and GSMP_disj: "i  set L. j  set L. if i = j then True else
                      comp_GSMP_disjoint public arity Ana Γ (pr i) (pr j) (M i) (M j) C"
  shows "comp_par_complsst  public arity Ana Γ pair_fun A M C"
using assms unfolding comp_par_complsst_def by presburger

lemma comp_par_complsstI':
  fixes pair_fun A MP0 pr Ms
  defines "MP0  λB. trmssst B  (pair' pair_fun) ` setopssst B"
    and "pr  λl. MP0 (proj_unl l A)"
    and "M  λl. case find ((=) l  fst) Ms of Some M  set (snd M) | None  {}"
  assumes L_def: "map fst Ms = remdups (map (the_LabelN  fst) (filter (Not  has_LabelS) A))"
    and L_gt: "length (map fst Ms) > 1"
    and cpc': "comp_par_comp'lsst public arity Ana Γ pair_fun A M C"
    and MP0_wf: "wftrms' arity (MP0 (unlabel A))"
    and GSMP_disj: "i  set (map fst Ms). j  set (map fst Ms). if i = j then True else
                      comp_GSMP_disjoint public arity Ana Γ (pr i) (pr j) (M i) (M j) C"
  shows "comp_par_complsst  public arity Ana Γ pair_fun A M C"
by (rule comp_par_complsstI[OF L_def L_gt cpc' MP0_wf[unfolded MP0_def]
                              GSMP_disj[unfolded pr_def MP0_def]])


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

sublocale labeled_stateful_typed_model
by unfold_locales

lemma GSMP_disjoint_if_comp_GSMP_disjoint:
  defines "f  λM. {t  δ | t δ. t  M  wtsubst δ  wftrms (subst_range δ)  fv (t  δ) = {}}"
  assumes AB'_wf: "wftrms' arity A'" "wftrms' arity B'"
    and C_wf: "wftrms' arity C"
    and AB'_disj: "comp_GSMP_disjoint public arity Ana Γ A' B' A B C"
  shows "GSMP_disjoint A' B' (f C - {m. {} c m})"
using GSMP_disjointI[of A' B' A B] AB'_wf AB'_disj C_wf
unfolding wftrms'_def comp_GSMP_disjoint_def f_def wftrm_code list_all_iff Let_def by blast 

lemma par_complsst_if_comp_par_complsst:
  defines "f  λM. {t  δ | t δ. t  M  wtsubst δ  wftrms (subst_range δ)  fv (t  δ) = {}}"
  assumes A: "comp_par_complsst public arity Ana Γ Pair A M C"
  shows "par_complsst A (f C - {m. {} c m})"
proof (unfold par_complsst_def; intro conjI)
  let ?Sec = "f C - {m. {} c m}"
  let ?L = "remdups (map (the_LabelN  fst) (filter (Not  has_LabelS) A))"
  let ?N1 = "λB. trmssst B  (pair' Pair) ` setopssst B"
  let ?N2 = "λB. trmssst B  pair ` setopssst B"
  let ?pr = "λl. ?N1 (proj_unl l A)"
  let  = "λp. var_rename (max_var (pair p))"

  note defs = pair_code wftrm_code wftrms'_def list_all_iff
              trms_listsst_is_trmssst setops_listsst_is_setopssst

  have 0:
      "length ?L > 1"
      "wftrms' arity (?N1 (unlabel A))"
      "wftrms' arity C"
      (* "has_all_wt_instances_of Γ (subtermsset C) C" *)
      (* "is_TComp_var_instance_closed Γ C" *)
      "i  set ?L. j  set ?L. i  j 
        comp_GSMP_disjoint public arity Ana Γ (?pr i) (?pr j) (M i) (M j) C"
      "(i,p)  setopslsst A. (j,q)  setopslsst A. i  j  mgu (pair p) (pair q   p) = None"
    using A unfolding comp_par_complsst_def comp_par_comp'lsst_def pair_code
    by meson+

  have L_in_iff: "l  set ?L  (a  set A. has_LabelN l a)" for l by force

  have A_wf_trms: "wftrms (trmslsst A  pair ` setopssst (unlabel A))"
    using 0(2) unfolding defs by auto
  hence A_proj_wf_trms: "wftrms (trmslsst (proj l A)  pair ` setopssst (proj_unl l A))" for l
    using trmssst_proj_subset(1)[of l A] setopssst_proj_subset(1)[of l A] by blast
  hence A_proj_wf_trms': "wftrms' arity (?N1 (proj_unl l A))" for l
    unfolding defs by auto

  note C_wf_trms = 0(3)[unfolded list_all_iff wftrms'_def wftrm_code[symmetric]]

(*   note 1 = has_all_wt_instances_ofD'[OF wf_trms_subterms[OF C_wf_trms] C_wf_trms 0(4)] *)

  have 2: "GSMP (?N2 (proj_unl l A))  GSMP (?N2 (proj_unl l' A))" when "l  set ?L" for l l'
    using that L_in_iff GSMP_mono[of "?N2 (proj_unl l A)" "?N2 (proj_unl l' A)"]
          trmssst_unlabel_subset_if_no_label[of l A]
          setopssst_unlabel_subset_if_no_label[of l A]
    unfolding list_ex_iff by fast

  have 3: "GSMP_disjoint (?N2 (proj_unl l1 A)) (?N2 (proj_unl l2 A)) ?Sec"
    when "l1  set ?L" "l2  set ?L" "l1  l2" for l1 l2
  proof -
    have "GSMP_disjoint (?N1 (proj_unl l1 A)) (?N1 (proj_unl l2 A)) ?Sec"
      using 0(4) that
            GSMP_disjoint_if_comp_GSMP_disjoint[
              OF A_proj_wf_trms'[of l1] A_proj_wf_trms'[of l2] 0(3),
              of "M l1" "M l2"]
      unfolding f_def by blast
    thus ?thesis
      unfolding pair_code trms_listsst_is_trmssst setops_listsst_is_setopssst
      by simp
  qed

  obtain a1 a2 where a: "a1  set ?L" "a2  set ?L" "a1  a2"
    using remdups_ex2[OF 0(1)] by atomize_elim auto

  show "ground ?Sec" unfolding f_def by fastforce

  { fix i p j q
    assume p: "(i,p)  setopslsst A" and q: "(j,q)  setopslsst A"
      and pq: "δ. Unifier δ (pair p) (pair q)"

    have "δ. Unifier δ (pair p) (pair q   p)"
      using pq vars_term_disjoint_imp_unifier[OF var_rename_fv_disjoint[of "pair p"], of _ "pair q"]
      by (metis (no_types, lifting) subst_subst_compose var_rename_inv_comp)
    hence "i = j" using 0(5) mgu_None_is_subst_neq[of "pair p" "pair q   p"] p q by fast
  } thus "(i,p)  setopslsst A. (j,q)  setopslsst A. (δ. Unifier δ (pair p) (pair q))  i = j"
    by blast

  show "l1 l2. l1  l2  GSMP_disjoint (?N2 (proj_unl l1 A)) (?N2 (proj_unl l2 A)) ?Sec"
    using 2 3 3[OF a] unfolding GSMP_disjoint_def by blast

(*   show "∀s ∈ ?Sec. ∀s' ∈ subterms s. {} ⊢c s' ∨ s' ∈ ?Sec"
  proof (intro ballI)
    fix s s'
    assume s: "s ∈ ?Sec" and s': "s' ⊑ s"
    then obtain t δ where t: "t ∈ C" "s = t ⋅ δ" "fv s = {}" "¬{} ⊢c s"
        and δ: "wtsubst δ" "wftrms (subst_range δ)"
      unfolding f_def by blast

    obtain m θ where m: "m ∈ C" "s' = m ⋅ θ" and θ: "wtsubst θ" "wftrms (subst_range θ)"
      using TComp_var_and_subterm_instance_closed_has_subterms_instances[
              OF 0(5,4) C_wf_trms in_subterms_Union[OF t(1)] s'[unfolded t(2)] δ]
      by blast
    thus "{} ⊢c s' ∨ s' ∈ ?Sec"
      using ground_subterm[OF t(3) s']
      unfolding f_def by blast
  qed *)

  show "s  ?Sec. ¬{} c s" by simp
qed

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,(('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"
  and label_witness1::"'lbl"
  and label_witness2::"'lbl"
begin

sublocale labeled_stateful_typing
by unfold_locales

lemma par_complsst_if_comp_par_complsst':
  defines "f  λM. {t  δ | t δ. t  M  wtsubst δ  wftrms (subst_range δ)  fv (t  δ) = {}}"
  assumes a: "comp_par_complsst public arity Ana Γ Pair A M C"
    and B: "b  set B. a  set A. δ. b = a lsstp δ  wtsubst δ  wftrms (subst_range δ)"
      (is "b  set B. a  set A. δ. b = a lsstp δ  ?D δ")
  shows "par_complsst B (f C - {m. {} c m})"
proof (unfold par_complsst_def; intro conjI)
  define N1 where "N1  λB::('fun, ('fun,'atom) term_type × nat) stateful_strand.
    trmssst B  (pair' Pair) ` setopssst B"

  define N2 where "N2  λB::('fun, ('fun,'atom) term_type × nat) stateful_strand.
    trmssst B  pair ` setopssst B"

  define L where "L  λA::('fun, ('fun,'atom) term_type × nat, 'lbl) labeled_stateful_strand.
    remdups (map (the_LabelN  fst) (filter (Not  has_LabelS) A))"

  define α where "α  λp. var_rename (max_var (pair p::('fun, ('fun,'atom) term_type × nat) term))
    ::('fun, ('fun,'atom) term_type × nat) subst"

  let ?Sec = "f C - {m. {} c m}"

  have 0:
      "length (L A) > 1"
      "wftrms' arity (N1 (unlabel A))"
      "wftrms' arity C"
     (*  "has_all_wt_instances_of Γ (subtermsset C) C" *)
      (* "is_TComp_var_instance_closed Γ C" *)
      "i  set (L A). j  set (L A). i  j 
        comp_GSMP_disjoint public arity Ana Γ (N1 (proj_unl i A)) (N1 (proj_unl j A)) (M i) (M j) C"
      "(i,p)  setopslsst A. (j,q)  setopslsst A. i  j  mgu (pair p) (pair q  α p) = None"
    using a unfolding comp_par_complsst_def comp_par_comp'lsst_def pair_code L_def N1_def α_def
    by meson+

  note 1 = trmssst_proj_subset(1) setopssst_proj_subset(1)

  have N1_iff_N2: "N1 A = N2 A" for A
    unfolding pair_code trms_listsst_is_trmssst setops_listsst_is_setopssst N1_def N2_def by simp

  have N2_proj_subset: "N2 (proj_unl l A)  N2 (unlabel A)"
    for l::'lbl and A::"('fun, ('fun,'atom) term_type × nat, 'lbl) labeled_stateful_strand"
    using 1(1)[of l A] image_mono[OF 1(2)[of l A], of pair] unfolding N2_def by blast

  have L_in_iff: "l  set (L A)  (a  set A. has_LabelN l a)" for l A
    unfolding L_def by force

  have L_B_subset_A: "l  set (L A)" when l: "l  set (L B)" for l
    using L_in_iff[of l B] L_in_iff[of l A] B l by fastforce

  note B_setops = setopslsst_wt_instance_ex[OF B]

  have B_proj: "b  set (proj l B). a  set (proj l A). δ. b = a lsstp δ  ?D δ" for l
    using proj_instance_ex[OF B] by fast

  have B': "t  N2 (unlabel B). s  N2 (unlabel A). δ. t = s  δ  ?D δ"
    using trmssst_setopssst_wt_instance_ex[OF B] unfolding N2_def by blast

  have B'_proj: "t  N2 (proj_unl l B). s  N2 (proj_unl l A). δ. t = s  δ  ?D δ" for l
    using trmssst_setopssst_wt_instance_ex[OF B_proj] unfolding N2_def by presburger

  have A_wf_trms: "wftrms (N2 (unlabel A))"
    using N1_iff_N2[of "unlabel A"] 0(2) unfolding wftrm_code wftrms'_def list_all_iff by auto
  hence A_proj_wf_trms: "wftrms (N2 (proj_unl l A))" for l
    using 1[of l] unfolding N2_def by blast
  hence A_proj_wf_trms': "wftrms' arity (N1 (proj_unl l A))" for l
    using N1_iff_N2[of "proj_unl l A"] unfolding wftrm_code wftrms'_def list_all_iff by presburger

  note C_wf_trms = 0(3)[unfolded list_all_iff wftrms'_def wftrm_code[symmetric]]

  have 2: "GSMP (N2 (proj_unl l A))  GSMP (N2 (proj_unl l' A))"
    when "l  set (L A)" for l l'
      and A::"('fun, ('fun,'atom) term_type × nat, 'lbl) labeled_stateful_strand"
    using that L_in_iff[of _ A] GSMP_mono[of "N2 (proj_unl l A)" "N2 (proj_unl l' A)"]
          trmssst_unlabel_subset_if_no_label[of l A]
          setopssst_unlabel_subset_if_no_label[of l A]
    unfolding list_ex_iff N2_def by fast

  have 3: "GSMP (N2 (proj_unl l B))  GSMP (N2 (proj_unl l A))" (is "?X  ?Y") for l
  proof
    fix t assume "t  ?X"
    hence t: "t  SMP (N2 (proj_unl l B))" "fv t = {}" unfolding GSMP_def by simp_all
    have "t  SMP (N2 (proj_unl l A))"
      using t(1) B'_proj[of l] SMP_wt_instances_subset[of "N2 (proj_unl l B)" "N2 (proj_unl l A)"]
      by metis
    thus "t  ?Y" using t(2) unfolding GSMP_def by fast
  qed

  have "GSMP_disjoint (N2 (proj_unl l1 A)) (N2 (proj_unl l2 A)) ?Sec"
    when "l1  set (L A)" "l2  set (L A)" "l1  l2" for l1 l2
  proof -
    have "GSMP_disjoint (N1 (proj_unl l1 A)) (N1 (proj_unl l2 A)) ?Sec"
      using 0(4) that
            GSMP_disjoint_if_comp_GSMP_disjoint[
              OF A_proj_wf_trms'[of l1] A_proj_wf_trms'[of l2] 0(3),
              of "M l1" "M l2"]
      unfolding f_def by blast
    thus ?thesis using N1_iff_N2 by simp
  qed
  hence 4: "GSMP_disjoint (N2 (proj_unl l1 B)) (N2 (proj_unl l2 B)) ?Sec"
    when "l1  set (L A)" "l2  set (L A)" "l1  l2" for l1 l2
    using that 3 unfolding GSMP_disjoint_def by blast

  { fix i p j q
    assume p: "(i,p)  setopslsst B" and q: "(j,q)  setopslsst B"
      and pq: "δ. Unifier δ (pair p) (pair q)"

    obtain p' δp where p': "(i,p')  setopslsst A" "p = p' p δp" "pair p = pair p'  δp"
      using p B_setops unfolding pair_def by auto

    obtain q' δq where q': "(j,q')  setopslsst A" "q = q' p δq" "pair q = pair q'  δq"
      using q B_setops unfolding pair_def by auto

    obtain θ where "Unifier θ (pair p) (pair q)" using pq by blast
    hence "δ. Unifier δ (pair p') (pair q'  α p')"
      using p'(3) q'(3) var_rename_inv_comp[of "pair q'"] subst_subst_compose
            vars_term_disjoint_imp_unifier[
              OF var_rename_fv_disjoint[of "pair p'"],
              of "δp s θ" "pair q'" "var_rename_inv (max_var_set (fv (pair p'))) s δq s θ"]
      unfolding α_def by fastforce
    hence "i = j"
      using mgu_None_is_subst_neq[of "pair p'" "pair q'  α p'"] p'(1) q'(1) 0(5)
      unfolding α_def by fast
  } thus "(i,p)  setopslsst B. (j,q)  setopslsst B. (δ. Unifier δ (pair p) (pair q))  i = j"
    by blast

  obtain a1 a2 where a: "a1  set (L A)" "a2  set (L A)" "a1  a2"
    using remdups_ex2[OF 0(1)[unfolded L_def]] unfolding L_def by atomize_elim auto

  show "l1 l2. l1  l2  GSMP_disjoint (N2 (proj_unl l1 B)) (N2 (proj_unl l2 B)) ?Sec"
    using 2[of _ B] 4 4[OF a] L_B_subset_A unfolding GSMP_disjoint_def by blast

  show "ground ?Sec" unfolding f_def by fastforce

(*   show "∀s ∈ ?Sec. ∀s' ∈ subterms s. {} ⊢c s' ∨ s' ∈ ?Sec"
  proof (intro ballI)
    fix s s'
    assume s: "s ∈ ?Sec" and s': "s' ⊑ s"
    then obtain t δ where t: "t ∈ C" "s = t ⋅ δ" "fv s = {}" "¬{} ⊢c s"
        and δ: "wtsubst δ" "wftrms (subst_range δ)"
      unfolding f_def by blast

    obtain m θ where m: "m ∈ C" "s' = m ⋅ θ" and θ: "wtsubst θ" "wftrms (subst_range θ)"
      using TComp_var_and_subterm_instance_closed_has_subterms_instances[
              OF 0(5,4) C_wf_trms in_subterms_Union[OF t(1)] s'[unfolded t(2)] δ]
      by blast
    thus "{} ⊢c s' ∨ s' ∈ ?Sec"
      using ground_subterm[OF t(3) s']
      unfolding f_def by blast
  qed *)

  show "s  ?Sec. ¬{} c s" by simp
qed

end

end