Theory Parallel_Compositionality

(*  Title:      Parallel_Compositionality.thy
Author:     Andreas Viktor Hess, DTU
Author:     Sebastian A. Mödersheim, DTU
Author:     Achim D. Brucker, The University of Sheffield
*)

section ‹Parallel Compositionality of Security Protocols›
theory Parallel_Compositionality
imports Typing_Result Labeled_Strands
begin

text‹\label{sec:Parallel-Compositionality}›

subsection ‹Definitions: Labeled Typed Model Locale›
locale labeled_typed_model = typed_model arity public Ana Γ
for arity::"'fun ⇒ nat"
and public::"'fun ⇒ bool"
and Ana::"('fun,'var) term ⇒ (('fun,'var) term list × ('fun,'var) term list)"
and Γ::"('fun,'var) term ⇒ ('fun,'atom::finite) term_type"
+
fixes label_witness1 and label_witness2::"'lbl"
assumes at_least_2_labels: "label_witness1 ≠ label_witness2"
begin

text ‹The Ground Sub-Message Patterns (GSMP)›
definition GSMP::"('fun,'var) terms ⇒ ('fun,'var) terms" where
"GSMP P ≡ {t ∈ SMP P. fv t = {}}"

definition typing_cond where
"typing_cond 𝒜 ≡
wf⇩s⇩t {} 𝒜 ∧
fv⇩s⇩t 𝒜 ∩ bvars⇩s⇩t 𝒜 = {} ∧
tfr⇩s⇩t 𝒜 ∧
wf⇩t⇩r⇩m⇩s (trms⇩s⇩t 𝒜) ∧
Ana_invar_subst (ik⇩s⇩t 𝒜 ∪ assignment_rhs⇩s⇩t 𝒜)"

subsection ‹Definitions: GSMP Disjointness and Parallel Composability›
definition GSMP_disjoint where
"GSMP_disjoint P1 P2 Secrets ≡ GSMP P1 ∩ GSMP P2 ⊆ Secrets ∪ {m. {} ⊢⇩c m}"

definition declassified⇩l⇩s⇩t where
"declassified⇩l⇩s⇩t (𝒜::('fun,'var,'lbl) labeled_strand) ℐ ≡
{s. ⋃{set ts | ts. (⋆, Receive ts) ∈ set (𝒜 ⋅⇩l⇩s⇩t ℐ)} ⊢ s}"

definition par_comp where
"par_comp (𝒜::('fun,'var,'lbl) labeled_strand) (Secrets::('fun,'var) terms) ≡
(∀l1 l2. l1 ≠ l2 ⟶ GSMP_disjoint (trms_proj⇩l⇩s⇩t l1 𝒜) (trms_proj⇩l⇩s⇩t l2 𝒜) Secrets) ∧
(∀s ∈ Secrets. ¬{} ⊢⇩c s) ∧
ground Secrets"

definition strand_leaks⇩l⇩s⇩t where
"strand_leaks⇩l⇩s⇩t 𝒜 Sec ℐ ≡ (∃t ∈ Sec - declassified⇩l⇩s⇩t 𝒜 ℐ. ∃l. (ℐ ⊨ ⟨proj_unl l 𝒜@[Send1 t]⟩))"

subsection ‹Definitions: GSMP-Restricted Intruder Deduction Variant›
definition intruder_deduct_hom::
"('fun,'var) terms ⇒ ('fun,'var,'lbl) labeled_strand ⇒ ('fun,'var) term ⇒ bool"
("⟨_;_⟩ ⊢⇩G⇩S⇩M⇩P _" 50)
where
"⟨M; 𝒜⟩ ⊢⇩G⇩S⇩M⇩P t ≡ ⟨M; λt. t ∈ GSMP (trms⇩l⇩s⇩t 𝒜)⟩ ⊢⇩r t"

lemma intruder_deduct_hom_AxiomH[simp]:
assumes "t ∈ M"
shows "⟨M; 𝒜⟩ ⊢⇩G⇩S⇩M⇩P t"
using intruder_deduct_restricted.AxiomR[of t M] assms
unfolding intruder_deduct_hom_def
by blast

lemma intruder_deduct_hom_ComposeH[simp]:
assumes "length X = arity f" "public f" "⋀x. x ∈ set X ⟹ ⟨M; 𝒜⟩ ⊢⇩G⇩S⇩M⇩P x"
and "Fun f X ∈ GSMP (trms⇩l⇩s⇩t 𝒜)"
shows "⟨M; 𝒜⟩ ⊢⇩G⇩S⇩M⇩P Fun f X"
using intruder_deduct_restricted.ComposeR[of X f M "λt. t ∈ GSMP (trms⇩l⇩s⇩t 𝒜)"] assms
unfolding intruder_deduct_hom_def
by blast

lemma intruder_deduct_hom_DecomposeH:
assumes "⟨M; 𝒜⟩ ⊢⇩G⇩S⇩M⇩P t" "Ana t = (K, T)" "⋀k. k ∈ set K ⟹ ⟨M; 𝒜⟩ ⊢⇩G⇩S⇩M⇩P k" "t⇩i ∈ set T"
shows "⟨M; 𝒜⟩ ⊢⇩G⇩S⇩M⇩P t⇩i"
using intruder_deduct_restricted.DecomposeR[of M "λt. t ∈ GSMP (trms⇩l⇩s⇩t 𝒜)" t] assms
unfolding intruder_deduct_hom_def
by blast

lemma intruder_deduct_hom_induct[consumes 1, case_names AxiomH ComposeH DecomposeH]:
assumes "⟨M; 𝒜⟩ ⊢⇩G⇩S⇩M⇩P t" "⋀t. t ∈ M ⟹ P M t"
"⋀X f. ⟦length X = arity f; public f;
⋀x. x ∈ set X ⟹ ⟨M; 𝒜⟩ ⊢⇩G⇩S⇩M⇩P x;
⋀x. x ∈ set X ⟹ P M x;
Fun f X ∈ GSMP (trms⇩l⇩s⇩t 𝒜)
⟧ ⟹ P M (Fun f X)"
"⋀t K T t⇩i. ⟦⟨M; 𝒜⟩ ⊢⇩G⇩S⇩M⇩P t; P M t; Ana t = (K, T);
⋀k. k ∈ set K ⟹ ⟨M; 𝒜⟩ ⊢⇩G⇩S⇩M⇩P k;
⋀k. k ∈ set K ⟹ P M k; t⇩i ∈ set T⟧ ⟹ P M t⇩i"
shows "P M t"
using intruder_deduct_restricted_induct[of M "λt. t ∈ GSMP (trms⇩l⇩s⇩t 𝒜)" t "λM Q t. P M t"] assms
unfolding intruder_deduct_hom_def
by blast

lemma ideduct_hom_mono:
"⟦⟨M; 𝒜⟩ ⊢⇩G⇩S⇩M⇩P t; M ⊆ M'⟧ ⟹ ⟨M'; 𝒜⟩ ⊢⇩G⇩S⇩M⇩P t"
using ideduct_restricted_mono[of M _ t M']
unfolding intruder_deduct_hom_def
by fast

subsection ‹Lemmata: GSMP›
lemma GSMP_disjoint_empty[simp]:
"GSMP_disjoint {} A Sec" "GSMP_disjoint A {} Sec"
unfolding GSMP_disjoint_def GSMP_def by fastforce+

lemma GSMP_mono:
assumes "N ⊆ M"
shows "GSMP N ⊆ GSMP M"
using SMP_mono[OF assms] unfolding GSMP_def by fast

lemma GSMP_SMP_mono:
assumes "SMP N ⊆ SMP M"
shows "GSMP N ⊆ GSMP M"
using assms unfolding GSMP_def by fast

lemma GSMP_subterm:
assumes "t ∈ GSMP M" "t' ⊑ t"
shows "t' ∈ GSMP M"
using SMP.Subterm[of t M t'] ground_subterm[of t t'] assms unfolding GSMP_def by auto

lemma GSMP_subterms: "subterms⇩s⇩e⇩t (GSMP M) = GSMP M"
using GSMP_subterm[of _ M] by blast

lemma GSMP_Ana_key:
assumes "t ∈ GSMP M" "Ana t = (K,T)" "k ∈ set K"
shows "k ∈ GSMP M"
using SMP.Ana[of t M K T k] Ana_keys_fv[of t K T] assms unfolding GSMP_def by auto

lemma GSMP_union: "GSMP (A ∪ B) = GSMP A ∪ GSMP B"
using SMP_union[of A B] unfolding GSMP_def by auto

lemma GSMP_Union: "GSMP (trms⇩l⇩s⇩t A) = (⋃l. GSMP (trms_proj⇩l⇩s⇩t l A))"
proof -
define P where "P ≡ (λl. trms_proj⇩l⇩s⇩t l A)"
define Q where "Q ≡ trms⇩l⇩s⇩t A"
have "SMP (⋃l. P l) = (⋃l. SMP (P l))" "Q = (⋃l. P l)"
unfolding P_def Q_def by (metis SMP_Union, metis trms⇩l⇩s⇩t_union)
hence "GSMP Q = (⋃l. GSMP (P l))" unfolding GSMP_def by auto
thus ?thesis unfolding P_def Q_def by metis
qed

lemma in_GSMP_in_proj: "t ∈ GSMP (trms⇩l⇩s⇩t A) ⟹ ∃n. t ∈ GSMP (trms_proj⇩l⇩s⇩t n A)"
using GSMP_Union[of A] by blast

lemma in_proj_in_GSMP: "t ∈ GSMP (trms_proj⇩l⇩s⇩t n A) ⟹ t ∈ GSMP (trms⇩l⇩s⇩t A)"
using GSMP_Union[of A] by blast

lemma GSMP_disjointE:
assumes A: "GSMP_disjoint (trms_proj⇩l⇩s⇩t n A) (trms_proj⇩l⇩s⇩t m A) Sec"
shows "GSMP (trms_proj⇩l⇩s⇩t n A) ∩ GSMP (trms_proj⇩l⇩s⇩t m A) ⊆ Sec ∪ {m. {} ⊢⇩c m}"
using assms unfolding GSMP_disjoint_def by auto

lemma GSMP_disjoint_term:
assumes "GSMP_disjoint (trms_proj⇩l⇩s⇩t l 𝒜) (trms_proj⇩l⇩s⇩t l' 𝒜) Sec"
shows "t ∉ GSMP (trms_proj⇩l⇩s⇩t l 𝒜) ∨ t ∉ GSMP (trms_proj⇩l⇩s⇩t l' 𝒜) ∨ t ∈ Sec ∨ {} ⊢⇩c t"
using assms unfolding GSMP_disjoint_def by blast

lemma GSMP_wt_subst_subset:
assumes "t ∈ GSMP (M ⋅⇩s⇩e⇩t ℐ)" "wt⇩s⇩u⇩b⇩s⇩t ℐ" "wf⇩t⇩r⇩m⇩s (subst_range ℐ)"
shows "t ∈ GSMP M"
using SMP_wt_subst_subset[OF _ assms(2,3), of t M] assms(1) unfolding GSMP_def by simp

lemma GSMP_wt_substI:
assumes "t ∈ M" "wt⇩s⇩u⇩b⇩s⇩t I" "wf⇩t⇩r⇩m⇩s (subst_range I)" "interpretation⇩s⇩u⇩b⇩s⇩t I"
shows "t ⋅ I ∈ GSMP M"
proof -
have "t ∈ SMP M" using assms(1) by auto
hence *: "t ⋅ I ∈ SMP M" using SMP.Substitution assms(2,3) wf_trm_subst_range_iff[of I] by simp
moreover have "fv (t ⋅ I) = {}"
using assms(1) interpretation_grounds_all'[OF assms(4)]
by auto
ultimately show ?thesis unfolding GSMP_def by simp
qed

lemma GSMP_disjoint_subset:
assumes "GSMP_disjoint L R S" "L' ⊆ L" "R' ⊆ R"
shows "GSMP_disjoint L' R' S"
using assms(1) SMP_mono[OF assms(2)] SMP_mono[OF assms(3)]
by (auto simp add: GSMP_def GSMP_disjoint_def)

subsection ‹Lemmata: Intruder Knowledge and Declassification›
lemma declassified⇩l⇩s⇩t_alt_def:
"declassified⇩l⇩s⇩t 𝒜 ℐ = {s. (⋃{set ts | ts. (⋆, Receive ts) ∈ set 𝒜}) ⋅⇩s⇩e⇩t ℐ ⊢ s}"
proof -
have 0:
"(l, receive⟨ts⟩⇩s⇩t) ∈ set (𝒜 ⋅⇩l⇩s⇩t ℐ) = (∃ts'. (l, receive⟨ts'⟩⇩s⇩t) ∈ set 𝒜 ∧ ts = ts' ⋅⇩l⇩i⇩s⇩t ℐ)"
(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⟩⇩s⇩t) = a ⋅⇩l⇩s⇩t⇩p ℐ" using Cons.prems 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'⟩⇩s⇩t) ∧ ts = ts' ⋅⇩l⇩i⇩s⇩t ℐ" using Cons.prems by auto
thus ?thesis unfolding a by (cases b) auto
qed (use Cons.IH in auto)
qed simp
qed

let ?M = "λA. ⋃{set ts |ts. (⋆, receive⟨ts⟩⇩s⇩t) ∈ set A}"

have 1: "?M (𝒜 ⋅⇩l⇩s⇩t ℐ) = ?M 𝒜 ⋅⇩s⇩e⇩t ℐ" (is "?A = ?B")
proof
show "?A ⊆ ?B"
proof
fix t assume t: "t ∈ ?A"
then obtain ts where ts: "t ∈ set ts" "(⋆, receive⟨ts⟩⇩s⇩t) ∈ set (𝒜 ⋅⇩l⇩s⇩t ℐ)" 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 ⋅⇩s⇩e⇩t ℐ" "(⋆, receive⟨ts⟩⇩s⇩t) ∈ set 𝒜" by blast
hence "(⋆, receive⟨ts ⋅⇩l⇩i⇩s⇩t ℐ⟩⇩s⇩t) ∈ set (𝒜 ⋅⇩l⇩s⇩t ℐ)" using 0[of ⋆ "ts ⋅⇩l⇩i⇩s⇩t ℐ"] by blast
thus "t ∈ ?A" using ts(1) by force
qed
qed

show ?thesis using 1 unfolding declassified⇩l⇩s⇩t_def by argo
qed

"{t | t ts. (⋆, Receive ts) ∈ set 𝒜 ∧ t ∈ set ts} ⋅⇩s⇩e⇩t ℐ ⊆ declassified⇩l⇩s⇩t 𝒜 ℐ"
unfolding declassified⇩l⇩s⇩t_alt_def by (fastforce intro: intruder_deduct.Axiom)

lemma ik_proj_subst_GSMP_subset:
assumes I: "wt⇩s⇩u⇩b⇩s⇩t I" "wf⇩t⇩r⇩m⇩s (subst_range I)" "interpretation⇩s⇩u⇩b⇩s⇩t I"
shows "ik⇩s⇩t (proj_unl n A) ⋅⇩s⇩e⇩t I ⊆ GSMP (trms_proj⇩l⇩s⇩t n A)"
proof
fix t assume "t ∈ ik⇩s⇩t (proj_unl n A) ⋅⇩s⇩e⇩t I"
hence *: "t ∈ trms_proj⇩l⇩s⇩t n A ⋅⇩s⇩e⇩t I" by auto
then obtain s where "s ∈ trms_proj⇩l⇩s⇩t n A" "t = s ⋅ I" by auto
hence "t ∈ SMP (trms_proj⇩l⇩s⇩t n A)" using SMP_I I(1,2) wf_trm_subst_range_iff[of I] by simp
moreover have "fv t = {}"
using * interpretation_grounds_all'[OF I(3)]
by auto
ultimately show "t ∈ GSMP (trms_proj⇩l⇩s⇩t n A)" unfolding GSMP_def by simp
qed

lemma ik_proj_subst_subterms_GSMP_subset:
assumes I: "wt⇩s⇩u⇩b⇩s⇩t I" "wf⇩t⇩r⇩m⇩s (subst_range I)" "interpretation⇩s⇩u⇩b⇩s⇩t I"
shows "subterms⇩s⇩e⇩t (ik⇩s⇩t (proj_unl n A) ⋅⇩s⇩e⇩t I) ⊆ GSMP (trms_proj⇩l⇩s⇩t n A)" (is "?A ⊆ ?B")
proof
fix t assume "t ⊑⇩s⇩e⇩t ik⇩s⇩t (proj_unl n A) ⋅⇩s⇩e⇩t I"
then obtain s where "s ∈ ik⇩s⇩t (proj_unl n A) ⋅⇩s⇩e⇩t I" "t ⊑ s" by fast
thus "t ∈ ?B"
using ik_proj_subst_GSMP_subset[OF I, of n A] ground_subterm[of s t]
SMP.Subterm[of s "trms⇩l⇩s⇩t (proj n A)" t]
unfolding GSMP_def
by blast
qed

lemma declassified_proj_eq: "declassified⇩l⇩s⇩t A I = declassified⇩l⇩s⇩t (proj n A) I"
unfolding declassified⇩l⇩s⇩t_alt_def proj_def by auto

lemma declassified_prefix_subset:
assumes AB: "prefix A B"
shows "declassified⇩l⇩s⇩t A I ⊆ declassified⇩l⇩s⇩t B I"
proof
fix t assume t: "t ∈ declassified⇩l⇩s⇩t A I"
obtain C where C: "B = A@C" using prefixE[OF AB] by metis
show "t ∈ declassified⇩l⇩s⇩t B I"
using t ideduct_mono[of
"⋃{set ts |ts. (⋆, receive⟨ts⟩⇩s⇩t) ∈ set A} ⋅⇩s⇩e⇩t I" t
"⋃{set ts |ts. (⋆, receive⟨ts⟩⇩s⇩t) ∈ set B} ⋅⇩s⇩e⇩t I"]
unfolding C declassified⇩l⇩s⇩t_alt_def by auto
qed

lemma declassified_proj_ik_subset:
"declassified⇩l⇩s⇩t A I ⊆ {s. ik⇩s⇩t (proj_unl n A) ⋅⇩s⇩e⇩t I ⊢ s}"
(is "?A A ⊆ ?P A A")
proof -
have *: "⋃{set ts |ts. (⋆, receive⟨ts⟩⇩s⇩t) ∈ set A} ⋅⇩s⇩e⇩t I ⊆ ik⇩s⇩t (proj_unl n A) ⋅⇩s⇩e⇩t I"
using proj_ik⇩s⇩t_is_proj_rcv_set by fastforce
show ?thesis
using ideduct_mono[OF _ *] unfolding declassified⇩l⇩s⇩t_alt_def by blast
qed

lemma deduct_proj_priv_term_prefix_ex:
assumes A: "ik⇩s⇩t (proj_unl l A) ⋅⇩s⇩e⇩t I ⊢ t"
and t: "¬{} ⊢⇩c t"
shows "∃B k s. (k = ⋆ ∨ k = ln l) ∧ prefix (B@[(k,receive⟨s⟩⇩s⇩t)]) A ∧
declassified⇩l⇩s⇩t ((B@[(k,receive⟨s⟩⇩s⇩t)])) I = declassified⇩l⇩s⇩t A I ∧
ik⇩s⇩t (proj_unl l (B@[(k,receive⟨s⟩⇩s⇩t)])) = ik⇩s⇩t (proj_unl l A)"
using A
proof (induction A rule: List.rev_induct)
case Nil
have "ik⇩s⇩t (proj_unl l []) ⋅⇩s⇩e⇩t 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 = "∃ts. b = receive⟨ts⟩⇩s⇩t"

have 0: "ik⇩s⇩t (proj_unl l (A@[a])) = ik⇩s⇩t (proj_unl l A)" when "?P ⟹ ¬?Q"
using that ik⇩s⇩t_snoc_no_receive_eq[OF that, of I "proj_unl l A"]
unfolding ik⇩s⇩t_is_rcv_set a by (cases "k = ⋆ ∨ k = (ln l)") auto

have 1: "declassified⇩l⇩s⇩t (A@[a]) I = declassified⇩l⇩s⇩t A I" when "?P ⟹ ¬?Q"
using that snoc.prems unfolding declassified⇩l⇩s⇩t_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

subsection ‹Lemmata: Homogeneous and Heterogeneous Terms (Deprecated Theory)›
text ‹The following theory is no longer needed for the compositionality result›
context
begin
private definition proj_specific where
"proj_specific n t 𝒜 Secrets ≡ t ∈ GSMP (trms_proj⇩l⇩s⇩t n 𝒜) - (Secrets ∪ {m. {} ⊢⇩c m})"

private definition heterogeneous⇩l⇩s⇩t where
"heterogeneous⇩l⇩s⇩t t 𝒜 Secrets ≡ (
(∃l1 l2. ∃s1 ∈ subterms t. ∃s2 ∈ subterms t.
l1 ≠ l2 ∧ proj_specific l1 s1 𝒜 Secrets ∧ proj_specific l2 s2 𝒜 Secrets))"

private abbreviation homogeneous⇩l⇩s⇩t where
"homogeneous⇩l⇩s⇩t t 𝒜 Secrets ≡ ¬heterogeneous⇩l⇩s⇩t t 𝒜 Secrets"

private definition intruder_deduct_hom'::
"('fun,'var) terms ⇒ ('fun,'var,'lbl) labeled_strand ⇒ ('fun,'var) terms ⇒ ('fun,'var) term
⇒ bool" ("⟨_;_;_⟩ ⊢⇩h⇩o⇩m _" 50)
where
"⟨M; 𝒜; Sec⟩ ⊢⇩h⇩o⇩m t ≡ ⟨M; λt. homogeneous⇩l⇩s⇩t t 𝒜 Sec ∧ t ∈ GSMP (trms⇩l⇩s⇩t 𝒜)⟩ ⊢⇩r t"

private lemma GSMP_disjoint_fst_specific_not_snd_specific:
assumes "GSMP_disjoint (trms_proj⇩l⇩s⇩t l 𝒜) (trms_proj⇩l⇩s⇩t l' 𝒜) Sec" "l ≠ l'"
and "proj_specific l m 𝒜 Sec"
shows "¬proj_specific l' m 𝒜 Sec"
using assms by (fastforce simp add: GSMP_disjoint_def proj_specific_def)

private lemma GSMP_disjoint_snd_specific_not_fst_specific:
assumes "GSMP_disjoint (trms_proj⇩l⇩s⇩t l 𝒜) (trms_proj⇩l⇩s⇩t l' 𝒜) Sec"
and "proj_specific l' m 𝒜 Sec"
shows "¬proj_specific l m 𝒜 Sec"
using assms by (auto simp add: GSMP_disjoint_def proj_specific_def)

private lemma GSMP_disjoint_intersection_not_specific:
assumes "GSMP_disjoint (trms_proj⇩l⇩s⇩t l 𝒜) (trms_proj⇩l⇩s⇩t l' 𝒜) Sec"
and "t ∈ Sec ∨ {} ⊢⇩c t"
shows "¬proj_specific l t 𝒜 Sec" "¬proj_specific l t 𝒜 Sec"
using assms by (auto simp add: GSMP_disjoint_def proj_specific_def)

private lemma proj_specific_secrets_anti_mono:
assumes "proj_specific l t 𝒜 Sec" "Sec' ⊆ Sec"
shows "proj_specific l t 𝒜 Sec'"
using assms unfolding proj_specific_def by fast

private lemma heterogeneous_secrets_anti_mono:
assumes "heterogeneous⇩l⇩s⇩t t 𝒜 Sec" "Sec' ⊆ Sec"
shows "heterogeneous⇩l⇩s⇩t t 𝒜 Sec'"
using assms proj_specific_secrets_anti_mono unfolding heterogeneous⇩l⇩s⇩t_def by metis

private lemma homogeneous_secrets_mono:
assumes "homogeneous⇩l⇩s⇩t t 𝒜 Sec'" "Sec' ⊆ Sec"
shows "homogeneous⇩l⇩s⇩t t 𝒜 Sec"
using assms heterogeneous_secrets_anti_mono by blast

private lemma heterogeneous_supterm:
assumes "heterogeneous⇩l⇩s⇩t t 𝒜 Sec" "t ⊑ t'"
shows "heterogeneous⇩l⇩s⇩t t' 𝒜 Sec"
proof -
obtain l1 l2 s1 s2 where *:
"l1 ≠ l2"
"s1 ⊑ t" "proj_specific l1 s1 𝒜 Sec"
"s2 ⊑ t" "proj_specific l2 s2 𝒜 Sec"
using assms(1) unfolding heterogeneous⇩l⇩s⇩t_def by fast
thus ?thesis
using term.order_trans[OF *(2) assms(2)] term.order_trans[OF *(4) assms(2)]
qed

private lemma homogeneous_subterm:
assumes "homogeneous⇩l⇩s⇩t t 𝒜 Sec" "t' ⊑ t"
shows "homogeneous⇩l⇩s⇩t t' 𝒜 Sec"
by (metis assms heterogeneous_supterm)

private lemma proj_specific_subterm:
assumes "t ⊑ t'" "proj_specific l t' 𝒜 Sec"
shows "proj_specific l t 𝒜 Sec ∨ t ∈ Sec ∨ {} ⊢⇩c t"
using GSMP_subterm[OF _ assms(1)] assms(2) by (auto simp add: proj_specific_def)

private lemma heterogeneous_term_is_Fun:
assumes "heterogeneous⇩l⇩s⇩t t A S" shows "∃f T. t = Fun f T"
using assms by (cases t) (auto simp add: GSMP_def heterogeneous⇩l⇩s⇩t_def proj_specific_def)

private lemma proj_specific_is_homogeneous:
assumes 𝒜: "∀l l'. l ≠ l' ⟶ GSMP_disjoint (trms_proj⇩l⇩s⇩t l 𝒜) (trms_proj⇩l⇩s⇩t l' 𝒜) Sec"
and t: "proj_specific l m 𝒜 Sec"
shows "homogeneous⇩l⇩s⇩t m 𝒜 Sec"
proof
assume "heterogeneous⇩l⇩s⇩t m 𝒜 Sec"
then obtain s l' where s: "s ∈ subterms m" "proj_specific l' s 𝒜 Sec" "l ≠ l'"
unfolding heterogeneous⇩l⇩s⇩t_def by atomize_elim auto
hence "s ∈ GSMP (trms_proj⇩l⇩s⇩t l 𝒜)" "s ∈ GSMP (trms_proj⇩l⇩s⇩t l' 𝒜)"
using t by (auto simp add: GSMP_def proj_specific_def)
hence "s ∈ Sec ∨ {} ⊢⇩c s"
using 𝒜 s(3) by (auto simp add: GSMP_disjoint_def)
thus False using s(2) by (auto simp add: proj_specific_def)
qed

private lemma deduct_synth_homogeneous:
assumes "{} ⊢⇩c t"
shows "homogeneous⇩l⇩s⇩t t 𝒜 Sec"
proof -
have "∀s ∈ subterms t. {} ⊢⇩c s" using deduct_synth_subterm[OF assms] by auto
thus ?thesis unfolding heterogeneous⇩l⇩s⇩t_def proj_specific_def by auto
qed

private lemma GSMP_proj_is_homogeneous:
assumes "∀l l'. l ≠ l' ⟶ GSMP_disjoint (trms_proj⇩l⇩s⇩t l A) (trms_proj⇩l⇩s⇩t l' A) Sec"
and "t ∈ GSMP (trms_proj⇩l⇩s⇩t l A)" "t ∉ Sec"
shows "homogeneous⇩l⇩s⇩t t A Sec"
proof
assume "heterogeneous⇩l⇩s⇩t t A Sec"
then obtain s l' where s: "s ∈ subterms t" "proj_specific l' s A Sec" "l ≠ l'"
unfolding heterogeneous⇩l⇩s⇩t_def by atomize_elim auto
hence "s ∈ GSMP (trms_proj⇩l⇩s⇩t l A)" "s ∈ GSMP (trms_proj⇩l⇩s⇩t l' A)"
using assms by (auto simp add: GSMP_def proj_specific_def)
hence "s ∈ Sec ∨ {} ⊢⇩c s" using assms(1) s(3) by (auto simp add: GSMP_disjoint_def)
thus False using s(2) by (auto simp add: proj_specific_def)
qed

private lemma homogeneous_is_not_proj_specific:
assumes "homogeneous⇩l⇩s⇩t m 𝒜 Sec"
shows "∃l::'lbl. ¬proj_specific l m 𝒜 Sec"
proof -
let ?P = "λl s. proj_specific l s 𝒜 Sec"
have "∀l1 l2. ∀s1∈subterms m. ∀s2∈subterms m. (l1 ≠ l2 ⟶ (¬?P l1 s1 ∨ ¬?P l2 s2))"
using assms heterogeneous⇩l⇩s⇩t_def by metis
then obtain l1 l2 where "l1 ≠ l2" "¬?P l1 m ∨ ¬?P l2 m"
by (metis term.order_refl at_least_2_labels)
thus ?thesis by metis
qed

private lemma secrets_are_homogeneous:
assumes "∀s ∈ Sec. P s ⟶ (∀s' ∈ subterms s. {} ⊢⇩c s' ∨ s' ∈ Sec)" "s ∈ Sec" "P s"
shows "homogeneous⇩l⇩s⇩t s 𝒜 Sec"
using assms by (auto simp add: heterogeneous⇩l⇩s⇩t_def proj_specific_def)

private lemma GSMP_is_homogeneous:
assumes 𝒜: "∀l l'. l ≠ l' ⟶ GSMP_disjoint (trms_proj⇩l⇩s⇩t l 𝒜) (trms_proj⇩l⇩s⇩t l' 𝒜) Sec"
and t: "t ∈ GSMP (trms⇩l⇩s⇩t 𝒜)" "t ∉ Sec"
shows "homogeneous⇩l⇩s⇩t t 𝒜 Sec"
proof -
obtain n where n: "t ∈ GSMP (trms_proj⇩l⇩s⇩t n 𝒜)" using in_GSMP_in_proj[OF t(1)] by atomize_elim auto
show ?thesis using GSMP_proj_is_homogeneous[OF 𝒜 n t(2)] by metis
qed

private lemma GSMP_intersection_is_homogeneous:
assumes 𝒜: "∀l l'. l ≠ l' ⟶ GSMP_disjoint (trms_proj⇩l⇩s⇩t l 𝒜) (trms_proj⇩l⇩s⇩t l' 𝒜) Sec"
and t: "t ∈ GSMP (trms_proj⇩l⇩s⇩t l 𝒜) ∩ GSMP (trms_proj⇩l⇩s⇩t l' 𝒜)" "l ≠ l'"
shows "homogeneous⇩l⇩s⇩t t 𝒜 Sec"
proof -
define M where "M ≡ GSMP (trms_proj⇩l⇩s⇩t l 𝒜)"
define M' where "M' ≡ GSMP (trms_proj⇩l⇩s⇩t l' 𝒜)"

have t_in: "t ∈ M ∩ M'" "t ∈ GSMP (trms⇩l⇩s⇩t 𝒜)"
using t(1) in_proj_in_GSMP[of t _ 𝒜]
unfolding M_def M'_def by blast+

have "M ∩ M' ⊆ Sec ∪ {m. {} ⊢⇩c m}"
using 𝒜 GSMP_disjointE[of l 𝒜 l' Sec] t(2)
unfolding M_def M'_def by presburger
moreover have "subterms⇩s⇩e⇩t (M ∩ M') = M ∩ M'"
using GSMP_subterms unfolding M_def M'_def by blast
ultimately have *: "subterms⇩s⇩e⇩t (M ∩ M') ⊆ Sec ∪ {m. {} ⊢⇩c m}"
by blast

show ?thesis
proof (cases "t ∈ Sec")
case True thus ?thesis
using * secrets_are_homogeneous[of Sec "λt. t ∈ M ∩ M'", OF _ _ t_in(1)]
by fast
qed (metis GSMP_is_homogeneous[OF 𝒜 t_in(2)])
qed

private lemma GSMP_is_homogeneous':
assumes 𝒜: "∀l l'. l ≠ l' ⟶ GSMP_disjoint (trms_proj⇩l⇩s⇩t l 𝒜) (trms_proj⇩l⇩s⇩t l' 𝒜) Sec"
and t: "t ∈ GSMP (trms⇩l⇩s⇩t 𝒜)"
"t ∉ Sec - ⋃{GSMP (trms_proj⇩l⇩s⇩t l1 𝒜) ∩ GSMP (trms_proj⇩l⇩s⇩t l2 𝒜) | l1 l2. l1 ≠ l2}"
shows "homogeneous⇩l⇩s⇩t t 𝒜 Sec"
using GSMP_is_homogeneous[OF 𝒜 t(1)] GSMP_intersection_is_homogeneous[OF 𝒜] t(2)
by blast

private lemma Ana_keys_homogeneous:
assumes 𝒜: "∀l l'. l ≠ l' ⟶ GSMP_disjoint (trms_proj⇩l⇩s⇩t l 𝒜) (trms_proj⇩l⇩s⇩t l' 𝒜) Sec"
and t: "t ∈ GSMP (trms⇩l⇩s⇩t 𝒜)"
and k: "Ana t = (K,T)" "k ∈ set K"
"k ∉ Sec - ⋃{GSMP (trms_proj⇩l⇩s⇩t l1 𝒜) ∩ GSMP (trms_proj⇩l⇩s⇩t l2 𝒜) | l1 l2. l1 ≠ l2}"
shows "homogeneous⇩l⇩s⇩t k 𝒜 Sec"
proof (cases "k ∈ ⋃{GSMP (trms_proj⇩l⇩s⇩t l1 𝒜) ∩ GSMP (trms_proj⇩l⇩s⇩t l2 𝒜) | l1 l2. l1 ≠ l2}")
case False
hence "k ∉ Sec" using k(3) by fast
moreover have "k ∈ GSMP (trms⇩l⇩s⇩t 𝒜)"
using t SMP.Ana[OF _ k(1,2)] Ana_keys_fv[OF k(1)] k(2)
unfolding GSMP_def by auto
ultimately show ?thesis using GSMP_is_homogeneous[OF 𝒜, of k] by metis
qed (use GSMP_intersection_is_homogeneous[OF 𝒜] in blast)

end

subsection ‹Lemmata: Intruder Deduction Equivalences›
lemma deduct_if_hom_deduct: "⟨M;A⟩ ⊢⇩G⇩S⇩M⇩P m ⟹ M ⊢ m"
using deduct_if_restricted_deduct unfolding intruder_deduct_hom_def by blast

lemma hom_deduct_if_hom_ik:
assumes "⟨M;A⟩ ⊢⇩G⇩S⇩M⇩P m" "∀m ∈ M. m ∈ GSMP (trms⇩l⇩s⇩t A)"
shows "m ∈ GSMP (trms⇩l⇩s⇩t A)"
proof -
let ?Q = "λm. m ∈ GSMP (trms⇩l⇩s⇩t A)"
have "?Q t'" when "?Q t" "t' ⊑ t" for t t'
using GSMP_subterm[OF _ that(2)] that(1)
by blast
thus ?thesis
using assms(1) restricted_deduct_if_restricted_ik[OF _ assms(2)]
unfolding intruder_deduct_hom_def
by blast
qed

lemma deduct_hom_if_synth:
assumes hom: "m ∈ GSMP (trms⇩l⇩s⇩t 𝒜)"
and m: "M ⊢⇩c m"
shows "⟨M; 𝒜⟩ ⊢⇩G⇩S⇩M⇩P m"
proof -
let ?Q = "λm. m ∈ GSMP (trms⇩l⇩s⇩t 𝒜)"
have "?Q t'" when "?Q t" "t' ⊑ t" for t t'
using GSMP_subterm[OF _ that(2)] that(1)
by blast
thus ?thesis
using assms deduct_restricted_if_synth[of ?Q]
unfolding intruder_deduct_hom_def
by blast
qed

lemma hom_deduct_if_deduct:
assumes M: "∀m ∈ M. m ∈ GSMP (trms⇩l⇩s⇩t 𝒜)"
and m: "M ⊢ m" "m ∈ GSMP (trms⇩l⇩s⇩t 𝒜)"
shows "⟨M; 𝒜⟩ ⊢⇩G⇩S⇩M⇩P m"
proof -
let ?P = "λx. x ∈ GSMP (trms⇩l⇩s⇩t 𝒜)"

(*   have GSMP_hom: "homogeneous⇩l⇩s⇩t t 𝒜 Sec" when "t ∈ GSMP (trms⇩l⇩s⇩t 𝒜)" for t
using 𝒜 GSMP_is_homogeneous[of 𝒜 Sec t]
secrets_are_homogeneous[of Sec "λx. True" t 𝒜] that
unfolding par_comp_def by blast *)

have P_Ana: "?P k" when "?P t" "Ana t = (K, T)" "k ∈ set K" for t K T k
using GSMP_Ana_key[OF _ that(2,3), of "trms⇩l⇩s⇩t 𝒜"] that (* GSMP_hom *)
by presburger

have P_subterm: "?P t'" when "?P t" "t' ⊑ t" for t t'
using GSMP_subterm[of _ "trms⇩l⇩s⇩t 𝒜"] (* homogeneous_subterm[of _ 𝒜 Sec] *) that
by blast

have P_m: "?P m"
using (* GSMP_hom[OF m(2)] *) m(2)
by metis

show ?thesis
using restricted_deduct_if_deduct'[OF M _ _ m(1) P_m] P_Ana P_subterm
unfolding intruder_deduct_hom_def
by fast
qed

subsection ‹Lemmata: Deduction Reduction of Parallel Composable Constraints›
lemma par_comp_hom_deduct:
assumes 𝒜: "par_comp 𝒜 Sec"
and M: "∀l. M l ⊆ GSMP (trms_proj⇩l⇩s⇩t l 𝒜)"
"∀l. Discl ⊆ {s. M l ⊢ s}"
and Sec: "∀l. ∀s ∈ Sec - Discl. ¬(⟨M l; 𝒜⟩ ⊢⇩G⇩S⇩M⇩P s)"
and t: "⟨⋃l. M l; 𝒜⟩ ⊢⇩G⇩S⇩M⇩P t"
shows "t ∉ Sec - Discl" (is ?A)
"∀l. t ∈ GSMP (trms_proj⇩l⇩s⇩t l 𝒜) ⟶ ⟨M l; 𝒜⟩ ⊢⇩G⇩S⇩M⇩P t" (is ?B)
proof -
have M': "∀l. ∀m ∈ M l. m ∈ GSMP (trms⇩l⇩s⇩t 𝒜)"
proof (intro allI ballI)
fix l m show "m ∈ M l ⟹ m ∈ GSMP (trms⇩l⇩s⇩t 𝒜)" using M(1) in_proj_in_GSMP[of m l 𝒜] by blast
qed

have Discl_hom_deduct: "⟨M l; 𝒜⟩ ⊢⇩G⇩S⇩M⇩P u" when u: "u ∈ Discl" "u ∈ GSMP (trms⇩l⇩s⇩t 𝒜)" for l u
proof-
have "M l ⊢ u" using M(2) u by auto
thus ?thesis using hom_deduct_if_deduct[of "M l" 𝒜 u] M(1) M' u by auto
qed

show ?A ?B using t
proof (induction t rule: intruder_deduct_hom_induct)
case (AxiomH t)
then obtain lt where t_in_proj_ik: "t ∈ M lt" by atomize_elim auto
show t_not_Sec: "t ∉ Sec - Discl"
proof
assume "t ∈ Sec - Discl"
hence "∀l. ¬(⟨M l; 𝒜⟩ ⊢⇩G⇩S⇩M⇩P t)" using Sec by auto
thus False using intruder_deduct_hom_AxiomH[OF t_in_proj_ik] by metis
qed

have 1: "∀l. t ∈ M l ⟶ t ∈ GSMP (trms_proj⇩l⇩s⇩t l 𝒜)"
using M(1,2) AxiomH by auto

have 3: "{} ⊢⇩c t ∨ t ∈ Discl"
when "l1 ≠ l2" "t ∈ GSMP (trms_proj⇩l⇩s⇩t l1 𝒜) ∩ GSMP (trms_proj⇩l⇩s⇩t l2 𝒜)" for l1 l2
using 𝒜 t_not_Sec that by (auto simp add: par_comp_def GSMP_disjoint_def)

have 4: "t ∈ GSMP (trms⇩l⇩s⇩t 𝒜)" using M(1) M' t_in_proj_ik by auto

show "∀l. t ∈ GSMP (trms_proj⇩l⇩s⇩t l 𝒜) ⟶ ⟨M l; 𝒜⟩ ⊢⇩G⇩S⇩M⇩P t"
by (metis (lifting) Int_iff empty_subsetI
1 3 4 Discl_hom_deduct t_in_proj_ik
intruder_deduct_hom_AxiomH[of t _ 𝒜]
deduct_hom_if_synth[of t 𝒜 "{}"]
ideduct_hom_mono[of "{}" 𝒜 t])
next
case (ComposeH T f)
show "∀l. Fun f T ∈ GSMP (trms_proj⇩l⇩s⇩t l 𝒜) ⟶ ⟨M l; 𝒜⟩ ⊢⇩G⇩S⇩M⇩P Fun f T"
proof (intro allI impI)
fix l
assume "Fun f T ∈ GSMP (trms_proj⇩l⇩s⇩t l 𝒜)"
hence "t ∈ GSMP (trms_proj⇩l⇩s⇩t l 𝒜)" when "t ∈ set T" for t
using that GSMP_subterm[OF _ subtermeqI''] by auto
thus "⟨M l; 𝒜⟩ ⊢⇩G⇩S⇩M⇩P Fun f T"
using ComposeH.IH(2) intruder_deduct_hom_ComposeH[OF ComposeH.hyps(1,2) _ ComposeH.hyps(4)]
by simp
qed
thus "Fun f T ∉ Sec - Discl"
using Sec ComposeH.hyps(4) trms⇩l⇩s⇩t_union[of 𝒜] GSMP_Union[of 𝒜] by blast
next
case (DecomposeH t K T t⇩i)
have ti_subt: "t⇩i ⊑ t" using Ana_subterm[OF DecomposeH.hyps(2)] ‹t⇩i ∈ set T› by auto
have t: "t ∈ GSMP (trms⇩l⇩s⇩t 𝒜)" using DecomposeH.hyps(1) hom_deduct_if_hom_ik M(1) M' by auto
have ti: "t⇩i ∈ GSMP (trms⇩l⇩s⇩t 𝒜)"
using intruder_deduct_hom_DecomposeH[OF DecomposeH.hyps] hom_deduct_if_hom_ik M(1) M' by auto

obtain l where l: "t ∈ GSMP (trms_proj⇩l⇩s⇩t l 𝒜)"
using in_GSMP_in_proj[of _ 𝒜] ti t by presburger

have K_IH: "⟨M l; 𝒜⟩ ⊢⇩G⇩S⇩M⇩P k" when "k ∈ set K" for k
using that GSMP_Ana_key[OF _ DecomposeH.hyps(2)] DecomposeH.IH(4) l by auto

have ti_IH: "⟨M l; 𝒜⟩ ⊢⇩G⇩S⇩M⇩P t⇩i"
using K_IH DecomposeH.IH(2) l
intruder_deduct_hom_DecomposeH[OF _ DecomposeH.hyps(2) _ ‹t⇩i ∈ set T›]
by blast
thus ti_not_Sec: "t⇩i ∉ Sec - Discl" using Sec by blast

have "{} ⊢⇩c t⇩i ∨ t⇩i ∈ Discl" when "t⇩i ∈ GSMP (trms_proj⇩l⇩s⇩t l' 𝒜)" "l' ≠ l" for l'
proof -
have "GSMP_disjoint (trms_proj⇩l⇩s⇩t l' 𝒜) (trms_proj⇩l⇩s⇩t l 𝒜) Sec"
using that(2) 𝒜 by (simp add: par_comp_def)
thus ?thesis
using ti_not_Sec GSMP_subterm[OF l ti_subt] that(1) by (auto simp add: GSMP_disjoint_def)
qed
hence "⟨M l'; 𝒜⟩ ⊢⇩G⇩S⇩M⇩P t⇩i" when "t⇩i ∈ GSMP (trms_proj⇩l⇩s⇩t l' 𝒜)" "l' ≠ l" for l'
using that Discl_hom_deduct[OF _ ti]
deduct_hom_if_synth[OF ti, THEN ideduct_hom_mono[OF _ empty_subsetI]]
by (cases "t⇩i ∈ Discl") simp_all
thus "∀l. t⇩i ∈ GSMP (trms_proj⇩l⇩s⇩t l 𝒜) ⟶ ⟨M l; 𝒜⟩ ⊢⇩G⇩S⇩M⇩P t⇩i"
using ti_IH by blast
qed
qed

lemma par_comp_deduct_proj:
assumes 𝒜: "par_comp 𝒜 Sec"
and M: "∀l. M l ⊆ GSMP (trms_proj⇩l⇩s⇩t l 𝒜)"
"∀l. Discl ⊆ {s. M l ⊢ s}"
and t: "(⋃l. M l) ⊢ t" "t ∈ GSMP (trms_proj⇩l⇩s⇩t l 𝒜)"
shows "M l ⊢ t ∨ (∃s ∈ Sec - Discl. ∃l. M l ⊢ s)"
using t
proof (induction t rule: intruder_deduct_induct)
case (Axiom t)
then obtain l' where t_in_ik_proj: "t ∈ M l'" by atomize_elim auto
show ?case
proof (cases "t ∈ Sec - Discl ∨ {} ⊢⇩c t")
case True thus ?thesis
by (cases "t ∈ Sec - Discl")
(metis intruder_deduct.Axiom[OF t_in_ik_proj],
use ideduct_mono[of "{}" t "M l"] in blast)
next
case False
hence "t ∉ Sec - Discl" "¬{} ⊢⇩c t" "t ∈ GSMP (trms_proj⇩l⇩s⇩t l 𝒜)" using Axiom by auto
hence "(∀l'. l ≠ l' ⟶ t ∉ GSMP (trms_proj⇩l⇩s⇩t l' 𝒜)) ∨ t ∈ Discl"
using 𝒜 unfolding GSMP_disjoint_def par_comp_def by auto
hence "(∀l'. l ≠ l' ⟶ t ∉ GSMP (trms_proj⇩l⇩s⇩t l' 𝒜)) ∨ M l ⊢ t ∨ {} ⊢⇩c t"
using M by blast
thus ?thesis
by (cases "∃s ∈ M l. t ⊑ s ∧ {s} ⊢ t")
(blast intro: ideduct_mono[of _ t "M l"],
metis (no_types, lifting) False M(1) intruder_deduct.Axiom subsetCE t_in_ik_proj)
qed
next
case (Compose T f)
hence "Fun f T ∈ GSMP (trms_proj⇩l⇩s⇩t l 𝒜)" using Compose.prems by auto
hence "t ∈ GSMP (trms_proj⇩l⇩s⇩t l 𝒜)" when "t ∈ set T" for t using that unfolding GSMP_def by auto
hence IH: "M l ⊢ t ∨ (∃s ∈ Sec - Discl. ∃l. M l ⊢ s)" when "t ∈ set T" for t
using that Compose.IH by auto
show ?case
by (cases "∀t ∈ set T. M l ⊢ t")
(metis intruder_deduct.Compose[OF Compose.hyps(1,2)], metis IH)
next
case (Decompose t K T t⇩i)
have hom_ik: "m ∈ GSMP (trms⇩l⇩s⇩t 𝒜)" when m: "m ∈ M l" for m l
using in_proj_in_GSMP[of m l 𝒜] M(1) m by blast

have "⟨⋃l. M l; 𝒜⟩ ⊢⇩G⇩S⇩M⇩P t⇩i"
using intruder_deduct.Decompose[OF Decompose.hyps]
hom_deduct_if_deduct[of "⋃l. M l"] hom_ik in_proj_in_GSMP[OF Decompose.prems(1)]
by blast
hence "(⟨M l; 𝒜⟩ ⊢⇩G⇩S⇩M⇩P t⇩i) ∨ (∃s ∈ Sec-Discl. ∃l. ⟨M l; 𝒜⟩ ⊢⇩G⇩S⇩M⇩P s)"
using par_comp_hom_deduct(2)[OF 𝒜 M] Decompose.prems(1)
by blast
thus ?case using deduct_if_hom_deduct[of _ 𝒜] by auto
qed

subsection ‹Theorem: Parallel Compositionality for Labeled Constraints›
lemma par_comp_prefix: assumes "par_comp (A@B) M" shows "par_comp A M"
proof -
let ?L = "λl. trms_proj⇩l⇩s⇩t l A ∪ trms_proj⇩l⇩s⇩t l B"
have "GSMP_disjoint (?L l1) (?L l2) M" when "l1 ≠ l2" for l1 l2
using that assms unfolding par_comp_def
by (metis trms⇩s⇩t_append proj_append(2) unlabel_append)
hence "GSMP_disjoint (trms_proj⇩l⇩s⇩t l1 A) (trms_proj⇩l⇩s⇩t l2 A) M" when "l1 ≠ l2" for l1 l2
using that SMP_union by (auto simp add: GSMP_def GSMP_disjoint_def)
thus ?thesis using assms unfolding par_comp_def by blast
qed

theorem par_comp_constr_typed:
assumes 𝒜: "par_comp 𝒜 Sec"
and ℐ: "ℐ ⊨ ⟨unlabel 𝒜⟩" "interpretation⇩s⇩u⇩b⇩s⇩t ℐ" "wt⇩s⇩u⇩b⇩s⇩t ℐ" "wf⇩t⇩r⇩m⇩s (subst_range ℐ)"
shows "(∀l. (ℐ ⊨ ⟨proj_unl l 𝒜⟩)) ∨
(∃𝒜' l' t. prefix 𝒜' 𝒜 ∧ suffix [(l', receive⟨t⟩⇩s⇩t)] 𝒜' ∧ (strand_leaks⇩l⇩s⇩t 𝒜' Sec ℐ))"
proof -
let ?sem = "λ𝒜. ⟦{}; 𝒜⟧⇩d ℐ"
let ?Q = "λ𝒜. ∀l. ?sem (proj_unl l 𝒜)"
let ?L = "λ𝒜'. ∃t ∈ Sec - declassified⇩l⇩s⇩t 𝒜' ℐ. ∃l. ?sem (proj_unl l 𝒜'@[send⟨[t]⟩⇩s⇩t])"
let ?P = "λ𝒜 𝒜' l' ts. prefix (𝒜'@[(l',receive⟨ts⟩⇩s⇩t)]) 𝒜 ∧ ?L (𝒜'@[(l',receive⟨ts⟩⇩s⇩t)])"

have "⟦{}; unlabel 𝒜⟧⇩d ℐ" using ℐ by (simp add: constr_sem_d_def)
with 𝒜 have aux: "?Q 𝒜 ∨ (∃𝒜'. prefix 𝒜' 𝒜 ∧ ?L 𝒜')"
proof (induction "unlabel 𝒜" arbitrary: 𝒜 rule: List.rev_induct)
case Nil
hence "𝒜 = []" using unlabel_nil_only_if_nil by simp
thus ?case by auto
next
case (snoc b B 𝒜)
hence disj: "GSMP_disjoint (trms_proj⇩l⇩s⇩t l1 𝒜) (trms_proj⇩l⇩s⇩t l2 𝒜) Sec"
when "l1 ≠ l2" for l1 l2
using that by (auto simp add: par_comp_def)

obtain a A n where a: "𝒜 = A@[a]" "a = (ln n, b) ∨ a = (⋆, b)"
using unlabel_snoc_inv[OF snoc.hyps(2)[symmetric]] by atomize_elim auto
hence A: "𝒜 = A@[(ln n, b)] ∨ 𝒜 = A@[(⋆, b)]" by metis

have 1: "B = unlabel A" using a snoc.hyps(2) unlabel_append[of A "[a]"] by auto
have 2: "par_comp A Sec" using par_comp_prefix snoc.prems(1) a by metis
have 3: "⟦{}; unlabel A⟧⇩d ℐ" by (metis 1 snoc.prems(2) snoc.hyps(2) strand_sem_split(3))
have IH: "(∀l. ⟦{}; proj_unl l A⟧⇩d ℐ) ∨ (∃𝒜'. prefix 𝒜' A ∧ ?L 𝒜')"
by (rule snoc.hyps(1)[OF 1 2 3])

show ?case
proof (cases "∀l. ⟦{}; proj_unl l A⟧⇩d ℐ")
case False
then obtain 𝒜' where 𝒜': "prefix 𝒜' A" "?L 𝒜'" by (metis IH)
hence "prefix 𝒜' (A@[a])" using a prefix_prefix[of _ A "[a]"] by simp
thus ?thesis using 𝒜'(2) a by auto
next
case True
note IH' = True
show ?thesis
proof (cases b)
case (Send ts)
hence "∀t ∈ set ts. ik⇩s⇩t (unlabel A) ⋅⇩s⇩e⇩t ℐ ⊢ t ⋅ ℐ"
using a ‹⟦{}; unlabel 𝒜⟧⇩d ℐ› strand_sem_split(2)[of "{}" "unlabel A" "unlabel [a]" ℐ]
unlabel_append[of A "[a]"]
by auto
hence *: "∀t ∈ set ts. (⋃l. (ik⇩s⇩t (proj_unl l A) ⋅⇩s⇩e⇩t ℐ)) ⊢ t ⋅ ℐ"
using proj_ik_union_is_unlabel_ik image_UN by metis

have "ik⇩s⇩t (proj_unl l 𝒜) = ik⇩s⇩t (proj_unl l A)" for l
using Send A
by (metis append_Nil2 ik⇩s⇩t.simps(3) proj_unl_cons(3) proj_nil(2)
singleton_lst_proj(1,2) proj_ik_append)
hence **: "ik⇩s⇩t (proj_unl l A) ⋅⇩s⇩e⇩t ℐ ⊆ GSMP (trms_proj⇩l⇩s⇩t l 𝒜)" for l
using ik_proj_subst_GSMP_subset[OF ℐ(3,4,2), of _ 𝒜]
by auto

note Discl =
declassified_proj_ik_subset(1)[of A ℐ]

have Sec: "ground Sec"
using 𝒜 by (auto simp add: par_comp_def)

(*         have Sec_hom: "homogeneous⇩l⇩s⇩t s 𝒜 Sec" when "s ∈ Sec" for s
using that secrets_are_homogeneous[of Sec "λ_. True" s 𝒜] snoc.prems(1)
unfolding par_comp_def by auto *)

have "∀m∈ik⇩s⇩t (proj_unl l 𝒜) ⋅⇩s⇩e⇩t ℐ. m ∈ GSMP (trms⇩l⇩s⇩t 𝒜)"
"ik⇩s⇩t (proj_unl l 𝒜) ⋅⇩s⇩e⇩t ℐ ⊆ GSMP (trms_proj⇩l⇩s⇩t l 𝒜)"
for l
using ik_proj_subst_GSMP_subset[OF ℐ(3,4,2), of _ 𝒜] GSMP_Union[of 𝒜] by auto
moreover have "ik⇩s⇩t (proj_unl l [a]) = {}" for l
using Send proj_ik⇩s⇩t_is_proj_rcv_set[of _ "[a]"] a(2) by auto
ultimately have M: "∀l. ik⇩s⇩t (proj_unl l A) ⋅⇩s⇩e⇩t ℐ ⊆ GSMP (trms_proj⇩l⇩s⇩t l 𝒜)"
using a(1) proj_ik_append[of _ A "[a]"] by auto

have prefix_A: "prefix A 𝒜" using A by auto

have "s ⋅ ℐ = s"
when "s ∈ Sec" for s
using that Sec by auto
hence leakage_case: "⟦{}; proj_unl l A@[Send1 s]⟧⇩d ℐ"
when "s ∈ Sec - declassified⇩l⇩s⇩t A ℐ" "ik⇩s⇩t (proj_unl l A) ⋅⇩s⇩e⇩t ℐ ⊢ s" for l s
using that strand_sem_append(2) IH' by auto

have proj_deduct_case_n:
"∀m. m ≠ n ⟶ ⟦{}; proj_unl m (A@[a])⟧⇩d ℐ"
"∀t ∈ set ts. ik⇩s⇩t (proj_unl n A) ⋅⇩s⇩e⇩t ℐ ⊢ t ⋅ ℐ ⟹ ⟦{}; proj_unl n (A@[a])⟧⇩d ℐ"
when "a = (ln n, Send ts)"
using that IH' proj_append(2)[of _ A] by auto

have proj_deduct_case_star:
"⟦{}; proj_unl l (A@[a])⟧⇩d ℐ"
when "a = (⋆, Send ts)" "∀t ∈ set ts. ik⇩s⇩t (proj_unl l A) ⋅⇩s⇩e⇩t ℐ ⊢ t ⋅ ℐ" for l
using that IH' proj_append(2)[of _ A] by auto

show ?thesis
proof (cases "∃l. ∃m ∈ ik⇩s⇩t (proj_unl l A) ⋅⇩s⇩e⇩t ℐ. m ∈ Sec - declassified⇩l⇩s⇩t A ℐ")
case True
then obtain l s where ls: "s ∈ Sec - declassified⇩l⇩s⇩t A ℐ" "ik⇩s⇩t (proj_unl l A) ⋅⇩s⇩e⇩t ℐ ⊢ s"
using intruder_deduct.Axiom by metis
thus ?thesis using leakage_case prefix_A by blast
next
case False
have A_decl_subset:
"∀l. declassified⇩l⇩s⇩t A ℐ ⊆ {s. ik⇩s⇩t (proj_unl l A) ⋅⇩s⇩e⇩t ℐ ⊢ s}"
using Discl unfolding a(1) by auto

note deduct_proj_lemma = par_comp_deduct_proj[OF snoc.prems(1) M A_decl_subset]

from a(2) show ?thesis
proof
assume "a = (ln n, b)"
hence "a = (ln n, Send ts)" "∀t ∈ set ts. t ⋅ ℐ ∈ GSMP (trms_proj⇩l⇩s⇩t n 𝒜)"
using Send a(1) trms_proj⇩l⇩s⇩t_append[of n A "[a]"]
GSMP_wt_substI[OF _ ℐ(3,4,2)]
by (metis, force)
hence
"a = (ln n, Send ts)"
"∀m. m ≠ n ⟶ ⟦{}; proj_unl m (A@[a])⟧⇩d ℐ"
"∀t ∈ set ts. ik⇩s⇩t (proj_unl n A) ⋅⇩s⇩e⇩t ℐ ⊢ t ⋅ ℐ ⟹ ⟦{}; proj_unl n (A@[a])⟧⇩d ℐ"
"∀t ∈ set ts. t ⋅ ℐ ∈ GSMP (trms_proj⇩l⇩s⇩t n 𝒜)"
using proj_deduct_case_n
by auto
hence "(∀l. ⟦{}; proj_unl l 𝒜⟧⇩d ℐ) ∨
(∃s ∈ Sec-declassified⇩l⇩s⇩t A ℐ. ∃l. ik⇩s⇩t (proj_unl l A) ⋅⇩s⇩e⇩t ℐ ⊢ s)"
using deduct_proj_lemma * unfolding a(1) list_all_iff by metis
thus ?thesis using leakage_case prefix_A by metis
next
assume "a = (⋆, b)"
hence ***: "a = (⋆, Send ts)" "list_all (λt. t ⋅ ℐ ∈ GSMP (trms_proj⇩l⇩s⇩t l 𝒜)) ts" for l
using Send a(1) GSMP_wt_substI[OF _ ℐ(3,4,2)] unfolding list_all_iff by (metis, force)
hence "t ⋅ ℐ ∈ Sec - declassified⇩l⇩s⇩t A ℐ ∨
t ⋅ ℐ ∈ declassified⇩l⇩s⇩t A ℐ ∨
t ⋅ ℐ ∈ {m. {} ⊢⇩c m}"
when "t ∈ set ts" for t
using that snoc.prems(1) a(1) at_least_2_labels
unfolding par_comp_def GSMP_disjoint_def list_all_iff
by blast
hence "(∃t ∈ set ts. t ⋅ ℐ ∈ Sec - declassified⇩l⇩s⇩t A ℐ) ∨
(∀t ∈ set ts. t ⋅ ℐ ∈ declassified⇩l⇩s⇩t A ℐ ∨ t ⋅ ℐ ∈ {m. {} ⊢⇩c m})"
by blast
thus ?thesis
proof
assume "∃t ∈ set ts. t ⋅ ℐ ∈ Sec - declassified⇩l⇩s⇩t A ℐ"
then obtain t where t:
"t ∈ set ts" "t ⋅ ℐ ∈ Sec - declassified⇩l⇩s⇩t A ℐ"
"(⋃l. ik⇩s⇩t (proj_unl l A) ⋅⇩s⇩e⇩t ℐ) ⊢ t ⋅ ℐ"
using * unfolding list_all_iff by blast
have "∃s ∈ Sec - declassified⇩l⇩s⇩t A ℐ. ∃l. ik⇩s⇩t (proj_unl l A) ⋅⇩s⇩e⇩t ℐ ⊢ s"
using t(1,2) deduct_proj_lemma[OF t(3)] ***(2) A a Discl
unfolding list_all_iff by blast
thus ?thesis using prefix_A leakage_case by blast
next
assume t: "∀t ∈ set ts. t ⋅ ℐ ∈ declassified⇩l⇩s⇩t A ℐ ∨ t ⋅ ℐ ∈ {m. {} ⊢⇩c m}"
moreover {
fix t l assume "t ∈ set ts" "t ⋅ ℐ ∈ declassified⇩l⇩s⇩t A ℐ"
hence "ik⇩s⇩t (proj_unl l A) ⋅⇩s⇩e⇩t ℐ ⊢ t ⋅ ℐ"
using intruder_deduct.Axiom Discl(1)[of l]
ideduct_mono[of _ "t ⋅ ℐ" "ik⇩s⇩t (proj_unl l A) ⋅⇩s⇩e⇩t ℐ"]
by blast
} moreover {
fix t l assume "t ∈ set ts" "t ⋅ ℐ ∈ {m. {} ⊢⇩c m}"
hence "ik⇩s⇩t (proj_unl l A) ⋅⇩s⇩e⇩t ℐ ⊢ t ⋅ ℐ"
using ideduct_mono[OF deduct_if_synth] by blast
} ultimately have "∀t ∈ set ts. ik⇩s⇩t (proj_unl l A) ⋅⇩s⇩e⇩t ℐ ⊢ t ⋅ ℐ" for l
by blast
thus ?thesis using proj_deduct_case_star[OF ***(1)] a(1) by fast
qed
qed
qed
next
hence "⟦{}; proj_unl l 𝒜⟧⇩d ℐ" for l
using IH' a proj_append(2)[of l A "[a]"]
unfolding unlabel_def proj_def by auto
thus ?thesis by metis
next
case (Equality ac t t')
hence *: "⟦M; [Equality ac t t']⟧⇩d ℐ" for M
using a ‹⟦{}; unlabel 𝒜⟧⇩d ℐ› unlabel_append[of A "[a]"]
by auto
show ?thesis
using a proj_append(2)[of _ A "[a]"] Equality
strand_sem_append(2)[OF _ *] IH'
unfolding unlabel_def proj_def by auto
next
case (Inequality X F)
hence *: "⟦M; [Inequality X F]⟧⇩d ℐ" for M
using a ‹⟦{}; unlabel 𝒜⟧⇩d ℐ› unlabel_append[of A "[a]"]
by auto
show ?thesis
using a proj_append(2)[of _ A "[a]"] Inequality
strand_sem_append(2)[OF _ *] IH'
unfolding unlabel_def proj_def by auto
qed
qed
qed

from aux have "?Q 𝒜 ∨ (∃𝒜' l' t. ?P 𝒜 𝒜' l' t)"
proof
assume "∃𝒜'. prefix 𝒜' 𝒜 ∧ ?L 𝒜'"
then obtain 𝒜' t l where 𝒜':
"prefix 𝒜' 𝒜" "t ∈ Sec - declassified⇩l⇩s⇩t 𝒜' ℐ" "?sem (proj_unl l 𝒜'@[send⟨[t]⟩⇩s⇩t])"
by blast

have *: "ik⇩s⇩t (proj_unl l 𝒜') ⋅⇩s⇩e⇩t ℐ ⊢ t ⋅ ℐ" "¬{} ⊢⇩c t ⋅ ℐ"
using 𝒜'(2) 𝒜 subst_ground_ident[of t ℐ] strand_sem_split(4)[OF 𝒜'(3)]
unfolding par_comp_def by (simp, fastforce)

obtain B k s where B:
"k = ⋆ ∨ k = ln l" "prefix (B@[(k, receive⟨s⟩⇩s⇩t)]) 𝒜'"
"declassified⇩l⇩s⇩t (B@[(k, receive⟨s⟩⇩s⇩t)]) ℐ = declassified⇩l⇩s⇩t 𝒜' ℐ"
"ik⇩s⇩t (proj_unl l (B@[(k, receive⟨s⟩⇩s⇩t)])) = ik⇩s⇩t (proj_unl l 𝒜')"
using deduct_proj_priv_term_prefix_ex[OF *] by force

have "prefix (B@[(k, receive⟨s⟩⇩s⇩t)]) 𝒜" using B(2) 𝒜'(1) unfolding prefix_def by force
moreover have "t ∈ Sec - declassified⇩l⇩s⇩t (B@[(k, receive⟨s⟩⇩s⇩t)]) ℐ" using B(3) 𝒜'(2) by blast
moreover have "?sem (proj_unl l (B@[(k, receive⟨s⟩⇩s⇩t)])@[send⟨[t]⟩⇩s⇩t])"
using *(1)[unfolded B(4)[symmetric]]
prefix_proj(2)[OF B(2), of l, unfolded prefix_def]
strand_sem_split(3)[OF 𝒜'(3)]
strand_sem_append(2)[
of _ _ ℐ  "[send⟨[t]⟩⇩s⇩t]",
OF strand_sem_split(3)[of "{}" "proj_unl l (B@[(k, receive⟨s⟩⇩s⇩t)])"]]
by force
ultimately show ?thesis by blast
qed simp
thus ?thesis
using ℐ(1) unfolding strand_leaks⇩l⇩s⇩t_def suffix_def constr_sem_d_def by blast
qed

end

locale labeled_typing =
labeled_typed_model arity public Ana Γ label_witness1 label_witness2
+ typing_result arity public Ana Γ
for arity::"'fun ⇒ nat"
and public::"'fun ⇒ bool"
and Ana::"('fun,'var) term ⇒ (('fun,'var) term list × ('fun,'var) term list)"
and Γ::"('fun,'var) term ⇒ ('fun,'atom::finite) term_type"
and label_witness1::"'lbl"
and label_witness2::"'lbl"
begin

theorem par_comp_constr:
assumes 𝒜: "par_comp 𝒜 Sec" "typing_cond (unlabel 𝒜)"
and ℐ: "ℐ ⊨ ⟨unlabel 𝒜⟩" "interpretation⇩s⇩u⇩b⇩s⇩t ℐ"
shows "∃ℐ⇩τ. interpretation⇩s⇩u⇩b⇩s⇩t ℐ⇩τ ∧ wt⇩s⇩u⇩b⇩s⇩t ℐ⇩τ ∧ wf⇩t⇩r⇩m⇩s (subst_range ℐ⇩τ) ∧ (ℐ⇩τ ⊨ ⟨unlabel 𝒜⟩) ∧
((∀l. (ℐ⇩τ ⊨ ⟨proj_unl l 𝒜⟩)) ∨
(∃𝒜' l' t. prefix 𝒜' 𝒜 ∧ suffix [(l', receive⟨t⟩⇩s⇩t)] 𝒜' ∧
(strand_leaks⇩l⇩s⇩t 𝒜' Sec ℐ⇩τ)))"
proof -
from 𝒜(2) have *:
"wf⇩s⇩t {} (unlabel 𝒜)"
"fv⇩s⇩t (unlabel 𝒜) ∩ bvars⇩s⇩t (unlabel 𝒜) = {}"
"tfr⇩s⇩t (unlabel 𝒜)"
"wf⇩t⇩r⇩m⇩s (trms⇩s⇩t (unlabel 𝒜))"
"Ana_invar_subst (ik⇩s⇩t (unlabel 𝒜) ∪ assignment_rhs⇩s⇩t (unlabel 𝒜))"
unfolding typing_cond_def tfr⇩s⇩t_def by metis+

obtain ℐ⇩τ where ℐ⇩τ: "ℐ⇩τ ⊨ ⟨unlabel 𝒜⟩" "interpretation⇩s⇩u⇩b⇩s⇩t ℐ⇩τ" "wt⇩s⇩u⇩b⇩s⇩t ℐ⇩τ" "wf⇩t⇩r⇩m⇩s (subst_range ℐ⇩τ)"
using wt_attack_if_tfr_attack_d[OF * ℐ(2,1)] by metis

show ?thesis using par_comp_constr_typed[OF 𝒜(1) ℐ⇩τ] ℐ⇩τ by auto
qed

end

subsection ‹Automated GSMP Disjointness›
locale labeled_typed_model' = typed_model' arity public Ana Γ +
labeled_typed_model arity public Ana Γ label_witness1 label_witness2
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 label_witness1 label_witness2::'lbl
begin

lemma GSMP_disjointI:
fixes A' A B B'::"('fun, ('fun, 'atom) term × nat) terms"
defines "f ≡ λM. {t ⋅ δ | t δ. t ∈ M ∧ wt⇩s⇩u⇩b⇩s⇩t δ ∧ wf⇩t⇩r⇩m⇩s (subst_range δ) ∧ fv (t ⋅ δ) = {}}"
and "δ ≡ var_rename (max_var_set (fv⇩s⇩e⇩t A))"
assumes A'_wf: "wf⇩t⇩r⇩m⇩s' arity A'"
and B'_wf: "wf⇩t⇩r⇩m⇩s' arity B'"
and A_inst: "has_all_wt_instances_of Γ A' A"
and B_inst: "has_all_wt_instances_of Γ B' (B ⋅⇩s⇩e⇩t δ)"
and A_SMP_repr: "finite_SMP_representation arity Ana Γ A"
and B_SMP_repr: "finite_SMP_representation arity Ana Γ (B ⋅⇩s⇩e⇩t δ)"
and AB_trms_disj:
"∀t ∈ A. ∀s ∈ B ⋅⇩s⇩e⇩t δ. Γ t = Γ s ∧ mgu t s ≠ None ⟶
(intruder_synth' public arity {} t) ∨ ((∃u ∈ Sec. is_wt_instance_of_cond Γ t u))"
and Sec_wf: "wf⇩t⇩r⇩m⇩s Sec"
shows "GSMP_disjoint A' B' ((f Sec) - {m. {} ⊢⇩c m})"
proof -
have A_wf: "wf⇩t⇩r⇩m⇩s A" and B_wf: "wf⇩t⇩r⇩m⇩s (B ⋅⇩s⇩e⇩t δ)"
and A'_wf': "wf⇩t⇩r⇩m⇩s A'" and B'_wf': "wf⇩t⇩r⇩m⇩s B'"
and A_finite: "finite A" and B_finite: "finite (B ⋅⇩s⇩e⇩t δ)"
using finite_SMP_representationD[OF A_SMP_repr]
finite_SMP_representationD[OF B_SMP_repr]
A'_wf B'_wf
unfolding wf⇩t⇩r⇩m⇩s_code[symmetric] wf⇩t⇩r⇩m_code[symmetric] list_all_iff by blast+

have AB_fv_disj: "fv⇩s⇩e⇩t A ∩ fv⇩s⇩e⇩t (B ⋅⇩s⇩e⇩t δ) = {}"
using var_rename_fv_set_disjoint'[of A B, unfolded δ_def[symmetric]] A_finite by simp

have "GSMP_disjoint A (B ⋅⇩s⇩e⇩t δ) ((f Sec) - {m. {} ⊢⇩c m})"
using ground_SMP_disjointI[OF AB_fv_disj A_SMP_repr B_SMP_repr Sec_wf AB_trms_disj]
unfolding GSMP_def GSMP_disjoint_def f_def by blast
moreover have "SMP A' ⊆ SMP A" "SMP B' ⊆ SMP (B ⋅⇩s⇩e⇩t δ)"
using SMP_I'[OF A'_wf' A_wf A_inst] SMP_SMP_subset[of A' A]
SMP_I'[OF B'_wf' B_wf B_inst] SMP_SMP_subset[of B' "B ⋅⇩s⇩e⇩t δ"]
by (blast, blast)
ultimately show ?thesis unfolding GSMP_def GSMP_disjoint_def by auto
qed

end

end