--- a/thys2/Paper/Paper.thy	Wed Feb 02 22:30:41 2022 +0000
+++ b/thys2/Paper/Paper.thy	Fri Feb 04 00:35:34 2022 +0000
@@ -374,7 +374,7 @@
   @{thm[mode=Axiom] bs6}\qquad
   @{thm[mode=Axiom] bs7}\\
   @{thm[mode=Rule] bs8[of "rs\<^sub>1" "rs\<^sub>2"]}\\
-  @{thm[mode=Axiom] ss1}\qquad
+  %@ { t hm[mode=Axiom] ss1}\qquad
   @{thm[mode=Rule] ss2[of "rs\<^sub>1" "rs\<^sub>2"]}\qquad
   @{thm[mode=Rule] ss3[of "r\<^sub>1" "r\<^sub>2"]}\\
   @{thm[mode=Axiom] ss4}\qquad

--- a/thys2/SizeBound4.thy	Wed Feb 02 22:30:41 2022 +0000
+++ b/thys2/SizeBound4.thy	Fri Feb 04 00:35:34 2022 +0000
@@ -1066,6 +1066,7 @@
 | "asize2 (ASTAR cs r) = Suc (asize2 r)"
 
 
+
 lemma asize2_fuse:
   shows "asize2 (fuse bs r) = asize2 r"
   apply(induct r arbitrary: bs)
@@ -1352,7 +1353,9 @@
   using binullable_intern apply blast
   using binullable_intern apply blast
   by (smt (verit, best) SEQs_eq_image add.commute add_Suc_right card_image_le dual_order.trans finite_pder trans_le_add2)
-  
+
+
+
 lemma
   "card (pder c r) \<le> asize (bsimp (bder c (intern r)))"
   apply(induct c r rule: pder.induct)
@@ -1370,6 +1373,8 @@
   oops
   
 
+
+
 (* below is the idempotency of bsimp *)
 
 lemma bsimp_ASEQ_fuse:

Binary file thys2/paper.pdf has changed