diff -r 1481f465e6ea -r c730d018ebfa thys2/SizeBoundStrong.thy
--- a/thys2/SizeBoundStrong.thy	Thu Apr 21 14:58:51 2022 +0100
+++ b/thys2/SizeBoundStrong.thy	Mon Apr 25 17:00:18 2022 +0100
@@ -701,18 +701,28 @@
   apply(simp_all)
   done
 
+lemma bdersStrong_append:
+  shows "bdersStrong r (s1 @ s2) = bdersStrong (bdersStrong r s1) s2"
+  apply(induct s1 arbitrary: r)
+   apply simp+
+  done
+
+
 lemma L_bsimp_ASEQ:
   "L (SEQ (erase r1) (erase r2)) = L (erase (bsimp_ASEQ bs r1 r2))"
   apply(induct bs r1 r2 rule: bsimp_ASEQ.induct)
   apply(simp_all)
   by (metis erase_fuse fuse.simps(4))
 
+
+
 lemma L_bsimp_AALTs:
   "L (erase (AALTs bs rs)) = L (erase (bsimp_AALTs bs rs))"
   apply(induct bs rs rule: bsimp_AALTs.induct)
   apply(simp_all add: erase_fuse)
   done
 
+
 lemma L_erase_AALTs:
   shows "L (erase (AALTs bs rs)) = \<Union> (L ` erase ` (set rs))"
   apply(induct rs)
@@ -971,18 +981,19 @@
   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> 
-                            bsimp_ASEQ bs (pAKC_aux rsa r1 (SEQ  (erase r1) ( ctx) )) r2   |
+                            bsimp_ASEQ bs (pAKC_aux rsa r1 (SEQ  (erase r2) ( ctx) )) r2   |
                                     (AALTs bs rs) \<Rightarrow> 
-                            bsimp_AALTs bs (flts (map (\<lambda>r. pAKC_aux rsa r ( ctx) ) rs))    |
+                            bsimp_AALTs bs (filter (\<lambda>r. r \<noteq> AZERO) (map (\<lambda>r. pAKC_aux rsa r ( ctx) ) rs) )    |
                                     r             \<Rightarrow> r
 )"
 
 
-
 inductive 
   rrewrite:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto> _" [99, 99] 99)
-where
-  "ASEQ bs AZERO r2 \<leadsto> AZERO"
+  where
+ "pAKC_aux rsa a2 ONE = a2' \<Longrightarrow> AALTs bs (rsa @ [a2] @ rsb) \<leadsto> AALTs bs (rsa @ [a2'] @ rsb)"
+
+| "ASEQ bs AZERO r2 \<leadsto> AZERO"
 | "ASEQ bs r1 AZERO \<leadsto> AZERO"
 | "ASEQ bs1 (AONE bs2) r \<leadsto> fuse (bs1@bs2) r"
 | "r1 \<leadsto> r2 \<Longrightarrow> ASEQ bs r1 r3 \<leadsto> ASEQ bs r2 r3"
@@ -994,7 +1005,6 @@
 | "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)"
-| "pAKC_aux rsa a2 ONE = a2' \<Longrightarrow> AALTs bs (rsa @ [a2] @ rsb) \<leadsto> AALTs bs (rsa @ [a2'] @ rsb)"
 
 
 inductive 
@@ -1040,13 +1050,15 @@
 lemma contextrewrites1: "r \<leadsto>* r' \<Longrightarrow> (AALTs bs (r#rs)) \<leadsto>* (AALTs bs (r'#rs))"
   apply(induct r r' rule: rrewrites.induct)
    apply simp
-  by (metis append_Cons append_Nil rrewrite.intros(6) rs2)
+
+  oops
 
 
 lemma contextrewrites2: "r \<leadsto>* r' \<Longrightarrow> (AALTs bs (rs1@[r]@rs)) \<leadsto>* (AALTs bs (rs1@[r']@rs))"
   apply(induct r r' rule: rrewrites.induct)
    apply simp
-  using rrewrite.intros(6) by blast
+  using rrewrite.intros(6) 
+  oops