From ef59bf6a36fcd8c42424aee433ab4f51fb4358d8 Mon Sep 17 00:00:00 2001
From: "Achim D. Brucker" <adbrucker@0x5f.org>
Date: Mon, 1 Mar 2021 05:47:16 +0000
Subject: [PATCH] Import of AFP for Isabelle 2021.

---
 .../Parallel_Compositionality.thy             |   1 +
 .../Stateful_Compositionality.thy             | 139 +++++++++---------
 .../Stateful_Typing.thy                       |   1 +
 .../Typing_Result.thy                         | 137 ++++++++---------
 .../document/root.tex                         |  14 +-
 .../examples/Example_Keyserver.thy            |   1 +
 .../examples/Example_TLS.thy                  |   1 +
 7 files changed, 149 insertions(+), 145 deletions(-)

diff --git a/Stateful_Protocol_Composition_and_Typing/Parallel_Compositionality.thy b/Stateful_Protocol_Composition_and_Typing/Parallel_Compositionality.thy
index f2bee5f..25f05a0 100644
--- a/Stateful_Protocol_Composition_and_Typing/Parallel_Compositionality.thy
+++ b/Stateful_Protocol_Composition_and_Typing/Parallel_Compositionality.thy
@@ -41,6 +41,7 @@ OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 *)
 
 section \<open>Parallel Compositionality of Security Protocols\<close>
+text \<open>\label{sec:Parallel-Compositionality}\<close>
 theory Parallel_Compositionality
 imports Typing_Result Labeled_Strands
 begin
diff --git a/Stateful_Protocol_Composition_and_Typing/Stateful_Compositionality.thy b/Stateful_Protocol_Composition_and_Typing/Stateful_Compositionality.thy
index 81cb5a5..848bc1b 100644
--- a/Stateful_Protocol_Composition_and_Typing/Stateful_Compositionality.thy
+++ b/Stateful_Protocol_Composition_and_Typing/Stateful_Compositionality.thy
@@ -38,6 +38,7 @@ OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 
 
 section \<open>Stateful Protocol Compositionality\<close>
+text \<open>\label{Stateful-Compositionality}\<close>
 
 theory Stateful_Compositionality
 imports Stateful_Typing Parallel_Compositionality Labeled_Stateful_Strands
@@ -56,7 +57,7 @@ proof -
   proof
     fix \<tau> assume \<tau>: "\<tau> \<in> \<Gamma> ` Var ` fv\<^sub>s\<^sub>s\<^sub>t\<^sub>p (a \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<delta>)"
     then obtain x where x: "x \<in> fv\<^sub>s\<^sub>s\<^sub>t\<^sub>p (a \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<delta>)" "\<Gamma> (Var x) = \<tau>" by moura
-  
+
     show "\<tau> \<in> \<Gamma> ` Var ` fv\<^sub>s\<^sub>s\<^sub>t\<^sub>p a"
     proof (cases "x \<in> fv\<^sub>s\<^sub>s\<^sub>t\<^sub>p a")
       case False
@@ -68,13 +69,13 @@ proof -
           using fv\<^sub>s\<^sub>s\<^sub>t\<^sub>p_NegCheck(1)[of X "F \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s rm_vars (set X) \<delta>" "G \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s rm_vars (set X) \<delta>"]
                 fv\<^sub>s\<^sub>s\<^sub>t\<^sub>p_NegCheck(1)[of X F G] False x(1)
           by fastforce+
-  
+
         obtain y where y: "y \<in> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F \<union> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s G" "x \<in> fv (rm_vars (set X) \<delta> y)"
           using fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s_subst_obtain_var[of _ _ "rm_vars (set X) \<delta>"]
                 fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s_subst_obtain_var[of _ _ "rm_vars (set X) \<delta>"]
                 *(1)
           by blast
-  
+
         have "fv (rm_vars (set X) \<delta> z) = {} \<or> (\<exists>u. rm_vars (set X) \<delta> z = Var u)" for z
           using assms(2) rm_vars_img_subset[of "set X" \<delta>] by blast
         hence "rm_vars (set X) \<delta> y = Var x" using y(2) by fastforce
@@ -94,7 +95,7 @@ proof -
   proof
     fix \<tau> assume \<tau>: "\<tau> \<in> \<Gamma> ` Var ` vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p (a \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<delta>)"
     then obtain x where x: "x \<in> vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p (a \<cdot>\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<delta>)" "\<Gamma> (Var x) = \<tau>" by moura
-  
+
     show "\<tau> \<in> \<Gamma> ` Var ` vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p a"
     proof (cases "x \<in> vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p a")
       case False
@@ -106,13 +107,13 @@ proof -
           using vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p_NegCheck[of X "F \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s rm_vars (set X) \<delta>" "G \<cdot>\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s rm_vars (set X) \<delta>"]
                 vars\<^sub>s\<^sub>s\<^sub>t\<^sub>p_NegCheck[of X F G] False x(1)
           by (fastforce, blast)
-  
+
         obtain y where y: "y \<in> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F \<union> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s G" "x \<in> fv (rm_vars (set X) \<delta> y)"
           using fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s_subst_obtain_var[of _ _ "rm_vars (set X) \<delta>"]
                 fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s_subst_obtain_var[of _ _ "rm_vars (set X) \<delta>"]
                 *(1)
           by blast
-  
+
         have "fv (rm_vars (set X) \<delta> z) = {} \<or> (\<exists>u. rm_vars (set X) \<delta> z = Var u)" for z
           using assms(2) rm_vars_img_subset[of "set X" \<delta>] by blast
         hence "rm_vars (set X) \<delta> y = Var x" using y(2) by fastforce
@@ -165,7 +166,7 @@ proof -
   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)
@@ -258,7 +259,7 @@ proof -
   proof -
     obtain k where k: "(k,d) \<in> set D - set (dbproj i D)"
       using d by force
-    
+
     have "(i,f) \<in> ((\<lambda>(t, s). (i, t, s)) ` set F') \<union> set D"
          "(k,d) \<in> ((\<lambda>(t, s). (i, t, s)) ` set F') \<union> set D"
       using f k by auto
@@ -310,12 +311,12 @@ proof (induction D rule: List.rev_induct)
   have "pair (t,s) \<cdot> \<I> = pair d \<cdot> \<I>" using di snoc.prems(2) by auto
   hence "\<exists>\<delta>. Unifier \<delta> (pair (t,s)) (pair d)" by auto
   hence 1: "i = j" using snoc.prems(1) di by fastforce
-  
+
   have "set D \<subseteq> 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
 
@@ -390,7 +391,7 @@ lemma setops\<^sub>l\<^sub>s\<^sub>s\<^sub>t\<^sub>p_pair_image[simp]:
 unfolding lpair_def by force+
 
 definition par_comp\<^sub>l\<^sub>s\<^sub>s\<^sub>t where
-  "par_comp\<^sub>l\<^sub>s\<^sub>s\<^sub>t (\<A>::('fun,'var,'lbl) labeled_stateful_strand) (Secrets::('fun,'var) terms) \<equiv> 
+  "par_comp\<^sub>l\<^sub>s\<^sub>s\<^sub>t (\<A>::('fun,'var,'lbl) labeled_stateful_strand) (Secrets::('fun,'var) terms) \<equiv>
     (\<forall>l1 l2. l1 \<noteq> l2 \<longrightarrow>
               GSMP_disjoint (trms\<^sub>s\<^sub>s\<^sub>t (proj_unl l1 \<A>) \<union> pair ` setops\<^sub>s\<^sub>s\<^sub>t (proj_unl l1 \<A>))
                             (trms\<^sub>s\<^sub>s\<^sub>t (proj_unl l2 \<A>) \<union> pair ` setops\<^sub>s\<^sub>s\<^sub>t (proj_unl l2 \<A>)) Secrets) \<and>
@@ -519,7 +520,7 @@ proof (unfold par_comp\<^sub>l\<^sub>s\<^sub>s\<^sub>t_def case_prod_unfold; int
     unfolding GSMP_disjoint_def by fastforce
   thus "?R (A \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<delta>)" unfolding M_def by blast
 
-  have "?Q A" using A unfolding par_comp\<^sub>l\<^sub>s\<^sub>s\<^sub>t_def by force 
+  have "?Q A" using A unfolding par_comp\<^sub>l\<^sub>s\<^sub>s\<^sub>t_def by force
   thus "?Q (A \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<delta>)" using \<delta>(3)
   proof (induction A)
     case (Cons a A)
@@ -531,7 +532,7 @@ proof (unfold par_comp\<^sub>l\<^sub>s\<^sub>s\<^sub>t_def case_prod_unfold; int
     have "?Q A" "subst_domain \<delta> \<inter> bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t A = {}"
       using Cons.prems 0 unfolding setops\<^sub>l\<^sub>s\<^sub>s\<^sub>t_def by auto
     hence IH: "?Q (A \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<delta>)" using Cons.IH unfolding setops\<^sub>l\<^sub>s\<^sub>s\<^sub>t_def by blast
-    
+
     have 1: "fst p = fst q"
       when p: "p \<in> setops\<^sub>l\<^sub>s\<^sub>s\<^sub>t\<^sub>p (a \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<delta>)"
         and q: "q \<in> setops\<^sub>l\<^sub>s\<^sub>s\<^sub>t\<^sub>p (a \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t\<^sub>p \<delta>)"
@@ -546,12 +547,12 @@ proof (unfold par_comp\<^sub>l\<^sub>s\<^sub>s\<^sub>t_def case_prod_unfold; int
       for p q
     proof -
       obtain p' X where p':
-          "p' \<in> setops\<^sub>l\<^sub>s\<^sub>s\<^sub>t A" "fst p = fst p'" 
+          "p' \<in> setops\<^sub>l\<^sub>s\<^sub>s\<^sub>t A" "fst p = fst p'"
           "X \<subseteq> bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t (a#A)" "snd p = snd p' \<cdot>\<^sub>p rm_vars X \<delta>"
         using setops\<^sub>l\<^sub>s\<^sub>s\<^sub>t_in_subst[OF p] 0 by blast
 
       obtain q' Y where q':
-          "q' \<in> setops\<^sub>l\<^sub>s\<^sub>s\<^sub>t\<^sub>p a" "fst q = fst q'" 
+          "q' \<in> setops\<^sub>l\<^sub>s\<^sub>s\<^sub>t\<^sub>p a" "fst q = fst q'"
           "Y \<subseteq> bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t (a#A)" "snd q = snd q' \<cdot>\<^sub>p rm_vars Y \<delta>"
         using setops\<^sub>l\<^sub>s\<^sub>s\<^sub>t\<^sub>p_in_subst[OF q] 0 by blast
 
@@ -592,9 +593,9 @@ proof -
   have 1: "wf\<^sub>s\<^sub>t 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: "fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s (unlabel Di) \<subseteq> X" 
+  have 2: "fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s (unlabel Di) \<subseteq> X"
     using assms(3) subseqs_set_subset(1)[OF assms(2)]
-    unfolding unlabel_def 
+    unfolding unlabel_def
     by fastforce
   { fix B::"('fun,'var) strand" assume "wf\<^sub>s\<^sub>t X B"
     hence "wf\<^sub>s\<^sub>t X (unlabel c1@B)" using 2 unfolding c1 unlabel_def by (induct Di) auto
@@ -647,7 +648,7 @@ proof
     using B by meson
   hence p: "p \<in> setops\<^sub>l\<^sub>s\<^sub>s\<^sub>t (A \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<delta>)"
     using b(2) unfolding setops\<^sub>l\<^sub>s\<^sub>s\<^sub>t_def subst_apply_labeled_stateful_strand_def by auto
-  
+
   obtain X q where q:
       "q \<in> setops\<^sub>l\<^sub>s\<^sub>s\<^sub>t A" "fst p = fst q" "snd p = snd q \<cdot>\<^sub>p rm_vars X \<delta>"
     using setops\<^sub>l\<^sub>s\<^sub>s\<^sub>t_in_subst[OF p] by blast
@@ -725,7 +726,7 @@ proof -
     hence 1: "fv\<^sub>l\<^sub>s\<^sub>t A'' \<subseteq> fv\<^sub>s\<^sub>s\<^sub>t AA \<union> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s (unlabel D)"
       using fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s_mono[of "unlabel (fltD1 Di)" "unlabel D"]
       unfolding unlabel_def fltD1_def by force
-    
+
     have 2: "fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s (unlabel Di) \<union> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s (unlabel (fltD1 Di)) \<subseteq> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s (unlabel D)"
       using subseqs_set_subset(1)[OF *(1)]
       unfolding fltD1_def unlabel_def
@@ -738,7 +739,7 @@ proof -
     hence 3: "fv\<^sub>l\<^sub>s\<^sub>t (constr Di) \<subseteq> fv t \<union> fv s \<union> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s (unlabel D)" using 2 by blast
 
     have 4: "fv\<^sub>s\<^sub>s\<^sub>t (unlabel A) = fv t \<union> fv s \<union> fv\<^sub>s\<^sub>s\<^sub>t AA" using iB by auto
-    
+
     have "fv\<^sub>s\<^sub>t (unlabel A') \<subseteq> fv\<^sub>s\<^sub>s\<^sub>t (unlabel A) \<union> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s (unlabel D)" using 1 3 4 5 by blast
     thus ?case by metis
   next
@@ -1023,12 +1024,12 @@ proof -
         using prems by moura
 
       have *: "wf'\<^sub>s\<^sub>s\<^sub>t X (unlabel A)" "fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s (unlabel D) \<subseteq> X" using prems si by auto
-      
+
       have "bvars\<^sub>s\<^sub>s\<^sub>t (unlabel A) \<subseteq> bvars\<^sub>s\<^sub>s\<^sub>t (unlabel ((i,\<forall>Y\<langle>\<or>\<noteq>: F \<or>\<notin>: F'\<rangle>)#A))"
            "fv\<^sub>s\<^sub>s\<^sub>t (unlabel A) \<subseteq> fv\<^sub>s\<^sub>s\<^sub>t (unlabel ((i,\<forall>Y\<langle>\<or>\<noteq>: F \<or>\<notin>: F'\<rangle>)#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
@@ -1105,7 +1106,7 @@ proof -
     from prems(1) have A': "A' \<in> set (tr\<^sub>p\<^sub>c A (List.insert (i,t,s) D))" by simp
 
     have 1: "list_all tfr\<^sub>s\<^sub>s\<^sub>t\<^sub>p (unlabel A)" using sublmm[OF prems(2,3,4,5)] by simp
-  
+
     have "pair ` setops\<^sub>s\<^sub>s\<^sub>t (unlabel ((i,insert\<langle>t,s\<rangle>)#A)) \<union> pair`snd`set D =
           pair ` setops\<^sub>s\<^sub>s\<^sub>t (unlabel A) \<union> pair`snd`set (List.insert (i,t,s) D)"
       by (auto simp add: setops\<^sub>s\<^sub>s\<^sub>t_def)
@@ -1149,7 +1150,7 @@ proof -
     have **: "?P1 A (filter (\<lambda>d. d \<notin> set Di) D)"
       using prems(4) bvars\<^sub>s\<^sub>s\<^sub>t_cons_subset[of "unlabel A" "delete\<langle>t,s\<rangle>"]
       unfolding unlabel_def by fastforce
-      
+
     have 1: "list_all tfr\<^sub>s\<^sub>t\<^sub>p (unlabel A'')"
       using IH[OF A''(3,2) sublmm(1,2)[OF prems(2,3,4,5)] ** *]
       by metis
@@ -1213,13 +1214,13 @@ proof -
       by moura
 
     have 1: "list_all tfr\<^sub>s\<^sub>t\<^sub>p (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)]] 
+      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: "\<Gamma> (pair (t,s)) = \<Gamma> (pair (snd d))"
       when "\<exists>\<delta>. Unifier \<delta> (pair (t,s)) (pair (snd d))"
       using that prems(2,5) A''(3) unfolding tfr\<^sub>s\<^sub>s\<^sub>t_def by (simp add: setops\<^sub>s\<^sub>s\<^sub>t_def)
-    
+
     show ?case using A''(1) 1 2 by fastforce
   next
     case (8 i X F F' A D)
@@ -1252,7 +1253,7 @@ proof -
 
     have 2: "(F' = [] \<and> Q1 F X) \<or> Q2 (trms\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F \<union> pair ` set F') X"
       using prems(2) unfolding Q1_def Q2_def by simp
-  
+
     have 3: "F' = [] \<Longrightarrow> Q1 F X \<Longrightarrow> list_all tfr\<^sub>s\<^sub>t\<^sub>p (unlabel constr)"
       using 0 2 tfr\<^sub>s\<^sub>t\<^sub>p_list_all_alt_def[of "unlabel constr"] unfolding Q1_def by auto
 
@@ -1414,7 +1415,7 @@ next
 
   define constr where
     "constr = (\<lambda>D. map (\<lambda>G. (i,\<forall>X\<langle>\<or>\<noteq>: (F@G)\<rangle>\<^sub>s\<^sub>t)) (tr\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F' (map snd (dbproj i D))))"
-  
+
   obtain B' where B':
       "B = constr D@B'"
       "B' \<in> set (tr\<^sub>p\<^sub>c S D)"
@@ -1661,7 +1662,7 @@ proof -
       define constr where "constr = (
         \<lambda>d::(('lbl strand_label \<times> ('fun,'var) term \<times> ('fun,'var) term)).
           (i,\<langle>ac: (pair (t',s)) \<doteq> (pair (snd d))\<rangle>\<^sub>s\<^sub>t))"
-      
+
       obtain A'' d where *: "A' = constr d#A''" "A'' \<in> set (tr\<^sub>p\<^sub>c S D)" "d \<in> set (dbproj i D)"
         using prems(3) constr_def by auto
       have "E \<noteq> []" using prems(1) by auto
@@ -1680,7 +1681,7 @@ proof -
 
       define constr where
         "constr = map (\<lambda>H. (i,\<forall>X\<langle>\<or>\<noteq>: (G@H)\<rangle>\<^sub>s\<^sub>t)) (tr\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s G' (map snd (dbproj i D)))"
-      
+
       obtain A'' where *: "A' = constr@A''" "A'' \<in> set (tr\<^sub>p\<^sub>c S D)"
         using prems(3) constr_def by auto
       have ***:  "(m, receive\<langle>t\<rangle>\<^sub>s\<^sub>t) \<notin> set constr" using constr_def by auto
@@ -1763,16 +1764,16 @@ proof
       let ?g1 = "\<lambda>d. \<forall>[]\<langle>\<or>\<noteq>: [(pair (t,s), pair d)]\<rangle>\<^sub>s\<^sub>t"
       let ?f2 = "\<lambda>d. (i, ?f1 (snd d))"
       let ?g2 = "\<lambda>d. (i, ?g1 (snd d))"
-  
+
       define constr1 where "constr1 = (\<lambda>Di. (map ?f1 Di)@(map ?g1 [d\<leftarrow>unlabel D. d \<notin> set Di]))"
       define constr2 where "constr2 = (\<lambda>Di. (map ?f2 Di)@(map ?g2 [d\<leftarrow>D. d \<notin> set Di]))"
-  
+
       obtain C' Di where C':
           "Di \<in> set (subseqs D)"
           "C = constr2 Di@C'"
           "C' \<in> set (tr'\<^sub>p\<^sub>c S [d\<leftarrow>D. d \<notin> set Di])"
         using "6.prems"(1) unfolding constr2_def by moura
-      
+
       have 0: "set [d\<leftarrow>D. d \<notin> set Di] \<subseteq> set D"
               "setops\<^sub>l\<^sub>s\<^sub>s\<^sub>t S \<subseteq> setops\<^sub>l\<^sub>s\<^sub>s\<^sub>t ((i, delete\<langle>t,s\<rangle>)#S)"
         by (auto simp add: setops\<^sub>l\<^sub>s\<^sub>s\<^sub>t_def)
@@ -1781,12 +1782,12 @@ proof
            \<forall>(k, q) \<in> setops\<^sub>l\<^sub>s\<^sub>s\<^sub>t S \<union> set [d\<leftarrow>D. d \<notin> set Di].
             p = q \<longrightarrow> j = k"
         using "6.prems"(2) by blast
-  
+
       have "\<forall>(i,p) \<in> set D \<union> set Di. \<forall>(j,q) \<in> set D \<union> set Di. p = q \<longrightarrow> i = j"
         using "6.prems"(2) subseqs_set_subset(1)[OF C'(1)] by blast
       hence 2: "unlabel [d\<leftarrow>D. d \<notin> set Di] = [d\<leftarrow>unlabel D. d \<notin> set (unlabel Di)]"
         using unlabel_filter_eq[of D "set Di"] unfolding unlabel_def by simp
-  
+
       have 3:
           "\<And>f g::('a \<times> 'a \<Rightarrow> 'c). \<And>A B::(('b \<times> 'a \<times> 'a) list).
               map snd ((map (\<lambda>d. (i, f (snd d))) A)@(map (\<lambda>d. (i, g (snd d))) B)) =
@@ -1797,12 +1798,12 @@ proof
         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 \<in> set (map unlabel (subseqs D))"
         using C'(1) unfolding unlabel_def by simp
       hence 5: "unlabel Di \<in> 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)
@@ -1810,7 +1811,7 @@ proof
           "C = (i,\<langle>ac: (pair (t,s)) \<doteq> (pair (snd d))\<rangle>\<^sub>s\<^sub>t)#C'"
           "C' \<in> set (tr'\<^sub>p\<^sub>c S D)" "d \<in> set D"
         using "7.prems"(1) by moura
-  
+
       have "setops\<^sub>l\<^sub>s\<^sub>s\<^sub>t S \<union> set D \<subseteq> setops\<^sub>l\<^sub>s\<^sub>s\<^sub>t ((i,InSet ac t s)#S) \<union> set D"
         by (auto simp add: setops\<^sub>l\<^sub>s\<^sub>s\<^sub>t_def)
       hence "\<forall>(j, p) \<in> setops\<^sub>l\<^sub>s\<^sub>s\<^sub>t S \<union> set D.
@@ -1825,7 +1826,7 @@ proof
           "C = map (\<lambda>G. (i,\<forall>X\<langle>\<or>\<noteq>: (F@G)\<rangle>\<^sub>s\<^sub>t)) (tr\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F' (map snd D))@C'"
           "C' \<in> set (tr'\<^sub>p\<^sub>c S D)"
         using "8.prems"(1) by moura
-  
+
       have "setops\<^sub>l\<^sub>s\<^sub>s\<^sub>t S \<union> set D \<subseteq> setops\<^sub>l\<^sub>s\<^sub>s\<^sub>t ((i,NegChecks X F F')#S) \<union> set D"
         by (auto simp add: setops\<^sub>l\<^sub>s\<^sub>s\<^sub>t_def)
       hence "\<forall>(j, p) \<in> setops\<^sub>l\<^sub>s\<^sub>s\<^sub>t S \<union> set D.
@@ -1882,7 +1883,7 @@ proof
         hence "j = ia" using Cons.prems(2) a Insert by (auto simp add: setops\<^sub>l\<^sub>s\<^sub>s\<^sub>t_def)
         hence "?P ia" using j(1) by metis
       } hence j: "?P ia" by metis
-      
+
       have 2: "\<forall>(k1, p) \<in> setops\<^sub>l\<^sub>s\<^sub>s\<^sub>t A \<union> set (List.insert (ia,t,s) D).
                \<forall>(k2, q) \<in> setops\<^sub>l\<^sub>s\<^sub>s\<^sub>t A \<union> set (List.insert (ia,t,s) D).
                  p = q \<longrightarrow> k1 = k2"
@@ -1894,7 +1895,7 @@ proof
       define c where "c \<equiv> (\<lambda>(i::'lbl strand_label) Di.
         map (\<lambda>d. (i,\<langle>check: (pair (t,s)) \<doteq> (pair (snd d))\<rangle>\<^sub>s\<^sub>t)) Di@
         map (\<lambda>d. (i,\<forall>[]\<langle>\<or>\<noteq>: [(pair (t,s), pair (snd d))]\<rangle>\<^sub>s\<^sub>t)) [d\<leftarrow>D. d \<notin> set Di])"
-      
+
       define d where "d \<equiv> (\<lambda>Di.
         map (\<lambda>d. \<langle>check: (pair (t,s)) \<doteq> (pair d)\<rangle>\<^sub>s\<^sub>t) Di@
         map (\<lambda>d. \<forall>[]\<langle>\<or>\<noteq>: [(pair (t,s), pair d)]\<rangle>\<^sub>s\<^sub>t) [d\<leftarrow>unlabel D. d \<notin> set Di])"
@@ -1919,14 +1920,14 @@ proof
         using Cons.prems(2) by blast
       hence 3: "[d\<leftarrow>unlabel D. d \<notin> set Di] = unlabel [d\<leftarrow>D. d \<notin> set Di']"
         using Di'(2) unlabel_filter_eq[of D "set Di'"] unfolding unlabel_def by auto
-      
+
       obtain C where C: "C \<in> set (tr'\<^sub>p\<^sub>c A [d\<leftarrow>D. d \<notin> set Di'])" "B' = unlabel C"
         using 3 Cons.IH[OF _ 2] B'(3) by auto
       hence 4: "c ia Di'@C \<in> set (tr'\<^sub>p\<^sub>c (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)
@@ -1938,7 +1939,7 @@ proof
       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': 
+      then obtain B' where B':
           "B = map (\<lambda>G. \<forall>X\<langle>\<or>\<noteq>: (F@G)\<rangle>\<^sub>s\<^sub>t) (tr\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F' (unlabel D))@B'"
           "B' \<in> set (tr (unlabel A) (unlabel D))"
         using Cons.prems(1) a by auto
@@ -1968,7 +1969,7 @@ proof
 
       obtain B' where B': "B = (i,send\<langle>t\<rangle>\<^sub>s\<^sub>t)#B'" "B' \<in> set (tr\<^sub>p\<^sub>c S D)"
         using prems(1) by moura
-          
+
       have 1: "\<lbrakk>M; unlabel B'\<rbrakk>\<^sub>d \<I>" using prems(2) B'(1) by simp
       have 4: "?R3 S D" using prems(3) by (auto simp add: setops\<^sub>l\<^sub>s\<^sub>s\<^sub>t_def)
       have 5: "?R4 S D" using prems(4) by force
@@ -1987,7 +1988,7 @@ proof
       note IH = "3.IH"
 
       obtain B' where B': "B = (i,receive\<langle>t\<rangle>\<^sub>s\<^sub>t)#B'" "B' \<in> set (tr\<^sub>p\<^sub>c S D)" using prems(1) by moura
-          
+
       have 1: "\<lbrakk>insert (t \<cdot> \<I>) M; unlabel B'\<rbrakk>\<^sub>d \<I> " using prems(2) B'(1) by simp
       have 4: "?R3 S D" using prems(3) by (auto simp add: setops\<^sub>l\<^sub>s\<^sub>s\<^sub>t_def)
       have 5: "?R4 S D" using prems(4) by force
@@ -2006,7 +2007,7 @@ proof
 
       obtain B' where B': "B = (i,\<langle>ac: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t)#B'" "B' \<in> set (tr\<^sub>p\<^sub>c S D)"
         using prems(1) by moura
-          
+
       have 1: "\<lbrakk>M; unlabel B'\<rbrakk>\<^sub>d \<I> " using prems(2) B'(1) by simp
       have 4: "?R3 S D" using prems(3) by (auto simp add: setops\<^sub>l\<^sub>s\<^sub>s\<^sub>t_def)
       have 5: "?R4 S D" using prems(4) by force
@@ -2026,7 +2027,7 @@ proof
       note IH = "5.IH"
 
       have B: "B \<in> set (tr\<^sub>p\<^sub>c S (List.insert (i,t,s) D))" using prems(1) by simp
-          
+
       have 1: "\<lbrakk>M; unlabel B\<rbrakk>\<^sub>d \<I> " using prems(2) B(1) by simp
       have 4: "?R3 S (List.insert (i,t,s) D)" using prems(3) by (auto simp add: setops\<^sub>l\<^sub>s\<^sub>s\<^sub>t_def)
       have 5: "?R4 S (List.insert (i,t,s) D)" using prems(4,5) by force
@@ -2070,7 +2071,7 @@ proof
           using dbproj_subseq_subset[OF B'(1)] by (auto simp add: setops\<^sub>l\<^sub>s\<^sub>s\<^sub>t_def)
         hence "(\<exists>\<delta>. Unifier \<delta> (pair p) (pair q)) \<Longrightarrow> j = k" using prems(3) by blast
       } hence 4: "?R3 S [d\<leftarrow>D. d \<notin> set Di]" by blast
-      
+
       have 5: "?R4 S (filter (\<lambda>d. d \<notin> set Di) D)" using prems(4) by force
       have 6: "?R5 S D" using prems(5) by force
 
@@ -2081,7 +2082,7 @@ proof
         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 "\<lbrakk>M; unlabel (?cl2 Di)\<rbrakk>\<^sub>d \<I>" using 7(1) 0(1) unfolding c unlabel_def by auto 
+      have "\<lbrakk>M; unlabel (?cl2 Di)\<rbrakk>\<^sub>d \<I>" using 7(1) 0(1) unfolding c unlabel_def by auto
       hence "\<lbrakk>M; ?cu2 Di\<rbrakk>\<^sub>d \<I>" by (metis 0(4))
       moreover {
         fix j p k q
@@ -2155,7 +2156,7 @@ proof
       obtain B' where B': "B = c@B'" "B' \<in> set (tr\<^sub>p\<^sub>c S D)" using prems(1) c by moura
 
       have 0: "ik\<^sub>s\<^sub>t (unlabel c) = {}" "ik\<^sub>s\<^sub>t (unlabel d) = {}"
-              "unlabel ?cl = ?cu" "unlabel ?dl = ?du" 
+              "unlabel ?cl = ?cu" "unlabel ?dl = ?du"
         unfolding c d unlabel_def by force+
 
       have "ik\<^sub>s\<^sub>t (unlabel c) = {}" unfolding c unlabel_def by force
@@ -2177,7 +2178,7 @@ proof
       have 8: "d@C \<in> set (tr'\<^sub>p\<^sub>c ((i,NegChecks X F F')#S) D)"
         using C(1) unfolding d unlabel_def by auto
 
-      have "\<lbrakk>M; unlabel ?cl\<rbrakk>\<^sub>d \<I>" using 7(1) unfolding c unlabel_def by auto 
+      have "\<lbrakk>M; unlabel ?cl\<rbrakk>\<^sub>d \<I>" using 7(1) unfolding c unlabel_def by auto
       hence "\<lbrakk>M; ?cu\<rbrakk>\<^sub>d \<I>" by (metis 0(3))
       moreover {
         fix j p k q
@@ -2213,7 +2214,7 @@ proof
 
       obtain C' where C': "C = (i,send\<langle>t\<rangle>\<^sub>s\<^sub>t)#C'" "C' \<in> set (tr'\<^sub>p\<^sub>c S D)"
         using prems(1) by moura
-          
+
       have 1: "\<lbrakk>M; unlabel C'\<rbrakk>\<^sub>d \<I> " using prems(2) C'(1) by simp
       have 4: "?R3 S D" using prems(3) by (auto simp add: setops\<^sub>l\<^sub>s\<^sub>s\<^sub>t_def)
       have 5: "?R4 S D" using prems(4) by force
@@ -2234,7 +2235,7 @@ proof
 
       obtain C' where C': "C = (i,receive\<langle>t\<rangle>\<^sub>s\<^sub>t)#C'" "C' \<in> set (tr'\<^sub>p\<^sub>c S D)"
         using prems(1) by moura
-          
+
       have 1: "\<lbrakk>insert (t \<cdot> \<I>) M; unlabel C'\<rbrakk>\<^sub>d \<I> " using prems(2) C'(1) by simp
       have 4: "?R3 S D" using prems(3) by (auto simp add: setops\<^sub>l\<^sub>s\<^sub>s\<^sub>t_def)
       have 5: "?R4 S D" using prems(4) by force
@@ -2253,7 +2254,7 @@ proof
 
       obtain C' where C': "C = (i,\<langle>ac: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t)#C'" "C' \<in> set (tr'\<^sub>p\<^sub>c S D)"
         using prems(1) by moura
-          
+
       have 1: "\<lbrakk>M; unlabel C'\<rbrakk>\<^sub>d \<I> " using prems(2) C'(1) by simp
       have 4: "?R3 S D" using prems(3) by (auto simp add: setops\<^sub>l\<^sub>s\<^sub>s\<^sub>t_def)
       have 5: "?R4 S D" using prems(4) by force
@@ -2273,7 +2274,7 @@ proof
       note IH = "5.IH"
 
       have C: "C \<in> set (tr'\<^sub>p\<^sub>c S (List.insert (i,t,s) D))" using prems(1) by simp
-          
+
       have 1: "\<lbrakk>M; unlabel C\<rbrakk>\<^sub>d \<I> " using prems(2) C(1) by simp
       have 4: "?R3 S (List.insert (i,t,s) D)" using prems(3) by (auto simp add: setops\<^sub>l\<^sub>s\<^sub>s\<^sub>t_def)
       have 5: "?R4 S (List.insert (i,t,s) D)" using prems(4,5) by force
@@ -2339,18 +2340,18 @@ proof
                \<forall>(k, q) \<in> {(i, t, s)} \<union> set D.
                 (\<exists>\<delta>. Unifier \<delta> (pair p) (pair q)) \<longrightarrow> j = k"
         by blast
-      moreover have "\<lbrakk>M; unlabel (?cl1 Di)\<rbrakk>\<^sub>d \<I>" using 7(1) unfolding c unlabel_append by auto 
+      moreover have "\<lbrakk>M; unlabel (?cl1 Di)\<rbrakk>\<^sub>d \<I>" using 7(1) unfolding c unlabel_append by auto
       hence "\<lbrakk>M; ?cu1 Di\<rbrakk>\<^sub>d \<I>" by (metis 0(3))
       ultimately have *: "Di \<in> set (subseqs (dbproj i D))"
         using labeled_sat_eqs_subseqs[OF C'(1)] by simp
       hence 8: "d Di@B \<in> set (tr\<^sub>p\<^sub>c ((i,delete\<langle>t,s\<rangle>)#S) D)"
         using B(1) unfolding d unlabel_def by auto
 
-      have "\<lbrakk>M; unlabel (?cl2 Di)\<rbrakk>\<^sub>d \<I>" using 7(1) 0(1) unfolding c unlabel_def by auto 
+      have "\<lbrakk>M; unlabel (?cl2 Di)\<rbrakk>\<^sub>d \<I>" using 7(1) 0(1) unfolding c unlabel_def by auto
       hence "\<lbrakk>M; ?cu2 Di\<rbrakk>\<^sub>d \<I>" by (metis 0(4))
       hence "\<lbrakk>M; ?du2 Di\<rbrakk>\<^sub>d \<I>" by (metis labeled_sat_ineq_dbproj)
       hence "\<lbrakk>M; unlabel (?dl2 Di)\<rbrakk>\<^sub>d \<I>" by (metis 0(6))
-      moreover have "\<lbrakk>M; unlabel (?cl1 Di)\<rbrakk>\<^sub>d \<I>" using 7(1) unfolding c unlabel_def by auto 
+      moreover have "\<lbrakk>M; unlabel (?cl1 Di)\<rbrakk>\<^sub>d \<I>" using 7(1) unfolding c unlabel_def by auto
       hence "\<lbrakk>M; unlabel (?dl1 Di)\<rbrakk>\<^sub>d \<I>" by (metis 0(3,5))
       ultimately have "\<lbrakk>M; unlabel (d Di)\<rbrakk>\<^sub>d \<I>" using 0(2) unfolding c d unlabel_def by force
       hence 9: "\<lbrakk>M; unlabel (d Di@B)\<rbrakk>\<^sub>d \<I>" using 0(2) B(2) unfolding unlabel_def by auto
@@ -2365,7 +2366,7 @@ proof
           "C = (i,\<langle>ac: (pair (t,s)) \<doteq> (pair (snd d))\<rangle>\<^sub>s\<^sub>t)#C'"
           "C' \<in> set (tr'\<^sub>p\<^sub>c S D)" "d \<in> set D"
         using prems(1) by moura
-          
+
       have 1: "\<lbrakk>M; unlabel C'\<rbrakk>\<^sub>d \<I> " using prems(2) C'(1) by simp
 
       { fix j p k q
@@ -2416,7 +2417,7 @@ proof
       obtain C' where C': "C = c@C'" "C' \<in> set (tr'\<^sub>p\<^sub>c S D)" using prems(1) c by moura
 
       have 0: "ik\<^sub>s\<^sub>t (unlabel c) = {}" "ik\<^sub>s\<^sub>t (unlabel d) = {}"
-              "unlabel ?cl = ?cu" "unlabel ?dl = ?du" 
+              "unlabel ?cl = ?cu" "unlabel ?dl = ?du"
         unfolding c d unlabel_def by force+
 
       have "ik\<^sub>s\<^sub>t (unlabel c) = {}" unfolding c unlabel_def by force
@@ -2438,7 +2439,7 @@ proof
       have 8: "d@B \<in> set (tr\<^sub>p\<^sub>c ((i,NegChecks X F F')#S) D)"
         using B(1) unfolding d unlabel_def by auto
 
-      have "\<lbrakk>M; unlabel ?cl\<rbrakk>\<^sub>d \<I>" using 7(1) unfolding c unlabel_def by auto 
+      have "\<lbrakk>M; unlabel ?cl\<rbrakk>\<^sub>d \<I>" using 7(1) unfolding c unlabel_def by auto
       hence "\<lbrakk>M; ?cu\<rbrakk>\<^sub>d \<I>" by (metis 0(3))
       moreover {
         fix j p k q
@@ -2657,7 +2658,7 @@ definition par_comp_prot_stateful where
 
 definition component_secure_prot_stateful where
   "component_secure_prot_stateful n P Sec attack \<equiv>
-    (\<forall>\<A> \<in> P. suffix [(ln n, Send (Fun attack []))] \<A> \<longrightarrow> 
+    (\<forall>\<A> \<in> P. suffix [(ln n, Send (Fun attack []))] \<A> \<longrightarrow>
      (\<forall>\<I>\<^sub>\<tau>. (interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>\<^sub>\<tau> \<and> wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>\<^sub>\<tau> \<and> wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<I>\<^sub>\<tau>)) \<longrightarrow>
             \<not>(\<I>\<^sub>\<tau> \<Turnstile>\<^sub>s (proj_unl n \<A>)) \<and>
             (\<forall>\<A>'. prefix \<A>' \<A> \<longrightarrow>
@@ -2678,13 +2679,13 @@ lemma par_comp_prot_impl_par_comp_stateful:
   assumes "par_comp_prot_stateful \<P> Sec" "\<A> \<in> \<P>"
   shows "par_comp\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<A> Sec"
 proof -
-  have *: 
+  have *:
       "\<forall>l1 l2. l1 \<noteq> l2 \<longrightarrow>
           GSMP_disjoint (\<Union>\<A> \<in> \<P>. trms\<^sub>s\<^sub>s\<^sub>t (proj_unl l1 \<A>) \<union> pair ` setops\<^sub>s\<^sub>s\<^sub>t (proj_unl l1 \<A>))
                         (\<Union>\<A> \<in> \<P>. trms\<^sub>s\<^sub>s\<^sub>t (proj_unl l2 \<A>) \<union> pair ` setops\<^sub>s\<^sub>s\<^sub>t (proj_unl l2 \<A>)) Sec"
     using assms(1) unfolding par_comp_prot_stateful_def by argo
   { fix l1 l2::'lbl assume **: "l1 \<noteq> l2"
-    hence ***: 
+    hence ***:
         "GSMP_disjoint (\<Union>\<A> \<in> \<P>. trms\<^sub>s\<^sub>s\<^sub>t (proj_unl l1 \<A>) \<union> pair ` setops\<^sub>s\<^sub>s\<^sub>t (proj_unl l1 \<A>))
                        (\<Union>\<A> \<in> \<P>. trms\<^sub>s\<^sub>s\<^sub>t (proj_unl l2 \<A>) \<union> pair ` setops\<^sub>s\<^sub>s\<^sub>t (proj_unl l2 \<A>)) Sec"
       using * by auto
@@ -2742,9 +2743,9 @@ proof -
       using par_comp_prot_impl_par_comp_stateful[OF P(2) \<A>(2)]
             typing_cond_prot_impl_typing_cond_stateful[OF tcp \<A>(2)]
       by metis+
-  
+
     have "unlabel (proj n \<A>) = proj_unl n \<A>" "proj_unl n \<A> = proj_unl n (proj n \<A>)"
-         "\<And>A. A \<in> Pi n \<Longrightarrow> proj n A = A" 
+         "\<And>A. A \<in> Pi n \<Longrightarrow> proj n A = A"
          "proj n \<A> = (proj n \<A>')@[(ln n, Send (Fun attack []))]"
       using P(1,3) \<A> by (auto simp add: proj_def unlabel_def component_prot_def composed_prot_def)
     moreover have "proj n \<A> \<in> Pi n"
@@ -2759,7 +2760,7 @@ proof -
                  (\<forall>I. declassified\<^sub>l\<^sub>s\<^sub>s\<^sub>t A I = declassified\<^sub>l\<^sub>s\<^sub>s\<^sub>t B I)"
         using * by metis
     }
-    ultimately have *: 
+    ultimately have *:
         "\<forall>\<I>\<^sub>\<tau>. interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>\<^sub>\<tau> \<and> wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>\<^sub>\<tau> \<and> wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<I>\<^sub>\<tau>) \<longrightarrow>
                   \<not>(\<I>\<^sub>\<tau> \<Turnstile>\<^sub>s (proj_unl n \<A>)) \<and> (\<forall>\<A>'. prefix \<A>' \<A> \<longrightarrow>
                         (\<forall>t \<in> Sec - declassified\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<A>' \<I>\<^sub>\<tau>. \<not>(\<I>\<^sub>\<tau> \<Turnstile>\<^sub>s (proj_unl n \<A>'@[Send t]))))"
diff --git a/Stateful_Protocol_Composition_and_Typing/Stateful_Typing.thy b/Stateful_Protocol_Composition_and_Typing/Stateful_Typing.thy
index 9e71d12..f9b0e67 100644
--- a/Stateful_Protocol_Composition_and_Typing/Stateful_Typing.thy
+++ b/Stateful_Protocol_Composition_and_Typing/Stateful_Typing.thy
@@ -37,6 +37,7 @@ OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 *)
 
 section \<open>Extending the Typing Result to Stateful Constraints\<close>
+text \<open>\label{sec:Stateful-Typing}\<close>
 
 theory Stateful_Typing
 imports Typing_Result Stateful_Strands
diff --git a/Stateful_Protocol_Composition_and_Typing/Typing_Result.thy b/Stateful_Protocol_Composition_and_Typing/Typing_Result.thy
index f696e12..76e47f0 100644
--- a/Stateful_Protocol_Composition_and_Typing/Typing_Result.thy
+++ b/Stateful_Protocol_Composition_and_Typing/Typing_Result.thy
@@ -37,6 +37,7 @@ OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 *)
 
 section \<open>The Typing Result\<close>
+text \<open>\label{sec:Typing-Result}\<close>
 
 theory Typing_Result
 imports Typed_Model
@@ -331,7 +332,7 @@ subsubsection \<open>Simple Constraints are Well-typed Satisfiable\<close>
 text \<open>Proving the existence of a well-typed interpretation\<close>
 context
 begin
-lemma wt_interpretation_exists: 
+lemma wt_interpretation_exists:
   obtains \<I>::"('fun,'var) subst"
   where "interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>" "subst_range \<I> \<subseteq> public_ground_wf_terms"
 proof
@@ -344,7 +345,7 @@ proof
       unfolding \<I>_def wf\<^sub>t\<^sub>r\<^sub>m_def by simp
   } hence props: "\<I> v = t \<Longrightarrow> \<Gamma> (Var v) = \<Gamma> t \<and> public_ground_wf_term t" for v t by metis
 
-  have "\<I> v \<noteq> Var v" for v using props pgwt_ground by force
+  have "\<I> v \<noteq> Var v" for v using props pgwt_ground by (simp add: empty_fv_not_var)
   hence "subst_domain \<I> = UNIV" by auto
   moreover have "ground (subst_range \<I>)" by (simp add: props pgwt_ground)
   ultimately show "interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>" by metis
@@ -377,7 +378,7 @@ proof -
       let ?Q = "\<lambda>c. \<Gamma> (Fun c []) = Var a \<and> public c"
       have " {c. ?Q c} - S = {c. ?P c}" by auto
       hence "infinite {c. ?P c}"
-        using Diff_infinite_finite[OF assms(1) infinite_typed_consts[of a]] 
+        using Diff_infinite_finite[OF assms(1) infinite_typed_consts[of a]]
         by metis
       hence "\<exists>c. ?P c" using not_finite_existsD by blast
       thus ?case using someI_ex[of ?P] by auto
@@ -406,7 +407,7 @@ proof -
       let ?Q = "\<lambda>c. \<Gamma> (Fun c []) = Var a \<and> public c"
       have " {c. ?Q c} - S = {c. ?P c}" by auto
       hence "infinite {c. ?P c}"
-        using Diff_infinite_finite[OF assms(1) infinite_typed_consts[of a]] 
+        using Diff_infinite_finite[OF assms(1) infinite_typed_consts[of a]]
         by metis
       hence "\<exists>c. ?P c" using not_finite_existsD by blast
       thus ?case
@@ -414,7 +415,7 @@ proof -
         by auto
     next
       case (Fun f T)
-      have f: "0 < arity f" "length T = arity f" "public f" 
+      have f: "0 < arity f" "length T = arity f" "public f"
         using Fun.prems fun_type_inv unfolding wf\<^sub>t\<^sub>r\<^sub>m_def by auto
       have "\<And>t. t \<in> set T \<Longrightarrow> ?P t"
         using Fun.prems wf_trm_subtermeq term.le_less_trans Fun_param_is_subterm
@@ -438,7 +439,7 @@ proof -
       let ?Q = "\<lambda>c. \<Gamma> (Fun c []) = Var a \<and> public c"
       have " {c. ?Q c} - S = {c. ?P c}" by auto
       hence "infinite {c. ?P c}"
-        using Diff_infinite_finite[OF assms(1) infinite_typed_consts[of a]] 
+        using Diff_infinite_finite[OF assms(1) infinite_typed_consts[of a]]
         by metis
       hence "\<exists>c. ?P c" using not_finite_existsD by blast
       thus ?case using someI_ex[of ?P] by auto
@@ -446,7 +447,7 @@ proof -
       case (Fun f T)
       have f: "0 < arity f" "length T = arity f" "public f" "T \<noteq> []"
         using Fun.prems fun_type_inv unfolding wf\<^sub>t\<^sub>r\<^sub>m_def by auto
-      obtain t' where t': "t' \<in> set T" by (meson all_not_in_conv f(4) set_empty) 
+      obtain t' where t': "t' \<in> set T" by (meson all_not_in_conv f(4) set_empty)
       have "\<And>t. t \<in> set T \<Longrightarrow> ?P t"
         using Fun.prems wf_trm_subtermeq term.le_less_trans Fun_param_is_subterm
         by metis
@@ -455,7 +456,7 @@ proof -
       then obtain c where c: "Fun c [] \<sqsubseteq> fresh_pgwt S t'" "c \<notin> S" using t' by metis
       thus ?case using t' by auto
     qed
-  } thus ?thesis using that assms \<Gamma>_wf'[OF assms(2)] \<Gamma>_wf(1) by blast 
+  } thus ?thesis using that assms \<Gamma>_wf'[OF assms(2)] \<Gamma>_wf(1) by blast
 qed
 
 private lemma fresh_pgwt_subterm_fresh:
@@ -470,13 +471,13 @@ proof -
       let ?Q = "\<lambda>c. \<Gamma> (Fun c []) = Var a \<and> public c"
       have " {c. ?Q c} - S = {c. ?P c}" by auto
       hence "infinite {c. ?P c}"
-        using Diff_infinite_finite[OF assms(1) infinite_typed_consts[of a]] 
+        using Diff_infinite_finite[OF assms(1) infinite_typed_consts[of a]]
         by metis
       hence "\<exists>c. ?P c" using not_finite_existsD by blast
       thus ?case using someI_ex[of ?P] assms(4) by auto
     next
       case (Fun f T)
-      have f: "0 < arity f" "length T = arity f" "public f" 
+      have f: "0 < arity f" "length T = arity f" "public f"
         using Fun.prems fun_type_inv unfolding wf\<^sub>t\<^sub>r\<^sub>m_def by auto
       have "\<And>t. t \<in> set T \<Longrightarrow> ?P t"
         using Fun.prems wf_trm_subtermeq term.le_less_trans Fun_param_is_subterm
@@ -611,7 +612,7 @@ next
       proof (cases "\<theta> y \<in> subst_range \<sigma> \<and> \<theta> z \<in> subst_range \<sigma>")
         case True
         hence **: "y \<in> subst_domain \<sigma>" "z \<in> subst_domain \<sigma>"
-          using \<theta> \<theta>_dom True * t(3) by (metis Un_iff term.order_refl insertE)+ 
+          using \<theta> \<theta>_dom True * t(3) by (metis Un_iff term.order_refl insertE)+
         hence "y \<noteq> x" "z \<noteq> x" using x_dom by auto
         hence "\<theta> y = \<sigma> y" "\<theta> z = \<sigma> z" using \<theta> by auto
         thus ?thesis using \<open>\<theta> y = \<theta> z\<close> \<sigma>(2) ** unfolding bij_betw_def inj_on_def by auto
@@ -627,9 +628,9 @@ next
   proof -
     { fix s assume "s \<sqsubseteq> t"
       hence "s \<in> {t. {} \<turnstile>\<^sub>c t}  - T"
-        using t(2,3) 
+        using t(2,3)
         by (metis Diff_eq_empty_iff Diff_iff Un_upper1 term.order_refl
-                  deduct_synth_subterm mem_Collect_eq) 
+                  deduct_synth_subterm mem_Collect_eq)
     } thus ?thesis using \<sigma>(3) \<theta> \<theta>_img by auto
   qed
   moreover have "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>" using \<theta> t(1) \<sigma>(5) unfolding wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by auto
@@ -802,7 +803,7 @@ theorem wt_sat_if_simple:
 proof -
   from \<open>wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S \<theta>\<close> have "wf\<^sub>s\<^sub>t {} S" "subst_idem \<theta>" and S_\<theta>_disj: "\<forall>v \<in> vars\<^sub>s\<^sub>t S. \<theta> v = Var v"
     using subst_idemI[of \<theta>] unfolding wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r_def wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by force+
-  
+
   obtain \<I>::"('fun,'var) subst"
     where \<I>: "interpretation\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<I>" "subst_range \<I> \<subseteq> public_ground_wf_terms"
     using wt_interpretation_exists by blast
@@ -857,8 +858,8 @@ proof -
     by (metis \<sigma>_subterm_inj subst_inj_on_is_bij_betw subterm_inj_on_alt_def)
 
   have "finite (subst_domain \<sigma>)" by(metis \<sigma>_fv_dom finite_vars(1))
-  hence \<sigma>_finite_img: "finite (subst_range \<sigma>)" using \<sigma>_bij_dom_img bij_betw_finite by blast 
-  
+  hence \<sigma>_finite_img: "finite (subst_range \<sigma>)" using \<sigma>_bij_dom_img bij_betw_finite by blast
+
   have \<sigma>_img_subterms: "\<forall>s \<in> subst_range \<sigma>. \<forall>u \<in> subst_range \<sigma>. (\<exists>v. v \<sqsubseteq> s \<and> v \<sqsubseteq> u) \<longrightarrow> s = u"
     by (metis \<sigma>_subterm_inj subterm_inj_on_alt_def')
 
@@ -879,13 +880,13 @@ proof -
 
   have \<sigma>_dom_bvars_disj: "\<forall>X F. Inequality X F \<in> set S \<longrightarrow> subst_domain \<sigma> \<inter> set X = {}"
     using ineqs_vars_not_bound \<sigma>_fv_dom by fastforce
-  
+
   have \<I>'1: "\<forall>X F \<delta>. Inequality X F \<in> set S \<longrightarrow> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F - set X \<subseteq> subst_domain \<I>'"
     using \<I>'(3) ineqs_vars_not_bound by fastforce
-  
+
   have \<I>'2: "\<forall>X F. Inequality X F \<in> set S \<longrightarrow> subst_domain \<I>' \<inter> set X = {}"
     using \<I>'(3) ineqs_vars_not_bound by blast
-  
+
   have doms_eq: "subst_domain \<I>' = subst_domain \<sigma>" using \<I>'(3) \<sigma>_fv_dom by simp
 
   have \<sigma>_ineqs_neq: "ineq_model \<sigma> X F" when "Inequality X F \<in> set S" for X F
@@ -911,13 +912,13 @@ proof -
     have "t \<cdot> \<delta> \<cdot> \<sigma> \<noteq> t' \<cdot> \<delta> \<cdot> \<sigma>" when "?P \<delta> X" for \<delta>
     proof -
       have tfr_assms: "Q1 F X \<or> Q2 F X" using tfr_ineq F_in by metis
-  
+
       have "Q1 F X \<Longrightarrow> \<forall>x \<in> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F - set X. \<exists>c. \<sigma> x = Fun c []"
       proof
         fix x assume "Q1 F X" and x: "x \<in> fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F - set X"
         then obtain a where "\<Gamma> (Var x) = TAtom a" unfolding Q1_def by moura
         hence a: "\<Gamma> (\<sigma> x) = TAtom a" using \<sigma>_wt unfolding wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by simp
-        
+
         have "x \<in> subst_domain \<sigma>" using \<sigma>_ineqs_fv_dom x F_in by auto
         then obtain f T where fT: "\<sigma> x = Fun f T" by (meson \<sigma>_img_ground ground_img_obtain_fun)
         hence "T = []" using \<sigma>_wf_trm a TAtom_term_cases by fastforce
@@ -925,9 +926,9 @@ proof -
       qed
       hence 1: "Q1 F X \<Longrightarrow> \<forall>x \<in> (fv t \<union> fv t') - set X. \<exists>c. \<sigma> x = Fun c []"
         using t_fv by auto
-  
+
       have 2: "\<not>Q1 F X \<Longrightarrow> Q2 F X" by (metis tfr_assms)
-  
+
       have 3: "subst_domain \<sigma> \<inter> set X = {}" using \<sigma>_dom_bvars_disj F_in by auto
 
       have 4: "subterms\<^sub>s\<^sub>e\<^sub>t (subst_range \<sigma>) \<inter> (subterms t \<union> subterms t') = {}"
@@ -949,16 +950,16 @@ proof -
           by blast+
         thus ?thesis using * by blast
       qed
-  
+
       have 5: "(fv t \<union> fv t') - subst_domain \<sigma> \<subseteq> set X"
         using \<sigma>_ineqs_fv_dom[OF F_in] t_fv
         by auto
-  
+
       have 6: "\<forall>\<delta>. ?P \<delta> X \<longrightarrow> t \<cdot> \<delta> \<cdot> \<I>' \<noteq> t' \<cdot> \<delta> \<cdot> \<I>'"
         by (metis t_def t'_def \<I>'(1) F_in ineq_model_singleE ineq_model_single_iff)
-  
+
       have 7: "fv t \<union> fv t' - set X \<subseteq> subst_domain \<I>'" using \<I>'1 F_in t_fv by force
-  
+
       have 8: "subst_domain \<I>' \<inter> set X = {}" using \<I>'2 F_in by auto
 
       have 9: "Q1' t t' X" when "Q1 F X"
@@ -984,11 +985,11 @@ proof -
       qed
 
       note 11 = \<sigma>_subterm_inj \<sigma>_img_ground 3 4 5
-  
+
       note 12 = 6 7 8 \<I>'(2) doms_eq
-  
+
       show "t \<cdot> \<delta> \<cdot> \<sigma> \<noteq> t' \<cdot> \<delta> \<cdot> \<sigma>"
-        using 1 2 9 10 that sat_ineq_subterm_inj_subst[OF 11 _ 12] 
+        using 1 2 9 10 that sat_ineq_subterm_inj_subst[OF 11 _ 12]
         unfolding Q1'_def Q2'_def by metis
     qed
     thus ?thesis by (metis t_def t'_def ineq_model_singleI ineq_model_single_iff)
@@ -1021,7 +1022,7 @@ proof -
       using subst_fv_dom_ground_if_ground_img[OF _ \<sigma>_img_ground] by metis+
     thus ?case using g Cons by (auto simp add: subst_apply_pairs_def)
   qed (simp add: subst_apply_pairs_def)
- 
+
   from \<sigma>_pgwt_img \<sigma>_ineqs_neq have \<sigma>_deduct: "M \<turnstile>\<^sub>c \<sigma> x" when "x \<in> subst_domain \<sigma>" for x M
     using that pgwt_deducible by fastforce
 
@@ -1034,7 +1035,7 @@ proof -
       hence "\<And>M. M \<turnstile>\<^sub>c Var v \<cdot> (\<theta> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<I>)"
         using \<I>_deduct \<sigma>_deduct
         by (metis ideduct_synth_subst_apply subst_apply_term.simps(1)
-                  subst_subst_compose trm_subst_ident') 
+                  subst_subst_compose trm_subst_ident')
       thus ?case using strand_sem_append(1)[OF S_sat] by (metis strand_sem_c.simps(1,2))
     next
       case (ConsIneq X F S)
@@ -1099,7 +1100,7 @@ proof -
   obtain S' \<theta>' where *: "simple S'" "(S,\<theta>) \<leadsto>\<^sup>* (S',\<theta>')" "\<lbrakk>{}; S'\<rbrakk>\<^sub>c \<I>"
     using LI_completeness[OF assms(3,2)] unfolding constr_sem_c_def
     by (meson term.order_refl)
-  have **: "wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S' \<theta>'" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>'" "list_all tfr\<^sub>s\<^sub>t\<^sub>p S'" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (trms\<^sub>s\<^sub>t S')" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<theta>')" 
+  have **: "wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S' \<theta>'" "wt\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>'" "list_all tfr\<^sub>s\<^sub>t\<^sub>p S'" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (trms\<^sub>s\<^sub>t S')" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<theta>')"
     using LI_preserves_welltypedness[OF *(2) assms(3,4,7) tfr]
           LI_preserves_wellformedness[OF *(2) assms(3)]
           LI_preserves_tfr[OF *(2) assms(3,4,7) tfr]
@@ -1479,7 +1480,7 @@ private lemma assignment_rhs\<^sub>e\<^sub>s\<^sub>t_append:
 by (metis assignment_rhs_append to_st_append)
 
 private lemma ik\<^sub>e\<^sub>s\<^sub>t_cons: "ik\<^sub>e\<^sub>s\<^sub>t (a#A) = ik\<^sub>e\<^sub>s\<^sub>t [a] \<union> ik\<^sub>e\<^sub>s\<^sub>t A"
-by (metis ik_append to_st_cons) 
+by (metis ik_append to_st_cons)
 
 private lemma ik\<^sub>e\<^sub>s\<^sub>t_append_subst:
   "ik\<^sub>e\<^sub>s\<^sub>t (A@B \<cdot>\<^sub>e\<^sub>s\<^sub>t \<theta>) = ik\<^sub>e\<^sub>s\<^sub>t (A \<cdot>\<^sub>e\<^sub>s\<^sub>t \<theta>) \<union> ik\<^sub>e\<^sub>s\<^sub>t (B \<cdot>\<^sub>e\<^sub>s\<^sub>t \<theta>)"
@@ -1565,7 +1566,7 @@ private lemma decomps\<^sub>e\<^sub>s\<^sub>t_assignment_rhs_empty:
   shows "assignment_rhs\<^sub>e\<^sub>s\<^sub>t A' = {}"
 using assms
 by (induction A' rule: decomps\<^sub>e\<^sub>s\<^sub>t.induct)
-   (simp_all add: decomp_assignment_rhs_empty assignment_rhs\<^sub>e\<^sub>s\<^sub>t_append) 
+   (simp_all add: decomp_assignment_rhs_empty assignment_rhs\<^sub>e\<^sub>s\<^sub>t_append)
 
 private lemma decomps\<^sub>e\<^sub>s\<^sub>t_finite_ik_append:
   assumes "finite M" "M \<subseteq> decomps\<^sub>e\<^sub>s\<^sub>t A N \<I>"
@@ -1856,7 +1857,7 @@ next
     }
     ultimately show ?case by force
   qed simp
-  
+
   { fix k assume "k \<in> set K"
     hence "ik\<^sub>e\<^sub>s\<^sub>t A \<union> M\<^sub>0 \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I> \<turnstile>\<^sub>c k \<cdot> \<I>" using Decompose.hyps by auto
     hence "ik\<^sub>e\<^sub>s\<^sub>t (decomp_rm\<^sub>e\<^sub>s\<^sub>t A) \<union> M\<^sub>0 \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I> \<turnstile> k \<cdot> \<I>"
@@ -1870,7 +1871,7 @@ next
     qed simp
   }
   hence **: "\<And>k. k \<in> set (K \<cdot>\<^sub>l\<^sub>i\<^sub>s\<^sub>t \<I>) \<Longrightarrow> ik\<^sub>e\<^sub>s\<^sub>t (decomp_rm\<^sub>e\<^sub>s\<^sub>t A) \<union> M\<^sub>0 \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I> \<turnstile> k" by auto
-  
+
   show ?case
   proof (cases "t \<in> ik\<^sub>e\<^sub>s\<^sub>t A \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>")
     case True thus ?thesis using Decompose.IH Decompose.prems(2) decomp_rm\<^sub>e\<^sub>s\<^sub>t_append by auto
@@ -1963,7 +1964,7 @@ proof (induction D rule: decomps\<^sub>e\<^sub>s\<^sub>t.induct)
   case (Decomp D f T K M) show ?case
     using sem\<^sub>e\<^sub>s\<^sub>t_c.Decompose[OF Decomp.IH[OF Decomp.prems] _ Decomp.hyps(3)]
           Decomp.hyps(5,6) ideduct_synth_mono ik\<^sub>e\<^sub>s\<^sub>t_append
-    by (metis (mono_tags, lifting) List.append_assoc image_Un sup_ge1) 
+    by (metis (mono_tags, lifting) List.append_assoc image_Un sup_ge1)
 qed auto
 
 private lemma decomps\<^sub>e\<^sub>s\<^sub>t_exist_aux:
@@ -2003,7 +2004,7 @@ proof -
     obtain D'' where D'': "D'' \<in> decomps\<^sub>e\<^sub>s\<^sub>t M N \<I>" "M \<union> ik\<^sub>e\<^sub>s\<^sub>t D'' \<turnstile>\<^sub>c t" by (metis Decompose.IH(1))
     obtain f X where fX: "t = Fun f X" "t\<^sub>i \<in> set X"
       using Decompose.hyps(2,4) by (cases t) (auto dest: Ana_fun_subterm)
-  
+
     from decomps\<^sub>e\<^sub>s\<^sub>t_append[OF D'(1) D''(1)] D'(2) D''(2) have *:
         "D'@D'' \<in> decomps\<^sub>e\<^sub>s\<^sub>t M N \<I>" "\<And>k. k \<in> set K \<Longrightarrow> M \<union> ik\<^sub>e\<^sub>s\<^sub>t (D'@D'') \<turnstile>\<^sub>c k"
         "M \<union> ik\<^sub>e\<^sub>s\<^sub>t (D'@D'') \<turnstile>\<^sub>c t"
@@ -2086,7 +2087,7 @@ proof -
         "ik\<^sub>e\<^sub>s\<^sub>t (A@[a]) \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I> = (ik\<^sub>e\<^sub>s\<^sub>t A \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>) \<union> (ik\<^sub>e\<^sub>s\<^sub>t [a] \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>)"
       using well_analyzed_split_left[OF snoc.prems(2)]
       by (auto simp add: to_st_append ik\<^sub>e\<^sub>s\<^sub>t_append_subst)
-      
+
     have "ik\<^sub>e\<^sub>s\<^sub>t [a \<cdot>\<^sub>e\<^sub>s\<^sub>t\<^sub>p \<I>] = ik\<^sub>e\<^sub>s\<^sub>t [a] \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>"
     proof (cases a)
       case (Step b) thus ?thesis by (cases b) auto
@@ -2099,7 +2100,7 @@ proof -
         by (auto dest: well_analyzed_inv simp add: ik\<^sub>e\<^sub>s\<^sub>t_append assignment_rhs\<^sub>e\<^sub>s\<^sub>t_append)
       hence "Ana (Fun f T \<cdot> \<I>) = (K \<cdot>\<^sub>l\<^sub>i\<^sub>s\<^sub>t \<I>, M \<cdot>\<^sub>l\<^sub>i\<^sub>s\<^sub>t \<I>)"
         using Ana_t snoc.prems(1)
-        unfolding Ana_invar_subst_def by force 
+        unfolding Ana_invar_subst_def by blast
       ultimately show ?thesis using Decomp t by (auto simp add: decomp_ik)
     qed
     thus ?case using IH unfolding subst_apply_extstrand_def by simp
@@ -2130,7 +2131,7 @@ proof -
         using t Decomp snoc.prems(2)
         by (auto dest: well_analyzed_inv simp add: ik\<^sub>e\<^sub>s\<^sub>t_append assignment_rhs\<^sub>e\<^sub>s\<^sub>t_append)
       hence "Ana (Fun f T \<cdot> \<I>) = (K \<cdot>\<^sub>l\<^sub>i\<^sub>s\<^sub>t \<I>, M \<cdot>\<^sub>l\<^sub>i\<^sub>s\<^sub>t \<I>)"
-        using Ana_t snoc.prems(1) unfolding Ana_invar_subst_def by force 
+        using Ana_t snoc.prems(1) unfolding Ana_invar_subst_def by blast
       ultimately show ?thesis using Decomp t by (auto simp add: decomp_assignment_rhs_empty)
     qed
     thus ?case using IH unfolding subst_apply_extstrand_def by simp
@@ -2196,7 +2197,7 @@ proof -
           have *: "(ik\<^sub>e\<^sub>s\<^sub>t A \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>) \<union> ik\<^sub>e\<^sub>s\<^sub>t (D@[Decomp (Fun f T)]) = (ik\<^sub>e\<^sub>s\<^sub>t A \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>) \<union> ik\<^sub>e\<^sub>s\<^sub>t D \<union> set M"
             using decomp_ik[OF \<open>Ana (Fun f T) = (K,M)\<close>] ik\<^sub>e\<^sub>s\<^sub>t_append[of D "[Decomp (Fun f T)]"]
             by auto
-          
+
           { fix t' assume "(ik\<^sub>e\<^sub>s\<^sub>t A \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>) \<union> ik\<^sub>e\<^sub>s\<^sub>t D \<union> set M \<turnstile>\<^sub>c t'"
             hence "(ik\<^sub>e\<^sub>s\<^sub>t A \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>) \<union> (ik\<^sub>e\<^sub>s\<^sub>t D' \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>) \<turnstile>\<^sub>c t'"
             proof (induction t' rule: intruder_synth_induct)
@@ -2311,7 +2312,7 @@ proof -
       have *: "\<And>m. m \<in> set M \<Longrightarrow> (ik\<^sub>e\<^sub>s\<^sub>t A \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>) \<union> (ik\<^sub>e\<^sub>s\<^sub>t D' \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>) \<turnstile>\<^sub>c m"
         using Ana_fun_subterm[OF \<open>Ana (Fun f T) = (K, M)\<close>] ComposeC.hyps(3)
         by auto
-      
+
       have **: "ik\<^sub>e\<^sub>s\<^sub>t (D@[Decomp (Fun f T)]) = ik\<^sub>e\<^sub>s\<^sub>t D \<union> set M"
         using decomp_ik[OF \<open>Ana (Fun f T) = (K, M)\<close>] ik\<^sub>e\<^sub>s\<^sub>t_append by auto
 
@@ -2347,7 +2348,7 @@ proof (intro conjI)
 
   have "wf\<^sub>s\<^sub>t (wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t ?A) (dual\<^sub>s\<^sub>t S)" using 1 2 3 assms(2) by auto
   thus "\<forall>S \<in> update\<^sub>s\<^sub>t \<S> ?S. wf\<^sub>s\<^sub>t (wfrestrictedvars\<^sub>e\<^sub>s\<^sub>t ?A) (dual\<^sub>s\<^sub>t S)" by (metis 3 \<S>)
-  
+
   have "fv\<^sub>s\<^sub>t S \<inter> bvars\<^sub>s\<^sub>t S = {}"
        "\<forall>S' \<in> \<S>. fv\<^sub>s\<^sub>t S \<inter> bvars\<^sub>s\<^sub>t S' = {}"
        "\<forall>S' \<in> \<S>. fv\<^sub>s\<^sub>t S' \<inter> bvars\<^sub>s\<^sub>t S = {}"
@@ -2495,7 +2496,7 @@ proof (intro conjI)
   moreover have "fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F - set X \<subseteq> fv\<^sub>s\<^sub>t (\<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t # S)" by auto
   ultimately have 5:
       "\<forall>S' \<in> \<S>. (fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F - set X) \<inter> bvars\<^sub>s\<^sub>t S' = {}"
-      "fv\<^sub>e\<^sub>s\<^sub>t ?A = fv\<^sub>e\<^sub>s\<^sub>t \<A> \<union> (fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F - set X)" "bvars\<^sub>e\<^sub>s\<^sub>t ?A = set X \<union> bvars\<^sub>e\<^sub>s\<^sub>t \<A>" 
+      "fv\<^sub>e\<^sub>s\<^sub>t ?A = fv\<^sub>e\<^sub>s\<^sub>t \<A> \<union> (fv\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F - set X)" "bvars\<^sub>e\<^sub>s\<^sub>t ?A = set X \<union> bvars\<^sub>e\<^sub>s\<^sub>t \<A>"
       "\<forall>S \<in> \<S>. fv\<^sub>s\<^sub>t S \<inter> set X = {}"
     using to_st_append
     by (blast, force, force, force)
@@ -2566,7 +2567,7 @@ proof -
   have "(trms\<^sub>e\<^sub>s\<^sub>t \<A>') = (trms\<^sub>e\<^sub>s\<^sub>t \<A>) \<union> {t}" "\<Union>(trms\<^sub>s\<^sub>t ` \<S>') \<union> {t} = \<Union>(trms\<^sub>s\<^sub>t ` \<S>)"
     using to_st_append trms\<^sub>s\<^sub>t_update\<^sub>s\<^sub>t_eq[OF assms(1)] assms(2,3) by auto
   thus ?thesis
-    by (metis (no_types, lifting) Un_insert_left Un_insert_right sup_bot.right_neutral) 
+    by (metis (no_types, lifting) Un_insert_left Un_insert_right sup_bot.right_neutral)
 qed
 
 private lemma trms\<^sub>s\<^sub>t_update\<^sub>s\<^sub>t_eq_eq:
@@ -2595,11 +2596,11 @@ private lemma ik\<^sub>s\<^sub>t_update\<^sub>s\<^sub>t_subset:
 proof -
   { fix t assume "t \<in> \<Union>(ik\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t ` (update\<^sub>s\<^sub>t \<S> (x#S)))"
     then obtain S' where S': "S' \<in> update\<^sub>s\<^sub>t \<S> (x#S)" "t \<in> ik\<^sub>s\<^sub>t (dual\<^sub>s\<^sub>t S')" by auto
-  
+
     have *: "ik\<^sub>s\<^sub>t (dual\<^sub>s\<^sub>t S) \<subseteq> ik\<^sub>s\<^sub>t (dual\<^sub>s\<^sub>t (x#S))"
       using ik_append[of "dual\<^sub>s\<^sub>t [x]" "dual\<^sub>s\<^sub>t S"] dual\<^sub>s\<^sub>t_append[of "[x]" S]
       by auto
-  
+
     hence "t \<in> \<Union>(ik\<^sub>s\<^sub>t`dual\<^sub>s\<^sub>t ` \<S>)"
     proof (cases "S' = S")
       case True thus ?thesis using * assms S' by auto
@@ -2610,7 +2611,7 @@ proof -
   moreover
   { fix t assume "t \<in> \<Union>(assignment_rhs\<^sub>s\<^sub>t ` (update\<^sub>s\<^sub>t \<S> (x#S)))"
     then obtain S' where S': "S' \<in> update\<^sub>s\<^sub>t \<S> (x#S)" "t \<in> assignment_rhs\<^sub>s\<^sub>t S'" by auto
-  
+
     have "assignment_rhs\<^sub>s\<^sub>t S \<subseteq> assignment_rhs\<^sub>s\<^sub>t (x#S)"
       using assignment_rhs_append[of "[x]" S] by simp
     hence "t \<in> \<Union>(assignment_rhs\<^sub>s\<^sub>t ` \<S>)"
@@ -2700,7 +2701,7 @@ proof -
     when "a = Check"
   proof -
     show ?C using that assms(2,3) by (simp add: assignment_rhs\<^sub>e\<^sub>s\<^sub>t_append)
-    show ?D using assms(1,2,3) ik\<^sub>s\<^sub>t_update\<^sub>s\<^sub>t_subset(2) by auto 
+    show ?D using assms(1,2,3) ik\<^sub>s\<^sub>t_update\<^sub>s\<^sub>t_subset(2) by auto
   qed
 
   show ?A using 1 2 by (metis subsetI)
@@ -2869,7 +2870,7 @@ proof (induction rule: rtranclp_induct2)
       by (metis UN_E Un_iff)
     have "t \<in> subterms\<^sub>s\<^sub>e\<^sub>t (trms\<^sub>e\<^sub>s\<^sub>t \<A>1)" using trms\<^sub>e\<^sub>s\<^sub>t_ik_assignment_rhsI t by auto
     hence "Fun f T \<in> SMP (trms\<^sub>e\<^sub>s\<^sub>t \<A>1)"
-      by (metis (no_types) SMP.MP SMP.Subterm UN_E t(2)) 
+      by (metis (no_types) SMP.MP SMP.Subterm UN_E t(2))
     hence "{Fun f T} \<subseteq> SMP (trms\<^sub>e\<^sub>s\<^sub>t \<A>1)" using SMP.Subterm[of "Fun f T"] by auto
     moreover have "trms\<^sub>e\<^sub>s\<^sub>t \<A>2 = insert (Fun f T) (trms\<^sub>e\<^sub>s\<^sub>t \<A>1)"
       using Decompose.hyps(3) by auto
@@ -2880,10 +2881,10 @@ proof (induction rule: rtranclp_induct2)
       using Decompose.hyps(2) SMP_union by auto
     moreover have "\<forall>t \<in> trms\<^sub>e\<^sub>s\<^sub>t \<A>1. wf\<^sub>t\<^sub>r\<^sub>m t" "wf\<^sub>t\<^sub>r\<^sub>m (Fun f T)"
       using Decompose.prems wf_trm_subterm t(2) t_wf unfolding tfr\<^sub>s\<^sub>e\<^sub>t_def by auto
-    hence "\<forall>t \<in> trms\<^sub>e\<^sub>s\<^sub>t \<A>2. wf\<^sub>t\<^sub>r\<^sub>m t" by (metis * SMP.MP SMP_wf_trm) 
+    hence "\<forall>t \<in> trms\<^sub>e\<^sub>s\<^sub>t \<A>2. wf\<^sub>t\<^sub>r\<^sub>m t" by (metis * SMP.MP SMP_wf_trm)
     hence "\<forall>t \<in> (\<Union>(trms\<^sub>s\<^sub>t ` \<S>2)) \<union> (trms\<^sub>e\<^sub>s\<^sub>t \<A>2). wf\<^sub>t\<^sub>r\<^sub>m t"
       using Decompose.prems Decompose.hyps(2) unfolding tfr\<^sub>s\<^sub>e\<^sub>t_def by force
-    ultimately show ?thesis using Decompose.prems unfolding tfr\<^sub>s\<^sub>e\<^sub>t_def by presburger 
+    ultimately show ?thesis using Decompose.prems unfolding tfr\<^sub>s\<^sub>e\<^sub>t_def by presburger
   qed (metis trms\<^sub>s\<^sub>t_update\<^sub>s\<^sub>t_eq_snd, metis trms\<^sub>s\<^sub>t_update\<^sub>s\<^sub>t_eq_rcv,
        metis trms\<^sub>s\<^sub>t_update\<^sub>s\<^sub>t_eq_eq, metis trms\<^sub>s\<^sub>t_update\<^sub>s\<^sub>t_eq_ineq)
 qed metis
@@ -2941,7 +2942,7 @@ proof (induction rule: rtranclp_induct2)
     hence 4: "\<forall>S \<in> {to_st \<A>2}. list_all tfr\<^sub>s\<^sub>t\<^sub>p S" using Equality by simp
     have 5: "\<S>2 = insert S (\<S>1 - {\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t#S})" "\<forall>S \<in> \<S>1. list_all tfr\<^sub>s\<^sub>t\<^sub>p S"
       using Equality by simp_all
-    have 6: "\<forall>S \<in> \<S>2. list_all tfr\<^sub>s\<^sub>t\<^sub>p S" 
+    have 6: "\<forall>S \<in> \<S>2. list_all tfr\<^sub>s\<^sub>t\<^sub>p S"
     proof
       fix S' assume "S' \<in> \<S>2"
       hence "S' \<in> \<S>1 \<or> S' = S" using 5(1) by auto
@@ -3021,7 +3022,7 @@ proof (induction rule: rtranclp_induct2)
           "\<Union>(assignment_rhs\<^sub>s\<^sub>t ` \<S>1) = \<Union>(assignment_rhs\<^sub>s\<^sub>t ` \<S>2)"
       by force+
     thus ?case using Nil by metis
-  next 
+  next
     case Send show ?case
       using ik\<^sub>s\<^sub>t_update\<^sub>s\<^sub>t_subset_snd[OF Send.hyps]
             Ana_invar_subst_subset[OF Send.prems]
@@ -3060,7 +3061,7 @@ proof (induction rule: rtranclp_induct2)
             \<or> Fun g S \<in> subterms\<^sub>s\<^sub>e\<^sub>t (assignment_rhs\<^sub>e\<^sub>s\<^sub>t \<A>1)"
         using Decompose * Ana_fun_subterm[OF Ana] by auto
       moreover have "Fun f T \<in> subterms\<^sub>s\<^sub>e\<^sub>t (ik\<^sub>e\<^sub>s\<^sub>t \<A>1 \<union> assignment_rhs\<^sub>e\<^sub>s\<^sub>t \<A>1)"
-        using trms\<^sub>e\<^sub>s\<^sub>t_ik_subtermsI Decompose.hyps(1) by auto 
+        using trms\<^sub>e\<^sub>s\<^sub>t_ik_subtermsI Decompose.hyps(1) by auto
       hence "subterms (Fun f T) \<subseteq> subterms\<^sub>s\<^sub>e\<^sub>t (ik\<^sub>e\<^sub>s\<^sub>t \<A>1 \<union> assignment_rhs\<^sub>e\<^sub>s\<^sub>t \<A>1)"
         by (metis in_subterms_subset_Union)
       hence "subterms\<^sub>s\<^sub>e\<^sub>t (set M) \<subseteq> subterms\<^sub>s\<^sub>e\<^sub>t (ik\<^sub>e\<^sub>s\<^sub>t \<A>1 \<union> assignment_rhs\<^sub>e\<^sub>s\<^sub>t \<A>1)"
@@ -3085,7 +3086,7 @@ proof (induction rule: rtranclp_induct2)
   show ?case
   proof (induction rule: pts_symbolic_c_induct)
     case Nil thus ?case by auto
-  next 
+  next
     case (Send t S)
     hence "fv\<^sub>e\<^sub>s\<^sub>t \<A>2 = fv\<^sub>e\<^sub>s\<^sub>t \<A>1 \<union> fv t" "bvars\<^sub>e\<^sub>s\<^sub>t \<A>2 = bvars\<^sub>e\<^sub>s\<^sub>t \<A>1"
           "fv\<^sub>s\<^sub>t (send\<langle>t\<rangle>\<^sub>s\<^sub>t#S) = fv t \<union> fv\<^sub>s\<^sub>t S"
@@ -3185,8 +3186,8 @@ next
     moreover have "(\<S>1, \<A>1d) \<Rightarrow>\<^sup>\<bullet>\<^sub>c (\<S>2, \<A>1d@[Step (receive\<langle>t\<rangle>\<^sub>s\<^sub>t)])"
       using Send.hyps(2) pts_symbolic_c.Send[OF Send.hyps(1), of \<A>1d] by simp
     moreover have "to_st (decomp_rm\<^sub>e\<^sub>s\<^sub>t (\<A>1d@[Step (receive\<langle>t\<rangle>\<^sub>s\<^sub>t)])) = \<A>2"
-      using Send.hyps(3) decomp_rm\<^sub>e\<^sub>s\<^sub>t_append \<A>1d(1) by (simp add: to_st_append) 
-    ultimately show ?case using \<A>1d(2) by auto      
+      using Send.hyps(3) decomp_rm\<^sub>e\<^sub>s\<^sub>t_append \<A>1d(1) by (simp add: to_st_append)
+    ultimately show ?case using \<A>1d(2) by auto
   next
     case (Equality a t t' S)
     hence "t \<cdot> \<I> = t' \<cdot> \<I>"
@@ -3197,7 +3198,7 @@ next
     moreover have "(\<S>1, \<A>1d) \<Rightarrow>\<^sup>\<bullet>\<^sub>c (\<S>2, \<A>1d@[Step (\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t)])"
       using Equality.hyps(2) pts_symbolic_c.Equality[OF Equality.hyps(1), of \<A>1d] by simp
     moreover have "to_st (decomp_rm\<^sub>e\<^sub>s\<^sub>t (\<A>1d@[Step (\<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t)])) = \<A>2"
-      using Equality.hyps(3) decomp_rm\<^sub>e\<^sub>s\<^sub>t_append \<A>1d(1) by (simp add: to_st_append) 
+      using Equality.hyps(3) decomp_rm\<^sub>e\<^sub>s\<^sub>t_append \<A>1d(1) by (simp add: to_st_append)
     ultimately show ?case using \<A>1d(2) by auto
   next
     case (Inequality X F S)
@@ -3209,7 +3210,7 @@ next
     moreover have "(\<S>1, \<A>1d) \<Rightarrow>\<^sup>\<bullet>\<^sub>c (\<S>2, \<A>1d@[Step (\<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t)])"
       using Inequality.hyps(2) pts_symbolic_c.Inequality[OF Inequality.hyps(1), of \<A>1d] by simp
     moreover have "to_st (decomp_rm\<^sub>e\<^sub>s\<^sub>t (\<A>1d@[Step (\<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t)])) = \<A>2"
-      using Inequality.hyps(3) decomp_rm\<^sub>e\<^sub>s\<^sub>t_append \<A>1d(1) by (simp add: to_st_append) 
+      using Inequality.hyps(3) decomp_rm\<^sub>e\<^sub>s\<^sub>t_append \<A>1d(1) by (simp add: to_st_append)
     ultimately show ?case using \<A>1d(2) by auto
   next
     case (Receive t S)
@@ -3235,7 +3236,7 @@ next
         "D \<in> decomps\<^sub>e\<^sub>s\<^sub>t (ik\<^sub>e\<^sub>s\<^sub>t \<A>1d) (assignment_rhs\<^sub>e\<^sub>s\<^sub>t \<A>1d) \<I>"
         "ik\<^sub>e\<^sub>s\<^sub>t (\<A>1d@D) \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I> \<turnstile>\<^sub>c t \<cdot> \<I>"
       using decomps\<^sub>e\<^sub>s\<^sub>t_exist_subst[OF * \<A>1d(3) ** assms(8)] unfolding Ana_invar_subst_def by auto
-    
+
     have "(\<S>, \<A>\<^sub>d) \<Rightarrow>\<^sup>\<bullet>\<^sub>c\<^sup>* (\<S>1, \<A>1d@D)" using \<A>1d(2) decomps\<^sub>e\<^sub>s\<^sub>t_pts_symbolic_c[OF D(1), of \<S>1] by auto
     hence "(\<S>, \<A>\<^sub>d) \<Rightarrow>\<^sup>\<bullet>\<^sub>c\<^sup>* (\<S>2, \<A>1d@D@[Step (send\<langle>t\<rangle>\<^sub>s\<^sub>t)])"
       using Receive(2) pts_symbolic_c.Receive[OF Receive.hyps(1), of "\<A>1d@D"] by auto
@@ -3266,15 +3267,15 @@ proof -
         by (simp add: decomp_rm\<^sub>e\<^sub>s\<^sub>t_append to_st_append)
     next
       case (Receive t S) thus ?case
-        using pts_symbolic.Receive[OF Receive.hyps(1), of "to_st (decomp_rm\<^sub>e\<^sub>s\<^sub>t \<A>1)"] 
+        using pts_symbolic.Receive[OF Receive.hyps(1), of "to_st (decomp_rm\<^sub>e\<^sub>s\<^sub>t \<A>1)"]
         by (simp add: decomp_rm\<^sub>e\<^sub>s\<^sub>t_append to_st_append)
     next
       case (Equality a t t' S) thus ?case
-        using pts_symbolic.Equality[OF Equality.hyps(1), of "to_st (decomp_rm\<^sub>e\<^sub>s\<^sub>t \<A>1)"] 
+        using pts_symbolic.Equality[OF Equality.hyps(1), of "to_st (decomp_rm\<^sub>e\<^sub>s\<^sub>t \<A>1)"]
         by (simp add: decomp_rm\<^sub>e\<^sub>s\<^sub>t_append to_st_append)
     next
       case (Inequality t t' S) thus ?case
-        using pts_symbolic.Inequality[OF Inequality.hyps(1), of "to_st (decomp_rm\<^sub>e\<^sub>s\<^sub>t \<A>1)"] 
+        using pts_symbolic.Inequality[OF Inequality.hyps(1), of "to_st (decomp_rm\<^sub>e\<^sub>s\<^sub>t \<A>1)"]
         by (simp add: decomp_rm\<^sub>e\<^sub>s\<^sub>t_append to_st_append)
     next
       case (Decompose t) thus ?case using decomp_rm\<^sub>e\<^sub>s\<^sub>t_append by simp
@@ -3345,7 +3346,7 @@ proof
         { assume "t \<in> set T" "t \<noteq> t'"
           hence "t \<sqsubset> t'" using Ana_subterm[OF Ana_t'] by blast
           hence ?thesis using SMP.Subterm[OF SMP.MP[OF ****(2)]] by auto
-        } 
+        }
         ultimately show ?thesis using Decomp by auto
       qed auto
     qed
@@ -3436,7 +3437,7 @@ proof -
 
   have "fv\<^sub>s\<^sub>t (dual\<^sub>s\<^sub>t \<A>) \<inter> bvars\<^sub>s\<^sub>t (dual\<^sub>s\<^sub>t \<A>) = {}" using assms(2) dual\<^sub>s\<^sub>t_fv dual\<^sub>s\<^sub>t_bvars by metis+
   hence 1: "wf\<^sub>s\<^sub>t\<^sub>s {dual\<^sub>s\<^sub>t \<A>}" using assms(1,2) dual\<^sub>s\<^sub>t_self_inverse[of \<A>] unfolding wf\<^sub>s\<^sub>t\<^sub>s_def by auto
-  
+
   have "\<Union>(trms\<^sub>s\<^sub>t ` {\<A>}) = trms\<^sub>s\<^sub>t \<A>" "\<Union>(trms\<^sub>s\<^sub>t ` {dual\<^sub>s\<^sub>t \<A>}) = trms\<^sub>s\<^sub>t (dual\<^sub>s\<^sub>t \<A>)" by auto
   hence "tfr\<^sub>s\<^sub>e\<^sub>t (\<Union>(trms\<^sub>s\<^sub>t ` {\<A>}))" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (\<Union>(trms\<^sub>s\<^sub>t ` {\<A>}))"
         "(\<Union>(trms\<^sub>s\<^sub>t ` {\<A>})) = \<Union>(trms\<^sub>s\<^sub>t ` {dual\<^sub>s\<^sub>t \<A>})"
diff --git a/Stateful_Protocol_Composition_and_Typing/document/root.tex b/Stateful_Protocol_Composition_and_Typing/document/root.tex
index f545a90..8a462d0 100644
--- a/Stateful_Protocol_Composition_and_Typing/document/root.tex
+++ b/Stateful_Protocol_Composition_and_Typing/document/root.tex
@@ -1,6 +1,6 @@
 \documentclass[10pt,DIV16,a4paper,abstract=true,twoside=semi,openright]
 {scrreprt}
-\usepackage[USenglish]{babel}
+\usepackage[english]{babel}
 \usepackage[numbers, sort&compress]{natbib}
 \usepackage{isabelle,isabellesym}
 \usepackage{booktabs}
@@ -22,8 +22,6 @@
   \begingroup% 
   \def\isacharunderscore{\textunderscore}%
   \section{#1 (\thy)}%
-  \def\isacharunderscore{-}%
-  \expandafter\label{sec:\isabellecontext}%
   \endgroup% 
 }
 
@@ -69,9 +67,9 @@
 The rest of this document is automatically generated from the formalization in Isabelle/HOL, i.e., all content is checked by Isabelle.
 The formalization presented in this entry is described in more detail in several publications:
 \begin{itemize}
-\item The typing result (\autoref{sec:Typing{-}Result} ``Typing\_Result'') for stateless protocols, the TLS formalization (\autoref{sec:Example{-}TLS} ``Example\_TLS''), and the theories depending on those (see \autoref{fig:session-graph}) are described in~\cite{hess.ea:formalizing:2017} and~\cite[chapter 3]{hess:typing:2018}.
-\item The typing result for stateful protocols (\autoref{sec:Stateful{-}Typing} ``Stateful\_Typing'') and the keyserver example (\autoref{sec:Example{-}Keyserver} ``Example\_Keyserver'') are described in~\cite{hess.ea:typing:2018} and~\cite[chapter 4]{hess:typing:2018}.
-\item The results on parallel composition for stateless protocols (\autoref{sec:Parallel{-}Compositionality} ``Parallel\_Compositionality'') and stateful protocols (\autoref{sec:Stateful{-}Compositionality} ``Stateful\_Compositionality'') are described in~\cite{hess.ea:stateful:2018} and~\cite[chapter 5]{hess:typing:2018}.
+\item The typing result (\autoref{sec:Typing-Result} ``Typing\_Result'') for stateless protocols, the TLS formalization (\autoref{sec:Example-TLS} ``Example\_TLS''), and the theories depending on those (see \autoref{fig:session-graph}) are described in~\cite{hess.ea:formalizing:2017} and~\cite[chapter 3]{hess:typing:2018}.
+\item The typing result for stateful protocols (\autoref{sec:Stateful-Typing} ``Stateful\_Typing'') and the keyserver example (\autoref{sec:Example-Keyserver} ``Example\_Keyserver'') are described in~\cite{hess.ea:typing:2018} and~\cite[chapter 4]{hess:typing:2018}.
+\item The results on parallel composition for stateless protocols (\autoref{sec:Parallel-Compositionality} ``Parallel\_Compositionality'') and stateful protocols (\autoref{sec:Stateful-Compositionality} ``Stateful\_Compositionality'') are described in~\cite{hess.ea:stateful:2018} and~\cite[chapter 5]{hess:typing:2018}.
 \end{itemize}
 Overall, the structure of this document follows the theory dependencies (see \autoref{fig:session-graph}): we start with introducing the technical preliminaries of our formalization (\autoref{cha:preliminaries}).
 Next, we introduce the typing results in \autoref{cha:typing} and \autoref{cha:stateful-typing}.
@@ -134,8 +132,8 @@ This work is an extension of the work described in~\cite{hess.ea:stateful:2018}
 \chapter{Examples}
 \label{cha:examples}
 In this chapter, we present two examples illustrating our results:
-In \autoref{sec:Example{-}TLS} we show that the TLS example from~\cite{hess.ea:formalizing:2017} is type-flaw resistant.
-In \autoref{sec:Example{-}Keyserver} we show that the keyserver examples from~\cite{hess.ea:typing:2018,hess.ea:stateful:2018} are also type-flaw resistant and that the steps of the composed keyserver protocol from~\cite{hess.ea:stateful:2018} satisfy our conditions for protocol composition. 
+In \autoref{sec:Example-TLS} we show that the TLS example from~\cite{hess.ea:formalizing:2017} is type-flaw resistant.
+In \autoref{sec:Example-Keyserver} we show that the keyserver examples from~\cite{hess.ea:typing:2018,hess.ea:stateful:2018} are also type-flaw resistant and that the steps of the composed keyserver protocol from~\cite{hess.ea:stateful:2018} satisfy our conditions for protocol composition. 
 \input{Example_TLS.tex}
 \input{Example_Keyserver.tex}
 
diff --git a/Stateful_Protocol_Composition_and_Typing/examples/Example_Keyserver.thy b/Stateful_Protocol_Composition_and_Typing/examples/Example_Keyserver.thy
index 0cfb404..0e44673 100644
--- a/Stateful_Protocol_Composition_and_Typing/examples/Example_Keyserver.thy
+++ b/Stateful_Protocol_Composition_and_Typing/examples/Example_Keyserver.thy
@@ -38,6 +38,7 @@ OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 
 
 section \<open>The Keyserver Example\<close>
+text \<open>\label{sec:Example-Keyserver}\<close>
 theory Example_Keyserver
 imports "../Stateful_Compositionality"
 begin
diff --git a/Stateful_Protocol_Composition_and_Typing/examples/Example_TLS.thy b/Stateful_Protocol_Composition_and_Typing/examples/Example_TLS.thy
index 75054f9..78d3d9b 100644
--- a/Stateful_Protocol_Composition_and_Typing/examples/Example_TLS.thy
+++ b/Stateful_Protocol_Composition_and_Typing/examples/Example_TLS.thy
@@ -37,6 +37,7 @@ OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 *)
 
 section \<open>Proving Type-Flaw Resistance of the TLS Handshake Protocol\<close>
+text \<open>\label{sec:Example-TLS}\<close>
 theory Example_TLS
 imports "../Typed_Model"
 begin