--- 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: