diff -r 426a93160f4a -r 09a57446696a thys2/SizeBoundStrong.thy
--- a/thys2/SizeBoundStrong.thy	Sat Mar 05 11:31:59 2022 +0000
+++ b/thys2/SizeBoundStrong.thy	Mon Mar 07 12:27:27 2022 +0000
@@ -621,12 +621,15 @@
   where
 "dBStrong [] acc = []"
 | "dBStrong (r # rs) acc = (if (erase r) \<in> (set acc) then dBStrong rs acc
-                            else (case (pruneRexp r (addToAcc r acc)) of  
-                                    AZERO \<Rightarrow> dBStrong rs ((addToAcc r acc) @ acc) |
-                                    r1    \<Rightarrow> r1 # (dBStrong rs ((addToAcc r acc) @ acc))
+                            else let newSubRexps = (addToAcc r acc) in 
+                                 (case (pruneRexp r newSubRexps) of  
+                                    AZERO \<Rightarrow> dBStrong rs (newSubRexps @ acc) |
+                                    r1    \<Rightarrow> r1 # (dBStrong rs (newSubRexps @ acc))
                                  )
                            )
                     "
+
+
 fun bsimpStrong :: "arexp \<Rightarrow> arexp "
   where
   "bsimpStrong (ASEQ bs1 r1 r2) = bsimp_ASEQ bs1 (bsimpStrong r1) (bsimpStrong r2)"
@@ -937,6 +940,22 @@
        apply(simp_all)
   done
 
+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) |
+                                    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)"
 
 
 
@@ -955,6 +974,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)"
 
 
 inductive