# HG changeset patch
# User Chengsong
# Date 1644075045 0
# Node ID b85f8e28fbd8b0b0f5319d9a546627243a57dfd7
# Parent  48876e1092f122643df61f543220b317c9b6c2c6# Parent  97f0221add2596535d23797d66b31a9290b3ce35
merge

diff -r 48876e1092f1 -r b85f8e28fbd8 thys2/Paper/Paper.thy
--- a/thys2/Paper/Paper.thy	Sat Feb 05 15:30:01 2022 +0000
+++ b/thys2/Paper/Paper.thy	Sat Feb 05 15:30:45 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
diff -r 48876e1092f1 -r b85f8e28fbd8 thys2/SizeBound4.thy
--- a/thys2/SizeBound4.thy	Sat Feb 05 15:30:01 2022 +0000
+++ b/thys2/SizeBound4.thy	Sat Feb 05 15:30:45 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:
diff -r 48876e1092f1 -r b85f8e28fbd8 thys2/paper.pdf
Binary file thys2/paper.pdf has changed