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) [d←dbproj 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) [d←D. 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) [d←D. d ∉ set Di]⟧d ℐ"
    (is "?P D")
  shows "⟦M; map (λd. ∀X⟨∨≠: [(pair (t,s), pair (snd d))]⟩st) [d←dbproj 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: "∀f∈set 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) D⟧d ℐ" (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) Di⟧d ℐ"
  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⟨ts⟩st)) (trpc A D)"
| "trpc ((i,receive⟨ts⟩)#A) D = map ((#) (i,receive⟨ts⟩st)) (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))
                                    [d←dbproj i D. d ∉ set Di])@B)
                          (trpc A [d←D. 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)) [d←dbproj i D. d ∉ set Di])@A))"
proof -
  let ?f = "[d←dbproj 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⟨t⟩st) ∈ 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⟨t⟩st) ∈ 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⟨t⟩st) ∈ set C} = {t. receive⟨t⟩st ∈ 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⟨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 "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⟨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 "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 [d←D. 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)) [d←dbproj i D. d ∉ set Di]"
    by atomize_elim auto
  hence "trmslst A'' ⊆ trmssst (unlabel A) ∪ pair ` setopssst (unlabel A) ∪
                       pair ` snd ` set [d←D. d ∉ set Di]"
    by (metis "6.IH")
  moreover have "set [d←D. 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 [d←dbproj 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⟨ts⟩st)#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⟨ts⟩st)#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)) [d←dbproj i D. d ∉ set Di]))"
      from prems si obtain Di A'' where A'':
          "A' = constr Di@A''" "A'' ∈ set (trpc A [d←D. 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 [d←D. 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)) [d←dbproj 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 [d←D. d ∉ set Di])"
    using prems constr_def by fastforce
  hence "proj n B' ∈ set (trpc (proj n S) (proj n [d←D. d ∉ set Di]))" using IH by simp
  hence IH': "proj n B' ∈ set (trpc (proj n S) [d←proj 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 "[d←proj 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⟨t⟩st) ∈ 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⟨t⟩st)] 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⟨t⟩st)] 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⟨t⟩st) ∧ 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⟨t⟩st ∉ snd ` set (constr Di)" unfolding constr_def by force
  hence "¬suffix [(l, receive⟨t⟩st)] (constr Di)" unfolding suffix_def by auto
  hence "1 ≤ length E'" using prems(2) E'(1) by (cases E') auto
  hence "suffix [(l, receive⟨t⟩st)] 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⟨t⟩st ≠ snd (constr d)" unfolding constr_def by force
  hence "suffix [(l, receive⟨t⟩st)] 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⟨t⟩st ∉ snd ` set constr" unfolding constr_def by force
  hence "¬suffix [(l, receive⟨t⟩st)] constr" unfolding suffix_def by auto
  hence "1 ≤ length E'" using prems(2) E'(1) by (cases E') auto
  hence "suffix [(l, receive⟨t⟩st)] 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⟨t⟩st) ∉ set C') ∧
                     (C = [] ∨ (∃n t. suffix [(n,receive⟨t⟩st)] 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⟨t⟩st")
        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⟨t⟩st) ∉ set C'"
      "C = [] ∨ (∃n t. suffix [(n,receive⟨t⟩st)] 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⟨t⟩st) ∈ set B ⟹ (m,receive⟨t⟩st) ∈ set C" using C by auto
  hence "⋀t. receive⟨t⟩st ∈ set (proj_unl n B) ⟹ receive⟨t⟩st ∈ 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⟨t⟩st)] 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⟨t⟩st)] 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⟨t⟩st) = (i, receive⟨t'⟩st)")
      case True
      note T = True
      show ?thesis
      proof (cases "suffix [(m, receive⟨t⟩st)] E'")
        case True
        hence "suffix [(m, receive⟨t⟩st)] 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⟨t⟩st)]" "(m, receive⟨t⟩st)" 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⟨t⟩st)] 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⟨t⟩st)] 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⟨t⟩st)] 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⟨t⟩st) ∉ 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⟨t⟩st)] E'" "prefix E' A''"
      using *(1) prems(1,2) suffix_append[of "[(m,receive⟨t⟩st)]" "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⟨t⟩st)] 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⟨t⟩st) ∉ 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⟨t⟩st)] E'" "prefix E' A''"
      using *(1) prems(1,2) suffix_append[of "[(m,receive⟨t⟩st)]" 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⟨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) 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⟨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) 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 [d←D. 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 "∀a∈M. ∀b∈M. P a b"
      when "M ⊆ N" "∀a∈N. ∀b∈N. 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⟨∨≠: u⟩st ∈ set (unlabel A'') ∨
         (∃d ∈ set (filter (λd. d ∉ set Di) D). u = [(pair (t,s), pair (snd d))] ∧ Q2 u X)"
      when "∀X⟨∨≠: u⟩st ∈ set (unlabel A')" for X u
      using that A''(1) unfolding Q2_def constr unlabel_def dbproj_def by force
    have 4: "∀d∈set 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⟨∨≠: u⟩st ∈ set (unlabel A')"
      hence "∀U⟨∨≠: u⟩st ∈ 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⟨∨≠: F⟩st)]" 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⟨ts⟩st)) (tr'pc A D)"
| "tr'pc ((i,receive⟨ts⟩)#A) D = map ((#) (i,receive⟨ts⟩st)) (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))
                                    [d←D. d ∉ set Di])@B)
                          (tr'pc A [d←D. 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 [d←unlabel D. d ∉ set Di]))"
      define constr2 where "constr2 = (λDi. (map ?f2 Di)@(map ?g2 [d←D. d ∉ set Di]))"
  
      obtain C' Di where C':
          "Di ∈ set (subseqs D)"
          "C = constr2 Di@C'"
          "C' ∈ set (tr'pc S [d←D. d ∉ set Di])"
        using "6.prems"(1) unfolding constr2_def by atomize_elim auto
      
      have 0: "set [d←D. 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 [d←D. d ∉ set Di].
           ∀(k, q) ∈ setopslsst S ∪ set [d←D. 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 [d←D. d ∉ set Di] = [d←unlabel 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 "[d←D. 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⟨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) Send by auto
    next
      case (Receive t)
      then obtain B' where B':
          "B = receive⟨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) 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)) [d←D. 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) [d←unlabel D. d ∉ set Di])"

      obtain B' Di where B':
          "B = d Di@B'" "Di ∈ set (subseqs (unlabel D))"
          "B' ∈ set (tr (unlabel A) [d←unlabel 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 [d←D. d ∉ set Di'].
               ∀(k, q) ∈ setopslsst A ∪ set [d←D. 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: "[d←unlabel D. d ∉ set Di] = unlabel [d←D. 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 [d←D. 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 B⟧d ℐ) ⟷ (∃C ∈ set (tr'pc A D). ⟦M; unlabel C⟧d ℐ)"
    (is "?P ⟷ ?Q")
proof
  { fix B assume "B ∈ set (trpc A D)" "⟦M; unlabel B⟧d ℐ"
    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⟨ts⟩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 ∈ set ts. M ⊢ t ⋅ ℐ" using prems(2) B'(1) by simp

      obtain C where C: "C ∈ set (tr'pc S D)" "⟦M; unlabel C⟧d ℐ"
        using IH[OF B'(2) 1 4 5 6] by atomize_elim auto
      hence "((i,send⟨ts⟩st)#C) ∈ set (tr'pc ((i,Send ts)#S) D)" "⟦M; unlabel ((i,send⟨ts⟩st)#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⟨ts⟩st)#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 C⟧d ℐ"
        using IH[OF B'(2) 1 4 5 6] by atomize_elim auto
      hence "((i,receive⟨ts⟩st)#C) ∈ set (tr'pc ((i,receive⟨ts⟩)#S) D)"
            "⟦(set ts ⋅set ℐ) ∪ M; unlabel ((i,receive⟨ts⟩st)#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 C⟧d ℐ"
        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 B⟧d ℐ " 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)) [d←dbproj i D. d∉set Di]"
      let ?cu2 = "λDi. map (λd. ∀[]⟨∨≠: [(pair (t,s), pair (snd d))]⟩st) [d←dbproj i D. d∉set 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)) [d←D. d∉set Di]"
      let ?du2 = "λDi. map (λd. ∀[]⟨∨≠: [(pair (t,s), pair (snd d))]⟩st) [d←D. d∉set 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 [d←D. 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 [d←D. d ∉ set Di]"
               "(k, q) ∈ setopslsst S ∪ set [d←D. 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 [d←D. 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 [d←D . d ∉ set Di])" "⟦M; unlabel C⟧d ℐ"
        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 Di⟧d ℐ" 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 Di⟧d ℐ" 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 C⟧d ℐ"
        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 C⟧d ℐ"
        using IH[OF B'(2) 1 4 5 6] by atomize_elim auto

      have 7: "⟦M; unlabel c⟧d ℐ" "⟦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 ?cl⟧d ℐ" using 7(1) unfolding c unlabel_def by auto 
      hence "⟦M; ?cu⟧d ℐ" 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; ?du⟧d ℐ" using labeled_sat_ineq_dbproj_sem_equiv[of i] by simp
      hence "⟦M; unlabel ?dl⟧d ℐ" by (metis 0(4))
      hence "⟦M; unlabel d⟧d ℐ" 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 C⟧d ℐ"
    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⟨ts⟩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 ∈ set ts. M ⊢ t ⋅ ℐ" using prems(2) C'(1) by simp

      obtain B where B: "B ∈ set (trpc S D)" "⟦M; unlabel B⟧d ℐ"
        using IH[OF C'(2) 1 4 5 6] by atomize_elim auto
      hence "((i,send⟨ts⟩st)#B) ∈ set (trpc ((i,Send ts)#S) D)"
            "⟦M; unlabel ((i,send⟨ts⟩st)#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⟨ts⟩st)#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 B⟧d ℐ"
        using IH[OF C'(2) 1 4 5 6] by atomize_elim auto
      hence "((i,receive⟨ts⟩st)#B) ∈ set (trpc ((i,receive⟨ts⟩)#S) D)"
            "⟦(set ts ⋅set ℐ) ∪ M; unlabel ((i,receive⟨ts⟩st)#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 B⟧d ℐ"
        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 C⟧d ℐ " 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)) [d←dbproj i D. d∉set Di]"
      let ?du2 = "λDi. map (λd. ∀[]⟨∨≠: [(pair (t,s), pair (snd d))]⟩st) [d←dbproj i D. d∉set 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)) [d←D. d∉set Di]"
      let ?cu2 = "λDi. map (λd. ∀[]⟨∨≠: [(pair (t,s), pair (snd d))]⟩st) [d←D. d∉set 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 [d←D. 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 [d←D. d ∉ set Di]"
               "(k, q) ∈ setopslsst S ∪ set [d←D. 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 [d←D. 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 [d←D. d ∉ set Di])" "⟦M; unlabel B⟧d ℐ"
        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 Di⟧d ℐ" 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 Di⟧d ℐ" by (metis 0(4))
      hence "⟦M; ?du2 Di⟧d ℐ" 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 B⟧d ℐ"
        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 B⟧d ℐ"
        using IH[OF C'(2) 1 4 5 6] by atomize_elim auto

      have 7: "⟦M; unlabel c⟧d ℐ" "⟦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 ?cl⟧d ℐ" using 7(1) unfolding c unlabel_def by auto 
      hence "⟦M; ?cu⟧d ℐ" 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; ?du⟧d ℐ" using labeled_sat_ineq_dbproj_sem_equiv[of i] by simp
      hence "⟦M; unlabel ?dl⟧d ℐ" by (metis 0(4))
      hence "⟦M; unlabel d⟧d ℐ" 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 A⟧s ℐ ⟷ (∃B ∈ set (tr'pc A D). ⟦M; unlabel B⟧d ℐ)"
        (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 A⟧s ℐ ⟷ (∃B ∈ set (trpc A D). ⟦M; unlabel B⟧d ℐ)"
  (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 ℐ' ⟷
        (∃B∈set (trpc 𝒜 []). ⟦{}; unlabel B⟧d ℐ')"
    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⟨ts⟩st)] 𝒜'' ∧
                    (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 ℐ' ⟷
        (∃B∈set (trpc 𝒜 []). ⟦{}; unlabel B⟧d ℐ')"
    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⟨ts⟩st)] 𝒜'' ∧
                    (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⟨ts⟩st]⟧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δ = B ⋅set var_rename (max_var_set (fvset A))
    in has_all_wt_instances_of Γ A' A ∧
       has_all_wt_instances_of Γ B' Bδ ∧
       finite_SMP_representation arity Ana Γ A ∧
       finite_SMP_representation arity Ana Γ Bδ ∧
       (∀t ∈ A. ∀s ∈ Bδ. Γ 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