diff -r c6351a96bf80 -r a7e98deebb5c thys2/SizeBoundStrong.thy
--- a/thys2/SizeBoundStrong.thy	Tue Mar 08 00:50:40 2022 +0000
+++ b/thys2/SizeBoundStrong.thy	Wed Mar 09 17:33:08 2022 +0000
@@ -942,21 +942,14 @@
 
 fun pAKC_aux :: "arexp list \<Rightarrow> arexp \<Rightarrow> rexp \<Rightarrow> arexp"
   where
-"pAKC_aux rsa r ctx = (if (L (SEQ (erase r) ctx)) \<subseteq> (L (erase (AALTs [] rsa))) then AZERO else
-                          case r of (ASEQ bs r1 r2) \<Rightarrow> pAKC_aux rsa r1 (SEQ (erase r1) ctx)     |
-                                    (AALTs bs rs) \<Rightarrow> AALTs bs (map (\<lambda>r. pAKC_aux rsa r ctx) rs) |
+"pAKC_aux rsa r ctx = (if (L (SEQ (erase r) ( ctx) )) \<subseteq> (L (erase (AALTs [] rsa))) then AZERO else
+                          case r of (ASEQ bs r1 r2) \<Rightarrow> 
+                            bsimp_ASEQ bs (pAKC_aux rsa r1 (SEQ  (erase r1) ( ctx) )) r2   |
+                                    (AALTs bs rs) \<Rightarrow> 
+                            bsimp_AALTs bs (flts (map (\<lambda>r. pAKC_aux rsa r ( ctx) ) rs))    |
                                     r             \<Rightarrow> r
 )"
 
-|"pAKC_aux rsa (ASEQ bs1 a1 a2) ctx = (if (L (SEQ (SEQ (erase a1) (erase a2)) ctx)) \<subseteq>
-                                              L (erase (AALTs [] rsa)) 
-                                          then AZERO 
-                                          else (pAKC_aux rsa a1 (ASEQ bs1 a2 ctx)))"
-| "pAKC_aux rsa (AALTs bs1 rs1) ctx = ctx "
-
-fun pruneAwayKnownComponents :: "arexp list \<Rightarrow> arexp \<Rightarrow> arexp" where
-"pruneAwayKnownComponents rsa (ASEQ bs r1 r2) = (pAKC_aux rsa r1 r2)"
-
 
 
 inductive 
@@ -974,7 +967,7 @@
 | "AALTs bs [] \<leadsto> AZERO"
 | "AALTs bs [r] \<leadsto> fuse bs r"
 | "erase a1 = erase a2 \<Longrightarrow> AALTs bs (rsa@[a1]@rsb@[a2]@rsc) \<leadsto> AALTs bs (rsa@[a1]@rsb@rsc)"
-| "pruneAwayKnownComponents rsa a2 = a2' \<Longrightarrow> AALTs bs (rsa @ [a2] @ rsb) \<leadsto> AALTs bs (rsa @ [a2'] @ rsb)"
+| "pAKC_aux rsa a2 ONE = a2' \<Longrightarrow> AALTs bs (rsa @ [a2] @ rsb) \<leadsto> AALTs bs (rsa @ [a2'] @ rsb)"
 
 
 inductive